flux_middle/
big_int.rs

1use std::fmt;
2
3use rustc_macros::{Decodable, Encodable};
4
5/// A signed integer in the range [-2^128, 2^128], represented by a `u128` and an explicit sign.
6///
7/// In the logic, we work mathematical integers so we could represent them with arbitrary precision
8/// integers. We instead take the simpler approach of using a fixed size representation that allows
9/// us to store any Rust literal, i.e., we can represent both `i128::MIN` and `u128::MAX`. This works
10/// because we never do arithmetic. We can change the representation in the future (and use arbitrary
11/// precision integers) if this ever becomes a problem, e.g., if we want to do (precise) arithmetic
12/// during constant folding.
13#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash, Encodable, Decodable, PartialOrd, Ord)]
14pub struct BigInt {
15    sign: Sign,
16    val: u128,
17}
18
19/// This are in order so negative is less than non-negative.
20#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable, PartialOrd, Ord)]
21enum Sign {
22    Negative,
23    NonNegative,
24}
25
26impl BigInt {
27    pub const ZERO: BigInt = BigInt { sign: Sign::NonNegative, val: 0 };
28    pub const ONE: BigInt = BigInt { sign: Sign::NonNegative, val: 1 };
29
30    pub fn is_negative(&self) -> bool {
31        matches!(self.sign, Sign::Negative)
32    }
33
34    pub fn abs(&self) -> u128 {
35        self.val
36    }
37
38    /// Given the bit width of a signed integer type, produces the minimum integer for
39    /// that type, i.e., -2^(bit_width - 1).
40    pub fn int_min(bit_width: u32) -> BigInt {
41        BigInt { sign: Sign::Negative, val: 1u128 << (bit_width - 1) }
42    }
43
44    /// Given the bit width of a signed integer type, produces the maximum integer for
45    /// that type, i.e., 2^(bit_width - 1) - 1.
46    pub fn int_max(bit_width: u32) -> BigInt {
47        (i128::MAX >> (128 - bit_width)).into()
48    }
49
50    /// Given the bit width of an unsigned integer type, produces the maximum
51    /// unsigned integer for that type, i.e., 2^bit_width - 1.
52    pub fn uint_max(bit_width: u32) -> BigInt {
53        (u128::MAX >> (128 - bit_width)).into()
54    }
55}
56
57impl From<usize> for BigInt {
58    fn from(val: usize) -> Self {
59        BigInt { sign: Sign::NonNegative, val: val as u128 }
60    }
61}
62
63impl From<u128> for BigInt {
64    fn from(val: u128) -> Self {
65        BigInt { sign: Sign::NonNegative, val }
66    }
67}
68
69impl From<i128> for BigInt {
70    fn from(val: i128) -> Self {
71        let sign = if val < 0 { Sign::Negative } else { Sign::NonNegative };
72        BigInt { sign, val: val.unsigned_abs() }
73    }
74}
75
76impl From<i32> for BigInt {
77    fn from(val: i32) -> Self {
78        // TODO(nilehmann) use Flux to prove this doesn't overflow
79        if val < 0 {
80            BigInt { sign: Sign::Negative, val: -(val as i64) as u128 }
81        } else {
82            BigInt { sign: Sign::NonNegative, val: val as u128 }
83        }
84    }
85}
86
87impl From<u32> for BigInt {
88    fn from(val: u32) -> Self {
89        BigInt { sign: Sign::NonNegative, val: val as u128 }
90    }
91}
92
93impl fmt::Display for BigInt {
94    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95        match self.sign {
96            Sign::NonNegative => write!(f, "{}", self.val),
97            Sign::Negative => write!(f, "-{}", self.val),
98        }
99    }
100}
flux_middle/big_int.rs

flux_middle/
big_int.rs
