Merge branch 'main' into update-toolchain-2023-09-23

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"

cprover_bindings/src/goto_program/builtin.rs

@@ -329,7 +329,7 @@ impl BuiltinFn {
 /// Converters: build symbols and expressions from Builtins
 impl BuiltinFn {
     pub fn as_symbol(&self) -> Symbol {
-        Symbol::builtin_function(&self.to_string(), self.param_types(), self.return_type())
+        Symbol::builtin_function(self.to_string(), self.param_types(), self.return_type())
     }
 
     pub fn as_expr(&self) -> Expr {

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         let mem_place =
-            self.symbol_table.lookup(&self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr();
+            self.symbol_table.lookup(self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr();
         mem_place.address_of()
     }
 
@@ -573,16 +573,16 @@ impl<'tcx> GotocCtx<'tcx> {
         // initializers. For example, for a boolean static variable, the variable will have type
         // CBool and the initializer will be a single byte (a one-character array) representing the
         // bit pattern for the boolean value.
-        let alloc_typ_ref = self.ensure_struct(&struct_name, &struct_name, |ctx, _| {
+        let alloc_typ_ref = self.ensure_struct(struct_name, struct_name, |ctx, _| {
             ctx.codegen_allocation_data(alloc)
                 .iter()
                 .enumerate()
                 .map(|(i, d)| match d {
                     AllocData::Bytes(bytes) => DatatypeComponent::field(
-                        &i.to_string(),
+                        i.to_string(),
                         Type::unsigned_int(8).array_of(bytes.len()),
                     ),
-                    AllocData::Expr(e) => DatatypeComponent::field(&i.to_string(), e.typ().clone()),
+                    AllocData::Expr(e) => DatatypeComponent::field(i.to_string(), e.typ().clone()),
                 })
                 .collect()
         });

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -268,8 +268,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     | ty::Param(_)
                     | ty::Infer(_)
                     | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"),
-                    ty::Tuple(_) => Ok(parent_expr
-                        .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)),
+                    ty::Tuple(_) => {
+                        Ok(parent_expr
+                            .member(Self::tuple_fld_name(field.index()), &self.symbol_table))
+                    }
                     ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field(
                         parent_expr,
                         *field,
@@ -278,10 +280,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     // if we fall here, then we are handling either a struct or a union
                     ty::Adt(def, _) => {
                         let field = &def.variants().raw[0].fields[*field];
-                        Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table))
+                        Ok(parent_expr.member(field.name.to_string(), &self.symbol_table))
                     }
                     ty::Closure(..) => {
-                        Ok(parent_expr.member(&field.index().to_string(), &self.symbol_table))
+                        Ok(parent_expr.member(field.index().to_string(), &self.symbol_table))
                     }
                     ty::Generator(..) => {
                         let field_name = self.generator_field_name(field.as_usize());
@@ -299,7 +301,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // if we fall here, then we are handling an enum
             TypeOrVariant::Variant(parent_var) => {
                 let field = &parent_var.fields[*field];
-                Ok(parent_expr.member(&field.name.to_string(), &self.symbol_table))
+                Ok(parent_expr.member(field.name.to_string(), &self.symbol_table))
             }
             TypeOrVariant::GeneratorVariant(_var_idx) => {
                 let field_name = self.generator_field_name(field.index());

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -864,7 +864,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // We need to pad to the next offset
             let padding_size = next_offset - current_offset;
             let name = format!("$pad{idx}");
-            Some(DatatypeComponent::padding(&name, padding_size.bits()))
+            Some(DatatypeComponent::padding(name, padding_size.bits()))
         } else {
             None
         }
@@ -1378,7 +1378,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .iter()
                 .map(|f| {
                     DatatypeComponent::field(
-                        &f.name.to_string(),
+                        f.name.to_string(),
                         ctx.codegen_ty(f.ty(ctx.tcx, subst)),
                     )
                 })
@@ -1641,7 +1641,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     None
                 } else {
                     Some(DatatypeComponent::field(
-                        &case.name.to_string(),
+                        case.name.to_string(),
                         self.codegen_enum_case_struct(
                             name,
                             pretty_name,

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -271,7 +271,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
                     let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
                     let test_model_path = &metadata.goto_file.as_ref().unwrap();
-                    std::fs::copy(&model_path, &test_model_path).expect(&format!(
+                    std::fs::copy(&model_path, test_model_path).expect(&format!(
                         "Failed to copy {} to {}",
                         model_path.display(),
                         test_model_path.display()

kani-compiler/src/kani_compiler.rs

@@ -352,7 +352,7 @@ impl KaniCompiler {
     /// Write the metadata to a file
     fn store_metadata(&self, metadata: &KaniMetadata, filename: &Path) {
         debug!(?filename, "write_metadata");
-        let out_file = File::create(&filename).unwrap();
+        let out_file = File::create(filename).unwrap();
         let writer = BufWriter::new(out_file);
         if self.queries.lock().unwrap().args().output_pretty_json {
             serde_json::to_writer_pretty(writer, &metadata).unwrap();

kani-compiler/src/kani_middle/reachability.rs

@@ -725,7 +725,7 @@ mod debug {
                 debug!(?target, "dump_dot");
                 let outputs = tcx.output_filenames(());
                 let path = outputs.output_path(OutputType::Metadata).with_extension("dot");
-                let out_file = File::create(&path)?;
+                let out_file = File::create(path)?;
                 let mut writer = BufWriter::new(out_file);
                 writeln!(writer, "digraph ReachabilityGraph {{")?;
                 if target.is_empty() {

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/args/mod.rs

@@ -427,7 +427,7 @@ fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> {
     if is_set {
         Err(Error::raw(
             ErrorKind::UnknownArgument,
-            &format!("argument `{}` cannot be used with standalone Kani.", name),
+            format!("argument `{}` cannot be used with standalone Kani.", name),
         ))
     } else {
         Ok(())
@@ -453,7 +453,7 @@ impl ValidateArgs for StandaloneArgs {
             if !input.is_file() {
                 return Err(Error::raw(
                     ErrorKind::InvalidValue,
-                    &format!(
+                    format!(
                         "Invalid argument: Input invalid. `{}` is not a regular file.",
                         input.display()
                     ),
@@ -583,7 +583,7 @@ impl ValidateArgs for VerificationArgs {
             if out_dir.exists() && !out_dir.is_dir() {
                 return Err(Error::raw(
                     ErrorKind::InvalidValue,
-                    &format!(
+                    format!(
                         "Invalid argument: `--target-dir` argument `{}` is not a directory",
                         out_dir.display()
                     ),

kani-driver/src/args/playback_args.rs

@@ -74,7 +74,7 @@ impl ValidateArgs for KaniPlaybackArgs {
         if !self.input.is_file() {
             return Err(Error::raw(
                 ErrorKind::InvalidValue,
-                &format!(
+                format!(
                     "Invalid argument: Input invalid. `{}` is not a regular file.",
                     self.input.display()
                 ),

kani-driver/src/assess/metadata.rs

@@ -88,7 +88,7 @@ pub struct SessionError {
 /// If given the argument to so do, write the assess metadata to the target file.
 pub(crate) fn write_metadata(args: &AssessArgs, metadata: AssessMetadata) -> Result<()> {
     if let Some(path) = &args.emit_metadata {
-        let out_file = File::create(&path)?;
+        let out_file = File::create(path)?;
         let writer = BufWriter::new(out_file);
         // use pretty for now to keep things readable and debuggable, but this should change eventually
         serde_json::to_writer_pretty(writer, &metadata)?;

kani-driver/src/assess/scan.rs

@@ -179,7 +179,7 @@ fn invoke_assess(
     // Additionally, this should be `--manifest-path` but `cargo kani` doesn't support that yet.
     cmd.arg("-p").arg(package);
     cmd.arg("--enable-unstable"); // This has to be after `-p` due to an argument parsing bug in kani-driver
-    cmd.args(&["assess", "--emit-metadata"])
+    cmd.args(["assess", "--emit-metadata"])
         .arg(outfile)
         .current_dir(dir)
         .stdout(log.try_clone()?)

kani-driver/src/concrete_playback/playback.rs

@@ -84,7 +84,7 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result<PathBuf>
         rustc_args.push("--error-format=json".into());
     }
 
-    let mut cmd = Command::new(&install.kani_compiler()?);
+    let mut cmd = Command::new(install.kani_compiler()?);
     cmd.args(rustc_args);
 
     session::run_terminal(&args.playback.common_opts, cmd)?;

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/project.rs

@@ -364,6 +364,6 @@ fn metadata_with_function(
 // Note: `out_dir` is already on canonical form, so no need to invoke `try_new()`.
 fn standalone_artifact(out_dir: &Path, crate_name: &String, typ: ArtifactType) -> Artifact {
     let mut path = out_dir.join(crate_name);
-    let _ = path.set_extension(&typ);
+    let _ = path.set_extension(typ);
     Artifact { path, typ }
 }

kani-driver/src/session.rs

@@ -216,7 +216,7 @@ pub fn run_redirect(
             stdout.display()
         );
     }
-    let output_file = std::fs::File::create(&stdout)?;
+    let output_file = std::fs::File::create(stdout)?;
     cmd.stdout(output_file);
 
     let program = cmd.get_program().to_string_lossy().to_string();

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)