Skip to content

Coverage metadata should include mappings for all source code #3445

Open
@adpaco-aws

Description

@adpaco-aws

In the integration of Rust's code coverage instrumentation being introduced in #3119, coverage metadata consists of just the canonical paths for all source code files.

Ideally, this metadata should be extended with coverage information for each function in the project, not just those deemed reachable by the reachability analysis. This is necessary for kani-cov (the coverage-focused tool being introduced in #3121) to be able to produce coverage summaries and reports that include coverage data for the entire project.

For example, for the test

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 }

we get coverage results for the reachable functions main and test_cov, but not for _other_function:

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

We can mitigate this for function and line metrics in #3121 by using (for example) tools like syn on the source code files, but we cannot do the same for region metrics because region information for each function is only available to us when compiling the function in Kani. However, this is not the case for non-reachable functions which won't be compiled, so we cannot fully record that information.

Additionally, storing the coverage mappings into the coverage metadata file would save us some work at compilation time to determine the code regions that a particular counter is covering. This process could be done in kani-cov so the effort spent postprocessing coverage properties could be practically omitted.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions