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

Cryptol.Backend.What4

Description

Synopsis

data What4 sym = What4 {
- w4 :: sym
- w4defs :: MVar (Pred sym)
- w4funs :: MVar (What4FunCache sym)
- w4uninterpWarns :: MVar (Set Text)
}
type What4FunCache sym = Map Text (SomeSymFn sym)
data SomeSymFn sym = forall args ret. SomeSymFn (SymFn sym args ret)
newtype W4Eval sym a = W4Eval {
- evalPartial :: W4Conn sym (W4Result sym a)
}
newtype W4Conn sym a = W4Conn {
- evalConn :: sym -> Eval a
}
data W4Result sym a
- = W4Error !EvalErrorEx
- | W4Result !(Pred sym) !a
w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a
doEval :: IsSymExprBuilder sym => Eval a -> W4Conn sym a
total :: IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
getSym :: W4Conn sym sym
w4And :: IsSymExprBuilder sym => Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4Not :: IsSymExprBuilder sym => Pred sym -> W4Conn sym (Pred sym)
w4ITE :: IsSymExprBuilder sym => Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
addDefEqn :: IsSymExprBuilder sym => What4 sym -> Pred sym -> W4Eval sym ()
addSafety :: IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
evalError :: IsSymExprBuilder sym => EvalError -> W4Eval sym a
assertBVDivisor :: IsSymExprBuilder sym => What4 sym -> SWord sym -> W4Eval sym ()
assertIntDivisor :: IsSymExprBuilder sym => What4 sym -> SymInteger sym -> W4Eval sym ()
sModAdd :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModSub :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModMult :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
sModNegate :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sLg2 :: IsSymExprBuilder 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
w4bvShl :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvLshr :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvAshr :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRol :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRor :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
fpRoundingMode :: IsSymExprBuilder sym => What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpBinArith :: IsSymExprBuilder sym => SFloatBinArith sym -> What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
fpCvtToInteger :: (IsSymExprBuilder 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 :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym)
sModRecip :: IsSymExprBuilder sym => What4 sym -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)

Documentation

data What4 sym Source #

Constructors

What4
Fields w4 :: sym w4defs :: MVar (Pred sym) w4funs :: MVar (What4FunCache sym) w4uninterpWarns :: MVar (Set Text)

Instances

Instances details

IsSymExprBuilder sym => Backend (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 Associated Types type SBit (What4 sym) Source # type SWord (What4 sym) Source # type SInteger (What4 sym) Source # type SFloat (What4 sym) Source # type SEval (What4 sym) :: Type -> Type Source # Methods isReady :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (Maybe a) 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 -> Maybe (SEval (What4 sym) a) -> String -> SEval (What4 sym) (SEval (What4 sym) a) Source # sSpark :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source # sPushFrame :: What4 sym -> Name -> Range -> SEval (What4 sym) a -> SEval (What4 sym) a Source # sWithCallStack :: What4 sym -> CallStack -> SEval (What4 sym) a -> SEval (What4 sym) a Source # sModifyCallStack :: What4 sym -> (CallStack -> CallStack) -> SEval (What4 sym) a -> SEval (What4 sym) a Source # sGetCallStack :: What4 sym -> SEval (What4 sym) CallStack 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 # 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 # fpAsLit :: What4 sym -> SFloat (What4 sym) -> Maybe BF 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 # fpExactLit :: What4 sym -> BF -> 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 # iteFloat :: What4 sym -> SBit (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (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 # wordShiftLeft :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordShiftRight :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordSignedShiftRight :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordRotateLeft :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # wordRotateRight :: 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 # wordToSignedInt :: 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 # znRecip :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (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 # fpLogicalEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpNaN :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym)) Source # fpPosInf :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SFloat (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 # fpAbs :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source # fpSqrt :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source # fpFMA :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source # fpIsZero :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpIsNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpIsNaN :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpIsInf :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpIsNorm :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpIsSubnorm :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source # fpToBits :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source # fpFromBits :: What4 sym -> Integer -> Integer -> SWord (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 # fpToRational :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym)) Source # fpFromRational :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SRational (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #
type SBit (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 type SBit (What4 sym) = Pred sym
type SEval (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 type SEval (What4 sym) = W4Eval sym
type SFloat (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 type SFloat (What4 sym) = SFloat sym
type SInteger (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 type SInteger (What4 sym) = SymInteger sym
type SWord (What4 sym) Source #
Instance details Defined in Cryptol.Backend.What4 type SWord (What4 sym) = SWord sym

type What4FunCache sym = Map Text (SomeSymFn sym) Source #

data SomeSymFn sym Source #

Constructors

forall args ret. SomeSymFn (SymFn sym args ret)

newtype W4Eval sym a Source #

This is the monad used for symbolic evaluation. It adds to aspects to Eval---WConn 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

Instances details

IsSymExprBuilder sym => MonadIO (W4Eval sym) Source #
Instance details Defined in Cryptol.Backend.What4 Methods liftIO :: IO a -> W4Eval sym a #
IsSymExprBuilder sym => Applicative (W4Eval sym) Source #
Instance details Defined in Cryptol.Backend.What4 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 #
IsSymExprBuilder sym => Functor (W4Eval sym) Source #
Instance details Defined in Cryptol.Backend.What4 Methods fmap :: (a -> b) -> W4Eval sym a -> W4Eval sym b # (<$) :: a -> W4Eval sym b -> W4Eval sym a #
IsSymExprBuilder sym => Monad (W4Eval sym) Source #
Instance details Defined in Cryptol.Backend.What4 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 #

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 a

Instances

Instances details

IsSymExprBuilder sym => MonadIO (W4Conn sym) Source #
Instance details Defined in Cryptol.Backend.What4 Methods liftIO :: IO a -> W4Conn sym a #
IsSymExprBuilder sym => Applicative (W4Conn sym) Source #
Instance details Defined in Cryptol.Backend.What4 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 #
IsSymExprBuilder sym => Functor (W4Conn sym) Source #
Instance details Defined in Cryptol.Backend.What4 Methods fmap :: (a -> b) -> W4Conn sym a -> W4Conn sym b # (<$) :: a -> W4Conn sym b -> W4Conn sym a #
IsSymExprBuilder sym => Monad (W4Conn sym) Source #
Instance details Defined in Cryptol.Backend.What4 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 #

data W4Result sym a Source #

The symbolic value we computed.

Constructors

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

Instances

Instances details

Functor (W4Result sym) Source #
Instance details Defined in Cryptol.Backend.What4 Methods fmap :: (a -> b) -> W4Result sym a -> W4Result sym b # (<$) :: a -> W4Result sym b -> W4Result sym a #

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

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

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

A value with no context.

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

A total value.

getSym :: W4Conn sym sym Source #

Access the symbolic back-end

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

Record a definition. addDef :: W4.Pred sym -> W4Conn sym () addDef p = W4Conn _ -> pure W4Defs { w4Defs = p, w4Result = () }

Compute conjunction.

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

Compute negation.

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

Compute if-then-else.

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

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

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

Add s safety condition.

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

A fully undefined symbolic value

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

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

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

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

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

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

sLg2 :: IsSymExprBuilder 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 #

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

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

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

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

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

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

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

fpCvtToInteger :: (IsSymExprBuilder 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 :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym) Source #

sModRecip :: IsSymExprBuilder sym => What4 sym -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym) Source #