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

charon_driver/translate/
translate_items.rs
