charon_driver/translate/
translate_items.rs

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

charon_driver/translate/
translate_items.rs
