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

Rust's coverage instrumentation assumes function calls never panic #3441

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

Rust's coverage instrumentation assumes function calls never panic #3441

adpaco-aws opened this issue Aug 15, 2024 · 0 comments
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue Z-UnstableFeature Issues that only occur if a unstable feature is enabled

Comments

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Aug 15, 2024

The integration with the Rust coverage instrumentation being introduced in #3119 seems to work well for all cases except for function calls causing panics or other control-flow divergences. Take the following example:

14 fn some_function(a: u64, b: u64) -> bool{
15     if a > b { panic!(); false } else { true}
16 }
17
18 #[kani::proof]
19 fn panics() {
20    let a: u64 = kani::any();
21    let b: u64 = kani::any();
22    panic!();
23    assert!(some_function(a, b));
24 }

The instrumentation introduced in #3119 reports a single region for the whole function, which is considered to be covered:

Failed Checks: explicit panic
 File: "src/main.rs", line 15, in some_function

VERIFICATION:- FAILED

Source-based code coverage results:

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

src/main.rs (some_function)
 * 14:1 - 15:13 COVERED
 * 15:16 - 15:24 COVERED
 * 15:41 - 16:2 COVERED

This is very relevant when using certain Kani APIs like kani::assume(...) because the code following it will be reported as being within the same (covered) region when actually that part might not being covered. For example, let's take the program:

1 #[kani::proof]
2 fn dummy() {
3     let x: u32 = kani::any();
4     kani::assume(false);
5     assert!(x == 2);
6 }

The results we currently obtain are:

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

which are incorrect. Instead, there should be:

  1. One region from the beginning of the function to the end of the kani::assume(..) statement.
  2. Another region containing the assert!(x == 2) statement which is actually unreachable during verification.

Note that this is an issue with the Rust coverage instrumentation, which assumes that function calls never panic. This assumption does result in a much more efficient instrumentation. According to this Zulip thread, the Rust team will attempt to lift this assumption and potentially provide options to disable the optimization. The issue tracking this work is mainly rust-lang/rust#78544.

@adpaco-aws adpaco-aws added [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue Z-UnstableFeature Issues that only occur if a unstable feature is enabled labels Aug 15, 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] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue Z-UnstableFeature Issues that only occur if a unstable feature is enabled
Projects
None yet
Development

No branches or pull requests

1 participant