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

charon_driver/translate/
translate_crate.rs
