charon_lib/ast/
values_utils.rs

1//! Implementations for [crate::values]
2use crate::ast::*;
3
4#[derive(Debug, Clone)]
5pub enum ScalarError {
6    /// Attempt to use a signed scalar as an unsigned scalar or vice-versa
7    IncorrectSign,
8    /// Out of bounds scalar
9    OutOfBounds,
10    UnsupportedPtrSize,
11}
12/// Our redefinition of Result - we don't care much about the I/O part.
13pub type ScalarResult<T> = std::result::Result<T, ScalarError>;
14
15macro_rules! from_le_bytes {
16    ($m:ident, $b:ident, [$(($i_ty: ty, $i:ident, $s:ident, $n_ty:ty, $t:ty)),*]) => {
17        match $m {
18            $(
19                IntegerTy::$s(<$i_ty>::$i) => {
20                    let n = size_of::<$n_ty>();
21                    let b: [u8; _] = $b[0..n].try_into().unwrap();
22                    ScalarValue::$s(<$i_ty>::$i, <$n_ty>::from_le_bytes(b) as $t)
23                }
24            )*
25        }
26    }
27}
28
29impl Literal {
30    pub fn char_from_le_bytes(bits: u128) -> Self {
31        let b: [u8; 4] = bits.to_le_bytes()[0..4].try_into().unwrap();
32        Literal::Char(std::char::from_u32(u32::from_le_bytes(b)).unwrap())
33    }
34
35    pub fn from_bits(lit_ty: &LiteralTy, bits: u128) -> Option<Self> {
36        match *lit_ty {
37            LiteralTy::Int(int_ty) => Some(Literal::Scalar(ScalarValue::from_bits(
38                IntegerTy::Signed(int_ty),
39                bits,
40            ))),
41            LiteralTy::UInt(uint_ty) => Some(Literal::Scalar(ScalarValue::from_bits(
42                IntegerTy::Unsigned(uint_ty),
43                bits,
44            ))),
45            LiteralTy::Char => Some(Literal::char_from_le_bytes(bits)),
46            _ => None,
47        }
48    }
49}
50
51impl ScalarValue {
52    fn ptr_size_max(ptr_size: ByteCount, signed: bool) -> ScalarResult<u128> {
53        match ptr_size {
54            2 => Ok(if signed {
55                i16::MAX as u128
56            } else {
57                u16::MAX as u128
58            }),
59            4 => Ok(if signed {
60                i32::MAX as u128
61            } else {
62                u32::MAX as u128
63            }),
64            8 => Ok(if signed {
65                i64::MAX as u128
66            } else {
67                u64::MAX as u128
68            }),
69            _ => Err(ScalarError::UnsupportedPtrSize),
70        }
71    }
72
73    fn ptr_size_min(ptr_size: ByteCount, signed: bool) -> ScalarResult<i128> {
74        match ptr_size {
75            2 => Ok(if signed {
76                i16::MIN as i128
77            } else {
78                u16::MIN as i128
79            }),
80            4 => Ok(if signed {
81                i32::MIN as i128
82            } else {
83                u32::MIN as i128
84            }),
85            8 => Ok(if signed {
86                i64::MIN as i128
87            } else {
88                u64::MIN as i128
89            }),
90            _ => Err(ScalarError::UnsupportedPtrSize),
91        }
92    }
93
94    pub fn ty(&self) -> IntegerTy {
95        match self {
96            ScalarValue::Signed(ty, _) => IntegerTy::Signed(*ty),
97            ScalarValue::Unsigned(ty, _) => IntegerTy::Unsigned(*ty),
98        }
99    }
100
101    pub fn is_int(&self) -> bool {
102        matches!(self, ScalarValue::Signed(_, _))
103    }
104
105    pub fn is_uint(&self) -> bool {
106        matches!(self, ScalarValue::Unsigned(_, _))
107    }
108
109    /// When computing the result of binary operations, we convert the values
110    /// to u128 then back to the target type (while performing dynamic checks
111    /// of course).
112    pub fn as_uint(&self) -> ScalarResult<u128> {
113        match self {
114            ScalarValue::Unsigned(_, v) => Ok(*v),
115            _ => Err(ScalarError::IncorrectSign),
116        }
117    }
118
119    pub fn uint_is_in_bounds(ptr_size: ByteCount, ty: UIntTy, v: u128) -> bool {
120        match ty {
121            UIntTy::Usize => v <= Self::ptr_size_max(ptr_size, false).unwrap(),
122            UIntTy::U8 => v <= (u8::MAX as u128),
123            UIntTy::U16 => v <= (u16::MAX as u128),
124            UIntTy::U32 => v <= (u32::MAX as u128),
125            UIntTy::U64 => v <= (u64::MAX as u128),
126            UIntTy::U128 => true,
127        }
128    }
129
130    pub fn from_unchecked_uint(ty: UIntTy, v: u128) -> ScalarValue {
131        ScalarValue::Unsigned(ty, v)
132    }
133
134    pub fn from_uint(ptr_size: ByteCount, ty: UIntTy, v: u128) -> ScalarResult<Self> {
135        if !ScalarValue::uint_is_in_bounds(ptr_size, ty, v) {
136            trace!("Not in bounds for {:?}: {}", ty, v);
137            Err(ScalarError::OutOfBounds)
138        } else {
139            Ok(ScalarValue::from_unchecked_uint(ty, v))
140        }
141    }
142
143    pub fn mk_usize(ptr_size: ByteCount, v: u64) -> Self {
144        ScalarValue::from_uint(ptr_size, UIntTy::Usize, v as u128).unwrap()
145    }
146
147    /// When computing the result of binary operations, we convert the values
148    /// to i128 then back to the target type (while performing dynamic checks
149    /// of course).
150    pub fn as_int(&self) -> ScalarResult<i128> {
151        match self {
152            ScalarValue::Signed(_, v) => Ok(*v),
153            _ => Err(ScalarError::IncorrectSign),
154        }
155    }
156
157    pub fn int_is_in_bounds(ptr_size: ByteCount, ty: IntTy, v: i128) -> bool {
158        match ty {
159            IntTy::Isize => {
160                v >= Self::ptr_size_min(ptr_size, true).unwrap()
161                    && v <= Self::ptr_size_max(ptr_size, true).unwrap() as i128
162            }
163            IntTy::I8 => v >= (i8::MIN as i128) && v <= (i8::MAX as i128),
164            IntTy::I16 => v >= (i16::MIN as i128) && v <= (i16::MAX as i128),
165            IntTy::I32 => v >= (i32::MIN as i128) && v <= (i32::MAX as i128),
166            IntTy::I64 => v >= (i64::MIN as i128) && v <= (i64::MAX as i128),
167            IntTy::I128 => true,
168        }
169    }
170
171    pub fn from_unchecked_int(ty: IntTy, v: i128) -> ScalarValue {
172        ScalarValue::Signed(ty, v)
173    }
174
175    /// Most integers are represented as `u128` by rustc. We must be careful not to sign-extend.
176    pub fn to_bits(&self) -> u128 {
177        match *self {
178            ScalarValue::Unsigned(_, v) => v,
179            ScalarValue::Signed(_, v) => u128::from_le_bytes(v.to_le_bytes()),
180        }
181    }
182
183    /// Translates little endian bytes into a corresponding `ScalarValue`.
184    /// This needs to do the round-trip to the correct integer type to guarantee
185    /// that the values are correctly sign-extended (e.g. if the bytes encode -1i8, taking all 16 bytes
186    /// would lead to the value 255i128 instead of -1i128).
187    pub fn from_le_bytes(ty: IntegerTy, bytes: [u8; 16]) -> Self {
188        from_le_bytes!(
189            ty,
190            bytes,
191            [
192                (IntTy, Isize, Signed, isize, i128),
193                (IntTy, I8, Signed, i8, i128),
194                (IntTy, I16, Signed, i16, i128),
195                (IntTy, I32, Signed, i32, i128),
196                (IntTy, I64, Signed, i64, i128),
197                (IntTy, I128, Signed, i128, i128),
198                (UIntTy, Usize, Unsigned, usize, u128),
199                (UIntTy, U8, Unsigned, u8, u128),
200                (UIntTy, U16, Unsigned, u16, u128),
201                (UIntTy, U32, Unsigned, u32, u128),
202                (UIntTy, U64, Unsigned, u64, u128),
203                (UIntTy, U128, Unsigned, u128, u128)
204            ]
205        )
206    }
207
208    pub fn from_bits(ty: IntegerTy, bits: u128) -> Self {
209        let bytes = bits.to_le_bytes();
210        Self::from_le_bytes(ty, bytes)
211    }
212
213    /// **Warning**: most constants are stored as u128 by rustc. When converting
214    /// to i128, it is not correct to do `v as i128`, we must reinterpret the
215    /// bits (see [ScalarValue::from_le_bytes]).
216    pub fn from_int(ptr_size: ByteCount, ty: IntTy, v: i128) -> ScalarResult<ScalarValue> {
217        if !ScalarValue::int_is_in_bounds(ptr_size, ty, v) {
218            Err(ScalarError::OutOfBounds)
219        } else {
220            Ok(ScalarValue::from_unchecked_int(ty, v))
221        }
222    }
223
224    /// Increment the value, staying within the same integer type. Returns `None` on overflow.
225    pub fn add(self, n: u128) -> Option<Self> {
226        Some(match self {
227            ScalarValue::Unsigned(ty, v) => ScalarValue::Unsigned(ty, v.checked_add(n)?),
228            ScalarValue::Signed(ty, v) => {
229                ScalarValue::Signed(ty, v.checked_add(n.try_into().unwrap())?)
230            }
231        })
232    }
233
234    pub fn to_constant(self) -> ConstantExpr {
235        let literal_ty = match self {
236            ScalarValue::Signed(int_ty, _) => LiteralTy::Int(int_ty),
237            ScalarValue::Unsigned(uint_ty, _) => LiteralTy::UInt(uint_ty),
238        };
239        ConstantExpr {
240            kind: ConstantExprKind::Literal(Literal::Scalar(self)),
241            ty: TyKind::Literal(literal_ty).into_ty(),
242        }
243    }
244}
245
246/// Custom serializer that stores 128 bit integers as strings to avoid overflow.
247pub(crate) mod scalar_value_ser_de {
248    use std::{marker::PhantomData, str::FromStr};
249
250    use serde::de::{Deserializer, Error};
251
252    pub fn serialize<S, V>(val: &V, serializer: S) -> Result<S::Ok, S::Error>
253    where
254        S: serde::ser::Serializer,
255        V: ToString,
256    {
257        serializer.serialize_str(&val.to_string())
258    }
259
260    /// Stateful variant for types that derive `SerializeState`: the state is irrelevant for a
261    /// scalar, so we delegate to the stateless [`serialize`].
262    pub fn serialize_state<S, State: ?Sized, V>(
263        val: &V,
264        _state: &State,
265        serializer: S,
266    ) -> Result<S::Ok, S::Error>
267    where
268        S: serde::ser::Serializer,
269        V: ToString,
270    {
271        serialize(val, serializer)
272    }
273
274    pub fn deserialize<'de, D, V>(deserializer: D) -> Result<V, D::Error>
275    where
276        D: Deserializer<'de>,
277        V: FromStr,
278    {
279        struct Visitor<V> {
280            _val: PhantomData<V>,
281        }
282        impl<'de, V> serde::de::Visitor<'de> for Visitor<V>
283        where
284            V: FromStr,
285        {
286            type Value = V;
287            fn expecting(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
288                write!(f, "ScalarValue value")
289            }
290            fn visit_str<E>(self, v: &str) -> Result<Self::Value, E>
291            where
292                E: Error,
293            {
294                v.parse()
295                    .map_err(|_| E::custom("Could not parse 128 bit integer!"))
296            }
297        }
298        deserializer.deserialize_str(Visitor { _val: PhantomData })
299    }
300
301    /// Stateful variant for types that derive `DeserializeState`: the state is irrelevant for a
302    /// scalar, so we delegate to the stateless [`deserialize`].
303    pub fn deserialize_state<'de, D, State: ?Sized, V>(
304        _state: &State,
305        deserializer: D,
306    ) -> Result<V, D::Error>
307    where
308        D: Deserializer<'de>,
309        V: FromStr,
310    {
311        deserialize(deserializer)
312    }
313}
314
315#[cfg(test)]
316mod test {
317    use super::*;
318
319    #[test]
320    fn test_big_endian_scalars() -> ScalarResult<()> {
321        let u128 = 0x12345678901234567890123456789012u128;
322        let le_bytes = u128.to_le_bytes();
323
324        let le_scalar = ScalarValue::from_le_bytes(IntegerTy::Unsigned(UIntTy::U128), le_bytes);
325        assert_eq!(le_scalar, ScalarValue::Unsigned(UIntTy::U128, u128));
326
327        let i64 = 0x1234567890123456i64;
328        let le_bytes = (i64 as i128).to_le_bytes();
329        let le_scalar = ScalarValue::from_le_bytes(IntegerTy::Signed(IntTy::I64), le_bytes);
330        assert_eq!(le_scalar, ScalarValue::Signed(IntTy::I64, i64 as i128));
331
332        Ok(())
333    }
334}
charon_lib/ast/values_utils.rs

charon_lib/ast/
values_utils.rs
