charon_driver/translate/
translate_items.rs

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

charon_driver/translate/
translate_items.rs
