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

charon_lib/ast/bodies/
values.rs
