From f1221b1b25e9e2896a9dfef48768cabc677b0ef6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 20 Sep 2024 11:40:16 -0400 Subject: [PATCH] Fix storing coverage data in cargo projects (#3527) This PR changes the condition we use to decide where to store the coverage data resulting from a coverage-enabled verification run. The previous condition would otherwise cause Kani to crash at the end of the run in some cases: ``` Source-based code coverage results: src/pair.rs (pair::Pair::new) * 6:5 - 8:6 COVERED src/pair.rs (pair::Pair::sum) * 9:5 - 11:6 COVERED src/pair.rs (pair::kani_tests::test_one_plus_two) * 29:5 - 32:6 COVERED Verification Time: 0.083455205s thread 'main' panicked at kani-driver/src/coverage/cov_session.rs:70:43: called `Option::unwrap()` on a `None` value note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ``` The PR also adds a new `cargo-coverage` mode to `compiletest` which runs `cargo kani` with the source-based coverage feature enabled. This ensures that coverage-enabled `cargo kani` runs are also being tested, and will also be helpful for testing the upcoming coverage tool (#3121) with cargo packages. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/coverage/cov_session.rs | 4 +-- scripts/kani-regression.sh | 1 + tests/cargo-coverage/simple-lib/Cargo.toml | 10 ++++++ tests/cargo-coverage/simple-lib/src/lib.rs | 25 ++++++++++++++ tests/cargo-coverage/simple-lib/src/pair.rs | 33 +++++++++++++++++++ .../simple-lib/test_one_plus_two.expected | 10 ++++++ .../simple-lib/test_sum.expected | 10 ++++++ tools/compiletest/src/common.rs | 3 ++ tools/compiletest/src/main.rs | 8 +++-- tools/compiletest/src/runtest.rs | 33 +++++++++++++++++-- 10 files changed, 131 insertions(+), 6 deletions(-) create mode 100644 tests/cargo-coverage/simple-lib/Cargo.toml create mode 100644 tests/cargo-coverage/simple-lib/src/lib.rs create mode 100644 tests/cargo-coverage/simple-lib/src/pair.rs create mode 100644 tests/cargo-coverage/simple-lib/test_one_plus_two.expected create mode 100644 tests/cargo-coverage/simple-lib/test_sum.expected diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index df82d982bd72..bf6b34d3cd0b 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/kani-driver/src/coverage/cov_session.rs @@ -18,7 +18,7 @@ impl KaniSession { /// Note: Currently, coverage mappings are not included due to technical /// limitations. But this is where we should save them. pub fn save_coverage_metadata(&self, project: &Project, stamp: &String) -> Result<()> { - if self.args.target_dir.is_some() { + if project.input.is_none() { self.save_coverage_metadata_cargo(project, stamp) } else { self.save_coverage_metadata_standalone(project, stamp) @@ -97,7 +97,7 @@ impl KaniSession { results: &Vec, stamp: &String, ) -> Result<()> { - if self.args.target_dir.is_some() { + if project.input.is_none() { self.save_coverage_results_cargo(results, stamp) } else { self.save_coverage_results_standalone(project, results, stamp) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index b1de293d533c..bd6b04d7386e 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -60,6 +60,7 @@ TESTS=( "cargo-ui cargo-kani" "script-based-pre exec" "coverage coverage-based" + "cargo-coverage cargo-coverage" "kani-docs cargo-kani" "kani-fixme kani-fixme" ) diff --git a/tests/cargo-coverage/simple-lib/Cargo.toml b/tests/cargo-coverage/simple-lib/Cargo.toml new file mode 100644 index 000000000000..23f843337dc7 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "simple-lib" +version = "0.1.0" +edition = "2018" + +[dependencies] + +[workspace] diff --git a/tests/cargo-coverage/simple-lib/src/lib.rs b/tests/cargo-coverage/simple-lib/src/lib.rs new file mode 100644 index 000000000000..f5f23c6a2acb --- /dev/null +++ b/tests/cargo-coverage/simple-lib/src/lib.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +pub mod pair; +pub use pair::Pair; + +#[cfg(test)] +mod tests { + #[test] + fn it_works() { + assert_eq!(2 + 2, 4); + } +} + +#[cfg(kani)] +mod kani_tests { + use super::*; + + #[kani::proof] + fn test_sum() { + let a: u64 = kani::any(); + let b: u64 = kani::any(); + let p = Pair::new(a, b); + assert!(p.sum() == a.wrapping_add(b)); + } +} diff --git a/tests/cargo-coverage/simple-lib/src/pair.rs b/tests/cargo-coverage/simple-lib/src/pair.rs new file mode 100644 index 000000000000..0201156c4225 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/src/pair.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +pub struct Pair(pub u64, pub u64); + +impl Pair { + pub fn new(a: u64, b: u64) -> Self { + Pair(a, b) + } + pub fn sum(&self) -> u64 { + self.0.wrapping_add(self.1) + } +} + +#[cfg(test)] +mod tests { + use super::*; + #[test] + fn one_plus_two() { + let p = Pair::new(1, 2); + assert_eq!(p.sum(), 3); + } +} + +#[cfg(kani)] +mod kani_tests { + use super::*; + + #[kani::proof] + fn test_one_plus_two() { + let p = Pair::new(1, 2); + assert!(p.sum() == 3); + } +} diff --git a/tests/cargo-coverage/simple-lib/test_one_plus_two.expected b/tests/cargo-coverage/simple-lib/test_one_plus_two.expected new file mode 100644 index 000000000000..6010f6fe7b3d --- /dev/null +++ b/tests/cargo-coverage/simple-lib/test_one_plus_two.expected @@ -0,0 +1,10 @@ +Source-based code coverage results: + +src/pair.rs (pair::Pair::new)\ + * 6:5 - 8:6 COVERED + +src/pair.rs (pair::Pair::sum)\ + * 9:5 - 11:6 COVERED + +src/pair.rs (pair::kani_tests::test_one_plus_two)\ + * 29:5 - 32:6 COVERED diff --git a/tests/cargo-coverage/simple-lib/test_sum.expected b/tests/cargo-coverage/simple-lib/test_sum.expected new file mode 100644 index 000000000000..ea1bd5ad3a62 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/test_sum.expected @@ -0,0 +1,10 @@ +Source-based code coverage results: + +src/lib.rs (kani_tests::test_sum)\ + * 19:5 - 24:6 COVERED + +src/pair.rs (pair::Pair::new)\ + * 6:5 - 8:6 COVERED + +src/pair.rs (pair::Pair::sum)\ + * 9:5 - 11:6 COVERED diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index 99ec78bef693..d5c4ccf3c116 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -17,6 +17,7 @@ use test::ColorConfig; pub enum Mode { Kani, KaniFixme, + CargoCoverage, CargoKani, CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`. CoverageBased, @@ -34,6 +35,7 @@ impl FromStr for Mode { "cargo-kani" => Ok(CargoKani), "cargo-kani-test" => Ok(CargoKaniTest), "coverage-based" => Ok(CoverageBased), + "cargo-coverage" => Ok(CargoCoverage), "exec" => Ok(Exec), "expected" => Ok(Expected), "stub-tests" => Ok(Stub), @@ -47,6 +49,7 @@ impl fmt::Display for Mode { let s = match *self { Kani => "kani", KaniFixme => "kani-fixme", + CargoCoverage => "cargo-coverage", CargoKani => "cargo-kani", CargoKaniTest => "cargo-kani-test", CoverageBased => "coverage-based", diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 94cbd561aa51..dd1284d7a3c9 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -349,7 +349,7 @@ fn collect_tests_from_dir( tests: &mut Vec, ) -> io::Result<()> { match config.mode { - Mode::CargoKani | Mode::CargoKaniTest => { + Mode::CargoCoverage | Mode::CargoKani | Mode::CargoKaniTest => { collect_expected_tests_from_dir(config, dir, relative_dir_path, inputs, tests) } Mode::Exec => collect_exec_tests_from_dir(config, dir, relative_dir_path, inputs, tests), @@ -378,7 +378,11 @@ 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!(config.mode == Mode::CargoKani || config.mode == Mode::CargoKaniTest); + assert!( + config.mode == Mode::CargoCoverage + || 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 c8387c691296..c6575db17819 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -8,7 +8,7 @@ use crate::common::KaniFailStep; use crate::common::{output_base_dir, output_base_name}; use crate::common::{ - CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, + CargoCoverage, CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, }; use crate::common::{Config, TestPaths}; use crate::header::TestProps; @@ -74,6 +74,7 @@ impl<'test> TestCx<'test> { match self.config.mode { Kani => self.run_kani_test(), KaniFixme => self.run_kani_test(), + CargoCoverage => self.run_cargo_coverage_test(), CargoKani => self.run_cargo_kani_test(false), CargoKaniTest => self.run_cargo_kani_test(true), CoverageBased => self.run_expected_coverage_test(), @@ -313,7 +314,7 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } - /// Run coverage based output for kani on a single file + /// Run Kani with coverage enabled on a single source file fn run_kani_with_coverage(&self) -> ProcRes { let mut kani = Command::new("kani"); if !self.props.compile_flags.is_empty() { @@ -329,6 +330,34 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } + /// Run Kani with coverage enabled on a cargo package + fn run_cargo_coverage_test(&self) { + // 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 + 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("kani") + .arg("--coverage") + .arg("-Zsource-coverage") + .arg("--target-dir") + .arg(self.output_base_dir().join("target")) + .current_dir(parent_dir); + + if "expected" != self.testpaths.file.file_name().unwrap() { + cargo.args(["--harness", function_name]); + } + cargo.args(&self.config.extra_args); + + let proc_res = self.compose_and_run(cargo); + self.verify_output(&proc_res, &self.testpaths.file); + + // TODO: We should probably be checking the exit status somehow + // See https://github.com/model-checking/kani/issues/1895 + } + /// Runs an executable file and: /// * Checks the expected output if an expected file is specified /// * Checks the exit code (assumed to be 0 by default)