charon_driver/translate/
translate_items.rs

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

charon_driver/translate/
translate_items.rs
