From 75a975d82972028c9c0274347b8064a4f5b953e3 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Tue, 1 Jun 2021 14:07:09 +0000 Subject: [PATCH 1/3] Copy 1 rust-test to compiletest. --- scripts/rmc-regression.sh | 1 + src/bootstrap/bootstrap.py | 1 + src/bootstrap/builder.rs | 1 + src/bootstrap/test.rs | 8 +++++ src/test/cbmc/Closure/main.rs | 47 ++++++++++++++++++++++++++++ src/tools/compiletest/src/common.rs | 6 ++++ src/tools/compiletest/src/main.rs | 4 ++- src/tools/compiletest/src/runtest.rs | 30 ++++++++++++++++-- 8 files changed, 95 insertions(+), 3 deletions(-) create mode 100644 src/test/cbmc/Closure/main.rs diff --git a/scripts/rmc-regression.sh b/scripts/rmc-regression.sh index 2ce03a7ba20c..6ffb13029fc1 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..7a87f15f6527 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/src/test/cbmc/Closure/main.rs b/src/test/cbmc/Closure/main.rs new file mode 100644 index 000000000000..4826b716c2d8 --- /dev/null +++ b/src/test/cbmc/Closure/main.rs @@ -0,0 +1,47 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! test that we implement closures correctly + +fn closure_with_empty_args() { + let bytes = vec![0]; + let b = bytes.get(0).ok_or_else(|| ()).unwrap(); + assert!(*b == 0); +} + +fn closure_with_1_arg() { + let b = Some(3); + let r = b.map(|x| x + 1); + assert!(r == Some(4)); +} + +fn takes_unit_args i32>(f: F) -> i32 { + f(1, (), 3) +} + +fn test_unit_args() { + let r = takes_unit_args(|a, _b, c| a + c); + assert!(r == 4); +} + +fn takes_three_args i32>(f: F) -> i32 { + f(1, 2, 3) +} + +fn test_three_args() { + let r = takes_three_args(|a, b, c| a + b + c); + assert!(r == 6); +} + +fn test_env() { + let x = 3; + let r = takes_three_args(|a, b, c| a + b + c + x); + assert!(r == 9); +} + +fn main() { + closure_with_empty_args(); + closure_with_1_arg(); + test_three_args(); + test_unit_args(); + test_env(); +} 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..9777300e88c5 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(), } } @@ -1791,6 +1792,22 @@ impl<'test> TestCx<'test> { fn compose_and_run_compiler(&self, mut rustc: Command, input: Option) -> ProcRes { let aux_dir = self.build_all_auxiliary(&mut rustc); + + if (self.config.mode == RMC) { + // add the RMC scripts directory to the PATH environment variable + if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") { + rustc.env( + String::from("PATH"), + format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val), + ); + } else { + rustc.env( + String::from("PATH"), + String::from(self.config.rmc_dir_path.to_str().unwrap()), + ); + } + } + self.props.unset_rustc_env.clone().iter().fold(&mut rustc, |rustc, v| rustc.env_remove(v)); rustc.envs(self.props.rustc_env.clone()); self.compose_and_run( @@ -2009,7 +2026,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 +2386,15 @@ impl<'test> TestCx<'test> { } } + fn run_rmc_test(&self) { + let mut rmc = Command::new("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("compilation 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" } From 09ebedb29511469288f30ed7d8b04f95ae0cc76b Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Wed, 2 Jun 2021 17:28:20 +0000 Subject: [PATCH 2/3] Add comments and address other concerns. --- src/bootstrap/test.rs | 2 +- .../test/cbmc}/Bool-BoolOperators/main.rs | 0 src/test/cbmc/Closure/main.rs | 47 ------------------- src/tools/compiletest/src/runtest.rs | 36 +++++++------- 4 files changed, 20 insertions(+), 65 deletions(-) rename {rust-tests/cbmc-reg => src/test/cbmc}/Bool-BoolOperators/main.rs (100%) delete mode 100644 src/test/cbmc/Closure/main.rs diff --git a/src/bootstrap/test.rs b/src/bootstrap/test.rs index 7a87f15f6527..1a53141ecb2b 100644 --- a/src/bootstrap/test.rs +++ b/src/bootstrap/test.rs @@ -1214,7 +1214,7 @@ 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 + // 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()); 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/test/cbmc/Closure/main.rs b/src/test/cbmc/Closure/main.rs deleted file mode 100644 index 4826b716c2d8..000000000000 --- a/src/test/cbmc/Closure/main.rs +++ /dev/null @@ -1,47 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! test that we implement closures correctly - -fn closure_with_empty_args() { - let bytes = vec![0]; - let b = bytes.get(0).ok_or_else(|| ()).unwrap(); - assert!(*b == 0); -} - -fn closure_with_1_arg() { - let b = Some(3); - let r = b.map(|x| x + 1); - assert!(r == Some(4)); -} - -fn takes_unit_args i32>(f: F) -> i32 { - f(1, (), 3) -} - -fn test_unit_args() { - let r = takes_unit_args(|a, _b, c| a + c); - assert!(r == 4); -} - -fn takes_three_args i32>(f: F) -> i32 { - f(1, 2, 3) -} - -fn test_three_args() { - let r = takes_three_args(|a, b, c| a + b + c); - assert!(r == 6); -} - -fn test_env() { - let x = 3; - let r = takes_three_args(|a, b, c| a + b + c + x); - assert!(r == 9); -} - -fn main() { - closure_with_empty_args(); - closure_with_1_arg(); - test_three_args(); - test_unit_args(); - test_env(); -} diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 9777300e88c5..3dce211c4b4e 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -1792,22 +1792,6 @@ impl<'test> TestCx<'test> { fn compose_and_run_compiler(&self, mut rustc: Command, input: Option) -> ProcRes { let aux_dir = self.build_all_auxiliary(&mut rustc); - - if (self.config.mode == RMC) { - // add the RMC scripts directory to the PATH environment variable - if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") { - rustc.env( - String::from("PATH"), - format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val), - ); - } else { - rustc.env( - String::from("PATH"), - String::from(self.config.rmc_dir_path.to_str().unwrap()), - ); - } - } - self.props.unset_rustc_env.clone().iter().fold(&mut rustc, |rustc, v| rustc.env_remove(v)); rustc.envs(self.props.rustc_env.clone()); self.compose_and_run( @@ -2386,12 +2370,30 @@ 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 model checker on the test file specified by `self.testpaths.file`. A "verification failed!" error is printed to the 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, and + // 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("compilation failed!", &proc_res); + self.fatal_proc_rec("verification failed!", &proc_res); } } From b709fc46b49d1fc6cb9b2155e2cdc6fda338a4b9 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Wed, 2 Jun 2021 18:01:21 +0000 Subject: [PATCH 3/3] Modify comments. --- src/tools/compiletest/src/runtest.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 3dce211c4b4e..f3bbcd0961d9 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2382,12 +2382,13 @@ impl<'test> TestCx<'test> { } } - /// Runs rmc model checker on the test file specified by `self.testpaths.file`. A "verification failed!" error is printed to the stdout if verfication fails. + /// 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, and - // 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. + // 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);