diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index a4e820463..0b78fced5 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.145" +let supported_charon_version = "0.1.146" diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml index 4c57b0fff..100cfa31c 100644 --- a/charon-ml/src/PrintExpressions.ml +++ b/charon-ml/src/PrintExpressions.ml @@ -88,6 +88,8 @@ and nullop_to_string (env : 'a fmt_env) (op : nullop) : string = | AlignOf -> "align_of" | OffsetOf _ -> "offset_of(?)" | UbChecks -> "ub_checks" + | ContractChecks -> "contract_checks" + | OverflowChecks -> "overflow_checks" and unop_to_string (env : 'a fmt_env) (unop : unop) : string = match unop with diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index 131ea5fe9..3a70a808f 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/charon-ml/src/generated/Generated_Expressions.ml @@ -216,7 +216,13 @@ and field_proj_kind = and local_id = (LocalId.id[@visitors.opaque]) (** Nullary operation *) -and nullop = SizeOf | AlignOf | OffsetOf of (int * field_id) list | UbChecks +and nullop = + | SizeOf + | AlignOf + | OffsetOf of type_decl_ref * variant_id option * field_id + | UbChecks + | OverflowChecks + | ContractChecks and operand = | Copy of place diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index a5edb9218..c4ffb6b2f 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1295,12 +1295,14 @@ and nullop_of_json (ctx : of_json_ctx) (js : json) : (nullop, string) result = (match js with | `String "SizeOf" -> Ok SizeOf | `String "AlignOf" -> Ok AlignOf - | `Assoc [ ("OffsetOf", offset_of) ] -> - let* offset_of = - list_of_json (pair_of_json int_of_json field_id_of_json) ctx offset_of - in - Ok (OffsetOf offset_of) + | `Assoc [ ("OffsetOf", `List [ x_0; x_1; x_2 ]) ] -> + let* x_0 = type_decl_ref_of_json ctx x_0 in + let* x_1 = option_of_json variant_id_of_json ctx x_1 in + let* x_2 = field_id_of_json ctx x_2 in + Ok (OffsetOf (x_0, x_1, x_2)) | `String "UbChecks" -> Ok UbChecks + | `String "OverflowChecks" -> Ok OverflowChecks + | `String "ContractChecks" -> Ok ContractChecks | _ -> Error "") and operand_of_json (ctx : of_json_ctx) (js : json) : (operand, string) result = diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 54a8787d9..5b8e54e9d 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -219,7 +219,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.145" +version = "0.1.146" dependencies = [ "annotate-snippets", "anstream", @@ -836,7 +836,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.3.5" -source = "git+https://github.com/AeneasVerif/hax?branch=main#ac6529a23e683c0bc86b348e7d75fad524182851" +source = "git+https://github.com/AeneasVerif/hax?branch=main#111a897f8265f458a44bd2027b66c10b0252d4f6" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -847,7 +847,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.3.5" -source = "git+https://github.com/AeneasVerif/hax?branch=main#ac6529a23e683c0bc86b348e7d75fad524182851" +source = "git+https://github.com/AeneasVerif/hax?branch=main#111a897f8265f458a44bd2027b66c10b0252d4f6" dependencies = [ "extension-traits", "hax-adt-into", @@ -864,7 +864,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.3.5" -source = "git+https://github.com/AeneasVerif/hax?branch=main#ac6529a23e683c0bc86b348e7d75fad524182851" +source = "git+https://github.com/AeneasVerif/hax?branch=main#111a897f8265f458a44bd2027b66c10b0252d4f6" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 0e3ae2785..17905486f 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.145" +version = "0.1.146" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/rust-toolchain b/charon/rust-toolchain index 60f603ea2..7abf500f6 100644 --- a/charon/rust-toolchain +++ b/charon/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2025-11-08" +channel = "nightly-2025-11-23" components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ] targets = [ "x86_64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ] diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index 6b7bf2c71..f20af5681 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -176,9 +176,10 @@ pub enum UnOp { pub enum NullOp { SizeOf, AlignOf, - #[drive(skip)] - OffsetOf(Vec<(usize, FieldId)>), + OffsetOf(TypeDeclRef, Option, FieldId), UbChecks, + OverflowChecks, + ContractChecks, } /// For all the variants: the first type gives the source type, the second one gives diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 6054d45ef..1964548e0 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -252,4 +252,19 @@ impl FnPtr { generics: generics.into(), } } + + /// Get the generics for the pre-monomorphization item. + pub fn pre_mono_generics<'a>(&'a self, krate: &'a TranslatedCrate) -> &'a GenericArgs { + match *self.kind { + FnPtrKind::Fun(FunId::Regular(fun_id)) => krate + .item_name(fun_id) + .unwrap() + .mono_args() + .unwrap_or(&self.generics), + // We don't mono builtins. + FnPtrKind::Fun(FunId::Builtin(..)) => &self.generics, + // Can't happen in mono mode. + FnPtrKind::Trait(..) => &self.generics, + } + } } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 480e4dc36..aa4e298c0 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -593,6 +593,12 @@ impl LiteralTy { } } +impl From for Ty { + fn from(value: LiteralTy) -> Self { + TyKind::Literal(value).into_ty() + } +} + /// A value of type `T` bound by the generic parameters of item /// `item`. Used when dealing with multiple items at a time, to /// ensure we don't mix up generics. diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 80c613ddc..208d0c9ad 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -542,23 +542,13 @@ impl BodyTransCtx<'_, '_, '_> { self.translate_operand(span, left)?, self.translate_operand(span, right)?, )), - hax::Rvalue::NullaryOp(nullop, ty) => { - trace!("NullOp: {:?}", nullop); - let ty = self.translate_ty(span, ty)?; - let op = match nullop { - hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf( - fields - .iter() - .copied() - .map(|(n, idx)| (n, translate_field_id(idx))) - .collect(), - ), - hax::NullOp::UbChecks => NullOp::UbChecks, - hax::NullOp::ContractChecks => { - raise_error!(self, span, "charon does not support contracts"); - } + hax::Rvalue::NullaryOp(hax::NullOp::RuntimeChecks(check)) => { + let op = match check { + hax::RuntimeChecks::UbChecks => NullOp::UbChecks, + hax::RuntimeChecks::OverflowChecks => NullOp::OverflowChecks, + hax::RuntimeChecks::ContractChecks => NullOp::ContractChecks, }; - Ok(Rvalue::NullaryOp(op, ty)) + Ok(Rvalue::NullaryOp(op, LiteralTy::Bool.into())) } hax::Rvalue::UnaryOp(unop, operand) => { let operand = self.translate_operand(span, operand)?; diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index d47af4ac7..654e4b09b 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -351,11 +351,14 @@ impl ItemTransCtx<'_, '_> { // arg-N, rest... // We then add N statements of the form `locals[N+3] := move locals[2].N`, // to destructure the arguments. - let GExprBody { + let Body::Unstructured(GExprBody { locals, body: blocks, .. - } = body.as_unstructured_mut().unwrap(); + }) = &mut body + else { + return Ok(body); + }; blocks.dyn_visit_mut(|local: &mut LocalId| { if local.index() >= 2 { diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index 042eb783f..2c5961166 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -92,15 +92,19 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .try_collect()?; expressions::ConstantExprKind::Adt(None, fields) } - ConstantExprKind::TraitConst { impl_expr, name } => { - let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?; - let name = TraitItemName(name.into()); - expressions::ConstantExprKind::TraitConst(trait_ref, name) - } - ConstantExprKind::GlobalName(item) => { - let global_ref = self.translate_global_decl_ref(span, item)?; - expressions::ConstantExprKind::Global(global_ref) - } + ConstantExprKind::NamedGlobal(item) => match &item.in_trait { + Some(impl_expr) => { + let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?; + // Trait consts can't have their own generics. + assert!(item.generic_args.is_empty()); + let name = self.translate_trait_item_name(&item.def_id)?; + expressions::ConstantExprKind::TraitConst(trait_ref, name) + } + None => { + let global_ref = self.translate_global_decl_ref(span, item)?; + expressions::ConstantExprKind::Global(global_ref) + } + }, ConstantExprKind::Borrow(v) if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) = v.contents.as_ref() => diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 405ac01ef..8399aecf2 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -972,12 +972,24 @@ impl FmtWithCtx for Name { } impl FmtWithCtx for NullOp { - fn fmt_with_ctx(&self, _ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { + fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { let op = match self { NullOp::SizeOf => "size_of", NullOp::AlignOf => "align_of", - NullOp::OffsetOf(_) => "offset_of(?)", + &NullOp::OffsetOf(ref ty, variant, field) => { + let tid = *ty.id.as_adt().expect("found offset_of of a non-adt type"); + write!(f, "offset_of({}.", ty.with_ctx(ctx))?; + if let Some(variant) = variant { + ctx.format_enum_variant_name(f, tid, variant)?; + write!(f, ".")?; + } + ctx.format_field_name(f, tid, variant, field)?; + write!(f, ")")?; + return Ok(()); + } NullOp::UbChecks => "ub_checks", + NullOp::OverflowChecks => "overflow_checks", + NullOp::ContractChecks => "contract_checks", }; write!(f, "{op}") } diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 7c24538e9..09b49a2d5 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -53,7 +53,7 @@ pub trait AstFormatter: Sized { where GenericParams: HasVectorOf; - fn format_enum_variant( + fn format_enum_variant_name( &self, f: &mut fmt::Formatter<'_>, type_id: TypeDeclId, @@ -67,7 +67,17 @@ pub trait AstFormatter: Sized { } else { &variant_id.to_pretty_string() }; - write!(f, "{}::{variant}", type_id.with_ctx(self)) + write!(f, "{variant}") + } + fn format_enum_variant( + &self, + f: &mut fmt::Formatter<'_>, + type_id: TypeDeclId, + variant_id: VariantId, + ) -> fmt::Result { + write!(f, "{}::", type_id.with_ctx(self))?; + self.format_enum_variant_name(f, type_id, variant_id)?; + Ok(()) } fn format_field_name( diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 4f79a59e6..7ba0b48b6 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -35,6 +35,7 @@ pub mod resugar { pub mod reconstruct_asserts; pub mod reconstruct_boxes; pub mod reconstruct_fallible_operations; + pub mod reconstruct_intrinsics; pub mod reconstruct_matches; } @@ -133,6 +134,9 @@ pub static ULLBC_PASSES: &[Pass] = &[ // **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]. UnstructuredBody(&resugar::reconstruct_fallible_operations::Transform), + // Recognize calls to the `offset_of` intrinsics and replace them with the corresponding + // `NullOp`. + UnstructuredBody(&resugar::reconstruct_intrinsics::Transform), // # Micro-pass: 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, diff --git a/charon/src/transform/resugar/reconstruct_intrinsics.rs b/charon/src/transform/resugar/reconstruct_intrinsics.rs new file mode 100644 index 000000000..d4444d828 --- /dev/null +++ b/charon/src/transform/resugar/reconstruct_intrinsics.rs @@ -0,0 +1,54 @@ +use crate::transform::TransformCtx; +use crate::transform::ctx::{BodyTransformCtx, UllbcPass}; +use crate::ullbc_ast::*; + +pub struct Transform; +impl UllbcPass for Transform { + fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { + decl.transform_ullbc_terminators(ctx, |ctx, term| { + let TerminatorKind::Call { call, target, .. } = &term.kind else { + return; + }; + let FnOperand::Regular(fn_ptr) = &call.func else { + return; + }; + let FnPtrKind::Fun(FunId::Regular(fun_id)) = &fn_ptr.kind else { + return; + }; + let Some(fun_decl) = ctx.ctx.translated.fun_decls.get(*fun_id) else { + return; + }; + if fun_decl.item_meta.lang_item.as_deref() == Some("offset_of") + && let generics = fn_ptr.pre_mono_generics(&ctx.ctx.translated) + && let Some(ty) = generics.types.get(TypeVarId::ZERO) + && let TyKind::Adt(tref) = ty.kind() + && let TypeId::Adt(type_id) = tref.id + && let [Operand::Const(arg0), Operand::Const(arg1)] = call.args.as_slice() + && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned( + UIntTy::U32, + variant_id, + ))) = &arg0.kind + && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned( + UIntTy::U32, + field_id, + ))) = &arg1.kind + && let Some(tdecl) = ctx.ctx.translated.type_decls.get(type_id) + { + // TODO: move into a pass, maybe also size_of/align_of? or remove the nullops. + // maybe this is a constant also. + let variant_id = if tdecl.kind.is_enum() { + Some(VariantId::from_usize(*variant_id as usize)) + } else { + None + }; + let field_id = FieldId::from_usize(*field_id as usize); + let rval = Rvalue::NullaryOp( + NullOp::OffsetOf(tref.clone(), variant_id, field_id), + Ty::mk_usize(), + ); + ctx.insert_assn_stmt(call.dest.clone(), rval); + term.kind = TerminatorKind::Goto { target: *target }; + } + }); + } +} diff --git a/charon/src/transform/simplify_output/hide_marker_traits.rs b/charon/src/transform/simplify_output/hide_marker_traits.rs index 33b945ae7..d89faebe2 100644 --- a/charon/src/transform/simplify_output/hide_marker_traits.rs +++ b/charon/src/transform/simplify_output/hide_marker_traits.rs @@ -76,6 +76,7 @@ impl TransformPass for Transform { "core::marker::Send", "core::marker::Sync", "core::marker::Unpin", + "core::clone::TrivialClone", ] } else { vec![] diff --git a/charon/tests/cargo/dependencies.out b/charon/tests/cargo/dependencies.out index 5543caed0..eed574d7d 100644 --- a/charon/tests/cargo/dependencies.out +++ b/charon/tests/cargo/dependencies.out @@ -3,8 +3,6 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::marker::MetaSized #[lang_item("meta_sized")] diff --git a/charon/tests/cargo/unsafe_.out b/charon/tests/cargo/unsafe_.out index 2144d3552..20d71b48b 100644 --- a/charon/tests/cargo/unsafe_.out +++ b/charon/tests/cargo/unsafe_.out @@ -3,11 +3,9 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, -// Full name: core::fmt::rt::{Arguments<'a>}::new_const -pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), N>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str +pub fn from_str<'a>(@1: &'static (Str)) -> Arguments<'a> = // Full name: std::io::stdio::_print @@ -30,30 +28,13 @@ fn main() let @0: (); // return let @1: (); // anonymous local let @2: Arguments<'_>; // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @7: Array<&'_ (Str), 1 : usize>; // anonymous local - - storage_live(@6) - storage_live(@7) - @7 := [const ("Hello, world!\n")] - @6 := &@7 - storage_live(@5) + @0 := () storage_live(@1) storage_live(@2) - storage_live(@3) - storage_live(@4) - @5 := move (@6) - @4 := &*(@5) - @3 := &*(@4) - @2 := new_const<'_, 1 : usize>(move (@3)) - storage_dead(@3) + @2 := from_str<'_>(const ("Hello, world!\n")) @1 := _print<'_>(move (@2)) storage_dead(@2) - storage_dead(@4) storage_dead(@1) @0 := () return diff --git a/charon/tests/ui/assoc-const-with-generics.out b/charon/tests/ui/assoc-const-with-generics.out index 4f802b6a5..90860363f 100644 --- a/charon/tests/ui/assoc-const-with-generics.out +++ b/charon/tests/ui/assoc-const-with-generics.out @@ -162,6 +162,9 @@ impl HasDefaultLen for Array<(), N> { non-dyn-compatible } +// Full name: test_crate::{impl HasDefaultLen for Array}::LEN +pub const {impl HasDefaultLen for Array}::LEN: usize = {impl HasDefaultLen for Array}::LEN() + // Full name: test_crate::{impl HasDefaultLen for Array}::LEN pub fn {impl HasDefaultLen for Array}::LEN() -> usize { @@ -173,15 +176,12 @@ pub fn {impl HasDefaultLen for Array}::LEN() -> usi if move (@1) { @0 := const (N) } else { - @0 := const ({impl HasDefaultLen for Array}::LEN) + @0 := copy ({impl HasDefaultLen for Array}::LEN) } storage_dead(@1) return } -// Full name: test_crate::{impl HasDefaultLen for Array}::LEN -pub const {impl HasDefaultLen for Array}::LEN: usize = {impl HasDefaultLen for Array}::LEN() - // Full name: test_crate::{impl HasDefaultLen for Array} impl HasDefaultLen for Array { parent_clause0 = {built_in impl MetaSized for Array} diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index e4e6ee8eb..202e50d30 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -41,8 +41,6 @@ impl Default for u32 { // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::marker::Destruct #[lang_item("destruct")] diff --git a/charon/tests/ui/copy_nonoverlapping.out b/charon/tests/ui/copy_nonoverlapping.out index 21f4a0932..fcc9043ad 100644 --- a/charon/tests/ui/copy_nonoverlapping.out +++ b/charon/tests/ui/copy_nonoverlapping.out @@ -4,6 +4,10 @@ #[lang_item("alloc_layout")] pub opaque type Layout +// Full name: core::alloc::layout::{Layout}::from_size_align_unchecked +pub unsafe fn from_size_align_unchecked(@1: usize, @2: usize) -> Layout += + // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -16,12 +20,6 @@ pub trait Sized non-dyn-compatible } -// Full name: core::alloc::layout::{Layout}::new -pub fn new() -> Layout -where - [@TraitClause0]: Sized, -= - // Full name: core::intrinsics::size_of pub fn size_of() -> usize where @@ -116,7 +114,7 @@ where { let @0: Layout; // return - @0 := new[@TraitClause0::parent_clause0]() + @0 := from_size_align_unchecked(const (@TraitClause0::SIZE), const (@TraitClause0::ALIGN)) return } diff --git a/charon/tests/ui/copy_nonoverlapping.rs b/charon/tests/ui/copy_nonoverlapping.rs index 29a5ce46a..043bd00c8 100644 --- a/charon/tests/ui/copy_nonoverlapping.rs +++ b/charon/tests/ui/copy_nonoverlapping.rs @@ -1,6 +1,7 @@ //@ charon-args=--extract-opaque-bodies //@ charon-args=--opaque core::ptr::copy_nonoverlapping::precondition_check //@ charon-args=--opaque core::alloc::layout::_::new +//@ charon-args=--opaque core::alloc::layout::_::from_size_align_unchecked //@ charon-args=--opaque core::alloc::layout::Layout use std::mem; diff --git a/charon/tests/ui/desugar_drops_to_calls.out b/charon/tests/ui/desugar_drops_to_calls.out index 42032f5ff..11ee8f184 100644 --- a/charon/tests/ui/desugar_drops_to_calls.out +++ b/charon/tests/ui/desugar_drops_to_calls.out @@ -3,11 +3,9 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, -// Full name: core::fmt::rt::{Arguments<'a>}::new_const -pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), N>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str +pub fn from_str<'a>(@1: &'static (Str)) -> Arguments<'a> = // Full name: core::marker::MetaSized @@ -219,30 +217,13 @@ pub fn {impl Drop for Point}::drop<'_0>(@1: &'_0 mut (Point)) let self@1: &'_ mut (Point); // arg #1 let @2: (); // anonymous local let @3: Arguments<'_>; // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @7: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @8: Array<&'_ (Str), 1 : usize>; // anonymous local - - storage_live(@7) - storage_live(@8) - @8 := [const ("Dropping Point\n")] - @7 := &@8 - storage_live(@6) + @0 := () storage_live(@2) storage_live(@3) - storage_live(@4) - storage_live(@5) - @6 := move (@7) - @5 := &*(@6) - @4 := &*(@5) - @3 := new_const<'_, 1 : usize>(move (@4)) - storage_dead(@4) + @3 := from_str<'_>(const ("Dropping Point\n")) @2 := _print<'_>(move (@3)) storage_dead(@3) - storage_dead(@5) storage_dead(@2) @0 := () return diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index a1ed321ea..d99a6f362 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -169,11 +169,11 @@ where struct test_crate::Join::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: Join<_dyn, T> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause0_2::parent_clause1::Left = Ty2 + @TraitClause0_2::parent_clause2::Right = Ty3)), - method_join_method: fn<'_0_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0_2]: Join<_dyn, T> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause0_2::parent_clause1::Left = Ty2 + @TraitClause0_2::parent_clause2::Right = Ty3))) -> (Ty2, Ty3), + drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: Join<_dyn, T> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause0_2::parent_clause2::Right = Ty2 + @TraitClause0_2::parent_clause1::Left = Ty3)), + method_join_method: fn<'_0_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0_2]: Join<_dyn, T> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause0_2::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause0_2::parent_clause2::Right = Ty2 + @TraitClause0_2::parent_clause1::Left = Ty3))) -> (Ty3, Ty2), 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 @@ -553,27 +553,27 @@ fn {impl Join for i32}::join_method<'_0>(@1: &'_0 (i32)) -> (i32, i32) } // Full name: test_crate::{impl Join for i32}::{vtable_drop_shim} -fn {impl Join for i32}::{vtable_drop_shim}(@1: *mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)) +fn {impl Join for i32}::{vtable_drop_shim}(@1: *mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)) { let ret@0: (); // return - let dyn_self@1: *mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32); // arg #1 + let dyn_self@1: *mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32); // arg #1 let target_self@2: *mut i32; // local ret@0 := () storage_live(target_self@2) - target_self@2 := concretize<*mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32), *mut i32>(move (dyn_self@1)) + target_self@2 := concretize<*mut (dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32), *mut i32>(move (dyn_self@1)) return } // 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 exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32))) -> (i32, i32) +fn {impl Join for i32}::join_method::{vtable_method}<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32))) -> (i32, i32) { let @0: (i32, i32); // return - let @1: &'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)); // arg #1 + let @1: &'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)); // arg #1 let @2: &'_0 (i32); // anonymous local storage_live(@2) - @2 := concretize<&'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)), &'_0 (i32)>(move (@1)) + @2 := concretize<&'_0 ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)), &'_0 (i32)>(move (@1)) @0 := {impl Join for i32}::join_method<'_0>(move (@2)) return } @@ -622,11 +622,11 @@ impl Join for i32 { fn main() { let @0: (); // return - let v@1: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)); // local + let v@1: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)); // local let @2: &'_ (i32); // anonymous local let @3: &'_ (i32); // anonymous local let @4: (i32, i32); // anonymous local - let @5: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)); // anonymous local + let @5: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)); // anonymous local let @6: &'_ (i32); // anonymous local let @7: &'_ (i32); // anonymous local let @8: i32; // anonymous local @@ -643,7 +643,7 @@ fn main() @6 := move (@7) @3 := &*(@6) @2 := &*(@3) - v@1 := unsize_cast<&'_ (i32), &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause1::Left = i32 + @TraitClause0_1::parent_clause2::Right = i32)), {impl Join for i32}>(move (@2)) + v@1 := unsize_cast<&'_ (i32), &'_ ((dyn exists<_dyn> [@TraitClause0_1]: Join<_dyn, i32> + _dyn : '_ + @TraitClause0_1::parent_clause1::parent_clause1::Internal = i32 + @TraitClause0_1::parent_clause2::Right = i32 + @TraitClause0_1::parent_clause1::Left = i32)), {impl Join for i32}>(move (@2)) storage_dead(@2) storage_dead(@3) storage_live(@4) diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out index 8325a73c4..0b2e6fcbc 100644 --- a/charon/tests/ui/gosim-demo.out +++ b/charon/tests/ui/gosim-demo.out @@ -121,8 +121,14 @@ pub struct Error {} // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, + +// Full name: core::fmt::rt::Argument +#[lang_item("format_argument")] +pub opaque type Argument<'a> + +// Full name: core::fmt::{Arguments<'a>}::new +pub unsafe fn new<'a, const N : usize, const M : usize>(@1: &'a (Array), @2: &'a (Array, M>)) -> Arguments<'a> += // Full name: core::result::Result #[lang_item("Result")] @@ -173,10 +179,6 @@ impl Debug for i32 { vtable: {impl Debug for i32}::{vtable} } -// Full name: core::fmt::rt::Argument -#[lang_item("format_argument")] -pub opaque type Argument<'a> - // Full name: core::fmt::rt::{Argument<'_0>}::new_debug pub fn new_debug<'_0, '_1, T>(@1: &'_1 (T)) -> Argument<'_1> where @@ -184,10 +186,6 @@ where [@TraitClause1]: Debug, = -// Full name: core::fmt::rt::{Arguments<'a>}::new_v1 -pub fn new_v1<'a, const P : usize, const A : usize>(@1: &'a (Array<&'static (Str), P>), @2: &'a (Array, A>)) -> Arguments<'a> -= - // Full name: core::iter::adapters::zip::TrustedRandomAccessNoCoerce pub trait TrustedRandomAccessNoCoerce { @@ -460,12 +458,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::slice::iter::Iter @@ -551,15 +549,14 @@ where let args@13: Array, 1 : usize>; // local let @14: Argument<'_>; // anonymous local let @15: &'_ (&'_ (T)); // anonymous local - let @16: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @17: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local + let @16: &'_ (Array); // anonymous local + let @17: &'_ (Array); // anonymous local let @18: &'_ (Array, 1 : usize>); // anonymous local let @19: &'_ (Array, 1 : usize>); // anonymous local - let @20: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @21: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @22: Array<&'_ (Str), 2 : usize>; // anonymous local + let @20: Array; // anonymous local + let @21: (); // anonymous local + let @22: &'_ (Array); // anonymous local - storage_live(@20) @0 := () storage_live(@2) storage_live(@3) @@ -595,23 +592,24 @@ where storage_live(@15) @15 := &*((args@11).0) @14 := new_debug<'_, '_, &'_ (T)>[{built_in impl Sized for &'_ (T)}, {impl Debug for &'_0 (T)}<'_, T>[@TraitClause1]](move (@15)) - storage_live(@21) - storage_live(@22) - @22 := [const ("- "), const ("\n")] - @21 := &@22 storage_dead(@15) args@13 := [move (@14)] storage_dead(@14) storage_live(@16) storage_live(@17) - @20 := move (@21) - @17 := &*(@20) + storage_live(@20) + @20 := [const (2 : u8), const (45 : u8), const (32 : u8), const (192 : u8), const (1 : u8), const (10 : u8), const (0 : u8)] + storage_live(@21) + @21 := () + storage_live(@22) + @22 := &@20 + @17 := move (@22) @16 := &*(@17) storage_live(@18) storage_live(@19) @19 := &args@13 @18 := &*(@19) - @10 := new_v1<'_, 2 : usize, 1 : usize>(move (@16), move (@18)) + @10 := new<'_, 7 : usize, 1 : usize>(move (@16), move (@18)) storage_dead(@19) storage_dead(@18) storage_dead(@17) diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index 2de9dd0c1..4764bec93 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -27,6 +27,15 @@ where [@TraitClause0]: Clone, = +// Full name: core::clone::TrivialClone +#[lang_item("trivial_clone")] +pub trait TrivialClone +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Clone + non-dyn-compatible +} + // Full name: core::marker::Copy #[lang_item("copy")] pub trait Copy @@ -78,6 +87,13 @@ impl Clone for Foo { non-dyn-compatible } +// Full name: test_crate::{impl TrivialClone for Foo} +impl TrivialClone for Foo { + parent_clause0 = {built_in impl MetaSized for Foo} + parent_clause1 = {impl Clone for Foo} + non-dyn-compatible +} + // Full name: test_crate::{impl Copy for Foo} impl Copy for Foo { parent_clause0 = {built_in impl MetaSized for Foo} diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out index 6b56b5ae4..459fc3689 100644 --- a/charon/tests/ui/issue-297-cfg.out +++ b/charon/tests/ui/issue-297-cfg.out @@ -410,12 +410,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::slice::iter::Chunks diff --git a/charon/tests/ui/issue-395-failed-to-normalize.out b/charon/tests/ui/issue-395-failed-to-normalize.out index 87344a49e..5fccd0ad4 100644 --- a/charon/tests/ui/issue-395-failed-to-normalize.out +++ b/charon/tests/ui/issue-395-failed-to-normalize.out @@ -389,12 +389,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } fn UNIT_METADATA() diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 0f12667a7..f5ab09f19 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -191,8 +191,6 @@ where // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::iter::adapters::zip::TrustedRandomAccessNoCoerce pub trait TrustedRandomAccessNoCoerce @@ -534,12 +532,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::panicking::AssertKind diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out index ccbebcb4b..8ce9ff61f 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -27,6 +27,15 @@ where [@TraitClause0]: Clone, = +// Full name: core::clone::TrivialClone +#[lang_item("trivial_clone")] +pub trait TrivialClone +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Clone + non-dyn-compatible +} + // Full name: core::marker::Copy #[lang_item("copy")] pub trait Copy @@ -88,6 +97,13 @@ impl Copy for Foo { non-dyn-compatible } +// Full name: test_crate::{impl TrivialClone for Foo} +impl TrivialClone for Foo { + parent_clause0 = {built_in impl MetaSized for Foo} + parent_clause1 = {impl Clone for Foo} + non-dyn-compatible +} + // Full name: test_crate::Ordering enum Ordering { Less, diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out index 1df242d4c..8b1cc0b71 100644 --- a/charon/tests/ui/iterator.out +++ b/charon/tests/ui/iterator.out @@ -339,12 +339,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::default::Default @@ -1651,8 +1651,6 @@ where // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::ops::arith::AddAssign #[lang_item("add_assign")] diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 459ab55f0..bbbac34c2 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -665,12 +665,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::slice::index::private_slice_index::Sealed diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out index 724a80552..a7082cbbe 100644 --- a/charon/tests/ui/monomorphization/dyn-trait.out +++ b/charon/tests/ui/monomorphization/dyn-trait.out @@ -19,28 +19,28 @@ error: `dyn Trait` is not yet supported with `--monomorphize` | ^ error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2866:1 + --> /rustc/library/alloc/src/string.rs:2851:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/marker.rs:178:1 + --> /rustc/library/core/src/marker.rs:179:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/core/src/fmt/mod.rs:1186:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/marker.rs:178:1 + --> /rustc/library/core/src/marker.rs:179:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/core/src/fmt/mod.rs:1186:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/core/src/fmt/mod.rs:1186:1 note: the error occurred when translating `core::fmt::Display::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -48,13 +48,13 @@ note: the error occurred when translating `core::fmt::Display:: /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/core/src/fmt/mod.rs:1186:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/fmt/mod.rs:1032:5 + --> /rustc/library/core/src/fmt/mod.rs:1211:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/core/src/fmt/mod.rs:1186:1 note: the error occurred when translating `core::fmt::Display::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -62,7 +62,7 @@ note: the error occurred when translating `core::fmt::Display:: /rustc/library/core/src/fmt/mod.rs:1032:5 + --> /rustc/library/core/src/fmt/mod.rs:1211:5 note: the error occurred when translating `core::fmt::Display::fmt::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -70,10 +70,10 @@ note: the error occurred when translating `core::fmt::Display::fmt:: /rustc/library/core/src/fmt/mod.rs:1032:5 + --> /rustc/library/core/src/fmt/mod.rs:1211:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/marker.rs:178:1 + --> /rustc/library/core/src/marker.rs:179:1 note: the error occurred when translating `core::marker::MetaSized::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -81,10 +81,10 @@ note: the error occurred when translating `core::marker::MetaSized:: /rustc/library/core/src/marker.rs:178:1 + --> /rustc/library/core/src/marker.rs:179:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/core/src/marker.rs:178:1 + --> /rustc/library/core/src/marker.rs:179:1 note: the error occurred when translating `core::marker::MetaSized::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -92,7 +92,7 @@ note: the error occurred when translating `core::marker::MetaSized:: /rustc/library/alloc/src/string.rs:2684:1 + --> /rustc/library/alloc/src/string.rs:2669:1 note: the error occurred when translating `alloc::string::{impl core::fmt::Display::}::{vtable}`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:12:27 @@ -100,40 +100,40 @@ note: the error occurred when translating `alloc::string::{impl core::fmt::Displ 12 | let _ = dyn_to_string(&str); | ---- error: Item `alloc::string::{impl#25}` caused errors; ignoring. - --> /rustc/library/alloc/src/string.rs:2684:1 + --> /rustc/library/alloc/src/string.rs:2669:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2866:1 + --> /rustc/library/alloc/src/string.rs:2851:1 note: the error occurred when translating `alloc::string::{impl#4}::`, which is (transitively) used at the following location(s): error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2841:1 + --> /rustc/library/alloc/src/string.rs:2826:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2866:1 + --> /rustc/library/alloc/src/string.rs:2851:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2841:1 + --> /rustc/library/alloc/src/string.rs:2826:1 note: the error occurred when translating `alloc::string::ToString::`, which is (transitively) used at the following location(s): error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2841:1 + --> /rustc/library/alloc/src/string.rs:2826:1 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2855:5 + --> /rustc/library/alloc/src/string.rs:2840:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2855:5 + --> /rustc/library/alloc/src/string.rs:2840:5 note: the error occurred when translating `alloc::string::ToString::to_string::`, which is (transitively) used at the following location(s): error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2855:5 + --> /rustc/library/alloc/src/string.rs:2840:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 note: the error occurred when translating `alloc::string::{impl alloc::string::ToString::}::to_string::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -141,10 +141,10 @@ note: the error occurred when translating `alloc::string::{impl alloc::string::T 7 | x.to_string() | ------------- error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 note: the error occurred when translating `alloc::string::{impl alloc::string::ToString::}::to_string::`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:7:5 @@ -152,6 +152,6 @@ note: the error occurred when translating `alloc::string::{impl alloc::string::T 7 | x.to_string() | ------------- error: `dyn Trait` is not yet supported with `--monomorphize` - --> /rustc/library/alloc/src/string.rs:2868:5 + --> /rustc/library/alloc/src/string.rs:2853:5 ERROR Charon failed to translate this code (34 errors) diff --git a/charon/tests/ui/panics.out b/charon/tests/ui/panics.out index 66dc242b3..8aa2b2229 100644 --- a/charon/tests/ui/panics.out +++ b/charon/tests/ui/panics.out @@ -3,19 +3,13 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, -// Full name: core::fmt::rt::Argument -#[lang_item("format_argument")] -pub opaque type Argument<'a> - -// Full name: core::fmt::rt::{Arguments<'a>}::new_const -pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), N>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str_nonconst +pub fn from_str_nonconst<'a>(@1: &'static (Str)) -> Arguments<'a> = -// Full name: core::fmt::rt::{Arguments<'a>}::new_v1 -pub fn new_v1<'a, const P : usize, const A : usize>(@1: &'a (Array<&'static (Str), P>), @2: &'a (Array, A>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str +pub fn from_str<'a>(@1: &'static (Str)) -> Arguments<'a> = fn UNIT_METADATA() @@ -42,26 +36,10 @@ fn panic2() { let @0: (); // return let @1: Arguments<'_>; // anonymous local - let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: Array<&'_ (Str), 1 : usize>; // anonymous local - - storage_live(@5) - storage_live(@6) - @6 := [const ("O no!")] - @5 := &@6 - storage_live(@4) + @0 := () storage_live(@1) - storage_live(@2) - storage_live(@3) - @4 := move (@5) - @3 := &*(@4) - @2 := &*(@3) - @1 := new_const<'_, 1 : usize>(move (@2)) - storage_dead(@2) + @1 := from_str<'_>(const ("O no!")) panic(core::panicking::panic_fmt) } @@ -70,42 +48,10 @@ fn panic3() { let @0: (); // return let @1: Arguments<'_>; // anonymous local - let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array, 0 : usize>); // anonymous local - let @5: &'_ (Array, 0 : usize>); // anonymous local - let @6: &'_ (Array, 0 : usize>); // anonymous local - let @7: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @8: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Array, 0 : usize>); // anonymous local - let @11: Array, 0 : usize>; // anonymous local - - storage_live(@8) - storage_live(@9) - @9 := [const ("O no!")] - @8 := &@9 - storage_live(@10) - storage_live(@11) - @11 := [] - @10 := &@11 - storage_live(@6) - storage_live(@7) + @0 := () storage_live(@1) - storage_live(@2) - storage_live(@3) - @7 := move (@8) - @3 := &*(@7) - @2 := &*(@3) - storage_live(@4) - storage_live(@5) - @6 := move (@10) - @5 := &*(@6) - @4 := &*(@5) - @1 := new_v1<'_, 1 : usize, 0 : usize>(move (@2), move (@4)) - storage_dead(@4) - storage_dead(@2) + @1 := from_str_nonconst<'_>(const ("O no!")) panic(core::panicking::panic_fmt) } @@ -130,30 +76,14 @@ fn panic5() let @0: (); // return let @1: bool; // anonymous local let @2: Arguments<'_>; // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @7: Array<&'_ (Str), 1 : usize>; // anonymous local - storage_live(@5) @0 := () storage_live(@1) @1 := const (false) if move (@1) { } else { - storage_live(@6) - storage_live(@7) - @7 := [const ("assert failed")] - @6 := &@7 storage_live(@2) - storage_live(@3) - storage_live(@4) - @5 := move (@6) - @4 := &*(@5) - @3 := &*(@4) - @2 := new_const<'_, 1 : usize>(move (@3)) - storage_dead(@3) + @2 := from_str<'_>(const ("assert failed")) panic(core::panicking::panic_fmt) } storage_dead(@1) @@ -175,42 +105,10 @@ fn panic7() { let @0: (); // return let @1: Arguments<'_>; // anonymous local - let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array, 0 : usize>); // anonymous local - let @5: &'_ (Array, 0 : usize>); // anonymous local - let @6: &'_ (Array, 0 : usize>); // anonymous local - let @7: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @8: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Array, 0 : usize>); // anonymous local - let @11: Array, 0 : usize>; // anonymous local - - storage_live(@8) - storage_live(@9) - @9 := [const ("internal error: entered unreachable code: can't reach this")] - @8 := &@9 - storage_live(@10) - storage_live(@11) - @11 := [] - @10 := &@11 - storage_live(@6) - storage_live(@7) + @0 := () storage_live(@1) - storage_live(@2) - storage_live(@3) - @7 := move (@8) - @3 := &*(@7) - @2 := &*(@3) - storage_live(@4) - storage_live(@5) - @6 := move (@10) - @5 := &*(@6) - @4 := &*(@5) - @1 := new_v1<'_, 1 : usize, 0 : usize>(move (@2), move (@4)) - storage_dead(@4) - storage_dead(@2) + @1 := from_str_nonconst<'_>(const ("internal error: entered unreachable code: can't reach this")) panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/plain-panic-str.out b/charon/tests/ui/plain-panic-str.out index bf2893a9e..0d944b716 100644 --- a/charon/tests/ui/plain-panic-str.out +++ b/charon/tests/ui/plain-panic-str.out @@ -3,11 +3,9 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, -// Full name: core::fmt::rt::{Arguments<'a>}::new_const -pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), N>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str +pub fn from_str<'a>(@1: &'static (Str)) -> Arguments<'a> = fn UNIT_METADATA() @@ -25,26 +23,10 @@ fn main() { let @0: (); // return let @1: Arguments<'_>; // anonymous local - let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: Array<&'_ (Str), 1 : usize>; // anonymous local - - storage_live(@5) - storage_live(@6) - @6 := [const ("O no")] - @5 := &@6 - storage_live(@4) + @0 := () storage_live(@1) - storage_live(@2) - storage_live(@3) - @4 := move (@5) - @3 := &*(@4) - @2 := &*(@3) - @1 := new_const<'_, 1 : usize>(move (@2)) - storage_dead(@2) + @1 := from_str<'_>(const ("O no")) panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index cf66a1413..f70c7deea 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -118,6 +118,7 @@ where = // Full name: core::hash::BuildHasher +#[lang_item("BuildHasher")] pub trait BuildHasher { parent_clause0 : [@TraitClause0]: MetaSized diff --git a/charon/tests/ui/ptr-offset.out b/charon/tests/ui/ptr-offset.out index 5f8438712..e895b3001 100644 --- a/charon/tests/ui/ptr-offset.out +++ b/charon/tests/ui/ptr-offset.out @@ -7,25 +7,6 @@ pub opaque type Layout // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, - -// Full name: core::fmt::rt::Count -#[lang_item("format_count")] -pub enum Count { - Is(u16), - Param(usize), - Implied, -} - -// Full name: core::fmt::rt::Placeholder -#[lang_item("format_placeholder")] -pub struct Placeholder { - position: usize, - flags: u32, - precision: Count, - width: Count, -} // Full name: core::fmt::rt::Argument #[lang_item("format_argument")] @@ -137,29 +118,13 @@ where non-dyn-compatible } -// Full name: core::option::Option -#[lang_item("Option")] -pub enum Option -where - [@TraitClause0]: Sized, -{ - None, - Some(T), -} - // Full name: core::panicking::panic_nounwind_fmt pub fn panic_nounwind_fmt<'_0>(@1: Arguments<'_0>, @2: bool) -> ! = -fn UNIT_METADATA() -{ - let @0: (); // return - - @0 := () - return -} - -const UNIT_METADATA: () = @Fun0() +// Full name: core::ptr::non_null::NonNull +#[lang_item("NonNull")] +pub opaque type NonNull // Full name: core::ptr::const_ptr::{*const T}::offset::precondition_check fn precondition_check(@1: *const (), @2: isize, @3: usize) @@ -169,106 +134,124 @@ fn precondition_check(@1: *const (), @2: isize, @3: usize) let count@2: isize; // arg #2 let size@3: usize; // arg #3 let @4: bool; // anonymous local - let @5: !; // anonymous local - let @6: Arguments<'_>; // anonymous local - let pieces@7: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @8: Array<&'_ (Str), 1 : usize>; // anonymous local - let rhs@9: isize; // local - let self@10: usize; // local - let @11: i64; // anonymous local - let b@12: bool; // local - let @13: (i64, bool); // anonymous local + let msg@5: &'_ (Str); // local + let @6: !; // anonymous local + let @7: Arguments<'_>; // anonymous local + let rhs@8: isize; // local + let self@9: usize; // local + let @10: i64; // anonymous local + let b@11: bool; // local + let @12: (i64, bool); // anonymous local + let @13: i64; // anonymous local let @14: i64; // anonymous local - let @15: i64; // anonymous local - let byte_offset@16: isize; // local - let @17: (); // anonymous local - let @18: usize; // anonymous local - let overflow@19: bool; // local + let byte_offset@15: isize; // local + let @16: (); // anonymous local + let @17: usize; // anonymous local + let overflow@18: bool; // local + let @19: bool; // anonymous local let @20: bool; // anonymous local - let @21: bool; // anonymous local - let @22: (u64, bool); // anonymous local + let @21: (u64, bool); // anonymous local + let @22: u64; // anonymous local let @23: u64; // anonymous local - let @24: u64; // anonymous local - let @25: &'_ (Slice<&'_ (Str)>); // anonymous local - let @26: &'_ (Slice>); // anonymous local - let @27: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local - - storage_live(@5) - storage_live(pieces@7) - storage_live(byte_offset@16) - storage_live(@17) + let @24: NonNull; // anonymous local + let @25: *const u8; // anonymous local + let @26: NonNull>; // anonymous local + let @27: usize; // anonymous local + let @28: usize; // anonymous local + let @29: usize; // anonymous local + let @30: *const Str; // anonymous local + let @31: &'_ (Slice); // anonymous local + + storage_live(msg@5) + storage_live(@6) + storage_live(byte_offset@15) + storage_live(@16) @0 := () storage_live(@4) - storage_live(overflow@19) - storage_live(rhs@9) - rhs@9 := cast(copy (size@3)) - storage_live(b@12) - storage_live(@11) + storage_live(overflow@18) + storage_live(rhs@8) + rhs@8 := cast(copy (size@3)) + storage_live(b@11) + storage_live(@10) + storage_live(@12) storage_live(@13) + @13 := cast(copy (count@2)) storage_live(@14) - @14 := cast(copy (count@2)) - storage_live(@15) - @15 := cast(copy (rhs@9)) - @13 := move (@14) checked.* move (@15) - storage_dead(@15) + @14 := cast(copy (rhs@8)) + @12 := move (@13) checked.* move (@14) storage_dead(@14) - @11 := copy ((@13).0) - b@12 := copy ((@13).1) storage_dead(@13) - byte_offset@16 := cast(copy (@11)) - storage_dead(@11) - if copy (b@12) { - @17 := cold_path() - storage_dead(b@12) - storage_dead(rhs@9) - storage_dead(overflow@19) + @10 := copy ((@12).0) + b@11 := copy ((@12).1) + storage_dead(@12) + byte_offset@15 := cast(copy (@10)) + storage_dead(@10) + if copy (b@11) { + @16 := cold_path() + storage_dead(b@11) + storage_dead(rhs@8) + storage_dead(overflow@18) } else { - storage_dead(b@12) - storage_dead(rhs@9) - storage_live(self@10) - self@10 := transmute<*const (), usize>(copy (this@1)) + storage_dead(b@11) + storage_dead(rhs@8) + storage_live(self@9) + self@9 := transmute<*const (), usize>(copy (this@1)) + storage_live(@20) + storage_live(@17) + @17 := cast(copy (byte_offset@15)) storage_live(@21) - storage_live(@18) - @18 := cast(copy (byte_offset@16)) storage_live(@22) + @22 := cast(copy (self@9)) storage_live(@23) - @23 := cast(copy (self@10)) - storage_live(@24) - @24 := cast(copy (@18)) - @22 := move (@23) checked.+ move (@24) - storage_dead(@24) + @23 := cast(copy (@17)) + @21 := move (@22) checked.+ move (@23) storage_dead(@23) - @21 := copy ((@22).1) storage_dead(@22) - storage_dead(@18) - storage_live(@20) - @20 := copy (byte_offset@16) < const (0 : isize) - overflow@19 := copy (@21) ^ move (@20) - storage_dead(@20) + @20 := copy ((@21).1) storage_dead(@21) - storage_dead(self@10) - @4 := ~(copy (overflow@19)) - storage_dead(overflow@19) + storage_dead(@17) + storage_live(@19) + @19 := copy (byte_offset@15) < const (0 : isize) + overflow@18 := copy (@20) ^ move (@19) + storage_dead(@19) + storage_dead(@20) + storage_dead(self@9) + @4 := ~(copy (overflow@18)) + storage_dead(overflow@18) if move (@4) { storage_dead(@4) return } else { } } - storage_live(@6) - storage_live(@8) - @8 := [const ("unsafe precondition(s) violated: ptr::offset requires the address calculation to not overflow\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@7 := &@8 + msg@5 := const ("unsafe precondition(s) violated: ptr::offset requires the address calculation to not overflow\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@7) + storage_live(@24) storage_live(@25) - @25 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@7)) + storage_live(@30) + @30 := &raw const *(msg@5) with_metadata(copy (msg@5.metadata)) + @25 := cast<*const Str, *const u8>(copy (@30)) + storage_dead(@30) + @24 := transmute<*const u8, NonNull>(copy (@25)) + storage_dead(@25) storage_live(@26) - @26 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(copy ({promoted_const}<'_, 1 : usize>)) storage_live(@27) - @27 := Option::None { } - @6 := Arguments { 0: copy (@25), 1: move (@27), 2: copy (@26) } + storage_live(@28) + storage_live(@29) + storage_live(@31) + @31 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: ptr::offset requires the address calculation to not overflow\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @29 := copy (@31.metadata) + storage_dead(@31) + @28 := move (@29) wrap.<< const (1 : i32) + storage_dead(@29) + @27 := move (@28) | const (1 : usize) + storage_dead(@28) + @26 := transmute>>(move (@27)) + storage_dead(@27) + @7 := Arguments { 0: move (@24), 1: move (@26) } storage_dead(@26) - storage_dead(@25) - @5 := panic_nounwind_fmt<'_>(move (@6), const (false)) + storage_dead(@24) + @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) } // Full name: core::ptr::const_ptr::{*const T}::offset @@ -303,6 +286,16 @@ where [@TraitClause0]: Sized, = +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::main fn main() { diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out index 761a0b873..d0a72d08a 100644 --- a/charon/tests/ui/quantified-clause.out +++ b/charon/tests/ui/quantified-clause.out @@ -389,12 +389,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::result::Result diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index 803c7aed5..fe303b621 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -185,23 +185,6 @@ impl Copy for usize { non-dyn-compatible } -// Full name: core::fmt::rt::Count -#[lang_item("format_count")] -pub enum Count { - Is(u16), - Param(usize), - Implied, -} - -// Full name: core::fmt::rt::Placeholder -#[lang_item("format_placeholder")] -pub struct Placeholder { - position: usize, - flags: u32, - precision: Count, - width: Count, -} - // Full name: core::ptr::non_null::NonNull #[lang_item("NonNull")] pub struct NonNull { @@ -240,25 +223,11 @@ pub struct Argument<'a> { // Full name: core::fmt::Arguments #[lang_item("format_arguments")] -pub struct Arguments<'a> -where - 'a : 'a, -{ - pieces: &'a (Slice<&'static (Str)>), - fmt: Option<&'a (Slice)>[{built_in impl Sized for &'_ (Slice)}], - args: &'a (Slice>), -} - -fn UNIT_METADATA() -{ - let @0: (); // return - - @0 := () - return +pub struct Arguments<'a> { + template: NonNull, + args: NonNull>, } -const UNIT_METADATA: () = @Fun0() - // Full name: core::panicking::panic_nounwind_fmt::compiletime fn compiletime<'_0>(@1: Arguments<'_0>, @2: bool) -> ! { @@ -294,48 +263,60 @@ fn core::ptr::alignment::{Alignment}::new_unchecked::precondition_check(@1: usiz { let @0: (); // return let align@1: usize; // arg #1 - let @2: !; // anonymous local - let @3: Arguments<'_>; // anonymous local - let pieces@4: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - let @6: u32; // anonymous local - let @7: &'_ (Slice<&'_ (Str)>); // anonymous local - let @8: &'_ (Slice>); // anonymous local - let @9: &'_ (Array, 0 : usize>); // anonymous local - let @10: Array, 0 : usize>; // anonymous local - let @11: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@2: &'_ (Str); // local + let @3: !; // anonymous local + let @4: Arguments<'_>; // anonymous local + let @5: u32; // anonymous local + let @6: NonNull; // anonymous local + let @7: *const u8; // anonymous local + let @8: NonNull>; // anonymous local + let @9: usize; // anonymous local + let @10: usize; // anonymous local + let @11: usize; // anonymous local + let @12: *const Str; // anonymous local + let @13: &'_ (Slice); // anonymous local - storage_live(@2) - storage_live(pieces@4) + storage_live(msg@2) + storage_live(@3) @0 := () - storage_live(@6) - @6 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](move (align@1)) - switch move (@6) { + storage_live(@5) + @5 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](move (align@1)) + switch move (@5) { 1 : u32 => { }, _ => { - storage_live(@9) - storage_live(@10) - @10 := [] - @9 := &@10 - storage_dead(@6) - storage_live(@3) - storage_live(@5) - @5 := [const ("unsafe precondition(s) violated: Alignment::new_unchecked requires a power of two\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@4 := &@5 + storage_dead(@5) + msg@2 := const ("unsafe precondition(s) violated: Alignment::new_unchecked requires a power of two\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@4) + storage_live(@6) storage_live(@7) - @7 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@4)) + storage_live(@12) + @12 := &raw const *(msg@2) with_metadata(copy (msg@2.metadata)) + @7 := cast<*const Str, *const u8>(copy (@12)) + storage_dead(@12) + @6 := transmute<*const u8, NonNull>(copy (@7)) + storage_dead(@7) storage_live(@8) - @8 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@9)) + storage_live(@9) + storage_live(@10) storage_live(@11) - @11 := Option::None { } - @3 := Arguments { pieces: copy (@7), fmt: move (@11), args: copy (@8) } + storage_live(@13) + @13 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: Alignment::new_unchecked requires a power of two\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @11 := copy (@13.metadata) + storage_dead(@13) + @10 := move (@11) wrap.<< const (1 : i32) + storage_dead(@11) + @9 := move (@10) | const (1 : usize) + storage_dead(@10) + @8 := transmute>>(move (@9)) + storage_dead(@9) + @4 := Arguments { template: move (@6), args: move (@8) } storage_dead(@8) - storage_dead(@7) - @2 := panic_nounwind_fmt<'_>(move (@3), const (false)) + storage_dead(@6) + @3 := panic_nounwind_fmt<'_>(move (@4), const (false)) }, } - storage_dead(@6) + storage_dead(@5) return } @@ -452,64 +433,297 @@ fn is_size_align_valid(@1: usize, @2: usize) -> bool return } -// Full name: core::mem::SizedTypeProperties -pub trait SizedTypeProperties -{ - parent_clause0 : [@TraitClause0]: Sized - const SIZE : usize - const ALIGN : usize - const IS_ZST : bool - const LAYOUT : Layout - const MAX_SLICE_LEN : usize - non-dyn-compatible -} - fn core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(@1: usize, @2: usize) { let @0: (); // return let size@1: usize; // arg #1 let align@2: usize; // arg #2 let @3: bool; // anonymous local - let @4: !; // anonymous local - let @5: Arguments<'_>; // anonymous local - let pieces@6: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @7: Array<&'_ (Str), 1 : usize>; // anonymous local - let @8: &'_ (Slice<&'_ (Str)>); // anonymous local - let @9: &'_ (Slice>); // anonymous local - let @10: &'_ (Array, 0 : usize>); // anonymous local - let @11: Array, 0 : usize>; // anonymous local - let @12: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@4: &'_ (Str); // local + let @5: !; // anonymous local + let @6: Arguments<'_>; // anonymous local + let @7: NonNull; // anonymous local + let @8: *const u8; // anonymous local + let @9: NonNull>; // anonymous local + let @10: usize; // anonymous local + let @11: usize; // anonymous local + let @12: usize; // anonymous local + let @13: *const Str; // anonymous local + let @14: &'_ (Slice); // anonymous local - storage_live(@4) - storage_live(pieces@6) + storage_live(msg@4) + storage_live(@5) @0 := () storage_live(@3) @3 := is_size_align_valid(move (size@1), move (align@2)) if move (@3) { } else { - storage_live(@10) - storage_live(@11) - @11 := [] - @10 := &@11 - storage_live(@5) + msg@4 := const ("unsafe precondition(s) violated: Layout::from_size_align_unchecked requires that align is a power of 2 and the rounded-up allocation size does not exceed isize::MAX\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@6) storage_live(@7) - @7 := [const ("unsafe precondition(s) violated: Layout::from_size_align_unchecked requires that align is a power of 2 and the rounded-up allocation size does not exceed isize::MAX\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@6 := &@7 storage_live(@8) - @8 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@6)) + storage_live(@13) + @13 := &raw const *(msg@4) with_metadata(copy (msg@4.metadata)) + @8 := cast<*const Str, *const u8>(copy (@13)) + storage_dead(@13) + @7 := transmute<*const u8, NonNull>(copy (@8)) + storage_dead(@8) storage_live(@9) - @9 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@10)) + storage_live(@10) + storage_live(@11) storage_live(@12) - @12 := Option::None { } - @5 := Arguments { pieces: copy (@8), fmt: move (@12), args: copy (@9) } + storage_live(@14) + @14 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: Layout::from_size_align_unchecked requires that align is a power of 2 and the rounded-up allocation size does not exceed isize::MAX\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @12 := copy (@14.metadata) + storage_dead(@14) + @11 := move (@12) wrap.<< const (1 : i32) + storage_dead(@12) + @10 := move (@11) | const (1 : usize) + storage_dead(@11) + @9 := transmute>>(move (@10)) + storage_dead(@10) + @6 := Arguments { template: move (@7), args: move (@9) } storage_dead(@9) - storage_dead(@8) - @4 := panic_nounwind_fmt<'_>(move (@5), const (false)) + storage_dead(@7) + @5 := panic_nounwind_fmt<'_>(move (@6), const (false)) + } + storage_dead(@3) + return +} + +// Full name: core::alloc::layout::{Layout}::from_size_align_unchecked +pub unsafe fn from_size_align_unchecked(@1: usize, @2: usize) -> Layout +{ + let @0: Layout; // return + let size@1: usize; // arg #1 + let align@2: usize; // arg #2 + let @3: bool; // anonymous local + let @4: (); // anonymous local + let @5: Alignment; // anonymous local + + storage_live(@4) + storage_live(@3) + @3 := ub_checks + if move (@3) { + @4 := core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(copy (size@1), copy (align@2)) + } else { } storage_dead(@3) + storage_live(@5) + @5 := transmute(copy (align@2)) + @0 := Layout { size: copy (size@1), align: move (@5) } + storage_dead(@5) + return +} + +// Full name: core::alloc::AllocError +pub struct AllocError {} + +// Full name: core::alloc::Allocator +pub trait Allocator +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn allocate<'_0_1> = core::alloc::Allocator::allocate<'_0_1, Self>[Self] + fn allocate_zeroed<'_0_1> = core::alloc::Allocator::allocate_zeroed<'_0_1, Self>[Self] + fn deallocate<'_0_1> = core::alloc::Allocator::deallocate<'_0_1, Self>[Self] + fn grow<'_0_1> = core::alloc::Allocator::grow<'_0_1, Self>[Self] + fn grow_zeroed<'_0_1> = core::alloc::Allocator::grow_zeroed<'_0_1, Self>[Self] + fn shrink<'_0_1> = core::alloc::Allocator::shrink<'_0_1, Self>[Self] + fn by_ref<'_0_1, [@TraitClause0_1]: Sized> = core::alloc::Allocator::by_ref<'_0_1, Self>[Self, @TraitClause0_1] + vtable: core::alloc::Allocator::{vtable} +} + +pub fn core::alloc::Allocator::allocate<'_0, Self>(@1: &'_0 (Self), @2: Layout) -> Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}] +where + [@TraitClause0]: Allocator, += + +// Full name: core::ops::control_flow::ControlFlow +#[lang_item("ControlFlow")] +pub enum ControlFlow +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + Continue(C), + Break(B), +} + +// Full name: core::convert::Infallible +pub enum Infallible { +} + +// Full name: core::ptr::const_ptr::{*const T}::is_aligned_to +pub fn is_aligned_to(@1: *const T, @2: usize) -> bool +{ + let @0: bool; // return + let self@1: *const T; // arg #1 + let align@2: usize; // arg #2 + let @3: Arguments<'_>; // anonymous local + let @4: usize; // anonymous local + let @5: usize; // anonymous local + let @6: usize; // anonymous local + let @7: u32; // anonymous local + let @8: *const (); // anonymous local + let s@9: &'_ (Str); // local + let @10: NonNull; // anonymous local + let @11: *const u8; // anonymous local + let @12: NonNull>; // anonymous local + let @13: usize; // anonymous local + let @14: usize; // anonymous local + let @15: usize; // anonymous local + let @16: *const Str; // anonymous local + let @17: &'_ (Slice); // anonymous local + + storage_live(@7) + @7 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy (align@2)) + switch move (@7) { + 1 : u32 => { + }, + _ => { + storage_dead(@7) + storage_live(@3) + storage_live(s@9) + s@9 := const ("is_aligned_to: align is not a power-of-two") + storage_live(@10) + storage_live(@11) + storage_live(@16) + @16 := &raw const *(s@9) with_metadata(copy (s@9.metadata)) + @11 := cast<*const Str, *const u8>(copy (@16)) + storage_dead(@16) + @10 := transmute<*const u8, NonNull>(copy (@11)) + storage_dead(@11) + storage_live(@12) + storage_live(@13) + storage_live(@14) + storage_live(@15) + storage_live(@17) + @17 := transmute<&'_ (Str), &'_ (Slice)>(const ("is_aligned_to: align is not a power-of-two")) + @15 := copy (@17.metadata) + storage_dead(@17) + @14 := move (@15) wrap.<< const (1 : i32) + storage_dead(@15) + @13 := move (@14) | const (1 : usize) + storage_dead(@14) + @12 := transmute>>(move (@13)) + storage_dead(@13) + @3 := Arguments { template: move (@10), args: move (@12) } + storage_dead(@12) + storage_dead(@10) + storage_dead(s@9) + panic(core::panicking::panic_fmt) + }, + } + storage_dead(@7) + storage_live(@4) + storage_live(@5) + storage_live(@8) + @8 := cast<*const T, *const ()>(copy (self@1)) + @5 := transmute<*const (), usize>(copy (@8)) + storage_dead(@8) + storage_live(@6) + @6 := copy (align@2) wrap.- const (1 : usize) + @4 := move (@5) & move (@6) + storage_dead(@6) + storage_dead(@5) + @0 := move (@4) == const (0 : usize) + storage_dead(@4) return } +fn core::ptr::write_bytes::precondition_check(@1: *const (), @2: usize, @3: bool) +{ + let @0: (); // return + let addr@1: *const (); // arg #1 + let align@2: usize; // arg #2 + let zero_size@3: bool; // arg #3 + let @4: bool; // anonymous local + let msg@5: &'_ (Str); // local + let @6: !; // anonymous local + let @7: Arguments<'_>; // anonymous local + let @8: bool; // anonymous local + let @9: bool; // anonymous local + let @10: usize; // anonymous local + let @11: NonNull; // anonymous local + let @12: *const u8; // anonymous local + let @13: NonNull>; // anonymous local + let @14: usize; // anonymous local + let @15: usize; // anonymous local + let @16: usize; // anonymous local + let @17: *const Str; // anonymous local + let @18: &'_ (Slice); // anonymous local + + storage_live(msg@5) + storage_live(@6) + @0 := () + storage_live(@4) + storage_live(@8) + @8 := is_aligned_to<()>(copy (addr@1), move (align@2)) + if move (@8) { + if copy (zero_size@3) { + storage_dead(@8) + storage_dead(@4) + return + } else { + storage_live(@9) + storage_live(@10) + @10 := transmute<*const (), usize>(copy (addr@1)) + @9 := move (@10) == const (0 : usize) + storage_dead(@10) + @4 := ~(move (@9)) + storage_dead(@9) + storage_dead(@8) + if move (@4) { + storage_dead(@4) + return + } else { + } + } + } else { + storage_dead(@8) + } + msg@5 := const ("unsafe precondition(s) violated: ptr::write_bytes requires that the destination pointer is aligned and non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@7) + storage_live(@11) + storage_live(@12) + storage_live(@17) + @17 := &raw const *(msg@5) with_metadata(copy (msg@5.metadata)) + @12 := cast<*const Str, *const u8>(copy (@17)) + storage_dead(@17) + @11 := transmute<*const u8, NonNull>(copy (@12)) + storage_dead(@12) + storage_live(@13) + storage_live(@14) + storage_live(@15) + storage_live(@16) + storage_live(@18) + @18 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: ptr::write_bytes requires that the destination pointer is aligned and non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @16 := copy (@18.metadata) + storage_dead(@18) + @15 := move (@16) wrap.<< const (1 : i32) + storage_dead(@16) + @14 := move (@15) | const (1 : usize) + storage_dead(@15) + @13 := transmute>>(move (@14)) + storage_dead(@14) + @7 := Arguments { template: move (@11), args: move (@13) } + storage_dead(@13) + storage_dead(@11) + @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) +} + +// Full name: core::mem::SizedTypeProperties +pub trait SizedTypeProperties +{ + parent_clause0 : [@TraitClause0]: Sized + const SIZE : usize + const ALIGN : usize + const IS_ZST : bool + const LAYOUT : Layout + const MAX_SLICE_LEN : usize + non-dyn-compatible +} + // Full name: core::intrinsics::size_of pub fn size_of() -> usize where @@ -585,6 +799,23 @@ 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 @@ -649,38 +880,8 @@ where [@TraitClause0]: SizedTypeProperties, = MAX_SLICE_LEN() -pub fn core::alloc::layout::{Layout}::new() -> Layout -where - [@TraitClause0]: Sized, -{ - let @0: Layout; // return - let @1: bool; // anonymous local - let @2: (); // anonymous local - let @3: Alignment; // anonymous local - let size@4: usize; // local - let align@5: usize; // local - - storage_live(@2) - storage_live(size@4) - storage_live(align@5) - size@4 := const ({impl SizedTypeProperties for T}[@TraitClause0]::SIZE) - align@5 := const ({impl SizedTypeProperties for T}[@TraitClause0]::ALIGN) - storage_live(@1) - @1 := ub_checks - if move (@1) { - @2 := core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(copy (size@4), copy (align@5)) - } else { - } - storage_dead(@1) - storage_live(@3) - @3 := transmute(copy (align@5)) - @0 := Layout { size: copy (size@4), align: move (@3) } - storage_dead(@3) - return -} - -// Full name: core::mem::{impl SizedTypeProperties for T} -impl SizedTypeProperties for T +// Full name: core::mem::{impl SizedTypeProperties for T} +impl SizedTypeProperties for T where [@TraitClause0]: Sized, { @@ -693,175 +894,6 @@ where non-dyn-compatible } -// Full name: core::mem::SizedTypeProperties::LAYOUT -pub const LAYOUT: Layout -where - [@TraitClause0]: SizedTypeProperties, - = LAYOUT() - -// Full name: core::mem::SizedTypeProperties::LAYOUT -pub fn LAYOUT() -> Layout -where - [@TraitClause0]: SizedTypeProperties, -{ - let @0: Layout; // return - - @0 := core::alloc::layout::{Layout}::new[@TraitClause0::parent_clause0]() - return -} - -// Full name: core::alloc::AllocError -pub struct AllocError {} - -// Full name: core::alloc::Allocator -pub trait Allocator -{ - parent_clause0 : [@TraitClause0]: MetaSized - fn allocate<'_0_1> = core::alloc::Allocator::allocate<'_0_1, Self>[Self] - fn allocate_zeroed<'_0_1> = core::alloc::Allocator::allocate_zeroed<'_0_1, Self>[Self] - fn deallocate<'_0_1> = core::alloc::Allocator::deallocate<'_0_1, Self>[Self] - fn grow<'_0_1> = core::alloc::Allocator::grow<'_0_1, Self>[Self] - fn grow_zeroed<'_0_1> = core::alloc::Allocator::grow_zeroed<'_0_1, Self>[Self] - fn shrink<'_0_1> = core::alloc::Allocator::shrink<'_0_1, Self>[Self] - fn by_ref<'_0_1, [@TraitClause0_1]: Sized> = core::alloc::Allocator::by_ref<'_0_1, Self>[Self, @TraitClause0_1] - vtable: core::alloc::Allocator::{vtable} -} - -pub fn core::alloc::Allocator::allocate<'_0, Self>(@1: &'_0 (Self), @2: Layout) -> Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}] -where - [@TraitClause0]: Allocator, -= - -// Full name: core::ops::control_flow::ControlFlow -#[lang_item("ControlFlow")] -pub enum ControlFlow -where - [@TraitClause0]: Sized, - [@TraitClause1]: Sized, -{ - Continue(C), - Break(B), -} - -// Full name: core::convert::Infallible -pub enum Infallible { -} - -fn core::ptr::write_bytes::precondition_check(@1: *const (), @2: usize, @3: bool) -{ - let @0: (); // return - let addr@1: *const (); // arg #1 - let align@2: usize; // arg #2 - let zero_size@3: bool; // arg #3 - let @4: bool; // anonymous local - let @5: !; // anonymous local - let @6: Arguments<'_>; // anonymous local - let pieces@7: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @8: Array<&'_ (Str), 1 : usize>; // anonymous local - let @9: bool; // anonymous local - let @10: Arguments<'_>; // anonymous local - let @11: usize; // anonymous local - let @12: usize; // anonymous local - let @13: usize; // anonymous local - let @14: u32; // anonymous local - let @15: &'_ (Slice<&'_ (Str)>); // anonymous local - let @16: &'_ (Slice>); // anonymous local - let @17: &'_ (Slice<&'_ (Str)>); // anonymous local - let @18: &'_ (Slice>); // anonymous local - let @19: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @20: Array<&'_ (Str), 1 : usize>; // anonymous local - let @21: &'_ (Array, 0 : usize>); // anonymous local - let @22: Array, 0 : usize>; // anonymous local - let @23: &'_ (Array, 0 : usize>); // anonymous local - let @24: Array, 0 : usize>; // anonymous local - let @25: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local - let @26: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local - - storage_live(@5) - storage_live(pieces@7) - @0 := () - storage_live(@4) - storage_live(@12) - storage_live(@14) - @14 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy (align@2)) - switch move (@14) { - 1 : u32 => { - }, - _ => { - storage_live(@19) - storage_live(@20) - @20 := [const ("is_aligned_to: align is not a power-of-two")] - @19 := &@20 - storage_live(@21) - storage_live(@22) - @22 := [] - @21 := &@22 - storage_dead(@14) - storage_live(@10) - storage_live(@15) - @15 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@19)) - storage_live(@16) - @16 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@21)) - storage_live(@25) - @25 := Option::None { } - @10 := Arguments { pieces: copy (@15), fmt: move (@25), args: copy (@16) } - storage_dead(@16) - storage_dead(@15) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@14) - storage_live(@11) - @12 := transmute<*const (), usize>(copy (addr@1)) - storage_live(@13) - @13 := copy (align@2) wrap.- const (1 : usize) - @11 := copy (@12) & move (@13) - storage_dead(@13) - switch move (@11) { - 0 : usize => { - storage_dead(@11) - if copy (zero_size@3) { - storage_dead(@12) - storage_dead(@4) - return - } else { - storage_live(@9) - @9 := copy (@12) == const (0 : usize) - @4 := ~(move (@9)) - storage_dead(@9) - storage_dead(@12) - if move (@4) { - storage_dead(@4) - return - } else { - } - } - }, - _ => { - storage_dead(@11) - storage_dead(@12) - }, - } - storage_live(@23) - storage_live(@24) - @24 := [] - @23 := &@24 - storage_live(@6) - storage_live(@8) - @8 := [const ("unsafe precondition(s) violated: ptr::write_bytes requires that the destination pointer is aligned and non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@7 := &@8 - storage_live(@17) - @17 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@7)) - storage_live(@18) - @18 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@23)) - storage_live(@26) - @26 := Option::None { } - @6 := Arguments { pieces: copy (@17), fmt: move (@26), args: copy (@18) } - storage_dead(@18) - storage_dead(@17) - @5 := panic_nounwind_fmt<'_>(move (@6), const (false)) -} - // Full name: core::intrinsics::write_bytes pub unsafe fn write_bytes(@1: *mut T, @2: u8, @3: usize) where @@ -974,29 +1006,44 @@ pub fn cold_path() return } -// Full name: core::fmt::rt::{Arguments<'a>}::new_const -pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), N>)) -> Arguments<'a> +// Full name: core::fmt::{Arguments<'a>}::from_str +pub fn from_str<'a>(@1: &'static (Str)) -> Arguments<'a> { let @0: Arguments<'_>; // return - let pieces@1: &'_ (Array<&'_ (Str), N>); // arg #1 - let @2: &'_ (Slice<&'_ (Str)>); // anonymous local - let @3: &'_ (Slice>); // anonymous local - let @4: &'_ (Array, 0 : usize>); // anonymous local - let @5: Array, 0 : usize>; // anonymous local - let @6: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let s@1: &'_ (Str); // arg #1 + let @2: NonNull; // anonymous local + let @3: *const u8; // anonymous local + let @4: NonNull>; // anonymous local + let @5: usize; // anonymous local + let @6: usize; // anonymous local + let @7: usize; // anonymous local + let @8: *const Str; // anonymous local + let @9: &'_ (Slice); // anonymous local - storage_live(@4) - storage_live(@5) - @5 := [] - @4 := &@5 storage_live(@2) - @2 := @ArrayToSliceShared<'_, &'_ (Str), N>(copy (pieces@1)) storage_live(@3) - @3 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@4)) - storage_live(@6) - @6 := Option::None { } - @0 := Arguments { pieces: copy (@2), fmt: move (@6), args: copy (@3) } + storage_live(@8) + @8 := &raw const *(s@1) with_metadata(copy (s@1.metadata)) + @3 := cast<*const Str, *const u8>(copy (@8)) + storage_dead(@8) + @2 := transmute<*const u8, NonNull>(copy (@3)) storage_dead(@3) + storage_live(@4) + storage_live(@5) + storage_live(@6) + storage_live(@7) + storage_live(@9) + @9 := transmute<&'_ (Str), &'_ (Slice)>(copy (s@1)) + @7 := copy (@9.metadata) + storage_dead(@9) + @6 := move (@7) wrap.<< const (1 : i32) + storage_dead(@7) + @5 := move (@6) | const (1 : usize) + storage_dead(@6) + @4 := transmute>>(move (@5)) + storage_dead(@5) + @0 := Arguments { template: move (@2), args: move (@4) } + storage_dead(@4) storage_dead(@2) return } @@ -1009,23 +1056,13 @@ pub fn panic_nounwind(@1: &'static (Str)) -> ! let expr@1: &'_ (Str); // arg #1 let @2: !; // anonymous local let @3: Arguments<'_>; // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: Array<&'_ (Str), 1 : usize>; // anonymous local - let @7: &'_ (Str); // anonymous local + let @4: &'_ (Str); // anonymous local storage_live(@2) storage_live(@3) storage_live(@4) - storage_live(@5) - storage_live(@6) - storage_live(@7) - @7 := copy (expr@1) - @6 := [move (@7)] - storage_dead(@7) - @5 := &@6 - @4 := &*(@5) - @3 := new_const<'_, 1 : usize>(move (@4)) + @4 := copy (expr@1) + @3 := from_str<'_>(move (@4)) storage_dead(@4) @2 := panic_nounwind_fmt<'_>(move (@3), const (false)) } @@ -1118,560 +1155,116 @@ fn core::ptr::copy_nonoverlapping::precondition_check(@1: *const (), @2: *mut () let is_zst@10: bool; // local let @11: bool; // anonymous local let ptr@12: *const (); // local - let @13: !; // anonymous local - let @14: Arguments<'_>; // anonymous local - let pieces@15: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @16: Array<&'_ (Str), 1 : usize>; // anonymous local + let msg@13: &'_ (Str); // local + let @14: !; // anonymous local + let @15: Arguments<'_>; // anonymous local + let @16: bool; // anonymous local let @17: bool; // anonymous local - let @18: Arguments<'_>; // anonymous local - let @19: usize; // anonymous local - let @20: usize; // anonymous local + let @18: usize; // anonymous local + let @19: bool; // anonymous local + let @20: bool; // anonymous local let @21: usize; // anonymous local - let @22: u32; // anonymous local - let @23: &'_ (Slice<&'_ (Str)>); // anonymous local - let @24: &'_ (Slice>); // anonymous local - let @25: bool; // anonymous local - let @26: Arguments<'_>; // anonymous local + let @22: NonNull; // anonymous local + let @23: *const u8; // anonymous local + let @24: NonNull>; // anonymous local + let @25: usize; // anonymous local + let @26: usize; // anonymous local let @27: usize; // anonymous local - let @28: usize; // anonymous local - let @29: u32; // anonymous local - let @30: &'_ (Slice<&'_ (Str)>); // anonymous local - let @31: &'_ (Slice>); // anonymous local - let @32: &'_ (Slice<&'_ (Str)>); // anonymous local - let @33: &'_ (Slice>); // anonymous local - let @34: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @35: Array<&'_ (Str), 1 : usize>; // anonymous local - let @36: &'_ (Array, 0 : usize>); // anonymous local - let @37: Array, 0 : usize>; // anonymous local - let @38: &'_ (Array, 0 : usize>); // anonymous local - let @39: Array, 0 : usize>; // anonymous local - let @40: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @41: Array<&'_ (Str), 1 : usize>; // anonymous local - let @42: &'_ (Array, 0 : usize>); // anonymous local - let @43: Array, 0 : usize>; // anonymous local - let @44: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local - let @45: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local - let @46: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let @28: *const Str; // anonymous local + let @29: &'_ (Slice); // anonymous local storage_live(zero_size@7) storage_live(ptr@12) - storage_live(@13) - storage_live(pieces@15) - storage_live(@21) + storage_live(msg@13) + storage_live(@14) @0 := () storage_live(@6) switch copy (count@5) { 0 : usize => { - }, - _ => { - zero_size@7 := copy (size@3) == const (0 : usize) + zero_size@7 := const (true) storage_live(@8) storage_live(align@9) align@9 := copy (align@4) storage_live(is_zst@10) is_zst@10 := copy (zero_size@7) - storage_live(@20) - storage_live(@22) - @22 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy (align@4)) - switch move (@22) { - 1 : u32 => { - }, - _ => { - storage_live(@34) - storage_live(@35) - @35 := [const ("is_aligned_to: align is not a power-of-two")] - @34 := &@35 - storage_live(@36) - storage_live(@37) - @37 := [] - @36 := &@37 - storage_dead(@22) - storage_live(@18) - storage_live(@23) - @23 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@34)) - storage_live(@24) - @24 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@36)) - storage_live(@44) - @44 := Option::None { } - @18 := Arguments { pieces: copy (@23), fmt: move (@44), args: copy (@24) } - storage_dead(@24) - storage_dead(@23) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@22) - storage_live(@19) - @20 := transmute<*const (), usize>(copy (src@1)) - @21 := copy (align@4) wrap.- const (1 : usize) - @19 := copy (@20) & copy (@21) - switch move (@19) { - 0 : usize => { - storage_dead(@19) - if copy (is_zst@10) { - storage_dead(@20) - storage_dead(is_zst@10) - storage_dead(align@9) - storage_live(@11) - ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) - storage_live(@28) - storage_live(@29) - @29 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](move (align@4)) - switch move (@29) { - 1 : u32 => { - }, - _ => { - storage_live(@40) - storage_live(@41) - @41 := [const ("is_aligned_to: align is not a power-of-two")] - @40 := &@41 - storage_live(@42) - storage_live(@43) - @43 := [] - @42 := &@43 - storage_dead(@29) - storage_live(@26) - storage_live(@30) - @30 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@40)) - storage_live(@31) - @31 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@42)) - storage_live(@46) - @46 := Option::None { } - @26 := Arguments { pieces: copy (@30), fmt: move (@46), args: copy (@31) } - storage_dead(@31) - storage_dead(@30) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@29) - storage_live(@27) - @28 := transmute<*mut (), usize>(copy (dst@2)) - @27 := copy (@28) & copy (@21) - switch move (@27) { - 0 : usize => { - storage_dead(@27) - if copy (zero_size@7) { - storage_dead(@28) - @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) - storage_dead(@11) - storage_dead(@8) - if move (@6) { - storage_dead(@6) - return - } else { - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } else { - storage_live(@25) - @25 := copy (@28) == const (0 : usize) - @11 := ~(move (@25)) - storage_dead(@25) - storage_dead(@28) - if move (@11) { - @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) - storage_dead(@11) - storage_dead(@8) - if move (@6) { - storage_dead(@6) - return - } else { - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } else { - storage_dead(@11) - storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } - }, - _ => { - storage_dead(@27) - storage_dead(@28) - storage_dead(@11) - storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - }, + storage_live(@16) + @16 := is_aligned_to<()>(copy (src@1), copy (align@4)) + if move (@16) { + storage_dead(@16) + storage_dead(is_zst@10) + storage_dead(align@9) + storage_live(@11) + ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) + storage_live(@19) + @19 := is_aligned_to<()>(copy (ptr@12), move (align@4)) + if move (@19) { + if copy (zero_size@7) { + storage_dead(@19) + @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) + storage_dead(@11) + storage_dead(@8) + if move (@6) { + storage_dead(@6) + return + } else { } } else { - storage_live(@17) - @17 := copy (@20) == const (0 : usize) - @8 := ~(move (@17)) - storage_dead(@17) + storage_live(@20) + storage_live(@21) + @21 := transmute<*mut (), usize>(copy (dst@2)) + @20 := move (@21) == const (0 : usize) + storage_dead(@21) + @11 := ~(move (@20)) storage_dead(@20) - if move (@8) { - storage_dead(is_zst@10) - storage_dead(align@9) - storage_live(@11) - ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) - storage_live(@28) - storage_live(@29) - @29 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](move (align@4)) - switch move (@29) { - 1 : u32 => { - }, - _ => { - storage_live(@40) - storage_live(@41) - @41 := [const ("is_aligned_to: align is not a power-of-two")] - @40 := &@41 - storage_live(@42) - storage_live(@43) - @43 := [] - @42 := &@43 - storage_dead(@29) - storage_live(@26) - storage_live(@30) - @30 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@40)) - storage_live(@31) - @31 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@42)) - storage_live(@46) - @46 := Option::None { } - @26 := Arguments { pieces: copy (@30), fmt: move (@46), args: copy (@31) } - storage_dead(@31) - storage_dead(@30) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@29) - storage_live(@27) - @28 := transmute<*mut (), usize>(copy (dst@2)) - @27 := copy (@28) & copy (@21) - switch move (@27) { - 0 : usize => { - storage_dead(@27) - if copy (zero_size@7) { - storage_dead(@28) - @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) - storage_dead(@11) - storage_dead(@8) - if move (@6) { - storage_dead(@6) - return - } else { - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } else { - storage_live(@25) - @25 := copy (@28) == const (0 : usize) - @11 := ~(move (@25)) - storage_dead(@25) - storage_dead(@28) - if move (@11) { - @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) - storage_dead(@11) - storage_dead(@8) - if move (@6) { - storage_dead(@6) - return - } else { - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } else { - storage_dead(@11) - storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - } - } - }, - _ => { - storage_dead(@27) - storage_dead(@28) - storage_dead(@11) - storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - }, + storage_dead(@19) + if move (@11) { + @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) + storage_dead(@11) + storage_dead(@8) + if move (@6) { + storage_dead(@6) + return + } else { } } else { - storage_dead(is_zst@10) - storage_dead(align@9) storage_dead(@11) storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) } } - }, - _ => { + } else { storage_dead(@19) - storage_dead(@20) - storage_dead(is_zst@10) - storage_dead(align@9) storage_dead(@11) storage_dead(@8) - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) - }, - } - }, - } - zero_size@7 := const (true) - storage_live(@8) - storage_live(align@9) - align@9 := copy (align@4) - storage_live(is_zst@10) - is_zst@10 := copy (zero_size@7) - storage_live(@20) - storage_live(@22) - @22 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](copy (align@4)) - switch move (@22) { - 1 : u32 => { - }, - _ => { - storage_live(@34) - storage_live(@35) - @35 := [const ("is_aligned_to: align is not a power-of-two")] - @34 := &@35 - storage_live(@36) - storage_live(@37) - @37 := [] - @36 := &@37 - storage_dead(@22) - storage_live(@18) - storage_live(@23) - @23 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@34)) - storage_live(@24) - @24 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@36)) - storage_live(@44) - @44 := Option::None { } - @18 := Arguments { pieces: copy (@23), fmt: move (@44), args: copy (@24) } - storage_dead(@24) - storage_dead(@23) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@22) - storage_live(@19) - @20 := transmute<*const (), usize>(copy (src@1)) - @21 := copy (align@4) wrap.- const (1 : usize) - @19 := copy (@20) & copy (@21) - switch move (@19) { - 0 : usize => { - storage_dead(@19) - storage_dead(@20) - storage_dead(is_zst@10) - storage_dead(align@9) - storage_live(@11) - ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) - storage_live(@28) - storage_live(@29) - @29 := ctpop[{built_in impl Sized for usize}, {impl Copy for usize}](move (align@4)) - switch move (@29) { - 1 : u32 => { - }, - _ => { - storage_live(@40) - storage_live(@41) - @41 := [const ("is_aligned_to: align is not a power-of-two")] - @40 := &@41 - storage_live(@42) - storage_live(@43) - @43 := [] - @42 := &@43 - storage_dead(@29) - storage_live(@26) - storage_live(@30) - @30 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@40)) - storage_live(@31) - @31 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@42)) - storage_live(@46) - @46 := Option::None { } - @26 := Arguments { pieces: copy (@30), fmt: move (@46), args: copy (@31) } - storage_dead(@31) - storage_dead(@30) - panic(core::panicking::panic_fmt) - }, - } - storage_dead(@29) - storage_live(@27) - @28 := transmute<*mut (), usize>(copy (dst@2)) - @27 := copy (@28) & copy (@21) - switch move (@27) { - 0 : usize => { - storage_dead(@27) - if copy (zero_size@7) { - storage_dead(@28) - @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) - storage_dead(@11) - storage_dead(@8) - if move (@6) { - storage_dead(@6) - return - } else { - } - } else { - storage_live(@25) - @25 := copy (@28) == const (0 : usize) - @11 := ~(move (@25)) - storage_dead(@25) - storage_dead(@28) - if move (@11) { + } + } else { + storage_dead(@16) + storage_dead(is_zst@10) + storage_dead(align@9) + storage_dead(@11) + storage_dead(@8) + } + }, + _ => { + zero_size@7 := copy (size@3) == const (0 : usize) + storage_live(@8) + storage_live(align@9) + align@9 := copy (align@4) + storage_live(is_zst@10) + is_zst@10 := copy (zero_size@7) + storage_live(@16) + @16 := is_aligned_to<()>(copy (src@1), copy (align@4)) + if move (@16) { + if copy (is_zst@10) { + storage_dead(@16) + storage_dead(is_zst@10) + storage_dead(align@9) + storage_live(@11) + ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) + storage_live(@19) + @19 := is_aligned_to<()>(copy (ptr@12), move (align@4)) + if move (@19) { + if copy (zero_size@7) { + storage_dead(@19) @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) storage_dead(@11) storage_dead(@8) @@ -1681,46 +1274,132 @@ fn core::ptr::copy_nonoverlapping::precondition_check(@1: *const (), @2: *mut () } else { } } else { + storage_live(@20) + storage_live(@21) + @21 := transmute<*mut (), usize>(copy (dst@2)) + @20 := move (@21) == const (0 : usize) + storage_dead(@21) + @11 := ~(move (@20)) + storage_dead(@20) + storage_dead(@19) + if move (@11) { + @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) + storage_dead(@11) + storage_dead(@8) + if move (@6) { + storage_dead(@6) + return + } else { + } + } else { + storage_dead(@11) + storage_dead(@8) + } + } + } else { + storage_dead(@19) + storage_dead(@11) + storage_dead(@8) + } + } else { + storage_live(@17) + storage_live(@18) + @18 := transmute<*const (), usize>(copy (src@1)) + @17 := move (@18) == const (0 : usize) + storage_dead(@18) + @8 := ~(move (@17)) + storage_dead(@17) + storage_dead(@16) + if move (@8) { + storage_dead(is_zst@10) + storage_dead(align@9) + storage_live(@11) + ptr@12 := cast<*mut (), *const ()>(copy (dst@2)) + storage_live(@19) + @19 := is_aligned_to<()>(copy (ptr@12), move (align@4)) + if move (@19) { + if copy (zero_size@7) { + storage_dead(@19) + @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) + storage_dead(@11) + storage_dead(@8) + if move (@6) { + storage_dead(@6) + return + } else { + } + } else { + storage_live(@20) + storage_live(@21) + @21 := transmute<*mut (), usize>(copy (dst@2)) + @20 := move (@21) == const (0 : usize) + storage_dead(@21) + @11 := ~(move (@20)) + storage_dead(@20) + storage_dead(@19) + if move (@11) { + @6 := runtime(move (src@1), move (ptr@12), move (size@3), move (count@5)) + storage_dead(@11) + storage_dead(@8) + if move (@6) { + storage_dead(@6) + return + } else { + } + } else { + storage_dead(@11) + storage_dead(@8) + } + } + } else { + storage_dead(@19) storage_dead(@11) storage_dead(@8) } + } else { + storage_dead(is_zst@10) + storage_dead(align@9) + storage_dead(@11) + storage_dead(@8) } - }, - _ => { - storage_dead(@27) - storage_dead(@28) - storage_dead(@11) - storage_dead(@8) - }, + } + } else { + storage_dead(@16) + storage_dead(is_zst@10) + storage_dead(align@9) + storage_dead(@11) + storage_dead(@8) } }, - _ => { - storage_dead(@19) - storage_dead(@20) - storage_dead(is_zst@10) - storage_dead(align@9) - storage_dead(@11) - storage_dead(@8) - }, } - storage_live(@38) - storage_live(@39) - @39 := [] - @38 := &@39 - storage_live(@14) - storage_live(@16) - @16 := [const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@15 := &@16 - storage_live(@32) - @32 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@15)) - storage_live(@33) - @33 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@38)) - storage_live(@45) - @45 := Option::None { } - @14 := Arguments { pieces: copy (@32), fmt: move (@45), args: copy (@33) } - storage_dead(@33) - storage_dead(@32) - @13 := panic_nounwind_fmt<'_>(move (@14), const (false)) + msg@13 := const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@15) + storage_live(@22) + storage_live(@23) + storage_live(@28) + @28 := &raw const *(msg@13) with_metadata(copy (msg@13.metadata)) + @23 := cast<*const Str, *const u8>(copy (@28)) + storage_dead(@28) + @22 := transmute<*const u8, NonNull>(copy (@23)) + storage_dead(@23) + storage_live(@24) + storage_live(@25) + storage_live(@26) + storage_live(@27) + storage_live(@29) + @29 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @27 := copy (@29.metadata) + storage_dead(@29) + @26 := move (@27) wrap.<< const (1 : i32) + storage_dead(@27) + @25 := move (@26) | const (1 : usize) + storage_dead(@26) + @24 := transmute>>(move (@25)) + storage_dead(@25) + @15 := Arguments { template: move (@22), args: move (@24) } + storage_dead(@24) + storage_dead(@22) + @14 := panic_nounwind_fmt<'_>(move (@15), const (false)) } pub unsafe fn core::alloc::Allocator::grow<'_0, Self>(@1: &'_0 (Self), @2: NonNull, @3: Layout, @4: Layout) -> Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}] @@ -2117,88 +1796,112 @@ fn core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(@1: *mut { let @0: (); // return let ptr@1: *mut (); // arg #1 - let @2: !; // anonymous local - let @3: Arguments<'_>; // anonymous local - let pieces@4: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - let @6: usize; // anonymous local - let @7: &'_ (Slice<&'_ (Str)>); // anonymous local - let @8: &'_ (Slice>); // anonymous local - let @9: &'_ (Array, 0 : usize>); // anonymous local - let @10: Array, 0 : usize>; // anonymous local - let @11: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@2: &'_ (Str); // local + let @3: !; // anonymous local + let @4: Arguments<'_>; // anonymous local + let @5: usize; // anonymous local + let @6: NonNull; // anonymous local + let @7: *const u8; // anonymous local + let @8: NonNull>; // anonymous local + let @9: usize; // anonymous local + let @10: usize; // anonymous local + let @11: usize; // anonymous local + let @12: *const Str; // anonymous local + let @13: &'_ (Slice); // anonymous local - storage_live(@2) - storage_live(pieces@4) + storage_live(msg@2) + storage_live(@3) @0 := () - storage_live(@6) - @6 := transmute<*mut (), usize>(copy (ptr@1)) - switch move (@6) { + storage_live(@5) + @5 := transmute<*mut (), usize>(copy (ptr@1)) + switch move (@5) { 0 : usize => { }, _ => { - storage_dead(@6) + storage_dead(@5) return }, } - storage_live(@9) - storage_live(@10) - @10 := [] - @9 := &@10 - storage_dead(@6) - storage_live(@3) - storage_live(@5) - @5 := [const ("unsafe precondition(s) violated: NonNull::new_unchecked requires that the pointer is non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@4 := &@5 + storage_dead(@5) + msg@2 := const ("unsafe precondition(s) violated: NonNull::new_unchecked requires that the pointer is non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@4) + storage_live(@6) storage_live(@7) - @7 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@4)) + storage_live(@12) + @12 := &raw const *(msg@2) with_metadata(copy (msg@2.metadata)) + @7 := cast<*const Str, *const u8>(copy (@12)) + storage_dead(@12) + @6 := transmute<*const u8, NonNull>(copy (@7)) + storage_dead(@7) storage_live(@8) - @8 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@9)) + storage_live(@9) + storage_live(@10) storage_live(@11) - @11 := Option::None { } - @3 := Arguments { pieces: copy (@7), fmt: move (@11), args: copy (@8) } + storage_live(@13) + @13 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: NonNull::new_unchecked requires that the pointer is non-null\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @11 := copy (@13.metadata) + storage_dead(@13) + @10 := move (@11) wrap.<< const (1 : i32) + storage_dead(@11) + @9 := move (@10) | const (1 : usize) + storage_dead(@10) + @8 := transmute>>(move (@9)) + storage_dead(@9) + @4 := Arguments { template: move (@6), args: move (@8) } storage_dead(@8) - storage_dead(@7) - @2 := panic_nounwind_fmt<'_>(move (@3), const (false)) + storage_dead(@6) + @3 := panic_nounwind_fmt<'_>(move (@4), const (false)) } fn core::hint::assert_unchecked::precondition_check(@1: bool) { let @0: (); // return let cond@1: bool; // arg #1 - let @2: !; // anonymous local - let @3: Arguments<'_>; // anonymous local - let pieces@4: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - let @6: &'_ (Slice<&'_ (Str)>); // anonymous local - let @7: &'_ (Slice>); // anonymous local - let @8: &'_ (Array, 0 : usize>); // anonymous local - let @9: Array, 0 : usize>; // anonymous local - let @10: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@2: &'_ (Str); // local + let @3: !; // anonymous local + let @4: Arguments<'_>; // anonymous local + let @5: NonNull; // anonymous local + let @6: *const u8; // anonymous local + let @7: NonNull>; // anonymous local + let @8: usize; // anonymous local + let @9: usize; // anonymous local + let @10: usize; // anonymous local + let @11: *const Str; // anonymous local + let @12: &'_ (Slice); // anonymous local - storage_live(@2) - storage_live(pieces@4) + storage_live(msg@2) + storage_live(@3) @0 := () if copy (cond@1) { } else { - storage_live(@8) - storage_live(@9) - @9 := [] - @8 := &@9 - storage_live(@3) + msg@2 := const ("unsafe precondition(s) violated: hint::assert_unchecked must never be called when the condition is false\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@4) storage_live(@5) - @5 := [const ("unsafe precondition(s) violated: hint::assert_unchecked must never be called when the condition is false\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@4 := &@5 storage_live(@6) - @6 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@4)) + storage_live(@11) + @11 := &raw const *(msg@2) with_metadata(copy (msg@2.metadata)) + @6 := cast<*const Str, *const u8>(copy (@11)) + storage_dead(@11) + @5 := transmute<*const u8, NonNull>(copy (@6)) + storage_dead(@6) storage_live(@7) - @7 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@8)) + storage_live(@8) + storage_live(@9) storage_live(@10) - @10 := Option::None { } - @3 := Arguments { pieces: copy (@6), fmt: move (@10), args: copy (@7) } + storage_live(@12) + @12 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: hint::assert_unchecked must never be called when the condition is false\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @10 := copy (@12.metadata) + storage_dead(@12) + @9 := move (@10) wrap.<< const (1 : i32) + storage_dead(@10) + @8 := move (@9) | const (1 : usize) + storage_dead(@9) + @7 := transmute>>(move (@8)) + storage_dead(@8) + @4 := Arguments { template: move (@5), args: move (@7) } storage_dead(@7) - storage_dead(@6) - @2 := panic_nounwind_fmt<'_>(move (@3), const (false)) + storage_dead(@5) + @3 := panic_nounwind_fmt<'_>(move (@4), const (false)) } return } @@ -3000,12 +2703,15 @@ pub unsafe fn {impl Allocator for Global}::shrink<'_0>(@1: &'_0 (Global), @2: No let @65: bool; // anonymous local let @66: usize; // anonymous local let @67: AllocError; // anonymous local - let @68: Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}]; // anonymous local - let @69: Option>[{built_in impl Sized for NonNull}]; // anonymous local - let @70: AllocError; // anonymous local - let @71: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local - let @72: AllocError; // anonymous local - let @73: Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}]; // anonymous local + let @68: Result[{built_in impl Sized for Infallible}, {built_in impl Sized for AllocError}]; // anonymous local + let @69: 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 @70: Option>[{built_in impl Sized for NonNull}]; // anonymous local + let @71: AllocError; // anonymous local + let @72: Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}]; // anonymous local + let @73: AllocError; // anonymous local + let @74: Result, AllocError>[{built_in impl Sized for NonNull}, {built_in impl Sized for AllocError}]; // anonymous local + let @75: AllocError; // anonymous local + let @76: Result>, AllocError>[{built_in impl Sized for NonNull>}, {built_in impl Sized for AllocError}]; // anonymous local storage_live(new_size@5) storage_live(@6) @@ -3041,6 +2747,202 @@ pub unsafe fn {impl Allocator for Global}::shrink<'_0>(@1: &'_0 (Global), @2: No storage_dead(@45) @9 := copy (@10) == move (@11) if move (@9) { + storage_dead(@11) + storage_dead(@9) + storage_live(cond@12) + @13 := copy ((old_layout@3).size) + cond@12 := copy (new_size@5) <= copy (@13) + @47 := ub_checks + if copy (@47) { + @46 := core::hint::assert_unchecked::precondition_check(copy (cond@12)) + assert(copy (cond@12) == true) + storage_dead(cond@12) + storage_live(ptr@15) + storage_live(self@16) + self@16 := copy (ptr@2) + ptr@15 := transmute, *mut u8>(copy (ptr@2)) + storage_dead(self@16) + storage_live(new_size@17) + new_size@17 := copy (new_size@5) + raw_ptr@14 := __rust_realloc(move (ptr@15), move (@13), move (@10), copy (new_size@5)) + storage_dead(new_size@17) + storage_dead(ptr@15) + storage_live(@18) + storage_live(self@19) + storage_live(self@20) + storage_live(ptr@21) + ptr@21 := copy (raw_ptr@14) + @49 := cast<*mut u8, *const u8>(copy (raw_ptr@14)) + storage_live(@50) + @50 := transmute<*mut u8, usize>(copy (raw_ptr@14)) + switch move (@50) { + 0 : usize => { + storage_dead(@50) + storage_live(@70) + @70 := Option::None { } + self@20 := move (@70) + }, + _ => { + storage_dead(@50) + storage_live(@48) + storage_live(@52) + @52 := cast<*mut u8, *mut ()>(copy (raw_ptr@14)) + @51 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@52)) + storage_dead(@52) + @48 := NonNull { pointer: copy (@49) } + self@20 := Option::Some { 0: move (@48) } + storage_dead(@48) + }, + } + } else { + assert(copy (cond@12) == true) + storage_dead(cond@12) + storage_live(ptr@15) + storage_live(self@16) + self@16 := copy (ptr@2) + ptr@15 := transmute, *mut u8>(copy (ptr@2)) + storage_dead(self@16) + storage_live(new_size@17) + new_size@17 := copy (new_size@5) + raw_ptr@14 := __rust_realloc(move (ptr@15), move (@13), move (@10), copy (new_size@5)) + storage_dead(new_size@17) + storage_dead(ptr@15) + storage_live(@18) + storage_live(self@19) + storage_live(self@20) + storage_live(ptr@21) + ptr@21 := copy (raw_ptr@14) + @49 := cast<*mut u8, *const u8>(copy (raw_ptr@14)) + storage_live(@50) + @50 := transmute<*mut u8, usize>(copy (raw_ptr@14)) + switch move (@50) { + 0 : usize => { + storage_dead(@50) + storage_live(@70) + @70 := Option::None { } + self@20 := move (@70) + }, + _ => { + storage_dead(@50) + storage_live(@48) + if copy (@47) { + storage_live(@52) + @52 := cast<*mut u8, *mut ()>(copy (raw_ptr@14)) + @51 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@52)) + storage_dead(@52) + } else { + } + @48 := NonNull { pointer: copy (@49) } + self@20 := Option::Some { 0: move (@48) } + storage_dead(@48) + }, + } + } + storage_dead(ptr@21) + storage_live(v@53) + match self@20 { + Option::None => { + storage_live(@73) + @73 := AllocError { } + storage_live(@74) + @74 := Result::Err { 0: move (@73) } + self@19 := move (@74) + storage_dead(v@53) + storage_dead(self@20) + storage_live(v@54) + match self@19 { + Result::Ok => { + v@54 := move ((self@19 as variant Result::Ok).0) + @18 := ControlFlow::Continue { 0: copy (v@54) } + storage_dead(v@54) + storage_dead(self@19) + ptr@22 := copy ((@18 as variant ControlFlow::Continue).0) + storage_dead(@18) + storage_live(@23) + storage_live(ptr@55) + storage_live(data@56) + data@56 := transmute, *mut u8>(copy (ptr@22)) + ptr@55 := @PtrFromPartsMut<'_, Slice>(copy (data@56), copy (new_size@5)) + storage_dead(data@56) + storage_live(@59) + if copy (@47) { + storage_live(@58) + @58 := transmute, *mut ()>(copy (ptr@22)) + @57 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@58)) + storage_dead(@58) + } else { + } + @59 := cast<*mut Slice, *const Slice>(copy (ptr@55)) + @23 := NonNull { pointer: copy (@59) } + storage_dead(@59) + storage_dead(ptr@55) + @0 := Result::Ok { 0: move (@23) } + storage_dead(@23) + return + }, + Result::Err => { + storage_dead(v@54) + storage_dead(self@19) + storage_live(@75) + @75 := AllocError { } + storage_live(@76) + @76 := Result::Err { 0: move (@75) } + @0 := move (@76) + storage_dead(@18) + return + }, + } + }, + Option::Some => { + v@53 := move ((self@20 as variant Option::Some).0) + self@19 := Result::Ok { 0: copy (v@53) } + storage_dead(v@53) + storage_dead(self@20) + storage_live(v@54) + match self@19 { + Result::Ok => { + v@54 := move ((self@19 as variant Result::Ok).0) + @18 := ControlFlow::Continue { 0: copy (v@54) } + storage_dead(v@54) + storage_dead(self@19) + ptr@22 := copy ((@18 as variant ControlFlow::Continue).0) + storage_dead(@18) + storage_live(@23) + storage_live(ptr@55) + storage_live(data@56) + data@56 := transmute, *mut u8>(copy (ptr@22)) + ptr@55 := @PtrFromPartsMut<'_, Slice>(copy (data@56), copy (new_size@5)) + storage_dead(data@56) + storage_live(@59) + if copy (@47) { + storage_live(@58) + @58 := transmute, *mut ()>(copy (ptr@22)) + @57 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@58)) + storage_dead(@58) + } else { + } + @59 := cast<*mut Slice, *const Slice>(copy (ptr@55)) + @23 := NonNull { pointer: copy (@59) } + storage_dead(@59) + storage_dead(ptr@55) + @0 := Result::Ok { 0: move (@23) } + storage_dead(@23) + return + }, + Result::Err => { + storage_dead(v@54) + storage_dead(self@19) + storage_live(@75) + @75 := AllocError { } + storage_live(@76) + @76 := Result::Err { 0: move (@75) } + @0 := move (@76) + storage_dead(@18) + return + }, + } + }, + } } else { storage_dead(@11) storage_dead(@9) @@ -3050,211 +2952,123 @@ pub unsafe fn {impl Allocator for Global}::shrink<'_0>(@1: &'_0 (Global), @2: No storage_live(v@60) match self@25 { Result::Ok => { - }, - Result::Err => { + v@60 := move ((self@25 as variant Result::Ok).0) + @24 := ControlFlow::Continue { 0: copy (v@60) } storage_dead(v@60) storage_dead(self@25) + match @24 { + ControlFlow::Continue => { + new_ptr@26 := copy ((@24 as variant ControlFlow::Continue).0) + storage_dead(@24) + 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 Slice>(copy (new_ptr@26)) + dst@29 := cast<*mut Slice, *mut u8>(copy (@61)) + storage_live(@65) + @65 := ub_checks + if copy (@65) { + storage_live(@63) + @63 := transmute, *const ()>(copy (ptr@2)) + storage_live(@64) + @64 := cast<*mut Slice, *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@5)) + storage_dead(@64) + storage_dead(@63) + } else { + } + copy_nonoverlapping(copy (src@27), copy (dst@29), copy (new_size@5)) + storage_dead(@65) + storage_dead(dst@29) + storage_dead(src@27) + storage_live(@66) + @66 := copy ((old_layout@3).size) + switch move (@66) { + 0 : usize => { + }, + _ => { + @30 := __rust_dealloc(move (ptr@28), move (@66), move (@10)) + }, + } + storage_dead(@66) + @0 := Result::Ok { 0: copy (new_ptr@26) } + return + }, + ControlFlow::Break => { + storage_live(@71) + @71 := AllocError { } + storage_live(@72) + @72 := Result::Err { 0: move (@71) } + @0 := move (@72) + storage_dead(@24) + return + }, + } + }, + Result::Err => { storage_live(@67) @67 := AllocError { } storage_live(@68) @68 := Result::Err { 0: move (@67) } - @0 := move (@68) - storage_dead(@24) - return - }, - } - v@60 := move ((self@25 as variant Result::Ok).0) - @24 := ControlFlow::Continue { 0: copy (v@60) } - storage_dead(v@60) - storage_dead(self@25) - new_ptr@26 := copy ((@24 as variant ControlFlow::Continue).0) - storage_dead(@24) - 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 Slice>(copy (new_ptr@26)) - dst@29 := cast<*mut Slice, *mut u8>(copy (@61)) - storage_live(@65) - @65 := ub_checks - if copy (@65) { - storage_live(@63) - @63 := transmute, *const ()>(copy (ptr@2)) - storage_live(@64) - @64 := cast<*mut Slice, *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@5)) - storage_dead(@64) - storage_dead(@63) - } else { - } - copy_nonoverlapping(copy (src@27), copy (dst@29), copy (new_size@5)) - storage_dead(@65) - storage_dead(dst@29) - storage_dead(src@27) - storage_live(@66) - @66 := copy ((old_layout@3).size) - switch move (@66) { - 0 : usize => { - }, - _ => { - @30 := __rust_dealloc(move (ptr@28), move (@66), move (@10)) - }, - } - storage_dead(@66) - @0 := Result::Ok { 0: copy (new_ptr@26) } - return - } - storage_dead(@11) - storage_dead(@9) - storage_live(cond@12) - @13 := copy ((old_layout@3).size) - cond@12 := copy (new_size@5) <= copy (@13) - @47 := ub_checks - if copy (@47) { - @46 := core::hint::assert_unchecked::precondition_check(copy (cond@12)) - assert(copy (cond@12) == true) - storage_dead(cond@12) - storage_live(ptr@15) - storage_live(self@16) - self@16 := copy (ptr@2) - ptr@15 := transmute, *mut u8>(copy (ptr@2)) - storage_dead(self@16) - storage_live(new_size@17) - new_size@17 := copy (new_size@5) - raw_ptr@14 := __rust_realloc(move (ptr@15), move (@13), move (@10), copy (new_size@5)) - storage_dead(new_size@17) - storage_dead(ptr@15) - storage_live(@18) - storage_live(self@19) - storage_live(self@20) - storage_live(ptr@21) - ptr@21 := copy (raw_ptr@14) - @49 := cast<*mut u8, *const u8>(copy (raw_ptr@14)) - storage_live(@50) - @50 := transmute<*mut u8, usize>(copy (raw_ptr@14)) - switch move (@50) { - 0 : usize => { - storage_dead(@50) - storage_live(@69) - @69 := Option::None { } - self@20 := move (@69) - }, - _ => { - storage_dead(@50) - storage_live(@48) - storage_live(@52) - @52 := cast<*mut u8, *mut ()>(copy (raw_ptr@14)) - @51 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@52)) - storage_dead(@52) - @48 := NonNull { pointer: copy (@49) } - self@20 := Option::Some { 0: move (@48) } - storage_dead(@48) - }, - } - } else { - assert(copy (cond@12) == true) - storage_dead(cond@12) - storage_live(ptr@15) - storage_live(self@16) - self@16 := copy (ptr@2) - ptr@15 := transmute, *mut u8>(copy (ptr@2)) - storage_dead(self@16) - storage_live(new_size@17) - new_size@17 := copy (new_size@5) - raw_ptr@14 := __rust_realloc(move (ptr@15), move (@13), move (@10), copy (new_size@5)) - storage_dead(new_size@17) - storage_dead(ptr@15) - storage_live(@18) - storage_live(self@19) - storage_live(self@20) - storage_live(ptr@21) - ptr@21 := copy (raw_ptr@14) - @49 := cast<*mut u8, *const u8>(copy (raw_ptr@14)) - storage_live(@50) - @50 := transmute<*mut u8, usize>(copy (raw_ptr@14)) - switch move (@50) { - 0 : usize => { - storage_dead(@50) storage_live(@69) - @69 := Option::None { } - self@20 := move (@69) - }, - _ => { - storage_dead(@50) - storage_live(@48) - if copy (@47) { - storage_live(@52) - @52 := cast<*mut u8, *mut ()>(copy (raw_ptr@14)) - @51 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@52)) - storage_dead(@52) - } else { + @69 := ControlFlow::Break { 0: move (@68) } + @24 := move (@69) + storage_dead(v@60) + storage_dead(self@25) + match @24 { + ControlFlow::Continue => { + new_ptr@26 := copy ((@24 as variant ControlFlow::Continue).0) + storage_dead(@24) + 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 Slice>(copy (new_ptr@26)) + dst@29 := cast<*mut Slice, *mut u8>(copy (@61)) + storage_live(@65) + @65 := ub_checks + if copy (@65) { + storage_live(@63) + @63 := transmute, *const ()>(copy (ptr@2)) + storage_live(@64) + @64 := cast<*mut Slice, *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@5)) + storage_dead(@64) + storage_dead(@63) + } else { + } + copy_nonoverlapping(copy (src@27), copy (dst@29), copy (new_size@5)) + storage_dead(@65) + storage_dead(dst@29) + storage_dead(src@27) + storage_live(@66) + @66 := copy ((old_layout@3).size) + switch move (@66) { + 0 : usize => { + }, + _ => { + @30 := __rust_dealloc(move (ptr@28), move (@66), move (@10)) + }, + } + storage_dead(@66) + @0 := Result::Ok { 0: copy (new_ptr@26) } + return + }, + ControlFlow::Break => { + storage_live(@71) + @71 := AllocError { } + storage_live(@72) + @72 := Result::Err { 0: move (@71) } + @0 := move (@72) + storage_dead(@24) + return + }, } - @48 := NonNull { pointer: copy (@49) } - self@20 := Option::Some { 0: move (@48) } - storage_dead(@48) }, } } - storage_dead(ptr@21) - storage_live(v@53) - match self@20 { - Option::None => { - storage_live(@70) - @70 := AllocError { } - storage_live(@71) - @71 := Result::Err { 0: move (@70) } - self@19 := move (@71) - }, - Option::Some => { - v@53 := move ((self@20 as variant Option::Some).0) - self@19 := Result::Ok { 0: copy (v@53) } - }, - } - storage_dead(v@53) - storage_dead(self@20) - storage_live(v@54) - match self@19 { - Result::Ok => { - }, - Result::Err => { - storage_dead(v@54) - storage_dead(self@19) - storage_live(@72) - @72 := AllocError { } - storage_live(@73) - @73 := Result::Err { 0: move (@72) } - @0 := move (@73) - storage_dead(@18) - return - }, - } - v@54 := move ((self@19 as variant Result::Ok).0) - @18 := ControlFlow::Continue { 0: copy (v@54) } - storage_dead(v@54) - storage_dead(self@19) - ptr@22 := copy ((@18 as variant ControlFlow::Continue).0) - storage_dead(@18) - storage_live(@23) - storage_live(ptr@55) - storage_live(data@56) - data@56 := transmute, *mut u8>(copy (ptr@22)) - ptr@55 := @PtrFromPartsMut<'_, Slice>(copy (data@56), copy (new_size@5)) - storage_dead(data@56) - storage_live(@59) - if copy (@47) { - storage_live(@58) - @58 := transmute, *mut ()>(copy (ptr@22)) - @57 := core::ptr::non_null::{NonNull}::new_unchecked::precondition_check(move (@58)) - storage_dead(@58) - } else { - } - @59 := cast<*mut Slice, *const Slice>(copy (ptr@55)) - @23 := NonNull { pointer: copy (@59) } - storage_dead(@59) - storage_dead(ptr@55) - @0 := Result::Ok { 0: move (@23) } - storage_dead(@23) - return + undefined_behavior }, } storage_live(@32) @@ -3337,31 +3151,25 @@ impl Allocator for Global { vtable: {impl Allocator for Global}::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: alloc::alloc::handle_alloc_error::ct_error fn ct_error(@1: Layout) -> ! { let @0: !; // return let @1: Layout; // arg #1 let @2: Arguments<'_>; // anonymous local - let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @7: Array<&'_ (Str), 1 : usize>; // anonymous local - storage_live(@6) - storage_live(@7) - @7 := [const ("allocation failed")] - @6 := &@7 - storage_live(@5) storage_live(@2) - storage_live(@3) - storage_live(@4) - @5 := move (@6) - @4 := &*(@5) - @3 := &*(@4) - @2 := new_const<'_, 1 : usize>(move (@3)) - storage_dead(@3) + @2 := from_str<'_>(const ("allocation failed")) panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 6da5aa29c..28be2a7c0 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -4,6 +4,11 @@ #[lang_item("alloc_layout")] pub opaque type Layout +// Full name: core::intrinsics::offset_of +#[lang_item("offset_of")] +pub fn offset_of(@1: u32, @2: u32) -> usize += + // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -653,6 +658,7 @@ where let @12: usize; // anonymous local let @13: usize; // anonymous local let @14: usize; // anonymous local + let @15: usize; // anonymous local storage_live(@9) storage_live(@12) @@ -661,11 +667,13 @@ where size@1 := size_of[@TraitClause0]() storage_live(align@2) align@2 := align_of[@TraitClause0]() - storage_live(ub@3) + storage_live(@15) // This is `const (false)` in the MIR we get, but `true` in const evaluation. + @15 := offset_of(Struct[@TraitClause0].b) + storage_live(ub@3) ub@3 := ub_checks storage_live(offset@4) - offset@4 := offset_of(?)[@TraitClause0]> + offset@4 := move (@15) storage_live(@5) storage_live(@6) storage_live(@7) diff --git a/charon/tests/ui/simple/closure-inside-inline-const.out b/charon/tests/ui/simple/closure-inside-inline-const.out new file mode 100644 index 000000000..16e9f0c92 --- /dev/null +++ b/charon/tests/ui/simple/closure-inside-inline-const.out @@ -0,0 +1,229 @@ +# 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::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized + vtable: core::marker::Tuple::{vtable} +} + +// Full name: core::mem::size_of +#[lang_item("mem_size_of")] +pub fn size_of() -> usize +where + [@TraitClause0]: Sized, += + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] + vtable: core::ops::function::FnOnce::{vtable} +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] + vtable: core::ops::function::FnMut::{vtable} +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] + vtable: core::ops::function::Fn::{vtable} +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, += + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, += + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, += + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::foo::{const}::closure +struct closure +where + [@TraitClause0]: Sized, +{} + +// Full name: test_crate::foo +pub fn foo() -> usize +where + [@TraitClause0]: Sized, +{ + let @0: usize; // return + let @1: usize; // anonymous local + let _f@2: closure[@TraitClause0]; // local + + storage_live(@1) + storage_live(_f@2) + _f@2 := closure { } + @1 := size_of[@TraitClause0]() + storage_dead(_f@2) + @0 := move (@1) + return +} + +// Full name: test_crate::foo::{const}::{impl Fn<()> for closure[@TraitClause0]}::call +fn {impl Fn<()> for closure[@TraitClause0]}::call<'_0, T>(@1: &'_0 (closure[@TraitClause0]), @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let @1: &'_ (closure[@TraitClause0]); // arg #1 + let tupled_args@2: (); // arg #2 + + @0 := const (42 : i32) + return +} + +// Full name: test_crate::foo::{const}::{impl FnMut<()> for closure[@TraitClause0]}::call_mut +fn {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_0, T>(@1: &'_0 mut (closure[@TraitClause0]), @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let state@1: &'_0 mut (closure[@TraitClause0]); // arg #1 + let args@2: (); // arg #2 + let @3: &'_ (closure[@TraitClause0]); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<()> for closure[@TraitClause0]}::call<'_, T>[@TraitClause0](move (@3), move (args@2)) + return +} + +// Full name: test_crate::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place +fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +where + [@TraitClause0]: Sized, += + +// Full name: test_crate::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]} +impl Destruct for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + fn drop_in_place = {impl Destruct for closure[@TraitClause0]}::drop_in_place[@TraitClause0] + non-dyn-compatible +} + +// Full name: test_crate::foo::{const}::{impl FnOnce<()> for closure[@TraitClause0]}::call_once +fn {impl FnOnce<()> for closure[@TraitClause0]}::call_once(@1: closure[@TraitClause0], @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let @1: closure[@TraitClause0]; // arg #1 + let @2: (); // arg #2 + let @3: &'_ mut (closure[@TraitClause0]); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_, T>[@TraitClause0](move (@3), move (@2)) + drop[{impl Destruct for closure[@TraitClause0]}[@TraitClause0]] @1 + return +} + +// Full name: test_crate::foo::{const}::{impl FnOnce<()> for closure[@TraitClause0]} +impl FnOnce<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {built_in impl Sized for ()} + parent_clause2 = {built_in impl Tuple for ()} + parent_clause3 = {built_in impl Sized for i32} + type Output = i32 + fn call_once = {impl FnOnce<()> for closure[@TraitClause0]}::call_once[@TraitClause0] + non-dyn-compatible +} + +// Full name: test_crate::foo::{const}::{impl FnMut<()> for closure[@TraitClause0]} +impl FnMut<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {impl FnOnce<()> for closure[@TraitClause0]}[@TraitClause0] + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call_mut<'_0_1> = {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_0_1, T>[@TraitClause0] + non-dyn-compatible +} + +// Full name: test_crate::foo::{const}::{impl Fn<()> for closure[@TraitClause0]} +impl Fn<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {impl FnMut<()> for closure[@TraitClause0]}[@TraitClause0] + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call<'_0_1> = {impl Fn<()> for closure[@TraitClause0]}::call<'_0_1, T>[@TraitClause0] + non-dyn-compatible +} + + + diff --git a/charon/tests/ui/simple/closure-inside-inline-const.rs b/charon/tests/ui/simple/closure-inside-inline-const.rs new file mode 100644 index 000000000..0cf407c4f --- /dev/null +++ b/charon/tests/ui/simple/closure-inside-inline-const.rs @@ -0,0 +1,11 @@ +// This tests a closure inside a non-evaluable inline constant. This is tricky because both these +// items get fake generic params in rustc, for type inference purposes. Yet the generic args for +// the closure don't include the extra arg for its parent inline constant. Generally speaking we +// must manage these extra args by hand in hax. Thankfully they don't show up inside the MIR +// bodies, only in signatures. +pub fn foo() -> usize { + const { + let _f = || 42; + std::mem::size_of::() + } +} diff --git a/charon/tests/ui/simple/drop-cow.out b/charon/tests/ui/simple/drop-cow.out new file mode 100644 index 000000000..42a6a9204 --- /dev/null +++ b/charon/tests/ui/simple/drop-cow.out @@ -0,0 +1,129 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +// Full name: core::borrow::Borrow +#[lang_item("Borrow")] +pub trait Borrow +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: MetaSized + parent_clause2 : [@TraitClause2]: Destruct + parent_clause3 : [@TraitClause3]: Destruct + fn borrow<'_0_1> = borrow<'_0_1, Self, Borrowed>[Self] + vtable: core::borrow::Borrow::{vtable} +} + +// Full name: core::borrow::Borrow::borrow +pub fn borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed) +where + [@TraitClause0]: Borrow, += + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: alloc::borrow::ToOwned +#[lang_item("ToOwned")] +pub trait ToOwned +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Destruct + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Borrow + parent_clause4 : [@TraitClause4]: Destruct + type Owned + fn to_owned<'_0_1> = to_owned<'_0_1, Self>[Self] + non-dyn-compatible +} + +// Full name: alloc::borrow::ToOwned::to_owned +#[lang_item("to_owned_method")] +pub fn to_owned<'_0, Self>(@1: &'_0 (Self)) -> @TraitClause0::Owned +where + [@TraitClause0]: ToOwned, += + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::Cow +enum Cow<'a, B> +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: ToOwned, + [@TraitClause2]: Destruct, + B : 'a, + B : 'a, +{ + Borrowed(&'a (B)), + Owned(@TraitClause1::Owned), +} + +// Full name: test_crate::Cow::{impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place +fn {impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place<'a, B>(@1: *mut Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: ToOwned, + [@TraitClause2]: Destruct, + B : 'a, + B : 'a, += + +// Full name: test_crate::Cow::{impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]} +impl<'a, B> Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: ToOwned, + [@TraitClause2]: Destruct, + B : 'a, + B : 'a, +{ + fn drop_in_place = {impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2] + non-dyn-compatible +} + +// Full name: test_crate::drop_cow +fn drop_cow<'a, B>(@1: Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: ToOwned, + [@TraitClause2]: Destruct, + B : 'a, +{ + let @0: (); // return + let @1: Cow<'_, B>[@TraitClause0, @TraitClause1, @TraitClause2]; // arg #1 + + @0 := () + @0 := () + drop[{impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}<'_, B>[@TraitClause0, @TraitClause1, @TraitClause2]] @1 + return +} + + + diff --git a/charon/tests/ui/simple/drop-cow.rs b/charon/tests/ui/simple/drop-cow.rs new file mode 100644 index 000000000..8e90eb071 --- /dev/null +++ b/charon/tests/ui/simple/drop-cow.rs @@ -0,0 +1,17 @@ +//@ charon-args=--mir=elaborated +//@ charon-args=--add-drop-bounds +//! Test that we can generate drop glue for a polymorphic type that uses associated types (as that +//! used to cause ICEs in the compiler). +enum Cow<'a, B> +where + B: 'a + ToOwned + ?Sized, +{ + Borrowed(&'a B), + Owned(::Owned), +} + +fn drop_cow<'a, B>(_: Cow<'a, B>) +where + B: 'a + ToOwned + ?Sized, +{ +} diff --git a/charon/tests/ui/simple/foreign-inline-const.out b/charon/tests/ui/simple/foreign-inline-const.out new file mode 100644 index 000000000..d4b1be843 --- /dev/null +++ b/charon/tests/ui/simple/foreign-inline-const.out @@ -0,0 +1,245 @@ +# 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::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized + vtable: core::marker::Tuple::{vtable} +} + +// Full name: core::mem::size_of +#[lang_item("mem_size_of")] +pub fn size_of() -> usize +where + [@TraitClause0]: Sized, += + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] + vtable: core::ops::function::FnOnce::{vtable} +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] + vtable: core::ops::function::FnMut::{vtable} +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] + vtable: core::ops::function::Fn::{vtable} +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, += + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, += + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, += + +// Full name: closure_inside_inline_const::foo::{const}::closure +struct closure +where + [@TraitClause0]: Sized, +{} + +// Full name: closure_inside_inline_const::foo +pub fn foo() -> usize +where + [@TraitClause0]: Sized, +{ + let @0: usize; // return + let @1: usize; // anonymous local + let _f@2: closure[@TraitClause0]; // local + + storage_live(@1) + storage_live(_f@2) + _f@2 := closure { } + @1 := size_of[@TraitClause0]() + storage_dead(_f@2) + @0 := move (@1) + return +} + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: closure_inside_inline_const::foo::{const}::{impl Fn<()> for closure[@TraitClause0]}::call +fn {impl Fn<()> for closure[@TraitClause0]}::call<'_0, T>(@1: &'_0 (closure[@TraitClause0]), @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let @1: &'_ (closure[@TraitClause0]); // arg #1 + let tupled_args@2: (); // arg #2 + + @0 := const (42 : i32) + return +} + +// Full name: closure_inside_inline_const::foo::{const}::{impl FnMut<()> for closure[@TraitClause0]}::call_mut +fn {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_0, T>(@1: &'_0 mut (closure[@TraitClause0]), @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let state@1: &'_0 mut (closure[@TraitClause0]); // arg #1 + let args@2: (); // arg #2 + let @3: &'_ (closure[@TraitClause0]); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<()> for closure[@TraitClause0]}::call<'_, T>[@TraitClause0](move (@3), move (args@2)) + return +} + +// Full name: closure_inside_inline_const::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place +fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +where + [@TraitClause0]: Sized, += + +// Full name: closure_inside_inline_const::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]} +impl Destruct for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + fn drop_in_place = {impl Destruct for closure[@TraitClause0]}::drop_in_place[@TraitClause0] + non-dyn-compatible +} + +// Full name: closure_inside_inline_const::foo::{const}::{impl FnOnce<()> for closure[@TraitClause0]}::call_once +fn {impl FnOnce<()> for closure[@TraitClause0]}::call_once(@1: closure[@TraitClause0], @2: ()) -> i32 +where + [@TraitClause0]: Sized, +{ + let @0: i32; // return + let @1: closure[@TraitClause0]; // arg #1 + let @2: (); // arg #2 + let @3: &'_ mut (closure[@TraitClause0]); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_, T>[@TraitClause0](move (@3), move (@2)) + drop[{impl Destruct for closure[@TraitClause0]}[@TraitClause0]] @1 + return +} + +// Full name: closure_inside_inline_const::foo::{const}::{impl FnOnce<()> for closure[@TraitClause0]} +impl FnOnce<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {built_in impl Sized for ()} + parent_clause2 = {built_in impl Tuple for ()} + parent_clause3 = {built_in impl Sized for i32} + type Output = i32 + fn call_once = {impl FnOnce<()> for closure[@TraitClause0]}::call_once[@TraitClause0] + non-dyn-compatible +} + +// Full name: closure_inside_inline_const::foo::{const}::{impl FnMut<()> for closure[@TraitClause0]} +impl FnMut<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {impl FnOnce<()> for closure[@TraitClause0]}[@TraitClause0] + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call_mut<'_0_1> = {impl FnMut<()> for closure[@TraitClause0]}::call_mut<'_0_1, T>[@TraitClause0] + non-dyn-compatible +} + +// Full name: closure_inside_inline_const::foo::{const}::{impl Fn<()> for closure[@TraitClause0]} +impl Fn<()> for closure[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = {built_in impl MetaSized for closure[@TraitClause0]} + parent_clause1 = {impl FnMut<()> for closure[@TraitClause0]}[@TraitClause0] + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call<'_0_1> = {impl Fn<()> for closure[@TraitClause0]}::call<'_0_1, T>[@TraitClause0] + non-dyn-compatible +} + +// Full name: test_crate::bar +fn bar() +where + [@TraitClause0]: Sized, +{ + let @0: (); // return + let @1: usize; // anonymous local + + @0 := () + storage_live(@1) + @1 := foo[@TraitClause0]() + storage_dead(@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/foreign-inline-const.rs b/charon/tests/ui/simple/foreign-inline-const.rs new file mode 100644 index 000000000..97dbc979b --- /dev/null +++ b/charon/tests/ui/simple/foreign-inline-const.rs @@ -0,0 +1,5 @@ +//@ aux-crate=closure-inside-inline-const.rs +//@ charon-args=--include=closure_inside_inline_const +fn bar() { + closure_inside_inline_const::foo::(); +} diff --git a/charon/tests/ui/simple/gat-default.out b/charon/tests/ui/simple/gat-default.out index 4017eaa76..ab07f2761 100644 --- a/charon/tests/ui/simple/gat-default.out +++ b/charon/tests/ui/simple/gat-default.out @@ -1,5 +1,5 @@ -thread 'rustc' panicked at /rustc-dev/843f8ce2ebc01d35a30484eadc8a84cdc6130844/compiler/rustc_type_ir/src/binder.rs:781:9: +thread 'rustc' panicked at /rustc-dev/94b49fd998d6723e0a9240a7cff5f9df37b84dd8/compiler/rustc_type_ir/src/binder.rs:781:9: type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()] note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace error: Hax panicked when translating `test_crate::{impl#0}`. @@ -9,7 +9,7 @@ error: Hax panicked when translating `test_crate::{impl#0}`. | ^^^^^^^^^^^^^^^^^^^^^^ -thread 'rustc' panicked at /rustc-dev/843f8ce2ebc01d35a30484eadc8a84cdc6130844/compiler/rustc_type_ir/src/binder.rs:781:9: +thread 'rustc' panicked at /rustc-dev/94b49fd998d6723e0a9240a7cff5f9df37b84dd8/compiler/rustc_type_ir/src/binder.rs:781:9: type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()] error: Hax panicked when translating `test_crate::{impl#0}`. --> tests/ui/simple/gat-default.rs:9:1 diff --git a/charon/tests/ui/simple/generic-offset-of.out b/charon/tests/ui/simple/generic-offset-of.out new file mode 100644 index 000000000..58f566782 --- /dev/null +++ b/charon/tests/ui/simple/generic-offset-of.out @@ -0,0 +1,78 @@ +# Final LLBC before serialization: + +// Full name: core::intrinsics::offset_of +#[lang_item("offset_of")] +pub fn offset_of(@1: u32, @2: u32) -> usize += + +// 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 +} + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::B +struct B +where + [@TraitClause0]: Sized, +{ + y: u32, + t: T, +} + +// Full name: test_crate::A +struct A +where + [@TraitClause0]: Sized, +{ + x: B[@TraitClause0], +} + +// Full name: test_crate::foo +fn foo() +where + [@TraitClause0]: Sized, +{ + let @0: (); // return + let @1: usize; // anonymous local + let @2: usize; // anonymous local + let @3: usize; // anonymous local + let @4: usize; // anonymous local + let @5: usize; // anonymous local + + storage_live(@2) + storage_live(@5) + storage_live(@3) + @3 := offset_of(A[@TraitClause0].x) + storage_live(@4) + @4 := offset_of(B[@TraitClause0].y) + @5 := copy (@3) panic.+ copy (@4) + @2 := move (@5) + storage_dead(@4) + storage_dead(@3) + @0 := () + storage_live(@1) + @1 := move (@2) + storage_dead(@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/generic-offset-of.rs b/charon/tests/ui/simple/generic-offset-of.rs new file mode 100644 index 000000000..1d242eb09 --- /dev/null +++ b/charon/tests/ui/simple/generic-offset-of.rs @@ -0,0 +1,12 @@ +struct A { + x: B, +} + +struct B { + y: u32, + t: T, +} + +fn foo() { + let _ = std::mem::offset_of!(A, x.y); +} diff --git a/charon/tests/ui/simple/lending-iterator-gat.out b/charon/tests/ui/simple/lending-iterator-gat.out index cae05b42b..b3f42cd2c 100644 --- a/charon/tests/ui/simple/lending-iterator-gat.out +++ b/charon/tests/ui/simple/lending-iterator-gat.out @@ -3,8 +3,6 @@ // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::marker::MetaSized #[lang_item("meta_sized")] diff --git a/charon/tests/ui/simple/offset-of.out b/charon/tests/ui/simple/offset-of.out new file mode 100644 index 000000000..f920d4594 --- /dev/null +++ b/charon/tests/ui/simple/offset-of.out @@ -0,0 +1,38 @@ +# Final LLBC before serialization: + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::B +struct B { + y: u32, +} + +// Full name: test_crate::A +struct A { + x: B, +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let @1: usize; // anonymous local + + @0 := () + storage_live(@1) + @1 := const (0 : usize) + storage_dead(@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/offset-of.rs b/charon/tests/ui/simple/offset-of.rs new file mode 100644 index 000000000..b6af15c69 --- /dev/null +++ b/charon/tests/ui/simple/offset-of.rs @@ -0,0 +1,11 @@ +struct A { + x: B, +} + +struct B { + y: u32, +} + +fn main() { + let _ = std::mem::offset_of!(A, x.y); +} diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index 9ddd58d7e..cb23e1a0a 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -3,6 +3,12 @@ // Full name: core::fmt::Error pub struct Error {} +// Full name: core::ptr::non_null::NonNull +#[lang_item("NonNull")] +pub struct NonNull { + pointer: *const T, +} + // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -15,39 +21,6 @@ pub trait Sized non-dyn-compatible } -// Full name: core::option::Option -#[lang_item("Option")] -pub enum Option -where - [@TraitClause0]: Sized, -{ - None, - Some(T), -} - -// Full name: core::fmt::rt::Count -#[lang_item("format_count")] -pub enum Count { - Is(u16), - Param(usize), - Implied, -} - -// Full name: core::fmt::rt::Placeholder -#[lang_item("format_placeholder")] -pub struct Placeholder { - position: usize, - flags: u32, - precision: Count, - width: Count, -} - -// Full name: core::ptr::non_null::NonNull -#[lang_item("NonNull")] -pub struct NonNull { - pointer: *const T, -} - // Full name: core::result::Result #[lang_item("Result")] pub enum Result @@ -77,13 +50,9 @@ pub struct Argument<'a> { // Full name: core::fmt::Arguments #[lang_item("format_arguments")] -pub struct Arguments<'a> -where - 'a : 'a, -{ - pieces: &'a (Slice<&'static (Str)>), - fmt: Option<&'a (Slice)>[{built_in impl Sized for &'_ (Slice)}], - args: &'a (Slice>), +pub struct Arguments<'a> { + template: NonNull, + args: NonNull>, } fn core::slice::index::slice_index_fail::do_panic::runtime(@1: usize, @2: usize) -> ! @@ -172,6 +141,16 @@ where return } +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option +where + [@TraitClause0]: Sized, +{ + None, + Some(T), +} + fn core::slice::index::slice_index_fail::do_panic(@1: usize, @2: usize) -> ! { let @0: !; // return @@ -577,16 +556,6 @@ where return } -fn UNIT_METADATA() -{ - let @0: (); // return - - @0 := () - return -} - -const UNIT_METADATA: () = @Fun0() - // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked::precondition_check fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked::precondition_check(@1: usize, @2: usize, @3: usize) { @@ -596,18 +565,20 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} let len@3: usize; // arg #3 let @4: bool; // anonymous local let @5: bool; // anonymous local - let @6: !; // anonymous local - let @7: Arguments<'_>; // anonymous local - let pieces@8: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Slice<&'_ (Str)>); // anonymous local - let @11: &'_ (Slice>); // anonymous local - let @12: &'_ (Array, 0 : usize>); // anonymous local - let @13: Array, 0 : usize>; // anonymous local - let @14: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@6: &'_ (Str); // local + let @7: !; // anonymous local + let @8: Arguments<'_>; // anonymous local + let @9: NonNull; // anonymous local + let @10: *const u8; // anonymous local + let @11: NonNull>; // anonymous local + let @12: usize; // anonymous local + let @13: usize; // anonymous local + let @14: usize; // anonymous local + let @15: *const Str; // anonymous local + let @16: &'_ (Slice); // anonymous local - storage_live(@6) - storage_live(pieces@8) + storage_live(msg@6) + storage_live(@7) @0 := () storage_live(@4) @4 := copy (end@2) >= copy (start@1) @@ -622,24 +593,34 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} } } else { } - storage_live(@12) - storage_live(@13) - @13 := [] - @12 := &@13 - storage_live(@7) + msg@6 := const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@8) storage_live(@9) - @9 := [const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@8 := &@9 storage_live(@10) - @10 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@8)) + storage_live(@15) + @15 := &raw const *(msg@6) with_metadata(copy (msg@6.metadata)) + @10 := cast<*const Str, *const u8>(copy (@15)) + storage_dead(@15) + @9 := transmute<*const u8, NonNull>(copy (@10)) + storage_dead(@10) storage_live(@11) - @11 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@12)) + storage_live(@12) + storage_live(@13) storage_live(@14) - @14 := Option::None { } - @7 := Arguments { pieces: copy (@10), fmt: move (@14), args: copy (@11) } + storage_live(@16) + @16 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @14 := copy (@16.metadata) + storage_dead(@16) + @13 := move (@14) wrap.<< const (1 : i32) + storage_dead(@14) + @12 := move (@13) | const (1 : usize) + storage_dead(@13) + @11 := transmute>>(move (@12)) + storage_dead(@12) + @8 := Arguments { template: move (@9), args: move (@11) } storage_dead(@11) - storage_dead(@10) - @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) + storage_dead(@9) + @7 := panic_nounwind_fmt<'_>(move (@8), const (false)) } // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked @@ -704,18 +685,20 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} let len@3: usize; // arg #3 let @4: bool; // anonymous local let @5: bool; // anonymous local - let @6: !; // anonymous local - let @7: Arguments<'_>; // anonymous local - let pieces@8: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Slice<&'_ (Str)>); // anonymous local - let @11: &'_ (Slice>); // anonymous local - let @12: &'_ (Array, 0 : usize>); // anonymous local - let @13: Array, 0 : usize>; // anonymous local - let @14: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@6: &'_ (Str); // local + let @7: !; // anonymous local + let @8: Arguments<'_>; // anonymous local + let @9: NonNull; // anonymous local + let @10: *const u8; // anonymous local + let @11: NonNull>; // anonymous local + let @12: usize; // anonymous local + let @13: usize; // anonymous local + let @14: usize; // anonymous local + let @15: *const Str; // anonymous local + let @16: &'_ (Slice); // anonymous local - storage_live(@6) - storage_live(pieces@8) + storage_live(msg@6) + storage_live(@7) @0 := () storage_live(@4) @4 := copy (end@2) >= copy (start@1) @@ -730,24 +713,34 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} } } else { } - storage_live(@12) - storage_live(@13) - @13 := [] - @12 := &@13 - storage_live(@7) + msg@6 := const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@8) storage_live(@9) - @9 := [const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@8 := &@9 storage_live(@10) - @10 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@8)) + storage_live(@15) + @15 := &raw const *(msg@6) with_metadata(copy (msg@6.metadata)) + @10 := cast<*const Str, *const u8>(copy (@15)) + storage_dead(@15) + @9 := transmute<*const u8, NonNull>(copy (@10)) + storage_dead(@10) storage_live(@11) - @11 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(move (@12)) + storage_live(@12) + storage_live(@13) storage_live(@14) - @14 := Option::None { } - @7 := Arguments { pieces: copy (@10), fmt: move (@14), args: copy (@11) } + storage_live(@16) + @16 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @14 := copy (@16.metadata) + storage_dead(@16) + @13 := move (@14) wrap.<< const (1 : i32) + storage_dead(@14) + @12 := move (@13) | const (1 : usize) + storage_dead(@13) + @11 := transmute>>(move (@12)) + storage_dead(@12) + @8 := Arguments { template: move (@9), args: move (@11) } storage_dead(@11) - storage_dead(@10) - @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) + storage_dead(@9) + @7 := panic_nounwind_fmt<'_>(move (@8), const (false)) } // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked_mut @@ -1473,6 +1466,16 @@ where vtable: {impl SliceIndex> for RangeInclusive[{built_in impl Sized for usize}]}::{vtable}[@TraitClause0] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::slice_index_range pub fn slice_index_range<'_0>(@1: &'_0 (Slice)) -> &'_0 (Slice) { diff --git a/charon/tests/ui/simple/thread-local.out b/charon/tests/ui/simple/thread-local.out index 8bda50f8a..59889ddcf 100644 --- a/charon/tests/ui/simple/thread-local.out +++ b/charon/tests/ui/simple/thread-local.out @@ -1,4 +1,7 @@ -error: Unsupported constant: "Unhandled constant type" - --> /rustc/library/std/src/sys/thread_local/native/mod.rs:90:13 +error: charon does not support thread local references + --> /rustc/library/std/src/sys/thread_local/native/mod.rs:97:25 -ERROR Charon failed to translate this code (1 errors) +error: charon does not support thread local references + --> /rustc/library/std/src/sys/thread_local/native/mod.rs:105:25 + +ERROR Charon failed to translate this code (2 errors) diff --git a/charon/tests/ui/slice-index-range.out b/charon/tests/ui/slice-index-range.out index 4c9d1f166..00f3e1c58 100644 --- a/charon/tests/ui/slice-index-range.out +++ b/charon/tests/ui/slice-index-range.out @@ -50,25 +50,6 @@ where // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, - -// Full name: core::fmt::rt::Count -#[lang_item("format_count")] -pub enum Count { - Is(u16), - Param(usize), - Implied, -} - -// Full name: core::fmt::rt::Placeholder -#[lang_item("format_placeholder")] -pub struct Placeholder { - position: usize, - flags: u32, - precision: Count, - width: Count, -} // Full name: core::fmt::rt::Argument #[lang_item("format_argument")] @@ -151,6 +132,10 @@ fn core::slice::index::slice_index_fail::do_panic#3(@1: usize, @2: usize) -> ! pub fn panic_nounwind_fmt<'_0>(@1: Arguments<'_0>, @2: bool) -> ! = +// Full name: core::ptr::non_null::NonNull +#[lang_item("NonNull")] +pub opaque type NonNull + // Full name: core::slice::index::private_slice_index::Sealed pub trait Sealed { @@ -493,16 +478,6 @@ where return } -fn UNIT_METADATA() -{ - let @0: (); // return - - @0 := () - return -} - -const UNIT_METADATA: () = @Fun0() - // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked::precondition_check fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked::precondition_check(@1: usize, @2: usize, @3: usize) { @@ -512,16 +487,20 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} let len@3: usize; // arg #3 let @4: bool; // anonymous local let @5: bool; // anonymous local - let @6: !; // anonymous local - let @7: Arguments<'_>; // anonymous local - let pieces@8: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Slice<&'_ (Str)>); // anonymous local - let @11: &'_ (Slice>); // anonymous local - let @12: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@6: &'_ (Str); // local + let @7: !; // anonymous local + let @8: Arguments<'_>; // anonymous local + let @9: NonNull; // anonymous local + let @10: *const u8; // anonymous local + let @11: NonNull>; // anonymous local + let @12: usize; // anonymous local + let @13: usize; // anonymous local + let @14: usize; // anonymous local + let @15: *const Str; // anonymous local + let @16: &'_ (Slice); // anonymous local - storage_live(@6) - storage_live(pieces@8) + storage_live(msg@6) + storage_live(@7) @0 := () storage_live(@4) @4 := copy (end@2) >= copy (start@1) @@ -536,20 +515,34 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} } } else { } - storage_live(@7) + msg@6 := const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@8) storage_live(@9) - @9 := [const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@8 := &@9 storage_live(@10) - @10 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@8)) + storage_live(@15) + @15 := &raw const *(msg@6) with_metadata(copy (msg@6.metadata)) + @10 := cast<*const Str, *const u8>(copy (@15)) + storage_dead(@15) + @9 := transmute<*const u8, NonNull>(copy (@10)) + storage_dead(@10) storage_live(@11) - @11 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(copy ({promoted_const}<'_, 1 : usize>)) storage_live(@12) - @12 := Option::None { } - @7 := Arguments { 0: copy (@10), 1: move (@12), 2: copy (@11) } + storage_live(@13) + storage_live(@14) + storage_live(@16) + @16 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: slice::get_unchecked requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @14 := copy (@16.metadata) + storage_dead(@16) + @13 := move (@14) wrap.<< const (1 : i32) + storage_dead(@14) + @12 := move (@13) | const (1 : usize) + storage_dead(@13) + @11 := transmute>>(move (@12)) + storage_dead(@12) + @8 := Arguments { 0: move (@9), 1: move (@11) } storage_dead(@11) - storage_dead(@10) - @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) + storage_dead(@9) + @7 := panic_nounwind_fmt<'_>(move (@8), const (false)) } // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked @@ -614,16 +607,20 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} let len@3: usize; // arg #3 let @4: bool; // anonymous local let @5: bool; // anonymous local - let @6: !; // anonymous local - let @7: Arguments<'_>; // anonymous local - let pieces@8: &'_ (Array<&'_ (Str), 1 : usize>); // local - let @9: Array<&'_ (Str), 1 : usize>; // anonymous local - let @10: &'_ (Slice<&'_ (Str)>); // anonymous local - let @11: &'_ (Slice>); // anonymous local - let @12: Option<&'_ (Slice)>[{built_in impl Sized for &'_ (Slice)}]; // anonymous local + let msg@6: &'_ (Str); // local + let @7: !; // anonymous local + let @8: Arguments<'_>; // anonymous local + let @9: NonNull; // anonymous local + let @10: *const u8; // anonymous local + let @11: NonNull>; // anonymous local + let @12: usize; // anonymous local + let @13: usize; // anonymous local + let @14: usize; // anonymous local + let @15: *const Str; // anonymous local + let @16: &'_ (Slice); // anonymous local - storage_live(@6) - storage_live(pieces@8) + storage_live(msg@6) + storage_live(@7) @0 := () storage_live(@4) @4 := copy (end@2) >= copy (start@1) @@ -638,20 +635,34 @@ fn {impl SliceIndex> for Range[{built_in impl Sized for usize}]} } } else { } - storage_live(@7) + msg@6 := const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.") + storage_live(@8) storage_live(@9) - @9 := [const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")] - pieces@8 := &@9 storage_live(@10) - @10 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(copy (pieces@8)) + storage_live(@15) + @15 := &raw const *(msg@6) with_metadata(copy (msg@6.metadata)) + @10 := cast<*const Str, *const u8>(copy (@15)) + storage_dead(@15) + @9 := transmute<*const u8, NonNull>(copy (@10)) + storage_dead(@10) storage_live(@11) - @11 := @ArrayToSliceShared<'_, Argument<'_>, 0 : usize>(copy ({promoted_const}<'_, 1 : usize>)) storage_live(@12) - @12 := Option::None { } - @7 := Arguments { 0: copy (@10), 1: move (@12), 2: copy (@11) } + storage_live(@13) + storage_live(@14) + storage_live(@16) + @16 := transmute<&'_ (Str), &'_ (Slice)>(const ("unsafe precondition(s) violated: slice::get_unchecked_mut requires that the range is within the slice\n\nThis indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.")) + @14 := copy (@16.metadata) + storage_dead(@16) + @13 := move (@14) wrap.<< const (1 : i32) + storage_dead(@14) + @12 := move (@13) | const (1 : usize) + storage_dead(@13) + @11 := transmute>>(move (@12)) + storage_dead(@12) + @8 := Arguments { 0: move (@9), 1: move (@11) } storage_dead(@11) - storage_dead(@10) - @6 := panic_nounwind_fmt<'_>(move (@7), const (false)) + storage_dead(@9) + @7 := panic_nounwind_fmt<'_>(move (@8), const (false)) } // Full name: core::slice::index::{impl SliceIndex> for Range[{built_in impl Sized for usize}]}::get_unchecked_mut @@ -872,6 +883,16 @@ where vtable: {impl SliceIndex> for Range[{built_in impl Sized for usize}]}::{vtable}[@TraitClause0] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::main fn main() { diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index db4f35146..dae9962cc 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -1289,7 +1289,7 @@ where { let @0: usize; // return - @0 := const ({impl Trait for Wrapper[@TraitClause0]}[@TraitClause0, @TraitClause1]::LEN) + @0 := copy ({impl Trait for Wrapper[@TraitClause0]}::LEN[@TraitClause0, @TraitClause1]) return } diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out index d49fe9b9c..cdd9e2f1f 100644 --- a/charon/tests/ui/type_inference_is_order_dependent.out +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -44,8 +44,14 @@ pub struct Error {} // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, + +// Full name: core::fmt::rt::Argument +#[lang_item("format_argument")] +pub opaque type Argument<'a> + +// Full name: core::fmt::{Arguments<'a>}::new +pub unsafe fn new<'a, const N : usize, const M : usize>(@1: &'a (Array), @2: &'a (Array, M>)) -> Arguments<'a> += // Full name: core::result::Result #[lang_item("Result")] @@ -81,10 +87,6 @@ impl Debug for bool { vtable: {impl Debug for bool}::{vtable} } -// Full name: core::fmt::rt::Argument -#[lang_item("format_argument")] -pub opaque type Argument<'a> - // Full name: core::fmt::rt::{Argument<'_0>}::new_debug pub fn new_debug<'_0, '_1, T>(@1: &'_1 (T)) -> Argument<'_1> where @@ -92,10 +94,6 @@ where [@TraitClause1]: Debug, = -// Full name: core::fmt::rt::{Arguments<'a>}::new_v1 -pub fn new_v1<'a, const P : usize, const A : usize>(@1: &'a (Array<&'static (Str), P>), @2: &'a (Array, A>)) -> Arguments<'a> -= - // Full name: core::marker::Destruct #[lang_item("destruct")] pub trait Destruct @@ -171,15 +169,14 @@ where let args@6: Array, 1 : usize>; // local let @7: Argument<'_>; // anonymous local let @8: &'_ (U); // anonymous local - let @9: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @10: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local + let @9: &'_ (Array); // anonymous local + let @10: &'_ (Array); // anonymous local let @11: &'_ (Array, 1 : usize>); // anonymous local let @12: &'_ (Array, 1 : usize>); // anonymous local - let @13: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @14: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local - let @15: Array<&'_ (Str), 2 : usize>; // anonymous local + let @13: Array; // anonymous local + let @14: (); // anonymous local + let @15: &'_ (Array); // anonymous local - storage_live(@13) @0 := () storage_live(@1) storage_live(@2) @@ -195,23 +192,24 @@ where storage_live(@8) @8 := &*((args@3).0) @7 := new_debug<'_, '_, U>[@TraitClause1, @TraitClause5](move (@8)) - storage_live(@14) - storage_live(@15) - @15 := [const (""), const ("\n")] - @14 := &@15 storage_dead(@8) args@6 := [move (@7)] storage_dead(@7) storage_live(@9) storage_live(@10) - @13 := move (@14) - @10 := &*(@13) + storage_live(@13) + @13 := [const (192 : u8), const (1 : u8), const (10 : u8), const (0 : u8)] + storage_live(@14) + @14 := () + storage_live(@15) + @15 := &@13 + @10 := move (@15) @9 := &*(@10) storage_live(@11) storage_live(@12) @12 := &args@6 @11 := &*(@12) - @2 := new_v1<'_, 2 : usize, 1 : usize>(move (@9), move (@11)) + @2 := new<'_, 4 : usize, 1 : usize>(move (@9), move (@11)) storage_dead(@12) storage_dead(@11) storage_dead(@10) diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out index 785470f96..6223a68aa 100644 --- a/charon/tests/ui/ullbc-control-flow.out +++ b/charon/tests/ui/ullbc-control-flow.out @@ -577,12 +577,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } fn UNIT_METADATA() diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out index a5628f27d..1a650a7a1 100644 --- a/charon/tests/ui/unsupported/advanced-const-generics.out +++ b/charon/tests/ui/unsupported/advanced-const-generics.out @@ -1,34 +1,3 @@ -disabled backtrace -error[E9999]: Supposely unreachable place in the Rust AST. The label is "TranslateUneval". - This error report happend because some assumption about the Rust AST was broken. - - Context: - - self: UnevaluatedConst { def: test_crate::bar::{constant#0}, args: [N/#0] } - - ucv: UnevaluatedConst { - def: test_crate::bar::{constant#0}, - args: [ - N/#0, - ], - } - - --> tests/ui/unsupported/advanced-const-generics.rs:18:1 - | -18 | / fn bar() -19 | | where -20 | | [(); N + 1]:, - | |_________________^ - | - = note: ⚠️ This is a bug in Hax's frontend. - Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! - -error: Hax panicked when translating `test_crate::bar`. - --> tests/ui/unsupported/advanced-const-generics.rs:18:1 - | -18 | / fn bar() -19 | | where -20 | | [(); N + 1]:, - | |_________________^ - error: Constant parameters of non-literal type are not supported --> tests/ui/unsupported/advanced-const-generics.rs:14:8 | @@ -41,14 +10,11 @@ error: Item `test_crate::foo` caused errors; ignoring. 14 | fn foo() -> Foo { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -disabled backtrace -error: Hax panicked when translating `test_crate::bar`. - --> tests/ui/unsupported/advanced-const-generics.rs:18:1 +error: Well-formedness clauses are unsupported + --> tests/ui/unsupported/advanced-const-generics.rs:20:5 | -18 | / fn bar() -19 | | where -20 | | [(); N + 1]:, - | |_________________^ +20 | [(); N + 1]:, + | ^^^^^^^^^^^ error: Item `test_crate::bar` caused errors; ignoring. --> tests/ui/unsupported/advanced-const-generics.rs:18:1 @@ -58,6 +24,4 @@ error: Item `test_crate::bar` caused errors; ignoring. 20 | | [(); N + 1]:, | |_________________^ -error: aborting due to 1 previous error - -ERROR Code failed to compile +ERROR Charon failed to translate this code (4 errors) diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out index b79ffd8df..cbe9bff3f 100644 --- a/charon/tests/ui/unsupported/issue-79-bound-regions.out +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out @@ -388,12 +388,12 @@ where Self::parent_clause3::Output = O, Self::parent_clause3::Residual = Self, { - parent_clause0 : [@TraitClause0]: MetaSized + parent_clause0 : [@TraitClause0]: Sized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - vtable: core::ops::try_trait::Residual::{vtable} + non-dyn-compatible } // Full name: core::slice::iter::Iter diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 06f897811..1fe8c748b 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -46,8 +46,6 @@ pub struct Error {} // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> -where - 'a : 'a, // Full name: core::result::Result #[lang_item("Result")] diff --git a/flake.lock b/flake.lock index 2f3b1f7a5..78b572110 100644 --- a/flake.lock +++ b/flake.lock @@ -79,17 +79,17 @@ ] }, "locked": { - "lastModified": 1762569282, - "narHash": "sha256-vINZAJpXQTZd5cfh06Rcw7hesH7sGSvi+Tn+HUieJn8=", + "lastModified": 1763952169, + "narHash": "sha256-+PeDBD8P+NKauH+w7eO/QWCIp8Cx4mCfWnh9sJmy9CM=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8", + "rev": "ab726555a9a72e6dc80649809147823a813fa95b", "type": "github" }, "original": { "owner": "oxalica", "repo": "rust-overlay", - "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8", + "rev": "ab726555a9a72e6dc80649809147823a813fa95b", "type": "github" } }, diff --git a/flake.nix b/flake.nix index b88832922..7b9f0e45b 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ rust-overlay = { # We pin a specific commit because we require a relatively recent version # and flake dependents don't look at our flake.lock. - url = "github:oxalica/rust-overlay/a35a6144b976f70827c2fe2f5c89d16d8f9179d8"; + url = "github:oxalica/rust-overlay/ab726555a9a72e6dc80649809147823a813fa95b"; inputs.nixpkgs.follows = "nixpkgs"; }; crane.url = "github:ipetkov/crane";