diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 216d31027..0b0933eb9 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.129" +let supported_charon_version = "0.1.130" diff --git a/charon-ml/src/ExpressionsUtils.ml b/charon-ml/src/ExpressionsUtils.ml index 331a691db..5b61a64bb 100644 --- a/charon-ml/src/ExpressionsUtils.ml +++ b/charon-ml/src/ExpressionsUtils.ml @@ -1,7 +1,7 @@ open Expressions let unop_can_fail : unop -> bool = function - | Neg (OPanic | OUB) | Cast _ | PtrMetadata -> true + | Neg (OPanic | OUB) | Cast _ -> true | Neg OWrap | Not -> false let binop_can_fail : binop -> bool = function diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index b49ad683a..2150abc37 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -53,5 +53,6 @@ type 'fun_body gcrate = { global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; + unit_metadata : global_decl_ref; } [@@deriving show] diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 9001bcbeb..701181dd4 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -96,6 +96,7 @@ and gtranslated_crate_of_json ("global_decls", globals); ("trait_decls", trait_decls); ("trait_impls", trait_impls); + ("unit_metadata", unit_metadata); ("ordered_decls", declarations); ] -> let* ctx = id_to_file_of_json files in @@ -126,6 +127,7 @@ and gtranslated_crate_of_json vector_of_json trait_impl_id_of_json trait_impl_of_json ctx trait_impls in + let* unit_metadata = global_decl_ref_of_json ctx unit_metadata in let type_decls = TypeDeclId.Map.of_list @@ -159,6 +161,7 @@ and gtranslated_crate_of_json global_decls; trait_decls; trait_impls; + unit_metadata; } | _ -> Error "") diff --git a/charon-ml/src/LlbcAstUtils.ml b/charon-ml/src/LlbcAstUtils.ml index 09142f41c..e8b08d7dd 100644 --- a/charon-ml/src/LlbcAstUtils.ml +++ b/charon-ml/src/LlbcAstUtils.ml @@ -207,6 +207,7 @@ class ['self] map_crate_with_span = global_decls; trait_decls; trait_impls; + unit_metadata; } = crate in @@ -235,6 +236,9 @@ class ['self] map_crate_with_span = let trait_impls = TraitImplId.Map.map (self#visit_trait_impl decl_span_info) trait_impls in + let unit_metadata = + self#visit_global_decl_ref decl_span_info unit_metadata + in { name; options; @@ -245,6 +249,7 @@ class ['self] map_crate_with_span = global_decls; trait_decls; trait_impls; + unit_metadata; } end @@ -386,6 +391,7 @@ class ['self] iter_crate_with_span = global_decls; trait_decls; trait_impls; + unit_metadata; } = crate in @@ -404,7 +410,8 @@ class ['self] iter_crate_with_span = trait_decls; TraitImplId.Map.iter (fun _ -> self#visit_trait_impl decl_span_info) - trait_impls + trait_impls; + self#visit_global_decl_ref decl_span_info unit_metadata end (** For error reporting: compute which local definitions (transitively) depend diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml index 02706a7c5..1738b895c 100644 --- a/charon-ml/src/PrintExpressions.ml +++ b/charon-ml/src/PrintExpressions.ml @@ -58,6 +58,7 @@ let rec projection_elem_to_string (env : 'a fmt_env) (sub : string) | Some variant_id -> let variant_name = adt_variant_to_string env adt_id variant_id in "(" ^ sub ^ " as " ^ variant_name ^ ")." ^ field_name) + | PtrMetadata -> sub ^ ".metadata" and place_to_string (env : 'a fmt_env) (p : place) : string = match p.kind with @@ -90,7 +91,6 @@ and unop_to_string (env : 'a fmt_env) (unop : unop) : string = match unop with | Not -> "¬" | Neg om -> overflow_mode_to_string om ^ ".-" - | PtrMetadata -> "ptr_metadata" | Cast cast_kind -> cast_kind_to_string env cast_kind and overflow_mode_to_string (mode : overflow_mode) : string = @@ -145,20 +145,22 @@ and operand_to_string (env : 'a fmt_env) (op : operand) : string = and rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string = match rv with | Use op -> operand_to_string env op - | RvRef (p, bk) -> begin + | RvRef (p, bk, op) -> begin + let op = operand_to_string env op in let p = place_to_string env p in match bk with - | BShared -> "&" ^ p - | BMut -> "&mut " ^ p - | BTwoPhaseMut -> "&two-phase " ^ p - | BUniqueImmutable -> "&uniq " ^ p - | BShallow -> "&shallow " ^ p + | BShared -> "&(" ^ p ^ ", " ^ op ^ ")" + | BMut -> "&mut (" ^ p ^ ", " ^ op ^ ")" + | BTwoPhaseMut -> "&two-phase (" ^ p ^ ", " ^ op ^ ")" + | BUniqueImmutable -> "&uniq (" ^ p ^ ", " ^ op ^ ")" + | BShallow -> "&shallow (" ^ p ^ ", " ^ op ^ ")" end - | RawPtr (p, pk) -> begin + | RawPtr (p, pk, op) -> begin + let op = operand_to_string env op in let p = place_to_string env p in match pk with - | RShared -> "&raw const " ^ p - | RMut -> "&raw mut " ^ p + | RShared -> "&raw const (" ^ p ^ ", " ^ op ^ ")" + | RMut -> "&raw mut (" ^ p ^ ", " ^ op ^ ")" end | NullaryOp (op, ty) -> nullop_to_string env op ^ "<" ^ ty_to_string env ty ^ ">" diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 75be79649..9b08bde5f 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -289,7 +289,17 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = let env = fmt_env_push_regions env f.binder_regions in let fn = fn_ptr_to_string env f.binder_value in fn - | TDynTrait _ -> "dyn (TODO)" + | TDynTrait pred -> + let regions, clauses = + generic_params_to_strings env pred.binder.binder_params + in + let reg_str = + match regions with + | [] -> "" + | r :: _ -> " + " ^ r + in + "dyn (" ^ String.concat " + " clauses ^ reg_str ^ ")" + | TPtrMetadata ty -> "PtrMetadata(" ^ ty_to_string env ty ^ ")" | TError msg -> "type_error (\"" ^ msg ^ "\")" (** Return two lists: @@ -402,14 +412,14 @@ and raw_attribute_to_string (attr : raw_attribute) : string = in attr.path ^ args -let trait_param_to_string (env : 'a fmt_env) (clause : trait_param) : string = +and trait_param_to_string (env : 'a fmt_env) (clause : trait_param) : string = let clause_id = trait_clause_id_to_string env clause.clause_id in let trait = region_binder_to_string trait_decl_ref_to_string env clause.trait in "[" ^ clause_id ^ "]: " ^ trait -let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) : +and generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) : string list * string list = let ({ regions; types; const_generics; trait_clauses; _ } : generic_params) = generics diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index bfe7abdfe..1a2fdd706 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/charon-ml/src/generated/Generated_Expressions.ml @@ -245,6 +245,14 @@ and projection_elem = be used as left-values and right-values. We should never have projections to fields of symbolic variants (they should have been expanded before through a match). *) + | PtrMetadata + (** A built-in pointer (a reference, raw pointer, or [Box]) in Rust is + always a fat pointer: it contains an address and metadata for the + pointed-to place. This metadata is empty for sized types, it's the + length for slices, and the vtable for [dyn Trait]. + + We consider such pointers to be like a struct with two fields; this + represent access to the metadata "field". *) | ProjIndex of operand * bool (** MIR imposes that the argument to an index projection be a local variable, meaning that even constant indices into arrays are let-bound @@ -270,11 +278,24 @@ and projection_elem = "R" or "Rv", this would avoid collisions *) and rvalue = | Use of operand (** Lifts an operand as an rvalue. *) - | RvRef of place * borrow_kind (** Takes a reference to the given place. *) - | RawPtr of place * ref_kind + | RvRef of place * borrow_kind * operand + (** Takes a reference to the given place. The [Operand] refers to the init + value of the metadata, it is [()] if no metadata + + Fields: + - [place] + - [kind] + - [ptr_metadata] *) + | RawPtr of place * ref_kind * operand (** Takes a raw pointer with the given mutability to the given place. This is generated by pointer casts like [&v as *const _] or raw borrow - expressions like [&raw const v.] *) + expressions like [&raw const v.] Like [Ref], the [Operand] refers to + the init value of the metadata, it is [()] if no metadata. + + Fields: + - [place] + - [kind] + - [ptr_metadata] *) | BinaryOp of binop * operand * operand (** Binary operations (note that we merge "checked" and "unchecked" binops) *) @@ -306,19 +327,9 @@ and rvalue = Remark: in case of closures, the aggregated value groups the closure id together with its state. *) | Len of place * ty * const_generic option - (** Length of a memory location. The run-time length of e.g. a vector or a - slice is represented differently (but pretty-prints the same, FIXME). - Should be seen as a function of signature: - - [fn(&[T;N]) -> usize] - - [fn(&[T]) -> usize] - - We store the type argument and the const generic (the latter only for - arrays). - - [Len] is automatically introduced by rustc, notably for the bound - checks: we eliminate it together with the bounds checks whenever - possible. There are however occurrences that we don't eliminate (yet). - For instance, for the following Rust code: + (** Length of a place of type [[T]] or [[T; N]]. This applies to the place + itself, not to a pointer value. This is inserted by rustc in a single + case: slice patterns. {@rust[ fn slice_pattern_4(x: &[()]) { match x { @@ -326,9 +337,7 @@ and rvalue = _ => (), } } - ]} - rustc introduces a check that the length of the slice is exactly equal - to 1 and that we preserve. *) + ]} *) | Repeat of operand * ty * const_generic (** [Repeat(x, n)] creates an array where [x] is copied [n] times. @@ -343,9 +352,6 @@ and rvalue = and unop = | Not | Neg of overflow_mode (** This can overflow, for [-i::MIN]. *) - | PtrMetadata - (** Retreive the metadata part of a fat pointer. For slices, this - retreives their length. *) | Cast of cast_kind (** Casts are rvalues in MIR, but we treat them as unops. *) diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index c7996ecb5..734a3372e 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1336,6 +1336,7 @@ and projection_elem_of_json (ctx : of_json_ctx) (js : json) : let* x_0 = field_proj_kind_of_json ctx x_0 in let* x_1 = field_id_of_json ctx x_1 in Ok (Field (x_0, x_1)) + | `String "PtrMetadata" -> Ok PtrMetadata | `Assoc [ ("Index", `Assoc [ ("offset", offset); ("from_end", from_end) ]) ] -> let* offset = box_of_json operand_of_json ctx offset in @@ -1359,8 +1360,11 @@ and ptr_metadata_of_json (ctx : of_json_ctx) (js : json) : | `String "None" -> Ok NoMetadata | `String "Length" -> Ok Length | `Assoc [ ("VTable", v_table) ] -> - let* v_table = v_table_of_json ctx v_table in + let* v_table = type_decl_ref_of_json ctx v_table in Ok (VTable v_table) + | `Assoc [ ("InheritFrom", inherit_from) ] -> + let* inherit_from = ty_of_json ctx inherit_from in + Ok (InheritFrom inherit_from) | _ -> Error "") and raw_attribute_of_json (ctx : of_json_ctx) (js : json) : @@ -1431,14 +1435,30 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result = | `Assoc [ ("Use", use) ] -> let* use = operand_of_json ctx use in Ok (Use use) - | `Assoc [ ("Ref", `List [ x_0; x_1 ]) ] -> - let* x_0 = place_of_json ctx x_0 in - let* x_1 = borrow_kind_of_json ctx x_1 in - Ok (RvRef (x_0, x_1)) - | `Assoc [ ("RawPtr", `List [ x_0; x_1 ]) ] -> - let* x_0 = place_of_json ctx x_0 in - let* x_1 = ref_kind_of_json ctx x_1 in - Ok (RawPtr (x_0, x_1)) + | `Assoc + [ + ( "Ref", + `Assoc + [ + ("place", place); ("kind", kind); ("ptr_metadata", ptr_metadata); + ] ); + ] -> + let* place = place_of_json ctx place in + let* kind = borrow_kind_of_json ctx kind in + let* ptr_metadata = operand_of_json ctx ptr_metadata in + Ok (RvRef (place, kind, ptr_metadata)) + | `Assoc + [ + ( "RawPtr", + `Assoc + [ + ("place", place); ("kind", kind); ("ptr_metadata", ptr_metadata); + ] ); + ] -> + let* place = place_of_json ctx place in + let* kind = ref_kind_of_json ctx kind in + let* ptr_metadata = operand_of_json ctx ptr_metadata in + Ok (RawPtr (place, kind, ptr_metadata)) | `Assoc [ ("BinaryOp", `List [ x_0; x_1; x_2 ]) ] -> let* x_0 = binop_of_json ctx x_0 in let* x_1 = operand_of_json ctx x_1 in @@ -1866,6 +1886,9 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = | `Assoc [ ("FnDef", fn_def) ] -> let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in Ok (TFnDef fn_def) + | `Assoc [ ("PtrMetadata", ptr_metadata) ] -> + let* ptr_metadata = ty_of_json ctx ptr_metadata in + Ok (TPtrMetadata ptr_metadata) | `Assoc [ ("Error", error) ] -> let* error = string_of_json ctx error in Ok (TError error) @@ -1891,9 +1914,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) : let* src = item_kind_of_json ctx src in let* kind = type_decl_kind_of_json ctx kind in let* layout = option_of_json layout_of_json ctx layout in - let* ptr_metadata = - option_of_json ptr_metadata_of_json ctx ptr_metadata - in + let* ptr_metadata = ptr_metadata_of_json ctx ptr_metadata in Ok ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata } : type_decl) @@ -1990,7 +2011,6 @@ and unop_of_json (ctx : of_json_ctx) (js : json) : (unop, string) result = | `Assoc [ ("Neg", neg) ] -> let* neg = overflow_mode_of_json ctx neg in Ok (Neg neg) - | `String "PtrMetadata" -> Ok PtrMetadata | `Assoc [ ("Cast", cast) ] -> let* cast = cast_kind_of_json ctx cast in Ok (Cast cast) @@ -2009,12 +2029,6 @@ and unsizing_metadata_of_json (ctx : of_json_ctx) (js : json) : | `String "Unknown" -> Ok MetaUnknown | _ -> Error "") -and v_table_of_json (ctx : of_json_ctx) (js : json) : (v_table, string) result = - combine_error_msgs js __FUNCTION__ - (match js with - | `Null -> Ok () - | _ -> Error "") - and variant_of_json (ctx : of_json_ctx) (js : json) : (variant, string) result = combine_error_msgs js __FUNCTION__ (match js with diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index bc6e70a8e..25a69c25e 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -573,6 +573,9 @@ and ty = given that the type here is polymorpohic in the late-bound variables (those that could appear in a function pointer type like [for<'a> fn(&'a u32)]), we need to bind them here. *) + | TPtrMetadata of ty + (** As a marker of taking out metadata from a given type The internal type + is assumed to be a type variable *) | TError of string (** A type that could not be computed or was incorrect. *) (** Reference to a type declaration or builtin type. *) @@ -841,11 +844,18 @@ and path_elem = and ptr_metadata = | NoMetadata (** Types that need no metadata, namely [T: Sized] types. *) | Length - (** Metadata for [[T]], [str], and user-defined types that directly or - indirectly contain one of these two. *) - | VTable of v_table - (** Metadata for [dyn Trait] and user-defined types that directly or - indirectly contain a [dyn Trait]. *) + (** Metadata for [[T]] and [str], and user-defined types that directly or + indirectly contain one of the two. Of type [usize]. Notably, length + for [[T]] denotes the number of elements in the slice. While for [str] + it denotes the number of bytes in the string. *) + | VTable of type_decl_ref + (** Metadata for [dyn Trait], referring to the vtable struct, also for + user-defined types that directly or indirectly contain a [dyn Trait]. + Of type [&'static vtable] *) + | InheritFrom of ty + (** Unknown due to generics, but will inherit from the given type. This is + consistent with [::Metadata]. Of type + [TyKind::Metadata(Ty)]. *) (** Describes how we represent the active enum variant in memory. *) and tag_encoding = @@ -884,14 +894,8 @@ and type_decl = { (** The layout of the type. Information may be partial because of generics or dynamically- sized types. If rustc cannot compute a layout, it is [None]. *) - ptr_metadata : ptr_metadata option; - (** The metadata associated with a pointer to the type. This is [None] if - we could not compute it because of generics. The information is - *accurate* if it is [Some] while if it is [None], it may still be - theoretically computable but due to some limitation to be fixed, we - are unable to obtain the info. See - [translate_types::{impl ItemTransCtx}::translate_ptr_metadata] for - more details. *) + ptr_metadata : ptr_metadata; + (** The metadata associated with a pointer to the type. *) } and type_decl_kind = @@ -909,10 +913,6 @@ and type_decl_kind = (** Used if an error happened during the extraction, and we don't panic on error. *) -(** A placeholder for the vtable of a trait object. To be implemented in the - future when [dyn Trait] is fully supported. *) -and v_table = unit - and variant = { span : span; attr_info : attr_info; diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 820f23bd0..a74ffa327 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -201,7 +201,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.129" +version = "0.1.130" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 4702321ed..05e847c06 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.129" +version = "0.1.130" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index a2f850118..6e16a181a 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -66,6 +66,13 @@ pub enum ProjectionElem { /// We should never have projections to fields of symbolic variants (they /// should have been expanded before through a match). Field(FieldProjKind, FieldId), + /// A built-in pointer (a reference, raw pointer, or `Box`) in Rust is always a fat pointer: it + /// contains an address and metadata for the pointed-to place. This metadata is empty for sized + /// types, it's the length for slices, and the vtable for `dyn Trait`. + /// + /// We consider such pointers to be like a struct with two fields; this represent access to the + /// metadata "field". + PtrMetadata, /// MIR imposes that the argument to an index projection be a local variable, meaning /// that even constant indices into arrays are let-bound as separate variables. /// We **eliminate** this variant in a micro-pass for LLBC. @@ -157,8 +164,6 @@ pub enum UnOp { /// This can overflow, for `-i::MIN`. #[drive(skip)] Neg(OverflowMode), - /// Retreive the metadata part of a fat pointer. For slices, this retreives their length. - PtrMetadata, /// Casts are rvalues in MIR, but we treat them as unops. Cast(CastKind), } @@ -581,11 +586,21 @@ pub enum Rvalue { /// Lifts an operand as an rvalue. Use(Operand), /// Takes a reference to the given place. + /// The `Operand` refers to the init value of the metadata, it is `()` if no metadata #[charon::rename("RvRef")] - Ref(Place, BorrowKind), + Ref { + place: Place, + kind: BorrowKind, + ptr_metadata: Operand, + }, /// Takes a raw pointer with the given mutability to the given place. This is generated by /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.` - RawPtr(Place, RefKind), + /// Like `Ref`, the `Operand` refers to the init value of the metadata, it is `()` if no metadata. + RawPtr { + place: Place, + kind: RefKind, + ptr_metadata: Operand, + }, /// Binary operations (note that we merge "checked" and "unchecked" binops) BinaryOp(BinOp, Operand, Operand), /// Unary operation (e.g. not, neg) @@ -616,18 +631,8 @@ pub enum Rvalue { /// Remark: in case of closures, the aggregated value groups the closure id /// together with its state. Aggregate(AggregateKind, Vec), - /// Length of a memory location. The run-time length of e.g. a vector or a slice is - /// represented differently (but pretty-prints the same, FIXME). - /// Should be seen as a function of signature: - /// - `fn(&[T;N]) -> usize` - /// - `fn(&[T]) -> usize` - /// - /// We store the type argument and the const generic (the latter only for arrays). - /// - /// `Len` is automatically introduced by rustc, notably for the bound checks: - /// we eliminate it together with the bounds checks whenever possible. - /// There are however occurrences that we don't eliminate (yet). - /// For instance, for the following Rust code: + /// Length of a place of type `[T]` or `[T; N]`. This applies to the place itself, not to a + /// pointer value. This is inserted by rustc in a single case: slice patterns. /// ```text /// fn slice_pattern_4(x: &[()]) { /// match x { @@ -636,8 +641,6 @@ pub enum Rvalue { /// } /// } /// ``` - /// rustc introduces a check that the length of the slice is exactly equal - /// to 1 and that we preserve. Len(Place, Ty, Option), /// `Repeat(x, n)` creates an array where `x` is copied `n` times. /// diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 5965c1ae8..f6c953282 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -1,6 +1,5 @@ //! This file groups everything which is linked to implementations about [crate::expressions] use crate::ast::*; -use crate::ids::Vector; impl Place { pub fn new(local_id: LocalId, ty: Ty) -> Place { @@ -56,11 +55,11 @@ impl Place { pub fn project_auto_ty( self, - type_decls: &Vector, + krate: &TranslatedCrate, proj: ProjectionElem, ) -> Result { Ok(Place { - ty: proj.project_type(type_decls, &self.ty)?, + ty: proj.project_type(krate, &self.ty)?, kind: PlaceKind::Projection(Box::new(self), proj), }) } @@ -74,7 +73,7 @@ impl Place { tref.generics.types[0].clone() } Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..) - | FnPtr(..) | FnDef(..) | Error(..) => panic!("internal type error"), + | FnPtr(..) | FnDef(..) | PtrMetadata(..) | Error(..) => panic!("internal type error"), }; Place { ty: proj_ty, @@ -92,6 +91,22 @@ impl Place { } } +impl Operand { + pub fn mk_const_unit() -> Self { + Operand::Const(Box::new(ConstantExpr { + kind: ConstantExprKind::Adt(None, Vec::new()), + ty: Ty::mk_unit(), + })) + } + + pub fn ty(&self) -> &Ty { + match self { + Operand::Copy(place) | Operand::Move(place) => place.ty(), + Operand::Const(constant_expr) => &constant_expr.ty, + } + } +} + impl Rvalue { pub fn unit_value() -> Self { Rvalue::Aggregate( @@ -116,11 +131,7 @@ impl BorrowKind { impl ProjectionElem { /// Compute the type obtained when applying the current projection to a place of type `ty`. - pub fn project_type( - &self, - type_decls: &Vector, - ty: &Ty, - ) -> Result { + pub fn project_type(&self, krate: &TranslatedCrate, ty: &Ty) -> Result { use ProjectionElem::*; Ok(match self { Deref => { @@ -131,7 +142,7 @@ impl ProjectionElem { tref.generics.types[0].clone() } Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..) - | FnPtr(..) | FnDef(..) | Error(..) => { + | FnPtr(..) | FnDef(..) | PtrMetadata(..) | Error(..) => { // Type error return Err(()); } @@ -143,7 +154,7 @@ impl ProjectionElem { match pkind { Adt(type_decl_id, variant_id) => { // Can fail if the type declaration was not translated. - let type_decl = type_decls.get(*type_decl_id).ok_or(())?; + let type_decl = krate.type_decls.get(*type_decl_id).ok_or(())?; let tref = ty.as_adt().ok_or(())?; assert!(TypeId::Adt(*type_decl_id) == tref.id); use TypeDeclKind::*; @@ -181,6 +192,7 @@ impl ProjectionElem { .clone(), } } + PtrMetadata => ty.get_ptr_metadata(krate).into_type(), Index { .. } | Subslice { .. } => ty.as_array_or_slice().ok_or(())?.clone(), }) } diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs index 5adc463df..3b95588b9 100644 --- a/charon/src/ast/gast_utils.rs +++ b/charon/src/ast/gast_utils.rs @@ -43,6 +43,13 @@ impl Body { } impl Locals { + pub fn new(arg_count: usize) -> Self { + Self { + arg_count, + locals: Default::default(), + } + } + /// Creates a new variable and returns a place pointing to it. pub fn new_var(&mut self, name: Option, ty: Ty) -> Place { let local_id = self.locals.push_with(|index| Local { diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 9f7bca252..43e5c8d5f 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -156,6 +156,9 @@ pub struct TranslatedCrate { pub trait_decls: Vector, /// The translated trait declarations pub trait_impls: Vector, + /// A `const UNIT: () = ();` used whenever we make a thin pointer/reference to avoid creating a + /// local `let unit = ();` variable. It is always `Some`. + pub unit_metadata: Option, /// The re-ordered groups of declarations, initialized as empty. #[drive(skip)] pub ordered_decls: Option, diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index c29828c91..09326df1e 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -16,7 +16,7 @@ impl PathElem { impl Name { /// Convert a path like `["std", "alloc", "Box"]` to a name. Needed on occasion when crafting /// names that were not present in the original code. - pub(crate) fn from_path(path: &[&str]) -> Name { + pub fn from_path(path: &[&str]) -> Name { Name { name: path .iter() diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 8dbe5fe48..64c811cef 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -381,11 +381,6 @@ pub struct Layout { pub variant_layouts: Vector, } -/// A placeholder for the vtable of a trait object. -/// To be implemented in the future when `dyn Trait` is fully supported. -#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] -pub struct VTable; - /// The metadata stored in a pointer. That's the information stored in pointers alongside /// their address. It's empty for `Sized` types, and interesting for unsized /// aka dynamically-sized types. @@ -394,12 +389,20 @@ pub enum PtrMetadata { /// Types that need no metadata, namely `T: Sized` types. #[charon::rename("NoMetadata")] None, - /// Metadata for `[T]`, `str`, and user-defined types - /// that directly or indirectly contain one of these two. + /// Metadata for `[T]` and `str`, and user-defined types + /// that directly or indirectly contain one of the two. + /// Of type `usize`. + /// Notably, length for `[T]` denotes the number of elements in the slice. + /// While for `str` it denotes the number of bytes in the string. Length, - /// Metadata for `dyn Trait` and user-defined types - /// that directly or indirectly contain a `dyn Trait`. - VTable(VTable), + /// Metadata for `dyn Trait`, referring to the vtable struct, + /// also for user-defined types that directly or indirectly contain a `dyn Trait`. + /// Of type `&'static vtable` + VTable(TypeDeclRef), + /// Unknown due to generics, but will inherit from the given type. + /// This is consistent with `::Metadata`. + /// Of type `TyKind::Metadata(Ty)`. + InheritFrom(Ty), } /// A type declaration. @@ -430,12 +433,7 @@ pub struct TypeDecl { /// sized types. If rustc cannot compute a layout, it is `None`. pub layout: Option, /// The metadata associated with a pointer to the type. - /// This is `None` if we could not compute it because of generics. - /// The information is *accurate* if it is `Some` - /// while if it is `None`, it may still be theoretically computable - /// but due to some limitation to be fixed, we are unable to obtain the info. - /// See `translate_types::{impl ItemTransCtx}::translate_ptr_metadata` for more details. - pub ptr_metadata: Option, + pub ptr_metadata: PtrMetadata, } generate_index_type!(VariantId, "Variant"); @@ -822,6 +820,9 @@ pub enum TyKind { /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`), /// we need to bind them here. FnDef(RegionBinder), + /// As a marker of taking out metadata from a given type + /// The internal type is assumed to be a type variable + PtrMetadata(Ty), /// A type that could not be computed or was incorrect. #[drive(skip)] Error(String), diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 8df9a6203..e9cc33dd6 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -1,6 +1,8 @@ //! This file groups everything which is linked to implementations about [crate::types] use crate::ast::*; +use crate::formatter::IntoFormatter; use crate::ids::Vector; +use crate::pretty::FmtWithCtx; use derive_generic_visitor::*; use itertools::Itertools; use std::collections::HashSet; @@ -640,6 +642,10 @@ impl Ty { Self::mk_tuple(vec![]) } + pub fn mk_usize() -> Ty { + TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into() + } + pub fn mk_tuple(tys: Vec) -> Ty { TyKind::Adt(TypeDeclRef { id: TypeId::Tuple, @@ -696,6 +702,71 @@ impl Ty { } } + pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata { + let ref ty_decls = translated.type_decls; + match self.kind() { + TyKind::Adt(ty_ref) => { + // there are two cases: + // 1. if the declared type has a fixed metadata, just returns it + // 2. if it depends on some other types or the generic itself + match ty_ref.id { + TypeId::Adt(type_decl_id) => { + let Some(decl) = ty_decls.get(type_decl_id) else { + return PtrMetadata::InheritFrom(Ty::new(TyKind::Error(format!( + "Internal Error: type decl id not found during getting metadata: {type_decl_id}" + )))); + }; + match &decl.ptr_metadata { + // if it depends on some type, recursion with the binding env + PtrMetadata::InheritFrom(ty) => { + let ty = ty.clone().substitute(&ty_ref.generics); + ty.get_ptr_metadata(translated) + } + // otherwise, simply returns it + meta => meta.clone().substitute(&ty_ref.generics), + } + } + // the metadata of a tuple is simply the last field + TypeId::Tuple => { + match ty_ref.generics.types.iter().last() { + // `None` refers to the unit type `()` + None => PtrMetadata::None, + // Otherwise, simply recurse + Some(ty) => ty.get_ptr_metadata(translated), + } + } + // Box is a pointer like ref & raw ptr, hence no metadata + TypeId::Builtin(BuiltinTy::Box) => PtrMetadata::None, + // Array: `[T; N]` has no metadata + TypeId::Builtin(BuiltinTy::Array) => PtrMetadata::None, + // `[T]` & `str` all have metadata length + TypeId::Builtin(BuiltinTy::Slice) => PtrMetadata::Length, + TypeId::Builtin(BuiltinTy::Str) => PtrMetadata::Length, + } + } + TyKind::DynTrait(pred) => match pred.vtable_ref(translated) { + Some(vtable) => PtrMetadata::VTable(vtable), + None => PtrMetadata::InheritFrom( + TyKind::Error(format!( + "Vtable for dyn trait {} not found", + pred.with_ctx(&translated.into_fmt()) + )) + .into(), + ), + }, + TyKind::TraitType(..) | TyKind::TypeVar(_) => PtrMetadata::InheritFrom(self.clone()), + TyKind::Literal(_) + | TyKind::Never + | TyKind::Ref(..) + | TyKind::RawPtr(..) + | TyKind::FnPtr(..) + | TyKind::FnDef(..) + | TyKind::Error(_) => PtrMetadata::None, + // The metadata itself must be Sized, hence must with `PtrMetadata::None` + TyKind::PtrMetadata(_) => PtrMetadata::None, + } + } + pub fn as_array_or_slice(&self) -> Option<&Ty> { match self.kind() { TyKind::Adt(ty_ref) @@ -785,6 +856,21 @@ impl TraitRef { } } +impl PtrMetadata { + pub fn into_type(self) -> Ty { + match self { + PtrMetadata::None => Ty::mk_unit(), + PtrMetadata::Length => Ty::mk_usize(), + PtrMetadata::VTable(type_decl_ref) => Ty::new(TyKind::Ref( + Region::Static, + Ty::new(TyKind::Adt(type_decl_ref)), + RefKind::Shared, + )), + PtrMetadata::InheritFrom(ty) => Ty::new(TyKind::PtrMetadata(ty)), + } + } +} + impl Field { /// The new name for this field, as suggested by the `#[charon::rename]` attribute. pub fn renamed_name(&self) -> Option<&str> { @@ -819,6 +905,115 @@ impl Variant { } } +impl DynPredicate { + /// Get the vtable declaration reference with current generics applied. + /// Matches associated types from the vtable's generics with the dyn predicates's constraints. + /// + /// Rustc guarantees all associated types are specified in a `dyn Trait` type. + pub fn vtable_ref(&self, translated: &TranslatedCrate) -> Option { + // Get vtable_ref's ID with trait-ref's generics from dyn-self applied. + // Add associated types in correct order following the vtable's generics. + + // 0. Prepare trait name for debug/error messages + let trait_name = self.binder.params.trait_clauses[0] + .trait_ + .skip_binder + .id + .with_ctx(&translated.into_fmt()) + .to_string(); + + // 1. Get vtable ref from trait declaration + // Provides: 1) final return ID, 2) correct order of associated types + // Firstly, get the trait declaration for the vtable ref it stores. + let Some(trait_decl) = translated + .trait_decls + .get(self.binder.params.trait_clauses[0].trait_.skip_binder.id) + else { + return None; + }; + + // Get vtable ref from definition for correct ID. + // Generics in vtable ref are placeholders but provide correct order of the associated types. + let Some(vtable_ref) = &trait_decl.vtable else { + panic!( + "Vtable for trait {} is None, meaning the trait is non-dyn-compatible!", + trait_name + ); + }; + + // 2. Get correct generics for vtable ref from `dyn_self_ty` + // The binder contains all target generics info. + let binder = &self.binder; + + // 3. Prepare "basic part" of generics from trait ref (without associated types) + // The trait ref `dyn Trait<_dyn, Arg1, ..., ArgN>`, no associated types. + // First trait clause is the target one for vtable, guaranteed by `DynPredicate`. + let trait_ref = binder.params.trait_clauses[0].trait_.clone().erase(); + // Type vars (except `_dyn`) are one level deeper, move out after removing `_dyn`. + trace!( + "Getting vtable ref with trait-decl-ref {}.", + trait_ref.with_ctx(&translated.into_fmt()) + ); + let mut generics = trait_ref.generics.clone(); + // Remove the first `_dyn` type argument + generics.types.remove_and_shift_ids(TypeVarId::ZERO); + // Move out of predicate binder for `_dyn` + generics = generics.move_from_under_binder().unwrap(); + + // 4. Prepare associated types part in same order as vtable's generics + // Utilise the vtable ref form: + // `{vtable}` + // + // Use trait ID + assoc name (`Trait::AssocTy`) to uniquely identify + let assoc_tys = vtable_ref + .generics + .types + .iter() + .filter_map(|ty| { + if let TyKind::TraitType(tref, name) = &ty.kind() { + Some((tref.trait_decl_ref.skip_binder.id, name.clone())) + } else { + None + } + }) + .collect_vec(); + + // Find correct type argument from dyn trait's constraints for each assoc type. + // TODO: use proper normalization here instead of doing it by hand + for (trait_id, assoc_name) in assoc_tys { + // Find it + let Some(assoc_ty) = binder.params.trait_type_constraints.iter().find_map(|c| { + let c = c.clone().erase(); + if c.trait_ref.trait_decl_ref.skip_binder.id == trait_id + && c.type_name == assoc_name + { + // Move potentially bounded type out of `_dyn` binder + Some(c.ty.clone().move_from_under_binder().unwrap()) + } else { + None + } + }) else { + let dyn_self_ty = Ty::new(TyKind::DynTrait(self.clone())); + panic!( + "Could not find associated type {}::{} for vtable of trait {} in dyn Trait type: {}", + trait_id.with_ctx(&translated.into_fmt()), + assoc_name, + trait_name, + dyn_self_ty.with_ctx(&translated.into_fmt()) + ); + }; + // Push it + generics.types.push(assoc_ty); + } + + // 5. Return vtable ref's ID with correct generics + Some(TypeDeclRef { + id: vtable_ref.id, + generics, + }) + } +} + impl RefKind { pub fn mutable(x: bool) -> Self { if x { Self::Mut } else { Self::Shared } diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 7172ea192..51527f923 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -51,7 +51,7 @@ use indexmap::IndexMap; TranslatedCrate, TypeDeclKind, TypeId, TypeParam, TypeVarId, llbc_ast::StatementId, ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::StatementKind, ullbc_ast::TerminatorKind, ullbc_ast::SwitchTargets, - UnOp, UnsizingMetadata, Local, Variant, VariantId, LocalId, CopyNonOverlapping, Layout, VariantLayout, PtrMetadata, VTable, + UnOp, UnsizingMetadata, Local, Variant, VariantId, LocalId, CopyNonOverlapping, Layout, VariantLayout, PtrMetadata, TraitAssocTy, TraitAssocConst, TraitMethod, TraitAssocTyImpl, for Box, for Option, diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 43fbb3b89..44ce8292b 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -396,7 +396,12 @@ impl BodyTransCtx<'_, '_, '_> { } /// Translate an rvalue - fn translate_rvalue(&mut self, span: Span, rvalue: &hax::Rvalue) -> Result { + fn translate_rvalue( + &mut self, + span: Span, + rvalue: &hax::Rvalue, + tgt_ty: &Ty, + ) -> Result { match rvalue { hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)), hax::Rvalue::CopyForDeref(place) => { @@ -414,7 +419,13 @@ impl BodyTransCtx<'_, '_, '_> { hax::Rvalue::Ref(_region, borrow_kind, place) => { let place = self.translate_place(span, place)?; let borrow_kind = translate_borrow_kind(*borrow_kind); - Ok(Rvalue::Ref(place, borrow_kind)) + Ok(Rvalue::Ref { + place, + kind: borrow_kind, + // Use `()` as a placeholder now. + // Will be fixed by the cleanup pass `insert_ptr_metadata`. + ptr_metadata: Operand::mk_const_unit(), + }) } hax::Rvalue::RawPtr(mtbl, place) => { let mtbl = match mtbl { @@ -423,7 +434,13 @@ impl BodyTransCtx<'_, '_, '_> { hax::RawPtrKind::FakeForPtrMetadata => RefKind::Shared, }; let place = self.translate_place(span, place)?; - Ok(Rvalue::RawPtr(place, mtbl)) + Ok(Rvalue::RawPtr { + place, + kind: mtbl, + // Use `()` as a placeholder now. + // Will be fixed by the cleanup pass `insert_ptr_metadata`. + ptr_metadata: Operand::mk_const_unit(), + }) } hax::Rvalue::Len(place) => { let place = self.translate_place(span, place)?; @@ -556,15 +573,20 @@ impl BodyTransCtx<'_, '_, '_> { Ok(Rvalue::NullaryOp(op, ty)) } hax::Rvalue::UnaryOp(unop, operand) => { + let operand = self.translate_operand(span, operand)?; let unop = match unop { hax::UnOp::Not => UnOp::Not, hax::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap), - hax::UnOp::PtrMetadata => UnOp::PtrMetadata, + hax::UnOp::PtrMetadata => match operand { + Operand::Copy(p) | Operand::Move(p) => { + return Ok(Rvalue::Use(Operand::Copy( + p.project(ProjectionElem::PtrMetadata, tgt_ty.clone()), + ))); + } + Operand::Const(_) => panic!("const metadata"), + }, }; - Ok(Rvalue::UnaryOp( - unop, - self.translate_operand(span, operand)?, - )) + Ok(Rvalue::UnaryOp(unop, operand)) } hax::Rvalue::Discriminant(place) => { let place = self.translate_place(span, place)?; @@ -718,7 +740,7 @@ impl BodyTransCtx<'_, '_, '_> { let t_statement: Option = match &*statement.kind { hax::StatementKind::Assign((place, rvalue)) => { let t_place = self.translate_place(span, place)?; - let t_rvalue = self.translate_rvalue(span, rvalue)?; + let t_rvalue = self.translate_rvalue(span, rvalue, t_place.ty())?; Some(StatementKind::Assign(t_place, t_rvalue)) } hax::StatementKind::SetDiscriminant { diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index 37c042268..1333b641c 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -467,10 +467,7 @@ impl ItemTransCtx<'_, '_> { })), }); - let mut locals = Locals { - arg_count: 2, - locals: Vector::new(), - }; + let mut locals = Locals::new(2); let mut statements = vec![]; let mut blocks = Vector::default(); @@ -484,7 +481,12 @@ impl ItemTransCtx<'_, '_> { statements.push(mk_stt(StatementKind::Assign( reborrow.clone(), - Rvalue::Ref(deref_state, BorrowKind::Shared), + // the state must be Sized, hence `()` as ptr-metadata + Rvalue::Ref { + place: deref_state, + kind: BorrowKind::Shared, + ptr_metadata: Operand::mk_const_unit(), + }, ))); let start_block = blocks.reserve_slot(); @@ -716,10 +718,7 @@ impl ItemTransCtx<'_, '_> { generics: impl_ref.generics.clone(), }); - let mut locals = Locals { - arg_count: signature.inputs.len(), - locals: Vector::new(), - }; + let mut locals = Locals::new(signature.inputs.len()); let mut statements = vec![]; let mut blocks = Vector::default(); diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index fe984d5c6..562368d2e 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -660,6 +660,8 @@ pub fn translate<'tcx, 'ctx>( &ctx.items_to_translate ); + ctx.translate_unit_metadata_const(); + // Translate. // // For as long as the queue of items to translate is not empty, we pop the top item and diff --git a/charon/src/bin/charon-driver/translate/translate_functions.rs b/charon/src/bin/charon-driver/translate/translate_functions.rs index 2e9710796..28baee089 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions.rs @@ -9,7 +9,6 @@ use super::translate_ctx::*; use charon_lib::ast::*; use charon_lib::common::*; use charon_lib::formatter::IntoFormatter; -use charon_lib::ids::Vector; use charon_lib::pretty::FmtWithCtx; use charon_lib::ullbc_ast::*; use itertools::Itertools; @@ -107,10 +106,7 @@ impl ItemTransCtx<'_, '_> { let tref = self .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?; let output_ty = self.translate_ty(span, output_ty)?; - let mut locals = Locals { - arg_count: fields.len(), - locals: Vector::new(), - }; + let mut locals = Locals::new(fields.len()); locals.new_var(None, output_ty); let args: Vec<_> = fields .iter() diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 56b4471a3..efdcb919f 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -191,6 +191,67 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let item = self.translated.get_item(id); Ok(item.unwrap()) } + + /// Add a `const UNIT: () = ();` const, used as metadata for thin pointers/references. + pub fn translate_unit_metadata_const(&mut self) { + use charon_lib::ullbc_ast::*; + let name = Name::from_path(&["UNIT_METADATA"]); + let item_meta = ItemMeta { + name, + span: Span::dummy(), + source_text: None, + attr_info: AttrInfo::default(), + is_local: false, + opacity: ItemOpacity::Foreign, + lang_item: None, + }; + + let body = { + let mut body = GExprBody { + span: Span::dummy(), + locals: Locals::new(0), + comments: Default::default(), + body: Vector::default(), + }; + let _ = body.locals.new_var(None, Ty::mk_unit()); + body.body.push(BlockData { + statements: Default::default(), + terminator: Terminator::new(Span::dummy(), TerminatorKind::Return), + }); + body + }; + + let global_id = self.translated.global_decls.reserve_slot(); + let initializer = self.translated.fun_decls.push_with(|def_id| FunDecl { + def_id, + item_meta: item_meta.clone(), + kind: ItemKind::TopLevel, + is_global_initializer: Some(global_id), + signature: FunSig { + is_unsafe: false, + generics: Default::default(), + inputs: vec![], + output: Ty::mk_unit(), + }, + body: Ok(Body::Unstructured(body)), + }); + self.translated.global_decls.set_slot( + global_id, + GlobalDecl { + def_id: global_id, + item_meta, + generics: Default::default(), + ty: Ty::mk_unit(), + kind: ItemKind::TopLevel, + global_kind: GlobalKind::NamedConst, + init: initializer, + }, + ); + self.translated.unit_metadata = Some(GlobalDeclRef { + id: global_id, + generics: Box::new(GenericArgs::empty()), + }); + } } impl ItemTransCtx<'_, '_> { @@ -344,7 +405,7 @@ impl ItemTransCtx<'_, '_> { Err(err) => TypeDeclKind::Error(err.msg), }; let layout = self.translate_layout(def.this()); - let ptr_metadata = self.translate_ptr_metadata(def.this()); + let ptr_metadata = self.translate_ptr_metadata(span, def.this())?; let type_def = TypeDecl { def_id: trans_id, item_meta, diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index 18442aba7..b9ca84f9a 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -430,7 +430,8 @@ impl ItemTransCtx<'_, '_> { }, kind, layout: Some(layout), - ptr_metadata: None, + // A vtable struct is always sized + ptr_metadata: PtrMetadata::None, }) } } @@ -635,10 +636,7 @@ impl ItemTransCtx<'_, '_> { impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, ) -> Result { - let mut locals = Locals { - arg_count: 0, - locals: Vector::new(), - }; + let mut locals = Locals::new(0); let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone()); diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 55709c495..212794102 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -361,7 +361,11 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { /// Translate a Dynamically Sized Type metadata kind. /// /// Returns `None` if the type is generic, or if it is not a DST. - pub fn translate_ptr_metadata(&self, item: &hax::ItemRef) -> Option { + pub fn translate_ptr_metadata( + &mut self, + span: Span, + item: &hax::ItemRef, + ) -> Result { // prepare the call to the method use rustc_middle::ty; let tcx = self.t_ctx.tcx; @@ -373,23 +377,46 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .instantiate(tcx, item.rustc_args(hax_state)); // call the key method - match tcx - .struct_tail_raw( - ty, - |ty| tcx.try_normalize_erasing_regions(ty_env, ty).unwrap_or(ty), - || {}, - ) - .kind() - { - ty::Foreign(..) => Some(PtrMetadata::None), - ty::Str | ty::Slice(..) => Some(PtrMetadata::Length), - ty::Dynamic(..) => Some(PtrMetadata::VTable(VTable)), - // This is NOT accurate -- if there is no generic clause that states `?Sized` - // Then it will be safe to return `Some(PtrMetadata::None)`. - // TODO: inquire the generic clause to get the accurate info. - ty::Placeholder(..) | ty::Infer(..) | ty::Param(..) | ty::Bound(..) => None, - _ => Some(PtrMetadata::None), - } + let raw_ty = tcx.struct_tail_raw( + ty, + |ty| tcx.try_normalize_erasing_regions(ty_env, ty).unwrap_or(ty), + || {}, + ); + let hax_ty: &hax::Ty = &self.t_ctx.catch_sinto(hax_state, span, &raw_ty)?; + + let ret = match raw_ty.kind() { + ty::Foreign(..) => PtrMetadata::None, + ty::Str | ty::Slice(..) => PtrMetadata::Length, + ty::Dynamic(..) => match hax_ty.kind() { + hax::TyKind::Dynamic(_, preds, _) => { + let vtable = self + .translate_region_binder( + span, + &preds.predicates[0].0.kind, + |ctx, kind: &hax::ClauseKind| { + let hax::ClauseKind::Trait(trait_predicate) = kind else { + unreachable!() + }; + Ok(ctx + .translate_vtable_struct_ref(span, &trait_predicate.trait_ref)? + .unwrap()) + }, + )? + .erase(); + PtrMetadata::VTable(vtable) + } + _ => unreachable!("Unexpected hax type {hax_ty:?} for dynamic type: {ty:?}"), + }, + ty::Param(..) => PtrMetadata::InheritFrom(self.translate_ty(span, hax_ty)?), + ty::Placeholder(..) | ty::Infer(..) | ty::Bound(..) => { + panic!( + "We should never encounter a placeholder, infer, or bound type from ptr_metadata translation. Got: {raw_ty:?}" + ) + } + _ => PtrMetadata::None, + }; + + Ok(ret) } /// Translate a type layout. diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index f592fd10b..e47888efe 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -130,6 +130,7 @@ impl Pattern { | TyKind::DynTrait(..) | TyKind::FnPtr(..) | TyKind::FnDef(..) + | TyKind::PtrMetadata(..) | TyKind::Error(..) => false, } } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index c450a709e..fb04771e2 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1045,6 +1045,9 @@ impl FmtWithCtx for Place { write!(f, "({sub}).{field_id}") } }, + ProjectionElem::PtrMetadata => { + write!(f, "{sub}.metadata") + } ProjectionElem::Index { offset, from_end: true, @@ -1199,7 +1202,11 @@ impl FmtWithCtx for Rvalue { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Rvalue::Use(x) => write!(f, "{}", x.with_ctx(ctx)), - Rvalue::Ref(place, borrow_kind) => { + Rvalue::Ref { + place, + kind: borrow_kind, + ptr_metadata, + } => { let borrow_kind = match borrow_kind { BorrowKind::Shared => "&", BorrowKind::Mut => "&mut ", @@ -1207,14 +1214,40 @@ impl FmtWithCtx for Rvalue { BorrowKind::UniqueImmutable => "&uniq ", BorrowKind::Shallow => "&shallow ", }; - write!(f, "{borrow_kind}{}", place.with_ctx(ctx)) + if ptr_metadata.ty().is_unit() { + // Hide unit metadata + write!(f, "{borrow_kind}{}", place.with_ctx(ctx))?; + } else { + write!( + f, + "{borrow_kind}{} with_metadata({})", + place.with_ctx(ctx), + ptr_metadata.with_ctx(ctx) + )?; + } + Ok(()) } - Rvalue::RawPtr(place, mutability) => { + Rvalue::RawPtr { + place, + kind: mutability, + ptr_metadata, + } => { let ptr_kind = match mutability { RefKind::Shared => "&raw const ", RefKind::Mut => "&raw mut ", }; - write!(f, "{ptr_kind}{}", place.with_ctx(ctx)) + if ptr_metadata.ty().is_unit() { + // Hide unit metadata + write!(f, "{ptr_kind}{}", place.with_ctx(ctx))?; + } else { + write!( + f, + "{ptr_kind}{} with_metadata({})", + place.with_ctx(ctx), + ptr_metadata.with_ctx(ctx) + )?; + } + Ok(()) } Rvalue::BinaryOp(binop, x, y) => { @@ -1817,6 +1850,9 @@ impl FmtWithCtx for Ty { }; write!(f, "{value}",) } + TyKind::PtrMetadata(ty) => { + write!(f, "PtrMetadata<{}>", ty.with_ctx(ctx)) + } TyKind::Error(msg) => write!(f, "type_error(\"{msg}\")"), } } @@ -1919,7 +1955,6 @@ impl FmtWithCtx for UnOp { match self { UnOp::Not => write!(f, "~"), UnOp::Neg(mode) => write!(f, "{}.-", mode), - UnOp::PtrMetadata => write!(f, "ptr_metadata"), UnOp::Cast(kind) => write!(f, "{}", kind.with_ctx(ctx)), } } diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 65db1b0b2..a6bdeface 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -237,3 +237,18 @@ impl fmt::Display for TransformCtx { self.translated.fmt(f) } } + +/// A helper trait that captures the usual operation in body transformation. +pub trait BodyTransformCtx { + /// Create a local & return the place pointing to it + fn get_locals_mut(&mut self) -> &mut Locals; + fn insert_storage_live_stmt(&mut self, local: LocalId); + fn insert_storage_dead_stmt(&mut self, local: LocalId); + fn insert_assn_stmt(&mut self, place: Place, rvalue: Rvalue); + fn get_ctx(&self) -> &TransformCtx; + fn fresh_var(&mut self, name: Option, ty: Ty) -> Place { + let var = self.get_locals_mut().new_var(name, ty); + self.insert_storage_live_stmt(var.local_id().unwrap()); + var + } +} diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs index eb6229ce9..d7bcceac2 100644 --- a/charon/src/transform/index_to_function_calls.rs +++ b/charon/src/transform/index_to_function_calls.rs @@ -1,6 +1,9 @@ //! Desugar array/slice index operations to function calls. + use crate::llbc_ast::*; use crate::transform::TransformCtx; +use crate::transform::ctx::BodyTransformCtx; +use crate::transform::insert_ptr_metadata::{BodyTransformCtxWithParams, compute_place_metadata}; use derive_generic_visitor::*; use super::ctx::LlbcPass; @@ -11,7 +14,7 @@ use super::ctx::LlbcPass; /// We accumulate the new assignments as statements in the visitor, and at the end we insert these /// statements before the one that was just explored. #[derive(Visitor)] -struct IndexVisitor<'a> { +struct IndexVisitor<'a, 'b> { locals: &'a mut Locals, /// Statements to prepend to the statement currently being explored. statements: Vec, @@ -22,18 +25,97 @@ struct IndexVisitor<'a> { place_mutability_stack: Vec, // Span of the statement. span: Span, + ctx: &'b TransformCtx, + params: &'a GenericParams, } -impl<'a> IndexVisitor<'a> { - fn fresh_var(&mut self, name: Option, ty: Ty) -> Place { - let var = self.locals.new_var(name, ty); - let live_kind = StatementKind::StorageLive(var.local_id().unwrap()); - self.statements.push(Statement::new(self.span, live_kind)); - var +impl BodyTransformCtx for IndexVisitor<'_, '_> { + fn get_locals_mut(&mut self) -> &mut Locals { + self.locals + } + + fn insert_storage_live_stmt(&mut self, local: LocalId) { + let statement = StatementKind::StorageLive(local); + self.statements.push(Statement::new(self.span, statement)); + } + + fn insert_assn_stmt(&mut self, place: Place, rvalue: Rvalue) { + let statement = StatementKind::Assign(place, rvalue); + self.statements.push(Statement::new(self.span, statement)); + } + + fn get_ctx(&self) -> &TransformCtx { + self.ctx + } + + fn insert_storage_dead_stmt(&mut self, local: LocalId) { + let statement = StatementKind::StorageDead(local); + self.statements.push(Statement::new(self.span, statement)); } +} +impl BodyTransformCtxWithParams for IndexVisitor<'_, '_> { + fn get_params(&self) -> &GenericParams { + self.params + } +} + +/// When `from_end` is true, we need to compute `len(p) - last_arg` instead of just using `last_arg`. +/// Otherwise, we simply return `last_arg`. +/// New local variables are created as needed. +/// +/// The `last_arg` is either the `offset` for `Index` or the `to` for `Subslice` for the projections. +pub fn compute_subslice_end_idx( + ctx: &mut T, + len_place: &Place, + last_arg: Operand, + from_end: bool, +) -> Operand { + if from_end { + // `storage_live(len_var)` + // `len_var = len(p)` + let len_var = ctx.fresh_var(None, Ty::mk_usize()); + ctx.insert_assn_stmt( + len_var.clone(), + Rvalue::Len( + len_place.clone(), + len_place.ty().clone(), + len_place + .ty() + .as_adt() + .unwrap() + .generics + .const_generics + .get(0.into()) + .cloned(), + ), + ); + + // `storage_live(index_var)` + // `index_var = len_var - last_arg` + // `storage_dead(len_var)` + let index_var = ctx.fresh_var(None, Ty::mk_usize()); + ctx.insert_assn_stmt( + index_var.clone(), + Rvalue::BinaryOp( + BinOp::Sub(OverflowMode::UB), + Operand::Copy(len_var.clone()), + last_arg, + ), + ); + ctx.insert_storage_dead_stmt(len_var.local_id().unwrap()); + Operand::Copy(index_var) + } else { + last_arg + } +} + +impl<'a, 'b> IndexVisitor<'a, 'b> { + /// transform `place: subplace[i]` into indexing function calls for `subplace` and `i` fn transform_place(&mut self, mut_access: bool, place: &mut Place) { use ProjectionElem::*; + // This function is naturally called recusively, so `subplace` cannot be another `Index` or `Subslice`. + // Hence, `subplace`, if still projecting, must be either a `Deref` or a `Field`. let Some((subplace, pe @ (Index { .. } | Subslice { .. }))) = place.as_projection() else { return; }; @@ -82,6 +164,9 @@ impl<'a> IndexVisitor<'a> { .into_ty() }; + // do something similar to the `input_var` below, but for the metadata. + let ptr_metadata = compute_place_metadata(self, subplace); + // Push the statements: // `storage_live(tmp0)` // `tmp0 = &{mut}p` @@ -89,7 +174,11 @@ impl<'a> IndexVisitor<'a> { let input_var = self.fresh_var(None, input_ty); let kind = StatementKind::Assign( input_var.clone(), - Rvalue::Ref(subplace.clone(), BorrowKind::mutable(mut_access)), + Rvalue::Ref { + place: subplace.clone(), + kind: BorrowKind::mutable(mut_access), + ptr_metadata, + }, ); self.statements.push(Statement::new(self.span, kind)); input_var @@ -111,40 +200,8 @@ impl<'a> IndexVisitor<'a> { } => (x.as_ref().clone(), *from_end), _ => unreachable!(), }; - if from_end { - // `storage_live(len_var)` - // `len_var = len(p)` - let usize_ty = TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into_ty(); - let len_var = self.fresh_var(None, usize_ty.clone()); - let kind = StatementKind::Assign( - len_var.clone(), - Rvalue::Len( - subplace.clone(), - subplace.ty().clone(), - tref.generics.const_generics.get(0.into()).cloned(), - ), - ); - self.statements.push(Statement::new(self.span, kind)); - - // `storage_live(index_var)` - // `index_var = len_var - last_arg` - // `storage_dead(len_var)` - let index_var = self.fresh_var(None, usize_ty); - let kind = StatementKind::Assign( - index_var.clone(), - Rvalue::BinaryOp( - BinOp::Sub(OverflowMode::UB), - Operand::Copy(len_var.clone()), - last_arg, - ), - ); - self.statements.push(Statement::new(self.span, kind)); - let dead_kind = StatementKind::StorageDead(len_var.local_id().unwrap()); - self.statements.push(Statement::new(self.span, dead_kind)); - args.push(Operand::Copy(index_var)); - } else { - args.push(last_arg); - } + let to_idx = compute_subslice_end_idx(self, subplace, last_arg, from_end); + args.push(to_idx); // Call the indexing function: // `storage_live(tmp1)` @@ -182,8 +239,8 @@ impl<'a> IndexVisitor<'a> { } /// The visitor methods. -impl VisitBodyMut for IndexVisitor<'_> { - /// We explore places from the inside-out. +impl VisitBodyMut for IndexVisitor<'_, '_> { + /// We explore places from the inside-out --- recursion naturally happens here. fn exit_place(&mut self, place: &mut Place) { // We have intercepted every traversal that would reach a place and pushed the correct // mutability on the stack. @@ -215,12 +272,21 @@ impl VisitBodyMut for IndexVisitor<'_> { match x { // `UniqueImmutable` de facto gives mutable access and only shows up if there is nested // mutable access. - RawPtr(_, RefKind::Mut) - | Ref(_, BorrowKind::Mut | BorrowKind::TwoPhaseMut | BorrowKind::UniqueImmutable) => { - self.visit_inner_with_mutability(x, true) + RawPtr { + kind: RefKind::Mut, .. + } + | Ref { + kind: BorrowKind::Mut | BorrowKind::TwoPhaseMut | BorrowKind::UniqueImmutable, + .. + } => self.visit_inner_with_mutability(x, true), + RawPtr { + kind: RefKind::Shared, + .. + } + | Ref { + kind: BorrowKind::Shared | BorrowKind::Shallow, + .. } - RawPtr(_, RefKind::Shared) - | Ref(_, BorrowKind::Shared | BorrowKind::Shallow) | Discriminant(..) | Len(..) => self.visit_inner_with_mutability(x, false), @@ -236,6 +302,45 @@ impl VisitBodyMut for IndexVisitor<'_> { pub struct Transform; +impl Transform { + fn transform_body_with_param( + &self, + ctx: &mut TransformCtx, + b: &mut ExprBody, + params: &GenericParams, + ) { + b.body.transform(|st: &mut Statement| { + let mut visitor = IndexVisitor { + locals: &mut b.locals, + statements: Vec::new(), + place_mutability_stack: Vec::new(), + span: st.span, + ctx: &ctx, + params, + }; + use StatementKind::*; + match &mut st.kind { + Assign(..) + | SetDiscriminant(..) + | CopyNonOverlapping(_) + | Drop(..) + | Deinit(..) + | Call(..) => { + let _ = visitor.visit_inner_with_mutability(st, true); + } + Switch(..) => { + let _ = visitor.visit_inner_with_mutability(st, false); + } + Nop | Error(..) | Assert(..) | Abort(..) | StorageDead(..) | StorageLive(..) + | Return | Break(..) | Continue(..) | Loop(..) => { + let _ = st.drive_body_mut(&mut visitor); + } + } + visitor.statements + }); + } +} + /// We do the following. /// /// If `p` is a projection (for instance: `var`, `*var`, `var.f`, etc.), we @@ -295,33 +400,13 @@ pub struct Transform; /// *tmp1 = x /// ``` impl LlbcPass for Transform { - fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) { - b.body.transform(|st: &mut Statement| { - let mut visitor = IndexVisitor { - locals: &mut b.locals, - statements: Vec::new(), - place_mutability_stack: Vec::new(), - span: st.span, - }; - use StatementKind::*; - match &mut st.kind { - Assign(..) - | SetDiscriminant(..) - | CopyNonOverlapping(_) - | Drop(..) - | Deinit(..) - | Call(..) => { - let _ = visitor.visit_inner_with_mutability(st, true); - } - Switch(..) => { - let _ = visitor.visit_inner_with_mutability(st, false); - } - Nop | Error(..) | Assert(..) | Abort(..) | StorageDead(..) | StorageLive(..) - | Return | Break(..) | Continue(..) | Loop(..) => { - let _ = st.drive_body_mut(&mut visitor); - } - } - visitor.statements - }); + fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { + if let Ok(body) = &mut decl.body { + self.transform_body_with_param( + ctx, + body.as_structured_mut().unwrap(), + &decl.signature.generics, + ) + } } } diff --git a/charon/src/transform/insert_ptr_metadata.rs b/charon/src/transform/insert_ptr_metadata.rs new file mode 100644 index 000000000..6ba44bd37 --- /dev/null +++ b/charon/src/transform/insert_ptr_metadata.rs @@ -0,0 +1,218 @@ +use crate::formatter::IntoFormatter; +use crate::pretty::FmtWithCtx; +use crate::transform::TransformCtx; +use crate::transform::ctx::BodyTransformCtx; +use crate::transform::index_to_function_calls::compute_subslice_end_idx; +use crate::{transform::ctx::UllbcPass, ullbc_ast::*}; +use derive_generic_visitor::*; + +#[derive(Visitor)] +struct BodyVisitor<'a, 'b> { + locals: &'a mut Locals, + /// Statements to prepend to the statement currently being explored. + statements: Vec, + span: Span, + ctx: &'b TransformCtx, + params: &'a GenericParams, +} + +fn is_sized_type_var(ctx: &mut T, ty: &Ty) -> bool { + match ty.kind() { + TyKind::TypeVar(..) => { + if ctx.get_ctx().options.hide_marker_traits { + // If we're hiding `Sized`, let's consider everything to be sized. + return true; + } + let params = ctx.get_params(); + for clause in ¶ms.trait_clauses { + let tref = clause.trait_.clone().erase(); + // Check if it is `Sized` + if tref.generics.types[0] == *ty + && ctx + .get_ctx() + .translated + .trait_decls + .get(tref.id) + .and_then(|decl| decl.item_meta.lang_item.clone()) + == Some("sized".into()) + { + return true; + } + } + false + } + _ => false, + } +} + +/// No metadata. We use the `unit_metadata` global to avoid having to define unit locals +/// everywhere. +fn no_metadata(ctx: &T) -> Operand { + let unit_meta = ctx.get_ctx().translated.unit_metadata.clone().unwrap(); + Operand::Copy(Place::new_global(unit_meta, Ty::mk_unit())) +} + +/// Compute the metadata for a place. Return `None` if the place has no metadata. +fn compute_place_metadata_inner( + ctx: &mut T, + place: &Place, + metadata_ty: &Ty, +) -> Option { + let (subplace, proj) = place.as_projection()?; + match proj { + // The outermost deref we encountered gives us the metadata of the place. + ProjectionElem::Deref => { + let metadata_place = subplace + .clone() + .project(ProjectionElem::PtrMetadata, metadata_ty.clone()); + Some(Operand::Copy(metadata_place)) + } + ProjectionElem::Field { .. } => compute_place_metadata_inner(ctx, subplace, metadata_ty), + // Indexing for array & slice will only result in sized types, hence no metadata + ProjectionElem::Index { .. } => None, + // Ptr metadata is always sized. + ProjectionElem::PtrMetadata { .. } => None, + // Subslice must have metadata length, compute the metadata here as `to` - `from` + ProjectionElem::Subslice { from, to, from_end } => { + let to_idx = compute_subslice_end_idx(ctx, subplace, *to.clone(), *from_end); + let diff_place = ctx.fresh_var(None, Ty::mk_usize()); + ctx.insert_assn_stmt( + diff_place.clone(), + // Overflow is UB and should have been prevented by a bound check beforehand. + Rvalue::BinaryOp(BinOp::Sub(OverflowMode::UB), to_idx, *from.clone()), + ); + Some(Operand::Copy(diff_place)) + } + } +} + +/// Emit statements that compute the metadata of the given place. Returns an operand containing the +/// metadata value. +pub fn compute_place_metadata( + ctx: &mut T, + place: &Place, +) -> Operand { + trace!( + "getting ptr metadata for place: {}", + place.with_ctx(&ctx.get_ctx().into_fmt()) + ); + let metadata_ty = place + .ty() + .get_ptr_metadata(&ctx.get_ctx().translated) + .into_type(); + if metadata_ty.is_unit() + || matches!(metadata_ty.kind(), TyKind::PtrMetadata(ty) if is_sized_type_var(ctx, ty)) + { + // If the type var is known to be `Sized`, then no metadata is needed + return no_metadata(ctx); + } + trace!( + "computed metadata type: {}", + metadata_ty.with_ctx(&ctx.get_ctx().into_fmt()) + ); + compute_place_metadata_inner(ctx, place, &metadata_ty).unwrap_or_else(|| no_metadata(ctx)) +} + +pub trait BodyTransformCtxWithParams: BodyTransformCtx { + fn get_params(&self) -> &GenericParams; +} + +impl BodyTransformCtxWithParams for BodyVisitor<'_, '_> { + fn get_params(&self) -> &GenericParams { + self.params + } +} + +impl BodyTransformCtx for BodyVisitor<'_, '_> { + fn get_locals_mut(&mut self) -> &mut Locals { + self.locals + } + + fn insert_storage_live_stmt(&mut self, local: LocalId) { + self.statements + .push(Statement::new(self.span, StatementKind::StorageLive(local))); + } + + fn insert_assn_stmt(&mut self, place: Place, rvalue: Rvalue) { + self.statements.push(Statement::new( + self.span, + StatementKind::Assign(place, rvalue), + )); + } + + fn get_ctx(&self) -> &TransformCtx { + self.ctx + } + + fn insert_storage_dead_stmt(&mut self, local: LocalId) { + self.statements + .push(Statement::new(self.span, StatementKind::StorageDead(local))); + } +} + +impl VisitBodyMut for BodyVisitor<'_, '_> { + fn visit_rvalue(&mut self, x: &mut Rvalue) -> ::std::ops::ControlFlow { + if let Rvalue::Ref { + place, + ptr_metadata, + .. + } + | Rvalue::RawPtr { + place, + ptr_metadata, + .. + } = x + { + *ptr_metadata = compute_place_metadata(self, place); + } + Continue(()) + } +} + +pub struct Transform; + +impl Transform { + fn transform_body_with_param( + &self, + ctx: &mut TransformCtx, + b: &mut ExprBody, + params: &GenericParams, + ) { + b.body.iter_mut().for_each(|data| { + data.transform(|st: &mut Statement| { + let mut visitor = BodyVisitor { + locals: &mut b.locals, + statements: Vec::new(), + span: st.span, + ctx: &ctx, + params, + }; + let _ = st.drive_body_mut(&mut visitor); + visitor.statements + }); + }); + } +} + +/// This pass computes the metadata for Rvalue, which is used to create references and raw pointers. +/// E.g., in cases like: +/// ```ignore +/// let x = &[mut] (*some_v).field; +/// ``` +/// If the `(*some_v).field` is a DST, like `[i32]`, we will need to fetch the metadata, i.e., the length of the slice, +/// and store it in a local variable, then we have: +/// ```ignore +/// let x = Rvalue::Ref { place:(*some_v).field, kind: [mut], ptr_metadata: PtrMetadata(some_v) }; +/// ``` +/// There should be a new local variable introduced to store `PtrMetadata(some_v)`. +impl UllbcPass for Transform { + fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { + if let Ok(body) = &mut decl.body { + self.transform_body_with_param( + ctx, + body.as_unstructured_mut().unwrap(), + &decl.signature.generics, + ) + } + } +} diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 721ec9d97..be808b050 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -14,6 +14,7 @@ pub mod index_to_function_calls; pub mod inline_local_panic_functions; pub mod inline_promoted_consts; pub mod insert_assign_return_unit; +pub mod insert_ptr_metadata; pub mod insert_storage_lives; pub mod lift_associated_item_clauses; pub mod merge_goto_chains; @@ -32,6 +33,7 @@ pub mod remove_unused_locals; pub mod remove_unused_methods; pub mod remove_unused_self_clause; pub mod reorder_decls; +pub mod resolve_sized_ptr_metadata_inherit; pub mod simplify_constants; pub mod skip_trait_refs_when_known; pub mod ullbc_to_llbc; @@ -70,6 +72,11 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[ // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove // some sources of mutual recursion. UnstructuredBody(&skip_trait_refs_when_known::Transform), + // For the `PtrMetadata::InheritFrom` case in the type definitions + // If the given inherited type var is bounded by `Sized`, we resolve it to `None`. + NonBody(&resolve_sized_ptr_metadata_inherit::Transform), + // Compute the metadata & insert for Rvalue + UnstructuredBody(&insert_ptr_metadata::Transform), // Change trait associated types to be type parameters instead. See the module for details. NonBody(&expand_associated_types::Transform), ]; diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs index c379bb41c..ec71c8e54 100644 --- a/charon/src/transform/remove_dynamic_checks.rs +++ b/charon/src/transform/remove_dynamic_checks.rs @@ -90,16 +90,12 @@ fn remove_dynamic_checks( // We return the statements we want to keep, which must be a prefix of `block.statements`. let statements_to_keep = match statements { // Bounds checks for slices. They look like: - // l := ptr_metadata(copy a) + // l := use(copy a.metadata) // b := copy x < copy l // assert(move b == true) [ Statement { - kind: - StatementKind::Assign( - len, - Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Copy(len_op)), - ), + kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))), .. }, Statement { @@ -120,25 +116,33 @@ fn remove_dynamic_checks( .. }, rest @ .., - ] if lt_op2 == len && cond == is_in_bounds && len_op.ty().is_ref() => rest, + ] if lt_op2 == len + && cond == is_in_bounds + && let Some((_, ProjectionElem::PtrMetadata)) = len_op.as_projection() => + { + rest + } // Sometimes that instead looks like: // a := &raw const *z - // l := ptr_metadata(move a) + // l := use(copy a.metadata) // b := copy x < copy l // assert(move b == true) [ - Statement { - kind: StatementKind::Assign(reborrow, Rvalue::RawPtr(_, RefKind::Shared)), - .. - }, Statement { kind: StatementKind::Assign( - len, - Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Move(len_op)), + reborrow, + Rvalue::RawPtr { + kind: RefKind::Shared, + .. + }, ), .. }, + Statement { + kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))), + .. + }, Statement { kind: StatementKind::Assign( @@ -157,7 +161,13 @@ fn remove_dynamic_checks( .. }, rest @ .., - ] if reborrow == len_op && lt_op2 == len && cond == is_in_bounds => rest, + ] if lt_op2 == len + && cond == is_in_bounds + && let Some((slice_place, ProjectionElem::PtrMetadata)) = len_op.as_projection() + && reborrow == slice_place => + { + rest + } // Zero checks for division and remainder. They look like: // b := copy y == const 0 diff --git a/charon/src/transform/resolve_sized_ptr_metadata_inherit.rs b/charon/src/transform/resolve_sized_ptr_metadata_inherit.rs new file mode 100644 index 000000000..61bc9b777 --- /dev/null +++ b/charon/src/transform/resolve_sized_ptr_metadata_inherit.rs @@ -0,0 +1,63 @@ +use crate::{ast::*, formatter::IntoFormatter, pretty::FmtWithCtx}; + +use super::{TransformCtx, ctx::TransformPass}; + +pub struct Transform; + +impl TransformPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + // If we're hiding `Sized`, let's consider everything to be sized. + let everything_is_sized = ctx.options.hide_marker_traits; + let trait_decls = &ctx.translated.trait_decls; + let mut metadata = vec![]; + for type_decl in &ctx.translated.type_decls { + let fmt = &ctx.into_fmt(); + let meta = match &type_decl.ptr_metadata { + PtrMetadata::InheritFrom(ty) => { + match ty.kind() { + TyKind::TypeVar(..) => { + let is_sized = everything_is_sized + || type_decl.generics.trait_clauses.iter().any(|clause| { + let impl_trait = clause.trait_.clone().erase(); + impl_trait.generics.types[0] == *ty && { + let trait_decl = trait_decls.get(impl_trait.id).unwrap(); + matches!(trait_decl.item_meta.lang_item, Some("sized")) + } + }); + if is_sized { + trace!( + "Resolved ptr-metadata for type {}", + type_decl.def_id.with_ctx(fmt) + ); + PtrMetadata::None + } else { + trace!( + "Ptr-metadata for type {} inheriting from {} is not Sized, keep inheritance.", + type_decl.def_id.with_ctx(fmt), + ty.with_ctx(fmt) + ); + // Otherwise, it cannot be resolved + PtrMetadata::InheritFrom(ty.clone()) + } + } + // Will there be other cases? + _ => { + trace!( + "Non-type-var inheritance found for type: {}, inheriting from: {}", + type_decl.def_id.with_ctx(fmt), + ty.with_ctx(fmt) + ); + PtrMetadata::InheritFrom(ty.clone()) + } + } + } + x => x.clone(), + }; + metadata.push(meta); + } + let mut iter = metadata.into_iter(); + for type_decl in &mut ctx.translated.type_decls { + type_decl.ptr_metadata = iter.next().unwrap(); + } + } +} diff --git a/charon/src/transform/simplify_constants.rs b/charon/src/transform/simplify_constants.rs index 2d1851100..28e94ae9a 100644 --- a/charon/src/transform/simplify_constants.rs +++ b/charon/src/transform/simplify_constants.rs @@ -71,10 +71,18 @@ fn transform_constant_expr( } ConstantExprKind::Ref(bval) => { match bval.kind { - ConstantExprKind::Global(global_ref) => Operand::Move(new_var( - Rvalue::Ref(Place::new_global(global_ref, bval.ty), BorrowKind::Shared), - val.ty, - )), + ConstantExprKind::Global(global_ref) => { + let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit()); + Operand::Move(new_var( + // This is a reference to a global constant, which must be Sized, so no metadata + Rvalue::Ref { + place: Place::new_global(global_ref, bval.ty), + kind: BorrowKind::Shared, + ptr_metadata: Operand::Move(unit_metadata), + }, + val.ty, + )) + } _ => { // Recurse on the borrowed value let bval_ty = bval.ty.clone(); @@ -83,8 +91,18 @@ fn transform_constant_expr( // Evaluate the referenced value let bvar = new_var(Rvalue::Use(bval), bval_ty); + let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit()); + // Borrow the value - let ref_var = new_var(Rvalue::Ref(bvar, BorrowKind::Shared), val.ty); + // As the value is originally an argument, it must be Sized + let ref_var = new_var( + Rvalue::Ref { + place: bvar, + kind: BorrowKind::Shared, + ptr_metadata: Operand::Move(unit_metadata), + }, + val.ty, + ); Operand::Move(ref_var) } @@ -92,10 +110,18 @@ fn transform_constant_expr( } ConstantExprKind::Ptr(rk, bval) => { match bval.kind { - ConstantExprKind::Global(global_ref) => Operand::Move(new_var( - Rvalue::RawPtr(Place::new_global(global_ref, bval.ty), rk), - val.ty, - )), + ConstantExprKind::Global(global_ref) => { + let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit()); + Operand::Move(new_var( + // This is a raw pointer to a global constant, which must be Sized, so no metadata + Rvalue::RawPtr { + place: Place::new_global(global_ref, bval.ty), + kind: rk, + ptr_metadata: Operand::Move(unit_metadata), + }, + val.ty, + )) + } _ => { // Recurse on the borrowed value let bval_ty = bval.ty.clone(); @@ -104,8 +130,18 @@ fn transform_constant_expr( // Evaluate the referenced value let bvar = new_var(Rvalue::Use(bval), bval_ty); + let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit()); + // Borrow the value - let ref_var = new_var(Rvalue::RawPtr(bvar, rk), val.ty); + // As the value is originally an argument, it must be Sized, hence no metadata + let ref_var = new_var( + Rvalue::RawPtr { + place: bvar, + kind: rk, + ptr_metadata: Operand::Move(unit_metadata), + }, + val.ty, + ); Operand::Move(ref_var) } diff --git a/charon/tests/cargo/build-script.out b/charon/tests/cargo/build-script.out index 2d9cb5979..c851748a7 100644 --- a/charon/tests/cargo/build-script.out +++ b/charon/tests/cargo/build-script.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_cargo_build_script::FOO pub fn FOO() -> u8 { diff --git a/charon/tests/cargo/dependencies.out b/charon/tests/cargo/dependencies.out index 71b08e3fe..0c23d238d 100644 --- a/charon/tests/cargo/dependencies.out +++ b/charon/tests/cargo/dependencies.out @@ -68,6 +68,16 @@ where [@TraitClause2]: FnOnce, @TraitClause2::Output = T, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_cargo_dependencies::main::silly_incr::closure struct closure {} diff --git a/charon/tests/cargo/toml.out b/charon/tests/cargo/toml.out index a04bc3120..359b0e49a 100644 --- a/charon/tests/cargo/toml.out +++ b/charon/tests/cargo/toml.out @@ -37,6 +37,16 @@ where return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_cargo_toml::main fn main() { diff --git a/charon/tests/cargo/unsafe_.out b/charon/tests/cargo/unsafe_.out index 2251cda76..e6fc4169b 100644 --- a/charon/tests/cargo/unsafe_.out +++ b/charon/tests/cargo/unsafe_.out @@ -12,6 +12,16 @@ pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : u // Full name: std::io::stdio::_print pub fn _print<'_0>(@1: Arguments<'_0>) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: unsafe::main fn main() { diff --git a/charon/tests/cargo/workspace.out b/charon/tests/cargo/workspace.out index bca0b1347..ecf1e05d9 100644 --- a/charon/tests/cargo/workspace.out +++ b/charon/tests/cargo/workspace.out @@ -9,6 +9,16 @@ pub fn random_number() -> u32 return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: crate2::extra_random_number pub fn extra_random_number() -> u32 { diff --git a/charon/tests/cli.rs b/charon/tests/cli.rs index 1abe9179a..5d1726f17 100644 --- a/charon/tests/cli.rs +++ b/charon/tests/cli.rs @@ -104,12 +104,6 @@ fn charon_cargo_features() -> Result<()> { "Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {main:?}." ); - let count_fn = stdout.matches("fn").count(); - ensure!( - count_fn == 1, - "Output of `{cmd}` is:\n{stdout:?}\nThe count of `fn` should only be one." - ); - ensure!( !stdout.contains(take_mut), "Output of `{cmd}` is:\n{stdout:?}\nIt shouldn't contain {take_mut:?}." @@ -123,7 +117,6 @@ fn charon_cargo_target() -> Result<()> { let target = "riscv64gc-unknown-none-elf"; let dir = "tests/cargo/multi-targets"; - let fn_ = "pub fn"; #[cfg(target_family = "unix")] charon(&["cargo", "--print-llbc"], dir, |stdout, cmd| { @@ -132,12 +125,6 @@ fn charon_cargo_target() -> Result<()> { stdout.contains(main), "Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {main:?}." ); - - let count_fn = stdout.matches(fn_).count(); - ensure!( - count_fn == 1, - "Output of `{cmd}` is:\n{stdout:?}\nThe count of {fn_:?} should only be one." - ); Ok(()) })?; @@ -148,12 +135,6 @@ fn charon_cargo_target() -> Result<()> { stdout.contains(main), "Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {main:?}." ); - - let count_fn = stdout.matches(fn_).count(); - ensure!( - count_fn == 1, - "Output of `{cmd}` is:\n{stdout:?}\nThe count of {fn_:?} should only be one." - ); Ok(()) })?; @@ -164,12 +145,6 @@ fn charon_cargo_target() -> Result<()> { stdout.contains(main), "Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {main:?}." ); - - let count_fn = stdout.matches(fn_).count(); - ensure!( - count_fn == 1, - "Output of `{cmd}` is:\n{stdout:?}\nThe count of {fn_:?} should only be one." - ); Ok(()) }) } @@ -187,12 +162,6 @@ fn charon_rustc() -> Result<()> { stdout.contains(fn_), "Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {fn_:?}." ); - - let count_fn = stdout.matches("fn").count(); - ensure!( - count_fn == 1, - "Output of `{cmd}` is:\n{stdout:?}\nThe count of `fn` should only be one." - ); Ok(()) }) } diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index f538b9c28..7cadbf8b9 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -93,7 +93,7 @@ fn spans() -> anyhow::Result<()> { } ", )?; - let function = &crate_data.fun_decls[0]; + let function = &crate_data.fun_decls[1]; // Span of the whole function. assert_eq!(repr_span(function.item_meta.span), "2:8-10:9"); @@ -292,20 +292,20 @@ fn attributes() -> anyhow::Result<()> { vec!["clippy::foo"] ); assert_eq!( - unknown_attrs(&crate_data.global_decls[0].item_meta), + unknown_attrs(&crate_data.global_decls[1].item_meta), vec!["clippy::foo"] ); assert_eq!( - unknown_attrs(&crate_data.global_decls[1].item_meta), + unknown_attrs(&crate_data.global_decls[2].item_meta), vec!["clippy::foo"] ); - assert!(unknown_attrs(&crate_data.fun_decls[0].item_meta).is_empty()); + assert!(unknown_attrs(&crate_data.fun_decls[1].item_meta).is_empty()); assert_eq!( - crate_data.fun_decls[0].item_meta.attr_info.inline, + crate_data.fun_decls[1].item_meta.attr_info.inline, Some(InlineAttr::Never) ); assert_eq!( - crate_data.fun_decls[0] + crate_data.fun_decls[1] .item_meta .attr_info .attributes @@ -458,7 +458,7 @@ fn rename_attribute() -> anyhow::Result<()> { ); assert_eq!( - crate_data.fun_decls[0] + crate_data.fun_decls[1] .item_meta .attr_info .rename @@ -467,7 +467,7 @@ fn rename_attribute() -> anyhow::Result<()> { ); assert_eq!( - crate_data.fun_decls[1] + crate_data.fun_decls[2] .item_meta .attr_info .rename @@ -476,7 +476,7 @@ fn rename_attribute() -> anyhow::Result<()> { ); assert_eq!( - crate_data.fun_decls[2] + crate_data.fun_decls[3] .item_meta .attr_info .rename @@ -485,7 +485,7 @@ fn rename_attribute() -> anyhow::Result<()> { ); assert_eq!( - crate_data.fun_decls[4] + crate_data.fun_decls[5] .item_meta .attr_info .rename @@ -539,7 +539,7 @@ fn rename_attribute() -> anyhow::Result<()> { ); assert_eq!( - crate_data.global_decls[0] + crate_data.global_decls[1] .item_meta .attr_info .rename @@ -580,10 +580,11 @@ fn declaration_groups() -> anyhow::Result<()> { "#, )?; - // There are two function items: one for `foo`, one for the initializer of `Trait::FOO`. - assert_eq!(crate_data.fun_decls.iter().count(), 2); + // There are 3 function items: one for `foo`, one for the initializer of `Trait::FOO`, and + // one for the initializer of UNIT_METADATA (always included). + assert_eq!(crate_data.fun_decls.iter().count(), 3); let decl_groups = crate_data.ordered_decls.unwrap(); - assert_eq!(decl_groups.len(), 6); + assert_eq!(decl_groups.len(), 8); Ok(()) } @@ -638,7 +639,7 @@ fn known_trait_method_call() -> Result<(), Box> { } "#, )?; - let function = &crate_data.fun_decls[0]; + let function = &crate_data.fun_decls[1]; assert_eq!( repr_name(&crate_data, &function.item_meta.name), "test_crate::use_default" diff --git a/charon/tests/dynamic-sized-type-info.rs b/charon/tests/dynamic-sized-type-info.rs index 44eb21e4a..c4ae026a3 100644 --- a/charon/tests/dynamic-sized-type-info.rs +++ b/charon/tests/dynamic-sized-type-info.rs @@ -45,6 +45,10 @@ fn ptr_metadata() -> anyhow::Result<()> { x: u32, y: T, } + struct GenericWithUnsize { + x: u32, + y: T + } struct GenericNotLastField { x: u32, y: T, @@ -54,6 +58,10 @@ fn ptr_metadata() -> anyhow::Result<()> { x: u32, y: Box, } + struct GenericBehindIndirectionUnsized { + x: u32, + y: Box, + } // Charon doesn't recognize that we know the metadata in this case. That's ok. struct ThinGeneric { x: u32, @@ -62,12 +70,12 @@ fn ptr_metadata() -> anyhow::Result<()> { "#, &[], )?; - let meta_kinds: IndexMap> = crate_data + let meta_kinds: IndexMap = crate_data .type_decls .iter() .map(|td| { let name = repr_name(&crate_data, &td.item_meta.name); - (name, td.ptr_metadata.as_ref()) + (name, &td.ptr_metadata) }) .collect(); let str = serde_json::to_string_pretty(&meta_kinds)?; diff --git a/charon/tests/ptr-metadata.json b/charon/tests/ptr-metadata.json index 8e1dcc938..e4e326d66 100644 --- a/charon/tests/ptr-metadata.json +++ b/charon/tests/ptr-metadata.json @@ -6,13 +6,31 @@ "test_crate::MoreSliceDst": "Length", "test_crate::Embedded": "Length", "test_crate::DynTrait": { - "VTable": null + "VTable": { + "id": { + "Adt": 13 + }, + "generics": { + "regions": [], + "types": [], + "const_generics": [], + "trait_refs": [] + } + } + }, + "test_crate::GenericInLastField": "None", + "test_crate::GenericWithUnsize": { + "InheritFrom": { + "TypeVar": { + "Free": 0 + } + } }, - "test_crate::GenericInLastField": null, "test_crate::GenericNotLastField": "None", "test_crate::GenericBehindIndirection": "None", - "test_crate::ThinGeneric": null, - "test_crate::Showable::{vtable}": null, + "test_crate::GenericBehindIndirectionUnsized": "None", + "test_crate::ThinGeneric": "None", + "test_crate::Showable::{vtable}": "None", "alloc::alloc::Global": "None", "core::cmp::Ordering": "None", "core::option::Option": "None", diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 16b06f3c9..b50c1cd29 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -268,6 +268,16 @@ pub fn len<'_0, T>(@1: &'_0 (Slice)) -> usize where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::AB pub enum AB { A, @@ -320,7 +330,7 @@ where @3 := &mut *(s@1) @2 := @ArrayToSliceMut<'_, T, 32 : usize>(move (@3)) storage_dead(@3) - @0 := &mut *(@2) + @0 := &mut *(@2) with_metadata(copy (@2.metadata)) storage_dead(@2) return } @@ -376,7 +386,7 @@ where let @2: &'_ (Slice); // anonymous local storage_live(@2) - @2 := &*(s@1) + @2 := &*(s@1) with_metadata(copy (s@1.metadata)) @0 := len<'_, T>[@TraitClause0](move (@2)) storage_dead(@2) return @@ -498,7 +508,7 @@ where storage_live(@4) @4 := copy (i@2) storage_live(@5) - @5 := &*(s@1) + @5 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@6) @6 := @SliceIndexShared<'_, T>(move (@5), copy (@4)) @3 := &*(@6) @@ -527,7 +537,7 @@ where storage_live(@5) @5 := copy (i@2) storage_live(@6) - @6 := &mut *(s@1) + @6 := &mut *(s@1) with_metadata(copy (s@1.metadata)) storage_live(@7) @7 := @SliceIndexMut<'_, T>(move (@6), copy (@5)) @4 := &mut *(@7) @@ -556,7 +566,7 @@ pub fn slice_subslice_shared_<'_0>(@1: &'_0 (Slice), @2: usize, @3: usize) storage_live(@4) storage_live(@5) storage_live(@6) - @6 := &*(x@1) + @6 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@7) storage_live(@8) @8 := copy (y@2) @@ -568,8 +578,8 @@ pub fn slice_subslice_shared_<'_0>(@1: &'_0 (Slice), @2: usize, @3: usize) @5 := {impl Index for Slice}::index<'_, u32, Range[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]](move (@6), move (@7)) storage_dead(@7) storage_dead(@6) - @4 := &*(@5) - @0 := &*(@4) + @4 := &*(@5) with_metadata(copy (@5.metadata)) + @0 := &*(@4) with_metadata(copy (@4.metadata)) storage_dead(@5) storage_dead(@4) return @@ -594,7 +604,7 @@ pub fn slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice), @2: usize, @3: usize) storage_live(@5) storage_live(@6) storage_live(@7) - @7 := &mut *(x@1) + @7 := &mut *(x@1) with_metadata(copy (x@1.metadata)) storage_live(@8) storage_live(@9) @9 := copy (y@2) @@ -606,9 +616,9 @@ pub fn slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice), @2: usize, @3: usize) @6 := {impl IndexMut for Slice}::index_mut<'_, u32, Range[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]](move (@7), move (@8)) storage_dead(@8) storage_dead(@7) - @5 := &mut *(@6) - @4 := &mut *(@5) - @0 := &mut *(@4) + @5 := &mut *(@6) with_metadata(copy (@6.metadata)) + @4 := &mut *(@5) with_metadata(copy (@5.metadata)) + @0 := &mut *(@4) with_metadata(copy (@4.metadata)) storage_dead(@6) storage_dead(@5) storage_dead(@4) @@ -642,7 +652,7 @@ pub fn array_to_slice_mut_<'_0>(@1: &'_0 mut (Array)) -> &'_0 m @3 := &mut *(x@1) @2 := @ArrayToSliceMut<'_, u32, 32 : usize>(move (@3)) storage_dead(@3) - @0 := &mut *(@2) + @0 := &mut *(@2) with_metadata(copy (@2.metadata)) storage_dead(@2) return } @@ -676,8 +686,8 @@ pub fn array_subslice_shared_<'_0>(@1: &'_0 (Array), @2: usize, @5 := {impl Index for Array}::index<'_, u32, Range[Sized], Slice, 32 : usize>[Sized, Sized[Sized]>, {impl Index for Slice}[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]]](move (@6), move (@7)) storage_dead(@7) storage_dead(@6) - @4 := &*(@5) - @0 := &*(@4) + @4 := &*(@5) with_metadata(copy (@5.metadata)) + @0 := &*(@4) with_metadata(copy (@4.metadata)) storage_dead(@5) storage_dead(@4) return @@ -714,9 +724,9 @@ pub fn array_subslice_mut_<'_0>(@1: &'_0 mut (Array), @2: usize @6 := {impl IndexMut for Array}::index_mut<'_, u32, Range[Sized], Slice, 32 : usize>[Sized, Sized[Sized]>, {impl IndexMut for Slice}[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]]](move (@7), move (@8)) storage_dead(@8) storage_dead(@7) - @5 := &mut *(@6) - @4 := &mut *(@5) - @0 := &mut *(@4) + @5 := &mut *(@6) with_metadata(copy (@6.metadata)) + @4 := &mut *(@5) with_metadata(copy (@5.metadata)) + @0 := &mut *(@4) with_metadata(copy (@4.metadata)) storage_dead(@6) storage_dead(@5) storage_dead(@4) @@ -739,7 +749,7 @@ where storage_live(@3) @3 := const (0 : usize) storage_live(@4) - @4 := &*(s@1) + @4 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@5) @5 := @SliceIndexShared<'_, T>(move (@4), copy (@3)) @2 := &*(@5) @@ -888,12 +898,12 @@ pub fn incr_slice_self<'_0>(@1: &'_0 mut (Slice)) storage_live(@2) @2 := const (0 : usize) storage_live(@6) - @6 := &*(s@1) + @6 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@7) @7 := @SliceIndexShared<'_, u32>(move (@6), copy (@2)) @3 := copy (*(@7)) panic.+ const (1 : u32) storage_live(@4) - @4 := &mut *(s@1) + @4 := &mut *(s@1) with_metadata(copy (s@1.metadata)) storage_live(@5) @5 := @SliceIndexMut<'_, u32>(move (@4), copy (@2)) *(@5) := move (@3) @@ -1128,7 +1138,7 @@ pub fn index_slice_u32_0<'_0>(@1: &'_0 (Slice)) -> u32 storage_live(@2) @2 := const (0 : usize) storage_live(@3) - @3 := &*(x@1) + @3 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@4) @4 := @SliceIndexShared<'_, u32>(move (@3), copy (@2)) @0 := copy (*(@4)) @@ -1148,7 +1158,7 @@ pub fn index_mut_slice_u32_0<'_0>(@1: &'_0 mut (Slice)) -> u32 storage_live(@2) @2 := const (0 : usize) storage_live(@3) - @3 := &*(x@1) + @3 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@4) @4 := @SliceIndexShared<'_, u32>(move (@3), copy (@2)) @0 := copy (*(@4)) @@ -1330,7 +1340,7 @@ pub fn update_mut_slice<'_0>(@1: &'_0 mut (Slice)) storage_live(@2) @2 := const (0 : usize) storage_live(@3) - @3 := &mut *(x@1) + @3 := &mut *(x@1) with_metadata(copy (x@1.metadata)) storage_live(@4) @4 := @SliceIndexMut<'_, u32>(move (@3), copy (@2)) *(@4) := const (1 : u32) @@ -1424,8 +1434,8 @@ pub fn range_all() @5 := {impl IndexMut for Array}::index_mut<'_, u32, Range[Sized], Slice, 4 : usize>[Sized, Sized[Sized]>, {impl IndexMut for Slice}[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]]](move (@6), move (@7)) storage_dead(@7) storage_dead(@6) - @4 := &mut *(@5) - @3 := &two-phase-mut *(@4) + @4 := &mut *(@5) with_metadata(copy (@5.metadata)) + @3 := &two-phase-mut *(@4) with_metadata(copy (@4.metadata)) @2 := update_mut_slice<'_>(move (@3)) storage_dead(@3) storage_dead(@5) @@ -1568,7 +1578,7 @@ pub fn sum<'_0>(@1: &'_0 (Slice)) -> u32 @6 := copy (i@3) storage_live(@7) storage_live(@8) - @8 := &*(s@1) + @8 := &*(s@1) with_metadata(copy (s@1.metadata)) @7 := len<'_, u32>[Sized](move (@8)) storage_dead(@8) @5 := move (@6) < move (@7) @@ -1583,7 +1593,7 @@ pub fn sum<'_0>(@1: &'_0 (Slice)) -> u32 storage_live(@10) @10 := copy (i@3) storage_live(@14) - @14 := &*(s@1) + @14 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@15) @15 := @SliceIndexShared<'_, u32>(move (@14), copy (@10)) @9 := copy (*(@15)) @@ -1660,12 +1670,12 @@ pub fn sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u32 storage_live(@5) storage_live(@6) storage_live(@7) - @7 := &*(s@1) + @7 := &*(s@1) with_metadata(copy (s@1.metadata)) @6 := len<'_, u32>[Sized](move (@7)) storage_dead(@7) storage_live(@8) storage_live(@9) - @9 := &*(s2@2) + @9 := &*(s2@2) with_metadata(copy (s2@2.metadata)) @8 := len<'_, u32>[Sized](move (@9)) storage_dead(@9) @5 := move (@6) == move (@8) @@ -1689,7 +1699,7 @@ pub fn sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u32 @13 := copy (i@10) storage_live(@14) storage_live(@15) - @15 := &*(s@1) + @15 := &*(s@1) with_metadata(copy (s@1.metadata)) @14 := len<'_, u32>[Sized](move (@15)) storage_dead(@15) @12 := move (@13) < move (@14) @@ -1705,7 +1715,7 @@ pub fn sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u32 storage_live(@18) @18 := copy (i@10) storage_live(@27) - @27 := &*(s@1) + @27 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@28) @28 := @SliceIndexShared<'_, u32>(move (@27), copy (@18)) @17 := copy (*(@28)) @@ -1713,7 +1723,7 @@ pub fn sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u32 storage_live(@20) @20 := copy (i@10) storage_live(@25) - @25 := &*(s2@2) + @25 := &*(s2@2) with_metadata(copy (s2@2.metadata)) storage_live(@26) @26 := @SliceIndexShared<'_, u32>(move (@25), copy (@20)) @19 := copy (*(@26)) @@ -1768,7 +1778,7 @@ pub fn f0() storage_live(@5) @5 := const (0 : usize) storage_live(@6) - @6 := &mut *(s@1) + @6 := &mut *(s@1) with_metadata(copy (s@1.metadata)) storage_live(@7) @7 := @SliceIndexMut<'_, u32>(move (@6), copy (@5)) *(@7) := const (1 : u32) @@ -1845,8 +1855,8 @@ pub fn f4<'_0>(@1: &'_0 (Array), @2: usize, @3: usize) -> &'_0 @5 := {impl Index for Array}::index<'_, u32, Range[Sized], Slice, 32 : usize>[Sized, Sized[Sized]>, {impl Index for Slice}[Sized], Slice>[Sized, Sized[Sized]>, {impl SliceIndex, Slice> for Range[Sized]}[Sized]]](move (@6), move (@7)) storage_dead(@7) storage_dead(@6) - @4 := &*(@5) - @0 := &*(@4) + @4 := &*(@5) with_metadata(copy (@5.metadata)) + @0 := &*(@4) with_metadata(copy (@4.metadata)) storage_dead(@5) storage_dead(@4) return @@ -1902,7 +1912,7 @@ pub fn f3() -> u32 @12 := &b@5 @11 := &*(@12) @10 := f4<'_>(move (@11), const (16 : usize), const (18 : usize)) - @9 := &*(@10) + @9 := &*(@10) with_metadata(copy (@10.metadata)) storage_dead(@11) @0 := sum2<'_, '_>(move (@6), move (@9)) storage_dead(@9) @@ -2040,7 +2050,7 @@ pub fn zero_slice<'_0>(@1: &'_0 mut (Slice)) i@2 := const (0 : usize) storage_live(len@3) storage_live(@4) - @4 := &*(a@1) + @4 := &*(a@1) with_metadata(copy (a@1.metadata)) len@3 := len<'_, u8>[Sized](move (@4)) storage_dead(@4) loop { @@ -2056,7 +2066,7 @@ pub fn zero_slice<'_0>(@1: &'_0 mut (Slice)) storage_live(@8) @8 := copy (i@2) storage_live(@11) - @11 := &mut *(a@1) + @11 := &mut *(a@1) with_metadata(copy (a@1.metadata)) storage_live(@12) @12 := @SliceIndexMut<'_, u8>(move (@11), copy (@8)) *(@12) := const (0 : u8) @@ -2099,7 +2109,7 @@ pub fn iter_mut_slice<'_0>(@1: &'_0 mut (Slice)) storage_live(@8) storage_live(len@2) storage_live(@3) - @3 := &*(a@1) + @3 := &*(a@1) with_metadata(copy (a@1.metadata)) len@2 := len<'_, u8>[Sized](move (@3)) storage_dead(@3) storage_live(i@4) @@ -2173,7 +2183,7 @@ pub fn sum_mut_slice<'_0>(@1: &'_0 mut (Slice)) -> u32 @6 := copy (i@2) storage_live(@7) storage_live(@8) - @8 := &*(a@1) + @8 := &*(a@1) with_metadata(copy (a@1.metadata)) @7 := len<'_, u32>[Sized](move (@8)) storage_dead(@8) @5 := move (@6) < move (@7) @@ -2188,7 +2198,7 @@ pub fn sum_mut_slice<'_0>(@1: &'_0 mut (Slice)) -> u32 storage_live(@10) @10 := copy (i@2) storage_live(@14) - @14 := &*(a@1) + @14 := &*(a@1) with_metadata(copy (a@1.metadata)) storage_live(@15) @15 := @SliceIndexShared<'_, u32>(move (@14), copy (@10)) @9 := copy (*(@15)) @@ -2325,7 +2335,7 @@ fn slice_pattern_4<'_0>(@1: &'_0 (Slice<()>)) } storage_live(_named@5) storage_live(@6) - @6 := &*(x@1) + @6 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@7) @7 := @SliceIndexShared<'_, ()>(move (@6), const (0 : usize)) _named@5 := &*(@7) diff --git a/charon/tests/ui/arrays_const_generics.out b/charon/tests/ui/arrays_const_generics.out index aaf89da4f..27555f1ee 100644 --- a/charon/tests/ui/arrays_const_generics.out +++ b/charon/tests/ui/arrays_const_generics.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::index_array_generic pub fn index_array_generic(@1: Array, @2: usize) -> u32 { diff --git a/charon/tests/ui/assoc-const-with-generics.out b/charon/tests/ui/assoc-const-with-generics.out index a00cd650e..ca8756a25 100644 --- a/charon/tests/ui/assoc-const-with-generics.out +++ b/charon/tests/ui/assoc-const-with-generics.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::V struct V where diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index 6258d21eb..702f9240d 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -145,6 +145,16 @@ pub fn to_owned<'_0, Self, Clause0_Owned>(@1: &'_0 (Self)) -> Clause0_Owned where [@TraitClause0]: ToOwned, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + trait test_crate::Foo<'a, Self, Self_Item> where Self_Item : 'a, diff --git a/charon/tests/ui/bitwise.out b/charon/tests/ui/bitwise.out index 55481eb19..6a6bc996f 100644 --- a/charon/tests/ui/bitwise.out +++ b/charon/tests/ui/bitwise.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::shift_u32 pub fn shift_u32(@1: u32) -> u32 { diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out index 7b5d785bf..582d25c37 100644 --- a/charon/tests/ui/call-to-known-trait-method.out +++ b/charon/tests/ui/call-to-known-trait-method.out @@ -108,6 +108,16 @@ where #[lang_item("String")] pub opaque type String +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Struct struct Struct where diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index 28981feac..a00118792 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::main::closure struct closure {} diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index f85a55196..87f180e36 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -146,6 +146,16 @@ where non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::incr_u32 pub fn incr_u32(@1: u32) -> u32 { diff --git a/charon/tests/ui/closures_with_where.out b/charon/tests/ui/closures_with_where.out index 25ee8b690..c1754e923 100644 --- a/charon/tests/ui/closures_with_where.out +++ b/charon/tests/ui/closures_with_where.out @@ -75,6 +75,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Ops trait Ops { diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index ace98cb42..a7e52a6b8 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -79,6 +79,16 @@ pub fn len<'_0, T>(@1: &'_0 (Slice)) -> usize where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::function_call fn function_call(@1: u32) { @@ -161,7 +171,7 @@ pub fn sum<'_0>(@1: &'_0 (Slice)) -> u32 @10 := copy (i@3) storage_live(@11) storage_live(@12) - @12 := &*(s@1) + @12 := &*(s@1) with_metadata(copy (s@1.metadata)) @11 := len<'_, u32>[Sized](move (@12)) storage_dead(@12) @9 := move (@10) < move (@11) @@ -177,7 +187,7 @@ pub fn sum<'_0>(@1: &'_0 (Slice)) -> u32 // Add to running sum @14 := copy (i@3) storage_live(@27) - @27 := &*(s@1) + @27 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@28) @28 := @SliceIndexShared<'_, u32>(move (@27), copy (@14)) @13 := copy (*(@28)) diff --git a/charon/tests/ui/constants.out b/charon/tests/ui/constants.out index 5c7a90ebf..5617d5378 100644 --- a/charon/tests/ui/constants.out +++ b/charon/tests/ui/constants.out @@ -32,6 +32,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::X0 pub fn X0() -> u32 { @@ -374,13 +384,16 @@ pub fn S2() -> u32 let @0: u32; // return let @1: u32; // anonymous local let @2: &'_ (u32); // anonymous local - let @3: &'_ (u32); // anonymous local + let @3: (); // anonymous local + let @4: &'_ (u32); // anonymous local storage_live(@3) + storage_live(@4) storage_live(@1) storage_live(@2) - @3 := &S1 - @2 := move (@3) + @3 := () + @4 := &S1 + @2 := move (@4) @1 := copy (*(@2)) @0 := incr(move (@1)) storage_dead(@2) diff --git a/charon/tests/ui/copy_nonoverlapping.out b/charon/tests/ui/copy_nonoverlapping.out index 70b60c550..28bbf2182 100644 --- a/charon/tests/ui/copy_nonoverlapping.out +++ b/charon/tests/ui/copy_nonoverlapping.out @@ -61,6 +61,16 @@ where return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::write fn write<'_0, '_1, T>(@1: &'_0 mut (T), @2: &'_1 (T)) where diff --git a/charon/tests/ui/cross_compile_32_bit.out b/charon/tests/ui/cross_compile_32_bit.out index 122064a40..bab3307bf 100644 --- a/charon/tests/ui/cross_compile_32_bit.out +++ b/charon/tests/ui/cross_compile_32_bit.out @@ -13,6 +13,16 @@ pub opaque type NonNull // Full name: core::ptr::non_null::{NonNull}::new_unchecked pub unsafe fn new_unchecked(@1: *mut T) -> NonNull +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasPointerNiche enum HasPointerNiche { First, diff --git a/charon/tests/ui/cross_compile_big_endian.out b/charon/tests/ui/cross_compile_big_endian.out index d6c8e8199..5beb77f12 100644 --- a/charon/tests/ui/cross_compile_big_endian.out +++ b/charon/tests/ui/cross_compile_big_endian.out @@ -9,6 +9,16 @@ pub const MAX: usize = MAX() // Full name: core::num::{u128}::to_ne_bytes pub fn to_ne_bytes(@1: u128) -> Array +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::S fn S() -> Array { diff --git a/charon/tests/ui/demo.out b/charon/tests/ui/demo.out index 90e4b2c36..5f1df5b22 100644 --- a/charon/tests/ui/demo.out +++ b/charon/tests/ui/demo.out @@ -16,6 +16,16 @@ pub trait Sized #[lang_item("global_alloc_ty")] pub struct Global {} +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::choose pub fn choose<'a, T>(@1: bool, @2: &'a mut (T), @3: &'a mut (T)) -> &'a mut (T) where diff --git a/charon/tests/ui/dictionary_passing_style_woes.out b/charon/tests/ui/dictionary_passing_style_woes.out index 60ad2b1f2..3666c56a0 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.out +++ b/charon/tests/ui/dictionary_passing_style_woes.out @@ -58,6 +58,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Iterator trait Iterator { diff --git a/charon/tests/ui/disambiguator.out b/charon/tests/ui/disambiguator.out index 8c1bef88f..da2cfdc44 100644 --- a/charon/tests/ui/disambiguator.out +++ b/charon/tests/ui/disambiguator.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + fn test_crate::nonzero_disambiguator::my_function() { let @0: (); // return diff --git a/charon/tests/ui/diverging.out b/charon/tests/ui/diverging.out index a9a08e7c7..9c50b32f0 100644 --- a/charon/tests/ui/diverging.out +++ b/charon/tests/ui/diverging.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::my_panic fn my_panic(@1: u32) -> ! { diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index c113a4024..8495ae7ca 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -186,6 +186,16 @@ where vtable: {impl ToString for T}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::construct fn construct(@1: T) -> alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : 'static)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized] where @@ -201,7 +211,7 @@ fn destruct<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _d let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // anonymous local storage_live(@2) - @2 := &*(x@1) + @2 := &*(x@1) with_metadata(copy (x@1.metadata)) @0 := {impl ToString for T}::to_string<'_, (dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Display<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>](move (@2)) storage_dead(@2) return diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index cd74f1daa..fc673780b 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -42,6 +42,16 @@ pub fn core::ops::arith::Add::add(@1: Self, @2: Rhs) -> @TraitClause0 where [@TraitClause0]: Add, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Super trait Super { @@ -295,14 +305,20 @@ fn {impl Join for i32}::join_method<'_0>(@1: &'_0 (i32)) -> (i32, i32) fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} { let ret@0: test_crate::Join::{vtable}; // return - let @1: &'static (test_crate::Left::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local - let @2: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @1: (); // anonymous local + let @2: &'static (test_crate::Left::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @3: (); // anonymous local + let @4: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local storage_live(@1) storage_live(@2) - @1 := &{impl Left for i32}::{vtable} - @2 := &{impl Right for i32}::{vtable} - ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({impl Join for i32}::join_method), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1), super_trait_2: move (@2) } + storage_live(@3) + storage_live(@4) + @1 := () + @2 := &{impl Left for i32}::{vtable} + @3 := () + @4 := &{impl Right for i32}::{vtable} + ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({impl Join for i32}::join_method), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } return } @@ -342,7 +358,7 @@ fn main() storage_dead(@3) storage_live(@5) storage_live(@6) - @6 := &*(v@1) + @6 := &*(v@1) with_metadata(copy (v@1.metadata)) @5 := Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::join_method<'_>(move (@6)) storage_dead(@6) storage_dead(@5) diff --git a/charon/tests/ui/explicit-drop-bounds.out b/charon/tests/ui/explicit-drop-bounds.out index e9130862e..5a4da2173 100644 --- a/charon/tests/ui/explicit-drop-bounds.out +++ b/charon/tests/ui/explicit-drop-bounds.out @@ -39,6 +39,16 @@ impl Drop for String { non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 9c2bfe922..27ac7cebc 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -218,6 +218,16 @@ where vtable: {impl Drop for Vec[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + pub fn test_crate::swap<'a, T>(@1: &'a mut (T), @2: &'a mut (T)) where [@TraitClause0]: Sized, diff --git a/charon/tests/ui/find-sized-clause.out b/charon/tests/ui/find-sized-clause.out index bac3f30ec..29720bd02 100644 --- a/charon/tests/ui/find-sized-clause.out +++ b/charon/tests/ui/find-sized-clause.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/float.out b/charon/tests/ui/float.out index 7fe90638b..115580076 100644 --- a/charon/tests/ui/float.out +++ b/charon/tests/ui/float.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::test_float fn test_float(@1: f64) -> f64 { diff --git a/charon/tests/ui/foreign-constant.out b/charon/tests/ui/foreign-constant.out index 659e9ee7d..4aa2f20b8 100644 --- a/charon/tests/ui/foreign-constant.out +++ b/charon/tests/ui/foreign-constant.out @@ -6,6 +6,16 @@ pub fn CONSTANT() -> u8 // Full name: foreign_constant_aux::CONSTANT pub const CONSTANT: u8 = CONSTANT() +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo() -> u8 { diff --git a/charon/tests/ui/gat-causes-unhandled-ty-clause.out b/charon/tests/ui/gat-causes-unhandled-ty-clause.out index 56d139f51..e6092e902 100644 --- a/charon/tests/ui/gat-causes-unhandled-ty-clause.out +++ b/charon/tests/ui/gat-causes-unhandled-ty-clause.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasAssoc trait HasAssoc { diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out index 32bfecab0..979d3971d 100644 --- a/charon/tests/ui/gosim-demo.out +++ b/charon/tests/ui/gosim-demo.out @@ -490,6 +490,16 @@ where // Full name: std::io::stdio::_eprint pub fn _eprint<'_0>(@1: Arguments<'_0>) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::debug_slice fn debug_slice<'_0, T>(@1: &'_0 (Slice)) where diff --git a/charon/tests/ui/hide-marker-traits.out b/charon/tests/ui/hide-marker-traits.out index af60ee085..52294188d 100644 --- a/charon/tests/ui/hide-marker-traits.out +++ b/charon/tests/ui/hide-marker-traits.out @@ -13,6 +13,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Idx trait Idx diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out index f61eaa900..0c500ba94 100644 --- a/charon/tests/ui/impl-trait.out +++ b/charon/tests/ui/impl-trait.out @@ -94,6 +94,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo pub trait Foo { @@ -242,7 +252,7 @@ where storage_live(@5) @5 := &foo@1 @4 := @TraitClause1::parent_clause2::get_ty<'_>(move (@5)) - @3 := &*(@4) + @3 := &*(@4) with_metadata(copy (@4.metadata)) storage_dead(@5) @2 := @TraitClause1::parent_clause2::parent_clause2::clone<'_>(move (@3)) storage_dead(@3) diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index e1b3ead69..cde049b3e 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -279,6 +279,16 @@ where return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::use_inlines fn use_inlines() -> u32 { diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index ffc8cb293..68c3236fb 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -43,6 +43,16 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo struct Foo {} diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out index 9ae0f000e..821d7ed68 100644 --- a/charon/tests/ui/issue-120-bare-discriminant-read.out +++ b/charon/tests/ui/issue-120-bare-discriminant-read.out @@ -50,6 +50,16 @@ where non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::discriminant_value fn discriminant_value<'_0, T>(@1: &'_0 (Option[@TraitClause0])) -> isize where diff --git a/charon/tests/ui/issue-159-heterogeneous-recursive-definitions.out b/charon/tests/ui/issue-159-heterogeneous-recursive-definitions.out index 91429c9a8..a0f1bfaa7 100644 --- a/charon/tests/ui/issue-159-heterogeneous-recursive-definitions.out +++ b/charon/tests/ui/issue-159-heterogeneous-recursive-definitions.out @@ -4,6 +4,16 @@ #[lang_item("meta_sized")] pub trait MetaSized +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Ops trait Ops { diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out index fc0507916..fc778937c 100644 --- a/charon/tests/ui/issue-165-vec-macro.out +++ b/charon/tests/ui/issue-165-vec-macro.out @@ -120,6 +120,16 @@ where vtable: {impl Drop for Vec[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo() { diff --git a/charon/tests/ui/issue-166-self-constructors.out b/charon/tests/ui/issue-166-self-constructors.out index 0b220da0d..4fee6f086 100644 --- a/charon/tests/ui/issue-166-self-constructors.out +++ b/charon/tests/ui/issue-166-self-constructors.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo enum Foo { A, diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out index f7cd8f1b1..377f111b2 100644 --- a/charon/tests/ui/issue-297-cfg.out +++ b/charon/tests/ui/issue-297-cfg.out @@ -425,6 +425,16 @@ pub fn chunks<'_0, T>(@1: &'_0 (Slice), @2: usize) -> Chunks<'_0, T>[@TraitCl where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::f1 fn f1<'_0>(@1: &'_0 (Slice)) -> usize { @@ -459,7 +469,7 @@ fn f1<'_0>(@1: &'_0 (Slice)) -> usize storage_live(@6) @6 := const (0 : usize) storage_live(@14) - @14 := &*(a@1) + @14 := &*(a@1) with_metadata(copy (a@1.metadata)) storage_live(@15) @15 := @SliceIndexShared<'_, u8>(move (@14), copy (@6)) @5 := copy (*(@15)) @@ -472,7 +482,7 @@ fn f1<'_0>(@1: &'_0 (Slice)) -> usize storage_live(@9) @9 := const (1 : usize) storage_live(@12) - @12 := &*(a@1) + @12 := &*(a@1) with_metadata(copy (a@1.metadata)) storage_live(@13) @13 := @SliceIndexShared<'_, u8>(move (@12), copy (@9)) @8 := copy (*(@13)) @@ -628,7 +638,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@5) storage_live(@6) storage_live(@7) - @7 := &*(a@1) + @7 := &*(a@1) with_metadata(copy (a@1.metadata)) @6 := chunks<'_, u8>[Sized](move (@7), const (3 : usize)) storage_dead(@7) @5 := {impl IntoIterator for I}::into_iter[Sized]>[Sized[Sized]>, {impl Iterator for Chunks<'a, T>[@TraitClause0]}<'_, u8>[Sized]](move (@6)) @@ -656,7 +666,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@16) @16 := const (0 : usize) storage_live(@56) - @56 := &*(bytes@13) + @56 := &*(bytes@13) with_metadata(copy (bytes@13.metadata)) storage_live(@57) @57 := @SliceIndexShared<'_, u8>(move (@56), copy (@16)) @15 := copy (*(@57)) @@ -668,7 +678,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@19) @19 := const (1 : usize) storage_live(@54) - @54 := &*(bytes@13) + @54 := &*(bytes@13) with_metadata(copy (bytes@13.metadata)) storage_live(@55) @55 := @SliceIndexShared<'_, u8>(move (@54), copy (@19)) @18 := copy (*(@55)) @@ -680,7 +690,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@22) @22 := const (2 : usize) storage_live(@52) - @52 := &*(bytes@13) + @52 := &*(bytes@13) with_metadata(copy (bytes@13.metadata)) storage_live(@53) @53 := @SliceIndexShared<'_, u8>(move (@52), copy (@22)) @21 := copy (*(@53)) @@ -733,7 +743,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@39) @39 := copy (sampled@3) storage_live(@48) - @48 := &mut *(result@2) + @48 := &mut *(result@2) with_metadata(copy (result@2.metadata)) storage_live(@49) @49 := @SliceIndexMut<'_, i16>(move (@48), copy (@39)) *(@49) := move (@38) @@ -769,7 +779,7 @@ fn f2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 mut (Slice)) -> usize storage_live(@46) @46 := copy (sampled@3) storage_live(@50) - @50 := &mut *(result@2) + @50 := &mut *(result@2) with_metadata(copy (result@2.metadata)) storage_live(@51) @51 := @SliceIndexMut<'_, i16>(move (@50), copy (@46)) *(@51) := move (@45) diff --git a/charon/tests/ui/issue-320-slice-pattern.out b/charon/tests/ui/issue-320-slice-pattern.out index 5994175aa..db0b826ca 100644 --- a/charon/tests/ui/issue-320-slice-pattern.out +++ b/charon/tests/ui/issue-320-slice-pattern.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::slice_pat1 fn slice_pat1() { @@ -110,16 +120,19 @@ fn slice_pat3() let @8: usize; // anonymous local let @9: usize; // anonymous local let @10: bool; // anonymous local - let @11: &'_ (Slice); // anonymous local + let @11: usize; // anonymous local let @12: usize; // anonymous local let @13: usize; // anonymous local - let @14: &'_ (i32); // anonymous local - let @15: &'_ (Slice); // anonymous local + let @14: &'_ (Slice); // anonymous local + let @15: usize; // anonymous local let @16: usize; // anonymous local - let @17: usize; // anonymous local + let @17: &'_ (i32); // anonymous local let @18: &'_ (Slice); // anonymous local - let @19: &'_ (Slice); // anonymous local - let @20: &'_ (i32); // anonymous local + let @19: usize; // anonymous local + let @20: usize; // anonymous local + let @21: &'_ (Slice); // anonymous local + let @22: &'_ (Slice); // anonymous local + let @23: &'_ (i32); // anonymous local storage_live(@8) storage_live(@9) @@ -148,31 +161,38 @@ fn slice_pat3() storage_dead(_a@5) panic(core::panicking::panic_explicit) } - storage_live(@19) - @19 := &*(slice@1) - storage_live(@20) - @20 := @SliceIndexShared<'_, i32>(move (@19), const (0 : usize)) - _a@5 := &*(@20) - storage_live(@15) - @15 := &*(slice@1) - storage_live(@16) - @16 := len(*(slice@1)) - storage_live(@17) - @17 := copy (@16) ub.- const (1 : usize) - storage_dead(@16) - storage_live(@18) - @18 := @SliceSubSliceShared<'_, i32>(move (@15), const (1 : usize), copy (@17)) - _b@6 := &*(@18) + storage_live(@22) + @22 := &*(slice@1) with_metadata(copy (slice@1.metadata)) + storage_live(@23) + @23 := @SliceIndexShared<'_, i32>(move (@22), const (0 : usize)) + _a@5 := &*(@23) storage_live(@11) - @11 := &*(slice@1) + @11 := len(*(slice@1)) storage_live(@12) - @12 := len(*(slice@1)) + @12 := copy (@11) ub.- const (1 : usize) + storage_dead(@11) storage_live(@13) @13 := copy (@12) ub.- const (1 : usize) - storage_dead(@12) + storage_live(@18) + @18 := &*(slice@1) with_metadata(copy (slice@1.metadata)) + storage_live(@19) + @19 := len(*(slice@1)) + storage_live(@20) + @20 := copy (@19) ub.- const (1 : usize) + storage_dead(@19) + storage_live(@21) + @21 := @SliceSubSliceShared<'_, i32>(move (@18), const (1 : usize), copy (@20)) + _b@6 := &*(@21) with_metadata(copy (@13)) storage_live(@14) - @14 := @SliceIndexShared<'_, i32>(move (@11), copy (@13)) - _c@7 := &*(@14) + @14 := &*(slice@1) with_metadata(copy (slice@1.metadata)) + storage_live(@15) + @15 := len(*(slice@1)) + storage_live(@16) + @16 := copy (@15) ub.- const (1 : usize) + storage_dead(@15) + storage_live(@17) + @17 := @SliceIndexShared<'_, i32>(move (@14), copy (@16)) + _c@7 := &*(@17) @0 := () storage_dead(_c@7) storage_dead(_b@6) @@ -183,5 +203,84 @@ fn slice_pat3() return } +// Full name: test_crate::slice_pat4 +fn slice_pat4<'_0>(@1: &'_0 (Slice)) +{ + let @0: (); // return + let x@1: &'_ (Slice); // arg #1 + let @2: usize; // anonymous local + let @3: usize; // anonymous local + let @4: bool; // anonymous local + let _y@5: &'_ (u32); // local + let @6: &'_ (Slice); // anonymous local + let @7: &'_ (u32); // anonymous local + + storage_live(@2) + storage_live(@3) + storage_live(@4) + @2 := len(*(x@1)) + @3 := const (1 : usize) + @4 := move (@2) == move (@3) + if move (@4) { + } + else { + @0 := () + @0 := () + return + } + storage_live(_y@5) + storage_live(@6) + @6 := &*(x@1) with_metadata(copy (x@1.metadata)) + storage_live(@7) + @7 := @SliceIndexShared<'_, u32>(move (@6), const (0 : usize)) + _y@5 := &*(@7) + @0 := () + storage_dead(_y@5) + @0 := () + return +} + +// Full name: test_crate::Unsized +struct Unsized { + Slice, +} + +// Full name: test_crate::slice_pat5 +fn slice_pat5<'_0>(@1: &'_0 (Unsized)) +{ + let @0: (); // return + let x@1: &'_ (Unsized); // arg #1 + let @2: usize; // anonymous local + let @3: usize; // anonymous local + let @4: bool; // anonymous local + let _y@5: u32; // local + let @6: &'_ (Slice); // anonymous local + let @7: &'_ (u32); // anonymous local + + storage_live(@2) + storage_live(@3) + storage_live(@4) + @2 := len((*(x@1)).0) + @3 := const (1 : usize) + @4 := move (@2) == move (@3) + if move (@4) { + } + else { + @0 := () + @0 := () + return + } + storage_live(_y@5) + storage_live(@6) + @6 := &(*(x@1)).0 with_metadata(copy (x@1.metadata)) + storage_live(@7) + @7 := @SliceIndexShared<'_, u32>(move (@6), const (0 : usize)) + _y@5 := copy (*(@7)) + @0 := () + storage_dead(_y@5) + @0 := () + return +} + diff --git a/charon/tests/ui/issue-320-slice-pattern.rs b/charon/tests/ui/issue-320-slice-pattern.rs index 5339b896b..7e541406c 100644 --- a/charon/tests/ui/issue-320-slice-pattern.rs +++ b/charon/tests/ui/issue-320-slice-pattern.rs @@ -12,3 +12,20 @@ fn slice_pat3() { let slice: &[_] = &[0; 4]; let [_a, _b @ .., _c] = slice else { panic!() }; } + +fn slice_pat4(x: &[u32]) { + match x { + [_y] => {} + _ => {} + } +} + +/// This test generates a `RValue::Len` on a place that isn't `Deref`. It's a regression test to +/// avoid the mistaken assumption that `Len` only applies to `Deref` places. +struct Unsized([u32]); +fn slice_pat5(x: &Unsized) { + match x.0 { + [_y] => {} + _ => {} + } +} diff --git a/charon/tests/ui/issue-322-macro-disambiguator.out b/charon/tests/ui/issue-322-macro-disambiguator.out index 20b198f0c..4a35431e1 100644 --- a/charon/tests/ui/issue-322-macro-disambiguator.out +++ b/charon/tests/ui/issue-322-macro-disambiguator.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + struct test_crate::main::AssertIsAsBytes {} struct test_crate::main::AssertIsAsBytes#1 {} diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out index 56fcacc86..67a985fed 100644 --- a/charon/tests/ui/issue-323-closure-borrow.out +++ b/charon/tests/ui/issue-323-closure-borrow.out @@ -67,6 +67,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Rng struct Rng {} diff --git a/charon/tests/ui/issue-369-mismatched-genericparams.out b/charon/tests/ui/issue-369-mismatched-genericparams.out index f8597f608..00094c08d 100644 --- a/charon/tests/ui/issue-369-mismatched-genericparams.out +++ b/charon/tests/ui/issue-369-mismatched-genericparams.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::FromResidual pub trait FromResidual { diff --git a/charon/tests/ui/issue-372-type-param-out-of-range.out b/charon/tests/ui/issue-372-type-param-out-of-range.out index ab6f0e8c8..9180bb3c6 100644 --- a/charon/tests/ui/issue-372-type-param-out-of-range.out +++ b/charon/tests/ui/issue-372-type-param-out-of-range.out @@ -55,6 +55,16 @@ pub fn 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::S pub struct S<'a, K> where diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index 2113484ef..4909b5ac3 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -58,6 +58,16 @@ impl Drop for String { #[lang_item("string_new")] pub fn new() -> String +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::F fn F() -> fn(u8) -> Option[Sized] { diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out index 10bf2aeaf..ea15b7783 100644 --- a/charon/tests/ui/issue-394-rpit-with-lifetime.out +++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out @@ -90,6 +90,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::sparse_transitions::closure struct closure<'a> {} diff --git a/charon/tests/ui/issue-395-failed-to-normalize.out b/charon/tests/ui/issue-395-failed-to-normalize.out index d6d50f21a..cbff4c642 100644 --- a/charon/tests/ui/issue-395-failed-to-normalize.out +++ b/charon/tests/ui/issue-395-failed-to-normalize.out @@ -376,6 +376,16 @@ where vtable: core::ops::try_trait::Residual::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait pub trait Trait { diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index 9e424494a..a14835336 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -180,6 +180,16 @@ where [@TraitClause1]: Sized, [@TraitClause2]: Debug, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::trait_error pub fn trait_error<'_0>(@1: &'_0 (Slice)) { @@ -192,7 +202,7 @@ pub fn trait_error<'_0>(@1: &'_0 (Slice)) storage_live(_array@2) storage_live(@3) storage_live(@4) - @4 := &*(s@1) + @4 := &*(s@1) with_metadata(copy (s@1.metadata)) @3 := {impl TryInto for T}::try_into<&'_ (Slice), Array>[Sized<&'_ (Slice)>, Sized>, {impl TryFrom<&'_0 (Slice)> for Array}<'_, u8, 4 : usize>[Sized, {impl Copy for u8}]](move (@4)) storage_dead(@4) _array@2 := unwrap, TryFromSliceError>[Sized>, Sized, {impl Debug for TryFromSliceError}](move (@3)) diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index d5f8eea75..b2cab8c0a 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -180,6 +180,16 @@ where [@TraitClause1]: Sized, [@TraitClause2]: Debug, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::trait_error fn trait_error<'_0>(@1: &'_0 (Slice)) { @@ -192,7 +202,7 @@ fn trait_error<'_0>(@1: &'_0 (Slice)) storage_live(_array@2) storage_live(@3) storage_live(@4) - @4 := &*(s@1) + @4 := &*(s@1) with_metadata(copy (s@1.metadata)) @3 := {impl TryInto for T}::try_into<&'_ (Slice), Array>[Sized<&'_ (Slice)>, Sized>, {impl TryFrom<&'_0 (Slice)> for Array}<'_, u8, 4 : usize>[Sized, {impl Copy for u8}]](move (@4)) storage_dead(@4) _array@2 := unwrap, TryFromSliceError>[Sized>, Sized, {impl Debug for TryFromSliceError}](move (@3)) diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index eda42f771..372b2b5a9 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -536,6 +536,16 @@ pub fn core::slice::{Slice}::len<'_0, T>(@1: &'_0 (Slice)) -> usize where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::map::closure struct closure {} @@ -749,14 +759,14 @@ fn select<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) storage_live(@7) storage_live(@8) storage_live(@9) - @9 := &*(lhs@1) + @9 := &*(lhs@1) with_metadata(copy (lhs@1.metadata)) @8 := core::slice::{Slice}::len<'_, u8>[Sized](move (@9)) storage_dead(@9) @7 := &@8 storage_live(@10) storage_live(@11) storage_live(@12) - @12 := &*(rhs@2) + @12 := &*(rhs@2) with_metadata(copy (rhs@2.metadata)) @11 := core::slice::{Slice}::len<'_, u8>[Sized](move (@12)) storage_dead(@12) @10 := &@11 diff --git a/charon/tests/ui/issue-507-cfg.out b/charon/tests/ui/issue-507-cfg.out index afd4d489e..a697f95bf 100644 --- a/charon/tests/ui/issue-507-cfg.out +++ b/charon/tests/ui/issue-507-cfg.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::CONST fn CONST() -> u8 { diff --git a/charon/tests/ui/issue-70-override-provided-method.2.out b/charon/tests/ui/issue-70-override-provided-method.2.out index 80b1f88cb..e282d980e 100644 --- a/charon/tests/ui/issue-70-override-provided-method.2.out +++ b/charon/tests/ui/issue-70-override-provided-method.2.out @@ -4,6 +4,16 @@ #[lang_item("meta_sized")] pub trait MetaSized +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { @@ -31,13 +41,13 @@ where storage_live(@2) storage_live(@3) - @3 := &*(self@1) + @3 := &*(self@1) with_metadata(copy (self@1.metadata)) @2 := @TraitClause0::required<'_>(move (@3)) storage_dead(@3) storage_dead(@2) storage_live(@4) storage_live(@5) - @5 := &*(self@1) + @5 := &*(self@1) with_metadata(copy (self@1.metadata)) @4 := @TraitClause0::provided2<'_>(move (@5)) storage_dead(@5) storage_dead(@4) @@ -60,13 +70,13 @@ where storage_live(@2) storage_live(@3) - @3 := &*(self@1) + @3 := &*(self@1) with_metadata(copy (self@1.metadata)) @2 := @TraitClause0::required<'_>(move (@3)) storage_dead(@3) storage_dead(@2) storage_live(@4) storage_live(@5) - @5 := &*(self@1) + @5 := &*(self@1) with_metadata(copy (self@1.metadata)) @4 := @TraitClause0::provided1<'_>(move (@5)) storage_dead(@5) storage_dead(@4) diff --git a/charon/tests/ui/issue-70-override-provided-method.3.out b/charon/tests/ui/issue-70-override-provided-method.3.out index 3ca404614..a4912c67e 100644 --- a/charon/tests/ui/issue-70-override-provided-method.3.out +++ b/charon/tests/ui/issue-70-override-provided-method.3.out @@ -98,6 +98,16 @@ where non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::GenericTrait trait GenericTrait { diff --git a/charon/tests/ui/issue-70-override-provided-method.out b/charon/tests/ui/issue-70-override-provided-method.out index 6de30d14d..519c34623 100644 --- a/charon/tests/ui/issue-70-override-provided-method.out +++ b/charon/tests/ui/issue-70-override-provided-method.out @@ -109,6 +109,16 @@ where vtable: {impl PartialEq[@TraitClause0]> for Option[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } +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/issue-72-hash-missing-impl.out b/charon/tests/ui/issue-72-hash-missing-impl.out index 9774f72a0..6e6f5c388 100644 --- a/charon/tests/ui/issue-72-hash-missing-impl.out +++ b/charon/tests/ui/issue-72-hash-missing-impl.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Hasher pub trait Hasher { diff --git a/charon/tests/ui/issue-73-extern.out b/charon/tests/ui/issue-73-extern.out index 6e257f262..bb7ef7310 100644 --- a/charon/tests/ui/issue-73-extern.out +++ b/charon/tests/ui/issue-73-extern.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo unsafe fn foo(@1: i32) 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 7004f68e8..e4cf7d938 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -43,6 +43,16 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo enum Foo { A, diff --git a/charon/tests/ui/issue-92-nonpositive-variant-indices.out b/charon/tests/ui/issue-92-nonpositive-variant-indices.out index adfeca4e3..6507d665f 100644 --- a/charon/tests/ui/issue-92-nonpositive-variant-indices.out +++ b/charon/tests/ui/issue-92-nonpositive-variant-indices.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Ordering enum Ordering { Less, diff --git a/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out b/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out index 51fd22559..b858c561c 100644 --- a/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out +++ b/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait1 pub trait Trait1 { diff --git a/charon/tests/ui/issue-94-recursive-trait-defns.out b/charon/tests/ui/issue-94-recursive-trait-defns.out index 5a203b78a..8ae892433 100644 --- a/charon/tests/ui/issue-94-recursive-trait-defns.out +++ b/charon/tests/ui/issue-94-recursive-trait-defns.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait1 pub trait Trait1 { diff --git a/charon/tests/ui/issue-97-missing-parent-item-clause.out b/charon/tests/ui/issue-97-missing-parent-item-clause.out index d69aad815..95336be25 100644 --- a/charon/tests/ui/issue-97-missing-parent-item-clause.out +++ b/charon/tests/ui/issue-97-missing-parent-item-clause.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Ord pub trait Ord { diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out index 11853ce9b..1db7f802a 100644 --- a/charon/tests/ui/iterator.out +++ b/charon/tests/ui/iterator.out @@ -4499,6 +4499,16 @@ pub fn chunks_exact<'_0, T>(@1: &'_0 (Slice), @2: usize) -> ChunksExact<'_0, 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/loops.out b/charon/tests/ui/loops.out index 058d7c675..45d454f39 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -794,6 +794,16 @@ where vtable: {impl IndexMut for Vec[@TraitClause0, @TraitClause2]}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::test_loop1 pub fn test_loop1(@1: u32) -> u32 { diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out index bec897c19..8ce7e708b 100644 --- a/charon/tests/ui/matches.out +++ b/charon/tests/ui/matches.out @@ -26,6 +26,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::E1 pub enum E1 { V1, diff --git a/charon/tests/ui/max_char.out b/charon/tests/ui/max_char.out index e743bf783..24b3787ec 100644 --- a/charon/tests/ui/max_char.out +++ b/charon/tests/ui/max_char.out @@ -20,6 +20,16 @@ pub fn core::char::MAX() -> char pub const core::char::MAX: char = core::char::MAX() +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/method-impl-generalization.out b/charon/tests/ui/method-impl-generalization.out index 20a424073..15686875e 100644 --- a/charon/tests/ui/method-impl-generalization.out +++ b/charon/tests/ui/method-impl-generalization.out @@ -58,6 +58,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/method-ref.out b/charon/tests/ui/method-ref.out index e124a4f16..c9ef3d001 100644 --- a/charon/tests/ui/method-ref.out +++ b/charon/tests/ui/method-ref.out @@ -20,6 +20,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Ord trait Ord { diff --git a/charon/tests/ui/ml-name-matcher-tests.out b/charon/tests/ui/ml-name-matcher-tests.out index 2c2e015c8..93285ad8f 100644 --- a/charon/tests/ui/ml-name-matcher-tests.out +++ b/charon/tests/ui/ml-name-matcher-tests.out @@ -182,6 +182,16 @@ where #[lang_item("global_alloc_ty")] pub struct Global {} +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::bar fn bar() { @@ -294,13 +304,13 @@ fn foo() storage_live(@8) storage_live(@9) storage_live(@10) - @10 := &*(slice@4) + @10 := &*(slice@4) with_metadata(copy (slice@4.metadata)) storage_live(@11) @11 := RangeFrom { start: const (1 : usize) } @9 := {impl Index for Slice}::index<'_, bool, RangeFrom[Sized]>[Sized, Sized[Sized]>, {impl SliceIndex> for RangeFrom[Sized]}[Sized]](move (@10), move (@11)) storage_dead(@11) storage_dead(@10) - @8 := &*(@9) + @8 := &*(@9) with_metadata(copy (@9.metadata)) storage_dead(@8) @0 := () storage_dead(@9) diff --git a/charon/tests/ui/monomorphization/adt_proj.out b/charon/tests/ui/monomorphization/adt_proj.out index e94b502a6..b0c23f964 100644 --- a/charon/tests/ui/monomorphization/adt_proj.out +++ b/charon/tests/ui/monomorphization/adt_proj.out @@ -19,6 +19,16 @@ pub enum Result:: { Err(u32), } +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/monomorphization/bound_lifetime.out b/charon/tests/ui/monomorphization/bound_lifetime.out index 64fc21d03..2ce361974 100644 --- a/charon/tests/ui/monomorphization/bound_lifetime.out +++ b/charon/tests/ui/monomorphization/bound_lifetime.out @@ -19,6 +19,16 @@ pub enum Option::<&'_ (u32)> { Some(&'_ (u32)), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo<'_0>(@1: &'_0 (u32)) -> Option::<&'_ (u32)> { diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index 5ac030516..f02143ea3 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -97,6 +97,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: closure<'_, '_>, @2: (u8, u8)) pub fn core::ops::function::FnOnce::call_once::, (u8, u8)>(@1: closure<'_, '_>, @2: (u8, u8)) -> u8 +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::main::{impl Fn::, (u8, u8)>}::call fn {impl Fn::, (u8, u8)>}::call<'_0, '_1, '_2>(@1: &'_2 (closure<'_0, '_1>), @2: (u8, u8)) -> u8 { diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 4187da696..e5621c7bc 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -81,6 +81,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: closure, @2: (u8)) -> u8 pub fn core::ops::function::FnOnce::call_once::(@1: closure, @2: (u8)) -> u8 +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::main::{impl FnOnce::}::call_once fn {impl FnOnce::}::call_once(@1: closure, @2: (u8)) -> u8 { diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index 517a55a57..069037d7a 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -208,6 +208,16 @@ pub fn core::ops::function::FnOnce::call_once::, ( pub fn core::ops::function::FnOnce::call_once::, (u8)>(@1: test_crate::main::closure#1<'_>, @2: (u8)) -> u8 +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::main::{impl Fn::, (u8)>}::call fn {impl Fn::, (u8)>}::call<'_0, '_1>(@1: &'_1 (test_crate::main::closure<'_0>), @2: (u8)) -> u8 { diff --git a/charon/tests/ui/monomorphization/fn_ptr_generics.out b/charon/tests/ui/monomorphization/fn_ptr_generics.out index eade5f1bd..d70f08712 100644 --- a/charon/tests/ui/monomorphization/fn_ptr_generics.out +++ b/charon/tests/ui/monomorphization/fn_ptr_generics.out @@ -19,6 +19,16 @@ pub enum Option:: { Some(u8), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::init_option fn init_option() { diff --git a/charon/tests/ui/monomorphization/fndefs-casts.out b/charon/tests/ui/monomorphization/fndefs-casts.out index 7ca3cf3cd..8d7402a79 100644 --- a/charon/tests/ui/monomorphization/fndefs-casts.out +++ b/charon/tests/ui/monomorphization/fndefs-casts.out @@ -150,6 +150,16 @@ pub fn call_mut:: foo::<'_0>, (&'_ (u32))><'_0>(@1: &'_0 mut (for< // Full name: core::ops::function::FnOnce::call_once:: foo::<'_0>, (&'_ (u32))> pub fn call_once:: foo::<'_0>, (&'_ (u32))>(@1: for<'_0> foo::<'_0_0>, @2: (&'_ (u32))) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::foo:: fn foo::<'_0>(@1: &'_0 (u8)) { diff --git a/charon/tests/ui/monomorphization/global_with_generics.out b/charon/tests/ui/monomorphization/global_with_generics.out index 666cfd690..0207e8105 100644 --- a/charon/tests/ui/monomorphization/global_with_generics.out +++ b/charon/tests/ui/monomorphization/global_with_generics.out @@ -24,6 +24,16 @@ pub trait Sized:: non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::Foo:: struct Foo:: { value: i32, @@ -64,13 +74,16 @@ fn main() let @0: (); // return let _b@1: bool; // local let @2: &'_ (Foo::); // anonymous local - let @3: &'_ (Foo::); // anonymous local + let @3: (); // anonymous local + let @4: &'_ (Foo::); // anonymous local storage_live(@3) + storage_live(@4) storage_live(_b@1) storage_live(@2) - @3 := &FooBool - @2 := move (@3) + @3 := () + @4 := &FooBool + @2 := move (@4) _b@1 := copy ((*(@2)).value) storage_dead(@2) @0 := () diff --git a/charon/tests/ui/monomorphization/rec-adt.out b/charon/tests/ui/monomorphization/rec-adt.out index 3170a999f..67b4dd6dd 100644 --- a/charon/tests/ui/monomorphization/rec-adt.out +++ b/charon/tests/ui/monomorphization/rec-adt.out @@ -61,6 +61,16 @@ pub enum Option::>> { #[lang_item("NonNull")] pub opaque type NonNull +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::LinkedList:: pub struct LinkedList:: { head: Option::>>, diff --git a/charon/tests/ui/monomorphization/trait_impls.out b/charon/tests/ui/monomorphization/trait_impls.out index 6236f595d..b060c4ff9 100644 --- a/charon/tests/ui/monomorphization/trait_impls.out +++ b/charon/tests/ui/monomorphization/trait_impls.out @@ -24,6 +24,16 @@ pub trait Drop:: // Full name: core::ops::drop::Drop::drop:: pub fn drop::<'_0>(@1: &'_0 mut (bool)) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::Trait:: pub trait Trait:: { diff --git a/charon/tests/ui/monomorphization/trait_impls_ullbc.out b/charon/tests/ui/monomorphization/trait_impls_ullbc.out index 809bb8412..8b4c21971 100644 --- a/charon/tests/ui/monomorphization/trait_impls_ullbc.out +++ b/charon/tests/ui/monomorphization/trait_impls_ullbc.out @@ -61,6 +61,18 @@ pub trait Drop:: // Full name: core::ops::drop::Drop::drop:: pub fn drop::<'_0>(@1: &'_0 mut (bool)) +fn UNIT_METADATA() +{ + let @0: (); // return + + bb0: { + @0 := (); + return; + } +} + +const UNIT_METADATA: () = @Fun1() + // Full name: test_crate::do_test:: fn do_test::(@1: bool, @2: bool) { diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index a93cf75a0..0d111988e 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -110,6 +110,16 @@ where vtable: {impl DerefMut for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Pair pub struct Pair where diff --git a/charon/tests/ui/opacity.out b/charon/tests/ui/opacity.out index cd7194378..ccdee1c54 100644 --- a/charon/tests/ui/opacity.out +++ b/charon/tests/ui/opacity.out @@ -111,6 +111,16 @@ where return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo() { diff --git a/charon/tests/ui/opaque-trait.out b/charon/tests/ui/opaque-trait.out index 5997e9a26..f491df8b3 100644 --- a/charon/tests/ui/opaque-trait.out +++ b/charon/tests/ui/opaque-trait.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/opaque_attribute.out b/charon/tests/ui/opaque_attribute.out index aeb7d8425..434a6541b 100644 --- a/charon/tests/ui/opaque_attribute.out +++ b/charon/tests/ui/opaque_attribute.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::BoolTrait pub trait BoolTrait { diff --git a/charon/tests/ui/panics.out b/charon/tests/ui/panics.out index eaf14e2cd..6bf639270 100644 --- a/charon/tests/ui/panics.out +++ b/charon/tests/ui/panics.out @@ -16,6 +16,16 @@ pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : u // 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), const P : usize>), @2: &'a (Array, const A : usize>)) -> Arguments<'a> +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::panic1 fn panic1() { diff --git a/charon/tests/ui/params.out b/charon/tests/ui/params.out index 591594a13..e71a2ef61 100644 --- a/charon/tests/ui/params.out +++ b/charon/tests/ui/params.out @@ -16,6 +16,16 @@ pub trait Sized #[lang_item("global_alloc_ty")] pub struct Global {} +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::test_static fn test_static(@1: &'static (u32)) -> &'static (u32) { diff --git a/charon/tests/ui/plain-panic-str.out b/charon/tests/ui/plain-panic-str.out index 29150cee9..335bc0207 100644 --- a/charon/tests/ui/plain-panic-str.out +++ b/charon/tests/ui/plain-panic-str.out @@ -9,6 +9,16 @@ where // Full name: core::fmt::rt::{Arguments<'a>}::new_const pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> Arguments<'a> +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/pointers-in-consts-no-warns.out b/charon/tests/ui/pointers-in-consts-no-warns.out index ffff62d44..ee0059e9b 100644 --- a/charon/tests/ui/pointers-in-consts-no-warns.out +++ b/charon/tests/ui/pointers-in-consts-no-warns.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::DISGUISED_INT fn DISGUISED_INT() -> *const () { diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index 4f5f8107a..11547b4dc 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -265,6 +265,16 @@ impl BuildHasher for RandomState { vtable: {impl BuildHasher for RandomState}::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::get_or_insert pub fn get_or_insert<'_0>(@1: &'_0 mut (HashMap[Sized, Sized, Sized])) -> &'_0 (u32) { diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index fe940d74c..bbff78b6b 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -112,6 +112,16 @@ where non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::wrap fn wrap<'a>(@1: &'a (u32)) -> Option<&'a (u32)>[Sized<&'a (u32)>] { diff --git a/charon/tests/ui/projection-index-from-end.out b/charon/tests/ui/projection-index-from-end.out index 640694ac7..08f7a1773 100644 --- a/charon/tests/ui/projection-index-from-end.out +++ b/charon/tests/ui/projection-index-from-end.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::slice_pattern_end fn slice_pattern_end<'_0>(@1: &'_0 (Slice<()>)) { @@ -29,7 +39,7 @@ fn slice_pattern_end<'_0>(@1: &'_0 (Slice<()>)) } storage_live(_named@5) storage_live(@6) - @6 := &*(x@1) + @6 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@7) @7 := len(*(x@1)) storage_live(@8) diff --git a/charon/tests/ui/ptr-offset.out b/charon/tests/ui/ptr-offset.out index 4433464b2..b20ccafda 100644 --- a/charon/tests/ui/ptr-offset.out +++ b/charon/tests/ui/ptr-offset.out @@ -55,6 +55,16 @@ where // 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::const_ptr::{*const T}::offset::precondition_check fn precondition_check(@1: *const (), @2: isize, @3: usize) { diff --git a/charon/tests/ui/ptr_no_provenance.out b/charon/tests/ui/ptr_no_provenance.out index 429bc6a34..0968ab1be 100644 --- a/charon/tests/ui/ptr_no_provenance.out +++ b/charon/tests/ui/ptr_no_provenance.out @@ -295,6 +295,16 @@ where return } +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 8bcdfe3f9..42cb1f4bc 100644 --- a/charon/tests/ui/quantified-clause.out +++ b/charon/tests/ui/quantified-clause.out @@ -401,6 +401,16 @@ where Err(E), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo(@1: F) where diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index cf21957bb..987d4e851 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -257,6 +257,16 @@ where args: &'a (Slice>), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: core::panicking::panic_nounwind_fmt::compiletime fn compiletime<'_0>(@1: Arguments<'_0>, @2: bool) -> ! { @@ -719,7 +729,7 @@ where self@7 := cast<*mut Slice, *mut u8>(copy (@13)) storage_dead(self@8) storage_live(count@9) - count@9 := ptr_metadata(copy (@13)) + count@9 := copy (@13.metadata) storage_live(@17) @17 := ub_checks if copy (@17) { @@ -4212,7 +4222,7 @@ where @2 := ManuallyDrop { value: copy (b@1) } @3 := copy ((@2).value) @4 := transmute, *const T>(copy (((@3).0).pointer)) - @0 := &raw mut *(@4) + @0 := &raw mut *(@4) with_metadata(copy (@4.metadata)) storage_dead(@2) return } @@ -4236,10 +4246,10 @@ where storage_live(@3) @4 := copy (((b@1).0).pointer) @3 := transmute, *const T>(copy (@4)) - @2 := &raw mut *(@3) + @2 := &raw mut *(@3) with_metadata(copy (@3.metadata)) storage_dead(@3) storage_dead(@4) - @0 := &mut *(@2) + @0 := &mut *(@2) with_metadata(copy (@2.metadata)) return } diff --git a/charon/tests/ui/reconstruct_early_return.out b/charon/tests/ui/reconstruct_early_return.out index fa7a8cafe..7943325de 100644 --- a/charon/tests/ui/reconstruct_early_return.out +++ b/charon/tests/ui/reconstruct_early_return.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::f fn f() -> usize { diff --git a/charon/tests/ui/region-inference-vars.out b/charon/tests/ui/region-inference-vars.out index fc8a6dfc3..e1bac621c 100644 --- a/charon/tests/ui/region-inference-vars.out +++ b/charon/tests/ui/region-inference-vars.out @@ -23,6 +23,16 @@ where Err(E), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::MyTryFrom pub trait MyTryFrom { diff --git a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out index a9d7dabf8..a8de64322 100644 --- a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out +++ b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out @@ -82,6 +82,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Se where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::PrimeField pub trait PrimeField { diff --git a/charon/tests/ui/remove-dynamic-checks.out b/charon/tests/ui/remove-dynamic-checks.out index 7f2fe44e7..6b20a009f 100644 --- a/charon/tests/ui/remove-dynamic-checks.out +++ b/charon/tests/ui/remove-dynamic-checks.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::neg_test pub fn neg_test(@1: i32) -> i32 { @@ -594,6 +604,23 @@ fn shr_i32_manual_cast(@1: i32, @2: i32) -> i32 return } +// Full name: test_crate::index_slice_ignore_value +fn index_slice_ignore_value<'_0>(@1: &'_0 (Slice)) +{ + let @0: (); // return + let x@1: &'_ (Slice); // arg #1 + let @2: usize; // anonymous local + + storage_live(@2) + // FIXME: Bug: the bound check is removed but the place is not mentioned, so the translated + // function doesn't panic on empty slices anymore. + @2 := const (0 : usize) + storage_dead(@2) + @0 := () + @0 := () + return +} + pub fn test_crate::_() -> isize { let @0: isize; // return @@ -807,7 +834,7 @@ fn div_unsigned_to_slice<'_0>(@1: &'_0 mut (Slice), @2: u32) storage_live(@4) @4 := const (0 : usize) storage_live(@5) - @5 := &mut *(result@1) + @5 := &mut *(result@1) with_metadata(copy (result@1.metadata)) storage_live(@6) @6 := @SliceIndexMut<'_, u32>(move (@5), copy (@4)) *(@6) := move (@3) panic./ const (3329 : u32) @@ -834,7 +861,7 @@ fn div_signed_to_slice<'_0>(@1: &'_0 mut (Slice), @2: i32) storage_live(@4) @4 := const (0 : usize) storage_live(@5) - @5 := &mut *(result@1) + @5 := &mut *(result@1) with_metadata(copy (result@1.metadata)) storage_live(@6) @6 := @SliceIndexMut<'_, i32>(move (@5), copy (@4)) *(@6) := move (@3) panic./ const (3329 : i32) @@ -864,7 +891,7 @@ fn add_to_slice<'_0>(@1: &'_0 mut (Slice), @2: u32) storage_live(@5) @5 := const (0 : usize) storage_live(@6) - @6 := &mut *(result@1) + @6 := &mut *(result@1) with_metadata(copy (result@1.metadata)) storage_live(@7) @7 := @SliceIndexMut<'_, u32>(move (@6), copy (@5)) *(@7) := move (@4) @@ -902,7 +929,7 @@ fn add_to_slice2<'_0>(@1: &'_0 mut (Slice), @2: usize, @3: u8) @6 := move (@8) storage_dead(@7) storage_live(@9) - @9 := &mut *(result@1) + @9 := &mut *(result@1) with_metadata(copy (result@1.metadata)) storage_live(@10) @10 := @SliceIndexMut<'_, u8>(move (@9), copy (@6)) *(@10) := move (@5) diff --git a/charon/tests/ui/remove-dynamic-checks.rs b/charon/tests/ui/remove-dynamic-checks.rs index d271afada..e64070bac 100644 --- a/charon/tests/ui/remove-dynamic-checks.rs +++ b/charon/tests/ui/remove-dynamic-checks.rs @@ -102,6 +102,12 @@ fn shr_i32_manual_cast(x: i32, y: i32) -> i32 { x >> (y as u32) } +fn index_slice_ignore_value(x: &[u32]) { + // FIXME: Bug: the bound check is removed but the place is not mentioned, so the translated + // function doesn't panic on empty slices anymore. + let _ = x[0]; +} + // Checking the simplification of binop operations *inside* global constants. // Even in release mode, rustc inserts additional checks inside constant bodies. pub const _: isize = 1 + 1; diff --git a/charon/tests/ui/rename_attribute.out b/charon/tests/ui/rename_attribute.out index 5186c2b14..2968e4d80 100644 --- a/charon/tests/ui/rename_attribute.out +++ b/charon/tests/ui/rename_attribute.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::BoolTrait pub trait BoolTrait { diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index 2cda8b548..8dc27d044 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -201,6 +201,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: core::result::unwrap_failed fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_1))) -> ! diff --git a/charon/tests/ui/rust-name-matcher-tests.out b/charon/tests/ui/rust-name-matcher-tests.out index bd4b0bf57..3e970f2e7 100644 --- a/charon/tests/ui/rust-name-matcher-tests.out +++ b/charon/tests/ui/rust-name-matcher-tests.out @@ -26,6 +26,16 @@ where #[lang_item("global_alloc_ty")] pub struct Global {} +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::bar fn bar() { diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 7a8ed7288..84d498a3f 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -131,6 +131,16 @@ where vtable: {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::addr_of fn addr_of() { diff --git a/charon/tests/ui/scopes.out b/charon/tests/ui/scopes.out index 167edacf2..7abce1c26 100644 --- a/charon/tests/ui/scopes.out +++ b/charon/tests/ui/scopes.out @@ -4,6 +4,16 @@ #[lang_item("meta_sized")] pub trait MetaSized +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait<'a, Self> { diff --git a/charon/tests/ui/send_bound.out b/charon/tests/ui/send_bound.out index a250b53bf..7023f5695 100644 --- a/charon/tests/ui/send_bound.out +++ b/charon/tests/ui/send_bound.out @@ -30,6 +30,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo(@1: M) where diff --git a/charon/tests/ui/simple-cmp.out b/charon/tests/ui/simple-cmp.out index 52c7dcb6e..36087fe85 100644 --- a/charon/tests/ui/simple-cmp.out +++ b/charon/tests/ui/simple-cmp.out @@ -136,6 +136,16 @@ impl Ord for i32 { non-dyn-compatible } +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/simple/addition.out b/charon/tests/ui/simple/addition.out index 113ceb3d9..bf81070d4 100644 --- a/charon/tests/ui/simple/addition.out +++ b/charon/tests/ui/simple/addition.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/additions.out b/charon/tests/ui/simple/additions.out index 9f93d7773..cd51da622 100644 --- a/charon/tests/ui/simple/additions.out +++ b/charon/tests/ui/simple/additions.out @@ -165,6 +165,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +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/simple/array_index.out b/charon/tests/ui/simple/array_index.out index d862a5a06..38eb01dc2 100644 --- a/charon/tests/ui/simple/array_index.out +++ b/charon/tests/ui/simple/array_index.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::first pub fn first(@1: Array) -> u32 { diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out index 56c1071e0..402af3e0e 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out index 394812fee..acd158098 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out index d137bc3b4..1513b8d31 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out @@ -26,6 +26,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out index 920370008..80996f5b1 100644 --- a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasOutput pub trait HasOutput { diff --git a/charon/tests/ui/simple/assoc-type-with-fn-bound.out b/charon/tests/ui/simple/assoc-type-with-fn-bound.out index ce386396f..0ed58f343 100644 --- a/charon/tests/ui/simple/assoc-type-with-fn-bound.out +++ b/charon/tests/ui/simple/assoc-type-with-fn-bound.out @@ -70,6 +70,16 @@ pub fn call_once(@1: Self, @2: Args) -> Clause0_Outp where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait pub trait Trait { diff --git a/charon/tests/ui/simple/basic-mono.out b/charon/tests/ui/simple/basic-mono.out index 75dfaa50c..c226c9e14 100644 --- a/charon/tests/ui/simple/basic-mono.out +++ b/charon/tests/ui/simple/basic-mono.out @@ -12,6 +12,16 @@ pub trait Sized:: non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::<10 : usize> fn foo::<10 : usize>() { diff --git a/charon/tests/ui/simple/box-into-inner.out b/charon/tests/ui/simple/box-into-inner.out index f567774c1..f76f57742 100644 --- a/charon/tests/ui/simple/box-into-inner.out +++ b/charon/tests/ui/simple/box-into-inner.out @@ -68,6 +68,16 @@ impl Drop for String { non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::into_inner fn into_inner(@1: alloc::boxed::Box[MetaSized, Sized]) { diff --git a/charon/tests/ui/simple/box-new.out b/charon/tests/ui/simple/box-new.out index 217375633..bde5f69b2 100644 --- a/charon/tests/ui/simple/box-new.out +++ b/charon/tests/ui/simple/box-new.out @@ -101,6 +101,16 @@ where vtable: {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause2]}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } +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/simple/call-foreign-defaulted-method.out b/charon/tests/ui/simple/call-foreign-defaulted-method.out index 7ac6b49c5..c98225844 100644 --- a/charon/tests/ui/simple/call-foreign-defaulted-method.out +++ b/charon/tests/ui/simple/call-foreign-defaulted-method.out @@ -4,6 +4,16 @@ #[lang_item("meta_sized")] pub trait MetaSized +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + pub fn test_crate::foo::{impl Trait for ()}::defaulted<'_0>(@1: &'_0 (())) { let @0: (); // return diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out index 542842267..b5fdaa11f 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -25,6 +25,16 @@ pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait pub trait Trait { diff --git a/charon/tests/ui/simple/call-method-via-supertrait-bound.out b/charon/tests/ui/simple/call-method-via-supertrait-bound.out index 9ffc5e78a..55723d2e4 100644 --- a/charon/tests/ui/simple/call-method-via-supertrait-bound.out +++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.out @@ -26,6 +26,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::OtherTrait trait OtherTrait { diff --git a/charon/tests/ui/simple/closure-capture-ref-by-move.out b/charon/tests/ui/simple/closure-capture-ref-by-move.out index 771331da1..805387176 100644 --- a/charon/tests/ui/simple/closure-capture-ref-by-move.out +++ b/charon/tests/ui/simple/closure-capture-ref-by-move.out @@ -67,6 +67,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::closure struct closure<'_0> { &'_0 mut (i32), diff --git a/charon/tests/ui/simple/closure-fn.out b/charon/tests/ui/simple/closure-fn.out index edd1cbb44..4de7f9396 100644 --- a/charon/tests/ui/simple/closure-fn.out +++ b/charon/tests/ui/simple/closure-fn.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::apply_to fn apply_to<'_0, impl Fn(u8, u8) -> u8>(@1: &'_0 (impl Fn(u8, u8) -> u8)) -> u8 where diff --git a/charon/tests/ui/simple/closure-fnmut.out b/charon/tests/ui/simple/closure-fnmut.out index e1bdded29..4d354b214 100644 --- a/charon/tests/ui/simple/closure-fnmut.out +++ b/charon/tests/ui/simple/closure-fnmut.out @@ -67,6 +67,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::apply_to_zero_mut fn apply_to_zero_mut u8>(@1: impl FnMut(u8) -> u8) -> u8 where diff --git a/charon/tests/ui/simple/closure-fnonce.out b/charon/tests/ui/simple/closure-fnonce.out index a4892b9e2..72d829ec6 100644 --- a/charon/tests/ui/simple/closure-fnonce.out +++ b/charon/tests/ui/simple/closure-fnonce.out @@ -55,6 +55,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::apply_to_zero_once fn apply_to_zero_once u8>(@1: impl FnOnce(u8) -> u8) -> u8 where diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out index 657d18778..0c4fc452b 100644 --- a/charon/tests/ui/simple/closure-inside-impl.out +++ b/charon/tests/ui/simple/closure-inside-impl.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo pub struct Foo where diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index 8656a284b..71148d3a2 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Thing trait Thing { diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out index 4e0e13c03..5323c7c9b 100644 --- a/charon/tests/ui/simple/closure-with-drops.out +++ b/charon/tests/ui/simple/closure-with-drops.out @@ -95,6 +95,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + struct test_crate::foo::closure where [@TraitClause0]: Sized, diff --git a/charon/tests/ui/simple/conditional-drop.out b/charon/tests/ui/simple/conditional-drop.out index 68abfc93e..6cc274f5b 100644 --- a/charon/tests/ui/simple/conditional-drop.out +++ b/charon/tests/ui/simple/conditional-drop.out @@ -60,6 +60,16 @@ where vtable: {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::use_box fn use_box(@1: alloc::boxed::Box[MetaSized, Sized, Drop, {impl Drop for Global}]) { diff --git a/charon/tests/ui/simple/const-subslice.out b/charon/tests/ui/simple/const-subslice.out index 8dd174081..866f25c3f 100644 --- a/charon/tests/ui/simple/const-subslice.out +++ b/charon/tests/ui/simple/const-subslice.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::main fn main() { @@ -10,17 +20,20 @@ fn main() let @4: usize; // anonymous local let @5: *const u8; // anonymous local let @6: Slice; // anonymous local - let @7: &'_ (Slice); // anonymous local + let @7: (); // anonymous local + let @8: &'_ (Slice); // anonymous local storage_live(@6) storage_live(@7) + storage_live(@8) storage_live(y@1) @6 := [const (0 : u8), const (1 : u8), const (2 : u8)] - @7 := &@6 - y@1 := move (@7) + @7 := () + @8 := &@6 + y@1 := move (@8) storage_live(z@2) storage_live(@3) - @3 := &raw const *(y@1) + @3 := &raw const *(y@1) with_metadata(copy (y@1.metadata)) z@2 := cast<*const Slice, *const u8>(move (@3)) storage_dead(@3) storage_live(@4) diff --git a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out index 964dd7a06..23bb0e41b 100644 --- a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out +++ b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasAssoc trait HasAssoc { diff --git a/charon/tests/ui/simple/drop-string.out b/charon/tests/ui/simple/drop-string.out index 9861eb79c..203a82034 100644 --- a/charon/tests/ui/simple/drop-string.out +++ b/charon/tests/ui/simple/drop-string.out @@ -54,6 +54,16 @@ pub struct String { vec: Vec[Sized, Sized, Drop, {impl Drop for Global}], } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop pub fn {impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4])) where diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 519aa3648..9b7f632fa 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -92,6 +92,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::takes_fn fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_0 + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool))) { @@ -108,7 +118,7 @@ fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, ( counter@2 := const (0 : u32) storage_live(@3) storage_live(@4) - @4 := &*(f@1) + @4 := &*(f@1) with_metadata(copy (f@1.metadata)) storage_live(@5) storage_live(@6) storage_live(@7) diff --git a/charon/tests/ui/simple/gat-check-binder-levels.out b/charon/tests/ui/simple/gat-check-binder-levels.out index 0827934b5..958e5790a 100644 --- a/charon/tests/ui/simple/gat-check-binder-levels.out +++ b/charon/tests/ui/simple/gat-check-binder-levels.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Link pub trait Link { diff --git a/charon/tests/ui/simple/gat-complex-lifetimes.out b/charon/tests/ui/simple/gat-complex-lifetimes.out index 33875532f..33dc7103b 100644 --- a/charon/tests/ui/simple/gat-complex-lifetimes.out +++ b/charon/tests/ui/simple/gat-complex-lifetimes.out @@ -26,6 +26,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo pub trait Foo { diff --git a/charon/tests/ui/simple/gat-implied-clause.out b/charon/tests/ui/simple/gat-implied-clause.out index 0996552c9..c3b327003 100644 --- a/charon/tests/ui/simple/gat-implied-clause.out +++ b/charon/tests/ui/simple/gat-implied-clause.out @@ -49,6 +49,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/generic-cast-to-dyn.out b/charon/tests/ui/simple/generic-cast-to-dyn.out index 7fb60b85f..1941c053f 100644 --- a/charon/tests/ui/simple/generic-cast-to-dyn.out +++ b/charon/tests/ui/simple/generic-cast-to-dyn.out @@ -40,6 +40,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : 'static)) where @@ -58,7 +68,7 @@ where @4 := &*(x@1) @3 := unsize_cast<&'_ (T), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), @TraitClause1>(move (@4)) storage_dead(@4) - @2 := &*(@3) + @2 := &*(@3) with_metadata(copy (@3.metadata)) @0 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), Any<(dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)>>(move (@2)) storage_dead(@3) storage_dead(@2) diff --git a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out index 1cae97af2..be915f334 100644 --- a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out +++ b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasType trait HasType { diff --git a/charon/tests/ui/simple/generic-impl-with-defaulted-method.out b/charon/tests/ui/simple/generic-impl-with-defaulted-method.out index 7e27ea309..9619da6ef 100644 --- a/charon/tests/ui/simple/generic-impl-with-defaulted-method.out +++ b/charon/tests/ui/simple/generic-impl-with-defaulted-method.out @@ -22,6 +22,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::BoolTrait pub trait BoolTrait { diff --git a/charon/tests/ui/simple/generic-impl-with-method.out b/charon/tests/ui/simple/generic-impl-with-method.out index e81b29965..95f91ac79 100644 --- a/charon/tests/ui/simple/generic-impl-with-method.out +++ b/charon/tests/ui/simple/generic-impl-with-method.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait pub trait Trait { diff --git a/charon/tests/ui/simple/hide-drops.out b/charon/tests/ui/simple/hide-drops.out index f77962d93..4769312f9 100644 --- a/charon/tests/ui/simple/hide-drops.out +++ b/charon/tests/ui/simple/hide-drops.out @@ -25,6 +25,16 @@ pub opaque type String #[lang_item("string_new")] pub fn new() -> String +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::use_string fn use_string(@1: String) { diff --git a/charon/tests/ui/simple/lending-iterator-gat.out b/charon/tests/ui/simple/lending-iterator-gat.out index 401799a18..00545c5a8 100644 --- a/charon/tests/ui/simple/lending-iterator-gat.out +++ b/charon/tests/ui/simple/lending-iterator-gat.out @@ -104,6 +104,16 @@ pub enum AssertKind { Match, } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::LendingIterator pub trait LendingIterator { diff --git a/charon/tests/ui/simple/match-on-char.out b/charon/tests/ui/simple/match-on-char.out index 45290e351..fa6dc69b7 100644 --- a/charon/tests/ui/simple/match-on-char.out +++ b/charon/tests/ui/simple/match-on-char.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/match-on-float.out b/charon/tests/ui/simple/match-on-float.out index 69cd3fe6c..8f1408b54 100644 --- a/charon/tests/ui/simple/match-on-float.out +++ b/charon/tests/ui/simple/match-on-float.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/mem-discriminant-from-derive.out b/charon/tests/ui/simple/mem-discriminant-from-derive.out index 64f25ab98..dcb7dda8c 100644 --- a/charon/tests/ui/simple/mem-discriminant-from-derive.out +++ b/charon/tests/ui/simple/mem-discriminant-from-derive.out @@ -193,6 +193,16 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Enum enum Enum { Some(u8), diff --git a/charon/tests/ui/simple/metadata-without-marker-trait.out b/charon/tests/ui/simple/metadata-without-marker-trait.out new file mode 100644 index 000000000..170eab206 --- /dev/null +++ b/charon/tests/ui/simple/metadata-without-marker-trait.out @@ -0,0 +1,35 @@ +# Final LLBC before serialization: + +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option { + None, + Some(T), +} + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::wrap_shared_in_option +pub fn wrap_shared_in_option<'a, T>(@1: &'a (T)) -> Option<&'a (T)> +{ + let @0: Option<&'_ (T)>; // return + let x@1: &'_ (T); // arg #1 + let @2: &'_ (T); // anonymous local + + storage_live(@2) + @2 := &*(x@1) + @0 := Option::Some { 0: move (@2) } + storage_dead(@2) + return +} + + + diff --git a/charon/tests/ui/simple/metadata-without-marker-trait.rs b/charon/tests/ui/simple/metadata-without-marker-trait.rs new file mode 100644 index 000000000..b6494cb81 --- /dev/null +++ b/charon/tests/ui/simple/metadata-without-marker-trait.rs @@ -0,0 +1,4 @@ +//@ charon-args=--hide-marker-traits +pub fn wrap_shared_in_option<'a, T>(x: &'a T) -> Option<&'a T> { + Option::Some(x) +} diff --git a/charon/tests/ui/simple/method-with-assoc-type-constraint.out b/charon/tests/ui/simple/method-with-assoc-type-constraint.out index de0725d0b..ec45cf8b1 100644 --- a/charon/tests/ui/simple/method-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/method-with-assoc-type-constraint.out @@ -26,6 +26,16 @@ pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::IntoIterator pub trait IntoIterator { diff --git a/charon/tests/ui/simple/multiple-promoteds.out b/charon/tests/ui/simple/multiple-promoteds.out index f2acf9271..f39246ec0 100644 --- a/charon/tests/ui/simple/multiple-promoteds.out +++ b/charon/tests/ui/simple/multiple-promoteds.out @@ -42,6 +42,16 @@ pub fn core::ops::arith::Add::add(@1: Self, @2: Rhs) -> @TraitClause0 where [@TraitClause0]: Add, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::six fn six() -> u32 { diff --git a/charon/tests/ui/simple/nested-closure-trait-ref.out b/charon/tests/ui/simple/nested-closure-trait-ref.out index 2e16f573a..e3f0b252e 100644 --- a/charon/tests/ui/simple/nested-closure-trait-ref.out +++ b/charon/tests/ui/simple/nested-closure-trait-ref.out @@ -106,6 +106,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + struct test_crate::foo::closure::closure where [@TraitClause0]: Sized, diff --git a/charon/tests/ui/simple/nested-closure.out b/charon/tests/ui/simple/nested-closure.out index 91f00d841..64a00a8b0 100644 --- a/charon/tests/ui/simple/nested-closure.out +++ b/charon/tests/ui/simple/nested-closure.out @@ -106,6 +106,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo struct Foo<'a, T> where diff --git a/charon/tests/ui/simple/nested-inline-const.out b/charon/tests/ui/simple/nested-inline-const.out index a6638e379..81b13991c 100644 --- a/charon/tests/ui/simple/nested-inline-const.out +++ b/charon/tests/ui/simple/nested-inline-const.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/non-lifetime-gats.out b/charon/tests/ui/simple/non-lifetime-gats.out index ca5260a20..8c00f0f60 100644 --- a/charon/tests/ui/simple/non-lifetime-gats.out +++ b/charon/tests/ui/simple/non-lifetime-gats.out @@ -79,6 +79,16 @@ where vtable: {impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::PointerFamily pub trait PointerFamily { diff --git a/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out b/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out index 0a22ff9a4..844a3dc03 100644 --- a/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out +++ b/charon/tests/ui/simple/opaque-trait-with-clause-in-method.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::opaque::Product pub trait Product { diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out index 5db65e5b3..c992fa70c 100644 --- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out @@ -84,6 +84,16 @@ pub fn call_once(@1: Self, @2: Args) -> Clause0_Outp where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::flabada pub fn flabada<'a>(@1: &'a (())) -> &'a (()) { diff --git a/charon/tests/ui/simple/pointee_metadata.out b/charon/tests/ui/simple/pointee_metadata.out index 878431dcb..e0f57b099 100644 --- a/charon/tests/ui/simple/pointee_metadata.out +++ b/charon/tests/ui/simple/pointee_metadata.out @@ -212,6 +212,16 @@ pub trait Pointee // Full name: core::ptr::const_ptr::{*const T}::to_raw_parts pub fn to_raw_parts(@1: *const T) -> (*const (), Pointee::Metadata) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::empty_metadata fn empty_metadata() { diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out index c521d40b7..9c4c5b5a9 100644 --- a/charon/tests/ui/simple/promoted-closure-no-warns.out +++ b/charon/tests/ui/simple/promoted-closure-no-warns.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::closure struct closure {} diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out index c521d40b7..9c4c5b5a9 100644 --- a/charon/tests/ui/simple/promoted-closure.out +++ b/charon/tests/ui/simple/promoted-closure.out @@ -83,6 +83,16 @@ pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> where [@TraitClause0]: FnOnce, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo::closure struct closure {} diff --git a/charon/tests/ui/simple/promoted-in-generic-fn.out b/charon/tests/ui/simple/promoted-in-generic-fn.out index d10289d36..d75385821 100644 --- a/charon/tests/ui/simple/promoted-in-generic-fn.out +++ b/charon/tests/ui/simple/promoted-in-generic-fn.out @@ -18,6 +18,16 @@ pub fn size_of() -> usize where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::f fn f() where diff --git a/charon/tests/ui/simple/promoted-inside-impl.out b/charon/tests/ui/simple/promoted-inside-impl.out index f1bfab04c..3f3f9c11b 100644 --- a/charon/tests/ui/simple/promoted-inside-impl.out +++ b/charon/tests/ui/simple/promoted-inside-impl.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo pub struct Foo where diff --git a/charon/tests/ui/simple/promoted-literal-addition-overflow.out b/charon/tests/ui/simple/promoted-literal-addition-overflow.out index f7313d489..27137fbc9 100644 --- a/charon/tests/ui/simple/promoted-literal-addition-overflow.out +++ b/charon/tests/ui/simple/promoted-literal-addition-overflow.out @@ -6,6 +6,16 @@ pub fn MAX() -> u32 // Full name: core::num::{u32}::MAX pub const MAX: u32 = MAX() +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::overflow fn overflow() -> &'static (u32) { diff --git a/charon/tests/ui/simple/promoted-literal-addition.out b/charon/tests/ui/simple/promoted-literal-addition.out index 153576de5..b4548277f 100644 --- a/charon/tests/ui/simple/promoted-literal-addition.out +++ b/charon/tests/ui/simple/promoted-literal-addition.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::two fn two() -> &'static (u32) { diff --git a/charon/tests/ui/simple/promoted-u32-slice.out b/charon/tests/ui/simple/promoted-u32-slice.out index c0e60166d..701a91e9f 100644 --- a/charon/tests/ui/simple/promoted-u32-slice.out +++ b/charon/tests/ui/simple/promoted-u32-slice.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo pub fn foo() -> &'static (Slice) { diff --git a/charon/tests/ui/simple/ptr-from-raw-parts.out b/charon/tests/ui/simple/ptr-from-raw-parts.out index a9a86403b..9b177c57c 100644 --- a/charon/tests/ui/simple/ptr-from-raw-parts.out +++ b/charon/tests/ui/simple/ptr-from-raw-parts.out @@ -258,6 +258,16 @@ where return } +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/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out index 877654e79..5ea1839d7 100644 --- a/charon/tests/ui/simple/ptr_metadata.out +++ b/charon/tests/ui/simple/ptr_metadata.out @@ -286,6 +286,16 @@ pub fn null() -> *const T where [@TraitClause0]: Thin, +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/simple/ptr_to_promoted.out b/charon/tests/ui/simple/ptr_to_promoted.out index fe84032d5..b8ac80e07 100644 --- a/charon/tests/ui/simple/ptr_to_promoted.out +++ b/charon/tests/ui/simple/ptr_to_promoted.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/quantified-trait-type-constraint.out b/charon/tests/ui/simple/quantified-trait-type-constraint.out index 8d078c0d4..caf19335f 100644 --- a/charon/tests/ui/simple/quantified-trait-type-constraint.out +++ b/charon/tests/ui/simple/quantified-trait-type-constraint.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait<'a, Self, Self_Type> { diff --git a/charon/tests/ui/simple/ref-in-const.out b/charon/tests/ui/simple/ref-in-const.out index 654e7c665..0961d62e8 100644 --- a/charon/tests/ui/simple/ref-in-const.out +++ b/charon/tests/ui/simple/ref-in-const.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::SOME_INT fn SOME_INT() -> &'static (&'static (i32)) { diff --git a/charon/tests/ui/simple/slice_increment.out b/charon/tests/ui/simple/slice_increment.out index 5fdc45ba7..e6b488ea0 100644 --- a/charon/tests/ui/simple/slice_increment.out +++ b/charon/tests/ui/simple/slice_increment.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::incr pub fn incr<'_0>(@1: &'_0 mut (Slice)) { @@ -16,12 +26,12 @@ pub fn incr<'_0>(@1: &'_0 mut (Slice)) storage_live(@2) @2 := const (0 : usize) storage_live(@6) - @6 := &*(s@1) + @6 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@7) @7 := @SliceIndexShared<'_, u32>(move (@6), copy (@2)) @3 := copy (*(@7)) panic.+ const (1 : u32) storage_live(@4) - @4 := &mut *(s@1) + @4 := &mut *(s@1) with_metadata(copy (s@1.metadata)) storage_live(@5) @5 := @SliceIndexMut<'_, u32>(move (@4), copy (@2)) *(@5) := move (@3) diff --git a/charon/tests/ui/simple/slice_index.out b/charon/tests/ui/simple/slice_index.out index 0f5bfbb3c..e38f15e4e 100644 --- a/charon/tests/ui/simple/slice_index.out +++ b/charon/tests/ui/simple/slice_index.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::first pub fn first<'_0>(@1: &'_0 (Slice)) -> u32 { @@ -12,7 +22,7 @@ pub fn first<'_0>(@1: &'_0 (Slice)) -> u32 storage_live(@2) @2 := const (0 : usize) storage_live(@3) - @3 := &*(s@1) + @3 := &*(s@1) with_metadata(copy (s@1.metadata)) storage_live(@4) @4 := @SliceIndexShared<'_, u32>(move (@3), copy (@2)) @0 := copy (*(@4)) diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index 572a44534..55ce799ec 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -86,6 +86,16 @@ where args: &'a (Slice>), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: core::fmt::rt::{Arguments<'a>}::new_const pub fn new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> Arguments<'a> { @@ -433,13 +443,13 @@ where new_len@6 := copy ((@3 as variant Option::Some).0) storage_live(@7) storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := copy (self@4) <= move (@8) if move (@7) { storage_dead(@8) storage_live(@10) storage_live(@11) - @11 := &raw const *(slice@2) + @11 := &raw const *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@14) storage_live(@15) @14 := cast<*const Slice, *const T>(copy (@11)) @@ -448,7 +458,7 @@ where storage_dead(@15) storage_dead(@14) storage_dead(@11) - @9 := &*(@10) + @9 := &*(@10) with_metadata(copy (@10.metadata)) @0 := Option::Some { 0: copy (@9) } storage_dead(@10) storage_dead(@3) @@ -518,13 +528,13 @@ where new_len@6 := copy ((@3 as variant Option::Some).0) storage_live(@7) storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := copy (self@4) <= move (@8) if move (@7) { storage_dead(@8) storage_live(@10) storage_live(ptr@11) - ptr@11 := &raw mut *(slice@2) + ptr@11 := &raw mut *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@14) storage_live(@15) @14 := cast<*mut Slice, *mut T>(copy (ptr@11)) @@ -533,7 +543,7 @@ where storage_dead(@15) storage_dead(@14) storage_dead(ptr@11) - @9 := &mut *(@10) + @9 := &mut *(@10) with_metadata(copy (@10.metadata)) @0 := Option::Some { 0: copy (@9) } storage_dead(@10) storage_dead(@3) @@ -640,7 +650,7 @@ where storage_live(@6) @6 := copy ((self@1).end) storage_live(@7) - @7 := ptr_metadata(copy (slice@2)) + @7 := copy (slice@2.metadata) @4 := {impl SliceIndex> for Range[Sized]}::get_unchecked::precondition_check(move (@5), move (@6), move (@7)) storage_dead(@7) storage_dead(@6) @@ -755,7 +765,7 @@ where storage_live(@6) @6 := copy ((self@1).end) storage_live(@7) - @7 := ptr_metadata(copy (slice@2)) + @7 := copy (slice@2.metadata) @4 := {impl SliceIndex> for Range[Sized]}::get_unchecked_mut::precondition_check(move (@5), move (@6), move (@7)) storage_dead(@7) storage_dead(@6) @@ -830,7 +840,7 @@ where new_len@4 := copy ((@5 as variant Option::Some).0) storage_dead(@5) storage_live(@8) - @9 := ptr_metadata(copy (slice@2)) + @9 := copy (slice@2.metadata) @8 := copy (self@6) > copy (@9) if move (@8) { } @@ -838,7 +848,7 @@ where storage_dead(@8) storage_live(@11) storage_live(@12) - @12 := &raw const *(slice@2) + @12 := &raw const *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@15) storage_live(@16) @15 := cast<*const Slice, *const T>(copy (@12)) @@ -847,7 +857,7 @@ where storage_dead(@16) storage_dead(@15) storage_dead(@12) - @0 := &*(@11) + @0 := &*(@11) with_metadata(copy (@11.metadata)) storage_dead(@11) return } @@ -909,7 +919,7 @@ where new_len@4 := copy ((@5 as variant Option::Some).0) storage_dead(@5) storage_live(@8) - @9 := ptr_metadata(copy (slice@2)) + @9 := copy (slice@2.metadata) @8 := copy (self@6) > copy (@9) if move (@8) { } @@ -917,7 +927,7 @@ where storage_dead(@8) storage_live(@11) storage_live(ptr@12) - ptr@12 := &raw mut *(slice@2) + ptr@12 := &raw mut *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@15) storage_live(@16) @15 := cast<*mut Slice, *mut T>(copy (ptr@12)) @@ -926,7 +936,7 @@ where storage_dead(@16) storage_dead(@15) storage_dead(ptr@12) - @0 := &mut *(@11) + @0 := &mut *(@11) with_metadata(copy (@11.metadata)) storage_dead(@11) return } @@ -1041,13 +1051,13 @@ where storage_dead(@14) storage_live(@9) storage_live(@10) - @10 := ptr_metadata(copy (slice@2)) + @10 := copy (slice@2.metadata) @9 := copy (exclusive_end@6) <= move (@10) if move (@9) { storage_dead(@10) storage_live(@12) storage_live(@13) - @13 := &raw const *(slice@2) + @13 := &raw const *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@16) storage_live(@17) @16 := cast<*const Slice, *const T>(copy (@13)) @@ -1056,7 +1066,7 @@ where storage_dead(@17) storage_dead(@16) storage_dead(@13) - @11 := &*(@12) + @11 := &*(@12) with_metadata(copy (@12.metadata)) @0 := Option::Some { 0: copy (@11) } storage_dead(@12) } @@ -1158,13 +1168,13 @@ where storage_dead(@14) storage_live(@9) storage_live(@10) - @10 := ptr_metadata(copy (slice@2)) + @10 := copy (slice@2.metadata) @9 := copy (exclusive_end@6) <= move (@10) if move (@9) { storage_dead(@10) storage_live(@12) storage_live(ptr@13) - ptr@13 := &raw mut *(slice@2) + ptr@13 := &raw mut *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@16) storage_live(@17) @16 := cast<*mut Slice, *mut T>(copy (ptr@13)) @@ -1173,7 +1183,7 @@ where storage_dead(@17) storage_dead(@16) storage_dead(ptr@13) - @11 := &mut *(@12) + @11 := &mut *(@12) with_metadata(copy (@12.metadata)) @0 := Option::Some { 0: copy (@11) } storage_dead(@12) } @@ -1237,7 +1247,7 @@ where @6 := ub_checks if move (@6) { storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := {impl SliceIndex> for Range[Sized]}::get_unchecked::precondition_check(copy (self@5), copy (exclusive_end@3), move (@8)) storage_dead(@8) } @@ -1303,7 +1313,7 @@ where @6 := ub_checks if move (@6) { storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := {impl SliceIndex> for Range[Sized]}::get_unchecked_mut::precondition_check(copy (self@5), copy (exclusive_end@3), move (@8)) storage_dead(@8) } @@ -1482,14 +1492,14 @@ pub fn slice_index_range<'_0>(@1: &'_0 (Slice)) -> &'_0 (Slice) storage_live(@2) storage_live(@3) storage_live(@4) - @4 := &*(slice@1) + @4 := &*(slice@1) with_metadata(copy (slice@1.metadata)) storage_live(@5) @5 := new[Sized](const (0 : usize), const (10 : usize)) @3 := {impl Index for Slice}::index<'_, u8, RangeInclusive[Sized]>[Sized, Sized[Sized]>, {impl SliceIndex> for RangeInclusive[Sized]}[Sized]](move (@4), move (@5)) storage_dead(@5) storage_dead(@4) - @2 := &*(@3) - @0 := &*(@2) + @2 := &*(@3) with_metadata(copy (@3.metadata)) + @0 := &*(@2) with_metadata(copy (@2.metadata)) storage_dead(@3) storage_dead(@2) return diff --git a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out index e00f1fd97..707795d40 100644 --- a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::HasAssoc trait HasAssoc { diff --git a/charon/tests/ui/simple/trait-alias.out b/charon/tests/ui/simple/trait-alias.out index 3df1ecc94..4be456077 100644 --- a/charon/tests/ui/simple/trait-alias.out +++ b/charon/tests/ui/simple/trait-alias.out @@ -58,6 +58,16 @@ where Some(T), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/trait-default-const-cross-crate.out b/charon/tests/ui/simple/trait-default-const-cross-crate.out index 69f2b318e..94a02dbd3 100644 --- a/charon/tests/ui/simple/trait-default-const-cross-crate.out +++ b/charon/tests/ui/simple/trait-default-const-cross-crate.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: trait_default_const::Trait trait Trait { diff --git a/charon/tests/ui/simple/trait-default-const.out b/charon/tests/ui/simple/trait-default-const.out index 94836fbc7..8ab054ada 100644 --- a/charon/tests/ui/simple/trait-default-const.out +++ b/charon/tests/ui/simple/trait-default-const.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Trait trait Trait { diff --git a/charon/tests/ui/simple/uncheck-ops.out b/charon/tests/ui/simple/uncheck-ops.out index c95c33585..380aef859 100644 --- a/charon/tests/ui/simple/uncheck-ops.out +++ b/charon/tests/ui/simple/uncheck-ops.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +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/simple/vec-push.out b/charon/tests/ui/simple/vec-push.out index aa992d92f..70392bb44 100644 --- a/charon/tests/ui/simple/vec-push.out +++ b/charon/tests/ui/simple/vec-push.out @@ -69,6 +69,16 @@ where len: usize, } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: alloc::vec::{Vec[@TraitClause0, @TraitClause1]}::push pub fn push<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1]), @2: T) where diff --git a/charon/tests/ui/simple/vec-with-capacity.out b/charon/tests/ui/simple/vec-with-capacity.out index 618112055..692a52a72 100644 --- a/charon/tests/ui/simple/vec-with-capacity.out +++ b/charon/tests/ui/simple/vec-with-capacity.out @@ -199,6 +199,16 @@ where vtable: {impl Drop for Vec[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::vec fn vec() { diff --git a/charon/tests/ui/simple/wrapping-ops.out b/charon/tests/ui/simple/wrapping-ops.out index 5b0eacce4..f5033d022 100644 --- a/charon/tests/ui/simple/wrapping-ops.out +++ b/charon/tests/ui/simple/wrapping-ops.out @@ -33,6 +33,16 @@ pub fn wrapping_mul(@1: u8, @2: u8) -> u8 return } +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/skip-borrowck.out b/charon/tests/ui/skip-borrowck.out index 921ab9d3b..c44619120 100644 --- a/charon/tests/ui/skip-borrowck.out +++ b/charon/tests/ui/skip-borrowck.out @@ -12,6 +12,16 @@ pub trait Sized non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::choose fn choose<'a, T>(@1: bool, @2: &'a mut (T), @3: &'a mut (T)) -> &'a mut (T) where diff --git a/charon/tests/ui/slice-index-range.out b/charon/tests/ui/slice-index-range.out index 1fecedb13..231bbb5e7 100644 --- a/charon/tests/ui/slice-index-range.out +++ b/charon/tests/ui/slice-index-range.out @@ -293,13 +293,13 @@ where new_len@6 := copy ((@3 as variant Option::Some).0) storage_live(@7) storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := copy (self@4) <= move (@8) if move (@7) { storage_dead(@8) storage_live(@10) storage_live(@11) - @11 := &raw const *(slice@2) + @11 := &raw const *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@14) storage_live(@15) @14 := cast<*const Slice, *const T>(copy (@11)) @@ -308,7 +308,7 @@ where storage_dead(@15) storage_dead(@14) storage_dead(@11) - @9 := &*(@10) + @9 := &*(@10) with_metadata(copy (@10.metadata)) @0 := Option::Some { 0: copy (@9) } storage_dead(@10) storage_dead(@3) @@ -378,13 +378,13 @@ where new_len@6 := copy ((@3 as variant Option::Some).0) storage_live(@7) storage_live(@8) - @8 := ptr_metadata(copy (slice@2)) + @8 := copy (slice@2.metadata) @7 := copy (self@4) <= move (@8) if move (@7) { storage_dead(@8) storage_live(@10) storage_live(ptr@11) - ptr@11 := &raw mut *(slice@2) + ptr@11 := &raw mut *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@14) storage_live(@15) @14 := cast<*mut Slice, *mut T>(copy (ptr@11)) @@ -393,7 +393,7 @@ where storage_dead(@15) storage_dead(@14) storage_dead(ptr@11) - @9 := &mut *(@10) + @9 := &mut *(@10) with_metadata(copy (@10.metadata)) @0 := Option::Some { 0: copy (@9) } storage_dead(@10) storage_dead(@3) @@ -409,6 +409,16 @@ where return } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: core::slice::index::{impl SliceIndex> for Range[Sized]}::get_unchecked::precondition_check fn {impl SliceIndex> for Range[Sized]}::get_unchecked::precondition_check(@1: usize, @2: usize, @3: usize) { @@ -494,7 +504,7 @@ where storage_live(@6) @6 := copy ((self@1).end) storage_live(@7) - @7 := ptr_metadata(copy (slice@2)) + @7 := copy (slice@2.metadata) @4 := {impl SliceIndex> for Range[Sized]}::get_unchecked::precondition_check(move (@5), move (@6), move (@7)) storage_dead(@7) storage_dead(@6) @@ -603,7 +613,7 @@ where storage_live(@6) @6 := copy ((self@1).end) storage_live(@7) - @7 := ptr_metadata(copy (slice@2)) + @7 := copy (slice@2.metadata) @4 := {impl SliceIndex> for Range[Sized]}::get_unchecked_mut::precondition_check(move (@5), move (@6), move (@7)) storage_dead(@7) storage_dead(@6) @@ -678,7 +688,7 @@ where new_len@4 := copy ((@5 as variant Option::Some).0) storage_dead(@5) storage_live(@8) - @9 := ptr_metadata(copy (slice@2)) + @9 := copy (slice@2.metadata) @8 := copy (self@6) > copy (@9) if move (@8) { } @@ -686,7 +696,7 @@ where storage_dead(@8) storage_live(@11) storage_live(@12) - @12 := &raw const *(slice@2) + @12 := &raw const *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@15) storage_live(@16) @15 := cast<*const Slice, *const T>(copy (@12)) @@ -695,7 +705,7 @@ where storage_dead(@16) storage_dead(@15) storage_dead(@12) - @0 := &*(@11) + @0 := &*(@11) with_metadata(copy (@11.metadata)) storage_dead(@11) return } @@ -757,7 +767,7 @@ where new_len@4 := copy ((@5 as variant Option::Some).0) storage_dead(@5) storage_live(@8) - @9 := ptr_metadata(copy (slice@2)) + @9 := copy (slice@2.metadata) @8 := copy (self@6) > copy (@9) if move (@8) { } @@ -765,7 +775,7 @@ where storage_dead(@8) storage_live(@11) storage_live(ptr@12) - ptr@12 := &raw mut *(slice@2) + ptr@12 := &raw mut *(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@15) storage_live(@16) @15 := cast<*mut Slice, *mut T>(copy (ptr@12)) @@ -774,7 +784,7 @@ where storage_dead(@16) storage_dead(@15) storage_dead(ptr@12) - @0 := &mut *(@11) + @0 := &mut *(@11) with_metadata(copy (@11.metadata)) storage_dead(@11) return } @@ -831,14 +841,14 @@ fn main() @3 := {impl Index for Array}::index<'_, i32, Range[Sized], 6 : usize>[Sized, Sized[Sized]>, {impl Index for Slice}[Sized]>[Sized, Sized[Sized]>, {impl SliceIndex> for Range[Sized]}[Sized]]](move (@4), move (@5)) storage_dead(@5) storage_dead(@4) - slice@2 := &*(@3) + slice@2 := &*(@3) with_metadata(copy (@3.metadata)) storage_live(@6) storage_live(@7) storage_live(@8) storage_live(@9) @9 := const (0 : usize) storage_live(@10) - @10 := &*(slice@2) + @10 := &*(slice@2) with_metadata(copy (slice@2.metadata)) storage_live(@11) @11 := @SliceIndexShared<'_, i32>(move (@10), copy (@9)) @8 := copy (*(@11)) diff --git a/charon/tests/ui/start_from.out b/charon/tests/ui/start_from.out index 3fd12a9a5..0dedd42bb 100644 --- a/charon/tests/ui/start_from.out +++ b/charon/tests/ui/start_from.out @@ -42,6 +42,16 @@ where [@TraitClause0]: Clone, [@TraitClause1]: Destruct, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun4() + // Full name: core::iter::sources::once::Once #[lang_item("IterOnce")] pub opaque type Once diff --git a/charon/tests/ui/statics.out b/charon/tests/ui/statics.out index 8ca5c3c59..c4f5e6d3e 100644 --- a/charon/tests/ui/statics.out +++ b/charon/tests/ui/statics.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::constant::CONST fn CONST() -> usize { @@ -64,28 +74,37 @@ fn shared_static() let @4: &'_ (usize); // anonymous local let _ptr@5: *const usize; // local let @6: &'_ (usize); // anonymous local - let @7: &'_ (usize); // anonymous local + let @7: (); // anonymous local let @8: &'_ (usize); // anonymous local - let @9: &'_ (usize); // anonymous local + let @9: (); // anonymous local + let @10: &'_ (usize); // anonymous local + let @11: (); // anonymous local + let @12: &'_ (usize); // anonymous local storage_live(@7) storage_live(@8) storage_live(@9) + storage_live(@10) + storage_live(@11) + storage_live(@12) storage_live(_val@1) storage_live(@2) - @7 := &SHARED_STATIC - @2 := move (@7) + @7 := () + @8 := &SHARED_STATIC + @2 := move (@8) _val@1 := copy (*(@2)) storage_dead(@2) storage_live(_ref@3) storage_live(@4) - @8 := &SHARED_STATIC - @4 := move (@8) + @9 := () + @10 := &SHARED_STATIC + @4 := move (@10) _ref@3 := &*(@4) storage_live(_ptr@5) storage_live(@6) - @9 := &SHARED_STATIC - @6 := move (@9) + @11 := () + @12 := &SHARED_STATIC + @6 := move (@12) _ptr@5 := &raw const *(@6) @0 := () storage_dead(@6) @@ -123,42 +142,57 @@ fn mut_static() let @8: *mut usize; // anonymous local let _ptr_mut@9: *mut usize; // local let @10: *mut usize; // anonymous local - let @11: *mut usize; // anonymous local + let @11: (); // anonymous local let @12: *mut usize; // anonymous local - let @13: *mut usize; // anonymous local + let @13: (); // anonymous local let @14: *mut usize; // anonymous local - let @15: *mut usize; // anonymous local + let @15: (); // anonymous local + let @16: *mut usize; // anonymous local + let @17: (); // anonymous local + let @18: *mut usize; // anonymous local + let @19: (); // anonymous local + let @20: *mut usize; // anonymous local storage_live(@11) storage_live(@12) storage_live(@13) storage_live(@14) storage_live(@15) + storage_live(@16) + storage_live(@17) + storage_live(@18) + storage_live(@19) + storage_live(@20) storage_live(_val@1) storage_live(@2) - @11 := &raw mut MUT_STATIC - @2 := move (@11) + @11 := () + @12 := &raw mut MUT_STATIC + @2 := move (@12) _val@1 := copy (*(@2)) storage_dead(@2) storage_live(_ref@3) storage_live(@4) - @12 := &raw mut MUT_STATIC - @4 := move (@12) + @13 := () + @14 := &raw mut MUT_STATIC + @4 := move (@14) _ref@3 := &*(@4) storage_live(_ref_mut@5) storage_live(@6) - @13 := &raw mut MUT_STATIC - @6 := move (@13) + @15 := () + @16 := &raw mut MUT_STATIC + @6 := move (@16) _ref_mut@5 := &mut *(@6) storage_live(_ptr@7) storage_live(@8) - @14 := &raw mut MUT_STATIC - @8 := move (@14) + @17 := () + @18 := &raw mut MUT_STATIC + @8 := move (@18) _ptr@7 := &raw const *(@8) storage_live(_ptr_mut@9) storage_live(@10) - @15 := &raw mut MUT_STATIC - @10 := move (@15) + @19 := () + @20 := &raw mut MUT_STATIC + @10 := move (@20) _ptr_mut@9 := &raw mut *(@10) @0 := () storage_dead(@10) @@ -206,13 +240,16 @@ fn non_copy_static() let @0: (); // return let @1: &'_ (Foo); // anonymous local let @2: &'_ (Foo); // anonymous local - let @3: &'_ (Foo); // anonymous local + let @3: (); // anonymous local + let @4: &'_ (Foo); // anonymous local storage_live(@3) + storage_live(@4) storage_live(@1) storage_live(@2) - @3 := &FOO - @2 := move (@3) + @3 := () + @4 := &FOO + @2 := move (@4) @1 := &*(@2) @0 := method<'_>(move (@1)) storage_dead(@1) diff --git a/charon/tests/ui/stealing.out b/charon/tests/ui/stealing.out index 2f407e4f1..6827b5f5c 100644 --- a/charon/tests/ui/stealing.out +++ b/charon/tests/ui/stealing.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::SLICE fn SLICE() -> Array<(), 4 : usize> { diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index 3f8e52008..afe2aa814 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -105,6 +105,16 @@ where vtable: {impl ToString for T}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::FOO fn FOO() -> &'static (Str) { @@ -124,15 +134,18 @@ fn BAR() -> &'static (Slice) let @1: &'_ (Array); // anonymous local let @2: &'_ (Array); // anonymous local let @3: Array; // anonymous local - let @4: &'_ (Array); // anonymous local + let @4: (); // anonymous local + let @5: &'_ (Array); // anonymous local storage_live(@3) storage_live(@4) + storage_live(@5) storage_live(@1) storage_live(@2) @3 := [const (104 : u8), const (101 : u8), const (108 : u8), const (108 : u8), const (111 : u8)] - @4 := &@3 - @2 := move (@4) + @4 := () + @5 := &@3 + @2 := move (@5) @1 := &*(@2) @0 := @ArrayToSliceShared<'_, u8, 5 : usize>(move (@1)) storage_dead(@2) @@ -155,7 +168,7 @@ fn main() storage_live(@2) storage_live(@3) @3 := const ("Hello") - @2 := &*(@3) + @2 := &*(@3) with_metadata(copy (@3.metadata)) _s@1 := {impl ToString for T}::to_string<'_, Str>[MetaSized, {impl Display for Str}](move (@2)) storage_dead(@2) storage_dead(@3) diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 9c657da2a..744609e83 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -122,6 +122,16 @@ where #[lang_item("String")] pub opaque type String +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::BoolTrait pub trait BoolTrait { diff --git a/charon/tests/ui/traits_special.out b/charon/tests/ui/traits_special.out index b57479284..b464eb410 100644 --- a/charon/tests/ui/traits_special.out +++ b/charon/tests/ui/traits_special.out @@ -23,6 +23,16 @@ where Err(E), } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::From pub trait From { diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out index 98daa8bf3..3c89e0b3c 100644 --- a/charon/tests/ui/type_alias.out +++ b/charon/tests/ui/type_alias.out @@ -128,6 +128,16 @@ where non-dyn-compatible } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Generic2 struct Generic2<'a, T> where diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out index f680744f0..60f450c89 100644 --- a/charon/tests/ui/type_inference_is_order_dependent.out +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -107,6 +107,16 @@ where // Full name: std::io::stdio::_print pub fn _print<'_0>(@1: Arguments<'_0>) +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Left trait Left { diff --git a/charon/tests/ui/typenum.out b/charon/tests/ui/typenum.out index 2a68cbc59..2bb5ff9e8 100644 --- a/charon/tests/ui/typenum.out +++ b/charon/tests/ui/typenum.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::UInt pub struct UInt { U, diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out index 85ebb175f..6c9e9480d 100644 --- a/charon/tests/ui/ullbc-control-flow.out +++ b/charon/tests/ui/ullbc-control-flow.out @@ -547,6 +547,18 @@ where vtable: core::ops::try_trait::Residual::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + bb0: { + @0 := (); + return; + } +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::nested_loops_enum pub fn nested_loops_enum(@1: usize, @2: usize) -> usize { diff --git a/charon/tests/ui/unions.out b/charon/tests/ui/unions.out index 996c76f25..034255397 100644 --- a/charon/tests/ui/unions.out +++ b/charon/tests/ui/unions.out @@ -1,5 +1,15 @@ # Final LLBC before serialization: +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo union Foo { one: u64, diff --git a/charon/tests/ui/unsafe-impl-send.out b/charon/tests/ui/unsafe-impl-send.out index 437c18fca..4de681dfc 100644 --- a/charon/tests/ui/unsafe-impl-send.out +++ b/charon/tests/ui/unsafe-impl-send.out @@ -4,6 +4,16 @@ #[lang_item("Send")] pub trait Send +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Foo struct Foo { *const (), diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 6f4a50c1c..73fc60e49 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -274,6 +274,16 @@ pub fn null() -> *const T where [@TraitClause0]: Thin, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::call_unsafe_fn fn call_unsafe_fn() { @@ -345,13 +355,16 @@ fn access_mutable_static() let @0: (); // return let @1: *mut usize; // anonymous local let @2: usize; // anonymous local - let @3: *mut usize; // anonymous local + let @3: (); // anonymous local + let @4: *mut usize; // anonymous local storage_live(@2) storage_live(@3) + storage_live(@4) storage_live(@1) - @3 := &raw mut COUNTER - @1 := move (@3) + @3 := () + @4 := &raw mut COUNTER + @1 := move (@4) @2 := copy (*(@1)) panic.+ const (1 : usize) *(@1) := move (@2) storage_dead(@1) diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index f033ba1ba..2cbfda595 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -177,6 +177,16 @@ impl Display for String { vtable: {impl Display for String}::{vtable} } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::foo fn foo() { diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out index 53634e3fd..8f5cb7436 100644 --- a/charon/tests/ui/unsupported/issue-79-bound-regions.out +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out @@ -406,6 +406,16 @@ pub fn iter<'_0, T>(@1: &'_0 (Slice)) -> Iter<'_0, T>[@TraitClause0] where [@TraitClause0]: Sized, +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::main fn main() { @@ -433,7 +443,7 @@ fn main() storage_live(@6) storage_live(@7) storage_live(@8) - @8 := &*(slice@1) + @8 := &*(slice@1) with_metadata(copy (slice@1.metadata)) @7 := iter<'_, i32>[Sized](move (@8)) @6 := &two-phase-mut @7 storage_dead(@8) diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 1624b22b9..c10b188fd 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -173,6 +173,16 @@ where vtable: {impl ToString for T}::{vtable}[@TraitClause0, @TraitClause1] } +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + // Full name: test_crate::Super trait Super { @@ -261,11 +271,14 @@ fn {impl Checkable for i32}::check<'_0>(@1: &'_0 (i32)) -> bool fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: &'static (test_crate::Super::{vtable}); // anonymous local + let @1: (); // anonymous local + let @2: &'static (test_crate::Super::{vtable}); // anonymous local storage_live(@1) - @1 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1) } + storage_live(@2) + @1 := () + @2 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } return } @@ -354,7 +367,7 @@ where @4 := &*(arg@1) @3 := unsize_cast<&'_ (T), &'_ ((dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)), @TraitClause1>(move (@4)) storage_dead(@4) - @2 := &*(@3) + @2 := &*(@3) with_metadata(copy (@3.metadata)) @0 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)), &'_ ((dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)), NoParam<(dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)>>(move (@2)) storage_dead(@3) storage_dead(@2) @@ -461,7 +474,7 @@ where storage_dead(@3) storage_dead(@4) storage_live(@6) - @6 := &two-phase-mut *(x@2) + @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata)) storage_live(@7) @7 := &*(arg@1) @0 := Modifiable<(dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_), T>::modify<'_, '_>(move (@6), move (@7)) @@ -523,7 +536,7 @@ where storage_live(@4) storage_live(@5) - @5 := &*(self@1) + @5 := &*(self@1) with_metadata(copy (self@1.metadata)) storage_live(@6) @6 := &*(t32@2) @4 := @TraitClause0::parent_clause1::operate_on<'_, '_>(move (@5), move (@6)) @@ -532,7 +545,7 @@ where storage_dead(@4) storage_live(@7) storage_live(@8) - @8 := &*(self@1) + @8 := &*(self@1) with_metadata(copy (self@1.metadata)) storage_live(@9) @9 := &*(t64@3) @7 := @TraitClause0::parent_clause2::operate_on<'_, '_>(move (@8), move (@9)) @@ -672,14 +685,20 @@ fn test_crate::{impl Both32And64 for i32}::both_operate<'_0, '_1, '_2>(@1: &'_0 fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} { let ret@0: test_crate::Both32And64::{vtable}; // return - let @1: &'static (test_crate::BaseOn::{vtable}); // anonymous local - let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @1: (); // anonymous local + let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @3: (); // anonymous local + let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local storage_live(@1) storage_live(@2) - @1 := &{impl BaseOn for i32}::{vtable} - @2 := &{impl BaseOn for i32}::{vtable} - ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for provided methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1), super_trait_2: move (@2) } + storage_live(@3) + storage_live(@4) + @1 := () + @2 := &{impl BaseOn for i32}::{vtable} + @3 := () + @4 := &{impl BaseOn for i32}::{vtable} + ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for provided methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } return } @@ -719,7 +738,7 @@ fn use_alias<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Both32And64<_dyn> storage_live(@2) storage_live(@3) - @3 := &*(x@1) + @3 := &*(x@1) with_metadata(copy (x@1.metadata)) storage_live(@4) storage_live(@5) storage_live(@6) @@ -868,7 +887,7 @@ fn main() storage_live(@5) storage_live(@6) storage_live(@7) - @7 := &*(x@1) + @7 := &*(x@1) with_metadata(copy (x@1.metadata)) @6 := Checkable<(dyn exists<_dyn> [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_), i32>::check<'_>(move (@7)) if move (@6) { } @@ -899,7 +918,7 @@ fn main() storage_live(@19) storage_live(@20) @20 := const ("Hello") - @19 := &*(@20) + @19 := &*(@20) with_metadata(copy (@20.metadata)) @18 := {impl ToString for T}::to_string<'_, Str>[MetaSized, {impl Display for Str}](move (@19)) storage_dead(@19) @17 := &@18 @@ -925,7 +944,7 @@ fn main() storage_live(@23) storage_live(@24) storage_live(@25) - @25 := &two-phase-mut *(y@8) + @25 := &two-phase-mut *(y@8) with_metadata(copy (y@8.metadata)) storage_live(@26) storage_live(@27) storage_live(@28) @@ -995,7 +1014,7 @@ fn main() @47 := &@48 @46 := &*(@47) @45 := to_dyn_obj<'_, i32>[Sized, {impl NoParam for i32}](move (@46)) - @44 := &*(@45) + @44 := &*(@45) with_metadata(copy (@45.metadata)) z@43 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)), &'_ ((dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)), NoParam<(dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)>>(move (@44)) storage_dead(@46) storage_dead(@44) @@ -1004,7 +1023,7 @@ fn main() storage_dead(@45) storage_live(@49) storage_live(@50) - @50 := &*(z@43) + @50 := &*(z@43) with_metadata(copy (z@43.metadata)) @49 := NoParam<(dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)>::dummy<'_>(move (@50)) storage_dead(@50) storage_dead(@49) @@ -1020,7 +1039,7 @@ fn main() storage_dead(@53) storage_live(@55) storage_live(@56) - @56 := &*(a@51) + @56 := &*(a@51) with_metadata(copy (a@51.metadata)) storage_live(@57) storage_live(@58) storage_live(@59)