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    Str(String),
28    ByteStr(Vec<u8>),
29}
30
31/// The subset of [Expr] that corresponds to constants.
32#[derive_group(Serializers)]
33#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
34pub enum ConstantExprKind {
35    Literal(ConstantLiteral),
36    // Adts (structs, enums, unions) or closures.
37    Adt {
38        info: VariantInformations,
39        fields: Vec<ConstantFieldExpr>,
40    },
41    Array {
42        fields: Vec<ConstantExpr>,
43    },
44    Tuple {
45        fields: Vec<ConstantExpr>,
46    },
47    /// A top-level constant or a constant appearing in an impl block.
48    ///
49    /// Remark: constants *can* have generic parameters.
50    /// Example:
51    /// ```text
52    /// struct V<const N: usize, T> {
53    ///   x: [T; N],
54    /// }
55    ///
56    /// impl<const N: usize, T> V<N, T> {
57    ///   const LEN: usize = N; // This has generics <N, T>
58    /// }
59    /// ```
60    ///
61    /// If `options.inline_anon_consts` is `false`, this is also used for inline const blocks and
62    /// advanced const generics expressions.
63    GlobalName(ItemRef),
64    /// A trait constant
65    ///
66    /// Ex.:
67    /// ```text
68    /// impl Foo for Bar {
69    ///   const C : usize = 32; // <-
70    /// }
71    /// ```
72    TraitConst {
73        impl_expr: ImplExpr,
74        name: String,
75    },
76    /// A shared reference to a static variable.
77    Borrow(ConstantExpr),
78    /// A raw borrow (`*const` or `*mut`).
79    RawBorrow {
80        mutability: Mutability,
81        arg: ConstantExpr,
82    },
83    /// A cast `<source> as <type>`, `<type>` is stored as the type of
84    /// the current constant expression. Currently, this is only used
85    /// to represent `lit as *mut T` or `lit as *const T`, where `lit`
86    /// is a `usize` literal.
87    Cast {
88        source: ConstantExpr,
89    },
90    ConstRef {
91        id: ParamConst,
92    },
93    FnPtr(ItemRef),
94    /// A blob of memory containing the byte representation of the value. This can occur when
95    /// evaluating MIR constants. Interpreting this back to a structured value is left as an
96    /// exercice to the consumer.
97    Memory(Vec<u8>),
98    Todo(String),
99}
100
101#[derive_group(Serializers)]
102#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
103pub struct ConstantFieldExpr {
104    pub field: DefId,
105    pub value: ConstantExpr,
106}
107
108/// Rustc has different representation for constants: one for MIR
109/// ([`rustc_middle::mir::Const`]), one for the type system
110/// ([`rustc_middle::ty::ConstKind`]). For simplicity hax maps those
111/// two construct to one same `ConstantExpr` type.
112pub type ConstantExpr = Decorated<ConstantExprKind>;
113
114// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one
115pub type ConstantKind = ConstantExpr;
116
117#[cfg(feature = "rustc")]
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
127#[cfg(feature = "rustc")]
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                    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            ..c
192        }
193    }
194}
195
196#[cfg(feature = "rustc")]
197pub use self::uneval::*;
198#[cfg(feature = "rustc")]
199mod uneval;
hax_frontend_exporter/constant_utils.rs

hax_frontend_exporter/
constant_utils.rs
