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

charon_driver/hax/constant_utils/
uneval.rs
