Add progress indicator and log file output for concise terminal output

When in an interactive terminal, `kani main.rs --log-file log.txt` will
now print:
```
$ kani main.rs --log-file log.txt
Kani Rust Verifier 0.66.0 (standalone)
  [00:00:00] [########################################] 2/2 (0s)
Verification complete | Succeeded: 2 | Failed: 0 | Timed out: 0                                                             Manual Harness Summary:
Complete - 2 successfully verified harnesses, 0 failures, 2 total.
```
where `########################################` will be updated up
until the run is complete. This enables users to more quickly grasp how
much work Kani has already completed, which may be particularly useful
when running thousands of harnesses with `autoharness`.

Co-authored-by: Kani autonomous agent

Author: tautschnig

Cargo.lock

@@ -866,6 +866,19 @@ dependencies = [
  "serde_core",
 ]
 
+[[package]]
+name = "indicatif"
+version = "0.18.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9375e112e4b463ec1b1c6c011953545c65a30164fbab5b581df32b3abf0dcb88"
+dependencies = [
+ "console",
+ "portable-atomic",
+ "unicode-width",
+ "unit-prefix",
+ "web-time",
+]
+
 [[package]]
 name = "indoc"
 version = "2.0.7"
@@ -1002,6 +1015,7 @@ dependencies = [
  "clap",
  "comfy-table",
  "console",
+ "indicatif",
  "kani_metadata",
  "once_cell",
  "pathdiff",
@@ -2377,6 +2391,12 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254"
 
+[[package]]
+name = "unit-prefix"
+version = "0.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "81e544489bf3d8ef66c953931f56617f423cd4b5494be343d9b9d3dda037b9a3"
+
 [[package]]
 name = "unsafe-libyaml"
 version = "0.2.11"
@@ -2480,6 +2500,16 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "web-time"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb"
+dependencies = [
+ "js-sys",
+ "wasm-bindgen",
+]
+
 [[package]]
 name = "which"
 version = "7.0.3"

kani-driver/Cargo.toml

@@ -36,6 +36,7 @@ which = "8"
 time = {version = "0.3.36", features = ["formatting"]}
 tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
 chrono = { version = "0.4.41", default-features = false, features = [ "clock" ]}
+indicatif = "0.18"
 
 
 # A good set of suggested dependencies can be found in rustup:

kani-driver/src/args/mod.rs

@@ -326,6 +326,12 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub output_into_files: bool,
 
+    /// Write verbose and terse log output to the specified file.
+    /// When enabled with an interactive terminal, progress indicator will be shown on terminal
+    /// while detailed logs are written to the file.
+    #[arg(long, value_name = "PATH")]
+    pub log_file: Option<PathBuf>,
+
     /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
     #[arg(long, hide = true)]
     pub print_llbc: bool,

kani-driver/src/call_cbmc.rs

@@ -9,6 +9,7 @@ use std::collections::BTreeMap;
 use std::collections::btree_map::Entry;
 use std::ffi::OsString;
 use std::fmt::Write;
+use std::io::IsTerminal;
 use std::path::Path;
 use std::sync::OnceLock;
 use std::time::{Duration, Instant};
@@ -120,6 +121,10 @@ impl KaniSession {
 
         let start_time = Instant::now();
 
+        // Determine if we should suppress terminal output (redirect to log file)
+        let suppress_terminal = self.args.log_file.is_some() && std::io::stdout().is_terminal();
+        let log_file_path = self.args.log_file.clone();
+
         let res = if let Some(timeout) = self.args.harness_timeout {
             tokio::time::timeout(
                 timeout.into(),
@@ -129,6 +134,8 @@ impl KaniSession {
                         self.args.extra_pointer_checks,
                         self.args.common_args.quiet,
                         &self.args.output_format,
+                        suppress_terminal,
+                        log_file_path.as_ref(),
                     )
                 }),
             )
@@ -140,6 +147,8 @@ impl KaniSession {
                     self.args.extra_pointer_checks,
                     self.args.common_args.quiet,
                     &self.args.output_format,
+                    suppress_terminal,
+                    log_file_path.as_ref(),
                 )
             })
             .await)

kani-driver/src/cbmc_property_renderer.rs

@@ -10,6 +10,9 @@ use once_cell::sync::Lazy;
 use regex::Regex;
 use rustc_demangle::demangle;
 use std::collections::HashMap;
+use std::fs::OpenOptions;
+use std::io::Write;
+use std::path::PathBuf;
 
 type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>;
 
@@ -165,12 +168,15 @@ impl ParserItem {
 /// filter and transform it into the format we expect.
 ///
 /// This will output "messages" live as they stream in if `output_format` is
-/// set to `regular` but will otherwise not print.
+/// set to `regular` but will otherwise not print. When `suppress_terminal` is true
+/// and a log file path is provided, output is redirected to the log file instead.
 pub fn kani_cbmc_output_filter(
     item: ParserItem,
     extra_ptr_checks: bool,
     quiet: bool,
     output_format: &OutputFormat,
+    suppress_terminal: bool,
+    log_file: Option<&PathBuf>,
 ) -> Option<ParserItem> {
     // Some items (e.g., messages) are skipped.
     // We could also process them and decide to skip later.
@@ -183,14 +189,34 @@ pub fn kani_cbmc_output_filter(
     if !quiet {
         let formatted_item = format_item(&processed_item, output_format);
         if let Some(fmt_item) = formatted_item {
-            println!("{fmt_item}");
+            if suppress_terminal {
+                // Write to log file instead of terminal
+                if let Some(log_path) = log_file {
+                    if let Err(e) = write_to_log_file(log_path, &fmt_item) {
+                        eprintln!(
+                            "Failed to write CBMC output to log file {}: {}",
+                            log_path.display(),
+                            e
+                        );
+                    }
+                }
+            } else {
+                // Normal terminal output
+                println!("{fmt_item}");
+            }
         }
     }
     // TODO: Record processed items and dump them into a JSON file
     // <https://github.com/model-checking/kani/issues/942>
     Some(processed_item)
 }
 
+/// Helper function to write output to log file
+fn write_to_log_file(log_file_path: &PathBuf, content: &str) -> std::io::Result<()> {
+    let mut file = OpenOptions::new().create(true).append(true).open(log_file_path)?;
+    writeln!(file, "{}", content)
+}
+
 /// Processes a `ParserItem`. In general, all items are returned as they are,
 /// except for:
 ///  * Error messages, which may be edited.

kani-driver/src/harness_runner.rs

@@ -5,11 +5,12 @@ use anyhow::{Error, Result, bail};
 use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata};
 use rayon::prelude::*;
 use std::fs::File;
-use std::io::Write;
+use std::io::{IsTerminal, Write};
 use std::path::Path;
 
 use crate::args::{NumThreads, OutputFormat};
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
+use crate::progress_indicator::ProgressIndicator;
 use crate::project::Project;
 use crate::session::{BUG_REPORT_URL, KaniSession};
 
@@ -56,6 +57,15 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
+
+        // Determine if we should show progress indicator
+        let show_progress = self.sess.args.log_file.is_some()
+            && !self.sess.args.common_args.quiet
+            && std::io::stdout().is_terminal();
+
+        // Create progress indicator
+        let progress_indicator = ProgressIndicator::new(sorted_harnesses.len(), show_progress);
+
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
             match self.sess.args.jobs() {
@@ -86,6 +96,15 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                     }
 
                     let result = self.sess.check_harness(goto_file, harness)?;
+
+                    // Update progress indicator if active
+                    if progress_indicator.is_active() {
+                        let succeeded = result.status == VerificationStatus::Success;
+                        let timed_out =
+                            matches!(&result.results, Err(crate::call_cbmc::ExitStatus::Timeout));
+                        progress_indicator.update_with_result(succeeded, timed_out);
+                    }
+
                     if self.sess.args.fail_fast && result.status == VerificationStatus::Failure {
                         Err(Error::new(FailFastHarnessInfo {
                             index_to_failing_harness: idx,
@@ -97,6 +116,10 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                 })
                 .collect::<Result<Vec<_>>>()
         });
+
+        // Finish progress indicator
+        progress_indicator.finish();
+
         match results {
             Ok(results) => Ok(results),
             Err(err) => {
@@ -127,14 +150,40 @@ impl KaniSession {
             }
 
             let output = result.render(&self.args.output_format, harness.attributes.should_panic);
-            if rayon::current_num_threads() > 1 {
-                println!("Thread {thread_index}: {output}");
+
+            // If log file is specified, write to log file instead of stdout
+            if let Some(ref log_file_path) = self.args.log_file {
+                self.write_to_log_file(log_file_path, &output, thread_index);
             } else {
-                println!("{output}");
+                // Normal stdout output
+                if rayon::current_num_threads() > 1 {
+                    println!("Thread {thread_index}: {output}");
+                } else {
+                    println!("{output}");
+                }
             }
         }
     }
 
+    fn write_to_log_file(&self, log_file_path: &PathBuf, output: &str, thread_index: usize) {
+        use std::fs::OpenOptions;
+
+        let result = OpenOptions::new().create(true).append(true).open(log_file_path).and_then(
+            |mut file| {
+                let formatted_output = if rayon::current_num_threads() > 1 {
+                    format!("Thread {thread_index}: {output}\n")
+                } else {
+                    format!("{output}\n")
+                };
+                file.write_all(formatted_output.as_bytes())
+            },
+        );
+
+        if let Err(e) = result {
+            eprintln!("Failed to write to log file {}: {}", log_file_path.display(), e);
+        }
+    }
+
     fn should_print_output(&self) -> bool {
         !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
     }
@@ -179,6 +228,10 @@ impl KaniSession {
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
         let thread_index = rayon::current_thread_index().unwrap_or_default();
+
+        // Determine if we should suppress console output (when using log file with progress indicator)
+        let suppress_console = self.args.log_file.is_some() && std::io::stdout().is_terminal();
+
         if !self.args.common_args.quiet {
             // If the harness is automatically generated, pretty_name refers to the function under verification.
             let mut msg = if harness.is_automatically_generated {
@@ -201,7 +254,12 @@ impl KaniSession {
                 msg = format!("Thread {thread_index}: {msg}");
             }
 
-            println!("{msg}");
+            // Write to log file if specified, otherwise to stdout
+            if let Some(ref log_file_path) = self.args.log_file {
+                self.write_to_log_file(log_file_path, &msg, thread_index);
+            } else if !suppress_console {
+                println!("{msg}");
+            }
         }
 
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;

kani-driver/src/main.rs

@@ -35,6 +35,7 @@ mod coverage;
 mod harness_runner;
 mod list;
 mod metadata;
+mod progress_indicator;
 mod project;
 mod session;
 mod util;