Fix cargo rmc to support multiple dependencies (rust-lang#451) (rust-lang#557)

When building multiple dependencies, rmc compilation generates multiple
*json files which need to be merged before running CBMC.

This remove the assumption that only json file is generated and use all
the generated json files to generated the gotoc.

Author: celinval

scripts/cargo-rmc

@@ -27,16 +27,15 @@ def main():
 
         pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
         symbol_table_jsons = glob.glob(pattern)
-        rmc.ensure(len(symbol_table_jsons) == 1, f"Unexpected number of json outputs: {len(symbol_table_jsons)}")
+        rmc.ensure(len(symbol_table_jsons) > 0, f"Unexpected number of json outputs: {len(symbol_table_jsons)}")
 
         cbmc_runnable_filename = os.path.join(args.target_dir, "cbmc_runnable.out")
         c_runnable_filename = os.path.join(args.target_dir, "cbmc_runnable.c")
 
-        if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(symbol_table_jsons[0], cbmc_runnable_filename, args.verbose, args.keep_temps, args.dry_run):
-            return 1
+        out_files = rmc.symbol_table_to_gotoc(symbol_table_jsons, args.verbose, args.keep_temps, args.dry_run)
 
-        if EXIT_CODE_SUCCESS != rmc.link_c_lib(cbmc_runnable_filename, cbmc_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
-            return 1
+        rmc.link_c_lib(out_files, cbmc_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function,
+                       args.dry_run)
 
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
             return 1
@@ -50,21 +49,19 @@ def main():
     symbol_table_jsons = glob.glob(pattern)
 
     if not args.dry_run:
-        rmc.ensure(len(symbol_table_jsons) == 1, f"Unexpected number of json outputs: {len(symbol_table_jsons)}")
+        rmc.ensure(len(symbol_table_jsons) > 0, f"Unexpected number of json outputs: {len(symbol_table_jsons)}")
     else:
         # Add a dummy value so dry-run works.
         symbol_table_jsons = ["dry-run.symtab.json"]
 
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
     symbols_filename = os.path.join(args.target_dir, "cbmc.symbols")
-    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(symbol_table_jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):
-        return 1
+    out_files = rmc.symbol_table_to_gotoc(symbol_table_jsons, args.verbose, args.keep_temps, args.dry_run)
 
     args.c_lib.append(str(RMC_C_LIB))
 
-    if EXIT_CODE_SUCCESS != rmc.link_c_lib(cbmc_filename, cbmc_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
-        return 1
+    rmc.link_c_lib(out_files, cbmc_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run)
 
     if args.gen_c:
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run):

scripts/rmc

@@ -30,11 +30,10 @@ def main():
         if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, base, json_runnable_filename, args.verbose, args.debug, args.keep_temps, args.mangler, args.dry_run, ["gen-c"]):
             return 1
 
-        if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_runnable_filename, goto_runnable_filename, args.verbose, args.keep_temps, args.dry_run):
-            return 1
+        out_files = rmc.symbol_table_to_gotoc([json_runnable_filename], args.verbose, args.keep_temps, args.dry_run)
 
-        if EXIT_CODE_SUCCESS != rmc.link_c_lib(goto_runnable_filename, goto_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
-            return 1
+        rmc.link_c_lib(out_files, goto_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function,
+                       args.dry_run)
 
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
             return 1
@@ -49,8 +48,7 @@ def main():
     if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, base, symbol_table_json_filename, args.verbose, args.debug, args.keep_temps, args.mangler, args.dry_run, args.use_abs, args.abs_type, []):
         return 1
 
-    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(symbol_table_json_filename, goto_filename, args.verbose, args.keep_temps, args.dry_run):
-        return 1
+    out_files = rmc.symbol_table_to_gotoc([symbol_table_json_filename], args.verbose, args.keep_temps, args.dry_run)
 
     args.c_lib.append(str(RMC_C_LIB))
 
@@ -63,8 +61,7 @@ def main():
         RMC_C_HASHSET = RMC_C_STUB / "hashset" / "hashset.c"
         args.c_lib.append(str(RMC_C_HASHSET))
 
-    if EXIT_CODE_SUCCESS != rmc.link_c_lib(goto_filename, goto_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
-        return 1
+    rmc.link_c_lib(out_files, goto_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run)
 
     if args.gen_c:
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose, args.dry_run):

scripts/rmc.py

@@ -137,20 +137,25 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve
 
     return process.returncode
 
+def rustc_flags(mangler, symbol_table_passes):
+    flags = [
+        "-Z", "codegen-backend=gotoc",
+        "-Z", "trim-diagnostic-paths=no",
+        "-Z", f"symbol-mangling-version={mangler}",
+        "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}",
+        "-Z", "human_readable_cgu_names",
+        f"--cfg={RMC_CFG}"]
+    if "RUSTFLAGS" in os.environ:
+        flags += os.environ["RUSTFLAGS"].split(" ")
+    return flags
+
 # Generates a symbol table from a rust file
 def compile_single_rust_file(input_filename, base, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0", dry_run=False, use_abs=False, abs_type="std", symbol_table_passes=[]):
     if not keep_temps:
         atexit.register(delete_file, output_filename)
         atexit.register(delete_file, base + ".type_map.json")
 
-    build_cmd = [RMC_RUSTC_EXE,
-            "-Z", "codegen-backend=gotoc",
-            "-Z", "trim-diagnostic-paths=no",
-            "-Z", f"symbol-mangling-version={mangler}",
-            "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}",
-            "--crate-type=lib",
-            "-Z", "human_readable_cgu_names",
-            f"--cfg={RMC_CFG}"]
+    build_cmd = [RMC_RUSTC_EXE, "--crate-type=lib"] + rustc_flags(mangler, symbol_table_passes)
 
     if use_abs:
         build_cmd += ["-Z", "force-unstable-if-unmarked=yes",
@@ -159,8 +164,6 @@ def compile_single_rust_file(input_filename, base, output_filename, verbose=Fals
 
     build_cmd += ["-o", base + ".o", input_filename]
 
-    if "RUSTFLAGS" in os.environ:
-        build_cmd += os.environ["RUSTFLAGS"].split(" ")
     build_env = os.environ
     if debug:
         add_rmc_rustc_debug_to_env(build_env)
@@ -171,19 +174,9 @@ def compile_single_rust_file(input_filename, base, output_filename, verbose=Fals
 def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry_run=False, symbol_table_passes=[]):
     ensure(os.path.isdir(crate), f"Invalid path to crate: {crate}")
 
-    rustflags = [
-        "-Z", "codegen-backend=gotoc",
-        "-Z", "trim-diagnostic-paths=no",
-        "-Z", f"symbol-mangling-version={mangler}",
-        "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}",
-        "-Z", "human_readable_cgu_names",
-        f"--cfg={RMC_CFG}"]
-    rustflags = " ".join(rustflags)
-    if "RUSTFLAGS" in os.environ:
-        rustflags = os.environ["RUSTFLAGS"] + " " + rustflags
-
+    rustflags = rustc_flags(mangler, symbol_table_passes)
     build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)]
-    build_env = {"RUSTFLAGS": rustflags,
+    build_env = {"RUSTFLAGS": " ".join(rustflags),
                  "RUSTC": RMC_RUSTC_EXE,
                  "PATH": os.environ["PATH"],
                  }
@@ -198,16 +191,25 @@ def append_unwind_tip(text):
     return text + unwind_tip
 
 # Generates a goto program from a symbol table
-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, dry_run=dry_run)
+def symbol_table_to_gotoc(json_files, verbose=False, keep_temps=False, dry_run=False):
+    out_files = []
+    for json in json_files:
+        out_file = json + ".out"
+        out_files.append(out_file)
+        if not keep_temps:
+            atexit.register(delete_file, out_file)
+
+        cmd = ["symtab2gb", json, "--out", out_file]
+        if run_cmd(cmd, label="to-gotoc", verbose=verbose, dry_run=dry_run) != EXIT_CODE_SUCCESS:
+            raise Exception("Failed to run command: {}".format(" ".join(cmd)))
+
+    return out_files
 
 # Links in external C programs into a goto program
-def link_c_lib(src, dst, c_lib, verbose=False, quiet=False, function="main", dry_run=False):
-    cmd = ["goto-cc"] + ["--function", function] + [src] + c_lib + ["-o", dst]
-    return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run)
+def link_c_lib(srcs, dst, c_lib, verbose=False, quiet=False, function="main", dry_run=False):
+    cmd = ["goto-cc"] + ["--function", function] + srcs + c_lib + ["-o", dst]
+    if run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run) != EXIT_CODE_SUCCESS:
+        raise Exception("Failed to run command: {}".format(" ".join(cmd)))
 
 # Runs CBMC on a goto program
 def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False):

src/test/expected/dry-run/expected

@@ -1,4 +1,4 @@
-rmc-rustc -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z symbol-mangling-version=v0 -Z symbol_table_passes= --crate-type=lib -Z human_readable_cgu_names --cfg=rmc
+rmc-rustc --crate-type=lib -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z symbol-mangling-version=v0 -Z symbol_table_passes= -Z human_readable_cgu_names --cfg=rmc
 symtab2gb
 goto-cc --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

src/test/rmc-multicrate/type-mismatch/run-mismatch-test.sh

@@ -13,20 +13,15 @@ echo
 cd $(dirname $0)
 rm -rf /tmp/type_mismatch_test_build
 cd mismatch
-# Disable warnings until https://github.com/model-checking/rmc/issues/573 is fixed
-RUSTC_LOG=error CARGO_TARGET_DIR=/tmp/type_mismatch_test_build RUST_BACKTRACE=1 RUSTFLAGS="-Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo build
-
-# Convert from JSON to Gotoc 
-cd /tmp/type_mismatch_test_build/debug/deps/
-ls *.symtab.json | xargs symtab2gb
+RESULT="/tmp/dependency_test_result.txt"
 
-# Add the entry point and remove unused functions
-goto-cc --function main *.out -o a.out 
-goto-instrument --drop-unused-functions a.out b.out 
+# Disable warnings until https://github.com/model-checking/rmc/issues/573 is fixed
+export RUSTC_LOG=error
+export CARGO_TARGET_DIR=/tmp/type_mismatch_test_build
+export RUST_BACKTRACE=1
+cargo rmc &> $RESULT
 
 # Run the solver
-RESULT="/tmp/dependency_test_result.txt"
-cbmc b.out &> $RESULT
 if ! grep -q "VERIFICATION SUCCESSFUL" $RESULT; then
   cat $RESULT
   echo