From 7bdbba21b686c2195e7f7027cd5a32964eae03f3 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 22 Mar 2022 16:51:21 -0700 Subject: [PATCH 1/8] Disable reach assertions in visualize mode --- src/cargo-kani/src/args.rs | 5 +++++ src/cargo-kani/src/call_single_file.rs | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) 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()); } From 5c3a8b47abcd7eab263ff66837cdd552611eb154 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 22 Mar 2022 17:06:40 -0700 Subject: [PATCH 2/8] Make file location relative to current dir. Should we make it relative to the project dir instead?? --- scripts/cbmc_json_parser.py | 28 ++++++++++++++++++- .../src/codegen_cprover_gotoc/codegen/span.rs | 2 +- 2 files changed, 28 insertions(+), 2 deletions(-) diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index b9ba67703e46..72fafc6aac4d 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,34 @@ 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 + + if not path.exists(self.filename): + # I'm not sure this can happen today, but keep it here for future + # proofing. + return self.filename + + cwd = os.getcwd() + if path.commonpath([self.filename, cwd]) == cwd: + return path.relpath(self.filename) + + home_path = path.expanduser("~") + if path.commonpath([self.filename, home_path]) == home_path: + return "~/{}".format(path.relpath(self.filename, 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/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, From 9ab8d902a4c66b2b5746e36f5ef9dabfc45a22a9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 23 Mar 2022 14:59:37 -0700 Subject: [PATCH 3/8] Add test for this. Unfortunately, the output changes depending on the directory where the regression is running from, so we cannot check that logic. --- 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 ++++++++++++++++ 4 files changed, 50 insertions(+) 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/tests/ui/code-location/expected b/tests/ui/code-location/expected new file mode 100644 index 000000000000..f3c69a174ded --- /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 +~/.rustup/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. +} From 157695a56199c4d0bbb2e94fed1d394d4deb53a4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 23 Mar 2022 16:05:07 -0700 Subject: [PATCH 4/8] Fix regression --- scripts/cbmc_json_parser.py | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index 72fafc6aac4d..31ecf4a546a9 100755 --- a/scripts/cbmc_json_parser.py +++ b/scripts/cbmc_json_parser.py @@ -111,13 +111,16 @@ def filepath(self): # proofing. return self.filename + # 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([self.filename, cwd]) == cwd: - return path.relpath(self.filename) + if path.commonpath([full_path, cwd]) == cwd: + return path.relpath(full_path) home_path = path.expanduser("~") - if path.commonpath([self.filename, home_path]) == home_path: - return "~/{}".format(path.relpath(self.filename, home_path)) + if path.commonpath([full_path, home_path]) == home_path: + return "~/{}".format(path.relpath(full_path, home_path)) return self.filename From 25bca149cdbce21368d6ca6494cdcf2c3b35e31b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Mar 2022 15:02:55 -0700 Subject: [PATCH 5/8] Remove check if file exists and added unit tests --- scripts/cbmc_json_parser.py | 5 -- scripts/kani-regression.sh | 3 ++ scripts/test_parser.py | 102 ++++++++++++++++++++++++++++++++++++ 3 files changed, 105 insertions(+), 5 deletions(-) create mode 100644 scripts/test_parser.py diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index 31ecf4a546a9..2ba5bfa4c1aa 100755 --- a/scripts/cbmc_json_parser.py +++ b/scripts/cbmc_json_parser.py @@ -106,11 +106,6 @@ def filepath(self): if not self.filename: return None - if not path.exists(self.filename): - # I'm not sure this can happen today, but keep it here for future - # proofing. - return self.filename - # Reference to C files use relative paths, while rust uses absolute. # Normalize both to be absolute first. full_path = path.abspath(self.filename) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index bca61a5bfa2c..4147b6ef93f6 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_parser.py + # Build all packages in the workspace cargo build diff --git a/scripts/test_parser.py b/scripts/test_parser.py new file mode 100644 index 000000000000..41ef6b8b105f --- /dev/null +++ b/scripts/test_parser.py @@ -0,0 +1,102 @@ +# 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""" + path = tempfile.gettempdir() + json = source_json(path) + src_loc = SourceLocation(json) + self.assertEqual(src_loc.filepath(), path) + + 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() From 8202abac945ce3ae6ff4d6e40d3634f84ea4c844 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Mar 2022 15:08:15 -0700 Subject: [PATCH 6/8] Update expected file --- tests/ui/code-location/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index f3c69a174ded..78d1e389708f 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -1,6 +1,6 @@ module/mod.rs:10:5 in function module::not_empty main.rs:13:5 in function same_file -~/.rustup/toolchains +/toolchains/ alloc/src/vec/mod.rs:2821:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL From 0a00fe2a15ffc6ed795318aed5221f0be45601af Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Mar 2022 15:24:49 -0700 Subject: [PATCH 7/8] Making one test more reliable --- scripts/test_parser.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/scripts/test_parser.py b/scripts/test_parser.py index 41ef6b8b105f..5fd4aba13514 100644 --- a/scripts/test_parser.py +++ b/scripts/test_parser.py @@ -23,11 +23,15 @@ class SourceLocationTest(unittest.TestCase): """ Unit tests for SourceLocation """ def test_source_location_valid_path(self): - """Path returned by filepath() works for valid paths""" + """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) - self.assertEqual(src_loc.filepath(), path) + 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""" From e6c52de5050f803fa818ee867a2f3d149828ffd2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Mar 2022 15:46:56 -0700 Subject: [PATCH 8/8] Rename test script --- scripts/kani-regression.sh | 2 +- scripts/{test_parser.py => test_cbmc_json_parser.py} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename scripts/{test_parser.py => test_cbmc_json_parser.py} (100%) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 4147b6ef93f6..2ad7ae03d5af 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -26,7 +26,7 @@ check-cbmc-viewer-version.py --major 2 --minor 10 ${SCRIPT_DIR}/kani-fmt.sh --check # Parser tests -PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_parser.py +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_parser.py b/scripts/test_cbmc_json_parser.py similarity index 100% rename from scripts/test_parser.py rename to scripts/test_cbmc_json_parser.py