Lang.Crucible.Simulator.Evaluation

This module provides operations evaluating Crucible expressions.

Documentation

type EvalAppFunc sym app = forall f. (forall tp. f tp -> IO (RegValue sym tp)) -> forall tp. app f tp -> IO (RegValue sym tp)

evalApp

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]

Given a list of Booleans l, selectedIndices returns the indices of true values in l.

indexSymbolic

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

complexRealAsChar :: (MonadFail m, IsExpr val) => val BaseComplexType -> m Word16

indexVectorWithSymNat

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

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

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.