From 3e16db29b4058dbf1f906591e9c7b89164b081bf Mon Sep 17 00:00:00 2001 From: N1ark Date: Sun, 31 May 2026 21:25:18 +0100 Subject: [PATCH 1/2] Bump rustc to `nightly-2026-05-31` --- charon/rust-toolchain | 2 +- charon/rustc_trait_elaboration/src/ctx.rs | 2 +- .../src/elaboration.rs | 14 +- .../rustc_trait_elaboration/src/item_ref.rs | 6 +- .../rustc_trait_elaboration/src/predicates.rs | 4 +- charon/rustc_trait_elaboration/src/utils.rs | 26 +- charon/src/bin/charon-driver/driver.rs | 11 +- .../hax/constant_utils/uneval.rs | 3 +- .../src/bin/charon-driver/hax/rustc_utils.rs | 30 +- charon/src/bin/charon-driver/hax/traits.rs | 11 +- .../src/bin/charon-driver/hax/types/def_id.rs | 5 +- .../charon-driver/hax/types/new/item_ref.rs | 8 +- .../hax/types/new/synthetic_items.rs | 5 +- charon/src/bin/charon-driver/hax/types/ty.rs | 20 +- .../translate/translate_bodies.rs | 12 +- .../translate/translate_predicates.rs | 1 - .../translate/translate_types.rs | 32 +- charon/src/pretty/formatter.rs | 6 +- charon/tests/ui/arrays.out | 81 ++- charon/tests/ui/closures.out | 7 +- charon/tests/ui/desugar_drops_to_calls.out | 35 +- .../tests/ui/desugar_drops_to_calls_mono.out | 35 +- charon/tests/ui/drop_after_overflow.out | 11 +- .../tests/ui/dyn-with-diamond-supertraits.out | 44 +- charon/tests/ui/issue-378-ctor-as-fn.out | 7 +- .../tests/ui/monomorphization/closure-fn.out | 5 +- .../ui/monomorphization/closure-fnonce.out | 5 +- charon/tests/ui/monomorphization/closures.out | 15 +- .../issue-917-inline-const-with-poly-type.out | 5 +- charon/tests/ui/ptr-offset.out | 2 +- charon/tests/ui/raw-boxes.out | 674 +++++++++--------- .../invalid-reconstruct-assert.out | 9 +- .../issue-1073-out-of-bounds-body-region.out | 441 +----------- .../issue-1074-vtable-supertrait.out | 5 +- charon/tests/ui/result-unwrap.out | 2 +- charon/tests/ui/simple/box-dyn-fnonce-raw.out | 11 +- charon/tests/ui/simple/box-dyn-fnonce.out | 4 +- charon/tests/ui/simple/builtin-drop-mono.out | 89 +-- charon/tests/ui/simple/builtin-drop.out | 116 ++- charon/tests/ui/simple/closure-fnonce.out | 5 +- .../closure-uses-ambient-self-clause.out | 7 +- charon/tests/ui/simple/closure-with-drops.out | 12 +- charon/tests/ui/simple/drop-cow.out | 9 +- .../simple/drop-glue-with-const-generic.out | 4 +- .../tests/ui/simple/drop-string-desugar.out | 17 +- charon/tests/ui/simple/drop-string.out | 7 +- .../ui/simple/dyn-cast-to-supertrait.out | 5 +- .../tests/ui/simple/lending-iterator-gat.out | 7 +- .../simple/single-variant-enum-drop-glue.out | 9 +- charon/tests/ui/simple/slice_index_range.out | 96 +-- charon/tests/ui/simple/struct-with-drops.out | 24 +- charon/tests/ui/simple/vec-push.out | 3 +- charon/tests/ui/slice-index-range.out | 84 ++- charon/tests/ui/traits.out | 9 +- flake.nix | 2 +- 55 files changed, 832 insertions(+), 1269 deletions(-) diff --git a/charon/rust-toolchain b/charon/rust-toolchain index 560f57966..3c98116ae 100644 --- a/charon/rust-toolchain +++ b/charon/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2026-04-18" +channel = "nightly-2026-05-31" components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ] targets = [ "x86_64-unknown-linux-gnu", "x86_64-apple-darwin", "x86_64-pc-windows-msvc", "aarch64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ] diff --git a/charon/rustc_trait_elaboration/src/ctx.rs b/charon/rustc_trait_elaboration/src/ctx.rs index 4533ae832..f23fe250c 100644 --- a/charon/rustc_trait_elaboration/src/ctx.rs +++ b/charon/rustc_trait_elaboration/src/ctx.rs @@ -103,7 +103,7 @@ impl<'tcx> PredicateCache<'tcx> { return predicates; } let predicates = compute(); - let _ = self.values.insert(def_id, predicates.clone()); + self.values.insert_unique(def_id, predicates.clone()); predicates } } diff --git a/charon/rustc_trait_elaboration/src/elaboration.rs b/charon/rustc_trait_elaboration/src/elaboration.rs index 8f44e0333..af6a290c2 100644 --- a/charon/rustc_trait_elaboration/src/elaboration.rs +++ b/charon/rustc_trait_elaboration/src/elaboration.rs @@ -242,7 +242,11 @@ impl<'tcx> PredicateSearcher<'tcx> { let item_bounds = item_bounds .iter_trait_clauses() // Substitute the item generics - .map(|(_, tref)| EarlyBinder::bind(tref).instantiate(tcx, args)) + .map(|(_, tref)| { + EarlyBinder::bind(tref) + .instantiate(tcx, args) + .skip_normalization() + }) .enumerate(); // Add all the bounds on the corresponding associated item. @@ -351,7 +355,7 @@ impl<'tcx> PredicateSearcher<'tcx> { .filter_map(|assoc| { let ty = Ty::new_projection(tcx, assoc.def_id, erased_tref.skip_binder().args); - let ty = crate::erase_and_norm(tcx, self.typing_env, ty); + let ty = crate::erase_and_norm(tcx, self.typing_env, Unnormalized::new(ty)); if let TyKind::Alias(alias_ty) = ty.kind() && alias_ty.kind.def_id() == assoc.def_id { @@ -489,7 +493,11 @@ impl<'tcx> PredicateSearcher<'tcx> { predicates .iter_trait_clauses() // Substitute the item generics - .map(|(_, trait_ref)| EarlyBinder::bind(trait_ref).instantiate(tcx, generics)) + .map(|(_, trait_ref)| { + EarlyBinder::bind(trait_ref) + .instantiate(tcx, generics) + .skip_normalization() + }) // Resolve .map(|trait_ref| self.resolve(&trait_ref)) .collect() diff --git a/charon/rustc_trait_elaboration/src/item_ref.rs b/charon/rustc_trait_elaboration/src/item_ref.rs index 5fbfe7cb0..0330969dc 100644 --- a/charon/rustc_trait_elaboration/src/item_ref.rs +++ b/charon/rustc_trait_elaboration/src/item_ref.rs @@ -77,7 +77,7 @@ impl<'tcx> PredicateSearcher<'tcx> { let tcx = self.elab_ctx.tcx; let typing_env = self.typing_env; // Normalize the generics. - let mut generics = normalize(tcx, typing_env, generics); + let mut generics = normalize(tcx, typing_env, ty::Unnormalized::new_wip(generics)); if tcx.is_typeck_child(def_id) { // Rustc gives closures/inline consts extra generic for inference that we don't care about. @@ -92,7 +92,9 @@ impl<'tcx> PredicateSearcher<'tcx> { let self_pred = self_predicate(tcx, tr_def_id); // Substitute to be in the context of the current item. let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id)); - let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics); + let self_pred = ty::EarlyBinder::bind(self_pred) + .instantiate(tcx, generics) + .skip_norm_wip(); let num_trait_req_clauses = ItemPredicates::required_recursively(elab_ctx, tr_def_id).len(); Some((self.resolve(&self_pred), num_trait_req_clauses)) diff --git a/charon/rustc_trait_elaboration/src/predicates.rs b/charon/rustc_trait_elaboration/src/predicates.rs index 0cd6ed12a..ca662dab1 100644 --- a/charon/rustc_trait_elaboration/src/predicates.rs +++ b/charon/rustc_trait_elaboration/src/predicates.rs @@ -390,7 +390,9 @@ impl<'tcx> ItemPredicates<'tcx> { /// Substitute all the predicates with these args. pub fn instantiate(mut self, tcx: TyCtxt<'tcx>, args: ty::GenericArgsRef<'tcx>) -> Self { for predicate in self.iter_mut() { - predicate.clause = ty::EarlyBinder::bind(predicate.clause).instantiate(tcx, args); + predicate.clause = ty::EarlyBinder::bind(predicate.clause) + .instantiate(tcx, args) + .skip_norm_wip(); } self } diff --git a/charon/rustc_trait_elaboration/src/utils.rs b/charon/rustc_trait_elaboration/src/utils.rs index d97742a33..07c93e779 100644 --- a/charon/rustc_trait_elaboration/src/utils.rs +++ b/charon/rustc_trait_elaboration/src/utils.rs @@ -29,20 +29,25 @@ use rustc_middle::ty::*; /// Normalize a value. -pub fn normalize<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, value: T) -> T +pub fn normalize<'tcx, T>( + tcx: TyCtxt<'tcx>, + typing_env: TypingEnv<'tcx>, + unnormalized: Unnormalized<'tcx, T>, +) -> T where T: TypeFoldable> + Clone, { use rustc_infer::infer::TyCtxtInferExt; use rustc_middle::traits::ObligationCause; use rustc_trait_selection::traits::query::normalize::QueryNormalizeExt; + let value = unnormalized.clone().skip_normalization(); let (infcx, param_env) = tcx.infer_ctxt().build_with_typing_env(typing_env); infcx .at(&ObligationCause::dummy(), param_env) - .query_normalize(value.clone()) + .query_normalize(value) // We ignore the generated outlives relations. Unsure what we should do with them. .map(|x| x.value) - .unwrap_or(value) + .unwrap_or(unnormalized.skip_normalization()) } /// Erase free regions from the given value. Largely copied from `tcx.erase_and_anonymize_regions`, but also @@ -92,14 +97,19 @@ where // Normalize and erase lifetimes, erasing more lifetimes than normal because we might be already // inside a binder and rustc doesn't like that. -pub fn erase_and_norm<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, x: T) -> T +pub fn erase_and_norm<'tcx, T>( + tcx: TyCtxt<'tcx>, + typing_env: TypingEnv<'tcx>, + x: Unnormalized<'tcx, T>, +) -> T where T: TypeFoldable> + Copy, { + let fallback = x.skip_normalization(); erase_free_regions( tcx, tcx.try_normalize_erasing_regions(typing_env, x) - .unwrap_or(x), + .unwrap_or(fallback), ) } @@ -115,7 +125,11 @@ pub fn normalize_bound_val<'tcx, T>( where T: TypeFoldable> + Copy, { - Binder::dummy(erase_and_norm(tcx, typing_env, x.skip_binder())) + Binder::dummy(erase_and_norm( + tcx, + typing_env, + Unnormalized::new_wip(x.skip_binder()), + )) } pub trait ToPolyTraitRef<'tcx> { diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index ffdd98dcd..3f90a7a31 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -28,7 +28,6 @@ fn run_compiler_with_callbacks( fn set_mir_options(config: &mut Config) { config.opts.unstable_opts.always_encode_mir = true; config.opts.unstable_opts.mir_opt_level = Some(0); - config.opts.unstable_opts.mir_emit_retag = true; config.opts.unstable_opts.mir_preserve_ub = true; let disabled_mir_passes = ["CheckAlignment"]; for pass in disabled_mir_passes { @@ -42,12 +41,14 @@ fn set_mir_options(config: &mut Config) { /// Enable rustc's parallel front-end. fn set_parallel_frontend(config: &mut Config) { - if config.opts.unstable_opts.threads <= 1 { + if config.opts.unstable_opts.threads.is_none_or(|t| t <= 1) { // Match rustc's `-Zthreads=0` behavior. const RUSTC_MAX_THREADS_CAP: usize = 256; - config.opts.unstable_opts.threads = std::thread::available_parallelism() - .map_or(1, |n| n.get()) - .min(RUSTC_MAX_THREADS_CAP); + config.opts.unstable_opts.threads = Some( + std::thread::available_parallelism() + .map_or(1, |n| n.get()) + .min(RUSTC_MAX_THREADS_CAP), + ); } } diff --git a/charon/src/bin/charon-driver/hax/constant_utils/uneval.rs b/charon/src/bin/charon-driver/hax/constant_utils/uneval.rs index 62da4652b..d913bf83a 100644 --- a/charon/src/bin/charon-driver/hax/constant_utils/uneval.rs +++ b/charon/src/bin/charon-driver/hax/constant_utils/uneval.rs @@ -109,6 +109,7 @@ pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>( .ok()? .ok()?; let ty = tcx.type_of(uv.def).instantiate(tcx, uv.args); + let ty = normalize(tcx, typing_env, ty); Some(ty::Const::new_value(tcx, val, ty)) } @@ -172,7 +173,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( ty: rustc_middle::ty::Ty<'tcx>, span: rustc_span::Span, ) -> ConstantExpr { - let ty = normalize(s.base().tcx, s.typing_env(), ty); + let ty = normalize(s.base().tcx, s.typing_env(), ty::Unnormalized::new_wip(ty)); let kind = match (&*valtree, ty.kind()) { (_, ty::Ref(_, inner_ty, _)) => { diff --git a/charon/src/bin/charon-driver/hax/rustc_utils.rs b/charon/src/bin/charon-driver/hax/rustc_utils.rs index 977e1ee0a..88c215526 100644 --- a/charon/src/bin/charon-driver/hax/rustc_utils.rs +++ b/charon/src/bin/charon-driver/hax/rustc_utils.rs @@ -17,7 +17,7 @@ where T: ty::TypeFoldable> + Clone, { match args { - None => x.instantiate_identity(), + None => x.instantiate_identity().skip_normalization(), Some(args) => normalize(tcx, typing_env, x.instantiate(tcx, args)), } } @@ -51,7 +51,9 @@ impl<'tcx, T: ty::TypeFoldable>> ty::Binder<'tcx, T> { tcx: ty::TyCtxt<'tcx>, generics: &[ty::GenericArg<'tcx>], ) -> ty::Binder<'tcx, T> { - ty::EarlyBinder::bind(self).instantiate(tcx, generics) + ty::EarlyBinder::bind(self) + .instantiate(tcx, generics) + .skip_normalization() } } @@ -173,10 +175,12 @@ pub fn get_method_sig<'tcx>( let implemented_trait_ref = tcx .impl_trait_ref(impl_def_id) .instantiate(tcx, method_args); + let implemented_trait_ref = normalize(tcx, typing_env, implemented_trait_ref); // Construct arguments for the declared method generics in the context of the implemented // method generics. let decl_args = method_args.rebase_onto(tcx, impl_def_id, implemented_trait_ref.args); - let mut sig = declared_sig.instantiate(tcx, decl_args); + let sig = declared_sig.instantiate(tcx, decl_args); + let sig = normalize(tcx, typing_env, sig); if let container_named_lts = tcx .generics_of(impl_def_id) @@ -195,9 +199,10 @@ pub fn get_method_sig<'tcx>( { // Avoids using the same lifetime name twice in the same scope (once in impl parameters, // second in the method declaration late-bound vars). - sig = tcx.anonymize_bound_vars(sig); + tcx.anonymize_bound_vars(sig) + } else { + sig } - normalize(tcx, typing_env, sig) } /// Generates a list of `::Ty` type aliases for each non-gat associated type of the @@ -231,7 +236,7 @@ pub fn assoc_tys_for_trait<'tcx>( .iter_instantiated(tcx, tref.args) { if let Some(pred) = clause.as_trait_clause() { - let tref = erase_and_norm(tcx, typing_env, pred.skip_binder().trait_ref); + let tref = erase_and_norm(tcx, typing_env, pred.map(|b| b.skip_binder().trait_ref)); gather_assoc_tys(tcx, typing_env, assoc_tys, tref); } } @@ -278,7 +283,7 @@ pub fn dyn_self_ty<'tcx>( tcx.mk_poly_existential_predicates(&preds) }; let ty = tcx.mk_ty_from_kind(ty::Dynamic(preds, re_erased)); - let ty = normalize(tcx, typing_env, ty); + let ty = normalize(tcx, typing_env, ty::Unnormalized::new_wip(ty)); Some(ty) } @@ -296,7 +301,9 @@ pub fn closure_once_shim<'tcx>( ty::ClosureKind::FnOnce => return None, }; let mir = tcx.instance_mir(instance.def).clone(); - let mir = ty::EarlyBinder::bind(mir).instantiate(tcx, instance.args); + let mir = ty::EarlyBinder::bind(mir) + .instantiate(tcx, instance.args) + .skip_normalization(); Some(mir) } @@ -306,12 +313,11 @@ pub fn drop_glue_shim<'tcx>( instantiate: Option>, ) -> mir::Body<'tcx> { let tcx = s.base().tcx; - let drop_in_place = - tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, rustc_span::DUMMY_SP); + let drop_in_place = tcx.require_lang_item(rustc_hir::LangItem::DropGlue, rustc_span::DUMMY_SP); let ty = def_id.type_of(s); let ty = match instantiate { - None => ty.instantiate_identity(), - Some(args) => ty.instantiate(tcx, args), + None => ty.instantiate_identity().skip_normalization(), + Some(args) => ty.instantiate(tcx, args).skip_normalization(), }; let instance_kind = ty::InstanceKind::DropGlue(drop_in_place, Some(ty)); tcx.instance_mir(instance_kind).clone() diff --git a/charon/src/bin/charon-driver/hax/traits.rs b/charon/src/bin/charon-driver/hax/traits.rs index ce5d05a7a..be1944fcd 100644 --- a/charon/src/bin/charon-driver/hax/traits.rs +++ b/charon/src/bin/charon-driver/hax/traits.rs @@ -144,8 +144,11 @@ pub fn super_clause_to_clause_and_trait_proof<'tcx, S: UnderOwnerState<'tcx>>( ) { return None; } - let impl_trait_ref = - rustc_middle::ty::Binder::dummy(tcx.impl_trait_ref(impl_did).instantiate_identity()); + let impl_trait_ref = rustc_middle::ty::Binder::dummy( + tcx.impl_trait_ref(impl_did) + .instantiate_identity() + .skip_normalization(), + ); let new_clause = clause.instantiate_supertrait(tcx, impl_trait_ref); let trait_proof = solve_trait( s, @@ -227,7 +230,9 @@ pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>( let self_pred = self_predicate(tcx, tr_def_id); // Substitute to be in the context of the current item. let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id)); - let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics); + let self_pred = ty::EarlyBinder::bind(self_pred) + .instantiate(tcx, generics) + .skip_normalization(); // Resolve Some(solve_trait(s, self_pred)) diff --git a/charon/src/bin/charon-driver/hax/types/def_id.rs b/charon/src/bin/charon-driver/hax/types/def_id.rs index f657a3c1a..cb028715d 100644 --- a/charon/src/bin/charon-driver/hax/types/def_id.rs +++ b/charon/src/bin/charon-driver/hax/types/def_id.rs @@ -165,7 +165,8 @@ impl VirtualImplAssocItem { let tcx = s.base().tcx; let impl_trait_ref = tcx .impl_trait_ref(self.trait_impl_id) - .instantiate_identity(); + .instantiate_identity() + .skip_normalization(); self.args_for_item_decl(s, impl_trait_ref.args) } } @@ -483,7 +484,7 @@ impl DefId { let item_predicates = tcx .predicates_of(id.item_decl_id) .instantiate_own(tcx, item_args) - .map(|(predicate, _)| predicate); + .map(|(predicate, _)| predicate.skip_normalization()); param_env_from_clauses(tcx, impl_predicates.chain(item_predicates)) } DefIdBase::Real(def_id) diff --git a/charon/src/bin/charon-driver/hax/types/new/item_ref.rs b/charon/src/bin/charon-driver/hax/types/new/item_ref.rs index 99d4d34fe..41be572af 100644 --- a/charon/src/bin/charon-driver/hax/types/new/item_ref.rs +++ b/charon/src/bin/charon-driver/hax/types/new/item_ref.rs @@ -219,7 +219,7 @@ impl ItemRef { rustc_utils::assoc_tys_for_trait(tcx, typing_env, tref) .into_iter() .map(|alias_ty| ty::Ty::new_alias(tcx, alias_ty)) - .map(|ty| normalize(tcx, typing_env, ty)) + .map(|ty| normalize(tcx, typing_env, ty::Unnormalized::new(ty))) .map(|ty| ty.sinto(s)) .collect() } @@ -227,7 +227,11 @@ impl ItemRef { /// Erase lifetimes from the generic arguments of this item. pub fn erase<'tcx, S: UnderOwnerState<'tcx>>(&self, s: &S) -> Self { let args = self.rustc_args(s); - let args = erase_and_norm(s.base().tcx, s.typing_env(), args); + let args = erase_and_norm( + s.base().tcx, + s.typing_env(), + ty::Unnormalized::new_wip(args), + ); Self::translate_from_hax_def_id(s, self.def_id.clone(), args) } diff --git a/charon/src/bin/charon-driver/hax/types/new/synthetic_items.rs b/charon/src/bin/charon-driver/hax/types/new/synthetic_items.rs index eda961e1d..7f8cba9f3 100644 --- a/charon/src/bin/charon-driver/hax/types/new/synthetic_items.rs +++ b/charon/src/bin/charon-driver/hax/types/new/synthetic_items.rs @@ -1,7 +1,7 @@ use crate::hax::prelude::*; use { - rustc_hir::definitions::DisambiguatorState, + rustc_hir::definitions::PerParentDisambiguatorState, rustc_middle::ty, rustc_span::{DUMMY_SP, Symbol, def_id::DefId as RDefId}, rustc_type_ir::Upcast, @@ -42,8 +42,7 @@ impl<'tcx> GlobalCache<'tcx> { return *def_id; } let tcx = s.base().tcx; - let mut disambiguator_state = DisambiguatorState::new(); - + let mut disambiguator_state = PerParentDisambiguatorState::default(); let name = &item.name(); // Create a fake item, to which we'll assign generics and a param_env, which we can // then use to generate the `FullDefKind` we want. diff --git a/charon/src/bin/charon-driver/hax/types/ty.rs b/charon/src/bin/charon-driver/hax/types/ty.rs index e853e7455..470ed2ff4 100644 --- a/charon/src/bin/charon-driver/hax/types/ty.rs +++ b/charon/src/bin/charon-driver/hax/types/ty.rs @@ -266,7 +266,7 @@ impl FieldDef { instantiate: ty::GenericArgsRef<'tcx>, ) -> FieldDef { let tcx = s.base().tcx; - let ty = fdef.ty(tcx, instantiate).sinto(s); + let ty = normalize(tcx, s.typing_env(), fdef.ty(tcx, instantiate)).sinto(s); let name = { let name = fdef.name.sinto(s); let is_user_provided = { @@ -551,7 +551,9 @@ pub struct GenericParamDef { ty::GenericParamDefKind::Lifetime => GenericParamDefKind::Lifetime, ty::GenericParamDefKind::Type { has_default, synthetic } => GenericParamDefKind::Type { has_default, synthetic }, ty::GenericParamDefKind::Const { has_default, .. } => { - let ty = s.base().tcx.type_of(self.def_id).instantiate_identity().sinto(s); + let tcx = s.base().tcx; + let ty = tcx.type_of(self.def_id).instantiate_identity(); + let ty = normalize(tcx, s.typing_env(), ty).sinto(s); GenericParamDefKind::Const { has_default, ty } }, } @@ -629,7 +631,7 @@ impl Alias { // Try to normalize the alias first. let ty = ty::Ty::new_alias(tcx, *alias_ty); - let ty = crate::hax::traits::normalize(tcx, typing_env, ty); + let ty = normalize(tcx, typing_env, ty::Unnormalized::new(ty)); let ty::Alias(alias_ty) = ty.kind() else { let ty: Ty = ty.sinto(s); return ty.kind().clone(); @@ -643,6 +645,7 @@ impl Alias { RustAliasKind::Opaque { def_id } => { // Reveal the underlying `impl Trait` type. let ty = tcx.type_of(def_id).instantiate(tcx, alias_ty.args); + let ty = normalize(tcx, s.typing_env(), ty); AliasKind::Opaque { hidden_ty: ty.sinto(s), } @@ -711,7 +714,7 @@ pub enum TyKind { let item = translate_item_ref(s, *fun_id, generics); let tcx = s.base().tcx; let fn_sig = tcx.fn_sig(*fun_id).instantiate(tcx, generics); - let fn_sig = Box::new(fn_sig.sinto(s)); + let fn_sig = Box::new(normalize(tcx, s.typing_env(), fn_sig).sinto(s)); TyKind::FnDef { item, fn_sig } }, )] @@ -723,11 +726,10 @@ pub enum TyKind { #[custom_arm( ty::TyKind::FnPtr(tys, header) => { + let fn_sig_kind = ty::FnSigKind::new(header.abi(), header.safety(), header.c_variadic()); let sig = tys.map_bound(|tys| ty::FnSig { inputs_and_output: tys.inputs_and_output, - c_variadic: header.c_variadic, - safety: header.safety, - abi: header.abi, + fn_sig_kind, }); TyKind::Arrow(Box::new(sig.sinto(s))) }, @@ -1060,8 +1062,11 @@ pub struct TyFnSig { pub inputs: Vec, #[value(self.output().sinto(s))] pub output: Ty, + #[value(self.c_variadic())] pub c_variadic: bool, + #[value(self.safety())] pub safety: Safety, + #[value(self.abi())] pub abi: ExternAbi, } @@ -1567,6 +1572,7 @@ impl AssocItem { let implemented_trait_ref = tcx .impl_trait_ref(container_id) .instantiate(tcx, container_args); + let implemented_trait_ref = normalize(tcx, s.typing_env(), implemented_trait_ref); let implemented_trait_item = { let implemented_item_id = implemented_item_id.sinto(s); let generics = diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 6ae7ba082..138805aae 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -917,7 +917,7 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { tgt_ty: &Ty, ) -> Result { match rvalue { - mir::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)), + mir::Rvalue::Use(operand, _) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)), mir::Rvalue::CopyForDeref(place) => { // According to the documentation, it seems to be an optimisation // for drop elaboration. We treat it as a regular copy. @@ -1148,6 +1148,13 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { "charon does not support unsafe lifetime binders" ); } + mir::Rvalue::Reborrow(..) => { + raise_error!( + self, + span, + "charon does not support reborrow rvalues (for Reborrow traits)" + ); + } } } @@ -1216,8 +1223,6 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { Some(StatementKind::PlaceMention(place)) } } - // This is for the stacked borrows memory model. - mir::StatementKind::Retag(_, _) => None, // These two are only there to make borrow-checking accept less code, and are removed // in later MIRs. mir::StatementKind::FakeRead(..) => None, @@ -1287,7 +1292,6 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { destination, target, unwind, - fn_span: _, .. } => self.translate_function_call(span, func, args, destination, target, unwind)?, TerminatorKind::Assert { diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index a12d03f69..97ca285fb 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -31,7 +31,6 @@ impl<'tcx> TranslateCtx<'tcx> { SolverTraitLangItem::AsyncFnKindHelper => return None, SolverTraitLangItem::AsyncFnMut => BuiltinImplData::AsyncFnMut, SolverTraitLangItem::AsyncFnOnce => BuiltinImplData::AsyncFnOnce, - SolverTraitLangItem::AsyncFnOnceOutput => return None, SolverTraitLangItem::AsyncIterator => return None, SolverTraitLangItem::BikeshedGuaranteedNoDrop => return None, SolverTraitLangItem::Clone => BuiltinImplData::Clone, diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 0ccf877ac..35bef6ea7 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -443,6 +443,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .def_id .type_of(hax_state) .instantiate(tcx, item.rustc_args(hax_state)); + let ty = hax::normalize(tcx, ty_env, ty); // Get the tail type, which determines the metadata of `ty`. let tail_ty = tcx.struct_tail_raw( @@ -503,10 +504,26 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { use rustc_abi as r_abi; fn translate_variant_layout( - variant_layout: &r_abi::LayoutData, + variant_layout: &r_abi::VariantLayout, tagger: Vec<(ByteCount, ScalarValue)>, ) -> Option { - let field_offsets = match &variant_layout.fields { + let field_offsets = variant_layout + .field_offsets + .iter() + .map(|o| o.bytes()) + .collect(); + Some(VariantLayout { + field_offsets, + uninhabited: variant_layout.is_uninhabited(), + tagger, + }) + } + + fn translate_layout_data( + layout_data: &r_abi::LayoutData, + tagger: Vec<(ByteCount, ScalarValue)>, + ) -> Option { + let field_offsets = match &layout_data.fields { r_abi::FieldsShape::Arbitrary { offsets, .. } => { offsets.iter().map(|o| o.bytes()).collect() } @@ -516,7 +533,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { }; Some(VariantLayout { field_offsets, - uninhabited: variant_layout.is_uninhabited(), + uninhabited: layout_data.is_uninhabited(), tagger, }) } @@ -549,6 +566,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .def_id .type_of(hax_state) .instantiate(tcx, item.rustc_args(hax_state)); + let ty = hax::normalize(tcx, ty_env, ty); let pseudo_input = ty_env.as_query_input(ty); let ptr_size = self.translated.the_target_information().target_pointer_size; @@ -629,8 +647,8 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .. } => { if niche_variants.contains(untagged_variant) - && let Some(start) = tag_for_variant(*niche_variants.start()) - && let Some(end) = tag_for_variant(*niche_variants.end()) + && let Some(start) = tag_for_variant(niche_variants.start) + && let Some(end) = tag_for_variant(niche_variants.last) { // Add an inner discriminator; the outer one filters the whole range of // values considered to be discriminants, the inner one selects known @@ -669,11 +687,11 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { }; let mut variant_layouts: IndexVec> = (0..n_variants).map(|_| None).collect(); - variant_layouts[variant_id] = translate_variant_layout(&layout, vec![]); + variant_layouts[variant_id] = translate_layout_data(&layout, vec![]); variant_layouts } r_abi::FieldsShape::Union(_) => { - vec![translate_variant_layout(&layout, vec![])].into() + vec![translate_layout_data(&layout, vec![])].into() } r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Array { .. } => { vec![].into() diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 1a7b47c14..3d03cc119 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -65,7 +65,7 @@ pub trait AstFormatter: Sized { { write!(f, "{name}") } else { - write!(f, "{}", &method_id.to_pretty_string()) + write!(f, "{}", method_id.to_pretty_string()) } } fn format_assoc_type_name( @@ -80,7 +80,7 @@ pub trait AstFormatter: Sized { { write!(f, "{name}") } else { - write!(f, "{}", &type_id.to_pretty_string()) + write!(f, "{}", type_id.to_pretty_string()) } } fn format_assoc_const_name( @@ -95,7 +95,7 @@ pub trait AstFormatter: Sized { { write!(f, "{name}") } else { - write!(f, "{}", &const_id.to_pretty_string()) + write!(f, "{}", const_id.to_pretty_string()) } } fn format_enum_variant_name( diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 9c361b766..cad4620ea 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -91,6 +91,13 @@ where Some(T), } +// Full name: core::ptr::drop_glue +#[lang_item("drop_glue")] +unsafe fn drop_glue<'_0, T>(_1: &'_0 mut T) +where + TraitClause0: (T: Destruct), += + // Full name: core::slice::index::private_slice_index::Sealed pub trait Sealed { @@ -256,54 +263,70 @@ where TraitClause0: (T: Sized), = -// Full name: test_crate::::{impl Destruct for [T; N]}::drop_in_place -unsafe fn {impl Destruct for [T; N]}::drop_in_place(_1: *mut [T; N]) +// Full name: test_crate::::{impl Destruct for [T]}::drop_in_place +unsafe fn {impl Destruct for [T]}::drop_in_place(_1: *mut [T]) where TraitClause0: (T: Sized), { let _0: (); // return - let _1: *mut [T; N]; // arg #1 - let _2: &'1 mut [T; N]; // anonymous local - let _3: *mut [T; N]; // anonymous local - let _4: *mut [T]; // anonymous local - let _5: usize; // anonymous local - let _6: usize; // anonymous local - let _7: *mut T; // anonymous local - let _8: bool; // anonymous local - let _9: &'_ mut [T]; // anonymous local - let _10: &'_ mut T; // anonymous local + let _1: &'1 mut [T]; // arg #1 + let _2: usize; // anonymous local + let _3: usize; // anonymous local + let _4: *mut T; // anonymous local + let _5: bool; // anonymous local + let _6: &'_ mut [T]; // anonymous local + let _7: &'_ mut T; // anonymous local storage_live(_2) storage_live(_3) storage_live(_4) storage_live(_5) - storage_live(_6) - storage_live(_7) - storage_live(_8) _0 = () - _2 = &mut (*_1) - _3 = &raw mut (*_2) - _4 = unsize_cast<*mut [T; N], *mut [T], N>(move _3) - _5 = copy _4.metadata - _6 = const 0 : usize + _2 = copy _1.metadata + _3 = const 0 : usize loop { - _8 = copy _6 == copy _5 - if move _8 { + _5 = copy _3 == copy _2 + if move _5 { break 0 } else { - storage_live(_9) - _9 = &mut (*_4) with_metadata(copy _4.metadata) - storage_live(_10) - _10 = @SliceIndexMut<'_, T>(move _9, copy _6) - _7 = &raw mut (*_10) - _6 = move _6 wrap.+ const 1 : usize - drop[{built_in impl Destruct for T}::drop_in_place] (*_7) + storage_live(_6) + _6 = &mut (*_1) with_metadata(copy _1.metadata) + storage_live(_7) + _7 = @SliceIndexMut<'_, T>(move _6, copy _3) + _4 = &raw mut (*_7) + _3 = move _3 wrap.+ const 1 : usize + drop[{built_in impl Destruct for T}::drop_in_place] (*_4) continue 0 } } return } +// Full name: test_crate::::{impl Destruct for [T]} +impl Destruct for [T] +where + TraitClause0: (T: Sized), +{ + fn drop_in_place = {impl Destruct for [T]}::drop_in_place[TraitClause0] + non-dyn-compatible +} + +// Full name: test_crate::::{impl Destruct for [T; N]}::drop_in_place +unsafe fn {impl Destruct for [T; N]}::drop_in_place(_1: *mut [T; N]) +where + TraitClause0: (T: Sized), +{ + let _0: (); // return + let _1: &'1 mut [T; N]; // arg #1 + let _2: &'3 mut [T]; // anonymous local + + storage_live(_2) + _0 = () + _2 = @ArrayToSliceMut<'_, T, N>(move _1) + _0 = drop_glue<'6, [T]>[{impl Destruct for [T]}[TraitClause0]](move _2) + return +} + // Full name: test_crate::::{impl Destruct for [T; N]} impl Destruct for [T; N] where diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index bee6796f9..e2f1a75de 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -140,13 +140,10 @@ where unsafe fn {impl Destruct for (A,)}::drop_in_place(_1: *mut (A,)) { let _0: (); // return - let _1: *mut (A,); // arg #1 - let _2: &'1 mut (A,); // anonymous local + let _1: &'1 mut (A,); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - drop[{built_in impl Destruct for A}::drop_in_place] (*_2).0 + drop[{built_in impl Destruct for A}::drop_in_place] (*_1).0 return } diff --git a/charon/tests/ui/desugar_drops_to_calls.out b/charon/tests/ui/desugar_drops_to_calls.out index dcd289670..de6713e2f 100644 --- a/charon/tests/ui/desugar_drops_to_calls.out +++ b/charon/tests/ui/desugar_drops_to_calls.out @@ -193,30 +193,27 @@ pub fn {impl Drop for Point}::drop<'_0>(self_1: &'_0 mut Point) unsafe fn {impl Destruct for Point}::drop_in_place(_1: *mut Point) { let _0: (); // return - let _1: *mut Point; // arg #1 - let _2: &'1 mut Point; // anonymous local - let _3: &'2 mut Point; // anonymous local - let _4: (); // anonymous local - let drop_arg_5: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local - let drop_ret_6: (); // local - let drop_arg_7: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local - let drop_ret_8: (); // local + let _1: &'1 mut Point; // arg #1 + let _2: &'2 mut Point; // anonymous local + let _3: (); // anonymous local + let drop_arg_4: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local + let drop_ret_5: (); // local + let drop_arg_6: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local + let drop_ret_7: (); // local storage_live(_2) storage_live(_3) - storage_live(_4) _0 = () _2 = &mut (*_1) - _3 = &mut (*_2) - _4 = {impl Drop for Point}::drop<'4>(move _3) - storage_live(drop_arg_5) - drop_arg_5 = &raw mut ((*_2)).x - storage_live(drop_ret_6) - drop_ret_6 = {impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}](move drop_arg_5) - storage_live(drop_arg_7) - drop_arg_7 = &raw mut ((*_2)).y - storage_live(drop_ret_8) - drop_ret_8 = {impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}](move drop_arg_7) + _3 = {impl Drop for Point}::drop<'4>(move _2) + storage_live(drop_arg_4) + drop_arg_4 = &raw mut ((*_1)).x + storage_live(drop_ret_5) + drop_ret_5 = {impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}](move drop_arg_4) + storage_live(drop_arg_6) + drop_arg_6 = &raw mut ((*_1)).y + storage_live(drop_ret_7) + drop_ret_7 = {impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}](move drop_arg_6) return } diff --git a/charon/tests/ui/desugar_drops_to_calls_mono.out b/charon/tests/ui/desugar_drops_to_calls_mono.out index 2e9f068de..1fa7d0b04 100644 --- a/charon/tests/ui/desugar_drops_to_calls_mono.out +++ b/charon/tests/ui/desugar_drops_to_calls_mono.out @@ -164,30 +164,27 @@ pub fn drop<'_0>(self_1: &'_0 mut Point) unsafe fn {impl Destruct for Point}::drop_in_place(_1: *mut Point) { let _0: (); // return - let _1: *mut Point; // arg #1 - let _2: &'1 mut Point; // anonymous local - let _3: &'2 mut Point; // anonymous local - let _4: (); // anonymous local - let drop_arg_5: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local - let drop_ret_6: (); // local - let drop_arg_7: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local - let drop_ret_8: (); // local + let _1: &'1 mut Point; // arg #1 + let _2: &'2 mut Point; // anonymous local + let _3: (); // anonymous local + let drop_arg_4: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local + let drop_ret_5: (); // local + let drop_arg_6: *mut alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]; // local + let drop_ret_7: (); // local storage_live(_2) storage_live(_3) - storage_live(_4) _0 = () _2 = &mut (*_1) - _3 = &mut (*_2) - _4 = drop<'4>(move _3) - storage_live(drop_arg_5) - drop_arg_5 = &raw mut ((*_2)).x - storage_live(drop_ret_6) - drop_ret_6 = {impl Destruct for alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]}::drop_in_place(move drop_arg_5) - storage_live(drop_arg_7) - drop_arg_7 = &raw mut ((*_2)).y - storage_live(drop_ret_8) - drop_ret_8 = {impl Destruct for alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]}::drop_in_place(move drop_arg_7) + _3 = drop<'4>(move _2) + storage_live(drop_arg_4) + drop_arg_4 = &raw mut ((*_1)).x + storage_live(drop_ret_5) + drop_ret_5 = {impl Destruct for alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]}::drop_in_place(move drop_arg_4) + storage_live(drop_arg_6) + drop_arg_6 = &raw mut ((*_1)).y + storage_live(drop_ret_7) + drop_ret_7 = {impl Destruct for alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]}::drop_in_place(move drop_arg_6) return } diff --git a/charon/tests/ui/drop_after_overflow.out b/charon/tests/ui/drop_after_overflow.out index 5715814c4..6ea9eb0b0 100644 --- a/charon/tests/ui/drop_after_overflow.out +++ b/charon/tests/ui/drop_after_overflow.out @@ -79,19 +79,16 @@ pub fn {impl Drop for Foo}::drop<'_0>(self_1: &'_0 mut Foo) unsafe fn {impl Destruct for Foo}::drop_in_place(_1: *mut Foo) { let _0: (); // return - let _1: *mut Foo; // arg #1 - let _2: &'1 mut Foo; // anonymous local - let _3: &'2 mut Foo; // anonymous local - let _4: (); // anonymous local + let _1: &'1 mut Foo; // arg #1 + let _2: &'2 mut Foo; // anonymous local + let _3: (); // anonymous local bb0: { storage_live(_2); storage_live(_3); - storage_live(_4); _0 = (); _2 = &mut (*_1); - _3 = &mut (*_2); - _4 = {impl Drop for Foo}::drop<'4>(move _3) -> bb2 (unwind: bb1); + _3 = {impl Drop for Foo}::drop<'4>(move _2) -> bb2 (unwind: bb1); } bb1: { diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index bff213d72..f427135a0 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -66,10 +66,10 @@ where struct test_crate::Left::{vtable} { size: usize, align: usize, - drop: unsafe fn(*mut (dyn Left)), - method_left_method: fn<'_0_1>(&'_0_1 (dyn Left)) -> Ty1, + drop: unsafe fn(*mut (dyn Left)), + method_left_method: fn<'_0_1>(&'_0_1 (dyn Left)) -> Ty0, super_trait_0: &'static core::marker::MetaSized::{vtable}, - super_trait_1: &'static test_crate::Internal::{vtable}, + super_trait_1: &'static test_crate::Internal::{vtable}, } // Full name: test_crate::Left @@ -119,11 +119,11 @@ where struct test_crate::Join::{vtable} { size: usize, align: usize, - drop: unsafe fn(*mut (dyn Join)), - method_join_method: fn<'_0_1>(&'_0_1 (dyn Join)) -> (Ty3, Ty2), + drop: unsafe fn(*mut (dyn Join)), + method_join_method: fn<'_0_1>(&'_0_1 (dyn Join)) -> (Ty0, Ty3), super_trait_0: &'static core::marker::MetaSized::{vtable}, - super_trait_1: &'static test_crate::Left::{vtable}, - super_trait_2: &'static test_crate::Right::{vtable}, + super_trait_1: &'static test_crate::Left::{vtable}, + super_trait_2: &'static test_crate::Right::{vtable}, } // Full name: test_crate::Join @@ -302,28 +302,28 @@ fn {impl Left for i32}::left_method<'_0>(self_1: &'_0 i32) -> i32 } // Full name: test_crate::{impl Left for i32}::left_method::{vtable_method} -fn {impl Left for i32}::left_method::{vtable_method}<'_0>(_1: &'_0 (dyn Left)) -> i32 +fn {impl Left for i32}::left_method::{vtable_method}<'_0>(_1: &'_0 (dyn Left)) -> i32 { let _0: i32; // return - let _1: &'_0 (dyn Left + '0); // arg #1 + let _1: &'_0 (dyn Left + '0); // arg #1 let _2: &'_0 i32; // anonymous local storage_live(_2) - _2 = concretize<&'_0 (dyn Left + '1), &'_0 i32>(move _1) + _2 = concretize<&'_0 (dyn Left + '1), &'_0 i32>(move _1) _0 = {impl Left for i32}::left_method<'_0>(move _2) return } // Full name: test_crate::{impl Left for i32}::{vtable_drop_shim} -unsafe fn {impl Left for i32}::{vtable_drop_shim}(dyn_self_1: *mut (dyn Left)) +unsafe fn {impl Left for i32}::{vtable_drop_shim}(dyn_self_1: *mut (dyn Left)) { let ret_0: (); // return - let dyn_self_1: *mut (dyn Left + '0); // arg #1 + let dyn_self_1: *mut (dyn Left + '0); // arg #1 let target_self_2: *mut i32; // local ret_0 = () storage_live(target_self_2) - target_self_2 = concretize<*mut (dyn Left + '1), *mut i32>(move dyn_self_1) + target_self_2 = concretize<*mut (dyn Left + '1), *mut i32>(move dyn_self_1) return } @@ -494,28 +494,28 @@ fn {impl Join for i32}::join_method<'_0>(self_1: &'_0 i32) -> (i32, i32) } // Full name: test_crate::{impl Join for i32}::join_method::{vtable_method} -fn {impl Join for i32}::join_method::{vtable_method}<'_0>(_1: &'_0 (dyn Join)) -> (i32, i32) +fn {impl Join for i32}::join_method::{vtable_method}<'_0>(_1: &'_0 (dyn Join)) -> (i32, i32) { let _0: (i32, i32); // return - let _1: &'_0 (dyn Join + '0); // arg #1 + let _1: &'_0 (dyn Join + '0); // arg #1 let _2: &'_0 i32; // anonymous local storage_live(_2) - _2 = concretize<&'_0 (dyn Join + '1), &'_0 i32>(move _1) + _2 = concretize<&'_0 (dyn Join + '1), &'_0 i32>(move _1) _0 = {impl Join for i32}::join_method<'_0>(move _2) return } // Full name: test_crate::{impl Join for i32}::{vtable_drop_shim} -unsafe fn {impl Join for i32}::{vtable_drop_shim}(dyn_self_1: *mut (dyn Join)) +unsafe fn {impl Join for i32}::{vtable_drop_shim}(dyn_self_1: *mut (dyn Join)) { let ret_0: (); // return - let dyn_self_1: *mut (dyn Join + '0); // arg #1 + let dyn_self_1: *mut (dyn Join + '0); // arg #1 let target_self_2: *mut i32; // local ret_0 = () storage_live(target_self_2) - target_self_2 = concretize<*mut (dyn Join + '1), *mut i32>(move dyn_self_1) + target_self_2 = concretize<*mut (dyn Join + '1), *mut i32>(move dyn_self_1) return } @@ -557,11 +557,11 @@ impl Join for i32 { fn main() { let _0: (); // return - let v_1: &'3 (dyn Join + '4); // local + let v_1: &'3 (dyn Join + '4); // local let _2: &'6 i32; // anonymous local let _3: &'7 i32; // anonymous local let _4: (i32, i32); // anonymous local - let _5: &'8 (dyn Join + '9); // anonymous local + let _5: &'8 (dyn Join + '9); // anonymous local let _6: &'10 i32; // anonymous local let _7: &'11 i32; // anonymous local let _8: &'19 i32; // anonymous local @@ -581,7 +581,7 @@ fn main() _6 = move _7 _3 = &(*_6) _2 = &(*_3) - v_1 = unsize_cast<&'6 i32, &'12 (dyn Join + '13), &{impl Join for i32}::{vtable}>(move _2) + v_1 = unsize_cast<&'6 i32, &'12 (dyn Join + '13), &{impl Join for i32}::{vtable}>(move _2) storage_dead(_2) storage_dead(_3) storage_live(_4) diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index 29ac4fb82..43ba9c564 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -74,13 +74,10 @@ struct Foo { unsafe fn {impl Destruct for Foo}::drop_in_place(_1: *mut Foo) { let _0: (); // return - let _1: *mut Foo; // arg #1 - let _2: &'1 mut Foo; // anonymous local + let _1: &'1 mut Foo; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - drop[{impl Destruct for String}::drop_in_place] ((*_2)).1 + drop[{impl Destruct for String}::drop_in_place] ((*_1)).1 return } diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index 37d2b84c4..ec9ef16b6 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -249,12 +249,9 @@ fn main() unsafe fn {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1>(_1: *mut closure<'_0, '_1>) { let _0: (); // return - let _1: *mut closure<'_0, '_1>; // arg #1 - let _2: &'1 mut closure<'_0, '_1>; // anonymous local + let _1: &'1 mut closure<'_0, '_1>; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 8bb15b636..1fdcdcb49 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -111,12 +111,9 @@ fn main() unsafe fn {impl Destruct for closure}::drop_in_place(_1: *mut closure) { let _0: (); // return - let _1: *mut closure; // arg #1 - let _2: &'1 mut closure; // anonymous local + let _1: &'1 mut closure; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index f7a2213a4..2f44a06c1 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -281,12 +281,9 @@ fn main() unsafe fn {impl Destruct for test_crate::main::closure<'_0>}::drop_in_place<'_0>(_1: *mut test_crate::main::closure<'_0>) { let _0: (); // return - let _1: *mut test_crate::main::closure<'_0>; // arg #1 - let _2: &'1 mut test_crate::main::closure<'_0>; // anonymous local + let _1: &'1 mut test_crate::main::closure<'_0>; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } @@ -294,12 +291,9 @@ unsafe fn {impl Destruct for test_crate::main::closure<'_0>}::drop_in_place<'_0> unsafe fn {impl Destruct for test_crate::main::closure#1<'_0>}::drop_in_place<'_0>(_1: *mut test_crate::main::closure#1<'_0>) { let _0: (); // return - let _1: *mut test_crate::main::closure#1<'_0>; // arg #1 - let _2: &'1 mut test_crate::main::closure#1<'_0>; // anonymous local + let _1: &'1 mut test_crate::main::closure#1<'_0>; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } @@ -307,12 +301,9 @@ unsafe fn {impl Destruct for test_crate::main::closure#1<'_0>}::drop_in_place<'_ unsafe fn {impl Destruct for test_crate::main::closure#2}::drop_in_place(_1: *mut test_crate::main::closure#2) { let _0: (); // return - let _1: *mut test_crate::main::closure#2; // arg #1 - let _2: &'1 mut test_crate::main::closure#2; // anonymous local + let _1: &'1 mut test_crate::main::closure#2; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out index 2b0cccccb..43e0e3ed9 100644 --- a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out +++ b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out @@ -175,12 +175,9 @@ impl Fn<((),)> for closure::<()> { unsafe fn {impl Destruct for closure::<()>}::drop_in_place::<()>(_1: *mut closure::<()>) { let _0: (); // return - let _1: *mut closure::<()>; // arg #1 - let _2: &'1 mut closure::<()>; // anonymous local + let _1: &'1 mut closure::<()>; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/ptr-offset.out b/charon/tests/ui/ptr-offset.out index 4bac2c046..d20930a54 100644 --- a/charon/tests/ui/ptr-offset.out +++ b/charon/tests/ui/ptr-offset.out @@ -189,7 +189,6 @@ fn precondition_check(this_1: *const (), count_2: isize, size_3: usize) storage_live(rhs_8) rhs_8 = cast(copy size_3) storage_live(b_11) - storage_live(_10) storage_live(_12) storage_live(_13) _13 = cast(copy count_2) @@ -198,6 +197,7 @@ fn precondition_check(this_1: *const (), count_2: isize, size_3: usize) _12 = move _13 checked.* move _14 storage_dead(_14) storage_dead(_13) + storage_live(_10) _10 = copy _12.0 b_11 = copy _12.1 storage_dead(_12) diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index b4759c2cd..a5078d53c 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -659,12 +659,10 @@ where storage_live(_3) storage_live(self_4) self_4 = TraitClause0::allocate<'3>(move self_1, move layout_2) - storage_live(v_11) match self_4 { Result::Ok => { }, Result::Err => { - storage_dead(v_11) storage_dead(self_4) storage_live(_14) storage_live(_15) @@ -682,6 +680,7 @@ where return }, } + storage_live(v_11) v_11 = move (self_4 as variant Result::Ok).0 _3 = ControlFlow::Continue { 0: copy v_11 } storage_dead(v_11) @@ -819,18 +818,16 @@ fn runtime(src_1: *const (), dst_2: *const (), size_3: usize, count_4: usize) -> let _17: (); // anonymous local let _18: bool; // anonymous local - storage_live(src_usize_5) - storage_live(dst_usize_6) storage_live(_7) - storage_live(size_8) storage_live(diff_10) storage_live(_17) + storage_live(src_usize_5) src_usize_5 = transmute<*const (), usize>(copy src_1) + storage_live(dst_usize_6) dst_usize_6 = transmute<*const (), usize>(copy dst_2) storage_live(_9) storage_live(b_12) storage_live(a_16) - storage_live(_11) storage_live(_13) storage_live(_14) _14 = cast(copy size_3) @@ -839,6 +836,7 @@ fn runtime(src_1: *const (), dst_2: *const (), size_3: usize, count_4: usize) -> _13 = move _14 checked.* move _15 storage_dead(_15) storage_dead(_14) + storage_live(_11) _11 = copy _13.0 b_12 = copy _13.1 storage_dead(_13) @@ -849,6 +847,7 @@ fn runtime(src_1: *const (), dst_2: *const (), size_3: usize, count_4: usize) -> _9 = Option::Some { 0: copy a_16 } storage_dead(a_16) storage_dead(b_12) + storage_live(size_8) size_8 = copy (_9 as variant Option::Some).0 storage_dead(_9) storage_live(_18) @@ -860,6 +859,9 @@ fn runtime(src_1: *const (), dst_2: *const (), size_3: usize, count_4: usize) -> } storage_dead(_18) _0 = move diff_10 >= copy size_8 + storage_dead(size_8) + storage_dead(dst_usize_6) + storage_dead(src_usize_5) return } _17 = cold_path() @@ -1101,12 +1103,10 @@ where storage_live(_5) storage_live(self_6) self_6 = TraitClause0::allocate<'9>(copy self_1, move new_layout_4) - storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_13) storage_dead(self_6) storage_live(_14) storage_live(_15) @@ -1124,6 +1124,7 @@ where return }, } + storage_live(v_13) v_13 = move (self_6 as variant Result::Ok).0 _5 = ControlFlow::Continue { 0: copy v_13 } storage_dead(v_13) @@ -1202,12 +1203,10 @@ where storage_live(_5) storage_live(self_6) self_6 = TraitClause0::allocate_zeroed<'9>(copy self_1, move new_layout_4) - storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_13) storage_dead(self_6) storage_live(_14) storage_live(_15) @@ -1225,6 +1224,7 @@ where return }, } + storage_live(v_13) v_13 = move (self_6 as variant Result::Ok).0 _5 = ControlFlow::Continue { 0: copy v_13 } storage_dead(v_13) @@ -1303,12 +1303,10 @@ where storage_live(_5) storage_live(self_6) self_6 = TraitClause0::allocate<'9>(copy self_1, copy new_layout_4) - storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_13) storage_dead(self_6) storage_live(_14) storage_live(_15) @@ -1326,6 +1324,7 @@ where return }, } + storage_live(v_13) v_13 = move (self_6 as variant Result::Ok).0 _5 = ControlFlow::Continue { 0: copy v_13 } storage_dead(v_13) @@ -1869,7 +1868,6 @@ fn alloc_impl_runtime(layout_1: Layout, zeroed_2: bool) -> Result, let _40: AllocError; // anonymous local let _41: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - storage_live(size_3) storage_live(raw_ptr_6) storage_live(_10) storage_live(ptr_11) @@ -1879,9 +1877,33 @@ fn alloc_impl_runtime(layout_1: Layout, zeroed_2: bool) -> Result, storage_live(_20) storage_live(_24) storage_live(_30) + storage_live(size_3) size_3 = copy (layout_1).size switch copy size_3 { 0 : usize => { + storage_live(_4) + storage_live(data_5) + _13 = copy (layout_1).align + data_5 = transmute>(copy _13) + storage_live(ptr_14) + storage_live(data_15) + data_15 = transmute(copy _13) + ptr_14 = *mut (copy data_15, const 0 : usize) + storage_dead(data_15) + storage_live(_34) + _34 = ub_checks + if move _34 { + storage_live(_17) + _17 = transmute(copy _13) + _16 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _17) + storage_dead(_17) + } else { + } + _4 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_14) + storage_dead(ptr_14) + storage_dead(data_5) + _0 = Result::Ok { 0: move _4 } + storage_dead(_4) }, _ => { if copy zeroed_2 { @@ -1904,6 +1926,32 @@ fn alloc_impl_runtime(layout_1: Layout, zeroed_2: bool) -> Result, _23 = transmute<*mut u8, usize>(copy raw_ptr_6) switch copy _23 { 0 : usize => { + storage_dead(_23) + storage_live(_37) + _37 = Option::None { } + self_9 = move _37 + storage_live(_38) + _38 = AllocError { } + storage_live(_39) + _39 = Result::Err { 0: move _38 } + self_8 = move _39 + storage_dead(self_9) + storage_dead(self_8) + storage_live(_32) + storage_live(_33) + _32 = @discriminant(_10) + _33 = copy _32 == const 1 : isize + assert(move _33 == true) else undefined_behavior + storage_live(_40) + _40 = AllocError { } + storage_live(_41) + _41 = Result::Err { 0: move _40 } + _0 = move _41 + storage_dead(_33) + storage_dead(_32) + storage_dead(_7) + storage_dead(size_3) + return }, _ => { storage_dead(_23) @@ -1951,63 +1999,11 @@ fn alloc_impl_runtime(layout_1: Layout, zeroed_2: bool) -> Result, storage_dead(ptr_28) _0 = Result::Ok { 0: move _12 } storage_dead(_12) - return }, } - storage_dead(_23) - storage_live(_37) - _37 = Option::None { } - self_9 = move _37 - storage_live(v_26) - storage_live(_38) - _38 = AllocError { } - storage_live(_39) - _39 = Result::Err { 0: move _38 } - self_8 = move _39 - storage_dead(v_26) - storage_dead(self_9) - storage_live(v_27) - storage_dead(v_27) - storage_dead(self_8) - storage_live(_32) - storage_live(_33) - _32 = @discriminant(_10) - _33 = copy _32 == const 1 : isize - assert(move _33 == true) else undefined_behavior - storage_live(_40) - _40 = AllocError { } - storage_live(_41) - _41 = Result::Err { 0: move _40 } - _0 = move _41 - storage_dead(_33) - storage_dead(_32) - storage_dead(_7) - return }, } - storage_live(_4) - storage_live(data_5) - _13 = copy (layout_1).align - data_5 = transmute>(copy _13) - storage_live(ptr_14) - storage_live(data_15) - data_15 = transmute(copy _13) - ptr_14 = *mut (copy data_15, const 0 : usize) - storage_dead(data_15) - storage_live(_34) - _34 = ub_checks - if move _34 { - storage_live(_17) - _17 = transmute(copy _13) - _16 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _17) - storage_dead(_17) - } else { - } - _4 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_14) - storage_dead(ptr_14) - storage_dead(data_5) - _0 = Result::Ok { 0: move _4 } - storage_dead(_4) + storage_dead(size_3) return } @@ -2083,9 +2079,6 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: let _66: AllocError; // anonymous local let _67: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - storage_live(old_size_6) - storage_live(new_size_10) - storage_live(raw_ptr_12) storage_live(_16) storage_live(ptr_17) storage_live(_18) @@ -2099,9 +2092,11 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: storage_live(_45) storage_live(_50) storage_live(_53) + storage_live(old_size_6) old_size_6 = copy (old_layout_3).size switch copy old_size_6 { 0 : usize => { + _0 = alloc_impl_runtime(move new_layout_4, move zeroed_5) }, _ => { storage_live(_7) @@ -2115,6 +2110,131 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: storage_dead(_30) _7 = move _8 == move _9 if move _7 { + storage_dead(_9) + storage_dead(_8) + storage_dead(_7) + storage_live(new_size_10) + new_size_10 = copy (new_layout_4).size + storage_live(cond_11) + cond_11 = copy new_size_10 >= copy old_size_6 + storage_live(_56) + _56 = ub_checks + if move _56 { + _31 = core::hint::assert_unchecked::precondition_check(copy cond_11) + } else { + } + assert(copy cond_11 == true) else undefined_behavior + storage_dead(cond_11) + storage_live(raw_ptr_12) + raw_ptr_12 = __rust_realloc(move ptr_2, copy old_size_6, move _29, copy new_size_10) + storage_live(_13) + storage_live(self_14) + storage_live(self_15) + storage_live(_33) + _33 = transmute<*mut u8, usize>(copy raw_ptr_12) + switch copy _33 { + 0 : usize => { + storage_dead(_33) + storage_live(_63) + _63 = Option::None { } + self_15 = move _63 + storage_live(_64) + _64 = AllocError { } + storage_live(_65) + _65 = Result::Err { 0: move _64 } + self_14 = move _65 + storage_dead(self_15) + storage_dead(self_14) + storage_live(_38) + storage_live(_39) + _38 = @discriminant(_16) + _39 = copy _38 == const 1 : isize + assert(move _39 == true) else undefined_behavior + storage_live(_66) + _66 = AllocError { } + storage_live(_67) + _67 = Result::Err { 0: move _66 } + _0 = move _67 + storage_dead(_39) + storage_dead(_38) + storage_dead(_13) + storage_dead(raw_ptr_12) + storage_dead(new_size_10) + storage_dead(old_size_6) + return + }, + _ => { + storage_dead(_33) + storage_live(_32) + storage_live(_58) + _58 = ub_checks + if move _58 { + storage_live(_35) + _35 = cast<*mut u8, *mut ()>(copy raw_ptr_12) + _34 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _35) + storage_dead(_35) + } else { + } + _32 = transmute<*mut u8, NonNull>(copy raw_ptr_12) + self_15 = Option::Some { 0: move _32 } + storage_dead(_32) + storage_live(v_36) + v_36 = move (self_15 as variant Option::Some).0 + self_14 = Result::Ok { 0: copy v_36 } + storage_dead(v_36) + storage_dead(self_15) + storage_live(v_37) + v_37 = move (self_14 as variant Result::Ok).0 + _13 = ControlFlow::Continue { 0: copy v_37 } + storage_dead(v_37) + storage_dead(self_14) + ptr_17 = copy (_13 as variant ControlFlow::Continue).0 + storage_dead(_13) + if copy zeroed_5 { + storage_live(self_19) + self_19 = copy raw_ptr_12 offset copy old_size_6 + storage_live(count_20) + count_20 = copy new_size_10 wrap.- copy old_size_6 + storage_live(_59) + _59 = ub_checks + if move _59 { + storage_live(_41) + _41 = cast<*mut u8, *const ()>(copy self_19) + storage_live(_42) + _42 = copy count_20 == const 0 : usize + _40 = core::ptr::write_bytes::precondition_check(move _41, const 1 : usize, move _42) + storage_dead(_42) + storage_dead(_41) + } else { + } + _18 = write_bytes[{built_in impl Sized for u8}](move self_19, const 0 : u8, move count_20) + storage_dead(count_20) + storage_dead(self_19) + } else { + } + storage_live(_21) + storage_live(ptr_43) + storage_live(data_44) + data_44 = transmute, *mut u8>(copy ptr_17) + ptr_43 = *mut (copy data_44, copy new_size_10) + storage_dead(data_44) + storage_live(_60) + _60 = ub_checks + if move _60 { + storage_live(_46) + _46 = transmute, *mut ()>(copy ptr_17) + _45 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _46) + storage_dead(_46) + } else { + } + _21 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_43) + storage_dead(ptr_43) + _0 = Result::Ok { 0: move _21 } + storage_dead(_21) + storage_dead(raw_ptr_12) + storage_dead(new_size_10) + }, + } } else { storage_dead(_9) storage_dead(_8) @@ -2122,12 +2242,10 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: storage_live(_22) storage_live(self_23) self_23 = alloc_impl_runtime(move new_layout_4, move zeroed_5) - storage_live(v_47) match self_23 { Result::Ok => { }, Result::Err => { - storage_dead(v_47) storage_dead(self_23) storage_live(_48) storage_live(_49) @@ -2142,9 +2260,11 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: storage_dead(_49) storage_dead(_48) storage_dead(_22) + storage_dead(old_size_6) return }, } + storage_live(v_47) v_47 = move (self_23 as variant Result::Ok).0 _22 = ControlFlow::Continue { 0: copy v_47 } storage_dead(v_47) @@ -2179,134 +2299,10 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: storage_dead(src_26) _28 = __rust_dealloc(move ptr_2, move old_size_6, move _29) _0 = Result::Ok { 0: copy new_ptr_25 } - return } - storage_dead(_9) - storage_dead(_8) - storage_dead(_7) - new_size_10 = copy (new_layout_4).size - storage_live(cond_11) - cond_11 = copy new_size_10 >= copy old_size_6 - storage_live(_56) - _56 = ub_checks - if move _56 { - _31 = core::hint::assert_unchecked::precondition_check(copy cond_11) - } else { - } - assert(copy cond_11 == true) else undefined_behavior - storage_dead(cond_11) - raw_ptr_12 = __rust_realloc(move ptr_2, copy old_size_6, move _29, copy new_size_10) - storage_live(_13) - storage_live(self_14) - storage_live(self_15) - storage_live(_33) - _33 = transmute<*mut u8, usize>(copy raw_ptr_12) - switch copy _33 { - 0 : usize => { - }, - _ => { - storage_dead(_33) - storage_live(_32) - storage_live(_58) - _58 = ub_checks - if move _58 { - storage_live(_35) - _35 = cast<*mut u8, *mut ()>(copy raw_ptr_12) - _34 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _35) - storage_dead(_35) - } else { - } - _32 = transmute<*mut u8, NonNull>(copy raw_ptr_12) - self_15 = Option::Some { 0: move _32 } - storage_dead(_32) - storage_live(v_36) - v_36 = move (self_15 as variant Option::Some).0 - self_14 = Result::Ok { 0: copy v_36 } - storage_dead(v_36) - storage_dead(self_15) - storage_live(v_37) - v_37 = move (self_14 as variant Result::Ok).0 - _13 = ControlFlow::Continue { 0: copy v_37 } - storage_dead(v_37) - storage_dead(self_14) - ptr_17 = copy (_13 as variant ControlFlow::Continue).0 - storage_dead(_13) - if copy zeroed_5 { - storage_live(self_19) - self_19 = copy raw_ptr_12 offset copy old_size_6 - storage_live(count_20) - count_20 = copy new_size_10 wrap.- copy old_size_6 - storage_live(_59) - _59 = ub_checks - if move _59 { - storage_live(_41) - _41 = cast<*mut u8, *const ()>(copy self_19) - storage_live(_42) - _42 = copy count_20 == const 0 : usize - _40 = core::ptr::write_bytes::precondition_check(move _41, const 1 : usize, move _42) - storage_dead(_42) - storage_dead(_41) - } else { - } - _18 = write_bytes[{built_in impl Sized for u8}](move self_19, const 0 : u8, move count_20) - storage_dead(count_20) - storage_dead(self_19) - } else { - } - storage_live(_21) - storage_live(ptr_43) - storage_live(data_44) - data_44 = transmute, *mut u8>(copy ptr_17) - ptr_43 = *mut (copy data_44, copy new_size_10) - storage_dead(data_44) - storage_live(_60) - _60 = ub_checks - if move _60 { - storage_live(_46) - _46 = transmute, *mut ()>(copy ptr_17) - _45 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _46) - storage_dead(_46) - } else { - } - _21 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_43) - storage_dead(ptr_43) - _0 = Result::Ok { 0: move _21 } - storage_dead(_21) - return - }, - } - storage_dead(_33) - storage_live(_63) - _63 = Option::None { } - self_15 = move _63 - storage_live(v_36) - storage_live(_64) - _64 = AllocError { } - storage_live(_65) - _65 = Result::Err { 0: move _64 } - self_14 = move _65 - storage_dead(v_36) - storage_dead(self_15) - storage_live(v_37) - storage_dead(v_37) - storage_dead(self_14) - storage_live(_38) - storage_live(_39) - _38 = @discriminant(_16) - _39 = copy _38 == const 1 : isize - assert(move _39 == true) else undefined_behavior - storage_live(_66) - _66 = AllocError { } - storage_live(_67) - _67 = Result::Err { 0: move _66 } - _0 = move _67 - storage_dead(_39) - storage_dead(_38) - storage_dead(_13) - return }, } - _0 = alloc_impl_runtime(move new_layout_4, move zeroed_5) + storage_dead(old_size_6) return } @@ -2387,10 +2383,8 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ let _71: AllocError; // anonymous local let _72: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - storage_live(new_size_6) storage_live(_7) storage_live(_14) - storage_live(raw_ptr_15) storage_live(_19) storage_live(ptr_20) storage_live(_24) @@ -2404,9 +2398,46 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ storage_live(_47) storage_live(_54) storage_live(_57) + storage_live(new_size_6) new_size_6 = copy (new_layout_4).size switch copy new_size_6 { 0 : usize => { + storage_live(_30) + _30 = copy (old_layout_3).size + switch copy _30 { + 0 : usize => { + }, + _ => { + storage_live(_31) + _31 = copy (old_layout_3).align + _7 = __rust_dealloc(move ptr_2, move _30, move _31) + storage_dead(_31) + }, + } + storage_dead(_30) + storage_live(_8) + storage_live(data_9) + _32 = copy (new_layout_4).align + data_9 = transmute>(copy _32) + storage_live(ptr_33) + storage_live(data_34) + data_34 = transmute(copy _32) + ptr_33 = *mut (copy data_34, const 0 : usize) + storage_dead(data_34) + storage_live(_61) + _61 = ub_checks + if move _61 { + storage_live(_36) + _36 = transmute(copy _32) + _35 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _36) + storage_dead(_36) + } else { + } + _8 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_33) + storage_dead(ptr_33) + storage_dead(data_9) + _0 = Result::Ok { 0: move _8 } + storage_dead(_8) }, _ => { storage_live(_10) @@ -2420,6 +2451,106 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ storage_dead(_37) _10 = move _11 == move _12 if move _10 { + storage_dead(_12) + storage_dead(_11) + storage_dead(_10) + storage_live(cond_13) + _14 = copy (old_layout_3).size + cond_13 = copy new_size_6 <= copy _14 + storage_live(_62) + _62 = ub_checks + if move _62 { + _38 = core::hint::assert_unchecked::precondition_check(copy cond_13) + } else { + } + assert(copy cond_13 == true) else undefined_behavior + storage_dead(cond_13) + storage_live(raw_ptr_15) + raw_ptr_15 = __rust_realloc(move ptr_2, move _14, move _29, copy new_size_6) + storage_live(_16) + storage_live(self_17) + storage_live(self_18) + storage_live(_40) + _40 = transmute<*mut u8, usize>(copy raw_ptr_15) + switch copy _40 { + 0 : usize => { + storage_dead(_40) + storage_live(_68) + _68 = Option::None { } + self_18 = move _68 + storage_live(_69) + _69 = AllocError { } + storage_live(_70) + _70 = Result::Err { 0: move _69 } + self_17 = move _70 + storage_dead(self_18) + storage_dead(self_17) + storage_live(_49) + storage_live(_50) + _49 = @discriminant(_19) + _50 = copy _49 == const 1 : isize + assert(move _50 == true) else undefined_behavior + storage_live(_71) + _71 = AllocError { } + storage_live(_72) + _72 = Result::Err { 0: move _71 } + _0 = move _72 + storage_dead(_50) + storage_dead(_49) + storage_dead(_16) + storage_dead(raw_ptr_15) + storage_dead(new_size_6) + return + }, + _ => { + storage_dead(_40) + storage_live(_39) + storage_live(_64) + _64 = ub_checks + if move _64 { + storage_live(_42) + _42 = cast<*mut u8, *mut ()>(copy raw_ptr_15) + _41 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _42) + storage_dead(_42) + } else { + } + _39 = transmute<*mut u8, NonNull>(copy raw_ptr_15) + self_18 = Option::Some { 0: move _39 } + storage_dead(_39) + storage_live(v_43) + v_43 = move (self_18 as variant Option::Some).0 + self_17 = Result::Ok { 0: copy v_43 } + storage_dead(v_43) + storage_dead(self_18) + storage_live(v_44) + v_44 = move (self_17 as variant Result::Ok).0 + _16 = ControlFlow::Continue { 0: copy v_44 } + storage_dead(v_44) + storage_dead(self_17) + ptr_20 = copy (_16 as variant ControlFlow::Continue).0 + storage_dead(_16) + storage_live(_21) + storage_live(ptr_45) + storage_live(data_46) + data_46 = transmute, *mut u8>(copy ptr_20) + ptr_45 = *mut (copy data_46, copy new_size_6) + storage_dead(data_46) + storage_live(_65) + _65 = ub_checks + if move _65 { + storage_live(_48) + _48 = transmute, *mut ()>(copy ptr_20) + _47 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _48) + storage_dead(_48) + } else { + } + _21 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_45) + storage_dead(ptr_45) + _0 = Result::Ok { 0: move _21 } + storage_dead(_21) + storage_dead(raw_ptr_15) + }, + } } else { storage_dead(_12) storage_dead(_11) @@ -2427,12 +2558,10 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ storage_live(_22) storage_live(self_23) self_23 = alloc_impl_runtime(move new_layout_4, const false) - storage_live(v_51) match self_23 { Result::Ok => { }, Result::Err => { - storage_dead(v_51) storage_dead(self_23) storage_live(_52) storage_live(_53) @@ -2447,9 +2576,11 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ storage_dead(_53) storage_dead(_52) storage_dead(_22) + storage_dead(new_size_6) return }, } + storage_live(v_51) v_51 = move (self_23 as variant Result::Ok).0 _22 = ControlFlow::Continue { 0: copy v_51 } storage_dead(v_51) @@ -2493,147 +2624,10 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ } storage_dead(_60) _0 = Result::Ok { 0: copy new_ptr_25 } - return } - storage_dead(_12) - storage_dead(_11) - storage_dead(_10) - storage_live(cond_13) - _14 = copy (old_layout_3).size - cond_13 = copy new_size_6 <= copy _14 - storage_live(_62) - _62 = ub_checks - if move _62 { - _38 = core::hint::assert_unchecked::precondition_check(copy cond_13) - } else { - } - assert(copy cond_13 == true) else undefined_behavior - storage_dead(cond_13) - raw_ptr_15 = __rust_realloc(move ptr_2, move _14, move _29, copy new_size_6) - storage_live(_16) - storage_live(self_17) - storage_live(self_18) - storage_live(_40) - _40 = transmute<*mut u8, usize>(copy raw_ptr_15) - switch copy _40 { - 0 : usize => { - }, - _ => { - storage_dead(_40) - storage_live(_39) - storage_live(_64) - _64 = ub_checks - if move _64 { - storage_live(_42) - _42 = cast<*mut u8, *mut ()>(copy raw_ptr_15) - _41 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _42) - storage_dead(_42) - } else { - } - _39 = transmute<*mut u8, NonNull>(copy raw_ptr_15) - self_18 = Option::Some { 0: move _39 } - storage_dead(_39) - storage_live(v_43) - v_43 = move (self_18 as variant Option::Some).0 - self_17 = Result::Ok { 0: copy v_43 } - storage_dead(v_43) - storage_dead(self_18) - storage_live(v_44) - v_44 = move (self_17 as variant Result::Ok).0 - _16 = ControlFlow::Continue { 0: copy v_44 } - storage_dead(v_44) - storage_dead(self_17) - ptr_20 = copy (_16 as variant ControlFlow::Continue).0 - storage_dead(_16) - storage_live(_21) - storage_live(ptr_45) - storage_live(data_46) - data_46 = transmute, *mut u8>(copy ptr_20) - ptr_45 = *mut (copy data_46, copy new_size_6) - storage_dead(data_46) - storage_live(_65) - _65 = ub_checks - if move _65 { - storage_live(_48) - _48 = transmute, *mut ()>(copy ptr_20) - _47 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _48) - storage_dead(_48) - } else { - } - _21 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_45) - storage_dead(ptr_45) - _0 = Result::Ok { 0: move _21 } - storage_dead(_21) - return - }, - } - storage_dead(_40) - storage_live(_68) - _68 = Option::None { } - self_18 = move _68 - storage_live(v_43) - storage_live(_69) - _69 = AllocError { } - storage_live(_70) - _70 = Result::Err { 0: move _69 } - self_17 = move _70 - storage_dead(v_43) - storage_dead(self_18) - storage_live(v_44) - storage_dead(v_44) - storage_dead(self_17) - storage_live(_49) - storage_live(_50) - _49 = @discriminant(_19) - _50 = copy _49 == const 1 : isize - assert(move _50 == true) else undefined_behavior - storage_live(_71) - _71 = AllocError { } - storage_live(_72) - _72 = Result::Err { 0: move _71 } - _0 = move _72 - storage_dead(_50) - storage_dead(_49) - storage_dead(_16) - return - }, - } - storage_live(_30) - _30 = copy (old_layout_3).size - switch copy _30 { - 0 : usize => { - }, - _ => { - storage_live(_31) - _31 = copy (old_layout_3).align - _7 = __rust_dealloc(move ptr_2, move _30, move _31) - storage_dead(_31) }, } - storage_dead(_30) - storage_live(_8) - storage_live(data_9) - _32 = copy (new_layout_4).align - data_9 = transmute>(copy _32) - storage_live(ptr_33) - storage_live(data_34) - data_34 = transmute(copy _32) - ptr_33 = *mut (copy data_34, const 0 : usize) - storage_dead(data_34) - storage_live(_61) - _61 = ub_checks - if move _61 { - storage_live(_36) - _36 = transmute(copy _32) - _35 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _36) - storage_dead(_36) - } else { - } - _8 = transmute<*mut [u8], NonNull<[u8]>>(copy ptr_33) - storage_dead(ptr_33) - storage_dead(data_9) - _0 = Result::Ok { 0: move _8 } - storage_dead(_8) + storage_dead(new_size_6) return } @@ -2810,7 +2804,6 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 let _6: *mut u8; // anonymous local let _7: *mut [u8]; // anonymous local - storage_live(ptr_3) storage_live(_4) storage_live(_2) _2 = alloc_impl_runtime(copy layout_1, const false) @@ -2821,6 +2814,7 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 _4 = handle_alloc_error(move layout_1) }, } + storage_live(ptr_3) ptr_3 = copy (_2 as variant Result::Ok).0 storage_live(_5) storage_live(_6) @@ -2832,6 +2826,7 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 storage_dead(_6) _0 = transmute, *mut u8>(copy _5) storage_dead(_5) + storage_dead(ptr_3) storage_dead(_2) return } @@ -2933,6 +2928,7 @@ where _3 = transmute, *const T>(copy _4) _2 = &raw mut (*_3) with_metadata(copy _3.metadata) storage_dead(_3) + storage_dead(_4) _0 = &mut (*_2) with_metadata(copy _2.metadata) return } diff --git a/charon/tests/ui/regressions/invalid-reconstruct-assert.out b/charon/tests/ui/regressions/invalid-reconstruct-assert.out index 989022b1f..5a24c3374 100644 --- a/charon/tests/ui/regressions/invalid-reconstruct-assert.out +++ b/charon/tests/ui/regressions/invalid-reconstruct-assert.out @@ -161,11 +161,8 @@ where bb0: { storage_live(base_5); - storage_live(half_8); - storage_live(mid_10); storage_live(_15); storage_live(_21); - storage_live(result_25); storage_live(_30); storage_live(_36); storage_live(_38); @@ -208,10 +205,12 @@ where bb5: { storage_dead(_7); + storage_live(half_8); storage_live(_9); _9 = copy size_3; half_8 = move _9 ub./ const 2 : usize; storage_dead(_9); + storage_live(mid_10); storage_live(_11); _11 = copy base_5; mid_10 = move _11 wrap.+ copy half_8; @@ -333,6 +332,8 @@ where storage_dead(_16); size_3 = copy size_3 wrap.- copy half_8; storage_dead(cmp_12); + storage_dead(mid_10); + storage_dead(half_8); storage_dead(_6); goto bb4; } @@ -349,6 +350,7 @@ where } bb22: { + storage_live(result_25); storage_live(_26); storage_live(_27); _27 = copy _39 == const -1 : i8; @@ -382,6 +384,7 @@ where assert(copy cond_28 == true) else undefined_behavior; storage_dead(cond_28); _0 = Result::Err { 0: copy result_25 }; + storage_dead(result_25); goto bb28; } diff --git a/charon/tests/ui/regressions/issue-1073-out-of-bounds-body-region.out b/charon/tests/ui/regressions/issue-1073-out-of-bounds-body-region.out index 1510ef242..3ee78f30b 100644 --- a/charon/tests/ui/regressions/issue-1073-out-of-bounds-body-region.out +++ b/charon/tests/ui/regressions/issue-1073-out-of-bounds-body-region.out @@ -1,446 +1,19 @@ # Final LLBC before serialization: -// Full name: core::ffi::c_void -#[lang_item("c_void")] -pub enum c_void { - __variant1, - __variant2, -} - -// Full name: core::fmt::Arguments -#[lang_item("format_arguments")] -pub opaque type Arguments<'a> - -// Full name: core::fmt::rt::Argument -#[lang_item("format_argument")] -pub opaque type Argument<'a> - -// Full name: core::marker::MetaSized -#[lang_item("meta_sized")] -pub trait MetaSized - -// Full name: core::marker::Sized -#[lang_item("sized")] -pub trait Sized -{ - proof ImpliedClause0: (Self: MetaSized) - non-dyn-compatible -} +// Full name: core::io::io_slice::IoSlice +pub opaque type IoSlice<'a> -// Full name: core::marker::PhantomData -#[lang_item("phantom_data")] -pub struct PhantomData {} - -// Full name: core::option::Option -#[lang_item("Option")] -pub enum Option -where - TraitClause0: (T: Sized), -{ - None, - Some(T), -} - -// Full name: core::ptr::non_null::NonNull -#[lang_item("NonNull")] -pub opaque type NonNull - -// Full name: core::slice::index::slice_index_fail -fn slice_index_fail(_1: usize, _2: usize, _3: usize) -> ! +// Full name: core::io::io_slice::{IoSlice<'a>}::advance_slices +pub fn advance_slices<'a, '_1, '_2>(_1: &'_1 mut &'_2 mut [IoSlice<'a>], _2: usize) = -// Full name: core::slice::iter::Iter -#[lang_item("SliceIter")] -pub opaque type Iter<'a, T> -where - TraitClause0: (T: Sized), - TypeOutlives0: T: 'a, - TypeOutlives1: T: 'a, - -// Full name: core::slice::raw::from_raw_parts::precondition_check -fn precondition_check(_1: *mut (), _2: usize, _3: usize, _4: usize) -= - -pub opaque type std::io::IoSlice<'a> - -// Full name: libc::unix::iovec -pub struct iovec { - iov_base: *mut c_void, - iov_len: usize, -} - -pub opaque type std::sys::io::io_slice::iovec::IoSlice<'a> - -// Full name: std::io::{std::io::IoSlice<'a>}::advance_slices -pub fn advance_slices<'a, '_1, '_2>(bufs_1: &'_1 mut &'_2 mut [std::io::IoSlice<'a>], n_2: usize) -{ - let _0: (); // return - let bufs_1: &'7 mut &'8 mut [std::io::IoSlice<'9>]; // arg #1 - let n_2: usize; // arg #2 - let remove_3: usize; // local - let iter_4: Iter<'16, std::io::IoSlice<'17>>[{built_in impl Sized for std::io::IoSlice<'17>}]; // local - let _5: Option<&'34 std::io::IoSlice<'35>>[{built_in impl Sized for &'34 std::io::IoSlice<'35>}]; // anonymous local - let buf_6: &'50 std::io::IoSlice<'51>; // local - let _7: Option[{built_in impl Sized for usize}]; // anonymous local - let self_8: usize; // local - let _9: &'52 mut [std::io::IoSlice<'53>]; // anonymous local - let self_10: &'54 mut [std::io::IoSlice<'55>]; // local - let _11: Arguments<'57>; // anonymous local - let self_12: &'60 mut std::io::IoSlice<'61>; // local - let self_13: &'62 mut [std::io::IoSlice<'63>]; // local - let self_14: &'64 mut [std::io::IoSlice<'65>]; // local - let _15: &'66 mut [std::io::IoSlice<'67>]; // anonymous local - let _16: &'68 mut [std::io::IoSlice<'69>]; // anonymous local - let len_17: usize; // local - let ptr_18: NonNull>; // local - let self_19: NonNull<[std::io::IoSlice<'73>]>; // local - let end_or_len_20: *const std::io::IoSlice<'75>; // local - let _21: *mut std::io::IoSlice<'77>; // anonymous local - let self_22: *mut std::io::IoSlice<'78>; // local - let _23: *const [std::io::IoSlice<'80>]; // anonymous local - let _24: *mut std::io::IoSlice<'81>; // anonymous local - let _25: *mut [std::io::IoSlice<'83>]; // anonymous local - let ptr_26: NonNull>; // local - let end_or_len_27: *const std::io::IoSlice<'85>; // local - let _28: bool; // anonymous local - let _29: NonNull>; // anonymous local - let _30: NonNull>; // anonymous local - let _31: &'94 std::io::IoSlice<'95>; // anonymous local - let _32: *mut std::io::IoSlice<'98>; // anonymous local - let _33: *mut std::io::IoSlice<'99>; // anonymous local - let _34: *mut std::io::IoSlice<'100>; // anonymous local - let _35: *const std::io::IoSlice<'101>; // anonymous local - let data_36: *const u8; // local - let _37: *mut c_void; // anonymous local - let len_38: usize; // local - let _39: (); // anonymous local - let _40: *mut (); // anonymous local - let _41: bool; // anonymous local - let _42: usize; // anonymous local - let src_43: &'107 mut [std::io::IoSlice<'108>]; // local - let _44: bool; // anonymous local - let _45: usize; // anonymous local - let _46: !; // anonymous local - let new_len_47: usize; // local - let _48: *mut [std::io::IoSlice<'109>]; // anonymous local - let ptr_49: *mut [std::io::IoSlice<'110>]; // local - let _50: *mut std::io::IoSlice<'111>; // anonymous local - let _51: *mut std::io::IoSlice<'112>; // anonymous local - let _52: usize; // anonymous local - let s_53: &'114 str; // local - let _54: NonNull; // anonymous local - let _55: *const u8; // anonymous local - let _56: NonNull>; // anonymous local - let _57: usize; // anonymous local - let _58: usize; // anonymous local - let _59: usize; // anonymous local - let _60: *const str; // anonymous local - let _61: &'119 [u8]; // anonymous local - let _62: bool; // anonymous local - let _63: usize; // anonymous local - let _64: Arguments<'124>; // anonymous local - let _65: *mut c_void; // anonymous local - let self_66: *mut c_void; // local - let s_67: &'125 str; // local - let _68: NonNull; // anonymous local - let _69: *const u8; // anonymous local - let _70: NonNull>; // anonymous local - let _71: usize; // anonymous local - let _72: usize; // anonymous local - let _73: usize; // anonymous local - let _74: *const str; // anonymous local - let _75: &'127 [u8]; // anonymous local - let _76: bool; // anonymous local - let _77: &'191 mut [std::io::IoSlice<'192>; 0 : usize]; // anonymous local - let _78: &'231 mut [std::io::IoSlice<'183>; 0 : usize]; // anonymous local - let _79: [std::io::IoSlice<'183>; 0 : usize]; // anonymous local - let _80: PhantomData<&'139 std::io::IoSlice<'140>>; // anonymous local - let _81: &'_ mut [std::io::IoSlice<'214>]; // anonymous local - let _82: &'_ mut std::io::IoSlice<'214>; // anonymous local - - storage_live(remove_3) - storage_live(iter_4) - storage_live(buf_6) - storage_live(_9) - storage_live(self_10) - storage_live(self_12) - storage_live(self_13) - storage_live(self_14) - storage_live(_15) - storage_live(_16) - storage_live(len_38) - storage_live(_39) - storage_live(_46) - _0 = () - remove_3 = const 0 : usize - self_13 = copy (*bufs_1) - storage_live(len_17) - storage_live(ptr_18) - storage_live(end_or_len_20) - len_17 = copy self_13.metadata - storage_live(self_19) - storage_live(_23) - _23 = &raw const (*self_13) with_metadata(copy self_13.metadata) - self_19 = transmute<*const [std::io::IoSlice<'80>], NonNull<[std::io::IoSlice<'131>]>>(copy _23) - storage_dead(_23) - storage_live(_24) - storage_live(_25) - _25 = transmute]>, *mut [std::io::IoSlice<'132>]>(copy self_19) - _24 = cast<*mut [std::io::IoSlice<'83>], *mut std::io::IoSlice<'133>>(copy _25) - storage_dead(_25) - ptr_18 = transmute<*mut std::io::IoSlice<'81>, NonNull>>(copy _24) - storage_dead(_24) - storage_dead(self_19) - storage_live(_21) - storage_live(self_22) - self_22 = transmute>, *mut std::io::IoSlice<'135>>(copy ptr_18) - _21 = copy self_22 offset copy len_17 - storage_dead(self_22) - end_or_len_20 = cast<*mut std::io::IoSlice<'77>, *const std::io::IoSlice<'136>>(copy _21) - storage_dead(_21) - storage_live(_80) - _80 = PhantomData { } - iter_4 = Iter { 0: copy ptr_18, 1: copy end_or_len_20, 2: move _80 } - storage_dead(end_or_len_20) - storage_dead(ptr_18) - storage_dead(len_17) - loop { - storage_live(_5) - storage_live(ptr_26) - storage_live(end_or_len_27) - storage_live(_29) - storage_live(_31) - storage_live(_32) - ptr_26 = copy (iter_4).0 - end_or_len_27 = copy (iter_4).1 - storage_live(_28) - _29 = transmute<*const std::io::IoSlice<'85>, NonNull>>(copy end_or_len_27) - _32 = transmute>, *mut std::io::IoSlice<'150>>(copy ptr_26) - storage_live(_33) - _33 = transmute>, *mut std::io::IoSlice<'151>>(copy _29) - _28 = copy _32 == copy _33 - storage_dead(_33) - if move _28 { - storage_dead(_28) - storage_dead(_32) - storage_dead(_31) - storage_dead(_29) - storage_dead(end_or_len_27) - storage_dead(ptr_26) - break 0 - } else { - storage_dead(_28) - storage_live(_30) - storage_live(_34) - _34 = copy _32 offset const 1 : usize - _30 = transmute<*mut std::io::IoSlice<'100>, NonNull>>(copy _34) - storage_dead(_34) - (iter_4).0 = move _30 - storage_dead(_30) - storage_live(_35) - _35 = transmute>, *const std::io::IoSlice<'154>>(copy ptr_26) - _31 = &(*_35) - storage_dead(_35) - _5 = Option::Some { 0: copy _31 } - storage_dead(_32) - storage_dead(_31) - storage_dead(_29) - storage_dead(end_or_len_27) - storage_dead(ptr_26) - buf_6 = copy (_5 as variant Option::Some).0 - storage_live(_7) - storage_live(self_8) - self_8 = copy n_2 - storage_live(_37) - storage_live(data_36) - _37 = copy ((((*buf_6)).0).0).iov_base - data_36 = cast<*mut c_void, *const u8>(copy _37) - len_38 = copy ((((*buf_6)).0).0).iov_len - storage_live(_76) - _76 = ub_checks - if move _76 { - storage_live(_40) - _40 = cast<*mut c_void, *mut ()>(copy _37) - _39 = precondition_check(move _40, const 1 : usize, const 1 : usize, copy len_38) - storage_dead(_40) - } else { - } - storage_dead(data_36) - storage_dead(_37) - storage_live(_41) - _41 = copy self_8 < copy len_38 - if move _41 { - storage_dead(_41) - storage_dead(self_8) - storage_dead(_7) - break 0 - } else { - } - storage_live(_42) - _42 = copy self_8 ub.- copy len_38 - _7 = Option::Some { 0: move _42 } - storage_dead(_42) - storage_dead(_41) - storage_dead(self_8) - n_2 = copy (_7 as variant Option::Some).0 - remove_3 = copy remove_3 wrap.+ const 1 : usize - storage_dead(_7) - storage_dead(_5) - continue 0 - } - } - storage_live(_77) - storage_live(_78) - storage_live(_79) - _79 = [] - _78 = &mut _79 - _77 = move _78 - storage_dead(_5) - storage_live(src_43) - src_43 = @ArrayToSliceMut<'_, std::io::IoSlice<'192>, 0 : usize>(move _77) - self_10 = copy (*bufs_1) - (*bufs_1) = copy src_43 - storage_dead(src_43) - storage_live(_45) - storage_live(new_len_47) - storage_live(_44) - _45 = copy self_10.metadata - _44 = copy remove_3 > copy _45 - if move _44 { - } else { - storage_dead(_44) - new_len_47 = copy _45 ub.- copy remove_3 - storage_live(_48) - storage_live(ptr_49) - ptr_49 = &raw mut (*self_10) with_metadata(copy self_10.metadata) - storage_live(_50) - storage_live(_51) - _50 = cast<*mut [std::io::IoSlice<'110>], *mut std::io::IoSlice<'198>>(copy ptr_49) - _51 = copy _50 offset copy remove_3 - _48 = @PtrFromPartsMut<'_, [std::io::IoSlice<'199>]>(copy _51, copy new_len_47) - storage_dead(_51) - storage_dead(_50) - storage_dead(ptr_49) - _9 = &mut (*_48) with_metadata(copy _48.metadata) - storage_dead(_48) - storage_dead(new_len_47) - storage_dead(_45) - (*bufs_1) = copy _9 - self_14 = copy (*bufs_1) - storage_live(_52) - _52 = copy self_14.metadata - switch copy _52 { - 0 : usize => { - }, - _ => { - storage_dead(_52) - _15 = copy (*bufs_1) - _16 = copy (*bufs_1) - storage_live(_81) - _81 = &mut (*_16) with_metadata(copy _16.metadata) - storage_live(_82) - _82 = @SliceIndexMut<'_, std::io::IoSlice<'214>>(move _81, const 0 : usize) - self_12 = &two-phase-mut (*_82) - storage_live(_62) - storage_live(_63) - _63 = copy ((((*self_12)).0).0).iov_len - _62 = move _63 < copy n_2 - if move _62 { - } else { - storage_dead(_63) - storage_dead(_62) - ((((*self_12)).0).0).iov_len = copy ((((*self_12)).0).0).iov_len wrap.- copy n_2 - storage_live(_65) - storage_live(self_66) - self_66 = copy ((((*self_12)).0).0).iov_base - _65 = copy self_66 offset copy n_2 - storage_dead(self_66) - ((((*self_12)).0).0).iov_base = copy _65 - storage_dead(_65) - return - } - storage_dead(_63) - storage_live(_64) - storage_live(s_67) - s_67 = const "advancing IoSlice beyond its length" - storage_live(_68) - storage_live(_69) - storage_live(_74) - _74 = &raw const (*s_67) with_metadata(copy s_67.metadata) - _69 = cast<*const str, *const u8>(copy _74) - storage_dead(_74) - _68 = transmute<*const u8, NonNull>(copy _69) - storage_dead(_69) - storage_live(_70) - storage_live(_71) - storage_live(_72) - storage_live(_73) - storage_live(_75) - _75 = transmute<&'220 str, &'219 [u8]>(const "advancing IoSlice beyond its length") - _73 = copy _75.metadata - storage_dead(_75) - _72 = move _73 wrap.<< const 1 : i32 - storage_dead(_73) - _71 = move _72 | const 1 : usize - storage_dead(_72) - _70 = transmute>>(move _71) - storage_dead(_71) - _64 = Arguments { 0: move _68, 1: move _70 } - storage_dead(_70) - storage_dead(_68) - storage_dead(s_67) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(_52) - switch copy n_2 { - 0 : usize => { - }, - _ => { - storage_live(_11) - storage_live(s_53) - s_53 = const "advancing io slices beyond their length" - storage_live(_54) - storage_live(_55) - storage_live(_60) - _60 = &raw const (*s_53) with_metadata(copy s_53.metadata) - _55 = cast<*const str, *const u8>(copy _60) - storage_dead(_60) - _54 = transmute<*const u8, NonNull>(copy _55) - storage_dead(_55) - storage_live(_56) - storage_live(_57) - storage_live(_58) - storage_live(_59) - storage_live(_61) - _61 = transmute<&'209 str, &'208 [u8]>(const "advancing io slices beyond their length") - _59 = copy _61.metadata - storage_dead(_61) - _58 = move _59 wrap.<< const 1 : i32 - storage_dead(_59) - _57 = move _58 | const 1 : usize - storage_dead(_58) - _56 = transmute>>(move _57) - storage_dead(_57) - _11 = Arguments { 0: move _54, 1: move _56 } - storage_dead(_56) - storage_dead(_54) - storage_dead(s_53) - panic(core::panicking::panic_fmt) - }, - } - return - } - _46 = slice_index_fail(move remove_3, copy _45, move _45) -} - // Full name: test_crate::foo -pub fn foo<'_0, '_1, '_2>(bufs_1: &'_0 mut &'_1 mut [std::io::IoSlice<'_2>]) +pub fn foo<'_0, '_1, '_2>(bufs_1: &'_0 mut &'_1 mut [IoSlice<'_2>]) { let _0: (); // return - let bufs_1: &'7 mut &'8 mut [std::io::IoSlice<'9>]; // arg #1 + let bufs_1: &'7 mut &'8 mut [IoSlice<'9>]; // arg #1 let _2: (); // anonymous local - let _3: &'10 mut &'11 mut [std::io::IoSlice<'12>]; // anonymous local + let _3: &'10 mut &'11 mut [IoSlice<'12>]; // anonymous local _0 = () storage_live(_2) diff --git a/charon/tests/ui/regressions/issue-1074-vtable-supertrait.out b/charon/tests/ui/regressions/issue-1074-vtable-supertrait.out index c4be39193..178108e9b 100644 --- a/charon/tests/ui/regressions/issue-1074-vtable-supertrait.out +++ b/charon/tests/ui/regressions/issue-1074-vtable-supertrait.out @@ -55,12 +55,9 @@ pub struct MyStruct {} unsafe fn {impl Destruct for MyStruct}::drop_in_place(_1: *mut MyStruct) { let _0: (); // return - let _1: *mut MyStruct; // arg #1 - let _2: &'1 mut MyStruct; // anonymous local + let _1: &'1 mut MyStruct; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index c9ec142fe..228e30dd6 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -134,7 +134,6 @@ where let _5: &'6 E; // anonymous local storage_live(_3) - storage_live(_5) match self_1 { Result::Ok => { }, @@ -142,6 +141,7 @@ where storage_live(e_2) e_2 = move (self_1 as variant Result::Err).0 storage_live(_4) + storage_live(_5) _5 = &e_2 _4 = unsize_cast<&'6 E, &'7 (dyn Debug + '8), &vtable_of(TraitClause2)>(copy _5) _3 = unwrap_failed<'11, '12>(const "called `Result::unwrap()` on an `Err` value", move _4) diff --git a/charon/tests/ui/simple/box-dyn-fnonce-raw.out b/charon/tests/ui/simple/box-dyn-fnonce-raw.out index ed26f064e..225b6a4cd 100644 --- a/charon/tests/ui/simple/box-dyn-fnonce-raw.out +++ b/charon/tests/ui/simple/box-dyn-fnonce-raw.out @@ -292,7 +292,6 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 let _6: *mut u8; // anonymous local let _7: *mut [u8]; // anonymous local - storage_live(ptr_3) storage_live(_4) storage_live(_2) _2 = alloc_impl_runtime(copy layout_1, const false) @@ -303,6 +302,7 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 _4 = handle_alloc_error(move layout_1) }, } + storage_live(ptr_3) ptr_3 = copy (_2 as variant Result::Ok).0 storage_live(_5) storage_live(_6) @@ -314,6 +314,7 @@ fn box_new_uninit(layout_1: Layout) -> *mut u8 storage_dead(_6) _0 = transmute, *mut u8>(copy _5) storage_dead(_5) + storage_dead(ptr_3) storage_dead(_2) return } @@ -364,18 +365,18 @@ where let _16: bool; // anonymous local let _17: bool; // anonymous local - storage_live(layout_2) storage_live(_4) storage_live(_5) storage_live(size_7) storage_live(_10) storage_live(_11) storage_live(unique_12) + _0 = () storage_live(ptr_14) storage_live(ptr_15) - _0 = () ptr_14 = copy (((*self_1)).0).0 ptr_15 = copy (((*self_1)).0).1 + storage_live(layout_2) storage_live(t_3) _4 = transmute, *mut T>(copy ptr_14) t_3 = transmute, *const T>(copy ptr_14) @@ -412,9 +413,11 @@ where storage_dead(_13) _5 = TraitClause2::deallocate<'7>(move _6, move unique_12, move layout_2) storage_dead(_6) - return }, } + storage_dead(layout_2) + storage_dead(ptr_14) + storage_dead(ptr_15) return } diff --git a/charon/tests/ui/simple/box-dyn-fnonce.out b/charon/tests/ui/simple/box-dyn-fnonce.out index 59b4ceca3..39181177c 100644 --- a/charon/tests/ui/simple/box-dyn-fnonce.out +++ b/charon/tests/ui/simple/box-dyn-fnonce.out @@ -1,5 +1,5 @@ error: trying to access the allocator field from Box, but it is being treated as a builtin (without allocator) - --> /rustc/library/alloc/src/boxed.rs:2259:51 + --> /rustc/library/alloc/src/boxed.rs:2277:51 note: the error occurred when translating `alloc::boxed::{impl core::ops::function::FnOnce for alloc::boxed::Box[TraitClause1, TraitClause2]}::call_once`, which is (transitively) used at the following location(s): --> tests/ui/simple/box-dyn-fnonce.rs:4:5 @@ -7,7 +7,7 @@ note: the error occurred when translating `alloc::boxed::{impl core::ops::functi 4 | f(); | --- error: trying to access the allocator field from Box, but it is being treated as a builtin (without allocator) - --> /rustc/library/alloc/src/boxed.rs:1940:17 + --> /rustc/library/alloc/src/boxed.rs:1958:17 note: the error occurred when translating `alloc::boxed::{impl core::ops::drop::Drop for alloc::boxed::Box[TraitClause0, TraitClause1]}::drop`, which is (transitively) used at the following location(s): --> tests/ui/simple/box-dyn-fnonce.rs:4:5 diff --git a/charon/tests/ui/simple/builtin-drop-mono.out b/charon/tests/ui/simple/builtin-drop-mono.out index 041089f10..729a49b13 100644 --- a/charon/tests/ui/simple/builtin-drop-mono.out +++ b/charon/tests/ui/simple/builtin-drop-mono.out @@ -49,6 +49,11 @@ unsafe fn core::marker::Destruct::drop_in_place::<(String, String)>(_1: *mut (St unsafe fn core::marker::Destruct::drop_in_place::(_1: *mut String) = +// Full name: core::ptr::drop_glue::<[String]> +#[lang_item("drop_glue")] +unsafe fn drop_glue::<[String]><'_0>(_1: &'_0 mut [String]) += + // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box<[String]>[{built_in impl MetaSized for [String]}, {built_in impl Sized for Global}, {impl Destruct for [String]}, {impl Destruct for Global}]} impl Destruct for alloc::boxed::Box<[String]>[{built_in impl MetaSized for [String]}, {built_in impl Sized for Global}, {impl Destruct for [String]}, {impl Destruct for Global}] { non-dyn-compatible @@ -73,45 +78,13 @@ impl Destruct for (String, String) { unsafe fn {impl Destruct for [String; 4 : usize]}::drop_in_place::(_1: *mut [String; 4 : usize]) { let _0: (); // return - let _1: *mut [String; 4 : usize]; // arg #1 - let _2: &'1 mut [String; 4 : usize]; // anonymous local - let _3: *mut [String; 4 : usize]; // anonymous local - let _4: *mut [String]; // anonymous local - let _5: usize; // anonymous local - let _6: usize; // anonymous local - let _7: *mut String; // anonymous local - let _8: bool; // anonymous local - let _9: &'_ mut [String]; // anonymous local - let _10: &'_ mut String; // anonymous local + let _1: &'1 mut [String; 4 : usize]; // arg #1 + let _2: &'3 mut [String]; // anonymous local storage_live(_2) - storage_live(_3) - storage_live(_4) - storage_live(_5) - storage_live(_6) - storage_live(_7) - storage_live(_8) _0 = () - _2 = &mut (*_1) - _3 = &raw mut (*_2) - _4 = unsize_cast<*mut [String; 4 : usize], *mut [String], 4 : usize>(move _3) - _5 = copy _4.metadata - _6 = const 0 : usize - loop { - _8 = copy _6 == copy _5 - if move _8 { - break 0 - } else { - storage_live(_9) - _9 = &mut (*_4) with_metadata(copy _4.metadata) - storage_live(_10) - _10 = @SliceIndexMut<'_, String>(move _9, copy _6) - _7 = &raw mut (*_10) - _6 = move _6 wrap.+ const 1 : usize - drop[{impl Destruct for String}::drop_in_place] (*_7) - continue 0 - } - } + _2 = @ArrayToSliceMut<'_, String, 4 : usize>(move _1) + _0 = drop_glue::<[String]><'6>(move _2) return } @@ -119,36 +92,33 @@ unsafe fn {impl Destruct for [String; 4 : usize]}::drop_in_place::(_1: *mut [String]) { let _0: (); // return - let _1: *mut [String]; // arg #1 - let _2: &'1 mut [String]; // anonymous local + let _1: &'1 mut [String]; // arg #1 + let _2: usize; // anonymous local let _3: usize; // anonymous local - let _4: usize; // anonymous local - let _5: *mut String; // anonymous local - let _6: bool; // anonymous local - let _7: &'_ mut [String]; // anonymous local - let _8: &'_ mut String; // anonymous local + let _4: *mut String; // anonymous local + let _5: bool; // anonymous local + let _6: &'_ mut [String]; // anonymous local + let _7: &'_ mut String; // anonymous local storage_live(_2) storage_live(_3) storage_live(_4) storage_live(_5) - storage_live(_6) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - _3 = copy _2.metadata - _4 = const 0 : usize + _2 = copy _1.metadata + _3 = const 0 : usize loop { - _6 = copy _4 == copy _3 - if move _6 { + _5 = copy _3 == copy _2 + if move _5 { break 0 } else { + storage_live(_6) + _6 = &mut (*_1) with_metadata(copy _1.metadata) storage_live(_7) - _7 = &mut (*_2) with_metadata(copy _2.metadata) - storage_live(_8) - _8 = @SliceIndexMut<'_, String>(move _7, copy _4) - _5 = &raw mut (*_8) - _4 = move _4 wrap.+ const 1 : usize - drop[{impl Destruct for String}::drop_in_place] (*_5) + _7 = @SliceIndexMut<'_, String>(move _6, copy _3) + _4 = &raw mut (*_7) + _3 = move _3 wrap.+ const 1 : usize + drop[{impl Destruct for String}::drop_in_place] (*_4) continue 0 } } @@ -159,14 +129,11 @@ unsafe fn {impl Destruct for [String]}::drop_in_place::(_1: *mut [String unsafe fn {impl Destruct for (String, String)}::drop_in_place::(_1: *mut (String, String)) { let _0: (); // return - let _1: *mut (String, String); // arg #1 - let _2: &'1 mut (String, String); // anonymous local + let _1: &'1 mut (String, String); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - drop[{impl Destruct for String}::drop_in_place] (*_2).0 - drop[{impl Destruct for String}::drop_in_place] (*_2).1 + drop[{impl Destruct for String}::drop_in_place] (*_1).0 + drop[{impl Destruct for String}::drop_in_place] (*_1).1 return } diff --git a/charon/tests/ui/simple/builtin-drop.out b/charon/tests/ui/simple/builtin-drop.out index 2fbd98d57..00b7a23f8 100644 --- a/charon/tests/ui/simple/builtin-drop.out +++ b/charon/tests/ui/simple/builtin-drop.out @@ -23,6 +23,14 @@ pub trait Destruct unsafe fn core::marker::Destruct::drop_in_place(_1: *mut Self) = +// Full name: core::ptr::drop_glue +#[lang_item("drop_glue")] +unsafe fn drop_glue<'_0, T>(_1: &'_0 mut T) +where + TraitClause0: (T: Destruct), + TraitClause1: (T: Destruct), += + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} @@ -60,115 +68,80 @@ impl Destruct for String { non-dyn-compatible } -// Full name: test_crate::::{impl Destruct for [T; N]}::drop_in_place -unsafe fn {impl Destruct for [T; N]}::drop_in_place(_1: *mut [T; N]) +// Full name: test_crate::::{impl Destruct for [T]}::drop_in_place +unsafe fn {impl Destruct for [T]}::drop_in_place(_1: *mut [T]) where TraitClause0: (T: Sized), TraitClause1: (T: Destruct), { let _0: (); // return - let _1: *mut [T; N]; // arg #1 - let _2: &'1 mut [T; N]; // anonymous local - let _3: *mut [T; N]; // anonymous local - let _4: *mut [T]; // anonymous local - let _5: usize; // anonymous local - let _6: usize; // anonymous local - let _7: *mut T; // anonymous local - let _8: bool; // anonymous local - let _9: &'_ mut [T]; // anonymous local - let _10: &'_ mut T; // anonymous local + let _1: &'1 mut [T]; // arg #1 + let _2: usize; // anonymous local + let _3: usize; // anonymous local + let _4: *mut T; // anonymous local + let _5: bool; // anonymous local + let _6: &'_ mut [T]; // anonymous local + let _7: &'_ mut T; // anonymous local storage_live(_2) storage_live(_3) storage_live(_4) storage_live(_5) - storage_live(_6) - storage_live(_7) - storage_live(_8) _0 = () - _2 = &mut (*_1) - _3 = &raw mut (*_2) - _4 = unsize_cast<*mut [T; N], *mut [T], N>(move _3) - _5 = copy _4.metadata - _6 = const 0 : usize + _2 = copy _1.metadata + _3 = const 0 : usize loop { - _8 = copy _6 == copy _5 - if move _8 { + _5 = copy _3 == copy _2 + if move _5 { break 0 } else { - storage_live(_9) - _9 = &mut (*_4) with_metadata(copy _4.metadata) - storage_live(_10) - _10 = @SliceIndexMut<'_, T>(move _9, copy _6) - _7 = &raw mut (*_10) - _6 = move _6 wrap.+ const 1 : usize - drop[TraitClause1::drop_in_place] (*_7) + storage_live(_6) + _6 = &mut (*_1) with_metadata(copy _1.metadata) + storage_live(_7) + _7 = @SliceIndexMut<'_, T>(move _6, copy _3) + _4 = &raw mut (*_7) + _3 = move _3 wrap.+ const 1 : usize + drop[TraitClause1::drop_in_place] (*_4) continue 0 } } return } -// Full name: test_crate::::{impl Destruct for [T; N]} -impl Destruct for [T; N] +// Full name: test_crate::::{impl Destruct for [T]} +impl Destruct for [T] where TraitClause0: (T: Sized), TraitClause1: (T: Destruct), { - fn drop_in_place = {impl Destruct for [T; N]}::drop_in_place[TraitClause0, TraitClause1] + fn drop_in_place = {impl Destruct for [T]}::drop_in_place[TraitClause0, TraitClause1] non-dyn-compatible } -// Full name: test_crate::::{impl Destruct for [T]}::drop_in_place -unsafe fn {impl Destruct for [T]}::drop_in_place(_1: *mut [T]) +// Full name: test_crate::::{impl Destruct for [T; N]}::drop_in_place +unsafe fn {impl Destruct for [T; N]}::drop_in_place(_1: *mut [T; N]) where TraitClause0: (T: Sized), TraitClause1: (T: Destruct), { let _0: (); // return - let _1: *mut [T]; // arg #1 - let _2: &'1 mut [T]; // anonymous local - let _3: usize; // anonymous local - let _4: usize; // anonymous local - let _5: *mut T; // anonymous local - let _6: bool; // anonymous local - let _7: &'_ mut [T]; // anonymous local - let _8: &'_ mut T; // anonymous local + let _1: &'1 mut [T; N]; // arg #1 + let _2: &'3 mut [T]; // anonymous local storage_live(_2) - storage_live(_3) - storage_live(_4) - storage_live(_5) - storage_live(_6) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - _3 = copy _2.metadata - _4 = const 0 : usize - loop { - _6 = copy _4 == copy _3 - if move _6 { - break 0 - } else { - storage_live(_7) - _7 = &mut (*_2) with_metadata(copy _2.metadata) - storage_live(_8) - _8 = @SliceIndexMut<'_, T>(move _7, copy _4) - _5 = &raw mut (*_8) - _4 = move _4 wrap.+ const 1 : usize - drop[TraitClause1::drop_in_place] (*_5) - continue 0 - } - } + _2 = @ArrayToSliceMut<'_, T, N>(move _1) + _0 = drop_glue<'6, [T]>[{impl Destruct for [T]}[TraitClause0, TraitClause1], {impl Destruct for [T]}[TraitClause0, TraitClause1]](move _2) return } -// Full name: test_crate::::{impl Destruct for [T]} -impl Destruct for [T] +// Full name: test_crate::::{impl Destruct for [T; N]} +impl Destruct for [T; N] where TraitClause0: (T: Sized), TraitClause1: (T: Destruct), { - fn drop_in_place = {impl Destruct for [T]}::drop_in_place[TraitClause0, TraitClause1] + fn drop_in_place = {impl Destruct for [T; N]}::drop_in_place[TraitClause0, TraitClause1] non-dyn-compatible } @@ -180,14 +153,11 @@ where TraitClause2: (B: Destruct), { let _0: (); // return - let _1: *mut (A, B); // arg #1 - let _2: &'1 mut (A, B); // anonymous local + let _1: &'1 mut (A, B); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - drop[TraitClause1::drop_in_place] (*_2).0 - drop[TraitClause2::drop_in_place] (*_2).1 + drop[TraitClause1::drop_in_place] (*_1).0 + drop[TraitClause2::drop_in_place] (*_1).1 return } diff --git a/charon/tests/ui/simple/closure-fnonce.out b/charon/tests/ui/simple/closure-fnonce.out index d48247290..c30095d38 100644 --- a/charon/tests/ui/simple/closure-fnonce.out +++ b/charon/tests/ui/simple/closure-fnonce.out @@ -87,12 +87,9 @@ struct NotCopy {} unsafe fn {impl Destruct for NotCopy}::drop_in_place(_1: *mut NotCopy) { let _0: (); // return - let _1: *mut NotCopy; // arg #1 - let _2: &'1 mut NotCopy; // anonymous local + let _1: &'1 mut NotCopy; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index 5fc96f95d..154eac398 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -97,13 +97,10 @@ trait Thing unsafe fn {impl Destruct for (A,)}::drop_in_place(_1: *mut (A,)) { let _0: (); // return - let _1: *mut (A,); // arg #1 - let _2: &'1 mut (A,); // anonymous local + let _1: &'1 mut (A,); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - drop[{built_in impl Destruct for A}::drop_in_place] (*_2).0 + drop[{built_in impl Destruct for A}::drop_in_place] (*_1).0 return } diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out index e8e52a273..965b0d7c4 100644 --- a/charon/tests/ui/simple/closure-with-drops.out +++ b/charon/tests/ui/simple/closure-with-drops.out @@ -114,13 +114,10 @@ where TraitClause1: (T: Destruct), { let _0: (); // return - let _1: *mut test_crate::foo::closure[TraitClause0, TraitClause1]; // arg #1 - let _2: &'1 mut test_crate::foo::closure[TraitClause0, TraitClause1]; // anonymous local + let _1: &'1 mut test_crate::foo::closure[TraitClause0, TraitClause1]; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - drop[TraitClause1::drop_in_place] ((*_2)).0 + drop[TraitClause1::drop_in_place] ((*_1)).0 return } @@ -210,12 +207,9 @@ fn bar() unsafe fn {impl Destruct for test_crate::bar::closure}::drop_in_place(_1: *mut test_crate::bar::closure) { let _0: (); // return - let _1: *mut test_crate::bar::closure; // arg #1 - let _2: &'1 mut test_crate::bar::closure; // anonymous local + let _1: &'1 mut test_crate::bar::closure; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/simple/drop-cow.out b/charon/tests/ui/simple/drop-cow.out index 667758fae..e10b5edca 100644 --- a/charon/tests/ui/simple/drop-cow.out +++ b/charon/tests/ui/simple/drop-cow.out @@ -85,17 +85,14 @@ where TypeOutlives1: B: 'a, { let _0: (); // return - let _1: *mut Cow<'a, B>[TraitClause0, TraitClause1, TraitClause2]; // arg #1 - let _2: &'1 mut Cow<'a, B>[TraitClause0, TraitClause1, TraitClause2]; // anonymous local + let _1: &'1 mut Cow<'a, B>[TraitClause0, TraitClause1, TraitClause2]; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - match (*_2) { + match (*_1) { Cow::Borrowed => { }, _ => { - drop[TraitClause1::ImpliedClause4::drop_in_place] ((*_2) as variant Cow::Owned).0 + drop[TraitClause1::ImpliedClause4::drop_in_place] ((*_1) as variant Cow::Owned).0 return }, } diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic.out b/charon/tests/ui/simple/drop-glue-with-const-generic.out index 08bec9022..8b380a1ee 100644 --- a/charon/tests/ui/simple/drop-glue-with-const-generic.out +++ b/charon/tests/ui/simple/drop-glue-with-const-generic.out @@ -1,4 +1,4 @@ -error: internal compiler error: /rustc-dev/e9e32aca5a4ffd08cbc29547b039d64b92a2c03b/compiler/rustc_middle/src/ty/sty.rs:354:13: cannot find `K/#0` in param-env: ParamEnv { +error: internal compiler error: /rustc-dev/f8a08b688cbe60acc386ed1fbd1b7cbaaf5576b1/compiler/rustc_middle/src/ty/sty.rs:360:13: cannot find `K/#0` in param-env: ParamEnv { caller_bounds: [ Binder { value: HostEffectPredicate { trait_ref: , constness: Maybe }, bound_vars: [] }, Binder { value: TraitPredicate(, polarity:Positive), bound_vars: [] }, @@ -6,7 +6,7 @@ error: internal compiler error: /rustc-dev/e9e32aca5a4ffd08cbc29547b039d64b92a2c } -thread 'rustc' panicked at /rustc-dev/e9e32aca5a4ffd08cbc29547b039d64b92a2c03b/compiler/rustc_middle/src/ty/sty.rs:354:13: +thread 'rustc' panicked at /rustc-dev/f8a08b688cbe60acc386ed1fbd1b7cbaaf5576b1/compiler/rustc_middle/src/ty/sty.rs:360:13: Box note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace error: rustc panicked while retrieving drop glue. This is known to happen with `--precise-drops`; to silence this warning, pass `--opaque '{impl core::marker::Destruct for test_crate::PortableHash}'` to charon diff --git a/charon/tests/ui/simple/drop-string-desugar.out b/charon/tests/ui/simple/drop-string-desugar.out index 5a955ffd5..211c2aa78 100644 --- a/charon/tests/ui/simple/drop-string-desugar.out +++ b/charon/tests/ui/simple/drop-string-desugar.out @@ -65,18 +65,15 @@ where unsafe fn {impl Destruct for String}::drop_in_place(_1: *mut String) { let _0: (); // return - let _1: *mut String; // arg #1 - let _2: &'1 mut String; // anonymous local - let drop_arg_3: *mut Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}]; // local - let drop_ret_4: (); // local + let _1: &'1 mut String; // arg #1 + let drop_arg_2: *mut Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}]; // local + let drop_ret_3: (); // local - storage_live(_2) _0 = () - _2 = &mut (*_1) - storage_live(drop_arg_3) - drop_arg_3 = &raw mut ((*_2)).vec - storage_live(drop_ret_4) - drop_ret_4 = {impl Destruct for Vec[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}](move drop_arg_3) + storage_live(drop_arg_2) + drop_arg_2 = &raw mut ((*_1)).vec + storage_live(drop_ret_3) + drop_ret_3 = {impl Destruct for Vec[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}](move drop_arg_2) return } diff --git a/charon/tests/ui/simple/drop-string.out b/charon/tests/ui/simple/drop-string.out index abbe36796..25d64e1fb 100644 --- a/charon/tests/ui/simple/drop-string.out +++ b/charon/tests/ui/simple/drop-string.out @@ -65,13 +65,10 @@ where unsafe fn {impl Destruct for String}::drop_in_place(_1: *mut String) { let _0: (); // return - let _1: *mut String; // arg #1 - let _2: &'1 mut String; // anonymous local + let _1: &'1 mut String; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - drop[{impl Destruct for Vec[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}]] ((*_2)).vec + drop[{impl Destruct for Vec[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}, {built_in impl Destruct for u8}, {impl Destruct for Global}]] ((*_1)).vec return } diff --git a/charon/tests/ui/simple/dyn-cast-to-supertrait.out b/charon/tests/ui/simple/dyn-cast-to-supertrait.out index 627d6ece5..0e9bc5e13 100644 --- a/charon/tests/ui/simple/dyn-cast-to-supertrait.out +++ b/charon/tests/ui/simple/dyn-cast-to-supertrait.out @@ -91,12 +91,9 @@ struct HouseCat {} unsafe fn {impl Destruct for HouseCat}::drop_in_place(_1: *mut HouseCat) { let _0: (); // return - let _1: *mut HouseCat; // arg #1 - let _2: &'1 mut HouseCat; // anonymous local + let _1: &'1 mut HouseCat; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) return } diff --git a/charon/tests/ui/simple/lending-iterator-gat.out b/charon/tests/ui/simple/lending-iterator-gat.out index 1639eb13a..9456877ad 100644 --- a/charon/tests/ui/simple/lending-iterator-gat.out +++ b/charon/tests/ui/simple/lending-iterator-gat.out @@ -109,13 +109,10 @@ pub trait LendingIterator unsafe fn {impl Destruct for (A,)}::drop_in_place(_1: *mut (A,)) { let _0: (); // return - let _1: *mut (A,); // arg #1 - let _2: &'1 mut (A,); // anonymous local + let _1: &'1 mut (A,); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - drop[{built_in impl Destruct for A}::drop_in_place] (*_2).0 + drop[{built_in impl Destruct for A}::drop_in_place] (*_1).0 return } diff --git a/charon/tests/ui/simple/single-variant-enum-drop-glue.out b/charon/tests/ui/simple/single-variant-enum-drop-glue.out index 1d32d0ffe..453cce2e8 100644 --- a/charon/tests/ui/simple/single-variant-enum-drop-glue.out +++ b/charon/tests/ui/simple/single-variant-enum-drop-glue.out @@ -43,17 +43,14 @@ pub enum Thing { unsafe fn {impl Destruct for Thing}::drop_in_place(_1: *mut Thing) { let _0: (); // return - let _1: *mut Thing; // arg #1 - let _2: &'1 mut Thing; // anonymous local + let _1: &'1 mut Thing; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - match (*_2) { + match (*_1) { _ => { }, } - drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1]}::drop_in_place<(), Global>[{built_in impl MetaSized for ()}, {built_in impl Sized for Global}]] ((*_2) as variant Thing::A).0 + drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1]}::drop_in_place<(), Global>[{built_in impl MetaSized for ()}, {built_in impl Sized for Global}]] ((*_1) as variant Thing::A).0 return } diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index 2a03c5994..b3fe109bc 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -90,21 +90,21 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &start_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -113,17 +113,17 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _7 = Argument { ty: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -132,10 +132,10 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _8 = Argument { ty: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -148,6 +148,7 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _3 = Arguments { template: move _20, args: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -182,21 +183,21 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &end_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -205,17 +206,17 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _7 = Argument { ty: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -224,10 +225,10 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _8 = Argument { ty: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -240,6 +241,7 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _3 = Arguments { template: move _20, args: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -274,21 +276,21 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &start_1 args_5 = &end_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -297,17 +299,17 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _7 = Argument { ty: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -316,10 +318,10 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _8 = Argument { ty: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -332,6 +334,7 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _3 = Arguments { template: move _20, args: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -366,21 +369,21 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &end_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -389,17 +392,17 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _7 = Argument { ty: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -408,10 +411,10 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _8 = Argument { ty: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -424,6 +427,7 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _3 = Arguments { template: move _20, args: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -729,13 +733,12 @@ where storage_live(start_3) storage_live(end_4) - storage_live(exhausted_5) - storage_live(len_6) - storage_live(new_len_13) storage_live(_16) start_3 = copy (self_1).start end_4 = copy (self_1).end + storage_live(exhausted_5) exhausted_5 = copy (self_1).exhausted + storage_live(len_6) len_6 = copy slice_2.metadata storage_live(_7) storage_live(_8) @@ -767,13 +770,14 @@ where storage_dead(_17) storage_dead(rhs_12) storage_dead(self_11) + storage_live(new_len_13) new_len_13 = copy (_10 as variant Option::Some).0 storage_live(_14) storage_live(ptr_15) ptr_15 = &raw mut (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_19) - storage_live(_20) _19 = cast<*mut [T], *mut T>(copy ptr_15) + storage_live(_20) _20 = copy _19 offset copy start_3 _14 = @PtrFromPartsMut<'_, [T]>(copy _20, copy new_len_13) storage_dead(_20) @@ -781,8 +785,11 @@ where storage_dead(ptr_15) _0 = &mut (*_14) with_metadata(copy _14.metadata) storage_dead(_14) + storage_dead(new_len_13) storage_dead(_10) storage_dead(_7) + storage_dead(len_6) + storage_dead(exhausted_5) return } storage_dead(_17) @@ -825,13 +832,12 @@ where storage_live(start_3) storage_live(end_4) - storage_live(exhausted_5) - storage_live(len_6) - storage_live(new_len_13) storage_live(_16) start_3 = copy (self_1).start end_4 = copy (self_1).end + storage_live(exhausted_5) exhausted_5 = copy (self_1).exhausted + storage_live(len_6) len_6 = copy slice_2.metadata storage_live(_7) storage_live(_8) @@ -863,13 +869,14 @@ where storage_dead(_17) storage_dead(rhs_12) storage_dead(self_11) + storage_live(new_len_13) new_len_13 = copy (_10 as variant Option::Some).0 storage_live(_14) storage_live(_15) _15 = &raw const (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_19) - storage_live(_20) _19 = cast<*const [T], *const T>(copy _15) + storage_live(_20) _20 = copy _19 offset copy start_3 _14 = @PtrFromPartsShared<'_, [T]>(copy _20, copy new_len_13) storage_dead(_20) @@ -877,8 +884,11 @@ where storage_dead(_15) _0 = &(*_14) with_metadata(copy _14.metadata) storage_dead(_14) + storage_dead(new_len_13) storage_dead(_10) storage_dead(_7) + storage_dead(len_6) + storage_dead(exhausted_5) return } storage_dead(_17) @@ -991,7 +1001,8 @@ where self_9 = copy exclusive_end_3 } else { } - storage_live(new_len_6) + storage_dead(self_10) + storage_dead(self_11) storage_live(_12) _12 = ub_checks if move _12 { @@ -1001,10 +1012,11 @@ where storage_dead(_5) } else { } + storage_live(new_len_6) new_len_6 = copy exclusive_end_3 ub.- copy self_9 storage_live(_7) - storage_live(_8) _7 = cast<*mut [T], *mut T>(copy slice_2) + storage_live(_8) _8 = copy _7 offset copy self_9 _0 = @PtrFromPartsMut<'_, [T]>(copy _8, copy new_len_6) storage_dead(_8) @@ -1112,7 +1124,8 @@ where self_9 = copy exclusive_end_3 } else { } - storage_live(new_len_6) + storage_dead(self_10) + storage_dead(self_11) storage_live(_12) _12 = ub_checks if move _12 { @@ -1122,10 +1135,11 @@ where storage_dead(_5) } else { } + storage_live(new_len_6) new_len_6 = copy exclusive_end_3 ub.- copy self_9 storage_live(_7) - storage_live(_8) _7 = cast<*const [T], *const T>(copy slice_2) + storage_live(_8) _8 = copy _7 offset copy self_9 _0 = @PtrFromPartsShared<'_, [T]>(copy _8, copy new_len_6) storage_dead(_8) @@ -1164,7 +1178,6 @@ where storage_live(exclusive_end_6) storage_live(new_len_12) storage_live(self_15) - storage_live(self_16) storage_live(_3) self_4 = copy (self_1).end _5 = copy slice_2.metadata @@ -1174,6 +1187,7 @@ where _17 = Option::None { } _0 = move _17 } else { + storage_live(self_16) self_15 = move (self_1).start self_16 = move (self_1).exhausted exclusive_end_6 = copy self_4 wrap.+ const 1 : usize @@ -1181,7 +1195,7 @@ where self_15 = copy exclusive_end_6 } else { } - storage_live(_8) + storage_dead(self_16) storage_live(_11) _11 = copy exclusive_end_6 < copy self_15 if move _11 { @@ -1195,12 +1209,13 @@ where storage_live(_7) _7 = copy exclusive_end_6 <= copy _5 if move _7 { + storage_live(_8) storage_live(_9) storage_live(ptr_10) ptr_10 = &raw mut (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_13) - storage_live(_14) _13 = cast<*mut [T], *mut T>(copy ptr_10) + storage_live(_14) _14 = copy _13 offset copy self_15 _9 = @PtrFromPartsMut<'_, [T]>(copy _14, copy new_len_12) storage_dead(_14) @@ -1209,6 +1224,7 @@ where _8 = &mut (*_9) with_metadata(copy _9.metadata) _0 = Option::Some { 0: copy _8 } storage_dead(_9) + storage_dead(_8) } else { storage_live(_18) _18 = Option::None { } @@ -1216,7 +1232,6 @@ where } } storage_dead(_7) - storage_dead(_8) } storage_dead(_3) return @@ -1252,7 +1267,6 @@ where storage_live(exclusive_end_6) storage_live(new_len_12) storage_live(self_15) - storage_live(self_16) storage_live(_3) self_4 = copy (self_1).end _5 = copy slice_2.metadata @@ -1262,6 +1276,7 @@ where _17 = Option::None { } _0 = move _17 } else { + storage_live(self_16) self_15 = move (self_1).start self_16 = move (self_1).exhausted exclusive_end_6 = copy self_4 wrap.+ const 1 : usize @@ -1269,7 +1284,7 @@ where self_15 = copy exclusive_end_6 } else { } - storage_live(_8) + storage_dead(self_16) storage_live(_11) _11 = copy exclusive_end_6 < copy self_15 if move _11 { @@ -1283,12 +1298,13 @@ where storage_live(_7) _7 = copy exclusive_end_6 <= copy _5 if move _7 { + storage_live(_8) storage_live(_9) storage_live(_10) _10 = &raw const (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_13) - storage_live(_14) _13 = cast<*const [T], *const T>(copy _10) + storage_live(_14) _14 = copy _13 offset copy self_15 _9 = @PtrFromPartsShared<'_, [T]>(copy _14, copy new_len_12) storage_dead(_14) @@ -1297,6 +1313,7 @@ where _8 = &(*_9) with_metadata(copy _9.metadata) _0 = Option::Some { 0: copy _8 } storage_dead(_9) + storage_dead(_8) } else { storage_live(_18) _18 = Option::None { } @@ -1304,7 +1321,6 @@ where } } storage_dead(_7) - storage_dead(_8) } storage_dead(_3) return diff --git a/charon/tests/ui/simple/struct-with-drops.out b/charon/tests/ui/simple/struct-with-drops.out index a8d99a046..92bcb77b5 100644 --- a/charon/tests/ui/simple/struct-with-drops.out +++ b/charon/tests/ui/simple/struct-with-drops.out @@ -88,20 +88,17 @@ pub fn {impl Drop for B}::drop<'_0>(self_1: &'_0 mut B) unsafe fn {impl Destruct for B}::drop_in_place(_1: *mut B) { let _0: (); // return - let _1: *mut B; // arg #1 - let _2: &'1 mut B; // anonymous local - let _3: &'2 mut B; // anonymous local - let _4: (); // anonymous local + let _1: &'1 mut B; // arg #1 + let _2: &'2 mut B; // anonymous local + let _3: (); // anonymous local storage_live(_2) storage_live(_3) - storage_live(_4) _0 = () _2 = &mut (*_1) - _3 = &mut (*_2) - _4 = {impl Drop for B}::drop<'4>(move _3) - drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_2)).x - drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_2)).y + _3 = {impl Drop for B}::drop<'4>(move _2) + drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_1)).x + drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_1)).y return } @@ -109,14 +106,11 @@ unsafe fn {impl Destruct for B}::drop_in_place(_1: *mut B) unsafe fn {impl Destruct for A}::drop_in_place(_1: *mut A) { let _0: (); // return - let _1: *mut A; // arg #1 - let _2: &'1 mut A; // anonymous local + let _1: &'1 mut A; // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) - drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_2)).x - drop[{impl Destruct for B}::drop_in_place] ((*_2)).b + drop[{impl Destruct for alloc::boxed::Box[TraitClause0, TraitClause1, TraitClause2, TraitClause3]}::drop_in_place[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}]] ((*_1)).x + drop[{impl Destruct for B}::drop_in_place] ((*_1)).b return } diff --git a/charon/tests/ui/simple/vec-push.out b/charon/tests/ui/simple/vec-push.out index 44c390aec..e9da198de 100644 --- a/charon/tests/ui/simple/vec-push.out +++ b/charon/tests/ui/simple/vec-push.out @@ -209,9 +209,9 @@ where let self_11: UsizeNoHighBit; // local let _12: NonNull; // anonymous local - storage_live(len_3) storage_live(_6) storage_live(end_8) + storage_live(len_3) len_3 = copy ((*self_1)).len storage_live(_4) storage_live(_5) @@ -250,6 +250,7 @@ where storage_dead(src_10) ((*self_1)).len = copy len_3 wrap.+ const 1 : usize _0 = &mut (*end_8) + storage_dead(len_3) return } diff --git a/charon/tests/ui/slice-index-range.out b/charon/tests/ui/slice-index-range.out index 30d9ccaa4..174cb739f 100644 --- a/charon/tests/ui/slice-index-range.out +++ b/charon/tests/ui/slice-index-range.out @@ -103,21 +103,21 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &start_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -126,17 +126,17 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _7 = Argument { 0: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -145,10 +145,10 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _8 = Argument { 0: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -161,6 +161,7 @@ fn core::slice::index::slice_index_fail::do_panic::runtime(start_1: usize, len_2 _3 = Arguments { 0: move _20, 1: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -195,21 +196,21 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &end_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -218,17 +219,17 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _7 = Argument { 0: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -237,10 +238,10 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _8 = Argument { 0: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -253,6 +254,7 @@ fn core::slice::index::slice_index_fail::do_panic#1::runtime(end_1: usize, len_2 _3 = Arguments { 0: move _20, 1: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -287,21 +289,21 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &start_1 args_5 = &end_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -310,17 +312,17 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _7 = Argument { 0: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -329,10 +331,10 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _8 = Argument { 0: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -345,6 +347,7 @@ fn core::slice::index::slice_index_fail::do_panic#2::runtime(start_1: usize, end _3 = Arguments { 0: move _20, 1: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -379,21 +382,21 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 storage_live(args_4) storage_live(args_5) - storage_live(args_9) storage_live(_3) args_4 = &end_1 args_5 = &len_2 storage_live(args_6) storage_live(_7) - storage_live(_13) storage_live(_14) storage_live(_10) storage_live(_11) _14 = &raw const (*args_4) _11 = transmute<*const usize, NonNull<()>>(copy _14) storage_live(_12) + storage_live(_13) _13 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'25, '26, '27>) _12 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _13) + storage_dead(_13) storage_live(_22) _22 = PhantomData { } _10 = ArgumentType::Placeholder { value: move _11, formatter: copy _12, _lifetime: move _22 } @@ -402,17 +405,17 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _7 = Argument { 0: move _10 } storage_dead(_10) storage_dead(_14) - storage_dead(_13) storage_live(_8) - storage_live(_18) storage_live(_19) storage_live(_15) storage_live(_16) _19 = &raw const (*args_5) _16 = transmute<*const usize, NonNull<()>>(copy _19) storage_live(_17) + storage_live(_18) _18 = cast {impl Display for usize}::fmt<'_0_1, '_1_1, '_2_1>, fn<'_0_1, '_1_1, '_2_1>(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(const {impl Display for usize}::fmt<'36, '37, '38>) _17 = transmute(&'_0_1 usize, &'_1_1 mut Formatter<'_2_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut Formatter<'_1_1>) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}]>(copy _18) + storage_dead(_18) storage_live(_23) _23 = PhantomData { } _15 = ArgumentType::Placeholder { value: move _16, formatter: copy _17, _lifetime: move _23 } @@ -421,10 +424,10 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _8 = Argument { 0: move _15 } storage_dead(_15) storage_dead(_19) - storage_dead(_18) args_6 = [move _7, move _8] storage_dead(_8) storage_dead(_7) + storage_live(args_9) args_9 = &args_6 storage_live(_20) storage_live(_24) @@ -437,6 +440,7 @@ fn core::slice::index::slice_index_fail::do_panic#3::runtime(end_1: usize, len_2 _3 = Arguments { 0: move _20, 1: move _21 } storage_dead(_21) storage_dead(_20) + storage_dead(args_9) panic(core::panicking::panic_fmt) } @@ -716,7 +720,6 @@ where storage_live(self_4) storage_live(rhs_5) - storage_live(new_len_6) storage_live(_11) storage_live(_3) self_4 = copy (self_1).end @@ -731,6 +734,7 @@ where _3 = Option::Some { 0: move _14 } storage_dead(_14) storage_dead(_13) + storage_live(new_len_6) new_len_6 = copy (_3 as variant Option::Some).0 storage_live(_7) storage_live(_8) @@ -742,8 +746,8 @@ where storage_live(ptr_10) ptr_10 = &raw mut (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_15) - storage_live(_16) _15 = cast<*mut [T], *mut T>(copy ptr_10) + storage_live(_16) _16 = copy _15 offset copy rhs_5 _9 = @PtrFromPartsMut<'_, [T]>(copy _16, copy new_len_6) storage_dead(_16) @@ -751,11 +755,13 @@ where storage_dead(ptr_10) _0 = &mut (*_9) with_metadata(copy _9.metadata) storage_dead(_9) + storage_dead(new_len_6) storage_dead(_3) storage_dead(_7) return } else { storage_dead(_8) + storage_dead(new_len_6) } } storage_dead(_3) @@ -789,7 +795,6 @@ where storage_live(self_4) storage_live(rhs_5) - storage_live(new_len_6) storage_live(_11) storage_live(_3) self_4 = copy (self_1).end @@ -804,6 +809,7 @@ where _3 = Option::Some { 0: move _14 } storage_dead(_14) storage_dead(_13) + storage_live(new_len_6) new_len_6 = copy (_3 as variant Option::Some).0 storage_live(_7) storage_live(_8) @@ -815,8 +821,8 @@ where storage_live(_10) _10 = &raw const (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_15) - storage_live(_16) _15 = cast<*const [T], *const T>(copy _10) + storage_live(_16) _16 = copy _15 offset copy rhs_5 _9 = @PtrFromPartsShared<'_, [T]>(copy _16, copy new_len_6) storage_dead(_16) @@ -824,11 +830,13 @@ where storage_dead(_10) _0 = &(*_9) with_metadata(copy _9.metadata) storage_dead(_9) + storage_dead(new_len_6) storage_dead(_3) storage_dead(_7) return } else { storage_dead(_8) + storage_dead(new_len_6) } } storage_dead(_3) @@ -924,7 +932,6 @@ where let _12: bool; // anonymous local storage_live(_3) - storage_live(new_len_7) storage_live(offset_9) storage_live(_12) _12 = ub_checks @@ -941,18 +948,20 @@ where storage_dead(_4) } else { } + storage_live(new_len_7) storage_live(_8) _8 = copy (self_1).end offset_9 = copy (self_1).start new_len_7 = move _8 ub.- copy offset_9 storage_dead(_8) storage_live(_10) - storage_live(_11) _10 = cast<*mut [T], *mut T>(copy slice_2) + storage_live(_11) _11 = copy _10 offset copy offset_9 _0 = @PtrFromPartsMut<'_, [T]>(copy _11, copy new_len_7) storage_dead(_11) storage_dead(_10) + storage_dead(new_len_7) return } @@ -1043,7 +1052,6 @@ where let _12: bool; // anonymous local storage_live(_3) - storage_live(new_len_7) storage_live(offset_9) storage_live(_12) _12 = ub_checks @@ -1060,18 +1068,20 @@ where storage_dead(_4) } else { } + storage_live(new_len_7) storage_live(_8) _8 = copy (self_1).end offset_9 = copy (self_1).start new_len_7 = move _8 ub.- copy offset_9 storage_dead(_8) storage_live(_10) - storage_live(_11) _10 = cast<*const [T], *const T>(copy slice_2) + storage_live(_11) _11 = copy _10 offset copy offset_9 _0 = @PtrFromPartsShared<'_, [T]>(copy _11, copy new_len_7) storage_dead(_11) storage_dead(_10) + storage_dead(new_len_7) return } @@ -1100,8 +1110,6 @@ where storage_live(self_4) storage_live(rhs_5) - storage_live(new_len_6) - storage_live(_9) storage_live(_3) self_4 = copy (self_1).end rhs_5 = copy (self_1).start @@ -1119,6 +1127,7 @@ where _3 = Option::Some { 0: move _13 } storage_dead(_13) storage_dead(_12) + storage_live(new_len_6) new_len_6 = copy (_3 as variant Option::Some).0 storage_live(_7) storage_live(_8) @@ -1126,12 +1135,13 @@ where _7 = copy self_4 <= move _8 if move _7 { storage_dead(_8) + storage_live(_9) storage_live(_10) storage_live(ptr_11) ptr_11 = &raw mut (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_14) - storage_live(_15) _14 = cast<*mut [T], *mut T>(copy ptr_11) + storage_live(_15) _15 = copy _14 offset copy rhs_5 _10 = @PtrFromPartsMut<'_, [T]>(copy _15, copy new_len_6) storage_dead(_15) @@ -1140,9 +1150,12 @@ where _9 = &mut (*_10) with_metadata(copy _10.metadata) _0 = Option::Some { 0: copy _9 } storage_dead(_10) + storage_dead(_9) + storage_dead(new_len_6) storage_dead(_3) } else { storage_dead(_8) + storage_dead(new_len_6) storage_dead(_3) storage_live(_16) _16 = Option::None { } @@ -1178,8 +1191,6 @@ where storage_live(self_4) storage_live(rhs_5) - storage_live(new_len_6) - storage_live(_9) storage_live(_3) self_4 = copy (self_1).end rhs_5 = copy (self_1).start @@ -1197,6 +1208,7 @@ where _3 = Option::Some { 0: move _13 } storage_dead(_13) storage_dead(_12) + storage_live(new_len_6) new_len_6 = copy (_3 as variant Option::Some).0 storage_live(_7) storage_live(_8) @@ -1204,12 +1216,13 @@ where _7 = copy self_4 <= move _8 if move _7 { storage_dead(_8) + storage_live(_9) storage_live(_10) storage_live(_11) _11 = &raw const (*slice_2) with_metadata(copy slice_2.metadata) storage_live(_14) - storage_live(_15) _14 = cast<*const [T], *const T>(copy _11) + storage_live(_15) _15 = copy _14 offset copy rhs_5 _10 = @PtrFromPartsShared<'_, [T]>(copy _15, copy new_len_6) storage_dead(_15) @@ -1218,9 +1231,12 @@ where _9 = &(*_10) with_metadata(copy _10.metadata) _0 = Option::Some { 0: copy _9 } storage_dead(_10) + storage_dead(_9) + storage_dead(new_len_6) storage_dead(_3) } else { storage_dead(_8) + storage_dead(new_len_6) storage_dead(_3) storage_live(_16) _16 = Option::None { } diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index b494f7095..812e169d1 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -129,14 +129,11 @@ where TraitClause0: (A: Sized), { let _0: (); // return - let _1: *mut (A, B); // arg #1 - let _2: &'1 mut (A, B); // anonymous local + let _1: &'1 mut (A, B); // arg #1 - storage_live(_2) _0 = () - _2 = &mut (*_1) with_metadata(copy _1.metadata) - drop[{built_in impl Destruct for A}::drop_in_place] (*_2).0 - drop[{built_in impl Destruct for B}::drop_in_place] (*_2).1 + drop[{built_in impl Destruct for A}::drop_in_place] (*_1).0 + drop[{built_in impl Destruct for B}::drop_in_place] (*_1).1 return } diff --git a/flake.nix b/flake.nix index 68c7fa91c..844a2ca99 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ rust-overlay = { # We pin a specific commit because we require a relatively recent version # and flake dependents don't look at our flake.lock. - url = "github:oxalica/rust-overlay/40b0a3a193e0840c76174b4a322874c8f6dd0a63"; + url = "github:oxalica/rust-overlay/51390d0bfca0a68a8c337d215a4bbeddc2ca616e"; inputs.nixpkgs.follows = "nixpkgs"; }; crane.url = "github:ipetkov/crane"; From 65dcdb566e05472a6bca8074318c05f729e30177 Mon Sep 17 00:00:00 2001 From: N1ark Date: Mon, 1 Jun 2026 10:10:36 +0100 Subject: [PATCH 2/2] Add `WithRetag` to `Rvalue::Use` --- charon-ml/src/CharonVersion.ml | 2 +- charon-ml/src/PrintFmt.ml | 2 +- .../src/generated/Generated_Expressions.ml | 6 +++++- charon-ml/src/generated/Generated_OfJson.ml | 15 ++++++++++--- .../src/generated/Generated_OfPostcard.ml | 12 ++++++++++- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/expressions.rs | 11 +++++++++- .../translate/translate_bodies.rs | 21 +++++++++++++------ .../translate/translate_closures.rs | 2 +- .../translate/translate_trait_objects.rs | 11 ++++++---- charon/src/pretty/fmt_with_ctx.rs | 2 +- charon/src/transform/ctx.rs | 2 +- .../reconstruct_fallible_operations.rs | 4 ++-- .../resugar/reconstruct_vec_boxes.rs | 9 +++++--- .../index_intermediate_assigns.rs | 5 ++++- .../index_to_function_calls.rs | 2 +- .../inline_selected_functions.rs | 7 +++++-- .../simplify_output/remove_unit_locals.rs | 2 +- .../simplify_output/simplify_constants.rs | 4 ++-- 20 files changed, 88 insertions(+), 35 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index d1cdda052..201c56597 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.208" +let supported_charon_version = "0.1.209" diff --git a/charon-ml/src/PrintFmt.ml b/charon-ml/src/PrintFmt.ml index f69781467..5bb46d237 100644 --- a/charon-ml/src/PrintFmt.ml +++ b/charon-ml/src/PrintFmt.ml @@ -1355,7 +1355,7 @@ and pp_aggregate (env : fmt_env) (agg : aggregate_kind) (fmt : Format.formatter) and pp_rvalue (env : fmt_env) (fmt : Format.formatter) (rv : rvalue) : unit = match rv with - | Use op -> pp_operand env fmt op + | Use (op, _) -> pp_operand env fmt op | RvRef (p, bk, op) -> begin let p = place_to_string env p in let borrow_kind = diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index 3a57ef9f7..54e06530f 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/charon-ml/src/generated/Generated_Expressions.ml @@ -245,7 +245,7 @@ and projection_elem = the aggregate kind to operands TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions *) and rvalue = - | Use of operand (** Lifts an operand as an rvalue. *) + | Use of operand * with_retag (** Lifts an operand as an rvalue. *) | RvRef of place * borrow_kind * operand (** Takes a reference to the given place. The [Operand] refers to the init value of the metadata, it is [()] if no metadata @@ -317,6 +317,10 @@ and unop = | Neg of overflow_mode (** This can overflow, for [-i::MIN]. *) | Cast of cast_kind (** Casts are rvalues in MIR, but we treat them as unops. *) + +(** Used for [[Rvalue::Use]] to indicate whether the operand should be retagged + (this is used for Rust's aliasing model). *) +and with_retag = NoRetag | YesRetag [@@deriving show, eq, diff --git a/charon-ml/src/generated/Generated_OfJson.ml b/charon-ml/src/generated/Generated_OfJson.ml index 45a0b994c..9c8182dce 100644 --- a/charon-ml/src/generated/Generated_OfJson.ml +++ b/charon-ml/src/generated/Generated_OfJson.ml @@ -1108,9 +1108,10 @@ and region_param_of_json (ctx : of_json_ctx) (js : json) : and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result = combine_error_msgs js __FUNCTION__ (match js with - | `Assoc [ ("Use", use) ] -> - let* use = operand_of_json ctx use in - Ok (Use use) + | `Assoc [ ("Use", `List [ x_0; x_1 ]) ] -> + let* x_0 = operand_of_json ctx x_0 in + let* x_1 = with_retag_of_json ctx x_1 in + Ok (Use (x_0, x_1)) | `Assoc [ ( "Ref", @@ -1546,6 +1547,14 @@ and variant_id_of_json (ctx : of_json_ctx) (js : json) : | x -> VariantId.id_of_json ctx x | _ -> Error "") +and with_retag_of_json (ctx : of_json_ctx) (js : json) : + (with_retag, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `String "No" -> Ok NoRetag + | `String "Yes" -> Ok YesRetag + | _ -> Error "") + module Ullbc = struct open UllbcAst diff --git a/charon-ml/src/generated/Generated_OfPostcard.ml b/charon-ml/src/generated/Generated_OfPostcard.ml index 2fe43a1d5..45a7b5836 100644 --- a/charon-ml/src/generated/Generated_OfPostcard.ml +++ b/charon-ml/src/generated/Generated_OfPostcard.ml @@ -1030,7 +1030,8 @@ and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : match __tag with | 0 -> let* x_0 = operand_of_postcard ctx st in - Ok (Use x_0) + let* x_1 = with_retag_of_postcard ctx st in + Ok (Use (x_0, x_1)) | 1 -> let* place = place_of_postcard ctx st in let* kind = borrow_kind_of_postcard ctx st in @@ -1389,6 +1390,15 @@ and variant_id_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : (variant_id, string) result = combine_error_msgs st __FUNCTION__ (VariantId.id_of_postcard ctx st) +and with_retag_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : + (with_retag, string) result = + combine_error_msgs st __FUNCTION__ + (let* __tag = int_of_postcard ctx st in + match __tag with + | 0 -> Ok NoRetag + | 1 -> Ok YesRetag + | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag)) + module Ullbc = struct open UllbcAst diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 69e88fce3..6f8c4f453 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -252,7 +252,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.208" +version = "0.1.209" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 83a69a5cc..3416ea7c9 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -25,7 +25,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] } [package] name = "charon" -version = "0.1.208" +version = "0.1.209" authors.workspace = true edition.workspace = true license.workspace = true diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index d36890fbe..cf9b1450d 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -671,6 +671,15 @@ pub struct ConstantExpr { pub ty: Ty, } +/// Used for [`Rvalue::Use`] to indicate whether the operand should be retagged (this is used +/// for Rust's aliasing model). +#[derive(Debug, Hash, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Retag"))] +pub enum WithRetag { + No, + Yes, +} + /// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC). /// We can also factor out the unops, binops with the function calls. /// TODO: move the aggregate kind to operands @@ -690,7 +699,7 @@ pub struct ConstantExpr { )] pub enum Rvalue { /// Lifts an operand as an rvalue. - Use(Operand), + Use(Operand, #[drive(skip)] WithRetag), /// Takes a reference to the given place. /// The `Operand` refers to the init value of the metadata, it is `()` if no metadata #[cfg_attr(feature = "charon_on_charon", charon::rename("RvRef"))] diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 138805aae..c2e6290e1 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -170,7 +170,7 @@ impl<'tcx> ItemTransCtx<'tcx, '_> { let ret = bb.new_var(None, c.ty.clone()); bb.push_statement(StatementKind::Assign( ret, - Rvalue::Use(Operand::Const(Box::new(c))), + Rvalue::Use(Operand::Const(Box::new(c)), WithRetag::No), )); Ok(Body::Unstructured(bb.build())) } else { @@ -917,12 +917,18 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { tgt_ty: &Ty, ) -> Result { match rvalue { - mir::Rvalue::Use(operand, _) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)), + mir::Rvalue::Use(operand, retag) => { + let retag = match retag { + mir::WithRetag::Yes => WithRetag::Yes, + mir::WithRetag::No => WithRetag::No, + }; + Ok(Rvalue::Use(self.translate_operand(span, operand)?, retag)) + } mir::Rvalue::CopyForDeref(place) => { // According to the documentation, it seems to be an optimisation // for drop elaboration. We treat it as a regular copy. let place = self.translate_place(span, place)?; - Ok(Rvalue::Use(Operand::Copy(place))) + Ok(Rvalue::Use(Operand::Copy(place), WithRetag::No)) } mir::Rvalue::Repeat(operand, cnst) => { let c = self.translate_ty_constant_expr(span, cnst)?; @@ -1037,9 +1043,12 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { mir::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap), mir::UnOp::PtrMetadata => match operand { Operand::Copy(p) | Operand::Move(p) => { - return Ok(Rvalue::Use(Operand::Copy( - p.project(ProjectionElem::PtrMetadata, tgt_ty.clone()), - ))); + return Ok(Rvalue::Use( + Operand::Copy( + p.project(ProjectionElem::PtrMetadata, tgt_ty.clone()), + ), + WithRetag::No, + )); } Operand::Const(_) => { panic!("unexpected metadata operand") diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index f4a2e6e89..2081ec474 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -375,7 +375,7 @@ impl<'tcx> ItemTransCtx<'tcx, '_> { span, StatementKind::Assign( locals.place_for_var(local_id), - Rvalue::Use(Operand::Move(nth_field)), + Rvalue::Use(Operand::Move(nth_field), WithRetag::No), ), ) }); diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index cace84bd5..bd5f6a219 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -951,10 +951,13 @@ impl<'tcx> ItemTransCtx<'tcx, '_> { // ``` let mut mk_cast = |(method_name, method_ty, method_shim): (String, Ty, FnPtr)| { let method_local = builder.new_var(Some(method_name.clone()), method_ty.clone()); - let shim = Rvalue::Use(Operand::Const(Box::new(ConstantExpr { - kind: ConstantExprKind::FnDef(method_shim.clone()), - ty: method_ty.clone(), - }))); + let shim = Rvalue::Use( + Operand::Const(Box::new(ConstantExpr { + kind: ConstantExprKind::FnDef(method_shim.clone()), + ty: method_ty.clone(), + })), + WithRetag::No, + ); let cast_local = builder.new_var( Some("erased_".to_string() + method_name.as_str()), ty.clone(), diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 9191b4c39..d73f655d0 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1573,7 +1573,7 @@ impl_display_via_ctx!(Rvalue); impl FmtWithCtx for Rvalue { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Rvalue::Use(x) => write!(f, "{}", x.with_ctx(ctx)), + Rvalue::Use(x, _) => write!(f, "{}", x.with_ctx(ctx)), Rvalue::Ref { place, kind: borrow_kind, diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index d072bfa77..e0b36673f 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -224,7 +224,7 @@ pub trait BodyTransformCtx: Sized { /// Assign an rvalue to a place, unless the rvalue is a move in which case we just use the /// moved place. fn rval_to_place(&mut self, rvalue: Rvalue, ty: Ty) -> Place { - if let Rvalue::Use(Operand::Move(place)) = rvalue { + if let Rvalue::Use(Operand::Move(place), WithRetag::No) = rvalue { place } else { let var = self.fresh_var(None, ty); diff --git a/charon/src/transform/resugar/reconstruct_fallible_operations.rs b/charon/src/transform/resugar/reconstruct_fallible_operations.rs index 60854cdb1..8f9fbd4b1 100644 --- a/charon/src/transform/resugar/reconstruct_fallible_operations.rs +++ b/charon/src/transform/resugar/reconstruct_fallible_operations.rs @@ -160,7 +160,7 @@ fn remove_dynamic_checks( // assert(move b == true) [ Statement { - kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))), + kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op), _)), .. }, Statement { @@ -209,7 +209,7 @@ fn remove_dynamic_checks( .. }, Statement { - kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))), + kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op), _)), .. }, Statement { diff --git a/charon/src/transform/resugar/reconstruct_vec_boxes.rs b/charon/src/transform/resugar/reconstruct_vec_boxes.rs index 463adac64..585b7e747 100644 --- a/charon/src/transform/resugar/reconstruct_vec_boxes.rs +++ b/charon/src/transform/resugar/reconstruct_vec_boxes.rs @@ -177,7 +177,7 @@ fn find_next_move_of( let block = &body.body[cursor.block]; while cursor.statement < block.statements.len() { let st = &body[cursor]; - if let Some((dst_place, Rvalue::Use(Operand::Move(src_place)))) = st.kind.as_assign() + if let Some((dst_place, Rvalue::Use(Operand::Move(src_place), _))) = st.kind.as_assign() && src_place == src { return Some((cursor, dst_place.clone())); @@ -220,7 +220,7 @@ fn find_move_in_block( ) -> Option { let mut out = None; for (statement, st) in body.body[block].statements.iter().enumerate() { - if let Some((dst_place, Rvalue::Use(Operand::Move(src_place)))) = st.kind.as_assign() + if let Some((dst_place, Rvalue::Use(Operand::Move(src_place), _))) = st.kind.as_assign() && dst_place == dst && src_place == src { @@ -437,7 +437,10 @@ impl UllbcPass for Transform { )); target_block.statements.push(Statement::new( rw.span, - StatementKind::Assign(rw.box_array, Rvalue::Use(Operand::Move(box_array_local))), + StatementKind::Assign( + rw.box_array, + Rvalue::Use(Operand::Move(box_array_local), WithRetag::No), + ), )); target_block.statements.push(Statement::new( rw.span, diff --git a/charon/src/transform/simplify_output/index_intermediate_assigns.rs b/charon/src/transform/simplify_output/index_intermediate_assigns.rs index 96ee84bf4..860716932 100644 --- a/charon/src/transform/simplify_output/index_intermediate_assigns.rs +++ b/charon/src/transform/simplify_output/index_intermediate_assigns.rs @@ -74,7 +74,10 @@ impl UllbcPass for Transform { { // Fresh local variable for the temporary assignment let tmp_var = ctx.fresh_var(None, lhs.ty().clone()); - let tmp_rhs = std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone()))); + let tmp_rhs = std::mem::replace( + rhs, + Rvalue::Use(Operand::Move(tmp_var.clone()), WithRetag::No), + ); // Introduce the intermediate let-binding ctx.insert_assn_stmt(tmp_var, tmp_rhs) } diff --git a/charon/src/transform/simplify_output/index_to_function_calls.rs b/charon/src/transform/simplify_output/index_to_function_calls.rs index 7c6d1afec..c607033ba 100644 --- a/charon/src/transform/simplify_output/index_to_function_calls.rs +++ b/charon/src/transform/simplify_output/index_to_function_calls.rs @@ -186,7 +186,7 @@ impl VisitBodyMut for IndexVisitor<'_, '_> { | Discriminant(..) | Len(..) => self.visit_inner_with_mutability(x, false), - Use(_) | NullaryOp(..) | UnaryOp(..) | BinaryOp(..) | Aggregate(..) | Repeat(..) => { + Use(..) | NullaryOp(..) | UnaryOp(..) | BinaryOp(..) | Aggregate(..) | Repeat(..) => { self.visit_inner(x) } } diff --git a/charon/src/transform/simplify_output/inline_selected_functions.rs b/charon/src/transform/simplify_output/inline_selected_functions.rs index 772f7ee9b..3b219ae29 100644 --- a/charon/src/transform/simplify_output/inline_selected_functions.rs +++ b/charon/src/transform/simplify_output/inline_selected_functions.rs @@ -127,7 +127,7 @@ impl UllbcPass for Transform { let arg_place = outer_body.locals.place_for_var(arg_local); [ StatementKind::StorageLive(arg_local), - StatementKind::Assign(arg_place, Rvalue::Use(arg)), + StatementKind::Assign(arg_place, Rvalue::Use(arg, WithRetag::Yes)), ] })) .map(|kind| Statement::new(span, kind)), @@ -140,7 +140,10 @@ impl UllbcPass for Transform { let return_place = outer_body.locals.place_for_var(return_local); final_block.statements.push(Statement::new( span, - StatementKind::Assign(dest_place, Rvalue::Use(Operand::Move(return_place))), + StatementKind::Assign( + dest_place, + Rvalue::Use(Operand::Move(return_place), WithRetag::Yes), + ), )); let final_block = outer_body.body.push(final_block); diff --git a/charon/src/transform/simplify_output/remove_unit_locals.rs b/charon/src/transform/simplify_output/remove_unit_locals.rs index c1a57495b..c025484d8 100644 --- a/charon/src/transform/simplify_output/remove_unit_locals.rs +++ b/charon/src/transform/simplify_output/remove_unit_locals.rs @@ -13,7 +13,7 @@ impl UllbcPass for Transform { // other `Rvalue`s as they might have side-effects (e.g. reading through a pointer). body.visit_statements(|st| { if let StatementKind::Assign(_, rvalue) = &mut st.kind - && let Rvalue::Use(Operand::Move(from) | Operand::Copy(from)) = rvalue + && let Rvalue::Use(Operand::Move(from) | Operand::Copy(from), _) = rvalue && from.is_local() && from.ty().is_unit() { diff --git a/charon/src/transform/simplify_output/simplify_constants.rs b/charon/src/transform/simplify_output/simplify_constants.rs index 4d8e83d55..bceb3adb0 100644 --- a/charon/src/transform/simplify_output/simplify_constants.rs +++ b/charon/src/transform/simplify_output/simplify_constants.rs @@ -62,7 +62,7 @@ fn transform_constant_expr( // Evaluate the referenced value let bval_ty = bval.ty().clone(); - ctx.rval_to_place(Rvalue::Use(bval), bval_ty) + ctx.rval_to_place(Rvalue::Use(bval, WithRetag::No), bval_ty) } }; match (rk, metadata) { @@ -180,7 +180,7 @@ impl UllbcPass for Transform { { Rvalue::Repeat(op.clone(), ty.clone(), len) } - Rvalue::Use(Operand::Const(e)) if e.kind.is_adt() && e.ty.is_unit() => { + Rvalue::Use(Operand::Const(e), _) if e.kind.is_adt() && e.ty.is_unit() => { Rvalue::unit_value() } _ => rvalue,