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
13use itertools::Itertools;
14pub use rustc_middle::mir::Promoted as PromotedId;
15use rustc_span::DUMMY_SP;
16use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty};
17
18sinto_reexport!(hir::Safety);
19sinto_reexport!(hir::Mutability);
20sinto_reexport!(hir::def::CtorKind);
21sinto_reexport!(hir::def::MacroKinds);
22sinto_reexport!(hir::def::CtorOf);
23sinto_reexport!(rustc_span::symbol::Symbol);
24sinto_reexport!(rustc_span::symbol::ByteSymbol);
25
26/// Reflects [`rustc_hir::def::DefKind`]
27#[derive(AdtInto)]
28#[args(<S>, from: rustc_hir::def::DefKind, state: S as tcx)]
29#[derive(Debug, Clone, PartialEq, Hash, Eq)]
30pub enum DefKind {
31    Mod,
32    Struct,
33    Union,
34    Enum,
35    Variant,
36    Trait,
37    TyAlias,
38    ForeignTy,
39    TraitAlias,
40    AssocTy,
41    TyParam,
42    Fn,
43    Const {
44        is_type_const: bool,
45    },
46    ConstParam,
47    Static {
48        safety: Safety,
49        mutability: Mutability,
50        nested: bool,
51    },
52    Ctor(CtorOf, CtorKind),
53    AssocFn,
54    AssocConst {
55        is_type_const: bool,
56    },
57    Macro(MacroKinds),
58    ExternCrate,
59    Use,
60    ForeignMod,
61    AnonConst,
62    InlineConst,
63    #[disable_mapping]
64    /// Added by hax: promoted constants don't have def_ids in rustc but they do in hax.
65    PromotedConst,
66    OpaqueTy,
67    Field,
68    LifetimeParam,
69    GlobalAsm,
70    Impl {
71        of_trait: bool,
72    },
73    Closure,
74    SyntheticCoroutineBody,
75}
76
77/// The crate name under which synthetic items are exported under.
78const SYNTHETIC_CRATE_NAME: &str = "<synthetic>";
79
80/// Reflects [`rustc_hir::def_id::DefId`], augmented to also give ids to promoted constants (which
81/// have their own ad-hoc numbering scheme in rustc for now).
82#[derive(Clone, PartialEq, Eq)]
83pub struct DefId {
84    pub(crate) contents: HashConsed<DefIdContents>,
85}
86
87#[derive(Debug, Hash, Clone, PartialEq, Eq)]
88pub struct DefIdContents {
89    pub base: DefIdBase,
90    /// The kind of definition this `DefId` points to.
91    pub kind: crate::hax::DefKind,
92}
93
94#[derive(Debug, Hash, Clone, Copy, PartialEq, Eq)]
95pub enum DefIdBase {
96    Real(RDefId),
97    Promoted(RDefId, PromotedId),
98    /// This represents the context made of the trait impl generics plus the associated item
99    /// generics declared in the trait. We use that context to trait solve the mapping from
100    /// declared method generics to implemented method generics.
101    ImplAssocItem(VirtualImplAssocItem),
102    /// A completely fictitious item, we use this for arrays, slices and tuples to make
103    /// monomorphization and other shenanigans easier.
104    Synthetic(SyntheticItem),
105}
106
107#[derive(Debug, Hash, Clone, Copy, PartialEq, Eq)]
108pub struct VirtualImplAssocItem {
109    /// The trait impl.
110    pub trait_impl_id: RDefId,
111    /// The item declaration.
112    pub item_decl_id: RDefId,
113    /// The item implementation.
114    pub item_impl_id: RDefId,
115}
116
117impl VirtualImplAssocItem {
118    pub fn new(trait_impl_id: RDefId, item_decl_id: RDefId, item_impl_id: RDefId) -> Self {
119        Self {
120            trait_impl_id,
121            item_decl_id,
122            item_impl_id,
123        }
124    }
125
126    /// Arguments just for the item itself (works for both decl and impl), valid in the virtual
127    /// item context.
128    fn own_args<'tcx>(&self, s: &impl BaseState<'tcx>) -> Vec<ty::GenericArg<'tcx>> {
129        let tcx = s.base().tcx;
130        DefId::make_assoc_item_impl(s, *self)
131            .generics_of(s)
132            .own_params
133            .iter()
134            .map(|param| tcx.mk_param_from_def(param))
135            .collect()
136    }
137
138    /// Construct generic args for the item declaration, valid in the virtual item context.
139    pub fn args_for_item_decl<'tcx>(
140        &self,
141        s: &impl BaseState<'tcx>,
142        trait_args: ty::GenericArgsRef<'tcx>,
143    ) -> ty::GenericArgsRef<'tcx> {
144        let tcx = s.base().tcx;
145        tcx.mk_args_from_iter(trait_args.iter().chain(self.own_args(s)))
146    }
147
148    /// Construct generic args for the item implementation, valid in the virtual item context.
149    pub fn args_for_item_impl<'tcx>(
150        &self,
151        s: &impl BaseState<'tcx>,
152        impl_args: ty::GenericArgsRef<'tcx>,
153    ) -> ty::GenericArgsRef<'tcx> {
154        let tcx = s.base().tcx;
155        tcx.mk_args_from_iter(impl_args.iter().chain(self.own_args(s)))
156    }
157
158    /// Construct generic args for the item declaration, valid in the virtual item context.
159    pub fn identity_args_for_item_decl<'tcx>(
160        &self,
161        s: &impl BaseState<'tcx>,
162    ) -> ty::GenericArgsRef<'tcx> {
163        let tcx = s.base().tcx;
164        let impl_trait_ref = tcx
165            .impl_trait_ref(self.trait_impl_id)
166            .instantiate_identity()
167            .skip_normalization();
168        self.args_for_item_decl(s, impl_trait_ref.args)
169    }
170}
171
172impl DefIdContents {
173    pub fn make_def_id<'tcx, S: BaseState<'tcx>>(self, _s: &S) -> DefId {
174        let contents = HashConsed::new(self);
175        DefId { contents }
176    }
177}
178
179impl rustc_trait_elaboration::ItemId for DefId {
180    type State<'tcx> = StateWithBase<'tcx>;
181
182    fn from_rust_def_id<'tcx>(s: &Self::State<'tcx>, def_id: RDefId) -> Self {
183        def_id.sinto(s)
184    }
185
186    fn generics_of<'tcx>(&self, s: &Self::State<'tcx>) -> &'tcx ty::Generics {
187        DefId::generics_of(self, s)
188    }
189
190    fn param_env<'tcx>(&self, s: &Self::State<'tcx>) -> ty::ParamEnv<'tcx> {
191        DefId::param_env(self, s)
192    }
193
194    fn predicates_defined_on<'tcx>(
195        &self,
196        s: &Self::State<'tcx>,
197        direction: PredicateDirection,
198    ) -> ItemPredicates<'tcx, Self> {
199        let tcx = s.base().tcx;
200        match self.base {
201            DefIdBase::Real(def_id) => ItemPredicates::defined_on(tcx, s, def_id, direction),
202            DefIdBase::ImplAssocItem(id) => {
203                let item_args = id.identity_args_for_item_decl(s);
204                ItemPredicates::defined_on(tcx, s, id.item_decl_id, direction)
205                    .instantiate(tcx, item_args)
206            }
207            DefIdBase::Synthetic(synthetic) => {
208                synthetic.predicates_defined_on(s, self.clone(), direction)
209            }
210            DefIdBase::Promoted(..) => ItemPredicates::new_unmapped(DUMMY_SP, []),
211        }
212    }
213
214    fn self_pred<'tcx>(&self, s: &Self::State<'tcx>) -> Option<ty::PolyTraitRef<'tcx>> {
215        let tcx = s.base().tcx;
216        match self.base {
217            DefIdBase::Real(def_id) => def_id.self_pred(&tcx),
218            _ => None,
219        }
220    }
221
222    fn as_identity_assoc_ty<'tcx>(&self, s: &Self::State<'tcx>) -> Option<ty::Ty<'tcx>> {
223        let tcx = s.base().tcx;
224        match self.base {
225            DefIdBase::Real(def_id) => def_id.as_identity_assoc_ty(&tcx),
226            _ => None,
227        }
228    }
229
230    fn typeck_parent<'tcx>(&self, s: &Self::State<'tcx>) -> Option<Self> {
231        let tcx = s.base().tcx;
232        match self.base {
233            DefIdBase::Real(def_id) => def_id.typeck_parent(&tcx).map(|def_id| def_id.sinto(s)),
234            DefIdBase::Promoted(def_id, ..) => Some(tcx.typeck_root_def_id(def_id).sinto(s)),
235            DefIdBase::ImplAssocItem(..) | DefIdBase::Synthetic(..) => None,
236        }
237    }
238
239    fn parent_of_assoc<'tcx>(&self, s: &Self::State<'tcx>) -> Option<Self> {
240        let tcx = s.base().tcx;
241        match self.base {
242            DefIdBase::Real(def_id) => def_id.parent_of_assoc(&tcx).map(|def_id| def_id.sinto(s)),
243            DefIdBase::ImplAssocItem(id) => Some(id.trait_impl_id.sinto(s)),
244            _ => None,
245        }
246    }
247
248    fn parent_for_clauses<'tcx>(&self, s: &Self::State<'tcx>) -> Option<Self> {
249        let tcx = s.base().tcx;
250        match self.base {
251            DefIdBase::Real(def_id) => def_id
252                .parent_for_clauses(&tcx)
253                .map(|def_id| def_id.sinto(s)),
254            DefIdBase::ImplAssocItem(id) => Some(id.trait_impl_id.sinto(s)),
255            DefIdBase::Promoted(def_id, _) => Some(def_id.sinto(s)),
256            DefIdBase::Synthetic(..) => None,
257        }
258    }
259
260    fn takes_explicit_self_clause<'tcx>(&self, s: &Self::State<'tcx>) -> bool {
261        let tcx = s.base().tcx;
262        match self.base {
263            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => {
264                def_id.takes_explicit_self_clause(&tcx)
265            }
266            DefIdBase::ImplAssocItem(id) => id.item_decl_id.takes_explicit_self_clause(&tcx),
267            DefIdBase::Synthetic(..) => false,
268        }
269    }
270
271    fn find_in_impl<'tcx>(&self, s: &Self::State<'tcx>, trait_impl: &Self) -> Option<Self> {
272        let tcx = s.base().tcx;
273        let trait_impl = trait_impl.as_real_def_id()?;
274        match self.base {
275            DefIdBase::Real(def_id) => def_id
276                .find_in_impl(&tcx, &trait_impl)
277                .map(|def_id| def_id.sinto(s)),
278            _ => None,
279        }
280    }
281}
282
283impl DefId {
284    /// The rustc def_id corresponding to this item, if there is one. Promoted constants don't have
285    /// a rustc def_id.
286    pub fn as_real_def_id(&self) -> Option<RDefId> {
287        match self.base {
288            DefIdBase::Real(did) => Some(did),
289            _ => None,
290        }
291    }
292    /// The rustc def_id of this item. Panics if this is not a real rustc item.
293    pub fn real_rust_def_id(&self) -> RDefId {
294        self.as_real_def_id().unwrap()
295    }
296    /// The def_id of this item or its parent if this is a promoted constant.
297    pub fn as_real_or_promoted(&self) -> Option<RDefId> {
298        match self.base {
299            DefIdBase::Real(did) | DefIdBase::Promoted(did, ..) => Some(did),
300            _ => None,
301        }
302    }
303    pub fn promoted_id(&self) -> Option<PromotedId> {
304        match self.base {
305            DefIdBase::Promoted(_, promoted) => Some(promoted),
306            _ => None,
307        }
308    }
309    /// Returns the [`SyntheticItem`] encoded by this hax [`DefId`], if any.
310    pub fn as_synthetic<'tcx>(&self, _s: &impl BaseState<'tcx>) -> Option<SyntheticItem> {
311        match self.base {
312            DefIdBase::Synthetic(v) => Some(v),
313            _ => None,
314        }
315    }
316
317    pub fn is_local(&self) -> bool {
318        match self.base {
319            DefIdBase::Real(did) | DefIdBase::Promoted(did, ..) => did.is_local(),
320            DefIdBase::ImplAssocItem(id) => id.trait_impl_id.is_local(),
321            DefIdBase::Synthetic(..) => false,
322        }
323    }
324    pub fn is_typeck_child<'tcx>(&self, s: &impl BaseState<'tcx>) -> bool {
325        match self.base {
326            DefIdBase::Real(did) => s.base().tcx.is_typeck_child(did),
327            _ => false,
328        }
329    }
330
331    fn make<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> Self {
332        let base = DefIdBase::Real(def_id);
333        let tcx = s.base().tcx;
334        let contents = DefIdContents {
335            base,
336            kind: get_def_kind(tcx, def_id).sinto(s),
337        };
338        contents.make_def_id(s)
339    }
340
341    pub fn make_synthetic<'tcx, S: BaseState<'tcx>>(s: &S, synthetic: SyntheticItem) -> Self {
342        let contents = DefIdContents {
343            base: DefIdBase::Synthetic(synthetic),
344            kind: DefKind::Struct,
345        };
346        contents.make_def_id(s)
347    }
348
349    /// Construct a hax `DefId` for the nth promoted constant of the current item. That `DefId` has
350    /// no corresponding rustc `DefId`.
351    pub fn make_promoted_child<'tcx, S: BaseState<'tcx>>(
352        &self,
353        s: &S,
354        promoted_id: PromotedId,
355    ) -> Self {
356        let contents = DefIdContents {
357            base: DefIdBase::Promoted(self.real_rust_def_id(), promoted_id),
358            kind: DefKind::PromotedConst,
359        };
360        contents.make_def_id(s)
361    }
362
363    pub fn make_assoc_item_impl<'tcx, S: BaseState<'tcx>>(
364        s: &S,
365        vitem: VirtualImplAssocItem,
366    ) -> Self {
367        let tcx = s.base().tcx;
368        let contents = DefIdContents {
369            base: DefIdBase::ImplAssocItem(vitem),
370            kind: get_def_kind(tcx, vitem.item_decl_id).sinto(s),
371        };
372        contents.make_def_id(s)
373    }
374}
375
376impl DefId {
377    fn crate_name_and_disambig<'tcx>(&self, s: &impl BaseState<'tcx>) -> (Symbol, u32) {
378        let tcx = s.base().tcx;
379        match self.base {
380            DefIdBase::Real(def_id)
381            | DefIdBase::Promoted(def_id, ..)
382            | DefIdBase::ImplAssocItem(VirtualImplAssocItem {
383                trait_impl_id: def_id,
384                ..
385            }) => s.with_global_cache(|cache| cache.crate_name(tcx, def_id.krate)),
386            DefIdBase::Synthetic(..) => (Symbol::intern(SYNTHETIC_CRATE_NAME), 0),
387        }
388    }
389
390    pub fn crate_name<'tcx>(&self, s: &impl BaseState<'tcx>) -> Symbol {
391        self.crate_name_and_disambig(s).0
392    }
393
394    /// Get the span of the definition of this item. This is the span used in diagnostics when
395    /// referring to the item.
396    pub fn def_span<'tcx>(&self, s: &impl BaseState<'tcx>) -> Span {
397        use DefKind::*;
398        let tcx = s.base().tcx;
399        match self.base {
400            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => {
401                if let ForeignMod = &self.kind {
402                    // This kind causes `def_span` to panic.
403                    rustc_span::DUMMY_SP
404                } else if let Some(ldid) = def_id.as_local()
405                    && let hir_id = tcx.local_def_id_to_hir_id(ldid)
406                    && matches!(tcx.hir_node(hir_id), rustc_hir::Node::Synthetic)
407                {
408                    // This kind causes `def_span` to panic.
409                    rustc_span::DUMMY_SP
410                } else {
411                    tcx.def_span(def_id)
412                }
413            }
414            DefIdBase::ImplAssocItem(id) => tcx.def_span(id.item_impl_id),
415            DefIdBase::Synthetic(..) => rustc_span::DUMMY_SP,
416        }
417        .sinto(s)
418    }
419
420    /// The `PathItem` corresponding to this item.
421    pub fn path_item<'tcx>(&self, s: &impl BaseState<'tcx>) -> DisambiguatedDefPathItem {
422        match self.base {
423            DefIdBase::Real(def_id) => {
424                let tcx = s.base().tcx;
425                // Set the def_id so the `CrateRoot` path item can fetch the crate name.
426                let s = &s.with_hax_owner(self);
427                tcx.def_path(def_id)
428                    .data
429                    .last()
430                    .map(|x| x.sinto(s))
431                    .unwrap_or_else(|| {
432                        let (name, disambiguator) = self.crate_name_and_disambig(s);
433                        DisambiguatedDefPathItem {
434                            disambiguator,
435                            data: DefPathItem::CrateRoot { name },
436                        }
437                    })
438            }
439            DefIdBase::Promoted(_, id) => DisambiguatedDefPathItem {
440                data: DefPathItem::PromotedConst,
441                // Reuse the promoted id as disambiguator, like for inline consts.
442                disambiguator: id.as_u32(),
443            },
444            DefIdBase::ImplAssocItem(id) => {
445                let s = &s.with_hax_owner(self);
446                s.base()
447                    .tcx
448                    .def_path(id.item_decl_id)
449                    .data
450                    .last()
451                    .map(|x| x.sinto(s))
452                    .unwrap()
453            }
454            DefIdBase::Synthetic(synthetic) => DisambiguatedDefPathItem {
455                disambiguator: 0,
456                data: DefPathItem::TypeNs(Symbol::intern(&synthetic.name())),
457            },
458        }
459    }
460
461    pub fn parent<'tcx>(&self, s: &impl BaseState<'tcx>) -> Option<DefId> {
462        match self.base {
463            DefIdBase::Real(def_id) => s.tcx().opt_parent(def_id),
464            DefIdBase::Promoted(def_id, _) => Some(def_id),
465            DefIdBase::ImplAssocItem(id) => Some(id.trait_impl_id),
466            DefIdBase::Synthetic(..) => Some(rustc_span::def_id::CRATE_DEF_ID.to_def_id()),
467        }
468        .sinto(s)
469    }
470}
471
472impl DefId {
473    pub fn can_have_generics<'tcx>(&self, s: &impl BaseState<'tcx>) -> bool {
474        let tcx = s.base().tcx;
475        match self.base {
476            DefIdBase::Real(def_id)
477            | DefIdBase::Promoted(def_id, ..)
478            | DefIdBase::ImplAssocItem(VirtualImplAssocItem {
479                item_decl_id: def_id,
480                ..
481            }) => can_have_generics(tcx, def_id),
482            DefIdBase::Synthetic(synthetic) => synthetic.can_have_generics(s),
483        }
484    }
485
486    pub fn generics_of<'tcx>(&self, s: &impl BaseState<'tcx>) -> &'tcx ty::Generics {
487        let tcx = s.base().tcx;
488        match self.base {
489            DefIdBase::Real(def_id) => tcx.generics_of(def_id),
490            DefIdBase::Synthetic(synthetic) => synthetic.generics_of(s),
491            DefIdBase::Promoted(def_id, ..) => s.with_item_cache(self, |cache| {
492                if let Some(generics) = cache.virtual_generics {
493                    return generics;
494                }
495                let generics = Box::leak(Box::new(ty::Generics {
496                    parent: Some(def_id),
497                    parent_count: tcx.generics_of(def_id).count(),
498                    own_params: Default::default(),
499                    param_def_id_to_index: Default::default(),
500                    has_self: false,
501                    has_late_bound_regions: None,
502                }));
503                cache.virtual_generics = Some(generics);
504                generics
505            }),
506            DefIdBase::ImplAssocItem(id) => s.with_item_cache(self, |cache| {
507                if let Some(generics) = cache.virtual_generics {
508                    return generics;
509                }
510                // We build a custom environment here.
511                let item_id = id.item_impl_id;
512                let decl_generics = tcx.generics_of(item_id);
513                let parent_count = tcx.generics_of(id.trait_impl_id).count();
514                let own_params = tcx
515                    .generics_of(id.item_decl_id)
516                    .own_params
517                    .iter()
518                    .cloned()
519                    .enumerate()
520                    .map(|(i, mut param)| {
521                        param.index = parent_count as u32 + i as u32;
522                        param
523                    })
524                    .collect_vec();
525                let param_def_id_to_index = own_params
526                    .iter()
527                    .map(|param| (param.def_id, param.index))
528                    .collect();
529                let generics = Box::leak(Box::new(ty::Generics {
530                    parent: Some(id.trait_impl_id),
531                    parent_count,
532                    own_params,
533                    param_def_id_to_index,
534                    has_self: decl_generics.has_self,
535                    has_late_bound_regions: decl_generics.has_late_bound_regions,
536                }));
537                cache.virtual_generics = Some(generics);
538                generics
539            }),
540        }
541    }
542
543    pub fn identity_args<'tcx>(&self, s: &impl BaseState<'tcx>) -> ty::GenericArgsRef<'tcx> {
544        let tcx = s.base().tcx;
545        match self.base {
546            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => {
547                if can_have_generics(tcx, def_id) {
548                    ty::GenericArgs::identity_for_item(tcx, def_id)
549                } else {
550                    ty::GenericArgsRef::default()
551                }
552            }
553            DefIdBase::Synthetic(synthetic) => synthetic.identity_args(s),
554            DefIdBase::ImplAssocItem(_) => panic!(
555                "virtual trait impl associated items do not have a \
556                sensible `identity_args`. consider `identity_args_for_item_decl`"
557            ),
558        }
559    }
560
561    pub fn param_env<'tcx>(&self, s: &impl BaseState<'tcx>) -> ty::ParamEnv<'tcx> {
562        let tcx = s.base().tcx;
563        match self.base {
564            DefIdBase::ImplAssocItem(id) => {
565                let item_args = id.identity_args_for_item_decl(s);
566                let impl_predicates = tcx.param_env(id.trait_impl_id).caller_bounds().iter();
567                let item_predicates = tcx
568                    .predicates_of(id.item_decl_id)
569                    .instantiate_own(tcx, item_args)
570                    .map(|(predicate, _)| predicate.skip_normalization());
571                param_env_from_clauses(tcx, impl_predicates.chain(item_predicates))
572            }
573            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => {
574                if can_have_generics(tcx, def_id) {
575                    tcx.param_env(def_id)
576                } else {
577                    ty::ParamEnv::empty()
578                }
579            }
580            DefIdBase::Synthetic(synthetic) => synthetic.param_env(s),
581        }
582    }
583
584    pub fn typing_env<'tcx>(&self, s: &impl BaseState<'tcx>) -> ty::TypingEnv<'tcx> {
585        ty::TypingEnv::new(self.param_env(s), ty::TypingMode::PostAnalysis)
586    }
587
588    pub fn required_predicates<'tcx, S: BaseState<'tcx>>(
589        &self,
590        s: &S,
591    ) -> ItemPredicates<'tcx, Self> {
592        let state = s.base_state();
593        ItemPredicates::required(s.base().elab_ctx, &state, self.clone())
594    }
595
596    pub fn type_of<'tcx, S: BaseState<'tcx>>(&self, s: &S) -> ty::EarlyBinder<'tcx, ty::Ty<'tcx>> {
597        let tcx: ty::TyCtxt<'tcx> = s.base().tcx;
598        match self.base {
599            DefIdBase::Real(def_id) | DefIdBase::Promoted(def_id, ..) => tcx.type_of(def_id),
600            DefIdBase::Synthetic(synthetic) => synthetic.type_of(s),
601            DefIdBase::ImplAssocItem(id) => tcx.type_of(id.item_decl_id),
602        }
603    }
604}
605
606impl DefId {
607    /// Gets the visibility (`pub` or not) of the definition. Returns `None` for defs that don't have a
608    /// meaningful visibility.
609    pub fn visibility<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<bool> {
610        use DefKind::*;
611        match self.kind {
612            AssocConst { .. }
613            | AssocFn
614            | Const { .. }
615            | Enum
616            | Field
617            | Fn
618            | ForeignTy
619            | Macro { .. }
620            | Mod
621            | Static { .. }
622            | Struct
623            | Trait
624            | TraitAlias
625            | TyAlias { .. }
626            | Union
627            | Use
628            | Variant => {
629                let def_id = self.as_real_def_id()?;
630                Some(tcx.visibility(def_id).is_public())
631            }
632            // These kinds don't have visibility modifiers (which would cause `visibility` to panic).
633            AnonConst
634            | AssocTy
635            | Closure
636            | ConstParam
637            | Ctor { .. }
638            | ExternCrate
639            | ForeignMod
640            | GlobalAsm
641            | Impl { .. }
642            | InlineConst
643            | PromotedConst
644            | LifetimeParam
645            | OpaqueTy
646            | SyntheticCoroutineBody
647            | TyParam => None,
648        }
649    }
650
651    /// Gets the attributes of the definition.
652    pub fn attrs<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> &'tcx [rustc_hir::Attribute] {
653        use DefKind::*;
654        match self.kind {
655            // These kinds cause `get_attrs` to panic.
656            ConstParam | LifetimeParam | TyParam | ForeignMod | InlineConst => &[],
657            _ => {
658                if let Some(def_id) = self.as_real_def_id() {
659                    if let Some(ldid) = def_id.as_local() {
660                        tcx.hir_attrs(tcx.local_def_id_to_hir_id(ldid))
661                    } else {
662                        tcx.attrs_for_def(def_id)
663                    }
664                } else {
665                    &[]
666                }
667            }
668        }
669    }
670}
671
672impl std::ops::Deref for DefId {
673    type Target = DefIdContents;
674    fn deref(&self) -> &Self::Target {
675        &self.contents
676    }
677}
678
679impl std::fmt::Debug for DefId {
680    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
681        match self.base {
682            DefIdBase::Real(def_id) => write!(f, "{def_id:?}"),
683            DefIdBase::Promoted(def_id, promoted) => {
684                write!(f, "{def_id:?}::promoted#{}", promoted.as_u32())
685            }
686            DefIdBase::Synthetic(item) => write!(f, "{}", item.name()),
687            DefIdBase::ImplAssocItem(id) => {
688                write!(f, "{:?}::{:?}", id.trait_impl_id, id.item_decl_id)
689            }
690        }
691    }
692}
693
694impl std::hash::Hash for DefId {
695    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
696        self.base.hash(state);
697    }
698}
699
700/// Gets the kind of the definition. Can't use `def_kind` directly because this crashes on the
701/// crate root.
702pub(crate) fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> hir::def::DefKind {
703    if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() {
704        // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table
705        // isn't properly initialized otherwise.
706        let _ = tcx.def_span(def_id);
707    };
708    tcx.def_kind(def_id)
709}
710
711impl<'s, S: BaseState<'s>> SInto<S, DefId> for RDefId {
712    fn sinto(&self, s: &S) -> DefId {
713        if let Some(def_id) = s.with_global_cache(|cache| cache.def_ids.get(self).cloned()) {
714            return def_id;
715        }
716        let def_id = DefId::make(s, *self);
717        s.with_global_cache(|cache| {
718            cache.def_ids.insert(*self, def_id.clone());
719        });
720        def_id
721    }
722}
723
724impl<S> SInto<S, DefId> for DefId {
725    fn sinto(&self, _s: &S) -> DefId {
726        self.clone()
727    }
728}
729
730/// Reflects [`rustc_hir::definitions::DefPathData`]
731
732#[derive(Clone, Debug, Hash, PartialEq, Eq, AdtInto)]
733#[args(<'ctx, S: UnderOwnerState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as s)]
734pub enum DefPathItem {
735    CrateRoot {
736        #[value(s.owner().crate_name(s))]
737        name: Symbol,
738    },
739    Impl,
740    ForeignMod,
741    Use,
742    GlobalAsm,
743    TypeNs(Symbol),
744    ValueNs(Symbol),
745    MacroNs(Symbol),
746    LifetimeNs(Symbol),
747    Closure,
748    Ctor,
749    AnonConst,
750    #[disable_mapping]
751    PromotedConst,
752    OpaqueTy,
753    OpaqueLifetime(Symbol),
754    AnonAssocTy(Symbol),
755    SyntheticCoroutineBody,
756    NestedStatic,
757}
758
759#[derive(Clone, Debug, Hash, PartialEq, Eq, AdtInto)]
760#[args(<'a, S: UnderOwnerState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s)]
761/// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
762pub struct DisambiguatedDefPathItem {
763    pub data: DefPathItem,
764    pub disambiguator: u32,
765}
charon_driver/hax/types/def_id.rs

charon_driver/hax/types/
def_id.rs
