From db42ee996ade70116a75b291072a7c1189a3d913 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 28 Jul 2023 16:42:28 -0400 Subject: [PATCH 1/4] Line coverage reports (#2609) Co-authored-by: jaisnan Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/assert.rs | 30 +++++- .../codegen_cprover_gotoc/codegen/block.rs | 38 ++++++- .../codegen/intrinsic.rs | 2 +- kani-compiler/src/kani_compiler.rs | 2 + kani-compiler/src/kani_queries/mod.rs | 1 + kani-compiler/src/parser.rs | 9 ++ kani-driver/src/args/common.rs | 2 + kani-driver/src/args/mod.rs | 14 +++ kani-driver/src/call_cbmc.rs | 17 ++- kani-driver/src/call_single_file.rs | 4 + kani-driver/src/cbmc_output_parser.rs | 14 ++- kani-driver/src/cbmc_property_renderer.rs | 102 +++++++++++++++++- kani-driver/src/harness_runner.rs | 6 +- scripts/kani-regression.sh | 1 + .../coverage/reachable/assert-false/expected | 8 ++ tests/coverage/reachable/assert-false/main.rs | 19 ++++ .../reachable/assert/reachable_pass/expected | 4 + .../reachable/assert/reachable_pass/test.rs | 10 ++ .../reachable/bounds/reachable_fail/expected | 4 + .../reachable/bounds/reachable_fail/test.rs | 11 ++ .../div-zero/reachable_fail/expected | 4 + .../reachable/div-zero/reachable_fail/test.rs | 11 ++ .../div-zero/reachable_pass/expected | 4 + .../reachable/div-zero/reachable_pass/test.rs | 11 ++ .../overflow/reachable_fail/expected | 5 + .../reachable/overflow/reachable_fail/test.rs | 15 +++ .../overflow/reachable_pass/expected | 7 ++ .../reachable/overflow/reachable_pass/test.rs | 17 +++ .../rem-zero/reachable_fail/expected | 4 + .../reachable/rem-zero/reachable_fail/test.rs | 11 ++ .../rem-zero/reachable_pass/expected | 4 + .../reachable/rem-zero/reachable_pass/test.rs | 11 ++ tests/coverage/unreachable/abort/expected | 7 ++ tests/coverage/unreachable/abort/main.rs | 21 ++++ tests/coverage/unreachable/assert/expected | 7 ++ tests/coverage/unreachable/assert/test.rs | 18 ++++ tests/coverage/unreachable/assert_eq/expected | 5 + tests/coverage/unreachable/assert_eq/test.rs | 11 ++ tests/coverage/unreachable/assert_ne/expected | 6 ++ tests/coverage/unreachable/assert_ne/test.rs | 14 +++ .../unreachable/assume_assert/expected | 4 + .../unreachable/assume_assert/main.rs | 8 ++ tests/coverage/unreachable/bounds/expected | 4 + tests/coverage/unreachable/bounds/test.rs | 12 +++ tests/coverage/unreachable/break/expected | 9 ++ tests/coverage/unreachable/break/main.rs | 19 ++++ tests/coverage/unreachable/check_id/expected | 16 +++ tests/coverage/unreachable/check_id/main.rs | 25 +++++ tests/coverage/unreachable/compare/expected | 7 ++ tests/coverage/unreachable/compare/main.rs | 16 +++ .../unreachable/contradiction/expected | 6 ++ .../unreachable/contradiction/main.rs | 13 +++ .../unreachable/debug-assert/expected | 4 + .../coverage/unreachable/debug-assert/main.rs | 10 ++ tests/coverage/unreachable/divide/expected | 7 ++ tests/coverage/unreachable/divide/main.rs | 19 ++++ .../unreachable/early-return/expected | 10 ++ .../coverage/unreachable/early-return/main.rs | 19 ++++ .../unreachable/if-statement/expected | 10 ++ .../coverage/unreachable/if-statement/main.rs | 20 ++++ .../unreachable/multiple-harnesses/expected | 39 +++++++ .../unreachable/multiple-harnesses/main.rs | 44 ++++++++ tests/coverage/unreachable/return/expected | 8 ++ tests/coverage/unreachable/return/main.rs | 17 +++ .../unreachable/tutorial_unreachable/expected | 5 + .../unreachable/tutorial_unreachable/main.rs | 11 ++ tests/coverage/unreachable/variant/expected | 10 ++ tests/coverage/unreachable/variant/main.rs | 29 +++++ tests/coverage/unreachable/vectors/expected | 6 ++ tests/coverage/unreachable/vectors/main.rs | 19 ++++ .../unreachable/while-loop-break/expected | 11 ++ .../unreachable/while-loop-break/main.rs | 23 ++++ tools/compiletest/src/common.rs | 3 + tools/compiletest/src/main.rs | 2 +- tools/compiletest/src/runtest.rs | 28 ++++- 75 files changed, 967 insertions(+), 17 deletions(-) create mode 100644 tests/coverage/reachable/assert-false/expected create mode 100644 tests/coverage/reachable/assert-false/main.rs create mode 100644 tests/coverage/reachable/assert/reachable_pass/expected create mode 100644 tests/coverage/reachable/assert/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/bounds/reachable_fail/expected create mode 100644 tests/coverage/reachable/bounds/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/div-zero/reachable_fail/expected create mode 100644 tests/coverage/reachable/div-zero/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/div-zero/reachable_pass/expected create mode 100644 tests/coverage/reachable/div-zero/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/overflow/reachable_fail/expected create mode 100644 tests/coverage/reachable/overflow/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/overflow/reachable_pass/expected create mode 100644 tests/coverage/reachable/overflow/reachable_pass/test.rs create mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/expected create mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/test.rs create mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/expected create mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/test.rs create mode 100644 tests/coverage/unreachable/abort/expected create mode 100644 tests/coverage/unreachable/abort/main.rs create mode 100644 tests/coverage/unreachable/assert/expected create mode 100644 tests/coverage/unreachable/assert/test.rs create mode 100644 tests/coverage/unreachable/assert_eq/expected create mode 100644 tests/coverage/unreachable/assert_eq/test.rs create mode 100644 tests/coverage/unreachable/assert_ne/expected create mode 100644 tests/coverage/unreachable/assert_ne/test.rs create mode 100644 tests/coverage/unreachable/assume_assert/expected create mode 100644 tests/coverage/unreachable/assume_assert/main.rs create mode 100644 tests/coverage/unreachable/bounds/expected create mode 100644 tests/coverage/unreachable/bounds/test.rs create mode 100644 tests/coverage/unreachable/break/expected create mode 100644 tests/coverage/unreachable/break/main.rs create mode 100644 tests/coverage/unreachable/check_id/expected create mode 100644 tests/coverage/unreachable/check_id/main.rs create mode 100644 tests/coverage/unreachable/compare/expected create mode 100644 tests/coverage/unreachable/compare/main.rs create mode 100644 tests/coverage/unreachable/contradiction/expected create mode 100644 tests/coverage/unreachable/contradiction/main.rs create mode 100644 tests/coverage/unreachable/debug-assert/expected create mode 100644 tests/coverage/unreachable/debug-assert/main.rs create mode 100644 tests/coverage/unreachable/divide/expected create mode 100644 tests/coverage/unreachable/divide/main.rs create mode 100644 tests/coverage/unreachable/early-return/expected create mode 100644 tests/coverage/unreachable/early-return/main.rs create mode 100644 tests/coverage/unreachable/if-statement/expected create mode 100644 tests/coverage/unreachable/if-statement/main.rs create mode 100644 tests/coverage/unreachable/multiple-harnesses/expected create mode 100644 tests/coverage/unreachable/multiple-harnesses/main.rs create mode 100644 tests/coverage/unreachable/return/expected create mode 100644 tests/coverage/unreachable/return/main.rs create mode 100644 tests/coverage/unreachable/tutorial_unreachable/expected create mode 100644 tests/coverage/unreachable/tutorial_unreachable/main.rs create mode 100644 tests/coverage/unreachable/variant/expected create mode 100644 tests/coverage/unreachable/variant/main.rs create mode 100644 tests/coverage/unreachable/vectors/expected create mode 100644 tests/coverage/unreachable/vectors/main.rs create mode 100644 tests/coverage/unreachable/while-loop-break/expected create mode 100644 tests/coverage/unreachable/while-loop-break/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index bcf452602930..27203c7218c6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -29,7 +29,7 @@ use tracing::debug; /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover) /// /// Each property class should justify its existence with a note about the special handling it recieves. -#[derive(Debug, Clone, EnumString, AsRefStr)] +#[derive(Debug, Clone, EnumString, AsRefStr, PartialEq)] #[strum(serialize_all = "snake_case")] pub enum PropertyClass { /// Overflow panics that can be generated by Intrisics. @@ -45,6 +45,19 @@ pub enum PropertyClass { /// /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure. Cover, + /// The class of checks used for code coverage instrumentation. Only needed + /// when working on coverage-related features. + /// + /// Do not mistake with `Cover`, they are different: + /// - `CodeCoverage` checks have a fixed condition (`false`) and description. + /// - `CodeCoverage` checks are filtered out from verification results and + /// postprocessed to build coverage reports. + /// - `Cover` checks can be added by users (using the `kani::cover` macro), + /// while `CodeCoverage` checks are not exposed to users (i.e., they are + /// automatically added if running with the coverage option). + /// + /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure. + CodeCoverage, /// Ordinary (Rust) assertions and panics. /// /// SPECIAL BEHAVIOR: These assertion failures should be observable during normal execution of Rust code. @@ -134,6 +147,21 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) } + /// Generate a cover statement for code coverage reports. + pub fn codegen_coverage(&self, span: Span) -> Stmt { + let loc = self.codegen_caller_span(&Some(span)); + // Should use Stmt::cover, but currently this doesn't work with CBMC + // unless it is run with '--cover cover' (see + // https://github.com/diffblue/cbmc/issues/6613). So for now use + // `assert(false)`. + self.codegen_assert( + Expr::bool_false(), + PropertyClass::CodeCoverage, + "code coverage for location", + loc, + ) + } + // The above represent the basic operations we can perform w.r.t. assert/assume/cover // Below are various helper functions for constructing the above more easily. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index b015be5b401c..bc6738e8ead0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -16,25 +16,55 @@ impl<'tcx> GotocCtx<'tcx> { debug!(?bb, "Codegen basicblock"); self.current_fn_mut().set_current_bb(bb); let label: String = self.current_fn().find_label(&bb); + let check_coverage = self.queries.check_coverage; // the first statement should be labelled. if there is no statements, then the // terminator should be labelled. match bbd.statements.len() { 0 => { let term = bbd.terminator(); let tcode = self.codegen_terminator(term); - self.current_fn_mut().push_onto_block(tcode.with_label(label)); + // When checking coverage, the `coverage` check should be + // labelled instead. + if check_coverage { + let span = term.source_info.span; + let cover = self.codegen_coverage(span); + self.current_fn_mut().push_onto_block(cover.with_label(label)); + self.current_fn_mut().push_onto_block(tcode); + } else { + self.current_fn_mut().push_onto_block(tcode.with_label(label)); + } } _ => { let stmt = &bbd.statements[0]; let scode = self.codegen_statement(stmt); - self.current_fn_mut().push_onto_block(scode.with_label(label)); + // When checking coverage, the `coverage` check should be + // labelled instead. + if check_coverage { + let span = stmt.source_info.span; + let cover = self.codegen_coverage(span); + self.current_fn_mut().push_onto_block(cover.with_label(label)); + self.current_fn_mut().push_onto_block(scode); + } else { + self.current_fn_mut().push_onto_block(scode.with_label(label)); + } for s in &bbd.statements[1..] { + if check_coverage { + let span = s.source_info.span; + let cover = self.codegen_coverage(span); + self.current_fn_mut().push_onto_block(cover); + } let stmt = self.codegen_statement(s); self.current_fn_mut().push_onto_block(stmt); } - let term = self.codegen_terminator(bbd.terminator()); - self.current_fn_mut().push_onto_block(term); + let term = bbd.terminator(); + if check_coverage { + let span = term.source_info.span; + let cover = self.codegen_coverage(span); + self.current_fn_mut().push_onto_block(cover); + } + let tcode = self.codegen_terminator(term); + self.current_fn_mut().push_onto_block(tcode); } } self.current_fn_mut().reset_current_bb(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4bd5566f9d7c..af06c456a7b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -188,7 +188,7 @@ impl<'tcx> GotocCtx<'tcx> { let a = fargs.remove(0); let b = fargs.remove(0); let div_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone()); - let div_overflow_check = self.codegen_assert( + let div_overflow_check = self.codegen_assert_assume( div_does_not_overflow, PropertyClass::ArithmeticOverflow, format!("attempt to compute {} which would overflow", intrinsic).as_str(), diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 2a5e4c188578..ef766c562941 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -349,6 +349,7 @@ impl Callbacks for KaniCompiler { let queries = &mut (*self.queries.lock().unwrap()); queries.emit_vtable_restrictions = matches.get_flag(parser::RESTRICT_FN_PTRS); queries.check_assertion_reachability = matches.get_flag(parser::ASSERTION_REACH_CHECKS); + queries.check_coverage = matches.get_flag(parser::COVERAGE_CHECKS); queries.output_pretty_json = matches.get_flag(parser::PRETTY_OUTPUT_FILES); queries.ignore_global_asm = matches.get_flag(parser::IGNORE_GLOBAL_ASM); queries.write_json_symtab = @@ -364,6 +365,7 @@ impl Callbacks for KaniCompiler { { queries.stubbing_enabled = true; } + debug!(?queries, "config end"); } } diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index b8446bb7a023..44573bf124d8 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -28,6 +28,7 @@ pub enum ReachabilityType { #[derive(Debug, Default, Clone)] pub struct QueryDb { pub check_assertion_reachability: bool, + pub check_coverage: bool, pub emit_vtable_restrictions: bool, pub output_pretty_json: bool, pub ignore_global_asm: bool, diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index 2ff81a90bc7c..a947fdc61eaa 100644 --- a/kani-compiler/src/parser.rs +++ b/kani-compiler/src/parser.rs @@ -28,6 +28,9 @@ pub const RESTRICT_FN_PTRS: &str = "restrict-vtable-fn-ptrs"; /// Option name used to enable assertion reachability checks. pub const ASSERTION_REACH_CHECKS: &str = "assertion-reach-checks"; +/// Option name used to enable coverage checks. +pub const COVERAGE_CHECKS: &str = "coverage-checks"; + /// Option name used to use json pretty-print for output files. pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files"; @@ -98,6 +101,12 @@ pub fn parser() -> Command { .help("Check the reachability of every assertion.") .action(ArgAction::SetTrue), ) + .arg( + Arg::new(COVERAGE_CHECKS) + .long(COVERAGE_CHECKS) + .help("Check the reachability of every statement.") + .action(ArgAction::SetTrue), + ) .arg( Arg::new(REACHABILITY) .long(REACHABILITY) diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index 746482c6985e..a4325ca610fa 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -44,6 +44,8 @@ pub enum UnstableFeatures { ConcretePlayback, /// Enable Kani's unstable async library. AsyncLib, + /// Enable line coverage instrumentation/reports + LineCoverage, } impl ValidateArgs for CommonArgs { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 31cae95e2a61..626f2d81be93 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -300,6 +300,10 @@ pub struct VerificationArgs { )] pub enable_stubbing: bool, + /// Enable Kani coverage output alongside verification result + #[arg(long, hide_short_help = true)] + pub coverage: bool, + /// Arguments to pass down to Cargo #[command(flatten)] pub cargo: CargoCommonArgs, @@ -640,6 +644,16 @@ impl ValidateArgs for VerificationArgs { } } + if self.coverage + && !self.common_args.unstable_features.contains(&UnstableFeatures::LineCoverage) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `--coverage` argument is unstable and requires `-Z \ + line-coverage` to be used.", + )); + } + Ok(()) } } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index daddfdf62f1c..96770d562e79 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -13,7 +13,7 @@ use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput, }; -use crate::cbmc_property_renderer::{format_result, kani_cbmc_output_filter}; +use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::session::KaniSession; #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -303,14 +303,23 @@ impl VerificationResult { } } - pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String { + pub fn render( + &self, + output_format: &OutputFormat, + should_panic: bool, + coverage_mode: bool, + ) -> String { match &self.results { Ok(results) => { let status = self.status; let failed_properties = self.failed_properties; let show_checks = matches!(output_format, OutputFormat::Regular); - let mut result = - format_result(results, status, should_panic, failed_properties, show_checks); + + let mut result = if coverage_mode { + format_coverage(results, status, should_panic, failed_properties, show_checks) + } else { + format_result(results, status, should_panic, failed_properties, show_checks) + }; writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap(); result } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index caf3dd7339a3..1522071fdefd 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -96,6 +96,10 @@ impl KaniSession { flags.push("--enable-stubbing".into()); } + if self.args.coverage { + flags.push("--coverage-checks".into()); + } + flags.extend( self.args .common_args diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 70e13b7dda06..8bdd45034190 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -96,11 +96,17 @@ pub struct PropertyId { impl Property { const COVER_PROPERTY_CLASS: &str = "cover"; + const COVERAGE_PROPERTY_CLASS: &str = "code_coverage"; pub fn property_class(&self) -> String { self.property_id.class.clone() } + // Returns true if this is a code_coverage check + pub fn is_code_coverage_property(&self) -> bool { + self.property_id.class == Self::COVERAGE_PROPERTY_CLASS + } + /// Returns true if this is a cover property pub fn is_cover_property(&self) -> bool { self.property_id.class == Self::COVER_PROPERTY_CLASS @@ -322,11 +328,13 @@ impl std::fmt::Display for TraceData { #[serde(rename_all = "UPPERCASE")] pub enum CheckStatus { Failure, - Satisfied, // for cover properties only + Covered, // for `code_coverage` properties only + Satisfied, // for `cover` properties only Success, Undetermined, Unreachable, - Unsatisfiable, // for cover properties only + Uncovered, // for `code_coverage` properties only + Unsatisfiable, // for `cover` properties only } impl std::fmt::Display for CheckStatus { @@ -334,6 +342,8 @@ impl std::fmt::Display for CheckStatus { let check_str = match self { CheckStatus::Satisfied => style("SATISFIED").green(), CheckStatus::Success => style("SUCCESS").green(), + CheckStatus::Covered => style("COVERED").green(), + CheckStatus::Uncovered => style("UNCOVERED").red(), CheckStatus::Failure => style("FAILURE").red(), CheckStatus::Unreachable => style("UNREACHABLE").yellow(), CheckStatus::Undetermined => style("UNDETERMINED").yellow(), diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 8da67dae7ab1..be788c5d1c0c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -8,7 +8,8 @@ use console::style; use once_cell::sync::Lazy; use regex::Regex; use rustc_demangle::demangle; -use std::collections::HashMap; +use std::collections::{BTreeMap, HashMap}; +use strum_macros::{AsRefStr, Display}; type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>; @@ -149,6 +150,15 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { map }); +#[derive(PartialEq, Eq, AsRefStr, Clone, Copy, Display)] +#[strum(serialize_all = "UPPERCASE")] +// The status of coverage reported by Kani +enum CoverageStatus { + Full, + Partial, + None, +} + const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani"; const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop"; const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion"; @@ -421,6 +431,72 @@ pub fn format_result( result_str } +/// Separate checks into coverage and non-coverage based on property class and format them separately for --coverage. We report both verification and processed coverage +/// results +pub fn format_coverage( + properties: &[Property], + status: VerificationStatus, + should_panic: bool, + failed_properties: FailedProperties, + show_checks: bool, +) -> String { + let (coverage_checks, non_coverage_checks): (Vec, Vec) = + properties.iter().cloned().partition(|x| x.property_class() == "code_coverage"); + + let verification_output = + format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks); + let coverage_output = format_result_coverage(&coverage_checks); + let result = format!("{}\n{}", verification_output, coverage_output); + + result +} + +/// Generate coverage result from all coverage properties (i.e., checks with `code_coverage` property class). +/// Loops through each of the checks with the `code_coverage` property class on a line and gives: +/// - A status `FULL` if all checks pertaining to a line number are `COVERED` +/// - A status `NONE` if all checks related to a line are `UNCOVERED` +/// - Otherwise (i.e., if the line contains both) it reports `PARTIAL`. +/// +/// Used when the user requests coverage information with `--coverage`. +/// Output is tested through the `coverage-based` testing suite, not the regular +/// `expected` suite. +fn format_result_coverage(properties: &[Property]) -> String { + let mut formatted_output = String::new(); + formatted_output.push_str("\nCoverage Results:\n"); + + let mut coverage_results: BTreeMap> = + BTreeMap::default(); + for prop in properties { + let src = prop.source_location.clone(); + let file_entries = coverage_results.entry(src.file.unwrap()).or_default(); + let check_status = if prop.status == CheckStatus::Covered { + CoverageStatus::Full + } else { + CoverageStatus::None + }; + + // Create Map> + file_entries + .entry(src.line.unwrap().parse().unwrap()) + .and_modify(|line_status| { + if *line_status != check_status { + *line_status = CoverageStatus::Partial + } + }) + .or_insert(check_status); + } + + // Create formatted string that is returned to the user as output + for (file, checks) in coverage_results.iter() { + for (line_number, coverage_status) in checks { + formatted_output.push_str(&format!("{}, {}, {}\n", file, line_number, coverage_status)); + } + formatted_output.push('\n'); + } + + formatted_output +} + /// Attempts to build a message for a failed property with as much detailed /// information on the source location as possible. fn build_failure_message(description: String, trace: &Option>) -> String { @@ -512,7 +588,8 @@ pub fn postprocess_result(properties: Vec, extra_ptr_checks: bool) -> let updated_properties = update_properties_with_reach_status(properties_filtered, has_fundamental_failures); - update_results_of_cover_checks(updated_properties) + let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties); + update_results_of_cover_checks(results_after_code_coverage) } /// Determines if there is property with status `FAILURE` and the given description @@ -613,6 +690,27 @@ fn update_properties_with_reach_status( properties } +/// Update the results of `code_coverage` (NOT `cover`) properties. +/// - `SUCCESS` -> `UNCOVERED` +/// - `FAILURE` -> `COVERED` +/// Note that these statuses are intermediate statuses that aren't reported to +/// users but rather internally consumed and reported finally as `PARTIAL`, `FULL` +/// or `NONE` based on aggregated line coverage results. +fn update_results_of_code_covererage_checks(mut properties: Vec) -> Vec { + for prop in properties.iter_mut() { + if prop.is_code_coverage_property() { + prop.status = match prop.status { + CheckStatus::Success => CheckStatus::Uncovered, + CheckStatus::Failure => CheckStatus::Covered, + _ => unreachable!( + "status for coverage checks should be either `SUCCESS` or `FAILURE` prior to postprocessing" + ), + }; + } + } + properties +} + /// Update the results of cover properties. /// We encode cover(cond) as assert(!cond), so if the assertion /// fails, then the cover property is satisfied and vice versa. diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index fdafa8a5c18b..fa1aef3d763a 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -96,7 +96,11 @@ impl KaniSession { if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { println!( "{}", - result.render(&self.args.output_format, harness.attributes.should_panic) + result.render( + &self.args.output_format, + harness.attributes.should_panic, + self.args.coverage + ) ); } self.gen_and_add_concrete_playback(harness, &mut result)?; diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index fd04b579deb3..01afd6e2de59 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -38,6 +38,7 @@ cargo test -p kani_metadata # Declare testing suite information (suite and mode) TESTS=( "script-based-pre exec" + "coverage coverage-based" "kani kani" "expected expected" "ui expected" diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected new file mode 100644 index 000000000000..7a9fef1ca77c --- /dev/null +++ b/tests/coverage/reachable/assert-false/expected @@ -0,0 +1,8 @@ +coverage/reachable/assert-false/main.rs, 6, FULL +coverage/reachable/assert-false/main.rs, 7, FULL +coverage/reachable/assert-false/main.rs, 11, FULL +coverage/reachable/assert-false/main.rs, 12, FULL +coverage/reachable/assert-false/main.rs, 15, FULL +coverage/reachable/assert-false/main.rs, 16, FULL +coverage/reachable/assert-false/main.rs, 17, PARTIAL +coverage/reachable/assert-false/main.rs, 19, FULL diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs new file mode 100644 index 000000000000..42563b1cd518 --- /dev/null +++ b/tests/coverage/reachable/assert-false/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the assert is reported as `PARTIAL` for having both `COVERED` and `UNCOVERED` coverage checks +fn any_bool() -> bool { + kani::any() +} + +#[kani::proof] +fn main() { + if any_bool() { + assert!(false); + } + + if any_bool() { + let s = "Fail with custom runtime message"; + assert!(false, "{}", s); + } +} diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected new file mode 100644 index 000000000000..67ae085a3e83 --- /dev/null +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/assert/reachable_pass/test.rs, 6, FULL +coverage/reachable/assert/reachable_pass/test.rs, 7, FULL +coverage/reachable/assert/reachable_pass/test.rs, 8, FULL +coverage/reachable/assert/reachable_pass/test.rs, 10, FULL diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs new file mode 100644 index 000000000000..72acca2b764c --- /dev/null +++ b/tests/coverage/reachable/assert/reachable_pass/test.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: u32 = kani::any_where(|val| *val == 5); + if x > 3 { + assert!(x > 4); // FULL: `x > 4` since `x = 5` + } +} diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected new file mode 100644 index 000000000000..af2f30e51fe2 --- /dev/null +++ b/tests/coverage/reachable/bounds/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE +coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL +coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs new file mode 100644 index 000000000000..cebd78b2d5d9 --- /dev/null +++ b/tests/coverage/reachable/bounds/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn get(s: &[i16], index: usize) -> i16 { + s[index] // PARTIAL: `s[index]` is covered, but `index = 15` induces a failure +} // NONE: `index = 15` caused failure earlier + +#[kani::proof] +fn main() { + get(&[7, -83, 19], 15); +} // NONE: `index = 15` caused failure earlier diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected new file mode 100644 index 000000000000..1ec1abefffd8 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE +coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..5f69005ee712 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn div(x: u16, y: u16) -> u16 { + x / y // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED` +} + +#[kani::proof] +fn main() { + div(678, 0); +} diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected new file mode 100644 index 000000000000..c7bfb5961c0b --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/div-zero/reachable_pass/test.rs, 5, PARTIAL +coverage/reachable/div-zero/reachable_pass/test.rs, 6, FULL +coverage/reachable/div-zero/reachable_pass/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_pass/test.rs, 11, FULL diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/reachable/div-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..766fb5a89d88 --- /dev/null +++ b/tests/coverage/reachable/div-zero/reachable_pass/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn div(x: u16, y: u16) -> u16 { + if y != 0 { x / y } else { 0 } // PARTIAL: some cases are `COVERED`, others are not +} + +#[kani::proof] +fn main() { + div(11, 3); +} diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected new file mode 100644 index 000000000000..f20826fb1a8e --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_fail/expected @@ -0,0 +1,5 @@ +coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL +coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/reachable/overflow/reachable_fail/test.rs new file mode 100644 index 000000000000..d435612f2342 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_fail/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani reports the correct coverage results in the case of an +//! arithmetic overflow failure (caused by the second call to `cond_reduce`). + +fn cond_reduce(thresh: u32, x: u32) -> u32 { + if x > thresh { x - 50 } else { x } // PARTIAL: some cases are `COVERED`, others are not +} + +#[kani::proof] +fn main() { + cond_reduce(60, 70); + cond_reduce(40, 42); +} // NONE: Caused by the arithmetic overflow failure from the second call to `cond_reduce` diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected new file mode 100644 index 000000000000..5becf2cd23e7 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_pass/expected @@ -0,0 +1,7 @@ +coverage/reachable/overflow/reachable_pass/test.rs, 8, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 9, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 13, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 14, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 15, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 16, FULL +coverage/reachable/overflow/reachable_pass/test.rs, 17, FULL diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/reachable/overflow/reachable_pass/test.rs new file mode 100644 index 000000000000..0b05874efc84 --- /dev/null +++ b/tests/coverage/reachable/overflow/reachable_pass/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani reports the correct coverage results (`FULL` for all lines) +//! in a case where arithmetic overflow failures are prevented. + +fn reduce(x: u32) -> u32 { + if x > 1000 { x - 1000 } else { x } +} + +#[kani::proof] +fn main() { + reduce(7); + reduce(33); + reduce(728); + reduce(1079); +} diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected new file mode 100644 index 000000000000..f7fa6ed7efeb --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected @@ -0,0 +1,4 @@ +coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL +coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE +coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..400c7e02340b --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn rem(x: u16, y: u16) -> u16 { + x % y // PARTIAL: `x % y` is covered but induces a division failure +} // NONE: Caused by division failure earlier + +#[kani::proof] +fn main() { + rem(678, 0); +} // NONE: Caused by division failure earlier diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/expected b/tests/coverage/reachable/rem-zero/reachable_pass/expected new file mode 100644 index 000000000000..f3d5934d785d --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_pass/expected @@ -0,0 +1,4 @@ +coverage/reachable/rem-zero/reachable_pass/test.rs, 5, PARTIAL +coverage/reachable/rem-zero/reachable_pass/test.rs, 6, FULL +coverage/reachable/rem-zero/reachable_pass/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_pass/test.rs, 11, FULL diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..41ed28f7b903 --- /dev/null +++ b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn rem(x: u16, y: u16) -> u16 { + if y != 0 { x % y } else { 0 } +} + +#[kani::proof] +fn main() { + rem(11, 3); +} diff --git a/tests/coverage/unreachable/abort/expected b/tests/coverage/unreachable/abort/expected new file mode 100644 index 000000000000..473b0f5a8d4d --- /dev/null +++ b/tests/coverage/unreachable/abort/expected @@ -0,0 +1,7 @@ +coverage/unreachable/abort/main.rs, 10, PARTIAL +coverage/unreachable/abort/main.rs, 11, FULL +coverage/unreachable/abort/main.rs, 13, FULL +coverage/unreachable/abort/main.rs, 15, FULL +coverage/unreachable/abort/main.rs, 17, NONE +coverage/unreachable/abort/main.rs, 20, NONE +coverage/unreachable/abort/main.rs, 21, NONE diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs new file mode 100644 index 000000000000..2941ec126f3c --- /dev/null +++ b/tests/coverage/unreachable/abort/main.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Test that the abort() function is respected and nothing beyond it will execute. + +use std::process; + +#[kani::proof] +fn main() { + for i in 0..4 { + if i == 1 { + // This comes first and it should be reachable. + process::abort(); + } + if i == 2 { + // This should never happen. + process::exit(1); + } + } + assert!(false, "This is unreachable"); +} diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected new file mode 100644 index 000000000000..f5b5f8044769 --- /dev/null +++ b/tests/coverage/unreachable/assert/expected @@ -0,0 +1,7 @@ +coverage/unreachable/assert/test.rs, 6, FULL +coverage/unreachable/assert/test.rs, 7, FULL +coverage/unreachable/assert/test.rs, 9, FULL +coverage/unreachable/assert/test.rs, 10, NONE +coverage/unreachable/assert/test.rs, 12, NONE +coverage/unreachable/assert/test.rs, 16, FULL +coverage/unreachable/assert/test.rs, 18, FULL diff --git a/tests/coverage/unreachable/assert/test.rs b/tests/coverage/unreachable/assert/test.rs new file mode 100644 index 000000000000..e7bddead756a --- /dev/null +++ b/tests/coverage/unreachable/assert/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn foo() { + let x: i32 = kani::any(); + if x > 5 { + // fails + assert!(x < 4); + if x < 3 { + // unreachable + assert!(x == 2); + } + } else { + // passes + assert!(x <= 5); + } +} diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected new file mode 100644 index 000000000000..f4e7608b2c13 --- /dev/null +++ b/tests/coverage/unreachable/assert_eq/expected @@ -0,0 +1,5 @@ +coverage/unreachable/assert_eq/test.rs, 6, FULL +coverage/unreachable/assert_eq/test.rs, 7, FULL +coverage/unreachable/assert_eq/test.rs, 8, FULL +coverage/unreachable/assert_eq/test.rs, 9, NONE +coverage/unreachable/assert_eq/test.rs, 11, FULL diff --git a/tests/coverage/unreachable/assert_eq/test.rs b/tests/coverage/unreachable/assert_eq/test.rs new file mode 100644 index 000000000000..29623498e715 --- /dev/null +++ b/tests/coverage/unreachable/assert_eq/test.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: i32 = kani::any(); + let y = if x > 10 { 15 } else { 33 }; + if y > 50 { + assert_eq!(y, 55); + } +} diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected new file mode 100644 index 000000000000..3b57defb4c36 --- /dev/null +++ b/tests/coverage/unreachable/assert_ne/expected @@ -0,0 +1,6 @@ +coverage/unreachable/assert_ne/test.rs, 6, FULL +coverage/unreachable/assert_ne/test.rs, 7, FULL +coverage/unreachable/assert_ne/test.rs, 8, FULL +coverage/unreachable/assert_ne/test.rs, 10, FULL +coverage/unreachable/assert_ne/test.rs, 11, NONE +coverage/unreachable/assert_ne/test.rs, 14, FULL diff --git a/tests/coverage/unreachable/assert_ne/test.rs b/tests/coverage/unreachable/assert_ne/test.rs new file mode 100644 index 000000000000..44b0ca82383e --- /dev/null +++ b/tests/coverage/unreachable/assert_ne/test.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + let x: u32 = kani::any(); + if x > 0 { + let y = x / 2; + // y is strictly less than x + if y == x { + assert_ne!(y, 1); + } + } +} diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected new file mode 100644 index 000000000000..8c1ae8a247d2 --- /dev/null +++ b/tests/coverage/unreachable/assume_assert/expected @@ -0,0 +1,4 @@ +coverage/unreachable/assume_assert/main.rs, 5, FULL +coverage/unreachable/assume_assert/main.rs, 6, FULL +coverage/unreachable/assume_assert/main.rs, 7, NONE +coverage/unreachable/assume_assert/main.rs, 8, NONE diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs new file mode 100644 index 000000000000..c4d5d65c6640 --- /dev/null +++ b/tests/coverage/unreachable/assume_assert/main.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] +fn check_assume_assert() { + let a: u8 = kani::any(); + kani::assume(false); + assert!(a < 5); +} diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected new file mode 100644 index 000000000000..610372000a01 --- /dev/null +++ b/tests/coverage/unreachable/bounds/expected @@ -0,0 +1,4 @@ +coverage/unreachable/bounds/test.rs, 5, PARTIAL +coverage/unreachable/bounds/test.rs, 6, FULL +coverage/unreachable/bounds/test.rs, 11, FULL +coverage/unreachable/bounds/test.rs, 12, FULL diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs new file mode 100644 index 000000000000..c37c9d0dcad6 --- /dev/null +++ b/tests/coverage/unreachable/bounds/test.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn get(s: &[i16], index: usize) -> i16 { + if index < s.len() { s[index] } else { -1 } +} + +#[kani::proof] +fn main() { + //get(&[7, -83, 19], 2); + get(&[5, 206, -46, 321, 8], 8); +} diff --git a/tests/coverage/unreachable/break/expected b/tests/coverage/unreachable/break/expected new file mode 100644 index 000000000000..dcb013c50c3d --- /dev/null +++ b/tests/coverage/unreachable/break/expected @@ -0,0 +1,9 @@ +coverage/unreachable/break/main.rs, 5, PARTIAL +coverage/unreachable/break/main.rs, 6, FULL +coverage/unreachable/break/main.rs, 7, FULL +coverage/unreachable/break/main.rs, 11, NONE +coverage/unreachable/break/main.rs, 12, PARTIAL +coverage/unreachable/break/main.rs, 16, FULL +coverage/unreachable/break/main.rs, 17, FULL +coverage/unreachable/break/main.rs, 18, FULL +coverage/unreachable/break/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/unreachable/break/main.rs new file mode 100644 index 000000000000..4e795bd2a6ea --- /dev/null +++ b/tests/coverage/unreachable/break/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn find_positive(nums: &[i32]) -> Option { + for &num in nums { + if num > 0 { + return Some(num); + } + } + // This part is unreachable if there is at least one positive number. + None +} + +#[kani::proof] +fn main() { + let numbers = [-3, -1, 0, 2, 4]; + let result = find_positive(&numbers); + assert_eq!(result, Some(2)); +} diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected new file mode 100644 index 000000000000..214cbfa827bd --- /dev/null +++ b/tests/coverage/unreachable/check_id/expected @@ -0,0 +1,16 @@ +coverage/unreachable/check_id/main.rs, 5, FULL +coverage/unreachable/check_id/main.rs, 6, FULL +coverage/unreachable/check_id/main.rs, 8, NONE +coverage/unreachable/check_id/main.rs, 10, FULL +coverage/unreachable/check_id/main.rs, 14, FULL +coverage/unreachable/check_id/main.rs, 15, FULL +coverage/unreachable/check_id/main.rs, 16, FULL +coverage/unreachable/check_id/main.rs, 17, FULL +coverage/unreachable/check_id/main.rs, 18, FULL +coverage/unreachable/check_id/main.rs, 19, FULL +coverage/unreachable/check_id/main.rs, 20, FULL +coverage/unreachable/check_id/main.rs, 21, FULL +coverage/unreachable/check_id/main.rs, 22, FULL +coverage/unreachable/check_id/main.rs, 23, FULL +coverage/unreachable/check_id/main.rs, 24, FULL +coverage/unreachable/check_id/main.rs, 25, NONE diff --git a/tests/coverage/unreachable/check_id/main.rs b/tests/coverage/unreachable/check_id/main.rs new file mode 100644 index 000000000000..8273a9bcc679 --- /dev/null +++ b/tests/coverage/unreachable/check_id/main.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn foo(x: i32) { + assert!(1 + 1 == 2); + if x < 9 { + // unreachable + assert!(2 + 2 == 4); + } +} + +#[kani::proof] +fn main() { + assert!(1 + 1 == 2); + let x = if kani::any() { 33 } else { 57 }; + foo(x); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(1 + 1 == 2); + assert!(3 + 3 == 5); +} diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/unreachable/compare/expected new file mode 100644 index 000000000000..6187e232cbe7 --- /dev/null +++ b/tests/coverage/unreachable/compare/expected @@ -0,0 +1,7 @@ +coverage/unreachable/compare/main.rs, 6, PARTIAL +coverage/unreachable/compare/main.rs, 7, FULL +coverage/unreachable/compare/main.rs, 11, FULL +coverage/unreachable/compare/main.rs, 12, FULL +coverage/unreachable/compare/main.rs, 13, FULL +coverage/unreachable/compare/main.rs, 14, FULL +coverage/unreachable/compare/main.rs, 16, FULL diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/unreachable/compare/main.rs new file mode 100644 index 000000000000..a10fb84e29a8 --- /dev/null +++ b/tests/coverage/unreachable/compare/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn compare(x: u16, y: u16) -> u16 { + // The line below should be reported as PARTIAL for having both REACHABLE and UNREACHABLE checks + if x >= y { 1 } else { 0 } +} + +#[kani::proof] +fn main() { + let x: u16 = kani::any(); + let y: u16 = kani::any(); + if x >= y { + compare(x, y); + } +} diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected new file mode 100644 index 000000000000..ca67a4938193 --- /dev/null +++ b/tests/coverage/unreachable/contradiction/expected @@ -0,0 +1,6 @@ +coverage/unreachable/contradiction/main.rs, 5, FULL +coverage/unreachable/contradiction/main.rs, 6, FULL +coverage/unreachable/contradiction/main.rs, 7, PARTIAL +coverage/unreachable/contradiction/main.rs, 8, NONE +coverage/unreachable/contradiction/main.rs, 11, FULL +coverage/unreachable/contradiction/main.rs, 13, FULL diff --git a/tests/coverage/unreachable/contradiction/main.rs b/tests/coverage/unreachable/contradiction/main.rs new file mode 100644 index 000000000000..fe79107e8962 --- /dev/null +++ b/tests/coverage/unreachable/contradiction/main.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] +fn contradiction() { + let x: u8 = kani::any(); + if x > 5 { + if x < 2 { + let y = x; + } + } else { + assert!(x < 10); + } +} diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected new file mode 100644 index 000000000000..25fdfed4c863 --- /dev/null +++ b/tests/coverage/unreachable/debug-assert/expected @@ -0,0 +1,4 @@ +coverage/unreachable/debug-assert/main.rs, 6, PARTIAL +coverage/unreachable/debug-assert/main.rs, 7, PARTIAL +coverage/unreachable/debug-assert/main.rs, 8, NONE +coverage/unreachable/debug-assert/main.rs, 10, NONE diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs new file mode 100644 index 000000000000..ab3ab41e47d0 --- /dev/null +++ b/tests/coverage/unreachable/debug-assert/main.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn main() { + for i in 0..4 { + debug_assert!(i > 0, "This should fail and stop the execution"); + assert!(i == 0, "This should be unreachable"); + } +} diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected new file mode 100644 index 000000000000..63081358941a --- /dev/null +++ b/tests/coverage/unreachable/divide/expected @@ -0,0 +1,7 @@ +coverage/unreachable/divide/main.rs, 6, FULL +coverage/unreachable/divide/main.rs, 7, FULL +coverage/unreachable/divide/main.rs, 9, NONE +coverage/unreachable/divide/main.rs, 11, FULL +coverage/unreachable/divide/main.rs, 15, FULL +coverage/unreachable/divide/main.rs, 16, FULL +coverage/unreachable/divide/main.rs, 17, FULL diff --git a/tests/coverage/unreachable/divide/main.rs b/tests/coverage/unreachable/divide/main.rs new file mode 100644 index 000000000000..ba6afab83135 --- /dev/null +++ b/tests/coverage/unreachable/divide/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that checks for UNREACHABLE panics. The panic is reported as NONE for the assumption that the divisor is not zero. +fn divide(a: i32, b: i32) -> i32 { + if b != 0 { + return a / b; + } else { + panic!("Division by zero"); + } +} + +#[kani::proof] +fn main() { + let y: i32 = kani::any(); + kani::assume(y != 0); + let result = divide(10, y); + assert_eq!(result, 5); +} diff --git a/tests/coverage/unreachable/early-return/expected b/tests/coverage/unreachable/early-return/expected new file mode 100644 index 000000000000..466c1775408b --- /dev/null +++ b/tests/coverage/unreachable/early-return/expected @@ -0,0 +1,10 @@ +coverage/unreachable/early-return/main.rs, 5, PARTIAL +coverage/unreachable/early-return/main.rs, 6, FULL +coverage/unreachable/early-return/main.rs, 7, FULL +coverage/unreachable/early-return/main.rs, 10, NONE +coverage/unreachable/early-return/main.rs, 11, PARTIAL +coverage/unreachable/early-return/main.rs, 15, FULL +coverage/unreachable/early-return/main.rs, 16, FULL +coverage/unreachable/early-return/main.rs, 17, FULL +coverage/unreachable/early-return/main.rs, 18, FULL +coverage/unreachable/early-return/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/early-return/main.rs b/tests/coverage/unreachable/early-return/main.rs new file mode 100644 index 000000000000..4e50c1f8a3b7 --- /dev/null +++ b/tests/coverage/unreachable/early-return/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn find_index(nums: &[i32], target: i32) -> Option { + for (index, &num) in nums.iter().enumerate() { + if num == target { + return Some(index); + } + } + None +} + +#[kani::proof] +fn main() { + let numbers = [10, 20, 30, 40, 50]; + let target = 30; + let result = find_index(&numbers, target); + assert_eq!(result, Some(2)); +} diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected new file mode 100644 index 000000000000..4460f23a80de --- /dev/null +++ b/tests/coverage/unreachable/if-statement/expected @@ -0,0 +1,10 @@ +coverage/unreachable/if-statement/main.rs, 5, FULL +coverage/unreachable/if-statement/main.rs, 7, PARTIAL +coverage/unreachable/if-statement/main.rs, 8, NONE +coverage/unreachable/if-statement/main.rs, 9, NONE +coverage/unreachable/if-statement/main.rs, 11, NONE +coverage/unreachable/if-statement/main.rs, 13, FULL +coverage/unreachable/if-statement/main.rs, 17, FULL +coverage/unreachable/if-statement/main.rs, 18, FULL +coverage/unreachable/if-statement/main.rs, 19, FULL +coverage/unreachable/if-statement/main.rs, 20, FULL diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/unreachable/if-statement/main.rs new file mode 100644 index 000000000000..f497cd76808e --- /dev/null +++ b/tests/coverage/unreachable/if-statement/main.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn check_number(num: i32) -> &'static str { + if num > 0 { + // The line is partially covered because the if statement is UNREACHABLE while the else statement is reachable + if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" } + } else if num < 0 { + "Negative" + } else { + "Zero" + } +} + +#[kani::proof] +fn main() { + let number = 7; + let result = check_number(number); + assert_eq!(result, "Positive and Odd"); +} diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected new file mode 100644 index 000000000000..17a52666c08d --- /dev/null +++ b/tests/coverage/unreachable/multiple-harnesses/expected @@ -0,0 +1,39 @@ +Checking harness fully_covered... +coverage/unreachable/multiple-harnesses/main.rs, 5, FULL +coverage/unreachable/multiple-harnesses/main.rs, 7, FULL +coverage/unreachable/multiple-harnesses/main.rs, 8, FULL +coverage/unreachable/multiple-harnesses/main.rs, 9, FULL +coverage/unreachable/multiple-harnesses/main.rs, 11, FULL +coverage/unreachable/multiple-harnesses/main.rs, 13, FULL +coverage/unreachable/multiple-harnesses/main.rs, 14, FULL +coverage/unreachable/multiple-harnesses/main.rs, 15, FULL +coverage/unreachable/multiple-harnesses/main.rs, 17, FULL +coverage/unreachable/multiple-harnesses/main.rs, 20, FULL +coverage/unreachable/multiple-harnesses/main.rs, 21, FULL +coverage/unreachable/multiple-harnesses/main.rs, 23, FULL +coverage/unreachable/multiple-harnesses/main.rs, 26, FULL +coverage/unreachable/multiple-harnesses/main.rs, 40, FULL +coverage/unreachable/multiple-harnesses/main.rs, 41, FULL +coverage/unreachable/multiple-harnesses/main.rs, 42, FULL +coverage/unreachable/multiple-harnesses/main.rs, 43, FULL +coverage/unreachable/multiple-harnesses/main.rs, 44, FULL + +Checking harness mostly_covered... +coverage/unreachable/multiple-harnesses/main.rs, 5, FULL +coverage/unreachable/multiple-harnesses/main.rs, 7, FULL +coverage/unreachable/multiple-harnesses/main.rs, 8, FULL +coverage/unreachable/multiple-harnesses/main.rs, 9, FULL +coverage/unreachable/multiple-harnesses/main.rs, 11, FULL +coverage/unreachable/multiple-harnesses/main.rs, 13, FULL +coverage/unreachable/multiple-harnesses/main.rs, 14, FULL +coverage/unreachable/multiple-harnesses/main.rs, 15, FULL +coverage/unreachable/multiple-harnesses/main.rs, 17, FULL +coverage/unreachable/multiple-harnesses/main.rs, 20, FULL +coverage/unreachable/multiple-harnesses/main.rs, 21, FULL +coverage/unreachable/multiple-harnesses/main.rs, 23, NONE +coverage/unreachable/multiple-harnesses/main.rs, 26, FULL +coverage/unreachable/multiple-harnesses/main.rs, 31, FULL +coverage/unreachable/multiple-harnesses/main.rs, 32, FULL +coverage/unreachable/multiple-harnesses/main.rs, 33, FULL +coverage/unreachable/multiple-harnesses/main.rs, 34, FULL +coverage/unreachable/multiple-harnesses/main.rs, 35, FULL diff --git a/tests/coverage/unreachable/multiple-harnesses/main.rs b/tests/coverage/unreachable/multiple-harnesses/main.rs new file mode 100644 index 000000000000..9cf7dc4101e6 --- /dev/null +++ b/tests/coverage/unreachable/multiple-harnesses/main.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn estimate_size(x: u32) -> u32 { + assert!(x < 4096); + + if x < 256 { + if x < 128 { + return 1; + } else { + return 3; + } + } else if x < 1024 { + if x > 1022 { + return 4; + } else { + return 5; + } + } else { + if x < 2048 { + return 7; + } else { + return 9; + } + } +} + +#[cfg(kani)] +#[kani::proof] +fn mostly_covered() { + let x: u32 = kani::any(); + kani::assume(x < 2048); + let y = estimate_size(x); + assert!(y < 10); +} + +#[cfg(kani)] +#[kani::proof] +fn fully_covered() { + let x: u32 = kani::any(); + kani::assume(x < 4096); + let y = estimate_size(x); + assert!(y < 10); +} diff --git a/tests/coverage/unreachable/return/expected b/tests/coverage/unreachable/return/expected new file mode 100644 index 000000000000..139f81840aab --- /dev/null +++ b/tests/coverage/unreachable/return/expected @@ -0,0 +1,8 @@ +coverage/unreachable/return/main.rs, 5, FULL +coverage/unreachable/return/main.rs, 6, FULL +coverage/unreachable/return/main.rs, 9, NONE +coverage/unreachable/return/main.rs, 10, PARTIAL +coverage/unreachable/return/main.rs, 14, FULL +coverage/unreachable/return/main.rs, 15, FULL +coverage/unreachable/return/main.rs, 16, FULL +coverage/unreachable/return/main.rs, 17, FULL diff --git a/tests/coverage/unreachable/return/main.rs b/tests/coverage/unreachable/return/main.rs new file mode 100644 index 000000000000..ccd76a5b4f8e --- /dev/null +++ b/tests/coverage/unreachable/return/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn greet(is_guest: bool) -> &'static str { + if is_guest { + return "Welcome, Guest!"; + } + // This part is unreachable if is_guest is true. + "Hello, User!" +} + +#[kani::proof] +fn main() { + let is_guest = true; + let message = greet(is_guest); + assert_eq!(message, "Welcome, Guest!"); +} diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected new file mode 100644 index 000000000000..cf45a502d295 --- /dev/null +++ b/tests/coverage/unreachable/tutorial_unreachable/expected @@ -0,0 +1,5 @@ +coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE +coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL diff --git a/tests/coverage/unreachable/tutorial_unreachable/main.rs b/tests/coverage/unreachable/tutorial_unreachable/main.rs new file mode 100644 index 000000000000..c56e591446cf --- /dev/null +++ b/tests/coverage/unreachable/tutorial_unreachable/main.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn unreachable_example() { + let x = 5; + let y = x + 2; + if x > y { + assert!(x < 8); + } +} diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected new file mode 100644 index 000000000000..8fa3ec8b870f --- /dev/null +++ b/tests/coverage/unreachable/variant/expected @@ -0,0 +1,10 @@ +coverage/unreachable/variant/main.rs, 15, FULL +coverage/unreachable/variant/main.rs, 16, NONE +coverage/unreachable/variant/main.rs, 17, NONE +coverage/unreachable/variant/main.rs, 18, FULL +coverage/unreachable/variant/main.rs, 19, NONE +coverage/unreachable/variant/main.rs, 21, NONE +coverage/unreachable/variant/main.rs, 23, FULL +coverage/unreachable/variant/main.rs, 27, FULL +coverage/unreachable/variant/main.rs, 28, FULL +coverage/unreachable/variant/main.rs, 29, FULL diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs new file mode 100644 index 000000000000..ca53b8ccfd18 --- /dev/null +++ b/tests/coverage/unreachable/variant/main.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a `match` statement matching on +//! all enum variants. + +enum Direction { + Up, + Down, + Left, + Right, +} + +fn print_direction(dir: Direction) { + match dir { + Direction::Up => println!("Going up!"), + Direction::Down => println!("Going down!"), + Direction::Left => println!("Going left!"), + Direction::Right => println!("Going right!"), + // This part is unreachable since we cover all variants in the match. + _ => {} + } +} + +#[kani::proof] +fn main() { + let direction = Direction::Left; + print_direction(direction); +} diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected new file mode 100644 index 000000000000..e47941f17db2 --- /dev/null +++ b/tests/coverage/unreachable/vectors/expected @@ -0,0 +1,6 @@ +coverage/unreachable/vectors/main.rs, 8, FULL +coverage/unreachable/vectors/main.rs, 11, FULL +coverage/unreachable/vectors/main.rs, 13, PARTIAL +coverage/unreachable/vectors/main.rs, 15, NONE +coverage/unreachable/vectors/main.rs, 17, FULL +coverage/unreachable/vectors/main.rs, 19, FULL diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs new file mode 100644 index 000000000000..a44c4bb47c3d --- /dev/null +++ b/tests/coverage/unreachable/vectors/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a guarded out-of-bounds access. + +#[kani::proof] +fn main() { + let numbers = vec![1, 2, 3, 4, 5]; + + // Attempt to access the 10th element of the vector, which is out of bounds. + let tenth_element = numbers.get(9); + + if let Some(value) = tenth_element { + // This part is unreachable since the vector has only 5 elements (indices 0 to 4). + println!("The 10th element is: {}", value); + } else { + println!("The 10th element is out of bounds!"); + } +} diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected new file mode 100644 index 000000000000..a0e43c183846 --- /dev/null +++ b/tests/coverage/unreachable/while-loop-break/expected @@ -0,0 +1,11 @@ +coverage/unreachable/while-loop-break/main.rs, 8, FULL +coverage/unreachable/while-loop-break/main.rs, 9, FULL +coverage/unreachable/while-loop-break/main.rs, 10, FULL +coverage/unreachable/while-loop-break/main.rs, 11, FULL +coverage/unreachable/while-loop-break/main.rs, 13, FULL +coverage/unreachable/while-loop-break/main.rs, 15, NONE +coverage/unreachable/while-loop-break/main.rs, 16, PARTIAL +coverage/unreachable/while-loop-break/main.rs, 20, FULL +coverage/unreachable/while-loop-break/main.rs, 21, FULL +coverage/unreachable/while-loop-break/main.rs, 22, FULL +coverage/unreachable/while-loop-break/main.rs, 23, FULL diff --git a/tests/coverage/unreachable/while-loop-break/main.rs b/tests/coverage/unreachable/while-loop-break/main.rs new file mode 100644 index 000000000000..cb7c6276b147 --- /dev/null +++ b/tests/coverage/unreachable/while-loop-break/main.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks coverage results in an example with a `while` loop that returns before +//! running the last iteration. + +fn find_first_negative(nums: &[i32]) -> Option { + let mut index = 0; + while index < nums.len() { + if nums[index] < 0 { + return Some(nums[index]); + } + index += 1; + } + None +} + +#[kani::proof] +fn main() { + let numbers = [1, 2, -3, 4, -5]; + let result = find_first_negative(&numbers); + assert_eq!(result, Some(-3)); +} diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index f71bc535a11e..99ec78bef693 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -19,6 +19,7 @@ pub enum Mode { KaniFixme, CargoKani, CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`. + CoverageBased, Exec, Expected, Stub, @@ -32,6 +33,7 @@ impl FromStr for Mode { "kani-fixme" => Ok(KaniFixme), "cargo-kani" => Ok(CargoKani), "cargo-kani-test" => Ok(CargoKaniTest), + "coverage-based" => Ok(CoverageBased), "exec" => Ok(Exec), "expected" => Ok(Expected), "stub-tests" => Ok(Stub), @@ -47,6 +49,7 @@ impl fmt::Display for Mode { KaniFixme => "kani-fixme", CargoKani => "cargo-kani", CargoKaniTest => "cargo-kani-test", + CoverageBased => "coverage-based", Exec => "exec", Expected => "expected", Stub => "stub-tests", diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 0dd403ba1b2f..cdef1446763a 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -94,7 +94,7 @@ pub fn parse_config(args: Vec) -> Config { .optflag("", "report-time", "report the time of each test. Configuration is done via env variables, like \ rust unit tests.") - .optmulti("", "kani-flag", + .optmulti("", "kani-flag", "pass extra flags to Kani. Note that this may cause spurious failures if the \ passed flag conflicts with the test configuration. Only works for `kani`, \ `cargo-kani`, and `expected` modes." diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 04647f7b6572..7fad336dffdc 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -7,7 +7,9 @@ use crate::common::KaniFailStep; use crate::common::{output_base_dir, output_base_name}; -use crate::common::{CargoKani, CargoKaniTest, Exec, Expected, Kani, KaniFixme, Stub}; +use crate::common::{ + CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, +}; use crate::common::{Config, TestPaths}; use crate::header::TestProps; use crate::read2::read2; @@ -75,6 +77,7 @@ impl<'test> TestCx<'test> { KaniFixme => self.run_kani_test(), CargoKani => self.run_cargo_kani_test(false), CargoKaniTest => self.run_cargo_kani_test(true), + CoverageBased => self.run_expected_coverage_test(), Exec => self.run_exec_test(), Expected => self.run_expected_test(), Stub => self.run_stub_test(), @@ -311,6 +314,22 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } + /// Run coverage based output for kani on a single file + fn run_kani_with_coverage(&self) -> ProcRes { + let mut kani = Command::new("kani"); + if !self.props.compile_flags.is_empty() { + kani.env("RUSTFLAGS", self.props.compile_flags.join(" ")); + } + kani.arg(&self.testpaths.file).args(&self.props.kani_flags); + kani.arg("--coverage").args(&["-Z", "line-coverage"]); + + if !self.props.cbmc_flags.is_empty() { + kani.arg("--cbmc-args").args(&self.props.cbmc_flags); + } + + self.compose_and_run(kani) + } + /// Runs an executable file and: /// * Checks the expected output if an expected file is specified /// * Checks the exit code (assumed to be 0 by default) @@ -380,6 +399,13 @@ impl<'test> TestCx<'test> { self.verify_output(&proc_res, &expected_path); } + /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`. + fn run_expected_coverage_test(&self) { + let proc_res = self.run_kani_with_coverage(); + let expected_path = self.testpaths.file.parent().unwrap().join("expected"); + self.verify_output(&proc_res, &expected_path); + } + /// Runs Kani with stub implementations of various data structures. /// Currently, it only runs tests for the Vec module with the (Kani)Vec /// abstraction. At a later stage, it should be possible to add command-line From f024d23c46e3f0010004f6e09a869338755ce260 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 28 Jul 2023 19:25:40 -0700 Subject: [PATCH 2/4] Delay writing metadata file (no UX impact) (#2628) Kani compiler will now only store KaniMetadata after compiling all harnesses. Before, we were storing before codegen in the first iteration of the compiler. This will still allow us to generate metadata without actually performing codegen, if we ever implement a `kani list` subcommand. The metadata won't be stored though if Kani fails to codegen. However, we don't do anything extra with that file if the compilation fails. This change is required for #2493 and contracts work. This will allow us to store information collected during code generation. --- kani-compiler/src/kani_compiler.rs | 215 +++++++++++++++++++++++------ kani_metadata/src/harness.rs | 6 +- 2 files changed, 174 insertions(+), 47 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index ef766c562941..a1e231301566 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -39,6 +39,7 @@ use std::collections::{BTreeMap, HashMap}; use std::fs::File; use std::io::BufWriter; use std::mem; +use std::path::{Path, PathBuf}; use std::process::ExitCode; use std::sync::{Arc, Mutex}; use tracing::debug; @@ -71,12 +72,21 @@ type HarnessId = DefPathHash; /// A set of stubs. type Stubs = BTreeMap; -#[derive(Debug)] +#[derive(Clone, Debug)] struct HarnessInfo { pub metadata: HarnessMetadata, pub stub_map: Stubs, } +/// Store some relevant information about the crate compilation. +#[derive(Clone, Debug)] +struct CrateInfo { + /// The name of the crate being compiled. + pub name: String, + /// The metadata output path that shall be generated as part of the crate compilation. + pub output_path: PathBuf, +} + /// Represents the current compilation stage. /// /// The Kani compiler may run the Rust compiler multiple times since stubbing has to be applied @@ -85,20 +95,28 @@ struct HarnessInfo { /// - We always start in the [CompilationStage::Init]. /// - After [CompilationStage::Init] we transition to either /// - [CompilationStage::CodegenNoStubs] on a regular crate compilation, this will follow Init. -/// - [CompilationStage::Done], running the compiler to gather information, such as `--version` -/// will skip code generation completely, and there is no work to be done. +/// - [CompilationStage::CompilationSkipped], running the compiler to gather information, such as +/// `--version` will skip code generation completely, and there is no work to be done. /// - After the [CompilationStage::CodegenNoStubs], we transition to either /// - [CompilationStage::CodegenWithStubs] when there is at least one harness with stubs. /// - [CompilationStage::Done] where there is no harness left to process. /// - The [CompilationStage::CodegenWithStubs] can last multiple Rust compiler runs. Once there is /// no harness left, we move to [CompilationStage::Done]. +/// - The final stages are either [CompilationStage::Done] or [CompilationStage::CompilationSkipped]. +/// - [CompilationStage::Done] represents the final state of the compiler after a successful +/// compilation. The crate metadata is stored here (even if no codegen was actually performed). +/// - [CompilationStage::CompilationSkipped] no compilation was actually performed. +/// No work needs to be done. +/// - Note: In a scenario where the compilation fails, the compiler will exit immediately, +/// independent on the stage. Any artifact produced shouldn't be used. /// I.e.: /// ```dot /// graph CompilationStage { -/// Init -> {CodegenNoStubs, Done} +/// Init -> {CodegenNoStubs, CompilationSkipped} /// CodegenNoStubs -> {CodegenStubs, Done} /// // Loop up to N harnesses times. /// CodegenStubs -> {CodegenStubs, Done} +/// CompilationSkipped /// Done /// } /// ``` @@ -108,11 +126,14 @@ enum CompilationStage { /// Initial state that the compiler is always instantiated with. /// In this stage, we initialize the Query and collect all harnesses. Init, + /// State where the compiler ran but didn't actually compile anything (e.g.: --version). + CompilationSkipped, /// Stage where the compiler will perform codegen of all harnesses that don't use stub. CodegenNoStubs { target_harnesses: Vec, next_harnesses: Vec>, all_harnesses: HashMap, + crate_info: CrateInfo, }, /// Stage where the compiler will codegen harnesses that use stub, one group at a time. /// The harnesses at this stage are grouped according to the stubs they are using. For now, @@ -121,18 +142,17 @@ enum CompilationStage { target_harnesses: Vec, next_harnesses: Vec>, all_harnesses: HashMap, + crate_info: CrateInfo, + }, + Done { + metadata: Option<(KaniMetadata, CrateInfo)>, }, - Done, } impl CompilationStage { pub fn is_init(&self) -> bool { matches!(self, CompilationStage::Init) } - - pub fn is_done(&self) -> bool { - matches!(self, CompilationStage::Done) - } } /// This object controls the compiler behavior. @@ -160,7 +180,7 @@ impl KaniCompiler { /// Since harnesses may have different attributes that affect compilation, Kani compiler can /// actually invoke the rust compiler multiple times. pub fn run(&mut self, orig_args: Vec) -> Result<(), ErrorGuaranteed> { - while !self.stage.is_done() { + loop { debug!(next=?self.stage, "run"); match &self.stage { CompilationStage::Init => { @@ -178,14 +198,28 @@ impl KaniCompiler { args.push(extra_arg); self.run_compilation_session(&args)?; } - CompilationStage::Done => { - unreachable!("There's nothing to be done here.") + CompilationStage::Done { metadata: Some((kani_metadata, crate_info)) } => { + // Only store metadata for harnesses for now. + // TODO: This should only skip None. + // https://github.com/model-checking/kani/issues/2493 + if self.queries.lock().unwrap().reachability_analysis + == ReachabilityType::Harnesses + { + // Store metadata file. + // We delay storing the metadata so we can include information collected + // during codegen. + self.store_metadata(&kani_metadata, &crate_info.output_path); + } + return Ok(()); + } + CompilationStage::Done { metadata: None } + | CompilationStage::CompilationSkipped => { + return Ok(()); } }; self.next_stage(); } - Ok(()) } /// Set up the next compilation stage after a `rustc` run. @@ -193,22 +227,35 @@ impl KaniCompiler { self.stage = match &mut self.stage { CompilationStage::Init => { // This may occur when user passes arguments like --version or --help. - CompilationStage::Done + CompilationStage::Done { metadata: None } } - CompilationStage::CodegenNoStubs { next_harnesses, all_harnesses, .. } - | CompilationStage::CodegenWithStubs { next_harnesses, all_harnesses, .. } => { + CompilationStage::CodegenNoStubs { + next_harnesses, all_harnesses, crate_info, .. + } + | CompilationStage::CodegenWithStubs { + next_harnesses, + all_harnesses, + crate_info, + .. + } => { if let Some(target_harnesses) = next_harnesses.pop() { assert!(!target_harnesses.is_empty(), "expected at least one target harness"); CompilationStage::CodegenWithStubs { target_harnesses, next_harnesses: mem::take(next_harnesses), all_harnesses: mem::take(all_harnesses), + crate_info: crate_info.clone(), } } else { - CompilationStage::Done + CompilationStage::Done { + metadata: Some(( + generate_metadata(&crate_info, all_harnesses), + crate_info.clone(), + )), + } } } - CompilationStage::Done => { + CompilationStage::Done { .. } | CompilationStage::CompilationSkipped => { unreachable!() } }; @@ -225,6 +272,10 @@ impl KaniCompiler { /// Gather and process all harnesses from this crate that shall be compiled. fn process_harnesses(&self, tcx: TyCtxt) -> CompilationStage { + let crate_info = CrateInfo { + name: tcx.crate_name(LOCAL_CRATE).as_str().into(), + output_path: metadata_output_path(tcx), + }; if self.queries.lock().unwrap().reachability_analysis == ReachabilityType::Harnesses { let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id)); @@ -250,14 +301,13 @@ impl KaniCompiler { // Generate code without stubs. (all_harnesses.keys().cloned().collect(), vec![]) }; - // Store metadata file. - self.store_metadata(tcx, &all_harnesses); - // Even if no_stubs is empty we still need to store metadata. + // Even if no_stubs is empty we still need to store rustc metadata. CompilationStage::CodegenNoStubs { target_harnesses: no_stubs, next_harnesses: group_by_stubs(with_stubs, &all_harnesses), all_harnesses, + crate_info, } } else { // Leave other reachability type handling as is for now. @@ -265,6 +315,7 @@ impl KaniCompiler { target_harnesses: vec![], next_harnesses: vec![], all_harnesses: HashMap::default(), + crate_info, } } } @@ -291,25 +342,14 @@ impl KaniCompiler { .collect(); Compilation::Continue } - CompilationStage::Init | CompilationStage::Done => unreachable!(), + CompilationStage::Init + | CompilationStage::Done { .. } + | CompilationStage::CompilationSkipped => unreachable!(), } } /// Write the metadata to a file - fn store_metadata(&self, tcx: TyCtxt, all_harnesses: &HashMap) { - let (proof_harnesses, test_harnesses) = all_harnesses - .values() - .map(|info| &info.metadata) - .cloned() - .partition(|md| md.attributes.proof); - let metadata = KaniMetadata { - crate_name: tcx.crate_name(LOCAL_CRATE).as_str().into(), - proof_harnesses, - unsupported_features: vec![], - test_harnesses, - }; - let mut filename = tcx.output_filenames(()).output_path(OutputType::Object); - filename.set_extension(ArtifactType::Metadata); + fn store_metadata(&self, metadata: &KaniMetadata, filename: &Path) { debug!(?filename, "write_metadata"); let out_file = File::create(&filename).unwrap(); let writer = BufWriter::new(out_file); @@ -388,10 +428,34 @@ impl Callbacks for KaniCompiler { } } +/// Generate [KaniMetadata] for the target crate. +fn generate_metadata( + crate_info: &CrateInfo, + all_harnesses: &HashMap, +) -> KaniMetadata { + let (proof_harnesses, test_harnesses) = all_harnesses + .values() + .map(|info| &info.metadata) + .cloned() + .partition(|md| md.attributes.proof); + KaniMetadata { + crate_name: crate_info.name.clone(), + proof_harnesses, + unsupported_features: vec![], + test_harnesses, + } +} + +/// Extract the filename for the metadata file. +fn metadata_output_path(tcx: TyCtxt) -> PathBuf { + let mut filename = tcx.output_filenames(()).output_path(OutputType::Object); + filename.set_extension(ArtifactType::Metadata); + filename +} + #[cfg(test)] mod tests { - use super::{HarnessInfo, Stubs}; - use crate::kani_compiler::{group_by_stubs, HarnessId}; + use super::*; use kani_metadata::{HarnessAttributes, HarnessMetadata}; use rustc_data_structures::fingerprint::Fingerprint; use rustc_hir::definitions::DefPathHash; @@ -404,12 +468,12 @@ mod tests { DefPathHash(Fingerprint::new(id, 0)) } - fn mock_metadata() -> HarnessMetadata { + fn mock_metadata(name: String, krate: String) -> HarnessMetadata { HarnessMetadata { - pretty_name: String::from("dummy"), - mangled_name: String::from("dummy"), - crate_name: String::from("dummy"), - original_file: String::from("dummy"), + pretty_name: name.clone(), + mangled_name: name.clone(), + original_file: format!("{}.rs", krate), + crate_name: krate, original_start_line: 10, original_end_line: 20, goto_file: None, @@ -418,7 +482,7 @@ mod tests { } fn mock_info_with_stubs(stub_map: Stubs) -> HarnessInfo { - HarnessInfo { metadata: mock_metadata(), stub_map } + HarnessInfo { metadata: mock_metadata("dummy".to_string(), "crate".to_string()), stub_map } } #[test] @@ -458,4 +522,67 @@ mod tests { ); assert!(grouped.contains(&vec![harness_2])); } + + #[test] + fn test_generate_metadata() { + // Mock inputs. + let name = "my_crate".to_string(); + let crate_info = CrateInfo { name: name.clone(), output_path: PathBuf::default() }; + + let mut info = mock_info_with_stubs(Stubs::default()); + info.metadata.attributes.proof = true; + let id = mock_next_id(); + let all_harnesses = HashMap::from([(id, info.clone())]); + + // Call generate metadata. + let metadata = generate_metadata(&crate_info, &all_harnesses); + + // Check output. + assert_eq!(metadata.crate_name, name); + assert_eq!(metadata.proof_harnesses.len(), 1); + assert_eq!(*metadata.proof_harnesses.first().unwrap(), info.metadata); + } + + #[test] + fn test_generate_empty_metadata() { + // Mock inputs. + let name = "my_crate".to_string(); + let crate_info = CrateInfo { name: name.clone(), output_path: PathBuf::default() }; + let all_harnesses = HashMap::new(); + + // Call generate metadata. + let metadata = generate_metadata(&crate_info, &all_harnesses); + + // Check output. + assert_eq!(metadata.crate_name, name); + assert_eq!(metadata.proof_harnesses.len(), 0); + } + + #[test] + fn test_generate_metadata_with_multiple_harness() { + // Mock inputs. + let krate = "my_crate".to_string(); + let crate_info = CrateInfo { name: krate.clone(), output_path: PathBuf::default() }; + + let harnesses = ["h1", "h2", "h3"]; + let infos = harnesses.map(|harness| { + let mut metadata = mock_metadata(harness.to_string(), krate.clone()); + metadata.attributes.proof = true; + (mock_next_id(), HarnessInfo { stub_map: Stubs::default(), metadata }) + }); + let all_harnesses = HashMap::from(infos.clone()); + + // Call generate metadata. + let metadata = generate_metadata(&crate_info, &all_harnesses); + + // Check output. + assert_eq!(metadata.crate_name, krate); + assert_eq!(metadata.proof_harnesses.len(), infos.len()); + assert!( + metadata + .proof_harnesses + .iter() + .all(|harness| harnesses.contains(&&*harness.pretty_name)) + ); + } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 2aadc70e9468..2356f9bdf42f 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -6,7 +6,7 @@ use serde::{Deserialize, Serialize}; use std::path::PathBuf; /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct HarnessMetadata { /// The fully qualified name the user gave to the function (i.e. includes the module path). pub pretty_name: String, @@ -27,7 +27,7 @@ pub struct HarnessMetadata { } /// The attributes added by the user to control how a harness is executed. -#[derive(Debug, Clone, Serialize, Deserialize, Default)] +#[derive(Debug, Clone, Serialize, Deserialize, Default, PartialEq)] pub struct HarnessAttributes { /// Whether the harness has been annotated with proof. pub proof: bool, @@ -42,7 +42,7 @@ pub struct HarnessAttributes { } /// The stubbing type. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct Stub { pub original: String, pub replacement: String, From 06f0b5c395e954e9395708437764c447e3b0c899 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 31 Jul 2023 08:55:27 -0400 Subject: [PATCH 3/4] Include temporary test files to gitgnore (#2644) Signed-off-by: Felipe R. Monteiro --- tests/.gitignore | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/.gitignore b/tests/.gitignore index e5e7c802005a..55cf0ad46a3b 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,2 +1,12 @@ *.goto -*.json \ No newline at end of file +*.json + +# Temporary folders +rmet*/ +kani_concrete_playback + +# Binary artifacts +*out +smoke +check_tests +function From c15294e239a4a09786b36d4aa814261561dced91 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 31 Jul 2023 12:58:36 -0700 Subject: [PATCH 4/4] Add support to array-based SIMD (#2633) Originally, repr(simd) supported only multi-field form. An array based version was later added and it's likely to become the only supported way (https://github.com/rust-lang/compiler-team/issues/621). The array-based version is currently used in the standard library, and it is used to implement `portable-simd`. This change adds support to instantiating and using the array-based version. --- .../codegen_cprover_gotoc/codegen/place.rs | 121 ++++++++++++------ .../codegen_cprover_gotoc/codegen/rvalue.rs | 40 +++--- tests/kani/SIMD/array_simd_repr.rs | 36 ++++++ tests/kani/SIMD/multi_field_simd.rs | 28 ++++ tests/kani/SIMD/portable_simd.rs | 15 +++ tests/kani/SIMD/simd_float_ops_fixme.rs | 39 ++++++ 6 files changed, 225 insertions(+), 54 deletions(-) create mode 100644 tests/kani/SIMD/array_simd_repr.rs create mode 100644 tests/kani/SIMD/multi_field_simd.rs create mode 100644 tests/kani/SIMD/portable_simd.rs create mode 100644 tests/kani/SIMD/simd_float_ops_fixme.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 95fadc7bbaf2..4482ee1d1f84 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -23,7 +23,7 @@ use tracing::{debug, trace, warn}; /// A projection in Kani can either be to a type (the normal case), /// or a variant in the case of a downcast. -#[derive(Debug)] +#[derive(Copy, Clone, Debug)] pub enum TypeOrVariant<'tcx> { Type(Ty<'tcx>), Variant(&'tcx VariantDef), @@ -235,15 +235,21 @@ impl<'tcx> TypeOrVariant<'tcx> { } impl<'tcx> GotocCtx<'tcx> { + /// Codegen field access for types that allow direct field projection. + /// + /// I.e.: Algebraic data types, closures, and generators. + /// + /// Other composite types such as array only support index projection. fn codegen_field( &mut self, - res: Expr, - t: TypeOrVariant<'tcx>, - f: &FieldIdx, + parent_expr: Expr, + parent_ty_or_var: TypeOrVariant<'tcx>, + field: &FieldIdx, + field_ty_or_var: TypeOrVariant<'tcx>, ) -> Result { - match t { - TypeOrVariant::Type(t) => { - match t.kind() { + match parent_ty_or_var { + TypeOrVariant::Type(parent_ty) => { + match parent_ty.kind() { ty::Alias(..) | ty::Bool | ty::Char @@ -254,56 +260,98 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Never | ty::FnDef(..) | ty::GeneratorWitness(..) + | ty::GeneratorWitnessMIR(..) | ty::Foreign(..) | ty::Dynamic(..) | ty::Bound(..) | ty::Placeholder(..) | ty::Param(_) | ty::Infer(_) - | ty::Error(_) => unreachable!("type {:?} does not have a field", t), - ty::Tuple(_) => { - Ok(res.member(&Self::tuple_fld_name(f.index()), &self.symbol_table)) - } - ty::Adt(def, _) if def.repr().simd() => { - // this is a SIMD vector - the index represents one - // of the elements, so we want to index as an array - // Example: - // pub struct i64x2(i64, i64); - // fn main() { - // let v = i64x2(1, 2); - // assert!(v.0 == 1); // refers to the first i64 - // assert!(v.1 == 2); - // } - let size_index = Expr::int_constant(f.index(), Type::size_t()); - Ok(res.index_array(size_index)) - } + | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"), + ty::Tuple(_) => Ok(parent_expr + .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)), + ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field( + parent_expr, + *field, + field_ty_or_var.expect_type(), + )), // if we fall here, then we are handling either a struct or a union ty::Adt(def, _) => { - let field = &def.variants().raw[0].fields[*f]; - Ok(res.member(&field.name.to_string(), &self.symbol_table)) + let field = &def.variants().raw[0].fields[*field]; + Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) + } + ty::Closure(..) => { + Ok(parent_expr.member(&field.index().to_string(), &self.symbol_table)) } - ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)), ty::Generator(..) => { - let field_name = self.generator_field_name(f.as_usize()); - Ok(res + let field_name = self.generator_field_name(field.as_usize()); + Ok(parent_expr .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) } - _ => unimplemented!(), + ty::Str | ty::Array(_, _) | ty::Slice(_) | ty::RawPtr(_) | ty::Ref(_, _, _) => { + unreachable!( + "element of {parent_ty:?} is not accessed via field projection" + ) + } } } // if we fall here, then we are handling an enum - TypeOrVariant::Variant(v) => { - let field = &v.fields[*f]; - Ok(res.member(&field.name.to_string(), &self.symbol_table)) + TypeOrVariant::Variant(parent_var) => { + let field = &parent_var.fields[*field]; + Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table)) } TypeOrVariant::GeneratorVariant(_var_idx) => { - let field_name = self.generator_field_name(f.index()); - Ok(res.member(field_name, &self.symbol_table)) + let field_name = self.generator_field_name(field.index()); + Ok(parent_expr.member(field_name, &self.symbol_table)) } } } + /// This is a SIMD vector, which has 2 possible internal representations: + /// 1- Multi-field representation (original and currently deprecated) + /// In this case, a field is one lane (i.e.: one element) + /// Example: + /// ```ignore + /// pub struct i64x2(i64, i64); + /// fn main() { + /// let v = i64x2(1, 2); + /// assert!(v.0 == 1); // refers to the first i64 + /// assert!(v.1 == 2); + /// } + /// ``` + /// 2- Array-based representation + /// In this case, the projection refers to the entire array. + /// ```ignore + /// pub struct i64x2([i64; 2]); + /// fn main() { + /// let v = i64x2([1, 2]); + /// assert!(v.0 == [1, 2]); // refers to the entire array + /// } + /// ``` + /// * Note that projection inside SIMD structs may eventually become illegal. + /// See thread. + /// + /// Since the goto representation for both is the same, we use the expected type to decide + /// what to return. + fn codegen_simd_field( + &mut self, + parent_expr: Expr, + field: FieldIdx, + field_ty: Ty<'tcx>, + ) -> Expr { + if matches!(field_ty.kind(), ty::Array { .. }) { + // Array based + assert_eq!(field.index(), 0); + let field_typ = self.codegen_ty(field_ty); + parent_expr.reinterpret_cast(field_typ) + } else { + // Return the given field. + let index_expr = Expr::int_constant(field.index(), Type::size_t()); + parent_expr.index_array(index_expr) + } + } + /// If a local is a function definition, ignore the local variable name and /// generate a function call based on the def id. /// @@ -424,7 +472,8 @@ impl<'tcx> GotocCtx<'tcx> { } ProjectionElem::Field(f, t) => { let typ = TypeOrVariant::Type(t); - let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f)?; + let expr = + self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f, typ)?; ProjectedPlace::try_new( expr, typ, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 22b26a3489b4..88a2f3cd4a2c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -582,24 +582,28 @@ impl<'tcx> GotocCtx<'tcx> { AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => { let typ = self.codegen_ty(res_ty); let layout = self.layout_of(res_ty); - let vector_element_type = typ.base_type().unwrap().clone(); - Expr::vector_expr( - typ, - layout - .fields - .index_by_increasing_offset() - .map(|idx| { - let cgo = self.codegen_operand(&operands[idx.into()]); - // The input operand might actually be a one-element array, as seen - // when running assess on firecracker. - if *cgo.typ() == vector_element_type { - cgo - } else { - cgo.transmute_to(vector_element_type.clone(), &self.symbol_table) - } - }) - .collect(), - ) + trace!(shape=?layout.fields, "codegen_rvalue_aggregate"); + assert!(operands.len() > 0, "SIMD vector cannot be empty"); + if operands.len() == 1 { + let data = self.codegen_operand(&operands[0u32.into()]); + if data.typ().is_array() { + // Array-based SIMD representation. + data.transmute_to(typ, &self.symbol_table) + } else { + // Multi field-based representation with one field. + Expr::vector_expr(typ, vec![data]) + } + } else { + // Multi field SIMD representation. + Expr::vector_expr( + typ, + layout + .fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx.into()])) + .collect(), + ) + } } AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => { self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc) diff --git a/tests/kani/SIMD/array_simd_repr.rs b/tests/kani/SIMD/array_simd_repr.rs new file mode 100644 index 000000000000..076427415091 --- /dev/null +++ b/tests/kani/SIMD/array_simd_repr.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that Kani can properly handle SIMD declaration and field access using array syntax. + +#![allow(non_camel_case_types)] +#![feature(repr_simd)] + +#[repr(simd)] +#[derive(Clone, PartialEq, Eq, PartialOrd, kani::Arbitrary)] +pub struct i64x2([i64; 2]); + +#[kani::proof] +fn check_diff() { + let x = i64x2([1, 2]); + let y = i64x2([3, 4]); + assert!(x != y); +} + +#[kani::proof] +fn check_ge() { + let x: i64x2 = kani::any(); + kani::assume(x.0[0] > 0); + kani::assume(x.0[1] > 0); + assert!(x > i64x2([0, 0])); +} + +#[derive(Clone, Debug)] +#[repr(simd)] +struct CustomSimd([T; LANES]); + +#[kani::proof] +fn simd_vec() { + let simd = CustomSimd([0u8; 10]); + let idx: usize = kani::any_where(|x: &usize| *x < 10); + assert_eq!(simd.0[idx], 0); +} diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs new file mode 100644 index 000000000000..d54cf1a07bdb --- /dev/null +++ b/tests/kani/SIMD/multi_field_simd.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that Kani can properly handle SIMD declaration and field access using multi-field syntax. +//! Note: Multi-field SIMD is actually being deprecated, but until it's removed, we might +//! as well keep supporting it. +//! See for more details. + +#![allow(non_camel_case_types)] +#![feature(repr_simd)] + +#[repr(simd)] +#[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)] +pub struct i64x2(i64, i64); + +#[kani::proof] +fn check_diff() { + let x = i64x2(1, 2); + let y = i64x2(3, 4); + assert!(x != y); +} + +#[kani::proof] +fn check_ge() { + let x: i64x2 = kani::any(); + kani::assume(x.0 > 0); + kani::assume(x.1 > 0); + assert!(x > i64x2(0, 0)); +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs new file mode 100644 index 000000000000..9f7d0f536dcc --- /dev/null +++ b/tests/kani/SIMD/portable_simd.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we have basic support of portable SIMD. +#![feature(portable_simd)] + +use std::simd::u64x16; + +#[kani::proof] +fn check_sum_any() { + let a = u64x16::splat(0); + let b = u64x16::from_array(kani::any()); + // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632 + assert_eq!((a + b).as_array(), b.as_array()); +} diff --git a/tests/kani/SIMD/simd_float_ops_fixme.rs b/tests/kani/SIMD/simd_float_ops_fixme.rs new file mode 100644 index 000000000000..d258a2119eca --- /dev/null +++ b/tests/kani/SIMD/simd_float_ops_fixme.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can handle SIMD defined in the standard library +//! FIXME: +#![allow(non_camel_case_types)] +#![feature(repr_simd, platform_intrinsics, portable_simd)] +use std::simd::f32x4; + +extern "platform-intrinsic" { + fn simd_add(x: T, y: T) -> T; + fn simd_eq(x: T, y: T) -> U; +} + +#[repr(simd)] +#[derive(Clone, PartialEq, kani::Arbitrary)] +pub struct f32x2(f32, f32); + +impl f32x2 { + fn as_array(&self) -> &[f32; 2] { + unsafe { &*(self as *const f32x2 as *const [f32; 2]) } + } +} + +#[kani::proof] +fn check_sum() { + let a = f32x2(0.0, 0.0); + let b = kani::any::(); + let sum = unsafe { simd_add(a.clone(), b) }; + assert_eq!(sum.as_array(), a.as_array()); +} + +#[kani::proof] +fn check_sum_portable() { + let a = f32x4::splat(0.0); + let b = f32x4::from_array(kani::any()); + // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632 + assert_eq!((a + b).as_array(), b.as_array()); +}