A few output improvements (model-checking#976)

* Disable reach assertions in visualize mode
* Make file location relative to current dir
* Add unit tests

scripts/cbmc_json_parser.py

@@ -26,6 +26,7 @@
 
 from colorama import Fore, Style
 from enum import Enum
+from os import path
 
 # Enum to store the style of output that is given by the argument flags
 output_style_switcher = {
@@ -95,9 +96,32 @@ def __init__(self, source_location={}):
         self.column = source_location.get("column", None)
         self.line = source_location.get("line", None)
 
+    def filepath(self):
+        """ Return a more user friendly path.
+
+        - If the path is inside the current directory, return a relative path.
+        - If not but the path is in the ${HOME} directory, return relative to ${HOME}
+        - Otherwise, return the path as is.
+        """
+        if not self.filename:
+            return None
+
+        # Reference to C files use relative paths, while rust uses absolute.
+        # Normalize both to be absolute first.
+        full_path = path.abspath(self.filename)
+        cwd = os.getcwd()
+        if path.commonpath([full_path, cwd]) == cwd:
+            return path.relpath(full_path)
+
+        home_path = path.expanduser("~")
+        if path.commonpath([full_path, home_path]) == home_path:
+            return "~/{}".format(path.relpath(full_path, home_path))
+
+        return self.filename
+
     def __str__(self):
         if self.filename:
-            s = f"{self.filename}"
+            s = f"{self.filepath()}"
             if self.line:
                 s += f":{self.line}"
                 if self.column:

scripts/kani-regression.sh

@@ -25,6 +25,9 @@ check-cbmc-viewer-version.py --major 2 --minor 10
 # Formatting check
 ${SCRIPT_DIR}/kani-fmt.sh --check
 
+# Parser tests
+PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_cbmc_json_parser.py
+
 # Build all packages in the workspace
 cargo build
 

scripts/test_cbmc_json_parser.py

@@ -0,0 +1,106 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+import unittest
+import os
+import tempfile
+from cbmc_json_parser import SourceLocation
+
+
+def source_json(filename=None, function=None, line=None, column=None):
+    result = dict()
+    if filename:
+        result["file"] = filename
+    if function:
+        result["function"] = function
+    if column:
+        result["column"] = column
+    if line:
+        result["line"] = line
+    return result
+
+
+class SourceLocationTest(unittest.TestCase):
+    """ Unit tests for SourceLocation """
+
+    def test_source_location_valid_path(self):
+        """Path returned by filepath() works for valid paths
+
+            Note: Check is loose because I couldn't find a reliable way to control a real path location.
+        """
+        path = tempfile.gettempdir()
+        json = source_json(path)
+        src_loc = SourceLocation(json)
+        possible_output = {path, os.path.relpath(path), os.path.relpath(path, os.path.expanduser("~"))}
+        self.assertIn(src_loc.filepath(), possible_output)
+
+    def test_source_location_invalid_path(self):
+        """Path returned by filepath() returns the input path if it doesn't exist"""
+        path = "/rust/made/up/path/lib.rs"
+        json = source_json(path)
+        src_loc = SourceLocation(json)
+        self.assertEqual(src_loc.filepath(), path)
+
+    def test_source_location_relative_path(self):
+        """Path returned by filepath() is relative if the input is also relative"""
+        relpath = "dummy/target.rs"
+        json = source_json(relpath)
+        src_loc = SourceLocation(json)
+        self.assertEqual(src_loc.filepath(), relpath)
+
+    def test_source_location_absolute_cwd_path(self):
+        """Path returned by filepath() is relative to current directory
+
+            Note that the file may not exist that this should still hold.
+        """
+        relpath = "dummy/target.rs"
+        path = os.path.join(os.getcwd(), relpath)
+        self.assertNotEqual(relpath, path)
+
+        json = source_json(path)
+        src_loc = SourceLocation(json)
+        self.assertEqual(src_loc.filepath(), relpath)
+
+    def test_source_location_absolute_user_path(self):
+        """Path returned by filepath() is relative to current directory
+
+            Note that the file may not exist that this should still hold.
+        """
+        relpath = "~/dummy/target.rs"
+        path = os.path.expanduser(relpath)
+        self.assertNotEqual(relpath, path)
+
+        json = source_json(path)
+        src_loc = SourceLocation(json)
+        self.assertEqual(src_loc.filepath(), relpath)
+
+    def test_source_location_relative_user_path(self):
+        """Path returned by filepath() is relative to current directory
+
+            Note that the file may not exist that this should still hold.
+        """
+        relpath = "~/dummy/target.rs"
+        json = source_json(relpath)
+        src_loc = SourceLocation(json)
+        self.assertEqual(src_loc.filepath(), relpath)
+
+    def test_source_location_with_no_path(self):
+        """Function filepath() is None if no file is given in the input"""
+        json = source_json(function="main")
+        src_loc = SourceLocation(json)
+        self.assertIsNone(src_loc.filepath())
+
+    def test_source_location_output_format(self):
+        """Check that output includes all the information provided"""
+        path = "/rust/made/up/path/lib.rs"
+        function = "harness"
+        line = 10
+        column = 8
+        json = source_json(path, function, line, column)
+        src_loc = str(SourceLocation(json))
+        self.assertIn(path, src_loc)
+        self.assertIn(f"{path}:{line}:{column}", src_loc)
+        self.assertIn(function, src_loc)
+
+
+if __name__ == '__main__':
+    unittest.main()

src/cargo-kani/src/args.rs

@@ -142,6 +142,11 @@ impl KaniArgs {
         self.restrict_vtable
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
+
+    pub fn assertion_reach_checks(&self) -> bool {
+        // Turn them off when visualizing an error trace.
+        !self.no_assertion_reach_checks && !self.visualize
+    }
 }
 
 arg_enum! {

src/cargo-kani/src/call_single_file.rs

@@ -107,7 +107,7 @@ impl KaniSession {
         if self.args.restrict_vtable() {
             flags.push("--restrict-vtable-fn-ptrs".into());
         }
-        if !self.args.no_assertion_reach_checks {
+        if self.args.assertion_reach_checks() {
             flags.push("--assertion-reach-checks".into());
         }
 

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

@@ -14,7 +14,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let lo = smap.lookup_char_pos(sp.lo());
         let line = lo.line;
         let col = 1 + lo.col_display;
-        let filename0 = lo.file.name.prefer_remapped().to_string_lossy().to_string();
+        let filename0 = lo.file.name.prefer_local().to_string_lossy().to_string();
         let filename1 = match std::fs::canonicalize(filename0.clone()) {
             Ok(pathbuf) => pathbuf.to_str().unwrap().to_string(),
             Err(_) => filename0,

tests/ui/code-location/expected

@@ -0,0 +1,7 @@
+module/mod.rs:10:5 in function module::not_empty
+main.rs:13:5 in function same_file
+/toolchains/
+alloc/src/vec/mod.rs:2821:81 in function <std::vec::Vec<T, A> as std::ops::Drop>::drop
+
+VERIFICATION:- SUCCESSFUL
+

tests/ui/code-location/main.rs

@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --function harness
+//
+//! This test is to check how file names are displayed in the Kani output.
+
+mod module;
+
+use module::not_empty;
+
+fn same_file(cond: bool) {
+    assert!(cond);
+}
+
+#[kani::proof]
+fn harness() {
+    let x = true;
+    same_file(x);
+
+    let v = vec![1];
+    not_empty(&v);
+}
+
+fn main() {}

tests/ui/code-location/module/expected

@@ -0,0 +1,2 @@
+VERIFICATION:- SUCCESSFUL
+

tests/ui/code-location/module/mod.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: --function empty_harness
+
+// This file is to be used as a module on a different test, but the compiletest will still run
+// kani on this file. Use an empty harness instead.
+
+pub fn not_empty(v: &[i32]) {
+    assert!(!v.is_empty());
+}
+
+#[kani::proof]
+fn empty_harness() {
+    // No-op to overcome compile test.
+}