From fb08f3e11384a36585de3db13c8bcd9b6c0060d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Oct 2023 22:17:09 +0200 Subject: [PATCH] Create concrete playback temp files in source directory (#2804) Concrete playback seeks to generate unit tests in the original source file. An intermediate temporary file is used to reduce the risk of corrupting original source files. Once the temporary file has been completely written to, it is to be atomically moved to replace the source file. This can only be done on the same file system. We now create the temporary file in the same source directory as the original source file to ensure we are on the same file system. The implementation uses NamedTempFile from the tempfile crate, which renders our own tempfile implementation redundant. Tested on Ubuntu 20.04 with /tmp on a different partition (where our regression tests would previously fail). Resolves: #2705 --- Cargo.lock | 20 +++++ kani-driver/Cargo.toml | 1 + .../src/concrete_playback/test_generator.rs | 25 +++--- kani-driver/src/util.rs | 78 ------------------- 4 files changed, 35 insertions(+), 89 deletions(-) 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..492369fb32eb 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,28 @@ 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; but first flush all updates to disk, which persist wouldn't take care of. + temp_file.as_file().sync_all()?; + 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)