diff --git a/Cargo.lock b/Cargo.lock index 878d61a62889..72eb37af2211 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -316,6 +316,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" @@ -500,6 +509,7 @@ dependencies = [ "strum", "strum_macros", "tempfile", + "time", "toml", "tracing", "tracing-subscriber", @@ -660,6 +670,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" @@ -767,6 +783,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" @@ -1179,6 +1201,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" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index f78cf3eba707..4ee81d0c7d3e 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::mir::{Place, ProjectionElem}; use stable_mir::ty::{Span as SpanStable, TypeAndMut}; use strum_macros::{AsRefStr, EnumString}; @@ -148,18 +149,19 @@ 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, + 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)`. - self.codegen_assert( - Expr::bool_false(), - PropertyClass::CodeCoverage, - "code coverage for location", - 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 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 a1afa343a6e7..0793e0c4688f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -216,3 +216,74 @@ impl<'tcx> GotocCtx<'tcx> { self.reset_current_fn(); } } + +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; + + type CoverageOpaque = stable_mir::Opaque; + + /// Retrieves the `CodeRegion` associated with the data in a + /// `CoverageOpaque` object. + pub fn region_from_coverage_opaque( + tcx: TyCtxt, + coverage_opaque: &CoverageOpaque, + instance: Instance, + ) -> Option { + let cov_term = parse_coverage_opaque(coverage_opaque); + region_from_coverage(tcx, cov_term, instance) + } + + /// 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)); + + // 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 + } + + /// 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(); + let num = num_str.parse::().unwrap(); + 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(); + CovTerm::Expression(num.into()) + } else { + 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 b8db1a3d52b6..81407c4dc704 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::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}; @@ -158,12 +159,28 @@ impl<'tcx> GotocCtx<'tcx> { location, ) } + 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 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 + 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/Cargo.toml b/kani-driver/Cargo.toml index c57ec8e8e2f2..27fef66ffb65 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -34,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/args/mod.rs b/kani-driver/src/args/mod.rs index 2d7593e8050a..c3cfc113af64 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -615,12 +615,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-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 4e8e83b562af..e69062a0cd4f 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -206,7 +206,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 387a9723fcdb..bc4424aeb231 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -3,10 +3,15 @@ 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; use std::path::Path; use std::process::Command; +use std::sync::OnceLock; use std::time::{Duration, Instant}; use crate::args::{OutputFormat, VerificationArgs}; @@ -14,6 +19,8 @@ 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::{CoverageRegion, CoverageTerm}; use crate::session::KaniSession; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. @@ -54,6 +61,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 { @@ -273,12 +282,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, } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure @@ -288,6 +299,7 @@ impl VerificationResult { results: Err(output.process_status), runtime, generated_concrete_test: false, + coverage_results: None, } } } @@ -299,6 +311,7 @@ impl VerificationResult { results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, + coverage_results: None, } } @@ -312,23 +325,26 @@ impl VerificationResult { results: Err(42), runtime: Duration::from_secs(0), generated_concrete_test: false, + coverage_results: None, } } - 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; 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) }; @@ -404,6 +420,74 @@ 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; + } + + // Postprocessing the coverage results involves matching on the descriptions + // of code coverage properties with the `counter_re` regex. These are two + // real examples of such descriptions: + // + // ``` + // CounterIncrement(0) $test_cov$ - src/main.rs:5:1 - 6:15 + // ExpressionUsed(0) $test_cov$ - src/main.rs:6:19 - 6:28 + // ``` + // + // The span is further processed to extract the code region attributes. + // Ideally, we should have coverage mappings (i.e., the relation between + // counters and code regions) available in the coverage metadata: + // . 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(|| { + Regex::new( + r#"^(?CounterIncrement|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) = counter_re.captures(&prop.description) { + let kind = &captures["kind"]; + let counter_num = &captures["counter_num"]; + let function = demangle(&captures["func_name"]).to_string(); + let status = prop.status; + let span = captures["span"].to_string(); + + 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), + }; + let region = CoverageRegion::from_str(span); + + let cov_check = CoverageCheck::new(function, term, region, status); + let file = cov_check.region.file.clone(); + + if let Entry::Vacant(e) = coverage_results.entry(file.clone()) { + e.insert(vec![cov_check]); + } else { + coverage_results.entry(file).and_modify(|checks| checks.push(cov_check)); + } + prop_processed = true; + } + + assert!(prop_processed, "error: coverage property not processed\n{prop:?}"); + } + + 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/call_single_file.rs b/kani-driver/src/call_single_file.rs index 4b30fe877507..868d1adce636 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -155,6 +155,11 @@ impl KaniSession { pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec { let mut flags: Vec<_> = base_rustc_flags(lib_config); // 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), + ); + } flags.extend_from_slice( &[ "-C", diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index b3a78e8d03e2..8ef1ee153106 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 4f32028b5866..a0202169863c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -4,12 +4,12 @@ use crate::args::OutputFormat; use crate::call_cbmc::{FailedProperties, VerificationStatus}; use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem}; +use crate::coverage::cov_results::CoverageResults; use console::style; use once_cell::sync::Lazy; use regex::Regex; use rustc_demangle::demangle; -use std::collections::{BTreeMap, HashMap}; -use strum_macros::{AsRefStr, Display}; +use std::collections::HashMap; type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>; @@ -150,15 +150,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"; @@ -431,72 +422,31 @@ 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, 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 coverage_output = format_result_coverage(&coverage_checks); - let result = format!("{}\n{}", verification_output, 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 } -/// Generate coverage result from all coverage properties (i.e., checks with `code_coverage` property class). -/// Loops through each of the checks with the `code_coverage` property class on a line and gives: -/// - A status `FULL` if all checks pertaining to a line number are `COVERED` -/// - A status `NONE` if all checks related to a line are `UNCOVERED` -/// - Otherwise (i.e., if the line contains both) it reports `PARTIAL`. -/// -/// Used when the user requests coverage information with `--coverage`. -/// Output is tested through the `coverage-based` testing suite, not the regular -/// `expected` suite. -fn format_result_coverage(properties: &[Property]) -> String { - let mut formatted_output = String::new(); - formatted_output.push_str("\nCoverage Results:\n"); - - let mut coverage_results: BTreeMap> = - BTreeMap::default(); - for prop in properties { - let src = prop.source_location.clone(); - let file_entries = coverage_results.entry(src.file.unwrap()).or_default(); - let check_status = if prop.status == CheckStatus::Covered { - CoverageStatus::Full - } else { - CoverageStatus::None - }; - - // Create Map> - file_entries - .entry(src.line.unwrap().parse().unwrap()) - .and_modify(|line_status| { - if *line_status != check_status { - *line_status = CoverageStatus::Partial - } - }) - .or_insert(check_status); - } - - // Create formatted string that is returned to the user as output - for (file, checks) in coverage_results.iter() { - for (line_number, coverage_status) in checks { - formatted_output.push_str(&format!("{}, {}, {}\n", file, line_number, coverage_status)); - } - formatted_output.push('\n'); - } - - formatted_output -} - /// Attempts to build a message for a failed property with as much detailed /// information on the source location as possible. fn build_failure_message(description: String, trace: &Option>) -> String { diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs new file mode 100644 index 000000000000..845ae7de21bb --- /dev/null +++ b/kani-driver/src/coverage/cov_results.rs @@ -0,0 +1,96 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::cbmc_output_parser::CheckStatus; +use serde::{Deserialize, Serialize}; +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>, +} + +impl CoverageResults { + pub fn new(data: BTreeMap>) -> Self { + Self { data } + } +} + +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_default().push(check.clone()); + } + + 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)?; + } + } + Ok(()) + } +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +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, Serialize, Deserialize)] +pub enum CoverageTerm { + Counter(u32), + Expression(u32), +} + +#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)] +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 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 } + } +} diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs new file mode 100644 index 000000000000..df82d982bd72 --- /dev/null +++ b/kani-driver/src/coverage/cov_session.rs @@ -0,0 +1,176 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use std::fs; +use std::fs::File; +use std::io::Write; + +use crate::harness_runner::HarnessResult; +use crate::project::Project; +use crate::KaniSession; +use anyhow::{bail, Result}; + +impl KaniSession { + /// 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<()> { + 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 + .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}")); + + // 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(()) + } + + 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(project, 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)?; + 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 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(()) + } + + 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/coverage/mod.rs b/kani-driver/src/coverage/mod.rs new file mode 100644 index 000000000000..2f7072aa82aa --- /dev/null +++ b/kani-driver/src/coverage/mod.rs @@ -0,0 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub mod cov_results; +pub mod cov_session; diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 992e226e45db..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)?; @@ -192,6 +188,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 +200,11 @@ impl KaniSession { Ok(()) } + + /// Show a coverage summary. + /// + /// This is just a placeholder for now. + fn show_coverage_summary(&self) -> Result<()> { + Ok(()) + } } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 3bb38ed1294c..d3bd697d2ea4 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 time::{format_description, OffsetDateTime}; use args::{check_is_valid, CargoKaniSubcommand}; use args_toml::join_args; @@ -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; @@ -129,6 +131,23 @@ 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 { + // 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)?; + } + session.print_final_summary(&results) } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 2bc0845cdb46..e0d2d2edd139 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,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, 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 +309,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) } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 120ab0a9e55c..11df998c820f 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-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, /// Memory predicate APIs. diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected new file mode 100644 index 000000000000..91142ebf94fc --- /dev/null +++ b/tests/coverage/abort/expected @@ -0,0 +1,13 @@ +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/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/assert/expected b/tests/coverage/assert/expected new file mode 100644 index 000000000000..46bb664cf6f5 --- /dev/null +++ b/tests/coverage/assert/expected @@ -0,0 +1,9 @@ +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/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/assert_eq/expected b/tests/coverage/assert_eq/expected new file mode 100644 index 000000000000..c2eee7adf803 --- /dev/null +++ b/tests/coverage/assert_eq/expected @@ -0,0 +1,8 @@ +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_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/assert_ne/expected b/tests/coverage/assert_ne/expected new file mode 100644 index 000000000000..c9b727da0f82 --- /dev/null +++ b/tests/coverage/assert_ne/expected @@ -0,0 +1,9 @@ +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/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/break/expected b/tests/coverage/break/expected new file mode 100644 index 000000000000..739735cdf1a2 --- /dev/null +++ b/tests/coverage/break/expected @@ -0,0 +1,13 @@ +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/break/main.rs similarity index 82% rename from tests/coverage/unreachable/break/main.rs rename to tests/coverage/break/main.rs index 4e795bd2a6ea..79f422a0c283 100644 --- a/tests/coverage/unreachable/break/main.rs +++ b/tests/coverage/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/compare/expected b/tests/coverage/compare/expected new file mode 100644 index 000000000000..153dbfa37d80 --- /dev/null +++ b/tests/coverage/compare/expected @@ -0,0 +1,11 @@ +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/compare/main.rs similarity index 73% rename from tests/coverage/unreachable/compare/main.rs rename to tests/coverage/compare/main.rs index a10fb84e29a8..43318ac0547e 100644 --- a/tests/coverage/unreachable/compare/main.rs +++ b/tests/coverage/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/contradiction/expected b/tests/coverage/contradiction/expected new file mode 100644 index 000000000000..db3676d7da15 --- /dev/null +++ b/tests/coverage/contradiction/expected @@ -0,0 +1,9 @@ +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/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/debug-assert/expected b/tests/coverage/debug-assert/expected new file mode 100644 index 000000000000..fbe57690d347 --- /dev/null +++ b/tests/coverage/debug-assert/expected @@ -0,0 +1,10 @@ +Source-based code coverage results: + +main.rs (main)\ + * 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 diff --git a/tests/coverage/debug-assert/main.rs b/tests/coverage/debug-assert/main.rs new file mode 100644 index 000000000000..a57a45c8c724 --- /dev/null +++ b/tests/coverage/debug-assert/main.rs @@ -0,0 +1,15 @@ +// 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 { + debug_assert!(i > 0, "This should fail and stop the execution"); + assert!(i == 0, "This should be unreachable"); + } +} diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected new file mode 100644 index 000000000000..f351005f4f22 --- /dev/null +++ b/tests/coverage/div-zero/expected @@ -0,0 +1,9 @@ +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/div-zero/test.rs similarity index 64% rename from tests/coverage/reachable/div-zero/reachable_pass/test.rs rename to tests/coverage/div-zero/test.rs index 766fb5a89d88..e858b57a12be 100644 --- a/tests/coverage/reachable/div-zero/reachable_pass/test.rs +++ b/tests/coverage/div-zero/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/early-return/expected b/tests/coverage/early-return/expected new file mode 100644 index 000000000000..53cde3abeaf8 --- /dev/null +++ b/tests/coverage/early-return/expected @@ -0,0 +1,12 @@ +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/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/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected new file mode 100644 index 000000000000..4e8382d10a6f --- /dev/null +++ b/tests/coverage/if-statement-multi/expected @@ -0,0 +1,11 @@ +Source-based code coverage results: + +test.rs (main)\ + * 21:1 - 26:2 COVERED + +test.rs (test_cov)\ + * 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/if-statement-multi/test.rs b/tests/coverage/if-statement-multi/test.rs new file mode 100644 index 000000000000..ac00dec3f451 --- /dev/null +++ b/tests/coverage/if-statement-multi/test.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --coverage -Zsource-coverage + +//! 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!"); +} + +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); +} diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected new file mode 100644 index 000000000000..b85b95de9c84 --- /dev/null +++ b/tests/coverage/if-statement/expected @@ -0,0 +1,14 @@ +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/if-statement/main.rs similarity index 78% rename from tests/coverage/unreachable/if-statement/main.rs rename to tests/coverage/if-statement/main.rs index f497cd76808e..c18d4dd4a5e4 100644 --- a/tests/coverage/unreachable/if-statement/main.rs +++ b/tests/coverage/if-statement/main.rs @@ -3,7 +3,7 @@ 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 { "Negative" 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/known_issues/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected new file mode 100644 index 000000000000..55f3235d7d24 --- /dev/null +++ b/tests/coverage/known_issues/assume_assert/expected @@ -0,0 +1,4 @@ +Source-based code coverage results: + +main.rs (check_assume_assert)\ + * 11:1 - 15:2 COVERED diff --git a/tests/coverage/known_issues/assume_assert/main.rs b/tests/coverage/known_issues/assume_assert/main.rs new file mode 100644 index 000000000000..90f26b2121fa --- /dev/null +++ b/tests/coverage/known_issues/assume_assert/main.rs @@ -0,0 +1,15 @@ +// 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. More details in +//! . + +#[kani::proof] +fn check_assume_assert() { + let a: u8 = kani::any(); + kani::assume(false); + assert!(a < 5); +} 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 72% rename from tests/coverage/unreachable/variant/main.rs rename to tests/coverage/known_issues/variant/main.rs index 76a589147bca..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, @@ -12,6 +14,7 @@ enum Direction { } fn print_direction(dir: Direction) { + // For some reason, `dir`'s span is reported as `UNCOVERED` too match dir { Direction::Up => println!("Going up!"), Direction::Down => println!("Going down!"), diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected new file mode 100644 index 000000000000..b5362147fed1 --- /dev/null +++ b/tests/coverage/multiple-harnesses/expected @@ -0,0 +1,37 @@ +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 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/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/overflow-failure/expected b/tests/coverage/overflow-failure/expected new file mode 100644 index 000000000000..db4f29d51336 --- /dev/null +++ b/tests/coverage/overflow-failure/expected @@ -0,0 +1,9 @@ +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/overflow-failure/test.rs similarity index 66% rename from tests/coverage/reachable/overflow/reachable_fail/test.rs rename to tests/coverage/overflow-failure/test.rs index d435612f2342..cd711f3aeb9e 100644 --- a/tests/coverage/reachable/overflow/reachable_fail/test.rs +++ b/tests/coverage/overflow-failure/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/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected new file mode 100644 index 000000000000..4d17761505eb --- /dev/null +++ b/tests/coverage/overflow-full-coverage/expected @@ -0,0 +1,9 @@ +Source-based code coverage results: + +test.rs (main)\ + * 12:1 - 17:2 COVERED + +test.rs (reduce)\ + * 7:1 - 8:16 COVERED\ + * 8:19 - 8:27 COVERED\ + * 8:37 - 8:38 COVERED diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/overflow-full-coverage/test.rs similarity index 62% rename from tests/coverage/reachable/overflow/reachable_pass/test.rs rename to tests/coverage/overflow-full-coverage/test.rs index 0b05874efc84..1c3467275b33 100644 --- a/tests/coverage/reachable/overflow/reachable_pass/test.rs +++ b/tests/coverage/overflow-full-coverage/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/assert-false/expected b/tests/coverage/reachable/assert-false/expected deleted file mode 100644 index 97ffbe1d96e4..000000000000 --- a/tests/coverage/reachable/assert-false/expected +++ /dev/null @@ -1,8 +0,0 @@ -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 diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs deleted file mode 100644 index 42563b1cd518..000000000000 --- a/tests/coverage/reachable/assert-false/main.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Check that the assert is reported as `PARTIAL` for having both `COVERED` and `UNCOVERED` coverage checks -fn any_bool() -> bool { - kani::any() -} - -#[kani::proof] -fn main() { - if any_bool() { - assert!(false); - } - - if any_bool() { - let s = "Fail with custom runtime message"; - assert!(false, "{}", s); - } -} diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected deleted file mode 100644 index 9d21185b3a83..000000000000 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ /dev/null @@ -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/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs deleted file mode 100644 index 72acca2b764c..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); // FULL: `x > 4` since `x = 5` - } -} diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected deleted file mode 100644 index fedfec8b2a1e..000000000000 --- a/tests/coverage/reachable/bounds/reachable_fail/expected +++ /dev/null @@ -1,4 +0,0 @@ -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 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 cebd78b2d5d9..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] // PARTIAL: `s[index]` is covered, but `index = 15` induces a failure -} // NONE: `index = 15` caused failure earlier - -#[kani::proof] -fn main() { - get(&[7, -83, 19], 15); -} // NONE: `index = 15` caused failure earlier diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected deleted file mode 100644 index c1ac77404680..000000000000 --- a/tests/coverage/reachable/div-zero/reachable_fail/expected +++ /dev/null @@ -1,4 +0,0 @@ -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 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 5f69005ee712..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 // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED` -} - -#[kani::proof] -fn main() { - div(678, 0); -} diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected deleted file mode 100644 index c7bfb5961c0b..000000000000 --- a/tests/coverage/reachable/div-zero/reachable_pass/expected +++ /dev/null @@ -1,4 +0,0 @@ -coverage/reachable/div-zero/reachable_pass/test.rs, 5, PARTIAL -coverage/reachable/div-zero/reachable_pass/test.rs, 6, FULL -coverage/reachable/div-zero/reachable_pass/test.rs, 10, FULL -coverage/reachable/div-zero/reachable_pass/test.rs, 11, FULL diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected deleted file mode 100644 index d45edcc37a63..000000000000 --- a/tests/coverage/reachable/overflow/reachable_fail/expected +++ /dev/null @@ -1,5 +0,0 @@ -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 diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected deleted file mode 100644 index 5becf2cd23e7..000000000000 --- a/tests/coverage/reachable/overflow/reachable_pass/expected +++ /dev/null @@ -1,7 +0,0 @@ -coverage/reachable/overflow/reachable_pass/test.rs, 8, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 9, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 13, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 14, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 15, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 16, FULL -coverage/reachable/overflow/reachable_pass/test.rs, 17, FULL diff --git a/tests/coverage/reachable/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 deleted file mode 100644 index 473b0f5a8d4d..000000000000 --- a/tests/coverage/unreachable/abort/expected +++ /dev/null @@ -1,7 +0,0 @@ -coverage/unreachable/abort/main.rs, 10, PARTIAL -coverage/unreachable/abort/main.rs, 11, FULL -coverage/unreachable/abort/main.rs, 13, FULL -coverage/unreachable/abort/main.rs, 15, FULL -coverage/unreachable/abort/main.rs, 17, NONE -coverage/unreachable/abort/main.rs, 20, NONE -coverage/unreachable/abort/main.rs, 21, NONE diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected deleted file mode 100644 index 9bc6d8faa4f9..000000000000 --- a/tests/coverage/unreachable/assert/expected +++ /dev/null @@ -1,7 +0,0 @@ -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 diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected deleted file mode 100644 index 9b13c3c96ded..000000000000 --- a/tests/coverage/unreachable/assert_eq/expected +++ /dev/null @@ -1,5 +0,0 @@ -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 diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected deleted file mode 100644 index f027f432e280..000000000000 --- a/tests/coverage/unreachable/assert_ne/expected +++ /dev/null @@ -1,6 +0,0 @@ -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 diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected deleted file mode 100644 index 8c1ae8a247d2..000000000000 --- a/tests/coverage/unreachable/assume_assert/expected +++ /dev/null @@ -1,4 +0,0 @@ -coverage/unreachable/assume_assert/main.rs, 5, FULL -coverage/unreachable/assume_assert/main.rs, 6, FULL -coverage/unreachable/assume_assert/main.rs, 7, NONE -coverage/unreachable/assume_assert/main.rs, 8, NONE diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs deleted file mode 100644 index c4d5d65c6640..000000000000 --- a/tests/coverage/unreachable/assume_assert/main.rs +++ /dev/null @@ -1,8 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -#[kani::proof] -fn check_assume_assert() { - let a: u8 = kani::any(); - kani::assume(false); - assert!(a < 5); -} diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected deleted file mode 100644 index 610372000a01..000000000000 --- a/tests/coverage/unreachable/bounds/expected +++ /dev/null @@ -1,4 +0,0 @@ -coverage/unreachable/bounds/test.rs, 5, PARTIAL -coverage/unreachable/bounds/test.rs, 6, FULL -coverage/unreachable/bounds/test.rs, 11, FULL -coverage/unreachable/bounds/test.rs, 12, FULL diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs deleted file mode 100644 index c37c9d0dcad6..000000000000 --- a/tests/coverage/unreachable/bounds/test.rs +++ /dev/null @@ -1,12 +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(&[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 deleted file mode 100644 index dcb013c50c3d..000000000000 --- a/tests/coverage/unreachable/break/expected +++ /dev/null @@ -1,9 +0,0 @@ -coverage/unreachable/break/main.rs, 5, PARTIAL -coverage/unreachable/break/main.rs, 6, FULL -coverage/unreachable/break/main.rs, 7, FULL -coverage/unreachable/break/main.rs, 11, NONE -coverage/unreachable/break/main.rs, 12, PARTIAL -coverage/unreachable/break/main.rs, 16, FULL -coverage/unreachable/break/main.rs, 17, FULL -coverage/unreachable/break/main.rs, 18, FULL -coverage/unreachable/break/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected deleted file mode 100644 index a2d296f0f9a3..000000000000 --- a/tests/coverage/unreachable/check_id/expected +++ /dev/null @@ -1,16 +0,0 @@ -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 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/compare/expected b/tests/coverage/unreachable/compare/expected deleted file mode 100644 index 6187e232cbe7..000000000000 --- a/tests/coverage/unreachable/compare/expected +++ /dev/null @@ -1,7 +0,0 @@ -coverage/unreachable/compare/main.rs, 6, PARTIAL -coverage/unreachable/compare/main.rs, 7, FULL -coverage/unreachable/compare/main.rs, 11, FULL -coverage/unreachable/compare/main.rs, 12, FULL -coverage/unreachable/compare/main.rs, 13, FULL -coverage/unreachable/compare/main.rs, 14, FULL -coverage/unreachable/compare/main.rs, 16, FULL diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected deleted file mode 100644 index 4234fc328e1e..000000000000 --- a/tests/coverage/unreachable/contradiction/expected +++ /dev/null @@ -1,7 +0,0 @@ -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 diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected deleted file mode 100644 index 25fdfed4c863..000000000000 --- a/tests/coverage/unreachable/debug-assert/expected +++ /dev/null @@ -1,4 +0,0 @@ -coverage/unreachable/debug-assert/main.rs, 6, PARTIAL -coverage/unreachable/debug-assert/main.rs, 7, PARTIAL -coverage/unreachable/debug-assert/main.rs, 8, NONE -coverage/unreachable/debug-assert/main.rs, 10, NONE diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs deleted file mode 100644 index ab3ab41e47d0..000000000000 --- a/tests/coverage/unreachable/debug-assert/main.rs +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[kani::proof] -fn main() { - for i in 0..4 { - debug_assert!(i > 0, "This should fail and stop the execution"); - assert!(i == 0, "This should be unreachable"); - } -} diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected 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 deleted file mode 100644 index 466c1775408b..000000000000 --- a/tests/coverage/unreachable/early-return/expected +++ /dev/null @@ -1,10 +0,0 @@ -coverage/unreachable/early-return/main.rs, 5, PARTIAL -coverage/unreachable/early-return/main.rs, 6, FULL -coverage/unreachable/early-return/main.rs, 7, FULL -coverage/unreachable/early-return/main.rs, 10, NONE -coverage/unreachable/early-return/main.rs, 11, PARTIAL -coverage/unreachable/early-return/main.rs, 15, FULL -coverage/unreachable/early-return/main.rs, 16, FULL -coverage/unreachable/early-return/main.rs, 17, FULL -coverage/unreachable/early-return/main.rs, 18, FULL -coverage/unreachable/early-return/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected deleted file mode 100644 index 8b481863a163..000000000000 --- a/tests/coverage/unreachable/if-statement/expected +++ /dev/null @@ -1,10 +0,0 @@ -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 diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected deleted file mode 100644 index 17a52666c08d..000000000000 --- a/tests/coverage/unreachable/multiple-harnesses/expected +++ /dev/null @@ -1,39 +0,0 @@ -Checking harness fully_covered... -coverage/unreachable/multiple-harnesses/main.rs, 5, FULL -coverage/unreachable/multiple-harnesses/main.rs, 7, FULL -coverage/unreachable/multiple-harnesses/main.rs, 8, FULL -coverage/unreachable/multiple-harnesses/main.rs, 9, FULL -coverage/unreachable/multiple-harnesses/main.rs, 11, FULL -coverage/unreachable/multiple-harnesses/main.rs, 13, FULL -coverage/unreachable/multiple-harnesses/main.rs, 14, FULL -coverage/unreachable/multiple-harnesses/main.rs, 15, FULL -coverage/unreachable/multiple-harnesses/main.rs, 17, FULL -coverage/unreachable/multiple-harnesses/main.rs, 20, FULL -coverage/unreachable/multiple-harnesses/main.rs, 21, FULL -coverage/unreachable/multiple-harnesses/main.rs, 23, FULL -coverage/unreachable/multiple-harnesses/main.rs, 26, FULL -coverage/unreachable/multiple-harnesses/main.rs, 40, FULL -coverage/unreachable/multiple-harnesses/main.rs, 41, FULL -coverage/unreachable/multiple-harnesses/main.rs, 42, FULL -coverage/unreachable/multiple-harnesses/main.rs, 43, FULL -coverage/unreachable/multiple-harnesses/main.rs, 44, FULL - -Checking harness mostly_covered... -coverage/unreachable/multiple-harnesses/main.rs, 5, FULL -coverage/unreachable/multiple-harnesses/main.rs, 7, FULL -coverage/unreachable/multiple-harnesses/main.rs, 8, FULL -coverage/unreachable/multiple-harnesses/main.rs, 9, FULL -coverage/unreachable/multiple-harnesses/main.rs, 11, FULL -coverage/unreachable/multiple-harnesses/main.rs, 13, FULL -coverage/unreachable/multiple-harnesses/main.rs, 14, FULL -coverage/unreachable/multiple-harnesses/main.rs, 15, FULL -coverage/unreachable/multiple-harnesses/main.rs, 17, FULL -coverage/unreachable/multiple-harnesses/main.rs, 20, FULL -coverage/unreachable/multiple-harnesses/main.rs, 21, FULL -coverage/unreachable/multiple-harnesses/main.rs, 23, NONE -coverage/unreachable/multiple-harnesses/main.rs, 26, FULL -coverage/unreachable/multiple-harnesses/main.rs, 31, FULL -coverage/unreachable/multiple-harnesses/main.rs, 32, FULL -coverage/unreachable/multiple-harnesses/main.rs, 33, FULL -coverage/unreachable/multiple-harnesses/main.rs, 34, FULL -coverage/unreachable/multiple-harnesses/main.rs, 35, FULL diff --git a/tests/coverage/unreachable/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 deleted file mode 100644 index 624aa520edc9..000000000000 --- a/tests/coverage/unreachable/tutorial_unreachable/expected +++ /dev/null @@ -1,5 +0,0 @@ -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 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 8fa3ec8b870f..000000000000 --- a/tests/coverage/unreachable/variant/expected +++ /dev/null @@ -1,10 +0,0 @@ -coverage/unreachable/variant/main.rs, 15, FULL -coverage/unreachable/variant/main.rs, 16, NONE -coverage/unreachable/variant/main.rs, 17, NONE -coverage/unreachable/variant/main.rs, 18, FULL -coverage/unreachable/variant/main.rs, 19, NONE -coverage/unreachable/variant/main.rs, 21, NONE -coverage/unreachable/variant/main.rs, 23, FULL -coverage/unreachable/variant/main.rs, 27, FULL -coverage/unreachable/variant/main.rs, 28, FULL -coverage/unreachable/variant/main.rs, 29, FULL diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected deleted file mode 100644 index e47941f17db2..000000000000 --- a/tests/coverage/unreachable/vectors/expected +++ /dev/null @@ -1,6 +0,0 @@ -coverage/unreachable/vectors/main.rs, 8, FULL -coverage/unreachable/vectors/main.rs, 11, FULL -coverage/unreachable/vectors/main.rs, 13, PARTIAL -coverage/unreachable/vectors/main.rs, 15, NONE -coverage/unreachable/vectors/main.rs, 17, FULL -coverage/unreachable/vectors/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs 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/unreachable/while-loop-break/expected deleted file mode 100644 index dc66d3e823d3..000000000000 --- a/tests/coverage/unreachable/while-loop-break/expected +++ /dev/null @@ -1,11 +0,0 @@ -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 diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected new file mode 100644 index 000000000000..34afef9ee12c --- /dev/null +++ b/tests/coverage/while-loop-break/expected @@ -0,0 +1,13 @@ +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/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 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..0a422280e51d --- /dev/null +++ b/tests/ui/save-coverage-results/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); +} 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);