charon_driver/translate/
translate_items.rs

1use super::translate_bodies::BodyTransCtx;
2use super::translate_crate::*;
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use charon_lib::formatter::IntoFormatter;
6use charon_lib::pretty::FmtWithCtx;
7use derive_generic_visitor::Visitor;
8use itertools::Itertools;
9use std::mem;
10use std::ops::ControlFlow;
11
12impl<'tcx, 'ctx> TranslateCtx<'tcx> {
13    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
14        let trans_id = self.register_no_enqueue(&None, item_src);
15        let def_id = item_src.def_id();
16        if let Some(trans_id) = trans_id {
17            if self.translate_stack.contains(&trans_id) {
18                register_error!(
19                    self,
20                    Span::dummy(),
21                    "Cycle detected while translating {def_id:?}! Stack: {:?}",
22                    &self.translate_stack
23                );
24                return;
25            } else {
26                self.translate_stack.push(trans_id);
27            }
28        }
29        self.with_def_id(def_id, trans_id, |mut ctx| {
30            let span = ctx.def_span(def_id);
31            // Catch cycles
32            let res = {
33                // Stopgap measure because there are still many panics in charon and hax.
34                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
35                std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
36            };
37            match res {
38                Ok(Ok(())) => return,
39                // Translation error
40                Ok(Err(_)) => {
41                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
42                }
43                // Panic
44                Err(_) => register_error!(
45                    ctx,
46                    span,
47                    "Thread panicked when extracting item `{def_id:?}`."
48                ),
49            };
50        });
51        // We must be careful not to early-return from this function to not unbalance the stack.
52        self.translate_stack.pop();
53    }
54
55    pub(crate) fn translate_item_aux(
56        &mut self,
57        item_src: &TransItemSource,
58        trans_id: Option<AnyTransId>,
59    ) -> Result<(), Error> {
60        // Translate the meta information
61        let name = self.translate_name(item_src)?;
62        if let Some(trans_id) = trans_id {
63            self.translated.item_names.insert(trans_id, name.clone());
64        }
65        let opacity = self.opacity_for_name(&name);
66        if opacity.is_invisible() {
67            // Don't even start translating the item. In particular don't call `hax_def` on it.
68            return Ok(());
69        }
70        let def = self.hax_def_for_item(&item_src.item)?;
71        let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
72
73        // Initialize the item translation context
74        let mut bt_ctx = ItemTransCtx::new(item_src.clone(), trans_id, self);
75        match &item_src.kind {
76            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module => {
77                bt_ctx.register_module(item_meta, &def);
78            }
79            TransItemSourceKind::Type => {
80                let Some(AnyTransId::Type(id)) = trans_id else {
81                    unreachable!()
82                };
83                let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
84                self.translated.type_decls.set_slot(id, ty);
85            }
86            TransItemSourceKind::Fun => {
87                let Some(AnyTransId::Fun(id)) = trans_id else {
88                    unreachable!()
89                };
90                let fun_decl = bt_ctx.translate_function(id, item_meta, &def)?;
91                self.translated.fun_decls.set_slot(id, fun_decl);
92            }
93            TransItemSourceKind::Global => {
94                let Some(AnyTransId::Global(id)) = trans_id else {
95                    unreachable!()
96                };
97                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
98                self.translated.global_decls.set_slot(id, global_decl);
99            }
100            TransItemSourceKind::TraitDecl => {
101                let Some(AnyTransId::TraitDecl(id)) = trans_id else {
102                    unreachable!()
103                };
104                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
105                self.translated.trait_decls.set_slot(id, trait_decl);
106            }
107            TransItemSourceKind::TraitImpl(kind) => {
108                let Some(AnyTransId::TraitImpl(id)) = trans_id else {
109                    unreachable!()
110                };
111                let trait_impl = match kind {
112                    TraitImplSource::Normal => bt_ctx.translate_trait_impl(id, item_meta, &def)?,
113                    TraitImplSource::TraitAlias => {
114                        bt_ctx.translate_trait_alias_blanket_impl(id, item_meta, &def)?
115                    }
116                    &TraitImplSource::Closure(kind) => {
117                        bt_ctx.translate_closure_trait_impl(id, item_meta, &def, kind)?
118                    }
119                    TraitImplSource::DropGlue => bt_ctx.translate_drop_impl(id, item_meta, &def)?,
120                };
121                self.translated.trait_impls.set_slot(id, trait_impl);
122            }
123            &TransItemSourceKind::ClosureMethod(kind) => {
124                let Some(AnyTransId::Fun(id)) = trans_id else {
125                    unreachable!()
126                };
127                let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, kind)?;
128                self.translated.fun_decls.set_slot(id, fun_decl);
129            }
130            TransItemSourceKind::ClosureAsFnCast => {
131                let Some(AnyTransId::Fun(id)) = trans_id else {
132                    unreachable!()
133                };
134                let fun_decl = bt_ctx.translate_stateless_closure_as_fn(id, item_meta, &def)?;
135                self.translated.fun_decls.set_slot(id, fun_decl);
136            }
137            TransItemSourceKind::DropGlueMethod => {
138                let Some(AnyTransId::Fun(id)) = trans_id else {
139                    unreachable!()
140                };
141                let fun_decl = bt_ctx.translate_drop_method(id, item_meta, &def)?;
142                self.translated.fun_decls.set_slot(id, fun_decl);
143            }
144            TransItemSourceKind::VTable => {
145                let Some(AnyTransId::Type(id)) = trans_id else {
146                    unreachable!()
147                };
148                let ty_decl = bt_ctx.translate_vtable_struct(id, item_meta, &def)?;
149                self.translated.type_decls.set_slot(id, ty_decl);
150            }
151            TransItemSourceKind::VTableInstance(impl_kind) => {
152                let Some(AnyTransId::Global(id)) = trans_id else {
153                    unreachable!()
154                };
155                let global_decl =
156                    bt_ctx.translate_vtable_instance(id, item_meta, &def, impl_kind)?;
157                self.translated.global_decls.set_slot(id, global_decl);
158            }
159            TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
160                let Some(AnyTransId::Fun(id)) = trans_id else {
161                    unreachable!()
162                };
163                let fun_decl =
164                    bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?;
165                self.translated.fun_decls.set_slot(id, fun_decl);
166            }
167            TransItemSourceKind::VTableMethod => {
168                // let Some(AnyTransId::Fun(id)) = trans_id else {
169                //     unreachable!()
170                // };
171                // let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
172                // self.translated.fun_decls.set_slot(id, fun_decl);
173            }
174        }
175        Ok(())
176    }
177
178    /// While translating an item you may need the contents of another. Use this to retreive the
179    /// translated version of this item. Use with care as this could create cycles.
180    pub(crate) fn get_or_translate(&mut self, id: AnyTransId) -> Result<AnyTransItem<'_>, Error> {
181        // We have to call `get_item` a few times because we're running into the classic `Polonius`
182        // problem case.
183        if self.translated.get_item(id).is_none() {
184            let item_source = self.reverse_id_map.get(&id).unwrap().clone();
185            self.translate_item(&item_source);
186            if self.translated.get_item(id).is_none() {
187                let span = self.def_span(item_source.def_id());
188                raise_error!(self, span, "Failed to translate item {id:?}.")
189            }
190        }
191        let item = self.translated.get_item(id);
192        Ok(item.unwrap())
193    }
194}
195
196impl ItemTransCtx<'_, '_> {
197    /// Register the items inside this module or inherent impl.
198    // TODO: we may want to accumulate the set of modules we found, to check that all
199    // the opaque modules given as arguments actually exist
200    #[tracing::instrument(skip(self, item_meta))]
201    pub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) {
202        if !item_meta.opacity.is_transparent() {
203            return;
204        }
205        match def.kind() {
206            hax::FullDefKind::InherentImpl { items, .. } => {
207                for assoc in items {
208                    self.t_ctx.enqueue_module_item(&assoc.def_id);
209                }
210            }
211            hax::FullDefKind::Mod { items, .. } => {
212                for (_, def_id) in items {
213                    self.t_ctx.enqueue_module_item(def_id);
214                }
215            }
216            hax::FullDefKind::ForeignMod { items, .. } => {
217                for def_id in items {
218                    self.t_ctx.enqueue_module_item(def_id);
219                }
220            }
221            _ => panic!("Item should be a module but isn't: {def:?}"),
222        }
223    }
224
225    pub(crate) fn get_item_kind(
226        &mut self,
227        span: Span,
228        def: &hax::FullDef,
229    ) -> Result<ItemKind, Error> {
230        let assoc = match def.kind() {
231            hax::FullDefKind::AssocTy {
232                associated_item, ..
233            }
234            | hax::FullDefKind::AssocConst {
235                associated_item, ..
236            }
237            | hax::FullDefKind::AssocFn {
238                associated_item, ..
239            } => associated_item,
240            hax::FullDefKind::Closure { args, .. } => {
241                let info = self.translate_closure_info(span, args)?;
242                return Ok(ItemKind::Closure { info });
243            }
244            _ => return Ok(ItemKind::TopLevel),
245        };
246        Ok(match &assoc.container {
247            // E.g.:
248            // ```
249            // impl<T> List<T> {
250            //   fn new() -> Self { ... } <- inherent method
251            // }
252            // ```
253            hax::AssocItemContainer::InherentImplContainer { .. } => ItemKind::TopLevel,
254            // E.g.:
255            // ```
256            // impl Foo for Bar {
257            //   fn baz(...) { ... } // <- implementation of a trait method
258            // }
259            // ```
260            hax::AssocItemContainer::TraitImplContainer {
261                impl_,
262                implemented_trait_ref,
263                implemented_trait_item,
264                overrides_default,
265                ..
266            } => {
267                let impl_ref =
268                    self.translate_trait_impl_ref(span, impl_, TraitImplSource::Normal)?;
269                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
270                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
271                    // Ensure we translate the corresponding decl signature.
272                    // FIXME(self_clause): also ensure we translate associated globals
273                    // consistently; to do once we have clearer `Self` clause handling.
274                    let _: FunDeclId =
275                        self.register_item(span, implemented_trait_item, TransItemSourceKind::Fun);
276                }
277                let item_name = self.t_ctx.translate_trait_item_name(def.def_id())?;
278                ItemKind::TraitImpl {
279                    impl_ref,
280                    trait_ref,
281                    item_name,
282                    reuses_default: !overrides_default,
283                }
284            }
285            // This method is the *declaration* of a trait item
286            // E.g.:
287            // ```
288            // trait Foo {
289            //   fn baz(...); // <- declaration of a trait method
290            // }
291            // ```
292            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
293                // The trait id should be Some(...): trait markers (that we may eliminate)
294                // don't have associated items.
295                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
296                let item_name = self.t_ctx.translate_trait_item_name(def.def_id())?;
297                ItemKind::TraitDecl {
298                    trait_ref,
299                    item_name,
300                    has_default: assoc.has_value,
301                }
302            }
303        })
304    }
305
306    /// Translate a type definition.
307    ///
308    /// Note that we translate the types one by one: we don't need to take into
309    /// account the fact that some types are mutually recursive at this point
310    /// (we will need to take that into account when generating the code in a file).
311    #[tracing::instrument(skip(self, item_meta))]
312    pub fn translate_type_decl(
313        mut self,
314        trans_id: TypeDeclId,
315        item_meta: ItemMeta,
316        def: &hax::FullDef,
317    ) -> Result<TypeDecl, Error> {
318        let span = item_meta.span;
319
320        // Translate generics and predicates
321        self.translate_def_generics(span, def)?;
322
323        // Get the kind of the type decl -- is it a closure?
324        let src = self.get_item_kind(span, def)?;
325
326        // Translate type body
327        let kind = match &def.kind {
328            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
329            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
330            hax::FullDefKind::TyAlias { ty, .. } => {
331                // Don't error on missing trait refs.
332                self.error_on_impl_expr_error = false;
333                self.translate_ty(span, ty).map(TypeDeclKind::Alias)
334            }
335            hax::FullDefKind::Adt { .. } => self.translate_adt_def(trans_id, span, &item_meta, def),
336            hax::FullDefKind::Closure { args, .. } => {
337                self.translate_closure_adt(trans_id, span, &args)
338            }
339            _ => panic!("Unexpected item when translating types: {def:?}"),
340        };
341
342        let kind = match kind {
343            Ok(kind) => kind,
344            Err(err) => TypeDeclKind::Error(err.msg),
345        };
346        let layout = self.translate_layout(def.this());
347        let ptr_metadata = self.translate_ptr_metadata(def.this());
348        let type_def = TypeDecl {
349            def_id: trans_id,
350            item_meta,
351            generics: self.into_generics(),
352            kind,
353            src,
354            layout,
355            ptr_metadata,
356        };
357
358        Ok(type_def)
359    }
360
361    /// Translate one function.
362    #[tracing::instrument(skip(self, item_meta))]
363    pub fn translate_function(
364        mut self,
365        def_id: FunDeclId,
366        item_meta: ItemMeta,
367        def: &hax::FullDef,
368    ) -> Result<FunDecl, Error> {
369        trace!("About to translate function:\n{:?}", def.def_id());
370        let span = item_meta.span;
371
372        // Translate the function signature
373        trace!("Translating function signature");
374        let signature = self.translate_function_signature(def, &item_meta)?;
375
376        // Check whether this function is a method declaration for a trait definition.
377        // If this is the case, it shouldn't contain a body.
378        let kind = self.get_item_kind(span, def)?;
379        let is_trait_method_decl_without_default = match &kind {
380            ItemKind::TraitDecl { has_default, .. } => !has_default,
381            _ => false,
382        };
383
384        let is_global_initializer = matches!(
385            def.kind(),
386            hax::FullDefKind::Const { .. }
387                | hax::FullDefKind::AssocConst { .. }
388                | hax::FullDefKind::Static { .. }
389        );
390        let is_global_initializer = is_global_initializer
391            .then(|| self.register_item(span, def.this(), TransItemSourceKind::Global));
392
393        let body = if item_meta.opacity.with_private_contents().is_opaque()
394            || is_trait_method_decl_without_default
395        {
396            Err(Opaque)
397        } else if let hax::FullDefKind::Ctor {
398            adt_def_id,
399            ctor_of,
400            variant_id,
401            fields,
402            output_ty,
403            ..
404        } = def.kind()
405        {
406            let body = self.build_ctor_body(
407                span,
408                def,
409                adt_def_id,
410                ctor_of,
411                *variant_id,
412                fields,
413                output_ty,
414            )?;
415            Ok(body)
416        } else {
417            // Translate the body. This doesn't store anything if we can't/decide not to translate
418            // this body.
419            let mut bt_ctx = BodyTransCtx::new(&mut self);
420            match bt_ctx.translate_def_body(item_meta.span, def) {
421                Ok(Ok(body)) => Ok(body),
422                // Opaque declaration
423                Ok(Err(Opaque)) => Err(Opaque),
424                // Translation error.
425                // FIXME: handle error cases more explicitly.
426                Err(_) => Err(Opaque),
427            }
428        };
429        Ok(FunDecl {
430            def_id,
431            item_meta,
432            signature,
433            kind,
434            is_global_initializer,
435            body,
436        })
437    }
438
439    /// Translate one global.
440    #[tracing::instrument(skip(self, item_meta))]
441    pub fn translate_global(
442        mut self,
443        def_id: GlobalDeclId,
444        item_meta: ItemMeta,
445        def: &hax::FullDef,
446    ) -> Result<GlobalDecl, Error> {
447        trace!("About to translate global:\n{:?}", def.def_id());
448        let span = item_meta.span;
449
450        // Translate the generics and predicates - globals *can* have generics
451        // Ex.:
452        // ```
453        // impl<const N : usize> Foo<N> {
454        //   const LEN : usize = N;
455        // }
456        // ```
457        self.translate_def_generics(span, def)?;
458
459        // Retrieve the kind
460        let item_kind = self.get_item_kind(span, def)?;
461
462        trace!("Translating global type");
463        let ty = match &def.kind {
464            hax::FullDefKind::Const { ty, .. }
465            | hax::FullDefKind::AssocConst { ty, .. }
466            | hax::FullDefKind::Static { ty, .. } => ty,
467            _ => panic!("Unexpected def for constant: {def:?}"),
468        };
469        let ty = self.translate_ty(span, ty)?;
470
471        let global_kind = match &def.kind {
472            hax::FullDefKind::Static { .. } => GlobalKind::Static,
473            hax::FullDefKind::Const {
474                kind: hax::ConstKind::TopLevel,
475                ..
476            }
477            | hax::FullDefKind::AssocConst { .. } => GlobalKind::NamedConst,
478            hax::FullDefKind::Const { .. } => GlobalKind::AnonConst,
479            _ => panic!("Unexpected def for constant: {def:?}"),
480        };
481
482        let initializer = self.register_item(span, def.this(), TransItemSourceKind::Fun);
483
484        Ok(GlobalDecl {
485            def_id,
486            item_meta,
487            generics: self.into_generics(),
488            ty,
489            kind: item_kind,
490            global_kind,
491            init: initializer,
492        })
493    }
494
495    #[tracing::instrument(skip(self, item_meta))]
496    pub fn translate_trait_decl(
497        mut self,
498        def_id: TraitDeclId,
499        item_meta: ItemMeta,
500        def: &hax::FullDef,
501    ) -> Result<TraitDecl, Error> {
502        trace!("About to translate trait decl:\n{:?}", def.def_id());
503        trace!("Trait decl id:\n{:?}", def_id);
504
505        let span = item_meta.span;
506
507        // Translate the generics
508        // Note that in the generics returned by [translate_def_generics], the trait refs only
509        // contain the local trait clauses. The parent clauses are stored in
510        // `self.parent_trait_clauses`.
511        self.translate_def_generics(span, def)?;
512
513        let (hax::FullDefKind::Trait {
514            implied_predicates, ..
515        }
516        | hax::FullDefKind::TraitAlias {
517            implied_predicates, ..
518        }) = def.kind()
519        else {
520            raise_error!(self, span, "Unexpected definition: {def:?}");
521        };
522
523        // Register implied predicates.
524        let mut preds =
525            self.translate_predicates(implied_predicates, PredicateOrigin::WhereClauseOnTrait)?;
526        let parent_clauses = mem::take(&mut preds.trait_clauses);
527        // Consider the other predicates as required since the distinction doesn't matter for
528        // non-trait-clauses.
529        self.innermost_generics_mut().take_predicates_from(preds);
530
531        let vtable = self.translate_vtable_struct_ref(span, def.this())?;
532
533        if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
534            // Trait aliases don't have any items. Everything interesting is in the parent clauses.
535            return Ok(TraitDecl {
536                def_id,
537                item_meta,
538                parent_clauses,
539                generics: self.into_generics(),
540                consts: Default::default(),
541                types: Default::default(),
542                methods: Default::default(),
543                vtable,
544            });
545        }
546
547        let hax::FullDefKind::Trait {
548            items,
549            self_predicate,
550            ..
551        } = &def.kind
552        else {
553            unreachable!()
554        };
555        let self_trait_ref = TraitRef {
556            kind: TraitRefKind::SelfId,
557            trait_decl_ref: RegionBinder::empty(
558                self.translate_trait_predicate(span, self_predicate)?,
559            ),
560        };
561        let items: Vec<(TraitItemName, &hax::AssocItem)> = items
562            .iter()
563            .map(|item| -> Result<_, Error> {
564                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
565                Ok((name, item))
566            })
567            .try_collect()?;
568
569        // Translate the associated items
570        // We do something subtle here: TODO: explain
571        let mut consts = Vec::new();
572        let mut types = Vec::new();
573        let mut methods = Vec::new();
574        for (item_name, hax_item) in &items {
575            let item_def_id = &hax_item.def_id;
576            let item_span = self.def_span(item_def_id);
577
578            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
579            // polymorphic item as usual.
580            let trans_kind = match hax_item.kind {
581                hax::AssocKind::Fn { .. } => TransItemSourceKind::Fun,
582                hax::AssocKind::Const { .. } => TransItemSourceKind::Global,
583                hax::AssocKind::Type { .. } => TransItemSourceKind::Type,
584            };
585            let poly_item_def = self.poly_hax_def(item_def_id)?;
586            let (item_src, item_def) = if self.monomorphize() {
587                if poly_item_def.has_own_generics() {
588                    // Skip items that have generics of their own (as rustc defines these). This
589                    // skips GAT and generic methods. This does not skip methods with late-bound
590                    // lifetimes as these aren't considered generic arguments to the method itself
591                    // by rustc.
592                    continue;
593                } else {
594                    let item = def.this().with_def_id(self.hax_state(), item_def_id);
595                    let item_def = self.hax_def(&item)?;
596                    let item_src = TransItemSource::monomorphic(&item, trans_kind);
597                    (item_src, item_def)
598                }
599            } else {
600                let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
601                (item_src, poly_item_def)
602            };
603
604            match item_def.kind() {
605                hax::FullDefKind::AssocFn { .. } => {
606                    let binder_kind = BinderKind::TraitMethod(def_id, item_name.clone());
607                    let mut method = self.translate_binder_for_def(
608                        item_span,
609                        binder_kind,
610                        &item_def,
611                        |bt_ctx| {
612                            // If the trait is opaque, we only translate the signature of a method
613                            // with default body if it's overridden or used somewhere else.
614                            // We insert the `Binder<FunDeclRef>` unconditionally here, and remove
615                            // the ones that correspond to untranslated functions in the
616                            // `remove_unused_methods` pass.
617                            // FIXME: this triggers the translation of traits used in the method
618                            // clauses, despite the fact that we may end up not needing them.
619                            let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
620                                || item_meta.opacity.is_transparent()
621                                || !hax_item.has_value
622                            {
623                                bt_ctx.register_and_enqueue(item_span, item_src)
624                            } else {
625                                bt_ctx.register_no_enqueue(item_span, &item_src)
626                            };
627
628                            assert_eq!(bt_ctx.binding_levels.len(), 2);
629                            let fun_generics = bt_ctx
630                                .outermost_binder()
631                                .params
632                                .identity_args_at_depth(DeBruijnId::one())
633                                .concat(
634                                    &bt_ctx
635                                        .innermost_binder()
636                                        .params
637                                        .identity_args_at_depth(DeBruijnId::zero()),
638                                );
639                            let fn_ref = FunDeclRef {
640                                id: fun_id,
641                                generics: Box::new(fun_generics),
642                            };
643                            Ok(TraitMethod {
644                                name: item_name.clone(),
645                                item: fn_ref,
646                            })
647                        },
648                    )?;
649                    // In hax, associated items take an extra explicit `Self: Trait` clause, but we
650                    // don't want that to be part of the method clauses. Hence we remove the first
651                    // bound clause and replace its uses with references to the ambient `Self`
652                    // clause available in trait declarations.
653                    if !self.monomorphize() {
654                        struct ReplaceSelfVisitor;
655                        impl VarsVisitor for ReplaceSelfVisitor {
656                            fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
657                                if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
658                                    // Replace clause 0 and decrement the others.
659                                    Some(if let Some(new_id) = clause_id.index().checked_sub(1) {
660                                        TraitRefKind::Clause(DeBruijnVar::Bound(
661                                            DeBruijnId::ZERO,
662                                            TraitClauseId::new(new_id),
663                                        ))
664                                    } else {
665                                        TraitRefKind::SelfId
666                                    })
667                                } else {
668                                    None
669                                }
670                            }
671                        }
672                        method.params.visit_vars(&mut ReplaceSelfVisitor);
673                        method.skip_binder.visit_vars(&mut ReplaceSelfVisitor);
674                        method
675                            .params
676                            .trait_clauses
677                            .remove_and_shift_ids(TraitClauseId::ZERO);
678                        method.params.trait_clauses.iter_mut().for_each(|clause| {
679                            clause.clause_id -= 1;
680                        });
681                    }
682                    methods.push(method);
683                }
684                hax::FullDefKind::AssocConst { ty, .. } => {
685                    // Check if the constant has a value (i.e., a body).
686                    let default = hax_item.has_value.then(|| {
687                        // The parameters of the constant are the same as those of the item that
688                        // declares them.
689                        let id = self.register_and_enqueue(item_span, item_src);
690                        let mut generics = self.the_only_binder().params.identity_args();
691                        generics.trait_refs.push(self_trait_ref.clone());
692                        GlobalDeclRef {
693                            id,
694                            generics: Box::new(generics),
695                        }
696                    });
697                    let ty = self.translate_ty(item_span, ty)?;
698                    consts.push(TraitAssocConst {
699                        name: item_name.clone(),
700                        ty,
701                        default,
702                    });
703                }
704                // Monomorphic traits need no associated types.
705                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
706                hax::FullDefKind::AssocTy {
707                    value,
708                    implied_predicates,
709                    ..
710                } => {
711                    let binder_kind = BinderKind::TraitType(def_id, item_name.clone());
712                    let assoc_ty =
713                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
714                            // Also add the implied predicates.
715                            let mut preds = ctx.translate_predicates(
716                                &implied_predicates,
717                                PredicateOrigin::TraitItem(item_name.clone()),
718                            )?;
719                            let implied_clauses = mem::take(&mut preds.trait_clauses);
720                            // Consider the other predicates as required since the distinction doesn't
721                            // matter for non-trait-clauses.
722                            ctx.innermost_generics_mut().take_predicates_from(preds);
723
724                            let default = value
725                                .as_ref()
726                                .map(|ty| ctx.translate_ty(item_span, ty))
727                                .transpose()?;
728                            Ok(TraitAssocTy {
729                                name: item_name.clone(),
730                                default,
731                                implied_clauses,
732                            })
733                        })?;
734                    types.push(assoc_ty);
735                }
736                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
737            }
738        }
739
740        // In case of a trait implementation, some values may not have been
741        // provided, in case the declaration provided default values. We
742        // check those, and lookup the relevant values.
743        Ok(TraitDecl {
744            def_id,
745            item_meta,
746            parent_clauses,
747            generics: self.into_generics(),
748            consts,
749            types,
750            methods,
751            vtable,
752        })
753    }
754
755    #[tracing::instrument(skip(self, item_meta))]
756    pub fn translate_trait_impl(
757        mut self,
758        def_id: TraitImplId,
759        item_meta: ItemMeta,
760        def: &hax::FullDef,
761    ) -> Result<TraitImpl, Error> {
762        trace!("About to translate trait impl:\n{:?}", def.def_id());
763        trace!("Trait impl id:\n{:?}", def_id);
764
765        let span = item_meta.span;
766
767        self.translate_def_generics(span, def)?;
768
769        let hax::FullDefKind::TraitImpl {
770            trait_pred,
771            implied_impl_exprs,
772            items: impl_items,
773            ..
774        } = &def.kind
775        else {
776            unreachable!()
777        };
778
779        // Retrieve the information about the implemented trait.
780        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
781        let trait_id = implemented_trait.id;
782        // A `TraitRef` that points to this impl with the correct generics.
783        let self_predicate = TraitRef {
784            kind: TraitRefKind::TraitImpl(TraitImplRef {
785                id: def_id,
786                generics: Box::new(self.the_only_binder().params.identity_args()),
787            }),
788            trait_decl_ref: RegionBinder::empty(implemented_trait.clone()),
789        };
790
791        let vtable = self.translate_vtable_instance_ref(span, &trait_pred.trait_ref, def.this())?;
792
793        // The trait refs which implement the parent clauses of the implemented trait decl.
794        let parent_trait_refs = self.translate_trait_impl_exprs(span, &implied_impl_exprs)?;
795
796        {
797            // Debugging
798            let ctx = self.into_fmt();
799            let refs = parent_trait_refs
800                .iter()
801                .map(|c| c.with_ctx(&ctx))
802                .format("\n");
803            trace!(
804                "Trait impl: {:?}\n- parent_trait_refs:\n{}",
805                def.def_id(),
806                refs
807            );
808        }
809
810        // Explore the associated items
811        let mut consts = Vec::new();
812        let mut types = Vec::new();
813        let mut methods = Vec::new();
814
815        for impl_item in impl_items {
816            use hax::ImplAssocItemValue::*;
817            let name = self
818                .t_ctx
819                .translate_trait_item_name(&impl_item.decl_def_id)?;
820            let item_def_id = impl_item.def_id();
821            let item_span = self.def_span(item_def_id);
822            //
823            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
824            // polymorphic item as usual.
825            let poly_item_def = self.poly_hax_def(item_def_id)?;
826            let trans_kind = match poly_item_def.kind() {
827                hax::FullDefKind::AssocFn { .. } => TransItemSourceKind::Fun,
828                hax::FullDefKind::AssocConst { .. } => TransItemSourceKind::Global,
829                hax::FullDefKind::AssocTy { .. } => TransItemSourceKind::Type,
830                _ => unreachable!(),
831            };
832            let (item_src, item_def) = if self.monomorphize() {
833                if poly_item_def.has_own_generics() {
834                    continue;
835                } else {
836                    let item = match &impl_item.value {
837                        // Real item: we reuse the impl arguments to get a reference to the item.
838                        Provided { def_id, .. } => def.this().with_def_id(self.hax_state(), def_id),
839                        // Defaulted item: we use the implemented trait arguments.
840                        _ => trait_pred
841                            .trait_ref
842                            .with_def_id(self.hax_state(), &impl_item.decl_def_id),
843                    };
844                    let item_def = self.hax_def(&item)?;
845                    let item_src = TransItemSource::monomorphic(&item, trans_kind);
846                    (item_src, item_def)
847                }
848            } else {
849                let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
850                (item_src, poly_item_def)
851            };
852
853            match item_def.kind() {
854                hax::FullDefKind::AssocFn { .. } => {
855                    match &impl_item.value {
856                        Provided { is_override, .. } => {
857                            let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
858                            let fn_ref = self.translate_binder_for_def(
859                                item_span,
860                                binder_kind,
861                                &item_def,
862                                |bt_ctx| {
863                                    // If the impl is opaque, we only translate the signature of a
864                                    // method with a default body if it's directly used somewhere
865                                    // else.
866                                    // We insert the `Binder<FunDeclRef>` unconditionally here, and
867                                    // remove the ones that correspond to untranslated functions in
868                                    // the `remove_unused_methods` pass.
869                                    let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
870                                        || item_meta.opacity.is_transparent()
871                                        || !*is_override
872                                    {
873                                        bt_ctx.register_and_enqueue(item_span, item_src)
874                                    } else {
875                                        bt_ctx.register_no_enqueue(item_span, &item_src)
876                                    };
877
878                                    // TODO: there's probably a cleaner way to write this
879                                    assert_eq!(bt_ctx.binding_levels.len(), 2);
880                                    let fun_generics = bt_ctx
881                                        .outermost_binder()
882                                        .params
883                                        .identity_args_at_depth(DeBruijnId::one())
884                                        .concat(
885                                            &bt_ctx
886                                                .innermost_binder()
887                                                .params
888                                                .identity_args_at_depth(DeBruijnId::zero()),
889                                        );
890                                    Ok(FunDeclRef {
891                                        id: fun_id,
892                                        generics: Box::new(fun_generics),
893                                    })
894                                },
895                            )?;
896                            methods.push((name, fn_ref));
897                        }
898                        DefaultedFn { .. } => {
899                            // TODO: handle defaulted methods
900                        }
901                        _ => unreachable!(),
902                    }
903                }
904                hax::FullDefKind::AssocConst { .. } => {
905                    let id = self.register_and_enqueue(item_span, item_src);
906                    // The parameters of the constant are the same as those of the item that
907                    // declares them.
908                    let generics = match &impl_item.value {
909                        Provided { .. } => self.the_only_binder().params.identity_args(),
910                        _ => {
911                            let mut generics = implemented_trait.generics.as_ref().clone();
912                            generics.trait_refs.push(self_predicate.clone());
913                            generics
914                        }
915                    };
916                    let gref = GlobalDeclRef {
917                        id,
918                        generics: Box::new(generics),
919                    };
920                    consts.push((name, gref));
921                }
922                // Monomorphic traits have no associated types.
923                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
924                hax::FullDefKind::AssocTy { value, .. } => {
925                    let binder_kind = BinderKind::TraitType(trait_id, name.clone());
926                    let assoc_ty =
927                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
928                            let ty = match &impl_item.value {
929                                Provided { .. } => value.as_ref().unwrap(),
930                                DefaultedTy { ty, .. } => ty,
931                                _ => unreachable!(),
932                            };
933                            let ty = ctx.translate_ty(item_span, &ty)?;
934                            let implied_trait_refs = ctx.translate_trait_impl_exprs(
935                                item_span,
936                                &impl_item.required_impl_exprs,
937                            )?;
938                            Ok(TraitAssocTyImpl {
939                                value: ty,
940                                implied_trait_refs,
941                            })
942                        })?;
943                    types.push((name.clone(), assoc_ty));
944                }
945                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
946            }
947        }
948
949        Ok(TraitImpl {
950            def_id,
951            item_meta,
952            impl_trait: implemented_trait,
953            generics: self.into_generics(),
954            parent_trait_refs,
955            consts,
956            types,
957            methods,
958            vtable,
959        })
960    }
961
962    /// Generate a blanket impl for this trait, as in:
963    /// ```
964    ///     trait Alias<U> = Trait<Option<U>, Item = u32> + Clone;
965    /// ```
966    /// becomes:
967    /// ```
968    ///     trait Alias<U>: Trait<Option<U>, Item = u32> + Clone {}
969    ///     impl<U, Self: Trait<Option<U>, Item = u32> + Clone> Alias<U> for Self {}
970    /// ```
971    #[tracing::instrument(skip(self, item_meta))]
972    pub fn translate_trait_alias_blanket_impl(
973        mut self,
974        def_id: TraitImplId,
975        item_meta: ItemMeta,
976        def: &hax::FullDef,
977    ) -> Result<TraitImpl, Error> {
978        let span = item_meta.span;
979
980        self.translate_def_generics(span, def)?;
981
982        let hax::FullDefKind::TraitAlias {
983            implied_predicates, ..
984        } = &def.kind
985        else {
986            raise_error!(self, span, "Unexpected definition: {def:?}");
987        };
988
989        let trait_id = self.register_item(span, def.this(), TransItemSourceKind::TraitDecl);
990
991        // Register the trait implied clauses as required clauses for the impl.
992        assert!(self.innermost_generics_mut().trait_clauses.is_empty());
993        self.register_predicates(implied_predicates, PredicateOrigin::WhereClauseOnTrait)?;
994
995        let mut generics = self.the_only_binder().params.identity_args();
996        // Do the inverse operation: the trait considers the clauses as implied.
997        let parent_trait_refs = mem::take(&mut generics.trait_refs);
998        let implemented_trait = TraitDeclRef {
999            id: trait_id,
1000            generics: Box::new(generics),
1001        };
1002
1003        let mut timpl = TraitImpl {
1004            def_id,
1005            item_meta,
1006            impl_trait: implemented_trait,
1007            generics: self.the_only_binder().params.clone(),
1008            parent_trait_refs,
1009            consts: Default::default(),
1010            types: Default::default(),
1011            methods: Default::default(),
1012            // TODO(dyn)
1013            vtable: None,
1014        };
1015        // We got the predicates from a trait decl, so they may refer to the virtual `Self`
1016        // clause, which doesn't exist for impls. We fix that up here.
1017        {
1018            struct FixSelfVisitor {
1019                binder_depth: DeBruijnId,
1020            }
1021            struct UnhandledSelf;
1022            impl Visitor for FixSelfVisitor {
1023                type Break = UnhandledSelf;
1024            }
1025            impl VisitorWithBinderDepth for FixSelfVisitor {
1026                fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
1027                    &mut self.binder_depth
1028                }
1029            }
1030            impl VisitAstMut for FixSelfVisitor {
1031                fn visit<'a, T: AstVisitable>(&'a mut self, x: &mut T) -> ControlFlow<Self::Break> {
1032                    VisitWithBinderDepth::new(self).visit(x)
1033                }
1034                fn visit_trait_ref_kind(
1035                    &mut self,
1036                    kind: &mut TraitRefKind,
1037                ) -> ControlFlow<Self::Break> {
1038                    match kind {
1039                        TraitRefKind::SelfId => return ControlFlow::Break(UnhandledSelf),
1040                        TraitRefKind::ParentClause(sub, clause_id)
1041                            if matches!(sub.kind, TraitRefKind::SelfId) =>
1042                        {
1043                            *kind = TraitRefKind::Clause(DeBruijnVar::bound(
1044                                self.binder_depth,
1045                                *clause_id,
1046                            ))
1047                        }
1048                        _ => (),
1049                    }
1050                    self.visit_inner(kind)
1051                }
1052            }
1053            match timpl.drive_mut(&mut FixSelfVisitor {
1054                binder_depth: DeBruijnId::zero(),
1055            }) {
1056                ControlFlow::Continue(()) => {}
1057                ControlFlow::Break(UnhandledSelf) => {
1058                    register_error!(
1059                        self,
1060                        span,
1061                        "Found `Self` clause we can't handle \
1062                         in a trait alias blanket impl."
1063                    );
1064                }
1065            }
1066        };
1067
1068        Ok(timpl)
1069    }
1070
1071    /// Make a trait impl from a hax `VirtualTraitImpl`. Used for constructing fake trait impls for
1072    /// builtin types like `FnOnce`.
1073    #[tracing::instrument(skip(self, item_meta))]
1074    pub fn translate_virtual_trait_impl(
1075        &mut self,
1076        def_id: TraitImplId,
1077        item_meta: ItemMeta,
1078        vimpl: &hax::VirtualTraitImpl,
1079    ) -> Result<TraitImpl, Error> {
1080        let span = item_meta.span;
1081        let trait_def = self.hax_def(&vimpl.trait_pred.trait_ref)?;
1082        let hax::FullDefKind::Trait {
1083            items: trait_items, ..
1084        } = trait_def.kind()
1085        else {
1086            panic!()
1087        };
1088
1089        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
1090        let parent_trait_refs = self.translate_trait_impl_exprs(span, &vimpl.implied_impl_exprs)?;
1091
1092        let mut types = vec![];
1093        // Monomorphic traits have no associated types.
1094        if !self.monomorphize() {
1095            let type_items = trait_items.iter().filter(|assoc| match assoc.kind {
1096                hax::AssocKind::Type { .. } => true,
1097                _ => false,
1098            });
1099            for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) {
1100                let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?;
1101                let assoc_ty = TraitAssocTyImpl {
1102                    value: self.translate_ty(span, ty)?,
1103                    implied_trait_refs: self.translate_trait_impl_exprs(span, impl_exprs)?,
1104                };
1105                let binder_kind = BinderKind::TraitType(implemented_trait.id, name.clone());
1106                types.push((name, Binder::empty(binder_kind, assoc_ty)));
1107            }
1108        }
1109
1110        let generics = self.the_only_binder().params.clone();
1111        Ok(TraitImpl {
1112            def_id,
1113            item_meta,
1114            impl_trait: implemented_trait,
1115            generics,
1116            parent_trait_refs,
1117            consts: vec![],
1118            types,
1119            methods: vec![],
1120            // TODO(dyn): generate vtable instances for builtin traits
1121            vtable: None,
1122        })
1123    }
1124}
charon_driver/translate/translate_items.rs

charon_driver/translate/
translate_items.rs
