Added --visualize flag to rmc and cargo-rmc.

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:
    ```

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__":

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

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 <cbmc_filename> -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):