Skip to content

Update toolchain to nightly-2026-06-22 #2155

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jhjourdan merged 1 commit into from
Jun 22, 2026
Merged

Update toolchain to nightly-2026-06-22 #2155

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion creusot-metadata/src/encoder.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ use std::{

pub struct MetadataEncoder<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
pub opaque: FileEncoder,
pub opaque: FileEncoder<'a>,
type_shorthands: FxHashMap<Ty<'tcx>, usize>,
predicate_shorthands: FxHashMap<PredicateKind<'tcx>, usize>,
file_to_file_index: FxHashMap<*const SourceFile, SourceFileIndex>,
Expand Down
1 change: 0 additions & 1 deletion creusot-std/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,6 @@
range_bounds_is_empty,
bound_copied,
auto_traits,
new_range_api_legacy,
negative_impls,
exact_size_is_empty,
)
Expand Down
32 changes: 14 additions & 18 deletions creusot/src/analysis.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,26 +445,25 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
if self.body_specs.erased_locals.contains(pl.local) {
continue;
}
let ty = pl.ty(&self.body().local_decls, self.tcx());
let ty = self.tcx().normalize_erasing_regions(self.typing_env, Unnormalized::new(ty));
let tcx = self.tcx();
let ty = pl.ty(&self.body().local_decls, tcx);
let ty = tcx.normalize_erasing_regions(self.typing_env, Unnormalized::new(ty));
use TyKind::*;
match ty.ty.kind() {
Adt(adt_def, subst) => {
if adt_def.is_box() {
res_partial.push(All(self.tcx().mk_place_deref(pl)));
res_partial.push(All(tcx.mk_place_deref(pl)));
} else if adt_def.is_enum() {
if let Some(vid) = ty.variant_index {
let var = adt_def.variant(vid);
for (fi, fd) in var.fields.iter_enumerated() {
res_partial.push(All(self.tcx().mk_place_field(
pl,
fi,
fd.ty(self.tcx(), subst),
)));
let ty = tcx
.normalize_erasing_regions(self.typing_env, fd.ty(tcx, subst));
res_partial.push(All(tcx.mk_place_field(pl, fi, ty)));
}
} else {
for (i, _var) in adt_def.variants().iter().enumerate() {
res_partial.push(All(self.tcx().mk_place_downcast(
res_partial.push(All(tcx.mk_place_downcast(
pl,
*adt_def,
VariantIdx::new(i),
Expand All @@ -474,12 +473,10 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
} else {
let mut has_priv = false;
for (fi, fd) in adt_def.non_enum_variant().fields.iter_enumerated() {
if fd.vis.is_accessible_from(self.body().source.def_id(), self.tcx()) {
res_partial.push(All(self.tcx().mk_place_field(
pl,
fi,
fd.ty(self.tcx(), subst),
)));
if fd.vis.is_accessible_from(self.body().source.def_id(), tcx) {
let ty = tcx
.normalize_erasing_regions(self.typing_env, fd.ty(tcx, subst));
res_partial.push(All(tcx.mk_place_field(pl, fi, ty)));
} else {
has_priv = true;
}
Expand All @@ -492,13 +489,13 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {

Tuple(tys) => {
for (i, ty) in tys.iter().enumerate() {
res_partial.push(All(self.tcx().mk_place_field(pl, FieldIdx::new(i), ty)));
res_partial.push(All(tcx.mk_place_field(pl, FieldIdx::new(i), ty)));
}
}

Closure(_did, substs) => {
for (i, ty) in substs.as_closure().upvar_tys().iter().enumerate() {
res_partial.push(All(self.tcx().mk_place_field(pl, FieldIdx::new(i), ty)));
res_partial.push(All(tcx.mk_place_field(pl, FieldIdx::new(i), ty)));
}
}

Expand Down Expand Up @@ -698,7 +695,6 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
| StorageLive(_)
| FakeRead(_)
| AscribeUserType(_, _)
| Retag(_, _)
| Coverage(_)
| PlaceMention(_)
| ConstEvalCounter
Expand Down
1 change: 0 additions & 1 deletion creusot/src/analysis/borrows.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,6 @@ impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {

mir::StatementKind::FakeRead(..)
| mir::StatementKind::SetDiscriminant { .. }
| mir::StatementKind::Retag { .. }
| mir::StatementKind::PlaceMention(..)
| mir::StatementKind::AscribeUserType(..)
| mir::StatementKind::Coverage(..)
Expand Down
4 changes: 2 additions & 2 deletions creusot/src/backend/clone_map.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,8 +138,8 @@ pub(crate) trait Namer<'tcx> {
/// Ideally we'd like to avoid caring about normalization in the backend,
/// but we still need this for normalizing field types after instantiation.
/// Also for normalizing RPITs but that seems easier to get rid of if we ever care to.
fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ty: T) -> T {
self.tcx().normalize_erasing_regions(self.typing_env(), Unnormalized::new(ty))
fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ty: Unnormalized<'tcx, T>) -> T {
self.tcx().normalize_erasing_regions(self.typing_env(), ty)
}

fn import_prelude_module(&self, module: PreMod) {
Expand Down
12 changes: 8 additions & 4 deletions creusot/src/backend/clone_map/elaborator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -685,7 +685,8 @@ fn postcondition_once_term<'tcx>(
// Handle `FnGhostWrapper`
TyKind::Adt(def, subst_inner) if Intrinsic::FnGhostWrapper.is(ctx, def.did()) => {
let mut subst_postcond = subst.to_vec();
let closure_ty = def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner);
let closure_ty =
names.normalize(def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner));
subst_postcond[1] = GenericArg::from(closure_ty);
let subst_postcond = ctx.mk_args(&subst_postcond);
let post_fn = Intrinsic::PostconditionOnce.get(ctx);
Expand Down Expand Up @@ -766,7 +767,8 @@ fn postcondition_mut_term<'tcx>(
// Handle `FnGhostWrapper`
TyKind::Adt(def, subst_inner) if Intrinsic::FnGhostWrapper.is(ctx, def.did()) => {
let mut subst_postcond = subst.to_vec();
let closure_ty = def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner);
let closure_ty =
names.normalize(def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner));
subst_postcond[1] = GenericArg::from(closure_ty);
let subst_postcond = ctx.mk_args(&subst_postcond);
let post_fn = Intrinsic::PostconditionMut.get(ctx);
Expand Down Expand Up @@ -851,7 +853,8 @@ fn postcondition_term<'tcx>(
}
// Handle `FnGhostWrapper`
TyKind::Adt(def, subst_inner) if Intrinsic::FnGhostWrapper.is(ctx, def.did()) => {
let closure_ty = def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner);
let closure_ty =
names.normalize(def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner));
let mut subst_postcond = subst.to_vec();
subst_postcond[1] = GenericArg::from(closure_ty);
let subst_postcond = ctx.mk_args(&subst_postcond);
Expand Down Expand Up @@ -958,7 +961,8 @@ fn precondition_term<'tcx>(
// Handle `FnGhostWrapper`
TyKind::Adt(def, subst_inner) if Intrinsic::FnGhostWrapper.is(ctx, def.did()) => {
let mut subst_postcond = subst.to_vec();
let closure_ty = def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner);
let closure_ty =
names.normalize(def.all_fields().next().unwrap().ty(ctx.tcx, subst_inner));
subst_postcond[1] = GenericArg::from(closure_ty);
let subst_postcond = ctx.mk_args(&subst_postcond);
let pre_fn = Intrinsic::Precondition.get(ctx);
Expand Down
75 changes: 60 additions & 15 deletions creusot/src/backend/optimization/invariants.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ pub(crate) fn infer_invariant<'tcx>(
let mut unchanged_trms = vec![];
for (&l, t) in changed.0.iter() {
let trm = Term::var(l, body.locals[&l].ty);
t.to_unchanged_term_vec(ctx, scope, trm, &mut unchanged_trms);
t.to_unchanged_term_vec(ctx, scope, typing_env, trm, &mut unchanged_trms);
}

for u in unchanged_trms {
Expand Down Expand Up @@ -131,7 +131,7 @@ pub(crate) fn infer_invariant<'tcx>(
let ty_inv_places = ty_inv_analysis_states
.swap_remove(&k)
.unwrap_or_default()
.to_tyinv_place_vec(&changed, ctx, body);
.to_tyinv_place_vec(&changed, ctx, body, typing_env);
for pl in ty_inv_places {
let inv = projections_term(
ctx,
Expand Down Expand Up @@ -183,6 +183,7 @@ impl ChangedPlacesTree {
&self,
ctx: &TranslationCtx<'tcx>,
scope: DefId,
typing_env: TypingEnv<'tcx>,
t: Term<'tcx>,
acc: &mut Vec<Term<'tcx>>,
) {
Expand All @@ -192,14 +193,20 @@ impl ChangedPlacesTree {
if let TyKind::Ref(_, _, Mutability::Mut) = t.ty.kind() {
acc.push(t.clone().fin())
}
c.to_unchanged_term_vec(ctx, scope, t.deref(), acc);
c.to_unchanged_term_vec(ctx, scope, typing_env, t.deref(), acc);
}
Self::Fields(c) => match t.ty.kind() {
TyKind::Closure(_, subst) => {
for ((idx, c), ty) in c.iter_enumerated().zip_eq(subst.as_closure().upvar_tys())
{
if let Some(c) = c {
c.to_unchanged_term_vec(ctx, scope, t.clone().proj(idx, ty), acc);
c.to_unchanged_term_vec(
ctx,
scope,
typing_env,
t.clone().proj(idx, ty),
acc,
);
} else {
acc.push(t.clone().proj(idx, ty));
}
Expand All @@ -208,7 +215,13 @@ impl ChangedPlacesTree {
TyKind::Tuple(tys) => {
for ((idx, c), ty) in c.iter_enumerated().zip_eq(tys.iter()) {
if let Some(c) = c {
c.to_unchanged_term_vec(ctx, scope, t.clone().proj(idx, ty), acc);
c.to_unchanged_term_vec(
ctx,
scope,
typing_env,
t.clone().proj(idx, ty),
acc,
);
} else {
acc.push(t.clone().proj(idx, ty));
}
Expand All @@ -221,9 +234,16 @@ impl ChangedPlacesTree {
for ((idx, fdef), c) in
def.non_enum_variant().fields.iter_enumerated().zip_eq(c)
{
let ty = fdef.ty(ctx.tcx, subst);
let ty =
ctx.tcx.normalize_erasing_regions(typing_env, fdef.ty(ctx.tcx, subst));
if let Some(c) = c {
c.to_unchanged_term_vec(ctx, scope, t.clone().proj(idx, ty), acc);
c.to_unchanged_term_vec(
ctx,
scope,
typing_env,
t.clone().proj(idx, ty),
acc,
);
} else if fdef.vis.is_accessible_from(scope, ctx.tcx) {
acc.push(t.clone().proj(idx, ty));
}
Expand Down Expand Up @@ -426,7 +446,9 @@ impl TyInvPlacesTree {
.variant(place_ty.variant_index.unwrap_or(VariantIdx::ZERO))
.fields
.iter()
.map(|f| f.ty(ctx.tcx, subst))
.map(|f| {
ctx.tcx.normalize_erasing_regions(ctx.typing_env, f.ty(ctx.tcx, subst))
})
.collect(),
_ => unreachable!(),
};
Expand Down Expand Up @@ -480,7 +502,12 @@ impl TyInvPlacesTree {
.variants()
.iter()
.map(|v| {
if v.fields.iter().all(|f| is_tyinv_trivial(f.ty(ctx.tcx, subst))) {
if v.fields.iter().all(|f| {
is_tyinv_trivial(ctx.tcx.normalize_erasing_regions(
ctx.typing_env,
f.ty(ctx.tcx, subst),
))
}) {
Self::Top
} else {
Self::TyInv
Expand All @@ -503,7 +530,12 @@ impl TyInvPlacesTree {
} else if has_no_user_invariant(ctx, place_ty.ty, ctx.typing_env)
&& vs.iter().zip_eq(def.variants()).all(|(t, v)| {
matches!(t, Self::TyInv)
|| v.fields.iter().all(|f| is_tyinv_trivial(f.ty(ctx.tcx, subst)))
|| v.fields.iter().all(|f| {
is_tyinv_trivial(ctx.tcx.normalize_erasing_regions(
ctx.typing_env,
f.ty(ctx.tcx, subst),
))
})
})
{
*self = Self::TyInv
Expand Down Expand Up @@ -551,6 +583,7 @@ impl TyInvPlacesTree {
changed: &ChangedPlacesTree,
ctx: &TranslationCtx<'tcx>,
local: Ident,
typing_env: TypingEnv<'tcx>,
mut projection: Vec<ProjectionElem<'tcx>>,
mut place_ty: PlaceTy<'tcx>,
acc: &mut Vec<Place<'tcx>>,
Expand All @@ -567,7 +600,7 @@ impl TyInvPlacesTree {
projection.push(ProjectionElem::Deref);
assert_matches!(place_ty.variant_index, None);
place_ty.ty = place_ty.ty.builtin_deref(true).unwrap();
s.to_tyinv_place_vec(changed, ctx, local, projection, place_ty, acc)
s.to_tyinv_place_vec(changed, ctx, local, typing_env, projection, place_ty, acc)
}
Self::Fields(flds) => {
let changed: Box<dyn Iterator<Item = &Option<ChangedPlacesTree>>> = match changed {
Expand All @@ -579,10 +612,21 @@ impl TyInvPlacesTree {
};
for ((idx, s), changed) in flds.iter_enumerated().zip(changed) {
let Some(changed) = changed else { continue };
let ty = PlaceTy::field_ty(ctx.tcx, place_ty.ty, place_ty.variant_index, idx);
let ty = ctx.tcx.normalize_erasing_regions(
typing_env,
PlaceTy::field_ty(ctx.tcx, place_ty.ty, place_ty.variant_index, idx),
);
let mut proj = projection.clone();
proj.push(ProjectionElem::Field(idx, ty));
s.to_tyinv_place_vec(changed, ctx, local, proj, PlaceTy::from_ty(ty), acc);
s.to_tyinv_place_vec(
changed,
ctx,
local,
typing_env,
proj,
PlaceTy::from_ty(ty),
acc,
);
}
}
Self::Downcasts(vs) => {
Expand All @@ -591,7 +635,7 @@ impl TyInvPlacesTree {
let mut proj = projection.clone();
proj.push(ProjectionElem::Downcast(None, idx));
place_ty.variant_index = Some(idx);
s.to_tyinv_place_vec(changed, ctx, local, proj, place_ty, acc);
s.to_tyinv_place_vec(changed, ctx, local, typing_env, proj, place_ty, acc);
}
}
}
Expand Down Expand Up @@ -694,12 +738,13 @@ impl TyInvState {
changed: &ChangedPlaces,
ctx: &TranslationCtx<'tcx>,
body: &Body<'tcx>,
typing_env: TypingEnv<'tcx>,
) -> Vec<Place<'tcx>> {
let mut acc = vec![];
for (&local, state) in &self.0 {
let Some(changed) = changed.0.get(&local) else { continue };
let placety = PlaceTy::from_ty(body.locals[&local].ty);
state.to_tyinv_place_vec(changed, ctx, local, vec![], placety, &mut acc);
state.to_tyinv_place_vec(changed, ctx, local, typing_env, vec![], placety, &mut acc);
}
acc
}
Expand Down
4 changes: 2 additions & 2 deletions creusot/src/backend/program.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ use rustc_abi::VariantIdx;
use rustc_hir::{Safety, def::DefKind, def_id::DefId};
use rustc_middle::{
mir::{BasicBlock, BinOp, PlaceTy, ProjectionElem, START_BLOCK, UnOp},
ty::{self, AdtDef, GenericArgs, GenericArgsRef, Ty, TyCtxt, TyKind},
ty::{self, AdtDef, GenericArgs, GenericArgsRef, Ty, TyCtxt, TyKind, Unnormalized},
};
use rustc_span::{DUMMY_SP, Span};
use rustc_type_ir::IntTy;
Expand Down Expand Up @@ -153,7 +153,7 @@ pub(crate) fn to_why_body<'tcx>(
let (mut sig, variant) = {
let mut sig = sig.clone();
// normalize any RPITs away
sig.output = names.normalize(sig.output);
sig.output = names.normalize(Unnormalized::new(sig.output));
let variant = sig.contract.variant.clone();
sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, def_id);
(lower_program_sig(ctx, names, name, sig, def_id, name::return_()), variant)
Expand Down
Loading
Loading