Verify all Kani attributes in all crate items upfront (#2536)

The Kani attributes were being lazily evaluated in some cases. We have also been handling duplicated attribute inconsistently.

Instead, validate all the attributes upfront and print all the errors found. Also, for all attributes that multiple occurrences is redundant, we emit an error if user provides 2 or more.

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

@@ -49,21 +49,49 @@ impl KaniAttributeKind {
 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 {
- // 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()) {
+ // Check that all attributes are correctly used and well formed.
+ let is_harness = attributes.contains_key(&KaniAttributeKind::Proof);
+ for (kind, attrs) in attributes {
+ if !is_harness && kind.is_harness_only() {
  tcx.sess.span_err(
  attrs[0].span,
  format!(
  "the `{}` attribute also requires the `#[kani::proof]` attribute",
- attr.as_ref()
+ kind.as_ref()
  )
  .as_str(),
  );
  }
+ match kind {
+ KaniAttributeKind::ShouldPanic => {
+ expect_single(tcx, kind, &attrs);
+ attrs.iter().for_each(|attr| {
+ expect_no_args(tcx, kind, attr);
+ })
+ }
+ KaniAttributeKind::Solver => {
+ expect_single(tcx, kind, &attrs);
+ attrs.iter().for_each(|attr| {
+ parse_solver(tcx, attr);
+ })
+ }
+ KaniAttributeKind::Stub => {
+ parse_stubs(tcx, def_id, attrs);
+ }
+ KaniAttributeKind::Unwind => {
+ expect_single(tcx, kind, &attrs);
+ attrs.iter().for_each(|attr| {
+ parse_unwind(tcx, attr);
+ })
+ }
+ KaniAttributeKind::Proof => {
+ expect_single(tcx, kind, &attrs);
+ attrs.iter().for_each(|attr| check_proof_attribute(tcx, def_id, attr))
+ }
+ KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| {
+ let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(tcx));
+ }),
+ };
  }
 }
 
@@ -85,53 +113,39 @@ 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.
-pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessAttributes> {
+/// Note that all attributes should be valid by now.
+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 => {
- expect_single(tcx, kind, &attributes);
- harness.should_panic = true
- }
- KaniAttributeKind::Solver => {
- // Make sure the solver is not already set
- harness.solver = parse_solver(tcx, expect_single(tcx, kind, &attributes));
- }
- KaniAttributeKind::Stub => {
- harness.stubs = parse_stubs(tcx, def_id, attributes);
- }
- KaniAttributeKind::Unwind => {
- harness.unwind_value =
- parse_unwind(tcx, expect_single(tcx, kind, &attributes))
- }
- 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.
 ///
-/// 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.
+/// TODO: Improve error message by printing the span of the harness instead of the definition.
 pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
  if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) {
  // skip closures due to an issue with rustc.
@@ -141,21 +155,12 @@ pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id:
  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:?}"
- );
- }
+ let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();
+ if !enabled_features.contains(&unstable_attr.feature) {
+ // Reached an unstable attribute that was not enabled.
+ report_unstable_forbidden(tcx, def_id, &unstable_attr);
+ } else {
+ debug!(enabled=?attr, ?def_id, "check_unstable_features");
  }
  }
  }
@@ -197,13 +202,9 @@ fn expect_single<'a>(
 }
 
 /// Check that if an item is tagged with a proof_attribute, it is a valid harness.
-fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attributes: &Vec<&Attribute>) {
- assert!(!proof_attributes.is_empty());
- let span = proof_attributes.first().unwrap().span;
- if proof_attributes.len() > 1 {
- tcx.sess.span_warn(proof_attributes[0].span, "duplicate attribute");
- }
-
+fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attribute: &Attribute) {
+ let span = proof_attribute.span;
+ expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute);
  if tcx.def_kind(def_id) != DefKind::Fn {
  tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions");
  } else if tcx.generics_of(def_id).requires_monomorphization(tcx) {
@@ -296,6 +297,15 @@ impl<'a> TryFrom<&'a Attribute> for UnstableAttribute {
  }
 }
 
+fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) {
+ if !attr.is_word() {
+ tcx.sess
+ .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref()))
+ .help("remove the extra argument")
+ .emit();
+ }
+}
+
 /// 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
@@ -494,12 +504,15 @@ 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 solver `{ident_str}`"));
+ tcx.sess.span_err(attr.span, format!("unknown attribute `{ident_str}`"));
  err
  })
  .ok()

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]\
-| ^^^^^^^^^^^^^^
+| ^^^^^^^^^^^^^^\
+|\