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

charon_driver/translate/
translate_crate.rs
