diff --git a/scripts/rmc-regression.sh b/scripts/rmc-regression.sh index a562f0f9fdbf..553adbb4b8d0 100755 --- a/scripts/rmc-regression.sh +++ b/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 diff --git a/src/bootstrap/bootstrap.py b/src/bootstrap/bootstrap.py index 149a899cef7a..f2565f4c8894 100644 --- a/src/bootstrap/bootstrap.py +++ b/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 diff --git a/src/bootstrap/builder.rs b/src/bootstrap/builder.rs index f3049a747579..40b93b0ab61a 100644 --- a/src/bootstrap/builder.rs +++ b/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!( diff --git a/src/bootstrap/test.rs b/src/bootstrap/test.rs index 16b3c6419e83..1a53141ecb2b 100644 --- a/src/bootstrap/test.rs +++ b/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::().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. diff --git a/rust-tests/cbmc-reg/Bool-BoolOperators/main.rs b/src/test/cbmc/Bool-BoolOperators/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Bool-BoolOperators/main.rs rename to src/test/cbmc/Bool-BoolOperators/main.rs diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs index 408c0b8da0b2..373598487902 100644 --- a/src/tools/compiletest/src/common.rs +++ b/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, diff --git a/src/tools/compiletest/src/main.rs b/src/tools/compiletest/src/main.rs index d53e19f2908e..f6c66a6a6b12 100644 --- a/src/tools/compiletest/src/main.rs +++ b/src/tools/compiletest/src/main.rs @@ -58,6 +58,7 @@ pub fn parse_config(args: Vec) -> 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) -> 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) -> 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(), diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 54b079a3e861..f3bbcd0961d9 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/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" }