bv-0.5: Bit-vector arithmetic library

Copyright (c) 2012-2016 Iago Abal(c) 2012-2013 HASLab & University of Minho BSD3 Iago Abal None Haskell98

Data.BitVector

Description

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.

Synopsis

# Bit-vectors

type BitVector = BV Source #

An alias for BV.

data BV Source #

Big-endian pseudo size-polymorphic bit-vectors.

Instances

size :: BV -> Int Source #

The size of a bit-vector.

width :: BV -> Int Source #

An alias for size.

nat :: BV -> Integer Source #

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

uint :: BV -> Integer Source #

An alias for nat.

int :: BV -> Integer Source #

2's complement value of a bit-vector.

>>> int 3
-1

>>> int 12
-4


# Creation

The empty bit-vector, ie. 0.

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

Create a bit-vector given a size and an integer value.

>>> bitVec 4 3
3


This function also handles negative values.

>>> bitVec 4 (-1)
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, 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]
[ 1, 3, 5 ]


ones :: Int -> BV Source #

Create a mask of ones.

zeros :: Int -> BV Source #

Create a mask of zeros.

# Test

isNat :: BV -> Bool Source #

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

isPos :: BV -> Bool Source #

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

# 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


(/=.) :: BV -> BV -> Bool infix 4 Source #

Fixed-size inequality.

The negated version of ==..

(<.) :: BV -> BV -> Bool infix 4 Source #

Fixed-size less-than.

(<=.) :: BV -> BV -> Bool infix 4 Source #

Fixed-size less-than-or-equals.

(>.) :: BV -> BV -> Bool infix 4 Source #

Fixed-size greater-than.

(>=.) :: BV -> BV -> Bool infix 4 Source #

Fixed-size greater-than-or-equals.

slt :: BV -> BV -> Bool infix 4 Source #

Fixed-size signed less-than.

sle :: BV -> BV -> Bool infix 4 Source #

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

sgt :: BV -> BV -> Bool infix 4 Source #

Fixed-size signed greater-than.

sge :: BV -> BV -> Bool infix 4 Source #

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

# Indexing

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

Bit indexing.

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

>>> 2 @. 0
False

>>> 2 @. 1
True


index :: Integral ix => ix -> BV -> Bool Source #

index i a == a @. i

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

Bit-string extraction.

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


extract :: Integral ix => ix -> ix -> BV -> BV Source #

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

(@:) :: 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 !. 0
False


least :: Integral ix => ix -> BV -> BV Source #

Take least significant bits.

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

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

Take most significant bits.

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

msb :: BV -> Bool Source #

Most significant bit.

msb u == u !. 0

lsb :: BV -> Bool Source #

Least significant bit.

lsb u == u @. 0

msb1 :: BV -> Int Source #

Most significant 1-bit.

Pre: input must be non-zero.

>>> msb1 2
1

>>> msb1 4
2


lsb1 :: BV -> Int Source #

Least significant 1-bit.

Pre: input must be non-zero.

>>> msb1 3
0

>>> msb1 6
1


# Arithmetic

signumI :: Integral a => BV -> a Source #

Bit-vector signum as an Integral.

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 == 0 !!!

sdiv :: BV -> BV -> BV Source #

2's complement signed division.

srem :: BV -> BV -> BV Source #

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

smod :: BV -> BV -> BV Source #

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

lg2 :: BV -> BV Source #

Ceiling logarithm base 2.

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

# List-like operations

(#) :: BV -> BV -> BV infixr 5 Source #

Concatenation of two bit-vectors.

cat :: BV -> BV -> BV Source #

Deprecated: Use (#) or append instead

Concatenation of two bit-vectors.

append :: BV -> BV -> BV Source #

Concatenation of two bit-vectors.

concat :: [BV] -> BV Source #

An alias for join.

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

Logical extension.

>>> zeroExtend 3 1
1


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

Arithmetic extension.

>>> signExtend 2 1
1

>>> signExtend 2 3
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
reverse == fromBits . reverse . 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

and :: [BV] -> BV Source #

Conjunction.

Essentially, and == foldr1 (.&.).

Returns 1 if the input list is empty.

and_ :: [BV] -> BV Source #

Deprecated: Use corresponding versions without underscore

Conjunction.

Essentially, and == foldr1 (.&.).

Returns 1 if the input list is empty.

or :: [BV] -> BV Source #

Disjunction.

Essentially, or == foldr1 (.|.).

Returns 0 if the input list is empty.

or_ :: [BV] -> BV Source #

Deprecated: Use corresponding versions without underscore

Disjunction.

Essentially, or == foldr1 (.|.).

Returns 0 if the input list is empty.

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

Split a bit-vector k times.

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


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

Split a bit-vector into n-wide pieces.

>>> group 3 15
[1,7]


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

Deprecated: Use corresponding versions without underscore

Split a bit-vector into n-wide pieces.

>>> group 3 15
[1,7]


join :: [BV] -> BV Source #

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

>>> join [3,2]
14


# Bitwise operations

not :: BV -> BV Source #

An alias for complement.

not_ :: BV -> BV Source #

Deprecated: Use corresponding versions without underscore

An alias for complement.

nand :: BV -> BV -> BV Source #

Negated .&..

nor :: BV -> BV -> BV Source #

Negated .|..

xnor :: BV -> BV -> BV Source #

Negated xor.

(<<.) :: BV -> BV -> BV infixl 8 Source #

Left shift.

shl :: BV -> BV -> BV infixl 8 Source #

Left shift.

(>>.) :: BV -> BV -> BV infixl 8 Source #

Logical right shift.

shr :: BV -> BV -> BV infixl 8 Source #

Logical right shift.

ashr :: BV -> BV -> BV infixl 8 Source #

Arithmetic right shift

(<<<.) :: BV -> BV -> BV infixl 8 Source #

Rotate left.

rol :: BV -> BV -> BV infixl 8 Source #

Rotate left.

(>>>.) :: BV -> BV -> BV infixl 8 Source #

Rotate right.

ror :: BV -> BV -> BV infixl 8 Source #

Rotate right.

# Conversion

fromBool :: Bool -> BV Source #

Create a bit-vector from a single bit.

fromBits :: [Bool] -> BV Source #

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

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


toBits :: BV -> [Bool] Source #

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

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


# Pretty-printing

showBin :: BV -> String Source #

Show a bit-vector in binary form.

showOct :: BV -> String Source #

Show a bit-vector in octal form.

showHex :: BV -> String Source #

Show a bit-vector in hexadecimal form.