From db42ee996ade70116a75b291072a7c1189a3d913 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 28 Jul 2023 16:42:28 -0400 Subject: [PATCH] Line coverage reports (#2609) Co-authored-by: jaisnan Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/assert.rs | 30 +++++- .../codegen_cprover_gotoc/codegen/block.rs | 38 ++++++- .../codegen/intrinsic.rs | 2 +- kani-compiler/src/kani_compiler.rs | 2 + kani-compiler/src/kani_queries/mod.rs | 1 + kani-compiler/src/parser.rs | 9 ++ kani-driver/src/args/common.rs | 2 + kani-driver/src/args/mod.rs | 14 +++ kani-driver/src/call_cbmc.rs | 17 ++- kani-driver/src/call_single_file.rs | 4 + kani-driver/src/cbmc_output_parser.rs | 14 ++- kani-driver/src/cbmc_property_renderer.rs | 102 +++++++++++++++++- kani-driver/src/harness_runner.rs | 6 +- scripts/kani-regression.sh | 1 + .../coverage/reachable/assert-false/expected | 8 ++ tests/coverage/reachable/assert-false/main.rs | 19 ++++ .../reachable/assert/reachable_pass/expected | 4 + .../reachable/assert/reachable_pass/test.rs | 10 ++ .../reachable/bounds/reachable_fail/expected | 4 + .../reachable/bounds/reachable_fail/test.rs | 11 ++ .../div-zero/reachable_fail/expected | 4 + .../reachable/div-zero/reachable_fail/test.rs | 11 ++ .../div-zero/reachable_pass/expected | 4 + .../reachable/div-zero/reachable_pass/test.rs | 11 ++ .../overflow/reachable_fail/expected | 5 + .../reachable/overflow/reachable_fail/test.rs | 15 +++ .../overflow/reachable_pass/expected | 7 ++ .../reachable/overflow/reachable_pass/test.rs | 17 +++ .../rem-zero/reachable_fail/expected | 4 + .../reachable/rem-zero/reachable_fail/test.rs | 11 ++ .../rem-zero/reachable_pass/expected | 4 + .../reachable/rem-zero/reachable_pass/test.rs | 11 ++ tests/coverage/unreachable/abort/expected | 7 ++ tests/coverage/unreachable/abort/main.rs | 21 ++++ tests/coverage/unreachable/assert/expected | 7 ++ tests/coverage/unreachable/assert/test.rs | 18 ++++ tests/coverage/unreachable/assert_eq/expected | 5 + tests/coverage/unreachable/assert_eq/test.rs | 11 ++ tests/coverage/unreachable/assert_ne/expected | 6 ++ tests/coverage/unreachable/assert_ne/test.rs | 14 +++ .../unreachable/assume_assert/expected | 4 + .../unreachable/assume_assert/main.rs | 8 ++ tests/coverage/unreachable/bounds/expected | 4 + tests/coverage/unreachable/bounds/test.rs | 12 +++ tests/coverage/unreachable/break/expected | 9 ++ tests/coverage/unreachable/break/main.rs | 19 ++++ tests/coverage/unreachable/check_id/expected | 16 +++ tests/coverage/unreachable/check_id/main.rs | 25 +++++ tests/coverage/unreachable/compare/expected | 7 ++ tests/coverage/unreachable/compare/main.rs | 16 +++ .../unreachable/contradiction/expected | 6 ++ .../unreachable/contradiction/main.rs | 13 +++ .../unreachable/debug-assert/expected | 4 + .../coverage/unreachable/debug-assert/main.rs | 10 ++ tests/coverage/unreachable/divide/expected | 7 ++ tests/coverage/unreachable/divide/main.rs | 19 ++++ .../unreachable/early-return/expected | 10 ++ .../coverage/unreachable/early-return/main.rs | 19 ++++ .../unreachable/if-statement/expected | 10 ++ .../coverage/unreachable/if-statement/main.rs | 20 ++++ .../unreachable/multiple-harnesses/expected | 39 +++++++ .../unreachable/multiple-harnesses/main.rs | 44 ++++++++ tests/coverage/unreachable/return/expected | 8 ++ tests/coverage/unreachable/return/main.rs | 17 +++ .../unreachable/tutorial_unreachable/expected | 5 + .../unreachable/tutorial_unreachable/main.rs | 11 ++ tests/coverage/unreachable/variant/expected | 10 ++ tests/coverage/unreachable/variant/main.rs | 29 +++++ tests/coverage/unreachable/vectors/expected | 6 ++ tests/coverage/unreachable/vectors/main.rs | 19 ++++ .../unreachable/while-loop-break/expected | 11 ++ .../unreachable/while-loop-break/main.rs | 23 ++++ tools/compiletest/src/common.rs | 3 + tools/compiletest/src/main.rs | 2 +- tools/compiletest/src/runtest.rs | 28 ++++- 75 files changed, 967 insertions(+), 17 deletions(-) create mode 100644 tests/coverage/reachable/assert-false/expected create mode 100644 tests/coverage/reachable/assert-false/main.rs create mode 100644 tests/coverage/reachable/assert/reachable_pass/expected create mode 100644 tests/coverage/reachable/assert/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/bounds/reachable_fail/expected create mode 100644 tests/coverage/reachable/bounds/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/div-zero/reachable_fail/expected create mode 100644 tests/coverage/reachable/div-zero/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/div-zero/reachable_pass/expected create mode 100644 tests/coverage/reachable/div-zero/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/overflow/reachable_fail/expected create mode 100644 tests/coverage/reachable/overflow/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/overflow/reachable_pass/expected create mode 100644 tests/coverage/reachable/overflow/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/expected create mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/expected create mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/test.rs create mode 100644 tests/coverage/unreachable/abort/expected create mode 100644 tests/coverage/unreachable/abort/main.rs create mode 100644 tests/coverage/unreachable/assert/expected create mode 100644 tests/coverage/unreachable/assert/test.rs create mode 100644 tests/coverage/unreachable/assert_eq/expected create mode 100644 tests/coverage/unreachable/assert_eq/test.rs create mode 100644 tests/coverage/unreachable/assert_ne/expected create mode 100644 tests/coverage/unreachable/assert_ne/test.rs create mode 100644 tests/coverage/unreachable/assume_assert/expected create mode 100644 tests/coverage/unreachable/assume_assert/main.rs create mode 100644 tests/coverage/unreachable/bounds/expected create mode 100644 tests/coverage/unreachable/bounds/test.rs create mode 100644 tests/coverage/unreachable/break/expected create mode 100644 tests/coverage/unreachable/break/main.rs create mode 100644 tests/coverage/unreachable/check_id/expected create mode 100644 tests/coverage/unreachable/check_id/main.rs create mode 100644 tests/coverage/unreachable/compare/expected create mode 100644 tests/coverage/unreachable/compare/main.rs create mode 100644 tests/coverage/unreachable/contradiction/expected create mode 100644 tests/coverage/unreachable/contradiction/main.rs create mode 100644 tests/coverage/unreachable/debug-assert/expected create mode 100644 tests/coverage/unreachable/debug-assert/main.rs create mode 100644 tests/coverage/unreachable/divide/expected create mode 100644 tests/coverage/unreachable/divide/main.rs create mode 100644 tests/coverage/unreachable/early-return/expected create mode 100644 tests/coverage/unreachable/early-return/main.rs create mode 100644 tests/coverage/unreachable/if-statement/expected create mode 100644 tests/coverage/unreachable/if-statement/main.rs create mode 100644 tests/coverage/unreachable/multiple-harnesses/expected create mode 100644 tests/coverage/unreachable/multiple-harnesses/main.rs create mode 100644 tests/coverage/unreachable/return/expected create mode 100644 tests/coverage/unreachable/return/main.rs create mode 100644 tests/coverage/unreachable/tutorial_unreachable/expected create mode 100644 tests/coverage/unreachable/tutorial_unreachable/main.rs create mode 100644 tests/coverage/unreachable/variant/expected create mode 100644 tests/coverage/unreachable/variant/main.rs create mode 100644 tests/coverage/unreachable/vectors/expected create mode 100644 tests/coverage/unreachable/vectors/main.rs create mode 100644 tests/coverage/unreachable/while-loop-break/expected create mode 100644 tests/coverage/unreachable/while-loop-break/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index bcf452602930..27203c7218c6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index b015be5b401c..bc6738e8ead0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/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(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4bd5566f9d7c..af06c456a7b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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(), diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 2a5e4c188578..ef766c562941 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/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"); } } diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index b8446bb7a023..44573bf124d8 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/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, diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index 2ff81a90bc7c..a947fdc61eaa 100644 --- a/kani-compiler/src/parser.rs +++ b/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) diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index 746482c6985e..a4325ca610fa 100644 --- a/kani-driver/src/args/common.rs +++ b/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 { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 31cae95e2a61..626f2d81be93 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -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, @@ -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(()) } } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index daddfdf62f1c..96770d562e79 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/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 } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index caf3dd7339a3..1522071fdefd 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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 diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 70e13b7dda06..8bdd45034190 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -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 @@ -322,11 +328,13 @@ 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 { @@ -334,6 +342,8 @@ impl std::fmt::Display for CheckStatus { 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(), diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 8da67dae7ab1..be788c5d1c0c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -8,7 +8,8 @@ use console::style; use once_cell::sync::Lazy; use regex::Regex; use rustc_demangle::demangle; -use std::collections::HashMap; +use std::collections::{BTreeMap, HashMap}; +use strum_macros::{AsRefStr, Display}; type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>; @@ -149,6 +150,15 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { map }); +#[derive(PartialEq, Eq, AsRefStr, Clone, Copy, Display)] +#[strum(serialize_all = "UPPERCASE")] +// The status of coverage reported by Kani +enum CoverageStatus { + Full, + Partial, + None, +} + const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani"; const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop"; const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion"; @@ -421,6 +431,72 @@ pub fn format_result( result_str } +/// Separate checks into coverage and non-coverage based on property class and format them separately 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 (coverage_checks, non_coverage_checks): (Vec, Vec) = + properties.iter().cloned().partition(|x| x.property_class() == "code_coverage"); + + let verification_output = + format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks); + let coverage_output = format_result_coverage(&coverage_checks); + let result = format!("{}\n{}", verification_output, coverage_output); + + result +} + +/// Generate coverage result from all coverage properties (i.e., checks with `code_coverage` property class). +/// Loops through each of the checks with the `code_coverage` property class on a line and gives: +/// - A status `FULL` if all checks pertaining to a line number are `COVERED` +/// - A status `NONE` if all checks related to a line are `UNCOVERED` +/// - Otherwise (i.e., if the line contains both) it reports `PARTIAL`. +/// +/// Used when the user requests coverage information with `--coverage`. +/// Output is tested through the `coverage-based` testing suite, not the regular +/// `expected` suite. +fn format_result_coverage(properties: &[Property]) -> String { + let mut formatted_output = String::new(); + formatted_output.push_str("\nCoverage Results:\n"); + + let mut coverage_results: BTreeMap> = + BTreeMap::default(); + for prop in properties { + let src = prop.source_location.clone(); + let file_entries = coverage_results.entry(src.file.unwrap()).or_default(); + let check_status = if prop.status == CheckStatus::Covered { + CoverageStatus::Full + } else { + CoverageStatus::None + }; + + // Create Map> + file_entries + .entry(src.line.unwrap().parse().unwrap()) + .and_modify(|line_status| { + if *line_status != check_status { + *line_status = CoverageStatus::Partial + } + }) + .or_insert(check_status); + } + + // 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>) -> String { @@ -512,7 +588,8 @@ pub fn postprocess_result(properties: Vec, extra_ptr_checks: bool) -> let updated_properties = update_properties_with_reach_status(properties_filtered, has_fundamental_failures); - update_results_of_cover_checks(updated_properties) + let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties); + update_results_of_cover_checks(results_after_code_coverage) } /// Determines if there is property with status `FAILURE` and the given description @@ -613,6 +690,27 @@ fn update_properties_with_reach_status( properties } +/// Update the results of `code_coverage` (NOT `cover`) properties. +/// - `SUCCESS` -> `UNCOVERED` +/// - `FAILURE` -> `COVERED` +/// Note that these statuses are intermediate statuses that aren't reported to +/// users but rather internally consumed and reported finally as `PARTIAL`, `FULL` +/// or `NONE` based on aggregated line coverage results. +fn update_results_of_code_covererage_checks(mut properties: Vec) -> Vec { + for prop in properties.iter_mut() { + if prop.is_code_coverage_property() { + prop.status = match prop.status { + CheckStatus::Success => CheckStatus::Uncovered, + CheckStatus::Failure => CheckStatus::Covered, + _ => unreachable!( + "status for coverage checks should be either `SUCCESS` or `FAILURE` prior to postprocessing" + ), + }; + } + } + properties +} + /// Update the results of cover properties. /// We encode cover(cond) as assert(!cond), so if the assertion /// fails, then the cover property is satisfied and vice versa. diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index fdafa8a5c18b..fa1aef3d763a 100644 --- a/kani-driver/src/harness_runner.rs +++ b/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)?; diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index fd04b579deb3..01afd6e2de59 100755 --- a/scripts/kani-regression.sh +++ b/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" diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected new file mode 100644 index 000000000000..7a9fef1ca77c --- /dev/null +++ b/tests/coverage/reachable/assert-false/expected @@ -0,0 +1,8 @@ +coverage/reachable/assert-false/main.rs, 6, FULL +coverage/reachable/assert-false/main.rs, 7, FULL +coverage/reachable/assert-false/main.rs, 11, FULL +coverage/reachable/assert-false/main.rs, 12, FULL +coverage/reachable/assert-false/main.rs, 15, FULL +coverage/reachable/assert-false/main.rs, 16, FULL +coverage/reachable/assert-false/main.rs, 17, PARTIAL +coverage/reachable/assert-false/main.rs, 19, FULL diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs new file mode 100644 index 000000000000..42563b1cd518 --- /dev/null +++ b/tests/coverage/reachable/assert-false/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the assert is reported as `PARTIAL` for having both `COVERED` and `UNCOVERED` coverage checks +fn any_bool() -> bool { + kani::any() +} + +#[kani::proof] +fn main() { + if any_bool() { + assert!(false); + } + + if any_bool() { + let s = "Fail with custom runtime message"; + assert!(false, "{}", s); + } +} diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected new file mode 100644 index 000000000000..67ae085a3e83 --- /dev/null +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/assert/reachable_pass/test.rs, 6, FULL +coverage/reachable/assert/reachable_pass/test.rs, 7, FULL +coverage/reachable/assert/reachable_pass/test.rs, 8, FULL +coverage/reachable/assert/reachable_pass/test.rs, 10, FULL diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs new file mode 100644 index 000000000000..72acca2b764c --- /dev/null +++ b/tests/coverage/reachable/assert/reachable_pass/test.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: u32 = kani::any_where(|val| *val == 5); + if x > 3 { + assert!(x > 4); // FULL: `x > 4` since `x = 5` + } +} diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected new file mode 100644 index 000000000000..af2f30e51fe2 --- /dev/null +++ b/tests/coverage/reachable/bounds/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE +coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL +coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs new file mode 100644 index 000000000000..cebd78b2d5d9 --- /dev/null +++ b/tests/coverage/reachable/bounds/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn get(s: &[i16], index: usize) -> i16 { + s[index] // PARTIAL: `s[index]` is covered, but `index = 15` induces a failure +} // NONE: `index = 15` caused failure earlier + +#[kani::proof] +fn main() { + get(&[7, -83, 19], 15); +} // NONE: `index = 15` caused failure earlier diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected new file mode 100644 index 000000000000..1ec1abefffd8 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE +coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..5f69005ee712 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn div(x: u16, y: u16) -> u16 { + x / y // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED` +} + +#[kani::proof] +fn main() { + div(678, 0); +} diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected new file mode 100644 index 000000000000..c7bfb5961c0b --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/div-zero/reachable_pass/test.rs, 5, PARTIAL +coverage/reachable/div-zero/reachable_pass/test.rs, 6, FULL +coverage/reachable/div-zero/reachable_pass/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_pass/test.rs, 11, FULL diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/reachable/div-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..766fb5a89d88 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_pass/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn div(x: u16, y: u16) -> u16 { + if y != 0 { x / y } else { 0 } // PARTIAL: some cases are `COVERED`, others are not +} + +#[kani::proof] +fn main() { + div(11, 3); +} diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected new file mode 100644 index 000000000000..f20826fb1a8e --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_fail/expected @@ -0,0 +1,5 @@ +coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL +coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/reachable/overflow/reachable_fail/test.rs new file mode 100644 index 000000000000..d435612f2342 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_fail/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani reports the correct coverage results in the case of an +//! arithmetic overflow failure (caused by the second call to `cond_reduce`). + +fn cond_reduce(thresh: u32, x: u32) -> u32 { + if x > thresh { x - 50 } else { x } // PARTIAL: some cases are `COVERED`, others are not +} + +#[kani::proof] +fn main() { + cond_reduce(60, 70); + cond_reduce(40, 42); +} // NONE: Caused by the arithmetic overflow failure from the second call to `cond_reduce` diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected new file mode 100644 index 000000000000..5becf2cd23e7 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_pass/expected @@ -0,0 +1,7 @@ +coverage/reachable/overflow/reachable_pass/test.rs, 8, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 9, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 13, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 14, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 15, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 16, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 17, FULL diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/reachable/overflow/reachable_pass/test.rs new file mode 100644 index 000000000000..0b05874efc84 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_pass/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani reports the correct coverage results (`FULL` for all lines) +//! in a case where arithmetic overflow failures are prevented. + +fn reduce(x: u32) -> u32 { + if x > 1000 { x - 1000 } else { x } +} + +#[kani::proof] +fn main() { + reduce(7); + reduce(33); + reduce(728); + reduce(1079); +} diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected new file mode 100644 index 000000000000..f7fa6ed7efeb --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE +coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..400c7e02340b --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn rem(x: u16, y: u16) -> u16 { + x % y // PARTIAL: `x % y` is covered but induces a division failure +} // NONE: Caused by division failure earlier + +#[kani::proof] +fn main() { + rem(678, 0); +} // NONE: Caused by division failure earlier diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/expected b/tests/coverage/reachable/rem-zero/reachable_pass/expected new file mode 100644 index 000000000000..f3d5934d785d --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/rem-zero/reachable_pass/test.rs, 5, PARTIAL +coverage/reachable/rem-zero/reachable_pass/test.rs, 6, FULL +coverage/reachable/rem-zero/reachable_pass/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_pass/test.rs, 11, FULL diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..41ed28f7b903 --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn rem(x: u16, y: u16) -> u16 { + if y != 0 { x % y } else { 0 } +} + +#[kani::proof] +fn main() { + rem(11, 3); +} diff --git a/tests/coverage/unreachable/abort/expected b/tests/coverage/unreachable/abort/expected new file mode 100644 index 000000000000..473b0f5a8d4d --- /dev/null +++ b/tests/coverage/unreachable/abort/expected @@ -0,0 +1,7 @@ +coverage/unreachable/abort/main.rs, 10, PARTIAL +coverage/unreachable/abort/main.rs, 11, FULL +coverage/unreachable/abort/main.rs, 13, FULL +coverage/unreachable/abort/main.rs, 15, FULL +coverage/unreachable/abort/main.rs, 17, NONE +coverage/unreachable/abort/main.rs, 20, NONE +coverage/unreachable/abort/main.rs, 21, NONE diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs new file mode 100644 index 000000000000..2941ec126f3c --- /dev/null +++ b/tests/coverage/unreachable/abort/main.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Test that the abort() function is respected and nothing beyond it will execute. + +use std::process; + +#[kani::proof] +fn main() { + for i in 0..4 { + if i == 1 { + // This comes first and it should be reachable. + process::abort(); + } + if i == 2 { + // This should never happen. + process::exit(1); + } + } + assert!(false, "This is unreachable"); +} diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected new file mode 100644 index 000000000000..f5b5f8044769 --- /dev/null +++ b/tests/coverage/unreachable/assert/expected @@ -0,0 +1,7 @@ +coverage/unreachable/assert/test.rs, 6, FULL +coverage/unreachable/assert/test.rs, 7, FULL +coverage/unreachable/assert/test.rs, 9, FULL +coverage/unreachable/assert/test.rs, 10, NONE +coverage/unreachable/assert/test.rs, 12, NONE +coverage/unreachable/assert/test.rs, 16, FULL +coverage/unreachable/assert/test.rs, 18, FULL diff --git a/tests/coverage/unreachable/assert/test.rs b/tests/coverage/unreachable/assert/test.rs new file mode 100644 index 000000000000..e7bddead756a --- /dev/null +++ b/tests/coverage/unreachable/assert/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn foo() { + let x: i32 = kani::any(); + if x > 5 { + // fails + assert!(x < 4); + if x < 3 { + // unreachable + assert!(x == 2); + } + } else { + // passes + assert!(x <= 5); + } +} diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected new file mode 100644 index 000000000000..f4e7608b2c13 --- /dev/null +++ b/tests/coverage/unreachable/assert_eq/expected @@ -0,0 +1,5 @@ +coverage/unreachable/assert_eq/test.rs, 6, FULL +coverage/unreachable/assert_eq/test.rs, 7, FULL +coverage/unreachable/assert_eq/test.rs, 8, FULL +coverage/unreachable/assert_eq/test.rs, 9, NONE +coverage/unreachable/assert_eq/test.rs, 11, FULL diff --git a/tests/coverage/unreachable/assert_eq/test.rs b/tests/coverage/unreachable/assert_eq/test.rs new file mode 100644 index 000000000000..29623498e715 --- /dev/null +++ b/tests/coverage/unreachable/assert_eq/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: i32 = kani::any(); + let y = if x > 10 { 15 } else { 33 }; + if y > 50 { + assert_eq!(y, 55); + } +} diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected new file mode 100644 index 000000000000..3b57defb4c36 --- /dev/null +++ b/tests/coverage/unreachable/assert_ne/expected @@ -0,0 +1,6 @@ +coverage/unreachable/assert_ne/test.rs, 6, FULL +coverage/unreachable/assert_ne/test.rs, 7, FULL +coverage/unreachable/assert_ne/test.rs, 8, FULL +coverage/unreachable/assert_ne/test.rs, 10, FULL +coverage/unreachable/assert_ne/test.rs, 11, NONE +coverage/unreachable/assert_ne/test.rs, 14, FULL diff --git a/tests/coverage/unreachable/assert_ne/test.rs b/tests/coverage/unreachable/assert_ne/test.rs new file mode 100644 index 000000000000..44b0ca82383e --- /dev/null +++ b/tests/coverage/unreachable/assert_ne/test.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: u32 = kani::any(); + if x > 0 { + let y = x / 2; + // y is strictly less than x + if y == x { + assert_ne!(y, 1); + } + } +} diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected new file mode 100644 index 000000000000..8c1ae8a247d2 --- /dev/null +++ b/tests/coverage/unreachable/assume_assert/expected @@ -0,0 +1,4 @@ +coverage/unreachable/assume_assert/main.rs, 5, FULL +coverage/unreachable/assume_assert/main.rs, 6, FULL +coverage/unreachable/assume_assert/main.rs, 7, NONE +coverage/unreachable/assume_assert/main.rs, 8, NONE diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs new file mode 100644 index 000000000000..c4d5d65c6640 --- /dev/null +++ b/tests/coverage/unreachable/assume_assert/main.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] +fn check_assume_assert() { + let a: u8 = kani::any(); + kani::assume(false); + assert!(a < 5); +} diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected new file mode 100644 index 000000000000..610372000a01 --- /dev/null +++ b/tests/coverage/unreachable/bounds/expected @@ -0,0 +1,4 @@ +coverage/unreachable/bounds/test.rs, 5, PARTIAL +coverage/unreachable/bounds/test.rs, 6, FULL +coverage/unreachable/bounds/test.rs, 11, FULL +coverage/unreachable/bounds/test.rs, 12, FULL diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs new file mode 100644 index 000000000000..c37c9d0dcad6 --- /dev/null +++ b/tests/coverage/unreachable/bounds/test.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn get(s: &[i16], index: usize) -> i16 { + if index < s.len() { s[index] } else { -1 } +} + +#[kani::proof] +fn main() { + //get(&[7, -83, 19], 2); + get(&[5, 206, -46, 321, 8], 8); +} diff --git a/tests/coverage/unreachable/break/expected b/tests/coverage/unreachable/break/expected new file mode 100644 index 000000000000..dcb013c50c3d --- /dev/null +++ b/tests/coverage/unreachable/break/expected @@ -0,0 +1,9 @@ +coverage/unreachable/break/main.rs, 5, PARTIAL +coverage/unreachable/break/main.rs, 6, FULL +coverage/unreachable/break/main.rs, 7, FULL +coverage/unreachable/break/main.rs, 11, NONE +coverage/unreachable/break/main.rs, 12, PARTIAL +coverage/unreachable/break/main.rs, 16, FULL +coverage/unreachable/break/main.rs, 17, FULL +coverage/unreachable/break/main.rs, 18, FULL +coverage/unreachable/break/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/unreachable/break/main.rs new file mode 100644 index 000000000000..4e795bd2a6ea --- /dev/null +++ b/tests/coverage/unreachable/break/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn find_positive(nums: &[i32]) -> Option { + for &num in nums { + if num > 0 { + return Some(num); + } + } + // This part is unreachable if there is at least one positive number. + None +} + +#[kani::proof] +fn main() { + let numbers = [-3, -1, 0, 2, 4]; + let result = find_positive(&numbers); + assert_eq!(result, Some(2)); +} diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected new file mode 100644 index 000000000000..214cbfa827bd --- /dev/null +++ b/tests/coverage/unreachable/check_id/expected @@ -0,0 +1,16 @@ +coverage/unreachable/check_id/main.rs, 5, FULL +coverage/unreachable/check_id/main.rs, 6, FULL +coverage/unreachable/check_id/main.rs, 8, NONE +coverage/unreachable/check_id/main.rs, 10, FULL +coverage/unreachable/check_id/main.rs, 14, FULL +coverage/unreachable/check_id/main.rs, 15, FULL +coverage/unreachable/check_id/main.rs, 16, FULL +coverage/unreachable/check_id/main.rs, 17, FULL +coverage/unreachable/check_id/main.rs, 18, FULL +coverage/unreachable/check_id/main.rs, 19, FULL +coverage/unreachable/check_id/main.rs, 20, FULL +coverage/unreachable/check_id/main.rs, 21, FULL +coverage/unreachable/check_id/main.rs, 22, FULL +coverage/unreachable/check_id/main.rs, 23, FULL +coverage/unreachable/check_id/main.rs, 24, FULL +coverage/unreachable/check_id/main.rs, 25, NONE diff --git a/tests/coverage/unreachable/check_id/main.rs b/tests/coverage/unreachable/check_id/main.rs new file mode 100644 index 000000000000..8273a9bcc679 --- /dev/null +++ b/tests/coverage/unreachable/check_id/main.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn foo(x: i32) { + assert!(1 + 1 == 2); + if x < 9 { + // unreachable + assert!(2 + 2 == 4); + } +} + +#[kani::proof] +fn main() { + assert!(1 + 1 == 2); + let x = if kani::any() { 33 } else { 57 }; + foo(x); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(3 + 3 == 5); +} diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/unreachable/compare/expected new file mode 100644 index 000000000000..6187e232cbe7 --- /dev/null +++ b/tests/coverage/unreachable/compare/expected @@ -0,0 +1,7 @@ +coverage/unreachable/compare/main.rs, 6, PARTIAL +coverage/unreachable/compare/main.rs, 7, FULL +coverage/unreachable/compare/main.rs, 11, FULL +coverage/unreachable/compare/main.rs, 12, FULL +coverage/unreachable/compare/main.rs, 13, FULL +coverage/unreachable/compare/main.rs, 14, FULL +coverage/unreachable/compare/main.rs, 16, FULL diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/unreachable/compare/main.rs new file mode 100644 index 000000000000..a10fb84e29a8 --- /dev/null +++ b/tests/coverage/unreachable/compare/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn compare(x: u16, y: u16) -> u16 { + // The line below should be reported as PARTIAL for having both REACHABLE and UNREACHABLE checks + if x >= y { 1 } else { 0 } +} + +#[kani::proof] +fn main() { + let x: u16 = kani::any(); + let y: u16 = kani::any(); + if x >= y { + compare(x, y); + } +} diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected new file mode 100644 index 000000000000..ca67a4938193 --- /dev/null +++ b/tests/coverage/unreachable/contradiction/expected @@ -0,0 +1,6 @@ +coverage/unreachable/contradiction/main.rs, 5, FULL +coverage/unreachable/contradiction/main.rs, 6, FULL +coverage/unreachable/contradiction/main.rs, 7, PARTIAL +coverage/unreachable/contradiction/main.rs, 8, NONE +coverage/unreachable/contradiction/main.rs, 11, FULL +coverage/unreachable/contradiction/main.rs, 13, FULL diff --git a/tests/coverage/unreachable/contradiction/main.rs b/tests/coverage/unreachable/contradiction/main.rs new file mode 100644 index 000000000000..fe79107e8962 --- /dev/null +++ b/tests/coverage/unreachable/contradiction/main.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] +fn contradiction() { + let x: u8 = kani::any(); + if x > 5 { + if x < 2 { + let y = x; + } + } else { + assert!(x < 10); + } +} diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected new file mode 100644 index 000000000000..25fdfed4c863 --- /dev/null +++ b/tests/coverage/unreachable/debug-assert/expected @@ -0,0 +1,4 @@ +coverage/unreachable/debug-assert/main.rs, 6, PARTIAL +coverage/unreachable/debug-assert/main.rs, 7, PARTIAL +coverage/unreachable/debug-assert/main.rs, 8, NONE +coverage/unreachable/debug-assert/main.rs, 10, NONE diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs new file mode 100644 index 000000000000..ab3ab41e47d0 --- /dev/null +++ b/tests/coverage/unreachable/debug-assert/main.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + for i in 0..4 { + debug_assert!(i > 0, "This should fail and stop the execution"); + assert!(i == 0, "This should be unreachable"); + } +} diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected new file mode 100644 index 000000000000..63081358941a --- /dev/null +++ b/tests/coverage/unreachable/divide/expected @@ -0,0 +1,7 @@ +coverage/unreachable/divide/main.rs, 6, FULL +coverage/unreachable/divide/main.rs, 7, FULL +coverage/unreachable/divide/main.rs, 9, NONE +coverage/unreachable/divide/main.rs, 11, FULL +coverage/unreachable/divide/main.rs, 15, FULL +coverage/unreachable/divide/main.rs, 16, FULL +coverage/unreachable/divide/main.rs, 17, FULL diff --git a/tests/coverage/unreachable/divide/main.rs b/tests/coverage/unreachable/divide/main.rs new file mode 100644 index 000000000000..ba6afab83135 --- /dev/null +++ b/tests/coverage/unreachable/divide/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that checks for UNREACHABLE panics. The panic is reported as NONE for the assumption that the divisor is not zero. +fn divide(a: i32, b: i32) -> i32 { + if b != 0 { + return a / b; + } else { + panic!("Division by zero"); + } +} + +#[kani::proof] +fn main() { + let y: i32 = kani::any(); + kani::assume(y != 0); + let result = divide(10, y); + assert_eq!(result, 5); +} diff --git a/tests/coverage/unreachable/early-return/expected b/tests/coverage/unreachable/early-return/expected new file mode 100644 index 000000000000..466c1775408b --- /dev/null +++ b/tests/coverage/unreachable/early-return/expected @@ -0,0 +1,10 @@ +coverage/unreachable/early-return/main.rs, 5, PARTIAL +coverage/unreachable/early-return/main.rs, 6, FULL +coverage/unreachable/early-return/main.rs, 7, FULL +coverage/unreachable/early-return/main.rs, 10, NONE +coverage/unreachable/early-return/main.rs, 11, PARTIAL +coverage/unreachable/early-return/main.rs, 15, FULL +coverage/unreachable/early-return/main.rs, 16, FULL +coverage/unreachable/early-return/main.rs, 17, FULL +coverage/unreachable/early-return/main.rs, 18, FULL +coverage/unreachable/early-return/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/early-return/main.rs b/tests/coverage/unreachable/early-return/main.rs new file mode 100644 index 000000000000..4e50c1f8a3b7 --- /dev/null +++ b/tests/coverage/unreachable/early-return/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn find_index(nums: &[i32], target: i32) -> Option { + for (index, &num) in nums.iter().enumerate() { + if num == target { + return Some(index); + } + } + None +} + +#[kani::proof] +fn main() { + let numbers = [10, 20, 30, 40, 50]; + let target = 30; + let result = find_index(&numbers, target); + assert_eq!(result, Some(2)); +} diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected new file mode 100644 index 000000000000..4460f23a80de --- /dev/null +++ b/tests/coverage/unreachable/if-statement/expected @@ -0,0 +1,10 @@ +coverage/unreachable/if-statement/main.rs, 5, FULL +coverage/unreachable/if-statement/main.rs, 7, PARTIAL +coverage/unreachable/if-statement/main.rs, 8, NONE +coverage/unreachable/if-statement/main.rs, 9, NONE +coverage/unreachable/if-statement/main.rs, 11, NONE +coverage/unreachable/if-statement/main.rs, 13, FULL +coverage/unreachable/if-statement/main.rs, 17, FULL +coverage/unreachable/if-statement/main.rs, 18, FULL +coverage/unreachable/if-statement/main.rs, 19, FULL +coverage/unreachable/if-statement/main.rs, 20, FULL diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/unreachable/if-statement/main.rs new file mode 100644 index 000000000000..f497cd76808e --- /dev/null +++ b/tests/coverage/unreachable/if-statement/main.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn check_number(num: i32) -> &'static str { + if num > 0 { + // The line is partially covered because the if statement is UNREACHABLE while the else statement is reachable + if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" } + } else if num < 0 { + "Negative" + } else { + "Zero" + } +} + +#[kani::proof] +fn main() { + let number = 7; + let result = check_number(number); + assert_eq!(result, "Positive and Odd"); +} diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected new file mode 100644 index 000000000000..17a52666c08d --- /dev/null +++ b/tests/coverage/unreachable/multiple-harnesses/expected @@ -0,0 +1,39 @@ +Checking harness fully_covered... +coverage/unreachable/multiple-harnesses/main.rs, 5, FULL +coverage/unreachable/multiple-harnesses/main.rs, 7, FULL +coverage/unreachable/multiple-harnesses/main.rs, 8, FULL +coverage/unreachable/multiple-harnesses/main.rs, 9, FULL +coverage/unreachable/multiple-harnesses/main.rs, 11, FULL +coverage/unreachable/multiple-harnesses/main.rs, 13, FULL +coverage/unreachable/multiple-harnesses/main.rs, 14, FULL +coverage/unreachable/multiple-harnesses/main.rs, 15, FULL +coverage/unreachable/multiple-harnesses/main.rs, 17, FULL +coverage/unreachable/multiple-harnesses/main.rs, 20, FULL +coverage/unreachable/multiple-harnesses/main.rs, 21, FULL +coverage/unreachable/multiple-harnesses/main.rs, 23, FULL +coverage/unreachable/multiple-harnesses/main.rs, 26, FULL +coverage/unreachable/multiple-harnesses/main.rs, 40, FULL +coverage/unreachable/multiple-harnesses/main.rs, 41, FULL +coverage/unreachable/multiple-harnesses/main.rs, 42, FULL +coverage/unreachable/multiple-harnesses/main.rs, 43, FULL +coverage/unreachable/multiple-harnesses/main.rs, 44, FULL + +Checking harness mostly_covered... +coverage/unreachable/multiple-harnesses/main.rs, 5, FULL +coverage/unreachable/multiple-harnesses/main.rs, 7, FULL +coverage/unreachable/multiple-harnesses/main.rs, 8, FULL +coverage/unreachable/multiple-harnesses/main.rs, 9, FULL +coverage/unreachable/multiple-harnesses/main.rs, 11, FULL +coverage/unreachable/multiple-harnesses/main.rs, 13, FULL +coverage/unreachable/multiple-harnesses/main.rs, 14, FULL +coverage/unreachable/multiple-harnesses/main.rs, 15, FULL +coverage/unreachable/multiple-harnesses/main.rs, 17, FULL +coverage/unreachable/multiple-harnesses/main.rs, 20, FULL +coverage/unreachable/multiple-harnesses/main.rs, 21, FULL +coverage/unreachable/multiple-harnesses/main.rs, 23, NONE +coverage/unreachable/multiple-harnesses/main.rs, 26, FULL +coverage/unreachable/multiple-harnesses/main.rs, 31, FULL +coverage/unreachable/multiple-harnesses/main.rs, 32, FULL +coverage/unreachable/multiple-harnesses/main.rs, 33, FULL +coverage/unreachable/multiple-harnesses/main.rs, 34, FULL +coverage/unreachable/multiple-harnesses/main.rs, 35, FULL diff --git a/tests/coverage/unreachable/multiple-harnesses/main.rs b/tests/coverage/unreachable/multiple-harnesses/main.rs new file mode 100644 index 000000000000..9cf7dc4101e6 --- /dev/null +++ b/tests/coverage/unreachable/multiple-harnesses/main.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn estimate_size(x: u32) -> u32 { + assert!(x < 4096); + + if x < 256 { + if x < 128 { + return 1; + } else { + return 3; + } + } else if x < 1024 { + if x > 1022 { + return 4; + } else { + return 5; + } + } else { + if x < 2048 { + return 7; + } else { + return 9; + } + } +} + +#[cfg(kani)] +#[kani::proof] +fn mostly_covered() { + let x: u32 = kani::any(); + kani::assume(x < 2048); + let y = estimate_size(x); + assert!(y < 10); +} + +#[cfg(kani)] +#[kani::proof] +fn fully_covered() { + let x: u32 = kani::any(); + kani::assume(x < 4096); + let y = estimate_size(x); + assert!(y < 10); +} diff --git a/tests/coverage/unreachable/return/expected b/tests/coverage/unreachable/return/expected new file mode 100644 index 000000000000..139f81840aab --- /dev/null +++ b/tests/coverage/unreachable/return/expected @@ -0,0 +1,8 @@ +coverage/unreachable/return/main.rs, 5, FULL +coverage/unreachable/return/main.rs, 6, FULL +coverage/unreachable/return/main.rs, 9, NONE +coverage/unreachable/return/main.rs, 10, PARTIAL +coverage/unreachable/return/main.rs, 14, FULL +coverage/unreachable/return/main.rs, 15, FULL +coverage/unreachable/return/main.rs, 16, FULL +coverage/unreachable/return/main.rs, 17, FULL diff --git a/tests/coverage/unreachable/return/main.rs b/tests/coverage/unreachable/return/main.rs new file mode 100644 index 000000000000..ccd76a5b4f8e --- /dev/null +++ b/tests/coverage/unreachable/return/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn greet(is_guest: bool) -> &'static str { + if is_guest { + return "Welcome, Guest!"; + } + // This part is unreachable if is_guest is true. + "Hello, User!" +} + +#[kani::proof] +fn main() { + let is_guest = true; + let message = greet(is_guest); + assert_eq!(message, "Welcome, Guest!"); +} diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected new file mode 100644 index 000000000000..cf45a502d295 --- /dev/null +++ b/tests/coverage/unreachable/tutorial_unreachable/expected @@ -0,0 +1,5 @@ +coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE +coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL diff --git a/tests/coverage/unreachable/tutorial_unreachable/main.rs b/tests/coverage/unreachable/tutorial_unreachable/main.rs new file mode 100644 index 000000000000..c56e591446cf --- /dev/null +++ b/tests/coverage/unreachable/tutorial_unreachable/main.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn unreachable_example() { + let x = 5; + let y = x + 2; + if x > y { + assert!(x < 8); + } +} diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected new file mode 100644 index 000000000000..8fa3ec8b870f --- /dev/null +++ b/tests/coverage/unreachable/variant/expected @@ -0,0 +1,10 @@ +coverage/unreachable/variant/main.rs, 15, FULL +coverage/unreachable/variant/main.rs, 16, NONE +coverage/unreachable/variant/main.rs, 17, NONE +coverage/unreachable/variant/main.rs, 18, FULL +coverage/unreachable/variant/main.rs, 19, NONE +coverage/unreachable/variant/main.rs, 21, NONE +coverage/unreachable/variant/main.rs, 23, FULL +coverage/unreachable/variant/main.rs, 27, FULL +coverage/unreachable/variant/main.rs, 28, FULL +coverage/unreachable/variant/main.rs, 29, FULL diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs new file mode 100644 index 000000000000..ca53b8ccfd18 --- /dev/null +++ b/tests/coverage/unreachable/variant/main.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a `match` statement matching on +//! all enum variants. + +enum Direction { + Up, + Down, + Left, + Right, +} + +fn print_direction(dir: Direction) { + match dir { + Direction::Up => println!("Going up!"), + Direction::Down => println!("Going down!"), + Direction::Left => println!("Going left!"), + Direction::Right => println!("Going right!"), + // This part is unreachable since we cover all variants in the match. + _ => {} + } +} + +#[kani::proof] +fn main() { + let direction = Direction::Left; + print_direction(direction); +} diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected new file mode 100644 index 000000000000..e47941f17db2 --- /dev/null +++ b/tests/coverage/unreachable/vectors/expected @@ -0,0 +1,6 @@ +coverage/unreachable/vectors/main.rs, 8, FULL +coverage/unreachable/vectors/main.rs, 11, FULL +coverage/unreachable/vectors/main.rs, 13, PARTIAL +coverage/unreachable/vectors/main.rs, 15, NONE +coverage/unreachable/vectors/main.rs, 17, FULL +coverage/unreachable/vectors/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs new file mode 100644 index 000000000000..a44c4bb47c3d --- /dev/null +++ b/tests/coverage/unreachable/vectors/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a guarded out-of-bounds access. + +#[kani::proof] +fn main() { + let numbers = vec![1, 2, 3, 4, 5]; + + // Attempt to access the 10th element of the vector, which is out of bounds. + let tenth_element = numbers.get(9); + + if let Some(value) = tenth_element { + // This part is unreachable since the vector has only 5 elements (indices 0 to 4). + println!("The 10th element is: {}", value); + } else { + println!("The 10th element is out of bounds!"); + } +} diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected new file mode 100644 index 000000000000..a0e43c183846 --- /dev/null +++ b/tests/coverage/unreachable/while-loop-break/expected @@ -0,0 +1,11 @@ +coverage/unreachable/while-loop-break/main.rs, 8, FULL +coverage/unreachable/while-loop-break/main.rs, 9, FULL +coverage/unreachable/while-loop-break/main.rs, 10, FULL +coverage/unreachable/while-loop-break/main.rs, 11, FULL +coverage/unreachable/while-loop-break/main.rs, 13, FULL +coverage/unreachable/while-loop-break/main.rs, 15, NONE +coverage/unreachable/while-loop-break/main.rs, 16, PARTIAL +coverage/unreachable/while-loop-break/main.rs, 20, FULL +coverage/unreachable/while-loop-break/main.rs, 21, FULL +coverage/unreachable/while-loop-break/main.rs, 22, FULL +coverage/unreachable/while-loop-break/main.rs, 23, FULL diff --git a/tests/coverage/unreachable/while-loop-break/main.rs b/tests/coverage/unreachable/while-loop-break/main.rs new file mode 100644 index 000000000000..cb7c6276b147 --- /dev/null +++ b/tests/coverage/unreachable/while-loop-break/main.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a `while` loop that returns before +//! running the last iteration. + +fn find_first_negative(nums: &[i32]) -> Option { + let mut index = 0; + while index < nums.len() { + if nums[index] < 0 { + return Some(nums[index]); + } + index += 1; + } + None +} + +#[kani::proof] +fn main() { + let numbers = [1, 2, -3, 4, -5]; + let result = find_first_negative(&numbers); + assert_eq!(result, Some(-3)); +} diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index f71bc535a11e..99ec78bef693 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -19,6 +19,7 @@ pub enum Mode { KaniFixme, CargoKani, CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`. + CoverageBased, Exec, Expected, Stub, @@ -32,6 +33,7 @@ impl FromStr for Mode { "kani-fixme" => Ok(KaniFixme), "cargo-kani" => Ok(CargoKani), "cargo-kani-test" => Ok(CargoKaniTest), + "coverage-based" => Ok(CoverageBased), "exec" => Ok(Exec), "expected" => Ok(Expected), "stub-tests" => Ok(Stub), @@ -47,6 +49,7 @@ impl fmt::Display for Mode { KaniFixme => "kani-fixme", CargoKani => "cargo-kani", CargoKaniTest => "cargo-kani-test", + CoverageBased => "coverage-based", Exec => "exec", Expected => "expected", Stub => "stub-tests", diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 0dd403ba1b2f..cdef1446763a 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -94,7 +94,7 @@ pub fn parse_config(args: Vec) -> Config { .optflag("", "report-time", "report the time of each test. Configuration is done via env variables, like \ rust unit tests.") - .optmulti("", "kani-flag", + .optmulti("", "kani-flag", "pass extra flags to Kani. Note that this may cause spurious failures if the \ passed flag conflicts with the test configuration. Only works for `kani`, \ `cargo-kani`, and `expected` modes." diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 04647f7b6572..7fad336dffdc 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -7,7 +7,9 @@ use crate::common::KaniFailStep; use crate::common::{output_base_dir, output_base_name}; -use crate::common::{CargoKani, CargoKaniTest, Exec, Expected, Kani, KaniFixme, Stub}; +use crate::common::{ + CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, +}; use crate::common::{Config, TestPaths}; use crate::header::TestProps; use crate::read2::read2; @@ -75,6 +77,7 @@ impl<'test> TestCx<'test> { KaniFixme => self.run_kani_test(), CargoKani => self.run_cargo_kani_test(false), CargoKaniTest => self.run_cargo_kani_test(true), + CoverageBased => self.run_expected_coverage_test(), Exec => self.run_exec_test(), Expected => self.run_expected_test(), Stub => self.run_stub_test(), @@ -311,6 +314,22 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } + /// Run coverage based output for kani on a single file + fn run_kani_with_coverage(&self) -> ProcRes { + let mut kani = Command::new("kani"); + if !self.props.compile_flags.is_empty() { + kani.env("RUSTFLAGS", self.props.compile_flags.join(" ")); + } + kani.arg(&self.testpaths.file).args(&self.props.kani_flags); + kani.arg("--coverage").args(&["-Z", "line-coverage"]); + + if !self.props.cbmc_flags.is_empty() { + kani.arg("--cbmc-args").args(&self.props.cbmc_flags); + } + + self.compose_and_run(kani) + } + /// Runs an executable file and: /// * Checks the expected output if an expected file is specified /// * Checks the exit code (assumed to be 0 by default) @@ -380,6 +399,13 @@ impl<'test> TestCx<'test> { self.verify_output(&proc_res, &expected_path); } + /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`. + fn run_expected_coverage_test(&self) { + let proc_res = self.run_kani_with_coverage(); + let expected_path = self.testpaths.file.parent().unwrap().join("expected"); + self.verify_output(&proc_res, &expected_path); + } + /// Runs Kani with stub implementations of various data structures. /// Currently, it only runs tests for the Vec module with the (Kani)Vec /// abstraction. At a later stage, it should be possible to add command-line