kani-cov: A coverage tool for Kani

[adpaco-aws]

This PR introduces kani-cov, a coverage-oriented tool for Kani. This new tool will help users aggregate raw coverage results produced by Kani and generate human-readable coverage summaries and reports.

kani-cov allows using three different subcommands: merge, summary and report. In the following, we will show how each one of these commands can be used.

The merge subcommand

The merge subcommand takes raw coverage results from Kani (AKA "kaniraw" files) and generates aggregated coverage results which are stored into another file (AKA a "kanicov" file). This new file can then be used for generating summaries or reports.

For example, if we assume this Rust code is in main.rs:

1 fn _other_function() {
2    println!("Hello, world!");
3 }
4
5 fn test_cov(val: u32) -> bool {
6     if val < 3 || val == 42 {
7         true
8     } else {
9         false
10    }
11 }
12
13 #[cfg_attr(kani, kani::proof)]
14 fn main() {
15    let test1 = test_cov(1);
16    let test2 = test_cov(2);
17    assert!(test1);
18    assert!(test2);
19 }

and we execute Kani with coverage enabled

kani main.rs --coverage -Zsource-coverage

the raw coverage results will be saved to a folder

[info] Coverage results saved to /home/ubuntu/coverage-experiments/src/kanicov_2024-09-23_23-49

we now can aggregate those results with the merge subcommand

kani-cov merge kanicov_2024-09-23_23-49/*kaniraw.json

which by default produces a default_kanicov.json file. We can also use the --output <path> option to change the name of the file.

The type of file we just produced is known as the "profile" or the "kanicov" file, and contains aggregated coverage results which may have been originated in multiple verification sessions. This file is a required input for the other two subcommands.

The summary subcommand

Now that we have both the "kanicov" file and the "kanimap" file, we are ready to produce coverage metrics with the summary subcommand:

kani-cov summary kanicov_2024-09-23_23-49/kanicov_2024-09-23_23-49_kanimap.json --profile default_kanicov.json

This outputs a table including coverage metrics for functions, lines and regions for each file referenced in the coverage mappings:

| Filename                                      | Function (%) | Line (%)     | Region (%)  |
| --------------------------------------------- | ------------ | ------------ | ----------- |
| /home/ubuntu/coverage-experiments/src/main.rs | 2/3 (66.67)  | 8/12 (66.67) | 4/6 (66.67) |

Since the default format is markdown, the table can also be rendered as in this PR description:

Filename	Function (%)	Line (%)	Region (%)
/home/ubuntu/coverage-experiments/src/main.rs	2/3 (66.67)	8/12 (66.67)	4/6 (66.67)

At present, no other formats are available. But the JSON and CSV formats would be really nice and easy to have.

The report subcommand

Coverage reports go a little further and allow users to visualize coverage information on the source code.

The report requires the same input files as the summary subcommand:

kani-cov report kanicov_2024-09-23_23-49/kanicov_2024-09-23_23-49_kanimap.json --profile default_kanicov.json

When calling this command from a terminal, it will render like this:

However, if you're redirecting the output to a file, it will back off to another text-based mode which simply uses ``` and ''' to represent opening and closing escapes for the coverage regions. This is just another format called escapes which can be explicitly requested as

kani-cov report kanicov_2024-09-23_23-49/kanicov_2024-09-23_23-49_kanimap.json --profile default_kanicov.json --format=escapes

Similar to the summary command, this will iterate over the files in the coverage mappings, compute coverage information and highlight any uncovered regions (except #3543).

Testing

This PR also changes compiletest to automatically call the merge and report subcommands on the coverage test suite. The tests have been blessed using the --fix-expected option and this Python3 script that removes the first line (path to the file) and adds \ after each line so an exact match is expected.

import os

def process_files(directory):
    for filename in os.listdir(directory):
        if filename == "expected":
            file_path = os.path.join(directory, filename)
            with open(file_path, "r") as file:
                lines = file.readlines()
            
            # Remove the first line
            lines = lines[1:]
            
            # Add the character `\` after every line
            processed_lines = []
            for i, line in enumerate(lines):
                processed_lines.append(line.replace("\n", "\\\n"))
            
            # Write the processed lines back to the file
            with open(file_path, "w") as file:
                file.writelines(processed_lines)

Callouts / Known issues

This PR only introduces kani-cov. It doesn't plug kani-cov into kani-driver so it's automatically run when using the --coverage option, nor it prepares the kani-cov binary for distribution. This is better to address later.

This PR also spawns a few issues:

• Some coverage results point to non-existing regions #3543 forces us to filter out certain coverage results to avoid issues with the report command. It is important that we investigate where these coverage results come from and their semantics as this represents a soundness issue.
• Check structures and other code is duplicated in kani-cov #3541 is to avoid duplicating certain data structures that currently live in kani-driver. We should probably have a different crate for these structures and import them from kani-driver and kani-cov, but this is more of a distribution problem that doesn't need to be tackled here.
• Filenames stored in raw coverage results should be absolute #3542 requires us to match filenames when extracting function coverage results. It's not a big deal, but it'll likely improve the tool's robustness in the long term.

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

[celinval]

Are we planning to release this tool or is it only for developers?

[adpaco-aws]

Are we planning to release this tool or is it only for developers?

The plan is to release the tool. More details in the upcoming RFC.

[adpaco-aws]

Note to self: Consider highlighting uncovered spans in red as the default behavior. At the very least, discuss in the RFC.

[feliperodri]

Thanks for implementing all my comments. I have one last before approving it. Why the issue #3543 is classified as a soundness issue now? As far as I understood, the coverage report feature will crash in the cases you mentioned in the issue. Will it report false coverage reports in any case? This is important to fix before stabilization, but it seems to me unnecessary to classify this as a soundness issue.

[carolynzech]

I'd recommend making the type aliases public and incorporating them throughout merge.rs and summary.rs as well, but not a blocker for this PR.
Excited to use this feature!

[adpaco-aws]

Why the issue #3543 is classified as a soundness issue now? As far as I understood, the coverage report feature will crash in the cases you mentioned in the issue. Will it report false coverage reports in any case? This is important to fix before stabilization, but it seems to me unnecessary to classify this as a soundness issue.

The reason #3543 was classified as a soundness issue is because we were filtering out the results which could lead to a crash in kani-cov. Filtering out these results can be considered a soundness issue because, even if they're spurious failures coming from the Rust coverage instrumentation, we could be hiding other issues. It all depends on how we define soundness for coverage and the origin of these coverage artifacts.

Regardless, I've changed how we handle the checks with these out-of-bounds regions to replicate the spurious failure instead. Since we only need to extend the line by one space to represent the check in such cases, we just do that now. In other words, we are now reporting the same spurious failures, which may be more confusing for users but avoids soundness concerns. For example, for the test in tests/coverage/assert we get this report:

/home/ubuntu/kani/tests/coverage/assert/test.rs
   1|     | // Copyright Kani Contributors
   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
   3|     | 
   4|     | #[kani::proof]
   5|    1| fn foo() {
   6|    1|     let x: i32 = kani::any();
   7|    1|     if x > 5 {
   8|     |         // fails
   9|    1|         assert!(x < 4);
  10|    1|         if x < 3 ```{'''
  11|    0| ```            // unreachable'''
  12|    0| ```            assert!(x == 2);'''
  13|    0| ```        }'''``` '''
  14|    1|     } else {
  15|    1|         // passes
  16|    1|         assert!(x <= 5);
  17|    1|     }
  18|     | }

Note the single region represented at the end of line 13? In the original source code, that space doesn't exist. But we can create that space in this representation and report the same result that the instrumentation gives us. It's less noticeable in the terminal output, but we also "draw it" there:

In addition to this change, I've added some more documentation to the code handling this special case and updated #3543 (labeled as "spurious failure" now). Please don't hesitate to ask for more clarifications if you need them. @carolynzech I've also implemented your suggestions to use the type aliases in other modules of kani-cov. Thanks!