From c9e3f78cafd50ec0bf98ac4d313d79644b191006 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 24 Jun 2021 16:59:51 +0000 Subject: [PATCH 01/10] Use `--unwinding-assertions` flag by default --- scripts/cargo-rmc | 5 +++ scripts/rmc | 5 +++ scripts/rmc.py | 12 ++++++ src/test/cbmc/LoopLoop_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 40 +++++++++++++++++++ src/test/cbmc/LoopWhile_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 37 +++++++++++++++++ src/test/cbmc/Slice/main.rs | 2 +- src/test/cbmc/SwitchInt/main.rs | 2 +- src/test/cbmc/Whitespace/main.rs | 2 +- src/test/prusti/Binary_search_fail.rs | 2 +- src/test/smack/loops/gauss_sum_nondet.rs | 2 +- src/test/smack/loops/gauss_sum_nondet_fail.rs | 2 +- src/test/smack/loops/iterator.rs | 2 +- src/test/smack/loops/iterator_fail.rs | 2 +- 15 files changed, 109 insertions(+), 10 deletions(-) create mode 100644 src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs create mode 100644 src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 501b4052203e..3fc6673012d6 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -31,6 +31,7 @@ def main(): parser.add_argument("--wkdir", default=".") parser.add_argument("--function", default="main") parser.add_argument("crate", help="crate to verify") + parser.add_argument("--no-default-flags", action="store_true") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -41,6 +42,10 @@ def main(): if not rmc.dependencies_in_path(): return 1 + # Add a set of CBMC arguments by default unless `--no-default-args` is being used + if not args.no_default_flags: + rmc.add_default_cbmc_flags(args) + rmc.cargo_build(args.crate, args.target_dir, args.verbose, args.debug, args.mangler) diff --git a/scripts/rmc b/scripts/rmc index 8f6fb137beb7..52da270ad470 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -27,6 +27,7 @@ def main(): parser.add_argument("--visualize", action="store_true") parser.add_argument("--srcdir", default=".") parser.add_argument("--wkdir", default=".") + parser.add_argument("--no-default-flags", action="store_true") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -41,6 +42,10 @@ def main(): if not rmc.dependencies_in_path(): return 1 + + # Add a set of CBMC arguments by default unless `--no-default-args` is being used + if not args.no_default_flags: + rmc.add_default_cbmc_flags(args) base, ext = os.path.splitext(args.input) if ext != ".rs": diff --git a/scripts/rmc.py b/scripts/rmc.py index 95fd31725a98..ff335916febd 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -11,6 +11,7 @@ RMC_RUSTC_EXE = "rmc-rustc" EXIT_CODE_SUCCESS = 0 +DEFAULT_CBMC_FLAGS = ["--unwinding-assertions"] def is_exe(name): from shutil import which @@ -31,6 +32,17 @@ def delete_file(filename): except OSError: pass +# Add a set of default CBMC arguments +def add_default_cbmc_flags(args): + if not args.no_default_flags: + # We print a warning if the user has specified one of the default flags + # Otherwise we append the default flags to CBMC arguments + for arg in DEFAULT_CBMC_FLAGS: + # This behavior must be reviewed if the set of default flags is extended + if arg in args.cbmc_args: + print("WARNING: Default CBMC argument `{}` not added (already specified)".format(arg)) + else: + args.cbmc_args.append(arg) def add_rmc_rustc_debug_to_env(env): env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_llvm::gotoc") diff --git a/src/test/cbmc/LoopLoop_NonReturning/main.rs b/src/test/cbmc/LoopLoop_NonReturning/main.rs index 9e88fe1c4b50..f3f24ec4e71f 100644 --- a/src/test/cbmc/LoopLoop_NonReturning/main.rs +++ b/src/test/cbmc/LoopLoop_NonReturning/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 10 --unwinding-assertions +// cbmc-flags: --unwind 10 include!("../../rmc-prelude.rs"); diff --git a/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs new file mode 100644 index 000000000000..9a22b2d33527 --- /dev/null +++ b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -0,0 +1,40 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-default-flags +// cbmc-flags: --unwind 9 + +include!("../../rmc-prelude.rs"); + +// This example tests the RMC flag `--no-default-flags` +// +// It is the same as `main.rs` except for the flags passed to RMC and CBMC +// Running it with `--unwind 10` is not enough to unwind the loop +// and generates this verification output: +// +// [main.unwind.0] line 30 unwinding assertion loop 0: FAILURE +// [main.assertion.1] line 38 assertion failed: a == 0: SUCCESS +// ** 1 of 2 failed (2 iterations) +// VERIFICATION FAILED +// +// But with `--no-default-flags` we will avoid introducing a unwinding assertion: +// +// [main.assertion.1] line 38 assertion failed: a == 0: SUCCESS +// +// ** 0 of 1 failed (1 iterations) +// VERIFICATION SUCCESSFUL +fn main() { + let mut a: u32 = __nondet(); + + if a < 1024 { + loop { + a = a / 2; + + if a == 0 { + break; + } + } + + assert!(a == 0); + } +} diff --git a/src/test/cbmc/LoopWhile_NonReturning/main.rs b/src/test/cbmc/LoopWhile_NonReturning/main.rs index 48aeb4c8ef30..17c634651615 100644 --- a/src/test/cbmc/LoopWhile_NonReturning/main.rs +++ b/src/test/cbmc/LoopWhile_NonReturning/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 11 --unwinding-assertions +// cbmc-flags: --unwind 11 include!("../../rmc-prelude.rs"); diff --git a/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs new file mode 100644 index 000000000000..3117068f1a8e --- /dev/null +++ b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -0,0 +1,37 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-default-flags +// cbmc-flags: --unwind 10 + +include!("../../rmc-prelude.rs"); + +// This example tests the RMC flag `--no-default-flags` +// +// It is the same as `main.rs` except for the flags passed to RMC and CBMC +// Running it with `--unwind 10` is not enough to unwind the loop +// and generates this verification output: +// +// [main.unwind.0] line 30 unwinding assertion loop 0: FAILURE +// [main.assertion.1] line 34 assertion failed: a == 0: SUCCESS +// +// ** 1 of 2 failed (2 iterations) +// VERIFICATION FAILED +// +// But with `--no-default-flags` we will avoid introducing a unwinding assertion: +// +// [main.assertion.1] line 34 assertion failed: a == 0: SUCCESS +// +// ** 0 of 1 failed (1 iterations) +// VERIFICATION SUCCESSFUL +fn main() { + let mut a: u32 = __nondet(); + + if a < 1024 { + while a > 0 { + a = a / 2; + } + + assert!(a == 0); + } +} diff --git a/src/test/cbmc/Slice/main.rs b/src/test/cbmc/Slice/main.rs index 419493b77b57..eaf911150ec1 100644 --- a/src/test/cbmc/Slice/main.rs +++ b/src/test/cbmc/Slice/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 6 --unwinding-assertions +// cbmc-flags: --unwind 6 fn main() { let name: &str = "hello"; diff --git a/src/test/cbmc/SwitchInt/main.rs b/src/test/cbmc/SwitchInt/main.rs index b16413d70175..7c99721c9f40 100644 --- a/src/test/cbmc/SwitchInt/main.rs +++ b/src/test/cbmc/SwitchInt/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwind 2 fn doswitch_int() -> i32 { for i in [99].iter() { diff --git a/src/test/cbmc/Whitespace/main.rs b/src/test/cbmc/Whitespace/main.rs index b602f93ad621..0faa4516797f 100644 --- a/src/test/cbmc/Whitespace/main.rs +++ b/src/test/cbmc/Whitespace/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 2 --unwinding-assertions +// cbmc-flags: --unwind 2 fn main() { let mut iter = "A few words".split_whitespace(); diff --git a/src/test/prusti/Binary_search_fail.rs b/src/test/prusti/Binary_search_fail.rs index 1aaa60f36767..40223377b0ac 100644 --- a/src/test/prusti/Binary_search_fail.rs +++ b/src/test/prusti/Binary_search_fail.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// cbmc-flags: --unwind 4 --unwinding-assertions +// cbmc-flags: --unwind 4 use std::cmp::Ordering::*; diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs index 7f4c999a4bfc..33c70312017f 100644 --- a/src/test/smack/loops/gauss_sum_nondet.rs +++ b/src/test/smack/loops/gauss_sum_nondet.rs @@ -3,7 +3,7 @@ // @flag --no-memory-splitting --unroll=4 // @expect verified -// cbmc-flags: --unwind 5 --unwinding-assertions +// cbmc-flags: --unwind 5 include!("../../rmc-prelude.rs"); diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs index b1d96e29a762..d29f31dc2d50 100644 --- a/src/test/smack/loops/gauss_sum_nondet_fail.rs +++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs @@ -3,7 +3,7 @@ // @flag --no-memory-splitting --unroll=10 // @expect error -// cbmc-flags: --unwind 5 --unwinding-assertions +// cbmc-flags: --unwind 5 include!("../../rmc-prelude.rs"); diff --git a/src/test/smack/loops/iterator.rs b/src/test/smack/loops/iterator.rs index 8081798312cb..7d810fe79e03 100644 --- a/src/test/smack/loops/iterator.rs +++ b/src/test/smack/loops/iterator.rs @@ -3,7 +3,7 @@ // @flag --no-memory-splitting --unroll=4 // @expect verified -// cbmc-flags: --unwind 5 --unwinding-assertions +// cbmc-flags: --unwind 5 fn fac(n: u64) -> u64 { match n { diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs index 051dd8b3581f..72fca0cf5134 100644 --- a/src/test/smack/loops/iterator_fail.rs +++ b/src/test/smack/loops/iterator_fail.rs @@ -3,7 +3,7 @@ // @flag --no-memory-splitting --unroll=10 // @expect error -// cbmc-flags: --unwind 5 --unwinding-assertions +// cbmc-flags: --unwind 5 fn fac(n: u64) -> u64 { match n { From f9ac00800e6ce59c22dad160fefd7692021251d9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 25 Jun 2021 14:01:38 +0000 Subject: [PATCH 02/10] Scan CBMC output and make recommendations (unwinding) --- scripts/rmc.py | 39 ++++++++++++++++++++++++--- src/test/expected/unwind_tip/expected | 2 ++ src/test/expected/unwind_tip/main.rs | 29 ++++++++++++++++++++ 3 files changed, 66 insertions(+), 4 deletions(-) create mode 100644 src/test/expected/unwind_tip/expected create mode 100644 src/test/expected/unwind_tip/main.rs diff --git a/scripts/rmc.py b/scripts/rmc.py index ff335916febd..1462a114aa15 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -5,6 +5,7 @@ import atexit import os import os.path +import re RMC_CFG = "rmc" @@ -13,6 +14,21 @@ DEFAULT_CBMC_FLAGS = ["--unwinding-assertions"] +# A Scanner is intended to match a pattern with an output +# and edit the output based on an edit function +class Scanner: + def __init__(self, pattern, edit_fun): + self.pattern = re.compile(pattern) + self.edit_fun = edit_fun + + # Returns whether the scanner's pattern matches some text + def match(self, text): + return self.pattern.search(text) != None + + # Returns an edited output based on the scanner's edit function + def edit_output(self, text): + return self.edit_fun(text) + def is_exe(name): from shutil import which return which(name) is not None @@ -56,7 +72,7 @@ def print_rmc_step_status(step_name, completed_process, verbose=False): print(f"[RMC] stage: {step_name} ({status})") print(f"[RMC] cmd: {' '.join(completed_process.args)}") -def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False): +def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[]): process = subprocess.run( cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, env=env, cwd=cwd) @@ -65,14 +81,19 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve if label != None: print_rmc_step_status(label, process, verbose) + stdout = process.stdout + for scanner in scanners: + if scanner.match(stdout): + stdout = scanner.edit_output(stdout) + # Write to stdout if specified, or if failure, or verbose or debug if (output_to == "stdout" or process.returncode != EXIT_CODE_SUCCESS or verbose or debug) and not quiet: - print(process.stdout) + print(stdout) # Write to file if given if output_to != None and output_to != "stdout": with open(output_to, "w") as f: - f.write(process.stdout) + f.write(stdout) return process.returncode @@ -103,6 +124,10 @@ def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler= add_rmc_rustc_debug_to_env(build_env) return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug) +def append_unwind_tip(text): + unwind_tip = ("[RMC] info: Verification output shows one or more unwinding failures.\n" + "[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n") + return text + unwind_tip def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False): if not keep_temps: @@ -112,7 +137,13 @@ def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temp def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False): cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename] - return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet) + scanners = [] + if "--unwinding-assertions" in cbmc_args: + # Pass a scanner that shows a tip if the CBMC output contains unwinding failures + unwind_asserts_pattern = ".*unwinding assertion.*: FAILURE" + unwind_asserts_scanner = Scanner(unwind_asserts_pattern, append_unwind_tip) + scanners.append(unwind_asserts_scanner) + return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners) def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir="."): results_filename = os.path.join(outdir, "results.xml") diff --git a/src/test/expected/unwind_tip/expected b/src/test/expected/unwind_tip/expected new file mode 100644 index 000000000000..278819fbbe48 --- /dev/null +++ b/src/test/expected/unwind_tip/expected @@ -0,0 +1,2 @@ +[RMC] info: Verification output shows one or more unwinding failures. +[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. diff --git a/src/test/expected/unwind_tip/main.rs b/src/test/expected/unwind_tip/main.rs new file mode 100644 index 000000000000..66b974f5cac3 --- /dev/null +++ b/src/test/expected/unwind_tip/main.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 9 + +include!("../../rmc-prelude.rs"); + +// This example is a copy of the `cbmc` test in +// `src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs` +// +// The verification output should show an unwinding assertion failure. +// +// In this test, we check that RMC warns the user about unwinding failures +// and makes a recommendation to fix the issue. +fn main() { + let mut a: u32 = __nondet(); + + if a < 1024 { + loop { + a = a / 2; + + if a == 0 { + break; + } + } + + assert!(a == 0); + } +} From 448ba55e609a44b050ae6b1dc0391956d756347c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 25 Jun 2021 17:49:44 +0000 Subject: [PATCH 03/10] Use `--no-default-flags` in Leibniz's test to avoid failure --- src/test/cbmc/FunctionCall_Ret-Param/main.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/cbmc/FunctionCall_Ret-Param/main.rs b/src/test/cbmc/FunctionCall_Ret-Param/main.rs index 7344666bd9a8..52bd19275366 100644 --- a/src/test/cbmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/cbmc/FunctionCall_Ret-Param/main.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-flags: --no-default-flags // cbmc-flags: --unwind 10 include!("../../rmc-prelude.rs"); From 531967ddbf9d88551465558fc279f047ce5d1ccb Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 28 Jun 2021 14:22:53 +0000 Subject: [PATCH 04/10] Split checks into groups. Add flags for groups. Print flags. --- scripts/cargo-rmc | 13 ++++++++++--- scripts/rmc | 13 ++++++++++--- scripts/rmc.py | 43 ++++++++++++++++++++++++++++++++----------- 3 files changed, 52 insertions(+), 17 deletions(-) diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 3fc6673012d6..d2beb4c4f6ff 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -31,7 +31,11 @@ def main(): parser.add_argument("--wkdir", default=".") parser.add_argument("--function", default="main") parser.add_argument("crate", help="crate to verify") - parser.add_argument("--no-default-flags", action="store_true") + parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks") + parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") + parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") + parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") + parser.add_argument("--print-cbmc-flags", action="store_true", help="Print CBMC flags associated to an RMC invocation") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -42,10 +46,13 @@ def main(): if not rmc.dependencies_in_path(): return 1 - # Add a set of CBMC arguments by default unless `--no-default-args` is being used - if not args.no_default_flags: + # Add some CBMC flags by default unless `--no-default-checks` is being used + if not args.no_default_checks: rmc.add_default_cbmc_flags(args) + if args.print_cbmc_flags: + rmc.print_cbmc_flags(args) + rmc.cargo_build(args.crate, args.target_dir, args.verbose, args.debug, args.mangler) diff --git a/scripts/rmc b/scripts/rmc index 52da270ad470..d347f606d203 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -27,7 +27,11 @@ def main(): parser.add_argument("--visualize", action="store_true") parser.add_argument("--srcdir", default=".") parser.add_argument("--wkdir", default=".") - parser.add_argument("--no-default-flags", action="store_true") + parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks") + parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") + parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") + parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") + parser.add_argument("--print-cbmc-flags", action="store_true", help="Print CBMC flags associated to an RMC invocation") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -43,10 +47,13 @@ def main(): if not rmc.dependencies_in_path(): return 1 - # Add a set of CBMC arguments by default unless `--no-default-args` is being used - if not args.no_default_flags: + # Add some CBMC flags by default unless `--no-default-checks` is being used + if not args.no_default_checks: rmc.add_default_cbmc_flags(args) + if args.print_cbmc_flags: + rmc.print_cbmc_flags(args) + base, ext = os.path.splitext(args.input) if ext != ".rs": print("ERROR: Expecting .rs input file") diff --git a/scripts/rmc.py b/scripts/rmc.py index 1462a114aa15..3eba91ade9f5 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -12,7 +12,13 @@ RMC_RUSTC_EXE = "rmc-rustc" EXIT_CODE_SUCCESS = 0 -DEFAULT_CBMC_FLAGS = ["--unwinding-assertions"] +MEMORY_SAFETY_CHECKS = ["--pointer-check", + "--bounds-check"] +OVERFLOW_SAFETY_CHECKS = ["--float-overflow-check", + "--pointer-overflow-check", + "--signed-overflow-check", + "--unsigned-overflow-check"] +UNWINDING_CHECKS = ["--unwinding-assertions"] # A Scanner is intended to match a pattern with an output # and edit the output based on an edit function @@ -48,21 +54,36 @@ def delete_file(filename): except OSError: pass -# Add a set of default CBMC arguments +# Add a set of CBMC flags to the CBMC arguments +def add_set_cbmc_flags(args, flags): + # We print a warning if the user has passed the flag via `cbmc_args` + # Otherwise we append it to the CBMC arguments + for arg in flags: + # This behavior must be reviewed if the set of flags is extended + if arg in args.cbmc_args: + print("WARNING: Default CBMC argument `{}` not added (already specified)".format(arg)) + else: + args.cbmc_args.append(arg) + +# Add sets of default CBMC flags def add_default_cbmc_flags(args): - if not args.no_default_flags: - # We print a warning if the user has specified one of the default flags - # Otherwise we append the default flags to CBMC arguments - for arg in DEFAULT_CBMC_FLAGS: - # This behavior must be reviewed if the set of default flags is extended - if arg in args.cbmc_args: - print("WARNING: Default CBMC argument `{}` not added (already specified)".format(arg)) - else: - args.cbmc_args.append(arg) + if not args.no_memory_safety_checks: + add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS) + if not args.no_overflow_safety_checks: + add_set_cbmc_flags(args, OVERFLOW_SAFETY_CHECKS) + if not args.no_unwinding_checks: + add_set_cbmc_flags(args, UNWINDING_CHECKS) def add_rmc_rustc_debug_to_env(env): env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_llvm::gotoc") +def print_cbmc_flags(args): + line = "[RMC] info: CBMC will be called with " + if len(args.cbmc_args) == 0: + line += "no arguments" + else: + line += "arguments " + " ".join(args.cbmc_args) + print(line) def print_rmc_step_status(step_name, completed_process, verbose=False): status = "PASS" From 945c8e722bb0b150f2f5112a830a54c4208a67fc Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 6 Jul 2021 12:42:02 +0000 Subject: [PATCH 05/10] Allow dry runs for rmc and cargo-rmc --- scripts/cargo-rmc | 15 +++++------ scripts/rmc | 17 +++++------- scripts/rmc.py | 66 ++++++++++++++++++++++------------------------- 3 files changed, 44 insertions(+), 54 deletions(-) diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index d2beb4c4f6ff..47090147c99c 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -35,7 +35,7 @@ def main(): parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") - parser.add_argument("--print-cbmc-flags", action="store_true", help="Print CBMC flags associated to an RMC invocation") + parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -50,11 +50,8 @@ def main(): if not args.no_default_checks: rmc.add_default_cbmc_flags(args) - if args.print_cbmc_flags: - rmc.print_cbmc_flags(args) - rmc.cargo_build(args.crate, args.target_dir, - args.verbose, args.debug, args.mangler) + args.verbose, args.debug, args.mangler, args.dry_run) pattern = os.path.join(args.target_dir, "debug", "deps", "*.json") jsons = glob.glob(pattern) @@ -63,11 +60,11 @@ def main(): return 1 cbmc_filename = os.path.join(args.target_dir, "cbmc.out") c_filename = os.path.join(args.target_dir, "cbmc.c") - if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps): + if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run): return 1 if args.gen_c: - if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose): + if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run): return 1 if "--function" not in args.cbmc_args: @@ -76,9 +73,9 @@ def main(): if args.visualize: return rmc.run_visualize(cbmc_filename, args.cbmc_args, \ args.verbose, args.quiet, args.keep_temps, \ - args.function, args.srcdir, args.wkdir, args.target_dir) + args.function, args.srcdir, args.wkdir, args.target_dir, args.dry_run) else: - return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet) + return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run) if __name__ == "__main__": diff --git a/scripts/rmc b/scripts/rmc index d347f606d203..0d62c4c302d1 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -31,7 +31,7 @@ def main(): parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") - parser.add_argument("--print-cbmc-flags", action="store_true", help="Print CBMC flags associated to an RMC invocation") + parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() @@ -51,9 +51,6 @@ def main(): if not args.no_default_checks: rmc.add_default_cbmc_flags(args) - if args.print_cbmc_flags: - rmc.print_cbmc_flags(args) - base, ext = os.path.splitext(args.input) if ext != ".rs": print("ERROR: Expecting .rs input file") @@ -63,18 +60,18 @@ def main(): c_filename = base + ".c" symbols_filename = base + ".symbols" - if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_filename, args.verbose, args.debug, args.keep_temps, args.mangler): + if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_filename, args.verbose, args.debug, args.keep_temps, args.mangler, args.dry_run): return 1 - if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps): + if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps, args.dry_run): return 1 if args.gen_c: - if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose): + if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose, args.dry_run): return 1 if args.gen_symbols: - if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(goto_filename, symbols_filename, args.verbose): + if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(goto_filename, symbols_filename, args.verbose, args.dry_run): return 1 if "--function" not in args.cbmc_args: @@ -84,9 +81,9 @@ def main(): if args.visualize: retcode = rmc.run_visualize(goto_filename, args.cbmc_args, \ args.verbose, args.quiet, args.keep_temps, \ - args.function, args.srcdir, args.wkdir) + args.function, args.srcdir, args.wkdir, args.dry_run) else: - retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet) + retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run) if retcode == CBMC_VERIFICATION_FAILURE_EXIT_CODE and args.allow_cbmc_verification_failure: retcode = EXIT_CODE_SUCCESS return retcode diff --git a/scripts/rmc.py b/scripts/rmc.py index 3eba91ade9f5..1daa4ca6503d 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -77,14 +77,6 @@ def add_default_cbmc_flags(args): def add_rmc_rustc_debug_to_env(env): env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_llvm::gotoc") -def print_cbmc_flags(args): - line = "[RMC] info: CBMC will be called with " - if len(args.cbmc_args) == 0: - line += "no arguments" - else: - line += "arguments " + " ".join(args.cbmc_args) - print(line) - def print_rmc_step_status(step_name, completed_process, verbose=False): status = "PASS" if completed_process.returncode != EXIT_CODE_SUCCESS: @@ -93,7 +85,11 @@ def print_rmc_step_status(step_name, completed_process, verbose=False): print(f"[RMC] stage: {step_name} ({status})") print(f"[RMC] cmd: {' '.join(completed_process.args)}") -def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[]): +def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[], dry_run=False): + if dry_run: + print(' '.join(cmd)) + return EXIT_CODE_SUCCESS + process = subprocess.run( cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, env=env, cwd=cwd) @@ -118,7 +114,7 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve return process.returncode -def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0"): +def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0", dry_run=False): if not keep_temps: atexit.register(delete_file, output_filename) build_cmd = [RMC_RUSTC_EXE, "-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", @@ -127,10 +123,10 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb if debug: add_rmc_rustc_debug_to_env(build_env) - return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug) + return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug, dry_run=dry_run) -def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0"): +def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0", dry_run=False): rustflags = ["-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", f"--cfg={RMC_CFG}"] rustflags = " ".join(rustflags) if "RUSTFLAGS" in os.environ: @@ -143,20 +139,20 @@ def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler= } if debug: add_rmc_rustc_debug_to_env(build_env) - return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug) + return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run) def append_unwind_tip(text): unwind_tip = ("[RMC] info: Verification output shows one or more unwinding failures.\n" "[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n") return text + unwind_tip -def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False): +def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False, dry_run=False): if not keep_temps: atexit.register(delete_file, cbmc_filename) cmd = ["symtab2gb", json_filename, "--out", cbmc_filename] - return run_cmd(cmd, label="to-gotoc", verbose=verbose) + return run_cmd(cmd, label="to-gotoc", verbose=verbose, dry_run=dry_run) -def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False): +def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False): cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename] scanners = [] if "--unwinding-assertions" in cbmc_args: @@ -164,9 +160,9 @@ def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False): unwind_asserts_pattern = ".*unwinding assertion.*: FAILURE" unwind_asserts_scanner = Scanner(unwind_asserts_pattern, append_unwind_tip) scanners.append(unwind_asserts_scanner) - return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners) + return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners, dry_run=dry_run) -def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir="."): +def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir=".", dry_run=False): results_filename = os.path.join(outdir, "results.xml") coverage_filename = os.path.join(outdir, "coverage.xml") property_filename = os.path.join(outdir, "property.xml") @@ -181,27 +177,27 @@ def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_tem # 4) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c temp.goto > property.xml # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto --reportdir report - run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function) + run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function, dry_run=dry_run) - def run_cbmc_local(cbmc_args, output_to): + def run_cbmc_local(cbmc_args, output_to, dry_run=False): cbmc_cmd = ["cbmc"] + cbmc_args + [temp_goto_filename] - return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet) + return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet, dry_run=dry_run) cbmc_xml_args = cbmc_args + ["--xml-ui"] - retcode = run_cbmc_local(cbmc_xml_args + ["--trace"], results_filename) - run_cbmc_local(cbmc_xml_args + ["--cover", "location"], coverage_filename) - run_cbmc_local(cbmc_xml_args + ["--show-properties"], property_filename) + retcode = run_cbmc_local(cbmc_xml_args + ["--trace"], results_filename, dry_run=dry_run) + run_cbmc_local(cbmc_xml_args + ["--cover", "location"], coverage_filename, dry_run=dry_run) + run_cbmc_local(cbmc_xml_args + ["--show-properties"], property_filename, dry_run=dry_run) run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename, - property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report")) + property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"), dry_run=dry_run) return retcode -def run_goto_cc(src, dst, verbose=False, quiet=False, function="main"): +def run_goto_cc(src, dst, verbose=False, quiet=False, function="main", dry_run=False): cmd = ["goto-cc"] + ["--function", function] + [src] + ["-o", dst] - return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet) + return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run) -def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report"): +def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report", dry_run=False): cmd = ["cbmc-viewer"] + \ ["--result", results_filename] + \ ["--coverage", coverage_filename] + \ @@ -210,17 +206,17 @@ def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property ["--wkdir", os.path.realpath(wkdir)] + \ ["--goto", goto_filename] + \ ["--reportdir", reportdir] - return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet) + return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet, dry_run=dry_run) -def run_goto_instrument(input_filename, output_filename, args, verbose=False): +def run_goto_instrument(input_filename, output_filename, args, verbose=False, dry_run=False): cmd = ["goto-instrument"] + args + [input_filename] - return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename) + return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename, dry_run=dry_run) -def goto_to_c(goto_filename, c_filename, verbose=False): - return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose) +def goto_to_c(goto_filename, c_filename, verbose=False, dry_run=False): + return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose, dry_run=dry_run) -def goto_to_symbols(goto_filename, symbols_filename, verbose=False): - return run_goto_instrument(goto_filename, symbols_filename, ["--show-symbol-table"], verbose) +def goto_to_symbols(goto_filename, symbols_filename, verbose=False, dry_run=False): + return run_goto_instrument(goto_filename, symbols_filename, ["--show-symbol-table"], verbose, dry_run=dry_run) From 6112f95825b98f2972c65c1a46d27c8779513380 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 6 Jul 2021 13:55:59 +0000 Subject: [PATCH 06/10] Add starter-kit checks and fix tests --- scripts/cargo-rmc | 2 +- scripts/rmc | 2 +- scripts/rmc.py | 17 +++++++++++------ src/test/cbmc/CodegenConstValue/main.rs | 3 +++ src/test/cbmc/DynTrait/boxed_closure.rs | 2 ++ src/test/cbmc/DynTrait/dyn_fn_param.rs | 2 ++ src/test/cbmc/FunctionCall_Ret-Param/main.rs | 2 +- .../main_no_unwind_asserts.rs | 6 +++--- .../main_no_unwind_asserts.rs | 6 +++--- src/test/cbmc/PointerOffset/Stable/main.rs | 3 +++ src/test/cbmc/PointerOffset/Unstable/main.rs | 3 +++ src/test/cbmc/Pointers_OtherTypes/main.rs | 3 +++ src/test/cbmc/Strings/main.rs | 3 +++ src/test/cbmc/SwitchInt/main.rs | 1 + src/test/cbmc/Whitespace/main.rs | 1 + src/test/firecracker/virtio-block-parse/main.rs | 9 +++------ src/tools/compiletest/src/runtest.rs | 3 +++ 17 files changed, 47 insertions(+), 21 deletions(-) diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 47090147c99c..6cf2020fb7cc 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -33,7 +33,7 @@ def main(): parser.add_argument("crate", help="crate to verify") parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks") parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") - parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") + parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks") parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, diff --git a/scripts/rmc b/scripts/rmc index 0d62c4c302d1..4677d9056ca5 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -29,7 +29,7 @@ def main(): parser.add_argument("--wkdir", default=".") parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks") parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks") - parser.add_argument("--no-overflow-safety-checks", action="store_true", help="Disable default overflow checks") + parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks") parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks") parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, diff --git a/scripts/rmc.py b/scripts/rmc.py index 1daa4ca6503d..b89ca66eb50a 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -13,11 +13,16 @@ EXIT_CODE_SUCCESS = 0 MEMORY_SAFETY_CHECKS = ["--pointer-check", + "--pointer-primitive-check", "--bounds-check"] -OVERFLOW_SAFETY_CHECKS = ["--float-overflow-check", - "--pointer-overflow-check", - "--signed-overflow-check", - "--unsigned-overflow-check"] +OVERFLOW_CHECKS = ["--conversion-check", + "--div-by-zero-check", + "--float-overflow-check", + "--nan-check", + "--pointer-overflow-check", + "--signed-overflow-check", + "--undefined-shift-check", + "--unsigned-overflow-check"] UNWINDING_CHECKS = ["--unwinding-assertions"] # A Scanner is intended to match a pattern with an output @@ -69,8 +74,8 @@ def add_set_cbmc_flags(args, flags): def add_default_cbmc_flags(args): if not args.no_memory_safety_checks: add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS) - if not args.no_overflow_safety_checks: - add_set_cbmc_flags(args, OVERFLOW_SAFETY_CHECKS) + if not args.no_overflow_checks: + add_set_cbmc_flags(args, OVERFLOW_CHECKS) if not args.no_unwinding_checks: add_set_cbmc_flags(args, UNWINDING_CHECKS) diff --git a/src/test/cbmc/CodegenConstValue/main.rs b/src/test/cbmc/CodegenConstValue/main.rs index 34199e30b430..00308f8d7797 100644 --- a/src/test/cbmc/CodegenConstValue/main.rs +++ b/src/test/cbmc/CodegenConstValue/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-memory-safety-checks + const DEC_DIGITS_LUT: &'static [u8] = b"ab"; fn main() { // The next two assertions don't go through to CBMC diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs index 6f2e6042fbfd..8932dc706983 100644 --- a/src/test/cbmc/DynTrait/boxed_closure.rs +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +//rmc-flags: --no-memory-safety-checks + // Check that we can codegen a boxed dyn closure fn main() { diff --git a/src/test/cbmc/DynTrait/dyn_fn_param.rs b/src/test/cbmc/DynTrait/dyn_fn_param.rs index 6dfc62c6bfa9..269e2cbd3d16 100644 --- a/src/test/cbmc/DynTrait/dyn_fn_param.rs +++ b/src/test/cbmc/DynTrait/dyn_fn_param.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +//rmc-flags: --no-memory-safety-checks + // Check that we can pass a dyn function pointer to a stand alone // function definition diff --git a/src/test/cbmc/FunctionCall_Ret-Param/main.rs b/src/test/cbmc/FunctionCall_Ret-Param/main.rs index 52bd19275366..1c11888678e7 100644 --- a/src/test/cbmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/cbmc/FunctionCall_Ret-Param/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-flags: --no-default-flags +// rmc-flags: --no-unwinding-checks // cbmc-flags: --unwind 10 include!("../../rmc-prelude.rs"); diff --git a/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs index 9a22b2d33527..75d177d0f177 100644 --- a/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-flags: --no-default-flags +// rmc-flags: --no-default-checks // cbmc-flags: --unwind 9 include!("../../rmc-prelude.rs"); -// This example tests the RMC flag `--no-default-flags` +// This example tests the RMC flag `--no-default-checks` // // It is the same as `main.rs` except for the flags passed to RMC and CBMC // Running it with `--unwind 10` is not enough to unwind the loop @@ -17,7 +17,7 @@ include!("../../rmc-prelude.rs"); // ** 1 of 2 failed (2 iterations) // VERIFICATION FAILED // -// But with `--no-default-flags` we will avoid introducing a unwinding assertion: +// But with `--no-default-checks` we will avoid introducing a unwinding assertion: // // [main.assertion.1] line 38 assertion failed: a == 0: SUCCESS // diff --git a/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs index 3117068f1a8e..4c5e6181ed5b 100644 --- a/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-flags: --no-default-flags +// rmc-flags: --no-default-checks // cbmc-flags: --unwind 10 include!("../../rmc-prelude.rs"); -// This example tests the RMC flag `--no-default-flags` +// This example tests the RMC flag `--no-default-checks` // // It is the same as `main.rs` except for the flags passed to RMC and CBMC // Running it with `--unwind 10` is not enough to unwind the loop @@ -18,7 +18,7 @@ include!("../../rmc-prelude.rs"); // ** 1 of 2 failed (2 iterations) // VERIFICATION FAILED // -// But with `--no-default-flags` we will avoid introducing a unwinding assertion: +// But with `--no-default-checks` we will avoid introducing a unwinding assertion: // // [main.assertion.1] line 34 assertion failed: a == 0: SUCCESS // diff --git a/src/test/cbmc/PointerOffset/Stable/main.rs b/src/test/cbmc/PointerOffset/Stable/main.rs index 07467bd01386..b75b11686ec8 100644 --- a/src/test/cbmc/PointerOffset/Stable/main.rs +++ b/src/test/cbmc/PointerOffset/Stable/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-overflow-checks + fn main() { // pub unsafe fn offset_from(self, origin: *const T) -> isize // Calculates the distance between two pointers. The returned value diff --git a/src/test/cbmc/PointerOffset/Unstable/main.rs b/src/test/cbmc/PointerOffset/Unstable/main.rs index 93246a1c461f..0218227f8204 100644 --- a/src/test/cbmc/PointerOffset/Unstable/main.rs +++ b/src/test/cbmc/PointerOffset/Unstable/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-overflow-checks + #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; diff --git a/src/test/cbmc/Pointers_OtherTypes/main.rs b/src/test/cbmc/Pointers_OtherTypes/main.rs index 5bc83711b1ce..97ac657547a6 100644 --- a/src/test/cbmc/Pointers_OtherTypes/main.rs +++ b/src/test/cbmc/Pointers_OtherTypes/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-overflow-checks + include!("../../rmc-prelude.rs"); fn main() { diff --git a/src/test/cbmc/Strings/main.rs b/src/test/cbmc/Strings/main.rs index a9b7cdaf6008..3a9275b8c2c9 100644 --- a/src/test/cbmc/Strings/main.rs +++ b/src/test/cbmc/Strings/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --no-overflow-checks + fn test1() { let str = "foo"; let string = str.to_string(); diff --git a/src/test/cbmc/SwitchInt/main.rs b/src/test/cbmc/SwitchInt/main.rs index 7c99721c9f40..c69b282c67de 100644 --- a/src/test/cbmc/SwitchInt/main.rs +++ b/src/test/cbmc/SwitchInt/main.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 fn doswitch_int() -> i32 { diff --git a/src/test/cbmc/Whitespace/main.rs b/src/test/cbmc/Whitespace/main.rs index 0faa4516797f..b461f9038bd8 100644 --- a/src/test/cbmc/Whitespace/main.rs +++ b/src/test/cbmc/Whitespace/main.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 fn main() { diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index 6809364c220f..092b67f1614a 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -1,13 +1,10 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// --unwinding-assertions -// + +// rmc-flags: --no-overflow-checks + // Example from Firecracker virtio block device // We test the parse function against an arbitrary guest memory -// Outstanding issues: -// - Padstone-4795 (std::io:error in enum variant) -// RMC changes -// - strict is_valid check and loop in descriptor chain check during parse #![allow(dead_code)] #![allow(unused_variables)] diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 1bb368bf1fd5..3272274b1299 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2478,8 +2478,11 @@ impl<'test> TestCx<'test> { let parent_dir = self.testpaths.file.parent().unwrap(); // The name of the function to test is the same as the stem of `*.expected` file let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap(); + // `cargo-rmc` has issues with default flags so we pass `--no-default-checks` to disable them + // https://github.com/model-checking/rmc/issues/289 cargo .arg("rmc") + .arg("--no-default-checks") .args(["--function", function_name]) .arg("--target") .arg(self.output_base_dir().join("target")) From c3a9c95196ce840d245c83e604221e876cd816f0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 7 Jul 2021 15:16:00 +0000 Subject: [PATCH 07/10] Add expected test for dry-run feature --- src/test/expected/dry-run/expected | 3 +++ src/test/expected/dry-run/main.rs | 9 +++++++++ 2 files changed, 12 insertions(+) create mode 100644 src/test/expected/dry-run/expected create mode 100644 src/test/expected/dry-run/main.rs diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected new file mode 100644 index 000000000000..4f5d77caff9f --- /dev/null +++ b/src/test/expected/dry-run/expected @@ -0,0 +1,3 @@ +rmc-rustc -Z codegen-backend=gotoc -Z symbol-mangling-version=v0 --cfg=rmc +symtab2gb +cbmc --pointer-check --pointer-primitive-check --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main \ No newline at end of file diff --git a/src/test/expected/dry-run/main.rs b/src/test/expected/dry-run/main.rs new file mode 100644 index 000000000000..0530bb82ed2c --- /dev/null +++ b/src/test/expected/dry-run/main.rs @@ -0,0 +1,9 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-flags: --dry-run + +// `--dry-run` causes RMC to print out commands instead of running them +// In `expected` you will find substrings of these commands because the +// concrete paths depend on your working directory. +fn main() {} From 41c3da81ca1ad77fff9d239729836e5c5d9e86ec Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 7 Jul 2021 15:16:18 +0000 Subject: [PATCH 08/10] Dry-run: Emulate running proc. instead of just printing --- scripts/rmc.py | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/scripts/rmc.py b/scripts/rmc.py index b89ca66eb50a..9251dafba6f4 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -91,13 +91,17 @@ def print_rmc_step_status(step_name, completed_process, verbose=False): print(f"[RMC] cmd: {' '.join(completed_process.args)}") def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[], dry_run=False): + # If this a dry run, we emulate running a successful process whose output is the command itself + # We set `output_to` to `stdout` so that the output is not omitted below if dry_run: - print(' '.join(cmd)) - return EXIT_CODE_SUCCESS - - process = subprocess.run( - cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, - env=env, cwd=cwd) + if output_to == None: + output_to = "stdout" + cmd_line = ' '.join(cmd) + process = subprocess.CompletedProcess(None, EXIT_CODE_SUCCESS, stdout=cmd_line) + else: + process = subprocess.run( + cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, + env=env, cwd=cwd) # Print status if label != None: From bb83b253e4d55374a0342a7e048aae656ddace97 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 7 Jul 2021 18:10:27 +0000 Subject: [PATCH 09/10] Add explanations for checks disabled. Other minor fixes. --- src/test/cbmc/CodegenConstValue/main.rs | 4 ++++ src/test/cbmc/DynTrait/boxed_closure.rs | 5 +++++ src/test/cbmc/DynTrait/dyn_fn_param.rs | 5 +++++ src/test/cbmc/FunctionCall_Ret-Param/main.rs | 4 ++++ src/test/cbmc/PointerOffset/Stable/main.rs | 6 ++++++ src/test/cbmc/PointerOffset/Unstable/main.rs | 6 ++++++ src/test/cbmc/Pointers_OtherTypes/main.rs | 5 +++++ src/test/cbmc/Strings/main.rs | 9 +++++++++ src/test/cbmc/SwitchInt/main.rs | 5 +++++ src/test/cbmc/Whitespace/main.rs | 6 ++++++ src/test/expected/dry-run/expected | 2 +- src/test/firecracker/virtio-block-parse/main.rs | 5 +++++ 12 files changed, 61 insertions(+), 1 deletion(-) diff --git a/src/test/cbmc/CodegenConstValue/main.rs b/src/test/cbmc/CodegenConstValue/main.rs index 00308f8d7797..c64ec0fc2996 100644 --- a/src/test/cbmc/CodegenConstValue/main.rs +++ b/src/test/cbmc/CodegenConstValue/main.rs @@ -3,6 +3,10 @@ // rmc-flags: --no-memory-safety-checks +// We use `--no-memory-safety-checks` in this test to avoid getting +// a verification failure: +// [main.pointer_dereference.5] line 16 dereference failure: pointer outside object bounds in *lut_ptr: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 const DEC_DIGITS_LUT: &'static [u8] = b"ab"; fn main() { // The next two assertions don't go through to CBMC diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs index 8932dc706983..04930cd0f544 100644 --- a/src/test/cbmc/DynTrait/boxed_closure.rs +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -3,6 +3,11 @@ //rmc-flags: --no-memory-safety-checks +// We use `--no-memory-safety-checks` in this test to avoid getting +// a verification failure: +// [pointer_dereference.7] invalid function pointer: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + // Check that we can codegen a boxed dyn closure fn main() { diff --git a/src/test/cbmc/DynTrait/dyn_fn_param.rs b/src/test/cbmc/DynTrait/dyn_fn_param.rs index 269e2cbd3d16..51aa618616e0 100644 --- a/src/test/cbmc/DynTrait/dyn_fn_param.rs +++ b/src/test/cbmc/DynTrait/dyn_fn_param.rs @@ -3,6 +3,11 @@ //rmc-flags: --no-memory-safety-checks +// We use `--no-memory-safety-checks` in this test to avoid getting +// a verification failure: +// [pointer_dereference.14] invalid function pointer: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + // Check that we can pass a dyn function pointer to a stand alone // function definition diff --git a/src/test/cbmc/FunctionCall_Ret-Param/main.rs b/src/test/cbmc/FunctionCall_Ret-Param/main.rs index 1c11888678e7..10f8d1b0203b 100644 --- a/src/test/cbmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/cbmc/FunctionCall_Ret-Param/main.rs @@ -4,6 +4,10 @@ // rmc-flags: --no-unwinding-checks // cbmc-flags: --unwind 10 +// We use `--no-unwinding-checks` in this test to avoid getting +// a verification failure (the loop being unwound depends on +// a nondet. variable) + include!("../../rmc-prelude.rs"); fn main() { diff --git a/src/test/cbmc/PointerOffset/Stable/main.rs b/src/test/cbmc/PointerOffset/Stable/main.rs index b75b11686ec8..9d6ecad8d5a4 100644 --- a/src/test/cbmc/PointerOffset/Stable/main.rs +++ b/src/test/cbmc/PointerOffset/Stable/main.rs @@ -3,6 +3,12 @@ // rmc-flags: --no-overflow-checks +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [overflow.1] arithmetic overflow on signed - in var_11 - var_12: FAILURE +// [overflow.2] arithmetic overflow on signed - in var_11 - var_12: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + fn main() { // pub unsafe fn offset_from(self, origin: *const T) -> isize // Calculates the distance between two pointers. The returned value diff --git a/src/test/cbmc/PointerOffset/Unstable/main.rs b/src/test/cbmc/PointerOffset/Unstable/main.rs index 0218227f8204..0ada27120326 100644 --- a/src/test/cbmc/PointerOffset/Unstable/main.rs +++ b/src/test/cbmc/PointerOffset/Unstable/main.rs @@ -3,6 +3,12 @@ // rmc-flags: --no-overflow-checks +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [overflow.2] arithmetic overflow on signed - in var_23 - var_24: FAILURE +// [overflow.4] arithmetic overflow on signed - in var_33 - var_34: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; diff --git a/src/test/cbmc/Pointers_OtherTypes/main.rs b/src/test/cbmc/Pointers_OtherTypes/main.rs index 97ac657547a6..a09ec879dc68 100644 --- a/src/test/cbmc/Pointers_OtherTypes/main.rs +++ b/src/test/cbmc/Pointers_OtherTypes/main.rs @@ -3,6 +3,11 @@ // rmc-flags: --no-overflow-checks +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [main.NaN.1] line 25 NaN on * in var_30 * 0.0f: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + include!("../../rmc-prelude.rs"); fn main() { diff --git a/src/test/cbmc/Strings/main.rs b/src/test/cbmc/Strings/main.rs index 3a9275b8c2c9..c7cc4fc3193e 100644 --- a/src/test/cbmc/Strings/main.rs +++ b/src/test/cbmc/Strings/main.rs @@ -3,6 +3,15 @@ // rmc-flags: --no-overflow-checks +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [_RINvMNtCs9Odk7Lrvgnw_4core6optionINtB3_6OptioncE5ok_orjECs21hi0yVfW1J_4main.overflow.1] line 569 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&self + 0)) - 1114112: FAILURE +// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.1] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_4) + 0)) - 1114112: FAILURE +// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.2] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_7) + 0)) - 1114112: FAILURE +// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.3] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.0) + 0)) - 1114112: FAILURE +// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.4] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.1) + 0)) - 1114112: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + fn test1() { let str = "foo"; let string = str.to_string(); diff --git a/src/test/cbmc/SwitchInt/main.rs b/src/test/cbmc/SwitchInt/main.rs index c69b282c67de..9c341457e204 100644 --- a/src/test/cbmc/SwitchInt/main.rs +++ b/src/test/cbmc/SwitchInt/main.rs @@ -4,6 +4,11 @@ // rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [_RNvCs21hi0yVfW1J_4main14doswitch_chars.overflow.1] line 17 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_7 + 0)) - 1114112: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + fn doswitch_int() -> i32 { for i in [99].iter() { if *i == 99 { diff --git a/src/test/cbmc/Whitespace/main.rs b/src/test/cbmc/Whitespace/main.rs index b461f9038bd8..3e321e7a83b2 100644 --- a/src/test/cbmc/Whitespace/main.rs +++ b/src/test/cbmc/Whitespace/main.rs @@ -4,6 +4,12 @@ // rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [_RNvXs3_NtNtCs9Odk7Lrvgnw_4core3str4iterNtB5_11CharIndicesNtNtNtNtB9_4iter6traits8iterator8Iterator4nextCs21hi0yVfW1J_4main.overflow.1] line 141 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_4 + 0)) - 1114112: FAILURE +// [_RNvXs5_NtNtCs9Odk7Lrvgnw_4core3str7patternINtB5_19MultiCharEqSearcherNtB7_12IsWhitespaceENtB5_8Searcher4nextCs21hi0yVfW1J_4main.overflow.1] line 641 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_5 + 8)) - 1114112: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + fn main() { let mut iter = "A few words".split_whitespace(); match iter.next() { diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected index 4f5d77caff9f..0d62f1a40a36 100644 --- a/src/test/expected/dry-run/expected +++ b/src/test/expected/dry-run/expected @@ -1,3 +1,3 @@ rmc-rustc -Z codegen-backend=gotoc -Z symbol-mangling-version=v0 --cfg=rmc symtab2gb -cbmc --pointer-check --pointer-primitive-check --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main \ No newline at end of file +cbmc --pointer-check --pointer-primitive-check --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index 092b67f1614a..79dae3416031 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -3,6 +3,11 @@ // rmc-flags: --no-overflow-checks +// We use `--no-overflow-checks` in this test to avoid getting +// a verification failure: +// [overflow.1] arithmetic overflow on unsigned + in var_6 + var_7: FAILURE +// Tracking issue: https://github.com/model-checking/rmc/issues/307 + // Example from Firecracker virtio block device // We test the parse function against an arbitrary guest memory From c213892542b7279953dc927fa0f7eef85663cad5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Jul 2021 18:15:52 +0000 Subject: [PATCH 10/10] Order. Rename. Cover flags. --- scripts/cargo-rmc | 2 +- scripts/rmc | 6 ++++-- scripts/rmc.py | 22 ++++++++++++---------- src/test/expected/dry-run/expected | 2 +- 4 files changed, 18 insertions(+), 14 deletions(-) diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 6cf2020fb7cc..c5361d5b6cbd 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -48,7 +48,7 @@ def main(): # Add some CBMC flags by default unless `--no-default-checks` is being used if not args.no_default_checks: - rmc.add_default_cbmc_flags(args) + rmc.add_selected_default_cbmc_flags(args) rmc.cargo_build(args.crate, args.target_dir, args.verbose, args.debug, args.mangler, args.dry_run) diff --git a/scripts/rmc b/scripts/rmc index 4677d9056ca5..f1a62274ad53 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -49,7 +49,7 @@ def main(): # Add some CBMC flags by default unless `--no-default-checks` is being used if not args.no_default_checks: - rmc.add_default_cbmc_flags(args) + rmc.add_selected_default_cbmc_flags(args) base, ext = os.path.splitext(args.input) if ext != ".rs": @@ -79,7 +79,9 @@ def main(): args.cbmc_args.append(str(RMC_C_LIB)) if args.visualize: - retcode = rmc.run_visualize(goto_filename, args.cbmc_args, \ + # Use a separate set of flags for coverage checking (empty for now) + cover_args = [] + retcode = rmc.run_visualize(goto_filename, args.cbmc_args, cover_args, \ args.verbose, args.quiet, args.keep_temps, \ args.function, args.srcdir, args.wkdir, args.dry_run) else: diff --git a/scripts/rmc.py b/scripts/rmc.py index 9251dafba6f4..24b48f7d5578 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -12,9 +12,9 @@ RMC_RUSTC_EXE = "rmc-rustc" EXIT_CODE_SUCCESS = 0 -MEMORY_SAFETY_CHECKS = ["--pointer-check", - "--pointer-primitive-check", - "--bounds-check"] +MEMORY_SAFETY_CHECKS = ["--bounds-check", + "--pointer-check", + "--pointer-primitive-check"] OVERFLOW_CHECKS = ["--conversion-check", "--div-by-zero-check", "--float-overflow-check", @@ -70,8 +70,8 @@ def add_set_cbmc_flags(args, flags): else: args.cbmc_args.append(arg) -# Add sets of default CBMC flags -def add_default_cbmc_flags(args): +# Add sets of selected default CBMC flags +def add_selected_default_cbmc_flags(args): if not args.no_memory_safety_checks: add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS) if not args.no_overflow_checks: @@ -171,7 +171,7 @@ def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False scanners.append(unwind_asserts_scanner) return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners, dry_run=dry_run) -def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir=".", dry_run=False): +def run_visualize(cbmc_filename, prop_args, cover_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir=".", dry_run=False): results_filename = os.path.join(outdir, "results.xml") coverage_filename = os.path.join(outdir, "coverage.xml") property_filename = os.path.join(outdir, "property.xml") @@ -192,10 +192,12 @@ def run_cbmc_local(cbmc_args, output_to, dry_run=False): cbmc_cmd = ["cbmc"] + cbmc_args + [temp_goto_filename] return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet, dry_run=dry_run) - cbmc_xml_args = cbmc_args + ["--xml-ui"] - retcode = run_cbmc_local(cbmc_xml_args + ["--trace"], results_filename, dry_run=dry_run) - run_cbmc_local(cbmc_xml_args + ["--cover", "location"], coverage_filename, dry_run=dry_run) - run_cbmc_local(cbmc_xml_args + ["--show-properties"], property_filename, dry_run=dry_run) + cbmc_prop_args = prop_args + ["--xml-ui"] + cbmc_cover_args = cover_args + ["--xml-ui"] + + retcode = run_cbmc_local(cbmc_prop_args + ["--trace"], results_filename, dry_run=dry_run) + run_cbmc_local(cbmc_cover_args + ["--cover", "location"], coverage_filename, dry_run=dry_run) + run_cbmc_local(cbmc_prop_args + ["--show-properties"], property_filename, dry_run=dry_run) run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename, property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"), dry_run=dry_run) diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected index 0d62f1a40a36..e862a76a7290 100644 --- a/src/test/expected/dry-run/expected +++ b/src/test/expected/dry-run/expected @@ -1,3 +1,3 @@ rmc-rustc -Z codegen-backend=gotoc -Z symbol-mangling-version=v0 --cfg=rmc symtab2gb -cbmc --pointer-check --pointer-primitive-check --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main +cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main