Copyright	(c) 2020 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Safe Haskell	None
Language	Haskell2010

Cryptol.Eval.What4.Value

Description

Synopsis

data What4 sym = What4 sym
type Value sym = GenValue (What4 sym)
newtype W4Eval sym a = W4Eval {
- evalPartial :: W4Conn sym (W4Result sym a)
}
newtype W4Conn sym a = W4Conn {
- evalConn :: sym -> Eval (W4Defs sym a)
}
data W4Defs sym a = W4Defs {
- w4Defs :: !(Pred sym)
- w4Result :: !a
}
data W4Result sym a
- = W4Error !EvalError
- | W4Result !(Pred sym) !a
w4Eval :: W4Eval sym a -> sym -> Eval (W4Defs sym (W4Result sym a))
w4Thunk :: Eval (W4Defs sym (W4Result sym a)) -> W4Eval sym a
doEval :: IsExprBuilder sym => Eval a -> W4Conn sym a
total :: IsExprBuilder sym => W4Conn sym a -> W4Eval sym a
getSym :: IsExprBuilder sym => W4Conn sym sym
addDef :: Pred sym -> W4Conn sym ()
w4And :: IsExprBuilder sym => Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4Not :: IsExprBuilder sym => Pred sym -> W4Conn sym (Pred sym)
w4ITE :: IsExprBuilder sym => Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
addDefEqn :: IsExprBuilder sym => Pred sym -> W4Eval sym ()
addSafety :: IsExprBuilder sym => Pred sym -> W4Eval sym ()
evalError :: IsExprBuilder sym => EvalError -> W4Eval sym a
assertBVDivisor :: IsExprBuilder sym => sym -> SWord sym -> W4Eval sym ()
assertIntDivisor :: IsExprBuilder sym => sym -> SymInteger sym -> W4Eval sym ()
sModAdd :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModSub :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModMult :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModNegate :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sLg2 :: IsExprBuilder sym => sym -> SWord sym -> SEval (What4 sym) (SWord sym)
evalPanic :: String -> [String] -> a
lazyIte :: (IsExpr p, Monad m) => (p BaseBoolType -> a -> a -> m a) -> p BaseBoolType -> m a -> m a -> m a
indexFront_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym)
indexBack_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym)
indexFront_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym)
indexBack_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym)
indexFront_bits :: forall sym. IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym)
indexBack_bits :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym)
wordValueEqualsInteger :: forall sym. IsExprBuilder sym => sym -> WordValue (What4 sym) -> Integer -> W4Eval sym (Pred sym)
updateFrontSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym))
updateBackSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym))
updateFrontSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym))
sshrV :: IsExprBuilder sym => sym -> Value sym
w4bvShl :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvLshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvAshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRol :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRor :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
fpRoundingMode :: IsExprBuilder sym => What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpBinArith :: IsExprBuilder sym => SFloatBinArith sym -> What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
fpCvtToInteger :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToRational :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtFromRational :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym)

Documentation

data What4 sym Source #

Constructors

What4 sym

Instances

IsExprBuilder sym => Backend (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Associated Types type SBit (What4 sym) :: Type Source # type SWord (What4 sym) :: Type Source # type SInteger (What4 sym) :: Type Source # type SFloat (What4 sym) :: Type Source # type SEval (What4 sym) :: Type -> Type Source # Methods isReady :: What4 sym -> SEval (What4 sym) a -> Bool Source # sDeclareHole :: What4 sym -> String -> SEval (What4 sym) (SEval (What4 sym) a, SEval (What4 sym) a -> SEval (What4 sym) ()) Source # sDelayFill :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source # sSpark :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source # mergeEval :: What4 sym -> (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a) -> SBit (What4 sym) -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) a Source # assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) () Source # raiseError :: What4 sym -> EvalError -> SEval (What4 sym) a Source # ppBit :: What4 sym -> SBit (What4 sym) -> Doc Source # ppWord :: What4 sym -> PPOpts -> SWord (What4 sym) -> Doc Source # ppInteger :: What4 sym -> PPOpts -> SInteger (What4 sym) -> Doc Source # ppFloat :: What4 sym -> PPOpts -> SFloat (What4 sym) -> Doc Source # bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool Source # wordLen :: What4 sym -> SWord (What4 sym) -> Integer Source # wordAsLit :: What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer) Source # wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char Source # integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer Source # bitLit :: What4 sym -> Bool -> SBit (What4 sym) Source # wordLit :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym)) Source # integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym)) Source # fpLit :: What4 sym -> Integer -> Integer -> Rational -> SEval (What4 sym) (SFloat (What4 sym)) Source # iteBit :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # iteWord :: What4 sym -> SBit (What4 sym) -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # iteInteger :: What4 sym -> SBit (What4 sym) -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # bitEq :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # bitOr :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # bitAnd :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # bitXor :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # bitComplement :: What4 sym -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # wordBit :: What4 sym -> SWord (What4 sym) -> Integer -> SEval (What4 sym) (SBit (What4 sym)) Source # wordUpdate :: What4 sym -> SWord (What4 sym) -> Integer -> SBit (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # packWord :: What4 sym -> [SBit (What4 sym)] -> SEval (What4 sym) (SWord (What4 sym)) Source # unpackWord :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)] Source # wordFromInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # joinWord :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # splitWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym)) Source # extractWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordOr :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordAnd :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordXor :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordComplement :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordPlus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordMinus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordMult :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordSignedDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordSignedMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordNegate :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordLg2 :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordEq :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # wordSignedLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # wordLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # wordGreaterThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # wordToInt :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intPlus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intNegate :: What4 sym -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intMinus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intMult :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intDiv :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intMod :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # intEq :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # intLessThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # intGreaterThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # intToZn :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znToInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znPlus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znNegate :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znMinus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znMult :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # znEq :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpLessThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpGreaterThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpPlus :: FPArith2 (What4 sym) Source # fpMinus :: FPArith2 (What4 sym) Source # fpMult :: FPArith2 (What4 sym) Source # fpDiv :: FPArith2 (What4 sym) Source # fpNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source # fpToInteger :: What4 sym -> String -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source # fpFromInteger :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #
type SBit (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value type SBit (What4 sym) = Pred sym
type SWord (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value type SWord (What4 sym) = SWord sym
type SInteger (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value type SInteger (What4 sym) = SymInteger sym
type SFloat (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value type SFloat (What4 sym) = SFloat sym
type SEval (What4 sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value type SEval (What4 sym) = W4Eval sym

type Value sym = GenValue (What4 sym) Source #

newtype W4Eval sym a Source #

This is the monad used for symbolic evaluation. It adds to aspects to Eval' keeps track of the backend and collects definitional predicates, and W4Eval adds support for partially defined values

Constructors

W4Eval
Fields evalPartial :: W4Conn sym (W4Result sym a)

Instances

IsExprBuilder sym => Monad (W4Eval sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods (>>=) :: W4Eval sym a -> (a -> W4Eval sym b) -> W4Eval sym b # (>>) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym b # return :: a -> W4Eval sym a # fail :: String -> W4Eval sym a #
IsExprBuilder sym => Functor (W4Eval sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods fmap :: (a -> b) -> W4Eval sym a -> W4Eval sym b # (<$) :: a -> W4Eval sym b -> W4Eval sym a #
IsExprBuilder sym => Applicative (W4Eval sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods pure :: a -> W4Eval sym a # (<>) :: W4Eval sym (a -> b) -> W4Eval sym a -> W4Eval sym b # liftA2 :: (a -> b -> c) -> W4Eval sym a -> W4Eval sym b -> W4Eval sym c # (>) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym b # (<*) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym a #
IsExprBuilder sym => MonadIO (W4Eval sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods liftIO :: IO a -> W4Eval sym a #

newtype W4Conn sym a Source #

This layer has the symbolic back-end, and can keep track of definitional predicates used when working with uninterpreted constants defined via a property.

Constructors

W4Conn
Fields evalConn :: sym -> Eval (W4Defs sym a)

Instances

IsExprBuilder sym => Monad (W4Conn sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods (>>=) :: W4Conn sym a -> (a -> W4Conn sym b) -> W4Conn sym b # (>>) :: W4Conn sym a -> W4Conn sym b -> W4Conn sym b # return :: a -> W4Conn sym a # fail :: String -> W4Conn sym a #
IsExprBuilder sym => Functor (W4Conn sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods fmap :: (a -> b) -> W4Conn sym a -> W4Conn sym b # (<$) :: a -> W4Conn sym b -> W4Conn sym a #
IsExprBuilder sym => Applicative (W4Conn sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods pure :: a -> W4Conn sym a # (<>) :: W4Conn sym (a -> b) -> W4Conn sym a -> W4Conn sym b # liftA2 :: (a -> b -> c) -> W4Conn sym a -> W4Conn sym b -> W4Conn sym c # (>) :: W4Conn sym a -> W4Conn sym b -> W4Conn sym b # (<*) :: W4Conn sym a -> W4Conn sym b -> W4Conn sym a #
IsExprBuilder sym => MonadIO (W4Conn sym) Source #
Instance details Defined in Cryptol.Eval.What4.Value Methods liftIO :: IO a -> W4Conn sym a #

data W4Defs sym a Source #

Keep track of a value and a context defining uninterpeted vairables.

Constructors

W4Defs
Fields w4Defs :: !(Pred sym) w4Result :: !a

data W4Result sym a Source #

The symbolic value we computed.

Constructors

W4Error !EvalError	A malformed value
W4Result !(Pred sym) !a	safety predicate and result: the result only makes sense when the predicate holds.

w4Eval :: W4Eval sym a -> sym -> Eval (W4Defs sym (W4Result sym a)) Source #

w4Thunk :: Eval (W4Defs sym (W4Result sym a)) -> W4Eval sym a Source #

doEval :: IsExprBuilder sym => Eval a -> W4Conn sym a Source #

A value with no context.

total :: IsExprBuilder sym => W4Conn sym a -> W4Eval sym a Source #

A total value.

getSym :: IsExprBuilder sym => W4Conn sym sym Source #

Access the symbolic back-end

addDef :: Pred sym -> W4Conn sym () Source #

Record a definition.

w4And :: IsExprBuilder sym => Pred sym -> Pred sym -> W4Conn sym (Pred sym) Source #

Compute conjunction.

w4Not :: IsExprBuilder sym => Pred sym -> W4Conn sym (Pred sym) Source #

Compute negation.

w4ITE :: IsExprBuilder sym => Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym) Source #

Compute if-then-else.

addDefEqn :: IsExprBuilder sym => Pred sym -> W4Eval sym () Source #

Add a definitional equation. This will always be asserted when we make queries to the solver.

addSafety :: IsExprBuilder sym => Pred sym -> W4Eval sym () Source #

Add s safety condition.

evalError :: IsExprBuilder sym => EvalError -> W4Eval sym a Source #

A fully undefined symbolic value

assertBVDivisor :: IsExprBuilder sym => sym -> SWord sym -> W4Eval sym () Source #

assertIntDivisor :: IsExprBuilder sym => sym -> SymInteger sym -> W4Eval sym () Source #

sModAdd :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModSub :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModMult :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModNegate :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> IO (SymInteger sym) Source #

sLg2 :: IsExprBuilder sym => sym -> SWord sym -> SEval (What4 sym) (SWord sym) Source #

Try successive powers of 2 to find the first that dominates the input. We could perhaps reduce to using CLZ instead...

evalPanic :: String -> [String] -> a Source #

lazyIte :: (IsExpr p, Monad m) => (p BaseBoolType -> a -> a -> m a) -> p BaseBoolType -> m a -> m a -> m a Source #

indexFront_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexBack_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexFront_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexBack_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexFront_bits :: forall sym. IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym) Source #

indexBack_bits :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym) Source #

wordValueEqualsInteger :: forall sym. IsExprBuilder sym => sym -> WordValue (What4 sym) -> Integer -> W4Eval sym (Pred sym) Source #

Compare a symbolic word value with a concrete integer.

updateFrontSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym)) Source #

updateBackSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym)) Source #

updateFrontSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym)) Source #

updateBackSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym)) Source #

sshrV :: IsExprBuilder sym => sym -> Value sym Source #

w4bvShl :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvLshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvAshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvRol :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvRor :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

fpRoundingMode :: IsExprBuilder sym => What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode Source #

fpBinArith :: IsExprBuilder sym => SFloatBinArith sym -> What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpCvtToInteger :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym) Source #

fpCvtToRational :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> SFloat sym -> SEval sym (SRational sym) Source #

fpCvtFromRational :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym) Source #