From 23f4e70b5c5774bf34921f21ba2d62932215e0b0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 6 Aug 2024 17:09:29 -0400 Subject: [PATCH 1/3] first draft of cover_or_fail with tests --- .../codegen_cprover_gotoc/codegen/assert.rs | 15 +++++++ .../codegen_cprover_gotoc/overrides/hooks.rs | 42 +++++++++++++++++++ kani-driver/src/call_cbmc.rs | 9 +++- kani-driver/src/cbmc_output_parser.rs | 7 ++++ kani-driver/src/cbmc_property_renderer.rs | 5 ++- library/kani/src/lib.rs | 13 ++++++ library/kani_core/src/lib.rs | 10 +++++ .../cover-or-fail/cover-fail/expected | 7 ++++ .../expected/cover-or-fail/cover-fail/main.rs | 31 ++++++++++++++ .../cover-or-fail/cover-message/expected | 15 +++++++ .../cover-or-fail/cover-message/main.rs | 19 +++++++++ .../cover-or-fail/cover-pass/expected | 11 +++++ .../expected/cover-or-fail/cover-pass/main.rs | 14 +++++++ .../cover-or-fail/cover-undetermined/expected | 11 +++++ .../cover-or-fail/cover-undetermined/main.rs | 16 +++++++ .../expected | 7 ++++ .../main.rs | 17 ++++++++ .../expected | 9 ++++ .../main.rs | 31 ++++++++++++++ .../cover-or-fail/cover-unreachable/expected | 16 +++++++ .../cover-or-fail/cover-unreachable/main.rs | 20 +++++++++ tests/expected/cover/cover-message/main.rs | 4 +- 22 files changed, 323 insertions(+), 6 deletions(-) create mode 100644 tests/expected/cover-or-fail/cover-fail/expected create mode 100644 tests/expected/cover-or-fail/cover-fail/main.rs create mode 100644 tests/expected/cover-or-fail/cover-message/expected create mode 100644 tests/expected/cover-or-fail/cover-message/main.rs create mode 100644 tests/expected/cover-or-fail/cover-pass/expected create mode 100644 tests/expected/cover-or-fail/cover-pass/main.rs create mode 100644 tests/expected/cover-or-fail/cover-undetermined/expected create mode 100644 tests/expected/cover-or-fail/cover-undetermined/main.rs create mode 100644 tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected create mode 100644 tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs create mode 100644 tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/expected create mode 100644 tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/main.rs create mode 100644 tests/expected/cover-or-fail/cover-unreachable/expected create mode 100644 tests/expected/cover-or-fail/cover-unreachable/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index f78cf3eba707..05c1005428da 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -45,6 +45,11 @@ pub enum PropertyClass { /// /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure. Cover, + /// See [GotocCtx::codegen_cover] below. Generally just an `assert(false)` that's not an error. + /// + /// SPECIAL BEHAVIOR: Same as PropertyClass::Cover, except unreachable or unsatisfiable + /// conditions cause verification failure. + CoverOrFail, /// The class of checks used for code coverage instrumentation. Only needed /// when working on coverage-related features. /// @@ -147,6 +152,16 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) } + /// Generate code to cover the given condition at the current location + pub fn codegen_cover_or_fail(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt { + let loc = self.codegen_caller_span_stable(span); + // Should use Stmt::cover, but currently this doesn't work with CBMC + // unless it is run with '--cover cover' (see + // https://github.com/diffblue/cbmc/issues/6613). So for now use + // assert(!cond). + self.codegen_assert(cond.not(), PropertyClass::CoverOrFail, msg, loc) + } + /// Generate a cover statement for code coverage reports. pub fn codegen_coverage(&self, span: SpanStable) -> Stmt { let loc = self.codegen_caller_span_stable(span); diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index c0df279932f6..3fe392ece6a2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -79,6 +79,47 @@ impl GotocHook for Cover { } } +/// A hook for Kani's `cover_or_fail` function (declared in `library/kani/src/lib.rs`). +/// The function takes two arguments: a condition expression (bool) and a +/// message (&'static str). +/// The hook codegens the function as a cover property that checks whether the +/// condition is satisfiable. If the condition is undetermined, unreachable, +/// or unsatisfiable, verification fails. +struct CoverOrFail; +impl GotocHook for CoverOrFail { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniCoverOrFail") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + let msg = gcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); + + Stmt::block( + vec![ + reach_stmt, + gcx.codegen_cover_or_fail(cond, &msg, span), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + struct Assume; impl GotocHook for Assume { fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { @@ -547,6 +588,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Assert), Rc::new(Check), Rc::new(Cover), + Rc::new(CoverOrFail), Rc::new(Nondet), Rc::new(IsAllocated), Rc::new(PointerObject), diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 387a9723fcdb..a13e76384d53 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -386,8 +386,13 @@ fn verification_outcome_from_properties( /// Determines the `FailedProperties` variant that corresponds to an array of properties fn determine_failed_properties(properties: &[Property]) -> FailedProperties { - let failed_properties: Vec<&Property> = - properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect(); + let failed_properties: Vec<&Property> = properties + .iter() + .filter(|prop| { + prop.status == CheckStatus::Failure + || (prop.is_cover_or_fail_property() && prop.status != CheckStatus::Satisfied) + }) + .collect(); // Return `FAILURE` if there isn't at least one failed property if failed_properties.is_empty() { FailedProperties::None diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index b3a78e8d03e2..3df5cd076e18 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -96,6 +96,7 @@ pub struct PropertyId { impl Property { const COVER_PROPERTY_CLASS: &'static str = "cover"; + const COVER_OR_FAIL_PROPERTY_CLASS: &'static str = "cover_or_fail"; const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage"; pub fn property_class(&self) -> String { @@ -110,6 +111,12 @@ impl Property { /// Returns true if this is a cover property pub fn is_cover_property(&self) -> bool { self.property_id.class == Self::COVER_PROPERTY_CLASS + || self.property_id.class == Self::COVER_OR_FAIL_PROPERTY_CLASS + } + + /// Returns true if this is a cover or fail property + pub fn is_cover_or_fail_property(&self) -> bool { + self.property_id.class == Self::COVER_OR_FAIL_PROPERTY_CLASS } pub fn property_name(&self) -> String { diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 4f32028b5866..de592fd343bc 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -247,8 +247,9 @@ fn format_item_terse(_item: &ParserItem) -> Option { /// /// This function reports the results of normal checks (e.g. assertions and /// arithmetic overflow checks) and cover properties (specified using the -/// `kani::cover` macro) separately. Cover properties currently do not impact -/// the overall verification success or failure. +/// `kani::cover` or `kani::cover_or_fail` macros) separately. +/// The results of `kani::cover` do not affect overall verification success or failure, +/// while any unreachable or unsatisfiable `kani::cover_or_fail`s will trigger verification failure. /// /// TODO: We could `write!` to `result_str` instead /// diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 59a89622a52d..c8ff7cd8e16e 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -73,6 +73,19 @@ macro_rules! cover { }; } +#[macro_export] +macro_rules! cover_or_fail { + () => { + kani::cover_or_fail(true, "cover location"); + }; + ($cond:expr $(,)?) => { + kani::cover_or_fail($cond, concat!("cover condition: ", stringify!($cond))); + }; + ($cond:expr, $msg:literal) => { + kani::cover_or_fail($cond, $msg); + }; +} + /// `implies!(premise => conclusion)` means that if the `premise` is true, so /// must be the `conclusion`. /// diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 6cbe98d30df2..c0ac51e7b357 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -176,6 +176,16 @@ macro_rules! kani_intrinsics { #[rustc_diagnostic_item = "KaniCover"] pub const fn cover(_cond: bool, _msg: &'static str) {} + /// Creates a cover property with the specified condition and message. + /// Provides the same functionality as `kani::cover` with the additional constraint that + /// unreachability or unsatisfiability causes verification failure. + /// See `kani::cover` for examples. + /// This function is called by the [`cover_or_fail!`] macro. The macro is more + /// convenient to use. + #[inline(never)] + #[rustc_diagnostic_item = "KaniCoverOrFail"] + pub const fn cover_or_fail(_cond: bool, _msg: &'static str) {} + /// This creates an symbolic *valid* value of type `T`. You can assign the return value of this /// function to a variable that you want to make symbolic. /// diff --git a/tests/expected/cover-or-fail/cover-fail/expected b/tests/expected/cover-or-fail/cover-fail/expected new file mode 100644 index 000000000000..efd668eabaa6 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-fail/expected @@ -0,0 +1,7 @@ +Status: UNSATISFIABLE\ +Description: "cover condition: x != 0"\ +in function cover_overconstrained + + ** 0 of 1 cover properties satisfied + +VERIFICATION:- FAILED diff --git a/tests/expected/cover-or-fail/cover-fail/main.rs b/tests/expected/cover-or-fail/cover-fail/main.rs new file mode 100644 index 000000000000..250e764f1a5a --- /dev/null +++ b/tests/expected/cover-or-fail/cover-fail/main.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that overconstraining could lead to unsatisfiable cover statements + +enum Sign { + Positive, + Negative, + Zero, +} + +fn get_sign(x: i32) -> Sign { + if x > 0 { + Sign::Positive + } else if x < 0 { + Sign::Negative + } else { + Sign::Zero + } +} + +#[kani::proof] +fn cover_overconstrained() { + let x: i32 = kani::any(); + let sign = get_sign(x); + + match sign { + Sign::Zero => kani::cover_or_fail!(x != 0), + _ => {} + } +} diff --git a/tests/expected/cover-or-fail/cover-message/expected b/tests/expected/cover-or-fail/cover-message/expected new file mode 100644 index 000000000000..d2b3e0208d76 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-message/expected @@ -0,0 +1,15 @@ +Status: SATISFIED\ +Description: "foo may return Err"\ +main.rs:17:20 in function cover_match + +Status: SATISFIED\ +Description: "y may be greater than 20"\ +main.rs:15:28 in function cover_match + +Status: UNSATISFIABLE\ +Description: "y may be greater than 10"\ +main.rs:16:18 in function cover_match + + ** 2 of 3 cover properties satisfied + +VERIFICATION:- FAILED diff --git a/tests/expected/cover-or-fail/cover-message/main.rs b/tests/expected/cover-or-fail/cover-message/main.rs new file mode 100644 index 000000000000..72a28b385237 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-message/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that the message used in the kani::cover_or_fail macro appears in the results + +fn foo(x: i32) -> Result { + if x < 100 { Ok(x / 2) } else { Err("x is too big") } +} + +#[kani::proof] +#[kani::unwind(21)] +fn cover_match() { + let x = kani::any(); + match foo(x) { + Ok(y) if x > 20 => kani::cover_or_fail!(y > 20, "y may be greater than 20"), // satisfiable + Ok(y) => kani::cover_or_fail!(y > 10, "y may be greater than 10"), // unsatisfiable + Err(_s) => kani::cover_or_fail!(true, "foo may return Err"), // satisfiable + } +} diff --git a/tests/expected/cover-or-fail/cover-pass/expected b/tests/expected/cover-or-fail/cover-pass/expected new file mode 100644 index 000000000000..59b85ec64ee1 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-pass/expected @@ -0,0 +1,11 @@ +Status: SATISFIED\ +Description: "cover condition: sorted == arr"\ +main.rs:12:5 in function cover_sorted + +Status: SATISFIED\ +Description: "cover condition: sorted != arr"\ +main.rs:13:5 in function cover_sorted + + ** 2 of 2 cover properties satisfied + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover-or-fail/cover-pass/main.rs b/tests/expected/cover-or-fail/cover-pass/main.rs new file mode 100644 index 000000000000..e9fe658ddb93 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-pass/main.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that a sorted array may be the same or different than the original + +#[kani::proof] +#[kani::unwind(21)] +fn cover_sorted() { + let arr: [i32; 5] = kani::any(); + let mut sorted = arr.clone(); + sorted.sort(); + kani::cover_or_fail!(sorted == arr); + kani::cover_or_fail!(sorted != arr); +} diff --git a/tests/expected/cover-or-fail/cover-undetermined/expected b/tests/expected/cover-or-fail/cover-undetermined/expected new file mode 100644 index 000000000000..dcbc9fddb12e --- /dev/null +++ b/tests/expected/cover-or-fail/cover-undetermined/expected @@ -0,0 +1,11 @@ +Status: UNDETERMINED\ +Description: "cover condition: sum == 10"\ +main.rs:15:5 in function cover_undetermined + + ** 0 of 1 cover properties satisfied (1 undetermined) + +Failed Checks: unwinding assertion loop 0 + +VERIFICATION:- FAILED +[Kani] info: Verification output shows one or more unwinding failures. +[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. diff --git a/tests/expected/cover-or-fail/cover-undetermined/main.rs b/tests/expected/cover-or-fail/cover-undetermined/main.rs new file mode 100644 index 000000000000..666f5161cdb7 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-undetermined/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that a failed unwinding assertion would lead to reporting a cover +/// property as UNDETERMINED if it's not satisfiable with the given unwind bound + +#[kani::proof] +#[kani::unwind(10)] +fn cover_undetermined() { + let x = [1; 10]; + let mut sum = 0; + for i in x { + sum += i; + } + kani::cover_or_fail!(sum == 10); +} diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected new file mode 100644 index 000000000000..060fd20dd324 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected @@ -0,0 +1,7 @@ +Status: UNREACHABLE\ +Description: "cover location"\ +in function my_function + + ** 0 of 1 cover properties satisfied (1 unreachable) + +VERIFICATION:- FAILED diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs new file mode 100644 index 000000000000..a6676cd918aa --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Example of cover_or_fail being used outside a proof harness with an unreachability failure + +fn my_function(x: bool) { + if x { + kani::cover_or_fail!(); + } +} + +#[kani::proof] +fn proof() { + // Since my_function() *is* reachable from the proof harness (i.e., CBMC's entry point), + // but the kani::cover_or_fail!() call *may or may not be* reachable, verification fails + my_function(false); +} diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/expected b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/expected new file mode 100644 index 000000000000..f64080f966fe --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/expected @@ -0,0 +1,9 @@ +Status: SUCCESS\ +Description: "assertion failed: true"\ +in function proof_a + +Status: SUCCESS\ +Description: "assertion failed: true"\ +in function proof_b + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/main.rs b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/main.rs new file mode 100644 index 000000000000..951dac1668bb --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-pass/main.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Examples of cover_or_fail being used outside proof harnesses +// Both of these calls are unreachable from the proof harness, +// yet verification succeeds + +fn my_function() { + kani::cover_or_fail!(); +} + +#[kani::proof] +fn proof_a() { + // Since my_function() isn't reachable from the proof harness (i.e., CBMC's entry point), + // the verification succeeds + assert!(true); +} + +fn my_function_b() { + if false { + kani::cover_or_fail!(); + } +} + +#[kani::proof] +fn proof_b() { + // The kani::cover_or_fail call in my_function_b() gets optimized out because it will never be called, + // so we don't execute the coverage check and verification succeeds + my_function_b(); + assert!(true); +} diff --git a/tests/expected/cover-or-fail/cover-unreachable/expected b/tests/expected/cover-or-fail/cover-unreachable/expected new file mode 100644 index 000000000000..8da400b53c2b --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable/expected @@ -0,0 +1,16 @@ +Status: UNREACHABLE\ +Description: "cover condition: x == 2"\ +in function cover_unreachable + +Status: UNREACHABLE\ +Description: "Unreachable with a message"\ +in function cover_unreachable + +Status: SATISFIED\ +Description: "cover condition: x == 5"\ +in function cover_unreachable + + + ** 1 of 3 cover properties satisfied (2 unreachable) + +VERIFICATION:- FAILED diff --git a/tests/expected/cover-or-fail/cover-unreachable/main.rs b/tests/expected/cover-or-fail/cover-unreachable/main.rs new file mode 100644 index 000000000000..7876f1902b19 --- /dev/null +++ b/tests/expected/cover-or-fail/cover-unreachable/main.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that Kani reports an unreachable cover property as such + +#[kani::proof] +fn cover_unreachable() { + let x: i32 = kani::any(); + if x > 10 { + if x < 5 { + kani::cover_or_fail!(x == 2); // unreachable + } + } else { + if x > 20 { + kani::cover_or_fail!(x == 30, "Unreachable with a message"); // unreachable + } else { + kani::cover_or_fail!(x == 5); // satisfiable + } + } +} diff --git a/tests/expected/cover/cover-message/main.rs b/tests/expected/cover/cover-message/main.rs index 3e40a90d05a0..8c5400cf8ed8 100644 --- a/tests/expected/cover/cover-message/main.rs +++ b/tests/expected/cover/cover-message/main.rs @@ -13,7 +13,7 @@ fn cover_match() { let x = kani::any(); match foo(x) { Ok(y) if x > 20 => kani::cover!(y > 20, "y may be greater than 20"), // satisfiable - Ok(y) => kani::cover!(y > 10, "y may be greater than 10"), // unsatisfiable - Err(_s) => kani::cover!(true, "foo may return Err"), // satisfiable + Ok(y) => kani::cover!(y > 10, "y may be greater than 10"), // unsatisfiable + Err(_s) => kani::cover!(true, "foo may return Err"), // satisfiable } } From 9857cc8724fc51dc19e2511a29954875b8c0167c Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 6 Aug 2024 18:50:37 -0400 Subject: [PATCH 2/3] add test case similar to bolero issue --- .../expected | 4 +++- .../cover-unreachable-outside-harness-fail/main.rs | 14 ++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected index 060fd20dd324..32750cf08918 100644 --- a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected @@ -2,6 +2,8 @@ Status: UNREACHABLE\ Description: "cover location"\ in function my_function - ** 0 of 1 cover properties satisfied (1 unreachable) +Status: UNREACHABLE\ +Description: "cover location"\ +in function test VERIFICATION:- FAILED diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs index a6676cd918aa..7b72d6ac9caf 100644 --- a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs @@ -15,3 +15,17 @@ fn proof() { // but the kani::cover_or_fail!() call *may or may not be* reachable, verification fails my_function(false); } + +// Simplified version of the .filter(|_| false).for_each(|_| {} pattern +// in https://github.com/model-checking/kani/issues/2792 +fn test() { + let my_vec: Vec = vec![1, 2, 3]; + my_vec.into_iter().filter(|_| false).for_each(|_| { + kani::cover_or_fail!(); + }); +} + +#[kani::proof] +fn bolero_use_case() { + test(); +} From 7f263f7536b2f5de097b833b44853a22838d67e8 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 7 Aug 2024 09:38:35 -0400 Subject: [PATCH 3/3] make clippy happy --- .../cover-unreachable-outside-harness-fail/main.rs | 2 +- tests/expected/cover/cover-message/main.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs index 7b72d6ac9caf..e86c78c509c0 100644 --- a/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs +++ b/tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs @@ -16,7 +16,7 @@ fn proof() { my_function(false); } -// Simplified version of the .filter(|_| false).for_each(|_| {} pattern +// .filter(|_| false).for_each(|_| {} pattern // in https://github.com/model-checking/kani/issues/2792 fn test() { let my_vec: Vec = vec![1, 2, 3]; diff --git a/tests/expected/cover/cover-message/main.rs b/tests/expected/cover/cover-message/main.rs index 8c5400cf8ed8..3e40a90d05a0 100644 --- a/tests/expected/cover/cover-message/main.rs +++ b/tests/expected/cover/cover-message/main.rs @@ -13,7 +13,7 @@ fn cover_match() { let x = kani::any(); match foo(x) { Ok(y) if x > 20 => kani::cover!(y > 20, "y may be greater than 20"), // satisfiable - Ok(y) => kani::cover!(y > 10, "y may be greater than 10"), // unsatisfiable - Err(_s) => kani::cover!(true, "foo may return Err"), // satisfiable + Ok(y) => kani::cover!(y > 10, "y may be greater than 10"), // unsatisfiable + Err(_s) => kani::cover!(true, "foo may return Err"), // satisfiable } }