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!(
89        tcx.def_kind(did),
90        rustc_hir::def::DefKind::AnonConst | rustc_hir::def::DefKind::InlineConst
91    )
92}
93
94/// Evaluate a `ty::Const`.
95pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
96    s: &S,
97    uv: rustc_middle::ty::UnevaluatedConst<'tcx>,
98) -> Option<ty::Const<'tcx>> {
99    use ty::TypeVisitableExt;
100    let tcx = s.base().tcx;
101    let typing_env = s.typing_env();
102    if uv.has_non_region_param() {
103        return None;
104    }
105    let span = tcx.def_span(uv.def);
106    let erased_uv = tcx.erase_and_anonymize_regions(uv);
107    let val = tcx
108        .const_eval_resolve_for_typeck(typing_env, erased_uv, span)
109        .ok()?
110        .ok()?;
111    let ty = tcx.type_of(uv.def).instantiate(tcx, uv.args);
112    let ty = normalize(tcx, typing_env, ty);
113    Some(ty::Const::new_value(tcx, val, ty))
114}
115
116impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
117    #[tracing::instrument(level = "trace", skip(s))]
118    fn sinto(&self, s: &S) -> ConstantExpr {
119        let tcx = s.base().tcx;
120        let span = rustc_span::DUMMY_SP;
121        match self.kind() {
122            ty::ConstKind::Param(p) => {
123                let ty = p.find_const_ty_from_env(s.param_env());
124                let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
125                kind.decorate(ty.sinto(s), span.sinto(s))
126            }
127            ty::ConstKind::Infer(..) => {
128                fatal!(s[span], "ty::ConstKind::Infer node? {:#?}", self)
129            }
130
131            ty::ConstKind::Unevaluated(ucv) => {
132                if s.base().options.inline_anon_consts
133                    && is_anon_const(ucv.def, tcx)
134                    && let Some(val) = eval_ty_constant(s, ucv)
135                {
136                    val.sinto(s)
137                } else {
138                    use rustc_middle::query::QueryKey;
139                    let span = tcx
140                        .def_ident_span(ucv.def)
141                        .unwrap_or_else(|| ucv.def.default_span(tcx));
142                    let item = translate_item_ref(s, ucv.def, ucv.args);
143                    let kind = ConstantExprKind::NamedGlobal(item);
144                    let ty = tcx.type_of(ucv.def).instantiate(tcx, ucv.args);
145                    let ty = normalize(tcx, s.typing_env(), ty);
146                    kind.decorate(ty.sinto(s), span.sinto(s))
147                }
148            }
149
150            ty::ConstKind::Value(val) => valtree_to_constant_expr(s, val.valtree, val.ty, span),
151            ty::ConstKind::Error(_) => fatal!(s[span], "ty::ConstKind::Error"),
152            ty::ConstKind::Expr(e) => fatal!(s[span], "ty::ConstKind::Expr {:#?}", e),
153
154            ty::ConstKind::Bound(i, bound) => {
155                supposely_unreachable_fatal!(s[span], "ty::ConstKind::Bound"; {i, bound})
156            }
157            _ => fatal!(s[span], "unexpected case"),
158        }
159    }
160}
161
162impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Value<'tcx> {
163    #[tracing::instrument(level = "trace", skip(s))]
164    fn sinto(&self, s: &S) -> ConstantExpr {
165        valtree_to_constant_expr(s, self.valtree, self.ty, rustc_span::DUMMY_SP)
166    }
167}
168
169#[tracing::instrument(level = "trace", skip(s))]
170pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
171    s: &S,
172    valtree: rustc_middle::ty::ValTree<'tcx>,
173    ty: rustc_middle::ty::Ty<'tcx>,
174    span: rustc_span::Span,
175) -> ConstantExpr {
176    let ty = normalize(s.base().tcx, s.typing_env(), ty::Unnormalized::new_wip(ty));
177
178    let kind = match (&*valtree, ty.kind()) {
179        (_, ty::Ref(_, inner_ty, _)) => {
180            ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
181        }
182        (ty::ValTreeKind::Branch(valtrees), ty::Str) => {
183            let bytes = valtrees
184                .iter()
185                .map(|x| match x.try_to_leaf() {
186                    Some(leaf) => leaf.to_u8(),
187                    None => fatal!(
188                        s[span],
189                        "Expected a flat list of leaves while translating \
190                            a str literal, got a arbitrary valtree."
191                    ),
192                })
193                .collect();
194            ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
195        }
196        (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
197            let fields = fields.iter().map(|field| field.sinto(s)).collect();
198            match ty.kind() {
199                ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
200                ty::Tuple(_) => ConstantExprKind::Tuple { fields },
201                _ => unreachable!(),
202            }
203        }
204        (ty::ValTreeKind::Branch(_), ty::Adt(def, _)) => {
205            let contents: rustc_middle::ty::DestructuredAdtConst =
206                ty::Value { valtree, ty }.destructure_adt_const();
207
208            let fields = contents.fields.iter().copied();
209            let variant_idx = contents.variant;
210            let variant_def = &def.variant(variant_idx);
211
212            ConstantExprKind::Adt {
213                kind: get_variant_kind(def, variant_idx, s),
214                fields: fields
215                    .into_iter()
216                    .zip(&variant_def.fields)
217                    .map(|(value, field)| ConstantFieldExpr {
218                        field: field.did.sinto(s),
219                        value: value.sinto(s),
220                    })
221                    .collect(),
222            }
223        }
224        (ty::ValTreeKind::Leaf(x), ty::RawPtr(_, _)) => {
225            let raw_address = x.to_bits_unchecked();
226            ConstantExprKind::Literal(ConstantLiteral::PtrNoProvenance(raw_address))
227        }
228        (ty::ValTreeKind::Leaf(x), _) => {
229            ConstantExprKind::Literal(scalar_int_to_constant_literal(s, *x, ty))
230        }
231        _ => supposely_unreachable_fatal!(
232            s[span], "valtree_to_expr";
233            {valtree, ty}
234        ),
235    };
236    kind.decorate(ty.sinto(s), span.sinto(s))
237}
238
239/// Use the const-eval interpreter to convert an evaluated operand back to a structured
240/// constant expression.
241fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
242    s: &S,
243    span: rustc_span::Span,
244    ecx: &rustc_const_eval::const_eval::CompileTimeInterpCx<'tcx>,
245    op: rustc_const_eval::interpret::OpTy<'tcx>,
246) -> InterpResult<'tcx, ConstantExpr> {
247    use rustc_const_eval::interpret::Projectable;
248    // Code inspired from `try_destructure_mir_constant_for_user_output` and
249    // `const_eval::eval_queries::op_to_const`.
250    let tcx = s.base().tcx;
251    let ty = op.layout.ty;
252    // Helper for struct-likes.
253    let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| {
254        (0..field_count).map(move |i| {
255            let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?;
256            op_to_const(s, span, ecx, field_op)
257        })
258    };
259    let kind = match ty.kind() {
260        // Detect statics
261        _ if let Some(place) = op.as_mplace_or_imm().left()
262            && let ptr = place.ptr()
263            && let (alloc_id, _, _) = ecx.ptr_get_alloc_id(ptr, 0)?
264            && let interpret::GlobalAlloc::Static(did) = tcx.global_alloc(alloc_id) =>
265        {
266            let item = translate_item_ref(s, did, ty::GenericArgsRef::default());
267            ConstantExprKind::NamedGlobal(item)
268        }
269        ty::Char | ty::Bool | ty::Uint(_) | ty::Int(_) | ty::Float(_) => {
270            let scalar = ecx.read_scalar(&op)?;
271            let scalar_int = scalar.try_to_scalar_int().unwrap();
272            let lit = scalar_int_to_constant_literal(s, scalar_int, ty);
273            ConstantExprKind::Literal(lit)
274        }
275        ty::Adt(adt_def, ..) if adt_def.is_union() => {
276            ConstantExprKind::Todo("Cannot translate constant of union type".into())
277        }
278        ty::Adt(adt_def, ..) => {
279            let variant = ecx.read_discriminant(&op)?;
280            let op = if adt_def.is_enum() {
281                ecx.project_downcast(&op, variant)?
282            } else {
283                op
284            };
285            let field_count = adt_def.variants()[variant].fields.len();
286            let fields = read_fields(op, 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::Pat(..) => {
371            let op = ecx.project_field(&op, FieldIdx::from_u16(0))?;
372            *op_to_const(s, span, ecx, op)?.contents
373        }
374        ty::Dynamic(..)
375        | ty::Foreign(..)
376        | ty::UnsafeBinder(..)
377        | ty::CoroutineClosure(..)
378        | ty::Coroutine(..)
379        | ty::CoroutineWitness(..) => ConstantExprKind::Todo("Unhandled constant type".into()),
380        ty::Alias(..) | ty::Param(..) | ty::Bound(..) | ty::Placeholder(..) | ty::Infer(..) => {
381            fatal!(s[span], "Encountered evaluated constant of non-monomorphic type"; {op})
382        }
383        ty::Never | ty::Error(..) => {
384            fatal!(s[span], "Encountered evaluated constant of invalid type"; {ty})
385        }
386    };
387    let val = kind.decorate(ty.sinto(s), span.sinto(s));
388    interp_ok(val)
389}
390
391pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
392    s: &S,
393    ty: rustc_middle::ty::Ty<'tcx>,
394    val: mir::ConstValue,
395    span: rustc_span::Span,
396) -> InterpResult<'tcx, ConstantExpr> {
397    let tcx = s.base().tcx;
398    let typing_env = s.typing_env();
399    let (ecx, op) =
400        rustc_const_eval::const_eval::mk_eval_cx_for_const_val(tcx.at(span), typing_env, val, ty)
401            .unwrap();
402    op_to_const(s, span, &ecx, op)
403}
charon_driver/hax/constant_utils/uneval.rs

charon_driver/hax/constant_utils/
uneval.rs
