diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9a9a9012bd5a..5f0c0c92e5d3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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: // diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index a8c7dbfda93e..cdb17b8cd0ac 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/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() diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4abc3495e6ec..24726e0f9655 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/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 { +/// 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 { // 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 { 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::(); + 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() diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 03e163699d2e..506779001689 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/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), } diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected index efdc64c9df65..49db2367b832 100644 --- a/tests/cargo-ui/unstable-attr/invalid/expected +++ b/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 = "")]\ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ + |\ + = note: expected format: #[kani::unstable(feature="", issue="", reason="")]\ + = 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="", issue="", reason="")] + +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="", issue="", reason="")]\ -= 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="", issue="", reason="")] -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="", issue="", reason="")] diff --git a/tests/ui/invalid-attribute/attrs.rs b/tests/ui/invalid-attribute/attrs.rs new file mode 100644 index 000000000000..77b176a25c46 --- /dev/null +++ b/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() {} diff --git a/tests/ui/invalid-attribute/expected b/tests/ui/invalid-attribute/expected new file mode 100644 index 000000000000..75be29c13e83 --- /dev/null +++ b/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)]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +| + diff --git a/tests/ui/invalid-harnesses/expected b/tests/ui/invalid-harnesses/expected index bc24569a9522..7def51a0d85a 100644 --- a/tests/ui/invalid-harnesses/expected +++ b/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]\ diff --git a/tests/ui/logging/warning/expected b/tests/ui/logging/warning/expected index 49552eae9143..d272819a13ff 100644 --- a/tests/ui/logging/warning/expected +++ b/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. + diff --git a/tests/ui/logging/warning/trivial.rs b/tests/ui/logging/warning/trivial.rs index ca3304bcf70e..d6ec3a6cb762 100644 --- a/tests/ui/logging/warning/trivial.rs +++ b/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 ()>(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); } diff --git a/tests/ui/multiple-proof-attributes/expected b/tests/ui/multiple-proof-attributes/expected index 5907806a163f..2b8b560f92fd 100644 --- a/tests/ui/multiple-proof-attributes/expected +++ b/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]\ -| ^^^^^^^^^^^^^^ +| ^^^^^^^^^^^^^^\ +|\