charon_driver/translate/
translate_trait_objects.rs

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

charon_driver/translate/
translate_trait_objects.rs
