1/3 Updating for nightly-2023-06-25

floriangru · floriangru · commit e1caf6f54b6c · 2023-06-26T15:45:26.000+02:00
Patches: * rust-lang/rust#112119 * rust-lang/rust#108293 (partially) * rust-lang/rust#112786 * rust-lang/rust#112060 * rust-lang/rust#112163 * rust-lang/rust#112238 * rust-lang/rust#112165
diff --git a/ci/rust-toolchain b/ci/rust-toolchain
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-05-26"
-components = [ "rustfmt", "rustc-dev", "llvm-tools-preview" ]
+channel = "nightly-2023-06-25"
+components = [ "rustfmt", "rustc-dev", "llvm-tools" ]
diff --git a/creusot-contracts-proc/src/invariant.rs b/creusot-contracts-proc/src/invariant.rs
@@ -56,7 +56,7 @@ pub struct Loop {
 
 fn filter_invariants(attrs: &mut Vec<Attribute>) -> Vec<Attribute> {
     attrs
-        .drain_filter(|attr| attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false))
+        .extract_if(|attr| attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false))
         .collect()
 }
 
diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs
@@ -1,4 +1,4 @@
-#![feature(box_patterns, drain_filter, extend_one, proc_macro_def_site)]
+#![feature(box_patterns, extract_if, extend_one, proc_macro_def_site)]
 extern crate proc_macro;
 use extern_spec::ExternSpecs;
 use pearlite_syn::*;
diff --git a/creusot/src/analysis.rs b/creusot/src/analysis.rs
@@ -111,7 +111,6 @@ pub(crate) fn categorize(context: PlaceContext) -> Option<DefUse> {
         PlaceContext::MutatingUse(MutatingUseContext::Borrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::SharedBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::ShallowBorrow) |
-        PlaceContext::NonMutatingUse(NonMutatingUseContext::UniqueBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::PlaceMention) |
         PlaceContext::MutatingUse(MutatingUseContext::AddressOf) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::AddressOf) |
diff --git a/creusot/src/analysis/frozen_locals.rs b/creusot/src/analysis/frozen_locals.rs
@@ -121,15 +121,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     type Idx = BorrowIndex;
 
     fn before_statement_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _statement: &mir::Statement<'tcx>,
         _location: Location,
     ) {
     }
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         stmt: &mir::Statement<'tcx>,
         location: Location,
@@ -184,15 +184,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     }
 
     fn before_terminator_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _terminator: &mir::Terminator<'tcx>,
         _location: Location,
     ) {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
@@ -211,7 +211,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _block: mir::BasicBlock,
         _return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
diff --git a/creusot/src/analysis/init_locals.rs b/creusot/src/analysis/init_locals.rs
@@ -34,7 +34,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         loc: Location,
@@ -43,7 +43,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &Terminator<'tcx>,
         loc: Location,
@@ -52,7 +52,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: BasicBlock,
         return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -62,7 +62,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
 
     /// See `Analysis::apply_yield_resume_effect`.
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -114,7 +114,6 @@ where
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::ShallowBorrow
-                | NonMutatingUseContext::UniqueBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,
diff --git a/creusot/src/analysis/liveness_no_drop.rs b/creusot/src/analysis/liveness_no_drop.rs
@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         location: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: mir::BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
@@ -66,7 +66,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: mir::BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -197,7 +197,6 @@ impl DefUse {
                 | NonMutatingUseContext::ShallowBorrow
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::PlaceMention
-                | NonMutatingUseContext::UniqueBorrow,
             ) => Some(DefUse::Use),
             PlaceContext::MutatingUse(MutatingUseContext::Drop) => None,
 
diff --git a/creusot/src/analysis/uninit_locals.rs b/creusot/src/analysis/uninit_locals.rs
@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         loc: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &Terminator<'tcx>,
         loc: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: BasicBlock,
         return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -67,7 +67,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
 
     /// See `Analysis::apply_yield_resume_effect`.
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -112,7 +112,6 @@ where
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::ShallowBorrow
-                | NonMutatingUseContext::UniqueBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,
diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs
@@ -109,9 +109,9 @@ impl<'tcx> Dependency<'tcx> {
         };
 
         match &mut self {
-            Dependency::Item(_, s) => *s = EarlyBinder(*s).subst(tcx, substs),
+            Dependency::Item(_, s) => *s = EarlyBinder::bind(*s).subst(tcx, substs),
             Dependency::Type(ty) | Dependency::TyInv(ty) => {
-                *ty = EarlyBinder(*ty).subst(tcx, substs)
+                *ty = EarlyBinder::bind(*ty).subst(tcx, substs)
             }
         };
         self
diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
@@ -414,7 +414,7 @@ pub(super) fn mk_binders(func: Exp, args: Vec<Exp>) -> Exp {
 fn is_identity_from<'tcx>(tcx: TyCtxt<'tcx>, id: DefId, subst: SubstsRef<'tcx>) -> bool {
     if tcx.def_path_str(id) == "std::convert::From::from" && subst.len() == 1 {
         let out_ty: Ty<'tcx> = tcx.fn_sig(id).no_bound_vars().unwrap().output().skip_binder();
-        return subst[0].expect_ty() == EarlyBinder(out_ty).subst(tcx, subst);
+        return subst[0].expect_ty() == EarlyBinder::bind(out_ty).subst(tcx, subst);
     }
     false
 }
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
@@ -347,7 +347,9 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
                 for pred in es.predicates_for(self.tcx, subst) {
                     let obligation_cause = ObligationCause::dummy();
                     let obligation = Obligation::new(self.tcx, obligation_cause, param_env, pred);
-                    if !selcx.predicate_may_hold_fatal(&obligation) {
+                    if selcx.evaluate_root_obligation(&obligation).map_or(
+                        false, // Overflow has occurred, and treat the obligation as possibly holding.
+                        |result| !result.may_apply()) {
                         additional_predicates.push(
                             self.tcx.try_normalize_erasing_regions(base_env, pred).unwrap_or(pred),
                         )
diff --git a/creusot/src/lib.rs b/creusot/src/lib.rs
@@ -1,5 +1,5 @@
 #![feature(rustc_private, register_tool)]
-#![feature(box_patterns, control_flow_enum, drain_filter)]
+#![feature(box_patterns, control_flow_enum, extract_if)]
 #![feature(let_chains, never_type, try_blocks)]
 
 #[macro_use]
diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs
@@ -31,7 +31,7 @@ impl<'tcx> ExternSpec<'tcx> {
         tcx: TyCtxt<'tcx>,
         sub: SubstsRef<'tcx>,
     ) -> Vec<Predicate<'tcx>> {
-        EarlyBinder(self.additional_predicates.clone()).subst(tcx, sub)
+        EarlyBinder::bind(self.additional_predicates.clone()).subst(tcx, sub)
     }
 }
 
diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
@@ -547,7 +547,7 @@ pub(crate) fn closure_contract<'tcx>(
 
         normalize(ctx.tcx, ctx.param_env(def_id), &mut postcondition);
 
-        let unnest_sig = EarlyBinder(ctx.sig(unnest_id).clone()).subst(ctx.tcx, unnest_subst);
+        let unnest_sig = EarlyBinder::bind(ctx.sig(unnest_id).clone()).subst(ctx.tcx, unnest_subst);
 
         let mut unnest = closure_unnest(ctx.tcx, def_id, subst);
         normalize(ctx.tcx, ctx.param_env(def_id), &mut unnest);
diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs
@@ -75,7 +75,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 }
             },
             Rvalue::Ref(_, ss, pl) => match ss {
-                Shared | Shallow | Unique => {
+                Shared | Shallow => {
                     if self.erased_locals.contains(pl.local) {
                         return;
                     }
diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
@@ -230,7 +230,7 @@ pub(crate) fn evaluate_additional_predicates<'tcx>(
     param_env: ParamEnv<'tcx>,
     sp: Span,
 ) -> Result<(), Vec<FulfillmentError<'tcx>>> {
-    let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx.tcx);
+    let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx);
     for predicate in p {
         let predicate = infcx.tcx.erase_regions(predicate);
         let cause = ObligationCause::dummy_with_span(sp);
diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs
@@ -295,9 +295,9 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
 
                 use rustc_middle::mir;
                 let op = match op {
-                    mir::BinOp::Add => BinOp::Add,
-                    mir::BinOp::Sub => BinOp::Sub,
-                    mir::BinOp::Mul => BinOp::Mul,
+                    mir::BinOp::Add | mir::BinOp::AddUnchecked => BinOp::Add,
+                    mir::BinOp::Sub | mir::BinOp::SubUnchecked => BinOp::Sub,
+                    mir::BinOp::Mul | mir::BinOp::MulUnchecked => BinOp::Mul,
                     mir::BinOp::Div => BinOp::Div,
                     mir::BinOp::Rem => BinOp::Rem,
                     mir::BinOp::BitXor => {
@@ -309,10 +309,10 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                     mir::BinOp::BitOr => {
                         return Err(Error::new(self.thir[expr].span, "unsupported operation"))
                     }
-                    mir::BinOp::Shl => {
+                    mir::BinOp::Shl | mir::BinOp::ShlUnchecked => {
                         return Err(Error::new(self.thir[expr].span, "unsupported operation"))
                     }
-                    mir::BinOp::Shr => {
+                    mir::BinOp::Shr | mir::BinOp::ShrUnchecked=> {
                         return Err(Error::new(self.thir[expr].span, "unsupported operation"))
                     }
                     mir::BinOp::Lt => BinOp::Lt,
diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs
@@ -103,7 +103,7 @@ impl ContractClauses {
             let term = ctx.term(var_id).unwrap().clone();
             out.variant = Some(term);
         };
-        EarlyBinder(out)
+        EarlyBinder::bind(out)
     }
 
     pub(crate) fn iter_ids(&self) -> impl Iterator<Item = DefId> + '_ {
diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs
@@ -77,7 +77,7 @@ impl<'tcx> TranslationCtx<'tcx> {
 
             let subst = InternalSubsts::identity_for_item(self.tcx, impl_item);
 
-            let refn_subst = subst.rebase_onto(self.tcx, impl_id, trait_ref.0.substs);
+            let refn_subst = subst.rebase_onto(self.tcx, impl_id, trait_ref.skip_binder().substs);
 
             // TODO: Clean up and abstract
             let predicates = self
@@ -121,7 +121,7 @@ fn logic_refinement_term<'tcx>(
     let trait_sig = {
         let pre_sig = ctx.sig(trait_item_id).clone();
         let param_env = ctx.param_env(impl_item_id);
-        EarlyBinder(pre_sig).subst(ctx.tcx, refn_subst).normalize(ctx.tcx, param_env)
+        EarlyBinder::bind(pre_sig).subst(ctx.tcx, refn_subst).normalize(ctx.tcx, param_env)
     };
 
     let impl_sig = ctx.sig(impl_item_id).clone();
@@ -335,7 +335,7 @@ pub(crate) fn still_specializable<'tcx>(
         let trait_generics = substs.truncate_to(tcx, tcx.generics_of(trait_id));
         !is_final && trait_generics.still_further_specializable()
     } else if let Some(impl_id) = tcx.impl_of_method(def_id) && tcx.trait_id_of_impl(impl_id).is_some() {
-        let is_final = tcx.impl_defaultness(def_id).is_final();
+        let is_final = tcx.defaultness(def_id).is_final();
         let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
         !is_final && trait_ref.subst(tcx, substs).still_further_specializable()
     } else {
diff --git a/creusot/src/util.rs b/creusot/src/util.rs
@@ -484,7 +484,7 @@ fn elaborate_type_invariants<'tcx>(
         }
 
         if let Some(term) = pearlite::type_invariant_term(ctx, def_id, *name, *span, *ty) {
-            let term = EarlyBinder(term).subst(ctx.tcx, subst);
+            let term = EarlyBinder::bind(term).subst(ctx.tcx, subst);
 
             if ty.is_mutable_ptr() {
                 let inner = ty.builtin_deref(true).unwrap().ty;
@@ -509,7 +509,7 @@ fn elaborate_type_invariants<'tcx>(
         ret_ty_span.unwrap_or_else(|| ctx.tcx.def_span(def_id)),
         pre_sig.output,
     ) {
-        let term = EarlyBinder(term).subst(ctx.tcx, subst);
+        let term = EarlyBinder::bind(term).subst(ctx.tcx, subst);
         pre_sig.contract.ensures.push(term);
     }
 }
diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs
@@ -103,7 +103,7 @@ pub(crate) fn validate_impls(ctx: &TranslationCtx) {
             continue;
         }
 
-        let trait_ref = ctx.impl_trait_ref(*impl_id).unwrap().0;
+        let trait_ref = ctx.impl_trait_ref(*impl_id).unwrap().skip_binder();
 
         if util::is_trusted(ctx.tcx, trait_ref.def_id)
             != util::is_trusted(ctx.tcx, impl_id.to_def_id())

Original file line number	Diff line number	Diff line change
`@@ -56,7 +56,7 @@ pub struct Loop {`
`56`	`56`
`57`	`57`	`fn filter_invariants(attrs: &mut Vec<Attribute>) -> Vec<Attribute> {`
`58`	`58`	`attrs`
`59`		`- .drain_filter(\|attr\| attr.path().get_ident().map(\|i\| i == "invariant").unwrap_or(false))`
	`59`	`+ .extract_if(\|attr\| attr.path().get_ident().map(\|i\| i == "invariant").unwrap_or(false))`
`60`	`60`	`.collect()`
`61`	`61`	`}`
`62`	`62`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-#![feature(box_patterns, drain_filter, extend_one, proc_macro_def_site)]`
	`1`	`+#![feature(box_patterns, extract_if, extend_one, proc_macro_def_site)]`
`2`	`2`	`extern crate proc_macro;`
`3`	`3`	`use extern_spec::ExternSpecs;`
`4`	`4`	`use pearlite_syn::*;`
Original file line number	Diff line number	Diff line change
`@@ -414,7 +414,7 @@ pub(super) fn mk_binders(func: Exp, args: Vec<Exp>) -> Exp {`
`414`	`414`	`fn is_identity_from<'tcx>(tcx: TyCtxt<'tcx>, id: DefId, subst: SubstsRef<'tcx>) -> bool {`
`415`	`415`	`if tcx.def_path_str(id) == "std::convert::From::from" && subst.len() == 1 {`
`416`	`416`	`let out_ty: Ty<'tcx> = tcx.fn_sig(id).no_bound_vars().unwrap().output().skip_binder();`
`417`		`- return subst[0].expect_ty() == EarlyBinder(out_ty).subst(tcx, subst);`
	`417`	`+ return subst[0].expect_ty() == EarlyBinder::bind(out_ty).subst(tcx, subst);`
`418`	`418`	`}`
`419`	`419`	`false`
`420`	`420`	`}`