charon_lib/ast/
types.rs

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

charon_lib/ast/
types.rs
