From 7aa1d87f4d5521d3d21e16b2a61715e354dd8049 Mon Sep 17 00:00:00 2001 From: ssyram Date: Wed, 8 Oct 2025 16:29:45 +0800 Subject: [PATCH 1/5] initial vtable support for closures TODO: fix the `translate_vtable_shim` part, then remove the "//@ known-failure" in the test `simple/dyn-fn` example --- .../translate/translate_bodies.rs | 69 +++- .../translate/translate_closures.rs | 2 +- .../translate/translate_crate.rs | 4 +- .../translate/translate_items.rs | 8 +- .../charon-driver/translate/translate_meta.rs | 2 +- .../translate/translate_trait_objects.rs | 362 +++++++++++++++++- .../tests/ui/dyn-with-diamond-supertraits.out | 8 +- charon/tests/ui/simple/dyn-fn.out | 290 ++------------ charon/tests/ui/simple/dyn-fn.rs | 1 + charon/tests/ui/vtables.out | 8 +- charon/tests/ui/vtables.rs | 15 + 11 files changed, 476 insertions(+), 293 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 9291ba347..ec82e16f3 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(); + 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 4e384d0db..a145d90e3 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -282,7 +282,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 0bb069380..635e0348d 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -69,7 +69,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`]. @@ -282,7 +282,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { | ClosureAsFnCast | DropGlueMethod | 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 e447123cd..301df25dc 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -164,11 +164,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); } } @@ -187,6 +187,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let span = self.def_span(item_source.def_id()); raise_error!(self, span, "Failed to translate item {id:?}.") } + // This prevents re-translating of the same item in the usual queue processing loop. + // If this is not present, if the function is called before the usual processing loop, + // `processed` does not record the item as processed, and we end up translating it again. + self.processed.insert(item_source); } let item = self.translated.get_item(id); Ok(item.unwrap()) diff --git a/charon/src/bin/charon-driver/translate/translate_meta.rs b/charon/src/bin/charon-driver/translate/translate_meta.rs index d7d8a7959..d835aa879 100644 --- a/charon/src/bin/charon-driver/translate/translate_meta.rs +++ b/charon/src/bin/charon-driver/translate/translate_meta.rs @@ -362,7 +362,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 5a9bbbcd8..638f90c3c 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -234,6 +234,18 @@ 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 @@ -480,22 +492,48 @@ 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, TraitDeclRef, TypeDeclRef), Error> { - let implemented_trait = match impl_def.kind() { - hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref, - _ => unreachable!(), + 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 implemented_trait = self.translate_trait_decl_ref(span, implemented_trait)?; - let impl_ref = self.translate_item( - span, - impl_def.this(), - TransItemSourceKind::TraitImpl(*impl_kind), - )?; Ok((impl_ref, implemented_trait, vtable_struct_ref)) } @@ -570,7 +608,7 @@ 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) } @@ -594,12 +632,30 @@ 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() @@ -637,8 +693,107 @@ 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); } @@ -742,6 +897,155 @@ impl ItemTransCtx<'_, '_> { })) } + fn gen_closure_vtable_instance_init_body( + &mut self, + span: Span, + impl_def: &hax::FullDef, + vtable_struct_ref: TypeDeclRef, + closure_kind: ClosureKind, + ) -> Result { + let mut locals = Locals { + arg_count: 0, + locals: Vector::new(), + }; + let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); + let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone()); + + 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"), + }; + + // Retreive the expected field types from the struct definition. This avoids complicated + // substitutions. + let field_tys = { + let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone(); + let ItemRef::Type(vtable_def) = + self.t_ctx.get_or_translate(vtable_decl_id.into())? + else { + unreachable!() + }; + let TypeDeclKind::Struct(fields) = &vtable_def.kind else { + unreachable!() + }; + fields + .iter() + .map(|f| &f.ty) + .cloned() + .map(|ty| ty.substitute(&vtable_struct_ref.generics)) + .collect_vec() + }; + + let mut statements = vec![]; + let mut aggregate_fields = vec![]; + // For each vtable field, assign the desired value to a new local. + let mut field_ty_iter = field_tys.into_iter(); + let mut mk_field = |kind| { + aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty: field_ty_iter.next().unwrap() }))); + }; + + // Add the standard vtable metadata fields (size, align, drop) + // like usual instance, the value will be provided in a pass later + mk_field( + ConstantExprKind::Opaque("closure size".to_string()), + ); + mk_field( + ConstantExprKind::Opaque("closure align".to_string()), + ); + mk_field( + ConstantExprKind::Opaque("closure drop".to_string()), + ); + + // 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 closure_kind != ClosureKind::FnOnce { + mk_field(self.generate_closure_method_shim_ref( + span, + impl_def, + closure_kind, + )? + ); + } + + let trait_def = self.hax_def(&trait_impl.trait_pred.trait_ref)?; + self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, mk_field)?; + + // Create the aggregate for the vtable struct + let ret_rvalue = Rvalue::Aggregate( + AggregateKind::Adt(vtable_struct_ref.clone(), None, None), + aggregate_fields, + ); + statements.push(Statement::new( + span, + StatementKind::Assign(ret_place.clone(), ret_rvalue), + )); + + let block = BlockData { + statements, + terminator: Terminator { + span, + kind: TerminatorKind::Return, + comments_before: Vec::new(), + }, + }; + + Ok(Body::Unstructured(GExprBody { + span, + locals, + comments: Vec::new(), + body: [block].into(), + })) + } + + 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)) + } + fn generate_concretization( &mut self, span: Span, @@ -794,6 +1098,16 @@ impl ItemTransCtx<'_, '_> { let body = self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?; Ok(body) } + TraitImplSource::Closure(closure_kind) => { + // For closures, we need to generate the vtable init body differently + let body = self.gen_closure_vtable_instance_init_body( + span, + impl_def, + vtable_struct_ref, + *closure_kind, + )?; + Ok(body) + } _ => { raise_error!( self, @@ -836,6 +1150,7 @@ impl ItemTransCtx<'_, '_> { target_receiver: &Ty, shim_signature: &FunSig, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let mut locals = Locals { arg_count: shim_signature.inputs.len(), @@ -864,7 +1179,15 @@ impl ItemTransCtx<'_, '_> { self.generate_concretization(span, &mut statements, &shim_self, &target_self)?; let call = { - 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 = Box::new(self.outermost_binder().params.identity_args()); Call { func: FnOperand::Regular(FnPtr { @@ -921,6 +1244,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)?; @@ -961,7 +1285,7 @@ impl ItemTransCtx<'_, '_> { ); let body = - self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?; + 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-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index e66957f58..6debb3b1e 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -319,14 +319,16 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable}; // return let @1: (); // anonymous local - let @2: &'static (test_crate::Left::{vtable}); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local let @3: (); // anonymous local - let @4: &'static (test_crate::Right::{vtable}); // anonymous local + let @4: &'static (test_crate::Left::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local storage_live(@1) @1 := () storage_live(@2) - @2 := &{impl Left for i32}::{vtable} + @2 := &core::marker::MetaSized::{vtable} storage_live(@3) @3 := () storage_live(@4) diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 06b817fbf..7170c5067 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -1,257 +1,33 @@ -# Final LLBC before serialization: - -// Full name: core::marker::MetaSized -#[lang_item("meta_sized")] -pub trait MetaSized - -// Full name: core::marker::Sized -#[lang_item("sized")] -pub trait Sized -{ - parent_clause0 : [@TraitClause0]: MetaSized - non-dyn-compatible -} - -// Full name: core::marker::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> = drop<'_0_0, Self>[Self] - vtable: core::ops::drop::Drop::{vtable} -} - -// 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} -} - -// 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> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - vtable: core::ops::function::FnMut::{vtable} -} - -struct core::ops::function::Fn::{vtable} { - size: usize, - align: usize, - drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), - method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::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> = core::ops::function::Fn::call<'_0_0, 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]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_0 + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool))) -{ - let @0: (); // return - let f@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // arg #1 - let counter@2: u32; // local - let @3: bool; // anonymous local - let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::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> = {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_0_0> - 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> = {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_0_0> - non-dyn-compatible -} - -// Full name: test_crate::gives_fn -fn gives_fn() -{ - let @0: (); // return - let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::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]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::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/vtables.out b/charon/tests/ui/vtables.out index 49c9b8d8b..248698019 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -707,14 +707,16 @@ fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} { let ret@0: test_crate::Both32And64::{vtable}; // return let @1: (); // anonymous local - let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local let @3: (); // anonymous local - let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::BaseOn::{vtable}); // anonymous local storage_live(@1) @1 := () storage_live(@2) - @2 := &{impl BaseOn for i32}::{vtable} + @2 := &core::marker::MetaSized::{vtable} storage_live(@3) @3 := () storage_live(@4) 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; } From 28701419be22ddf0e05f1f0fe2319ba6f87bea99 Mon Sep 17 00:00:00 2001 From: sam <1205470772@qq.com> Date: Wed, 22 Oct 2025 10:28:14 +0800 Subject: [PATCH 2/5] minor: cargo fmt --- .../translate/translate_trait_objects.rs | 164 ++++++++++-------- 1 file changed, 89 insertions(+), 75 deletions(-) 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 638f90c3c..3a5ef7e2f 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -245,7 +245,9 @@ impl ItemTransCtx<'_, '_> { // 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(()); } + 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 @@ -608,7 +610,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(TraitImplSource::Normal))? + .translate_fn_ptr( + span, + &item_ref, + TransItemSourceKind::VTableMethod(TraitImplSource::Normal), + )? .erase(); ConstantExprKind::FnPtr(shim_ref) } @@ -636,19 +642,18 @@ impl ItemTransCtx<'_, '_> { 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!(), - } + 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:?}" - ), + kind => raise_error!(self, span, "TODO: Unknown type of impl full def: {kind:?}"), }; // let hax::FullDefKind::TraitImpl { // implied_impl_exprs, .. @@ -697,66 +702,69 @@ impl ItemTransCtx<'_, '_> { // 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, - } - }); + 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() + 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), - ), + 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() + } 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); - + 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 - ), - )?; + 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); + 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, @@ -764,9 +772,17 @@ impl ItemTransCtx<'_, '_> { 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()) + 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 { .. } => { @@ -932,8 +948,7 @@ impl ItemTransCtx<'_, '_> { // substitutions. let field_tys = { let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone(); - let ItemRef::Type(vtable_def) = - self.t_ctx.get_or_translate(vtable_decl_id.into())? + let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())? else { unreachable!() }; @@ -953,30 +968,22 @@ impl ItemTransCtx<'_, '_> { // For each vtable field, assign the desired value to a new local. let mut field_ty_iter = field_tys.into_iter(); let mut mk_field = |kind| { - aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty: field_ty_iter.next().unwrap() }))); + aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { + kind, + ty: field_ty_iter.next().unwrap(), + }))); }; // Add the standard vtable metadata fields (size, align, drop) // like usual instance, the value will be provided in a pass later - mk_field( - ConstantExprKind::Opaque("closure size".to_string()), - ); - mk_field( - ConstantExprKind::Opaque("closure align".to_string()), - ); - mk_field( - ConstantExprKind::Opaque("closure drop".to_string()), - ); + mk_field(ConstantExprKind::Opaque("closure size".to_string())); + mk_field(ConstantExprKind::Opaque("closure align".to_string())); + mk_field(ConstantExprKind::Opaque("closure drop".to_string())); // 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 closure_kind != ClosureKind::FnOnce { - mk_field(self.generate_closure_method_shim_ref( - span, - impl_def, - closure_kind, - )? - ); + mk_field(self.generate_closure_method_shim_ref(span, impl_def, closure_kind)?); } let trait_def = self.hax_def(&trait_impl.trait_pred.trait_ref)?; @@ -1035,7 +1042,9 @@ impl ItemTransCtx<'_, '_> { 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); + generics + .regions + .insert_and_shift_ids(RegionId::ZERO, Region::Erased); // Create function pointer to the shim let fn_ptr = FnPtr { @@ -1284,8 +1293,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, impl_kind)?; + let body = self.translate_vtable_shim_body( + span, + &target_receiver, + &signature, + impl_func_def, + impl_kind, + )?; Ok(FunDecl { def_id: fun_id, From d0bc90bbf936ad1eb1e784ad48dfacb9e57921bf Mon Sep 17 00:00:00 2001 From: sam <1205470772@qq.com> Date: Fri, 24 Oct 2025 10:50:44 +0800 Subject: [PATCH 3/5] rerun of 'make test' --- .../tests/ui/dyn-with-diamond-supertraits.out | 12 ++++--- charon/tests/ui/vtable-simple.out | 8 ++++- charon/tests/ui/vtables.out | 36 +++++++++++++++---- 3 files changed, 44 insertions(+), 12 deletions(-) diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index 6debb3b1e..a0e0dcf0b 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -321,9 +321,9 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @4: &'static (test_crate::Left::{vtable}); // anonymous local let @5: (); // anonymous local - let @6: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @6: &'static (test_crate::Right::{vtable}); // anonymous local storage_live(@1) @1 := () @@ -332,8 +332,12 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} for i32}::{vtable} - ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + @4 := &{impl Left for i32}::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl Right for i32}::{vtable} + ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({vtable_method}<'_>), super_trait_0: move (@2), super_trait_1: move (@4), super_trait_2: move (@6) } return } diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index fe2b69230..e84826b04 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -121,8 +121,14 @@ where [@TraitClause1]: Clone, { let ret@0: test_crate::Modifiable::{vtable}; // return + let @1: (); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := () + storage_live(@2) + @2 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@2) } return } diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 248698019..7647ad026 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -285,13 +285,19 @@ fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable}< { let ret@0: test_crate::Checkable::{vtable}; // return let @1: (); // anonymous local - let @2: &'static (test_crate::Super::{vtable}); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @3: (); // anonymous local + let @4: &'static (test_crate::Super::{vtable}); // anonymous local storage_live(@1) @1 := () storage_live(@2) - @2 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } + @2 := &core::marker::MetaSized::{vtable} + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: move (@2), super_trait_1: move (@4) } return } @@ -451,8 +457,14 @@ where [@TraitClause1]: Clone, { let ret@0: test_crate::Modifiable::{vtable}; // return + let @1: (); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := () + storage_live(@2) + @2 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@2) } return } @@ -720,8 +732,12 @@ fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl BaseOn for i32}::{vtable} - ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + @4 := &{impl BaseOn for i32}::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl BaseOn for i32}::{vtable} + ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: move (@2), super_trait_1: move (@4), super_trait_2: move (@6) } return } @@ -815,8 +831,14 @@ fn {impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'a, '_1>(@1: & fn {impl LifetimeTrait for i32}::{vtable}() -> test_crate::LifetimeTrait::{vtable} { let ret@0: test_crate::LifetimeTrait::{vtable}; // return + let @1: (); // anonymous local + let @2: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::LifetimeTrait::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := () + storage_live(@2) + @2 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::LifetimeTrait::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: move (@2) } return } From 18ccb35f7212bc3ce4e304d3f96d66b9114e8a6b Mon Sep 17 00:00:00 2001 From: sam <1205470772@qq.com> Date: Fri, 24 Oct 2025 13:09:05 +0800 Subject: [PATCH 4/5] refactor gen_vtable_instance_init_body to handle the closure case --- .../translate/translate_trait_objects.rs | 216 +++++++----------- 1 file changed, 78 insertions(+), 138 deletions(-) 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 3a5ef7e2f..8f16c30e4 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,5 +1,5 @@ use itertools::Itertools; -use std::mem; +use std::{mem, vec}; use super::{ translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel, @@ -817,7 +817,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 { ... }; @@ -828,18 +828,52 @@ impl ItemTransCtx<'_, '_> { span: Span, impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, + impl_kind: &TraitImplSource, ) -> Result { 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()); - let hax::FullDefKind::TraitImpl { - trait_pred, items, .. - } = impl_def.kind() - else { - unreachable!() + // Get trait definition (`trait_def`) and assoticated items (`items`). + // The `items` for closure is empty: method_call of closure is treated separately. + let (trait_def , items) = { + match impl_kind { + TraitImplSource::Normal => { + let hax::FullDefKind::TraitImpl { + trait_pred, items, .. + } = impl_def.kind() + else { + unreachable!() + }; + (self.hax_def(&trait_pred.trait_ref)?, 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"), + }; + (self.hax_def(&trait_impl.trait_pred.trait_ref)?, &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)?; // Retreive the expected field types from the struct definition. This avoids complicated // substitutions. @@ -869,17 +903,44 @@ impl ItemTransCtx<'_, '_> { aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty }))); }; - // TODO(dyn): provide values - mk_field(ConstantExprKind::Opaque("unknown size".to_string())); - mk_field(ConstantExprKind::Opaque("unknown align".to_string())); - mk_field(ConstantExprKind::Opaque("unknown drop".to_string())); + // Configure the placeholder for the standard vtable metadata fields (size, align, drop). + // The value will be provided in a pass later + let metadata_fields = match impl_kind { + TraitImplSource::Normal => { + vec!["unknown size", "unknown align", "unknown drop"] + }, + TraitImplSource::Closure(_) => { + vec!["closure size", "closure align", "closure drop"] + }, + _ => { + raise_error!( + self, + span, + "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" + ); + } + }; + // mk_field of the vtable metadata fields. + metadata_fields + .iter() + .for_each(|field| mk_field(ConstantExprKind::Opaque(field.to_string()))); + // 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, @@ -888,107 +949,6 @@ impl ItemTransCtx<'_, '_> { ) } - // Construct the final struct. - statements.push(Statement::new( - span, - StatementKind::Assign( - ret_place, - Rvalue::Aggregate( - AggregateKind::Adt(vtable_struct_ref.clone(), None, None), - aggregate_fields, - ), - ), - )); - - let block = BlockData { - statements, - terminator: Terminator::new(span, TerminatorKind::Return), - }; - - Ok(Body::Unstructured(GExprBody { - span, - locals, - comments: Vec::new(), - body: [block].into(), - })) - } - - fn gen_closure_vtable_instance_init_body( - &mut self, - span: Span, - impl_def: &hax::FullDef, - vtable_struct_ref: TypeDeclRef, - closure_kind: ClosureKind, - ) -> Result { - let mut locals = Locals { - arg_count: 0, - locals: Vector::new(), - }; - let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); - let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone()); - - 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"), - }; - - // Retreive the expected field types from the struct definition. This avoids complicated - // substitutions. - let field_tys = { - let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone(); - let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())? - else { - unreachable!() - }; - let TypeDeclKind::Struct(fields) = &vtable_def.kind else { - unreachable!() - }; - fields - .iter() - .map(|f| &f.ty) - .cloned() - .map(|ty| ty.substitute(&vtable_struct_ref.generics)) - .collect_vec() - }; - - let mut statements = vec![]; - let mut aggregate_fields = vec![]; - // For each vtable field, assign the desired value to a new local. - let mut field_ty_iter = field_tys.into_iter(); - let mut mk_field = |kind| { - aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { - kind, - ty: field_ty_iter.next().unwrap(), - }))); - }; - - // Add the standard vtable metadata fields (size, align, drop) - // like usual instance, the value will be provided in a pass later - mk_field(ConstantExprKind::Opaque("closure size".to_string())); - mk_field(ConstantExprKind::Opaque("closure align".to_string())); - mk_field(ConstantExprKind::Opaque("closure drop".to_string())); - - // 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 closure_kind != ClosureKind::FnOnce { - mk_field(self.generate_closure_method_shim_ref(span, impl_def, closure_kind)?); - } - - let trait_def = self.hax_def(&trait_impl.trait_pred.trait_ref)?; - self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, mk_field)?; - // Create the aggregate for the vtable struct let ret_rvalue = Rvalue::Aggregate( AggregateKind::Adt(vtable_struct_ref.clone(), None, None), @@ -1001,11 +961,7 @@ impl ItemTransCtx<'_, '_> { let block = BlockData { statements, - terminator: Terminator { - span, - kind: TerminatorKind::Return, - comments_before: Vec::new(), - }, + terminator: Terminator::new(span, TerminatorKind::Return), }; Ok(Body::Unstructured(GExprBody { @@ -1102,29 +1058,13 @@ 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) - } - TraitImplSource::Closure(closure_kind) => { - // For closures, we need to generate the vtable init body differently - let body = self.gen_closure_vtable_instance_init_body( + let body = + self.gen_vtable_instance_init_body( span, impl_def, vtable_struct_ref, - *closure_kind, - )?; - Ok(body) - } - _ => { - raise_error!( - self, - span, - "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" - ); - } - }; + impl_kind, + ).map_err(|_| Opaque); Ok(FunDecl { def_id: init_func_id, From ed5744b1bb7715907f64b11e6defaef41c5aa20e Mon Sep 17 00:00:00 2001 From: sam <1205470772@qq.com> Date: Fri, 24 Oct 2025 15:00:03 +0800 Subject: [PATCH 5/5] rerun 'make test' --- charon/tests/ui/dyn-trait.out | 1 - .../tests/ui/dyn-with-diamond-supertraits.out | 60 ++++++++++++---- charon/tests/ui/vtable-simple.out | 8 ++- charon/tests/ui/vtables.out | 68 +++++++++++++++---- 4 files changed, 107 insertions(+), 30 deletions(-) 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/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 }