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
118#[cfg(feature = "rustc")]
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
128#[cfg(feature = "rustc")]
129impl From<ConstantExpr> for Expr {
130    fn from(c: ConstantExpr) -> Expr {
131        use ConstantExprKind::*;
132        let kind = match *c.contents {
133            Literal(lit) => {
134                use ConstantLiteral::*;
135                let mut neg = false;
136                let node = match lit {
137                    Bool(b) => LitKind::Bool(b),
138                    Char(c) => LitKind::Char(c),
139                    Int(i) => {
140                        use LitIntType::*;
141                        match i {
142                            ConstantInt::Uint(v, t) => LitKind::Int(v, Unsigned(t)),
143                            ConstantInt::Int(v, t) => {
144                                neg = v.is_negative();
145                                LitKind::Int(v.abs_diff(0), Signed(t))
146                            }
147                        }
148                    }
149                    Float(f, ty) => LitKind::Float(f, LitFloatType::Suffixed(ty)),
150                    PtrNoProvenance(p) => LitKind::Int(p, LitIntType::Unsigned(UintTy::Usize)),
151                    ByteStr(raw) => LitKind::ByteStr(raw, StrStyle::Cooked),
152                    Str(raw) => LitKind::Str(raw, StrStyle::Cooked),
153                };
154                let span = c.span.clone();
155                let lit = Spanned { span, node };
156                ExprKind::Literal { lit, neg }
157            }
158            Adt { info, fields } => ExprKind::Adt(AdtExpr {
159                info,
160                fields: fields.into_iter().map(|field| field.into()).collect(),
161                base: AdtExprBase::None,
162                user_ty: None,
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            ..c
194        }
195    }
196}
197
198#[cfg(feature = "rustc")]
199pub use self::uneval::*;
200#[cfg(feature = "rustc")]
201mod uneval;
hax_frontend_exporter/constant_utils.rs

hax_frontend_exporter/
constant_utils.rs
