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};
6use std::ops::DerefMut;
7
8/// A type.
9///
10/// This is an interned value; see `TyKind` for the actual contents.
11#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
12#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
13#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
14pub struct Ty(pub HashConsed<WithCachedTypeInfo<TyKind>>);
15
16/// A type.
17///
18/// This is interned as `Ty`, making it cheap to clone and compare.
19#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
20#[derive(VariantName, EnumIsA, EnumAsGetters, EnumToGetters, VariantIndexArity)]
21#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
22#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
23pub enum TyKind {
24    /// A scalar (integers, floats, `char`, or `bool`).
25    Scalar(ScalarTy),
26    /// An array `[T; N]`. The third field is the proof that `T: Sized`; it is absent with
27    /// `--hide-marker-traits`.
28    Array(Ty, ConstantExpr, Option<TraitRef>),
29    /// A slice `[T]`. The second field is the proof that `T: Sized`; it is absent with
30    /// `--hide-marker-traits`.
31    Slice(Ty, Option<TraitRef>),
32    /// An ADT: structs, enums, unions, as well as tuples and `str`.
33    Adt(TypeDeclRef),
34    /// A reference: `&T` or `&mut T`.
35    Ref(Region, Ty, RefKind),
36    /// A raw pointer.
37    RawPtr(Ty, RefKind),
38    /// The unique type associated with each function item. Each function item is given a unique
39    /// type that has the function's early-bound generics. This type is not generally nameable in
40    /// Rust; it's a ZST (there's a unique value), and a value of that type can be cast to a
41    /// function pointer or passed to functions that expect `FnOnce`/`FnMut`/`Fn` parameters.
42    ///
43    /// There's a binder here because charon function items take both early and late-bound
44    /// lifetimes as arguments; given that the type we're pointing to is polymorphic in the
45    /// late-bound variables, we need to bind them here.
46    ///
47    /// ```rust
48    /// // `'a` is early-bound, 'b is late-bound.
49    /// fn foo<'a, 'b>(x: &'a u32, y: &'b u32)
50    /// where u32: 'b
51    /// {}
52    /// ```
53    /// For rustc, there's a ZST `foo<'a>`, that can be cast to a `for<'b> fn(&'a u32, &'b u32)`
54    /// function pointer.
55    /// For charon, there's an item `foo<'a, 'b>`, and the `FnDef` item that corresponds to rustc's
56    /// `foo<'a>` is represented as `FnDef(for<'b> foo<'a, 'b>)`.
57    FnDef(RegionBinder<FnPtr>),
58    /// Function pointer type. This is a literal pointer to a region of memory that contains a
59    /// callable function.
60    ///
61    /// A function pointer can have lifetime generics, e.g. `for<'a> fn(&'a mut u32) -> &'a u32`,
62    /// hence the binder.
63    FnPtr(RegionBinder<FunSig>),
64    /// `dyn Trait`: erased value known to implement `Trait`. A pointer to it will carry a vtable
65    /// pointer that stores the methods that can be called on this value.
66    DynTrait(DynPredicate),
67    /// A pattern type: a type that is representationally identical to its base type, except the
68    /// only valid values are the ones that match the pattern.
69    Pattern(Ty, TypePattern),
70    /// The never type, the canonical uninhabited type.
71    Never,
72
73    /// A type variable.
74    #[cfg_attr(feature = "charon_on_charon", charon::rename("TVar"))]
75    TypeVar(TypeDbVar),
76    /// A trait associated type: `<T as Trait>::AssocType<Args>`.
77    TraitType(TraitRef, AssocTypeId, GenericArgs),
78    /// The type of pointer metadata for the given type; e.g. for `[T]`, this type is `usize`. The
79    /// way to write this type in Rust is `<X as core::ptr::Pointee>::Metadata`.
80    PtrMetadata(Ty),
81
82    /// A type that could not be computed or was incorrect.
83    Error(String),
84}
85
86/// Types of primitive scalar values.
87#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
88#[derive(VariantName, EnumIsA, EnumAsGetters, VariantIndexArity)]
89#[derive(
90    Serialize,
91    Deserialize,
92    SerializeState,
93    DeserializeState,
94    Drive,
95    DriveMut,
96    DriveTwo
97)]
98#[cfg_attr(feature = "charon_on_charon", charon::rename("ScalarType"))]
99#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
100#[serde_state(stateless)]
101pub enum ScalarTy {
102    Integer(IntegerTy),
103    Float(FloatTy),
104    Bool,
105    Char,
106}
107
108#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
109#[derive(EnumIsA, VariantName)]
110#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
111#[cfg_attr(feature = "charon_on_charon", charon::rename("IntegerType"))]
112pub enum IntegerTy {
113    Signed(IntTy),
114    Unsigned(UIntTy),
115}
116
117#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
118#[derive(EnumIsA, VariantName)]
119#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
120pub enum IntTy {
121    Isize,
122    I8,
123    I16,
124    I32,
125    I64,
126    I128,
127}
128
129#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
130#[derive(EnumIsA, VariantName)]
131#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
132pub enum UIntTy {
133    Usize,
134    U8,
135    U16,
136    U32,
137    U64,
138    U128,
139}
140
141#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
142#[derive(EnumIsA, VariantName)]
143#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
144#[cfg_attr(feature = "charon_on_charon", charon::rename("FloatType"))]
145pub enum FloatTy {
146    F16,
147    F32,
148    F64,
149    F128,
150}
151
152/// Builtin ADT identifiers.
153#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
154#[derive(EnumIsA, EnumAsGetters, VariantName)]
155#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
156#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
157pub enum BuiltinAdt {
158    /// A tuple `(A, B, ...)`, including `unit`.
159    Tuple,
160    /// Boxes; always detected, though they are only treated as primitives with `--treat-box-as-builtin`
161    Box,
162    /// The `str` type, which corresponds to a `[u8]` that encodes a string with UTF-8.
163    Str,
164}
165
166#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
167#[derive(VariantName, EnumIsA)]
168#[derive(
169    Serialize,
170    Deserialize,
171    SerializeState,
172    DeserializeState,
173    Drive,
174    DriveMut,
175    DriveTwo
176)]
177#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("R"))]
178#[serde_state(stateless)]
179pub enum RefKind {
180    Mut,
181    Shared,
182}
183
184/// The contents of a `dyn Trait` type.
185#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
186#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
187pub struct DynPredicate {
188    /// This binder binds a single type `T`, which is considered existentially quantified. The
189    /// predicates in the binder apply to `T` and represent the `dyn Trait` constraints.
190    /// E.g. `dyn Iterator<Item=u32> + Send` is represented as `exists<T: Iterator<Item=u32> + Send> T`.
191    ///
192    /// Only the first trait clause may have methods. We use the vtable of this trait in the `dyn
193    /// Trait` pointer metadata.
194    pub binder: Binder<Ty>,
195}
196
197/// A type-level pattern used by [`TyKind::Pattern`].
198#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
199#[derive(VariantName, EnumIsA)]
200#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
201#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
202pub enum TypePattern {
203    Range(ConstantExpr, ConstantExpr),
204    OrPattern(Vec<TypePattern>),
205    NotNull,
206}
207
208macro_rules! static_type {
209    ($e:expr) => {{
210        use std::sync::LazyLock;
211        static TY: LazyLock<Ty> = LazyLock::new(|| $e.into_ty());
212        TY.clone()
213    }};
214}
215
216impl Ty {
217    pub fn new(kind: TyKind) -> Self {
218        Ty(HashConsed::new(WithCachedTypeInfo::new(kind)))
219    }
220
221    pub fn kind(&self) -> &TyKind {
222        self.0.inner()
223    }
224
225    /// Temporarily allow mutation of the `TyKind`, cloning it if needed.
226    pub fn as_mut(&mut self) -> impl DerefMut<Target = TyKind> {
227        struct TyMutRef<T: DerefMut<Target = WithCachedTypeInfo<TyKind>>>(T);
228
229        impl<T: DerefMut<Target = WithCachedTypeInfo<TyKind>>> std::ops::Deref for TyMutRef<T> {
230            type Target = TyKind;
231            fn deref(&self) -> &Self::Target {
232                &self.0
233            }
234        }
235        impl<T: DerefMut<Target = WithCachedTypeInfo<TyKind>>> DerefMut for TyMutRef<T> {
236            fn deref_mut(&mut self) -> &mut Self::Target {
237                self.0.value_mut()
238            }
239        }
240
241        impl<T: DerefMut<Target = WithCachedTypeInfo<TyKind>>> Drop for TyMutRef<T> {
242            fn drop(&mut self) {
243                self.0.recompute_type_info();
244            }
245        }
246
247        TyMutRef(self.0.as_mut())
248    }
249    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
250        f(&mut self.as_mut())
251    }
252
253    /// Return the unit type
254    pub fn mk_unit() -> Ty {
255        static_type!(TyKind::Adt(TypeDeclRef {
256            id: TypeDeclId::UNIT,
257            generics: Box::new(GenericArgs::empty()),
258            builtin: Some(BuiltinAdt::Tuple),
259        }))
260    }
261
262    pub fn mk_bool() -> Ty {
263        static_type!(TyKind::Scalar(ScalarTy::Bool))
264    }
265
266    pub fn mk_u8() -> Ty {
267        static_type!(TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(
268            UIntTy::U8
269        ))))
270    }
271
272    pub fn mk_usize() -> Ty {
273        static_type!(TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(
274            UIntTy::Usize
275        ))))
276    }
277
278    pub fn mk_array(ty: Ty, len: ConstantExpr, ty_is_sized: Option<TraitRef>) -> Ty {
279        TyKind::Array(ty, len, ty_is_sized).into_ty()
280    }
281
282    pub fn mk_slice(ty: Ty, ty_is_sized: Option<TraitRef>) -> Ty {
283        TyKind::Slice(ty, ty_is_sized).into_ty()
284    }
285
286    /// Return true if it is actually unit (i.e.: 0-tuple)
287    pub fn is_unit(&self) -> bool {
288        *self == Ty::mk_unit()
289    }
290
291    pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata {
292        let ty_decls = &translated.type_decls;
293        match self.kind() {
294            TyKind::Pattern(ty, _) => ty.get_ptr_metadata(translated),
295            TyKind::Adt(ty_ref) => {
296                // there are two cases:
297                // 1. if the declared type has a fixed metadata, just returns it
298                // 2. if it depends on some other types or the generic itself
299                let Some(decl) = ty_decls.get(ty_ref.id) else {
300                    return PtrMetadata::InheritFrom(self.clone());
301                };
302                match decl.ptr_metadata.clone().substitute(&ty_ref.generics) {
303                    // if it depends on some type, recursion with the binding env
304                    PtrMetadata::InheritFrom(ty) => ty.get_ptr_metadata(translated),
305                    // otherwise, simply return it
306                    meta => meta,
307                }
308            }
309            TyKind::DynTrait(pred) => match pred.vtable_ref(translated) {
310                Some(vtable) => PtrMetadata::VTable(vtable),
311                None => PtrMetadata::InheritFrom(self.clone()),
312            },
313            // `[T]` has metadata length
314            TyKind::Slice(..) => PtrMetadata::Length,
315            TyKind::TraitType(..) | TyKind::TypeVar(_) => PtrMetadata::InheritFrom(self.clone()),
316            TyKind::Scalar(_)
317            | TyKind::Never
318            | TyKind::Ref(..)
319            | TyKind::RawPtr(..)
320            | TyKind::FnPtr(..)
321            | TyKind::FnDef(..)
322            | TyKind::Array(..)
323            | TyKind::Error(_) => PtrMetadata::None,
324            // The metadata itself must be Sized, hence must with `PtrMetadata::None`
325            TyKind::PtrMetadata(_) => PtrMetadata::None,
326        }
327    }
328
329    /// The field types of a tuple, in order. Panics if the type is not a tuple,
330    /// or if the type declaration is not found in the crate.
331    pub fn as_tuple_fields(&self, translated: &TranslatedCrate) -> Vec<Ty> {
332        let Some(tref) = self.as_adt().filter(|tref| tref.is_tuple()) else {
333            unreachable!("as_tuple_fields called on non-tuple type {:?}", self);
334        };
335
336        // Avoid doing a substitution if the tuple is polymorphic and we can just
337        // retrieve the fields from the generics, since substitutions won't work
338        // in case `--unbind-item-vars` is set.
339        let is_instantiated = translated
340            .item_names
341            .get(&ItemId::Type(tref.id))
342            .map(|name| name.name.iter().any(|elem| elem.is_instantiated()))
343            .unwrap_or(false);
344        if !is_instantiated {
345            return tref.generics.types.as_vec().clone();
346        }
347
348        translated
349            .type_decls
350            .get(tref.id)
351            .and_then(|decl| decl.kind.as_struct())
352            .expect("the declaration of specialized tuple {tref:?} is missing")
353            .iter()
354            .map(|f| f.ty.clone().substitute(&tref.generics))
355            .collect()
356    }
357
358    pub fn as_adt(&self) -> Option<&TypeDeclRef> {
359        self.kind().as_adt()
360    }
361}
362
363impl TyKind {
364    pub fn into_ty(self) -> Ty {
365        Ty::new(self)
366    }
367
368    pub fn is_usize(&self) -> bool {
369        self.as_scalar().is_some_and(|s| s.is_usize())
370    }
371
372    pub fn is_unsigned_scalar(&self) -> bool {
373        match self {
374            TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(_))) => true,
375            TyKind::Pattern(ty, _) => ty.is_unsigned_scalar(),
376            _ => false,
377        }
378    }
379
380    pub fn is_signed_scalar(&self) -> bool {
381        match self {
382            TyKind::Scalar(ScalarTy::Integer(IntegerTy::Signed(_))) => true,
383            TyKind::Pattern(ty, _) => ty.is_signed_scalar(),
384            _ => false,
385        }
386    }
387
388    pub fn is_bool(&self) -> bool {
389        matches!(self, TyKind::Scalar(ScalarTy::Bool))
390    }
391
392    pub fn is_str(&self) -> bool {
393        match self {
394            TyKind::Adt(ty_ref) => ty_ref.is_str(),
395            _ => false,
396        }
397    }
398
399    /// Return true if the type is Box
400    pub fn is_box(&self) -> bool {
401        match self {
402            TyKind::Adt(ty_ref) => ty_ref.is_box(),
403            _ => false,
404        }
405    }
406
407    pub fn is_tuple(&self) -> bool {
408        match self {
409            TyKind::Adt(ty_ref) => ty_ref.is_tuple(),
410            _ => false,
411        }
412    }
413
414    pub fn as_adt_id(&self) -> Option<TypeDeclId> {
415        self.as_adt().map(|a| a.id)
416    }
417
418    pub fn as_box(&self) -> Option<&Ty> {
419        match self {
420            TyKind::Adt(ty_ref) if ty_ref.is_box() => Some(&ty_ref.generics.types[0]),
421            _ => None,
422        }
423    }
424
425    pub fn as_box_mut(&mut self) -> Option<&mut Ty> {
426        match self {
427            TyKind::Adt(ty_ref) if ty_ref.is_box() => Some(&mut ty_ref.generics.types[0]),
428            _ => None,
429        }
430    }
431
432    pub fn builtin_deref(&self) -> Option<&Ty> {
433        match self {
434            TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => Some(ty),
435            TyKind::Adt(ty_ref) if ty_ref.is_box() => Some(&ty_ref.generics.types[0]),
436            _ => None,
437        }
438    }
439
440    pub fn builtin_deref_mut(&mut self) -> Option<&mut Ty> {
441        match self {
442            TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => Some(ty),
443            TyKind::Adt(ty_ref) if ty_ref.is_box() => Some(&mut ty_ref.generics.types[0]),
444            _ => None,
445        }
446    }
447
448    pub fn as_array_or_slice(&self) -> Option<&Ty> {
449        match self {
450            TyKind::Slice(ty, _) | TyKind::Array(ty, ..) => Some(ty),
451            _ => None,
452        }
453    }
454
455    pub fn as_array_or_slice_mut(&mut self) -> Option<&mut Ty> {
456        match self {
457            TyKind::Slice(ty, _) | TyKind::Array(ty, ..) => Some(ty),
458            _ => None,
459        }
460    }
461}
462
463impl IntegerTy {
464    pub fn to_unsigned(&self) -> Self {
465        match self {
466            IntegerTy::Signed(IntTy::Isize) => IntegerTy::Unsigned(UIntTy::Usize),
467            IntegerTy::Signed(IntTy::I8) => IntegerTy::Unsigned(UIntTy::U8),
468            IntegerTy::Signed(IntTy::I16) => IntegerTy::Unsigned(UIntTy::U16),
469            IntegerTy::Signed(IntTy::I32) => IntegerTy::Unsigned(UIntTy::U32),
470            IntegerTy::Signed(IntTy::I64) => IntegerTy::Unsigned(UIntTy::U64),
471            IntegerTy::Signed(IntTy::I128) => IntegerTy::Unsigned(UIntTy::U128),
472            _ => *self,
473        }
474    }
475
476    /// Important: this returns the target byte count for the types.
477    /// Must not be used for host types from rustc.
478    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
479        match self {
480            IntegerTy::Signed(ty) => ty.target_size(ptr_size),
481            IntegerTy::Unsigned(ty) => ty.target_size(ptr_size),
482        }
483    }
484}
485
486impl ScalarTy {
487    pub fn is_usize(&self) -> bool {
488        matches!(self, ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::Usize)))
489    }
490
491    /// Important: this returns the target byte count for the types.
492    /// Must not be used for host types from rustc.
493    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
494        match self {
495            ScalarTy::Integer(int_ty) => int_ty.target_size(ptr_size),
496            ScalarTy::Float(float_ty) => float_ty.target_size(),
497            ScalarTy::Char => 4,
498            ScalarTy::Bool => 1,
499        }
500    }
501}
502
503impl RefKind {
504    pub fn mutable(x: bool) -> Self {
505        if x { Self::Mut } else { Self::Shared }
506    }
507}
508
509impl DynPredicate {
510    /// Get a reference to the vtable type that corresponds to this predicate.
511    pub fn vtable_ref(&self, translated: &TranslatedCrate) -> Option<TypeDeclRef> {
512        let dyn_ty = TyKind::DynTrait(self.clone()).into_ty();
513        // The first clause is the one relevant for the vtable. We're extracting it from our binder
514        // so must give a value for the `Self` type.
515        let relevant_tref = self.binder.params.trait_clauses[0]
516            .trait_
517            .clone()
518            .erase()
519            .substitute(&GenericArgs::new_types([dyn_ty].into()));
520
521        // Get the vtable ref from the trait decl
522        let trait_decl = translated.trait_decls.get(relevant_tref.id)?;
523        let vtable_ref = trait_decl
524            .vtable
525            .clone()?
526            .substitute_with_self(&relevant_tref.generics, &TraitRefKind::Dyn);
527        Some(vtable_ref)
528    }
529}
530
531impl From<ScalarTy> for Ty {
532    fn from(value: ScalarTy) -> Self {
533        TyKind::Scalar(value).into_ty()
534    }
535}
536
537impl From<TyKind> for Ty {
538    fn from(kind: TyKind) -> Ty {
539        kind.into_ty()
540    }
541}
542
543/// Convenience impl.
544impl std::ops::Deref for Ty {
545    type Target = WithCachedTypeInfo<TyKind>;
546    fn deref(&self) -> &Self::Target {
547        &self.0
548    }
549}
550
551/// Dummy impl, only there to avoid overflow computing whether our types are `Send` given the giant
552/// recursive knot of types we have.
553unsafe impl Send for Ty {}
charon_lib/ast/type_level/types.rs

charon_lib/ast/type_level/
types.rs
