charon_driver/translate/
translate_trait_objects.rs

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

charon_driver/translate/
translate_trait_objects.rs
