charon_driver/translate/
translate_trait_objects.rs

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

charon_driver/translate/
translate_trait_objects.rs
