Create concrete playback temp files in source directory

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: model-checking#2705

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"

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"

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())

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<BufWriter<File>>,
-        renamed: bool,
-    }
-
-    impl TempFile {
-        /// Create a temp file
-        pub fn try_new(suffix_name: &str) -> Result<Self, Error> {
-            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)