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

charon_lib/ast/items/
type_decl.rs
