From 08f03d661e1f1af8216ec07c68a90c89f76ec861 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 12 Jun 2026 15:17:38 +0200 Subject: [PATCH] Update toolchain to nightly-2026-06-22 --- creusot-metadata/src/encoder.rs | 2 +- creusot-std/src/lib.rs | 1 - creusot/src/analysis.rs | 32 ++++---- creusot/src/analysis/borrows.rs | 1 - creusot/src/backend/clone_map.rs | 4 +- creusot/src/backend/clone_map/elaborator.rs | 12 ++- .../src/backend/optimization/invariants.rs | 75 +++++++++++++++---- creusot/src/backend/program.rs | 4 +- creusot/src/backend/resolve.rs | 18 ++--- creusot/src/backend/term.rs | 6 +- creusot/src/backend/ty_inv.rs | 22 ++---- creusot/src/cleanup_spec_closures.rs | 1 + creusot/src/ctx.rs | 49 ++++++++---- creusot/src/gather_spec_closures.rs | 2 +- creusot/src/translation/constant.rs | 28 ++++--- creusot/src/translation/function.rs | 10 +-- creusot/src/translation/function/statement.rs | 4 +- creusot/src/translation/pearlite/from_thir.rs | 15 ++-- creusot/src/util.rs | 2 +- creusot/src/validate/opacity.rs | 45 +++++------ creusot/src/validate/recursive_types.rs | 2 +- creusot/src/very_stable_hash.rs | 2 +- flake.lock | 24 +++--- rust-toolchain | 2 +- .../trait_def_and_impl_disagree.stderr | 12 +-- 25 files changed, 216 insertions(+), 159 deletions(-) diff --git a/creusot-metadata/src/encoder.rs b/creusot-metadata/src/encoder.rs index 9dccf5abec..a2c3e3e715 100644 --- a/creusot-metadata/src/encoder.rs +++ b/creusot-metadata/src/encoder.rs @@ -22,7 +22,7 @@ use std::{ pub struct MetadataEncoder<'a, 'tcx> { tcx: TyCtxt<'tcx>, - pub opaque: FileEncoder, + pub opaque: FileEncoder<'a>, type_shorthands: FxHashMap, usize>, predicate_shorthands: FxHashMap, usize>, file_to_file_index: FxHashMap<*const SourceFile, SourceFileIndex>, diff --git a/creusot-std/src/lib.rs b/creusot-std/src/lib.rs index 22257cede3..356a814c73 100644 --- a/creusot-std/src/lib.rs +++ b/creusot-std/src/lib.rs @@ -64,7 +64,6 @@ range_bounds_is_empty, bound_copied, auto_traits, - new_range_api_legacy, negative_impls, exact_size_is_empty, ) diff --git a/creusot/src/analysis.rs b/creusot/src/analysis.rs index d806440f78..d134d397ba 100644 --- a/creusot/src/analysis.rs +++ b/creusot/src/analysis.rs @@ -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), @@ -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; } @@ -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))); } } @@ -698,7 +695,6 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> { | StorageLive(_) | FakeRead(_) | AscribeUserType(_, _) - | Retag(_, _) | Coverage(_) | PlaceMention(_) | ConstEvalCounter diff --git a/creusot/src/analysis/borrows.rs b/creusot/src/analysis/borrows.rs index a91972a3d7..c9917e858b 100644 --- a/creusot/src/analysis/borrows.rs +++ b/creusot/src/analysis/borrows.rs @@ -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(..) diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index b2cb4b79a6..816dbe815a 100644 --- a/creusot/src/backend/clone_map.rs +++ b/creusot/src/backend/clone_map.rs @@ -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>>(&self, ty: T) -> T { - self.tcx().normalize_erasing_regions(self.typing_env(), Unnormalized::new(ty)) + fn normalize>>(&self, ty: Unnormalized<'tcx, T>) -> T { + self.tcx().normalize_erasing_regions(self.typing_env(), ty) } fn import_prelude_module(&self, module: PreMod) { diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index 76a4b07818..768729bfea 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/creusot/src/backend/clone_map/elaborator.rs @@ -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); @@ -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); @@ -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); @@ -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); diff --git a/creusot/src/backend/optimization/invariants.rs b/creusot/src/backend/optimization/invariants.rs index f12350a0cd..f561b7b7fc 100644 --- a/creusot/src/backend/optimization/invariants.rs +++ b/creusot/src/backend/optimization/invariants.rs @@ -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 { @@ -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, @@ -183,6 +183,7 @@ impl ChangedPlacesTree { &self, ctx: &TranslationCtx<'tcx>, scope: DefId, + typing_env: TypingEnv<'tcx>, t: Term<'tcx>, acc: &mut Vec>, ) { @@ -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)); } @@ -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)); } @@ -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)); } @@ -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!(), }; @@ -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 @@ -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 @@ -551,6 +583,7 @@ impl TyInvPlacesTree { changed: &ChangedPlacesTree, ctx: &TranslationCtx<'tcx>, local: Ident, + typing_env: TypingEnv<'tcx>, mut projection: Vec>, mut place_ty: PlaceTy<'tcx>, acc: &mut Vec>, @@ -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>> = match changed { @@ -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) => { @@ -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); } } } @@ -694,12 +738,13 @@ impl TyInvState { changed: &ChangedPlaces, ctx: &TranslationCtx<'tcx>, body: &Body<'tcx>, + typing_env: TypingEnv<'tcx>, ) -> Vec> { 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 } diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index d113317565..14e687c9b7 100644 --- a/creusot/src/backend/program.rs +++ b/creusot/src/backend/program.rs @@ -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; @@ -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) diff --git a/creusot/src/backend/resolve.rs b/creusot/src/backend/resolve.rs index 48c8382bb6..cc2d389b9a 100644 --- a/creusot/src/backend/resolve.rs +++ b/creusot/src/backend/resolve.rs @@ -2,7 +2,7 @@ use std::collections::HashSet; use rustc_ast::Mutability; use rustc_hir::def_id::DefId; -use rustc_middle::ty::{GenericArg, Ty, TypingEnv, Unnormalized}; +use rustc_middle::ty::{GenericArg, Ty, TypingEnv}; use rustc_span::{DUMMY_SP, Span}; use rustc_type_ir::TyKind; @@ -60,14 +60,10 @@ pub fn is_resolve_trivial<'tcx>( return false; } AdtKind::Box(ty) => stack.push(ty), - AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => { - stack.extend(def.all_fields().map(|f| { - ctx.normalize_erasing_regions( - typing_env, - Unnormalized::new(f.ty(ctx.tcx, subst)), - ) - })) - } + AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => stack.extend( + def.all_fields() + .map(|f| ctx.normalize_erasing_regions(typing_env, f.ty(ctx.tcx, subst))), + ), }, TyKind::Closure(_, subst) => stack.extend(subst.as_closure().upvar_tys()), TyKind::Param(_) @@ -123,7 +119,7 @@ pub(crate) fn structural_resolve<'tcx>( let mut exp = Some(Term::true_(ctx.tcx)); let fields = var.fields.iter_enumerated().map(|(ix, f)| { let sym = Ident::fresh_local(&format!("x{}", ix.as_usize())); - let fty = f.ty(ctx.tcx, subst); + let fty = names.normalize(f.ty(ctx.tcx, subst)); exp = Some(exp.take().unwrap().conj(ctx.resolve( names.source_id(), names.typing_env(), @@ -139,7 +135,7 @@ pub(crate) fn structural_resolve<'tcx>( let mut exp = Term::true_(ctx.tcx); for (ix, f) in adt.non_enum_variant().fields.iter_enumerated() { if f.vis.is_accessible_from(names.source_id(), ctx.tcx) { - let fty = f.ty(ctx.tcx, subst); + let fty = names.normalize(f.ty(ctx.tcx, subst)); exp = exp.conj(ctx.resolve( names.source_id(), names.typing_env(), diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs index c8b0995783..20a732ef24 100644 --- a/creusot/src/backend/term.rs +++ b/creusot/src/backend/term.rs @@ -543,7 +543,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> { } Literal::ZST => Exp::unit(), Literal::String(ref string) => Constant::String(string.clone()).into(), - Literal::Bytes(ref bytes) => todo!(), + Literal::Bytes(ref _bytes) => todo!(), } } } @@ -605,7 +605,9 @@ pub(crate) fn tyconst_to_term_final<'tcx>( use rustc_type_ir::ConstKind::*; match c.kind() { Value(ty::Value { ty, valtree }) => valtree_to_term(valtree, ctx, ty, env, span), - Unevaluated(ty::UnevaluatedConst { def, args }) => Some(Term::item(def, args, ty)), + Unevaluated(ty::UnevaluatedConst { kind, args, .. }) => { + Some(Term::item(kind.opt_def_id().unwrap(), args, ty)) + } Param(p) => { let tcx = ctx.tcx; let def_id = tcx.generics_of(caller_id).const_param(p, tcx).def_id; diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs index 3b49671e2c..dbd49abb82 100644 --- a/creusot/src/backend/ty_inv.rs +++ b/creusot/src/backend/ty_inv.rs @@ -69,14 +69,10 @@ pub(crate) fn is_tyinv_trivial<'tcx>( AdtKind::Struct { partially_opaque: true } | AdtKind::Opaque { always: false } | AdtKind::Empty => return false, - AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => { - stack.extend(def.all_fields().map(|f| { - ctx.normalize_erasing_regions( - typing_env, - Unnormalized::new(f.ty(ctx.tcx, subst)), - ) - })) - } + AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => stack.extend( + def.all_fields() + .map(|f| ctx.normalize_erasing_regions(typing_env, f.ty(ctx.tcx, subst))), + ), AdtKind::Box(_) => unreachable!(), }, TyKind::Closure(_, subst) => stack.extend(subst.as_closure().upvar_tys()), @@ -199,7 +195,7 @@ fn structural_invariant<'tcx>( let mut exp = Term::true_(ctx.tcx); let fields = var_def.fields.iter_enumerated().map(|(field_idx, field_def)| { let field_name = Ident::fresh_local(field_name(field_def.name.as_str())); - let field_ty = field_def.ty(ctx.tcx, subst); + let field_ty = names.normalize(field_def.ty(ctx.tcx, subst)); conj_inv_call(ctx, names, &mut exp, Term::var(field_name, field_ty)); (field_idx, Pattern::binder(field_name, field_ty)) }); @@ -214,12 +210,8 @@ fn structural_invariant<'tcx>( let mut exp = Term::true_(ctx.tcx); for (field_idx, field_def) in def.non_enum_variant().fields.iter_enumerated() { if field_def.vis.is_accessible_from(names.source_id(), ctx.tcx) { - conj_inv_call( - ctx, - names, - &mut exp, - subject.clone().proj(field_idx, field_def.ty(ctx.tcx, subst)), - ) + let ty = names.normalize(field_def.ty(ctx.tcx, subst)); + conj_inv_call(ctx, names, &mut exp, subject.clone().proj(field_idx, ty)) } } if partially_opaque { diff --git a/creusot/src/cleanup_spec_closures.rs b/creusot/src/cleanup_spec_closures.rs index 466fc88306..3443857915 100644 --- a/creusot/src/cleanup_spec_closures.rs +++ b/creusot/src/cleanup_spec_closures.rs @@ -166,6 +166,7 @@ pub(crate) fn make_loop<'tcx>() -> IndexVec> { let mut body = IndexVec::new(); body.push(BasicBlockData::new( Some(Terminator { + attributes: Default::default(), source_info: SourceInfo::outermost(rustc_span::DUMMY_SP), kind: TerminatorKind::Return, }), diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index 2e8cf30248..f5931f1cb7 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -204,34 +204,55 @@ impl<'tcx> Deref for TranslationCtx<'tcx> { } pub(crate) fn gather_params_open_inv(tcx: TyCtxt) -> HashMap> { - struct VisitFns<'tcx, 'a>( - TyCtxt<'tcx>, - HashMap>, - &'a ResolverAstLowering<'tcx>, - ); + struct VisitFns<'tcx, 'a> { + tcx: TyCtxt<'tcx>, + resolver: &'a ResolverAstLowering<'tcx>, + parent_id: Option, + open_inv_params: HashMap>, + } impl<'a> Visitor<'a> for VisitFns<'_, 'a> { + fn visit_item(&mut self, item: &'a rustc_ast::Item) { + let old = std::mem::replace(&mut self.parent_id, Some(item.id)); + rustc_ast::visit::walk_item(self, item); + self.parent_id = old; + } + + fn visit_assoc_item( + &mut self, + item: &'a rustc_ast::AssocItem, + ctxt: rustc_ast::visit::AssocCtxt, + ) -> Self::Result { + let old = std::mem::replace(&mut self.parent_id, Some(item.id)); + rustc_ast::visit::walk_assoc_item(self, item, ctxt); + self.parent_id = old; + } + fn visit_fn(&mut self, fk: FnKind<'a>, _: &AttrVec, _: Span, node: NodeId) { - let (shift, decl) = match fk { - FnKind::Fn(_, _, Fn { sig: FnSig { decl, .. }, .. }) => (0, decl), - FnKind::Closure(_, _, decl, _) => (1, decl), + let data = &self.resolver.owners[&self.parent_id.unwrap()]; + let (shift, decl, id) = match fk { + FnKind::Fn(_, _, Fn { sig: FnSig { decl, .. }, .. }) => (0, decl, data.def_id), + FnKind::Closure(_, _, decl, _) => { + (1, decl, *data.node_id_to_def_id.get(&node).unwrap()) + } }; let mut open_inv_params = DenseBitSet::new_empty(shift + decl.inputs.len()); for (i, p) in (shift..).zip(decl.inputs.iter()) { - if is_open_inv_param(self.0, p) { + if is_open_inv_param(self.tcx, p) { open_inv_params.insert(i); } } - let defid = self.2.node_id_to_def_id[&node].to_def_id(); - assert!(self.1.insert(defid, open_inv_params).is_none()); + assert!(self.open_inv_params.insert(id.to_def_id(), open_inv_params).is_none()); walk_fn(self, fk) } } - let (resolver, cr) = &*tcx.resolver_for_lowering().borrow(); + let (resolver, cr) = tcx.resolver_for_lowering(); + let resolver = &*resolver.borrow(); + let cr = &*cr.borrow(); - let mut visit = VisitFns(tcx, HashMap::new(), resolver); + let mut visit = VisitFns { tcx, resolver, parent_id: None, open_inv_params: HashMap::new() }; visit.visit_crate(cr); - visit.1 + visit.open_inv_params } impl<'tcx> TranslationCtx<'tcx> { diff --git a/creusot/src/gather_spec_closures.rs b/creusot/src/gather_spec_closures.rs index 1d531b5187..d063f7dabd 100644 --- a/creusot/src/gather_spec_closures.rs +++ b/creusot/src/gather_spec_closures.rs @@ -76,7 +76,7 @@ impl<'tcx> Visitor<'tcx> for Closures<'tcx> { Rvalue::Aggregate(box AggregateKind::Closure(id, _), _) => { self.closures.insert(*id); } - Rvalue::Use(Operand::Constant(box ck)) => { + Rvalue::Use(Operand::Constant(box ck), _) => { if let Some(def_id) = snapshot_closure_id(self.tcx, ck.const_.ty()) { self.closures.insert(def_id); } diff --git a/creusot/src/translation/constant.rs b/creusot/src/translation/constant.rs index a0dc7912e8..0c0ed20279 100644 --- a/creusot/src/translation/constant.rs +++ b/creusot/src/translation/constant.rs @@ -7,7 +7,7 @@ use rustc_abi::Size; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::{ mir::{self, ConstOperand, ConstValue, TerminatorKind, interpret::AllocRange}, - ty::{self, ConstKind, Ty, TypingEnv}, + ty::{self, ConstKind, Ty, TyCtxt, TypingEnv, UnevaluatedConstKind}, }; use rustc_span::Span; @@ -169,7 +169,11 @@ pub fn try_const_to_term<'tcx>( let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst); let ty = ctx.tcx.normalize_erasing_regions(typing_env, ty); let span = ctx.def_span(def_id); - let uneval = ty::UnevaluatedConst::new(def_id, subst); + let uneval = ty::UnevaluatedConst::new( + ctx.tcx, + ty::UnevaluatedConstKind::new_from_def_id(ctx.tcx, def_id), + subst, + ); match ctx.const_eval_resolve_for_typeck(typing_env, uneval, span) { Ok(Ok(val)) => valtree_to_term(val, ctx, ty, typing_env, span), _ => try_const_synonym(def_id, subst, ctx, typing_env), @@ -232,23 +236,22 @@ fn try_const_synonym<'tcx>( let ty::Instance { def, args } = ty::Instance::try_resolve(ctx.tcx, typing_env, def_id, subst).ok()??; let body = ctx.instance_mir(def); - let (c, ty, span) = simple_body_const(body)?; + let (c, ty, span) = simple_body_const(ctx.tcx, body)?; match c { ConstKind::Param(p) => { let c = args.const_at(p.index as usize); Some(Term::const_(c, ty, span)) } ConstKind::Unevaluated(u) - if matches!( - ctx.def_kind(u.def), - DefKind::Const { .. } | DefKind::AssocConst { .. } - ) => + if let UnevaluatedConstKind::Projection { def_id } + | UnevaluatedConstKind::Free { def_id } + | UnevaluatedConstKind::Inherent { def_id } = u.kind => { let (u, ty) = ctx.tcx.normalize_erasing_regions( typing_env, ty::EarlyBinder::bind((u, ty)).instantiate(ctx.tcx, args), ); - Some(Term::item(u.def, u.args, ty).span(span)) + Some(Term::item(def_id, u.args, ty).span(span)) } _ => None, } @@ -256,7 +259,10 @@ fn try_const_synonym<'tcx>( /// Extract constant from MIR body. It should be a single assignment `_0 = const M`. /// Otherwise return `None`. -fn simple_body_const<'tcx>(body: &mir::Body<'tcx>) -> Option<(ConstKind<'tcx>, Ty<'tcx>, Span)> { +fn simple_body_const<'tcx>( + tcx: TyCtxt<'tcx>, + body: &mir::Body<'tcx>, +) -> Option<(ConstKind<'tcx>, Ty<'tcx>, Span)> { if body.basic_blocks.len() != 1 { return None; } @@ -268,11 +274,11 @@ fn simple_body_const<'tcx>(body: &mir::Body<'tcx>) -> Option<(ConstKind<'tcx>, T if lhs.local != mir::Local::from_u32(0) || lhs.projection.len() != 0 { return None; } - let mir::Rvalue::Use(mir::Operand::Constant(rhs)) = rhs else { return None }; + let mir::Rvalue::Use(mir::Operand::Constant(rhs), _) = rhs else { return None }; match rhs.const_ { mir::Const::Ty(ty, c) => Some((c.kind(), ty, rhs.span)), mir::Const::Unevaluated(u, ty) => { - Some((rustc_type_ir::ConstKind::Unevaluated(u.shrink()), ty, rhs.span)) + Some((rustc_type_ir::ConstKind::Unevaluated(u.shrink(tcx)), ty, rhs.span)) } _ => return None, } diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs index e4837ec6f1..a9cb2984fb 100644 --- a/creusot/src/translation/function.rs +++ b/creusot/src/translation/function.rs @@ -292,11 +292,11 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> { } if let TyKind::Adt(adt_def, subst) = place_ty.ty.kind() && let Some(vi) = place_ty.variant_index - && adt_def - .variant(vi) - .fields - .iter() - .all(|f| self.skip_resolve_type(f.ty(self.tcx(), subst))) + && adt_def.variant(vi).fields.iter().all(|f| { + self.skip_resolve_type( + self.tcx().normalize_erasing_regions(self.typing_env, f.ty(self.tcx(), subst)), + ) + }) { assert_matches!(rpl, ResolvedPlace::All(_)); return; diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs index 9feb0448a2..f2c00fde3c 100644 --- a/creusot/src/translation/function/statement.rs +++ b/creusot/src/translation/function/statement.rs @@ -36,7 +36,6 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { | StatementKind::StorageLive(_) | StatementKind::FakeRead(_) | StatementKind::AscribeUserType(_, _) - | StatementKind::Retag(_, _) | StatementKind::Coverage(_) | StatementKind::PlaceMention(_) | StatementKind::ConstEvalCounter @@ -60,7 +59,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { let ty = rvalue.ty(self.body, self.tcx()); let span = si.span; let rval: RValue<'tcx> = match rvalue { - Rvalue::Use(op) => match op { + Rvalue::Use(op, _) => match op { Move(_pl) | Copy(_pl) => RValue::Operand(self.translate_operand(op, span)), Constant(box c) => { if let TyKind::Closure(def_id, _) = c.const_.ty().peel_refs().kind() @@ -209,6 +208,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { _, ) => self.ctx.crash_and_error(si.span, format!("Unsupported pointer cast: {rvalue:?}")), Rvalue::CopyForDeref(_) + | Rvalue::Reborrow(..) | Rvalue::ThreadLocalRef(_) | Rvalue::WrapUnsafeBinder(_, _) => self.ctx.crash_and_error( si.span, diff --git a/creusot/src/translation/pearlite/from_thir.rs b/creusot/src/translation/pearlite/from_thir.rs index 5b40d2f624..a61ce2747d 100644 --- a/creusot/src/translation/pearlite/from_thir.rs +++ b/creusot/src/translation/pearlite/from_thir.rs @@ -17,7 +17,7 @@ use rustc_middle::{ self, AdtExpr, ArmId, Block, ClosureExpr, ExprId, ExprKind, LocalVarId, Pat, PatKind, StmtId, StmtKind, Thir, }, - ty::{CapturedPlace, Ty, TyKind, adjustment::PointerCoercion}, + ty::{CapturedPlace, Ty, TyKind, TypingEnv, adjustment::PointerCoercion}, }; use rustc_span::{ErrorGuaranteed, Symbol, sym}; use std::{ @@ -55,7 +55,8 @@ pub(crate) fn from_thir_with_triggers<'tcx>( let did = id.into(); let (thir, expr) = ctx.thir_body(id); let thir = &thir.borrow(); - let lower = ThirTerm { ctx, item_id: id, thir }; + let typing_env = ctx.typing_env(did); + let lower = ThirTerm { ctx, item_id: id, thir, typing_env }; let (triggers, body) = lower.body_term(expr)?; @@ -132,6 +133,7 @@ struct ThirTerm<'a, 'tcx> { ctx: &'a TranslationCtx<'tcx>, item_id: LocalDefId, thir: &'a Thir<'tcx>, + typing_env: TypingEnv<'tcx>, } // TODO: Ensure that types are correct during this translation, in particular @@ -466,12 +468,13 @@ impl<'tcx> ThirTerm<'_, 'tcx> { for missing_field in missing { let missing_field: FieldIdx = missing_field.into(); + let missing_field_ty = self.ctx.tcx.normalize_erasing_regions( + self.typing_env, + variant.fields[missing_field].ty(self.ctx.tcx, args), + ); fields.push(( missing_field, - base.clone().proj( - missing_field, - variant.fields[missing_field].ty(self.ctx.tcx, args), - ), + base.clone().proj(missing_field, missing_field_ty), )); } } diff --git a/creusot/src/util.rs b/creusot/src/util.rs index 07b01c6e5b..f749c6c4e0 100644 --- a/creusot/src/util.rs +++ b/creusot/src/util.rs @@ -96,7 +96,7 @@ pub fn forge_def_id_from( } fn compute_stable_hash(key: DefKey, parent: DefPathHash) -> DefPathHash { - let mut hasher = rustc_data_structures::stable_hasher::StableHasher::new(); + let mut hasher = rustc_data_structures::stable_hash::StableHasher::new(); // The new path is in the same crate as `parent`, and will contain the stable_crate_id. // Therefore, we only need to include information of the parent's local hash. diff --git a/creusot/src/validate/opacity.rs b/creusot/src/validate/opacity.rs index 7ee3d8919c..0142b6e390 100644 --- a/creusot/src/validate/opacity.rs +++ b/creusot/src/validate/opacity.rs @@ -23,9 +23,17 @@ struct OpacityVisitor<'a, 'tcx> { } impl OpacityVisitor<'_, '_> { - fn is_visible_enough(&self, id: DefId) -> bool { - let Opacity::Transparent(op) = self.opacity else { return true }; - self.ctx.visibility(id).is_at_least(op, self.ctx.tcx) + /// Assert that `id` is visible from the body of `self.item` with opacity `self.opacity`. + fn assert_visible(&self, id: DefId, span: Span) { + if !self.is_visible(id) { + self.error(id, span) + } + } + + fn is_visible(&self, id: DefId) -> bool { + use std::cmp::Ordering::{Equal, Greater}; + let Opacity::Transparent(self_vis) = self.opacity else { return true }; + matches!(self.ctx.visibility(id).partial_cmp(self_vis, self.ctx.tcx), Some(Greater | Equal)) } fn error(&self, id: DefId, span: Span) { @@ -49,33 +57,21 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { if matches!(self.ctx.def_kind(id), DefKind::ConstParam) { return; } - if !self.is_visible_enough(id) { - self.error(id, term.span) - } - } - &TermKind::Call { id, .. } => { - if !self.is_visible_enough(id) { - self.error(id, term.span) - } + self.assert_visible(id, term.span); } + &TermKind::Call { id, .. } => self.assert_visible(id, term.span), &TermKind::Constructor { variant, .. } => { if let Some(adt) = term.ty.ty_adt_def() { - if !self.is_visible_enough(adt.did()) { - self.error(adt.did(), term.span); - } + self.assert_visible(adt.did(), term.span); for fld in &adt.variant(variant).fields { - if !self.is_visible_enough(fld.did) { - self.error(fld.did, term.span); - } + self.assert_visible(fld.did, term.span); } } } &TermKind::Projection { idx, ref lhs } => { if let Some(adt) = lhs.ty.ty_adt_def() { let fdid = adt.non_enum_variant().fields[idx].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, term.span); - } + self.assert_visible(fdid, term.span); } } &TermKind::Reborrow { ref projections, ref inner } => { @@ -89,9 +85,8 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { && adt.is_struct() { let fdid = adt.non_enum_variant().fields[*field_idx].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, term.span); - } + + self.assert_visible(fdid, term.span); } } ProjectionElem::Deref | ProjectionElem::Index(_) => (), @@ -111,9 +106,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { let fields_def = &pat.ty.ty_adt_def().unwrap().variants()[*variant_idx].fields; for (fld, _) in patterns { let fdid = fields_def[*fld].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, pat.span); - } + self.assert_visible(fdid, pat.span); } } _ => (), diff --git a/creusot/src/validate/recursive_types.rs b/creusot/src/validate/recursive_types.rs index 291a60dc59..1092c51ff5 100644 --- a/creusot/src/validate/recursive_types.rs +++ b/creusot/src/validate/recursive_types.rs @@ -342,7 +342,7 @@ fn build_type_graph(ctx: &TranslationCtx) -> TypeGraph { Struct(..) | Enum(..) | Union(..) => { add_type(ctx, item.owner_id.to_def_id(), &mut graph) } - Trait(..) => add_trait(ctx, item.owner_id.to_def_id(), &mut graph), + Trait { .. } => add_trait(ctx, item.owner_id.to_def_id(), &mut graph), _ => {} } } diff --git a/creusot/src/very_stable_hash.rs b/creusot/src/very_stable_hash.rs index a6a77444a2..c5d1eebc96 100644 --- a/creusot/src/very_stable_hash.rs +++ b/creusot/src/very_stable_hash.rs @@ -1,4 +1,4 @@ -use rustc_data_structures::stable_hasher::StableHasher; +use rustc_data_structures::stable_hash::StableHasher; use rustc_hashes::Hash64; use rustc_hir::{ def_id::{CrateNum, DefId}, diff --git a/flake.lock b/flake.lock index b37fcf96c2..8a6f411ad3 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "crane": { "locked": { - "lastModified": 1773189535, - "narHash": "sha256-E1G/Or6MWeP+L6mpQ0iTFLpzSzlpGrITfU2220Gq47g=", + "lastModified": 1781825982, + "narHash": "sha256-SlXKwIRIhrOSAcTjCB3ftPLzJWZStQIPS7J1FlZPnKk=", "owner": "ipetkov", "repo": "crane", - "rev": "6fa2fb4cf4a89ba49fc9dd5a3eb6cde99d388269", + "rev": "469fd08d0bcf6926321fa973c6777fbc87785dd7", "type": "github" }, "original": { @@ -20,11 +20,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1777988971, - "narHash": "sha256-qIoWPDs+0/8JecyYgE3gpKQxW/4bLW/gp45vow9ioCQ=", + "lastModified": 1778716662, + "narHash": "sha256-m1Yf0wZ8j1OHjTc2UwHwyQRSnNeSgLJOd7q5Y45hzi4=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "0678d8986be1661af6bb555f3489f2fdfc31f6ff", + "rev": "f7c1a2d347e4c52d5fb8d10cb4d94b5884e546fb", "type": "github" }, "original": { @@ -35,11 +35,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1773068389, - "narHash": "sha256-vMrm7Pk2hjBRPnCSjhq1pH0bg350Z+pXhqZ9ICiqqCs=", + "lastModified": 1781509190, + "narHash": "sha256-uJZs9Di8I6ciTp6jiojj0HzlNpBkud8ax5aT/O5aJkw=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "44bae273f9f82d480273bab26f5c50de3724f52f", + "rev": "d6df3513510aa548c83868fd22bfddd0a8c0a0d4", "type": "github" }, "original": { @@ -78,11 +78,11 @@ ] }, "locked": { - "lastModified": 1777259803, - "narHash": "sha256-fIb/EoVu/1U0qVrE6qZCJ2WCfprRpywNIAVzKEACIQc=", + "lastModified": 1782098508, + "narHash": "sha256-YeBVH+avasLg/ZTOyshNI4qfU8p5RbMs9O8944A1QDg=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "a6cb2224d975e16b5e67de688c6ad306f7203425", + "rev": "67eed429b53d462923d9be580cfc9ed372f7564f", "type": "github" }, "original": { diff --git a/rust-toolchain b/rust-toolchain index ec3e8f4b4d..3591f6952d 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2026-04-21" +channel = "nightly-2026-06-22" components = [ "rustfmt", "rustc-dev", "llvm-tools" ] diff --git a/tests/should_fail/terminates/trait_def_and_impl_disagree.stderr b/tests/should_fail/terminates/trait_def_and_impl_disagree.stderr index b277db1c46..f2e9b4496e 100644 --- a/tests/should_fail/terminates/trait_def_and_impl_disagree.stderr +++ b/tests/should_fail/terminates/trait_def_and_impl_disagree.stderr @@ -1,3 +1,9 @@ +error: Expected `h` to be `#[check(ghost)]` as specified by the trait declaration + --> trait_def_and_impl_disagree.rs:22:5 + | +22 | fn h() {} + | ^^^^^^ + error: Expected `f` to be `#[check(terminates)]` as specified by the trait declaration --> trait_def_and_impl_disagree.rs:17:5 | @@ -10,11 +16,5 @@ error: Expected `g` to be `#[check(ghost)]` as specified by the trait declaratio 20 | fn g() {} | ^^^^^^ -error: Expected `h` to be `#[check(ghost)]` as specified by the trait declaration - --> trait_def_and_impl_disagree.rs:22:5 - | -22 | fn h() {} - | ^^^^^^ - error: aborting due to 3 previous errors