charon_driver/hax/types/
def_id.rs

1//! This module contains the type definition for `DefId` and the types
2//! `DefId` depends on.
3//!
4//! This is purposely a very small isolated module:
5//! `hax-engine-names-extract` uses those types, but we don't want
6//! `hax-engine-names-extract` to have a build dependency on the whole
7//! frontend, that double the build times for the Rust part of hax.
8
9use crate::hax::AdtInto;
10use crate::hax::prelude::*;
11use charon_lib::ast::HashConsed;
12
13pub use rustc_middle::mir::Promoted as PromotedId;
14use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty};
15
16sinto_reexport!(hir::Safety);
17sinto_reexport!(hir::Mutability);
18sinto_reexport!(hir::def::CtorKind);
19sinto_reexport!(hir::def::MacroKinds);
20sinto_reexport!(hir::def::CtorOf);
21sinto_reexport!(rustc_span::symbol::Symbol);
22sinto_reexport!(rustc_span::symbol::ByteSymbol);
23
24/// Reflects [`rustc_hir::def::DefKind`]
25#[derive(AdtInto)]
26#[args(<S>, from: rustc_hir::def::DefKind, state: S as tcx)]
27#[derive(Debug, Clone, PartialEq, Hash, Eq)]
28pub enum DefKind {
29    Mod,
30    Struct,
31    Union,
32    Enum,
33    Variant,
34    Trait,
35    TyAlias,
36    ForeignTy,
37    TraitAlias,
38    AssocTy,
39    TyParam,
40    Fn,
41    Const,
42    ConstParam,
43    Static {
44        safety: Safety,
45        mutability: Mutability,
46        nested: bool,
47    },
48    Ctor(CtorOf, CtorKind),
49    AssocFn,
50    AssocConst,
51    Macro(MacroKinds),
52    ExternCrate,
53    Use,
54    ForeignMod,
55    AnonConst,
56    InlineConst,
57    #[disable_mapping]
58    /// Added by hax: promoted constants don't have def_ids in rustc but they do in hax.
59    PromotedConst,
60    OpaqueTy,
61    Field,
62    LifetimeParam,
63    GlobalAsm,
64    Impl {
65        of_trait: bool,
66    },
67    Closure,
68    SyntheticCoroutineBody,
69}
70
71/// The crate name under which synthetic items are exported under.
72const SYNTHETIC_CRATE_NAME: &str = "<synthetic>";
73
74/// Reflects [`rustc_hir::def_id::DefId`], augmented to also give ids to promoted constants (which
75/// have their own ad-hoc numbering scheme in rustc for now).
76#[derive(Clone, PartialEq, Eq)]
77pub struct DefId {
78    pub(crate) contents: HashConsed<DefIdContents>,
79}
80
81#[derive(Debug, Hash, Clone, PartialEq, Eq)]
82pub struct DefIdContents {
83    pub base: DefIdBase,
84    /// The kind of definition this `DefId` points to.
85    pub kind: crate::hax::DefKind,
86}
87
88#[derive(Debug, Hash, Clone, Copy, PartialEq, Eq)]
89pub enum DefIdBase {
90    Real(RDefId),
91    Promoted(RDefId, PromotedId),
92    Synthetic(SyntheticItem, RDefId),
93}
94
95impl DefIdBase {
96    pub fn underlying_def_id(self) -> Option<RDefId> {
97        match self {
98            Self::Real(did) | Self::Promoted(did, ..) => Some(did),
99            Self::Synthetic(.., did) => Some(did),
100        }
101    }
102    pub fn as_real(self) -> Option<RDefId> {
103        match self {
104            Self::Real(did) => Some(did),
105            _ => None,
106        }
107    }
108    pub fn as_promoted(self) -> Option<(RDefId, PromotedId)> {
109        match self {
110            Self::Promoted(did, promoted) => Some((did, promoted)),
111            _ => None,
112        }
113    }
114    pub fn as_real_or_promoted(self) -> Option<RDefId> {
115        match self {
116            Self::Real(did) | Self::Promoted(did, ..) => Some(did),
117            _ => None,
118        }
119    }
120    pub fn as_synthetic(self) -> Option<SyntheticItem> {
121        if let Self::Synthetic(v, _) = self {
122            Some(v)
123        } else {
124            None
125        }
126    }
127}
128
129impl DefIdContents {
130    pub fn make_def_id<'tcx, S: BaseState<'tcx>>(self, _s: &S) -> DefId {
131        let contents = HashConsed::new(self);
132        DefId { contents }
133    }
134}
135
136impl DefId {
137    /// The rustc def_id corresponding to this item, if there is one. Promoted constants don't have
138    /// a rustc def_id.
139    pub fn as_rust_def_id(&self) -> Option<RDefId> {
140        self.base.as_real()
141    }
142    /// The rustc def_id of this item. Panics if this is not a real rustc item.
143    pub fn real_rust_def_id(&self) -> RDefId {
144        self.as_rust_def_id().unwrap()
145    }
146    /// The def_id of this item or its parent if this is a promoted constant.
147    pub fn underlying_rust_def_id(&self) -> Option<RDefId> {
148        self.base.as_real_or_promoted()
149    }
150    /// The def_id of this item, or its parent if this is a promoted constant, or a made-up `DefId`
151    /// for synthetic items. The method is explicitly named to phase out `DefId`s for synthetic
152    /// items.
153    pub fn as_def_id_even_synthetic(&self) -> RDefId {
154        self.base.underlying_def_id().unwrap()
155    }
156
157    pub fn is_local(&self) -> bool {
158        self.base
159            .underlying_def_id()
160            .is_some_and(|did| did.is_local())
161    }
162    pub fn promoted_id(&self) -> Option<PromotedId> {
163        self.base.as_promoted().map(|(_, p)| p)
164    }
165
166    fn make<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> Self {
167        let base = match s.with_global_cache(|c| c.reverse_synthetic_map.get(&def_id).copied()) {
168            None => DefIdBase::Real(def_id),
169            Some(synthetic) => return Self::make_synthetic(s, synthetic, def_id),
170        };
171        let tcx = s.base().tcx;
172        let contents = DefIdContents {
173            base,
174            kind: get_def_kind(tcx, def_id).sinto(s),
175        };
176        contents.make_def_id(s)
177    }
178
179    pub fn make_synthetic<'tcx, S: BaseState<'tcx>>(
180        s: &S,
181        synthetic: SyntheticItem,
182        def_id: RDefId,
183    ) -> Self {
184        let contents = DefIdContents {
185            base: DefIdBase::Synthetic(synthetic, def_id),
186            kind: DefKind::Struct,
187        };
188        contents.make_def_id(s)
189    }
190
191    /// Returns the [`SyntheticItem`] encoded by a [rustc `DefId`](RDefId), if
192    /// any.
193    ///
194    /// Note that this method relies on rustc indexes, which are session
195    /// specific. See [`Self`] documentation.
196    pub fn as_synthetic<'tcx>(&self, _s: &impl BaseState<'tcx>) -> Option<SyntheticItem> {
197        self.base.as_synthetic()
198    }
199
200    pub fn parent<'tcx>(&self, s: &impl BaseState<'tcx>) -> Option<DefId> {
201        match self.base {
202            DefIdBase::Real(def_id) => s.tcx().opt_parent(def_id),
203            DefIdBase::Promoted(def_id, _) => Some(def_id),
204            DefIdBase::Synthetic(..) => Some(rustc_span::def_id::CRATE_DEF_ID.to_def_id()),
205        }
206        .sinto(s)
207    }
208
209    pub fn crate_name<'tcx>(&self, s: &impl BaseState<'tcx>) -> Symbol {
210        let tcx = s.base().tcx;
211        match self.base {
212            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => {
213                tcx.crate_name(def_id.krate)
214            }
215            DefIdBase::Synthetic(..) => Symbol::intern(SYNTHETIC_CRATE_NAME),
216        }
217    }
218
219    /// The `PathItem` corresponding to this item.
220    pub fn path_item<'tcx>(&self, s: &impl BaseState<'tcx>) -> DisambiguatedDefPathItem {
221        match self.base {
222            DefIdBase::Real(def_id) => {
223                let tcx = s.base().tcx;
224                // Set the def_id so the `CrateRoot` path item can fetch the crate name.
225                let state_with_id = s.with_hax_owner(self);
226                tcx.def_path(def_id)
227                    .data
228                    .last()
229                    .map(|x| x.sinto(&state_with_id))
230                    .unwrap_or_else(|| DisambiguatedDefPathItem {
231                        disambiguator: 0,
232                        data: DefPathItem::CrateRoot {
233                            name: self.crate_name(s),
234                        },
235                    })
236            }
237            DefIdBase::Promoted(_, id) => DisambiguatedDefPathItem {
238                data: DefPathItem::PromotedConst,
239                // Reuse the promoted id as disambiguator, like for inline consts.
240                disambiguator: id.as_u32(),
241            },
242            DefIdBase::Synthetic(synthetic, ..) => DisambiguatedDefPathItem {
243                disambiguator: 0,
244                data: DefPathItem::TypeNs(Symbol::intern(&synthetic.name())),
245            },
246        }
247    }
248
249    /// Construct a hax `DefId` for the nth promoted constant of the current item. That `DefId` has
250    /// no corresponding rustc `DefId`.
251    pub fn make_promoted_child<'tcx, S: BaseState<'tcx>>(
252        &self,
253        s: &S,
254        promoted_id: PromotedId,
255    ) -> Self {
256        let contents = DefIdContents {
257            base: DefIdBase::Promoted(self.real_rust_def_id(), promoted_id),
258            kind: DefKind::PromotedConst,
259        };
260        contents.make_def_id(s)
261    }
262}
263
264impl DefId {
265    /// Gets the visibility (`pub` or not) of the definition. Returns `None` for defs that don't have a
266    /// meaningful visibility.
267    pub fn visibility<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<bool> {
268        use DefKind::*;
269        match self.kind {
270            AssocConst
271            | AssocFn
272            | Const
273            | Enum
274            | Field
275            | Fn
276            | ForeignTy
277            | Macro { .. }
278            | Mod
279            | Static { .. }
280            | Struct
281            | Trait
282            | TraitAlias
283            | TyAlias { .. }
284            | Union
285            | Use
286            | Variant => {
287                let def_id = self.as_rust_def_id()?;
288                Some(tcx.visibility(def_id).is_public())
289            }
290            // These kinds don't have visibility modifiers (which would cause `visibility` to panic).
291            AnonConst
292            | AssocTy
293            | Closure
294            | ConstParam
295            | Ctor { .. }
296            | ExternCrate
297            | ForeignMod
298            | GlobalAsm
299            | Impl { .. }
300            | InlineConst
301            | PromotedConst
302            | LifetimeParam
303            | OpaqueTy
304            | SyntheticCoroutineBody
305            | TyParam => None,
306        }
307    }
308
309    /// Gets the attributes of the definition.
310    pub fn attrs<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> &'tcx [rustc_hir::Attribute] {
311        use DefKind::*;
312        match self.kind {
313            // These kinds cause `get_attrs` to panic.
314            ConstParam | LifetimeParam | TyParam | ForeignMod | InlineConst => &[],
315            _ => {
316                if let Some(def_id) = self.as_rust_def_id() {
317                    if let Some(ldid) = def_id.as_local() {
318                        tcx.hir_attrs(tcx.local_def_id_to_hir_id(ldid))
319                    } else {
320                        tcx.attrs_for_def(def_id)
321                    }
322                } else {
323                    &[]
324                }
325            }
326        }
327    }
328}
329
330impl std::ops::Deref for DefId {
331    type Target = DefIdContents;
332    fn deref(&self) -> &Self::Target {
333        &self.contents
334    }
335}
336
337impl std::fmt::Debug for DefId {
338    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
339        match self.base {
340            DefIdBase::Real(def_id) => write!(f, "{def_id:?}"),
341            DefIdBase::Promoted(def_id, promoted) => {
342                write!(f, "{def_id:?}::promoted#{}", promoted.as_u32())
343            }
344            DefIdBase::Synthetic(item, _) => write!(f, "{}", item.name()),
345        }
346    }
347}
348
349impl std::hash::Hash for DefId {
350    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
351        self.base.hash(state);
352    }
353}
354
355/// Gets the kind of the definition. Can't use `def_kind` directly because this crashes on the
356/// crate root.
357pub(crate) fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> hir::def::DefKind {
358    if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() {
359        // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table
360        // isn't properly initialized otherwise.
361        let _ = tcx.def_span(def_id);
362    };
363    tcx.def_kind(def_id)
364}
365
366impl<'s, S: BaseState<'s>> SInto<S, DefId> for RDefId {
367    fn sinto(&self, s: &S) -> DefId {
368        if let Some(def_id) = s.with_item_cache(*self, |cache| cache.def_id.clone()) {
369            return def_id;
370        }
371        let def_id = DefId::make(s, *self);
372        s.with_item_cache(*self, |cache| cache.def_id = Some(def_id.clone()));
373        def_id
374    }
375}
376
377/// Reflects [`rustc_hir::definitions::DefPathData`]
378
379#[derive(Clone, Debug, Hash, PartialEq, Eq, AdtInto)]
380#[args(<'ctx, S: UnderOwnerState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as s)]
381pub enum DefPathItem {
382    CrateRoot {
383        #[value(s.base().tcx.crate_name(s.owner_id().krate).sinto(s))]
384        name: Symbol,
385    },
386    Impl,
387    ForeignMod,
388    Use,
389    GlobalAsm,
390    TypeNs(Symbol),
391    ValueNs(Symbol),
392    MacroNs(Symbol),
393    LifetimeNs(Symbol),
394    Closure,
395    Ctor,
396    LateAnonConst,
397    AnonConst,
398    #[disable_mapping]
399    PromotedConst,
400    DesugaredAnonymousLifetime,
401    OpaqueTy,
402    OpaqueLifetime(Symbol),
403    AnonAssocTy(Symbol),
404    SyntheticCoroutineBody,
405    NestedStatic,
406}
407
408#[derive(Clone, Debug, Hash, PartialEq, Eq, AdtInto)]
409#[args(<'a, S: UnderOwnerState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s)]
410/// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
411pub struct DisambiguatedDefPathItem {
412    pub data: DefPathItem,
413    pub disambiguator: u32,
414}
charon_driver/hax/types/def_id.rs

charon_driver/hax/types/
def_id.rs
