flux_middle/
big_int.rs

1use std::{cmp::Ordering, 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)]
14pub struct BigInt {
15    sign: Sign,
16    val: u128,
17}
18
19impl PartialOrd for BigInt {
20    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
21        Some(self.cmp(other))
22    }
23}
24
25impl Ord for BigInt {
26    fn cmp(&self, other: &Self) -> Ordering {
27        match (self.sign, other.sign) {
28            (Sign::Negative, Sign::NonNegative) => Ordering::Less,
29            (Sign::NonNegative, Sign::Negative) => Ordering::Greater,
30            (Sign::NonNegative, Sign::NonNegative) => self.val.cmp(&other.val),
31            (Sign::Negative, Sign::Negative) => other.val.cmp(&self.val),
32        }
33    }
34}
35
36/// This are in order so negative is less than non-negative.
37#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable, PartialOrd, Ord)]
38enum Sign {
39    Negative,
40    NonNegative,
41}
42
43impl BigInt {
44    pub const ZERO: BigInt = BigInt { sign: Sign::NonNegative, val: 0 };
45    pub const ONE: BigInt = BigInt { sign: Sign::NonNegative, val: 1 };
46
47    pub fn is_negative(&self) -> bool {
48        matches!(self.sign, Sign::Negative)
49    }
50
51    pub fn abs(&self) -> u128 {
52        self.val
53    }
54
55    /// Given the bit width of a signed integer type, produces the minimum integer for
56    /// that type, i.e., -2^(bit_width - 1).
57    pub fn int_min(bit_width: u32) -> BigInt {
58        BigInt { sign: Sign::Negative, val: 1u128 << (bit_width - 1) }
59    }
60
61    /// Given the bit width of a signed integer type, produces the maximum integer for
62    /// that type, i.e., 2^(bit_width - 1) - 1.
63    pub fn int_max(bit_width: u32) -> BigInt {
64        (i128::MAX >> (128 - bit_width)).into()
65    }
66
67    /// Given the bit width of an unsigned integer type, produces the maximum
68    /// unsigned integer for that type, i.e., 2^bit_width - 1.
69    pub fn uint_max(bit_width: u32) -> BigInt {
70        (u128::MAX >> (128 - bit_width)).into()
71    }
72}
73
74impl From<usize> for BigInt {
75    fn from(val: usize) -> Self {
76        BigInt { sign: Sign::NonNegative, val: val as u128 }
77    }
78}
79
80impl From<u128> for BigInt {
81    fn from(val: u128) -> Self {
82        BigInt { sign: Sign::NonNegative, val }
83    }
84}
85
86impl From<i128> for BigInt {
87    fn from(val: i128) -> Self {
88        let sign = if val < 0 { Sign::Negative } else { Sign::NonNegative };
89        BigInt { sign, val: val.unsigned_abs() }
90    }
91}
92
93impl From<i32> for BigInt {
94    fn from(val: i32) -> Self {
95        // TODO(nilehmann) use Flux to prove this doesn't overflow
96        if val < 0 {
97            BigInt { sign: Sign::Negative, val: -(val as i64) as u128 }
98        } else {
99            BigInt { sign: Sign::NonNegative, val: val as u128 }
100        }
101    }
102}
103
104impl From<u32> for BigInt {
105    fn from(val: u32) -> Self {
106        BigInt { sign: Sign::NonNegative, val: val as u128 }
107    }
108}
109
110impl From<u64> for BigInt {
111    fn from(val: u64) -> Self {
112        BigInt { sign: Sign::NonNegative, val: val as u128 }
113    }
114}
115
116impl fmt::Display for BigInt {
117    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
118        match self.sign {
119            Sign::NonNegative => write!(f, "{}", self.val),
120            Sign::Negative => write!(f, "-{}", self.val),
121        }
122    }
123}
flux_middle/big_int.rs

flux_middle/
big_int.rs
