charon_driver/hax/constant_utils/
uneval.rs

1//! Reconstruct structured expressions from rustc's various constant representations.
2use super::*;
3use rustc_const_eval::interpret::{FnVal, InterpResult, interp_ok};
4use rustc_middle::mir::interpret;
5use rustc_middle::{mir, ty};
6
7impl ConstantLiteral {
8    /// Rustc always represents string constants as `&[u8]`, but this
9    /// is not nice to consume. This associated function interpret
10    /// bytes as an unicode string, and as a byte string otherwise.
11    fn byte_str(bytes: Vec<u8>) -> Self {
12        match String::from_utf8(bytes.clone()) {
13            Ok(s) => Self::Str(s),
14            Err(_) => Self::ByteStr(bytes),
15        }
16    }
17}
18
19#[tracing::instrument(level = "trace", skip(s))]
20pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
21    s: &S,
22    x: rustc_middle::ty::ScalarInt,
23    ty: rustc_middle::ty::Ty<'tcx>,
24) -> ConstantLiteral {
25    match ty.kind() {
26        ty::Char => ConstantLiteral::Char(
27            char::try_from(x).s_expect(s, "scalar_int_to_constant_literal: expected a char"),
28        ),
29        ty::Bool => ConstantLiteral::Bool(
30            x.try_to_bool()
31                .s_expect(s, "scalar_int_to_constant_literal: expected a bool"),
32        ),
33        ty::Int(kind) => {
34            let v = x.to_int(x.size());
35            ConstantLiteral::Int(ConstantInt::Int(v, kind.sinto(s)))
36        }
37        ty::Uint(kind) => {
38            let v = x.to_uint(x.size());
39            ConstantLiteral::Int(ConstantInt::Uint(v, kind.sinto(s)))
40        }
41        ty::Float(kind) => {
42            let v = x.to_bits_unchecked();
43            bits_and_type_to_float_constant_literal(v, kind.sinto(s))
44        }
45        ty::Pat(inner, _) => scalar_int_to_constant_literal(s, x, *inner),
46        _ => {
47            let ty_sinto: Ty = ty.sinto(s);
48            supposely_unreachable_fatal!(
49                s,
50                "scalar_int_to_constant_literal_ExpectedLiteralType";
51                { ty, ty_sinto, x }
52            )
53        }
54    }
55}
56
57/// Converts a bit-representation of a float of type `ty` to a constant literal
58fn bits_and_type_to_float_constant_literal(bits: u128, ty: FloatTy) -> ConstantLiteral {
59    use rustc_apfloat::{Float, ieee};
60    let string = match &ty {
61        FloatTy::F16 => ieee::Half::from_bits(bits).to_string(),
62        FloatTy::F32 => ieee::Single::from_bits(bits).to_string(),
63        FloatTy::F64 => ieee::Double::from_bits(bits).to_string(),
64        FloatTy::F128 => ieee::Quad::from_bits(bits).to_string(),
65    };
66    ConstantLiteral::Float(string, ty)
67}
68
69impl ConstantExprKind {
70    pub fn decorate(self, ty: Ty, _span: Span) -> Decorated<Self> {
71        Decorated {
72            contents: Box::new(self),
73            ty,
74        }
75    }
76}
77
78/// Whether a `DefId` is a `AnonConst`. An anonymous constant is
79/// generated by Rustc, hoisting every constat bits from items as
80/// separate top-level items. This AnonConst mechanism is internal to
81/// Rustc; we don't want to reflect that, instead we prefer inlining
82/// those. `is_anon_const` is used to detect such AnonConst so that we
83/// can evaluate and inline them.
84pub(crate) fn is_anon_const(
85    did: rustc_span::def_id::DefId,
86    tcx: rustc_middle::ty::TyCtxt<'_>,
87) -> bool {
88    matches!(tcx.def_kind(did), rustc_hir::def::DefKind::AnonConst)
89}
90
91/// Evaluate a `ty::Const`.
92pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
93    s: &S,
94    uv: rustc_middle::ty::AliasConst<'tcx>,
95) -> Option<ty::Const<'tcx>> {
96    use ty::TypeVisitableExt;
97    let tcx = s.base().tcx;
98    let typing_env = s.typing_env();
99    if uv.has_non_region_param() {
100        return None;
101    }
102    let def = uv.kind.opt_def_id().unwrap();
103    let span = tcx.def_span(def);
104    let erased_uv = tcx.erase_and_anonymize_regions(uv);
105    let val = tcx
106        .const_eval_resolve_for_typeck(typing_env, erased_uv, span)
107        .ok()?
108        .ok()?;
109    let ty = tcx.type_of(def).instantiate(tcx, uv.args);
110    let ty = normalize(tcx, typing_env, ty);
111    Some(ty::Const::new_value(tcx, val, ty))
112}
113
114impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
115    #[tracing::instrument(level = "trace", skip(s))]
116    fn sinto(&self, s: &S) -> ConstantExpr {
117        let tcx = s.base().tcx;
118        let span = rustc_span::DUMMY_SP;
119        match self.kind() {
120            ty::ConstKind::Param(p) => {
121                let ty = p.find_const_ty_from_env(s.param_env());
122                let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
123                kind.decorate(ty.sinto(s), span.sinto(s))
124            }
125            ty::ConstKind::Infer(..) => {
126                fatal!(s[span], "ty::ConstKind::Infer node? {:#?}", self)
127            }
128
129            ty::ConstKind::Alias(_, ucv) => {
130                let def = ucv
131                    .kind
132                    .opt_def_id()
133                    .expect("AliasConstKind with no def id?");
134                if s.base().options.inline_anon_consts
135                    && is_anon_const(def, tcx)
136                    && let Some(val) = eval_ty_constant(s, ucv)
137                {
138                    val.sinto(s)
139                } else {
140                    use rustc_middle::query::QueryKey;
141                    let span = tcx
142                        .def_ident_span(def)
143                        .unwrap_or_else(|| def.default_span(tcx));
144                    let item = translate_item_ref(s, def, ucv.args);
145                    let kind = ConstantExprKind::NamedGlobal(item);
146                    let ty = tcx.type_of(def).instantiate(tcx, ucv.args);
147                    let ty = normalize(tcx, s.typing_env(), ty);
148                    kind.decorate(ty.sinto(s), span.sinto(s))
149                }
150            }
151
152            ty::ConstKind::Value(val) => valtree_to_constant_expr(s, val.valtree, val.ty, span),
153            ty::ConstKind::Error(_) => fatal!(s[span], "ty::ConstKind::Error"),
154            ty::ConstKind::Expr(e) => fatal!(s[span], "ty::ConstKind::Expr {:#?}", e),
155
156            ty::ConstKind::Bound(i, bound) => {
157                supposely_unreachable_fatal!(s[span], "ty::ConstKind::Bound"; {i, bound})
158            }
159            _ => fatal!(s[span], "unexpected case"),
160        }
161    }
162}
163
164impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Value<'tcx> {
165    #[tracing::instrument(level = "trace", skip(s))]
166    fn sinto(&self, s: &S) -> ConstantExpr {
167        valtree_to_constant_expr(s, self.valtree, self.ty, rustc_span::DUMMY_SP)
168    }
169}
170
171#[tracing::instrument(level = "trace", skip(s))]
172pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
173    s: &S,
174    valtree: rustc_middle::ty::ValTree<'tcx>,
175    ty: rustc_middle::ty::Ty<'tcx>,
176    span: rustc_span::Span,
177) -> ConstantExpr {
178    let ty = normalize(s.base().tcx, s.typing_env(), ty::Unnormalized::new_wip(ty));
179
180    let kind = match (&*valtree, ty.kind()) {
181        (_, ty::Ref(_, inner_ty, _)) => {
182            ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
183        }
184        (ty::ValTreeKind::Branch(valtrees), ty::Str) => {
185            let bytes = valtrees
186                .iter()
187                .map(|x| match x.try_to_leaf() {
188                    Some(leaf) => leaf.to_u8(),
189                    None => fatal!(
190                        s[span],
191                        "Expected a flat list of leaves while translating \
192                            a str literal, got a arbitrary valtree."
193                    ),
194                })
195                .collect();
196            ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
197        }
198        (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
199            let fields = fields.iter().map(|field| field.sinto(s)).collect();
200            match ty.kind() {
201                ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
202                ty::Tuple(_) => ConstantExprKind::Tuple { fields },
203                _ => unreachable!(),
204            }
205        }
206        (ty::ValTreeKind::Branch(_), ty::Adt(def, _)) => {
207            let contents: rustc_middle::ty::DestructuredAdtConst =
208                ty::Value { valtree, ty }.destructure_adt_const();
209
210            let fields = contents.fields.iter().copied();
211            let variant_idx = contents.variant;
212            let variant_def = &def.variant(variant_idx);
213
214            ConstantExprKind::Adt {
215                kind: get_variant_kind(def, variant_idx, s),
216                fields: fields
217                    .into_iter()
218                    .zip(&variant_def.fields)
219                    .map(|(value, field)| ConstantFieldExpr {
220                        field: field.did.sinto(s),
221                        value: value.sinto(s),
222                    })
223                    .collect(),
224            }
225        }
226        (ty::ValTreeKind::Leaf(x), ty::RawPtr(_, _)) => {
227            let raw_address = x.to_bits_unchecked();
228            ConstantExprKind::Literal(ConstantLiteral::PtrNoProvenance(raw_address))
229        }
230        (ty::ValTreeKind::Leaf(x), _) => {
231            ConstantExprKind::Literal(scalar_int_to_constant_literal(s, *x, ty))
232        }
233        _ => supposely_unreachable_fatal!(
234            s[span], "valtree_to_expr";
235            {valtree, ty}
236        ),
237    };
238    kind.decorate(ty.sinto(s), span.sinto(s))
239}
240
241/// Use the const-eval interpreter to convert an evaluated operand back to a structured
242/// constant expression.
243fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
244    s: &S,
245    span: rustc_span::Span,
246    ecx: &rustc_const_eval::const_eval::CompileTimeInterpCx<'tcx>,
247    op: rustc_const_eval::interpret::OpTy<'tcx>,
248) -> InterpResult<'tcx, ConstantExpr> {
249    use rustc_const_eval::interpret::Projectable;
250    // Code inspired from `try_destructure_mir_constant_for_user_output` and
251    // `const_eval::eval_queries::op_to_const`.
252    let tcx = s.base().tcx;
253    let ty = op.layout.ty;
254    // Helper for struct-likes.
255    let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| {
256        (0..field_count).map(move |i| {
257            let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?;
258            op_to_const(s, span, ecx, field_op)
259        })
260    };
261    let kind = match ty.kind() {
262        // Detect statics
263        _ if let Some(place) = op.as_mplace_or_imm().left()
264            && let ptr = place.ptr()
265            && let (alloc_id, _, _) = ecx.ptr_get_alloc_id(ptr, 0)?
266            && let interpret::GlobalAlloc::Static(did) = tcx.global_alloc(alloc_id) =>
267        {
268            let item = translate_item_ref(s, did, ty::GenericArgsRef::default());
269            ConstantExprKind::NamedGlobal(item)
270        }
271        ty::Char | ty::Bool | ty::Uint(_) | ty::Int(_) | ty::Float(_) => {
272            let scalar = ecx.read_scalar(&op)?;
273            let scalar_int = scalar.try_to_scalar_int().unwrap();
274            let lit = scalar_int_to_constant_literal(s, scalar_int, ty);
275            ConstantExprKind::Literal(lit)
276        }
277        ty::Adt(adt_def, ..) if adt_def.is_union() => {
278            ConstantExprKind::Todo("Cannot translate constant of union type".into())
279        }
280        ty::Adt(adt_def, ..) => {
281            let variant = ecx.read_discriminant(&op)?;
282            let op = if adt_def.is_enum() {
283                ecx.project_downcast(&op, variant)?
284            } else {
285                op
286            };
287            let field_count = adt_def.variants()[variant].fields.len();
288            let fields = read_fields(op, field_count)
289                .zip(&adt_def.variant(variant).fields)
290                .map(|(value, field)| {
291                    interp_ok(ConstantFieldExpr {
292                        field: field.did.sinto(s),
293                        value: value?,
294                    })
295                })
296                .collect::<InterpResult<Vec<_>>>()?;
297            ConstantExprKind::Adt {
298                kind: get_variant_kind(adt_def, variant, s),
299                fields,
300            }
301        }
302        ty::Closure(def_id, args) => {
303            // A closure is essentially an adt with funky generics and some builtin impls.
304            let def_id: DefId = def_id.sinto(s);
305            let field_count = args.as_closure().upvar_tys().len();
306            let fields = read_fields(op, field_count)
307                .map(|value| {
308                    interp_ok(ConstantFieldExpr {
309                        // HACK: Closure fields don't have their own def_id, but Charon doesn't use
310                        // field DefIds so we put a dummy one.
311                        field: def_id.clone(),
312                        value: value?,
313                    })
314                })
315                .collect::<InterpResult<Vec<_>>>()?;
316            ConstantExprKind::Adt {
317                kind: VariantKind::Struct,
318                fields,
319            }
320        }
321        ty::Tuple(args) => {
322            let fields = read_fields(op, args.len()).collect::<InterpResult<Vec<_>>>()?;
323            ConstantExprKind::Tuple { fields }
324        }
325        ty::Array(..) | ty::Slice(..) => {
326            let len = op.len(ecx)?;
327            let fields = (0..len)
328                .map(|i| {
329                    let op = ecx.project_index(&op, i)?;
330                    op_to_const(s, span, ecx, op)
331                })
332                .collect::<InterpResult<Vec<_>>>()?;
333            ConstantExprKind::Array { fields }
334        }
335        ty::Str => {
336            let str = ecx.read_str(&op.assert_mem_place())?;
337            ConstantExprKind::Literal(ConstantLiteral::Str(str.to_owned()))
338        }
339        ty::FnDef(def_id, args) => {
340            let args = args.no_bound_vars().expect("bound variables in FnDef");
341            let item = translate_item_ref(s, *def_id, args);
342            ConstantExprKind::FnDef(item)
343        }
344        ty::FnPtr(..) => {
345            let fn_ptr = ecx.read_pointer(&op)?;
346            let FnVal::Instance(instance) = ecx.get_ptr_fn(fn_ptr)?;
347            let def_id = instance.def_id();
348            let generics = instance.args;
349            let fun = translate_item_ref(s, def_id, generics);
350            ConstantExprKind::FnPtr(fun)
351        }
352        ty::RawPtr(..) | ty::Ref(..) => {
353            if let Some(op) = ecx.deref_pointer(&op).discard_err() {
354                // Valid pointer case
355                let val = op_to_const(s, span, ecx, op.into())?;
356                match ty.kind() {
357                    ty::Ref(..) => ConstantExprKind::Borrow(val),
358                    ty::RawPtr(.., mutability) => ConstantExprKind::RawBorrow {
359                        arg: val,
360                        mutability: mutability.sinto(s),
361                    },
362                    _ => unreachable!(),
363                }
364            } else {
365                // Invalid pointer; try reading it as a raw address
366                let scalar = ecx.read_scalar(&op)?;
367                let scalar_int = scalar.try_to_scalar_int().unwrap();
368                let v = scalar_int.to_uint(scalar_int.size());
369                let lit = ConstantLiteral::PtrNoProvenance(v);
370                ConstantExprKind::Literal(lit)
371            }
372        }
373        ty::Pat(..) => {
374            let op = ecx.project_field(&op, FieldIdx::from_u16(0))?;
375            *op_to_const(s, span, ecx, op)?.contents
376        }
377        ty::Dynamic(..)
378        | ty::Foreign(..)
379        | ty::UnsafeBinder(..)
380        | ty::CoroutineClosure(..)
381        | ty::Coroutine(..)
382        | ty::CoroutineWitness(..) => ConstantExprKind::Todo("Unhandled constant type".into()),
383        ty::Alias(..) | ty::Param(..) | ty::Bound(..) | ty::Placeholder(..) | ty::Infer(..) => {
384            fatal!(s[span], "Encountered evaluated constant of non-monomorphic type"; {op})
385        }
386        ty::Never | ty::Error(..) => {
387            fatal!(s[span], "Encountered evaluated constant of invalid type"; {ty})
388        }
389    };
390    let val = kind.decorate(ty.sinto(s), span.sinto(s));
391    interp_ok(val)
392}
393
394pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
395    s: &S,
396    ty: rustc_middle::ty::Ty<'tcx>,
397    val: mir::ConstValue,
398    span: rustc_span::Span,
399) -> InterpResult<'tcx, ConstantExpr> {
400    let tcx = s.base().tcx;
401    let typing_env = s.typing_env();
402    let (ecx, op) =
403        rustc_const_eval::const_eval::mk_eval_cx_for_const_val(tcx.at(span), typing_env, val, ty)
404            .unwrap();
405    op_to_const(s, span, &ecx, op)
406}
charon_driver/hax/constant_utils/uneval.rs

charon_driver/hax/constant_utils/
uneval.rs
