Address PR feedback

 - Break down check attribute function
 - Improve comment
 - Add debug_assert for invalid unstable attribute
 - Make all fields required

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;
@@ -148,54 +149,53 @@ 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) {
-                        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 using this API.",
-                            unstable_attr.feature
-                        ));
-                        err.emit();
-                    }
+                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);
                 }
-                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();
+                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,
@@ -256,34 +256,59 @@ struct UnstableAttribute {
     /// The feature identifier.
     feature: String,
     /// A link to the stabilization tracking issue.
-    issue: Option<String>,
+    issue: String,
     /// A user friendly message that describes the reason why this feature is marked as unstable.
-    reason: Option<String>,
+    reason: 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)?;
+#[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 structure.
+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(format!("unexpected argument `{}`", invalid_keys.join("`, `")))
+            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: args
-                    .get("feature")
-                    .ok_or("missing feature identifier".to_string())?
-                    .clone(),
-                issue: args.get("issue").cloned(),
-                reason: args.get("reason").cloned(),
+                feature: get_val("feature")?,
+                issue: get_val("issue")?,
+                reason: get_val("reason")?,
             })
         }
     }

kani-driver/src/args_toml.rs

@@ -136,11 +136,12 @@ fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     Ok((args, cbmc_args))
 }
 
+/// Parse an entry from the unstable table and convert it into a `-Z <unstable_feature>` argument
 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}"),
+        _ => bail!("Expected no arguments for unstable feature `{name}` but found `{value}`"),
     }
 }
 
@@ -216,6 +217,8 @@ fn get_table<'a>(start: &'a Value, table: &str) -> Option<&'a Table> {
 
 #[cfg(test)]
 mod tests {
+    use std::str::FromStr;
+
     use super::*;
 
     #[test]
@@ -265,4 +268,50 @@ mod tests {
         assert_eq!(merged[4], OsString::from("--trace"));
         assert_eq!(merged[5], OsString::from("--fake"));
     }
+
+    #[test]
+    fn check_multiple_table_works() {
+        let data = "[workspace.metadata.kani.unstable]
+                         disabled-feature=false
+                         enabled-feature=true
+                         [workspace.metadata.kani.flags]
+                         kani-arg=\"value\"
+                         cbmc-args=[\"--dummy\"]";
+        let (kani_args, cbmc_args) = toml_to_args(data).unwrap();
+        assert_eq!(kani_args, vec!["-Zenabled-feature", "--kani-arg", "value"]);
+        assert_eq!(cbmc_args, vec!["--cbmc-args", "--dummy"]);
+    }
+
+    #[test]
+    fn check_unstable_table_works() {
+        let data = "[workspace.metadata.kani.unstable]
+                         disabled-feature=false
+                         enabled-feature=true";
+        let (kani_args, cbmc_args) = toml_to_args(data).unwrap();
+        assert_eq!(kani_args, vec!["-Zenabled-feature"]);
+        assert!(cbmc_args.is_empty());
+    }
+
+    #[test]
+    fn check_unstable_entry_enabled() -> Result<()> {
+        let name = String::from("feature");
+        assert_eq!(
+            unstable_entry(&name, &Value::Boolean(true))?,
+            Some(OsString::from_str("-Zfeature")?)
+        );
+        Ok(())
+    }
+
+    #[test]
+    fn check_unstable_entry_disabled() -> Result<()> {
+        let name = String::from("feature");
+        assert_eq!(unstable_entry(&name, &Value::Boolean(false))?, None);
+        Ok(())
+    }
+
+    #[test]
+    fn check_unstable_entry_invalid() {
+        let name = String::from("feature");
+        assert!(matches!(unstable_entry(&name, &Value::String("".to_string())), Err(_)));
+    }
 }

rfc/src/rfcs/0006-unstable-api.md

@@ -63,7 +63,7 @@ unstable = { unstable-options = true }
 In order to mark an API as unstable, we will add the following attribute to the APIs marked as unstable:
 
 ```rust
-#[kani::unstable(feature="<IDENTIFIER>", issue="<TRACKING_ISSUE_NUMBER>", reason="<OPTIONAL_DESCRIPTION>")]
+#[kani::unstable(feature="<IDENTIFIER>", issue="<TRACKING_ISSUE_NUMBER>", reason="<DESCRIPTION>")]
 pub fn unstable_api() {}
 ```
 

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

@@ -1,31 +1,10 @@
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`
-lib.rs\
-|\
-| #[kani::unstable(reason = "just checking", issue = "<link>")]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
-|\
-= note: expected format: `#[kani::unstable(feature="<IDENTIFIER>", issue="<OPTIONAL_ISSUE>", reason="<OPTIONAL_DESCRIPTION>")]`
-
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `1010`
-lib.rs\
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\
+src/lib.rs\
 |\
 | #[kani::unstable(feature("invalid_args"))]\
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-= note: expected format: `#[kani::unstable(feature="<IDENTIFIER>", issue="<OPTIONAL_ISSUE>", reason="<OPTIONAL_DESCRIPTION>")]`
-
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature`
-lib.rs\
-|\
-| #[kani::unstable(feature, issue)]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
-|\
-= note: expected format: `#[kani::unstable(feature="<IDENTIFIER>", issue="<OPTIONAL_ISSUE>", reason="<OPTIONAL_DESCRIPTION>")]`
+= note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]\
+= note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: failed to parse `#[kani::unstable]`: missing feature identifier
-lib.rs\
-|\
-| #[kani::unstable(1010)]\
-| ^^^^^^^^^^^^^^^^^^^^^^^\
-|\
-= note: expected format: `#[kani::unstable(feature="<IDENTIFIER>", issue="<OPTIONAL_ISSUE>", reason="<OPTIONAL_DESCRIPTION>")]`
+error: internal compiler error

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

@@ -1,9 +1,9 @@
 error: Use of unstable feature `always_fails`: do not enable\
 |\
 note: the function `defs::always_fails` is unstable:\
-lib.rs:5:1\
+lib.rs\
 |\
 | pub fn always_fails() {\
 | ^^^^^^^^^^^^^^^^^^^^^\
 = note: see issue <link> for more information\
-= help: use `-Z always_fails` to enable use this API.
+= help: use `-Z always_fails` to enable using this function.