Line coverage reports

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,
+ "cover_experiment",
+ 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(),

kani-compiler/src/kani_compiler.rs

@@ -349,6 +349,7 @@ impl Callbacks for KaniCompiler {
  let queries = &mut (*self.queries.lock().unwrap());
  queries.emit_vtable_restrictions = matches.get_flag(parser::RESTRICT_FN_PTRS);
  queries.check_assertion_reachability = matches.get_flag(parser::ASSERTION_REACH_CHECKS);
+ queries.check_coverage = matches.get_flag(parser::COVERAGE_CHECKS);
  queries.output_pretty_json = matches.get_flag(parser::PRETTY_OUTPUT_FILES);
  queries.ignore_global_asm = matches.get_flag(parser::IGNORE_GLOBAL_ASM);
  queries.write_json_symtab =
@@ -364,6 +365,7 @@ impl Callbacks for KaniCompiler {
  {
  queries.stubbing_enabled = true;
  }
+
  debug!(?queries, "config end");
  }
  }

kani-compiler/src/kani_queries/mod.rs

@@ -28,6 +28,7 @@ pub enum ReachabilityType {
 #[derive(Debug, Default, Clone)]
 pub struct QueryDb {
  pub check_assertion_reachability: bool,
+ pub check_coverage: bool,
  pub emit_vtable_restrictions: bool,
  pub output_pretty_json: bool,
  pub ignore_global_asm: bool,

kani-compiler/src/parser.rs

@@ -28,6 +28,9 @@ pub const RESTRICT_FN_PTRS: &str = "restrict-vtable-fn-ptrs";
 /// Option name used to enable assertion reachability checks.
 pub const ASSERTION_REACH_CHECKS: &str = "assertion-reach-checks";
 
+/// Option name used to enable coverage checks.
+pub const COVERAGE_CHECKS: &str = "coverage-checks";
+
 /// Option name used to use json pretty-print for output files.
 pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files";
 
@@ -98,6 +101,12 @@ pub fn parser() -> Command {
  .help("Check the reachability of every assertion.")
  .action(ArgAction::SetTrue),
  )
+ .arg(
+ Arg::new(COVERAGE_CHECKS)
+ .long(COVERAGE_CHECKS)
+ .help("Check the reachability of every statement.")
+ .action(ArgAction::SetTrue),
+ )
  .arg(
  Arg::new(REACHABILITY)
  .long(REACHABILITY)

kani-driver/src/args/common.rs

@@ -44,6 +44,8 @@ pub enum UnstableFeatures {
  ConcretePlayback,
  /// Enable Kani's unstable async library.
  AsyncLib,
+ /// Enable line coverage instrumentation/reports
+ LineCoverage,
 }
 
 impl ValidateArgs for CommonArgs {

kani-driver/src/args/mod.rs

@@ -300,6 +300,9 @@ pub struct VerificationArgs {
  )]
  pub enable_stubbing: bool,
 
+ #[arg(long, hide_short_help = true)]
+ pub coverage: bool,
+
  /// Arguments to pass down to Cargo
  #[command(flatten)]
  pub cargo: CargoCommonArgs,
@@ -640,6 +643,16 @@ impl ValidateArgs for VerificationArgs {
  }
  }
 
+ if self.coverage
+ && !self.common_args.unstable_features.contains(&UnstableFeatures::LineCoverage)
+ {
+ return Err(Error::raw(
+ ErrorKind::MissingRequiredArgument,
+ "The `--coverage` argument is unstable and requires `-Z \
+ line-coverage` to be used.",
+ ));
+ }
+
  Ok(())
  }
 }

kani-driver/src/call_cbmc.rs

@@ -13,7 +13,7 @@ use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
  extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput,
 };
-use crate::cbmc_property_renderer::{format_result, kani_cbmc_output_filter};
+use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::session::KaniSession;
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -303,14 +303,23 @@ impl VerificationResult {
  }
  }
 
- pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String {
+ pub fn render(
+ &self,
+ output_format: &OutputFormat,
+ should_panic: bool,
+ coverage_mode: bool,
+ ) -> String {
  match &self.results {
  Ok(results) => {
  let status = self.status;
  let failed_properties = self.failed_properties;
  let show_checks = matches!(output_format, OutputFormat::Regular);
- let mut result =
- format_result(results, status, should_panic, failed_properties, show_checks);
+
+ let mut result = if coverage_mode {
+ format_coverage(results, status, should_panic, failed_properties, show_checks)
+ } else {
+ format_result(results, status, should_panic, failed_properties, show_checks)
+ };
  writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
  result
  }

kani-driver/src/call_single_file.rs

@@ -96,6 +96,10 @@ impl KaniSession {
  flags.push("--enable-stubbing".into());
  }
 
+ if self.args.coverage {
+ flags.push("--coverage-checks".into());
+ }
+
  flags.extend(
  self.args
  .common_args

kani-driver/src/cbmc_output_parser.rs

@@ -96,14 +96,16 @@ pub struct PropertyId {
 
 impl Property {
  const COVER_PROPERTY_CLASS: &str = "cover";
+ const COVERAGE_PROPERTY_CLASS: &str = "coverage";
 
  pub fn property_class(&self) -> String {
  self.property_id.class.clone()
  }
 
  /// Returns true if this is a cover property
  pub fn is_cover_property(&self) -> bool {
- self.property_id.class == Self::COVER_PROPERTY_CLASS
+ self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
+ || self.property_id.class == Self::COVER_PROPERTY_CLASS
  }
 
  pub fn property_name(&self) -> String {

kani-driver/src/cbmc_property_renderer.rs

@@ -8,7 +8,7 @@ use console::style;
 use once_cell::sync::Lazy;
 use regex::Regex;
 use rustc_demangle::demangle;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 
 type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>;
 
@@ -421,6 +421,102 @@ pub fn format_result(
  result_str
 }
 
+/// Seperate checks into coverage and non-coverage based on property class and format them seperately for --coverage. We report both verification and processed coverage
+/// results
+pub fn format_coverage(
+ properties: &[Property],
+ status: VerificationStatus,
+ should_panic: bool,
+ failed_properties: FailedProperties,
+ show_checks: bool,
+) -> String {
+ let non_coverage_checks: Vec<Property> =
+ properties.iter().filter(|&x| x.property_class() != "code_coverage").cloned().collect();
+ let coverage_checks: Vec<Property> =
+ properties.iter().filter(|&x| x.property_class() == "code_coverage").cloned().collect();
+
+ let verification_output =
+ format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks);
+ let coverage_output = format_result_coverage(&coverage_checks);
+ print!("printing coverage output = {}", coverage_output);
+ let result = format!("{}\n{}", verification_output, coverage_output);
+
+ result
+}
+
+/// Generate coverage result from all coverage properties (i.e., the checks with "coverage" property class).
+/// To be used when the user requests coverage information with --coverage. The output is tested through the coverage-based testing suite, not the regular expected suite.
+/// Loops through each of the check with a coverage property class and gives a status of FULL if all checks pertaining
+/// to a line number are SATISFIED. Similarly, it gives a status of NONE if all checks related to a line are UNSAT. If a line has both, it reports PARTIAL coverage.
+fn format_result_coverage(properties: &[Property]) -> String {
+ let mut formatted_output = String::new();
+ formatted_output.push_str("\nCoverage Results:\n");
+
+ let mut coverage_checks: Vec<&Property> = properties.iter().collect();
+
+ coverage_checks.sort_by_key(|check| (&check.source_location.file, &check.source_location.line));
+
+ let mut files: HashMap<String, Vec<(usize, CheckStatus)>> = HashMap::new();
+ for check in coverage_checks {
+ // Get line number and filename
+ let line_number: usize = check.source_location.line.as_ref().unwrap().parse().unwrap();
+ let file_name: String = check.source_location.file.as_ref().unwrap().to_string();
+
+ // Add to the files lookup map
+ files.entry(file_name.clone()).or_insert_with(Vec::new).push((line_number, check.status));
+ }
+
+ let mut coverage_results: HashMap<String, Vec<(usize, String)>> = HashMap::new();
+
+ for (file, val) in files {
+ let mut lines: HashSet<usize> = HashSet::new();
+ let mut line_results: Vec<(usize, String)> = Vec::new();
+ for check in val.clone() {
+ lines.insert(check.0);
+ }
+
+ // For each of these lines, create a map from line -> status
+ // example - {3 -> ["SAT", "UNSAT"], 4 -> ["UNSAT"] ...}
+ for line in lines.iter() {
+ let is_line_satisfied: Vec<_> = val
+ .iter()
+ .filter(|(line_number_accumulated, _)| *line == *line_number_accumulated)
+ .collect();
+
+ // Report lines as FULL if all of the coverage checks (property class = code_coverage) say FAILURE, NONE if all of the coverage checks say SUCCESS,
+ // and PARTIAL if there is a mix of the two
+ let covered_status: String = if is_line_satisfied
+ .iter()
+ .all(|&is_satisfiable| is_satisfiable.1.to_string().contains("FAILURE"))
+ {
+ "FULL".to_string()
+ } else if is_line_satisfied
+ .iter()
+ .all(|&is_satisfiable| is_satisfiable.1.to_string().contains("SUCCESS"))
+ {
+ "NONE".to_string()
+ } else {
+ "PARTIAL".to_string()
+ };
+
+ line_results.push((*line, covered_status));
+ }
+
+ line_results.sort_by_key(|&(line, _)| line);
+ coverage_results.insert(file.clone(), line_results);
+ }
+
+ // Create formatted string that is returned to the user as output
+ for (file, checks) in coverage_results.iter() {
+ for (line_number, coverage_status) in checks {
+ formatted_output.push_str(&format!("{}, {}, {}\n", file, line_number, coverage_status));
+ }
+ formatted_output.push('\n');
+ }
+
+ formatted_output
+}
+
 /// Attempts to build a message for a failed property with as much detailed
 /// information on the source location as possible.
 fn build_failure_message(description: String, trace: &Option<Vec<TraceItem>>) -> String {

kani-driver/src/harness_runner.rs

@@ -96,7 +96,11 @@ impl KaniSession {
  if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
  println!(
  "{}",
- result.render(&self.args.output_format, harness.attributes.should_panic)
+ result.render(
+ &self.args.output_format,
+ harness.attributes.should_panic,
+ self.args.coverage
+ )
  );
  }
  self.gen_and_add_concrete_playback(harness, &mut result)?;