charon_driver/hax/types/
adt.rs

1use crate::hax::prelude::*;
2
3use rustc_middle::ty;
4
5/// Reflects [`ty::VariantDiscr`]
6#[derive(Debug, Clone, AdtInto)]
7#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::VariantDiscr, state: S as gstate)]
8pub enum DiscriminantDefinition {
9    Explicit(DefId),
10    Relative(u32),
11}
12
13/// Reflects [`ty::util::Discr`]
14#[derive(Debug, Clone, AdtInto)]
15#[args(< S: UnderOwnerState<'tcx>>, from: ty::util::Discr<'tcx>, state: S as gstate)]
16pub struct DiscriminantValue<'tcx> {
17    pub val: u128,
18    pub ty: Ty<'tcx>,
19}
20
21/// Reflects [`ty::Visibility`]
22#[derive(Debug, Clone)]
23pub enum Visibility<Id> {
24    Public,
25    Restricted(Id),
26}
27
28impl<S, T: SInto<S, U>, U> SInto<S, Visibility<U>> for ty::Visibility<T> {
29    fn sinto(&self, s: &S) -> Visibility<U> {
30        use ty::Visibility as T;
31        match self {
32            T::Public => Visibility::Public,
33            T::Restricted(id) => Visibility::Restricted(id.sinto(s)),
34        }
35    }
36}
37
38/// Reflects [`ty::FieldDef`]
39#[derive(Debug, Clone)]
40pub struct FieldDef<'tcx> {
41    pub did: DefId,
42    /// Field definition of [tuple
43    /// structs](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types)
44    /// are anonymous, in that case `name` is [`None`].
45    pub name: Option<Symbol>,
46    pub vis: Visibility<DefId>,
47    pub ty: Ty<'tcx>,
48    pub span: Span,
49}
50
51impl<'tcx> FieldDef<'tcx> {
52    pub fn sfrom<S: UnderOwnerState<'tcx>>(
53        s: &S,
54        fdef: &ty::FieldDef,
55        instantiate: ty::GenericArgsRef<'tcx>,
56    ) -> FieldDef<'tcx> {
57        let tcx = s.base().tcx;
58        let ty = normalize(tcx, s.typing_env(), fdef.ty(tcx, instantiate)).sinto(s);
59        let name = {
60            let name = fdef.name.sinto(s);
61            let is_user_provided = {
62                // SH: Note that the only way I found of checking if the user wrote the name or if it
63                // is just an integer generated by rustc is by checking if it is just made of
64                // numerals...
65                name.to_string().parse::<usize>().is_err()
66            };
67            is_user_provided.then_some(name)
68        };
69
70        FieldDef {
71            did: fdef.did.sinto(s),
72            name,
73            vis: fdef.vis.map_id(|mod_id| mod_id.to_def_id()).sinto(s),
74            ty,
75            span: tcx.def_span(fdef.did).sinto(s),
76        }
77    }
78}
79
80/// Reflects [`ty::VariantDef`]
81#[derive(Debug, Clone)]
82pub struct VariantDef<'tcx> {
83    pub def_id: DefId,
84    pub ctor: Option<(CtorKind, DefId)>,
85    pub name: Symbol,
86    pub discr_def: DiscriminantDefinition,
87    pub discr_val: DiscriminantValue<'tcx>,
88    /// The definitions of the fields on this variant. In case of [tuple
89    /// structs/variants](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types),
90    /// the fields are anonymous, otherwise fields are named.
91    pub fields: IndexVec<FieldIdx, FieldDef<'tcx>>,
92    /// Span of the definition of the variant
93    pub span: Span,
94}
95
96impl<'tcx> VariantDef<'tcx> {
97    pub(crate) fn sfrom<S: UnderOwnerState<'tcx>>(
98        s: &S,
99        def: &ty::VariantDef,
100        discr_val: ty::util::Discr<'tcx>,
101        instantiate: Option<ty::GenericArgsRef<'tcx>>,
102    ) -> Self {
103        let def_id = def.def_id.sinto(s);
104        let instantiate = instantiate.unwrap_or_else(|| def_id.identity_args(s));
105        VariantDef {
106            def_id,
107            ctor: def.ctor.sinto(s),
108            name: def.name.sinto(s),
109            discr_def: def.discr.sinto(s),
110            discr_val: discr_val.sinto(s),
111            fields: def
112                .fields
113                .iter()
114                .map(|f| FieldDef::sfrom(s, f, instantiate))
115                .collect(),
116            span: s.base().tcx.def_span(def.def_id).sinto(s),
117        }
118    }
119}
120
121/// Reflects [`ty::AdtKind`]
122#[derive(Debug, Copy, Clone)]
123pub enum AdtKind {
124    Struct,
125    Union,
126    Enum,
127    /// We sometimes pretend arrays are an ADT and generate a `FullDef` for them.
128    Array,
129    /// We sometimes pretend slices are an ADT and generate a `FullDef` for them.
130    Slice,
131    /// Tuples get a type declaration of their own, we always generate a `FullDef` for them.
132    Tuple,
133    /// `str` gets a type declaration of its own, we always generate a `FullDef` for it.
134    Str,
135}
136
137impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, AdtKind> for ty::AdtKind {
138    fn sinto(&self, _s: &S) -> AdtKind {
139        match self {
140            ty::AdtKind::Struct => AdtKind::Struct,
141            ty::AdtKind::Union => AdtKind::Union,
142            ty::AdtKind::Enum => AdtKind::Enum,
143        }
144    }
145}
146
147/// Reflects [`rustc_abi::ReprOptions`].
148#[derive(Debug, Clone, AdtInto)]
149#[args(< S: UnderOwnerState<'tcx>>, from: rustc_abi::ReprOptions, state: S as s)]
150pub struct ReprOptions<'tcx> {
151    /// Whether an explicit integer representation was specified.
152    #[value(self.int.is_some())]
153    pub int_specified: bool,
154    /// The actual discriminant type resulting from the representation options.
155    #[value({
156        use rustc_middle::ty::util::IntTypeExt;
157        self.discr_type().to_ty(s.base().tcx).sinto(s)
158    })]
159    pub typ: Ty<'tcx>,
160    pub align: Option<Align>,
161    pub pack: Option<Align>,
162    #[value(ReprFlags { is_c: self.c(), is_transparent: self.transparent(), is_simd: self.simd() })]
163    pub flags: ReprFlags,
164}
165
166/// The representation flags without the ones irrelevant outside of rustc.
167#[derive(Debug, Default, Clone)]
168pub struct ReprFlags {
169    pub is_c: bool,
170    pub is_transparent: bool,
171    pub is_simd: bool,
172}
173
174/// Reflects [`rustc_abi::Align`]. We store the exponent of the alignment.
175#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
176#[derive(AdtInto)]
177#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_abi::Align, state: S as _s)]
178pub struct Align {
179    /// The real alignment is `1 << (pow2_plus_one - 1)`. We store `pow2 + 1` to have a niche.
180    #[value({
181           std::num::NonZeroU8::new(self.bytes().trailing_zeros() as u8 + 1).unwrap()
182        })]
183    pow2_plus_one: std::num::NonZeroU8,
184}
185
186impl Align {
187    /// The alignment in bytes.
188    pub fn bytes(self) -> u64 {
189        1 << (self.pow2_plus_one.get() - 1)
190    }
191}
charon_driver/hax/types/adt.rs

charon_driver/hax/types/
adt.rs
