Create an RMC crate and load it as part of rmc-rustc (rust-lang#597)

* Adding support to new rmc prelude definitions

- Create an rmc crate (rust-lang#231).
- Used rust compliant names for the functions (rust-lang#589).
- Changed rmc-rustc to inject the rmc prelude as part of the compilation
  as well as other rmc configuration flags.
- Added options to rmc-rustc to print binary path and flags so it can be
  used in other scripts.

* Add a script to build rmc library

* Update tests to use new injected prelude.

Author: celinval

.github/workflows/rmc.yml

@@ -51,10 +51,12 @@ jobs:
           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
+
       - name: Execute RMC regression
         run: ./scripts/rmc-regression.sh
 
-
       - name: Install dashboard dependencies
         if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
         run: ./scripts/setup/install_dashboard_deps.sh

Cargo.lock

@@ -3310,6 +3310,10 @@ dependencies = [
  "rls-span",
 ]
 
+[[package]]
+name = "rmc"
+version = "0.1.0"
+
 [[package]]
 name = "rust-demangler"
 version = "0.0.1"

Cargo.toml

@@ -4,6 +4,7 @@ members = [
   "compiler/rustc",
   "library/std",
   "library/test",
+  "library/rmc",
   "src/rustdoc-json-types",
   "src/tools/cargotest",
   "src/tools/clippy",
@@ -55,7 +56,9 @@ exclude = [
   # stdarch has its own Cargo workspace
   "library/stdarch",
   # dependency tests have their own workspace
-  "src/test/rmc-dependency-test/dependency3"
+  "src/test/rmc-dependency-test/dependency3",
+  # cargo rmc tests should also have their own workspace
+  "src/test/cargo-rmc"
 ]
 
 [profile.release.package.compiler_builtins]

compiler/rustc_codegen_rmc/src/overrides/hooks.rs

@@ -12,14 +12,13 @@ use super::stubs::{HashMapStub, VecStub};
 use crate::utils::{instance_name_is, instance_name_starts_with};
 use crate::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
-use rustc_hir::definitions::DefPathDataName;
 use rustc_middle::mir::{BasicBlock, Place};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt};
 use rustc_span::Span;
 use std::rc::Rc;
-use tracing::debug;
+use tracing::{debug, warn};
 
 pub trait GotocTypeHook<'tcx> {
     fn hook_applies(&self, tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool;
@@ -66,19 +65,29 @@ fn output_of_instance_is_never<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>
     }
 }
 
+fn matches_function(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>, attr_name: &str) -> bool {
+    let attr_sym = rustc_span::symbol::Symbol::intern(attr_name);
+    if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) {
+        if instance.def.def_id() == *attr_id {
+            debug!("matched: {:?} {:?}", attr_id, attr_sym);
+            return true;
+        }
+    }
+    false
+}
+
 struct ExpectFail;
 impl<'tcx> GotocHook<'tcx> for ExpectFail {
     fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
-        let def_path = tcx.def_path(instance.def.def_id());
-        if let Some(data) = def_path.data.last() {
-            match data.data.name() {
-                DefPathDataName::Named(name) => {
-                    return name.to_string().starts_with("__VERIFIER_expect_fail");
-                }
-                DefPathDataName::Anon { .. } => (),
-            }
+        // Deprecate old __VERIFIER notation that doesn't respect rust naming conventions.
+        // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599
+        if instance_name_starts_with(tcx, instance, "__VERIFIER_expect_fail") {
+            warn!(
+                "The function __VERIFIER_expect_fail is deprecated. Use rmc::expect_fail instead"
+            );
+            return true;
         }
-        false
+        matches_function(tcx, instance, "RmcExpectFail")
     }
 
     fn handle(
@@ -109,16 +118,13 @@ impl<'tcx> GotocHook<'tcx> for ExpectFail {
 struct Assume;
 impl<'tcx> GotocHook<'tcx> for Assume {
     fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
-        let def_path = tcx.def_path(instance.def.def_id());
-        if let Some(data) = def_path.data.last() {
-            match data.data.name() {
-                DefPathDataName::Named(name) => {
-                    return name.to_string().starts_with("__VERIFIER_assume");
-                }
-                DefPathDataName::Anon { .. } => (),
-            }
+        // Deprecate old __VERIFIER notation that doesn't respect rust naming conventions.
+        // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599
+        if instance_name_starts_with(tcx, instance, "__VERIFIER_assume") {
+            warn!("The function __VERIFIER_assume is deprecated. Use rmc::assume instead");
+            return true;
         }
-        false
+        matches_function(tcx, instance, "RmcAssume")
     }
 
     fn handle(
@@ -149,7 +155,13 @@ struct Nondet;
 
 impl<'tcx> GotocHook<'tcx> for Nondet {
     fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
-        instance_name_starts_with(tcx, instance, "__nondet")
+        // Deprecate old __nondet since it doesn't match rust naming conventions.
+        // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599
+        if instance_name_starts_with(tcx, instance, "__nondet") {
+            warn!("The function __nondet is deprecated. Use rmc::nondet instead");
+            return true;
+        }
+        matches_function(tcx, instance, "RmcNonDet")
     }
 
     fn handle(

compiler/rustc_codegen_rmc/src/overrides/mod.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! This module provides a mechanism which RMC can use to override standard codegen.
-//! For example, we the RMC provides pseudo-functions, such as __VERIFIER_assume().
+//! For example, we the RMC provides pseudo-functions, such as rmc::assume().
 //! These functions should not be codegenned as MIR.
 //! Instead, we use a "hook" to generate the correct CBMC intrinsic.
 

library/rmc/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "rmc"
+version = "0.1.0"
+edition = "2018"
+license = "MIT OR Apache-2.0"
+
+[dependencies]

library/rmc/src/lib.rs

@@ -0,0 +1,53 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(rustc_attrs)] // Used for rustc_diagnostic_item.
+
+/// Creates an assumption that will be valid after this statement run. Note that the assumption
+/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
+/// program will exit successfully.
+///
+/// # Example:
+///
+/// The code snippet below should never panic.
+///
+/// ```rust
+/// let i : i32 = rmc::nondet();
+/// rmc::assume(i > 10);
+/// if i < 0 {
+///   panic!("This will never panic");
+/// }
+/// ```
+///
+/// The following code may panic though:
+///
+/// ```rust
+/// let i : i32 = rmc::nondet();
+/// assert!(i < 0, "This may panic and verification should fail.");
+/// rmc::assume(i > 10);
+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "RmcAssume"]
+pub fn assume(_cond: bool) {}
+
+/// This creates an unconstrained value of type `T`. You can assign the return value of this
+/// function to a variable that you want to make symbolic.
+///
+/// # Example:
+///
+/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
+/// under all possible i32 input values.
+///
+/// ```rust
+/// let inputA = rmc::nondet::<i32>();
+/// fn_under_verification(inputA);
+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "RmcNonDet"]
+pub fn nondet<T>() -> T {
+    unimplemented!("RMC nondet")
+}
+
+/// Function used in tests for cases where the condition is not always true.
+#[inline(never)]
+#[rustc_diagnostic_item = "RmcExpectFail"]
+pub fn expect_fail(_cond: bool, _message: &str) {}

scripts/codegen-firecracker.sh

@@ -24,7 +24,11 @@ echo
 # At the moment, we only test codegen for the virtio module
 cd $RMC_DIR/firecracker/src/devices/src/virtio/
 # Disable warnings until https://github.com/model-checking/rmc/issues/573 is fixed
-RUSTC_LOG=error RUST_BACKTRACE=1 RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo build --target x86_64-unknown-linux-gnu
+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
 
 echo
 echo "Finished Firecracker codegen regression successfully..."

scripts/rmc-rustc

@@ -2,19 +2,62 @@
 # 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
 set -eu
 
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 REPO_DIR="$(dirname $SCRIPT_DIR)"
 
-shopt -s nullglob
-RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc)
+get_rmc_path() {
+    shopt -s nullglob
+    RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc)
 
-if [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]; then
-    echo "ERROR: Could not find RMC binary."
-    echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc"
-    echo "Was RMC successfully built first?"
-    exit 1
-fi
+    if [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]; then
+        echo "ERROR: Could not find RMC binary."
+        echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc"
+        echo "Was RMC successfully built first?"
+        exit 1
+    fi
+    echo ${RMC_CANDIDATES[0]}
+}
+
+get_rmc_lib_path() {
+    if [ -z "${RMC_LIB_PATH:-""}" ]
+    then
+        RMC_LIB_CANDIDATES=("$REPO_DIR"/target/*/librmc.rlib)
+        if [[ ${#RMC_LIB_CANDIDATES[@]} -ne 1 ]]; then
+            echo "ERROR: Could not find RMC library."
+            echo "Looked for: \"$REPO_DIR/target/*/librmc.rlib\""
+            echo "Was RMC library successfully built first?"
+            exit 1
+        fi
+        echo $(dirname ${RMC_LIB_CANDIDATES[0]})
+    else
+        echo ${RMC_LIB_PATH}
+    fi
+}
+
+RMC_PATH=$(get_rmc_path)
 
-"${RMC_CANDIDATES[0]}" "$@"
+RMC_FLAGS="--crate-type=lib \
+        -Z codegen-backend=gotoc \
+        -Z trim-diagnostic-paths=no \
+        -Z human_readable_cgu_names \
+        --cfg=rmc \
+        -L $(get_rmc_lib_path) \
+        --extern rmc"
+
+if [ "${1:-''}" == "--rmc-flags" ]
+then
+    echo ${RMC_FLAGS}
+elif [ "${1:-''}" == "--rmc-path" ]
+then
+    echo ${RMC_PATH}
+else
+    # Execute rmc
+   "${RMC_PATH}" ${RMC_FLAGS} "$@"
+fi

scripts/rmc.py

@@ -149,12 +149,9 @@ def run_cmd(
 
 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
@@ -176,7 +173,7 @@ def compile_single_rust_file(
         atexit.register(delete_file, output_filename)
         atexit.register(delete_file, base + ".type_map.json")
 
-    build_cmd = [RMC_RUSTC_EXE, "--crate-type=lib"] + rustc_flags(mangler, symbol_table_passes)
+    build_cmd = [RMC_RUSTC_EXE] + rustc_flags(mangler, symbol_table_passes)
 
     if use_abs:
         build_cmd += ["-Z", "force-unstable-if-unmarked=yes",
@@ -199,10 +196,14 @@ def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry
     build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)]
     build_env = {"RUSTFLAGS": " ".join(rustflags),
                  "RUSTC": RMC_RUSTC_EXE,
-                 "PATH": os.environ["PATH"],
+                 "PATH": os.environ["PATH"]
                  }
     if debug:
         add_rmc_rustc_debug_to_env(build_env)
+    if verbose:
+        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

scripts/setup/build_rmc_lib.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -o errexit
+set -o nounset
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+SCRIPTS_DIR="$(dirname $SCRIPT_DIR)"
+REPO_DIR="$(dirname $SCRIPTS_DIR)"
+
+export RUSTC=$(${SCRIPTS_DIR}/rmc-rustc --rmc-path)
+cargo build --manifest-path "${REPO_DIR}/library/rmc/Cargo.toml" $@
+

scripts/std-lib-regression.sh

@@ -40,16 +40,17 @@ fi
 STD_LIB_LOG="/tmp/StdLibTest/log.txt"
 
 echo "Starting cargo build with RMC"
-RUSTC_LOG=error \
-  RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" \
-  RUSTC=rmc-rustc cargo +nightly build -Z build-std --target $TARGET 2>&1 \
+export RUSTC_LOG=error
+export RUSTFLAGS=$(${SCRIPT_DIR}/rmc-rustc --rmc-flags)
+export RUSTC=$(${SCRIPT_DIR}/rmc-rustc --rmc-path)
+cargo +nightly build -Z build-std --target $TARGET 2>&1 \
   | tee $STD_LIB_LOG
 
 # For now, we expect a linker error, but no modules should fail with a compiler
-# panic. 
+# panic.
 #
 # With https://github.com/model-checking/rmc/issues/109, this check can be
-# removed to just allow the success of the previous line to determine the 
+# removed to just allow the success of the previous line to determine the
 # success of this script (with no $STD_LIB_LOG needed)
 
 # TODO: this check is insufficient if the failure is before codegen

src/test/benchmarks/Vector/append.rs

@@ -9,11 +9,11 @@ include!{"../benchmark-prelude.rs"}
 fn operate_on_vec(times: usize) {
     let mut v: Vec<u32> = Vec::with_capacity(times);
     for i in 0..times {
-        v.push(__nondet());
+        v.push(rmc::nondet());
     }
     let mut v2: Vec<u32> = Vec::with_capacity(times);
     for i in 0..times {
-        v2.push(__nondet());
+        v2.push(rmc::nondet());
     }
     v.append(&mut v2);
     assert!(v.len() == times * 2);