diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 320d574a01f8..905910b54f06 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -11,7 +11,7 @@ use std::path::Path; use crate::args::OutputFormat; use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; -use crate::session::KaniSession; +use crate::session::{BUG_REPORT_URL, KaniSession}; use std::env::current_dir; use std::path::PathBuf; @@ -170,7 +170,7 @@ impl KaniSession { // If the harness is automatically generated, pretty_name refers to the function under verification. let mut msg = if harness.is_automatically_generated { format!( - "Automatic verification: Checking function {} against all possible inputs...", + "Autoverify: Checking function {} against all possible inputs...", harness.pretty_name ) } else { @@ -190,60 +190,99 @@ impl KaniSession { Ok(result) } + /// Prints the results from running the `autoverify` subcommand. + fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { + let (successes, failures): (Vec<_>, Vec<_>) = + automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); + + let succeeding = successes.len(); + let failing = failures.len(); + let total = succeeding + failing; + + if failing > 0 { + println!("Summary:"); + } + for failure in failures.iter() { + println!("Verification failed for - {}", failure.harness.pretty_name); + } + + if total > 0 { + println!( + "Autoverify: Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." + ); + } else { + println!(" + Autoverify: No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."); + } + + Ok(()) + } + /// Concludes a session by printing a summary report and exiting the process with an /// error code (if applicable). /// /// Note: Takes `self` "by ownership". This function wants to be able to drop before /// exiting with an error code, if needed. pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> { + if self.args.common_args.quiet { + return Ok(()); + } + + let (automatic, manual): (Vec<_>, Vec<_>) = + results.iter().partition(|r| r.harness.is_automatically_generated); + + if self.auto_verify { + self.print_autoverify_summary(automatic)?; + } + let (successes, failures): (Vec<_>, Vec<_>) = - results.iter().partition(|r| r.result.status == VerificationStatus::Success); + manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success); let succeeding = successes.len(); let failing = failures.len(); let total = succeeding + failing; - if self.args.concrete_playback.is_some() - && !self.args.common_args.quiet - && results.iter().all(|r| !r.result.generated_concrete_test) - { - println!( - "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." - ) + if self.args.concrete_playback.is_some() { + if failures.is_empty() { + println!( + "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." + ) + } else if failures.iter().all(|r| !r.result.generated_concrete_test) { + eprintln!( + "The concrete playback feature did not generate unit tests, but there were failing harnesses. Please file a bug report at {BUG_REPORT_URL}" + ) + } } // We currently omit a summary if there was just 1 harness - if !self.args.common_args.quiet { - if failing > 0 { - println!("Summary:"); - } - for failure in failures.iter() { - println!("Verification failed for - {}", failure.harness.pretty_name); - } + if failing > 0 { + println!("Summary:"); + } + for failure in failures.iter() { + println!("Verification failed for - {}", failure.harness.pretty_name); + } - if total > 0 { - println!( - "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." - ); - } else { - match self.args.harnesses.as_slice() { - [] => - // TODO: This could use a better message, possibly with links to Kani documentation. - // New users may encounter this and could use a pointer to how to write proof harnesses. - { - println!( - "No proof harnesses (functions with #[kani::proof]) were found to verify." - ) - } - [harness] => { - bail!("no harnesses matched the harness filter: `{harness}`") - } - harnesses => bail!( - "no harnesses matched the harness filters: `{}`", - harnesses.join("`, `") - ), - }; - } + if total > 0 { + println!( + "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." + ); + } else { + match self.args.harnesses.as_slice() { + [] => + // TODO: This could use a better message, possibly with links to Kani documentation. + // New users may encounter this and could use a pointer to how to write proof harnesses. + { + println!( + "No proof harnesses (functions with #[kani::proof]) were found to verify." + ) + } + [harness] => { + bail!("no harnesses matched the harness filter: `{harness}`") + } + harnesses => { + bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) + } + }; } if self.args.coverage { diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index db2a98358e45..9c2e8e5ced0c 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -23,6 +23,9 @@ use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; /// `export KANI_LOG=kani_driver=debug`. const LOG_ENV_VAR: &str = "KANI_LOG"; +pub const BUG_REPORT_URL: &str = + "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md"; + /// Contains information about the execution environment and arguments that affect operations pub struct KaniSession { /// The common command-line arguments diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected index c8bf50d6a0d1..314b4b6fad9e 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected @@ -1,19 +1,19 @@ -Checking function should_fail::max against all possible inputs... +Autoverify: Checking function should_fail::max against all possible inputs... assertion\ - Status: FAILURE\ - Description: "|result : &u32| *result == x" -Checking function should_pass::has_loop_contract against all possible inputs... +Autoverify: Checking function should_pass::has_loop_contract against all possible inputs... should_pass::has_loop_contract.assertion\ - Status: SUCCESS\ - Description: "assertion failed: x == 2" -Checking function should_pass::has_recursion_gcd against all possible inputs... +Autoverify: Checking function should_pass::has_recursion_gcd against all possible inputs... assertion\ - Status: SUCCESS\ - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" -Checking function should_pass::div against all possible inputs... +Autoverify: Checking function should_pass::div against all possible inputs... Verification failed for - should_fail::max -Complete - 3 successfully verified harnesses, 1 failures, 4 total. +Autoverify: Complete - 3 successfully verified functions, 1 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected index e960e9180e91..ee74fa8d5ad6 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.expected @@ -1,40 +1,40 @@ -Automatic verification: Checking function yes_harness::f_tuple against all possible inputs... -Automatic verification: Checking function yes_harness::f_maybe_uninit against all possible inputs... -Automatic verification: Checking function yes_harness::f_result against all possible inputs... -Automatic verification: Checking function yes_harness::f_option against all possible inputs... -Automatic verification: Checking function yes_harness::f_array against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_isize against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_usize against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_char against all possible inputs... -Automatic verification: Checking function yes_harness::f_bool against all possible inputs... -Automatic verification: Checking function yes_harness::f_isize against all possible inputs... -Automatic verification: Checking function yes_harness::f_i128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_usize against all possible inputs... -Automatic verification: Checking function yes_harness::f_u128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_unsupported_return_type against all possible inputs... -Automatic verification: Checking function yes_harness::f_multiple_args against all possible inputs... -Automatic verification: Checking function yes_harness::f_derives_arbitrary against all possible inputs... -Automatic verification: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... -Complete - 39 successfully verified harnesses, 0 failures, 39 total. \ No newline at end of file +Autoverify: Checking function yes_harness::f_tuple against all possible inputs... +Autoverify: Checking function yes_harness::f_maybe_uninit against all possible inputs... +Autoverify: Checking function yes_harness::f_result against all possible inputs... +Autoverify: Checking function yes_harness::f_option against all possible inputs... +Autoverify: Checking function yes_harness::f_array against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_isize against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i128 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i64 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i32 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i16 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i8 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_usize against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u128 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u64 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u32 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u16 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u8 against all possible inputs... +Autoverify: Checking function yes_harness::f_f128 against all possible inputs... +Autoverify: Checking function yes_harness::f_f16 against all possible inputs... +Autoverify: Checking function yes_harness::f_f64 against all possible inputs... +Autoverify: Checking function yes_harness::f_f32 against all possible inputs... +Autoverify: Checking function yes_harness::f_char against all possible inputs... +Autoverify: Checking function yes_harness::f_bool against all possible inputs... +Autoverify: Checking function yes_harness::f_isize against all possible inputs... +Autoverify: Checking function yes_harness::f_i128 against all possible inputs... +Autoverify: Checking function yes_harness::f_i64 against all possible inputs... +Autoverify: Checking function yes_harness::f_i32 against all possible inputs... +Autoverify: Checking function yes_harness::f_i16 against all possible inputs... +Autoverify: Checking function yes_harness::f_i8 against all possible inputs... +Autoverify: Checking function yes_harness::f_usize against all possible inputs... +Autoverify: Checking function yes_harness::f_u128 against all possible inputs... +Autoverify: Checking function yes_harness::f_u64 against all possible inputs... +Autoverify: Checking function yes_harness::f_u32 against all possible inputs... +Autoverify: Checking function yes_harness::f_u16 against all possible inputs... +Autoverify: Checking function yes_harness::f_u8 against all possible inputs... +Autoverify: Checking function yes_harness::f_unsupported_return_type against all possible inputs... +Autoverify: Checking function yes_harness::f_multiple_args against all possible inputs... +Autoverify: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Autoverify: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Autoverify: Complete - 39 successfully verified functions, 0 failures, 39 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected index 520d6d6c94b8..8e5400a5edae 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected @@ -1,47 +1,42 @@ -Checking harness panic_harness... -panic.assertion\ +Autoverify: Checking function panic against all possible inputs... +Check 1: panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" -Checking harness integer_overflow_harness... +Autoverify: Checking function integer_overflow against all possible inputs... assertion\ - - Status: FAILURE\ + - Status: FAILURE - Description: "attempt to add with overflow" -Checking harness oob_unsafe_array_access_harness... +Autoverify: Checking function oob_unsafe_array_access against all possible inputs... oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ + - Description: "dereference failure: pointer outside object bounds" -Checking harness oob_safe_array_access_harness... - +Autoverify: Checking function oob_safe_array_access against all possible inputs... >::index.assertion\ - Status: FAILURE\ - Description: "index out of bounds: the length is less than or equal to the given index" +Autoverify: Complete - 0 successfully verified functions, 4 failures, 4 total. -Checking function panic against all possible inputs... - -Check 1: panic.assertion\ +Checking harness panic_harness... +panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" -Checking function integer_overflow against all possible inputs... - +Checking harness integer_overflow_harness... assertion\ - - Status: FAILURE + - Status: FAILURE\ - Description: "attempt to add with overflow" -Checking function oob_unsafe_array_access against all possible inputs... - +Checking harness oob_unsafe_array_access_harness... oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ - - Description: "dereference failure: pointer outside object bounds" - -Checking function oob_safe_array_access against all possible inputs... +Checking harness oob_safe_array_access_harness... >::index.assertion\ - Status: FAILURE\ - Description: "index out of bounds: the length is less than or equal to the given index" -Complete - 0 successfully verified harnesses, 8 failures, 8 total. - +Complete - 0 successfully verified harnesses, 4 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs index c91a4de37ca1..92e711eb5d0b 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zautomatic-harnesses // Test the bodies of the automatically generated harnesses: // do they catch the same failures as manual ones?