From 2e33085d6c738a7ea8b87670a3e78fb3c05d6106 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 21 Apr 2022 18:34:00 -0400 Subject: [PATCH] Feature : Unwind attribute (#1031) * Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind --- docs/src/kani-single-file.md | 2 +- docs/src/regression-testing.md | 2 +- docs/src/tutorial-loop-unwinding.md | 14 +-- docs/src/tutorial-real-code.md | 2 +- docs/src/tutorial/loops-unwinding/Cargo.toml | 7 +- docs/src/tutorial/loops-unwinding/src/lib.rs | 1 + docs/src/workarounds.md | 4 +- kani-driver/src/args.rs | 18 +++- kani-driver/src/args_toml.rs | 8 +- kani-driver/src/call_cbmc.rs | 89 +++++++++++++++++-- kani-driver/src/call_cbmc_viewer.rs | 34 +++++-- kani-driver/src/main.rs | 4 +- kani-driver/src/metadata.rs | 12 +-- .../{harness.expected => harness_1.expected} | 2 +- .../simple-unwind-annotation/src/lib.rs | 2 +- .../expected | 2 +- .../dry-run-flag-conflict-auto-unwind/main.rs | 3 +- tests/expected/dynamic-error-trait/main.rs | 3 +- tests/expected/never-return/check_never.rs | 2 +- tests/expected/raw_slice/slice.rs | 2 +- tests/expected/raw_slice_c_repr/slice.rs | 2 +- tests/expected/raw_slice_packed/slice.rs | 1 - .../report/insufficient_unwind/test.rs | 3 +- tests/expected/unwind_tip/main.rs | 3 +- .../virtio-balloon-compact/ignore-main.rs | 2 +- tests/kani/Closure/fn_mut_closure.rs | 3 +- tests/kani/CopyIntrinsics/main_fixme.rs | 2 +- tests/kani/DynTrait/drop_nested_boxed_dyn.rs | 3 +- .../DynTrait/drop_nested_boxed_dyn_fail.rs | 3 +- tests/kani/DynTrait/nested_boxes.rs | 3 +- tests/kani/DynTrait/nested_boxes_fail.rs | 3 +- tests/kani/FunctionCall_Ret-Param/main.rs | 2 +- .../SizeOfVal/fixme_size_of_fat_ptr.rs | 2 +- tests/kani/Invariants/array.rs | 2 +- tests/kani/Invariants/array_raw_fail.rs | 2 +- tests/kani/Iterator/into_iter.rs | 2 +- tests/kani/Iterator/try_fold.rs | 2 +- tests/kani/LoopLoop_NonReturning/main.rs | 3 +- .../main_no_unwind_asserts.rs | 2 +- tests/kani/LoopWhile_NonReturning/main.rs | 3 +- .../main_no_unwind_asserts.rs | 2 +- tests/kani/NondetSlices/test3.rs | 2 +- tests/kani/NondetSlices/test4.rs | 2 +- tests/kani/NondetSlices/test5.rs | 2 +- tests/kani/PhantomData/phantom_fixme.rs | 2 +- .../Projection/fixme_dyn_dyn_projection.rs | 2 +- .../Projection/fixme_dyn_slice_projection.rs | 2 +- tests/kani/Projection/slice_dyn_projection.rs | 2 +- .../kani/Projection/slice_slice_projection.rs | 2 +- tests/kani/Slice/main.rs | 3 +- tests/kani/Slice/size_of.rs | 2 +- tests/kani/SwitchInt/main.rs | 3 +- tests/kani/Vectors/fixme_main.rs | 2 +- tests/kani/Vectors/vector_extend_in_new.rs | 3 +- tests/kani/Vectors/vector_extend_loop.rs | 3 +- tests/kani/Whitespace/main.rs | 3 +- tests/prusti/Binary_search.rs | 2 +- tests/smack/loops/gauss_sum_nondet.rs | 2 +- tests/smack/loops/gauss_sum_nondet_fail.rs | 3 +- tests/smack/loops/iterator.rs | 3 +- tests/smack/loops/iterator_fail.rs | 3 +- tests/ui/check_operations/operations.rs | 2 +- 62 files changed, 210 insertions(+), 103 deletions(-) rename tests/cargo-kani/simple-unwind-annotation/{harness.expected => harness_1.expected} (68%) diff --git a/docs/src/kani-single-file.md b/docs/src/kani-single-file.md index 1676986e9988..8683e22a8f15 100644 --- a/docs/src/kani-single-file.md +++ b/docs/src/kani-single-file.md @@ -24,7 +24,7 @@ The most common `kani` arguments are the following: * `--harness `: By default, Kani checks all proof harnesses it finds. You can switch to checking a single harness using this flag. - * `--unwind `: Set a global upper [loop + * `--default-unwind `: Set a global upper [loop unwinding](./tutorial-loop-unwinding.md) bound on all loops. This can force termination when CBMC tries to unwind loops indefinitely. diff --git a/docs/src/regression-testing.md b/docs/src/regression-testing.md index 07c99358668e..633368777357 100644 --- a/docs/src/regression-testing.md +++ b/docs/src/regression-testing.md @@ -107,7 +107,7 @@ be specified in single Rust files by adding a comment at the top of the file: For example, to use an unwinding value of 4 in a test, we can write: ```rust,noplaypen -// kani-flags: --unwind 4 +// kani-flags: --default-unwind 4 ``` For `cargo-kani` tests, the preferred way to pass command-line options is adding diff --git a/docs/src/tutorial-loop-unwinding.md b/docs/src/tutorial-loop-unwinding.md index bd8920476b38..a16005fbc617 100644 --- a/docs/src/tutorial-loop-unwinding.md +++ b/docs/src/tutorial-loop-unwinding.md @@ -30,13 +30,13 @@ Bounding proofs like this means we may no longer be proving as much as we origin Who's to say, if we prove everything works up to size 10, that there isn't a novel bug lurking, expressible only with problems of size 11+? But, let's get back to the issue at hand. -We can "make progress" in our work by giving Kani a global bound on the problem size using the `--unwind ` flag. +We can "make progress" in our work by giving Kani a global bound on the problem size using the `--default-unwind ` flag. This flag puts a fixed upper bound on loop unwinding. Kani will automatically generate verification conditions that help us understand if that bound isn't enough. Let's start with a small unwinding value: ``` -# kani src/lib.rs --unwind 1 +# kani src/lib.rs --default-unwind 1 Check 69: .unwind.0 - Status: FAILURE - Description: "unwinding assertion loop 0" @@ -50,19 +50,19 @@ This output is showing us two things: 2. We aren't seeing other failures if we only unwind the loop once. The execution can't progress far enough to reveal the bug we're interested in (which actually only happens in the last iteration of the loop). -Doing an initial `--unwind 1` is generally enough to force termination, but often too little for verification. +Doing an initial `--default-unwind 1` is generally enough to force termination, but often too little for verification. We were clearly aiming at a size limit of 10 in our proof harness, so let's try a few things: ``` -# kani src/lib.rs --unwind 10 | grep Failed +# kani src/lib.rs --default-unwind 10 | grep Failed Failed Checks: unwinding assertion loop 0 ``` A bound of 10 still isn't enough because we generally need to unwind one greater than the number of executed loop iterations: ``` -# kani src/lib.rs --unwind 11 | grep Failed +# kani src/lib.rs --default-unwind 11 | grep Failed Failed Checks: index out of bounds: the length is less than or equal to the given index Failed Checks: dereference failure: pointer outside object bounds Failed Checks: unwinding assertion loop 0 @@ -72,7 +72,7 @@ We're still not seeing the unwinding assertion failure go away! This is because our error is really an off-by-one problem, we loop one too many times, so let's add one more: ``` -# kani src/lib.rs --unwind 12 | grep Failed +# kani src/lib.rs --default-unwind 12 | grep Failed Failed Checks: index out of bounds: the length is less than or equal to the given index Failed Checks: dereference failure: pointer outside object bounds ``` @@ -80,4 +80,4 @@ Failed Checks: dereference failure: pointer outside object bounds Kani is now sure we've unwound the loop enough to verify our proof harness, and now we're seeing just the bound checking failures from the off-by-one error. 1. Exercise: Fix the off-by-one bounds error and get Kani to verify successfully. -2. Exercise: After fixing the error, `--unwind 11` works. Why? +2. Exercise: After fixing the error, `--default-unwind 11` works. Why? diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md index db8c77f1a4a1..9ccfb52d396e 100644 --- a/docs/src/tutorial-real-code.md +++ b/docs/src/tutorial-real-code.md @@ -77,7 +77,7 @@ Running Kani on this simple starting point will help figure out: 2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because now you've over-constrained the inputs. 3. Whether Kani will support all the Rust features involved. 4. Whether you've started with a tractable problem. -(If the problem is initially intractable, try `--unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.) +(If the problem is initially intractable, try `--default-unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.) Once you've got something working, the next step is to prove more interesting properties than what Kani covers by default. You accomplish this by adding new assertions (not just in your harness, but also to the code being run). diff --git a/docs/src/tutorial/loops-unwinding/Cargo.toml b/docs/src/tutorial/loops-unwinding/Cargo.toml index 23dc909857f6..76ed895a2f2d 100644 --- a/docs/src/tutorial/loops-unwinding/Cargo.toml +++ b/docs/src/tutorial/loops-unwinding/Cargo.toml @@ -5,9 +5,4 @@ name = "loops-unwinding" version = "0.1.0" edition = "2018" -[dependencies] - -[workspace] - -[package.metadata.kani] -flags = { unwind = "11" } +[workspace] \ No newline at end of file diff --git a/docs/src/tutorial/loops-unwinding/src/lib.rs b/docs/src/tutorial/loops-unwinding/src/lib.rs index 637544f6b05b..be27df525155 100644 --- a/docs/src/tutorial/loops-unwinding/src/lib.rs +++ b/docs/src/tutorial/loops-unwinding/src/lib.rs @@ -17,6 +17,7 @@ fn initialize_prefix(length: usize, buffer: &mut [u8]) { // ANCHOR: kani #[cfg(kani)] #[kani::proof] +#[kani::unwind(11)] fn main() { const LIMIT: usize = 10; let mut buffer: [u8; LIMIT] = [1; LIMIT]; diff --git a/docs/src/workarounds.md b/docs/src/workarounds.md index 546af0df30ca..1a3aa6018100 100644 --- a/docs/src/workarounds.md +++ b/docs/src/workarounds.md @@ -6,7 +6,7 @@ issues in the Kani project. ## CBMC arguments Kani is able to handle common CBMC arguments as if they were its own (e.g., -`--unwind `), but sometimes it may be necessary to use CBMC arguments which +`--default-unwind `), but sometimes it may be necessary to use CBMC arguments which are not handled by Kani. To pass additional arguments for CBMC, you pass `--cbmc-args` to Kani. Note that @@ -26,7 +26,7 @@ cargo kani []* --cbmc-args []* ### Individual loop bounds -Setting `--unwind ` affects every loop in a harness. +Setting `--default-unwind ` affects every loop in a harness. Once you know a particular loop is causing trouble, sometimes it can be helpful to provide a specific bound for it. In the general case, specifying just the highest bound globally for all loops diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 77402945591e..681ba6e3ef95 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -104,6 +104,9 @@ pub struct KaniArgs { pub object_bits: u32, /// Specify the value used for loop unwinding in CBMC #[structopt(long)] + pub default_unwind: Option, + /// Specify the value used for loop unwinding for the specified harness in CBMC + #[structopt(long, requires("harness"))] pub unwind: Option, /// Turn on automatic loop unwinding #[structopt(long)] @@ -283,15 +286,15 @@ impl KaniArgs { let extra_unwind = self.cbmc_args.contains(&OsString::from("--unwind")); let extra_auto_unwind = self.cbmc_args.contains(&OsString::from("--auto-unwind")); let extras = extra_auto_unwind || extra_unwind; - let natives = self.auto_unwind || self.unwind.is_some(); + let natives = self.auto_unwind || self.default_unwind.is_some(); let any_auto_unwind = extra_auto_unwind || self.auto_unwind; - let any_unwind = self.unwind.is_some() || extra_unwind; + let any_unwind = self.default_unwind.is_some() || extra_unwind; // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. // We should consider improving the error messages slightly in a later pull request. if any_auto_unwind && any_unwind { Error::with_description( - "Conflicting flags: `--auto-unwind` is not compatible with other `--unwind` flags.", + "Conflicting flags: `--auto-unwind` is not compatible with other `--default-unwind` flags.", ErrorKind::ArgumentConflict, ) .exit(); @@ -365,6 +368,15 @@ mod tests { assert_eq!(err.kind, ErrorKind::ArgumentConflict); } + #[test] + fn check_unwind_conflicts() { + // --unwind cannot be called without --harness + let args = vec!["kani", "file.rs", "--unwind", "3"]; + let app = StandaloneArgs::clap(); + let err = app.get_matches_from_safe(args).unwrap_err(); + assert_eq!(err.kind, ErrorKind::MissingRequiredArgument); + } + fn parse_unstable_disabled(args: &str) -> Result, Error> { let args = format!("kani file.rs {}", args); let app = StandaloneArgs::clap(); diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index 69c02816e7f6..0201d23de361 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -152,18 +152,18 @@ mod tests { #[test] fn check_toml_parsing() { let a = "[workspace.metadata.kani] - flags = { default-checks = false, unwind = \"2\", cbmc-args = [\"--fake\"] }"; + flags = { default-checks = false, default-unwind = \"2\", cbmc-args = [\"--fake\"] }"; let b = toml_to_args(a).unwrap(); // default first, then unwind thanks to btree ordering. // cbmc-args always last. - assert_eq!(b.0, vec!["--no-default-checks", "--unwind", "2"]); + assert_eq!(b.0, vec!["--no-default-checks", "--default-unwind", "2"]); assert_eq!(b.1, vec!["--cbmc-args", "--fake"]); } #[test] fn check_merge_args_with_only_command_line_args() { let cmd_args: Vec = - ["cargo_kani", "--no-default-checks", "--unwind", "2", "--cbmc-args", "--fake"] + ["cargo_kani", "--no-default-checks", "--default-unwind", "2", "--cbmc-args", "--fake"] .iter() .map(|&s| s.into()) .collect(); @@ -174,7 +174,7 @@ mod tests { #[test] fn check_merge_args_with_only_config_kani_args() { let cfg_args: Vec = - ["--no-default-checks", "--unwind", "2"].iter().map(|&s| s.into()).collect(); + ["--no-default-checks", "--default-unwind", "2"].iter().map(|&s| s.into()).collect(); let merged = merge_args(vec!["kani".into()], cfg_args.clone(), Vec::new()).unwrap(); assert_eq!(merged[0], OsString::from("kani")); assert_eq!(merged[1..], cfg_args); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 78bf86e88be6..f54776975cad 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -2,10 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::{bail, Result}; +use kani_metadata::HarnessMetadata; use std::ffi::OsString; use std::path::Path; use std::process::Command; +use crate::args::KaniArgs; use crate::session::KaniSession; #[derive(PartialEq)] @@ -16,7 +18,7 @@ pub enum VerificationStatus { impl KaniSession { /// Verify a goto binary that's been prepared with goto-instrument - pub fn run_cbmc(&self, file: &Path) -> Result { + pub fn run_cbmc(&self, file: &Path, harness: &HarnessMetadata) -> Result { let output_filename = crate::util::append_path(file, "cbmc_output"); { @@ -24,7 +26,7 @@ impl KaniSession { temps.push(output_filename.clone()); } - let args: Vec = self.cbmc_flags(file)?; + let args: Vec = self.cbmc_flags(file, harness)?; // TODO get cbmc path from self let mut cmd = Command::new("cbmc"); @@ -73,15 +75,19 @@ impl KaniSession { } /// "Internal," but also used by call_cbmc_viewer - pub fn cbmc_flags(&self, file: &Path) -> Result> { + pub fn cbmc_flags( + &self, + file: &Path, + harness_metadata: &HarnessMetadata, + ) -> Result> { let mut args = self.cbmc_check_flags(); args.push("--object-bits".into()); args.push(self.args.object_bits.to_string().into()); - if let Some(unwind) = self.args.unwind { + if let Some(unwind_value) = resolve_unwind_value(&self.args, harness_metadata) { args.push("--unwind".into()); - args.push(unwind.to_string().into()); + args.push(unwind_value.to_string().into()); } else if self.args.auto_unwind { args.push("--auto-unwind".into()); } @@ -127,3 +133,76 @@ impl KaniSession { args } } + +/// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind) +pub fn resolve_unwind_value(args: &KaniArgs, harness_metadata: &HarnessMetadata) -> Option { + // Check for which flag is being passed and prioritize extracting unwind from the + // respective flag/annotation. + if let Some(harness_unwind) = args.unwind { + Some(harness_unwind) + } else if let Some(annotation_unwind) = harness_metadata.unwind_value { + Some(annotation_unwind) + } else if let Some(default_unwind) = args.default_unwind { + Some(default_unwind) + } else { + None + } +} + +#[cfg(test)] +mod tests { + use crate::args; + use crate::metadata::mock_proof_harness; + use structopt::StructOpt; + + use super::*; + + #[test] + fn check_resolve_unwind_value() { + // Command line unwind value for specific harnesses take precedence over default annotation value + let args_empty = ["kani"]; + let args_only_default = ["kani", "--default-unwind", "2"]; + let args_only_harness = ["kani", "--unwind", "1", "--harness", "check_one"]; + let args_both = + ["kani", "--default-unwind", "2", "--unwind", "1", "--harness", "check_one"]; + + let harness_none = mock_proof_harness("check_one", None); + let harness_some = mock_proof_harness("check_one", Some(3)); + + // test against no unwind annotation + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_empty), &harness_none), + None + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_only_default), &harness_none), + Some(2) + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_only_harness), &harness_none), + Some(1) + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_both), &harness_none), + Some(1) + ); + + // test against unwind annotation + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_empty), &harness_some), + Some(3) + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_only_default), &harness_some), + Some(3) + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_only_harness), &harness_some), + Some(1) + ); + assert_eq!( + resolve_unwind_value(&args::KaniArgs::from_iter(args_both), &harness_some), + Some(1) + ); + } +} diff --git a/kani-driver/src/call_cbmc_viewer.rs b/kani-driver/src/call_cbmc_viewer.rs index 461fc34734c9..e7a7d33aa718 100644 --- a/kani-driver/src/call_cbmc_viewer.rs +++ b/kani-driver/src/call_cbmc_viewer.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; +use kani_metadata::HarnessMetadata; use std::ffi::OsString; use std::path::Path; use std::process::Command; @@ -12,7 +13,12 @@ use crate::util::alter_extension; impl KaniSession { /// Run CBMC appropriately to produce 3 output XML files, then run cbmc-viewer on them to produce a report. /// Viewer doesn't give different error codes depending on verification failure, so as long as it works, we report success. - pub fn run_visualize(&self, file: &Path, report_dir: &Path) -> Result<()> { + pub fn run_visualize( + &self, + file: &Path, + report_dir: &Path, + harness_metadata: &HarnessMetadata, + ) -> Result<()> { let results_filename = alter_extension(file, "results.xml"); let coverage_filename = alter_extension(file, "coverage.xml"); let property_filename = alter_extension(file, "property.xml"); @@ -24,9 +30,19 @@ impl KaniSession { temps.push(property_filename.clone()); } - self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename)?; - self.cbmc_variant(file, &["--xml-ui", "--cover", "location"], &coverage_filename)?; - self.cbmc_variant(file, &["--xml-ui", "--show-properties"], &property_filename)?; + self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?; + self.cbmc_variant( + file, + &["--xml-ui", "--cover", "location"], + &coverage_filename, + harness_metadata, + )?; + self.cbmc_variant( + file, + &["--xml-ui", "--show-properties"], + &property_filename, + harness_metadata, + )?; let args: Vec = vec![ "--result".into(), @@ -59,8 +75,14 @@ impl KaniSession { Ok(()) } - fn cbmc_variant(&self, file: &Path, extra_args: &[&str], output: &Path) -> Result<()> { - let mut args = self.cbmc_flags(file)?; + fn cbmc_variant( + &self, + file: &Path, + extra_args: &[&str], + output: &Path, + harness: &HarnessMetadata, + ) -> Result<()> { + let mut args = self.cbmc_flags(file, harness)?; args.extend(extra_args.iter().map(|x| x.into())); // TODO fix this hack, abstractions are wrong diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index bd3bbb678c96..e9d1af63745b 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -132,11 +132,11 @@ impl KaniSession { } if self.args.visualize { - self.run_visualize(binary, report_dir)?; + self.run_visualize(binary, report_dir, harness)?; // Strictly speaking, we're faking success here. This is more "no error" Ok(VerificationStatus::Success) } else { - self.run_cbmc(binary) + self.run_cbmc(binary, harness) } } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 8321d3e30b1c..241a5aa330c0 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -123,7 +123,7 @@ impl KaniSession { pub fn determine_targets(&self, metadata: &KaniMetadata) -> Result> { if let Some(name) = &self.args.function { // --function is untranslated, create a mock harness - return Ok(vec![mock_proof_harness(name)]); + return Ok(vec![mock_proof_harness(name, None)]); } if let Some(name) = &self.args.harness { // Linear search, since this is only ever called once @@ -140,13 +140,13 @@ impl KaniSession { } } -fn mock_proof_harness(name: &str) -> HarnessMetadata { +pub fn mock_proof_harness(name: &str, unwind_value: Option) -> HarnessMetadata { HarnessMetadata { pretty_name: name.into(), mangled_name: name.into(), original_file: "".into(), original_line: "".into(), - unwind_value: None, + unwind_value: unwind_value, } } @@ -196,9 +196,9 @@ mod tests { #[test] fn check_find_proof_harness() { let harnesses = vec![ - mock_proof_harness("check_one"), - mock_proof_harness("module::check_two"), - mock_proof_harness("module::not_check_three"), + mock_proof_harness("check_one", None), + mock_proof_harness("module::check_two", None), + mock_proof_harness("module::not_check_three", None), ]; assert!(find_proof_harness("check_three", &harnesses).is_err()); assert!( diff --git a/tests/cargo-kani/simple-unwind-annotation/harness.expected b/tests/cargo-kani/simple-unwind-annotation/harness_1.expected similarity index 68% rename from tests/cargo-kani/simple-unwind-annotation/harness.expected rename to tests/cargo-kani/simple-unwind-annotation/harness_1.expected index 9dc068369282..b4fede93c306 100644 --- a/tests/cargo-kani/simple-unwind-annotation/harness.expected +++ b/tests/cargo-kani/simple-unwind-annotation/harness_1.expected @@ -1,2 +1,2 @@ -FAILURE\ +UNDETERMINED\ assertion failed: counter < 10 diff --git a/tests/cargo-kani/simple-unwind-annotation/src/lib.rs b/tests/cargo-kani/simple-unwind-annotation/src/lib.rs index 2705b506b358..c97065ce947b 100644 --- a/tests/cargo-kani/simple-unwind-annotation/src/lib.rs +++ b/tests/cargo-kani/simple-unwind-annotation/src/lib.rs @@ -4,7 +4,7 @@ // TODO: When unwind is hooked up, `harness.expected` should now see success #[kani::proof] #[kani::unwind(9)] -fn harness() { +fn harness_1() { let mut counter = 0; loop { counter += 1; diff --git a/tests/expected/dry-run-flag-conflict-auto-unwind/expected b/tests/expected/dry-run-flag-conflict-auto-unwind/expected index c9a58cb411de..ff9e37aacd50 100644 --- a/tests/expected/dry-run-flag-conflict-auto-unwind/expected +++ b/tests/expected/dry-run-flag-conflict-auto-unwind/expected @@ -1 +1 @@ -Conflicting flags: `--auto-unwind` is not compatible with other `--unwind` flags. \ No newline at end of file +Conflicting flags: `--auto-unwind` is not compatible with other `--default-unwind` flags. \ No newline at end of file diff --git a/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs b/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs index efc5f2a3da8e..fbc132f886cb 100644 --- a/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs +++ b/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs @@ -1,8 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --dry-run --auto-unwind --enable-unstable --function main -// cbmc-flags: --unwind 2 +// kani-flags: --dry-run --auto-unwind --default-unwind 2 --enable-unstable --function main // `--dry-run` causes Kani to print out commands instead of running them // In `expected` you will find substrings of these commands because the diff --git a/tests/expected/dynamic-error-trait/main.rs b/tests/expected/dynamic-error-trait/main.rs index 945e1e718cdb..d71a06685b49 100644 --- a/tests/expected/dynamic-error-trait/main.rs +++ b/tests/expected/dynamic-error-trait/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwinding-assertions use std::io::{self, Read, Write}; @@ -24,6 +24,7 @@ impl MemoryMapping { } #[kani::proof] +#[kani::unwind(2)] fn main() { let mm = MemoryMapping::new(2); if mm.is_ok() { diff --git a/tests/expected/never-return/check_never.rs b/tests/expected/never-return/check_never.rs index 2de156424fc6..3b5496da7235 100644 --- a/tests/expected/never-return/check_never.rs +++ b/tests/expected/never-return/check_never.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --unwind 11 +// kani-flags: --default-unwind 11 //! Check that we can verify code inside functions that never return. //! See https://github.com/model-checking/kani/issues/648 for more detail. diff --git a/tests/expected/raw_slice/slice.rs b/tests/expected/raw_slice/slice.rs index 3a8b987f9744..fee42f728415 100644 --- a/tests/expected/raw_slice/slice.rs +++ b/tests/expected/raw_slice/slice.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 //! This test case has a bunch of checks related to structures using raw slices ([T]). use std::mem; diff --git a/tests/expected/raw_slice_c_repr/slice.rs b/tests/expected/raw_slice_c_repr/slice.rs index 6bb4aef7d017..aa2ec8f1d4a5 100644 --- a/tests/expected/raw_slice_c_repr/slice.rs +++ b/tests/expected/raw_slice_c_repr/slice.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 // This test is basically the same as ../raw_slice/slice.rs but using repr(C) instead. //! This test case has a bunch of checks related to structures using raw slices ([T]). diff --git a/tests/expected/raw_slice_packed/slice.rs b/tests/expected/raw_slice_packed/slice.rs index c4e894e055eb..8dbf1c21590e 100644 --- a/tests/expected/raw_slice_packed/slice.rs +++ b/tests/expected/raw_slice_packed/slice.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 // This test is basically the same as ../raw_slice/slice.rs but using repr(C) instead. //! This test case has a bunch of checks related to structures using raw slices ([T]). diff --git a/tests/expected/report/insufficient_unwind/test.rs b/tests/expected/report/insufficient_unwind/test.rs index 9bea5c4dcaea..0f31624ad779 100644 --- a/tests/expected/report/insufficient_unwind/test.rs +++ b/tests/expected/report/insufficient_unwind/test.rs @@ -4,9 +4,8 @@ // This test checks that Kani reports UNDETERMINED if the specified unwinding is // insufficient. The minimum required unwinding is 7. -// kani-flags: --unwind 6 - #[kani::proof] +#[kani::unwind(6)] fn main() { let x: bool = kani::any(); let v = if x { vec![1, 2, 3] } else { vec![1, 1, 1, 1, 1, 1] }; diff --git a/tests/expected/unwind_tip/main.rs b/tests/expected/unwind_tip/main.rs index 83150c0f5591..e3c0feccf19b 100644 --- a/tests/expected/unwind_tip/main.rs +++ b/tests/expected/unwind_tip/main.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 9 - // This example is a copy of the `cbmc` test in // `src/test/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs` // @@ -11,6 +9,7 @@ // In this test, we check that Kani warns the user about unwinding failures // and makes a recommendation to fix the issue. #[kani::proof] +#[kani::unwind(9)] fn main() { let mut a: u32 = kani::any(); diff --git a/tests/firecracker/virtio-balloon-compact/ignore-main.rs b/tests/firecracker/virtio-balloon-compact/ignore-main.rs index a9cd8d6254b9..13dc5bcdb4b0 100644 --- a/tests/firecracker/virtio-balloon-compact/ignore-main.rs +++ b/tests/firecracker/virtio-balloon-compact/ignore-main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// Try with: kani ignore-main.rs -- --unwind 3 --unwinding-assertions --pointer-check --object-bits 11 +// Try with: kani ignore-main.rs -- --default-unwind 3 --unwinding-assertions --pointer-check --object-bits 11 // With kissat as the solver (--external-sat-solver /path/to/kissat) this takes ~5mins pub const MAX_PAGE_COMPACT_BUFFER: usize = 2048; diff --git a/tests/kani/Closure/fn_mut_closure.rs b/tests/kani/Closure/fn_mut_closure.rs index e0eabd823d64..9b9df014d153 100644 --- a/tests/kani/Closure/fn_mut_closure.rs +++ b/tests/kani/Closure/fn_mut_closure.rs @@ -4,8 +4,6 @@ // Check that we can pass a FnMut closure to a stand alone // function definition. -// kani-flags: --unwind 6 - fn each(x: &[T], mut f: F) where F: FnMut(&T), @@ -16,6 +14,7 @@ where } #[kani::proof] +#[kani::unwind(6)] fn main() { let mut sum = 0_usize; let elems = [1_usize, 2, 3, 4, 5]; diff --git a/tests/kani/CopyIntrinsics/main_fixme.rs b/tests/kani/CopyIntrinsics/main_fixme.rs index 2118109b66bf..dff586d23723 100644 --- a/tests/kani/CopyIntrinsics/main_fixme.rs +++ b/tests/kani/CopyIntrinsics/main_fixme.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(core_intrinsics)] -/// kani main.rs -- --unwind 20 --unwinding-assertions +/// kani main.rs -- --default-unwind 20 --unwinding-assertions use std::mem; use std::ptr; diff --git a/tests/kani/DynTrait/drop_nested_boxed_dyn.rs b/tests/kani/DynTrait/drop_nested_boxed_dyn.rs index 4bea45747d09..32aa050a5c1f 100644 --- a/tests/kani/DynTrait/drop_nested_boxed_dyn.rs +++ b/tests/kani/DynTrait/drop_nested_boxed_dyn.rs @@ -5,7 +5,7 @@ // There is an implicit self-recursive call to drop_in_place, so we // need to set an unwind bound. -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwinding-assertions static mut CELL: i32 = 0; @@ -20,6 +20,7 @@ impl Drop for Concrete { } #[kani::proof] +#[kani::unwind(2)] fn main() { // Check normal box { diff --git a/tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs b/tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs index 5a427aea4a65..d773ea801535 100644 --- a/tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs +++ b/tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-verify-fail -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwinding-assertions static mut CELL: i32 = 0; @@ -17,6 +17,7 @@ impl Drop for Concrete { } #[kani::proof] +#[kani::unwind(2)] fn main() { // Check normal box { diff --git a/tests/kani/DynTrait/nested_boxes.rs b/tests/kani/DynTrait/nested_boxes.rs index 538dbe8ce7b0..c48f77cc16ab 100644 --- a/tests/kani/DynTrait/nested_boxes.rs +++ b/tests/kani/DynTrait/nested_boxes.rs @@ -4,7 +4,7 @@ // This test checks the size and align fields for 3-deep nested trait pointers. The // outter 2 dynamic trait objects have fat pointers as their backing data. -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwinding-assertions #![feature(core_intrinsics)] #![feature(ptr_metadata)] @@ -21,6 +21,7 @@ struct Foo { } #[kani::proof] +#[kani::unwind(2)] fn main() { let dyn_trait1: Box = Box::new(Foo { _a: 1, _b: 2 }); let dyn_trait2: Box = Box::new(dyn_trait1); diff --git a/tests/kani/DynTrait/nested_boxes_fail.rs b/tests/kani/DynTrait/nested_boxes_fail.rs index 484baa9a6148..81297dc8291c 100644 --- a/tests/kani/DynTrait/nested_boxes_fail.rs +++ b/tests/kani/DynTrait/nested_boxes_fail.rs @@ -6,7 +6,7 @@ // outter 2 dynamic trait objects have fat pointers as their backing data. // In this failing tests, assertions are inverted to use !=. -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwinding-assertions #![feature(core_intrinsics)] #![feature(ptr_metadata)] @@ -23,6 +23,7 @@ struct Foo { } #[kani::proof] +#[kani::unwind(2)] fn main() { let dyn_trait1: Box = Box::new(Foo { _a: 1, _b: 2 }); let dyn_trait2: Box = Box::new(dyn_trait1); diff --git a/tests/kani/FunctionCall_Ret-Param/main.rs b/tests/kani/FunctionCall_Ret-Param/main.rs index 245f81bfb0d6..ae3af15db9f0 100644 --- a/tests/kani/FunctionCall_Ret-Param/main.rs +++ b/tests/kani/FunctionCall_Ret-Param/main.rs @@ -2,13 +2,13 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --no-unwinding-checks -// cbmc-flags: --unwind 10 // We use `--no-unwinding-checks` in this test to avoid getting // a verification failure (the loop being unwound depends on // a nondet. variable) #[kani::proof] +#[kani::unwind(10)] fn main() { let x: u32 = kani::any(); let pi = 3.14159265359; diff --git a/tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs b/tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs index ab9fa402ea64..408a6badc5f7 100644 --- a/tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs +++ b/tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 //! This test case checks the behavior of size_of_val for traits. use std::mem::size_of_val; diff --git a/tests/kani/Invariants/array.rs b/tests/kani/Invariants/array.rs index 0ee9be7c71cf..e9afc724f539 100644 --- a/tests/kani/Invariants/array.rs +++ b/tests/kani/Invariants/array.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --unwind 3 // Check that the Invariant implementation for array respect the underlying types invariant. extern crate kani; @@ -9,6 +8,7 @@ extern crate kani; use kani::Invariant; #[kani::proof] +#[kani::unwind(3)] fn main() { let arr: [char; 2] = kani::any(); assert!(arr[0].is_valid()); diff --git a/tests/kani/Invariants/array_raw_fail.rs b/tests/kani/Invariants/array_raw_fail.rs index b137a4d3b1fd..621364cea81f 100644 --- a/tests/kani/Invariants/array_raw_fail.rs +++ b/tests/kani/Invariants/array_raw_fail.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --unwind 3 // Check that any_raw for arrays do not respect the elements invariants. extern crate kani; @@ -9,6 +8,7 @@ extern crate kani; use kani::Invariant; #[kani::proof] +#[kani::unwind(3)] fn main() { let arr_raw: [char; 2] = unsafe { kani::any_raw() }; kani::expect_fail(arr_raw[0].is_valid(), "Should fail"); diff --git a/tests/kani/Iterator/into_iter.rs b/tests/kani/Iterator/into_iter.rs index d29ca3baea01..3913ab7f4eb6 100644 --- a/tests/kani/Iterator/into_iter.rs +++ b/tests/kani/Iterator/into_iter.rs @@ -2,11 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // compile-flags: --edition 2018 -// kani-flags: --unwind 4 // // This reproduces the issue seen in "Failures when iterating over results". // See https://github.com/model-checking/kani/issues/556 for more information. #[kani::proof] +#[kani::unwind(4)] pub fn main() { let numbers = vec![1, 10, -1]; let positives: Vec<_> = numbers.into_iter().filter(|&n| n > 0).collect(); diff --git a/tests/kani/Iterator/try_fold.rs b/tests/kani/Iterator/try_fold.rs index aec24b4a008c..ba395e10e12c 100644 --- a/tests/kani/Iterator/try_fold.rs +++ b/tests/kani/Iterator/try_fold.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 3 #[kani::proof] +#[kani::unwind(3)] fn main() { let arr = [(1, 2), (2, 2)]; let result = arr.iter().try_fold((), |acc, &i| Some(())); diff --git a/tests/kani/LoopLoop_NonReturning/main.rs b/tests/kani/LoopLoop_NonReturning/main.rs index a95b81ef77c4..a3c1258d8caa 100644 --- a/tests/kani/LoopLoop_NonReturning/main.rs +++ b/tests/kani/LoopLoop_NonReturning/main.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 10 - #[kani::proof] +#[kani::unwind(10)] fn main() { let mut a: u32 = kani::any(); diff --git a/tests/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/tests/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs index 6a5098c1a1de..1cdf53ed8f87 100644 --- a/tests/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs +++ b/tests/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --no-default-checks -// cbmc-flags: --unwind 9 // This example tests the Kani flag `--no-default-checks` // @@ -22,6 +21,7 @@ // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL #[kani::proof] +#[kani::unwind(9)] fn main() { let mut a: u32 = kani::any(); diff --git a/tests/kani/LoopWhile_NonReturning/main.rs b/tests/kani/LoopWhile_NonReturning/main.rs index 3a85fef3bbc5..8b6984ffd348 100644 --- a/tests/kani/LoopWhile_NonReturning/main.rs +++ b/tests/kani/LoopWhile_NonReturning/main.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 11 - #[kani::proof] +#[kani::unwind(11)] fn main() { let mut a: u32 = kani::any(); diff --git a/tests/kani/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/tests/kani/LoopWhile_NonReturning/main_no_unwind_asserts.rs index c43d77d4da7f..1ab77cfe100e 100644 --- a/tests/kani/LoopWhile_NonReturning/main_no_unwind_asserts.rs +++ b/tests/kani/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --no-default-checks -// cbmc-flags: --unwind 10 // This example tests the Kani flag `--no-default-checks` // @@ -23,6 +22,7 @@ // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL #[kani::proof] +#[kani::unwind(10)] fn main() { let mut a: u32 = kani::any(); diff --git a/tests/kani/NondetSlices/test3.rs b/tests/kani/NondetSlices/test3.rs index 6cb56e4154df..db12628c1b38 100644 --- a/tests/kani/NondetSlices/test3.rs +++ b/tests/kani/NondetSlices/test3.rs @@ -3,7 +3,7 @@ // This test uses kani::slice::any_slice of i32 -// kani-flags: --unwind 6 +// kani-flags: --default-unwind 6 #[kani::proof] fn check_any_slice_i32() { diff --git a/tests/kani/NondetSlices/test4.rs b/tests/kani/NondetSlices/test4.rs index 2c2c4046dccb..ab533d49bf76 100644 --- a/tests/kani/NondetSlices/test4.rs +++ b/tests/kani/NondetSlices/test4.rs @@ -4,7 +4,7 @@ // This test checks that values returned by `kani::slice::any_slice` satisfy the // type invariant -// kani-flags: --unwind 4 +// kani-flags: --default-unwind 4 extern crate kani; use kani::slice::{any_slice, AnySlice}; diff --git a/tests/kani/NondetSlices/test5.rs b/tests/kani/NondetSlices/test5.rs index c7aec940bb1c..0e66657a488a 100644 --- a/tests/kani/NondetSlices/test5.rs +++ b/tests/kani/NondetSlices/test5.rs @@ -4,7 +4,7 @@ // This test checks that values returned by `kani::slice::any_raw_slice` do // *not* necessarily satisfy the type invariant -// kani-flags: --unwind 4 +// kani-flags: --default-unwind 4 extern crate kani; use kani::slice::{any_raw_slice, AnySlice}; diff --git a/tests/kani/PhantomData/phantom_fixme.rs b/tests/kani/PhantomData/phantom_fixme.rs index 2b112244257d..315a9ede0769 100644 --- a/tests/kani/PhantomData/phantom_fixme.rs +++ b/tests/kani/PhantomData/phantom_fixme.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // compile-flags: --edition 2018 -// kani-flags: --unwind 4 +// kani-flags: --default-unwind 4 // // Testcase based on https://doc.rust-lang.org/rust-by-example/generics/phantom/testcase_units.html // which reproduces issue https://github.com/model-checking/kani/issues/560 diff --git a/tests/kani/Projection/fixme_dyn_dyn_projection.rs b/tests/kani/Projection/fixme_dyn_dyn_projection.rs index 0a524b6e59b0..d42ccbf96a5b 100644 --- a/tests/kani/Projection/fixme_dyn_dyn_projection.rs +++ b/tests/kani/Projection/fixme_dyn_dyn_projection.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 //! This test case checks the usage of dyn Trait. use std::mem::size_of_val; diff --git a/tests/kani/Projection/fixme_dyn_slice_projection.rs b/tests/kani/Projection/fixme_dyn_slice_projection.rs index 7fb5ca702c48..a254b2714f87 100644 --- a/tests/kani/Projection/fixme_dyn_slice_projection.rs +++ b/tests/kani/Projection/fixme_dyn_slice_projection.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 //! This test case checks the usage of dyn Trait<[u8]>. use std::mem::size_of_val; diff --git a/tests/kani/Projection/slice_dyn_projection.rs b/tests/kani/Projection/slice_dyn_projection.rs index 527a32eebb0d..8f6a44b3d015 100644 --- a/tests/kani/Projection/slice_dyn_projection.rs +++ b/tests/kani/Projection/slice_dyn_projection.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 //! Check that nested fat pointers work. This used to trigger an issue. //! The projection should only keep track of the inner most dereferenced diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs index c4fc25717e67..31b13315e1b2 100644 --- a/tests/kani/Projection/slice_slice_projection.rs +++ b/tests/kani/Projection/slice_slice_projection.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 5 +// kani-flags: --default-unwind 5 //! This test case checks the usage of slices of slices (&[&[T]]). use std::mem::size_of_val; diff --git a/tests/kani/Slice/main.rs b/tests/kani/Slice/main.rs index 3b3b27d603db..2f996f00b978 100644 --- a/tests/kani/Slice/main.rs +++ b/tests/kani/Slice/main.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 6 - #[kani::proof] +#[kani::unwind(6)] fn main() { let name: &str = "hello"; assert!(name == "hello"); diff --git a/tests/kani/Slice/size_of.rs b/tests/kani/Slice/size_of.rs index 49dcc2ce6b8c..e7ae4b310d3b 100644 --- a/tests/kani/Slice/size_of.rs +++ b/tests/kani/Slice/size_of.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 6 #![feature(core_intrinsics)] #![feature(const_size_of_val)] @@ -11,6 +10,7 @@ pub const fn size_of_val(val: &T) -> usize { } #[kani::proof] +#[kani::unwind(6)] fn main() { let name: &str = "hello"; let len = size_of_val(name); diff --git a/tests/kani/SwitchInt/main.rs b/tests/kani/SwitchInt/main.rs index fa977d38168a..8fe875e137b1 100644 --- a/tests/kani/SwitchInt/main.rs +++ b/tests/kani/SwitchInt/main.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 2 - fn doswitch_int() -> i32 { for i in [99].iter() { if *i == 99 { @@ -31,6 +29,7 @@ fn doswitch_bytes() -> i32 { } #[kani::proof] +#[kani::unwind(2)] fn main() { let v = doswitch_int(); assert!(v == 1); diff --git a/tests/kani/Vectors/fixme_main.rs b/tests/kani/Vectors/fixme_main.rs index 82bbe0d73b79..c2b0d6acfa67 100644 --- a/tests/kani/Vectors/fixme_main.rs +++ b/tests/kani/Vectors/fixme_main.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 0 #[derive(Clone, Copy, Debug, Eq, PartialEq, Ord, PartialOrd)] pub struct GuestAddress(pub u64); @@ -11,6 +10,7 @@ pub struct GuestRegionMmap { // TODO: running this with --unwrap 2 causes CBMC to hang in propositional reduction. #[kani::proof] +#[kani::unwind(0)] fn main() { let r = GuestRegionMmap { guest_base: GuestAddress(0) }; let mut regions: Vec = vec![]; diff --git a/tests/kani/Vectors/vector_extend_in_new.rs b/tests/kani/Vectors/vector_extend_in_new.rs index fee9871faf7f..a2d10f6c24ea 100644 --- a/tests/kani/Vectors/vector_extend_in_new.rs +++ b/tests/kani/Vectors/vector_extend_in_new.rs @@ -5,9 +5,10 @@ // the vec![i; j] constructor. // There is an implicit loop, so we need an explicit unwind -// cbmc-flags: --unwind 3 --unwinding-assertions +// cbmc-flags: --unwinding-assertions #[kani::proof] +#[kani::unwind(3)] fn main() { let a: Vec> = vec![vec![0; 2]; 1]; assert!(a.len() == 1); diff --git a/tests/kani/Vectors/vector_extend_loop.rs b/tests/kani/Vectors/vector_extend_loop.rs index 15772ebffc70..ea5fc8ce8d71 100644 --- a/tests/kani/Vectors/vector_extend_loop.rs +++ b/tests/kani/Vectors/vector_extend_loop.rs @@ -1,9 +1,10 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --unwind 3 +// kani-flags: --default-unwind 3 #[kani::proof] +#[kani::unwind(3)] fn main() { let mut v: Vec = Vec::new(); for (start, len) in vec![(0, 1), (1, 2)] { diff --git a/tests/kani/Whitespace/main.rs b/tests/kani/Whitespace/main.rs index 704b382a832d..211d64a217bf 100644 --- a/tests/kani/Whitespace/main.rs +++ b/tests/kani/Whitespace/main.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 2 - #[kani::proof] +#[kani::unwind(2)] fn main() { let mut iter = "A few words".split_whitespace(); match iter.next() { diff --git a/tests/prusti/Binary_search.rs b/tests/prusti/Binary_search.rs index 76ea4f0c1b9d..edc032068e33 100644 --- a/tests/prusti/Binary_search.rs +++ b/tests/prusti/Binary_search.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-verify-fail -// cbmc-flags: --unwind 4 use std::cmp::Ordering::*; @@ -48,6 +47,7 @@ fn get() -> [i32; 11] { } #[kani::proof] +#[kani::unwind(4)] fn main() { let x = get(); let y = kani::any(); diff --git a/tests/smack/loops/gauss_sum_nondet.rs b/tests/smack/loops/gauss_sum_nondet.rs index cb9fea745e1f..17b5fd3dd8c1 100644 --- a/tests/smack/loops/gauss_sum_nondet.rs +++ b/tests/smack/loops/gauss_sum_nondet.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 5 #[kani::proof] +#[kani::unwind(5)] fn main() { let mut sum = 0; let b: u64 = kani::any(); diff --git a/tests/smack/loops/gauss_sum_nondet_fail.rs b/tests/smack/loops/gauss_sum_nondet_fail.rs index e5bfdf7dfa5d..af3570e8b7da 100644 --- a/tests/smack/loops/gauss_sum_nondet_fail.rs +++ b/tests/smack/loops/gauss_sum_nondet_fail.rs @@ -3,8 +3,9 @@ // @flag --no-memory-splitting --unroll=10 // @expect error // kani-verify-fail -// cbmc-flags: --unwind 5 +#[kani::proof] +#[kani::unwind(5)] pub fn main() { let mut sum = 0; let b: u64 = kani::any(); diff --git a/tests/smack/loops/iterator.rs b/tests/smack/loops/iterator.rs index d9ec0d13d1f4..07d1486c1791 100644 --- a/tests/smack/loops/iterator.rs +++ b/tests/smack/loops/iterator.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 5 - fn fac(n: u64) -> u64 { match n { 0 => 1, @@ -12,6 +10,7 @@ fn fac(n: u64) -> u64 { } #[kani::proof] +#[kani::unwind(5)] fn main() { let mut a = 1; let n = kani::any(); diff --git a/tests/smack/loops/iterator_fail.rs b/tests/smack/loops/iterator_fail.rs index 84cd330f91ee..05557467e710 100644 --- a/tests/smack/loops/iterator_fail.rs +++ b/tests/smack/loops/iterator_fail.rs @@ -3,7 +3,6 @@ // @flag --no-memory-splitting --unroll=10 // @expect error // kani-verify-fail -// cbmc-flags: --unwind 5 fn fac(n: u64) -> u64 { match n { @@ -13,6 +12,8 @@ fn fac(n: u64) -> u64 { } } +#[kani::proof] +#[kani::unwind(5)] pub fn main() { let mut a = 1; let n = kani::any(); diff --git a/tests/ui/check_operations/operations.rs b/tests/ui/check_operations/operations.rs index 6bfcec93b682..c5976ad63b76 100644 --- a/tests/ui/check_operations/operations.rs +++ b/tests/ui/check_operations/operations.rs @@ -2,12 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // // Check the message printed when a checked operation fails. -// kani-flags: --unwind 3 extern crate kani; use kani::any; #[kani::proof] +#[kani::unwind(3)] fn main() { let _ = any::() + any::(); let _ = any::() - any::();