Merge branch 'main' into future-clippy-warnings

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

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)