From edec4dc0cf0ae1490374603001e35f77ba9de9de Mon Sep 17 00:00:00 2001 From: Alexander Aghili <43054019+Alexander-Aghili@users.noreply.github.com> Date: Mon, 4 Nov 2024 19:03:26 -0800 Subject: [PATCH] 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 Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Co-authored-by: Celina G. Val --- kani-driver/Cargo.toml | 1 + kani-driver/src/args/mod.rs | 14 +++++ kani-driver/src/harness_runner.rs | 54 +++++++++++++++---- .../individual_file_output/config.yml | 3 ++ .../individual_file_output.sh | 46 ++++++++++++++++ .../sample_crate/Cargo.toml | 15 ++++++ .../sample_crate/src/lib.rs | 19 +++++++ 7 files changed, 143 insertions(+), 9 deletions(-) create mode 100644 tests/script-based-pre/individual_file_output/config.yml create mode 100755 tests/script-based-pre/individual_file_output/individual_file_output.sh create mode 100644 tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml create mode 100644 tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index d1460a9c943d..844b844b8ef4 100644 --- a/kani-driver/Cargo.toml +++ b/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 diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 6901828b4dd7..0eb2f0d6c999 100644 --- a/kani-driver/src/args/mod.rs +++ b/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, diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 32f184b3ce6a..f34e150efbad 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -4,6 +4,8 @@ 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; @@ -11,6 +13,9 @@ 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 { + 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) } diff --git a/tests/script-based-pre/individual_file_output/config.yml b/tests/script-based-pre/individual_file_output/config.yml new file mode 100644 index 000000000000..932ebf466727 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/individual_file_output/individual_file_output.sh b/tests/script-based-pre/individual_file_output/individual_file_output.sh new file mode 100755 index 000000000000..49d110983527 --- /dev/null +++ b/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} diff --git a/tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml b/tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml new file mode 100644 index 000000000000..39cfab289878 --- /dev/null +++ b/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)'] } diff --git a/tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs b/tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs new file mode 100644 index 000000000000..3cf83c8e3597 --- /dev/null +++ b/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 = kani::any(); + kani::cover!(result.is_ok()); + } + + #[kani::proof] + fn any_is_err() { + let result: Result = kani::any(); + kani::cover!(result.is_err()); + } +}