charon_lib/ast/type_level/
types.rs

1use crate::ast::*;
2use derive_generic_visitor::*;
3use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
4use serde::{Deserialize, Serialize};
5use serde_state::{DeserializeState, SerializeState};
6
7/// A type.
8///
9/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
10/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
11#[derive(
12    Debug,
13    Clone,
14    PartialEq,
15    Eq,
16    PartialOrd,
17    Ord,
18    Hash,
19    SerializeState,
20    DeserializeState,
21    Drive,
22    DriveMut,
23    DriveTwo,
24)]
25#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
26pub struct Ty(pub HashConsed<TyKind>);
27
28#[derive(
29    Debug,
30    Clone,
31    PartialEq,
32    Eq,
33    PartialOrd,
34    Ord,
35    Hash,
36    VariantName,
37    EnumIsA,
38    EnumAsGetters,
39    EnumToGetters,
40    VariantIndexArity,
41    SerializeState,
42    DeserializeState,
43    Drive,
44    DriveMut,
45    DriveTwo,
46)]
47#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
48pub enum TyKind {
49    /// An ADT.
50    /// Note that here ADTs are very general. They can be:
51    /// - user-defined ADTs
52    /// - tuples (including `unit`, which is a 0-tuple)
53    /// - built-in types (includes some primitive types, e.g., arrays or slices)
54    ///
55    /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
56    /// The last list is used encode const generics, e.g., the size of an array
57    ///
58    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
59    /// types.
60    Adt(TypeDeclRef),
61    #[cfg_attr(feature = "charon_on_charon", charon::rename("TVar"))]
62    TypeVar(TypeDbVar),
63    Literal(LiteralTy),
64    /// The never type, for computations which don't return. It is sometimes
65    /// necessary for intermediate variables. For instance, if we do (coming
66    /// from the rust documentation):
67    /// ```text
68    /// let num: u32 = match get_a_number() {
69    ///     Some(num) => num,
70    ///     None => break,
71    /// };
72    /// ```
73    /// the second branch will have type `Never`. Also note that `Never`
74    /// can be coerced to any type.
75    ///
76    /// Note that we eliminate the variables which have this type in a micro-pass.
77    /// As statements don't have types, this type disappears eventually disappears
78    /// from the AST.
79    Never,
80    // We don't support floating point numbers on purpose (for now)
81    /// A borrow
82    Ref(Region, Ty, RefKind),
83    /// A raw pointer.
84    RawPtr(Ty, RefKind),
85    /// A trait associated type
86    ///
87    /// Ex.:
88    /// ```text
89    /// trait Foo {
90    ///   type Bar; // type associated to the trait Foo
91    /// }
92    /// ```
93    TraitType(TraitRef, AssocTypeId, GenericArgs),
94    /// `dyn Trait`
95    DynTrait(DynPredicate),
96    /// Function pointer type. This is a literal pointer to a region of memory that
97    /// contains a callable function.
98    /// This is a function signature with limited generics: it only supports lifetime generics, not
99    /// other kinds of generics.
100    FnPtr(RegionBinder<FunSig>),
101    /// The unique type associated with each function item. Each function item is given
102    /// a unique generic type that takes as input the function's early-bound generics. This type
103    /// is not generally nameable in Rust; it's a ZST (there's a unique value), and a value of that type
104    /// can be cast to a function pointer or passed to functions that expect `FnOnce`/`FnMut`/`Fn` parameters.
105    /// There's a binder here because charon function items take both early and late-bound
106    /// lifetimes as arguments; given that the type here is polymorpohic in the late-bound
107    /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`),
108    /// we need to bind them here.
109    FnDef(RegionBinder<FnPtr>),
110    /// As a marker of taking out metadata from a given type
111    /// The internal type is assumed to be a type variable
112    PtrMetadata(Ty),
113    /// An array type `[T; N]`
114    Array(Ty, Box<ConstantExpr>),
115    /// A slice type `[T]`
116    Slice(Ty),
117    /// A pattern type. This is a newtype over the first type whose valid values are restricted by
118    /// the pattern.
119    Pattern(Ty, TypePattern),
120    /// A type that could not be computed or was incorrect.
121    #[drive(skip)]
122    Error(String),
123}
124
125#[derive(
126    Debug,
127    PartialEq,
128    Eq,
129    Copy,
130    Clone,
131    EnumIsA,
132    VariantName,
133    Serialize,
134    Deserialize,
135    Drive,
136    DriveMut,
137    DriveTwo,
138    Hash,
139    Ord,
140    PartialOrd,
141)]
142pub enum IntTy {
143    Isize,
144    I8,
145    I16,
146    I32,
147    I64,
148    I128,
149}
150
151#[derive(
152    Debug,
153    PartialEq,
154    Eq,
155    Copy,
156    Clone,
157    EnumIsA,
158    VariantName,
159    Serialize,
160    Deserialize,
161    Drive,
162    DriveMut,
163    DriveTwo,
164    Hash,
165    Ord,
166    PartialOrd,
167)]
168pub enum UIntTy {
169    Usize,
170    U8,
171    U16,
172    U32,
173    U64,
174    U128,
175}
176
177#[derive(
178    Debug,
179    PartialEq,
180    Eq,
181    Copy,
182    Clone,
183    EnumIsA,
184    VariantName,
185    Serialize,
186    Deserialize,
187    Drive,
188    DriveMut,
189    DriveTwo,
190    Hash,
191    Ord,
192    PartialOrd,
193)]
194#[cfg_attr(feature = "charon_on_charon", charon::rename("IntegerType"))]
195pub enum IntegerTy {
196    Signed(IntTy),
197    Unsigned(UIntTy),
198}
199
200#[derive(
201    Debug,
202    PartialEq,
203    Eq,
204    Copy,
205    Clone,
206    EnumIsA,
207    VariantName,
208    Serialize,
209    Deserialize,
210    Drive,
211    DriveMut,
212    DriveTwo,
213    Hash,
214    Ord,
215    PartialOrd,
216)]
217#[cfg_attr(feature = "charon_on_charon", charon::rename("FloatType"))]
218pub enum FloatTy {
219    F16,
220    F32,
221    F64,
222    F128,
223}
224
225/// Types of primitive values. Either an integer, bool, char
226#[derive(
227    Debug,
228    PartialEq,
229    Eq,
230    Clone,
231    Copy,
232    VariantName,
233    EnumIsA,
234    EnumAsGetters,
235    VariantIndexArity,
236    Serialize,
237    Deserialize,
238    SerializeState,
239    DeserializeState,
240    Drive,
241    DriveMut,
242    DriveTwo,
243    Hash,
244    Ord,
245    PartialOrd,
246)]
247#[cfg_attr(feature = "charon_on_charon", charon::rename("LiteralType"))]
248#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
249#[serde_state(stateless)]
250pub enum LiteralTy {
251    Int(IntTy),
252    UInt(UIntTy),
253    Float(FloatTy),
254    Bool,
255    Char,
256}
257
258/// Builtin types identifiers.
259///
260/// WARNING: for now, all the built-in types are covariant in the generic
261/// parameters (if there are). Adding types which don't satisfy this
262/// will require to update the code abstracting the signatures (to properly
263/// take into account the lifetime constraints).
264///
265/// TODO: update to not hardcode the types (except `Box` maybe) and be more
266/// modular.
267/// TODO: move to builtins.rs?
268#[derive(
269    Debug,
270    PartialEq,
271    Eq,
272    Clone,
273    Copy,
274    EnumIsA,
275    EnumAsGetters,
276    VariantName,
277    Serialize,
278    Deserialize,
279    Drive,
280    DriveMut,
281    DriveTwo,
282    Hash,
283    Ord,
284    PartialOrd,
285)]
286#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
287pub enum BuiltinTy {
288    /// Tuple type.
289    Tuple,
290    /// Boxes are de facto a primitive type.
291    Box,
292    /// Primitive type
293    Str,
294}
295
296impl BuiltinTy {
297    pub fn get_name(self) -> Name {
298        let name: &[_] = match self {
299            BuiltinTy::Box => &["alloc", "boxed", "Box"],
300            BuiltinTy::Str => &["str"],
301            BuiltinTy::Tuple => &["Tuple"],
302        };
303        Name::from_path(name)
304    }
305}
306
307#[derive(
308    Debug,
309    PartialEq,
310    Eq,
311    Clone,
312    Copy,
313    Hash,
314    VariantName,
315    EnumIsA,
316    Serialize,
317    Deserialize,
318    SerializeState,
319    DeserializeState,
320    Drive,
321    DriveMut,
322    DriveTwo,
323    Ord,
324    PartialOrd,
325)]
326#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("R"))]
327#[serde_state(stateless)]
328pub enum RefKind {
329    Mut,
330    Shared,
331}
332
333/// The contents of a `dyn Trait` type.
334#[derive(
335    Debug,
336    Clone,
337    PartialEq,
338    Eq,
339    PartialOrd,
340    Ord,
341    Hash,
342    SerializeState,
343    DeserializeState,
344    Drive,
345    DriveMut,
346    DriveTwo,
347)]
348pub struct DynPredicate {
349    /// This binder binds a single type `T`, which is considered existentially quantified. The
350    /// predicates in the binder apply to `T` and represent the `dyn Trait` constraints.
351    /// E.g. `dyn Iterator<Item=u32> + Send` is represented as `exists<T: Iterator<Item=u32> + Send> T`.
352    ///
353    /// Only the first trait clause may have methods. We use the vtable of this trait in the `dyn
354    /// Trait` pointer metadata.
355    pub binder: Binder<Ty>,
356}
357
358/// A type-level pattern used by [`TyKind::Pattern`].
359#[derive(
360    Debug,
361    Clone,
362    PartialEq,
363    Eq,
364    PartialOrd,
365    Ord,
366    Hash,
367    VariantName,
368    EnumIsA,
369    SerializeState,
370    DeserializeState,
371    Drive,
372    DriveMut,
373    DriveTwo,
374)]
375#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
376pub enum TypePattern {
377    Range(Box<ConstantExpr>, Box<ConstantExpr>),
378    OrPattern(Vec<TypePattern>),
379    NotNull,
380}
381
382macro_rules! static_type {
383    ($e:expr) => {{
384        use std::sync::LazyLock;
385        static TY: LazyLock<Ty> = LazyLock::new(|| $e.into_ty());
386        TY.clone()
387    }};
388}
389
390impl Ty {
391    pub fn new(kind: TyKind) -> Self {
392        Ty(HashConsed::new(kind))
393    }
394
395    pub fn kind(&self) -> &TyKind {
396        self.0.inner()
397    }
398
399    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
400        self.0.with_inner_mut(f)
401    }
402
403    /// Return the unit type
404    pub fn mk_unit() -> Ty {
405        static_type!(Ty::mk_tuple(vec![]).kind().clone())
406    }
407
408    pub fn mk_bool() -> Ty {
409        static_type!(TyKind::Literal(LiteralTy::Bool))
410    }
411
412    pub fn mk_usize() -> Ty {
413        static_type!(TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)))
414    }
415
416    pub fn mk_tuple(tys: Vec<Ty>) -> Ty {
417        TyKind::Adt(TypeDeclRef {
418            id: TypeId::Builtin(BuiltinTy::Tuple),
419            generics: Box::new(GenericArgs::new_types(tys.into())),
420        })
421        .into_ty()
422    }
423
424    pub fn mk_array(ty: Ty, len: ConstantExpr) -> Ty {
425        TyKind::Array(ty, Box::new(len)).into_ty()
426    }
427
428    pub fn mk_slice(ty: Ty) -> Ty {
429        TyKind::Slice(ty).into_ty()
430    }
431    /// Return true if it is actually unit (i.e.: 0-tuple)
432    pub fn is_unit(&self) -> bool {
433        match self.as_tuple() {
434            Some(tys) => tys.is_empty(),
435            None => false,
436        }
437    }
438
439    /// Return true if this is a scalar type
440    pub fn is_scalar(&self) -> bool {
441        match self.kind() {
442            TyKind::Literal(kind) => kind.is_int() || kind.is_uint(),
443            TyKind::Pattern(ty, _) => ty.is_scalar(),
444            _ => false,
445        }
446    }
447
448    pub fn is_unsigned_scalar(&self) -> bool {
449        match self.kind() {
450            TyKind::Literal(LiteralTy::UInt(_)) => true,
451            TyKind::Pattern(ty, _) => ty.is_unsigned_scalar(),
452            _ => false,
453        }
454    }
455
456    pub fn is_signed_scalar(&self) -> bool {
457        match self.kind() {
458            TyKind::Literal(LiteralTy::Int(_)) => true,
459            TyKind::Pattern(ty, _) => ty.is_signed_scalar(),
460            _ => false,
461        }
462    }
463
464    pub fn is_str(&self) -> bool {
465        match self.kind() {
466            TyKind::Adt(ty_ref) => ty_ref.is_str(),
467            _ => false,
468        }
469    }
470
471    /// Return true if the type is Box
472    pub fn is_box(&self) -> bool {
473        match self.kind() {
474            TyKind::Adt(ty_ref) => ty_ref.is_box(),
475            _ => false,
476        }
477    }
478
479    pub fn as_box(&self) -> Option<&Ty> {
480        match self.kind() {
481            TyKind::Adt(ty_ref) if ty_ref.is_box() => Some(&ty_ref.generics.types[0]),
482            _ => None,
483        }
484    }
485
486    pub fn as_adt_id(&self) -> Option<TypeDeclId> {
487        self.kind().as_adt()?.as_adt()
488    }
489
490    pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata {
491        let ty_decls = &translated.type_decls;
492        match self.kind() {
493            TyKind::Pattern(ty, _) => ty.get_ptr_metadata(translated),
494            TyKind::Adt(ty_ref) => {
495                // there are two cases:
496                // 1. if the declared type has a fixed metadata, just returns it
497                // 2. if it depends on some other types or the generic itself
498                match ty_ref.as_builtin() {
499                    None => {
500                        let Some(decl) = ty_decls.get(ty_ref.adt_id()) else {
501                            return PtrMetadata::InheritFrom(self.clone());
502                        };
503                        match decl.ptr_metadata.clone().substitute(&ty_ref.generics) {
504                            // if it depends on some type, recursion with the binding env
505                            PtrMetadata::InheritFrom(ty) => ty.get_ptr_metadata(translated),
506                            // otherwise, simply return it
507                            meta => meta,
508                        }
509                    }
510                    // the metadata of a tuple is simply the last field
511                    Some(BuiltinTy::Tuple) => {
512                        match ty_ref.generics.types.iter().last() {
513                            // `None` refers to the unit type `()`
514                            None => PtrMetadata::None,
515                            // Otherwise, simply recurse
516                            Some(ty) => ty.get_ptr_metadata(translated),
517                        }
518                    }
519                    // Box is a pointer like ref & raw ptr, hence no metadata
520                    Some(BuiltinTy::Box) => PtrMetadata::None,
521                    // `str` has metadata length
522                    Some(BuiltinTy::Str) => PtrMetadata::Length,
523                }
524            }
525            TyKind::DynTrait(pred) => match pred.vtable_ref(translated) {
526                Some(vtable) => PtrMetadata::VTable(vtable),
527                None => PtrMetadata::InheritFrom(self.clone()),
528            },
529            // `[T]` has metadata length
530            TyKind::Slice(..) => PtrMetadata::Length,
531            TyKind::TraitType(..) | TyKind::TypeVar(_) => PtrMetadata::InheritFrom(self.clone()),
532            TyKind::Literal(_)
533            | TyKind::Never
534            | TyKind::Ref(..)
535            | TyKind::RawPtr(..)
536            | TyKind::FnPtr(..)
537            | TyKind::FnDef(..)
538            | TyKind::Array(..)
539            | TyKind::Error(_) => PtrMetadata::None,
540            // The metadata itself must be Sized, hence must with `PtrMetadata::None`
541            TyKind::PtrMetadata(_) => PtrMetadata::None,
542        }
543    }
544
545    pub fn as_ref_or_ptr(&self) -> Option<&Ty> {
546        match self.kind() {
547            TyKind::RawPtr(ty, _) | TyKind::Ref(_, ty, _) => Some(ty),
548            _ => None,
549        }
550    }
551
552    pub fn as_array_or_slice(&self) -> Option<&Ty> {
553        match self.kind() {
554            TyKind::Slice(ty) | TyKind::Array(ty, _) => Some(ty),
555            _ => None,
556        }
557    }
558
559    pub fn as_tuple(&self) -> Option<&IndexVec<TypeVarId, Ty>> {
560        match self.kind() {
561            TyKind::Adt(ty_ref) if ty_ref.is_tuple() => Some(&ty_ref.generics.types),
562            _ => None,
563        }
564    }
565
566    pub fn as_adt(&self) -> Option<&TypeDeclRef> {
567        self.kind().as_adt()
568    }
569}
570
571impl TyKind {
572    pub fn into_ty(self) -> Ty {
573        Ty::new(self)
574    }
575}
576
577impl IntegerTy {
578    pub fn to_unsigned(&self) -> Self {
579        match self {
580            IntegerTy::Signed(IntTy::Isize) => IntegerTy::Unsigned(UIntTy::Usize),
581            IntegerTy::Signed(IntTy::I8) => IntegerTy::Unsigned(UIntTy::U8),
582            IntegerTy::Signed(IntTy::I16) => IntegerTy::Unsigned(UIntTy::U16),
583            IntegerTy::Signed(IntTy::I32) => IntegerTy::Unsigned(UIntTy::U32),
584            IntegerTy::Signed(IntTy::I64) => IntegerTy::Unsigned(UIntTy::U64),
585            IntegerTy::Signed(IntTy::I128) => IntegerTy::Unsigned(UIntTy::U128),
586            _ => *self,
587        }
588    }
589
590    /// Important: this returns the target byte count for the types.
591    /// Must not be used for host types from rustc.
592    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
593        match self {
594            IntegerTy::Signed(ty) => ty.target_size(ptr_size),
595            IntegerTy::Unsigned(ty) => ty.target_size(ptr_size),
596        }
597    }
598}
599
600impl LiteralTy {
601    pub fn to_integer_ty(&self) -> Option<IntegerTy> {
602        match self {
603            Self::Int(int_ty) => Some(IntegerTy::Signed(*int_ty)),
604            Self::UInt(uint_ty) => Some(IntegerTy::Unsigned(*uint_ty)),
605            _ => None,
606        }
607    }
608
609    /// Important: this returns the target byte count for the types.
610    /// Must not be used for host types from rustc.
611    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
612        match self {
613            LiteralTy::Int(int_ty) => int_ty.target_size(ptr_size),
614            LiteralTy::UInt(uint_ty) => uint_ty.target_size(ptr_size),
615            LiteralTy::Float(float_ty) => float_ty.target_size(),
616            LiteralTy::Char => 4,
617            LiteralTy::Bool => 1,
618        }
619    }
620}
621
622impl RefKind {
623    pub fn mutable(x: bool) -> Self {
624        if x { Self::Mut } else { Self::Shared }
625    }
626}
627
628impl DynPredicate {
629    /// Get a reference to the vtable type that corresponds to this predicate.
630    pub fn vtable_ref(&self, translated: &TranslatedCrate) -> Option<TypeDeclRef> {
631        let dyn_ty = TyKind::DynTrait(self.clone()).into_ty();
632        // The first clause is the one relevant for the vtable. We're extracting it from our binder
633        // so must give a value for the `Self` type.
634        let relevant_tref = self.binder.params.trait_clauses[0]
635            .trait_
636            .clone()
637            .erase()
638            .substitute(&GenericArgs::new_types([dyn_ty].into_iter().collect()));
639
640        // Get the vtable ref from the trait decl
641        let trait_decl = translated.trait_decls.get(relevant_tref.id)?;
642        let vtable_ref = trait_decl
643            .vtable
644            .clone()?
645            .substitute_with_self(&relevant_tref.generics, &TraitRefKind::Dyn);
646        Some(vtable_ref)
647    }
648}
649
650impl From<LiteralTy> for Ty {
651    fn from(value: LiteralTy) -> Self {
652        TyKind::Literal(value).into_ty()
653    }
654}
655
656impl From<TyKind> for Ty {
657    fn from(kind: TyKind) -> Ty {
658        kind.into_ty()
659    }
660}
661
662/// Convenience impl.
663impl std::ops::Deref for Ty {
664    type Target = TyKind;
665
666    fn deref(&self) -> &Self::Target {
667        self.kind()
668    }
669}
charon_lib/ast/type_level/types.rs

charon_lib/ast/type_level/
types.rs
