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 expressions 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    ConstRef {
74        id: ParamConst,
75    },
76    /// A function definition, corresponding to a particular item. This is a ZST, unlike `FnPtr`.
77    FnDef(ItemRef),
78    /// A function pointer. This is an actual pointer to that function.
79    FnPtr(ItemRef),
80    /// A blob of memory containing the byte representation of the value. This can occur when
81    /// evaluating MIR constants (e.g. unions). Interpreting this back to a structured value
82    /// is left as an exercice to the consumer.
83    Memory(Vec<ConstantByte>),
84    Todo(String),
85}
86
87/// A byte of an evaluated constant, in the MiniRust sense.
88#[derive(Clone, Debug, Hash, PartialEq, Eq)]
89pub enum ConstantByte {
90    /// An uninitialized byte (e.g. padding, or the bytes of a union not covered by the active
91    /// field).
92    Uninit,
93    /// A concrete byte value.
94    Value(u8),
95    /// A byte that is part of a pointer with provenance. The `u8` is the offset of this byte
96    /// within the pointer.
97    Provenance(ConstantByteProvenance, u8),
98}
99
100/// What a pointer byte in an evaluated constant points to.
101#[derive(Clone, Debug, Hash, PartialEq, Eq)]
102pub enum ConstantByteProvenance {
103    /// A pointer to a static.
104    Global(ItemRef),
105    /// A pointer to a function.
106    Function(ItemRef),
107    /// A pointer to anything else (an anonymous allocation, a vtable...).
108    Unknown,
109}
110
111#[derive(Clone, Debug, Hash, PartialEq, Eq)]
112pub struct ConstantFieldExpr {
113    pub field: DefId,
114    pub value: ConstantExpr,
115}
116
117/// Rustc has different representation for constants: one for MIR
118/// ([`rustc_middle::mir::Const`]), one for the type system
119/// ([`rustc_middle::ty::ConstKind`]). For simplicity hax maps those
120/// two construct to one same `ConstantExpr` type.
121pub type ConstantExpr = Decorated<ConstantExprKind>;
122
123// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one
124pub type ConstantKind = ConstantExpr;
125
126pub use self::uneval::*;
127mod uneval;
charon_driver/hax/constant_utils.rs

charon_driver/hax/
constant_utils.rs
