diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 020e6f062..018827cd5 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.109" +let supported_charon_version = "0.1.110" diff --git a/charon-ml/src/OfJsonBasic.ml b/charon-ml/src/OfJsonBasic.ml index 91059fb2e..29393cb2c 100644 --- a/charon-ml/src/OfJsonBasic.ml +++ b/charon-ml/src/OfJsonBasic.ml @@ -56,6 +56,18 @@ let pair_of_json (a_of_json : 'ctx -> json -> ('a, string) result) Ok (a, b) | _ -> Error ("pair_of_json failed on: " ^ show js) +let triple_of_json (a_of_json : 'ctx -> json -> ('a, string) result) + (b_of_json : 'ctx -> json -> ('b, string) result) + (c_of_json : 'ctx -> json -> ('c, string) result) (ctx : 'ctx) (js : json) : + ('a * 'b * 'c, string) result = + match js with + | `List [ a; b; c ] -> + let* a = a_of_json ctx a in + let* b = b_of_json ctx b in + let* c = c_of_json ctx c in + Ok (a, b, c) + | _ -> Error ("triple_of_json failed on: " ^ show js) + let list_of_json (a_of_json : 'ctx -> json -> ('a, string) result) (ctx : 'ctx) (js : json) : ('a list, string) result = combine_error_msgs js "list_of_json" diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index 9f06d3c6b..a54f9d149 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -36,7 +36,7 @@ module Ast = struct | StorageDead var_id -> indent ^ "storage_dead " ^ local_id_to_string env var_id | Deinit p -> indent ^ "deinit " ^ place_to_string env p - | Drop p -> indent ^ "drop " ^ place_to_string env p + | Drop (p, _) -> indent ^ "drop " ^ place_to_string env p | Assert a -> assertion_to_string env indent a | Call call -> call_to_string env indent call | Abort (Panic _) -> indent ^ "panic" diff --git a/charon-ml/src/PrintUllbcAst.ml b/charon-ml/src/PrintUllbcAst.ml index 84b91b4b7..86b389f57 100644 --- a/charon-ml/src/PrintUllbcAst.ml +++ b/charon-ml/src/PrintUllbcAst.ml @@ -33,7 +33,7 @@ module Ast = struct | StorageDead var_id -> indent ^ "storage_dead " ^ local_id_to_string env var_id | Deinit p -> indent ^ "deinit " ^ place_to_string env p - | Drop p -> indent ^ "drop " ^ place_to_string env p + | Drop (p, _) -> indent ^ "drop " ^ place_to_string env p | CopyNonOverlapping { src; dst; count } -> indent ^ "copy_non_overlapping(" ^ operand_to_string env src ^ ", " ^ operand_to_string env dst ^ ", " diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 8880c88d9..d5caaef2d 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -337,6 +337,9 @@ type cli_options = { trait definitions to be mutually recursive with their method declarations. This flag removes [Self] clauses that aren't used to break this mutual recursion. *) + add_drop_bounds : bool; + (** Whether to add [Drop] bounds everywhere to enable proper tracking of + what code runs on a given [drop] call. *) start_from : string list; (** A list of item paths to use as starting points for the translation. We will translate these items and any items they refer to, according to diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 4547b5715..7509ae9f0 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -316,6 +316,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : ("remove_associated_types", remove_associated_types); ("hide_marker_traits", hide_marker_traits); ("remove_unused_self_clauses", remove_unused_self_clauses); + ("add_drop_bounds", add_drop_bounds); ("start_from", start_from); ("no_cargo", no_cargo); ("rustc_args", rustc_args); @@ -357,6 +358,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : let* remove_unused_self_clauses = bool_of_json ctx remove_unused_self_clauses in + let* add_drop_bounds = bool_of_json ctx add_drop_bounds in let* start_from = list_of_json string_of_json ctx start_from in let* no_cargo = bool_of_json ctx no_cargo in let* rustc_args = list_of_json string_of_json ctx rustc_args in @@ -397,6 +399,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : remove_associated_types; hide_marker_traits; remove_unused_self_clauses; + add_drop_bounds; start_from; no_cargo; rustc_args; @@ -1708,7 +1711,8 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) : in let* types = list_of_json - (pair_of_json trait_item_name_of_json ty_of_json) + (triple_of_json trait_item_name_of_json ty_of_json + (vector_of_json trait_clause_id_of_json trait_ref_of_json)) ctx types in Ok (BuiltinOrAuto (trait_decl_ref, parent_trait_refs, types)) diff --git a/charon-ml/src/generated/Generated_LlbcAst.ml b/charon-ml/src/generated/Generated_LlbcAst.ml index 7b8068c1c..c5315a9f7 100644 --- a/charon-ml/src/generated/Generated_LlbcAst.ml +++ b/charon-ml/src/generated/Generated_LlbcAst.ml @@ -29,7 +29,7 @@ and raw_statement = the function's body, in which case it is implicitly deallocated at the end of the function. *) | Deinit of place - | Drop of place + | Drop of place * trait_ref (** Drop the value at the given place. For MIR built and promoted, this is a conditional drop: the value will diff --git a/charon-ml/src/generated/Generated_LlbcOfJson.ml b/charon-ml/src/generated/Generated_LlbcOfJson.ml index 31fc04f48..f6ba4106d 100644 --- a/charon-ml/src/generated/Generated_LlbcOfJson.ml +++ b/charon-ml/src/generated/Generated_LlbcOfJson.ml @@ -40,9 +40,10 @@ and raw_statement_of_json (ctx : of_json_ctx) (js : json) : | `Assoc [ ("Deinit", deinit) ] -> let* deinit = place_of_json ctx deinit in Ok (Deinit deinit) - | `Assoc [ ("Drop", drop) ] -> - let* drop = place_of_json ctx drop in - Ok (Drop drop) + | `Assoc [ ("Drop", `List [ x_0; x_1 ]) ] -> + let* x_0 = place_of_json ctx x_0 in + let* x_1 = trait_ref_of_json ctx x_1 in + Ok (Drop (x_0, x_1)) | `Assoc [ ("Assert", assert_) ] -> let* assert_ = assertion_of_json ctx assert_ in Ok (Assert assert_) diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index bae6972fc..f514bd449 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -327,7 +327,7 @@ and trait_instance_id = | BuiltinOrAuto of trait_decl_ref region_binder * trait_ref list - * (trait_item_name * ty) list + * (trait_item_name * ty * trait_ref list) list (** A trait implementation that is computed by the compiler, such as for built-in trait [Sized]. This morally points to an invisible [impl] block; as such it contains the information we may need from one. diff --git a/charon-ml/src/generated/Generated_UllbcAst.ml b/charon-ml/src/generated/Generated_UllbcAst.ml index f4781c7e6..727dfbdc6 100644 --- a/charon-ml/src/generated/Generated_UllbcAst.ml +++ b/charon-ml/src/generated/Generated_UllbcAst.ml @@ -29,7 +29,7 @@ and raw_statement = the function's body, in which case it is implicitly deallocated at the end of the function. *) | Deinit of place - | Drop of place + | Drop of place * trait_ref | Assert of assertion (** A built-in assert, which corresponds to runtime checks that we remove, namely: bounds checks, over/underflow checks, div/rem by zero checks, diff --git a/charon-ml/src/generated/Generated_UllbcOfJson.ml b/charon-ml/src/generated/Generated_UllbcOfJson.ml index 30b099ba4..08a4be69a 100644 --- a/charon-ml/src/generated/Generated_UllbcOfJson.ml +++ b/charon-ml/src/generated/Generated_UllbcOfJson.ml @@ -54,9 +54,10 @@ and raw_statement_of_json (ctx : of_json_ctx) (js : json) : | `Assoc [ ("Deinit", deinit) ] -> let* deinit = place_of_json ctx deinit in Ok (Deinit deinit) - | `Assoc [ ("Drop", drop) ] -> - let* drop = place_of_json ctx drop in - Ok (Drop drop) + | `Assoc [ ("Drop", `List [ x_0; x_1 ]) ] -> + let* x_0 = place_of_json ctx x_0 in + let* x_1 = trait_ref_of_json ctx x_1 in + Ok (Drop (x_0, x_1)) | `Assoc [ ("Assert", assert_) ] -> let* assert_ = assertion_of_json ctx assert_ in Ok (Assert assert_) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 528421ba0..373eb6c65 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -200,7 +200,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.109" +version = "0.1.110" dependencies = [ "annotate-snippets", "anstream", @@ -438,9 +438,9 @@ dependencies = [ [[package]] name = "derive_generic_visitor" -version = "0.1.1" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e1c241e4f464b614bd7650f1a7c4c0e20e5ef21564d6b916b4c51fd76f7688" +checksum = "8f97cf6da50801d6ce913a011f0588883b9ef894603adc3cb40ebe1eb1ac43e5" dependencies = [ "derive_generic_visitor_macros", ] @@ -788,7 +788,7 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" [[package]] name = "hax-adt-into" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#358c68c886e13101fa27df8b7766d636c574cc43" +source = "git+https://github.com/AeneasVerif/hax?branch=main#7382371b43796c7a1b4abc8cd12153fe0f1409ec" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -799,7 +799,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#358c68c886e13101fa27df8b7766d636c574cc43" +source = "git+https://github.com/AeneasVerif/hax?branch=main#7382371b43796c7a1b4abc8cd12153fe0f1409ec" dependencies = [ "extension-traits", "hax-adt-into", @@ -816,7 +816,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#358c68c886e13101fa27df8b7766d636c574cc43" +source = "git+https://github.com/AeneasVerif/hax?branch=main#7382371b43796c7a1b4abc8cd12153fe0f1409ec" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 2a9337b32..8e95e7e56 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.109" +version = "0.1.110" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/llbc_ast.rs b/charon/src/ast/llbc_ast.rs index e7efcd9f9..e73debe9a 100644 --- a/charon/src/ast/llbc_ast.rs +++ b/charon/src/ast/llbc_ast.rs @@ -41,7 +41,7 @@ pub enum RawStatement { /// it has not already been moved out. For MIR elaborated and optimized, this is a real drop. /// /// This drop is then equivalent to a call to `std::ptr::drop_in_place(&raw mut place)`. - Drop(Place), + Drop(Place, TraitRef), Assert(Assert), Call(Call), /// Panic also handles "unreachable". We keep the name of the panicking function that was diff --git a/charon/src/ast/meta.rs b/charon/src/ast/meta.rs index edc4fe00c..0c744f41a 100644 --- a/charon/src/ast/meta.rs +++ b/charon/src/ast/meta.rs @@ -136,7 +136,7 @@ pub struct RawAttribute { } /// Information about the attributes and visibility of an item, field or variant.. -#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] +#[derive(Debug, Default, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct AttrInfo { /// Attributes (`#[...]`). pub attributes: Vec, diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index a0fa754bb..97cc8abfd 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -130,7 +130,7 @@ pub enum TraitRefKind { /// FnOnce`. parent_trait_refs: Vector, /// The values of the associated types for this trait. - types: Vec<(TraitItemName, Ty)>, + types: Vec<(TraitItemName, Ty, Vector)>, }, /// The automatically-generated implementation for `dyn Trait`. diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 203f8cadb..1bfb6a9e4 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -656,6 +656,27 @@ impl TypeDeclRef { } } +impl TraitRef { + pub fn new_builtin( + trait_id: TraitDeclId, + ty: Ty, + parents: Vector, + ) -> Self { + let trait_decl_ref = RegionBinder::empty(TraitDeclRef { + id: trait_id, + generics: Box::new(GenericArgs::new_types([ty].into())), + }); + TraitRef { + kind: TraitRefKind::BuiltinOrAuto { + trait_decl_ref: trait_decl_ref.clone(), + parent_trait_refs: parents, + types: Default::default(), + }, + trait_decl_ref, + } + } +} + impl Field { /// The new name for this field, as suggested by the `#[charon::rename]` attribute. pub fn renamed_name(&self) -> Option<&str> { diff --git a/charon/src/ast/ullbc_ast.rs b/charon/src/ast/ullbc_ast.rs index 96a812b48..9af04316f 100644 --- a/charon/src/ast/ullbc_ast.rs +++ b/charon/src/ast/ullbc_ast.rs @@ -36,7 +36,7 @@ pub enum RawStatement { /// is implicitly deallocated at the end of the function. StorageDead(LocalId), Deinit(Place), - Drop(Place), + Drop(Place, TraitRef), /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check. Assert(Assert), diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 120de9899..308ce2db1 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -55,6 +55,7 @@ use indexmap::IndexMap; for Box, for Option, for (A, B), + for (A, B, C), for Result, for OutlivesPred, for Vec, @@ -143,6 +144,7 @@ impl AstVisitable for IndexMap { AbortKind, BinOp, BorrowKind, ConstantExpr, ConstGeneric, FieldId, FieldProjKind, TypeDeclRef, FunDeclId, FunIdOrTraitMethodRef, GenericArgs, GlobalDeclRef, IntegerTy, NullOp, RefKind, ScalarValue, Span, Ty, TypeDeclId, TypeId, UnOp, VariantId, LocalId, + TraitRef, ), // Types that we unconditionally explore. drive( @@ -155,6 +157,7 @@ impl AstVisitable for IndexMap { for Option, for Result, for (A, B), + for (A, B, C), for Vec, for Vector, ), diff --git a/charon/src/bin/charon-driver/translate/mod.rs b/charon/src/bin/charon-driver/translate/mod.rs index 6ea8021e0..57b4afd84 100644 --- a/charon/src/bin/charon-driver/translate/mod.rs +++ b/charon/src/bin/charon-driver/translate/mod.rs @@ -5,6 +5,7 @@ pub mod translate_closures; pub mod translate_constants; pub mod translate_crate; pub mod translate_ctx; +pub mod translate_drops; pub mod translate_functions; pub mod translate_generics; pub mod translate_items; diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 790bbb0fe..b3540521c 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -814,12 +814,14 @@ impl BodyTransCtx<'_, '_, '_> { TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior), TerminatorKind::Drop { place, + impl_expr, target, unwind: _, // We consider that panic is an error, and don't model unwinding .. } => { let place = self.translate_place(span, place)?; - statements.push(Statement::new(span, RawStatement::Drop(place))); + let tref = self.translate_trait_impl_expr(span, impl_expr)?; + statements.push(Statement::new(span, RawStatement::Drop(place, tref))); let target = self.translate_basic_block_id(*target); RawTerminator::Goto { target } } diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index e267661a9..3a02de2fa 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -632,32 +632,35 @@ impl ItemTransCtx<'_, '_> { let input = Ty::mk_tuple(inputs); let parent_trait_refs = { - // Makes a built-in trait ref for `ty: trait`. - let builtin_tref = |trait_id, ty| { - let generics = Box::new(GenericArgs::new_types([ty].into())); - let trait_decl_ref = TraitDeclRef { - id: trait_id, - generics, - }; - let trait_decl_ref = RegionBinder::empty(trait_decl_ref); - TraitRef { - kind: TraitRefKind::BuiltinOrAuto { - trait_decl_ref: trait_decl_ref.clone(), - parent_trait_refs: Vector::new(), - types: vec![], - }, - trait_decl_ref, - } - }; - + let input_is_meta_sized = + TraitRef::new_builtin(meta_sized_trait, input.clone(), Default::default()); + let input_is_sized = TraitRef::new_builtin( + sized_trait, + input.clone(), + [input_is_meta_sized.clone()].into(), + ); + let input_is_tuple = TraitRef::new_builtin( + tuple_trait, + input.clone(), + [input_is_meta_sized.clone()].into(), + ); match target_kind { - ClosureKind::FnOnce => [ - builtin_tref(meta_sized_trait, input.clone()), - builtin_tref(sized_trait, input.clone()), - builtin_tref(tuple_trait, input.clone()), - builtin_tref(sized_trait, output.clone()), - ] - .into(), + ClosureKind::FnOnce => { + let output_is_meta_sized = + TraitRef::new_builtin(meta_sized_trait, output.clone(), Default::default()); + let output_is_sized = TraitRef::new_builtin( + sized_trait, + output.clone(), + [output_is_meta_sized].into(), + ); + [ + input_is_meta_sized, + input_is_sized, + input_is_tuple, + output_is_sized, + ] + .into() + } ClosureKind::FnMut | ClosureKind::Fn => { let parent_kind = match target_kind { ClosureKind::FnOnce => unreachable!(), @@ -673,10 +676,10 @@ impl ItemTransCtx<'_, '_> { trait_decl_ref: RegionBinder::empty(parent_predicate), }; [ - builtin_tref(meta_sized_trait, input.clone()), + input_is_meta_sized, parent_trait_ref, - builtin_tref(sized_trait, input.clone()), - builtin_tref(tuple_trait, input.clone()), + input_is_sized, + input_is_tuple, ] .into() } diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 49925b6da..b295c6eb8 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -51,6 +51,10 @@ pub enum TransItemSourceKind { ClosureMethod(ClosureKind), /// A cast of a state-less closure as a function pointer. ClosureAsFnCast, + /// A fictitious trait impl corresponding to the drop glue code for the given ADT. + DropGlueImpl, + /// The `drop` method for the impl above. + DropGlueMethod, } impl TransItemSource { @@ -62,6 +66,17 @@ impl TransItemSource { &self.def_id } + /// Whether this item is the "main" item for this def_id or not (e.g. drop impl/methods are not + /// the main item). + pub(crate) fn is_derived_item(&self) -> bool { + use TransItemSourceKind::*; + match self.kind { + Global | TraitDecl | TraitImpl | InherentImpl | Module | Fun | Type => false, + ClosureTraitImpl(..) | ClosureMethod(..) | ClosureAsFnCast | DropGlueImpl + | DropGlueMethod => true, + } + } + /// Value with which we order values. fn sort_key(&self) -> impl Ord + '_ { (self.def_id.index, &self.kind) @@ -141,34 +156,25 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let item_id = match self.id_map.get(src) { Some(tid) => *tid, None => { + use TransItemSourceKind::*; let trans_id = match src.kind { - TransItemSourceKind::Type => { - AnyTransId::Type(self.translated.type_decls.reserve_slot()) - } - TransItemSourceKind::TraitDecl => { - AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()) - } - TransItemSourceKind::TraitImpl | TransItemSourceKind::ClosureTraitImpl(..) => { + Type => AnyTransId::Type(self.translated.type_decls.reserve_slot()), + TraitDecl => AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()), + TraitImpl | ClosureTraitImpl(..) | DropGlueImpl => { AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot()) } - TransItemSourceKind::Global => { - AnyTransId::Global(self.translated.global_decls.reserve_slot()) - } - TransItemSourceKind::Fun - | TransItemSourceKind::ClosureMethod(..) - | TransItemSourceKind::ClosureAsFnCast => { + Global => AnyTransId::Global(self.translated.global_decls.reserve_slot()), + Fun | ClosureMethod(..) | ClosureAsFnCast | DropGlueMethod => { AnyTransId::Fun(self.translated.fun_decls.reserve_slot()) } - TransItemSourceKind::InherentImpl | TransItemSourceKind::Module => { - return None; - } + InherentImpl | Module => return None, }; // Add the id to the queue of declarations to translate self.id_map.insert(src.clone(), trans_id); self.reverse_id_map.insert(trans_id, src.clone()); // Store the name early so the name matcher can identify paths. We can't to it for // trait impls because they register themselves when computing their name. - if !matches!(src.kind, TransItemSourceKind::TraitImpl) { + if !matches!(src.kind, TraitImpl) { if let Ok(name) = self.def_id_to_name(src.as_def_id()) { self.translated.item_names.insert(trans_id, name); } @@ -302,6 +308,30 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { .as_global() .unwrap() } + + pub(crate) fn register_drop_trait_impl_id( + &mut self, + src: &Option, + def_id: &hax::DefId, + ) -> TraitImplId { + *self + .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueImpl) + .unwrap() + .as_trait_impl() + .unwrap() + } + + pub(crate) fn register_drop_method_id( + &mut self, + src: &Option, + def_id: &hax::DefId, + ) -> FunDeclId { + *self + .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueMethod) + .unwrap() + .as_fun() + .unwrap() + } } // Id and item reference registration. @@ -506,6 +536,33 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { let src = self.make_dep_source(span); self.t_ctx.register_closure_as_fun_decl_id(&src, id) } + + pub(crate) fn register_drop_trait_impl_id( + &mut self, + span: Span, + id: &hax::DefId, + ) -> TraitImplId { + let src = self.make_dep_source(span); + self.t_ctx.register_drop_trait_impl_id(&src, id) + } + + pub(crate) fn translate_drop_trait_impl_ref( + &mut self, + span: Span, + item: &hax::ItemRef, + ) -> Result { + let id = self.register_drop_trait_impl_id(span, &item.def_id); + let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?; + Ok(TraitImplRef { + id, + generics: Box::new(generics), + }) + } + + pub(crate) fn register_drop_method_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId { + let src = self.make_dep_source(span); + self.t_ctx.register_drop_method_id(&src, id) + } } #[tracing::instrument(skip(tcx))] @@ -518,7 +575,7 @@ pub fn translate<'tcx, 'ctx>( tcx, hax::options::Options { inline_anon_consts: true, - resolve_drop_bounds: false, + resolve_drop_bounds: options.add_drop_bounds, }, ); diff --git a/charon/src/bin/charon-driver/translate/translate_drops.rs b/charon/src/bin/charon-driver/translate/translate_drops.rs new file mode 100644 index 000000000..901f0d0e5 --- /dev/null +++ b/charon/src/bin/charon-driver/translate/translate_drops.rs @@ -0,0 +1,186 @@ +use crate::translate::translate_bodies::BodyTransCtx; + +use super::translate_ctx::*; +use charon_lib::ast::*; +use hax_frontend_exporter as hax; + +impl ItemTransCtx<'_, '_> { + fn translate_drop_method_body( + &mut self, + span: Span, + def: &hax::FullDef, + ) -> Result, Error> { + let (hax::FullDefKind::Struct { drop_glue, .. } + | hax::FullDefKind::Enum { drop_glue, .. } + | hax::FullDefKind::Union { drop_glue, .. } + | hax::FullDefKind::Closure { drop_glue, .. }) = def.kind() + else { + panic!("Unexpected def adt: {def:?}") + }; + let Some(body) = drop_glue else { + return Ok(Err(Opaque)); + }; + + let mut bt_ctx = BodyTransCtx::new(self); + Ok(match bt_ctx.translate_body(span, body, &def.source_text) { + Ok(Ok(body)) => Ok(body), + Ok(Err(Opaque)) => Err(Opaque), + Err(_) => Err(Opaque), + }) + } + + /// Construct the `Ty` corresponding to the current adt. The generics must be the generics for + /// that def_id. + fn adt_self_ty(&mut self, span: Span, def_id: &hax::DefId) -> Result { + // The def_id must correspond to a type definition. + let self_decl_id = self.register_type_decl_id(span, def_id); + let self_ty = TyKind::Adt(TypeDeclRef { + id: TypeId::Adt(self_decl_id), + generics: Box::new(self.the_only_binder().params.identity_args()), + }) + .into_ty(); + Ok(self_ty) + } + + fn adt_drop_predicate( + &mut self, + span: Span, + def_id: &hax::DefId, + ) -> Result { + let drop_trait = self.get_lang_item(rustc_hir::LangItem::Drop); + let drop_trait = self.register_trait_decl_id(span, &drop_trait); + + let self_ty = self.adt_self_ty(span, def_id)?; + let implemented_trait = TraitDeclRef { + id: drop_trait, + generics: Box::new(GenericArgs::new_types([self_ty.clone()].into())), + }; + Ok(implemented_trait) + } + + /// Given an item that is a closure, generate the `call_once`/`call_mut`/`call` method + /// (depending on `target_kind`). + #[tracing::instrument(skip(self, item_meta))] + pub fn translate_drop_method( + mut self, + def_id: FunDeclId, + item_meta: ItemMeta, + def: &hax::FullDef, + ) -> Result { + let span = item_meta.span; + let drop_impl_id = self.register_drop_trait_impl_id(span, def.def_id()); + + self.translate_def_generics(span, def)?; + + let implemented_trait = self.adt_drop_predicate(span, def.def_id())?; + let self_ty = implemented_trait.generics.types[0].clone(); + let impl_ref = TraitImplRef { + id: drop_impl_id, + generics: Box::new(self.the_only_binder().params.identity_args()), + }; + + let kind = ItemKind::TraitImpl { + impl_ref, + trait_ref: implemented_trait, + item_name: TraitItemName("drop".to_owned()), + reuses_default: false, + }; + + // Add the method lifetime generic. + assert!(self.innermost_binder_mut().bound_region_vars.is_empty()); + let region_id = self + .innermost_binder_mut() + .push_bound_region(hax::BoundRegionKind::Anon); + + let body = if item_meta.opacity.with_private_contents().is_opaque() { + Err(Opaque) + } else { + self.translate_drop_method_body(span, def)? + }; + + let input = TyKind::Ref( + Region::Var(DeBruijnVar::new_at_zero(region_id)), + self_ty, + RefKind::Mut, + ) + .into_ty(); + let signature = FunSig { + generics: self.into_generics(), + is_unsafe: false, + inputs: vec![input], + output: Ty::mk_unit(), + }; + + Ok(FunDecl { + def_id, + item_meta, + signature, + kind, + is_global_initializer: None, + body, + }) + } + + #[tracing::instrument(skip(self, item_meta))] + pub fn translate_drop_impl( + mut self, + impl_id: TraitImplId, + item_meta: ItemMeta, + def: &hax::FullDef, + ) -> Result { + let span = item_meta.span; + + self.translate_def_generics(span, def)?; + + let implemented_trait = self.adt_drop_predicate(span, def.def_id())?; + let drop_trait = implemented_trait.id; + + // Construct the method reference. + let method_id = self.register_drop_method_id(span, &def.def_id); + let method_name = TraitItemName("drop".to_owned()); + let method_binder = { + let mut method_params = GenericParams::empty(); + method_params + .regions + .push_with(|index| RegionVar { index, name: None }); + + let generics = self + .outermost_binder() + .params + .identity_args_at_depth(DeBruijnId::one()) + .concat(&method_params.identity_args_at_depth(DeBruijnId::zero())); + Binder::new( + BinderKind::TraitMethod(drop_trait, method_name.clone()), + method_params, + FunDeclRef { + id: method_id, + generics: Box::new(generics), + }, + ) + }; + + let parent_trait_refs = { + let meta_sized_trait = self.get_lang_item(rustc_hir::LangItem::MetaSized); + let meta_sized_trait = self.register_trait_decl_id(span, &meta_sized_trait); + let self_ty = implemented_trait.generics.types[0].clone(); + [TraitRef::new_builtin( + meta_sized_trait, + self_ty, + Default::default(), + )] + .into() + }; + + Ok(TraitImpl { + def_id: impl_id, + item_meta, + impl_trait: implemented_trait, + generics: self.into_generics(), + methods: vec![(method_name, method_binder)], + parent_trait_refs, + type_clauses: Default::default(), + consts: Default::default(), + types: Default::default(), + }) + } +} diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 0a1201503..55898b130 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -121,6 +121,20 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let fun_decl = bt_ctx.translate_stateless_closure_as_fn(id, item_meta, &def)?; self.translated.fun_decls.set_slot(id, fun_decl); } + TransItemSourceKind::DropGlueImpl => { + let Some(AnyTransId::TraitImpl(id)) = trans_id else { + unreachable!() + }; + let timpl = bt_ctx.translate_drop_impl(id, item_meta, &def)?; + self.translated.trait_impls.set_slot(id, timpl); + } + TransItemSourceKind::DropGlueMethod => { + let Some(AnyTransId::Fun(id)) = trans_id else { + unreachable!() + }; + let fun_decl = bt_ctx.translate_drop_method(id, item_meta, &def)?; + self.translated.fun_decls.set_slot(id, fun_decl); + } } Ok(()) } diff --git a/charon/src/bin/charon-driver/translate/translate_meta.rs b/charon/src/bin/charon-driver/translate/translate_meta.rs index 0e3839bea..2416274ee 100644 --- a/charon/src/bin/charon-driver/translate/translate_meta.rs +++ b/charon/src/bin/charon-driver/translate/translate_meta.rs @@ -308,16 +308,36 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let def_id = src.as_def_id(); let mut name = self.def_id_to_name(def_id)?; match src.kind { - TransItemSourceKind::ClosureTraitImpl(kind) - | TransItemSourceKind::ClosureMethod(kind) => { - let _ = name.name.pop(); // Pop the `{closure}` path item - let impl_id = self.register_closure_trait_impl_id(&None, def_id, kind); + TransItemSourceKind::ClosureTraitImpl(..) + | TransItemSourceKind::ClosureMethod(..) + | TransItemSourceKind::DropGlueImpl + | TransItemSourceKind::DropGlueMethod => { + let impl_id = match src.kind { + TransItemSourceKind::ClosureTraitImpl(kind) + | TransItemSourceKind::ClosureMethod(kind) => { + let _ = name.name.pop(); // Pop the `{closure}` + self.register_closure_trait_impl_id(&None, def_id, kind) + } + TransItemSourceKind::DropGlueImpl | TransItemSourceKind::DropGlueMethod => { + self.register_drop_trait_impl_id(&None, def_id) + } + _ => unreachable!(), + }; + name.name.push(PathElem::Impl(ImplElem::Trait(impl_id))); - if matches!(src.kind, TransItemSourceKind::ClosureMethod(..)) { - let fn_name = kind.method_name().to_string(); - name.name - .push(PathElem::Ident(fn_name, Disambiguator::ZERO)); + match src.kind { + TransItemSourceKind::ClosureMethod(kind) => { + let fn_name = kind.method_name().to_string(); + name.name + .push(PathElem::Ident(fn_name, Disambiguator::ZERO)); + } + TransItemSourceKind::DropGlueMethod => { + let fn_name = "drop".to_string(); + name.name + .push(PathElem::Ident(fn_name, Disambiguator::ZERO)); + } + _ => {} } } TransItemSourceKind::TraitImpl if matches!(def_id.kind, hax::DefKind::TraitAlias) => { @@ -470,12 +490,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { } let span = def.source_span.as_ref().unwrap_or(&def.span); let span = self.translate_span_from_hax(span); - let attr_info = self.translate_attr_info(def); let is_local = def.def_id.is_local; - let lang_item = def - .lang_item - .clone() - .or_else(|| def.diagnostic_item.clone()); + let (attr_info, lang_item) = if item_src.is_derived_item() { + (AttrInfo::default(), None) + } else { + let attr_info = self.translate_attr_info(def); + let lang_item = def + .lang_item + .clone() + .or_else(|| def.diagnostic_item.clone()); + (attr_info, lang_item) + }; let opacity = if self.is_extern_item(def) || attr_info.attributes.iter().any(|attr| attr.is_opaque()) diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 87c054471..3196e3b96 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -189,6 +189,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { trait_decl_ref: PolyTraitDeclRef, ) -> Result { trace!("impl_expr: {:#?}", impl_source); + use hax::DropData; use hax::ImplExprAtom; let trait_ref = match &impl_source.r#impl { @@ -336,10 +337,11 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { let parent_trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?; let types = types .iter() - .map(|(def_id, ty)| { + .map(|(def_id, ty, impl_exprs)| { let name = self.t_ctx.translate_trait_item_name(def_id)?; let ty = self.translate_ty(span, ty)?; - Ok((name, ty)) + let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?; + Ok((name, ty, trait_refs)) }) .try_collect()?; TraitRefKind::BuiltinOrAuto { @@ -353,6 +355,33 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { trait_decl_ref, } } + ImplExprAtom::Drop(DropData::Glue { ty, .. }) + if let hax::TyKind::Adt(item) = ty.kind() => + { + let impl_ref = self.translate_drop_trait_impl_ref(span, item)?; + TraitRef { + kind: TraitRefKind::TraitImpl(impl_ref), + trait_decl_ref, + } + } + ImplExprAtom::Drop(..) => { + let meta_sized_trait = self.get_lang_item(rustc_hir::LangItem::MetaSized); + let meta_sized_trait = self.register_trait_decl_id(span, &meta_sized_trait); + let self_ty = trait_decl_ref.clone().erase().generics.types[0].clone(); + TraitRef { + kind: TraitRefKind::BuiltinOrAuto { + trait_decl_ref: trait_decl_ref.clone(), + parent_trait_refs: [TraitRef::new_builtin( + meta_sized_trait, + self_ty, + Default::default(), + )] + .into(), + types: vec![], + }, + trait_decl_ref, + } + } ImplExprAtom::Error(msg) => { let trait_ref = TraitRef { kind: TraitRefKind::Unknown(msg.clone()), @@ -363,9 +392,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { } trait_ref } - ImplExprAtom::Drop(..) => { - raise_error!(self, span, "Unsupported predicate: drop glue") - } }; Ok(trait_ref) } diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index fa584d65d..62e006ecc 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -64,7 +64,21 @@ impl Pattern { name: &Name, args: Option<&GenericArgs>, ) -> bool { - let zipped = self.elems.iter().zip_longest(&name.name).collect_vec(); + let mut scrutinee_elems = name.name.as_slice(); + // Patterns that start with an impl block match that impl block anywhere. In such a case we + // truncate the scrutinee name to start with the rightmost impl in its name. This isn't + // fully precise in case of impls within impls, but we'll ignore that. + if let Some(PatElem::Impl(_)) = self.elems.first() { + if let Some((i, _)) = scrutinee_elems + .iter() + .enumerate() + .rfind(|(_, elem)| elem.is_impl()) + { + scrutinee_elems = &scrutinee_elems[i..]; + } + } + + let zipped = self.elems.iter().zip_longest(scrutinee_elems).collect_vec(); let zipped_len = zipped.len(); for (i, x) in zipped.into_iter().enumerate() { let is_last = i + 1 == zipped_len; diff --git a/charon/src/options.rs b/charon/src/options.rs index 36dec9982..fc5765f17 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -155,6 +155,11 @@ pub struct CliOpts { #[clap(long)] #[serde(default)] pub remove_unused_self_clauses: bool, + /// Whether to add `Drop` bounds everywhere to enable proper tracking of what code runs on a + /// given `drop` call. + #[clap(long)] + #[serde(default)] + pub add_drop_bounds: bool, /// A list of item paths to use as starting points for the translation. We will translate these /// items and any items they refer to, according to the opacity rules. When absent, we start /// from the path `crate` (which translates the whole crate). @@ -280,6 +285,11 @@ impl CliOpts { self.remove_associated_types.push("*".to_owned()); self.hide_marker_traits = true; self.remove_unused_self_clauses = true; + // Hide drop impls because they often involve nested borrows. which aeneas + // doesn't handle yet. + self.exclude.push("core::ops::drop::Drop".to_owned()); + self.exclude + .push("{impl core::ops::drop::Drop for _}".to_owned()); } Preset::Eurydice => { self.remove_associated_types.push("*".to_owned()); @@ -472,6 +482,7 @@ impl TranslateOptions { /// Find the opacity requested for the given name. This does not take into account /// `#[charon::opaque]` annotations, only cli parameters. + #[tracing::instrument(skip(self, krate), ret)] pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity { // Find the most precise pattern that matches this name. There is always one since // the list contains the `_` pattern. If there are conflicting settings for this item, we diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 6dd109a55..9ad74dd7e 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1308,8 +1308,13 @@ impl FmtWithCtx for ullbc::Statement { RawStatement::Deinit(place) => { write!(f, "{tab}deinit({})", place.with_ctx(ctx)) } - RawStatement::Drop(place) => { - write!(f, "{tab}drop {}", place.with_ctx(ctx)) + RawStatement::Drop(place, tref) => { + write!( + f, + "{tab}drop[{}] {}", + tref.with_ctx(ctx), + place.with_ctx(ctx), + ) } RawStatement::Assert(assert) => write!(f, "{tab}{}", assert.with_ctx(ctx)), RawStatement::Nop => write!(f, "{tab}nop"), @@ -1352,8 +1357,8 @@ impl FmtWithCtx for llbc::Statement { RawStatement::Deinit(place) => { write!(f, "deinit({})", place.with_ctx(ctx)) } - RawStatement::Drop(place) => { - write!(f, "drop {}", place.with_ctx(ctx)) + RawStatement::Drop(place, tref) => { + write!(f, "drop[{}] {}", tref.with_ctx(ctx), place.with_ctx(ctx),) } RawStatement::Assert(assert) => { write!(f, "{}", assert.with_ctx(ctx),) @@ -1662,7 +1667,7 @@ impl FmtWithCtx for TraitRefKind { if !types.is_empty() { let types = types .iter() - .map(|(name, ty)| { + .map(|(name, ty, _)| { let ty = ty.with_ctx(ctx); format!("{name} = {ty}") }) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 48955e79f..63700515c 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -234,10 +234,64 @@ impl VisitAst for CheckGenericsVisitor<'_> { } } fn enter_trait_ref_kind(&mut self, x: &TraitRefKind) { - if let TraitRefKind::Clause(var) = x { - if self.binder_stack.get_var(*var).is_none() { - self.error(format!("Found incorrect clause var: {var}")); + match x { + TraitRefKind::Clause(var) => { + if self.binder_stack.get_var(*var).is_none() { + self.error(format!("Found incorrect clause var: {var}")); + } + } + TraitRefKind::BuiltinOrAuto { + trait_decl_ref, + parent_trait_refs, + types, + } => { + let trait_id = trait_decl_ref.skip_binder.id; + let target = GenericsSource::item(trait_id); + let Some(tdecl) = self.ctx.translated.trait_decls.get(trait_id) else { + return; + }; + if tdecl + .item_meta + .lang_item + .as_deref() + .is_some_and(|s| matches!(s, "pointee_trait" | "discriminant_kind")) + { + // These traits have builtin assoc types that we can't resolve. + return; + } + let fmt = &self.ctx.into_fmt(); + let args_fmt = &self.val_fmt_ctx(); + self.zip_assert_match( + &tdecl.parent_clauses, + parent_trait_refs, + fmt, + args_fmt, + "builtin trait parent clauses", + &target, + |tclause, tref| self.assert_clause_matches(&fmt, tclause, tref), + ); + let types_match = types.len() == tdecl.types.len() + && tdecl + .types + .iter() + .zip(types.iter()) + .all(|(dname, (iname, _, _))| dname == iname); + if !types_match { + let target = target.with_ctx(args_fmt); + let a = tdecl.types.iter().format(", "); + let b = types + .iter() + .map(|(_, ty, _)| ty.with_ctx(args_fmt)) + .format(", "); + self.error(format!( + "Mismatched types in builtin trait ref:\ + \ntarget: {target}\ + \nexpected: [{a}]\ + \n got: [{b}]" + )); + } } + _ => {} } } diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs index 05c00f793..2189b036e 100644 --- a/charon/src/transform/expand_associated_types.rs +++ b/charon/src/transform/expand_associated_types.rs @@ -858,7 +858,7 @@ impl<'a> ComputeItemModifications<'a> { types, .. } => { - for (name, ty) in types.iter().cloned() { + for (name, ty, _) in types.iter().cloned() { let path = TraitRefPath::self_ref().with_assoc_type(name); out.push((path, ty)); } @@ -982,8 +982,8 @@ impl UpdateItemBody<'_> { } => match path.pop_first_parent() { None => types .iter() - .find(|(name, _)| name == &path.type_name) - .map(|(_, ty)| ty.clone()), + .find(|(name, _, _)| name == &path.type_name) + .map(|(_, ty, _)| ty.clone()), Some((parent_clause_id, sub_path)) => { let parent_ref = &parent_trait_refs[parent_clause_id]; self.lookup_path_on_trait_ref(&sub_path, &parent_ref.kind) @@ -1133,12 +1133,22 @@ impl VisitAstMut for UpdateItemBody<'_> { // implemented trait info at each level. This would require hax to give us more info. let kind_clone = kind.clone(); match kind { + TraitRefKind::Dyn(tref) => { + self.process_poly_trait_decl_ref(tref, kind_clone); + } TraitRefKind::BuiltinOrAuto { trait_decl_ref: tref, + types, .. - } - | TraitRefKind::Dyn(tref) => { + } => { self.process_poly_trait_decl_ref(tref, kind_clone); + let target = GenericsSource::item(tref.skip_binder.id); + if let Some(decl_modifs) = self.item_modifications.get(&target) { + assert!(decl_modifs.required_extra_assoc_types().count() == 0); + if decl_modifs.add_type_params { + types.clear(); + } + } } _ => {} } diff --git a/charon/src/transform/hide_marker_traits.rs b/charon/src/transform/hide_marker_traits.rs index 7221727cf..05d7c8af3 100644 --- a/charon/src/transform/hide_marker_traits.rs +++ b/charon/src/transform/hide_marker_traits.rs @@ -11,21 +11,8 @@ struct RemoveMarkersVisitor { exclude: HashSet, } -// Remove clauses and trait refs that mention the offending traits. This relies on the fact that -// `Vector::remove` does not shift indices: it simply leaves an empty slot. -// FIXME: this is a footgun, it caused at least https://github.com/AeneasVerif/charon/issues/561. -impl VisitAstMut for RemoveMarkersVisitor { - fn enter_generic_params(&mut self, args: &mut GenericParams) { - let trait_clauses = &mut args.trait_clauses; - for i in trait_clauses.all_indices() { - let clause = &trait_clauses[i]; - if self.exclude.contains(&clause.trait_.skip_binder.id) { - trait_clauses.remove(i); - } - } - } - fn enter_generic_args(&mut self, args: &mut GenericArgs) { - let trait_refs = &mut args.trait_refs; +impl RemoveMarkersVisitor { + fn filter_trait_refs(&mut self, trait_refs: &mut Vector) { for i in trait_refs.all_indices() { let tref = &trait_refs[i]; if self.exclude.contains(&tref.trait_decl_ref.skip_binder.id) { @@ -33,8 +20,8 @@ impl VisitAstMut for RemoveMarkersVisitor { } } } - fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) { - let trait_clauses = &mut tdecl.parent_clauses; + + fn filter_trait_clauses(&mut self, trait_clauses: &mut Vector) { for i in trait_clauses.all_indices() { let clause = &trait_clauses[i]; if self.exclude.contains(&clause.trait_.skip_binder.id) { @@ -42,12 +29,34 @@ impl VisitAstMut for RemoveMarkersVisitor { } } } +} + +// Remove clauses and trait refs that mention the offending traits. This relies on the fact that +// `Vector::remove` does not shift indices: it simply leaves an empty slot. +// FIXME: this is a footgun, it caused at least https://github.com/AeneasVerif/charon/issues/561. +impl VisitAstMut for RemoveMarkersVisitor { + fn enter_generic_params(&mut self, args: &mut GenericParams) { + self.filter_trait_clauses(&mut args.trait_clauses); + } + fn enter_generic_args(&mut self, args: &mut GenericArgs) { + self.filter_trait_refs(&mut args.trait_refs); + } + fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) { + self.filter_trait_clauses(&mut tdecl.parent_clauses); + } fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) { - let trait_refs = &mut timpl.parent_trait_refs; - for i in trait_refs.all_indices() { - let tref = &trait_refs[i]; - if self.exclude.contains(&tref.trait_decl_ref.skip_binder.id) { - trait_refs.remove(i); + self.filter_trait_refs(&mut timpl.parent_trait_refs); + } + fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) { + if let TraitRefKind::BuiltinOrAuto { + parent_trait_refs, + types, + .. + } = x + { + self.filter_trait_refs(parent_trait_refs); + for (_, _, trait_refs) in types { + self.filter_trait_refs(trait_refs); } } } diff --git a/charon/src/transform/lift_associated_item_clauses.rs b/charon/src/transform/lift_associated_item_clauses.rs index bcc524591..d3efaa0b4 100644 --- a/charon/src/transform/lift_associated_item_clauses.rs +++ b/charon/src/transform/lift_associated_item_clauses.rs @@ -45,8 +45,8 @@ impl TransformPass for Transform { // Update trait refs. ctx.translated.dyn_visit_mut(|trkind: &mut TraitRefKind| { use TraitRefKind::*; - if let ItemClause(..) = trkind { - take_mut::take(trkind, |trkind| { + match trkind { + ItemClause(..) => take_mut::take(trkind, |trkind| { let ItemClause(trait_ref, trait_decl, item_name, item_clause_id) = trkind else { unreachable!() @@ -62,7 +62,21 @@ impl TransformPass for Transform { Some(new_id) => ParentClause(trait_ref, trait_decl, new_id), None => ItemClause(trait_ref, trait_decl, item_name, item_clause_id), } - }) + }), + BuiltinOrAuto { + parent_trait_refs, + types, + .. + } => { + for (_, _, ty_trait_refs) in types { + for tref in std::mem::take(ty_trait_refs) { + // Note: this assumes that we listed the types in the same order as in + // the trait decl, which we do. + parent_trait_refs.push(tref); + } + } + } + _ => {} } }); } diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs index aad6756b0..ddca052c2 100644 --- a/charon/src/transform/ullbc_to_llbc.rs +++ b/charon/src/transform/ullbc_to_llbc.rs @@ -1461,7 +1461,7 @@ fn translate_statement(st: &src::Statement) -> Option { src::RawStatement::StorageLive(var_id) => tgt::RawStatement::StorageLive(var_id), src::RawStatement::StorageDead(var_id) => tgt::RawStatement::StorageDead(var_id), src::RawStatement::Deinit(place) => tgt::RawStatement::Deinit(place), - src::RawStatement::Drop(place) => tgt::RawStatement::Drop(place), + src::RawStatement::Drop(place, tref) => tgt::RawStatement::Drop(place, tref), src::RawStatement::Assert(assert) => tgt::RawStatement::Assert(assert), src::RawStatement::Nop => tgt::RawStatement::Nop, src::RawStatement::Error(s) => tgt::RawStatement::Error(s), diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index a3acc3d19..e181127b5 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -71,6 +71,19 @@ where fn index_mut<'_0> = {impl IndexMut for Array}::index_mut<'_0_0, T, I, Clause2_Clause1_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + pub fn core::ops::index::Index::index<'_0, Self, Idx, Clause0_Output>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Clause0_Output) where [@TraitClause0]: Index, @@ -317,7 +330,7 @@ where storage_dead(@3) @0 := len<'_, T>[@TraitClause0](move (@2)) storage_dead(@2) - drop s@1 + drop[Drop>] s@1 return } diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index c09bead7a..197af4e32 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -69,6 +69,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -151,7 +164,7 @@ where } // Full name: test_crate::{impl test_crate::Foo<'a, Option<&'a (T)>[Sized<&'_ (T)>]> for &'a (T)}::use_item_required -fn {impl test_crate::Foo<'a, Option<&'a (T)>[Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>(@1: Option<&'_ (T)>[Sized<&'_ (T)>]) -> Option<&'_ (T)>[Sized<&'_ (T)>] +fn {impl test_crate::Foo<'a, Option<&'a (T)>[Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>(@1: Option<&'a (T)>[Sized<&'_ (T)>]) -> Option<&'a (T)>[Sized<&'_ (T)>] where [@TraitClause0]: Sized, { @@ -286,7 +299,7 @@ where let x@1: Clause2_Item; // arg #1 @0 := move (x@1) - drop x@1 + drop[Drop] x@1 return } @@ -410,8 +423,8 @@ where parent_clause3 : [@TraitClause3]: Sized } -// Full name: test_crate::params::{impl test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'_ (())))> for ()} -impl<'a, T> test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'_ (())))> for () +// Full name: test_crate::params::{impl test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'a (())))> for ()} +impl<'a, T> test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'a (())))> for () where [@TraitClause0]: Sized, T : 'a, diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out index 76d8b8a04..1cb479703 100644 --- a/charon/tests/ui/call-to-known-trait-method.out +++ b/charon/tests/ui/call-to-known-trait-method.out @@ -82,6 +82,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::string::String #[lang_item("String")] pub opaque type String @@ -106,7 +119,7 @@ where storage_live(@1) @1 := @TraitClause1::default() @0 := Struct { 0: move (@1) } - drop @1 + drop[Drop] @1 storage_dead(@1) return } diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index 47b3a7785..0477abb3a 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -109,7 +122,7 @@ fn {impl FnOnce<()> for closure}::call_once(@1: closure, @2: ()) storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 @0 := () return } diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index 84cfff92d..d0c5cdab8 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -77,6 +77,18 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::Fn #[lang_item("r#fn")] pub trait Fn @@ -110,6 +122,20 @@ where Some(T), } +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]}::drop +fn {impl Drop for Option[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (Option[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]} +impl Drop for Option[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for Option[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: test_crate::incr_u32 pub fn incr_u32(@1: u32) -> u32 { @@ -163,19 +189,19 @@ where @7 := move (x@3) @6 := (move (@7)) @4 := @TraitClause2::call<'_>(move (@5), move (@6)) - drop @7 + drop[Drop] @7 storage_dead(@7) storage_dead(@6) storage_dead(@5) @0 := Option::Some { 0: move (@4) } - drop @4 + drop[Drop] @4 storage_dead(@4) - drop x@3 + drop[Drop] x@3 storage_dead(x@3) }, } - drop f@2 - drop x@1 + drop[Drop] f@2 + drop[{impl Drop for Option[@TraitClause0]}[@TraitClause0]] x@1 return } @@ -212,7 +238,7 @@ where storage_dead(@6) storage_dead(@5) @0 := Option::Some { 0: move (@4) } - drop @4 + drop[Drop] @4 storage_dead(@4) storage_dead(x@3) return @@ -277,7 +303,7 @@ fn {impl FnOnce<(u32), u32> for test_crate::test_closure_u32::closure}::call_onc storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32), u32> for test_crate::test_closure_u32::closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -404,7 +430,7 @@ fn {impl FnOnce<(u32, u32), u32> for test_crate::test_closure_u32s::closure}::ca storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32, u32), u32> for test_crate::test_closure_u32s::closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -522,7 +548,7 @@ fn {impl FnOnce<(&'_ (u32)), &'_ (u32)> for test_crate::test_closure_ref_u32::cl storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (u32)), &'_ (u32)> for test_crate::test_closure_ref_u32::closure}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -648,7 +674,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (T)), &'_ (T)> for test_crate::test_closure_ref_param::closure[@TraitClause0]}::call_mut<'_0, '_, T>[@TraitClause0](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0]>] @1 return } @@ -797,7 +823,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (T)), &'_ (T)> for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}::call_mut<'_, '_1, '_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 return } @@ -939,7 +965,7 @@ fn {impl FnOnce<(u32), u32> for test_crate::test_map_option2::closure}::call_onc storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32), u32> for test_crate::test_map_option2::closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -1020,7 +1046,7 @@ where let x@1: T; // arg #1 @0 := move (x@1) - drop x@1 + drop[Drop] x@1 return } @@ -1074,7 +1100,7 @@ where @2 := &x@1 @0 := @TraitClause1::clone<'_>(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop] x@1 return } @@ -1122,7 +1148,7 @@ where storage_dead(@4) storage_dead(@3) storage_dead(f@2) - drop x@1 + drop[Drop] x@1 return } @@ -1188,7 +1214,7 @@ fn {impl FnOnce<(u32), u32> for test_crate::test_map_option3::closure}::call_onc storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32), u32> for test_crate::test_map_option3::closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -1308,7 +1334,7 @@ fn {impl FnOnce<(&'_ (&'_ (u32))), u32> for test_crate::test_regions::closure}:: storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions::closure}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -1380,7 +1406,7 @@ fn {impl FnOnce<(&'_ (&'_ (u32))), u32> for test_crate::test_regions_casted::clo storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions_casted::closure}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -1557,7 +1583,7 @@ fn {impl FnOnce<(u32), u32> for test_crate::test_closure_capture::closure<'_0, ' storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32), u32> for test_crate::test_closure_capture::closure<'_0, '_1>}::call_mut<'_0, '_1, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 return } @@ -1612,7 +1638,7 @@ where @4 := &x@3 @0 := @TraitClause1::clone<'_>(move (@4)) storage_dead(@4) - drop x@3 + drop[Drop] x@3 return } @@ -1641,13 +1667,13 @@ where @6 := move (x@1) @5 := (move (@6)) @0 := {impl Fn<(T), T> for test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]}::call<'_, T>[@TraitClause0, @TraitClause1](move (@3), move (@5)) - drop @6 + drop[Drop] @6 storage_dead(@6) storage_dead(@5) storage_dead(@3) storage_dead(f@2) storage_dead(@4) - drop x@1 + drop[Drop] x@1 return } @@ -1682,7 +1708,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(T), T> for test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]}::call_mut<'_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 return } @@ -1752,7 +1778,7 @@ fn {impl FnOnce<(i32), i32> for test_crate::test_array_map::closure}::call_once( storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(i32), i32> for test_crate::test_array_map::closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } @@ -1876,7 +1902,7 @@ fn {impl FnOnce<(&'_ (usize)), ()> for test_crate::test_fnmut_with_ref::closure< storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (usize)), ()> for test_crate::test_fnmut_with_ref::closure<'_0>}::call_mut<'_0, '_1, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 @0 := () return } diff --git a/charon/tests/ui/closures_with_where.out b/charon/tests/ui/closures_with_where.out index 05af07a4e..15b92abb1 100644 --- a/charon/tests/ui/closures_with_where.out +++ b/charon/tests/ui/closures_with_where.out @@ -49,6 +49,19 @@ where [@TraitClause2]: FnMut, @TraitClause2::parent_clause1::Output = T, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output where [@TraitClause0]: FnMut, @@ -111,7 +124,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(usize)> for closure[@TraitClause0, @TraitClause1]}::call_mut<'_, T, const K : usize>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 return } diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index 5767ae6f2..dc2d54431 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -39,6 +39,19 @@ pub opaque type Arguments<'a> where 'a : 'a, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -289,7 +302,7 @@ where let @1: T; // arg #1 @0 := () - drop @1 + drop[Drop] @1 @0 := () return } diff --git a/charon/tests/ui/constants.out b/charon/tests/ui/constants.out index 1e911061f..168f65406 100644 --- a/charon/tests/ui/constants.out +++ b/charon/tests/ui/constants.out @@ -15,6 +15,19 @@ pub fn core::num::{u32}::MAX() -> u32 pub const core::num::{u32}::MAX: u32 = core::num::{u32}::MAX() +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + pub fn test_crate::X0() -> u32 { let @0: u32; // return @@ -187,9 +200,9 @@ where storage_live(@2) @2 := move (value@1) @0 := Wrap { value: move (@2) } - drop @2 + drop[Drop] @2 storage_dead(@2) - drop value@1 + drop[Drop] value@1 return } diff --git a/charon/tests/ui/dictionary_passing_style_woes.out b/charon/tests/ui/dictionary_passing_style_woes.out index d06ed9df5..81143599a 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.out +++ b/charon/tests/ui/dictionary_passing_style_woes.out @@ -40,6 +40,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::Iterator trait Iterator { @@ -78,7 +91,7 @@ where let t@1: Clause1_Item; // arg #1 @0 := move (t@1) - drop t@1 + drop[Drop] t@1 return } @@ -97,7 +110,7 @@ where @2 := move (t@1) @0 := callee[@TraitClause0, @TraitClause1](move (@2)) storage_dead(@2) - drop t@1 + drop[Drop] t@1 return } @@ -142,7 +155,7 @@ where @2 := &x@1 @0 := @TraitClause1::parent_clause1::method<'_>(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop] x@1 return } @@ -160,7 +173,7 @@ where @2 := &x@1 @0 := @TraitClause1::parent_clause1::method<'_>(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop] x@1 return } @@ -190,9 +203,9 @@ where @4 := b[@TraitClause0, @TraitClause2](move (@5)) storage_dead(@5) @0 := (move (@2), move (@4)) - drop @4 + drop[Drop] @4 storage_dead(@4) - drop @2 + drop[Drop] @2 storage_dead(@2) return } diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 3e191268b..7ad01ec12 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -148,6 +148,18 @@ where [@TraitClause0]: Sized, [@TraitClause1]: ZeroablePrimitive, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::{Option[@TraitClause0]}::unwrap #[lang_item("option_unwrap")] pub fn unwrap(@1: Option[@TraitClause0]) -> T @@ -176,6 +188,22 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]} +impl Drop for Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + pub fn test_crate::swap<'a, T>(@1: &'a mut (T), @2: &'a mut (T)) where [@TraitClause0]: Sized, @@ -232,7 +260,7 @@ pub fn test_vec_push() storage_dead(@3) storage_dead(@2) @0 := () - drop v@1 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] v@1 storage_dead(v@1) @0 := () return diff --git a/charon/tests/ui/generic-associated-types.out b/charon/tests/ui/generic-associated-types.out index 17d6c2971..98437cd56 100644 --- a/charon/tests/ui/generic-associated-types.out +++ b/charon/tests/ui/generic-associated-types.out @@ -34,6 +34,78 @@ error: Error during trait resolution: Found unsupported GAT `Item` when resolvin 29 | while let Some(item) = iter.next() { | ^^^^^^^^^^^ +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + +error: Error during trait resolution: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` + --> tests/ui/generic-associated-types.rs:31:5 + | +31 | } + | ^ + error: Generic associated types are not supported --> tests/ui/generic-associated-types.rs:48:9 | @@ -58,4 +130,4 @@ error: Error during trait resolution: Found unsupported GAT `Type` when resolvin 55 | x.foo() | ^^^^^^^ -ERROR Charon failed to translate this code (10 errors) +ERROR Charon failed to translate this code (22 errors) diff --git a/charon/tests/ui/hide-marker-traits.out b/charon/tests/ui/hide-marker-traits.out index afd99ed63..fbffef4ad 100644 --- a/charon/tests/ui/hide-marker-traits.out +++ b/charon/tests/ui/hide-marker-traits.out @@ -1,5 +1,17 @@ # Final LLBC before serialization: +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::Idx trait Idx @@ -19,5 +31,17 @@ where vector: IndexVec[@TraitClause1], } +// Full name: test_crate::foo +fn foo(@1: T) +{ + let @0: (); // return + let _x@1: T; // arg #1 + + @0 := () + drop[Drop] _x@1 + @0 := () + return +} + diff --git a/charon/tests/ui/hide-marker-traits.rs b/charon/tests/ui/hide-marker-traits.rs index 251770086..ca496ecba 100644 --- a/charon/tests/ui/hide-marker-traits.rs +++ b/charon/tests/ui/hide-marker-traits.rs @@ -15,3 +15,7 @@ where { vector: IndexVec, } + +// Makes a `TraitRef::Builtin` for `Drop`. Regression test: we used to not remove marker traits +// from that. +fn foo(_x: T) {} diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out index b660929b1..90c80c73c 100644 --- a/charon/tests/ui/impl-trait.out +++ b/charon/tests/ui/impl-trait.out @@ -57,6 +57,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -146,11 +159,11 @@ fn use_foo() storage_dead(@5) @2 := {impl Clone for u32}::clone<'_>(move (@3)) storage_dead(@3) - drop @2 + drop[Drop] @2 storage_dead(@4) storage_dead(@2) @0 := () - drop foo@1 + drop[Drop<()>] foo@1 storage_dead(foo@1) @0 := () return @@ -166,12 +179,13 @@ pub trait RPITIT fn make_foo = test_crate::RPITIT::make_foo[Self] } -pub fn test_crate::RPITIT::make_foo() -> @TraitClause0:: +pub fn test_crate::RPITIT::make_foo() where [@TraitClause0]: RPITIT, { let @0: (); // return + @0 := () @0 := () return } @@ -220,11 +234,11 @@ where storage_dead(@5) @2 := @TraitClause1::parent_clause2::parent_clause2::clone<'_>(move (@3)) storage_dead(@3) - drop @2 + drop[Drop<@TraitClause1::parent_clause2::Type>] @2 storage_dead(@4) storage_dead(@2) @0 := () - drop foo@1 + drop[Drop<@TraitClause1::>] foo@1 storage_dead(foo@1) @0 := () return @@ -314,7 +328,7 @@ pub fn use_wrap() @6 := &@7 @5 := &*(@6) @4 := (move (@5)) - @2 := FnOnce[Sized], (&'_ (u32))> where Output = WrapClone<&'_ (u32)>[Sized<&'_ (u32)>, {impl Clone for &'_0 (T)}<'_, u32>]::call_once(move (@3), move (@4)) + @2 := {impl FnOnce<(&'_ (U))> for closure[@TraitClause0]}::call_once<'_, u32>[Sized](move (@3), move (@4)) storage_dead(@5) storage_dead(@4) storage_dead(@3) @@ -322,7 +336,7 @@ pub fn use_wrap() storage_dead(@6) storage_dead(@2) @0 := () - drop f@1 + drop[Drop[Sized]>] f@1 storage_dead(f@1) @0 := () return diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index db279bdd2..d6daa591f 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -21,6 +21,14 @@ where Some(T), } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + // Full name: core::bool::{bool}::then_some pub fn then_some(@1: bool, @2: T) -> Option[@TraitClause0] where @@ -35,7 +43,7 @@ where } else { @0 := Option::None { } - drop t@2 + drop[Drop] t@2 return } storage_live(@3) @@ -127,6 +135,22 @@ pub fn core::num::{usize}::MAX() -> usize pub const core::num::{usize}::MAX: usize = core::num::{usize}::MAX() +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) +{ + let @0: (); // return + let to_drop@1: *mut T; // arg #1 + + @0 := drop_in_place(move (to_drop@1)) + @0 := () + return +} + // Full name: core::ptr::non_null::NonNull #[lang_item("NonNull")] pub struct NonNull { @@ -175,6 +199,46 @@ where len: usize, } +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + let @0: (); // return + let self@1: &'_ mut (Vec[@TraitClause0, @TraitClause1]); // arg #1 + let @2: *mut Slice; // anonymous local + let data@3: *mut T; // local + let len@4: usize; // local + let @5: NonNull; // anonymous local + + storage_live(@2) + storage_live(data@3) + storage_live(@5) + @5 := copy (((((*(self@1)).buf).inner).ptr).pointer) + data@3 := transmute, *mut T>(copy (@5)) + storage_dead(@5) + storage_live(len@4) + len@4 := copy ((*(self@1)).len) + @2 := @PtrFromPartsMut<'_, Slice>(copy (data@3), copy (len@4)) + storage_dead(len@4) + storage_dead(data@3) + @0 := drop_in_place>(move (@2)) + storage_dead(@2) + @0 := () + return +} + +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]} +impl Drop for Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: issue_114_opaque_bodies_aux::inline_always pub fn inline_always() -> u32 { @@ -288,7 +352,7 @@ fn vec(@1: Vec[Sized, Sized]) let _x@1: Vec[Sized, Sized]; // arg #1 @0 := () - drop _x@1 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] _x@1 @0 := () return } @@ -315,7 +379,7 @@ where let _x@1: T; // arg #1 @0 := () - drop _x@1 + drop[Drop] _x@1 @0 := () return } diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out index 5b43b1c6c..adad255a7 100644 --- a/charon/tests/ui/issue-120-bare-discriminant-read.out +++ b/charon/tests/ui/issue-120-bare-discriminant-read.out @@ -11,6 +11,18 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -21,6 +33,20 @@ where Some(T), } +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]}::drop +fn {impl Drop for Option[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (Option[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]} +impl Drop for Option[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for Option[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: test_crate::discriminant_value fn discriminant_value<'_0, T>(@1: &'_0 (Option[@TraitClause0])) -> isize where @@ -65,7 +91,7 @@ where @0 := move (@2) != const (0 : isize) storage_dead(@2) storage_dead(@4) - drop opt@1 + drop[{impl Drop for Option[@TraitClause0]}[@TraitClause0]] opt@1 return } @@ -85,7 +111,7 @@ where @0 := const (1 : isize) }, } - drop opt@1 + drop[{impl Drop for Option[@TraitClause0]}[@TraitClause0]] opt@1 return } diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out index 2fd2f1805..b8deaec46 100644 --- a/charon/tests/ui/issue-165-vec-macro.out +++ b/charon/tests/ui/issue-165-vec-macro.out @@ -40,6 +40,18 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} @@ -48,6 +60,22 @@ pub struct Global {} #[lang_item("exchange_malloc")] unsafe fn exchange_malloc(@1: usize, @2: usize) -> *mut u8 +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: alloc::vec::Vec #[lang_item("Vec")] pub opaque type Vec @@ -69,6 +97,22 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Clone, +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]} +impl Drop for Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: test_crate::foo fn foo() { @@ -89,8 +133,8 @@ fn foo() @4 := @BoxNew>[MetaSized>, Sized](move (@6)) @3 := move (@4) @2 := unsize_cast>[MetaSized>, Sized], alloc::boxed::Box>[MetaSized>, Sized]>(move (@3)) - drop @3 - drop @4 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @3 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @4 storage_dead(@4) storage_dead(@3) _v@1 := into_vec[Sized, Sized](move (@2)) @@ -98,9 +142,9 @@ fn foo() storage_live(_v2@5) _v2@5 := from_elem[Sized, {impl Clone for i32}](const (1 : i32), const (10 : usize)) @0 := () - drop _v2@5 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] _v2@5 storage_dead(_v2@5) - drop _v@1 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] _v@1 storage_dead(_v@1) @0 := () return @@ -132,13 +176,13 @@ pub fn bar() storage_dead(@5) @3 := move (@4) @2 := unsize_cast>[MetaSized>, Sized], alloc::boxed::Box>[MetaSized>, Sized]>(move (@3)) - drop @3 - drop @4 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @3 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @4 storage_dead(@4) storage_dead(@3) @1 := into_vec[Sized, Sized](move (@2)) storage_dead(@2) - drop @1 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] @1 storage_dead(@1) @0 := () @0 := () diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out index 3180f393f..9f6de0eb9 100644 --- a/charon/tests/ui/issue-323-closure-borrow.out +++ b/charon/tests/ui/issue-323-closure-borrow.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -118,7 +131,7 @@ fn {impl FnOnce<()> for closure<'_0>}::call_once<'_0>(@1: closure<'_0>, @2: ()) storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 @0 := () return } diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index d3940ef5b..32a4df587 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -11,6 +11,18 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -30,6 +42,15 @@ where #[lang_item("String")] pub opaque type String +// Full name: alloc::string::String::{impl Drop for String}::drop +fn {impl Drop for String}::drop<'_0>(@1: &'_0 mut (String)) + +// Full name: alloc::string::String::{impl Drop for String} +impl Drop for String { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for String}::drop<'_0_0> +} + // Full name: alloc::string::{String}::new #[lang_item("string_new")] pub fn new() -> String @@ -49,6 +70,26 @@ struct test_crate::Foo { String, } +// Full name: test_crate::Foo::{impl Drop for test_crate::Foo}::drop +fn {impl Drop for test_crate::Foo}::drop<'_0>(@1: &'_0 mut (test_crate::Foo)) +{ + let @0: (); // return + let @1: *mut test_crate::Foo; // arg #1 + let @2: &'_ mut (test_crate::Foo); // anonymous local + + storage_live(@2) + @2 := &mut *(@1) + drop[{impl Drop for String}] (*(@2)).1 + @0 := () + return +} + +// Full name: test_crate::Foo::{impl Drop for test_crate::Foo} +impl Drop for test_crate::Foo { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for test_crate::Foo}::drop<'_0_0> +} + fn test_crate::Foo(@1: u32, @2: String) -> test_crate::Foo { let @0: test_crate::Foo; // return @@ -132,7 +173,7 @@ fn main() @9 := test_crate::Foo(const (42 : u32), move (@11)) storage_dead(@11) storage_dead(@10) - drop @9 + drop[{impl Drop for test_crate::Foo}] @9 storage_dead(@9) storage_live(f@12) f@12 := const (Variant<'_, i32>[Sized]) diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out index 4b293b547..965104561 100644 --- a/charon/tests/ui/issue-394-rpit-with-lifetime.out +++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out @@ -64,6 +64,19 @@ where [@TraitClause2]: FnMut, @TraitClause2::parent_clause1::Output = Option[@TraitClause0], +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output where [@TraitClause0]: FnMut, @@ -97,7 +110,7 @@ fn {impl FnOnce<()> for closure<'_>}::call_once<'a>(@1: closure<'_>, @2: ()) -> storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for closure<'_>}::call_mut<'_, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 return } diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 9b7db684e..389a28e61 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -417,6 +417,19 @@ where Break(B), } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output where [@TraitClause0]: FnMut, @@ -519,7 +532,7 @@ fn {impl FnOnce<(i32)> for closure}::call_once(@1: closure, @2: (i32)) -> i32 storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(i32)> for closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } 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 26df841b4..807c9481c 100644 --- a/charon/tests/ui/issue-70-override-provided-method.3.out +++ b/charon/tests/ui/issue-70-override-provided-method.3.out @@ -52,6 +52,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -122,8 +135,8 @@ where @0 := () } storage_dead(@3) - drop y@2 - drop x@1 + drop[Drop] y@2 + drop[Drop] x@1 @0 := () return } @@ -181,7 +194,7 @@ where @0 := () } storage_dead(@3) - drop y@2 + drop[Drop] y@2 @0 := () return } @@ -251,8 +264,8 @@ where @0 := () } storage_dead(@3) - drop y@2 - drop x@1 + drop[Drop] y@2 + drop[Drop[@TraitClause0]>] x@1 @0 := () return } diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out index 2c67c2597..5187b4be9 100644 --- a/charon/tests/ui/iterator.out +++ b/charon/tests/ui/iterator.out @@ -1325,6 +1325,28 @@ where fn into_iter = {impl IntoIterator for Array}::into_iter[@TraitClause0] } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +// Full name: core::array::iter::{impl Drop for IntoIter[@TraitClause0]}::drop +pub fn {impl Drop for IntoIter[@TraitClause0]}::drop<'_0, T, const N : usize>(@1: &'_0 mut (IntoIter[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: core::array::iter::{impl Drop for IntoIter[@TraitClause0]} +impl Drop for IntoIter[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for IntoIter[@TraitClause0]}::drop<'_0_0, T, const N : usize>[@TraitClause0] +} + #[lang_item("clone_fn")] pub fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self where @@ -2249,6 +2271,10 @@ pub fn core::ops::arith::AddAssign::add_assign<'_0, Self, Rhs>(@1: &'_0 mut (Sel where [@TraitClause0]: AddAssign, +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnMut::call_mut pub fn call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output where @@ -2377,7 +2403,7 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: FnMut, + [@TraitClause3]: FnMut, @TraitClause3::parent_clause1::Output = (), #[lang_item("iter_filter")] @@ -2581,7 +2607,7 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized, - [@TraitClause3]: FnMut, + [@TraitClause3]: FnMut, @TraitClause3::parent_clause1::Output = B, pub fn core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::reduce<'a, T, F>(@1: Iter<'a, T>[@TraitClause0], @2: F) -> Option<&'a (T)>[{impl Iterator for Iter<'a, T>[@TraitClause0]}<'a, T>[@TraitClause0]::parent_clause1] @@ -2610,7 +2636,7 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: FnMut, + [@TraitClause3]: FnMut, @TraitClause3::parent_clause1::Output = bool, // Full name: core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::any @@ -2619,16 +2645,16 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: FnMut, + [@TraitClause3]: FnMut, @TraitClause3::parent_clause1::Output = bool, // Full name: core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::find -pub fn {impl Iterator for Iter<'a, T>[@TraitClause0]}::find<'a, '_1, T, P>(@1: &'_1 mut (Iter<'a, T>[@TraitClause0]), @2: P) -> Option<&'_ (T)>[Sized<&'_ (T)>] +pub fn {impl Iterator for Iter<'a, T>[@TraitClause0]}::find<'a, '_1, T, P>(@1: &'_1 mut (Iter<'a, T>[@TraitClause0]), @2: P) -> Option<&'a (T)>[Sized<&'_ (T)>] where [@TraitClause0]: Sized, [@TraitClause1]: Sized

, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: for<'_0> FnMut, + [@TraitClause3]: for<'_0> FnMut, for<'_0> @TraitClause3::parent_clause1::Output = bool, // Full name: core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::find_map @@ -2638,7 +2664,7 @@ where [@TraitClause1]: Sized, [@TraitClause2]: Sized, [@TraitClause3]: Sized[@TraitClause0]>, - [@TraitClause4]: FnMut, + [@TraitClause4]: FnMut, @TraitClause4::parent_clause1::Output = Option[@TraitClause1], pub fn core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::try_find<'a, '_1, T, R, impl FnMut(&Self::Item) -> R>(@1: &'_1 mut (Iter<'a, T>[@TraitClause0]), @2: impl FnMut(&Self::Item) -> R) -> @TraitClause5::TryType @@ -2659,7 +2685,7 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized

, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: FnMut, + [@TraitClause3]: FnMut, @TraitClause3::parent_clause1::Output = bool, // Full name: core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::rposition @@ -2896,7 +2922,7 @@ where [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, - [@TraitClause3]: for<'_0, '_1> FnMut, + [@TraitClause3]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause3::parent_clause1::Output = bool, pub fn core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by_key<'a, T, F, K>(@1: Iter<'a, T>[@TraitClause0], @2: F) -> bool @@ -2910,7 +2936,7 @@ where @TraitClause4::parent_clause1::Output = K, // Full name: core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::__iterator_get_unchecked -pub unsafe fn {impl Iterator for Iter<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (Iter<'a, T>[@TraitClause0]), @2: usize) -> &'_ (T) +pub unsafe fn {impl Iterator for Iter<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (Iter<'a, T>[@TraitClause0]), @2: usize) -> &'a (T) where [@TraitClause0]: Sized, @@ -2935,7 +2961,7 @@ where fn intersperse<[@TraitClause0]: Sized[@TraitClause0]>, [@TraitClause1]: Clone<&'a (T)>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::intersperse<'a, T>[@TraitClause0, @TraitClause0_0, @TraitClause0_1] fn intersperse_with, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = &'a (T)> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::intersperse_with<'a, T, G>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn map, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, @TraitClause1_3::parent_clause1::Output = B> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::map<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] - fn for_each, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = ()> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::for_each<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn for_each, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = ()> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::for_each<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn filter, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0> FnMut, for<'_0> @TraitClause1_2::parent_clause1::Output = bool> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::filter<'a, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn filter_map, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, @TraitClause1_3::parent_clause1::Output = Option[@TraitClause1_0]> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::filter_map<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] fn enumerate<[@TraitClause0]: Sized[@TraitClause0]>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::enumerate<'a, T>[@TraitClause0, @TraitClause0_0] @@ -2960,15 +2986,15 @@ where fn is_partitioned, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::is_partitioned<'a, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn try_fold<'_0, B, F, R, [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized, [@TraitClause3]: Sized[@TraitClause0]>, [@TraitClause4]: FnMut, [@TraitClause5]: Try, @TraitClause1_4::parent_clause1::Output = R, @TraitClause1_5::Output = B> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::try_fold<'a, '_0_0, T, B, F, R>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4, @TraitClause0_5] fn try_for_each<'_0, F, R, [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, [@TraitClause4]: Try, @TraitClause1_3::parent_clause1::Output = R, @TraitClause1_4::Output = ()> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::try_for_each<'a, '_0_0, T, F, R>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] - fn fold, [@TraitClause1]: Sized, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = B> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::fold<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn fold, [@TraitClause1]: Sized, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = B> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::fold<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn reduce, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = &'a (T)> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::reduce<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn try_reduce<'_0, R, impl FnMut(Self::Item, Self::Item) -> R, [@TraitClause0]: Sized, [@TraitClause1]: Sized R>, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: Try, [@TraitClause4]: Residual<@TraitClause1_3::Residual, Option<&'a (T)>[{impl Iterator for Iter<'a, T>[@TraitClause0]}<'a, T>[@TraitClause0]::parent_clause1]>, [@TraitClause5]: FnMut R, (&'a (T), &'a (T))>, @TraitClause1_3::Output = &'a (T), @TraitClause1_5::parent_clause1::Output = R> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::try_reduce<'a, '_0_0, T, R, impl FnMut(Self::Item, Self::Item) -> R>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4, @TraitClause0_5] - fn all<'_0, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::all<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] - fn any<'_0, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::any<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] - fn find<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0> FnMut, for<'_0> @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::find<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] - fn find_map<'_0, B, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, @TraitClause1_3::parent_clause1::Output = Option[@TraitClause1_0]> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::find_map<'a, '_0_0, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] + fn all<'_0, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::all<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn any<'_0, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::any<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn find<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0> FnMut, for<'_0> @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::find<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn find_map<'_0, B, F, [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, @TraitClause1_3::parent_clause1::Output = Option[@TraitClause1_0]> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::find_map<'a, '_0_0, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] fn try_find<'_0, R, impl FnMut(&Self::Item) -> R, [@TraitClause0]: Sized, [@TraitClause1]: Sized R>, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: Try, [@TraitClause4]: Residual<@TraitClause1_3::Residual, Option<&'a (T)>[{impl Iterator for Iter<'a, T>[@TraitClause0]}<'a, T>[@TraitClause0]::parent_clause1]>, [@TraitClause5]: for<'_0> FnMut R, (&'_0_0 (&'a (T)))>, @TraitClause1_3::Output = bool, for<'_0> @TraitClause1_5::parent_clause1::Output = R> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::try_find<'a, '_0_0, T, R, impl FnMut(&Self::Item) -> R>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4, @TraitClause0_5] - fn position<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::position<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn position<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: FnMut, @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::position<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn rposition<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: FnMut, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: ExactSizeIterator[@TraitClause0]>, [@TraitClause4]: DoubleEndedIterator[@TraitClause0]>, @TraitClause1_1::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::rposition<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn max<[@TraitClause0]: Sized[@TraitClause0]>, [@TraitClause1]: Ord<&'a (T)>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::max<'a, T>[@TraitClause0, @TraitClause0_0, @TraitClause0_1] fn min<[@TraitClause0]: Sized[@TraitClause0]>, [@TraitClause1]: Ord<&'a (T)>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::min<'a, T>[@TraitClause0, @TraitClause0_0, @TraitClause0_1] @@ -2996,7 +3022,7 @@ where fn gt, [@TraitClause1]: IntoIterator, [@TraitClause2]: PartialOrd<&'a (T), @TraitClause1_1::Item>, [@TraitClause3]: Sized[@TraitClause0]>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::gt<'a, T, I>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] fn ge, [@TraitClause1]: IntoIterator, [@TraitClause2]: PartialOrd<&'a (T), @TraitClause1_1::Item>, [@TraitClause3]: Sized[@TraitClause0]>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::ge<'a, T, I>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] fn is_sorted<[@TraitClause0]: Sized[@TraitClause0]>, [@TraitClause1]: PartialOrd<&'a (T), &'a (T)>> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted<'a, T>[@TraitClause0, @TraitClause0_0, @TraitClause0_1] - fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] + fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by_key<'a, T, F, K>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0] } @@ -3029,7 +3055,7 @@ where [@TraitClause0]: Sized, // Full name: core::slice::iter::{impl Iterator for Chunks<'a, T>[@TraitClause0]}::last -pub fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::last<'a, T>(@1: Chunks<'a, T>[@TraitClause0]) -> Option<&'_ (Slice)>[Sized<&'_ (Slice)>] +pub fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::last<'a, T>(@1: Chunks<'a, T>[@TraitClause0]) -> Option<&'a (Slice)>[Sized<&'_ (Slice)>] where [@TraitClause0]: Sized, @@ -3038,7 +3064,7 @@ where [@TraitClause0]: Sized, // Full name: core::slice::iter::{impl Iterator for Chunks<'a, T>[@TraitClause0]}::nth -pub fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::nth<'a, '_1, T>(@1: &'_1 mut (Chunks<'a, T>[@TraitClause0]), @2: usize) -> Option<&'_ (Slice)>[Sized<&'_ (Slice)>] +pub fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::nth<'a, '_1, T>(@1: &'_1 mut (Chunks<'a, T>[@TraitClause0]), @2: usize) -> Option<&'a (Slice)>[Sized<&'_ (Slice)>] where [@TraitClause0]: Sized, @@ -3617,7 +3643,7 @@ where @TraitClause4::parent_clause1::Output = K, // Full name: core::slice::iter::{impl Iterator for Chunks<'a, T>[@TraitClause0]}::__iterator_get_unchecked -pub unsafe fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice) +pub unsafe fn {impl Iterator for Chunks<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'a (Slice) where [@TraitClause0]: Sized, @@ -3736,7 +3762,7 @@ where [@TraitClause0]: Sized, // Full name: core::slice::iter::{impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::last -pub fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::last<'a, T>(@1: ChunksExact<'a, T>[@TraitClause0]) -> Option<&'_ (Slice)>[Sized<&'_ (Slice)>] +pub fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::last<'a, T>(@1: ChunksExact<'a, T>[@TraitClause0]) -> Option<&'a (Slice)>[Sized<&'_ (Slice)>] where [@TraitClause0]: Sized, @@ -3745,7 +3771,7 @@ where [@TraitClause0]: Sized, // Full name: core::slice::iter::{impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::nth -pub fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::nth<'a, '_1, T>(@1: &'_1 mut (ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> Option<&'_ (Slice)>[Sized<&'_ (Slice)>] +pub fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::nth<'a, '_1, T>(@1: &'_1 mut (ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> Option<&'a (Slice)>[Sized<&'_ (Slice)>] where [@TraitClause0]: Sized, @@ -4324,7 +4350,7 @@ where @TraitClause4::parent_clause1::Output = K, // Full name: core::slice::iter::{impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::__iterator_get_unchecked -pub unsafe fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice) +pub unsafe fn {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> &'a (Slice) where [@TraitClause0]: Sized, @@ -4570,9 +4596,9 @@ fn main() storage_dead(@11) storage_dead(@9) storage_dead(@8) - drop iter@7 + drop[{impl Drop for IntoIter[@TraitClause0]}[Sized]] iter@7 storage_dead(iter@7) - drop @4 + drop[{impl Drop for IntoIter[@TraitClause0]}[Sized]] @4 storage_dead(@4) storage_dead(@3) storage_live(@15) diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out index 8cc39a7cf..8d58f1280 100644 --- a/charon/tests/ui/matches.out +++ b/charon/tests/ui/matches.out @@ -11,6 +11,19 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::E1 pub enum E1 { V1, @@ -45,7 +58,7 @@ where let x@1: T; // arg #1 @0 := move (x@1) - drop x@1 + drop[Drop] x@1 return } diff --git a/charon/tests/ui/method-impl-generalization.out b/charon/tests/ui/method-impl-generalization.out index 727bbd4eb..e02f66eee 100644 --- a/charon/tests/ui/method-impl-generalization.out +++ b/charon/tests/ui/method-impl-generalization.out @@ -40,6 +40,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::Trait trait Trait { @@ -79,7 +92,7 @@ where let _other@2: T; // arg #2 @0 := () - drop _other@2 + drop[Drop] _other@2 @0 := () return } diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index b88606429..4e51c77bb 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -18,6 +18,14 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -253,7 +261,7 @@ fn test_crate::main::{impl FnOnce<(u8, u8)> for closure<'_0, '_1>}::call_once::< storage_live(@3) @3 := &mut @1 @0 := test_crate::main::{impl FnMut<(u8, u8)> for closure<'_0, '_1>}::call_mut::<'_, '_, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 return } @@ -271,7 +279,7 @@ fn test_crate::apply_to_once::>(@1: test_cra @0 := {impl FnOnce<(u8, u8)> for closure<'_0, '_1>}<'_, '_>::call_once(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop>] f@1 return } diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 56a13840b..2d9e2e04e 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -24,6 +24,14 @@ struct NotCopy {} #[lang_item("mem_drop")] pub fn core::mem::drop::(@1: NotCopy) +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -122,7 +130,7 @@ fn test_crate::apply_to_zero_once::(@1: closure) -> u8 @0 := {impl FnOnce<(u8)> for closure}::call_once(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop] f@1 return } diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index 949ac7d57..428bfb28a 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -24,6 +24,14 @@ struct Thing {} #[lang_item("mem_drop")] pub fn core::mem::drop::(@1: Thing) +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -128,7 +136,7 @@ fn test_crate::apply_to_zero::>(@1: test_crate:: @0 := {impl Fn<(u8)> for test_crate::main::closure<'_0>}<'_>::call(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop>] f@1 return } @@ -197,7 +205,7 @@ fn test_crate::apply_to_zero_mut::>(@1: test_c @0 := {impl FnMut<(u8)> for test_crate::main::closure#1<'_0>}<'_>::call_mut(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop>] f@1 return } @@ -286,7 +294,7 @@ fn test_crate::apply_to_zero_once::(@1: test_crate: @0 := {impl FnOnce<(u8)> for test_crate::main::closure#2}::call_once(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop] f@1 return } diff --git a/charon/tests/ui/monomorphization/fndefs-casts.out b/charon/tests/ui/monomorphization/fndefs-casts.out index 007b0f9ee..53ef070c2 100644 --- a/charon/tests/ui/monomorphization/fndefs-casts.out +++ b/charon/tests/ui/monomorphization/fndefs-casts.out @@ -18,6 +18,14 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -108,7 +116,7 @@ fn test_crate::takes_closure::>(@1: test_crate::foo:: storage_dead(@2) storage_dead(@6) storage_dead(@5) - drop c@1 + drop[Drop>] c@1 @0 := () return } diff --git a/charon/tests/ui/monomorphization/trait_impls.out b/charon/tests/ui/monomorphization/trait_impls.out index 541c9e84b..cdb9c711b 100644 --- a/charon/tests/ui/monomorphization/trait_impls.out +++ b/charon/tests/ui/monomorphization/trait_impls.out @@ -37,6 +37,14 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + fn test_crate::do_test::(@1: bool, @2: bool) { let @0: (); // return @@ -66,8 +74,8 @@ fn test_crate::do_test::(@1: bool, @2: bool) storage_dead(@4) storage_dead(@3) @0 := () - drop expected@2 - drop init@1 + drop[Drop] expected@2 + drop[Drop] init@1 @0 := () return } diff --git a/charon/tests/ui/monomorphization/trait_impls_ullbc.out b/charon/tests/ui/monomorphization/trait_impls_ullbc.out index 751a4d43a..2dce428fe 100644 --- a/charon/tests/ui/monomorphization/trait_impls_ullbc.out +++ b/charon/tests/ui/monomorphization/trait_impls_ullbc.out @@ -37,6 +37,14 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + fn test_crate::do_test::(@1: bool, @2: bool) { let @0: (); // return @@ -62,8 +70,8 @@ fn test_crate::do_test::(@1: bool, @2: bool) } bb2: { - drop expected@2; - drop init@1; + drop[Drop] expected@2; + drop[Drop] init@1; unwind_continue; } @@ -73,8 +81,8 @@ fn test_crate::do_test::(@1: bool, @2: bool) storage_dead(@4); storage_dead(@3); @0 := (); - drop expected@2; - drop init@1; + drop[Drop] expected@2; + drop[Drop] init@1; @0 := (); return; } diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index b56d04d78..c2f1a77ea 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -38,10 +38,38 @@ pub fn core::ops::deref::DerefMut::deref_mut<'_0, Self>(@1: &'_0 mut (Self)) -> where [@TraitClause0]: DerefMut, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: alloc::boxed::{impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::deref pub fn {impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::deref<'_0, T, A>(@1: &'_0 (alloc::boxed::Box[@TraitClause0, @TraitClause1])) -> &'_0 (T) where @@ -94,6 +122,20 @@ where Nil, } +// Full name: test_crate::List::{impl Drop for List[@TraitClause0]}::drop +fn {impl Drop for List[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (List[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: test_crate::List::{impl Drop for List[@TraitClause0]} +impl Drop for List[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for List[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: test_crate::One pub enum One where @@ -194,6 +236,20 @@ where T, } +// Full name: test_crate::IdType::{impl Drop for IdType[@TraitClause0]}::drop +fn {impl Drop for IdType[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (IdType[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: test_crate::IdType::{impl Drop for IdType[@TraitClause0]} +impl Drop for IdType[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for IdType[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: test_crate::use_id_type pub fn use_id_type(@1: IdType[@TraitClause0]) -> T where @@ -203,7 +259,7 @@ where let x@1: IdType[@TraitClause0]; // arg #1 @0 := move ((x@1).0) - drop x@1 + drop[{impl Drop for IdType[@TraitClause0]}[@TraitClause0]] x@1 return } @@ -219,9 +275,9 @@ where storage_live(@2) @2 := move (x@1) @0 := IdType { 0: move (@2) } - drop @2 + drop[Drop] @2 storage_dead(@2) - drop x@1 + drop[Drop] x@1 return } @@ -373,10 +429,10 @@ pub fn test_list1() @2 := @BoxNew[Sized]>[Sized[Sized]>](move (@3)) storage_dead(@3) l@1 := List::Cons { 0: const (0 : i32), 1: move (@2) } - drop @2 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[Sized], Global>[MetaSized[Sized]>, Sized]] @2 storage_dead(@2) @0 := () - drop l@1 + drop[{impl Drop for List[@TraitClause0]}[Sized]] l@1 storage_dead(l@1) @0 := () return @@ -425,7 +481,7 @@ pub fn test_box1() @0 := () storage_dead(x@4) storage_dead(x@2) - drop b@1 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] b@1 storage_dead(b@1) @0 := () return @@ -505,15 +561,15 @@ where storage_live(@5) @5 := move (*(tl@3)) @0 := (move (@4), move (@5)) - drop @5 + drop[{impl Drop for List[@TraitClause0]}[@TraitClause0]] @5 storage_dead(@5) - drop @4 + drop[Drop] @4 storage_dead(@4) - drop tl@3 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[@TraitClause0], Global>[MetaSized[@TraitClause0]>, Sized]] tl@3 storage_dead(tl@3) - drop hd@2 + drop[Drop] hd@2 storage_dead(hd@2) - drop l@1 + drop[{impl Drop for List[@TraitClause0]}[@TraitClause0]] l@1 return } diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index 45f2e2786..5fa07d990 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -69,6 +69,18 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -79,6 +91,22 @@ where Some(T), } +// Full name: core::result::Result::{impl Drop for Result[@TraitClause0, @TraitClause1]}::drop +fn {impl Drop for Result[@TraitClause0, @TraitClause1]}::drop<'_0, T, E>(@1: &'_0 mut (Result[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + +// Full name: core::result::Result::{impl Drop for Result[@TraitClause0, @TraitClause1]} +impl Drop for Result[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Result[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, E>[@TraitClause0, @TraitClause1] +} + // Full name: test_crate::wrap fn wrap<'a>(@1: &'a (u32)) -> Option<&'a (u32)>[Sized<&'a (u32)>] { @@ -125,7 +153,7 @@ fn foo() @3 := &ref_b@1 @2 := try_borrow<'_, bool>[MetaSized](move (@3)) storage_dead(@3) - drop @2 + drop[{impl Drop for Result[@TraitClause0, @TraitClause1]}[MetaSized], BorrowError>[Sized[MetaSized]>, Sized]] @2 storage_dead(@2) @0 := () storage_dead(ref_b@1) diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out index 544f64298..2954ec183 100644 --- a/charon/tests/ui/quantified-clause.out +++ b/charon/tests/ui/quantified-clause.out @@ -265,6 +265,19 @@ where Break(B), } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -374,7 +387,7 @@ where let _f@1: F; // arg #1 @0 := () - drop _f@1 + drop[Drop] _f@1 @0 := () return } diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index b7f5e4298..ef3ee4fa0 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -147,6 +147,14 @@ pub fn {impl Clone for usize}::clone<'_0>(@1: &'_0 (usize)) -> usize return } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + pub fn core::clone::impls::{impl Clone for usize}::clone_from<'_0, '_1>(@1: &'_0 mut (usize), @2: &'_1 (usize)) where [@TraitClause0]: Destruct, @@ -158,7 +166,7 @@ where storage_live(@3) @3 := {impl Clone for usize}::clone<'_>(move (source@2)) - drop *(self@1) + drop[Drop] *(self@1) *(self@1) := move (@3) storage_dead(@3) @0 := () @@ -2015,13 +2023,35 @@ where storage_live(@3) @3 := @TraitClause0::clone<'_>(move (source@2)) - drop *(self@1) + drop[Drop] *(self@1) *(self@1) := move (@3) storage_dead(@3) @0 := () return } +// Full name: core::intrinsics::size_of_val +pub unsafe fn size_of_val(@1: *const T) -> usize +where + [@TraitClause0]: MetaSized, +{ + let @0: usize; // return + let ptr@1: *const T; // arg #1 + + undefined_behavior +} + +// Full name: core::intrinsics::align_of_val +pub unsafe fn align_of_val(@1: *const T) -> usize +where + [@TraitClause0]: MetaSized, +{ + let @0: usize; // return + let ptr@1: *const T; // arg #1 + + undefined_behavior +} + // Full name: core::num::niche_types::NonZeroUsizeInner pub struct NonZeroUsizeInner { usize, @@ -2048,7 +2078,7 @@ where storage_live(@3) @3 := {impl Clone for NonZeroUsizeInner}::clone<'_>(move (source@2)) - drop *(self@1) + drop[Drop] *(self@1) *(self@1) := move (@3) storage_dead(@3) @0 := () @@ -2110,6 +2140,10 @@ where @TraitClause1::NonZeroInner, } +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ptr::unique::Unique #[lang_item("ptr_unique")] pub struct Unique { @@ -5874,7 +5908,7 @@ where storage_dead(@4) storage_dead(@3) @0 := copy ((@2).0) - drop @2 + drop[Drop<(*mut T, A)>] @2 storage_dead(@2) return } @@ -5913,7 +5947,7 @@ where storage_dead(@5) storage_dead(@4) @2 := copy ((@3).0) - drop @3 + drop[Drop<(*mut T, A)>] @3 storage_dead(@3) storage_dead(b@8) @0 := &mut *(@2) @@ -5921,6 +5955,97 @@ where return } +// Full name: alloc::boxed::{impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop +pub fn {impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop<'_0, T, A>(@1: &'_0 mut (Box[@TraitClause0, @TraitClause1, @TraitClause2])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + [@TraitClause2]: Allocator, +{ + let @0: (); // return + let self@1: &'_ mut (Box[@TraitClause0, @TraitClause1, @TraitClause2]); // arg #1 + let layout@2: Layout; // local + let t@3: *const T; // local + let @4: *mut T; // anonymous local + let self@5: &'_ (Layout); // local + let @6: (); // anonymous local + let @7: &'_ (A); // anonymous local + let size@8: usize; // local + let align@9: usize; // local + let @10: bool; // anonymous local + let @11: (); // anonymous local + let @12: Alignment; // anonymous local + let unique@13: NonNull; // local + let @14: *const u8; // anonymous local + let ptr@15: NonNull; // local + let ptr@16: PhantomData; // local + + storage_live(layout@2) + storage_live(@4) + storage_live(@6) + storage_live(@7) + storage_live(size@8) + storage_live(@11) + storage_live(unique@13) + storage_live(@14) + storage_live(ptr@15) + storage_live(ptr@16) + ptr@15 := copy (((*(self@1)).0).pointer) + ptr@16 := copy (((*(self@1)).0)._marker) + storage_live(t@3) + @4 := transmute, *mut T>(copy (ptr@15)) + t@3 := transmute, *const T>(copy (ptr@15)) + storage_live(align@9) + size@8 := size_of_val[@TraitClause0](copy (t@3)) + align@9 := align_of_val[@TraitClause0](move (t@3)) + storage_live(@10) + @10 := ub_checks + if move (@10) { + @11 := core::alloc::layout::{Layout}::from_size_align_unchecked::precondition_check(copy (size@8), copy (align@9)) + } + else { + } + storage_dead(@10) + storage_live(@12) + @12 := transmute(copy (align@9)) + layout@2 := Layout { size: copy (size@8), align: move (@12) } + storage_dead(@12) + storage_dead(align@9) + storage_dead(t@3) + storage_live(self@5) + self@5 := &layout@2 + storage_dead(self@5) + switch move (size@8) { + 0 : usize => { + }, + _ => { + storage_live(@7) + @7 := &(*(self@1)).1 + storage_live(@14) + @14 := cast<*mut T, *const u8>(copy (@4)) + unique@13 := NonNull { pointer: move (@14) } + storage_dead(@14) + @6 := @TraitClause2::deallocate<'_>(move (@7), move (unique@13), copy (layout@2)) + storage_dead(@7) + @0 := () + return + }, + } + @0 := () + return +} + +// Full name: alloc::boxed::{impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2]} +impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + [@TraitClause2]: Allocator, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1, @TraitClause2]> + fn drop<'_0> = {impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1, @TraitClause2] +} + // Full name: test_crate::foo unsafe fn foo() { @@ -5959,7 +6084,7 @@ unsafe fn foo() i@8 := copy (*(@9)) @0 := () storage_dead(i@8) - drop b@6 + drop[{impl Drop for Box[@TraitClause0, @TraitClause1, @TraitClause2]}[MetaSized, Sized, {impl Allocator for Global}]] b@6 storage_dead(b@6) storage_dead(p@2) storage_dead(b@1) 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 b4750b9ee..fb5d2c037 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 @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -152,7 +165,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(()), ()> for closure[@TraitClause0, @TraitClause1]}::call_mut<'_, F, Clause1_Repr>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 @0 := () return } diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index cd0c41426..c40a0f24b 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -183,6 +183,19 @@ impl Display for u32 { fn fmt<'_0, '_1, '_2> = {impl Display for u32}::fmt<'_0_0, '_0_1, '_0_2> } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::result::unwrap_failed fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 (dyn (exists(TODO)))) -> ! diff --git a/charon/tests/ui/rust-name-matcher-tests.rs b/charon/tests/ui/rust-name-matcher-tests.rs index 5aca0f729..7998608f9 100644 --- a/charon/tests/ui/rust-name-matcher-tests.rs +++ b/charon/tests/ui/rust-name-matcher-tests.rs @@ -24,6 +24,9 @@ trait Trait { } #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}")] +#[pattern::pass("_::{impl test_crate::Trait<_> for _}")] +#[pattern::pass("*::{impl test_crate::Trait<_> for _}")] +#[pattern::pass("{impl test_crate::Trait<_> for _}")] #[pattern::pass("test_crate::{impl test_crate::Trait<_, _>}")] #[pattern::fail("test_crate::{impl test_crate::Trait<_>}")] #[pattern::fail("test_crate::{impl test_crate::Trait<_, _> for _}")] @@ -44,6 +47,7 @@ trait Trait { #[pattern::fail("test_crate::Trait<_>")] impl Trait> for Box { #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}::method")] + #[pattern::pass("{impl test_crate::Trait<_> for _}::method")] #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}::_")] #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}")] #[pattern::pass("test_crate::{impl test_crate::Trait<_, _>}"::method)] diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index ed9af22cc..c38879a39 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -38,6 +38,18 @@ pub fn core::f64::{f64}::MIN() -> f64 pub const core::f64::{f64}::MIN: f64 = core::f64::{f64}::MIN() +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -92,6 +104,22 @@ pub struct Global {} #[lang_item("exchange_malloc")] unsafe fn exchange_malloc(@1: usize, @2: usize) -> *mut u8 +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: test_crate::addr_of fn addr_of() { @@ -308,7 +336,7 @@ fn {impl FnOnce<(u8)> for closure}::call_once(@1: closure, @2: (u8)) storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u8)> for closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 @0 := () return } @@ -407,9 +435,9 @@ fn boxes() storage_live(@2) @2 := @BoxNew[MetaSized, Sized](const (42 : i32)) @1 := move (@2) - drop @2 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @2 storage_dead(@2) - drop @1 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @1 storage_dead(@1) @0 := () @0 := () diff --git a/charon/tests/ui/send_bound.out b/charon/tests/ui/send_bound.out index a2d2e48c4..0ca235346 100644 --- a/charon/tests/ui/send_bound.out +++ b/charon/tests/ui/send_bound.out @@ -15,6 +15,19 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::foo fn foo(@1: M) where @@ -25,7 +38,7 @@ where let _msg@1: M; // arg #1 @0 := () - drop _msg@1 + drop[Drop] _msg@1 @0 := () return } diff --git a/charon/tests/ui/simple/additions.out b/charon/tests/ui/simple/additions.out index 7b28dd5a5..6cba30bed 100644 --- a/charon/tests/ui/simple/additions.out +++ b/charon/tests/ui/simple/additions.out @@ -32,6 +32,14 @@ pub fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self where [@TraitClause0]: Clone, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + // Full name: core::clone::Clone::clone_from pub fn clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self)) where @@ -45,7 +53,7 @@ where storage_live(@3) @3 := @TraitClause0::clone<'_>(move (source@2)) - drop *(self@1) + drop[Drop] *(self@1) *(self@1) := move (@3) storage_dead(@3) @0 := () @@ -73,7 +81,7 @@ where storage_live(@3) @3 := {impl Clone for u8}::clone<'_>(move (source@2)) - drop *(self@1) + drop[Drop] *(self@1) *(self@1) := move (@3) storage_dead(@3) @0 := () @@ -155,6 +163,11 @@ pub fn overflowing_add(@1: u8, @2: u8) -> (u8, bool) return } +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::main fn main() { 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 39f3b6e22..7c6f19588 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out @@ -11,6 +11,19 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::Trait trait Trait { @@ -28,7 +41,7 @@ where let it@1: I; // arg #1 @0 := () - drop it@1 + drop[Drop] it@1 @0 := () return } @@ -55,7 +68,7 @@ where @2 := move (it@1) @0 := takes_trait[@TraitClause1::parent_clause1, @TraitClause1::parent_clause2](move (@2)) storage_dead(@2) - drop it@1 + drop[Drop] it@1 @0 := () return } diff --git a/charon/tests/ui/simple/box-into-inner.out b/charon/tests/ui/simple/box-into-inner.out index c40cfdebb..ac43264dd 100644 --- a/charon/tests/ui/simple/box-into-inner.out +++ b/charon/tests/ui/simple/box-into-inner.out @@ -55,6 +55,15 @@ where #[lang_item("String")] pub opaque type String +// Full name: alloc::string::String::{impl Drop for String}::drop +fn {impl Drop for String}::drop<'_0>(@1: &'_0 mut (String)) + +// Full name: alloc::string::String::{impl Drop for String} +impl Drop for String { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for String}::drop<'_0_0> +} + // Full name: test_crate::into_inner fn into_inner(@1: alloc::boxed::Box[MetaSized, Sized]) { @@ -96,7 +105,7 @@ fn into_inner(@1: alloc::boxed::Box[MetaSized, Sized]) assert(copy (@13) == true) _x@2 := move (*(@6)) @0 := () - drop _x@2 + drop[{impl Drop for String}] _x@2 storage_dead(_x@2) @5 := transmute, *const String>(copy ((*(b@1)).0)) @3 := &mut b@1 diff --git a/charon/tests/ui/simple/box-new.out b/charon/tests/ui/simple/box-new.out index 68175585e..aa2fcd5b8 100644 --- a/charon/tests/ui/simple/box-new.out +++ b/charon/tests/ui/simple/box-new.out @@ -11,10 +11,38 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: test_crate::main fn main() { @@ -23,7 +51,7 @@ fn main() storage_live(@1) @1 := @BoxNew[Sized](const (42 : i32)) - drop @1 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @1 storage_dead(@1) @0 := () @0 := () 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 b3810ef43..a0a876622 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 @@ -11,6 +11,18 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::Trait pub trait Trait { @@ -32,6 +44,20 @@ where S, } +// Full name: test_crate::HashMap::{impl Drop for HashMap[@TraitClause0]}::drop +fn {impl Drop for HashMap[@TraitClause0]}::drop<'_0, S>(@1: &'_0 mut (HashMap[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: test_crate::HashMap::{impl Drop for HashMap[@TraitClause0]} +impl Drop for HashMap[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for HashMap[@TraitClause0]}::drop<'_0_0, S>[@TraitClause0] +} + // Full name: test_crate::{HashMap[@TraitClause0]}::get pub fn get(@1: HashMap[@TraitClause0], @2: Q) where @@ -44,8 +70,8 @@ where let _k@2: Q; // arg #2 @0 := () - drop _k@2 - drop _x@1 + drop[Drop] _k@2 + drop[{impl Drop for HashMap[@TraitClause0]}[@TraitClause0]] _x@1 @0 := () return } @@ -62,8 +88,8 @@ where let _k@2: Q; // arg #2 @0 := () - drop _k@2 - drop _x@1 + drop[Drop] _k@2 + drop[{impl Drop for HashMap[@TraitClause0]}[@TraitClause0]] _x@1 @0 := () return } 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 2cd8978e7..6fc5f0ec8 100644 --- a/charon/tests/ui/simple/call-method-via-supertrait-bound.out +++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.out @@ -11,6 +11,19 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::OtherTrait trait OtherTrait { @@ -77,7 +90,7 @@ where storage_dead(@3) storage_dead(@2) @0 := () - drop x@1 + drop[Drop] x@1 @0 := () return } 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 87b592d41..67c68a2eb 100644 --- a/charon/tests/ui/simple/closure-capture-ref-by-move.out +++ b/charon/tests/ui/simple/closure-capture-ref-by-move.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -115,7 +128,7 @@ fn {impl FnOnce<()> for closure<'_0>}::call_once<'_0>(@1: closure<'_0>, @2: ()) storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 @0 := () return } diff --git a/charon/tests/ui/simple/closure-fn.out b/charon/tests/ui/simple/closure-fn.out index e130a2667..b1fa89639 100644 --- a/charon/tests/ui/simple/closure-fn.out +++ b/charon/tests/ui/simple/closure-fn.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -127,7 +140,7 @@ where @0 := @TraitClause1::call_once(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop u8>] f@1 return } @@ -212,7 +225,7 @@ fn {impl FnOnce<(u8, u8)> for closure<'_0, '_1>}::call_once<'_0, '_1>(@1: closur storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u8, u8)> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 return } diff --git a/charon/tests/ui/simple/closure-fnmut.out b/charon/tests/ui/simple/closure-fnmut.out index f2e829618..dde90bf92 100644 --- a/charon/tests/ui/simple/closure-fnmut.out +++ b/charon/tests/ui/simple/closure-fnmut.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -68,7 +81,7 @@ where @0 := @TraitClause1::call_mut<'_>(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop u8>] f@1 return } @@ -117,7 +130,7 @@ fn {impl FnOnce<(u8)> for closure<'_0>}::call_once<'_0>(@1: closure<'_0>, @2: (u storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u8)> for closure<'_0>}::call_mut<'_0, '_>(move (@3), move (@2)) - drop @1 + drop[Drop>] @1 return } diff --git a/charon/tests/ui/simple/closure-fnonce.out b/charon/tests/ui/simple/closure-fnonce.out index 0127b1503..044110a43 100644 --- a/charon/tests/ui/simple/closure-fnonce.out +++ b/charon/tests/ui/simple/closure-fnonce.out @@ -18,12 +18,23 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } -// Full name: core::mem::drop #[lang_item("mem_drop")] -pub fn drop(@1: T) +pub fn core::mem::drop(@1: T) where [@TraitClause0]: Sized, +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -59,7 +70,7 @@ where @0 := @TraitClause1::call_once(move (@2), move (@3)) storage_dead(@3) storage_dead(@2) - drop f@1 + drop[Drop u8>] f@1 return } @@ -89,7 +100,7 @@ fn {impl FnOnce<(u8)> for closure}::call_once(@1: closure, @2: (u8)) -> u8 storage_live(@4) storage_live(@5) @5 := move ((@1).0) - @4 := drop[Sized](move (@5)) + @4 := core::mem::drop[Sized](move (@5)) storage_dead(@5) storage_dead(@4) storage_live(@6) diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out index 56bebf929..220d95cad 100644 --- a/charon/tests/ui/simple/closure-inside-impl.out +++ b/charon/tests/ui/simple/closure-inside-impl.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -146,7 +159,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(())> for closure[@TraitClause0, @TraitClause1]}::call_mut<'_, F, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 @0 := () return } diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index 44bc51dc1..cec7918d6 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -92,7 +105,7 @@ where storage_live(@3) @3 := move ((tupled_args@2).0) @0 := () - drop @3 + drop[Drop<@TraitClause0::Item>] @3 @0 := () return } @@ -118,12 +131,12 @@ where @5 := move (i@1) @4 := (move (@5)) @0 := {impl Fn<(@TraitClause0::Item)> for closure[@TraitClause0]}::call<'_, Self>[@TraitClause0](move (@2), move (@4)) - drop @5 + drop[Drop<@TraitClause0::Item>] @5 storage_dead(@5) storage_dead(@4) storage_dead(@2) storage_dead(@3) - drop i@1 + drop[Drop<@TraitClause0::Item>] i@1 @0 := () return } @@ -158,7 +171,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(@TraitClause0::Item)> for closure[@TraitClause0]}::call_mut<'_, Self>[@TraitClause0](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0]>] @1 @0 := () return } diff --git a/charon/tests/ui/simple/conditional-drop.out b/charon/tests/ui/simple/conditional-drop.out index dbbe69f1d..ca8f52d2d 100644 --- a/charon/tests/ui/simple/conditional-drop.out +++ b/charon/tests/ui/simple/conditional-drop.out @@ -1,21 +1,69 @@ # Final LLBC before serialization: -// Full name: alloc::string::String -#[lang_item("String")] -pub opaque type String +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized -// Full name: alloc::string::{String}::new -#[lang_item("string_new")] -pub fn new() -> String +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: alloc::alloc::Global +#[lang_item("global_alloc_ty")] +pub struct Global {} + +// Full name: alloc::alloc::Global::{impl Drop for Global}::drop +fn {impl Drop for Global}::drop<'_0>(@1: &'_0 mut (Global)) + +// Full name: alloc::alloc::Global::{impl Drop for Global} +impl Drop for Global { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for Global}::drop<'_0_0> +} + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + [@TraitClause3]: Drop, + [@TraitClause4]: Drop, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + [@TraitClause3]: Drop, + [@TraitClause4]: Drop, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4] +} -// Full name: test_crate::use_string -fn use_string(@1: String) +// Full name: test_crate::use_box +fn use_box(@1: alloc::boxed::Box[MetaSized, Sized, Drop, {impl Drop for Global}]) { let @0: (); // return - let @1: String; // arg #1 + let @1: alloc::boxed::Box[MetaSized, Sized, Drop, {impl Drop for Global}]; // arg #1 @0 := () - drop @1 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}[MetaSized, Sized, Drop, {impl Drop for Global}]] @1 @0 := () return } @@ -24,27 +72,27 @@ fn use_string(@1: String) fn main() { let @0: (); // return - let s@1: String; // local + let b@1: alloc::boxed::Box[MetaSized, Sized, Drop, {impl Drop for Global}]; // local let @2: bool; // anonymous local let @3: (); // anonymous local - let @4: String; // anonymous local + let @4: alloc::boxed::Box[MetaSized, Sized, Drop, {impl Drop for Global}]; // anonymous local let @5: bool; // anonymous local storage_live(@3) storage_live(@4) storage_live(@5) @5 := const (false) - storage_live(s@1) + storage_live(b@1) @5 := const (true) - s@1 := new() + b@1 := @BoxNew[Sized, Drop](const (1 : u32)) storage_live(@2) @2 := const (false) if move (@2) { storage_live(@3) storage_live(@4) @5 := const (false) - @4 := move (s@1) - @3 := use_string(move (@4)) + @4 := move (b@1) + @3 := use_box(move (@4)) storage_dead(@4) storage_dead(@3) @0 := () @@ -53,14 +101,14 @@ fn main() @0 := () } storage_dead(@2) - // `s` is dropped implicitly here + // `b` is dropped implicitly here if copy (@5) { - drop s@1 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}[MetaSized, Sized, Drop, {impl Drop for Global}]] b@1 } else { } @5 := const (false) - storage_dead(s@1) + storage_dead(b@1) @0 := () return } diff --git a/charon/tests/ui/simple/conditional-drop.rs b/charon/tests/ui/simple/conditional-drop.rs index 7a211f9e4..cd3c13a90 100644 --- a/charon/tests/ui/simple/conditional-drop.rs +++ b/charon/tests/ui/simple/conditional-drop.rs @@ -1,10 +1,11 @@ //@ charon-args=--mir=elaborated -fn use_string(_: String) {} +//@ charon-args=--add-drop-bounds +fn use_box(_: Box) {} fn main() { - let s = String::new(); + let b = Box::new(1u32); if false { - use_string(s); + use_box(b); } - // `s` is dropped implicitly here + // `b` is dropped implicitly here } diff --git a/charon/tests/ui/simple/drop-string.out b/charon/tests/ui/simple/drop-string.out new file mode 100644 index 000000000..980ff73d2 --- /dev/null +++ b/charon/tests/ui/simple/drop-string.out @@ -0,0 +1,126 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: alloc::alloc::Global +#[lang_item("global_alloc_ty")] +pub struct Global {} + +// Full name: alloc::alloc::Global::{impl Drop for Global}::drop +fn {impl Drop for Global}::drop<'_0>(@1: &'_0 mut (Global)) + +// Full name: alloc::alloc::Global::{impl Drop for Global} +impl Drop for Global { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for Global}::drop<'_0_0> +} + +// Full name: alloc::vec::Vec +#[lang_item("Vec")] +pub opaque type Vec +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + [@TraitClause3]: Drop, + [@TraitClause4]: Drop, + +// Full name: alloc::string::String +#[lang_item("String")] +pub struct String { + vec: Vec[Sized, Sized, Drop, {impl Drop for Global}], +} + +// 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 + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + [@TraitClause3]: Drop, + [@TraitClause4]: Drop, + +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]} +impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, + [@TraitClause3]: Drop, + [@TraitClause4]: Drop, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]> + fn drop<'_0> = {impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4] +} + +// Full name: alloc::string::String::{impl Drop for String}::drop +fn {impl Drop for String}::drop<'_0>(@1: &'_0 mut (String)) +{ + let @0: (); // return + let @1: *mut String; // arg #1 + let @2: &'_ mut (String); // anonymous local + + storage_live(@2) + @2 := &mut *(@1) + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}[Sized, Sized, Drop, {impl Drop for Global}]] (*(@2)).vec + @0 := () + return +} + +// Full name: alloc::string::String::{impl Drop for String} +impl Drop for String { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for String}::drop<'_0_0> +} + +// Full name: alloc::string::{String}::new +#[lang_item("string_new")] +pub fn new() -> String + +// Full name: test_crate::use_string +fn use_string(@1: String) +{ + let @0: (); // return + let @1: String; // arg #1 + + @0 := () + drop[{impl Drop for String}] @1 + @0 := () + return +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let _s@1: String; // local + + storage_live(_s@1) + _s@1 := new() + @0 := () + drop[{impl Drop for String}] _s@1 + storage_dead(_s@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/drop-string.rs b/charon/tests/ui/simple/drop-string.rs new file mode 100644 index 000000000..46814f134 --- /dev/null +++ b/charon/tests/ui/simple/drop-string.rs @@ -0,0 +1,8 @@ +//@ charon-args=--mir=elaborated +//@ charon-args=--add-drop-bounds +//@ charon-args=--include=alloc::string::String +fn use_string(_: String) {} + +fn main() { + let _s = String::new(); +} diff --git a/charon/tests/ui/simple/hide-drops.out b/charon/tests/ui/simple/hide-drops.out new file mode 100644 index 000000000..2d47957bc --- /dev/null +++ b/charon/tests/ui/simple/hide-drops.out @@ -0,0 +1,55 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: alloc::string::String +#[lang_item("String")] +pub opaque type String + +// Full name: alloc::string::{String}::new +#[lang_item("string_new")] +pub fn new() -> String + +// Full name: test_crate::use_string +fn use_string(@1: String) +{ + let @0: (); // return + let @1: String; // arg #1 + + @0 := () + drop[{impl#0}] @1 + @0 := () + return +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let _s@1: String; // local + + storage_live(_s@1) + _s@1 := new() + @0 := () + drop[{impl#0}] _s@1 + storage_dead(_s@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/hide-drops.rs b/charon/tests/ui/simple/hide-drops.rs new file mode 100644 index 000000000..1ffbb50b3 --- /dev/null +++ b/charon/tests/ui/simple/hide-drops.rs @@ -0,0 +1,6 @@ +//@ charon-arg=--exclude={impl core::ops::drop::Drop for _} +fn use_string(_: String) {} + +fn main() { + let _s = String::new(); +} 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 af3bf1b14..aa67e4a28 100644 --- a/charon/tests/ui/simple/method-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/method-with-assoc-type-constraint.out @@ -11,6 +11,19 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: test_crate::IntoIterator pub trait IntoIterator { @@ -42,7 +55,7 @@ where let iter@1: I; // arg #1 @0 := () - drop iter@1 + drop[Drop] iter@1 @0 := () return } diff --git a/charon/tests/ui/simple/multiple-promoteds.out b/charon/tests/ui/simple/multiple-promoteds.out index 7cf7e5edc..5afc93d29 100644 --- a/charon/tests/ui/simple/multiple-promoteds.out +++ b/charon/tests/ui/simple/multiple-promoteds.out @@ -39,18 +39,6 @@ pub fn core::ops::arith::Add::add(@1: Self, @2: Rhs) -> @TraitClause0 where [@TraitClause0]: Add, -// Full name: core::ops::arith::{impl Add for u32}::add -pub fn {impl Add for u32}::add(@1: u32, @2: u32) -> u32 - -// Full name: core::ops::arith::{impl Add for u32} -impl Add for u32 { - parent_clause0 = MetaSized - parent_clause1 = Sized - parent_clause2 = Sized - type Output = u32 - fn add = {impl Add for u32}::add -} - // 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 446e7951f..4ea8a807b 100644 --- a/charon/tests/ui/simple/nested-closure-trait-ref.out +++ b/charon/tests/ui/simple/nested-closure-trait-ref.out @@ -39,6 +39,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -203,7 +216,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]}::call_mut<'_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0, @TraitClause1]>] @1 return } diff --git a/charon/tests/ui/simple/nested-closure.out b/charon/tests/ui/simple/nested-closure.out index b6fa26d88..38306b601 100644 --- a/charon/tests/ui/simple/nested-closure.out +++ b/charon/tests/ui/simple/nested-closure.out @@ -39,6 +39,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -286,7 +299,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<()> for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::call_mut<'_, '_1, '_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]>] @1 return } @@ -361,7 +374,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (u32))> for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::call_mut<'_, '_1, '_2, '_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]>] @1 return } @@ -436,7 +449,7 @@ where storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(&'_ (u32))> for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::call_mut<'_, '_1, '_2, '_, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) - drop @1 + drop[Drop[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]>] @1 return } 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 b6e5967cf..f2bd21b0c 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 @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -84,7 +97,7 @@ where let @1: F; // arg #1 @0 := () - drop @1 + drop[Drop] @1 @0 := () return } diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out index b958409f7..a46e6d97e 100644 --- a/charon/tests/ui/simple/promoted-closure-no-warns.out +++ b/charon/tests/ui/simple/promoted-closure-no-warns.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -132,7 +145,7 @@ fn {impl FnOnce<(u32)> for closure}::call_once(@1: closure, @2: (u32)) -> u32 storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32)> for closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out index b958409f7..a46e6d97e 100644 --- a/charon/tests/ui/simple/promoted-closure.out +++ b/charon/tests/ui/simple/promoted-closure.out @@ -18,6 +18,19 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -132,7 +145,7 @@ fn {impl FnOnce<(u32)> for closure}::call_once(@1: closure, @2: (u32)) -> u32 storage_live(@3) @3 := &mut @1 @0 := {impl FnMut<(u32)> for closure}::call_mut<'_>(move (@3), move (@2)) - drop @1 + drop[Drop] @1 return } diff --git a/charon/tests/ui/simple/ptr-from-raw-parts.out b/charon/tests/ui/simple/ptr-from-raw-parts.out index 6335d07b8..da8df36b0 100644 --- a/charon/tests/ui/simple/ptr-from-raw-parts.out +++ b/charon/tests/ui/simple/ptr-from-raw-parts.out @@ -11,6 +11,228 @@ pub trait Sized parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::clone::Clone +#[lang_item("clone")] +pub trait Clone +{ + parent_clause0 : [@TraitClause0]: Sized + fn clone<'_0> = clone<'_0_0, Self>[Self] +} + +// Full name: core::clone::Clone::clone +#[lang_item("clone_fn")] +pub fn clone<'_0, Self>(@1: &'_0 (Self)) -> Self +where + [@TraitClause0]: Clone, + +// Full name: core::cmp::PartialEq +#[lang_item("eq")] +pub trait PartialEq +{ + fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>[Self] +} + +#[lang_item("cmp_partialeq_eq")] +pub fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +where + [@TraitClause0]: PartialEq, + +// Full name: core::cmp::Eq +#[lang_item("Eq")] +pub trait Eq +{ + parent_clause0 : [@TraitClause0]: PartialEq +} + +// Full name: core::cmp::Ordering +#[lang_item("Ordering")] +pub enum Ordering { + Less, + Equal, + Greater, +} + +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option +where + [@TraitClause0]: Sized, +{ + None, + Some(T), +} + +// Full name: core::cmp::PartialOrd +#[lang_item("partial_ord")] +pub trait PartialOrd +{ + parent_clause0 : [@TraitClause0]: PartialEq + fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>[Self] +} + +// Full name: core::cmp::Ord +#[lang_item("Ord")] +pub trait Ord +{ + parent_clause0 : [@TraitClause0]: Eq + parent_clause1 : [@TraitClause1]: PartialOrd + fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>[Self] +} + +#[lang_item("ord_cmp_method")] +pub fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> Ordering +where + [@TraitClause0]: Ord, + +#[lang_item("cmp_partialord_cmp")] +pub fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> Option[Sized] +where + [@TraitClause0]: PartialOrd, + +// Full name: core::cmp::impls::{impl PartialEq<()> for ()}::eq +pub fn {impl PartialEq<()> for ()}::eq<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> bool + +// Full name: core::cmp::impls::{impl PartialEq<()> for ()} +impl PartialEq<()> for () { + fn eq<'_0, '_1> = {impl PartialEq<()> for ()}::eq<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Eq for ()} +impl Eq for () { + parent_clause0 = {impl PartialEq<()> for ()} +} + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()}::partial_cmp +pub fn {impl PartialOrd<()> for ()}::partial_cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Option[Sized] + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()} +impl PartialOrd<()> for () { + parent_clause0 = {impl PartialEq<()> for ()} + fn partial_cmp<'_0, '_1> = {impl PartialOrd<()> for ()}::partial_cmp<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Ord for ()}::cmp +pub fn {impl Ord for ()}::cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Ordering + +// Full name: core::cmp::impls::{impl Ord for ()} +impl Ord for () { + parent_clause0 = {impl Eq for ()} + parent_clause1 = {impl PartialOrd<()> for ()} + fn cmp<'_0, '_1> = {impl Ord for ()}::cmp<'_0_0, '_0_1> +} + +// Full name: core::fmt::Error +pub struct Error {} + +// Full name: core::fmt::Formatter +#[lang_item("Formatter")] +pub opaque type Formatter<'a> +where + 'a : 'a, + +// Full name: core::result::Result +#[lang_item("Result")] +pub enum Result +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + Ok(T), + Err(E), +} + +// Full name: core::fmt::Debug +#[lang_item("Debug")] +pub trait Debug +{ + fn fmt<'_0, '_1, '_2> = core::fmt::Debug::fmt<'_0_0, '_0_1, '_0_2, Self>[Self] +} + +pub fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] +where + [@TraitClause0]: Debug, + +// Full name: core::fmt::{impl Debug for ()}::fmt +pub fn {impl Debug for ()}::fmt<'_0, '_1, '_2>(@1: &'_0 (()), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] + +// Full name: core::fmt::{impl Debug for ()} +impl Debug for () { + fn fmt<'_0, '_1, '_2> = {impl Debug for ()}::fmt<'_0_0, '_0_1, '_0_2> +} + +// Full name: core::hash::Hasher +pub trait Hasher +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn finish<'_0> = finish<'_0_0, Self>[Self] + fn write<'_0, '_1> = write<'_0_0, '_0_1, Self>[Self] +} + +// Full name: core::hash::Hash +#[lang_item("Hash")] +pub trait Hash +{ + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = core::hash::Hash::hash<'_0_0, '_0_1, Self, H>[Self, @TraitClause0_0, @TraitClause0_1] +} + +pub fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) +where + [@TraitClause0]: Hash, + [@TraitClause1]: Sized, + [@TraitClause2]: Hasher, + +// Full name: core::hash::Hasher::finish +pub fn finish<'_0, Self>(@1: &'_0 (Self)) -> u64 +where + [@TraitClause0]: Hasher, + +// Full name: core::hash::Hasher::write +pub fn write<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Slice)) +where + [@TraitClause0]: Hasher, + +// Full name: core::hash::impls::{impl Hash for ()}::hash +pub fn {impl Hash for ()}::hash<'_0, '_1, H>(@1: &'_0 (()), @2: &'_1 mut (H)) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Hasher, + +// Full name: core::hash::impls::{impl Hash for ()} +impl Hash for () { + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = {impl Hash for ()}::hash<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1] +} + +// Full name: core::marker::Send +#[lang_item("Send")] +pub trait Send + +// Full name: core::marker::Copy +#[lang_item("copy")] +pub trait Copy +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Clone +} + +// Full name: core::marker::Sync +#[lang_item("sync")] +pub trait Sync + +// Full name: core::marker::Freeze +#[lang_item("freeze")] +pub trait Freeze + +// Full name: core::marker::Unpin +#[lang_item("unpin")] +pub trait Unpin + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + // Full name: core::ptr::metadata::from_raw_parts pub fn from_raw_parts(@1: *const impl Thin, @2: Pointee::Metadata) -> *const T where diff --git a/charon/tests/ui/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out index e3e3979eb..2b6d729bf 100644 --- a/charon/tests/ui/simple/ptr_metadata.out +++ b/charon/tests/ui/simple/ptr_metadata.out @@ -29,12 +29,11 @@ where #[lang_item("eq")] pub trait PartialEq { - fn eq<'_0, '_1> = eq<'_0_0, '_0_1, Self, Rhs>[Self] + fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>[Self] } -// Full name: core::cmp::PartialEq::eq #[lang_item("cmp_partialeq_eq")] -pub fn eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +pub fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool where [@TraitClause0]: PartialEq, @@ -68,7 +67,7 @@ where pub trait PartialOrd { parent_clause0 : [@TraitClause0]: PartialEq - fn partial_cmp<'_0, '_1> = partial_cmp<'_0_0, '_0_1, Self, Rhs>[Self] + fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>[Self] } // Full name: core::cmp::Ord @@ -77,21 +76,51 @@ pub trait Ord { parent_clause0 : [@TraitClause0]: Eq parent_clause1 : [@TraitClause1]: PartialOrd - fn cmp<'_0, '_1> = cmp<'_0_0, '_0_1, Self>[Self] + fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>[Self] } -// Full name: core::cmp::Ord::cmp #[lang_item("ord_cmp_method")] -pub fn cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> Ordering +pub fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> Ordering where [@TraitClause0]: Ord, -// Full name: core::cmp::PartialOrd::partial_cmp #[lang_item("cmp_partialord_cmp")] -pub fn partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> Option[Sized] +pub fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> Option[Sized] where [@TraitClause0]: PartialOrd, +// Full name: core::cmp::impls::{impl PartialEq<()> for ()}::eq +pub fn {impl PartialEq<()> for ()}::eq<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> bool + +// Full name: core::cmp::impls::{impl PartialEq<()> for ()} +impl PartialEq<()> for () { + fn eq<'_0, '_1> = {impl PartialEq<()> for ()}::eq<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Eq for ()} +impl Eq for () { + parent_clause0 = {impl PartialEq<()> for ()} +} + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()}::partial_cmp +pub fn {impl PartialOrd<()> for ()}::partial_cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Option[Sized] + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()} +impl PartialOrd<()> for () { + parent_clause0 = {impl PartialEq<()> for ()} + fn partial_cmp<'_0, '_1> = {impl PartialOrd<()> for ()}::partial_cmp<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Ord for ()}::cmp +pub fn {impl Ord for ()}::cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Ordering + +// Full name: core::cmp::impls::{impl Ord for ()} +impl Ord for () { + parent_clause0 = {impl Eq for ()} + parent_clause1 = {impl PartialOrd<()> for ()} + fn cmp<'_0, '_1> = {impl Ord for ()}::cmp<'_0_0, '_0_1> +} + // Full name: core::fmt::Error pub struct Error {} @@ -116,14 +145,21 @@ where #[lang_item("Debug")] pub trait Debug { - fn fmt<'_0, '_1, '_2> = fmt<'_0_0, '_0_1, '_0_2, Self>[Self] + fn fmt<'_0, '_1, '_2> = core::fmt::Debug::fmt<'_0_0, '_0_1, '_0_2, Self>[Self] } -// Full name: core::fmt::Debug::fmt -pub fn fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] +pub fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] where [@TraitClause0]: Debug, +// Full name: core::fmt::{impl Debug for ()}::fmt +pub fn {impl Debug for ()}::fmt<'_0, '_1, '_2>(@1: &'_0 (()), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] + +// Full name: core::fmt::{impl Debug for ()} +impl Debug for () { + fn fmt<'_0, '_1, '_2> = {impl Debug for ()}::fmt<'_0_0, '_0_1, '_0_2> +} + // Full name: core::hash::Hasher pub trait Hasher { @@ -136,11 +172,10 @@ pub trait Hasher #[lang_item("Hash")] pub trait Hash { - fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = hash<'_0_0, '_0_1, Self, H>[Self, @TraitClause0_0, @TraitClause0_1] + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = core::hash::Hash::hash<'_0_0, '_0_1, Self, H>[Self, @TraitClause0_0, @TraitClause0_1] } -// Full name: core::hash::Hash::hash -pub fn hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) +pub fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) where [@TraitClause0]: Hash, [@TraitClause1]: Sized, @@ -156,6 +191,17 @@ pub fn write<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Slice)) where [@TraitClause0]: Hasher, +// Full name: core::hash::impls::{impl Hash for ()}::hash +pub fn {impl Hash for ()}::hash<'_0, '_1, H>(@1: &'_0 (()), @2: &'_1 mut (H)) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Hasher, + +// Full name: core::hash::impls::{impl Hash for ()} +impl Hash for () { + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = {impl Hash for ()}::hash<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1] +} + // Full name: core::marker::Send #[lang_item("Send")] pub trait Send diff --git a/charon/tests/ui/simple/trait-alias.out b/charon/tests/ui/simple/trait-alias.out index d5d671287..d1a3415fa 100644 --- a/charon/tests/ui/simple/trait-alias.out +++ b/charon/tests/ui/simple/trait-alias.out @@ -31,6 +31,19 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::option::Option #[lang_item("Option")] pub enum Option @@ -117,10 +130,10 @@ where @3 := &x@1 @2 := @TraitClause1::parent_clause2::clone<'_>(move (@3)) storage_dead(@3) - drop @2 + drop[Drop] @2 storage_dead(@2) @0 := () - drop x@1 + drop[Drop] x@1 @0 := () return } diff --git a/charon/tests/ui/simple/vec-push.out b/charon/tests/ui/simple/vec-push.out index e136703d7..bc78e9122 100644 --- a/charon/tests/ui/simple/vec-push.out +++ b/charon/tests/ui/simple/vec-push.out @@ -14,6 +14,19 @@ pub trait Sized // Full name: core::num::niche_types::UsizeNoHighBit pub opaque type UsizeNoHighBit +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ptr::non_null::NonNull #[lang_item("NonNull")] pub opaque type NonNull diff --git a/charon/tests/ui/simple/vec-with-capacity.out b/charon/tests/ui/simple/vec-with-capacity.out index 8337847b6..0fe02feea 100644 --- a/charon/tests/ui/simple/vec-with-capacity.out +++ b/charon/tests/ui/simple/vec-with-capacity.out @@ -66,6 +66,30 @@ where const MAX_SLICE_LEN = core::mem::SizedTypeProperties::MAX_SLICE_LEN[{impl SizedTypeProperties for T}[@TraitClause0]] } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) + +// Full name: core::ptr::non_null::NonNull +#[lang_item("NonNull")] +pub opaque type NonNull + +// Full name: core::ptr::unique::Unique +#[lang_item("ptr_unique")] +pub opaque type Unique + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} @@ -124,6 +148,46 @@ where return } +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (Vec[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + let @0: (); // return + let self@1: &'_ mut (Vec[@TraitClause0, @TraitClause1]); // arg #1 + let @2: *mut Slice; // anonymous local + let data@3: *mut T; // local + let len@4: usize; // local + let @5: NonNull; // anonymous local + + storage_live(@2) + storage_live(data@3) + storage_live(@5) + @5 := copy (((((*(self@1)).buf).0).0).0) + data@3 := transmute, *mut T>(copy (@5)) + storage_dead(@5) + storage_live(len@4) + len@4 := copy ((*(self@1)).len) + @2 := @PtrFromPartsMut<'_, Slice>(copy (data@3), copy (len@4)) + storage_dead(len@4) + storage_dead(data@3) + @0 := drop_in_place>(move (@2)) + storage_dead(@2) + @0 := () + return +} + +// Full name: alloc::vec::{impl Drop for Vec[@TraitClause0, @TraitClause1]} +impl Drop for Vec[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: Sized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Vec[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: test_crate::vec fn vec() { @@ -132,7 +196,7 @@ fn vec() storage_live(@1) @1 := with_capacity[Sized](const (42 : usize)) - drop @1 + drop[{impl Drop for Vec[@TraitClause0, @TraitClause1]}[Sized, Sized]] @1 storage_dead(@1) @0 := () @0 := () diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index 84975d6e4..44c5985d1 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -50,10 +50,31 @@ impl Display for Str { fn fmt<'_0, '_1, '_2> = {impl Display for Str}::fmt<'_0_0, '_0_1, '_0_2> } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::string::String #[lang_item("String")] pub opaque type String +// Full name: alloc::string::String::{impl Drop for String}::drop +fn {impl Drop for String}::drop<'_0>(@1: &'_0 mut (String)) + +// Full name: alloc::string::String::{impl Drop for String} +impl Drop for String { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for String}::drop<'_0_0> +} + // Full name: alloc::string::ToString #[lang_item("ToString")] pub trait ToString @@ -134,7 +155,7 @@ fn main() storage_dead(@2) storage_dead(@3) @0 := () - drop _s@1 + drop[{impl Drop for String}] _s@1 storage_dead(_s@1) @0 := () return diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 7e02a2ce9..16f0e69fa 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -18,6 +18,18 @@ pub trait Tuple parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -74,6 +86,20 @@ where Some(T), } +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]}::drop +fn {impl Drop for Option[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (Option[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: core::option::Option::{impl Drop for Option[@TraitClause0]} +impl Drop for Option[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for Option[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: core::result::Result #[lang_item("Result")] pub enum Result @@ -237,7 +263,7 @@ where @0 := const (false) } storage_dead(@2) - drop x@1 + drop[{impl Drop for Option[@TraitClause0]}[@TraitClause0]] x@1 return } @@ -255,7 +281,7 @@ where @2 := &x@1 @0 := @TraitClause1::get_bool<'_>(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop] x@1 return } @@ -315,7 +341,7 @@ where @0 := move (@6) storage_dead(@4) storage_dead(@2) - drop self@1 + drop[Drop<(A, A)>] self@1 return } @@ -342,7 +368,7 @@ where @2 := move (x@1) @0 := {impl ToU64 for (A, A)}::to_u64[@TraitClause0, @TraitClause1](move (@2)) storage_dead(@2) - drop x@1 + drop[Drop<(T, T)>] x@1 return } @@ -360,7 +386,7 @@ where @2 := move (x@1) @0 := @TraitClause1::to_u64(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop<(T, T)>] x@1 return } @@ -386,6 +412,20 @@ where x: T, } +// Full name: test_crate::Wrapper::{impl Drop for Wrapper[@TraitClause0]}::drop +fn {impl Drop for Wrapper[@TraitClause0]}::drop<'_0, T>(@1: &'_0 mut (Wrapper[@TraitClause0])) +where + [@TraitClause0]: Sized, + +// Full name: test_crate::Wrapper::{impl Drop for Wrapper[@TraitClause0]} +impl Drop for Wrapper[@TraitClause0] +where + [@TraitClause0]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0]> + fn drop<'_0> = {impl Drop for Wrapper[@TraitClause0]}::drop<'_0_0, T>[@TraitClause0] +} + // Full name: test_crate::{impl ToU64 for Wrapper[@TraitClause0]}::to_u64 pub fn {impl ToU64 for Wrapper[@TraitClause0]}::to_u64(@1: Wrapper[@TraitClause0]) -> u64 where @@ -400,7 +440,7 @@ where @2 := move ((self@1).x) @0 := @TraitClause1::to_u64(move (@2)) storage_dead(@2) - drop self@1 + drop[{impl Drop for Wrapper[@TraitClause0]}[@TraitClause0]] self@1 return } @@ -442,7 +482,7 @@ where @2 := move (x@1) @0 := {impl ToU64 for Wrapper[@TraitClause0]}::to_u64[@TraitClause0, @TraitClause1](move (@2)) storage_dead(@2) - drop x@1 + drop[{impl Drop for Wrapper[@TraitClause0]}[@TraitClause0]] x@1 return } @@ -509,7 +549,7 @@ where @2 := move (y@1) @0 := @TraitClause2::of_type[@TraitClause1, @TraitClause3, @TraitClause0](move (@2)) storage_dead(@2) - drop y@1 + drop[Drop] y@1 return } @@ -544,7 +584,7 @@ where @2 := move (y@1) @0 := @TraitClause2::of_type[@TraitClause0](move (@2)) storage_dead(@2) - drop y@1 + drop[Drop] y@1 return } @@ -621,7 +661,7 @@ where storage_dead(@6) storage_dead(y@5) storage_dead(x@3) - drop x@2 + drop[Drop] x@2 return } @@ -767,7 +807,7 @@ where let @1: @TraitClause1::W; // arg #1 @0 := () - drop @1 + drop[Drop<@TraitClause1::W>] @1 @0 := () return } @@ -786,7 +826,7 @@ where @2 := move (x@1) @0 := @TraitClause1::parent_clause3::to_u64(move (@2)) storage_dead(@2) - drop x@1 + drop[Drop<@TraitClause1::W>] x@1 return } @@ -1265,7 +1305,7 @@ where let @1: F; // arg #1 @0 := () - drop @1 + drop[Drop] @1 @0 := () return } diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out index 24f41f607..96eb0a786 100644 --- a/charon/tests/ui/type_inference_is_order_dependent.out +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -91,6 +91,19 @@ where // 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> +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: std::io::stdio::_print pub fn _print<'_0>(@1: Arguments<'_0>) @@ -176,7 +189,7 @@ where storage_dead(@8) @1 := _print<'_>(move (@2)) storage_dead(@2) - drop @7 + drop[Drop] @7 storage_dead(@7) storage_dead(@6) storage_dead(args@3) diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 9ab35b558..64a3dae6a 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -29,12 +29,11 @@ where #[lang_item("eq")] pub trait PartialEq { - fn eq<'_0, '_1> = eq<'_0_0, '_0_1, Self, Rhs>[Self] + fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>[Self] } -// Full name: core::cmp::PartialEq::eq #[lang_item("cmp_partialeq_eq")] -pub fn eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +pub fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool where [@TraitClause0]: PartialEq, @@ -68,7 +67,7 @@ where pub trait PartialOrd { parent_clause0 : [@TraitClause0]: PartialEq - fn partial_cmp<'_0, '_1> = partial_cmp<'_0_0, '_0_1, Self, Rhs>[Self] + fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>[Self] } // Full name: core::cmp::Ord @@ -77,21 +76,51 @@ pub trait Ord { parent_clause0 : [@TraitClause0]: Eq parent_clause1 : [@TraitClause1]: PartialOrd - fn cmp<'_0, '_1> = cmp<'_0_0, '_0_1, Self>[Self] + fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>[Self] } -// Full name: core::cmp::Ord::cmp #[lang_item("ord_cmp_method")] -pub fn cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> Ordering +pub fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> Ordering where [@TraitClause0]: Ord, -// Full name: core::cmp::PartialOrd::partial_cmp #[lang_item("cmp_partialord_cmp")] -pub fn partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> Option[Sized] +pub fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> Option[Sized] where [@TraitClause0]: PartialOrd, +// Full name: core::cmp::impls::{impl PartialEq<()> for ()}::eq +pub fn {impl PartialEq<()> for ()}::eq<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> bool + +// Full name: core::cmp::impls::{impl PartialEq<()> for ()} +impl PartialEq<()> for () { + fn eq<'_0, '_1> = {impl PartialEq<()> for ()}::eq<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Eq for ()} +impl Eq for () { + parent_clause0 = {impl PartialEq<()> for ()} +} + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()}::partial_cmp +pub fn {impl PartialOrd<()> for ()}::partial_cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Option[Sized] + +// Full name: core::cmp::impls::{impl PartialOrd<()> for ()} +impl PartialOrd<()> for () { + parent_clause0 = {impl PartialEq<()> for ()} + fn partial_cmp<'_0, '_1> = {impl PartialOrd<()> for ()}::partial_cmp<'_0_0, '_0_1> +} + +// Full name: core::cmp::impls::{impl Ord for ()}::cmp +pub fn {impl Ord for ()}::cmp<'_0, '_1>(@1: &'_0 (()), @2: &'_1 (())) -> Ordering + +// Full name: core::cmp::impls::{impl Ord for ()} +impl Ord for () { + parent_clause0 = {impl Eq for ()} + parent_clause1 = {impl PartialOrd<()> for ()} + fn cmp<'_0, '_1> = {impl Ord for ()}::cmp<'_0_0, '_0_1> +} + // Full name: core::fmt::Error pub struct Error {} @@ -116,14 +145,21 @@ where #[lang_item("Debug")] pub trait Debug { - fn fmt<'_0, '_1, '_2> = fmt<'_0_0, '_0_1, '_0_2, Self>[Self] + fn fmt<'_0, '_1, '_2> = core::fmt::Debug::fmt<'_0_0, '_0_1, '_0_2, Self>[Self] } -// Full name: core::fmt::Debug::fmt -pub fn fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] +pub fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] where [@TraitClause0]: Debug, +// Full name: core::fmt::{impl Debug for ()}::fmt +pub fn {impl Debug for ()}::fmt<'_0, '_1, '_2>(@1: &'_0 (()), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] + +// Full name: core::fmt::{impl Debug for ()} +impl Debug for () { + fn fmt<'_0, '_1, '_2> = {impl Debug for ()}::fmt<'_0_0, '_0_1, '_0_2> +} + // Full name: core::hash::Hasher pub trait Hasher { @@ -136,11 +172,10 @@ pub trait Hasher #[lang_item("Hash")] pub trait Hash { - fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = hash<'_0_0, '_0_1, Self, H>[Self, @TraitClause0_0, @TraitClause0_1] + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = core::hash::Hash::hash<'_0_0, '_0_1, Self, H>[Self, @TraitClause0_0, @TraitClause0_1] } -// Full name: core::hash::Hash::hash -pub fn hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) +pub fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) where [@TraitClause0]: Hash, [@TraitClause1]: Sized, @@ -156,6 +191,17 @@ pub fn write<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Slice)) where [@TraitClause0]: Hasher, +// Full name: core::hash::impls::{impl Hash for ()}::hash +pub fn {impl Hash for ()}::hash<'_0, '_1, H>(@1: &'_0 (()), @2: &'_1 mut (H)) +where + [@TraitClause0]: Sized, + [@TraitClause1]: Hasher, + +// Full name: core::hash::impls::{impl Hash for ()} +impl Hash for () { + fn hash<'_0, '_1, H, [@TraitClause0]: Sized, [@TraitClause1]: Hasher> = {impl Hash for ()}::hash<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1] +} + pub unsafe fn core::intrinsics::assume(@1: bool) // Full name: core::marker::Send diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index 23e2502c9..93522452f 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -31,10 +31,38 @@ pub trait Destruct parent_clause0 : [@TraitClause0]: MetaSized } +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = core::ops::drop::Drop::drop<'_0_0, Self>[Self] +} + +pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::boxed::{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]} +impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: alloc::rc::Rc #[lang_item("Rc")] pub opaque type Rc @@ -46,10 +74,35 @@ pub fn alloc::rc::{Rc[@TraitClause0::parent_clause0, Sized]}: where [@TraitClause0]: Sized, +// Full name: alloc::rc::{impl Drop for Rc[@TraitClause0, @TraitClause1]}::drop +pub fn {impl Drop for Rc[@TraitClause0, @TraitClause1]}::drop<'_0, T, A>(@1: &'_0 mut (Rc[@TraitClause0, @TraitClause1])) +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, + +// Full name: alloc::rc::{impl Drop for Rc[@TraitClause0, @TraitClause1]} +impl Drop for Rc[@TraitClause0, @TraitClause1] +where + [@TraitClause0]: MetaSized, + [@TraitClause1]: Sized, +{ + parent_clause0 = MetaSized[@TraitClause0, @TraitClause1]> + fn drop<'_0> = {impl Drop for Rc[@TraitClause0, @TraitClause1]}::drop<'_0_0, T, A>[@TraitClause0, @TraitClause1] +} + // Full name: alloc::string::String #[lang_item("String")] pub opaque type String +// Full name: alloc::string::String::{impl Drop for String}::drop +fn {impl Drop for String}::drop<'_0>(@1: &'_0 mut (String)) + +// Full name: alloc::string::String::{impl Drop for String} +impl Drop for String { + parent_clause0 = MetaSized + fn drop<'_0> = {impl Drop for String}::drop<'_0_0> +} + #[lang_item("string_new")] pub fn alloc::string::{String}::new() -> String @@ -106,10 +159,10 @@ fn foo() @7 := copy (array@1) @6 := @BoxNew>[Sized>](move (@7)) @5 := unsize_cast>[MetaSized>, Sized], alloc::boxed::Box>[MetaSized>, Sized]>(move (@6)) - drop @6 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @6 storage_dead(@7) storage_dead(@6) - drop @5 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @5 storage_dead(@5) storage_live(@8) storage_live(@9) @@ -117,10 +170,10 @@ fn foo() @10 := copy (array@1) @9 := alloc::rc::{Rc[@TraitClause0::parent_clause0, Sized]}::new>[Sized>](move (@10)) @8 := unsize_cast, Global>[MetaSized>, Sized], Rc, Global>[MetaSized>, Sized]>(move (@9)) - drop @9 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @9 storage_dead(@10) storage_dead(@9) - drop @8 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}, Global>[MetaSized>, Sized]] @8 storage_dead(@8) storage_live(string@11) string@11 := alloc::string::{String}::new() @@ -142,10 +195,10 @@ fn foo() storage_dead(@18) @16 := @BoxNew[Sized](move (@17)) @15 := unsize_cast[MetaSized, Sized], alloc::boxed::Box[MetaSized, Sized]>(move (@16)) - drop @16 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @16 storage_dead(@17) storage_dead(@16) - drop @15 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @15 storage_dead(@15) storage_live(@19) storage_live(@20) @@ -156,13 +209,13 @@ fn foo() storage_dead(@22) @20 := alloc::rc::{Rc[@TraitClause0::parent_clause0, Sized]}::new[Sized](move (@21)) @19 := unsize_cast[MetaSized, Sized], Rc[MetaSized, Sized]>(move (@20)) - drop @20 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @20 storage_dead(@21) storage_dead(@20) - drop @19 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @19 storage_dead(@19) @0 := () - drop string@11 + drop[{impl Drop for String}] string@11 storage_dead(string@11) storage_dead(array@1) @0 := ()