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

charon_lib/ast/bodies/
values.rs
