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

charon_driver/translate/
translate_items.rs
