From ae64a17b36a08f409d302b7452a96b6be861b26b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 26 Apr 2024 14:25:37 +0000 Subject: [PATCH 01/21] Move content into new RFC file --- rfc/src/rfcs/0008-line-coverage.md | 2 +- rfc/src/rfcs/0010-source-coverage.md | 300 +++++++++++++++++++++++++++ 2 files changed, 301 insertions(+), 1 deletion(-) create mode 100644 rfc/src/rfcs/0010-source-coverage.md diff --git a/rfc/src/rfcs/0008-line-coverage.md b/rfc/src/rfcs/0008-line-coverage.md index d2bedab8bdef..a0f287bee96e 100644 --- a/rfc/src/rfcs/0008-line-coverage.md +++ b/rfc/src/rfcs/0008-line-coverage.md @@ -1,7 +1,7 @@ - **Feature Name:** Line coverage (`line-coverage`) - **Feature Request Issue:** - **RFC PR:** -- **Status:** Unstable +- **Status:** Cancelled - **Version:** 0 - **Proof-of-concept:** (Kani) + (Kani VS Code Extension) diff --git a/rfc/src/rfcs/0010-source-coverage.md b/rfc/src/rfcs/0010-source-coverage.md new file mode 100644 index 000000000000..dfb5fbf90e69 --- /dev/null +++ b/rfc/src/rfcs/0010-source-coverage.md @@ -0,0 +1,300 @@ +- **Feature Name:** Source-based code coverage (`source-coverage`) +- **Feature Request Issue:** +- **RFC PR:** +- **Status:** Under Review +- **Version:** 2 +- **Proof-of-concept:** (Kani) + (`kani-cov`) + +------------------- + +## Summary + +A source-based code coverage feature for Kani built on top of Rust's coverage instrumentation. + +## User Impact + +Nowadays, users can't easily obtain verification-based coverage reports in Kani. +Generally speaking, these reports show which parts of the code under verification are covered and which are not. +Because of that, users rely on these reports to ensure that their harnesses are sound +---that is, that properties are checked for the entire body of code they're expecting to cover. + +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. + +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. + +### Update: from line to source coverage + +In the previous version of this RFC, we introduced and made available a line coverage option in Kani. +This option has since then allowed us to gather more data around the expectations for a coverage option in Kani. + +For example, the line coverage output we produced wasn't easy to interpret without knowing some implementation details. +Aside from that, the feature requested in [#2795](https://github.com/model-checking/kani/issues/2795) +alludes to the need of providing coverage-specific tooling in Kani. +Nevertheless, as captured in [#2640](https://github.com/model-checking/kani/issues/2640), +source-based coverage results provide the clearest and most precise coverage information. + +In this RFC, we propose an integration with [Rust's source-based code coverage instrumentation](https://doc.rust-lang.org/rustc/instrument-coverage.html). +The integration would allow us to report source-based code coverage results from Kani. +Also, we propose adding a new user-facing, coverage-focused tool called `kani-cov`. +The tool would allow users to process coverage results generated by Kani and produce +coverage artifacts such as summaries and reports according to their preferences. +In the [next section](#user-experience), we'll explain in more detail how we +expect `kani-cov` to assist with coverage-related tasks. + +With these changes, we expect our coverage options to become more flexible, precise and efficient. +In the [last section](#future-possibilities) of this RFC, +we'll also discuss the requirements for a potential integration of this coverage feature with the LLVM toolchain. + +## User Experience + +The proposed coverage workflow reproduces that of the most popular coverage frameworks. +First, let's delve into the LLVM coverage workflow, followed by an explanation of our proposal. + +### The LLVM code coverage workflow + +The LLVM project is home to one of the most popular code coverage frameworks. +The workflow associated to the LLVM framework is described in the documentation for [source-based code coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)[^note-source], but we briefly describe it here to better relate it with our proposal. + +In short, the LLVM code coverage workflow follows three steps: + 1. **Compiling with coverage enabled.** This causes the compiler to generate an instrumented program. + 2. **Running the instrumented program.** This generates binary-encoded `.profraw` files. + 3. **Using tools to aggregate and export coverage information into other formats.** + +When working in a `cargo` project, step 1 can be done through this command: + +```sh +RUSTFLAGS='-Cinstrument-coverage' cargo build +``` + +The same flag must to be used for step 2: + +```sh +RUSTFLAGS='-Cinstrument-coverage' cargo run +``` + +This should populate the directory with at least one `.profraw` file. +Each `.profraw` file corresponds to a specific source code file in your project. + +At this point, we'll have produced the artifacts that we generally require for the LLVM tools: + 1. **The instrumented binary** which, in addition to the instrumented program, + contains additional information (e.g., the coverage mappings) required to + interpret the profiling results. + 2. **The `.profraw` files** which essentially includes the profiling results + (counter and expression values) for each function of the corresponding source + code file. + +For step 3, the commands will depend on what kind of results we want. +Most likely we will have to merge the `.profraw` files and produce a `.profdata` file as follows: + +```sh +llvm-profdata merge -sparse *.profraw -o output.profdata +``` + +Then, we can use a command such as + +```sh +llvm-cov show target/debug/binary —instr-profile=output.profdata -show-line-counts-or-regions +``` + +to visualize the code coverage through the terminal as in the image: + +![Source-based code coverage with `llvm-cov`](https://github.com/model-checking/kani/assets/73246657/4f8a973d-8977-4c0b-822d-e73ed6d223aa) + +or the command + +```sh +llvm-cov report target/debug/binary --instr-profile=output.profdata --show-region-summary +``` + +to produce coverage summaries like this: + +``` +Filename Regions Missed Regions Cover Functions Missed Functions Executed Lines Missed Lines Cover Branches Missed Branches Cover +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +/long/long/path/to/my/project/binary/src/main.rs 9 3 66.67% 3 1 66.67% 14 4 71.43% 0 0 - +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +TOTAL 9 3 66.67% 3 1 66.67% 14 4 71.43% 0 0 - +``` + +[^note-source]: The LLVM project refers to their own coverage feature as "source-based code coverage". +It's not rare to see the term "region coverage" being used instead to refer to the same thing. +That's because LLVM's source-based code coverage feature can report coverage for code regions, +but other coverage frameworks don't support the concept of code regions. + +### The Kani coverage workflow + +The proposed Kani coverage workflow imitates the LLVM coverage workflow as much as possible. + +The two main components of the Kani coverage workflow will be the following: + 1. A new subcommand `cov` that drives the coverage workflow in Kani and + produces machine-readable coverage results. + 2. A new tool `kani-cov` that consumes the machine-readable coverage results + emitted by Kani to produce human-readable results in the desired format(s). + +Therefore, the first part of the coverage workflow will be managed by Kani. +Then, in the other part, we will use the `kani-cov` tool to produce the coverage +output(s) we're interested in. + +In the following, we describe each one of these components in more detail. + +#### The `-cov` option + +The coverage workflow will be kicked off through a new `-cov` option: + +```sh +cargo kani -cov +``` + +The main difference with respect to the regular verification workflow is that, +at the end of the verification-based coverage run, Kani will generate two types +of files: + - One single file `.kanimap` file for the project. This file will contain the + coverage mappings for the project's source code. + - One `.kaniraw` file for each harness. This file will contain the + verification-based results for the coverage-oriented properties corresponding + to a given harness. + +Note that `.kaniraw` files correspond to `.profraw` files in the LLVM coverage +workflow. Similarly, the `.kanimap` file corresponds to the coverage-related +information that's embedded into the project's binaries in the LLVM coverage +workflow.[^note-kanimap] + +The files will be written into a new timestamped directory associated with the +coverage run. The path to this directory will be printed to standard output in +by default. For example, the [draft implementation](https://github.com/model-checking/kani/pull/3119) +writes the coverage files into the `target/kani//cov/` directory. + +Users aren't expected to read the information in any of these files. +Therefore, there's no need to restrict their format. +The [draft implementation](https://github.com/model-checking/kani/pull/3119) +uses the JSON format but we might consider using a binary format if it doesn't +scale. + +[^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). +The [draft implementation of `kani-cov`](https://github.com/model-checking/kani/pull/3121) +simply reads the source files referred to by the code coverage checks, but it +doesn't get information about code trimmed out by the MIR linker. + +#### The `kani-cov` tool + +The `kani-cov` tool will be used to process coverage information generated by +Kani and produce coverage outputs as indicated by the user. +Hence, the `kani-cov` tool corresponds to the set of LLVM tools +(`llvm-profdata`, `llvm-cov`, etc.) that are used to produce coverage outputs +through the LLVM coverage workflow. + +In contrast to LLVM, we'll have a single tool for all Kani coverage-related needs. +We suggest that the tool initially offers three subcommands[^note-export]: + - `merge`: to combine the coverage results of one or more `.kaniraw` files into + a single `.kanicov` file, which will be required for the other subcommands. + - `report`: to display a summary of the coverage results. + - `show`: to produce source-based code coverage reports in human-readable formats (e.g., HTML). + + +Let's assume that we've run `cargo kani cov` and generated coverage files in the `my-coverage` folder. +Then, we'd use `kani-cov` as follows to combine the coverage results[^note-exclude] for all harnesses: + +```sh +kani-cov merge my-coverage/*.kaniraw -o my-coverage.kanicov +``` + +Let's say the user is first interested in reading a coverage summary through the terminal. +They will have to use the `report` command for that: + +```sh +kani-cov report my-coverage/default.kanimap -instr-profile=my-coverage.kanicov --show-summary +``` + +The command could print a coverage summary like: + +``` +| Filename | Regions | Missed Regions | Cover | Functions | ... +| -------- | ------- | -------------- | ----- | --------- | ... +| main.rs | 9 | 3 | 66.67 | 3 | ... +[...] +``` + +Now, let's say the user wants to produce an HTML report of the coverage results. +They will have to use the `show` command for that: + +```sh +kani-cov show my-coverage/default.kanimap -format=html -instr-profile=my-coverage.kanicov -o coverage-report +``` + +This time, the command will generate a `coverage-report` folder including a +browsable HTML webpage that highlights the regions covered in the source +according to the coverage results in `my-coverage.kanicov`. + +[^note-export]: The `llvm-cov` tool includes the option [`gcov`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-gcov) to export into GCC's coverage format [Gcov](https://en.wikipedia.org/wiki/Gcov), +and the option [`export`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-export) to export into the LCOV format. +I'd strongly recommend against adding format-specific options to `kani-cov` +unless there are technical reasons to do so. + +[^note-exclude]: Options to exclude certain coverage results (e.g, from the standard library) will likely be part of this option. + +#### Integration with the Kani VS Code Extension + +We will update the coverage feature of the +[Kani VS Code Extension](https://github.com/model-checking/kani-vscode-extension) +to follow this new coverage workflow. +In other words, the extension will first run Kani with the `-cov` option and +use `kani-cov` to produce a `.kanicov` file with the coverage results. +The extension will consume the source-based code coverage results and +highlight region coverage in the source code seen from VS Code. + +We could also consider other coverage-related features in order to enhance the +experience through the Kani VS Code Extension. For example, we could +automatically show the percentage of covered regions in the status bar by +additionally extracting a summary of the coverage results. + +Finally, we could also consider an integration with other code coverage tools. +For example, if we wanted to integrate with the VS Code extensions +[Code Coverage](https://marketplace.visualstudio.com/items?itemName=markis.code-coverage) or +[Coverage Gutters](https://marketplace.visualstudio.com/items?itemName=ryanluker.vscode-coverage-gutters), +we would only need to extend `kani-cov` to export coverage results to the LCOV +format or integrate Kani with LLVM tools as discussed in [Integration with LLVM](#integration-with-llvm). + +## Detailed Design + +THIS SECTION INTENTIONALLY LEFT BLANK. + +## Rationale and alternatives + +### Other coverage implementations + +In a previous version of this feature, we used an ad-hoc coverage implementation. +In addition to being very inefficient[^note-benchmarks], the line-based coverage +results were not trivial to interpret by users. +At the moment, there's only another unstable, GCC-compatible code coverage implementation +based on the Gcov format. The Gcov format is line-based so it's not able +to report region coverage results. +In other words, it's not as advanced nor precise as the source-based implementation. + +[^note-benchmarks]: Actual performance benchmarks to follow in [#3119](https://github.com/model-checking/kani/pull/3119). + +## Open questions + + - Do we want to instrument dependencies by default? Preliminary benchmarking results show a slowdown of 100% and greater. + More evaluations are required to determine how we handle instrumentation for dependencies, and what options we might want + to provide to users. + - How do we handle features/options for `kani-cov`? In particular, do we need more details in this RFC? + +## Future possibilities + +### Integration with LLVM + +We don't pursue an integration with the LLVM framework in this RFC. +We recommend against doing so at this time due to various technical limitations. +In a future revision, I'll explain these limitations and how we can make steps to overcome them. From d1ab79a0c65555fd3ec3faf91acb546a9a522790 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 26 Apr 2024 14:47:10 +0000 Subject: [PATCH 02/21] Link to previous work (line coverage) --- rfc/src/rfcs/0010-source-coverage.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0010-source-coverage.md b/rfc/src/rfcs/0010-source-coverage.md index dfb5fbf90e69..fe2bcba64693 100644 --- a/rfc/src/rfcs/0010-source-coverage.md +++ b/rfc/src/rfcs/0010-source-coverage.md @@ -2,7 +2,7 @@ - **Feature Request Issue:** - **RFC PR:** - **Status:** Under Review -- **Version:** 2 +- **Version:** 1 - **Proof-of-concept:** (Kani) + (`kani-cov`) ------------------- @@ -36,7 +36,8 @@ Which translates into faster and more reliable coverage options for users. ### Update: from line to source coverage -In the previous version of this RFC, we introduced and made available a line coverage option in Kani. +In our first attempt to add a coverage feature fully managed by Kani, we introduced and made available a line coverage option +(see [RFC: Line coverage](0008-line-coverage.md) for more details). This option has since then allowed us to gather more data around the expectations for a coverage option in Kani. For example, the line coverage output we produced wasn't easy to interpret without knowing some implementation details. @@ -54,6 +55,7 @@ In the [next section](#user-experience), we'll explain in more detail how we expect `kani-cov` to assist with coverage-related tasks. With these changes, we expect our coverage options to become more flexible, precise and efficient. +These options are expected to replace the previous options available through the line coverage feature. In the [last section](#future-possibilities) of this RFC, we'll also discuss the requirements for a potential integration of this coverage feature with the LLVM toolchain. From f6cf59eb8611f976eee87b0f48156c35ee8025f6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 26 Apr 2024 15:07:59 +0000 Subject: [PATCH 03/21] Increment ID and add to `SUMMARY.md` --- rfc/src/SUMMARY.md | 1 + .../rfcs/{0010-source-coverage.md => 0011-source-coverage.md} | 0 2 files changed, 1 insertion(+) rename rfc/src/rfcs/{0010-source-coverage.md => 0011-source-coverage.md} (100%) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index f8d5dc5639f5..83cfaed0a01d 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -15,3 +15,4 @@ - [0007-global-conditions](rfcs/0007-global-conditions.md) - [0008-line-coverage](rfcs/0008-line-coverage.md) - [0009-function-contracts](rfcs/0009-function-contracts.md) +- [0011-source-coverage](rfcs/0011-source-coverage.md) diff --git a/rfc/src/rfcs/0010-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md similarity index 100% rename from rfc/src/rfcs/0010-source-coverage.md rename to rfc/src/rfcs/0011-source-coverage.md From 7e73de893981710c3f45f41c83dcdfe58ec37cbd Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 26 Apr 2024 19:17:24 +0000 Subject: [PATCH 04/21] Changes for a simpler UX --- rfc/src/rfcs/0011-source-coverage.md | 165 ++++++++++++++++++--------- 1 file changed, 108 insertions(+), 57 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index fe2bcba64693..f529f14ae53f 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -38,7 +38,7 @@ Which translates into faster and more reliable coverage options for users. In our first attempt to add a coverage feature fully managed by Kani, we introduced and made available a line coverage option (see [RFC: Line coverage](0008-line-coverage.md) for more details). -This option has since then allowed us to gather more data around the expectations for a coverage option in Kani. +This option has since then allowed us to gather more data around the expectations for a coverage feature in Kani. For example, the line coverage output we produced wasn't easy to interpret without knowing some implementation details. Aside from that, the feature requested in [#2795](https://github.com/model-checking/kani/issues/2795) @@ -61,7 +61,7 @@ we'll also discuss the requirements for a potential integration of this coverage ## User Experience -The proposed coverage workflow reproduces that of the most popular coverage frameworks. +The proposed experience is partially inspired by that of the most popular coverage frameworks. First, let's delve into the LLVM coverage workflow, followed by an explanation of our proposal. ### The LLVM code coverage workflow @@ -137,86 +137,90 @@ but other coverage frameworks don't support the concept of code regions. ### The Kani coverage workflow -The proposed Kani coverage workflow imitates the LLVM coverage workflow as much as possible. - The two main components of the Kani coverage workflow will be the following: - 1. A new subcommand `cov` that drives the coverage workflow in Kani and - produces machine-readable coverage results. - 2. A new tool `kani-cov` that consumes the machine-readable coverage results - emitted by Kani to produce human-readable results in the desired format(s). - -Therefore, the first part of the coverage workflow will be managed by Kani. -Then, in the other part, we will use the `kani-cov` tool to produce the coverage -output(s) we're interested in. + 1. The existing `--coverage` flag that drives the coverage workflow in Kani and + produces basic coverage results by default. + 2. A new subcommand `cov` that allows users to further process raw coverage + information emitted by Kani to produce customized coverage results (i.e., + different to the ones produced by default with the `--coverage` option). + +In constrast to the LLVM workflow, where human-readable coverage results can +be produced only after a sequence of LLVM tool commands, we provide some +coverage results by default. +This aligns better with our UX philosophy, and removes the need for a wrapper +around our coverage features like +[`cargo-llvm-cov`](https://github.com/taiki-e/cargo-llvm-cov). +Alternatively, the `cov` subcommand offers the ability required to +produce more specific coverage results if needed. +We anticipate the `cov` subcommand being particularly useful in less +standard project setups, giving the users the flexibility required to produce +coverage results tailored to their specific needs. In the following, we describe each one of these components in more detail. -#### The `-cov` option +#### The `--coverage` option -The coverage workflow will be kicked off through a new `-cov` option: +The default coverage workflow will be kicked off through the unstable +`--coverage` option: ```sh -cargo kani -cov +cargo kani --coverage -Zsource-coverage ``` The main difference with respect to the regular verification workflow is that, -at the end of the verification-based coverage run, Kani will generate two types -of files: - - One single file `.kanimap` file for the project. This file will contain the - coverage mappings for the project's source code. - - One `.kaniraw` file for each harness. This file will contain the - verification-based results for the coverage-oriented properties corresponding - to a given harness. +at the end of the verification-based coverage run, Kani will generate two coverage +results: + - A coverage summary corresponding to the coverage achieved by the harnesses + included in the verification run. This summary will be printed after the + verification output. + - A coverage report corresponding to the coverage achieved by the harnesses + included in the verification run. The report will be placed in the same target + directory where the raw coverage files are put. The path to the report will + also be printed after the verification output. + +Therefore, a typical `--coverage` run could look like this: -Note that `.kaniraw` files correspond to `.profraw` files in the LLVM coverage -workflow. Similarly, the `.kanimap` file corresponds to the coverage-related -information that's embedded into the project's binaries in the LLVM coverage -workflow.[^note-kanimap] +``` +VERIFICATION:- SUCCESSFUL -The files will be written into a new timestamped directory associated with the -coverage run. The path to this directory will be printed to standard output in -by default. For example, the [draft implementation](https://github.com/model-checking/kani/pull/3119) -writes the coverage files into the `target/kani//cov/` directory. +Coverage Results: -Users aren't expected to read the information in any of these files. -Therefore, there's no need to restrict their format. -The [draft implementation](https://github.com/model-checking/kani/pull/3119) -uses the JSON format but we might consider using a binary format if it doesn't -scale. +| Filename | Regions | Missed Regions | Cover | Functions | Missed Functions | Cover | +| -------- | ------- | -------------- | ----- | --------- | ---------------- | ----- | +| main.rs | 9 | 3 | 66.67 | 3 | 1 | 33.33 | +| file.rs | 11 | 5 | 45.45 | 2 | 1 | 50.00 | -[^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). -The [draft implementation of `kani-cov`](https://github.com/model-checking/kani/pull/3121) -simply reads the source files referred to by the code coverage checks, but it -doesn't get information about code trimmed out by the MIR linker. +Coverage report available in target/kani/x86_64-unknown-linux-gnu/cov/kani_2024-04-26_15-30-00/report/index.html +``` -#### The `kani-cov` tool +#### The `cov` subcommand -The `kani-cov` tool will be used to process coverage information generated by -Kani and produce coverage outputs as indicated by the user. -Hence, the `kani-cov` tool corresponds to the set of LLVM tools +The `cov` subcommand will be used to process raw coverage information generated +by Kani and produce coverage outputs as indicated by the user. +Hence, the `cov` subcommand corresponds to the set of LLVM tools (`llvm-profdata`, `llvm-cov`, etc.) that are used to produce coverage outputs through the LLVM coverage workflow. -In contrast to LLVM, we'll have a single tool for all Kani coverage-related needs. -We suggest that the tool initially offers three subcommands[^note-export]: - - `merge`: to combine the coverage results of one or more `.kaniraw` files into - a single `.kanicov` file, which will be required for the other subcommands. - - `report`: to display a summary of the coverage results. - - `show`: to produce source-based code coverage reports in human-readable formats (e.g., HTML). +In contrast to LLVM, we'll have a single subcommand for all Kani coverage-related needs. +We suggest that the subcommand initially offers two options: + 1. An option to merge the coverage results from one or more files and a source + code snapshot[^note-snapshot] into a single file. + 2. An option to produce coverage outputs from coverage results, including summaries + or coverage reports in human-readable formats (e.g., HTML). - -Let's assume that we've run `cargo kani cov` and generated coverage files in the `my-coverage` folder. -Then, we'd use `kani-cov` as follows to combine the coverage results[^note-exclude] for all harnesses: +Let's assume that we've run `cargo kani --coverage -Zsource-coverage` and +generated coverage files in the `my-coverage` folder. Then, we'd use `cargo kani cov` +as follows to combine the coverage results[^note-exclude] for all harnesses: ```sh -kani-cov merge my-coverage/*.kaniraw -o my-coverage.kanicov +cargo kani cov --merge my-coverage/*.kaniraw -o my-coverage.kanicov ``` Let's say the user is first interested in reading a coverage summary through the terminal. They will have to use the `report` command for that: ```sh -kani-cov report my-coverage/default.kanimap -instr-profile=my-coverage.kanicov --show-summary +cargo kani cov --summary my-coverage/default.kanimap -instr-profile=my-coverage.kanicov ``` The command could print a coverage summary like: @@ -229,10 +233,10 @@ The command could print a coverage summary like: ``` Now, let's say the user wants to produce an HTML report of the coverage results. -They will have to use the `show` command for that: +They will have to use the `--report` command for that: ```sh -kani-cov show my-coverage/default.kanimap -format=html -instr-profile=my-coverage.kanicov -o coverage-report +cargo kani cov --report my-coverage/default.kanimap -format=html -instr-profile=my-coverage.kanicov -o coverage-report ``` This time, the command will generate a `coverage-report` folder including a @@ -246,6 +250,10 @@ unless there are technical reasons to do so. [^note-exclude]: Options to exclude certain coverage results (e.g, from the standard library) will likely be part of this option. +[^note-snapshot]: Source code snapshots are necessary to produce coverage +reports for items that otherwise are unreachable or have been sliced away during +the compilation process. + #### Integration with the Kani VS Code Extension We will update the coverage feature of the @@ -270,7 +278,50 @@ format or integrate Kani with LLVM tools as discussed in [Integration with LLVM] ## Detailed Design -THIS SECTION INTENTIONALLY LEFT BLANK. +Note: This section is still being worked on. Feel free to ignore it for now. + +### The Rust coverage instrumentation + +### The default coverage workflow + +In this section, we describe the default `--coverage` workflow from a +developer's point of view. This will hopefully help developers understand how +the different coverage components in Kani are connected. For example, we'll +describe the raw coverage information that gets produced throughout the default +`--coverage` workflow and define the basic `cov` commands that it will execute. + +The main difference with respect to the regular verification workflow is that, +at the end of the verification-based coverage run, Kani will generate two types +of files: + - One single file `.kanimap` file for the project. This file will contain the + coverage mappings for the project's source code. + - One `.kaniraw` file for each harness. This file will contain the + verification-based results for the coverage-oriented properties corresponding + to a given harness. + +Note that `.kaniraw` files correspond to `.profraw` files in the LLVM coverage +workflow. Similarly, the `.kanimap` file corresponds to the coverage-related +information that's embedded into the project's binaries in the LLVM coverage +workflow.[^note-kanimap] + +The files will be written into a new timestamped directory associated with the +coverage run. The path to this directory will be printed to standard output in +by default. For example, the [draft implementation](https://github.com/model-checking/kani/pull/3119) +writes the coverage files into the `target/kani//cov/` directory. + +Users aren't expected to read the information in any of these files. +Therefore, there's no need to restrict their format. +The [draft implementation](https://github.com/model-checking/kani/pull/3119) +uses the JSON format but we might consider using a binary format if it doesn't +scale. + +In addition, Kani will produce two types of coverage results: + 1. A coverage summary + +[^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). +The [draft implementation of `kani-cov`](https://github.com/model-checking/kani/pull/3121) +simply reads the source files referred to by the code coverage checks, but it +doesn't get information about code trimmed out by the MIR linker. ## Rationale and alternatives From 580fa33243b68bc3c7272d84592bc5e31e7d57a4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 31 Jul 2024 19:51:50 +0000 Subject: [PATCH 05/21] Add intro to "Design - coverage instrumentation" subsection --- rfc/src/rfcs/0011-source-coverage.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index f529f14ae53f..77ab978cdc06 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -282,6 +282,20 @@ Note: This section is still being worked on. Feel free to ignore it for now. ### The Rust coverage instrumentation +The Rust compiler includes two code coverage implementations: + * A source-based coverage implementation which uses LLVM's coverage + instrumentation to generate precise coverage data. This implementation can be + enabled with `-C instrument-coverage`. + * A Gcov-based coverage implementation that derives coverage data based on + DebugInfo. This implementation can be enabled with `-Z profile`. + +The [Instrumentation-based Code Coverage](https://doc.rust-lang.org/rustc/instrument-coverage.html) +chapter from the `rustc` book describes in detail how to enable and use the LLVM +instrumentation-based coverage feature. In contrast, the +[LLVM Source-Based Code Coverage](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html) +chapter from the `rustc` development guide documents how the LLVM +coverage instrumentation is performed in the Rust compiler. + ### The default coverage workflow In this section, we describe the default `--coverage` workflow from a From f934614871c5c32c1f6f3192a687cb072e3f85a5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 31 Jul 2024 20:16:34 +0000 Subject: [PATCH 06/21] Remaining intro and new subsections --- rfc/src/rfcs/0011-source-coverage.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 77ab978cdc06..ff2434bababe 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -296,6 +296,19 @@ instrumentation-based coverage feature. In contrast, the chapter from the `rustc` development guide documents how the LLVM coverage instrumentation is performed in the Rust compiler. +In this section, we will first summarize some information from the +[LLVM Source-Based Code Coverage](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html) +chapter, limited to details which are relevant to the development of the +source-based coverage feature in Kani. Then, we will explain how Kani taps into +the Rust coverage instrumentation to perform its own coverage instrumentation +and be able to report source-based code coverage results. This will also include +mentions to current issues with this implementation, which we plan to further +discuss in [Future possibilities](#future-possibilities). + +#### Understanding the Rust coverage instrumentation + +#### Integrating the instrumentation into Kani + ### The default coverage workflow In this section, we describe the default `--coverage` workflow from a From 9cab1084aecf7661ed7b4f5cf7c54e163be03a30 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 31 Jul 2024 21:35:11 +0000 Subject: [PATCH 07/21] Partial explanation of Rust instrumentation --- rfc/src/rfcs/0011-source-coverage.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index ff2434bababe..873bf268ff5c 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -307,6 +307,18 @@ discuss in [Future possibilities](#future-possibilities). #### Understanding the Rust coverage instrumentation +The LLVM coverage instrumentation is implemented in the Rust compiler as a +[MIR pass called `InstrumentCoverage`](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html#mir-pass-instrumentcoverage). + +**Note: Explain what result is important for Kani first** + +The MIR pass first builds a coverage-specific version of the MIR Control Flow +Graph (CFG) from the MIR. The initial version of this CFG is based on the MIR's +`BasicBlock`s, which then gets refined by combining blocks that can be chained +from a coverage-relevant point of view. The final version of the coverage CFG +can then be used to compute the mix of `Counter`s and `Expression`s that +represent the coverage information. + #### Integrating the instrumentation into Kani ### The default coverage workflow From 734f5838332f8fc6df8f73cf6b524fd640983013 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 1 Aug 2024 21:37:34 +0000 Subject: [PATCH 08/21] Complete subsection on Rust coverage instrumentation --- rfc/src/rfcs/0011-source-coverage.md | 43 ++++++++++++++++++++++++---- 1 file changed, 38 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 873bf268ff5c..778cd33edeed 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -310,14 +310,47 @@ discuss in [Future possibilities](#future-possibilities). The LLVM coverage instrumentation is implemented in the Rust compiler as a [MIR pass called `InstrumentCoverage`](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html#mir-pass-instrumentcoverage). -**Note: Explain what result is important for Kani first** - The MIR pass first builds a coverage-specific version of the MIR Control Flow Graph (CFG) from the MIR. The initial version of this CFG is based on the MIR's `BasicBlock`s, which then gets refined by combining blocks that can be chained -from a coverage-relevant point of view. The final version of the coverage CFG -can then be used to compute the mix of `Counter`s and `Expression`s that -represent the coverage information. +from a coverage-relevant point of view. The final version of the coverage CFG is +then used to determine where to inject the +[`StatementKind::Coverage`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Coverage) +statements in order to measure coverage for a single region coverage span. + +The injection of `StatementKind::Coverage` statements is the main result we are +interested in for the integration with Kani. Additionally, the instrumentation +will also attach the +[`FunctionCoverageInfo`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/struct.FunctionCoverageInfo.html) +structure to each function's body.[^note-coverage-info] +This result is also needed at the moment because coverage statements do not +include information on the code region they are supposed to cover. +However, `FunctionCoverageInfo` contains the +[coverage mappings](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/struct.Mapping.html), +which represent the relation between +[coverage counters](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html) +and code regions. + +As explained in [MIR Pass: +`InstrumentCoverage`](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html#mir-pass-instrumentcoverage), +many coverage statements will not be converted into a physical +counter[^note-physical-counter]. Instead, they will be converted into a +*coverage-counter expression* that can be calculated based on other coverage +counters. We highly recommend looking at the example in [MIR Pass: +`InstrumentCoverage`](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html#mir-pass-instrumentcoverage) +to better understand how this works. This optimization is mainly done for +performance reasons because incrementing a physical counter causes a +non-negligible overhead, especially within loops. Fortunately, the Rust coverage +instrumentation also computes the mix of `Counter`s and `Expression`s that make +up the coverage statements. + +[^note-coverage-info]: It is important to note that the StableMIR interface does + not include `FunctionCoverageInfo` in function bodies. Because of that, we + need to pull it from the internal `rustc` function bodies. + +[^note-physical-counter]: By *physical counter*, we refer to a global program +variable that is initialized to zero and incremented by one each time that the +execution goes through. #### Integrating the instrumentation into Kani From 6fbf8e8bfa6e2c893a84dc9edfd7be25a34087fb Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 2 Aug 2024 15:37:41 +0000 Subject: [PATCH 09/21] Format footnotes so it's clear they're footnotes --- rfc/src/rfcs/0011-source-coverage.md | 49 ++++++++++++++++------------ 1 file changed, 29 insertions(+), 20 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 778cd33edeed..fbe0479e6a01 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -130,10 +130,11 @@ Filename Regions Missed Regions TOTAL 9 3 66.67% 3 1 66.67% 14 4 71.43% 0 0 - ``` -[^note-source]: The LLVM project refers to their own coverage feature as "source-based code coverage". -It's not rare to see the term "region coverage" being used instead to refer to the same thing. -That's because LLVM's source-based code coverage feature can report coverage for code regions, -but other coverage frameworks don't support the concept of code regions. +[^note-source]: The LLVM project refers to their own coverage feature as + "source-based code coverage". It's not rare to see the term "region coverage" + being used instead to refer to the same thing. That's because LLVM's + source-based code coverage feature can report coverage for code regions, but + other coverage frameworks don't support the concept of code regions. ### The Kani coverage workflow @@ -243,16 +244,21 @@ This time, the command will generate a `coverage-report` folder including a browsable HTML webpage that highlights the regions covered in the source according to the coverage results in `my-coverage.kanicov`. -[^note-export]: The `llvm-cov` tool includes the option [`gcov`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-gcov) to export into GCC's coverage format [Gcov](https://en.wikipedia.org/wiki/Gcov), -and the option [`export`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-export) to export into the LCOV format. -I'd strongly recommend against adding format-specific options to `kani-cov` -unless there are technical reasons to do so. +[^note-export]: The `llvm-cov` tool includes the option + [`gcov`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-gcov) to + export into GCC's coverage format [Gcov](https://en.wikipedia.org/wiki/Gcov), + and the option + [`export`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-export) + to export into the LCOV format. I'd strongly recommend against adding + format-specific options to `kani-cov` unless there are technical reasons to + do so. -[^note-exclude]: Options to exclude certain coverage results (e.g, from the standard library) will likely be part of this option. +[^note-exclude]: Options to exclude certain coverage results (e.g, from the + standard library) will likely be part of this option. [^note-snapshot]: Source code snapshots are necessary to produce coverage -reports for items that otherwise are unreachable or have been sliced away during -the compilation process. + reports for items that otherwise are unreachable or have been sliced away + during the compilation process. #### Integration with the Kani VS Code Extension @@ -345,12 +351,12 @@ instrumentation also computes the mix of `Counter`s and `Expression`s that make up the coverage statements. [^note-coverage-info]: It is important to note that the StableMIR interface does - not include `FunctionCoverageInfo` in function bodies. Because of that, we - need to pull it from the internal `rustc` function bodies. + not include `FunctionCoverageInfo` in function bodies. Because of that, we + need to pull it from the internal `rustc` function bodies. [^note-physical-counter]: By *physical counter*, we refer to a global program -variable that is initialized to zero and incremented by one each time that the -execution goes through. + variable that is initialized to zero and incremented by one each time that + the execution goes through. #### Integrating the instrumentation into Kani @@ -390,10 +396,12 @@ scale. In addition, Kani will produce two types of coverage results: 1. A coverage summary -[^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). -The [draft implementation of `kani-cov`](https://github.com/model-checking/kani/pull/3121) -simply reads the source files referred to by the code coverage checks, but it -doesn't get information about code trimmed out by the MIR linker. +[^note-kanimap]: Note that the `.kanimap` generation isn't implemented in + [#3119](https://github.com/model-checking/kani/pull/3119). The [draft + implementation of + `kani-cov`](https://github.com/model-checking/kani/pull/3121) simply reads + the source files referred to by the code coverage checks, but it doesn't get + information about code trimmed out by the MIR linker. ## Rationale and alternatives @@ -407,7 +415,8 @@ based on the Gcov format. The Gcov format is line-based so it's not able to report region coverage results. In other words, it's not as advanced nor precise as the source-based implementation. -[^note-benchmarks]: Actual performance benchmarks to follow in [#3119](https://github.com/model-checking/kani/pull/3119). +[^note-benchmarks]: Actual performance benchmarks to follow in + [#3119](https://github.com/model-checking/kani/pull/3119). ## Open questions From 049f61036c9d80448ea240a95fc10f64399d95af Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 2 Aug 2024 17:15:37 +0000 Subject: [PATCH 10/21] A little more info. on counter kinds --- rfc/src/rfcs/0011-source-coverage.md | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index fbe0479e6a01..a825d4e269c9 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -346,9 +346,16 @@ counters. We highly recommend looking at the example in [MIR Pass: `InstrumentCoverage`](https://rustc-dev-guide.rust-lang.org/llvm-coverage-instrumentation.html#mir-pass-instrumentcoverage) to better understand how this works. This optimization is mainly done for performance reasons because incrementing a physical counter causes a -non-negligible overhead, especially within loops. Fortunately, the Rust coverage -instrumentation also computes the mix of `Counter`s and `Expression`s that make -up the coverage statements. +non-negligible overhead, especially within loops. + +The `StatementKind::Coverage` statements that are injected by the Rust coverage +instrumentation contain a [`CoverageKind`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html) field indicating the type of coverage counter. The variant +[`CounterIncrement`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html#variant.CounterIncrement) +represents physical counters, while +[`ExpressionUsed`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html#variant.ExpressionUsed) +represents the counter expressions that we just discussed. +Other variants such as `SpanMarker` or `BlockMarker` are not relevant to this +work since they should have been erased after the `InstrumentCoverage` pass. [^note-coverage-info]: It is important to note that the StableMIR interface does not include `FunctionCoverageInfo` in function bodies. Because of that, we From 459e15a80f5f1acf2b2d0e675e7de5cf28f79608 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 5 Aug 2024 21:17:27 +0000 Subject: [PATCH 11/21] Explanation of method (postprocess not included) --- rfc/src/rfcs/0011-source-coverage.md | 48 +++++++++++++++++++++++++++- 1 file changed, 47 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index a825d4e269c9..8b07e41c0b89 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -348,7 +348,7 @@ to better understand how this works. This optimization is mainly done for performance reasons because incrementing a physical counter causes a non-negligible overhead, especially within loops. -The `StatementKind::Coverage` statements that are injected by the Rust coverage +The (`StatementKind::`)`Coverage` statements that are injected by the Rust coverage instrumentation contain a [`CoverageKind`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html) field indicating the type of coverage counter. The variant [`CounterIncrement`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html#variant.CounterIncrement) represents physical counters, while @@ -367,6 +367,52 @@ work since they should have been erased after the `InstrumentCoverage` pass. #### Integrating the instrumentation into Kani +Now that we have explained what the Rust coverage instrumentation does at a high +level, we should be ready to discuss how it can be used from Kani. Here, we will +follow an approach where, during the codegen stage, we generate a Kani +reachability check for each code region and, after the verification stage, we +postprocess the information in those checks to generate the coverage +information. So this section will essentially be a retelling of the +implementation in [#3119](https://github.com/model-checking/kani/pull/3119), and +we will discuss variations/extensions of this approach in the +[appropriate](#rationale-and-alternatives) [sections](#future-possibilities). + +Clearly, the first step is adding `-C instrument-coverage` to the `rustc` flags +we use when calling the compiler to codegen. This flag enables the Rust coverage +instrumentation that we discussed earlier, resulting in + 1. the injection of + [`Coverage`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Coverage) + statements in the MIR code, and + 2. the inclusion of [`FunctionCoverageInfo`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/struct.FunctionCoverageInfo.html) in function bodies. + +The next step is handling the `Coverage` statements from `codegen_statement`. + +Each `Coverage` statement contains opaque coverage +information[^note-opaque-coverage] of the +[`CoverageKind`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CoverageKind.html) +type which can be processed to determine the type of coverage counter +(`CounterIncrement` for physical counters, `ExpressionUsed` for counter +expressions) and the ID number of the counter. These two pieces of information allow us to +uniquely identify the counter within a given function. For example, +`CounterIncrement(0)` would generally refer to the first physical counter in the +function. + +Unfortunately, the `CoverageKind` information does not tell us anything about +the code region that the counter covers. However, the code region information +can be pulled from the coverage mappings included in the `FunctionCoverageInfo` +that is attached to the (internal) function body. Note that the coverage +mappings includes information about all the coverage counters in a function, +even for counters which have been dropped. Matching the `CoverageKind` +information with that of the counters in the coverage mappings allows us to +retrieve the code region for any counter. + + +[^note-opaque-coverage]: The Rust compiler uses the `Opaque` type to prevent +others from interfacing with unstable types (e.g., the `Coverage` type +[here](https://github.com/rust-lang/rust/blob/f7eefec4e03f5ba723fbc04d94dbc1203b7c9bff/compiler/stable_mir/src/mir/body.rs#L389)). +Nonetheless, this can be worked around by serializing its contents and parsing +it back into an internal data type. + ### The default coverage workflow In this section, we describe the default `--coverage` workflow from a From bab8d91ad488af073c9e30abfcd5943d65052a1f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 6 Aug 2024 16:02:45 +0000 Subject: [PATCH 12/21] Finish integration subsection --- rfc/src/rfcs/0011-source-coverage.md | 60 ++++++++++++++++++++++++---- 1 file changed, 53 insertions(+), 7 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 8b07e41c0b89..5d68034031db 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -398,14 +398,60 @@ uniquely identify the counter within a given function. For example, function. Unfortunately, the `CoverageKind` information does not tell us anything about -the code region that the counter covers. However, the code region information -can be pulled from the coverage mappings included in the `FunctionCoverageInfo` -that is attached to the (internal) function body. Note that the coverage -mappings includes information about all the coverage counters in a function, -even for counters which have been dropped. Matching the `CoverageKind` -information with that of the counters in the coverage mappings allows us to -retrieve the code region for any counter. +the code region that the counter covers. However, data about the code region can +be pulled from the coverage mappings included in the `FunctionCoverageInfo` that +is attached to the (internal) function body. Note that the coverage mappings +includes information about all the coverage counters in a function, even for +counters which have been dropped. Matching the `CoverageKind` information with +that of the counters in the coverage mappings allows us to retrieve the code +region for any counter. + +Using all this data, we generate a coverage check that maintains the essence of +the coverage checks described in the +[RFC for line coverage](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html): + +> 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. + +Therefore, the last step is to postprocess the results from coverage checks to +produce coverage results. This is not too complicated to do since the checks +already include the counter information (type + ID) and the function name in +the check's description. If the span of the code region is also included +(this is what [#3119](https://github.com/model-checking/kani/pull/3119) is +currently doing), we can directly generate a primitive output like this: +``` + () + * - + * ... + * - +``` + +For example, for the test case in +[#3119](https://github.com/model-checking/kani/pull/3119) we report this: + +``` +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 +``` + +> **NOTE: This section has been written according to the implementation in +> [#3119](https://github.com/model-checking/kani/pull/3119), which currently +> produces a text-based output like the one shown above. There is ongoing work to +> store the coverage mappings in a separate file (as described in the next +> section), which would save us the need to attach code region data to the +> coverage checks.** [^note-opaque-coverage]: The Rust compiler uses the `Opaque` type to prevent others from interfacing with unstable types (e.g., the `Coverage` type From 9114e4502679b5b377312fdf0a6c14664dcd97ec Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 6 Aug 2024 18:19:02 +0000 Subject: [PATCH 13/21] Make clarification on coverage statements to instrument --- rfc/src/rfcs/0011-source-coverage.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 5d68034031db..43b453b9acba 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -406,9 +406,9 @@ counters which have been dropped. Matching the `CoverageKind` information with that of the counters in the coverage mappings allows us to retrieve the code region for any counter. -Using all this data, we generate a coverage check that maintains the essence of -the coverage checks described in the -[RFC for line coverage](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html): +Using all this data, for each coverage statement[^note-expression-integration] we generate a coverage check +that maintains the essence of the coverage checks described in the [RFC for line +coverage](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html): > 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). @@ -459,6 +459,12 @@ others from interfacing with unstable types (e.g., the `Coverage` type Nonetheless, this can be worked around by serializing its contents and parsing it back into an internal data type. +[^note-expression-integration]: We could follow an alternative approach where we +do not instrument each coverage statement, but only those that correspond to +physical counters. Unfortunately, doing so would lead to incorrect coverage +results due to the arithmetic nature of expression-based counters. We elaborate +on this topic in the later parts of this document. + ### The default coverage workflow In this section, we describe the default `--coverage` workflow from a From 3303b7f6b716b07b5565d00d825d2ea44cc70535 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 02:17:46 +0000 Subject: [PATCH 14/21] Complete subsection on LLVM integration --- rfc/src/rfcs/0011-source-coverage.md | 49 +++++++++++++++++++++++++--- 1 file changed, 45 insertions(+), 4 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 43b453b9acba..a094a8e9c8af 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -363,7 +363,7 @@ work since they should have been erased after the `InstrumentCoverage` pass. [^note-physical-counter]: By *physical counter*, we refer to a global program variable that is initialized to zero and incremented by one each time that - the execution goes through. + the execution passes through. #### Integrating the instrumentation into Kani @@ -523,6 +523,8 @@ In other words, it's not as advanced nor precise as the source-based implementat [^note-benchmarks]: Actual performance benchmarks to follow in [#3119](https://github.com/model-checking/kani/pull/3119). +### Optimization with coverage-counter expressions + ## Open questions - Do we want to instrument dependencies by default? Preliminary benchmarking results show a slowdown of 100% and greater. @@ -534,6 +536,45 @@ In other words, it's not as advanced nor precise as the source-based implementat ### Integration with LLVM -We don't pursue an integration with the LLVM framework in this RFC. -We recommend against doing so at this time due to various technical limitations. -In a future revision, I'll explain these limitations and how we can make steps to overcome them. +As part of this work, we explored a potential integration with the LLVM +framework. The idea behind such an integration would essentially involve +producing coverage results in formats compatible with the LLVM framework (e.g., +the `.profraw` format). The main advantage of integrating with the LLVM +framework in this way is that we would not need a tool like `kani-cov` to +aggregate coverage results; we could just use LLVM tools such as `llvm-profdata` +and `llvm-cov` to consume them. + +However, at this time we recommend against integrating with LLVM due to these reasons: + 1. Generating the instrumented binary used in the [LLVM coverage + workflow](#the-llvm-code-coverage-workflow) requires a standard `rustc` + compilation with `--cfg kani` in addition to other flags including `-C + instrument-coverage`. This is likely to result in compilation errors since the + standard `rustc` backend cannot produce code for Kani APIs, for example. + 2. Producing the `.profraw` files requires executing the instrumented binary at + least once. This would be an issue for Rust projects which assume a particular + environment for their execution. + 3. There are no stable interfaces to create or modify files in formats + compatible with the LLVM framework. Even though the documentation for the [LLVM + Code Coverage Mapping Format](https://llvm.org/docs/CoverageMappingFormat.html) + is excellent, the easiest way to interact with files on these format is through + LLVM tools (e.g., + [`llvm-cov`](https://github.com/llvm/llvm-project/tree/main/llvm/tools/llvm-cov)) + which bring in many other LLVM dependencies. During our exploration, we + attempted to decode and re-encode files in the `.profraw` to set the counter + data to the values obtained during verification. To this end, we tried tools + like [`llvm-profparser`](https://github.com/xd009642/llvm-profparser/) which + can be used as a replacement for `llvm-profdata` and `llvm-cov` but failed to + parse coverage files emitted by the Rust compiler (this is also related to the + next point). Another crate that we used is + [`coverage-dump`](https://github.com/rust-lang/rust/tree/master/src/tools/coverage-dump), + a recent tool in the Rust compiler used for testing purposes. `coverage-dump` + extracts coverage mappings from LLVM IR assembly files (i.e., human-readable + `*.ll` files) but does not work with the binary-encoded formats. Finally, we + also built some ad-hoc tooling to perform these modifications but it soon + became evident that we would need to develop it further in order to handle any + program. + 4. LLVM releases a new version approximately every six months. This would + likely result in another "toolchain update" problem for Kani in order to + provide compatibility with newer LLVM versions. Moreover, the Rust compiler + supplies their own version of LLVM tools (`rust-profdata`, `rust-cov`, etc.) + which are fully compatible with coverage-related artifacts produced by `rustc`. From 51f9049aa64026bcda538e6fb8f71a9ff7c3d22a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 13:30:05 +0000 Subject: [PATCH 15/21] Shorten introduction --- rfc/src/rfcs/0011-source-coverage.md | 42 ++++++++-------------------- 1 file changed, 11 insertions(+), 31 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index a094a8e9c8af..b18981e2755b 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -13,51 +13,31 @@ A source-based code coverage feature for Kani built on top of Rust's coverage in ## User Impact -Nowadays, users can't easily obtain verification-based coverage reports in Kani. -Generally speaking, these reports show which parts of the code under verification are covered and which are not. -Because of that, users rely on these reports to ensure that their harnesses are sound ----that is, that properties are checked for the entire body of code they're expecting to cover. - -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. - -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. - -### Update: from line to source coverage - In our first attempt to add a coverage feature fully managed by Kani, we introduced and made available a line coverage option (see [RFC: Line coverage](0008-line-coverage.md) for more details). This option has since then allowed us to gather more data around the expectations for a coverage feature in Kani. -For example, the line coverage output we produced wasn't easy to interpret without knowing some implementation details. +For example, the line coverage output we produced was not easy to interpret without knowing some implementation details. Aside from that, the feature requested in [#2795](https://github.com/model-checking/kani/issues/2795) alludes to the need of providing coverage-specific tooling in Kani. Nevertheless, as captured in [#2640](https://github.com/model-checking/kani/issues/2640), source-based coverage results provide the clearest and most precise coverage information. -In this RFC, we propose an integration with [Rust's source-based code coverage instrumentation](https://doc.rust-lang.org/rustc/instrument-coverage.html). -The integration would allow us to report source-based code coverage results from Kani. +In this RFC, we propose an integration with [Rust's source-based code coverage +instrumentation](https://doc.rust-lang.org/rustc/instrument-coverage.html). +This integration would allow us to report source-based code coverage results from Kani. Also, we propose adding a new user-facing, coverage-focused tool called `kani-cov`. The tool would allow users to process coverage results generated by Kani and produce coverage artifacts such as summaries and reports according to their preferences. -In the [next section](#user-experience), we'll explain in more detail how we +In the [next section](#user-experience), we will explain in more detail how we expect `kani-cov` to assist with coverage-related tasks. -With these changes, we expect our coverage options to become more flexible, precise and efficient. -These options are expected to replace the previous options available through the line coverage feature. -In the [last section](#future-possibilities) of this RFC, -we'll also discuss the requirements for a potential integration of this coverage feature with the LLVM toolchain. +With these changes, we expect our coverage options to become more flexible, +precise and efficient. These options are expected to replace the previous +options available through the line coverage feature. +In the [last section](#future-possibilities) of this RFC, we will also discuss +the requirements for a potential integration of this coverage feature with the +LLVM toolchain. ## User Experience From 1b0033754ddf22b324b788573f4fb7f3fe45342b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 15:03:38 +0000 Subject: [PATCH 16/21] Revise UX section --- rfc/src/rfcs/0011-source-coverage.md | 93 +++++++++++++++++----------- 1 file changed, 56 insertions(+), 37 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index b18981e2755b..82127bc92aca 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -17,11 +17,14 @@ In our first attempt to add a coverage feature fully managed by Kani, we introdu (see [RFC: Line coverage](0008-line-coverage.md) for more details). This option has since then allowed us to gather more data around the expectations for a coverage feature in Kani. -For example, the line coverage output we produced was not easy to interpret without knowing some implementation details. -Aside from that, the feature requested in [#2795](https://github.com/model-checking/kani/issues/2795) -alludes to the need of providing coverage-specific tooling in Kani. -Nevertheless, as captured in [#2640](https://github.com/model-checking/kani/issues/2640), -source-based coverage results provide the clearest and most precise coverage information. +For example, the line coverage output we produced was not easy to interpret +without knowing some implementation details. +Aside from that, the feature requested in +[#2795](https://github.com/model-checking/kani/issues/2795) alludes to the need +of providing coverage-specific tooling in Kani. +Nevertheless, as captured in +[#2640](https://github.com/model-checking/kani/issues/2640), source-based +coverage results provide the clearest and most precise coverage information. In this RFC, we propose an integration with [Rust's source-based code coverage instrumentation](https://doc.rust-lang.org/rustc/instrument-coverage.html). @@ -41,13 +44,17 @@ LLVM toolchain. ## User Experience -The proposed experience is partially inspired by that of the most popular coverage frameworks. -First, let's delve into the LLVM coverage workflow, followed by an explanation of our proposal. +The proposed experience is partially inspired by that of the most popular +coverage frameworks. +First, let us delve into the LLVM coverage workflow, followed by an explanation +of our proposal. ### The LLVM code coverage workflow The LLVM project is home to one of the most popular code coverage frameworks. -The workflow associated to the LLVM framework is described in the documentation for [source-based code coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)[^note-source], but we briefly describe it here to better relate it with our proposal. +The workflow associated to the LLVM framework is described in the documentation for +[source-based code coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)[^note-source], +but we briefly describe it here to better relate it with our proposal. In short, the LLVM code coverage workflow follows three steps: 1. **Compiling with coverage enabled.** This causes the compiler to generate an instrumented program. @@ -69,21 +76,25 @@ RUSTFLAGS='-Cinstrument-coverage' cargo run This should populate the directory with at least one `.profraw` file. Each `.profraw` file corresponds to a specific source code file in your project. -At this point, we'll have produced the artifacts that we generally require for the LLVM tools: +At this point, we will have produced the artifacts that we generally require for +the LLVM tools: 1. **The instrumented binary** which, in addition to the instrumented program, contains additional information (e.g., the coverage mappings) required to interpret the profiling results. 2. **The `.profraw` files** which essentially includes the profiling results - (counter and expression values) for each function of the corresponding source - code file. + (e.g., counter values) for each function of the corresponding source code file. For step 3, the commands will depend on what kind of results we want. -Most likely we will have to merge the `.profraw` files and produce a `.profdata` file as follows: +Most likely we will have to merge the `.profraw` files and produce a `.profdata` +file as follows: ```sh llvm-profdata merge -sparse *.profraw -o output.profdata ``` +The resulting `.profdata` file will contain the aggregated coverage results from +the `.profraw` files passed to the `merge` command. + Then, we can use a command such as ```sh @@ -111,31 +122,35 @@ TOTAL 9 3 ``` [^note-source]: The LLVM project refers to their own coverage feature as - "source-based code coverage". It's not rare to see the term "region coverage" - being used instead to refer to the same thing. That's because LLVM's - source-based code coverage feature can report coverage for code regions, but - other coverage frameworks don't support the concept of code regions. + *source-based code coverage*. It is not rare to see the term *region + coverage* being used instead to refer to the same thing. That is because + LLVM's source-based code coverage feature can report coverage for code + regions, but other coverage frameworks do not support the concept of code + regions. ### The Kani coverage workflow -The two main components of the Kani coverage workflow will be the following: - 1. The existing `--coverage` flag that drives the coverage workflow in Kani and - produces basic coverage results by default. +The two main components of the Kani coverage workflow that we propose are the +following: + 1. The existing `--coverage` flag that drives the coverage workflow in Kani, + emits raw coverage data (as in the `.profraw` files), and produces basic + coverage results by default. 2. A new subcommand `cov` that allows users to further process raw coverage information emitted by Kani to produce customized coverage results (i.e., different to the ones produced by default with the `--coverage` option). + The `cov` subcommand is an alias for the `kani-cov` tool. -In constrast to the LLVM workflow, where human-readable coverage results can +In contrast to the LLVM workflow, where human-readable coverage results can be produced only after a sequence of LLVM tool commands, we provide some coverage results by default. This aligns better with our UX philosophy, and removes the need for a wrapper around our coverage features like [`cargo-llvm-cov`](https://github.com/taiki-e/cargo-llvm-cov). -Alternatively, the `cov` subcommand offers the ability required to -produce more specific coverage results if needed. -We anticipate the `cov` subcommand being particularly useful in less -standard project setups, giving the users the flexibility required to produce -coverage results tailored to their specific needs. +Alternatively, the `cov` subcommand offers the ability of producing more +specific coverage results if needed. +We anticipate the `cov` subcommand being particularly useful in less standard +project setups, giving the users the flexibility required to produce coverage +results tailored to their specific needs. In the following, we describe each one of these components in more detail. @@ -182,23 +197,28 @@ Hence, the `cov` subcommand corresponds to the set of LLVM tools (`llvm-profdata`, `llvm-cov`, etc.) that are used to produce coverage outputs through the LLVM coverage workflow. -In contrast to LLVM, we'll have a single subcommand for all Kani coverage-related needs. +In contrast to LLVM, we will have a single subcommand for all Kani +coverage-related needs. The `cov` subcommand will just call the `kani-cov` tool, +which is expected to be shipped along the rest of Kani binaries. + We suggest that the subcommand initially offers two options: 1. An option to merge the coverage results from one or more files and a source code snapshot[^note-snapshot] into a single file. 2. An option to produce coverage outputs from coverage results, including summaries or coverage reports in human-readable formats (e.g., HTML). -Let's assume that we've run `cargo kani --coverage -Zsource-coverage` and -generated coverage files in the `my-coverage` folder. Then, we'd use `cargo kani cov` -as follows to combine the coverage results[^note-exclude] for all harnesses: +Let's assume that we have run `cargo kani --coverage -Zsource-coverage` and +generated coverage files in the `my-coverage` folder. Then, we would use `cargo +kani cov` as follows to combine the coverage results[^note-exclude] for all +harnesses: ```sh cargo kani cov --merge my-coverage/*.kaniraw -o my-coverage.kanicov ``` -Let's say the user is first interested in reading a coverage summary through the terminal. -They will have to use the `report` command for that: +Let's say the user is first interested in reading a coverage summary through the +terminal. +They can use the `--summary` option for that: ```sh cargo kani cov --summary my-coverage/default.kanimap -instr-profile=my-coverage.kanicov @@ -214,7 +234,7 @@ The command could print a coverage summary like: ``` Now, let's say the user wants to produce an HTML report of the coverage results. -They will have to use the `--report` command for that: +They will have to use the `--report` option for that: ```sh cargo kani cov --report my-coverage/default.kanimap -format=html -instr-profile=my-coverage.kanicov -o coverage-report @@ -229,9 +249,8 @@ according to the coverage results in `my-coverage.kanicov`. export into GCC's coverage format [Gcov](https://en.wikipedia.org/wiki/Gcov), and the option [`export`](https://llvm.org/docs/CommandGuide/llvm-cov.html#llvm-cov-export) - to export into the LCOV format. I'd strongly recommend against adding - format-specific options to `kani-cov` unless there are technical reasons to - do so. + to export into the LCOV format. These may be good options to consider for + `kani-cov` in the future but we should focus on basic formats for now. [^note-exclude]: Options to exclude certain coverage results (e.g, from the standard library) will likely be part of this option. @@ -245,8 +264,8 @@ according to the coverage results in `my-coverage.kanicov`. We will update the coverage feature of the [Kani VS Code Extension](https://github.com/model-checking/kani-vscode-extension) to follow this new coverage workflow. -In other words, the extension will first run Kani with the `-cov` option and -use `kani-cov` to produce a `.kanicov` file with the coverage results. +In other words, the extension will first run Kani with the `--coverage` option and +use `kani cov` to produce a `.kanicov` file with the coverage results. The extension will consume the source-based code coverage results and highlight region coverage in the source code seen from VS Code. From 264bd7d3bdbfda3ec12c1a4143eb38b6a22b3ea2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 15:09:33 +0000 Subject: [PATCH 17/21] Just refer to coverage mappings for now --- rfc/src/rfcs/0011-source-coverage.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 82127bc92aca..7feffafd318b 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -202,8 +202,8 @@ coverage-related needs. The `cov` subcommand will just call the `kani-cov` tool, which is expected to be shipped along the rest of Kani binaries. We suggest that the subcommand initially offers two options: - 1. An option to merge the coverage results from one or more files and a source - code snapshot[^note-snapshot] into a single file. + 1. An option to merge the coverage results from one or more files and coverage + mappings[^note-snapshot] into a single file. 2. An option to produce coverage outputs from coverage results, including summaries or coverage reports in human-readable formats (e.g., HTML). @@ -255,9 +255,9 @@ according to the coverage results in `my-coverage.kanicov`. [^note-exclude]: Options to exclude certain coverage results (e.g, from the standard library) will likely be part of this option. -[^note-snapshot]: Source code snapshots are necessary to produce coverage - reports for items that otherwise are unreachable or have been sliced away - during the compilation process. +[^note-snapshot]: Coverage mappings essentially provide a snapshot of the source + code reports for items that otherwise are unreachable or have been sliced + away during the compilation process. #### Integration with the Kani VS Code Extension From c3e22d6407cd552a7c4975de33fdbbdadec900a6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 16:04:40 +0000 Subject: [PATCH 18/21] Short intro to design --- rfc/src/rfcs/0011-source-coverage.md | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 7feffafd318b..8ab00e9d9459 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -283,7 +283,17 @@ format or integrate Kani with LLVM tools as discussed in [Integration with LLVM] ## Detailed Design -Note: This section is still being worked on. Feel free to ignore it for now. +In this section, we provide more details on: + - The Rust coverage instrumentation and how it can be integrated into + Kani to produce source-based code coverage results. + - The proposed coverage workflow to be run by default in Kani when the + `--coverage` option is used. + +This information is mostly intended as a reference for Kani contributors. +Currently, the Rust coverage instrumentation continues to be developed. Because +of that, Rust toolchain upgrades may result in breaking changes to our own +coverage feature. This section should help developers to understand the general +approach and resolve such issues by themselves. ### The Rust coverage instrumentation @@ -464,7 +474,7 @@ physical counters. Unfortunately, doing so would lead to incorrect coverage results due to the arithmetic nature of expression-based counters. We elaborate on this topic in the later parts of this document. -### The default coverage workflow +### The default coverage workflow in Kani In this section, we describe the default `--coverage` workflow from a developer's point of view. This will hopefully help developers understand how From 703a4056fb6d3996f35a42fe08bdebfc8d428100 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Aug 2024 21:52:57 +0000 Subject: [PATCH 19/21] Part of counter expressions --- rfc/src/rfcs/0011-source-coverage.md | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 8ab00e9d9459..c9a3c289b2d6 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -532,8 +532,6 @@ In other words, it's not as advanced nor precise as the source-based implementat [^note-benchmarks]: Actual performance benchmarks to follow in [#3119](https://github.com/model-checking/kani/pull/3119). -### Optimization with coverage-counter expressions - ## Open questions - Do we want to instrument dependencies by default? Preliminary benchmarking results show a slowdown of 100% and greater. @@ -587,3 +585,26 @@ However, at this time we recommend against integrating with LLVM due to these re provide compatibility with newer LLVM versions. Moreover, the Rust compiler supplies their own version of LLVM tools (`rust-profdata`, `rust-cov`, etc.) which are fully compatible with coverage-related artifacts produced by `rustc`. + + +### Optimization with coverage-counter expressions + +In the [subsection related to the +integration](#integrating-the-instrumentation-into-kani), we noted that we could +follow an alternative approach where we only instrument coverage statements that +correspond to physical counters. In fact, this would be the logical choice since +the replacement of physical counters by expression-based counters would also be +a performance optimization for us. However, the expressions used for +expression-based counters are built with the arithmetic operators `Add` and +`Sub`. On the other hand, the coverage checks performed by Kani have a boolean +meaning: you either cover a region or you do not. + +It is not difficult to find cases where these two notions for coverage counters +are incompatible. For example + + +[^note-expression-integration]: We could follow an alternative approach where we +do not instrument each coverage statement, but only those that correspond to +physical counters. Unfortunately, doing so would lead to incorrect coverage +results due to the arithmetic nature of expression-based counters. We elaborate +on this topic in the later parts of this document. \ No newline at end of file From 1f49b1d00da880068d9aa5219899741778b61f9e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 20:18:12 +0000 Subject: [PATCH 20/21] Complete counter section --- rfc/src/rfcs/0011-source-coverage.md | 56 +++++++++++++++++++++------- 1 file changed, 43 insertions(+), 13 deletions(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index c9a3c289b2d6..232869a1236c 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -594,17 +594,47 @@ integration](#integrating-the-instrumentation-into-kani), we noted that we could follow an alternative approach where we only instrument coverage statements that correspond to physical counters. In fact, this would be the logical choice since the replacement of physical counters by expression-based counters would also be -a performance optimization for us. However, the expressions used for -expression-based counters are built with the arithmetic operators `Add` and -`Sub`. On the other hand, the coverage checks performed by Kani have a boolean -meaning: you either cover a region or you do not. - -It is not difficult to find cases where these two notions for coverage counters -are incompatible. For example - +a performance optimization for us. + +However, the expressions used in expression-based counters are built with the +arithmetic operators `Add` (`+`) and `Sub` (`-`). On the other hand, the +coverage checks performed by Kani have a boolean meaning: you either cover a +region or you do not. Thus, there are many cases where these two notions of +coverage counters are incompatible. For example, let's say we have this +function: + +```rust +fn check_value(val: u32) { + if val == VALUE { + do_this(); + } else { + do_that(); + } + do_something_else(); +} +``` -[^note-expression-integration]: We could follow an alternative approach where we -do not instrument each coverage statement, but only those that correspond to -physical counters. Unfortunately, doing so would lead to incorrect coverage -results due to the arithmetic nature of expression-based counters. We elaborate -on this topic in the later parts of this document. \ No newline at end of file +One way to optimize the counters in this function is to have two physical +counters for the branches of the `if` statement (`c1` and `c2`), and then an +expression-based counter associated to the `do_something_else()` statement +adding those (i.e., `c3 = c1 + c2`). If we have, for example, two executions for +this program, with each one taking a different branch, then the results for the +coverage counters will be `c1 = 1`, `c2 = 1` and `c3 = c1 + c2 = 2`. + +But what does `c3 = 2` mean in the context of a verification-based coverage +result? That is not clear. For instance, in a Kani trace, you could have a +nondeterministic value for `val` which just happens to be `val == VALUE` and not +at the same time. This would result in the same counters (`c1 = 1`, `c2 = 1` and +`c3 = 2`), but the program is being run only once! + +Note that finding a verification-based replacement for the runtime operators in +counter-based expressions is an interesting research topic. If we could +establish a relation between the runtime and verification expressions, then we +could avoid the instrumentation of coverage checks for expression-based +counters. For example, could we replace the `Add` operator (`+`) with an `Or` +operator (`||`)? Intuitively, this makes sense since verification-based coverage +counters are binary. It also seems to work for our example since covering any of +the branches should result in the `do_something_else()` statement being covered +as well, with the counter values now being `c1 = 1`, `c2 = 1` and `c3 = 1`. +However, it is not clear that this would work for all cases, nor it is clear +that we can replace `Sub` with another verification-based operator. From 5ed66ed2b39beda8cd8422c15a4b712d20d2103e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 20:30:15 +0000 Subject: [PATCH 21/21] Complete default behavior for Kani coverage workflow --- rfc/src/rfcs/0011-source-coverage.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 232869a1236c..9ea23c72a9d1 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -508,7 +508,10 @@ uses the JSON format but we might consider using a binary format if it doesn't scale. In addition, Kani will produce two types of coverage results: - 1. A coverage summary + 1. A coverage summary with the default options. + 2. A terminal-based coverage report with the default options. However, we will + only do this if the program is composed of a single source + file[^note-conditional-report]. [^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). The [draft @@ -517,6 +520,10 @@ In addition, Kani will produce two types of coverage results: the source files referred to by the code coverage checks, but it doesn't get information about code trimmed out by the MIR linker. +[^note-conditional-report]: In other words, standalone `kani` would always emit +these terminal-based reports, but `cargo kani` would not unless the project +contains a single Rust file (for example, `src/main.rs`). + ## Rationale and alternatives ### Other coverage implementations