Copyright | (c) 2013-2020 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Synopsis
- data Eval a
- runEval :: CallStack -> Eval a -> IO a
- io :: IO a -> Eval a
- delayFill :: Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
- ready :: a -> Eval a
- blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
- evalSpark :: Eval a -> Eval (Eval a)
- maybeReady :: Eval a -> Eval (Maybe a)
- data CallStack
- getCallStack :: Eval CallStack
- withCallStack :: CallStack -> Eval a -> Eval a
- modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a
- combineCallStacks :: CallStack -> CallStack -> CallStack
- pushCallFrame :: Name -> Range -> CallStack -> CallStack
- displayCallStack :: CallStack -> Doc
- data Unsupported = UnsupportedSymbolicOp String
- data EvalError
- data EvalErrorEx = EvalErrorEx CallStack EvalError
- evalPanic :: HasCallStack => String -> [String] -> a
- wordTooWide :: Integer -> a
- data WordTooWide = WordTooWide Integer
Evaluation monad
The monad for Cryptol evaluation. A computation is either "ready", which means it represents only trivial computation, or is an "eval" action which must be computed to get the answer, or it is a "thunk", which represents a delayed, shared computation.
:: Eval a | Computation to delay |
-> Maybe (Eval a) | Optional backup computation to run if a tight loop is detected |
-> String | message for the exception if a tight loop is detected |
-> Eval (Eval a) |
Delay the given evaluation computation, returning a thunk
which will run the computation when forced. Run the retry
computation instead if the resulting thunk is forced during
its own evaluation.
Produce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.
evalSpark :: Eval a -> Eval (Eval a) Source #
Begin executing the given operation in a separate thread, returning a thunk which will await the completion of the computation when forced.
maybeReady :: Eval a -> Eval (Maybe a) Source #
Test if a value is "ready", which means that it requires no computation to return.
Call stacks
The type of dynamic call stacks for the interpreter. New frames are pushed onto the right side of the sequence.
getCallStack :: Eval CallStack Source #
Get the current call stack
modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a Source #
Run the given action with a modify call stack
:: CallStack | call stack of the application context |
-> CallStack | call stack of the function being applied |
-> CallStack |
Combine the call stack of a function value with the call stack of the current calling context. This algorithm is the same one GHC uses to compute profiling calling contexts.
The algorithm is as follows.
ccs ++> ccsfn = ccs ++ dropCommonPrefix ccs ccsfn
where
dropCommonPrefix A B -- returns the suffix of B after removing any prefix common -- to both A and B.
pushCallFrame :: Name -> Range -> CallStack -> CallStack Source #
Add a call frame to the top of a call stack
displayCallStack :: CallStack -> Doc Source #
Pretty print a call stack with each call frame on a separate line, with most recent call frames at the top.
Error reporting
data Unsupported Source #
UnsupportedSymbolicOp String | Operation cannot be supported in the symbolic simulator |
Instances
Show Unsupported Source # | |
Defined in Cryptol.Backend.Monad showsPrec :: Int -> Unsupported -> ShowS # show :: Unsupported -> String # showList :: [Unsupported] -> ShowS # | |
Exception Unsupported Source # | |
Defined in Cryptol.Backend.Monad | |
PP Unsupported Source # | |
Defined in Cryptol.Backend.Monad |
Data type describing errors that can occur during evaluation.
InvalidIndex (Maybe Integer) | Out-of-bounds index |
DivideByZero | Division or modulus by 0 |
NegativeExponent | Exponentiation by negative integer |
LogNegative | Logarithm of a negative integer |
UserError String | Call to the Cryptol |
LoopError String | Detectable nontermination |
NoPrim Name | Primitive with no implementation |
BadRoundingMode Integer | Invalid rounding mode |
BadValue String | Value outside the domain of a partial function. |
data EvalErrorEx Source #
Instances
Show EvalErrorEx Source # | |
Defined in Cryptol.Backend.Monad showsPrec :: Int -> EvalErrorEx -> ShowS # show :: EvalErrorEx -> String # showList :: [EvalErrorEx] -> ShowS # | |
Exception EvalErrorEx Source # | |
Defined in Cryptol.Backend.Monad | |
PP EvalErrorEx Source # | |
Defined in Cryptol.Backend.Monad |
wordTooWide :: Integer -> a Source #
For when we know that a word is too wide and will exceed gmp's limits (though words approaching this size will probably cause the system to crash anyway due to lack of memory).
data WordTooWide Source #
WordTooWide Integer | Bitvector too large |
Instances
Show WordTooWide Source # | |
Defined in Cryptol.Backend.Monad showsPrec :: Int -> WordTooWide -> ShowS # show :: WordTooWide -> String # showList :: [WordTooWide] -> ShowS # | |
Exception WordTooWide Source # | |
Defined in Cryptol.Backend.Monad | |
PP WordTooWide Source # | |
Defined in Cryptol.Backend.Monad |