Line coverage reports

[adpaco-aws]

Description of changes:

Adds a coverage report feature to Kani that does not require cbmc-viewer.

In particular, it introduces the unstable --coverage verification option to kani-driver (only usable with the -Z line-coverage unstable feature), which in turn enables the --coverage-checks option in kani-compiler. This results in the injection of coverage checks (similar to cover statements, but with a fixed condition) before each Rust MIR statement and terminator in a basic block. The post-processing of coverage checks allows us to report coverage information at the line level.

This contribution also includes a new compiletest suite developed by @jaisnan for end-to-end testing of the emitted coverage information for different test cases.

The command is:

kani file.rs --coverage -Z line-coverage

For instance, for the assume_false.rs example

#[kani::proof]
fn wrong_coverage_2() {
    let a: u8 = kani::any();
    kani::assume(false);
    assert!(a < 5);
}

we obtain the verification results:

RESULTS:
Check 1: wrong_coverage_2.assertion.1
         - Status: UNREACHABLE
         - Description: "assertion failed: a < 5"
         - Location: assume_false.rs:5:5 in function wrong_coverage_2

and the following coverage results:

Coverage Results:
/home/ubuntu/kani/library/kani/src/lib.rs, 133, FULL
/home/ubuntu/kani/library/kani/src/lib.rs, 134, FULL
/home/ubuntu/kani/library/kani/src/lib.rs, 176, FULL
/home/ubuntu/kani/library/kani/src/lib.rs, 177, FULL

/home/ubuntu/kani/assume_false.rs, 3, FULL
/home/ubuntu/kani/assume_false.rs, 4, FULL
/home/ubuntu/kani/assume_false.rs, 5, NONE
/home/ubuntu/kani/assume_false.rs, 6, NONE

/home/ubuntu/kani/library/kani/src/arbitrary.rs, 55, FULL

Resolved issues:

Resolves #2585
Resolves #2608
Resolves #2610

Related RFC:

#2612

Call-outs:

Testing:

• How is this change tested? Existing tests + new coverage suite.

• Is this a refactor change? No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

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

[celinval]

I think we need to polish the coverage output to make it more intuitive, but this is a good start.

Please create issues to:

1. Improve the tests
2. Create a user friendly output
3. Export results to a well-supported output
4. Investigate if we can make some results more intuitive (maybe compare against Rust code coverage results).
5. All other open questions in the RFC

[zhassan-aws]

There are a few redundant tests remaining. Otherwise, looks good.

[adpaco-aws]

Created the following issues:

• Improve tests for coverage #2635
• Create user-friendly output for coverage #2636
• Export coverage results to a well-supported output #2638
• Avoid confusing results in coverage reports #2639
• Report source-based coverage results #2640
• Create a tool for aggregating coverage results #2641
• Investigate how coverage checks affect performance #2642

which I'm hoping take care of the remaining work here and in the RFC (#2618)

There are a few redundant tests remaining

Indeed, there were many tests that were redundant or didn't have a clear purpose. I removed a bunch of them and have #2635 for another pass.

[celinval]

@adpaco-aws should we create a milestone for those?

[adpaco-aws]

Yes, just created a Coverage reports milestone to keep track of all of these. I create a new one instead of using the Source-based coverage report generation milestone because that one contains issues with the visualize feature, and it's not clear to me that we should mix both.