cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2020 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell2010

Cryptol.Backend.Monad

Contents

- Evaluation monad
- Call stacks
- Error reporting

Description

Synopsis

- data Eval a
  - = Ready !a
  - | Eval !(CallStack -> IO a)
  - | Thunk !(TVar (ThunkState 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
  - = InvalidIndex (Maybe Integer)
  - | DivideByZero
  - | NegativeExponent
  - | LogNegative
  - | UserError String
  - | LoopError String
  - | NoPrim Name
  - | BadRoundingMode Integer
  - | BadValue String
  - | NoMatchingPropGuardCase String
  - | FFINotSupported Name
  - | FFITypeNumTooBig Name TParam Integer
- data EvalErrorEx = EvalErrorEx CallStack EvalError
- evalPanic :: HasCallStack => String -> [String] -> a
- wordTooWide :: Integer -> a
- data WordTooWide = WordTooWide Integer

# Evaluation monad

data Eval a Source #

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.

Constructors

Ready !a |
Eval !(CallStack -> IO a) |
Thunk !(TVar (ThunkState a)) |

#### Instances

Instances details

MonadIO Eval Source # |
Instance details Defined in Cryptol.Backend.Monad Methods liftIO :: IO a -> Eval a Source #
Applicative Eval Source # |
Instance details Defined in Cryptol.Backend.Monad Methods pure :: a -> Eval a Source # (<*>) :: Eval (a -> b) -> Eval a -> Eval b Source # liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c Source # (*>) :: Eval a -> Eval b -> Eval b Source # (<*) :: Eval a -> Eval b -> Eval a Source #
Functor Eval Source # |
Instance details Defined in Cryptol.Backend.Monad Methods fmap :: (a -> b) -> Eval a -> Eval b Source # (<$) :: a -> Eval b -> Eval a Source #
Monad Eval Source # |
Instance details Defined in Cryptol.Backend.Monad Methods (>>=) :: Eval a -> (a -> Eval b) -> Eval b Source # (>>) :: Eval a -> Eval b -> Eval b Source # return :: a -> Eval a Source #

runEval :: CallStack -> Eval a -> IO a Source #

Execute the given evaluation action.

io :: IO a -> Eval a Source #

Lift an `IO` computation into the `Eval` monad.

delayFill Source #

Arguments

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

ready :: a -> Eval a Source #

A computation that returns an already-evaluated value.

blackhole Source #

Arguments

:: String | A name to associate with this thunk.
-> Eval (Eval a, Eval a -> Eval ()) |

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

data CallStack Source #

The type of dynamic call stacks for the interpreter. New frames are pushed onto the right side of the sequence.

#### Instances

Instances details

Monoid CallStack Source # |
Instance details Defined in Cryptol.Backend.Monad Methods mempty :: CallStack Source # mappend :: CallStack -> CallStack -> CallStack Source # mconcat :: [CallStack] -> CallStack Source #
Semigroup CallStack Source # |
Instance details Defined in Cryptol.Backend.Monad Methods (<>) :: CallStack -> CallStack -> CallStack Source # sconcat :: NonEmpty CallStack -> CallStack Source # stimes :: Integral b => b -> CallStack -> CallStack Source #

getCallStack :: Eval CallStack Source #

Get the current call stack

withCallStack :: CallStack -> Eval a -> Eval a Source #

Execute the action with the given call stack

modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a Source #

Run the given action with a modify call stack

combineCallStacks Source #

Arguments

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

Constructors

UnsupportedSymbolicOp String | Operation cannot be supported in the symbolic simulator

#### Instances

Instances details

Exception Unsupported Source # |
Instance details Defined in Cryptol.Backend.Monad Methods toException :: Unsupported -> SomeException Source # fromException :: SomeException -> Maybe Unsupported Source # displayException :: Unsupported -> String Source #
Show Unsupported Source # |
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> Unsupported -> ShowS Source # show :: Unsupported -> String Source # showList :: [Unsupported] -> ShowS Source #
PP Unsupported Source # |
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> Unsupported -> Doc Source #

data EvalError Source #

Data type describing errors that can occur during evaluation.

Constructors

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 `error` primitive
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.
NoMatchingPropGuardCase String | No prop guard holds for the given type variables.
FFINotSupported Name | Foreign function cannot be called
FFITypeNumTooBig Name TParam Integer | Number passed to foreign function as a type argument is too large

#### Instances

Instances details

Show EvalError Source # |
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> EvalError -> ShowS Source # show :: EvalError -> String Source # showList :: [EvalError] -> ShowS Source #
PP EvalError Source # |
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> EvalError -> Doc Source #

data EvalErrorEx Source #

Constructors

EvalErrorEx CallStack EvalError |

#### Instances

Instances details

Exception EvalErrorEx Source # |
Instance details Defined in Cryptol.Backend.Monad Methods toException :: EvalErrorEx -> SomeException Source # fromException :: SomeException -> Maybe EvalErrorEx Source # displayException :: EvalErrorEx -> String Source #
Show EvalErrorEx Source # |
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> EvalErrorEx -> ShowS Source # show :: EvalErrorEx -> String Source # showList :: [EvalErrorEx] -> ShowS Source #
PP EvalErrorEx Source # |
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> EvalErrorEx -> Doc Source #

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

Panic from an `Eval` context.

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 #

Constructors

WordTooWide Integer | Bitvector too large

#### Instances

Instances details

Exception WordTooWide Source # |
Instance details Defined in Cryptol.Backend.Monad Methods toException :: WordTooWide -> SomeException Source # fromException :: SomeException -> Maybe WordTooWide Source # displayException :: WordTooWide -> String Source #
Show WordTooWide Source # |
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> WordTooWide -> ShowS Source # show :: WordTooWide -> String Source # showList :: [WordTooWide] -> ShowS Source #
PP WordTooWide Source # |
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> WordTooWide -> Doc Source #