-
Notifications
You must be signed in to change notification settings - Fork 88
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
1 parent
27cee8b
commit f1221b1
Showing
10 changed files
with
131 additions
and
6 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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); | ||
} | ||
} |
10 changes: 10 additions & 0 deletions
10
tests/cargo-coverage/simple-lib/test_one_plus_two.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters