From e1caf6f54b6cdaa53c81663e0e76a0fa93563f59 Mon Sep 17 00:00:00 2001 From: Florian Groult Date: Mon, 26 Jun 2023 15:45:26 +0200 Subject: [PATCH] 1/3 Updating for nightly-2023-06-25 Patches: * https://github.com/rust-lang/rust/pull/112119 * https://github.com/rust-lang/rust/pull/108293 (partially) * https://github.com/rust-lang/rust/pull/112786 * https://github.com/rust-lang/rust/pull/112060 * https://github.com/rust-lang/rust/pull/112163 * https://github.com/rust-lang/rust/pull/112238 * https://github.com/rust-lang/rust/pull/112165 --- ci/rust-toolchain | 4 ++-- creusot-contracts-proc/src/invariant.rs | 2 +- creusot-contracts-proc/src/lib.rs | 2 +- creusot/src/analysis.rs | 1 - creusot/src/analysis/frozen_locals.rs | 10 +++++----- creusot/src/analysis/init_locals.rs | 9 ++++----- creusot/src/analysis/liveness_no_drop.rs | 9 ++++----- creusot/src/analysis/uninit_locals.rs | 9 ++++----- creusot/src/backend/dependency.rs | 4 ++-- creusot/src/backend/term.rs | 2 +- creusot/src/ctx.rs | 4 +++- creusot/src/lib.rs | 2 +- creusot/src/translation/external.rs | 2 +- creusot/src/translation/function.rs | 2 +- creusot/src/translation/function/statement.rs | 2 +- creusot/src/translation/function/terminator.rs | 2 +- creusot/src/translation/pearlite.rs | 10 +++++----- creusot/src/translation/specification.rs | 2 +- creusot/src/translation/traits.rs | 6 +++--- creusot/src/util.rs | 4 ++-- creusot/src/validate.rs | 2 +- 21 files changed, 44 insertions(+), 46 deletions(-) diff --git a/ci/rust-toolchain b/ci/rust-toolchain index 48005cc8f4..94ee6fc908 100644 --- 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 index f0db246361..caf6e5a8c4 100644 --- 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) -> Vec { 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 index ac336a291a..8bc3a1e0de 100644 --- 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 index 80f02e2f32..54948199ee 100644 --- a/creusot/src/analysis.rs +++ b/creusot/src/analysis.rs @@ -111,7 +111,6 @@ pub(crate) fn categorize(context: PlaceContext) -> Option { 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 index 076dd73d5e..14aed01404 100644 --- a/creusot/src/analysis/frozen_locals.rs +++ b/creusot/src/analysis/frozen_locals.rs @@ -121,7 +121,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> { type Idx = BorrowIndex; fn before_statement_effect( - &self, + &mut self, _trans: &mut impl GenKill, _statement: &mir::Statement<'tcx>, _location: Location, @@ -129,7 +129,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> { } fn statement_effect( - &self, + &mut self, trans: &mut impl GenKill, stmt: &mir::Statement<'tcx>, location: Location, @@ -184,7 +184,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> { } fn before_terminator_effect( - &self, + &mut self, _trans: &mut impl GenKill, _terminator: &mir::Terminator<'tcx>, _location: Location, @@ -192,7 +192,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> { } fn terminator_effect( - &self, + &mut self, trans: &mut impl GenKill, 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, _block: mir::BasicBlock, _return_places: dataflow::CallReturnPlaces<'_, 'tcx>, diff --git a/creusot/src/analysis/init_locals.rs b/creusot/src/analysis/init_locals.rs index e0d7618322..8f79b4733d 100644 --- 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, 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, 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, _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, _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 index a8806e159d..46765f7d5e 100644 --- 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, 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, 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, _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, _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 index 02b6a462a2..89b3a4dcb1 100644 --- 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, 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, 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, _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, _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 index 6b1165bd30..046966ca26 100644 --- 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 index 25f88d067a..c2b389395d 100644 --- 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 { 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 index 8dbfdb0ef9..a295bbb174 100644 --- 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 index 707c90b5ea..f68eaaf7ba 100644 --- 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 index 236152bc12..41be34020d 100644 --- 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> { - 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 index 243e545275..cc2f5613ec 100644 --- 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 index 45e8ffbd2e..4b80eb6db7 100644 --- 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 index 1244df94fd..3b9af0f756 100644 --- 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>> { - let mut fulfill_cx = >::new(infcx.tcx); + let mut fulfill_cx = >::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 index 72aa95f8ed..0d00fe5d72 100644 --- 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 index b972a020d6..cc7c8f1786 100644 --- 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 + '_ { diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index ef83a23063..81dad04e62 100644 --- 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 index 88e344fce4..7fa1595130 100644 --- 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 index 35c2ec5fed..e01c00e888 100644 --- 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())