From 49405b2a124b87191bd2334a78218311543bdb58 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 19 Jun 2023 12:22:25 -0700 Subject: [PATCH] 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. --- .../compiler_interface.rs | 3 +- kani-compiler/src/kani_compiler.rs | 7 +- kani-compiler/src/kani_middle/attributes.rs | 157 ++++++++++-------- kani-compiler/src/kani_middle/metadata.rs | 2 +- tests/cargo-ui/unstable-attr/invalid/expected | 36 +++- tests/ui/invalid-attribute/attrs.rs | 15 ++ tests/ui/invalid-attribute/expected | 27 +++ tests/ui/invalid-harnesses/expected | 2 +- tests/ui/logging/warning/expected | 5 +- tests/ui/logging/warning/trivial.rs | 13 +- tests/ui/multiple-proof-attributes/expected | 7 +- 11 files changed, 181 insertions(+), 93 deletions(-) create mode 100644 tests/ui/invalid-attribute/attrs.rs create mode 100644 tests/ui/invalid-attribute/expected 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]\ -| ^^^^^^^^^^^^^^ +| ^^^^^^^^^^^^^^\ +|\