diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 9291ba347..d796c1d49 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -529,11 +529,70 @@ impl BodyTransCtx<'_, '_, '_> { ), ); } - // TODO(dyn): more ways of registering vtable instance? - _ => { - trace!( - "impl_expr not triggering registering vtable: {:?}", - impl_expr + hax::ImplExprAtom::Builtin { .. } => { + // Handle built-in implementations, including closures + let tref = &impl_expr.r#trait; + let hax_state = self.hax_state_with_id().clone(); + let trait_def = self.hax_def( + &tref.hax_skip_binder_ref().erase(&hax_state), + )?; + let closure_kind = + trait_def.lang_item.as_deref().and_then(|lang| { + match lang { + "fn_once" => Some(ClosureKind::FnOnce), + "fn_mut" => Some(ClosureKind::FnMut), + "fn" | "r#fn" => Some(ClosureKind::Fn), + _ => None, + } + }); + + // Check if this is a closure trait implementation + if let Some(closure_kind) = closure_kind + && let Some(hax::GenericArg::Type(closure_ty)) = + impl_expr + .r#trait + .hax_skip_binder_ref() + .generic_args + .first() + && let hax::TyKind::Closure(closure_args) = + closure_ty.kind() + { + // Register the closure vtable instance + let _: GlobalDeclId = self.register_item( + span, + &closure_args.item, + TransItemSourceKind::VTableInstance( + TraitImplSource::Closure(closure_kind), + ), + ); + } else { + raise_error!( + self.i_ctx, + span, + "Handle non-closure virtual trait implementations." + ); + } + } + hax::ImplExprAtom::LocalBound { .. } => { + // No need to register anything here as there is no concrete impl + // This results in that: the vtable instance in generic case might not exist + // But this case should not happen in the monomorphized case + if self.monomorphize() { + raise_error!( + self.i_ctx, + span, + "Unexpected `LocalBound` in monomorphized context" + ) + } + } + hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => { + // No need to register anything for these cases + } + hax::ImplExprAtom::SelfImpl { .. } => { + raise_error!( + self.i_ctx, + span, + "`SelfImpl` should not appear in the function body" ) } }; diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index dfa4895a6..ec03d9b7f 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -283,7 +283,7 @@ impl ItemTransCtx<'_, '_> { /// Given an item that is a closure, generate the signature of the /// `call_once`/`call_mut`/`call` method (depending on `target_kind`). - fn translate_closure_method_sig( + pub fn translate_closure_method_sig( &mut self, def: &hax::FullDef, span: Span, diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 628c26b89..b47d90712 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -76,7 +76,7 @@ pub enum TransItemSourceKind { /// Shim function to store a method in a vtable; give a method with `self: Ptr` argument, /// this takes a `Ptr` and forwards to the method. The `DefId` refers to the method /// implementation. - VTableMethod, + VTableMethod(TraitImplSource), } /// The kind of a [`TransItemSourceKind::TraitImpl`]. @@ -293,7 +293,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { | EmptyDropMethod | DropInPlaceMethod(..) | VTableInstanceInitializer(..) - | VTableMethod => ItemId::Fun(self.translated.fun_decls.reserve_slot()), + | VTableMethod(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()), InherentImpl | Module => return None, }; // Add the id to the queue of declarations to translate diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 109f09268..d02aa9179 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -175,11 +175,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?; self.translated.fun_decls.set_slot(id, fun_decl); } - TransItemSourceKind::VTableMethod => { + TransItemSourceKind::VTableMethod(impl_kind) => { let Some(ItemId::Fun(id)) = trans_id else { unreachable!() }; - let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?; + let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?; self.translated.fun_decls.set_slot(id, fun_decl); } } diff --git a/charon/src/bin/charon-driver/translate/translate_meta.rs b/charon/src/bin/charon-driver/translate/translate_meta.rs index ec47cf9cb..5b6995c62 100644 --- a/charon/src/bin/charon-driver/translate/translate_meta.rs +++ b/charon/src/bin/charon-driver/translate/translate_meta.rs @@ -368,7 +368,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { name.name .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO)); } - TransItemSourceKind::VTableMethod => { + TransItemSourceKind::VTableMethod(..) => { name.name.push(PathElem::Ident( "{vtable_method}".into(), Disambiguator::ZERO, diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index 383652101..03d104080 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,6 +1,6 @@ use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use itertools::Itertools; -use std::mem; +use std::{mem, vec}; use super::{ translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel, @@ -252,6 +252,20 @@ impl ItemTransCtx<'_, '_> { else { return Ok(()); }; + // The `FnOnce::call_once` is not compatible with the dyn-compatibility as described in: + // https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility + // But the Rustc offers a special backdoor for this and allows this method to be `vtable_safe`. + // The only way to call such a function seems to be with `Box`. + // The implementation of `Box::call_once` is a special case and should translate specially with some special magic. + // TODO(ssyram): in the future we may implement the function with type `fn call_once(self: Box, Args) -> Output` + // This function is the vtable-specific version of the `call_once` method. + // A very special case that the type signature differs from the original signature. + // Anyway, if we allow this to happen, there will be a severe breakage in that we can perform concretization on `dyn FnOnce`, + // This will make the life in backend tools, especially Eurydice much harder. + // Likewise, we skip translation of the `call_once` method below in the instance. + if trait_def.lang_item == Some("fn_once".into()) { + return Ok(()); + } let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?; // It's ok to translate the method signature in the context of the trait because @@ -518,22 +532,49 @@ impl ItemTransCtx<'_, '_> { fn get_vtable_instance_info<'a>( &mut self, span: Span, - impl_def: &'a hax::FullDef, + def: &'a hax::FullDef, impl_kind: &TraitImplSource, - ) -> Result<(TraitImplRef, TypeDeclRef), Error> { - let implemented_trait = match impl_def.kind() { - hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref, - _ => unreachable!(), + ) -> Result<(TraitImplRef, TraitDeclRef, TypeDeclRef), Error> { + let (implemented_trait, impl_ref) = match def.kind() { + hax::FullDefKind::TraitImpl { trait_pred, .. } => ( + &trait_pred.trait_ref, + self.translate_item(span, def.this(), TransItemSourceKind::TraitImpl(*impl_kind))?, + ), + hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + args, + .. + } => { + // For closures, get the trait implementation based on the closure kind + let closure_trait_impl = match impl_kind { + TraitImplSource::Closure(ClosureKind::FnOnce) => fn_once_impl, + TraitImplSource::Closure(ClosureKind::FnMut) => { + fn_mut_impl.as_ref().expect("FnMut impl should exist") + } + TraitImplSource::Closure(ClosureKind::Fn) => { + fn_impl.as_ref().expect("Fn impl should exist") + } + _ => unreachable!("Expected closure trait impl source"), + }; + let target_kind = match impl_kind { + TraitImplSource::Closure(kind) => *kind, + _ => unreachable!(), + }; + ( + &closure_trait_impl.trait_pred.trait_ref, + self.translate_closure_bound_impl_ref(span, args, target_kind)? + .erase(), + ) + } + _ => panic!("Unknown type of impl full def: {:?}", def.kind()), }; let vtable_struct_ref = self .translate_vtable_struct_ref(span, implemented_trait)? .expect("trait should be dyn-compatible"); - let impl_ref = self.translate_item( - span, - impl_def.this(), - TransItemSourceKind::TraitImpl(*impl_kind), - )?; - Ok((impl_ref, vtable_struct_ref)) + let implemented_trait = self.translate_trait_decl_ref(span, implemented_trait)?; + Ok((impl_ref, implemented_trait, vtable_struct_ref)) } /// E.g., @@ -561,7 +602,7 @@ impl ItemTransCtx<'_, '_> { self.translate_def_generics(span, impl_def)?; self.check_no_monomorphize(span)?; - let (impl_ref, vtable_struct_ref) = + let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; // Initializer function for this global. let init = self.register_item( @@ -607,7 +648,11 @@ impl ItemTransCtx<'_, '_> { // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`. let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id); let shim_ref = self - .translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)? + .translate_fn_ptr( + span, + &item_ref, + TransItemSourceKind::VTableMethod(TraitImplSource::Normal), + )? .erase(); ConstantExprKind::FnPtr(shim_ref) } @@ -631,12 +676,29 @@ impl ItemTransCtx<'_, '_> { impl_def: &hax::FullDef, mut mk_field: impl FnMut(ConstantExprKind), ) -> Result<(), Error> { - let hax::FullDefKind::TraitImpl { - implied_impl_exprs, .. - } = impl_def.kind() - else { - unreachable!() + let implied_impl_exprs = match impl_def.kind() { + hax::FullDefKind::TraitImpl { + implied_impl_exprs, .. + } => implied_impl_exprs, + hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + .. + } => match trait_def.lang_item { + Some("fn") | Some("r#fn") => &fn_impl.as_ref().unwrap().implied_impl_exprs, + Some("fn_once") => &fn_once_impl.as_ref().implied_impl_exprs, + Some("fn_mut") => &fn_mut_impl.as_ref().unwrap().implied_impl_exprs, + _ => unreachable!(), + }, + kind => raise_error!(self, span, "TODO: Unknown type of impl full def: {kind:?}"), }; + // let hax::FullDefKind::TraitImpl { + // implied_impl_exprs, .. + // } = impl_def.kind() + // else { + // unreachable!() + // }; let hax::FullDefKind::Trait { implied_predicates, .. } = trait_def.kind() @@ -674,8 +736,118 @@ impl ItemTransCtx<'_, '_> { }); ConstantExprKind::Ref(global) } - // TODO(dyn): builtin impls - _ => ConstantExprKind::Opaque("missing supertrait vtable".into()), + hax::ImplExprAtom::Builtin { trait_data, .. } => { + // Handle built-in implementations, including closures + let tref = &impl_expr.r#trait; + let hax_state = self.hax_state_with_id(); + let trait_def = self.hax_def(&tref.hax_skip_binder_ref().erase(hax_state))?; + + trace!( + "Processing builtin impl for trait {:?}, lang_item: {:?}, trait_data: {:?}", + trait_def.def_id(), + trait_def.lang_item, + trait_data + ); + + let closure_kind = trait_def.lang_item.as_deref().and_then(|lang| match lang { + "fn_once" => Some(ClosureKind::FnOnce), + "fn_mut" => Some(ClosureKind::FnMut), + "fn" | "r#fn" => Some(ClosureKind::Fn), + _ => None, + }); + + // Check if this is a closure trait implementation + if let Some(closure_kind) = closure_kind + && let Some(hax::GenericArg::Type(closure_ty)) = + impl_expr.r#trait.hax_skip_binder_ref().generic_args.first() + && let hax::TyKind::Closure(closure_args) = closure_ty.kind() + { + // Register the closure vtable instance + let vtable_instance_ref: GlobalDeclRef = self.translate_item( + span, + &closure_args.item, + TransItemSourceKind::VTableInstance(TraitImplSource::Closure( + closure_kind, + )), + )?; + let global = Box::new(ConstantExpr { + kind: ConstantExprKind::Global(vtable_instance_ref), + ty: fn_ptr_ty, + }); + ConstantExprKind::Ref(global) + } else if self + .translate_vtable_struct_ref(span, impl_expr.r#trait.hax_skip_binder_ref())? + .is_some() + { + // For other builtin traits that are dyn-compatible, try to create a vtable instance + trace!( + "Handling dyn-compatible builtin trait: {:?}", + trait_def.lang_item + ); + + // TODO(ssyram): for now, we don't know how to translate other kinds of built-in traits, just take their names + // The challenge is that we need an impl_ref, but builtin traits don't have concrete impls + // Let's try using the trait reference itself as the impl reference + // A simple case would be that they are all marker traits like `core::marker::MetaSized` + let trait_ref = impl_expr.r#trait.hax_skip_binder_ref(); + let mut vtable_instance_ref: GlobalDeclRef = self + .translate_item_no_enqueue( + span, + trait_ref, + TransItemSourceKind::VTableInstance( + TraitImplSource::Normal, // Builtin traits are normal impls + ), + )?; + // Remove the first `Self` argument + vtable_instance_ref + .generics + .types + .remove_and_shift_ids(TypeVarId::ZERO); + let global = Box::new(ConstantExpr { + kind: ConstantExprKind::Global(vtable_instance_ref), + ty: fn_ptr_ty, + }); + ConstantExprKind::Ref(global) + } else { + // For non-dyn-compatible builtin traits, we don't need vtable instances + trace!( + "Non-dyn-compatible builtin trait: {:?}", + trait_def.lang_item + ); + ConstantExprKind::Opaque( + format!( + "non-dyn-compatible builtin trait {:?}", + trait_def.lang_item.as_deref().unwrap_or("unknown") + ) + .into(), + ) + } + } + hax::ImplExprAtom::LocalBound { .. } => { + // No need to register anything here as there is no concrete impl + // This results in that: the vtable instance in generic case might not exist + // But this case should not happen in the monomorphized case + if self.monomorphize() { + raise_error!( + self, + span, + "Unexpected `LocalBound` in monomorphized context" + ) + } else { + ConstantExprKind::Opaque("generic supertrait vtable".into()) + } + } + hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => { + // No need to register anything for these cases + ConstantExprKind::Opaque("dyn or error supertrait vtable".into()) + } + hax::ImplExprAtom::SelfImpl { .. } => { + raise_error!( + self, + span, + "`SelfImpl` should not appear in vtable construction" + ) + } }; mk_field(kind); } @@ -683,7 +855,7 @@ impl ItemTransCtx<'_, '_> { } /// Generate the body of the vtable instance function. - /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls. + /// It handles `impl Trait for T` implementation and builtin impls (including closure). /// ```ignore /// let ret@0 : VTable; /// ret@0 = VTable { ... }; @@ -694,13 +866,55 @@ impl ItemTransCtx<'_, '_> { span: Span, impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, + impl_kind: &TraitImplSource, ) -> Result { - let hax::FullDefKind::TraitImpl { - trait_pred, items, .. - } = impl_def.kind() - else { - unreachable!() + // let mut locals = Locals::new(0); + // let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); + // let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone()); + + // Get trait definition (`trait_def`) and assoticated items (`items`). + // The `items` for closure is empty: method_call of closure is treated separately. + let (trait_pred, items) = { + match impl_kind { + TraitImplSource::Normal => { + let hax::FullDefKind::TraitImpl { + trait_pred, items, .. + } = impl_def.kind() + else { + unreachable!() + }; + (trait_pred, items) + } + TraitImplSource::Closure(closure_kind) => { + let hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + .. + } = impl_def.kind() + else { + unreachable!() + }; + // Get the appropriate trait implementation for this closure kind + let trait_impl = match closure_kind { + ClosureKind::FnOnce => fn_once_impl, + ClosureKind::FnMut => { + fn_mut_impl.as_ref().expect("FnMut impl should exist") + } + ClosureKind::Fn => fn_impl.as_ref().expect("Fn impl should exist"), + }; + (&trait_impl.trait_pred, &vec![]) + } + _ => { + raise_error!( + self, + span, + "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" + ); + } + } }; + let trait_def = self.hax_def(&trait_pred.trait_ref)?; let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?; // The type this impl is for. @@ -792,12 +1006,23 @@ impl ItemTransCtx<'_, '_> { }; mk_field(ConstantExprKind::FnPtr(fn_ptr)); + // Add usual method for item in items { self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?; } + // Add the closure method (call, call_mut) + // We do not translate `call_once` for the reason discussed above -- the function is not dyn-compatible + if let TraitImplSource::Closure(closure_kind) = *impl_kind + && !matches!(closure_kind, ClosureKind::FnOnce) + { + mk_field(self.generate_closure_method_shim_ref(span, impl_def, closure_kind)?); + } + + // Add supertraits to vtable value. self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?; + // Check if every field is filled if field_ty_iter.next().is_some() { raise_error!( self, @@ -818,6 +1043,45 @@ impl ItemTransCtx<'_, '_> { Ok(Body::Unstructured(builder.build())) } + fn generate_closure_method_shim_ref( + &mut self, + span: Span, + impl_def: &hax::FullDef, + closure_kind: ClosureKind, + ) -> Result { + // Register the closure method shim + let shim_id: FunDeclId = self.register_item( + span, + impl_def.this(), + TransItemSourceKind::VTableMethod(TraitImplSource::Closure(closure_kind)), + ); + + let mut generics = Box::new(self.the_only_binder().params.identity_args()); + + // Add the arguments for region binders of the closure + let hax::FullDefKind::Closure { args, .. } = impl_def.kind() else { + unreachable!() + }; + // The signature can only contain region binders + let sig = &args.fn_sig; + for _ in &sig.bound_vars { + // The late-bound region binders are at last, for the whole closure, as per `translate_closures`, use push + generics.regions.push(Region::Erased); + } + // Finally, one more region for the receiver, this is at first, as it is the region of the function itself, use insert at head + generics + .regions + .insert_and_shift_ids(RegionId::ZERO, Region::Erased); + + // Create function pointer to the shim + let fn_ptr = FnPtr { + kind: Box::new(shim_id.into()), + generics, + }; + + Ok(ConstantExprKind::FnPtr(fn_ptr)) + } + pub(crate) fn translate_vtable_instance_init( mut self, init_func_id: FunDeclId, @@ -829,7 +1093,7 @@ impl ItemTransCtx<'_, '_> { self.translate_def_generics(span, impl_def)?; self.check_no_monomorphize(span)?; - let (impl_ref, vtable_struct_ref) = + let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; let init_for = self.register_item( span, @@ -845,19 +1109,9 @@ impl ItemTransCtx<'_, '_> { output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())), }; - let body = match impl_kind { - TraitImplSource::Normal => { - let body = self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?; - Ok(body) - } - _ => { - raise_error!( - self, - span, - "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" - ); - } - }; + let body = self + .gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref, impl_kind) + .map_err(|_| Opaque); Ok(FunDecl { def_id: init_func_id, @@ -892,6 +1146,7 @@ impl ItemTransCtx<'_, '_> { target_receiver: &Ty, shim_signature: &FunSig, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let mut builder = BodyBuilder::new(span, shim_signature.inputs.len()); @@ -918,8 +1173,18 @@ impl ItemTransCtx<'_, '_> { ); builder.push_statement(StatementKind::Assign(target_self.clone(), rval)); - let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun); + let fun_id = self.register_item( + span, + &impl_func_def.this(), + match impl_kind { + TraitImplSource::Normal => TransItemSourceKind::Fun, + TraitImplSource::Closure(kind) => TransItemSourceKind::ClosureMethod(*kind), + _ => unreachable!(), + }, + ); + let generics = self.outermost_binder().params.identity_args(); + builder.call(Call { func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)), args: method_args @@ -937,6 +1202,7 @@ impl ItemTransCtx<'_, '_> { fun_id: FunDeclId, item_meta: ItemMeta, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let span = item_meta.span; self.check_no_monomorphize(span)?; @@ -976,8 +1242,13 @@ impl ItemTransCtx<'_, '_> { signature.inputs[0].with_ctx(&self.into_fmt()) ); - let body = - self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?; + let body = self.translate_vtable_shim_body( + span, + &target_receiver, + &signature, + impl_func_def, + impl_kind, + )?; Ok(FunDecl { def_id: fun_id, diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index 91ebc4bf3..29ea8c428 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -99,7 +99,6 @@ struct core::ops::function::FnOnce::{vtable} { size: usize, align: usize, drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: FnOnce<_dyn, Args> + _dyn : '_ + @TraitClause0_2::Output = Ty0)), - method_call_once: fn((dyn exists<_dyn> [@TraitClause0_2]: FnOnce<_dyn, Args> + _dyn : '_ + @TraitClause0_2::Output = Ty0), Args) -> Ty0, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index e7f5962f5..1fbbd9517 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -234,12 +234,18 @@ fn {impl Super for i32}::{vtable}() -> test_crate::Super::{vtable} let ret@0: test_crate::Super::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: move (@4) } return } @@ -290,12 +296,18 @@ fn {impl Internal for i32}::{vtable}() -> test_crate::Internal::{vtable} let ret@0: test_crate::Internal::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Internal::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_internal_method: const ({impl Internal for i32}::internal_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Internal::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_internal_method: const ({impl Internal for i32}::internal_method::{vtable_method}<'_>), super_trait_0: move (@4) } return } @@ -348,7 +360,9 @@ fn {impl Left for i32}::{vtable}() -> test_crate::Left::{vtable} let size@1: usize; // local let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::Internal::{vtable}); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::Internal::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of @@ -357,8 +371,12 @@ fn {impl Left for i32}::{vtable}() -> test_crate::Left::{vtable} storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl Internal for i32}::{vtable} - ret@0 := test_crate::Left::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_left_method: const ({impl Left for i32}::left_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + @4 := &core::marker::MetaSized::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl Internal for i32}::{vtable} + ret@0 := test_crate::Left::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_left_method: const ({impl Left for i32}::left_method::{vtable_method}<'_>), super_trait_0: move (@4), super_trait_1: move (@6) } return } @@ -442,9 +460,11 @@ fn {impl Right for i32}::{vtable}() -> test_crate::Right::{vtable}); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local let @5: (); // anonymous local - let @6: &'static (test_crate::Super::{vtable}); // anonymous local + let @6: &'static (test_crate::Internal::{vtable}); // anonymous local + let @7: (); // anonymous local + let @8: &'static (test_crate::Super::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of @@ -453,12 +473,16 @@ fn {impl Right for i32}::{vtable}() -> test_crate::Right::{vtable} for i32}::{vtable} - ret@0 := test_crate::Right::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_right_method: const ({impl Right for i32}::right_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4), super_trait_2: move (@6) } + @6 := &{impl Internal for i32}::{vtable} + storage_live(@7) + @7 := () + storage_live(@8) + @8 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Right::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_right_method: const ({impl Right for i32}::right_method::{vtable_method}<'_>), super_trait_0: move (@4), super_trait_1: move (@6), super_trait_2: move (@8) } return } @@ -523,9 +547,11 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable}); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local let @5: (); // anonymous local - let @6: &'static (test_crate::Right::{vtable}); // anonymous local + let @6: &'static (test_crate::Left::{vtable}); // anonymous local + let @7: (); // anonymous local + let @8: &'static (test_crate::Right::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of @@ -534,12 +560,16 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} for i32}::{vtable} - ret@0 := test_crate::Join::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_join_method: const ({impl Join for i32}::join_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4), super_trait_2: move (@6) } + @6 := &{impl Left for i32}::{vtable} + storage_live(@7) + @7 := () + storage_live(@8) + @8 := &{impl Right for i32}::{vtable} + ret@0 := test_crate::Join::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_join_method: const ({impl Join for i32}::join_method::{vtable_method}<'_>), super_trait_0: move (@4), super_trait_1: move (@6), super_trait_2: move (@8) } return } diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 8b1adb25b..7170c5067 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -1,284 +1,33 @@ -# Final LLBC before serialization: - -// Full name: core::marker::MetaSized -#[lang_item("meta_sized")] -pub trait MetaSized - -struct core::marker::MetaSized::{vtable} { - size: usize, - align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: MetaSized<_dyn> + _dyn : '_)), -} - -// Full name: core::marker::Sized -#[lang_item("sized")] -pub trait Sized -{ - parent_clause0 : [@TraitClause0]: MetaSized - non-dyn-compatible -} - -// Full name: core::marker::Tuple -#[lang_item("tuple_trait")] -pub trait Tuple -{ - parent_clause0 : [@TraitClause0]: MetaSized - vtable: core::marker::Tuple::{vtable} -} - -// Full name: core::ops::drop::Drop -#[lang_item("drop")] -pub trait Drop -{ - parent_clause0 : [@TraitClause0]: MetaSized - fn drop<'_0_1> = drop<'_0_1, Self>[Self] - fn drop_in_place = drop_in_place - vtable: core::ops::drop::Drop::{vtable} -} - -// Full name: core::ops::drop::Drop::drop_in_place -fn drop_in_place(@1: *mut 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 -{ - parent_clause0 : [@TraitClause0]: MetaSized - parent_clause1 : [@TraitClause1]: Sized - parent_clause2 : [@TraitClause2]: Tuple - parent_clause3 : [@TraitClause3]: Sized - type Output - fn call_once = core::ops::function::FnOnce::call_once[Self] - vtable: core::ops::function::FnOnce::{vtable} -} - -struct core::ops::function::FnOnce::{vtable} { - size: usize, - align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: FnOnce<_dyn, Args> + _dyn : '_ + @TraitClause0_2::Output = Ty0)), - method_call_once: fn((dyn exists<_dyn> [@TraitClause0_2]: FnOnce<_dyn, Args> + _dyn : '_ + @TraitClause0_2::Output = Ty0), Args) -> Ty0, - super_trait_0: &'static (core::marker::MetaSized::{vtable}), -} - -// Full name: core::ops::function::FnMut -#[lang_item("fn_mut")] -pub trait FnMut -{ - parent_clause0 : [@TraitClause0]: MetaSized - parent_clause1 : [@TraitClause1]: FnOnce - parent_clause2 : [@TraitClause2]: Sized - parent_clause3 : [@TraitClause3]: Tuple - fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] - vtable: core::ops::function::FnMut::{vtable} -} - -struct core::ops::function::FnMut::{vtable} { - size: usize, - align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause0_2::parent_clause1::Output = Ty0)), - method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn exists<_dyn> [@TraitClause0_2]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause0_2::parent_clause1::Output = Ty0)), Args) -> Ty0, - super_trait_0: &'static (core::marker::MetaSized::{vtable}), - super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), -} - -struct core::ops::function::Fn::{vtable} { - size: usize, - align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0_2]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Output = Ty0)), - method_call: fn<'_0_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0_2]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause0_2::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Ty0, - super_trait_0: &'static (core::marker::MetaSized::{vtable}), - super_trait_1: &'static (core::ops::function::FnMut::{vtable}), -} - -// Full name: core::ops::function::Fn -#[lang_item("r#fn")] -pub trait Fn -{ - parent_clause0 : [@TraitClause0]: MetaSized - parent_clause1 : [@TraitClause1]: FnMut - parent_clause2 : [@TraitClause2]: Sized - parent_clause3 : [@TraitClause3]: Tuple - fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] - vtable: core::ops::function::Fn::{vtable} -} - -pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output -where - [@TraitClause0]: Fn, - -pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output -where - [@TraitClause0]: FnMut, - -pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output -where - [@TraitClause0]: FnOnce, - -fn UNIT_METADATA() -{ - let @0: (); // return - - @0 := () - return -} - -const UNIT_METADATA: () = @Fun0() - -// Full name: test_crate::takes_fn -fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0_1]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_0 + for<'a> @TraitClause0_1::parent_clause1::parent_clause1::Output = bool))) -{ - let @0: (); // return - let f@1: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause0_1::parent_clause1::parent_clause1::Output = bool)); // arg #1 - let counter@2: u32; // local - let @3: bool; // anonymous local - let @4: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause0_1::parent_clause1::parent_clause1::Output = bool)); // anonymous local - let @5: (&'_ mut (u32)); // anonymous local - let @6: &'_ mut (u32); // anonymous local - let @7: &'_ mut (u32); // anonymous local - - @0 := () - storage_live(counter@2) - counter@2 := const (0 : u32) - storage_live(@3) - storage_live(@4) - @4 := &*(f@1) with_metadata(copy (f@1.metadata)) - storage_live(@5) - storage_live(@6) - storage_live(@7) - @7 := &mut counter@2 - @6 := &two-phase-mut *(@7) - @5 := (move (@6)) - @3 := (move (*(@4.metadata)).method_call)(move (@4), move (@5)) - if move (@3) { - storage_dead(@7) - storage_dead(@6) - storage_dead(@5) - storage_dead(@4) - @0 := () - } - else { - storage_dead(@7) - storage_dead(@6) - storage_dead(@5) - storage_dead(@4) - @0 := () - } - storage_dead(@3) - storage_dead(counter@2) - return -} - -// Full name: test_crate::gives_fn::closure -struct closure {} - -// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::call -fn {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_1>(@1: &'_1 (closure), @2: (&'_0 mut (u32))) -> bool -{ - let @0: bool; // return - let @1: &'_ (closure); // arg #1 - let tupled_args@2: (&'_0 mut (u32)); // arg #2 - let counter@3: &'_ mut (u32); // local - let @4: u32; // anonymous local - - storage_live(counter@3) - storage_live(@4) - counter@3 := move ((tupled_args@2).0) - @4 := copy (*(counter@3)) panic.+ const (1 : u32) - *(counter@3) := move (@4) - @0 := const (true) - return -} - -// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::call_mut -fn {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(@1: &'_1 mut (closure), @2: (&'_0 mut (u32))) -> bool -{ - let @0: bool; // return - let state@1: &'_1 mut (closure); // arg #1 - let args@2: (&'_0 mut (u32)); // arg #2 - let @3: &'_ (closure); // anonymous local - - storage_live(@3) - @3 := &*(state@1) - @0 := {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_>(move (@3), move (args@2)) - return -} - -// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::call_once -fn {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0>(@1: closure, @2: (&'_0 mut (u32))) -> bool -{ - let @0: bool; // return - let @1: closure; // arg #1 - let @2: (&'_ mut (u32)); // arg #2 - let @3: &'_ mut (closure); // anonymous local - - storage_live(@3) - @3 := &mut @1 - @0 := {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_>(move (@3), move (@2)) - drop[Drop] @1 - return -} - -// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure} -impl<'_0> FnOnce<(&'_ mut (u32))> for closure { - parent_clause0 = MetaSized - parent_clause1 = Sized<(&'_ mut (u32))> - parent_clause2 = Tuple<(&'_ mut (u32))> - parent_clause3 = Sized - type Output = bool - fn call_once = {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0> - non-dyn-compatible -} - -// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure} -impl<'_0> FnMut<(&'_ mut (u32))> for closure { - parent_clause0 = MetaSized - parent_clause1 = {impl FnOnce<(&'_ mut (u32))> for closure}<'_0> - parent_clause2 = Sized<(&'_ mut (u32))> - parent_clause3 = Tuple<(&'_ mut (u32))> - fn call_mut<'_0_1> = {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_0_1> - non-dyn-compatible -} - -// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure} -impl<'_0> Fn<(&'_ mut (u32))> for closure { - parent_clause0 = MetaSized - parent_clause1 = {impl FnMut<(&'_ mut (u32))> for closure}<'_0> - parent_clause2 = Sized<(&'_ mut (u32))> - parent_clause3 = Tuple<(&'_ mut (u32))> - fn call<'_0_1> = {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_0_1> - non-dyn-compatible -} - -// Full name: test_crate::gives_fn -fn gives_fn() -{ - let @0: (); // return - let @1: &'_ ((dyn exists<_dyn> [@TraitClause0_1]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause0_1::parent_clause1::parent_clause1::Output = bool)); // anonymous local - let @2: &'_ (closure); // anonymous local - let @3: &'_ (closure); // anonymous local - let @4: closure; // anonymous local - - @0 := () - storage_live(@1) - storage_live(@2) - storage_live(@3) - storage_live(@4) - @4 := closure { } - @3 := &@4 - @2 := &*(@3) - @1 := unsize_cast<&'_ (closure), &'_ ((dyn exists<_dyn> [@TraitClause0_1]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause0_1::parent_clause1::parent_clause1::Output = bool)), {impl Fn<(&'_ mut (u32))> for closure}<'_>>(move (@2)) - storage_dead(@2) - @0 := takes_fn<'_>(move (@1)) - storage_dead(@1) - storage_dead(@4) - storage_dead(@3) - return -} - - - +error: Trying to generate a vtable shim for a non-vtable-safe method + --> tests/ui/simple/dyn-fn.rs:8:15 + | + 8 | takes_fn(&|counter| { + | _______________^ + 9 | | *counter += 1; +10 | | true +11 | | }) + | |_____^ + +error: Item `test_crate::gives_fn::{closure#0}` caused errors; ignoring. + --> tests/ui/simple/dyn-fn.rs:8:15 + | +8 | takes_fn(&|counter| { + | ^^^^^^^^^ + +error: Trying to generate a vtable shim for a non-vtable-safe method + --> tests/ui/simple/dyn-fn.rs:8:15 + | + 8 | takes_fn(&|counter| { + | _______________^ + 9 | | *counter += 1; +10 | | true +11 | | }) + | |_____^ + +error: Item `test_crate::gives_fn::{closure#0}` caused errors; ignoring. + --> tests/ui/simple/dyn-fn.rs:8:15 + | +8 | takes_fn(&|counter| { + | ^^^^^^^^^ + +ERROR Charon failed to translate this code (4 errors) diff --git a/charon/tests/ui/simple/dyn-fn.rs b/charon/tests/ui/simple/dyn-fn.rs index c71ace687..f4755d629 100644 --- a/charon/tests/ui/simple/dyn-fn.rs +++ b/charon/tests/ui/simple/dyn-fn.rs @@ -1,3 +1,4 @@ +//@ known-failure fn takes_fn(f: &dyn for<'a> Fn(&'a mut u32) -> bool) { let mut counter = 0; if f(&mut counter) {} diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index 13b1013e5..86deaeb8e 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -147,12 +147,18 @@ where let ret@0: test_crate::Modifiable::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@4) } return } diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index d97f74653..327efc750 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -282,12 +282,18 @@ fn {impl Super for i32}::{vtable}() -> test_crate::Super::{vtable} let ret@0: test_crate::Super::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: move (@4) } return } @@ -340,7 +346,9 @@ fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable}< let size@1: usize; // local let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::Super::{vtable}); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::Super::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of @@ -349,8 +357,12 @@ fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable}< storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + @4 := &core::marker::MetaSized::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: move (@4), super_trait_1: move (@6) } return } @@ -512,12 +524,18 @@ where let ret@0: test_crate::Modifiable::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@4) } return } @@ -709,12 +727,18 @@ fn {impl BaseOn for i32}::{vtable}() -> test_crate::BaseOn::{vtable} let ret@0: test_crate::BaseOn::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: move (@4) } return } @@ -785,12 +809,18 @@ fn {impl BaseOn for i32}::{vtable}() -> test_crate::BaseOn::{vtable} let ret@0: test_crate::BaseOn::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: move (@4) } return } @@ -848,9 +878,11 @@ fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} let size@1: usize; // local let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local let @5: (); // anonymous local - let @6: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @6: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @7: (); // anonymous local + let @8: &'static (test_crate::BaseOn::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of @@ -859,12 +891,16 @@ fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl BaseOn for i32}::{vtable} + @4 := &core::marker::MetaSized::{vtable} storage_live(@5) @5 := () storage_live(@6) - @6 := &{impl BaseOn for i32}::{vtable} - ret@0 := test_crate::Both32And64::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4), super_trait_2: move (@6) } + @6 := &{impl BaseOn for i32}::{vtable} + storage_live(@7) + @7 := () + storage_live(@8) + @8 := &{impl BaseOn for i32}::{vtable} + ret@0 := test_crate::Both32And64::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: move (@4), super_trait_1: move (@6), super_trait_2: move (@8) } return } @@ -960,12 +996,18 @@ fn {impl LifetimeTrait for i32}::{vtable}() -> test_crate::LifetimeTrait::{vtabl let ret@0: test_crate::LifetimeTrait::{vtable}; // return let size@1: usize; // local let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (core::marker::MetaSized::{vtable}); // anonymous local storage_live(size@1) size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::LifetimeTrait::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::LifetimeTrait::{vtable} { size: move (size@1), align: move (align@2), drop: const (Drop::drop_in_place), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: move (@4) } return } diff --git a/charon/tests/ui/vtables.rs b/charon/tests/ui/vtables.rs index 9393d084b..2c5be620c 100644 --- a/charon/tests/ui/vtables.rs +++ b/charon/tests/ui/vtables.rs @@ -28,6 +28,21 @@ fn to_dyn_obj(arg: &T) -> &dyn NoParam { arg } +// #[derive(Clone)] +// struct MyStruct { +// a: i32, +// b: String, +// } + +// fn ok_clone(arg: &T) -> T { +// arg.clone() +// } +// fn use_ok_clone(arg: &String) -> String { +// ok_clone(arg); +// let s = MyStruct { a: 10, b: String::from("Hello") }; +// ok_clone(&s).b +// } + trait Modifiable { fn modify(&mut self, arg: &T) -> T; }