Added v0 mangler as default for rmc, and added --mangler option. (rust-lang#170)

Author: vecchiot-aws

scripts/cargo-rmc

@@ -21,6 +21,7 @@ def main():
     parser.add_argument("--quiet", "-q", action="store_true")
     parser.add_argument("--debug", action="store_true")
     parser.add_argument("--keep-temps", action="store_true")
+    parser.add_argument("--mangler", default="v0")
     parser.add_argument("crate", help="crate to verify")
     parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
@@ -31,7 +32,7 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
-    rmc.cargo_build(args.crate, args.verbose, args.debug)
+    rmc.cargo_build(args.crate, args.verbose, args.debug, args.mangler)
 
     pattern = f"target/debug/deps/*.json"
     jsons = glob.glob(pattern)

scripts/rmc

@@ -23,6 +23,7 @@ def main():
     parser.add_argument("--gen-c", action="store_true")
     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("cbmc_args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
@@ -41,7 +42,7 @@ 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):
+    if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_filename, args.verbose, args.debug, args.keep_temps, args.mangler):
         return 1
 
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps):

scripts/rmc.py

@@ -44,10 +44,10 @@ def print_rmc_step_status(step_name, completed_process, verbose=False):
         print(f"[RMC] cmd: {' '.join(completed_process.args)}")
 
 
-def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False):
+def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0"):
     if not keep_temps:
         atexit.register(delete_file, output_filename)
-    build_cmd = [RMC_RUSTC_EXE, "-Z", "codegen-backend=gotoc",
+    build_cmd = [RMC_RUSTC_EXE, "-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}",
                  f"--cfg={RMC_CFG}", "-o", output_filename, input_filename]
     build_env = os.environ
     if debug:
@@ -60,8 +60,8 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb
     return process.returncode
 
 
-def cargo_build(crate, verbose=False, debug=False):
-    rustflags = ["-Z", "codegen-backend=gotoc", f"--cfg={RMC_CFG}"]
+def cargo_build(crate, verbose=False, debug=False, mangler="v0"):
+    rustflags = ["-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", f"--cfg={RMC_CFG}"]
     rustflags = " ".join(rustflags)
     if "RUSTFLAGS" in os.environ:
         rustflags = os.environ["RUSTFLAGS"] + " " + rustflags