Use default CBMC flags in RMC

scripts/cargo-rmc

@@ -31,6 +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-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-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,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
@@ -41,8 +46,12 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
+    # Add some CBMC flags by default unless `--no-default-checks` is being used
+    if not args.no_default_checks:
+        rmc.add_selected_default_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)
@@ -51,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:
@@ -64,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__":

scripts/rmc

@@ -27,6 +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-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-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,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
@@ -41,6 +46,10 @@ def main():
 
     if not rmc.dependencies_in_path():
         return 1
+
+    # Add some CBMC flags by default unless `--no-default-checks` is being used
+    if not args.no_default_checks:
+        rmc.add_selected_default_cbmc_flags(args)
 
     base, ext = os.path.splitext(args.input)
     if ext != ".rs":
@@ -51,30 +60,32 @@ 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:
         args.cbmc_args.extend(["--function", args.function])
 
     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.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

scripts/rmc.py

@@ -5,12 +5,40 @@
 import atexit
 import os
 import os.path
+import re
 
 
 RMC_CFG = "rmc"
 RMC_RUSTC_EXE = "rmc-rustc"
 EXIT_CODE_SUCCESS = 0
 
+MEMORY_SAFETY_CHECKS = ["--bounds-check",
+                        "--pointer-check",
+                        "--pointer-primitive-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
+# 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
@@ -31,11 +59,29 @@ def delete_file(filename):
     except OSError:
         pass
 
+# 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 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:
+        add_set_cbmc_flags(args, OVERFLOW_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_rmc_step_status(step_name, completed_process, verbose=False):
     status = "PASS"
     if completed_process.returncode != EXIT_CODE_SUCCESS:
@@ -44,27 +90,40 @@ 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):
-    process = subprocess.run(
-        cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
-        env=env, cwd=cwd)
+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:
+        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:
         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
 
-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}",
@@ -73,10 +132,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:
@@ -89,20 +148,30 @@ 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]
-    return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet)
-
-def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir="."):
+    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, dry_run=dry_run)
+
+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")
@@ -117,27 +186,29 @@ 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_prop_args = prop_args + ["--xml-ui"]
+    cbmc_cover_args = cover_args + ["--xml-ui"]
 
-    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_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"))
+                    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] + \
@@ -146,17 +217,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)

src/test/cbmc/CodegenConstValue/main.rs

@@ -1,5 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// 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

src/test/cbmc/DynTrait/boxed_closure.rs

@@ -1,6 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//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() {

src/test/cbmc/DynTrait/dyn_fn_param.rs

@@ -1,6 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//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