Check for exact match of reachability check ID (rust-lang#1093)

Author: zhassan-aws

scripts/cbmc_json_parser.py

@@ -50,6 +50,7 @@ class GlobalMessages(str, Enum):
     REACH_CHECK_DESC = "[KANI_REACHABILITY_CHECK]"
     REACH_CHECK_KEY = "reachCheckResult"
     CHECK_ID = "KANI_CHECK_ID"
+    CHECK_ID_RE = CHECK_ID + r"_.*_([0-9])*"
     UNSUPPORTED_CONSTRUCT_DESC = "is not currently supported by Kani"
     UNWINDING_ASSERT_DESC = "unwinding assertion loop"
 
@@ -300,7 +301,9 @@ def postprocess_results(properties, extra_ptr_check):
                 property["status"] = "UNDETERMINED"
         elif GlobalMessages.REACH_CHECK_KEY in property and property[GlobalMessages.REACH_CHECK_KEY] == "SUCCESS":
             # Change SUCCESS to UNREACHABLE
-            assert property["status"] == "SUCCESS", "** ERROR: Expecting an unreachable property to have a status of \"SUCCESS\""
+            description = property["description"]
+            assert property[
+                "status"] == "SUCCESS", f"** ERROR: Expecting the unreachable property \"{description}\" to have a status of \"SUCCESS\""
             property["status"] = "UNREACHABLE"
 
     messages = ""
@@ -517,7 +520,7 @@ def annotate_properties_with_reach_results(properties, reach_checks):
     for reach_check in reach_checks:
         description = reach_check["description"]
         # Extract the ID of the assert from the description
-        match_obj = re.search(GlobalMessages.CHECK_ID + r"_.*_([0-9])*", description)
+        match_obj = re.search(GlobalMessages.CHECK_ID_RE, description)
         if not match_obj:
             raise Exception("Error: failed to extract check ID for reachability check \"" + description + "\"")
         check_id = match_obj.group(0)
@@ -531,8 +534,13 @@ def get_matching_property(properties, check_id):
     Find the property with the given ID
     """
     for property in properties:
-        if check_id in property["description"]:
-            return property
+        description = property["description"]
+        match_obj = re.search("\\[" + GlobalMessages.CHECK_ID_RE + "\\]", description)
+        # Currently, not all properties have a check ID
+        if match_obj:
+            prop_check_id = match_obj.group(0)
+            if prop_check_id == "[" + check_id + "]":
+                return property
     raise Exception("Error: failed to find a property with ID \"" + check_id + "\"")
 
 
@@ -551,7 +559,7 @@ def remove_check_ids_from_description(properties):
     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]*\] ")
+    check_id_pattern = re.compile(r"\[" + GlobalMessages.CHECK_ID_RE + r"\] ")
     for property in properties:
         property["description"] = re.sub(check_id_pattern, "", property["description"])
 

tests/expected/reach/check_id/expected

@@ -0,0 +1,10 @@
+Status: FAILURE\
+Description: "assertion failed: 3 + 3 == 5"
+
+Status: UNREACHABLE\
+Description: "assertion failed: 2 + 2 == 4"
+
+Status: SUCCESS\
+Description: "assertion failed: 1 + 1 == 2"
+
+VERIFICATION:- FAILED

tests/expected/reach/check_id/main.rs

@@ -0,0 +1,30 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test has more than 10 asserts to satisfy the condition that two check
+// IDs are a prefix of each other, e.g.:
+//     KANI_CHECK_ID_reach_check.225019a5::reach_check_1
+//     KANI_CHECK_ID_reach_check.225019a5::reach_check_10
+
+fn foo(x: i32) {
+    assert!(1 + 1 == 2);
+    if x < 9 {
+        // unreachable
+        assert!(2 + 2 == 4);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    assert!(1 + 1 == 2);
+    let x = if kani::any() { 33 } else { 57 };
+    foo(x);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(3 + 3 == 5);
+}