Add reachability checks for cover properties (rust-lang#2024)

Co-authored-by: Celina G. Val <[email protected]>

Author: zhassan-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -21,6 +21,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
+use kani_queries::UserInput;
 use rustc_span::Span;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
@@ -59,6 +60,9 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
     FiniteCheck,
+    /// Checks added by Kani compiler to determine whether a property (e.g.
+    /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable
+    ReachabilityCheck,
     /// Checks added by Kani compiler to detect safety conditions violation.
     /// E.g., things that trigger UB or unstable behavior.
     ///
@@ -134,9 +138,41 @@ impl<'tcx> GotocCtx<'tcx> {
     // The above represent the basic operations we can perform w.r.t. assert/assume/cover
     // Below are various helper functions for constructing the above more easily.
 
-    /// A shorthand for cover(true)
-    pub fn codegen_cover_loc(&self, msg: &str, span: Option<Span>) -> Stmt {
-        self.codegen_cover(Expr::bool_true(), msg, span)
+    /// Given the message for a property, generate a reachability check that is
+    /// meant to check whether the property is reachable. The function returns a
+    /// modified version of the provided message that should be used for the
+    /// property to allow the CBMC output parser to pair the property with its
+    /// reachability check.
+    /// If reachability checks are disabled, the function returns the message
+    /// unmodified and an empty (skip) statement.
+    pub fn codegen_reachability_check(
+        &mut self,
+        msg: String,
+        span: Option<Span>,
+    ) -> (String, Stmt) {
+        let loc = self.codegen_caller_span(&span);
+        if self.queries.get_check_assertion_reachability() {
+            // Generate a unique ID for the assert
+            let assert_id = self.next_check_id();
+            // Generate a message for the reachability check that includes the unique ID
+            let reach_msg = assert_id.clone();
+            // Also add the unique ID as a prefix to the assert message so that it can be
+            // easily paired with the reachability check
+            let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id);
+            // inject a reachability check, which is a (non-blocking)
+            // assert(false) whose failure indicates that this line is reachable.
+            // The property class (`PropertyClass:ReachabilityCheck`) is used by
+            // the CBMC output parser to distinguish those checks from others.
+            let check = self.codegen_assert(
+                Expr::bool_false(),
+                PropertyClass::ReachabilityCheck,
+                &reach_msg,
+                loc,
+            );
+            (msg, check)
+        } else {
+            (msg, Stmt::skip(loc))
+        }
     }
 
     /// A shorthand for generating a CBMC assert-assume(false)

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -6,7 +6,6 @@ use super::PropertyClass;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use kani_queries::UserInput;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
@@ -226,16 +225,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     msg.description()
                 };
 
-                // TODO: switch to tagging assertions via the property class once CBMC allows that:
-                // https://github.com/diffblue/cbmc/issues/6692
-                let (msg_str, reach_stmt) = if self.queries.get_check_assertion_reachability() {
-                    let check_id = self.next_check_id();
-                    let msg_str = GotocCtx::add_prefix_to_msg(msg, &check_id);
-                    let reach_msg = GotocCtx::reachability_check_message(&check_id);
-                    (msg_str, self.codegen_cover_loc(&reach_msg, Some(term.source_info.span)))
-                } else {
-                    (msg.to_string(), Stmt::skip(loc))
-                };
+                let (msg_str, reach_stmt) =
+                    self.codegen_reachability_check(msg.to_owned(), Some(term.source_info.span));
 
                 Stmt::block(
                     vec![

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

@@ -12,7 +12,6 @@ use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
-use kani_queries::UserInput;
 use rustc_middle::mir::{BasicBlock, Place};
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{Instance, TyCtxt};
@@ -75,14 +74,16 @@ impl<'tcx> GotocHook<'tcx> for Cover {
         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);
+
+        let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span);
 
         Stmt::block(
             vec![
+                reach_stmt,
                 tcx.codegen_cover(cond, &msg, span),
                 Stmt::goto(tcx.current_fn().find_label(&target), caller_loc),
             ],
-            loc,
+            caller_loc,
         )
     }
 }
@@ -139,20 +140,7 @@ impl<'tcx> GotocHook<'tcx> for Assert {
         let target = target.unwrap();
         let caller_loc = tcx.codegen_caller_span(&span);
 
-        // TODO: switch to tagging assertions via the property class once CBMC allows that:
-        // https://github.com/diffblue/cbmc/issues/6692
-        let (msg, reach_stmt) = if tcx.queries.get_check_assertion_reachability() {
-            // Generate a unique ID for the assert
-            let assert_id = tcx.next_check_id();
-            // Add this ID as a prefix to the assert message so that it can be
-            // easily paired with the reachability check
-            let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id);
-            let reach_msg = GotocCtx::reachability_check_message(&assert_id);
-            // inject a reachability (cover) check to the current location
-            (msg, tcx.codegen_cover_loc(&reach_msg, span))
-        } else {
-            (msg, Stmt::skip(caller_loc))
-        };
+        let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span);
 
         // Since `cond` might have side effects, assign it to a temporary
         // variable so that it's evaluated once, then assert and assume it

kani-compiler/src/codegen_cprover_gotoc/utils/names.rs

@@ -117,15 +117,6 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn add_prefix_to_msg(msg: &str, prefix: &str) -> String {
         format!("[{prefix}] {msg}")
     }
-
-    /// Generate a message for the reachability check of an assert with ID
-    /// `check_id`. The message is of the form:
-    /// \[KANI_REACHABILITY_CHECK\] `<ID of assert>`
-    /// The check_id is generated using the GotocCtx::next_check_id method and
-    /// is a unique string identifier for that check.
-    pub fn reachability_check_message(check_id: &str) -> String {
-        format!("[KANI_REACHABILITY_CHECK] {check_id}")
-    }
 }
 
 /// The full crate name should use the Codegen Unit builder to include full name resolution,

kani-driver/src/cbmc_property_renderer.rs

@@ -151,7 +151,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
 const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
 const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
 const DEFAULT_ASSERTION: &str = "assertion";
-const REACH_CHECK_DESC: &str = "[KANI_REACHABILITY_CHECK]";
 
 impl ParserItem {
     /// Determines if an item must be skipped or not.
@@ -591,6 +590,9 @@ fn update_properties_with_reach_status(
 /// fails, then the cover property is satisfied and vice versa.
 /// - SUCCESS -> UNSATISFIABLE
 /// - FAILURE -> SATISFIED
+/// Note that if the cover property was unreachable, its status at this point
+/// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
+/// `update_properties_with_reach_status` is called beforehand
 fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
@@ -622,25 +624,12 @@ fn remove_check_ids_from_description(mut properties: Vec<Property>) -> Vec<Prope
     properties
 }
 
-/// Given a description, this splits properties into two groups:
-///  1. Properties that don't contain the description
-///  2. Properties that contain the description
-fn filter_properties(properties: Vec<Property>, message: &str) -> (Vec<Property>, Vec<Property>) {
-    let mut filtered_properties = Vec::<Property>::new();
-    let mut removed_properties = Vec::<Property>::new();
-    for prop in properties {
-        if prop.description.contains(message) {
-            removed_properties.push(prop);
-        } else {
-            filtered_properties.push(prop);
-        }
-    }
-    (filtered_properties, removed_properties)
-}
-
-/// Filters reachability checks with `filter_properties`
+/// Partitions `properties` into reachability checks (identified by the
+/// "reachability_check" property class) and non-reachability checks
 fn filter_reach_checks(properties: Vec<Property>) -> (Vec<Property>, Vec<Property>) {
-    filter_properties(properties, REACH_CHECK_DESC)
+    let (reach_checks, other_checks): (Vec<_>, Vec<_>) =
+        properties.into_iter().partition(|prop| prop.property_class() == "reachability_check");
+    (other_checks, reach_checks)
 }
 
 /// Filters out Kani-generated sanity checks with a `SUCCESS` status
@@ -680,11 +669,11 @@ fn filter_ptr_checks(properties: Vec<Property>) -> Vec<Property> {
 /// includes the ID of the assert for which we want to check its reachability.
 /// The description of a reachability check uses the following template:
 /// ```text
-/// [KANI_REACHABILITY_CHECK] <ID of original assert>
+/// <ID of original assert>
 /// ```
 /// e.g.:
 /// ```text
-/// [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_foo.6875c808::foo_0
+/// KANI_CHECK_ID_foo.6875c808::foo_0
 /// ```
 /// This function first collects all data from reachability checks. Then,
 /// it updates the reachability status for all properties accordingly.

library/kani/src/lib.rs

@@ -78,6 +78,7 @@ pub const fn assert(_cond: bool, _msg: &'static str) {
 /// 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
+///  - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE)
 ///
 /// This function is called by the [`cover!`] macro. The macro is more
 /// convenient to use.

tests/expected/cover/cover-fail/expected

@@ -1,6 +1,6 @@
 Status: UNSATISFIABLE\
-Description: "cover location"\
-main.rs:29:23 in function cover_overconstrained
+Description: "cover condition: x != 0"\
+in function cover_overconstrained
 
  ** 0 of 1 cover properties satisfied
 

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

@@ -22,11 +22,10 @@ fn get_sign(x: i32) -> Sign {
 #[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!(),
+        Sign::Zero => kani::cover!(x != 0),
         _ => {}
     }
 }

tests/expected/cover/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:- SUCCESSFUL

tests/expected/cover/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!(x == 2); // unreachable
+        }
+    } else {
+        if x > 20 {
+            kani::cover!(x == 30, "Unreachable with a message"); // unreachable
+        } else {
+            kani::cover!(x == 5); // satisfiable
+        }
+    }
+}