Supporting vtables for closures

charon/src/bin/charon-driver/translate/translate_bodies.rs

@@ -529,11 +529,70 @@ impl BodyTransCtx<'_, '_, '_> {
                                             ),
                                         );
                                     }
-                                    // TODO(dyn): more ways of registering vtable instance?
-                                    _ => {
-                                        trace!(
-                                            "impl_expr not triggering registering vtable: {:?}",
-                                            impl_expr
+                                    hax::ImplExprAtom::Builtin { .. } => {
+                                        // Handle built-in implementations, including closures
+                                        let tref = &impl_expr.r#trait;
+                                        let hax_state = self.hax_state_with_id().clone();
+                                        let trait_def = self.hax_def(
+                                            &tref.hax_skip_binder_ref().erase(&hax_state),
+                                        )?;
+                                        let closure_kind =
+                                            trait_def.lang_item.as_deref().and_then(|lang| {
+                                                match lang {
+                                                    "fn_once" => Some(ClosureKind::FnOnce),
+                                                    "fn_mut" => Some(ClosureKind::FnMut),
+                                                    "fn" | "r#fn" => Some(ClosureKind::Fn),
+                                                    _ => None,
+                                                }
+                                            });
+
+                                        // Check if this is a closure trait implementation
+                                        if let Some(closure_kind) = closure_kind
+                                            && let Some(hax::GenericArg::Type(closure_ty)) =
+                                                impl_expr
+                                                    .r#trait
+                                                    .hax_skip_binder_ref()
+                                                    .generic_args
+                                                    .first()
+                                            && let hax::TyKind::Closure(closure_args) =
+                                                closure_ty.kind()
+                                        {
+                                            // Register the closure vtable instance
+                                            let _: GlobalDeclId = self.register_item(
+                                                span,
+                                                &closure_args.item,
+                                                TransItemSourceKind::VTableInstance(
+                                                    TraitImplSource::Closure(closure_kind),
+                                                ),
+                                            );
+                                        } else {
+                                            raise_error!(
+                                                self.i_ctx,
+                                                span,
+                                                "Handle non-closure virtual trait implementations."
+                                            );
+                                        }
+                                    }
+                                    hax::ImplExprAtom::LocalBound { .. } => {
+                                        // No need to register anything here as there is no concrete impl
+                                        // This results in that: the vtable instance in generic case might not exist
+                                        // But this case should not happen in the monomorphized case
+                                        if self.monomorphize() {
+                                            raise_error!(
+                                                self.i_ctx,
+                                                span,
+                                                "Unexpected `LocalBound` in monomorphized context"
+                                            )
+                                        }
+                                    }
+                                    hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => {
+                                        // No need to register anything for these cases
+                                    }
+                                    hax::ImplExprAtom::SelfImpl { .. } => {
+                                        raise_error!(
+                                            self.i_ctx,
+                                            span,
+                                            "`SelfImpl` should not appear in the function body"
                                         )
                                     }
                                 };

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,

charon/src/bin/charon-driver/translate/translate_crate.rs

@@ -76,7 +76,7 @@ pub enum TransItemSourceKind {
     /// Shim function to store a method in a vtable; give a method with `self: Ptr<Self>` argument,
     /// this takes a `Ptr<dyn Trait>` and forwards to the method. The `DefId` refers to the method
     /// implementation.
-    VTableMethod,
+    VTableMethod(TraitImplSource),
 }
 
 /// The kind of a [`TransItemSourceKind::TraitImpl`].
@@ -293,7 +293,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     | EmptyDropMethod
                     | DropInPlaceMethod(..)
                     | VTableInstanceInitializer(..)
-                    | VTableMethod => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
+                    | VTableMethod(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
                     InherentImpl | Module => return None,
                 };
                 // Add the id to the queue of declarations to translate
@@ -438,7 +438,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
     }
 
     /// Register this item and don't enqueue it for translation.
-    #[expect(dead_code)]
     pub(crate) fn translate_item_no_enqueue<T: TryFrom<DeclRef<ItemId>>>(
         &mut self,
         span: Span,

charon/src/bin/charon-driver/translate/translate_items.rs

@@ -175,11 +175,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?;
                 self.translated.fun_decls.set_slot(id, fun_decl);
             }
-            TransItemSourceKind::VTableMethod => {
+            TransItemSourceKind::VTableMethod(impl_kind) => {
                 let Some(ItemId::Fun(id)) = trans_id else {
                     unreachable!()
                 };
-                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
+                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?;
                 self.translated.fun_decls.set_slot(id, fun_decl);
             }
         }

charon/src/bin/charon-driver/translate/translate_meta.rs

@@ -368,7 +368,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                 name.name
                     .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
             }
-            TransItemSourceKind::VTableMethod => {
+            TransItemSourceKind::VTableMethod(..) => {
                 name.name.push(PathElem::Ident(
                     "{vtable_method}".into(),
                     Disambiguator::ZERO,