Introduce a kani macro for checking coverage

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -46,6 +46,39 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
     false
 }
 
+struct Cover;
+impl<'tcx> GotocHook<'tcx> for Cover {
+    fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
+        matches_function(tcx, instance, "KaniCover")
+    }
+
+    fn handle(
+        &self,
+        tcx: &mut GotocCtx<'tcx>,
+        _instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        _assign_to: Place<'tcx>,
+        target: Option<BasicBlock>,
+        span: Option<Span>,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let cond = fargs.remove(0).cast_to(Type::bool());
+        let msg = fargs.remove(0);
+        let msg = tcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = tcx.codegen_caller_span(&span);
+        let loc = tcx.codegen_span_option(span);
+
+        Stmt::block(
+            vec![
+                tcx.codegen_cover(cond, &msg, span),
+                Stmt::goto(tcx.current_fn().find_label(&target), caller_loc),
+            ],
+            loc,
+        )
+    }
+}
+
 struct ExpectFail;
 impl<'tcx> GotocHook<'tcx> for ExpectFail {
     fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
@@ -369,6 +402,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
             Rc::new(Panic),
             Rc::new(Assume),
             Rc::new(Assert),
+            Rc::new(Cover),
             Rc::new(ExpectFail),
             Rc::new(Nondet),
             Rc::new(RustAlloc),

kani-driver/src/cbmc_output_parser.rs

@@ -82,10 +82,17 @@ pub struct PropertyId {
 }
 
 impl Property {
+    const COVER_PROPERTY_CLASS: &str = "cover";
+
     pub fn property_class(&self) -> String {
         self.property_id.class.clone()
     }
 
+    /// Returns true if this is a cover property
+    pub fn is_cover_property(&self) -> bool {
+        self.property_id.class == Self::COVER_PROPERTY_CLASS
+    }
+
     pub fn property_name(&self) -> String {
         let class = &self.property_id.class;
         let id = self.property_id.id;
@@ -293,18 +300,22 @@ impl std::fmt::Display for TraceData {
 #[serde(rename_all = "UPPERCASE")]
 pub enum CheckStatus {
     Failure,
+    Satisfied, // for cover properties only
     Success,
     Undetermined,
     Unreachable,
+    Unsatisfiable, // for cover properties only
 }
 
 impl std::fmt::Display for CheckStatus {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let check_str = match self {
+            CheckStatus::Satisfied => style("SATISFIED").green(),
             CheckStatus::Success => style("SUCCESS").green(),
             CheckStatus::Failure => style("FAILURE").red(),
             CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
             CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
+            CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(),
         };
         write!(f, "{check_str}")
     }

kani-driver/src/cbmc_property_renderer.rs

@@ -240,6 +240,12 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
     let mut number_tests_undetermined = 0;
     let mut failed_tests: Vec<&Property> = vec![];
 
+    // cover checks
+    let mut number_covers_satisfied = 0;
+    let mut number_covers_undetermined = 0;
+    let mut number_covers_unreachable = 0;
+    let mut number_covers_unsatisfiable = 0;
+
     let mut index = 1;
 
     if show_checks {
@@ -258,10 +264,26 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
                 failed_tests.push(prop);
             }
             CheckStatus::Undetermined => {
-                number_tests_undetermined += 1;
+                if prop.is_cover_property() {
+                    number_covers_undetermined += 1;
+                } else {
+                    number_tests_undetermined += 1;
+                }
             }
             CheckStatus::Unreachable => {
-                number_tests_unreachable += 1;
+                if prop.is_cover_property() {
+                    number_covers_unreachable += 1;
+                } else {
+                    number_tests_unreachable += 1;
+                }
+            }
+            CheckStatus::Satisfied => {
+                assert!(prop.is_cover_property());
+                number_covers_satisfied += 1;
+            }
+            CheckStatus::Unsatisfiable => {
+                assert!(prop.is_cover_property());
+                number_covers_unsatisfiable += 1;
             }
             _ => (),
         }
@@ -291,7 +313,14 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
         result_str.push_str("\nVERIFICATION RESULT:");
     }
 
-    let summary = format!("\n ** {number_tests_failed} of {} failed", properties.len());
+    let number_cover_properties = number_covers_satisfied
+        + number_covers_unreachable
+        + number_covers_unsatisfiable
+        + number_covers_undetermined;
+
+    let number_properties = properties.len() - number_cover_properties;
+
+    let summary = format!("\n ** {number_tests_failed} of {} failed", number_properties);
     result_str.push_str(&summary);
 
     let mut other_status = Vec::<String>::new();
@@ -310,6 +339,31 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
     }
     result_str.push('\n');
 
+    if number_cover_properties > 0 {
+        // Print a summary line for cover properties
+        let summary = format!(
+            "\n ** {number_covers_unsatisfiable} of {} cover properties unsatisfiable",
+            number_cover_properties
+        );
+        result_str.push_str(&summary);
+        let mut other_status = Vec::<String>::new();
+        if number_covers_undetermined > 0 {
+            let undetermined_str = format!("{number_covers_undetermined} undetermined");
+            other_status.push(undetermined_str);
+        }
+        if number_covers_unreachable > 0 {
+            let unreachable_str = format!("{number_covers_unreachable} unreachable");
+            other_status.push(unreachable_str);
+        }
+        if !other_status.is_empty() {
+            result_str.push_str(" (");
+            result_str.push_str(&other_status.join(","));
+            result_str.push(')');
+        }
+        result_str.push('\n');
+        result_str.push('\n');
+    }
+
     for prop in failed_tests {
         let failure_message = build_failure_message(prop.description.clone(), &prop.trace.clone());
         result_str.push_str(&failure_message);
@@ -413,7 +467,7 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
     let (properties_without_reachs, reach_checks) = filter_reach_checks(properties_with_undefined);
     // Filter out successful sanity checks introduced during compilation
     let properties_without_sanity_checks = filter_sanity_checks(properties_without_reachs);
-    // Annotate properties with the results from reachability checks
+    // Annotate properties with the results of reachability checks
     let properties_annotated =
         annotate_properties_with_reach_results(properties_without_sanity_checks, reach_checks);
     // Remove reachability check IDs from regular property descriptions
@@ -429,7 +483,9 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
         || has_failed_unwinding_asserts
         || has_reachable_undefined_functions;
 
-    update_properties_with_reach_status(properties_filtered, has_fundamental_failures)
+    let updated_properties =
+        update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
+    update_results_of_cover_checks(updated_properties)
 }
 
 /// Determines if there is property with status `FAILURE` and the given description
@@ -495,7 +551,7 @@ fn get_readable_description(property: &Property) -> String {
     original
 }
 
-/// Performs a last pass to update all properties as follows:
+/// Performs a pass to update all properties as follows:
 ///  1. Descriptions are replaced with more readable ones.
 ///  2. If there were failures that made the verification result unreliable
 ///     (e.g., a reachable unsupported construct), changes all `SUCCESS` results
@@ -525,6 +581,23 @@ fn update_properties_with_reach_status(
     properties
 }
 
+/// Update the results of cover properties.
+/// We encode cover(cond) as assert(!cond), so if the assertion
+/// fails, then the cover property is satisfied and vice versa.
+/// - SUCCESS -> UNSATISFIABLE
+/// - FAILURE -> SATISFIED
+fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
+    for prop in properties.iter_mut() {
+        if prop.property_class() == "cover" {
+            if prop.status == CheckStatus::Success {
+                prop.status = CheckStatus::Unsatisfiable;
+            } else if prop.status == CheckStatus::Failure {
+                prop.status = CheckStatus::Satisfied;
+            }
+        }
+    }
+    properties
+}
 /// Some Kani-generated asserts have a unique ID in their description of the form:
 /// ```text
 /// [KANI_CHECK_ID_<crate-fn-name>_<index>]

library/kani/src/lib.rs

@@ -64,6 +64,17 @@ pub const fn assert(_cond: bool, _msg: &'static str) {
     }
 }
 
+/// Creates a cover property with the specified condition and message.
+///
+/// # Example:
+///
+/// ```rust
+/// kani::cover(slice.len() == 0, "The slice may have a length of 0");
+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniCover"]
+pub fn cover(_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.
 ///
@@ -138,5 +149,54 @@ pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 
+/// A macro to check if a condition is satisfiable at a specific location in the
+/// code.
+///
+/// # Example 1:
+///
+/// ```rust
+/// let mut set: BTreeSet<i32> = BTreeSet::new();
+/// set.insert(kani::any());
+/// set.insert(kani::any());
+/// // check if the set can end up with a single element (if both elements
+/// // inserted were the same)
+/// kani::cover!(set.len() == 1);
+/// ```
+/// The macro can also be called without any arguments to check if a location is
+/// reachable.
+///
+/// # Example 2:
+///
+/// ```rust
+/// match e {
+///     MyEnum::A => { /* .. */ }
+///     MyEnum::B => {
+///         // make sure the `MyEnum::B` variant is possible
+///         kani::cover!();
+///         // ..
+///     }
+/// }
+/// ```
+///
+/// A custom message can also be passed to the macro.
+///
+/// # Example 3:
+///
+/// ```rust
+/// kani::cover!(x > y, "x can be greater than y")
+/// ```
+#[macro_export]
+macro_rules! cover {
+    () => {
+        kani::cover(true, "cover location");
+    };
+    ($cond:expr $(,)?) => {
+        kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
+    };
+    ($cond:expr, $msg:literal) => {
+        kani::cover($cond, $msg);
+    };
+}
+
 /// Kani proc macros must be in a separate crate
 pub use kani_macros::*;

tests/expected/cover/cover-fail/expected

@@ -0,0 +1,7 @@
+Status: UNSATISFIABLE\
+Description: "cover location"\
+main.rs:29:23 in function cover_overconstrained
+
+ ** 1 of 1 cover properties unsatisfiable
+
+VERIFICATION:- SUCCESSFUL

tests/expected/cover/cover-fail/main.rs

@@ -0,0 +1,32 @@
+// 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();
+    kani::assume(x != 0);
+    let sign = get_sign(x);
+
+    match sign {
+        Sign::Zero => kani::cover!(),
+        _ => {}
+    }
+}

tests/expected/cover/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
+
+ ** 1 of 3 cover properties unsatisfiable
+
+VERIFICATION:- SUCCESSFUL

tests/expected/cover/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 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!(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
+    }
+}

tests/expected/cover/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
+
+ ** 0 of 2 cover properties unsatisfiable
+
+VERIFICATION:- SUCCESSFUL