charon_driver/hax/constant_utils/
uneval.rs

1//! Reconstruct structured expressions from rustc's various constant representations.
2use super::*;
3use rustc_const_eval::const_eval;
4use rustc_const_eval::interpret::{FnVal, InterpResult, interp_ok};
5use rustc_middle::mir::interpret;
6use rustc_middle::{mir, ty};
7
8impl ConstantLiteral {
9    /// Rustc always represents string constants as `&[u8]`, but this
10    /// is not nice to consume. This associated function interpret
11    /// bytes as an unicode string, and as a byte string otherwise.
12    fn byte_str(bytes: Vec<u8>) -> Self {
13        match String::from_utf8(bytes.clone()) {
14            Ok(s) => Self::Str(s),
15            Err(_) => Self::ByteStr(bytes),
16        }
17    }
18}
19
20#[tracing::instrument(level = "trace", skip(s))]
21pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
22    s: &S,
23    x: rustc_middle::ty::ScalarInt,
24    ty: rustc_middle::ty::Ty<'tcx>,
25) -> ConstantLiteral {
26    match ty.kind() {
27        ty::Char => ConstantLiteral::Char(
28            char::try_from(x).s_expect(s, "scalar_int_to_constant_literal: expected a char"),
29        ),
30        ty::Bool => ConstantLiteral::Bool(
31            x.try_to_bool()
32                .s_expect(s, "scalar_int_to_constant_literal: expected a bool"),
33        ),
34        ty::Int(kind) => {
35            let v = x.to_int(x.size());
36            ConstantLiteral::Int(ConstantInt::Int(v, kind.sinto(s)))
37        }
38        ty::Uint(kind) => {
39            let v = x.to_uint(x.size());
40            ConstantLiteral::Int(ConstantInt::Uint(v, kind.sinto(s)))
41        }
42        ty::Float(kind) => {
43            let v = x.to_bits_unchecked();
44            bits_and_type_to_float_constant_literal(v, kind.sinto(s))
45        }
46        ty::Pat(inner, _) => scalar_int_to_constant_literal(s, x, *inner),
47        _ => {
48            let ty_sinto: Ty = ty.sinto(s);
49            supposely_unreachable_fatal!(
50                s,
51                "scalar_int_to_constant_literal_ExpectedLiteralType";
52                { ty, ty_sinto, x }
53            )
54        }
55    }
56}
57
58/// Converts a bit-representation of a float of type `ty` to a constant literal
59fn bits_and_type_to_float_constant_literal(bits: u128, ty: FloatTy) -> ConstantLiteral {
60    use rustc_apfloat::{Float, ieee};
61    let string = match &ty {
62        FloatTy::F16 => ieee::Half::from_bits(bits).to_string(),
63        FloatTy::F32 => ieee::Single::from_bits(bits).to_string(),
64        FloatTy::F64 => ieee::Double::from_bits(bits).to_string(),
65        FloatTy::F128 => ieee::Quad::from_bits(bits).to_string(),
66    };
67    ConstantLiteral::Float(string, ty)
68}
69
70impl ConstantExprKind {
71    pub fn decorate(self, ty: Ty, _span: Span) -> Decorated<Self> {
72        Decorated {
73            contents: Box::new(self),
74            ty,
75        }
76    }
77}
78
79/// Whether a `DefId` is a `AnonConst`. An anonymous constant is
80/// generated by Rustc, hoisting every constat bits from items as
81/// separate top-level items. This AnonConst mechanism is internal to
82/// Rustc; we don't want to reflect that, instead we prefer inlining
83/// those. `is_anon_const` is used to detect such AnonConst so that we
84/// can evaluate and inline them.
85pub(crate) fn is_anon_const(
86    did: rustc_span::def_id::DefId,
87    tcx: rustc_middle::ty::TyCtxt<'_>,
88) -> bool {
89    matches!(tcx.def_kind(did), rustc_hir::def::DefKind::AnonConst)
90}
91
92/// Evaluate a `ty::Const`.
93pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
94    s: &S,
95    uv: rustc_middle::ty::AliasConst<'tcx>,
96) -> Option<ty::Const<'tcx>> {
97    use ty::TypeVisitableExt;
98    let tcx = s.base().tcx;
99    let typing_env = s.typing_env();
100    if uv.has_non_region_param() {
101        return None;
102    }
103    let def = uv.kind.opt_def_id().unwrap();
104    let span = tcx.def_span(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(def).instantiate(tcx, uv.args);
111    let ty = normalize(tcx, typing_env, ty);
112    Some(ty::Const::new_value(tcx, val, ty))
113}
114
115impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
116    #[tracing::instrument(level = "trace", skip(s))]
117    fn sinto(&self, s: &S) -> ConstantExpr {
118        let tcx = s.base().tcx;
119        let span = rustc_span::DUMMY_SP;
120        match self.kind() {
121            ty::ConstKind::Param(p) => {
122                let ty = p.find_const_ty_from_env(s.param_env());
123                let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
124                kind.decorate(ty.sinto(s), span.sinto(s))
125            }
126            ty::ConstKind::Infer(..) => {
127                fatal!(s[span], "ty::ConstKind::Infer node? {:#?}", self)
128            }
129
130            ty::ConstKind::Alias(_, ucv) => {
131                let def = ucv
132                    .kind
133                    .opt_def_id()
134                    .expect("AliasConstKind with no def id?");
135                if s.base().options.inline_anon_consts
136                    && is_anon_const(def, tcx)
137                    && let Some(val) = eval_ty_constant(s, ucv)
138                {
139                    val.sinto(s)
140                } else {
141                    use rustc_middle::query::QueryKey;
142                    let span = tcx
143                        .def_ident_span(def)
144                        .unwrap_or_else(|| def.default_span(tcx));
145                    let item = translate_item_ref(s, def, ucv.args);
146                    let kind = ConstantExprKind::NamedGlobal(item);
147                    let ty = tcx.type_of(def).instantiate(tcx, ucv.args);
148                    let ty = normalize(tcx, s.typing_env(), ty);
149                    kind.decorate(ty.sinto(s), span.sinto(s))
150                }
151            }
152
153            ty::ConstKind::Value(val) => valtree_to_constant_expr(s, val.valtree, val.ty, span),
154            ty::ConstKind::Error(_) => fatal!(s[span], "ty::ConstKind::Error"),
155            ty::ConstKind::Expr(e) => fatal!(s[span], "ty::ConstKind::Expr {:#?}", e),
156
157            ty::ConstKind::Bound(i, bound) => {
158                supposely_unreachable_fatal!(s[span], "ty::ConstKind::Bound"; {i, bound})
159            }
160            _ => fatal!(s[span], "unexpected case"),
161        }
162    }
163}
164
165impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Value<'tcx> {
166    #[tracing::instrument(level = "trace", skip(s))]
167    fn sinto(&self, s: &S) -> ConstantExpr {
168        valtree_to_constant_expr(s, self.valtree, self.ty, rustc_span::DUMMY_SP)
169    }
170}
171
172#[tracing::instrument(level = "trace", skip(s))]
173pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
174    s: &S,
175    valtree: rustc_middle::ty::ValTree<'tcx>,
176    ty: rustc_middle::ty::Ty<'tcx>,
177    span: rustc_span::Span,
178) -> ConstantExpr {
179    let ty = normalize(s.base().tcx, s.typing_env(), ty::Unnormalized::new_wip(ty));
180
181    let kind = match (&*valtree, ty.kind()) {
182        (_, ty::Ref(_, inner_ty, _)) => {
183            ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
184        }
185        (ty::ValTreeKind::Branch(valtrees), ty::Str) => {
186            let bytes = valtrees
187                .iter()
188                .map(|x| match x.try_to_leaf() {
189                    Some(leaf) => leaf.to_u8(),
190                    None => fatal!(
191                        s[span],
192                        "Expected a flat list of leaves while translating \
193                            a str literal, got a arbitrary valtree."
194                    ),
195                })
196                .collect();
197            ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
198        }
199        (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
200            let fields = fields.iter().map(|field| field.sinto(s)).collect();
201            match ty.kind() {
202                ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
203                ty::Tuple(_) => ConstantExprKind::Tuple { fields },
204                _ => unreachable!(),
205            }
206        }
207        (ty::ValTreeKind::Branch(_), ty::Adt(def, _)) => {
208            let contents: rustc_middle::ty::DestructuredAdtConst =
209                ty::Value { valtree, ty }.destructure_adt_const();
210
211            let fields = contents.fields.iter().copied();
212            let variant_idx = contents.variant;
213            let variant_def = &def.variant(variant_idx);
214
215            ConstantExprKind::Adt {
216                kind: get_variant_kind(def, variant_idx, s),
217                fields: fields
218                    .into_iter()
219                    .zip(&variant_def.fields)
220                    .map(|(value, field)| ConstantFieldExpr {
221                        field: field.did.sinto(s),
222                        value: value.sinto(s),
223                    })
224                    .collect(),
225            }
226        }
227        (ty::ValTreeKind::Leaf(x), ty::RawPtr(_, _)) => {
228            let raw_address = x.to_bits_unchecked();
229            ConstantExprKind::Literal(ConstantLiteral::PtrNoProvenance(raw_address))
230        }
231        (ty::ValTreeKind::Leaf(x), _) => {
232            ConstantExprKind::Literal(scalar_int_to_constant_literal(s, *x, ty))
233        }
234        _ => supposely_unreachable_fatal!(
235            s[span], "valtree_to_expr";
236            {valtree, ty}
237        ),
238    };
239    kind.decorate(ty.sinto(s), span.sinto(s))
240}
241
242/// The provenance to give to the bytes of a pointer into the given allocation.
243fn alloc_provenance<'tcx, S: UnderOwnerState<'tcx>>(
244    s: &S,
245    alloc_id: interpret::AllocId,
246) -> ConstantByteProvenance {
247    use interpret::GlobalAlloc::*;
248    let tcx = s.base().tcx;
249    match tcx.global_alloc(alloc_id) {
250        Function { instance } => ConstantByteProvenance::Function(translate_item_ref(
251            s,
252            instance.def_id(),
253            instance.args,
254        )),
255        // TODO: nested statics are synthetic items that make the rest of the machinery ICE, so we
256        // don't turn them into named globals yet.
257        Static(did)
258            if let rustc_hir::def::DefKind::Static { nested: false, .. } = tcx.def_kind(did) =>
259        {
260            ConstantByteProvenance::Global(translate_item_ref(s, did, Default::default()))
261        }
262        // TODO: TypeIds, anonymous allocations.
263        // VTables are not reachable here, I believe: it's UB to attempt reading a VTable's data.
264        _ => ConstantByteProvenance::Unknown,
265    }
266}
267
268/// Read the raw bytes of an evaluated operand, keeping track of uninitialized bytes and pointer
269/// provenance. Used for values that have no structured representation (e.g. unions).
270fn op_to_raw_bytes<'tcx, S: UnderOwnerState<'tcx>>(
271    s: &S,
272    ecx: &const_eval::CompileTimeInterpCx<'tcx>,
273    op: &rustc_const_eval::interpret::OpTy<'tcx>,
274) -> InterpResult<'tcx, Vec<ConstantByte>> {
275    op.as_mplace_or_imm().either(
276        |mplace| mplace_to_raw_bytes(s, ecx, &mplace),
277        |imm| interp_ok(imm_to_raw_bytes(s, &imm)),
278    )
279}
280
281/// The bytes of an immediate, which is made of at most two scalars.
282fn imm_to_raw_bytes<'tcx, S: UnderOwnerState<'tcx>>(
283    s: &S,
284    imm: &rustc_const_eval::interpret::ImmTy<'tcx>,
285) -> Vec<ConstantByte> {
286    use rustc_abi::Size;
287    use rustc_const_eval::interpret::Immediate;
288    let mut bytes = vec![ConstantByte::Uninit; imm.layout.size.bytes_usize()];
289    let mut write = |offset: Size, scalar: interpret::Scalar| {
290        match scalar {
291            interpret::Scalar::Int(int) => {
292                let mut scalar = vec![0; int.size().bytes_usize()];
293                let endian = s.base().tcx.data_layout.endian;
294                interpret::write_target_uint(endian, &mut scalar, int.to_bits(int.size())).unwrap();
295                for (i, b) in scalar.into_iter().enumerate() {
296                    bytes[offset.bytes_usize() + i] = ConstantByte::Value(b);
297                }
298            }
299            interpret::Scalar::Ptr(ptr, size) => {
300                let prov = alloc_provenance(s, ptr.provenance.alloc_id());
301                for i in 0..size {
302                    bytes[offset.bytes_usize() + i as usize] =
303                        ConstantByte::Provenance(prov.clone(), i);
304                }
305            }
306        };
307    };
308    match **imm {
309        Immediate::Uninit => {}
310        Immediate::Scalar(a) => write(Size::ZERO, a),
311        Immediate::ScalarPair(a, b) => {
312            let rustc_abi::BackendRepr::ScalarPair { b_offset, .. } = imm.layout.backend_repr
313            else {
314                unreachable!()
315            };
316            write(Size::ZERO, a);
317            write(b_offset, b);
318        }
319    }
320    bytes
321}
322
323/// The bytes of a value in memory.
324fn mplace_to_raw_bytes<'tcx, S: UnderOwnerState<'tcx>>(
325    s: &S,
326    ecx: &const_eval::CompileTimeInterpCx<'tcx>,
327    mplace: &rustc_const_eval::interpret::MPlaceTy<'tcx>,
328) -> InterpResult<'tcx, Vec<ConstantByte>> {
329    use rustc_abi::Size;
330    let size = mplace.layout.size;
331    if size.bytes() == 0 {
332        return interp_ok(vec![]);
333    }
334    let (alloc_id, offset, _) = ecx.ptr_get_alloc_id(mplace.ptr(), size.bytes() as i64)?;
335    let alloc = ecx.get_alloc_raw(alloc_id)?;
336    let range = interpret::alloc_range(offset, size);
337    let raw_bytes = alloc.get_bytes_unchecked(range);
338    let mut bytes: Vec<ConstantByte> = (0..size.bytes())
339        .map(
340            |i| match alloc.init_mask().get(offset + Size::from_bytes(i)) {
341                true => ConstantByte::Value(raw_bytes[i as usize]),
342                false => ConstantByte::Uninit,
343            },
344        )
345        .collect();
346
347    for (prov_range, prov) in alloc.provenance().get_range(range, ecx) {
348        let prov = alloc_provenance(s, prov.alloc_id());
349        for i in 0..prov_range.size.bytes() {
350            let pos = prov_range.start + Size::from_bytes(i);
351            if range.start <= pos && pos < range.end() {
352                bytes[(pos - range.start).bytes_usize()] =
353                    ConstantByte::Provenance(prov.clone(), i as u8);
354            }
355        }
356    }
357    interp_ok(bytes)
358}
359
360/// Use the const-eval interpreter to convert an evaluated operand back to a structured
361/// constant expression.
362fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
363    s: &S,
364    span: rustc_span::Span,
365    ecx: &const_eval::CompileTimeInterpCx<'tcx>,
366    op: rustc_const_eval::interpret::OpTy<'tcx>,
367) -> InterpResult<'tcx, ConstantExpr> {
368    use rustc_const_eval::interpret::Projectable;
369    // Code inspired from `try_destructure_mir_constant_for_user_output` and
370    // `const_eval::eval_queries::op_to_const`.
371    let tcx = s.base().tcx;
372    let ty = op.layout.ty;
373    // Helper for struct-likes.
374    let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| {
375        (0..field_count).map(move |i| {
376            let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?;
377            op_to_const(s, span, ecx, field_op)
378        })
379    };
380    let kind = match ty.kind() {
381        // Preserve references to statics. Nested statics are are synthetic items that make the
382        // rest of the machinery ICE, so we don't turn them into named globals here.
383        _ if let Some(place) = op.as_mplace_or_imm().left()
384            && let ptr = place.ptr()
385            && let Some((alloc_id, _, _)) = ecx.ptr_get_alloc_id(ptr, 0).discard_err()
386            && let interpret::GlobalAlloc::Static(did) = tcx.global_alloc(alloc_id)
387            && let rustc_hir::def::DefKind::Static { nested: false, .. } = tcx.def_kind(did) =>
388        {
389            let item = translate_item_ref(s, did, ty::GenericArgsRef::default());
390            ConstantExprKind::NamedGlobal(item)
391        }
392        ty::Char | ty::Bool | ty::Uint(_) | ty::Int(_) | ty::Float(_) => {
393            let scalar = ecx.read_scalar(&op)?;
394            let scalar_int = scalar.try_to_scalar_int().unwrap();
395            let lit = scalar_int_to_constant_literal(s, scalar_int, ty);
396            ConstantExprKind::Literal(lit)
397        }
398        ty::Adt(adt_def, ..) if adt_def.is_union() => {
399            ConstantExprKind::Memory(op_to_raw_bytes(s, ecx, &op)?)
400        }
401        ty::Adt(adt_def, ..) => {
402            let variant = ecx.read_discriminant(&op)?;
403            let op = if adt_def.is_enum() {
404                ecx.project_downcast(&op, variant)?
405            } else {
406                op
407            };
408            let field_count = adt_def.variants()[variant].fields.len();
409            let fields = read_fields(op, field_count)
410                .zip(&adt_def.variant(variant).fields)
411                .map(|(value, field)| {
412                    interp_ok(ConstantFieldExpr {
413                        field: field.did.sinto(s),
414                        value: value?,
415                    })
416                })
417                .collect::<InterpResult<Vec<_>>>()?;
418            ConstantExprKind::Adt {
419                kind: get_variant_kind(adt_def, variant, s),
420                fields,
421            }
422        }
423        ty::Closure(def_id, args) => {
424            // A closure is essentially an adt with funky generics and some builtin impls.
425            let def_id: DefId = def_id.sinto(s);
426            let field_count = args.as_closure().upvar_tys().len();
427            let fields = read_fields(op, field_count)
428                .map(|value| {
429                    interp_ok(ConstantFieldExpr {
430                        // HACK: Closure fields don't have their own def_id, but Charon doesn't use
431                        // field DefIds so we put a dummy one.
432                        field: def_id.clone(),
433                        value: value?,
434                    })
435                })
436                .collect::<InterpResult<Vec<_>>>()?;
437            ConstantExprKind::Adt {
438                kind: VariantKind::Struct,
439                fields,
440            }
441        }
442        ty::Tuple(args) => {
443            let fields = read_fields(op, args.len()).collect::<InterpResult<Vec<_>>>()?;
444            ConstantExprKind::Tuple { fields }
445        }
446        ty::Array(..) | ty::Slice(..) => {
447            let len = op.len(ecx)?;
448            let fields = (0..len)
449                .map(|i| {
450                    let op = ecx.project_index(&op, i)?;
451                    op_to_const(s, span, ecx, op)
452                })
453                .collect::<InterpResult<Vec<_>>>()?;
454            ConstantExprKind::Array { fields }
455        }
456        ty::Str => {
457            let str = ecx.read_str(&op.assert_mem_place())?;
458            ConstantExprKind::Literal(ConstantLiteral::Str(str.to_owned()))
459        }
460        ty::FnDef(def_id, args) => {
461            let args = args.no_bound_vars().expect("bound variables in FnDef");
462            let item = translate_item_ref(s, *def_id, args);
463            ConstantExprKind::FnDef(item)
464        }
465        ty::FnPtr(..) => {
466            let fn_ptr = ecx.read_pointer(&op)?;
467            let FnVal::Instance(instance) = ecx.get_ptr_fn(fn_ptr)?;
468            let def_id = instance.def_id();
469            let generics = instance.args;
470            let fun = translate_item_ref(s, def_id, generics);
471            ConstantExprKind::FnPtr(fun)
472        }
473        ty::RawPtr(..) | ty::Ref(..) => {
474            // Make sure we only read through if it's not dangling!
475            let place_dangling = ecx.deref_pointer(&op).discard_err();
476            let place = place_dangling
477                .filter(|place| ecx.ptr_get_alloc_id(place.ptr(), 0).discard_err().is_some());
478            if let Some(op) = place {
479                // Valid pointer case
480                let val = op_to_const(s, span, ecx, op.into())?;
481                match ty.kind() {
482                    ty::Ref(..) => ConstantExprKind::Borrow(val),
483                    ty::RawPtr(.., mutability) => ConstantExprKind::RawBorrow {
484                        arg: val,
485                        mutability: mutability.sinto(s),
486                    },
487                    _ => unreachable!(),
488                }
489            } else {
490                // Invalid pointer; try reading it as a raw address
491                let scalar = ecx.read_scalar(&op)?;
492                let scalar_int = scalar.try_to_scalar_int().unwrap();
493                let v = scalar_int.to_uint(scalar_int.size());
494                let lit = ConstantLiteral::PtrNoProvenance(v);
495                ConstantExprKind::Literal(lit)
496            }
497        }
498        ty::Pat(..) => {
499            let op = ecx.project_field(&op, FieldIdx::from_u16(0))?;
500            *op_to_const(s, span, ecx, op)?.contents
501        }
502        ty::Dynamic(..)
503        | ty::Foreign(..)
504        | ty::UnsafeBinder(..)
505        | ty::CoroutineClosure(..)
506        | ty::Coroutine(..)
507        | ty::CoroutineWitness(..) => ConstantExprKind::Todo("Unhandled constant type".into()),
508        ty::Alias(..) | ty::Param(..) | ty::Bound(..) | ty::Placeholder(..) | ty::Infer(..) => {
509            fatal!(s[span], "Encountered evaluated constant of non-monomorphic type"; {op})
510        }
511        ty::Never | ty::Error(..) => {
512            fatal!(s[span], "Encountered evaluated constant of invalid type"; {ty})
513        }
514    };
515    let val = kind.decorate(ty.sinto(s), span.sinto(s));
516    interp_ok(val)
517}
518
519pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
520    s: &S,
521    ty: rustc_middle::ty::Ty<'tcx>,
522    val: mir::ConstValue,
523    span: rustc_span::Span,
524) -> InterpResult<'tcx, ConstantExpr> {
525    let tcx = s.base().tcx;
526    let typing_env = s.typing_env();
527    let (ecx, op) =
528        const_eval::mk_eval_cx_for_const_val(tcx.at(span), typing_env, val, ty).unwrap();
529    op_to_const(s, span, &ecx, op)
530}
charon_driver/hax/constant_utils/uneval.rs

charon_driver/hax/constant_utils/
uneval.rs
