Skip to content

Commit

Permalink
Create concrete playback temp files in source directory (model-checki…
Browse files Browse the repository at this point in the history 
…ng#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: model-checking#2705
  • Loading branch information
@tautschnig
tautschnig authored Oct 4, 2023
1 parent 62f136c commit fb08f3e
Show file tree
Hide file tree
Showing 4 changed files with 35 additions and 89 deletions.
20 changes: 20 additions & 0 deletions Cargo.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -504,6 +510,7 @@ dependencies = [
"serde_json",
"strum 0.25.0",
"strum_macros 0.25.2",
"tempfile",
"toml",
"tracing",
"tracing-subscriber",
Expand Down Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions kani-driver/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
25 changes: 14 additions & 11 deletions kani-driver/src/concrete_playback/test_generator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.
Expand Down Expand Up @@ -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())
Expand Down
78 changes: 0 additions & 78 deletions kani-driver/src/util.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit fb08f3e

Please sign in to comment.