charon_driver/translate/
translate_trait_objects.rs

1use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
2use itertools::Itertools;
3use std::mem;
4
5use super::{
6    translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel,
7};
8use charon_lib::formatter::IntoFormatter;
9use charon_lib::ids::Vector;
10use charon_lib::pretty::FmtWithCtx;
11use charon_lib::ullbc_ast::*;
12
13fn dummy_public_attr_info() -> AttrInfo {
14    AttrInfo {
15        public: true,
16        ..Default::default()
17    }
18}
19
20fn usize_ty() -> Ty {
21    Ty::new(TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)))
22}
23
24/// Takes a `T` valid in the context of a trait ref and transforms it into a `T` valid in the
25/// context of its vtable definition, i.e. no longer mentions the `Self` type or `Self` clause. If
26/// `new_self` is `Some`, we replace any mention of the `Self` type with it; otherwise we panic if
27/// `Self` is mentioned.
28/// If `for_method` is true, we're handling a value coming from a `AssocFn`, which takes the `Self`
29/// clause as its first clause parameter. Otherwise we're in trait scope, where the `Self` clause
30/// is represented with `TraitRefKind::SelfId`.
31fn dynify<T: TyVisitable>(mut x: T, new_self: Option<Ty>, for_method: bool) -> T {
32    struct ReplaceSelfVisitor {
33        new_self: Option<Ty>,
34        for_method: bool,
35    }
36    impl VarsVisitor for ReplaceSelfVisitor {
37        fn visit_type_var(&mut self, v: TypeDbVar) -> Option<Ty> {
38            if let DeBruijnVar::Bound(DeBruijnId::ZERO, type_id) = v {
39                // Replace type 0 and decrement the others.
40                Some(if let Some(new_id) = type_id.index().checked_sub(1) {
41                    TyKind::TypeVar(DeBruijnVar::Bound(DeBruijnId::ZERO, TypeVarId::new(new_id)))
42                        .into_ty()
43                } else {
44                    self.new_self.clone().expect(
45                        "Found unexpected `Self` 
46                        type when constructing vtable",
47                    )
48                })
49            } else {
50                None
51            }
52        }
53
54        fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
55            if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
56                if self.for_method && clause_id == TraitClauseId::ZERO {
57                    // That's the `Self` clause.
58                    Some(TraitRefKind::Dyn)
59                } else {
60                    panic!("Found unexpected clause var when constructing vtable: {v}")
61                }
62            } else {
63                None
64            }
65        }
66
67        fn visit_self_clause(&mut self) -> Option<TraitRefKind> {
68            Some(TraitRefKind::Dyn)
69        }
70    }
71    x.visit_vars(&mut ReplaceSelfVisitor {
72        new_self,
73        for_method,
74    });
75    x
76}
77
78//// Translate the `dyn Trait` type.
79impl ItemTransCtx<'_, '_> {
80    pub fn check_at_most_one_pred_has_methods(
81        &mut self,
82        span: Span,
83        preds: &hax::GenericPredicates,
84    ) -> Result<(), Error> {
85        // Only the first clause is allowed to have methods.
86        for (clause, _) in preds.predicates.iter().skip(1) {
87            if let hax::ClauseKind::Trait(trait_predicate) = clause.kind.hax_skip_binder_ref() {
88                let trait_def_id = &trait_predicate.trait_ref.def_id;
89                let trait_def = self.poly_hax_def(trait_def_id)?;
90                let has_methods = match trait_def.kind() {
91                    hax::FullDefKind::Trait { items, .. } => items
92                        .iter()
93                        .any(|assoc| matches!(assoc.kind, hax::AssocKind::Fn { .. })),
94                    hax::FullDefKind::TraitAlias { .. } => false,
95                    _ => unreachable!(),
96                };
97                if has_methods {
98                    raise_error!(
99                        self,
100                        span,
101                        "`dyn Trait` with multiple method-bearing predicates is not supported"
102                    );
103                }
104            }
105        }
106        Ok(())
107    }
108
109    pub fn translate_existential_predicates(
110        &mut self,
111        span: Span,
112        self_ty: &hax::ParamTy,
113        preds: &hax::GenericPredicates,
114        region: &hax::Region,
115    ) -> Result<DynPredicate, Error> {
116        // This is a robustness check: the current version of Rustc
117        // accepts at most one method-bearing predicate in a trait object.
118        // But things may change in the future.
119        self.check_at_most_one_pred_has_methods(span, preds)?;
120
121        // Translate the region outside the binder.
122        let region = self.translate_region(span, region)?;
123        let region = region.move_under_binder();
124
125        // Add a binder that contains the existentially quantified type.
126        self.binding_levels.push(BindingLevel::new(true));
127
128        // Add the existentially quantified type.
129        let ty_id = self
130            .innermost_binder_mut()
131            .push_type_var(self_ty.index, self_ty.name.clone());
132        let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty();
133
134        self.innermost_binder_mut()
135            .params
136            .types_outlive
137            .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
138        self.register_predicates(preds, PredicateOrigin::Dyn)?;
139
140        let params = self.binding_levels.pop().unwrap().params;
141        let binder = Binder {
142            params: params,
143            skip_binder: ty,
144            kind: BinderKind::Dyn,
145        };
146        Ok(DynPredicate { binder })
147    }
148}
149
150//// Generate the vtable struct.
151impl ItemTransCtx<'_, '_> {
152    /// Query whether a trait is dyn compatible.
153    /// TODO(dyn): for now we return `false` if the trait has any associated types, as we don't
154    /// handle associated types in vtables.
155    pub fn trait_is_dyn_compatible(&mut self, def_id: &hax::DefId) -> Result<bool, Error> {
156        let def = self.poly_hax_def(def_id)?;
157        Ok(match def.kind() {
158            hax::FullDefKind::Trait { dyn_self, .. }
159            | hax::FullDefKind::TraitAlias { dyn_self, .. } => dyn_self.is_some(),
160            _ => false,
161        })
162    }
163
164    /// Check whether this trait ref is of the form `Self: Trait<...>`.
165    fn pred_is_for_self(&self, tref: &hax::TraitRef) -> bool {
166        let first_ty = tref
167            .generic_args
168            .iter()
169            .filter_map(|arg| match arg {
170                hax::GenericArg::Type(ty) => Some(ty),
171                _ => None,
172            })
173            .next();
174        match first_ty {
175            None => false,
176            Some(first_ty) => match first_ty.kind() {
177                hax::TyKind::Param(param_ty) if param_ty.index == 0 => {
178                    assert_eq!(param_ty.name, "Self");
179                    true
180                }
181                _ => false,
182            },
183        }
184    }
185
186    pub fn translate_vtable_struct_ref(
187        &mut self,
188        span: Span,
189        tref: &hax::TraitRef,
190    ) -> Result<Option<TypeDeclRef>, Error> {
191        self.translate_vtable_struct_ref_maybe_enqueue(true, span, tref)
192    }
193
194    pub fn translate_vtable_struct_ref_no_enqueue(
195        &mut self,
196        span: Span,
197        tref: &hax::TraitRef,
198    ) -> Result<Option<TypeDeclRef>, Error> {
199        self.translate_vtable_struct_ref_maybe_enqueue(false, span, tref)
200    }
201
202    /// Given a trait ref, return a reference to its vtable struct, if it is dyn compatible.
203    pub fn translate_vtable_struct_ref_maybe_enqueue(
204        &mut self,
205        enqueue: bool,
206        span: Span,
207        tref: &hax::TraitRef,
208    ) -> Result<Option<TypeDeclRef>, Error> {
209        if !self.trait_is_dyn_compatible(&tref.def_id)? {
210            return Ok(None);
211        }
212        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
213        // `dyn Trait`.
214        let mut vtable_ref: TypeDeclRef =
215            self.translate_item_maybe_enqueue(span, enqueue, tref, TransItemSourceKind::VTable)?;
216        // Remove the `Self` type variable from the generic parameters.
217        vtable_ref
218            .generics
219            .types
220            .remove_and_shift_ids(TypeVarId::ZERO);
221
222        // The vtable type also takes associated types as parameters.
223        let assoc_tys: Vec<_> = tref
224            .trait_associated_types(self.hax_state_with_id())
225            .iter()
226            .map(|ty| self.translate_ty(span, ty))
227            .try_collect()?;
228        vtable_ref.generics.types.extend(assoc_tys);
229
230        Ok(Some(vtable_ref))
231    }
232
233    /// Add a `method_name: fn(...) -> ...` field for the method.
234    fn add_method_to_vtable_def(
235        &mut self,
236        span: Span,
237        trait_def: &hax::FullDef,
238        mut mk_field: impl FnMut(String, Ty),
239        item: &hax::AssocItem,
240    ) -> Result<(), Error> {
241        let item_def_id = &item.def_id;
242        let item_def = self.hax_def(
243            &trait_def
244                .this()
245                .with_def_id(&self.t_ctx.hax_state, item_def_id),
246        )?;
247        let hax::FullDefKind::AssocFn {
248            sig,
249            vtable_sig: Some(_),
250            ..
251        } = item_def.kind()
252        else {
253            return Ok(());
254        };
255
256        let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
257        // It's ok to translate the method signature in the context of the trait because
258        // `vtable_sig: Some(_)` ensures the method has no generics of its own.
259        let sig = self.translate_fun_sig(span, sig)?;
260        let ty = TyKind::FnPtr(sig).into_ty();
261
262        mk_field(format!("method_{}", item_name.0), ty);
263        Ok(())
264    }
265
266    /// Add `super_trait_n: &'static SuperTraitNVTable` fields.
267    fn add_supertraits_to_vtable_def(
268        &mut self,
269        span: Span,
270        mut mk_field: impl FnMut(String, Ty),
271        implied_predicates: &hax::GenericPredicates,
272    ) -> Result<(), Error> {
273        let mut counter = (0..).into_iter();
274        for (clause, _span) in &implied_predicates.predicates {
275            if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() {
276                // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
277                if !self.pred_is_for_self(&pred.trait_ref) {
278                    continue;
279                }
280                let vtbl_struct = self
281                    .translate_region_binder(span, &clause.kind, |ctx, _| {
282                        ctx.translate_vtable_struct_ref(span, &pred.trait_ref)
283                    })?
284                    .erase()
285                    .expect("parent trait should be dyn compatible");
286                let ty = Ty::new(TyKind::Ref(
287                    Region::Static,
288                    Ty::new(TyKind::Adt(vtbl_struct)),
289                    RefKind::Shared,
290                ));
291                mk_field(format!("super_trait_{}", counter.next().unwrap()), ty);
292            }
293        }
294        Ok(())
295    }
296
297    fn gen_vtable_struct_fields(
298        &mut self,
299        span: Span,
300        trait_def: &hax::FullDef,
301        implied_predicates: &hax::GenericPredicates,
302    ) -> Result<Vector<FieldId, Field>, Error> {
303        let mut fields = Vector::new();
304        let mut mk_field = |name, ty| {
305            fields.push(Field {
306                span,
307                attr_info: dummy_public_attr_info(),
308                name: Some(name),
309                ty,
310            });
311        };
312
313        // Add the basic fields.
314        // Field: `size: usize`
315        mk_field("size".into(), usize_ty());
316        // Field: `align: usize`
317        mk_field("align".into(), usize_ty());
318        // Field: `drop: fn(*mut Self)` -- `Self` is just a placeholder, will be dynified below.
319        mk_field("drop".into(), {
320            let self_ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
321            let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
322            Ty::new(TyKind::FnPtr(RegionBinder::empty((
323                [self_ptr].into(),
324                Ty::mk_unit(),
325            ))))
326        });
327
328        // Add the method pointers (trait aliases don't have methods).
329        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
330            for item in items {
331                self.add_method_to_vtable_def(span, trait_def, &mut mk_field, item)?;
332            }
333        }
334
335        // Add the supertrait vtables.
336        self.add_supertraits_to_vtable_def(span, &mut mk_field, implied_predicates)?;
337
338        Ok(fields)
339    }
340
341    /// This is a temporary check until we support `dyn Trait` with `--monomorphize`.
342    pub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), Error> {
343        if self.monomorphize() {
344            raise_error!(
345                self,
346                span,
347                "`dyn Trait` is not yet supported with `--monomorphize`; \
348                use `--monomorphize-conservative` instead"
349            )
350        }
351        Ok(())
352    }
353
354    /// Construct the type of the vtable for this trait.
355    ///
356    /// It's a struct that has for generics the generics of the trait + one parameter for each
357    /// associated type of the trait and its parents.
358    ///
359    /// struct TraitVTable<TraitArgs.., AssocTys..> {
360    ///   size: usize,
361    ///   align: usize,
362    ///   drop: fn(*mut dyn Trait<...>),
363    ///   method_name: fn(&dyn Trait<...>, Args..) -> Output,
364    ///   ... other methods
365    ///   super_trait_0: &'static SuperTrait0VTable
366    ///   ... other supertraits
367    /// }
368    pub(crate) fn translate_vtable_struct(
369        mut self,
370        type_id: TypeDeclId,
371        item_meta: ItemMeta,
372        trait_def: &hax::FullDef,
373    ) -> Result<TypeDecl, Error> {
374        let span = item_meta.span;
375        if !self.trait_is_dyn_compatible(trait_def.def_id())? {
376            raise_error!(
377                self,
378                span,
379                "Trying to compute the vtable type \
380                for a non-dyn-compatible trait"
381            );
382        }
383        self.check_no_monomorphize(span)?;
384
385        self.translate_def_generics(span, trait_def)?;
386
387        let (hax::FullDefKind::Trait {
388            dyn_self,
389            implied_predicates,
390            ..
391        }
392        | hax::FullDefKind::TraitAlias {
393            dyn_self,
394            implied_predicates,
395            ..
396        }) = trait_def.kind()
397        else {
398            panic!()
399        };
400        let Some(dyn_self) = dyn_self else {
401            panic!("Trying to generate a vtable for a non-dyn-compatible trait")
402        };
403
404        // The `dyn Trait<Args..>` type for this trait.
405        let mut dyn_self = {
406            let dyn_self = self.translate_ty(span, dyn_self)?;
407            let TyKind::DynTrait(mut dyn_pred) = dyn_self.kind().clone() else {
408                panic!("incorrect `dyn_self`")
409            };
410
411            // Add one generic parameter for each associated type of this trait and its parents. We
412            // then use that in `dyn_self`
413            for (i, ty_constraint) in dyn_pred
414                .binder
415                .params
416                .trait_type_constraints
417                .iter_mut()
418                .enumerate()
419            {
420                let name = format!("Ty{i}");
421                let new_ty = self
422                    .the_only_binder_mut()
423                    .params
424                    .types
425                    .push_with(|index| TypeParam { index, name });
426                // Moving that type under two levels of binders: the `DynPredicate` binder and the
427                // type constraint binder.
428                let new_ty =
429                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::new(2), new_ty)).into_ty();
430                ty_constraint.skip_binder.ty = new_ty;
431            }
432            TyKind::DynTrait(dyn_pred).into_ty()
433        };
434
435        let (mut kind, layout) = if item_meta.opacity.with_private_contents().is_opaque() {
436            (TypeDeclKind::Opaque, None)
437        } else {
438            // First construct fields that use the real method signatures (which may use the `Self`
439            // type). We fixup the types and generics below.
440            let fields = self.gen_vtable_struct_fields(span, trait_def, implied_predicates)?;
441            let kind = TypeDeclKind::Struct(fields);
442            let layout = self.generate_naive_layout(span, &kind)?;
443            (kind, Some(layout))
444        };
445
446        // Replace any use of `Self` with `dyn Trait<...>`, and remove the `Self` type variable
447        // from the generic parameters.
448        let mut generics = self.into_generics();
449        {
450            dyn_self = dynify(dyn_self, None, false);
451            generics = dynify(generics, Some(dyn_self.clone()), false);
452            kind = dynify(kind, Some(dyn_self.clone()), true);
453            generics.types.remove_and_shift_ids(TypeVarId::ZERO);
454            generics.types.iter_mut().for_each(|ty| {
455                ty.index -= 1;
456            });
457        }
458
459        let dyn_predicate = dyn_self
460            .kind()
461            .as_dyn_trait()
462            .expect("incorrect `dyn_self`");
463        Ok(TypeDecl {
464            def_id: type_id,
465            item_meta: item_meta,
466            generics: generics,
467            src: ItemSource::VTableTy {
468                dyn_predicate: dyn_predicate.clone(),
469            },
470            kind,
471            layout,
472            // A vtable struct is always sized
473            ptr_metadata: PtrMetadata::None,
474            repr: None,
475        })
476    }
477}
478
479//// Generate a vtable value.
480impl ItemTransCtx<'_, '_> {
481    pub fn translate_vtable_instance_ref(
482        &mut self,
483        span: Span,
484        trait_ref: &hax::TraitRef,
485        impl_ref: &hax::ItemRef,
486    ) -> Result<Option<GlobalDeclRef>, Error> {
487        self.translate_vtable_instance_ref_maybe_enqueue(true, span, trait_ref, impl_ref)
488    }
489
490    pub fn translate_vtable_instance_ref_no_enqueue(
491        &mut self,
492        span: Span,
493        trait_ref: &hax::TraitRef,
494        impl_ref: &hax::ItemRef,
495    ) -> Result<Option<GlobalDeclRef>, Error> {
496        self.translate_vtable_instance_ref_maybe_enqueue(false, span, trait_ref, impl_ref)
497    }
498
499    pub fn translate_vtable_instance_ref_maybe_enqueue(
500        &mut self,
501        enqueue: bool,
502        span: Span,
503        trait_ref: &hax::TraitRef,
504        impl_ref: &hax::ItemRef,
505    ) -> Result<Option<GlobalDeclRef>, Error> {
506        if !self.trait_is_dyn_compatible(&trait_ref.def_id)? {
507            return Ok(None);
508        }
509        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
510        // `dyn Trait` coercion.
511        // TODO(dyn): To do this properly we'd need to know for each clause whether it ultimately
512        // ends up used in a vtable cast.
513        let vtable_ref: GlobalDeclRef = self.translate_item_maybe_enqueue(
514            span,
515            enqueue,
516            impl_ref,
517            TransItemSourceKind::VTableInstance(TraitImplSource::Normal),
518        )?;
519        Ok(Some(vtable_ref))
520    }
521
522    /// Local helper function to get the vtable struct reference and trait declaration reference
523    fn get_vtable_instance_info<'a>(
524        &mut self,
525        span: Span,
526        impl_def: &'a hax::FullDef,
527        impl_kind: &TraitImplSource,
528    ) -> Result<(TraitImplRef, TypeDeclRef), Error> {
529        let implemented_trait = match impl_def.kind() {
530            hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref,
531            _ => unreachable!(),
532        };
533        let vtable_struct_ref = self
534            .translate_vtable_struct_ref(span, implemented_trait)?
535            .expect("trait should be dyn-compatible");
536        let impl_ref = self.translate_item(
537            span,
538            impl_def.this(),
539            TransItemSourceKind::TraitImpl(*impl_kind),
540        )?;
541        Ok((impl_ref, vtable_struct_ref))
542    }
543
544    /// E.g.,
545    /// ```
546    /// global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
547    ///     size: size_of(Foo),
548    ///     align: align_of(Foo),
549    ///     drop: <Foo as Drop>::drop,
550    ///     method_0: <Foo as Trait>::method_0::{shim},
551    ///     method_1: <Foo as Trait>::method_1::{shim},
552    ///     ...
553    ///     super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
554    ///     super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
555    ///     ...
556    /// }
557    /// ```
558    pub(crate) fn translate_vtable_instance(
559        mut self,
560        global_id: GlobalDeclId,
561        item_meta: ItemMeta,
562        impl_def: &hax::FullDef,
563        impl_kind: &TraitImplSource,
564    ) -> Result<GlobalDecl, Error> {
565        let span = item_meta.span;
566        self.translate_def_generics(span, impl_def)?;
567        self.check_no_monomorphize(span)?;
568
569        let (impl_ref, vtable_struct_ref) =
570            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
571        // Initializer function for this global.
572        let init = self.register_item(
573            span,
574            impl_def.this(),
575            TransItemSourceKind::VTableInstanceInitializer(*impl_kind),
576        );
577
578        Ok(GlobalDecl {
579            def_id: global_id,
580            item_meta,
581            generics: self.into_generics(),
582            src: ItemSource::VTableInstance { impl_ref },
583            // it should be static to have its own address
584            global_kind: GlobalKind::Static,
585            ty: Ty::new(TyKind::Adt(vtable_struct_ref)),
586            init,
587        })
588    }
589
590    fn add_method_to_vtable_value(
591        &mut self,
592        span: Span,
593        impl_def: &hax::FullDef,
594        item: &hax::ImplAssocItem,
595        mut mk_field: impl FnMut(ConstantExprKind),
596    ) -> Result<(), Error> {
597        // Exit if the item isn't a vtable safe method.
598        match self.poly_hax_def(&item.decl_def_id)?.kind() {
599            hax::FullDefKind::AssocFn {
600                vtable_sig: Some(_),
601                ..
602            } => {}
603            _ => return Ok(()),
604        }
605
606        let const_kind = match &item.value {
607            hax::ImplAssocItemValue::Provided {
608                def_id: item_def_id,
609                ..
610            } => {
611                // The method is vtable safe so it has no generics, hence we can reuse the impl
612                // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`.
613                let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id);
614                let shim_ref = self
615                    .translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)?
616                    .erase();
617                ConstantExprKind::FnPtr(shim_ref)
618            }
619            hax::ImplAssocItemValue::DefaultedFn { .. } => ConstantExprKind::Opaque(
620                "shim for default methods \
621                    aren't yet supported"
622                    .to_string(),
623            ),
624            _ => return Ok(()),
625        };
626
627        mk_field(const_kind);
628
629        Ok(())
630    }
631
632    fn add_supertraits_to_vtable_value(
633        &mut self,
634        span: Span,
635        trait_def: &hax::FullDef,
636        impl_def: &hax::FullDef,
637        mut mk_field: impl FnMut(ConstantExprKind),
638    ) -> Result<(), Error> {
639        let hax::FullDefKind::TraitImpl {
640            implied_impl_exprs, ..
641        } = impl_def.kind()
642        else {
643            unreachable!()
644        };
645        let hax::FullDefKind::Trait {
646            implied_predicates, ..
647        } = trait_def.kind()
648        else {
649            unreachable!()
650        };
651        for ((clause, _), impl_expr) in implied_predicates.predicates.iter().zip(implied_impl_exprs)
652        {
653            let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
654                continue;
655            };
656            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
657            if !self.pred_is_for_self(&pred.trait_ref) {
658                continue;
659            }
660
661            let vtable_def_ref = self
662                .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
663                    ctx.translate_vtable_struct_ref(span, tref)
664                })?
665                .erase()
666                .expect("parent trait should be dyn compatible");
667            let fn_ptr_ty = TyKind::Adt(vtable_def_ref).into_ty();
668            let kind = match &impl_expr.r#impl {
669                hax::ImplExprAtom::Concrete(impl_item) => {
670                    let vtable_instance_ref = self
671                        .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
672                            ctx.translate_vtable_instance_ref(span, tref, impl_item)
673                        })?
674                        .erase()
675                        .expect("parent trait should be dyn compatible");
676                    let global = Box::new(ConstantExpr {
677                        kind: ConstantExprKind::Global(vtable_instance_ref),
678                        ty: fn_ptr_ty,
679                    });
680                    ConstantExprKind::Ref(global)
681                }
682                // TODO(dyn): builtin impls
683                _ => ConstantExprKind::Opaque("missing supertrait vtable".into()),
684            };
685            mk_field(kind);
686        }
687        Ok(())
688    }
689
690    /// Generate the body of the vtable instance function.
691    /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls.
692    /// ```ignore
693    /// let ret@0 : VTable;
694    /// ret@0 = VTable { ... };
695    /// return;
696    /// ```
697    fn gen_vtable_instance_init_body(
698        &mut self,
699        span: Span,
700        impl_def: &hax::FullDef,
701        vtable_struct_ref: TypeDeclRef,
702    ) -> Result<Body, Error> {
703        let hax::FullDefKind::TraitImpl {
704            trait_pred, items, ..
705        } = impl_def.kind()
706        else {
707            unreachable!()
708        };
709        let trait_def = self.hax_def(&trait_pred.trait_ref)?;
710        let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?;
711        // The type this impl is for.
712        let self_ty = &implemented_trait.generics.types[0];
713
714        let mut builder = BodyBuilder::new(span, 0);
715        let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone()));
716        let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone());
717
718        // Retreive the expected field types from the struct definition. This avoids complicated
719        // substitutions.
720        let field_tys = {
721            let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone();
722            let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())?
723            else {
724                unreachable!()
725            };
726            let TypeDeclKind::Struct(fields) = &vtable_def.kind else {
727                unreachable!()
728            };
729            fields
730                .iter()
731                .map(|f| &f.ty)
732                .cloned()
733                .map(|ty| ty.substitute(&vtable_struct_ref.generics))
734                .collect_vec()
735        };
736
737        let mut aggregate_fields = vec![];
738        // For each vtable field, assign the desired value to a new local.
739        let mut field_ty_iter = field_tys.into_iter();
740
741        let size_ty = field_ty_iter.next().unwrap();
742        let size_local = builder.new_var(Some("size".to_string()), size_ty);
743        builder.push_statement(StatementKind::Assign(
744            size_local.clone(),
745            Rvalue::NullaryOp(NullOp::SizeOf, self_ty.clone()),
746        ));
747        aggregate_fields.push(Operand::Move(size_local));
748
749        let align_ty = field_ty_iter.next().unwrap();
750        let align_local = builder.new_var(Some("align".to_string()), align_ty);
751        builder.push_statement(StatementKind::Assign(
752            align_local.clone(),
753            Rvalue::NullaryOp(NullOp::AlignOf, self_ty.clone()),
754        ));
755        aggregate_fields.push(Operand::Move(align_local));
756
757        // Helper to fill in the remaining fields with constant values.
758        let mut mk_field = |kind| {
759            let ty = field_ty_iter.next().unwrap();
760            aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty })));
761        };
762
763        // Build a reference to `std::ptr::drop_in_place<T>`.
764        // let drop_in_place: hax::ItemRef = {
765        //     // TODO: use the method instead
766        //     let s = self.hax_state_with_id();
767        //     let drop_in_place = self.tcx.lang_items().drop_in_place_fn().unwrap();
768        //     let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
769        //     let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
770        //     hax::ItemRef::translate(s, drop_in_place, generics)
771        // };
772        // let fn_ptr = self
773        //     .translate_fn_ptr(span, &drop_in_place, TransItemSourceKind::Fun)?
774        //     .erase();
775        let fn_ptr = {
776            // Build a reference to `impl Drop for T`.
777            let drop_trait = self.tcx.lang_items().drop_trait().unwrap();
778            let drop_impl_expr: hax::ImplExpr = {
779                let s = self.hax_state_with_id();
780                let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
781                let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
782                let drop_tref =
783                    rustc_middle::ty::TraitRef::new_from_args(self.tcx, drop_trait, generics);
784                hax::solve_trait(s, rustc_middle::ty::Binder::dummy(drop_tref))
785            };
786            let drop_tref = self.translate_trait_impl_expr(span, &drop_impl_expr)?;
787            let method_id = self.register_item(
788                span,
789                drop_impl_expr.r#trait.hax_skip_binder_ref(),
790                TransItemSourceKind::DropInPlaceMethod(None),
791            );
792            let item_name = TraitItemName("drop_in_place".into());
793            FnPtr::new(
794                FnPtrKind::Trait(drop_tref, item_name, method_id),
795                GenericArgs::empty(),
796            )
797        };
798        mk_field(ConstantExprKind::FnPtr(fn_ptr));
799
800        for item in items {
801            self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?;
802        }
803
804        self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?;
805
806        if field_ty_iter.next().is_some() {
807            raise_error!(
808                self,
809                span,
810                "Missed some fields in vtable value construction"
811            )
812        }
813
814        // Construct the final struct.
815        builder.push_statement(StatementKind::Assign(
816            ret_place,
817            Rvalue::Aggregate(
818                AggregateKind::Adt(vtable_struct_ref.clone(), None, None),
819                aggregate_fields,
820            ),
821        ));
822
823        Ok(Body::Unstructured(builder.build()))
824    }
825
826    pub(crate) fn translate_vtable_instance_init(
827        mut self,
828        init_func_id: FunDeclId,
829        item_meta: ItemMeta,
830        impl_def: &hax::FullDef,
831        impl_kind: &TraitImplSource,
832    ) -> Result<FunDecl, Error> {
833        let span = item_meta.span;
834        self.translate_def_generics(span, impl_def)?;
835        self.check_no_monomorphize(span)?;
836
837        let (impl_ref, vtable_struct_ref) =
838            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
839        let init_for = self.register_item(
840            span,
841            impl_def.this(),
842            TransItemSourceKind::VTableInstance(*impl_kind),
843        );
844
845        // Signature: `() -> VTable`.
846        let sig = FunSig {
847            is_unsafe: false,
848            generics: self.the_only_binder().params.clone(),
849            inputs: vec![],
850            output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())),
851        };
852
853        let body = match impl_kind {
854            _ if item_meta.opacity.with_private_contents().is_opaque() => Err(Opaque),
855            TraitImplSource::Normal => {
856                let body = self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?;
857                Ok(body)
858            }
859            _ => {
860                raise_error!(
861                    self,
862                    span,
863                    "Don't know how to generate a vtable for a virtual impl {impl_kind:?}"
864                );
865            }
866        };
867
868        Ok(FunDecl {
869            def_id: init_func_id,
870            item_meta: item_meta,
871            signature: sig,
872            src: ItemSource::VTableInstance { impl_ref },
873            is_global_initializer: Some(init_for),
874            body,
875        })
876    }
877
878    /// The target vtable shim body looks like:
879    /// ```ignore
880    /// local ret@0 : ReturnTy;
881    /// // the shim receiver of this shim function
882    /// local shim_self@1 : ShimReceiverTy;
883    /// // the arguments of the impl function
884    /// local arg1@2 : Arg1Ty;
885    /// ...
886    /// local argN@N : ArgNTy;
887    /// // the target receiver of the impl function
888    /// local target_self@(N+1) : TargetReceiverTy;
889    /// // perform some conversion to cast / re-box the shim receiver to the target receiver
890    /// ...
891    /// target_self@(N+1) := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
892    /// // call the impl function and assign the result to ret@0
893    /// ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N);
894    /// ```
895    fn translate_vtable_shim_body(
896        &mut self,
897        span: Span,
898        target_receiver: &Ty,
899        shim_signature: &FunSig,
900        impl_func_def: &hax::FullDef,
901    ) -> Result<Body, Error> {
902        let mut builder = BodyBuilder::new(span, shim_signature.inputs.len());
903
904        let ret_place = builder.new_var(None, shim_signature.output.clone());
905        let mut method_args = shim_signature
906            .inputs
907            .iter()
908            .map(|ty| builder.new_var(None, ty.clone()))
909            .collect_vec();
910        let target_self = builder.new_var(None, target_receiver.clone());
911
912        // Replace the `dyn Trait` receiver with the concrete one.
913        let shim_self = mem::replace(&mut method_args[0], target_self.clone());
914
915        // Perform the core concretization cast.
916        // FIXME: need to unpack & re-pack the structure for cases like `Rc`, `Arc`, `Pin` and
917        // (when --raw-boxes is on) `Box`
918        let rval = Rvalue::UnaryOp(
919            UnOp::Cast(CastKind::Concretize(
920                shim_self.ty().clone(),
921                target_self.ty().clone(),
922            )),
923            Operand::Move(shim_self.clone()),
924        );
925        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
926
927        let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun);
928        let generics = self.outermost_binder().params.identity_args();
929        builder.call(Call {
930            func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)),
931            args: method_args
932                .into_iter()
933                .map(|arg| Operand::Move(arg))
934                .collect(),
935            dest: ret_place,
936        });
937
938        Ok(Body::Unstructured(builder.build()))
939    }
940
941    pub(crate) fn translate_vtable_shim(
942        mut self,
943        fun_id: FunDeclId,
944        item_meta: ItemMeta,
945        impl_func_def: &hax::FullDef,
946    ) -> Result<FunDecl, Error> {
947        let span = item_meta.span;
948        self.check_no_monomorphize(span)?;
949
950        let hax::FullDefKind::AssocFn {
951            vtable_sig: Some(vtable_sig),
952            sig: target_signature,
953            ..
954        } = impl_func_def.kind()
955        else {
956            raise_error!(
957                self,
958                span,
959                "Trying to generate a vtable shim for a non-vtable-safe method"
960            );
961        };
962
963        // Replace to get the true signature of the shim function.
964        // As `translate_function_signature` will use the `sig` field of the `hax::FullDef`
965        // TODO: this is a hack.
966        let shim_func_def = {
967            let mut def = impl_func_def.clone();
968            let hax::FullDefKind::AssocFn { sig, .. } = &mut def.kind else {
969                unreachable!()
970            };
971            *sig = vtable_sig.clone();
972            def
973        };
974
975        // Compute the correct signature for the shim
976        let signature = self.translate_function_signature(&shim_func_def, &item_meta)?;
977
978        let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?;
979
980        trace!(
981            "[VtableShim] Obtained dyn signature with receiver type: {}",
982            signature.inputs[0].with_ctx(&self.into_fmt())
983        );
984
985        let body = if item_meta.opacity.with_private_contents().is_opaque() {
986            Err(Opaque)
987        } else {
988            Ok(self.translate_vtable_shim_body(
989                span,
990                &target_receiver,
991                &signature,
992                impl_func_def,
993            )?)
994        };
995
996        Ok(FunDecl {
997            def_id: fun_id,
998            item_meta,
999            signature,
1000            src: ItemSource::VTableMethodShim,
1001            is_global_initializer: None,
1002            body,
1003        })
1004    }
1005}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
