Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coverage metadata should include mappings for all source code #3445

Open
adpaco-aws opened this issue Aug 16, 2024 · 0 comments
Open

Coverage metadata should include mappings for all source code #3445

adpaco-aws opened this issue Aug 16, 2024 · 0 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.

Comments

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Aug 16, 2024

In the integration of Rust's code coverage instrumentation being introduced in #3119, coverage metadata consists of just the canonical paths for all source code files.

Ideally, this metadata should be extended with coverage information for each function in the project, not just those deemed reachable by the reachability analysis. This is necessary for kani-cov (the coverage-focused tool being introduced in #3121) to be able to produce coverage summaries and reports that include coverage data for the entire project.

For example, for the test

1 fn _other_function() {
2    println!("Hello, world!");
3 }
4
5 fn test_cov(val: u32) -> bool {
6     if val < 3 || val == 42 {
7         true
8     } else {
9         false
10    }
11 }
12
13 #[cfg_attr(kani, kani::proof)]
14 fn main() {
15    let test1 = test_cov(1);
16    let test2 = test_cov(2);
17    assert!(test1);
18    assert!(test2);
19 }

we get coverage results for the reachable functions main and test_cov, but not for _other_function:

src/main.rs (main)
 * 14:1 - 19:2 COVERED

src/main.rs (test_cov)
 * 5:1 - 6:15 COVERED
 * 6:19 - 6:28 UNCOVERED
 * 7:9 - 7:13 COVERED
 * 9:9 - 9:14 UNCOVERED
 * 11:1 - 11:2 COVERED

We can mitigate this for function and line metrics in #3121 by using (for example) tools like syn on the source code files, but we cannot do the same for region metrics because region information for each function is only available to us when compiling the function in Kani. However, this is not the case for non-reachable functions which won't be compiled, so we cannot fully record that information.

Additionally, storing the coverage mappings into the coverage metadata file would save us some work at compilation time to determine the code regions that a particular counter is covering. This process could be done in kani-cov so the effort spent postprocessing coverage properties could be practically omitted.

@adpaco-aws adpaco-aws added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Aug 16, 2024
@adpaco-aws adpaco-aws added the [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. label Aug 16, 2024
github-merge-queue bot pushed a commit that referenced this issue Aug 27, 2024
This PR replaces the line-based coverage instrumentation we introduced
in #2609 with the standard source-based code coverage instrumentation
performed by the Rust compiler.

As a result, we now insert code coverage checks in the
`StatementKind::Coverage(..)` statements produced by the Rust compiler
during compilation. These checks include coverage-relevant
information[^note-internal] such as the coverage counter/expression they
represent [^note-instrument]. Both the coverage metadata (`kanimap`) and
coverage results (`kaniraw`) are saved into files after the verification
stage.

Unfortunately, we currently have a chicken-egg problem with this PR and
#3121, where we introduce a tool named `kani-cov` to postprocess
coverage results. As explained in #3143, `kani-cov` is expected to be an
alias for the `cov` subcommand and provide most of the postprocessing
features for coverage-related purposes. But, the tool will likely be
introduced after this change. Therefore, we propose to temporarily print
a list of the regions in each function with their associated coverage
status (i.e., `COVERED` or `UNCOVERED`).

### Source-based code coverage: An example

The main advantage of source-based coverage results is their precision
with respect to the source code. The [Source-based Code
Coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)
documentation explains more details about the LLVM coverage workflow and
its different options.

For example, let's take this Rust code:
```rust
1 fn _other_function() {
2    println!("Hello, world!");
3 }
4
5 fn test_cov(val: u32) -> bool {
6     if val < 3 || val == 42 {
7         true
8     } else {
9         false
10    }
11 }
12
13 #[cfg_attr(kani, kani::proof)]
14 fn main() {
15    let test1 = test_cov(1);
16    let test2 = test_cov(2);
17    assert!(test1);
18    assert!(test2);
19 }
```

Compiling and running the program with `rustc` and the `-C
instrument-coverage` flag, and using the LLVM tools can get us the
following coverage result:


![Image](https://github.com/model-checking/kani/assets/73246657/9070e390-6e0b-4add-828d-d9f9caacad07)


In contrast, the `cargo kani --coverage -Zsource-coverage` command
currently generates:

```
src/main.rs (main)
 * 14:1 - 19:2 COVERED

src/main.rs (test_cov)
 * 5:1 - 6:15 COVERED
 * 6:19 - 6:28 UNCOVERED
 * 7:9 - 7:13 COVERED
 * 9:9 - 9:14 UNCOVERED
 * 11:1 - 11:2 COVERED
```

which is a verification-based coverage result almost equivalent to the
runtime coverage results.

### Benchmarking

We have evaluated the performance impact of the instrumentation using
the `kani-perf.sh` suite (14 benchmarks). For each test, we compare the
average time to run standard verification against the average time to
run verification with the source-based code coverage feature
enabled[^note-line-evaluation].

The evaluation has been performed on an EC2 `m5a.4xlarge` instance
running Ubuntu 22.04. The experimental data has been obtained by running
the `kani-perf.sh` script 10 times for each version (`only verification`
and `verification + coverage`), computing the average and standard
deviation. We've split this data into `small` (tests taking 60s or less)
and `large` (tests taking more than 60s) and drawn the two graphs below.

#### Performance comparison - `small` benchmarks


![performance_comparison_small](https://github.com/user-attachments/assets/679cf412-0193-4b0c-a78c-2d0fb702706f)

#### Performance comparison - `large` benchmarks


![performance_comparison_large](https://github.com/user-attachments/assets/4bb5a895-7f57-49e0-86b5-5fea67fad939)

#### Comments on performance

Looking at the small tests, the performance impact seems negligible in
such cases. The difference is more noticeable in the large tests, where
the time to run verification and coverage can take 2x or even more. It
wouldn't be surprising that, as programs become larger, the complexity
of the coverage checking grows exponentially as well. However, since
most verification jobs don't take longer than 30min (1800s), it's OK to
say that coverage checking represents a 100-200% slowdown in the worst
case w.r.t. standard verification.

It's also worth noting a few other things:
* The standard deviation remains similar in most cases, meaning that the
coverage feature doesn't have an impact on their stability.
* We haven't tried any SAT solvers other than the ones used by default
for each benchmark. It's possible that other solvers perform
better/worse with the coverage feature enabled.

### Call-outs
 * The soundness issue documented in #3441.
* The issue with saving coverage mappings for non-reachable functions
documented in #3445.
* I've modified the test cases in `tests/coverage/` to test this
feature. Since this technique is simpler, we don't need that many test
cases. However, it's possible I've left some test cases which don't
contribute much. Please let me know if you want to add/remove a test
case.

[^note-internal]: The coverage mappings can't be accessed through the
StableMIR interface so we retrieve them through the internal API.

[^note-instrument]: The instrumentation replaces certain counters with
expressions based on other counters when possible to avoid a part of the
runtime overhead. More details can be found
[here](https://github.com/rust-lang/rustc-dev-guide/blob/master/src/llvm-coverage-instrumentation.md#mir-pass-instrumentcoverage).
Unfortunately, we can't avoid instrumenting expressions at the moment.

[^note-line-evaluation]: We have not compared performance against the
line-based code coverage feature because it doesn't seem worth it. The
line-based coverage feature is guaranteed to include more coverage
checks than the source-based one for any function. In addition,
source-based results are more precise than line-based ones. So this
change represents both a quantitative and qualitative improvement.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
Projects
None yet
Development

No branches or pull requests

1 participant