crucible/
bitvector.rs

1use core::cmp::Ordering;
2use core::intrinsics;
3use core::marker::PhantomData;
4use core::ops::{Neg, Not, Add, Sub, Mul, Div, Rem, BitAnd, BitOr, BitXor, Shl, Shr};
5
6use crate::symbolic::Symbolic;
7
8/// An unsigned integer (bitvector), whose size is indicated by the type parameter `S`.
9pub struct Bv<S: Size + ?Sized> {
10    _dummy: u8,
11    _marker: PhantomData<S>,
12}
13
14pub trait Size {
15    fn make_symbolic(desc: &str) -> Bv<Self>;
16}
17
18pub struct _128;
19impl Size for _128 {
20    fn make_symbolic(desc: &str) -> Bv<Self> { make_symbolic_128(desc) }
21}
22
23pub struct _256;
24impl Size for _256 {
25    fn make_symbolic(desc: &str) -> Bv<Self> { make_symbolic_256(desc) }
26}
27
28pub struct _512;
29impl Size for _512 {
30    fn make_symbolic(desc: &str) -> Bv<Self> { make_symbolic_512(desc) }
31}
32
33
34/// An unsigned 128-bit integer.
35pub type Bv128 = Bv<_128>;
36/// An unsigned 256-bit integer.
37pub type Bv256 = Bv<_256>;
38/// An unsigned 512-bit integer.
39pub type Bv512 = Bv<_512>;
40
41
42impl<S: Size> Bv<S> {
43    // Defining overrides for constants is tricky: rustc will const-evaluate based on the
44    // definition, and crux-mir will only see the actual struct literal, not the name of the
45    // constant.  Here we handle it by setting a different value for `_dummy` in each constant, so
46    // that code in crux-mir can distinguish them.
47    //
48    // Note there are no `const fn`s defined on this type - those would make things a lot more
49    // difficult.
50    pub const ZERO: Self = Bv { _dummy: 0, _marker: PhantomData };
51    pub const ONE: Self = Bv { _dummy: 1, _marker: PhantomData };
52    pub const MAX: Self = Bv { _dummy: 2, _marker: PhantomData };
53}
54
55
56/// Arbitrary bitvector-to-bitvector conversion.  Either truncates or zero-extends depending on the
57/// relative sizes of `T` and `U`.  Both `T` and `U` must be represented as  bitvectors (`BVType`)
58/// at the Crucible level, which is the case for both `Bv` and primitive integer types.  (Note that
59/// this still zero-extends when used on signed integers: `convert::<i8, i16>(-1)` return `255`,
60/// not `-1`.)
61pub fn convert<T, U>(x: T) -> U {
62    unimplemented!()
63}
64
65macro_rules! impl_from_bv {
66    ($($S1:ty, $S2:ty;)*) => {
67        $(
68            impl From<Bv<$S1>> for Bv<$S2> {
69                fn from(x: Bv<$S1>) -> Bv<$S2> {
70                    convert(x)
71                }
72            }
73        )*
74    };
75}
76
77impl_from_bv! {
78    _128, _256;
79    _128, _512;
80    _256, _128;
81    _256, _512;
82    _512, _128;
83    _512, _256;
84}
85
86macro_rules! impl_into_prim {
87    ($($T:ty),*) => {
88        $(
89            impl<S: Size> From<Bv<S>> for $T {
90                fn from(x: Bv<S>) -> $T {
91                    convert(x)
92                }
93            }
94        )*
95    };
96}
97
98macro_rules! impl_from_into_prim {
99    ($($T:ty),*) => {
100        $(
101            impl<S: Size> From<$T> for Bv<S> {
102                fn from(x: $T) -> Bv<S> {
103                    convert(x)
104                }
105            }
106        )*
107        impl_into_prim!($($T),*);
108    };
109}
110
111macro_rules! impl_from_into_prim_signed {
112    ($($T:ty),*) => {
113        $(
114            impl<S: Size> From<$T> for Bv<S> {
115                fn from(x: $T) -> Bv<S> {
116                    assert!(x >= 0, "can't convert negative integer to unsigned bitvector");
117                    convert(x)
118                }
119            }
120        )*
121        impl_into_prim!($($T),*);
122    };
123}
124
125impl_from_into_prim!(u8, u16, u32, u64, u128, usize);
126impl_from_into_prim_signed!(i8, i16, i32, i64, i128, isize);
127
128
129macro_rules! impl_unops {
130    ($($Op:ident, $op:ident;)*) => {
131        $(
132            impl<S: Size> $Op for Bv<S> {
133                type Output = Bv<S>;
134                fn $op(self) -> Bv<S> {
135                    unimplemented!()
136                }
137            }
138        )*
139    };
140}
141
142macro_rules! impl_binops {
143    ($($Op:ident, $op:ident;)*) => {
144        $(
145            impl<S: Size> $Op<Bv<S>> for Bv<S> {
146                type Output = Bv<S>;
147                fn $op(self, other: Bv<S>) -> Bv<S> {
148                    unimplemented!()
149                }
150            }
151        )*
152    };
153}
154
155macro_rules! impl_shift_ops {
156    ($($Op:ident, $op:ident;)*) => {
157        $(
158            // Crucible shift ops require the shift amount and value use the same bitvector width,
159            // so we convert `usize` to the right `Bv` type before calling the real shift function.
160
161            fn $op<S: Size>(x: Bv<S>, y: Bv<S>) -> Bv<S> {
162                unimplemented!()
163            }
164
165            impl<S: Size> $Op<usize> for Bv<S> {
166                type Output = Bv<S>;
167                fn $op(self, shift: usize) -> Bv<S> {
168                    $op(self, shift.into())
169                }
170            }
171        )*
172    };
173}
174
175impl_unops! {
176    Not, not;
177}
178
179impl_binops! {
180    Add, add;
181    Sub, sub;
182    Mul, mul;
183    Div, div;
184    Rem, rem;
185    BitAnd, bitand;
186    BitOr, bitor;
187    BitXor, bitxor;
188}
189
190impl_shift_ops! {
191    Shl, shl;
192    Shr, shr;
193}
194
195
196impl<S: Size> Bv<S> {
197    pub fn overflowing_add(self, other: Bv<S>) -> (Bv<S>, bool) {
198        unimplemented!()
199    }
200
201    pub fn overflowing_sub(self, other: Bv<S>) -> (Bv<S>, bool) {
202        unimplemented!()
203    }
204
205    pub fn overflowing_mul(self, other: Bv<S>) -> (Bv<S>, bool) {
206        unimplemented!()
207    }
208
209    pub fn leading_zeros(self) -> u32 {
210        unimplemented!()
211    }
212}
213
214
215impl<S: Size> Clone for Bv<S> {
216    fn clone(&self) -> Bv<S> {
217        *self
218    }
219}
220
221impl<S: Size> Copy for Bv<S> {}
222
223impl<S: Size> PartialEq<Bv<S>> for Bv<S> {
224    fn eq(&self, other: &Bv<S>) -> bool {
225        unimplemented!()
226    }
227}
228
229impl<S: Size> Eq for Bv<S> {}
230
231impl<S: Size> PartialOrd<Bv<S>> for Bv<S> {
232    fn partial_cmp(&self, other: &Bv<S>) -> Option<Ordering> {
233        Some(self.cmp(other))
234    }
235
236    fn lt(&self, other: &Bv<S>) -> bool {
237        unimplemented!()
238    }
239}
240
241impl<S: Size> Ord for Bv<S> {
242    fn cmp(&self, other: &Bv<S>) -> Ordering {
243        if self.eq(other) { Ordering::Equal }
244        else if self.lt(other) { Ordering::Less }
245        else { Ordering::Greater }
246    }
247}
248
249impl<S: Size> Symbolic for Bv<S> {
250    fn symbolic(desc: &str) -> Bv<S> {
251        S::make_symbolic(desc)
252    }
253}
254
255// Override hooks for constructing symbolic bitvectors.
256fn make_symbolic_128(desc: &str) -> Bv<_128> { unimplemented!() }
257fn make_symbolic_256(desc: &str) -> Bv<_256> { unimplemented!() }
258fn make_symbolic_512(desc: &str) -> Bv<_512> { unimplemented!() }
crucible/bitvector.rs

crucible/
bitvector.rs
