diff --git a/Cargo.lock b/Cargo.lock index d361244a5005..59770bbda6d2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -374,6 +374,12 @@ dependencies = [ "libc", ] +[[package]] +name = "fastrand" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25cbce373ec4653f1a01a31e8a5e5ec0c622dc27ff9c4e6606eefef5cbbed4a5" + [[package]] name = "getopts" version = "0.2.21" @@ -504,6 +510,7 @@ dependencies = [ "serde_json", "strum 0.25.0", "strum_macros 0.25.2", + "tempfile", "toml", "tracing", "tracing-subscriber", @@ -1190,6 +1197,19 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb94d2f3cc536af71caac6b6fcebf65860b347e7ce0cc9ebe8f70d3e521054ef" +dependencies = [ + "cfg-if", + "fastrand", + "redox_syscall", + "rustix", + "windows-sys 0.48.0", +] + [[package]] name = "thiserror" version = "1.0.49" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index c541803bb10d..2f01fa9e83dd 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -29,6 +29,7 @@ rayon = "1.5.3" comfy-table = "7.0.1" strum = {version = "0.25.0"} strum_macros = {version = "0.25.2"} +tempfile = "3" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} rand = "0.8" diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 049b294c9848..ccaf5e684691 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -7,7 +7,6 @@ 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; @@ -18,6 +17,7 @@ use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, Write}; use std::path::Path; use std::process::Command; +use tempfile::NamedTempFile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -158,25 +158,26 @@ impl KaniSession { // Create temp file if !unit_tests.is_empty() { - let mut temp_file = TempFile::try_new("concrete_playback.tmp")?; + let source_basedir = Path::new(source_path).parent().unwrap_or(Path::new(".")); + let mut temp_file = NamedTempFile::with_prefix_in("concrete_playback", source_basedir)?; 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() { 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 in unit_tests.iter() { - for unit_test_line in unit_test.code.iter() { - curr_line_num += 1; - writeln!(temp_writer, "{unit_test_line}")?; - } + writeln!(temp_file, "{line}")?; + if curr_line_num == proof_harness_end_line { + for unit_test in unit_tests.iter() { + for unit_test_line in unit_test.code.iter() { + curr_line_num += 1; + writeln!(temp_file, "{unit_test_line}")?; } } } } - temp_file.rename(source_path).expect("Could not rename file"); + + // Renames are usually automic, so we won't corrupt the user's source file during a crash. + temp_file.persist(source_path).expect("Could not rename file"); } Ok(!unit_tests.is_empty()) diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index a9800785f869..1e0957dc7726 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -14,84 +14,6 @@ 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)