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

charon_driver/translate/
translate_crate.rs
