Copyright | (c) Galois Inc. 2018 |
---|---|

License | BSD-3 |

Maintainer | Ben Selfridge <benselfridge@galois.com> |

Stability | experimental |

Portability | portable |

Safe Haskell | None |

Language | Haskell2010 |

This module defines a width-parameterized `BV`

type and various
associated operations. A

is a newtype around an `BV`

w`Integer`

, so
operations that require the width take an explicit

argument. We explicitly do not allow widths that cannot be represented
as an `NatRepr`

w`Int`

, as we appeal to the underlying `Num`

and
`Bits`

instances on `Integer`

for the implementation of many
of the same operations (which, in turn, require those widths to be
`Int`

s).

We omit all typeclass instances that require compile-time knowledge of
bitvector width, or force a signed or unsigned intepretation. Those
instances can be recovered via the use of
`SignedBV`

or
`UnsignedBV`

.

This module should be imported qualified, as many of the names clash with those in Prelude or other base packages.

## Synopsis

- data BV (w :: Nat) :: Type
- pattern BV :: Integer -> BV w
- data NatRepr (n :: Nat)
- knownNat :: forall (n :: Nat). KnownNat n => NatRepr n
- mkBV :: NatRepr w -> Integer -> BV w
- mkBVUnsigned :: NatRepr w -> Integer -> Maybe (BV w)
- mkBVSigned :: 1 <= w => NatRepr w -> Integer -> Maybe (BV w)
- unsignedClamp :: NatRepr w -> Integer -> BV w
- signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w
- minUnsigned :: NatRepr w -> BV w
- maxUnsigned :: NatRepr w -> BV w
- minSigned :: 1 <= w => NatRepr w -> BV w
- maxSigned :: 1 <= w => NatRepr w -> BV w
- zero :: NatRepr w -> BV w
- one :: 1 <= w => NatRepr w -> BV w
- width :: NatRepr w -> BV w
- bool :: Bool -> BV 1
- word8 :: Word8 -> BV 8
- word16 :: Word16 -> BV 16
- word32 :: Word32 -> BV 32
- word64 :: Word64 -> BV 64
- int8 :: Int8 -> BV 8
- int16 :: Int16 -> BV 16
- int32 :: Int32 -> BV 32
- int64 :: Int64 -> BV 64
- bitsBE :: [Bool] -> Pair NatRepr BV
- bitsLE :: [Bool] -> Pair NatRepr BV
- bytesBE :: [Word8] -> Pair NatRepr BV
- bytesLE :: [Word8] -> Pair NatRepr BV
- bytestringBE :: ByteString -> Pair NatRepr BV
- bytestringLE :: ByteString -> Pair NatRepr BV
- asSigned :: 1 <= w => NatRepr w -> BV w -> Integer
- asUnsigned :: BV w -> Integer
- asNatural :: BV w -> Natural
- asBitsBE :: NatRepr w -> BV w -> [Bool]
- asBitsLE :: NatRepr w -> BV w -> [Bool]
- asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]
- asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]
- asBytestringBE :: NatRepr w -> BV w -> Maybe ByteString
- asBytestringLE :: NatRepr w -> BV w -> Maybe ByteString
- and :: BV w -> BV w -> BV w
- or :: BV w -> BV w -> BV w
- xor :: BV w -> BV w -> BV w
- complement :: NatRepr w -> BV w -> BV w
- shl :: NatRepr w -> BV w -> Natural -> BV w
- lshr :: NatRepr w -> BV w -> Natural -> BV w
- ashr :: 1 <= w => NatRepr w -> BV w -> Natural -> BV w
- rotateL :: NatRepr w -> BV w -> Natural -> BV w
- rotateR :: NatRepr w -> BV w -> Natural -> BV w
- bit :: (ix + 1) <= w => NatRepr w -> NatRepr ix -> BV w
- bit' :: NatRepr w -> Natural -> BV w
- setBit :: (ix + 1) <= w => NatRepr ix -> BV w -> BV w
- setBit' :: NatRepr w -> Natural -> BV w -> BV w
- clearBit :: (ix + 1) <= w => NatRepr w -> NatRepr ix -> BV w -> BV w
- clearBit' :: NatRepr w -> Natural -> BV w -> BV w
- complementBit :: (ix + 1) <= w => NatRepr ix -> BV w -> BV w
- complementBit' :: NatRepr w -> Natural -> BV w -> BV w
- testBit :: (ix + 1) <= w => NatRepr ix -> BV w -> Bool
- testBit' :: Natural -> BV w -> Bool
- popCount :: BV w -> BV w
- ctz :: NatRepr w -> BV w -> BV w
- clz :: NatRepr w -> BV w -> BV w
- truncBits :: Natural -> BV w -> BV w
- add :: NatRepr w -> BV w -> BV w -> BV w
- sub :: NatRepr w -> BV w -> BV w -> BV w
- mul :: NatRepr w -> BV w -> BV w -> BV w
- uquot :: BV w -> BV w -> BV w
- squot :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- sdiv :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- urem :: BV w -> BV w -> BV w
- srem :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- smod :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- uquotRem :: BV w -> BV w -> (BV w, BV w)
- squotRem :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)
- sdivMod :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)
- abs :: 1 <= w => NatRepr w -> BV w -> BV w
- negate :: NatRepr w -> BV w -> BV w
- signBit :: 1 <= w => NatRepr w -> BV w -> BV w
- signum :: 1 <= w => NatRepr w -> BV w -> BV w
- slt :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool
- sle :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool
- ult :: BV w -> BV w -> Bool
- ule :: BV w -> BV w -> Bool
- umin :: BV w -> BV w -> BV w
- umax :: BV w -> BV w -> BV w
- smin :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- smax :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w
- concat :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
- select :: (ix + w') <= w => NatRepr ix -> NatRepr w' -> BV w -> BV w'
- select' :: Natural -> NatRepr w' -> BV w -> BV w'
- zext :: (w + 1) <= w' => NatRepr w' -> BV w -> BV w'
- sext :: (1 <= w, (w + 1) <= w') => NatRepr w -> NatRepr w' -> BV w -> BV w'
- trunc :: (w' + 1) <= w => NatRepr w' -> BV w -> BV w'
- trunc' :: NatRepr w' -> BV w -> BV w'
- mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
- succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
- succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
- predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
- predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
- enumFromToUnsigned :: BV w -> BV w -> [BV w]
- enumFromToSigned :: 1 <= w => NatRepr w -> BV w -> BV w -> [BV w]
- uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)
- uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)
- sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)
- ppHex :: NatRepr w -> BV w -> String
- ppBin :: NatRepr w -> BV w -> String
- ppOct :: NatRepr w -> BV w -> String
- ppDec :: NatRepr w -> BV w -> String

`BV`

type

data BV (w :: Nat) :: Type Source #

Bitvector datatype, parameterized by width.

#### Instances

EqF BV Source # | |

ShowF BV Source # | |

Lift (BV w :: Type) Source # | |

Eq (BV w) Source # | |

Ord (BV w) Source # | Uses an unsigned ordering, but |

Read (BV w) Source # | |

Show (BV w) Source # | |

Generic (BV w) Source # | |

NFData (BV w) Source # | |

Defined in Data.BitVector.Sized.Internal | |

Hashable (BV w) Source # | |

Defined in Data.BitVector.Sized.Internal | |

type Rep (BV w) Source # | |

Defined in Data.BitVector.Sized.Internal |

`NatRepr`

s (from parameterized-utils)

A runtime presentation of a type-level `Nat`

.

This can be used for performing dynamic checks on a type-level natural numbers.

#### Instances

TestEquality NatRepr | |

Defined in Data.Parameterized.NatRepr.Internal | |

DecidableEq NatRepr | |

OrdF NatRepr | |

Defined in Data.Parameterized.NatRepr.Internal compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool # ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool # geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool # gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool # | |

ShowF NatRepr | |

HashableF NatRepr | |

Defined in Data.Parameterized.NatRepr.Internal | |

KnownNat n => KnownRepr NatRepr (n :: Nat) | |

Defined in Data.Parameterized.NatRepr.Internal | |

Eq (NatRepr m) | |

KnownNat n => Data (NatRepr n) | |

Defined in Data.Parameterized.NatRepr.Internal gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) # toConstr :: NatRepr n -> Constr # dataTypeOf :: NatRepr n -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) # gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # | |

Show (NatRepr n) | |

Hashable (NatRepr n) | |

Defined in Data.Parameterized.NatRepr.Internal | |

PolyEq (NatRepr m) (NatRepr n) | |

knownNat :: forall (n :: Nat). KnownNat n => NatRepr n #

This generates a NatRepr from a type-level context.

# Constructors

Construct a bitvector with a particular width, where the width is
provided as an explicit `NatRepr`

argument. The input `Integer`

,
whether positive or negative, is silently truncated to fit into the
number of bits demanded by the return type. The width cannot be
arbitrarily large; it must be representable as an `Int`

.

`>>>`

BV 10`mkBV (knownNat @4) 10`

`>>>`

BV 2`mkBV (knownNat @2) 10`

`>>>`

BV 14`mkBV (knownNat @4) (-2)`

unsignedClamp :: NatRepr w -> Integer -> BV w Source #

`unsignedClamp w i`

rounds `i`

to the nearest value between `0`

and `2^w - 1`

(inclusive).

signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w Source #

`signedClamp w i`

rounds `i`

to the nearest value between
`-2^(w-1)`

and `2^(w-1) - 1`

(inclusive).

minUnsigned :: NatRepr w -> BV w Source #

The minimum unsigned value for bitvector with given width (always 0).

maxUnsigned :: NatRepr w -> BV w Source #

The maximum unsigned value for bitvector with given width.

minSigned :: 1 <= w => NatRepr w -> BV w Source #

The minimum value for bitvector in two's complement with given width.

maxSigned :: 1 <= w => NatRepr w -> BV w Source #

The maximum value for bitvector in two's complement with given width.

# Construction from fixed-width data types

bytesBE :: [Word8] -> Pair NatRepr BV Source #

Construct a `BV`

from a list of bytes, in big endian order (bytes
with lower value index in the list are mapped to higher order bytes
in the output bitvector).

`>>>`

(24,BV 257)`case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)`

bytesLE :: [Word8] -> Pair NatRepr BV Source #

Construct a `BV`

from a list of bytes, in little endian order
(bytes with lower value index in the list are mapped to lower
order bytes in the output bitvector).

`>>>`

(24,BV 65792)`case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)`

bytestringBE :: ByteString -> Pair NatRepr BV Source #

Construct a `BV`

from a big-endian bytestring.

`>>>`

(24,BV 257)`case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)`

bytestringLE :: ByteString -> Pair NatRepr BV Source #

Construct a `BV`

from a little-endian bytestring.

`>>>`

(24,BV 65792)`case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)`

# Conversions to primitive types

asSigned :: 1 <= w => NatRepr w -> BV w -> Integer Source #

Signed interpretation of a bitvector as an Integer.

asUnsigned :: BV w -> Integer Source #

Unsigned interpretation of a bitvector as a positive Integer.

asBitsBE :: NatRepr w -> BV w -> [Bool] Source #

Convert a bitvector to a list of bits, in big endian order (higher order bits in the bitvector are mapped to lower indices in the output list).

`>>>`

[False,True,True,False,True]`asBitsBE (knownNat @5) (mkBV knownNat 0b1101)`

asBitsLE :: NatRepr w -> BV w -> [Bool] Source #

Convert a bitvector to a list of bits, in little endian order (lower order bits in the bitvector are mapped to lower indices in the output list).

`>>>`

[True,False,True,True,False]`asBitsLE (knownNat @5) (mkBV knownNat 0b1101)`

asBytesBE :: NatRepr w -> BV w -> Maybe [Word8] Source #

Convert a bitvector to a list of bytes, in big endian order
(higher order bytes in the bitvector are mapped to lower indices in
the output list). Return `Nothing`

if the width is not a multiple
of 8.

`>>>`

Just [170,187,204,221]`asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)`

asBytesLE :: NatRepr w -> BV w -> Maybe [Word8] Source #

Convert a bitvector to a list of bytes, in little endian order
(lower order bytes in the bitvector are mapped to lower indices in
the output list). Return `Nothing`

if the width is not a multiple
of 8.

`>>>`

Just [221,204,187,170]`asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)`

asBytestringBE :: NatRepr w -> BV w -> Maybe ByteString Source #

`asBytesBE`

, but for bytestrings.

asBytestringLE :: NatRepr w -> BV w -> Maybe ByteString Source #

`asBytesLE`

, but for bytestrings.

# Bits operations (width-preserving)

`BV`

versions of the functions in `Data.Bits`

.

ashr :: 1 <= w => NatRepr w -> BV w -> Natural -> BV w Source #

Right arithmetic shift by positive `Natural`

.

The `BV`

that has a particular bit set, and is 0 everywhere
else.

`setBit bv ix`

is the same as `or bv (bit knownNat ix)`

.

:: (ix + 1) <= w | |

=> NatRepr w | Desired output width |

-> NatRepr ix | Index of bit to clear |

-> BV w | Original bitvector |

-> BV w |

`clearBit w bv ix`

is the same as `and bv (complement (bit w ix))`

.

`complementBit bv ix`

is the same as `xor bv (bit knownNat ix)`

.

Like `complementBit`

, but without the requirement that the index
bit refers to an actual bit in the input `BV`

. If it is out of
range, just silently return the original input.

truncBits :: Natural -> BV w -> BV w Source #

Truncate a bitvector to a particular width given at runtime, while keeping the type-level width constant.

# Arithmetic operations (width-preserving)

uquot :: BV w -> BV w -> BV w Source #

Bitvector division (unsigned). Rounds to zero. Division by zero yields a runtime error.

squot :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector division (signed). Rounds to zero. Division by zero yields a runtime error.

sdiv :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector division (signed). Rounds to negative infinity. Division by zero yields a runtime error.

urem :: BV w -> BV w -> BV w Source #

Bitvector remainder after division (unsigned), when rounded to zero. Division by zero yields a runtime error.

srem :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.

smod :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector remainder after division (signed), when rounded to negative infinity. Division by zero yields a runtime error.

abs :: 1 <= w => NatRepr w -> BV w -> BV w Source #

Bitvector absolute value. Returns the 2's complement magnitude of the bitvector.

signum :: 1 <= w => NatRepr w -> BV w -> BV w Source #

Return 1 if positive, -1 if negative, and 0 if 0.

# Variable-width operations

These are functions that involve bit vectors of different lengths.

:: NatRepr w | Width of higher-order bits |

-> NatRepr w' | Width of lower-order bits |

-> BV w | Higher-order bits |

-> BV w' | Lower-order bits |

-> BV (w + w') |

Concatenate two bitvectors. The first argument gets placed in the higher order bits.

`>>>`

BV 6`concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)`

`>>>`

it :: BV 5`:type it`

:: (ix + w') <= w | |

=> NatRepr ix | Index to start selecting from |

-> NatRepr w' | Desired output width |

-> BV w | Bitvector to select from |

-> BV w' |

Slice out a smaller bitvector from a larger one.

`>>>`

BV 3`select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)`

`>>>`

it :: BV 4`:type it`

:: Natural | Index to start selecting from |

-> NatRepr w' | Desired output width |

-> BV w | Bitvector to select from |

-> BV w' |

Like `select`

, but takes a `Natural`

as the index to start
selecting from. Neither the index nor the output width is checked
to ensure the resulting `BV`

lies entirely within the bounds of the
original bitvector. Any bits "selected" from beyond the bounds of
the input bitvector will be 0.

`>>>`

BV 6`select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)`

`>>>`

it :: BV 4`:type it`

Zero-extend a bitvector to one of strictly greater width.

`>>>`

BV 13`zext (knownNat @8) (mkBV (knownNat @4) 0b1101)`

`>>>`

it :: BV 8`:type it`

:: (1 <= w, (w + 1) <= w') | |

=> NatRepr w | Width of input bitvector |

-> NatRepr w' | Desired output width |

-> BV w | Bitvector to extend |

-> BV w' |

Sign-extend a bitvector to one of strictly greater width.

Truncate a bitvector to one of strictly smaller width.

Like `trunc`

, but allows the input width to be greater than or
equal to the output width, in which case it just performs a zero
extension.

mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w') Source #

Wide multiply of two bitvectors.

# Enum operations

succUnsigned :: NatRepr w -> BV w -> Maybe (BV w) Source #

Unsigned successor. `succUnsigned w (maxUnsigned w)`

returns `Nothing`

.

succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) Source #

Signed successor. `succSigned w (maxSigned w)`

returns `Nothing`

.

predUnsigned :: NatRepr w -> BV w -> Maybe (BV w) Source #

Unsigned predecessor. `predUnsigned w zero`

returns `Nothing`

.

predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) Source #

Signed predecessor. `predSigned w (minSigned w)`

returns `Nothing`

.

List of all unsigned bitvectors from a lower to an upper bound, inclusive.

List of all signed bitvectors from a lower to an upper bound, inclusive.

# Generating random bitvectors

uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w) Source #

Generates a bitvector uniformly distributed over all possible values for a
given width. (See `uniformM`

).

uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w) Source #

Generates a bitvector uniformly distributed over the provided range
(interpreted as a range of *unsigned* bitvectors), which is interpreted as
inclusive in the lower and upper bound. (See
`uniformRM`

).

sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w) Source #

Generates a bitvector uniformly distributed over the provided range
(interpreted as a range of *signed* bitvectors), which is interpreted as
inclusive in the lower and upper bound. (See
`uniformRM`

).