- **Feature Name:** Line coverage (`line-coverage`) - **Feature Request Issue:** - **RFC PR:** - **Status:** Unstable - **Version:** 0 - **Proof-of-concept:** (Kani) + (Kani VS Code Extension) ------------------- ## Summary Add verification-based line coverage reports to Kani. ## User Impact Nowadays, users can't easily obtain verification-based coverage reports in Kani. Generally speaking, coverage reports show which parts of the code under verification are covered and which are not. Because of that, coverage is often seen as a great metric to determine the quality of a verification effort. Moreover, some users prefer using coverage information for harness development and debugging. That's because coverage information provides users with more familiar way to interpret verification results. This RFC proposes adding a new option for verification-based line coverage reports to Kani. As mentioned earlier, we expect users to employ this coverage-related option on several stages of a verification effort: * **Learning:** New users are more familiar with coverage reports than property-based results. * **Development:** Some users prefer coverage results to property-based results since they are easier to interpret. * **CI Integration**: Users may want to enforce a minimum percentage of code coverage for new contributions. * **Debugging:** Users may find coverage reports particularly helpful when inputs are over-constrained (missing some corner cases). * **Evaluation:** Users can easily evaluate where and when more verification work is needed (some projects aim for 100% coverage). Moreover, adding this option directly to Kani, instead of relying on another tools, is likely to: 1. Increase the speed of development 2. Improve testing for coverage features Which translates into faster and more reliable coverage options for users. ## User Experience The goal is for Kani to generate code coverage report per harness in a well established format, such as [LCOV](https://github.com/linux-test-project/lcov), and possibly a summary in the output. For now, we will focus on an interim solution that will enable us to assess the results of [our instrumentation](#injection-of-coverage-checks) and enable integration with the Kani VS Code extension. ### High-level changes For the first version, this experimental feature will report verification results along coverage reports. Because of that, we'll add a new section `Coverage results` that shows coverage results for each individual harness. In the following, we describe an experimental output format. Note that the final output format and overall UX is to be determined. ### Experimental output format for coverage results The `Coverage results` section for each harness will produce coverage information in a CSV format as follows: ``` , , ``` where `` is either `FULL`, `PARTIAL` or `NONE`. As mentioned, this format is designed for evaluating the [native instrumentation-based design](#detailed-design) and is likely to be substituted with another well-established format as soon as possible. **Users are not expected to consume this output directly.** Instead, coverage data is to be consumed by the [Kani VS Code extension](https://github.com/model-checking/kani-vscode-extension) and displayed as in [the VS Code Extension prototype](https://github.com/model-checking/kani-vscode-extension/pull/122). How to activate and display coverage information in the extension is out of scope for this RFC. That said, a proof-of-concept implementation is available [here](https://github.com/model-checking/kani-vscode-extension/pull/122). ## Detailed Design ### Architecture We will add a new unstable `--coverage` verification option to Kani which will require `-Z line-coverage` until this feature is stabilized. We will also add a new `--coverage-checks` option to `kani-compiler`, which will result in the injection of coverage checks before each Rust statement and terminator[^coverage-experiments]. This option will be supplied by `kani-driver` when the `--coverage` option is selected. These options will cause Kani to inject coverage checks during compilation and postprocess them to produce the coverage results sections described earlier. ### Coverage Checks Coverage checks are a new class of checks similar to [`cover` checks](https://model-checking.github.io/kani/rfc/rfcs/0003-cover-statement.html). The main difference is that users cannot directly interact with coverage checks (i.e., they cannot add or remove them manually). Coverage checks are encoded as an `assert(false)` statement (to test reachability) with a fixed description. In addition, coverage checks are: * Hidden from verification results. * Postprocessed to produce coverage results. In the following, we describe the injection and postprocessing procedures to generate coverage results. #### Injection of Coverage Checks The injection of coverage checks will be done while generating code for basic blocks. This allows us to add one coverage check before each statement and terminator, which provides the most accurate results[^coverage-experiments]. It's not completely clear how this compares to the coverage instrumentation done in the Rust compiler, but an exploration to use the compiler APIs revealed that they're quite similar[^coverage-api]. #### Postprocessing Coverage Checks The injection of coverage checks often results in one or more checks per line (assuming a well-formatted program). We'll postprocess these checks so for each line - if all checks are `SATISFIED`: return `FULL` - if all checks are `UNSATISFIED`: return `NONE` - otherwise: return `PARTIAL` We won't report coverage status for lines which don't include a coverage check. ## Rationale and alternatives ### Benefits from a native coverage solution Kani has relied on [`cbmc-viewer`](https://github.com/model-checking/cbmc-viewer) to report coverage information since the beginning. In essence, `cbmc-viewer` consumes data from coverage-focused invocations of CBMC and produces an HTML report containing (1) coverage information and (2) counterexample traces. Recently, there have been some issues with the coverage information reported by `cbmc-viewer` (e.g., [#2048](https://github.com/model-checking/kani/issues/2048) or [#1707](https://github.com/model-checking/kani/issues/1707)), forcing us to mark the `--visualize` option as unstable and disable coverage results in the reports (in [#2206](https://github.com/model-checking/kani/pull/2206)). However, it's possible for Kani to report coverage information without `cbmc-viewer`, as explained before. This would give Kani control on both ends: * **The instrumentation performed** on the program. Eventually, this would allow us to report more precise coverage information (maybe similar to [Rust's instrument-based code coverage](https://doc.rust-lang.org/rustc/instrument-coverage.html)). * **The format of the coverage report** to be generated. Similarly, this would allow us to generate coverage data in different formats (see [#1706](https://github.com/model-checking/kani/issues/1706) for GCOV, or [#1777](https://github.com/model-checking/kani/issues/1777) for LCOV). While technically this is also doable from `cbmc-viewer`'s output, development is likely to be faster this way. #### Coverage through `cbmc-viewer` As an alternative, we could fix and use `cbmc-viewer` to report line coverage. Most of the issues with `cbmc-viewer` are generally due to: 1. Missing locations due to non-propagation of locations in either Kani or CBMC. 2. Differences in the definition of a basic block in CBMC and Rust's MIR. 3. Scarce documentation for coverage-related options (i.e., `--cover