Cryptol.Backend.What4

Documentation

data What4 sym

Constructors

What4

Fields

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

Instances

IsSymExprBuilder sym => Backend (What4 sym)

Defined in Cryptol.Backend.What4

Associated Types

type SBit (What4 sym)

type SWord (What4 sym)

type SInteger (What4 sym)

type SFloat (What4 sym)

type SEval (What4 sym) :: Type -> Type

Methods

isReady :: What4 sym -> SEval (What4 sym) a -> Bool

sDeclareHole :: What4 sym -> String -> SEval (What4 sym) (SEval (What4 sym) a, SEval (What4 sym) a -> SEval (What4 sym) ())

sDelayFill :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a)

sSpark :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a)

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

assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()

raiseError :: What4 sym -> EvalError -> SEval (What4 sym) a

ppBit :: What4 sym -> SBit (What4 sym) -> Doc

ppWord :: What4 sym -> PPOpts -> SWord (What4 sym) -> Doc

ppInteger :: What4 sym -> PPOpts -> SInteger (What4 sym) -> Doc

ppFloat :: What4 sym -> PPOpts -> SFloat (What4 sym) -> Doc

bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool

wordLen :: What4 sym -> SWord (What4 sym) -> Integer

wordAsLit :: What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer)

wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char

integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer

bitLit :: What4 sym -> Bool -> SBit (What4 sym)

wordLit :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym))

integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))

fpLit :: What4 sym -> Integer -> Integer -> Rational -> SEval (What4 sym) (SFloat (What4 sym))

fpExactLit :: What4 sym -> BF -> SEval (What4 sym) (SFloat (What4 sym))

iteBit :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

iteWord :: What4 sym -> SBit (What4 sym) -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

iteInteger :: What4 sym -> SBit (What4 sym) -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

bitEq :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

bitOr :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

bitAnd :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

bitXor :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

bitComplement :: What4 sym -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

wordBit :: What4 sym -> SWord (What4 sym) -> Integer -> SEval (What4 sym) (SBit (What4 sym))

wordUpdate :: What4 sym -> SWord (What4 sym) -> Integer -> SBit (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

packWord :: What4 sym -> [SBit (What4 sym)] -> SEval (What4 sym) (SWord (What4 sym))

unpackWord :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)]

wordFromInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

joinWord :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

splitWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym))

extractWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordOr :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordAnd :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordXor :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordComplement :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordPlus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordMinus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordMult :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordSignedDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordSignedMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordNegate :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordLg2 :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))

wordEq :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

wordSignedLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

wordLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

wordGreaterThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

wordToInt :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intPlus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intNegate :: What4 sym -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intMinus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intMult :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intDiv :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intMod :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

intEq :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

intLessThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

intGreaterThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

intToZn :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znToInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znPlus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znNegate :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znMinus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znMult :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

znEq :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

znRecip :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

fpEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

fpLessThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

fpGreaterThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

fpLogicalEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))

fpPlus :: FPArith2 (What4 sym)

fpMinus :: FPArith2 (What4 sym)

fpMult :: FPArith2 (What4 sym)

fpDiv :: FPArith2 (What4 sym)

fpNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))

fpToInteger :: What4 sym -> String -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))

fpFromInteger :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))

type SBit (What4 sym)

Defined in Cryptol.Backend.What4

type SBit (What4 sym) = Pred sym

type SWord (What4 sym)

Defined in Cryptol.Backend.What4

type SWord (What4 sym) = SWord sym

type SInteger (What4 sym)

Defined in Cryptol.Backend.What4

type SInteger (What4 sym) = SymInteger sym

type SFloat (What4 sym)

Defined in Cryptol.Backend.What4

type SFloat (What4 sym) = SFloat sym

type SEval (What4 sym)

Defined in Cryptol.Backend.What4

type SEval (What4 sym) = W4Eval sym

type What4FunCache sym = Map Text (SomeSymFn sym)

data SomeSymFn sym

Constructors

forall args ret. SomeSymFn (SymFn sym args ret)

newtype W4Eval sym a

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

IsSymExprBuilder sym => Monad (W4Eval sym)

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

IsSymExprBuilder sym => Functor (W4Eval sym)

Defined in Cryptol.Backend.What4

Methods

fmap :: (a -> b) -> W4Eval sym a -> W4Eval sym b

(<$) :: a -> W4Eval sym b -> W4Eval sym a

IsSymExprBuilder sym => Applicative (W4Eval sym)

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 => MonadIO (W4Eval sym)

Defined in Cryptol.Backend.What4

Methods

liftIO :: IO a -> W4Eval sym a

newtype W4Conn sym a

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

IsSymExprBuilder sym => Monad (W4Conn sym)

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

IsSymExprBuilder sym => Functor (W4Conn sym)

Defined in Cryptol.Backend.What4

Methods

fmap :: (a -> b) -> W4Conn sym a -> W4Conn sym b

(<$) :: a -> W4Conn sym b -> W4Conn sym a

IsSymExprBuilder sym => Applicative (W4Conn sym)

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 => MonadIO (W4Conn sym)

Defined in Cryptol.Backend.What4

Methods

liftIO :: IO a -> W4Conn sym a

data W4Result sym a

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 (W4Result sym a)

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

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

A value with no context.

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

A total value.

getSym :: W4Conn sym sym

Access the symbolic back-end

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

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)

Compute negation.

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

Compute if-then-else.

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

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

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

Add s safety condition.

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

A fully undefined symbolic value

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)

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

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)