diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 6651f72db7c2..bb9df4ad92cd 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -156,6 +156,9 @@ pub struct VerificationArgs { #[arg(long)] pub force_build: bool, + #[arg(long, requires("enable_unstable"))] + pub fail_uncoverable: bool, + /// Toggle between different styles of output #[arg(long, default_value = "regular", ignore_case = true, value_enum)] pub output_format: OutputFormat, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index a806331401cd..ae9883516bc8 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -28,7 +28,7 @@ pub enum VerificationStatus { /// Represents failed properties in three different categories. /// This simplifies the process to determine and format verification results. -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Copy, Debug, PartialEq)] pub enum FailedProperties { // No failures None, @@ -38,13 +38,95 @@ pub enum FailedProperties { Other, } +// Represents the global status for cover statements in two categories. +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum CoversStatus { + // All cover statements are satisfied + AllSatisfied, + // Not all cover statement are satisfied + Other, +} + +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum GlobalCondition { + ShouldPanic { enabled: bool, status: FailedProperties }, + FailUncoverable { enabled: bool, status: CoversStatus }, +} + +impl GlobalCondition { + pub fn enabled(&self) -> bool { + match &self { + Self::ShouldPanic { enabled, .. } => *enabled, + Self::FailUncoverable { enabled, .. } => *enabled, + } + } + + pub fn name(&self) -> &str { + match &self { + Self::ShouldPanic { .. } => "should_panic", + Self::FailUncoverable { .. } => "fail_uncoverable", + } + } + + pub fn passed(&self) -> bool { + match &self { + Self::ShouldPanic { status, .. } => *status == FailedProperties::PanicsOnly, + Self::FailUncoverable { status, .. } => *status == CoversStatus::AllSatisfied, + } + } + + pub fn reason(&self) -> &str { + match &self { + Self::ShouldPanic { status, .. } => match *status { + FailedProperties::None => "encountered no panics, but at least one was expected", + FailedProperties::PanicsOnly => "encountered one or more panics as expected", + FailedProperties::Other => { + "encountered failures other than panics, which were unexpected" + } + }, + Self::FailUncoverable { status, .. } => match *status { + CoversStatus::AllSatisfied => "all cover statements were satisfied as expected", + CoversStatus::Other => { + "encountered one or more cover statements which were not satisfied" + } + }, + } + } + + pub fn blame_properties<'a>(&self, properties: &'a [Property]) -> Vec<&'a Property> { + match &self { + Self::ShouldPanic { status, .. } => match *status { + FailedProperties::None => properties + .iter() + .filter(|prop| { + prop.property_class() == "assertion" && prop.status != CheckStatus::Failure + }) + .collect(), + FailedProperties::Other => properties + .iter() + .filter(|prop| { + prop.property_class() != "assertion" && prop.status == CheckStatus::Failure + }) + .collect(), + _ => vec![], + }, + Self::FailUncoverable { .. } => properties + .iter() + .filter(|prop| { + prop.property_class() == "cover" && prop.status != CheckStatus::Satisfied + }) + .collect(), + } + } +} + /// Our (kani-driver) notions of CBMC results. #[derive(Debug)] pub struct VerificationResult { /// Whether verification should be considered to have succeeded, or have failed. pub status: VerificationStatus, /// The compact representation for failed properties - pub failed_properties: FailedProperties, + pub global_conditions: Vec, /// The parsed output, message by message, of CBMC. However, the `Result` message has been /// removed and is available in `results` instead. pub messages: Option>, @@ -93,7 +175,12 @@ impl KaniSession { ) })?; - VerificationResult::from(output, harness.attributes.should_panic, start_time) + VerificationResult::from( + output, + harness.attributes.should_panic, + self.args.fail_uncoverable, + start_time, + ) }; Ok(verification_results) @@ -251,17 +338,18 @@ impl VerificationResult { fn from( output: VerificationOutput, should_panic: bool, + fail_uncoverable: bool, start_time: Instant, ) -> VerificationResult { let runtime = start_time.elapsed(); let (items, results) = extract_results(output.processed_items); if let Some(results) = results { - let (status, failed_properties) = - verification_outcome_from_properties(&results, should_panic); + let (status, global_conditions) = + verification_outcome_from_properties(&results, should_panic, fail_uncoverable); VerificationResult { status, - failed_properties, + global_conditions, messages: Some(items), results: Ok(results), runtime, @@ -271,7 +359,7 @@ impl VerificationResult { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure VerificationResult { status: VerificationStatus::Failure, - failed_properties: FailedProperties::Other, + global_conditions: vec![], messages: Some(items), results: Err(output.process_status), runtime, @@ -283,7 +371,7 @@ impl VerificationResult { pub fn mock_success() -> VerificationResult { VerificationResult { status: VerificationStatus::Success, - failed_properties: FailedProperties::None, + global_conditions: vec![], messages: None, results: Ok(vec![]), runtime: Duration::from_secs(0), @@ -294,7 +382,7 @@ impl VerificationResult { fn mock_failure() -> VerificationResult { VerificationResult { status: VerificationStatus::Failure, - failed_properties: FailedProperties::Other, + global_conditions: vec![], messages: None, // on failure, exit codes in theory might be used, // but `mock_failure` should never be used in a context where they will, @@ -305,22 +393,16 @@ impl VerificationResult { } } - pub fn render( - &self, - output_format: &OutputFormat, - should_panic: bool, - coverage_mode: bool, - ) -> String { + pub fn render(&self, output_format: &OutputFormat, coverage_mode: bool) -> String { match &self.results { Ok(results) => { let status = self.status; - let failed_properties = self.failed_properties; + let global_conditions = &self.global_conditions; let show_checks = matches!(output_format, OutputFormat::Regular); - let mut result = if coverage_mode { - format_coverage(results, status, should_panic, failed_properties, show_checks) + format_coverage(results, status, global_conditions, show_checks) } else { - format_result(results, status, should_panic, failed_properties, show_checks) + format_result(results, status, global_conditions, show_checks) }; writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap(); result @@ -358,20 +440,56 @@ impl VerificationResult { fn verification_outcome_from_properties( properties: &[Property], should_panic: bool, -) -> (VerificationStatus, FailedProperties) { + fail_uncoverable: bool, +) -> (VerificationStatus, Vec) { + // Compute the results for all global conditions + let should_panic_cond = compute_should_panic_condition(should_panic, properties); + let fail_uncoverable_cond = compute_fail_uncoverable_condition(fail_uncoverable, properties); + // Create a vector with results for global conditions + let global_conditions = vec![should_panic_cond, fail_uncoverable_cond]; + // Determine the overall outcome taking into account all global conditions + let status = outcome_from_global_conditions(properties, &global_conditions); + (status, global_conditions) +} + +fn compute_should_panic_condition(enabled: bool, properties: &[Property]) -> GlobalCondition { let failed_properties = determine_failed_properties(properties); - let status = if should_panic { - match failed_properties { - FailedProperties::None | FailedProperties::Other => VerificationStatus::Failure, - FailedProperties::PanicsOnly => VerificationStatus::Success, + GlobalCondition::ShouldPanic { enabled, status: failed_properties } +} + +fn compute_fail_uncoverable_condition(enabled: bool, properties: &[Property]) -> GlobalCondition { + let failed_covers = determine_satisfiable_covers(properties); + GlobalCondition::FailUncoverable { enabled, status: failed_covers } +} + +// Determine the overall verification result considering the enabled global conditions +fn outcome_from_global_conditions( + properties: &[Property], + global_conditions: &[GlobalCondition], +) -> VerificationStatus { + let enabled_global_conditions = !global_conditions + .iter() + .filter(|cond| cond.enabled()) + .collect::>() + .is_empty(); + + if !enabled_global_conditions { + // If no global conditions are enabled, the outcome only depends on failed properties + let failed_properties = determine_failed_properties(properties); + if failed_properties == FailedProperties::None { + VerificationStatus::Success + } else { + VerificationStatus::Failure } } else { - match failed_properties { - FailedProperties::None => VerificationStatus::Success, - FailedProperties::PanicsOnly | FailedProperties::Other => VerificationStatus::Failure, + let all_global_conditions_passed = + global_conditions.iter().all(|cond| if cond.enabled() { cond.passed() } else { true }); + if all_global_conditions_passed { + VerificationStatus::Success + } else { + VerificationStatus::Failure } - }; - (status, failed_properties) + } } /// Determines the `FailedProperties` variant that corresponds to an array of properties @@ -394,6 +512,17 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties { } } +/// Determines the `CoverStatus` variant that corresponds to an array of properties +fn determine_satisfiable_covers(properties: &[Property]) -> CoversStatus { + let cover_properties: Vec<&Property> = + properties.iter().filter(|prop| prop.property_class() == "cover").collect(); + if cover_properties.iter().all(|prop| prop.status == CheckStatus::Satisfied) { + CoversStatus::AllSatisfied + } else { + CoversStatus::Other + } +} + /// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind) pub fn resolve_unwind_value( args: &VerificationArgs, diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 62ef748a1ad5..71d1d50d44bb 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::args::OutputFormat; -use crate::call_cbmc::{FailedProperties, VerificationStatus}; +use crate::call_cbmc::{GlobalCondition, VerificationStatus}; use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem}; use console::style; use once_cell::sync::Lazy; @@ -255,8 +255,7 @@ fn format_item_terse(_item: &ParserItem) -> Option { pub fn format_result( properties: &Vec, status: VerificationStatus, - should_panic: bool, - failed_properties: FailedProperties, + global_conditions: &Vec, show_checks: bool, ) -> String { let mut result_str = String::new(); @@ -332,6 +331,39 @@ pub fn format_result( index += 1; } + let enabled_global_conditions = !global_conditions + .iter() + .filter(|cond| cond.enabled()) + .collect::>() + .is_empty(); + + let mut global_condition_failures = false; + if enabled_global_conditions { + result_str.push_str("GLOBAL CONDITIONS:\n"); + for cond in global_conditions { + if cond.enabled() { + let (cond_status, blame_properties) = if cond.passed() { + (CheckStatus::Success, None) + } else { + global_condition_failures = true; + (CheckStatus::Failure, Some(cond.blame_properties(&properties))) + }; + result_str.push_str(&format!( + " - {}: {} ({})\n", + cond.name(), + cond_status, + cond.reason() + )); + if !cond.passed() { + for prop in blame_properties.unwrap() { + let failure_message = + build_failure_message(prop.description.clone(), &prop.trace.clone()); + result_str.push_str(&failure_message); + } + } + } + } + } if show_checks { result_str.push_str("\nSUMMARY:"); } else { @@ -398,19 +430,14 @@ pub fn format_result( } else { style("FAILED").red() }; - let should_panic_info = if should_panic { - match failed_properties { - FailedProperties::None => " (encountered no panics, but at least one was expected)", - FailedProperties::PanicsOnly => " (encountered one or more panics as expected)", - FailedProperties::Other => { - " (encountered failures other than panics, which were unexpected)" - } - } - } else { - "" - }; - let overall_result = format!("\nVERIFICATION:- {verification_result}{should_panic_info}\n"); + + let overall_result = format!("\nVERIFICATION:- {verification_result}"); + result_str.push_str(&overall_result); + if global_condition_failures { + result_str.push_str(" (one or more global conditions failed)"); + } + result_str.push('\n'); // Ideally, we should generate two `ParserItem::Message` and push them // into the parser iterator so they are the next messages to be processed. @@ -436,15 +463,14 @@ pub fn format_result( pub fn format_coverage( properties: &[Property], status: VerificationStatus, - should_panic: bool, - failed_properties: FailedProperties, + global_conditions: &Vec, 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); + format_result(&non_coverage_checks, status, global_conditions, show_checks); let coverage_output = format_result_coverage(&coverage_checks); let result = format!("{}\n{}", verification_output, coverage_output); diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 2cd8bb7cbd70..51202faa4250 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -122,14 +122,7 @@ impl KaniSession { // When quiet, we don't want to print anything at all. // When output is old, we also don't have real results to print. if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { - println!( - "{}", - result.render( - &self.args.output_format, - harness.attributes.should_panic, - self.args.coverage - ) - ); + println!("{}", result.render(&self.args.output_format, self.args.coverage)); } self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) diff --git a/tests/ui/fail-uncoverable/all-covered/expected b/tests/ui/fail-uncoverable/all-covered/expected new file mode 100644 index 000000000000..08619ce04aae --- /dev/null +++ b/tests/ui/fail-uncoverable/all-covered/expected @@ -0,0 +1,10 @@ + +harness1.cover.1\ +Status: SATISFIED\ +Description: "cover location" +harness2.cover.1\ +Status: SATISFIED\ +Description: "cover condition: x == 1" +GLOBAL CONDITIONS:\ + - fail_uncoverable: SUCCESS (all cover statements were satisfied as expected) +Complete - 2 successfully verified harnesses, 0 failures, 2 total. \ No newline at end of file diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs new file mode 100644 index 000000000000..2708c2870590 --- /dev/null +++ b/tests/ui/fail-uncoverable/all-covered/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-unstable --fail-uncoverable + +//! Checks that all cover statements are satisfied and enabling +//! `--fail-uncoverable` doesn't cause unexpected failures. + +#[kani::proof] +fn harness1() { + kani::cover!(); +} + +#[kani::proof] +fn harness2() { + let x: u32 = kani::any(); + kani::cover!(x == 1); +} diff --git a/tests/ui/fail-uncoverable/uncoverable/expected b/tests/ui/fail-uncoverable/uncoverable/expected new file mode 100644 index 000000000000..3bbe34073732 --- /dev/null +++ b/tests/ui/fail-uncoverable/uncoverable/expected @@ -0,0 +1,7 @@ + +harness_uncoverable.cover.1\ +Status: UNREACHABLE\ +Description: "cover location" +GLOBAL CONDITIONS:\ + - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied) +VERIFICATION:- FAILED (one or more global conditions failed) \ No newline at end of file diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs new file mode 100644 index 000000000000..dfde7f6eedb3 --- /dev/null +++ b/tests/ui/fail-uncoverable/uncoverable/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-unstable --fail-uncoverable + +//! Checks that enabling the `--fail-uncoverable` option triggers a +//! condition-based failure due to a `cover` statement not being satisfied. +//! +//! Note: The `cover` statement isn't satisfied because it's unreachable. + +#[kani::proof] +fn harness_uncoverable() { + let x: i32 = kani::any(); + kani::assume(x >= 0); + if x < 0 { + kani::cover!(); + } +} diff --git a/tests/ui/fail-uncoverable/unsatisfied/expected b/tests/ui/fail-uncoverable/unsatisfied/expected new file mode 100644 index 000000000000..87de3ca9d023 --- /dev/null +++ b/tests/ui/fail-uncoverable/unsatisfied/expected @@ -0,0 +1,7 @@ + +harness_unsatisfied.cover.1\ +Status: UNSATISFIABLE\ +Description: "cover condition: x == -1" +GLOBAL CONDITIONS:\ + - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied) +VERIFICATION:- FAILED (one or more global conditions failed) \ No newline at end of file diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs new file mode 100644 index 000000000000..a8e2bb689510 --- /dev/null +++ b/tests/ui/fail-uncoverable/unsatisfied/test.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-unstable --fail-uncoverable + +//! Checks that enabling the `--fail-uncoverable` option triggers a +//! condition-based failure due to a `cover` statement not being satisfied. +//! +//! Note: The `cover` statement isn't satisfied because the condition `x == -1` +//! cannot be satisfied. + +#[kani::proof] +fn harness_unsatisfied() { + let x: i32 = kani::any(); + kani::assume(x >= 0); + kani::cover!(x == -1); +} diff --git a/tests/ui/should-panic-attribute/expected-panics/expected b/tests/ui/should-panic-attribute/expected-panics/expected index 855801a7c0df..83c2c0f2f95c 100644 --- a/tests/ui/should-panic-attribute/expected-panics/expected +++ b/tests/ui/should-panic-attribute/expected-panics/expected @@ -1,4 +1,6 @@ ** 2 of 2 failed Failed Checks: panicked on the `if` branch! Failed Checks: panicked on the `else` branch! -VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +GLOBAL CONDITIONS:\ + - should_panic: SUCCESS (encountered one or more panics as expected) +VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected index be42df7fb7f6..8ce1a5a34b67 100644 --- a/tests/ui/should-panic-attribute/no-panics/expected +++ b/tests/ui/should-panic-attribute/no-panics/expected @@ -1,5 +1,6 @@ check.assertion\ SUCCESS\ assertion failed: 1 + 1 == 2 - -VERIFICATION:- FAILED (encountered no panics, but at least one was expected) +GLOBAL CONDITIONS:\ + - should_panic: FAILURE (encountered no panics, but at least one was expected) +VERIFICATION:- FAILED (one or more global conditions failed) diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected index b3a4cb77c6ae..909b3dafd87a 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/expected +++ b/tests/ui/should-panic-attribute/unexpected-failures/expected @@ -2,8 +2,11 @@ arithmetic_overflow\ Status: FAILURE\ Description: "attempt to shift by excessive shift distance" +GLOBAL CONDITIONS:\ + - should_panic: FAILURE (encountered failures other than panics, which were unexpected) + Failed Checks: panicked on the `1` arm! Failed Checks: panicked on the `0` arm! Failed Checks: attempt to shift by excessive shift distance -VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) +VERIFICATION:- FAILED (one or more global conditions failed)