From 8d4e6f9a0eaae76aaa01f49a43686018cefb8bbb Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Mon, 7 Mar 2022 15:33:27 -0500 Subject: [PATCH] Unwind Attribute without Python Changes (#846) * Unwind Attribute without Python Changes --- library/kani_macros/src/lib.rs | 26 +++- .../codegen_cprover_gotoc/codegen/function.rs | 125 ++++++++++++++++-- .../codegen_cprover_gotoc/context/metadata.rs | 2 + .../simple-proof-annotation/Cargo.toml | 2 +- .../simple-unwind-annotation/Cargo.toml | 13 ++ .../simple-unwind-annotation/main.expected | 1 + .../simple-unwind-annotation/src/main.rs | 32 +++++ tests/kani/Unwind-Attribute/fixme_lib.rs | 21 +++ tests/ui/arguments-proof/expected | 6 + tests/ui/arguments-proof/main.rs | 20 +++ tests/ui/multiple-proof-attributes/expected | 9 ++ tests/ui/multiple-proof-attributes/main.rs | 21 +++ tests/ui/unsupported-annotation/expected | 7 + tests/ui/unsupported-annotation/main.rs | 21 +++ tests/ui/unwind-multiple-arguments/expected | 5 + tests/ui/unwind-multiple-arguments/main.rs | 21 +++ tests/ui/unwind-without-proof/expected | 6 + tests/ui/unwind-without-proof/main.rs | 20 +++ 18 files changed, 345 insertions(+), 13 deletions(-) create mode 100644 tests/cargo-kani/simple-unwind-annotation/Cargo.toml create mode 100644 tests/cargo-kani/simple-unwind-annotation/main.expected create mode 100644 tests/cargo-kani/simple-unwind-annotation/src/main.rs create mode 100644 tests/kani/Unwind-Attribute/fixme_lib.rs create mode 100644 tests/ui/arguments-proof/expected create mode 100644 tests/ui/arguments-proof/main.rs create mode 100644 tests/ui/multiple-proof-attributes/expected create mode 100644 tests/ui/multiple-proof-attributes/main.rs create mode 100644 tests/ui/unsupported-annotation/expected create mode 100644 tests/ui/unsupported-annotation/main.rs create mode 100644 tests/ui/unwind-multiple-arguments/expected create mode 100644 tests/ui/unwind-multiple-arguments/main.rs create mode 100644 tests/ui/unwind-without-proof/expected create mode 100644 tests/ui/unwind-without-proof/main.rs diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8b1c734073b9..1c011bbaf462 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -36,9 +36,10 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { #[cfg(kani)] #[proc_macro_attribute] -pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { +pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); + assert!(attr.to_string().len() == 0, "#[kani::proof] does not take any arguments"); result.extend("#[kanitool::proof]".parse::().unwrap()); // no_mangle is a temporary hack to make the function "public" so it gets codegen'd result.extend("#[no_mangle]".parse::().unwrap()); @@ -49,3 +50,26 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { // $item // ) } + +#[cfg(not(kani))] +#[proc_macro_attribute] +pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream { + // When the config is not kani, we should leave the function alone + item +} + +/// Set Loop unwind limit for proof harnesses +/// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'. +/// arg - Takes in a integer value (u32) that represents the unwind value for the harness. +#[cfg(kani)] +#[proc_macro_attribute] +pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { + let mut result = TokenStream::new(); + + // Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)] + let insert_string = "#[kanitool::unwind(".to_owned() + &attr.clone().to_string() + ")]"; + result.extend(insert_string.parse::().unwrap()); + + result.extend(item); + result +} diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 6eef2689a15a..afbf80f20e06 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -8,9 +8,12 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Stmt, Symbol}; use cbmc::InternString; use rustc_ast::ast; +use rustc_ast::{Attribute, LitKind}; +use rustc_middle::mir::coverage::Op; use rustc_middle::mir::{HasLocalDecls, Local}; use rustc_middle::ty::{self, Instance}; use std::collections::BTreeMap; +use std::convert::TryInto; use std::iter::FromIterator; use tracing::{debug, warn}; @@ -238,21 +241,50 @@ impl<'tcx> GotocCtx<'tcx> { /// This updates the goto context with any information that should be accumulated from a function's /// attributes. /// - /// Currently, this is only proof harness annotations. - /// i.e. `#[kani::proof]` (which kani_macros translates to `#[kanitool::proof]` for us to handle here) + /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) fn handle_kanitool_attributes(&mut self) { - let instance = self.current_fn().instance(); + let all_attributes = self.tcx.get_attrs(self.current_fn().instance().def_id()); + let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes); - for attr in self.tcx.get_attrs(instance.def_id()) { - match kanitool_attr_name(attr).as_deref() { - Some("proof") => self.handle_kanitool_proof(), - _ => {} + if proof_attributes.is_empty() && !other_attributes.is_empty() { + self.tcx.sess.span_err( + other_attributes[0].1.span, + format!( + "The {} attribute also requires the '#[kani::proof]' attribute", + other_attributes[0].0 + ) + .as_str(), + ); + return; + } + if proof_attributes.len() > 1 { + // No return because this only requires a warning + self.tcx.sess.span_warn(proof_attributes[0].span, "Only one '#[kani::proof]' allowed"); + } + if !proof_attributes.is_empty() { + self.create_proof_harness(other_attributes); + } + } + + /// Create the proof harness struct using the handler methods for various attributes + fn create_proof_harness(&mut self, other_attributes: Vec<(String, &Attribute)>) { + let mut harness = self.default_kanitool_proof(); + for attr in other_attributes.iter() { + match attr.0.as_str() { + "unwind" => self.handle_kanitool_unwind(attr.1, &mut harness), + _ => { + self.tcx.sess.span_err( + attr.1.span, + format!("Unsupported Annotation -> {}", attr.0.as_str()).as_str(), + ); + } } } + self.proof_harnesses.push(harness); } - /// Update `self` (the goto context) to add the current function as a listed proof harness - fn handle_kanitool_proof(&mut self) { + /// Create the default proof harness for the current function + fn default_kanitool_proof(&mut self) -> HarnessMetadata { let current_fn = self.current_fn(); let pretty_name = current_fn.readable_name().to_owned(); let mangled_name = current_fn.name(); @@ -263,9 +295,39 @@ impl<'tcx> GotocCtx<'tcx> { mangled_name, original_file: loc.filename().unwrap(), original_line: loc.line().unwrap().to_string(), + unwind_value: None, }; - self.proof_harnesses.push(harness); + harness + } + + /// Updates the proof harness with new unwind value + fn handle_kanitool_unwind(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) { + // If some unwind value already exists, then the current unwind being handled is a duplicate + if !harness.unwind_value.is_none() { + self.tcx.sess.span_err(attr.span, "Only one '#[kani::unwind]' allowed"); + return; + } + // Get Attribute value and if it's not none, assign it to the metadata + match extract_integer_argument(attr) { + None => { + // There are no integers or too many arguments given to the attribute + self.tcx + .sess + .span_err(attr.span, "Exactly one Unwind Argument as Integer accepted"); + return; + } + Some(unwind_integer_value) => { + let val: Result = unwind_integer_value.try_into(); + if val.is_err() { + self.tcx + .sess + .span_err(attr.span, "Value above maximum permitted value - u32::MAX"); + return; + } + harness.unwind_value = Some(val.unwrap()); + } + } } } @@ -273,10 +335,51 @@ impl<'tcx> GotocCtx<'tcx> { fn kanitool_attr_name(attr: &ast::Attribute) -> Option { match &attr.kind { ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _) - if segments.len() == 2 && segments[0].ident.as_str() == "kanitool" => + if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" => { Some(segments[1].ident.as_str().to_string()) } _ => None, } } + +/// Partition all the attributes into two buckets, proof_attributes and other_attributes +fn partition_kanitool_attributes( + all_attributes: &[Attribute], +) -> (Vec<&Attribute>, Vec<(String, &Attribute)>) { + let mut proof_attributes = vec![]; + let mut other_attributes = vec![]; + + for attr in all_attributes { + // Get the string the appears after "kanitool::" in each attribute string. + // Ex - "proof" | "unwind" etc. + if let Some(attribute_string) = kanitool_attr_name(attr).as_deref() { + if attribute_string == "proof" { + proof_attributes.push(attr); + } else { + other_attributes.push((attribute_string.to_string(), attr)); + } + } + } + + (proof_attributes, other_attributes) +} + +/// Extracts the integer value argument from the attribute provided +/// For example, `unwind(8)` return `Some(8)` +fn extract_integer_argument(attr: &Attribute) -> Option { + // Vector of meta items , that contain the arguments given the attribute + let attr_args = attr.meta_item_list()?; + // Only extracts one integer value as argument + if attr_args.len() == 1 { + let x = attr_args[0].literal()?; + match x.kind { + LitKind::Int(y, ..) => Some(y), + _ => None, + } + } + // Return none if there are no attributes or if there's too many attributes + else { + None + } +} diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs index bc2f902fff86..71d29793ef04 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs @@ -17,6 +17,8 @@ pub struct HarnessMetadata { pub original_file: String, /// The line in that file where the proof harness begins pub original_line: String, + /// Optional data to store unwind value + pub unwind_value: Option, } /// The structure of `.kani-metadata.json` files, which are emitted for each crate diff --git a/tests/cargo-kani/simple-proof-annotation/Cargo.toml b/tests/cargo-kani/simple-proof-annotation/Cargo.toml index 65db548b9745..eacfc782c17d 100644 --- a/tests/cargo-kani/simple-proof-annotation/Cargo.toml +++ b/tests/cargo-kani/simple-proof-annotation/Cargo.toml @@ -9,4 +9,4 @@ edition = "2021" [dependencies] [kani.flags] -output-format = "old" \ No newline at end of file +output-format = "old" diff --git a/tests/cargo-kani/simple-unwind-annotation/Cargo.toml b/tests/cargo-kani/simple-unwind-annotation/Cargo.toml new file mode 100644 index 000000000000..3d1eb70fa5bc --- /dev/null +++ b/tests/cargo-kani/simple-unwind-annotation/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "simple-unwind-annotation" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[kani.flags] +output-format = "old" +function = "harness" diff --git a/tests/cargo-kani/simple-unwind-annotation/main.expected b/tests/cargo-kani/simple-unwind-annotation/main.expected new file mode 100644 index 000000000000..538119c6993f --- /dev/null +++ b/tests/cargo-kani/simple-unwind-annotation/main.expected @@ -0,0 +1 @@ +[harness.assertion.2] line 21 assertion failed: counter < 10: FAILURE diff --git a/tests/cargo-kani/simple-unwind-annotation/src/main.rs b/tests/cargo-kani/simple-unwind-annotation/src/main.rs new file mode 100644 index 000000000000..3f8ec7ba55c9 --- /dev/null +++ b/tests/cargo-kani/simple-unwind-annotation/src/main.rs @@ -0,0 +1,32 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --function harness + +// The expected file presently looks for "1 == 2" above. +// But eventually this test may start to fail as we might stop regarding 'main' +// as a valid proof harness, since it isn't annotated as such. +// This test should be updated if we go that route. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof] +#[kani::unwind(9)] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} + +#[kani::proof] +fn harness_2() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/kani/Unwind-Attribute/fixme_lib.rs b/tests/kani/Unwind-Attribute/fixme_lib.rs new file mode 100644 index 000000000000..faaa50965ce8 --- /dev/null +++ b/tests/kani/Unwind-Attribute/fixme_lib.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks + +// Added to fix me because there are no tests for the annotations themselves. +// TODO : The unwind value needs to be parsed and the unwind needs to be applied to each harness, we do not test this behavior yet. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof] +#[kani::unwind(10)] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/ui/arguments-proof/expected b/tests/ui/arguments-proof/expected new file mode 100644 index 000000000000..6d1e3d011bd2 --- /dev/null +++ b/tests/ui/arguments-proof/expected @@ -0,0 +1,6 @@ + --> main.rs:13:1 + | +13 | #[kani::proof(some, argument2)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + = help: message: #[kani::proof] does not take any arguments diff --git a/tests/ui/arguments-proof/main.rs b/tests/ui/arguments-proof/main.rs new file mode 100644 index 000000000000..2ae4d241dd72 --- /dev/null +++ b/tests/ui/arguments-proof/main.rs @@ -0,0 +1,20 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks + +// This test is to check Kani's error handling for harnesses that have proof attributes +// with arguments when the expected declaration takes no arguments. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof(some, argument2)] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/ui/multiple-proof-attributes/expected b/tests/ui/multiple-proof-attributes/expected new file mode 100644 index 000000000000..1f18f4d6fd88 --- /dev/null +++ b/tests/ui/multiple-proof-attributes/expected @@ -0,0 +1,9 @@ +warning: Only one '#[kani::proof]' allowed + --> main.rs:14:1 + | +14 | #[kani::proof] + | ^^^^^^^^^^^^^^ + | + = note: this warning originates in the attribute macro `kani::proof` (in Nightly builds, run with -Z macro-backtrace for more info) + +warning: 1 warning emitted diff --git a/tests/ui/multiple-proof-attributes/main.rs b/tests/ui/multiple-proof-attributes/main.rs new file mode 100644 index 000000000000..dbbe9c4cf6cc --- /dev/null +++ b/tests/ui/multiple-proof-attributes/main.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks --verbose + +// This test is to check Kani's error handling for harnesses that have multiple proof annotations +// declared. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof] +#[kani::proof] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/ui/unsupported-annotation/expected b/tests/ui/unsupported-annotation/expected new file mode 100644 index 000000000000..6de8a1336de2 --- /dev/null +++ b/tests/ui/unsupported-annotation/expected @@ -0,0 +1,7 @@ +error[E0433]: failed to resolve: could not find `test_annotation` in `kani` + --> main.rs:14:9 + | +14 | #[kani::test_annotation] + | ^^^^^^^^^^^^^^^ could not find `test_annotation` in `kani` + +error: aborting due to previous error diff --git a/tests/ui/unsupported-annotation/main.rs b/tests/ui/unsupported-annotation/main.rs new file mode 100644 index 000000000000..77f3da3a3817 --- /dev/null +++ b/tests/ui/unsupported-annotation/main.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks --verbose + +// This test is to check Kani's error handling for harnesses that have multiple proof annotations +// declared. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof] +#[kani::test_annotation] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/ui/unwind-multiple-arguments/expected b/tests/ui/unwind-multiple-arguments/expected new file mode 100644 index 000000000000..964125cb8700 --- /dev/null +++ b/tests/ui/unwind-multiple-arguments/expected @@ -0,0 +1,5 @@ +error: Exactly one Unwind Argument as Integer accepted + --> main.rs:14:1 + | +14 | #[kani::unwind(10,5)] + | ^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/ui/unwind-multiple-arguments/main.rs b/tests/ui/unwind-multiple-arguments/main.rs new file mode 100644 index 000000000000..5f1434f4aa49 --- /dev/null +++ b/tests/ui/unwind-multiple-arguments/main.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks + +// This test is to check Kani's error handling for harnesses that have unwind attributes +// that have multiple arguments provided when only one is allowed. + +fn main() { + assert!(1 == 2); +} + +#[kani::proof] +#[kani::unwind(10,5)] +fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 10); + } +} diff --git a/tests/ui/unwind-without-proof/expected b/tests/ui/unwind-without-proof/expected new file mode 100644 index 000000000000..5b1f8bba569c --- /dev/null +++ b/tests/ui/unwind-without-proof/expected @@ -0,0 +1,6 @@ +error: The unwind attribute also requires the '#[kani::proof]' attribute + --> main.rs:13:1 + | +13 | #[kani::unwind(7)] + | ^^^^^^^^^^^^^^^^^^ + | diff --git a/tests/ui/unwind-without-proof/main.rs b/tests/ui/unwind-without-proof/main.rs new file mode 100644 index 000000000000..a4f0d290b0ca --- /dev/null +++ b/tests/ui/unwind-without-proof/main.rs @@ -0,0 +1,20 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --no-unwinding-checks --function harness + +// This test is to check Kani's error handling for harnesses that have unwind attributes +// without '#[kani::proof]' attribute declared + +fn main() { + assert!(1 == 2); +} + +#[kani::unwind(7)] +pub fn harness() { + let mut counter = 0; + loop { + counter += 1; + assert!(counter < 8); + } +}