hax_frontend_exporter/
constant_utils.rs

1use crate::prelude::*;
2
3#[derive_group(Serializers)]
4#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
5pub enum ConstantInt {
6    Int(
7        #[serde(with = "serialize_int::signed")]
8        #[schemars(with = "String")]
9        i128,
10        IntTy,
11    ),
12    Uint(
13        #[serde(with = "serialize_int::unsigned")]
14        #[schemars(with = "String")]
15        u128,
16        UintTy,
17    ),
18}
19
20#[derive_group(Serializers)]
21#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
22pub enum ConstantLiteral {
23    Bool(bool),
24    Char(char),
25    Float(String, FloatTy),
26    Int(ConstantInt),
27    PtrNoProvenance(u128),
28    Str(String),
29    ByteStr(Vec<u8>),
30}
31
32/// The subset of [Expr] that corresponds to constants.
33#[derive_group(Serializers)]
34#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
35pub enum ConstantExprKind {
36    Literal(ConstantLiteral),
37    // Adts (structs, enums, unions) or closures.
38    Adt {
39        info: VariantInformations,
40        fields: Vec<ConstantFieldExpr>,
41    },
42    Array {
43        fields: Vec<ConstantExpr>,
44    },
45    Tuple {
46        fields: Vec<ConstantExpr>,
47    },
48    /// A top-level constant or a constant appearing in an impl block.
49    ///
50    /// Remark: constants *can* have generic parameters.
51    /// Example:
52    /// ```text
53    /// struct V<const N: usize, T> {
54    ///   x: [T; N],
55    /// }
56    ///
57    /// impl<const N: usize, T> V<N, T> {
58    ///   const LEN: usize = N; // This has generics <N, T>
59    /// }
60    /// ```
61    ///
62    /// If `options.inline_anon_consts` is `false`, this is also used for inline const blocks and
63    /// advanced const generics expressions.
64    GlobalName(ItemRef),
65    /// A trait constant
66    ///
67    /// Ex.:
68    /// ```text
69    /// impl Foo for Bar {
70    ///   const C : usize = 32; // <-
71    /// }
72    /// ```
73    TraitConst {
74        impl_expr: ImplExpr,
75        name: String,
76    },
77    /// A shared reference to a static variable.
78    Borrow(ConstantExpr),
79    /// A raw borrow (`*const` or `*mut`).
80    RawBorrow {
81        mutability: Mutability,
82        arg: ConstantExpr,
83    },
84    /// A cast `<source> as <type>`, `<type>` is stored as the type of
85    /// the current constant expression. Currently, this is only used
86    /// to represent `lit as *mut T` or `lit as *const T`, where `lit`
87    /// is a `usize` literal.
88    Cast {
89        source: ConstantExpr,
90    },
91    ConstRef {
92        id: ParamConst,
93    },
94    FnPtr(ItemRef),
95    /// A blob of memory containing the byte representation of the value. This can occur when
96    /// evaluating MIR constants. Interpreting this back to a structured value is left as an
97    /// exercice to the consumer.
98    Memory(Vec<u8>),
99    Todo(String),
100}
101
102#[derive_group(Serializers)]
103#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
104pub struct ConstantFieldExpr {
105    pub field: DefId,
106    pub value: ConstantExpr,
107}
108
109/// Rustc has different representation for constants: one for MIR
110/// ([`rustc_middle::mir::Const`]), one for the type system
111/// ([`rustc_middle::ty::ConstKind`]). For simplicity hax maps those
112/// two construct to one same `ConstantExpr` type.
113pub type ConstantExpr = Decorated<ConstantExprKind>;
114
115// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one
116pub type ConstantKind = ConstantExpr;
117
118impl From<ConstantFieldExpr> for FieldExpr {
119    fn from(c: ConstantFieldExpr) -> FieldExpr {
120        FieldExpr {
121            value: c.value.into(),
122            field: c.field,
123        }
124    }
125}
126
127impl From<ConstantExpr> for Expr {
128    fn from(c: ConstantExpr) -> Expr {
129        use ConstantExprKind::*;
130        let kind = match *c.contents {
131            Literal(lit) => {
132                use ConstantLiteral::*;
133                let mut neg = false;
134                let node = match lit {
135                    Bool(b) => LitKind::Bool(b),
136                    Char(c) => LitKind::Char(c),
137                    Int(i) => {
138                        use LitIntType::*;
139                        match i {
140                            ConstantInt::Uint(v, t) => LitKind::Int(v, Unsigned(t)),
141                            ConstantInt::Int(v, t) => {
142                                neg = v.is_negative();
143                                LitKind::Int(v.abs_diff(0), Signed(t))
144                            }
145                        }
146                    }
147                    Float(f, ty) => LitKind::Float(f, LitFloatType::Suffixed(ty)),
148                    PtrNoProvenance(p) => LitKind::Int(p, LitIntType::Unsigned(UintTy::Usize)),
149                    ByteStr(raw) => LitKind::ByteStr(raw, StrStyle::Cooked),
150                    Str(raw) => LitKind::Str(raw, StrStyle::Cooked),
151                };
152                let span = c.span.clone();
153                let lit = Spanned { span, node };
154                ExprKind::Literal { lit, neg }
155            }
156            Adt { info, fields } => ExprKind::Adt(AdtExpr {
157                info,
158                fields: fields.into_iter().map(|field| field.into()).collect(),
159                base: AdtExprBase::None,
160                user_ty: None,
161            }),
162            GlobalName(item) => ExprKind::GlobalName {
163                item,
164                constructor: None,
165            },
166            Borrow(e) => ExprKind::Borrow {
167                borrow_kind: BorrowKind::Shared,
168                arg: e.into(),
169            },
170            RawBorrow { mutability, arg } => ExprKind::RawBorrow {
171                mutability,
172                arg: arg.into(),
173            },
174            ConstRef { id } => ExprKind::ConstRef { id },
175            Array { fields } => ExprKind::Array {
176                fields: fields.into_iter().map(|field| field.into()).collect(),
177            },
178            Tuple { fields } => ExprKind::Tuple {
179                fields: fields.into_iter().map(|field| field.into()).collect(),
180            },
181            Cast { source } => ExprKind::Cast {
182                source: source.into(),
183            },
184            kind @ (FnPtr { .. } | TraitConst { .. } | Memory { .. }) => {
185                ExprKind::Todo(format!("Unsupported constant kind. kind={:#?}", kind))
186            }
187            Todo(msg) => ExprKind::Todo(msg),
188        };
189        Decorated {
190            contents: Box::new(kind),
191            ty: c.ty,
192            span: c.span,
193            hir_id: c.hir_id,
194            attributes: c.attributes,
195        }
196    }
197}
198
199#[cfg(feature = "rustc")]
200pub use self::uneval::*;
201#[cfg(feature = "rustc")]
202mod uneval;
hax_frontend_exporter/constant_utils.rs

hax_frontend_exporter/
constant_utils.rs
