bv-sized-1.0.4: a bitvector datatype that is parameterized by the vector width
Copyright(c) Galois Inc. 2018
LicenseBSD-3
MaintainerBen Selfridge <benselfridge@galois.com>
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Data.BitVector.Sized

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

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

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 #

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 #

showF :: forall (tp :: k). BV tp -> String #

showsPrecF :: forall (tp :: k). Int -> BV tp -> String -> String #

Lift (BV w :: Type) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Methods

lift :: BV w -> Q Exp #

liftTyped :: BV w -> Q (TExp (BV w)) #

Eq (BV w) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Methods

(==) :: BV w -> BV w -> Bool #

(/=) :: BV w -> BV w -> Bool #

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 #

(<) :: BV w -> BV w -> Bool #

(<=) :: BV w -> BV w -> Bool #

(>) :: BV w -> BV w -> Bool #

(>=) :: BV w -> BV w -> Bool #

max :: BV w -> BV w -> BV w #

min :: BV w -> BV w -> BV w #

Read (BV w) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Show (BV w) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Methods

showsPrec :: Int -> BV w -> ShowS #

show :: BV w -> String #

showList :: [BV w] -> ShowS #

Generic (BV w) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Associated Types

type Rep (BV w) :: Type -> Type #

Methods

from :: BV w -> Rep (BV w) x #

to :: Rep (BV w) x -> BV w #

NFData (BV w) Source # 
Instance details

Defined in Data.BitVector.Sized.Internal

Methods

rnf :: BV w -> () #

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.4-EGq9mNcoBii2hKyuvBNKlW" '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.

NatReprs (from parameterized-utils)

data NatRepr (n :: Nat) #

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

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

OrdF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

showF :: forall (tp :: k). NatRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> NatRepr tp -> String -> String #

HashableF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSaltF :: forall (tp :: k). Int -> NatRepr tp -> Int #

hashF :: forall (tp :: k). NatRepr tp -> Int #

KnownNat n => KnownRepr NatRepr (n :: Nat) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n #

Eq (NatRepr m) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

(==) :: NatRepr m -> NatRepr m -> Bool #

(/=) :: NatRepr m -> NatRepr m -> Bool #

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

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) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

showsPrec :: Int -> NatRepr n -> ShowS #

show :: NatRepr n -> String #

showList :: [NatRepr n] -> ShowS #

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

polyEq :: NatRepr m -> NatRepr n -> Bool #

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

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