From dd9412c061c49cfba511d10c83d400c99a236f87 Mon Sep 17 00:00:00 2001 From: Thomas Del Vecchio Date: Tue, 25 May 2021 15:07:18 -0400 Subject: [PATCH] Added v0 mangler as default for rmc, and added --mangler option. --- scripts/cargo-rmc | 3 ++- scripts/rmc | 3 ++- scripts/rmc.py | 8 ++++---- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 8723e3538876..8d386b961b15 100755 --- a/scripts/cargo-rmc +++ b/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) diff --git a/scripts/rmc b/scripts/rmc index a6336fabf4f0..7461b12c0d18 100755 --- a/scripts/rmc +++ b/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): diff --git a/scripts/rmc.py b/scripts/rmc.py index 81fe1ef4998a..c6aeab115793 100644 --- a/scripts/rmc.py +++ b/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