From 72522bcfe1b65d105e40efae9278a720bd6a8968 Mon Sep 17 00:00:00 2001 From: Alexander Date: Fri, 19 Jul 2024 03:56:01 +0000 Subject: [PATCH 1/8] Added individual output to files + args, still issues with directory input and target directory --- kani-driver/src/args/mod.rs | 4 +++ kani-driver/src/harness_runner.rs | 53 +++++++++++++++++++++++++++---- 2 files changed, 51 insertions(+), 6 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index d043035bcab2..7c50e8698441 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -275,6 +275,10 @@ pub struct VerificationArgs { )] pub synthesize_loop_contracts: bool, + //Harness Output into individual files + #[arg(long, hide_short_help = true, requires("enable_unstable"))] + 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 diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 992e226e45db..9990843936fe 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -11,6 +11,9 @@ use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; use crate::session::KaniSession; +use std::fs::File; +use std::io::Write; + /// 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. /// @@ -122,14 +125,52 @@ impl KaniSession { // 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( + let file_output: String = Default::default(); + if self.args.output_into_files { + + //target_dir might fail if not UTF-8 Encoded path + let targ_dir = self.args.target_dir.clone(); + let dir_str; + //This is to ensure that null won't brake, might be a better way to do this + if targ_dir != None { + dir_str = String::from(targ_dir.unwrap().into_os_string().into_string().unwrap().to_owned() + "/"); + } else { + dir_str = String::from("./test/"); + } + let file_name = String::from(dir_str.to_owned() + &harness.pretty_name.clone()); + let path = Path::new(&file_name); + let prefix = path.parent().unwrap(); + std::fs::create_dir_all(prefix).unwrap(); + + let file = File::create(&harness.pretty_name.clone()); + + let file_output = result.render( + &OutputFormat::Regular, + harness.attributes.should_panic, + self.args.coverage, + ); + + + + if let Err(e) = writeln!(file.unwrap(), "{}", file_output) { + eprintln!("Failed to write to file {}: {}", file_name, e); + } + + + } + let output; + //Only render clone if Terse format + if !self.args.output_into_files || self.args.output_format == OutputFormat::Terse { + output = result.render( &self.args.output_format, harness.attributes.should_panic, - self.args.coverage - ) - ); + self.args.coverage, + ); + } else { + output = file_output.clone(); + } + + println!("{}", output); } self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) From 5b85c39f4deba0b270a4b779cef8ca333658befd Mon Sep 17 00:00:00 2001 From: Alexander Date: Fri, 19 Jul 2024 04:24:29 +0000 Subject: [PATCH 2/8] Harness refactor + directory fix --- kani-driver/src/harness_runner.rs | 104 ++++++++++++++++-------------- 1 file changed, 54 insertions(+), 50 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 9990843936fe..de72c5798b66 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -104,6 +104,59 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { } impl KaniSession { + + fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) { + if self.should_print_output() { + let output = if self.args.output_into_files { + self.write_output_to_file(result, harness) + } else { + self.render_output(result, harness) + }; + + println!("{}", output); + } + } + + fn should_print_output(&self) -> bool { + return !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old; + } + + fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) -> String { + let target_dir = self.get_target_dir(); + let file_name = format!("{}/{}", target_dir, harness.pretty_name); + 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 = self.render_output(result, harness); + if let Err(e) = writeln!(file, "{}", file_output) { + eprintln!("Failed to write to file {}: {}", file_name, e); + } + + return file_output; + } + + fn get_target_dir(&self) -> String { + return self.args.target_dir + .clone() + .map_or_else(|| "./kani_output".to_string(), |dir| { + format!("{}/", dir.into_os_string().into_string().unwrap()) + }); + } + + fn render_output(&self, result: &VerificationResult, harness: &HarnessMetadata) -> String { + let format = if !self.args.output_into_files || self.args.output_format == OutputFormat::Terse { + &self.args.output_format + } else { + &OutputFormat::Regular + }; + + return result.render(format, harness.attributes.should_panic, self.args.coverage) + } + + /// Run the verification process for a single harness pub(crate) fn check_harness( &self, @@ -122,56 +175,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 { - let file_output: String = Default::default(); - if self.args.output_into_files { - - //target_dir might fail if not UTF-8 Encoded path - let targ_dir = self.args.target_dir.clone(); - let dir_str; - //This is to ensure that null won't brake, might be a better way to do this - if targ_dir != None { - dir_str = String::from(targ_dir.unwrap().into_os_string().into_string().unwrap().to_owned() + "/"); - } else { - dir_str = String::from("./test/"); - } - let file_name = String::from(dir_str.to_owned() + &harness.pretty_name.clone()); - let path = Path::new(&file_name); - let prefix = path.parent().unwrap(); - std::fs::create_dir_all(prefix).unwrap(); - - let file = File::create(&harness.pretty_name.clone()); - - let file_output = result.render( - &OutputFormat::Regular, - harness.attributes.should_panic, - self.args.coverage, - ); - - - - if let Err(e) = writeln!(file.unwrap(), "{}", file_output) { - eprintln!("Failed to write to file {}: {}", file_name, e); - } - - - } - let output; - //Only render clone if Terse format - if !self.args.output_into_files || self.args.output_format == OutputFormat::Terse { - output = result.render( - &self.args.output_format, - harness.attributes.should_panic, - self.args.coverage, - ); - } else { - output = file_output.clone(); - } - - println!("{}", output); - } + self.process_output(&result, harness); self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) } From 0a40e1bedc6956f4f1e12a5d717086745159fd3c Mon Sep 17 00:00:00 2001 From: Alexander Date: Fri, 19 Jul 2024 05:02:39 +0000 Subject: [PATCH 3/8] Quick format fix and refactor to fix the output correctness --- kani-driver/src/harness_runner.rs | 31 +++++++++---------------------- 1 file changed, 9 insertions(+), 22 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index de72c5798b66..56066638128e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -107,21 +107,20 @@ impl KaniSession { fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) { if self.should_print_output() { - let output = if self.args.output_into_files { - self.write_output_to_file(result, harness) - } else { - self.render_output(result, harness) - }; + 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, self.args.coverage); println!("{}", output); } } fn should_print_output(&self) -> bool { - return !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old; + !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old } - fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) -> String { + fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) { let target_dir = self.get_target_dir(); let file_name = format!("{}/{}", target_dir, harness.pretty_name); let path = Path::new(&file_name); @@ -129,31 +128,19 @@ impl KaniSession { 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, self.args.coverage); - let file_output = self.render_output(result, harness); if let Err(e) = writeln!(file, "{}", file_output) { eprintln!("Failed to write to file {}: {}", file_name, e); } - - return file_output; } fn get_target_dir(&self) -> String { - return self.args.target_dir + self.args.target_dir .clone() .map_or_else(|| "./kani_output".to_string(), |dir| { format!("{}/", dir.into_os_string().into_string().unwrap()) - }); - } - - fn render_output(&self, result: &VerificationResult, harness: &HarnessMetadata) -> String { - let format = if !self.args.output_into_files || self.args.output_format == OutputFormat::Terse { - &self.args.output_format - } else { - &OutputFormat::Regular - }; - - return result.render(format, harness.attributes.should_panic, self.args.coverage) + }) } From 6a951b477ef5518911f262488aa370fffab74c89 Mon Sep 17 00:00:00 2001 From: Alexander Aghili Date: Mon, 22 Jul 2024 22:16:09 -0700 Subject: [PATCH 4/8] Refactor of harness runner update for Harness Output Individual Files --- kani-driver/src/harness_runner.rs | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 56066638128e..906b7d6bc12e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -14,6 +14,9 @@ use crate::session::KaniSession; use std::fs::File; use std::io::Write; +use std::path::PathBuf; +use std::env::current_dir; + /// 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. /// @@ -121,8 +124,8 @@ impl KaniSession { } fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) { - let target_dir = self.get_target_dir(); - let file_name = format!("{}/{}", target_dir, harness.pretty_name); + 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(); @@ -131,16 +134,15 @@ impl KaniSession { let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic, self.args.coverage); if let Err(e) = writeln!(file, "{}", file_output) { - eprintln!("Failed to write to file {}: {}", file_name, e); + eprintln!("Failed to write to file {}: {}", file_name.into_os_string().into_string().unwrap(), e); } } - fn get_target_dir(&self) -> String { - self.args.target_dir + fn result_output_dir(&self) -> Result { + let target_dir = self.args.target_dir .clone() - .map_or_else(|| "./kani_output".to_string(), |dir| { - format!("{}/", dir.into_os_string().into_string().unwrap()) - }) + .map_or_else(|| current_dir(), |dir| Ok(dir))?; + Ok(target_dir.join("kani_results")) } From 01bd260124db147a31a4990af68465eb857c4c10 Mon Sep 17 00:00:00 2001 From: Alexander Aghili Date: Wed, 31 Jul 2024 07:16:22 -0700 Subject: [PATCH 5/8] Untested configuration options change (commit to get to server to test) --- kani-driver/src/args/mod.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 7c50e8698441..382542b4fc2b 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -643,6 +643,21 @@ 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(()) } } From 2524fa1b7343e3bd26d94afc7482574b4ad0d667 Mon Sep 17 00:00:00 2001 From: Alexander Date: Wed, 31 Jul 2024 20:28:35 +0000 Subject: [PATCH 6/8] Remove enable-unstable requirement --- kani-driver/src/args/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 382542b4fc2b..310105f75940 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -276,7 +276,7 @@ pub struct VerificationArgs { pub synthesize_loop_contracts: bool, //Harness Output into individual files - #[arg(long, hide_short_help = true, requires("enable_unstable"))] + #[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 From 1e125f4764ef67ddd9c3760a7d9273366da61b7f Mon Sep 17 00:00:00 2001 From: Alexander Date: Sun, 4 Aug 2024 17:53:40 +0000 Subject: [PATCH 7/8] Comments + formatting --- kani-driver/src/args/mod.rs | 9 ++++----- kani-driver/src/harness_runner.rs | 31 ++++++++++++++++++++----------- 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 310105f75940..82d4bedf7547 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -643,10 +643,9 @@ impl ValidateArgs for VerificationArgs { )); } - if self.output_into_files - && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions) - { - + 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 { @@ -656,7 +655,7 @@ impl ValidateArgs for VerificationArgs { unstable options support.", )); } - } + } Ok(()) } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 906b7d6bc12e..47f5b01ad48e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -14,8 +14,8 @@ use crate::session::KaniSession; use std::fs::File; use std::io::Write; -use std::path::PathBuf; 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. @@ -107,14 +107,17 @@ 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, self.args.coverage); + let output = result.render( + &self.args.output_format, + harness.attributes.should_panic, + self.args.coverage, + ); println!("{}", output); } } @@ -131,21 +134,27 @@ impl KaniSession { 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, self.args.coverage); + let file_output = result.render( + &OutputFormat::Regular, + harness.attributes.should_panic, + self.args.coverage, + ); if let Err(e) = writeln!(file, "{}", file_output) { - eprintln!("Failed to write to file {}: {}", file_name.into_os_string().into_string().unwrap(), e); + 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(), |dir| Ok(dir))?; + let target_dir = + self.args.target_dir.clone().map_or_else(current_dir, Ok)?; Ok(target_dir.join("kani_results")) } - /// Run the verification process for a single harness pub(crate) fn check_harness( &self, @@ -164,7 +173,7 @@ impl KaniSession { } else { let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; - self.process_output(&result, harness); + self.process_output(&result, harness); self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) } From cca964871542b5ca1509949eee9b84e99d5eb383 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 14 Aug 2024 14:22:57 -0700 Subject: [PATCH 8/8] Update kani-driver/src/harness_runner.rs --- kani-driver/src/harness_runner.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 47f5b01ad48e..484d22228fe4 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -150,8 +150,7 @@ impl KaniSession { } fn result_output_dir(&self) -> Result { - let target_dir = - self.args.target_dir.clone().map_or_else(current_dir, Ok)?; + let target_dir = self.args.target_dir.clone().map_or_else(current_dir, Ok)?; Ok(target_dir.join("kani_results")) }