Introduce a kani macro for checking coverage (#2011)

Author: zhassan-aws

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

@@ -46,6 +46,47 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
     false
 }
 
+/// A hook for Kani's `cover` 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. Unlike assertions, cover properties currently do
+/// not have an impact on verification success or failure. See
+/// <https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0003-cover-statement.md>
+/// for more details.
+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 +410,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

@@ -231,15 +231,26 @@ fn format_item_terse(_item: &ParserItem) -> Option<String> {
 /// This could be split into two functions for clarity, but at the moment
 /// it uses the flag `show_checks` which depends on the output format.
 ///
+/// 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.
+///
 /// TODO: We could `write!` to `result_str` instead
 /// <https://github.com/model-checking/kani/issues/1480>
 pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
     let mut result_str = String::new();
-    let mut number_tests_failed = 0;
-    let mut number_tests_unreachable = 0;
-    let mut number_tests_undetermined = 0;
+    let mut number_checks_failed = 0;
+    let mut number_checks_unreachable = 0;
+    let mut number_checks_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 {
@@ -254,14 +265,30 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
 
         match status {
             CheckStatus::Failure => {
-                number_tests_failed += 1;
+                number_checks_failed += 1;
                 failed_tests.push(prop);
             }
             CheckStatus::Undetermined => {
-                number_tests_undetermined += 1;
+                if prop.is_cover_property() {
+                    number_covers_undetermined += 1;
+                } else {
+                    number_checks_undetermined += 1;
+                }
             }
             CheckStatus::Unreachable => {
-                number_tests_unreachable += 1;
+                if prop.is_cover_property() {
+                    number_covers_unreachable += 1;
+                } else {
+                    number_checks_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,16 +318,23 @@ 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_checks_failed} of {} failed", number_properties);
     result_str.push_str(&summary);
 
     let mut other_status = Vec::<String>::new();
-    if number_tests_undetermined > 0 {
-        let undetermined_str = format!("{number_tests_undetermined} undetermined");
+    if number_checks_undetermined > 0 {
+        let undetermined_str = format!("{number_checks_undetermined} undetermined");
         other_status.push(undetermined_str);
     }
-    if number_tests_unreachable > 0 {
-        let unreachable_str = format!("{number_tests_unreachable} unreachable");
+    if number_checks_unreachable > 0 {
+        let unreachable_str = format!("{number_checks_unreachable} unreachable");
         other_status.push(unreachable_str);
     }
     if !other_status.is_empty() {
@@ -310,13 +344,38 @@ 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_satisfied} of {} cover properties satisfied",
+            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);
     }
 
     let verification_result =
-        if number_tests_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() };
+        if number_checks_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() };
     let overall_result = format!("\nVERIFICATION:- {verification_result}\n");
     result_str.push_str(&overall_result);
 
@@ -413,7 +472,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 +488,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 +556,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 +586,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.is_cover_property() {
+            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,28 @@ 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");
+/// ```
+///
+/// A cover property checks if there is at least one execution that satisfies
+/// the specified condition at the location in which the function is called.
+///
+/// Cover properties are reported as:
+///  - SATISFIED: if Kani found an execution that satisfies the condition
+///  - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied
+///
+/// This function is called by the [`cover!`] macro. The macro is more
+/// convenient to use.
+///
+#[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 +160,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
+
+ ** 0 of 1 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL