From e8efb27a2aefb066880ff84a4bdca7f34dd2a0c9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 12:38:40 +0000 Subject: [PATCH 1/8] 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 --- Cargo.lock | 30 +++++ kani-driver/Cargo.toml | 1 + kani-driver/src/args/mod.rs | 6 + kani-driver/src/call_cbmc.rs | 9 ++ kani-driver/src/cbmc_property_renderer.rs | 30 ++++- kani-driver/src/harness_runner.rs | 68 +++++++++- kani-driver/src/main.rs | 1 + kani-driver/src/progress_indicator.rs | 148 ++++++++++++++++++++++ tests/ui/log-file-output/expected | 2 + tests/ui/log-file-output/main.rs | 21 +++ 10 files changed, 309 insertions(+), 7 deletions(-) create mode 100644 kani-driver/src/progress_indicator.rs create mode 100644 tests/ui/log-file-output/expected create mode 100644 tests/ui/log-file-output/main.rs diff --git a/Cargo.lock b/Cargo.lock index 71b4a78545a0..afb51db12cb1 100644 --- a/Cargo.lock +++ b/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" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 75447228764d..ead5afbbac48 100644 --- a/kani-driver/Cargo.toml +++ b/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: diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index f7aef031f479..a00ae27f1b4a 100644 --- a/kani-driver/src/args/mod.rs +++ b/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, + /// Print final LLBC for Lean backend. This requires the `-Z lean` option. #[arg(long, hide = true)] pub print_llbc: bool, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 3eeede9f68e4..d56be4517a2f 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/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) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index a64562d51162..d5a23fc760c5 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/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 { // Some items (e.g., messages) are skipped. // We could also process them and decide to skip later. @@ -183,7 +189,21 @@ 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 @@ -191,6 +211,12 @@ pub fn kani_cbmc_output_filter( 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. diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 708a4064cd72..809ce686035e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/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>> { 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::>>() }); + + // 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 { 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")?; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 21b74e8672c7..3f602ab1f27a 100644 --- a/kani-driver/src/main.rs +++ b/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; diff --git a/kani-driver/src/progress_indicator.rs b/kani-driver/src/progress_indicator.rs new file mode 100644 index 000000000000..3addc865416c --- /dev/null +++ b/kani-driver/src/progress_indicator.rs @@ -0,0 +1,148 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Progress indicator for verification harness execution + +use indicatif::{MultiProgress, ProgressBar, ProgressStyle}; +use std::io::IsTerminal; +use std::sync::Arc; +use std::sync::atomic::{AtomicUsize, Ordering}; + +/// Tracks statistics for harness verification progress +#[derive(Debug, Clone)] +pub struct VerificationStats { + pub total: usize, + pub completed: Arc, + pub succeeded: Arc, + pub failed: Arc, + pub timed_out: Arc, +} + +impl VerificationStats { + pub fn new(total: usize) -> Self { + Self { + total, + completed: Arc::new(AtomicUsize::new(0)), + succeeded: Arc::new(AtomicUsize::new(0)), + failed: Arc::new(AtomicUsize::new(0)), + timed_out: Arc::new(AtomicUsize::new(0)), + } + } + + pub fn increment_completed(&self) { + self.completed.fetch_add(1, Ordering::SeqCst); + } + + pub fn increment_succeeded(&self) { + self.succeeded.fetch_add(1, Ordering::SeqCst); + } + + pub fn increment_failed(&self) { + self.failed.fetch_add(1, Ordering::SeqCst); + } + + pub fn increment_timed_out(&self) { + self.timed_out.fetch_add(1, Ordering::SeqCst); + } + + pub fn get_completed(&self) -> usize { + self.completed.load(Ordering::SeqCst) + } + + pub fn get_succeeded(&self) -> usize { + self.succeeded.load(Ordering::SeqCst) + } + + pub fn get_failed(&self) -> usize { + self.failed.load(Ordering::SeqCst) + } + + pub fn get_timed_out(&self) -> usize { + self.timed_out.load(Ordering::SeqCst) + } +} + +/// Progress indicator for verification harness execution +pub struct ProgressIndicator { + progress_bar: Option, + stats: VerificationStats, +} + +impl ProgressIndicator { + /// Create a new progress indicator if running in an interactive terminal and log file is enabled + pub fn new(total_harnesses: usize, show_progress: bool) -> Self { + let stats = VerificationStats::new(total_harnesses); + + if show_progress && std::io::stdout().is_terminal() { + let multi_progress = MultiProgress::new(); + let progress_bar = multi_progress.add(ProgressBar::new(total_harnesses as u64)); + + progress_bar.set_style( + ProgressStyle::with_template( + "{spinner:.green} [{elapsed_precise}] [{bar:40.cyan/blue}] {pos}/{len} ({eta})\n{msg}" + ) + .unwrap() + .progress_chars("#>-"), + ); + + progress_bar.set_message("Verifying harnesses..."); + + Self { progress_bar: Some(progress_bar), stats } + } else { + Self { progress_bar: None, stats } + } + } + + /// Update progress with the result of a harness verification + pub fn update_with_result(&self, succeeded: bool, timed_out: bool) { + self.stats.increment_completed(); + + if timed_out { + self.stats.increment_timed_out(); + } else if succeeded { + self.stats.increment_succeeded(); + } else { + self.stats.increment_failed(); + } + + if let Some(ref pb) = self.progress_bar { + pb.inc(1); + let completed = self.stats.get_completed(); + let succeeded = self.stats.get_succeeded(); + let failed = self.stats.get_failed(); + let timed_out = self.stats.get_timed_out(); + + pb.set_message(format!( + "Completed: {}/{} | Succeeded: {} | Failed: {} | Timed out: {}", + completed, self.stats.total, succeeded, failed, timed_out + )); + } + } + + /// Finish the progress indicator + pub fn finish(&self) { + if let Some(ref pb) = self.progress_bar { + let succeeded = self.stats.get_succeeded(); + let failed = self.stats.get_failed(); + let timed_out = self.stats.get_timed_out(); + + pb.finish_with_message(format!( + "Verification complete | Succeeded: {} | Failed: {} | Timed out: {}", + succeeded, failed, timed_out + )); + } + } + + /// Check if progress indicator is active + pub fn is_active(&self) -> bool { + self.progress_bar.is_some() + } + + /// Get the statistics + /// + /// This method provides access to the underlying verification statistics, + /// which may be useful for testing, monitoring, or external reporting purposes. + #[allow(dead_code)] + pub fn stats(&self) -> &VerificationStats { + &self.stats + } +} diff --git a/tests/ui/log-file-output/expected b/tests/ui/log-file-output/expected new file mode 100644 index 000000000000..11fb84163bc3 --- /dev/null +++ b/tests/ui/log-file-output/expected @@ -0,0 +1,2 @@ +Checking harness test_simple_verification... +Checking harness test_another_harness... diff --git a/tests/ui/log-file-output/main.rs b/tests/ui/log-file-output/main.rs new file mode 100644 index 000000000000..8c17f6a471f0 --- /dev/null +++ b/tests/ui/log-file-output/main.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --log-file verification.log +// +// This test checks that the --log-file option works correctly +// and writes verification output to the specified file + +#[kani::proof] +fn test_simple_verification() { + let x: u32 = kani::any(); + if x < 100 { + assert!(x < 100); + } +} + +#[kani::proof] +fn test_another_harness() { + let y: i32 = kani::any(); + assert!(y == y); +} From 1dfbba966b53cf6a38930eb3242b9e6dcd589b86 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 12:50:37 +0000 Subject: [PATCH 2/8] Clippy fix --- kani-driver/src/cbmc_property_renderer.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index d5a23fc760c5..2eed4171ad28 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -191,15 +191,14 @@ pub fn kani_cbmc_output_filter( if let Some(fmt_item) = formatted_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) { + if let Some(log_path) = log_file + && 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}"); From 1e7b13dff4a412972c24946918ead9fa74fc3f46 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 13:55:53 +0100 Subject: [PATCH 3/8] Update kani-driver/src/harness_runner.rs Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- kani-driver/src/harness_runner.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 809ce686035e..d966dbdb21b3 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -257,7 +257,7 @@ impl KaniSession { // 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 { + } else { println!("{msg}"); } } From 2931d7c357440a83cbd347a17e0f1266aabc9ebd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 14:00:12 +0100 Subject: [PATCH 4/8] Update kani-driver/src/progress_indicator.rs Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- kani-driver/src/progress_indicator.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/progress_indicator.rs b/kani-driver/src/progress_indicator.rs index 3addc865416c..cbeab2bc4861 100644 --- a/kani-driver/src/progress_indicator.rs +++ b/kani-driver/src/progress_indicator.rs @@ -72,7 +72,7 @@ impl ProgressIndicator { pub fn new(total_harnesses: usize, show_progress: bool) -> Self { let stats = VerificationStats::new(total_harnesses); - if show_progress && std::io::stdout().is_terminal() { + if show_progress { let multi_progress = MultiProgress::new(); let progress_bar = multi_progress.add(ProgressBar::new(total_harnesses as u64)); From 7ecb88febc387969c2c0398894f5d05a99a47e64 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 13:00:53 +0000 Subject: [PATCH 5/8] No need for multi_progress --- kani-driver/src/harness_runner.rs | 3 --- kani-driver/src/progress_indicator.rs | 6 ++---- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index d966dbdb21b3..c947cb71e22e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -229,9 +229,6 @@ impl KaniSession { ) -> Result { 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 { diff --git a/kani-driver/src/progress_indicator.rs b/kani-driver/src/progress_indicator.rs index cbeab2bc4861..3c0b4ba5e003 100644 --- a/kani-driver/src/progress_indicator.rs +++ b/kani-driver/src/progress_indicator.rs @@ -2,8 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Progress indicator for verification harness execution -use indicatif::{MultiProgress, ProgressBar, ProgressStyle}; -use std::io::IsTerminal; +use indicatif::{ProgressBar, ProgressStyle}; use std::sync::Arc; use std::sync::atomic::{AtomicUsize, Ordering}; @@ -73,8 +72,7 @@ impl ProgressIndicator { let stats = VerificationStats::new(total_harnesses); if show_progress { - let multi_progress = MultiProgress::new(); - let progress_bar = multi_progress.add(ProgressBar::new(total_harnesses as u64)); + let progress_bar = ProgressBar::new(total_harnesses as u64); progress_bar.set_style( ProgressStyle::with_template( From 6ac6f32cdeded90d5b93920b7d3a2cd978a9a3c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Jan 2026 13:08:50 +0000 Subject: [PATCH 6/8] fmt --- kani-driver/src/cbmc_property_renderer.rs | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 2eed4171ad28..88641b9ff18e 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -192,13 +192,14 @@ pub fn kani_cbmc_output_filter( if suppress_terminal { // Write to log file instead of terminal if let Some(log_path) = log_file - && let Err(e) = write_to_log_file(log_path, &fmt_item) { - eprintln!( - "Failed to write CBMC output to log file {}: {}", - log_path.display(), - e - ); - } + && 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}"); From 48e4aba653bad0e37ef409c2d0fd19ed4745909b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Feb 2026 10:22:16 +0000 Subject: [PATCH 7/8] Disentangle terminal/log-file logic --- kani-driver/src/call_cbmc.rs | 11 ++-------- kani-driver/src/cbmc_property_renderer.rs | 25 ++++++++--------------- kani-driver/src/harness_runner.rs | 1 - tests/ui/log-file-output/expected | 5 +++-- 4 files changed, 14 insertions(+), 28 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index d56be4517a2f..7c3891798dd6 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -9,7 +9,6 @@ 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}; @@ -121,10 +120,6 @@ 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(), @@ -134,8 +129,7 @@ impl KaniSession { self.args.extra_pointer_checks, self.args.common_args.quiet, &self.args.output_format, - suppress_terminal, - log_file_path.as_ref(), + self.args.log_file.as_ref(), ) }), ) @@ -147,8 +141,7 @@ impl KaniSession { self.args.extra_pointer_checks, self.args.common_args.quiet, &self.args.output_format, - suppress_terminal, - log_file_path.as_ref(), + self.args.log_file.as_ref(), ) }) .await) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 88641b9ff18e..1b028ad956ec 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -168,14 +168,13 @@ 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. When `suppress_terminal` is true -/// and a log file path is provided, output is redirected to the log file instead. +/// 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, - suppress_terminal: bool, log_file: Option<&PathBuf>, ) -> Option { // Some items (e.g., messages) are skipped. @@ -189,20 +188,14 @@ pub fn kani_cbmc_output_filter( if !quiet { let formatted_item = format_item(&processed_item, output_format); if let Some(fmt_item) = formatted_item { - if suppress_terminal { - // Write to log file instead of terminal - if let Some(log_path) = log_file - && 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 + if log_file.is_none() { println!("{fmt_item}"); + } else if let Err(e) = write_to_log_file(log_file.unwrap(), &fmt_item) { + eprintln!( + "Failed to write CBMC output to log file {}: {}", + log_file.unwrap().display(), + e + ); } } } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index c947cb71e22e..f097aa78a48e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -228,7 +228,6 @@ impl KaniSession { harness: &HarnessMetadata, ) -> Result { let thread_index = rayon::current_thread_index().unwrap_or_default(); - 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 { diff --git a/tests/ui/log-file-output/expected b/tests/ui/log-file-output/expected index 11fb84163bc3..6a72096f3292 100644 --- a/tests/ui/log-file-output/expected +++ b/tests/ui/log-file-output/expected @@ -1,2 +1,3 @@ -Checking harness test_simple_verification... -Checking harness test_another_harness... +Kani Rust Verifier \ +Manual Harness Summary:\ +Complete - 2 successfully verified harnesses, 0 failures, 2 total. From 3c8c8ce36e44187c58c8ed30e8913b769ebf404e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Feb 2026 11:30:44 +0000 Subject: [PATCH 8/8] Clippy --- kani-driver/src/cbmc_property_renderer.rs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 1b028ad956ec..cf8f3a693d12 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -188,14 +188,16 @@ pub fn kani_cbmc_output_filter( if !quiet { let formatted_item = format_item(&processed_item, output_format); if let Some(fmt_item) = formatted_item { - if log_file.is_none() { + 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}"); - } else if let Err(e) = write_to_log_file(log_file.unwrap(), &fmt_item) { - eprintln!( - "Failed to write CBMC output to log file {}: {}", - log_file.unwrap().display(), - e - ); } } }