From 5e7095c16759a887e5073f7daed23410fe114557 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 8 Nov 2022 17:27:59 -0800 Subject: [PATCH] Integrate latest s2n-quic proofs in Kani CI (#1862) --- scripts/kani-perf.sh | 2 +- .../s2n-quic/quic/s2n-quic-core/expected | 1 + .../vectored_copy_fuzz_test.expected | 22 ------------------- tests/perf/s2n-quic | 2 +- tools/compiletest/src/common.rs | 8 +++---- tools/compiletest/src/main.rs | 6 ++--- tools/compiletest/src/runtest.rs | 21 +++++++----------- 7 files changed, 16 insertions(+), 46 deletions(-) create mode 100644 tests/perf/overlays/s2n-quic/quic/s2n-quic-core/expected delete mode 100644 tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index 96144487f9160..e73986a32ae22 100755 --- a/scripts/kani-perf.sh +++ b/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=$? diff --git a/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/expected b/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/expected new file mode 100644 index 0000000000000..610b05dc4e673 --- /dev/null +++ b/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/expected @@ -0,0 +1 @@ +successfully verified harnesses, 0 failures diff --git a/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected b/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected deleted file mode 100644 index c0b7bedc0fcf2..0000000000000 --- a/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected +++ /dev/null @@ -1,22 +0,0 @@ -Status: SUCCESS\ -Description: "assertion failed: a == b" - -Status: SUCCESS\ -Description: "assertion failed: from.len() > from_index" - -Status: SUCCESS\ -Description: "assertion failed: to.len() > to_index" - -Status: SUCCESS\ -Description: "assertion failed: from.len() >= from_offset" - -Status: SUCCESS\ -Description: "assertion failed: to.len() >= to_offset" - -Status: SUCCESS\ -Description: "assertion failed: from.len() >= len" - -Status: SUCCESS\ -Description: "assertion failed: to.len() >= len" - -VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 2158407ada569..e1353ac5b7beb 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 2158407ada56905d9627331923263bfc6f6b43d6 +Subproject commit e1353ac5b7bebb2ab523748adafcc6400b8130be diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index c947ac769cded..26779a3869637 100644 --- a/tools/compiletest/src/common.rs +++ b/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 - pub mir_linker: bool, } #[derive(Debug, Clone)] diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 2a0716f8a34b1..4598aeabd4def 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -157,7 +157,6 @@ pub fn parse_config(args: Vec) -> 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, ) -> 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)? { diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index d50cc2ccaf818..f769e7d6ed61d 100644 --- a/tools/compiletest/src/runtest.rs +++ b/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);