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

Cryptol.Eval.What4

Description

Synopsis

data What4 sym = What4 sym
data W4Result sym a
- = W4Error !EvalError
- | W4Result !(Pred sym) !a
data W4Defs sym a = W4Defs {
- w4Defs :: !(Pred sym)
- w4Result :: !a
}
data W4Eval sym a
w4Eval :: W4Eval sym a -> sym -> Eval (W4Defs sym (W4Result sym a))
type Value sym = GenValue (What4 sym)
evalPrim :: IsSymExprBuilder sym => sym -> PrimIdent -> Maybe (Value 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

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.

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

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 #

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

type Value sym = GenValue (What4 sym) Source #

evalPrim :: IsSymExprBuilder sym => sym -> PrimIdent -> Maybe (Value sym) Source #