what4-1.1: Solver-agnostic symbolic values support for issuing queries
CopyrightGalois Inc. 2018-2020
LicenseBSD3
Maintainerrdockins@galois.com
Stabilityexperimental
Portabilitynon-portable (language extensions)
Safe HaskellNone
LanguageHaskell2010

What4.SWord

Description

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

Synopsis

Documentation

data SWord sym where Source #

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

Instances details
Show (SWord sym) Source # 
Instance details

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

Return the signed value if this is a constant bitvector

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

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

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

Interpret the bit-vector as an unsigned integer

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

Interpret the bit-vector as a signed integer

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

bvWidth :: forall sym. SWord sym -> Integer Source #

Get the width of a bitvector

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

Create a bitvector with the given width and value

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

bvAtBE Source #

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

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

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

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

Arguments

:: forall sym. IsExprBuilder sym 
=> sym 
-> Integer

Starting index, from 0 as most significant bit

-> Integer

Number of bits to take (must be > 0)

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

Arguments

:: forall sym. IsExprBuilder sym 
=> sym 
-> Integer

Starting index, from 0 as most significant bit

-> Integer

Number of bits to take (must be > 0)

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

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

If-then-else applied to bitvectors.

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

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

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

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

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

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

Logic operations

bvNot :: SWordUn Source #

Bitwise complement

bvAnd :: SWordBin Source #

Bitwise logical and.

bvOr :: SWordBin Source #

Bitwise logical or.

bvXor :: SWordBin Source #

Bitwise logical exclusive or.

Arithmetic operations

bvNeg :: SWordUn Source #

2's complement negation.

bvAdd :: SWordBin Source #

Add two bitvectors.

bvSub :: SWordBin Source #

Subtract one bitvector from another.

bvMul :: SWordBin Source #

Multiply one bitvector by another.

bvUDiv :: SWordBin Source #

Unsigned bitvector division.

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

bvURem :: SWordBin Source #

Unsigned bitvector remainder.

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

bvSDiv :: SWordBin Source #

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

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

Return true if bitvectors are equal.

bvsle :: PredBin Source #

Signed less-than-or-equal.

bvslt :: PredBin Source #

Signed less-than.

bvule :: PredBin Source #

Unsigned less-than-or-equal.

bvult :: PredBin Source #

Unsigned less-than.

bvsge :: PredBin Source #

Signed greater-than-or-equal.

bvsgt :: PredBin Source #

Signed greater-than.

bvuge :: PredBin Source #

Unsigned greater-than-or-equal.

bvugt :: PredBin Source #

Unsigned greater-than.

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

bit-counting operations

bvPopcount :: SWordUn Source #

bvLg2 :: SWordUn Source #

Shift and rotates

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

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

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

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

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

Zero- and sign-extend

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

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

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

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