Adopt Rust's source-based code coverage instrumentation

[adpaco-aws]

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¹ such as the coverage counter/expression they represent ². 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 documentation explains more details about the LLVM coverage workflow and its different options.

For example, let's take this Rust code:

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:

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³.

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 - large benchmarks

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 Rust's coverage instrumentation assumes function calls never panic #3441.
• The issue with saving coverage mappings for non-reachable functions documented in Coverage metadata should include mappings for all source code #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.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Footnotes

1. The coverage mappings can't be accessed through the StableMIR interface so we retrieve them through the internal API. ↩

2. 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. Unfortunately, we can't avoid instrumenting expressions at the moment. ↩

3. 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. ↩

[adpaco-aws]

Ready for review again - I've taken the chance to reorganize the tests/coverage folder so that it's not so nested. There's even a known_issue folder that contains the tests with known issues. I've removed some more tests that seemed redundant to me too. Hope that makes it easier to review.

[zhassan-aws]

Looks great! I haven't looked at the CBMC result parsing part yet.

[zhassan-aws]

A few nits. Thanks @adpaco-aws!

[adpaco-aws]

Thank you, @zhassan-aws ! I will hold the merge of this PR until #3143 is merged.

Also, the other we talked about this feature breaking the coverage feature in the VS Code extension. I recall agreeing to keeping the line-based coverage option but, on a second thought, I think it'd just be easier to remove it here and integrate the VS Code extension with the source-based feature. I'm meeting @jaisnan soon to make sure that's the case and coordinate on the integration.