From a605840609e865ad477baf6a3e2d13453a1e46e0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 15 Jun 2023 16:56:37 -0700 Subject: [PATCH] Fix tests + a few more changes --- .../compiler_interface.rs | 3 +- kani-compiler/src/kani_compiler.rs | 7 ++- kani-compiler/src/kani_middle/attributes.rs | 62 +++++++++---------- 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, 125 insertions(+), 54 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 9744cde97f6a..24726e0f9655 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/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 { +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 { 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 attribute `{ident_str}`")); 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]\ -| ^^^^^^^^^^^^^^ +| ^^^^^^^^^^^^^^\ +|\