cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Eval

Description

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
  - = 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
- data Unsupported = UnsupportedSymbolicOp String
- data WordTooWide = WordTooWide Integer
- forceValue :: Backend sym => GenValue sym -> SEval sym ()
- checkProp :: Prop -> Bool

# Documentation

moduleEnv Source #

Arguments

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

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

Execute the given evaluation action.

data EvalOpts Source #

Some options for evalutaion

Constructors

EvalOpts |

Fields

- evalLogger :: Logger

  Where to print stuff (e.g., for `trace`)

- evalPPOpts :: PPOpts

  How to pretty print things.

data PPOpts Source #

How to pretty print things when evaluating

Constructors

PPOpts |

Fields

- useAscii :: Bool
- useBase :: Int
- useInfLength :: Int
- useFPBase :: Int
- useFPFormat :: PPFloatFormat
- useFieldOrder :: FieldOrder

#### Instances

Instances details

Show PPOpts Source # |
Instance details Defined in Cryptol.Utils.PP Methods showsPrec :: Int -> PPOpts -> ShowS Source # show :: PPOpts -> String Source # showList :: [PPOpts] -> ShowS Source #

defaultPPOpts :: PPOpts Source #

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.

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

type EvalEnv = GenEvalEnv Concrete Source #

emptyEnv :: GenEvalEnv sym Source #

Evaluation environment with no bindings

evalExpr Source #

Arguments

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

evalDecls Source #

Arguments

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

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

forceValue :: Backend sym => GenValue sym -> SEval sym () Source #

Force the evaluation of a value

checkProp :: Prop -> Bool Source #

Checks whether an evaluated `Prop` holds