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,10 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
     Cover,
+    /// See [GotocCtx::codegen_coverage] below. Always an `assert(false)` that's not an error.
+    ///
+    /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
+    Coverage,
     /// Ordinary (Rust) assertions and panics.
     ///
     /// SPECIAL BEHAVIOR: These assertion failures should be observable during normal execution of Rust code.
@@ -101,7 +105,11 @@ impl<'tcx> GotocCtx<'tcx> {
         loc: Location,
     ) -> Stmt {
         let property_name = property_class.as_str();
-        Stmt::assert(cond, property_name, message, loc)
+        if self.queries.check_coverage && property_class != PropertyClass::Coverage {
+            Stmt::assume(cond, loc)
+        } else {
+            Stmt::assert(cond, property_name, message, loc)
+        }
     }
 
     /// Generates a CBMC assumption.
@@ -134,6 +142,16 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
     }
 
+    /// Generate code for 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::Coverage, "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

@@ -18,23 +18,54 @@ impl<'tcx> GotocCtx<'tcx> {
         let label: String = self.current_fn().find_label(&bb);
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
+        let check_coverage = self.queries.check_coverage;
         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));
+                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));
+                    let tcode = self.codegen_terminator(term);
+                    self.current_fn_mut().push_onto_block(tcode);
+                } else {
+                    let tcode = self.codegen_terminator(term);
+                    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));
+                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));
+                    let scode = self.codegen_statement(stmt);
+                    self.current_fn_mut().push_onto_block(scode);
+                } else {
+                    let scode = self.codegen_statement(stmt);
+                    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;
+                        // TODO: Push cover statement based on some TBD condition
+                        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);
+                // TODO: test with division by zero or overflow that false
+                // assumption will be in the middle of the basic block
+                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/kani_compiler.rs

@@ -348,6 +348,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 =
@@ -363,6 +364,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 assertion reachability 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/mod.rs

@@ -300,6 +300,9 @@ pub struct VerificationArgs {
     )]
     pub enable_stubbing: bool,
 
+    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
+    pub coverage: bool,
+
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoCommonArgs,

kani-driver/src/call_cbmc.rs

@@ -13,7 +13,9 @@ 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_result, format_result_coverage, kani_cbmc_output_filter,
+};
 use crate::session::KaniSession;
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -303,16 +305,38 @@ 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);
-                writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
-                result
+
+                // If --coverage is on, return the post-processed results
+                if coverage_mode {
+                    return format_result_coverage(results);
+                }
+
+                match output_format {
+                    OutputFormat::Regular | OutputFormat::Terse => {
+                        let mut result = format_result(
+                            results,
+                            status,
+                            should_panic,
+                            failed_properties,
+                            show_checks,
+                        );
+                        writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32())
+                            .unwrap();
+                        result
+                    }
+                    OutputFormat::Old => todo!(),
+                }
             }
             Err(exit_status) => {
                 let verification_result = console::style("FAILED").red();

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,86 @@ pub fn format_result(
     result_str
 }
 
+/// Formats a coverage result item (i.e., the subset of verification 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 COVERED if all checks pertaining
+/// to a line number are SATISFIED. Otherwise, it gives a status of UNCOVERED.
+pub fn format_result_coverage(properties: &[Property]) -> String {
+    let mut formatted_output = String::new();
+    formatted_output.push_str("\nCoverage Results:\n");
+
+    let coverage_checks: Vec<Property> =
+        properties.iter().filter(|&x| x.property_class() == "coverage").cloned().collect();
+
+    let mut sorted_checks: Vec<&Property> = coverage_checks.iter().collect();
+
+    sorted_checks.sort_by_key(|check| (&check.source_location.file, &check.source_location.line));
+
+    let mut files: HashMap<String, Vec<(usize, String)>> = HashMap::new();
+    for check in sorted_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
+        if !files.contains_key(&file_name) {
+            files.insert(file_name.clone(), vec![(line_number, check.status.clone().to_string())]);
+        } else {
+            files
+                .get_mut(&file_name)
+                .unwrap()
+                .push((line_number, check.status.clone().to_string()));
+        }
+    }
+
+    let mut coverage_results: HashMap<String, Vec<(usize, String)>> = HashMap::new();
+
+    // loop through the files list and create a list of lines accessible in that file
+    for file in files.keys() {
+        let mut lines: HashSet<usize> = HashSet::new();
+        let mut line_results: Vec<(usize, String)> = Vec::new();
+        for check in files.get(file).unwrap() {
+            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<_> = files
+                .get(file)
+                .unwrap()
+                .iter()
+                .filter(|(line_number_accumulated, _)| *line == *line_number_accumulated)
+                .collect();
+
+            // If any of the statuses is UNSAT, we report that line as UNCOVERED
+            let covered_status: String = if is_line_satisfied
+                .iter()
+                .all(|&is_satisfiable| is_satisfiable.1.contains("SATISFIED"))
+            {
+                "COVERED".to_string()
+            } else {
+                "UNCOVERED".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)?;
@@ -154,7 +158,7 @@ impl KaniSession {
         }
 
         // We currently omit a summary if there was just 1 harness
-        if !self.args.common_args.quiet && !self.args.visualize {
+        if !self.args.common_args.quiet && !self.args.visualize && !self.args.coverage {
             if failing > 0 {
                 println!("Summary:");
             }

scripts/kani-regression.sh

@@ -38,6 +38,7 @@ cargo test -p kani_metadata
 # Declare testing suite information (suite and mode)
 TESTS=(
     "script-based-pre exec"
+    "coverage coverage-based"
     "kani kani"
     "expected expected"
     "ui expected"

tests/coverage/reachable/assert-false/expected

@@ -0,0 +1,21 @@
+library/kani/src/arbitrary.rs, 55, COVERED
+library/kani/src/arbitrary.rs, 79, COVERED
+library/kani/src/arbitrary.rs, 80, COVERED
+library/kani/src/arbitrary.rs, 81, COVERED
+library/kani/src/arbitrary.rs, 82, COVERED
+
+library/kani/src/lib.rs, 133, COVERED
+library/kani/src/lib.rs, 134, COVERED
+library/kani/src/lib.rs, 176, COVERED
+library/kani/src/lib.rs, 177, COVERED
+
+tests/coverage/reachable/assert-false/main.rs, 11, COVERED
+tests/coverage/reachable/assert-false/main.rs, 12, COVERED
+tests/coverage/reachable/assert-false/main.rs, 16, COVERED
+tests/coverage/reachable/assert-false/main.rs, 17, COVERED
+tests/coverage/reachable/assert-false/main.rs, 20, COVERED
+tests/coverage/reachable/assert-false/main.rs, 21, COVERED
+tests/coverage/reachable/assert-false/main.rs, 22, UNCOVERED
+tests/coverage/reachable/assert-false/main.rs, 25, COVERED
+tests/coverage/reachable/assert-false/main.rs, 26, UNCOVERED
+tests/coverage/reachable/assert-false/main.rs, 28, COVERED