charon_driver/translate/
translate_trait_objects.rs

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

charon_driver/translate/
translate_trait_objects.rs
