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

charon_lib/ast/bodies/
values.rs
