Move all tests under rust-tests to compiletest. (rust-lang#168)

* Move all tests under rust-tests to compiletest.

* Remove execute permissions for a regression.

* Address concerns.

Author: bdalrhm

rust-tests/.gitignore

@@ -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

rust-tests/run.sh

@@ -462,9 +462,14 @@ impl<'a> Builder<'a> {
                 test::HtmlCheck,
                 // 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!(

scripts/rmc-regression.sh

@@ -1202,6 +1202,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,

src/bootstrap/builder.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;

src/bootstrap/test.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/ArithEqualOperators/main.rs renamed to src/test/cbmc/ArithEqualOperators/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/ArithOperators/main.rs renamed to src/test/cbmc/ArithOperators/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/Asm/main_fixme.rs renamed to src/test/cbmc/Asm/main_fixme.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/Assert/UninitValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/UninitValid/fixme_main_fail.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/Assert/ZeroValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/ZeroValid/fixme_main_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 2 --unwinding-assertions
+
 fn doswitch_int() -> i32 {
     for i in [99].iter() {
         if *i == 99 {

rust-tests/cbmc-reg/Assert/ZeroValid/main.rs renamed to src/test/cbmc/Assert/ZeroValid/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/cbmc-reg/Assume/main.rs renamed to src/test/cbmc/Assume/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 4 --unwinding-assertions
+
 use std::cmp::Ordering::*;
 
 /// this is interestingly a wrong implementation at

rust-tests/cbmc-reg/Assume/main_fail.rs renamed to src/test/cbmc/Assume/main_fail.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/cbmc-reg/Atomics/Stable/CompareExchange/main.rs renamed to src/test/cbmc/Atomics/Stable/CompareExchange/main.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/cbmc-reg/Atomics/Stable/Fence/main.rs renamed to src/test/cbmc/Atomics/Stable/Fence/main.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/cbmc-reg/Atomics/Stable/FetchAdd/main.rs renamed to src/test/cbmc/Atomics/Stable/FetchAdd/main.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,

rust-tests/cbmc-reg/Atomics/Stable/FetchAnd/main.rs renamed to src/test/cbmc/Atomics/Stable/FetchAnd/main.rs

@@ -59,6 +59,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
@@ -142,6 +146,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![],
@@ -222,6 +228,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));
                     if edition == "2021" {
@@ -512,6 +526,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();
@@ -852,6 +876,13 @@ pub fn make_test_description<R: Read>(
         .join("gcc-ld")
         .join(if config.host.contains("windows") { "ld.exe" } else { "ld" })
         .exists();
+
+    if config.mode == Mode::RMC {
+        // If the path to the test contains "fixme" or "ignore", skip it.
+        let file_path = path.to_str().unwrap();
+        ignore |= file_path.contains("fixme") || file_path.contains("ignore");
+    }
+
     iter_header(path, src, &mut |revision, ln| {
         if revision.is_some() && revision != cfg {
             return;

rust-tests/cbmc-reg/Atomics/Stable/FetchOr/main.rs renamed to src/test/cbmc/Atomics/Stable/FetchOr/main.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),
         }
     }
@@ -2398,19 +2399,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);
+            }
         }
     }