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<Option<TypeDeclRef>, Error> {
192        self.translate_vtable_struct_ref_maybe_enqueue(true, span, tref)
193    }
194
195    pub fn translate_vtable_struct_ref_no_enqueue(
196        &mut self,
197        span: Span,
198        tref: &hax::TraitRef,
199    ) -> Result<Option<TypeDeclRef>, Error> {
200        self.translate_vtable_struct_ref_maybe_enqueue(false, span, tref)
201    }
202
203    /// Given a trait ref, return a reference to its vtable struct, if it is dyn compatible.
204    pub fn translate_vtable_struct_ref_maybe_enqueue(
205        &mut self,
206        enqueue: bool,
207        span: Span,
208        tref: &hax::TraitRef,
209    ) -> Result<Option<TypeDeclRef>, Error> {
210        if !self.trait_is_dyn_compatible(&tref.def_id)? {
211            return Ok(None);
212        }
213        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
214        // `dyn Trait`.
215        let mut vtable_ref: TypeDeclRef =
216            self.translate_item_maybe_enqueue(span, enqueue, tref, TransItemSourceKind::VTable)?;
217        // Remove the `Self` type variable from the generic parameters.
218        vtable_ref
219            .generics
220            .types
221            .remove_and_shift_ids(TypeVarId::ZERO);
222
223        // The vtable type also takes associated types as parameters.
224        let assoc_tys: Vec<_> = tref
225            .trait_associated_types(self.hax_state_with_id())
226            .iter()
227            .map(|ty| self.translate_ty(span, ty))
228            .try_collect()?;
229        vtable_ref.generics.types.extend(assoc_tys);
230
231        Ok(Some(vtable_ref))
232    }
233
234    fn prepare_vtable_fields(
235        &mut self,
236        trait_def: &hax::FullDef,
237        implied_predicates: &hax::GenericPredicates,
238    ) -> Result<VTableData, Error> {
239        let mut supertrait_map: IndexMap<TraitClauseId, _> =
240            (0..implied_predicates.predicates.len())
241                .map(|_| None)
242                .collect();
243        let mut fields = IndexVec::new();
244
245        // Basic fields.
246        fields.push(TrVTableField::Size);
247        fields.push(TrVTableField::Align);
248        fields.push(TrVTableField::Drop);
249
250        // Method fields.
251        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
252            for item in items {
253                let item_def_id = &item.def_id;
254                // This is ok because dyn-compatible methods don't have generics.
255                let item_def =
256                    self.hax_def(&trait_def.this().with_def_id(self.hax_state(), item_def_id))?;
257                if let hax::FullDefKind::AssocFn {
258                    sig,
259                    vtable_sig: Some(_),
260                    ..
261                } = item_def.kind()
262                {
263                    let name = self.translate_trait_item_name(&item_def_id)?;
264                    fields.push(TrVTableField::Method(name, sig.clone()));
265                }
266            }
267        }
268
269        // Supertrait fields.
270        for (i, (clause, _span)) in implied_predicates.predicates.iter().enumerate() {
271            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
272            if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref()
273                && self.pred_is_for_self(&pred.trait_ref)
274            {
275                let trait_clause_id = TraitClauseId::from_raw(i);
276                supertrait_map[trait_clause_id] = Some(fields.next_idx());
277                fields.push(TrVTableField::SuperTrait(trait_clause_id, clause.clone()));
278            }
279        }
280
281        Ok(VTableData {
282            fields,
283            supertrait_map,
284        })
285    }
286
287    fn gen_vtable_struct_fields(
288        &mut self,
289        span: Span,
290        vtable_data: &VTableData,
291    ) -> Result<IndexVec<FieldId, Field>, Error> {
292        let mut fields = IndexVec::new();
293        let mut supertrait_counter = (0..).into_iter();
294        for field in &vtable_data.fields {
295            let (name, ty) = match field {
296                TrVTableField::Size => ("size".into(), usize_ty()),
297                TrVTableField::Align => ("align".into(), usize_ty()),
298                TrVTableField::Drop => {
299                    let self_ty =
300                        TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
301                    let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
302                    let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(FunSig {
303                        is_unsafe: true,
304                        inputs: [self_ptr].into(),
305                        output: Ty::mk_unit(),
306                    })));
307                    ("drop".into(), drop_ty)
308                }
309                TrVTableField::Method(item_name, sig) => {
310                    // It's ok to translate the method signature in the context of the trait because
311                    // `vtable_sig: Some(_)` ensures the method has no generics of its own.
312                    let sig = self.translate_poly_fun_sig(span, &sig)?;
313                    let ty = TyKind::FnPtr(sig).into_ty();
314                    let field_name = format!("method_{}", item_name.0);
315                    (field_name, ty)
316                }
317                TrVTableField::SuperTrait(_, clause) => {
318                    let vtbl_struct =
319                        self.translate_region_binder(span, &clause.kind, |ctx, kind| {
320                            let hax::ClauseKind::Trait(pred) = kind else {
321                                unreachable!()
322                            };
323                            let tyref = ctx
324                                .translate_vtable_struct_ref(span, &pred.trait_ref)?
325                                .expect("parent trait should be dyn compatible");
326                            Ok(tyref)
327                        })?;
328                    let vtbl_struct = self.erase_region_binder(vtbl_struct);
329                    let ty = Ty::new(TyKind::Ref(
330                        Region::Static,
331                        Ty::new(TyKind::Adt(vtbl_struct)),
332                        RefKind::Shared,
333                    ));
334                    let name = format!("super_trait_{}", supertrait_counter.next().unwrap());
335                    (name, ty)
336                }
337            };
338            fields.push(Field {
339                span,
340                attr_info: AttrInfo::dummy_public(),
341                name: Some(name),
342                ty,
343            });
344        }
345        Ok(fields)
346    }
347
348    /// This is a temporary check until we support `dyn Trait` with `--monomorphize`.
349    pub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), Error> {
350        if self.monomorphize() {
351            raise_error!(
352                self,
353                span,
354                "`dyn Trait` is not yet supported with `--monomorphize`"
355            )
356        }
357        Ok(())
358    }
359
360    /// Construct the type of the vtable for this trait.
361    ///
362    /// It's a struct that has for generics the generics of the trait + one parameter for each
363    /// associated type of the trait and its parents.
364    ///
365    /// struct TraitVTable<TraitArgs.., AssocTys..> {
366    ///   size: usize,
367    ///   align: usize,
368    ///   drop: fn(*mut dyn Trait<...>),
369    ///   method_name: fn(&dyn Trait<...>, Args..) -> Output,
370    ///   ... other methods
371    ///   super_trait_0: &'static SuperTrait0VTable
372    ///   ... other supertraits
373    /// }
374    pub(crate) fn translate_vtable_struct(
375        mut self,
376        type_id: TypeDeclId,
377        item_meta: ItemMeta,
378        trait_def: &hax::FullDef,
379    ) -> Result<TypeDecl, Error> {
380        let span = item_meta.span;
381        if !self.trait_is_dyn_compatible(trait_def.def_id())? {
382            raise_error!(
383                self,
384                span,
385                "Trying to compute the vtable type \
386                for a non-dyn-compatible trait"
387            );
388        }
389        self.check_no_monomorphize(span)?;
390
391        let (hax::FullDefKind::Trait {
392            dyn_self,
393            implied_predicates,
394            ..
395        }
396        | hax::FullDefKind::TraitAlias {
397            dyn_self,
398            implied_predicates,
399            ..
400        }) = trait_def.kind()
401        else {
402            panic!()
403        };
404        let Some(dyn_self) = dyn_self else {
405            panic!("Trying to generate a vtable for a non-dyn-compatible trait")
406        };
407
408        // The `dyn Trait<Args..>` type for this trait.
409        let mut dyn_self = {
410            let dyn_self = self.translate_ty(span, dyn_self)?;
411            let TyKind::DynTrait(mut dyn_pred) = dyn_self.kind().clone() else {
412                panic!("incorrect `dyn_self`")
413            };
414
415            // Add one generic parameter for each associated type of this trait and its parents. We
416            // then use that in `dyn_self`
417            for (i, ty_constraint) in dyn_pred
418                .binder
419                .params
420                .trait_type_constraints
421                .iter_mut()
422                .enumerate()
423            {
424                let name = format!("Ty{i}");
425                let new_ty = self
426                    .the_only_binder_mut()
427                    .params
428                    .types
429                    .push_with(|index| TypeParam { index, name });
430                // Moving that type under two levels of binders: the `DynPredicate` binder and the
431                // type constraint binder.
432                let new_ty =
433                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::new(2), new_ty)).into_ty();
434                ty_constraint.skip_binder.ty = new_ty;
435            }
436            TyKind::DynTrait(dyn_pred).into_ty()
437        };
438
439        let mut field_map = IndexVec::new();
440        let mut supertrait_map: IndexMap<TraitClauseId, _> =
441            (0..implied_predicates.predicates.len())
442                .map(|_| None)
443                .collect();
444        let (mut kind, layout) = if item_meta.opacity.with_private_contents().is_opaque() {
445            (TypeDeclKind::Opaque, None)
446        } else {
447            // First construct fields that use the real method signatures (which may use the `Self`
448            // type). We fixup the types and generics below.
449            let vtable_data = self.prepare_vtable_fields(trait_def, implied_predicates)?;
450            let fields = self.gen_vtable_struct_fields(span, &vtable_data)?;
451            let kind = TypeDeclKind::Struct(fields);
452            let layout = self.generate_naive_layout(span, &kind)?;
453            supertrait_map = vtable_data.supertrait_map;
454            field_map = vtable_data.fields.map_ref(|tr_field| match *tr_field {
455                TrVTableField::Size => VTableField::Size,
456                TrVTableField::Align => VTableField::Align,
457                TrVTableField::Drop => VTableField::Drop,
458                TrVTableField::Method(name, ..) => VTableField::Method(name),
459                TrVTableField::SuperTrait(clause_id, ..) => VTableField::SuperTrait(clause_id),
460            });
461            (kind, Some(layout))
462        };
463
464        // Replace any use of `Self` with `dyn Trait<...>`, and remove the `Self` type variable
465        // from the generic parameters.
466        let mut generics = self.into_generics();
467        {
468            dyn_self = dynify(dyn_self, None, false);
469            generics = dynify(generics, Some(dyn_self.clone()), false);
470            kind = dynify(kind, Some(dyn_self.clone()), true);
471            generics.types.remove_and_shift_ids(TypeVarId::ZERO);
472            generics.types.iter_mut().for_each(|ty| {
473                ty.index -= 1;
474            });
475        }
476
477        let dyn_predicate = dyn_self
478            .kind()
479            .as_dyn_trait()
480            .expect("incorrect `dyn_self`");
481        Ok(TypeDecl {
482            def_id: type_id,
483            item_meta: item_meta,
484            generics: generics,
485            src: ItemSource::VTableTy {
486                dyn_predicate: dyn_predicate.clone(),
487                field_map,
488                supertrait_map,
489            },
490            kind,
491            layout,
492            // A vtable struct is always sized
493            ptr_metadata: PtrMetadata::None,
494            repr: None,
495        })
496    }
497}
498
499//// Generate a vtable value.
500impl ItemTransCtx<'_, '_> {
501    pub fn translate_vtable_instance_ref(
502        &mut self,
503        span: Span,
504        trait_ref: &hax::TraitRef,
505        impl_ref: &hax::ItemRef,
506    ) -> Result<Option<GlobalDeclRef>, Error> {
507        self.translate_vtable_instance_ref_maybe_enqueue(true, span, trait_ref, impl_ref)
508    }
509
510    pub fn translate_vtable_instance_ref_no_enqueue(
511        &mut self,
512        span: Span,
513        trait_ref: &hax::TraitRef,
514        impl_ref: &hax::ItemRef,
515    ) -> Result<Option<GlobalDeclRef>, Error> {
516        self.translate_vtable_instance_ref_maybe_enqueue(false, span, trait_ref, impl_ref)
517    }
518
519    pub fn translate_vtable_instance_ref_maybe_enqueue(
520        &mut self,
521        enqueue: bool,
522        span: Span,
523        trait_ref: &hax::TraitRef,
524        impl_ref: &hax::ItemRef,
525    ) -> Result<Option<GlobalDeclRef>, Error> {
526        if !self.trait_is_dyn_compatible(&trait_ref.def_id)? {
527            return Ok(None);
528        }
529        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
530        // `dyn Trait` coercion.
531        // TODO(dyn): To do this properly we'd need to know for each clause whether it ultimately
532        // ends up used in a vtable cast.
533        let vtable_ref: GlobalDeclRef = self.translate_item_maybe_enqueue(
534            span,
535            enqueue,
536            impl_ref,
537            TransItemSourceKind::VTableInstance(TraitImplSource::Normal),
538        )?;
539        Ok(Some(vtable_ref))
540    }
541
542    /// Local helper function to get the vtable struct reference and trait declaration reference
543    fn get_vtable_instance_info<'a>(
544        &mut self,
545        span: Span,
546        impl_def: &'a hax::FullDef,
547        impl_kind: &TraitImplSource,
548    ) -> Result<(TraitImplRef, TypeDeclRef), Error> {
549        let implemented_trait = match impl_def.kind() {
550            hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref,
551            _ => unreachable!(),
552        };
553        let vtable_struct_ref = self
554            .translate_vtable_struct_ref(span, implemented_trait)?
555            .expect("trait should be dyn-compatible");
556        let impl_ref = self.translate_item(
557            span,
558            impl_def.this(),
559            TransItemSourceKind::TraitImpl(*impl_kind),
560        )?;
561        Ok((impl_ref, vtable_struct_ref))
562    }
563
564    /// E.g.,
565    /// ```
566    /// global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
567    ///     size: size_of(Foo),
568    ///     align: align_of(Foo),
569    ///     drop: <Foo as Destruct>::drop_in_place,
570    ///     method_0: <Foo as Trait>::method_0::{shim},
571    ///     method_1: <Foo as Trait>::method_1::{shim},
572    ///     ...
573    ///     super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
574    ///     super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
575    ///     ...
576    /// }
577    /// ```
578    pub(crate) fn translate_vtable_instance(
579        mut self,
580        global_id: GlobalDeclId,
581        item_meta: ItemMeta,
582        impl_def: &hax::FullDef,
583        impl_kind: &TraitImplSource,
584    ) -> Result<GlobalDecl, Error> {
585        let span = item_meta.span;
586        self.check_no_monomorphize(span)?;
587
588        let (impl_ref, vtable_struct_ref) =
589            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
590        // Initializer function for this global.
591        let init = self.register_item(
592            span,
593            impl_def.this(),
594            TransItemSourceKind::VTableInstanceInitializer(*impl_kind),
595        );
596
597        Ok(GlobalDecl {
598            def_id: global_id,
599            item_meta,
600            generics: self.into_generics(),
601            src: ItemSource::VTableInstance { impl_ref },
602            // it should be static to have its own address
603            global_kind: GlobalKind::Static,
604            ty: Ty::new(TyKind::Adt(vtable_struct_ref)),
605            init,
606        })
607    }
608
609    fn add_method_to_vtable_value(
610        &mut self,
611        span: Span,
612        impl_def: &hax::FullDef,
613        item: &hax::ImplAssocItem,
614        mut mk_field: impl FnMut(ConstantExprKind),
615    ) -> Result<(), Error> {
616        // Exit if the item isn't a vtable safe method.
617        match self.poly_hax_def(&item.decl_def_id)?.kind() {
618            hax::FullDefKind::AssocFn {
619                vtable_sig: Some(_),
620                ..
621            } => {}
622            _ => return Ok(()),
623        }
624
625        let const_kind = match &item.value {
626            hax::ImplAssocItemValue::Provided {
627                def_id: item_def_id,
628                ..
629            } => {
630                // The method is vtable safe so it has no generics, hence we can reuse the impl
631                // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`.
632                let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id);
633                let shim_ref =
634                    self.translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)?;
635                ConstantExprKind::FnDef(shim_ref)
636            }
637            hax::ImplAssocItemValue::DefaultedFn { .. } => ConstantExprKind::Opaque(
638                "shim for default methods \
639                    aren't yet supported"
640                    .to_string(),
641            ),
642            _ => return Ok(()),
643        };
644
645        mk_field(const_kind);
646
647        Ok(())
648    }
649
650    fn add_supertraits_to_vtable_value(
651        &mut self,
652        span: Span,
653        trait_def: &hax::FullDef,
654        impl_def: &hax::FullDef,
655        mut mk_field: impl FnMut(ConstantExprKind),
656    ) -> Result<(), Error> {
657        let hax::FullDefKind::TraitImpl {
658            implied_impl_exprs, ..
659        } = impl_def.kind()
660        else {
661            unreachable!()
662        };
663        let hax::FullDefKind::Trait {
664            implied_predicates, ..
665        } = trait_def.kind()
666        else {
667            unreachable!()
668        };
669        for ((clause, _), impl_expr) in implied_predicates.predicates.iter().zip(implied_impl_exprs)
670        {
671            let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
672                continue;
673            };
674            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
675            if !self.pred_is_for_self(&pred.trait_ref) {
676                continue;
677            }
678
679            let bound_tyref =
680                self.translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
681                    let tyref = ctx
682                        .translate_vtable_struct_ref(span, tref)?
683                        .expect("parent trait should be dyn compatible");
684                    Ok(tyref)
685                })?;
686            let vtable_def_ref = self.erase_region_binder(bound_tyref);
687            let fn_ptr_ty = TyKind::Adt(vtable_def_ref).into_ty();
688            let kind = match &impl_expr.r#impl {
689                hax::ImplExprAtom::Concrete(impl_item) => {
690                    let bound_gref: RegionBinder<GlobalDeclRef> =
691                        self.translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
692                            let gref = ctx
693                                .translate_vtable_instance_ref(span, tref, impl_item)?
694                                .expect("parent trait should be dyn compatible");
695                            Ok(gref)
696                        })?;
697                    let vtable_instance_ref = self.erase_region_binder(bound_gref);
698                    let global = Box::new(ConstantExpr {
699                        kind: ConstantExprKind::Global(vtable_instance_ref),
700                        ty: fn_ptr_ty,
701                    });
702                    ConstantExprKind::Ref(global)
703                }
704                // TODO(dyn): builtin impls
705                _ => ConstantExprKind::Opaque("missing supertrait vtable".into()),
706            };
707            mk_field(kind);
708        }
709        Ok(())
710    }
711
712    /// Generate the body of the vtable instance function.
713    /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls.
714    /// ```ignore
715    /// let ret@0 : VTable;
716    /// ret@0 = VTable { ... };
717    /// return;
718    /// ```
719    fn gen_vtable_instance_init_body(
720        &mut self,
721        span: Span,
722        impl_def: &hax::FullDef,
723        vtable_struct_ref: TypeDeclRef,
724    ) -> Result<Body, Error> {
725        let hax::FullDefKind::TraitImpl {
726            trait_pred, items, ..
727        } = impl_def.kind()
728        else {
729            unreachable!()
730        };
731        let trait_def = self.hax_def(&trait_pred.trait_ref)?;
732        let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?;
733        // The type this impl is for.
734        let self_ty = &implemented_trait.generics.types[0];
735
736        let mut builder = BodyBuilder::new(span, 0);
737        let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone()));
738        let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone());
739
740        // Retreive the expected field types from the struct definition. This avoids complicated
741        // substitutions.
742        let field_tys = {
743            let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone();
744            let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())?
745            else {
746                unreachable!()
747            };
748            let TypeDeclKind::Struct(fields) = &vtable_def.kind else {
749                unreachable!()
750            };
751            fields
752                .iter()
753                .map(|f| &f.ty)
754                .cloned()
755                .map(|ty| ty.substitute(&vtable_struct_ref.generics))
756                .collect_vec()
757        };
758
759        let mut aggregate_fields = vec![];
760        // For each vtable field, assign the desired value to a new local.
761        let mut field_ty_iter = field_tys.into_iter();
762
763        let size_ty = field_ty_iter.next().unwrap();
764        let size_local = builder.new_var(Some("size".to_string()), size_ty);
765        builder.push_statement(StatementKind::Assign(
766            size_local.clone(),
767            Rvalue::NullaryOp(NullOp::SizeOf, self_ty.clone()),
768        ));
769        aggregate_fields.push(Operand::Move(size_local));
770
771        let align_ty = field_ty_iter.next().unwrap();
772        let align_local = builder.new_var(Some("align".to_string()), align_ty);
773        builder.push_statement(StatementKind::Assign(
774            align_local.clone(),
775            Rvalue::NullaryOp(NullOp::AlignOf, self_ty.clone()),
776        ));
777        aggregate_fields.push(Operand::Move(align_local));
778
779        // Helper to fill in the remaining fields with constant values.
780        let mut mk_field = |kind| {
781            let ty = field_ty_iter.next().unwrap();
782            aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty })));
783        };
784
785        let drop_shim =
786            self.translate_item(span, impl_def.this(), TransItemSourceKind::VTableDropShim)?;
787
788        mk_field(ConstantExprKind::FnDef(drop_shim));
789
790        for item in items {
791            self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?;
792        }
793
794        self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?;
795
796        if field_ty_iter.next().is_some() {
797            raise_error!(
798                self,
799                span,
800                "Missed some fields in vtable value construction"
801            )
802        }
803
804        // Construct the final struct.
805        builder.push_statement(StatementKind::Assign(
806            ret_place,
807            Rvalue::Aggregate(
808                AggregateKind::Adt(vtable_struct_ref.clone(), None, None),
809                aggregate_fields,
810            ),
811        ));
812
813        Ok(Body::Unstructured(builder.build()))
814    }
815
816    pub(crate) fn translate_vtable_instance_init(
817        mut self,
818        init_func_id: FunDeclId,
819        item_meta: ItemMeta,
820        impl_def: &hax::FullDef,
821        impl_kind: &TraitImplSource,
822    ) -> Result<FunDecl, Error> {
823        let span = item_meta.span;
824        self.check_no_monomorphize(span)?;
825
826        let (impl_ref, vtable_struct_ref) =
827            self.get_vtable_instance_info(span, impl_def, impl_kind)?;
828        let init_for = self.register_item(
829            span,
830            impl_def.this(),
831            TransItemSourceKind::VTableInstance(*impl_kind),
832        );
833
834        // Signature: `() -> VTable`.
835        let sig = FunSig {
836            is_unsafe: false,
837            inputs: vec![],
838            output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())),
839        };
840
841        let body = match impl_kind {
842            _ if item_meta.opacity.with_private_contents().is_opaque() => Body::Opaque,
843            TraitImplSource::Normal => {
844                self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?
845            }
846            _ => {
847                raise_error!(
848                    self,
849                    span,
850                    "Don't know how to generate a vtable for a virtual impl {impl_kind:?}"
851                );
852            }
853        };
854
855        Ok(FunDecl {
856            def_id: init_func_id,
857            item_meta: item_meta,
858            generics: self.into_generics(),
859            signature: sig,
860            src: ItemSource::VTableInstance { impl_ref },
861            is_global_initializer: Some(init_for),
862            body,
863        })
864    }
865
866    /// The target vtable shim body looks like:
867    /// ```ignore
868    /// local ret@0 : ReturnTy;
869    /// // the shim receiver of this shim function
870    /// local shim_self@1 : ShimReceiverTy;
871    /// // the arguments of the impl function
872    /// local arg1@2 : Arg1Ty;
873    /// ...
874    /// local argN@N : ArgNTy;
875    /// // the target receiver of the impl function
876    /// local target_self@(N+1) : TargetReceiverTy;
877    /// // perform some conversion to cast / re-box the shim receiver to the target receiver
878    /// ...
879    /// target_self@(N+1) := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
880    /// // call the impl function and assign the result to ret@0
881    /// ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N);
882    /// ```
883    fn translate_vtable_shim_body(
884        &mut self,
885        span: Span,
886        target_receiver: &Ty,
887        shim_signature: &FunSig,
888        impl_func_def: &hax::FullDef,
889    ) -> Result<Body, Error> {
890        let mut builder = BodyBuilder::new(span, shim_signature.inputs.len());
891
892        let ret_place = builder.new_var(None, shim_signature.output.clone());
893        let mut method_args = shim_signature
894            .inputs
895            .iter()
896            .map(|ty| builder.new_var(None, ty.clone()))
897            .collect_vec();
898        let target_self = builder.new_var(None, target_receiver.clone());
899
900        // Replace the `dyn Trait` receiver with the concrete one.
901        let shim_self = mem::replace(&mut method_args[0], target_self.clone());
902
903        // Perform the core concretization cast.
904        // FIXME: need to unpack & re-pack the structure for cases like `Rc`, `Arc`, `Pin` and
905        // (when --raw-boxes is on) `Box`
906        let rval = Rvalue::UnaryOp(
907            UnOp::Cast(CastKind::Concretize(
908                shim_self.ty().clone(),
909                target_self.ty().clone(),
910            )),
911            Operand::Move(shim_self.clone()),
912        );
913        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
914
915        let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun);
916        let generics = self.outermost_binder().params.identity_args();
917        builder.call(Call {
918            func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)),
919            args: method_args
920                .into_iter()
921                .map(|arg| Operand::Move(arg))
922                .collect(),
923            dest: ret_place,
924        });
925
926        Ok(Body::Unstructured(builder.build()))
927    }
928
929    /// The target vtable drop_shim body looks like:
930    /// ```ignore
931    /// local ret@0 : ();
932    /// // the shim receiver of this drop_shim function
933    /// local shim_self@1 : ShimReceiverTy;
934    /// // the target receiver of the drop_shim
935    /// local target_self@2 : TargetReceiverTy;
936    /// // perform some conversion to cast / re-box the drop_shim receiver to the target receiver
937    /// target_self@2 := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
938    /// Drop(*target_self@2);
939    /// ```
940    fn translate_vtable_drop_shim_body(
941        &mut self,
942        span: Span,
943        shim_receiver: &Ty,
944        target_receiver: &Ty,
945        trait_pred: &TraitPredicate,
946    ) -> Result<Body, Error> {
947        let mut builder = BodyBuilder::new(span, 1);
948
949        builder.new_var(Some("ret".into()), Ty::mk_unit());
950        let dyn_self = builder.new_var(Some("dyn_self".into()), shim_receiver.clone());
951        let target_self = builder.new_var(Some("target_self".into()), target_receiver.clone());
952
953        // Perform the core concretization cast.
954        let rval = Rvalue::UnaryOp(
955            UnOp::Cast(CastKind::Concretize(
956                dyn_self.ty().clone(),
957                target_self.ty().clone(),
958            )),
959            Operand::Move(dyn_self.clone()),
960        );
961        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
962
963        // Build a reference to `impl Destruct for T`. Given the
964        // target_receiver type `T`, use Hax to solve `T: Destruct`
965        // and translate the resolved result to `TraitRef` of the
966        // `drop_in_place`
967        let destruct_trait = self.tcx.lang_items().destruct_trait().unwrap();
968        let impl_expr: hax::ImplExpr = {
969            let s = self.hax_state_with_id();
970            let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
971            let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
972            let tref =
973                rustc_middle::ty::TraitRef::new_from_args(self.tcx, destruct_trait, generics);
974            hax::solve_trait(s, rustc_middle::ty::Binder::dummy(tref))
975        };
976        let tref = self.translate_trait_impl_expr(span, &impl_expr)?;
977
978        // Drop(*target_self)
979        let drop_arg = target_self.clone().deref();
980        builder.insert_drop(drop_arg, tref);
981
982        Ok(Body::Unstructured(builder.build()))
983    }
984
985    pub(crate) fn translate_vtable_drop_shim(
986        mut self,
987        fun_id: FunDeclId,
988        item_meta: ItemMeta,
989        impl_def: &hax::FullDef,
990    ) -> Result<FunDecl, Error> {
991        let span = item_meta.span;
992
993        let hax::FullDefKind::TraitImpl {
994            dyn_self: Some(dyn_self),
995            trait_pred,
996            ..
997        } = impl_def.kind()
998        else {
999            raise_error!(
1000                self,
1001                span,
1002                "Trying to generate a vtable drop shim for a non-trait impl"
1003            );
1004        };
1005
1006        // `*mut dyn Trait`
1007        let ref_dyn_self =
1008            TyKind::RawPtr(self.translate_ty(span, dyn_self)?, RefKind::Mut).into_ty();
1009        // `*mut T` for `impl Trait for T`
1010        let ref_target_self = {
1011            let impl_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
1012            TyKind::RawPtr(impl_trait.generics.types[0].clone(), RefKind::Mut).into_ty()
1013        };
1014
1015        // `*mut dyn Trait -> ()`
1016        let signature = FunSig {
1017            is_unsafe: true,
1018            inputs: vec![ref_dyn_self.clone()],
1019            output: Ty::mk_unit(),
1020        };
1021
1022        let body: Body = self.translate_vtable_drop_shim_body(
1023            span,
1024            &ref_dyn_self,
1025            &ref_target_self,
1026            trait_pred,
1027        )?;
1028
1029        Ok(FunDecl {
1030            def_id: fun_id,
1031            item_meta,
1032            generics: self.into_generics(),
1033            signature,
1034            src: ItemSource::VTableMethodShim,
1035            is_global_initializer: None,
1036            body,
1037        })
1038    }
1039
1040    pub(crate) fn translate_vtable_shim(
1041        mut self,
1042        fun_id: FunDeclId,
1043        item_meta: ItemMeta,
1044        impl_func_def: &hax::FullDef,
1045    ) -> Result<FunDecl, Error> {
1046        let span = item_meta.span;
1047        self.check_no_monomorphize(span)?;
1048
1049        let hax::FullDefKind::AssocFn {
1050            vtable_sig: Some(vtable_sig),
1051            sig: target_signature,
1052            ..
1053        } = impl_func_def.kind()
1054        else {
1055            raise_error!(
1056                self,
1057                span,
1058                "Trying to generate a vtable shim for a non-vtable-safe method"
1059            );
1060        };
1061
1062        // The signature of the shim function.
1063        let signature = self.translate_fun_sig(span, &vtable_sig.value)?;
1064        // The concrete receiver we will cast to.
1065        let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?;
1066
1067        trace!(
1068            "[VtableShim] Obtained dyn signature with receiver type: {}",
1069            signature.inputs[0].with_ctx(&self.into_fmt())
1070        );
1071
1072        let body = if item_meta.opacity.with_private_contents().is_opaque() {
1073            Body::Opaque
1074        } else {
1075            self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?
1076        };
1077
1078        Ok(FunDecl {
1079            def_id: fun_id,
1080            item_meta,
1081            generics: self.into_generics(),
1082            signature,
1083            src: ItemSource::VTableMethodShim,
1084            is_global_initializer: None,
1085            body,
1086        })
1087    }
1088}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
