Add progress indicator and log file output for concise terminal output

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.47", 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

@@ -129,6 +129,7 @@ impl KaniSession {
                         self.args.extra_pointer_checks,
                         self.args.common_args.quiet,
                         &self.args.output_format,
+                        self.args.log_file.as_ref(),
                     )
                 }),
             )
@@ -140,6 +141,7 @@ impl KaniSession {
                     self.args.extra_pointer_checks,
                     self.args.common_args.quiet,
                     &self.args.output_format,
+                    self.args.log_file.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,14 @@ 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 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,
+    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 +188,30 @@ 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 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 {
+                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
     }
@@ -201,7 +250,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 {
+                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;