Skip to content

Supporting vtables for closures #871

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Sam-Ni wants to merge 6 commits into from
Closed

Supporting vtables for closures #871

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7aa1d87
initial vtable support for closures
ssyram Oct 8, 2025
2870141
minor: cargo fmt
Sam-Ni Oct 22, 2025
d0bc90b
rerun of 'make test'
Sam-Ni Oct 24, 2025
18ccb35
refactor gen_vtable_instance_init_body to handle the closure case
Sam-Ni Oct 24, 2025
1e0f973
Merge remote-tracking branch 'upstream/main' into vtable-closure
Sam-Ni Oct 24, 2025
ed5744b
rerun 'make test'
Sam-Ni Oct 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 64 additions & 5 deletions charon/src/bin/charon-driver/translate/translate_bodies.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
)
}
};
Expand Down
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/translate/translate_closures.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
4 changes: 2 additions & 2 deletions charon/src/bin/charon-driver/translate/translate_crate.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`].
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions charon/src/bin/charon-driver/translate/translate_items.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
Expand Down
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/translate/translate_meta.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Loading
Loading