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

charon_driver/translate/
translate_items.rs
