Harness output individual files (#3360)

Resolves #3356 

1. Changes allow for directory with individual output of files named by
the full harness name. --output-into-files command line argument will
allow for placing all output of individual harnesses into files named by
the full harness pretty_name. The output directory is either
--target-dir or a hard coded default: "kani_output" directory. (These
can be changed if there is a better interface). Still prints output to
std::out exactly as previous.
2. Previously, all output was placed into std::out. This will allow for
some control over output. It will also enable easier parsing of harness
output.
3. Only solved #3356 but could be expanded to include more features.
4. Ran manually to check the flags and output behaved as expected.
Indeed:
--output-into-files enabled will place output into individual files,
disabled will not
--output-terse will create terse output to command line, regular output
to individual files if --output-into-files is enabled.
--target-dir will place output into target-dir directory when
--output-into-files is enabled, and will not place file output when
disabled.

Let me know if you need specific explanations of code segments, a clean
list of all the testing configurations, or any feature enhancement for
greater configuration options.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Alexander Aghili <[email protected]>
Co-authored-by: Jaisurya Nanduri <[email protected]>
Co-authored-by: Celina G. Val <[email protected]>

kani-driver/Cargo.toml

@@ -38,6 +38,7 @@ which = "6"
 time = {version = "0.3.36", features = ["formatting"]}
 tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
 
+
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml
 # Here are a few notes I'm keeping after looking through these

kani-driver/src/args/mod.rs

@@ -314,6 +314,10 @@ pub struct VerificationArgs {
     )]
     pub synthesize_loop_contracts: bool,
 
+    //Harness Output into individual files
+    #[arg(long, hide_short_help = true)]
+    pub output_into_files: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
@@ -673,6 +677,16 @@ impl ValidateArgs for VerificationArgs {
             ));
         }
 
+        if self.output_into_files
+            && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `--output-into-files` argument is unstable and requires `-Z unstable-options` to enable \
+            unstable options support.",
+            ));
+        }
+
         if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Lean) {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,

kani-driver/src/harness_runner.rs

@@ -4,13 +4,18 @@
 use anyhow::{Result, bail};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
+use std::fs::File;
+use std::io::Write;
 use std::path::Path;
 
 use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
 
+use std::env::current_dir;
+use std::path::PathBuf;
+
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
 ///
@@ -39,7 +44,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         self.check_stubbing(harnesses)?;
 
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
-
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
             if let Some(x) = self.sess.args.jobs() {
@@ -101,6 +105,45 @@ impl<'pr> HarnessRunner<'_, 'pr> {
 }
 
 impl KaniSession {
+    fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+        if self.should_print_output() {
+            if self.args.output_into_files {
+                self.write_output_to_file(result, harness);
+            }
+
+            let output = result.render(&self.args.output_format, harness.attributes.should_panic);
+            println!("{}", output);
+        }
+    }
+
+    fn should_print_output(&self) -> bool {
+        !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
+    }
+
+    fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+        let target_dir = self.result_output_dir().unwrap();
+        let file_name = target_dir.join(harness.pretty_name.clone());
+        let path = Path::new(&file_name);
+        let prefix = path.parent().unwrap();
+
+        std::fs::create_dir_all(prefix).unwrap();
+        let mut file = File::create(&file_name).unwrap();
+        let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+
+        if let Err(e) = writeln!(file, "{}", file_output) {
+            eprintln!(
+                "Failed to write to file {}: {}",
+                file_name.into_os_string().into_string().unwrap(),
+                e
+            );
+        }
+    }
+
+    fn result_output_dir(&self) -> Result<PathBuf> {
+        let target_dir = self.args.target_dir.clone().map_or_else(current_dir, Ok)?;
+        Ok(target_dir.join("result_output_dir")) //Hardcode output to result_output_dir, may want to make it adjustable?
+    }
+
     /// Run the verification process for a single harness
     pub(crate) fn check_harness(
         &self,
@@ -119,14 +162,7 @@ impl KaniSession {
         } else {
             let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-            // When quiet, we don't want to print anything at all.
-            // When output is old, we also don't have real results to print.
-            if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
-                println!(
-                    "{}",
-                    result.render(&self.args.output_format, harness.attributes.should_panic)
-                );
-            }
+            self.process_output(&result, harness);
             self.gen_and_add_concrete_playback(harness, &mut result)?;
             Ok(result)
         }

tests/script-based-pre/individual_file_output/config.yml

@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: individual_file_output.sh

tests/script-based-pre/individual_file_output/individual_file_output.sh

@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+OUT_DIR=tmp_sample_crate
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+
+# Move the original source to the output folder since it will be modified
+cp -r sample_crate ${OUT_DIR}
+pushd $OUT_DIR
+
+echo "Run verification..."
+cargo kani -Z unstable-options --output-into-files
+
+OUTPUT_DIR="result_output_dir" 
+
+# Check if the output directory exists
+if [ ! -d "$OUTPUT_DIR" ]; then
+    echo "Output directory $OUT_DIR/$OUTPUT_DIR does not exist. Verification failed."
+    exit 1
+fi
+
+# Check if there are any files in the output directory
+output_files=("$OUTPUT_DIR"/*)
+
+if [ ${#output_files[@]} -eq 0 ]; then
+    echo "No files found in the output directory. Verification failed."
+    exit 1
+fi
+
+# Check if each file contains text
+for file in "${output_files[@]}"; do
+    if [ ! -s "$file" ]; then
+        echo "File $file is empty. Verification failed."
+        exit 1
+    else
+        echo "File $file is present and contains text."
+    fi
+done
+
+popd
+rm -rf ${OUT_DIR}

tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"
+
+[package.metadata.kani.flags]
+concrete-playback = "inplace"
+
+[package.metadata.kani.unstable]
+concrete-playback = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that we can correctly generate tests from a cover statement and run them.
+
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    fn any_is_ok() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_ok());
+    }
+
+    #[kani::proof]
+    fn any_is_err() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_err());
+    }
+}