Move cargo tests to compiletest.

scripts/cargo-rmc

@@ -6,6 +6,7 @@ import argparse
 import glob
 import sys
 import rmc
+import os
 
 
 EXIT_CODE_SUCCESS = 0
@@ -25,6 +26,8 @@ def main():
     parser.add_argument("--mangler", default="v0")
     parser.add_argument("--visualize", action="store_true")
     parser.add_argument("--srcdir", default=".")
+    parser.add_argument("--target-dir", default="target",
+                        help="Directory for all generated artifacts")
     parser.add_argument("--wkdir", default=".")
     parser.add_argument("crate", help="crate to verify")
     parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
@@ -42,15 +45,16 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
-    rmc.cargo_build(args.crate, args.verbose, args.debug, args.mangler)
+    rmc.cargo_build(args.crate, args.target_dir,
+                    args.verbose, args.debug, args.mangler)
 
-    pattern = f"target/debug/deps/*.json"
+    pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
     if len(jsons) != 1:
         print("ERROR: unexpected number of json outputs")
         return 1
-    cbmc_filename = "cbmc.out"
-    c_filename = "cbmc.c"
+    cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
+    c_filename = os.path.join(args.target_dir, "cbmc.c")
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps):
         return 1
 
@@ -64,7 +68,7 @@ def main():
     if args.visualize:
         return rmc.run_visualize(cbmc_filename, args.cbmc_args, \
                                  args.verbose, args.quiet, args.keep_temps, \
-                                 args.function, args.srcdir, args.wkdir)
+                                 args.function, args.srcdir, args.wkdir, args.target_dir)
     else:
         return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet)
 

scripts/rmc-regression.sh

@@ -21,17 +21,10 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Formatting check
 ./x.py fmt --check
 
-# Standalone rmc tests
+# Standalone rmc tests and cargo tests
 pushd $RUST_DIR
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
-./x.py test -i --stage 1 cbmc firecracker prusti smack
-
-# Standalone cargo-rmc tests
-cd cargo-rmc-tests
-for DIR in */; do
-  ./run.py $DIR
-done
-popd
+./x.py test -i --stage 1 cbmc firecracker prusti smack cargo-rmc
 
 # run-make tests
 ./x.py test -i --stage 1 src/test/run-make --test-args gotoc

scripts/rmc.py

@@ -76,13 +76,13 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb
     return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug)
 
 
-def cargo_build(crate, verbose=False, debug=False, mangler="v0"):
+def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0"):
     rustflags = ["-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", f"--cfg={RMC_CFG}"]
     rustflags = " ".join(rustflags)
     if "RUSTFLAGS" in os.environ:
         rustflags = os.environ["RUSTFLAGS"] + " " + rustflags
 
-    build_cmd = ["cargo", "build"]
+    build_cmd = ["cargo", "build", "--target-dir", target_dir]
     build_env = {"RUSTFLAGS": rustflags,
                  "RUSTC": RMC_RUSTC_EXE,
                  "PATH": os.environ["PATH"],
@@ -102,11 +102,11 @@ def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False):
     cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename]
     return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet)
 
-def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir="."):
-    results_filename = "results.xml"
-    coverage_filename = "coverage.xml"
-    property_filename = "property.xml"
-    temp_goto_filename = "temp.goto"
+def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir="."):
+    results_filename = os.path.join(outdir, "results.xml")
+    coverage_filename = os.path.join(outdir, "coverage.xml")
+    property_filename = os.path.join(outdir, "property.xml")
+    temp_goto_filename = os.path.join(outdir, "temp.goto")
     if not keep_temps:
         for filename in [results_filename, coverage_filename, property_filename, temp_goto_filename]:
             atexit.register(delete_file, filename)
@@ -115,7 +115,7 @@ def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_tem
     # 2) cbmc --xml-ui --trace ~/rmc/library/rmc/rmc_lib.c temp.goto > results.xml
     # 3) cbmc --xml-ui --cover location ~/rmc/library/rmc/rmc_lib.c temp.goto > coverage.xml
     # 4) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c temp.goto > property.xml
-    # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto
+    # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto --reportdir report
 
     run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet)
 
@@ -128,22 +128,24 @@ def run_cbmc_local(cbmc_args, output_to):
     run_cbmc_local(cbmc_xml_args + ["--cover", "location"], coverage_filename)
     run_cbmc_local(cbmc_xml_args + ["--show-properties"], property_filename)
 
-    run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename, property_filename, verbose, quiet, srcdir, wkdir)
+    run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename,
+                    property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"))
 
     return retcode
 
 def run_goto_cc(src, dst, verbose=False, quiet=False, function="main"):
     cmd = ["goto-cc"] + ["--function", function] + [src] + ["-o", dst]
     return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet)
 
-def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir="."):
+def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report"):
     cmd = ["cbmc-viewer"] + \
           ["--result", results_filename] + \
           ["--coverage", coverage_filename] + \
           ["--property", property_filename] + \
           ["--srcdir", os.path.realpath(srcdir)] + \
           ["--wkdir", os.path.realpath(wkdir)] + \
-          ["--goto", goto_filename]
+          ["--goto", goto_filename] + \
+          ["--reportdir", reportdir]
     return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet)
 
 

src/bootstrap/builder.rs

@@ -440,6 +440,7 @@ impl<'a> Builder<'a> {
                 test::Prusti,
                 test::Serial,
                 test::SMACK,
+                test::CargoRMC,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
             ),

src/bootstrap/test.rs

@@ -1131,6 +1131,8 @@ default_test!(Serial { path: "src/test/serial", mode: "rmc", suite: "serial" });
 
 default_test!(SMACK { path: "src/test/smack", mode: "rmc", suite: "smack" });
 
+default_test!(CargoRMC { path: "src/test/cargo-rmc", mode: "cargo-rmc", suite: "cargo-rmc" });
+
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 struct Compiletest {
     compiler: Compiler,

src/test/cargo-rmc/.gitignore

@@ -0,0 +1 @@
+Cargo.lock

src/test/cargo-rmc/simple-main/main.expected

@@ -0,0 +1,2 @@
+[main.assertion.1] line 4 assertion failed: 1 == 2: FAILURE
+VERIFICATION FAILED

cargo-rmc-tests/empty-main/src/main.rs → src/test/cargo-rmc/simple-main/src/main.rs

@@ -1,3 +1,5 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-fn main() {}
+fn main() {
+    assert!(1 == 2);
+}

src/tools/compiletest/src/common.rs

@@ -24,6 +24,7 @@ pub enum Mode {
     MirOpt,
     Assembly,
     RMC,
+    CargoRMC,
 }
 
 impl Mode {
@@ -55,6 +56,7 @@ impl FromStr for Mode {
             "mir-opt" => Ok(MirOpt),
             "assembly" => Ok(Assembly),
             "rmc" => Ok(RMC),
+            "cargo-rmc" => Ok(CargoRMC),
             _ => Err(()),
         }
     }
@@ -77,6 +79,7 @@ impl fmt::Display for Mode {
             MirOpt => "mir-opt",
             Assembly => "assembly",
             RMC => "rmc",
+            CargoRMC => "cargo-rmc",
         };
         fmt::Display::fmt(s, f)
     }

src/tools/compiletest/src/main.rs

@@ -76,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 | rmc",
+            | rustdoc-json | codegen-units | incremental | run-make | ui | js-doc-test | mir-opt | assembly | rmc | cargo-rmc",
         )
         .reqopt(
             "",
@@ -582,6 +582,24 @@ fn collect_tests_from_dir(
     let build_dir = output_relative_path(config, relative_dir_path);
     fs::create_dir_all(&build_dir).unwrap();
 
+    // If we find a `Cargo.toml` file in the current directory and we're in
+    // Cargo-rmc mode, we should look for `*.expected` files and create an
+    // output directory corresponding to each to avoid race conditions during
+    // the testing phase. We immediately return after adding the tests to avoid
+    // treating `*.rs` files as tests.
+    if config.mode == Mode::CargoRMC && dir.join("Cargo.toml").exists() {
+        for file in fs::read_dir(dir)? {
+            let file_path = file?.path();
+            if file_path.to_str().unwrap().ends_with(".expected") {
+                fs::create_dir_all(&build_dir.join(file_path.file_stem().unwrap())).unwrap();
+                let paths =
+                    TestPaths { file: file_path, relative_dir: relative_dir_path.to_path_buf() };
+                tests.extend(make_test(config, &paths, inputs));
+            }
+        }
+        return Ok(());
+    }
+
     // Add each `.rs` file as a test, and recurse further on any
     // subdirectories we find, except for `aux` directories.
     for file in fs::read_dir(dir)? {

src/tools/compiletest/src/runtest.rs

@@ -2,7 +2,9 @@
 
 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, RMC};
+use crate::common::{
+    Assembly, CargoRMC, 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};
@@ -352,6 +354,7 @@ impl<'test> TestCx<'test> {
             Assembly => self.run_assembly_test(),
             JsDocTest => self.run_js_doc_test(),
             RMC => self.run_rmc_test(),
+            CargoRMC => self.run_cargo_rmc_test(),
         }
     }
 
@@ -2012,7 +2015,7 @@ impl<'test> TestCx<'test> {
                 rustc.arg(dir_opt);
             }
             RunPassValgrind | Pretty | DebugInfo | Codegen | Rustdoc | RustdocJson | RunMake
-            | CodegenUnits | JsDocTest | Assembly | RMC => {
+            | CodegenUnits | JsDocTest | Assembly | RMC | CargoRMC => {
                 // do not use JSON output
             }
         }
@@ -2411,6 +2414,47 @@ impl<'test> TestCx<'test> {
         }
     }
 
+    /// Runs cargo-rmc on the function specified by the stem of `self.testpaths.file`.
+    /// An error message is printed to stdout if verification result does not
+    /// contain the expected output in `self.testpaths.file`.
+    fn run_cargo_rmc_test(&self) {
+        // We create our own command for the same reasons listed in `run_rmc_test` method.
+        let mut cargo = Command::new("cargo");
+        // We run `cargo` on the directory where we found the `*.expected` file
+        let parent_dir = self.testpaths.file.parent().unwrap();
+        // The name of the function to test is the same as the stem of `*.expected` file
+        let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap();
+        cargo
+            .arg("rmc")
+            .arg("--target")
+            .arg(self.output_base_dir().join("target"))
+            .arg(&parent_dir)
+            .arg("--")
+            .args(["--function", function_name]);
+        self.add_rmc_dir_to_path(&mut cargo);
+        let proc_res = self.compose_and_run_compiler(cargo, None);
+        let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();
+        // Print an error if the verification result does not contains the expected lines.
+        if let Some(line) = TestCx::contains_lines(&proc_res.stdout, expected.split('\n').collect())
+        {
+            self.fatal_proc_rec(
+                &format!("test failed: expected output to contain the line: {}", line),
+                &proc_res,
+            );
+        }
+    }
+
+    /// Looks for each line in `str`. Returns `None` if all line are in `str`.
+    /// Otherwise, it returns the first line not found in `str`.
+    fn contains_lines<'a>(str: &str, lines: Vec<&'a str>) -> Option<&'a str> {
+        for line in lines {
+            if !str.contains(line) {
+                return Some(line);
+            }
+        }
+        None
+    }
+
     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" }