charon_driver/translate/
translate_items.rs

1use super::translate_crate::*;
2use super::translate_ctx::*;
3use crate::hax;
4use crate::hax::SInto;
5use charon_lib::ast::*;
6use charon_lib::formatter::IntoFormatter;
7use charon_lib::pretty::FmtWithCtx;
8use derive_generic_visitor::Visitor;
9use itertools::Itertools;
10use rustc_span::sym;
11use std::mem;
12use std::ops::ControlFlow;
13
14impl<'tcx> TranslateCtx<'tcx> {
15    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
16        let trans_id = self.register_no_enqueue(&None, item_src);
17        let def_id = item_src.def_id();
18        if let Some(trans_id) = trans_id {
19            if self.translate_stack.contains(&trans_id) {
20                register_error!(
21                    self,
22                    Span::dummy(),
23                    "Cycle detected while translating {def_id:?}! Stack: {:?}",
24                    &self.translate_stack
25                );
26                return;
27            } else {
28                self.translate_stack.push(trans_id);
29            }
30        }
31        self.with_def_id(def_id, trans_id, |mut ctx| {
32            let span = ctx.def_span(def_id);
33            // Catch cycles
34            let res = {
35                // Stopgap measure because there are still many panics in charon and hax.
36                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
37                std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
38            };
39            match res {
40                Ok(Ok(())) => return,
41                // Translation error
42                Ok(Err(_)) => {
43                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
44                }
45                // Panic
46                Err(_) => register_error!(
47                    ctx,
48                    span,
49                    "Thread panicked when extracting item `{def_id:?}`."
50                ),
51            };
52        });
53        // We must be careful not to early-return from this function to not unbalance the stack.
54        self.translate_stack.pop();
55    }
56
57    pub(crate) fn translate_item_aux(
58        &mut self,
59        item_src: &TransItemSource,
60        trans_id: Option<ItemId>,
61    ) -> Result<(), Error> {
62        // Translate the meta information
63        let name = self.translate_name(item_src)?;
64        if let Some(trans_id) = trans_id {
65            self.translated.item_names.insert(trans_id, name.clone());
66        }
67        let opacity = self.opacity_for_name(&name);
68        if opacity.is_invisible() {
69            // Don't even start translating the item. In particular don't call `hax_def` on it.
70            return Ok(());
71        }
72        let def = self.hax_def_for_item(&item_src.item)?;
73        let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
74        if item_meta.opacity.is_invisible() {
75            return Ok(());
76        }
77
78        // For items in the current crate that have bodies, also enqueue items defined in that
79        // body.
80        if !item_meta.opacity.is_opaque()
81            && let Some(def_id) = def.def_id().as_rust_def_id()
82            && let Some(ldid) = def_id.as_local()
83            && let node = self.tcx.hir_node_by_def_id(ldid)
84            && let Some(body_id) = node.body_id()
85        {
86            use rustc_hir::intravisit;
87            #[allow(non_local_definitions)]
88            impl<'tcx> intravisit::Visitor<'tcx> for TranslateCtx<'tcx> {
89                fn visit_nested_item(&mut self, id: rustc_hir::ItemId) {
90                    let def_id = id.owner_id.def_id.to_def_id();
91                    let def_id = def_id.sinto(&self.hax_state);
92                    self.enqueue_module_item(&def_id);
93                }
94            }
95            let body = self.tcx.hir_body(body_id);
96            intravisit::walk_body(self, body);
97        }
98
99        // Initialize the item translation context
100        let mut bt_ctx = ItemTransCtx::new(item_src.clone(), trans_id, self);
101        trace!(
102            "About to translate item `{:?}` as a {:?}; \
103            target_id={trans_id:?}, mono={}",
104            def.def_id(),
105            item_src.kind,
106            bt_ctx.monomorphize(),
107        );
108        if !matches!(
109            &item_src.kind,
110            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module,
111        ) {
112            bt_ctx.translate_item_generics(item_meta.span, &def, &item_src.kind)?;
113        }
114        match &item_src.kind {
115            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module => {
116                bt_ctx.register_module(item_meta, &def);
117            }
118            TransItemSourceKind::Type => {
119                let Some(ItemId::Type(id)) = trans_id else {
120                    unreachable!()
121                };
122                let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
123                self.translated.type_decls.set_slot(id, ty);
124            }
125            TransItemSourceKind::Fun => {
126                let Some(ItemId::Fun(id)) = trans_id else {
127                    unreachable!()
128                };
129                let fun_decl = bt_ctx.translate_fun_decl(id, item_meta, &def)?;
130                self.translated.fun_decls.set_slot(id, fun_decl);
131            }
132            TransItemSourceKind::Global => {
133                let Some(ItemId::Global(id)) = trans_id else {
134                    unreachable!()
135                };
136                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
137                self.translated.global_decls.set_slot(id, global_decl);
138            }
139            TransItemSourceKind::TraitDecl => {
140                let Some(ItemId::TraitDecl(id)) = trans_id else {
141                    unreachable!()
142                };
143                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
144                self.translated.trait_decls.set_slot(id, trait_decl);
145            }
146            TransItemSourceKind::TraitImpl(kind) => {
147                let Some(ItemId::TraitImpl(id)) = trans_id else {
148                    unreachable!()
149                };
150                // In Mono mode, only user-defined trait is supported for now.
151                let trait_impl = match kind {
152                    TraitImplSource::Normal => bt_ctx.translate_trait_impl(id, item_meta, &def)?,
153                    TraitImplSource::TraitAlias => {
154                        bt_ctx.translate_trait_alias_blanket_impl(id, item_meta, &def)?
155                    }
156                    &TraitImplSource::Closure(kind) => {
157                        bt_ctx.translate_closure_trait_impl(id, item_meta, &def, kind)?
158                    }
159                    TraitImplSource::ImplicitDestruct => {
160                        bt_ctx.translate_implicit_destruct_impl(id, item_meta, &def)?
161                    }
162                };
163                self.translated.trait_impls.set_slot(id, trait_impl);
164            }
165            &TransItemSourceKind::DefaultedMethod(impl_kind, _, method_id) => {
166                let Some(ItemId::Fun(id)) = trans_id else {
167                    unreachable!()
168                };
169                let fun_decl =
170                    bt_ctx.translate_defaulted_method(id, item_meta, &def, impl_kind, method_id)?;
171                self.translated.fun_decls.set_slot(id, fun_decl);
172            }
173            &TransItemSourceKind::ClosureMethod(kind) => {
174                let Some(ItemId::Fun(id)) = trans_id else {
175                    unreachable!()
176                };
177                let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, kind)?;
178                self.translated.fun_decls.set_slot(id, fun_decl);
179            }
180            TransItemSourceKind::ClosureAsFnCast => {
181                let Some(ItemId::Fun(id)) = trans_id else {
182                    unreachable!()
183                };
184                let fun_decl = bt_ctx.translate_stateless_closure_as_fn(id, item_meta, &def)?;
185                self.translated.fun_decls.set_slot(id, fun_decl);
186            }
187            &TransItemSourceKind::DropInPlaceMethod(impl_kind) => {
188                let Some(ItemId::Fun(id)) = trans_id else {
189                    unreachable!()
190                };
191                let fun_decl =
192                    bt_ctx.translate_drop_in_place_method(id, item_meta, &def, impl_kind)?;
193                self.translated.fun_decls.set_slot(id, fun_decl);
194            }
195            TransItemSourceKind::VTable => {
196                let Some(ItemId::Type(id)) = trans_id else {
197                    unreachable!()
198                };
199                let ty_decl = bt_ctx.translate_vtable_struct(id, item_meta, &def)?;
200                self.translated.type_decls.set_slot(id, ty_decl);
201            }
202            TransItemSourceKind::VTableInstance(impl_kind) => {
203                let Some(ItemId::Global(id)) = trans_id else {
204                    unreachable!()
205                };
206                let global_decl =
207                    bt_ctx.translate_vtable_instance(id, item_meta, &def, impl_kind)?;
208                self.translated.global_decls.set_slot(id, global_decl);
209            }
210            TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
211                let Some(ItemId::Fun(id)) = trans_id else {
212                    unreachable!()
213                };
214                let fun_decl =
215                    bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?;
216                self.translated.fun_decls.set_slot(id, fun_decl);
217            }
218            TransItemSourceKind::VTableMethod => {
219                let Some(ItemId::Fun(id)) = trans_id else {
220                    unreachable!()
221                };
222                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
223                self.translated.fun_decls.set_slot(id, fun_decl);
224            }
225            TransItemSourceKind::VTableDropShim => {
226                let Some(ItemId::Fun(id)) = trans_id else {
227                    unreachable!()
228                };
229                let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def)?;
230                self.translated.fun_decls.set_slot(id, fun_decl);
231            }
232        }
233        Ok(())
234    }
235
236    /// While translating an item you may need the contents of another. Use this to retreive the
237    /// translated version of this item. Use with care as this could create cycles.
238    pub(crate) fn get_or_translate(&mut self, id: ItemId) -> Result<krate::ItemRef<'_>, Error> {
239        // We have to call `get_item` a few times because we're running into the classic `Polonius`
240        // problem case.
241        if self.translated.get_item(id).is_none() {
242            let item_source = self.reverse_id_map.get(&id).unwrap().clone();
243            self.translate_item(&item_source);
244            if self.translated.get_item(id).is_none() {
245                let span = self.def_span(item_source.def_id());
246                let name = self
247                    .translated
248                    .item_name(id)
249                    .map(|n| n.to_string_with_ctx(&self.into_fmt()))
250                    .unwrap_or_else(|| id.to_string());
251                // Not a real error, its message won't be displayed.
252                return Err(Error {
253                    span,
254                    msg: format!("Failed to translate item {name}."),
255                });
256                // raise_error!(self, span, "Failed to translate item {name}.")
257            }
258            // Add to avoid the double translation of the same item
259            self.processed.insert(item_source.clone());
260        }
261        let item = self.translated.get_item(id);
262        Ok(item.unwrap())
263    }
264
265    /// Record that `method_id` is an implementation of the given method of the trait. If the
266    /// method is not used anywhere yet we simply record the implementation. If the method is used
267    /// then we enqueue it for translation.
268    pub fn register_method_impl(
269        &mut self,
270        trait_id: TraitDeclId,
271        method_id: TraitMethodId,
272        fun_id: FunDeclId,
273    ) {
274        match &mut self.method_status[trait_id][method_id] {
275            MethodStatus::Unused { implementors } => {
276                implementors.insert(fun_id);
277            }
278            MethodStatus::Used => {
279                self.enqueue_id(fun_id);
280            }
281        }
282    }
283
284    /// Mark the method as "used", which will enqueue for translation all the implementations of
285    /// that method.
286    pub fn mark_method_as_used(&mut self, trait_id: TraitDeclId, method_id: TraitMethodId) {
287        let old_status = mem::replace(
288            &mut self.method_status[trait_id][method_id],
289            MethodStatus::Used,
290        );
291        match old_status {
292            MethodStatus::Unused { implementors } => {
293                for fun_id in implementors {
294                    self.enqueue_id(fun_id);
295                }
296            }
297            MethodStatus::Used => {}
298        }
299    }
300
301    /// Keep only the methods we marked as "used".
302    pub fn remove_unused_methods(&mut self) {
303        let method_is_used = |trait_id: TraitDeclId, method_id: TraitMethodId| {
304            matches!(self.method_status[trait_id][method_id], MethodStatus::Used)
305        };
306        for tdecl in self.translated.trait_decls.iter_mut() {
307            tdecl
308                .methods
309                .retain(|i, _m| method_is_used(tdecl.def_id, i));
310        }
311        for timpl in self.translated.trait_impls.iter_mut() {
312            let trait_id = timpl.impl_trait.id;
313            timpl.methods.retain(|i, _m| method_is_used(trait_id, i));
314        }
315    }
316}
317
318impl<'tcx> ItemTransCtx<'tcx, '_> {
319    /// Register the items inside this module or inherent impl.
320    // TODO: we may want to accumulate the set of modules we found, to check that all
321    // the opaque modules given as arguments actually exist
322    #[tracing::instrument(skip(self, item_meta, def))]
323    pub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef<'tcx>) {
324        if !item_meta.opacity.is_transparent() {
325            return;
326        }
327        match def.kind() {
328            hax::FullDefKind::InherentImpl { items, .. } => {
329                for assoc in items {
330                    self.t_ctx.enqueue_module_item(&assoc.def_id);
331                }
332            }
333            hax::FullDefKind::Mod { items, .. } => {
334                for (_, def_id) in items {
335                    self.t_ctx.enqueue_module_item(def_id);
336                }
337            }
338            hax::FullDefKind::ForeignMod { items, .. } => {
339                for def_id in items {
340                    self.t_ctx.enqueue_module_item(def_id);
341                }
342            }
343            _ => panic!("Item should be a module but isn't: {def:?}"),
344        }
345    }
346
347    pub(crate) fn get_item_source(
348        &mut self,
349        span: Span,
350        def: &hax::FullDef<'tcx>,
351    ) -> Result<ItemSource, Error> {
352        let assoc = match def.kind() {
353            hax::FullDefKind::AssocTy {
354                associated_item, ..
355            }
356            | hax::FullDefKind::AssocConst {
357                associated_item, ..
358            }
359            | hax::FullDefKind::AssocFn {
360                associated_item, ..
361            } => associated_item,
362            hax::FullDefKind::Closure { args, .. } => {
363                let info = self.translate_closure_info(span, args)?;
364                return Ok(ItemSource::Closure { info });
365            }
366            _ => return Ok(ItemSource::TopLevel),
367        };
368        Ok(match &assoc.container {
369            // E.g.:
370            // ```
371            // impl<T> List<T> {
372            //   fn new() -> Self { ... } <- inherent method
373            // }
374            // ```
375            hax::AssocItemContainer::InherentImplContainer { .. } => ItemSource::TopLevel,
376            // E.g.:
377            // ```
378            // impl Foo for Bar {
379            //   fn baz(...) { ... } // <- implementation of a trait method
380            // }
381            // ```
382            hax::AssocItemContainer::TraitImplContainer {
383                impl_,
384                implemented_trait_ref,
385                overrides_default,
386                ..
387            } => {
388                let impl_ref =
389                    self.translate_trait_impl_ref(span, impl_, TraitImplSource::Normal)?;
390                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
391                let item_id = self.translate_assoc_item_id(trait_ref.id, def.def_id())?;
392                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
393                    // If the implementation is getting translated, that means the method is
394                    // getting used.
395                    let method_id = *item_id.as_method().unwrap();
396                    self.mark_method_as_used(trait_ref.id, method_id);
397                }
398                ItemSource::TraitImpl {
399                    impl_ref,
400                    trait_ref,
401                    item_id,
402                    reuses_default: !overrides_default,
403                }
404            }
405            // This method is the *declaration* of a trait item
406            // E.g.:
407            // ```
408            // trait Foo {
409            //   fn baz(...); // <- declaration of a trait method
410            // }
411            // ```
412            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
413                // The trait id should be Some(...): trait markers (that we may eliminate)
414                // don't have associated items.
415                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
416                let item_id = self.translate_assoc_item_id(trait_ref.id, def.def_id())?;
417                ItemSource::TraitDecl {
418                    trait_ref,
419                    item_id,
420                    has_default: assoc.has_value,
421                }
422            }
423        })
424    }
425
426    /// Translate a type definition.
427    ///
428    /// Note that we translate the types one by one: we don't need to take into
429    /// account the fact that some types are mutually recursive at this point
430    /// (we will need to take that into account when generating the code in a file).
431    #[tracing::instrument(skip(self, item_meta, def))]
432    pub fn translate_type_decl(
433        mut self,
434        trans_id: TypeDeclId,
435        item_meta: ItemMeta,
436        def: &hax::FullDef<'tcx>,
437    ) -> Result<TypeDecl, Error> {
438        let span = item_meta.span;
439
440        // Get the kind of the type decl -- is it a closure?
441        let src = self.get_item_source(span, def)?;
442
443        let mut repr: Option<ReprOptions> = None;
444
445        // Translate type body
446        let kind = match &def.kind {
447            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
448            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
449            hax::FullDefKind::TyAlias { ty, .. } => {
450                // Don't error on missing trait refs.
451                self.error_on_impl_expr_error = false;
452                self.translate_ty(span, ty).map(TypeDeclKind::Alias)
453            }
454            hax::FullDefKind::Adt { repr: hax_repr, .. } => {
455                repr = Some(self.translate_repr_options(hax_repr));
456                self.translate_adt_def(trans_id, span, &item_meta, def)
457            }
458            hax::FullDefKind::Closure { args, .. } => self.translate_closure_adt(span, args),
459            _ => panic!("Unexpected item when translating types: {def:?}"),
460        };
461
462        let kind = match kind {
463            Ok(kind) => kind,
464            Err(err) => TypeDeclKind::Error(err.msg),
465        };
466        let layout = self
467            .translate_layout(def.this())
468            .into_iter()
469            .map(|l| (self.get_target_triple(), l))
470            .collect();
471        let ptr_metadata = self.translate_ptr_metadata(span, def.this())?;
472        let type_def = TypeDecl {
473            def_id: trans_id,
474            item_meta,
475            generics: self.into_generics(),
476            kind,
477            src,
478            layout,
479            ptr_metadata,
480            repr,
481        };
482
483        Ok(type_def)
484    }
485
486    /// Translate one function.
487    #[tracing::instrument(skip(self, item_meta, def))]
488    pub fn translate_fun_decl(
489        mut self,
490        def_id: FunDeclId,
491        item_meta: ItemMeta,
492        def: &hax::FullDef<'tcx>,
493    ) -> Result<FunDecl, Error> {
494        let span = item_meta.span;
495
496        let src = self.get_item_source(span, def)?;
497
498        if let hax::FullDefKind::Ctor {
499            fields, output_ty, ..
500        } = def.kind()
501        {
502            let signature = FunSig {
503                inputs: fields
504                    .iter()
505                    .map(|field| self.translate_ty(span, &field.ty))
506                    .try_collect()?,
507                output: self.translate_ty(span, output_ty)?,
508                is_unsafe: false,
509            };
510
511            let body = if item_meta.opacity.with_private_contents().is_opaque() {
512                Body::Opaque
513            } else {
514                self.build_ctor_body(span, def)?
515            };
516            return Ok(FunDecl {
517                def_id,
518                item_meta,
519                generics: self.into_generics(),
520                signature,
521                src,
522                is_global_initializer: None,
523                body,
524            });
525        }
526
527        // Translate the function signature
528        trace!("Translating function signature");
529        let signature = match &def.kind {
530            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
531                self.translate_fun_sig(span, &sig.value)?
532            }
533            hax::FullDefKind::Const { ty, .. }
534            | hax::FullDefKind::AssocConst { ty, .. }
535            | hax::FullDefKind::Static { ty, .. } => FunSig {
536                inputs: vec![],
537                output: self.translate_ty(span, ty)?,
538                is_unsafe: false,
539            },
540            _ => panic!("Unexpected definition for function: {def:?}"),
541        };
542
543        // Check whether this function is a method declaration for a trait definition.
544        // If this is the case, it shouldn't contain a body.
545        let is_trait_method_decl_without_default = match &src {
546            ItemSource::TraitDecl { has_default, .. } => !has_default,
547            _ => false,
548        };
549
550        let intrinsic_name = def
551            .def_id()
552            .as_rust_def_id()
553            .and_then(|id| self.tcx.intrinsic(id))
554            .map(|i| i.name.to_ident_string());
555
556        let is_global_initializer = matches!(
557            def.kind(),
558            hax::FullDefKind::Const { .. }
559                | hax::FullDefKind::AssocConst { .. }
560                | hax::FullDefKind::Static { .. }
561        );
562        let is_global_initializer = is_global_initializer
563            .then(|| self.register_item(span, def.this(), TransItemSourceKind::Global));
564
565        let body = if let Some(name) = intrinsic_name {
566            let arg_names = self.translate_argument_names(span, def, signature.inputs.len());
567            Body::Intrinsic { name, arg_names }
568        } else if let Some(name) = self.t_ctx.extern_item_symbol_name(def) {
569            Body::Extern(name)
570        } else if item_meta.opacity.with_private_contents().is_opaque() {
571            Body::Opaque
572        } else if is_trait_method_decl_without_default {
573            Body::TraitMethodWithoutDefault
574        } else {
575            // Translate the MIR body for this definition.
576            self.translate_def_body(item_meta.span, def)
577        };
578        Ok(FunDecl {
579            def_id,
580            item_meta,
581            generics: self.into_generics(),
582            signature,
583            src,
584            is_global_initializer,
585            body,
586        })
587    }
588
589    /// Translate one global.
590    #[tracing::instrument(skip(self, item_meta, def))]
591    pub fn translate_global(
592        mut self,
593        def_id: GlobalDeclId,
594        item_meta: ItemMeta,
595        def: &hax::FullDef<'tcx>,
596    ) -> Result<GlobalDecl, Error> {
597        let span = item_meta.span;
598
599        // Retrieve the kind
600        let item_source = self.get_item_source(span, def)?;
601
602        trace!("Translating global type");
603        let ty = match &def.kind {
604            hax::FullDefKind::Const { ty, .. }
605            | hax::FullDefKind::AssocConst { ty, .. }
606            | hax::FullDefKind::Static { ty, .. } => ty,
607            _ => panic!("Unexpected def for constant: {def:?}"),
608        };
609        let ty = self.translate_ty(span, ty)?;
610
611        let global_kind = match &def.kind {
612            hax::FullDefKind::Static { .. } => GlobalKind::Static,
613            hax::FullDefKind::Const {
614                kind: hax::ConstKind::TopLevel,
615                ..
616            }
617            | hax::FullDefKind::AssocConst { .. } => GlobalKind::NamedConst,
618            hax::FullDefKind::Const { .. } => GlobalKind::AnonConst,
619            _ => panic!("Unexpected def for constant: {def:?}"),
620        };
621
622        let initializer = self.register_item(span, def.this(), TransItemSourceKind::Fun);
623
624        Ok(GlobalDecl {
625            def_id,
626            item_meta,
627            generics: self.into_generics(),
628            ty,
629            src: item_source,
630            global_kind,
631            init: initializer,
632        })
633    }
634
635    // either Poly or MonoTrait
636    #[tracing::instrument(skip(self, item_meta, def))]
637    pub fn translate_trait_decl(
638        mut self,
639        trait_decl_id: TraitDeclId,
640        item_meta: ItemMeta,
641        def: &hax::FullDef<'tcx>,
642    ) -> Result<TraitDecl, Error> {
643        let span = item_meta.span;
644
645        let (hax::FullDefKind::Trait {
646            implied_predicates, ..
647        }
648        | hax::FullDefKind::TraitAlias {
649            implied_predicates, ..
650        }) = def.kind()
651        else {
652            raise_error!(self, span, "Unexpected definition: {def:?}");
653        };
654
655        // Register implied predicates. We gather the clauses and consider the other predicates as
656        // required since the distinction doesn't matter for non-trait-clauses.
657        let mut implied_clauses = Default::default();
658        self.translate_predicates(
659            implied_predicates,
660            PredicateOrigin::WhereClauseOnTrait,
661            Some(&mut implied_clauses),
662        )?;
663
664        let vtable = self.translate_vtable_struct_ref_no_enqueue(span, def.this())?;
665
666        if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
667            // Trait aliases don't have any items. Everything interesting is in the parent clauses.
668            return Ok(TraitDecl {
669                def_id: trait_decl_id,
670                item_meta,
671                implied_clauses,
672                generics: self.into_generics(),
673                consts: Default::default(),
674                types: Default::default(),
675                methods: Default::default(),
676                vtable,
677            });
678        }
679
680        let hax::FullDefKind::Trait {
681            items,
682            self_predicate,
683            ..
684        } = &def.kind
685        else {
686            unreachable!()
687        };
688        let self_trait_ref = TraitRef::new(
689            TraitRefKind::SelfId,
690            RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?),
691        );
692
693        // Translate the associated items
694        self.register_assoc_items(def.def_id(), trait_decl_id)?;
695        let mut consts: IndexMap<AssocConstId, _> = IndexMap::new();
696        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
697        let mut methods: IndexMap<TraitMethodId, _> = IndexMap::new();
698
699        // skip all associated items of trait decl in mono mode
700        // question: what if the associated methods (or consts) has default implmentation?
701        // TODO: support default methods and default consts
702        if self.monomorphize() {
703            return Ok(TraitDecl {
704                def_id: trait_decl_id,
705                item_meta,
706                implied_clauses,
707                generics: self.into_generics(),
708                consts,
709                types,
710                methods,
711                vtable,
712            });
713        }
714
715        for hax_item in items {
716            let item_def_id = &hax_item.def_id;
717            let item_span = self.def_span(item_def_id);
718            let assoc_item_id = self.translate_assoc_item_id(trait_decl_id, item_def_id)?;
719            let item_name = self
720                .translated
721                .assoc_item_name(trait_decl_id, assoc_item_id);
722
723            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
724            // polymorphic item as usual.
725            let trans_kind = match hax_item.kind {
726                hax::AssocKind::Fn { .. } => TransItemSourceKind::Fun,
727                hax::AssocKind::Const { .. } => TransItemSourceKind::Global,
728                hax::AssocKind::Type { .. } => TransItemSourceKind::Type,
729            };
730
731            let item_def = self.poly_hax_def(item_def_id)?;
732            let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
733            let attr_info = self.translate_attr_info(&item_def);
734
735            match item_def.kind() {
736                hax::FullDefKind::AssocFn { sig, .. } => {
737                    let trait_method_id = *assoc_item_id.as_method().unwrap();
738                    let fun_id = self.register_no_enqueue(item_span, &item_src);
739                    // Register this method.
740                    self.register_method_impl(trait_decl_id, trait_method_id, fun_id);
741                    // By default we only enqueue required methods (those that don't have a default
742                    // impl). If the trait is transparent, we enqueue all its methods.
743                    if self.options.translate_all_methods
744                        || item_meta.opacity.is_transparent()
745                        || !hax_item.has_value
746                    {
747                        self.mark_method_as_used(trait_decl_id, trait_method_id);
748                    }
749
750                    let binder_kind = BinderKind::TraitMethod(trait_decl_id, trait_method_id);
751                    let mut method = self.translate_binder_for_def(
752                        item_span,
753                        binder_kind,
754                        &item_def,
755                        |bt_ctx| {
756                            assert_eq!(bt_ctx.binding_levels.len(), 2);
757                            let fun_generics = bt_ctx
758                                .outermost_binder()
759                                .params
760                                .identity_args_at_depth(DeBruijnId::one())
761                                .concat(
762                                    &bt_ctx
763                                        .innermost_binder()
764                                        .params
765                                        .identity_args_at_depth(DeBruijnId::zero()),
766                                );
767                            let fn_ref = FunDeclRef {
768                                id: fun_id,
769                                generics: Box::new(fun_generics),
770                            };
771                            // `skip_binder` is allowed because `translate_binder_for_def` puts the
772                            // late bound params in scope.
773                            let signature =
774                                bt_ctx.translate_fun_sig(span, sig.hax_skip_binder_ref())?;
775                            Ok(TraitMethod {
776                                name: item_name,
777                                attr_info,
778                                signature,
779                                item: fn_ref,
780                            })
781                        },
782                    )?;
783                    // In hax, associated items take an extra explicit `Self: Trait` clause, but we
784                    // don't want that to be part of the method clauses. Hence we remove the first
785                    // bound clause and replace its uses with references to the ambient `Self`
786                    // clause available in trait declarations.
787                    struct ReplaceSelfVisitor;
788                    impl VarsVisitor for ReplaceSelfVisitor {
789                        fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
790                            if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
791                                // Replace clause 0 and decrement the others.
792                                Some(if let Some(new_id) = clause_id.index().checked_sub(1) {
793                                    TraitRefKind::Clause(DeBruijnVar::Bound(
794                                        DeBruijnId::ZERO,
795                                        TraitClauseId::new(new_id),
796                                    ))
797                                } else {
798                                    TraitRefKind::SelfId
799                                })
800                            } else {
801                                None
802                            }
803                        }
804                    }
805                    method.params.visit_vars(&mut ReplaceSelfVisitor);
806                    method.skip_binder.visit_vars(&mut ReplaceSelfVisitor);
807                    method
808                        .params
809                        .trait_clauses
810                        .remove_and_shift_ids(TraitClauseId::ZERO);
811                    method.params.trait_clauses.iter_mut().for_each(|clause| {
812                        clause.clause_id -= 1;
813                    });
814
815                    // We insert the `Binder<TraitMethod>` unconditionally here; we'll remove the
816                    // ones that correspond to unused methods at the end of translation.
817                    methods.set_slot_extend(trait_method_id, method);
818                }
819                hax::FullDefKind::AssocConst { ty, .. } => {
820                    let assoc_const_id = *assoc_item_id.as_const().unwrap();
821                    // The const is defined in a context that has an extra `Self: Trait` clause, so
822                    // we translate it bound first.
823                    let bound_assoc_const = self.translate_binder_for_def(
824                        item_span,
825                        BinderKind::Other,
826                        &item_def,
827                        |ctx| {
828                            // Check if the constant has a value (i.e., a body).
829                            let default = hax_item.has_value.then(|| {
830                                // The parameters of the constant are the same as those of the item that
831                                // declares them.
832                                let id = ctx.register_and_enqueue(item_span, item_src);
833                                let generics = ctx
834                                    .outermost_binder()
835                                    .params
836                                    .identity_args_at_depth(DeBruijnId::one())
837                                    .concat(
838                                        &ctx.innermost_binder()
839                                            .params
840                                            .identity_args_at_depth(DeBruijnId::zero()),
841                                    );
842                                GlobalDeclRef {
843                                    id,
844                                    generics: Box::new(generics),
845                                }
846                            });
847                            let ty = ctx.translate_ty(item_span, ty)?;
848                            Ok(TraitAssocConst {
849                                name: item_name,
850                                attr_info,
851                                ty,
852                                default,
853                            })
854                        },
855                    )?;
856                    let assoc_const = bound_assoc_const.apply(&{
857                        let mut generics = GenericArgs::empty();
858                        // Provide the `Self` clause.
859                        generics.trait_refs.push(self_trait_ref.clone());
860                        generics
861                    });
862                    consts.set_slot_extend(assoc_const_id, assoc_const);
863                }
864                hax::FullDefKind::AssocTy {
865                    implied_predicates,
866                    value: default,
867                    ..
868                } => {
869                    let assoc_type_id = *assoc_item_id.as_type().unwrap();
870                    let binder_kind = BinderKind::TraitType(trait_decl_id, assoc_type_id);
871                    let assoc_ty =
872                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
873                            // Also add the implied predicates.
874                            let mut implied_clauses = Default::default();
875                            ctx.translate_predicates(
876                                implied_predicates,
877                                PredicateOrigin::TraitItem(assoc_type_id),
878                                Some(&mut implied_clauses),
879                            )?;
880
881                            let default = default
882                                .as_ref()
883                                .map(|(ty, impl_exprs)| -> Result<_, Error> {
884                                    let ty = ctx.translate_ty(item_span, ty)?;
885                                    let trefs = ctx.translate_trait_impl_exprs(span, impl_exprs)?;
886                                    Ok(TraitAssocTyImpl {
887                                        value: ty,
888                                        implied_trait_refs: trefs,
889                                    })
890                                })
891                                .transpose()?;
892                            Ok(TraitAssocTy {
893                                name: item_name,
894                                attr_info,
895                                default,
896                                implied_clauses,
897                            })
898                        })?;
899                    types.set_slot_extend(assoc_type_id, assoc_ty);
900                }
901                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
902            }
903        }
904
905        if def.lang_item == Some(sym::destruct) {
906            // Add a `drop_in_place(*mut self)` method that contains the drop glue for this type.
907            let (method_id, method_binder) =
908                self.prepare_drop_in_place_method(def, span, def.def_id(), trait_decl_id, None)?;
909            let method_name = self.translated.assoc_item_name(trait_decl_id, method_id);
910            self.mark_method_as_used(trait_decl_id, method_id);
911            let method = method_binder.map(|fn_ref| {
912                let self_ty = if self.monomorphize() {
913                    // FIXME: put something real here
914                    Ty::mk_unit()
915                } else {
916                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::one(), TypeVarId::ZERO))
917                        .into_ty()
918                };
919                let signature = self.drop_in_place_method_sig(self_ty);
920                TraitMethod {
921                    name: method_name,
922                    item: fn_ref,
923                    attr_info: AttrInfo::dummy_public(),
924                    signature,
925                }
926            });
927            methods.set_slot_extend(method_id, method);
928        }
929
930        // In case of a trait implementation, some values may not have been
931        // provided, in case the declaration provided default values. We
932        // check those, and lookup the relevant values.
933        Ok(TraitDecl {
934            def_id: trait_decl_id,
935            item_meta,
936            implied_clauses,
937            generics: self.into_generics(),
938            consts,
939            types,
940            methods,
941            vtable,
942        })
943    }
944
945    #[tracing::instrument(skip(self, item_meta, def))]
946    pub fn translate_trait_impl(
947        mut self,
948        def_id: TraitImplId,
949        item_meta: ItemMeta,
950        def: &hax::FullDef<'tcx>,
951    ) -> Result<TraitImpl, Error> {
952        let span = item_meta.span;
953
954        let hax::FullDefKind::TraitImpl {
955            trait_pred,
956            implied_impl_exprs,
957            items: impl_items,
958            ..
959        } = &def.kind
960        else {
961            unreachable!()
962        };
963
964        // Retrieve the information about the implemented trait.
965        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
966        let trait_id = implemented_trait.id;
967        // A `TraitRef` that points to this impl with the correct generics.
968        let self_predicate = TraitRef::new(
969            TraitRefKind::TraitImpl(TraitImplRef {
970                id: def_id,
971                generics: Box::new(self.the_only_binder().params.identity_args()),
972            }),
973            RegionBinder::empty(implemented_trait.clone()),
974        );
975
976        let vtable =
977            self.translate_vtable_instance_ref_no_enqueue(span, &trait_pred.trait_ref, def.this())?;
978
979        // The trait refs which implement the parent clauses of the implemented trait decl.
980        let implied_trait_refs = self.translate_trait_impl_exprs(span, implied_impl_exprs)?;
981
982        {
983            // Debugging
984            let ctx = self.into_fmt();
985            let refs = implied_trait_refs
986                .iter()
987                .map(|c| c.with_ctx(&ctx))
988                .format("\n");
989            trace!(
990                "Trait impl: {:?}\n- implied_trait_refs:\n{}",
991                def.def_id(),
992                refs
993            );
994        }
995
996        let implemented_trait_def = self.poly_hax_def(&trait_pred.trait_ref.def_id)?;
997        if implemented_trait_def.lang_item == Some(sym::destruct) {
998            raise_error!(
999                self,
1000                span,
1001                "found an explicit impl of `core::marker::Destruct`, this should not happen"
1002            );
1003        }
1004
1005        // Explore the associated items
1006        let mut consts: IndexMap<AssocConstId, _> = IndexMap::new();
1007        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
1008        let mut methods: IndexMap<TraitMethodId, _> = IndexMap::new();
1009
1010        // In mono mode, we do not translate any associated items in trait impl.
1011        if self.monomorphize() {
1012            return Ok(TraitImpl {
1013                def_id,
1014                item_meta,
1015                impl_trait: implemented_trait,
1016                generics: self.into_generics(),
1017                implied_trait_refs,
1018                consts,
1019                types,
1020                methods,
1021                vtable,
1022            });
1023        }
1024
1025        for impl_item in impl_items {
1026            use crate::hax::ImplAssocItemValue::*;
1027            let item_def_id = impl_item.def_id();
1028            let item_span = self.def_span(item_def_id);
1029            let assoc_item_id = self.translate_assoc_item_id(trait_id, item_def_id)?;
1030
1031            // In not-mono mode, we use the polymorphic item as usual.
1032            let item_def = self.poly_hax_def(item_def_id)?;
1033            let trans_kind = match item_def.kind() {
1034                hax::FullDefKind::AssocFn { .. } => TransItemSourceKind::Fun,
1035                hax::FullDefKind::AssocConst { .. } => TransItemSourceKind::Global,
1036                hax::FullDefKind::AssocTy { .. } => TransItemSourceKind::Type,
1037                _ => unreachable!(),
1038            };
1039            let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
1040
1041            match item_def.kind() {
1042                hax::FullDefKind::AssocFn { .. } => {
1043                    let trait_method_id = *assoc_item_id.as_method().unwrap();
1044                    let fun_id: FunDeclId = {
1045                        let method_src = match &impl_item.value {
1046                            Provided { .. } => item_src,
1047                            // This will generate a copy of the default method. Note that the base
1048                            // item for `DefaultedMethod` is the trait impl.
1049                            DefaultedFn { .. } => TransItemSource::from_item(
1050                                def.this(),
1051                                TransItemSourceKind::DefaultedMethod(
1052                                    TraitImplSource::Normal,
1053                                    trait_id,
1054                                    trait_method_id,
1055                                ),
1056                                self.monomorphize(),
1057                            ),
1058                            _ => unreachable!(),
1059                        };
1060                        self.register_no_enqueue(item_span, &method_src)
1061                    };
1062
1063                    // Register this method.
1064                    self.register_method_impl(trait_id, trait_method_id, fun_id);
1065                    // By default we only enqueue required methods (those that don't have a default
1066                    // impl). If the impl is transparent, we enqueue all the implemented methods.
1067                    if matches!(impl_item.value, Provided { .. })
1068                        && item_meta.opacity.is_transparent()
1069                    {
1070                        self.mark_method_as_used(trait_id, trait_method_id);
1071                    }
1072
1073                    let binder_kind = BinderKind::TraitMethod(trait_id, trait_method_id);
1074                    let bound_fn_ref = match &impl_item.value {
1075                        Provided { .. } => self.translate_binder_for_def(
1076                            item_span,
1077                            binder_kind,
1078                            &item_def,
1079                            |ctx| {
1080                                let generics = ctx
1081                                    .outermost_generics()
1082                                    .identity_args_at_depth(DeBruijnId::one())
1083                                    .concat(
1084                                        &ctx.innermost_generics()
1085                                            .identity_args_at_depth(DeBruijnId::zero()),
1086                                    );
1087                                Ok(FunDeclRef {
1088                                    id: fun_id,
1089                                    generics: Box::new(generics),
1090                                })
1091                            },
1092                        )?,
1093                        DefaultedFn { .. } => {
1094                            // Retrieve the method generics from the trait decl.
1095                            let bound_method =
1096                                match self.get_or_translate(implemented_trait.id.into()) {
1097                                    Ok(ItemRef::TraitDecl(tdecl)) => {
1098                                        tdecl.methods.get(trait_method_id).cloned()
1099                                    }
1100                                    _ => None,
1101                                };
1102                            let Some(bound_method) = bound_method else {
1103                                continue;
1104                            };
1105                            let method_params =
1106                                bound_method.substitute_with_tref(&self_predicate).params;
1107
1108                            let generics = self
1109                                .outermost_generics()
1110                                .identity_args_at_depth(DeBruijnId::one())
1111                                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
1112                            let fn_ref = FunDeclRef {
1113                                id: fun_id,
1114                                generics: Box::new(generics),
1115                            };
1116                            Binder::new(binder_kind, method_params, fn_ref)
1117                        }
1118                        _ => unreachable!(),
1119                    };
1120
1121                    // We insert the `Binder<FunDeclRef>` unconditionally here; we'll remove the
1122                    // ones that correspond to unused methods at the end of translation.
1123                    methods.set_slot_extend(trait_method_id, bound_fn_ref);
1124                }
1125                hax::FullDefKind::AssocConst { .. } => {
1126                    let assoc_const_id = *assoc_item_id.as_const().unwrap();
1127                    let id = self.register_and_enqueue(item_span, item_src);
1128                    // The parameters of the constant are the same as those of the item that
1129                    // declares them.
1130                    let generics = match &impl_item.value {
1131                        Provided { .. } => self.the_only_binder().params.identity_args(),
1132                        _ => {
1133                            let mut generics = implemented_trait.generics.as_ref().clone();
1134                            // For default consts, we add an extra `Self` predicate.
1135                            generics.trait_refs.push(self_predicate.clone());
1136                            generics
1137                        }
1138                    };
1139                    let gref = GlobalDeclRef {
1140                        id,
1141                        generics: Box::new(generics),
1142                    };
1143                    consts.set_slot_extend(assoc_const_id, gref);
1144                }
1145                hax::FullDefKind::AssocTy { value, .. } => {
1146                    let assoc_type_id = *assoc_item_id.as_type().unwrap();
1147                    let binder_kind = BinderKind::TraitType(trait_id, assoc_type_id);
1148                    let assoc_ty = match &impl_item.value {
1149                        Provided { .. } => self.translate_binder_for_def(
1150                            item_span,
1151                            binder_kind,
1152                            &item_def,
1153                            |ctx| {
1154                                let (ty, _impl_exprs) = value.as_ref().unwrap();
1155                                let ty = ctx.translate_ty(item_span, ty)?;
1156                                let implied_trait_refs = ctx.translate_trait_impl_exprs(
1157                                    item_span,
1158                                    &impl_item.required_impl_exprs,
1159                                )?;
1160                                Ok(TraitAssocTyImpl {
1161                                    value: ty,
1162                                    implied_trait_refs,
1163                                })
1164                            },
1165                        )?,
1166                        DefaultedTy { .. } => {
1167                            // Retrieve the type from the trait decl.
1168                            let trait_id = implemented_trait.id;
1169                            let bound_ty = match self.get_or_translate(trait_id.into()) {
1170                                Ok(ItemRef::TraitDecl(tdecl)) => tdecl.types.get(assoc_type_id),
1171                                _ => None,
1172                            };
1173                            let Some(bound_ty) = bound_ty else {
1174                                register_error!(
1175                                    self,
1176                                    item_span,
1177                                    "couldn't translate defaulted associated type; \
1178                                    either the corresponding trait decl caused errors \
1179                                    or it was declared opaque."
1180                                );
1181                                continue;
1182                            };
1183                            bound_ty
1184                                .clone()
1185                                .substitute_with_tref(&self_predicate)
1186                                .map(|ty_decl: TraitAssocTy| ty_decl.default.unwrap())
1187                        }
1188                        _ => unreachable!(),
1189                    };
1190
1191                    types.set_slot_extend(assoc_type_id, assoc_ty);
1192                }
1193                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
1194            }
1195        }
1196
1197        Ok(TraitImpl {
1198            def_id,
1199            item_meta,
1200            impl_trait: implemented_trait,
1201            generics: self.into_generics(),
1202            implied_trait_refs,
1203            consts,
1204            types,
1205            methods,
1206            vtable,
1207        })
1208    }
1209
1210    /// Generate a blanket impl for this trait, as in:
1211    /// ```
1212    ///     trait Alias<U> = Trait<Option<U>, Item = u32> + Clone;
1213    /// ```
1214    /// becomes:
1215    /// ```
1216    ///     trait Alias<U>: Trait<Option<U>, Item = u32> + Clone {}
1217    ///     impl<U, Self: Trait<Option<U>, Item = u32> + Clone> Alias<U> for Self {}
1218    /// ```
1219    #[tracing::instrument(skip(self, item_meta, def))]
1220    pub fn translate_trait_alias_blanket_impl(
1221        mut self,
1222        def_id: TraitImplId,
1223        item_meta: ItemMeta,
1224        def: &hax::FullDef<'tcx>,
1225    ) -> Result<TraitImpl, Error> {
1226        let span = item_meta.span;
1227
1228        let hax::FullDefKind::TraitAlias {
1229            implied_predicates,
1230            self_predicate,
1231            ..
1232        } = &def.kind
1233        else {
1234            raise_error!(self, span, "Unexpected definition: {def:?}");
1235        };
1236
1237        // Retrieve the information about the implemented trait.
1238        let implemented_trait = self.translate_trait_ref(span, &self_predicate.trait_ref)?;
1239
1240        // Register the trait implied clauses as required clauses for the impl.
1241        assert!(self.innermost_generics_mut().trait_clauses.is_empty());
1242        self.register_predicates(implied_predicates, PredicateOrigin::WhereClauseOnTrait)?;
1243
1244        let mut generics = self.the_only_binder().params.identity_args();
1245        // Do the inverse operation: the trait considers the clauses as implied.
1246        let implied_trait_refs = mem::take(&mut generics.trait_refs);
1247
1248        let mut timpl = TraitImpl {
1249            def_id,
1250            item_meta,
1251            impl_trait: implemented_trait,
1252            generics: self.the_only_binder().params.clone(),
1253            implied_trait_refs,
1254            consts: Default::default(),
1255            types: Default::default(),
1256            methods: Default::default(),
1257            // TODO(dyn)
1258            vtable: None,
1259        };
1260        // We got the predicates from a trait decl, so they may refer to the virtual `Self`
1261        // clause, which doesn't exist for impls. We fix that up here.
1262        {
1263            struct FixSelfVisitor {
1264                binder_depth: DeBruijnId,
1265            }
1266            struct UnhandledSelf;
1267            impl Visitor for FixSelfVisitor {
1268                type Break = UnhandledSelf;
1269            }
1270            impl VisitorWithBinderDepth for FixSelfVisitor {
1271                fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
1272                    &mut self.binder_depth
1273                }
1274            }
1275            impl VisitAstMut for FixSelfVisitor {
1276                fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
1277                    VisitWithBinderDepth::new(self).visit(x)
1278                }
1279                fn visit_trait_ref_kind(
1280                    &mut self,
1281                    kind: &mut TraitRefKind,
1282                ) -> ControlFlow<Self::Break> {
1283                    match kind {
1284                        TraitRefKind::SelfId => return ControlFlow::Break(UnhandledSelf),
1285                        TraitRefKind::ParentClause(sub, clause_id)
1286                            if matches!(sub.kind, TraitRefKind::SelfId) =>
1287                        {
1288                            *kind = TraitRefKind::Clause(DeBruijnVar::bound(
1289                                self.binder_depth,
1290                                *clause_id,
1291                            ))
1292                        }
1293                        _ => (),
1294                    }
1295                    self.visit_inner(kind)
1296                }
1297            }
1298            match timpl.drive_mut(&mut FixSelfVisitor {
1299                binder_depth: DeBruijnId::zero(),
1300            }) {
1301                ControlFlow::Continue(()) => {}
1302                ControlFlow::Break(UnhandledSelf) => {
1303                    register_error!(
1304                        self,
1305                        span,
1306                        "Found `Self` clause we can't handle \
1307                         in a trait alias blanket impl."
1308                    );
1309                }
1310            }
1311        };
1312
1313        Ok(timpl)
1314    }
1315
1316    /// Make a trait impl from a hax `VirtualTraitImpl`. Used for constructing fake trait impls for
1317    /// builtin types like `FnOnce`.
1318    #[tracing::instrument(skip(self, item_meta))]
1319    pub fn translate_virtual_trait_impl(
1320        &mut self,
1321        def_id: TraitImplId,
1322        item_meta: ItemMeta,
1323        vimpl: &hax::VirtualTraitImpl,
1324    ) -> Result<TraitImpl, Error> {
1325        let span = item_meta.span;
1326        let trait_def = self.hax_def(&vimpl.trait_pred.trait_ref)?;
1327        let hax::FullDefKind::Trait {
1328            items: trait_items, ..
1329        } = trait_def.kind()
1330        else {
1331            panic!()
1332        };
1333
1334        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
1335        let implied_trait_refs =
1336            self.translate_trait_impl_exprs(span, &vimpl.implied_impl_exprs)?;
1337
1338        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
1339        // Monomorphic traits have no associated types.
1340        if !self.monomorphize() {
1341            let type_items = trait_items
1342                .iter()
1343                .filter(|assoc| matches!(assoc.kind, hax::AssocKind::Type { .. }));
1344            for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) {
1345                let assoc_type_id =
1346                    self.translate_assoc_type_id(implemented_trait.id, &assoc.def_id)?;
1347                let assoc_ty = TraitAssocTyImpl {
1348                    value: self.translate_ty(span, ty)?,
1349                    implied_trait_refs: self.translate_trait_impl_exprs(span, impl_exprs)?,
1350                };
1351                let binder_kind = BinderKind::TraitType(implemented_trait.id, assoc_type_id);
1352                types.set_slot_extend(assoc_type_id, Binder::empty(binder_kind, assoc_ty));
1353            }
1354        }
1355
1356        let generics = self.the_only_binder().params.clone();
1357        Ok(TraitImpl {
1358            def_id,
1359            item_meta,
1360            impl_trait: implemented_trait,
1361            generics,
1362            implied_trait_refs,
1363            consts: IndexMap::new(),
1364            types,
1365            methods: IndexMap::new(),
1366            // TODO(dyn): generate vtable instances for builtin traits
1367            vtable: None,
1368        })
1369    }
1370
1371    /// In case an impl does not override a trait method, this duplicates the original trait method
1372    /// and adjusts its generics to make the corresponding impl method.
1373    #[tracing::instrument(skip(self, item_meta, def))]
1374    pub fn translate_defaulted_method(
1375        &mut self,
1376        def_id: FunDeclId,
1377        item_meta: ItemMeta,
1378        def: &hax::FullDef<'tcx>,
1379        impl_kind: TraitImplSource,
1380        method_id: TraitMethodId,
1381    ) -> Result<FunDecl, Error> {
1382        let span = item_meta.span;
1383
1384        let hax::FullDefKind::TraitImpl { trait_pred, .. } = &def.kind else {
1385            unreachable!()
1386        };
1387
1388        // Retrieve the information about the implemented trait.
1389        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
1390        // A `TraitRef` that points to this impl with the correct generics.
1391        let self_impl_ref = self.translate_trait_impl_ref(span, def.this(), impl_kind)?;
1392        let self_predicate_kind = TraitRefKind::TraitImpl(self_impl_ref.clone());
1393
1394        // Build a reference to the original declared method.
1395        let ItemRef::TraitDecl(tdecl) = self.get_or_translate(implemented_trait.id.into())? else {
1396            panic!()
1397        };
1398        let Some(bound_method) = tdecl.methods.get(method_id) else {
1399            let method_name = self
1400                .translated
1401                .assoc_item_name(implemented_trait.id, method_id);
1402            raise_error!(
1403                self,
1404                span,
1405                "Could not find a method with name \
1406                `{method_name}` in trait `{:?}`",
1407                trait_pred.trait_ref.def_id,
1408            )
1409        };
1410        let bound_fn_ref: Binder<FunDeclRef> = bound_method
1411            .clone()
1412            .substitute_with_self(&implemented_trait.generics, &self_predicate_kind)
1413            .map(|m| m.item);
1414
1415        // Now we need to create the generic params for the new method. These are the concatenation
1416        // of the impl params and the method params. We obtain that by making the two existing
1417        // binders explicit and using `binder.flatten()`.
1418        let bound_fn_ref: Binder<Binder<FunDeclRef>> = Binder {
1419            params: self.outermost_generics().clone(),
1420            skip_binder: bound_fn_ref,
1421            kind: BinderKind::Other,
1422        };
1423        let bound_fn_ref: Binder<FunDeclRef> = bound_fn_ref.flatten();
1424
1425        // Create a copy of the provided method with the new generics.
1426        let original_method_id = bound_fn_ref.skip_binder.id;
1427        let ItemRef::Fun(fun_decl) = self.get_or_translate(original_method_id.into())? else {
1428            panic!()
1429        };
1430        let mut fun_decl = fun_decl
1431            .clone()
1432            .substitute_params(bound_fn_ref.map(|x| *x.generics));
1433
1434        // Update the rest of the data.
1435        fun_decl.def_id = def_id;
1436        // We use the span of the *impl*, not the span of the default method in the
1437        // original trait declaration.
1438        fun_decl.item_meta = ItemMeta {
1439            name: item_meta.name,
1440            opacity: item_meta.opacity,
1441            is_local: item_meta.is_local,
1442            span: item_meta.span,
1443            source_text: fun_decl.item_meta.source_text,
1444            attr_info: fun_decl.item_meta.attr_info,
1445            lang_item: fun_decl.item_meta.lang_item,
1446        };
1447        fun_decl.src = if let ItemSource::TraitDecl {
1448            trait_ref, item_id, ..
1449        } = fun_decl.src
1450        {
1451            ItemSource::TraitImpl {
1452                impl_ref: self_impl_ref.clone(),
1453                trait_ref,
1454                item_id,
1455                reuses_default: true,
1456            }
1457        } else {
1458            unreachable!()
1459        };
1460        if !item_meta.opacity.is_transparent() {
1461            fun_decl.body = Body::Opaque;
1462        }
1463
1464        Ok(fun_decl)
1465    }
1466}
charon_driver/translate/translate_items.rs

charon_driver/translate/
translate_items.rs
