From 50ce2753382ae1e8ddc6409576584b04be267372 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:14:47 +0000 Subject: [PATCH 1/4] Generate unit test, line by line --- kani-driver/Cargo.toml | 1 + kani-driver/src/concrete_playback.rs | 51 ++++++++++++++++------------ 2 files changed, 30 insertions(+), 22 deletions(-) diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index caa14c81328..291035121fe 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -39,6 +39,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt" tracing-tree = "0.2.2" rand = "0.8" which = "4.4.0" +tempfile = "3.3.0" # A good set of suggested dependencies can be found in rustup: # https://github.com/rust-lang/rustup/blob/master/Cargo.toml diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index 66971603c7b..173c9324276 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -15,9 +15,10 @@ use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; use std::fs::File; use std::hash::{Hash, Hasher}; -use std::io::{BufRead, BufReader, Write}; +use std::io::{BufRead, BufReader, BufWriter, Write}; use std::path::Path; use std::process::Command; +use tempfile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -107,20 +108,17 @@ impl KaniSession { Ok(()) } - /// Writes the new source code to a user's source file using a tempfile as the means. - /// Returns whether the unit test was already in the old source code. + /// Writes the new source code to a temporary file. Returns whether the unit test was already in the old source code. fn add_test_inplace( &self, source_path: &str, proof_harness_end_line: usize, unit_test: &UnitTest, ) -> Result { - // Read from source - let source_file = File::open(source_path).unwrap(); + let source_file = File::open(source_path)?; let source_reader = BufReader::new(source_file); - - // Create temp file - let mut temp_file = TempFile::try_new("concrete_playback.tmp")?; + let mut temp_file = tempfile::NamedTempFile::new()?; + let mut temp_writer = BufWriter::new(&mut temp_file); let mut curr_line_num = 0; // Use a buffered reader/writer to generate the unit test line by line @@ -132,22 +130,31 @@ impl KaniSession { source_path, unit_test.name, ); } - // the drop impl will take care of flushing and resetting + // temp file gets deleted automatically when function goes out of scope return Ok(true); } 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_line in unit_test.code.iter() { - curr_line_num += 1; - writeln!(temp_writer, "{unit_test_line}")?; - } + writeln!(temp_writer, "{}", line)?; + if curr_line_num == proof_harness_end_line { + for unit_test_line in unit_test.code.iter() { + curr_line_num += 1; + writeln!(temp_writer, "{}", unit_test_line)?; } } } - temp_file.rename(source_path).expect("Could not rename file"); + // 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_file.path(), source_path).with_context(|| { + format!("Couldn't rename tmp source file to actual src file `{source_path}`.") + })?; + + // temp file gets deleted automatically by the NamedTempFile handler Ok(false) } @@ -197,6 +204,11 @@ impl KaniSession { } } +struct UnitTest { + code: Vec, + name: String, +} + /// Generate a formatted unit test from a list of concrete values. fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest { // Hash the concrete values along with the proof harness name. @@ -259,11 +271,6 @@ struct FileLineRange { line_range: Option<(usize, usize)>, } -struct UnitTest { - code: Vec, - name: String, -} - /// Extract concrete values from the CBMC output processed items. /// Note: we extract items that roughly look like the following: /// ```json From 839561a4f5c8cc0a6d73a2a337c246f019e9a754 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:18:01 +0000 Subject: [PATCH 2/4] clippy changes --- kani-driver/src/concrete_playback.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index 173c9324276..12b92635dda 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -18,7 +18,7 @@ use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, BufWriter, Write}; use std::path::Path; use std::process::Command; -use tempfile; +use tempfile::NamedTempFile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -117,7 +117,7 @@ impl KaniSession { ) -> Result { let source_file = File::open(source_path)?; let source_reader = BufReader::new(source_file); - let mut temp_file = tempfile::NamedTempFile::new()?; + let mut temp_file = NamedTempFile::new()?; let mut temp_writer = BufWriter::new(&mut temp_file); let mut curr_line_num = 0; @@ -134,11 +134,11 @@ impl KaniSession { return Ok(true); } curr_line_num += 1; - writeln!(temp_writer, "{}", line)?; + writeln!(temp_writer, "{line}")?; if curr_line_num == proof_harness_end_line { for unit_test_line in unit_test.code.iter() { curr_line_num += 1; - writeln!(temp_writer, "{}", unit_test_line)?; + writeln!(temp_writer, "{unit_test_line}")?; } } } From 7b29d2c5f7df30686b325510520e33cd118b2dd8 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:19:55 +0000 Subject: [PATCH 3/4] add tempfile dependency --- Cargo.lock | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index 475e8611ada..38eaf9e1c11 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -410,6 +410,15 @@ dependencies = [ "libc", ] +[[package]] +name = "fastrand" +version = "1.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51093e27b0797c359783294ca4f0a911c270184cb10f85783b118614a1501be" +dependencies = [ + "instant", +] + [[package]] name = "getopts" version = "0.2.21" @@ -509,6 +518,15 @@ dependencies = [ "hashbrown 0.12.3", ] +[[package]] +name = "instant" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" +dependencies = [ + "cfg-if", +] + [[package]] name = "io-lifetimes" version = "1.0.10" @@ -604,6 +622,7 @@ dependencies = [ "serde_json", "strum", "strum_macros", + "tempfile", "toml", "tracing", "tracing-subscriber", @@ -1049,6 +1068,15 @@ version = "0.6.29" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" +[[package]] +name = "remove_dir_all" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3acd125665422973a33ac9d3dd2df85edad0f4ae9b00dafb1a05e43a9f5ef8e7" +dependencies = [ + "winapi", +] + [[package]] name = "rustc-demangle" version = "0.1.22" From 54470611afd34002c639c5c15bea6e92c9ccb04d Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 13 Apr 2023 02:43:40 +0000 Subject: [PATCH 4/4] Upgrade Rust toolchain to nightly-2023-02-05 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 7844043def0..4747ffef5d2 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-02-04" +channel = "nightly-2023-02-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]