charon_driver/translate/
translate_items.rs

1use super::translate_crate::*;
2use super::translate_ctx::*;
3use crate::hax;
4use crate::hax::{BaseState, SInto, UnderOwnerState};
5use charon_lib::ast::*;
6use charon_lib::formatter::IntoFormatter;
7use charon_lib::options::ConstHandling;
8use charon_lib::pretty::FmtWithCtx;
9use derive_generic_visitor::Visitor;
10use itertools::Itertools;
11use rustc_middle::ty;
12use rustc_span::sym;
13use std::mem;
14use std::ops::ControlFlow;
15
16impl<'tcx> TranslateCtx<'tcx> {
17    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource<'tcx>) {
18        let _guard = charon_lib::timing::scope_lazy("translate-item", || {
19            let kind = format!("{:?}", item_src.kind);
20            kind.split('(').next().unwrap().to_owned()
21        });
22        let trans_id = self.register_no_enqueue(&None, item_src);
23        let def_id = item_src.def_id();
24        if self.translate_stack.contains(&trans_id) {
25            register_error!(
26                self,
27                Span::dummy(),
28                "Cycle detected while translating {def_id:?}! Stack: {:?}",
29                &self.translate_stack
30            );
31            return;
32        }
33        self.translate_stack.push(trans_id);
34        self.with_def_id(def_id, &trans_id, |mut ctx| {
35            let span = ctx.def_span(def_id);
36            // Catch cycles
37            let res = {
38                // Stopgap measure because there are still many panics in charon and hax.
39                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
40                std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
41            };
42            match res {
43                Ok(Ok(())) => return,
44                // Translation error
45                Ok(Err(_)) => {
46                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
47                }
48                // Panic
49                Err(_) => register_error!(
50                    ctx,
51                    span,
52                    "Thread panicked when extracting item `{def_id:?}`."
53                ),
54            };
55        });
56        if let Some(trans_id) = trans_id.as_item()
57            && self.errors.borrow().item_has_errors(trans_id)
58            && let Some(mut item) = self.translated.get_item_mut(trans_id)
59        {
60            item.item_meta().has_errors = true;
61        }
62        // We must be careful not to early-return from this function to not unbalance the stack.
63        self.translate_stack.pop();
64    }
65
66    pub(crate) fn translate_item_aux(
67        &mut self,
68        item_src: &TransItemSource<'tcx>,
69        trans_id: ItemOrModuleId,
70    ) -> Result<(), Error> {
71        // The name may have already been computed.
72        let name = match trans_id
73            .as_item()
74            .and_then(|id| self.translated.item_names.get(&id))
75        {
76            Some(name) => name.clone(),
77            None => {
78                let name = self.translate_name(item_src)?;
79                if let Some(trans_id) = trans_id.as_item() {
80                    self.translated.item_names.insert(trans_id, name.clone());
81                }
82                name
83            }
84        };
85        let opacity = self.opacity_for_name(&name);
86        if opacity.is_invisible() {
87            // Don't even start translating the item. In particular don't call `hax_def` on it.
88            return Ok(());
89        }
90        let def = self.hax_def_for_item(&item_src.item)?;
91        let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
92        if item_meta.opacity.is_invisible() {
93            return Ok(());
94        }
95
96        // For items in the current crate that have bodies, also enqueue items defined in that
97        // body.
98        if !item_meta.opacity.is_opaque()
99            && let Some(def_id) = def.def_id().as_real_def_id()
100            && let Some(ldid) = def_id.as_local()
101            && let node = self.tcx.hir_node_by_def_id(ldid)
102            && let Some(body_id) = node.body_id()
103        {
104            use rustc_hir::intravisit;
105            struct EnqueueNestedItems<'a, 'tcx> {
106                ctx: &'a mut TranslateCtx<'tcx>,
107                parent: ContainmentNode,
108            }
109            impl<'tcx> intravisit::Visitor<'tcx> for EnqueueNestedItems<'_, 'tcx> {
110                fn visit_nested_item(&mut self, id: rustc_hir::ItemId) {
111                    let def_id = id.owner_id.def_id.to_def_id();
112                    let def_id = def_id.sinto(&self.ctx.hax_state);
113                    self.ctx.enqueue_module_item(&def_id, self.parent);
114                }
115            }
116            let body = self.tcx.hir_body(body_id);
117            intravisit::walk_body(
118                &mut EnqueueNestedItems {
119                    ctx: self,
120                    parent: trans_id.into(),
121                },
122                body,
123            );
124        }
125
126        // Initialize the item translation context
127        let mut bt_ctx = ItemTransCtx::new(item_src.clone(), trans_id, self);
128        trace!(
129            "About to translate item `{:?}` as a {:?}; \
130            target_id={trans_id:?}, mono={}",
131            def.def_id(),
132            item_src.kind,
133            bt_ctx.monomorphize(),
134        );
135        if !matches!(
136            &item_src.kind,
137            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module,
138        ) {
139            bt_ctx.translate_item_generics(item_meta.span, &def, &item_src.kind)?;
140        }
141        match &item_src.kind {
142            TransItemSourceKind::InherentImpl | TransItemSourceKind::Module => {
143                bt_ctx.register_module(item_meta, &def);
144            }
145            TransItemSourceKind::Type => {
146                let id = trans_id.expect_item();
147                let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
148                self.translated.type_decls.set_slot(id, ty);
149            }
150            TransItemSourceKind::Fun | TransItemSourceKind::IntrinsicFallback => {
151                let id = trans_id.expect_item();
152                let fun_decl = bt_ctx.translate_fun_decl(id, item_meta, &def)?;
153                self.translated.fun_decls.set_slot(id, fun_decl);
154            }
155            TransItemSourceKind::Global => {
156                let id = trans_id.expect_item();
157                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
158                self.translated.global_decls.set_slot(id, global_decl);
159            }
160            TransItemSourceKind::TraitDecl => {
161                let id = trans_id.expect_item();
162                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
163                self.translated.trait_decls.set_slot(id, trait_decl);
164            }
165            TransItemSourceKind::TraitImpl(kind) => {
166                let id = trans_id.expect_item();
167                // In Mono mode, only user-defined trait is supported for now.
168                let trait_impl = match kind {
169                    TransImplSource::Normal => bt_ctx.translate_trait_impl(id, item_meta, &def)?,
170                    TransImplSource::TraitAlias => {
171                        bt_ctx.translate_trait_alias_blanket_impl(id, item_meta, &def)?
172                    }
173                    &TransImplSource::Callable(kind) => {
174                        bt_ctx.translate_closure_trait_impl(id, item_meta, &def, kind)?
175                    }
176                    TransImplSource::ImplicitDestruct => {
177                        bt_ctx.translate_implicit_destruct_impl(id, item_meta, &def)?
178                    }
179                    TransImplSource::Marker => {
180                        unreachable!("marker impls are only used as vtable item sources")
181                    }
182                };
183                self.translated.trait_impls.set_slot(id, trait_impl);
184            }
185            &TransItemSourceKind::CallableMethod(kind) => {
186                let id = trans_id.expect_item();
187                let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, kind)?;
188                self.translated.fun_decls.set_slot(id, fun_decl);
189            }
190            TransItemSourceKind::ClosureAsFnCast => {
191                let id = trans_id.expect_item();
192                let fun_decl = bt_ctx.translate_stateless_closure_as_fn(id, item_meta, &def)?;
193                self.translated.fun_decls.set_slot(id, fun_decl);
194            }
195            &TransItemSourceKind::DropGlueMethod(impl_kind) => {
196                let id = trans_id.expect_item();
197                let fun_decl = bt_ctx.translate_drop_glue_method(id, item_meta, &def, impl_kind)?;
198                self.translated.fun_decls.set_slot(id, fun_decl);
199            }
200            TransItemSourceKind::VTable => {
201                let id = trans_id.expect_item();
202                let ty_decl = bt_ctx.translate_vtable_struct(id, item_meta, &def)?;
203                self.translated.type_decls.set_slot(id, ty_decl);
204            }
205            &TransItemSourceKind::VTableInstance(impl_kind) => {
206                let id = trans_id.expect_item();
207                let global_decl =
208                    bt_ctx.translate_vtable_instance(id, item_meta, &def, impl_kind)?;
209                self.translated.global_decls.set_slot(id, global_decl);
210            }
211            &TransItemSourceKind::VTableMethod(impl_kind) => {
212                let id = trans_id.expect_item();
213                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?;
214                self.translated.fun_decls.set_slot(id, fun_decl);
215            }
216            &TransItemSourceKind::VTableDropShim(impl_kind) => {
217                let id = trans_id.expect_item();
218                let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def, impl_kind)?;
219                self.translated.fun_decls.set_slot(id, fun_decl);
220            }
221        }
222        Ok(())
223    }
224
225    /// While translating an item you may need the contents of another. Use this to retreive the
226    /// translated version of this item. Use with care as this could create cycles.
227    pub(crate) fn get_or_translate(&mut self, id: ItemId) -> Result<ItemRef<'_>, Error> {
228        // We have to call `get_item` a few times because we're running into the classic `Polonius`
229        // problem case.
230        if self.translated.get_item(id).is_none() {
231            let item_source = self.reverse_id_map.get(&id).unwrap().clone();
232            self.translate_item(&item_source);
233            if self.translated.get_item(id).is_none() {
234                let span = self.def_span(item_source.def_id());
235                let name = id.to_string_with_ctx(&self.into_fmt());
236                // Not a real error, its message won't be displayed.
237                return Err(Error {
238                    span,
239                    msg: format!("Failed to translate item {name}."),
240                });
241                // raise_error!(self, span, "Failed to translate item {name}.")
242            }
243            // Add to avoid the double translation of the same item
244            self.processed.insert(item_source.clone());
245        }
246        let item = self.translated.get_item(id);
247        Ok(item.unwrap())
248    }
249
250    /// Record that `method_id` is an implementation of the given method of the trait. If the
251    /// method is not used anywhere yet we simply record the implementation. If the method is used
252    /// then we enqueue it for translation.
253    pub fn register_method_impl(
254        &mut self,
255        trait_id: TraitDeclId,
256        method_id: TraitMethodId,
257        fun_id: FunDeclId,
258    ) {
259        match &mut self.method_status[trait_id][method_id] {
260            MethodStatus::Unused { implementors } => {
261                implementors.insert(fun_id);
262            }
263            MethodStatus::Used => {
264                self.enqueue_id(fun_id);
265            }
266        }
267    }
268
269    /// Mark the method as "used", which will enqueue for translation all the implementations of
270    /// that method.
271    pub fn mark_method_as_used(&mut self, trait_id: TraitDeclId, method_id: TraitMethodId) {
272        let old_status = mem::replace(
273            &mut self.method_status[trait_id][method_id],
274            MethodStatus::Used,
275        );
276        match old_status {
277            MethodStatus::Unused { implementors } => {
278                for fun_id in implementors {
279                    self.enqueue_id(fun_id);
280                }
281            }
282            MethodStatus::Used => {}
283        }
284    }
285
286    /// Keep only the methods we marked as "used".
287    pub fn remove_unused_methods(&mut self) {
288        let method_is_used = |trait_id: TraitDeclId, method_id: TraitMethodId| {
289            matches!(self.method_status[trait_id][method_id], MethodStatus::Used)
290        };
291        for tdecl in self.translated.trait_decls.iter_mut() {
292            tdecl
293                .methods
294                .retain(|i, _m| method_is_used(tdecl.def_id, i));
295        }
296        for timpl in self.translated.trait_impls.iter_mut() {
297            let trait_id = timpl.impl_trait.id;
298            timpl.methods.retain(|i, _m| method_is_used(trait_id, i));
299        }
300    }
301}
302
303enum TraitItemSource {
304    Default {
305        trait_ref: TraitDeclRef,
306        item_id: AssocItemId,
307    },
308    Impl {
309        impl_ref: TraitImplRef,
310        trait_ref: TraitDeclRef,
311        item_id: AssocItemId,
312        reuses_default: bool,
313    },
314}
315
316impl<'tcx> ItemTransCtx<'tcx, '_> {
317    /// Register the items inside this module or inherent impl.
318    // TODO: we may want to accumulate the set of modules we found, to check that all
319    // the opaque modules given as arguments actually exist
320    #[tracing::instrument(skip(self, item_meta, def))]
321    pub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef<'tcx>) {
322        if !item_meta.opacity.is_transparent() {
323            return;
324        }
325        let this: ContainmentNode = self.item_id.into();
326        match def.kind() {
327            hax::FullDefKind::InherentImpl(i) => {
328                for assoc in i.items(self.hax_state()) {
329                    self.t_ctx.enqueue_module_item(&assoc.def_id, this);
330                }
331            }
332            hax::FullDefKind::Mod(m) => {
333                for (_, def_id) in m.items(self.hax_state()) {
334                    self.t_ctx.enqueue_module_item(def_id, this);
335                }
336            }
337            hax::FullDefKind::ForeignMod(m) => {
338                for def_id in m.items() {
339                    self.t_ctx.enqueue_module_item(def_id, this);
340                }
341            }
342            _ => panic!("Item should be a module but isn't: {def:?}"),
343        }
344    }
345
346    fn get_trait_item_source(
347        &mut self,
348        span: Span,
349        def: &hax::FullDef<'tcx>,
350    ) -> Result<Option<TraitItemSource>, Error> {
351        let assoc = match def.kind() {
352            hax::FullDefKind::AssocConst(c) => c.associated_item(),
353            hax::FullDefKind::AssocFn(f) => f.associated_item(),
354            _ => return Ok(None),
355        };
356        Ok(Some(match &assoc.container {
357            // E.g.:
358            // ```
359            // impl<T> List<T> {
360            //   fn new() -> Self { ... } <- inherent method
361            // }
362            // ```
363            hax::AssocItemContainer::InherentImplContainer { .. } => return Ok(None),
364            // E.g.:
365            // ```
366            // impl Foo for Bar {
367            //   fn baz(...) { ... } // <- implementation of a trait method
368            // }
369            // ```
370            hax::AssocItemContainer::TraitImplContainer {
371                impl_,
372                implemented_trait_ref,
373                ..
374            } => {
375                let impl_ref =
376                    self.translate_trait_impl_ref(span, impl_, TransImplSource::Normal)?;
377                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
378                let item_id = self.translate_assoc_item_id(trait_ref.id, def.def_id())?;
379                if matches!(def.kind(), hax::FullDefKind::AssocFn(_)) {
380                    // If the implementation is getting translated, that means the method is
381                    // getting used.
382                    let method_id = *item_id.as_method().unwrap();
383                    self.mark_method_as_used(trait_ref.id, method_id);
384                }
385                TraitItemSource::Impl {
386                    impl_ref,
387                    trait_ref,
388                    item_id,
389                    reuses_default: false,
390                }
391            }
392            // This method is the *declaration* of a trait item
393            // E.g.:
394            // ```
395            // trait Foo {
396            //   fn baz(...); // <- declaration of a trait method
397            // }
398            // ```
399            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
400                // The trait id should be Some(...): trait markers (that we may eliminate)
401                // don't have associated items.
402                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
403                let item_id = self.translate_assoc_item_id(trait_ref.id, def.def_id())?;
404                if matches!(def.kind(), hax::FullDefKind::AssocFn(_)) {
405                    // If the method fundecl is getting translated, that means the method is
406                    // getting used.
407                    let method_id = *item_id.as_method().unwrap();
408                    self.mark_method_as_used(trait_ref.id, method_id);
409                }
410                debug_assert!(assoc.has_value);
411                TraitItemSource::Default { trait_ref, item_id }
412            }
413        }))
414    }
415
416    /// Translate a type definition.
417    ///
418    /// Note that we translate the types one by one: we don't need to take into
419    /// account the fact that some types are mutually recursive at this point
420    /// (we will need to take that into account when generating the code in a file).
421    #[tracing::instrument(skip(self, item_meta, def))]
422    pub fn translate_type_decl(
423        mut self,
424        trans_id: TypeDeclId,
425        item_meta: ItemMeta,
426        def: &hax::FullDef<'tcx>,
427    ) -> Result<TypeDecl, Error> {
428        let span = item_meta.span;
429
430        // Get the kind of the type decl.
431        let src = if let hax::FullDefKind::Closure(_) = def.kind() {
432            let info = self.translate_closure_info(span, def)?;
433            TypeSource::Closure { info }
434        } else if let Some(builtin) = self.recognize_builtin_adt(def.this()) {
435            TypeSource::Builtin(builtin)
436        } else {
437            TypeSource::Normal
438        };
439
440        // Translate type body
441        let kind = match &def.kind {
442            _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
443            hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
444            hax::FullDefKind::TyAlias(a) => {
445                // Don't error on missing trait refs.
446                self.error_on_trait_proof_error = false;
447                self.translate_ty(span, a.ty()).map(TypeDeclKind::Alias)
448            }
449            hax::FullDefKind::Adt(_) => self.translate_adt_def(trans_id, span, &item_meta, def),
450            hax::FullDefKind::Closure(c) => self.translate_closure_adt(span, c),
451            _ => panic!("Unexpected item when translating types: {def:?}"),
452        };
453
454        let kind = match kind {
455            Ok(kind) => kind,
456            Err(err) => TypeDeclKind::Error(err.msg),
457        };
458        let layout = self
459            .translate_layout(span, def, &kind)
460            .into_iter()
461            .map(|l| (self.get_target_triple(), l))
462            .collect();
463        let ptr_metadata = self.translate_ptr_metadata(span, def.this())?;
464        let marker_traits = self.outermost_generics().is_empty().then(|| {
465            let ty = def.type_of(&self.hax_state).unwrap();
466            let tcx = self.hax_state.base().tcx;
467            let typing_env = self.hax_state.typing_env();
468            let implements = |trait_id| {
469                let tref = ty::Binder::dummy(ty::TraitRef::new(tcx, trait_id, [ty]));
470                !hax::solve_trait(&self.hax_state, tref).kind.is_error()
471            };
472            Box::new(ImplementsMarkerTraits {
473                is_sized: ty.is_sized(tcx, typing_env),
474                is_send: implements(tcx.get_diagnostic_item(sym::Send).unwrap()),
475                is_sync: implements(tcx.lang_items().sync_trait().unwrap()),
476                is_freeze: ty.is_freeze(tcx, typing_env),
477                is_unpin: ty.is_unpin(tcx, typing_env),
478            })
479        });
480        Ok(TypeDecl {
481            def_id: trans_id,
482            item_meta,
483            generics: self.into_generics(),
484            kind,
485            src,
486            layout,
487            ptr_metadata,
488            marker_traits,
489        })
490    }
491
492    /// Translate one function.
493    #[tracing::instrument(skip(self, item_meta, def))]
494    pub fn translate_fun_decl(
495        mut self,
496        def_id: FunDeclId,
497        item_meta: ItemMeta,
498        def: &hax::FullDef<'tcx>,
499    ) -> Result<FunDecl, Error> {
500        let span = item_meta.span;
501
502        let src = if matches!(
503            def.kind(),
504            hax::FullDefKind::Const(_)
505                | hax::FullDefKind::AssocConst(_)
506                | hax::FullDefKind::Static(_)
507        ) {
508            let global_id = self.register_item(span, def.this(), TransItemSourceKind::Global);
509            FunSource::GlobalInitializer(GlobalDeclRef {
510                id: global_id,
511                generics: Box::new(self.outermost_generics().identity_args()),
512            })
513        } else if matches!(def.kind(), hax::FullDefKind::Ctor(_)) {
514            FunSource::AdtConstructor
515        } else if let hax::FullDefKind::AssocFn(f) = def.kind()
516            && let hax::AssocItemContainer::InherentImplContainer { self_ty, .. } =
517                &f.associated_item().container
518        {
519            FunSource::InherentImpl {
520                self_ty: self.translate_ty(span, self_ty)?,
521            }
522        } else {
523            match self.get_trait_item_source(span, def)? {
524                None => FunSource::Normal,
525                Some(TraitItemSource::Default { trait_ref, item_id }) => FunSource::TraitDefault {
526                    trait_ref,
527                    item_id: *item_id.as_method().unwrap(),
528                },
529                Some(TraitItemSource::Impl {
530                    impl_ref,
531                    trait_ref,
532                    item_id,
533                    reuses_default,
534                }) => FunSource::TraitImpl {
535                    impl_ref,
536                    trait_ref,
537                    item_id: *item_id.as_method().unwrap(),
538                    reuses_default,
539                },
540            }
541        };
542
543        if let hax::FullDefKind::Ctor(ctor) = def.kind() {
544            let signature = FunSig {
545                inputs: ctor
546                    .fields()
547                    .iter()
548                    .map(|field| self.translate_ty(span, &field.ty))
549                    .try_collect()?,
550                output: self.translate_ty(span, ctor.output_ty())?,
551                is_unsafe: false,
552                abi: Abi::rust(),
553                is_variadic: false,
554            };
555
556            let body = if item_meta.opacity.with_private_contents().is_opaque() {
557                Body::Opaque
558            } else {
559                self.build_ctor_body(span, def)?
560            };
561            return Ok(FunDecl {
562                def_id,
563                item_meta,
564                generics: self.into_generics(),
565                signature: Box::new(signature),
566                src,
567                body,
568            });
569        }
570
571        // Translate the function signature
572        trace!("Translating function signature");
573        let signature = match &def.kind {
574            hax::FullDefKind::Fn(f) => self.translate_fun_sig(span, &f.sig().value)?,
575            hax::FullDefKind::AssocFn(f) => self.translate_fun_sig(span, &f.sig().value)?,
576            hax::FullDefKind::Const(_)
577            | hax::FullDefKind::AssocConst(_)
578            | hax::FullDefKind::Static(_) => {
579                let ty = match &def.kind {
580                    hax::FullDefKind::Const(c) => c.ty(),
581                    hax::FullDefKind::AssocConst(c) => c.ty(),
582                    hax::FullDefKind::Static(s) => s.ty(),
583                    _ => unreachable!(),
584                };
585                FunSig {
586                    inputs: vec![],
587                    output: self.translate_ty(span, ty)?,
588                    is_unsafe: false,
589                    abi: Abi::rust(),
590                    is_variadic: false,
591                }
592            }
593            _ => panic!("Unexpected definition for function: {def:?}"),
594        };
595
596        let intrinsic = def
597            .def_id()
598            .as_real_def_id()
599            .and_then(|id| self.tcx.intrinsic(id));
600
601        let body = if let Some(intrinsic) = intrinsic
602            && intrinsic.name == sym::type_id
603            && TransItemSourceKind::IntrinsicFallback == self.item_src.kind
604        {
605            self.build_type_id_body(span, &signature)?
606        } else if let Some(intrinsic) = intrinsic
607            && TransItemSourceKind::IntrinsicFallback != self.item_src.kind
608        {
609            // we special-case type_id: we give it a custom fallback that is the spec
610            let is_type_id = intrinsic.name == sym::type_id;
611            let arg_names = self.translate_argument_names(span, def, signature.inputs.len());
612            let fallback = if intrinsic.must_be_overridden && !is_type_id {
613                None
614            } else {
615                let kind = TransItemSourceKind::IntrinsicFallback;
616                Some(self.translate_item(span, def.this(), kind)?)
617            };
618            // from nightly-2026-10-29 onwards, we can use tcx.tool_attrs for this (https://rust.tf/164900)
619            let fallback_is_spec = item_meta
620                .attr_info
621                .attributes
622                .iter()
623                .filter_map(|a| a.as_unknown())
624                .any(|a| a.path == "miri::intrinsic_fallback_is_spec");
625            Body::Intrinsic {
626                name: intrinsic.name.to_ident_string(),
627                arg_names,
628                fallback,
629                fallback_is_spec: fallback_is_spec || is_type_id,
630            }
631        } else if let Some(name) = self.t_ctx.extern_item_symbol_name(def) {
632            Body::Extern(name)
633        } else if item_meta.diagnostic_item.as_deref()
634            == Some(names::BOX_ASSUME_INIT_INTO_VEC_UNSAFE)
635            && self.options.treat_box_as_builtin
636        {
637            // FIXME(#865): the MIR we get is unusably optimized. Instead we build our own body
638            // here.
639            self.build_box_assume_init_into_vec_unsafe(span, def)?
640        } else if item_meta.lang_item.as_ref() == Some(&from_rustc::LangItem::DropGlue) {
641            self.build_drop_glue_body(span, def, &signature)?
642        } else if item_meta.opacity.with_private_contents().is_opaque() {
643            Body::Opaque
644        } else {
645            // Translate the MIR body for this definition.
646            self.translate_def_body(item_meta.span, def)
647        };
648        Ok(FunDecl {
649            def_id,
650            item_meta,
651            generics: self.into_generics(),
652            signature: Box::new(signature),
653            src,
654            body,
655        })
656    }
657
658    /// Translate one global.
659    #[tracing::instrument(skip(self, item_meta, def))]
660    pub fn translate_global(
661        mut self,
662        def_id: GlobalDeclId,
663        item_meta: ItemMeta,
664        def: &hax::FullDef<'tcx>,
665    ) -> Result<GlobalDecl, Error> {
666        let span = item_meta.span;
667
668        // Retrieve the kind
669        let item_source = match self.get_trait_item_source(span, def)? {
670            None => GlobalSource::Normal,
671            Some(TraitItemSource::Default { trait_ref, item_id }) => GlobalSource::TraitDefault {
672                trait_ref,
673                item_id: *item_id.as_const().unwrap(),
674            },
675            Some(TraitItemSource::Impl {
676                impl_ref,
677                trait_ref,
678                item_id,
679                reuses_default,
680            }) => GlobalSource::TraitImpl {
681                impl_ref,
682                trait_ref,
683                item_id: *item_id.as_const().unwrap(),
684                reuses_default,
685            },
686        };
687
688        trace!("Translating global type");
689        let ty = match &def.kind {
690            hax::FullDefKind::Const(c) => c.ty(),
691            hax::FullDefKind::AssocConst(c) => c.ty(),
692            hax::FullDefKind::Static(s) => s.ty(),
693            _ => panic!("Unexpected def for constant: {def:?}"),
694        };
695        let ty = self.translate_ty(span, ty)?;
696
697        let (size, align) = if let hax::DefIdBase::Alloc(alloc_id) = def.def_id().base {
698            let tcx = self.t_ctx.tcx;
699            let alloc = rustc_const_uneval::GlobalRef::Alloc(alloc_id)
700                .memory(tcx)
701                .unwrap()
702                .inner();
703            (
704                Size::new(alloc.size().bytes()),
705                Size::new(alloc.align.bytes()),
706            )
707        } else {
708            (
709                Size::from_expr(SizeExpr::size_of(&ty)),
710                Size::from_expr(SizeExpr::align_of(&ty)),
711            )
712        };
713
714        let global_kind = match &def.kind {
715            hax::FullDefKind::Static(s) => {
716                let is_mut = s.mutability() == hax::Mutability::Mut;
717                let is_safe = s.safety() == hax::Safety::Safe;
718                let is_thread_local = s.thread_local();
719                GlobalKind::Static {
720                    is_mut,
721                    is_safe,
722                    is_thread_local,
723                }
724            }
725            hax::FullDefKind::Const(c) if matches!(c.kind(), hax::ConstKind::TopLevel) => {
726                GlobalKind::NamedConst
727            }
728            hax::FullDefKind::AssocConst(_) => GlobalKind::NamedConst,
729            hax::FullDefKind::Const(_) => GlobalKind::AnonConst,
730            _ => panic!("Unexpected def for constant: {def:?}"),
731        };
732
733        // Try to evaluate the constant/static into a value if requested. This isn't always
734        // possible (e.g. for generic constants or recursive statics), in which case we fall back
735        // to a call to the initializer below. Globals that stand for an anonymous allocation have
736        // no initializer, so they are always evaluated.
737        let is_anon_alloc = matches!(def.def_id().base, hax::DefIdBase::Alloc(..));
738        let mode = match self.options.consts {
739            ConstHandling::Bytes => Some(hax::ReadMode::Bytes),
740            ConstHandling::Values => Some(hax::ReadMode::Structured),
741            ConstHandling::Initializers if is_anon_alloc => Some(hax::ReadMode::Structured),
742            ConstHandling::Initializers => None,
743        };
744        let evaluated = mode.and_then(|mode| def.evaluate(self.hax_state_with_id(), mode));
745        let value = if let hax::FullDefKind::Static(_) = def.kind()
746            && let Some(rust_def_id) = def.def_id().as_real_def_id()
747            && self
748                .t_ctx
749                .tcx
750                .codegen_fn_attrs(rust_def_id)
751                .import_linkage
752                .is_some()
753            && let Some(symbol) = self.t_ctx.extern_item_symbol_name(def)
754        {
755            // A foreign static with `#[linkage]` holds the address of the symbol it names.
756            let addr = ConstantExpr::new(
757                ConstantExprKind::ExternSymbol(symbol),
758                Ty::new(TyKind::RawPtr(Ty::mk_unit(), RefKind::Shared)),
759            );
760            ConstantExpr::new(
761                ConstantExprKind::Cast(addr, CastKind::Transmute(ty.clone())),
762                ty.clone(),
763            )
764        } else if let Some(evaluated) = evaluated {
765            self.translate_constant_expr(span, &evaluated)?
766        } else {
767            // Default: the value is a call to the initializer function, which uses the same
768            // generic parameters as the global.
769            let initializer = self.register_item(span, def.this(), TransItemSourceKind::Fun);
770            ConstantExpr::new(
771                ConstantExprKind::Call(
772                    FnPtr::new(
773                        FnPtrKind::Fun(initializer),
774                        self.outermost_generics().identity_args(),
775                    ),
776                    vec![],
777                ),
778                ty.clone(),
779            )
780        };
781
782        Ok(GlobalDecl {
783            def_id,
784            item_meta,
785            generics: self.into_generics(),
786            ty,
787            size,
788            align,
789            ptr_metadata: ConstantExpr::mk_unit(),
790            src: item_source,
791            global_kind,
792            value,
793        })
794    }
795
796    // either Poly or MonoTrait
797    #[tracing::instrument(skip(self, item_meta, def))]
798    pub fn translate_trait_decl(
799        mut self,
800        trait_decl_id: TraitDeclId,
801        item_meta: ItemMeta,
802        def: &hax::FullDef<'tcx>,
803    ) -> Result<TraitDecl, Error> {
804        let span = item_meta.span;
805
806        let implied_predicates = match def.kind() {
807            hax::FullDefKind::Trait(t) => t.implied_predicates(),
808            hax::FullDefKind::TraitAlias(t) => t.implied_predicates(),
809            _ => raise_error!(self, span, "Unexpected definition: {def:?}"),
810        };
811        let (src, is_unsafe) = match def.kind() {
812            hax::FullDefKind::Trait(tr) => (TraitDeclSource::Normal, tr.is_unsafe()),
813            hax::FullDefKind::TraitAlias(_) => (TraitDeclSource::TraitAlias, false),
814            _ => unreachable!(),
815        };
816
817        // Register implied predicates. We gather the clauses and consider the other predicates as
818        // required since the distinction doesn't matter for non-trait-clauses.
819        let mut implied_clauses = Default::default();
820        self.translate_predicates(
821            implied_predicates,
822            PredicateOrigin::WhereClauseOnTrait,
823            Some(&mut implied_clauses),
824        )?;
825
826        let vtable = self.translate_vtable_struct_ref_no_enqueue(span, def.this())?;
827
828        if let hax::FullDefKind::TraitAlias(_) = def.kind() {
829            // Trait aliases don't have any items. Everything interesting is in the parent clauses.
830            return Ok(TraitDecl {
831                def_id: trait_decl_id,
832                item_meta,
833                src,
834                is_unsafe,
835                implied_clauses,
836                generics: self.into_generics(),
837                consts: Default::default(),
838                types: Default::default(),
839                methods: Default::default(),
840                vtable,
841            });
842        }
843
844        let hax::FullDefKind::Trait(t) = &def.kind else {
845            unreachable!()
846        };
847        let self_trait_ref = TraitRef::new(
848            TraitRefKind::SelfId,
849            self.translate_trait_predicate(span, t.self_predicate())?,
850        );
851
852        // Translate the associated items
853        self.register_assoc_items(def.def_id(), trait_decl_id)?;
854        let mut consts: IndexMap<AssocConstId, _> = IndexMap::new();
855        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
856        let mut methods: IndexMap<TraitMethodId, _> = IndexMap::new();
857
858        if def.lang_item == Some(sym::destruct) {
859            // Add a `drop_in_place(*mut self)` method that contains the drop glue for this type.
860            let destruct_trait_def_id = def.def_id();
861            let method_id =
862                self.translate_drop_glue_method_id(destruct_trait_def_id, trait_decl_id)?;
863            self.mark_method_as_used(trait_decl_id, method_id);
864            let method = {
865                let method_name = self.translated.assoc_item_name(trait_decl_id, method_id);
866                let mut method_item_meta = ItemMeta::dummy_public(
867                    span,
868                    item_meta.name.clone(),
869                    item_meta.is_local,
870                    item_meta.opacity,
871                );
872                method_item_meta.name.name.push(PathElem::Ident(
873                    method_name.to_string(),
874                    Disambiguator::ZERO,
875                ));
876                let self_ty = if self.monomorphize() {
877                    // FIXME: put something real here
878                    Ty::mk_unit()
879                } else {
880                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::one(), TypeVarId::ZERO))
881                        .into_ty()
882                };
883                let signature = self.drop_glue_method_sig(
884                    self_ty,
885                    Region::Var(DeBruijnVar::new_at_zero(RegionId::ZERO)),
886                );
887                let method_params = Self::drop_glue_params();
888                Binder::new(
889                    BinderKind::TraitMethod(trait_decl_id, method_id),
890                    method_params,
891                    TraitMethod {
892                        name: method_name,
893                        default: None,
894                        item_meta: method_item_meta,
895                        signature,
896                    },
897                )
898            };
899            methods.set_slot_extend(method_id, method);
900        }
901
902        // skip all associated items of trait decl in mono mode
903        // question: what if the associated methods (or consts) has default implmentation?
904        // TODO: support default methods and default consts
905        if self.monomorphize() {
906            return Ok(TraitDecl {
907                def_id: trait_decl_id,
908                item_meta,
909                src,
910                is_unsafe,
911                implied_clauses,
912                generics: self.into_generics(),
913                consts,
914                types,
915                methods,
916                vtable,
917            });
918        }
919
920        for hax_item in t.items(self.hax_state()) {
921            let item_def_id = &hax_item.def_id;
922            let item_span = self.def_span(item_def_id);
923            let assoc_item_id = self.translate_assoc_item_id(trait_decl_id, item_def_id)?;
924            let item_name = self
925                .translated
926                .assoc_item_name(trait_decl_id, assoc_item_id);
927
928            // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
929            // polymorphic item as usual.
930            let trans_kind = match hax_item.kind {
931                hax::AssocKind::Fn { .. } => TransItemSourceKind::Fun,
932                hax::AssocKind::Const { .. } => TransItemSourceKind::Global,
933                hax::AssocKind::Type { .. } => TransItemSourceKind::Type,
934            };
935
936            let item_def = self.poly_hax_def(item_def_id)?;
937            let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
938            let attr_info = self.translate_attr_info(&item_def);
939
940            match item_def.kind() {
941                hax::FullDefKind::AssocFn(f) => {
942                    let trait_method_id = *assoc_item_id.as_method().unwrap();
943                    let method_name = self.translate_name(&item_src)?;
944                    let method_opacity = self.opacity_for_name(&method_name);
945                    let method_item_meta =
946                        self.translate_item_meta(&item_def, &item_src, method_name, method_opacity);
947                    let method_containment_id =
948                        ContainmentNode::TraitMethod(trait_decl_id, trait_method_id);
949                    // By default we only enqueue required methods (those that don't have a default
950                    // impl). If the trait is transparent, we enqueue all its methods.
951                    if self.options.translate_all_methods
952                        || item_meta.opacity.is_transparent()
953                        || !hax_item.has_value
954                    {
955                        self.mark_method_as_used(trait_decl_id, trait_method_id);
956                        self.record_containment(
957                            ItemId::TraitDecl(trait_decl_id),
958                            method_containment_id,
959                        );
960                    }
961                    let default_fun_id = f.associated_item().has_value.then(|| {
962                        let fun_id = self.register_no_enqueue(item_span, &item_src);
963                        // Register this method.
964                        self.register_method_impl(trait_decl_id, trait_method_id, fun_id);
965                        self.record_containment(method_containment_id, ItemId::Fun(fun_id));
966                        fun_id
967                    });
968
969                    let binder_kind = BinderKind::TraitMethod(trait_decl_id, trait_method_id);
970                    let mut method = self.translate_binder_for_def(
971                        item_span,
972                        binder_kind,
973                        &item_def,
974                        |bt_ctx| {
975                            assert_eq!(bt_ctx.binding_levels.len(), 2);
976                            let default = default_fun_id.map(|id| {
977                                let fun_generics = bt_ctx
978                                    .outermost_binder()
979                                    .params
980                                    .identity_args_at_depth(DeBruijnId::one())
981                                    .concat(
982                                        &bt_ctx
983                                            .innermost_binder()
984                                            .params
985                                            .identity_args_at_depth(DeBruijnId::zero()),
986                                    );
987                                FunDeclRef {
988                                    id,
989                                    generics: Box::new(fun_generics),
990                                }
991                            });
992                            // `skip_binder` is allowed because `translate_binder_for_def` puts the
993                            // late bound params in scope.
994                            let signature =
995                                bt_ctx.translate_fun_sig(span, f.sig().hax_skip_binder_ref())?;
996                            Ok(TraitMethod {
997                                name: item_name,
998                                item_meta: method_item_meta,
999                                signature,
1000                                default,
1001                            })
1002                        },
1003                    )?;
1004                    // In hax, associated items take an extra explicit `Self: Trait` clause, but we
1005                    // don't want that to be part of the method clauses. Hence we remove the first
1006                    // bound clause and replace its uses with references to the ambient `Self`
1007                    // clause available in trait declarations.
1008                    struct ReplaceSelfVisitor;
1009                    impl VarsVisitor for ReplaceSelfVisitor {
1010                        fn visit_clause_var(
1011                            &mut self,
1012                            v: ClauseDbVar,
1013                        ) -> Option<ClauseReplacement> {
1014                            if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
1015                                // Replace clause 0 and decrement the others.
1016                                Some(if let Some(new_id) = clause_id.index().checked_sub(1) {
1017                                    ClauseReplacement::Var(DeBruijnVar::Bound(
1018                                        DeBruijnId::ZERO,
1019                                        TraitClauseId::new(new_id),
1020                                    ))
1021                                } else {
1022                                    ClauseReplacement::Proof(RegionBinder::empty(
1023                                        TraitRefKind::SelfId,
1024                                    ))
1025                                })
1026                            } else {
1027                                None
1028                            }
1029                        }
1030                    }
1031                    method.params.visit_vars(&mut ReplaceSelfVisitor);
1032                    method.skip_binder.visit_vars(&mut ReplaceSelfVisitor);
1033                    method
1034                        .params
1035                        .trait_clauses
1036                        .remove_and_shift_ids(TraitClauseId::ZERO);
1037                    method.params.trait_clauses.iter_mut().for_each(|clause| {
1038                        clause.clause_id -= 1;
1039                    });
1040
1041                    // We insert the `Binder<TraitMethod>` unconditionally here; we'll remove the
1042                    // ones that correspond to unused methods at the end of translation.
1043                    methods.set_slot_extend(trait_method_id, method);
1044                }
1045                hax::FullDefKind::AssocConst(c) => {
1046                    let assoc_const_id = *assoc_item_id.as_const().unwrap();
1047                    // The const is defined in a context that has an extra `Self: Trait` clause, so
1048                    // we translate it bound first.
1049                    let bound_assoc_const = self.translate_binder_for_def(
1050                        item_span,
1051                        BinderKind::Other,
1052                        &item_def,
1053                        |ctx| {
1054                            // Check if the constant has a value (i.e., a body).
1055                            let default = hax_item.has_value.then(|| {
1056                                // The parameters of the constant are the same as those of the item that
1057                                // declares them.
1058                                let id = ctx.register_and_enqueue(item_span, item_src);
1059                                if item_meta.opacity.is_transparent() {
1060                                    ctx.record_containment(
1061                                        ItemId::TraitDecl(trait_decl_id),
1062                                        ItemId::Global(id),
1063                                    );
1064                                }
1065                                let generics = ctx
1066                                    .outermost_binder()
1067                                    .params
1068                                    .identity_args_at_depth(DeBruijnId::one())
1069                                    .concat(
1070                                        &ctx.innermost_binder()
1071                                            .params
1072                                            .identity_args_at_depth(DeBruijnId::zero()),
1073                                    );
1074                                GlobalDeclRef {
1075                                    id,
1076                                    generics: Box::new(generics),
1077                                }
1078                            });
1079                            let ty = ctx.translate_ty(item_span, c.ty())?;
1080                            Ok(TraitAssocConst {
1081                                name: item_name,
1082                                attr_info,
1083                                ty,
1084                                default,
1085                            })
1086                        },
1087                    )?;
1088                    let assoc_const = bound_assoc_const.apply(&{
1089                        let mut generics = GenericArgs::empty();
1090                        // Provide the `Self` clause.
1091                        generics
1092                            .trait_refs
1093                            .push(PolyTraitRef::empty(self_trait_ref.clone()));
1094                        generics
1095                    });
1096                    consts.set_slot_extend(assoc_const_id, assoc_const);
1097                }
1098                hax::FullDefKind::AssocTy(assoc_ty_def) => {
1099                    let assoc_type_id = *assoc_item_id.as_type().unwrap();
1100                    let binder_kind = BinderKind::TraitType(trait_decl_id, assoc_type_id);
1101                    let assoc_ty =
1102                        self.translate_binder_for_def(item_span, binder_kind, &item_def, |ctx| {
1103                            // Also add the implied predicates.
1104                            let mut implied_clauses = Default::default();
1105                            ctx.translate_predicates(
1106                                assoc_ty_def.implied_predicates(),
1107                                PredicateOrigin::TraitItem(assoc_type_id),
1108                                Some(&mut implied_clauses),
1109                            )?;
1110
1111                            let default = assoc_ty_def
1112                                .value(ctx.hax_state())
1113                                .map(|(ty, trait_proofs)| -> Result<_, Error> {
1114                                    let ty = ctx.translate_ty(item_span, &ty)?;
1115                                    let trefs = ctx.translate_trait_proofs(span, &trait_proofs)?;
1116                                    Ok(TraitAssocTyImpl {
1117                                        value: ty,
1118                                        implied_trait_refs: trefs,
1119                                    })
1120                                })
1121                                .transpose()?;
1122                            Ok(TraitAssocTy {
1123                                name: item_name,
1124                                attr_info,
1125                                default,
1126                                implied_clauses,
1127                            })
1128                        })?;
1129                    types.set_slot_extend(assoc_type_id, assoc_ty);
1130                }
1131                _ => panic!("Unexpected definition for trait item: {item_def:?}"),
1132            }
1133        }
1134
1135        // In case of a trait implementation, some values may not have been
1136        // provided, in case the declaration provided default values. We
1137        // check those, and lookup the relevant values.
1138        Ok(TraitDecl {
1139            def_id: trait_decl_id,
1140            item_meta,
1141            src,
1142            is_unsafe,
1143            implied_clauses,
1144            generics: self.into_generics(),
1145            consts,
1146            types,
1147            methods,
1148            vtable,
1149        })
1150    }
1151
1152    #[tracing::instrument(skip(self, item_meta, def))]
1153    pub fn translate_trait_impl(
1154        mut self,
1155        def_id: TraitImplId,
1156        item_meta: ItemMeta,
1157        def: &hax::FullDef<'tcx>,
1158    ) -> Result<TraitImpl, Error> {
1159        let span = item_meta.span;
1160
1161        let hax::FullDefKind::TraitImpl(timpl) = &def.kind else {
1162            unreachable!()
1163        };
1164
1165        // Retrieve the information about the implemented trait.
1166        let trait_pred = timpl.trait_pred();
1167        let implemented_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
1168        let trait_id = implemented_trait.id;
1169        let is_negative = !trait_pred.is_positive;
1170        let is_unsafe = timpl.is_unsafe();
1171
1172        // Translate the bare minimum needed for names.
1173        if self.is_poly_in_mono(&self.item_src) {
1174            let implied_trait_refs =
1175                self.translate_trait_proofs(span, timpl.implied_trait_proofs())?;
1176            return Ok(TraitImpl {
1177                def_id,
1178                item_meta,
1179                src: TraitImplSource::Normal,
1180                impl_trait: implemented_trait,
1181                is_negative,
1182                is_unsafe,
1183                generics: self.into_generics(),
1184                implied_trait_refs,
1185                consts: Default::default(),
1186                types: Default::default(),
1187                methods: Default::default(),
1188                vtable: VTableDecl::Unknown("polymorphic impl in monomorphic mode".into()),
1189            });
1190        }
1191
1192        // A `TraitRef` that points to this impl with the correct generics.
1193        let self_predicate = TraitRef::new(
1194            TraitRefKind::TraitImpl(TraitImplRef {
1195                id: def_id,
1196                generics: Box::new(self.the_only_binder().params.identity_args()),
1197            }),
1198            implemented_trait.clone(),
1199        );
1200
1201        let vtable = self.translate_trait_impl_vtable(
1202            span,
1203            &trait_pred.trait_ref,
1204            def.this(),
1205            TransImplSource::Normal,
1206        )?;
1207
1208        // The trait refs which implement the parent clauses of the implemented trait decl.
1209        let implied_trait_refs = self.translate_trait_proofs(span, timpl.implied_trait_proofs())?;
1210
1211        {
1212            // Debugging
1213            let ctx = self.into_fmt();
1214            let refs = implied_trait_refs
1215                .iter()
1216                .map(|c| c.with_ctx(&ctx))
1217                .format("\n");
1218            trace!(
1219                "Trait impl: {:?}\n- implied_trait_refs:\n{}",
1220                def.def_id(),
1221                refs
1222            );
1223        }
1224
1225        let implemented_trait_def = self.poly_hax_def(&trait_pred.trait_ref.def_id)?;
1226        if implemented_trait_def.lang_item == Some(sym::destruct) {
1227            raise_error!(
1228                self,
1229                span,
1230                "found an explicit impl of `core::marker::Destruct`, this should not happen"
1231            );
1232        }
1233
1234        // Explore the associated items
1235        let mut consts: IndexMap<AssocConstId, _> = IndexMap::new();
1236        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
1237        let mut methods: IndexMap<TraitMethodId, _> = IndexMap::new();
1238
1239        // In mono mode, we do not translate any associated items in trait impl.
1240        if self.monomorphize() {
1241            return Ok(TraitImpl {
1242                def_id,
1243                item_meta,
1244                src: TraitImplSource::Normal,
1245                impl_trait: implemented_trait,
1246                is_negative,
1247                is_unsafe,
1248                generics: self.into_generics(),
1249                implied_trait_refs,
1250                consts,
1251                types,
1252                methods,
1253                vtable,
1254            });
1255        }
1256
1257        for impl_item in timpl.items(self.hax_state()) {
1258            let item_def_id = impl_item.def_id().unwrap_or(impl_item.decl_def_id());
1259            let item_span = self.def_span(item_def_id);
1260            let assoc_item_id = self.translate_assoc_item_id(trait_id, item_def_id)?;
1261
1262            // In not-mono mode, we use the polymorphic item as usual.
1263            let trans_kind = match item_def_id.kind {
1264                hax::DefKind::AssocFn => TransItemSourceKind::Fun,
1265                hax::DefKind::AssocConst => TransItemSourceKind::Global,
1266                hax::DefKind::AssocTy => TransItemSourceKind::Type,
1267                _ => unreachable!(),
1268            };
1269            let item_src = TransItemSource::polymorphic(item_def_id, trans_kind);
1270
1271            match item_def_id.kind {
1272                hax::DefKind::AssocFn => {
1273                    let trait_method_id = *assoc_item_id.as_method().unwrap();
1274                    let binder_kind = BinderKind::TraitMethod(trait_id, trait_method_id);
1275                    let bound_fn_ref = match &impl_item.value {
1276                        Some(value) => {
1277                            // By default we only enqueue required methods (those that don't have a default
1278                            // impl). If the impl is transparent, we enqueue all the implemented methods.
1279                            if item_meta.opacity.is_transparent() {
1280                                self.mark_method_as_used(trait_id, trait_method_id);
1281                            }
1282                            self.translate_item_binder(
1283                                item_span,
1284                                binder_kind,
1285                                value,
1286                                PredicateOrigin::WhereClauseOnFn,
1287                                |ctx, value| {
1288                                    let bound_fn_ptr = ctx.translate_bound_fn_ptr_no_enqueue(
1289                                        item_span,
1290                                        &value.item,
1291                                        TransItemSourceKind::Fun,
1292                                    )?;
1293                                    // FIXME(#513): the regions may not match.
1294                                    let late_bound_regions: RegionArgs = ctx
1295                                        .innermost_binder()
1296                                        .bound_region_vars
1297                                        .iter()
1298                                        .map(|rid| Region::Var(DeBruijnVar::new_at_zero(*rid)))
1299                                        .collect();
1300                                    let fn_ptr = bound_fn_ptr.apply(late_bound_regions);
1301                                    Ok(FunDeclRef {
1302                                        id: *fn_ptr.kind.as_fun().unwrap(),
1303                                        generics: fn_ptr.generics,
1304                                    })
1305                                },
1306                            )?
1307                        }
1308                        None => {
1309                            // Reuse the default method from the trait declaration.
1310                            let bound_method = match self.get_or_translate(trait_id.into()) {
1311                                Ok(ItemRef::TraitDecl(tdecl)) => {
1312                                    tdecl.methods.get(trait_method_id).cloned()
1313                                }
1314                                _ => None,
1315                            };
1316                            let Some(bound_method) = bound_method else {
1317                                continue;
1318                            };
1319                            bound_method
1320                                .substitute_with_tref(&self_predicate)
1321                                .map(|method| {
1322                                    method
1323                                        .default
1324                                        .expect("default method should have a default")
1325                                })
1326                        }
1327                    };
1328
1329                    // Register this method.
1330                    self.register_method_impl(
1331                        trait_id,
1332                        trait_method_id,
1333                        bound_fn_ref.skip_binder.id,
1334                    );
1335                    if item_meta.opacity.is_transparent() && impl_item.value.is_some() {
1336                        self.record_containment(
1337                            ItemId::TraitImpl(def_id),
1338                            ItemId::Fun(bound_fn_ref.skip_binder.id),
1339                        );
1340                    }
1341
1342                    // We insert the `Binder<FunDeclRef>` unconditionally here; we'll remove the
1343                    // ones that correspond to unused methods at the end of translation.
1344                    methods.set_slot_extend(trait_method_id, bound_fn_ref);
1345                }
1346                hax::DefKind::AssocConst => {
1347                    let assoc_const_id = *assoc_item_id.as_const().unwrap();
1348                    let id = self.register_and_enqueue(item_span, item_src);
1349                    if item_meta.opacity.is_transparent() && impl_item.value.is_some() {
1350                        self.record_containment(ItemId::TraitImpl(def_id), ItemId::Global(id));
1351                    }
1352                    // The parameters of the constant are the same as those of the item that
1353                    // declares them.
1354                    let generics = match &impl_item.value {
1355                        Some(_) => self.the_only_binder().params.identity_args(),
1356                        None => {
1357                            let mut generics = implemented_trait.generics.as_ref().clone();
1358                            // For default consts, we add an extra `Self` predicate.
1359                            generics
1360                                .trait_refs
1361                                .push(PolyTraitRef::empty(self_predicate.clone()));
1362                            generics
1363                        }
1364                    };
1365                    let gref = GlobalDeclRef {
1366                        id,
1367                        generics: Box::new(generics),
1368                    };
1369                    consts.set_slot_extend(assoc_const_id, gref);
1370                }
1371                hax::DefKind::AssocTy => {
1372                    let assoc_type_id = *assoc_item_id.as_type().unwrap();
1373                    let binder_kind = BinderKind::TraitType(trait_id, assoc_type_id);
1374                    let assoc_ty = match &impl_item.value {
1375                        Some(impl_value) => self.translate_item_binder(
1376                            item_span,
1377                            binder_kind,
1378                            impl_value,
1379                            PredicateOrigin::WhereClauseOnType,
1380                            |ctx, impl_value| {
1381                                let ty = ctx.translate_ty(
1382                                    item_span,
1383                                    impl_value.assoc_ty_value.as_ref().unwrap(),
1384                                )?;
1385                                let implied_trait_refs = ctx.translate_trait_proofs(
1386                                    item_span,
1387                                    &impl_value.implied_trait_proofs,
1388                                )?;
1389                                Ok(TraitAssocTyImpl {
1390                                    value: ty,
1391                                    implied_trait_refs,
1392                                })
1393                            },
1394                        )?,
1395                        None => {
1396                            // Retrieve the type from the trait decl.
1397                            let trait_id = implemented_trait.id;
1398                            let bound_ty = match self.get_or_translate(trait_id.into()) {
1399                                Ok(ItemRef::TraitDecl(tdecl)) => tdecl.types.get(assoc_type_id),
1400                                _ => None,
1401                            };
1402                            let Some(bound_ty) = bound_ty else {
1403                                register_error!(
1404                                    self,
1405                                    item_span,
1406                                    "couldn't translate defaulted associated type; \
1407                                    either the corresponding trait decl caused errors \
1408                                    or it was declared opaque."
1409                                );
1410                                continue;
1411                            };
1412                            bound_ty
1413                                .clone()
1414                                .substitute_with_tref(&self_predicate)
1415                                .map(|ty_decl: TraitAssocTy| ty_decl.default.unwrap())
1416                        }
1417                    };
1418
1419                    types.set_slot_extend(assoc_type_id, assoc_ty);
1420                }
1421                _ => panic!("Unexpected definition for trait item: {item_def_id:?}"),
1422            }
1423        }
1424
1425        Ok(TraitImpl {
1426            def_id,
1427            item_meta,
1428            src: TraitImplSource::Normal,
1429            impl_trait: implemented_trait,
1430            is_negative,
1431            is_unsafe,
1432            generics: self.into_generics(),
1433            implied_trait_refs,
1434            consts,
1435            types,
1436            methods,
1437            vtable,
1438        })
1439    }
1440
1441    /// Generate a blanket impl for this trait, as in:
1442    /// ```
1443    ///     trait Alias<U> = Trait<Option<U>, Item = u32> + Clone;
1444    /// ```
1445    /// becomes:
1446    /// ```
1447    ///     trait Alias<U>: Trait<Option<U>, Item = u32> + Clone {}
1448    ///     impl<U, Self: Trait<Option<U>, Item = u32> + Clone> Alias<U> for Self {}
1449    /// ```
1450    #[tracing::instrument(skip(self, item_meta, def))]
1451    pub fn translate_trait_alias_blanket_impl(
1452        mut self,
1453        def_id: TraitImplId,
1454        item_meta: ItemMeta,
1455        def: &hax::FullDef<'tcx>,
1456    ) -> Result<TraitImpl, Error> {
1457        let span = item_meta.span;
1458
1459        let hax::FullDefKind::TraitAlias(t) = &def.kind else {
1460            raise_error!(self, span, "Unexpected definition: {def:?}");
1461        };
1462
1463        // Retrieve the information about the implemented trait.
1464        let implemented_trait = self.translate_trait_ref(span, &t.self_predicate().trait_ref)?;
1465
1466        // Register the trait implied clauses as required clauses for the impl.
1467        assert!(self.innermost_generics_mut().trait_clauses.is_empty());
1468        self.register_predicates(t.implied_predicates(), PredicateOrigin::WhereClauseOnTrait)?;
1469
1470        let mut generics = self.the_only_binder().params.identity_args();
1471        // Do the inverse operation: the trait considers the clauses as implied.
1472        let implied_trait_refs = mem::take(&mut generics.trait_refs);
1473
1474        let mut timpl = TraitImpl {
1475            def_id,
1476            item_meta,
1477            src: TraitImplSource::TraitAlias,
1478            impl_trait: implemented_trait,
1479            is_negative: false,
1480            is_unsafe: false,
1481            generics: self.the_only_binder().params.clone(),
1482            implied_trait_refs,
1483            consts: Default::default(),
1484            types: Default::default(),
1485            methods: Default::default(),
1486            // TODO(dyn)
1487            vtable: VTableDecl::Unknown("vtables of trait alias impls are not supported".into()),
1488        };
1489        // We got the predicates from a trait decl, so they may refer to the virtual `Self`
1490        // clause, which doesn't exist for impls. We fix that up here.
1491        {
1492            struct FixSelfVisitor {
1493                binder_depth: DeBruijnId,
1494            }
1495            struct UnhandledSelf;
1496            impl Visitor for FixSelfVisitor {
1497                type Break = UnhandledSelf;
1498            }
1499            impl VisitorWithBinderDepth for FixSelfVisitor {
1500                fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
1501                    &mut self.binder_depth
1502                }
1503            }
1504            impl VisitAstMut for FixSelfVisitor {
1505                fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
1506                    VisitWithBinderDepth::new(self).visit(x)
1507                }
1508                fn visit_trait_ref_kind(
1509                    &mut self,
1510                    kind: &mut TraitRefKind,
1511                ) -> ControlFlow<Self::Break> {
1512                    match kind {
1513                        TraitRefKind::SelfId => return ControlFlow::Break(UnhandledSelf),
1514                        TraitRefKind::ParentClause(sub, clause_id, clause_args)
1515                            if matches!(sub.kind, TraitRefKind::SelfId) =>
1516                        {
1517                            *kind = TraitRefKind::Clause(
1518                                DeBruijnVar::bound(self.binder_depth, *clause_id),
1519                                clause_args.clone(),
1520                            )
1521                        }
1522                        _ => (),
1523                    }
1524                    self.visit_inner(kind)
1525                }
1526            }
1527            match timpl.drive_mut(&mut FixSelfVisitor {
1528                binder_depth: DeBruijnId::zero(),
1529            }) {
1530                ControlFlow::Continue(()) => {}
1531                ControlFlow::Break(UnhandledSelf) => {
1532                    register_error!(
1533                        self,
1534                        span,
1535                        "Found `Self` clause we can't handle \
1536                         in a trait alias blanket impl."
1537                    );
1538                }
1539            }
1540        };
1541
1542        Ok(timpl)
1543    }
1544
1545    /// Make a trait impl from a hax `VirtualTraitImpl`. Used for constructing fake trait impls for
1546    /// builtin types like `FnOnce`.
1547    #[tracing::instrument(skip(self, item_meta))]
1548    pub fn translate_virtual_trait_impl(
1549        &mut self,
1550        def_id: TraitImplId,
1551        item_meta: ItemMeta,
1552        vtable_item: &hax::ItemRef<'tcx>,
1553        impl_kind: TransImplSource,
1554        vimpl: &hax::VirtualTraitImpl<'tcx>,
1555    ) -> Result<TraitImpl, Error> {
1556        let span = item_meta.span;
1557        let src = match impl_kind {
1558            TransImplSource::Callable(kind) => TraitImplSource::Closure { kind },
1559            TransImplSource::ImplicitDestruct => TraitImplSource::Destruct,
1560            _ => unreachable!("not a virtual impl source: {impl_kind:?}"),
1561        };
1562
1563        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
1564        let implied_trait_refs = self.translate_trait_proofs(span, &vimpl.implied_trait_proofs)?;
1565        let vtable = self.translate_trait_impl_vtable(
1566            span,
1567            &vimpl.trait_pred.trait_ref,
1568            vtable_item,
1569            impl_kind,
1570        )?;
1571
1572        let mut types: IndexMap<AssocTypeId, _> = IndexMap::new();
1573        // Monomorphic traits have no associated types.
1574        if !self.monomorphize() {
1575            let trait_def = self.poly_hax_def(&vimpl.trait_pred.trait_ref.def_id)?;
1576            let hax::FullDefKind::Trait(t) = trait_def.kind() else {
1577                panic!()
1578            };
1579            let trait_items = t.items(self.hax_state());
1580            let type_items = trait_items
1581                .iter()
1582                .filter(|assoc| matches!(assoc.kind, hax::AssocKind::Type { .. }));
1583            for ((ty, trait_proofs), assoc) in vimpl.types.iter().zip(type_items) {
1584                let assoc_type_id =
1585                    self.translate_assoc_type_id(implemented_trait.id, &assoc.def_id)?;
1586                let assoc_ty = TraitAssocTyImpl {
1587                    value: self.translate_ty(span, ty)?,
1588                    implied_trait_refs: self.translate_trait_proofs(span, trait_proofs)?,
1589                };
1590                let binder_kind = BinderKind::TraitType(implemented_trait.id, assoc_type_id);
1591                types.set_slot_extend(assoc_type_id, Binder::empty(binder_kind, assoc_ty));
1592            }
1593        }
1594
1595        let generics = self.the_only_binder().params.clone();
1596        Ok(TraitImpl {
1597            def_id,
1598            item_meta,
1599            src,
1600            impl_trait: implemented_trait,
1601            is_negative: false,
1602            is_unsafe: false,
1603            generics,
1604            implied_trait_refs,
1605            consts: IndexMap::new(),
1606            types,
1607            methods: IndexMap::new(),
1608            vtable,
1609        })
1610    }
1611}
charon_driver/translate/translate_items.rs

charon_driver/translate/
translate_items.rs
