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

charon_driver/translate/
translate_crate.rs
