From ce9ec64685635d713d78c15af7edd27c0a2978d0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Mar 2022 23:05:15 -0700 Subject: [PATCH] A few output improvements (#976) * Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests --- scripts/cbmc_json_parser.py | 26 ++++- scripts/kani-regression.sh | 3 + scripts/test_cbmc_json_parser.py | 106 ++++++++++++++++++ src/cargo-kani/src/args.rs | 5 + src/cargo-kani/src/call_single_file.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/span.rs | 2 +- tests/ui/code-location/expected | 7 ++ tests/ui/code-location/main.rs | 25 +++++ tests/ui/code-location/module/expected | 2 + tests/ui/code-location/module/mod.rs | 16 +++ 10 files changed, 191 insertions(+), 3 deletions(-) create mode 100644 scripts/test_cbmc_json_parser.py create mode 100644 tests/ui/code-location/expected create mode 100644 tests/ui/code-location/main.rs create mode 100644 tests/ui/code-location/module/expected create mode 100644 tests/ui/code-location/module/mod.rs diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index b9ba67703e46..2ba5bfa4c1aa 100755 --- a/scripts/cbmc_json_parser.py +++ b/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: diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index bca61a5bfa2c..2ad7ae03d5af 100755 --- a/scripts/kani-regression.sh +++ b/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 diff --git a/scripts/test_cbmc_json_parser.py b/scripts/test_cbmc_json_parser.py new file mode 100644 index 000000000000..5fd4aba13514 --- /dev/null +++ b/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() diff --git a/src/cargo-kani/src/args.rs b/src/cargo-kani/src/args.rs index f026f1d21f8a..5e9849d8fce0 100644 --- a/src/cargo-kani/src/args.rs +++ b/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! { diff --git a/src/cargo-kani/src/call_single_file.rs b/src/cargo-kani/src/call_single_file.rs index 4c19ed94c342..15dc3c5a04cc 100644 --- a/src/cargo-kani/src/call_single_file.rs +++ b/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()); } diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 2348a0031b60..f5bf992e1122 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/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, diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected new file mode 100644 index 000000000000..78d1e389708f --- /dev/null +++ b/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 as std::ops::Drop>::drop + +VERIFICATION:- SUCCESSFUL + diff --git a/tests/ui/code-location/main.rs b/tests/ui/code-location/main.rs new file mode 100644 index 000000000000..3b5bef4dfe11 --- /dev/null +++ b/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() {} diff --git a/tests/ui/code-location/module/expected b/tests/ui/code-location/module/expected new file mode 100644 index 000000000000..1270084b3357 --- /dev/null +++ b/tests/ui/code-location/module/expected @@ -0,0 +1,2 @@ +VERIFICATION:- SUCCESSFUL + diff --git a/tests/ui/code-location/module/mod.rs b/tests/ui/code-location/module/mod.rs new file mode 100644 index 000000000000..8bc84e565315 --- /dev/null +++ b/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. +}