charon_driver/hax/constant_utils/
uneval.rs

1//! Translate constants to hax: type-system constants, and the values read by `rustc_const_uneval`.
2use super::*;
3use annotate_snippets::Level;
4use rustc_const_uneval::{AllocTarget, Byte, ConstReader, PtrTarget, ReadError};
5use rustc_middle::ty;
6
7#[tracing::instrument(level = "trace", skip(s))]
8fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
9    s: &S,
10    x: rustc_middle::ty::ScalarInt,
11    ty: rustc_middle::ty::Ty<'tcx>,
12) -> ConstantLiteral {
13    match ty.kind() {
14        ty::Char => ConstantLiteral::Char(
15            char::try_from(x).expect("scalar_int_to_constant_literal: expected a char"),
16        ),
17        ty::Bool => ConstantLiteral::Bool(
18            x.try_to_bool()
19                .expect("scalar_int_to_constant_literal: expected a bool"),
20        ),
21        ty::Int(kind) => {
22            let v = x.to_int(x.size());
23            ConstantLiteral::Int(ConstantInt::Int(v, kind.sinto(s)))
24        }
25        ty::Uint(kind) => {
26            let v = x.to_uint(x.size());
27            ConstantLiteral::Int(ConstantInt::Uint(v, kind.sinto(s)))
28        }
29        ty::Float(kind) => {
30            let v = x.to_bits_unchecked();
31            bits_and_type_to_float_constant_literal(v, kind.sinto(s))
32        }
33        _ => unreachable!("not a literal type: {ty:?}"),
34    }
35}
36
37/// Converts a bit-representation of a float of type `ty` to a constant literal
38fn bits_and_type_to_float_constant_literal(bits: u128, ty: FloatTy) -> ConstantLiteral {
39    use rustc_apfloat::{Float, ieee};
40    let string = match &ty {
41        FloatTy::F16 => ieee::Half::from_bits(bits).to_string(),
42        FloatTy::F32 => ieee::Single::from_bits(bits).to_string(),
43        FloatTy::F64 => ieee::Double::from_bits(bits).to_string(),
44        FloatTy::F128 => ieee::Quad::from_bits(bits).to_string(),
45    };
46    ConstantLiteral::Float(string, bits, ty)
47}
48
49impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr<'tcx>> for ty::Const<'tcx> {
50    #[tracing::instrument(level = "trace", skip(s))]
51    fn sinto(&self, s: &S) -> ConstantExpr<'tcx> {
52        let tcx = s.base().tcx;
53        let span = rustc_span::DUMMY_SP;
54        match self.kind() {
55            ty::ConstKind::Param(p) => {
56                let ty = p.find_const_ty_from_env(s.param_env());
57                let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
58                ConstantExpr::new(kind, ty.sinto(s))
59            }
60            ty::ConstKind::Alias(_, ucv) => {
61                let def = ucv
62                    .kind
63                    .opt_def_id()
64                    .expect("AliasConstKind with no def id?");
65                let src = ConstSource::TyConst(ucv);
66                if s.base().options.inline_anon_consts
67                    // Rustc hoists inline `const {}` blocks and constant expressions into
68                    // separate `AnonConst` items. This is internal to rustc, so we prefer inlining
69                    // their value.
70                    && matches!(tcx.def_kind(def), rustc_hir::def::DefKind::AnonConst)
71                    && let Some(val) = read_const(s, tcx.def_span(def), src, ReadMode::Structured)
72                {
73                    val
74                } else {
75                    let item = translate_item_ref(s, def, ucv.args);
76                    let kind = ConstantExprKind::NamedGlobal(item);
77                    let ty = tcx.type_of(def).instantiate(tcx, ucv.args);
78                    let ty = normalize(tcx, s.typing_env(), ty);
79                    ConstantExpr::new(kind, ty.sinto(s))
80                }
81            }
82            ty::ConstKind::Value(val) => val.sinto(s),
83            _ => {
84                let msg = format!("unexpected constant kind: {self:?}");
85                s.raise(Level::ERROR, span, msg.clone());
86                let ty = Ty::new(s, TyKind::Error);
87                ConstantExpr::new(ConstantExprKind::Todo(msg), ty)
88            }
89        }
90    }
91}
92
93impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr<'tcx>> for ty::Value<'tcx> {
94    #[tracing::instrument(level = "trace", skip(s))]
95    fn sinto(&self, s: &S) -> ConstantExpr<'tcx> {
96        let span = rustc_span::DUMMY_SP;
97        read_const(s, span, ConstSource::ValTree(*self), ReadMode::Structured).unwrap_or_else(
98            || {
99                ConstantExpr::new(
100                    ConstantExprKind::Todo("ConstValTree".into()),
101                    self.ty.sinto(s),
102                )
103            },
104        )
105    }
106}
107
108/// The reader for constants evaluated in the current context.
109fn const_reader<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> ConstReader<'tcx> {
110    ConstReader {
111        tcx: s.base().tcx,
112        typing_env: s.typing_env(),
113        config: s.base().options.consts,
114        alloc_types: s.with_global_cache(|cache| cache.alloc_types.clone()),
115    }
116}
117
118/// The global standing for `self`.
119impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ItemRef<'tcx>> for GlobalRef {
120    fn sinto(&self, s: &S) -> ItemRef<'tcx> {
121        match *self {
122            GlobalRef::Static(did) => translate_item_ref(s, did, Default::default()),
123            GlobalRef::Alloc(alloc_id) => {
124                let def_id = DefId::make_anon_alloc(s, alloc_id);
125                ItemRef::dummy_without_generics(s, def_id)
126            }
127        }
128    }
129}
130
131impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, FnPtrTarget<'tcx>>
132    for rustc_const_uneval::FnTarget<'tcx>
133{
134    fn sinto(&self, s: &S) -> FnPtrTarget<'tcx> {
135        use rustc_const_uneval::FnTarget;
136        match *self {
137            FnTarget::Instance(instance) => {
138                FnPtrTarget::Fn(translate_item_ref(s, instance.def_id(), instance.args))
139            }
140            FnTarget::ClosureAsFn(def_id, args) => {
141                FnPtrTarget::ClosureAsFn(ClosureTy::sfrom(s, def_id, args))
142            }
143        }
144    }
145}
146
147/// The metadata of a pointer to a value of type `from` unsized to type `to`.
148fn unsizing_metadata<'tcx, S: UnderOwnerState<'tcx>>(
149    s: &S,
150    from: ty::Ty<'tcx>,
151    to: ty::Ty<'tcx>,
152) -> UnsizingMetadata<'tcx> {
153    let from = ty::Ty::new_imm_ptr(s.base().tcx, from);
154    let to = ty::Ty::new_imm_ptr(s.base().tcx, to);
155    let (path, metadata) = compute_unsizing_metadata(s, from, to);
156    assert!(path.is_empty(), "Non-empty unsize path in const ptr");
157    metadata
158}
159
160/// The provenance to give to the bytes of a pointer into the given allocation.
161impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantByteProvenance<'tcx>> for AllocTarget<'tcx> {
162    fn sinto(&self, s: &S) -> ConstantByteProvenance<'tcx> {
163        match *self {
164            AllocTarget::Fn(target) => {
165                let fn_ptr_ty = target.fn_ptr_ty(s.base().tcx, s.typing_env());
166                ConstantByteProvenance::Function(target.sinto(s), fn_ptr_ty.sinto(s))
167            }
168            AllocTarget::Global(global) => ConstantByteProvenance::Global(global.sinto(s)),
169            AllocTarget::TypeId(ty) => ConstantByteProvenance::TypeId(ty.sinto(s)),
170            AllocTarget::VTable(ty, preds) => {
171                let tcx = s.base().tcx;
172                let dyn_ty = ty::Ty::new_dynamic(tcx, preds, tcx.lifetimes.re_erased);
173                match unsizing_metadata(s, ty, dyn_ty) {
174                    UnsizingMetadata::DirectVTable(proof) => ConstantByteProvenance::VTable(proof),
175                    metadata => unreachable!("unexpected vtable metadata {metadata:?}"),
176                }
177            }
178        }
179    }
180}
181
182impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr<'tcx>>
183    for rustc_const_uneval::Const<'tcx>
184{
185    fn sinto(&self, s: &S) -> ConstantExpr<'tcx> {
186        use rustc_const_uneval::ConstKind;
187        // The value of a pattern type is described at its base type.
188        let ty = match self.ty.kind() {
189            ty::Pat(base_ty, _) => *base_ty,
190            _ => self.ty,
191        };
192        let unsizing_metadata = |unsize: &Option<rustc_const_uneval::Unsize<'tcx>>| {
193            unsize.map(|unsize| unsizing_metadata(s, unsize.from, unsize.to))
194        };
195        let kind = match &self.kind {
196            ConstKind::Scalar(scalar_int) => {
197                ConstantExprKind::Literal(scalar_int_to_constant_literal(s, *scalar_int, ty))
198            }
199            ConstKind::PtrNoProvenance(addr) => {
200                ConstantExprKind::Literal(ConstantLiteral::PtrNoProvenance(*addr))
201            }
202            ConstKind::Str(str) => ConstantExprKind::Literal(ConstantLiteral::Str(str.clone())),
203            ConstKind::ByteStr(bytes) => {
204                ConstantExprKind::Literal(ConstantLiteral::ByteStr(bytes.clone()))
205            }
206            ConstKind::Aggregate { variant, fields } => {
207                let fields = fields.iter().map(|field| field.sinto(s));
208                match ty.kind() {
209                    ty::Adt(adt_def, _) => {
210                        let variant = variant.unwrap();
211                        ConstantExprKind::Adt {
212                            kind: get_variant_kind(adt_def, variant, s),
213                            fields: fields
214                                .zip(&adt_def.variant(variant).fields)
215                                .map(|(value, field)| ConstantFieldExpr {
216                                    field: field.did.sinto(s),
217                                    value,
218                                })
219                                .collect(),
220                        }
221                    }
222                    ty::Closure(def_id, _) => {
223                        let def_id: DefId = def_id.sinto(s);
224                        ConstantExprKind::Adt {
225                            kind: VariantKind::Struct,
226                            fields: fields
227                                .map(|value| ConstantFieldExpr {
228                                    // HACK: Closure fields don't have their own def_id, but Charon
229                                    // doesn't use field DefIds so we put a dummy one.
230                                    field: def_id.clone(),
231                                    value,
232                                })
233                                .collect(),
234                        }
235                    }
236                    ty::Tuple(_) => ConstantExprKind::Tuple {
237                        fields: fields.collect(),
238                    },
239                    ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array {
240                        fields: fields.collect(),
241                    },
242                    _ => unreachable!("unexpected aggregate type {ty:?}"),
243                }
244            }
245            ConstKind::Repeat { value, .. } => ConstantExprKind::Repeat {
246                value: value.sinto(s),
247            },
248            ConstKind::FnDef { def, args } => {
249                ConstantExprKind::FnDef(translate_item_ref(s, *def, args))
250            }
251            ConstKind::FnPtr(target) => ConstantExprKind::FnPtr(target.sinto(s)),
252            ConstKind::Ptr { target, unsize } => {
253                let metadata = unsizing_metadata(unsize);
254                let (base, projections) = match target {
255                    PtrTarget::Global {
256                        target,
257                        ty,
258                        projections,
259                    } => {
260                        let prov = match *target {
261                            // We name the globals we point into, even the ones that we otherwise
262                            // inline.
263                            AllocTarget::Global(global) => {
264                                ConstantByteProvenance::Global(global.sinto(s))
265                            }
266                            _ => target.sinto(s),
267                        };
268                        let projections = projections
269                            .iter()
270                            .map(|(proj, ty)| {
271                                use rustc_const_uneval::Projection;
272                                let proj = match *proj {
273                                    Projection::Field(variant, field) => {
274                                        ConstantProjectionElem::Field(variant, field)
275                                    }
276                                    Projection::Index(i) => ConstantProjectionElem::Index(i),
277                                    Projection::Subslice { from, to } => {
278                                        ConstantProjectionElem::Subslice { from, to }
279                                    }
280                                    Projection::Offset {
281                                        count,
282                                        ty: elem_ty,
283                                        in_bounds,
284                                    } => ConstantProjectionElem::Offset {
285                                        count,
286                                        ty: elem_ty.sinto(s),
287                                        in_bounds,
288                                        pointee_is_sized: solve_sized(s, *ty),
289                                    },
290                                };
291                                (proj, ty.sinto(s))
292                            })
293                            .collect();
294                        (ConstantPtrBase::Global(prov, ty.sinto(s)), projections)
295                    }
296                    PtrTarget::Inline(val) => (ConstantPtrBase::Value(val.sinto(s)), vec![]),
297                };
298                ConstantExprKind::Ptr {
299                    base,
300                    projections,
301                    metadata,
302                }
303            }
304            ConstKind::PtrCast { ptr, unsize } => {
305                ConstantExprKind::PtrCast(ptr.sinto(s), unsizing_metadata(unsize))
306            }
307            ConstKind::Memory(bytes) => {
308                // The bytes of a pointer share their provenance; we convert it only once.
309                let mut last_prov: Option<(AllocTarget, ConstantByteProvenance)> = None;
310                let bytes = bytes.iter().map(|byte| match *byte {
311                    Byte::Uninit => ConstantByte::Uninit,
312                    Byte::Value(v) => ConstantByte::Value(v),
313                    Byte::Ptr(target, offset, i) => {
314                        if last_prov.as_ref().is_none_or(|(last, _)| *last != target) {
315                            last_prov = Some((target, target.sinto(s)));
316                        }
317                        let prov = last_prov.as_ref().unwrap().1.clone();
318                        ConstantByte::Provenance(prov, offset.bytes(), i)
319                    }
320                });
321                ConstantExprKind::Memory(bytes.collect())
322            }
323            ConstKind::TypeId(ty) => ConstantExprKind::TypeId(ty.sinto(s)),
324            ConstKind::Unsupported(msg) => ConstantExprKind::Todo(msg.to_string()),
325        };
326        ConstantExpr::new(kind, self.ty.sinto(s))
327    }
328}
329
330/// Evaluate `src` and read it back as a `ConstantExpr`.
331pub fn read_const<'tcx, S: UnderOwnerState<'tcx>>(
332    s: &S,
333    span: rustc_span::Span,
334    src: ConstSource<'tcx>,
335    mode: ReadMode,
336) -> Option<ConstantExpr<'tcx>> {
337    match const_reader(s).read(span, src, mode) {
338        Ok(val) => Some(val.sinto(s)),
339        Err(ReadError::NotEvaluable) => None,
340        Err(err) => {
341            s.raise(
342                Level::WARNING,
343                span,
344                format!("Couldn't convert constant {src:?} back to an expression: {err:?}"),
345            );
346            None
347        }
348    }
349}
charon_driver/hax/constant_utils/uneval.rs

charon_driver/hax/constant_utils/
uneval.rs
