Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generate unit test line by line (for --inplace) #2213

Merged
merged 22 commits into from
Mar 2, 2023
Merged
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
323a025
Generate unit test, line by line
jaisnan Feb 16, 2023
23b92d0
Remove tempfile crate because it crashes cargo audit
jaisnan Feb 17, 2023
a71f204
Add formatting
jaisnan Feb 17, 2023
362fb14
Remove temp files when there is a unit test present already
jaisnan Feb 20, 2023
6790b0c
Merge branch 'main' into Generate-test-by-line
jaisnan Feb 20, 2023
0c3bbe9
Add tempfile struct
jaisnan Feb 22, 2023
ff6d7fd
Add error handling
jaisnan Feb 22, 2023
0616fa8
add source file path to expect
jaisnan Feb 23, 2023
7e855af
Merge branch 'Generate-test-by-line' of https://github.com/jaisnan/ka…
jaisnan Feb 23, 2023
332c57e
Merge branch 'main' into Generate-test-by-line
jaisnan Feb 23, 2023
ad56cb1
fix formatting CI error
jaisnan Feb 23, 2023
ab65607
Merge branch 'Generate-test-by-line' of https://github.com/jaisnan/ka…
jaisnan Feb 23, 2023
d7cbfc9
Merge branch 'main' into Generate-test-by-line
jaisnan Feb 23, 2023
ba2b156
Merge branch 'main' of https://github.com/model-checking/kani into Ge…
jaisnan Feb 27, 2023
fa36a2a
add rename and drop impl to a tempfile struct
jaisnan Feb 28, 2023
c92133e
remove explicit drop calls
jaisnan Feb 28, 2023
8c1354a
Merge branch 'Generate-test-by-line' of https://github.com/jaisnan/ka…
jaisnan Feb 28, 2023
cf0a1f5
Add warnings and reformat try_new()
jaisnan Feb 28, 2023
b7fbf5e
Merge branch 'main' into Generate-test-by-line
jaisnan Feb 28, 2023
631a48e
Merge branch 'main' into Generate-test-by-line
jaisnan Mar 1, 2023
f3eae97
Merge branch 'main' of https://github.com/model-checking/kani into Ge…
jaisnan Mar 2, 2023
ffcc83e
Merge branch 'Generate-test-by-line' of https://github.com/jaisnan/ka…
jaisnan Mar 2, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Add tempfile struct
  • Loading branch information
jaisnan committed Feb 22, 2023
commit 0c3bbe9a471f71ffb2e9488ccb910aae0c293a72
51 changes: 39 additions & 12 deletions kani-driver/src/concrete_playback.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,41 @@ use std::env;
use std::ffi::OsString;
use std::fs::{self, remove_file, File};
use std::hash::{Hash, Hasher};
use std::io::{BufRead, BufReader, BufWriter, Write};
use std::path::Path;
use std::io::{BufRead, BufReader, BufWriter, Error, Write};
use std::path::{Path, PathBuf};
use std::process::Command;

struct TempFile {
file: File,
temp_path: PathBuf,
}

impl TempFile {
fn new() -> Result<Self, Error> {
// Create temp file
let mut temp_path = env::temp_dir();
temp_path.push("concrete_overwrite.tmp");
let temp_file = match File::create(&temp_path) {
Ok(f) => f,
Err(e) => return Err(e),
};
Ok(Self { file: temp_file, temp_path })
}
}

impl Drop for TempFile {
fn drop(&mut self) -> () {
if let Err(e) = self.file.sync_all() {
eprintln!("Error syncing tempfile: {}", e);
}

drop(&self.file);
if let Err(e) = remove_file(&self.temp_path) {
eprintln!("Error removing the tempfile: {}", e);
}
}
}

impl KaniSession {
/// The main driver for generating concrete playback unit tests and adding them to source code.
pub fn gen_and_add_concrete_playback(
Expand Down Expand Up @@ -116,10 +147,11 @@ impl KaniSession {
let source_reader = BufReader::new(source_file);

// Create temp file
let mut temp_path = env::temp_dir();
temp_path.push("concrete_overwrite.tmp");
let mut temp_file = File::create(&temp_path)?;
let mut temp_writer = BufWriter::new(&mut temp_file);
let mut temp_file = match TempFile::new() {
Ok(f) => f,
Err(_) => return Ok(false),
};
let mut temp_writer = BufWriter::new(&mut temp_file.file);
let mut curr_line_num = 0;

// Use a buffered reader/writer to generate the unit test line by line
Expand All @@ -133,7 +165,6 @@ impl KaniSession {
}
drop(temp_writer);
drop(temp_file);
remove_file(temp_path)?;
return Ok(true);
}
curr_line_num += 1;
Expand All @@ -146,19 +177,15 @@ impl KaniSession {
}
}

// Flush before we remove/rename the file.
temp_writer.flush()?;

// Have to drop the bufreader to be able to reuse and rename the moved temp file
drop(temp_writer);

// Renames are usually automic, so we won't corrupt the user's source file during a crash.
fs::rename(&temp_path, source_path).with_context(|| {
fs::rename(&temp_file.temp_path, source_path).with_context(|| {
format!("Couldn't rename tmp source file to actual src file `{source_path}`.")
})?;

drop(temp_file);
remove_file(temp_path)?;

Ok(false)
}
Expand Down