What4.SWord

A wrapper for What4 bitvectors so that the width is not tracked statically.

Documentation

data SWord sym where

A What4 symbolic bitvector where the size does not appear in the type

Constructors

DBV :: (IsExpr (SymExpr sym), 1 <= w) => SymBV sym w -> SWord sym

ZBV :: SWord sym

Instances

Show (SWord sym)

Defined in What4.SWord

Methods

showsPrec :: Int -> SWord sym -> ShowS

show :: SWord sym -> String

showList :: [SWord sym] -> ShowS

bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer

Return the signed value if this is a constant bitvector

bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer

Return the unsigned value if this is a constant bitvector

integerToBV :: forall sym width. (Show width, Integral width, IsExprBuilder sym) => sym -> SymInteger sym -> width -> IO (SWord sym)

Convert an integer to an unsigned bitvector. The input value is reduced modulo 2^w.

bvToInteger :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (SymInteger sym)

Interpret the bit-vector as an unsigned integer

sbvToInteger :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (SymInteger sym)

Interpret the bit-vector as a signed integer

freshBV :: forall sym. IsSymExprBuilder sym => sym -> SolverSymbol -> Integer -> IO (SWord sym)

bvWidth :: forall sym. SWord sym -> Integer

Get the width of a bitvector

bvLit :: forall sym. IsExprBuilder sym => sym -> Integer -> Integer -> IO (SWord sym)

Create a bitvector with the given width and value

bvFill :: forall sym. IsExprBuilder sym => sym -> Integer -> Pred sym -> IO (SWord sym)

bvAtBE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> SWord sym

-> Integer

Index of bit (0 is the most significant bit)

-> IO (Pred sym)

Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

bvAtLE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> SWord sym

-> Integer

Index of bit (0 is the most significant bit)

-> IO (Pred sym)

Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in little-endian ordering, meaning the least-significant bit is bit 0

bvSetBE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> SWord sym

-> Integer

Index of bit (0 is the most significant bit)

-> Pred sym

-> IO (SWord sym)

Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

bvSetLE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> SWord sym

-> Integer

Index of bit (0 is the most significant bit)

-> Pred sym

-> IO (SWord sym)

Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

bvSliceBE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> Integer

Starting index, from 0 as most significant bit

-> Integer

Number of bits to take

-> SWord sym

-> IO (SWord sym)

Select a subsequence from a bitvector, with bits numbered in Big Endian order (most significant bit is 0). This fails if idx + n is >= w

bvSliceLE

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> Integer

Starting index, from 0 as most significant bit

-> Integer

Number of bits to take

-> SWord sym

-> IO (SWord sym)

Select a subsequence from a bitvector, with bits numbered in Little Endian order (least significant bit is 0). This fails if idx + n is >= w

bvJoin

Arguments

:: forall sym. IsExprBuilder sym

=> sym

-> SWord sym

most significant bits

-> SWord sym

least significant bits

-> IO (SWord sym)

Concatenate two bitvectors.

bvIte :: forall sym. IsExprBuilder sym => sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)

If-then-else applied to bitvectors.

bvPackBE :: forall sym. (IsExpr (SymExpr sym), IsExprBuilder sym) => sym -> Vector (Pred sym) -> IO (SWord sym)

convert a vector of booleans to a bitvector. The input are used in Big Endian order (most significant bit first)

bvPackLE :: forall sym. (IsExpr (SymExpr sym), IsExprBuilder sym) => sym -> Vector (Pred sym) -> IO (SWord sym)

convert a vector of booleans to a bitvector. The inputs are used in Little Endian order (least significant bit first)

bvUnpackBE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Vector (Pred sym))

Explode a bitvector into a vector of booleans in Big Endian order (most significant bit first)

bvUnpackLE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Vector (Pred sym))

Explode a bitvector into a vector of booleans in Little Endian order (least significant bit first)

bvForall :: IsSymExprBuilder sym => sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)

unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)

signedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)

Logic operations

bvNot :: SWordUn

Bitwise complement

bvAnd :: SWordBin

Bitwise logical and.

bvOr :: SWordBin

Bitwise logical or.

bvXor :: SWordBin

Bitwise logical exclusive or.

Arithmetic operations

bvNeg :: SWordUn

2's complement negation.

bvAdd :: SWordBin

Add two bitvectors.

bvSub :: SWordBin

Subtract one bitvector from another.

bvMul :: SWordBin

Multiply one bitvector by another.

bvUDiv :: SWordBin

Unsigned bitvector division.

The result is undefined when y is zero, but is otherwise equal to floor( x / y ).

bvURem :: SWordBin

Unsigned bitvector remainder.

The result is undefined when y is zero, but is otherwise equal to x - (bvUdiv x y) * y.

bvSDiv :: SWordBin

Signed bitvector division. The result is truncated to zero.

The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs.

NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.

bvSRem :: SWordBin

Signed bitvector remainder.

The result of bvSrem x y is undefined when y is zero, but is otherwise equal to x - (bvSdiv x y) * y.

Comparison operations

bvEq :: PredBin

Return true if bitvectors are equal.

bvsle :: PredBin

Signed less-than-or-equal.

bvslt :: PredBin

Signed less-than.

bvule :: PredBin

Unsigned less-than-or-equal.

bvult :: PredBin

Unsigned less-than.

bvsge :: PredBin

Signed greater-than-or-equal.

bvsgt :: PredBin

Signed greater-than.

bvuge :: PredBin

Unsigned greater-than-or-equal.

bvugt :: PredBin

Unsigned greater-than.

bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)

bit-counting operations

bvPopcount :: SWordUn

bvCountLeadingZeros :: SWordUn

bvCountTrailingZeros :: SWordUn

bvLg2 :: SWordUn

Shift and rotates

bvShl :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)

bvLshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)

bvAshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)

bvRol :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)

bvRor :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)

Zero- and sign-extend

bvZext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)

Zero-extend a value, adding the specified number of bits.

bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)

Sign-extend a value, adding the specified number of bits.