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

charon_driver/translate/
translate_crate.rs
