Skip to content

Commit

Permalink
Line coverage reports (#2609)
Browse files Browse the repository at this point in the history
Co-authored-by: jaisnan <jaisnan@amazon.com>
Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
  • Loading branch information
3 people authored Jul 28, 2023
1 parent a2a1e85 commit db42ee9
Show file tree
Hide file tree
Showing 75 changed files with 967 additions and 17 deletions.
30 changes: 29 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.

Expand Down
38 changes: 34 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
Expand Down
2 changes: 2 additions & 0 deletions kani-compiler/src/kani_compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -364,6 +365,7 @@ impl Callbacks for KaniCompiler {
{
queries.stubbing_enabled = true;
}

debug!(?queries, "config end");
}
}
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/kani_queries/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
9 changes: 9 additions & 0 deletions kani-compiler/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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";

Expand Down Expand Up @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions kani-driver/src/args/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
14 changes: 14 additions & 0 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -300,6 +300,10 @@ pub struct VerificationArgs {
)]
pub enable_stubbing: bool,

/// Enable Kani coverage output alongside verification result
#[arg(long, hide_short_help = true)]
pub coverage: bool,

/// Arguments to pass down to Cargo
#[command(flatten)]
pub cargo: CargoCommonArgs,
Expand Down Expand Up @@ -640,6 +644,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(())
}
}
Expand Down
17 changes: 13 additions & 4 deletions kani-driver/src/call_cbmc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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
}
Expand Down
4 changes: 4 additions & 0 deletions kani-driver/src/call_single_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 12 additions & 2 deletions kani-driver/src/cbmc_output_parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,11 +96,17 @@ pub struct PropertyId {

impl Property {
const COVER_PROPERTY_CLASS: &str = "cover";
const COVERAGE_PROPERTY_CLASS: &str = "code_coverage";

pub fn property_class(&self) -> String {
self.property_id.class.clone()
}

// Returns true if this is a code_coverage check
pub fn is_code_coverage_property(&self) -> bool {
self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
}

/// Returns true if this is a cover property
pub fn is_cover_property(&self) -> bool {
self.property_id.class == Self::COVER_PROPERTY_CLASS
Expand Down Expand Up @@ -322,18 +328,22 @@ impl std::fmt::Display for TraceData {
#[serde(rename_all = "UPPERCASE")]
pub enum CheckStatus {
Failure,
Satisfied, // for cover properties only
Covered, // for `code_coverage` properties only
Satisfied, // for `cover` properties only
Success,
Undetermined,
Unreachable,
Unsatisfiable, // for cover properties only
Uncovered, // for `code_coverage` properties only
Unsatisfiable, // for `cover` properties only
}

impl std::fmt::Display for CheckStatus {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let check_str = match self {
CheckStatus::Satisfied => style("SATISFIED").green(),
CheckStatus::Success => style("SUCCESS").green(),
CheckStatus::Covered => style("COVERED").green(),
CheckStatus::Uncovered => style("UNCOVERED").red(),
CheckStatus::Failure => style("FAILURE").red(),
CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
Expand Down
Loading

0 comments on commit db42ee9

Please sign in to comment.