bv-sized-1.0.5: a bitvector datatype that is parameterized by the vector width

Copyright | (c) Galois Inc. 2018
License | BSD-3
Maintainer | Ben Selfridge <benselfridge@galois.com>
Stability | experimental
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.BitVector.Sized

Contents

- `BV` type
- `NatRepr`s (from parameterized-utils)
- Constructors
- Construction from fixed-width data types
- Conversions to primitive types
- Bits operations (width-preserving)
- Arithmetic operations (width-preserving)
- Variable-width operations
- Enum operations
- Generating random bitvectors
- Pretty printing

Description

This module defines a width-parameterized `BV` type and various associated operations. A ``BV` w` is a newtype around an `Integer`, so operations that require the width take an explicit ``NatRepr` w` argument. We explicitly do not allow widths that cannot be represented as an `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'
- zresize :: NatRepr w' -> BV w -> BV w'
- sresize :: 1 <= w => NatRepr w -> 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

Instances details

EqF BV Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods eqF :: forall (a :: k). BV a -> BV a -> Bool Source #
ShowF BV Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods withShow :: forall p q (tp :: k) a. p BV -> q tp -> (Show (BV tp) => a) -> a Source # showF :: forall (tp :: k). BV tp -> String Source # showsPrecF :: forall (tp :: k). Int -> BV tp -> String -> String Source #
Lift (BV w :: Type) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods lift :: Quote m => BV w -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => BV w -> Code m (BV w) Source #
Generic (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Associated Types type Rep (BV w) :: Type -> Type Source # Methods from :: BV w -> Rep (BV w) x Source # to :: Rep (BV w) x -> BV w Source #
Read (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods readsPrec :: Int -> ReadS (BV w) Source # readList :: ReadS [BV w] Source # readPrec :: ReadPrec (BV w) Source # readListPrec :: ReadPrec [BV w] Source #
Show (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods showsPrec :: Int -> BV w -> ShowS Source # show :: BV w -> String Source # showList :: [BV w] -> ShowS Source #
NFData (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods rnf :: BV w -> () Source #
Eq (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods (==) :: BV w -> BV w -> Bool Source # (/=) :: BV w -> BV w -> Bool Source #
Ord (BV w) Source # | Uses an unsigned ordering, but `ule` and `ult` are preferred. We provide this instance to allow the use of `BV` in situations where an arbitrary ordering is required (e.g., as the keys in a map)
Instance details Defined in Data.BitVector.Sized.Internal Methods compare :: BV w -> BV w -> Ordering Source # (<) :: BV w -> BV w -> Bool Source # (<=) :: BV w -> BV w -> Bool Source # (>) :: BV w -> BV w -> Bool Source # (>=) :: BV w -> BV w -> Bool Source # max :: BV w -> BV w -> BV w Source # min :: BV w -> BV w -> BV w Source #
Hashable (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal Methods hashWithSalt :: Int -> BV w -> Int # hash :: BV w -> Int #
type Rep (BV w) Source # |
Instance details Defined in Data.BitVector.Sized.Internal type Rep (BV w) = D1 ('MetaData "BV" "Data.BitVector.Sized.Internal" "bv-sized-1.0.5-IDKhEWZ3nUo3z3zx0EtHRF" 'True) (C1 ('MetaCons "BV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

pattern BV :: Integer -> BV w Source #

Get the underlying `Integer` representation from a `BV`. We guarantee that `(\(BV.BV x) -> x) == BV.asUnsigned`.

# `NatRepr`s (from parameterized-utils)

data NatRepr (n :: Nat) Source #

A runtime presentation of a type-level `Nat`.

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

#### Instances

Instances details

TestEquality NatRepr |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b) Source #
HashableF NatRepr |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSaltF :: forall (tp :: k). Int -> NatRepr tp -> Int Source # hashF :: forall (tp :: k). NatRepr tp -> Int Source #
OrdF NatRepr |

Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source #

ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source #

geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source #

gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source #

ShowF NatRepr |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods withShow :: forall p q (tp :: k) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a Source # showF :: forall (tp :: k). NatRepr tp -> String Source # showsPrecF :: forall (tp :: k). Int -> NatRepr tp -> String -> String Source #
DecidableEq NatRepr |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
KnownNat n => KnownRepr NatRepr (n :: Nat) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods knownRepr :: NatRepr n Source #
KnownNat n => Data (NatRepr n) |

Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) Source #

toConstr :: NatRepr n -> Constr Source #

dataTypeOf :: NatRepr n -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) Source #

gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

Show (NatRepr n) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods showsPrec :: Int -> NatRepr n -> ShowS Source # show :: NatRepr n -> String Source # showList :: [NatRepr n] -> ShowS Source #
Eq (NatRepr m) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods (==) :: NatRepr m -> NatRepr m -> Bool Source # (/=) :: NatRepr m -> NatRepr m -> Bool Source #
Hashable (NatRepr n) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSalt :: Int -> NatRepr n -> Int # hash :: NatRepr n -> Int #
PolyEq (NatRepr m) (NatRepr n) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n) Source # polyEq :: NatRepr m -> NatRepr n -> Bool Source #

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

This generates a NatRepr from a type-level context.

# Constructors

mkBV Source #

Arguments

:: NatRepr w | Desired bitvector width
-> Integer | Integer value to truncate to bitvector width
-> BV w |

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

    >>> mkBV (knownNat @4) 10
    BV 10
    >>> mkBV (knownNat @2) 10
    BV 2
    >>> mkBV (knownNat @4) (-2)
    BV 14

mkBVUnsigned Source #

Arguments

:: NatRepr w | Desired bitvector width
-> Integer | Integer value
-> Maybe (BV w) |

Like `mkBV`, but returns `Nothing` if unsigned input integer cannot be represented in `w` bits.

mkBVSigned Source #

Arguments

:: 1 <= w |
=> NatRepr w | Desired bitvector width
-> Integer | Integer value
-> Maybe (BV w) |

Like `mkBV`, but returns `Nothing` if signed input integer cannot be represented in `w` bits.

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.

zero :: NatRepr w -> BV w Source #

The zero bitvector of any width.

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

The bitvector with value 1, of any positive width.

width :: NatRepr w -> BV w Source #

The bitvector whose value is its own width, of any width.

# Construction from fixed-width data types

bool :: Bool -> BV 1 Source #

Construct a `BV` from a `Bool`.

word8 :: Word8 -> BV 8 Source #

Construct a `BV` from a `Word8`.

word16 :: Word16 -> BV 16 Source #

Construct a `BV` from a `Word16`.

word32 :: Word32 -> BV 32 Source #

Construct a `BV` from a `Word32`.

word64 :: Word64 -> BV 64 Source #

Construct a `BV` from a `Word64`.

int8 :: Int8 -> BV 8 Source #

Construct a `BV` from an `Int8`.

int16 :: Int16 -> BV 16 Source #

Construct a `BV` from an `Int16`.

int32 :: Int32 -> BV 32 Source #

Construct a `BV` from an `Int32`.

int64 :: Int64 -> BV 64 Source #

Construct a `BV` from an `Int64`.

bitsBE :: [Bool] -> Pair NatRepr BV Source #

Construct a `BV` from a list of bits, in big endian order (bits with lower value index in the list are mapped to higher order bits in the output bitvector). Return the resulting `BV` along with its width.

    >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
    (2,BV 2)

bitsLE :: [Bool] -> Pair NatRepr BV Source #

Construct a `BV` from a list of bits, in little endian order (bits with lower value index in the list are mapped to lower order bits in the output bitvector). Return the resulting `BV` along with its width.

    >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
    (2,BV 1)

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

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

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

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

bytestringBE :: ByteString -> Pair NatRepr BV Source #

Construct a `BV` from a big-endian bytestring.

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

bytestringLE :: ByteString -> Pair NatRepr BV Source #

Construct a `BV` from a little-endian bytestring.

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

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

asNatural :: BV w -> Natural Source #

Unsigned interpretation of a bitvector as a Natural.

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

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

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

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

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.

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

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.

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

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

and :: BV w -> BV w -> BV w Source #

Bitwise and.

or :: BV w -> BV w -> BV w Source #

Bitwise or.

xor :: BV w -> BV w -> BV w Source #

Bitwise xor.

complement :: NatRepr w -> BV w -> BV w Source #

Bitwise complement (flip every bit).

shl :: NatRepr w -> BV w -> Natural -> BV w Source #

Left shift by positive `Natural`.

lshr :: NatRepr w -> BV w -> Natural -> BV w Source #

Right logical shift by positive `Natural`.

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

Right arithmetic shift by positive `Natural`.

rotateL :: NatRepr w -> BV w -> Natural -> BV w Source #

Bitwise rotate left.

rotateR :: NatRepr w -> BV w -> Natural -> BV w Source #

Bitwise rotate right.

bit Source #

Arguments

:: (ix + 1) <= w |
=> NatRepr w | Desired output width
-> NatRepr ix | Index of bit to set
-> BV w |

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

bit' Source #

Arguments

:: NatRepr w | Desired output width
-> Natural | Index of bit to set
-> BV w |

Like `bit`, but without the requirement that the index bit refers to an actual bit in the output `BV`. If it is out of range, just silently return the zero bitvector.

setBit Source #

Arguments

:: (ix + 1) <= w |
=> NatRepr ix | Index of bit to set
-> BV w | Original bitvector
-> BV w |

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

setBit' Source #

Arguments

:: NatRepr w | Desired output width
-> Natural | Index of bit to set
-> BV w | Original bitvector
-> BV w |

Like `setBit`, 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.

clearBit Source #

Arguments

:: (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))`.

clearBit' Source #

Arguments

:: NatRepr w | Desired output width
-> Natural | Index of bit to clear
-> BV w | Original bitvector
-> BV w |

Like `clearBit`, 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.

complementBit Source #

Arguments

:: (ix + 1) <= w |
=> NatRepr ix | Index of bit to flip
-> BV w | Original bitvector
-> BV w |

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

complementBit' Source #

Arguments

:: NatRepr w | Desired output width
-> Natural | Index of bit to flip
-> BV w | Original bitvector
-> BV w |

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.

testBit :: (ix + 1) <= w => NatRepr ix -> BV w -> Bool Source #

Test if a particular bit is set.

testBit' :: Natural -> BV w -> Bool Source #

Like `testBit`, but takes a `Natural` for the bit index. If the index is out of bounds, return `False`.

popCount :: BV w -> BV w Source #

Get the number of 1 bits in a `BV`.

ctz :: NatRepr w -> BV w -> BV w Source #

Count trailing zeros in a `BV`.

clz :: NatRepr w -> BV w -> BV w Source #

Count leading zeros in a `BV`.

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)

add :: NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector add.

sub :: NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector subtract.

mul :: NatRepr w -> BV w -> BV w -> BV w Source #

Bitvector multiply.

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.

uquotRem :: BV w -> BV w -> (BV w, BV w) Source #

`uquot` and `urem` returned as a pair.

squotRem :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w) Source #

`squot` and `srem` returned as a pair.

sdivMod :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w) Source #

`sdiv` and `smod` returned as a pair.

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

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

negate :: NatRepr w -> BV w -> BV w Source #

2's complement bitvector negation.

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

Get the sign bit as a `BV`.

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

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

slt :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool Source #

Signed less than.

sle :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool Source #

Signed less than or equal.

ult :: BV w -> BV w -> Bool Source #

Unsigned less than.

ule :: BV w -> BV w -> Bool Source #

Unsigned less than or equal.

umin :: BV w -> BV w -> BV w Source #

Unsigned minimum of two bitvectors.

umax :: BV w -> BV w -> BV w Source #

Unsigned maximum of two bitvectors.

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

Signed minimum of two bitvectors.

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

Signed maximum of two bitvectors.

# Variable-width operations

These are functions that involve bit vectors of different lengths.

concat Source #

Arguments

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

    >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
    BV 6
    >>> :type it
    it :: BV 5

select Source #

Arguments

:: (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.

    >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
    BV 3
    >>> :type it
    it :: BV 4

select' Source #

Arguments

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

    >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
    BV 6
    >>> :type it
    it :: BV 4

zext Source #

Arguments

:: (w + 1) <= w' |
=> NatRepr w' | Desired output width
-> BV w | Bitvector to extend
-> BV w' |

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

    >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
    BV 13
    >>> :type it
    it :: BV 8

sext Source #

Arguments

:: (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.

trunc Source #

Arguments

:: (w' + 1) <= w |
=> NatRepr w' | Desired output width
-> BV w | Bitvector to truncate
-> BV w' |

Truncate a bitvector to one of strictly smaller width.

trunc' Source #

Arguments

:: NatRepr w' | Desired output width
-> BV w | Bitvector to truncate
-> BV w' |

Deprecated: Use zresize instead

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.

zresize Source #

Arguments

:: NatRepr w' | Desired output width
-> BV w | Bitvector to resize
-> BV w' |

Resizes a bitvector. If `w' > w`, perform a zero extension.

sresize Source #

Arguments

:: 1 <= w |
=> NatRepr w | Width of input vector
-> NatRepr w' | Desired output width
-> BV w | Bitvector to resize
-> BV w' |

Resizes a bitvector. If `w' > w`, perform a signed 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`.

enumFromToUnsigned Source #

Arguments

:: BV w | Lower bound
-> BV w | Upper bound
-> [BV w] |

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

enumFromToSigned Source #

Arguments

:: 1 <= w |
=> NatRepr w |
-> BV w | Lower bound
-> BV w | Upper bound
-> [BV w] |

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

# Generating random bitvectors

`BV` versions of the functions in `Random`.

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

# Pretty printing

ppHex :: NatRepr w -> BV w -> String Source #

Pretty print in hex

ppBin :: NatRepr w -> BV w -> String Source #

Pretty print in binary

ppOct :: NatRepr w -> BV w -> String Source #

Pretty print in octal

ppDec :: NatRepr w -> BV w -> String Source #

Pretty print in decimal