Change cargo rmc script to use RUSTC binary during build (rust-lang#613) (rust-lang#615)

When the crate contains a build script, cargo compiles the build script first without the RUSTFLAGS. Thus, we cannot use rmc-rustc directly, or it will try to compile the build script with rmc enabled. We then fail to generate the script binary.

* Add --build-target to cargo rmc

Author: celinval

scripts/cargo-rmc

@@ -9,6 +9,7 @@ import rmc
 import rmc_flags
 import os
 import pathlib
+import platform
 import toml
 
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
@@ -22,7 +23,7 @@ def main():
     rmc.ensure_dependencies_in_path()
 
     if args.gen_c_runnable:
-        rmc.cargo_build(args.crate, args.target_dir,
+        rmc.cargo_build(args.crate, args.target_dir, args.build_target,
                         args.verbose, args.debug, args.mangler, args.dry_run, ["gen-c"])
 
         pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
@@ -42,10 +43,13 @@ def main():
 
         rmc.gen_c_postprocess(c_runnable_filename, args.dry_run)
 
-    rmc.cargo_build(args.crate, args.target_dir,
+    rmc.cargo_build(args.crate, args.target_dir, args.build_target,
                     args.verbose, args.debug, args.mangler, args.dry_run, [])
 
-    pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
+    if args.build_target:
+        pattern = os.path.join(args.target_dir, args.build_target, "debug", "deps", "*.symtab.json")
+    else:
+        pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
     symbol_table_jsons = glob.glob(pattern)
 
     if not args.dry_run:
@@ -108,6 +112,24 @@ def main():
 
     return retcode
 
+
+def default_build_target():
+    """
+    Returns the default build target based on the current OS.
+
+    This function will return None for windows and print a warning.
+    """
+    machine = platform.uname()
+    if machine.system == "Linux":
+        return"x86_64-unknown-linux-gnu"
+
+    if machine.system == "Darwin":
+        return "x86_64-apple-darwin"
+
+    print("WARNING: No default build target exists for this platform. Please use --build-target to set the correct target")
+    return None
+
+
 def parse_args():
     # Create parser
     def create_parser():
@@ -124,6 +146,8 @@ def parse_args():
         config_group.add_argument("--config-toml",
                                   help="Where to read configuration from; defaults to crate's Cargo.toml")
         config_group.add_argument("--no-config-toml", action="store_true", help="Do not use any configuration toml")
+        config_group.add_argument("--build-target", help="Build for the target triple.",
+                                  default=default_build_target())
 
         exclude_flags = []
         rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)

scripts/rmc.py

@@ -189,13 +189,37 @@ def compile_single_rust_file(
     return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug, dry_run=dry_run)
 
 # Generates a symbol table (and some other artifacts) from a rust crate
-def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry_run=False, symbol_table_passes=[]):
+def cargo_build(
+        crate,
+        target_dir,
+        build_target=None,
+        verbose=False,
+        debug=False,
+        mangler="v0",
+        dry_run=False,
+        symbol_table_passes=[]):
     ensure(os.path.isdir(crate), f"Invalid path to crate: {crate}")
 
-    rustflags = rustc_flags(mangler, symbol_table_passes)
+    def get_config(option):
+        process = subprocess.run(
+            [RMC_RUSTC_EXE, option],
+            universal_newlines=True,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.STDOUT,
+            env=os.environ,
+            cwd=crate)
+        if process.returncode != EXIT_CODE_SUCCESS:
+            raise Exception("[Error] Fail to extract rmc configuration.\n{}".format(
+                process.stdout))
+        return process.stdout
+
+    rustflags = rustc_flags(mangler, symbol_table_passes) + get_config("--rmc-flags").split()
+    rustc_path = get_config("--rmc-path").strip()
     build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)]
+    if build_target:
+        build_cmd += ["--target", str(build_target)]
     build_env = {"RUSTFLAGS": " ".join(rustflags),
-                 "RUSTC": RMC_RUSTC_EXE,
+                 "RUSTC": rustc_path,
                  "PATH": os.environ["PATH"]
                  }
     if debug:
@@ -204,6 +228,7 @@ def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry
         build_cmd.append("-v")
     if dry_run:
         print("{}".format(build_env))
+
     return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run)
 
 # Adds information about unwinding to the RMC output

src/test/cargo-rmc/.gitignore

@@ -1 +1,2 @@
+target/
 Cargo.lock

src/test/cargo-rmc/dependencies/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "foo"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+memchr = { version = "2", default-features = false }
+rand = "0.8.4"

src/test/cargo-rmc/dependencies/check_dummy.expected

@@ -0,0 +1 @@
+[check_dummy.assertion.1] line 8 assertion failed: x > 2: SUCCESS

src/test/cargo-rmc/dependencies/src/lib.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[no_mangle]
+pub fn check_dummy() {
+    let x = rmc::nondet::<u8>();
+    rmc::assume(x > 10);
+    assert!(x > 2);
+}