Skip to content

Commit e1caf6f

Browse files
floriangrufloriangru
committed
1/3 Updating for nightly-2023-06-25
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
1 parent ee50ea2 commit e1caf6f

21 files changed

+44
-46
lines changed

‎ci/rust-toolchain

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
[toolchain]
2-
channel = "nightly-2023-05-26"
3-
components = [ "rustfmt", "rustc-dev", "llvm-tools-preview" ]
2+
channel = "nightly-2023-06-25"
3+
components = [ "rustfmt", "rustc-dev", "llvm-tools" ]

‎creusot-contracts-proc/src/invariant.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ pub struct Loop {
5656

5757
fn filter_invariants(attrs: &mut Vec<Attribute>) -> Vec<Attribute> {
5858
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))
6060
.collect()
6161
}
6262

‎creusot-contracts-proc/src/lib.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff 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)]
22
extern crate proc_macro;
33
use extern_spec::ExternSpecs;
44
use pearlite_syn::*;

‎creusot/src/analysis.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,6 @@ pub(crate) fn categorize(context: PlaceContext) -> Option<DefUse> {
111111
PlaceContext::MutatingUse(MutatingUseContext::Borrow) |
112112
PlaceContext::NonMutatingUse(NonMutatingUseContext::SharedBorrow) |
113113
PlaceContext::NonMutatingUse(NonMutatingUseContext::ShallowBorrow) |
114-
PlaceContext::NonMutatingUse(NonMutatingUseContext::UniqueBorrow) |
115114
PlaceContext::NonMutatingUse(NonMutatingUseContext::PlaceMention) |
116115
PlaceContext::MutatingUse(MutatingUseContext::AddressOf) |
117116
PlaceContext::NonMutatingUse(NonMutatingUseContext::AddressOf) |

‎creusot/src/analysis/frozen_locals.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -121,15 +121,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
121121
type Idx = BorrowIndex;
122122

123123
fn before_statement_effect(
124-
&self,
124+
&mut self,
125125
_trans: &mut impl GenKill<Self::Idx>,
126126
_statement: &mir::Statement<'tcx>,
127127
_location: Location,
128128
) {
129129
}
130130

131131
fn statement_effect(
132-
&self,
132+
&mut self,
133133
trans: &mut impl GenKill<Self::Idx>,
134134
stmt: &mir::Statement<'tcx>,
135135
location: Location,
@@ -184,15 +184,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
184184
}
185185

186186
fn before_terminator_effect(
187-
&self,
187+
&mut self,
188188
_trans: &mut impl GenKill<Self::Idx>,
189189
_terminator: &mir::Terminator<'tcx>,
190190
_location: Location,
191191
) {
192192
}
193193

194194
fn terminator_effect(
195-
&self,
195+
&mut self,
196196
trans: &mut impl GenKill<Self::Idx>,
197197
terminator: &mir::Terminator<'tcx>,
198198
location: Location,
@@ -211,7 +211,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
211211
}
212212

213213
fn call_return_effect(
214-
&self,
214+
&mut self,
215215
_trans: &mut impl GenKill<Self::Idx>,
216216
_block: mir::BasicBlock,
217217
_return_places: dataflow::CallReturnPlaces<'_, 'tcx>,

‎creusot/src/analysis/init_locals.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
3434
type Idx = Local;
3535

3636
fn statement_effect(
37-
&self,
37+
&mut self,
3838
trans: &mut impl GenKill<Self::Idx>,
3939
statement: &mir::Statement<'tcx>,
4040
loc: Location,
@@ -43,7 +43,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
4343
}
4444

4545
fn terminator_effect(
46-
&self,
46+
&mut self,
4747
trans: &mut impl GenKill<Self::Idx>,
4848
terminator: &Terminator<'tcx>,
4949
loc: Location,
@@ -52,7 +52,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
5252
}
5353

5454
fn call_return_effect(
55-
&self,
55+
&mut self,
5656
trans: &mut impl GenKill<Self::Idx>,
5757
_block: BasicBlock,
5858
return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -62,7 +62,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
6262

6363
/// See `Analysis::apply_yield_resume_effect`.
6464
fn yield_resume_effect(
65-
&self,
65+
&mut self,
6666
trans: &mut impl GenKill<Self::Idx>,
6767
_resume_block: BasicBlock,
6868
resume_place: mir::Place<'tcx>,
@@ -114,7 +114,6 @@ where
114114
| NonMutatingUseContext::Copy
115115
| NonMutatingUseContext::SharedBorrow
116116
| NonMutatingUseContext::ShallowBorrow
117-
| NonMutatingUseContext::UniqueBorrow
118117
| NonMutatingUseContext::AddressOf
119118
| NonMutatingUseContext::PlaceMention
120119
| NonMutatingUseContext::Projection,

‎creusot/src/analysis/liveness_no_drop.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
3535
type Idx = Local;
3636

3737
fn statement_effect(
38-
&self,
38+
&mut self,
3939
trans: &mut impl GenKill<Self::Idx>,
4040
statement: &mir::Statement<'tcx>,
4141
location: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
4444
}
4545

4646
fn terminator_effect(
47-
&self,
47+
&mut self,
4848
trans: &mut impl GenKill<Self::Idx>,
4949
terminator: &mir::Terminator<'tcx>,
5050
location: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
5353
}
5454

5555
fn call_return_effect(
56-
&self,
56+
&mut self,
5757
trans: &mut impl GenKill<Self::Idx>,
5858
_block: mir::BasicBlock,
5959
return_places: CallReturnPlaces<'_, 'tcx>,
@@ -66,7 +66,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
6666
}
6767

6868
fn yield_resume_effect(
69-
&self,
69+
&mut self,
7070
trans: &mut impl GenKill<Self::Idx>,
7171
_resume_block: mir::BasicBlock,
7272
resume_place: mir::Place<'tcx>,
@@ -197,7 +197,6 @@ impl DefUse {
197197
| NonMutatingUseContext::ShallowBorrow
198198
| NonMutatingUseContext::SharedBorrow
199199
| NonMutatingUseContext::PlaceMention
200-
| NonMutatingUseContext::UniqueBorrow,
201200
) => Some(DefUse::Use),
202201
PlaceContext::MutatingUse(MutatingUseContext::Drop) => None,
203202

‎creusot/src/analysis/uninit_locals.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
3535
type Idx = Local;
3636

3737
fn statement_effect(
38-
&self,
38+
&mut self,
3939
trans: &mut impl GenKill<Self::Idx>,
4040
statement: &mir::Statement<'tcx>,
4141
loc: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
4444
}
4545

4646
fn terminator_effect(
47-
&self,
47+
&mut self,
4848
trans: &mut impl GenKill<Self::Idx>,
4949
terminator: &Terminator<'tcx>,
5050
loc: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
5353
}
5454

5555
fn call_return_effect(
56-
&self,
56+
&mut self,
5757
trans: &mut impl GenKill<Self::Idx>,
5858
_block: BasicBlock,
5959
return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -67,7 +67,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
6767

6868
/// See `Analysis::apply_yield_resume_effect`.
6969
fn yield_resume_effect(
70-
&self,
70+
&mut self,
7171
trans: &mut impl GenKill<Self::Idx>,
7272
_resume_block: BasicBlock,
7373
resume_place: mir::Place<'tcx>,
@@ -112,7 +112,6 @@ where
112112
| NonMutatingUseContext::Copy
113113
| NonMutatingUseContext::SharedBorrow
114114
| NonMutatingUseContext::ShallowBorrow
115-
| NonMutatingUseContext::UniqueBorrow
116115
| NonMutatingUseContext::AddressOf
117116
| NonMutatingUseContext::PlaceMention
118117
| NonMutatingUseContext::Projection,

‎creusot/src/backend/dependency.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -109,9 +109,9 @@ impl<'tcx> Dependency<'tcx> {
109109
};
110110

111111
match &mut self {
112-
Dependency::Item(_, s) => *s = EarlyBinder(*s).subst(tcx, substs),
112+
Dependency::Item(_, s) => *s = EarlyBinder::bind(*s).subst(tcx, substs),
113113
Dependency::Type(ty) | Dependency::TyInv(ty) => {
114-
*ty = EarlyBinder(*ty).subst(tcx, substs)
114+
*ty = EarlyBinder::bind(*ty).subst(tcx, substs)
115115
}
116116
};
117117
self

‎creusot/src/backend/term.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -414,7 +414,7 @@ pub(super) fn mk_binders(func: Exp, args: Vec<Exp>) -> Exp {
414414
fn is_identity_from<'tcx>(tcx: TyCtxt<'tcx>, id: DefId, subst: SubstsRef<'tcx>) -> bool {
415415
if tcx.def_path_str(id) == "std::convert::From::from" && subst.len() == 1 {
416416
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);
418418
}
419419
false
420420
}

‎creusot/src/ctx.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -347,7 +347,9 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
347347
for pred in es.predicates_for(self.tcx, subst) {
348348
let obligation_cause = ObligationCause::dummy();
349349
let obligation = Obligation::new(self.tcx, obligation_cause, param_env, pred);
350-
if !selcx.predicate_may_hold_fatal(&obligation) {
350+
if selcx.evaluate_root_obligation(&obligation).map_or(
351+
false, // Overflow has occurred, and treat the obligation as possibly holding.
352+
|result| !result.may_apply()) {
351353
additional_predicates.push(
352354
self.tcx.try_normalize_erasing_regions(base_env, pred).unwrap_or(pred),
353355
)

‎creusot/src/lib.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
#![feature(rustc_private, register_tool)]
2-
#![feature(box_patterns, control_flow_enum, drain_filter)]
2+
#![feature(box_patterns, control_flow_enum, extract_if)]
33
#![feature(let_chains, never_type, try_blocks)]
44

55
#[macro_use]

‎creusot/src/translation/external.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ impl<'tcx> ExternSpec<'tcx> {
3131
tcx: TyCtxt<'tcx>,
3232
sub: SubstsRef<'tcx>,
3333
) -> Vec<Predicate<'tcx>> {
34-
EarlyBinder(self.additional_predicates.clone()).subst(tcx, sub)
34+
EarlyBinder::bind(self.additional_predicates.clone()).subst(tcx, sub)
3535
}
3636
}
3737

‎creusot/src/translation/function.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -547,7 +547,7 @@ pub(crate) fn closure_contract<'tcx>(
547547

548548
normalize(ctx.tcx, ctx.param_env(def_id), &mut postcondition);
549549

550-
let unnest_sig = EarlyBinder(ctx.sig(unnest_id).clone()).subst(ctx.tcx, unnest_subst);
550+
let unnest_sig = EarlyBinder::bind(ctx.sig(unnest_id).clone()).subst(ctx.tcx, unnest_subst);
551551

552552
let mut unnest = closure_unnest(ctx.tcx, def_id, subst);
553553
normalize(ctx.tcx, ctx.param_env(def_id), &mut unnest);

‎creusot/src/translation/function/statement.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
7575
}
7676
},
7777
Rvalue::Ref(_, ss, pl) => match ss {
78-
Shared | Shallow | Unique => {
78+
Shared | Shallow => {
7979
if self.erased_locals.contains(pl.local) {
8080
return;
8181
}

‎creusot/src/translation/function/terminator.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,7 @@ pub(crate) fn evaluate_additional_predicates<'tcx>(
230230
param_env: ParamEnv<'tcx>,
231231
sp: Span,
232232
) -> Result<(), Vec<FulfillmentError<'tcx>>> {
233-
let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx.tcx);
233+
let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx);
234234
for predicate in p {
235235
let predicate = infcx.tcx.erase_regions(predicate);
236236
let cause = ObligationCause::dummy_with_span(sp);

‎creusot/src/translation/pearlite.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -295,9 +295,9 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
295295

296296
use rustc_middle::mir;
297297
let op = match op {
298-
mir::BinOp::Add => BinOp::Add,
299-
mir::BinOp::Sub => BinOp::Sub,
300-
mir::BinOp::Mul => BinOp::Mul,
298+
mir::BinOp::Add | mir::BinOp::AddUnchecked => BinOp::Add,
299+
mir::BinOp::Sub | mir::BinOp::SubUnchecked => BinOp::Sub,
300+
mir::BinOp::Mul | mir::BinOp::MulUnchecked => BinOp::Mul,
301301
mir::BinOp::Div => BinOp::Div,
302302
mir::BinOp::Rem => BinOp::Rem,
303303
mir::BinOp::BitXor => {
@@ -309,10 +309,10 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
309309
mir::BinOp::BitOr => {
310310
return Err(Error::new(self.thir[expr].span, "unsupported operation"))
311311
}
312-
mir::BinOp::Shl => {
312+
mir::BinOp::Shl | mir::BinOp::ShlUnchecked => {
313313
return Err(Error::new(self.thir[expr].span, "unsupported operation"))
314314
}
315-
mir::BinOp::Shr => {
315+
mir::BinOp::Shr | mir::BinOp::ShrUnchecked=> {
316316
return Err(Error::new(self.thir[expr].span, "unsupported operation"))
317317
}
318318
mir::BinOp::Lt => BinOp::Lt,

‎creusot/src/translation/specification.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ impl ContractClauses {
103103
let term = ctx.term(var_id).unwrap().clone();
104104
out.variant = Some(term);
105105
};
106-
EarlyBinder(out)
106+
EarlyBinder::bind(out)
107107
}
108108

109109
pub(crate) fn iter_ids(&self) -> impl Iterator<Item = DefId> + '_ {

‎creusot/src/translation/traits.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ impl<'tcx> TranslationCtx<'tcx> {
7777

7878
let subst = InternalSubsts::identity_for_item(self.tcx, impl_item);
7979

80-
let refn_subst = subst.rebase_onto(self.tcx, impl_id, trait_ref.0.substs);
80+
let refn_subst = subst.rebase_onto(self.tcx, impl_id, trait_ref.skip_binder().substs);
8181

8282
// TODO: Clean up and abstract
8383
let predicates = self
@@ -121,7 +121,7 @@ fn logic_refinement_term<'tcx>(
121121
let trait_sig = {
122122
let pre_sig = ctx.sig(trait_item_id).clone();
123123
let param_env = ctx.param_env(impl_item_id);
124-
EarlyBinder(pre_sig).subst(ctx.tcx, refn_subst).normalize(ctx.tcx, param_env)
124+
EarlyBinder::bind(pre_sig).subst(ctx.tcx, refn_subst).normalize(ctx.tcx, param_env)
125125
};
126126

127127
let impl_sig = ctx.sig(impl_item_id).clone();
@@ -335,7 +335,7 @@ pub(crate) fn still_specializable<'tcx>(
335335
let trait_generics = substs.truncate_to(tcx, tcx.generics_of(trait_id));
336336
!is_final && trait_generics.still_further_specializable()
337337
} else if let Some(impl_id) = tcx.impl_of_method(def_id) && tcx.trait_id_of_impl(impl_id).is_some() {
338-
let is_final = tcx.impl_defaultness(def_id).is_final();
338+
let is_final = tcx.defaultness(def_id).is_final();
339339
let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
340340
!is_final && trait_ref.subst(tcx, substs).still_further_specializable()
341341
} else {

‎creusot/src/util.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,7 @@ fn elaborate_type_invariants<'tcx>(
484484
}
485485

486486
if let Some(term) = pearlite::type_invariant_term(ctx, def_id, *name, *span, *ty) {
487-
let term = EarlyBinder(term).subst(ctx.tcx, subst);
487+
let term = EarlyBinder::bind(term).subst(ctx.tcx, subst);
488488

489489
if ty.is_mutable_ptr() {
490490
let inner = ty.builtin_deref(true).unwrap().ty;
@@ -509,7 +509,7 @@ fn elaborate_type_invariants<'tcx>(
509509
ret_ty_span.unwrap_or_else(|| ctx.tcx.def_span(def_id)),
510510
pre_sig.output,
511511
) {
512-
let term = EarlyBinder(term).subst(ctx.tcx, subst);
512+
let term = EarlyBinder::bind(term).subst(ctx.tcx, subst);
513513
pre_sig.contract.ensures.push(term);
514514
}
515515
}

‎creusot/src/validate.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ pub(crate) fn validate_impls(ctx: &TranslationCtx) {
103103
continue;
104104
}
105105

106-
let trait_ref = ctx.impl_trait_ref(*impl_id).unwrap().0;
106+
let trait_ref = ctx.impl_trait_ref(*impl_id).unwrap().skip_binder();
107107

108108
if util::is_trusted(ctx.tcx, trait_ref.def_id)
109109
!= util::is_trusted(ctx.tcx, impl_id.to_def_id())

0 commit comments

Comments
 (0)