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. Interpreting this back to a structured value is left as an
82    /// exercice to the consumer.
83    Memory(Vec<u8>),
84    Todo(String),
85}
86
87#[derive(Clone, Debug, Hash, PartialEq, Eq)]
88pub struct ConstantFieldExpr {
89    pub field: DefId,
90    pub value: ConstantExpr,
91}
92
93/// Rustc has different representation for constants: one for MIR
94/// ([`rustc_middle::mir::Const`]), one for the type system
95/// ([`rustc_middle::ty::ConstKind`]). For simplicity hax maps those
96/// two construct to one same `ConstantExpr` type.
97pub type ConstantExpr = Decorated<ConstantExprKind>;
98
99// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one
100pub type ConstantKind = ConstantExpr;
101
102pub use self::uneval::*;
103mod uneval;
charon_driver/hax/constant_utils.rs

charon_driver/hax/
constant_utils.rs
