Adopt Rust's source-based code coverage instrumentation

Cargo.lock

@@ -315,6 +315,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"
@@ -401,9 +410,9 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.3.0"
+version = "2.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "de3fc2e30ba82dd1b3911c8de1ffc143c74a914a14e99514d7637e3099df5ea0"
+checksum = "93ead53efc7ea8ed3cfb0c79fc8023fbb782a5432b52830b6518941cebe6505c"
 dependencies = [
  "equivalent",
  "hashbrown",
@@ -481,6 +490,7 @@ dependencies = [
  "strum",
  "strum_macros",
  "tempfile",
+ "time",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -632,6 +642,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"
@@ -729,6 +745,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"
@@ -1139,6 +1161,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: