Skip to content

Commit c8cab33

Browse files
ssyramssyram
committed
initial vtable support for closures
TODO: fix the `translate_vtable_shim` part, then remove the "//@ known-failure" in the test `simple/dyn-fn` example
1 parent c1db667 commit c8cab33

File tree

13 files changed

+587
-331
lines changed

13 files changed

+587
-331
lines changed

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

Lines changed: 64 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -529,11 +529,70 @@ impl BodyTransCtx<'_, '_, '_> {
529529
),
530530
);
531531
}
532-
// TODO(dyn): more ways of registering vtable instance?
533-
_ => {
534-
trace!(
535-
"impl_expr not triggering registering vtable: {:?}",
536-
impl_expr
532+
hax::ImplExprAtom::Builtin { .. } => {
533+
// Handle built-in implementations, including closures
534+
let tref = &impl_expr.r#trait;
535+
let hax_state = self.hax_state_with_id();
536+
let trait_def = self.hax_def(
537+
&tref.hax_skip_binder_ref().erase(&hax_state),
538+
)?;
539+
let closure_kind =
540+
trait_def.lang_item.as_deref().and_then(|lang| {
541+
match lang {
542+
"fn_once" => Some(ClosureKind::FnOnce),
543+
"fn_mut" => Some(ClosureKind::FnMut),
544+
"fn" | "r#fn" => Some(ClosureKind::Fn),
545+
_ => None,
546+
}
547+
});
548+
549+
// Check if this is a closure trait implementation
550+
if let Some(closure_kind) = closure_kind
551+
&& let Some(hax::GenericArg::Type(closure_ty)) =
552+
impl_expr
553+
.r#trait
554+
.hax_skip_binder_ref()
555+
.generic_args
556+
.first()
557+
&& let hax::TyKind::Closure(closure_args) =
558+
closure_ty.kind()
559+
{
560+
// Register the closure vtable instance
561+
let _: GlobalDeclId = self.register_item(
562+
span,
563+
&closure_args.item,
564+
TransItemSourceKind::VTableInstance(
565+
TraitImplSource::Closure(closure_kind),
566+
),
567+
);
568+
} else {
569+
raise_error!(
570+
self.i_ctx,
571+
span,
572+
"Handle non-closure virtual trait implementations."
573+
);
574+
}
575+
}
576+
hax::ImplExprAtom::LocalBound { .. } => {
577+
// No need to register anything here as there is no concrete impl
578+
// This results in that: the vtable instance in generic case might not exist
579+
// But this case should not happen in the monomorphized case
580+
if self.monomorphize() {
581+
raise_error!(
582+
self.i_ctx,
583+
span,
584+
"Unexpected `LocalBound` in monomorphized context"
585+
)
586+
}
587+
}
588+
hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => {
589+
// No need to register anything for these cases
590+
}
591+
hax::ImplExprAtom::SelfImpl { .. } => {
592+
raise_error!(
593+
self.i_ctx,
594+
span,
595+
"`SelfImpl` should not appear in the function body"
537596
)
538597
}
539598
};

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -282,7 +282,7 @@ impl ItemTransCtx<'_, '_> {
282282

283283
/// Given an item that is a closure, generate the signature of the
284284
/// `call_once`/`call_mut`/`call` method (depending on `target_kind`).
285-
fn translate_closure_method_sig(
285+
pub fn translate_closure_method_sig(
286286
&mut self,
287287
def: &hax::FullDef,
288288
span: Span,

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ pub enum TransItemSourceKind {
6969
/// Shim function to store a method in a vtable; give a method with `self: Ptr<Self>` argument,
7070
/// this takes a `Ptr<dyn Trait>` and forwards to the method. The `DefId` refers to the method
7171
/// implementation.
72-
VTableMethod,
72+
VTableMethod(TraitImplSource),
7373
}
7474

7575
/// The kind of a [`TransItemSourceKind::TraitImpl`].
@@ -282,7 +282,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
282282
| ClosureAsFnCast
283283
| DropGlueMethod
284284
| VTableInstanceInitializer(..)
285-
| VTableMethod => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
285+
| VTableMethod(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
286286
InherentImpl | Module => return None,
287287
};
288288
// Add the id to the queue of declarations to translate

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -164,11 +164,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
164164
bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?;
165165
self.translated.fun_decls.set_slot(id, fun_decl);
166166
}
167-
TransItemSourceKind::VTableMethod => {
167+
TransItemSourceKind::VTableMethod(impl_kind) => {
168168
let Some(ItemId::Fun(id)) = trans_id else {
169169
unreachable!()
170170
};
171-
let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
171+
let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?;
172172
self.translated.fun_decls.set_slot(id, fun_decl);
173173
}
174174
}
@@ -187,6 +187,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
187187
let span = self.def_span(item_source.def_id());
188188
raise_error!(self, span, "Failed to translate item {id:?}.")
189189
}
190+
// This prevents re-translating of the same item in the usual queue processing loop.
191+
// If this is not present, if the function is called before the usual processing loop,
192+
// `processed` does not record the item as processed, and we end up translating it again.
193+
self.processed.insert(item_source);
190194
}
191195
let item = self.translated.get_item(id);
192196
Ok(item.unwrap())

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -362,7 +362,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
362362
name.name
363363
.push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
364364
}
365-
TransItemSourceKind::VTableMethod => {
365+
TransItemSourceKind::VTableMethod(..) => {
366366
name.name.push(PathElem::Ident(
367367
"{vtable_method}".into(),
368368
Disambiguator::ZERO,

0 commit comments

Comments
 (0)