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

charon_driver/translate/
translate_items.rs
