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(TraitImplSource),
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 appropriate `TraitImplSource::Closure` impl.
69    ClosureMethod(ClosureKind),
70    /// A cast of a state-less closure as 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(TraitImplSource),
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(TraitImplSource),
80    /// The initializer function of the `VTableInstance`.
81    VTableInstanceInitializer(TraitImplSource),
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 TraitImplSource {
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. The `DefId` is that of the closure.
98    Closure(ClosureKind),
99    /// A fictitious `impl Destruct for T` that contains the drop glue code for the given ADT. The
100    /// `DefId` is that of the ADT.
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            Self::monomorphic(item, kind)
126        } else {
127            Self::polymorphic(&item.def_id, kind)
128        }
129    }
130
131    /// Refers to the polymorphic version of this item.
132    pub fn polymorphic(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
133        Self::new(RustcItem::Poly(def_id.clone()), kind)
134    }
135
136    /// Refers to the monomorphic version of this item.
137    pub fn monomorphic(item: &hax::ItemRef, kind: TransItemSourceKind) -> Self {
138        Self::new(RustcItem::Mono(item.clone()), kind)
139    }
140
141    /// Refers to the monomorphic trait (or vtable).
142    /// See the docs of `RustcItem::MonoTrait` for details.
143    pub fn monomorphic_trait(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
144        Self::new(RustcItem::MonoTrait(def_id.clone()), kind)
145    }
146
147    pub fn def_id(&self) -> &hax::DefId {
148        self.item.def_id()
149    }
150
151    /// Keep the same def_id but change the kind.
152    pub(crate) fn with_kind(&self, kind: TransItemSourceKind) -> Self {
153        let mut ret = self.clone();
154        ret.kind = kind;
155        ret
156    }
157
158    /// For virtual items that have a parent (typically a method impl), return this parent. Does
159    /// not attempt to generally compute the parent of an item. Used to compute names.
160    pub(crate) fn parent(&self) -> Option<Self> {
161        let parent_kind = match self.kind {
162            TransItemSourceKind::ClosureMethod(kind) => {
163                TransItemSourceKind::TraitImpl(TraitImplSource::Closure(kind))
164            }
165            TransItemSourceKind::DropGlueMethod(impl_kind)
166            | TransItemSourceKind::VTableInstance(impl_kind)
167            | TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
168                TransItemSourceKind::TraitImpl(impl_kind)
169            }
170            _ => return None,
171        };
172        Some(self.with_kind(parent_kind))
173    }
174
175    /// Whether this item is the "main" item for this def_id or not (e.g. Destruct impl/methods are not
176    /// the main item).
177    pub(crate) fn is_derived_item(&self) -> bool {
178        use TransItemSourceKind::*;
179        !matches!(
180            self.kind,
181            Global
182                | TraitDecl
183                | TraitImpl(TraitImplSource::Normal)
184                | InherentImpl
185                | Module
186                | Fun
187                | Type
188        )
189    }
190}
191
192impl RustcItem {
193    pub fn def_id(&self) -> &hax::DefId {
194        match self {
195            RustcItem::Poly(def_id) => def_id,
196            RustcItem::Mono(item_ref) => &item_ref.def_id,
197            RustcItem::MonoTrait(def_id) => def_id,
198        }
199    }
200}
201
202impl<'tcx> TranslateCtx<'tcx> {
203    /// If this is a method declaration without a default, return the `DefId` of its parent trait.
204    fn is_method_decl_without_default(&mut self, def_id: &hax::DefId) -> Option<hax::DefId> {
205        if matches!(def_id.kind, hax::DefKind::AssocFn)
206            && let def = self.poly_hax_def(def_id).ok()?
207            && let hax::FullDefKind::AssocFn {
208                associated_item, ..
209            } = def.kind()
210            && !associated_item.has_value
211            && let hax::AssocItemContainer::TraitContainer { trait_ref } =
212                &associated_item.container
213        {
214            Some(trait_ref.def_id.clone())
215        } else {
216            None
217        }
218    }
219
220    /// Resolve a path to a list of matching `DefId`s.
221    pub fn resolve_path(
222        &self,
223        span: Span,
224        pat: &NamePattern,
225        strict: bool,
226    ) -> Result<Vec<rustc_span::def_id::DefId>, Error> {
227        super::resolve_path::def_path_def_ids(&self.hax_state, pat, strict).map_err(|err| {
228            register_error!(self, span, "failed to resolve item path `{pat}`: {err}")
229        })
230    }
231
232    /// Returns the default translation kind for the given `DefId`. Returns `None` for items that
233    /// we don't translate. Errors on unexpected items.
234    pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
235        use crate::hax::DefKind::*;
236        Some(match &def_id.kind {
237            Enum | Struct | Union | TyAlias | ForeignTy => TransItemSourceKind::Type,
238            Fn | AssocFn => TransItemSourceKind::Fun,
239            Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
240            Trait | TraitAlias => TransItemSourceKind::TraitDecl,
241            Impl { of_trait: true } => TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
242            Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
243            Mod | ForeignMod => TransItemSourceKind::Module,
244
245            // We skip these
246            ExternCrate | GlobalAsm | Macro { .. } | Use => return None,
247            // These can happen when doing `--start-from` on a foreign crate. We can skip them
248            // because their parents will already have been registered.
249            Ctor { .. } | Variant => return None,
250            // We cannot encounter these since they're not top-level items.
251            AnonConst
252            | AssocTy
253            | Closure
254            | ConstParam
255            | Field
256            | InlineConst
257            | PromotedConst
258            | LifetimeParam
259            | OpaqueTy
260            | SyntheticCoroutineBody
261            | TyParam => {
262                let span = self.def_span(def_id);
263                register_error!(
264                    self,
265                    span,
266                    "Cannot register item `{def_id:?}` with kind `{:?}`",
267                    def_id.kind
268                );
269                return None;
270            }
271        })
272    }
273
274    /// Add this item to the queue of items to translate. Each translated item will then
275    /// recursively register the items it refers to. We call this on the crate root and end up
276    /// exploring the whole crate.
277    #[tracing::instrument(skip(self))]
278    pub fn enqueue_module_item(&mut self, def_id: &hax::DefId) {
279        if let Some(trait_def_id) = self.is_method_decl_without_default(def_id) {
280            // Don't translate the method itself as it doesn't correspond to an item, translate the
281            // trait instead.
282            self.enqueue_module_item(&trait_def_id);
283            return;
284        }
285        let Some(kind) = self.base_kind_for_item(def_id) else {
286            return;
287        };
288        let item_src = if self.options.monomorphize_with_hax {
289            if let Ok(def) = self.poly_hax_def(def_id)
290                && !def.has_any_generics()
291            {
292                // Monomorphize this item and the items it depends on.
293                TransItemSource::monomorphic(def.this(), kind)
294            } else {
295                // Skip polymorphic items and items that cause errors.
296                return;
297            }
298        } else {
299            TransItemSource::polymorphic(def_id, kind)
300        };
301        let _: Option<ItemId> = self.register_and_enqueue(&None, item_src);
302    }
303
304    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
305        &mut self,
306        dep_src: &Option<DepSource>,
307        src: &TransItemSource,
308    ) -> Option<T> {
309        let item_id = match self.id_map.get(src) {
310            Some(tid) => *tid,
311            None => {
312                use TransItemSourceKind::*;
313                let trans_id = match src.kind {
314                    Type | VTable => ItemId::Type(self.translated.type_decls.reserve_slot()),
315                    TraitDecl => ItemId::TraitDecl(self.translated.trait_decls.reserve_slot()),
316                    TraitImpl(..) => ItemId::TraitImpl(self.translated.trait_impls.reserve_slot()),
317                    Global | VTableInstance(..) => {
318                        ItemId::Global(self.translated.global_decls.reserve_slot())
319                    }
320                    Fun
321                    | ClosureMethod(..)
322                    | ClosureAsFnCast
323                    | DropGlueMethod(..)
324                    | VTableInstanceInitializer(..)
325                    | VTableMethod
326                    | VTableDropShim => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
327                    InherentImpl | Module => return None,
328                };
329                // Add the id to the queue of declarations to translate
330                self.id_map.insert(src.clone(), trans_id);
331                self.reverse_id_map.insert(trans_id, src.clone());
332                // Store the name early so the name matcher can identify paths.
333                if let Ok(name) = self.translate_name(src) {
334                    self.translated.item_names.insert(trans_id, name);
335                }
336                trans_id
337            }
338        };
339        self.errors
340            .borrow_mut()
341            .register_dep_source(dep_src, item_id, src.def_id().is_local());
342        item_id.try_into().ok()
343    }
344
345    /// Register this item source and enqueue it for translation.
346    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
347        &mut self,
348        dep_src: &Option<DepSource>,
349        item_src: TransItemSource,
350    ) -> Option<T> {
351        let id = self.register_no_enqueue(dep_src, &item_src);
352        self.items_to_translate.push_back(item_src);
353        id
354    }
355
356    /// Enqueue an item from its id.
357    pub(crate) fn enqueue_id(&mut self, id: impl Into<ItemId>) {
358        let id = id.into();
359        if self.translated.get_item(id).is_none() {
360            let item_src = self.reverse_id_map[&id].clone();
361            self.items_to_translate.push_back(item_src);
362        }
363    }
364
365    /// Register the associated types of this trait.
366    pub fn register_assoc_items(
367        &mut self,
368        trait_def_id: &hax::DefId,
369        trait_id: TraitDeclId,
370    ) -> Result<(), Error> {
371        if self.method_status.get(trait_id).is_some() {
372            return Ok(());
373        }
374        let trait_def = self.poly_hax_def(trait_def_id)?;
375        let hax::FullDefKind::Trait { items, .. } = trait_def.kind() else {
376            unreachable!()
377        };
378        let names = self
379            .translated
380            .assoc_item_names
381            .get_or_insert_with(trait_id, Default::default);
382        for item in items {
383            let name = TraitItemName(
384                item.name
385                    .as_ref()
386                    .map(|n| n.to_string().into())
387                    .unwrap_or_default(),
388            );
389            let id: AssocItemId = match item.kind {
390                hax::AssocKind::Type { .. } => names.types.push(name).into(),
391                hax::AssocKind::Fn { .. } => names.methods.push(name).into(),
392                hax::AssocKind::Const { .. } => names.consts.push(name).into(),
393            };
394            self.assoc_item_id_map.insert(item.def_id.clone(), id);
395        }
396        // Add a virtual method to the `Destruct` trait.
397        if trait_def.lang_item == Some(sym::destruct) {
398            let method_name = TraitItemName("drop_glue".into());
399            names.methods.push(method_name);
400        }
401        self.method_status.get_or_insert_with(trait_id, || {
402            names.methods.map_ref(|_| MethodStatus::default())
403        });
404        Ok(())
405    }
406
407    /// Get the unique per-trait id corresponding to this associated item. The `DefId` can be of an
408    /// item declaration or item implementation.
409    pub fn translate_assoc_item_id(
410        &mut self,
411        trait_id: TraitDeclId,
412        item_def_id: &hax::DefId,
413    ) -> Result<AssocItemId, Error> {
414        // The same assoc item `DefId` could belong to several `TraitDeclId`s because of
415        // monomorphization, so we only return the item id if we know this trait's data is
416        // initialized.
417        if let Some(&item_id) = self.assoc_item_id_map.get(item_def_id)
418            && self.method_status.get(trait_id).is_some()
419        {
420            return Ok(item_id);
421        }
422
423        let item_def = self.poly_hax_def(item_def_id)?;
424        let assoc = match item_def.kind() {
425            hax::FullDefKind::AssocTy {
426                associated_item, ..
427            }
428            | hax::FullDefKind::AssocConst {
429                associated_item, ..
430            }
431            | hax::FullDefKind::AssocFn {
432                associated_item, ..
433            } => associated_item,
434            _ => panic!("Unexpected def for associated item: {item_def:?}"),
435        };
436        let decl_def_id = assoc.implemented_trait_item_id();
437
438        if decl_def_id != item_def_id
439            && let Some(&item_id) = self.assoc_item_id_map.get(decl_def_id)
440            && self.method_status.get(trait_id).is_some()
441        {
442            self.assoc_item_id_map.insert(item_def_id.clone(), item_id);
443            return Ok(item_id);
444        }
445
446        let trait_def_id = decl_def_id.parent(&self.hax_state).unwrap();
447        self.register_assoc_items(&trait_def_id, trait_id)?;
448        let item_id = *self.assoc_item_id_map.get(decl_def_id).unwrap();
449        Ok(item_id)
450    }
451
452    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
453    /// This does not make the method be considered "used"; use `mark_method_as_used` for that.
454    pub fn translate_trait_method_id_no_enqueue(
455        &mut self,
456        trait_id: TraitDeclId,
457        def_id: &hax::DefId,
458    ) -> Result<TraitMethodId, Error> {
459        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
460        Ok(*item_id.as_method().unwrap())
461    }
462    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
463    /// This makes the method be considered "used".
464    pub fn translate_trait_method_id(
465        &mut self,
466        trait_id: TraitDeclId,
467        def_id: &hax::DefId,
468    ) -> Result<TraitMethodId, Error> {
469        let method_id = self.translate_trait_method_id_no_enqueue(trait_id, def_id)?;
470        self.mark_method_as_used(trait_id, method_id);
471        Ok(method_id)
472    }
473    /// Register a trait associated type and return its `AssocTypeId`. This id is unique per trait.
474    pub fn translate_assoc_type_id(
475        &mut self,
476        trait_id: TraitDeclId,
477        def_id: &hax::DefId,
478    ) -> Result<AssocTypeId, Error> {
479        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
480        Ok(*item_id.as_type().unwrap())
481    }
482    /// Register a trait associated const and return its `AssocTypeId`. This id is unique per trait.
483    pub fn translate_assoc_const_id(
484        &mut self,
485        trait_id: TraitDeclId,
486        def_id: &hax::DefId,
487    ) -> Result<AssocConstId, Error> {
488        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
489        Ok(*item_id.as_const().unwrap())
490    }
491
492    pub(crate) fn register_target_info(&mut self) {
493        let target_data = &self.tcx.data_layout;
494        let triple = self.get_target_triple();
495
496        let mut primitive_alignments = SeqHashMap::new();
497        primitive_alignments.insert(LiteralTy::Bool, target_data.i8_align.bytes());
498        primitive_alignments.insert(LiteralTy::Int(IntTy::I8), target_data.i8_align.bytes());
499        primitive_alignments.insert(LiteralTy::Int(IntTy::I16), target_data.i16_align.bytes());
500        primitive_alignments.insert(LiteralTy::Int(IntTy::I32), target_data.i32_align.bytes());
501        primitive_alignments.insert(LiteralTy::Int(IntTy::I64), target_data.i64_align.bytes());
502        primitive_alignments.insert(LiteralTy::Int(IntTy::I128), target_data.i128_align.bytes());
503        primitive_alignments.insert(
504            LiteralTy::Int(IntTy::Isize),
505            target_data.pointer_align().bytes(),
506        );
507        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U8), target_data.i8_align.bytes());
508        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U16), target_data.i16_align.bytes());
509        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U32), target_data.i32_align.bytes());
510        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U64), target_data.i64_align.bytes());
511        primitive_alignments.insert(
512            LiteralTy::UInt(UIntTy::U128),
513            target_data.i128_align.bytes(),
514        );
515        primitive_alignments.insert(
516            LiteralTy::UInt(UIntTy::Usize),
517            target_data.pointer_align().bytes(),
518        );
519        primitive_alignments.insert(
520            LiteralTy::Float(FloatTy::F16),
521            target_data.f16_align.bytes(),
522        );
523        primitive_alignments.insert(
524            LiteralTy::Float(FloatTy::F32),
525            target_data.f32_align.bytes(),
526        );
527        primitive_alignments.insert(
528            LiteralTy::Float(FloatTy::F64),
529            target_data.f64_align.bytes(),
530        );
531        primitive_alignments.insert(
532            LiteralTy::Float(FloatTy::F128),
533            target_data.f128_align.bytes(),
534        );
535        // INFO: This is not explicitly guaranteed by the reference, but by the implementation of rustc.
536        // https://doc.rust-lang.org/1.97.1/nightly-rustc/src/rustc_ty_utils/layout.rs.html#391
537        primitive_alignments.insert(LiteralTy::Char, target_data.i32_align.bytes());
538
539        let info = krate::TargetInfo {
540            target_pointer_size: target_data.pointer_size().bytes(),
541            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
542            c_enum_min_size: target_data.c_enum_min_size.size().bytes(),
543            primitive_alignments,
544        };
545        self.translated.target_information.insert(triple, info);
546    }
547}
548
549// Id and item reference registration.
550impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
551    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
552        Some(DepSource {
553            src_id: self.item_id?,
554            span: self.item_src.def_id().is_local().then_some(span),
555        })
556    }
557
558    /// Register this item source and enqueue it for translation.
559    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
560        &mut self,
561        span: Span,
562        item_src: TransItemSource,
563    ) -> T {
564        let dep_src = self.make_dep_source(span);
565        self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
566    }
567
568    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
569        &mut self,
570        span: Span,
571        src: &TransItemSource,
572    ) -> T {
573        let dep_src = self.make_dep_source(span);
574        self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
575    }
576
577    /// Register this item and maybe enqueue it for translation.
578    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
579        &mut self,
580        span: Span,
581        enqueue: bool,
582        item: &hax::ItemRef,
583        kind: TransItemSourceKind,
584    ) -> T {
585        let item = if self.monomorphize() && item.has_param {
586            item.erase(self.hax_state_with_id())
587        } else {
588            item.clone()
589        };
590        // In mono mode:
591        //   1. If the item being registered is a `trait decl`, we construct a
592        //      `monomorphic_trait` item source.
593        //   2. Otherwise, if the current `item_trans_ctx` is under a `trait decl`
594        //      or a `vtable`, we construct a `poly` item.
595        //   3. In all other cases, we construct a `mono` item.
596        let item_src = if self.monomorphize() && matches!(kind, TransItemSourceKind::TraitDecl) {
597            TransItemSource::monomorphic_trait(&item.def_id, kind)
598        } else {
599            TransItemSource::from_item(
600                &item,
601                kind,
602                self.monomorphize()
603                    && !matches!(
604                        self.item_src.kind,
605                        TransItemSourceKind::TraitDecl | TransItemSourceKind::VTable
606                    ),
607            )
608        };
609        if enqueue {
610            self.register_and_enqueue(span, item_src)
611        } else {
612            self.register_no_enqueue(span, &item_src)
613        }
614    }
615
616    /// Register this item and enqueue it for translation.
617    pub(crate) fn register_item<T: TryFrom<ItemId>>(
618        &mut self,
619        span: Span,
620        item: &hax::ItemRef,
621        kind: TransItemSourceKind,
622    ) -> T {
623        self.register_item_maybe_enqueue(span, true, item, kind)
624    }
625
626    /// Register this item without enqueueing it for translation.
627    #[expect(dead_code)]
628    pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
629        &mut self,
630        span: Span,
631        item: &hax::ItemRef,
632        kind: TransItemSourceKind,
633    ) -> T {
634        self.register_item_maybe_enqueue(span, false, item, kind)
635    }
636
637    /// Register this item and maybe enqueue it for translation.
638    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<DeclRef<ItemId>>>(
639        &mut self,
640        span: Span,
641        hax_item: &hax::ItemRef,
642        kind: TransItemSourceKind,
643        enqueue: bool,
644    ) -> Result<T, Error> {
645        let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, hax_item, kind);
646        // In mono mode, we keep trait decls generic.
647        let mut generics = if self.monomorphize() && !matches!(kind, TransItemSourceKind::TraitDecl)
648        {
649            GenericArgs::empty()
650        } else {
651            self.translate_generic_args(span, &hax_item.generic_args, &hax_item.trait_proofs)?
652        };
653
654        // Add regions to make sure the item args match the params we set up in
655        // `translate_item_generics`.
656        if matches!(
657            hax_item.def_id.kind,
658            hax::DefKind::Fn | hax::DefKind::AssocFn | hax::DefKind::Closure
659        ) {
660            let def = self.hax_def(hax_item)?;
661            match def.kind() {
662                hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
663                    generics.regions.extend(
664                        sig.bound_vars
665                            .iter()
666                            .map(|_| self.translate_erased_region()),
667                    );
668                }
669                hax::FullDefKind::Closure { args, .. } => {
670                    let upvar_regions = if self.item_src.def_id() == &args.item.def_id {
671                        assert!(self.outermost_binder().closure_upvar_tys.is_some());
672                        self.outermost_binder().closure_upvar_regions.len()
673                    } else {
674                        // If we're not translating a closure item, fetch the closure adt
675                        // definition and add enough erased lifetimes to match its number of
676                        // arguments.
677                        let adt_decl_id: ItemId =
678                            self.register_item(span, hax_item, TransItemSourceKind::Type);
679                        let adt_decl = self.get_or_translate(adt_decl_id)?;
680                        let adt_generics = adt_decl.generic_params();
681                        adt_generics.regions.len() - generics.regions.len()
682                    };
683                    generics
684                        .regions
685                        .extend((0..upvar_regions).map(|_| self.translate_erased_region()));
686                    if let TransItemSourceKind::TraitImpl(TraitImplSource::Closure(..))
687                    | TransItemSourceKind::ClosureMethod(..)
688                    | TransItemSourceKind::ClosureAsFnCast = kind
689                    {
690                        generics.regions.extend(
691                            args.fn_sig
692                                .bound_vars
693                                .iter()
694                                .map(|_| self.translate_erased_region()),
695                        );
696                    }
697                    if let TransItemSourceKind::ClosureMethod(
698                        ClosureKind::FnMut | ClosureKind::Fn,
699                    ) = kind
700                    {
701                        generics.regions.push(self.translate_erased_region());
702                    }
703                    // If we're in the process of translating this same closure item (possibly with
704                    // a different `TransItemSourceKind`), we can reuse the generics they have in
705                    // common.
706                    if self.item_src.def_id() == &args.item.def_id {
707                        let depth = self.binding_levels.depth();
708                        for (a, b) in generics.regions.iter_mut().zip(
709                            self.outermost_binder()
710                                .params
711                                .identity_args_at_depth(depth)
712                                .regions,
713                        ) {
714                            *a = b;
715                        }
716                    }
717                }
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    /// Auxiliary function to translate function calls and references to functions.
835    /// Translate a function id applied with some substitutions.
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: TraitImplSource,
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
