what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | Galois Inc. 2018-2020
License | BSD3
Maintainer | rdockins@galois.com
Stability | experimental
Portability | non-portable (language extensions)
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.SWord

Contents

- Logic operations
- Arithmetic operations
- Comparison operations
- bit-counting operations
- Shift and rotates
- Zero- and sign-extend

Description

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

Synopsis

- data SWord sym where
  - DBV :: (IsExpr (SymExpr sym), 1 <= w) => SymBV sym w -> SWord sym
  - ZBV :: SWord sym
- bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
- bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
- integerToBV :: forall sym width. (Show width, Integral width, IsExprBuilder sym) => sym -> SymInteger sym -> width -> IO (SWord sym)
- bvToInteger :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (SymInteger sym)
- sbvToInteger :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (SymInteger sym)
- freshBV :: forall sym. IsSymExprBuilder sym => sym -> SolverSymbol -> Integer -> IO (SWord sym)
- bvWidth :: forall sym. SWord sym -> Integer
- bvLit :: forall sym. IsExprBuilder sym => sym -> Integer -> Integer -> IO (SWord sym)
- bvFill :: forall sym. IsExprBuilder sym => sym -> Integer -> Pred sym -> IO (SWord sym)
- bvAtBE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> Integer -> IO (Pred sym)
- bvAtLE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> Integer -> IO (Pred sym)
- bvSetBE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
- bvSetLE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
- bvSliceBE :: forall sym. IsExprBuilder sym => sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
- bvSliceLE :: forall sym. IsExprBuilder sym => sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
- bvJoin :: forall sym. IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
- bvIte :: forall sym. IsExprBuilder sym => sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
- bvPackBE :: forall sym. (IsExpr (SymExpr sym), IsExprBuilder sym) => sym -> Vector (Pred sym) -> IO (SWord sym)
- bvPackLE :: forall sym. (IsExpr (SymExpr sym), IsExprBuilder sym) => sym -> Vector (Pred sym) -> IO (SWord sym)
- bvUnpackBE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Vector (Pred sym))
- bvUnpackLE :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Vector (Pred sym))
- 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)
- bvNot :: SWordUn
- bvAnd :: SWordBin
- bvOr :: SWordBin
- bvXor :: SWordBin
- bvNeg :: SWordUn
- bvAdd :: SWordBin
- bvSub :: SWordBin
- bvMul :: SWordBin
- bvUDiv :: SWordBin
- bvURem :: SWordBin
- bvSDiv :: SWordBin
- bvSRem :: SWordBin
- bvEq :: PredBin
- bvsle :: PredBin
- bvslt :: PredBin
- bvule :: PredBin
- bvult :: PredBin
- bvsge :: PredBin
- bvsgt :: PredBin
- bvuge :: PredBin
- bvugt :: PredBin
- bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
- bvPopcount :: SWordUn
- bvCountLeadingZeros :: SWordUn
- bvCountTrailingZeros :: SWordUn
- bvLg2 :: SWordUn
- 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)
- bvZext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
- bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)

# 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 Source # show :: SWord sym -> String Source # showList :: [SWord sym] -> ShowS Source #

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

unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer) 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 #

bvCountLeadingZeros :: SWordUn Source #

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