| Copyright | (c) Galois Inc 2014-2016 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Simulator.Evaluation
Description
This module provides operations evaluating Crucible expressions.
Synopsis
- type EvalAppFunc sym app = forall f. (forall tp. f tp -> IO (RegValue sym tp)) -> forall tp. app f tp -> IO (RegValue sym tp)
- evalApp :: forall sym bak ext. IsSymBackend sym bak => bak -> IntrinsicTypes sym -> (Int -> String -> IO ()) -> EvalAppFunc sym (ExprExtension ext) -> EvalAppFunc sym (App ext)
- selectedIndices :: [Bool] -> [Natural]
- indexSymbolic :: IsSymBackend sym bak => bak -> (Pred sym -> a -> a -> IO a) -> ([Natural] -> IO a) -> [(Natural, Natural)] -> [SymNat sym] -> IO a
- integerAsChar :: Integer -> Word16
- complexRealAsChar :: (MonadFail m, IsExpr val) => val BaseComplexType -> m Word16
- indexVectorWithSymNat :: IsSymBackend sym bak => bak -> (Pred sym -> a -> a -> IO a) -> Vector a -> SymNat sym -> IO a
- adjustVectorWithSymNat :: IsSymBackend sym bak => bak -> (Pred sym -> a -> a -> IO a) -> Vector a -> SymNat sym -> (a -> IO a) -> IO (Vector a)
- updateVectorWithSymNat :: IsSymBackend sym bak => bak -> (Pred sym -> a -> a -> IO a) -> Vector a -> SymNat sym -> a -> IO (Vector a)
Documentation
type EvalAppFunc sym app = forall f. (forall tp. f tp -> IO (RegValue sym tp)) -> forall tp. app f tp -> IO (RegValue sym tp) Source #
Arguments
| :: forall sym bak ext. IsSymBackend sym bak | |
| => bak | |
| -> IntrinsicTypes sym | |
| -> (Int -> String -> IO ()) | Function for logging messages. |
| -> EvalAppFunc sym (ExprExtension ext) | |
| -> EvalAppFunc sym (App ext) |
Evaluate the application.
selectedIndices :: [Bool] -> [Natural] Source #
Given a list of Booleans l, selectedIndices returns the indices of
true values in l.
Arguments
| :: IsSymBackend sym bak | |
| => bak | |
| -> (Pred sym -> a -> a -> IO a) | Function for combining results together. |
| -> ([Natural] -> IO a) | Concrete index function. |
| -> [(Natural, Natural)] | High and low bounds at the indices. |
| -> [SymNat sym] | |
| -> IO a |
Lookup a value in an array that may be at a symbolic offset.
This function takes a list of symbolic indices as natural numbers along with a pair of lower and upper bounds for each index. It assumes that the indices are all in range.
integerAsChar :: Integer -> Word16 Source #
complexRealAsChar :: (MonadFail m, IsExpr val) => val BaseComplexType -> m Word16 Source #
indexVectorWithSymNat Source #
Arguments
| :: IsSymBackend sym bak | |
| => bak | |
| -> (Pred sym -> a -> a -> IO a) | Ite function |
| -> Vector a | |
| -> SymNat sym | |
| -> IO a |
Get value stored in vector at a symbolic index.
adjustVectorWithSymNat Source #
Arguments
| :: IsSymBackend sym bak | |
| => bak | Symbolic backend |
| -> (Pred sym -> a -> a -> IO a) | Ite function |
| -> Vector a | Vector to update |
| -> SymNat sym | Index to update |
| -> (a -> IO a) | Adjustment function to apply |
| -> IO (Vector a) |
Update a vector at a given natural number index.
updateVectorWithSymNat Source #
Arguments
| :: IsSymBackend sym bak | |
| => bak | Symbolic backend |
| -> (Pred sym -> a -> a -> IO a) | Ite function |
| -> Vector a | Vector to update |
| -> SymNat sym | Index to update |
| -> a | New value to assign |
| -> IO (Vector a) |
Update a vector at a given natural number index.