Add reachability checks for some auto-generated asserts (#838)

scripts/cbmc_json_parser.py

@@ -203,6 +203,7 @@ def postprocess_results(properties):
     has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC)
     properties, reach_checks = filter_reach_checks(properties)
     annotate_properties_with_reach_results(properties, reach_checks)
+    remove_check_ids_from_description(properties)
 
     for property in properties:
         if has_reachable_unsupported_constructs or has_failed_unwinding_asserts:
@@ -283,9 +284,6 @@ def annotate_properties_with_reach_results(properties, reach_checks):
         prop = get_matching_property(properties, check_id)
         # Attach the result of the reachability check to this property
         prop[GlobalMessages.REACH_CHECK_KEY] = reach_check["status"]
-        # Remove the ID from the property's description so that it's not shown
-        # to the user
-        prop["description"] = prop["description"].replace("[" + check_id + "] ", "", 1)
 
 
 def get_matching_property(properties, check_id):
@@ -298,6 +296,26 @@ def get_matching_property(properties, check_id):
     raise Exception("Error: failed to find a property with ID \"" + check_id + "\"")
 
 
+def remove_check_ids_from_description(properties):
+    """
+    Some asserts generated by Kani have a unique ID in their description that is
+    of the form:
+
+    [KANI_CHECK_ID_<crate-fn-name>_<index>]
+
+    e.g.:
+
+    [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0
+
+    This function removes those IDs from the property's description so that
+    they're not shown to the user. The removal of the IDs should only be done
+    after all ID-based post-processing is done.
+    """
+    check_id_pattern = re.compile(r"\[" + GlobalMessages.CHECK_ID + r"_.*_[0-9]*\] ")
+    for property in properties:
+        property["description"] = re.sub(check_id_pattern, "", property["description"])
+
+
 def construct_solver_information_message(solver_information):
     """
     From the extracted information, construct a message and append to the final Output

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

@@ -5,6 +5,7 @@ use super::typ::FN_RETURN_VOID_VAR_NAME;
 use crate::codegen_cprover_gotoc::utils;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
+use kani_queries::UserInput;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
@@ -89,15 +90,27 @@ 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))
+                };
+
                 Stmt::block(
                     vec![
+                        reach_stmt,
                         cond.cast_to(Type::bool()).if_then_else(
-                            Stmt::goto(self.current_fn().find_label(target), loc.clone()),
+                            Stmt::goto(self.current_fn().find_label(target), loc),
                             None,
-                            loc.clone(),
+                            loc,
                         ),
-                        Stmt::assert_false(msg, loc.clone()),
-                        Stmt::goto(self.current_fn().find_label(target), loc.clone()),
+                        Stmt::assert_false(&msg_str, loc),
+                        Stmt::goto(self.current_fn().find_label(target), loc),
                     ],
                     loc,
                 )

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

@@ -165,34 +165,38 @@ impl<'tcx> GotocHook<'tcx> for Assert {
         assert_eq!(fargs.len(), 2);
         let cond = fargs.remove(0).cast_to(Type::bool());
         let msg = fargs.remove(0);
-        let mut msg = utils::extract_const_message(&msg).unwrap();
+        let msg = utils::extract_const_message(&msg).unwrap();
         let target = target.unwrap();
         let caller_loc = tcx.codegen_caller_span(&span);
 
-        let mut stmts: Vec<Stmt> = Vec::new();
-
-        if tcx.queries.get_check_assertion_reachability() {
+        // 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();
-            // Use a description of the form:
-            // [KANI_REACHABILITY_CHECK] <check ID>
-            // for reachability checks
-            msg = format!("[{}] {}", assert_id, msg);
-            let reach_msg = format!("[KANI_REACHABILITY_CHECK] {}", assert_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
-            stmts.push(tcx.codegen_cover_loc(&reach_msg, span));
-        }
+            (msg, tcx.codegen_cover_loc(&reach_msg, span))
+        } else {
+            (msg, Stmt::skip(caller_loc))
+        };
 
         // Since `cond` might have side effects, assign it to a temporary
         // variable so that it's evaluated once, then assert and assume it
         let tmp = tcx.gen_temp_variable(cond.typ().clone(), caller_loc.clone()).to_expr();
-        stmts.append(&mut vec![
-            Stmt::decl(tmp.clone(), Some(cond), caller_loc.clone()),
-            Stmt::assert(tmp.clone(), &msg, caller_loc.clone()),
-            Stmt::assume(tmp, caller_loc.clone()),
-            Stmt::goto(tcx.current_fn().find_label(&target), caller_loc.clone()),
-        ]);
-        Stmt::block(stmts, caller_loc)
+        Stmt::block(
+            vec![
+                reach_stmt,
+                Stmt::decl(tmp.clone(), Some(cond), caller_loc.clone()),
+                Stmt::assert(tmp.clone(), &msg, caller_loc.clone()),
+                Stmt::assume(tmp, caller_loc.clone()),
+                Stmt::goto(tcx.current_fn().find_label(&target), caller_loc.clone()),
+            ],
+            caller_loc,
+        )
     }
 }
 

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

@@ -109,6 +109,22 @@ impl<'tcx> GotocCtx<'tcx> {
         // TODO: use def_id https://github.com/model-checking/kani/issues/364
         idx.to_string().into()
     }
+
+    /// Add a prefix of the form:
+    /// [<prefix>]
+    /// to the provided message
+    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,

tests/expected/reach/bounds/reachable_fail/expected

@@ -0,0 +1,2 @@
+FAILURE
+Failed Checks: index out of bounds: the length is less than or equal to the given index

tests/expected/reach/bounds/reachable_fail/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// index-out-of-bounds checks and that it reports ones that are unreachable.
+// The check in this test is reachable and doesn't hold, so should be reported
+// as FAILURE
+
+fn get(s: &[i16], index: usize) -> i16 {
+    s[index]
+}
+
+fn main() {
+    get(&[7, -83, 19], 15);
+}

tests/expected/reach/bounds/reachable_pass/expected

@@ -0,0 +1 @@
+SUCCESS

tests/expected/reach/bounds/reachable_pass/test.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// index-out-of-bounds checks and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn get(s: &[i16], index: usize) -> i16 {
+    if index < s.len() { s[index] } else { -1 }
+}
+
+fn main() {
+    get(&[7, -83, 19], 2);
+}

tests/expected/reach/bounds/unreachable/expected

@@ -0,0 +1 @@
+UNREACHABLE

tests/expected/reach/bounds/unreachable/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// index-out-of-bounds checks and that it reports ones that are unreachable.
+// The check in this test is unreachable, so should be reported as UNREACHABLE
+
+fn get(s: &[i16], index: usize) -> i16 {
+    if index < s.len() { s[index] } else { -1 }
+}
+
+fn main() {
+    //get(&[7, -83, 19], 2);
+    get(&[5, 206, -46, 321, 8], 8);
+}

tests/expected/reach/div-zero/reachable_fail/expected

@@ -0,0 +1,2 @@
+FAILURE
+Failed Checks: attempt to divide by zero

tests/expected/reach/div-zero/reachable_fail/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// divide-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable and doesn't hold, so should be reported
+// as FAILURE
+
+fn div(x: u16, y: u16) -> u16 {
+    x / y
+}
+
+fn main() {
+    div(678, 0);
+}

tests/expected/reach/div-zero/reachable_pass/expected

@@ -0,0 +1 @@
+SUCCESS

tests/expected/reach/div-zero/reachable_pass/test.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// divide-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn div(x: u16, y: u16) -> u16 {
+    if y != 0 { x / y } else { 0 }
+}
+
+fn main() {
+    div(11, 3);
+}

tests/expected/reach/div-zero/unreachable/expected

@@ -0,0 +1 @@
+UNREACHABLE

tests/expected/reach/div-zero/unreachable/test.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks
+
+// This test checks that kani injects a reachability check for
+// divide-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is unreachable, so should be reported as UNREACHABLE
+
+fn div(x: u16, y: u16) -> u16 {
+    if y != 0 { x / y } else { 0 }
+}
+
+fn main() {
+    div(5, 0);
+}

tests/expected/reach/overflow-neg/reachable_fail/expected

@@ -0,0 +1,2 @@
+FAILURE
+Failed Checks: attempt to negate with overflow

tests/expected/reach/overflow-neg/reachable_fail/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for negation
+// overflow checks and that it reports ones that are unreachable
+// The negation overflow check in this test is reachable and doesn't hold, so
+// should be reported as FAILURE
+
+fn negate(x: i32) -> i32 {
+    -x
+}
+
+fn main() {
+    negate(std::i32::MIN);
+}

tests/expected/reach/overflow-neg/reachable_pass/expected

@@ -0,0 +1 @@
+SUCCESS

tests/expected/reach/overflow-neg/reachable_pass/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for negation
+// overflow checks and that it reports ones that are unreachable
+// The negation overflow check in this test is reachable, so should be
+// reported as SUCCESS
+
+fn negate(x: i32) -> i32 {
+    if x != std::i32::MIN { -x } else { std::i32::MAX }
+}
+
+fn main() {
+    negate(7532);
+}

tests/expected/reach/overflow-neg/unreachable/expected

@@ -0,0 +1 @@
+UNREACHABLE

tests/expected/reach/overflow-neg/unreachable/test.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for negation
+// overflow checks and that it reports ones that are unreachable
+// The negation overflow check in this test is unreachable, so should be
+// reported as UNREACHABLE
+
+fn negate(x: i32) -> i32 {
+    if x != std::i32::MIN { -x } else { std::i32::MAX }
+}
+
+fn main() {
+    negate(std::i32::MIN);
+}

tests/expected/reach/overflow/reachable_fail/expected

@@ -0,0 +1,2 @@
+FAILURE
+Failed Checks: attempt to subtract with overflow

tests/expected/reach/overflow/reachable_fail/test.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for arithmetic
+// overflow checks and that it reports ones that are unreachable.
+// The arithmetic overflow check in this test is reachable but does not hold, so
+// should be reported as FAILURE
+
+fn cond_reduce(thresh: u32, x: u32) -> u32 {
+    if x > thresh { x - 50 } else { x }
+}
+
+fn main() {
+    cond_reduce(60, 70);
+    cond_reduce(40, 42);
+}

tests/expected/reach/overflow/reachable_pass/expected

@@ -0,0 +1 @@
+SUCCESS

tests/expected/reach/overflow/reachable_pass/test.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for arithmetic
+// overflow checks and that it reports ones that are unreachable.
+// The arithmetic overflow check in this test is reachable, so should be
+// reported as SUCCESS
+
+fn reduce(x: u32) -> u32 {
+    if x > 1000 { x - 1000 } else { x }
+}
+
+fn main() {
+    reduce(7);
+    reduce(33);
+    reduce(728);
+    reduce(1079);
+}

tests/expected/reach/overflow/unreachable/expected

@@ -0,0 +1 @@
+UNREACHABLE

tests/expected/reach/overflow/unreachable/test.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --assertion-reach-checks --output-format regular
+
+// This test checks that kani injects a reachability check for arithmetic
+// overflow checks and that it reports ones that are unreachable
+// The arithmetic overflow check in this test is unreachable, so should be
+// reported as UNREACHABLE
+
+fn reduce(x: u32) -> u32 {
+    if x > 1000 { x - 1000 } else { x }
+}
+
+fn main() {
+    reduce(7);
+    reduce(33);
+    reduce(728);
+}