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

charon_lib/ast/type_level/
types.rs
