charon_driver/translate/
translate_crate.rs

1//! This file governs the overall translation of items.
2//!
3//! Translation works as follows: we translate each `TransItemSource` of interest into an
4//! appropriate item. In the process of translating an item we may find more `hax::DefId`s of
5//! interest; we register those as an appropriate `TransItemSource`, which will 1/ enqueue the item
6//! so that it eventually gets translated too, and 2/ return an `ItemId` we can use to refer to
7//! it.
8//!
9//! We start with the DefId of the current crate (or of anything passed to `--start-from`) and
10//! recursively translate everything we find.
11//!
12//! There's another important component at play: opacity. Each item is assigned an opacity based on
13//! its name. By default, items from the local crate are transparent and items from foreign crates
14//! are opaque (this can be controlled with `--include`, `--opaque` and `--exclude`). If an item is
15//! opaque, its signature/"outer shell" will be translated (e.g. for functions that's the
16//! signature) but not its contents.
17use super::translate_ctx::*;
18use charon_lib::ast::*;
19use charon_lib::options::{CliOpts, TranslateOptions};
20use charon_lib::transform::TransformCtx;
21use hax::SInto;
22use itertools::Itertools;
23use macros::VariantIndexArity;
24use rustc_middle::ty::TyCtxt;
25use std::cell::RefCell;
26use std::path::PathBuf;
27
28/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
29/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
30/// `FunDecl` one (for its initializer function).
31#[derive(Clone, Debug, PartialEq, Eq, Hash)]
32pub struct TransItemSource {
33    pub item: RustcItem,
34    pub kind: TransItemSourceKind,
35}
36
37/// Refers to a rustc item. Can be either the polymorphic version of the item, or a
38/// monomorphization of it.
39#[derive(Clone, Debug, PartialEq, Eq, Hash)]
40pub enum RustcItem {
41    Poly(hax::DefId),
42    Mono(hax::ItemRef),
43}
44
45/// The kind of a [`TransItemSource`].
46#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
47pub enum TransItemSourceKind {
48    Global,
49    TraitDecl,
50    TraitImpl(TraitImplSource),
51    Fun,
52    Type,
53    /// We don't translate these as proper items, but we translate them a bit in names.
54    InherentImpl,
55    /// We don't translate these as proper items, but we use them to explore the crate.
56    Module,
57    /// The `call_*` method of the appropriate `TraitImplSource::Closure` impl.
58    ClosureMethod(ClosureKind),
59    /// A cast of a state-less closure as a function pointer.
60    ClosureAsFnCast,
61    /// The `drop` method of a `TraitImplSource::ImplicitDrop` trait impl; that method does
62    /// nothing.
63    EmptyDropMethod,
64    /// The `drop_in_place` method of a `Drop` impl or decl. It contains the drop glue that calls
65    /// `Drop::drop` for the type and then drops its fields. if the `TraitImplSource` is `None`
66    /// this is the method declaration (and the DefId is that of the `Drop` trait), otherwise this
67    /// is a method implementation (and the DefId is either that of a `impl Drop for Foo` impl, or
68    /// that of an ADT in case of an implicit `Drop` impl).
69    DropInPlaceMethod(Option<TraitImplSource>),
70    /// The virtual table struct definition for a trait. The `DefId` is that of the trait.
71    VTable,
72    /// The static vtable value for a specific impl.
73    VTableInstance(TraitImplSource),
74    /// The initializer function of the `VTableInstance`.
75    VTableInstanceInitializer(TraitImplSource),
76    /// Shim function to store a method in a vtable; give a method with `self: Ptr<Self>` argument,
77    /// this takes a `Ptr<dyn Trait>` and forwards to the method. The `DefId` refers to the method
78    /// implementation.
79    VTableMethod,
80}
81
82/// The kind of a [`TransItemSourceKind::TraitImpl`].
83#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
84pub enum TraitImplSource {
85    /// A user-written trait impl with a `DefId`.
86    Normal,
87    /// The blanket impl we generate for a trait alias. The `DefId` is that of the trait alias.
88    TraitAlias,
89    /// An impl of the appropriate `Fn*` trait for a closure. The `DefId` is that of the closure.
90    Closure(ClosureKind),
91    /// A fictitious `impl Drop for T` that contains the drop glue code for the given ADT. The
92    /// `DefId` is that of the ADT.
93    ImplicitDrop,
94}
95
96impl TransItemSource {
97    pub fn new(item: RustcItem, kind: TransItemSourceKind) -> Self {
98        if let RustcItem::Mono(item) = &item {
99            if item.has_param {
100                panic!("Item is not monomorphic: {item:?}")
101            }
102        }
103        Self { item, kind }
104    }
105
106    /// Refers to the given item. Depending on `monomorphize`, this chooses between the monomorphic
107    /// and polymorphic versions of the item.
108    pub fn from_item(item: &hax::ItemRef, kind: TransItemSourceKind, monomorphize: bool) -> Self {
109        if monomorphize {
110            Self::monomorphic(item, kind)
111        } else {
112            Self::polymorphic(&item.def_id, kind)
113        }
114    }
115
116    /// Refers to the polymorphic version of this item.
117    pub fn polymorphic(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
118        Self::new(RustcItem::Poly(def_id.clone()), kind)
119    }
120
121    /// Refers to the monomorphic version of this item.
122    pub fn monomorphic(item: &hax::ItemRef, kind: TransItemSourceKind) -> Self {
123        Self::new(RustcItem::Mono(item.clone()), kind)
124    }
125
126    pub fn def_id(&self) -> &hax::DefId {
127        self.item.def_id()
128    }
129
130    /// Keep the same def_id but change the kind.
131    pub(crate) fn with_kind(&self, kind: TransItemSourceKind) -> Self {
132        let mut ret = self.clone();
133        ret.kind = kind;
134        ret
135    }
136
137    /// For virtual items that have a parent (typically a method impl), return this parent. Does
138    /// not attempt to generally compute the parent of an item. Used to compute names.
139    pub(crate) fn parent(&self) -> Option<Self> {
140        let parent_kind = match self.kind {
141            TransItemSourceKind::ClosureMethod(kind) => {
142                TransItemSourceKind::TraitImpl(TraitImplSource::Closure(kind))
143            }
144            TransItemSourceKind::EmptyDropMethod => {
145                TransItemSourceKind::TraitImpl(TraitImplSource::ImplicitDrop)
146            }
147            TransItemSourceKind::DropInPlaceMethod(Some(impl_kind))
148            | TransItemSourceKind::VTableInstance(impl_kind)
149            | TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
150                TransItemSourceKind::TraitImpl(impl_kind)
151            }
152            TransItemSourceKind::DropInPlaceMethod(None) => TransItemSourceKind::TraitDecl,
153            _ => return None,
154        };
155        Some(self.with_kind(parent_kind))
156    }
157
158    /// Whether this item is the "main" item for this def_id or not (e.g. drop impl/methods are not
159    /// the main item).
160    pub(crate) fn is_derived_item(&self) -> bool {
161        use TransItemSourceKind::*;
162        match self.kind {
163            Global
164            | TraitDecl
165            | TraitImpl(TraitImplSource::Normal)
166            | InherentImpl
167            | Module
168            | Fun
169            | Type => false,
170            _ => true,
171        }
172    }
173
174    /// Value with which we order values.
175    fn sort_key(&self) -> impl Ord + '_ {
176        let item_id = match &self.item {
177            RustcItem::Poly(_) => None,
178            RustcItem::Mono(item) => Some(item.id()),
179        };
180        (self.def_id().index, &self.kind, item_id)
181    }
182}
183
184impl RustcItem {
185    pub fn def_id(&self) -> &hax::DefId {
186        match self {
187            RustcItem::Poly(def_id) => def_id,
188            RustcItem::Mono(item_ref) => &item_ref.def_id,
189        }
190    }
191}
192
193/// Manual impls because `DefId` is not orderable.
194impl PartialOrd for TransItemSource {
195    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
196        Some(self.cmp(other))
197    }
198}
199impl Ord for TransItemSource {
200    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
201        self.sort_key().cmp(&other.sort_key())
202    }
203}
204
205impl<'tcx, 'ctx> TranslateCtx<'tcx> {
206    /// Returns the default translation kind for the given `DefId`. Returns `None` for items that
207    /// we don't translate. Errors on unexpected items.
208    pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
209        use hax::DefKind::*;
210        Some(match &def_id.kind {
211            Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
212                TransItemSourceKind::Type
213            }
214            Fn { .. } | AssocFn { .. } => TransItemSourceKind::Fun,
215            Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
216            Trait { .. } | TraitAlias { .. } => TransItemSourceKind::TraitDecl,
217            Impl { of_trait: true } => TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
218            Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
219            Mod { .. } | ForeignMod { .. } => TransItemSourceKind::Module,
220
221            // We skip these
222            ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => return None,
223            // We cannot encounter these since they're not top-level items.
224            AnonConst { .. }
225            | AssocTy { .. }
226            | Closure { .. }
227            | ConstParam { .. }
228            | Ctor { .. }
229            | Field { .. }
230            | InlineConst { .. }
231            | PromotedConst { .. }
232            | LifetimeParam { .. }
233            | OpaqueTy { .. }
234            | SyntheticCoroutineBody { .. }
235            | TyParam { .. }
236            | Variant { .. } => {
237                let span = self.def_span(def_id);
238                register_error!(
239                    self,
240                    span,
241                    "Cannot register item `{def_id:?}` with kind `{:?}`",
242                    def_id.kind
243                );
244                return None;
245            }
246        })
247    }
248
249    /// Add this item to the queue of items to translate. Each translated item will then
250    /// recursively register the items it refers to. We call this on the crate root and end up
251    /// exploring the whole crate.
252    #[tracing::instrument(skip(self))]
253    pub fn enqueue_module_item(&mut self, def_id: &hax::DefId) {
254        let Some(kind) = self.base_kind_for_item(def_id) else {
255            return;
256        };
257        let item_src = if self.options.monomorphize_with_hax {
258            if let Ok(def) = self.poly_hax_def(def_id)
259                && !def.has_any_generics()
260            {
261                // Monomorphize this item and the items it depends on.
262                TransItemSource::monomorphic(def.this(), kind)
263            } else {
264                // Skip polymorphic items and items that cause errors.
265                return;
266            }
267        } else {
268            TransItemSource::polymorphic(def_id, kind)
269        };
270        let _: Option<ItemId> = self.register_and_enqueue(&None, item_src);
271    }
272
273    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
274        &mut self,
275        dep_src: &Option<DepSource>,
276        src: &TransItemSource,
277    ) -> Option<T> {
278        let item_id = match self.id_map.get(src) {
279            Some(tid) => *tid,
280            None => {
281                use TransItemSourceKind::*;
282                let trans_id = match src.kind {
283                    Type | VTable => ItemId::Type(self.translated.type_decls.reserve_slot()),
284                    TraitDecl => ItemId::TraitDecl(self.translated.trait_decls.reserve_slot()),
285                    TraitImpl(..) => ItemId::TraitImpl(self.translated.trait_impls.reserve_slot()),
286                    Global | VTableInstance(..) => {
287                        ItemId::Global(self.translated.global_decls.reserve_slot())
288                    }
289                    Fun
290                    | ClosureMethod(..)
291                    | ClosureAsFnCast
292                    | EmptyDropMethod
293                    | DropInPlaceMethod(..)
294                    | VTableInstanceInitializer(..)
295                    | VTableMethod => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
296                    InherentImpl | Module => return None,
297                };
298                // Add the id to the queue of declarations to translate
299                self.id_map.insert(src.clone(), trans_id);
300                self.reverse_id_map.insert(trans_id, src.clone());
301                // Store the name early so the name matcher can identify paths.
302                if let Ok(name) = self.translate_name(src) {
303                    self.translated.item_names.insert(trans_id, name);
304                }
305                trans_id
306            }
307        };
308        self.errors
309            .borrow_mut()
310            .register_dep_source(dep_src, item_id, src.def_id().is_local);
311        item_id.try_into().ok()
312    }
313
314    /// Register this item source and enqueue it for translation.
315    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
316        &mut self,
317        dep_src: &Option<DepSource>,
318        item_src: TransItemSource,
319    ) -> Option<T> {
320        let id = self.register_no_enqueue(dep_src, &item_src);
321        self.items_to_translate.insert(item_src);
322        id
323    }
324
325    pub(crate) fn register_target_info(&mut self) {
326        let target_data = &self.tcx.data_layout;
327        self.translated.target_information = krate::TargetInfo {
328            target_pointer_size: target_data.pointer_size().bytes(),
329            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
330        }
331    }
332}
333
334pub struct ItemRef<Id> {
335    id: Id,
336    generics: BoxedArgs,
337}
338
339// Implement `ItemRef<_>` -> `FooDeclRef` conversions.
340macro_rules! convert_item_ref {
341    ($item_ref_ty:ident($id:ident)) => {
342        impl TryFrom<ItemRef<ItemId>> for $item_ref_ty {
343            type Error = ();
344            fn try_from(item: ItemRef<ItemId>) -> Result<Self, ()> {
345                Ok($item_ref_ty {
346                    id: item.id.try_into()?,
347                    generics: item.generics,
348                })
349            }
350        }
351        impl From<ItemRef<$id>> for $item_ref_ty {
352            fn from(item: ItemRef<$id>) -> Self {
353                $item_ref_ty {
354                    id: item.id,
355                    generics: item.generics,
356                }
357            }
358        }
359    };
360}
361convert_item_ref!(TypeDeclRef(TypeId));
362convert_item_ref!(FunDeclRef(FunDeclId));
363convert_item_ref!(MaybeBuiltinFunDeclRef(FunId));
364convert_item_ref!(GlobalDeclRef(GlobalDeclId));
365convert_item_ref!(TraitDeclRef(TraitDeclId));
366convert_item_ref!(TraitImplRef(TraitImplId));
367impl TryFrom<ItemRef<ItemId>> for FnPtr {
368    type Error = ();
369    fn try_from(item: ItemRef<ItemId>) -> Result<Self, ()> {
370        let id: FunId = item.id.try_into()?;
371        Ok(FnPtr::new(id.into(), item.generics))
372    }
373}
374
375// Id and item reference registration.
376impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
377    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
378        Some(DepSource {
379            src_id: self.item_id?,
380            span: self.item_src.def_id().is_local.then_some(span),
381        })
382    }
383
384    /// Register this item source and enqueue it for translation.
385    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
386        &mut self,
387        span: Span,
388        item_src: TransItemSource,
389    ) -> T {
390        let dep_src = self.make_dep_source(span);
391        self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
392    }
393
394    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
395        &mut self,
396        span: Span,
397        src: &TransItemSource,
398    ) -> T {
399        let dep_src = self.make_dep_source(span);
400        self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
401    }
402
403    /// Register this item and maybe enqueue it for translation.
404    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
405        &mut self,
406        span: Span,
407        enqueue: bool,
408        item: &hax::ItemRef,
409        kind: TransItemSourceKind,
410    ) -> T {
411        let item = if self.monomorphize() && item.has_param {
412            item.erase(self.hax_state_with_id())
413        } else {
414            item.clone()
415        };
416        let item_src = TransItemSource::from_item(&item, kind, self.monomorphize());
417        if enqueue {
418            self.register_and_enqueue(span, item_src)
419        } else {
420            self.register_no_enqueue(span, &item_src)
421        }
422    }
423
424    /// Register this item and enqueue it for translation.
425    pub(crate) fn register_item<T: TryFrom<ItemId>>(
426        &mut self,
427        span: Span,
428        item: &hax::ItemRef,
429        kind: TransItemSourceKind,
430    ) -> T {
431        self.register_item_maybe_enqueue(span, true, item, kind)
432    }
433
434    /// Register this item without enqueueing it for translation.
435    #[expect(dead_code)]
436    pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
437        &mut self,
438        span: Span,
439        item: &hax::ItemRef,
440        kind: TransItemSourceKind,
441    ) -> T {
442        self.register_item_maybe_enqueue(span, false, item, kind)
443    }
444
445    /// Register this item and maybe enqueue it for translation.
446    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<ItemRef<ItemId>>>(
447        &mut self,
448        span: Span,
449        enqueue: bool,
450        item: &hax::ItemRef,
451        kind: TransItemSourceKind,
452    ) -> Result<T, Error> {
453        let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, item, kind);
454        let generics = if self.monomorphize() {
455            Ok(GenericArgs::empty())
456        } else {
457            self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)
458        }?;
459        let item = ItemRef {
460            id,
461            generics: Box::new(generics),
462        };
463        Ok(item.try_into().ok().unwrap())
464    }
465
466    /// Register this item and enqueue it for translation.
467    ///
468    /// Note: for `FnPtr`s use `translate_fn_ptr` instead, as this handles late-bound variables
469    /// correctly. For `TypeDeclRef`s use `translate_type_decl_ref` instead, as this correctly
470    /// recognizes built-in types.
471    pub(crate) fn translate_item<T: TryFrom<ItemRef<ItemId>>>(
472        &mut self,
473        span: Span,
474        item: &hax::ItemRef,
475        kind: TransItemSourceKind,
476    ) -> Result<T, Error> {
477        self.translate_item_maybe_enqueue(span, true, item, kind)
478    }
479
480    /// Register this item and don't enqueue it for translation.
481    #[expect(dead_code)]
482    pub(crate) fn translate_item_no_enqueue<T: TryFrom<ItemRef<ItemId>>>(
483        &mut self,
484        span: Span,
485        item: &hax::ItemRef,
486        kind: TransItemSourceKind,
487    ) -> Result<T, Error> {
488        self.translate_item_maybe_enqueue(span, false, item, kind)
489    }
490
491    /// Translate a type def id
492    pub(crate) fn translate_type_decl_ref(
493        &mut self,
494        span: Span,
495        item: &hax::ItemRef,
496    ) -> Result<TypeDeclRef, Error> {
497        match self.recognize_builtin_type(item)? {
498            Some(id) => {
499                let generics =
500                    self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
501                Ok(TypeDeclRef {
502                    id: TypeId::Builtin(id),
503                    generics: Box::new(generics),
504                })
505            }
506            None => self.translate_item(span, item, TransItemSourceKind::Type),
507        }
508    }
509
510    /// Translate a function def id
511    pub(crate) fn translate_fun_item(
512        &mut self,
513        span: Span,
514        item: &hax::ItemRef,
515        kind: TransItemSourceKind,
516    ) -> Result<MaybeBuiltinFunDeclRef, Error> {
517        match self.recognize_builtin_fun(item)? {
518            Some(id) => {
519                let generics =
520                    self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
521                Ok(MaybeBuiltinFunDeclRef {
522                    id: FunId::Builtin(id),
523                    generics: Box::new(generics),
524                })
525            }
526            None => self.translate_item(span, item, kind),
527        }
528    }
529
530    /// Auxiliary function to translate function calls and references to functions.
531    /// Translate a function id applied with some substitutions.
532    #[tracing::instrument(skip(self, span))]
533    pub(crate) fn translate_fn_ptr(
534        &mut self,
535        span: Span,
536        item: &hax::ItemRef,
537        kind: TransItemSourceKind,
538    ) -> Result<RegionBinder<FnPtr>, Error> {
539        let fun_item = self.translate_fun_item(span, item, kind)?;
540        let late_bound = match self.hax_def(item)?.kind() {
541            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
542                Some(sig.as_ref().rebind(()))
543            }
544            _ => None,
545        };
546        let bound_generics =
547            self.append_late_bound_to_generics(span, *fun_item.generics, late_bound)?;
548        let fun_id = match &item.in_trait {
549            // Direct function call
550            None => FnPtrKind::Fun(fun_item.id),
551            // Trait method
552            Some(impl_expr) => {
553                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
554                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
555                let method_decl_id = *fun_item
556                    .id
557                    .as_regular()
558                    .expect("methods are not builtin functions");
559                FnPtrKind::Trait(trait_ref.move_under_binder(), name, method_decl_id)
560            }
561        };
562        Ok(bound_generics.map(|generics| FnPtr::new(fun_id, generics)))
563    }
564
565    pub(crate) fn translate_global_decl_ref(
566        &mut self,
567        span: Span,
568        item: &hax::ItemRef,
569    ) -> Result<GlobalDeclRef, Error> {
570        self.translate_item(span, item, TransItemSourceKind::Global)
571    }
572
573    pub(crate) fn translate_trait_decl_ref(
574        &mut self,
575        span: Span,
576        item: &hax::ItemRef,
577    ) -> Result<TraitDeclRef, Error> {
578        self.translate_item(span, item, TransItemSourceKind::TraitDecl)
579    }
580
581    pub(crate) fn translate_trait_impl_ref(
582        &mut self,
583        span: Span,
584        item: &hax::ItemRef,
585        kind: TraitImplSource,
586    ) -> Result<TraitImplRef, Error> {
587        self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
588    }
589}
590
591#[tracing::instrument(skip(tcx))]
592pub fn translate<'tcx, 'ctx>(
593    options: &CliOpts,
594    tcx: TyCtxt<'tcx>,
595    sysroot: PathBuf,
596) -> TransformCtx {
597    let hax_state = hax::state::State::new(
598        tcx,
599        hax::options::Options {
600            inline_anon_consts: true,
601            bounds_options: hax::options::BoundsOptions {
602                resolve_drop: options.add_drop_bounds,
603                prune_sized: false,
604            },
605        },
606    );
607
608    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
609        .to_def_id()
610        .sinto(&hax_state);
611    let crate_name = crate_def_id.krate.clone();
612    trace!("# Crate: {}", crate_name);
613
614    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
615    let translate_options = TranslateOptions::new(&mut error_ctx, options);
616    let mut ctx = TranslateCtx {
617        tcx,
618        sysroot,
619        hax_state,
620        options: translate_options,
621        errors: RefCell::new(error_ctx),
622        translated: TranslatedCrate {
623            crate_name,
624            options: options.clone(),
625            ..TranslatedCrate::default()
626        },
627        id_map: Default::default(),
628        reverse_id_map: Default::default(),
629        file_to_id: Default::default(),
630        items_to_translate: Default::default(),
631        processed: Default::default(),
632        translate_stack: Default::default(),
633        cached_item_metas: Default::default(),
634        cached_names: Default::default(),
635    };
636    ctx.register_target_info();
637
638    if options.start_from.is_empty() {
639        // Recursively register all the items in the crate, starting from the crate root.
640        ctx.enqueue_module_item(&crate_def_id);
641    } else {
642        // Start translating from the selected items.
643        for path in options.start_from.iter() {
644            let path = path.split("::").collect_vec();
645            let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
646            match resolved {
647                Ok(resolved) => {
648                    for def_id in resolved {
649                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
650                        ctx.enqueue_module_item(&def_id);
651                    }
652                }
653                Err(path) => {
654                    let path = path.join("::");
655                    register_error!(
656                        ctx,
657                        Span::dummy(),
658                        "path {path} does not correspond to any item"
659                    );
660                }
661            }
662        }
663    }
664
665    trace!(
666        "Queue after we explored the crate:\n{:?}",
667        &ctx.items_to_translate
668    );
669
670    ctx.translate_unit_metadata_const();
671
672    // Translate.
673    //
674    // For as long as the queue of items to translate is not empty, we pop the top item and
675    // translate it. If an item refers to non-translated (potentially external) items, we add them
676    // to the queue.
677    //
678    // Note that the order in which we translate the definitions doesn't matter:
679    // we never need to lookup a translated definition, and only use the map
680    // from Rust ids to translated ids.
681    while let Some(item_src) = ctx.items_to_translate.pop_first() {
682        trace!("About to translate item: {:?}", item_src);
683        if ctx.processed.insert(item_src.clone()) {
684            ctx.translate_item(&item_src);
685        }
686    }
687
688    // Return the context, dropping the hax state and rustc `tcx`.
689    TransformCtx {
690        options: ctx.options,
691        translated: ctx.translated,
692        errors: ctx.errors,
693    }
694}