From 4b504b218bbebf85cc56730091010ea1e79fd192 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 2 Mar 2023 00:02:21 -0800 Subject: [PATCH] Generate unit test line by line (for --inplace) (#2213) --- Cargo.lock | 37 +++++ kani-driver/Cargo.toml | 1 + kani-driver/src/concrete_playback.rs | 231 +++++++++++++++++---------- kani-driver/src/util.rs | 78 +++++++++ 4 files changed, 262 insertions(+), 85 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a62707e9bdab0..ae60ec6456473 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -534,6 +534,7 @@ dependencies = [ "kani_metadata", "once_cell", "pathdiff", + "rand", "rayon", "regex", "rustc-demangle", @@ -849,6 +850,12 @@ version = "0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e0a7ae3ac2f1173085d398531c705756c94a4c56843785df85a60c1a0afac116" +[[package]] +name = "ppv-lite86" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" + [[package]] name = "proc-macro-error" version = "1.0.4" @@ -902,6 +909,36 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "rand" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +dependencies = [ + "libc", + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom", +] + [[package]] name = "rayon" version = "1.6.1" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 5135d31e38313..f2c7602efc30f 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -37,6 +37,7 @@ strum_macros = {version = "0.24.0"} tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} tracing-tree = "0.2.2" +rand = "0.8" which = "4.4.0" # A good set of suggested dependencies can be found in rustup: diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index c146ebfc256a3..3331541e6a23c 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -7,14 +7,15 @@ use crate::args::ConcretePlaybackMode; use crate::call_cbmc::VerificationResult; use crate::session::KaniSession; +use crate::util::tempfile::TempFile; use anyhow::{Context, Result}; use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; use kani_metadata::HarnessMetadata; use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; -use std::fs::{self, File}; +use std::fs::File; use std::hash::{Hash, Hasher}; -use std::io::{Read, Write}; +use std::io::{BufRead, BufReader, Write}; use std::path::Path; use std::process::Command; @@ -39,32 +40,36 @@ impl KaniSession { ), Some(concrete_vals) => { let pretty_name = harness.get_harness_name_unqualified(); - let concrete_playback = format_unit_test(&pretty_name, &concrete_vals); + let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals); match playback_mode { ConcretePlaybackMode::Print => { println!( "Concrete playback unit test for `{}`:\n```\n{}\n```", - &harness.pretty_name, &concrete_playback.unit_test_str + &harness.pretty_name, + &generated_unit_test.code.join("\n") ); println!( "INFO: To automatically add the concrete playback unit test `{}` to the \ src code, run Kani with `--concrete-playback=inplace`.", - &concrete_playback.unit_test_name + &generated_unit_test.name ); } ConcretePlaybackMode::InPlace => { if !self.args.quiet { println!( "INFO: Now modifying the source code to include the concrete playback unit test `{}`.", - &concrete_playback.unit_test_name + &generated_unit_test.name ); } self.modify_src_code( &harness.original_file, harness.original_end_line, - &concrete_playback, + &generated_unit_test, ) - .expect("Failed to modify source code"); + .expect(&format!( + "Failed to modify source code for the file `{}`", + &harness.original_file + )); } } verification_result.generated_concrete_test = true; @@ -79,88 +84,73 @@ impl KaniSession { &self, src_path: &str, proof_harness_end_line: usize, - concrete_playback: &UnitTest, + unit_test: &UnitTest, ) -> Result<()> { - let mut src_file = File::open(src_path) - .with_context(|| format!("Couldn't open user's source code file `{src_path}`"))?; - let mut src_as_str = String::new(); - src_file.read_to_string(&mut src_as_str).with_context(|| { - format!("Couldn't read user's source code file `{src_path}` as a string") - })?; - - // Short circuit if unit test already in source code. - if src_as_str.contains(&concrete_playback.unit_test_name) { - if !self.args.quiet { - println!( - "Concrete playback unit test `{}/{}` already found in source code, so skipping modification.", - src_path, concrete_playback.unit_test_name, - ); - } + let unit_test_already_in_src = + self.add_test_inplace(src_path, proof_harness_end_line, unit_test)?; + + if unit_test_already_in_src { return Ok(()); } - // Split the code into two different parts around the insertion point. - let src_newline_matches: Vec<_> = src_as_str.match_indices('\n').collect(); - // If the proof harness ends on the last line of source code, there won't be a newline. - let insertion_pt = if proof_harness_end_line == src_newline_matches.len() + 1 { - src_as_str.len() - } else { - // Existing newline goes with 2nd src half. We also manually add newline before unit test. - src_newline_matches[proof_harness_end_line - 1].0 - }; - let src_before_concrete_playback = &src_as_str[..insertion_pt]; - let src_after_concrete_playback = &src_as_str[insertion_pt..]; - - // Write new source lines to a tmp file, and then rename it to the actual user's source file. - // Renames are usually automic, so we won't corrupt the user's source file during a crash. - let tmp_src_path = src_path.to_string() + ".concrete_playback_overwrite"; - let mut tmp_src_file = File::create(&tmp_src_path) - .with_context(|| format!("Couldn't create tmp source code file `{tmp_src_path}`"))?; - write!( - tmp_src_file, - "{}\n{}{}", - src_before_concrete_playback, - concrete_playback.unit_test_str, - src_after_concrete_playback - ) - .with_context(|| { - format!("Couldn't write new src str into tmp src file `{tmp_src_path}`") - })?; - fs::rename(&tmp_src_path, src_path).with_context(|| { - format!("Couldn't rename tmp src file `{tmp_src_path}` to actual src file `{src_path}`") - })?; - // Run rustfmt on just the inserted lines. - let source_path = Path::new(src_path); - let parent_dir_as_path = source_path.parent().with_context(|| { - format!("Expected source file `{}` to be in a directory", source_path.display()) - })?; - let parent_dir_as_str = parent_dir_as_path.to_str().with_context(|| { - format!( - "Couldn't convert source file parent directory `{}` from str", - parent_dir_as_path.display() - ) - })?; - let src_file_name_as_osstr = source_path.file_name().with_context(|| { - format!("Couldn't get the file name from the source file `{}`", source_path.display()) - })?; - let src_file_name_as_str = src_file_name_as_osstr.to_str().with_context(|| { - format!( - "Couldn't convert source code file name `{src_file_name_as_osstr:?}` from OsStr to str" - ) - })?; - - let concrete_playback_num_lines = concrete_playback.unit_test_str.matches('\n').count() + 1; + let concrete_playback_num_lines = unit_test.code.len(); let unit_test_start_line = proof_harness_end_line + 1; let unit_test_end_line = unit_test_start_line + concrete_playback_num_lines - 1; + let src_path = Path::new(src_path); + let (path, file_name) = extract_parent_dir_and_src_file(src_path)?; let file_line_ranges = vec![FileLineRange { - file: src_file_name_as_str.to_string(), + file: file_name, line_range: Some((unit_test_start_line, unit_test_end_line)), }]; - self.run_rustfmt(&file_line_ranges, Some(parent_dir_as_str))?; + self.run_rustfmt(&file_line_ranges, Some(&path))?; Ok(()) } + /// Writes the new source code to a user's source file using a tempfile as the means. + /// Returns whether the unit test was already in the old source code. + fn add_test_inplace( + &self, + source_path: &str, + proof_harness_end_line: usize, + unit_test: &UnitTest, + ) -> Result { + // Read from source + let source_file = File::open(source_path).unwrap(); + let source_reader = BufReader::new(source_file); + + // Create temp file + let mut temp_file = TempFile::try_new("concrete_playback.tmp")?; + let mut curr_line_num = 0; + + // Use a buffered reader/writer to generate the unit test line by line + for line in source_reader.lines().flatten() { + if line.contains(&unit_test.name) { + if !self.args.quiet { + println!( + "Concrete playback unit test `{}/{}` already found in source code, so skipping modification.", + source_path, unit_test.name, + ); + } + // the drop impl will take care of flushing and resetting + return Ok(true); + } + curr_line_num += 1; + if let Some(temp_writer) = temp_file.writer.as_mut() { + writeln!(temp_writer, "{line}")?; + if curr_line_num == proof_harness_end_line { + for unit_test_line in unit_test.code.iter() { + curr_line_num += 1; + writeln!(temp_writer, "{unit_test_line}")?; + } + } + } + } + + temp_file.rename(source_path).expect("Could not rename file"); + Ok(false) + } + /// Run rustfmt on the given src file, and optionally on only the specific lines. fn run_rustfmt( &self, @@ -235,8 +225,7 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe .chain(func_after_concrete_vals) .collect(); - let full_func_code: String = full_func.join("\n"); - UnitTest { unit_test_str: full_func_code, unit_test_name: func_name } + UnitTest { code: full_func, name: func_name } } /// Format an initializer expression for a number of concrete values. @@ -256,14 +245,23 @@ fn format_concrete_vals(concrete_vals: &[ConcreteVal]) -> impl Iterator Result<(String, String)> { + let parent_dir_as_path = src_path.parent().unwrap(); + let parent_dir = parent_dir_as_path.to_string_lossy().to_string(); + let src_file_name_as_osstr = src_path.file_name(); + let src_file = src_file_name_as_osstr.unwrap().to_string_lossy().to_string(); + Ok((parent_dir, src_file)) +} + struct FileLineRange { file: String, line_range: Option<(usize, usize)>, } struct UnitTest { - unit_test_str: String, - unit_test_name: String, + code: Vec, + name: String, } /// Extract concrete values from the CBMC output processed items. @@ -379,6 +377,32 @@ mod tests { CheckStatus, Property, PropertyId, SourceLocation, TraceData, TraceItem, TraceValue, }; + /// util function for unit tests taht generates the rustfmt args used for formatting specific lines inside specific files. + /// note - adding this within the test mod because it gives a lint warning without it. + fn rustfmt_args(file_line_ranges: &[FileLineRange]) -> Vec { + let mut args: Vec = Vec::new(); + let mut line_range_dicts: Vec = Vec::new(); + for file_line_range in file_line_ranges { + if let Some((start_line, end_line)) = file_line_range.line_range { + let src_file = &file_line_range.file; + let line_range_dict = + format!("{{\"file\":\"{src_file}\",\"range\":[{start_line},{end_line}]}}"); + line_range_dicts.push(line_range_dict); + } + } + if !line_range_dicts.is_empty() { + // `--file-lines` arg is currently unstable. + args.push("--unstable-features".into()); + args.push("--file-lines".into()); + let line_range_dicts_combined = format!("[{}]", line_range_dicts.join(",")); + args.push(line_range_dicts_combined.into()); + } + for file_line_range in file_line_ranges { + args.push((&file_line_range.file).into()); + } + args + } + #[test] fn format_zero_concrete_vals() { let concrete_vals: [ConcreteVal; 0] = []; @@ -426,8 +450,8 @@ mod tests { let harness_name = "test_proof_harness"; let concrete_vals = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }]; let unit_test = format_unit_test(harness_name, &concrete_vals); - let full_func: Vec<&str> = unit_test.unit_test_str.split('\n').collect(); - let split_unit_test_name = split_unit_test_name(&unit_test.unit_test_name); + let full_func = unit_test.code; + let split_unit_test_name = split_unit_test_name(&unit_test.name); let expected_after_func_name = vec![ format!("{:<4}let concrete_vals: Vec> = vec![", " "), format!("{:<8}// 0", " "), @@ -442,14 +466,14 @@ mod tests { split_unit_test_name.before_hash, format!("kani_concrete_playback_{harness_name}") ); - assert_eq!(full_func[1], format!("fn {}() {{", unit_test.unit_test_name)); + assert_eq!(full_func[1], format!("fn {}() {{", unit_test.name)); assert_eq!(full_func[2..], expected_after_func_name); } /// Generates a unit test and returns its hash. fn extract_hash_from_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> String { let unit_test = format_unit_test(harness_name, concrete_vals); - split_unit_test_name(&unit_test.unit_test_name).hash + split_unit_test_name(&unit_test.name).hash } /// Two hashes should not be the same if either the harness_name or the concrete_vals changes. @@ -471,6 +495,43 @@ mod tests { assert_ne!(hash_base, hash_diff_interp_val); } + #[test] + fn check_rustfmt_args_no_line_ranges() { + let file_line_ranges = [FileLineRange { file: "file1".to_string(), line_range: None }]; + let args = rustfmt_args(&file_line_ranges); + let expected: Vec = vec!["file1".into()]; + assert_eq!(args, expected); + } + + #[test] + fn check_rustfmt_args_some_line_ranges() { + let file_line_ranges = [ + FileLineRange { file: "file1".to_string(), line_range: None }, + FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) }, + ]; + let args = rustfmt_args(&file_line_ranges); + let expected: Vec = [ + "--unstable-features", + "--file-lines", + "[{\"file\":\"path/to/file2\",\"range\":[1,3]}]", + "file1", + "path/to/file2", + ] + .into_iter() + .map(|arg| arg.into()) + .collect(); + assert_eq!(args, expected); + } + + #[test] + fn check_extract_parent_dir_and_src_file() { + let src_path = "/path/to/file.txt"; + let src_path = Path::new(src_path); + let (path, file_name) = extract_parent_dir_and_src_file(src_path).unwrap(); + assert_eq!(path, "/path/to"); + assert_eq!(file_name, "file.txt"); + } + /// Test util functions which extract the counter example values from a property. #[test] fn check_concrete_vals_extractor() { diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index 301b90338b308..2a4f7f1d926ee 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -14,6 +14,84 @@ use std::ffi::OsString; use std::path::{Path, PathBuf}; use std::process::Command; +pub mod tempfile { + use std::{ + env, + fs::{self, rename, File}, + io::{BufWriter, Error, Write}, + path::PathBuf, + }; + + use crate::util; + use ::rand; + use anyhow::Context; + use rand::Rng; + + /// Handle a writable temporary file which will be deleted when the object is dropped. + /// To save the contents of the file, users can invoke `rename` which will move the file to + /// its new location and no further deletion will be performed. + pub struct TempFile { + pub file: File, + pub temp_path: PathBuf, + pub writer: Option>, + renamed: bool, + } + + impl TempFile { + /// Create a temp file + pub fn try_new(suffix_name: &str) -> Result { + let mut temp_path = env::temp_dir(); + + // Generate a unique name for the temporary directory + let hash: u32 = rand::thread_rng().gen(); + let file_name: &str = &format!("kani_tmp_{hash}_{suffix_name}"); + + temp_path.push(file_name); + let temp_file = File::create(&temp_path)?; + let writer = BufWriter::new(temp_file.try_clone()?); + + Ok(Self { file: temp_file, temp_path, writer: Some(writer), renamed: false }) + } + + /// Rename the temporary file to the new path, replacing the original file if the path points to a file that already exists. + pub fn rename(mut self, source_path: &str) -> Result<(), String> { + // flush here + self.writer.as_mut().unwrap().flush().unwrap(); + self.writer = None; + // Renames are usually automic, so we won't corrupt the user's source file during a crash. + rename(&self.temp_path, source_path) + .with_context(|| format!("Error renaming file {}", self.temp_path.display())) + .unwrap(); + self.renamed = true; + Ok(()) + } + } + + /// Ensure that the bufwriter is flushed and temp variables are dropped + /// everytime the tempfile is out of scope + /// note: the fields for the struct are dropped automatically by destructor + impl Drop for TempFile { + fn drop(&mut self) { + // if writer is not flushed, flush it + if self.writer.as_ref().is_some() { + // couldn't use ? as drop does not handle returns + if let Err(e) = self.writer.as_mut().unwrap().flush() { + util::warning( + format!("failed to flush {}: {e}", self.temp_path.display()).as_str(), + ); + } + self.writer = None; + } + + if !self.renamed { + if let Err(_e) = fs::remove_file(&self.temp_path.clone()) { + util::warning(&format!("Error removing file {}", self.temp_path.display())); + } + } + } + } +} + /// Replace an extension with another one, in a new PathBuf. (See tests for examples) pub fn alter_extension(path: &Path, ext: &str) -> PathBuf { path.with_extension(ext)