Fix tests + a few more changes

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -11,7 +11,7 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
 };
-use crate::kani_middle::{check_crate_items, check_reachable_items, dump_mir_items};
+use crate::kani_middle::{check_reachable_items, dump_mir_items};
 use crate::kani_queries::{QueryDb, ReachabilityType};
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
@@ -217,7 +217,6 @@ impl CodegenBackend for GotocCodegenBackend {
         let queries = self.queries.lock().unwrap().clone();
         check_target(tcx.sess);
         check_options(tcx.sess);
-        check_crate_items(tcx, queries.ignore_global_asm);
 
         // Codegen all items that need to be processed according to the selected reachability mode:
         //

kani-compiler/src/kani_compiler.rs

@@ -18,6 +18,7 @@
 #[cfg(feature = "cprover")]
 use crate::codegen_cprover_gotoc::GotocCodegenBackend;
 use crate::kani_middle::attributes::is_proof_harness;
+use crate::kani_middle::check_crate_items;
 use crate::kani_middle::metadata::gen_proof_metadata;
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{self, harness_stub_map};
@@ -373,8 +374,10 @@ impl Callbacks for KaniCompiler {
         rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
     ) -> Compilation {
         if self.stage.is_init() {
-            self.stage =
-                rustc_queries.global_ctxt().unwrap().enter(|tcx| self.process_harnesses(tcx));
+            self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| {
+                check_crate_items(tcx, self.queries.lock().unwrap().ignore_global_asm);
+                self.process_harnesses(tcx)
+            });
         }
 
         self.prepare_codegen()

kani-compiler/src/kani_middle/attributes.rs

@@ -113,41 +113,34 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String {
     parse_str_value(&marker).unwrap()
 }
 
-/// Extract all Kani attributes for a given `def_id` if any exists.
+/// Extract harness attributes for a given `def_id`.
+///
 /// We only extract attributes for harnesses that are local to the current crate.
 /// Note that all attributes should be valid by now.
-pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessAttributes> {
+pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttributes {
     // Abort if not local.
-    def_id.as_local()?;
+    assert!(def_id.is_local(), "Expected a local item, but got: {def_id:?}");
     let attributes = extract_kani_attributes(tcx, def_id);
     trace!(?def_id, ?attributes, "extract_harness_attributes");
-    if attributes.contains_key(&KaniAttributeKind::Proof) {
-        Some(attributes.into_iter().fold(
-            HarnessAttributes::default(),
-            |mut harness, (kind, attributes)| {
-                match kind {
-                    KaniAttributeKind::ShouldPanic => harness.should_panic = true,
-                    KaniAttributeKind::Solver => {
-                        harness.solver = parse_solver(tcx, attributes[0]);
-                    }
-                    KaniAttributeKind::Stub => {
-                        harness.stubs = parse_stubs(tcx, def_id, attributes);
-                    }
-                    KaniAttributeKind::Unwind => {
-                        harness.unwind_value = parse_unwind(tcx, attributes[0])
-                    }
-                    KaniAttributeKind::Proof => harness.proof = true,
-                    KaniAttributeKind::Unstable => {
-                        // Internal attribute which shouldn't exist here.
-                        unreachable!()
-                    }
-                };
-                harness
-            },
-        ))
-    } else {
-        None
-    }
+    assert!(attributes.contains_key(&KaniAttributeKind::Proof));
+    attributes.into_iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
+        match kind {
+            KaniAttributeKind::ShouldPanic => harness.should_panic = true,
+            KaniAttributeKind::Solver => {
+                harness.solver = parse_solver(tcx, attributes[0]);
+            }
+            KaniAttributeKind::Stub => {
+                harness.stubs = parse_stubs(tcx, def_id, attributes);
+            }
+            KaniAttributeKind::Unwind => harness.unwind_value = parse_unwind(tcx, attributes[0]),
+            KaniAttributeKind::Proof => harness.proof = true,
+            KaniAttributeKind::Unstable => {
+                // Internal attribute which shouldn't exist here.
+                unreachable!()
+            }
+        };
+        harness
+    })
 }
 
 /// Check that any unstable API has been enabled. Otherwise, emit an error.
@@ -511,9 +504,12 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
         AttrKind::Normal(normal) => {
             let segments = &normal.item.path.segments;
             if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
-                assert_eq!(segments.len(), 2, "Unexpected kani attribute {segments:?}");
-                let ident_str = segments[1].ident.as_str();
-                KaniAttributeKind::try_from(ident_str)
+                let ident_str = segments[1..]
+                    .iter()
+                    .map(|segment| segment.ident.as_str())
+                    .intersperse("::")
+                    .collect::<String>();
+                KaniAttributeKind::try_from(ident_str.as_str())
                     .map_err(|err| {
                         debug!(?err, "attr_kind_failed");
                         tcx.sess.span_err(attr.span, format!("unknown attribute `{ident_str}`"));

kani-compiler/src/kani_middle/metadata.rs

@@ -36,7 +36,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne
         original_file: loc.filename,
         original_start_line: loc.start_line,
         original_end_line: loc.end_line,
-        attributes: attributes.unwrap_or_default(),
+        attributes,
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
     }

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

@@ -1,10 +1,32 @@
-error: failed to parse `#[kani::unstable]`:
-src/lib.rs\
+error: failed to parse `#[kani::unstable]`: missing `feature` field\
+lib.rs
+  |\
+9 | #[kani::unstable(reason = "just checking", issue = "<link>")]\
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+  |\
+  = 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]`: expected "key = value" pair, but found `feature("invalid_args")`\
+lib.rs\
+|\
+| #[kani::unstable(feature("invalid_args"))]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|\
+   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
+
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature`\
+lib.rs\
 |\
-| #[kani::unstable(\
-| ^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable(feature, issue)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-= 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)
+   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
 
-error: internal compiler error
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `1010`\
+lib.rs\
+|\
+| #[kani::unstable(1010)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^\
+|\
+   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]

tests/ui/invalid-attribute/attrs.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that invalid attributes are caught for all crate items
+
+#[kani::stub(invalid=opt)]
+pub fn unreachable_fn() {}
+
+// Also gracefully handle user embedded kanitool.
+#[kanitool::proof(invalid_argument)]
+#[kanitool::invalid::attribute]
+pub fn invalid_kanitool() {}
+
+#[kani::proof]
+pub fn valid_harness() {}

tests/ui/invalid-attribute/expected

@@ -0,0 +1,27 @@
+error: the `stub` attribute also requires the `#[kani::proof]` attribute\
+attrs.rs
+|\
+| #[kani::stub(invalid=opt)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|
+
+error: attribute `kani::stub` takes two path arguments; found 0\
+attrs.rs
+|\
+| #[kani::stub(invalid=opt)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|
+
+error: unknown attribute `invalid::attribute`\
+attrs.rs\
+|\
+| #[kanitool::invalid::attribute]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: unexpected argument for `proof`\
+attrs.rs\
+|\
+| #[kanitool::proof(invalid_argument)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|
+

tests/ui/invalid-harnesses/expected

@@ -1,4 +1,4 @@
-warning: duplicate attribute\
+error: only one '#[kani::proof]' attribute is allowed per harness\
 invalid.rs:\
 |\
 | #[kani::proof]\

tests/ui/logging/warning/expected

@@ -1 +1,4 @@
-warning: duplicate attribute
+warning: Found the following unsupported constructs:
+- TerminatorKind::InlineAsm (1)
+Verification will fail if one or more of these constructs is reachable.
+

tests/ui/logging/warning/trivial.rs

@@ -1,10 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// This test is to make sure we are correctly printing warnings from the kani-compiler.
+// kani-flags: --only-codegen
+//! This test is to make sure we are correctly printing warnings from the kani-compiler.
 
-// FIXME: This should also print a warning:
-// https://github.com/model-checking/kani/issues/922
 pub fn asm() {
     unsafe {
         std::arch::asm!("NOP");
@@ -15,9 +14,15 @@ fn is_true(b: bool) {
     assert!(b);
 }
 
+fn maybe_call<F: Fn() -> ()>(should_call: bool, f: F) {
+    if should_call {
+        f();
+    }
+}
+
 // Duplicate proof harness attributes should produce a warning
 #[kani::proof]
-#[kani::proof]
 fn harness() {
     is_true(true);
+    maybe_call(false, &asm);
 }

tests/ui/multiple-proof-attributes/expected

@@ -1,5 +1,6 @@
-warning: duplicate attribute\
-main.rs:\
+error: only one '#[kani::proof]' attribute is allowed per harness\
+main.rs\
 |\
 | #[kani::proof]\
-| ^^^^^^^^^^^^^^
+| ^^^^^^^^^^^^^^\
+|\