Enforce unstable APIs can only be used if the related feature is enab…

…led (#2386)

This PR adds the new opt-in option for users to enable unstable features (via -Z option or unstable table in Cargo.toml). This PR also adds logic to parse and verify APIs tagged with unstable.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

kani-compiler/kani_queries/src/lib.rs

@@ -41,6 +41,9 @@ pub trait UserInput {
 
     fn set_stubbing_enabled(&mut self, stubbing_enabled: bool);
     fn get_stubbing_enabled(&self) -> bool;
+
+    fn set_unstable_features(&mut self, features: &[String]);
+    fn get_unstable_features(&self) -> &[String];
 }
 
 /// This structure should only be used behind a synchronized reference or a snapshot.
@@ -54,6 +57,7 @@ pub struct QueryDb {
     write_json_symtab: bool,
     reachability_analysis: ReachabilityType,
     stubbing_enabled: bool,
+    unstable_features: Vec<String>,
 }
 
 impl QueryDb {
@@ -66,6 +70,7 @@ impl QueryDb {
             write_json_symtab: false,
             reachability_analysis: ReachabilityType::None,
             stubbing_enabled: false,
+            unstable_features: vec![],
         }))
     }
 }
@@ -126,4 +131,12 @@ impl UserInput for QueryDb {
     fn get_write_json_symtab(&self) -> bool {
         self.write_json_symtab
     }
+
+    fn set_unstable_features(&mut self, features: &[String]) {
+        self.unstable_features = Vec::from_iter(features.iter().cloned());
+    }
+
+    fn get_unstable_features(&self) -> &[String] {
+        &self.unstable_features
+    }
 }

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -9,6 +9,7 @@ use crate::kani_middle::analysis;
 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,
@@ -108,6 +109,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

@@ -6,6 +6,7 @@ use std::collections::BTreeMap;
 
 use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
 use rustc_ast::{AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
+use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{self, Instance, TyCtxt};
 use rustc_span::Span;
@@ -31,22 +32,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);
+
+    // 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(),
+            );
+        }
     }
 }
 
@@ -128,6 +148,54 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
     }
 }
 
+/// Check that any unstable API has been enabled. Otherwise, emit an error.
+///
+/// For now, this function will also validate whether the attribute usage is valid, and emit an
+/// error if not.
+///
+/// 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) => {
+                    // Reached an unstable attribute that was not enabled.
+                    report_unstable_forbidden(tcx, def_id, &unstable_attr);
+                }
+                Ok(attr) => debug!(enabled=?attr, ?def_id, "check_unstable_features"),
+                Err(error) => {
+                    // Ideally this check should happen when compiling the crate with the attribute,
+                    // not the crate under verification.
+                    error.report(tcx);
+                    debug_assert!(
+                        false,
+                        "expected well formed unstable attribute, but found: {error:?}"
+                    );
+                }
+            }
+        }
+    }
+}
+
+/// Report misusage of an unstable feature that was not enabled.
+fn report_unstable_forbidden(
+    tcx: TyCtxt,
+    def_id: DefId,
+    unstable_attr: &UnstableAttribute,
+) -> ErrorGuaranteed {
+    let fn_name = tcx.def_path_str(def_id);
+    tcx.sess
+        .struct_err(format!(
+            "Use of unstable feature `{}`: {}",
+            unstable_attr.feature, unstable_attr.reason
+        ))
+        .span_note(tcx.def_span(def_id), format!("the function `{fn_name}` is unstable:"))
+        .note(format!("see issue {} for more information", unstable_attr.issue))
+        .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
+        .emit()
+}
+
 fn expect_single<'a>(
     tcx: TyCtxt,
     kind: KaniAttributeKind,
@@ -182,6 +250,70 @@ 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: String,
+    /// A user friendly message that describes the reason why this feature is marked as unstable.
+    reason: String,
+}
+
+#[derive(Debug)]
+struct UnstableAttrParseError<'a> {
+    /// The reason why the parsing failed.
+    reason: String,
+    /// The attribute being parsed.
+    attr: &'a Attribute,
+}
+
+impl<'a> UnstableAttrParseError<'a> {
+    /// Report the error in a friendly format.
+    fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed {
+        tcx.sess
+            .struct_span_err(
+                self.attr.span,
+                format!("failed to parse `#[kani::unstable]`: {}", self.reason),
+            )
+            .note(format!(
+                "expected format: #[kani::unstable({}, {}, {})]",
+                r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
+            ))
+            .emit()
+    }
+}
+
+/// Try to parse an unstable attribute into an `UnstableAttribute`.
+impl<'a> TryFrom<&'a Attribute> for UnstableAttribute {
+    type Error = UnstableAttrParseError<'a>;
+    fn try_from(attr: &'a Attribute) -> Result<Self, Self::Error> {
+        let build_error = |reason: String| Self::Error { reason, attr };
+        let args = parse_key_values(attr).map_err(build_error)?;
+        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(build_error(format!("unexpected argument `{}`", invalid_keys.join("`, `"))))
+        } else {
+            let get_val = |name: &str| {
+                args.get(name).cloned().ok_or(build_error(format!("missing `{name}` field")))
+            };
+            Ok(UnstableAttribute {
+                feature: get_val("feature")?,
+                issue: get_val("issue")?,
+                reason: get_val("reason")?,
+            })
+        }
+    }
+}
+
 /// 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
@@ -347,6 +479,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 analysis;
 pub mod attributes;
@@ -51,6 +55,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-compiler/src/parser.rs

@@ -46,6 +46,9 @@ pub const HARNESS: &str = "harness";
 /// Option name used to enable stubbing.
 pub const ENABLE_STUBBING: &str = "enable-stubbing";
 
+/// Option name used to define unstable features.
+pub const UNSTABLE_FEATURE: &str = "unstable";
+
 /// Configure command options for the Kani compiler.
 pub fn parser() -> Command {
     let app = command!()
@@ -146,6 +149,13 @@ pub fn parser() -> Command {
                 .long("check-version")
                 .action(ArgAction::Set)
                 .help("Pass the kani version to the compiler to ensure cache coherence."),
+        )
+        .arg(
+            Arg::new(UNSTABLE_FEATURE)
+                .long(UNSTABLE_FEATURE)
+                .help("Enable an unstable feature")
+                .value_name("UNSTABLE_FEATURE")
+                .action(ArgAction::Append),
         );
     app
 }

kani-driver/src/args.rs

@@ -258,6 +258,10 @@ pub struct KaniArgs {
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoArgs,
+
+    /// Enable an unstable feature.
+    #[arg(short = 'Z', num_args(1), value_name = "UNSTABLE_FEATURE")]
+    pub unstable_features: Vec<UnstableFeatures>,
 }
 
 impl KaniArgs {
@@ -304,7 +308,7 @@ pub struct CargoArgs {
     pub no_default_features: bool,
 
     // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
-    /// Comma separated list of features to activate
+    /// Comma separated list of package features to activate
     #[arg(short = 'F', long)]
     features: Vec<String>,
 
@@ -349,6 +353,16 @@ pub enum ConcretePlaybackMode {
     InPlace,
 }
 
+#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)]
+#[strum(serialize_all = "kebab-case")]
+pub enum UnstableFeatures {
+    /// Allow replacing certain items with stubs (mocks).
+    /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html)
+    Stubbing,
+    /// Generate a C-like file equivalent to input program used for debugging purpose.
+    GenC,
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, ValueEnum)]
 pub enum OutputFormat {
     Regular,