charon_driver/translate/
translate_trait_objects.rs

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

charon_driver/translate/
translate_trait_objects.rs
