Integrate latest s2n-quic proofs in Kani CI (rust-lang#1862)

scripts/kani-perf.sh

@@ -25,7 +25,7 @@ for overlay_dir in ${PERF_DIR}/overlays/*/; do
 done
 
 suite="perf"
-mode="cargo-kani"
+mode="cargo-kani-test"
 echo "Check compiletest suite=$suite mode=$mode"
 cargo run -p compiletest -- --suite $suite --mode $mode
 exit_code=$?

tests/perf/overlays/s2n-quic/quic/s2n-quic-core/expected

@@ -0,0 +1 @@
+successfully verified harnesses, 0 failures

tools/compiletest/src/common.rs

@@ -18,6 +18,7 @@ pub enum Mode {
     Kani,
     KaniFixme,
     CargoKani,
+    CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`.
     Expected,
     Stub,
 }
@@ -29,6 +30,7 @@ impl FromStr for Mode {
             "kani" => Ok(Kani),
             "kani-fixme" => Ok(KaniFixme),
             "cargo-kani" => Ok(CargoKani),
+            "cargo-kani-test" => Ok(CargoKaniTest),
             "expected" => Ok(Expected),
             "stub-tests" => Ok(Stub),
             _ => Err(()),
@@ -42,6 +44,7 @@ impl fmt::Display for Mode {
             Kani => "kani",
             KaniFixme => "kani-fixme",
             CargoKani => "cargo-kani",
+            CargoKaniTest => "cargo-kani-test",
             Expected => "expected",
             Stub => "stub-tests",
         };
@@ -131,11 +134,6 @@ pub struct Config {
 
     /// Whether we will run the tests or not.
     pub dry_run: bool,
-
-    /// Allow us to run the regression with the mir linker enabled by default. For that, set
-    /// `RUSTFLAGS=--cfg=mir_linker` while compiling `compiletest`.
-    /// Remove this as part of <https://github.com/model-checking/kani/issues/1677>
-    pub mir_linker: bool,
 }
 
 #[derive(Debug, Clone)]

tools/compiletest/src/main.rs

@@ -157,7 +157,6 @@ pub fn parse_config(args: Vec<String>) -> Config {
         color,
         edition: matches.opt_str("edition"),
         force_rerun: matches.opt_present("force-rerun"),
-        mir_linker: cfg!(mir_linker),
         dry_run: matches.opt_present("dry-run"),
         timeout,
     }
@@ -176,7 +175,6 @@ pub fn log_config(config: &Config) {
     logv(c, format!("host: {}", config.host));
     logv(c, format!("verbose: {}", config.verbose));
     logv(c, format!("quiet: {}", config.quiet));
-    logv(c, format!("mir_linker: {}", config.mir_linker));
     logv(c, format!("timeout: {:?}", config.timeout));
     logv(
         c,
@@ -329,7 +327,7 @@ fn collect_tests_from_dir(
     tests: &mut Vec<test::TestDescAndFn>,
 ) -> io::Result<()> {
     match config.mode {
-        Mode::CargoKani => {
+        Mode::CargoKani | Mode::CargoKaniTest => {
             collect_expected_tests_from_dir(config, dir, relative_dir_path, inputs, tests)
         }
         _ => collect_rs_tests_from_dir(config, dir, relative_dir_path, inputs, tests),
@@ -357,7 +355,7 @@ fn collect_expected_tests_from_dir(
     // 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.
-    assert_eq!(config.mode, Mode::CargoKani);
+    assert!(config.mode == Mode::CargoKani || config.mode == Mode::CargoKaniTest);
 
     let has_cargo_toml = dir.join("Cargo.toml").exists();
     for file in fs::read_dir(dir)? {

tools/compiletest/src/runtest.rs

@@ -7,7 +7,7 @@
 
 use crate::common::KaniFailStep;
 use crate::common::{output_base_dir, output_base_name};
-use crate::common::{CargoKani, Expected, Kani, KaniFixme, Stub};
+use crate::common::{CargoKani, CargoKaniTest, Expected, Kani, KaniFixme, Stub};
 use crate::common::{Config, TestPaths};
 use crate::header::TestProps;
 use crate::json;
@@ -63,7 +63,8 @@ impl<'test> TestCx<'test> {
         match self.config.mode {
             Kani => self.run_kani_test(),
             KaniFixme => self.run_kani_test(),
-            CargoKani => self.run_cargo_kani_test(),
+            CargoKani => self.run_cargo_kani_test(false),
+            CargoKaniTest => self.run_cargo_kani_test(true),
             Expected => self.run_expected_test(),
             Stub => self.run_stub_test(),
         }
@@ -291,9 +292,10 @@ impl<'test> TestCx<'test> {
     }
 
     /// Runs cargo-kani on the function specified by the stem of `self.testpaths.file`.
+    /// The `test` parameter controls whether to specify `--tests` to `cargo kani`.
     /// An error message is printed to stdout if verification output does not
     /// contain the expected output in `self.testpaths.file`.
-    fn run_cargo_kani_test(&self) {
+    fn run_cargo_kani_test(&self, test: bool) {
         // We create our own command for the same reasons listed in `run_kani_test` method.
         let mut cargo = Command::new("cargo");
         // We run `cargo` on the directory where we found the `*.expected` file
@@ -305,15 +307,13 @@ impl<'test> TestCx<'test> {
             .arg("--target-dir")
             .arg(self.output_base_dir().join("target"))
             .current_dir(&parent_dir);
+        if test {
+            cargo.arg("--tests");
+        }
         if "expected" != self.testpaths.file.file_name().unwrap() {
             cargo.args(["--harness", function_name]);
         }
 
-        if self.config.mir_linker {
-            // Allow us to run the regression with the mir linker enabled by default.
-            cargo.arg("--enable-unstable").arg("--mir-linker");
-        }
-
         let proc_res = self.compose_and_run(cargo);
         let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();
         self.verify_output(&proc_res, &expected);
@@ -334,11 +334,6 @@ impl<'test> TestCx<'test> {
             kani.env("RUSTFLAGS", self.props.compile_flags.join(" "));
         }
 
-        if self.config.mir_linker {
-            // Allow us to run the regression with the mir linker enabled by default.
-            kani.arg("--enable-unstable").arg("--mir-linker");
-        }
-
         // Pass the test path along with Kani and CBMC flags parsed from comments at the top of the test file.
         kani.arg(&self.testpaths.file).args(&self.props.kani_flags);