Adopt Rust's source-based code coverage instrumentation (#3119)

This PR replaces the line-based coverage instrumentation we introduced
in #2609 with the standard source-based code coverage instrumentation
performed by the Rust compiler.

As a result, we now insert code coverage checks in the
`StatementKind::Coverage(..)` statements produced by the Rust compiler
during compilation. These checks include coverage-relevant
information[^note-internal] such as the coverage counter/expression they
represent [^note-instrument]. Both the coverage metadata (`kanimap`) and
coverage results (`kaniraw`) are saved into files after the verification
stage.

Unfortunately, we currently have a chicken-egg problem with this PR and
#3121, where we introduce a tool named `kani-cov` to postprocess
coverage results. As explained in #3143, `kani-cov` is expected to be an
alias for the `cov` subcommand and provide most of the postprocessing
features for coverage-related purposes. But, the tool will likely be
introduced after this change. Therefore, we propose to temporarily print
a list of the regions in each function with their associated coverage
status (i.e., `COVERED` or `UNCOVERED`).

### Source-based code coverage: An example

The main advantage of source-based coverage results is their precision
with respect to the source code. The [Source-based Code
Coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)
documentation explains more details about the LLVM coverage workflow and
its different options.

For example, let's take this Rust code:
```rust
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 }
```

Compiling and running the program with `rustc` and the `-C
instrument-coverage` flag, and using the LLVM tools can get us the
following coverage result:


![Image](https://github.com/model-checking/kani/assets/73246657/9070e390-6e0b-4add-828d-d9f9caacad07)


In contrast, the `cargo kani --coverage -Zsource-coverage` command
currently generates:

```
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
```

which is a verification-based coverage result almost equivalent to the
runtime coverage results.

### Benchmarking

We have evaluated the performance impact of the instrumentation using
the `kani-perf.sh` suite (14 benchmarks). For each test, we compare the
average time to run standard verification against the average time to
run verification with the source-based code coverage feature
enabled[^note-line-evaluation].

The evaluation has been performed on an EC2 `m5a.4xlarge` instance
running Ubuntu 22.04. The experimental data has been obtained by running
the `kani-perf.sh` script 10 times for each version (`only verification`
and `verification + coverage`), computing the average and standard
deviation. We've split this data into `small` (tests taking 60s or less)
and `large` (tests taking more than 60s) and drawn the two graphs below.

#### Performance comparison - `small` benchmarks


![performance_comparison_small](https://github.com/user-attachments/assets/679cf412-0193-4b0c-a78c-2d0fb702706f)

#### Performance comparison - `large` benchmarks


![performance_comparison_large](https://github.com/user-attachments/assets/4bb5a895-7f57-49e0-86b5-5fea67fad939)

#### Comments on performance

Looking at the small tests, the performance impact seems negligible in
such cases. The difference is more noticeable in the large tests, where
the time to run verification and coverage can take 2x or even more. It
wouldn't be surprising that, as programs become larger, the complexity
of the coverage checking grows exponentially as well. However, since
most verification jobs don't take longer than 30min (1800s), it's OK to
say that coverage checking represents a 100-200% slowdown in the worst
case w.r.t. standard verification.

It's also worth noting a few other things:
* The standard deviation remains similar in most cases, meaning that the
coverage feature doesn't have an impact on their stability.
* We haven't tried any SAT solvers other than the ones used by default
for each benchmark. It's possible that other solvers perform
better/worse with the coverage feature enabled.

### Call-outs
 * The soundness issue documented in #3441.
* The issue with saving coverage mappings for non-reachable functions
documented in #3445.
* I've modified the test cases in `tests/coverage/` to test this
feature. Since this technique is simpler, we don't need that many test
cases. However, it's possible I've left some test cases which don't
contribute much. Please let me know if you want to add/remove a test
case.

[^note-internal]: The coverage mappings can't be accessed through the
StableMIR interface so we retrieve them through the internal API.

[^note-instrument]: The instrumentation replaces certain counters with
expressions based on other counters when possible to avoid a part of the
runtime overhead. More details can be found
[here](https://github.com/rust-lang/rustc-dev-guide/blob/master/src/llvm-coverage-instrumentation.md#mir-pass-instrumentcoverage).
Unfortunately, we can't avoid instrumenting expressions at the moment.

[^note-line-evaluation]: We have not compared performance against the
line-based code coverage feature because it doesn't seem worth it. The
line-based coverage feature is guaranteed to include more coverage
checks than the source-based one for any function. In addition,
source-based results are more precise than line-based ones. So this
change represents both a quantitative and qualitative improvement.

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

Author: adpaco-aws

Cargo.lock

@@ -316,6 +316,15 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "deranged"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
+dependencies = [
+ "powerfmt",
+]
+
 [[package]]
 name = "either"
 version = "1.13.0"
@@ -500,6 +509,7 @@ dependencies = [
  "strum",
  "strum_macros",
  "tempfile",
+ "time",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -660,6 +670,12 @@ dependencies = [
  "num-traits",
 ]
 
+[[package]]
+name = "num-conv"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+
 [[package]]
 name = "num-integer"
 version = "0.1.46"
@@ -767,6 +783,12 @@ version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"
 
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
 [[package]]
 name = "ppv-lite86"
 version = "0.2.20"
@@ -1179,6 +1201,37 @@ dependencies = [
  "once_cell",
 ]
 
+[[package]]
+name = "time"
+version = "0.3.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
+dependencies = [
+ "deranged",
+ "itoa",
+ "num-conv",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
+dependencies = [
+ "num-conv",
+ "time-core",
+]
+
 [[package]]
 name = "toml"
 version = "0.8.19"

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -21,6 +21,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
+use rustc_middle::mir::coverage::CodeRegion;
 use stable_mir::mir::{Place, ProjectionElem};
 use stable_mir::ty::{Span as SpanStable, TypeAndMut};
 use strum_macros::{AsRefStr, EnumString};
@@ -148,18 +149,19 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Generate a cover statement for code coverage reports.
-    pub fn codegen_coverage(&self, span: SpanStable) -> Stmt {
+    pub fn codegen_coverage(
+        &self,
+        counter_data: &str,
+        span: SpanStable,
+        code_region: CodeRegion,
+    ) -> Stmt {
         let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
         // `assert(false)`.
-        self.codegen_assert(
-            Expr::bool_false(),
-            PropertyClass::CodeCoverage,
-            "code coverage for location",
-            loc,
-        )
+        let msg = format!("{counter_data} - {code_region:?}");
+        self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
     }
 
     // The above represent the basic operations we can perform w.r.t. assert/assume/cover

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -20,53 +20,24 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
         debug!(?bb, "codegen_block");
         let label = bb_label(bb);
-        let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
         match bbd.statements.len() {
             0 => {
                 let term = &bbd.terminator;
                 let tcode = self.codegen_terminator(term);
-                // When checking coverage, the `coverage` check should be
-                // labelled instead.
-                if check_coverage {
-                    let span = term.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover.with_label(label));
-                    self.current_fn_mut().push_onto_block(tcode);
-                } else {
-                    self.current_fn_mut().push_onto_block(tcode.with_label(label));
-                }
+                self.current_fn_mut().push_onto_block(tcode.with_label(label));
             }
             _ => {
                 let stmt = &bbd.statements[0];
                 let scode = self.codegen_statement(stmt);
-                // When checking coverage, the `coverage` check should be
-                // labelled instead.
-                if check_coverage {
-                    let span = stmt.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover.with_label(label));
-                    self.current_fn_mut().push_onto_block(scode);
-                } else {
-                    self.current_fn_mut().push_onto_block(scode.with_label(label));
-                }
+                self.current_fn_mut().push_onto_block(scode.with_label(label));
 
                 for s in &bbd.statements[1..] {
-                    if check_coverage {
-                        let span = s.span;
-                        let cover = self.codegen_coverage(span);
-                        self.current_fn_mut().push_onto_block(cover);
-                    }
                     let stmt = self.codegen_statement(s);
                     self.current_fn_mut().push_onto_block(stmt);
                 }
                 let term = &bbd.terminator;
-                if check_coverage {
-                    let span = term.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover);
-                }
                 let tcode = self.codegen_terminator(term);
                 self.current_fn_mut().push_onto_block(tcode);
             }

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -216,3 +216,74 @@ impl<'tcx> GotocCtx<'tcx> {
         self.reset_current_fn();
     }
 }
+
+pub mod rustc_smir {
+    use crate::stable_mir::CrateDef;
+    use rustc_middle::mir::coverage::CodeRegion;
+    use rustc_middle::mir::coverage::CovTerm;
+    use rustc_middle::mir::coverage::MappingKind::Code;
+    use rustc_middle::ty::TyCtxt;
+    use stable_mir::mir::mono::Instance;
+    use stable_mir::Opaque;
+
+    type CoverageOpaque = stable_mir::Opaque;
+
+    /// Retrieves the `CodeRegion` associated with the data in a
+    /// `CoverageOpaque` object.
+    pub fn region_from_coverage_opaque(
+        tcx: TyCtxt,
+        coverage_opaque: &CoverageOpaque,
+        instance: Instance,
+    ) -> Option<CodeRegion> {
+        let cov_term = parse_coverage_opaque(coverage_opaque);
+        region_from_coverage(tcx, cov_term, instance)
+    }
+
+    /// Retrieves the `CodeRegion` associated with a `CovTerm` object.
+    ///
+    /// Note: This function could be in the internal `rustc` impl for `Coverage`.
+    pub fn region_from_coverage(
+        tcx: TyCtxt<'_>,
+        coverage: CovTerm,
+        instance: Instance,
+    ) -> Option<CodeRegion> {
+        // We need to pull the coverage info from the internal MIR instance.
+        let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
+        let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
+
+        // Some functions, like `std` ones, may not have coverage info attached
+        // to them because they have been compiled without coverage flags.
+        if let Some(cov_info) = &body.function_coverage_info {
+            // Iterate over the coverage mappings and match with the coverage term.
+            for mapping in &cov_info.mappings {
+                let Code(term) = mapping.kind else { unreachable!() };
+                if term == coverage {
+                    return Some(mapping.code_region.clone());
+                }
+            }
+        }
+        None
+    }
+
+    /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`:
+    /// <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html>
+    ///
+    /// At present, a `CovTerm` can be one of the following:
+    ///  - `CounterIncrement(<num>)`: A physical counter.
+    ///  - `ExpressionUsed(<num>)`: An expression-based counter.
+    ///  - `Zero`: A counter with a constant zero value.
+    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm {
+        let coverage_str = coverage_opaque.to_string();
+        if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") {
+            let (num_str, _rest) = rest.split_once(')').unwrap();
+            let num = num_str.parse::<u32>().unwrap();
+            CovTerm::Counter(num.into())
+        } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") {
+            let (num_str, _rest) = rest.split_once(')').unwrap();
+            let num = num_str.parse::<u32>().unwrap();
+            CovTerm::Expression(num.into())
+        } else {
+            CovTerm::Zero
+        }
+    }
+}

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -3,6 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::{bb_label, PropertyClass};
+use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
@@ -158,12 +159,28 @@ impl<'tcx> GotocCtx<'tcx> {
                     location,
                 )
             }
+            StatementKind::Coverage(coverage_opaque) => {
+                let function_name = self.current_fn().readable_name();
+                let instance = self.current_fn().instance_stable();
+                let counter_data = format!("{coverage_opaque:?} ${function_name}$");
+                let maybe_code_region =
+                    region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
+                if let Some(code_region) = maybe_code_region {
+                    let coverage_stmt =
+                        self.codegen_coverage(&counter_data, stmt.span, code_region);
+                    // TODO: Avoid single-statement blocks when conversion of
+                    // standalone statements to the irep format is fixed.
+                    // More details in <https://github.com/model-checking/kani/issues/3012>
+                    Stmt::block(vec![coverage_stmt], location)
+                } else {
+                    Stmt::skip(location)
+                }
+            }
             StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(..)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
-            | StatementKind::Coverage { .. }
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)

kani-driver/Cargo.toml

@@ -34,6 +34,7 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 rand = "0.8"
 which = "6"
+time = {version = "0.3.36", features = ["formatting"]}
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/args/mod.rs

@@ -615,12 +615,12 @@ impl ValidateArgs for VerificationArgs {
         }
 
         if self.coverage
-            && !self.common_args.unstable_features.contains(UnstableFeature::LineCoverage)
+            && !self.common_args.unstable_features.contains(UnstableFeature::SourceCoverage)
         {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
                 "The `--coverage` argument is unstable and requires `-Z \
-            line-coverage` to be used.",
+            source-coverage` to be used.",
             ));
         }
 

kani-driver/src/call_cargo.rs

@@ -206,7 +206,7 @@ impl KaniSession {
         })
     }
 
-    fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
+    pub fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
         let mut cmd = MetadataCommand::new();
 
         // restrict metadata command to host platform. References: