Improve summary printing

Separate messages for autoverify vs. manual verification

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 {

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

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.

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.
+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.

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...
 <usize as std::slice::SliceIndex<[i32]>>::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...
 <usize as std::slice::SliceIndex<[i32]>>::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.

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?