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_extend_and_insert(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_extend_and_insert(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        let info = krate::TargetInfo {
496            target_pointer_size: target_data.pointer_size().bytes(),
497            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
498        };
499        self.translated.target_information.insert(triple, info);
500    }
501}
502
503// Id and item reference registration.
504impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
505    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
506        Some(DepSource {
507            src_id: self.item_id?,
508            span: self.item_src.def_id().is_local().then_some(span),
509        })
510    }
511
512    /// Register this item source and enqueue it for translation.
513    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
514        &mut self,
515        span: Span,
516        item_src: TransItemSource,
517    ) -> T {
518        let dep_src = self.make_dep_source(span);
519        self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
520    }
521
522    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
523        &mut self,
524        span: Span,
525        src: &TransItemSource,
526    ) -> T {
527        let dep_src = self.make_dep_source(span);
528        self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
529    }
530
531    /// Register this item and maybe enqueue it for translation.
532    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
533        &mut self,
534        span: Span,
535        enqueue: bool,
536        item: &hax::ItemRef,
537        kind: TransItemSourceKind,
538    ) -> T {
539        let item = if self.monomorphize() && item.has_param {
540            item.erase(self.hax_state_with_id())
541        } else {
542            item.clone()
543        };
544        // In mono mode:
545        //   1. If the item being registered is a `trait decl`, we construct a
546        //      `monomorphic_trait` item source.
547        //   2. Otherwise, if the current `item_trans_ctx` is under a `trait decl`
548        //      or a `vtable`, we construct a `poly` item.
549        //   3. In all other cases, we construct a `mono` item.
550        let item_src = if self.monomorphize() && matches!(kind, TransItemSourceKind::TraitDecl) {
551            TransItemSource::monomorphic_trait(&item.def_id, kind)
552        } else {
553            TransItemSource::from_item(
554                &item,
555                kind,
556                self.monomorphize()
557                    && !matches!(
558                        self.item_src.kind,
559                        TransItemSourceKind::TraitDecl | TransItemSourceKind::VTable
560                    ),
561            )
562        };
563        if enqueue {
564            self.register_and_enqueue(span, item_src)
565        } else {
566            self.register_no_enqueue(span, &item_src)
567        }
568    }
569
570    /// Register this item and enqueue it for translation.
571    pub(crate) fn register_item<T: TryFrom<ItemId>>(
572        &mut self,
573        span: Span,
574        item: &hax::ItemRef,
575        kind: TransItemSourceKind,
576    ) -> T {
577        self.register_item_maybe_enqueue(span, true, item, kind)
578    }
579
580    /// Register this item without enqueueing it for translation.
581    #[expect(dead_code)]
582    pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
583        &mut self,
584        span: Span,
585        item: &hax::ItemRef,
586        kind: TransItemSourceKind,
587    ) -> T {
588        self.register_item_maybe_enqueue(span, false, item, kind)
589    }
590
591    /// Register this item and maybe enqueue it for translation.
592    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<DeclRef<ItemId>>>(
593        &mut self,
594        span: Span,
595        hax_item: &hax::ItemRef,
596        kind: TransItemSourceKind,
597        enqueue: bool,
598    ) -> Result<T, Error> {
599        let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, hax_item, kind);
600        // In mono mode, we keep trait decls generic.
601        let mut generics = if self.monomorphize() && !matches!(kind, TransItemSourceKind::TraitDecl)
602        {
603            GenericArgs::empty()
604        } else {
605            self.translate_generic_args(span, &hax_item.generic_args, &hax_item.trait_proofs)?
606        };
607
608        // Add regions to make sure the item args match the params we set up in
609        // `translate_item_generics`.
610        if matches!(
611            hax_item.def_id.kind,
612            hax::DefKind::Fn | hax::DefKind::AssocFn | hax::DefKind::Closure
613        ) {
614            let def = self.hax_def(hax_item)?;
615            match def.kind() {
616                hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
617                    generics.regions.extend(
618                        sig.bound_vars
619                            .iter()
620                            .map(|_| self.translate_erased_region()),
621                    );
622                }
623                hax::FullDefKind::Closure { args, .. } => {
624                    let upvar_regions = if self.item_src.def_id() == &args.item.def_id {
625                        assert!(self.outermost_binder().closure_upvar_tys.is_some());
626                        self.outermost_binder().closure_upvar_regions.len()
627                    } else {
628                        // If we're not translating a closure item, fetch the closure adt
629                        // definition and add enough erased lifetimes to match its number of
630                        // arguments.
631                        let adt_decl_id: ItemId =
632                            self.register_item(span, hax_item, TransItemSourceKind::Type);
633                        let adt_decl = self.get_or_translate(adt_decl_id)?;
634                        let adt_generics = adt_decl.generic_params();
635                        adt_generics.regions.len() - generics.regions.len()
636                    };
637                    generics
638                        .regions
639                        .extend((0..upvar_regions).map(|_| self.translate_erased_region()));
640                    if let TransItemSourceKind::TraitImpl(TraitImplSource::Closure(..))
641                    | TransItemSourceKind::ClosureMethod(..)
642                    | TransItemSourceKind::ClosureAsFnCast = kind
643                    {
644                        generics.regions.extend(
645                            args.fn_sig
646                                .bound_vars
647                                .iter()
648                                .map(|_| self.translate_erased_region()),
649                        );
650                    }
651                    if let TransItemSourceKind::ClosureMethod(
652                        ClosureKind::FnMut | ClosureKind::Fn,
653                    ) = kind
654                    {
655                        generics.regions.push(self.translate_erased_region());
656                    }
657                    // If we're in the process of translating this same closure item (possibly with
658                    // a different `TransItemSourceKind`), we can reuse the generics they have in
659                    // common.
660                    if self.item_src.def_id() == &args.item.def_id {
661                        let depth = self.binding_levels.depth();
662                        for (a, b) in generics.regions.iter_mut().zip(
663                            self.outermost_binder()
664                                .params
665                                .identity_args_at_depth(depth)
666                                .regions,
667                        ) {
668                            *a = b;
669                        }
670                    }
671                }
672                _ => {}
673            }
674        }
675        if matches!(
676            kind,
677            TransItemSourceKind::DropGlueMethod(..) | TransItemSourceKind::VTableDropShim
678        ) {
679            generics = generics.concat(&self.drop_glue_generic_args());
680        }
681
682        let trait_ref = hax_item
683            .in_trait
684            .as_ref()
685            .map(|trait_proof| self.translate_trait_proof(span, trait_proof))
686            .transpose()?;
687        let item = DeclRef {
688            id,
689            generics: Box::new(generics),
690            trait_ref,
691        };
692        Ok(item.try_into().ok().unwrap())
693    }
694
695    /// Register this item and enqueue it for translation.
696    ///
697    /// Note: for `FnPtr`s use `translate_fn_ptr` instead, as this handles late-bound variables
698    /// correctly. For `TypeDeclRef`s use `translate_type_decl_ref` instead, as this correctly
699    /// recognizes built-in types.
700    pub(crate) fn translate_item<T: TryFrom<DeclRef<ItemId>>>(
701        &mut self,
702        span: Span,
703        item: &hax::ItemRef,
704        kind: TransItemSourceKind,
705    ) -> Result<T, Error> {
706        self.translate_item_maybe_enqueue(span, item, kind, true)
707    }
708
709    /// Translate a type def id
710    pub(crate) fn translate_type_decl_ref(
711        &mut self,
712        span: Span,
713        item: &hax::ItemRef,
714    ) -> Result<TypeDeclRef, Error> {
715        match self.recognize_builtin_type(item)? {
716            Some(id) => {
717                let generics =
718                    self.translate_generic_args(span, &item.generic_args, &item.trait_proofs)?;
719                Ok(TypeDeclRef {
720                    id: TypeId::Builtin(id),
721                    generics: Box::new(generics),
722                })
723            }
724            None => self.translate_item(span, item, TransItemSourceKind::Type),
725        }
726    }
727
728    pub(crate) fn translate_fun_item_maybe_enqueue(
729        &mut self,
730        span: Span,
731        item: &hax::ItemRef,
732        kind: TransItemSourceKind,
733        enqueue: bool,
734    ) -> Result<MaybeBuiltinFunDeclRef, Error> {
735        match self.recognize_builtin_fun(item)? {
736            Some(id) => {
737                let generics =
738                    self.translate_generic_args(span, &item.generic_args, &item.trait_proofs)?;
739                Ok(MaybeBuiltinFunDeclRef {
740                    id: FunId::Builtin(id),
741                    generics: Box::new(generics),
742                    trait_ref: None,
743                })
744            }
745            None => self.translate_item_maybe_enqueue(span, item, kind, enqueue),
746        }
747    }
748
749    /// Translate a reference to a trait method declaration without registering the declaration as
750    /// a `FunDecl`. `TraitDecl.methods` contains the declaration signature and metadata; only
751    /// default implementations give rise to a real function item.
752    fn translate_method_decl_fn_ptr(
753        &mut self,
754        span: Span,
755        item: &hax::ItemRef,
756    ) -> Result<Option<RegionBinder<FnPtr>>, Error> {
757        let Some(in_trait) = &item.in_trait else {
758            return Ok(None);
759        };
760        let def = self.hax_def(item)?;
761        let hax::FullDefKind::AssocFn {
762            associated_item,
763            sig,
764            ..
765        } = def.kind()
766        else {
767            return Ok(None);
768        };
769        if !matches!(
770            &associated_item.container,
771            hax::AssocItemContainer::TraitContainer { .. }
772        ) {
773            return Ok(None);
774        }
775
776        let trait_ref = self.translate_trait_proof(span, in_trait)?;
777        let generics = self.translate_generic_args(span, &item.generic_args, &item.trait_proofs)?;
778        self.translate_region_binder(span, &sig.as_ref().rebind(()), |ctx, _| {
779            let method_id = ctx.translate_trait_method_id(trait_ref.trait_id(), &item.def_id)?;
780            let fn_kind = FnPtrKind::Trait(trait_ref.move_under_binder(), method_id);
781            let generics = generics.move_under_binder();
782            let generics = generics.concat(&ctx.innermost_binder().params.identity_args());
783            Ok(FnPtr::new(fn_kind, generics))
784        })
785        .map(Some)
786    }
787
788    /// Auxiliary function to translate function calls and references to functions.
789    /// Translate a function id applied with some substitutions.
790    #[tracing::instrument(skip(self, span))]
791    pub(crate) fn translate_unbound_fn_ptr_maybe_enqueue(
792        &mut self,
793        span: Span,
794        item: &hax::ItemRef,
795        kind: TransItemSourceKind,
796        enqueue: bool,
797    ) -> Result<FnPtr, Error> {
798        let fun_item = self.translate_fun_item_maybe_enqueue(span, item, kind, enqueue)?;
799        let fun_id = match fun_item.trait_ref {
800            // Direct function call
801            None => FnPtrKind::Fun(fun_item.id),
802            // Trait method
803            Some(trait_ref) => {
804                let trait_decl_id = trait_ref.trait_id();
805                let method_id = self.translate_trait_method_id(trait_decl_id, &item.def_id)?;
806                FnPtrKind::Trait(trait_ref, method_id)
807            }
808        };
809        let mut generics = fun_item.generics;
810        // The last n regions are the late-bound ones and were provided as erased regions by
811        // `translate_item`.
812        for (a, b) in generics.regions.iter_mut().rev().zip(
813            self.innermost_binder()
814                .params
815                .identity_args()
816                .regions
817                .into_iter()
818                .rev(),
819        ) {
820            *a = b;
821        }
822        Ok(FnPtr::new(fun_id, generics))
823    }
824
825    #[tracing::instrument(skip(self, span))]
826    pub(crate) fn translate_bound_fn_ptr_maybe_enqueue(
827        &mut self,
828        span: Span,
829        item: &hax::ItemRef,
830        kind: TransItemSourceKind,
831        enqueue: bool,
832    ) -> Result<RegionBinder<FnPtr>, Error> {
833        if let Some(fn_ptr) = self.translate_method_decl_fn_ptr(span, item)? {
834            return Ok(fn_ptr);
835        }
836
837        let late_bound = self.hax_def(item)?.late_bound();
838        self.translate_region_binder(span, &late_bound, |ctx, _| {
839            ctx.translate_unbound_fn_ptr_maybe_enqueue(span, item, kind, enqueue)
840        })
841    }
842
843    /// Translate a reference to a function or trait method.
844    #[tracing::instrument(skip(self, span))]
845    pub(crate) fn translate_bound_fn_ptr(
846        &mut self,
847        span: Span,
848        item: &hax::ItemRef,
849        kind: TransItemSourceKind,
850    ) -> Result<RegionBinder<FnPtr>, Error> {
851        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, true)
852    }
853
854    pub(crate) fn translate_bound_fn_ptr_no_enqueue(
855        &mut self,
856        span: Span,
857        item: &hax::ItemRef,
858        kind: TransItemSourceKind,
859    ) -> Result<RegionBinder<FnPtr>, Error> {
860        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, false)
861    }
862
863    /// Translate a reference to a function or trait method, erasing or inferring its late-bound
864    /// lifetimes.
865    pub(crate) fn translate_fn_ptr(
866        &mut self,
867        span: Span,
868        item: &hax::ItemRef,
869        kind: TransItemSourceKind,
870    ) -> Result<FnPtr, Error> {
871        let fn_ptr = self.translate_bound_fn_ptr(span, item, kind)?;
872        let fn_ptr = self.erase_region_binder(fn_ptr);
873        Ok(fn_ptr)
874    }
875
876    pub(crate) fn translate_global_decl_ref(
877        &mut self,
878        span: Span,
879        item: &hax::ItemRef,
880    ) -> Result<GlobalDeclRef, Error> {
881        self.translate_item(span, item, TransItemSourceKind::Global)
882    }
883
884    pub(crate) fn translate_trait_decl_ref(
885        &mut self,
886        span: Span,
887        item: &hax::ItemRef,
888    ) -> Result<TraitDeclRef, Error> {
889        self.translate_item(span, item, TransItemSourceKind::TraitDecl)
890    }
891
892    pub(crate) fn translate_trait_impl_ref(
893        &mut self,
894        span: Span,
895        item: &hax::ItemRef,
896        kind: TraitImplSource,
897    ) -> Result<TraitImplRef, Error> {
898        self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
899    }
900}
901
902#[tracing::instrument(skip(tcx, error_ctx))]
903pub fn translate<'tcx>(
904    tcx: TyCtxt<'tcx>,
905    cli_options: &CliOpts,
906    mut error_ctx: ErrorCtx,
907    sysroot: PathBuf,
908) -> Result<TransformCtx, Error> {
909    let translate_options = TranslateOptions::new(&mut error_ctx, cli_options);
910
911    let traits_to_remove: HashSet<rustc_hir::def_id::DefId> = {
912        let hax_state = hax::state::State::new(
913            tcx,
914            hax::options::Options::default(),
915            hax::options::BoundsOptions::default(),
916        );
917        translate_options
918            .hide_traits
919            .iter()
920            .flat_map(|pat| super::resolve_path::def_path_def_ids(&hax_state, pat, true).unwrap())
921            .collect()
922    };
923    let hax_state = hax::state::State::new(
924        tcx,
925        hax::options::Options {
926            inline_anon_consts: !translate_options.raw_consts,
927        },
928        hax::options::BoundsOptions {
929            add_destruct_bounds: translate_options.add_destruct_bounds,
930            remove_traits: traits_to_remove,
931        },
932    );
933
934    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
935        .to_def_id()
936        .sinto(&hax_state);
937    let crate_name = crate_def_id.crate_name(&hax_state).to_string();
938    trace!("# Crate: {}", crate_name);
939
940    let mut ctx = TranslateCtx {
941        tcx,
942        sysroot,
943        hax_state,
944        options: translate_options,
945        errors: RefCell::new(error_ctx),
946        translated: TranslatedCrate {
947            crate_name,
948            options: cli_options.clone(),
949            ..TranslatedCrate::default()
950        },
951        method_status: Default::default(),
952        assoc_item_id_map: Default::default(),
953        id_map: Default::default(),
954        reverse_id_map: Default::default(),
955        file_to_id: Default::default(),
956        items_to_translate: Default::default(),
957        processed: Default::default(),
958        translate_stack: Default::default(),
959        cached_item_metas: Default::default(),
960        cached_names: Default::default(),
961        lt_mutability_computer: Default::default(),
962    };
963    ctx.register_target_info();
964
965    // Start translating from the selected items.
966    for start_from in ctx.options.start_from.clone() {
967        match start_from {
968            StartFrom::Pattern { pattern, strict } => {
969                if let Ok(def_ids) = ctx.resolve_path(Span::dummy(), &pattern, strict) {
970                    for def_id in def_ids {
971                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
972                        ctx.enqueue_module_item(&def_id);
973                    }
974                }
975            }
976            StartFrom::Attribute(attr_name) => {
977                let attr_path = attr_name
978                    .split("::")
979                    .map(rustc_span::Symbol::intern)
980                    .collect_vec();
981                let mut add_if_attr_matches = |ldid: rustc_hir::def_id::LocalDefId| {
982                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
983                    if !matches!(def_id.kind, hax::DefKind::Mod)
984                        && def_id.attrs(tcx).iter().any(|a| a.path_matches(&attr_path))
985                    {
986                        ctx.enqueue_module_item(&def_id);
987                    }
988                };
989                for ldid in tcx.hir_crate_items(()).definitions() {
990                    add_if_attr_matches(ldid)
991                }
992            }
993            StartFrom::Pub => {
994                let mut add_if_matches = |ldid: rustc_hir::def_id::LocalDefId| {
995                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
996                    if !matches!(def_id.kind, hax::DefKind::Mod)
997                        && def_id.visibility(tcx) == Some(true)
998                    {
999                        ctx.enqueue_module_item(&def_id);
1000                    }
1001                };
1002                for ldid in tcx.hir_crate_items(()).definitions() {
1003                    add_if_matches(ldid)
1004                }
1005            }
1006        }
1007    }
1008
1009    if ctx.errors.borrow().has_errors() {
1010        // Don't continue translating if there were errors while parsing options.
1011        return Err(Error::dummy());
1012    }
1013
1014    trace!(
1015        "Queue after we explored the crate:\n{:?}",
1016        &ctx.items_to_translate
1017    );
1018
1019    // Translate.
1020    //
1021    // For as long as the queue of items to translate is not empty, we pop the top item and
1022    // translate it. If an item refers to non-translated (potentially external) items, we add them
1023    // to the queue.
1024    //
1025    // Note that the order in which we translate the definitions doesn't matter:
1026    // we never need to lookup a translated definition, and only use the map
1027    // from Rust ids to translated ids.
1028    while let Some(item_src) = ctx.items_to_translate.pop_front() {
1029        if ctx.processed.insert(item_src.clone()) {
1030            ctx.translate_item(&item_src);
1031        }
1032    }
1033
1034    // Remove methods not marked as "used". They are never called and we made sure not to translate
1035    // them. This removes them from the traits and impls.
1036    ctx.remove_unused_methods();
1037
1038    // Return the context, dropping the hax state and rustc `tcx`.
1039    Ok(TransformCtx {
1040        options: ctx.options,
1041        translated: ctx.translated,
1042        errors: ctx.errors,
1043    })
1044}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
