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

charon_driver/translate/
translate_crate.rs
