Automatic toolchain upgrade to nightly-2023-02-05

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"

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

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::NamedTempFile;
 
 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<bool> {
-        // 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 = 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<String>,
+    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<String>,
-    name: String,
-}
-
 /// Extract concrete values from the CBMC output processed items.
 /// Note: we extract items that roughly look like the following:
 /// ```json

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"]