Data.BitVector

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.

Bit-vectors

type BitVector = BV

An alias for BV.

data BV

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

The size of a bit-vector.

width :: BV -> Int

An alias for size.

nat :: BV -> Integer

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

uint :: BV -> Integer

An alias for nat.

int :: BV -> Integer

2's complement value of a bit-vector.

Creation

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

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

Create a mask of ones.

zeros :: Int -> BV

Create a mask of zeros.

Comparison

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

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

Fixed-size inequality.

The negated version of ==..

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

Fixed-size less-than.

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

Fixed-size less-than-or-equals.

(>.) :: BV -> BV -> Bool

Fixed-size greater-than.

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

Fixed-size greater-than-or-equals.

slt :: BV -> BV -> Bool

Fixed-size signed less-than.

sle :: BV -> BV -> Bool

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

sgt :: BV -> BV -> Bool

Fixed-size signed greater-than.

sge :: BV -> BV -> Bool

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

Indexing

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

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

index i a == a @. i

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

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

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

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

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

Take least significant bits.

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

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

Take most significant bits.

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

msb :: BV -> Bool

Most significant bit.

msb u == u !. 0

lsb :: BV -> Bool

Least significant bit.

lsb u == u @. 0

msb1 :: BV -> Int

Most significant 1-bit.

Pre: input must be non-zero.

>>> msb1 [4]2
1

>>> msb1 [4]4
2

Arithmetic

sdiv :: BV -> BV -> BV

2's complement signed division.

srem :: BV -> BV -> BV

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

smod :: BV -> BV -> BV

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

lg2 :: BV -> BV

Ceiling logarithm base 2.

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

List-like operations

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

Concatenation of two bit-vectors.

cat :: BV -> BV -> BV

Concatenation of two bit-vectors.

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

Logical extension.

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

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

Arithmetic extension.

>>> signExtend 2 [2]1
[4]1

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

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

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

foldr_ f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))

foldr_ f e = fromBits . foldr f e . toBits

reverse_ :: BV -> BV

reverse_ == fromBits . reverse . toBits

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

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

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

and_ :: [BV] -> BV

Conjunction.

and_ == foldr1 (.&.)

or_ :: [BV] -> BV

Disjunction.

or_ == foldr1 (.|.)

split :: Integral times => times -> BV -> [BV]

Split a bit-vector k times.

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

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

Split a bit-vector into n-wide pieces.

>>> group_ 3 [4]15
[[3]1,[3]7]

join :: [BV] -> BV

Concatenate a list of bit-vectors.

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

Bitwise operations

module Data.Bits

not_ :: BV -> BV

An alias for complement.

nand :: BV -> BV -> BV

Negated .&..

nor :: BV -> BV -> BV

Negated .|..

xnor :: BV -> BV -> BV

Negated xor.

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

Left shift.

shl :: BV -> BV -> BV

Left shift.

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

Logical right shift.

shr :: BV -> BV -> BV

Logical right shift.

ashr :: BV -> BV -> BV

Arithmetic right shift

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

Rotate left.

rol :: BV -> BV -> BV

Rotate left.

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

Rotate right.

ror :: BV -> BV -> BV

Rotate right.

Conversion

fromBool :: Bool -> BV

Create a bit-vector from a single bit.

fromBits :: [Bool] -> BV

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

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

toBits :: BV -> [Bool]

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

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

Pretty-printing

showBin :: BV -> String

Show a bit-vector in binary form.

showOct :: BV -> String

Show a bit-vector in octal form.

showHex :: BV -> String

Show a bit-vector in hexadecimal form.

Utilities

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

Greatest natural number representable with n bits.

integerWidth :: Integer -> Int

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

>>> integerWith 4
3

>>> integerWith (-4)
4