charon_driver/translate/
translate_items.rs

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

charon_driver/translate/
translate_items.rs
