Supporting vtables for closures

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

@@ -582,7 +582,49 @@ impl BodyTransCtx<'_, '_, '_> {
                                             ),
                                         )?)
                                     }
-                                    // TODO(dyn): more ways of registering vtable instance?
+                                    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()
+                                        {
+                                            Some(self.translate_item(
+                                                span,
+                                                &closure_args.item,
+                                                TransItemSourceKind::VTableInstance(
+                                                    TraitImplSource::Closure(closure_kind),
+                                                ),
+                                            )?)
+                                        } else {
+                                            raise_error!(
+                                                self.i_ctx,
+                                                span,
+                                                "Handle non-closure virtual trait implementations."
+                                            );
+                                        }
+                                    }
                                     _ => {
                                         trace!(
                                             "impl_expr not triggering registering vtable: {:?}",

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

@@ -349,7 +349,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,
@@ -745,4 +745,43 @@ impl ItemTransCtx<'_, '_> {
             body,
         })
     }
+
+    pub fn generate_closure_method_shim_ref(
+        &mut self,
+        span: Span,
+        impl_def: &hax::FullDef,
+        closure_kind: ClosureKind,
+    ) -> Result<ConstantExprKind, Error> {
+        // 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))
+    }
 }

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

@@ -77,9 +77,9 @@ 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 drop shim function to be used in the vtable as a field, the ID is an `impl`.
-    VTableDropShim,
+    VTableDropShim(TraitImplSource),
 }
 
 /// The kind of a [`TransItemSourceKind::TraitImpl`].
@@ -294,8 +294,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     | ClosureAsFnCast
                     | DropInPlaceMethod(..)
                     | VTableInstanceInitializer(..)
-                    | VTableMethod
-                    | VTableDropShim => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
+                    | VTableMethod(..)
+                    | VTableDropShim(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
                     InherentImpl | Module => return None,
                 };
                 // Add the id to the queue of declarations to translate

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

@@ -188,18 +188,31 @@ 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 TraitImplSource::Closure(target_kind) =
+                let fun_decl = match impl_kind {
+                    TraitImplSource::Closure(target_kind) => {
+                        let ret = bt_ctx.translate_closure_vtable_shim(
+                            id,
+                            item_meta,
+                            &def,
+                            target_kind,
+                        )?;
+                        // eprintln!("{}", self.translated);
+                        ret
+                    }
+                    _ => bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?,
+                };
                 self.translated.fun_decls.set_slot(id, fun_decl);
             }
-            TransItemSourceKind::VTableDropShim => {
+            TransItemSourceKind::VTableDropShim(impl_kind) => {
                 let Some(ItemId::Fun(id)) = trans_id else {
                     unreachable!()
                 };
-                let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def)?;
+                let fun_decl = bt_ctx.translate_vtable_drop_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

@@ -397,13 +397,13 @@ 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,
                 ));
             }
-            TransItemSourceKind::VTableDropShim => {
+            TransItemSourceKind::VTableDropShim(..) => {
                 name.name.push(PathElem::Ident(
                     "{vtable_drop_shim}".into(),
                     Disambiguator::ZERO,