Remove expression from cbmc check descriptions (rust-lang#906)

* Remove expression from cbmc check descriptions

We have no control over the expression printed. These checks usually
end up printing some temporary variables which are rather confusing. For
now, we replace the message to remove the expressions and make it
 more user friendly.

scripts/cbmc_json_parser.py

@@ -20,9 +20,11 @@
 """
 
 import json
-from colorama import Fore, Style
+import os
 import re
 import sys
+
+from colorama import Fore, Style
 from enum import Enum
 
 # Enum to store the style of output that is given by the argument flags
@@ -206,6 +208,7 @@ def postprocess_results(properties):
     remove_check_ids_from_description(properties)
 
     for property in properties:
+        property["description"] = get_readable_description(property)
         if has_reachable_unsupported_constructs or has_failed_unwinding_asserts:
             # Change SUCCESS to UNDETERMINED for all properties
             if property["status"] == "SUCCESS":
@@ -255,6 +258,142 @@ def filter_properties(properties, message):
             filtered_properties.append(property)
     return filtered_properties, removed_properties
 
+class CProverCheck:
+    """ Represents a CProverCheck and provides methods to replace the check.
+
+        Objects of this class are used to represent specific types of CBMC's
+        check messages. It allow us to identify and to replace them by a more
+        user friendly message.
+
+        That includes rewriting them and removing information that don't
+        make sense in the ust context. E.g.:
+        - Original CBMC message: "dead object in OBJECT_SIZE(&temp_0)"
+                     Not in the original code -> ^^^^^^^^^^^^^^^^^^^^
+        - New message: "pointer to dead object"
+    """
+
+    def __init__(self, msg, new_msg=None):
+        self.original = msg
+        self.kani_msg = new_msg if new_msg else msg
+
+    def matches(self, msg):
+        return self.original in msg
+
+    def replace(self, msg):
+        return self.kani_msg
+
+
+CBMC_DESCRIPTIONS = {
+    "error_label": [],
+    "division-by-zero": [CProverCheck("division by zero")],
+    "enum-range-check": [CProverCheck("enum range check")],
+    "undefined-shift": [CProverCheck("shift distance is negative"),
+                        CProverCheck("shift distance too large"),
+                        CProverCheck("shift operand is negative"),
+                        CProverCheck("shift of non-integer type")],
+    "overflow": [
+        CProverCheck("result of signed mod is not representable"),
+        CProverCheck("arithmetic overflow on signed type conversion"),
+        CProverCheck("arithmetic overflow on signed division"),
+        CProverCheck("arithmetic overflow on signed unary minus"),
+        CProverCheck("arithmetic overflow on signed shl"),
+        CProverCheck("arithmetic overflow on unsigned unary minus"),
+        CProverCheck("arithmetic overflow on signed +", "arithmetic overflow on signed addition"),
+        CProverCheck("arithmetic overflow on signed -", "arithmetic overflow on signed subtraction"),
+        CProverCheck("arithmetic overflow on signed *", "arithmetic overflow on signed multiplication"),
+        CProverCheck("arithmetic overflow on unsigned +", "arithmetic overflow on unsigned addition"),
+        CProverCheck("arithmetic overflow on unsigned -", "arithmetic overflow on unsigned subtraction"),
+        CProverCheck("arithmetic overflow on unsigned *", "arithmetic overflow on unsigned multiplication"),
+        CProverCheck("arithmetic overflow on floating-point typecast"),
+        CProverCheck("arithmetic overflow on floating-point division"),
+        CProverCheck("arithmetic overflow on floating-point addition"),
+        CProverCheck("arithmetic overflow on floating-point subtraction"),
+        CProverCheck("arithmetic overflow on floating-point multiplication"),
+        CProverCheck("arithmetic overflow on unsigned to signed type conversion"),
+        CProverCheck("arithmetic overflow on float to signed integer type conversion"),
+        CProverCheck("arithmetic overflow on signed to unsigned type conversion"),
+        CProverCheck("arithmetic overflow on unsigned to unsigned type conversion"),
+        CProverCheck("arithmetic overflow on float to unsigned integer type conversion")],
+    "NaN": [
+        CProverCheck("NaN on +", "NaN on addition"),
+        CProverCheck("NaN on -", "NaN on subtraction"),
+        CProverCheck("NaN on /", "NaN on division"),
+        CProverCheck("NaN on *", "NaN on multiplication")],
+    "pointer": [
+        CProverCheck("same object violation")],
+    "pointer_arithmetic": [
+        CProverCheck("pointer relation: deallocated dynamic object"),
+        CProverCheck("pointer relation: dead object"),
+        CProverCheck("pointer relation: pointer NULL"),
+        CProverCheck("pointer relation: pointer invalid"),
+        CProverCheck("pointer relation: pointer outside dynamic object bounds"),
+        CProverCheck("pointer relation: pointer outside object bounds"),
+        CProverCheck("pointer relation: invalid integer address"),
+        CProverCheck("pointer arithmetic: deallocated dynamic object"),
+        CProverCheck("pointer arithmetic: dead object"),
+        CProverCheck("pointer arithmetic: pointer NULL"),
+        CProverCheck("pointer arithmetic: pointer invalid"),
+        CProverCheck("pointer arithmetic: pointer outside dynamic object bounds"),
+        CProverCheck("pointer arithmetic: pointer outside object bounds"),
+        CProverCheck("pointer arithmetic: invalid integer address")],
+    "pointer_dereference": [
+        CProverCheck("dereferenced function pointer must be", "dereference failure: invalid function pointer"),
+        CProverCheck("dereference failure: pointer NULL"),
+        CProverCheck("dereference failure: pointer invalid"),
+        CProverCheck("dereference failure: deallocated dynamic object"),
+        CProverCheck("dereference failure: dead object"),
+        CProverCheck("dereference failure: pointer outside dynamic object bounds"),
+        CProverCheck("dereference failure: pointer outside object bounds"),
+        CProverCheck("dereference failure: invalid integer address")],
+    "pointer_primitives": [
+        # These are very hard to understand without more context.
+        CProverCheck("pointer invalid"),
+        CProverCheck("deallocated dynamic object", "pointer to deallocated dynamic object"),
+        CProverCheck("dead object", "pointer to dead object"),
+        CProverCheck("pointer outside dynamic object bounds"),
+        CProverCheck("pointer outside object bounds"),
+        CProverCheck("invalid integer address")
+    ],
+    "array_bounds": [
+        CProverCheck("lower bound", "index out of bounds"),  # Irrelevant check. Only usize allowed as index.
+        # This one is redundant:
+        # CProverCheck("dynamic object upper bound", "access out of bounds"),
+        CProverCheck("upper bound", "index out of bounds: the length is less than or equal to the given index"), ],
+    "bit_count": [
+        CProverCheck("count trailing zeros is undefined for value zero"),
+        CProverCheck("count leading zeros is undefined for value zero")],
+    "memory-leak": [
+        CProverCheck("dynamically allocated memory never freed")],
+    # These pre-conditions should not print temporary variables since they are embedded in the libc implementation.
+    # They are added via __CPROVER_precondition.
+    # "precondition_instance": [],
+}
+
+def get_readable_description(prop):
+    """This function will return a user friendly property description.
+
+       For CBMC checks, it will ensure that the failure does not include any
+       temporary variable.
+    """
+    original = prop["description"]
+    # Id is structured as [<function>.]<property_class>.<counter>
+    prop_class = prop["property"].rsplit(".", 3)
+    # Do nothing if prop_class is diff than cbmc's convention
+    class_id = prop_class[-2] if len(prop_class) > 1 else None
+    if class_id in CBMC_DESCRIPTIONS:
+        # Contains a list for potential message translation [String].
+        prop_type = [check.replace(original) for check in CBMC_DESCRIPTIONS[class_id] if check.matches(original)]
+        if len(prop_type) != 1:
+            if "KANI_FAIL_ON_UNEXPECTED_DESCRIPTION" in os.environ:
+                print(f"Unexpected description: {original}\n"
+                      f"  - class_id: {class_id}\n"
+                      f"  - matches: {prop_type}\n")
+                exit(1)
+            else:
+                return original
+        else:
+            return prop_type[0]
+    return original
 
 def annotate_properties_with_reach_results(properties, reach_checks):
     """

scripts/kani-regression.sh

@@ -13,6 +13,11 @@ export PATH=$SCRIPT_DIR:$PATH
 EXTRA_X_PY_BUILD_ARGS="${EXTRA_X_PY_BUILD_ARGS:-}"
 KANI_DIR=$SCRIPT_DIR/..
 
+# This variable forces an error when there is a mismatch on the expected
+# descriptions from cbmc checks.
+# TODO: We should add a more robust mechanism to detect python unexpected behavior.
+export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
+
 # Required dependencies
 check-cbmc-version.py --major 5 --minor 50
 check-cbmc-viewer-version.py --major 2 --minor 10

tests/cargo-kani/output-format/main.expected

@@ -1,2 +1,2 @@
 Description: "assertion failed: 1 + 1 == 2"
-Description: "dead object in OBJECT_SIZE(&temp_0)"
+Description: "pointer to dead object"

tests/expected/array/expected

@@ -1,14 +1,4 @@
 SUCCESS\
-array 'y'.0 upper bound in y.0[var_8]
-SUCCESS\
-array 'y'.0 upper bound in y.0[var_12]
-FAILURE\
-array 'y'.0 upper bound in y.0[var_16]
-SUCCESS\
-array 'x'.0 upper bound in x.0[var_3]
-SUCCESS\
-array 'x'.0 upper bound in x.0[var_5]
-SUCCESS\
 assertion failed: y[0] == 1
 SUCCESS\
 assertion failed: y[1] == 2

tests/ui/cbmc_checks/float-overflow/check_message.rs

@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check we don't print temporary variables as part of CBMC messages.
+extern crate kani;
+
+use kani::any;
+
+// Use the result so rustc doesn't optimize them away.
+fn dummy(result: f32) -> f32 {
+    result.round()
+}
+
+#[kani::proof]
+fn main() {
+    dummy(any::<f32>() + any::<f32>());
+    dummy(any::<f32>() - any::<f32>());
+    dummy(any::<f32>() * any::<f32>());
+    dummy(any::<f32>() / any::<f32>()); // This is not emitting CBMC check.
+    dummy(any::<f32>() % any::<f32>()); // This is not emitting CBMC check.
+    dummy(-any::<f32>()); // This is not emitting CBMC check.
+}
+

tests/ui/cbmc_checks/float-overflow/expected

@@ -0,0 +1,9 @@
+Failed Checks: NaN on addition
+Failed Checks: arithmetic overflow on floating-point addition
+Failed Checks: NaN on subtraction
+Failed Checks: arithmetic overflow on floating-point subtraction
+Failed Checks: NaN on multiplication
+Failed Checks: arithmetic overflow on floating-point multiplication
+Failed Checks: NaN on division
+Failed Checks: arithmetic overflow on floating-point division
+Failed Checks: division by zero

tests/ui/cbmc_checks/pointer/check_message.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check we don't print temporary variables as part of CBMC messages.
+
+fn not_zero(p1: *const i32) {
+    assert!(unsafe { *p1 != 0 });
+}
+
+#[kani::proof]
+fn main() {
+    let mut ptr = 10 as *const i32;
+    if kani::any() {
+        let var1 = 0;
+        ptr = &var1 as *const i32;
+    }
+    not_zero(ptr);
+}
+

tests/ui/cbmc_checks/pointer/expected

@@ -0,0 +1,5 @@
+Failed Checks: dereference failure: pointer NULL
+Failed Checks: dereference failure: deallocated dynamic object
+Failed Checks: dereference failure: dead object
+Failed Checks: dereference failure: pointer outside object bounds
+Failed Checks: dereference failure: invalid integer address

tests/ui/cbmc_checks/signed-overflow/check_message.rs

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check we don't print temporary variables as part of CBMC messages.
+// cbmc-flags: --signed-overflow-check
+extern crate kani;
+
+use kani::any;
+
+// Ensure rustc encodes the operation.
+fn dummy(var: i32) {
+    kani::assume(var != 0);
+}
+
+
+#[kani::proof]
+fn main() {
+    dummy(any::<i32>() + any::<i32>());
+    dummy(any::<i32>() - any::<i32>());
+    dummy(any::<i32>() * any::<i32>());
+    dummy(any::<i32>() / any::<i32>()); // This is not emitting CBMC check.
+    dummy(any::<i32>() % any::<i32>()); // This is not emitting CBMC check.
+    dummy(any::<i32>() << any::<i32>());
+    dummy(any::<i32>() >> any::<i32>());
+    dummy(-any::<i32>()); // This is not emitting CBMC check.
+}
+

tests/ui/cbmc_checks/signed-overflow/expected

@@ -0,0 +1,14 @@
+Failed Checks: arithmetic overflow on signed addition
+Failed Checks: arithmetic overflow on signed subtraction
+Failed Checks: arithmetic overflow on signed multiplication
+Failed Checks: division by zero
+Failed Checks: arithmetic overflow on signed division
+Failed Checks: division by zero
+Failed Checks: result of signed mod is not representable
+Failed Checks: shift distance is negative
+Failed Checks: shift distance too large
+Failed Checks: shift operand is negative
+Failed Checks: arithmetic overflow on signed shl
+Failed Checks: shift distance is negative
+Failed Checks: shift distance too large
+Failed Checks: arithmetic overflow on signed unary minus

tests/ui/cbmc_checks/unsigned-overflow/check_message.rs

@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check we don't print temporary variables as part of CBMC messages.
+// cbmc-flags: --unsigned-overflow-check
+extern crate kani;
+
+use kani::any;
+
+// Ensure rustc encodes the operation.
+fn dummy(var: u32) {
+    kani::assume(var != 0);
+}
+
+#[kani::proof]
+fn main() {
+    dummy(any::<u32>() + any::<u32>());
+    dummy(any::<u32>() - any::<u32>());
+    dummy(any::<u32>() * any::<u32>());
+    dummy(any::<u32>() / any::<u32>());
+    dummy(any::<u32>() % any::<u32>());
+    dummy(any::<u32>() << any::<u32>());
+    dummy(any::<u32>() >> any::<u32>());
+}
+

tests/ui/cbmc_checks/unsigned-overflow/expected

@@ -0,0 +1,7 @@
+Failed Checks: arithmetic overflow on unsigned addition
+Failed Checks: arithmetic overflow on unsigned subtraction
+Failed Checks: arithmetic overflow on unsigned multiplication
+Failed Checks: division by zero
+Failed Checks: division by zero
+Failed Checks: shift distance too large
+Failed Checks: shift distance too large

tests/ui/regular-output-format-fail/expected

@@ -1,4 +1,4 @@
 Check 1: main.assertion.1
 Description: "assertion failed: 1 + 1 == 3"
-Description: "dead object in OBJECT_SIZE(&temp_0)"
-Failed Checks: assertion failed: 1 + 1 == 3
+Description: "pointer to dead object"
+Failed Checks: assertion failed: 1 + 1 == 3

tests/ui/regular-output-format-pass/expected

@@ -1,3 +1,3 @@
 Check 1: main.assertion.1
 Description: "assertion failed: 1 + 1 == 2"
-Description: "dead object in OBJECT_SIZE(&temp_0)"
+Description: "pointer to dead object"