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

charon_driver/translate/
translate_crate.rs
