From 93df8e7d144fb19eb0e819ae109eaf0aaeccda3e Mon Sep 17 00:00:00 2001 From: Thomas Del Vecchio Date: Thu, 20 May 2021 13:37:38 -0400 Subject: [PATCH] Added --visualize flag to rmc. --- README.md | 2 + scripts/cargo-rmc | 19 ++++++++- scripts/rmc | 18 +++++++- scripts/rmc.py | 106 ++++++++++++++++++++++++++++++---------------- 4 files changed, 106 insertions(+), 39 deletions(-) diff --git a/README.md b/README.md index 7a658527bf52..54a18f6ce6bb 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,8 @@ If you encounter issues when using RMC we encourage you to [the cmake instructions from the CBMC repo](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake). We recommend using `ninja` as the CBMC build system. +1. Install [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc/releases/latest). + 1. Configure RMC. We recommend using the following options: ``` diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 8d386b961b15..5ae39167734a 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -22,10 +22,19 @@ def main(): parser.add_argument("--debug", action="store_true") parser.add_argument("--keep-temps", action="store_true") parser.add_argument("--mangler", default="v0") + parser.add_argument("--visualize", action="store_true") + parser.add_argument("--srcdir", default=".") + parser.add_argument("--wkdir", default=".") parser.add_argument("crate", help="crate to verify") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() + + # In the future we hope to make this configurable in the command line. + # For now, however, changing this from "main" breaks rmc. + # Issue: https://github.com/model-checking/rmc/issues/169 + args.function = "main" + if args.quiet: args.verbose = False @@ -43,7 +52,15 @@ def main(): if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps): return 1 - return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet) + if "--function" not in args.cbmc_args: + args.cbmc_args.extend(["--function", args.function]) + + 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) + else: + return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet) if __name__ == "__main__": diff --git a/scripts/rmc b/scripts/rmc index 7461b12c0d18..8f6fb137beb7 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -24,9 +24,18 @@ def main(): parser.add_argument("--gen-symbols", action="store_true") parser.add_argument("--allow-cbmc-verification-failure", action="store_true") parser.add_argument("--mangler", default="v0") + parser.add_argument("--visualize", action="store_true") + parser.add_argument("--srcdir", default=".") + parser.add_argument("--wkdir", default=".") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() + + # In the future we hope to make this configurable in the command line. + # For now, however, changing this from "main" breaks rmc. + # Issue: https://github.com/model-checking/rmc/issues/169 + args.function = "main" + if args.quiet: args.verbose = False @@ -57,10 +66,15 @@ def main(): return 1 if "--function" not in args.cbmc_args: - args.cbmc_args.extend(["--function", "main"]) + args.cbmc_args.extend(["--function", args.function]) args.cbmc_args.append(str(RMC_C_LIB)) - retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet) + 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) + else: + retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet) 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 c6aeab115793..4690a20c9e1c 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -4,6 +4,7 @@ import subprocess import atexit import os +import os.path RMC_CFG = "rmc" @@ -17,7 +18,7 @@ def is_exe(name): def dependencies_in_path(): - for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "goto-instrument"]: + for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "cbmc-viewer", "goto-instrument", "goto-cc"]: if not is_exe(program): print("ERROR: Could not find {} in PATH".format(program)) return False @@ -43,6 +44,25 @@ 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) + + # Print status + if label != None: + print_rmc_step_status(label, process, verbose) + + # 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) + + # Write to file if given + if output_to != None and output_to != "stdout": + with open(output_to, "w") as f: + f.write(process.stdout) + + return process.returncode def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0"): if not keep_temps: @@ -52,12 +72,8 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb build_env = os.environ if debug: add_rmc_rustc_debug_to_env(build_env) - process = subprocess.run(build_cmd, universal_newlines=True, env=build_env, - stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - print_rmc_step_status("compile", process, verbose) - if process.returncode != EXIT_CODE_SUCCESS or verbose or debug: - print(process.stdout) - return process.returncode + + return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug) def cargo_build(crate, verbose=False, debug=False, mangler="v0"): @@ -73,49 +89,67 @@ def cargo_build(crate, verbose=False, debug=False, mangler="v0"): } if debug: add_rmc_rustc_debug_to_env(build_env) - process = subprocess.run(build_cmd, universal_newlines=True, cwd=crate, - env=build_env, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - print_rmc_step_status("build", process, verbose) - if process.returncode != EXIT_CODE_SUCCESS or verbose or debug: - print(process.stdout) - return process.returncode + return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug) def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False): if not keep_temps: atexit.register(delete_file, cbmc_filename) cmd = ["symtab2gb", json_filename, "--out", cbmc_filename] - process = subprocess.run( - cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - print_rmc_step_status("to-gotoc", process, verbose) - if process.returncode != EXIT_CODE_SUCCESS or verbose: - print(process.stdout) - return process.returncode - + return run_cmd(cmd, label="to-gotoc", verbose=verbose) def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False): cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename] - process = subprocess.Popen(cbmc_cmd, universal_newlines=True, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT) - if not quiet: - for line in iter(process.stdout.readline, ""): - print(line, end="") - process.stdout.close() - retcode = process.wait() - print_rmc_step_status("cbmc", process, verbose) + 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="."): + results_filename = "results.xml" + coverage_filename = "coverage.xml" + property_filename = "property.xml" + temp_goto_filename = "temp.goto" + if not keep_temps: + for filename in [results_filename, coverage_filename, property_filename, temp_goto_filename]: + atexit.register(delete_file, filename) + + # 1) goto-cc --function main -o temp.goto + # 2) cbmc --xml-ui --trace ~/rmc/library/rmc/rmc_lib.c temp.goto > results.xml + # 3) cbmc --xml-ui --cover location ~/rmc/library/rmc/rmc_lib.c temp.goto > coverage.xml + # 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 + + run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet) + + def run_cbmc_local(cbmc_args, output_to): + cbmc_cmd = ["cbmc"] + cbmc_args + [temp_goto_filename] + return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet) + + 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) + + run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename, property_filename, verbose, quiet, srcdir, wkdir) + return retcode +def run_goto_cc(src, dst, verbose=False, quiet=False, function="main"): + cmd = ["goto-cc"] + ["--function", function] + [src] + ["-o", dst] + return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet) + +def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir="."): + cmd = ["cbmc-viewer"] + \ + ["--result", results_filename] + \ + ["--coverage", coverage_filename] + \ + ["--property", property_filename] + \ + ["--srcdir", os.path.realpath(srcdir)] + \ + ["--wkdir", os.path.realpath(wkdir)] + \ + ["--goto", goto_filename] + return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet) + def run_goto_instrument(input_filename, output_filename, args, verbose=False): cmd = ["goto-instrument"] + args + [input_filename] - with open(output_filename, "w") as f: - process = subprocess.run( - cmd, universal_newlines=True, stdout=f, stderr=subprocess.PIPE) - print_rmc_step_status("goto-instrument", process, verbose) - if process.returncode != 0 or verbose: - print(process.stderr) - return process.returncode + return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename) def goto_to_c(goto_filename, c_filename, verbose=False):