Harness output individual files

kani-driver/Cargo.toml

@@ -36,6 +36,7 @@ rand = "0.8"
 which = "6"
 time = {version = "0.3.36", features = ["formatting"]}
 
+
 # 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

@@ -260,6 +260,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
@@ -609,6 +613,20 @@ impl ValidateArgs for VerificationArgs {
             ));
         }
 
+        if self.output_into_files
+            && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
+        {
+            if self.common_args.enable_unstable {
+                print_deprecated(&self.common_args, "`--enable-unstable`", "-Z unstable-options");
+            } else {
+                return Err(Error::raw(
+                    ErrorKind::MissingRequiredArgument,
+                    "The `--output-into-files` argument is unstable and requires `-Z unstable-options` to enable \
+                unstable options support.",
+                ));
+            }
+        }
+
         Ok(())
     }
 }

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<'sess, 'pr> HarnessRunner<'sess, '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<'sess, 'pr> HarnessRunner<'sess, '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());
+    }
+}