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.

`>>>`

[4]3`bitVec 4 3`

This function also handles negative values.

`>>>`

[4]15`bitVec 4 (-1)`

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]1, [2]3, [3]5 ]`[1,3,5] :: [BV]`

Sometimes we want to specify a list of bit-vectors literals of the same
size, and for that we can use `bitVects`

:

`>>>`

[ [3]1, [3]3, [3]5 ]`bitVecs 3 [1,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.

`>>>`

False`[n]k ==. [m]k`

`>>>`

True`[n]k ==. [n]k`

# Indexing

(@.) :: Integral ix => BV -> ix -> Bool infixl 9 Source #

Bit indexing.

`u @. i`

stands for the *i*-th bit of *u*.

`>>>`

False`[4]2 @. 0`

`>>>`

True`[4]2 @. 1`

(@@) :: Integral ix => BV -> (ix, ix) -> BV infixl 9 Source #

Bit-string extraction.

u @@ (j,i) == fromBits (map (u @.) [j,j-1..i])

`>>>`

[3]3`[4]7 @@ (3,1)`

(@:) :: 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)

`>>>`

False`[3]3 !. 0`

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.

`>>>`

1`msb1 [4]2`

`>>>`

2`msb1 [4]4`

Least significant 1-bit.

*Pre*: input must be non-zero.

`>>>`

0`msb1 [4]3`

`>>>`

1`msb1 [4]6`

# 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.

`>>>`

[4]1`zeroExtend 3 [1]1`

signExtend :: Integral size => size -> BV -> BV Source #

Arithmetic extension.

`>>>`

[4]1`signExtend 2 [2]1`

`>>>`

[4]15`signExtend 2 [2]3`

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.

`>>>`

[[2]0,[2]3,[2]3]`split 3 [4]15`

group :: Integral size => size -> BV -> [BV] Source #

Split a bit-vector into *n*-wide pieces.

`>>>`

[[3]1,[3]7]`group 3 [4]15`

group_ :: Integral size => size -> BV -> [BV] Source #

Deprecated: Use corresponding versions without underscore

Split a bit-vector into *n*-wide pieces.

`>>>`

[[3]1,[3]7]`group 3 [4]15`

Concatenate a (possibly empty) list of bit-vectors.

`>>>`

[4]14`join [[2]3,[2]2]`

# 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.

`>>>`

[3]1`fromBits [False, False, True]`

toBits :: BV -> [Bool] Source #

Create a big-endian list of bits from a bit-vector.

`>>>`

[True, False, True, True]`toBits [4]11`