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

hax_frontend_exporter/
constant_utils.rs
