Print tables of which functions we verified and which we skipped

kani-driver/src/autoharness/mod.rs

@@ -4,15 +4,89 @@
 use std::str::FromStr;
 
 use crate::args::Timeout;
+use crate::args::autoharness_args::{CargoAutoharnessArgs, StandaloneAutoharnessArgs};
 use crate::call_cbmc::VerificationStatus;
 use crate::call_single_file::to_rustc_arg;
 use crate::harness_runner::HarnessResult;
 use crate::session::KaniSession;
+use crate::{InvocationType, print_kani_version, project, verify_project};
 use anyhow::Result;
+use comfy_table::Table as PrettyTable;
+use kani_metadata::{AutoHarnessSkipReason, KaniMetadata};
 
 const AUTOHARNESS_TIMEOUT: &str = "30s";
 const LOOP_UNWIND_DEFAULT: u32 = 20;
 
+pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> {
+    let mut session = KaniSession::new(args.verify_opts)?;
+    session.enable_autoharness();
+    session.add_default_bounds();
+    session.add_auto_harness_args(
+        args.common_autoharness_args.include_function,
+        args.common_autoharness_args.exclude_function,
+    );
+    let project = project::cargo_project(&mut session, false)?;
+    let metadata = project.metadata.clone();
+    let res = verify_project(project, session);
+    print_skipped_fns(metadata);
+    res
+}
+
+pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
+    let mut session = KaniSession::new(args.verify_opts)?;
+    session.enable_autoharness();
+    session.add_default_bounds();
+    session.add_auto_harness_args(
+        args.common_autoharness_args.include_function,
+        args.common_autoharness_args.exclude_function,
+    );
+
+    if !session.args.common_args.quiet {
+        print_kani_version(InvocationType::Standalone);
+    }
+
+    let project = project::standalone_project(&args.input, args.crate_name, &session)?;
+    let metadata = project.metadata.clone();
+    let res = verify_project(project, session);
+    print_skipped_fns(metadata);
+    res
+}
+
+/// Print a table of the functions that we skipped and why.
+fn print_skipped_fns(metadata: Vec<KaniMetadata>) {
+    let mut skipped_fns = PrettyTable::new();
+    skipped_fns.set_header(vec!["Skipped Function", "Reason for Skipping"]);
+
+    for md in metadata {
+        let skipped_md = md.autoharness_skipped_fns.unwrap();
+        skipped_fns.add_rows(skipped_md.into_iter().filter_map(|(func, reason)| match reason {
+            AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => {
+                Some(vec![func, format!("{}: {}", reason, args.join(", "))])
+            }
+            AutoHarnessSkipReason::GenericFn
+            | AutoHarnessSkipReason::NoBody
+            | AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]),
+            // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation.
+            // For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations),
+            // it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful.
+            AutoHarnessSkipReason::KaniImpl => None,
+        }));
+    }
+
+    if skipped_fns.is_empty() {
+        println!(
+            "\nSkipped Functions: None. Kani generated automatic harnesses for all functions in the package."
+        );
+        return;
+    }
+
+    println!("\nKani did not generate automatic harnesses for the following functions.");
+    println!(
+        "If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832"
+    );
+    println!("{skipped_fns}");
+}
+
 impl KaniSession {
     /// Enable autoharness mode.
     pub fn enable_autoharness(&mut self) {
@@ -54,46 +128,50 @@ impl KaniSession {
 
         // TODO: it would be nice if we had access to which functions the user included/excluded here
         // so that we could print a comparison for them of any of the included functions that we skipped.
-        println!("Autoharness Summary:");
-        println!(
-            "Note that Kani will only generate an automatic harness for a function if it determines that each of its arguments implement the Arbitrary trait."
-        );
-        println!(
-            "Examine the summary closely to determine which functions were automatically verified."
-        );
-        if failing > 0 {
-            println!(
-                "Also note that Kani sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}."
-            );
-            println!(
-                "If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract)."
-            );
-        }
+        println!("\nAutoharness Summary:");
+
+        let mut verified_fns = PrettyTable::new();
+        verified_fns.set_header(vec![
+            "Selected Function",
+            "Kind of Automatic Harness",
+            "Verification Result",
+        ]);
 
-        // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place.
         for success in successes {
-            println!("Verification succeeded for - {}", success.harness.pretty_name);
+            verified_fns.add_row(vec![
+                success.harness.pretty_name.clone(),
+                success.harness.attributes.kind.to_string(),
+                success.result.status.to_string(),
+            ]);
         }
 
         for failure in failures {
-            println!("Verification failed for - {}", failure.harness.pretty_name);
+            verified_fns.add_row(vec![
+                failure.harness.pretty_name.clone(),
+                failure.harness.attributes.kind.to_string(),
+                failure.result.status.to_string(),
+            ]);
         }
 
-        if total > 0 {
+        println!("{verified_fns}");
+
+        if failing > 0 {
             println!(
-                "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
+                "Note that `kani autoharness` sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}."
             );
-        } else {
             println!(
-                "No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."
+                "If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract)."
             );
+        }
+
+        if total > 0 {
             println!(
-                "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive."
+                "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
             );
+        } else {
+            println!("No functions were eligible for automatic verification.");
         }
 
-        // Manual harness summary may come afterward, so separate them with a new line.
-        println!();
         Ok(())
     }
 }

kani-driver/src/call_cbmc.rs

@@ -12,6 +12,7 @@ use std::fmt::Write;
 use std::path::Path;
 use std::sync::OnceLock;
 use std::time::{Duration, Instant};
+use strum_macros::Display;
 use tokio::process::Command as TokioCommand;
 
 use crate::args::common::Verbosity;
@@ -29,7 +30,7 @@ use crate::util::render_command;
 /// Note: Kissat was marginally better, but it is an external solver which could be more unstable.
 static DEFAULT_SOLVER: CbmcSolver = CbmcSolver::Cadical;
 
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+#[derive(Clone, Copy, Debug, Display, PartialEq, Eq)]
 pub enum VerificationStatus {
     Success,
     Failure,

kani-driver/src/harness_runner.rs

@@ -246,10 +246,6 @@ impl KaniSession {
         let (automatic, manual): (Vec<_>, Vec<_>) =
             results.iter().partition(|r| r.harness.is_automatically_generated);
 
-        if self.auto_harness {
-            self.print_autoharness_summary(automatic)?;
-        }
-
         let (successes, failures): (Vec<_>, Vec<_>) =
             manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
 
@@ -269,10 +265,8 @@ impl KaniSession {
             }
         }
 
-        // We currently omit a summary if there was just 1 harness
-        if failing > 0 {
-            println!("Manual Harness Summary:");
-        }
+        println!("Manual Harness Summary:");
+
         for failure in failures.iter() {
             println!("Verification failed for - {}", failure.harness.pretty_name);
         }
@@ -304,7 +298,11 @@ impl KaniSession {
             self.show_coverage_summary()?;
         }
 
-        if failing > 0 {
+        if self.auto_harness {
+            self.print_autoharness_summary(automatic)?;
+        }
+
+        if failing > 0 && !self.auto_harness {
             // Failure exit code without additional error message
             drop(self);
             std::process::exit(1);

kani-driver/src/main.rs

@@ -5,6 +5,7 @@ use std::ffi::OsString;
 use std::process::ExitCode;
 
 use anyhow::Result;
+use autoharness::{autoharness_cargo, autoharness_standalone};
 use time::{OffsetDateTime, format_description};
 
 use args::{CargoKaniSubcommand, check_is_valid};
@@ -73,26 +74,21 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         return list_cargo(*list_args, args.verify_opts);
     }
 
+    if let Some(CargoKaniSubcommand::Autoharness(autoharness_args)) = args.command {
+        return autoharness_cargo(*autoharness_args);
+    }
+
     let mut session = match args.command {
         Some(CargoKaniSubcommand::Assess(assess_args)) => {
             let sess = session::KaniSession::new(args.verify_opts)?;
             return assess::run_assess(sess, *assess_args);
         }
-        Some(CargoKaniSubcommand::Autoharness(args)) => {
-            let mut sess = session::KaniSession::new(args.verify_opts)?;
-            sess.enable_autoharness();
-            sess.add_default_bounds();
-            sess.add_auto_harness_args(
-                args.common_autoharness_args.include_function,
-                args.common_autoharness_args.exclude_function,
-            );
-
-            sess
-        }
         Some(CargoKaniSubcommand::Playback(args)) => {
             return playback_cargo(*args);
         }
-        Some(CargoKaniSubcommand::List(_)) => unreachable!(),
+        Some(CargoKaniSubcommand::Autoharness(_)) | Some(CargoKaniSubcommand::List(_)) => {
+            unreachable!()
+        }
         None => session::KaniSession::new(args.verify_opts)?,
     };
 
@@ -115,20 +111,7 @@ fn standalone_main() -> Result<()> {
 
     let (session, project) = match args.command {
         Some(StandaloneSubcommand::Autoharness(args)) => {
-            let mut session = KaniSession::new(args.verify_opts)?;
-            session.enable_autoharness();
-            session.add_default_bounds();
-            session.add_auto_harness_args(
-                args.common_autoharness_args.include_function,
-                args.common_autoharness_args.exclude_function,
-            );
-
-            if !session.args.common_args.quiet {
-                print_kani_version(InvocationType::Standalone);
-            }
-
-            let project = project::standalone_project(&args.input, args.crate_name, &session)?;
-            (session, project)
+            return autoharness_standalone(*args);
         }
         Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args),
         Some(StandaloneSubcommand::List(list_args)) => {

kani_metadata/src/harness.rs

@@ -4,6 +4,7 @@
 use crate::CbmcSolver;
 use serde::{Deserialize, Serialize};
 use std::path::PathBuf;
+use strum_macros::Display;
 
 /// A CBMC-level `assigns` contract that needs to be enforced on a function.
 #[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
@@ -59,13 +60,16 @@ pub struct HarnessAttributes {
     pub verified_stubs: Vec<String>,
 }
 
-#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
+#[derive(Clone, Eq, PartialEq, Debug, Display, Serialize, Deserialize)]
 pub enum HarnessKind {
     /// Function was annotated with `#[kani::proof]`.
+    #[strum(serialize = "#[kani::proof]")]
     Proof,
     /// Function was annotated with `#[kani::proof_for_contract(target_fn)]`.
+    #[strum(serialize = "#[kani::proof_for_contract]")]
     ProofForContract { target_fn: String },
     /// This is a test harness annotated with `#[test]`.
+    #[strum(serialize = "#[test]")]
     Test,
 }
 

tests/script-based-pre/cargo_autoharness_contracts/contracts.expected

@@ -3,26 +3,42 @@ assertion\
 	 - Status: FAILURE\
 	 - Description: "|result : &u32| *result == x"
 
-Autoharness: Checking function should_pass::has_loop_contract's contract against all possible inputs...
-should_pass::has_loop_contract.assertion\
-	 - Status: SUCCESS\
-	 - Description: "assertion failed: x == 2"
+Autoharness: Checking function should_pass::div's contract against all possible inputs...
 
 Autoharness: Checking function should_pass::has_recursion_gcd's contract against all possible inputs...
 assertion\
 	 - Status: SUCCESS\
 	 - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0"
 
-Autoharness: Checking function should_pass::div's contract against all possible inputs...
-
 Autoharness: Checking function should_pass::unchecked_mul's contract against all possible inputs...
 arithmetic_overflow\
 	 - Status: SUCCESS\
 	 - Description: "attempt to compute `unchecked_mul` which would overflow"
 
-Verification succeeded for - should_pass::unchecked_mul
-Verification succeeded for - should_pass::has_loop_contract
-Verification succeeded for - should_pass::has_recursion_gcd
-Verification succeeded for - should_pass::div
-Verification failed for - should_fail::max
+Autoharness: Checking function should_pass::has_loop_contract against all possible inputs...
+should_pass::has_loop_contract.assertion\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: x == 2"
+
+Manual Harness Summary:
+No proof harnesses (functions with #[kani::proof]) were found to verify.
+
+Autoharness Summary:
++--------------------------------+-----------------------------+---------------------+
+| Selected Function              | Kind of Automatic Harness   | Verification Result |
++====================================================================================+
+| should_pass::unchecked_mul     | #[kani::proof_for_contract] | Success             |
+|--------------------------------+-----------------------------+---------------------|
+| should_pass::has_loop_contract | #[kani::proof]              | Success             |
+|--------------------------------+-----------------------------+---------------------|
+| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success             |
+|--------------------------------+-----------------------------+---------------------|
+| should_pass::div               | #[kani::proof_for_contract] | Success             |
+|--------------------------------+-----------------------------+---------------------|
+| should_fail::max               | #[kani::proof_for_contract] | Failure             |
++--------------------------------+-----------------------------+---------------------+
+Note that `kani autoharness` sets default --harness-timeout of 30s and --default-unwind of 20.
+If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract).
 Complete - 4 successfully verified functions, 1 failures, 5 total.
+
+Skipped Functions: None. Kani generated automatic harnesses for all functions in the package.

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected

@@ -1,3 +1,14 @@
 Autoharness: Checking function yes_harness against all possible inputs...
-Verification succeeded for - yes_harness
+
+Manual Harness Summary:
+No proof harnesses (functions with #[kani::proof]) were found to verify.
+
+Autoharness Summary:
++-------------------+---------------------------+---------------------+
+| Selected Function | Kind of Automatic Harness | Verification Result |
++=====================================================================+
+| yes_harness       | #[kani::proof]            | Success             |
++-------------------+---------------------------+---------------------+
 Complete - 1 successfully verified functions, 0 failures, 1 total.
+
+Skipped Functions: None. Kani generated automatic harnesses for all functions in the package.