Vtable Support for Closures

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"
                                         )
                                     }
                                 };

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

@@ -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`].

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())