Add rmc-compiler binary to drive rust compilation (rust-lang#722)

This change introduces a new compilation driver (rmc-compiler) that no longer depends on a modified version of the rust compiler, neither depends on the bootstrap script.

The rmc-compiler binary can be build using regular cargo build and can be used as a replacement to rustc with additional options that allow us to compile rust into goto-c.

Author: celinval

.github/workflows/format-check.yml

@@ -15,7 +15,7 @@ jobs:
       - name: Get paths for files added
         id: git-diff
         run: |
-          ignore='(.clang-format|.diff|.md|.props|expected|ignore|gitignore)$'
+          ignore='(.clang-format|.diff|.md|.props|expected|ignore|gitignore|Cargo.lock)$'
           files=$(git diff --ignore-submodules=all --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E $ignore | xargs)
           echo "::set-output name=paths::$files"
 

.github/workflows/rmc.yml

@@ -46,13 +46,11 @@ jobs:
           git config submodule."src/llvm-project".update none
           git submodule update --init --depth 1
 
-      - name: Build RMC
+      - name: Build RMC and RMC Library
         run: |
           export RUST_BACKTRACE=1
-          ./x.py build -i --stage 1 library/std
-
-      - name: Build RMC Library
-        run: bash -x ./scripts/setup/build_rmc_lib.sh
+          cd src/rmc-compiler
+          cargo build
 
       - name: Execute RMC regression
         run: ./scripts/rmc-regression.sh

Cargo.lock

@@ -3324,6 +3324,16 @@ dependencies = [
  "rmc_macros",
 ]
 
+[[package]]
+name = "rmc-compiler"
+version = "0.1.0"
+dependencies = [
+ "clap",
+ "rmc_queries",
+ "rustc_codegen_rmc",
+ "tracing",
+]
+
 [[package]]
 name = "rmc-link-restrictions"
 version = "0.1.0"
@@ -3338,6 +3348,13 @@ dependencies = [
 name = "rmc_macros"
 version = "0.1.0"
 
+[[package]]
+name = "rmc_queries"
+version = "0.1.0"
+dependencies = [
+ "tracing",
+]
+
 [[package]]
 name = "rmc_restrictions"
 version = "0.1.0"
@@ -3890,24 +3907,9 @@ dependencies = [
  "libc",
  "measureme 9.1.2",
  "num",
+ "rmc_queries",
  "rmc_restrictions",
  "rustc-demangle",
- "rustc_arena",
- "rustc_ast",
- "rustc_attr",
- "rustc_codegen_ssa",
- "rustc_data_structures",
- "rustc_errors",
- "rustc_fs_util",
- "rustc_hir",
- "rustc_index",
- "rustc_llvm",
- "rustc_metadata",
- "rustc_middle",
- "rustc_serialize",
- "rustc_session",
- "rustc_span",
- "rustc_target",
  "serde",
  "serde_json",
  "smallvec",
@@ -4186,7 +4188,6 @@ dependencies = [
  "rustc_borrowck",
  "rustc_builtin_macros",
  "rustc_codegen_llvm",
- "rustc_codegen_rmc",
  "rustc_codegen_ssa",
  "rustc_const_eval",
  "rustc_data_structures",

Cargo.toml

@@ -41,6 +41,7 @@ members = [
   "src/tools/html-checker",
   "src/tools/bump-stage0",
   "src/tools/lld-wrapper",
+  "src/rmc-compiler",
 ]
 
 exclude = [

compiler/rustc_codegen_rmc/Cargo.toml

@@ -31,7 +31,6 @@ rustc_data_structures = { path = "../rustc_data_structures" }
 rustc_codegen_ssa = { path = "../rustc_codegen_ssa" }
 rustc_symbol_mangling = { path = "../rustc_symbol_mangling" }
 rustc_codegen_llvm = { path = "../rustc_codegen_llvm", optional = true }
-rustc_codegen_rmc = { path = "../rustc_codegen_rmc" }
 rustc_hir = { path = "../rustc_hir" }
 rustc_metadata = { path = "../rustc_metadata" }
 rustc_const_eval = { path = "../rustc_const_eval" }

compiler/rustc_interface/Cargo.toml

@@ -764,7 +764,6 @@ fn test_debugging_options_tracking_hash() {
     tracked!(relax_elf_relocations, Some(true));
     tracked!(relro_level, Some(RelroLevel::Full));
     tracked!(remap_cwd_prefix, Some(PathBuf::from("abc")));
-    tracked!(emit_vtable_restrictions, true);
     tracked!(report_delayed_bugs, true);
     tracked!(sanitizer, SanitizerSet::ADDRESS);
     tracked!(sanitizer_memory_track_origins, 2);
@@ -776,7 +775,6 @@ fn test_debugging_options_tracking_hash() {
     tracked!(src_hash_algorithm, Some(SourceFileHashAlgorithm::Sha1));
     tracked!(stack_protector, StackProtector::All);
     tracked!(symbol_mangling_version, Some(SymbolManglingVersion::V0));
-    tracked!(symbol_table_passes, vec![String::from("identity")]);
     tracked!(teach, true);
     tracked!(thinlto, Some(true));
     tracked!(thir_unsafeck, true);

compiler/rustc_interface/src/tests.rs

@@ -254,7 +254,6 @@ pub fn get_codegen_backend(
             filename if filename.contains('.') => load_backend_from_dylib(filename.as_ref()),
             #[cfg(feature = "llvm")]
             "llvm" => rustc_codegen_llvm::LlvmCodegenBackend::new,
-            "gotoc" => rustc_codegen_rmc::GotocCodegenBackend::new,
             backend_name => get_codegen_sysroot(maybe_sysroot, backend_name),
         }
     });

compiler/rustc_interface/src/util.rs

@@ -1329,8 +1329,6 @@ options! {
         "choose which RELRO level to use"),
     remap_cwd_prefix: Option<PathBuf> = (None, parse_opt_pathbuf, [TRACKED],
         "remap paths under the current working directory to this path prefix"),
-    emit_vtable_restrictions: bool = (false, parse_bool, [TRACKED],
-        "restrict the targets of virtual table function pointer calls"),
     simulate_remapped_rust_src_base: Option<PathBuf> = (None, parse_opt_pathbuf, [TRACKED],
         "simulate the effect of remap-debuginfo = true at bootstrapping by remapping path \
         to rust's source base directory. only meant for testing purposes"),
@@ -1378,9 +1376,6 @@ options! {
     symbol_mangling_version: Option<SymbolManglingVersion> = (None,
         parse_symbol_mangling_version, [TRACKED],
         "which mangling version to use for symbol names ('legacy' (default) or 'v0')"),
-    symbol_table_passes: Vec<String> = (Vec::new(), parse_list, [TRACKED],
-        "transformations to perform to the symbol table after it has been generated. \
-        space separated"),
     teach: bool = (false, parse_bool, [TRACKED],
         "show extended diagnostic help (default: no)"),
     temps_dir: Option<String> = (None, parse_opt_string, [UNTRACKED],

compiler/rustc_session/src/options.rs

@@ -11,4 +11,4 @@ edition = "2021"
 [dependencies]
 rustc_data_structures = { path = "../../compiler/rustc_data_structures" }
 serde = {version = "1", features = ["derive"]}
-cbmc = { path = "../../compiler/cbmc" }
+cbmc = { path = "../../src/rmc-compiler/cbmc" }

library/rmc_restrictions/Cargo.toml

@@ -26,6 +26,9 @@ def main():
     if args.gen_c_runnable:
         rmc.cargo_build(args.crate, args.target_dir, args, ["gen-c"])
 
+        if args.only_codegen:
+            return 0
+
         pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
         symbol_table_jsons = glob.glob(pattern)
         rmc.ensure(len(symbol_table_jsons) > 0, f"Unexpected number of json outputs: {len(symbol_table_jsons)}")
@@ -52,6 +55,9 @@ def main():
 
     rmc.cargo_build(args.crate, args.target_dir, args)
 
+    if args.only_codegen:
+        return 0
+
     if args.build_target:
         pattern = os.path.join(args.target_dir, args.build_target, "debug", "deps", "*.symtab.json")
     else:
@@ -169,6 +175,7 @@ def parse_args():
         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())
+        config_group.add_argument("--only-codegen", action="store_true", help="RMC will only compile the crate.")
 
         exclude_flags = []
         rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)

scripts/cargo-rmc

@@ -26,9 +26,8 @@ cd $RMC_DIR/firecracker/src/devices/src/virtio/
 # Disable warnings until https://github.com/model-checking/rmc/issues/573 is fixed
 export RUSTC_LOG=error
 export RUST_BACKTRACE=1
-export RUSTFLAGS=$(${SCRIPT_DIR}/rmc-rustc --rmc-flags)
-export RUSTC=$(${SCRIPT_DIR}/rmc-rustc --rmc-path)
-cargo build --target x86_64-unknown-linux-gnu
+# RMC cannot locate Cargo.toml correctly: https://github.com/model-checking/rmc/issues/717
+cargo rmc --only-codegen --target x86_64-unknown-linux-gnu --no-config-toml
 
 echo
 echo "Finished Firecracker codegen regression successfully..."

scripts/codegen-firecracker.sh

@@ -20,13 +20,17 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Formatting check
 ./x.py fmt --check
 
-# Build RMC and RMC library
-./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
-./scripts/setup/build_rmc_lib.sh
+# Build RMC compiler and RMC library
+(cd "${RMC_DIR}/src/rmc-compiler"; cargo build)
+
+# Unit tests
+(cd src/rmc-compiler/cbmc; cargo test)
+(cd src/rmc-compiler; cargo test)
 
 # Standalone rmc tests, expected tests, and cargo tests
-./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs rmc-fixme
-./x.py test -i --stage 0 compiler/cbmc
+./x.py build -i src/tools/compiletest --stage 0
+export COMPILETEST_FORCE_STAGE0=1  # We don't care about the stage anymore. Remove this once we replace ./x.py test
+./x.py test -i --stage 0 rmc firecracker prusti smack expected cargo-rmc rmc-docs rmc-fixme
 
 # Check codegen for the standard library
 time "$SCRIPT_DIR"/std-lib-regression.sh

scripts/rmc-regression.sh

@@ -2,86 +2,54 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+
 # Usage:
-# rmc-rustc (--rmc-flags | --rmc-path)
-#   - This will print the configurations used to run rmc version of rustc.
-# rmc-rustc RUSTC_OPTIONS
-#   - This will run RUSTC with RMC flags + the given RUSTC_OPTIONS
+# RMCFLAGS="[<RMC_OPTIONS>]*" rmc-rustc --rmc-flags [<RUSTC_OPTIONS>]*
+#   - This will run rmc-compiler with RMC options provided via RMCFLAGS
+#     environment variable + the given RUSTC_OPTIONS.
+# rmc-rustc [<RMC_OPTIONS>]* [<RUSTC_OPTIONS>]*
+#   - This will run rmc-compiler with RMC options + the given RUSTC_OPTIONS
 set -eu
 
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 REPO_DIR="$(dirname $SCRIPT_DIR)"
 
 RMC_PATH=${RMC_PATH:-""}
-RMC_LIB_PATH=${RMC_LIB_PATH:-""}
 
 shopt -s nullglob
-set_rmc_path() {
-    local RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc)
+set_paths() {
+    # TODO: We should build into a specific folder.
+    local RMC_CANDIDATES=("$REPO_DIR"/target/*/rmc-compiler)
 
     if [ -z "${RMC_PATH}" ]
     then
         if [[ -z ${RMC_CANDIDATES:-""} ]] || [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]
         then
             echo "ERROR: Could not find RMC binary."
-            echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc"
+            echo "Looked for: '$REPO_DIR/target/*/rmc-compiler'"
             echo "Was RMC successfully built first?"
             exit 1
         fi
         RMC_PATH=${RMC_CANDIDATES[0]}
     fi
 }
 
-set_rmc_lib_path() {
-    if [ -z "${RMC_LIB_PATH}" ]
-    then
-        local RMC_LIB_CANDIDATES=("$REPO_DIR"/target/*/librmc.rlib)
-        if [[ -z ${RMC_LIB_CANDIDATES:-""} ]] || [[ ${#RMC_LIB_CANDIDATES[@]} -ne 1 ]]
-        then
-            echo "ERROR: Could not find RMC library."
-            echo "Looked for: \"$REPO_DIR/target/*/librmc.rlib\""
-            echo "Try running <RMC_ROOT>/scripts/setup/build_rmc_lib.sh"
-            exit 1
-        fi
-        RMC_LIB_PATH=$(dirname ${RMC_LIB_CANDIDATES[0]})
-    fi
-    # Having set RMC_LIB_PATH, find RMC_MACRO_LIB_PATH
-    local MACRO_LIB_CANDIDATE=(${RMC_LIB_PATH}/deps/librmc_macros-*)
-    if [[ ${#MACRO_LIB_CANDIDATE[@]} -ne 1 ]]
-    then
-        echo "ERROR: Could not find RMC library."
-        echo "Looked for: \"${RMC_LIB_PATH}/deps/librmc_macros-*\""
-        echo "Try running <RMC_ROOT>/scripts/setup/build_rmc_lib.sh"
-        exit 1
-    fi
-    RMC_MACRO_LIB_PATH="${MACRO_LIB_CANDIDATE[0]}"
-}
+set_paths
 
-set_rmc_path
-if [ "${1:-''}" == "--rmc-path" ]
+# Hack to enable cargo rmc
+#
+# The rmc-compiler requires the flags related to the rmc libraries to be
+# in front of the ones that control rustc.
+#
+# For cargo rmc, cargo sometimes adds flags before the custom RUSTFLAGS, hence,
+# we use a special environment variable to set RMC specific flags. These flags
+# should only be enabled if --rmc-flags is present.
+args="${*#--rmc-flags}"
+if [ "$args" != "$*" ]
 then
-    echo ${RMC_PATH}
+    FLAGS=("${RMCFLAGS} $args")
 else
-    set_rmc_lib_path
-    RMC_FLAGS="-Z codegen-backend=gotoc \
-            -C overflow-checks=on \
-            -C panic=abort \
-            -Z panic_abort_tests=yes \
-            -Z trim-diagnostic-paths=no \
-            -Z human_readable_cgu_names \
-            --cfg=rmc \
-            -Zcrate-attr=feature(register_tool) \
-            -Zcrate-attr=register_tool(rmctool) \
-            -L ${RMC_LIB_PATH} \
-            --extern rmc \
-            -L ${RMC_LIB_PATH}/deps \
-            --extern librmc_macros=${RMC_MACRO_LIB_PATH} \
-            "
-    if [ "${1:-''}" == "--rmc-flags" ]
-    then
-        echo ${RMC_FLAGS}
-    else
-        # Execute rmc
-       "${RMC_PATH}" ${RMC_FLAGS} "$@"
-    fi
+    FLAGS=("$args")
 fi
+
+"${RMC_PATH}" ${FLAGS}