Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- moduleEnv :: EvalPrims sym => sym -> Module -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
- runEval :: CallStack -> Eval a -> IO a
- data EvalOpts = EvalOpts {
- evalLogger :: Logger
- evalPPOpts :: PPOpts
- data PPOpts = PPOpts {
- useAscii :: Bool
- useBase :: Int
- useInfLength :: Int
- useFPBase :: Int
- useFPFormat :: PPFloatFormat
- useFieldOrder :: FieldOrder
- defaultPPOpts :: PPOpts
- data Eval a
- type EvalEnv = GenEvalEnv Concrete
- emptyEnv :: GenEvalEnv sym
- evalExpr :: (?range :: Range, EvalPrims sym) => sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
- evalDecls :: EvalPrims sym => sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
- evalNewtypeDecls :: EvalPrims sym => sym -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
- evalSel :: Backend sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
- evalSetSel :: forall sym. Backend sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- data EvalError
- data EvalErrorEx = EvalErrorEx CallStack EvalError
- data Unsupported = UnsupportedSymbolicOp String
- data WordTooWide = WordTooWide Integer
- forceValue :: Backend sym => GenValue sym -> SEval sym ()
Documentation
:: EvalPrims sym | |
=> sym | |
-> Module | Module containing declarations to evaluate |
-> GenEvalEnv sym | Environment to extend |
-> SEval sym (GenEvalEnv sym) |
Extend the given evaluation environment with all the declarations contained in the given module.
Some options for evalutaion
EvalOpts | |
|
How to pretty print things when evaluating
PPOpts | |
|
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.
type EvalEnv = GenEvalEnv Concrete Source #
emptyEnv :: GenEvalEnv sym Source #
Evaluation environment with no bindings
:: (?range :: Range, EvalPrims sym) | |
=> sym | |
-> GenEvalEnv sym | Evaluation environment |
-> Expr | Expression to evaluate |
-> SEval sym (GenValue sym) |
Evaluate a Cryptol expression to a value. This evaluator is parameterized
by the EvalPrims
class, which defines the behavior of bits and words, in
addition to providing implementations for all the primitives.
:: EvalPrims sym | |
=> sym | |
-> [DeclGroup] | Declaration groups to evaluate |
-> GenEvalEnv sym | Environment to extend |
-> SEval sym (GenEvalEnv sym) |
Extend the given evaluation environment with the result of evaluating the given collection of declaration groups.
evalNewtypeDecls :: EvalPrims sym => sym -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym) Source #
evalSel :: Backend sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym) Source #
Apply the the given "selector" form to the given value. Note that selectors are expected to apply only to values of the right type, e.g. tuple selectors expect only tuple values. The lifting of tuple an record selectors over functions and sequences has already been resolved earlier in the typechecker.
evalSetSel :: forall sym. Backend sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #
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 |
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 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 |