Move all tests under rust-tests to compiletest.

scripts/rmc-regression.sh

@@ -23,19 +23,14 @@ check-cbmc-version.py --major 5 --minor 30
 # Standalone rmc tests
 pushd $RUST_DIR
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
-cd rust-tests
-for TEST_DIR in cbmc-reg smack-regressions prusti-regressions; do
-    ./run.sh $TEST_DIR
-done
-./run.sh firecracker-like 2
+./x.py test -i --stage 1 cbmc firecracker prusti smack
 
 # Standalone cargo-rmc tests
-cd ../cargo-rmc-tests
+cd cargo-rmc-tests
 for DIR in */; do
   ./run.py $DIR
 done
 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/builder.rs

@@ -434,9 +434,14 @@ impl<'a> Builder<'a> {
                 test::RustdocJson,
                 // Run bootstrap close to the end as it's unlikely to fail
                 test::Bootstrap,
+                // RMC regression tests
+                test::CBMC,
+                test::Firecracker,
+                test::Prusti,
+                test::Serial,
+                test::SMACK,
                 // 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

@@ -1123,6 +1123,14 @@ default_test!(Assembly { path: "src/test/assembly", mode: "assembly", suite: "as
 
 default_test!(CBMC { path: "src/test/cbmc", mode: "rmc", suite: "cbmc" });
 
+default_test!(Firecracker { path: "src/test/firecracker", mode: "rmc", suite: "firecracker" });
+
+default_test!(Prusti { path: "src/test/prusti", mode: "rmc", suite: "prusti" });
+
+default_test!(Serial { path: "src/test/serial", mode: "rmc", suite: "serial" });
+
+default_test!(SMACK { path: "src/test/smack", mode: "rmc", suite: "smack" });
+
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 struct Compiletest {
     compiler: Compiler,

rust-tests/cbmc-reg/Count/Unstable/Ctlz/bounds_fail.rs → src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs

@@ -1,9 +1,11 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --bounds-check
+
 #![feature(core_intrinsics)]
 use std::intrinsics::ctlz_nonzero;
 
-/// rmc bounds_fail.rs -- --bounds-check
 fn main() {
     let uv8: u8 = 0;
     let uv16: u16 = 0;

rust-tests/cbmc-reg/Count/Unstable/Cttz/bounds_fail.rs → src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs

@@ -1,9 +1,11 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --bounds-check
+
 #![feature(core_intrinsics)]
 use std::intrinsics::cttz_nonzero;
 
-/// rmc bounds_fail.rs -- --bounds-check
 fn main() {
     let uv8: u8 = 0;
     let uv16: u16 = 0;

rust-tests/cbmc-reg/FunctionCall_Ret-Param/main.rs → src/test/cbmc/FunctionCall_Ret-Param/main.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 10
+
 fn __nondet<T>() -> T {
     unimplemented!()
 }

rust-tests/cbmc-reg/LoopLoop_NonReturning/main.rs → src/test/cbmc/LoopLoop_NonReturning/main.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 10 --unwinding-assertions
+
 fn __nondet<T>() -> T {
     unimplemented!()
 }

rust-tests/cbmc-reg/LoopWhile_NonReturning/main.rs → src/test/cbmc/LoopWhile_NonReturning/main.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 11 --unwinding-assertions
+
 fn __nondet<T>() -> T {
     unimplemented!()
 }

rust-tests/cbmc-reg/Slice/main.rs → src/test/cbmc/Slice/main.rs

@@ -1,6 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-/// rmc main.rs -- --unwind 6 --unwinding-assertions
+
+// cbmc-flags: --unwind 6 --unwinding-assertions
+
 fn main() {
     let name: &str = "hello";
     assert!(name == "hello");

rust-tests/cbmc-reg/SwitchInt/main.rs → src/test/cbmc/SwitchInt/main.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 2 --unwinding-assertions
+
 fn doswitch_int() -> i32 {
     for i in [99].iter() {
         if *i == 99 {

rust-tests/cbmc-reg/Whitespace/main.rs → src/test/cbmc/Whitespace/main.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 2 --unwinding-assertions
+
 fn main() {
     let mut iter = "A few words".split_whitespace();
     match iter.next() {

rust-tests/prusti-regressions/Binary_search_fail.rs → src/test/prusti/Binary_search_fail.rs

@@ -1,5 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 4 --unwinding-assertions
+
 use std::cmp::Ordering::*;
 
 /// this is interestingly a wrong implementation at

rust-tests/smack-regressions/loops/gauss_sum_nondet.rs → src/test/smack/loops/gauss_sum_nondet.rs

@@ -3,6 +3,8 @@
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
 
+// cbmc-flags: --unwind 5 --unwinding-assertions
+
 fn __nondet<T>() -> T {
     unimplemented!()
 }

rust-tests/smack-regressions/loops/gauss_sum_nondet_fail.rs → src/test/smack/loops/gauss_sum_nondet_fail.rs

@@ -3,6 +3,8 @@
 // @flag --no-memory-splitting --unroll=10
 // @expect error
 
+// cbmc-flags: --unwind 5 --unwinding-assertions
+
 fn __nondet<T>() -> T {
     unimplemented!()
 }

rust-tests/smack-regressions/loops/iterator.rs → src/test/smack/loops/iterator.rs

@@ -3,6 +3,8 @@
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
 
+// cbmc-flags: --unwind 5 --unwinding-assertions
+
 fn fac(n: u64) -> u64 {
     match n {
         0 => 1,

rust-tests/smack-regressions/loops/iterator_fail.rs → src/test/smack/loops/iterator_fail.rs

@@ -3,6 +3,8 @@
 // @flag --no-memory-splitting --unroll=10
 // @expect error
 
+// cbmc-flags: --unwind 5 --unwinding-assertions
+
 fn fac(n: u64) -> u64 {
     match n {
         0 => 1,

src/tools/compiletest/src/header.rs

@@ -51,6 +51,14 @@ impl EarlyProps {
         let has_tsan = util::TSAN_SUPPORTED_TARGETS.contains(&&*config.target);
         let has_hwasan = util::HWASAN_SUPPORTED_TARGETS.contains(&&*config.target);
 
+        if config.mode == Mode::RMC {
+            // If the path to the test contains "fixme" or "ignore", skip it.
+            let path = testfile.to_str().unwrap();
+            if path.contains("fixme") || path.contains("ignore") {
+                props.ignore = true;
+            }
+        }
+
         iter_header(testfile, None, rdr, &mut |ln| {
             // we should check if any only-<platform> exists and if it exists
             // and does not matches the current platform, skip the test
@@ -277,6 +285,10 @@ pub struct TestProps {
     pub error_patterns: Vec<String>,
     // Extra flags to pass to the compiler
     pub compile_flags: Vec<String>,
+    // Extra flags to pass to RMC
+    pub rmc_flags: Vec<String>,
+    // Extra flags to pass to CBMC
+    pub cbmc_flags: Vec<String>,
     // Extra flags to pass when the compiled code is run (such as --bench)
     pub run_flags: Option<String>,
     // If present, the name of a file that this test should match when
@@ -360,6 +372,8 @@ impl TestProps {
         TestProps {
             error_patterns: vec![],
             compile_flags: vec![],
+            rmc_flags: vec![],
+            cbmc_flags: vec![],
             run_flags: None,
             pp_exact: None,
             aux_builds: vec![],
@@ -436,6 +450,14 @@ impl TestProps {
                     self.compile_flags.extend(flags.split_whitespace().map(|s| s.to_owned()));
                 }
 
+                if let Some(flags) = config.parse_rmc_flags(ln) {
+                    self.rmc_flags.extend(flags.split_whitespace().map(|s| s.to_owned()));
+                }
+
+                if let Some(flags) = config.parse_cbmc_flags(ln) {
+                    self.cbmc_flags.extend(flags.split_whitespace().map(|s| s.to_owned()));
+                }
+
                 if let Some(edition) = config.parse_edition(ln) {
                     self.compile_flags.push(format!("--edition={}", edition));
                 }
@@ -729,6 +751,16 @@ impl Config {
         self.parse_name_value_directive(line, "compile-flags")
     }
 
+    /// Parses strings of the form `// rmc-flags: ...` and returns the options listed after `rmc-flags:`
+    fn parse_rmc_flags(&self, line: &str) -> Option<String> {
+        self.parse_name_value_directive(line, "rmc-flags")
+    }
+
+    /// Parses strings of the form `// cbmc-flags: ...` and returns the options listed after `cbmc-flags:`
+    fn parse_cbmc_flags(&self, line: &str) -> Option<String> {
+        self.parse_name_value_directive(line, "cbmc-flags")
+    }
+
     fn parse_and_update_revisions(&self, line: &str, existing: &mut Vec<String>) {
         if let Some(raw) = self.parse_name_value_directive(line, "revisions") {
             let mut duplicates: HashSet<_> = existing.iter().cloned().collect();

src/tools/compiletest/src/runtest.rs

@@ -396,6 +396,7 @@ impl<'test> TestCx<'test> {
                     panic!("revision name must begin with rpass, rfail, or cfail");
                 }
             }
+            RMC => !self.testpaths.file.to_str().unwrap().contains("fail"),
             mode => panic!("unimplemented for mode {:?}", mode),
         }
     }
@@ -2382,19 +2383,30 @@ impl<'test> TestCx<'test> {
         }
     }
 
-    /// Runs RMC on the test file specified by `self.testpaths.file`.
-    /// An error message is printed to stdout if verfication fails.
+    /// Runs RMC on the test file specified by `self.testpaths.file`. An error
+    /// message is printed to stdout if verification result is not expected.
     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");
+        // Pass the test path along with RMC and CBMC flags parsed from comments at the top of the test file.
+        rmc.args(&self.props.rmc_flags)
+            .arg(&self.testpaths.file)
+            .arg("--")
+            .args(&self.props.cbmc_flags);
         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);
+        // Print an error if the verification result is not expected.
+        if self.should_compile_successfully(self.pass_mode()) {
+            if !proc_res.status.success() {
+                self.fatal_proc_rec("test failed: expected success, got failure", &proc_res);
+            }
+        } else {
+            if proc_res.status.success() {
+                self.fatal_proc_rec("test failed: expected failure, got success", &proc_res);
+            }
         }
     }