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

charon_driver/translate/
translate_items.rs
