bv-0.2.2: Bit-vector arithmetic library

Maintainer Iago Abal None

Data.BitVector

Description

Implementation of bit-vectors as wrappers over `Integer`.

• Bit-vectors are interpreted as unsigned integers (i.e. natural numbers) except for some very specific cases.
• Bit-vectors are size-polymorphic insofar as most operations treat a bit-vector of size n as of size m for m >= n if required.

For documentation purposes we will write `[n]k` to denote a bit-vector of size `n` representing the natural number `k`.

Synopsis

# Bit-vectors

type BitVector = BVSource

An alias for `BV`.

data BV Source

Big-endian pseudo size-polymorphic bit-vectors.

Instances

 Enum BV Eq BV Integral BV Data BV Num BV Ord BV Real BV Show BV Typeable BV Bits BV

size :: BV -> IntSource

The size of a bit-vector.

width :: BV -> IntSource

An alias for `size`.

The value of a bit-vector, as a natural number.

An alias for `nat`.

2's complement value of a bit-vector.

# Creation

bitVec :: Integral a => Int -> a -> BVSource

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
```

ones :: Int -> BVSource

zeros :: Int -> BVSource

# Test

Test if the signed value of a bit-vector is a natural number.

Test if the signed value of a bit-vector is a positive number.

# Comparison

(==.) :: BV -> BV -> BoolSource

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
```

(/=.) :: BV -> BV -> BoolSource

Fixed-size inequality.

The negated version of `==.`.

(<.) :: BV -> BV -> BoolSource

Fixed-size less-than.

(<=.) :: BV -> BV -> BoolSource

Fixed-size less-than-or-equals.

(>.) :: BV -> BV -> BoolSource

Fixed-size greater-than.

(>=.) :: BV -> BV -> BoolSource

Fixed-size greater-than-or-equals.

slt :: BV -> BV -> BoolSource

Fixed-size signed less-than.

sle :: BV -> BV -> BoolSource

Fixed-size signed less-than-or-equals.

sgt :: BV -> BV -> BoolSource

Fixed-size signed greater-than.

sge :: BV -> BV -> BoolSource

Fixed-size signed greater-than-or-equals.

# Indexing

(@.) :: Integral ix => BV -> ix -> BoolSource

Bit indexing.

`u @. i` stands for the i-th bit of u.

````>>> ````[4]2 @. 0
```False
```
````>>> ````[4]2 @. 1
```True
```

index :: Integral ix => ix -> BV -> BoolSource

`index i a == a @. i`

(@@) :: Integral ix => BV -> (ix, ix) -> BVSource

Bit-string extraction.

`u @@ (j,i) == fromBits (map (u @.) [j,j-1..i])`
````>>> ````[4]7 @@ (3,1)
```[3]3
```

extract :: Integral ix => ix -> ix -> BV -> BVSource

`extract j i a == a @@ (j,i)`

(!.) :: Integral ix => BV -> ix -> BoolSource

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 -> BVSource

Take least significant bits.

`least m u == u @@ (m-1,0)`

most :: Integral ix => ix -> BV -> BVSource

Take most significant bits.

`most m u == u @@ (n-1,n-m)`

msb :: BV -> BoolSource

Most significant bit.

`msb u == u !. 0`

lsb :: BV -> BoolSource

Least significant bit.

`lsb u == u @. 0`

msb1 :: BV -> IntSource

Most significant 1-bit.

Pre: input must be non-zero.

````>>> ````msb1 [4]2
```1
```
````>>> ````msb1 [4]4
```2
```

# Arithmetic

signumI :: Integral a => BV -> aSource

Bit-vector `signum` as an `Integral`.

sdiv :: BV -> BV -> BVSource

2's complement signed division.

srem :: BV -> BV -> BVSource

2's complement signed remainder (sign follows dividend).

smod :: BV -> BV -> BVSource

2's complement signed remainder (sign follows divisor).

lg2 :: BV -> BVSource

Ceiling logarithm base 2.

Pre: input bit-vector must be non-zero.

# List-like operations

(#) :: BV -> BV -> BVSource

Concatenation of two bit-vectors.

cat :: BV -> BV -> BVSource

Concatenation of two bit-vectors.

zeroExtend :: Integral size => size -> BV -> BVSource

Logical extension.

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

signExtend :: Integral size => size -> BV -> BVSource

Arithmetic extension.

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

foldl_ :: (a -> Bool -> a) -> a -> BV -> aSource

`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 -> aSource

`foldr_ f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))`
`foldr_ f e = fromBits . foldr f e . toBits`
`reverse_ == fromBits . reverse . toBits`

replicate_ :: Integral size => size -> BV -> BVSource

Pre: if `replicate_ n u` then `n > 0` must hold.

`replicate_ n == fromBits . concat . replicate n . toBits`

and_ :: [BV] -> BVSource

Conjunction.

`and_ == foldr1 (.&.)`

or_ :: [BV] -> BVSource

Disjunction.

`or_ == foldr1 (.|.)`

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]
```

join :: [BV] -> BVSource

Concatenate a list of bit-vectors.

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

# Bitwise operations

module Data.Bits

not_ :: BV -> BVSource

An alias for `complement`.

nand :: BV -> BV -> BVSource

Negated `.&.`.

nor :: BV -> BV -> BVSource

Negated `.|.`.

xnor :: BV -> BV -> BVSource

Negated `xor`.

(<<.) :: BV -> BV -> BVSource

Left shift.

shl :: BV -> BV -> BVSource

Left shift.

(>>.) :: BV -> BV -> BVSource

Logical right shift.

shr :: BV -> BV -> BVSource

Logical right shift.

ashr :: BV -> BV -> BVSource

Arithmetic right shift

(<<<.) :: BV -> BV -> BVSource

Rotate left.

rol :: BV -> BV -> BVSource

Rotate left.

(>>>.) :: BV -> BV -> BVSource

Rotate right.

ror :: BV -> BV -> BVSource

Rotate right.

# Conversion

Create a bit-vector from a single bit.

fromBits :: [Bool] -> BVSource

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]
```

# Pretty-printing

Show a bit-vector in binary form.

Show a bit-vector in octal form.

Show a bit-vector in hexadecimal form.

# Utilities

maxNat :: (Integral a, Integral b) => a -> bSource

Greatest natural number representable with n bits.

Minimum width of a bit-vector to represent a given integer number.

````>>> ````integerWith 4
```3
```
````>>> ````integerWith (-4)
```4
```