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 petgraph::visit::{Dfs, Walker};
19use rustc_middle::ty::{self, TyCtxt};
20use rustc_span::{def_id::DefId, sym};
21use std::cell::RefCell;
22use std::collections::HashSet;
23use std::path::PathBuf;
24
25use super::translate_ctx::*;
26use crate::hax;
27use crate::hax::SInto;
28use charon_lib::ast::*;
29use charon_lib::name_matcher::NamePattern;
30use charon_lib::options::{CliOpts, ConstHandling, StartFrom, TranslateOptions};
31use charon_lib::transform::TransformCtx;
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(Debug, Clone, PartialEq, Eq, Hash)]
37pub struct TransItemSource<'tcx> {
38    pub item: RustcItem<'tcx>,
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(Debug, Clone, PartialEq, Eq, Hash)]
50pub enum RustcItem<'tcx> {
51    Poly(hax::DefId),
52    Mono(hax::ItemRef<'tcx>),
53    MonoTrait(hax::DefId),
54}
55
56/// The kind of a [`TransItemSource`].
57#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
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    /// Shim function to store a method in a vtable; give a method with `self: Ptr<Self>` argument,
81    /// this takes a `Ptr<dyn Trait>` and forwards to the method. For a `Normal` impl the `DefId`
82    /// refers to the method implementation; for a `Callable` one it refers to the closure or fn
83    /// item, whose `call_*` method has no `DefId` of its own.
84    VTableMethod(TransImplSource),
85    /// The drop shim function to be used in the vtable as a field.
86    VTableDropShim(TransImplSource),
87    /// The fallback body of an intrinsic. The `DefId` is that of the intrinsic.
88    IntrinsicFallback,
89}
90
91/// The kind of a [`TransItemSourceKind::TraitImpl`].
92#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
93pub enum TransImplSource {
94    /// A user-written trait impl with a `DefId`.
95    Normal,
96    /// The blanket impl we generate for a trait alias. The `DefId` is that of the trait alias.
97    TraitAlias,
98    /// An impl of the appropriate `Fn*` trait for a closure or function item.
99    Callable(ClosureKind),
100    /// A fictitious `impl Destruct for T` that contains the drop glue code for the given ADT or
101    /// closure. The `DefId` is that of the ADT or closure.
102    ImplicitDestruct,
103    /// A marker-trait implementation. The `DefId` is that of the trait.
104    Marker,
105}
106
107impl<'tcx> TransItemSource<'tcx> {
108    pub fn new(item: RustcItem<'tcx>, kind: TransItemSourceKind) -> Self {
109        if let RustcItem::Mono(item) = &item {
110            if item.has_non_lt_param {
111                panic!("Item is not monomorphic: {item:?}")
112            }
113        } else if let RustcItem::MonoTrait(_) = &item
114            && !kind.is_for_trait()
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(
124        item: &hax::ItemRef<'tcx>,
125        kind: TransItemSourceKind,
126        monomorphize: bool,
127    ) -> Self {
128        if monomorphize {
129            if kind.is_for_trait() {
130                Self::monomorphic_trait(&item.def_id, kind)
131            } else {
132                Self::monomorphic(item, kind)
133            }
134        } else {
135            Self::polymorphic(&item.def_id, kind)
136        }
137    }
138
139    /// Refers to the polymorphic version of this item.
140    pub fn polymorphic(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
141        Self::new(RustcItem::Poly(def_id.clone()), kind)
142    }
143
144    /// Refers to the monomorphic version of this item.
145    pub fn monomorphic(item: &hax::ItemRef<'tcx>, kind: TransItemSourceKind) -> Self {
146        Self::new(RustcItem::Mono(item.clone()), kind)
147    }
148
149    /// Refers to the monomorphic trait (or vtable).
150    /// See the docs of `RustcItem::MonoTrait` for details.
151    pub fn monomorphic_trait(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
152        Self::new(RustcItem::MonoTrait(def_id.clone()), kind)
153    }
154
155    pub fn def_id(&self) -> &hax::DefId {
156        self.item.def_id()
157    }
158
159    /// Keep the same def_id but change the kind.
160    pub(crate) fn with_kind(&self, kind: TransItemSourceKind) -> Self {
161        let mut ret = self.clone();
162        ret.kind = kind;
163        ret
164    }
165
166    /// For virtual items that have a parent (typically a method impl), return this parent. Does
167    /// not attempt to generally compute the parent of an item. Used to compute names.
168    pub(crate) fn parent(&self) -> Option<Self> {
169        let parent_kind = match self.kind {
170            TransItemSourceKind::CallableMethod(kind)
171            | TransItemSourceKind::VTableMethod(TransImplSource::Callable(kind)) => {
172                TransItemSourceKind::TraitImpl(TransImplSource::Callable(kind))
173            }
174            TransItemSourceKind::DropGlueMethod(TransImplSource::Marker)
175            | TransItemSourceKind::VTableInstance(TransImplSource::Marker)
176            | TransItemSourceKind::VTableDropShim(TransImplSource::Marker) => {
177                TransItemSourceKind::TraitDecl
178            }
179            TransItemSourceKind::DropGlueMethod(impl_kind)
180            | TransItemSourceKind::VTableInstance(impl_kind)
181            | TransItemSourceKind::VTableDropShim(impl_kind) => {
182                TransItemSourceKind::TraitImpl(impl_kind)
183            }
184            _ => return None,
185        };
186        Some(self.with_kind(parent_kind))
187    }
188
189    /// Whether this item is the "main" item for this def_id or not (e.g. Destruct impl/methods are not
190    /// the main item).
191    pub(crate) fn is_derived_item(&self) -> bool {
192        self.kind.is_derived_item()
193    }
194}
195
196impl TransItemSourceKind {
197    fn is_derived_item(self) -> bool {
198        use TransItemSourceKind::*;
199        !matches!(
200            self,
201            Global
202                | TraitDecl
203                | TraitImpl(TransImplSource::Normal)
204                | InherentImpl
205                | Module
206                | Fun
207                | Type
208        )
209    }
210
211    pub fn is_for_trait(&self) -> bool {
212        matches!(
213            self,
214            TransItemSourceKind::TraitDecl | TransItemSourceKind::VTable
215        )
216    }
217}
218
219impl<'tcx> RustcItem<'tcx> {
220    pub fn def_id(&self) -> &hax::DefId {
221        match self {
222            RustcItem::Poly(def_id) => def_id,
223            RustcItem::Mono(item_ref) => &item_ref.def_id,
224            RustcItem::MonoTrait(def_id) => def_id,
225        }
226    }
227}
228
229impl<'tcx> TranslateCtx<'tcx> {
230    /// If this is a trait method declaration, return the `DefId` of its parent trait.
231    fn as_trait_method_decl(&mut self, def_id: &hax::DefId) -> Option<hax::DefId> {
232        if matches!(def_id.kind, hax::DefKind::AssocFn)
233            && let def = self.poly_hax_def(def_id).ok()?
234            && let hax::FullDefKind::AssocFn(f) = def.kind()
235            && let associated_item = f.associated_item()
236            && let hax::AssocItemContainer::TraitContainer { trait_ref } =
237                &associated_item.container
238        {
239            Some(trait_ref.def_id.clone())
240        } else {
241            None
242        }
243    }
244
245    /// Resolve a path to a list of matching `DefId`s.
246    pub fn resolve_path(
247        &self,
248        span: Span,
249        pat: &NamePattern,
250        strict: bool,
251    ) -> Result<Vec<rustc_span::def_id::DefId>, Error> {
252        super::resolve_path::def_path_def_ids(&self.hax_state, pat, strict).map_err(|err| {
253            register_error!(self, span, "failed to resolve item path `{pat}`: {err}")
254        })
255    }
256
257    /// Resolve a path that is expected to name exactly one item.
258    pub fn resolve_single_path(
259        &self,
260        span: Span,
261        pat: &NamePattern,
262    ) -> Result<rustc_span::def_id::DefId, Error> {
263        self.resolve_path(span, pat, true)?
264            .into_iter()
265            .exactly_one()
266            .map_err(|_| register_error!(self, span, "expected exactly one item for path `{pat}`"))
267    }
268
269    fn register_polymorphic_function(&mut self, def_id: DefId) -> FunDeclId {
270        let def_id = def_id.sinto(&self.hax_state);
271        let item = TransItemSource::polymorphic(&def_id, TransItemSourceKind::Fun);
272        self.register_and_enqueue(&None, item).expect_item()
273    }
274
275    fn register_poly_function_by_path(&mut self, path: &str) -> Result<FunDeclId, Error> {
276        let path = NamePattern::parse(path).unwrap();
277        let def_id = self.resolve_single_path(Span::dummy(), &path)?;
278        Ok(self.register_polymorphic_function(def_id))
279    }
280
281    /// Register the std functions needed for `builtins_to_function_calls`.
282    fn register_builtin_functions(&mut self) -> Result<(), Error> {
283        if self.options.ops_to_function_calls {
284            self.register_poly_function_by_path("array::as_slice")?;
285            self.register_poly_function_by_path("array::as_mut_slice")?;
286            self.register_poly_function_by_path("core::array::repeat")?;
287        }
288        if self.options.index_to_function_calls {
289            let tcx = self.tcx;
290            for (trait_id, method_name) in [
291                (tcx.lang_items().index_trait().unwrap(), sym::index),
292                (tcx.lang_items().index_mut_trait().unwrap(), sym::index_mut),
293            ] {
294                let impls = tcx.all_impls(trait_id).filter(|&impl_id| {
295                    matches!(
296                        tcx.impl_trait_ref(impl_id).skip_binder().self_ty().kind(),
297                        ty::Array(..) | ty::Slice(..)
298                    )
299                });
300                for impl_id in impls {
301                    let method_id = tcx
302                        .associated_items(impl_id)
303                        .in_definition_order()
304                        .find(|item| item.name() == method_name)
305                        .unwrap()
306                        .def_id;
307                    self.register_polymorphic_function(method_id);
308                }
309            }
310            let trait_id = self.tcx.get_diagnostic_item(sym::SliceIndex).unwrap();
311            let impls = self.tcx.all_impls(trait_id).filter(|&impl_id| {
312                let trait_ref = tcx.impl_trait_ref(impl_id).skip_binder();
313                trait_ref.args.type_at(1).is_slice()
314                    && match trait_ref.self_ty().kind() {
315                        ty::Uint(ty::UintTy::Usize) => true,
316                        ty::Adt(def, args) => {
317                            tcx.is_lang_item(def.did(), rustc_hir::attrs::LangItem::Range)
318                                && args.type_at(0) == tcx.types.usize
319                        }
320                        _ => false,
321                    }
322            });
323            for impl_id in impls {
324                let methods = tcx
325                    .associated_items(impl_id)
326                    .in_definition_order()
327                    .filter(|item| item.name() == sym::index || item.name() == sym::index_mut)
328                    .map(|item| item.def_id);
329                for method_id in methods {
330                    self.register_polymorphic_function(method_id);
331                }
332            }
333        }
334        Ok(())
335    }
336
337    /// Returns the default translation kind for the given `DefId`. Returns `None` for items that
338    /// we don't translate. Errors on unexpected items.
339    pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
340        use crate::hax::DefKind::*;
341        Some(match &def_id.kind {
342            Enum | Struct | Union | TyAlias | ForeignTy => TransItemSourceKind::Type,
343            Fn | AssocFn => TransItemSourceKind::Fun,
344            Const | Static { .. } | AssocConst => TransItemSourceKind::Global,
345            Trait | TraitAlias => TransItemSourceKind::TraitDecl,
346            Impl { of_trait: true } => TransItemSourceKind::TraitImpl(TransImplSource::Normal),
347            Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
348            Mod | ForeignMod => TransItemSourceKind::Module,
349
350            // We skip these
351            ExternCrate | FnPtr | GlobalAsm | Macro { .. } | Use => return None,
352            // These can happen when doing `--start-from` on a foreign crate. We can skip them
353            // because their parents will already have been registered.
354            Ctor { .. } | Variant => return None,
355            // We cannot encounter these since they're not top-level items.
356            AnonConst
357            | AssocTy
358            | Closure
359            | ConstParam
360            | Field
361            | PromotedConst
362            | LifetimeParam
363            | OpaqueTy
364            | SyntheticCoroutineBody
365            | TestBinderConstraints
366            | TyParam => {
367                let span = self.def_span(def_id);
368                register_error!(
369                    self,
370                    span,
371                    "Cannot register item `{def_id:?}` with kind `{:?}`",
372                    def_id.kind
373                );
374                return None;
375            }
376        })
377    }
378
379    /// Add this item to the queue of items to translate. Each translated item will then
380    /// recursively register the items it refers to. We call this on the crate root and end up
381    /// exploring the whole crate.
382    #[tracing::instrument(skip(self))]
383    pub fn enqueue_module_item(
384        &mut self,
385        def_id: &hax::DefId,
386        // Item that contains this one.
387        parent: ContainmentNode,
388    ) -> Option<ItemOrModuleId> {
389        if let Some(trait_def_id) = self.as_trait_method_decl(def_id) {
390            // Selecting a method also selects its containing trait. Mark the method used so
391            // its default body is enqueued even if the trait is opaque.
392            let trait_item_id = self.enqueue_module_item(&trait_def_id, parent)?;
393            let trait_id = trait_item_id.expect_item();
394            let method_id = self.translate_trait_method_id(trait_id, def_id).ok()?;
395            self.record_containment(parent, ContainmentNode::TraitMethod(trait_id, method_id));
396            return Some(trait_item_id);
397        }
398        let kind = self.base_kind_for_item(def_id)?;
399        let item_src = if self.options.monomorphize_with_hax {
400            if let Ok(def) = self.poly_hax_def(def_id)
401                && !def.has_any_generics()
402            {
403                // Monomorphize this item and the items it depends on.
404                TransItemSource::monomorphic(def.this(), kind)
405            } else {
406                // Skip polymorphic items and items that cause errors.
407                return None;
408            }
409        } else {
410            TransItemSource::polymorphic(def_id, kind)
411        };
412        let id = self.register_and_enqueue(&None, item_src);
413        self.record_containment(parent, id);
414        Some(id)
415    }
416
417    /// Record that the parent contains the child, for the purposes of computing which items are
418    /// included in the "started from" set.
419    pub(crate) fn record_containment(
420        &mut self,
421        parent: impl Into<ContainmentNode>,
422        child: impl Into<ContainmentNode>,
423    ) {
424        self.containment_graph
425            .add_edge(parent.into(), child.into(), ());
426    }
427
428    /// Use the computed `containment_graph` to deduce which items should be considered as being
429    /// targeted by `--start-from`, which then affects which items are used to compute used
430    /// declarations.
431    fn compute_started_from(&mut self) {
432        let reachable: HashSet<_> = Dfs::new(&self.containment_graph, ContainmentNode::Start)
433            .iter(&self.containment_graph)
434            .collect();
435        for node in &reachable {
436            if let ContainmentNode::Item(ItemOrModuleId::Item(id)) = node
437                && let Some(mut item) = self.translated.get_item_mut(*id)
438            {
439                item.item_meta().started_from = true;
440            }
441        }
442        // Trait declarations also store method metadata.
443        for tdecl in self.translated.trait_decls.iter_mut() {
444            for (method_id, method) in tdecl.methods.iter_mut_indexed() {
445                let node = ContainmentNode::TraitMethod(tdecl.def_id, method_id);
446                method.skip_binder.item_meta.started_from = reachable.contains(&node);
447            }
448        }
449    }
450
451    /// Whether this item is polymorphic, while we are in monomorphic mode.
452    pub(crate) fn is_poly_in_mono(&self, item_src: &TransItemSource) -> bool {
453        self.options.monomorphize_with_hax && matches!(item_src.item, RustcItem::Poly(..))
454    }
455
456    pub(crate) fn register_no_enqueue(
457        &mut self,
458        dep_src: &Option<DepSource>,
459        src: &TransItemSource<'tcx>,
460    ) -> ItemOrModuleId {
461        let item_id = match self.id_map.get(src) {
462            Some(tid) => *tid,
463            None => {
464                use TransItemSourceKind::*;
465                let trans_id = match src.kind {
466                    Type | VTable => ItemId::Type(self.translated.type_decls.reserve_slot()),
467                    TraitDecl => ItemId::TraitDecl(self.translated.trait_decls.reserve_slot()),
468                    TraitImpl(..) => ItemId::TraitImpl(self.translated.trait_impls.reserve_slot()),
469                    Global | VTableInstance(..) => {
470                        ItemId::Global(self.translated.global_decls.reserve_slot())
471                    }
472                    Fun | CallableMethod(..) | ClosureAsFnCast | DropGlueMethod(..)
473                    | VTableMethod(..) | VTableDropShim(..) | IntrinsicFallback => {
474                        ItemId::Fun(self.translated.fun_decls.reserve_slot())
475                    }
476                    InherentImpl | Module => {
477                        return ItemOrModuleId::Module(src.def_id().real_rust_def_id());
478                    }
479                };
480                // Add the id to the queue of declarations to translate
481                self.id_map.insert(src.clone(), trans_id);
482                self.reverse_id_map.insert(trans_id, src.clone());
483                // Store the name early so the name matcher can identify paths.
484                if let Ok(name) = self.translate_name(src) {
485                    self.translated.item_names.insert(trans_id, name);
486                }
487                trans_id
488            }
489        };
490        self.errors
491            .borrow_mut()
492            .register_dep_source(dep_src, item_id, src.def_id().is_local());
493        ItemOrModuleId::Item(item_id)
494    }
495
496    /// Register this item source and enqueue it for translation.
497    pub(crate) fn register_and_enqueue(
498        &mut self,
499        dep_src: &Option<DepSource>,
500        item_src: TransItemSource<'tcx>,
501    ) -> ItemOrModuleId {
502        let id = self.register_no_enqueue(dep_src, &item_src);
503        self.items_to_translate.push_back(item_src);
504        id
505    }
506
507    /// Enqueue an item from its id.
508    pub(crate) fn enqueue_id(&mut self, id: impl Into<ItemId>) {
509        let id = id.into();
510        if self.translated.get_item(id).is_none() {
511            let item_src = self.reverse_id_map[&id].clone();
512            self.items_to_translate.push_back(item_src);
513        }
514    }
515
516    /// Register the associated types of this trait.
517    pub fn register_assoc_items(
518        &mut self,
519        trait_def_id: &hax::DefId,
520        trait_id: TraitDeclId,
521    ) -> Result<(), Error> {
522        if self.method_status.get(trait_id).is_some() {
523            return Ok(());
524        }
525        let trait_def = self.poly_hax_def(trait_def_id)?;
526        let hax::FullDefKind::Trait(t) = trait_def.kind() else {
527            unreachable!()
528        };
529        let names = self
530            .translated
531            .assoc_item_names
532            .get_or_insert_with(trait_id, Default::default);
533        for item in t.items(&self.hax_state) {
534            let name = TraitItemName(
535                item.name
536                    .as_ref()
537                    .map(|n| n.to_string().into())
538                    .unwrap_or_default(),
539            );
540            let id: AssocItemId = match item.kind {
541                hax::AssocKind::Type { .. } => names.types.push(name).into(),
542                hax::AssocKind::Fn { .. } => names.methods.push(name).into(),
543                hax::AssocKind::Const { .. } => names.consts.push(name).into(),
544            };
545            self.assoc_item_id_map.insert(item.def_id.clone(), id);
546        }
547        // Add a virtual method to the `Destruct` trait.
548        if trait_def.lang_item == Some(sym::destruct) {
549            let method_name = TraitItemName("drop_glue".into());
550            names.methods.push(method_name);
551        }
552        self.method_status.get_or_insert_with(trait_id, || {
553            names.methods.map_ref(|_| MethodStatus::default())
554        });
555        Ok(())
556    }
557
558    /// Get the unique per-trait id corresponding to this associated item. The `DefId` can be of an
559    /// item declaration or item implementation.
560    pub fn translate_assoc_item_id(
561        &mut self,
562        trait_id: TraitDeclId,
563        item_def_id: &hax::DefId,
564    ) -> Result<AssocItemId, Error> {
565        // The same assoc item `DefId` could belong to several `TraitDeclId`s because of
566        // monomorphization, so we only return the item id if we know this trait's data is
567        // initialized.
568        if let Some(&item_id) = self.assoc_item_id_map.get(item_def_id)
569            && self.method_status.get(trait_id).is_some()
570        {
571            return Ok(item_id);
572        }
573
574        let item_def = self.poly_hax_def(item_def_id)?;
575        let assoc = match item_def.kind() {
576            hax::FullDefKind::AssocTy(t) => t.associated_item(),
577            hax::FullDefKind::AssocConst(c) => c.associated_item(),
578            hax::FullDefKind::AssocFn(f) => f.associated_item(),
579            _ => panic!("Unexpected def for associated item: {item_def:?}"),
580        };
581        let decl_def_id = assoc.implemented_trait_item_id();
582
583        if decl_def_id != item_def_id
584            && let Some(&item_id) = self.assoc_item_id_map.get(decl_def_id)
585            && self.method_status.get(trait_id).is_some()
586        {
587            self.assoc_item_id_map.insert(item_def_id.clone(), item_id);
588            return Ok(item_id);
589        }
590
591        let trait_def_id = decl_def_id.parent(&self.hax_state).unwrap();
592        self.register_assoc_items(&trait_def_id, trait_id)?;
593        let item_id = *self.assoc_item_id_map.get(decl_def_id).unwrap();
594        Ok(item_id)
595    }
596
597    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
598    /// This does not make the method be considered "used"; use `mark_method_as_used` for that.
599    pub fn translate_trait_method_id_no_enqueue(
600        &mut self,
601        trait_id: TraitDeclId,
602        def_id: &hax::DefId,
603    ) -> Result<TraitMethodId, Error> {
604        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
605        Ok(*item_id.as_method().unwrap())
606    }
607    /// Register a trait method and return its `TraitMethodId`. This id is unique per trait.
608    /// This makes the method be considered "used".
609    pub fn translate_trait_method_id(
610        &mut self,
611        trait_id: TraitDeclId,
612        def_id: &hax::DefId,
613    ) -> Result<TraitMethodId, Error> {
614        let method_id = self.translate_trait_method_id_no_enqueue(trait_id, def_id)?;
615        self.mark_method_as_used(trait_id, method_id);
616        Ok(method_id)
617    }
618    /// Register a trait associated type and return its `AssocTypeId`. This id is unique per trait.
619    pub fn translate_assoc_type_id(
620        &mut self,
621        trait_id: TraitDeclId,
622        def_id: &hax::DefId,
623    ) -> Result<AssocTypeId, Error> {
624        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
625        Ok(*item_id.as_type().unwrap())
626    }
627    /// Register a trait associated const and return its `AssocTypeId`. This id is unique per trait.
628    pub fn translate_assoc_const_id(
629        &mut self,
630        trait_id: TraitDeclId,
631        def_id: &hax::DefId,
632    ) -> Result<AssocConstId, Error> {
633        let item_id = self.translate_assoc_item_id(trait_id, def_id)?;
634        Ok(*item_id.as_const().unwrap())
635    }
636
637    /// Claim the first type id for the declaration of the unit type.
638    pub(crate) fn reserve_unit_decl(&mut self) {
639        let def_id = hax::DefId::make_synthetic(&self.hax_state, hax::SyntheticItem::Tuple(0));
640        let item_src = if self.options.monomorphize_with_hax
641            && let Ok(def) = self.poly_hax_def(&def_id)
642        {
643            TransItemSource::monomorphic(def.this(), TransItemSourceKind::Type)
644        } else {
645            TransItemSource::polymorphic(&def_id, TransItemSourceKind::Type)
646        };
647        let id = if self.options.no_gen_tuple_structs {
648            self.register_and_enqueue(&None, item_src)
649        } else {
650            self.register_no_enqueue(&None, &item_src)
651        };
652        assert_eq!(
653            id,
654            ItemOrModuleId::Item(TypeDeclId::UNIT.into()),
655            "the unit type must come first"
656        );
657    }
658
659    pub(crate) fn register_target_info(&mut self) {
660        let target_data = &self.tcx.data_layout;
661        let triple = self.get_target_triple();
662
663        let mut primitive_alignments = SeqHashMap::new();
664        primitive_alignments.insert(ScalarTy::Bool, target_data.i8_align.bytes());
665        for (ty, alignment) in [
666            (IntegerTy::Signed(IntTy::I8), target_data.i8_align.bytes()),
667            (IntegerTy::Signed(IntTy::I16), target_data.i16_align.bytes()),
668            (IntegerTy::Signed(IntTy::I32), target_data.i32_align.bytes()),
669            (IntegerTy::Signed(IntTy::I64), target_data.i64_align.bytes()),
670            (
671                IntegerTy::Signed(IntTy::I128),
672                target_data.i128_align.bytes(),
673            ),
674            (
675                IntegerTy::Signed(IntTy::Isize),
676                target_data.pointer_align().bytes(),
677            ),
678            (
679                IntegerTy::Unsigned(UIntTy::U8),
680                target_data.i8_align.bytes(),
681            ),
682            (
683                IntegerTy::Unsigned(UIntTy::U16),
684                target_data.i16_align.bytes(),
685            ),
686            (
687                IntegerTy::Unsigned(UIntTy::U32),
688                target_data.i32_align.bytes(),
689            ),
690            (
691                IntegerTy::Unsigned(UIntTy::U64),
692                target_data.i64_align.bytes(),
693            ),
694            (
695                IntegerTy::Unsigned(UIntTy::U128),
696                target_data.i128_align.bytes(),
697            ),
698            (
699                IntegerTy::Unsigned(UIntTy::Usize),
700                target_data.pointer_align().bytes(),
701            ),
702        ] {
703            primitive_alignments.insert(ScalarTy::Integer(ty), alignment);
704        }
705        primitive_alignments.insert(ScalarTy::Float(FloatTy::F16), target_data.f16_align.bytes());
706        primitive_alignments.insert(ScalarTy::Float(FloatTy::F32), target_data.f32_align.bytes());
707        primitive_alignments.insert(ScalarTy::Float(FloatTy::F64), target_data.f64_align.bytes());
708        primitive_alignments.insert(
709            ScalarTy::Float(FloatTy::F128),
710            target_data.f128_align.bytes(),
711        );
712        // INFO: This is not explicitly guaranteed by the reference, but by the implementation of rustc.
713        // https://doc.rust-lang.org/1.97.1/nightly-rustc/src/rustc_ty_utils/layout.rs.html#391
714        primitive_alignments.insert(ScalarTy::Char, target_data.i32_align.bytes());
715
716        let c_enum_smallest_repr_ty = match target_data.c_enum_min_size {
717            rustc_abi::Integer::I8 => IntTy::I8,
718            rustc_abi::Integer::I16 => IntTy::I16,
719            rustc_abi::Integer::I32 => IntTy::I32,
720            rustc_abi::Integer::I64 => IntTy::I64,
721            rustc_abi::Integer::I128 => IntTy::I128,
722        };
723
724        let target = &self.tcx.sess.target;
725        let info = TargetInfo {
726            arch: self
727                .translate_rustc_arch(&target.arch)
728                .expect("all rustc Arch variants should be translated"),
729            vendor: target.vendor_symbol().to_string(),
730            os: self
731                .translate_rustc_os(&target.os)
732                .expect("all rustc Os variants should be translated"),
733            env: self
734                .translate_rustc_env(&target.env)
735                .expect("all rustc Env variants should be translated"),
736            cfg_abi: self
737                .translate_rustc_cfg_abi(&target.cfg_abi)
738                .expect("all rustc CfgAbi variants should be translated"),
739            families: target.families.iter().map(|f| f.to_string()).collect(),
740            binary_format: self
741                .translate_rustc_binary_format(&target.binary_format)
742                .expect("all rustc BinaryFormat variants should be translated"),
743            target_pointer_size: target_data.pointer_size().bytes(),
744            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
745            c_enum_smallest_repr_ty,
746            primitive_alignments,
747        };
748        self.translated.target_information.insert(triple, info);
749    }
750}
751
752// Id and item reference registration.
753impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
754    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
755        Some(DepSource {
756            src_id: self.item_id.as_item()?,
757            span: self.item_src.def_id().is_local().then_some(span),
758        })
759    }
760
761    /// Register this item source and enqueue it for translation.
762    pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
763        &mut self,
764        span: Span,
765        item_src: TransItemSource<'tcx>,
766    ) -> T {
767        let dep_src = self.make_dep_source(span);
768        self.t_ctx
769            .register_and_enqueue(&dep_src, item_src)
770            .expect_item()
771    }
772
773    pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
774        &mut self,
775        span: Span,
776        src: &TransItemSource<'tcx>,
777    ) -> T {
778        let dep_src = self.make_dep_source(span);
779        self.t_ctx.register_no_enqueue(&dep_src, src).expect_item()
780    }
781
782    /// Register this item and maybe enqueue it for translation.
783    pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
784        &mut self,
785        span: Span,
786        enqueue: bool,
787        item: &hax::ItemRef<'tcx>,
788        kind: TransItemSourceKind,
789    ) -> T {
790        let mono = self.should_monomorphize_item(item, kind);
791        let item = if mono && item.has_param {
792            item.erase(self.hax_state_with_id())
793        } else {
794            item.clone()
795        };
796        let item_src = TransItemSource::from_item(&item, kind, mono);
797        if enqueue {
798            self.register_and_enqueue(span, item_src)
799        } else {
800            self.register_no_enqueue(span, &item_src)
801        }
802    }
803
804    /// Register this item and enqueue it for translation.
805    pub(crate) fn register_item<T: TryFrom<ItemId>>(
806        &mut self,
807        span: Span,
808        item: &hax::ItemRef<'tcx>,
809        kind: TransItemSourceKind,
810    ) -> T {
811        self.register_item_maybe_enqueue(span, true, item, kind)
812    }
813
814    /// Register this item without enqueueing it for translation.
815    #[expect(dead_code)]
816    pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
817        &mut self,
818        span: Span,
819        item: &hax::ItemRef<'tcx>,
820        kind: TransItemSourceKind,
821    ) -> T {
822        self.register_item_maybe_enqueue(span, false, item, kind)
823    }
824
825    /// Register this item and maybe enqueue it for translation.
826    pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<DeclRef<ItemId>>>(
827        &mut self,
828        span: Span,
829        hax_item: &hax::ItemRef<'tcx>,
830        kind: TransItemSourceKind,
831        enqueue: bool,
832    ) -> Result<T, Error> {
833        let hax_item = if kind.is_derived_item() {
834            // If the original item is an associated item we should ignore that and refer to it
835            // like a top-level item.
836            &hax_item.re_resolve(self.hax_state_with_id(), hax::AssocItemResolution::None)
837        } else {
838            hax_item
839        };
840
841        let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, hax_item, kind);
842        // In mono mode, we keep trait decls generic.
843        let mut generics = if self.should_monomorphize_item(hax_item, kind)
844            && !matches!(kind, TransItemSourceKind::TraitDecl)
845        {
846            GenericArgs::empty()
847        } else {
848            self.translate_generic_args(span, hax_item)?
849        };
850
851        // Recover regions that rustc normally erases.
852        let regions = self.recover_extra_early_regions(span, hax_item)?;
853        generics.regions.extend(regions);
854
855        // Add regions to make sure the item args match the params we set up in
856        // `translate_item_generics`.
857        if matches!(
858            hax_item.def_id.kind,
859            hax::DefKind::Fn
860                | hax::DefKind::FnPtr
861                | hax::DefKind::AssocFn
862                | hax::DefKind::Closure
863                | hax::DefKind::Ctor(..)
864        ) {
865            let def = self.hax_def(hax_item)?;
866            let sig = match def.kind() {
867                hax::FullDefKind::Fn(f) => Some(f.sig()),
868                hax::FullDefKind::FnPtr(f) => Some(f.sig()),
869                hax::FullDefKind::AssocFn(f) => Some(f.sig()),
870                hax::FullDefKind::Ctor(f) => Some(f.sig()),
871                hax::FullDefKind::Closure(c)
872                    if let TransItemSourceKind::TraitImpl(TransImplSource::Callable(..))
873                    | TransItemSourceKind::VTableInstance(TransImplSource::Callable(..))
874                    | TransItemSourceKind::VTableDropShim(TransImplSource::Callable(..))
875                    | TransItemSourceKind::CallableMethod(..)
876                    | TransItemSourceKind::VTableMethod(TransImplSource::Callable(..))
877                    | TransItemSourceKind::ClosureAsFnCast = kind =>
878                {
879                    Some(c.sig())
880                }
881                _ => None,
882            };
883            if let Some(sig) = sig {
884                generics.regions.extend(
885                    sig.bound_vars
886                        .iter()
887                        .map(|_| self.translate_erased_region()),
888                );
889            }
890            if let TransItemSourceKind::CallableMethod(ClosureKind::FnMut | ClosureKind::Fn)
891            | TransItemSourceKind::VTableMethod(TransImplSource::Callable(
892                ClosureKind::FnMut | ClosureKind::Fn,
893            )) = kind
894            {
895                generics.regions.push(self.translate_erased_region());
896            }
897            // If we're in the process of translating this same item (possibly with a
898            // different `TransItemSourceKind`), we can reuse the generics they have in
899            // common.
900            if self.item_src.def_id() == &hax_item.def_id {
901                let depth = self.binding_levels.depth();
902                for (a, b) in generics.regions.iter_mut().zip(
903                    self.outermost_binder()
904                        .params
905                        .identity_args_at_depth(depth)
906                        .regions,
907                ) {
908                    *a = b;
909                }
910            }
911        }
912        if matches!(
913            kind,
914            TransItemSourceKind::DropGlueMethod(..) | TransItemSourceKind::VTableDropShim(..)
915        ) {
916            generics = generics.concat(&self.drop_glue_generic_args());
917        }
918
919        let trait_ref = hax_item
920            .in_trait
921            .as_ref()
922            .map(|trait_proof| self.translate_trait_proof(span, trait_proof))
923            .transpose()?
924            .map(PolyTraitRef::erase);
925
926        let item = DeclRef {
927            id,
928            generics: Box::new(generics),
929            trait_ref,
930        };
931        Ok(item.try_into().ok().unwrap())
932    }
933
934    /// Register this item and enqueue it for translation.
935    ///
936    /// Note: for `FnPtr`s use `translate_fn_ptr` instead, as this handles late-bound variables
937    /// correctly. For `TypeDeclRef`s use `translate_type_decl_ref` instead, as this correctly
938    /// recognizes built-in ADTs.
939    pub(crate) fn translate_item<T: TryFrom<DeclRef<ItemId>>>(
940        &mut self,
941        span: Span,
942        item: &hax::ItemRef<'tcx>,
943        kind: TransItemSourceKind,
944    ) -> Result<T, Error> {
945        self.translate_item_maybe_enqueue(span, item, kind, true)
946    }
947
948    /// Translate a type def id
949    pub(crate) fn translate_type_decl_ref(
950        &mut self,
951        span: Span,
952        item: &hax::ItemRef<'tcx>,
953    ) -> Result<TypeDeclRef, Error> {
954        self.translate_type_decl_ref_maybe_enqueue(span, item, TransItemSourceKind::Type, true)
955    }
956
957    /// Register a type item and maybe enqueue it for translation. Use this to
958    /// obtain a `TypeDeclRef`, don't construct one manually.
959    pub(crate) fn translate_type_decl_ref_maybe_enqueue(
960        &mut self,
961        span: Span,
962        item: &hax::ItemRef<'tcx>,
963        kind: TransItemSourceKind,
964        enqueue: bool,
965    ) -> Result<TypeDeclRef, Error> {
966        let builtin = match kind {
967            TransItemSourceKind::Type => self.recognize_builtin_adt(item),
968            _ => None,
969        };
970        if builtin == Some(BuiltinAdt::Tuple) && self.t_ctx.options.no_gen_tuple_structs {
971            // The declaration has no clauses, so we drop the `Sized` proofs of the fields.
972            let generics = self.translate_generic_args_without_trait_refs(span, item)?;
973            return Ok(TypeDeclRef {
974                id: TypeDeclId::UNIT,
975                generics: Box::new(generics),
976                builtin,
977            });
978        }
979        let item_ref: DeclRef<ItemId> =
980            self.translate_item_maybe_enqueue(span, item, kind, enqueue)?;
981        assert!(item_ref.trait_ref.is_none());
982        Ok(TypeDeclRef {
983            id: item_ref.id.try_into().unwrap(),
984            generics: item_ref.generics,
985            builtin,
986        })
987    }
988
989    /// Translate a reference to a trait method declaration without registering the declaration as
990    /// a `FunDecl`. `TraitDecl.methods` contains the declaration signature and metadata; only
991    /// default implementations give rise to a real function item.
992    fn translate_method_decl_fn_ptr(
993        &mut self,
994        span: Span,
995        item: &hax::ItemRef<'tcx>,
996    ) -> Result<Option<RegionBinder<FnPtr>>, Error> {
997        let Some(in_trait) = &item.in_trait else {
998            return Ok(None);
999        };
1000        let def = self.hax_def(item)?;
1001        let hax::FullDefKind::AssocFn(f) = def.kind() else {
1002            return Ok(None);
1003        };
1004        if !matches!(
1005            &f.associated_item().container,
1006            hax::AssocItemContainer::TraitContainer { .. }
1007        ) {
1008            return Ok(None);
1009        }
1010
1011        let trait_ref = self.translate_trait_proof(span, in_trait)?.erase();
1012        let generics = self.translate_generic_args(span, item)?;
1013        self.translate_region_binder(span, &f.sig().as_ref().rebind(()), |ctx, _| {
1014            let method_id = ctx.translate_trait_method_id(trait_ref.trait_id(), &item.def_id)?;
1015            let fn_kind = FnPtrKind::Trait(trait_ref.move_under_binder(), method_id);
1016            let generics = generics.move_under_binder();
1017            let generics = generics.concat(&ctx.innermost_binder().params.identity_args());
1018            Ok(FnPtr::new(fn_kind, generics))
1019        })
1020        .map(Some)
1021    }
1022
1023    /// Translate a function reference, assuming that the late-bound regions are in scope. Prefer
1024    /// the `translate_bound_fn_ptr*` methods whenever sensible.
1025    #[tracing::instrument(skip(self, span))]
1026    pub(crate) fn translate_unbound_fn_ptr_maybe_enqueue(
1027        &mut self,
1028        span: Span,
1029        item: &hax::ItemRef<'tcx>,
1030        kind: TransItemSourceKind,
1031        enqueue: bool,
1032    ) -> Result<FnPtr, Error> {
1033        let fun_item: DeclRef<ItemId> =
1034            self.translate_item_maybe_enqueue(span, item, kind, enqueue)?;
1035        let fun_item: DeclRef<FunDeclId> = fun_item.try_convert_id().unwrap();
1036        let fun_id = match fun_item.trait_ref {
1037            // Direct function call
1038            None => FnPtrKind::Fun(fun_item.id),
1039            // Trait method
1040            Some(trait_ref) => {
1041                let trait_decl_id = trait_ref.trait_id();
1042                let method_id = self.translate_trait_method_id(trait_decl_id, &item.def_id)?;
1043                FnPtrKind::Trait(trait_ref, method_id)
1044            }
1045        };
1046        let mut generics = fun_item.generics;
1047        // The last n regions are the late-bound ones and were provided as erased regions by
1048        // `translate_item`.
1049        for (a, b) in generics.regions.iter_mut().rev().zip(
1050            self.innermost_binder()
1051                .params
1052                .identity_args()
1053                .regions
1054                .into_iter()
1055                .rev(),
1056        ) {
1057            *a = b;
1058        }
1059        Ok(FnPtr::new(fun_id, generics))
1060    }
1061
1062    #[tracing::instrument(skip(self, span))]
1063    pub(crate) fn translate_bound_fn_ptr_maybe_enqueue(
1064        &mut self,
1065        span: Span,
1066        item: &hax::ItemRef<'tcx>,
1067        kind: TransItemSourceKind,
1068        enqueue: bool,
1069    ) -> Result<RegionBinder<FnPtr>, Error> {
1070        if let Some(fn_ptr) = self.translate_callable_method_fn_ptr(span, item)? {
1071            return Ok(fn_ptr);
1072        }
1073        if let Some(fn_ptr) = self.translate_method_decl_fn_ptr(span, item)? {
1074            return Ok(fn_ptr);
1075        }
1076
1077        let late_bound = self.hax_def(item)?.late_bound();
1078        self.translate_region_binder(span, &late_bound, |ctx, _| {
1079            ctx.translate_unbound_fn_ptr_maybe_enqueue(span, item, kind, enqueue)
1080        })
1081    }
1082
1083    /// Translate a reference to a function or trait method.
1084    #[tracing::instrument(skip(self, span))]
1085    pub(crate) fn translate_bound_fn_ptr(
1086        &mut self,
1087        span: Span,
1088        item: &hax::ItemRef<'tcx>,
1089        kind: TransItemSourceKind,
1090    ) -> Result<RegionBinder<FnPtr>, Error> {
1091        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, true)
1092    }
1093
1094    pub(crate) fn translate_bound_fn_ptr_no_enqueue(
1095        &mut self,
1096        span: Span,
1097        item: &hax::ItemRef<'tcx>,
1098        kind: TransItemSourceKind,
1099    ) -> Result<RegionBinder<FnPtr>, Error> {
1100        self.translate_bound_fn_ptr_maybe_enqueue(span, item, kind, false)
1101    }
1102
1103    /// Translate a reference to a function or trait method, erasing or inferring its late-bound
1104    /// lifetimes.
1105    pub(crate) fn translate_fn_ptr(
1106        &mut self,
1107        span: Span,
1108        item: &hax::ItemRef<'tcx>,
1109        kind: TransItemSourceKind,
1110    ) -> Result<FnPtr, Error> {
1111        let fn_ptr = self.translate_bound_fn_ptr(span, item, kind)?;
1112        let fn_ptr = self.erase_region_binder(fn_ptr);
1113        Ok(fn_ptr)
1114    }
1115
1116    pub(crate) fn translate_global_decl_ref(
1117        &mut self,
1118        span: Span,
1119        item: &hax::ItemRef<'tcx>,
1120    ) -> Result<GlobalDeclRef, Error> {
1121        self.translate_item(span, item, TransItemSourceKind::Global)
1122    }
1123
1124    pub(crate) fn translate_trait_decl_ref(
1125        &mut self,
1126        span: Span,
1127        item: &hax::ItemRef<'tcx>,
1128    ) -> Result<TraitDeclRef, Error> {
1129        self.translate_item(span, item, TransItemSourceKind::TraitDecl)
1130    }
1131
1132    pub(crate) fn translate_trait_impl_ref(
1133        &mut self,
1134        span: Span,
1135        item: &hax::ItemRef<'tcx>,
1136        kind: TransImplSource,
1137    ) -> Result<TraitImplRef, Error> {
1138        self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
1139    }
1140}
1141
1142#[tracing::instrument(skip(tcx, error_ctx))]
1143pub fn translate<'tcx>(
1144    tcx: TyCtxt<'tcx>,
1145    cli_options: &CliOpts,
1146    mut error_ctx: ErrorCtx,
1147    sysroot: PathBuf,
1148) -> Result<TransformCtx, Error> {
1149    let translate_options = TranslateOptions::new(&mut error_ctx, cli_options);
1150
1151    let traits_to_remove: HashSet<rustc_hir::def_id::DefId> = {
1152        let hax_state = hax::state::State::new(
1153            tcx,
1154            hax::options::Options::default(),
1155            hax::options::BoundsOptions::default(),
1156        );
1157        translate_options
1158            .hide_traits
1159            .iter()
1160            .flat_map(|pat| super::resolve_path::def_path_def_ids(&hax_state, pat, true).unwrap())
1161            .collect()
1162    };
1163    let hax_state = hax::state::State::new(
1164        tcx,
1165        hax::options::Options {
1166            inline_anon_consts: !translate_options.raw_consts,
1167            consts: rustc_const_uneval::Config {
1168                anon_allocs_as_globals: matches!(
1169                    translate_options.consts,
1170                    ConstHandling::Values | ConstHandling::Bytes
1171                ),
1172            },
1173            treat_box_as_builtin: translate_options.treat_box_as_builtin,
1174        },
1175        hax::options::BoundsOptions {
1176            add_destruct_bounds: translate_options.add_destruct_bounds,
1177            remove_traits: traits_to_remove,
1178        },
1179    );
1180
1181    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
1182        .to_def_id()
1183        .sinto(&hax_state);
1184    let crate_name = crate_def_id.crate_name(&hax_state).to_string();
1185    trace!("# Crate: {}", crate_name);
1186
1187    let mut ctx = TranslateCtx {
1188        tcx,
1189        sysroot,
1190        hax_state,
1191        options: translate_options,
1192        errors: RefCell::new(error_ctx),
1193        translated: TranslatedCrate {
1194            crate_name,
1195            options: cli_options.clone(),
1196            runtime_checks: RuntimeChecks {
1197                ub_checks: tcx.sess.ub_checks(),
1198                overflow_checks: tcx.sess.overflow_checks(),
1199                contract_checks: tcx.sess.contract_checks(),
1200            },
1201            ..TranslatedCrate::default()
1202        },
1203        method_status: Default::default(),
1204        assoc_item_id_map: Default::default(),
1205        id_map: Default::default(),
1206        reverse_id_map: Default::default(),
1207        file_to_id: Default::default(),
1208        items_to_translate: Default::default(),
1209        processed: Default::default(),
1210        containment_graph: Default::default(),
1211        translate_stack: Default::default(),
1212        cached_spans: Default::default(),
1213        cached_file_ids: Default::default(),
1214        cached_names: Default::default(),
1215        cached_item_metas: Default::default(),
1216        lt_mutability_computer: Default::default(),
1217    };
1218    ctx.register_target_info();
1219    ctx.reserve_unit_decl();
1220    ctx.register_builtin_functions()?;
1221
1222    // Start translating from the selected items.
1223    for start_from in ctx.options.start_from.clone() {
1224        match start_from {
1225            StartFrom::Pattern { pattern, strict } => {
1226                if let Ok(def_ids) = ctx.resolve_path(Span::dummy(), &pattern, strict) {
1227                    for def_id in def_ids {
1228                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
1229                        ctx.enqueue_module_item(&def_id, ContainmentNode::Start);
1230                    }
1231                }
1232            }
1233            StartFrom::Attribute(attr_name) => {
1234                let attr_path = attr_name
1235                    .split("::")
1236                    .map(rustc_span::Symbol::intern)
1237                    .collect_vec();
1238                let mut add_if_attr_matches = |ldid: rustc_hir::def_id::LocalDefId| {
1239                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
1240                    if !matches!(def_id.kind, hax::DefKind::Mod)
1241                        && def_id.attrs(tcx).iter().any(|a| a.path_matches(&attr_path))
1242                    {
1243                        ctx.enqueue_module_item(&def_id, ContainmentNode::Start);
1244                    }
1245                };
1246                for ldid in tcx.hir_crate_items(()).definitions() {
1247                    add_if_attr_matches(ldid)
1248                }
1249            }
1250            StartFrom::Pub => {
1251                let mut add_if_matches = |ldid: rustc_hir::def_id::LocalDefId| {
1252                    let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state);
1253                    if !matches!(def_id.kind, hax::DefKind::Mod)
1254                        && def_id.visibility(tcx) == Some(true)
1255                    {
1256                        ctx.enqueue_module_item(&def_id, ContainmentNode::Start);
1257                    }
1258                };
1259                for ldid in tcx.hir_crate_items(()).definitions() {
1260                    add_if_matches(ldid)
1261                }
1262            }
1263            StartFrom::GlobalCtors => {
1264                // Translate constructors that run before the program start; this is decided
1265                // by the linker, which is a bit obscure, so we follow the same logic as Miri. See:
1266                // https://github.com/rust-lang/miri/blob/ddd2b2fc87565b16fd38e7cab9838295aaca1c40/src/shims/global_ctor.rs
1267                use rustc_middle::middle::codegen_fn_attrs::CodegenFnAttrFlags;
1268                use rustc_middle::middle::exported_symbols::ExportedSymbol;
1269                use rustc_structures::CrateType;
1270                use rustc_target::spec::BinaryFormat;
1271                let is_ctor_section = |section: &str| match tcx.sess.target.binary_format {
1272                    BinaryFormat::Coff => section == ".CRT$XCU",
1273                    BinaryFormat::MachO => {
1274                        let mut parts = section.splitn(3, ',');
1275                        parts.next() == Some("__DATA")
1276                            && parts.next() == Some("__mod_init_func")
1277                            && matches!(parts.next(), None | Some("mod_init_funcs"))
1278                    }
1279                    BinaryFormat::Elf | BinaryFormat::Wasm => section == ".init_array",
1280                    _ => false,
1281                };
1282                let mut add_if_ctor = |rust_def_id: DefId, used: bool| {
1283                    if used
1284                        && let Some(section) = tcx.codegen_fn_attrs(rust_def_id).link_section
1285                        && is_ctor_section(section.as_str())
1286                    {
1287                        let def_id: hax::DefId = rust_def_id.sinto(&ctx.hax_state);
1288                        ctx.enqueue_module_item(&def_id, ContainmentNode::Start);
1289                    }
1290                };
1291                // For the local crate, we walk all its items and check their `#[used]` flags.
1292                // We can't do like below because if the crate is a binary its exported symbols
1293                // don't include its `#[used]` statics.
1294                for ldid in tcx.hir_crate_items(()).definitions() {
1295                    if tcx.def_kind(ldid).has_codegen_attrs() && !tcx.is_foreign_item(ldid) {
1296                        let flags = tcx.codegen_fn_attrs(ldid).flags;
1297                        let used = flags.intersects(
1298                            CodegenFnAttrFlags::USED_COMPILER | CodegenFnAttrFlags::USED_LINKER,
1299                        );
1300                        add_if_ctor(ldid.to_def_id(), used);
1301                    }
1302                }
1303                // For binary crates, we also look at the exported symbols of the dependencies,
1304                // because their constructors get linked into the final executable.
1305                if tcx.crate_types().contains(&CrateType::Executable) {
1306                    for &cnum in tcx.crates(()) {
1307                        if tcx.crate_dep_kind(cnum).macros_only() {
1308                            continue;
1309                        }
1310                        for &(symbol, info) in tcx.exported_non_generic_symbols(cnum) {
1311                            if let ExportedSymbol::NonGeneric(def_id) = symbol
1312                                && !tcx.is_foreign_item(def_id)
1313                            {
1314                                add_if_ctor(def_id, info.used);
1315                            }
1316                        }
1317                    }
1318                }
1319            }
1320        }
1321    }
1322
1323    if ctx.errors.borrow().has_errors() {
1324        // Don't continue translating if there were errors while parsing options.
1325        return Err(Error::dummy());
1326    }
1327
1328    trace!(
1329        "Queue after we explored the crate:\n{:?}",
1330        &ctx.items_to_translate
1331    );
1332
1333    // Translate.
1334    //
1335    // For as long as the queue of items to translate is not empty, we pop the top item and
1336    // translate it. If an item refers to non-translated (potentially external) items, we add them
1337    // to the queue.
1338    //
1339    // Note that the order in which we translate the definitions doesn't matter:
1340    // we never need to lookup a translated definition, and only use the map
1341    // from Rust ids to translated ids.
1342    while let Some(item_src) = ctx.items_to_translate.pop_front() {
1343        if ctx.processed.insert(item_src.clone()) {
1344            ctx.translate_item(&item_src);
1345        }
1346    }
1347
1348    // Remove methods not marked as "used". They are never called and we made sure not to translate
1349    // them. This removes them from the traits and impls.
1350    ctx.remove_unused_methods();
1351    ctx.compute_started_from();
1352
1353    // Return the context, dropping the hax state and rustc `tcx`.
1354    Ok(TransformCtx {
1355        options: ctx.options,
1356        translated: ctx.translated,
1357        errors: ctx.errors,
1358    })
1359}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
