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

charon_driver/translate/
translate_items.rs
