Implement check for kani::unstable attribute

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -8,6 +8,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::is_proof_harness;
 use crate::kani_middle::attributes::is_test_harness_description;
 use crate::kani_middle::check_crate_items;
+use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items,
@@ -107,6 +108,7 @@ impl CodegenBackend for GotocCodegenBackend {
             return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model());
         }
         dump_mir_items(tcx, &items);
+        check_reachable_items(gcx.tcx, &gcx.queries, &items);
 
         with_timer(
             || {

kani-compiler/src/kani_compiler.rs

@@ -146,6 +146,10 @@ impl Callbacks for KaniCompiler {
             );
             queries.set_reachability_analysis(matches.reachability_type());
 
+            if let Some(features) = matches.get_many::<String>(parser::UNSTABLE_FEATURE) {
+                queries.set_unstable_features(&features.cloned().collect::<Vec<_>>());
+            }
+
             // If appropriate, collect and set the stub mapping.
             if matches.get_flag(parser::ENABLE_STUBBING)
                 && queries.get_reachability_analysis() == ReachabilityType::Harnesses

kani-compiler/src/kani_middle/attributes.rs

@@ -31,23 +31,41 @@ enum KaniAttributeKind {
     Unwind,
 }
 
+impl KaniAttributeKind {
+    /// Returns whether an item is only relevant for harnesses.
+    pub fn is_harness_only(self) -> bool {
+        match self {
+            KaniAttributeKind::Proof
+            | KaniAttributeKind::ShouldPanic
+            | KaniAttributeKind::Solver
+            | KaniAttributeKind::Stub
+            | KaniAttributeKind::Unwind => true,
+            KaniAttributeKind::Unstable => false,
+        }
+    }
+}
+
 /// Check that all attributes assigned to an item is valid.
 /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
 /// the session and emit all errors found.
 pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) {
     let attributes = extract_kani_attributes(tcx, def_id);
-    tracing::info!(?def_id, ?attributes, "check_attributes");
+
+    // Check proof attribute correctness.
     if let Some(proof_attributes) = attributes.get(&KaniAttributeKind::Proof) {
         check_proof_attribute(tcx, def_id, proof_attributes);
-    } else if let Some((kind, attrs)) = attributes.first_key_value() {
-        tcx.sess.span_err(
-            attrs[0].span,
-            format!(
-                "the `{}` attribute also requires the '#[kani::proof]' attribute",
-                kind.as_ref()
-            )
-            .as_str(),
-        );
+    } else {
+        // Emit an error if a harness only attribute is used outside of a harness.
+        for (attr, attrs) in attributes.iter().filter(|(attr, _)| attr.is_harness_only()) {
+            tcx.sess.span_err(
+                attrs[0].span,
+                format!(
+                    "the `{}` attribute also requires the '#[kani::proof]' attribute",
+                    attr.as_ref()
+                )
+                .as_str(),
+            );
+        }
     }
 }
 
@@ -129,6 +147,55 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
     }
 }
 
+/// Check that any unstable API has been enabled. Otherwise, emit an error.
+/// TODO: Improve error message by printing the span of the callee instead of the definition.
+pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
+    let attributes = extract_kani_attributes(tcx, def_id);
+    if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) {
+        for attr in unstable_attrs {
+            match UnstableAttribute::try_from(*attr) {
+                Ok(unstable_attr) => {
+                    if !enabled_features.contains(&unstable_attr.feature) {
+                        let fn_name = tcx.def_path_str(def_id);
+                        let reason =
+                            unstable_attr.reason.map_or(String::default(), |r| format!(": {r}"));
+                        let mut err = tcx.sess.struct_err(format!(
+                            "Use of unstable feature `{}`{reason}",
+                            unstable_attr.feature
+                        ));
+                        err.span_note(
+                            tcx.def_span(def_id),
+                            format!("the function `{fn_name}` is unstable:"),
+                        );
+                        if let Some(link) = unstable_attr.issue {
+                            err.note(format!("see issue {link} for more information"));
+                        }
+                        err.help(format!(
+                            "use `-Z {}` to enable use this API.",
+                            unstable_attr.feature
+                        ));
+                        err.emit();
+                    }
+                }
+                Err(msg) => {
+                    tcx.sess
+                        .struct_span_err(
+                            attr.span,
+                            format!("failed to parse `#[kani::unstable]`: {msg}"),
+                        )
+                        .note(format!(
+                            "expected format: `#[kani::unstable({}, {}, {})]`",
+                            r#"feature="<IDENTIFIER>""#,
+                            r#"issue="<OPTIONAL_ISSUE>""#,
+                            r#"reason="<OPTIONAL_DESCRIPTION>""#
+                        ))
+                        .emit();
+                }
+            }
+        }
+    }
+}
+
 fn expect_single<'a>(
     tcx: TyCtxt,
     kind: KaniAttributeKind,
@@ -183,6 +250,45 @@ fn extract_kani_attributes(
     })
 }
 
+/// Attribute used to mark a Kani lib API unstable.
+#[derive(Debug)]
+struct UnstableAttribute {
+    /// The feature identifier.
+    feature: String,
+    /// A link to the stabilization tracking issue.
+    issue: Option<String>,
+    /// A user friendly message that describes the reason why this feature is marked as unstable.
+    reason: Option<String>,
+}
+
+/// Parse an unstable attribute into an UnstableAttribute structure.
+/// Errors will be reported to the user but aborting the execution is delayed.
+impl TryFrom<&Attribute> for UnstableAttribute {
+    type Error = String;
+    fn try_from(attr: &Attribute) -> Result<Self, Self::Error> {
+        let args = parse_key_values(attr)?;
+        let invalid_keys = args
+            .iter()
+            .filter_map(|(key, _)| {
+                (!matches!(key.as_str(), "feature" | "issue" | "reason")).then_some(key)
+            })
+            .cloned()
+            .collect::<Vec<_>>();
+        if !invalid_keys.is_empty() {
+            Err(format!("unexpected argument `{}`", invalid_keys.join("`, `")))
+        } else {
+            Ok(UnstableAttribute {
+                feature: args
+                    .get("feature")
+                    .ok_or("missing feature identifier".to_string())?
+                    .clone(),
+                issue: args.get("issue").cloned(),
+                reason: args.get("reason").cloned(),
+            })
+        }
+    }
+}
+
 /// Return the unwind value from the given attribute.
 fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
     // Get Attribute value and if it's not none, assign it to the metadata
@@ -348,6 +454,23 @@ fn parse_path(meta_item: &MetaItem) -> Option<String> {
     }
 }
 
+/// Parse the arguments of the attribute into a (key, value) map.
+fn parse_key_values(attr: &Attribute) -> Result<BTreeMap<String, String>, String> {
+    trace!(list=?attr.meta_item_list(), ?attr, "parse_key_values");
+    let args = attr.meta_item_list().ok_or("malformed attribute input")?;
+    args.iter()
+        .map(|arg| match arg.meta_item() {
+            Some(MetaItem { path: key, kind: MetaItemKind::NameValue(val), .. }) => {
+                Ok((key.segments.first().unwrap().ident.to_string(), val.symbol.to_string()))
+            }
+            _ => Err(format!(
+                r#"expected "key = value" pair, but found `{}`"#,
+                rustc_ast_pretty::pprust::meta_list_item_to_string(arg)
+            )),
+        })
+        .collect()
+}
+
 /// If the attribute is named `kanitool::name`, this extracts `name`
 fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
     match &attr.kind {

kani-compiler/src/kani_middle/mod.rs

@@ -3,7 +3,11 @@
 //! This module contains code that are backend agnostic. For example, MIR analysis
 //! and transformations.
 
+use std::collections::HashSet;
+
+use kani_queries::{QueryDb, UserInput};
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
+use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
     FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers,
@@ -15,7 +19,7 @@ use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 
-use self::attributes::check_attributes;
+use self::attributes::{check_attributes, check_unstable_features};
 
 pub mod attributes;
 pub mod coercion;
@@ -50,6 +54,23 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
     tcx.sess.abort_if_errors();
 }
 
+/// Check that all given items are supported and there's no misconfiguration.
+/// This method will exhaustively print any error / warning and it will abort at the end if any
+/// error was found.
+pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) {
+    // Avoid printing the same error multiple times for different instantiations of the same item.
+    let mut def_ids = HashSet::new();
+    for item in items {
+        let def_id = item.def_id();
+        if !def_ids.contains(&def_id) {
+            // Check if any unstable attribute was reached.
+            check_unstable_features(tcx, queries.get_unstable_features(), def_id);
+            def_ids.insert(def_id);
+        }
+    }
+    tcx.sess.abort_if_errors();
+}
+
 struct CompilerHelpers<'tcx> {
     tcx: TyCtxt<'tcx>,
 }

kani-compiler/src/main.rs

@@ -15,6 +15,7 @@
 #![feature(more_qualified_paths)]
 #![feature(iter_intersperse)]
 extern crate rustc_ast;
+extern crate rustc_ast_pretty;
 extern crate rustc_codegen_ssa;
 extern crate rustc_data_structures;
 extern crate rustc_driver;

kani-driver/src/args.rs

@@ -347,7 +347,8 @@ pub enum ConcretePlaybackMode {
     InPlace,
 }
 
-#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)]
+#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)]
+#[strum(serialize_all = "kebab-case")]
 pub enum UnstableFeatures {
     /// Allow replace certain items with stubs (mocks).
     /// See (RFC-0002)[https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html]

kani-driver/src/args_toml.rs

@@ -87,20 +87,40 @@ fn cargo_locate_project(input_args: &[OsString]) -> Result<PathBuf> {
 
 /// Parse a config toml string and extract the cargo-kani arguments we should try injecting.
 /// This returns two different vectors since all cbmc-args have to be at the end.
+/// We currently support the following entries:
+/// - flags: Flags that get directly passed to Kani.
+/// - unstable: Unstable features (it will be passed using `-Z` flag).
+/// The tables supported are:
+/// "workspace.metadata.kani", "package.metadata.kani", "kani"
 fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     let config = tomldata.parse::<Value>()?;
     // To make testing easier, our function contract is to produce a stable ordering of flags for a given input.
     // Consequently, we use BTreeMap instead of HashMap here.
     let mut map: BTreeMap<String, Value> = BTreeMap::new();
-    let tables = ["workspace.metadata.kani.flags", "package.metadata.kani.flags", "kani.flags"];
+    let tables = ["workspace.metadata.kani", "package.metadata.kani", "kani"];
+    let mut args = Vec::new();
 
     for table in tables {
-        if let Some(val) = get_table(&config, table) {
-            map.extend(val.iter().map(|(x, y)| (x.to_owned(), y.to_owned())));
+        if let Some(table) = get_table(&config, table) {
+            if let Some(entry) = table.get("flags") {
+                if let Some(val) = entry.as_table() {
+                    map.extend(val.iter().map(|(x, y)| (x.to_owned(), y.to_owned())));
+                }
+            }
+
+            if let Some(entry) = table.get("unstable") {
+                if let Some(val) = entry.as_table() {
+                    args.append(
+                        &mut val
+                            .iter()
+                            .filter_map(|(k, v)| unstable_entry(k, v).transpose())
+                            .collect::<Result<Vec<_>>>()?,
+                    );
+                }
+            }
         }
     }
 
-    let mut args = Vec::new();
     let mut cbmc_args = Vec::new();
 
     for (flag, value) in map {
@@ -116,6 +136,14 @@ fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     Ok((args, cbmc_args))
 }
 
+fn unstable_entry(name: &String, value: &Value) -> Result<Option<OsString>> {
+    match value {
+        Value::Boolean(b) if *b => Ok(Some(OsString::from(format!("-Z{name}")))),
+        Value::Boolean(b) if !b => Ok(None),
+        _ => bail!("Expected no arguments for unstable feature `{name}` but found {value}"),
+    }
+}
+
 /// Translates one toml entry (flag, value) into arguments and inserts it into `args`
 fn insert_arg_from_toml(flag: &str, value: &Value, args: &mut Vec<OsString>) -> Result<()> {
     match value {

kani-driver/src/call_single_file.rs

@@ -99,6 +99,10 @@ impl KaniSession {
             flags.push(format!("--harness={harness}"));
         }
 
+        flags.extend(
+            self.args.unstable_features.iter().map(|feature| format!("--unstable={feature}")),
+        );
+
         // This argument will select the Kani flavour of the compiler. It will be removed before
         // rustc driver is invoked.
         flags.push("--goto-c".into());

tests/cargo-ui/unstable-attr/defs/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "defs"
+version = "0.1.0"
+edition = "2021"
+description = "define a few fake unstable APIs used in other tests"
+
+[dependencies]
+
+[package.metadata.kani.flags]
+only-codegen = true

tests/cargo-ui/unstable-attr/defs/src/lib.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::unstable(feature = "always_fails", reason = "do not enable", issue = "<link>")]
+pub fn always_fails() {
+    assert!(false, "don't call me");
+}
+
+/// We use "gen-c" since it has to be an existing feature.
+#[kani::unstable(feature = "gen-c", reason = "internal fake api", issue = "<link>")]
+pub fn no_op() {
+    kani::cover!(true);
+}

tests/cargo-ui/unstable-attr/enabled/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "enabled"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+defs = {path = "../defs"}
+
+[package.metadata.kani.unstable]
+gen-c = true

tests/cargo-ui/unstable-attr/enabled/expected

@@ -0,0 +1,4 @@
+Checking harness harness...
+defs::no_op.cover\
+Status: SATISFIED
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/unstable-attr/enabled/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This is just to test that we can call an unstable feature.
+//! We also ensure that non-reachable unstable features do not affect our analysis.
+
+#[kani::proof]
+pub fn harness() {
+    defs::no_op();
+}