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

charon_driver/translate/
translate_crate.rs
