charon_driver/translate/
translate_trait_objects.rs

1use super::{
2    translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel,
3};
4
5use charon_lib::ids::Vector;
6use charon_lib::ullbc_ast::*;
7use itertools::Itertools;
8
9fn dummy_public_attr_info() -> AttrInfo {
10    AttrInfo {
11        public: true,
12        ..Default::default()
13    }
14}
15
16fn usize_ty() -> Ty {
17    Ty::new(TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)))
18}
19
20/// Takes a `T` valid in the context of a trait ref and transforms it into a `T` valid in the
21/// context of its vtable definition, i.e. no longer mentions the `Self` type or `Self` clause. If
22/// `new_self` is `Some`, we replace any mention of the `Self` type with it; otherwise we panic if
23/// `Self` is mentioned.
24/// If `for_method` is true, we're handling a value coming from a `AssocFn`, which takes the `Self`
25/// clause as its first clause parameter. Otherwise we're in trait scope, where the `Self` clause
26/// is represented with `TraitRefKind::SelfId`.
27fn dynify<T: TyVisitable>(mut x: T, new_self: Option<Ty>, for_method: bool) -> T {
28    struct ReplaceSelfVisitor {
29        new_self: Option<Ty>,
30        for_method: bool,
31    }
32    impl VarsVisitor for ReplaceSelfVisitor {
33        fn visit_type_var(&mut self, v: TypeDbVar) -> Option<Ty> {
34            if let DeBruijnVar::Bound(DeBruijnId::ZERO, type_id) = v {
35                // Replace type 0 and decrement the others.
36                Some(if let Some(new_id) = type_id.index().checked_sub(1) {
37                    TyKind::TypeVar(DeBruijnVar::Bound(DeBruijnId::ZERO, TypeVarId::new(new_id)))
38                        .into_ty()
39                } else {
40                    self.new_self.clone().expect(
41                        "Found unexpected `Self` 
42                        type when constructing vtable",
43                    )
44                })
45            } else {
46                None
47            }
48        }
49
50        fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
51            if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
52                if self.for_method && clause_id == TraitClauseId::ZERO {
53                    // That's the `Self` clause.
54                    Some(TraitRefKind::Dyn)
55                } else {
56                    panic!("Found unexpected clause var when constructing vtable: {v}")
57                }
58            } else {
59                None
60            }
61        }
62
63        fn visit_self_clause(&mut self) -> Option<TraitRefKind> {
64            Some(TraitRefKind::Dyn)
65        }
66    }
67    x.visit_vars(&mut ReplaceSelfVisitor {
68        new_self,
69        for_method,
70    });
71    x
72}
73
74//// Translate the `dyn Trait` type.
75impl ItemTransCtx<'_, '_> {
76    pub fn check_at_most_one_pred_has_methods(
77        &mut self,
78        span: Span,
79        preds: &hax::GenericPredicates,
80    ) -> Result<(), Error> {
81        // Only the first clause is allowed to have methods.
82        for (clause, _) in preds.predicates.iter().skip(1) {
83            if let hax::ClauseKind::Trait(trait_predicate) = clause.kind.hax_skip_binder_ref() {
84                let trait_def_id = &trait_predicate.trait_ref.def_id;
85                let trait_def = self.poly_hax_def(trait_def_id)?;
86                let has_methods = match trait_def.kind() {
87                    hax::FullDefKind::Trait { items, .. } => items
88                        .iter()
89                        .any(|assoc| matches!(assoc.kind, hax::AssocKind::Fn { .. })),
90                    hax::FullDefKind::TraitAlias { .. } => false,
91                    _ => unreachable!(),
92                };
93                if has_methods {
94                    raise_error!(
95                        self,
96                        span,
97                        "`dyn Trait` with multiple method-bearing predicates is not supported"
98                    );
99                }
100            }
101        }
102        Ok(())
103    }
104
105    pub fn translate_existential_predicates(
106        &mut self,
107        span: Span,
108        self_ty: &hax::ParamTy,
109        preds: &hax::GenericPredicates,
110        region: &hax::Region,
111    ) -> Result<DynPredicate, Error> {
112        // This is a robustness check: the current version of Rustc
113        // accepts at most one method-bearing predicate in a trait object.
114        // But things may change in the future.
115        self.check_at_most_one_pred_has_methods(span, preds)?;
116
117        // Translate the region outside the binder.
118        let region = self.translate_region(span, region)?;
119        let region = region.move_under_binder();
120
121        // Add a binder that contains the existentially quantified type.
122        self.binding_levels.push(BindingLevel::new(true));
123
124        // Add the existentially quantified type.
125        let ty_id = self
126            .innermost_binder_mut()
127            .push_type_var(self_ty.index, self_ty.name.clone());
128        let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty();
129
130        self.innermost_binder_mut()
131            .params
132            .types_outlive
133            .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
134        self.register_predicates(preds, PredicateOrigin::Dyn)?;
135
136        let params = self.binding_levels.pop().unwrap().params;
137        let binder = Binder {
138            params: params,
139            skip_binder: ty,
140            kind: BinderKind::Dyn,
141        };
142        Ok(DynPredicate { binder })
143    }
144}
145
146//// Generate the vtable struct.
147impl ItemTransCtx<'_, '_> {
148    /// Query whether a trait is dyn compatible.
149    /// TODO(dyn): for now we return `false` if the trait has any associated types, as we don't
150    /// handle associated types in vtables.
151    pub fn trait_is_dyn_compatible(&mut self, def_id: &hax::DefId) -> Result<bool, Error> {
152        let def = self.poly_hax_def(def_id)?;
153        Ok(match def.kind() {
154            hax::FullDefKind::Trait { dyn_self, .. }
155            | hax::FullDefKind::TraitAlias { dyn_self, .. } => dyn_self.is_some(),
156            _ => false,
157        })
158    }
159
160    /// Check whether this trait ref is of the form `Self: Trait<...>`.
161    fn pred_is_for_self(&self, tref: &hax::TraitRef) -> bool {
162        let first_ty = tref
163            .generic_args
164            .iter()
165            .filter_map(|arg| match arg {
166                hax::GenericArg::Type(ty) => Some(ty),
167                _ => None,
168            })
169            .next();
170        match first_ty {
171            None => false,
172            Some(first_ty) => match first_ty.kind() {
173                hax::TyKind::Param(param_ty) if param_ty.index == 0 => {
174                    assert_eq!(param_ty.name, "Self");
175                    true
176                }
177                _ => false,
178            },
179        }
180    }
181
182    /// Given a trait ref, return a reference to its vtable struct, if it is dyn compatible.
183    pub fn translate_vtable_struct_ref(
184        &mut self,
185        span: Span,
186        tref: &hax::TraitRef,
187    ) -> Result<Option<TypeDeclRef>, Error> {
188        if !self.trait_is_dyn_compatible(&tref.def_id)? {
189            return Ok(None);
190        }
191        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
192        // `dyn Trait`.
193        let mut vtable_ref: TypeDeclRef =
194            self.translate_item_no_enqueue(span, tref, TransItemSourceKind::VTable)?;
195        // Remove the `Self` type variable from the generic parameters.
196        vtable_ref
197            .generics
198            .types
199            .remove_and_shift_ids(TypeVarId::ZERO);
200
201        // The vtable type also takes associated types as parameters.
202        let assoc_tys: Vec<_> = tref
203            .trait_associated_types(&self.hax_state_with_id())
204            .iter()
205            .map(|ty| self.translate_ty(span, ty))
206            .try_collect()?;
207        vtable_ref.generics.types.extend(assoc_tys);
208
209        Ok(Some(vtable_ref))
210    }
211
212    /// Add a `method_name: fn(...) -> ...` field for the method.
213    fn add_method_to_vtable_def(
214        &mut self,
215        span: Span,
216        trait_def: &hax::FullDef,
217        mut mk_field: impl FnMut(String, Ty),
218        item: &hax::AssocItem,
219    ) -> Result<(), Error> {
220        let item_def_id = &item.def_id;
221        let item_def = self.hax_def(
222            &trait_def
223                .this()
224                .with_def_id(&self.t_ctx.hax_state, item_def_id),
225        )?;
226        let hax::FullDefKind::AssocFn {
227            sig,
228            vtable_safe: true,
229            ..
230        } = item_def.kind()
231        else {
232            return Ok(());
233        };
234
235        let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
236        // It's ok to translate the method signature in the context of the trait because
237        // `vtable_safe: true` ensures the method has no generics of its own.
238        let sig = self.translate_fun_sig(span, sig)?;
239        let ty = TyKind::FnPtr(sig).into_ty();
240
241        mk_field(format!("method_{}", item_name.0), ty);
242        Ok(())
243    }
244
245    /// Add `super_trait_n: &'static SuperTraitNVTable` fields.
246    fn add_supertraits_to_vtable_def(
247        &mut self,
248        span: Span,
249        mut mk_field: impl FnMut(String, Ty),
250        implied_predicates: &hax::GenericPredicates,
251    ) -> Result<(), Error> {
252        let mut counter = (0..).into_iter();
253        for (clause, _span) in &implied_predicates.predicates {
254            if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() {
255                // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
256                if !self.pred_is_for_self(&pred.trait_ref) {
257                    continue;
258                }
259                let vtbl_struct = self
260                    .translate_region_binder(span, &clause.kind, |ctx, _| {
261                        ctx.translate_vtable_struct_ref(span, &pred.trait_ref)
262                    })?
263                    .erase()
264                    .expect("parent trait should be dyn compatible");
265                let ty = Ty::new(TyKind::Ref(
266                    Region::Static,
267                    Ty::new(TyKind::Adt(vtbl_struct)),
268                    RefKind::Shared,
269                ));
270                mk_field(format!("super_trait_{}", counter.next().unwrap()), ty);
271            }
272        }
273        Ok(())
274    }
275
276    fn gen_vtable_struct_fields(
277        &mut self,
278        span: Span,
279        trait_def: &hax::FullDef,
280        implied_predicates: &hax::GenericPredicates,
281    ) -> Result<Vector<FieldId, Field>, Error> {
282        let mut fields = Vector::new();
283        let mut mk_field = |name, ty| {
284            fields.push(Field {
285                span,
286                attr_info: dummy_public_attr_info(),
287                name: Some(name),
288                ty,
289            });
290        };
291
292        // Add the basic fields.
293        // Field: `size: usize`
294        mk_field("size".into(), usize_ty());
295        // Field: `align: usize`
296        mk_field("align".into(), usize_ty());
297        // Field: `drop: fn(*mut Self)`
298        mk_field("drop".into(), {
299            let self_ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
300            let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
301            Ty::new(TyKind::FnPtr(RegionBinder::empty((
302                [self_ptr].into(),
303                Ty::mk_unit(),
304            ))))
305        });
306
307        // Add the method pointers (trait aliases don't have methods).
308        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
309            for item in items {
310                self.add_method_to_vtable_def(span, trait_def, &mut mk_field, item)?;
311            }
312        }
313
314        // Add the supertrait vtables.
315        self.add_supertraits_to_vtable_def(span, &mut mk_field, implied_predicates)?;
316
317        Ok(fields)
318    }
319
320    /// Construct the type of the vtable for this trait.
321    ///
322    /// It's a struct that has for generics the generics of the trait + one parameter for each
323    /// associated type of the trait and its parents.
324    /// TODO(dyn): add the associated types.
325    ///
326    /// struct TraitVTable<TraitArgs.., AssocTys..> {
327    ///   size: usize,
328    ///   align: usize,
329    ///   drop: fn(*mut dyn Trait<...>),
330    ///   method_name: fn(&dyn Trait<...>, Args..) -> Output,
331    ///   ... other methods
332    ///   super_trait_0: &'static SuperTrait0VTable
333    ///   ... other supertraits
334    /// }
335    pub(crate) fn translate_vtable_struct(
336        mut self,
337        type_id: TypeDeclId,
338        item_meta: ItemMeta,
339        trait_def: &hax::FullDef,
340    ) -> Result<TypeDecl, Error> {
341        let span = item_meta.span;
342        if !self.trait_is_dyn_compatible(trait_def.def_id())? {
343            raise_error!(
344                self,
345                span,
346                "Trying to compute the vtable type \
347                for a non-dyn-compatible trait"
348            );
349        }
350
351        self.translate_def_generics(span, trait_def)?;
352
353        let (hax::FullDefKind::Trait {
354            dyn_self,
355            implied_predicates,
356            ..
357        }
358        | hax::FullDefKind::TraitAlias {
359            dyn_self,
360            implied_predicates,
361            ..
362        }) = trait_def.kind()
363        else {
364            panic!()
365        };
366        let Some(dyn_self) = dyn_self else {
367            panic!("Trying to generate a vtable for a non-dyn-compatible trait")
368        };
369
370        // The `dyn Trait<Args..>` type for this trait.
371        let mut dyn_self = {
372            let dyn_self = self.translate_ty(span, dyn_self)?;
373            let TyKind::DynTrait(mut dyn_pred) = dyn_self.kind().clone() else {
374                panic!("incorrect `dyn_self`")
375            };
376
377            // Add one generic parameter for each associated type of this trait and its parents. We
378            // then use that in `dyn_self`
379            for (i, ty_constraint) in dyn_pred
380                .binder
381                .params
382                .trait_type_constraints
383                .iter_mut()
384                .enumerate()
385            {
386                let name = format!("Ty{i}");
387                let new_ty = self
388                    .the_only_binder_mut()
389                    .params
390                    .types
391                    .push_with(|index| TypeVar { index, name });
392                // Moving that type under two levels of binders: the `DynPredicate` binder and the
393                // type constraint binder.
394                let new_ty =
395                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::new(2), new_ty)).into_ty();
396                ty_constraint.skip_binder.ty = new_ty;
397            }
398            TyKind::DynTrait(dyn_pred).into_ty()
399        };
400
401        // First construct fields that use the real method signatures (which may use the `Self`
402        // type). We fixup the types and generics below.
403        let fields = self.gen_vtable_struct_fields(span, trait_def, implied_predicates)?;
404        let mut kind = TypeDeclKind::Struct(fields);
405        let layout = self.generate_naive_layout(span, &kind)?;
406
407        // Replace any use of `Self` with `dyn Trait<...>`, and remove the `Self` type variable
408        // from the generic parameters.
409        let mut generics = self.into_generics();
410        {
411            dyn_self = dynify(dyn_self, None, false);
412            generics = dynify(generics, Some(dyn_self.clone()), false);
413            kind = dynify(kind, Some(dyn_self.clone()), true);
414            generics.types.remove_and_shift_ids(TypeVarId::ZERO);
415            generics.types.iter_mut().for_each(|ty| {
416                ty.index -= 1;
417            });
418        }
419
420        let dyn_predicate = dyn_self
421            .kind()
422            .as_dyn_trait()
423            .expect("incorrect `dyn_self`");
424        Ok(TypeDecl {
425            def_id: type_id,
426            item_meta: item_meta,
427            generics: generics,
428            src: ItemKind::VTableTy {
429                dyn_predicate: dyn_predicate.clone(),
430            },
431            kind,
432            layout: Some(layout),
433            ptr_metadata: None,
434        })
435    }
436}
437
438//// Generate a vtable value.
439impl ItemTransCtx<'_, '_> {
440    pub fn translate_vtable_instance_ref(
441        &mut self,
442        span: Span,
443        trait_ref: &hax::TraitRef,
444        impl_ref: &hax::ItemRef,
445    ) -> Result<Option<GlobalDeclRef>, Error> {
446        if !self.trait_is_dyn_compatible(&trait_ref.def_id)? {
447            return Ok(None);
448        }
449        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
450        // `dyn Trait` coercion.
451        // TODO(dyn): To do this properly we'd need to know for each clause whether it ultimately
452        // ends up used in a vtable cast.
453        let vtable_ref: GlobalDeclRef = self.translate_item_no_enqueue(
454            span,
455            impl_ref,
456            TransItemSourceKind::VTableInstance(TraitImplSource::Normal),
457        )?;
458        Ok(Some(vtable_ref))
459    }
460
461    /// Local helper function to get the vtable struct reference and trait declaration reference
462    fn get_vtable_instance_info<'a>(
463        &mut self,
464        span: Span,
465        impl_def: &'a hax::FullDef,
466        impl_kind: &TraitImplSource,
467    ) -> Result<(TraitImplRef, TraitDeclRef, TypeDeclRef), Error> {
468        let implemented_trait = match impl_def.kind() {
469            hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref,
470            _ => unreachable!(),
471        };
472        let vtable_struct_ref = self
473            .translate_vtable_struct_ref(span, implemented_trait)?
474            .expect("trait should be dyn-compatible");
475        let implemented_trait = self.translate_trait_decl_ref(span, implemented_trait)?;
476        let impl_ref = self.translate_item(
477            span,
478            impl_def.this(),
479            TransItemSourceKind::TraitImpl(*impl_kind),
480        )?;
481        Ok((impl_ref, implemented_trait, vtable_struct_ref))
482    }
483
484    /// E.g.,
485    /// global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
486    ///     size: size_of(Foo),
487    ///     align: align_of(Foo),
488    ///     drop: <Foo as Drop>::drop,
489    ///     method_0: <Foo as Trait>::method_0::{shim},
490    ///     method_1: <Foo as Trait>::method_1::{shim},
491    ///     ...
492    ///     super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
493    ///     super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
494    ///     ...
495    /// }
496    pub(crate) fn translate_vtable_instance(
497        mut self,
498        global_id: GlobalDeclId,
499        item_meta: ItemMeta,
500        impl_def: &hax::FullDef,
501        impl_kind: &TraitImplSource,
502    ) -> Result<GlobalDecl, Error> {
503        let span = item_meta.span;
504        self.translate_def_generics(span, impl_def)?;
505
506        let (impl_ref, _, vtable_struct_ref) =
507            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
508        // Initializer function for this global.
509        let init = self.register_item(
510            span,
511            impl_def.this(),
512            TransItemSourceKind::VTableInstanceInitializer(*impl_kind),
513        );
514
515        Ok(GlobalDecl {
516            def_id: global_id,
517            item_meta,
518            generics: self.into_generics(),
519            kind: ItemKind::VTableInstance { impl_ref },
520            // it should be static to have its own address
521            global_kind: GlobalKind::Static,
522            ty: Ty::new(TyKind::Adt(vtable_struct_ref)),
523            init,
524        })
525    }
526
527    fn add_method_to_vtable_value(
528        &mut self,
529        span: Span,
530        impl_def: &hax::FullDef,
531        item: &hax::ImplAssocItem,
532        mut mk_field: impl FnMut(ConstantExprKind),
533    ) -> Result<(), Error> {
534        // Exit if the item isn't a vtable safe method.
535        match self.poly_hax_def(&item.decl_def_id)?.kind() {
536            hax::FullDefKind::AssocFn {
537                vtable_safe: true, ..
538            } => {}
539            _ => return Ok(()),
540        }
541
542        let const_kind = match &item.value {
543            hax::ImplAssocItemValue::Provided {
544                def_id: item_def_id,
545                ..
546            } => {
547                // The method is vtable safe so it has no generics, hence we can reuse the impl
548                // generics.
549                let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id);
550                let shim_ref =
551                    self.translate_item(span, &item_ref, TransItemSourceKind::VTableMethod)?;
552                ConstantExprKind::FnPtr(shim_ref)
553            }
554            hax::ImplAssocItemValue::DefaultedFn { .. } => ConstantExprKind::Opaque(
555                "shim for provided methods \
556                    aren't yet supported"
557                    .to_string(),
558            ),
559            _ => return Ok(()),
560        };
561
562        mk_field(const_kind);
563
564        Ok(())
565    }
566
567    fn add_supertraits_to_vtable_value(
568        &mut self,
569        span: Span,
570        trait_def: &hax::FullDef,
571        impl_def: &hax::FullDef,
572        mut mk_field: impl FnMut(ConstantExprKind),
573    ) -> Result<(), Error> {
574        let hax::FullDefKind::TraitImpl {
575            implied_impl_exprs, ..
576        } = impl_def.kind()
577        else {
578            unreachable!()
579        };
580        let hax::FullDefKind::Trait {
581            implied_predicates, ..
582        } = trait_def.kind()
583        else {
584            unreachable!()
585        };
586        for ((clause, _), impl_expr) in implied_predicates.predicates.iter().zip(implied_impl_exprs)
587        {
588            let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
589                continue;
590            };
591            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
592            if !self.pred_is_for_self(&pred.trait_ref) {
593                continue;
594            }
595
596            let vtable_def_ref = self
597                .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
598                    ctx.translate_vtable_struct_ref(span, tref)
599                })?
600                .erase()
601                .expect("parent trait should be dyn compatible");
602            let fn_ptr_ty = TyKind::Adt(vtable_def_ref).into_ty();
603            let kind = match &impl_expr.r#impl {
604                hax::ImplExprAtom::Concrete(impl_item) => {
605                    let vtable_instance_ref = self
606                        .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
607                            ctx.translate_vtable_instance_ref(span, tref, impl_item)
608                        })?
609                        .erase()
610                        .expect("parent trait should be dyn compatible");
611                    let global = Box::new(ConstantExpr {
612                        value: ConstantExprKind::Global(vtable_instance_ref),
613                        ty: fn_ptr_ty,
614                    });
615                    ConstantExprKind::Ref(global)
616                }
617                // TODO(dyn): builtin impls
618                _ => ConstantExprKind::Opaque("missing supertrait vtable".into()),
619            };
620            mk_field(kind);
621        }
622        Ok(())
623    }
624
625    /// Generate the body of the vtable instance function.
626    /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls.
627    /// ```ignore
628    /// let ret@0 : VTable;
629    /// ret@0 = VTable { ... };
630    /// return;
631    /// ```
632    fn gen_vtable_instance_init_body(
633        &mut self,
634        span: Span,
635        impl_def: &hax::FullDef,
636        vtable_struct_ref: TypeDeclRef,
637    ) -> Result<Body, Error> {
638        let mut locals = Locals {
639            arg_count: 0,
640            locals: Vector::new(),
641        };
642        let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone()));
643        let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone());
644
645        let hax::FullDefKind::TraitImpl {
646            trait_pred, items, ..
647        } = impl_def.kind()
648        else {
649            unreachable!()
650        };
651        let trait_def = self.hax_def(&trait_pred.trait_ref)?;
652
653        // Retreive the expected field types from the struct definition. This avoids complicated
654        // substitutions.
655        let field_tys = {
656            let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone();
657            let AnyTransItem::Type(vtable_def) =
658                self.t_ctx.get_or_translate(vtable_decl_id.into())?
659            else {
660                unreachable!()
661            };
662            let TypeDeclKind::Struct(fields) = &vtable_def.kind else {
663                unreachable!()
664            };
665            fields
666                .iter()
667                .map(|f| &f.ty)
668                .cloned()
669                .map(|ty| ty.substitute(&vtable_struct_ref.generics))
670                .collect_vec()
671        };
672
673        let mut statements = vec![];
674        let mut aggregate_fields = vec![];
675        // For each vtable field, assign the desired value to a new local.
676        let mut field_ty_iter = field_tys.into_iter();
677        let mut mk_field = |kind| {
678            let ty = field_ty_iter.next().unwrap();
679            aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { value: kind, ty })));
680        };
681
682        // TODO(dyn): provide values
683        mk_field(ConstantExprKind::Opaque("unknown size".to_string()));
684        mk_field(ConstantExprKind::Opaque("unknown align".to_string()));
685        mk_field(ConstantExprKind::Opaque("unknown drop".to_string()));
686
687        for item in items {
688            self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?;
689        }
690
691        self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?;
692
693        if field_ty_iter.next().is_some() {
694            raise_error!(
695                self,
696                span,
697                "Missed some fields in vtable value construction"
698            )
699        }
700
701        // Construct the final struct.
702        statements.push(Statement::new(
703            span,
704            StatementKind::Assign(
705                ret_place,
706                Rvalue::Aggregate(
707                    AggregateKind::Adt(vtable_struct_ref.clone(), None, None),
708                    aggregate_fields,
709                ),
710            ),
711        ));
712
713        let block = BlockData {
714            statements,
715            terminator: Terminator::new(span, TerminatorKind::Return),
716        };
717
718        Ok(Body::Unstructured(GExprBody {
719            span,
720            locals,
721            comments: Vec::new(),
722            body: [block].into(),
723        }))
724    }
725
726    pub(crate) fn translate_vtable_instance_init(
727        mut self,
728        init_func_id: FunDeclId,
729        item_meta: ItemMeta,
730        impl_def: &hax::FullDef,
731        impl_kind: &TraitImplSource,
732    ) -> Result<FunDecl, Error> {
733        let span = item_meta.span;
734        self.translate_def_generics(span, impl_def)?;
735
736        let (impl_ref, _, vtable_struct_ref) =
737            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
738        let init_for = self.register_item(
739            span,
740            impl_def.this(),
741            TransItemSourceKind::VTableInstance(*impl_kind),
742        );
743
744        // Signature: `() -> VTable`.
745        let sig = FunSig {
746            is_unsafe: false,
747            generics: self.the_only_binder().params.clone(),
748            inputs: vec![],
749            output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())),
750        };
751
752        let body = match impl_kind {
753            TraitImplSource::Normal => {
754                let body = self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?;
755                Ok(body)
756            }
757            _ => {
758                raise_error!(
759                    self,
760                    span,
761                    "Don't know how to generate a vtable for a virtual impl {impl_kind:?}"
762                );
763            }
764        };
765
766        Ok(FunDecl {
767            def_id: init_func_id,
768            item_meta: item_meta,
769            signature: sig,
770            kind: ItemKind::VTableInstance { impl_ref },
771            is_global_initializer: Some(init_for),
772            body,
773        })
774    }
775
776    // pub(crate) fn translate_vtable_shim(
777    //     self,
778    //     _fun_id: FunDeclId,
779    //     item_meta: ItemMeta,
780    //     _impl_func_def: &hax::FullDef,
781    // ) -> Result<FunDecl, Error> {
782    //     let span = item_meta.span;
783    //     raise_error!(self, span, "unimplemented")
784    // }
785}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
