Update dependencies (rustc nightly-2022-10-15, viper v4.0.0-RC)

analysis/src/domains/definitely_accessible/state.rs

@@ -227,6 +227,7 @@ fn pretty_print_place<'tcx>(
             }
             mir::ProjectionElem::Index(..)
             | mir::ProjectionElem::ConstantIndex { .. }
+            | mir::ProjectionElem::OpaqueCast(..)
             | mir::ProjectionElem::Subslice { .. } => {
                 // It's not possible to move-out or borrow an individual element.
                 unreachable!()

analysis/src/mir_utils.rs

@@ -220,7 +220,8 @@ pub fn expand_one_level<'tcx>(
         | mir::ProjectionElem::Index(..)
         | mir::ProjectionElem::ConstantIndex { .. }
         | mir::ProjectionElem::Subslice { .. }
-        | mir::ProjectionElem::Downcast(..) => vec![],
+        | mir::ProjectionElem::Downcast(..)
+        | mir::ProjectionElem::OpaqueCast(..) => vec![],
     };
     (new_current_place, other_places)
 }
@@ -326,21 +327,23 @@ pub fn is_copy<'tcx>(
         // `type_implements_trait` doesn't consider that.
         matches!(mutability, mir::Mutability::Not)
     } else if let Some(copy_trait) = tcx.lang_items().copy_trait() {
-        tcx.infer_ctxt().enter(|infcx| {
-            // If `ty` has any inference variables (e.g. a region variable), then using it with
-            // 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)
-                .must_apply_considering_regions()
-        })
+        let infcx = tcx.infer_ctxt().build();
+        // If `ty` has any inference variables (e.g. a region variable), then using it with
+        // 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)
+            .must_apply_considering_regions()
     } else {
         false
     }
 }
 
+/// Given an assignment `let _ = & <borrowed_place>`, this function returns the place that is
+/// blocked by the loan.
+/// For example, `let _ = &x.f.g` blocks just `x.f.g`, but `let _ = &x.f[0].g` blocks `x.f`.
 pub fn get_blocked_place<'tcx>(tcx: TyCtxt<'tcx>, borrowed: Place<'tcx>) -> Place<'tcx> {
     for (place_ref, place_elem) in borrowed.iter_projections() {
         match place_elem {
@@ -354,7 +357,9 @@ pub fn get_blocked_place<'tcx>(tcx: TyCtxt<'tcx>, borrowed: Place<'tcx>) -> Plac
                 })
                 .into();
             }
-            mir::ProjectionElem::Field(..) | mir::ProjectionElem::Downcast(..) => {
+            mir::ProjectionElem::Field(..)
+            | mir::ProjectionElem::Downcast(..)
+            | mir::ProjectionElem::OpaqueCast(..) => {
                 // Continue
             }
         }

prusti-common/src/vir/to_viper.rs

@@ -1221,7 +1221,7 @@ fn unsigned_max_for_size(size: BitVectorSize) -> u128 {
         BitVectorSize::BV16 => u16::MAX as u128,
         BitVectorSize::BV32 => u32::MAX as u128,
         BitVectorSize::BV64 => u64::MAX as u128,
-        BitVectorSize::BV128 => u128::MAX as u128,
+        BitVectorSize::BV128 => u128::MAX,
     }
 }
 

prusti-interface/src/environment/body.rs

@@ -4,11 +4,7 @@ use prusti_rustc_interface::{
     macros::{TyDecodable, TyEncodable},
     middle::{
         mir,
-        ty::{
-            self,
-            subst::{Subst, SubstsRef},
-            TyCtxt,
-        },
+        ty::{self, subst::SubstsRef, TyCtxt},
     },
     span::def_id::{DefId, LocalDefId},
 };

prusti-interface/src/environment/borrowck/regions.rs

@@ -67,11 +67,16 @@ impl PlaceRegions {
                         not supported"
                         .to_string(),
                 )),
-                mir::ProjectionElem::Downcast(_, _) => Err(PlaceRegionsError::Unsupported(
+                mir::ProjectionElem::Downcast(..) => Err(PlaceRegionsError::Unsupported(
                     "determining the region of a downcast is \
                         not supported"
                         .to_string(),
                 )),
+                mir::ProjectionElem::OpaqueCast(..) => Err(PlaceRegionsError::Unsupported(
+                    "determining the region of an opaque cast is \
+                        not supported"
+                        .to_string(),
+                )),
             })
             .collect::<Result<_, _>>()?;
         Ok((place.local, indices))

prusti-interface/src/environment/mir_body/patch/compiler.rs

@@ -104,14 +104,14 @@ impl<'tcx> MirPatch<'tcx> {
         let index = self.next_local;
         self.next_local += 1;
         self.new_locals.push(LocalDecl::new(ty, span));
-        Local::new(index as usize)
+        Local::new(index)
     }
 
     pub fn new_internal(&mut self, ty: Ty<'tcx>, span: Span) -> Local {
         let index = self.next_local;
         self.next_local += 1;
         self.new_locals.push(LocalDecl::new(ty, span).internal());
-        Local::new(index as usize)
+        Local::new(index)
     }
 
     pub fn new_block(&mut self, data: BasicBlockData<'tcx>) -> BasicBlock {

prusti-interface/src/environment/query.rs

@@ -6,9 +6,8 @@ use prusti_rustc_interface::{
     middle::{
         hir::map::Map,
         ty::{
-            self,
-            subst::{Subst, SubstsRef},
-            Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate, TraitRef, TyCtxt,
+            self, subst::SubstsRef, Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate,
+            TraitRef, TyCtxt,
         },
     },
     span::{
@@ -18,7 +17,10 @@ use prusti_rustc_interface::{
     },
     trait_selection::{
         infer::{InferCtxtExt, TyCtxtInferExt},
-        traits::{ImplSource, Obligation, ObligationCause, SelectionContext},
+        traits::{
+            query::evaluate_obligation::InferCtxtExt as QueryInferCtxtExt, ImplSource, Obligation,
+            ObligationCause, SelectionContext,
+        },
     },
 };
 use sealed::{IntoParam, IntoParamTcx};
@@ -270,23 +272,22 @@ impl<'tcx> EnvQuery<'tcx> {
         let proc_def_id = proc_def_id.into_param();
         if let Some(trait_id) = self.get_trait_of_item(proc_def_id) {
             debug!("Fetching implementations of method '{:?}' defined in trait '{}' with substs '{:?}'", proc_def_id, self.tcx.def_path_str(trait_id), substs);
-            let result = self.tcx.infer_ctxt().enter(|infcx| {
-                let mut sc = SelectionContext::new(&infcx);
-                let obligation = Obligation::new(
-                    ObligationCause::dummy(),
-                    // TODO(tymap): don't use reveal_all
-                    ParamEnv::reveal_all(),
-                    Binder::dummy(TraitPredicate {
-                        trait_ref: TraitRef {
-                            def_id: trait_id,
-                            substs,
-                        },
-                        constness: BoundConstness::NotConst,
-                        polarity: ImplPolarity::Positive,
-                    }),
-                );
-                sc.select(&obligation)
-            });
+            let infcx = self.tcx.infer_ctxt().build();
+            let mut sc = SelectionContext::new(&infcx);
+            let obligation = Obligation::new(
+                ObligationCause::dummy(),
+                // TODO(tymap): don't use reveal_all
+                ParamEnv::reveal_all(),
+                Binder::dummy(TraitPredicate {
+                    trait_ref: TraitRef {
+                        def_id: trait_id,
+                        substs,
+                    },
+                    constness: BoundConstness::NotConst,
+                    polarity: ImplPolarity::Positive,
+                }),
+            );
+            let result = sc.select(&obligation);
             match result {
                 Ok(Some(ImplSource::UserDefined(data))) => {
                     for item in self
@@ -384,21 +385,20 @@ impl<'tcx> EnvQuery<'tcx> {
         param_env: impl IntoParamTcx<'tcx, ParamEnv<'tcx>>,
     ) -> bool {
         assert!(self.tcx.is_trait(trait_def_id));
-        self.tcx.infer_ctxt().enter(|infcx| {
-            // If `ty` has any inference variables (e.g. a region variable), then using it with
-            // 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(
-                    trait_def_id,
-                    fresh_ty,
-                    trait_substs,
-                    param_env.into_param(self.tcx),
-                )
-                .must_apply_considering_regions()
-        })
+        let infcx = self.tcx.infer_ctxt().build();
+        // If `ty` has any inference variables (e.g. a region variable), then using it with
+        // 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(
+                trait_def_id,
+                fresh_ty,
+                trait_substs,
+                param_env.into_param(self.tcx),
+            )
+            .must_apply_considering_regions()
     }
 
     /// Return the default substitutions for a particular item, i.e. where each
@@ -419,7 +419,6 @@ impl<'tcx> EnvQuery<'tcx> {
         param_env: impl IntoParamTcx<'tcx, ParamEnv<'tcx>>,
     ) -> bool {
         debug!("Evaluating predicate {:?}", predicate);
-        use prusti_rustc_interface::trait_selection::traits::query::evaluate_obligation::InferCtxtExt;
 
         let obligation = Obligation::new(
             ObligationCause::dummy(),
@@ -429,7 +428,8 @@ impl<'tcx> EnvQuery<'tcx> {
 
         self.tcx
             .infer_ctxt()
-            .enter(|infcx| infcx.predicate_must_hold_considering_regions(&obligation))
+            .build()
+            .predicate_must_hold_considering_regions(&obligation)
     }
 
     /// Normalizes associated types in foldable types,
@@ -466,7 +466,7 @@ impl<'tcx> EnvQuery<'tcx> {
 
 mod sealed {
     use prusti_rustc_interface::{
-        hir::hir_id::HirId,
+        hir::hir_id::{HirId, OwnerId},
         middle::ty::{ParamEnv, TyCtxt},
         span::def_id::{DefId, LocalDefId},
     };
@@ -492,6 +492,18 @@ mod sealed {
             self.to_def_id()
         }
     }
+    impl IntoParam<DefId> for OwnerId {
+        #[inline(always)]
+        fn into_param(self) -> DefId {
+            self.to_def_id()
+        }
+    }
+    impl IntoParam<LocalDefId> for OwnerId {
+        #[inline(always)]
+        fn into_param(self) -> LocalDefId {
+            self.def_id
+        }
+    }
 
     pub trait IntoParamTcx<'tcx, P> {
         fn into_param(self, tcx: TyCtxt<'tcx>) -> P;
@@ -502,6 +514,12 @@ mod sealed {
             self.into_param()
         }
     }
+    impl<'tcx> IntoParamTcx<'tcx, HirId> for OwnerId {
+        #[inline(always)]
+        fn into_param(self, tcx: TyCtxt<'tcx>) -> HirId {
+            tcx.hir().local_def_id_to_hir_id(self.def_id)
+        }
+    }
     impl<'tcx> IntoParamTcx<'tcx, HirId> for LocalDefId {
         #[inline(always)]
         fn into_param(self, tcx: TyCtxt<'tcx>) -> HirId {

prusti-interface/src/environment/traits/rustc_codegen.rs

@@ -57,62 +57,61 @@ pub(super) fn codegen_fulfill_obligation<'tcx>(
 
     // Do the initial selection for the obligation. This yields the
     // shallow result we are looking for -- that is, what specific impl.
-    tcx.infer_ctxt().enter(|infcx| {
-        let mut selcx = SelectionContext::new(&infcx);
+    let infcx = tcx.infer_ctxt().build();
+    let mut selcx = SelectionContext::new(&infcx);
 
-        let obligation_cause = ObligationCause::dummy();
-        let obligation = Obligation::new(
-            obligation_cause,
-            param_env,
-            trait_ref.to_poly_trait_predicate(),
-        );
+    let obligation_cause = ObligationCause::dummy();
+    let obligation = Obligation::new(
+        obligation_cause,
+        param_env,
+        trait_ref.to_poly_trait_predicate(),
+    );
 
-        let selection = match selcx.select(&obligation) {
-            Ok(Some(selection)) => selection,
-            Ok(None) => return Err(CodegenObligationError::Ambiguity),
-            Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented),
-            Err(e) => {
-                panic!(
-                    "Encountered error `{:?}` selecting `{:?}` during codegen",
-                    e, trait_ref
-                )
-            }
-        };
+    let selection = match selcx.select(&obligation) {
+        Ok(Some(selection)) => selection,
+        Ok(None) => return Err(CodegenObligationError::Ambiguity),
+        Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented),
+        Err(e) => {
+            panic!(
+                "Encountered error `{:?}` selecting `{:?}` during codegen",
+                e, trait_ref
+            )
+        }
+    };
 
-        debug!("fulfill_obligation: selection={:?}", selection);
+    debug!("fulfill_obligation: selection={:?}", selection);
 
-        // Currently, we use a fulfillment context to completely resolve
-        // all nested obligations. This is because they can inform the
-        // inference of the impl's type parameters.
-        let mut fulfill_cx = FulfillmentContext::new();
-        let impl_source = selection.map(|predicate| {
-            debug!(
-                "fulfill_obligation: register_predicate_obligation {:?}",
-                predicate
-            );
-            fulfill_cx.register_predicate_obligation(&infcx, predicate);
-        });
+    // Currently, we use a fulfillment context to completely resolve
+    // all nested obligations. This is because they can inform the
+    // inference of the impl's type parameters.
+    let mut fulfill_cx = FulfillmentContext::new();
+    let impl_source = selection.map(|predicate| {
+        debug!(
+            "fulfill_obligation: register_predicate_obligation {:?}",
+            predicate
+        );
+        fulfill_cx.register_predicate_obligation(&infcx, predicate);
+    });
 
-        // In principle, we only need to do this so long as `impl_source`
-        // contains unbound type parameters. It could be a slight
-        // optimization to stop iterating early.
-        let errors = fulfill_cx.select_all_or_error(&infcx);
-        if !errors.is_empty() {
-            return Err(CodegenObligationError::FulfillmentError);
-        }
+    // In principle, we only need to do this so long as `impl_source`
+    // contains unbound type parameters. It could be a slight
+    // optimization to stop iterating early.
+    let errors = fulfill_cx.select_all_or_error(&infcx);
+    if !errors.is_empty() {
+        return Err(CodegenObligationError::FulfillmentError);
+    }
 
-        let impl_source = infcx.resolve_vars_if_possible(impl_source);
-        let impl_source = infcx.tcx.erase_regions(impl_source);
+    let impl_source = infcx.resolve_vars_if_possible(impl_source);
+    let impl_source = infcx.tcx.erase_regions(impl_source);
 
-        // Opaque types may have gotten their hidden types constrained, but we can ignore them safely
-        // as they will get constrained elsewhere, too.
-        let _opaque_types = infcx
-            .inner
-            .borrow_mut()
-            .opaque_type_storage
-            .take_opaque_types();
+    // Opaque types may have gotten their hidden types constrained, but we can ignore them safely
+    // as they will get constrained elsewhere, too.
+    let _opaque_types = infcx
+        .inner
+        .borrow_mut()
+        .opaque_type_storage
+        .take_opaque_types();
 
-        debug!("Cache miss: {trait_ref:?} => {impl_source:?}");
-        Ok(&*tcx.arena.alloc(impl_source))
-    })
+    debug!("Cache miss: {trait_ref:?} => {impl_source:?}");
+    Ok(&*tcx.arena.alloc(impl_source))
 }