Move 1 rust-test to compiletest.

scripts/rmc-regression.sh

@@ -38,3 +38,4 @@ popd
 
 # run-make tests
 ./x.py test -i --stage 1 src/test/run-make --test-args gotoc
+./x.py test -i --stage 1 src/test/cbmc

src/bootstrap/bootstrap.py

@@ -1171,6 +1171,7 @@ def bootstrap(help_triggered):
     env["BOOTSTRAP_PARENT_ID"] = str(os.getpid())
     env["BOOTSTRAP_PYTHON"] = sys.executable
     env["BUILD_DIR"] = build.build_dir
+    env["RMC_DIR"] = os.path.join(build.rust_root, 'scripts')
     env["RUSTC_BOOTSTRAP"] = '1'
     if toml_path:
         env["BOOTSTRAP_CONFIG"] = toml_path

src/bootstrap/builder.rs

@@ -436,6 +436,7 @@ impl<'a> Builder<'a> {
                 test::Bootstrap,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
+                test::CBMC,
             ),
             Kind::Bench => describe!(test::Crate, test::CrateLibrustc),
             Kind::Doc => describe!(

src/bootstrap/test.rs

@@ -1121,6 +1121,8 @@ host_test!(RunMakeFullDeps {
 
 default_test!(Assembly { path: "src/test/assembly", mode: "assembly", suite: "assembly" });
 
+default_test!(CBMC { path: "src/test/cbmc", mode: "rmc", suite: "cbmc" });
+
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 struct Compiletest {
     compiler: Compiler,
@@ -1212,6 +1214,12 @@ note: if you're sure you want to do this, please open an issue as to why. In the
         cmd.arg("--run-lib-path").arg(builder.sysroot_libdir(compiler, target));
         cmd.arg("--rustc-path").arg(builder.rustc(compiler));
 
+        // Pass the path to the RMC script directory as an option to compiletest.
+        if let Ok(path) = env::var("RMC_DIR") {
+            cmd.arg("--rmc-dir-path")
+                .arg(Path::new(&path).components().collect::<PathBuf>().to_str().unwrap());
+        }
+
         let is_rustdoc = suite.ends_with("rustdoc-ui") || suite.ends_with("rustdoc-js");
 
         // Avoid depending on rustdoc when we don't need it.

src/tools/compiletest/src/common.rs

@@ -23,6 +23,7 @@ pub enum Mode {
     JsDocTest,
     MirOpt,
     Assembly,
+    RMC,
 }
 
 impl Mode {
@@ -53,6 +54,7 @@ impl FromStr for Mode {
             "js-doc-test" => Ok(JsDocTest),
             "mir-opt" => Ok(MirOpt),
             "assembly" => Ok(Assembly),
+            "rmc" => Ok(RMC),
             _ => Err(()),
         }
     }
@@ -74,6 +76,7 @@ impl fmt::Display for Mode {
             JsDocTest => "js-doc-test",
             MirOpt => "mir-opt",
             Assembly => "assembly",
+            RMC => "rmc",
         };
         fmt::Display::fmt(s, f)
     }
@@ -192,6 +195,9 @@ pub struct Config {
     /// The rustc executable.
     pub rustc_path: PathBuf,
 
+    /// The path to the directory where the RMC executable is located
+    pub rmc_dir_path: PathBuf,
+
     /// The rustdoc executable.
     pub rustdoc_path: Option<PathBuf>,
 

src/tools/compiletest/src/main.rs

@@ -58,6 +58,7 @@ pub fn parse_config(args: Vec<String>) -> Config {
     opts.reqopt("", "compile-lib-path", "path to host shared libraries", "PATH")
         .reqopt("", "run-lib-path", "path to target shared libraries", "PATH")
         .reqopt("", "rustc-path", "path to rustc to use for compiling", "PATH")
+        .reqopt("", "rmc-dir-path", "path to directory where rmc is located", "PATH")
         .optopt("", "rustdoc-path", "path to rustdoc to use for compiling", "PATH")
         .optopt("", "rust-demangler-path", "path to rust-demangler to use in tests", "PATH")
         .reqopt("", "lldb-python", "path to python to use for doc tests", "PATH")
@@ -75,7 +76,7 @@ pub fn parse_config(args: Vec<String>) -> Config {
             "mode",
             "which sort of compile tests to run",
             "run-pass-valgrind | pretty | debug-info | codegen | rustdoc \
-            | rustdoc-json | codegen-units | incremental | run-make | ui | js-doc-test | mir-opt | assembly",
+            | rustdoc-json | codegen-units | incremental | run-make | ui | js-doc-test | mir-opt | assembly | rmc",
         )
         .reqopt(
             "",
@@ -215,6 +216,7 @@ pub fn parse_config(args: Vec<String>) -> Config {
         compile_lib_path: make_absolute(opt_path(matches, "compile-lib-path")),
         run_lib_path: make_absolute(opt_path(matches, "run-lib-path")),
         rustc_path: opt_path(matches, "rustc-path"),
+        rmc_dir_path: opt_path(matches, "rmc-dir-path"),
         rustdoc_path: matches.opt_str("rustdoc-path").map(PathBuf::from),
         rust_demangler_path: matches.opt_str("rust-demangler-path").map(PathBuf::from),
         lldb_python: matches.opt_str("lldb-python").unwrap(),

src/tools/compiletest/src/runtest.rs

@@ -2,7 +2,7 @@
 
 use crate::common::{expected_output_path, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT};
 use crate::common::{output_base_dir, output_base_name, output_testname_unique};
-use crate::common::{Assembly, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui};
+use crate::common::{Assembly, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui, RMC};
 use crate::common::{Codegen, CodegenUnits, DebugInfo, Debugger, Rustdoc};
 use crate::common::{CompareMode, FailMode, PassMode};
 use crate::common::{Config, TestPaths};
@@ -351,6 +351,7 @@ impl<'test> TestCx<'test> {
             MirOpt => self.run_mir_opt_test(),
             Assembly => self.run_assembly_test(),
             JsDocTest => self.run_js_doc_test(),
+            RMC => self.run_rmc_test(),
         }
     }
 
@@ -2009,7 +2010,7 @@ impl<'test> TestCx<'test> {
                 rustc.arg(dir_opt);
             }
             RunPassValgrind | Pretty | DebugInfo | Codegen | Rustdoc | RustdocJson | RunMake
-            | CodegenUnits | JsDocTest | Assembly => {
+            | CodegenUnits | JsDocTest | Assembly | RMC => {
                 // do not use JSON output
             }
         }
@@ -2369,6 +2370,34 @@ impl<'test> TestCx<'test> {
         }
     }
 
+    /// Adds rmc scripts directory to the `PATH` environment variable.
+    fn add_rmc_dir_to_path(&self, rmc: &mut Command) {
+        // If the PATH enviornment variable is already defined,
+        if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") {
+            // Add the RMC scripts directory to the PATH.
+            rmc.env(key, format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val));
+        } else {
+            // Otherwise, insert PATH as a new enviornment variable and set its value to the RMC scripts directory.
+            rmc.env(String::from("PATH"), String::from(self.config.rmc_dir_path.to_str().unwrap()));
+        }
+    }
+
+    /// Runs RMC on the test file specified by `self.testpaths.file`.
+    /// An error message is printed to stdout if verfication fails.
+    fn run_rmc_test(&self) {
+        // Other modes call self.compile_test(...). However, we cannot call it here for two reasons:
+        // 1. It calls rustc instead of RMC
+        // 2. It may pass some options that do not make sense for RMC
+        // So we create our own command to execute RMC and pass it to self.compose_and_run_compiler(...) directly.
+        let mut rmc = Command::new("rmc");
+        self.add_rmc_dir_to_path(&mut rmc);
+        rmc.arg(&self.testpaths.file);
+        let proc_res = self.compose_and_run_compiler(rmc, None);
+        if !proc_res.status.success() {
+            self.fatal_proc_rec("verification failed!", &proc_res);
+        }
+    }
+
     fn charset() -> &'static str {
         // FreeBSD 10.1 defaults to GDB 6.1.1 which doesn't support "auto" charset
         if cfg!(target_os = "freebsd") { "ISO-8859-1" } else { "UTF-8" }