Skip to content

Commit 13bfdd8

Browse files
adpaco-awsjaisnan
adpaco-aws
and
jaisnan
authored
RFC: Line Coverage (rust-lang#2612)
Co-authored-by: Jaisurya Nanduri <[email protected]>
1 parent a5e8945 commit 13bfdd8

File tree

2 files changed

+173
-0
lines changed

2 files changed

+173
-0
lines changed

‎rfc/src/SUMMARY.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,5 @@
1212
- [0004-loop-contract-synthesis](rfcs/0004-loop-contract-synthesis.md)
1313
- [0005-should-panic-attr](rfcs/0005-should-panic-attr.md)
1414
- [0006-unstable-api](rfcs/0006-unstable-api.md)
15+
- [0007-global-conditions](rfcs/0007-global-conditions.md)
16+
- [0008-line-coverage](rfcs/0008-line-coverage.md)

‎rfc/src/rfcs/0008-line-coverage.md

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
- **Feature Name:** Line coverage (`line-coverage`)
2+
- **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2610>
3+
- **RFC PR:** <https://github.com/model-checking/kani/pull/2609>
4+
- **Status:** Unstable
5+
- **Version:** 0
6+
- **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2609> (Kani) + <https://github.com/model-checking/kani-vscode-extension/pull/122> (Kani VS Code Extension)
7+
8+
-------------------
9+
10+
## Summary
11+
12+
Add verification-based line coverage reports to Kani.
13+
14+
## User Impact
15+
16+
Nowadays, users can't easily obtain verification-based coverage reports in Kani.
17+
Generally speaking, coverage reports show which parts of the code under verification are covered and which are not.
18+
Because of that, coverage is often seen as a great metric to determine the quality of a verification effort.
19+
20+
Moreover, some users prefer using coverage information for harness development and debugging.
21+
That's because coverage information provides users with more familiar way to interpret verification results.
22+
23+
This RFC proposes adding a new option for verification-based line coverage reports to Kani.
24+
As mentioned earlier, we expect users to employ this coverage-related option on several stages of a verification effort:
25+
* **Learning:** New users are more familiar with coverage reports than property-based results.
26+
* **Development:** Some users prefer coverage results to property-based results since they are easier to interpret.
27+
* **CI Integration**: Users may want to enforce a minimum percentage of code coverage for new contributions.
28+
* **Debugging:** Users may find coverage reports particularly helpful when inputs are over-constrained (missing some corner cases).
29+
* **Evaluation:** Users can easily evaluate where and when more verification work is needed (some projects aim for 100% coverage).
30+
31+
Moreover, adding this option directly to Kani, instead of relying on another tools, is likely to:
32+
1. Increase the speed of development
33+
2. Improve testing for coverage features
34+
35+
Which translates into faster and more reliable coverage options for users.
36+
37+
## User Experience
38+
39+
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.
40+
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.
41+
42+
### High-level changes
43+
44+
For the first version, this experimental feature will report verification results along coverage reports.
45+
Because of that, we'll add a new section `Coverage results` that shows coverage results for each individual harness.
46+
47+
In the following, we describe an experimental output format.
48+
Note that the final output format and overall UX is to be determined.
49+
50+
### Experimental output format for coverage results
51+
52+
The `Coverage results` section for each harness will produce coverage information in a CSV format as follows:
53+
```
54+
<file>, <line>, <status>
55+
```
56+
where `<status>` is either `FULL`, `PARTIAL` or `NONE`.
57+
58+
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.
59+
60+
**Users are not expected to consume this output directly.**
61+
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).
62+
63+
How to activate and display coverage information in the extension is out of scope for this RFC.
64+
That said, a proof-of-concept implementation is available [here](https://github.com/model-checking/kani-vscode-extension/pull/122).
65+
66+
## Detailed Design
67+
68+
### Architecture
69+
70+
We will add a new unstable `--coverage` verification option to Kani which will require `-Z line-coverage` until this feature is stabilized.
71+
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].
72+
This option will be supplied by `kani-driver` when the `--coverage` option is selected.
73+
These options will cause Kani to inject coverage checks during compilation and postprocess them to produce the coverage results sections described earlier.
74+
75+
### Coverage Checks
76+
77+
Coverage checks are a new class of checks similar to [`cover` checks](https://model-checking.github.io/kani/rfc/rfcs/0003-cover-statement.html).
78+
The main difference is that users cannot directly interact with coverage checks (i.e., they cannot add or remove them manually).
79+
Coverage checks are encoded as an `assert(false)` statement (to test reachability) with a fixed description.
80+
In addition, coverage checks are:
81+
* Hidden from verification results.
82+
* Postprocessed to produce coverage results.
83+
84+
In the following, we describe the injection and postprocessing procedures to generate coverage results.
85+
86+
#### Injection of Coverage Checks
87+
88+
The injection of coverage checks will be done while generating code for basic blocks.
89+
This allows us to add one coverage check before each statement and terminator, which provides the most accurate results[^coverage-experiments].
90+
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].
91+
92+
#### Postprocessing Coverage Checks
93+
94+
The injection of coverage checks often results in one or more checks per line (assuming a well-formatted program).
95+
We'll postprocess these checks so for each line
96+
- if all checks are `SATISFIED`: return `FULL`
97+
- if all checks are `UNSATISFIED`: return `NONE`
98+
- otherwise: return `PARTIAL`
99+
100+
We won't report coverage status for lines which don't include a coverage check.
101+
102+
## Rationale and alternatives
103+
104+
### Benefits from a native coverage solution
105+
106+
Kani has relied on [`cbmc-viewer`](https://github.com/model-checking/cbmc-viewer) to report coverage information since the beginning.
107+
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.
108+
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)).
109+
110+
However, it's possible for Kani to report coverage information without `cbmc-viewer`, as explained before.
111+
This would give Kani control on both ends:
112+
* **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)).
113+
* **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.
114+
115+
#### Coverage through `cbmc-viewer`
116+
117+
As an alternative, we could fix and use `cbmc-viewer` to report line coverage.
118+
119+
Most of the issues with `cbmc-viewer` are generally due to:
120+
1. Missing locations due to non-propagation of locations in either Kani or CBMC.
121+
2. Differences in the definition of a basic block in CBMC and Rust's MIR.
122+
3. Scarce documentation for coverage-related options (i.e., `--cover <option>`) in CBMC.
123+
4. Limited testing with Rust code in `cbmc-viewer`.
124+
125+
Note that (1) is not exclusive to coverage results from `cbmc-viewer`.
126+
Finding checks with missing locations and propagating them if possible (as suggested in [this comment](https://github.com/model-checking/kani/issues/2048#issuecomment-1599680694)) should be done regardless of the approach used for line coverage reports.
127+
128+
In contrast, (2) and (3) can be considered the main problems for Kani contributors to develop coverage options on top of `cbmc-viewer` and CBMC.
129+
It's not clear how much effort this would involve, but (3) is likely to require substantial documentation contributions.
130+
But (4) shouldn't be an issue if we decided to invest in `cbmc-viewer`.
131+
132+
Finally, the following downside must be considered:
133+
`cbmc-viewer` can report line coverage but **the path to report region-based coverage may involve a complete rewrite**.
134+
135+
#### Other output formats
136+
137+
One of the long-term goals for this feature is to provide a UX that is familiar for users.
138+
This is particularly relevant when talking about output formats.
139+
Some services and frameworks working with certain coverage output formats have become quite popular.
140+
141+
However, this version doesn't consider common output formats (i.e., GCOV or LCOV) since coverage results will only be consumed by the Kani VS Code Extension at first.
142+
But other output formats will be considered in the future.
143+
144+
## Open questions
145+
146+
Open questions:
147+
* Do we want to report line coverage as `COVERED`/`UNCOVERED` or `FULL`/`PARTIAL`/`NONE`?
148+
* Should we report coverage results and verification results or not? Doing both is likely to result in worse performance. We have to perform an experimental evaluation with hard benchmarks.
149+
* Should we instrument dependencies or not? Doing so is likely to result in worse performance. We have to perform an experimental evaluation.
150+
* What should be the final UX for this feature? For instance, we could print a coverage summary and generate a report file per harness. But it's not clear if individual results are relevant to users, so another possibility is to automatically combine results.
151+
* What's the most appropriate and well-established output format we can emit?
152+
* Determine if there are cases in which coverage information is confusing for users (due to, e.g., constant propagation or other compiler optimizations). How can work around such cases?
153+
* Do we want to report coverage information for dependencies? For CI, most users may be only interested in their code. Most coverage frameworks have an aggregation tool with [an option to exclude dependencies](https://doc.rust-lang.org/rustc/instrument-coverage.html#compiling-with-coverage-enabled) from coverage metrics.
154+
155+
Feedback to gather before stabilization:
156+
* Compare the injection-based approach in this RFC with [Rust's instrument-based code coverage](https://doc.rust-lang.org/rustc/instrument-coverage.html)?
157+
158+
159+
## Future possibilities
160+
161+
We expect many incremental improvements in the coverage area:
162+
1. Consuming the output produced in coverage results from the [Kani VS Code extension](https://github.com/model-checking/kani-vscode-extension).
163+
2. Building a tool that produces coverage results by combining the coverage results of more than one harness.
164+
3. Including span information in coverage checks and building region-based coverage reports.
165+
4. Adding new user-requested coverage formats such as GCOV [#1706](https://github.com/model-checking/kani/issues/1706) or LCOV [#1777](https://github.com/model-checking/kani/issues/1777).
166+
167+
[^coverage-experiments]: We have experimented with different options for injecting coverage checks.
168+
For example, we have tried injecting one before each basic block, or one before each statement, etc.
169+
The proposed option (one before each statement AND each terminator) gives us the most accurate results.
170+
171+
[^coverage-api]: In particular, comments in [`CoverageSpan`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_transform/coverage/spans/struct.CoverageSpan.html) and [`generate_coverage_spans`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_transform/coverage/spans/struct.CoverageSpans.html#method.generate_coverage_spans) hint that the initial set of spans come from `Statement`s and `Terminators`. [This comment](https://github.com/model-checking/kani/pull/2612#issuecomment-1646312827) goes in detail about the attempt to use the compiler APIs.

0 commit comments

Comments
 (0)