Copyright | (c) 2012-2016 Iago Abal (c) 2012-2013 HASLab & University of Minho |
---|---|
License | BSD3 |
Maintainer | Iago Abal <mail@iagoabal.eu> |
Safe Haskell | None |
Language | Haskell98 |
Bit-vector arithmetic inspired by SMT-LIB http://smt-lib.org/ and Cryptol http://cryptol.net/.
Bit-vectors are represented as a pair size and value,
where sizes are of type Int
and values are Integer
.
- Bit-vectors are interpreted as unsigned integers (i.e. natural numbers) except for some specific signed operations.
- Most operations are in some way size-polymorphic and, if required, will perform padding to adjust the size of input bit-vectors.
For documentation purposes we will write [n]k
to denote a bit-vector
of size n
representing the natural number k
.
- type BitVector = BV
- data BV
- size :: BV -> Int
- width :: BV -> Int
- nat :: BV -> Integer
- uint :: BV -> Integer
- int :: BV -> Integer
- nil :: BV
- bitVec :: Integral a => Int -> a -> BV
- bitVecs :: Integral a => Int -> [a] -> [BV]
- ones :: Int -> BV
- zeros :: Int -> BV
- isNat :: BV -> Bool
- isPos :: BV -> Bool
- (==.) :: BV -> BV -> Bool
- (/=.) :: BV -> BV -> Bool
- (<.) :: BV -> BV -> Bool
- (<=.) :: BV -> BV -> Bool
- (>.) :: BV -> BV -> Bool
- (>=.) :: BV -> BV -> Bool
- slt :: BV -> BV -> Bool
- sle :: BV -> BV -> Bool
- sgt :: BV -> BV -> Bool
- sge :: BV -> BV -> Bool
- (@.) :: Integral ix => BV -> ix -> Bool
- index :: Integral ix => ix -> BV -> Bool
- (@@) :: Integral ix => BV -> (ix, ix) -> BV
- extract :: Integral ix => ix -> ix -> BV -> BV
- (@:) :: Integral ix => BV -> [ix] -> BV
- (!.) :: Integral ix => BV -> ix -> Bool
- least :: Integral ix => ix -> BV -> BV
- most :: Integral ix => ix -> BV -> BV
- msb :: BV -> Bool
- lsb :: BV -> Bool
- msb1 :: BV -> Int
- lsb1 :: BV -> Int
- signumI :: Integral a => BV -> a
- pow :: Integral exp => BV -> exp -> BV
- sdiv :: BV -> BV -> BV
- srem :: BV -> BV -> BV
- smod :: BV -> BV -> BV
- lg2 :: BV -> BV
- (#) :: BV -> BV -> BV
- cat :: BV -> BV -> BV
- append :: BV -> BV -> BV
- concat :: [BV] -> BV
- zeroExtend :: Integral size => size -> BV -> BV
- signExtend :: Integral size => size -> BV -> BV
- foldl :: (a -> Bool -> a) -> a -> BV -> a
- foldl_ :: (a -> Bool -> a) -> a -> BV -> a
- foldr :: (Bool -> a -> a) -> a -> BV -> a
- foldr_ :: (Bool -> a -> a) -> a -> BV -> a
- reverse :: BV -> BV
- reverse_ :: BV -> BV
- replicate :: Integral size => size -> BV -> BV
- replicate_ :: Integral size => size -> BV -> BV
- and :: [BV] -> BV
- and_ :: [BV] -> BV
- or :: [BV] -> BV
- or_ :: [BV] -> BV
- split :: Integral times => times -> BV -> [BV]
- group :: Integral size => size -> BV -> [BV]
- group_ :: Integral size => size -> BV -> [BV]
- join :: [BV] -> BV
- not :: BV -> BV
- not_ :: BV -> BV
- nand :: BV -> BV -> BV
- nor :: BV -> BV -> BV
- xnor :: BV -> BV -> BV
- (<<.) :: BV -> BV -> BV
- shl :: BV -> BV -> BV
- (>>.) :: BV -> BV -> BV
- shr :: BV -> BV -> BV
- ashr :: BV -> BV -> BV
- (<<<.) :: BV -> BV -> BV
- rol :: BV -> BV -> BV
- (>>>.) :: BV -> BV -> BV
- ror :: BV -> BV -> BV
- fromBool :: Bool -> BV
- fromBits :: [Bool] -> BV
- toBits :: BV -> [Bool]
- showBin :: BV -> String
- showOct :: BV -> String
- showHex :: BV -> String
Bit-vectors
Big-endian pseudo size-polymorphic bit-vectors.
Creation
bitVec :: Integral a => Int -> a -> BV Source #
Create a bit-vector given a size and an integer value.
>>>
bitVec 4 3
[4]3
This function also handles negative values.
>>>
bitVec 4 (-1)
[4]15
bitVecs :: Integral a => Int -> [a] -> [BV] Source #
List of bit-vector literals of the same size
When a list of integer literals is interpreted as a list of bit-vectors,
fromInteger
is applied to each element invidually:
>>>
[1,3,5] :: [BV]
[ [1]1, [2]3, [3]5 ]
Sometimes we want to specify a list of bit-vectors literals of the same
size, and for that we can use bitVects
:
>>>
bitVecs 3 [1,3,5]
[ [3]1, [3]3, [3]5 ]
Test
Comparison
(==.) :: BV -> BV -> Bool infix 4 Source #
Fixed-size equality.
In contrast with ==
, which is size-polymorphic, this equality
requires both bit-vectors to be of equal size.
>>>
[n]k ==. [m]k
False
>>>
[n]k ==. [n]k
True
Indexing
(@.) :: Integral ix => BV -> ix -> Bool infixl 9 Source #
Bit indexing.
u @. i
stands for the i-th bit of u.
>>>
[4]2 @. 0
False
>>>
[4]2 @. 1
True
(@@) :: Integral ix => BV -> (ix, ix) -> BV infixl 9 Source #
Bit-string extraction.
u @@ (j,i) == fromBits (map (u @.) [j,j-1..i])
>>>
[4]7 @@ (3,1)
[3]3
(@:) :: Integral ix => BV -> [ix] -> BV infixl 9 Source #
Bit list indexing.
u @: is ==. fromBits $ List.map (u @.) is
(!.) :: Integral ix => BV -> ix -> Bool infixl 9 Source #
Reverse bit-indexing.
Index starting from the most significant bit.
u !. i == u @. (size u - i - 1)
>>>
[3]3 !. 0
False
least :: Integral ix => ix -> BV -> BV Source #
Take least significant bits.
least m u == u @@ (m-1,0)
Most significant 1-bit.
Pre: input must be non-zero.
>>>
msb1 [4]2
1
>>>
msb1 [4]4
2
Least significant 1-bit.
Pre: input must be non-zero.
>>>
msb1 [4]3
0
>>>
msb1 [4]6
1
Arithmetic
pow :: Integral exp => BV -> exp -> BV Source #
Bit-vector exponentiation.
pow [n]k e
computes k
raised to e
modulo n
.
This is faster than Haskell's (^) operator because it performs
modulo division just once. Besides, a^0 == [1]0
!!!
List-like operations
cat :: BV -> BV -> BV Source #
Deprecated: Use (#) or append instead
Concatenation of two bit-vectors.
zeroExtend :: Integral size => size -> BV -> BV Source #
Logical extension.
>>>
zeroExtend 3 [1]1
[4]1
signExtend :: Integral size => size -> BV -> BV Source #
Arithmetic extension.
>>>
signExtend 2 [2]1
[4]1
>>>
signExtend 2 [2]3
[4]15
foldl :: (a -> Bool -> a) -> a -> BV -> a Source #
foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
foldl f e = fromBits . foldl f e . toBits
foldl_ :: (a -> Bool -> a) -> a -> BV -> a Source #
Deprecated: Use corresponding versions without underscore
foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
foldl f e = fromBits . foldl f e . toBits
foldr :: (Bool -> a -> a) -> a -> BV -> a Source #
foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
foldr f e = fromBits . foldr f e . toBits
foldr_ :: (Bool -> a -> a) -> a -> BV -> a Source #
Deprecated: Use corresponding versions without underscore
foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
foldr f e = fromBits . foldr f e . toBits
Deprecated: Use corresponding versions without underscore
reverse == fromBits . reverse . toBits
replicate :: Integral size => size -> BV -> BV Source #
Pre: if replicate_ n u
then n > 0
must hold.
replicate_ n == fromBits . concat . replicate n . toBits
replicate_ :: Integral size => size -> BV -> BV Source #
Deprecated: Use corresponding versions without underscore
Pre: if replicate_ n u
then n > 0
must hold.
replicate_ n == fromBits . concat . replicate n . toBits
Conjunction.
Essentially, and == foldr1 (.&.)
.
Returns [1]1
if the input list is empty.
Deprecated: Use corresponding versions without underscore
Conjunction.
Essentially, and == foldr1 (.&.)
.
Returns [1]1
if the input list is empty.
Disjunction.
Essentially, or == foldr1 (.|.)
.
Returns [1]0
if the input list is empty.
Deprecated: Use corresponding versions without underscore
Disjunction.
Essentially, or == foldr1 (.|.)
.
Returns [1]0
if the input list is empty.
split :: Integral times => times -> BV -> [BV] Source #
Split a bit-vector k times.
>>>
split 3 [4]15
[[2]0,[2]3,[2]3]
group :: Integral size => size -> BV -> [BV] Source #
Split a bit-vector into n-wide pieces.
>>>
group 3 [4]15
[[3]1,[3]7]
group_ :: Integral size => size -> BV -> [BV] Source #
Deprecated: Use corresponding versions without underscore
Split a bit-vector into n-wide pieces.
>>>
group 3 [4]15
[[3]1,[3]7]
Concatenate a (possibly empty) list of bit-vectors.
>>>
join [[2]3,[2]2]
[4]14
Bitwise operations
Deprecated: Use corresponding versions without underscore
An alias for complement
.
Conversion
fromBits :: [Bool] -> BV Source #
Create a bit-vector from a big-endian list of bits.
>>>
fromBits [False, False, True]
[3]1
toBits :: BV -> [Bool] Source #
Create a big-endian list of bits from a bit-vector.
>>>
toBits [4]11
[True, False, True, True]