diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 16e30359b..565c18514 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -512,11 +512,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 fa0f1a01b..99ff68576 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 6ffcd2ddb..6e2b8701f 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -72,7 +72,7 @@ pub enum TransItemSourceKind { /// /// For technical reasons, it takes the `self_type` and `dyn_self_type`: /// the former is the type being implemented now while the latter is the `dyn Trait<...>` type. - VTableMethod(Ty, Ty), + VTableMethod(Ty, Ty, TraitImplSource), } /// The kind of a [`TransItemSourceKind::TraitImpl`]. diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index f6d2c70a5..48b223320 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -166,12 +166,12 @@ 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(self_ty, dyn_self) => { + TransItemSourceKind::VTableMethod(self_ty, dyn_self, impl_kind) => { let Some(AnyTransId::Fun(id)) = trans_id else { unreachable!() }; let fun_decl = - bt_ctx.translate_vtable_shim(id, item_meta, &self_ty, &dyn_self, &def)?; + bt_ctx.translate_vtable_shim(id, item_meta, &self_ty, &dyn_self, &def, impl_kind)?; self.translated.fun_decls.set_slot(id, fun_decl); } } @@ -190,6 +190,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_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index f2e915fd9..c39247afa 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,3 +1,4 @@ + use super::{ translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel, translate_predicates::PredicateLocation, @@ -231,6 +232,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 @@ -470,22 +483,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)) } @@ -561,7 +600,7 @@ impl ItemTransCtx<'_, '_> { let mut shim_ref: FnPtr = self.translate_item( span, &item_ref, - TransItemSourceKind::VTableMethod(self_ty.clone(), dyn_self.clone()), + TransItemSourceKind::VTableMethod(self_ty.clone(), dyn_self.clone(), TraitImplSource::Normal), )?; let ty = next_ty(); match ty.kind() { @@ -609,12 +648,30 @@ impl ItemTransCtx<'_, '_> { mut next_ty: impl FnMut() -> Ty, mut mk_field: impl FnMut(RawConstantExpr, Ty), ) -> 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() @@ -652,8 +709,107 @@ impl ItemTransCtx<'_, '_> { }); RawConstantExpr::Ref(global) } - // TODO(dyn): builtin impls - _ => RawConstantExpr::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 { + value: RawConstantExpr::Global(vtable_instance_ref), + ty: fn_ptr_ty, + }); + RawConstantExpr::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 { + value: RawConstantExpr::Global(vtable_instance_ref), + ty: fn_ptr_ty, + }); + RawConstantExpr::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); + RawConstantExpr::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 { + RawConstantExpr::Opaque("generic supertrait vtable".into()) + } + } + hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => { + // No need to register anything for these cases + RawConstantExpr::Opaque("dyn or error supertrait vtable".into()) + } + hax::ImplExprAtom::SelfImpl { .. } => { + raise_error!( + self, + span, + "`SelfImpl` should not appear in vtable construction" + ) + } }; mk_field(kind, next_ty()); } @@ -730,7 +886,7 @@ impl ItemTransCtx<'_, '_> { aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { value: kind, ty }))); }; - // TODO(dyn): provide values + // The metadata will be provided later in the `compute_vtable_metadata` pass mk_field( RawConstantExpr::Opaque("unknown size".to_string()), next_ty(), @@ -797,6 +953,192 @@ 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"), + }; + + let trait_ref = self.translate_trait_ref(span, &trait_impl.trait_pred.trait_ref)?; + let self_ty = trait_ref.generics.types[0].clone(); // This should be the closure type + + // 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 AnyTransItem::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 next_ty = || field_ty_iter.next().unwrap(); + let mut mk_field = |kind, ty| { + aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { value: kind, ty }))); + }; + + // Add the standard vtable metadata fields (size, align, drop) + // like usual instance, the value will be provided in a pass later + mk_field( + RawConstantExpr::Opaque("closure size".to_string()), + next_ty(), + ); + mk_field( + RawConstantExpr::Opaque("closure align".to_string()), + next_ty(), + ); + mk_field( + RawConstantExpr::Opaque("closure drop".to_string()), + next_ty(), + ); + + // 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 { + let call_method_ty = next_ty(); + let dyn_self = self.compute_closure_dyn_self(span, &call_method_ty, &vtable_struct_ref)?; + + mk_field(self.generate_closure_method_shim_ref( + span, + impl_def, + &self_ty, + &dyn_self, + closure_kind, + )?, + call_method_ty, + ); + } + + let trait_def = self.hax_def(&trait_impl.trait_pred.trait_ref)?; + self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, next_ty, 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, + RawStatement::Assign(ret_place.clone(), ret_rvalue), + )); + + let block = BlockData { + statements, + terminator: Terminator { + span, + content: RawTerminator::Return, + comments_before: Vec::new(), + }, + }; + + Ok(Body::Unstructured(GExprBody { + span, + locals, + comments: Vec::new(), + body: [block].into(), + })) + } + + /// Rebuild the `dyn_self` type from the `call_method_ty` and the args from the final `vtable-ref` + /// The `call_method_ty` will have form: `([&'_0] [mut] dyn Fn[Once|Mut]<...>, Args) -> Output` + /// While the actual `Args` & `Output` types are recorded in the vtable-ref + /// The `vtable_struct_ref` is `{vtable}` + fn compute_closure_dyn_self(&self, _span: Span, call_method_ty: &Ty, vtable_struct_ref: &TypeDeclRef) -> Result { + let raw_dyn_self = match call_method_ty.kind() { + TyKind::FnPtr(binder) => { + let receiver = &binder.clone().erase().0[0]; + match receiver.kind() { + TyKind::Ref(_, inner, _) => { + assert!(matches!(inner.kind(), TyKind::DynTrait(_))); + inner.clone() + }, + TyKind::DynTrait(_) => receiver.clone(), + _ => unreachable!(), + } + }, + _ => panic!("Unexpected call method type for closure: {}, Raw: {call_method_ty:?}", call_method_ty.with_ctx(&self.into_fmt())), + }; + Ok(raw_dyn_self.substitute(&vtable_struct_ref.generics)) + } + + fn generate_closure_method_shim_ref( + &mut self, + span: Span, + impl_def: &hax::FullDef, + self_ty: &Ty, + dyn_self: &Ty, + closure_kind: ClosureKind, + ) -> Result { + // Register the closure method shim + let shim_id: FunDeclId = self.register_item( + span, + impl_def.this(), + TransItemSourceKind::VTableMethod(self_ty.clone(), dyn_self.clone(), 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 { + func: Box::new(shim_id.into()), + generics, + }; + + Ok(RawConstantExpr::FnPtr(fn_ptr)) + } + fn check_concretization_ty_match( &self, span: Span, @@ -886,6 +1228,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, @@ -928,6 +1280,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(), @@ -956,7 +1309,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 { @@ -1016,17 +1377,31 @@ impl ItemTransCtx<'_, '_> { self_ty: &Ty, dyn_self: &Ty, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let span = item_meta.span; // compute the correct signature for the shim - let mut signature = self.translate_function_signature(impl_func_def, &item_meta)?; + let mut signature = match impl_kind { + TraitImplSource::Normal => self.translate_function_signature(impl_func_def, &item_meta)?, + TraitImplSource::Closure(kind) => { + self.translate_def_generics(span, impl_func_def)?; + let hax::FullDefKind::Closure { args, .. } = impl_func_def.kind() else { + unreachable!() + }; + // Following practice in `translate_closures`, add the new param + self.innermost_binder_mut() + .push_params_from_binder(args.fn_sig.rebind(()))?; + self.translate_closure_method_sig(impl_func_def, span, args, *kind)? + }, + _ => raise_error!(&self, item_meta.span, "vtable shims for non-closure virtual impls aren't supported, actual kind: {impl_kind:?}") + }; let target_receiver = signature.inputs[0].clone(); // dynify the receiver type, e.g., &T -> &dyn Trait when `impl ... for T` // Pin> -> Pin> when `impl ... for i32` signature.inputs[0].substitute_ty(self_ty, dyn_self); 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/src/transform/compute_vtable_metadata.rs b/charon/src/transform/compute_vtable_metadata.rs index 85c7d5764..380718124 100644 --- a/charon/src/transform/compute_vtable_metadata.rs +++ b/charon/src/transform/compute_vtable_metadata.rs @@ -436,15 +436,19 @@ impl<'a> VtableMetadataComputer<'a> { TypeId::Builtin(BuiltinTy::Array) => self.analyze_array_drop_case(type_decl_ref), TypeId::Tuple => self.analyze_tuple_drop_case(type_decl_ref), TypeId::Builtin(builtin_ty) => self.analyze_builtin_drop_case(builtin_ty, concrete_ty), - TypeId::Adt(_) => { - trace!("[ANALYZE] Found ADT type, looking for direct drop implementation"); - if let Some(fun_ref) = self.find_direct_drop_impl(concrete_ty)? { - Ok(DropCase::Direct(fun_ref)) - } else { - Ok(DropCase::Panic(format!( - "Drop implementation for {:?} not found or not translated", - concrete_ty - ))) + TypeId::Adt(ty_id) => { + let decl = self.ctx.translated.type_decls.get(*ty_id).unwrap(); + match &decl.drop_glue { + Some(impl_ref) => { + match self.ctx.translated.trait_impls.get(impl_ref.id) { + Some(timpl) => { + let method = &timpl.methods().find(|(name, _)| name.0 == "drop").unwrap().1; + Ok(DropCase::Direct(method.skip_binder.clone())) + } + None => unreachable!(), + } + } + None => Ok(DropCase::Empty), } } } @@ -977,6 +981,7 @@ impl<'a> DropShimCtx<'a> { content: RawTerminator::Abort(AbortKind::Panic(None)), comments_before: vec![format!("Panic: {}", msg)], }); + register_error!(self.ctx.ctx, self.span(), "Panic in generating drop shim: {}", msg); Ok(block_id) } diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out index 7ca3196c9..3b5a9729c 100644 --- a/charon/tests/ui/monomorphization/dyn-trait.out +++ b/charon/tests/ui/monomorphization/dyn-trait.out @@ -124,7 +124,7 @@ note: the error occurred when translating `core::marker::MetaSized::, bound_vars: [] }` in the current context: `Unimplemented` - --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/drop.rs:208:1 + --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/drop.rs:208:1 | 208 | pub trait Drop { | ^^^^^^^^^^^^^^ @@ -67,7 +67,7 @@ warning[E9999]: Could not find a clause for `Binder { value: , bound_vars: [] }` in the current context: `Unimplemented` - --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/drop.rs:241:5 + --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/drop.rs:241:5 | 241 | fn drop(&mut self); | ^^^^^^^^^^^^^^^^^^^ @@ -77,7 +77,7 @@ warning[E9999]: Could not find a clause for `Binder { value: , bound_vars: [] }` in the current context: `Unimplemented` - --> /Users/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/marker.rs:179:1 + --> /home/ssyram/.rustup/toolchains/nightly-2025-07-08-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/marker.rs:179:1 | 179 | pub trait MetaSized: PointeeSized { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 36fa4fe0e..6e2b4dfc7 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -47,6 +47,13 @@ pub trait FnOnce vtable: core::ops::function::FnOnce::{vtable} } +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: fn<'_0>(&'_0_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnOnce<_dyn, Args> + _dyn : '_ + @TraitClause1_0::Output = Ty0))), + super_trait_0: &'static (core::marker::MetaSized::{vtable}), +} + // Full name: core::ops::function::FnMut #[lang_item("fn_mut")] pub trait FnMut @@ -59,6 +66,15 @@ pub trait FnMut vtable: core::ops::function::FnMut::{vtable} } +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: fn<'_0>(&'_0_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = Ty0))), + method_call_mut: fn<'_0>(&'_0_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = Ty0)), Args) -> FnMut<(dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = Ty0), Args>::parent_clause1::Output, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable} [@TraitClause0]: FnMut<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = Ty0), Args>::parent_clause1::Output>), +} + struct core::ops::function::Fn::{vtable} { size: usize, align: usize, @@ -249,5 +265,117 @@ fn gives_fn() return } +fn {{impl FnOnce<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_0, '_1>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnOnce<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::Output = bool))) +{ + let ret@0: (); // return + let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnOnce<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::Output = bool)); // arg #1 + + ret@0 := () + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} +fn {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), bool>; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := core::ops::function::FnOnce::{vtable} { size: const (0 : usize), align: const (1 : usize), drop: const ({{impl FnOnce<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_, '_>), super_trait_0: move (@1) } + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} +static {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), bool> = {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}() + +fn {{impl FnMut<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_0, '_1>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool))) +{ + let ret@0: (); // return + let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool)); // arg #1 + + ret@0 := () + return +} + +// Full name: test_crate::gives_fn::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool)), @2: (&'_0 mut (u32))) -> bool +{ + let @0: bool; // return + let @1: &'_1 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool)); // arg #1 + let @2: (&'_0 mut (u32)); // arg #2 + let @3: &'_1 mut (closure); // anonymous local + + storage_live(@0) + storage_live(@1) + storage_live(@2) + storage_live(@3) + @3 := concretize<&'_1 mut ((dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool)), &'_1 mut (closure)>(move (@1)) + @0 := {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} +fn {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), bool>; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), FnMut<(dyn exists<_dyn> [@TraitClause0]: FnMut<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = bool), (&'_ mut (u32))>::parent_clause1::Output>); // anonymous local + + storage_live(@1) + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} + ret@0 := core::ops::function::FnMut::{vtable} { size: const (0 : usize), align: const (1 : usize), drop: const ({{impl FnMut<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_, '_>), method_call_mut: const ({vtable_method}<'_, '_>), super_trait_0: move (@1), super_trait_1: move (@2) } + return +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} +static {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), bool> = {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}() + +fn {{impl Fn<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_0, '_1>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool))) +{ + let ret@0: (); // return + let self@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // arg #1 + + ret@0 := () + return +} + +// Full name: test_crate::gives_fn::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)), @2: (&'_0 mut (u32))) -> bool +{ + let @0: bool; // return + let @1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // arg #1 + let @2: (&'_0 mut (u32)); // arg #2 + let @3: &'_1 (closure); // anonymous local + + storage_live(@0) + storage_live(@1) + storage_live(@2) + storage_live(@3) + @3 := concretize<&'_1 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)), &'_1 (closure)>(move (@1)) + @0 := {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::{vtable} +fn {impl Fn<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::Fn::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::Fn::{vtable}<(&'_ mut (u32)), bool>; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, (&'_ mut (u32))> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = bool), (&'_ mut (u32))>::parent_clause1::parent_clause1::Output>); // anonymous local + + storage_live(@1) + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} + ret@0 := core::ops::function::Fn::{vtable} { size: const (0 : usize), align: const (1 : usize), drop: const ({{impl Fn<(&'_ mut (u32))> for closure}}::{vtable}::{drop_method}<'_, '_>), method_call: const ({vtable_method}<'_, '_>), super_trait_0: move (@1), super_trait_1: move (@2) } + return +} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::{vtable} +static {impl Fn<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::Fn::{vtable}<(&'_ mut (u32)), bool> = {impl Fn<(&'_ mut (u32))> for closure}::{vtable}() + diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index 9fb9d89c8..ff231c96b 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -126,8 +126,11 @@ where [@TraitClause1]: Clone, { let ret@0: test_crate::Modifiable::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::Modifiable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Modifiable for i32}}::{vtable}::{drop_method}<'_, T>[@TraitClause0, @TraitClause1]), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Modifiable for i32}}::{vtable}::{drop_method}<'_, T>[@TraitClause0, @TraitClause1]), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@1) } return } diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 955ec5dbd..e87a3b51e 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -386,11 +386,14 @@ fn {impl Checkable for i32}::check::{vtable_method}<'_0>(@1: &'_0 ((dyn exi fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local storage_live(@1) - @1 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Checkable for i32}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1) } + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Checkable for i32}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: move (@1), super_trait_1: move (@2) } return } @@ -519,11 +522,14 @@ fn {impl Checkable for String}::check::{vtable_method}<'_0>(@1: &'_0 ((dyn fn {impl Checkable for String}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local storage_live(@1) - @1 := &{impl Super for String}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (24 : usize), align: const (8 : usize), drop: const ({{impl Checkable for String}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for String}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1) } + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl Super for String}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (24 : usize), align: const (8 : usize), drop: const ({{impl Checkable for String}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for String}::check::{vtable_method}<'_>), super_trait_0: move (@1), super_trait_1: move (@2) } return } @@ -681,11 +687,14 @@ fn {impl Checkable for Array}::check::{vtable_meth fn {impl Checkable for Array}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local storage_live(@1) - @1 := &{impl Super for Array}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_0)), align: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_0)), drop: const ({{impl Checkable for Array}}::{vtable}::{drop_method}<'_, const N : usize>), method_check: const ({impl Checkable for Array}::check::{vtable_method}<'_, const N : usize>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1) } + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl Super for Array}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_0)), align: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_0)), drop: const ({{impl Checkable for Array}}::{vtable}::{drop_method}<'_, const N : usize>), method_check: const ({impl Checkable for Array}::check::{vtable_method}<'_, const N : usize>), super_trait_0: move (@1), super_trait_1: move (@2) } return } @@ -805,11 +814,14 @@ fn {impl Checkable for (i32, String)}::check::{vtable_method}<'_0>(@1: &'_0 fn {impl Checkable for (i32, String)}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (test_crate::Super::{vtable} [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Output = i32), i32>::parent_clause1::Output>); // anonymous local storage_live(@1) - @1 := &{impl Super for (i32, String)}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (32 : usize), align: const (8 : usize), drop: const ({{impl Checkable for (i32, String)}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for (i32, String)}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1) } + storage_live(@2) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl Super for (i32, String)}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: const (32 : usize), align: const (8 : usize), drop: const ({{impl Checkable for (i32, String)}}::{vtable}::{drop_method}<'_>), method_check: const ({impl Checkable for (i32, String)}::check::{vtable_method}<'_>), super_trait_0: move (@1), super_trait_1: move (@2) } return } @@ -1089,8 +1101,11 @@ fn {impl NoParam for alloc::boxed::Box[MetaSized, Sized]}::dum fn {impl NoParam for alloc::boxed::Box[MetaSized, Sized]}::{vtable}() -> test_crate::NoParam::{vtable} { let ret@0: test_crate::NoParam::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::NoParam::{vtable} { size: const (Opaque(Layout not available: TODO: handle Box with ptr-metadata)), align: const (Opaque(Layout not available: TODO: handle Box with ptr-metadata)), drop: const ({{impl NoParam for alloc::boxed::Box[MetaSized, Sized]}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for alloc::boxed::Box[MetaSized, Sized]}::dummy::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::NoParam::{vtable} { size: const (Opaque(Layout not available: TODO: handle Box with ptr-metadata)), align: const (Opaque(Layout not available: TODO: handle Box with ptr-metadata)), drop: const ({{impl NoParam for alloc::boxed::Box[MetaSized, Sized]}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for alloc::boxed::Box[MetaSized, Sized]}::dummy::{vtable_method}<'_>), super_trait_0: move (@1) } return } @@ -1166,8 +1181,11 @@ fn {impl NoParam for (i32, i32)}::dummy::{vtable_method}<'_0>(@1: &'_0 ((dyn exi fn {impl NoParam for (i32, i32)}::{vtable}() -> test_crate::NoParam::{vtable} { let ret@0: test_crate::NoParam::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::NoParam::{vtable} { size: const (8 : usize), align: const (4 : usize), drop: const ({{impl NoParam for (i32, i32)}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for (i32, i32)}::dummy::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::NoParam::{vtable} { size: const (8 : usize), align: const (4 : usize), drop: const ({{impl NoParam for (i32, i32)}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for (i32, i32)}::dummy::{vtable_method}<'_>), super_trait_0: move (@1) } return } @@ -1265,8 +1283,11 @@ fn {impl NoParam for Array}::dummy::{vtable_method}<'_0>(@1: &' fn {impl NoParam for Array}::{vtable}() -> test_crate::NoParam::{vtable} { let ret@0: test_crate::NoParam::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::NoParam::{vtable} { size: const (40 : usize), align: const (4 : usize), drop: const ({{impl NoParam for Array}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for Array}::dummy::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::NoParam::{vtable} { size: const (40 : usize), align: const (4 : usize), drop: const ({{impl NoParam for Array}}::{vtable}::{drop_method}<'_>), method_dummy: const ({impl NoParam for Array}::dummy::{vtable_method}<'_>), super_trait_0: move (@1) } return } @@ -1384,8 +1405,11 @@ fn {impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i fn {impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i32, String), const M : usize>), const N : usize>}::{vtable}() -> test_crate::NoParam::{vtable} { let ret@0: test_crate::NoParam::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::NoParam::{vtable} { size: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_1)), align: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_1)), drop: const ({{impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i32, String), const M : usize>), const N : usize>}}::{vtable}::{drop_method}<'_, const N : usize, const M : usize>), method_dummy: const ({impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i32, String), const M : usize>), const N : usize>}::dummy::{vtable_method}<'_, const N : usize, const M : usize>), super_trait_0: const (Opaque(missing supertrait vtable)) } + storage_live(@1) + @1 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::NoParam::{vtable} { size: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_1)), align: const (Opaque(Layout not available: No instant available const generic value or wrong format value: @ConstGeneric0_1)), drop: const ({{impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i32, String), const M : usize>), const N : usize>}}::{vtable}::{drop_method}<'_, const N : usize, const M : usize>), method_dummy: const ({impl NoParam for Array<(String, Array<(i32, i32), const M : usize>, Array<(i32, String), const M : usize>), const N : usize>}::dummy::{vtable_method}<'_, const N : usize, const M : usize>), super_trait_0: move (@1) } return } @@ -1650,8 +1674,11 @@ where [@TraitClause1]: Clone, { let ret@0: test_crate::Modifiable::{vtable}; // return + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local - ret@0 := test_crate::Modifiable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Modifiable for i32}}::{vtable}::{drop_method}<'_, T>[@TraitClause0, @TraitClause1]), 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 := &core::marker::MetaSized::{vtable} + ret@0 := test_crate::Modifiable::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Modifiable for i32}}::{vtable}::{drop_method}<'_, T>[@TraitClause0, @TraitClause1]), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: move (@1) } return } @@ -1926,14 +1953,17 @@ fn {{impl Both32And64 for i32}}::{vtable}::{drop_method}<'_0>(@1: &'_0 mut ((dyn fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} { let ret@0: test_crate::Both32And64::{vtable}; // return - let @1: &'static (test_crate::BaseOn::{vtable}); // anonymous local - let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @1: &'static (core::marker::MetaSized::{vtable}); // anonymous local + let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @3: &'static (test_crate::BaseOn::{vtable}); // anonymous local storage_live(@1) storage_live(@2) - @1 := &{impl BaseOn for i32}::{vtable} - @2 := &{impl BaseOn for i32}::{vtable} - ret@0 := test_crate::Both32And64::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Both32And64 for i32}}::{vtable}::{drop_method}<'_>), 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 (@1), super_trait_2: move (@2) } + storage_live(@3) + @1 := &core::marker::MetaSized::{vtable} + @2 := &{impl BaseOn for i32}::{vtable} + @3 := &{impl BaseOn for i32}::{vtable} + ret@0 := test_crate::Both32And64::{vtable} { size: const (4 : usize), align: const (4 : usize), drop: const ({{impl Both32And64 for i32}}::{vtable}::{drop_method}<'_>), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: move (@1), super_trait_1: move (@2), super_trait_2: move (@3) } return } diff --git a/charon/tests/ui/vtables.rs b/charon/tests/ui/vtables.rs index 99df124eb..64daad57d 100644 --- a/charon/tests/ui/vtables.rs +++ b/charon/tests/ui/vtables.rs @@ -108,6 +108,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; }