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_frontend_exporter::{self as 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            && 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            TransItemSource::polymorphic(def_id, kind)
256        };
257        let _: Option<AnyTransId> = self.register_and_enqueue(&None, item_src);
258    }
259
260    pub(crate) fn register_no_enqueue<T: TryFrom<AnyTransId>>(
261        &mut self,
262        dep_src: &Option<DepSource>,
263        src: &TransItemSource,
264    ) -> Option<T> {
265        let item_id = match self.id_map.get(src) {
266            Some(tid) => *tid,
267            None => {
268                use TransItemSourceKind::*;
269                let trans_id = match src.kind {
270                    Type | VTable => AnyTransId::Type(self.translated.type_decls.reserve_slot()),
271                    TraitDecl => AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()),
272                    TraitImpl(..) => {
273                        AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
274                    }
275                    Global | VTableInstance(..) => {
276                        AnyTransId::Global(self.translated.global_decls.reserve_slot())
277                    }
278                    Fun
279                    | ClosureMethod(..)
280                    | ClosureAsFnCast
281                    | DropGlueMethod
282                    | VTableInstanceInitializer(..)
283                    | VTableMethod => AnyTransId::Fun(self.translated.fun_decls.reserve_slot()),
284                    InherentImpl | Module => return None,
285                };
286                // Add the id to the queue of declarations to translate
287                self.id_map.insert(src.clone(), trans_id);
288                self.reverse_id_map.insert(trans_id, src.clone());
289                // Store the name early so the name matcher can identify paths.
290                if let Ok(name) = self.translate_name(src) {
291                    self.translated.item_names.insert(trans_id, name);
292                }
293                trans_id
294            }
295        };
296        self.errors
297            .borrow_mut()
298            .register_dep_source(dep_src, item_id, src.def_id().is_local);
299        item_id.try_into().ok()
300    }
301
302    /// Register this item source and enqueue it for translation.
303    pub(crate) fn register_and_enqueue<T: TryFrom<AnyTransId>>(
304        &mut self,
305        dep_src: &Option<DepSource>,
306        item_src: TransItemSource,
307    ) -> Option<T> {
308        let id = self.register_no_enqueue(dep_src, &item_src);
309        self.items_to_translate.insert(item_src);
310        id
311    }
312
313    pub(crate) fn register_target_info(&mut self) {
314        let target_data = &self.tcx.data_layout;
315        self.translated.target_information = krate::TargetInfo {
316            target_pointer_size: target_data.pointer_size().bytes(),
317            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
318        }
319    }
320}
321
322pub struct ItemRef<Id> {
323    id: Id,
324    generics: BoxedArgs,
325}
326
327// Implement `ItemRef<_>` -> `FooDeclRef` conversions.
328macro_rules! convert_item_ref {
329    ($item_ref_ty:ident($id:ident)) => {
330        impl TryFrom<ItemRef<AnyTransId>> for $item_ref_ty {
331            type Error = ();
332            fn try_from(item: ItemRef<AnyTransId>) -> Result<Self, ()> {
333                Ok($item_ref_ty {
334                    id: item.id.try_into()?,
335                    generics: item.generics,
336                })
337            }
338        }
339        impl From<ItemRef<$id>> for $item_ref_ty {
340            fn from(item: ItemRef<$id>) -> Self {
341                $item_ref_ty {
342                    id: item.id,
343                    generics: item.generics,
344                }
345            }
346        }
347    };
348}
349convert_item_ref!(TypeDeclRef(TypeId));
350convert_item_ref!(FunDeclRef(FunDeclId));
351convert_item_ref!(MaybeBuiltinFunDeclRef(FunId));
352convert_item_ref!(GlobalDeclRef(GlobalDeclId));
353convert_item_ref!(TraitDeclRef(TraitDeclId));
354convert_item_ref!(TraitImplRef(TraitImplId));
355impl TryFrom<ItemRef<AnyTransId>> for FnPtr {
356    type Error = ();
357    fn try_from(item: ItemRef<AnyTransId>) -> Result<Self, ()> {
358        let id: FunId = item.id.try_into()?;
359        Ok(FnPtr {
360            func: Box::new(id.into()),
361            generics: item.generics,
362        })
363    }
364}
365
366// Id and item reference registration.
367impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
368    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
369        Some(DepSource {
370            src_id: self.item_id?,
371            span: self.item_src.def_id().is_local.then_some(span),
372        })
373    }
374
375    /// Register this item source and enqueue it for translation.
376    pub(crate) fn register_and_enqueue<T: TryFrom<AnyTransId>>(
377        &mut self,
378        span: Span,
379        item_src: TransItemSource,
380    ) -> T {
381        let dep_src = self.make_dep_source(span);
382        self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
383    }
384
385    pub(crate) fn register_no_enqueue<T: TryFrom<AnyTransId>>(
386        &mut self,
387        span: Span,
388        src: &TransItemSource,
389    ) -> T {
390        let dep_src = self.make_dep_source(span);
391        self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
392    }
393
394    /// Register this item and maybe enqueue it for translation.
395    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<AnyTransId>>(
396        &mut self,
397        span: Span,
398        enqueue: bool,
399        item: &hax::ItemRef,
400        kind: TransItemSourceKind,
401    ) -> T {
402        let item = if self.monomorphize() && item.has_param {
403            item.erase(&self.hax_state_with_id())
404        } else {
405            item.clone()
406        };
407        let item_src = TransItemSource::from_item(&item, kind, self.monomorphize());
408        if enqueue {
409            self.register_and_enqueue(span, item_src)
410        } else {
411            self.register_no_enqueue(span, &item_src)
412        }
413    }
414
415    /// Register this item and enqueue it for translation.
416    pub(crate) fn register_item<T: TryFrom<AnyTransId>>(
417        &mut self,
418        span: Span,
419        item: &hax::ItemRef,
420        kind: TransItemSourceKind,
421    ) -> T {
422        self.register_item_maybe_enqueue(span, true, item, kind)
423    }
424
425    /// Register this item without enqueueing it for translation.
426    #[expect(dead_code)]
427    pub(crate) fn register_item_no_enqueue<T: TryFrom<AnyTransId>>(
428        &mut self,
429        span: Span,
430        item: &hax::ItemRef,
431        kind: TransItemSourceKind,
432    ) -> T {
433        self.register_item_maybe_enqueue(span, false, item, kind)
434    }
435
436    /// Register this item and maybe enqueue it for translation.
437    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<ItemRef<AnyTransId>>>(
438        &mut self,
439        span: Span,
440        enqueue: bool,
441        item: &hax::ItemRef,
442        kind: TransItemSourceKind,
443    ) -> Result<T, Error> {
444        let id: AnyTransId = self.register_item_maybe_enqueue(span, enqueue, item, kind);
445        let generics = if self.monomorphize() {
446            Ok(GenericArgs::empty())
447        } else {
448            self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)
449        }?;
450        let item = ItemRef {
451            id,
452            generics: Box::new(generics),
453        };
454        Ok(item.try_into().ok().unwrap())
455    }
456
457    /// Register this item and enqueue it for translation.
458    pub(crate) fn translate_item<T: TryFrom<ItemRef<AnyTransId>>>(
459        &mut self,
460        span: Span,
461        item: &hax::ItemRef,
462        kind: TransItemSourceKind,
463    ) -> Result<T, Error> {
464        self.translate_item_maybe_enqueue(span, true, item, kind)
465    }
466
467    /// Register this item and don't enqueue it for translation.
468    pub(crate) fn translate_item_no_enqueue<T: TryFrom<ItemRef<AnyTransId>>>(
469        &mut self,
470        span: Span,
471        item: &hax::ItemRef,
472        kind: TransItemSourceKind,
473    ) -> Result<T, Error> {
474        self.translate_item_maybe_enqueue(span, false, item, kind)
475    }
476
477    /// Translate a type def id
478    pub(crate) fn translate_type_decl_ref(
479        &mut self,
480        span: Span,
481        item: &hax::ItemRef,
482    ) -> Result<TypeDeclRef, Error> {
483        match self.recognize_builtin_type(item)? {
484            Some(id) => {
485                let generics =
486                    self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
487                Ok(TypeDeclRef {
488                    id: TypeId::Builtin(id),
489                    generics: Box::new(generics),
490                })
491            }
492            None => self.translate_item(span, item, TransItemSourceKind::Type),
493        }
494    }
495
496    /// Translate a function def id
497    pub(crate) fn translate_fun_item(
498        &mut self,
499        span: Span,
500        item: &hax::ItemRef,
501    ) -> Result<MaybeBuiltinFunDeclRef, Error> {
502        match self.recognize_builtin_fun(item)? {
503            Some(id) => {
504                let generics =
505                    self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
506                Ok(MaybeBuiltinFunDeclRef {
507                    id: FunId::Builtin(id),
508                    generics: Box::new(generics),
509                })
510            }
511            None => self.translate_item(span, item, TransItemSourceKind::Fun),
512        }
513    }
514
515    /// Auxiliary function to translate function calls and references to functions.
516    /// Translate a function id applied with some substitutions.
517    #[tracing::instrument(skip(self, span))]
518    pub(crate) fn translate_fn_ptr(
519        &mut self,
520        span: Span,
521        item: &hax::ItemRef,
522    ) -> Result<RegionBinder<FnPtr>, Error> {
523        let fun_item = self.translate_fun_item(span, item)?;
524        let late_bound = match self.hax_def(item)?.kind() {
525            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
526                Some(sig.as_ref().rebind(()))
527            }
528            _ => None,
529        };
530        let bound_generics =
531            self.append_late_bound_to_generics(span, *fun_item.generics, late_bound)?;
532        let fun_id = match &item.in_trait {
533            // Direct function call
534            None => FunIdOrTraitMethodRef::Fun(fun_item.id),
535            // Trait method
536            Some(impl_expr) => {
537                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
538                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
539                let method_decl_id = *fun_item
540                    .id
541                    .as_regular()
542                    .expect("methods are not builtin functions");
543                FunIdOrTraitMethodRef::Trait(trait_ref.move_under_binder(), name, method_decl_id)
544            }
545        };
546        Ok(bound_generics.map(|generics| FnPtr {
547            func: Box::new(fun_id),
548            generics: Box::new(generics),
549        }))
550    }
551
552    pub(crate) fn translate_global_decl_ref(
553        &mut self,
554        span: Span,
555        item: &hax::ItemRef,
556    ) -> Result<GlobalDeclRef, Error> {
557        self.translate_item(span, item, TransItemSourceKind::Global)
558    }
559
560    pub(crate) fn translate_trait_decl_ref(
561        &mut self,
562        span: Span,
563        item: &hax::ItemRef,
564    ) -> Result<TraitDeclRef, Error> {
565        self.translate_item(span, item, TransItemSourceKind::TraitDecl)
566    }
567
568    pub(crate) fn translate_trait_impl_ref(
569        &mut self,
570        span: Span,
571        item: &hax::ItemRef,
572        kind: TraitImplSource,
573    ) -> Result<TraitImplRef, Error> {
574        self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
575    }
576}
577
578#[tracing::instrument(skip(tcx))]
579pub fn translate<'tcx, 'ctx>(
580    options: &CliOpts,
581    tcx: TyCtxt<'tcx>,
582    sysroot: PathBuf,
583) -> TransformCtx {
584    let hax_state = hax::state::State::new(
585        tcx,
586        hax::options::Options {
587            inline_anon_consts: true,
588            resolve_drop_bounds: options.add_drop_bounds,
589        },
590    );
591
592    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
593        .to_def_id()
594        .sinto(&hax_state);
595    let crate_name = crate_def_id.krate.clone();
596    trace!("# Crate: {}", crate_name);
597
598    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
599    let translate_options = TranslateOptions::new(&mut error_ctx, options);
600    let mut ctx = TranslateCtx {
601        tcx,
602        sysroot,
603        hax_state,
604        options: translate_options,
605        errors: RefCell::new(error_ctx),
606        translated: TranslatedCrate {
607            crate_name,
608            options: options.clone(),
609            ..TranslatedCrate::default()
610        },
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 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 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    // Translate.
655    //
656    // For as long as the queue of items to translate is not empty, we pop the top item and
657    // translate it. If an item refers to non-translated (potentially external) items, we add them
658    // to the queue.
659    //
660    // Note that the order in which we translate the definitions doesn't matter:
661    // we never need to lookup a translated definition, and only use the map
662    // from Rust ids to translated ids.
663    while let Some(item_src) = ctx.items_to_translate.pop_first() {
664        trace!("About to translate item: {:?}", item_src);
665        if ctx.processed.insert(item_src.clone()) {
666            ctx.translate_item(&item_src);
667        }
668    }
669
670    // Return the context, dropping the hax state and rustc `tcx`.
671    TransformCtx {
672        options: ctx.options,
673        translated: ctx.translated,
674        errors: ctx.errors,
675    }
676}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
