cover_or_fail! macro

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);

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<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        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),

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

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 {

kani-driver/src/cbmc_property_renderer.rs

@@ -247,8 +247,9 @@ fn format_item_terse(_item: &ParserItem) -> Option<String> {
 ///
 /// 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
 /// <https://github.com/model-checking/kani/issues/1480>

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`.
 ///

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.
         ///

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

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),
+        _ => {}
+    }
+}

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

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<i32, &'static str> {
+    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
+    }
+}

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

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);
+}

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`.

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);
+}

tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/expected

@@ -0,0 +1,9 @@
+Status: UNREACHABLE\
+Description: "cover location"\
+in function my_function
+
+Status: UNREACHABLE\
+Description: "cover location"\
+in function test
+
+VERIFICATION:- FAILED

tests/expected/cover-or-fail/cover-unreachable-outside-harness-fail/main.rs

@@ -0,0 +1,31 @@
+// 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);
+}
+
+// .filter(|_| false).for_each(|_| {} pattern
+// in https://github.com/model-checking/kani/issues/2792
+fn test() {
+    let my_vec: Vec<u8> = vec![1, 2, 3];
+    my_vec.into_iter().filter(|_| false).for_each(|_| {
+        kani::cover_or_fail!();
+    });
+}
+
+#[kani::proof]
+fn bolero_use_case() {
+    test();
+}

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

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);
+}