Merge pull request #1444 from viperproject/auto-update-nightly-2023-0…

…8-15

Update dependencies (rustc nightly-2023-08-15)

analysis/src/domains/reaching_definitions/state.rs

@@ -106,10 +106,7 @@ impl<'mir, 'tcx: 'mir> ReachingDefsState<'mir, 'tcx> {
         let stmt = &self.mir[location.block].statements[location.statement_index];
         if let mir::StatementKind::Assign(box (ref target, _)) = stmt.kind {
             if let Some(local) = target.as_local() {
-                let location_set = self
-                    .reaching_defs
-                    .entry(local)
-                    .or_insert_with(FxHashSet::default);
+                let location_set = self.reaching_defs.entry(local).or_default();
                 location_set.clear();
                 location_set.insert(DefLocation::Assignment(location));
             }
@@ -134,10 +131,7 @@ impl<'mir, 'tcx: 'mir> ReachingDefsState<'mir, 'tcx> {
                 if let Some(bb) = target {
                     let mut dest_state = self.clone();
                     if let Some(local) = destination.as_local() {
-                        let location_set = dest_state
-                            .reaching_defs
-                            .entry(local)
-                            .or_insert_with(FxHashSet::default);
+                        let location_set = dest_state.reaching_defs.entry(local).or_default();
                         location_set.clear();
                         location_set.insert(DefLocation::Assignment(location));
                     }
@@ -150,10 +144,8 @@ impl<'mir, 'tcx: 'mir> ReachingDefsState<'mir, 'tcx> {
                     // while keeping all others
                     if target.is_some() {
                         if let Some(local) = destination.as_local() {
-                            let location_set = cleanup_state
-                                .reaching_defs
-                                .entry(local)
-                                .or_insert_with(FxHashSet::default);
+                            let location_set =
+                                cleanup_state.reaching_defs.entry(local).or_default();
                             location_set.insert(DefLocation::Assignment(location));
                         }
                     }
@@ -182,10 +174,7 @@ impl<'mir, 'tcx: 'mir> AbstractState for ReachingDefsState<'mir, 'tcx> {
 
     fn join(&mut self, other: &Self) {
         for (local, other_locations) in other.reaching_defs.iter() {
-            let location_set = self
-                .reaching_defs
-                .entry(*local)
-                .or_insert_with(FxHashSet::default);
+            let location_set = self.reaching_defs.entry(*local).or_default();
             location_set.extend(other_locations);
         }
     }

analysis/src/mir_utils.rs

@@ -157,7 +157,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
             }
         }
         ty::Closure(_, substs) => {
-            for (index, subst_ty) in substs.as_closure().upvar_tys().enumerate() {
+            for (index, subst_ty) in substs.as_closure().upvar_tys().iter().enumerate() {
                 if Some(index) != without_field {
                     let field = FieldIdx::from_usize(index);
                     let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);
@@ -166,7 +166,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
             }
         }
         ty::Generator(_, substs, _) => {
-            for (index, subst_ty) in substs.as_generator().upvar_tys().enumerate() {
+            for (index, subst_ty) in substs.as_generator().upvar_tys().iter().enumerate() {
                 if Some(index) != without_field {
                     let field = FieldIdx::from_usize(index);
                     let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);

analysis/src/pointwise_state.rs

@@ -123,9 +123,7 @@ impl<'mir, 'tcx: 'mir, S: Serialize> PointwiseState<'mir, 'tcx, S> {
         &mut self,
         block: mir::BasicBlock,
     ) -> &mut FxHashMap<mir::BasicBlock, S> {
-        self.state_after_block
-            .entry(block)
-            .or_insert_with(FxHashMap::default)
+        self.state_after_block.entry(block).or_default()
     }
 
     /// Update the state before the `location`.

prusti-interface/src/environment/loops.rs

@@ -273,17 +273,15 @@ impl ProcedureLoops {
 
         let mut loop_bodies = FxHashMap::default();
         for &(source, target) in back_edges.iter() {
-            let body = loop_bodies.entry(target).or_insert_with(FxHashSet::default);
+            let body = loop_bodies.entry(target).or_default();
             collect_loop_body(target, source, real_edges, body);
         }
 
         let mut enclosing_loop_heads_set: FxHashMap<BasicBlockIndex, FxHashSet<BasicBlockIndex>> =
             FxHashMap::default();
         for (&loop_head, loop_body) in loop_bodies.iter() {
             for &block in loop_body.iter() {
-                let heads_set = enclosing_loop_heads_set
-                    .entry(block)
-                    .or_insert_with(FxHashSet::default);
+                let heads_set = enclosing_loop_heads_set.entry(block).or_default();
                 heads_set.insert(loop_head);
             }
         }

prusti-interface/src/environment/polonius_info.rs

@@ -314,9 +314,9 @@ pub fn graphviz<'tcx>(
         let from_block = from.location.block;
         let to = interner.get_point(to_index);
         let to_block = to.location.block;
-        let from_points = blocks.entry(from_block).or_insert_with(FxHashSet::default);
+        let from_points: &mut FxHashSet<_> = blocks.entry(from_block).or_default();
         from_points.insert(from_index);
-        let to_points = blocks.entry(to_block).or_insert_with(FxHashSet::default);
+        let to_points: &mut FxHashSet<_> = blocks.entry(to_block).or_default();
         to_points.insert(to_index);
         if from_block != to_block {
             block_edges.insert((from_block, to_block));
@@ -441,7 +441,7 @@ fn add_fake_facts<'a, 'tcx: 'a>(
     let mut outlives_at_point = FxHashMap::default();
     for &(region1, region2, point) in all_facts.subset_base.iter() {
         if !universal_region.contains(&region1) && !universal_region.contains(&region2) {
-            let subset_base = outlives_at_point.entry(point).or_insert_with(Vec::new);
+            let subset_base: &mut Vec<_> = outlives_at_point.entry(point).or_default();
             subset_base.push((region1, region2));
         }
     }
@@ -1174,7 +1174,6 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
             return Ok(None);
         };
         let (dest, source) = assignment.as_assign().unwrap();
-        let dest = dest;
         let source = source.clone();
         let location = self.loan_position[loan];
         Ok(Some(LoanPlaces {
@@ -2195,32 +2194,25 @@ impl AdditionalFacts {
         let mut zombie_requires_map =
             prusti_rustc_interface::data_structures::fx::FxHashMap::default();
         for (region, loan, point) in &zombie_requires.elements {
-            zombie_requires_map
-                .entry(*point)
-                .or_insert_with(BTreeMap::default)
-                .entry(*region)
-                .or_insert_with(BTreeSet::new)
-                .insert(*loan);
+            let loans_map: &mut BTreeMap<_, _> = zombie_requires_map.entry(*point).or_default();
+            let loans: &mut BTreeSet<_> = loans_map.entry(*region).or_default();
+            loans.insert(*loan);
         }
 
         let zombie_borrow_live_at = zombie_borrow_live_at.complete();
         let mut zombie_borrow_live_at_map =
             prusti_rustc_interface::data_structures::fx::FxHashMap::default();
         for (loan, point) in &zombie_borrow_live_at.elements {
-            zombie_borrow_live_at_map
-                .entry(*point)
-                .or_insert_with(Vec::new)
-                .push(*loan);
+            let loans: &mut Vec<_> = zombie_borrow_live_at_map.entry(*point).or_default();
+            loans.push(*loan);
         }
 
         let borrow_become_zombie_at = borrow_become_zombie_at.complete();
         let mut borrow_become_zombie_at_map =
             prusti_rustc_interface::data_structures::fx::FxHashMap::default();
         for (loan, point) in &borrow_become_zombie_at.elements {
-            borrow_become_zombie_at_map
-                .entry(*point)
-                .or_insert_with(Vec::new)
-                .push(*loan);
+            let loans: &mut Vec<_> = borrow_become_zombie_at_map.entry(*point).or_default();
+            loans.push(*loan);
         }
 
         (

prusti-interface/src/environment/query.rs

@@ -7,9 +7,7 @@ use prusti_rustc_interface::{
     hir::hir_id::HirId,
     middle::{
         hir::map::Map,
-        ty::{
-            self, BoundConstness, GenericArgsRef, ImplPolarity, ParamEnv, TraitPredicate, TyCtxt,
-        },
+        ty::{self, GenericArgsRef, ImplPolarity, ParamEnv, TraitPredicate, TyCtxt},
     },
     span::{
         def_id::{DefId, LocalDefId},
@@ -291,7 +289,6 @@ impl<'tcx> EnvQuery<'tcx> {
                 ParamEnv::reveal_all(),
                 TraitPredicate {
                     trait_ref,
-                    constness: BoundConstness::NotConst,
                     polarity: ImplPolarity::Positive,
                 },
             );

prusti-tests/tests/cargo_verify/prusti_toml_fail/output.stderr

@@ -1,2 +1,3 @@
-thread 'main' panicked at './Prusti.toml file contains unknown configuration flag: “CHECK_OVERFLOWS”', prusti-utils/src/config.rs:[..]
+thread 'main' panicked at prusti-utils/src/config.rs:[..]
+Found an unknown configuration flag `CHECK_OVERFLOWS` in the file `./Prusti.toml`
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

prusti-utils/src/config.rs

@@ -194,13 +194,13 @@ lazy_static::lazy_static! {
         settings.merge(
             Environment::with_prefix("DEFAULT_PRUSTI").ignore_empty(true)
         ).unwrap();
-        check_keys(&settings, &allowed_keys, "default environment variables");
+        check_keys(&settings, &allowed_keys, "the `DEFAULT_PRUSTI_*` environment variables");
 
         // 2. Override with an optional "Prusti.toml" file in manifest dir
         let manifest_dir = env::var("CARGO_MANIFEST_DIR").unwrap_or_else(|_| ".".to_string());
         let file = PathBuf::from(manifest_dir).join("Prusti.toml");
         settings.merge(File::from(file.as_path()).required(false)).unwrap();
-        check_keys(&settings, &allowed_keys, &format!("{} file", file.to_string_lossy()));
+        check_keys(&settings, &allowed_keys, &format!("the file `{}`", file.to_string_lossy()));
 
         // 3. Override with env variables (`PRUSTI_VIPER_BACKEND`, ...)
         settings.merge(
@@ -213,13 +213,13 @@ lazy_static::lazy_static! {
                 .with_list_parse_key("verify_only_basic_block_path")
                 .list_separator(" ")
         ).unwrap();
-        check_keys(&settings, &allowed_keys, "environment variables");
+        check_keys(&settings, &allowed_keys, "the `PRUSTI_*` environment variables");
 
         // 4. Override with command-line arguments -P<arg>=<val>
         settings.merge(
             CommandLine::with_prefix("-P").ignore_invalid(true)
         ).unwrap();
-        check_keys(&settings, &allowed_keys, "command line arguments");
+        check_keys(&settings, &allowed_keys, "the `-P` command line arguments");
 
         settings
     });
@@ -239,7 +239,7 @@ fn check_keys(settings: &Config, allowed_keys: &FxHashSet<String>, source: &str)
     for key in settings.cache.clone().into_table().unwrap().keys() {
         assert!(
             allowed_keys.contains(key),
-            "{source} contains unknown configuration flag: “{key}”",
+            "Found an unknown configuration flag `{key}` in {source}",
         );
     }
 }
@@ -322,14 +322,14 @@ pub fn viper_backend() -> String {
 /// configuration flag to the correct path to Z3.
 pub fn smt_solver_path() -> String {
     read_setting::<Option<String>>("smt_solver_path")
-        .expect("please set the smt_solver_path configuration flag")
+        .expect("Please set the smt_solver_path configuration flag")
 }
 
 /// The path to the SMT solver wrapper. `prusti-rustc` is expected to set this
 /// configuration flag to the correct path.
 pub fn smt_solver_wrapper_path() -> String {
     read_setting::<Option<String>>("smt_solver_wrapper_path")
-        .expect("please set the smt_solver_wrapper_path configuration flag")
+        .expect("Please set the smt_solver_wrapper_path configuration flag")
 }
 
 /// The path to the Boogie executable. `prusti-rustc` is expected to set this
@@ -359,7 +359,7 @@ pub fn viper_home() -> String {
 /// configuration flag to the correct path.
 pub fn java_home() -> String {
     read_setting::<Option<String>>("java_home")
-        .expect("please set the java_home configuration flag")
+        .expect("Please set the java_home configuration flag")
 }
 
 /// When enabled, Prusti will check for an absence of `panic!`s.
@@ -751,7 +751,7 @@ pub fn verification_deadline() -> Option<u64> {
     read_setting::<Option<i64>>("verification_deadline").map(|value| {
         value
             .try_into()
-            .expect("verification_deadline must be a valid u64")
+            .expect("Verification_deadline must be a valid u64")
     })
 }
 

prusti-viper/src/encoder/foldunfold/log.rs

@@ -11,7 +11,7 @@ use crate::encoder::foldunfold::{action::Action, perm::Perm, FoldUnfoldError};
 use log::trace;
 use prusti_common::utils::to_string::ToString;
 use rustc_hash::FxHashMap;
-use std::{cmp::Ordering, rc::Rc, sync::RwLock};
+use std::{cmp::Ordering, fmt::Write, rc::Rc, sync::RwLock};
 use vir_crate::polymorphic as vir;
 
 // Note: Now every PathCtxt has its own EventLog, because a Borrow no longer unique
@@ -100,7 +100,7 @@ impl EventLog {
         perm: vir::Expr,
         original_place: vir::Expr,
     ) {
-        let entry = self.duplicated_reads.entry(borrow).or_insert_with(Vec::new);
+        let entry = self.duplicated_reads.entry(borrow).or_default();
         entry.push((perm, original_place, self.id_generator));
         self.id_generator += 1;
     }
@@ -147,10 +147,10 @@ impl EventLog {
         trace!(
             "[exit] get_duplicated_read_permissions({:?}) = {}",
             borrow,
-            result
-                .iter()
-                .map(|(a, p, id)| format!("({a}, {p}, {id}), "))
-                .collect::<String>()
+            result.iter().fold(String::new(), |mut output, (a, p, id)| {
+                let _ = write!(output, "({a}, {p}, {id}), ");
+                output
+            })
         );
         result
             .into_iter()
@@ -161,10 +161,7 @@ impl EventLog {
     /// `perm` is an instance of either `PredicateAccessPredicate` or `FieldAccessPredicate`.
     pub fn log_convertion_to_read(&mut self, borrow: vir::borrows::Borrow, perm: vir::Expr) {
         assert!(perm.get_perm_amount() == vir::PermAmount::Remaining);
-        let entry = self
-            .converted_to_read_places
-            .entry(borrow)
-            .or_insert_with(Vec::new);
+        let entry = self.converted_to_read_places.entry(borrow).or_default();
         entry.push(perm);
     }
 

prusti-viper/src/encoder/foldunfold/mod.rs

@@ -16,7 +16,7 @@ use crate::encoder::high::types::HighTypeEncoderInterface;
 use prusti_common::{config, report, utils::to_string::ToString, vir::ToGraphViz, Stopwatch};
 use prusti_rustc_interface::middle::mir;
 use rustc_hash::{FxHashMap, FxHashSet};
-use std::{self, fmt, ops::Deref};
+use std::{self, fmt, fmt::Write, ops::Deref};
 use vir_crate::{
     polymorphic as vir,
     polymorphic::{
@@ -865,8 +865,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
                 "acc_perms = {}",
                 acc_perms
                     .iter()
-                    .map(|(a, p, id)| format!("({a}, {p}, {id}), "))
-                    .collect::<String>()
+                    .fold(String::new(), |mut output, (a, p, id)| {
+                        let _ = write!(output, "({a}, {p}, {id}), ");
+                        output
+                    })
             );
             for (place, perm_amount, _) in acc_perms {
                 trace!("acc place: {} {}", place, perm_amount);

prusti-viper/src/encoder/foldunfold/perm.rs

@@ -191,10 +191,8 @@ where
     fn group_by_label(&mut self) -> FxHashMap<Option<String>, Vec<Perm>> {
         let mut res_perms = FxHashMap::default();
         for perm in self {
-            res_perms
-                .entry(perm.get_label().cloned())
-                .or_insert_with(Vec::new)
-                .push(perm.clone());
+            let perms: &mut Vec<_> = res_perms.entry(perm.get_label().cloned()).or_default();
+            perms.push(perm.clone());
         }
         res_perms
     }

prusti-viper/src/encoder/foldunfold/process_expire_borrows.rs

@@ -197,7 +197,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> FoldUnfold<'p, 'v, 'tcx> {
                 for perm in &dropped_permissions {
                     let comment = format!("restored (from log): {perm}");
                     let key = (predecessor, curr_block_index);
-                    let entry = cfg.edges.entry(key).or_insert_with(Vec::new);
+                    let entry = cfg.edges.entry(key).or_default();
                     entry.push(vir::Stmt::comment(comment));
                 }
                 pctxt
@@ -228,7 +228,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> FoldUnfold<'p, 'v, 'tcx> {
                     }
                 }
                 let key = (src_index, curr_block_index);
-                let entry = cfg.edges.entry(key).or_insert_with(Vec::new);
+                let entry = cfg.edges.entry(key).or_default();
                 entry.extend(stmts_to_add);
             }
         }

prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs

@@ -843,7 +843,7 @@ where
         let ty = self.place_ty(self.place);
         match ty.kind() {
             ty::Closure(_, args) => {
-                let tys: Vec<_> = args.as_closure().upvar_tys().collect();
+                let tys: Vec<_> = args.as_closure().upvar_tys().iter().collect();
                 self.open_drop_for_tuple(&tys)
             }
             // Note that `elaborate_drops` only drops the upvars of a generator,
@@ -853,7 +853,7 @@ where
             // It effectively only contains upvars until the generator transformation runs.
             // See librustc_body/transform/generator.rs for more details.
             ty::Generator(_, args, _) => {
-                let tys: Vec<_> = args.as_generator().upvar_tys().collect();
+                let tys: Vec<_> = args.as_generator().upvar_tys().iter().collect();
                 self.open_drop_for_tuple(&tys)
             }
             ty::Tuple(fields) => self.open_drop_for_tuple(fields),