diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index b5f8e3708..2f346fa35 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.197" +let supported_charon_version = "0.1.198" diff --git a/charon-ml/src/Print.ml b/charon-ml/src/Print.ml index e50df6b17..b0761eb2a 100644 --- a/charon-ml/src/Print.ml +++ b/charon-ml/src/Print.ml @@ -936,8 +936,6 @@ and rvalue_to_string (env : fmt_env) (rv : rvalue) : string = "[" ^ operand_to_string env v ^ ";" ^ constant_expr_to_string env len ^ "]" - | ShallowInitBox (op, _) -> - "shallow-init-box(" ^ operand_to_string env op ^ ")" | Aggregate (akind, ops) -> aggregate_to_string env akind ops let item_id_to_string (id : item_id) : string = diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index f5e39ff78..3a57ef9f7 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/charon-ml/src/generated/Generated_Expressions.ml @@ -310,11 +310,6 @@ and rvalue = (** [Repeat(x, n)] creates an array where [x] is copied [n] times. We translate this to a function call for LLBC. *) - | ShallowInitBox of operand * ty - (** Transmutes a [*mut u8] (obtained from [malloc]) into - shallow-initialized [Box]. This only appears as part of lowering - [Box::new()] in some cases. We reconstruct the original [Box::new()] - call, but sometimes may fail to do so, leaking the expression. *) (** Unary operation *) and unop = diff --git a/charon-ml/src/generated/Generated_OfJson.ml b/charon-ml/src/generated/Generated_OfJson.ml index 2b6b74ab2..a265d1347 100644 --- a/charon-ml/src/generated/Generated_OfJson.ml +++ b/charon-ml/src/generated/Generated_OfJson.ml @@ -1137,10 +1137,6 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result = let* x_1 = ty_of_json ctx x_1 in let* x_2 = box_of_json constant_expr_of_json ctx x_2 in Ok (Repeat (x_0, x_1, x_2)) - | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] -> - let* x_0 = operand_of_json ctx x_0 in - let* x_1 = ty_of_json ctx x_1 in - Ok (ShallowInitBox (x_0, x_1)) | _ -> Error "") and scalar_value_of_json (ctx : of_json_ctx) (js : json) : diff --git a/charon-ml/src/generated/Generated_OfPostcard.ml b/charon-ml/src/generated/Generated_OfPostcard.ml index a31da29b8..28af2042e 100644 --- a/charon-ml/src/generated/Generated_OfPostcard.ml +++ b/charon-ml/src/generated/Generated_OfPostcard.ml @@ -1048,10 +1048,6 @@ and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : let* x_1 = ty_of_postcard ctx st in let* x_2 = box_of_postcard constant_expr_of_postcard ctx st in Ok (Repeat (x_0, x_1, x_2)) - | 10 -> - let* x_0 = operand_of_postcard ctx st in - let* x_1 = ty_of_postcard ctx st in - Ok (ShallowInitBox (x_0, x_1)) | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag)) and scalar_value_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : diff --git a/charon/AGENTS.md b/charon/AGENTS.md new file mode 100644 index 000000000..64106bc6f --- /dev/null +++ b/charon/AGENTS.md @@ -0,0 +1,62 @@ +# AGENTS.md + +Guidance for AI agents working on Charon. + +## Working Style + +- Charon is written with the following values in mind: correctness, robustness, maintainability, and + solving people's problems (also, finding joy in clean code and abstractions). +- The codebase is built around carefully-crafted invariants, e.g. how we go from rustc to hax to + charon for `GenericArgs`, or how mono mode is transparent most of the time. +- Read the surrounding code before editing. Most problems in this repository already have a nearby + pattern in another translation pass, AST utility, or normalization pass. +- We are the owners of this codebase, we can make deep changes if that's the best way to solve + a problem. +- Exercise judgment: sometimes the right fix is downstream (e.g. in aeneas) or upstream (e.g. in + rustc itself); I don't shy from fixing the bugs where they should be fixed (though well-placed + workarounds are often fine). +- Correctness comes first. We should be very careful when modifying what we got from rustc. Even + tricky cases should be handled correctly; if in doubt, double-check and add tests. +- Robustness comes second. Charon should be able to emit an llbc file even in the face of many + errors. Use panics appropriately, when they indicate a broken invariant within Charon. Use errors + when the invariant is less clear and/or there's high risk of it being broken in practice. +- Maintainability comes third. Prefer small, principled changes over local cleverness. A change that + introduces a ton of code at once is suspicious; there's often a cleaner way. I'm the sole + maintainer so any unneeded complexity is a cost I'll have to bear in the future. +- If in doubt, ask, and exercise judgment as a good OSS maintainer would. + +## Implementing Translation and Transformations + +- Avoid constructing generic arguments manually to avoid getting trait references wrong. Prefer + obtaining generics from an existing call, type, translated item, or Hax/rustc API. +- Be careful about monomorphized mode: it can break some assumptions such as the fact that a given + item exists only once. If an approach relies on polymorphic item paths, function names, or + non-monomorphized generic structure, either make it work in mono deliberately or gate the pass off + in mono mode. +- Prefer rustc and Hax APIs for item discovery and method resolution. Use `def_path_def_ids`/path + resolution for named standard items, and Hax `ItemRef`s when the result should flow through normal + Charon translation. +- Be careful with `ctx.translated`: some bodies stored there may not have gone through later body + cleanup passes yet. If a pass reads from translated bodies while transformations are fused, + consider whether it is seeing pre-pass or post-pass state. +- If a pass needs a declaration id, prefer an initializer (`Transform::new(ctx)`) that discovers it + once and stores it in the transform. Put prerequisites in `should_run`, including option gates and + whether required declarations were found. +- Keep algorithmic complexity under control: generally avoid iterating over the whole crate or + a whole body too many times. + +## Testing + +- Every fix should ideally have a reproducer. The test suite is quite flexible, use it. +- Changes to the generated output are to be double-checked: they can often indicate a bug. + Well-motivated changes are however totally fine. + +## OCaml vs Rust + +Charon is a hybrid codebase. A typical feature is mostly on the Rust side. However when the AST +changes, this must be propagated. Use `make generate-ml` to regenerate the generated OCaml files. + +## Versioning + +Any change to the AST must come with a version bump to make the deserializers emit nice errors. Just +bump the patch version in `Cargo.toml` then run `make test` at the root to propagate the changes. diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 6c6bd0976..6d2b36ccd 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -252,7 +252,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.197" +version = "0.1.198" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index ed03aa36b..5097e7a56 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -24,7 +24,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] } [package] name = "charon" -version = "0.1.197" +version = "0.1.198" authors.workspace = true edition.workspace = true license.workspace = true diff --git a/charon/rust-toolchain b/charon/rust-toolchain index 765fea85b..6b2c73aa1 100644 --- a/charon/rust-toolchain +++ b/charon/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2026-02-07" +channel = "nightly-2026-02-22" 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/src/ast/builtins.rs b/charon/src/ast/builtins.rs index eb46ad235..125d819ae 100644 --- a/charon/src/ast/builtins.rs +++ b/charon/src/ast/builtins.rs @@ -12,6 +12,15 @@ use crate::types::*; // We treat this one specially in the `inline_local_panic_functions` pass. See there for details. pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"]; +pub static BOX_ASSUME_INIT_INTO_VEC_UNSAFE: &str = "box_assume_init_into_vec_unsafe"; + +pub static BOX_WRITE: &str = "alloc::boxed::Box::write"; + +// The translated Charon name contains an inherent impl path element where the Rust path contains +// `Box`. `NamePattern` does not yet inspect inherent impl receiver types, so passes that match the +// translated name need this wildcarded pattern. +pub static BOX_WRITE_PATTERN: &str = "alloc::boxed::_::write"; + impl BuiltinTy { pub fn get_name(self) -> Name { let name: &[_] = match self { diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index fd2d3f2fd..d36890fbe 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -753,10 +753,6 @@ pub enum Rvalue { /// /// We translate this to a function call for LLBC. Repeat(Operand, Ty, Box), - /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box`. This - /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original - /// `Box::new()` call, but sometimes may fail to do so, leaking the expression. - ShallowInitBox(Operand, Ty), } /// An aggregated ADT. diff --git a/charon/src/ast/hash_cons.rs b/charon/src/ast/hash_cons.rs index d2fb403db..8f44f32c1 100644 --- a/charon/src/ast/hash_cons.rs +++ b/charon/src/ast/hash_cons.rs @@ -77,7 +77,6 @@ mod intern_table { U: indexmap::Equivalent>, { // Fast read-only check. - #[expect(irrefutable_let_patterns)] // https://github.com/rust-lang/rust/issues/139369 let arc = if let read_guard = INTERNED.read().unwrap() && let Some(map) = read_guard.get::() && let Some((arc, _id)) = map.get_key_value(&inner) diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index be6f41af3..e4b28f7a0 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -758,6 +758,10 @@ impl Ty { } } + pub fn as_adt_id(&self) -> Option { + self.kind().as_adt().and_then(|a| a.id.as_adt().cloned()) + } + pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata { let ty_decls = &translated.type_decls; match self.kind() { diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs index 2ed0e335a..180b358dc 100644 --- a/charon/src/ast/ullbc_ast_utils.rs +++ b/charon/src/ast/ullbc_ast_utils.rs @@ -6,6 +6,33 @@ use crate::meta::Span; use crate::ullbc_ast::*; use std::collections::HashMap; use std::mem; +use std::ops::{Index, IndexMut}; + +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct StmtLoc { + pub block: BlockId, + pub statement: usize, +} + +impl StmtLoc { + pub fn new(block: BlockId, statement: usize) -> Self { + StmtLoc { block, statement } + } + + pub fn block_start(block: BlockId) -> Self { + StmtLoc { + block, + statement: 0, + } + } + + pub fn after(self) -> Self { + StmtLoc { + block: self.block, + statement: self.statement + 1, + } + } +} impl SwitchTargets { pub fn targets(&self) -> SmallVec<[BlockId; 2]> { @@ -118,6 +145,23 @@ impl Terminator { } } } + + pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> { + match &self.kind { + TerminatorKind::Goto { target } => { + smallvec![*target] + } + TerminatorKind::Switch { targets, .. } => targets.targets(), + TerminatorKind::Call { target, .. } + | TerminatorKind::Drop { target, .. } + | TerminatorKind::Assert { target, .. } => { + smallvec![*target] + } + TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => { + smallvec![] + } + } + } } impl BlockData { @@ -165,22 +209,8 @@ impl BlockData { pub fn targets(&self) -> SmallVec<[BlockId; 2]> { self.terminator.targets() } - pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> { - match &self.terminator.kind { - TerminatorKind::Goto { target } => { - smallvec![*target] - } - TerminatorKind::Switch { targets, .. } => targets.targets(), - TerminatorKind::Call { target, .. } - | TerminatorKind::Drop { target, .. } - | TerminatorKind::Assert { target, .. } => { - smallvec![*target] - } - TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => { - smallvec![] - } - } + self.terminator.targets_ignoring_unwind() } /// Apply a transformer to all the statements. @@ -304,6 +334,19 @@ impl ExprBody { } } +impl Index for ExprBody { + type Output = Statement; + fn index(&self, loc: StmtLoc) -> &Self::Output { + &self.body[loc.block].statements[loc.statement] + } +} + +impl IndexMut for ExprBody { + fn index_mut(&mut self, loc: StmtLoc) -> &mut Self::Output { + &mut self.body[loc.block].statements[loc.statement] + } +} + /// Helper to construct a small ullbc body. pub struct BodyBuilder { /// The span to use for everything. diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index d225e4b10..0075e8242 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -11,7 +11,6 @@ #![expect(incomplete_features)] #![feature(box_patterns)] #![feature(deref_patterns)] -#![feature(if_let_guard)] #![feature(iter_array_chunks)] #![feature(iterator_try_collect)] #![feature(macro_metavar_expr)] diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 466510413..cbc1e1a9b 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -23,6 +23,7 @@ use charon_lib::ast::*; use charon_lib::formatter::FmtCtx; use charon_lib::formatter::IntoFormatter; use charon_lib::ids::IndexMap; +use charon_lib::name_matcher::NamePattern; use charon_lib::pretty::FmtWithCtx; use charon_lib::ullbc_ast::*; @@ -208,6 +209,258 @@ impl<'tcx> ItemTransCtx<'tcx, '_> { } } } + + fn translate_unsizing_metadata( + &mut self, + span: Span, + meta: hax::UnsizingMetadata, + ) -> Result { + Ok(match &meta { + hax::UnsizingMetadata::Length(len) => { + let len = self.translate_constant_expr(span, len)?; + UnsizingMetadata::Length(Box::new(len)) + } + hax::UnsizingMetadata::DirectVTable(impl_expr) => { + let tref = self.translate_trait_impl_expr(span, impl_expr)?; + let vtable = self.translate_vtable_instance_const(span, impl_expr)?; + UnsizingMetadata::VTable(tref, vtable) + } + hax::UnsizingMetadata::NestedVTable(dyn_impl_expr) => { + // This binds a fake `T: SrcTrait` variable. + let binder = + self.translate_dyn_binder(span, dyn_impl_expr, |ctx, _, impl_expr| { + ctx.translate_trait_impl_expr(span, impl_expr) + })?; + + // Compute the supertrait path from the source tref to the target + // tref. + let mut target_tref = &binder.skip_binder; + let mut clause_path: Vec<(TraitDeclId, TraitClauseId)> = vec![]; + while let TraitRefKind::ParentClause(tref, id) = &target_tref.kind { + clause_path.push((tref.trait_decl_ref.skip_binder.id, *id)); + target_tref = tref; + } + + let mut field_path = vec![]; + for &(trait_id, clause_id) in &clause_path { + if let Ok(ItemRef::TraitDecl(tdecl)) = self.get_or_translate(trait_id.into()) + && let &vtable_decl_id = tdecl.vtable.as_ref().unwrap().id.as_adt().unwrap() + && let Ok(ItemRef::Type(vtable_decl)) = + self.get_or_translate(vtable_decl_id.into()) + { + let ItemSource::VTableTy { supertrait_map, .. } = &vtable_decl.src else { + unreachable!() + }; + field_path.push(supertrait_map[clause_id].unwrap()); + } else { + break; + } + } + + if field_path.len() == clause_path.len() { + UnsizingMetadata::VTableUpcast(field_path) + } else { + UnsizingMetadata::Unknown + } + } + hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown, + }) + } + + /// Generate a fake function body for ADT constructors. + pub(crate) fn build_ctor_body( + &mut self, + span: Span, + def: &hax::FullDef<'tcx>, + ) -> Result { + let hax::FullDefKind::Ctor { + adt_def_id, + ctor_of, + variant_id, + fields, + output_ty, + } = def.kind() + else { + unreachable!() + }; + let tref = self + .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?; + let output_ty = self.translate_ty(span, output_ty)?; + + let mut builder = BodyBuilder::new(span, fields.len()); + let return_place = builder.new_var(None, output_ty); + let args: Vec<_> = fields + .iter() + .map(|field| -> Result { + let ty = self.translate_ty(span, &field.ty)?; + let place = builder.new_var(None, ty); + Ok(Operand::Move(place)) + }) + .try_collect()?; + let variant = match ctor_of { + hax::CtorOf::Struct => None, + hax::CtorOf::Variant => Some(self.translate_variant_id(*variant_id)), + }; + builder.push_statement(StatementKind::Assign( + return_place, + Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args), + )); + Ok(Body::Unstructured(builder.build())) + } + + /// FIXME(#865): Generate a function body for the `box_assume_init_into_vec_unsafe` function, + /// because the MIR we get for it is too optimized to be usable. + pub(crate) fn build_box_assume_init_into_vec_unsafe( + &mut self, + span: Span, + def: &hax::FullDef<'tcx>, + ) -> Result { + // pub fn box_assume_init_into_vec_unsafe( + // b: Box>, + // ) -> Vec { + // let x: Box<[T; N]> = unsafe { Box::assume_init(b) }; + // let y = x as Box<[T]>; + // core::slice::into_vec(y) + // } + let tcx = self.tcx; + let hax::FullDefKind::Fn { sig: hax_sig, .. } = def.kind() else { + unreachable!() + }; + let hax_sig = hax_sig.hax_skip_binder_ref(); + let sig = self.translate_fun_sig(span, hax_sig)?; + + // Get the `[T; N]` and `A` parameters. + let (array_rust_ty, alloc_rust_ty) = { + let input_box_rust_args = { + let hax::TyKind::Adt(input_box_item) = hax_sig.inputs[0].kind() else { + raise_error!(self, span, "expected a boxed input in the hax signature"); + }; + input_box_item.rustc_args(self.hax_state_with_id()) + }; + let maybe_uninit_array_rust_ty = input_box_rust_args[0].as_type().unwrap(); + let alloc_rust_ty = input_box_rust_args[1].as_type().unwrap(); + let ty::Adt(_, maybe_uninit_rust_args) = maybe_uninit_array_rust_ty.kind() else { + raise_error!( + self, + span, + "expected `MaybeUninit<[T; N]>` in the hax signature" + ); + }; + let Some(array_rust_ty) = maybe_uninit_rust_args[0].as_type() else { + raise_error!( + self, + span, + "expected the first `MaybeUninit` parameter to be a type" + ); + }; + (array_rust_ty, alloc_rust_ty) + }; + // `T` + let elem_rust_ty = array_rust_ty.builtin_index().unwrap(); + // `[T]` + let slice_rust_ty = ty::Ty::new_slice(tcx, elem_rust_ty); + // `Box<[T; N]>` + let box_array_rust_ty = ty::Ty::new_box(tcx, array_rust_ty); + let box_array_ty = self.translate_rustc_ty(span, &box_array_rust_ty)?; + // `Box<[T]>` + let box_slice_rust_ty = ty::Ty::new_box(tcx, slice_rust_ty); + let box_slice_ty = self.translate_rustc_ty(span, &box_slice_rust_ty)?; + + if !self.monomorphize() { + // Make `Box::write` available to a later construction pass. + let path = NamePattern::parse(builtins::BOX_WRITE).unwrap(); + let box_write_def_id = self + .resolve_path(span, &path, true)? + .into_iter() + .exactly_one() + .unwrap(); + let box_write_args = tcx.mk_args(&[array_rust_ty.into(), alloc_rust_ty.into()]); + let box_write_item = + hax::ItemRef::translate(self.hax_state_with_id(), box_write_def_id, box_write_args); + let _ = self.translate_fn_ptr(span, &box_write_item, TransItemSourceKind::Fun)?; + } + + let body = { + let mut builder = BodyBuilder::new(span, sig.inputs.len()); + let return_place = builder.new_var(Some("ret".to_string()), sig.output.clone()); + let input = builder.new_var(Some("b".to_string()), sig.inputs[0].clone()); + let initialized_box = builder.new_var(Some("x".to_string()), box_array_ty.clone()); + let box_slice = builder.new_var(Some("y".to_string()), box_slice_ty.clone()); + + builder.call({ + let assume_init_fn = { + let path = NamePattern::parse("alloc::boxed::Box::assume_init").unwrap(); + let assume_init_def_id = self + .resolve_path(span, &path, true)? + .into_iter() + // There's `assume_init` on `Box>` and `Box<[MU]>`, we want the former. + .filter(|&def_id| { + let sig = self.tcx.fn_sig(def_id); + !sig.skip_binder().inputs().skip_binder()[0] + .expect_boxed_ty() + .is_slice() + }) + .exactly_one() + .unwrap(); + let assume_init_args = + tcx.mk_args(&[array_rust_ty.into(), alloc_rust_ty.into()]); + let assume_init_item = hax::ItemRef::translate( + self.hax_state_with_id(), + assume_init_def_id, + assume_init_args, + ); + self.translate_fn_ptr(span, &assume_init_item, TransItemSourceKind::Fun)? + }; + Call { + func: FnOperand::Regular(assume_init_fn), + args: vec![Operand::Move(input)], + dest: initialized_box.clone(), + } + }); + + builder.push_statement({ + let meta = hax::compute_unsizing_metadata( + &self.hax_state, + box_array_rust_ty, + box_slice_rust_ty, + ); + let meta = self.translate_unsizing_metadata(span, meta)?; + StatementKind::Assign( + box_slice.clone(), + Rvalue::UnaryOp( + UnOp::Cast(CastKind::Unsize(box_array_ty, box_slice_ty, meta)), + Operand::Move(initialized_box), + ), + ) + }); + + builder.call({ + let into_vec_fn = { + let path = NamePattern::parse("slice::into_vec").unwrap(); + let into_vec_def_id = self + .resolve_path(span, &path, true)? + .into_iter() + .exactly_one() + .unwrap(); + let into_vec_args = tcx.mk_args(&[elem_rust_ty.into(), alloc_rust_ty.into()]); + let into_vec_item = hax::ItemRef::translate( + self.hax_state_with_id(), + into_vec_def_id, + into_vec_args, + ); + self.translate_fn_ptr(span, &into_vec_item, TransItemSourceKind::Fun)? + }; + Call { + func: FnOperand::Regular(into_vec_fn), + args: vec![Operand::Move(box_slice)], + dest: return_place, + } + }); + builder.build() + }; + + Ok(Body::Unstructured(body)) + } } impl<'tcx> BodyTransCtx<'tcx, '_, '_> { @@ -707,64 +960,7 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize, ..) => { let meta = hax::compute_unsizing_metadata(&self.hax_state, op_ty, *rust_tgt_ty); - let meta = match &meta { - hax::UnsizingMetadata::Length(len) => { - let len = self.translate_constant_expr(span, len)?; - UnsizingMetadata::Length(Box::new(len)) - } - hax::UnsizingMetadata::DirectVTable(impl_expr) => { - let tref = self.translate_trait_impl_expr(span, impl_expr)?; - let vtable = - self.translate_vtable_instance_const(span, impl_expr)?; - UnsizingMetadata::VTable(tref, vtable) - } - hax::UnsizingMetadata::NestedVTable(dyn_impl_expr) => { - // This binds a fake `T: SrcTrait` variable. - let binder = self.translate_dyn_binder( - span, - dyn_impl_expr, - |ctx, _, impl_expr| { - ctx.translate_trait_impl_expr(span, impl_expr) - }, - )?; - - // Compute the supertrait path from the source tref to the target - // tref. - let mut target_tref = &binder.skip_binder; - let mut clause_path: Vec<(TraitDeclId, TraitClauseId)> = vec![]; - while let TraitRefKind::ParentClause(tref, id) = &target_tref.kind { - clause_path.push((tref.trait_decl_ref.skip_binder.id, *id)); - target_tref = tref; - } - - let mut field_path = vec![]; - for &(trait_id, clause_id) in &clause_path { - if let Ok(ItemRef::TraitDecl(tdecl)) = - self.get_or_translate(trait_id.into()) - && let &vtable_decl_id = - tdecl.vtable.as_ref().unwrap().id.as_adt().unwrap() - && let Ok(ItemRef::Type(vtable_decl)) = - self.get_or_translate(vtable_decl_id.into()) - { - let ItemSource::VTableTy { supertrait_map, .. } = - &vtable_decl.src - else { - unreachable!() - }; - field_path.push(supertrait_map[clause_id].unwrap()); - } else { - break; - } - } - - if field_path.len() == clause_path.len() { - UnsizingMetadata::VTableUpcast(field_path) - } else { - UnsizingMetadata::Unknown - } - } - hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown, - }; + let meta = self.translate_unsizing_metadata(span, meta)?; CastKind::Unsize(src_ty, tgt_ty.clone(), meta) } }; @@ -900,11 +1096,6 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> { } } } - mir::Rvalue::ShallowInitBox(op, ty) => { - let op = self.translate_operand(span, op)?; - let ty = self.translate_rustc_ty(span, ty)?; - Ok(Rvalue::ShallowInitBox(op, ty)) - } mir::Rvalue::ThreadLocalRef(_) => { raise_error!( self, diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 5c4416ac7..6158f8f30 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -25,6 +25,7 @@ use super::translate_ctx::*; use crate::hax; use crate::hax::SInto; use charon_lib::ast::*; +use charon_lib::name_matcher::NamePattern; use charon_lib::options::{CliOpts, StartFrom, TranslateOptions}; use charon_lib::transform::TransformCtx; use macros::VariantIndexArity; @@ -206,6 +207,18 @@ impl RustcItem { } impl<'tcx> TranslateCtx<'tcx> { + /// Resolve a path to a list of matching `DefId`s. + pub fn resolve_path( + &self, + span: Span, + pat: &NamePattern, + strict: bool, + ) -> Result, Error> { + super::resolve_path::def_path_def_ids(&self.hax_state, pat, strict).map_err(|err| { + register_error!(self, span, "failed to resolve item path `{pat}`: {err}") + }) + } + /// Returns the default translation kind for the given `DefId`. Returns `None` for items that /// we don't translate. Errors on unexpected items. pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option { @@ -868,19 +881,10 @@ pub fn translate<'tcx>( for start_from in ctx.options.start_from.clone() { match start_from { StartFrom::Pattern { pattern, strict } => { - match super::resolve_path::def_path_def_ids(&ctx.hax_state, &pattern, strict) { - Ok(resolved) => { - for def_id in resolved { - let def_id: hax::DefId = def_id.sinto(&ctx.hax_state); - ctx.enqueue_module_item(&def_id); - } - } - Err(err) => { - register_error!( - ctx, - Span::dummy(), - "when processing starting pattern `{pattern}`: {err}" - ); + if let Ok(def_ids) = ctx.resolve_path(Span::dummy(), &pattern, strict) { + for def_id in def_ids { + let def_id: hax::DefId = def_id.sinto(&ctx.hax_state); + ctx.enqueue_module_item(&def_id); } } } diff --git a/charon/src/bin/charon-driver/translate/translate_functions.rs b/charon/src/bin/charon-driver/translate/translate_functions.rs index 47dff4c59..73e2379e7 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions.rs @@ -4,56 +4,12 @@ //! independently. use crate::hax; -use itertools::Itertools; use rustc_span::sym; use super::translate_ctx::*; -use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use charon_lib::ast::*; -use charon_lib::ullbc_ast::*; impl<'tcx> ItemTransCtx<'tcx, '_> { - /// Generate a fake function body for ADT constructors. - pub(crate) fn build_ctor_body( - &mut self, - span: Span, - def: &hax::FullDef<'tcx>, - ) -> Result { - let hax::FullDefKind::Ctor { - adt_def_id, - ctor_of, - variant_id, - fields, - output_ty, - } = def.kind() - else { - unreachable!() - }; - let tref = self - .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?; - let output_ty = self.translate_ty(span, output_ty)?; - - let mut builder = BodyBuilder::new(span, fields.len()); - let return_place = builder.new_var(None, output_ty); - let args: Vec<_> = fields - .iter() - .map(|field| -> Result { - let ty = self.translate_ty(span, &field.ty)?; - let place = builder.new_var(None, ty); - Ok(Operand::Move(place)) - }) - .try_collect()?; - let variant = match ctor_of { - hax::CtorOf::Struct => None, - hax::CtorOf::Variant => Some(self.translate_variant_id(*variant_id)), - }; - builder.push_statement(StatementKind::Assign( - return_place, - Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args), - )); - Ok(Body::Unstructured(builder.build())) - } - /// Checks whether the given id corresponds to a built-in type. pub(crate) fn recognize_builtin_fun( &mut self, diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 136cfb510..4c5c19616 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -557,6 +557,12 @@ impl<'tcx> ItemTransCtx<'tcx, '_> { Body::Intrinsic { name, arg_names } } else if let Some(name) = self.t_ctx.extern_item_symbol_name(def) { Body::Extern(name) + } else if item_meta.lang_item.as_deref() == Some(builtins::BOX_ASSUME_INIT_INTO_VEC_UNSAFE) + && self.options.treat_box_as_builtin + { + // FIXME(#865): the MIR we get is unusably optimized. Instead we build our own body + // here. + self.build_box_assume_init_into_vec_unsafe(span, def)? } else if item_meta.opacity.with_private_contents().is_opaque() { Body::Opaque } else if is_trait_method_decl_without_default { diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 97a4cc7fd..9684c62f8 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -6,7 +6,6 @@ //! //! To run it, call `cargo run --bin generate-ml`. It is also run by `make generate-ml` in the //! crate root. Don't forget to format the output code after regenerating. -#![feature(if_let_guard)] use anyhow::{Context, Result, bail}; use assert_cmd::cargo::CommandCargoExt; diff --git a/charon/src/lib.rs b/charon/src/lib.rs index d2089145d..a5530a177 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -24,7 +24,6 @@ clippy::should_implement_trait, clippy::useless_format )] -#![feature(if_let_guard)] // For when we use charon on itself :3 #![cfg_attr(feature = "charon_on_charon", feature(register_tool))] #![cfg_attr(feature = "charon_on_charon", register_tool(charon))] diff --git a/charon/src/options.rs b/charon/src/options.rs index 5bca0aee0..050afa930 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -693,6 +693,14 @@ impl TranslateOptions { opacities.push(("_".to_string(), Foreign)); } + if options.treat_box_as_builtin { + // Include this item's body, we inline it in a pass. + opacities.push(( + "alloc::boxed::box_assume_init_into_vec_unsafe".to_string(), + Transparent, + )); + } + // We always include the items from the crate. opacities.push(("crate".to_owned(), Transparent)); diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 0e2bca1ce..2f3e0b744 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1605,14 +1605,6 @@ impl FmtWithCtx for Rvalue { Rvalue::Repeat(op, _ty, cg) => { write!(f, "[{}; {}]", op.with_ctx(ctx), cg.with_ctx(ctx)) } - Rvalue::ShallowInitBox(op, ty) => { - write!( - f, - "shallow_init_box::<{}>({})", - ty.with_ctx(ctx), - op.with_ctx(ctx) - ) - } } } } diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 32e8a4746..115c1cbac 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -33,10 +33,10 @@ pub mod normalize { pub mod resugar { pub mod move_asserts_to_statements; pub mod reconstruct_asserts; - pub mod reconstruct_boxes; pub mod reconstruct_fallible_operations; pub mod reconstruct_intrinsics; pub mod reconstruct_matches; + pub mod reconstruct_vec_boxes; } /// Passes that make the output simpler/easier to consume. @@ -149,14 +149,14 @@ pub fn run_transformation_passes(options: &CliOpts, ctx: &mut TransformCtx) { // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this, // it must happen before passes that insert statements like [simplify_constants]. CowBox::Borrowed(&resugar::reconstruct_fallible_operations::Transform), + // Reconstruct `vec![x]` lowering to avoid unsafe operations. + // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of + // this, it must happen before passes that insert statements like [simplify_constants]. + // This must also happen after `inline_selected_functions`, and `merge_goto_chains`. + resugar::reconstruct_vec_boxes::Transform::new(ctx), // Recognize calls to the `offset_of` intrinsics and replace them with the // corresponding `NullOp`. CowBox::Borrowed(&resugar::reconstruct_intrinsics::Transform), - // Reconstruct the special `Box::new` operations inserted e.g. in the `vec![]` macro. - // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this, - // it must happen before passes that insert statements like [simplify_constants]. - // **WARNING**: this pass works across calls, hence must happen after `merge_goto_chains`, - CowBox::Borrowed(&resugar::reconstruct_boxes::Transform), // Reconstruct the asserts CowBox::Borrowed(&resugar::reconstruct_asserts::Transform), // Desugar the constants to other values/operands as much as possible. diff --git a/charon/src/transform/resugar/reconstruct_boxes.rs b/charon/src/transform/resugar/reconstruct_boxes.rs deleted file mode 100644 index cbaf6e533..000000000 --- a/charon/src/transform/resugar/reconstruct_boxes.rs +++ /dev/null @@ -1,167 +0,0 @@ -//! # Micro-pass: reconstruct piecewise box allocations using `malloc` and `ShallowInitBox`. - -use crate::register_error; -use crate::transform::TransformCtx; -use crate::ullbc_ast::*; - -use crate::transform::ctx::UllbcPass; - -pub struct Transform; - -/// The special `alloc::boxed::box_new(x)` intrinsic becomes the following: -/// -/// ```text -/// @4 := alloc::alloc::exchange_malloc(const .., const ..) -/// storage_live(@5) -/// @5 := shallow_init_box::(move (@4)) -/// // possibly some intermediate statements -/// *(@5) := x -/// ``` -/// -/// We reconstruct this into a call to `Box::new(x)`. -impl UllbcPass for Transform { - fn should_run(&self, options: &crate::options::TranslateOptions) -> bool { - options.treat_box_as_builtin - } - fn transform_body(&self, ctx: &mut TransformCtx, b: &mut ExprBody) { - // We need to find a block that has exchange_malloc as the terminator: - // ```text - // @4 := alloc::alloc::exchange_malloc(..) - // ``` - // We then check that that the target block starts with: - // ```text - // storage_live(@5) - // @5 := shallow_init_box::(move (@4)) - // ``` - // We then look for the assignment into the box and take a note of its index. - // ```text - // *(@5) := x - // ``` - // Finally, we replace all these assignments with a call to `@5 = Box::new(x)` - // We do so by replacing the terminator (exchange_malloc) with the correct call and adding - // a `StorageLive`. Everything else becomes Nop. - - for candidate_block_idx in b.body.indices() { - let second_block; - let box_place; - let box_generics; - let value_to_write; - let old_assign_idx; - let assign_span; - let unwind_target; - - if let Some(candidate_block) = b.body.get(candidate_block_idx) - // If the terminator is a call - && let TerminatorKind::Call { - target: target_block_idx, - call: - Call { - args: malloc_args, - func: _, // TODO: once we have a system to recognize intrinsics, check the call is to exchange_malloc. - dest: malloc_dest, - }, - on_unwind, - } = &candidate_block.terminator.kind - // The call has two const arguments - && let [Operand::Const(..), Operand::Const(..)] = malloc_args.as_slice() - && let Some(target_block) = b.body.get(*target_block_idx) - && let [Statement { - kind: StatementKind::StorageLive(target_var), - .. - }, Statement { - kind: - StatementKind::Assign(box_make, Rvalue::ShallowInitBox(Operand::Move(alloc_use), _)), - .. - }, rest @ ..] = target_block.statements.as_slice() - && alloc_use == malloc_dest - && let Some(local_id) = box_make.as_local() - && local_id == *target_var - && let TyKind::Adt(ty_ref) = box_make.ty().kind() - && let TypeId::Builtin(BuiltinTy::Box) = ty_ref.id - && let Some((assign_idx_in_rest, val, span)) = rest.iter().enumerate().find_map(|(idx, st)| { - if let Statement { - kind: StatementKind::Assign(box_deref, val), - span, - .. - } = st - && let Some((sub, ProjectionElem::Deref)) = box_deref.as_projection() - && sub == box_make - { - Some((idx, val, span)) - } else { - None - } - }) - { - box_place = box_make.clone(); - old_assign_idx = assign_idx_in_rest + 2; // +2 because rest skips the first two statements - value_to_write = val.clone(); - box_generics = ty_ref.generics.clone(); - second_block = *target_block_idx; - assign_span = *span; - unwind_target = *on_unwind; - } else { - continue; - } - - let first_block = b.body.get_mut(candidate_block_idx).unwrap(); - let box_place_local = box_place.as_local().unwrap(); - let value_to_write = match value_to_write { - Rvalue::Use(op) => op, - _ => { - // We need to create a new variable to store the value. - let name = b.locals[box_place_local].name.clone(); - let ty = box_generics.types[0].clone(); - let var = b.locals.new_var(name, ty); - first_block.statements.push(Statement::new( - assign_span, - StatementKind::StorageLive(var.as_local().unwrap()), - )); - first_block.statements.push(Statement::new( - assign_span, - StatementKind::Assign(var.clone(), value_to_write), - )); - Operand::Move(var) - } - }; - first_block.statements.push(Statement::new( - assign_span, - StatementKind::StorageLive(box_place_local), - )); - first_block.terminator.kind = TerminatorKind::Call { - call: Call { - func: FnOperand::Regular(FnPtr::new( - FnPtrKind::Fun(FunId::Builtin(BuiltinFunId::BoxNew)), - box_generics, - )), - args: vec![value_to_write], - dest: box_place, - }, - target: second_block, - on_unwind: unwind_target, - }; - - // We now update the statements in the second block. - let second_block = b.body.get_mut(second_block).unwrap(); - second_block.statements.get_mut(0).unwrap().kind = StatementKind::Nop; - second_block.statements.get_mut(1).unwrap().kind = StatementKind::Nop; - second_block - .statements - .get_mut(old_assign_idx) - .unwrap() - .kind = StatementKind::Nop; - } - - // Make sure we got all the `ShallowInitBox`es. - b.body.dyn_visit_in_body(|rvalue: &Rvalue| { - if rvalue.is_shallow_init_box() { - register_error!( - ctx, - b.span, - "Could not reconstruct `Box` initialization; \ - branching during `Box` initialization is not supported." - ); - } - }); - } -} diff --git a/charon/src/transform/resugar/reconstruct_vec_boxes.rs b/charon/src/transform/resugar/reconstruct_vec_boxes.rs new file mode 100644 index 000000000..4a2e5fbbb --- /dev/null +++ b/charon/src/transform/resugar/reconstruct_vec_boxes.rs @@ -0,0 +1,451 @@ +//! Reconstruct rustc's `vec![..]` lowering based on `Box>`. +//! +//! In `inline_selected_functions`, we inline the special `box_assume_init_into_vec_unsafe` +//! function. After that, a `vec![elems...]` expression ends up looking something like: +//! ```ignore +//! let mut box = Box::new_uninit::<[T; N]>(); +//! (((*box).1).0).0 = [elems...]; +//! let box = Box::assume_init(box); +//! .. +//! ``` +//! The split between assignment and `assume_init` is for performance. The `assume_init` call is +//! unsafe, so we rewrite it to use `Box::write` instead, and even `Box::new` if possible. +//! ```ignore +//! let box_uninit = Box::new_uninit::<[T; N]>(); +//! let arr = [elems...]; +//! let box = Box::write::<[T; N]>(box_uninit, arr); +//! .. +//! ``` +//! +//! See also: https://github.com/rust-lang/rust/pull/148190 + +use itertools::Itertools; +use std::collections::HashSet; + +use crate::ast::ullbc_ast_utils::StmtLoc; +use crate::name_matcher::NamePattern; +use crate::transform::ctx::UllbcPass; +use crate::transform::{CowBox, TransformCtx}; +use crate::ullbc_ast::*; + +pub struct Transform { + box_write: Option, +} + +struct Rewrite { + new_uninit_bid: BlockId, + new_uninit_target: BlockId, + drop_bid: BlockId, + target_bid: BlockId, + payload_loc: StmtLoc, + move_loc: StmtLoc, + arg_move_loc: StmtLoc, + span: Span, + payload_elems: Vec, + elem_ty: Ty, + len: Box, + uninit_box: Place, + branched_before_payload: bool, + box_array: Place, + box_array_generics: GenericArgs, + assume_init_generics: GenericArgs, + drop_on_unwind: BlockId, + assume_init_target: BlockId, +} + +struct PayloadAssign { + loc: StmtLoc, + span: Span, + payload_elems: Vec, + elem_ty: Ty, + len: Box, + branched_before_payload: bool, +} + +struct AssumeInitTail { + move_loc: StmtLoc, + drop_bid: BlockId, + target_bid: BlockId, + arg_move_loc: StmtLoc, + box_array: Place, + assume_init_generics: GenericArgs, + drop_on_unwind: BlockId, + assume_init_target: BlockId, +} + +fn assume_init_fn_ptr<'a>(ctx: &TransformCtx, call: &'a Call) -> Option<&'a FnPtr> { + if let FnOperand::Regular(fn_ptr) = &call.func + && let FnPtrKind::Fun(FunId::Regular(fid)) = *fn_ptr.kind + && ctx.translated.item_name(fid).short_str() == Some("assume_init") + { + Some(fn_ptr) + } else { + None + } +} + +fn box_inner(ty: &Ty) -> Option { + let TyKind::Adt(TypeDeclRef { + id: TypeId::Builtin(BuiltinTy::Box), + generics, + }) = ty.kind() + else { + return None; + }; + Some(generics.types[TypeVarId::from_usize(0)].clone()) +} + +fn box_generics(ty: &Ty) -> Option { + let TyKind::Adt(TypeDeclRef { + id: TypeId::Builtin(BuiltinTy::Box), + generics, + }) = ty.kind() + else { + return None; + }; + Some((**generics).clone()) +} + +/// Given `src`, find the unique statement of the form `src = [elems...]` +/// where the rvalue is an array aggregate. +/// +/// Also returns whether a straight-line path from `start` hits a branch before reaching the +/// assignment. We ignore unwind edges; this matches the later rewrite's ability to erase the +/// allocation when the normal path to initialization is linear. +fn find_array_assign(body: &ExprBody, start: BlockId, src_local: LocalId) -> Option { + let mut out = None; + for (bid, block) in body.body.iter_enumerated() { + for (idx, st) in block.statements.iter().enumerate() { + let Some((place, Rvalue::Aggregate(AggregateKind::Array(elem_ty, len), elems))) = + st.kind.as_assign() + else { + continue; + }; + if place.local_id() != Some(src_local) { + continue; + } + if out.is_some() { + return None; + } + + let loc = StmtLoc::new(bid, idx); + out = Some(PayloadAssign { + loc, + span: st.span, + payload_elems: elems.clone(), + elem_ty: elem_ty.clone(), + len: len.clone(), + branched_before_payload: branched_before(body, start, loc.block)?, + }); + } + } + out +} + +fn branched_before(body: &ExprBody, start: BlockId, target: BlockId) -> Option { + let mut block_id = start; + let mut visited = HashSet::new(); + while visited.insert(block_id) { + if block_id == target { + return Some(false); + } + + let block = &body.body[block_id]; + let targets = block.targets_ignoring_unwind(); + if targets.len() > 1 { + return Some(true); + } + block_id = targets.into_iter().exactly_one().ok()?; + } + None +} + +fn unique_target(term: &Terminator) -> Option { + term.targets_ignoring_unwind() + .into_iter() + .exactly_one() + .ok() +} + +fn find_next_move_of( + body: &ExprBody, + mut cursor: StmtLoc, + src: &Place, +) -> Option<(StmtLoc, Place)> { + let mut visited = HashSet::new(); + while visited.insert(cursor) { + 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() + && src_place == src + { + return Some((cursor, dst_place.clone())); + } + cursor = cursor.after(); + } + cursor = StmtLoc::block_start(unique_target(&block.terminator)?); + } + None +} + +fn find_next_drop( + body: &ExprBody, + mut block_id: BlockId, + dropped_place: &Place, +) -> Option<(BlockId, BlockId, BlockId)> { + let mut visited = HashSet::new(); + while visited.insert(block_id) { + let block = &body.body[block_id]; + if let TerminatorKind::Drop { + place: dropped, + target, + on_unwind, + .. + } = &block.terminator.kind + && dropped == dropped_place + { + return Some((block_id, *target, *on_unwind)); + } + block_id = unique_target(&block.terminator)?; + } + None +} + +fn find_move_in_block( + body: &ExprBody, + block: BlockId, + src: &Place, + dst: &Place, +) -> 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() + && dst_place == dst + && src_place == src + { + if out.is_some() { + return None; + } + out = Some(StmtLoc::new(block, statement)); + } + } + out +} + +fn find_assume_init_tail( + ctx: &TransformCtx, + body: &ExprBody, + cursor: StmtLoc, + uninit_box: &Place, +) -> Option { + let (move_loc, moved_box) = find_next_move_of(body, cursor, uninit_box)?; + let (drop_bid, target_bid, drop_on_unwind) = find_next_drop(body, move_loc.block, uninit_box)?; + + let target_block = &body.body[target_bid]; + let (call, assume_init_target, _unwind) = target_block.terminator.kind.as_call()?; + let assume_init_fn = assume_init_fn_ptr(ctx, call)?; + let [Operand::Move(init_box)] = call.args.as_slice() else { + return None; + }; + let arg_move_loc = find_move_in_block(body, target_bid, &moved_box, init_box)?; + + Some(AssumeInitTail { + move_loc, + drop_bid, + target_bid, + arg_move_loc, + box_array: call.dest.clone(), + assume_init_generics: assume_init_fn.generics.as_ref().clone(), + drop_on_unwind, + assume_init_target: *assume_init_target, + }) +} + +fn is_new_uninit_call(ctx: &TransformCtx, call: &Call) -> bool { + if !call.args.is_empty() { + return false; + } + + let FnOperand::Regular(fn_ptr) = &call.func else { + return false; + }; + let FnPtrKind::Fun(FunId::Regular(fid)) = *fn_ptr.kind else { + return false; + }; + ctx.translated.item_name(fid).short_str() == Some("new_uninit") +} + +impl Transform { + pub fn new(ctx: &mut TransformCtx) -> CowBox { + let pat = NamePattern::parse(crate::builtins::BOX_WRITE_PATTERN).unwrap(); + let box_write = ctx + .translated + .item_names + .iter() + .filter(|(_, name)| pat.matches(&ctx.translated, name)) + .filter_map(|(id, _)| id.as_fun()) + .copied() + .exactly_one() + .ok(); + CowBox::Owned(Box::new(Transform { box_write })) + } +} + +impl UllbcPass for Transform { + fn should_run(&self, options: &crate::options::TranslateOptions) -> bool { + options.treat_box_as_builtin && !options.monomorphize_with_hax && self.box_write.is_some() + } + + fn transform_body(&self, ctx: &mut TransformCtx, body: &mut ExprBody) { + // Checked in `should_run` + let box_write = self.box_write.unwrap(); + + // We are looking for, in (flattened) ULLBC: + // + // box1 = new_uninit() + // ... + // ((((*box1)).1).0).0 = [move _4] + // box2 = move box1 + // conditional_drop box1 + // box3 = move box2 + // box4 = assume_init(move box3) + let rewrites = body + .body + .iter_enumerated() + .filter_map(|(new_uninit_bid, block)| { + let TerminatorKind::Call { + call, + target: new_uninit_target, + .. + } = &block.terminator.kind + else { + return None; + }; + + if !is_new_uninit_call(ctx, call) { + return None; + } + // check uninit_box: Box> + let uninit_box = call.dest.clone(); + let maybe_uninit_array_ty = box_inner(uninit_box.ty())?; + let mu_decl = &ctx.translated.type_decls[maybe_uninit_array_ty.as_adt_id()?]; + if mu_decl.item_meta.lang_item.as_deref() != Some("maybe_uninit") { + return None; + }; + let uninit_box_l = uninit_box.local_id()?; + + // (*uninit_box).1.0.0 = [payload_elems...]: [elem_ty; len] + let payload = find_array_assign(body, *new_uninit_target, uninit_box_l)?; + + // assume_init(uninit_box2) + let tail = find_assume_init_tail(ctx, body, payload.loc.after(), &uninit_box)?; + let box_array_generics = box_generics(tail.box_array.ty())?; + + Some(Rewrite { + new_uninit_bid, + new_uninit_target: *new_uninit_target, + drop_bid: tail.drop_bid, + target_bid: tail.target_bid, + payload_loc: payload.loc, + move_loc: tail.move_loc, + arg_move_loc: tail.arg_move_loc, + span: payload.span, + payload_elems: payload.payload_elems, + elem_ty: payload.elem_ty, + len: payload.len, + uninit_box, + branched_before_payload: payload.branched_before_payload, + box_array_generics, + assume_init_generics: tail.assume_init_generics, + drop_on_unwind: tail.drop_on_unwind, + box_array: tail.box_array, + assume_init_target: tail.assume_init_target, + }) + }); + + for rw in rewrites.collect::>() { + let array_ty = Ty::mk_array(rw.elem_ty.clone(), *rw.len.clone()); + let array_local = body.locals.new_var(None, array_ty.clone()); + let box_array_ty = rw.box_array.ty().clone(); + let box_array_local = body.locals.new_var(None, box_array_ty.clone()); + + let array_lid = array_local.as_local().unwrap(); + let box_array_lid = box_array_local.as_local().unwrap(); + + body[rw.move_loc].kind = StatementKind::Nop; + body[rw.arg_move_loc].kind = StatementKind::Nop; + + body.body[rw.payload_loc.block].statements.splice( + rw.payload_loc.statement..=rw.payload_loc.statement, + [ + StatementKind::StorageLive(array_lid), + StatementKind::Assign( + array_local.clone(), + Rvalue::Aggregate( + AggregateKind::Array(rw.elem_ty.clone(), rw.len.clone()), + rw.payload_elems, + ), + ), + ] + .map(|k| Statement::new(rw.span, k)), + ); + + let (fn_ptr, args) = if rw.branched_before_payload { + ( + FnPtr::new( + FnPtrKind::Fun(FunId::Regular(box_write)), + rw.assume_init_generics, + ), + vec![ + Operand::Move(rw.uninit_box), + Operand::Move(array_local.clone()), + ], + ) + } else { + body.body[rw.new_uninit_bid].terminator.kind = TerminatorKind::Goto { + target: rw.new_uninit_target, + }; + ( + FnPtr::new( + FnPtrKind::Fun(FunId::Builtin(BuiltinFunId::BoxNew)), + rw.box_array_generics, + ), + vec![Operand::Move(array_local.clone())], + ) + }; + + let drop_block = &mut body.body[rw.drop_bid]; + drop_block.statements.push(Statement::new( + rw.span, + StatementKind::StorageLive(box_array_lid), + )); + drop_block.terminator.kind = TerminatorKind::Call { + call: Call { + func: FnOperand::Regular(fn_ptr), + args, + dest: box_array_local.clone(), + }, + target: rw.target_bid, + on_unwind: rw.drop_on_unwind, + }; + + let target_block = &mut body.body[rw.target_bid]; + target_block.statements.push(Statement::new( + rw.span, + StatementKind::StorageDead(array_lid), + )); + target_block.statements.push(Statement::new( + rw.span, + StatementKind::Assign(rw.box_array, Rvalue::Use(Operand::Move(box_array_local))), + )); + target_block.statements.push(Statement::new( + rw.span, + StatementKind::StorageDead(box_array_lid), + )); + target_block.terminator.kind = TerminatorKind::Goto { + target: rw.assume_init_target, + }; + } + } +} 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 bc4b8ffda..963a91583 100644 --- a/charon/src/transform/simplify_output/index_to_function_calls.rs +++ b/charon/src/transform/simplify_output/index_to_function_calls.rs @@ -186,8 +186,9 @@ impl VisitBodyMut for IndexVisitor<'_, '_> { | Discriminant(..) | Len(..) => self.visit_inner_with_mutability(x, false), - Use(_) | NullaryOp(..) | UnaryOp(..) | BinaryOp(..) | Aggregate(..) | Repeat(..) - | ShallowInitBox(..) => self.visit_inner(x), + 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 c60074e49..ed7738593 100644 --- a/charon/src/transform/simplify_output/inline_selected_functions.rs +++ b/charon/src/transform/simplify_output/inline_selected_functions.rs @@ -31,7 +31,11 @@ impl Transform { .is_global_initializer .and_then(|gid| ctx.translated.global_decls.get(gid)) .is_some_and(|gdecl| matches!(gdecl.global_kind, GlobalKind::AnonConst)); - is_local_panic_fn || is_anon_const_initializer + let is_vec_construction_fn = decl.item_meta.lang_item.as_deref() + == Some(builtins::BOX_ASSUME_INIT_INTO_VEC_UNSAFE); + is_local_panic_fn + || (is_anon_const_initializer && !ctx.options.raw_consts) + || (is_vec_construction_fn && ctx.options.treat_box_as_builtin) }) }) .collect(); @@ -56,7 +60,7 @@ impl UllbcPass for Transform { continue; }; let TerminatorKind::Call { - call, + call: Call { func, args, dest }, target, on_unwind, } = &mut block.terminator.kind @@ -65,8 +69,9 @@ impl UllbcPass for Transform { }; let target = *target; let on_unwind = *on_unwind; - let dest_place = call.dest.clone(); - let FnOperand::Regular(fn_ptr) = &call.func else { + let dest_place = dest.clone(); + let args = args.clone(); + let FnOperand::Regular(fn_ptr) = &func else { continue; }; let FnPtrKind::Fun(FunId::Regular(fun_id)) = fn_ptr.kind.as_ref() else { @@ -102,13 +107,6 @@ impl UllbcPass for Transform { inner_body.substitute(&fn_ptr.generics) }; - // The inner body assumes the return place is live; this is not the case once we inline - // it. - inner_body.body[0].statements.insert( - 0, - Statement::new(Span::dummy(), StatementKind::StorageLive(LocalId::ZERO)), - ); - let return_local = outer_body.locals.locals.next_idx(); inner_body.dyn_visit_in_body_mut(|l: &mut LocalId| { *l += return_local; @@ -118,6 +116,23 @@ impl UllbcPass for Transform { .locals .extend(mem::take(&mut inner_body.locals.locals)); + // The inner body assumes the return and arg places are live; allocate them, and + // initialize the args. + inner_body.body[0].statements.splice( + 0..0, + [StatementKind::StorageLive(return_local)] + .into_iter() + .chain(args.into_iter().enumerate().flat_map(|(i, arg)| { + let arg_local = return_local + i + 1; + let arg_place = outer_body.locals.place_for_var(arg_local); + [ + StatementKind::StorageLive(arg_local), + StatementKind::Assign(arg_place, Rvalue::Use(arg)), + ] + })) + .map(|kind| Statement::new(span, kind)), + ); + let mut final_block = BlockData::new_goto(span, target); // The inner body will write to `return_place`, but the outer body expects the value at diff --git a/charon/tests/ui/copy_nonoverlapping.out b/charon/tests/ui/copy_nonoverlapping.out index 809084d43..c10c25387 100644 --- a/charon/tests/ui/copy_nonoverlapping.out +++ b/charon/tests/ui/copy_nonoverlapping.out @@ -179,7 +179,8 @@ where [@TraitClause0]: Sized, = -pub fn core::intrinsics::align_of() -> usize +// Full name: core::intrinsics::align_of +pub fn align_of() -> usize where [@TraitClause0]: Sized, = @@ -191,6 +192,130 @@ impl Copy for usize { non-dyn-compatible } +// Full name: core::ptr::alignment::AlignmentEnum +enum AlignmentEnum { + _Align1Shl0, + _Align1Shl1, + _Align1Shl2, + _Align1Shl3, + _Align1Shl4, + _Align1Shl5, + _Align1Shl6, + _Align1Shl7, + _Align1Shl8, + _Align1Shl9, + _Align1Shl10, + _Align1Shl11, + _Align1Shl12, + _Align1Shl13, + _Align1Shl14, + _Align1Shl15, + _Align1Shl16, + _Align1Shl17, + _Align1Shl18, + _Align1Shl19, + _Align1Shl20, + _Align1Shl21, + _Align1Shl22, + _Align1Shl23, + _Align1Shl24, + _Align1Shl25, + _Align1Shl26, + _Align1Shl27, + _Align1Shl28, + _Align1Shl29, + _Align1Shl30, + _Align1Shl31, + _Align1Shl32, + _Align1Shl33, + _Align1Shl34, + _Align1Shl35, + _Align1Shl36, + _Align1Shl37, + _Align1Shl38, + _Align1Shl39, + _Align1Shl40, + _Align1Shl41, + _Align1Shl42, + _Align1Shl43, + _Align1Shl44, + _Align1Shl45, + _Align1Shl46, + _Align1Shl47, + _Align1Shl48, + _Align1Shl49, + _Align1Shl50, + _Align1Shl51, + _Align1Shl52, + _Align1Shl53, + _Align1Shl54, + _Align1Shl55, + _Align1Shl56, + _Align1Shl57, + _Align1Shl58, + _Align1Shl59, + _Align1Shl60, + _Align1Shl61, + _Align1Shl62, + _Align1Shl63, +} + +// Full name: core::ptr::alignment::Alignment +pub struct Alignment { + _inner_repr_trick: AlignmentEnum, +} + +// Full name: core::mem::SizedTypeProperties +pub trait SizedTypeProperties +{ + parent_clause0 : [@TraitClause0]: Sized + const SIZE : usize + const ALIGN : usize + const ALIGNMENT : Alignment + const IS_ZST : bool + const LAYOUT : Layout + const MAX_SLICE_LEN : usize + non-dyn-compatible +} + +// Full name: core::mem::SizedTypeProperties::SIZE +#[lang_item("mem_size_const")] +pub fn SIZE() -> usize +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: usize; // return + + _0 = size_of[@TraitClause0::parent_clause0]() + return +} + +// Full name: core::mem::SizedTypeProperties::SIZE +#[lang_item("mem_size_const")] +pub const SIZE: usize +where + [@TraitClause0]: SizedTypeProperties, + = SIZE() + +// Full name: core::mem::SizedTypeProperties::ALIGN +#[lang_item("mem_align_const")] +pub fn ALIGN() -> usize +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: usize; // return + + _0 = align_of[@TraitClause0::parent_clause0]() + return +} + +// Full name: core::mem::SizedTypeProperties::ALIGN +#[lang_item("mem_align_const")] +pub const ALIGN: usize +where + [@TraitClause0]: SizedTypeProperties, + = ALIGN() + // Full name: core::panicking::panic_nounwind_fmt pub fn panic_nounwind_fmt<'_0>(fmt_1: Arguments<'_0>, force_no_backtrace_2: bool) -> ! { @@ -273,79 +398,6 @@ fn core::ptr::alignment::{Alignment}::new_unchecked::precondition_check(align_1: return } -// Full name: core::ptr::alignment::AlignmentEnum -enum AlignmentEnum { - _Align1Shl0, - _Align1Shl1, - _Align1Shl2, - _Align1Shl3, - _Align1Shl4, - _Align1Shl5, - _Align1Shl6, - _Align1Shl7, - _Align1Shl8, - _Align1Shl9, - _Align1Shl10, - _Align1Shl11, - _Align1Shl12, - _Align1Shl13, - _Align1Shl14, - _Align1Shl15, - _Align1Shl16, - _Align1Shl17, - _Align1Shl18, - _Align1Shl19, - _Align1Shl20, - _Align1Shl21, - _Align1Shl22, - _Align1Shl23, - _Align1Shl24, - _Align1Shl25, - _Align1Shl26, - _Align1Shl27, - _Align1Shl28, - _Align1Shl29, - _Align1Shl30, - _Align1Shl31, - _Align1Shl32, - _Align1Shl33, - _Align1Shl34, - _Align1Shl35, - _Align1Shl36, - _Align1Shl37, - _Align1Shl38, - _Align1Shl39, - _Align1Shl40, - _Align1Shl41, - _Align1Shl42, - _Align1Shl43, - _Align1Shl44, - _Align1Shl45, - _Align1Shl46, - _Align1Shl47, - _Align1Shl48, - _Align1Shl49, - _Align1Shl50, - _Align1Shl51, - _Align1Shl52, - _Align1Shl53, - _Align1Shl54, - _Align1Shl55, - _Align1Shl56, - _Align1Shl57, - _Align1Shl58, - _Align1Shl59, - _Align1Shl60, - _Align1Shl61, - _Align1Shl62, - _Align1Shl63, -} - -// Full name: core::ptr::alignment::Alignment -pub struct Alignment { - _inner_repr_trick: AlignmentEnum, -} - // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -425,6 +477,61 @@ where _2 = unwrap_failed() } +// Full name: core::mem::SizedTypeProperties::ALIGNMENT +pub fn ALIGNMENT() -> Alignment +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: Alignment; // return + let _1: Option[{built_in impl Sized for Alignment}]; // anonymous local + + storage_live(_1) + _1 = new(const @TraitClause0::ALIGN) + _0 = unwrap[{built_in impl Sized for Alignment}](move _1) + storage_dead(_1) + return +} + +// Full name: core::mem::SizedTypeProperties::ALIGNMENT +pub const ALIGNMENT: Alignment +where + [@TraitClause0]: SizedTypeProperties, + = ALIGNMENT() + +// Full name: core::mem::SizedTypeProperties::IS_ZST +pub fn IS_ZST() -> bool +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: bool; // return + + _0 = const @TraitClause0::SIZE == const 0 : usize + return +} + +// Full name: core::mem::SizedTypeProperties::IS_ZST +pub const IS_ZST: bool +where + [@TraitClause0]: SizedTypeProperties, + = IS_ZST() + +// Full name: core::mem::SizedTypeProperties::LAYOUT +pub fn LAYOUT() -> Layout +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: Layout; // return + + _0 = from_size_align_unchecked(const @TraitClause0::SIZE, const @TraitClause0::ALIGN) + return +} + +// Full name: core::mem::SizedTypeProperties::LAYOUT +pub const LAYOUT: Layout +where + [@TraitClause0]: SizedTypeProperties, + = LAYOUT() + pub fn core::num::{usize}::MAX() -> usize { let _0: usize; // return @@ -449,19 +556,6 @@ pub fn core::num::{isize}::MAX() -> isize pub const core::num::{isize}::MAX: isize = core::num::{isize}::MAX() -// Full name: core::mem::SizedTypeProperties -pub trait SizedTypeProperties -{ - parent_clause0 : [@TraitClause0]: Sized - const SIZE : usize - const ALIGN : usize - const ALIGNMENT : Alignment - const IS_ZST : bool - const LAYOUT : Layout - const MAX_SLICE_LEN : usize - non-dyn-compatible -} - // Full name: core::mem::SizedTypeProperties::MAX_SLICE_LEN pub fn MAX_SLICE_LEN() -> usize where @@ -502,106 +596,6 @@ where [@TraitClause0]: SizedTypeProperties, = MAX_SLICE_LEN() -// Full name: core::mem::SizedTypeProperties::LAYOUT -pub fn LAYOUT() -> Layout -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: Layout; // return - - _0 = from_size_align_unchecked(const @TraitClause0::SIZE, const @TraitClause0::ALIGN) - return -} - -// Full name: core::mem::SizedTypeProperties::LAYOUT -pub const LAYOUT: Layout -where - [@TraitClause0]: SizedTypeProperties, - = LAYOUT() - -// Full name: core::mem::SizedTypeProperties::IS_ZST -pub fn IS_ZST() -> bool -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: bool; // return - - _0 = const @TraitClause0::SIZE == const 0 : usize - return -} - -// Full name: core::mem::SizedTypeProperties::IS_ZST -pub const IS_ZST: bool -where - [@TraitClause0]: SizedTypeProperties, - = IS_ZST() - -// Full name: core::mem::SizedTypeProperties::ALIGN -#[lang_item("mem_align_const")] -pub fn ALIGN() -> usize -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: usize; // return - - _0 = core::intrinsics::align_of[@TraitClause0::parent_clause0]() - return -} - -// Full name: core::mem::SizedTypeProperties::ALIGN -#[lang_item("mem_align_const")] -pub const ALIGN: usize -where - [@TraitClause0]: SizedTypeProperties, - = ALIGN() - -// Full name: core::mem::SizedTypeProperties::SIZE -#[lang_item("mem_size_const")] -pub fn SIZE() -> usize -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: usize; // return - - _0 = size_of[@TraitClause0::parent_clause0]() - return -} - -// Full name: core::mem::SizedTypeProperties::SIZE -#[lang_item("mem_size_const")] -pub const SIZE: usize -where - [@TraitClause0]: SizedTypeProperties, - = SIZE() - -#[lang_item("mem_align_of")] -pub fn core::mem::align_of() -> usize -where - [@TraitClause0]: Sized, -{ - let _0: usize; // return - - _0 = const {impl SizedTypeProperties for T}[@TraitClause0]::ALIGN - return -} - -// Full name: core::mem::SizedTypeProperties::ALIGNMENT -pub fn ALIGNMENT() -> Alignment -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: Alignment; // return - - _0 = of[@TraitClause0::parent_clause0]() - return -} - -// Full name: core::mem::SizedTypeProperties::ALIGNMENT -pub const ALIGNMENT: Alignment -where - [@TraitClause0]: SizedTypeProperties, - = ALIGNMENT() - // Full name: core::mem::{impl SizedTypeProperties for T} impl SizedTypeProperties for T where @@ -617,31 +611,6 @@ where non-dyn-compatible } -// Full name: core::ptr::alignment::{Alignment}::of -pub fn of() -> Alignment -where - [@TraitClause0]: Sized, -{ - let _0: Alignment; // return - let _1: Alignment; // anonymous local - let _2: Alignment; // anonymous local - let _3: Option[{built_in impl Sized for Alignment}]; // anonymous local - let _4: usize; // anonymous local - - storage_live(_1) - storage_live(_2) - storage_live(_3) - storage_live(_4) - _4 = core::mem::align_of[@TraitClause0]() - _3 = new(move _4) - storage_dead(_4) - _2 = unwrap[{built_in impl Sized for Alignment}](move _3) - storage_dead(_3) - _1 = move _2 - _0 = move _1 - return -} - fn core::ptr::copy_nonoverlapping::precondition_check(_1: *const (), _2: *mut (), _3: usize, _4: usize, _5: usize) = diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index 2eba27bec..d94b9316b 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -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)) -> (Ty2, 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 @@ -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/filtering/start_from_errors.out b/charon/tests/ui/filtering/start_from_errors.out index 1bbec7bae..86ed12614 100644 --- a/charon/tests/ui/filtering/start_from_errors.out +++ b/charon/tests/ui/filtering/start_from_errors.out @@ -1,28 +1,28 @@ error: failed to parse pattern `std::iter:once` (expected eof at :once) -error: when processing starting pattern `start_from_errors::module1`: path `start_from_errors` does not correspond to any item; did you mean `crate::start_from_errors`? +error: failed to resolve item path `start_from_errors::module1`: path `start_from_errors` does not correspond to any item; did you mean `crate::start_from_errors`? -error: when processing starting pattern `module2`: path `module2` does not correspond to any item; did you mean `crate::module2`? +error: failed to resolve item path `module2`: path `module2` does not correspond to any item; did you mean `crate::module2`? error: Cannot register item `core::ops::deref::Deref::Target` with kind `AssocTy` --> /rustc/library/core/src/ops/deref.rs:144:5 -error: when processing starting pattern `{impl crate::Type}`: `--start-from` does not support inherent impls +error: failed to resolve item path `{impl crate::Type}`: `--start-from` does not support inherent impls --> /rustc/library/core/src/ops/deref.rs:0:1 -error: when processing starting pattern `{impl crate::Trait for &crate::Type}`: `--start-from` only supports implementations on named types +error: failed to resolve item path `{impl crate::Trait for &crate::Type}`: `--start-from` only supports implementations on named types --> /rustc/library/core/src/ops/deref.rs:0:1 -error: when processing starting pattern `{impl crate::Trait for crate::MissingType}`: path `crate::MissingType` does not correspond to any item +error: failed to resolve item path `{impl crate::Trait for crate::MissingType}`: path `crate::MissingType` does not correspond to any item --> /rustc/library/core/src/ops/deref.rs:0:1 -error: when processing starting pattern `{impl crate::Trait<_> for _}`: `--start-from` does not support trait generics +error: failed to resolve item path `{impl crate::Trait<_> for _}`: `--start-from` does not support trait generics --> /rustc/library/core/src/ops/deref.rs:0:1 -error: when processing starting pattern `{impl crate::Trait for crate::Type}::missing_method`: path `{impl crate::Trait for crate::Type}::missing_method` does not correspond to any item +error: failed to resolve item path `{impl crate::Trait for crate::Type}::missing_method`: path `{impl crate::Trait for crate::Type}::missing_method` does not correspond to any item --> /rustc/library/core/src/ops/deref.rs:0:1 -error: when processing starting pattern `crate::{impl crate::Trait for crate::Type}`: `--start-from` only supports impl patterns if they're the first element of the path +error: failed to resolve item path `crate::{impl crate::Trait for crate::Type}`: `--start-from` only supports impl patterns if they're the first element of the path --> /rustc/library/core/src/ops/deref.rs:0:1 ERROR Code failed to compile diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index 340c12b7d..de1eb109e 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -107,7 +107,7 @@ pub struct PhantomData {} // Full name: core::num::niche_types::UsizeNoHighBit pub struct UsizeNoHighBit { - usize, + type_error("Unsupported type: "pattern_type!(usize is 0..=core::::num::niche_types::UsizeNoHighBit::0::{constant#1})""), } // Full name: core::num::{usize}::MAX diff --git a/charon/tests/ui/issue-114-opaque-bodies.rs b/charon/tests/ui/issue-114-opaque-bodies.rs index 01173e272..6c6c09422 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.rs +++ b/charon/tests/ui/issue-114-opaque-bodies.rs @@ -1,3 +1,4 @@ +//@ ignore-warnings //@ charon-args=--extract-opaque-bodies //@ charon-arg=--opaque={impl core::marker::Destruct for alloc::vec::Vec} //@ aux-crate=issue-114-opaque-bodies-aux.rs diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out index d23222a98..5fcf848d8 100644 --- a/charon/tests/ui/issue-165-vec-macro.out +++ b/charon/tests/ui/issue-165-vec-macro.out @@ -42,13 +42,6 @@ impl Clone for i32 { #[lang_item("global_alloc_ty")] pub struct Global {} -// Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) -where - [@TraitClause0]: MetaSized, - [@TraitClause1]: Sized, -= - // Full name: alloc::vec::Vec #[lang_item("Vec")] pub opaque type Vec @@ -57,7 +50,6 @@ where [@TraitClause1]: Sized, // Full name: alloc::slice::{[T]}::into_vec -#[lang_item("slice_into_vec")] pub fn into_vec(_1: alloc::boxed::Box<[T]>[{built_in impl MetaSized for [T]}, @TraitClause1]) -> Vec[@TraitClause0, @TraitClause1] where [@TraitClause0]: Sized, @@ -84,33 +76,33 @@ fn foo() { let _0: (); // return let _v_1: Vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}]; // local - let _2: alloc::boxed::Box<[i32]>[{built_in impl MetaSized for [i32]}, {built_in impl Sized for Global}]; // anonymous local - let _3: alloc::boxed::Box<[i32; 1 : usize]>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _4: alloc::boxed::Box<[i32; 1 : usize]>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _v2_5: Vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}]; // local + let _v2_2: Vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}]; // local + let ret_3: Vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}]; // local + let x_4: alloc::boxed::Box<[i32; 1 : usize]>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_5: alloc::boxed::Box<[i32]>[{built_in impl MetaSized for [i32]}, {built_in impl Sized for Global}]; // local let _6: [i32; 1 : usize]; // anonymous local + let _7: alloc::boxed::Box<[i32; 1 : usize]>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local _0 = () storage_live(_v_1) - storage_live(_2) - storage_live(_3) storage_live(_6) _6 = [const 1 : i32] - storage_live(_4) - _4 = @BoxNew<[i32; 1 : usize], Global>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}](move _6) - _3 = move _4 - _2 = unsize_cast[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[i32]>[{built_in impl MetaSized for [i32]}, {built_in impl Sized for Global}], 1 : usize>(move _3) - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[i32; 1 : usize], Global>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]] _3 - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[i32; 1 : usize], Global>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}]] _4 - storage_dead(_4) - storage_dead(_3) - _v_1 = into_vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}](move _2) - storage_dead(_2) - storage_live(_v2_5) - _v2_5 = from_elem[{built_in impl Sized for i32}, {impl Clone for i32}](const 1 : i32, const 10 : usize) + storage_live(_7) + _7 = @BoxNew<[i32; 1 : usize], Global>[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}](move _6) + storage_live(ret_3) + storage_live(x_4) + storage_live(y_5) + storage_dead(_6) + x_4 = move _7 + storage_dead(_7) + y_5 = unsize_cast[{built_in impl MetaSized for [i32; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[i32]>[{built_in impl MetaSized for [i32]}, {built_in impl Sized for Global}], 1 : usize>(move x_4) + ret_3 = into_vec[{built_in impl Sized for i32}, {built_in impl Sized for Global}](move y_5) + _v_1 = move ret_3 + storage_live(_v2_2) + _v2_2 = from_elem[{built_in impl Sized for i32}, {impl Clone for i32}](const 1 : i32, const 10 : usize) _0 = () - conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for i32}, {built_in impl Sized for Global}]] _v2_5 - storage_dead(_v2_5) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for i32}, {built_in impl Sized for Global}]] _v2_2 + storage_dead(_v2_2) conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for i32}, {built_in impl Sized for Global}]] _v_1 storage_dead(_v_1) return @@ -124,31 +116,31 @@ pub fn bar() { let _0: (); // return let _1: Vec[{built_in impl Sized for Foo}, {built_in impl Sized for Global}]; // anonymous local - let _2: alloc::boxed::Box<[Foo]>[{built_in impl MetaSized for [Foo]}, {built_in impl Sized for Global}]; // anonymous local - let _3: alloc::boxed::Box<[Foo; 1 : usize]>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _4: alloc::boxed::Box<[Foo; 1 : usize]>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _5: Foo; // anonymous local + let _2: Foo; // anonymous local + let ret_3: Vec[{built_in impl Sized for Foo}, {built_in impl Sized for Global}]; // local + let x_4: alloc::boxed::Box<[Foo; 1 : usize]>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_5: alloc::boxed::Box<[Foo]>[{built_in impl MetaSized for [Foo]}, {built_in impl Sized for Global}]; // local let _6: [Foo; 1 : usize]; // anonymous local + let _7: alloc::boxed::Box<[Foo; 1 : usize]>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local _0 = () storage_live(_1) storage_live(_2) - storage_live(_3) + _2 = Foo { } storage_live(_6) - _6 = [move _5] - storage_live(_4) - _4 = @BoxNew<[Foo; 1 : usize], Global>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}](move _6) - storage_live(_5) - _5 = Foo { } - storage_dead(_5) - _3 = move _4 - _2 = unsize_cast[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[Foo]>[{built_in impl MetaSized for [Foo]}, {built_in impl Sized for Global}], 1 : usize>(move _3) - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[Foo; 1 : usize], Global>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]] _3 - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[Foo; 1 : usize], Global>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}]] _4 - storage_dead(_4) - storage_dead(_3) - _1 = into_vec[{built_in impl Sized for Foo}, {built_in impl Sized for Global}](move _2) + _6 = [move _2] storage_dead(_2) + storage_live(_7) + _7 = @BoxNew<[Foo; 1 : usize], Global>[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}](move _6) + storage_live(ret_3) + storage_live(x_4) + storage_live(y_5) + storage_dead(_6) + x_4 = move _7 + storage_dead(_7) + y_5 = unsize_cast[{built_in impl MetaSized for [Foo; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[Foo]>[{built_in impl MetaSized for [Foo]}, {built_in impl Sized for Global}], 1 : usize>(move x_4) + ret_3 = into_vec[{built_in impl Sized for Foo}, {built_in impl Sized for Global}](move y_5) + _1 = move ret_3 conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for Foo}, {built_in impl Sized for Global}]] _1 storage_dead(_1) _0 = () diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index aacb9eeb2..e607d94c5 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -613,84 +613,6 @@ where Break(B), } -// Full name: core::option::Option -#[lang_item("Option")] -pub enum Option -where - [@TraitClause0]: Sized, -{ - None, - Some(T), -} - -pub fn core::ptr::alignment::{Alignment}::new(align_1: usize) -> Option[{built_in impl Sized for Alignment}] -{ - let _0: Option[{built_in impl Sized for Alignment}]; // return - let align_1: usize; // arg #1 - let _2: Alignment; // anonymous local - let _3: u32; // anonymous local - let _4: (); // anonymous local - let _5: bool; // anonymous local - let _6: Option[{built_in impl Sized for Alignment}]; // anonymous local - - storage_live(_4) - storage_live(_3) - _3 = ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy align_1) - switch copy _3 { - 1 : u32 => { - }, - _ => { - storage_dead(_3) - storage_live(_6) - _6 = Option::None { } - _0 = move _6 - return - }, - } - storage_dead(_3) - storage_live(_2) - storage_live(_5) - _5 = ub_checks - if move _5 { - _4 = core::ptr::alignment::{Alignment}::new_unchecked::precondition_check(copy align_1) - } else { - } - _2 = transmute(copy align_1) - _0 = Option::Some { 0: move _2 } - storage_dead(_2) - return -} - -// Full name: core::option::unwrap_failed -fn unwrap_failed() -> ! -{ - let _0: !; // return - - panic(core::panicking::panic) -} - -// Full name: core::option::{Option[@TraitClause0]}::unwrap -#[lang_item("option_unwrap")] -pub fn unwrap(self_1: Option[@TraitClause0]) -> T -where - [@TraitClause0]: Sized, -{ - let val_0: T; // return - let self_1: Option[@TraitClause0]; // arg #1 - let _2: !; // anonymous local - - storage_live(_2) - match self_1 { - Option::None => { - }, - Option::Some => { - val_0 = move (self_1 as variant Option::Some).0 - return - }, - } - _2 = unwrap_failed() -} - pub fn core::num::{usize}::MAX() -> usize { let _0: usize; // return @@ -813,7 +735,107 @@ where [@TraitClause0]: SizedTypeProperties, = IS_ZST() -pub fn core::intrinsics::align_of() -> usize +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option +where + [@TraitClause0]: Sized, +{ + None, + Some(T), +} + +pub fn core::ptr::alignment::{Alignment}::new(align_1: usize) -> Option[{built_in impl Sized for Alignment}] +{ + let _0: Option[{built_in impl Sized for Alignment}]; // return + let align_1: usize; // arg #1 + let _2: Alignment; // anonymous local + let _3: u32; // anonymous local + let _4: (); // anonymous local + let _5: bool; // anonymous local + let _6: Option[{built_in impl Sized for Alignment}]; // anonymous local + + storage_live(_4) + storage_live(_3) + _3 = ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy align_1) + switch copy _3 { + 1 : u32 => { + }, + _ => { + storage_dead(_3) + storage_live(_6) + _6 = Option::None { } + _0 = move _6 + return + }, + } + storage_dead(_3) + storage_live(_2) + storage_live(_5) + _5 = ub_checks + if move _5 { + _4 = core::ptr::alignment::{Alignment}::new_unchecked::precondition_check(copy align_1) + } else { + } + _2 = transmute(copy align_1) + _0 = Option::Some { 0: move _2 } + storage_dead(_2) + return +} + +// Full name: core::option::unwrap_failed +fn unwrap_failed() -> ! +{ + let _0: !; // return + + panic(core::panicking::panic) +} + +// Full name: core::option::{Option[@TraitClause0]}::unwrap +#[lang_item("option_unwrap")] +pub fn unwrap(self_1: Option[@TraitClause0]) -> T +where + [@TraitClause0]: Sized, +{ + let val_0: T; // return + let self_1: Option[@TraitClause0]; // arg #1 + let _2: !; // anonymous local + + storage_live(_2) + match self_1 { + Option::None => { + }, + Option::Some => { + val_0 = move (self_1 as variant Option::Some).0 + return + }, + } + _2 = unwrap_failed() +} + +// Full name: core::mem::SizedTypeProperties::ALIGNMENT +pub fn ALIGNMENT() -> Alignment +where + [@TraitClause0]: SizedTypeProperties, +{ + let _0: Alignment; // return + let _1: Option[{built_in impl Sized for Alignment}]; // anonymous local + + storage_live(_1) + _1 = core::ptr::alignment::{Alignment}::new(const @TraitClause0::ALIGN) + _0 = unwrap[{built_in impl Sized for Alignment}](move _1) + storage_dead(_1) + return +} + +// Full name: core::mem::SizedTypeProperties::ALIGNMENT +pub const ALIGNMENT: Alignment +where + [@TraitClause0]: SizedTypeProperties, + = ALIGNMENT() + +// Full name: core::intrinsics::align_of +pub fn align_of() -> usize where [@TraitClause0]: Sized, = @@ -826,7 +848,7 @@ where { let _0: usize; // return - _0 = core::intrinsics::align_of[@TraitClause0::parent_clause0]() + _0 = align_of[@TraitClause0::parent_clause0]() return } @@ -862,34 +884,6 @@ where [@TraitClause0]: SizedTypeProperties, = SIZE() -#[lang_item("mem_align_of")] -pub fn core::mem::align_of() -> usize -where - [@TraitClause0]: Sized, -{ - let _0: usize; // return - - _0 = const {impl SizedTypeProperties for T}[@TraitClause0]::ALIGN - return -} - -// Full name: core::mem::SizedTypeProperties::ALIGNMENT -pub fn ALIGNMENT() -> Alignment -where - [@TraitClause0]: SizedTypeProperties, -{ - let _0: Alignment; // return - - _0 = of[@TraitClause0::parent_clause0]() - return -} - -// Full name: core::mem::SizedTypeProperties::ALIGNMENT -pub const ALIGNMENT: Alignment -where - [@TraitClause0]: SizedTypeProperties, - = ALIGNMENT() - // Full name: core::mem::{impl SizedTypeProperties for T} impl SizedTypeProperties for T where @@ -905,31 +899,6 @@ where non-dyn-compatible } -// Full name: core::ptr::alignment::{Alignment}::of -pub fn of() -> Alignment -where - [@TraitClause0]: Sized, -{ - let _0: Alignment; // return - let _1: Alignment; // anonymous local - let _2: Alignment; // anonymous local - let _3: Option[{built_in impl Sized for Alignment}]; // anonymous local - let _4: usize; // anonymous local - - storage_live(_1) - storage_live(_2) - storage_live(_3) - storage_live(_4) - _4 = core::mem::align_of[@TraitClause0]() - _3 = core::ptr::alignment::{Alignment}::new(move _4) - storage_dead(_4) - _2 = unwrap[{built_in impl Sized for Alignment}](move _3) - storage_dead(_3) - _1 = move _2 - _0 = move _1 - return -} - // Full name: core::intrinsics::write_bytes pub unsafe fn write_bytes(dst_1: *mut T, val_2: u8, count_3: usize) where @@ -949,77 +918,88 @@ where let layout_2: Layout; // arg #2 let _3: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local let self_4: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let ptr_5: NonNull<[u8]>; // local - let _6: (); // anonymous local - let self_7: *mut u8; // local - let self_8: NonNull; // local - let count_9: usize; // local - let v_10: NonNull<[u8]>; // local - let _11: *const u8; // anonymous local - let _12: *mut [u8]; // anonymous local - let _13: (); // anonymous local - let _14: *const (); // anonymous local + let _5: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let ptr_6: NonNull<[u8]>; // local + let _7: (); // anonymous local + let self_8: *mut u8; // local + let self_9: NonNull; // local + let count_10: usize; // local + let v_11: NonNull<[u8]>; // local + let _12: *const u8; // anonymous local + let _13: *mut [u8]; // anonymous local + let _14: isize; // anonymous local let _15: bool; // anonymous local - let _16: bool; // anonymous local - let _17: AllocError; // anonymous local - let _18: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let _16: (); // anonymous local + let _17: *const (); // anonymous local + let _18: bool; // anonymous local + let _19: bool; // anonymous local + let _20: AllocError; // anonymous local + let _21: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - storage_live(ptr_5) - storage_live(_6) - storage_live(_12) + storage_live(_5) + storage_live(ptr_6) + storage_live(_7) storage_live(_13) + storage_live(_16) storage_live(_3) storage_live(self_4) self_4 = @TraitClause0::allocate<'3>(move self_1, move layout_2) - storage_live(v_10) + storage_live(v_11) match self_4 { Result::Ok => { }, Result::Err => { - storage_dead(v_10) + storage_dead(v_11) storage_dead(self_4) - storage_live(_17) - _17 = AllocError { } - storage_live(_18) - _18 = Result::Err { 0: move _17 } - _0 = move _18 + storage_live(_14) + storage_live(_15) + _14 = @discriminant(_5) + _15 = copy _14 == const 1 : isize + assert(move _15 == true) else undefined_behavior + storage_live(_20) + _20 = AllocError { } + storage_live(_21) + _21 = Result::Err { 0: move _20 } + _0 = move _21 + storage_dead(_15) + storage_dead(_14) storage_dead(_3) return }, } - v_10 = move (self_4 as variant Result::Ok).0 - _3 = ControlFlow::Continue { 0: copy v_10 } - storage_dead(v_10) + v_11 = move (self_4 as variant Result::Ok).0 + _3 = ControlFlow::Continue { 0: copy v_11 } + storage_dead(v_11) storage_dead(self_4) - ptr_5 = copy (_3 as variant ControlFlow::Continue).0 + ptr_6 = copy (_3 as variant ControlFlow::Continue).0 storage_dead(_3) - storage_live(self_7) storage_live(self_8) - storage_live(_11) - _12 = transmute, *mut [u8]>(copy ptr_5) - _11 = cast<*mut [u8], *const u8>(copy _12) - self_8 = NonNull { pointer: copy _11 } - storage_dead(_11) - self_7 = cast<*mut [u8], *mut u8>(copy _12) - storage_dead(self_8) - storage_live(count_9) - count_9 = copy _12.metadata - storage_live(_16) - _16 = ub_checks - if move _16 { - storage_live(_14) - _14 = cast<*mut [u8], *const ()>(copy _12) - storage_live(_15) - _15 = copy count_9 == const 0 : usize - _13 = core::ptr::write_bytes::precondition_check(move _14, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, move _15) - storage_dead(_15) - storage_dead(_14) + storage_live(self_9) + storage_live(_12) + _13 = transmute, *mut [u8]>(copy ptr_6) + _12 = cast<*mut [u8], *const u8>(copy _13) + self_9 = NonNull { pointer: copy _12 } + storage_dead(_12) + self_8 = cast<*mut [u8], *mut u8>(copy _13) + storage_dead(self_9) + storage_live(count_10) + count_10 = copy _13.metadata + storage_live(_19) + _19 = ub_checks + if move _19 { + storage_live(_17) + _17 = cast<*mut [u8], *const ()>(copy _13) + storage_live(_18) + _18 = copy count_10 == const 0 : usize + _16 = core::ptr::write_bytes::precondition_check(move _17, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, move _18) + storage_dead(_18) + storage_dead(_17) } else { } - _6 = write_bytes[{built_in impl Sized for u8}](move self_7, const 0 : u8, move count_9) - storage_dead(count_9) - storage_dead(self_7) - _0 = Result::Ok { 0: copy ptr_5 } + _7 = write_bytes[{built_in impl Sized for u8}](move self_8, const 0 : u8, move count_10) + storage_dead(count_10) + storage_dead(self_8) + _0 = Result::Ok { 0: copy ptr_6 } return } @@ -1371,74 +1351,85 @@ where let new_layout_4: Layout; // arg #4 let _5: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local let self_6: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let new_ptr_7: NonNull<[u8]>; // local - let src_8: *const u8; // local - let dst_9: *mut u8; // local - let count_10: usize; // local - let _11: (); // anonymous local - let v_12: NonNull<[u8]>; // local - let _13: *mut [u8]; // anonymous local - let _14: (); // anonymous local - let _15: *const (); // anonymous local - let _16: *mut (); // anonymous local - let _17: bool; // anonymous local - let _18: AllocError; // anonymous local - let _19: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - - storage_live(new_ptr_7) - storage_live(_11) - storage_live(_13) - storage_live(_14) + let _7: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let new_ptr_8: NonNull<[u8]>; // local + let src_9: *const u8; // local + let dst_10: *mut u8; // local + let count_11: usize; // local + let _12: (); // anonymous local + let v_13: NonNull<[u8]>; // local + let _14: isize; // anonymous local + let _15: bool; // anonymous local + let _16: *mut [u8]; // anonymous local + let _17: (); // anonymous local + let _18: *const (); // anonymous local + let _19: *mut (); // anonymous local + let _20: bool; // anonymous local + let _21: AllocError; // anonymous local + let _22: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + + storage_live(_7) + storage_live(new_ptr_8) + storage_live(_12) + storage_live(_16) + storage_live(_17) storage_live(_5) storage_live(self_6) self_6 = @TraitClause0::allocate<'9>(copy self_1, move new_layout_4) - storage_live(v_12) + storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_12) + storage_dead(v_13) storage_dead(self_6) - storage_live(_18) - _18 = AllocError { } - storage_live(_19) - _19 = Result::Err { 0: move _18 } - _0 = move _19 + storage_live(_14) + storage_live(_15) + _14 = @discriminant(_7) + _15 = copy _14 == const 1 : isize + assert(move _15 == true) else undefined_behavior + storage_live(_21) + _21 = AllocError { } + storage_live(_22) + _22 = Result::Err { 0: move _21 } + _0 = move _22 + storage_dead(_15) + storage_dead(_14) storage_dead(_5) return }, } - v_12 = move (self_6 as variant Result::Ok).0 - _5 = ControlFlow::Continue { 0: copy v_12 } - storage_dead(v_12) + v_13 = move (self_6 as variant Result::Ok).0 + _5 = ControlFlow::Continue { 0: copy v_13 } + storage_dead(v_13) storage_dead(self_6) - new_ptr_7 = copy (_5 as variant ControlFlow::Continue).0 + new_ptr_8 = copy (_5 as variant ControlFlow::Continue).0 storage_dead(_5) - storage_live(src_8) - src_8 = transmute, *const u8>(copy ptr_2) - storage_live(dst_9) - _13 = transmute, *mut [u8]>(copy new_ptr_7) - dst_9 = cast<*mut [u8], *mut u8>(copy _13) - storage_live(count_10) - count_10 = copy (old_layout_3).size - storage_live(_17) - _17 = ub_checks - if move _17 { - storage_live(_15) - _15 = transmute, *const ()>(copy ptr_2) - storage_live(_16) - _16 = cast<*mut [u8], *mut ()>(copy _13) - _14 = core::ptr::copy_nonoverlapping::precondition_check(move _15, move _16, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_10) - storage_dead(_16) - storage_dead(_15) + storage_live(src_9) + src_9 = transmute, *const u8>(copy ptr_2) + storage_live(dst_10) + _16 = transmute, *mut [u8]>(copy new_ptr_8) + dst_10 = cast<*mut [u8], *mut u8>(copy _16) + storage_live(count_11) + count_11 = copy (old_layout_3).size + storage_live(_20) + _20 = ub_checks + if move _20 { + storage_live(_18) + _18 = transmute, *const ()>(copy ptr_2) + storage_live(_19) + _19 = cast<*mut [u8], *mut ()>(copy _16) + _17 = core::ptr::copy_nonoverlapping::precondition_check(move _18, move _19, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_11) + storage_dead(_19) + storage_dead(_18) } else { } - copy_nonoverlapping(copy src_8, copy dst_9, copy count_10) - storage_dead(count_10) - storage_dead(dst_9) - storage_dead(src_8) - _11 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) - _0 = Result::Ok { 0: copy new_ptr_7 } + copy_nonoverlapping(copy src_9, copy dst_10, copy count_11) + storage_dead(count_11) + storage_dead(dst_10) + storage_dead(src_9) + _12 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) + _0 = Result::Ok { 0: copy new_ptr_8 } return } @@ -1453,74 +1444,85 @@ where let new_layout_4: Layout; // arg #4 let _5: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local let self_6: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let new_ptr_7: NonNull<[u8]>; // local - let src_8: *const u8; // local - let dst_9: *mut u8; // local - let count_10: usize; // local - let _11: (); // anonymous local - let v_12: NonNull<[u8]>; // local - let _13: *mut [u8]; // anonymous local - let _14: (); // anonymous local - let _15: *const (); // anonymous local - let _16: *mut (); // anonymous local - let _17: bool; // anonymous local - let _18: AllocError; // anonymous local - let _19: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - - storage_live(new_ptr_7) - storage_live(_11) - storage_live(_13) - storage_live(_14) + let _7: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let new_ptr_8: NonNull<[u8]>; // local + let src_9: *const u8; // local + let dst_10: *mut u8; // local + let count_11: usize; // local + let _12: (); // anonymous local + let v_13: NonNull<[u8]>; // local + let _14: isize; // anonymous local + let _15: bool; // anonymous local + let _16: *mut [u8]; // anonymous local + let _17: (); // anonymous local + let _18: *const (); // anonymous local + let _19: *mut (); // anonymous local + let _20: bool; // anonymous local + let _21: AllocError; // anonymous local + let _22: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + + storage_live(_7) + storage_live(new_ptr_8) + storage_live(_12) + storage_live(_16) + storage_live(_17) storage_live(_5) storage_live(self_6) self_6 = @TraitClause0::allocate_zeroed<'9>(copy self_1, move new_layout_4) - storage_live(v_12) + storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_12) + storage_dead(v_13) storage_dead(self_6) - storage_live(_18) - _18 = AllocError { } - storage_live(_19) - _19 = Result::Err { 0: move _18 } - _0 = move _19 + storage_live(_14) + storage_live(_15) + _14 = @discriminant(_7) + _15 = copy _14 == const 1 : isize + assert(move _15 == true) else undefined_behavior + storage_live(_21) + _21 = AllocError { } + storage_live(_22) + _22 = Result::Err { 0: move _21 } + _0 = move _22 + storage_dead(_15) + storage_dead(_14) storage_dead(_5) return }, } - v_12 = move (self_6 as variant Result::Ok).0 - _5 = ControlFlow::Continue { 0: copy v_12 } - storage_dead(v_12) + v_13 = move (self_6 as variant Result::Ok).0 + _5 = ControlFlow::Continue { 0: copy v_13 } + storage_dead(v_13) storage_dead(self_6) - new_ptr_7 = copy (_5 as variant ControlFlow::Continue).0 + new_ptr_8 = copy (_5 as variant ControlFlow::Continue).0 storage_dead(_5) - storage_live(src_8) - src_8 = transmute, *const u8>(copy ptr_2) - storage_live(dst_9) - _13 = transmute, *mut [u8]>(copy new_ptr_7) - dst_9 = cast<*mut [u8], *mut u8>(copy _13) - storage_live(count_10) - count_10 = copy (old_layout_3).size - storage_live(_17) - _17 = ub_checks - if move _17 { - storage_live(_15) - _15 = transmute, *const ()>(copy ptr_2) - storage_live(_16) - _16 = cast<*mut [u8], *mut ()>(copy _13) - _14 = core::ptr::copy_nonoverlapping::precondition_check(move _15, move _16, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_10) - storage_dead(_16) - storage_dead(_15) + storage_live(src_9) + src_9 = transmute, *const u8>(copy ptr_2) + storage_live(dst_10) + _16 = transmute, *mut [u8]>(copy new_ptr_8) + dst_10 = cast<*mut [u8], *mut u8>(copy _16) + storage_live(count_11) + count_11 = copy (old_layout_3).size + storage_live(_20) + _20 = ub_checks + if move _20 { + storage_live(_18) + _18 = transmute, *const ()>(copy ptr_2) + storage_live(_19) + _19 = cast<*mut [u8], *mut ()>(copy _16) + _17 = core::ptr::copy_nonoverlapping::precondition_check(move _18, move _19, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_11) + storage_dead(_19) + storage_dead(_18) } else { } - copy_nonoverlapping(copy src_8, copy dst_9, copy count_10) - storage_dead(count_10) - storage_dead(dst_9) - storage_dead(src_8) - _11 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) - _0 = Result::Ok { 0: copy new_ptr_7 } + copy_nonoverlapping(copy src_9, copy dst_10, copy count_11) + storage_dead(count_11) + storage_dead(dst_10) + storage_dead(src_9) + _12 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) + _0 = Result::Ok { 0: copy new_ptr_8 } return } @@ -1535,74 +1537,85 @@ where let new_layout_4: Layout; // arg #4 let _5: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local let self_6: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let new_ptr_7: NonNull<[u8]>; // local - let src_8: *const u8; // local - let dst_9: *mut u8; // local - let count_10: usize; // local - let _11: (); // anonymous local - let v_12: NonNull<[u8]>; // local - let _13: *mut [u8]; // anonymous local - let _14: (); // anonymous local - let _15: *const (); // anonymous local - let _16: *mut (); // anonymous local - let _17: bool; // anonymous local - let _18: AllocError; // anonymous local - let _19: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - - storage_live(new_ptr_7) - storage_live(_11) - storage_live(_13) - storage_live(_14) + let _7: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let new_ptr_8: NonNull<[u8]>; // local + let src_9: *const u8; // local + let dst_10: *mut u8; // local + let count_11: usize; // local + let _12: (); // anonymous local + let v_13: NonNull<[u8]>; // local + let _14: isize; // anonymous local + let _15: bool; // anonymous local + let _16: *mut [u8]; // anonymous local + let _17: (); // anonymous local + let _18: *const (); // anonymous local + let _19: *mut (); // anonymous local + let _20: bool; // anonymous local + let _21: AllocError; // anonymous local + let _22: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + + storage_live(_7) + storage_live(new_ptr_8) + storage_live(_12) + storage_live(_16) + storage_live(_17) storage_live(_5) storage_live(self_6) self_6 = @TraitClause0::allocate<'9>(copy self_1, copy new_layout_4) - storage_live(v_12) + storage_live(v_13) match self_6 { Result::Ok => { }, Result::Err => { - storage_dead(v_12) + storage_dead(v_13) storage_dead(self_6) - storage_live(_18) - _18 = AllocError { } - storage_live(_19) - _19 = Result::Err { 0: move _18 } - _0 = move _19 + storage_live(_14) + storage_live(_15) + _14 = @discriminant(_7) + _15 = copy _14 == const 1 : isize + assert(move _15 == true) else undefined_behavior + storage_live(_21) + _21 = AllocError { } + storage_live(_22) + _22 = Result::Err { 0: move _21 } + _0 = move _22 + storage_dead(_15) + storage_dead(_14) storage_dead(_5) return }, } - v_12 = move (self_6 as variant Result::Ok).0 - _5 = ControlFlow::Continue { 0: copy v_12 } - storage_dead(v_12) + v_13 = move (self_6 as variant Result::Ok).0 + _5 = ControlFlow::Continue { 0: copy v_13 } + storage_dead(v_13) storage_dead(self_6) - new_ptr_7 = copy (_5 as variant ControlFlow::Continue).0 + new_ptr_8 = copy (_5 as variant ControlFlow::Continue).0 storage_dead(_5) - storage_live(src_8) - src_8 = transmute, *const u8>(copy ptr_2) - storage_live(dst_9) - _13 = transmute, *mut [u8]>(copy new_ptr_7) - dst_9 = cast<*mut [u8], *mut u8>(copy _13) - storage_live(count_10) - count_10 = copy (new_layout_4).size - storage_live(_17) - _17 = ub_checks - if move _17 { - storage_live(_15) - _15 = transmute, *const ()>(copy ptr_2) - storage_live(_16) - _16 = cast<*mut [u8], *mut ()>(copy _13) - _14 = core::ptr::copy_nonoverlapping::precondition_check(move _15, move _16, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_10) - storage_dead(_16) - storage_dead(_15) + storage_live(src_9) + src_9 = transmute, *const u8>(copy ptr_2) + storage_live(dst_10) + _16 = transmute, *mut [u8]>(copy new_ptr_8) + dst_10 = cast<*mut [u8], *mut u8>(copy _16) + storage_live(count_11) + count_11 = copy (new_layout_4).size + storage_live(_20) + _20 = ub_checks + if move _20 { + storage_live(_18) + _18 = transmute, *const ()>(copy ptr_2) + storage_live(_19) + _19 = cast<*mut [u8], *mut ()>(copy _16) + _17 = core::ptr::copy_nonoverlapping::precondition_check(move _18, move _19, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy count_11) + storage_dead(_19) + storage_dead(_18) } else { } - copy_nonoverlapping(copy src_8, copy dst_9, copy count_10) - storage_dead(count_10) - storage_dead(dst_9) - storage_dead(src_8) - _11 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) - _0 = Result::Ok { 0: copy new_ptr_7 } + copy_nonoverlapping(copy src_9, copy dst_10, copy count_11) + storage_dead(count_11) + storage_dead(dst_10) + storage_dead(src_9) + _12 = @TraitClause0::deallocate<'11>(move self_1, move ptr_2, move old_layout_3) + _0 = Result::Ok { 0: copy new_ptr_8 } return } @@ -1764,19 +1777,19 @@ fn core::hint::assert_unchecked::precondition_check(cond_1: bool) } // Full name: alloc::alloc::__rust_alloc -unsafe fn __rust_alloc(_1: usize, _2: usize) -> *mut u8 +unsafe fn __rust_alloc(_1: usize, _2: Alignment) -> *mut u8 = // Full name: alloc::alloc::__rust_dealloc -unsafe fn __rust_dealloc(_1: *mut u8, _2: usize, _3: usize) +unsafe fn __rust_dealloc(_1: *mut u8, _2: usize, _3: Alignment) = // Full name: alloc::alloc::__rust_realloc -unsafe fn __rust_realloc(_1: *mut u8, _2: usize, _3: usize, _4: usize) -> *mut u8 +unsafe fn __rust_realloc(_1: *mut u8, _2: usize, _3: Alignment, _4: usize) -> *mut u8 = // Full name: alloc::alloc::__rust_alloc_zeroed -unsafe fn __rust_alloc_zeroed(_1: usize, _2: usize) -> *mut u8 +unsafe fn __rust_alloc_zeroed(_1: usize, _2: Alignment) -> *mut u8 = // Full name: alloc::alloc::__rust_no_alloc_shim_is_unstable_v2 @@ -1800,187 +1813,190 @@ fn alloc_impl_runtime(layout_1: Layout, zeroed_2: bool) -> Result, let _7: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull}]; // anonymous local let self_8: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // local let self_9: Option>[{built_in impl Sized for NonNull}]; // local - let ptr_10: NonNull; // local - let _11: NonNull<[u8]>; // anonymous local - let _12: Alignment; // anonymous local - let _13: *const u8; // anonymous local - let ptr_14: *mut [u8]; // local - let data_15: *mut u8; // local - let _16: (); // anonymous local - let _17: *mut (); // anonymous local - let _18: *const [u8]; // anonymous local - let _19: (); // anonymous local - let _20: usize; // anonymous local + let _10: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let ptr_11: NonNull; // local + let _12: NonNull<[u8]>; // anonymous local + let _13: Alignment; // anonymous local + let _14: *const u8; // anonymous local + let ptr_15: *mut [u8]; // local + let data_16: *mut u8; // local + let _17: (); // anonymous local + let _18: *mut (); // anonymous local + let _19: *const [u8]; // anonymous local + let _20: (); // anonymous local let _21: Alignment; // anonymous local let _22: (); // anonymous local - let _23: usize; // anonymous local - let _24: Alignment; // anonymous local - let _25: NonNull; // anonymous local - let _26: *const u8; // anonymous local - let _27: usize; // anonymous local - let _28: (); // anonymous local - let _29: *mut (); // anonymous local + let _23: Alignment; // anonymous local + let _24: NonNull; // anonymous local + let _25: *const u8; // anonymous local + let _26: usize; // anonymous local + let _27: (); // anonymous local + let _28: *mut (); // anonymous local + let v_29: NonNull; // local let v_30: NonNull; // local - let v_31: NonNull; // local - let ptr_32: *mut [u8]; // local - let data_33: *mut u8; // local - let _34: (); // anonymous local - let _35: *mut (); // anonymous local - let _36: *const [u8]; // anonymous local + let ptr_31: *mut [u8]; // local + let data_32: *mut u8; // local + let _33: (); // anonymous local + let _34: *mut (); // anonymous local + let _35: *const [u8]; // anonymous local + let _36: isize; // anonymous local let _37: bool; // anonymous local let _38: bool; // anonymous local let _39: bool; // anonymous local - let _40: Option>[{built_in impl Sized for NonNull}]; // anonymous local - let _41: AllocError; // anonymous local - let _42: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local - let _43: AllocError; // anonymous local - let _44: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let _40: bool; // anonymous local + let _41: Option>[{built_in impl Sized for NonNull}]; // anonymous local + let _42: AllocError; // anonymous local + let _43: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local + let _44: AllocError; // anonymous local + let _45: 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(ptr_10) - storage_live(_12) - storage_live(_16) - storage_live(_19) + storage_live(_10) + storage_live(ptr_11) + storage_live(_13) + storage_live(_17) + storage_live(_20) storage_live(_22) - storage_live(_26) - storage_live(_28) - storage_live(_34) + storage_live(_25) + storage_live(_27) + storage_live(_33) size_3 = copy (layout_1).size switch copy size_3 { 0 : usize => { }, _ => { if copy zeroed_2 { - _19 = __rust_no_alloc_shim_is_unstable_v2() - storage_live(_20) + _20 = __rust_no_alloc_shim_is_unstable_v2() storage_live(_21) _21 = copy (layout_1).align - _20 = transmute(copy _21) + raw_ptr_6 = __rust_alloc_zeroed(copy size_3, move _21) storage_dead(_21) - raw_ptr_6 = __rust_alloc_zeroed(copy size_3, move _20) - storage_dead(_20) } else { _22 = __rust_no_alloc_shim_is_unstable_v2() storage_live(_23) - storage_live(_24) - _24 = copy (layout_1).align - _23 = transmute(copy _24) - storage_dead(_24) + _23 = copy (layout_1).align raw_ptr_6 = __rust_alloc(copy size_3, move _23) storage_dead(_23) } storage_live(_7) storage_live(self_8) storage_live(self_9) - _26 = cast<*mut u8, *const u8>(copy raw_ptr_6) - storage_live(_27) - _27 = transmute<*mut u8, usize>(copy raw_ptr_6) - switch copy _27 { + _25 = cast<*mut u8, *const u8>(copy raw_ptr_6) + storage_live(_26) + _26 = transmute<*mut u8, usize>(copy raw_ptr_6) + switch copy _26 { 0 : usize => { }, _ => { - storage_dead(_27) - storage_live(_25) - storage_live(_38) - _38 = ub_checks - if move _38 { - storage_live(_29) - _29 = cast<*mut u8, *mut ()>(copy raw_ptr_6) - _28 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _29) - storage_dead(_29) + storage_dead(_26) + storage_live(_24) + storage_live(_39) + _39 = ub_checks + if move _39 { + storage_live(_28) + _28 = cast<*mut u8, *mut ()>(copy raw_ptr_6) + _27 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _28) + storage_dead(_28) } else { } - _25 = NonNull { pointer: copy _26 } - self_9 = Option::Some { 0: move _25 } - storage_dead(_25) + _24 = NonNull { pointer: copy _25 } + self_9 = Option::Some { 0: move _24 } + storage_dead(_24) + storage_live(v_29) + v_29 = move (self_9 as variant Option::Some).0 + self_8 = Result::Ok { 0: copy v_29 } + storage_dead(v_29) + storage_dead(self_9) storage_live(v_30) - v_30 = move (self_9 as variant Option::Some).0 - self_8 = Result::Ok { 0: copy v_30 } + v_30 = move (self_8 as variant Result::Ok).0 + _7 = ControlFlow::Continue { 0: copy v_30 } storage_dead(v_30) - storage_dead(self_9) - storage_live(v_31) - v_31 = move (self_8 as variant Result::Ok).0 - _7 = ControlFlow::Continue { 0: copy v_31 } - storage_dead(v_31) storage_dead(self_8) - ptr_10 = copy (_7 as variant ControlFlow::Continue).0 + ptr_11 = copy (_7 as variant ControlFlow::Continue).0 storage_dead(_7) - storage_live(_11) - storage_live(ptr_32) - storage_live(data_33) - data_33 = transmute, *mut u8>(copy ptr_10) - ptr_32 = *mut (copy data_33, copy size_3) - storage_dead(data_33) - storage_live(_36) - storage_live(_39) - _39 = ub_checks - if move _39 { - storage_live(_35) - _35 = transmute, *mut ()>(copy ptr_10) - _34 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _35) - storage_dead(_35) + storage_live(_12) + storage_live(ptr_31) + storage_live(data_32) + data_32 = transmute, *mut u8>(copy ptr_11) + ptr_31 = *mut (copy data_32, copy size_3) + storage_dead(data_32) + storage_live(_35) + storage_live(_40) + _40 = ub_checks + if move _40 { + storage_live(_34) + _34 = transmute, *mut ()>(copy ptr_11) + _33 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _34) + storage_dead(_34) } else { } - _36 = cast<*mut [u8], *const [u8]>(copy ptr_32) - _11 = NonNull { pointer: copy _36 } - storage_dead(_36) - storage_dead(ptr_32) - _0 = Result::Ok { 0: move _11 } - storage_dead(_11) + _35 = cast<*mut [u8], *const [u8]>(copy ptr_31) + _12 = NonNull { pointer: copy _35 } + storage_dead(_35) + storage_dead(ptr_31) + _0 = Result::Ok { 0: move _12 } + storage_dead(_12) return }, } - storage_dead(_27) - storage_live(_40) - _40 = Option::None { } - self_9 = move _40 - storage_live(v_30) + storage_dead(_26) storage_live(_41) - _41 = AllocError { } + _41 = Option::None { } + self_9 = move _41 + storage_live(v_29) storage_live(_42) - _42 = Result::Err { 0: move _41 } - self_8 = move _42 - storage_dead(v_30) + _42 = AllocError { } + storage_live(_43) + _43 = Result::Err { 0: move _42 } + self_8 = move _43 + storage_dead(v_29) storage_dead(self_9) - storage_live(v_31) - storage_dead(v_31) + storage_live(v_30) + storage_dead(v_30) storage_dead(self_8) - storage_live(_43) - _43 = AllocError { } + storage_live(_36) + storage_live(_37) + _36 = @discriminant(_10) + _37 = copy _36 == const 1 : isize + assert(move _37 == true) else undefined_behavior storage_live(_44) - _44 = Result::Err { 0: move _43 } - _0 = move _44 + _44 = AllocError { } + storage_live(_45) + _45 = Result::Err { 0: move _44 } + _0 = move _45 + storage_dead(_37) + storage_dead(_36) storage_dead(_7) return }, } storage_live(_4) storage_live(data_5) - _12 = copy (layout_1).align - storage_live(_13) - _13 = transmute(copy _12) - data_5 = NonNull { pointer: copy _13 } - storage_dead(_13) - storage_live(ptr_14) - storage_live(data_15) - data_15 = transmute(copy _12) - ptr_14 = *mut (copy data_15, const 0 : usize) - storage_dead(data_15) - storage_live(_18) - storage_live(_37) - _37 = ub_checks - if move _37 { - storage_live(_17) - _17 = transmute(copy _12) - _16 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _17) - storage_dead(_17) + _13 = copy (layout_1).align + storage_live(_14) + _14 = transmute(copy _13) + data_5 = NonNull { pointer: copy _14 } + storage_dead(_14) + storage_live(ptr_15) + storage_live(data_16) + data_16 = transmute(copy _13) + ptr_15 = *mut (copy data_16, const 0 : usize) + storage_dead(data_16) + storage_live(_19) + storage_live(_38) + _38 = ub_checks + if move _38 { + storage_live(_18) + _18 = transmute(copy _13) + _17 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _18) + storage_dead(_18) } else { } - _18 = cast<*mut [u8], *const [u8]>(copy ptr_14) - _4 = NonNull { pointer: copy _18 } - storage_dead(_18) - storage_dead(ptr_14) + _19 = cast<*mut [u8], *const [u8]>(copy ptr_15) + _4 = NonNull { pointer: copy _19 } + storage_dead(_19) + storage_dead(ptr_15) storage_dead(data_5) _0 = Result::Ok { 0: move _4 } storage_dead(_4) @@ -2007,259 +2023,283 @@ fn grow_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_3: let _14: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull}]; // anonymous local let self_15: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // local let self_16: Option>[{built_in impl Sized for NonNull}]; // local - let ptr_17: NonNull; // local - let _18: (); // anonymous local - let self_19: *mut u8; // local - let count_20: usize; // local - let _21: NonNull<[u8]>; // anonymous local - let _22: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local - let self_23: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let new_ptr_24: NonNull<[u8]>; // local - let src_25: *const u8; // local - let ptr_26: *mut u8; // local - let dst_27: *mut u8; // local - let _28: (); // anonymous local - let _29: Alignment; // anonymous local - let _30: Alignment; // anonymous local - let _31: (); // anonymous local - let _32: NonNull; // anonymous local - let _33: *const u8; // anonymous local - let _34: usize; // anonymous local - let _35: (); // anonymous local - let _36: *mut (); // anonymous local - let v_37: NonNull; // local - let v_38: NonNull; // local - let _39: (); // anonymous local - let _40: *const (); // anonymous local - let _41: bool; // anonymous local - let ptr_42: *mut [u8]; // local - let data_43: *mut u8; // local - let _44: (); // anonymous local - let _45: *mut (); // anonymous local - let _46: *const [u8]; // anonymous local - let v_47: NonNull<[u8]>; // local - let _48: *mut [u8]; // anonymous local - let _49: (); // anonymous local - let _50: *const (); // anonymous local - let _51: *mut (); // anonymous local - let _52: bool; // anonymous local + let _17: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let ptr_18: NonNull; // local + let _19: (); // anonymous local + let self_20: *mut u8; // local + let count_21: usize; // local + let _22: NonNull<[u8]>; // anonymous local + let _23: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local + let self_24: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local + let _25: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let new_ptr_26: NonNull<[u8]>; // local + let src_27: *const u8; // local + let ptr_28: *mut u8; // local + let dst_29: *mut u8; // local + let _30: (); // anonymous local + let _31: Alignment; // anonymous local + let _32: Alignment; // anonymous local + let _33: (); // anonymous local + let _34: NonNull; // anonymous local + let _35: *const u8; // anonymous local + let _36: usize; // anonymous local + let _37: (); // anonymous local + let _38: *mut (); // anonymous local + let v_39: NonNull; // local + let v_40: NonNull; // local + let _41: isize; // anonymous local + let _42: bool; // anonymous local + let _43: (); // anonymous local + let _44: *const (); // anonymous local + let _45: bool; // anonymous local + let ptr_46: *mut [u8]; // local + let data_47: *mut u8; // local + let _48: (); // anonymous local + let _49: *mut (); // anonymous local + let _50: *const [u8]; // anonymous local + let v_51: NonNull<[u8]>; // local + let _52: isize; // anonymous local let _53: bool; // anonymous local - let _54: bool; // anonymous local - let _55: bool; // anonymous local - let _56: bool; // anonymous local - let _57: AllocError; // anonymous local - let _58: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - let _59: Option>[{built_in impl Sized for NonNull}]; // anonymous local - let _60: AllocError; // anonymous local - let _61: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local - let _62: AllocError; // anonymous local - let _63: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let _54: *mut [u8]; // anonymous local + let _55: (); // anonymous local + let _56: *const (); // anonymous local + let _57: *mut (); // anonymous local + let _58: bool; // anonymous local + let _59: bool; // anonymous local + let _60: bool; // anonymous local + let _61: bool; // anonymous local + let _62: bool; // anonymous local + let _63: AllocError; // anonymous local + let _64: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let _65: Option>[{built_in impl Sized for NonNull}]; // anonymous local + let _66: AllocError; // anonymous local + let _67: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local + let _68: AllocError; // anonymous local + let _69: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local storage_live(old_size_6) - storage_live(_8) storage_live(new_size_10) storage_live(raw_ptr_12) - storage_live(ptr_17) - storage_live(_18) - storage_live(new_ptr_24) - storage_live(ptr_26) - storage_live(_28) - storage_live(_29) + storage_live(_17) + storage_live(ptr_18) + storage_live(_19) + storage_live(_25) + storage_live(new_ptr_26) + storage_live(ptr_28) + storage_live(_30) storage_live(_31) storage_live(_33) storage_live(_35) - storage_live(_39) - storage_live(_44) + storage_live(_37) + storage_live(_43) storage_live(_48) - storage_live(_49) + storage_live(_54) + storage_live(_55) old_size_6 = copy (old_layout_3).size switch copy old_size_6 { 0 : usize => { }, _ => { storage_live(_7) - _29 = copy (old_layout_3).align - _8 = transmute(copy _29) + storage_live(_8) + _31 = copy (old_layout_3).align + _8 = transmute(copy _31) storage_live(_9) - storage_live(_30) - _30 = copy (new_layout_4).align - _9 = transmute(copy _30) - storage_dead(_30) - _7 = copy _8 == move _9 + storage_live(_32) + _32 = copy (new_layout_4).align + _9 = transmute(copy _32) + storage_dead(_32) + _7 = move _8 == move _9 if move _7 { } else { storage_dead(_9) + storage_dead(_8) storage_dead(_7) - 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 { + storage_live(_23) + storage_live(self_24) + self_24 = alloc_impl_runtime(move new_layout_4, move zeroed_5) + storage_live(v_51) + match self_24 { Result::Ok => { }, Result::Err => { - storage_dead(v_47) - storage_dead(self_23) - storage_live(_57) - _57 = AllocError { } - storage_live(_58) - _58 = Result::Err { 0: move _57 } - _0 = move _58 - storage_dead(_22) + storage_dead(v_51) + storage_dead(self_24) + storage_live(_52) + storage_live(_53) + _52 = @discriminant(_25) + _53 = copy _52 == const 1 : isize + assert(move _53 == true) else undefined_behavior + storage_live(_63) + _63 = AllocError { } + storage_live(_64) + _64 = Result::Err { 0: move _63 } + _0 = move _64 + storage_dead(_53) + storage_dead(_52) + storage_dead(_23) return }, } - v_47 = move (self_23 as variant Result::Ok).0 - _22 = ControlFlow::Continue { 0: copy v_47 } - storage_dead(v_47) - storage_dead(self_23) - new_ptr_24 = copy (_22 as variant ControlFlow::Continue).0 - storage_dead(_22) - storage_live(src_25) - ptr_26 = transmute, *mut u8>(copy ptr_2) - src_25 = transmute, *const u8>(copy ptr_2) - storage_live(dst_27) - _48 = transmute, *mut [u8]>(copy new_ptr_24) - dst_27 = cast<*mut [u8], *mut u8>(copy _48) - storage_live(_53) - _53 = ub_checks - if move _53 { - storage_live(_50) - _50 = transmute, *const ()>(copy ptr_2) - storage_live(_51) - _51 = cast<*mut [u8], *mut ()>(copy _48) - _49 = core::ptr::copy_nonoverlapping::precondition_check(move _50, move _51, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy old_size_6) - storage_dead(_51) - storage_dead(_50) + v_51 = move (self_24 as variant Result::Ok).0 + _23 = ControlFlow::Continue { 0: copy v_51 } + storage_dead(v_51) + storage_dead(self_24) + new_ptr_26 = copy (_23 as variant ControlFlow::Continue).0 + storage_dead(_23) + storage_live(src_27) + ptr_28 = transmute, *mut u8>(copy ptr_2) + src_27 = transmute, *const u8>(copy ptr_2) + storage_live(dst_29) + _54 = transmute, *mut [u8]>(copy new_ptr_26) + dst_29 = cast<*mut [u8], *mut u8>(copy _54) + storage_live(_59) + _59 = ub_checks + if move _59 { + storage_live(_56) + _56 = transmute, *const ()>(copy ptr_2) + storage_live(_57) + _57 = cast<*mut [u8], *mut ()>(copy _54) + _55 = core::ptr::copy_nonoverlapping::precondition_check(move _56, move _57, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy old_size_6) + storage_dead(_57) + storage_dead(_56) } else { } - copy_nonoverlapping(copy src_25, copy dst_27, copy old_size_6) - storage_dead(dst_27) - storage_dead(src_25) - _28 = __rust_dealloc(move ptr_26, move old_size_6, move _8) - _0 = Result::Ok { 0: copy new_ptr_24 } + copy_nonoverlapping(copy src_27, copy dst_29, copy old_size_6) + storage_dead(dst_29) + storage_dead(src_27) + _30 = __rust_dealloc(move ptr_28, move old_size_6, move _31) + _0 = Result::Ok { 0: copy new_ptr_26 } 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(_52) - _52 = ub_checks - if move _52 { - _31 = core::hint::assert_unchecked::precondition_check(copy cond_11) + storage_live(_58) + _58 = ub_checks + if move _58 { + _33 = core::hint::assert_unchecked::precondition_check(copy cond_11) } else { } assert(copy cond_11 == true) else undefined_behavior storage_dead(cond_11) storage_live(ptr_13) ptr_13 = transmute, *mut u8>(copy ptr_2) - raw_ptr_12 = __rust_realloc(move ptr_13, copy old_size_6, move _8, copy new_size_10) + raw_ptr_12 = __rust_realloc(move ptr_13, copy old_size_6, move _31, copy new_size_10) storage_dead(ptr_13) storage_live(_14) storage_live(self_15) storage_live(self_16) - _33 = cast<*mut u8, *const u8>(copy raw_ptr_12) - storage_live(_34) - _34 = transmute<*mut u8, usize>(copy raw_ptr_12) - switch copy _34 { + _35 = cast<*mut u8, *const u8>(copy raw_ptr_12) + storage_live(_36) + _36 = transmute<*mut u8, usize>(copy raw_ptr_12) + switch copy _36 { 0 : usize => { }, _ => { - storage_dead(_34) - storage_live(_32) - storage_live(_54) - _54 = ub_checks - if move _54 { - storage_live(_36) - _36 = cast<*mut u8, *mut ()>(copy raw_ptr_12) - _35 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _36) - storage_dead(_36) + storage_dead(_36) + storage_live(_34) + storage_live(_60) + _60 = ub_checks + if move _60 { + storage_live(_38) + _38 = cast<*mut u8, *mut ()>(copy raw_ptr_12) + _37 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _38) + storage_dead(_38) } else { } - _32 = NonNull { pointer: copy _33 } - self_16 = Option::Some { 0: move _32 } - storage_dead(_32) - storage_live(v_37) - v_37 = move (self_16 as variant Option::Some).0 - self_15 = Result::Ok { 0: copy v_37 } - storage_dead(v_37) + _34 = NonNull { pointer: copy _35 } + self_16 = Option::Some { 0: move _34 } + storage_dead(_34) + storage_live(v_39) + v_39 = move (self_16 as variant Option::Some).0 + self_15 = Result::Ok { 0: copy v_39 } + storage_dead(v_39) storage_dead(self_16) - storage_live(v_38) - v_38 = move (self_15 as variant Result::Ok).0 - _14 = ControlFlow::Continue { 0: copy v_38 } - storage_dead(v_38) + storage_live(v_40) + v_40 = move (self_15 as variant Result::Ok).0 + _14 = ControlFlow::Continue { 0: copy v_40 } + storage_dead(v_40) storage_dead(self_15) - ptr_17 = copy (_14 as variant ControlFlow::Continue).0 + ptr_18 = copy (_14 as variant ControlFlow::Continue).0 storage_dead(_14) 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(_55) - _55 = ub_checks - if move _55 { - storage_live(_40) - _40 = cast<*mut u8, *const ()>(copy self_19) - storage_live(_41) - _41 = copy count_20 == const 0 : usize - _39 = core::ptr::write_bytes::precondition_check(move _40, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, move _41) - storage_dead(_41) - storage_dead(_40) + storage_live(self_20) + self_20 = copy raw_ptr_12 offset copy old_size_6 + storage_live(count_21) + count_21 = copy new_size_10 wrap.- copy old_size_6 + storage_live(_61) + _61 = ub_checks + if move _61 { + storage_live(_44) + _44 = cast<*mut u8, *const ()>(copy self_20) + storage_live(_45) + _45 = copy count_21 == const 0 : usize + _43 = core::ptr::write_bytes::precondition_check(move _44, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, move _45) + storage_dead(_45) + storage_dead(_44) } 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) + _19 = write_bytes[{built_in impl Sized for u8}](move self_20, const 0 : u8, move count_21) + storage_dead(count_21) + storage_dead(self_20) } else { } - storage_live(_21) - storage_live(ptr_42) - storage_live(data_43) - data_43 = transmute, *mut u8>(copy ptr_17) - ptr_42 = *mut (copy data_43, copy new_size_10) - storage_dead(data_43) - storage_live(_46) - storage_live(_56) - _56 = ub_checks - if move _56 { - storage_live(_45) - _45 = transmute, *mut ()>(copy ptr_17) - _44 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _45) - storage_dead(_45) + storage_live(_22) + storage_live(ptr_46) + storage_live(data_47) + data_47 = transmute, *mut u8>(copy ptr_18) + ptr_46 = *mut (copy data_47, copy new_size_10) + storage_dead(data_47) + storage_live(_50) + storage_live(_62) + _62 = ub_checks + if move _62 { + storage_live(_49) + _49 = transmute, *mut ()>(copy ptr_18) + _48 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _49) + storage_dead(_49) } else { } - _46 = cast<*mut [u8], *const [u8]>(copy ptr_42) - _21 = NonNull { pointer: copy _46 } - storage_dead(_46) - storage_dead(ptr_42) - _0 = Result::Ok { 0: move _21 } - storage_dead(_21) + _50 = cast<*mut [u8], *const [u8]>(copy ptr_46) + _22 = NonNull { pointer: copy _50 } + storage_dead(_50) + storage_dead(ptr_46) + _0 = Result::Ok { 0: move _22 } + storage_dead(_22) return }, } - storage_dead(_34) - storage_live(_59) - _59 = Option::None { } - self_16 = move _59 - storage_live(v_37) - storage_live(_60) - _60 = AllocError { } - storage_live(_61) - _61 = Result::Err { 0: move _60 } - self_15 = move _61 - storage_dead(v_37) + storage_dead(_36) + storage_live(_65) + _65 = Option::None { } + self_16 = move _65 + storage_live(v_39) + storage_live(_66) + _66 = AllocError { } + storage_live(_67) + _67 = Result::Err { 0: move _66 } + self_15 = move _67 + storage_dead(v_39) storage_dead(self_16) - storage_live(v_38) - storage_dead(v_38) + storage_live(v_40) + storage_dead(v_40) storage_dead(self_15) - storage_live(_62) - _62 = AllocError { } - storage_live(_63) - _63 = Result::Err { 0: move _62 } - _0 = move _63 + storage_live(_41) + storage_live(_42) + _41 = @discriminant(_17) + _42 = copy _41 == const 1 : isize + assert(move _42 == true) else undefined_behavior + storage_live(_68) + _68 = AllocError { } + storage_live(_69) + _69 = Result::Err { 0: move _68 } + _0 = move _69 + storage_dead(_42) + storage_dead(_41) storage_dead(_14) return }, @@ -2291,302 +2331,322 @@ fn shrink_impl_runtime<'_0>(self_1: &'_0 Global, ptr_2: NonNull, old_layout_ let _17: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull}]; // anonymous local let self_18: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // local let self_19: Option>[{built_in impl Sized for NonNull}]; // local - let ptr_20: NonNull; // local - let _21: NonNull<[u8]>; // anonymous local - let _22: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local - let self_23: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local - let new_ptr_24: NonNull<[u8]>; // local - let src_25: *const u8; // local - let ptr_26: *mut u8; // local - let dst_27: *mut u8; // local - let _28: (); // anonymous local - let _29: Alignment; // anonymous local - let _30: usize; // anonymous local - let ptr_31: *mut u8; // local + let _20: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let ptr_21: NonNull; // local + let _22: NonNull<[u8]>; // anonymous local + let _23: ControlFlow[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}], NonNull<[u8]>>[{built_in impl Sized for Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]}, {built_in impl Sized for NonNull<[u8]>}]; // anonymous local + let self_24: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // local + let _25: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let new_ptr_26: NonNull<[u8]>; // local + let src_27: *const u8; // local + let ptr_28: *mut u8; // local + let dst_29: *mut u8; // local + let _30: (); // anonymous local + let _31: Alignment; // anonymous local let _32: usize; // anonymous local - let _33: Alignment; // anonymous local + let ptr_33: *mut u8; // local let _34: Alignment; // anonymous local - let _35: *const u8; // anonymous local - let ptr_36: *mut [u8]; // local - let data_37: *mut u8; // local - let _38: (); // anonymous local - let _39: *mut (); // anonymous local - let _40: *const [u8]; // anonymous local - let _41: Alignment; // anonymous local - let _42: (); // anonymous local - let _43: NonNull; // anonymous local - let _44: *const u8; // anonymous local - let _45: usize; // anonymous local - let _46: (); // anonymous local - let _47: *mut (); // anonymous local - let v_48: NonNull; // local + let _35: Alignment; // anonymous local + let _36: *const u8; // anonymous local + let ptr_37: *mut [u8]; // local + let data_38: *mut u8; // local + let _39: (); // anonymous local + let _40: *mut (); // anonymous local + let _41: *const [u8]; // anonymous local + let _42: Alignment; // anonymous local + let _43: (); // anonymous local + let _44: NonNull; // anonymous local + let _45: *const u8; // anonymous local + let _46: usize; // anonymous local + let _47: (); // anonymous local + let _48: *mut (); // anonymous local let v_49: NonNull; // local - let ptr_50: *mut [u8]; // local - let data_51: *mut u8; // local - let _52: (); // anonymous local - let _53: *mut (); // anonymous local - let _54: *const [u8]; // anonymous local - let v_55: NonNull<[u8]>; // local - let _56: *mut [u8]; // anonymous local - let _57: (); // anonymous local - let _58: *const (); // anonymous local - let _59: *mut (); // anonymous local - let _60: usize; // anonymous local - let _61: bool; // anonymous local - let _62: bool; // anonymous local - let _63: bool; // anonymous local - let _64: bool; // anonymous local - let _65: bool; // anonymous local - let _66: AllocError; // anonymous local - let _67: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - let _68: Option>[{built_in impl Sized for NonNull}]; // anonymous local - let _69: AllocError; // anonymous local - let _70: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local + let v_50: NonNull; // local + let ptr_51: *mut [u8]; // local + let data_52: *mut u8; // local + let _53: (); // anonymous local + let _54: *mut (); // anonymous local + let _55: *const [u8]; // anonymous local + let _56: isize; // anonymous local + let _57: bool; // anonymous local + let v_58: NonNull<[u8]>; // local + let _59: isize; // anonymous local + let _60: bool; // anonymous local + let _61: *mut [u8]; // anonymous local + let _62: (); // anonymous local + let _63: *const (); // anonymous local + let _64: *mut (); // anonymous local + let _65: usize; // anonymous local + let _66: bool; // anonymous local + let _67: bool; // anonymous local + let _68: bool; // anonymous local + let _69: bool; // anonymous local + let _70: bool; // anonymous local let _71: AllocError; // anonymous local let _72: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let _73: Option>[{built_in impl Sized for NonNull}]; // anonymous local + let _74: AllocError; // anonymous local + let _75: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local + let _76: AllocError; // anonymous local + let _77: 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(_11) storage_live(_14) storage_live(raw_ptr_15) - storage_live(ptr_20) - storage_live(new_ptr_24) - storage_live(ptr_26) - storage_live(_28) - storage_live(_29) - storage_live(_34) - storage_live(_38) - storage_live(_42) - storage_live(_44) - storage_live(_46) - storage_live(_52) - storage_live(_56) - storage_live(_57) + storage_live(_20) + storage_live(ptr_21) + storage_live(_25) + storage_live(new_ptr_26) + storage_live(ptr_28) + storage_live(_30) + storage_live(_31) + storage_live(_35) + storage_live(_39) + storage_live(_43) + storage_live(_45) + storage_live(_47) + storage_live(_53) + storage_live(_61) + storage_live(_62) new_size_6 = copy (new_layout_4).size switch copy new_size_6 { 0 : usize => { }, _ => { storage_live(_10) - _29 = copy (old_layout_3).align - _11 = transmute(copy _29) + storage_live(_11) + _31 = copy (old_layout_3).align + _11 = transmute(copy _31) storage_live(_12) - storage_live(_41) - _41 = copy (new_layout_4).align - _12 = transmute(copy _41) - storage_dead(_41) - _10 = copy _11 == move _12 + storage_live(_42) + _42 = copy (new_layout_4).align + _12 = transmute(copy _42) + storage_dead(_42) + _10 = move _11 == move _12 if move _10 { } else { storage_dead(_12) + storage_dead(_11) storage_dead(_10) - storage_live(_22) - storage_live(self_23) - self_23 = alloc_impl_runtime(move new_layout_4, const false) - storage_live(v_55) - match self_23 { + storage_live(_23) + storage_live(self_24) + self_24 = alloc_impl_runtime(move new_layout_4, const false) + storage_live(v_58) + match self_24 { Result::Ok => { }, Result::Err => { - storage_dead(v_55) - storage_dead(self_23) - storage_live(_66) - _66 = AllocError { } - storage_live(_67) - _67 = Result::Err { 0: move _66 } - _0 = move _67 - storage_dead(_22) + storage_dead(v_58) + storage_dead(self_24) + storage_live(_59) + storage_live(_60) + _59 = @discriminant(_25) + _60 = copy _59 == const 1 : isize + assert(move _60 == true) else undefined_behavior + storage_live(_71) + _71 = AllocError { } + storage_live(_72) + _72 = Result::Err { 0: move _71 } + _0 = move _72 + storage_dead(_60) + storage_dead(_59) + storage_dead(_23) return }, } - v_55 = move (self_23 as variant Result::Ok).0 - _22 = ControlFlow::Continue { 0: copy v_55 } - storage_dead(v_55) - storage_dead(self_23) - new_ptr_24 = copy (_22 as variant ControlFlow::Continue).0 - storage_dead(_22) - storage_live(src_25) - ptr_26 = transmute, *mut u8>(copy ptr_2) - src_25 = transmute, *const u8>(copy ptr_2) - storage_live(dst_27) - _56 = transmute, *mut [u8]>(copy new_ptr_24) - dst_27 = cast<*mut [u8], *mut u8>(copy _56) - storage_live(_63) - _63 = ub_checks - if move _63 { - storage_live(_58) - _58 = transmute, *const ()>(copy ptr_2) - storage_live(_59) - _59 = cast<*mut [u8], *mut ()>(copy _56) - _57 = core::ptr::copy_nonoverlapping::precondition_check(move _58, move _59, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy new_size_6) - storage_dead(_59) - storage_dead(_58) + v_58 = move (self_24 as variant Result::Ok).0 + _23 = ControlFlow::Continue { 0: copy v_58 } + storage_dead(v_58) + storage_dead(self_24) + new_ptr_26 = copy (_23 as variant ControlFlow::Continue).0 + storage_dead(_23) + storage_live(src_27) + ptr_28 = transmute, *mut u8>(copy ptr_2) + src_27 = transmute, *const u8>(copy ptr_2) + storage_live(dst_29) + _61 = transmute, *mut [u8]>(copy new_ptr_26) + dst_29 = cast<*mut [u8], *mut u8>(copy _61) + storage_live(_68) + _68 = ub_checks + if move _68 { + storage_live(_63) + _63 = transmute, *const ()>(copy ptr_2) + storage_live(_64) + _64 = cast<*mut [u8], *mut ()>(copy _61) + _62 = core::ptr::copy_nonoverlapping::precondition_check(move _63, move _64, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::SIZE, const {impl SizedTypeProperties for T}[{built_in impl Sized for u8}]::ALIGN, copy new_size_6) + storage_dead(_64) + storage_dead(_63) } else { } - copy_nonoverlapping(copy src_25, copy dst_27, copy new_size_6) - storage_dead(dst_27) - storage_dead(src_25) - storage_live(_60) - _60 = copy (old_layout_3).size - switch copy _60 { + copy_nonoverlapping(copy src_27, copy dst_29, copy new_size_6) + storage_dead(dst_29) + storage_dead(src_27) + storage_live(_65) + _65 = copy (old_layout_3).size + switch copy _65 { 0 : usize => { }, _ => { - _28 = __rust_dealloc(move ptr_26, move _60, move _11) + _30 = __rust_dealloc(move ptr_28, move _65, move _31) }, } - storage_dead(_60) - _0 = Result::Ok { 0: copy new_ptr_24 } + storage_dead(_65) + _0 = Result::Ok { 0: copy new_ptr_26 } 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 { - _42 = core::hint::assert_unchecked::precondition_check(copy cond_13) + storage_live(_67) + _67 = ub_checks + if move _67 { + _43 = core::hint::assert_unchecked::precondition_check(copy cond_13) } else { } assert(copy cond_13 == true) else undefined_behavior storage_dead(cond_13) storage_live(ptr_16) ptr_16 = transmute, *mut u8>(copy ptr_2) - raw_ptr_15 = __rust_realloc(move ptr_16, move _14, move _11, copy new_size_6) + raw_ptr_15 = __rust_realloc(move ptr_16, move _14, move _31, copy new_size_6) storage_dead(ptr_16) storage_live(_17) storage_live(self_18) storage_live(self_19) - _44 = cast<*mut u8, *const u8>(copy raw_ptr_15) - storage_live(_45) - _45 = transmute<*mut u8, usize>(copy raw_ptr_15) - switch copy _45 { + _45 = cast<*mut u8, *const u8>(copy raw_ptr_15) + storage_live(_46) + _46 = transmute<*mut u8, usize>(copy raw_ptr_15) + switch copy _46 { 0 : usize => { }, _ => { - storage_dead(_45) - storage_live(_43) - storage_live(_64) - _64 = ub_checks - if move _64 { - storage_live(_47) - _47 = cast<*mut u8, *mut ()>(copy raw_ptr_15) - _46 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _47) - storage_dead(_47) + storage_dead(_46) + storage_live(_44) + storage_live(_69) + _69 = ub_checks + if move _69 { + storage_live(_48) + _48 = cast<*mut u8, *mut ()>(copy raw_ptr_15) + _47 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _48) + storage_dead(_48) } else { } - _43 = NonNull { pointer: copy _44 } - self_19 = Option::Some { 0: move _43 } - storage_dead(_43) - storage_live(v_48) - v_48 = move (self_19 as variant Option::Some).0 - self_18 = Result::Ok { 0: copy v_48 } - storage_dead(v_48) - storage_dead(self_19) + _44 = NonNull { pointer: copy _45 } + self_19 = Option::Some { 0: move _44 } + storage_dead(_44) storage_live(v_49) - v_49 = move (self_18 as variant Result::Ok).0 - _17 = ControlFlow::Continue { 0: copy v_49 } + v_49 = move (self_19 as variant Option::Some).0 + self_18 = Result::Ok { 0: copy v_49 } storage_dead(v_49) + storage_dead(self_19) + storage_live(v_50) + v_50 = move (self_18 as variant Result::Ok).0 + _17 = ControlFlow::Continue { 0: copy v_50 } + storage_dead(v_50) storage_dead(self_18) - ptr_20 = copy (_17 as variant ControlFlow::Continue).0 + ptr_21 = copy (_17 as variant ControlFlow::Continue).0 storage_dead(_17) - storage_live(_21) - storage_live(ptr_50) - storage_live(data_51) - data_51 = transmute, *mut u8>(copy ptr_20) - ptr_50 = *mut (copy data_51, copy new_size_6) - storage_dead(data_51) - storage_live(_54) - storage_live(_65) - _65 = ub_checks - if move _65 { - storage_live(_53) - _53 = transmute, *mut ()>(copy ptr_20) - _52 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _53) - storage_dead(_53) + storage_live(_22) + storage_live(ptr_51) + storage_live(data_52) + data_52 = transmute, *mut u8>(copy ptr_21) + ptr_51 = *mut (copy data_52, copy new_size_6) + storage_dead(data_52) + storage_live(_55) + storage_live(_70) + _70 = ub_checks + if move _70 { + storage_live(_54) + _54 = transmute, *mut ()>(copy ptr_21) + _53 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _54) + storage_dead(_54) } else { } - _54 = cast<*mut [u8], *const [u8]>(copy ptr_50) - _21 = NonNull { pointer: copy _54 } - storage_dead(_54) - storage_dead(ptr_50) - _0 = Result::Ok { 0: move _21 } - storage_dead(_21) + _55 = cast<*mut [u8], *const [u8]>(copy ptr_51) + _22 = NonNull { pointer: copy _55 } + storage_dead(_55) + storage_dead(ptr_51) + _0 = Result::Ok { 0: move _22 } + storage_dead(_22) return }, } - storage_dead(_45) - storage_live(_68) - _68 = Option::None { } - self_19 = move _68 - storage_live(v_48) - storage_live(_69) - _69 = AllocError { } - storage_live(_70) - _70 = Result::Err { 0: move _69 } - self_18 = move _70 - storage_dead(v_48) - storage_dead(self_19) + storage_dead(_46) + storage_live(_73) + _73 = Option::None { } + self_19 = move _73 storage_live(v_49) + storage_live(_74) + _74 = AllocError { } + storage_live(_75) + _75 = Result::Err { 0: move _74 } + self_18 = move _75 storage_dead(v_49) + storage_dead(self_19) + storage_live(v_50) + storage_dead(v_50) storage_dead(self_18) - storage_live(_71) - _71 = AllocError { } - storage_live(_72) - _72 = Result::Err { 0: move _71 } - _0 = move _72 + storage_live(_56) + storage_live(_57) + _56 = @discriminant(_20) + _57 = copy _56 == const 1 : isize + assert(move _57 == true) else undefined_behavior + storage_live(_76) + _76 = AllocError { } + storage_live(_77) + _77 = Result::Err { 0: move _76 } + _0 = move _77 + storage_dead(_57) + storage_dead(_56) storage_dead(_17) return }, } - storage_live(_30) - _30 = copy (old_layout_3).size - switch copy _30 { + storage_live(_32) + _32 = copy (old_layout_3).size + switch copy _32 { 0 : usize => { }, _ => { - storage_live(ptr_31) - ptr_31 = transmute, *mut u8>(copy ptr_2) - storage_live(_32) - storage_live(_33) - _33 = copy (old_layout_3).align - _32 = transmute(copy _33) - storage_dead(_33) - _7 = __rust_dealloc(move ptr_31, move _30, move _32) - storage_dead(_32) - storage_dead(ptr_31) + storage_live(ptr_33) + ptr_33 = transmute, *mut u8>(copy ptr_2) + storage_live(_34) + _34 = copy (old_layout_3).align + _7 = __rust_dealloc(move ptr_33, move _32, move _34) + storage_dead(_34) + storage_dead(ptr_33) }, } - storage_dead(_30) + storage_dead(_32) storage_live(_8) storage_live(data_9) - _34 = copy (new_layout_4).align - storage_live(_35) - _35 = transmute(copy _34) - data_9 = NonNull { pointer: copy _35 } - storage_dead(_35) - storage_live(ptr_36) - storage_live(data_37) - data_37 = transmute(copy _34) - ptr_36 = *mut (copy data_37, const 0 : usize) - storage_dead(data_37) - storage_live(_40) - storage_live(_61) - _61 = ub_checks - if move _61 { - storage_live(_39) - _39 = transmute(copy _34) - _38 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _39) - storage_dead(_39) + _35 = copy (new_layout_4).align + storage_live(_36) + _36 = transmute(copy _35) + data_9 = NonNull { pointer: copy _36 } + storage_dead(_36) + storage_live(ptr_37) + storage_live(data_38) + data_38 = transmute(copy _35) + ptr_37 = *mut (copy data_38, const 0 : usize) + storage_dead(data_38) + storage_live(_41) + storage_live(_66) + _66 = ub_checks + if move _66 { + storage_live(_40) + _40 = transmute(copy _35) + _39 = core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move _40) + storage_dead(_40) } else { } - _40 = cast<*mut [u8], *const [u8]>(copy ptr_36) - _8 = NonNull { pointer: copy _40 } - storage_dead(_40) - storage_dead(ptr_36) + _41 = cast<*mut [u8], *const [u8]>(copy ptr_37) + _8 = NonNull { pointer: copy _41 } + storage_dead(_41) + storage_dead(ptr_37) storage_dead(data_9) _0 = Result::Ok { 0: move _8 } storage_dead(_8) @@ -2641,8 +2701,7 @@ pub unsafe fn {impl Allocator for Global}::deallocate<'_0>(self_1: &'_0 Global, let layout_3: Layout; // arg #3 let _4: usize; // anonymous local let ptr_5: *mut u8; // local - let _6: usize; // anonymous local - let _7: Alignment; // anonymous local + let _6: Alignment; // anonymous local _0 = () storage_live(_4) @@ -2654,10 +2713,7 @@ pub unsafe fn {impl Allocator for Global}::deallocate<'_0>(self_1: &'_0 Global, storage_live(ptr_5) ptr_5 = transmute, *mut u8>(copy ptr_2) storage_live(_6) - storage_live(_7) - _7 = copy (layout_3).align - _6 = transmute(copy _7) - storage_dead(_7) + _6 = copy (layout_3).align _0 = __rust_dealloc(move ptr_5, move _4, move _6) storage_dead(_6) storage_dead(ptr_5) @@ -2742,54 +2798,6 @@ pub fn handle_alloc_error(layout_1: Layout) -> ! _0 = ct_error(move _2.0) } -// Full name: alloc::alloc::exchange_malloc -#[lang_item("exchange_malloc")] -unsafe fn exchange_malloc(size_1: usize, align_2: usize) -> *mut u8 -{ - let _0: *mut u8; // return - let size_1: usize; // arg #1 - let align_2: usize; // arg #2 - let layout_3: Layout; // local - let _4: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local - let ptr_5: NonNull<[u8]>; // local - let _6: !; // anonymous local - let _7: (); // anonymous local - let _8: Alignment; // anonymous local - let _9: *mut [u8]; // anonymous local - let _10: bool; // anonymous local - - storage_live(layout_3) - storage_live(ptr_5) - storage_live(_6) - storage_live(_7) - storage_live(_10) - _10 = ub_checks - if move _10 { - _7 = core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(copy size_1, copy align_2) - } else { - } - storage_live(_8) - _8 = transmute(copy align_2) - layout_3 = Layout { size: copy size_1, align: move _8 } - storage_dead(_8) - storage_live(_4) - _4 = alloc_impl_runtime(copy layout_3, const false) - match _4 { - Result::Ok => { - }, - Result::Err => { - _6 = handle_alloc_error(move layout_3) - }, - } - ptr_5 = copy (_4 as variant Result::Ok).0 - storage_live(_9) - _9 = transmute, *mut [u8]>(copy ptr_5) - _0 = cast<*mut [u8], *mut u8>(copy _9) - storage_dead(_9) - storage_dead(_4) - return -} - // Full name: alloc::boxed::Box #[lang_item("owned_box")] pub struct Box @@ -2817,27 +2825,57 @@ where { let _0: Box[@TraitClause0::parent_clause0, {built_in impl Sized for Global}, {impl Allocator for Global}]; // return let x_1: T; // arg #1 - let _2: *mut u8; // anonymous local - let _3: *const T; // anonymous local - let _4: NonNull; // anonymous local - let _5: Unique; // anonymous local - let _6: PhantomData; // anonymous local - let _7: Global; // anonymous local + let ptr_2: *mut T; // local + let size_3: usize; // local + let align_4: usize; // local + let layout_5: Layout; // local + let _6: Result, AllocError>[{built_in impl Sized for NonNull<[u8]>}, {built_in impl Sized for AllocError}]; // anonymous local + let ptr_7: NonNull<[u8]>; // local + let _8: !; // anonymous local + let _9: (); // anonymous local + let _10: Alignment; // anonymous local + let _11: *mut [u8]; // anonymous local + let _12: bool; // anonymous local - storage_live(_2) - storage_live(_3) - storage_live(_4) - storage_live(_5) - _2 = exchange_malloc(const {impl SizedTypeProperties for T}[@TraitClause0]::SIZE, const {impl SizedTypeProperties for T}[@TraitClause0]::ALIGN) - _3 = cast<*mut u8, *const T>(copy _2) - _4 = NonNull { pointer: copy _3 } + storage_live(ptr_2) + storage_live(_8) + storage_live(_9) + storage_live(_11) + storage_live(size_3) + size_3 = const {impl SizedTypeProperties for T}[@TraitClause0]::SIZE + storage_live(align_4) + align_4 = const {impl SizedTypeProperties for T}[@TraitClause0]::ALIGN + storage_live(layout_5) + storage_live(ptr_7) + storage_live(_12) + _12 = ub_checks + if move _12 { + _9 = core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(copy size_3, copy align_4) + } else { + } + storage_live(_10) + _10 = transmute(copy align_4) + layout_5 = Layout { size: copy size_3, align: move _10 } + storage_dead(_10) storage_live(_6) - _6 = PhantomData { } - _5 = Unique { pointer: copy _4, _marker: move _6 } - storage_live(_7) - _7 = Global { } - _0 = Box { 0: move _5, 1: move _7 } - (*_3) = move x_1 + _6 = alloc_impl_runtime(copy layout_5, const false) + match _6 { + Result::Ok => { + }, + Result::Err => { + _8 = handle_alloc_error(move layout_5) + }, + } + ptr_7 = copy (_6 as variant Result::Ok).0 + _11 = transmute, *mut [u8]>(copy ptr_7) + storage_dead(_6) + storage_dead(ptr_7) + storage_dead(layout_5) + storage_dead(align_4) + storage_dead(size_3) + ptr_2 = cast<*mut [u8], *mut T>(copy _11) + (*ptr_2) = move x_1 + _0 = transmute<*mut T, Box[@TraitClause0::parent_clause0, {built_in impl Sized for Global}, {impl Allocator for Global}]>(copy ptr_2) return } diff --git a/charon/tests/ui/regressions/issue-393-vec-with-control-flow.out b/charon/tests/ui/regressions/issue-393-vec-with-control-flow.out index 3b679d3e8..69d676020 100644 --- a/charon/tests/ui/regressions/issue-393-vec-with-control-flow.out +++ b/charon/tests/ui/regressions/issue-393-vec-with-control-flow.out @@ -1,10 +1,136 @@ -error: Could not reconstruct `Box` initialization; branching during `Box` initialization is not supported. - --> tests/ui/regressions/issue-393-vec-with-control-flow.rs:2:1 - | -2 | / pub fn next(b: bool) -> Option> { -3 | | let vec = vec![if b { 42 } else { return None }]; -4 | | Some(vec) -5 | | } - | |_^ - -ERROR Charon failed to translate this code (1 errors) +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::mem::maybe_uninit::MaybeUninit +#[lang_item("maybe_uninit")] +pub opaque type MaybeUninit +where + [@TraitClause0]: Sized, + +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option +where + [@TraitClause0]: Sized, +{ + None, + Some(T), +} + +// Full name: alloc::alloc::Global +#[lang_item("global_alloc_ty")] +pub struct Global {} + +// Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, += + +// Full name: alloc::boxed::{alloc::boxed::Box[@TraitClause0::parent_clause0, {built_in impl Sized for Global}]}::new_uninit +pub fn new_uninit() -> alloc::boxed::Box[@TraitClause0]>[{built_in impl MetaSized for MaybeUninit[@TraitClause0]}, {built_in impl Sized for Global}] +where + [@TraitClause0]: Sized, += + +// Full name: alloc::boxed::{alloc::boxed::Box[@TraitClause0]>[{built_in impl MetaSized for MaybeUninit[@TraitClause0]}, @TraitClause1]}::write +pub fn write(_1: alloc::boxed::Box[@TraitClause0]>[{built_in impl MetaSized for MaybeUninit[@TraitClause0]}, @TraitClause1], _2: T) -> alloc::boxed::Box[@TraitClause0::parent_clause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: alloc::vec::Vec +#[lang_item("Vec")] +pub opaque type Vec +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: alloc::slice::{[T]}::into_vec +pub fn into_vec(_1: alloc::boxed::Box<[T]>[{built_in impl MetaSized for [T]}, @TraitClause1]) -> Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut Vec[@TraitClause0, @TraitClause1]) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: test_crate::next +pub fn next(b_1: bool) -> Option[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}] +{ + let _0: Option[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}]; // return + let b_1: bool; // arg #1 + let vec_2: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let _3: alloc::boxed::Box[{built_in impl Sized for [u8; 1 : usize]}]>[{built_in impl MetaSized for MaybeUninit<[u8; 1 : usize]>[{built_in impl Sized for [u8; 1 : usize]}]}, {built_in impl Sized for Global}]; // anonymous local + let _4: u8; // anonymous local + let _5: bool; // anonymous local + let _6: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // anonymous local + let ret_7: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_8: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_9: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let _10: [u8; 1 : usize]; // anonymous local + let _11: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + storage_live(vec_2) + storage_live(_3) + _3 = new_uninit<[u8; 1 : usize]>[{built_in impl Sized for [u8; 1 : usize]}]() + storage_live(_4) + storage_live(_5) + _5 = copy b_1 + if move _5 { + } else { + _0 = Option::None { } + storage_dead(_5) + storage_dead(_4) + conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for [u8; 1 : usize]}], Global>[{built_in impl MetaSized for MaybeUninit<[u8; 1 : usize]>[{built_in impl Sized for [u8; 1 : usize]}]}, {built_in impl Sized for Global}]] _3 + storage_dead(_3) + storage_dead(vec_2) + return + } + _4 = const 42 : u8 + storage_dead(_5) + storage_live(_10) + _10 = [move _4] + storage_dead(_4) + storage_live(_11) + _11 = write<[u8; 1 : usize], Global>[{built_in impl Sized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _3, move _10) + storage_dead(_3) + storage_live(ret_7) + storage_live(x_8) + storage_live(y_9) + storage_dead(_10) + x_8 = move _11 + storage_dead(_11) + y_9 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_8) + ret_7 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_9) + vec_2 = move ret_7 + storage_live(_6) + _6 = move vec_2 + _0 = Option::Some { 0: move _6 } + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _6 + storage_dead(_6) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] vec_2 + storage_dead(vec_2) + return +} + + + diff --git a/charon/tests/ui/regressions/issue-393-vec-with-control-flow.rs b/charon/tests/ui/regressions/issue-393-vec-with-control-flow.rs index aa8278a28..712a45d2f 100644 --- a/charon/tests/ui/regressions/issue-393-vec-with-control-flow.rs +++ b/charon/tests/ui/regressions/issue-393-vec-with-control-flow.rs @@ -1,4 +1,3 @@ -//@ known-failure pub fn next(b: bool) -> Option> { let vec = vec![if b { 42 } else { return None }]; Some(vec) 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 8f578c6d6..7575499f4 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/efc9e1b50cbf2cede7ebe25f0a1fc64fd8b3e942/compiler/rustc_middle/src/ty/sty.rs:352:13: cannot find `K/#0` in param-env: ParamEnv { +error: internal compiler error: /rustc-dev/5fb2ff8611e5a4af4dc85977cfdecfbf3ffa6ade/compiler/rustc_middle/src/ty/sty.rs:352: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/efc9e1b50cbf2cede7ebe25f0a1fc64fd8b3e } -thread 'rustc' panicked at /rustc-dev/efc9e1b50cbf2cede7ebe25f0a1fc64fd8b3e942/compiler/rustc_middle/src/ty/sty.rs:352:13: +thread 'rustc' panicked at /rustc-dev/5fb2ff8611e5a4af4dc85977cfdecfbf3ffa6ade/compiler/rustc_middle/src/ty/sty.rs:352: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/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index 8fe1e1aca..ddd98098b 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -469,18 +469,6 @@ fn compiletime<'_0>(fmt_1: Arguments<'_0>, force_no_backtrace_2: bool) -> ! panic(core::panicking::panic_fmt) } -// Full name: core::num::{usize}::MAX -pub fn MAX() -> usize -{ - let _0: usize; // return - - _0 = ~(const 0 : usize) - return -} - -// Full name: core::num::{usize}::MAX -pub const MAX: usize = MAX() - // Full name: core::ops::range::RangeInclusive #[lang_item("RangeInclusive")] pub struct RangeInclusive @@ -1188,9 +1176,9 @@ where let slice_2: &'9 mut [T]; // arg #2 let _3: bool; // anonymous local let self_4: usize; // local - let exclusive_end_5: usize; // local - let _6: bool; // anonymous local - let _7: usize; // anonymous local + let _5: usize; // anonymous local + let exclusive_end_6: usize; // local + let _7: bool; // anonymous local let _8: &'12 mut [T]; // anonymous local let _9: *mut [T]; // anonymous local let ptr_10: *mut [T]; // local @@ -1204,13 +1192,15 @@ where let _18: Option<&'16 mut [T]>[{built_in impl Sized for &'18 mut [T]}]; // anonymous local storage_live(self_4) - storage_live(exclusive_end_5) + storage_live(_5) + 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 - _3 = copy self_4 == copy MAX + _5 = copy slice_2.metadata + _3 = copy self_4 >= copy _5 if move _3 { storage_live(_17) _17 = Option::None { } @@ -1218,28 +1208,25 @@ where } else { self_15 = move (self_1).start self_16 = move (self_1).exhausted - exclusive_end_5 = copy self_4 wrap.+ const 1 : usize + exclusive_end_6 = copy self_4 wrap.+ const 1 : usize if copy self_16 { - self_15 = copy exclusive_end_5 + self_15 = copy exclusive_end_6 } else { } storage_live(_8) storage_live(_11) - _11 = copy exclusive_end_5 < copy self_15 + _11 = copy exclusive_end_6 < copy self_15 if move _11 { storage_dead(_11) storage_live(_18) _18 = Option::None { } _0 = move _18 } else { - new_len_12 = copy exclusive_end_5 ub.- copy self_15 + new_len_12 = copy exclusive_end_6 ub.- copy self_15 storage_dead(_11) - storage_live(_6) storage_live(_7) - _7 = copy slice_2.metadata - _6 = copy exclusive_end_5 <= move _7 - if move _6 { - storage_dead(_7) + _7 = copy exclusive_end_6 <= copy _5 + if move _7 { storage_live(_9) storage_live(ptr_10) ptr_10 = &raw mut (*slice_2) with_metadata(copy slice_2.metadata) @@ -1255,13 +1242,12 @@ where _0 = Option::Some { 0: copy _8 } storage_dead(_9) } else { - storage_dead(_7) storage_live(_18) _18 = Option::None { } _0 = move _18 } } - storage_dead(_6) + storage_dead(_7) storage_dead(_8) } storage_dead(_3) @@ -1278,9 +1264,9 @@ where let slice_2: &'9 [T]; // arg #2 let _3: bool; // anonymous local let self_4: usize; // local - let exclusive_end_5: usize; // local - let _6: bool; // anonymous local - let _7: usize; // anonymous local + let _5: usize; // anonymous local + let exclusive_end_6: usize; // local + let _7: bool; // anonymous local let _8: &'12 [T]; // anonymous local let _9: *const [T]; // anonymous local let _10: *const [T]; // anonymous local @@ -1294,13 +1280,15 @@ where let _18: Option<&'16 [T]>[{built_in impl Sized for &'18 [T]}]; // anonymous local storage_live(self_4) - storage_live(exclusive_end_5) + storage_live(_5) + 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 - _3 = copy self_4 == copy MAX + _5 = copy slice_2.metadata + _3 = copy self_4 >= copy _5 if move _3 { storage_live(_17) _17 = Option::None { } @@ -1308,28 +1296,25 @@ where } else { self_15 = move (self_1).start self_16 = move (self_1).exhausted - exclusive_end_5 = copy self_4 wrap.+ const 1 : usize + exclusive_end_6 = copy self_4 wrap.+ const 1 : usize if copy self_16 { - self_15 = copy exclusive_end_5 + self_15 = copy exclusive_end_6 } else { } storage_live(_8) storage_live(_11) - _11 = copy exclusive_end_5 < copy self_15 + _11 = copy exclusive_end_6 < copy self_15 if move _11 { storage_dead(_11) storage_live(_18) _18 = Option::None { } _0 = move _18 } else { - new_len_12 = copy exclusive_end_5 ub.- copy self_15 + new_len_12 = copy exclusive_end_6 ub.- copy self_15 storage_dead(_11) - storage_live(_6) storage_live(_7) - _7 = copy slice_2.metadata - _6 = copy exclusive_end_5 <= move _7 - if move _6 { - storage_dead(_7) + _7 = copy exclusive_end_6 <= copy _5 + if move _7 { storage_live(_9) storage_live(_10) _10 = &raw const (*slice_2) with_metadata(copy slice_2.metadata) @@ -1345,13 +1330,12 @@ where _0 = Option::Some { 0: copy _8 } storage_dead(_9) } else { - storage_dead(_7) storage_live(_18) _18 = Option::None { } _0 = move _18 } } - storage_dead(_6) + storage_dead(_7) storage_dead(_8) } storage_dead(_3) diff --git a/charon/tests/ui/simple/vec-push.out b/charon/tests/ui/simple/vec-push.out index 0a4fad7ba..f4a830a2f 100644 --- a/charon/tests/ui/simple/vec-push.out +++ b/charon/tests/ui/simple/vec-push.out @@ -246,7 +246,7 @@ where storage_dead(self_9) storage_live(src_10) src_10 = move value_2 - (*end_8) = copy src_10 + (*end_8) = move src_10 storage_dead(src_10) ((*self_1)).len = copy len_3 wrap.+ const 1 : usize _0 = &mut (*end_8) diff --git a/charon/tests/ui/vec-reconstruct-move-values.out b/charon/tests/ui/vec-reconstruct-move-values.out index 993a288b4..b6fd87e21 100644 --- a/charon/tests/ui/vec-reconstruct-move-values.out +++ b/charon/tests/ui/vec-reconstruct-move-values.out @@ -16,13 +16,6 @@ pub trait Sized #[lang_item("global_alloc_ty")] pub struct Global {} -// Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) -where - [@TraitClause0]: MetaSized, - [@TraitClause1]: Sized, -= - // Full name: alloc::vec::Vec #[lang_item("Vec")] pub opaque type Vec @@ -31,7 +24,6 @@ where [@TraitClause1]: Sized, // Full name: alloc::slice::{[T]}::into_vec -#[lang_item("slice_into_vec")] pub fn into_vec(_1: alloc::boxed::Box<[T]>[{built_in impl MetaSized for [T]}, @TraitClause1]) -> Vec[@TraitClause0, @TraitClause1] where [@TraitClause0]: Sized, @@ -57,72 +49,72 @@ fn move_values(flag_1: bool) let flag_1: bool; // arg #1 let x_2: NoCopy; // local let _v_3: Vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]; // local - let _4: alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}]; // anonymous local - let _5: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _6: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _7: NoCopy; // anonymous local - let _8: bool; // anonymous local - let y_9: NoCopy; // local - let _w_10: Vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]; // local - let _11: alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}]; // anonymous local - let _12: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _13: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local - let _14: NoCopy; // anonymous local + let _4: NoCopy; // anonymous local + let _5: bool; // anonymous local + let y_6: NoCopy; // local + let _w_7: Vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]; // local + let _8: NoCopy; // anonymous local + let ret_9: Vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]; // local + let x_10: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_11: alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}]; // local + let ret_12: Vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]; // local + let x_13: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_14: alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}]; // local let _15: [NoCopy; 1 : usize]; // anonymous local - let _16: [NoCopy; 1 : usize]; // anonymous local + let _16: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _17: [NoCopy; 1 : usize]; // anonymous local + let _18: alloc::boxed::Box<[NoCopy; 1 : usize]>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local _0 = () storage_live(x_2) x_2 = NoCopy { 0: const 4 : u8 } storage_live(_v_3) storage_live(_4) - storage_live(_5) + _4 = move x_2 storage_live(_15) - _15 = [move _7] - storage_live(_6) - _6 = @BoxNew<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}](move _15) - storage_live(_7) - _7 = move x_2 - storage_dead(_7) - _5 = move _6 - _4 = unsize_cast[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}], 1 : usize>(move _5) - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]] _5 - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]] _6 - storage_dead(_6) - storage_dead(_5) - _v_3 = into_vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}](move _4) + _15 = [move _4] storage_dead(_4) - storage_live(_8) - _8 = copy flag_1 - if move _8 { - storage_live(y_9) - y_9 = NoCopy { 0: const 5 : u8 } - storage_live(_w_10) - storage_live(_11) - storage_live(_12) - storage_live(_16) - _16 = [move _14] - storage_live(_13) - _13 = @BoxNew<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}](move _16) - storage_live(_14) - _14 = move y_9 - storage_dead(_14) - _12 = move _13 - _11 = unsize_cast[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}], 1 : usize>(move _12) - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]] _12 - conditional_drop[{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}]] _13 - storage_dead(_13) - storage_dead(_12) - _w_10 = into_vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}](move _11) - storage_dead(_11) + storage_live(_16) + _16 = @BoxNew<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}](move _15) + storage_live(ret_9) + storage_live(x_10) + storage_live(y_11) + storage_dead(_15) + x_10 = move _16 + storage_dead(_16) + y_11 = unsize_cast[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}], 1 : usize>(move x_10) + ret_9 = into_vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}](move y_11) + _v_3 = move ret_9 + storage_live(_5) + _5 = copy flag_1 + if move _5 { + storage_live(y_6) + y_6 = NoCopy { 0: const 5 : u8 } + storage_live(_w_7) + storage_live(_8) + _8 = move y_6 + storage_live(_17) + _17 = [move _8] + storage_dead(_8) + storage_live(_18) + _18 = @BoxNew<[NoCopy; 1 : usize], Global>[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}](move _17) + storage_live(ret_12) + storage_live(x_13) + storage_live(y_14) + storage_dead(_17) + x_13 = move _18 + storage_dead(_18) + y_14 = unsize_cast[{built_in impl MetaSized for [NoCopy; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[NoCopy]>[{built_in impl MetaSized for [NoCopy]}, {built_in impl Sized for Global}], 1 : usize>(move x_13) + ret_12 = into_vec[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}](move y_14) + _w_7 = move ret_12 _0 = () - conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]] _w_10 - storage_dead(_w_10) - storage_dead(y_9) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]] _w_7 + storage_dead(_w_7) + storage_dead(y_6) } else { _0 = () } - storage_dead(_8) + storage_dead(_5) conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for NoCopy}, {built_in impl Sized for Global}]] _v_3 storage_dead(_v_3) storage_dead(x_2) diff --git a/charon/tests/ui/vec-reconstruct-multiple-adjacent.out b/charon/tests/ui/vec-reconstruct-multiple-adjacent.out index 4ba8dad61..5f7e4b5d9 100644 --- a/charon/tests/ui/vec-reconstruct-multiple-adjacent.out +++ b/charon/tests/ui/vec-reconstruct-multiple-adjacent.out @@ -1,11 +1,247 @@ -error: Could not reconstruct `Box` initialization; branching during `Box` initialization is not supported. - --> tests/ui/vec-reconstruct-multiple-adjacent.rs:12:1 - | -12 | / fn with_fn_calls() { -13 | | fn foo() -> u8 { -14 | | 42 -... | -17 | | } - | |_^ - -ERROR Charon failed to translate this code (1 errors) +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::clone::Clone +#[lang_item("clone")] +pub trait Clone +{ + parent_clause0 : [@TraitClause0]: Sized + fn clone<'_0_1> = core::clone::Clone::clone<'_0_1, Self>[Self] + non-dyn-compatible +} + +#[lang_item("clone_fn")] +pub fn core::clone::Clone::clone<'_0, Self>(_1: &'_0 Self) -> Self +where + [@TraitClause0]: Clone, += + +// Full name: core::clone::impls::{impl Clone for u8}::clone +pub fn {impl Clone for u8}::clone<'_0>(_1: &'_0 u8) -> u8 += + +// Full name: core::clone::impls::{impl Clone for u8} +impl Clone for u8 { + parent_clause0 = {built_in impl Sized for u8} + fn clone<'_0_1> = {impl Clone for u8}::clone<'_0_1> + non-dyn-compatible +} + +// Full name: alloc::alloc::Global +#[lang_item("global_alloc_ty")] +pub struct Global {} + +// Full name: alloc::vec::Vec +#[lang_item("Vec")] +pub opaque type Vec +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: alloc::slice::{[T]}::into_vec +pub fn into_vec(_1: alloc::boxed::Box<[T]>[{built_in impl MetaSized for [T]}, @TraitClause1]) -> Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut Vec[@TraitClause0, @TraitClause1]) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: alloc::vec::from_elem +#[lang_item("vec_from_elem")] +pub fn from_elem(_1: T, _2: usize) -> Vec[@TraitClause0, {built_in impl Sized for Global}] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Clone, += + +// Full name: test_crate::multiple_adjacent +fn multiple_adjacent() +{ + let _0: (); // return + let _a_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let _b_2: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let _c_3: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let ret_4: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_5: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_6: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let ret_7: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_8: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_9: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let ret_10: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_11: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_12: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let _13: [u8; 1 : usize]; // anonymous local + let _14: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _15: [u8; 1 : usize]; // anonymous local + let _16: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _17: [u8; 1 : usize]; // anonymous local + let _18: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + _0 = () + storage_live(_a_1) + storage_live(_13) + _13 = [const 1 : u8] + storage_live(_14) + _14 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _13) + storage_live(ret_4) + storage_live(x_5) + storage_live(y_6) + storage_dead(_13) + x_5 = move _14 + storage_dead(_14) + y_6 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_5) + ret_4 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_6) + _a_1 = move ret_4 + storage_live(_b_2) + storage_live(_15) + _15 = [const 2 : u8] + storage_live(_16) + _16 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _15) + storage_live(ret_7) + storage_live(x_8) + storage_live(y_9) + storage_dead(_15) + x_8 = move _16 + storage_dead(_16) + y_9 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_8) + ret_7 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_9) + _b_2 = move ret_7 + storage_live(_c_3) + storage_live(_17) + _17 = [const 3 : u8] + storage_live(_18) + _18 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _17) + storage_live(ret_10) + storage_live(x_11) + storage_live(y_12) + storage_dead(_17) + x_11 = move _18 + storage_dead(_18) + y_12 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_11) + ret_10 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_12) + _c_3 = move ret_10 + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _c_3 + storage_dead(_c_3) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _b_2 + storage_dead(_b_2) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _a_1 + storage_dead(_a_1) + return +} + +// Full name: test_crate::multiple_values +fn multiple_values() +{ + let _0: (); // return + let _a_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let ret_2: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_3: alloc::boxed::Box<[u8; 3 : usize]>[{built_in impl MetaSized for [u8; 3 : usize]}, {built_in impl Sized for Global}]; // local + let y_4: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let _5: [u8; 3 : usize]; // anonymous local + let _6: alloc::boxed::Box<[u8; 3 : usize]>[{built_in impl MetaSized for [u8; 3 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + _0 = () + storage_live(_a_1) + storage_live(_5) + _5 = [const 1 : u8, const 2 : u8, const 3 : u8] + storage_live(_6) + _6 = @BoxNew<[u8; 3 : usize], Global>[{built_in impl MetaSized for [u8; 3 : usize]}, {built_in impl Sized for Global}](move _5) + storage_live(ret_2) + storage_live(x_3) + storage_live(y_4) + storage_dead(_5) + x_3 = move _6 + storage_dead(_6) + y_4 = unsize_cast[{built_in impl MetaSized for [u8; 3 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 3 : usize>(move x_3) + ret_2 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_4) + _a_1 = move ret_2 + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _a_1 + storage_dead(_a_1) + return +} + +// Full name: test_crate::with_fn_calls::foo +fn foo() -> u8 +{ + let _0: u8; // return + + _0 = const 42 : u8 + return +} + +// Full name: test_crate::with_fn_calls +fn with_fn_calls() +{ + let _0: (); // return + let _a_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let _2: u8; // anonymous local + let _3: u8; // anonymous local + let ret_4: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_5: alloc::boxed::Box<[u8; 2 : usize]>[{built_in impl MetaSized for [u8; 2 : usize]}, {built_in impl Sized for Global}]; // local + let y_6: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let _7: [u8; 2 : usize]; // anonymous local + let _8: alloc::boxed::Box<[u8; 2 : usize]>[{built_in impl MetaSized for [u8; 2 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + _0 = () + storage_live(_a_1) + storage_live(_2) + _2 = foo() + storage_live(_3) + _3 = foo() + storage_live(_7) + _7 = [move _2, move _3] + storage_dead(_3) + storage_dead(_2) + storage_live(_8) + _8 = @BoxNew<[u8; 2 : usize], Global>[{built_in impl MetaSized for [u8; 2 : usize]}, {built_in impl Sized for Global}](move _7) + storage_live(ret_4) + storage_live(x_5) + storage_live(y_6) + storage_dead(_7) + x_5 = move _8 + storage_dead(_8) + y_6 = unsize_cast[{built_in impl MetaSized for [u8; 2 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 2 : usize>(move x_5) + ret_4 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_6) + _a_1 = move ret_4 + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _a_1 + storage_dead(_a_1) + return +} + +// Full name: test_crate::repeated +fn repeated() +{ + let _0: (); // return + let _a_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + + _0 = () + storage_live(_a_1) + _a_1 = from_elem[{built_in impl Sized for u8}, {impl Clone for u8}](const 1 : u8, const 3 : usize) + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _a_1 + storage_dead(_a_1) + return +} + + + diff --git a/charon/tests/ui/vec-reconstruct-multiple-adjacent.rs b/charon/tests/ui/vec-reconstruct-multiple-adjacent.rs index e7319918a..79475f660 100644 --- a/charon/tests/ui/vec-reconstruct-multiple-adjacent.rs +++ b/charon/tests/ui/vec-reconstruct-multiple-adjacent.rs @@ -1,4 +1,3 @@ -//@ known-failure fn multiple_adjacent() { let _a = vec![1u8]; let _b = vec![2u8]; diff --git a/charon/tests/ui/vec-reconstruct-nested.out b/charon/tests/ui/vec-reconstruct-nested.out index 94fc0d3e2..039182ba2 100644 --- a/charon/tests/ui/vec-reconstruct-nested.out +++ b/charon/tests/ui/vec-reconstruct-nested.out @@ -1,17 +1,171 @@ -error: Could not reconstruct `Box` initialization; branching during `Box` initialization is not supported. - --> tests/ui/vec-reconstruct-nested.rs:2:1 - | -2 | / fn nested_vecs() { -3 | | let _nested = vec![vec![1u8], vec![2u8]]; -4 | | } - | |_^ - -error: Could not reconstruct `Box` initialization; branching during `Box` initialization is not supported. - --> tests/ui/vec-reconstruct-nested.rs:6:1 - | -6 | / fn nested_single() { -7 | | let _nested = vec![vec![1u8]]; -8 | | } - | |_^ - -ERROR Charon failed to translate this code (2 errors) +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: alloc::alloc::Global +#[lang_item("global_alloc_ty")] +pub struct Global {} + +// Full name: alloc::vec::Vec +#[lang_item("Vec")] +pub opaque type Vec +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: alloc::slice::{[T]}::into_vec +pub fn into_vec(_1: alloc::boxed::Box<[T]>[{built_in impl MetaSized for [T]}, @TraitClause1]) -> Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(_1: *mut Vec[@TraitClause0, @TraitClause1]) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, += + +// Full name: test_crate::nested_vecs +fn nested_vecs() +{ + let _0: (); // return + let _nested_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]; // local + let _2: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // anonymous local + let _3: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // anonymous local + let ret_4: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_5: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_6: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let ret_7: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_8: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_9: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let ret_10: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]; // local + let x_11: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]}, {built_in impl Sized for Global}]; // local + let y_12: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]}, {built_in impl Sized for Global}]; // local + let _13: [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]; // anonymous local + let _14: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _15: [u8; 1 : usize]; // anonymous local + let _16: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _17: [u8; 1 : usize]; // anonymous local + let _18: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + _0 = () + storage_live(_nested_1) + storage_live(_2) + storage_live(_15) + _15 = [const 1 : u8] + storage_live(_16) + _16 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _15) + storage_live(ret_4) + storage_live(x_5) + storage_live(y_6) + storage_dead(_15) + x_5 = move _16 + storage_dead(_16) + y_6 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_5) + ret_4 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_6) + _2 = move ret_4 + storage_live(_3) + storage_live(_17) + _17 = [const 2 : u8] + storage_live(_18) + _18 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _17) + storage_live(ret_7) + storage_live(x_8) + storage_live(y_9) + storage_dead(_17) + x_8 = move _18 + storage_dead(_18) + y_9 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_8) + ret_7 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_9) + _3 = move ret_7 + storage_live(_13) + _13 = [move _2, move _3] + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _3 + storage_dead(_3) + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _2 + storage_dead(_2) + storage_live(_14) + _14 = @BoxNew<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize], Global>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]}, {built_in impl Sized for Global}](move _13) + storage_live(ret_10) + storage_live(x_11) + storage_live(y_12) + storage_dead(_13) + x_11 = move _14 + storage_dead(_14) + y_12 = unsize_cast[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 2 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]}, {built_in impl Sized for Global}], 2 : usize>(move x_11) + ret_10 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}], Global>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}](move y_12) + _nested_1 = move ret_10 + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}], Global>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]] _nested_1 + storage_dead(_nested_1) + return +} + +// Full name: test_crate::nested_single +fn nested_single() +{ + let _0: (); // return + let _nested_1: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]; // local + let _2: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // anonymous local + let ret_3: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; // local + let x_4: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_5: alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}]; // local + let ret_6: Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]; // local + let x_7: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]}, {built_in impl Sized for Global}]; // local + let y_8: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]}, {built_in impl Sized for Global}]; // local + let _9: [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]; // anonymous local + let _10: alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + let _11: [u8; 1 : usize]; // anonymous local + let _12: alloc::boxed::Box<[u8; 1 : usize]>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}]; // anonymous local + + _0 = () + storage_live(_nested_1) + storage_live(_2) + storage_live(_11) + _11 = [const 1 : u8] + storage_live(_12) + _12 = @BoxNew<[u8; 1 : usize], Global>[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}](move _11) + storage_live(ret_3) + storage_live(x_4) + storage_live(y_5) + storage_dead(_11) + x_4 = move _12 + storage_dead(_12) + y_5 = unsize_cast[{built_in impl MetaSized for [u8; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[u8]>[{built_in impl MetaSized for [u8]}, {built_in impl Sized for Global}], 1 : usize>(move x_4) + ret_3 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}](move y_5) + _2 = move ret_3 + storage_live(_9) + _9 = [move _2] + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}]] _2 + storage_dead(_2) + storage_live(_10) + _10 = @BoxNew<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize], Global>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]}, {built_in impl Sized for Global}](move _9) + storage_live(ret_6) + storage_live(x_7) + storage_live(y_8) + storage_dead(_9) + x_7 = move _10 + storage_dead(_10) + y_8 = unsize_cast[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]; 1 : usize]}, {built_in impl Sized for Global}], alloc::boxed::Box<[Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]>[{built_in impl MetaSized for [Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]]}, {built_in impl Sized for Global}], 1 : usize>(move x_7) + ret_6 = into_vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}], Global>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}](move y_8) + _nested_1 = move ret_6 + _0 = () + conditional_drop[{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place[{built_in impl Sized for u8}, {built_in impl Sized for Global}], Global>[{built_in impl Sized for Vec[{built_in impl Sized for u8}, {built_in impl Sized for Global}]}, {built_in impl Sized for Global}]] _nested_1 + storage_dead(_nested_1) + return +} + + + diff --git a/charon/tests/ui/vec-reconstruct-nested.rs b/charon/tests/ui/vec-reconstruct-nested.rs index ffd5f9427..c258fe9b2 100644 --- a/charon/tests/ui/vec-reconstruct-nested.rs +++ b/charon/tests/ui/vec-reconstruct-nested.rs @@ -1,4 +1,3 @@ -//@ known-failure fn nested_vecs() { let _nested = vec![vec![1u8], vec![2u8]]; }