Adopt Rust's source-based code coverage instrumentation

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: