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

charon_driver/translate/
translate_items.rs
