From b786e18d4ddc09a04c9e93ce983be86332a4b113 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 8 Feb 2024 22:00:33 +0000 Subject: [PATCH 01/59] Adopt Rust's region-based coverage instrumentation --- .../codegen_cprover_gotoc/codegen/assert.rs | 11 +- .../codegen_cprover_gotoc/codegen/block.rs | 33 +---- .../codegen_cprover_gotoc/codegen/function.rs | 56 +++++++++ .../codegen/statement.rs | 22 +++- kani-driver/src/args/coverage_args.rs | 17 +++ kani-driver/src/args/mod.rs | 6 + kani-driver/src/call_cbmc.rs | 7 ++ kani-driver/src/call_single_file.rs | 6 + kani-driver/src/cbmc_property_renderer.rs | 114 ++++++++++-------- kani-driver/src/coverage/coverage.rs | 23 ++++ kani-driver/src/coverage/mod.rs | 4 + kani-driver/src/main.rs | 5 + library/kani/src/lib.rs | 1 + tools/build-kani/src/sysroot.rs | 2 +- 14 files changed, 219 insertions(+), 88 deletions(-) create mode 100644 kani-driver/src/args/coverage_args.rs create mode 100644 kani-driver/src/coverage/coverage.rs create mode 100644 kani-driver/src/coverage/mod.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index cad3595bca50..a951a9349e90 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -21,6 +21,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; +use rustc_middle::mir::coverage::CodeRegion; use stable_mir::ty::Span as SpanStable; use strum_macros::{AsRefStr, EnumString}; use tracing::debug; @@ -147,18 +148,14 @@ impl<'tcx> GotocCtx<'tcx> { } /// Generate a cover statement for code coverage reports. - pub fn codegen_coverage(&self, span: SpanStable) -> Stmt { + pub fn codegen_coverage(&self, info: &str, span: SpanStable, code_region: CodeRegion) -> Stmt { let loc = self.codegen_caller_span_stable(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, - ) + let fmt = format!("{info} - {code_region:?}"); + self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &fmt, loc) } // The above represent the basic operations we can perform w.r.t. assert/assume/cover diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index 5fe28097a2e0..1b28de887002 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -20,53 +20,24 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) { debug!(?bb, "codegen_block"); let label = bb_label(bb); - let check_coverage = self.queries.args().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); - // When checking coverage, the `coverage` check should be - // labelled instead. - if check_coverage { - let span = term.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)); - } + self.current_fn_mut().push_onto_block(tcode.with_label(label)); } _ => { let stmt = &bbd.statements[0]; let scode = self.codegen_statement(stmt); - // When checking coverage, the `coverage` check should be - // labelled instead. - if check_coverage { - let span = stmt.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)); - } + self.current_fn_mut().push_onto_block(scode.with_label(label)); for s in &bbd.statements[1..] { - if check_coverage { - let span = s.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 = &bbd.terminator; - if check_coverage { - let span = term.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); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d55696bfdc87..195e90bd70c7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -216,3 +216,59 @@ impl<'tcx> GotocCtx<'tcx> { self.reset_current_fn(); } } + +pub mod rustc_smir { + use rustc_middle::mir::coverage::CovTerm; + use rustc_middle::ty::TyCtxt; + use stable_mir::mir::mono::Instance; + use stable_mir::Opaque; + use crate::stable_mir::CrateDef; + use rustc_middle::mir::coverage::CodeRegion; + + type CoverageOpaque = stable_mir::Opaque; + + /// Wrapper since we don't have a structured coverage. + pub fn coverage_opaque_span( + tcx: TyCtxt, + coverage_opaque: CoverageOpaque, + instance: Instance, + ) -> Option { + let cov_term = parse_coverage(coverage_opaque)?; + coverage_span(tcx, cov_term, instance) + } + + /// Function that should be the internal implementation of opaque + pub fn coverage_span<'tcx>(tcx: TyCtxt<'tcx>, coverage: CovTerm, instance: Instance) -> Option { + let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); + let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); + let cov_info = &body.function_coverage_info.clone().unwrap(); + // NOTE: This helps see coverage mappings a given function + // println!("COVERAGE: {:?}", &cov_info.mappings); + for mapping in &cov_info.mappings { + if mapping.kind.terms().next().unwrap() == coverage { + return Some(mapping.code_region.clone()); + } + } + None + } + + fn parse_coverage(coverage_opaque: Opaque) -> Option { + let coverage_clone = coverage_opaque.to_string(); + let coverage_str = { + let coverage_fmt = format!("{coverage_clone}"); + let cov_fmt_no_prefix = coverage_fmt.strip_prefix("Coverage { kind: ").unwrap(); + cov_fmt_no_prefix.strip_suffix(" }").unwrap().to_string() + }; + if coverage_str == "Zero" { + return Some(CovTerm::Zero); + } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { + let (num_str, _rest) = rest.split_once(")").unwrap(); + let num = num_str.parse::().unwrap(); + Some(CovTerm::Counter(num.into())) + } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { + let (num_str, _rest) = rest.split_once(")").unwrap(); + let num = num_str.parse::().unwrap(); + Some(CovTerm::Expression(num.into())) + } else { None } + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 9a78515fde90..e69624aedbb9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -17,6 +17,7 @@ use stable_mir::mir::{ Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, }; use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; +use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::coverage_opaque_span; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -108,12 +109,31 @@ impl<'tcx> GotocCtx<'tcx> { location, ) } + StatementKind::Coverage(cov) => { + // debug!(?opaque, "StatementKind::Coverage Opaque"); + // self.codegen_coverage(stmt.span) + + let fun = self.current_fn().readable_name(); + let instance = self.current_fn().instance_stable(); + let cov_info = format!("{cov:?} {fun}"); + // NOTE: This helps see the coverage info we're processing + println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); + let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); + if let Some(code_region) = cov_span { + let coverage_stmt = self.codegen_coverage(&cov_info, stmt.span, code_region); + // TODO: Avoid single-statement blocks when conversion of + // standalone statements to the irep format is fixed. + // More details in + Stmt::block(vec![coverage_stmt], location) + } else { + Stmt::skip(location) + } + } StatementKind::PlaceMention(_) => todo!(), StatementKind::FakeRead(..) | StatementKind::Retag(_, _) | StatementKind::AscribeUserType { .. } | StatementKind::Nop - | StatementKind::Coverage { .. } | StatementKind::ConstEvalCounter => Stmt::skip(location), } .with_location(location) diff --git a/kani-driver/src/args/coverage_args.rs b/kani-driver/src/args/coverage_args.rs new file mode 100644 index 000000000000..31827d88f0e8 --- /dev/null +++ b/kani-driver/src/args/coverage_args.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::args::CommonArgs; +use clap::Parser; + +#[derive(Debug, Parser)] +pub struct CargoCoverageArgs { + #[command(flatten)] + pub coverage: CoverageArgs, +} + +#[derive(Debug, clap::Args)] +pub struct CoverageArgs { + /// Common args always available to Kani subcommands. + #[command(flatten)] + pub common_opts: CommonArgs, +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 36d9e0af2d0e..2d7ce3415a84 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -6,10 +6,12 @@ pub mod assess_args; pub mod cargo; pub mod common; pub mod playback_args; +pub mod coverage_args; pub use assess_args::*; use self::common::*; +use self::coverage_args::CargoCoverageArgs; use crate::args::cargo::CargoTargetArgs; use crate::util::warning; use cargo::CargoCommonArgs; @@ -115,6 +117,9 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), + + /// TBD + Cov(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -489,6 +494,7 @@ impl ValidateArgs for CargoKaniSubcommand { match self { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), + CargoKaniSubcommand::Cov(_) => Ok(()), CargoKaniSubcommand::Playback(playback) => playback.validate(), } } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 7d0edf6f50e5..80e63d676506 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -14,6 +14,7 @@ use crate::cbmc_output_parser::{ extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; +use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; use crate::session::KaniSession; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. @@ -54,6 +55,8 @@ pub struct VerificationResult { pub runtime: Duration, /// Whether concrete playback generated a test pub generated_concrete_test: bool, + /// The coverage results? + pub coverage_results: Option, } impl KaniSession { @@ -262,6 +265,7 @@ impl VerificationResult { results: Ok(results), runtime, generated_concrete_test: false, + coverage_results: None, } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure @@ -271,6 +275,7 @@ impl VerificationResult { results: Err(output.process_status), runtime, generated_concrete_test: false, + coverage_results: None, } } } @@ -282,6 +287,7 @@ impl VerificationResult { results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, + coverage_results: None, } } @@ -295,6 +301,7 @@ impl VerificationResult { results: Err(42), runtime: Duration::from_secs(0), generated_concrete_test: false, + coverage_results: None, } } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 07899c8c4899..ea04dd0fb7de 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -123,6 +123,12 @@ impl KaniSession { let lib_path = lib_folder().unwrap(); let mut flags: Vec<_> = base_rustc_flags(lib_path); // We only use panic abort strategy for verification since we cannot handle unwind logic. + if self.args.coverage { + flags.extend_from_slice( + // &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "--emit=mir"].map(OsString::from), + &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "-C", "opt-level=0"].map(OsString::from), + ); + } flags.extend_from_slice( &[ "-C", diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index c233959abd6a..66933f4bc1f5 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -4,11 +4,16 @@ use crate::args::OutputFormat; use crate::call_cbmc::{FailedProperties, VerificationStatus}; use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem}; +use crate::coverage::cov_results::{CoverageCheck, CoverageRegion, CoverageResults, CoverageTerm, fmt_coverage_results}; use console::style; use once_cell::sync::Lazy; use regex::Regex; use rustc_demangle::demangle; use std::collections::{BTreeMap, HashMap}; +use std::fs::File; +use std::io::{BufRead, BufReader}; +use std::path::PathBuf; +use std::sync::OnceLock; use strum_macros::{AsRefStr, Display}; type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>; @@ -150,15 +155,6 @@ 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"; @@ -445,58 +441,80 @@ pub fn format_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); + let new_coverage_output = format_result_new_coverage(&coverage_checks); + let result = format!("{}\n{}", verification_output, new_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 { +fn format_result_new_coverage(properties: &[Property]) -> String { let mut formatted_output = String::new(); - formatted_output.push_str("\nCoverage Results:\n"); + formatted_output.push_str("\nCoverage Results (NEW):\n"); + + let mut coverage_results: CoverageResults = BTreeMap::default(); + + let re = { + static RE: OnceLock = OnceLock::new(); + RE.get_or_init(|| { + Regex::new( + r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + ) + .unwrap() + }) + }; - let mut coverage_results: BTreeMap> = - BTreeMap::default(); + let re2 = { + static RE: OnceLock = OnceLock::new(); + RE.get_or_init(|| { + Regex::new( + r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + ) + .unwrap() + }) + }; 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 - }; + if let Some(captures) = re.captures(&prop.description) { + let function = demangle(&captures["func_name"]).to_string(); + let counter_num = &captures["counter_num"]; + let status = prop.status; + let span = captures["span"].to_string(); + + let term = CoverageTerm::Counter(counter_num.parse().unwrap()); + let region = CoverageRegion::from_str(span); + + let cov_check = CoverageCheck::new(function, term, region, status); + let file = cov_check.region.file.clone(); + + if coverage_results.contains_key(&file) { + coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); + } else { + coverage_results.insert(file, vec![cov_check]); + } + } - // 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); - } + if let Some(captures) = re2.captures(&prop.description) { + let function = demangle(&captures["func_name"]).to_string(); + let expr_num = &captures["expr_num"]; + let status = prop.status; + let span = captures["span"].to_string(); + + let term = CoverageTerm::Expression(expr_num.parse().unwrap()); + let region = CoverageRegion::from_str(span); - // 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)); + let cov_check = CoverageCheck::new(function, term, region, status); + let file = cov_check.region.file.clone(); + + if coverage_results.contains_key(&file) { + coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); + } else { + coverage_results.insert(file, vec![cov_check]); + } } - formatted_output.push('\n'); } - - formatted_output + fmt_coverage_results(&coverage_results).expect("error: couldn't format coverage results") } + /// 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 { diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs new file mode 100644 index 000000000000..44f8cc1ea82b --- /dev/null +++ b/kani-driver/src/coverage/coverage.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::args::coverage_args::CargoCoverageArgs; +use crate::KaniSession; +use crate::project; +use crate::harness_runner; +use anyhow::Result; +use tracing::debug; + +pub fn coverage_cargo(mut session: KaniSession, _args: CargoCoverageArgs) -> Result<()> { + session.args.coverage = true; + let project = project::cargo_project(&session, false)?; + let harnesses = session.determine_targets(&project.get_all_harnesses())?; + debug!(n = harnesses.len(), ?harnesses, "coverage_cargo"); + + // Verification + let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; + let _results = runner.check_all_harnesses(&harnesses)?; + + // More to come later + Ok(()) +} diff --git a/kani-driver/src/coverage/mod.rs b/kani-driver/src/coverage/mod.rs new file mode 100644 index 000000000000..8bac21cc742c --- /dev/null +++ b/kani-driver/src/coverage/mod.rs @@ -0,0 +1,4 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +pub mod coverage; +pub mod cov_results; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 798625560970..71fa8ff8196a 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -11,6 +11,7 @@ use args_toml::join_args; use crate::args::StandaloneSubcommand; use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; +use crate::coverage::coverage::{coverage_cargo}; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; @@ -30,6 +31,7 @@ mod call_single_file; mod cbmc_output_parser; mod cbmc_property_renderer; mod concrete_playback; +mod coverage; mod harness_runner; mod metadata; mod project; @@ -78,6 +80,9 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } + Some(CargoKaniSubcommand::Cov(args)) => { + return coverage_cargo(session, *args); + } None => {} } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 25b1b389a2b1..a492620076a2 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -72,6 +72,7 @@ pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; #[cfg(not(feature = "concrete_playback"))] pub fn assume(cond: bool) { let _ = cond; + unreachable!("test"); } #[inline(never)] diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index b831ed0d63a8..ad0d61e539a2 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -74,7 +74,7 @@ pub fn build_lib(bin_folder: &Path) -> Result<()> { fn build_verification_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; - let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std"]; + let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std", "-Cinstrument-coverage", "-Z", "no-profiler-runtime"]; build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args) } From 87419455da16e539be83122e7b0272928e132a20 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 2 Apr 2024 15:52:46 +0000 Subject: [PATCH 02/59] Add missing file --- kani-driver/src/coverage/cov_results.rs | 77 +++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 kani-driver/src/coverage/cov_results.rs diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs new file mode 100644 index 000000000000..c62e5ae81972 --- /dev/null +++ b/kani-driver/src/coverage/cov_results.rs @@ -0,0 +1,77 @@ +use crate::cbmc_output_parser::CheckStatus; +use std::{collections::BTreeMap, fmt::Display}; +use std::fmt::{self, Write}; +use anyhow::Result; + +pub type CoverageResults = BTreeMap>; + +pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { + let mut fmt_string = String::new(); + for (file, checks) in coverage_results.iter() { + let mut checks_by_function: BTreeMap> = BTreeMap::new(); + + // // Group checks by function + for check in checks { + // Insert the check into the vector corresponding to its function + checks_by_function + .entry(check.function.clone()) + .or_insert_with(Vec::new) + .push(check.clone()); + } + + for (function, checks) in checks_by_function { + writeln!(fmt_string, "{file} ({function})")?; + let mut sorted_checks: Vec = checks.to_vec(); + sorted_checks.sort_by(|a, b| a.region.start.cmp(&b.region.start)); + for check in sorted_checks.iter() { + writeln!(fmt_string, " * {} {}", check.region, check.status)?; + } + writeln!(fmt_string, "")?; + } + } + Ok(fmt_string) +} + +#[derive(Debug, Clone)] +pub struct CoverageCheck { + pub function: String, + term: CoverageTerm, + pub region: CoverageRegion, + status: CheckStatus, +} + +impl CoverageCheck { + pub fn new(function: String, term: CoverageTerm, region: CoverageRegion, status: CheckStatus) -> Self { + Self {function, term, region, status } + } +} + +#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord)] +pub struct CoverageRegion { + pub file: String, + pub start: (u32, u32), + pub end: (u32, u32), +} + +impl Display for CoverageRegion { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}:{} - {}:{}", self.start.0, self.start.1, self.end.0, self.end.1) + } +} + +impl CoverageRegion { + pub fn from_str(str: String) -> Self { + let str_splits: Vec<&str> = str.split([':', '-']).map(|s| s.trim()).collect(); + assert_eq!(str_splits.len(), 5, "{str:?}"); + let file = str_splits[0].to_string(); + let start = (str_splits[1].parse().unwrap(), str_splits[2].parse().unwrap()); + let end = (str_splits[3].parse().unwrap(), str_splits[4].parse().unwrap()); + Self { file, start, end } + } +} + +#[derive(Debug, Clone)] +pub enum CoverageTerm { + Counter(u32), + Expression(u32), +} From b3813fd160907b41149b3fa697def21416c69c91 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Apr 2024 16:44:05 +0000 Subject: [PATCH 03/59] Serialize results --- kani-driver/src/call_cargo.rs | 2 +- kani-driver/src/call_cbmc.rs | 85 +++++++++++++++++++++-- kani-driver/src/cbmc_output_parser.rs | 4 +- kani-driver/src/cbmc_property_renderer.rs | 71 ++----------------- kani-driver/src/coverage/cov_results.rs | 19 +++-- kani-driver/src/coverage/coverage.rs | 44 +++++++++++- 6 files changed, 147 insertions(+), 78 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 9d27e5853696..34a6e3e1fd63 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -149,7 +149,7 @@ impl KaniSession { }) } - fn cargo_metadata(&self, build_target: &str) -> Result { + pub fn cargo_metadata(&self, build_target: &str) -> Result { let mut cmd = MetadataCommand::new(); // restrict metadata command to host platform. References: diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 80e63d676506..05a84de19746 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -3,19 +3,24 @@ use anyhow::{bail, Result}; use kani_metadata::{CbmcSolver, HarnessMetadata}; +use regex::Regex; +use rustc_demangle::demangle; use std::ffi::OsString; use std::fmt::Write; use std::path::Path; use std::process::Command; +use std::sync::OnceLock; use std::time::{Duration, Instant}; +use std::collections::BTreeMap; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; -use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; +use crate::coverage::cov_results::{self, CoverageCheck, CoverageResults}; use crate::session::KaniSession; +use crate::coverage::cov_results::{CoverageRegion, CoverageTerm}; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. /// Note: Kissat was marginally better, but it is an external solver which could be more unstable. @@ -259,13 +264,14 @@ impl VerificationResult { if let Some(results) = results { let (status, failed_properties) = verification_outcome_from_properties(&results, should_panic); + let coverage_results = coverage_results_from_properties(&results); VerificationResult { status, failed_properties, results: Ok(results), runtime, generated_concrete_test: false, - coverage_results: None, + coverage_results, } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure @@ -317,8 +323,8 @@ impl VerificationResult { let failed_properties = self.failed_properties; let show_checks = matches!(output_format, OutputFormat::Regular); - let mut result = if coverage_mode { - format_coverage(results, status, should_panic, failed_properties, show_checks) + let mut result = if let Some(cov_results) = &self.coverage_results { + format_coverage(results, cov_results, status, should_panic, failed_properties, show_checks) } else { format_result(results, status, should_panic, failed_properties, show_checks) }; @@ -394,6 +400,77 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties { } } +fn coverage_results_from_properties(properties: &[Property]) -> Option { + let cov_properties: Vec<&Property> = properties.iter().filter(|p| p.is_code_coverage_property()).collect(); + + if cov_properties.is_empty() { + return None; + } + + let re = { + static RE: OnceLock = OnceLock::new(); + RE.get_or_init(|| { + Regex::new( + r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + ) + .unwrap() + }) + }; + + let re2 = { + static RE: OnceLock = OnceLock::new(); + RE.get_or_init(|| { + Regex::new( + r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + ) + .unwrap() + }) + }; + let mut coverage_results: BTreeMap> = BTreeMap::default(); + + for prop in cov_properties { + if let Some(captures) = re.captures(&prop.description) { + let function = demangle(&captures["func_name"]).to_string(); + let counter_num = &captures["counter_num"]; + let status = prop.status; + let span = captures["span"].to_string(); + + let term = CoverageTerm::Counter(counter_num.parse().unwrap()); + let region = CoverageRegion::from_str(span); + + let cov_check = CoverageCheck::new(function, term, region, status); + let file = cov_check.region.file.clone(); + + if coverage_results.contains_key(&file) { + coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); + } else { + coverage_results.insert(file, vec![cov_check]); + } + } + + if let Some(captures) = re2.captures(&prop.description) { + let function = demangle(&captures["func_name"]).to_string(); + let expr_num = &captures["expr_num"]; + let status = prop.status; + let span = captures["span"].to_string(); + + let term = CoverageTerm::Expression(expr_num.parse().unwrap()); + let region = CoverageRegion::from_str(span); + + let cov_check = CoverageCheck::new(function, term, region, status); + let file = cov_check.region.file.clone(); + + if coverage_results.contains_key(&file) { + coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); + } else { + coverage_results.insert(file, vec![cov_check]); + } + } + } + + Some(CoverageResults::new(coverage_results)) + +} /// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind) pub fn resolve_unwind_value( args: &VerificationArgs, diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 127f98beab56..4fe7bea3d696 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -27,7 +27,7 @@ use anyhow::Result; use console::style; use pathdiff::diff_paths; use rustc_demangle::demangle; -use serde::{Deserialize, Deserializer}; +use serde::{Deserialize, Deserializer, Serialize}; use std::env; use std::io::{BufRead, BufReader}; @@ -321,7 +321,7 @@ impl std::fmt::Display for TraceData { } } -#[derive(Copy, Clone, Debug, Deserialize, PartialEq, Eq)] +#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] #[serde(rename_all = "UPPERCASE")] pub enum CheckStatus { Failure, diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 66933f4bc1f5..39ba609721fa 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -4,7 +4,7 @@ use crate::args::OutputFormat; use crate::call_cbmc::{FailedProperties, VerificationStatus}; use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem}; -use crate::coverage::cov_results::{CoverageCheck, CoverageRegion, CoverageResults, CoverageTerm, fmt_coverage_results}; +use crate::coverage::cov_results::{self, fmt_coverage_results, CoverageCheck, CoverageRegion, CoverageResults, CoverageTerm}; use console::style; use once_cell::sync::Lazy; use regex::Regex; @@ -431,87 +431,28 @@ pub fn format_result( /// results pub fn format_coverage( properties: &[Property], + cov_results: &CoverageResults, status: VerificationStatus, should_panic: bool, failed_properties: FailedProperties, show_checks: bool, ) -> String { - let (coverage_checks, non_coverage_checks): (Vec, Vec) = + 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 new_coverage_output = format_result_new_coverage(&coverage_checks); + let new_coverage_output = format_result_new_coverage(cov_results); let result = format!("{}\n{}", verification_output, new_coverage_output); result } -fn format_result_new_coverage(properties: &[Property]) -> String { +fn format_result_new_coverage(cov_results: &CoverageResults) -> String { let mut formatted_output = String::new(); formatted_output.push_str("\nCoverage Results (NEW):\n"); - let mut coverage_results: CoverageResults = BTreeMap::default(); - - let re = { - static RE: OnceLock = OnceLock::new(); - RE.get_or_init(|| { - Regex::new( - r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, - ) - .unwrap() - }) - }; - - let re2 = { - static RE: OnceLock = OnceLock::new(); - RE.get_or_init(|| { - Regex::new( - r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, - ) - .unwrap() - }) - }; - for prop in properties { - if let Some(captures) = re.captures(&prop.description) { - let function = demangle(&captures["func_name"]).to_string(); - let counter_num = &captures["counter_num"]; - let status = prop.status; - let span = captures["span"].to_string(); - - let term = CoverageTerm::Counter(counter_num.parse().unwrap()); - let region = CoverageRegion::from_str(span); - - let cov_check = CoverageCheck::new(function, term, region, status); - let file = cov_check.region.file.clone(); - - if coverage_results.contains_key(&file) { - coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); - } else { - coverage_results.insert(file, vec![cov_check]); - } - } - - if let Some(captures) = re2.captures(&prop.description) { - let function = demangle(&captures["func_name"]).to_string(); - let expr_num = &captures["expr_num"]; - let status = prop.status; - let span = captures["span"].to_string(); - - let term = CoverageTerm::Expression(expr_num.parse().unwrap()); - let region = CoverageRegion::from_str(span); - - let cov_check = CoverageCheck::new(function, term, region, status); - let file = cov_check.region.file.clone(); - - if coverage_results.contains_key(&file) { - coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); - } else { - coverage_results.insert(file, vec![cov_check]); - } - } - } - fmt_coverage_results(&coverage_results).expect("error: couldn't format coverage results") + fmt_coverage_results(&cov_results).expect("error: couldn't format coverage results") } diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index c62e5ae81972..94eb00874d82 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -2,12 +2,21 @@ use crate::cbmc_output_parser::CheckStatus; use std::{collections::BTreeMap, fmt::Display}; use std::fmt::{self, Write}; use anyhow::Result; +use serde::{Deserialize, Serialize}; -pub type CoverageResults = BTreeMap>; +#[derive(Clone, Debug, Serialize, Deserialize)] +pub struct CoverageResults { + pub data: BTreeMap>, +} +impl CoverageResults { + pub fn new(data: BTreeMap>) -> Self { + Self { data } + } +} pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { let mut fmt_string = String::new(); - for (file, checks) in coverage_results.iter() { + for (file, checks) in coverage_results.data.iter() { let mut checks_by_function: BTreeMap> = BTreeMap::new(); // // Group checks by function @@ -32,7 +41,7 @@ pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result Result<()> { session.args.coverage = true; let project = project::cargo_project(&session, false)?; @@ -16,8 +24,42 @@ pub fn coverage_cargo(mut session: KaniSession, _args: CargoCoverageArgs) -> Res // Verification let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; - let _results = runner.check_all_harnesses(&harnesses)?; + let results = runner.check_all_harnesses(&harnesses)?; + + let _ = session.save_cov_results(&results); // More to come later Ok(()) } + +impl KaniSession { + pub fn save_cov_results(&self, results: &Vec) -> Result<()> { + let build_target = env!("TARGET"); + let metadata = self.cargo_metadata(build_target)?; + let target_dir = self + .args + .target_dir + .as_ref() + .unwrap_or(&metadata.target_directory.clone().into()) + .clone() + .join("kani"); + + let outdir = target_dir.join(build_target).join("cov"); + + if !outdir.exists() { + fs::create_dir(&outdir)?; + } + + for harness_res in results { + let harness_name = harness_res.harness.mangled_name.clone(); + let file_name = outdir.join(harness_name).with_extension("kanicov"); + let mut cov_file = File::create(file_name)?; + + let cov_results = &harness_res.result.coverage_results.clone().unwrap(); + let serialized_data = serde_json::to_string(&cov_results)?; + cov_file.write_all(serialized_data.as_bytes())?; + } + + Ok(()) + } +} From 99eda5a3f09dd068e15fafa9c71973333b662efd Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Apr 2024 21:35:28 +0000 Subject: [PATCH 04/59] Print where coverage results are saved --- kani-driver/src/coverage/coverage.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index cbec9090326c..ec3d2b8e65af 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -60,6 +60,7 @@ impl KaniSession { cov_file.write_all(serialized_data.as_bytes())?; } + println!("[info] Coverage results saved to {}", &outdir.display()); Ok(()) } } From 42836c177eda708d62bd8d0e95236edb7bc68c98 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 5 Apr 2024 18:47:34 +0000 Subject: [PATCH 05/59] Match on parentheses, all props need to match --- .../src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/call_cbmc.rs | 8 ++++++-- kani-driver/src/coverage/coverage.rs | 3 --- library/kani/src/lib.rs | 1 - 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e69624aedbb9..3f7e363730e7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -115,7 +115,7 @@ impl<'tcx> GotocCtx<'tcx> { let fun = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let cov_info = format!("{cov:?} {fun}"); + let cov_info = format!("{cov:?} ({fun})"); // NOTE: This helps see the coverage info we're processing println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 05a84de19746..bc32ff597202 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -411,7 +411,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -421,7 +421,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -429,6 +429,8 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option> = BTreeMap::default(); for prop in cov_properties { + let mut prop_processed = false; + if let Some(captures) = re.captures(&prop.description) { let function = demangle(&captures["func_name"]).to_string(); let counter_num = &captures["counter_num"]; @@ -446,6 +448,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Option Result<()> { session.args.coverage = true; let project = project::cargo_project(&session, false)?; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index a492620076a2..25b1b389a2b1 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -72,7 +72,6 @@ pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; #[cfg(not(feature = "concrete_playback"))] pub fn assume(cond: bool) { let _ = cond; - unreachable!("test"); } #[inline(never)] From ec1f196ce11a3586528839481f9e373614a13871 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Apr 2024 18:53:16 +0000 Subject: [PATCH 06/59] Better splits --- .../src/codegen_cprover_gotoc/codegen/function.rs | 1 + .../src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/coverage/cov_results.rs | 14 +++++++++----- 3 files changed, 11 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 195e90bd70c7..93ac1434a5e9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -246,6 +246,7 @@ pub mod rustc_smir { // println!("COVERAGE: {:?}", &cov_info.mappings); for mapping in &cov_info.mappings { if mapping.kind.terms().next().unwrap() == coverage { + println!("COVERAGE: {:?}", mapping.code_region.clone()); return Some(mapping.code_region.clone()); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 3f7e363730e7..a5a1c0c4b58c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -117,7 +117,7 @@ impl<'tcx> GotocCtx<'tcx> { let instance = self.current_fn().instance_stable(); let cov_info = format!("{cov:?} ({fun})"); // NOTE: This helps see the coverage info we're processing - println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); + // println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); if let Some(code_region) = cov_span { let coverage_stmt = self.codegen_coverage(&cov_info, stmt.span, code_region); diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 94eb00874d82..d42d642c460e 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -70,11 +70,15 @@ impl Display for CoverageRegion { impl CoverageRegion { pub fn from_str(str: String) -> Self { - let str_splits: Vec<&str> = str.split([':', '-']).map(|s| s.trim()).collect(); - assert_eq!(str_splits.len(), 5, "{str:?}"); - let file = str_splits[0].to_string(); - let start = (str_splits[1].parse().unwrap(), str_splits[2].parse().unwrap()); - let end = (str_splits[3].parse().unwrap(), str_splits[4].parse().unwrap()); + let blank_splits: Vec<&str> = str.split_whitespace().map(|s| s.trim()).collect(); + assert!(blank_splits[1] == "-"); + let str_splits1: Vec<&str> = blank_splits[0].split([':']).collect(); + let str_splits2: Vec<&str> = blank_splits[2].split([':']).collect(); + assert_eq!(str_splits1.len(), 3, "{str:?}"); + assert_eq!(str_splits2.len(), 2, "{str:?}"); + let file = str_splits1[0].to_string(); + let start = (str_splits1[1].parse().unwrap(), str_splits1[2].parse().unwrap()); + let end = (str_splits2[0].parse().unwrap(), str_splits2[1].parse().unwrap()); Self { file, start, end } } } From a30de87083a6753ac39f870ade8223646ce0b7f9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 18 Apr 2024 21:14:53 +0000 Subject: [PATCH 07/59] Autoformat --- .../codegen_cprover_gotoc/codegen/function.rs | 18 +++++++++++------ .../codegen/statement.rs | 4 ++-- kani-driver/src/args/mod.rs | 2 +- kani-driver/src/call_cbmc.rs | 19 ++++++++++++------ kani-driver/src/call_single_file.rs | 3 ++- kani-driver/src/cbmc_property_renderer.rs | 5 +++-- kani-driver/src/coverage/cov_results.rs | 15 +++++++++----- kani-driver/src/coverage/coverage.rs | 20 +++++++++---------- kani-driver/src/coverage/mod.rs | 2 +- kani-driver/src/main.rs | 2 +- tools/build-kani/src/sysroot.rs | 8 +++++++- 11 files changed, 62 insertions(+), 36 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 93ac1434a5e9..8fdf817ee94a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -218,12 +218,12 @@ impl<'tcx> GotocCtx<'tcx> { } pub mod rustc_smir { + use crate::stable_mir::CrateDef; + use rustc_middle::mir::coverage::CodeRegion; use rustc_middle::mir::coverage::CovTerm; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::Opaque; - use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::CodeRegion; type CoverageOpaque = stable_mir::Opaque; @@ -238,7 +238,11 @@ pub mod rustc_smir { } /// Function that should be the internal implementation of opaque - pub fn coverage_span<'tcx>(tcx: TyCtxt<'tcx>, coverage: CovTerm, instance: Instance) -> Option { + pub fn coverage_span<'tcx>( + tcx: TyCtxt<'tcx>, + coverage: CovTerm, + instance: Instance, + ) -> Option { let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); @@ -264,12 +268,14 @@ pub mod rustc_smir { return Some(CovTerm::Zero); } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { let (num_str, _rest) = rest.split_once(")").unwrap(); - let num = num_str.parse::().unwrap(); - Some(CovTerm::Counter(num.into())) + let num = num_str.parse::().unwrap(); + Some(CovTerm::Counter(num.into())) } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { let (num_str, _rest) = rest.split_once(")").unwrap(); let num = num_str.parse::().unwrap(); Some(CovTerm::Expression(num.into())) - } else { None } + } else { + None + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index a5a1c0c4b58c..cc3cbbcefb85 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -3,6 +3,7 @@ use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; use super::{bb_label, PropertyClass}; +use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::coverage_opaque_span; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; @@ -17,7 +18,6 @@ use stable_mir::mir::{ Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, }; use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; -use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::coverage_opaque_span; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::Coverage(cov) => { // debug!(?opaque, "StatementKind::Coverage Opaque"); // self.codegen_coverage(stmt.span) - + let fun = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); let cov_info = format!("{cov:?} ({fun})"); diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 2d7ce3415a84..9d50927cbe64 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -5,8 +5,8 @@ pub mod assess_args; pub mod cargo; pub mod common; -pub mod playback_args; pub mod coverage_args; +pub mod playback_args; pub use assess_args::*; diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index bc32ff597202..f777d8aa79fc 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -5,13 +5,13 @@ use anyhow::{bail, Result}; use kani_metadata::{CbmcSolver, HarnessMetadata}; use regex::Regex; use rustc_demangle::demangle; +use std::collections::BTreeMap; use std::ffi::OsString; use std::fmt::Write; use std::path::Path; use std::process::Command; use std::sync::OnceLock; use std::time::{Duration, Instant}; -use std::collections::BTreeMap; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ @@ -19,8 +19,8 @@ use crate::cbmc_output_parser::{ }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::coverage::cov_results::{self, CoverageCheck, CoverageResults}; -use crate::session::KaniSession; use crate::coverage::cov_results::{CoverageRegion, CoverageTerm}; +use crate::session::KaniSession; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. /// Note: Kissat was marginally better, but it is an external solver which could be more unstable. @@ -324,7 +324,14 @@ impl VerificationResult { let show_checks = matches!(output_format, OutputFormat::Regular); let mut result = if let Some(cov_results) = &self.coverage_results { - format_coverage(results, cov_results, status, should_panic, failed_properties, show_checks) + format_coverage( + results, + cov_results, + status, + should_panic, + failed_properties, + show_checks, + ) } else { format_result(results, status, should_panic, failed_properties, show_checks) }; @@ -401,7 +408,8 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties { } fn coverage_results_from_properties(properties: &[Property]) -> Option { - let cov_properties: Vec<&Property> = properties.iter().filter(|p| p.is_code_coverage_property()).collect(); + let cov_properties: Vec<&Property> = + properties.iter().filter(|p| p.is_code_coverage_property()).collect(); if cov_properties.is_empty() { return None; @@ -439,7 +447,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Option String { fmt_coverage_results(&cov_results).expect("error: couldn't format coverage results") } - /// 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 { diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index d42d642c460e..5cd594325d69 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -1,8 +1,8 @@ use crate::cbmc_output_parser::CheckStatus; -use std::{collections::BTreeMap, fmt::Display}; -use std::fmt::{self, Write}; use anyhow::Result; use serde::{Deserialize, Serialize}; +use std::fmt::{self, Write}; +use std::{collections::BTreeMap, fmt::Display}; #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CoverageResults { @@ -27,7 +27,7 @@ pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result = checks.to_vec(); @@ -50,8 +50,13 @@ pub struct CoverageCheck { } impl CoverageCheck { - pub fn new(function: String, term: CoverageTerm, region: CoverageRegion, status: CheckStatus) -> Self { - Self {function, term, region, status } + pub fn new( + function: String, + term: CoverageTerm, + region: CoverageRegion, + status: CheckStatus, + ) -> Self { + Self { function, term, region, status } } } diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index 94922261dac4..56241cd9d9b3 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -6,10 +6,10 @@ use std::fs::File; use std::io::Write; use crate::args::coverage_args::CargoCoverageArgs; -use crate::KaniSession; -use crate::project; use crate::harness_runner; use crate::harness_runner::HarnessResult; +use crate::project; +use crate::KaniSession; use anyhow::Result; use tracing::debug; @@ -34,15 +34,15 @@ impl KaniSession { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; let target_dir = self - .args - .target_dir - .as_ref() - .unwrap_or(&metadata.target_directory.clone().into()) - .clone() - .join("kani"); - + .args + .target_dir + .as_ref() + .unwrap_or(&metadata.target_directory.clone().into()) + .clone() + .join("kani"); + let outdir = target_dir.join(build_target).join("cov"); - + if !outdir.exists() { fs::create_dir(&outdir)?; } diff --git a/kani-driver/src/coverage/mod.rs b/kani-driver/src/coverage/mod.rs index 8bac21cc742c..b03e6dfc8968 100644 --- a/kani-driver/src/coverage/mod.rs +++ b/kani-driver/src/coverage/mod.rs @@ -1,4 +1,4 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -pub mod coverage; pub mod cov_results; +pub mod coverage; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 71fa8ff8196a..56f3ed7d1ecf 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -11,7 +11,7 @@ use args_toml::join_args; use crate::args::StandaloneSubcommand; use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; -use crate::coverage::coverage::{coverage_cargo}; +use crate::coverage::coverage::coverage_cargo; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index ad0d61e539a2..4fb9b3a62f3a 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -74,7 +74,13 @@ pub fn build_lib(bin_folder: &Path) -> Result<()> { fn build_verification_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; - let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std", "-Cinstrument-coverage", "-Z", "no-profiler-runtime"]; + let compiler_args = [ + "--kani-compiler", + "-Cllvm-args=--ignore-global-asm --build-std", + "-Cinstrument-coverage", + "-Z", + "no-profiler-runtime", + ]; build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args) } From 3dfa074c9b4833a9552b8b4312b7e6a97e402844 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 20 Apr 2024 15:20:37 +0000 Subject: [PATCH 08/59] Fixes for toolchain upgrade sync --- .../src/codegen_cprover_gotoc/codegen/function.rs | 7 +------ kani-driver/src/args/mod.rs | 1 - kani-driver/src/call_cbmc.rs | 9 +++++---- kani-driver/src/cbmc_property_renderer.rs | 11 ++--------- 4 files changed, 8 insertions(+), 20 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 8fdf817ee94a..9bb5e22b9824 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -258,12 +258,7 @@ pub mod rustc_smir { } fn parse_coverage(coverage_opaque: Opaque) -> Option { - let coverage_clone = coverage_opaque.to_string(); - let coverage_str = { - let coverage_fmt = format!("{coverage_clone}"); - let cov_fmt_no_prefix = coverage_fmt.strip_prefix("Coverage { kind: ").unwrap(); - cov_fmt_no_prefix.strip_suffix(" }").unwrap().to_string() - }; + let coverage_str = coverage_opaque.to_string(); if coverage_str == "Zero" { return Some(CovTerm::Zero); } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 9d50927cbe64..f99bd31bc9b0 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -11,7 +11,6 @@ pub mod playback_args; pub use assess_args::*; use self::common::*; -use self::coverage_args::CargoCoverageArgs; use crate::args::cargo::CargoTargetArgs; use crate::util::warning; use cargo::CargoCommonArgs; diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index f777d8aa79fc..9ac561e0cc60 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -18,7 +18,7 @@ use crate::cbmc_output_parser::{ extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; -use crate::coverage::cov_results::{self, CoverageCheck, CoverageResults}; +use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; use crate::coverage::cov_results::{CoverageRegion, CoverageTerm}; use crate::session::KaniSession; @@ -315,7 +315,7 @@ impl VerificationResult { &self, output_format: &OutputFormat, should_panic: bool, - coverage_mode: bool, + _coverage_mode: bool, ) -> String { match &self.results { Ok(results) => { @@ -419,7 +419,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, + r#"^CounterIncrement\((?[0-9]+)\) \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -429,7 +429,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, + r#"^ExpressionUsed\((?[0-9]+)\) \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -478,6 +478,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option)>>; From 89dc04b52c6733b628a921d8e38771fa76f011fc Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 20 Apr 2024 15:48:51 +0000 Subject: [PATCH 09/59] Missing copyright --- kani-driver/src/coverage/cov_results.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 5cd594325d69..73767dd7d8d7 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -1,3 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + use crate::cbmc_output_parser::CheckStatus; use anyhow::Result; use serde::{Deserialize, Serialize}; From fe0ee147e154fdacbf0cd3fbb2becd027a4998b8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Apr 2024 20:33:23 +0000 Subject: [PATCH 10/59] Remove `cov` subcommand --- kani-driver/src/args/mod.rs | 4 ---- kani-driver/src/coverage/coverage.rs | 20 -------------------- kani-driver/src/main.rs | 8 ++++---- 3 files changed, 4 insertions(+), 28 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index f99bd31bc9b0..8332074cffcf 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -116,9 +116,6 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), - - /// TBD - Cov(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -493,7 +490,6 @@ impl ValidateArgs for CargoKaniSubcommand { match self { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), - CargoKaniSubcommand::Cov(_) => Ok(()), CargoKaniSubcommand::Playback(playback) => playback.validate(), } } diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index 56241cd9d9b3..5607356a0371 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -5,29 +5,9 @@ use std::fs; use std::fs::File; use std::io::Write; -use crate::args::coverage_args::CargoCoverageArgs; -use crate::harness_runner; use crate::harness_runner::HarnessResult; -use crate::project; use crate::KaniSession; use anyhow::Result; -use tracing::debug; - -pub fn coverage_cargo(mut session: KaniSession, _args: CargoCoverageArgs) -> Result<()> { - session.args.coverage = true; - let project = project::cargo_project(&session, false)?; - let harnesses = session.determine_targets(&project.get_all_harnesses())?; - debug!(n = harnesses.len(), ?harnesses, "coverage_cargo"); - - // Verification - let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; - let results = runner.check_all_harnesses(&harnesses)?; - - let _ = session.save_cov_results(&results); - - // More to come later - Ok(()) -} impl KaniSession { pub fn save_cov_results(&self, results: &Vec) -> Result<()> { diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 56f3ed7d1ecf..0af52b3a0bde 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -11,7 +11,6 @@ use args_toml::join_args; use crate::args::StandaloneSubcommand; use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; -use crate::coverage::coverage::coverage_cargo; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; @@ -80,9 +79,6 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } - Some(CargoKaniSubcommand::Cov(args)) => { - return coverage_cargo(session, *args); - } None => {} } @@ -123,6 +119,10 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; let results = runner.check_all_harnesses(&harnesses)?; + if session.args.coverage { + session.save_cov_results(&results)?; + } + session.print_final_summary(&results) } From 6fd483bb76d1e72736a3f164b4633e262d55f6f6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Apr 2024 20:39:06 +0000 Subject: [PATCH 11/59] Update unstable option for source coverage --- kani-driver/src/args/mod.rs | 4 ++-- kani_metadata/src/unstable.rs | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 8332074cffcf..d53a3f0a5714 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -636,12 +636,12 @@ impl ValidateArgs for VerificationArgs { } if self.coverage - && !self.common_args.unstable_features.contains(UnstableFeature::LineCoverage) + && !self.common_args.unstable_features.contains(UnstableFeature::SourceCoverage) { return Err(Error::raw( ErrorKind::MissingRequiredArgument, "The `--coverage` argument is unstable and requires `-Z \ - line-coverage` to be used.", + source-coverage` to be used.", )); } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 878b468dbdc3..4470b3101401 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -78,8 +78,9 @@ pub enum UnstableFeature { ConcretePlayback, /// Enable Kani's unstable async library. AsyncLib, - /// Enable line coverage instrumentation/reports. - LineCoverage, + /// Enable source-based code coverage workflow. + /// See [RFC-0008](https://model-checking.github.io/kani/rfc/rfcs/0008-source-coverage.html) + SourceCoverage, /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) FunctionContracts, /// Memory predicate APIs. From 12216ec9e81016a947c386d6b2d4c90e8886197e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Apr 2024 21:05:44 +0000 Subject: [PATCH 12/59] fixes for `clippy` --- .../src/codegen_cprover_gotoc/codegen/function.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 9bb5e22b9824..778d1fb89bfc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -238,8 +238,8 @@ pub mod rustc_smir { } /// Function that should be the internal implementation of opaque - pub fn coverage_span<'tcx>( - tcx: TyCtxt<'tcx>, + pub fn coverage_span( + tcx: TyCtxt<'_>, coverage: CovTerm, instance: Instance, ) -> Option { @@ -260,13 +260,13 @@ pub mod rustc_smir { fn parse_coverage(coverage_opaque: Opaque) -> Option { let coverage_str = coverage_opaque.to_string(); if coverage_str == "Zero" { - return Some(CovTerm::Zero); + Some(CovTerm::Zero) } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { - let (num_str, _rest) = rest.split_once(")").unwrap(); + let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); Some(CovTerm::Counter(num.into())) } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { - let (num_str, _rest) = rest.split_once(")").unwrap(); + let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); Some(CovTerm::Expression(num.into())) } else { From e010665741f2a89a6e1169decc99f7f41cb24162 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Apr 2024 21:06:03 +0000 Subject: [PATCH 13/59] Use square brackets to match on func. name --- kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/call_cbmc.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index cc3cbbcefb85..18ab3341d54e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -115,7 +115,7 @@ impl<'tcx> GotocCtx<'tcx> { let fun = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let cov_info = format!("{cov:?} ({fun})"); + let cov_info = format!("{cov:?} [{fun}]"); // NOTE: This helps see the coverage info we're processing // println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 9ac561e0cc60..956b646848dc 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -419,7 +419,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^CounterIncrement\((?[0-9]+)\) \((?[^)]+)\) - (?.+)"#, + r#"^CounterIncrement\((?[0-9]+)\) \[(?[^\]]+)\] - (?.+)"#, ) .unwrap() }) @@ -429,7 +429,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^ExpressionUsed\((?[0-9]+)\) \((?[^)]+)\) - (?.+)"#, + r#"^ExpressionUsed\((?[0-9]+)\) \[(?[^\]]+)\] - (?.+)"#, ) .unwrap() }) From d512c4bc3ffe78172b433cae37122f395adc34ac Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Apr 2024 21:25:06 +0000 Subject: [PATCH 14/59] Use curly brackets instead --- kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/call_cbmc.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 18ab3341d54e..c3e46da09175 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -115,7 +115,7 @@ impl<'tcx> GotocCtx<'tcx> { let fun = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let cov_info = format!("{cov:?} [{fun}]"); + let cov_info = format!("{cov:?} {{{fun}}}"); // NOTE: This helps see the coverage info we're processing // println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 956b646848dc..f114d01bc9e8 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -419,7 +419,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^CounterIncrement\((?[0-9]+)\) \[(?[^\]]+)\] - (?.+)"#, + r#"^CounterIncrement\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, ) .unwrap() }) @@ -429,7 +429,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^ExpressionUsed\((?[0-9]+)\) \[(?[^\]]+)\] - (?.+)"#, + r#"^ExpressionUsed\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, ) .unwrap() }) From c68c7ed2ed61887e9aa784d4e0c57ef9a6a9c6d6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 30 Jul 2024 15:46:46 +0000 Subject: [PATCH 15/59] Fix issues related to toolchain update --- .../src/codegen_cprover_gotoc/codegen/function.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 8deded172dd5..47bc6f7cdfc6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -244,12 +244,15 @@ pub mod rustc_smir { instance: Instance, ) -> Option { let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); - let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); + // let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); + let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); // NOTE: This helps see coverage mappings a given function // println!("COVERAGE: {:?}", &cov_info.mappings); + use rustc_middle::mir::coverage::MappingKind::Code; for mapping in &cov_info.mappings { - if mapping.kind.terms().next().unwrap() == coverage { + let Code(term) = mapping.kind else { todo!() }; + if term == coverage { println!("COVERAGE: {:?}", mapping.code_region.clone()); return Some(mapping.code_region.clone()); } From 77d53c2a8a816c4edebfdcbc2a7a2ee16a8ba343 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 20:31:41 +0000 Subject: [PATCH 16/59] Save timestamped coverage metadata and results --- Cargo.lock | 143 +++++++++++++++++++++++++++ kani-driver/Cargo.toml | 1 + kani-driver/src/coverage/coverage.rs | 62 +++++++++++- kani-driver/src/main.rs | 5 +- 4 files changed, 206 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 01dbccdd546a..3801688a15ec 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -23,6 +23,21 @@ dependencies = [ "memchr", ] +[[package]] +name = "android-tzdata" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e999941b234f3131b00bc13c22d06e8c5ff726d1b6318ac7eb276997bbb4fef0" + +[[package]] +name = "android_system_properties" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311" +dependencies = [ + "libc", +] + [[package]] name = "anstream" version = "0.6.15" @@ -100,6 +115,12 @@ dependencies = [ "which", ] +[[package]] +name = "bumpalo" +version = "3.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" + [[package]] name = "camino" version = "1.1.7" @@ -132,12 +153,32 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9e8aabfac534be767c909e0690571677d49f41bd8465ae876fe043d52ba5292" + [[package]] name = "cfg-if" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "chrono" +version = "0.4.38" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a21f936df1771bf62b77f047b726c4625ff2e8aa607c01ec06e5a05bd8463401" +dependencies = [ + "android-tzdata", + "iana-time-zone", + "js-sys", + "num-traits", + "wasm-bindgen", + "windows-targets", +] + [[package]] name = "clap" version = "4.5.11" @@ -226,6 +267,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "core-foundation-sys" +version = "0.8.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" + [[package]] name = "cprover_bindings" version = "0.53.0" @@ -372,6 +419,29 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "iana-time-zone" +version = "0.1.60" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7ffbb5a1b541ea2561f8c41c087286cc091e21e556a4f09a8f6cbf17b69b141" +dependencies = [ + "android_system_properties", + "core-foundation-sys", + "iana-time-zone-haiku", + "js-sys", + "wasm-bindgen", + "windows-core", +] + +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" +dependencies = [ + "cc", +] + [[package]] name = "indexmap" version = "2.2.6" @@ -403,6 +473,15 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" +[[package]] +name = "js-sys" +version = "0.3.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29c15563dc2726973df627357ce0c9ddddbea194836909d655df6a75d2cf296d" +dependencies = [ + "wasm-bindgen", +] + [[package]] name = "kani" version = "0.53.0" @@ -437,6 +516,7 @@ version = "0.53.0" dependencies = [ "anyhow", "cargo_metadata", + "chrono", "clap", "comfy-table", "console", @@ -1267,6 +1347,60 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +[[package]] +name = "wasm-bindgen" +version = "0.2.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4be2531df63900aeb2bca0daaaddec08491ee64ceecbee5076636a3b026795a8" +dependencies = [ + "cfg-if", + "wasm-bindgen-macro", +] + +[[package]] +name = "wasm-bindgen-backend" +version = "0.2.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "614d787b966d3989fa7bb98a654e369c762374fd3213d212cfc0251257e747da" +dependencies = [ + "bumpalo", + "log", + "once_cell", + "proc-macro2", + "quote", + "syn 2.0.72", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1f8823de937b71b9460c0c34e25f3da88250760bec0ebac694b49997550d726" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e94f17b526d0a461a191c78ea52bbce64071ed5c04c9ffe424dcb38f74171bb7" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.72", + "wasm-bindgen-backend", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af190c94f2773fdb3729c55b007a722abb5384da03bc0986df4c289bf5567e96" + [[package]] name = "which" version = "6.0.1" @@ -1310,6 +1444,15 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-core" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "33ab640c8d7e35bf8ba19b884ba838ceb4fba93a4e8c65a9059d08afcfc683d9" +dependencies = [ + "windows-targets", +] + [[package]] name = "windows-sys" version = "0.52.0" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index d58d686d7d43..0ec6493bbe35 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -15,6 +15,7 @@ publish = false kani_metadata = { path = "../kani_metadata" } cargo_metadata = "0.18.0" anyhow = "1" +chrono = "0.4.38" console = "0.15.1" once_cell = "1.19.0" serde = { version = "1", features = ["derive"] } diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index 5607356a0371..bc195cf0d35f 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -6,11 +6,20 @@ use std::fs::File; use std::io::Write; use crate::harness_runner::HarnessResult; +use crate::project::Project; use crate::KaniSession; -use anyhow::Result; +use anyhow::{bail, Result}; +use cargo_metadata::Package; +use chrono::Local; impl KaniSession { - pub fn save_cov_results(&self, results: &Vec) -> Result<()> { + /// Saves metadata required for coverage-related features. + /// At present, this metadata consists of the following: + /// - The file names of the project's source code. + /// + /// Note: Currently, coverage mappings are not included due to technical + /// limitations. But this is where we should save them. + pub fn save_coverage_metadata(&self, project: &Project, stamp: &String) -> Result<()> { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -21,15 +30,60 @@ impl KaniSession { .clone() .join("kani"); - let outdir = target_dir.join(build_target).join("cov"); + let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}")); + // Generally we don't expect this directory to exist, but there's no + // reason to delete it if it does. if !outdir.exists() { fs::create_dir(&outdir)?; } + // Collect paths to source files in the project + let mut source_targets = Vec::new(); + if let Some(metadata) = &project.cargo_metadata { + for package in &metadata.packages { + for target in &package.targets { + source_targets.push(target.src_path.clone()); + } + } + } else { + bail!("could not find project metadata required for coverage metadata"); + } + + let kanimap_name = format!("kanicov_{stamp}_kanimap"); + let file_name = outdir.join(kanimap_name).with_extension("json"); + let mut kanimap_file = File::create(file_name)?; + + let serialized_data = serde_json::to_string(&source_targets)?; + kanimap_file.write_all(serialized_data.as_bytes())?; + + Ok(()) + } + + /// Saves raw coverage check results required for coverage-related features. + pub fn save_coverage_results(&self, results: &Vec, stamp: &String) -> Result<()> { + let build_target = env!("TARGET"); + let metadata = self.cargo_metadata(build_target)?; + let target_dir = self + .args + .target_dir + .as_ref() + .unwrap_or(&metadata.target_directory.clone().into()) + .clone() + .join("kani"); + + let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}")); + + // This directory should have been created by `save_coverage_metadata`, + // so now we expect it to exist. + if !outdir.exists() { + bail!("directory associated to coverage run does not exist") + } + for harness_res in results { let harness_name = harness_res.harness.mangled_name.clone(); - let file_name = outdir.join(harness_name).with_extension("kanicov"); + let kaniraw_name = format!("{harness_name}_kaniraw"); + let file_name = outdir.join(kaniraw_name).with_extension("json"); let mut cov_file = File::create(file_name)?; let cov_results = &harness_res.result.coverage_results.clone().unwrap(); diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 41504315bf47..489bb0b3535b 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -5,6 +5,7 @@ use std::ffi::OsString; use std::process::ExitCode; use anyhow::Result; +use chrono::Local; use args::{check_is_valid, CargoKaniSubcommand}; use args_toml::join_args; @@ -131,7 +132,9 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let results = runner.check_all_harnesses(&harnesses)?; if session.args.coverage { - session.save_cov_results(&results)?; + let timestamp = Local::now().format("%Y-%m-%d_%H-%M").to_string(); + session.save_coverage_metadata(&project, ×tamp)?; + session.save_coverage_results(&results, ×tamp)?; } session.print_final_summary(&results) From d9ad862ffdfeff749fca23062e5482ed719d6403 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 20:33:32 +0000 Subject: [PATCH 17/59] Followup fix warnings and format --- .../src/codegen_cprover_gotoc/codegen/function.rs | 2 +- kani-driver/src/coverage/coverage.rs | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 47bc6f7cdfc6..f505a65f7206 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -248,7 +248,7 @@ pub mod rustc_smir { let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); // NOTE: This helps see coverage mappings a given function - // println!("COVERAGE: {:?}", &cov_info.mappings); + println!("MAPPINGS: {:?}", &cov_info.mappings); use rustc_middle::mir::coverage::MappingKind::Code; for mapping in &cov_info.mappings { let Code(term) = mapping.kind else { todo!() }; diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index bc195cf0d35f..4a8b44bc147b 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -9,8 +9,6 @@ use crate::harness_runner::HarnessResult; use crate::project::Project; use crate::KaniSession; use anyhow::{bail, Result}; -use cargo_metadata::Package; -use chrono::Local; impl KaniSession { /// Saves metadata required for coverage-related features. @@ -61,7 +59,11 @@ impl KaniSession { } /// Saves raw coverage check results required for coverage-related features. - pub fn save_coverage_results(&self, results: &Vec, stamp: &String) -> Result<()> { + pub fn save_coverage_results( + &self, + results: &Vec, + stamp: &String, + ) -> Result<()> { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -72,7 +74,7 @@ impl KaniSession { .clone() .join("kani"); - let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}")); + let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}")); // This directory should have been created by `save_coverage_metadata`, // so now we expect it to exist. From 655ee690e91a78fda32c41ae422e207e54b57224 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 20:48:08 +0000 Subject: [PATCH 18/59] Comment out debugging statements --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index f505a65f7206..0ba8c64c4bb4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -244,16 +244,14 @@ pub mod rustc_smir { instance: Instance, ) -> Option { let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); - // let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); - // NOTE: This helps see coverage mappings a given function - println!("MAPPINGS: {:?}", &cov_info.mappings); + // println!("MAPPINGS: {:?}", &cov_info.mappings); use rustc_middle::mir::coverage::MappingKind::Code; for mapping in &cov_info.mappings { let Code(term) = mapping.kind else { todo!() }; if term == coverage { - println!("COVERAGE: {:?}", mapping.code_region.clone()); + // println!("COVERAGE: {:?}", mapping.code_region.clone()); return Some(mapping.code_region.clone()); } } From ecf1f7e126583d51bfeb68be6f738b98443b8bbb Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 20:48:22 +0000 Subject: [PATCH 19/59] Do not instrument stdlib --- tools/build-kani/src/sysroot.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 5f1b574ea613..ca42fea3f441 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -85,13 +85,7 @@ pub fn build_lib(bin_folder: &Path) -> Result<()> { fn build_verification_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; - let compiler_args = [ - "--kani-compiler", - "-Cllvm-args=--ignore-global-asm --build-std", - "-Cinstrument-coverage", - "-Z", - "no-profiler-runtime", - ]; + let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std"]; let packages = ["std", "kani", "kani_macros"]; let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &compiler_args)?; copy_artifacts(&artifacts, &kani_sysroot_lib(), true) From e086ef11d559e8930b61fc193d38d5fe7f7c022f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 21:22:44 +0000 Subject: [PATCH 20/59] Better names in `codegen_coverage` --- kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 63cc3fd54a21..4683784a7909 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -149,14 +149,14 @@ impl<'tcx> GotocCtx<'tcx> { } /// Generate a cover statement for code coverage reports. - pub fn codegen_coverage(&self, info: &str, span: SpanStable, code_region: CodeRegion) -> Stmt { + pub fn codegen_coverage(&self, counter_data: &str, span: SpanStable, code_region: CodeRegion) -> Stmt { let loc = self.codegen_caller_span_stable(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)`. - let fmt = format!("{info} - {code_region:?}"); - self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &fmt, loc) + let msg = format!("{counter_data} - {code_region:?}"); + self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc) } // The above represent the basic operations we can perform w.r.t. assert/assume/cover From a8d5c8f7c897a8df3c052dc55db37e8d7e88346f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 21:24:19 +0000 Subject: [PATCH 21/59] Update RFC number --- kani_metadata/src/unstable.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 6ecb6cc0114f..b28032903fa6 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -79,7 +79,7 @@ pub enum UnstableFeature { /// Enable Kani's unstable async library. AsyncLib, /// Enable source-based code coverage workflow. - /// See [RFC-0008](https://model-checking.github.io/kani/rfc/rfcs/0008-source-coverage.html) + /// See [RFC-0011](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html) SourceCoverage, /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) FunctionContracts, From 0b5faa5ebe1efb1d48b5eaf51a28f0a79a44e755 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Aug 2024 21:41:37 +0000 Subject: [PATCH 22/59] Add placeholder to show coverage summary --- kani-driver/src/harness_runner.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 992e226e45db..f3b77fb9b231 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -192,6 +192,10 @@ impl KaniSession { } } + if self.args.coverage { + self.show_coverage_summary()?; + } + if failing > 0 { // Failure exit code without additional error message drop(self); @@ -200,4 +204,11 @@ impl KaniSession { Ok(()) } + + /// Show a coverage summary. + /// + /// This is just a placeholder for now. + fn show_coverage_summary(&self) -> Result<()> { + Ok(()) + } } From 0229a40ae37ff3dca449adbbcc0190ee6c222033 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 13 Aug 2024 20:10:25 +0000 Subject: [PATCH 23/59] Cleanup and document coverage-related compiler APIs --- .../codegen_cprover_gotoc/codegen/function.rs | 28 +++++++++++-------- .../codegen/statement.rs | 19 +++++-------- 2 files changed, 23 insertions(+), 24 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 0ba8c64c4bb4..b1526f12b807 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -224,41 +224,45 @@ pub mod rustc_smir { use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::Opaque; + use rustc_middle::mir::coverage::MappingKind::Code; type CoverageOpaque = stable_mir::Opaque; - /// Wrapper since we don't have a structured coverage. - pub fn coverage_opaque_span( + /// Retrieves the `CodeRegion` associated with the data in a + /// `CoverageOpaque` object. + pub fn region_from_coverage_opaque( tcx: TyCtxt, - coverage_opaque: CoverageOpaque, + coverage_opaque: &CoverageOpaque, instance: Instance, ) -> Option { - let cov_term = parse_coverage(coverage_opaque)?; - coverage_span(tcx, cov_term, instance) + let cov_term = parse_coverage_opaque(coverage_opaque)?; + region_from_coverage(tcx, cov_term, instance) } - /// Function that should be the internal implementation of opaque - pub fn coverage_span( + /// Retrieves the `CodeRegion` associated with a `CovTerm` object. + /// + /// Note: This function could be in the internal `rustc` impl for `Coverage`. + pub fn region_from_coverage( tcx: TyCtxt<'_>, coverage: CovTerm, instance: Instance, ) -> Option { + // We need to pull the coverage info from the internal MIR instance. let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); - // println!("MAPPINGS: {:?}", &cov_info.mappings); - use rustc_middle::mir::coverage::MappingKind::Code; + + // Iterate over the coverage mappings and match with the coverage term. for mapping in &cov_info.mappings { - let Code(term) = mapping.kind else { todo!() }; + let Code(term) = mapping.kind else { unreachable!() }; if term == coverage { - // println!("COVERAGE: {:?}", mapping.code_region.clone()); return Some(mapping.code_region.clone()); } } None } - fn parse_coverage(coverage_opaque: Opaque) -> Option { + fn parse_coverage_opaque(coverage_opaque: &Opaque) -> Option { let coverage_str = coverage_opaque.to_string(); if coverage_str == "Zero" { Some(CovTerm::Zero) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e5784ff119ad..520ebf190b5f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -3,7 +3,7 @@ use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; use super::{bb_label, PropertyClass}; -use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::coverage_opaque_span; +use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; @@ -159,18 +159,13 @@ impl<'tcx> GotocCtx<'tcx> { location, ) } - StatementKind::Coverage(cov) => { - // debug!(?opaque, "StatementKind::Coverage Opaque"); - // self.codegen_coverage(stmt.span) - - let fun = self.current_fn().readable_name(); + StatementKind::Coverage(coverage_opaque) => { + let function_name = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let cov_info = format!("{cov:?} {{{fun}}}"); - // NOTE: This helps see the coverage info we're processing - // println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); - let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); - if let Some(code_region) = cov_span { - let coverage_stmt = self.codegen_coverage(&cov_info, stmt.span, code_region); + let counter_data = format!("{coverage_opaque:?} {{{function_name}}}"); + let maybe_code_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); + if let Some(code_region) = maybe_code_region { + let coverage_stmt = self.codegen_coverage(&counter_data, stmt.span, code_region); // TODO: Avoid single-statement blocks when conversion of // standalone statements to the irep format is fixed. // More details in From e4dda7afec141eac9e015c1079de701f6b016726 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 13 Aug 2024 21:01:59 +0000 Subject: [PATCH 24/59] Improve coverage checks postprocessing --- kani-driver/src/call_cbmc.rs | 48 ++++++++++-------------------------- 1 file changed, 13 insertions(+), 35 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index e619413f6c2e..d36a901a05d9 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -432,57 +432,34 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); - RE.get_or_init(|| { + let counter_re = { + static COUNTER_RE: OnceLock = OnceLock::new(); + COUNTER_RE.get_or_init(|| { Regex::new( - r#"^CounterIncrement\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, + r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, ) .unwrap() }) }; - let re2 = { - static RE: OnceLock = OnceLock::new(); - RE.get_or_init(|| { - Regex::new( - r#"^ExpressionUsed\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, - ) - .unwrap() - }) - }; let mut coverage_results: BTreeMap> = BTreeMap::default(); for prop in cov_properties { let mut prop_processed = false; - if let Some(captures) = re.captures(&prop.description) { - let function = demangle(&captures["func_name"]).to_string(); + if let Some(captures) = counter_re.captures(&prop.description) { + let kind = &captures["kind"]; let counter_num = &captures["counter_num"]; - let status = prop.status; - let span = captures["span"].to_string(); - - let term = CoverageTerm::Counter(counter_num.parse().unwrap()); - let region = CoverageRegion::from_str(span); - - let cov_check = CoverageCheck::new(function, term, region, status); - let file = cov_check.region.file.clone(); - - if coverage_results.contains_key(&file) { - coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); - } else { - coverage_results.insert(file, vec![cov_check]); - } - prop_processed = true; - } - - if let Some(captures) = re2.captures(&prop.description) { let function = demangle(&captures["func_name"]).to_string(); - let expr_num = &captures["expr_num"]; let status = prop.status; let span = captures["span"].to_string(); - let term = CoverageTerm::Expression(expr_num.parse().unwrap()); + let counter_id = counter_num.parse().unwrap(); + let term = match kind { + "CounterIncrement" => CoverageTerm::Counter(counter_id), + "ExpressionUsed" => CoverageTerm::Expression(counter_id), + _ => unreachable!("counter kind could not be recognized: {:?} / {:?}", kind, prop.description), + }; let region = CoverageRegion::from_str(span); let cov_check = CoverageCheck::new(function, term, region, status); @@ -495,6 +472,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Date: Tue, 13 Aug 2024 22:18:28 +0000 Subject: [PATCH 25/59] Implement `Display` for `CoverageResults` and use --- kani-driver/src/call_cbmc.rs | 2 +- kani-driver/src/cbmc_property_renderer.rs | 13 ++--- kani-driver/src/coverage/cov_results.rs | 59 ++++++++++++----------- 3 files changed, 34 insertions(+), 40 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index d36a901a05d9..2fdc9711d211 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -60,7 +60,7 @@ pub struct VerificationResult { pub runtime: Duration, /// Whether concrete playback generated a test pub generated_concrete_test: bool, - /// The coverage results? + /// The coverage results pub coverage_results: Option, } diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index cd43618746d7..b3c40b0303a2 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -4,7 +4,7 @@ use crate::args::OutputFormat; use crate::call_cbmc::{FailedProperties, VerificationStatus}; use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem}; -use crate::coverage::cov_results::{fmt_coverage_results, CoverageResults}; +use crate::coverage::cov_results::CoverageResults; use console::style; use once_cell::sync::Lazy; use regex::Regex; @@ -437,19 +437,12 @@ pub fn format_coverage( let verification_output = format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks); - let new_coverage_output = format_result_new_coverage(cov_results); - let result = format!("{}\n{}", verification_output, new_coverage_output); + let cov_results_intro = "Source-based code coverage results:"; + let result = format!("{}\n{}\n\n{}", verification_output, cov_results_intro, cov_results); result } -fn format_result_new_coverage(cov_results: &CoverageResults) -> String { - let mut formatted_output = String::new(); - formatted_output.push_str("\nCoverage Results (NEW):\n"); - - fmt_coverage_results(&cov_results).expect("error: couldn't format coverage results") -} - /// 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 { diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 73767dd7d8d7..9bfa2673d22d 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -2,11 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::cbmc_output_parser::CheckStatus; -use anyhow::Result; use serde::{Deserialize, Serialize}; -use std::fmt::{self, Write}; -use std::{collections::BTreeMap, fmt::Display}; +use std::{collections::BTreeMap, fmt, fmt::Display}; +/// The coverage data maps a function name to a set of coverage checks. #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CoverageResults { pub data: BTreeMap>, @@ -17,31 +16,33 @@ impl CoverageResults { Self { data } } } -pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { - let mut fmt_string = String::new(); - for (file, checks) in coverage_results.data.iter() { - let mut checks_by_function: BTreeMap> = BTreeMap::new(); - // // Group checks by function - for check in checks { - // Insert the check into the vector corresponding to its function - checks_by_function - .entry(check.function.clone()) - .or_insert_with(Vec::new) - .push(check.clone()); - } +impl fmt::Display for CoverageResults { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + for (file, checks) in self.data.iter() { + let mut checks_by_function: BTreeMap> = BTreeMap::new(); + + // Group checks by function + for check in checks { + // Insert the check into the vector corresponding to its function + checks_by_function + .entry(check.function.clone()) + .or_insert_with(Vec::new) + .push(check.clone()); + } - for (function, checks) in checks_by_function { - writeln!(fmt_string, "{file} ({function})")?; - let mut sorted_checks: Vec = checks.to_vec(); - sorted_checks.sort_by(|a, b| a.region.start.cmp(&b.region.start)); - for check in sorted_checks.iter() { - writeln!(fmt_string, " * {} {}", check.region, check.status)?; + for (function, checks) in checks_by_function { + writeln!(f, "{file} ({function})")?; + let mut sorted_checks: Vec = checks.to_vec(); + sorted_checks.sort_by(|a, b| a.region.start.cmp(&b.region.start)); + for check in sorted_checks.iter() { + writeln!(f, " * {} {}", check.region, check.status)?; + } + writeln!(f, "")?; } - writeln!(fmt_string, "")?; } + Ok(()) } - Ok(fmt_string) } #[derive(Debug, Clone, Serialize, Deserialize)] @@ -63,6 +64,12 @@ impl CoverageCheck { } } +#[derive(Debug, Clone, Serialize, Deserialize)] +pub enum CoverageTerm { + Counter(u32), + Expression(u32), +} + #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)] pub struct CoverageRegion { pub file: String, @@ -90,9 +97,3 @@ impl CoverageRegion { Self { file, start, end } } } - -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum CoverageTerm { - Counter(u32), - Expression(u32), -} From f79e07477ed76b72917fa3b780dc31d91df32f6e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 13 Aug 2024 22:21:27 +0000 Subject: [PATCH 26/59] Clarify comment in `format_coverage` --- kani-driver/src/cbmc_property_renderer.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index b3c40b0303a2..1cb674b98eb5 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -422,8 +422,12 @@ 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 +/// Separate checks into coverage and non-coverage based on property class and +/// format them separately for `--coverage``. Then we report both verification +/// and processed coverage results. +/// +/// Note: The reporting of coverage results should be removed once `kani-cov` is +/// introduced. pub fn format_coverage( properties: &[Property], cov_results: &CoverageResults, From c0008d58c9c536c0ac784bba7a2f69ef80e71de0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 14:05:41 +0000 Subject: [PATCH 27/59] Reformat --- kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs | 7 ++++++- .../src/codegen_cprover_gotoc/codegen/function.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/statement.rs | 6 ++++-- kani-driver/src/call_cbmc.rs | 2 +- 4 files changed, 12 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 4683784a7909..4ee81d0c7d3e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -149,7 +149,12 @@ impl<'tcx> GotocCtx<'tcx> { } /// Generate a cover statement for code coverage reports. - pub fn codegen_coverage(&self, counter_data: &str, span: SpanStable, code_region: CodeRegion) -> Stmt { + pub fn codegen_coverage( + &self, + counter_data: &str, + span: SpanStable, + code_region: CodeRegion, + ) -> Stmt { let loc = self.codegen_caller_span_stable(span); // Should use Stmt::cover, but currently this doesn't work with CBMC // unless it is run with '--cover cover' (see diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index b1526f12b807..726c21d9d4ef 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -221,10 +221,10 @@ pub mod rustc_smir { use crate::stable_mir::CrateDef; use rustc_middle::mir::coverage::CodeRegion; use rustc_middle::mir::coverage::CovTerm; + use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::Opaque; - use rustc_middle::mir::coverage::MappingKind::Code; type CoverageOpaque = stable_mir::Opaque; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 520ebf190b5f..881cce94df3b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -163,9 +163,11 @@ impl<'tcx> GotocCtx<'tcx> { let function_name = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); let counter_data = format!("{coverage_opaque:?} {{{function_name}}}"); - let maybe_code_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); + let maybe_code_region = + region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); if let Some(code_region) = maybe_code_region { - let coverage_stmt = self.codegen_coverage(&counter_data, stmt.span, code_region); + let coverage_stmt = + self.codegen_coverage(&counter_data, stmt.span, code_region); // TODO: Avoid single-statement blocks when conversion of // standalone statements to the irep format is fixed. // More details in diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 2fdc9711d211..a532991b920e 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -458,7 +458,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option CoverageTerm::Counter(counter_id), "ExpressionUsed" => CoverageTerm::Expression(counter_id), - _ => unreachable!("counter kind could not be recognized: {:?} / {:?}", kind, prop.description), + _ => unreachable!("counter kind could not be recognized: {:?}", kind), }; let region = CoverageRegion::from_str(span); From 9730d5f3b1e469450266cf378a3a3d24fe7db267 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 16:11:30 +0000 Subject: [PATCH 28/59] Deal with `clippy` issues --- kani-driver/src/call_cbmc.rs | 7 ++++--- kani-driver/src/coverage/cov_results.rs | 4 ++-- kani-driver/src/coverage/{coverage.rs => cov_session.rs} | 0 kani-driver/src/coverage/mod.rs | 3 ++- 4 files changed, 8 insertions(+), 6 deletions(-) rename kani-driver/src/coverage/{coverage.rs => cov_session.rs} (100%) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index a532991b920e..e2aecb4767ac 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -5,6 +5,7 @@ use anyhow::{bail, Result}; use kani_metadata::{CbmcSolver, HarnessMetadata}; use regex::Regex; use rustc_demangle::demangle; +use std::collections::btree_map::Entry; use std::collections::BTreeMap; use std::ffi::OsString; use std::fmt::Write; @@ -465,10 +466,10 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Date: Wed, 14 Aug 2024 16:14:43 +0000 Subject: [PATCH 29/59] Reformat --- kani-driver/src/coverage/cov_results.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 15cd3b60eb71..845ae7de21bb 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -25,10 +25,7 @@ impl fmt::Display for CoverageResults { // Group checks by function for check in checks { // Insert the check into the vector corresponding to its function - checks_by_function - .entry(check.function.clone()) - .or_default() - .push(check.clone()); + checks_by_function.entry(check.function.clone()).or_default().push(check.clone()); } for (function, checks) in checks_by_function { From dc37cfd96ffbeb94e1e2a3220adfdb9519b64dfb Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 20:32:31 +0000 Subject: [PATCH 30/59] Bless coverage tests with source coverage results --- .../coverage/reachable/assert-false/expected | 20 +++-- tests/coverage/reachable/assert-false/main.rs | 1 - .../reachable/assert/reachable_pass/expected | 4 - .../reachable/bounds/reachable_fail/expected | 11 ++- .../reachable/bounds/reachable_fail/test.rs | 6 +- .../div-zero/reachable_fail/expected | 11 ++- .../reachable/div-zero/reachable_fail/test.rs | 2 +- .../div-zero/reachable_pass/expected | 13 +++- .../reachable/div-zero/reachable_pass/test.rs | 2 +- .../overflow/reachable_fail/expected | 14 ++-- .../reachable/overflow/reachable_fail/test.rs | 4 +- .../overflow/reachable_pass/expected | 20 +++-- .../reachable/overflow/reachable_pass/test.rs | 4 +- .../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 | 20 +++-- tests/coverage/unreachable/assert/expected | 16 ++-- tests/coverage/unreachable/assert_eq/expected | 13 ++-- tests/coverage/unreachable/assert_ne/expected | 15 ++-- .../unreachable/assume_assert/expected | 8 +- .../unreachable/assume_assert/main.rs | 6 ++ tests/coverage/unreachable/bounds/expected | 13 +++- tests/coverage/unreachable/bounds/test.rs | 1 - tests/coverage/unreachable/break/expected | 22 +++--- tests/coverage/unreachable/break/main.rs | 2 +- tests/coverage/unreachable/check_id/expected | 27 +++---- tests/coverage/unreachable/compare/expected | 18 +++-- tests/coverage/unreachable/compare/main.rs | 2 +- .../unreachable/contradiction/expected | 16 ++-- .../unreachable/debug-assert/expected | 14 +++- .../coverage/unreachable/debug-assert/main.rs | 5 ++ tests/coverage/unreachable/divide/expected | 7 -- tests/coverage/unreachable/divide/main.rs | 19 ----- .../unreachable/early-return/expected | 22 +++--- .../unreachable/if-statement/expected | 24 +++--- .../coverage/unreachable/if-statement/main.rs | 4 +- .../unreachable/multiple-harnesses/expected | 74 +++++++++---------- tests/coverage/unreachable/return/expected | 8 -- tests/coverage/unreachable/return/main.rs | 17 ----- .../unreachable/tutorial_unreachable/expected | 11 +-- tests/coverage/unreachable/variant/expected | 24 +++--- tests/coverage/unreachable/variant/main.rs | 2 +- tests/coverage/unreachable/vectors/expected | 12 +-- .../unreachable/while-loop-break/expected | 24 +++--- tools/compiletest/src/runtest.rs | 2 +- 47 files changed, 290 insertions(+), 300 deletions(-) delete mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/expected delete mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/test.rs delete mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/expected delete mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/test.rs delete mode 100644 tests/coverage/unreachable/divide/expected delete mode 100644 tests/coverage/unreachable/divide/main.rs delete mode 100644 tests/coverage/unreachable/return/expected delete mode 100644 tests/coverage/unreachable/return/main.rs diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected index 97ffbe1d96e4..b6043db371b6 100644 --- a/tests/coverage/reachable/assert-false/expected +++ b/tests/coverage/reachable/assert-false/expected @@ -1,8 +1,12 @@ -coverage/reachable/assert-false/main.rs, 6, FULL -coverage/reachable/assert-false/main.rs, 7, FULL -coverage/reachable/assert-false/main.rs, 11, PARTIAL -coverage/reachable/assert-false/main.rs, 12, PARTIAL -coverage/reachable/assert-false/main.rs, 15, PARTIAL -coverage/reachable/assert-false/main.rs, 16, FULL -coverage/reachable/assert-false/main.rs, 17, PARTIAL -coverage/reachable/assert-false/main.rs, 19, FULL +Source-based code coverage results: + +main.rs (any_bool)\ + * 4:1 - 6:2 COVERED + +main.rs (main)\ + * 9:1 - 10:18 COVERED\ + * 10:19 - 12:6 COVERED\ + * 12:6 - 12:7 COVERED\ + * 15:13 - 16:32 COVERED\ + * 17:6 - 17:7 COVERED\ + * 18:1 - 18:2 COVERED diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs index 42563b1cd518..034cc5e1951b 100644 --- a/tests/coverage/reachable/assert-false/main.rs +++ b/tests/coverage/reachable/assert-false/main.rs @@ -1,7 +1,6 @@ // 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() } diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected index 9d21185b3a83..e69de29bb2d1 100644 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -1,4 +0,0 @@ -coverage/reachable/assert/reachable_pass/test.rs, 6, FULL -coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL -coverage/reachable/assert/reachable_pass/test.rs, 8, FULL -coverage/reachable/assert/reachable_pass/test.rs, 10, FULL diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected index fedfec8b2a1e..51d953241b62 100644 --- a/tests/coverage/reachable/bounds/reachable_fail/expected +++ b/tests/coverage/reachable/bounds/reachable_fail/expected @@ -1,4 +1,7 @@ -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, PARTIAL -coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE +Source-based code coverage results: + +test.rs (get) + * 4:1 - 6:2 COVERED + +test.rs (main) + * 9:1 - 11:2 COVERED diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs index cebd78b2d5d9..585c35eafd4f 100644 --- a/tests/coverage/reachable/bounds/reachable_fail/test.rs +++ b/tests/coverage/reachable/bounds/reachable_fail/test.rs @@ -2,10 +2,10 @@ // 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 + s[index] +} #[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 index c1ac77404680..fdabea0e8acc 100644 --- a/tests/coverage/reachable/div-zero/reachable_fail/expected +++ b/tests/coverage/reachable/div-zero/reachable_fail/expected @@ -1,4 +1,7 @@ -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, PARTIAL -coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE +Source-based code coverage results: + +test.rs (div)\ + * 4:1 - 6:2 COVERED + +tests/coverage/reachable/div-zero/reachable_fail/test.rs (main)\ + * 9:1 - 11:2 COVERED diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs index 5f69005ee712..91af9a4ca802 100644 --- a/tests/coverage/reachable/div-zero/reachable_fail/test.rs +++ b/tests/coverage/reachable/div-zero/reachable_fail/test.rs @@ -2,7 +2,7 @@ // 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` + x / y } #[kani::proof] diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected index c7bfb5961c0b..f351005f4f22 100644 --- a/tests/coverage/reachable/div-zero/reachable_pass/expected +++ b/tests/coverage/reachable/div-zero/reachable_pass/expected @@ -1,4 +1,9 @@ -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 +Source-based code coverage results: + +test.rs (div)\ + * 4:1 - 5:14 COVERED\ + * 5:17 - 5:22 COVERED\ + * 5:32 - 5:33 UNCOVERED + +test.rs (main)\ + * 9:1 - 11:2 COVERED diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/reachable/div-zero/reachable_pass/test.rs index 766fb5a89d88..e858b57a12be 100644 --- a/tests/coverage/reachable/div-zero/reachable_pass/test.rs +++ b/tests/coverage/reachable/div-zero/reachable_pass/test.rs @@ -2,7 +2,7 @@ // 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 + if y != 0 { x / y } else { 0 } } #[kani::proof] diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected index d45edcc37a63..db4f29d51336 100644 --- a/tests/coverage/reachable/overflow/reachable_fail/expected +++ b/tests/coverage/reachable/overflow/reachable_fail/expected @@ -1,5 +1,9 @@ -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, PARTIAL -coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE +Source-based code coverage results: + +test.rs (cond_reduce)\ + * 7:1 - 8:18 COVERED\ + * 8:21 - 8:27 COVERED\ + * 8:37 - 8:38 UNCOVERED + +test.rs (main)\ + * 12:1 - 15:2 COVERED diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/reachable/overflow/reachable_fail/test.rs index d435612f2342..cd711f3aeb9e 100644 --- a/tests/coverage/reachable/overflow/reachable_fail/test.rs +++ b/tests/coverage/reachable/overflow/reachable_fail/test.rs @@ -5,11 +5,11 @@ //! 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 + if x > thresh { x - 50 } else { x } } #[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 index 5becf2cd23e7..7e8197c66289 100644 --- a/tests/coverage/reachable/overflow/reachable_pass/expected +++ b/tests/coverage/reachable/overflow/reachable_pass/expected @@ -1,7 +1,13 @@ -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 +Source-based code coverage results: + +tests/coverage/reachable/overflow/reachable_pass/test.rs (main) + * 12:1 - 17:2 COVERED\ + +tests/coverage/reachable/overflow/reachable_pass/test.rs (reduce) + * 7:1 - 8:16 COVERED\ + * 8:19 - 8:27 COVERED\ + * 8:37 - 8:38 COVERED\ + +Verification Time: 0.052936167s + +error: could not find project metadata required for coverage metadata diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/reachable/overflow/reachable_pass/test.rs index 0b05874efc84..1c3467275b33 100644 --- a/tests/coverage/reachable/overflow/reachable_pass/test.rs +++ b/tests/coverage/reachable/overflow/reachable_pass/test.rs @@ -1,8 +1,8 @@ // 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. +//! Checks that Kani reports all regions as `COVERED` as expected in this case +//! where arithmetic overflow failures are prevented. fn reduce(x: u32) -> u32 { if x > 1000 { x - 1000 } else { x } diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected deleted file mode 100644 index 7852461e4f57..000000000000 --- a/tests/coverage/reachable/rem-zero/reachable_fail/expected +++ /dev/null @@ -1,4 +0,0 @@ -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, PARTIAL -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 deleted file mode 100644 index 400c7e02340b..000000000000 --- a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs +++ /dev/null @@ -1,11 +0,0 @@ -// 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 deleted file mode 100644 index f3d5934d785d..000000000000 --- a/tests/coverage/reachable/rem-zero/reachable_pass/expected +++ /dev/null @@ -1,4 +0,0 @@ -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 deleted file mode 100644 index 41ed28f7b903..000000000000 --- a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs +++ /dev/null @@ -1,11 +0,0 @@ -// 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 index 473b0f5a8d4d..91142ebf94fc 100644 --- a/tests/coverage/unreachable/abort/expected +++ b/tests/coverage/unreachable/abort/expected @@ -1,7 +1,13 @@ -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 +Source-based code coverage results: + +main.rs (main)\ + * 9:1 - 9:11 COVERED\ + * 10:9 - 10:10 COVERED\ + * 10:14 - 10:18 COVERED\ + * 13:13 - 13:29 COVERED\ + * 14:10 - 15:18 COVERED\ + * 17:13 - 17:29 UNCOVERED\ + * 18:10 - 18:11 COVERED\ + * 20:5 - 20:12 UNCOVERED\ + * 20:20 - 20:41 UNCOVERED\ + * 21:1 - 21:2 UNCOVERED diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected index 9bc6d8faa4f9..46bb664cf6f5 100644 --- a/tests/coverage/unreachable/assert/expected +++ b/tests/coverage/unreachable/assert/expected @@ -1,7 +1,9 @@ -coverage/unreachable/assert/test.rs, 6, FULL -coverage/unreachable/assert/test.rs, 7, PARTIAL -coverage/unreachable/assert/test.rs, 9, PARTIAL -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 +Source-based code coverage results: + +test.rs (foo) + * 5:1 - 7:13 COVERED\ + * 9:9 - 10:17 COVERED\ + * 10:18 - 13:10 UNCOVERED\ + * 13:10 - 13:11 UNCOVERED\ + * 14:12 - 17:6 COVERED\ + * 18:1 - 18:2 COVERED diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected index 9b13c3c96ded..c2eee7adf803 100644 --- a/tests/coverage/unreachable/assert_eq/expected +++ b/tests/coverage/unreachable/assert_eq/expected @@ -1,5 +1,8 @@ -coverage/unreachable/assert_eq/test.rs, 6, FULL -coverage/unreachable/assert_eq/test.rs, 7, FULL -coverage/unreachable/assert_eq/test.rs, 8, PARTIAL -coverage/unreachable/assert_eq/test.rs, 9, NONE -coverage/unreachable/assert_eq/test.rs, 11, FULL +Source-based code coverage results: + +test.rs (main)\ + * 5:1 - 6:29 COVERED\ + * 7:25 - 7:27 COVERED\ + * 7:37 - 7:39 COVERED\ + * 8:15 - 10:6 UNCOVERED\ + * 10:6 - 10:7 COVERED diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected index f027f432e280..c9b727da0f82 100644 --- a/tests/coverage/unreachable/assert_ne/expected +++ b/tests/coverage/unreachable/assert_ne/expected @@ -1,6 +1,9 @@ -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, PARTIAL -coverage/unreachable/assert_ne/test.rs, 11, NONE -coverage/unreachable/assert_ne/test.rs, 14, FULL +Source-based code coverage results: + +test.rs (main)\ + * 5:1 - 7:13 COVERED\ + * 8:13 - 10:18 COVERED\ + * 10:19 - 12:10 UNCOVERED\ + * 12:10 - 12:11 COVERED\ + * 13:6 - 13:7 COVERED\ + * 14:1 - 14:2 COVERED diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected index 8c1ae8a247d2..ef5487f9462f 100644 --- a/tests/coverage/unreachable/assume_assert/expected +++ b/tests/coverage/unreachable/assume_assert/expected @@ -1,4 +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 +Source-based code coverage results: + +main.rs (check_assume_assert)\ + * 4:1 - 8:2 COVERED diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs index c4d5d65c6640..1eb5a08198b1 100644 --- a/tests/coverage/unreachable/assume_assert/main.rs +++ b/tests/coverage/unreachable/assume_assert/main.rs @@ -1,5 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test should check that the region after `kani::assume(false)` is +//! `UNCOVERED`. However, due to a technical limitation in `rustc`'s coverage +//! instrumentation, only one `COVERED` region is reported for the whole +//! function. +//! TODO: Create issue and paste here. #[kani::proof] fn check_assume_assert() { let a: u8 = kani::any(); diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected index 610372000a01..fc9f57841169 100644 --- a/tests/coverage/unreachable/bounds/expected +++ b/tests/coverage/unreachable/bounds/expected @@ -1,4 +1,9 @@ -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 +Source-based code coverage results: + +test.rs (get)\ + * 4:1 - 5:23 COVERED\ + * 5:26 - 5:34 UNCOVERED\ + * 5:44 - 5:46 COVERED + +test.rs (main)\ + * 9:1 - 12:2 COVERED diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs index c37c9d0dcad6..9ef6573b2a52 100644 --- a/tests/coverage/unreachable/bounds/test.rs +++ b/tests/coverage/unreachable/bounds/test.rs @@ -7,6 +7,5 @@ fn get(s: &[i16], index: usize) -> i16 { #[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 index dcb013c50c3d..739735cdf1a2 100644 --- a/tests/coverage/unreachable/break/expected +++ b/tests/coverage/unreachable/break/expected @@ -1,9 +1,13 @@ -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 +Source-based code coverage results: + +main.rs (find_positive)\ + * 4:1 - 4:47 COVERED\ + * 5:10 - 5:13 COVERED\ + * 5:17 - 5:21 COVERED\ + * 7:20 - 7:29 COVERED\ + * 8:10 - 8:11 COVERED\ + * 11:5 - 11:9 UNCOVERED\ + * 12:1 - 12:2 COVERED + +main.rs (main)\ + * 15:1 - 19:2 COVERED diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/unreachable/break/main.rs index 4e795bd2a6ea..79f422a0c283 100644 --- a/tests/coverage/unreachable/break/main.rs +++ b/tests/coverage/unreachable/break/main.rs @@ -7,7 +7,7 @@ fn find_positive(nums: &[i32]) -> Option { return Some(num); } } - // This part is unreachable if there is at least one positive number. + // `None` is unreachable because there is at least one positive number. None } diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected index a2d296f0f9a3..2506c6cfa2f6 100644 --- a/tests/coverage/unreachable/check_id/expected +++ b/tests/coverage/unreachable/check_id/expected @@ -1,16 +1,11 @@ -coverage/unreachable/check_id/main.rs, 5, FULL -coverage/unreachable/check_id/main.rs, 6, PARTIAL -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, PARTIAL -coverage/unreachable/check_id/main.rs, 25, NONE +Source-based code coverage results: + +main.rs (foo)\ + * 4:1 - 6:13 COVERED\ + * 6:14 - 9:6 UNCOVERED\ + * 9:6 - 9:7 COVERED + +main.rs (main)\ + * 13:1 - 14:24 COVERED\ + * 15:30 - 15:32 COVERED\ + * 15:42 - 15:44 COVERED diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/unreachable/compare/expected index 6187e232cbe7..153dbfa37d80 100644 --- a/tests/coverage/unreachable/compare/expected +++ b/tests/coverage/unreachable/compare/expected @@ -1,7 +1,11 @@ -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 +Source-based code coverage results: + +main.rs (compare)\ + * 4:1 - 6:14 COVERED\ + * 6:17 - 6:18 COVERED\ + * 6:28 - 6:29 UNCOVERED + +main.rs (main)\ + * 10:1 - 13:14 COVERED\ + * 13:15 - 15:6 COVERED\ + * 15:6 - 15:7 COVERED diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/unreachable/compare/main.rs index a10fb84e29a8..43318ac0547e 100644 --- a/tests/coverage/unreachable/compare/main.rs +++ b/tests/coverage/unreachable/compare/main.rs @@ -2,7 +2,7 @@ // 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 + // The case where `x < y` isn't possible so its region is `UNCOVERED` if x >= y { 1 } else { 0 } } diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected index 4234fc328e1e..db3676d7da15 100644 --- a/tests/coverage/unreachable/contradiction/expected +++ b/tests/coverage/unreachable/contradiction/expected @@ -1,7 +1,9 @@ -coverage/unreachable/contradiction/main.rs, 5, FULL -coverage/unreachable/contradiction/main.rs, 6, FULL -coverage/unreachable/contradiction/main.rs, 7, FULL -coverage/unreachable/contradiction/main.rs, 8, PARTIAL -coverage/unreachable/contradiction/main.rs, 9, NONE -coverage/unreachable/contradiction/main.rs, 12, FULL -coverage/unreachable/contradiction/main.rs, 14, FULL +Source-based code coverage results: + +main.rs (contradiction)\ + * 4:1 - 7:13 COVERED\ + * 8:12 - 8:17 COVERED\ + * 8:18 - 10:10 UNCOVERED\ + * 10:10 - 10:11 COVERED\ + * 11:12 - 13:6 COVERED\ + * 14:1 - 14:2 COVERED diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected index 25fdfed4c863..7b6a322ca040 100644 --- a/tests/coverage/unreachable/debug-assert/expected +++ b/tests/coverage/unreachable/debug-assert/expected @@ -1,4 +1,10 @@ -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 +Source-based code coverage results: + +tests/coverage/unreachable/debug-assert/main.rs (main) + * 5:1 - 5:11 COVERED\ + * 6:9 - 6:10 COVERED\ + * 6:14 - 6:18 COVERED\ + * 7:30 - 7:71 UNCOVERED\ + * 8:9 - 8:23 UNCOVERED\ + * 8:25 - 8:53 UNCOVERED\ + * 10:1 - 10:2 UNCOVERED diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs index ab3ab41e47d0..a57a45c8c724 100644 --- a/tests/coverage/unreachable/debug-assert/main.rs +++ b/tests/coverage/unreachable/debug-assert/main.rs @@ -1,6 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! This test checks that the regions after the `debug_assert` macro are +//! `UNCOVERED`. In fact, for this example, the region associated to `"This +//! should fail and stop the execution"` is also `UNCOVERED` because the macro +//! calls span two regions each. + #[kani::proof] fn main() { for i in 0..4 { diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected deleted file mode 100644 index 63081358941a..000000000000 --- a/tests/coverage/unreachable/divide/expected +++ /dev/null @@ -1,7 +0,0 @@ -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 deleted file mode 100644 index ba6afab83135..000000000000 --- a/tests/coverage/unreachable/divide/main.rs +++ /dev/null @@ -1,19 +0,0 @@ -// 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 index 466c1775408b..53cde3abeaf8 100644 --- a/tests/coverage/unreachable/early-return/expected +++ b/tests/coverage/unreachable/early-return/expected @@ -1,10 +1,12 @@ -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 +Source-based code coverage results: + +main.rs (find_index)\ + * 4:1 - 4:59 COVERED\ + * 5:10 - 5:21 COVERED\ + * 7:20 - 7:31 COVERED\ + * 8:10 - 8:11 COVERED\ + * 10:5 - 10:9 UNCOVERED\ + * 11:1 - 11:2 COVERED + +main.rs (main)\ + * 14:1 - 19:2 COVERED diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected index 8b481863a163..b85b95de9c84 100644 --- a/tests/coverage/unreachable/if-statement/expected +++ b/tests/coverage/unreachable/if-statement/expected @@ -1,10 +1,14 @@ -coverage/unreachable/if-statement/main.rs, 5, PARTIAL -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 +Source-based code coverage results: + +main.rs (check_number)\ + * 4:1 - 5:15 COVERED\ + * 7:12 - 7:24 COVERED\ + * 7:27 - 7:46 UNCOVERED\ + * 7:56 - 7:74 COVERED\ + * 8:15 - 8:22 UNCOVERED\ + * 9:9 - 9:19 UNCOVERED\ + * 11:9 - 11:15 UNCOVERED\ + * 13:1 - 13:2 COVERED + +main.rs (main)\ + * 16:1 - 20:2 COVERED diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/unreachable/if-statement/main.rs index f497cd76808e..030fd3bd29b4 100644 --- a/tests/coverage/unreachable/if-statement/main.rs +++ b/tests/coverage/unreachable/if-statement/main.rs @@ -3,9 +3,9 @@ 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 + // The next line is partially covered if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" } - } else if num < 0 { + } else if num < 0 { // From here on, only the terminator is covered "Negative" } else { "Zero" diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected index 17a52666c08d..b5362147fed1 100644 --- a/tests/coverage/unreachable/multiple-harnesses/expected +++ b/tests/coverage/unreachable/multiple-harnesses/expected @@ -1,39 +1,37 @@ -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 +Source-based code coverage results: -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 +main.rs (estimate_size)\ + * 4:1 - 7:15 COVERED\ + * 8:12 - 8:19 COVERED\ + * 9:20 - 9:21 COVERED\ + * 11:20 - 11:21 COVERED\ + * 13:15 - 13:23 COVERED\ + * 14:12 - 14:20 COVERED\ + * 15:20 - 15:21 COVERED\ + * 17:20 - 17:21 COVERED\ + * 20:12 - 20:20 COVERED\ + * 21:20 - 21:21 COVERED\ + * 23:20 - 23:21 COVERED\ + * 26:1 - 26:2 COVERED + +main.rs (fully_covered)\ + * 39:1 - 44:2 COVERED + +Source-based code coverage results: + +main.rs (estimate_size)\ + * 4:1 - 7:15 COVERED\ + * 8:12 - 8:19 COVERED\ + * 9:20 - 9:21 COVERED\ + * 11:20 - 11:21 COVERED\ + * 13:15 - 13:23 COVERED\ + * 14:12 - 14:20 COVERED\ + * 15:20 - 15:21 COVERED\ + * 17:20 - 17:21 COVERED\ + * 20:12 - 20:20 COVERED\ + * 21:20 - 21:21 COVERED\ + * 23:20 - 23:21 UNCOVERED\ + * 26:1 - 26:2 COVERED + +main.rs (mostly_covered)\ + * 30:1 - 35:2 COVERED diff --git a/tests/coverage/unreachable/return/expected b/tests/coverage/unreachable/return/expected deleted file mode 100644 index 139f81840aab..000000000000 --- a/tests/coverage/unreachable/return/expected +++ /dev/null @@ -1,8 +0,0 @@ -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 deleted file mode 100644 index ccd76a5b4f8e..000000000000 --- a/tests/coverage/unreachable/return/main.rs +++ /dev/null @@ -1,17 +0,0 @@ -// 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 index 624aa520edc9..fe2e32e1e528 100644 --- a/tests/coverage/unreachable/tutorial_unreachable/expected +++ b/tests/coverage/unreachable/tutorial_unreachable/expected @@ -1,5 +1,6 @@ -coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL -coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL -coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL -coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE -coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL +Source-based code coverage results: + +main.rs (unreachable_example)\ + * 5:1 - 8:13 COVERED\ + * 8:14 - 10:6 UNCOVERED\ + * 10:6 - 10:7 COVERED diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected index 8fa3ec8b870f..629eca0dcf8f 100644 --- a/tests/coverage/unreachable/variant/expected +++ b/tests/coverage/unreachable/variant/expected @@ -1,10 +1,14 @@ -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 +Source-based code coverage results: + +main.rs (main)\ + * 26:1 - 29:2 COVERED + +main.rs (print_direction)\ + * 14:1 - 14:36 COVERED\ + * 15:11 - 15:14 UNCOVERED\ + * 16:26 - 16:47 UNCOVERED\ + * 17:28 - 17:51 UNCOVERED\ + * 18:28 - 18:51 COVERED\ + * 19:34 - 19:63 UNCOVERED\ + * 21:14 - 21:45 UNCOVERED\ + * 23:1 - 23:2 COVERED diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs index 76a589147bca..7fec251c0ffe 100644 --- a/tests/coverage/unreachable/variant/main.rs +++ b/tests/coverage/unreachable/variant/main.rs @@ -12,7 +12,7 @@ enum Direction { } fn print_direction(dir: Direction) { - match dir { + match dir { // For some reason, `dir`'s span is reported as `UNCOVERED` too Direction::Up => println!("Going up!"), Direction::Down => println!("Going down!"), Direction::Left => println!("Going left!"), diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected index e47941f17db2..bb7a2d495852 100644 --- a/tests/coverage/unreachable/vectors/expected +++ b/tests/coverage/unreachable/vectors/expected @@ -1,6 +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 +Source-based code coverage results: + +main.rs (main)\ + * 7:1 - 11:39 COVERED\ + * 13:17 - 13:22 UNCOVERED\ + * 16:12 - 18:6 COVERED diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected index dc66d3e823d3..34afef9ee12c 100644 --- a/tests/coverage/unreachable/while-loop-break/expected +++ b/tests/coverage/unreachable/while-loop-break/expected @@ -1,11 +1,13 @@ -coverage/unreachable/while-loop-break/main.rs, 8, FULL -coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL -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 +Source-based code coverage results: + +main.rs (find_first_negative)\ + * 7:1 - 8:22 COVERED\ + * 9:11 - 9:29 COVERED\ + * 10:12 - 10:27 COVERED\ + * 11:20 - 11:37 COVERED\ + * 12:10 - 13:19 COVERED\ + * 15:5 - 15:9 UNCOVERED\ + * 16:1 - 16:2 COVERED + +main.rs (main)\ + * 19:1 - 23:2 COVERED diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 50f1e3035ac8..c8387c691296 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -320,7 +320,7 @@ impl<'test> TestCx<'test> { 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"]); + kani.arg("--coverage").args(["-Z", "source-coverage"]); if !self.props.cbmc_flags.is_empty() { kani.arg("--cbmc-args").args(&self.props.cbmc_flags); From f029874d5e4597bff0cf8a89ac2599183b454244 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 20:44:22 +0000 Subject: [PATCH 31/59] Bless tests more --- tests/coverage/reachable/assert-false/expected | 12 ------------ tests/coverage/reachable/assert-false/main.rs | 18 ------------------ .../reachable/overflow/reachable_pass/expected | 12 ++++-------- .../unreachable/assume_assert/expected | 2 +- tests/coverage/unreachable/bounds/expected | 2 +- .../coverage/unreachable/debug-assert/expected | 14 +++++++------- 6 files changed, 13 insertions(+), 47 deletions(-) delete mode 100644 tests/coverage/reachable/assert-false/expected delete mode 100644 tests/coverage/reachable/assert-false/main.rs diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected deleted file mode 100644 index b6043db371b6..000000000000 --- a/tests/coverage/reachable/assert-false/expected +++ /dev/null @@ -1,12 +0,0 @@ -Source-based code coverage results: - -main.rs (any_bool)\ - * 4:1 - 6:2 COVERED - -main.rs (main)\ - * 9:1 - 10:18 COVERED\ - * 10:19 - 12:6 COVERED\ - * 12:6 - 12:7 COVERED\ - * 15:13 - 16:32 COVERED\ - * 17:6 - 17:7 COVERED\ - * 18:1 - 18:2 COVERED diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs deleted file mode 100644 index 034cc5e1951b..000000000000 --- a/tests/coverage/reachable/assert-false/main.rs +++ /dev/null @@ -1,18 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -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/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected index 7e8197c66289..4d17761505eb 100644 --- a/tests/coverage/reachable/overflow/reachable_pass/expected +++ b/tests/coverage/reachable/overflow/reachable_pass/expected @@ -1,13 +1,9 @@ Source-based code coverage results: -tests/coverage/reachable/overflow/reachable_pass/test.rs (main) - * 12:1 - 17:2 COVERED\ +test.rs (main)\ + * 12:1 - 17:2 COVERED -tests/coverage/reachable/overflow/reachable_pass/test.rs (reduce) +test.rs (reduce)\ * 7:1 - 8:16 COVERED\ * 8:19 - 8:27 COVERED\ - * 8:37 - 8:38 COVERED\ - -Verification Time: 0.052936167s - -error: could not find project metadata required for coverage metadata + * 8:37 - 8:38 COVERED diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected index ef5487f9462f..d1dc56f00f5c 100644 --- a/tests/coverage/unreachable/assume_assert/expected +++ b/tests/coverage/unreachable/assume_assert/expected @@ -1,4 +1,4 @@ Source-based code coverage results: main.rs (check_assume_assert)\ - * 4:1 - 8:2 COVERED + * 10:1 - 14:2 COVERED diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected index fc9f57841169..b8658ab6163d 100644 --- a/tests/coverage/unreachable/bounds/expected +++ b/tests/coverage/unreachable/bounds/expected @@ -6,4 +6,4 @@ test.rs (get)\ * 5:44 - 5:46 COVERED test.rs (main)\ - * 9:1 - 12:2 COVERED + * 9:1 - 11:2 COVERED diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected index 7b6a322ca040..77029948807d 100644 --- a/tests/coverage/unreachable/debug-assert/expected +++ b/tests/coverage/unreachable/debug-assert/expected @@ -1,10 +1,10 @@ Source-based code coverage results: tests/coverage/unreachable/debug-assert/main.rs (main) - * 5:1 - 5:11 COVERED\ - * 6:9 - 6:10 COVERED\ - * 6:14 - 6:18 COVERED\ - * 7:30 - 7:71 UNCOVERED\ - * 8:9 - 8:23 UNCOVERED\ - * 8:25 - 8:53 UNCOVERED\ - * 10:1 - 10:2 UNCOVERED + * 10:1 - 10:11 COVERED\ + * 11:9 - 11:10 COVERED\ + * 11:14 - 11:18 COVERED\ + * 12:30 - 12:71 UNCOVERED\ + * 13:9 - 13:23 UNCOVERED\ + * 13:25 - 13:53 UNCOVERED\ + * 15:1 - 15:2 UNCOVERED From 6eefd6f1ec728228e1b744618a8eb3e8d78bd8ee Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 20:57:58 +0000 Subject: [PATCH 32/59] Fix postprocess with closures - bless test too --- .../src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/call_cbmc.rs | 2 +- tests/coverage/reachable/assert/reachable_pass/expected | 9 +++++++++ tests/coverage/reachable/assert/reachable_pass/test.rs | 2 +- 4 files changed, 12 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 881cce94df3b..b8ec5a95ad28 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::Coverage(coverage_opaque) => { let function_name = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let counter_data = format!("{coverage_opaque:?} {{{function_name}}}"); + let counter_data = format!("{coverage_opaque:?} ({function_name})"); let maybe_code_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); if let Some(code_region) = maybe_code_region { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index e2aecb4767ac..053fe61c0291 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -437,7 +437,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \{(?[^\}]+)\} - (?.+)"#, + r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \((?[^\)]+)\) - (?.+)"#, ) .unwrap() }) diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected index e69de29bb2d1..d71bfb8df74a 100644 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -0,0 +1,9 @@ +Source-based code coverage results: + +test.rs (main)\ + * 5:1 - 6:34 COVERED\ + * 7:14 - 9:6 COVERED\ + * 9:6 - 9:7 UNCOVERED + +test.rs (main::{closure#0})\ + * 6:40 - 6:49 COVERED diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs index 72acca2b764c..fe500a99cf5b 100644 --- a/tests/coverage/reachable/assert/reachable_pass/test.rs +++ b/tests/coverage/reachable/assert/reachable_pass/test.rs @@ -5,6 +5,6 @@ fn main() { let x: u32 = kani::any_where(|val| *val == 5); if x > 3 { - assert!(x > 4); // FULL: `x > 4` since `x = 5` + assert!(x > 4); } } From 0262056b092a5b867e18e5eec5f809a33a1fd7ef Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 21:08:26 +0000 Subject: [PATCH 33/59] Fix format in tests.. --- tests/coverage/unreachable/if-statement/main.rs | 2 +- tests/coverage/unreachable/variant/expected | 14 +++++++------- tests/coverage/unreachable/variant/main.rs | 3 ++- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/unreachable/if-statement/main.rs index 030fd3bd29b4..c18d4dd4a5e4 100644 --- a/tests/coverage/unreachable/if-statement/main.rs +++ b/tests/coverage/unreachable/if-statement/main.rs @@ -5,7 +5,7 @@ fn check_number(num: i32) -> &'static str { if num > 0 { // The next line is partially covered if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" } - } else if num < 0 { // From here on, only the terminator is covered + } else if num < 0 { "Negative" } else { "Zero" diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected index 629eca0dcf8f..2d1eb8d0fe60 100644 --- a/tests/coverage/unreachable/variant/expected +++ b/tests/coverage/unreachable/variant/expected @@ -5,10 +5,10 @@ main.rs (main)\ main.rs (print_direction)\ * 14:1 - 14:36 COVERED\ - * 15:11 - 15:14 UNCOVERED\ - * 16:26 - 16:47 UNCOVERED\ - * 17:28 - 17:51 UNCOVERED\ - * 18:28 - 18:51 COVERED\ - * 19:34 - 19:63 UNCOVERED\ - * 21:14 - 21:45 UNCOVERED\ - * 23:1 - 23:2 COVERED + * 16:11 - 16:14 UNCOVERED\ + * 17:26 - 17:47 UNCOVERED\ + * 18:28 - 18:51 UNCOVERED\ + * 19:28 - 19:51 COVERED\ + * 20:34 - 20:63 UNCOVERED\ + * 22:14 - 22:45 UNCOVERED\ + * 24:1 - 24:2 COVERED diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs index 7fec251c0ffe..faaacad43b63 100644 --- a/tests/coverage/unreachable/variant/main.rs +++ b/tests/coverage/unreachable/variant/main.rs @@ -12,7 +12,8 @@ enum Direction { } fn print_direction(dir: Direction) { - match dir { // For some reason, `dir`'s span is reported as `UNCOVERED` too + // For some reason, `dir`'s span is reported as `UNCOVERED` too + match dir { Direction::Up => println!("Going up!"), Direction::Down => println!("Going down!"), Direction::Left => println!("Going left!"), From be21bd7ede17753bd65edcce1e3151e120c61264 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 21:21:21 +0000 Subject: [PATCH 34/59] Manual `cargo update` to see if lock errors go away --- Cargo.lock | 84 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 47 insertions(+), 37 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f55c2f8c2f47..29c18bfbe0c1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -161,9 +161,12 @@ dependencies = [ [[package]] name = "cc" -version = "1.1.10" +version = "1.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e9e8aabfac534be767c909e0690571677d49f41bd8465ae876fe043d52ba5292" +checksum = "5fb8dd288a69fc53a1996d7ecfbf4a20d59065bff137ce7e56bbd620de191189" +dependencies = [ + "shlex", +] [[package]] name = "cfg-if" @@ -187,9 +190,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.13" +version = "4.5.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fbb260a053428790f3de475e304ff84cdbc4face759ea7a3e64c1edd938a7fc" +checksum = "11d8838454fda655dafd3accb2b6e2bea645b9e4078abe84a22ceb947235c5cc" dependencies = [ "clap_builder", "clap_derive", @@ -197,9 +200,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.13" +version = "4.5.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64b17d7ea74e9f833c7dbf2cbe4fb12ff26783eda4782a8975b72f895c9b4d99" +checksum = "216aec2b177652e3846684cbfe25c9964d18ec45234f0f5da5157b207ed1aab6" dependencies = [ "anstream", "anstyle", @@ -216,7 +219,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] @@ -471,9 +474,9 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.3.0" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de3fc2e30ba82dd1b3911c8de1ffc143c74a914a14e99514d7637e3099df5ea0" +checksum = "93ead53efc7ea8ed3cfb0c79fc8023fbb782a5432b52830b6518941cebe6505c" dependencies = [ "equivalent", "hashbrown", @@ -502,9 +505,9 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "js-sys" -version = "0.3.69" +version = "0.3.70" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "29c15563dc2726973df627357ce0c9ddddbea194836909d655df6a75d2cf296d" +checksum = "1868808506b929d7b0cfa8f75951347aa71bb21144b7791bae35d9bccfcfe37a" dependencies = [ "wasm-bindgen", ] @@ -590,7 +593,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] @@ -1030,29 +1033,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.204" +version = "1.0.207" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bc76f558e0cbb2a839d37354c575f1dc3fdc6546b5be373ba43d95f231bf7c12" +checksum = "5665e14a49a4ea1b91029ba7d3bca9f299e1f7cfa194388ccc20f14743e784f2" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.204" +version = "1.0.207" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222" +checksum = "6aea2634c86b0e8ef2cfdc0c340baede54ec27b1e46febd7f80dffb2aa44a00e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] name = "serde_json" -version = "1.0.122" +version = "1.0.124" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "784b6203951c57ff748476b126ccb5e8e2959a5c19e5c617ab1956be3dbc68da" +checksum = "66ad62847a56b3dba58cc891acd13884b9c61138d330c0d7b6181713d4fce38d" dependencies = [ "itoa", "memchr", @@ -1106,6 +1109,12 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + [[package]] name = "smallvec" version = "1.13.2" @@ -1152,7 +1161,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] @@ -1167,9 +1176,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.72" +version = "2.0.74" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af" +checksum = "1fceb41e3d546d0bd83421d3409b1460cc7444cd389341a4c880fe7a042cb3d7" dependencies = [ "proc-macro2", "quote", @@ -1206,7 +1215,7 @@ checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" dependencies = [ "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] @@ -1272,7 +1281,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] [[package]] @@ -1391,34 +1400,35 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.92" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4be2531df63900aeb2bca0daaaddec08491ee64ceecbee5076636a3b026795a8" +checksum = "a82edfc16a6c469f5f44dc7b571814045d60404b55a0ee849f9bcfa2e63dd9b5" dependencies = [ "cfg-if", + "once_cell", "wasm-bindgen-macro", ] [[package]] name = "wasm-bindgen-backend" -version = "0.2.92" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "614d787b966d3989fa7bb98a654e369c762374fd3213d212cfc0251257e747da" +checksum = "9de396da306523044d3302746f1208fa71d7532227f15e347e2d93e4145dd77b" dependencies = [ "bumpalo", "log", "once_cell", "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-macro" -version = "0.2.92" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1f8823de937b71b9460c0c34e25f3da88250760bec0ebac694b49997550d726" +checksum = "585c4c91a46b072c92e908d99cb1dcdf95c5218eeb6f3bf1efa991ee7a68cccf" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1426,22 +1436,22 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.92" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e94f17b526d0a461a191c78ea52bbce64071ed5c04c9ffe424dcb38f74171bb7" +checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" dependencies = [ "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", "wasm-bindgen-backend", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-shared" -version = "0.2.92" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af190c94f2773fdb3729c55b007a722abb5384da03bc0986df4c289bf5567e96" +checksum = "c62a0a307cb4a311d3a07867860911ca130c3494e8c2719593806c08bc5d0484" [[package]] name = "which" @@ -1610,5 +1620,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.72", + "syn 2.0.74", ] From db1b1a3a4187740634dd518e299c2dad6ca07ca6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 14 Aug 2024 21:59:06 +0000 Subject: [PATCH 35/59] Scaffold coverage results saving for standalone mdoe --- kani-driver/src/coverage/cov_session.rs | 32 +++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index 4a8b44bc147b..eeb340100cd5 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/kani-driver/src/coverage/cov_session.rs @@ -18,6 +18,14 @@ impl KaniSession { /// Note: Currently, coverage mappings are not included due to technical /// limitations. But this is where we should save them. pub fn save_coverage_metadata(&self, project: &Project, stamp: &String) -> Result<()> { + if self.args.target_dir.is_some() { + self.save_coverage_metadata_cargo(project, stamp) + } else { + self.save_coverage_metadata_standalone(project, stamp) + } + } + + fn save_coverage_metadata_cargo(&self, project: &Project, stamp: &String) -> Result<()> { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -58,11 +66,27 @@ impl KaniSession { Ok(()) } + fn save_coverage_metadata_standalone(&self, project: &Project, stamp: &String) -> Result<()> { + Ok(()) + } + /// Saves raw coverage check results required for coverage-related features. pub fn save_coverage_results( &self, results: &Vec, stamp: &String, + ) -> Result<()> { + if self.args.target_dir.is_some() { + self.save_coverage_results_cargo(results, stamp) + } else { + self.save_coverage_results_standalone(results, stamp) + } + } + + pub fn save_coverage_results_cargo( + &self, + results: &Vec, + stamp: &String, ) -> Result<()> { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; @@ -96,4 +120,12 @@ impl KaniSession { println!("[info] Coverage results saved to {}", &outdir.display()); Ok(()) } + + pub fn save_coverage_results_standalone( + &self, + results: &Vec, + stamp: &String, + ) -> Result<()> { + Ok(()) + } } From 0162d3072af4cb76f9ea0661d19bf5f2f2ee5229 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 17:29:55 +0000 Subject: [PATCH 36/59] Save coverage results with standalone mode --- kani-driver/src/coverage/cov_session.rs | 47 ++++++++++++++++++++++++- kani-driver/src/main.rs | 2 +- kani-driver/src/project.rs | 11 ++++-- 3 files changed, 55 insertions(+), 5 deletions(-) diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index eeb340100cd5..df82d982bd72 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/kani-driver/src/coverage/cov_session.rs @@ -67,19 +67,40 @@ impl KaniSession { } fn save_coverage_metadata_standalone(&self, project: &Project, stamp: &String) -> Result<()> { + let input = project.input.clone().unwrap().canonicalize().unwrap(); + let input_dir = input.parent().unwrap().to_path_buf(); + let outdir = input_dir.join(format!("kanicov_{stamp}")); + + // Generally we don't expect this directory to exist, but there's no + // reason to delete it if it does. + if !outdir.exists() { + fs::create_dir(&outdir)?; + } + + // In this case, the source files correspond to the input file + let source_targets = vec![input]; + + let kanimap_name = format!("kanicov_{stamp}_kanimap"); + let file_name = outdir.join(kanimap_name).with_extension("json"); + let mut kanimap_file = File::create(file_name)?; + + let serialized_data = serde_json::to_string(&source_targets)?; + kanimap_file.write_all(serialized_data.as_bytes())?; + Ok(()) } /// Saves raw coverage check results required for coverage-related features. pub fn save_coverage_results( &self, + project: &Project, results: &Vec, stamp: &String, ) -> Result<()> { if self.args.target_dir.is_some() { self.save_coverage_results_cargo(results, stamp) } else { - self.save_coverage_results_standalone(results, stamp) + self.save_coverage_results_standalone(project, results, stamp) } } @@ -123,9 +144,33 @@ impl KaniSession { pub fn save_coverage_results_standalone( &self, + project: &Project, results: &Vec, stamp: &String, ) -> Result<()> { + let input = project.input.clone().unwrap().canonicalize().unwrap(); + let input_dir = input.parent().unwrap().to_path_buf(); + let outdir = input_dir.join(format!("kanicov_{stamp}")); + + // This directory should have been created by `save_coverage_metadata`, + // so now we expect it to exist. + if !outdir.exists() { + bail!("directory associated to coverage run does not exist") + } + + for harness_res in results { + let harness_name = harness_res.harness.mangled_name.clone(); + let kaniraw_name = format!("{harness_name}_kaniraw"); + let file_name = outdir.join(kaniraw_name).with_extension("json"); + let mut cov_file = File::create(file_name)?; + + let cov_results = &harness_res.result.coverage_results.clone().unwrap(); + let serialized_data = serde_json::to_string(&cov_results)?; + cov_file.write_all(serialized_data.as_bytes())?; + } + + println!("[info] Coverage results saved to {}", &outdir.display()); + Ok(()) } } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 489bb0b3535b..1510de3eb777 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -134,7 +134,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { if session.args.coverage { let timestamp = Local::now().format("%Y-%m-%d_%H-%M").to_string(); session.save_coverage_metadata(&project, ×tamp)?; - session.save_coverage_results(&results, ×tamp)?; + session.save_coverage_results(&project, &results, ×tamp)?; } session.print_final_summary(&results) diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 2bc0845cdb46..4d6aee3a9a79 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -33,6 +33,9 @@ pub struct Project { /// The directory where all outputs should be directed to. This path represents the canonical /// version of outdir. pub outdir: PathBuf, + /// The path to the input file the project was built from. + /// Note that it will only be `Some(...)` if this was built from a standalone project. + pub input: Option, /// The collection of artifacts kept as part of this project. artifacts: Vec, /// Records the cargo metadata from the build, if there was any @@ -82,6 +85,7 @@ impl Project { fn try_new( session: &KaniSession, outdir: PathBuf, + input: Option, metadata: Vec, cargo_metadata: Option, failed_targets: Option>, @@ -115,7 +119,7 @@ impl Project { } } - Ok(Project { outdir, metadata, artifacts, cargo_metadata, failed_targets }) + Ok(Project { outdir, input, metadata, artifacts, cargo_metadata, failed_targets }) } } @@ -178,6 +182,7 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result Project::try_new( session, outdir, + None, metadata, Some(outputs.cargo_metadata), outputs.failed_targets, @@ -243,7 +248,7 @@ impl<'a> StandaloneProjectBuilder<'a> { let metadata = from_json(&self.metadata)?; // Create the project with the artifacts built by the compiler. - let result = Project::try_new(self.session, self.outdir, vec![metadata], None, None); + let result = Project::try_new(self.session, self.outdir, Some(self.input), vec![metadata], None, None); if let Ok(project) = &result { self.session.record_temporary_files(&project.artifacts); } @@ -297,5 +302,5 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result>>()?; - Project::try_new(session, outdir, metadata, None, None) + Project::try_new(session, outdir, None, metadata, None, None) } From 96206010b7bd847630506edb60a858bedd3ff441 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 17:30:29 +0000 Subject: [PATCH 37/59] Format fixes --- kani-driver/src/project.rs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 4d6aee3a9a79..e0d2d2edd139 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -248,7 +248,14 @@ impl<'a> StandaloneProjectBuilder<'a> { let metadata = from_json(&self.metadata)?; // Create the project with the artifacts built by the compiler. - let result = Project::try_new(self.session, self.outdir, Some(self.input), vec![metadata], None, None); + let result = Project::try_new( + self.session, + self.outdir, + Some(self.input), + vec![metadata], + None, + None, + ); if let Ok(project) = &result { self.session.record_temporary_files(&project.artifacts); } From 8511087452d35a8565105b022330ec52cba8639d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 17:42:52 +0000 Subject: [PATCH 38/59] Add test for saving coverage results --- tests/ui/save-coverage-results/expected | 3 +++ tests/ui/save-coverage-results/test.rs | 29 +++++++++++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/ui/save-coverage-results/expected create mode 100644 tests/ui/save-coverage-results/test.rs diff --git a/tests/ui/save-coverage-results/expected b/tests/ui/save-coverage-results/expected new file mode 100644 index 000000000000..77c9a0c33dcb --- /dev/null +++ b/tests/ui/save-coverage-results/expected @@ -0,0 +1,3 @@ +Source-based code coverage results: + +[info] Coverage results saved to diff --git a/tests/ui/save-coverage-results/test.rs b/tests/ui/save-coverage-results/test.rs new file mode 100644 index 000000000000..ae0dd6f35d6c --- /dev/null +++ b/tests/ui/save-coverage-results/test.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --coverage -Zsource-coverage + +//! Checks that we print a line which points the user to the path where coverage +//! results have been saved. The line should look like: +//! ``` +//! [info] Coverage results saved to /path/to/outdir/kanicov_YYYY-MM-DD_hh-mm +//! ``` + +fn _other_function() { + println!("Hello, world!"); +} + +fn test_cov(val: u32) -> bool { + if val < 3 || val == 42 { + true + } else { + false + } +} + +#[cfg_attr(kani, kani::proof)] +fn main() { + let test1 = test_cov(1); + let test2 = test_cov(2); + assert!(test1); + assert!(test2); +} From 93faa8a9133c9d354b8b84972e33ca232f0ffd48 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 18:39:35 +0000 Subject: [PATCH 39/59] Format new test --- tests/ui/save-coverage-results/test.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/ui/save-coverage-results/test.rs b/tests/ui/save-coverage-results/test.rs index ae0dd6f35d6c..0a422280e51d 100644 --- a/tests/ui/save-coverage-results/test.rs +++ b/tests/ui/save-coverage-results/test.rs @@ -13,11 +13,7 @@ fn _other_function() { } fn test_cov(val: u32) -> bool { - if val < 3 || val == 42 { - true - } else { - false - } + if val < 3 || val == 42 { true } else { false } } #[cfg_attr(kani, kani::proof)] From d484c5431bba761ca059953ea8ac06e45eb7e3e5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 18:44:45 +0000 Subject: [PATCH 40/59] Add running test to `coverage` --- tests/coverage/if-statement-multi/expected | 11 ++++++++++ tests/coverage/if-statement-multi/test.rs | 25 ++++++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 tests/coverage/if-statement-multi/expected create mode 100644 tests/coverage/if-statement-multi/test.rs diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected new file mode 100644 index 000000000000..fe6331eb7945 --- /dev/null +++ b/tests/coverage/if-statement-multi/expected @@ -0,0 +1,11 @@ +Source-based code coverage results: + +test.rs (main)\ + * 20:1 - 25:2 COVERED + +test.rs (test_cov)\ + * 15:1 - 16:15 COVERED\ + * 16:19 - 16:28 UNCOVERED\ + * 16:31 - 16:35 COVERED\ + * 16:45 - 16:50 UNCOVERED\ + * 17:1 - 17:2 COVERED diff --git a/tests/coverage/if-statement-multi/test.rs b/tests/coverage/if-statement-multi/test.rs new file mode 100644 index 000000000000..0a422280e51d --- /dev/null +++ b/tests/coverage/if-statement-multi/test.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --coverage -Zsource-coverage + +//! Checks that we print a line which points the user to the path where coverage +//! results have been saved. The line should look like: +//! ``` +//! [info] Coverage results saved to /path/to/outdir/kanicov_YYYY-MM-DD_hh-mm +//! ``` + +fn _other_function() { + println!("Hello, world!"); +} + +fn test_cov(val: u32) -> bool { + if val < 3 || val == 42 { true } else { false } +} + +#[cfg_attr(kani, kani::proof)] +fn main() { + let test1 = test_cov(1); + let test2 = test_cov(2); + assert!(test1); + assert!(test2); +} From 9afd0a3154c904041a71bf60addb48fd8950100f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 15 Aug 2024 20:06:23 +0000 Subject: [PATCH 41/59] Fix `variant.rs` test --- tests/coverage/unreachable/variant/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected index 2d1eb8d0fe60..06cdec3ff646 100644 --- a/tests/coverage/unreachable/variant/expected +++ b/tests/coverage/unreachable/variant/expected @@ -1,7 +1,7 @@ Source-based code coverage results: main.rs (main)\ - * 26:1 - 29:2 COVERED + * 27:1 - 30:2 COVERED main.rs (print_direction)\ * 14:1 - 14:36 COVERED\ From e630a329800cc973e6cdcb3b2dbf4671b9e8e76f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 16 Aug 2024 18:22:49 +0000 Subject: [PATCH 42/59] Avoid problems with functions with cov info --- .../src/codegen_cprover_gotoc/codegen/function.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 726c21d9d4ef..6cf934562c05 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -250,13 +250,16 @@ pub mod rustc_smir { // We need to pull the coverage info from the internal MIR instance. let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def)); - let cov_info = &body.function_coverage_info.clone().unwrap(); - // Iterate over the coverage mappings and match with the coverage term. - for mapping in &cov_info.mappings { - let Code(term) = mapping.kind else { unreachable!() }; - if term == coverage { - return Some(mapping.code_region.clone()); + // Some functions, like `std` ones, may not have coverage info attached + // to them because they have been compiled without coverage flags. + if let Some(cov_info) = &body.function_coverage_info { + // Iterate over the coverage mappings and match with the coverage term. + for mapping in &cov_info.mappings { + let Code(term) = mapping.kind else { unreachable!() }; + if term == coverage { + return Some(mapping.code_region.clone()); + } } } None From 7bfd91950de1fa0dc29afa87ceabd1eb4b8e3031 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 16 Aug 2024 18:57:13 +0000 Subject: [PATCH 43/59] Temp: Run `kani-perf.sh` with coverage on --- tools/compiletest/src/runtest.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index c8387c691296..60e0b715a98d 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -272,7 +272,9 @@ impl<'test> TestCx<'test> { .arg("kani") .arg("--target-dir") .arg(self.output_base_dir().join("target")) - .current_dir(parent_dir); + .current_dir(parent_dir) + .arg("--coverage") + .arg("-Zsource-coverage"); if test { cargo.arg("--tests"); } From 95e87888fafd196bb42bedb806ff81e9be5681ec Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 16 Aug 2024 20:24:53 +0000 Subject: [PATCH 44/59] Use $ as the separator for function names --- kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-driver/src/call_cbmc.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index b8ec5a95ad28..81407c4dc704 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::Coverage(coverage_opaque) => { let function_name = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); - let counter_data = format!("{coverage_opaque:?} ({function_name})"); + let counter_data = format!("{coverage_opaque:?} ${function_name}$"); let maybe_code_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); if let Some(code_region) = maybe_code_region { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 053fe61c0291..72bb2347ca11 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -437,7 +437,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \((?[^\)]+)\) - (?.+)"#, + r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, ) .unwrap() }) From a79c9d6bb3dc863eb60acdefe368691bbcc07e3a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 19:09:12 +0000 Subject: [PATCH 45/59] Remove comment and `-C opt-level=0` --- kani-driver/src/call_single_file.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index ef979e7233ec..07f4f53aaa5e 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -157,8 +157,7 @@ impl KaniSession { // We only use panic abort strategy for verification since we cannot handle unwind logic. if self.args.coverage { flags.extend_from_slice( - // &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "--emit=mir"].map(OsString::from), - &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "-C", "opt-level=0"] + &["-C", "instrument-coverage", "-Z", "no-profiler-runtime"] .map(OsString::from), ); } From 5a574f7e3758d49ee79747a7e1ff56568fa944f1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 19:11:28 +0000 Subject: [PATCH 46/59] Undo change in `compiletest` to run with coverage --- tools/compiletest/src/runtest.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 60e0b715a98d..c8387c691296 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -272,9 +272,7 @@ impl<'test> TestCx<'test> { .arg("kani") .arg("--target-dir") .arg(self.output_base_dir().join("target")) - .current_dir(parent_dir) - .arg("--coverage") - .arg("-Zsource-coverage"); + .current_dir(parent_dir); if test { cargo.arg("--tests"); } From 0943ee33e6936c1f6dc1d785b6dc571406d847f4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 19:22:23 +0000 Subject: [PATCH 47/59] Format --- kani-driver/src/call_single_file.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 07f4f53aaa5e..868d1adce636 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -157,8 +157,7 @@ impl KaniSession { // We only use panic abort strategy for verification since we cannot handle unwind logic. if self.args.coverage { flags.extend_from_slice( - &["-C", "instrument-coverage", "-Z", "no-profiler-runtime"] - .map(OsString::from), + &["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(OsString::from), ); } flags.extend_from_slice( From e6165a22a0db30cf73f41d2c9bd0aeaee6993292 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 20:22:40 +0000 Subject: [PATCH 48/59] Use `time` instead of `chrono` --- Cargo.lock | 206 +++++++++++----------------------------- kani-driver/Cargo.toml | 2 +- kani-driver/src/main.rs | 6 +- 3 files changed, 58 insertions(+), 156 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ab6f14e7d570..dcb6b5392292 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -23,21 +23,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "android-tzdata" -version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e999941b234f3131b00bc13c22d06e8c5ff726d1b6318ac7eb276997bbb4fef0" - -[[package]] -name = "android_system_properties" -version = "0.1.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311" -dependencies = [ - "libc", -] - [[package]] name = "anstream" version = "0.6.15" @@ -115,12 +100,6 @@ dependencies = [ "which", ] -[[package]] -name = "bumpalo" -version = "3.16.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" - [[package]] name = "byteorder" version = "1.5.0" @@ -159,35 +138,12 @@ dependencies = [ "thiserror", ] -[[package]] -name = "cc" -version = "1.1.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fb8dd288a69fc53a1996d7ecfbf4a20d59065bff137ce7e56bbd620de191189" -dependencies = [ - "shlex", -] - [[package]] name = "cfg-if" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" -[[package]] -name = "chrono" -version = "0.4.38" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a21f936df1771bf62b77f047b726c4625ff2e8aa607c01ec06e5a05bd8463401" -dependencies = [ - "android-tzdata", - "iana-time-zone", - "js-sys", - "num-traits", - "wasm-bindgen", - "windows-targets", -] - [[package]] name = "clap" version = "4.5.15" @@ -276,12 +232,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "core-foundation-sys" -version = "0.8.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" - [[package]] name = "cprover_bindings" version = "0.54.0" @@ -365,6 +315,15 @@ dependencies = [ "memchr", ] +[[package]] +name = "deranged" +version = "0.3.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4" +dependencies = [ + "powerfmt", +] + [[package]] name = "either" version = "1.13.0" @@ -449,29 +408,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "iana-time-zone" -version = "0.1.60" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e7ffbb5a1b541ea2561f8c41c087286cc091e21e556a4f09a8f6cbf17b69b141" -dependencies = [ - "android_system_properties", - "core-foundation-sys", - "iana-time-zone-haiku", - "js-sys", - "wasm-bindgen", - "windows-core", -] - -[[package]] -name = "iana-time-zone-haiku" -version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" -dependencies = [ - "cc", -] - [[package]] name = "indexmap" version = "2.4.0" @@ -503,15 +439,6 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" -[[package]] -name = "js-sys" -version = "0.3.70" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1868808506b929d7b0cfa8f75951347aa71bb21144b7791bae35d9bccfcfe37a" -dependencies = [ - "wasm-bindgen", -] - [[package]] name = "kani" version = "0.54.0" @@ -547,7 +474,6 @@ version = "0.54.0" dependencies = [ "anyhow", "cargo_metadata", - "chrono", "clap", "comfy-table", "console", @@ -564,6 +490,7 @@ dependencies = [ "strum", "strum_macros", "tempfile", + "time", "toml", "tracing", "tracing-subscriber", @@ -715,6 +642,12 @@ dependencies = [ "num-traits", ] +[[package]] +name = "num-conv" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9" + [[package]] name = "num-integer" version = "0.1.46" @@ -812,6 +745,12 @@ version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" +[[package]] +name = "powerfmt" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" + [[package]] name = "ppv-lite86" version = "0.2.20" @@ -1109,12 +1048,6 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - [[package]] name = "smallvec" version = "1.13.2" @@ -1228,6 +1161,37 @@ dependencies = [ "once_cell", ] +[[package]] +name = "time" +version = "0.3.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885" +dependencies = [ + "deranged", + "itoa", + "num-conv", + "powerfmt", + "serde", + "time-core", + "time-macros", +] + +[[package]] +name = "time-core" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3" + +[[package]] +name = "time-macros" +version = "0.2.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf" +dependencies = [ + "num-conv", + "time-core", +] + [[package]] name = "toml" version = "0.8.19" @@ -1398,61 +1362,6 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -[[package]] -name = "wasm-bindgen" -version = "0.2.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a82edfc16a6c469f5f44dc7b571814045d60404b55a0ee849f9bcfa2e63dd9b5" -dependencies = [ - "cfg-if", - "once_cell", - "wasm-bindgen-macro", -] - -[[package]] -name = "wasm-bindgen-backend" -version = "0.2.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9de396da306523044d3302746f1208fa71d7532227f15e347e2d93e4145dd77b" -dependencies = [ - "bumpalo", - "log", - "once_cell", - "proc-macro2", - "quote", - "syn 2.0.74", - "wasm-bindgen-shared", -] - -[[package]] -name = "wasm-bindgen-macro" -version = "0.2.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "585c4c91a46b072c92e908d99cb1dcdf95c5218eeb6f3bf1efa991ee7a68cccf" -dependencies = [ - "quote", - "wasm-bindgen-macro-support", -] - -[[package]] -name = "wasm-bindgen-macro-support" -version = "0.2.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.74", - "wasm-bindgen-backend", - "wasm-bindgen-shared", -] - -[[package]] -name = "wasm-bindgen-shared" -version = "0.2.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c62a0a307cb4a311d3a07867860911ca130c3494e8c2719593806c08bc5d0484" - [[package]] name = "which" version = "6.0.2" @@ -1496,15 +1405,6 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-core" -version = "0.52.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "33ab640c8d7e35bf8ba19b884ba838ceb4fba93a4e8c65a9059d08afcfc683d9" -dependencies = [ - "windows-targets", -] - [[package]] name = "windows-sys" version = "0.52.0" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 154f127a63c9..27fef66ffb65 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -15,7 +15,6 @@ publish = false kani_metadata = { path = "../kani_metadata" } cargo_metadata = "0.18.0" anyhow = "1" -chrono = "0.4.38" console = "0.15.1" once_cell = "1.19.0" serde = { version = "1", features = ["derive"] } @@ -35,6 +34,7 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} rand = "0.8" which = "6" +time = {version = "0.3.36", features = ["formatting"]} # A good set of suggested dependencies can be found in rustup: # https://github.com/rust-lang/rustup/blob/master/Cargo.toml diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 1510de3eb777..db76d1474836 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -5,7 +5,7 @@ use std::ffi::OsString; use std::process::ExitCode; use anyhow::Result; -use chrono::Local; +use time::{OffsetDateTime, format_description}; use args::{check_is_valid, CargoKaniSubcommand}; use args_toml::join_args; @@ -132,7 +132,9 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let results = runner.check_all_harnesses(&harnesses)?; if session.args.coverage { - let timestamp = Local::now().format("%Y-%m-%d_%H-%M").to_string(); + let time_now = OffsetDateTime::now_utc(); + let format = format_description::parse("[year]-[month]-[day]_[hour]-[minute]").unwrap(); + let timestamp = time_now.format(&format).unwrap(); session.save_coverage_metadata(&project, ×tamp)?; session.save_coverage_results(&project, &results, ×tamp)?; } From ecf1d7e93e691870bd25491cf56e2c8ef6634aa1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 20:26:40 +0000 Subject: [PATCH 49/59] Change in format --- kani-driver/src/main.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index db76d1474836..714edc2cfa1b 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -5,7 +5,7 @@ use std::ffi::OsString; use std::process::ExitCode; use anyhow::Result; -use time::{OffsetDateTime, format_description}; +use time::{format_description, OffsetDateTime}; use args::{check_is_valid, CargoKaniSubcommand}; use args_toml::join_args; From 047f24db5244906d21780c2ac9e8e170a424f3a9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 22:04:35 +0000 Subject: [PATCH 50/59] Fix test description --- tests/coverage/if-statement-multi/test.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tests/coverage/if-statement-multi/test.rs b/tests/coverage/if-statement-multi/test.rs index 0a422280e51d..ac00dec3f451 100644 --- a/tests/coverage/if-statement-multi/test.rs +++ b/tests/coverage/if-statement-multi/test.rs @@ -2,11 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --coverage -Zsource-coverage -//! Checks that we print a line which points the user to the path where coverage -//! results have been saved. The line should look like: -//! ``` -//! [info] Coverage results saved to /path/to/outdir/kanicov_YYYY-MM-DD_hh-mm -//! ``` +//! Checks that we are covering all regions except +//! * the `val == 42` condition +//! * the `false` branch +//! +//! No coverage information is shown for `_other_function` because it's sliced +//! off: fn _other_function() { println!("Hello, world!"); From 88ba7e563b62f5d312707db0f32c7d8c40d8f9d0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 22:06:33 +0000 Subject: [PATCH 51/59] Paste link to issue --- tests/coverage/unreachable/assume_assert/main.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs index 1eb5a08198b1..90f26b2121fa 100644 --- a/tests/coverage/unreachable/assume_assert/main.rs +++ b/tests/coverage/unreachable/assume_assert/main.rs @@ -4,8 +4,9 @@ //! This test should check that the region after `kani::assume(false)` is //! `UNCOVERED`. However, due to a technical limitation in `rustc`'s coverage //! instrumentation, only one `COVERED` region is reported for the whole -//! function. -//! TODO: Create issue and paste here. +//! function. More details in +//! . + #[kani::proof] fn check_assume_assert() { let a: u8 = kani::any(); From c0cc10d5fa16781c769d9a1c0f8f846ffce4feb6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 20 Aug 2024 23:07:39 +0000 Subject: [PATCH 52/59] Reorganize and document tests --- .../coverage/{unreachable => }/abort/expected | 0 .../coverage/{unreachable => }/abort/main.rs | 0 .../{unreachable => }/assert/expected | 0 .../coverage/{unreachable => }/assert/test.rs | 0 .../{unreachable => }/assert_eq/expected | 0 .../{unreachable => }/assert_eq/test.rs | 0 .../{unreachable => }/assert_ne/expected | 0 .../{unreachable => }/assert_ne/test.rs | 0 .../coverage/{unreachable => }/break/expected | 0 .../coverage/{unreachable => }/break/main.rs | 0 .../{unreachable => }/compare/expected | 0 .../{unreachable => }/compare/main.rs | 0 .../{unreachable => }/contradiction/expected | 0 .../{unreachable => }/contradiction/main.rs | 0 .../{unreachable => }/debug-assert/expected | 2 +- .../{unreachable => }/debug-assert/main.rs | 0 .../reachable_pass => div-zero}/expected | 0 .../reachable_pass => div-zero}/test.rs | 0 .../{unreachable => }/early-return/expected | 0 .../{unreachable => }/early-return/main.rs | 0 .../{unreachable => }/if-statement/expected | 0 .../{unreachable => }/if-statement/main.rs | 0 .../assert_uncovered_end/expected | 9 +++++++ .../known_issues/assert_uncovered_end/test.rs | 14 +++++++++++ .../assume_assert/expected | 0 .../assume_assert/main.rs | 0 .../known_issues/out-of-bounds/expected | 7 ++++++ .../known_issues/out-of-bounds/test.rs | 15 +++++++++++ tests/coverage/known_issues/variant/expected | 14 +++++++++++ .../variant/main.rs | 4 ++- .../multiple-harnesses/expected | 0 .../multiple-harnesses/main.rs | 0 .../expected | 0 .../test.rs | 0 .../expected | 0 .../test.rs | 0 .../reachable/assert/reachable_pass/expected | 9 ------- .../reachable/assert/reachable_pass/test.rs | 10 -------- .../reachable/bounds/reachable_fail/expected | 7 ------ .../reachable/bounds/reachable_fail/test.rs | 11 -------- .../div-zero/reachable_fail/expected | 7 ------ .../reachable/div-zero/reachable_fail/test.rs | 11 -------- tests/coverage/unreachable/bounds/expected | 9 ------- tests/coverage/unreachable/bounds/test.rs | 11 -------- tests/coverage/unreachable/check_id/expected | 11 -------- tests/coverage/unreachable/check_id/main.rs | 25 ------------------- .../unreachable/tutorial_unreachable/expected | 6 ----- .../unreachable/tutorial_unreachable/main.rs | 11 -------- tests/coverage/unreachable/variant/expected | 14 ----------- tests/coverage/unreachable/vectors/expected | 6 ----- tests/coverage/unreachable/vectors/main.rs | 19 -------------- .../while-loop-break/expected | 0 .../while-loop-break/main.rs | 0 53 files changed, 63 insertions(+), 169 deletions(-) rename tests/coverage/{unreachable => }/abort/expected (100%) rename tests/coverage/{unreachable => }/abort/main.rs (100%) rename tests/coverage/{unreachable => }/assert/expected (100%) rename tests/coverage/{unreachable => }/assert/test.rs (100%) rename tests/coverage/{unreachable => }/assert_eq/expected (100%) rename tests/coverage/{unreachable => }/assert_eq/test.rs (100%) rename tests/coverage/{unreachable => }/assert_ne/expected (100%) rename tests/coverage/{unreachable => }/assert_ne/test.rs (100%) rename tests/coverage/{unreachable => }/break/expected (100%) rename tests/coverage/{unreachable => }/break/main.rs (100%) rename tests/coverage/{unreachable => }/compare/expected (100%) rename tests/coverage/{unreachable => }/compare/main.rs (100%) rename tests/coverage/{unreachable => }/contradiction/expected (100%) rename tests/coverage/{unreachable => }/contradiction/main.rs (100%) rename tests/coverage/{unreachable => }/debug-assert/expected (80%) rename tests/coverage/{unreachable => }/debug-assert/main.rs (100%) rename tests/coverage/{reachable/div-zero/reachable_pass => div-zero}/expected (100%) rename tests/coverage/{reachable/div-zero/reachable_pass => div-zero}/test.rs (100%) rename tests/coverage/{unreachable => }/early-return/expected (100%) rename tests/coverage/{unreachable => }/early-return/main.rs (100%) rename tests/coverage/{unreachable => }/if-statement/expected (100%) rename tests/coverage/{unreachable => }/if-statement/main.rs (100%) create mode 100644 tests/coverage/known_issues/assert_uncovered_end/expected create mode 100644 tests/coverage/known_issues/assert_uncovered_end/test.rs rename tests/coverage/{unreachable => known_issues}/assume_assert/expected (100%) rename tests/coverage/{unreachable => known_issues}/assume_assert/main.rs (100%) create mode 100644 tests/coverage/known_issues/out-of-bounds/expected create mode 100644 tests/coverage/known_issues/out-of-bounds/test.rs create mode 100644 tests/coverage/known_issues/variant/expected rename tests/coverage/{unreachable => known_issues}/variant/main.rs (79%) rename tests/coverage/{unreachable => }/multiple-harnesses/expected (100%) rename tests/coverage/{unreachable => }/multiple-harnesses/main.rs (100%) rename tests/coverage/{reachable/overflow/reachable_fail => overflow-failure}/expected (100%) rename tests/coverage/{reachable/overflow/reachable_fail => overflow-failure}/test.rs (100%) rename tests/coverage/{reachable/overflow/reachable_pass => overflow-full-coverage}/expected (100%) rename tests/coverage/{reachable/overflow/reachable_pass => overflow-full-coverage}/test.rs (100%) delete mode 100644 tests/coverage/reachable/assert/reachable_pass/expected delete mode 100644 tests/coverage/reachable/assert/reachable_pass/test.rs delete mode 100644 tests/coverage/reachable/bounds/reachable_fail/expected delete mode 100644 tests/coverage/reachable/bounds/reachable_fail/test.rs delete mode 100644 tests/coverage/reachable/div-zero/reachable_fail/expected delete mode 100644 tests/coverage/reachable/div-zero/reachable_fail/test.rs delete mode 100644 tests/coverage/unreachable/bounds/expected delete mode 100644 tests/coverage/unreachable/bounds/test.rs delete mode 100644 tests/coverage/unreachable/check_id/expected delete mode 100644 tests/coverage/unreachable/check_id/main.rs delete mode 100644 tests/coverage/unreachable/tutorial_unreachable/expected delete mode 100644 tests/coverage/unreachable/tutorial_unreachable/main.rs delete mode 100644 tests/coverage/unreachable/variant/expected delete mode 100644 tests/coverage/unreachable/vectors/expected delete mode 100644 tests/coverage/unreachable/vectors/main.rs rename tests/coverage/{unreachable => }/while-loop-break/expected (100%) rename tests/coverage/{unreachable => }/while-loop-break/main.rs (100%) diff --git a/tests/coverage/unreachable/abort/expected b/tests/coverage/abort/expected similarity index 100% rename from tests/coverage/unreachable/abort/expected rename to tests/coverage/abort/expected diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/abort/main.rs similarity index 100% rename from tests/coverage/unreachable/abort/main.rs rename to tests/coverage/abort/main.rs diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/assert/expected similarity index 100% rename from tests/coverage/unreachable/assert/expected rename to tests/coverage/assert/expected diff --git a/tests/coverage/unreachable/assert/test.rs b/tests/coverage/assert/test.rs similarity index 100% rename from tests/coverage/unreachable/assert/test.rs rename to tests/coverage/assert/test.rs diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/assert_eq/expected similarity index 100% rename from tests/coverage/unreachable/assert_eq/expected rename to tests/coverage/assert_eq/expected diff --git a/tests/coverage/unreachable/assert_eq/test.rs b/tests/coverage/assert_eq/test.rs similarity index 100% rename from tests/coverage/unreachable/assert_eq/test.rs rename to tests/coverage/assert_eq/test.rs diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/assert_ne/expected similarity index 100% rename from tests/coverage/unreachable/assert_ne/expected rename to tests/coverage/assert_ne/expected diff --git a/tests/coverage/unreachable/assert_ne/test.rs b/tests/coverage/assert_ne/test.rs similarity index 100% rename from tests/coverage/unreachable/assert_ne/test.rs rename to tests/coverage/assert_ne/test.rs diff --git a/tests/coverage/unreachable/break/expected b/tests/coverage/break/expected similarity index 100% rename from tests/coverage/unreachable/break/expected rename to tests/coverage/break/expected diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/break/main.rs similarity index 100% rename from tests/coverage/unreachable/break/main.rs rename to tests/coverage/break/main.rs diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/compare/expected similarity index 100% rename from tests/coverage/unreachable/compare/expected rename to tests/coverage/compare/expected diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/compare/main.rs similarity index 100% rename from tests/coverage/unreachable/compare/main.rs rename to tests/coverage/compare/main.rs diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/contradiction/expected similarity index 100% rename from tests/coverage/unreachable/contradiction/expected rename to tests/coverage/contradiction/expected diff --git a/tests/coverage/unreachable/contradiction/main.rs b/tests/coverage/contradiction/main.rs similarity index 100% rename from tests/coverage/unreachable/contradiction/main.rs rename to tests/coverage/contradiction/main.rs diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/debug-assert/expected similarity index 80% rename from tests/coverage/unreachable/debug-assert/expected rename to tests/coverage/debug-assert/expected index 77029948807d..fbe57690d347 100644 --- a/tests/coverage/unreachable/debug-assert/expected +++ b/tests/coverage/debug-assert/expected @@ -1,6 +1,6 @@ Source-based code coverage results: -tests/coverage/unreachable/debug-assert/main.rs (main) +main.rs (main)\ * 10:1 - 10:11 COVERED\ * 11:9 - 11:10 COVERED\ * 11:14 - 11:18 COVERED\ diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/debug-assert/main.rs similarity index 100% rename from tests/coverage/unreachable/debug-assert/main.rs rename to tests/coverage/debug-assert/main.rs diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/div-zero/expected similarity index 100% rename from tests/coverage/reachable/div-zero/reachable_pass/expected rename to tests/coverage/div-zero/expected diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/div-zero/test.rs similarity index 100% rename from tests/coverage/reachable/div-zero/reachable_pass/test.rs rename to tests/coverage/div-zero/test.rs diff --git a/tests/coverage/unreachable/early-return/expected b/tests/coverage/early-return/expected similarity index 100% rename from tests/coverage/unreachable/early-return/expected rename to tests/coverage/early-return/expected diff --git a/tests/coverage/unreachable/early-return/main.rs b/tests/coverage/early-return/main.rs similarity index 100% rename from tests/coverage/unreachable/early-return/main.rs rename to tests/coverage/early-return/main.rs diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/if-statement/expected similarity index 100% rename from tests/coverage/unreachable/if-statement/expected rename to tests/coverage/if-statement/expected diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/if-statement/main.rs similarity index 100% rename from tests/coverage/unreachable/if-statement/main.rs rename to tests/coverage/if-statement/main.rs diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected new file mode 100644 index 000000000000..ceba065ce424 --- /dev/null +++ b/tests/coverage/known_issues/assert_uncovered_end/expected @@ -0,0 +1,9 @@ +Source-based code coverage results: + +test.rs (check_assert)\ + * 9:1 - 10:34 COVERED\ + * 11:14 - 13:6 COVERED\ + * 13:6 - 13:7 UNCOVERED + +test.rs (check_assert::{closure#0})\ + * 10:40 - 10:49 COVERED diff --git a/tests/coverage/known_issues/assert_uncovered_end/test.rs b/tests/coverage/known_issues/assert_uncovered_end/test.rs new file mode 100644 index 000000000000..c3da20c8b00b --- /dev/null +++ b/tests/coverage/known_issues/assert_uncovered_end/test.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that `check_assert` is fully covered. At present, the coverage for +//! this test reports an uncovered single-column region at the end of the `if` +//! statement: + +#[kani::proof] +fn check_assert() { + let x: u32 = kani::any_where(|val| *val == 5); + if x > 3 { + assert!(x > 4); + } +} diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected similarity index 100% rename from tests/coverage/unreachable/assume_assert/expected rename to tests/coverage/known_issues/assume_assert/expected diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/known_issues/assume_assert/main.rs similarity index 100% rename from tests/coverage/unreachable/assume_assert/main.rs rename to tests/coverage/known_issues/assume_assert/main.rs diff --git a/tests/coverage/known_issues/out-of-bounds/expected b/tests/coverage/known_issues/out-of-bounds/expected new file mode 100644 index 000000000000..8ab9e2e15627 --- /dev/null +++ b/tests/coverage/known_issues/out-of-bounds/expected @@ -0,0 +1,7 @@ +Source-based code coverage results: + +test.rs (get)\ + * 8:1 - 10:2 COVERED + +test.rs (main)\ + * 13:1 - 15:2 COVERED diff --git a/tests/coverage/known_issues/out-of-bounds/test.rs b/tests/coverage/known_issues/out-of-bounds/test.rs new file mode 100644 index 000000000000..83242590815b --- /dev/null +++ b/tests/coverage/known_issues/out-of-bounds/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test should check that the return in `get` is `UNCOVERED`. However, the +//! coverage results currently report that the whole function is `COVERED`, +//! likely due to + +fn get(s: &[i16], index: usize) -> i16 { + s[index] +} + +#[kani::proof] +fn main() { + get(&[7, -83, 19], 15); +} diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected new file mode 100644 index 000000000000..13383ed3bab0 --- /dev/null +++ b/tests/coverage/known_issues/variant/expected @@ -0,0 +1,14 @@ +Source-based code coverage results: + +main.rs (main)\ + * 29:1 - 32:2 COVERED + +main.rs (print_direction)\ + * 16:1 - 16:36 COVERED\ + * 18:11 - 18:14 UNCOVERED\ + * 19:26 - 19:47 UNCOVERED\ + * 20:28 - 20:51 UNCOVERED\ + * 21:28 - 21:51 COVERED\ + * 22:34 - 22:63 UNCOVERED\ + * 24:14 - 24:45 UNCOVERED\ + * 26:1 - 26:2 COVERED diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/known_issues/variant/main.rs similarity index 79% rename from tests/coverage/unreachable/variant/main.rs rename to tests/coverage/known_issues/variant/main.rs index faaacad43b63..c654ca355c45 100644 --- a/tests/coverage/unreachable/variant/main.rs +++ b/tests/coverage/known_issues/variant/main.rs @@ -2,7 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks coverage results in an example with a `match` statement matching on -//! all enum variants. +//! all enum variants. Currently, it does not yield the expected results because +//! it reports the `dir` in the match statement as `UNCOVERED`: +//! enum Direction { Up, diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected similarity index 100% rename from tests/coverage/unreachable/multiple-harnesses/expected rename to tests/coverage/multiple-harnesses/expected diff --git a/tests/coverage/unreachable/multiple-harnesses/main.rs b/tests/coverage/multiple-harnesses/main.rs similarity index 100% rename from tests/coverage/unreachable/multiple-harnesses/main.rs rename to tests/coverage/multiple-harnesses/main.rs diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/overflow-failure/expected similarity index 100% rename from tests/coverage/reachable/overflow/reachable_fail/expected rename to tests/coverage/overflow-failure/expected diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/overflow-failure/test.rs similarity index 100% rename from tests/coverage/reachable/overflow/reachable_fail/test.rs rename to tests/coverage/overflow-failure/test.rs diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/overflow-full-coverage/expected similarity index 100% rename from tests/coverage/reachable/overflow/reachable_pass/expected rename to tests/coverage/overflow-full-coverage/expected diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/overflow-full-coverage/test.rs similarity index 100% rename from tests/coverage/reachable/overflow/reachable_pass/test.rs rename to tests/coverage/overflow-full-coverage/test.rs diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected deleted file mode 100644 index d71bfb8df74a..000000000000 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ /dev/null @@ -1,9 +0,0 @@ -Source-based code coverage results: - -test.rs (main)\ - * 5:1 - 6:34 COVERED\ - * 7:14 - 9:6 COVERED\ - * 9:6 - 9:7 UNCOVERED - -test.rs (main::{closure#0})\ - * 6:40 - 6:49 COVERED diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs deleted file mode 100644 index fe500a99cf5b..000000000000 --- a/tests/coverage/reachable/assert/reachable_pass/test.rs +++ /dev/null @@ -1,10 +0,0 @@ -// 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); - } -} diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected deleted file mode 100644 index 51d953241b62..000000000000 --- a/tests/coverage/reachable/bounds/reachable_fail/expected +++ /dev/null @@ -1,7 +0,0 @@ -Source-based code coverage results: - -test.rs (get) - * 4:1 - 6:2 COVERED - -test.rs (main) - * 9:1 - 11:2 COVERED diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs deleted file mode 100644 index 585c35eafd4f..000000000000 --- a/tests/coverage/reachable/bounds/reachable_fail/test.rs +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -fn get(s: &[i16], index: usize) -> i16 { - s[index] -} - -#[kani::proof] -fn main() { - get(&[7, -83, 19], 15); -} diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected deleted file mode 100644 index fdabea0e8acc..000000000000 --- a/tests/coverage/reachable/div-zero/reachable_fail/expected +++ /dev/null @@ -1,7 +0,0 @@ -Source-based code coverage results: - -test.rs (div)\ - * 4:1 - 6:2 COVERED - -tests/coverage/reachable/div-zero/reachable_fail/test.rs (main)\ - * 9:1 - 11:2 COVERED diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs deleted file mode 100644 index 91af9a4ca802..000000000000 --- a/tests/coverage/reachable/div-zero/reachable_fail/test.rs +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -fn div(x: u16, y: u16) -> u16 { - x / y -} - -#[kani::proof] -fn main() { - div(678, 0); -} diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected deleted file mode 100644 index b8658ab6163d..000000000000 --- a/tests/coverage/unreachable/bounds/expected +++ /dev/null @@ -1,9 +0,0 @@ -Source-based code coverage results: - -test.rs (get)\ - * 4:1 - 5:23 COVERED\ - * 5:26 - 5:34 UNCOVERED\ - * 5:44 - 5:46 COVERED - -test.rs (main)\ - * 9:1 - 11:2 COVERED diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs deleted file mode 100644 index 9ef6573b2a52..000000000000 --- a/tests/coverage/unreachable/bounds/test.rs +++ /dev/null @@ -1,11 +0,0 @@ -// 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(&[5, 206, -46, 321, 8], 8); -} diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected deleted file mode 100644 index 2506c6cfa2f6..000000000000 --- a/tests/coverage/unreachable/check_id/expected +++ /dev/null @@ -1,11 +0,0 @@ -Source-based code coverage results: - -main.rs (foo)\ - * 4:1 - 6:13 COVERED\ - * 6:14 - 9:6 UNCOVERED\ - * 9:6 - 9:7 COVERED - -main.rs (main)\ - * 13:1 - 14:24 COVERED\ - * 15:30 - 15:32 COVERED\ - * 15:42 - 15:44 COVERED diff --git a/tests/coverage/unreachable/check_id/main.rs b/tests/coverage/unreachable/check_id/main.rs deleted file mode 100644 index 8273a9bcc679..000000000000 --- a/tests/coverage/unreachable/check_id/main.rs +++ /dev/null @@ -1,25 +0,0 @@ -// 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/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected deleted file mode 100644 index fe2e32e1e528..000000000000 --- a/tests/coverage/unreachable/tutorial_unreachable/expected +++ /dev/null @@ -1,6 +0,0 @@ -Source-based code coverage results: - -main.rs (unreachable_example)\ - * 5:1 - 8:13 COVERED\ - * 8:14 - 10:6 UNCOVERED\ - * 10:6 - 10:7 COVERED diff --git a/tests/coverage/unreachable/tutorial_unreachable/main.rs b/tests/coverage/unreachable/tutorial_unreachable/main.rs deleted file mode 100644 index c56e591446cf..000000000000 --- a/tests/coverage/unreachable/tutorial_unreachable/main.rs +++ /dev/null @@ -1,11 +0,0 @@ -// 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 deleted file mode 100644 index 06cdec3ff646..000000000000 --- a/tests/coverage/unreachable/variant/expected +++ /dev/null @@ -1,14 +0,0 @@ -Source-based code coverage results: - -main.rs (main)\ - * 27:1 - 30:2 COVERED - -main.rs (print_direction)\ - * 14:1 - 14:36 COVERED\ - * 16:11 - 16:14 UNCOVERED\ - * 17:26 - 17:47 UNCOVERED\ - * 18:28 - 18:51 UNCOVERED\ - * 19:28 - 19:51 COVERED\ - * 20:34 - 20:63 UNCOVERED\ - * 22:14 - 22:45 UNCOVERED\ - * 24:1 - 24:2 COVERED diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected deleted file mode 100644 index bb7a2d495852..000000000000 --- a/tests/coverage/unreachable/vectors/expected +++ /dev/null @@ -1,6 +0,0 @@ -Source-based code coverage results: - -main.rs (main)\ - * 7:1 - 11:39 COVERED\ - * 13:17 - 13:22 UNCOVERED\ - * 16:12 - 18:6 COVERED diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs deleted file mode 100644 index a44c4bb47c3d..000000000000 --- a/tests/coverage/unreachable/vectors/main.rs +++ /dev/null @@ -1,19 +0,0 @@ -// 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/while-loop-break/expected similarity index 100% rename from tests/coverage/unreachable/while-loop-break/expected rename to tests/coverage/while-loop-break/expected diff --git a/tests/coverage/unreachable/while-loop-break/main.rs b/tests/coverage/while-loop-break/main.rs similarity index 100% rename from tests/coverage/unreachable/while-loop-break/main.rs rename to tests/coverage/while-loop-break/main.rs From fb7c9e9134558148039ad17e0a3870c5edcc1e64 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 21 Aug 2024 14:54:39 +0000 Subject: [PATCH 53/59] Fix up some `expected` outputs --- tests/coverage/if-statement-multi/expected | 12 ++++++------ tests/coverage/known_issues/assume_assert/expected | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected index fe6331eb7945..4e8382d10a6f 100644 --- a/tests/coverage/if-statement-multi/expected +++ b/tests/coverage/if-statement-multi/expected @@ -1,11 +1,11 @@ Source-based code coverage results: test.rs (main)\ - * 20:1 - 25:2 COVERED + * 21:1 - 26:2 COVERED test.rs (test_cov)\ - * 15:1 - 16:15 COVERED\ - * 16:19 - 16:28 UNCOVERED\ - * 16:31 - 16:35 COVERED\ - * 16:45 - 16:50 UNCOVERED\ - * 17:1 - 17:2 COVERED + * 16:1 - 17:15 COVERED\ + * 17:19 - 17:28 UNCOVERED\ + * 17:31 - 17:35 COVERED\ + * 17:45 - 17:50 UNCOVERED\ + * 18:1 - 18:2 COVERED diff --git a/tests/coverage/known_issues/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected index d1dc56f00f5c..55f3235d7d24 100644 --- a/tests/coverage/known_issues/assume_assert/expected +++ b/tests/coverage/known_issues/assume_assert/expected @@ -1,4 +1,4 @@ Source-based code coverage results: main.rs (check_assume_assert)\ - * 10:1 - 14:2 COVERED + * 11:1 - 15:2 COVERED From cf3b46529bddce448e387de635cc4be6259ec7f9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 22 Aug 2024 13:49:26 +0000 Subject: [PATCH 54/59] Make `parse_coverage_opaque` return a `CovTerm` directly --- .../src/codegen_cprover_gotoc/codegen/function.rs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 6cf934562c05..e52c2cae30d1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -235,7 +235,7 @@ pub mod rustc_smir { coverage_opaque: &CoverageOpaque, instance: Instance, ) -> Option { - let cov_term = parse_coverage_opaque(coverage_opaque)?; + let cov_term = parse_coverage_opaque(coverage_opaque); region_from_coverage(tcx, cov_term, instance) } @@ -267,18 +267,16 @@ pub mod rustc_smir { fn parse_coverage_opaque(coverage_opaque: &Opaque) -> Option { let coverage_str = coverage_opaque.to_string(); - if coverage_str == "Zero" { - Some(CovTerm::Zero) - } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { + if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); - Some(CovTerm::Counter(num.into())) + CovTerm::Counter(num.into()) } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); - Some(CovTerm::Expression(num.into())) + CovTerm::Expression(num.into()) } else { - None + CovTerm::Zero } } } From a7ea4ee8380fce7d0c192fcde5f95a640a972b7f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 22 Aug 2024 13:51:11 +0000 Subject: [PATCH 55/59] Add documentation to `parse_coverage_opaque` --- .../src/codegen_cprover_gotoc/codegen/function.rs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index e52c2cae30d1..0793e0c4688f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -265,7 +265,14 @@ pub mod rustc_smir { None } - fn parse_coverage_opaque(coverage_opaque: &Opaque) -> Option { + /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`: + /// + /// + /// At present, a `CovTerm` can be one of the following: + /// - `CounterIncrement()`: A physical counter. + /// - `ExpressionUsed()`: An expression-based counter. + /// - `Zero`: A counter with a constant zero value. + fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm { let coverage_str = coverage_opaque.to_string(); if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { let (num_str, _rest) = rest.split_once(')').unwrap(); From 0d56bdd51f66f312791d33561ee815b51898313a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 22 Aug 2024 14:02:57 +0000 Subject: [PATCH 56/59] Remove `coverage_args` module --- kani-driver/src/args/coverage_args.rs | 17 ----------------- kani-driver/src/args/mod.rs | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kani-driver/src/args/coverage_args.rs diff --git a/kani-driver/src/args/coverage_args.rs b/kani-driver/src/args/coverage_args.rs deleted file mode 100644 index 31827d88f0e8..000000000000 --- a/kani-driver/src/args/coverage_args.rs +++ /dev/null @@ -1,17 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::args::CommonArgs; -use clap::Parser; - -#[derive(Debug, Parser)] -pub struct CargoCoverageArgs { - #[command(flatten)] - pub coverage: CoverageArgs, -} - -#[derive(Debug, clap::Args)] -pub struct CoverageArgs { - /// Common args always available to Kani subcommands. - #[command(flatten)] - pub common_opts: CommonArgs, -} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index b933c555b391..c3cfc113af64 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -5,7 +5,6 @@ pub mod assess_args; pub mod cargo; pub mod common; -pub mod coverage_args; pub mod playback_args; pub mod std_args; From 8912288b2cfdfee94150649a130914649092e0e8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 15:32:35 +0000 Subject: [PATCH 57/59] Add timestamp comment --- kani-driver/src/main.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 714edc2cfa1b..d3bd697d2ea4 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -132,9 +132,18 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let results = runner.check_all_harnesses(&harnesses)?; if session.args.coverage { + // We generate a timestamp to save the coverage data in a folder named + // `kanicov_` where `` is the current date based on `format` + // below. The purpose of adding timestamps to the folder name is to make + // coverage results easily identifiable. Using a timestamp makes + // coverage results not only distinguishable, but also easy to relate to + // verification runs. We expect this to be particularly helpful for + // users in a proof debugging session, who are usually interested in the + // most recent results. let time_now = OffsetDateTime::now_utc(); let format = format_description::parse("[year]-[month]-[day]_[hour]-[minute]").unwrap(); let timestamp = time_now.format(&format).unwrap(); + session.save_coverage_metadata(&project, ×tamp)?; session.save_coverage_results(&project, &results, ×tamp)?; } From 1f821fd8c74c4c2ab8148a517a0abd8784f499be Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 15:34:26 +0000 Subject: [PATCH 58/59] Fix args and comment in postprocessing --- kani-driver/src/call_cbmc.rs | 7 +------ kani-driver/src/cbmc_property_renderer.rs | 2 +- kani-driver/src/harness_runner.rs | 6 +----- 3 files changed, 3 insertions(+), 12 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 72bb2347ca11..66c30b931882 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -329,12 +329,7 @@ impl VerificationResult { } } - pub fn render( - &self, - output_format: &OutputFormat, - should_panic: bool, - _coverage_mode: bool, - ) -> String { + pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String { match &self.results { Ok(results) => { let status = self.status; diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 1cb674b98eb5..a0202169863c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -423,7 +423,7 @@ pub fn format_result( } /// Separate checks into coverage and non-coverage based on property class and -/// format them separately for `--coverage``. Then we report both verification +/// format them separately for `--coverage`. Then we report both verification /// and processed coverage results. /// /// Note: The reporting of coverage results should be removed once `kani-cov` is diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index f3b77fb9b231..7e432932ab29 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -124,11 +124,7 @@ 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, - self.args.coverage - ) + result.render(&self.args.output_format, harness.attributes.should_panic) ); } self.gen_and_add_concrete_playback(harness, &mut result)?; From 7ad9c8dfe8c096ca20d166f18246185557f7506f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 16:01:03 +0000 Subject: [PATCH 59/59] Add comment on regex --- kani-driver/src/call_cbmc.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 66c30b931882..bc4424aeb231 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -428,6 +428,20 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option. If that were the + // case, we would not need the spans in these descriptions. let counter_re = { static COUNTER_RE: OnceLock = OnceLock::new(); COUNTER_RE.get_or_init(|| {