Update dependencies (rustc nightly-2023-01-01, viper v4.0.1)

analysis/Cargo.toml

@@ -8,7 +8,7 @@ edition = "2021"
 log = { version = "0.4", features = ["release_max_level_info"] }
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
-env_logger = "0.9"
+env_logger = "0.10"
 syn = { version = "1.0", features = [ "full", "parsing" ] }
 derive_more = "0.99"
 prusti-rustc-interface = { path = "../prusti-rustc-interface" }

analysis/src/analysis_error.rs

@@ -23,14 +23,11 @@ impl AnalysisError {
         match self {
             AnalysisError::UnsupportedStatement(location) => {
                 let stmt = location_to_stmt_str(*location, mir);
-                format!("Unsupported statement at {:?}: {}", location, stmt)
+                format!("Unsupported statement at {location:?}: {stmt}")
             }
             AnalysisError::NoStateBeforeLocation(location) => {
                 let stmt = location_to_stmt_str(*location, mir);
-                format!(
-                    "There is no state before the statement at {:?} ({})",
-                    location, stmt
-                )
+                format!("There is no state before the statement at {location:?} ({stmt})")
             }
             AnalysisError::NoStateAfterBlock(bb) => {
                 let terminator = &mir[*bb].terminator();

analysis/src/bin/analysis-driver.rs

@@ -59,7 +59,7 @@ fn get_attribute<'tcx>(
                             segments,
                             tokens: _,
                         },
-                    args: ast::MacArgs::Empty,
+                    args: ast::AttrArgs::Empty,
                     tokens: _,
                 } => {
                     segments.len() == 2
@@ -265,7 +265,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
                             Err(e) => eprintln!("{}", e.to_pretty_str(body)),
                         }
                     }
-                    _ => panic!("Unknown domain argument: {}", abstract_domain),
+                    _ => panic!("Unknown domain argument: {abstract_domain}"),
                 }
             }
         });

analysis/src/domains/definitely_accessible/analysis.rs

@@ -65,12 +65,12 @@ impl<'mir, 'tcx: 'mir> DefinitelyAccessibleAnalysis<'mir, 'tcx> {
                     block,
                     statement_index,
                 };
-                let def_init_before = def_init.lookup_before(location).unwrap_or_else(|| {
-                    panic!("No 'def_init' state before location {:?}", location)
-                });
-                let borrowed_before = borrowed.lookup_before(location).unwrap_or_else(|| {
-                    panic!("No 'borrowed' state before location {:?}", location)
-                });
+                let def_init_before = def_init
+                    .lookup_before(location)
+                    .unwrap_or_else(|| panic!("No 'def_init' state before location {location:?}"));
+                let borrowed_before = borrowed
+                    .lookup_before(location)
+                    .unwrap_or_else(|| panic!("No 'borrowed' state before location {location:?}"));
                 let liveness_before = var_live_on_entry
                     .get(&location_table.start_index(location))
                     .unwrap_or(&empty_locals_set);
@@ -86,17 +86,17 @@ impl<'mir, 'tcx: 'mir> DefinitelyAccessibleAnalysis<'mir, 'tcx> {
             // Initialize the state of successors of terminators
             let def_init_after_block = def_init
                 .lookup_after_block(block)
-                .unwrap_or_else(|| panic!("No 'def_init' state after block {:?}", block));
+                .unwrap_or_else(|| panic!("No 'def_init' state after block {block:?}"));
             let borrowed_after_block = borrowed
                 .lookup_after_block(block)
-                .unwrap_or_else(|| panic!("No 'borrowed' state after block {:?}", block));
+                .unwrap_or_else(|| panic!("No 'borrowed' state after block {block:?}"));
             let available_after_block = analysis_state.lookup_mut_after_block(block);
             for successor in block_data.terminator().successors() {
                 let def_init_after = def_init_after_block.get(&successor).unwrap_or_else(|| {
-                    panic!("No 'def_init' state from {:?} to {:?}", block, successor)
+                    panic!("No 'def_init' state from {block:?} to {successor:?}")
                 });
                 let borrowed_after = borrowed_after_block.get(&successor).unwrap_or_else(|| {
-                    panic!("No 'borrowed' state from {:?} to {:?}", block, successor)
+                    panic!("No 'borrowed' state from {block:?} to {successor:?}")
                 });
                 let liveness_after = var_live_on_entry
                     .get(&location_table.start_index(successor.start_location()))

analysis/src/domains/definitely_accessible/state.rs

@@ -42,9 +42,7 @@ impl<'tcx> DefinitelyAccessibleState<'tcx> {
                 self.definitely_accessible
                     .iter()
                     .any(|&place| place == owned_place || is_prefix(owned_place, place)),
-                "In the state before {:?} the place {:?} is owned but not accessible",
-                location,
-                owned_place
+                "In the state before {location:?} the place {owned_place:?} is owned but not accessible"
             );
         }
     }
@@ -57,14 +55,14 @@ impl<'tcx> Serialize for DefinitelyAccessibleState<'tcx> {
         definitely_accessible_set.sort();
         let mut definitely_accessible_strings = vec![];
         for &place in definitely_accessible_set {
-            definitely_accessible_strings.push(format!("{:?}", place));
+            definitely_accessible_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("accessible", &definitely_accessible_strings)?;
         let mut definitely_owned_set: Vec<_> = self.definitely_owned.iter().collect();
         definitely_owned_set.sort();
         let mut definitely_owned_strings = vec![];
         for &place in definitely_owned_set {
-            definitely_owned_strings.push(format!("{:?}", place));
+            definitely_owned_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("owned", &definitely_owned_strings)?;
         seq.end()
@@ -147,16 +145,15 @@ impl<'mir, 'tcx: 'mir> PointwiseState<'mir, 'tcx, DefinitelyAccessibleState<'tcx
             let mut check_stmts = vec![];
             for &place in state.definitely_accessible.iter() {
                 if let Some(place_expr) = pretty_print_place(tcx, self.mir, place) {
-                    check_stmts.push(format!("{}let _ = & {};{}", before, place_expr, after));
+                    check_stmts.push(format!("{before}let _ = & {place_expr};{after}"));
                 }
             }
             for &place in state.definitely_owned.iter() {
                 if let Some(place_expr) = pretty_print_place(tcx, self.mir, place) {
                     let local_decl = &self.mir.local_decls[place.local];
                     // &mut cannot be used on locals that are not marked as mut
                     if local_decl.mutability != mir::Mutability::Not {
-                        check_stmts
-                            .push(format!("{}let _ = &mut {};{}", before, place_expr, after));
+                        check_stmts.push(format!("{before}let _ = &mut {place_expr};{after}"));
                     }
                 }
             }
@@ -202,7 +199,7 @@ fn pretty_print_place<'tcx>(
         })
         .map(|var_debug_info| var_debug_info.name);
     if let Some(name) = local_name {
-        pieces.push(format!("{}", name));
+        pieces.push(format!("{name}"));
     } else {
         return None;
     }
@@ -221,7 +218,7 @@ fn pretty_print_place<'tcx>(
             }
             mir::ProjectionElem::Field(field, field_ty) => {
                 let field_name = describe_field_from_ty(tcx, prev_ty, field, variant)?;
-                pieces.push(format!(".{})", field_name));
+                pieces.push(format!(".{field_name})"));
                 prev_ty = field_ty;
                 variant = None;
             }

analysis/src/domains/definitely_allocated/state.rs

@@ -38,7 +38,7 @@ impl<'mir, 'tcx: 'mir> Serialize for DefinitelyAllocatedState<'mir, 'tcx> {
         let mut seq = serializer.serialize_seq(Some(self.def_allocated_locals.len()))?;
         let oredered_set: BTreeSet<_> = self.def_allocated_locals.iter().collect();
         for local in oredered_set {
-            seq.serialize_element(&format!("{:?}", local))?;
+            seq.serialize_element(&format!("{local:?}"))?;
         }
         seq.end()
     }

analysis/src/domains/definitely_initialized/state.rs

@@ -69,7 +69,7 @@ impl<'mir, 'tcx: 'mir> Serialize for DefinitelyInitializedState<'mir, 'tcx> {
         let mut seq = serializer.serialize_seq(Some(self.def_init_places.len()))?;
         let ordered_place_set: BTreeSet<_> = self.def_init_places.iter().collect();
         for place in ordered_place_set {
-            seq.serialize_element(&format!("{:?}", place))?;
+            seq.serialize_element(&format!("{place:?}"))?;
         }
         seq.end()
     }
@@ -104,15 +104,11 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
                 if place1 != place2 {
                     debug_assert!(
                         !is_prefix(place1, place2),
-                        "The place {:?} is a prefix of the place {:?}",
-                        place2,
-                        place1
+                        "The place {place2:?} is a prefix of the place {place1:?}"
                     );
                     debug_assert!(
                         !is_prefix(place2, place1),
-                        "The place {:?} is a prefix of the place {:?}",
-                        place1,
-                        place2
+                        "The place {place1:?} is a prefix of the place {place2:?}"
                     );
                 }
             }
@@ -177,9 +173,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
         for &place1 in self.def_init_places.iter() {
             debug_assert!(
                 !is_prefix(place1, place) && !is_prefix(place, place1),
-                "Bug: failed to ensure that there are no prefixes: place={:?} place1={:?}",
-                place,
-                place1
+                "Bug: failed to ensure that there are no prefixes: place={place:?} place1={place1:?}"
             );
         }
 

analysis/src/domains/framing/analysis.rs

@@ -55,7 +55,7 @@ impl<'mir, 'tcx: 'mir> FramingAnalysis<'mir, 'tcx> {
                     statement_index,
                 };
                 let acc_before = accessibility.lookup_before(location).unwrap_or_else(|| {
-                    panic!("No 'accessibility' state before location {:?}", location)
+                    panic!("No 'accessibility' state before location {location:?}")
                 });
                 let mut compute_framing = ComputeFramingState::initial(body, self.tcx, acc_before);
                 if let Some(stmt) = body.stmt_at(location).left() {

analysis/src/domains/framing/state.rs

@@ -39,19 +39,15 @@ impl<'tcx> FramingState<'tcx> {
                 self.framed_accessible
                     .iter()
                     .any(|&place| place == owned_place || is_prefix(owned_place, place)),
-                "In the state before {:?} the framed place {:?} is owned but not accessible",
-                location,
-                owned_place
+                "In the state before {location:?} the framed place {owned_place:?} is owned but not accessible"
             );
         }
         for &owned_place in self.framed_accessible.iter() {
             debug_assert!(
                 accessibility.get_definitely_accessible()
                     .iter()
                     .any(|&place| place == owned_place || is_prefix(owned_place, place)),
-                "In the state before {:?} the place {:?} is not accessible, but it is framed as accessible",
-                location,
-                owned_place
+                "In the state before {location:?} the place {owned_place:?} is not accessible, but it is framed as accessible"
             );
         }
         for &owned_place in self.framed_owned.iter() {
@@ -60,9 +56,7 @@ impl<'tcx> FramingState<'tcx> {
                     .get_definitely_owned()
                     .iter()
                     .any(|&place| place == owned_place || is_prefix(owned_place, place)),
-                "In the state before {:?} the place {:?} is not owned, but it is framed as owned",
-                location,
-                owned_place
+                "In the state before {location:?} the place {owned_place:?} is not owned, but it is framed as owned"
             );
         }
     }
@@ -75,14 +69,14 @@ impl<'tcx> Serialize for FramingState<'tcx> {
         definitely_accessible_set.sort();
         let mut definitely_accessible_strings = vec![];
         for &place in definitely_accessible_set {
-            definitely_accessible_strings.push(format!("{:?}", place));
+            definitely_accessible_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("frame_accessible", &definitely_accessible_strings)?;
         let mut definitely_owned_set: Vec<_> = self.framed_owned.iter().collect();
         definitely_owned_set.sort();
         let mut definitely_owned_strings = vec![];
         for &place in definitely_owned_set {
-            definitely_owned_strings.push(format!("{:?}", place));
+            definitely_owned_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("frame_owned", &definitely_owned_strings)?;
         seq.end()

analysis/src/domains/maybe_borrowed/state.rs

@@ -31,14 +31,14 @@ impl<'tcx> Serialize for MaybeBorrowedState<'tcx> {
         maybe_shared_borrowed_set.sort();
         let mut maybe_shared_borrowed_strings = vec![];
         for &place in maybe_shared_borrowed_set {
-            maybe_shared_borrowed_strings.push(format!("{:?}", place));
+            maybe_shared_borrowed_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("frozen", &maybe_shared_borrowed_strings)?;
         let mut maybe_mut_borrowed_set: Vec<_> = self.maybe_mut_borrowed.iter().collect();
         maybe_mut_borrowed_set.sort();
         let mut maybe_mut_borrowed_strings = vec![];
         for &place in maybe_mut_borrowed_set {
-            maybe_mut_borrowed_strings.push(format!("{:?}", place));
+            maybe_mut_borrowed_strings.push(format!("{place:?}"));
         }
         seq.serialize_entry("blocked", &maybe_mut_borrowed_strings)?;
         seq.end()

analysis/src/domains/reaching_definitions/state.rs

@@ -87,12 +87,12 @@ impl<'mir, 'tcx: 'mir> Serialize for ReachingDefsState<'mir, 'tcx> {
                         let stmt = location_to_stmt_str(*l, self.mir);
                         // Include the location to differentiate between same statement on
                         // different lines.
-                        location_vec.push(format!("{:?}: {}", l, stmt));
+                        location_vec.push(format!("{l:?}: {stmt}"));
                     }
-                    DefLocation::Parameter(idx) => location_vec.push(format!("arg{}", idx)),
+                    DefLocation::Parameter(idx) => location_vec.push(format!("arg{idx}")),
                 }
             }
-            map.serialize_entry(&format!("{:?}", local), &location_vec)?;
+            map.serialize_entry(&format!("{local:?}"), &location_vec)?;
         }
         map.end()
     }

analysis/src/mir_utils.rs

@@ -87,7 +87,7 @@ pub fn location_to_stmt_str(location: mir::Location, mir: &mir::Body) -> String
     let bb_mir = &mir[location.block];
     if location.statement_index < bb_mir.statements.len() {
         let stmt = &bb_mir.statements[location.statement_index];
-        format!("{:?}", stmt)
+        format!("{stmt:?}")
     } else {
         // location = terminator
         let terminator = bb_mir.terminator();
@@ -133,8 +133,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
             ty::Adt(def, substs) => {
                 assert!(
                     def.is_struct(),
-                    "Only structs can be expanded. Got def={:?}.",
-                    def
+                    "Only structs can be expanded. Got def={def:?}."
                 );
                 let variant = def.non_enum_variant();
                 for (index, field_def) in variant.fields.iter().enumerate() {
@@ -332,9 +331,8 @@ pub fn is_copy<'tcx>(
         // the freshly-created `InferCtxt` (i.e. `tcx.infer_ctxt().enter(..)`) will cause
         // a panic, since those inference variables don't exist in the new `InferCtxt`.
         // See: https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Panic.20in.20is_copy_modulo_regions
-        let fresh_ty = infcx.freshen(ty);
         infcx
-            .type_implements_trait(copy_trait, fresh_ty, ty::List::empty(), param_env)
+            .type_implements_trait(copy_trait, [infcx.freshen(ty)], param_env)
             .must_apply_considering_regions()
     } else {
         false

analysis/src/pointwise_state.rs

@@ -48,7 +48,7 @@ impl<'mir, 'tcx: 'mir, S: Serialize> Serialize for PointwiseState<'mir, 'tcx, S>
                 let state = self.lookup_before(location).unwrap();
 
                 // output statement
-                stmt_vec.push(("state:", state, format!("statement: {:?}", stmt)));
+                stmt_vec.push(("state:", state, format!("statement: {stmt:?}")));
             }
 
             let term_location = self.mir.terminator_loc(bb);
@@ -60,11 +60,11 @@ impl<'mir, 'tcx: 'mir, S: Serialize> Serialize for PointwiseState<'mir, 'tcx, S>
             let map_after = self.lookup_after_block(bb).unwrap_or(&new_map);
             let ordered_succ_map: BTreeMap<_, _> = map_after
                 .iter()
-                .map(|(bb, s)| (format!("{:?}", bb), ("state:", s)))
+                .map(|(bb, s)| (format!("{bb:?}"), ("state:", s)))
                 .collect();
 
             map.serialize_entry(
-                &format!("{:?}", bb),
+                &format!("{bb:?}"),
                 &(
                     stmt_vec,
                     "state before terminator:",