Merge branch 'main' into issue-2253-simd-array

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

@@ -29,7 +29,7 @@ use tracing::debug;
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
-#[derive(Debug, Clone, EnumString, AsRefStr)]
+#[derive(Debug, Clone, EnumString, AsRefStr, PartialEq)]
 #[strum(serialize_all = "snake_case")]
 pub enum PropertyClass {
  /// Overflow panics that can be generated by Intrisics.
@@ -45,6 +45,19 @@ pub enum PropertyClass {
  ///
  /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
  Cover,
+ /// The class of checks used for code coverage instrumentation. Only needed
+ /// when working on coverage-related features.
+ ///
+ /// Do not mistake with `Cover`, they are different:
+ /// - `CodeCoverage` checks have a fixed condition (`false`) and description.
+ /// - `CodeCoverage` checks are filtered out from verification results and
+ /// postprocessed to build coverage reports.
+ /// - `Cover` checks can be added by users (using the `kani::cover` macro),
+ /// while `CodeCoverage` checks are not exposed to users (i.e., they are
+ /// automatically added if running with the coverage option).
+ ///
+ /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
+ CodeCoverage,
  /// Ordinary (Rust) assertions and panics.
  ///
  /// SPECIAL BEHAVIOR: These assertion failures should be observable during normal execution of Rust code.
@@ -134,6 +147,21 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
  }
 
+ /// Generate a cover statement for code coverage reports.
+ pub fn codegen_coverage(&self, span: Span) -> Stmt {
+ let loc = self.codegen_caller_span(&Some(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,
+ )
+ }
+
  // The above represent the basic operations we can perform w.r.t. assert/assume/cover
  // Below are various helper functions for constructing the above more easily.
 

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

@@ -16,25 +16,55 @@ impl<'tcx> GotocCtx<'tcx> {
  debug!(?bb, "Codegen basicblock");
  self.current_fn_mut().set_current_bb(bb);
  let label: String = self.current_fn().find_label(&bb);
+ let check_coverage = self.queries.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);
- self.current_fn_mut().push_onto_block(tcode.with_label(label));
+ // When checking coverage, the `coverage` check should be
+ // labelled instead.
+ if check_coverage {
+ let span = term.source_info.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));
+ }
  }
  _ => {
  let stmt = &bbd.statements[0];
  let scode = self.codegen_statement(stmt);
- self.current_fn_mut().push_onto_block(scode.with_label(label));
+ // When checking coverage, the `coverage` check should be
+ // labelled instead.
+ if check_coverage {
+ let span = stmt.source_info.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));
+ }
 
  for s in &bbd.statements[1..] {
+ if check_coverage {
+ let span = s.source_info.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 = self.codegen_terminator(bbd.terminator());
- self.current_fn_mut().push_onto_block(term);
+ let term = bbd.terminator();
+ if check_coverage {
+ let span = term.source_info.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);
  }
  }
  self.current_fn_mut().reset_current_bb();

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

@@ -188,7 +188,7 @@ impl<'tcx> GotocCtx<'tcx> {
  let a = fargs.remove(0);
  let b = fargs.remove(0);
  let div_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone());
- let div_overflow_check = self.codegen_assert(
+ let div_overflow_check = self.codegen_assert_assume(
  div_does_not_overflow,
  PropertyClass::ArithmeticOverflow,
  format!("attempt to compute {} which would overflow", intrinsic).as_str(),