charon_lib/ast/bodies/
values.rs

1//! Contains definitions for variables and constant values.
2use core::hash::Hash;
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
5use serde::{Deserialize, Serialize};
6use serde_state::{DeserializeState, SerializeState};
7use std::vec::Vec;
8
9use crate::ast::*;
10
11/// A constant expression.
12#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
13#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
14#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
15pub struct ConstantExpr(pub HashConsed<WithCachedTypeInfo<(ConstantExprKind, Ty)>>);
16
17#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
18#[derive(VariantName, EnumIsA, EnumAsGetters)]
19#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
20#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("C"))]
21pub enum ConstantExprKind {
22    /// Boolean value.
23    Bool(bool),
24    /// Integer value.
25    #[serde_state(stateless)]
26    Integer(IntegerValue),
27    /// Char value.
28    Char(char),
29    /// Float value.
30    #[serde_state(stateless)]
31    Float(FloatValue),
32    /// Value of an ADT (struct or enum).
33    ///
34    /// This is eliminated inside functions if `--raw-consts` is off.
35    Adt(Option<VariantId>, Vec<ConstantExpr>),
36    /// Array value.
37    ///
38    /// This is eliminated inside functions if `--raw-consts` is off.
39    Array(Vec<ConstantExpr>),
40    /// A shared reference to a constant value.
41    ///
42    /// This is eliminated inside functions if `--raw-consts` is off.
43    Ref(ConstantExpr, Option<UnsizingMetadata>),
44    /// A pointer to a static.
45    ///
46    /// This is eliminated inside functions if `--raw-consts` is off.
47    Ptr(RefKind, ConstantExpr, Option<UnsizingMetadata>),
48    /// `str` value.
49    Str(String),
50    /// Byte string value.
51    ByteStr(Vec<u8>),
52    /// ZST constant corresponding to the unique value of the type of a function item.
53    FnDef(FnPtr),
54    /// A function pointer value; this is a pointer (i.e. an address).
55    ///
56    /// This is eliminated inside functions if `--raw-consts` is off.
57    FnPtr(FnPtr),
58    /// A pointer with no provenance (e.g. 0 for the null pointer)
59    ///
60    /// This is eliminated inside functions if `--raw-consts` is off.
61    PtrNoProvenance(#[serde(with = "scalar_value_ser_de")] u128),
62    /// The `TypeId` value for a type.
63    TypeId(Ty),
64    /// Raw memory value obtained from constant evaluation. Used when a more structured
65    /// representation isn't possible (e.g. for unions) or just isn't implemented yet.
66    RawMemory(Vec<Byte>),
67
68    /// A const generic var
69    Var(ConstGenericDbVar),
70    /// The value of a constant/static.
71    ///
72    /// This is eliminated inside functions if `--raw-consts` is off.
73    Global(GlobalDeclRef),
74    /// A call to a `const fn`.
75    Call(FnPtr, Vec<ConstantExpr>),
76    /// A trait associated constant.
77    ///
78    /// E.g.:
79    /// ```text
80    /// impl Foo for Bar {
81    ///   const C : usize = 32; // <-
82    /// }
83    /// ```
84    TraitConst(TraitRef, AssocConstId),
85    /// A reference to the vtable `static` item for this trait ref. This can be normalized if we
86    /// emitted a vtable item.
87    ///
88    /// This is eliminated if `--raw-consts` is off.
89    VTableRef(TraitRef),
90    /// The integer discriminant value corresponding to this enum variant.
91    Discriminant(TypeDeclRef, VariantId),
92    /// The size of the given type.
93    SizeOf(Ty),
94    /// The alignment of the given type.
95    AlignOf(Ty),
96    /// The offset of the given field.
97    OffsetOf(TypeDeclRef, Option<VariantId>, FieldId),
98
99    /// A constant expression that Charon doesn't handle, along with the reason why.
100    Opaque(String),
101}
102
103/// A scalar value.
104#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
105#[derive(EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)]
106#[derive(
107    Serialize,
108    Deserialize,
109    SerializeState,
110    DeserializeState,
111    Drive,
112    DriveMut,
113    DriveTwo
114)]
115#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Integer"))]
116#[serde_state(stateless)]
117pub enum IntegerValue {
118    Unsigned(UIntTy, #[serde(with = "scalar_value_ser_de")] u128),
119    Signed(IntTy, #[serde(with = "scalar_value_ser_de")] i128),
120}
121
122/// This is simlar to the Scalar value above. However, instead of storing
123/// the float value itself, we store its String representation. This allows
124/// to derive the Eq and Ord traits, which are not implemented for floats
125#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
126#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
127pub struct FloatValue {
128    #[cfg_attr(feature = "charon_on_charon", charon::rename("float_value"))]
129    pub value: String,
130    #[cfg_attr(feature = "charon_on_charon", charon::rename("float_ty"))]
131    pub ty: FloatTy,
132}
133
134#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
135#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
136#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Prov"))]
137pub enum Provenance {
138    Global(GlobalDeclRef),
139    Function(FnPtr),
140    Unknown,
141}
142
143/// A byte, in the MiniRust sense: it can either be uninitialized, a concrete u8 value,
144/// or part of a pointer with provenance (e.g. to a global or a function)
145#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
146#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
147pub enum Byte {
148    /// An uninitialized byte
149    Uninit,
150    /// A concrete byte value
151    Value(u8),
152    /// A byte that is part of a pointer with provenance. The u8 is the offset within the
153    /// pointer. Note that we do not have an actual value for this pointer byte, unlike
154    /// MiniRust, as that is non-deterministic.
155    Provenance(Provenance, u8),
156}
157
158macro_rules! static_constant {
159    ($e:expr) => {{
160        use std::sync::LazyLock;
161        static CONSTANT: LazyLock<ConstantExpr> = LazyLock::new(|| $e);
162        CONSTANT.clone()
163    }};
164}
165
166impl ConstantExpr {
167    pub fn new(kind: ConstantExprKind, ty: Ty) -> Self {
168        Self(HashConsed::new(WithCachedTypeInfo::new((kind, ty))))
169    }
170
171    pub fn kind(&self) -> &ConstantExprKind {
172        &self.0.inner().0
173    }
174
175    pub fn ty(&self) -> &Ty {
176        &self.0.inner().1
177    }
178
179    pub fn with_contents_mut<R>(
180        &mut self,
181        f: impl FnOnce(&mut ConstantExprKind, &mut Ty) -> R,
182    ) -> R {
183        self.0
184            .with_inner_mut(|contents| contents.with_value_mut(|(kind, ty)| f(kind, ty)))
185    }
186
187    pub fn mk_unit() -> Self {
188        static_constant!(ConstantExpr::new(
189            ConstantExprKind::Adt(None, Vec::new()),
190            Ty::mk_unit(),
191        ))
192    }
193
194    pub fn mk_usize(value: u128) -> Self {
195        if value == 0 {
196            static_constant!(IntegerValue::mk_usize(0).to_constant())
197        } else {
198            IntegerValue::mk_usize(value).to_constant()
199        }
200    }
201
202    pub fn as_usize_literal(&self) -> Option<u128> {
203        match self.kind() {
204            ConstantExprKind::Integer(IntegerValue::Unsigned(UIntTy::Usize, value)) => Some(*value),
205            _ => None,
206        }
207    }
208}
209
210impl ConstantExprKind {
211    pub fn from_bits(scalar_ty: &ScalarTy, bits: u128) -> Option<Self> {
212        match *scalar_ty {
213            ScalarTy::Integer(int_ty) => Some(Self::Integer(IntegerValue::from_bits(int_ty, bits))),
214            ScalarTy::Bool => match bits {
215                0 => Some(Self::Bool(false)),
216                1 => Some(Self::Bool(true)),
217                _ => None,
218            },
219            ScalarTy::Char => {
220                let bytes: [u8; 4] = bits.to_le_bytes()[0..4].try_into().unwrap();
221                Some(Self::Char(
222                    std::char::from_u32(u32::from_le_bytes(bytes)).unwrap(),
223                ))
224            }
225            ScalarTy::Float(_) => None,
226        }
227    }
228}
229
230impl std::ops::Deref for ConstantExpr {
231    type Target = WithCachedTypeInfo<(ConstantExprKind, Ty)>;
232    fn deref(&self) -> &Self::Target {
233        &self.0
234    }
235}
236
237impl IntegerValue {
238    fn ptr_size_max(ptr_size: ByteCount, signed: bool) -> u128 {
239        match ptr_size {
240            2 => {
241                if signed {
242                    i16::MAX as u128
243                } else {
244                    u16::MAX as u128
245                }
246            }
247            4 => {
248                if signed {
249                    i32::MAX as u128
250                } else {
251                    u32::MAX as u128
252                }
253            }
254            8 => {
255                if signed {
256                    i64::MAX as u128
257                } else {
258                    u64::MAX as u128
259                }
260            }
261            _ => panic!("`ptr_size_max`: unsupported ptr size {ptr_size}"),
262        }
263    }
264
265    fn ptr_size_min(ptr_size: ByteCount, signed: bool) -> i128 {
266        match ptr_size {
267            2 => {
268                if signed {
269                    i16::MIN as i128
270                } else {
271                    u16::MIN as i128
272                }
273            }
274            4 => {
275                if signed {
276                    i32::MIN as i128
277                } else {
278                    u32::MIN as i128
279                }
280            }
281            8 => {
282                if signed {
283                    i64::MIN as i128
284                } else {
285                    u64::MIN as i128
286                }
287            }
288            _ => panic!("`ptr_size_min`: unsupported ptr size {ptr_size}"),
289        }
290    }
291
292    pub fn ty(&self) -> IntegerTy {
293        match self {
294            IntegerValue::Signed(ty, _) => IntegerTy::Signed(*ty),
295            IntegerValue::Unsigned(ty, _) => IntegerTy::Unsigned(*ty),
296        }
297    }
298
299    pub fn is_int(&self) -> bool {
300        matches!(self, IntegerValue::Signed(_, _))
301    }
302
303    pub fn is_uint(&self) -> bool {
304        matches!(self, IntegerValue::Unsigned(_, _))
305    }
306
307    /// When computing the result of binary operations, we convert the values
308    /// to u128 then back to the target type (while performing dynamic checks
309    /// of course).
310    pub fn as_uint(&self) -> Option<u128> {
311        match self {
312            IntegerValue::Unsigned(_, v) => Some(*v),
313            _ => None,
314        }
315    }
316
317    pub fn uint_is_in_bounds(ptr_size: ByteCount, ty: UIntTy, v: u128) -> bool {
318        match ty {
319            UIntTy::Usize => v <= Self::ptr_size_max(ptr_size, false),
320            UIntTy::U8 => v <= (u8::MAX as u128),
321            UIntTy::U16 => v <= (u16::MAX as u128),
322            UIntTy::U32 => v <= (u32::MAX as u128),
323            UIntTy::U64 => v <= (u64::MAX as u128),
324            UIntTy::U128 => true,
325        }
326    }
327
328    pub fn from_unchecked_uint(ty: UIntTy, v: u128) -> IntegerValue {
329        IntegerValue::Unsigned(ty, v)
330    }
331
332    pub fn from_uint(ptr_size: ByteCount, ty: UIntTy, v: u128) -> Option<Self> {
333        if !IntegerValue::uint_is_in_bounds(ptr_size, ty, v) {
334            None
335        } else {
336            Some(IntegerValue::from_unchecked_uint(ty, v))
337        }
338    }
339
340    pub fn mk_usize(value: u128) -> Self {
341        IntegerValue::Unsigned(UIntTy::Usize, value)
342    }
343
344    /// When computing the result of binary operations, we convert the values
345    /// to i128 then back to the target type (while performing dynamic checks
346    /// of course).
347    pub fn as_int(&self) -> Option<i128> {
348        match self {
349            IntegerValue::Signed(_, v) => Some(*v),
350            _ => None,
351        }
352    }
353
354    pub fn int_is_in_bounds(ptr_size: ByteCount, ty: IntTy, v: i128) -> bool {
355        match ty {
356            IntTy::Isize => {
357                v >= Self::ptr_size_min(ptr_size, true)
358                    && v <= Self::ptr_size_max(ptr_size, true) as i128
359            }
360            IntTy::I8 => v >= (i8::MIN as i128) && v <= (i8::MAX as i128),
361            IntTy::I16 => v >= (i16::MIN as i128) && v <= (i16::MAX as i128),
362            IntTy::I32 => v >= (i32::MIN as i128) && v <= (i32::MAX as i128),
363            IntTy::I64 => v >= (i64::MIN as i128) && v <= (i64::MAX as i128),
364            IntTy::I128 => true,
365        }
366    }
367
368    pub fn from_unchecked_int(ty: IntTy, v: i128) -> IntegerValue {
369        IntegerValue::Signed(ty, v)
370    }
371
372    /// Most integers are represented as `u128` by rustc. We must be careful not to sign-extend.
373    pub fn to_bits(&self) -> u128 {
374        match *self {
375            IntegerValue::Unsigned(_, v) => v,
376            IntegerValue::Signed(_, v) => u128::from_le_bytes(v.to_le_bytes()),
377        }
378    }
379
380    /// Translates little endian bytes into a corresponding `IntegerValue`.
381    /// This needs to do the round-trip to the correct integer type to guarantee
382    /// that the values are correctly sign-extended (e.g. if the bytes encode -1i8, taking all 16 bytes
383    /// would lead to the value 255i128 instead of -1i128).
384    pub fn from_le_bytes(ty: IntegerTy, bytes: [u8; 16]) -> Self {
385        macro_rules! from_le_bytes {
386            ($m:ident, $b:ident, [$(($i_ty: ty, $i:ident, $s:ident, $n_ty:ty, $t:ty)),*]) => {
387                match $m {
388                    $(
389                        IntegerTy::$s(<$i_ty>::$i) => {
390                            let n = size_of::<$n_ty>();
391                            let b: [u8; _] = $b[0..n].try_into().unwrap();
392                            IntegerValue::$s(<$i_ty>::$i, <$n_ty>::from_le_bytes(b) as $t)
393                        }
394                    )*
395                }
396            }
397        }
398
399        from_le_bytes!(
400            ty,
401            bytes,
402            [
403                (IntTy, Isize, Signed, isize, i128),
404                (IntTy, I8, Signed, i8, i128),
405                (IntTy, I16, Signed, i16, i128),
406                (IntTy, I32, Signed, i32, i128),
407                (IntTy, I64, Signed, i64, i128),
408                (IntTy, I128, Signed, i128, i128),
409                (UIntTy, Usize, Unsigned, usize, u128),
410                (UIntTy, U8, Unsigned, u8, u128),
411                (UIntTy, U16, Unsigned, u16, u128),
412                (UIntTy, U32, Unsigned, u32, u128),
413                (UIntTy, U64, Unsigned, u64, u128),
414                (UIntTy, U128, Unsigned, u128, u128)
415            ]
416        )
417    }
418
419    pub fn from_bits(ty: IntegerTy, bits: u128) -> Self {
420        let bytes = bits.to_le_bytes();
421        Self::from_le_bytes(ty, bytes)
422    }
423
424    /// **Warning**: most constants are stored as u128 by rustc. When converting
425    /// to i128, it is not correct to do `v as i128`, we must reinterpret the
426    /// bits (see [IntegerValue::from_le_bytes]).
427    pub fn from_int(ptr_size: ByteCount, ty: IntTy, v: i128) -> Option<IntegerValue> {
428        if !IntegerValue::int_is_in_bounds(ptr_size, ty, v) {
429            None
430        } else {
431            Some(IntegerValue::from_unchecked_int(ty, v))
432        }
433    }
434
435    /// Increment the value, staying within the same integer type. Returns `None` on overflow.
436    pub fn add(self, n: u128) -> Option<Self> {
437        Some(match self {
438            IntegerValue::Unsigned(ty, v) => IntegerValue::Unsigned(ty, v.checked_add(n)?),
439            IntegerValue::Signed(ty, v) => {
440                IntegerValue::Signed(ty, v.checked_add(n.try_into().unwrap())?)
441            }
442        })
443    }
444
445    pub fn to_constant(self) -> ConstantExpr {
446        let scalar_ty = ScalarTy::Integer(self.ty());
447        ConstantExpr::new(
448            ConstantExprKind::Integer(self),
449            TyKind::Scalar(scalar_ty).into_ty(),
450        )
451    }
452}
453
454/// Custom serializer that stores 128 bit integers as strings to avoid overflow.
455pub(crate) mod scalar_value_ser_de {
456    use std::{marker::PhantomData, str::FromStr};
457
458    use serde::de::{Deserializer, Error};
459
460    pub fn serialize<S, V>(val: &V, serializer: S) -> Result<S::Ok, S::Error>
461    where
462        S: serde::ser::Serializer,
463        V: ToString,
464    {
465        serializer.serialize_str(&val.to_string())
466    }
467
468    /// Stateful variant for types that derive `SerializeState`: the state is irrelevant for a
469    /// scalar, so we delegate to the stateless [`serialize`].
470    pub fn serialize_state<S, State: ?Sized, V>(
471        val: &V,
472        _state: &State,
473        serializer: S,
474    ) -> Result<S::Ok, S::Error>
475    where
476        S: serde::ser::Serializer,
477        V: ToString,
478    {
479        serialize(val, serializer)
480    }
481
482    pub fn deserialize<'de, D, V>(deserializer: D) -> Result<V, D::Error>
483    where
484        D: Deserializer<'de>,
485        V: FromStr,
486    {
487        struct Visitor<V> {
488            _val: PhantomData<V>,
489        }
490        impl<'de, V> serde::de::Visitor<'de> for Visitor<V>
491        where
492            V: FromStr,
493        {
494            type Value = V;
495            fn expecting(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
496                write!(f, "IntegerValue value")
497            }
498            fn visit_str<E>(self, v: &str) -> Result<Self::Value, E>
499            where
500                E: Error,
501            {
502                v.parse()
503                    .map_err(|_| E::custom("Could not parse 128 bit integer!"))
504            }
505        }
506        deserializer.deserialize_str(Visitor { _val: PhantomData })
507    }
508
509    /// Stateful variant for types that derive `DeserializeState`: the state is irrelevant for a
510    /// scalar, so we delegate to the stateless [`deserialize`].
511    pub fn deserialize_state<'de, D, State: ?Sized, V>(
512        _state: &State,
513        deserializer: D,
514    ) -> Result<V, D::Error>
515    where
516        D: Deserializer<'de>,
517        V: FromStr,
518    {
519        deserialize(deserializer)
520    }
521}
522
523#[cfg(test)]
524mod test {
525    use super::*;
526
527    #[test]
528    fn test_big_endian_scalars() {
529        let u128 = 0x12345678901234567890123456789012u128;
530        let le_bytes = u128.to_le_bytes();
531
532        let le_scalar = IntegerValue::from_le_bytes(IntegerTy::Unsigned(UIntTy::U128), le_bytes);
533        assert_eq!(le_scalar, IntegerValue::Unsigned(UIntTy::U128, u128));
534
535        let i64 = 0x1234567890123456i64;
536        let le_bytes = (i64 as i128).to_le_bytes();
537        let le_scalar = IntegerValue::from_le_bytes(IntegerTy::Signed(IntTy::I64), le_bytes);
538        assert_eq!(le_scalar, IntegerValue::Signed(IntTy::I64, i64 as i128));
539    }
540}
charon_lib/ast/bodies/values.rs

charon_lib/ast/bodies/
values.rs
