Skip to content

Commit e289cb9

Browse files
N1arkN1ark
committed
Generate VTable by fields
1 parent 409ff34 commit e289cb9

File tree

1 file changed

+85
-77
lines changed

1 file changed

+85
-77
lines changed

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

Lines changed: 85 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,14 @@ impl ItemTransCtx<'_, '_> {
140140
}
141141
}
142142

143+
enum VTableField {
144+
Size,
145+
Align,
146+
Drop,
147+
Method(hax::DefId, hax::Binder<hax::TyFnSig>),
148+
SuperTrait(hax::Clause),
149+
}
150+
143151
//// Generate the vtable struct.
144152
impl ItemTransCtx<'_, '_> {
145153
/// Query whether a trait is dyn compatible.
@@ -223,68 +231,49 @@ impl ItemTransCtx<'_, '_> {
223231
Ok(Some(vtable_ref))
224232
}
225233

226-
/// Add a `method_name: fn(...) -> ...` field for the method.
227-
fn add_method_to_vtable_def(
234+
fn vtable_fields(
228235
&mut self,
229-
span: Span,
230236
trait_def: &hax::FullDef,
231-
mut mk_field: impl FnMut(String, Ty),
232-
item: &hax::AssocItem,
233-
) -> Result<(), Error> {
234-
let item_def_id = &item.def_id;
235-
let item_def = self.hax_def(
236-
&trait_def
237-
.this()
238-
.with_def_id(&self.t_ctx.hax_state, item_def_id),
239-
)?;
240-
let hax::FullDefKind::AssocFn {
241-
sig,
242-
vtable_sig: Some(_),
243-
..
244-
} = item_def.kind()
245-
else {
246-
return Ok(());
247-
};
248-
249-
let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
250-
// It's ok to translate the method signature in the context of the trait because
251-
// `vtable_sig: Some(_)` ensures the method has no generics of its own.
252-
let sig = self.translate_fun_sig(span, sig)?;
253-
let ty = TyKind::FnPtr(sig).into_ty();
254-
255-
mk_field(format!("method_{}", item_name.0), ty);
256-
Ok(())
257-
}
258-
259-
/// Add `super_trait_n: &'static SuperTraitNVTable` fields.
260-
fn add_supertraits_to_vtable_def(
261-
&mut self,
262-
span: Span,
263-
mut mk_field: impl FnMut(String, Ty),
264237
implied_predicates: &hax::GenericPredicates,
265-
) -> Result<(), Error> {
266-
let mut counter = (0..).into_iter();
238+
) -> Result<Vec<VTableField>, Error> {
239+
let mut fields = vec![];
240+
// Basic fields.
241+
fields.push(VTableField::Size);
242+
fields.push(VTableField::Align);
243+
fields.push(VTableField::Drop);
244+
245+
// Method fields.
246+
if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
247+
for item in items {
248+
let item_def_id = &item.def_id;
249+
let item_def = self.hax_def(
250+
&trait_def
251+
.this()
252+
.with_def_id(&self.t_ctx.hax_state, item_def_id),
253+
)?;
254+
if let hax::FullDefKind::AssocFn {
255+
sig,
256+
vtable_sig: Some(_),
257+
..
258+
} = item_def.kind()
259+
{
260+
fields.push(VTableField::Method(item_def_id.clone(), sig.clone()));
261+
};
262+
}
263+
}
264+
265+
// Supertrait fields.
267266
for (clause, _span) in &implied_predicates.predicates {
268267
if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() {
269268
// If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
270269
if !self.pred_is_for_self(&pred.trait_ref) {
271270
continue;
272271
}
273-
let vtbl_struct = self
274-
.translate_region_binder(span, &clause.kind, |ctx, _| {
275-
ctx.translate_vtable_struct_ref(span, &pred.trait_ref)
276-
})?
277-
.erase()
278-
.expect("parent trait should be dyn compatible");
279-
let ty = Ty::new(TyKind::Ref(
280-
Region::Static,
281-
Ty::new(TyKind::Adt(vtbl_struct)),
282-
RefKind::Shared,
283-
));
284-
mk_field(format!("super_trait_{}", counter.next().unwrap()), ty);
272+
fields.push(VTableField::SuperTrait(clause.clone()));
285273
}
286274
}
287-
Ok(())
275+
276+
Ok(fields)
288277
}
289278

290279
fn gen_vtable_struct_fields(
@@ -294,40 +283,59 @@ impl ItemTransCtx<'_, '_> {
294283
implied_predicates: &hax::GenericPredicates,
295284
) -> Result<Vector<FieldId, Field>, Error> {
296285
let mut fields = Vector::new();
297-
let mut mk_field = |name, ty| {
286+
let mut supertrait_counter = (0..).into_iter();
287+
288+
let fields_list = self.vtable_fields(trait_def, implied_predicates)?;
289+
290+
for field in fields_list.into_iter() {
291+
let (name, ty) = match field {
292+
VTableField::Size => ("size".into(), usize_ty()),
293+
VTableField::Align => ("align".into(), usize_ty()),
294+
VTableField::Drop => {
295+
let self_ty =
296+
TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
297+
let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
298+
let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty((
299+
[self_ptr].into(),
300+
Ty::mk_unit(),
301+
))));
302+
("drop".into(), drop_ty)
303+
}
304+
VTableField::Method(item_def_id, sig) => {
305+
let item_name = self.t_ctx.translate_trait_item_name(&item_def_id)?;
306+
// It's ok to translate the method signature in the context of the trait because
307+
// `vtable_sig: Some(_)` ensures the method has no generics of its own.
308+
let sig = self.translate_fun_sig(span, &sig)?;
309+
let ty = TyKind::FnPtr(sig).into_ty();
310+
(format!("method_{}", item_name.0), ty)
311+
}
312+
VTableField::SuperTrait(clause) => {
313+
let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
314+
unreachable!()
315+
};
316+
let vtbl_struct = self
317+
.translate_region_binder(span, &clause.kind, |ctx, _| {
318+
ctx.translate_vtable_struct_ref(span, &pred.trait_ref)
319+
})?
320+
.erase()
321+
.expect("parent trait should be dyn compatible");
322+
let ty = Ty::new(TyKind::Ref(
323+
Region::Static,
324+
Ty::new(TyKind::Adt(vtbl_struct)),
325+
RefKind::Shared,
326+
));
327+
let name = format!("super_trait_{}", supertrait_counter.next().unwrap());
328+
(name, ty)
329+
}
330+
};
298331
fields.push(Field {
299332
span,
300333
attr_info: dummy_public_attr_info(),
301334
name: Some(name),
302335
ty,
303336
});
304-
};
305-
306-
// Add the basic fields.
307-
// Field: `size: usize`
308-
mk_field("size".into(), usize_ty());
309-
// Field: `align: usize`
310-
mk_field("align".into(), usize_ty());
311-
// Field: `drop: fn(*mut Self)` -- `Self` is just a placeholder, will be dynified below.
312-
mk_field("drop".into(), {
313-
let self_ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
314-
let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
315-
Ty::new(TyKind::FnPtr(RegionBinder::empty((
316-
[self_ptr].into(),
317-
Ty::mk_unit(),
318-
))))
319-
});
320-
321-
// Add the method pointers (trait aliases don't have methods).
322-
if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
323-
for item in items {
324-
self.add_method_to_vtable_def(span, trait_def, &mut mk_field, item)?;
325-
}
326337
}
327338

328-
// Add the supertrait vtables.
329-
self.add_supertraits_to_vtable_def(span, &mut mk_field, implied_predicates)?;
330-
331339
Ok(fields)
332340
}
333341

0 commit comments

Comments
 (0)