charon_driver/translate/
translate_trait_objects.rs

1use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
2use hax::{AssocItemContainer, GenericArg, TraitPredicate};
3use itertools::Itertools;
4use rustc_span::kw;
5use std::mem;
6
7use super::{
8    translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel,
9};
10use charon_lib::formatter::IntoFormatter;
11use charon_lib::ids::{IndexMap, IndexVec};
12use charon_lib::pretty::FmtWithCtx;
13use charon_lib::ullbc_ast::*;
14
15fn usize_ty() -> Ty {
16    Ty::new(TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)))
17}
18
19// Vtable method values that are used to vtable initilization functions.
20// In poly mode, they are const values of shim function pointers direcly filled in vtable fields.
21// In mono mode, they are used for construction of casting statements (see `mk_cast` in `gen_vtable_instance_init_body` for details).
22// Specifically, the tuple `(String, Ty, FnPtr)` represent method names,
23// the type of the shim function pointers and the shim function pointers, respectively.
24enum VtableMethodValue {
25    Const(ConstantExprKind),
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 ItemTransCtx<'_, '_> {
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: 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(TraitItemName, hax::Binder<hax::TyFnSig>),
182    SuperTrait(TraitClauseId, hax::Clause),
183}
184
185pub struct VTableData {
186    pub fields: IndexVec<FieldId, TrVTableField>,
187    pub supertrait_map: IndexMap<TraitClauseId, Option<FieldId>>,
188}
189
190//// Generate the vtable struct.
191impl ItemTransCtx<'_, '_> {
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,
293        implied_predicates: &hax::GenericPredicates,
294    ) -> Result<VTableData, Error> {
295        let mut supertrait_map: IndexMap<TraitClauseId, _> =
296            (0..implied_predicates.predicates.len())
297                .map(|_| None)
298                .collect();
299        let mut fields = IndexVec::new();
300
301        // Basic fields.
302        fields.push(TrVTableField::Size);
303        fields.push(TrVTableField::Align);
304        fields.push(TrVTableField::Drop);
305
306        // Method fields.
307        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
308            for item in items {
309                let item_def_id = &item.def_id;
310                // This is ok because dyn-compatible methods don't have generics.
311                let item_def =
312                    self.hax_def(&trait_def.this().with_def_id(self.hax_state(), item_def_id))?;
313                if let hax::FullDefKind::AssocFn {
314                    sig,
315                    vtable_sig: Some(_),
316                    ..
317                } = item_def.kind()
318                {
319                    let name = self.translate_trait_item_name(&item_def_id)?;
320                    fields.push(TrVTableField::Method(name, sig.clone()));
321                }
322            }
323        }
324
325        // Supertrait fields.
326        for (i, pred) in implied_predicates.iter_trait_clauses().enumerate() {
327            let trait_clause_id = TraitClauseId::from_raw(i); // One trait clause id per trait clause
328            let clause = &pred.clause;
329            let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else {
330                unreachable!()
331            };
332            // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait.
333            if self.pred_is_for_self(&pred.trait_ref) {
334                if !self.trait_is_dyn_compatible(&pred.trait_ref.def_id)? {
335                    // We add fake `Destruct` supertraits, but these are not dyn-compatible.
336                    self.assert_is_destruct(&pred.trait_ref);
337                    continue;
338                }
339                supertrait_map[trait_clause_id] = Some(fields.next_idx());
340                fields.push(TrVTableField::SuperTrait(trait_clause_id, clause.clone()));
341            }
342        }
343
344        Ok(VTableData {
345            fields,
346            supertrait_map,
347        })
348    }
349
350    /// The Charon+Hax machinery will add Destruct super-traits to trait bounds,
351    /// however for `dyn Trait` the Destruct super-trait is unexepcted, as it is not
352    /// dyn-compatible.
353    /// We use this function to ensure that any non dyn-compatible super-trait is
354    /// Destruct and can be safely ignored.
355    fn assert_is_destruct(&self, tref: &hax::TraitRef) {
356        assert!(
357            tref.def_id
358                .as_rust_def_id()
359                .is_some_and(|id| self.tcx.is_lang_item(id, rustc_hir::LangItem::Destruct)),
360            "unexpected non-dyn compatible supertrait: {:?}",
361            tref.def_id
362        );
363    }
364
365    fn gen_vtable_struct_fields(
366        &mut self,
367        span: Span,
368        self_trait_ref: &TraitRef,
369        vtable_data: &VTableData,
370    ) -> Result<IndexVec<FieldId, Field>, Error> {
371        let mut fields = IndexVec::new();
372        let mut supertrait_counter = (0..).into_iter();
373        for field in &vtable_data.fields {
374            let (name, ty) = match field {
375                TrVTableField::Size => ("size".into(), usize_ty()),
376                TrVTableField::Align => ("align".into(), usize_ty()),
377                TrVTableField::Drop => {
378                    // In Mono mode, drop shims are opaque function pointers.
379                    if self.monomorphize() {
380                        let erased_ptr_ty = Ty::new(TyKind::RawPtr(Ty::mk_unit(), RefKind::Shared));
381                        ("drop".into(), erased_ptr_ty)
382                    } else {
383                        let self_ty =
384                            TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
385                        let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
386                        let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(FunSig {
387                            is_unsafe: true,
388                            inputs: [self_ptr].into(),
389                            output: Ty::mk_unit(),
390                        })));
391                        ("drop".into(), drop_ty)
392                    }
393                }
394                TrVTableField::Method(item_name, sig) => {
395                    let field_name = format!("method_{}", item_name.0);
396                    // In Mono mode, method shims are opaque function pointers.
397                    if self.monomorphize() {
398                        let erased_ptr_ty = Ty::new(TyKind::RawPtr(Ty::mk_unit(), RefKind::Shared));
399                        (field_name, erased_ptr_ty)
400                    } else {
401                        // The method is defined in a context that has an extra `Self: Trait` clause, so
402                        // we translate it bound first.
403                        let bound_sig = self.inside_binder(BinderKind::Other, |ctx| {
404                            ctx.innermost_binder_mut()
405                                .trait_preds
406                                .insert(hax::GenericPredicateId::TraitSelf, TraitClauseId::ZERO);
407                            ctx.translate_poly_fun_sig(span, &sig)
408                        })?;
409                        let sig = bound_sig.apply(&{
410                            let mut generics = GenericArgs::empty();
411                            // Provide the `Self` clause.
412                            generics.trait_refs.push(self_trait_ref.clone());
413                            generics
414                        });
415                        let ty = TyKind::FnPtr(sig).into_ty();
416                        (field_name, ty)
417                    }
418                }
419                TrVTableField::SuperTrait(_, clause) => {
420                    let vtbl_struct =
421                        self.translate_region_binder(span, &clause.kind, |ctx, kind| {
422                            let hax::ClauseKind::Trait(pred) = kind else {
423                                unreachable!()
424                            };
425                            ctx.translate_vtable_struct_ref(span, &pred.trait_ref)
426                        })?;
427                    let vtbl_struct = self.erase_region_binder(vtbl_struct);
428                    let ty = Ty::new(TyKind::Ref(
429                        Region::Static,
430                        Ty::new(TyKind::Adt(vtbl_struct)),
431                        RefKind::Shared,
432                    ));
433                    let name = format!("super_trait_{}", supertrait_counter.next().unwrap());
434                    (name, ty)
435                }
436            };
437            fields.push(Field {
438                span,
439                attr_info: AttrInfo::dummy_public(),
440                name: Some(name),
441                ty,
442            });
443        }
444        Ok(fields)
445    }
446
447    // Register preshim functions for the drop shim function and method shim functions.
448    // See `translate_vtable_method_preshim` for the description of preshim functions.
449    #[tracing::instrument(skip(self, span))]
450    fn register_preshim(&mut self, span: Span, trait_def: &hax::FullDef) -> Result<(), Error> {
451        let item_src =
452            TransItemSource::monomorphic_trait(&trait_def.def_id(), TransItemSourceKind::TraitDecl);
453        let item_id = match self.t_ctx.id_map.get(&item_src) {
454            Some(tid) => *tid,
455            None => {
456                panic!("MONO: expected trait has not been translated");
457            }
458        };
459
460        let trait_id = item_id
461            .try_into()
462            .expect("MONO: The item_id should be a trait decl id");
463
464        let mut preshim_types = vec![];
465        for arg in trait_def.this().generic_args.iter().skip(1) {
466            if let GenericArg::Type(hax_ty) = arg {
467                preshim_types.push(self.translate_ty(span, hax_ty)?);
468            }
469        }
470        if let hax::FullDefKind::Trait {
471            dyn_self: Some(dyn_self),
472            ..
473        } = trait_def.kind()
474        {
475            let dyn_self = self.translate_ty(span, dyn_self)?;
476            if let TyKind::DynTrait(pred) = dyn_self.kind() {
477                for ttc in &pred.binder.params.trait_type_constraints {
478                    preshim_types.push(ttc.skip_binder.ty.clone());
479                }
480            }
481        }
482
483        if !self
484            .t_ctx
485            .translated_preshims
486            .insert((trait_id, preshim_types))
487        {
488            return Ok(());
489        }
490
491        // translate drop_preshim
492        let _: FnPtr = self.translate_item(
493            span,
494            trait_def.this(),
495            TransItemSourceKind::VTableDropPreShim,
496        )?;
497
498        // Method fields.
499        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
500            for item in items {
501                let item_def_id = &item.def_id;
502                // This is ok because dyn-compatible methods don't have generics.
503                let item_def =
504                    self.hax_def(&trait_def.this().with_def_id(self.hax_state(), item_def_id))?;
505                if let hax::FullDefKind::AssocFn {
506                    vtable_sig: Some(_),
507                    ..
508                } = item_def.kind()
509                {
510                    let name = self.translate_trait_item_name(&item_def_id)?;
511
512                    let _: FnPtr = self.translate_item(
513                        span,
514                        trait_def.this(),
515                        TransItemSourceKind::VTableMethodPreShim(trait_id, name),
516                    )?;
517                }
518            }
519        }
520
521        Ok(())
522    }
523
524    /// Construct the type of the vtable for this trait.
525    ///
526    /// It's a struct that has for generics the generics of the trait + one parameter for each
527    /// associated type of the trait and its parents.
528    ///
529    /// struct TraitVTable<TraitArgs.., AssocTys..> {
530    ///   size: usize,
531    ///   align: usize,
532    ///   drop: fn(*mut dyn Trait<...>),
533    ///   method_name: fn(&dyn Trait<...>, Args..) -> Output,
534    ///   ... other methods
535    ///   super_trait_0: &'static SuperTrait0VTable
536    ///   ... other supertraits
537    /// }
538    pub(crate) fn translate_vtable_struct(
539        mut self,
540        type_id: TypeDeclId,
541        item_meta: ItemMeta,
542        trait_def: &hax::FullDef,
543    ) -> Result<TypeDecl, Error> {
544        let mono = self.monomorphize();
545        let span = item_meta.span;
546        if !self.trait_is_dyn_compatible(trait_def.def_id())? {
547            raise_error!(
548                self,
549                span,
550                "Trying to compute the vtable type \
551                for a non-dyn-compatible trait"
552            );
553        }
554
555        let (hax::FullDefKind::Trait {
556            self_predicate,
557            dyn_self,
558            implied_predicates,
559            ..
560        }
561        | hax::FullDefKind::TraitAlias {
562            self_predicate,
563            dyn_self,
564            implied_predicates,
565            ..
566        }) = trait_def.kind()
567        else {
568            panic!()
569        };
570        let Some(dyn_self) = dyn_self else {
571            panic!("Trying to generate a vtable for a non-dyn-compatible trait")
572        };
573
574        let self_trait_ref = TraitRef::new(
575            TraitRefKind::SelfId,
576            RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?),
577        );
578
579        let mut field_map = IndexVec::new();
580        let mut supertrait_map: IndexMap<TraitClauseId, _> =
581            (0..implied_predicates.predicates.len())
582                .map(|_| None)
583                .collect();
584        let (mut kind, layout) = if item_meta.opacity.with_private_contents().is_opaque() {
585            (TypeDeclKind::Opaque, None)
586        } else {
587            // First construct fields that use the real method signatures (which may use the `Self`
588            // type). We fixup the types and generics below.
589            let vtable_data = self.prepare_vtable_fields(trait_def, implied_predicates)?;
590            let fields = self.gen_vtable_struct_fields(span, &self_trait_ref, &vtable_data)?;
591
592            let kind = TypeDeclKind::Struct(fields);
593            let layout = self.generate_naive_layout(span, &kind)?;
594            supertrait_map = vtable_data.supertrait_map;
595            field_map = vtable_data.fields.map_ref(|tr_field| match *tr_field {
596                TrVTableField::Size => VTableField::Size,
597                TrVTableField::Align => VTableField::Align,
598                TrVTableField::Drop => VTableField::Drop,
599                TrVTableField::Method(name, ..) => VTableField::Method(name),
600                TrVTableField::SuperTrait(clause_id, ..) => VTableField::SuperTrait(clause_id),
601            });
602            (kind, Some(layout))
603        };
604
605        let mut generics = Default::default();
606
607        let dyn_predicate = if mono {
608            DynPredicate {
609                binder: Binder {
610                    params: GenericParams::empty(),
611                    skip_binder: TyKind::Error(
612                        "mono vtable dyn predicate is intentionally erased".to_string(),
613                    )
614                    .into_ty(),
615                    kind: BinderKind::Dyn,
616                },
617            }
618        } else {
619            // The `dyn Trait<Args..>` type for this trait.
620            // This is only used in poly mode
621            let mut dyn_self = {
622                let dyn_self = self.translate_ty(span, dyn_self)?;
623                let TyKind::DynTrait(mut dyn_pred) = dyn_self.kind().clone() else {
624                    panic!("incorrect `dyn_self`")
625                };
626
627                // Add one generic parameter for each associated type of this trait and its parents. We
628                // then use that in `dyn_self`
629                for (i, ty_constraint) in dyn_pred
630                    .binder
631                    .params
632                    .trait_type_constraints
633                    .iter_mut()
634                    .enumerate()
635                {
636                    let name = format!("Ty{i}");
637                    let new_ty = self
638                        .the_only_binder_mut()
639                        .params
640                        .types
641                        .push_with(|index| TypeParam { index, name });
642                    // Moving that type under two levels of binders: the `DynPredicate` binder and the
643                    // type constraint binder.
644                    let new_ty =
645                        TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::new(2), new_ty)).into_ty();
646                    ty_constraint.skip_binder.ty = new_ty;
647                }
648                TyKind::DynTrait(dyn_pred).into_ty()
649            };
650
651            // Replace any use of `Self` with `dyn Trait<...>`, and remove the `Self` type variable
652            // from the generic parameters.
653            generics = self.into_generics();
654            {
655                dyn_self = dynify(dyn_self, None, false);
656                generics = dynify(generics, Some(dyn_self.clone()), false);
657                kind = dynify(kind, Some(dyn_self.clone()), true);
658                generics.types.remove_and_shift_ids(TypeVarId::ZERO);
659                generics.types.iter_mut().for_each(|ty| {
660                    ty.index -= 1;
661                });
662            }
663
664            dyn_self
665                .kind()
666                .as_dyn_trait()
667                .expect("incorrect `dyn_self`")
668                .clone()
669        };
670        Ok(TypeDecl {
671            def_id: type_id,
672            item_meta: item_meta,
673            generics: generics,
674            src: ItemSource::VTableTy {
675                dyn_predicate: dyn_predicate,
676                field_map,
677                supertrait_map,
678            },
679            kind,
680            layout,
681            // A vtable struct is always sized
682            ptr_metadata: PtrMetadata::None,
683            repr: None,
684        })
685    }
686}
687
688//// Generate a vtable value.
689impl ItemTransCtx<'_, '_> {
690    /// Construct a constant that represents a reference to the vtable corresponding to this this trait proof.
691    pub fn translate_vtable_instance_const(
692        &mut self,
693        span: Span,
694        impl_expr: &hax::ImplExpr,
695    ) -> Result<Box<ConstantExpr>, Error> {
696        let tref = impl_expr.r#trait.hax_skip_binder_ref();
697        if !self.trait_is_dyn_compatible(&tref.def_id)? {
698            raise_error!(
699                self,
700                span,
701                "Trait {:?} should be dyn-compatible",
702                tref.def_id
703            );
704        }
705
706        let vtbl_ty = {
707            let vtbl_ty = self.translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
708                ctx.translate_vtable_struct_ref(span, tref)
709            })?;
710            let vtbl_ty = self.erase_region_binder(vtbl_ty);
711            TyKind::Adt(vtbl_ty).into_ty()
712        };
713        let ty = TyKind::Ref(Region::Static, vtbl_ty.clone(), RefKind::Shared).into_ty();
714
715        let kind = {
716            if let hax::ImplExprAtom::Concrete(impl_item) = &impl_expr.r#impl {
717                // We could return `VTableRef` but we need to enqueue the translation of the static
718                // so may as well reuse that to normalize a bit.
719                let vtable_instance =
720                    self.translate_region_binder(span, &impl_expr.r#trait, |ctx, tref| {
721                        ctx.translate_vtable_instance_ref(span, tref, impl_item)
722                    })?;
723                let vtable_instance = self.erase_region_binder(vtable_instance);
724                let vtable_instance = Box::new(ConstantExpr {
725                    kind: ConstantExprKind::Global(vtable_instance),
726                    ty: vtbl_ty,
727                });
728                ConstantExprKind::Ref(vtable_instance, None)
729            } else {
730                ConstantExprKind::VTableRef(self.translate_trait_impl_expr(span, impl_expr)?)
731            }
732        };
733
734        Ok(Box::new(ConstantExpr { kind, ty }))
735    }
736
737    /// You may want `translate_vtable_instance_const` instead.
738    pub fn translate_vtable_instance_ref(
739        &mut self,
740        span: Span,
741        trait_ref: &hax::TraitRef,
742        impl_ref: &hax::ItemRef,
743    ) -> Result<GlobalDeclRef, Error> {
744        Ok(self
745            .translate_vtable_instance_ref_maybe_enqueue(true, span, trait_ref, impl_ref)?
746            .expect("trait should be dyn-compatible"))
747    }
748
749    pub fn translate_vtable_instance_ref_no_enqueue(
750        &mut self,
751        span: Span,
752        trait_ref: &hax::TraitRef,
753        impl_ref: &hax::ItemRef,
754    ) -> Result<Option<GlobalDeclRef>, Error> {
755        self.translate_vtable_instance_ref_maybe_enqueue(false, span, trait_ref, impl_ref)
756    }
757
758    pub fn translate_vtable_instance_ref_maybe_enqueue(
759        &mut self,
760        enqueue: bool,
761        span: Span,
762        trait_ref: &hax::TraitRef,
763        impl_ref: &hax::ItemRef,
764    ) -> Result<Option<GlobalDeclRef>, Error> {
765        if !self.trait_is_dyn_compatible(&trait_ref.def_id)? {
766            return Ok(None);
767        }
768        // Don't enqueue the vtable for translation by default. It will be enqueued if used in a
769        // `dyn Trait` coercion.
770        // TODO(dyn): To do this properly we'd need to know for each clause whether it ultimately
771        // ends up used in a vtable cast.
772        let vtable_ref: GlobalDeclRef = self.translate_item_maybe_enqueue(
773            span,
774            enqueue,
775            impl_ref,
776            TransItemSourceKind::VTableInstance(TraitImplSource::Normal),
777        )?;
778        Ok(Some(vtable_ref))
779    }
780
781    /// Local helper function to get the vtable struct reference and trait declaration reference
782    fn get_vtable_instance_info<'a>(
783        &mut self,
784        span: Span,
785        impl_def: &'a hax::FullDef,
786        impl_kind: &TraitImplSource,
787    ) -> Result<(Option<TraitImplRef>, TypeDeclRef), Error> {
788        let implemented_trait = match impl_def.kind() {
789            hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref,
790            _ => unreachable!(),
791        };
792        let vtable_struct_ref = self.translate_vtable_struct_ref(span, implemented_trait)?;
793        if self.monomorphize() {
794            return Ok((None, vtable_struct_ref));
795        }
796        let impl_ref = self.translate_item(
797            span,
798            impl_def.this(),
799            TransItemSourceKind::TraitImpl(*impl_kind),
800        )?;
801        Ok((Some(impl_ref), vtable_struct_ref))
802    }
803
804    /// E.g.,
805    /// ```
806    /// global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
807    ///     size: size_of(Foo),
808    ///     align: align_of(Foo),
809    ///     drop: <Foo as Destruct>::drop_in_place,
810    ///     method_0: <Foo as Trait>::method_0::{shim},
811    ///     method_1: <Foo as Trait>::method_1::{shim},
812    ///     ...
813    ///     super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
814    ///     super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
815    ///     ...
816    /// }
817    /// ```
818    pub(crate) fn translate_vtable_instance(
819        mut self,
820        global_id: GlobalDeclId,
821        item_meta: ItemMeta,
822        impl_def: &hax::FullDef,
823        impl_kind: &TraitImplSource,
824    ) -> Result<GlobalDecl, Error> {
825        let span = item_meta.span;
826
827        let (src, vtable_struct_ref) =
828            match self.get_vtable_instance_info(span, impl_def, impl_kind)? {
829                (Some(impl_ref), vtable_struct_ref) => {
830                    (ItemSource::VTableInstance { impl_ref }, vtable_struct_ref)
831                }
832                (None, vtable_struct_ref) => (ItemSource::VTableInstanceMono, vtable_struct_ref),
833            };
834
835        // In mono mode, register preshims for translation
836        if self.monomorphize() {
837            let trait_pred = match impl_def.kind() {
838                hax::FullDefKind::TraitImpl { trait_pred, .. } => trait_pred,
839                _ => unreachable!(),
840            };
841            let trait_def = self.hax_def(&trait_pred.trait_ref)?;
842            self.register_preshim(span, &trait_def)?;
843        }
844
845        // Initializer function for this global.
846        let init = self.register_item(
847            span,
848            impl_def.this(),
849            TransItemSourceKind::VTableInstanceInitializer(*impl_kind),
850        );
851
852        Ok(GlobalDecl {
853            def_id: global_id,
854            item_meta,
855            generics: self.into_generics(),
856            src,
857            // it should be static to have its own address
858            global_kind: GlobalKind::Static,
859            ty: Ty::new(TyKind::Adt(vtable_struct_ref)),
860            init,
861        })
862    }
863
864    fn add_method_to_vtable_value(
865        &mut self,
866        span: Span,
867        impl_def: &hax::FullDef,
868        item: &hax::ImplAssocItem,
869    ) -> Result<Option<VtableMethodValue>, Error> {
870        // Exit if the item isn't a vtable safe method.
871        let item_def = self.poly_hax_def(&item.decl_def_id)?;
872        let hax::FullDefKind::AssocFn {
873            vtable_sig: Some(_),
874            ..
875        } = item_def.kind()
876        else {
877            return Ok(None);
878        };
879
880        let vtable_value = match &item.value {
881            hax::ImplAssocItemValue::Provided {
882                def_id: item_def_id,
883                ..
884            } => {
885                // The method is vtable safe so it has no generics, hence we can reuse the impl
886                // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`.
887                let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id);
888                let shim_ref =
889                    self.translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)?;
890                // In mono mode, we cannot get real types of shim functions by looking up the ones in `struct vtable`
891                // because they are erased function pointers.
892                // Therefore, below we compute real types that are used for casting.
893                if self.monomorphize() {
894                    // Manually translate region params for dyn trait.
895                    // We create a new binding level by `translate_item_generics`
896                    // and restore the orginal one after computing `method_ty`.
897                    assert!(self.binding_levels.len() == 1);
898                    let orginal_binding = self.binding_levels.pop();
899                    let def = self.poly_hax_def(&item_ref.def_id)?;
900                    self.translate_item_generics(span, &def, &TransItemSourceKind::VTableMethod)?;
901
902                    let name = self.translate_trait_item_name(item.def_id())?;
903
904                    let assoc_fun_def = self.hax_def(&item_ref)?;
905                    let vtable_sig = match assoc_fun_def.kind() {
906                        hax::FullDefKind::AssocFn {
907                            vtable_sig: Some(vtable_sig),
908                            ..
909                        } => vtable_sig.clone(),
910                        _ => unreachable!("MONO: only assoc fun is supported"),
911                    };
912
913                    let signature = self.translate_fun_sig(span, &vtable_sig.value)?;
914                    // Add regions. this is ad-hoc...
915                    let method_ty = Ty::new(TyKind::FnPtr(RegionBinder {
916                        regions: self.outermost_generics().regions.clone(),
917                        skip_binder: signature,
918                    }));
919
920                    // Restore the orignal binding_levels.
921                    self.binding_levels.pop();
922                    if let Some(binding_level) = orginal_binding {
923                        self.binding_levels.push(binding_level);
924                    }
925
926                    VtableMethodValue::Cast((name.to_string(), method_ty, shim_ref))
927                } else {
928                    VtableMethodValue::Const(ConstantExprKind::FnDef(shim_ref))
929                }
930            }
931            hax::ImplAssocItemValue::DefaultedFn { .. } => VtableMethodValue::Const(
932                ConstantExprKind::Opaque("shim for default methods aren't yet supported".into()),
933            ),
934            _ => return Ok(None),
935        };
936
937        Ok(Some(vtable_value))
938    }
939
940    /// Generate the body of the vtable instance function.
941    /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls.
942    /// ```ignore
943    /// let ret@0 : VTable;
944    /// ret@0 = VTable { ... };
945    /// return;
946    /// ```
947    fn gen_vtable_instance_init_body(
948        &mut self,
949        span: Span,
950        impl_def: &hax::FullDef,
951        vtable_struct_ref: TypeDeclRef,
952    ) -> Result<Body, Error> {
953        let hax::FullDefKind::TraitImpl {
954            trait_pred,
955            implied_impl_exprs,
956            items,
957            ..
958        } = impl_def.kind()
959        else {
960            unreachable!()
961        };
962
963        let trait_def = self.hax_def(&trait_pred.trait_ref)?;
964        // We use `poly_trait_def` to fetch `implied_preds`, which is used to fetch supertrait in `prepare_vtable_fields`.
965        let poly_trait_def = self.poly_hax_def(&trait_pred.trait_ref.def_id)?;
966        let hax::FullDefKind::Trait {
967            implied_predicates: implied_preds,
968            ..
969        } = poly_trait_def.kind()
970        else {
971            unreachable!()
972        };
973
974        let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?;
975        // The type this impl is for.
976        let self_ty = &implemented_trait.generics.types[0];
977
978        let mut builder = BodyBuilder::new(span, 0);
979        let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone()));
980        let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone());
981
982        let vtable_data = self.prepare_vtable_fields(&trait_def, implied_preds)?;
983        // Retrieve the expected field types from the struct definition. This avoids complicated
984        // substitutions.
985        let field_tys = {
986            let vtable_decl_id = vtable_struct_ref.id.as_adt().unwrap().clone();
987            let ItemRef::Type(vtable_def) = self.t_ctx.get_or_translate(vtable_decl_id.into())?
988            else {
989                unreachable!()
990            };
991            let fields = match &vtable_def.kind {
992                TypeDeclKind::Struct(fields) => fields,
993                TypeDeclKind::Opaque => return Ok(Body::Opaque),
994                TypeDeclKind::Error(error) => return Err(Error::new(span, error.clone())),
995                _ => unreachable!(),
996            };
997            fields
998                .iter()
999                .map(|f| &f.ty)
1000                .cloned()
1001                .map(|ty| ty.substitute(&vtable_struct_ref.generics))
1002                .collect_vec()
1003        };
1004
1005        // Construct a list with one operand per vtable field.
1006        let mut aggregate_fields = vec![];
1007        let mut items_iter = items.iter();
1008        for (field, ty) in vtable_data.fields.into_iter().zip(field_tys) {
1009            // In poly mode, all fields of vtables can be filled with const values.
1010            let mk_const = |kind| {
1011                Operand::Const(Box::new(ConstantExpr {
1012                    kind,
1013                    ty: ty.clone(),
1014                }))
1015            };
1016            // In mono mode, we need to additioanlly cast shim function pointers to opaque ones before filling them.
1017            // Therefore, `mk_cast` receives `(method_name, method_ty, method_shim)` to construct casting statements.
1018            // For example, for the trait declaration and trait implementation in Rust:
1019            // ```
1020            // trait Trait {
1021            //      fn method(&self);
1022            // }
1023            // impl Trait for i32 {
1024            //      fn method(&self) {}
1025            // }
1026            // ```
1027            //  , `mk_cast` will generate the followging statements inside the vtable initialization function:
1028            // ```
1029            // fn vtable_init() -> vtable {
1030            //      ...
1031            //      let method_local: fn<'_0_1>(&'_0_1 (dyn Trait + '1));
1032            //      let cast_local: *const ();
1033            //
1034            //      method_local = const {shim}<'1>
1035            //      cast_local = cast<fn<'_0_1>(&'_0_1 (dyn Trait + '2)), *const ()>(move method_local)
1036            //      ...
1037            // }
1038            // ```
1039            let mut mk_cast = |(method_name, method_ty, method_shim): (String, Ty, FnPtr)| {
1040                let method_local = builder.new_var(Some(method_name.clone()), method_ty.clone());
1041                let shim = Rvalue::Use(Operand::Const(Box::new(ConstantExpr {
1042                    kind: ConstantExprKind::FnDef(method_shim.clone()),
1043                    ty: method_ty.clone(),
1044                })));
1045                let cast_local = builder.new_var(
1046                    Some("erased_".to_string() + method_name.as_str()),
1047                    ty.clone(),
1048                );
1049                let cast = Rvalue::UnaryOp(
1050                    UnOp::Cast(CastKind::RawPtr(
1051                        method_local.ty().clone(),
1052                        cast_local.ty().clone(),
1053                    )),
1054                    Operand::Move(method_local.clone()),
1055                );
1056
1057                builder.push_statement(StatementKind::Assign(method_local.clone(), shim));
1058                builder.push_statement(StatementKind::Assign(cast_local.clone(), cast));
1059                Operand::Move(cast_local)
1060            };
1061            let op = match field {
1062                TrVTableField::Size => {
1063                    let size_local = builder.new_var(Some("size".to_string()), ty);
1064                    builder.push_statement(StatementKind::Assign(
1065                        size_local.clone(),
1066                        Rvalue::NullaryOp(NullOp::SizeOf, self_ty.clone()),
1067                    ));
1068                    Operand::Move(size_local)
1069                }
1070                TrVTableField::Align => {
1071                    let align_local = builder.new_var(Some("align".to_string()), ty);
1072                    builder.push_statement(StatementKind::Assign(
1073                        align_local.clone(),
1074                        Rvalue::NullaryOp(NullOp::AlignOf, self_ty.clone()),
1075                    ));
1076                    Operand::Move(align_local)
1077                }
1078                TrVTableField::Drop => {
1079                    let drop_shim = self.translate_item(
1080                        span,
1081                        impl_def.this(),
1082                        TransItemSourceKind::VTableDropShim,
1083                    )?;
1084                    if self.monomorphize() {
1085                        // manually compute the type of drop shim function.
1086                        let hax::FullDefKind::Trait { dyn_self, .. } = trait_def.kind() else {
1087                            panic!()
1088                        };
1089
1090                        let Some(dyn_self) = dyn_self else {
1091                            panic!(
1092                                "MONO: Trying to generate a vtable for a non-dyn-compatible trait"
1093                            )
1094                        };
1095                        let ref_dyn_self =
1096                            TyKind::RawPtr(self.translate_ty(span, dyn_self)?, RefKind::Mut)
1097                                .into_ty();
1098                        let signature = FunSig {
1099                            is_unsafe: true,
1100                            inputs: vec![ref_dyn_self.clone()],
1101                            output: Ty::mk_unit(),
1102                        };
1103                        let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(signature)));
1104
1105                        mk_cast(("drop".to_string(), drop_ty.clone(), drop_shim))
1106                    } else {
1107                        mk_const(ConstantExprKind::FnDef(drop_shim))
1108                    }
1109                }
1110                TrVTableField::Method(..) => 'a: {
1111                    // Bit of a hack: we know the methods are in the right order. This is easier
1112                    // than trying to index into the items list by name.
1113                    for item in items_iter.by_ref() {
1114                        if let Some(kind) = self.add_method_to_vtable_value(span, impl_def, item)? {
1115                            match kind {
1116                                VtableMethodValue::Const(const_kind) => {
1117                                    break 'a mk_const(const_kind);
1118                                }
1119                                VtableMethodValue::Cast(method) => break 'a mk_cast(method),
1120                            }
1121                        }
1122                    }
1123                    unreachable!()
1124                }
1125                TrVTableField::SuperTrait(clause_id, _) => {
1126                    let impl_expr = &implied_impl_exprs[clause_id.index()];
1127                    let vtable = self.translate_vtable_instance_const(span, impl_expr)?;
1128                    Operand::Const(vtable)
1129                }
1130            };
1131            aggregate_fields.push(op);
1132        }
1133
1134        // Construct the final struct.
1135        builder.push_statement(StatementKind::Assign(
1136            ret_place,
1137            Rvalue::Aggregate(
1138                AggregateKind::Adt(vtable_struct_ref.clone(), None, None),
1139                aggregate_fields,
1140            ),
1141        ));
1142
1143        Ok(Body::Unstructured(builder.build()))
1144    }
1145
1146    pub(crate) fn translate_vtable_instance_init(
1147        mut self,
1148        init_func_id: FunDeclId,
1149        item_meta: ItemMeta,
1150        impl_def: &hax::FullDef,
1151        impl_kind: &TraitImplSource,
1152    ) -> Result<FunDecl, Error> {
1153        let span = item_meta.span;
1154
1155        let (src, vtable_struct_ref) =
1156            match self.get_vtable_instance_info(span, impl_def, impl_kind)? {
1157                (Some(impl_ref), vtable_struct_ref) => {
1158                    (ItemSource::VTableInstance { impl_ref }, vtable_struct_ref)
1159                }
1160                (None, vtable_struct_ref) => (ItemSource::VTableInstanceMono, vtable_struct_ref),
1161            };
1162
1163        let init_for = self.register_item(
1164            span,
1165            impl_def.this(),
1166            TransItemSourceKind::VTableInstance(*impl_kind),
1167        );
1168
1169        // Signature: `() -> VTable`.
1170        let sig = FunSig {
1171            is_unsafe: false,
1172            inputs: vec![],
1173            output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())),
1174        };
1175
1176        let body = match impl_kind {
1177            _ if item_meta.opacity.with_private_contents().is_opaque() => Body::Opaque,
1178            TraitImplSource::Normal => {
1179                self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)?
1180            }
1181            _ => {
1182                raise_error!(
1183                    self,
1184                    span,
1185                    "Don't know how to generate a vtable for a virtual impl {impl_kind:?}"
1186                );
1187            }
1188        };
1189
1190        Ok(FunDecl {
1191            def_id: init_func_id,
1192            item_meta: item_meta,
1193            generics: self.into_generics(),
1194            signature: sig,
1195            src,
1196            is_global_initializer: Some(init_for),
1197            body,
1198        })
1199    }
1200
1201    /// The target vtable shim body looks like:
1202    /// ```ignore
1203    /// local ret@0 : ReturnTy;
1204    /// // the shim receiver of this shim function
1205    /// local shim_self@1 : ShimReceiverTy;
1206    /// // the arguments of the impl function
1207    /// local arg1@2 : Arg1Ty;
1208    /// ...
1209    /// local argN@N : ArgNTy;
1210    /// // the target receiver of the impl function
1211    /// local target_self@(N+1) : TargetReceiverTy;
1212    /// // perform some conversion to cast / re-box the shim receiver to the target receiver
1213    /// ...
1214    /// target_self@(N+1) := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
1215    /// // call the impl function and assign the result to ret@0
1216    /// ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N);
1217    /// ```
1218    fn translate_vtable_shim_body(
1219        &mut self,
1220        span: Span,
1221        target_receiver: &Ty,
1222        shim_signature: &FunSig,
1223        impl_func_def: &hax::FullDef,
1224    ) -> Result<Body, Error> {
1225        let mut builder = BodyBuilder::new(span, shim_signature.inputs.len());
1226
1227        let ret_place = builder.new_var(None, shim_signature.output.clone());
1228        let mut method_args = shim_signature
1229            .inputs
1230            .iter()
1231            .map(|ty| builder.new_var(None, ty.clone()))
1232            .collect_vec();
1233        let target_self = builder.new_var(None, target_receiver.clone());
1234
1235        // Replace the `dyn Trait` receiver with the concrete one.
1236        let shim_self = mem::replace(&mut method_args[0], target_self.clone());
1237
1238        // Perform the core concretization cast.
1239        // FIXME: need to unpack & re-pack the structure for cases like `Rc`, `Arc`, `Pin` and
1240        // (when --raw-boxes is on) `Box`
1241        let rval = Rvalue::UnaryOp(
1242            UnOp::Cast(CastKind::Concretize(
1243                shim_self.ty().clone(),
1244                target_self.ty().clone(),
1245            )),
1246            Operand::Move(shim_self.clone()),
1247        );
1248        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
1249
1250        let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun);
1251        let generics = self.outermost_binder().params.identity_args();
1252        builder.call(Call {
1253            func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)),
1254            args: method_args
1255                .into_iter()
1256                .map(|arg| Operand::Move(arg))
1257                .collect(),
1258            dest: ret_place,
1259        });
1260
1261        Ok(Body::Unstructured(builder.build()))
1262    }
1263
1264    /// The target vtable drop_shim body looks like:
1265    /// ```ignore
1266    /// local ret@0 : ();
1267    /// // the shim receiver of this drop_shim function
1268    /// local shim_self@1 : ShimReceiverTy;
1269    /// // the target receiver of the drop_shim
1270    /// local target_self@2 : TargetReceiverTy;
1271    /// // perform some conversion to cast / re-box the drop_shim receiver to the target receiver
1272    /// target_self@2 := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
1273    /// Drop(*target_self@2);
1274    /// ```
1275    fn translate_vtable_drop_shim_body(
1276        &mut self,
1277        span: Span,
1278        shim_receiver: &Ty,
1279        target_receiver: &Ty,
1280        trait_pred: &TraitPredicate,
1281    ) -> Result<Body, Error> {
1282        let mut builder = BodyBuilder::new(span, 1);
1283
1284        builder.new_var(Some("ret".into()), Ty::mk_unit());
1285        let dyn_self = builder.new_var(Some("dyn_self".into()), shim_receiver.clone());
1286        let target_self = builder.new_var(Some("target_self".into()), target_receiver.clone());
1287
1288        // Perform the core concretization cast.
1289        let rval = Rvalue::UnaryOp(
1290            UnOp::Cast(CastKind::Concretize(
1291                dyn_self.ty().clone(),
1292                target_self.ty().clone(),
1293            )),
1294            Operand::Move(dyn_self.clone()),
1295        );
1296        builder.push_statement(StatementKind::Assign(target_self.clone(), rval));
1297
1298        // Build a reference to `impl Destruct for T`. Given the
1299        // target_receiver type `T`, use Hax to solve `T: Destruct`
1300        // and translate the resolved result to `TraitRef` of the
1301        // `drop_in_place`
1302        let destruct_trait = self.tcx.lang_items().destruct_trait().unwrap();
1303        let impl_expr: hax::ImplExpr = {
1304            let s = self.hax_state_with_id();
1305            let rustc_trait_args = trait_pred.trait_ref.rustc_args(s);
1306            let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type
1307            let tref =
1308                rustc_middle::ty::TraitRef::new_from_args(self.tcx, destruct_trait, generics);
1309            hax::solve_trait(s, rustc_middle::ty::Binder::dummy(tref))
1310        };
1311        let tref = self.translate_trait_impl_expr(span, &impl_expr)?;
1312
1313        // Drop(*target_self)
1314        let drop_arg = target_self.clone().deref();
1315        builder.insert_drop(drop_arg, tref);
1316
1317        Ok(Body::Unstructured(builder.build()))
1318    }
1319
1320    pub(crate) fn translate_vtable_drop_shim(
1321        mut self,
1322        fun_id: FunDeclId,
1323        item_meta: ItemMeta,
1324        impl_def: &hax::FullDef,
1325    ) -> Result<FunDecl, Error> {
1326        let span = item_meta.span;
1327
1328        let hax::FullDefKind::TraitImpl {
1329            dyn_self: Some(dyn_self),
1330            trait_pred,
1331            ..
1332        } = impl_def.kind()
1333        else {
1334            raise_error!(
1335                self,
1336                span,
1337                "Trying to generate a vtable drop shim for a non-trait impl"
1338            );
1339        };
1340
1341        // `*mut dyn Trait`
1342        let ref_dyn_self =
1343            TyKind::RawPtr(self.translate_ty(span, dyn_self)?, RefKind::Mut).into_ty();
1344        // `*mut T` for `impl Trait for T`
1345        let ref_target_self = {
1346            let impl_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
1347            TyKind::RawPtr(impl_trait.generics.types[0].clone(), RefKind::Mut).into_ty()
1348        };
1349
1350        // `*mut dyn Trait -> ()`
1351        let signature = FunSig {
1352            is_unsafe: true,
1353            inputs: vec![ref_dyn_self.clone()],
1354            output: Ty::mk_unit(),
1355        };
1356
1357        let body: Body = self.translate_vtable_drop_shim_body(
1358            span,
1359            &ref_dyn_self,
1360            &ref_target_self,
1361            trait_pred,
1362        )?;
1363
1364        Ok(FunDecl {
1365            def_id: fun_id,
1366            item_meta,
1367            generics: self.into_generics(),
1368            signature,
1369            src: ItemSource::VTableMethodShim,
1370            is_global_initializer: None,
1371            body,
1372        })
1373    }
1374
1375    pub(crate) fn translate_vtable_shim(
1376        mut self,
1377        fun_id: FunDeclId,
1378        item_meta: ItemMeta,
1379        impl_func_def: &hax::FullDef,
1380    ) -> Result<FunDecl, Error> {
1381        let span = item_meta.span;
1382
1383        let hax::FullDefKind::AssocFn {
1384            vtable_sig: Some(vtable_sig),
1385            sig: target_signature,
1386            ..
1387        } = impl_func_def.kind()
1388        else {
1389            raise_error!(
1390                self,
1391                span,
1392                "Trying to generate a vtable shim for a non-vtable-safe method"
1393            );
1394        };
1395
1396        // The signature of the shim function.
1397        let signature = self.translate_fun_sig(span, &vtable_sig.value)?;
1398        // The concrete receiver we will cast to.
1399        let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?;
1400
1401        trace!(
1402            "[VtableShim] Obtained dyn signature with receiver type: {}",
1403            signature.inputs[0].with_ctx(&self.into_fmt())
1404        );
1405
1406        let body = if item_meta.opacity.with_private_contents().is_opaque() {
1407            Body::Opaque
1408        } else {
1409            self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?
1410        };
1411
1412        Ok(FunDecl {
1413            def_id: fun_id,
1414            item_meta,
1415            generics: self.into_generics(),
1416            signature,
1417            src: ItemSource::VTableMethodShim,
1418            is_global_initializer: None,
1419            body,
1420        })
1421    }
1422
1423    // In mono mode, method (or drop) preshim functions are used for dynamic trait calls.
1424    // It does two things:
1425    // 1. It converts opaque shim functions stored in the vtable back into shim functions with dyn trait types
1426    // 2. It calls the converted shim function, passing the dyn trait object.
1427    #[tracing::instrument(skip(self, item_meta))]
1428    pub(crate) fn translate_vtable_method_preshim(
1429        mut self,
1430        fun_id: FunDeclId,
1431        item_meta: ItemMeta,
1432        trait_def: &hax::FullDef,
1433        name: &TraitItemName,
1434        trait_id: &TraitDeclId,
1435    ) -> Result<FunDecl, Error> {
1436        let span = item_meta.span;
1437
1438        let mut assoc_func_def = None;
1439        let mut assoc_types = None;
1440
1441        if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() {
1442            for item in items {
1443                let item_def_id = &item.def_id;
1444                // This is ok because dyn-compatible methods don't have generics.
1445                let item_def =
1446                    self.hax_def(&trait_def.this().with_def_id(self.hax_state(), item_def_id))?;
1447                if let hax::FullDefKind::AssocFn {
1448                    // sig,
1449                    // vtable_sig: Some(_),
1450                    ..
1451                } = item_def.kind()
1452                {
1453                    let fun_name = self.translate_trait_item_name(&item_def_id)?;
1454                    if fun_name == *name {
1455                        assoc_func_def = Some(item_def);
1456                    }
1457                }
1458                else if let hax::FullDefKind::AssocTy {
1459                    implied_predicates, ..}
1460                    = item_def.kind() {
1461                    trace!("MONO: show:\n {:?}", item_def.kind());
1462                    if let Some(pred) = implied_predicates.predicates.first() {
1463                        if let hax::ClauseKind::Trait(p) = &pred.clause.kind.value {
1464                            assoc_types = Some(p.trait_ref.generic_args.clone());
1465                        }
1466                    }
1467                }
1468            }
1469        }
1470
1471        let Some(assoc_func_def) = assoc_func_def else {
1472            panic!("MONO: assoc_func_def is not found");
1473        };
1474
1475        // manually translate region params for dyn trait
1476        assert!(self.binding_levels.len() == 1);
1477        self.binding_levels.pop();
1478        let def = self.poly_hax_def(&assoc_func_def.def_id())?;
1479        self.translate_item_generics(span, &def, &TransItemSourceKind::VTableMethod)?;
1480
1481        let hax::FullDefKind::AssocFn {
1482            vtable_sig: Some(vtable_sig),
1483            // sig: sig,
1484            associated_item,
1485            ..
1486        } = assoc_func_def.kind()
1487        else {
1488            raise_error!(self, span, "MONO: expected associative methods");
1489        };
1490
1491        let AssocItemContainer::TraitContainer {
1492            trait_ref: tref, ..
1493        } = &associated_item.container
1494        else {
1495            raise_error!(
1496                self,
1497                span,
1498                "MONO: expected trait ref of associative methods"
1499            );
1500        };
1501
1502        let trait_def = self.poly_hax_def(&tref.def_id)?;
1503
1504        // The signature of the shim function.
1505        let signature = self.translate_fun_sig(span, &vtable_sig.value)?;
1506
1507        // Add regions. this is ad-hoc...
1508        let method_ty = Ty::new(TyKind::FnPtr(RegionBinder {
1509            regions: self.outermost_generics().regions.clone(),
1510            skip_binder: signature.clone(),
1511        }));
1512
1513        let body: Body = self.translate_vtable_method_preshim_body(
1514            span,
1515            &signature.inputs[0],
1516            &method_ty,
1517            &trait_def,
1518            format!("method_{}", name.to_string()).as_str(),
1519        )?;
1520
1521        let mut types = vec![];
1522        let generic_args = tref.generic_args.clone();
1523        for arg in generic_args.iter().skip(1) {
1524            if let GenericArg::Type(hax_ty) = arg {
1525                types.push(self.translate_ty(span, hax_ty)?);
1526            }
1527        }
1528        if let Some(assoc_types) = assoc_types {
1529            for arg in assoc_types.iter() {
1530                if let GenericArg::Type(hax_ty) = arg {
1531                    types.push(self.translate_ty(span, hax_ty)?);
1532                }
1533            }
1534        }
1535
1536        Ok(FunDecl {
1537            def_id: fun_id,
1538            item_meta,
1539            // only keep regions
1540            generics: GenericParams {
1541                regions: self.into_generics().regions,
1542                ..GenericParams::empty()
1543            },
1544            signature: signature,
1545            src: ItemSource::VTableMethodPreShim(*trait_id, *name, types),
1546            is_global_initializer: None,
1547            body,
1548        })
1549    }
1550
1551    fn translate_vtable_method_preshim_body(
1552        &mut self,
1553        span: Span,
1554        shim_receiver: &Ty,
1555        drop_ty: &Ty,
1556        trait_def: &hax::FullDef,
1557        name: &str,
1558    ) -> Result<Body, Error> {
1559        let mut builder = BodyBuilder::new(span, 1);
1560
1561        let ret_var = builder.new_var(Some("ret".into()), Ty::mk_unit());
1562        let dyn_self = builder.new_var(Some("dyn_self".into()), shim_receiver.clone());
1563
1564        let erased_ptr_ty = Ty::new(TyKind::RawPtr(Ty::mk_unit(), RefKind::Shared));
1565        let erased_drop_shim_ptr = builder.new_var(
1566            Some(format!("erased_{}_shim_ptr", name).into()),
1567            erased_ptr_ty.clone(),
1568        );
1569        let drop_shim_ptr =
1570            builder.new_var(Some(format!("{}_shim_ptr", name).into()), drop_ty.clone());
1571        // let target_self = builder.new_var(Some("target_self".into()), target_receiver.clone());
1572
1573        // Construct the `(*ptr.ptr_metadata).method_field` place.
1574        let vtable_decl_ref = self.translate_vtable_struct_ref(span, trait_def.this())?;
1575        let vtable_decl_id = *vtable_decl_ref.id.as_adt().unwrap();
1576        let vtable_ty = TyKind::Adt(vtable_decl_ref).into_ty();
1577        let ptr_to_vtable_ty = Ty::new(TyKind::RawPtr(vtable_ty.clone(), RefKind::Shared));
1578
1579        let Some(vtable_decl) = self.t_ctx.translated.type_decls.get(vtable_decl_id) else {
1580            // error!("MONO: vtable_decl not found");
1581            panic!("MONO: vtable_decl not found");
1582        };
1583        // Retreive the method field from the vtable struct definition.
1584        let method_field_name = name;
1585        let Some((method_field_id, _)) = vtable_decl.get_field_by_name(None, &method_field_name)
1586        else {
1587            panic!(
1588                "Could not determine method index for {} in vtable",
1589                method_field_name
1590            );
1591        };
1592
1593        // Construct the `(*ptr.ptr_metadata).method_field` place.
1594        let drop_field_place = dyn_self
1595            .clone()
1596            .project(ProjectionElem::PtrMetadata, ptr_to_vtable_ty)
1597            .project(ProjectionElem::Deref, vtable_ty)
1598            .project(
1599                ProjectionElem::Field(FieldProjKind::Adt(vtable_decl_id, None), method_field_id),
1600                erased_ptr_ty.clone(),
1601            );
1602
1603        let drop_rval = Rvalue::Use(Operand::Copy(drop_field_place));
1604        builder.push_statement(StatementKind::Assign(
1605            erased_drop_shim_ptr.clone(),
1606            drop_rval,
1607        ));
1608
1609        // Perform the core concretization cast.
1610        let rval_cast = Rvalue::UnaryOp(
1611            UnOp::Cast(CastKind::RawPtr(
1612                erased_drop_shim_ptr.ty().clone(),
1613                drop_shim_ptr.ty().clone(),
1614            )),
1615            Operand::Move(erased_drop_shim_ptr.clone()),
1616        );
1617
1618        builder.push_statement(StatementKind::Assign(drop_shim_ptr.clone(), rval_cast));
1619
1620        builder.call(Call {
1621            func: FnOperand::Dynamic(Operand::Move(drop_shim_ptr)),
1622            args: vec![Operand::Move(dyn_self)],
1623            dest: ret_var,
1624        });
1625
1626        Ok(Body::Unstructured(builder.build()))
1627    }
1628
1629    pub(crate) fn translate_vtable_drop_preshim(
1630        mut self,
1631        fun_id: FunDeclId,
1632        item_meta: ItemMeta,
1633        trait_def: &hax::FullDef,
1634    ) -> Result<FunDecl, Error> {
1635        let span = item_meta.span;
1636
1637        let hax::FullDefKind::Trait { dyn_self, .. } = trait_def.kind() else {
1638            raise_error!(self, span, "MONO: Unsupported trait");
1639        };
1640        let Some(dyn_self) = dyn_self else {
1641            panic!("Trying to generate a vtable for a non-dyn-compatible trait")
1642        };
1643
1644        // `*mut dyn Trait`
1645        let ref_dyn_self =
1646            TyKind::RawPtr(self.translate_ty(span, dyn_self)?, RefKind::Mut).into_ty();
1647
1648        // `*mut dyn Trait -> ()`
1649        let signature = FunSig {
1650            is_unsafe: true,
1651            inputs: vec![ref_dyn_self.clone()],
1652            output: Ty::mk_unit(),
1653        };
1654
1655        let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(signature.clone())));
1656
1657        let body: Body = self.translate_vtable_drop_preshim_body(
1658            span,
1659            &ref_dyn_self,
1660            &drop_ty,
1661            trait_def,
1662            // &ref_target_self,
1663        )?;
1664
1665        Ok(FunDecl {
1666            def_id: fun_id,
1667            item_meta,
1668            // generics: self.into_generics(),
1669            generics: GenericParams::empty(),
1670            signature,
1671            src: ItemSource::VTableMethodShim,
1672            is_global_initializer: None,
1673            body,
1674        })
1675    }
1676
1677    fn translate_vtable_drop_preshim_body(
1678        &mut self,
1679        span: Span,
1680        shim_receiver: &Ty,
1681        drop_ty: &Ty,
1682        trait_def: &hax::FullDef,
1683    ) -> Result<Body, Error> {
1684        let mut builder = BodyBuilder::new(span, 1);
1685
1686        let ret_var = builder.new_var(Some("ret".into()), Ty::mk_unit());
1687        let dyn_self = builder.new_var(Some("dyn_self".into()), shim_receiver.clone());
1688
1689        let erased_ptr_ty = Ty::new(TyKind::RawPtr(Ty::mk_unit(), RefKind::Shared));
1690        let erased_drop_shim_ptr =
1691            builder.new_var(Some("erased_drop_shim_ptr".into()), erased_ptr_ty.clone());
1692        let drop_shim_ptr = builder.new_var(Some("drop_shim_ptr".into()), drop_ty.clone());
1693        // let target_self = builder.new_var(Some("target_self".into()), target_receiver.clone());
1694
1695        // Construct the `(*ptr.ptr_metadata).method_field` place.
1696        let vtable_decl_ref = self.translate_vtable_struct_ref(span, trait_def.this())?;
1697        let vtable_decl_id = *vtable_decl_ref.id.as_adt().unwrap();
1698        let vtable_ty = TyKind::Adt(vtable_decl_ref).into_ty();
1699        let ptr_to_vtable_ty = Ty::new(TyKind::RawPtr(vtable_ty.clone(), RefKind::Shared));
1700
1701        let Some(vtable_decl) = self.t_ctx.translated.type_decls.get(vtable_decl_id) else {
1702            // error!("MONO: vtable_decl not found");
1703            panic!("MONO: vtable_decl not found");
1704        };
1705        // Retreive the method field from the vtable struct definition.
1706        let method_field_name = format!("drop");
1707        let Some((method_field_id, _)) = vtable_decl.get_field_by_name(None, &method_field_name)
1708        else {
1709            panic!(
1710                "Could not determine method index for {} in vtable",
1711                method_field_name
1712            );
1713        };
1714
1715        // Construct the `(*ptr.ptr_metadata).drop_field` place.
1716        let drop_field_place = dyn_self
1717            .clone()
1718            .project(ProjectionElem::PtrMetadata, ptr_to_vtable_ty)
1719            .project(ProjectionElem::Deref, vtable_ty)
1720            .project(
1721                ProjectionElem::Field(FieldProjKind::Adt(vtable_decl_id, None), method_field_id),
1722                erased_ptr_ty.clone(),
1723            );
1724
1725        let drop_rval = Rvalue::Use(Operand::Copy(drop_field_place));
1726        builder.push_statement(StatementKind::Assign(
1727            erased_drop_shim_ptr.clone(),
1728            drop_rval,
1729        ));
1730
1731        // Perform the core concretization cast.
1732        let rval_cast = Rvalue::UnaryOp(
1733            UnOp::Cast(CastKind::RawPtr(
1734                erased_drop_shim_ptr.ty().clone(),
1735                drop_shim_ptr.ty().clone(),
1736            )),
1737            Operand::Move(erased_drop_shim_ptr.clone()),
1738        );
1739
1740        builder.push_statement(StatementKind::Assign(drop_shim_ptr.clone(), rval_cast));
1741
1742        builder.call(Call {
1743            func: FnOperand::Dynamic(Operand::Move(drop_shim_ptr)),
1744            args: vec![Operand::Move(dyn_self)],
1745            dest: ret_var,
1746        });
1747
1748        Ok(Body::Unstructured(builder.build()))
1749    }
1750}
charon_driver/translate/translate_trait_objects.rs

charon_driver/translate/
translate_trait_objects.rs
