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::{self, TyCtxt};
19use rustc_span::{def_id::DefId, sym};
20use std::cell::RefCell;
21use std::collections::HashSet;
22use std::path::PathBuf;
23
24use super::translate_ctx::*;
25use crate::hax;
26use crate::hax::SInto;
27use charon_lib::ast::*;
28use charon_lib::name_matcher::NamePattern;
29use charon_lib::options::{CliOpts, StartFrom, TranslateOptions};
30use charon_lib::transform::TransformCtx;
31use macros::VariantIndexArity;
32
33/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
34/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
35/// `FunDecl` one (for its initializer function).
36#[derive(Clone, Debug, PartialEq, Eq, Hash)]
37pub struct TransItemSource {
38    pub item: RustcItem,
39    pub kind: TransItemSourceKind,
40}
41
42/// Refers to a rustc item. Can be either the polymorphic version (`Poly`) of the item, or a
43/// monomorphization (`Mono` or `MonoTrait`) of it.
44/// For `MonoTrait` items, their kind should be either `trait decl` or `struct vtable`:
45///     1. the trait is translated as in poly mode, except that we don't translate any of its
46///        associated item lists.
47///     2. the vtable is translated with erased signature of the methods and without generic types.
48///        In other words, there is one "opaque" vtable per trait.
49#[derive(Clone, Debug, PartialEq, Eq, Hash)]
50pub enum RustcItem {
51    Poly(hax::DefId),
52    Mono(hax::ItemRef),
53    MonoTrait(hax::DefId),
54}
55
56/// The kind of a [`TransItemSource`].
57#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
58pub enum TransItemSourceKind {
59    Global,
60    TraitDecl,
61    TraitImpl(TransImplSource),
62    Fun,
63    Type,
64    /// We don't translate these as proper items, but we translate them a bit in names.
65    InherentImpl,
66    /// We don't translate these as proper items, but we use them to explore the crate.
67    Module,
68    /// The `call_*` method of the generated `Fn*` impl for a closure or fn item.
69    CallableMethod(ClosureKind),
70    /// A cast of a stateless closure to a function pointer.
71    ClosureAsFnCast,
72    /// The `drop_glue` method of a `Destruct` impl. It contains the drop glue that calls
73    /// `Drop::drop` for the type and then drops its fields. This is a method implementation (and
74    /// the DefId is that of the ADT or closure for which to generate the drop glue).
75    DropGlueMethod(TransImplSource),
76    /// The virtual table struct definition for a trait. The `DefId` is that of the trait.
77    VTable,
78    /// The static vtable value for a specific impl.
79    VTableInstance(TransImplSource),
80    /// The initializer function of the `VTableInstance`.
81    VTableInstanceInitializer(TransImplSource),
82    /// Shim function to store a method in a vtable; give a method with `self: Ptr<Self>` argument,
83    /// this takes a `Ptr<dyn Trait>` and forwards to the method. For a `Normal` impl the `DefId`
84    /// refers to the method implementation; for a `Callable` one it refers to the closure or fn
85    /// item, whose `call_*` method has no `DefId` of its own.
86    VTableMethod(TransImplSource),
87    /// The drop shim function to be used in the vtable as a field.
88    VTableDropShim(TransImplSource),
89}
90
91/// The kind of a [`TransItemSourceKind::TraitImpl`].
92#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
93pub enum TransImplSource {
94    /// A user-written trait impl with a `DefId`.
95    Normal,
96    /// The blanket impl we generate for a trait alias. The `DefId` is that of the trait alias.
97    TraitAlias,
98    /// An impl of the appropriate `Fn*` trait for a closure or function item.
99    Callable(ClosureKind),
100    /// A fictitious `impl Destruct for T` that contains the drop glue code for the given ADT or
101    /// closure. The `DefId` is that of the ADT or closure.
102    ImplicitDestruct,
103    /// A marker-trait implementation. The `DefId` is that of the trait.
104    Marker,
105}
106
107impl TransItemSource {
108    pub fn new(item: RustcItem, kind: TransItemSourceKind) -> Self {
109        if let RustcItem::Mono(item) = &item {
110            if item.has_non_lt_param {
111                panic!("Item is not monomorphic: {item:?}")
112            }
113        } else if let RustcItem::MonoTrait(_) = &item
114            && !matches!(
115                kind,
116                TransItemSourceKind::TraitDecl | TransItemSourceKind::VTable
117            )
118        {
119            panic!("Item kind {kind:?} should not be translated as monomorphic_trait")
120        }
121        Self { item, kind }
122    }
123
124    /// Refers to the given item. Depending on `monomorphize`, this chooses between the monomorphic
125    /// and polymorphic versions of the item.
126    pub fn from_item(item: &hax::ItemRef, kind: TransItemSourceKind, monomorphize: bool) -> Self {
127        if monomorphize {
128            if kind.is_for_trait() {
129                Self::monomorphic_trait(&item.def_id, kind)
130            } else {
131                Self::monomorphic(item, kind)
132            }
133        } else {
134            Self::polymorphic(&item.def_id, kind)
135        }
136    }
137
138    /// Refers to the polymorphic version of this item.
139    pub fn polymorphic(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
140        Self::new(RustcItem::Poly(def_id.clone()), kind)
141    }
142
143    /// Refers to the monomorphic version of this item.
144    pub fn monomorphic(item: &hax::ItemRef, kind: TransItemSourceKind) -> Self {
145        Self::new(RustcItem::Mono(item.clone()), kind)
146    }
147
148    /// Refers to the monomorphic trait (or vtable).
149    /// See the docs of `RustcItem::MonoTrait` for details.
150    pub fn monomorphic_trait(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
151        Self::new(RustcItem::MonoTrait(def_id.clone()), kind)
152    }
153
154    pub fn def_id(&self) -> &hax::DefId {
155        self.item.def_id()
156    }
157
158    /// Keep the same def_id but change the kind.
159    pub(crate) fn with_kind(&self, kind: TransItemSourceKind) -> Self {
160        let mut ret = self.clone();
161        ret.kind = kind;
162        ret
163    }
164
165    /// For virtual items that have a parent (typically a method impl), return this parent. Does
166    /// not attempt to generally compute the parent of an item. Used to compute names.
167    pub(crate) fn parent(&self) -> Option<Self> {
168        let parent_kind = match self.kind {
169            TransItemSourceKind::CallableMethod(kind)
170            | TransItemSourceKind::VTableMethod(TransImplSource::Callable(kind)) => {
171                TransItemSourceKind::TraitImpl(TransImplSource::Callable(kind))
172            }
173            TransItemSourceKind::DropGlueMethod(TransImplSource::Marker)
174            | TransItemSourceKind::VTableInstance(TransImplSource::Marker)
175            | TransItemSourceKind::VTableInstanceInitializer(TransImplSource::Marker)
176            | TransItemSourceKind::VTableDropShim(TransImplSource::Marker) => {
177                TransItemSourceKind::TraitDecl
178            }
179            TransItemSourceKind::DropGlueMethod(impl_kind)
180            | TransItemSourceKind::VTableInstance(impl_kind)
181            | TransItemSourceKind::VTableInstanceInitializer(impl_kind)
182            | TransItemSourceKind::VTableDropShim(impl_kind) => {
183                TransItemSourceKind::TraitImpl(impl_kind)
184            }
185            _ => return None,
186        };
187        Some(self.with_kind(parent_kind))
188    }
189
190    /// Whether this item is the "main" item for this def_id or not (e.g. Destruct impl/methods are not
191    /// the main item).
192    pub(crate) fn is_derived_item(&self) -> bool {
193        self.kind.is_derived_item()
194    }
195}
196
197impl TransItemSourceKind {
198    fn is_derived_item(self) -> bool {
199        use TransItemSourceKind::*;
200        !matches!(
201            self,
202            Global
203                | TraitDecl
204                | TraitImpl(TransImplSource::Normal)
205                | InherentImpl
206                | Module
207                | Fun
208                | Type
209        )
210    }
211
212    pub fn is_for_trait(&self) -> bool {
213        matches!(
214            self,
215            TransItemSourceKind::TraitDecl | TransItemSourceKind::VTable
216        )
217    }
218}
219
220impl RustcItem {
221    pub fn def_id(&self) -> &hax::DefId {
222        match self {
223            RustcItem::Poly(def_id) => def_id,
224            RustcItem::Mono(item_ref) => &item_ref.def_id,
225            RustcItem::MonoTrait(def_id) => def_id,
226        }
227    }
228}
229
230impl<'tcx> TranslateCtx<'tcx> {
231    /// If this is a method declaration without a default, return the `DefId` of its parent trait.
232    fn is_method_decl_without_default(&mut self, def_id: &hax::DefId) -> Option<hax::DefId> {
233        if matches!(def_id.kind, hax::DefKind::AssocFn)
234            && let def = self.poly_hax_def(def_id).ok()?
235            && let hax::FullDefKind::AssocFn {
236                associated_item, ..
237            } = def.kind()
238            && !associated_item.has_value
239            && let hax::AssocItemContainer::TraitContainer { trait_ref } =
240                &associated_item.container
241        {
242            Some(trait_ref.def_id.clone())
243        } else {
244            None
245        }
246    }
247
248    /// Resolve a path to a list of matching `DefId`s.
249    pub fn resolve_path(
250        &self,
251        span: Span,
252        pat: &NamePattern,
253        strict: bool,
254    ) -> Result<Vec<rustc_span::def_id::DefId>, Error> {
255        super::resolve_path::def_path_def_ids(&self.hax_state, pat, strict).map_err(|err| {
256            register_error!(self, span, "failed to resolve item path `{pat}`: {err}")
257        })
258    }
259
260    /// Resolve a path that is expected to name exactly one item.
261    pub fn resolve_single_path(
262        &self,
263        span: Span,
264        pat: &NamePattern,
265    ) -> Result<rustc_span::def_id::DefId, Error> {
266        self.resolve_path(span, pat, true)?
267            .into_iter()
268            .exactly_one()
269            .map_err(|_| register_error!(self, span, "expected exactly one item for path `{pat}`"))
270    }
271
272    fn register_polymorphic_function(&mut self, def_id: DefId) -> FunDeclId {
273        let def_id = def_id.sinto(&self.hax_state);
274        let item = TransItemSource::polymorphic(&def_id, TransItemSourceKind::Fun);
275        self.register_and_enqueue(&None, item).unwrap()
276    }
277
278    fn register_poly_function_by_path(&mut self, path: &str) -> Result<FunDeclId, Error> {
279        let path = NamePattern::parse(path).unwrap();
280        let def_id = self.resolve_single_path(Span::dummy(), &path)?;
281        Ok(self.register_polymorphic_function(def_id))
282    }
283
284    /// Register the std functions needed for `builtins_to_function_calls`.
285    fn register_builtin_functions(&mut self) -> Result<(), Error> {
286        if self.options.ops_to_function_calls {
287            self.register_poly_function_by_path("array::as_slice")?;
288            self.register_poly_function_by_path("array::as_mut_slice")?;
289            self.register_poly_function_by_path("core::array::repeat")?;
290        }
291        if self.options.index_to_function_calls {
292            let tcx = self.tcx;
293            for (trait_id, method_name) in [
294                (tcx.lang_items().index_trait().unwrap(), sym::index),
295                (tcx.lang_items().index_mut_trait().unwrap(), sym::index_mut),
296            ] {
297                let impls = tcx.all_impls(trait_id).filter(|&impl_id| {
298                    matches!(
299                        tcx.impl_trait_ref(impl_id).skip_binder().self_ty().kind(),
300                        ty::Array(..) | ty::Slice(..)
301                    )
302                });
303                for impl_id in impls {
304                    let method_id = tcx
305                        .associated_items(impl_id)
306                        .in_definition_order()
307                        .find(|item| item.name() == method_name)
308                        .unwrap()
309                        .def_id;
310                    self.register_polymorphic_function(method_id);
311                }
312            }
313            let trait_id = self.tcx.get_diagnostic_item(sym::SliceIndex).unwrap();
314            let impls = self.tcx.all_impls(trait_id).filter(|&impl_id| {
315                let trait_ref = tcx.impl_trait_ref(impl_id).skip_binder();
316                trait_ref.args.type_at(1).is_slice()
317                    && match trait_ref.self_ty().kind() {
318                        ty::Uint(ty::UintTy::Usize) => true,
319                        ty::Adt(def, args) => {
320                            tcx.is_lang_item(def.did(), rustc_attr_ir::LangItem::Range)
321                                && args.type_at(0) == tcx.types.usize
322                        }
323                        _ => false,
324                    }
325            });
326            for impl_id in impls {
327                let methods = tcx
328                    .associated_items(impl_id)
329                    .in_definition_order()
330                    .filter(|item| item.name() == sym::index || item.name() == sym::index_mut)
331                    .map(|item| item.def_id);
332                for method_id in methods {
333                    self.register_polymorphic_function(method_id);
334                }
335            }
336        }
337        Ok(())
338    }
339
340    /// Returns the default translation kind for the given `DefId`. Returns `None` for items that
341    /// we don't translate. Errors on unexpected items.
342    pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
343        use crate::hax::DefKind::*;
344        Some(match &def_id.kind {
345            Enum | Struct | Union | TyAlias | ForeignTy => TransItemSourceKind::Type,
346            Fn | AssocFn => TransItemSourceKind::Fun,
347            Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
348            Trait | TraitAlias => TransItemSourceKind::TraitDecl,
349            Impl { of_trait: true } => TransItemSourceKind::TraitImpl(TransImplSource::Normal),
350            Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
351            Mod | ForeignMod => TransItemSourceKind::Module,
352
353            // We skip these
354            ExternCrate | GlobalAsm | Macro { .. } | Use => return None,
355            // These can happen when doing `--start-from` on a foreign crate. We can skip them
356            // because their parents will already have been registered.
357            Ctor { .. } | Variant => return None,
358            // We cannot encounter these since they're not top-level items.
359            AnonConst
360            | AssocTy
361            | Closure
362            | ConstParam
363            | Field
364            | PromotedConst
365            | LifetimeParam
366            | OpaqueTy
367            | SyntheticCoroutineBody
368            | TyParam => {
369                let span = self.def_span(def_id);
370                register_error!(
371                    self,
372                    span,
373                    "Cannot register item `{def_id:?}` with kind `{:?}`",
374                    def_id.kind
375                );
376                return None;
377            }
378        })
379    }
380
381    /// Add this item to the queue of items to translate. Each translated item will then
382    /// recursively register the items it refers to. We call this on the crate root and end up
383    /// exploring the whole crate.
384    #[tracing::instrument(skip(self))]
385    pub fn enqueue_module_item(&mut self, def_id: &hax::DefId) {
386        if let Some(trait_def_id) = self.is_method_decl_without_default(def_id) {
387            // Don't translate the method itself as it doesn't correspond to an item, translate the
388            // trait instead.
389            self.enqueue_module_item(&trait_def_id);
390            return;
391        }
392        let Some(kind) = self.base_kind_for_item(def_id) else {
393            return;
394        };
395        let item_src = if self.options.monomorphize_with_hax {
396            if let Ok(def) = self.poly_hax_def(def_id)
397                && !def.has_any_generics()
398            {
399                // Monomorphize this item and the items it depends on.
400                TransItemSource::monomorphic(def.this(), kind)
401            } else {
402                // Skip polymorphic items and items that cause errors.
403                return;
404            }
405        } else {
406            TransItemSource::polymorphic(def_id, kind)
407        };
408        let _: Option<ItemId> = self.register_and_enqueue(&None, item_src);
409    }
410
411    /// Whether this item is polymorphic, while we are in monomorphic mode.
412    pub(crate) fn is_poly_in_mono(&self, item_src: &TransItemSource) -> bool {
413        self.options.monomorphize_with_hax && matches!(item_src.item, RustcItem::Poly(..))
414    }
415
416    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
417        &mut self,
418        dep_src: &Option<DepSource>,
419        src: &TransItemSource,
420    ) -> Option<T> {
421        let item_id = match self.id_map.get(src) {
422            Some(tid) => *tid,
423            None => {
424                use TransItemSourceKind::*;
425                let trans_id = match src.kind {
426                    Type | VTable => ItemId::Type(self.translated.type_decls.reserve_slot()),
427                    TraitDecl => ItemId::TraitDecl(self.translated.trait_decls.reserve_slot()),
428                    TraitImpl(..) => ItemId::TraitImpl(self.translated.trait_impls.reserve_slot()),
429                    Global | VTableInstance(..) => {
430                        ItemId::Global(self.translated.global_decls.reserve_slot())
431                    }
432                    Fun
433                    | CallableMethod(..)
434                    | ClosureAsFnCast
435                    | DropGlueMethod(..)
436                    | VTableInstanceInitializer(..)
437                    | VTableMethod(..)
438                    | VTableDropShim(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
439                    InherentImpl | Module => return None,
440                };
441                // Add the id to the queue of declarations to translate
442                self.id_map.insert(src.clone(), trans_id);
443                self.reverse_id_map.insert(trans_id, src.clone());
444                // Store the name early so the name matcher can identify paths.
445                if let Ok(name) = self.translate_name(src) {
446                    self.translated.item_names.insert(trans_id, name);
447                }
448                trans_id
449            }
450        };
451        self.errors
452            .borrow_mut()
453            .register_dep_source(dep_src, item_id, src.def_id().is_local());
454        item_id.try_into().ok()
455    }
456
457    /// Register this item source and enqueue it for translation.
458    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
459        &mut self,
460        dep_src: &Option<DepSource>,
461        item_src: TransItemSource,
462    ) -> Option<T> {
463        let id = self.register_no_enqueue(dep_src, &item_src);
464        self.items_to_translate.push_back(item_src);
465        id
466    }
467
468    /// Enqueue an item from its id.
469    pub(crate) fn enqueue_id(&mut self, id: impl Into<ItemId>) {
470        let id = id.into();
471        if self.translated.get_item(id).is_none() {
472            let item_src = self.reverse_id_map[&id].clone();
473            self.items_to_translate.push_back(item_src);
474        }
475    }
476
477    /// Register the associated types of this trait.
478    pub fn register_assoc_items(
479        &mut self,
480        trait_def_id: &hax::DefId,
481        trait_id: TraitDeclId,
482    ) -> Result<(), Error> {
483        if self.method_status.get(trait_id).is_some() {
484            return Ok(());
485        }
486        let trait_def = self.poly_hax_def(trait_def_id)?;
487        let hax::FullDefKind::Trait { items, .. } = trait_def.kind() else {
488            unreachable!()
489        };
490        let names = self
491            .translated
492            .assoc_item_names
493            .get_or_insert_with(trait_id, Default::default);
494        for item in items {
495            let name = TraitItemName(
496                item.name
497                    .as_ref()
498                    .map(|n| n.to_string().into())
499                    .unwrap_or_default(),
500            );
501            let id: AssocItemId = match item.kind {
502                hax::AssocKind::Type { .. } => names.types.push(name).into(),
503                hax::AssocKind::Fn { .. } => names.methods.push(name).into(),
504                hax::AssocKind::Const { .. } => names.consts.push(name).into(),
505            };
506            self.assoc_item_id_map.insert(item.def_id.clone(), id);
507        }
508        // Add a virtual method to the `Destruct` trait.
509        if trait_def.lang_item == Some(sym::destruct) {
510            let method_name = TraitItemName("drop_glue".into());
511            names.methods.push(method_name);
512        }
513        self.method_status.get_or_insert_with(trait_id, || {
514            names.methods.map_ref(|_| MethodStatus::default())
515        });
516        Ok(())
517    }
518
519    /// Get the unique per-trait id corresponding to this associated item. The `DefId` can be of an
520    /// item declaration or item implementation.
521    pub fn translate_assoc_item_id(
522        &mut self,
523        trait_id: TraitDeclId,
524        item_def_id: &hax::DefId,
525    ) -> Result<AssocItemId, Error> {
526        // The same assoc item `DefId` could belong to several `TraitDeclId`s because of
527        // monomorphization, so we only return the item id if we know this trait's data is
528        // initialized.
529        if let Some(&item_id) = self.assoc_item_id_map.get(item_def_id)
530            && self.method_status.get(trait_id).is_some()
531        {
532            return Ok(item_id);
533        }
534
535        let item_def = self.poly_hax_def(item_def_id)?;
536        let assoc = match item_def.kind() {
537            hax::FullDefKind::AssocTy {
538                associated_item, ..
539            }
540            | hax::FullDefKind::AssocConst {
541                associated_item, ..
542            }
543            | hax::FullDefKind::AssocFn {
544                associated_item, ..
545            } => associated_item,
546            _ => panic!("Unexpected def for associated item: {item_def:?}"),
547        };
548        let decl_def_id = assoc.implemented_trait_item_id();
549
550        if decl_def_id != item_def_id
551            && let Some(&item_id) = self.assoc_item_id_map.get(decl_def_id)
552            && self.method_status.get(trait_id).is_some()
553        {
554            self.assoc_item_id_map.insert(item_def_id.clone(), item_id);
555            return Ok(item_id);
556        }
557
558        let trait_def_id = decl_def_id.parent(&self.hax_state).unwrap();
559        self.register_assoc_items(&trait_def_id, trait_id)?;
560        let item_id = *self.assoc_item_id_map.get(decl_def_id).unwrap();
561        Ok(item_id)
562    }
563
564    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
565    /// This does not make the method be considered "used"; use `mark_method_as_used` for that.
566    pub fn translate_trait_method_id_no_enqueue(
567        &mut self,
568        trait_id: TraitDeclId,
569        def_id: &hax::DefId,
570    ) -> Result<TraitMethodId, Error> {
571        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
572        Ok(*item_id.as_method().unwrap())
573    }
574    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
575    /// This makes the method be considered "used".
576    pub fn translate_trait_method_id(
577        &mut self,
578        trait_id: TraitDeclId,
579        def_id: &hax::DefId,
580    ) -> Result<TraitMethodId, Error> {
581        let method_id = self.translate_trait_method_id_no_enqueue(trait_id, def_id)?;
582        self.mark_method_as_used(trait_id, method_id);
583        Ok(method_id)
584    }
585    /// Register a trait associated type and return its `AssocTypeId`. This id is unique per trait.
586    pub fn translate_assoc_type_id(
587        &mut self,
588        trait_id: TraitDeclId,
589        def_id: &hax::DefId,
590    ) -> Result<AssocTypeId, Error> {
591        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
592        Ok(*item_id.as_type().unwrap())
593    }
594    /// Register a trait associated const and return its `AssocTypeId`. This id is unique per trait.
595    pub fn translate_assoc_const_id(
596        &mut self,
597        trait_id: TraitDeclId,
598        def_id: &hax::DefId,
599    ) -> Result<AssocConstId, Error> {
600        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
601        Ok(*item_id.as_const().unwrap())
602    }
603
604    /// Claim the first type id for the declaration of the unit type.
605    pub(crate) fn reserve_unit_decl(&mut self) {
606        let def_id = hax::DefId::make_synthetic(&self.hax_state, hax::SyntheticItem::Tuple(0));
607        let item_src = if self.options.monomorphize_with_hax
608            && let Ok(def) = self.poly_hax_def(&def_id)
609        {
610            TransItemSource::monomorphic(def.this(), TransItemSourceKind::Type)
611        } else {
612            TransItemSource::polymorphic(&def_id, TransItemSourceKind::Type)
613        };
614        let id: Option<TypeDeclId> = if self.options.no_gen_tuple_structs {
615            self.register_and_enqueue(&None, item_src)
616        } else {
617            self.register_no_enqueue(&None, &item_src)
618        };
619        assert_eq!(id, Some(TypeDeclId::UNIT), "the unit type must come first");
620    }
621
622    pub(crate) fn register_target_info(&mut self) {
623        let target_data = &self.tcx.data_layout;
624        let triple = self.get_target_triple();
625
626        let mut primitive_alignments = SeqHashMap::new();
627        primitive_alignments.insert(ScalarTy::Bool, target_data.i8_align.bytes());
628        for (ty, alignment) in [
629            (IntegerTy::Signed(IntTy::I8), target_data.i8_align.bytes()),
630            (IntegerTy::Signed(IntTy::I16), target_data.i16_align.bytes()),
631            (IntegerTy::Signed(IntTy::I32), target_data.i32_align.bytes()),
632            (IntegerTy::Signed(IntTy::I64), target_data.i64_align.bytes()),
633            (
634                IntegerTy::Signed(IntTy::I128),
635                target_data.i128_align.bytes(),
636            ),
637            (
638                IntegerTy::Signed(IntTy::Isize),
639                target_data.pointer_align().bytes(),
640            ),
641            (
642                IntegerTy::Unsigned(UIntTy::U8),
643                target_data.i8_align.bytes(),
644            ),
645            (
646                IntegerTy::Unsigned(UIntTy::U16),
647                target_data.i16_align.bytes(),
648            ),
649            (
650                IntegerTy::Unsigned(UIntTy::U32),
651                target_data.i32_align.bytes(),
652            ),
653            (
654                IntegerTy::Unsigned(UIntTy::U64),
655                target_data.i64_align.bytes(),
656            ),
657            (
658                IntegerTy::Unsigned(UIntTy::U128),
659                target_data.i128_align.bytes(),
660            ),
661            (
662                IntegerTy::Unsigned(UIntTy::Usize),
663                target_data.pointer_align().bytes(),
664            ),
665        ] {
666            primitive_alignments.insert(ScalarTy::Integer(ty), alignment);
667        }
668        primitive_alignments.insert(ScalarTy::Float(FloatTy::F16), target_data.f16_align.bytes());
669        primitive_alignments.insert(ScalarTy::Float(FloatTy::F32), target_data.f32_align.bytes());
670        primitive_alignments.insert(ScalarTy::Float(FloatTy::F64), target_data.f64_align.bytes());
671        primitive_alignments.insert(
672            ScalarTy::Float(FloatTy::F128),
673            target_data.f128_align.bytes(),
674        );
675        // INFO: This is not explicitly guaranteed by the reference, but by the implementation of rustc.
676        // https://doc.rust-lang.org/1.97.1/nightly-rustc/src/rustc_ty_utils/layout.rs.html#391
677        primitive_alignments.insert(ScalarTy::Char, target_data.i32_align.bytes());
678
679        let c_enum_smallest_repr_ty = match target_data.c_enum_min_size {
680            rustc_abi::Integer::I8 => IntTy::I8,
681            rustc_abi::Integer::I16 => IntTy::I16,
682            rustc_abi::Integer::I32 => IntTy::I32,
683            rustc_abi::Integer::I64 => IntTy::I64,
684            rustc_abi::Integer::I128 => IntTy::I128,
685        };
686
687        let info = TargetInfo {
688            target_pointer_size: target_data.pointer_size().bytes(),
689            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
690            c_enum_smallest_repr_ty,
691            primitive_alignments,
692        };
693        self.translated.target_information.insert(triple, info);
694    }
695}
696
697// Id and item reference registration.
698impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
699    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
700        Some(DepSource {
701            src_id: self.item_id?,
702            span: self.item_src.def_id().is_local().then_some(span),
703        })
704    }
705
706    /// Register this item source and enqueue it for translation.
707    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
708        &mut self,
709        span: Span,
710        item_src: TransItemSource,
711    ) -> T {
712        let dep_src = self.make_dep_source(span);
713        self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
714    }
715
716    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
717        &mut self,
718        span: Span,
719        src: &TransItemSource,
720    ) -> T {
721        let dep_src = self.make_dep_source(span);
722        self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
723    }
724
725    /// Register this item and maybe enqueue it for translation.
726    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
727        &mut self,
728        span: Span,
729        enqueue: bool,
730        item: &hax::ItemRef,
731        kind: TransItemSourceKind,
732    ) -> T {
733        let item = if self.monomorphize() && item.has_param {
734            item.erase(self.hax_state_with_id())
735        } else {
736            item.clone()
737        };
738        // In mono mode:
739        //   1. If the item being registered is a `trait decl`, we construct a
740        //      `monomorphic_trait` item source.
741        //   2. Otherwise, if the current `item_trans_ctx` is under a `trait decl`
742        //      or a `vtable`, we construct a `poly` item.
743        //   3. In all other cases, we construct a `mono` item.
744        let mono =
745            self.monomorphize() && (kind.is_for_trait() || !self.item_src.kind.is_for_trait());
746        let item_src = TransItemSource::from_item(&item, kind, mono);
747        if enqueue {
748            self.register_and_enqueue(span, item_src)
749        } else {
750            self.register_no_enqueue(span, &item_src)
751        }
752    }
753
754    /// Register this item and enqueue it for translation.
755    pub(crate) fn register_item<T: TryFrom<ItemId>>(
756        &mut self,
757        span: Span,
758        item: &hax::ItemRef,
759        kind: TransItemSourceKind,
760    ) -> T {
761        self.register_item_maybe_enqueue(span, true, item, kind)
762    }
763
764    /// Register this item without enqueueing it for translation.
765    #[expect(dead_code)]
766    pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
767        &mut self,
768        span: Span,
769        item: &hax::ItemRef,
770        kind: TransItemSourceKind,
771    ) -> T {
772        self.register_item_maybe_enqueue(span, false, item, kind)
773    }
774
775    /// Register this item and maybe enqueue it for translation.
776    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<DeclRef<ItemId>>>(
777        &mut self,
778        span: Span,
779        hax_item: &hax::ItemRef,
780        kind: TransItemSourceKind,
781        enqueue: bool,
782    ) -> Result<T, Error> {
783        let hax_item = if kind.is_derived_item() {
784            // If the original item is an associated item we should ignore that and refer to it
785            // like a top-level item.
786            &hax_item.re_resolve(self.hax_state_with_id(), hax::AssocItemResolution::None)
787        } else {
788            hax_item
789        };
790
791        let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, hax_item, kind);
792        // In mono mode, we keep trait decls generic.
793        let mut generics = if self.monomorphize() && !matches!(kind, TransItemSourceKind::TraitDecl)
794        {
795            GenericArgs::empty()
796        } else {
797            self.translate_generic_args(span, &hax_item.generic_args, &hax_item.trait_proofs)?
798        };
799
800        // Add regions to make sure the item args match the params we set up in
801        // `translate_item_generics`.
802        if matches!(
803            hax_item.def_id.kind,
804            hax::DefKind::Fn
805                | hax::DefKind::AssocFn
806                | hax::DefKind::Closure
807                | hax::DefKind::Ctor(..)
808        ) {
809            let def = self.hax_def(hax_item)?;
810            match def.kind() {
811                hax::FullDefKind::Fn { sig, .. }
812                | hax::FullDefKind::AssocFn { sig, .. }
813                | hax::FullDefKind::Ctor { sig, .. } => {
814                    generics.regions.extend(
815                        sig.bound_vars
816                            .iter()
817                            .map(|_| self.translate_erased_region()),
818                    );
819                }
820                hax::FullDefKind::Closure { args, .. } => {
821                    let upvar_regions = if self.item_src.def_id() == &args.item.def_id {
822                        assert!(self.outermost_binder().closure_upvar_tys.is_some());
823                        self.outermost_binder().closure_upvar_regions.len()
824                    } else {
825                        // If we're not translating a closure item, fetch the closure adt
826                        // definition and add enough erased lifetimes to match its number of
827                        // arguments.
828                        let adt_decl_id: ItemId =
829                            self.register_item(span, hax_item, TransItemSourceKind::Type);
830                        let adt_decl = self.get_or_translate(adt_decl_id)?;
831                        let adt_generics = adt_decl.generic_params();
832                        adt_generics.regions.len() - generics.regions.len()
833                    };
834                    generics
835                        .regions
836                        .extend((0..upvar_regions).map(|_| self.translate_erased_region()));
837                    if let TransItemSourceKind::TraitImpl(TransImplSource::Callable(..))
838                    | TransItemSourceKind::VTableInstance(TransImplSource::Callable(..))
839                    | TransItemSourceKind::VTableInstanceInitializer(
840                        TransImplSource::Callable(..),
841                    )
842                    | TransItemSourceKind::VTableDropShim(TransImplSource::Callable(..))
843                    | TransItemSourceKind::CallableMethod(..)
844                    | TransItemSourceKind::VTableMethod(TransImplSource::Callable(..))
845                    | TransItemSourceKind::ClosureAsFnCast = kind
846                    {
847                        generics.regions.extend(
848                            args.fn_sig
849                                .bound_vars
850                                .iter()
851                                .map(|_| self.translate_erased_region()),
852                        );
853                    }
854                }
855                _ => {}
856            }
857            if let TransItemSourceKind::CallableMethod(ClosureKind::FnMut | ClosureKind::Fn)
858            | TransItemSourceKind::VTableMethod(TransImplSource::Callable(
859                ClosureKind::FnMut | ClosureKind::Fn,
860            )) = kind
861            {
862                generics.regions.push(self.translate_erased_region());
863            }
864            // If we're in the process of translating this same item (possibly with a
865            // different `TransItemSourceKind`), we can reuse the generics they have in
866            // common.
867            if self.item_src.def_id() == &hax_item.def_id {
868                let depth = self.binding_levels.depth();
869                for (a, b) in generics.regions.iter_mut().zip(
870                    self.outermost_binder()
871                        .params
872                        .identity_args_at_depth(depth)
873                        .regions,
874                ) {
875                    *a = b;
876                }
877            }
878        }
879        if matches!(
880            kind,
881            TransItemSourceKind::DropGlueMethod(..) | TransItemSourceKind::VTableDropShim(..)
882        ) {
883            generics = generics.concat(&self.drop_glue_generic_args());
884        }
885
886        let trait_ref = hax_item
887            .in_trait
888            .as_ref()
889            .map(|trait_proof| self.translate_trait_proof(span, trait_proof))
890            .transpose()?;
891
892        let item = DeclRef {
893            id,
894            generics: Box::new(generics),
895            trait_ref,
896        };
897        Ok(item.try_into().ok().unwrap())
898    }
899
900    /// Register this item and enqueue it for translation.
901    ///
902    /// Note: for `FnPtr`s use `translate_fn_ptr` instead, as this handles late-bound variables
903    /// correctly. For `TypeDeclRef`s use `translate_type_decl_ref` instead, as this correctly
904    /// recognizes built-in ADTs.
905    pub(crate) fn translate_item<T: TryFrom<DeclRef<ItemId>>>(
906        &mut self,
907        span: Span,
908        item: &hax::ItemRef,
909        kind: TransItemSourceKind,
910    ) -> Result<T, Error> {
911        self.translate_item_maybe_enqueue(span, item, kind, true)
912    }
913
914    /// Translate a type def id
915    pub(crate) fn translate_type_decl_ref(
916        &mut self,
917        span: Span,
918        item: &hax::ItemRef,
919    ) -> Result<TypeDeclRef, Error> {
920        self.translate_type_decl_ref_maybe_enqueue(span, item, TransItemSourceKind::Type, true)
921    }
922
923    /// Register a type item and maybe enqueue it for translation. Use this to
924    /// obtain a `TypeDeclRef`, don't construct one manually.
925    pub(crate) fn translate_type_decl_ref_maybe_enqueue(
926        &mut self,
927        span: Span,
928        item: &hax::ItemRef,
929        kind: TransItemSourceKind,
930        enqueue: bool,
931    ) -> Result<TypeDeclRef, Error> {
932        let builtin = match kind {
933            TransItemSourceKind::Type => self.recognize_builtin_adt(item),
934            _ => None,
935        };
936        if builtin == Some(BuiltinAdt::Tuple) && self.t_ctx.options.no_gen_tuple_structs {
937            let mut generics = self.translate_generic_args(span, &item.generic_args, &[])?;
938            // The declaration has no clauses, so we drop the `Sized` proofs of the fields.
939            generics.trait_refs.clear();
940            return Ok(TypeDeclRef {
941                id: TypeDeclId::UNIT,
942                generics: Box::new(generics),
943                builtin,
944            });
945        }
946        let item_ref: DeclRef<ItemId> =
947            self.translate_item_maybe_enqueue(span, item, kind, enqueue)?;
948        assert!(item_ref.trait_ref.is_none());
949        Ok(TypeDeclRef {
950            id: item_ref.id.try_into().unwrap(),
951            generics: item_ref.generics,
952            builtin,
953        })
954    }
955
956    /// Translate a reference to a trait method declaration without registering the declaration as
957    /// a `FunDecl`. `TraitDecl.methods` contains the declaration signature and metadata; only
958    /// default implementations give rise to a real function item.
959    fn translate_method_decl_fn_ptr(
960        &mut self,
961        span: Span,
962        item: &hax::ItemRef,
963    ) -> Result<Option<RegionBinder<FnPtr>>, Error> {
964        let Some(in_trait) = &item.in_trait else {
965            return Ok(None);
966        };
967        let def = self.hax_def(item)?;
968        let hax::FullDefKind::AssocFn {
969            associated_item,
970            sig,
971            ..
972        } = def.kind()
973        else {
974            return Ok(None);
975        };
976        if !matches!(
977            &associated_item.container,
978            hax::AssocItemContainer::TraitContainer { .. }
979        ) {
980            return Ok(None);
981        }
982
983        let trait_ref = self.translate_trait_proof(span, in_trait)?;
984        let generics = self.translate_generic_args(span, &item.generic_args, &item.trait_proofs)?;
985        self.translate_region_binder(span, &sig.as_ref().rebind(()), |ctx, _| {
986            let method_id = ctx.translate_trait_method_id(trait_ref.trait_id(), &item.def_id)?;
987            let fn_kind = FnPtrKind::Trait(trait_ref.move_under_binder(), method_id);
988            let generics = generics.move_under_binder();
989            let generics = generics.concat(&ctx.innermost_binder().params.identity_args());
990            Ok(FnPtr::new(fn_kind, generics))
991        })
992        .map(Some)
993    }
994
995    /// Translate a function reference, assuming that the late-bound regions are in scope. Prefer
996    /// the `translate_bound_fn_ptr*` methods whenever sensible.
997    #[tracing::instrument(skip(self, span))]
998    pub(crate) fn translate_unbound_fn_ptr_maybe_enqueue(
999        &mut self,
1000        span: Span,
1001        item: &hax::ItemRef,
1002        kind: TransItemSourceKind,
1003        enqueue: bool,
1004    ) -> Result<FnPtr, Error> {
1005        let fun_item: DeclRef<ItemId> =
1006            self.translate_item_maybe_enqueue(span, item, kind, enqueue)?;
1007        let fun_item: DeclRef<FunDeclId> = fun_item.try_convert_id().unwrap();
1008        let fun_id = match fun_item.trait_ref {
1009            // Direct function call
1010            None => FnPtrKind::Fun(fun_item.id),
1011            // Trait method
1012            Some(trait_ref) => {
1013                let trait_decl_id = trait_ref.trait_id();
1014                let method_id = self.translate_trait_method_id(trait_decl_id, &item.def_id)?;
1015                FnPtrKind::Trait(trait_ref, method_id)
1016            }
1017        };
1018        let mut generics = fun_item.generics;
1019        // The last n regions are the late-bound ones and were provided as erased regions by
1020        // `translate_item`.
1021        for (a, b) in generics.regions.iter_mut().rev().zip(
1022            self.innermost_binder()
1023                .params
1024                .identity_args()
1025                .regions
1026                .into_iter()
1027                .rev(),
1028        ) {
1029            *a = b;
1030        }
1031        Ok(FnPtr::new(fun_id, generics))
1032    }
1033
1034    #[tracing::instrument(skip(self, span))]
1035    pub(crate) fn translate_bound_fn_ptr_maybe_enqueue(
1036        &mut self,
1037        span: Span,
1038        item: &hax::ItemRef,
1039        kind: TransItemSourceKind,
1040        enqueue: bool,
1041    ) -> Result<RegionBinder<FnPtr>, Error> {
1042        if let Some(fn_ptr) = self.translate_callable_method_fn_ptr(span, item)? {
1043            return Ok(fn_ptr);
1044        }
1045        if let Some(fn_ptr) = self.translate_method_decl_fn_ptr(span, item)? {
1046            return Ok(fn_ptr);
1047        }
1048
1049        let late_bound = self.hax_def(item)?.late_bound();
1050        self.translate_region_binder(span, &late_bound, |ctx, _| {
1051            ctx.translate_unbound_fn_ptr_maybe_enqueue(span, item, kind, enqueue)
1052        })
1053    }
1054
1055    /// Translate a reference to a function or trait method.
1056    #[tracing::instrument(skip(self, span))]
1057    pub(crate) fn translate_bound_fn_ptr(
1058        &mut self,
1059        span: Span,
1060        item: &hax::ItemRef,
1061        kind: TransItemSourceKind,
1062    ) -> Result<RegionBinder<FnPtr>, Error> {
1063        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, true)
1064    }
1065
1066    pub(crate) fn translate_bound_fn_ptr_no_enqueue(
1067        &mut self,
1068        span: Span,
1069        item: &hax::ItemRef,
1070        kind: TransItemSourceKind,
1071    ) -> Result<RegionBinder<FnPtr>, Error> {
1072        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, false)
1073    }
1074
1075    /// Translate a reference to a function or trait method, erasing or inferring its late-bound
1076    /// lifetimes.
1077    pub(crate) fn translate_fn_ptr(
1078        &mut self,
1079        span: Span,
1080        item: &hax::ItemRef,
1081        kind: TransItemSourceKind,
1082    ) -> Result<FnPtr, Error> {
1083        let fn_ptr = self.translate_bound_fn_ptr(span, item, kind)?;
1084        let fn_ptr = self.erase_region_binder(fn_ptr);
1085        Ok(fn_ptr)
1086    }
1087
1088    pub(crate) fn translate_global_decl_ref(
1089        &mut self,
1090        span: Span,
1091        item: &hax::ItemRef,
1092    ) -> Result<GlobalDeclRef, Error> {
1093        self.translate_item(span, item, TransItemSourceKind::Global)
1094    }
1095
1096    pub(crate) fn translate_trait_decl_ref(
1097        &mut self,
1098        span: Span,
1099        item: &hax::ItemRef,
1100    ) -> Result<TraitDeclRef, Error> {
1101        self.translate_item(span, item, TransItemSourceKind::TraitDecl)
1102    }
1103
1104    pub(crate) fn translate_trait_impl_ref(
1105        &mut self,
1106        span: Span,
1107        item: &hax::ItemRef,
1108        kind: TransImplSource,
1109    ) -> Result<TraitImplRef, Error> {
1110        self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
1111    }
1112}
1113
1114#[tracing::instrument(skip(tcx, error_ctx))]
1115pub fn translate<'tcx>(
1116    tcx: TyCtxt<'tcx>,
1117    cli_options: &CliOpts,
1118    mut error_ctx: ErrorCtx,
1119    sysroot: PathBuf,
1120) -> Result<TransformCtx, Error> {
1121    let translate_options = TranslateOptions::new(&mut error_ctx, cli_options);
1122
1123    let traits_to_remove: HashSet<rustc_hir::def_id::DefId> = {
1124        let hax_state = hax::state::State::new(
1125            tcx,
1126            hax::options::Options::default(),
1127            hax::options::BoundsOptions::default(),
1128        );
1129        translate_options
1130            .hide_traits
1131            .iter()
1132            .flat_map(|pat| super::resolve_path::def_path_def_ids(&hax_state, pat, true).unwrap())
1133            .collect()
1134    };
1135    let hax_state = hax::state::State::new(
1136        tcx,
1137        hax::options::Options {
1138            inline_anon_consts: !translate_options.raw_consts,
1139        },
1140        hax::options::BoundsOptions {
1141            add_destruct_bounds: translate_options.add_destruct_bounds,
1142            remove_traits: traits_to_remove,
1143        },
1144    );
1145
1146    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
1147        .to_def_id()
1148        .sinto(&hax_state);
1149    let crate_name = crate_def_id.crate_name(&hax_state).to_string();
1150    trace!("# Crate: {}", crate_name);
1151
1152    let mut ctx = TranslateCtx {
1153        tcx,
1154        sysroot,
1155        hax_state,
1156        options: translate_options,
1157        errors: RefCell::new(error_ctx),
1158        translated: TranslatedCrate {
1159            crate_name,
1160            options: cli_options.clone(),
1161            ..TranslatedCrate::default()
1162        },
1163        method_status: Default::default(),
1164        assoc_item_id_map: Default::default(),
1165        id_map: Default::default(),
1166        reverse_id_map: Default::default(),
1167        file_to_id: Default::default(),
1168        items_to_translate: Default::default(),
1169        processed: Default::default(),
1170        translate_stack: Default::default(),
1171        cached_spans: Default::default(),
1172        cached_names: Default::default(),
1173        cached_item_metas: Default::default(),
1174        lt_mutability_computer: Default::default(),
1175    };
1176    ctx.register_target_info();
1177    ctx.reserve_unit_decl();
1178    ctx.register_builtin_functions()?;
1179
1180    // Start translating from the selected items.
1181    for start_from in ctx.options.start_from.clone() {
1182        match start_from {
1183            StartFrom::Pattern { pattern, strict } => {
1184                if let Ok(def_ids) = ctx.resolve_path(Span::dummy(), &pattern, strict) {
1185                    for def_id in def_ids {
1186                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
1187                        ctx.enqueue_module_item(&def_id);
1188                    }
1189                }
1190            }
1191            StartFrom::Attribute(attr_name) => {
1192                let attr_path = attr_name
1193                    .split("::")
1194                    .map(rustc_span::Symbol::intern)
1195                    .collect_vec();
1196                let mut add_if_attr_matches = |ldid: rustc_hir::def_id::LocalDefId| {
1197                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
1198                    if !matches!(def_id.kind, hax::DefKind::Mod)
1199                        && def_id.attrs(tcx).iter().any(|a| a.path_matches(&attr_path))
1200                    {
1201                        ctx.enqueue_module_item(&def_id);
1202                    }
1203                };
1204                for ldid in tcx.hir_crate_items(()).definitions() {
1205                    add_if_attr_matches(ldid)
1206                }
1207            }
1208            StartFrom::Pub => {
1209                let mut add_if_matches = |ldid: rustc_hir::def_id::LocalDefId| {
1210                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
1211                    if !matches!(def_id.kind, hax::DefKind::Mod)
1212                        && def_id.visibility(tcx) == Some(true)
1213                    {
1214                        ctx.enqueue_module_item(&def_id);
1215                    }
1216                };
1217                for ldid in tcx.hir_crate_items(()).definitions() {
1218                    add_if_matches(ldid)
1219                }
1220            }
1221        }
1222    }
1223
1224    if ctx.errors.borrow().has_errors() {
1225        // Don't continue translating if there were errors while parsing options.
1226        return Err(Error::dummy());
1227    }
1228
1229    trace!(
1230        "Queue after we explored the crate:\n{:?}",
1231        &ctx.items_to_translate
1232    );
1233
1234    // Translate.
1235    //
1236    // For as long as the queue of items to translate is not empty, we pop the top item and
1237    // translate it. If an item refers to non-translated (potentially external) items, we add them
1238    // to the queue.
1239    //
1240    // Note that the order in which we translate the definitions doesn't matter:
1241    // we never need to lookup a translated definition, and only use the map
1242    // from Rust ids to translated ids.
1243    while let Some(item_src) = ctx.items_to_translate.pop_front() {
1244        if ctx.processed.insert(item_src.clone()) {
1245            ctx.translate_item(&item_src);
1246        }
1247    }
1248
1249    // Remove methods not marked as "used". They are never called and we made sure not to translate
1250    // them. This removes them from the traits and impls.
1251    ctx.remove_unused_methods();
1252
1253    // Return the context, dropping the hax state and rustc `tcx`.
1254    Ok(TransformCtx {
1255        options: ctx.options,
1256        translated: ctx.translated,
1257        errors: ctx.errors,
1258    })
1259}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
