charon_lib/ast/
types.rs

1use crate::ast::*;
2use crate::ids::{IndexMap, IndexVec};
3use derive_generic_visitor::*;
4use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
5use serde::{Deserialize, Serialize};
6use serde_state::{DeserializeState, SerializeState};
7
8mod vars;
9pub use vars::*;
10
11#[derive(
12    Debug,
13    PartialEq,
14    Eq,
15    Copy,
16    Clone,
17    Hash,
18    PartialOrd,
19    Ord,
20    EnumIsA,
21    EnumAsGetters,
22    SerializeState,
23    DeserializeState,
24    Drive,
25    DriveMut,
26)]
27#[charon::variants_prefix("R")]
28pub enum Region {
29    /// Region variable. See `DeBruijnVar` for details.
30    Var(RegionDbVar),
31    /// Static region
32    Static,
33    /// Body-local region, considered existentially-bound at the level of a body.
34    Body(RegionId),
35    /// Erased region
36    Erased,
37}
38
39/// Identifier of a trait instance.
40/// This is derived from the trait resolution.
41///
42/// Should be read as a path inside the trait clauses which apply to the current
43/// definition. Note that every path designated by `TraitInstanceId` refers
44/// to a *trait instance*, which is why the [`TraitRefKind::Clause`] variant may seem redundant
45/// with some of the other variants.
46#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
47pub enum TraitRefKind {
48    /// A specific top-level implementation item.
49    TraitImpl(TraitImplRef),
50
51    /// One of the local clauses.
52    ///
53    /// Example:
54    /// ```text
55    /// fn f<T>(...) where T : Foo
56    ///                    ^^^^^^^
57    ///                    Clause(0)
58    /// ```
59    Clause(ClauseDbVar),
60
61    /// A parent clause
62    ///
63    /// Example:
64    /// ```text
65    /// trait Foo1 {}
66    /// trait Foo2 { fn f(); }
67    ///
68    /// trait Bar : Foo1 + Foo2 {}
69    ///             ^^^^   ^^^^
70    ///                    parent clause 1
71    ///     parent clause 0
72    ///
73    /// fn g<T : Bar>(x : T) {
74    ///   x.f()
75    ///   ^^^^^
76    ///   Parent(Clause(0), 1)::f(x)
77    ///                     ^
78    ///                     parent clause 1 of clause 0
79    /// }
80    /// ```
81    ParentClause(Box<TraitRef>, TraitClauseId),
82
83    /// A clause defined on an associated type. This variant is only used during translation; after
84    /// the `lift_associated_item_clauses` pass, clauses on items become `ParentClause`s.
85    ///
86    /// Example:
87    /// ```text
88    /// trait Foo {
89    ///   type W: Bar0 + Bar1 // Bar1 contains a method bar1
90    ///                  ^^^^
91    ///               this is the clause 1 applying to W
92    /// }
93    ///
94    /// fn f<T : Foo>(x : T::W) {
95    ///   x.bar1();
96    ///   ^^^^^^^
97    ///   ItemClause(Clause(0), W, 1)
98    ///                         ^^^^
99    ///                         clause 1 from item W (from local clause 0)
100    /// }
101    /// ```
102    ItemClause(Box<TraitRef>, TraitItemName, TraitClauseId),
103
104    /// The implicit `Self: Trait` clause. Present inside trait declarations, including trait
105    /// method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
106    #[charon::rename("Self")]
107    SelfId,
108
109    /// A trait implementation that is computed by the compiler, such as for built-in trait
110    /// `Sized`. This morally points to an invisible `impl` block; as such it contains
111    /// the information we may need from one.
112    BuiltinOrAuto {
113        #[drive(skip)]
114        builtin_data: BuiltinImplData,
115        /// Exactly like the same field on `TraitImpl`: the `TraitRef`s required to satisfy the
116        /// implied predicates on the trait declaration. E.g. since `FnMut: FnOnce`, a built-in `T:
117        /// FnMut` impl would have a `TraitRef` for `T: FnOnce`.
118        parent_trait_refs: IndexMap<TraitClauseId, TraitRef>,
119        /// The values of the associated types for this trait.
120        types: Vec<(TraitItemName, TraitAssocTyImpl)>,
121    },
122
123    /// The automatically-generated implementation for `dyn Trait`.
124    Dyn,
125
126    /// For error reporting.
127    #[charon::rename("UnknownTrait")]
128    #[drive(skip)]
129    Unknown(String),
130}
131
132/// Describes a built-in impl. Mostly lists the implemented trait, sometimes with more details
133/// about the contents of the implementation.
134#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
135#[charon::variants_prefix("Builtin")]
136pub enum BuiltinImplData {
137    // Marker traits (without methods).
138    Sized,
139    MetaSized,
140    Tuple,
141    Pointee,
142    DiscriminantKind,
143    // Auto traits (defined with `auto trait ...`).
144    Auto,
145
146    // Traits with methods.
147    /// An impl of `Destruct` for a type with no drop glue.
148    NoopDestruct,
149    /// An impl of `Destruct` for a type parameter, which we could not resolve because
150    /// `--add-drop-bounds` was not set.
151    UntrackedDestruct,
152    Fn,
153    FnMut,
154    FnOnce,
155    Copy,
156    Clone,
157}
158
159/// A reference to a trait.
160///
161/// This type is hash-consed, `TraitRefContents` contains the actual data.
162#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
163#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
164pub struct TraitRef(pub HashConsed<TraitRefContents>);
165
166#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
167pub struct TraitRefContents {
168    pub kind: TraitRefKind,
169    /// Not necessary, but useful
170    pub trait_decl_ref: PolyTraitDeclRef,
171}
172
173/// A predicate of the form `Type: Trait<Args>`.
174///
175/// About the generics, if we write:
176/// ```text
177/// impl Foo<bool> for String { ... }
178/// ```
179///
180/// The substitution is: `[String, bool]`.
181#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
182pub struct TraitDeclRef {
183    pub id: TraitDeclId,
184    pub generics: BoxedArgs,
185}
186
187/// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
188pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
189
190/// A reference to a tait impl, using the provided arguments.
191#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
192pub struct TraitImplRef {
193    pub id: TraitImplId,
194    pub generics: BoxedArgs,
195}
196
197/// .0 outlives .1
198#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
199pub struct OutlivesPred<T, U>(pub T, pub U);
200
201pub type RegionOutlives = OutlivesPred<Region, Region>;
202pub type TypeOutlives = OutlivesPred<Ty, Region>;
203
204/// A constraint over a trait associated type.
205///
206/// Example:
207/// ```text
208/// T : Foo<S = String>
209///         ^^^^^^^^^^
210/// ```
211#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
212pub struct TraitTypeConstraint {
213    pub trait_ref: TraitRef,
214    pub type_name: TraitItemName,
215    pub ty: Ty,
216}
217
218/// A set of generic arguments.
219#[derive(Clone, Eq, PartialEq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
220pub struct GenericArgs {
221    pub regions: IndexMap<RegionId, Region>,
222    pub types: IndexMap<TypeVarId, Ty>,
223    pub const_generics: IndexMap<ConstGenericVarId, ConstantExpr>,
224    // TODO: rename to match [GenericParams]?
225    pub trait_refs: IndexMap<TraitClauseId, TraitRef>,
226}
227
228pub type BoxedArgs = Box<GenericArgs>;
229
230/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
231/// issues in the derived ocaml visitors.
232#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
233pub struct RegionBinder<T> {
234    #[charon::rename("binder_regions")]
235    #[serde_state(stateless)]
236    pub regions: IndexMap<RegionId, RegionParam>,
237    /// Named this way to highlight accesses to the inner value that might be handling parameters
238    /// incorrectly. Prefer using helper methods.
239    #[charon::rename("binder_value")]
240    pub skip_binder: T,
241}
242
243#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
244#[charon::variants_prefix("BK")]
245pub enum BinderKind {
246    /// The parameters of a generic associated type.
247    TraitType(TraitDeclId, TraitItemName),
248    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
249    /// impls.
250    TraitMethod(TraitDeclId, TraitItemName),
251    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
252    InherentImplBlock,
253    /// Binder used for `dyn Trait` existential predicates.
254    Dyn,
255    /// Some other use of a binder outside the main Charon ast.
256    Other,
257}
258
259/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
260/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
261/// now), trait methods, GATs (TODO).
262#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
263pub struct Binder<T> {
264    #[charon::rename("binder_params")]
265    pub params: GenericParams,
266    /// Named this way to highlight accesses to the inner value that might be handling parameters
267    /// incorrectly. Prefer using helper methods.
268    #[charon::rename("binder_value")]
269    pub skip_binder: T,
270    /// The kind of binder this is.
271    #[charon::opaque]
272    #[drive(skip)]
273    pub kind: BinderKind,
274}
275
276/// Generic parameters for a declaration.
277/// We group the generics which come from the Rust compiler substitutions
278/// (the regions, types and const generics) as well as the trait clauses.
279/// The reason is that we consider that those are parameters that need to
280/// be filled. We group in a different place the predicates which are not
281/// trait clauses, because those enforce constraints but do not need to
282/// be filled with witnesses/instances.
283// FIXME: we use `IndexMap` instead of `IndexVec` because the `remove_marker_traits` pass would
284// otherwise need to renumber clauses across the whole crate and that was too painful.
285#[derive(
286    Default, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut,
287)]
288pub struct GenericParams {
289    #[serde_state(stateless)]
290    pub regions: IndexMap<RegionId, RegionParam>,
291    #[serde_state(stateless)]
292    pub types: IndexMap<TypeVarId, TypeParam>,
293    pub const_generics: IndexMap<ConstGenericVarId, ConstGenericParam>,
294    // TODO: rename to match [GenericArgs]?
295    pub trait_clauses: IndexMap<TraitClauseId, TraitParam>,
296    /// The first region in the pair outlives the second region
297    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
298    /// The type outlives the region
299    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
300    /// Constraints over trait associated types
301    pub trait_type_constraints: IndexMap<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
302}
303
304/// Where a given predicate came from.
305#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
306pub enum PredicateOrigin {
307    // Note: we use this for globals too, but that's only available with an unstable feature.
308    // ```
309    // fn function<T: Clone>() {}
310    // fn function<T>() where T: Clone {}
311    // const NONE<T: Copy>: Option<T> = None;
312    // ```
313    WhereClauseOnFn,
314    // ```
315    // struct Struct<T: Clone> {}
316    // struct Struct<T> where T: Clone {}
317    // type TypeAlias<T: Clone> = ...;
318    // ```
319    WhereClauseOnType,
320    // Note: this is both trait impls and inherent impl blocks.
321    // ```
322    // impl<T: Clone> Type<T> {}
323    // impl<T> Type<T> where T: Clone {}
324    // impl<T> Trait for Type<T> where T: Clone {}
325    // ```
326    WhereClauseOnImpl,
327    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
328    // implementation of it.
329    // ```
330    // trait Trait {}
331    // ```
332    TraitSelf,
333    // Note: this also includes supertrait constraints.
334    // ```
335    // trait Trait<T: Clone> {}
336    // trait Trait<T> where T: Clone {}
337    // trait Trait: Clone {}
338    // ```
339    WhereClauseOnTrait,
340    // ```
341    // trait Trait {
342    //     type AssocType: Clone;
343    // }
344    // ```
345    TraitItem(TraitItemName),
346    /// Clauses that are part of a `dyn Trait` type.
347    Dyn,
348}
349
350// rustc counts bytes in layouts as u64
351pub type ByteCount = u64;
352
353/// Simplified layout of a single variant.
354///
355/// Maps fields to their offset within the layout.
356#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
357pub struct VariantLayout {
358    /// The offset of each field.
359    #[drive(skip)]
360    pub field_offsets: IndexVec<FieldId, ByteCount>,
361    /// Whether the variant is uninhabited, i.e. has any valid possible value.
362    /// Note that uninhabited types can have arbitrary layouts.
363    #[drive(skip)]
364    pub uninhabited: bool,
365    /// The memory representation of the discriminant corresponding to this
366    /// variant. It must be of the same type as the corresponding [`DiscriminantLayout::tag_ty`].
367    ///
368    /// If it's `None`, then this variant is either:
369    /// - the untagged variant (cf. [`TagEncoding::Niche::untagged_variant`]) of a niched enum;
370    /// - the single variant of a struct;
371    /// - uninhabited.
372    #[drive(skip)]
373    pub tag: Option<ScalarValue>,
374}
375
376/// Describes how we represent the active enum variant in memory.
377#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
378pub enum TagEncoding {
379    /// Represents the direct encoding of the discriminant as the tag via integer casts.
380    Direct,
381    /// Represents the encoding of the discriminant in the niche of variant `untagged_variant`.
382    Niche { untagged_variant: VariantId },
383}
384
385/// Layout of the discriminant.
386/// Describes the offset of the discriminant field as well as its encoding
387/// as `tag` in memory.
388#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
389pub struct DiscriminantLayout {
390    /// The offset of the discriminant in bytes.
391    pub offset: ByteCount,
392    /// The representation type of the discriminant.
393    pub tag_ty: IntegerTy,
394    /// How the tag is encoding in memory.
395    pub encoding: TagEncoding,
396    // FIXME: Should probably contain the valid range of the tag, too.
397}
398
399/// Simplified type layout information.
400///
401/// Does not include information about niches.
402/// If the type does not have a fully known layout (e.g. it is ?Sized)
403/// some of the layout parts are not available.
404#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
405pub struct Layout {
406    /// The size of the type in bytes.
407    #[drive(skip)]
408    pub size: Option<ByteCount>,
409    /// The alignment, in bytes.
410    #[drive(skip)]
411    pub align: Option<ByteCount>,
412    /// The discriminant's layout, if any. Only relevant for types with multiple variants.
413    #[drive(skip)]
414    pub discriminant_layout: Option<DiscriminantLayout>,
415    /// Whether the type is uninhabited, i.e. has any valid value at all.
416    /// Note that uninhabited types can have arbitrary layouts: `(u32, !)` has space for the `u32`
417    /// and `enum E2 { A, B(!), C(i32, !) }` may have space for a discriminant.
418    #[drive(skip)]
419    pub uninhabited: bool,
420    /// Map from `VariantId` to the corresponding field layouts. Structs are modeled as having
421    /// exactly one variant, unions as having no variant.
422    pub variant_layouts: IndexVec<VariantId, VariantLayout>,
423}
424
425/// The metadata stored in a pointer. That's the information stored in pointers alongside
426/// their address. It's empty for `Sized` types, and interesting for unsized
427/// aka dynamically-sized types.
428#[derive(Debug, Clone, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut, Hash)]
429#[serde_state(default_state = ())]
430pub enum PtrMetadata {
431    /// Types that need no metadata, namely `T: Sized` types.
432    #[charon::rename("NoMetadata")]
433    None,
434    /// Metadata for `[T]` and `str`, and user-defined types
435    /// that directly or indirectly contain one of the two.
436    /// Of type `usize`.
437    /// Notably, length for `[T]` denotes the number of elements in the slice.
438    /// While for `str` it denotes the number of bytes in the string.
439    Length,
440    /// Metadata for `dyn Trait`, referring to the vtable struct,
441    /// also for user-defined types that directly or indirectly contain a `dyn Trait`.
442    /// Of type `&'static vtable`
443    VTable(TypeDeclRef),
444    /// Unknown due to generics, but will inherit from the given type.
445    /// This is consistent with `<Ty as Pointee>::Metadata`.
446    /// Of type `TyKind::Metadata(Ty)`.
447    InheritFrom(Ty),
448}
449
450/// Describes which layout algorithm is used for representing the corresponding type.
451/// Depends on the `#[repr(...)]` used.
452#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
453pub enum ReprAlgorithm {
454    /// The default layout algorithm. Used without an explicit `ŗepr` or for `repr(Rust)`.
455    Rust,
456    /// The C layout algorithm as enforced by `repr(C)`.
457    C,
458}
459
460/// Describes modifiers to the alignment and packing of the corresponding type.
461/// Represents `repr(align(n))` and `repr(packed(n))`.
462#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
463pub enum AlignmentModifier {
464    Align(ByteCount),
465    Pack(ByteCount),
466}
467
468/// The representation options as annotated by the user.
469///
470/// NOTE: This does not include less common/unstable representations such as `#[repr(simd)]`
471/// or the compiler internal `#[repr(linear)]`. Similarly, enum discriminant representations
472/// are encoded in [`Variant::discriminant`] and [`DiscriminantLayout`] instead.
473/// This only stores whether the discriminant type was derived from an explicit annotation.
474#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
475pub struct ReprOptions {
476    pub repr_algo: ReprAlgorithm,
477    pub align_modif: Option<AlignmentModifier>,
478    pub transparent: bool,
479    pub explicit_discr_type: bool,
480}
481
482/// A type declaration.
483///
484/// Types can be opaque or transparent.
485///
486/// Transparent types are local types not marked as opaque.
487/// Opaque types are the others: local types marked as opaque, and non-local
488/// types (coming from external dependencies).
489///
490/// In case the type is transparent, the declaration also contains the
491/// type definition (see [TypeDeclKind]).
492///
493/// A type can only be an ADT (structure or enumeration), as type aliases are
494/// inlined in MIR.
495#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
496pub struct TypeDecl {
497    #[drive(skip)]
498    pub def_id: TypeDeclId,
499    /// Meta information associated with the item.
500    pub item_meta: ItemMeta,
501    pub generics: GenericParams,
502    /// The context of the type: distinguishes top-level items from closure-related items.
503    pub src: ItemSource,
504    /// The type kind: enum, struct, or opaque.
505    pub kind: TypeDeclKind,
506    /// The layout of the type. Information may be partial because of generics or dynamically-
507    /// sized types. If rustc cannot compute a layout, it is `None`.
508    #[serde_state(stateless)]
509    pub layout: Option<Layout>,
510    /// The metadata associated with a pointer to the type.
511    pub ptr_metadata: PtrMetadata,
512    /// The representation options of this type declaration as annotated by the user.
513    /// Is `None` for foreign type declarations.
514    #[drive(skip)]
515    #[serde_state(stateless)]
516    pub repr: Option<ReprOptions>,
517}
518
519generate_index_type!(VariantId, "Variant");
520generate_index_type!(FieldId, "Field");
521
522#[derive(
523    Debug, Clone, EnumIsA, EnumAsGetters, SerializeState, DeserializeState, Drive, DriveMut,
524)]
525pub enum TypeDeclKind {
526    Struct(IndexVec<FieldId, Field>),
527    Enum(IndexVec<VariantId, Variant>),
528    Union(IndexVec<FieldId, Field>),
529    /// An opaque type.
530    ///
531    /// Either a local type marked as opaque, or an external type.
532    Opaque,
533    /// An alias to another type. This only shows up in the top-level list of items, as rustc
534    /// inlines uses of type aliases everywhere else.
535    Alias(Ty),
536    /// Used if an error happened during the extraction, and we don't panic
537    /// on error.
538    #[charon::rename("TDeclError")]
539    #[drive(skip)]
540    Error(String),
541}
542
543#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
544#[serde_state(stateless)]
545pub struct Variant {
546    pub span: Span,
547    #[drive(skip)]
548    pub attr_info: AttrInfo,
549    #[charon::rename("variant_name")]
550    #[drive(skip)]
551    pub name: String,
552    #[serde_state(stateful)]
553    pub fields: IndexVec<FieldId, Field>,
554    /// The discriminant value outputted by `std::mem::discriminant` for this variant. This can be
555    /// different than the value stored in memory (called `tag`). That one is described by
556    /// [`DiscriminantLayout`] and [`TagEncoding`].
557    pub discriminant: Literal,
558}
559
560#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
561#[serde_state(stateless)]
562pub struct Field {
563    pub span: Span,
564    #[drive(skip)]
565    pub attr_info: AttrInfo,
566    #[charon::rename("field_name")]
567    #[drive(skip)]
568    pub name: Option<String>,
569    #[charon::rename("field_ty")]
570    #[serde_state(stateful)]
571    pub ty: Ty,
572}
573
574#[derive(
575    Debug,
576    PartialEq,
577    Eq,
578    Copy,
579    Clone,
580    EnumIsA,
581    VariantName,
582    Serialize,
583    Deserialize,
584    Drive,
585    DriveMut,
586    Hash,
587    Ord,
588    PartialOrd,
589)]
590pub enum IntTy {
591    Isize,
592    I8,
593    I16,
594    I32,
595    I64,
596    I128,
597}
598
599#[derive(
600    Debug,
601    PartialEq,
602    Eq,
603    Copy,
604    Clone,
605    EnumIsA,
606    VariantName,
607    Serialize,
608    Deserialize,
609    Drive,
610    DriveMut,
611    Hash,
612    Ord,
613    PartialOrd,
614)]
615pub enum UIntTy {
616    Usize,
617    U8,
618    U16,
619    U32,
620    U64,
621    U128,
622}
623
624#[derive(
625    Debug,
626    PartialEq,
627    Eq,
628    Copy,
629    Clone,
630    EnumIsA,
631    VariantName,
632    Serialize,
633    Deserialize,
634    Drive,
635    DriveMut,
636    Hash,
637    Ord,
638    PartialOrd,
639)]
640#[charon::rename("IntegerType")]
641pub enum IntegerTy {
642    Signed(IntTy),
643    Unsigned(UIntTy),
644}
645
646#[derive(
647    Debug,
648    PartialEq,
649    Eq,
650    Copy,
651    Clone,
652    EnumIsA,
653    VariantName,
654    Serialize,
655    Deserialize,
656    Drive,
657    DriveMut,
658    Hash,
659    Ord,
660    PartialOrd,
661)]
662#[charon::rename("FloatType")]
663pub enum FloatTy {
664    F16,
665    F32,
666    F64,
667    F128,
668}
669
670#[derive(
671    Debug,
672    PartialEq,
673    Eq,
674    Clone,
675    Copy,
676    Hash,
677    VariantName,
678    EnumIsA,
679    Serialize,
680    Deserialize,
681    SerializeState,
682    DeserializeState,
683    Drive,
684    DriveMut,
685    Ord,
686    PartialOrd,
687)]
688#[charon::variants_prefix("R")]
689#[serde_state(stateless)]
690pub enum RefKind {
691    Mut,
692    Shared,
693}
694
695/// The nature of locations where a given lifetime parameter is used. If this lifetime ever flows
696/// to be used as the lifetime of a mutable reference `&'a mut` then we consider it mutable.
697#[derive(
698    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, EnumIsA,
699)]
700#[charon::variants_prefix("Lt")]
701pub enum LifetimeMutability {
702    /// A lifetime that is used for a mutable reference.
703    Mutable,
704    /// A lifetime used only in shared references.
705    Shared,
706    /// A lifetime for which we couldn't/didn't compute mutability.
707    Unknown,
708}
709
710/// Type identifier.
711///
712/// Allows us to factorize the code for built-in types, adts and tuples
713#[derive(
714    Debug,
715    PartialEq,
716    Eq,
717    Clone,
718    Copy,
719    VariantName,
720    EnumAsGetters,
721    EnumIsA,
722    SerializeState,
723    DeserializeState,
724    Drive,
725    DriveMut,
726    Hash,
727    Ord,
728    PartialOrd,
729)]
730#[charon::variants_prefix("T")]
731pub enum TypeId {
732    /// A "regular" ADT type.
733    ///
734    /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
735    /// and external ADTs).
736    #[charon::rename("TAdtId")]
737    Adt(TypeDeclId),
738    Tuple,
739    /// Built-in type. Either a primitive type like array or slice, or a
740    /// non-primitive type coming from a standard library
741    /// and that we handle like a primitive type. Types falling into this
742    /// category include: Box, Vec, Cell...
743    /// The Array and Slice types were initially modelled as primitive in
744    /// the [Ty] type. We decided to move them to built-in types as it allows
745    /// for more uniform treatment throughout the codebase.
746    #[charon::rename("TBuiltin")]
747    #[serde_state(stateless)]
748    Builtin(BuiltinTy),
749}
750
751/// Reference to a type declaration or builtin type.
752#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
753pub struct TypeDeclRef {
754    pub id: TypeId,
755    pub generics: BoxedArgs,
756}
757
758/// Types of primitive values. Either an integer, bool, char
759#[derive(
760    Debug,
761    PartialEq,
762    Eq,
763    Clone,
764    Copy,
765    VariantName,
766    EnumIsA,
767    EnumAsGetters,
768    VariantIndexArity,
769    Serialize,
770    Deserialize,
771    SerializeState,
772    DeserializeState,
773    Drive,
774    DriveMut,
775    Hash,
776    Ord,
777    PartialOrd,
778)]
779#[charon::rename("LiteralType")]
780#[charon::variants_prefix("T")]
781#[serde_state(stateless)]
782pub enum LiteralTy {
783    Int(IntTy),
784    UInt(UIntTy),
785    Float(FloatTy),
786    Bool,
787    Char,
788}
789
790/// A type.
791///
792/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
793/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
794#[derive(Debug, Clone, Hash, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut)]
795#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
796pub struct Ty(pub HashConsed<TyKind>);
797
798#[derive(
799    Debug,
800    Clone,
801    PartialEq,
802    Eq,
803    Hash,
804    VariantName,
805    EnumIsA,
806    EnumAsGetters,
807    EnumToGetters,
808    VariantIndexArity,
809    SerializeState,
810    DeserializeState,
811    Drive,
812    DriveMut,
813)]
814#[charon::variants_prefix("T")]
815pub enum TyKind {
816    /// An ADT.
817    /// Note that here ADTs are very general. They can be:
818    /// - user-defined ADTs
819    /// - tuples (including `unit`, which is a 0-tuple)
820    /// - built-in types (includes some primitive types, e.g., arrays or slices)
821    /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
822    /// The last list is used encode const generics, e.g., the size of an array
823    ///
824    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
825    /// types.
826    Adt(TypeDeclRef),
827    #[charon::rename("TVar")]
828    TypeVar(TypeDbVar),
829    Literal(LiteralTy),
830    /// The never type, for computations which don't return. It is sometimes
831    /// necessary for intermediate variables. For instance, if we do (coming
832    /// from the rust documentation):
833    /// ```text
834    /// let num: u32 = match get_a_number() {
835    ///     Some(num) => num,
836    ///     None => break,
837    /// };
838    /// ```
839    /// the second branch will have type `Never`. Also note that `Never`
840    /// can be coerced to any type.
841    ///
842    /// Note that we eliminate the variables which have this type in a micro-pass.
843    /// As statements don't have types, this type disappears eventually disappears
844    /// from the AST.
845    Never,
846    // We don't support floating point numbers on purpose (for now)
847    /// A borrow
848    Ref(Region, Ty, RefKind),
849    /// A raw pointer.
850    RawPtr(Ty, RefKind),
851    /// A trait associated type
852    ///
853    /// Ex.:
854    /// ```text
855    /// trait Foo {
856    ///   type Bar; // type associated to the trait Foo
857    /// }
858    /// ```
859    TraitType(TraitRef, TraitItemName),
860    /// `dyn Trait`
861    DynTrait(DynPredicate),
862    /// Function pointer type. This is a literal pointer to a region of memory that
863    /// contains a callable function.
864    /// This is a function signature with limited generics: it only supports lifetime generics, not
865    /// other kinds of generics.
866    FnPtr(RegionBinder<FunSig>),
867    /// The unique type associated with each function item. Each function item is given
868    /// a unique generic type that takes as input the function's early-bound generics. This type
869    /// is not generally nameable in Rust; it's a ZST (there's a unique value), and a value of that type
870    /// can be cast to a function pointer or passed to functions that expect `FnOnce`/`FnMut`/`Fn` parameters.
871    /// There's a binder here because charon function items take both early and late-bound
872    /// lifetimes as arguments; given that the type here is polymorpohic in the late-bound
873    /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`),
874    /// we need to bind them here.
875    FnDef(RegionBinder<FnPtr>),
876    /// As a marker of taking out metadata from a given type
877    /// The internal type is assumed to be a type variable
878    PtrMetadata(Ty),
879    /// An array type `[T; N]`
880    Array(Ty, Box<ConstantExpr>),
881    /// A slice type `[T]`
882    Slice(Ty),
883    /// A type that could not be computed or was incorrect.
884    #[drive(skip)]
885    Error(String),
886}
887
888/// Builtin types identifiers.
889///
890/// WARNING: for now, all the built-in types are covariant in the generic
891/// parameters (if there are). Adding types which don't satisfy this
892/// will require to update the code abstracting the signatures (to properly
893/// take into account the lifetime constraints).
894///
895/// TODO: update to not hardcode the types (except `Box` maybe) and be more
896/// modular.
897/// TODO: move to builtins.rs?
898#[derive(
899    Debug,
900    PartialEq,
901    Eq,
902    Clone,
903    Copy,
904    EnumIsA,
905    EnumAsGetters,
906    VariantName,
907    Serialize,
908    Deserialize,
909    Drive,
910    DriveMut,
911    Hash,
912    Ord,
913    PartialOrd,
914)]
915#[charon::variants_prefix("T")]
916pub enum BuiltinTy {
917    /// Boxes are de facto a primitive type.
918    Box,
919    /// Primitive type
920    Str,
921}
922
923#[derive(
924    Debug,
925    Copy,
926    Clone,
927    PartialEq,
928    Eq,
929    PartialOrd,
930    Ord,
931    Hash,
932    Serialize,
933    Deserialize,
934    Drive,
935    DriveMut,
936)]
937pub enum ClosureKind {
938    Fn,
939    FnMut,
940    FnOnce,
941}
942
943impl ClosureKind {
944    // pub fn trait_name(self) -> &'static str {}
945    pub fn method_name(self) -> &'static str {
946        match self {
947            ClosureKind::FnOnce => "call_once",
948            ClosureKind::FnMut => "call_mut",
949            ClosureKind::Fn => "call",
950        }
951    }
952}
953
954/// Additional information for closures.
955#[derive(Debug, Clone, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut)]
956pub struct ClosureInfo {
957    #[serde_state(stateless)]
958    pub kind: ClosureKind,
959    /// The `FnOnce` implementation of this closure -- always exists.
960    pub fn_once_impl: RegionBinder<TraitImplRef>,
961    /// The `FnMut` implementation of this closure, if any.
962    pub fn_mut_impl: Option<RegionBinder<TraitImplRef>>,
963    /// The `Fn` implementation of this closure, if any.
964    pub fn_impl: Option<RegionBinder<TraitImplRef>>,
965    /// The signature of the function that this closure represents.
966    pub signature: RegionBinder<FunSig>,
967}
968
969/// A function signature.
970#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
971pub struct FunSig {
972    /// Is the function unsafe or not
973    #[drive(skip)]
974    pub is_unsafe: bool,
975    pub inputs: Vec<Ty>,
976    pub output: Ty,
977}
978
979/// The contents of a `dyn Trait` type.
980#[derive(Debug, Clone, Hash, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut)]
981pub struct DynPredicate {
982    /// This binder binds a single type `T`, which is considered existentially quantified. The
983    /// predicates in the binder apply to `T` and represent the `dyn Trait` constraints.
984    /// E.g. `dyn Iterator<Item=u32> + Send` is represented as `exists<T: Iterator<Item=u32> + Send> T`.
985    ///
986    /// Only the first trait clause may have methods. We use the vtable of this trait in the `dyn
987    /// Trait` pointer metadata.
988    pub binder: Binder<Ty>,
989}
charon_lib/ast/types.rs

charon_lib/ast/
types.rs
