charon_driver/hax/
constant_utils.rs

1use crate::hax::prelude::*;
2
3#[derive(Clone, Debug, Hash, PartialEq, Eq)]
4pub enum ConstantInt {
5    Int(i128, IntTy),
6    Uint(u128, UintTy),
7}
8
9#[derive(Clone, Debug, Hash, PartialEq, Eq)]
10pub enum ConstantLiteral {
11    Bool(bool),
12    Char(char),
13    Float(String, FloatTy),
14    Int(ConstantInt),
15    PtrNoProvenance(u128),
16    Str(String),
17    ByteStr(Vec<u8>),
18}
19
20sinto_reexport!(rustc_abi::VariantIdx);
21
22/// Describe the kind of a variant
23#[derive(Clone, Debug, Hash, PartialEq, Eq)]
24pub enum VariantKind {
25    Struct,
26    Union,
27    Enum { index: VariantIdx },
28}
29
30/// The subset of [Expr] that corresponds to constants.
31#[derive(Clone, Debug, Hash, PartialEq, Eq)]
32pub enum ConstantExprKind {
33    Literal(ConstantLiteral),
34    // Adts (structs, enums, unions) or closures.
35    Adt {
36        kind: VariantKind,
37        fields: Vec<ConstantFieldExpr>,
38    },
39    Array {
40        fields: Vec<ConstantExpr>,
41    },
42    Tuple {
43        fields: Vec<ConstantExpr>,
44    },
45    /// A top-level or associated constant.
46    ///
47    /// Remark: constants *can* have generic parameters.
48    /// Example:
49    /// ```text
50    /// struct V<const N: usize, T> {
51    ///   x: [T; N],
52    /// }
53    ///
54    /// impl<const N: usize, T> V<N, T> {
55    ///   const LEN: usize = N; // This has generics <N, T>
56    /// }
57    ///
58    /// impl Foo for Bar {
59    ///   const C : usize = 32; // <-
60    /// }
61    /// ```
62    ///
63    /// If `options.inline_anon_consts` is `false`, this is also used for inline const blocks and
64    /// advanced const generics expressions.
65    NamedGlobal(ItemRef),
66    /// A shared reference to a static variable.
67    Borrow(ConstantExpr),
68    /// A raw borrow (`*const` or `*mut`).
69    RawBorrow {
70        mutability: Mutability,
71        arg: ConstantExpr,
72    },
73    /// A cast `<source> as <type>`, `<type>` is stored as the type of
74    /// the current constant expression. Currently, this is only used
75    /// to represent `lit as *mut T` or `lit as *const T`, where `lit`
76    /// is a `usize` literal.
77    Cast {
78        source: ConstantExpr,
79    },
80    ConstRef {
81        id: ParamConst,
82    },
83    /// A function definition, corresponding to a particular item. This is a ZST, unlike `FnPtr`.
84    FnDef(ItemRef),
85    /// A function pointer. This is an actual pointer to that function.
86    FnPtr(ItemRef),
87    /// A blob of memory containing the byte representation of the value. This can occur when
88    /// evaluating MIR constants. Interpreting this back to a structured value is left as an
89    /// exercice to the consumer.
90    Memory(Vec<u8>),
91    Todo(String),
92}
93
94#[derive(Clone, Debug, Hash, PartialEq, Eq)]
95pub struct ConstantFieldExpr {
96    pub field: DefId,
97    pub value: ConstantExpr,
98}
99
100/// Rustc has different representation for constants: one for MIR
101/// ([`rustc_middle::mir::Const`]), one for the type system
102/// ([`rustc_middle::ty::ConstKind`]). For simplicity hax maps those
103/// two construct to one same `ConstantExpr` type.
104pub type ConstantExpr = Decorated<ConstantExprKind>;
105
106// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one
107pub type ConstantKind = ConstantExpr;
108
109pub use self::uneval::*;
110mod uneval;
charon_driver/hax/constant_utils.rs

charon_driver/hax/
constant_utils.rs
