charon_lib/ast/items/
type_decl.rs

1use derive_generic_visitor::*;
2use macros::{EnumAsGetters, EnumIsA};
3use serde::{Deserialize, Serialize};
4use serde_state::{DeserializeState, SerializeState};
5
6use crate::ast::*;
7use crate::ids::IndexVec;
8use crate::utils::serialize_map_to_array::SeqHashMapToArray;
9
10/// A type declaration.
11///
12/// Types can be opaque or transparent.
13///
14/// Transparent types are local types not marked as opaque.
15/// Opaque types are the others: local types marked as opaque, and non-local
16/// types (coming from external dependencies).
17///
18/// In case the type is transparent, the declaration also contains the
19/// type definition (see [TypeDeclKind]).
20///
21/// A type can only be an ADT (structure or enumeration), as type aliases are
22/// inlined in MIR.
23#[derive(
24    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
25)]
26#[serde_state(state_implements = HashConsSerializerState)]
27pub struct TypeDecl {
28    pub def_id: TypeDeclId,
29    /// Meta information associated with the item.
30    pub item_meta: ItemMeta,
31    pub generics: GenericParams,
32    /// The context of the type: distinguishes top-level items from closure-related items etc.
33    pub src: TypeSource,
34    /// The type kind: enum, struct, or opaque.
35    pub kind: TypeDeclKind,
36    /// The layout of the type for each target. Information may be partial because of generics or
37    /// dynamically-sized types. If we cannot compute a layout, the target has no entry.
38    #[serde(with = "SeqHashMapToArray::<TargetTriple, Layout>")]
39    pub layout: SeqHashMap<TargetTriple, Layout>,
40    /// The metadata associated with a pointer to the type.
41    pub ptr_metadata: PtrMetadata,
42}
43
44generate_index_type!(VariantId, "Variant");
45generate_index_type!(FieldId, "Field");
46
47#[derive(
48    Debug,
49    PartialEq,
50    Eq,
51    Clone,
52    EnumIsA,
53    EnumAsGetters,
54    SerializeState,
55    DeserializeState,
56    Drive,
57    DriveMut,
58    DriveTwo,
59)]
60pub enum TypeDeclKind {
61    Struct(IndexVec<FieldId, Field>),
62    Enum(IndexVec<VariantId, Variant>),
63    Union(IndexVec<FieldId, Field>),
64    /// An opaque type.
65    ///
66    /// Either a local type marked as opaque, or an external type.
67    Opaque,
68    /// An alias to another type. This only shows up in the top-level list of items, as rustc
69    /// inlines uses of type aliases everywhere else.
70    Alias(Ty),
71    /// Used if an error happened during the extraction, and we don't panic
72    /// on error.
73    #[cfg_attr(feature = "charon_on_charon", charon::rename("TDeclError"))]
74    #[drive(skip)]
75    Error(String),
76}
77
78#[derive(
79    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
80)]
81#[serde_state(stateless)]
82pub struct Variant {
83    pub id: VariantId,
84    pub span: Span,
85    pub attr_info: AttrInfo,
86    #[cfg_attr(feature = "charon_on_charon", charon::rename("variant_name"))]
87    #[drive(skip)]
88    pub name: String,
89    #[serde_state(stateful)]
90    pub fields: IndexVec<FieldId, Field>,
91    /// The discriminant value outputted by `std::mem::discriminant` for this variant. This can be
92    /// different than the value stored in memory (called `tag`); that one is described by
93    /// [`Discriminator`] and [`VariantLayout::tagger`].
94    pub discriminant: Literal,
95}
96
97#[derive(
98    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
99)]
100#[serde_state(stateless)]
101pub struct Field {
102    pub span: Span,
103    pub attr_info: AttrInfo,
104    #[cfg_attr(feature = "charon_on_charon", charon::rename("field_name"))]
105    #[drive(skip)]
106    pub name: String,
107    /// Whether this field is positional, as in a tuple struct, tuple variant, or closure. If so,
108    /// its name is based on its position, such as `_0`; otherwise, it is a user-provided name.
109    pub is_positional: bool,
110    #[cfg_attr(feature = "charon_on_charon", charon::rename("field_ty"))]
111    #[serde_state(stateful)]
112    pub ty: Ty,
113}
114
115/// The metadata stored in a pointer. That's the information stored in pointers alongside
116/// their address. It's empty for `Sized` types, and interesting for unsized
117/// aka dynamically-sized types.
118#[derive(
119    Debug,
120    Clone,
121    PartialEq,
122    Eq,
123    PartialOrd,
124    Ord,
125    Hash,
126    SerializeState,
127    DeserializeState,
128    Drive,
129    DriveMut,
130    DriveTwo,
131)]
132#[serde_state(default_state = ())]
133pub enum PtrMetadata {
134    /// Types that need no metadata, namely `T: Sized` types.
135    #[cfg_attr(feature = "charon_on_charon", charon::rename("NoMetadata"))]
136    None,
137    /// Metadata for `[T]` and `str`, and user-defined types
138    /// that directly or indirectly contain one of the two.
139    /// Of type `usize`.
140    /// Notably, length for `[T]` denotes the number of elements in the slice.
141    /// While for `str` it denotes the number of bytes in the string.
142    Length,
143    /// Metadata for `dyn Trait`, referring to the vtable struct. Has type `&'static vtable`
144    VTable(TypeDeclRef),
145    /// Unknown due to generics, but will inherit from the given type.
146    /// This is consistent with `<Ty as Pointee>::Metadata`.
147    /// Of type `TyKind::Metadata(Ty)`.
148    InheritFrom(Ty),
149}
150
151/// Where a given type came from.
152#[derive(
153    Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo, PartialEq, Eq,
154)]
155#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Type"))]
156pub enum TypeSource {
157    /// A normal type declaration.
158    Normal,
159    /// The struct that carries the captured variables of a closure.
160    Closure { info: ClosureInfo },
161    /// Defines the vtable struct for a trait.
162    VTable {
163        /// The `dyn Trait` predicate implemented by this vtable.
164        dyn_predicate: DynPredicate,
165        /// Record what each vtable field means.
166        field_map: IndexVec<FieldId, VTableField>,
167        /// For each implied clause that is also a supertrait clause, records which field of the
168        /// vtable corresponds to it.
169        supertrait_map: IndexVec<TraitClauseId, Option<FieldId>>,
170    },
171}
172
173#[derive(
174    Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo, PartialEq, Eq,
175)]
176#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("VTable"))]
177pub enum VTableField {
178    Size,
179    Align,
180    Drop,
181    Method(TraitMethodId),
182    SuperTrait(TraitClauseId),
183}
184
185/// Additional information for closures.
186#[derive(
187    Debug,
188    Clone,
189    PartialEq,
190    Eq,
191    PartialOrd,
192    Ord,
193    SerializeState,
194    DeserializeState,
195    Drive,
196    DriveMut,
197    DriveTwo,
198)]
199pub struct ClosureInfo {
200    #[serde_state(stateless)]
201    pub kind: ClosureKind,
202    /// The `FnOnce` implementation of this closure -- always exists.
203    pub fn_once_impl: RegionBinder<TraitImplRef>,
204    /// The `FnMut` implementation of this closure, if any.
205    pub fn_mut_impl: Option<RegionBinder<TraitImplRef>>,
206    /// The `Fn` implementation of this closure, if any.
207    pub fn_impl: Option<RegionBinder<TraitImplRef>>,
208    /// The signature of the function that this closure represents.
209    pub signature: RegionBinder<FunSig>,
210}
211
212#[derive(
213    Debug,
214    Copy,
215    Clone,
216    PartialEq,
217    Eq,
218    PartialOrd,
219    Ord,
220    Hash,
221    Serialize,
222    Deserialize,
223    Drive,
224    DriveMut,
225    DriveTwo,
226)]
227pub enum ClosureKind {
228    Fn,
229    FnMut,
230    FnOnce,
231}
232
233impl TypeDecl {
234    pub fn get_field(&self, variant: Option<VariantId>, field: FieldId) -> Option<&Field> {
235        let fields = match &self.kind {
236            TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields) => fields,
237            TypeDeclKind::Enum(variants) => &variants[variant.unwrap()].fields,
238            _ => return None,
239        };
240        fields.get(field)
241    }
242
243    pub fn get_field_by_name(
244        &self,
245        variant: Option<VariantId>,
246        field_name: &str,
247    ) -> Option<(FieldId, &Field)> {
248        let fields = match &self.kind {
249            TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields) => fields,
250            TypeDeclKind::Enum(variants) => &variants[variant.unwrap()].fields,
251            _ => return None,
252        };
253        fields
254            .iter_enumerated()
255            .find(|(_, field)| field.name == field_name)
256    }
257}
258
259impl Variant {
260    /// The new name for this variant, as suggested by the `#[charon::rename]` and
261    /// `#[charon::variants_prefix]` attributes.
262    pub fn renamed_name(&self) -> &str {
263        self.attr_info
264            .rename
265            .as_deref()
266            .unwrap_or(self.name.as_ref())
267    }
268
269    /// Whether this variant has a `#[charon::opaque]` annotation.
270    pub fn is_opaque(&self) -> bool {
271        self.attr_info
272            .attributes
273            .iter()
274            .any(|attr| attr.is_opaque())
275    }
276}
277
278impl Field {
279    /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
280    pub fn renamed_name(&self) -> &str {
281        self.attr_info.rename.as_deref().unwrap_or(&self.name)
282    }
283
284    /// Whether this field has a `#[charon::opaque]` annotation.
285    pub fn is_opaque(&self) -> bool {
286        self.attr_info
287            .attributes
288            .iter()
289            .any(|attr| attr.is_opaque())
290    }
291}
292
293impl ClosureKind {
294    // pub fn trait_name(self) -> &'static str {}
295    pub fn method_name(self) -> &'static str {
296        match self {
297            ClosureKind::FnOnce => "call_once",
298            ClosureKind::FnMut => "call_mut",
299            ClosureKind::Fn => "call",
300        }
301    }
302}
303
304impl PtrMetadata {
305    pub fn into_type(self) -> Ty {
306        match self {
307            PtrMetadata::None => Ty::mk_unit(),
308            PtrMetadata::Length => Ty::mk_usize(),
309            PtrMetadata::VTable(type_decl_ref) => Ty::new(TyKind::Ref(
310                Region::Static,
311                Ty::new(TyKind::Adt(type_decl_ref)),
312                RefKind::Shared,
313            )),
314            PtrMetadata::InheritFrom(ty) => Ty::new(TyKind::PtrMetadata(ty)),
315        }
316    }
317}
charon_lib/ast/items/type_decl.rs

charon_lib/ast/items/
type_decl.rs
