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        // First construct fields that use the real method signatures (which may use the `Self`
436        // type). We fixup the types and generics below.
437        let fields = self.gen_vtable_struct_fields(span, trait_def, implied_predicates)?;
438        let mut kind = TypeDeclKind::Struct(fields);
439        let layout = self.generate_naive_layout(span, &kind)?;
440
441        // Replace any use of `Self` with `dyn Trait<...>`, and remove the `Self` type variable
442        // from the generic parameters.
443        let mut generics = self.into_generics();
444        {
445            dyn_self = dynify(dyn_self, None, false);
446            generics = dynify(generics, Some(dyn_self.clone()), false);
447            kind = dynify(kind, Some(dyn_self.clone()), true);
448            generics.types.remove_and_shift_ids(TypeVarId::ZERO);
449            generics.types.iter_mut().for_each(|ty| {
450                ty.index -= 1;
451            });
452        }
453
454        let dyn_predicate = dyn_self
455            .kind()
456            .as_dyn_trait()
457            .expect("incorrect `dyn_self`");
458        Ok(TypeDecl {
459            def_id: type_id,
460            item_meta: item_meta,
461            generics: generics,
462            src: ItemSource::VTableTy {
463                dyn_predicate: dyn_predicate.clone(),
464            },
465            kind,
466            layout: Some(layout),
467            // A vtable struct is always sized
468            ptr_metadata: PtrMetadata::None,
469            repr: None,
470        })
471    }
472}
473
474//// Generate a vtable value.
475impl ItemTransCtx<'_, '_> {
476    pub fn translate_vtable_instance_ref(
477        &mut self,
478        span: Span,
479        trait_ref: &hax::TraitRef,
480        impl_ref: &hax::ItemRef,
481    ) -> Result<Option<GlobalDeclRef>, Error> {
482        self.translate_vtable_instance_ref_maybe_enqueue(true, span, trait_ref, impl_ref)
483    }
484
485    pub fn translate_vtable_instance_ref_no_enqueue(
486        &mut self,
487        span: Span,
488        trait_ref: &hax::TraitRef,
489        impl_ref: &hax::ItemRef,
490    ) -> Result<Option<GlobalDeclRef>, Error> {
491        self.translate_vtable_instance_ref_maybe_enqueue(false, span, trait_ref, impl_ref)
492    }
493
494    pub fn translate_vtable_instance_ref_maybe_enqueue(
495        &mut self,
496        enqueue: bool,
497        span: Span,
498        trait_ref: &hax::TraitRef,
499        impl_ref: &hax::ItemRef,
500    ) -> Result<Option<GlobalDeclRef>, Error> {
501        if !self.trait_is_dyn_compatible(&trait_ref.def_id)? {
502            return Ok(None);
503        }
504        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
505        // `dyn Trait` coercion.
506        // TODO(dyn): To do this properly we'd need to know for each clause whether it ultimately
507        // ends up used in a vtable cast.
508        let vtable_ref: GlobalDeclRef = self.translate_item_maybe_enqueue(
509            span,
510            enqueue,
511            impl_ref,
512            TransItemSourceKind::VTableInstance(TraitImplSource::Normal),
513        )?;
514        Ok(Some(vtable_ref))
515    }
516
517    /// Local helper function to get the vtable struct reference and trait declaration reference
518    fn get_vtable_instance_info<'a>(
519        &mut self,
520        span: Span,
521        impl_def: &'a hax::FullDef,
522        impl_kind: &TraitImplSource,
523    ) -> Result<(TraitImplRef, TypeDeclRef), Error> {
524        let implemented_trait = match impl_def.kind() {
525            hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref,
526            _ => unreachable!(),
527        };
528        let vtable_struct_ref = self
529            .translate_vtable_struct_ref(span, implemented_trait)?
530            .expect("trait should be dyn-compatible");
531        let impl_ref = self.translate_item(
532            span,
533            impl_def.this(),
534            TransItemSourceKind::TraitImpl(*impl_kind),
535        )?;
536        Ok((impl_ref, vtable_struct_ref))
537    }
538
539    /// E.g.,
540    /// ```
541    /// global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
542    ///     size: size_of(Foo),
543    ///     align: align_of(Foo),
544    ///     drop: <Foo as Drop>::drop,
545    ///     method_0: <Foo as Trait>::method_0::{shim},
546    ///     method_1: <Foo as Trait>::method_1::{shim},
547    ///     ...
548    ///     super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
549    ///     super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
550    ///     ...
551    /// }
552    /// ```
553    pub(crate) fn translate_vtable_instance(
554        mut self,
555        global_id: GlobalDeclId,
556        item_meta: ItemMeta,
557        impl_def: &hax::FullDef,
558        impl_kind: &TraitImplSource,
559    ) -> Result<GlobalDecl, Error> {
560        let span = item_meta.span;
561        self.translate_def_generics(span, impl_def)?;
562        self.check_no_monomorphize(span)?;
563
564        let (impl_ref, vtable_struct_ref) =
565            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
566        // Initializer function for this global.
567        let init = self.register_item(
568            span,
569            impl_def.this(),
570            TransItemSourceKind::VTableInstanceInitializer(*impl_kind),
571        );
572
573        Ok(GlobalDecl {
574            def_id: global_id,
575            item_meta,
576            generics: self.into_generics(),
577            src: ItemSource::VTableInstance { impl_ref },
578            // it should be static to have its own address
579            global_kind: GlobalKind::Static,
580            ty: Ty::new(TyKind::Adt(vtable_struct_ref)),
581            init,
582        })
583    }
584
585    fn add_method_to_vtable_value(
586        &mut self,
587        span: Span,
588        impl_def: &hax::FullDef,
589        item: &hax::ImplAssocItem,
590        mut mk_field: impl FnMut(ConstantExprKind),
591    ) -> Result<(), Error> {
592        // Exit if the item isn't a vtable safe method.
593        match self.poly_hax_def(&item.decl_def_id)?.kind() {
594            hax::FullDefKind::AssocFn {
595                vtable_sig: Some(_),
596                ..
597            } => {}
598            _ => return Ok(()),
599        }
600
601        let const_kind = match &item.value {
602            hax::ImplAssocItemValue::Provided {
603                def_id: item_def_id,
604                ..
605            } => {
606                // The method is vtable safe so it has no generics, hence we can reuse the impl
607                // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`.
608                let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id);
609                let shim_ref = self
610                    .translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)?
611                    .erase();
612                ConstantExprKind::FnPtr(shim_ref)
613            }
614            hax::ImplAssocItemValue::DefaultedFn { .. } => ConstantExprKind::Opaque(
615                "shim for default methods \
616                    aren't yet supported"
617                    .to_string(),
618            ),
619            _ => return Ok(()),
620        };
621
622        mk_field(const_kind);
623
624        Ok(())
625    }
626
627    fn add_supertraits_to_vtable_value(
628        &mut self,
629        span: Span,
630        trait_def: &hax::FullDef,
631        impl_def: &hax::FullDef,
632        mut mk_field: impl FnMut(ConstantExprKind),
633    ) -> Result<(), Error> {
634        let hax::FullDefKind::TraitImpl {
635            implied_impl_exprs, ..
636        } = impl_def.kind()
637        else {
638            unreachable!()
639        };
640        let hax::FullDefKind::Trait {
641            implied_predicates, ..
642        } = trait_def.kind()
643        else {
644            unreachable!()
645        };
646        for ((clause, _), impl_expr) in implied_predicates.predicates.iter().zip(implied_impl_exprs)
647        {
648            let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
649                continue;
650            };
651            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
652            if !self.pred_is_for_self(&pred.trait_ref) {
653                continue;
654            }
655
656            let vtable_def_ref = self
657                .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
658                    ctx.translate_vtable_struct_ref(span, tref)
659                })?
660                .erase()
661                .expect("parent trait should be dyn compatible");
662            let fn_ptr_ty = TyKind::Adt(vtable_def_ref).into_ty();
663            let kind = match &impl_expr.r#impl {
664                hax::ImplExprAtom::Concrete(impl_item) => {
665                    let vtable_instance_ref = self
666                        .translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
667                            ctx.translate_vtable_instance_ref(span, tref, impl_item)
668                        })?
669                        .erase()
670                        .expect("parent trait should be dyn compatible");
671                    let global = Box::new(ConstantExpr {
672                        kind: ConstantExprKind::Global(vtable_instance_ref),
673                        ty: fn_ptr_ty,
674                    });
675                    ConstantExprKind::Ref(global)
676                }
677                // TODO(dyn): builtin impls
678                _ => ConstantExprKind::Opaque("missing supertrait vtable".into()),
679            };
680            mk_field(kind);
681        }
682        Ok(())
683    }
684
685    /// Generate the body of the vtable instance function.
686    /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls.
687    /// ```ignore
688    /// let ret@0 : VTable;
689    /// ret@0 = VTable { ... };
690    /// return;
691    /// ```
692    fn gen_vtable_instance_init_body(
693        &mut self,
694        span: Span,
695        impl_def: &hax::FullDef,
696        vtable_struct_ref: TypeDeclRef,
697    ) -> Result<Body, Error> {
698        let hax::FullDefKind::TraitImpl {
699            trait_pred, items, ..
700        } = impl_def.kind()
701        else {
702            unreachable!()
703        };
704        let trait_def = self.hax_def(&trait_pred.trait_ref)?;
705        let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?;
706        // The type this impl is for.
707        let self_ty = &implemented_trait.generics.types[0];
708
709        let mut builder = BodyBuilder::new(span, 0);
710        let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone()));
711        let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone());
712
713        // Retreive the expected field types from the struct definition. This avoids complicated
714        // substitutions.
715        let field_tys = {
716            let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone();
717            let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())?
718            else {
719                unreachable!()
720            };
721            let TypeDeclKind::Struct(fields) = &vtable_def.kind else {
722                unreachable!()
723            };
724            fields
725                .iter()
726                .map(|f| &f.ty)
727                .cloned()
728                .map(|ty| ty.substitute(&vtable_struct_ref.generics))
729                .collect_vec()
730        };
731
732        let mut aggregate_fields = vec![];
733        // For each vtable field, assign the desired value to a new local.
734        let mut field_ty_iter = field_tys.into_iter();
735
736        let size_ty = field_ty_iter.next().unwrap();
737        let size_local = builder.new_var(Some("size".to_string()), size_ty);
738        builder.push_statement(StatementKind::Assign(
739            size_local.clone(),
740            Rvalue::NullaryOp(NullOp::SizeOf, self_ty.clone()),
741        ));
742        aggregate_fields.push(Operand::Move(size_local));
743
744        let align_ty = field_ty_iter.next().unwrap();
745        let align_local = builder.new_var(Some("align".to_string()), align_ty);
746        builder.push_statement(StatementKind::Assign(
747            align_local.clone(),
748            Rvalue::NullaryOp(NullOp::AlignOf, self_ty.clone()),
749        ));
750        aggregate_fields.push(Operand::Move(align_local));
751
752        // Helper to fill in the remaining fields with constant values.
753        let mut mk_field = |kind| {
754            let ty = field_ty_iter.next().unwrap();
755            aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty })));
756        };
757
758        // Build a reference to `std::ptr::drop_in_place<T>`.
759        // let drop_in_place: hax::ItemRef = {
760        //     // TODO: use the method instead
761        //     let s = self.hax_state_with_id();
762        //     let drop_in_place = self.tcx.lang_items().drop_in_place_fn().unwrap();
763        //     let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
764        //     let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
765        //     hax::ItemRef::translate(s, drop_in_place, generics)
766        // };
767        // let fn_ptr = self
768        //     .translate_fn_ptr(span, &drop_in_place, TransItemSourceKind::Fun)?
769        //     .erase();
770        let fn_ptr = {
771            // Build a reference to `impl Drop for T`.
772            let drop_trait = self.tcx.lang_items().drop_trait().unwrap();
773            let drop_impl_expr: hax::ImplExpr = {
774                let s = self.hax_state_with_id();
775                let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
776                let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
777                let drop_tref =
778                    rustc_middle::ty::TraitRef::new_from_args(self.tcx, drop_trait, generics);
779                hax::solve_trait(s, rustc_middle::ty::Binder::dummy(drop_tref))
780            };
781            let drop_tref = self.translate_trait_impl_expr(span, &drop_impl_expr)?;
782            let method_id = self.register_item(
783                span,
784                drop_impl_expr.r#trait.hax_skip_binder_ref(),
785                TransItemSourceKind::DropInPlaceMethod(None),
786            );
787            let item_name = TraitItemName("drop_in_place".to_string());
788            FnPtr::new(
789                FnPtrKind::Trait(drop_tref, item_name, method_id),
790                GenericArgs::empty(),
791            )
792        };
793        mk_field(ConstantExprKind::FnPtr(fn_ptr));
794
795        for item in items {
796            self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?;
797        }
798
799        self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?;
800
801        if field_ty_iter.next().is_some() {
802            raise_error!(
803                self,
804                span,
805                "Missed some fields in vtable value construction"
806            )
807        }
808
809        // Construct the final struct.
810        builder.push_statement(StatementKind::Assign(
811            ret_place,
812            Rvalue::Aggregate(
813                AggregateKind::Adt(vtable_struct_ref.clone(), None, None),
814                aggregate_fields,
815            ),
816        ));
817
818        Ok(Body::Unstructured(builder.build()))
819    }
820
821    pub(crate) fn translate_vtable_instance_init(
822        mut self,
823        init_func_id: FunDeclId,
824        item_meta: ItemMeta,
825        impl_def: &hax::FullDef,
826        impl_kind: &TraitImplSource,
827    ) -> Result<FunDecl, Error> {
828        let span = item_meta.span;
829        self.translate_def_generics(span, impl_def)?;
830        self.check_no_monomorphize(span)?;
831
832        let (impl_ref, vtable_struct_ref) =
833            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
834        let init_for = self.register_item(
835            span,
836            impl_def.this(),
837            TransItemSourceKind::VTableInstance(*impl_kind),
838        );
839
840        // Signature: `() -> VTable`.
841        let sig = FunSig {
842            is_unsafe: false,
843            generics: self.the_only_binder().params.clone(),
844            inputs: vec![],
845            output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())),
846        };
847
848        let body = match impl_kind {
849            TraitImplSource::Normal => {
850                let body = self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?;
851                Ok(body)
852            }
853            _ => {
854                raise_error!(
855                    self,
856                    span,
857                    "Don't know how to generate a vtable for a virtual impl {impl_kind:?}"
858                );
859            }
860        };
861
862        Ok(FunDecl {
863            def_id: init_func_id,
864            item_meta: item_meta,
865            signature: sig,
866            src: ItemSource::VTableInstance { impl_ref },
867            is_global_initializer: Some(init_for),
868            body,
869        })
870    }
871
872    /// The target vtable shim body looks like:
873    /// ```ignore
874    /// local ret@0 : ReturnTy;
875    /// // the shim receiver of this shim function
876    /// local shim_self@1 : ShimReceiverTy;
877    /// // the arguments of the impl function
878    /// local arg1@2 : Arg1Ty;
879    /// ...
880    /// local argN@N : ArgNTy;
881    /// // the target receiver of the impl function
882    /// local target_self@(N+1) : TargetReceiverTy;
883    /// // perform some conversion to cast / re-box the shim receiver to the target receiver
884    /// ...
885    /// target_self@(N+1) := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
886    /// // call the impl function and assign the result to ret@0
887    /// ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N);
888    /// ```
889    fn translate_vtable_shim_body(
890        &mut self,
891        span: Span,
892        target_receiver: &Ty,
893        shim_signature: &FunSig,
894        impl_func_def: &hax::FullDef,
895    ) -> Result<Body, Error> {
896        let mut builder = BodyBuilder::new(span, shim_signature.inputs.len());
897
898        let ret_place = builder.new_var(None, shim_signature.output.clone());
899        let mut method_args = shim_signature
900            .inputs
901            .iter()
902            .map(|ty| builder.new_var(None, ty.clone()))
903            .collect_vec();
904        let target_self = builder.new_var(None, target_receiver.clone());
905
906        // Replace the `dyn Trait` receiver with the concrete one.
907        let shim_self = mem::replace(&mut method_args[0], target_self.clone());
908
909        // Perform the core concretization cast.
910        // FIXME: need to unpack & re-pack the structure for cases like `Rc`, `Arc`, `Pin` and
911        // (when --raw-boxes is on) `Box`
912        let rval = Rvalue::UnaryOp(
913            UnOp::Cast(CastKind::Concretize(
914                shim_self.ty().clone(),
915                target_self.ty().clone(),
916            )),
917            Operand::Move(shim_self.clone()),
918        );
919        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
920
921        let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun);
922        let generics = self.outermost_binder().params.identity_args();
923        builder.call(Call {
924            func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)),
925            args: method_args
926                .into_iter()
927                .map(|arg| Operand::Move(arg))
928                .collect(),
929            dest: ret_place,
930        });
931
932        Ok(Body::Unstructured(builder.build()))
933    }
934
935    pub(crate) fn translate_vtable_shim(
936        mut self,
937        fun_id: FunDeclId,
938        item_meta: ItemMeta,
939        impl_func_def: &hax::FullDef,
940    ) -> Result<FunDecl, Error> {
941        let span = item_meta.span;
942        self.check_no_monomorphize(span)?;
943
944        let hax::FullDefKind::AssocFn {
945            vtable_sig: Some(vtable_sig),
946            sig: target_signature,
947            ..
948        } = impl_func_def.kind()
949        else {
950            raise_error!(
951                self,
952                span,
953                "Trying to generate a vtable shim for a non-vtable-safe method"
954            );
955        };
956
957        // Replace to get the true signature of the shim function.
958        // As `translate_function_signature` will use the `sig` field of the `hax::FullDef`
959        // TODO: this is a hack.
960        let shim_func_def = {
961            let mut def = impl_func_def.clone();
962            let hax::FullDefKind::AssocFn { sig, .. } = &mut def.kind else {
963                unreachable!()
964            };
965            *sig = vtable_sig.clone();
966            def
967        };
968
969        // Compute the correct signature for the shim
970        let signature = self.translate_function_signature(&shim_func_def, &item_meta)?;
971
972        let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?;
973
974        trace!(
975            "[VtableShim] Obtained dyn signature with receiver type: {}",
976            signature.inputs[0].with_ctx(&self.into_fmt())
977        );
978
979        let body =
980            self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?;
981
982        Ok(FunDecl {
983            def_id: fun_id,
984            item_meta,
985            signature,
986            src: ItemSource::VTableMethodShim,
987            is_global_initializer: None,
988            body: Ok(body),
989        })
990    }
991}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
