Lang.Crucible.Simulator.OverrideSim

Define the main simulation monad OverrideSim and basic operations on it.

Monad definition

newtype OverrideSim p sym ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType) a

Monad for running symbolic simulator.

Type parameters:

• p the "personality", i.e. user-defined state parameterized by sym
• sym the symbolic backend
• ext the syntax extension (Lang.Crucible.CFG.Extension)
• rtp global return type
• args argument types for the current frame
• ret return type of the current frame
• a the value type

Constructors

Sim

Fields

• unSim :: StateContT (SimState p sym ext rtp (OverrideLang ret) ('Just args)) (ExecState p sym ext rtp) IO a

Instances

MonadST RealWorld (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

liftST :: ST RealWorld a -> OverrideSim p sym ext rtp args ret a

MonadFail (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

fail :: String -> OverrideSim p sym ext rtp args ret a

MonadIO (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

liftIO :: IO a -> OverrideSim p sym ext rtp args ret a

Applicative (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

pure :: a -> OverrideSim p sym ext rtp args ret a

(<*>) :: OverrideSim p sym ext rtp args ret (a -> b) -> OverrideSim p sym ext rtp args ret a -> OverrideSim p sym ext rtp args ret b

liftA2 :: (a -> b -> c) -> OverrideSim p sym ext rtp args ret a -> OverrideSim p sym ext rtp args ret b -> OverrideSim p sym ext rtp args ret c

(*>) :: OverrideSim p sym ext rtp args ret a -> OverrideSim p sym ext rtp args ret b -> OverrideSim p sym ext rtp args ret b

(<*) :: OverrideSim p sym ext rtp args ret a -> OverrideSim p sym ext rtp args ret b -> OverrideSim p sym ext rtp args ret a

Functor (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

fmap :: (a -> b) -> OverrideSim p sym ext rtp args ret a -> OverrideSim p sym ext rtp args ret b

(<$) :: a -> OverrideSim p sym ext rtp args ret b -> OverrideSim p sym ext rtp args ret a

Monad (OverrideSim p sym ext rtp args r)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

(>>=) :: OverrideSim p sym ext rtp args r a -> (a -> OverrideSim p sym ext rtp args r b) -> OverrideSim p sym ext rtp args r b

(>>) :: OverrideSim p sym ext rtp args r a -> OverrideSim p sym ext rtp args r b -> OverrideSim p sym ext rtp args r b

return :: a -> OverrideSim p sym ext rtp args r a

MonadVerbosity (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

getVerbosity :: OverrideSim p sym ext rtp args ret Int

whenVerbosity :: (Int -> Bool) -> OverrideSim p sym ext rtp args ret () -> OverrideSim p sym ext rtp args ret ()

getLogFunction :: OverrideSim p sym ext rtp args ret (Int -> String -> IO ())

getLogLnFunction :: OverrideSim p sym ext rtp args ret (Int -> String -> IO ())

showWarning :: String -> OverrideSim p sym ext rtp args ret ()

showWarningWhen :: (Int -> Bool) -> String -> OverrideSim p sym ext rtp args ret ()

MonadThrow (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

throwM :: (HasCallStack, Exception e) => e -> OverrideSim p sym ext rtp args ret a

MonadCont (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

callCC :: ((a -> OverrideSim p sym ext rtp args ret b) -> OverrideSim p sym ext rtp args ret a) -> OverrideSim p sym ext rtp args ret a

MonadState (SimState p sym ext rtp (OverrideLang ret) ('Just args)) (OverrideSim p sym ext rtp args ret)

Defined in Lang.Crucible.Simulator.OverrideSim

Methods

get :: OverrideSim p sym ext rtp args ret (SimState p sym ext rtp (OverrideLang ret) ('Just args))

put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret ()

state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a

runOverrideSim

Arguments

:: TypeRepr tp

return type

-> OverrideSim p sym ext rtp args tp (RegValue sym tp)

action to execute

-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)

Turn an OverrideSim action into an ExecCont that can be executed using standard Crucible execution primitives like executeCrucible.

Monad operations

withSimContext :: StateT (SimContext p sym ext) IO a -> OverrideSim p sym ext rtp args ret a

getContext :: OverrideSim p sym ext rtp args ret (SimContext p sym ext)

getSymInterface :: OverrideSim p sym ext rtp args ret sym

ovrWithBackend :: (forall bak. IsSymBackend sym bak => bak -> OverrideSim p sym ext rtp args ret a) -> OverrideSim p sym ext rtp args ret a

bindFnHandle :: FnHandle args ret -> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()

Associate a definition (either an Override or a CFG) with the given handle.

bindCFG :: CFG ext blocks args ret -> OverrideSim p sym ext rtp a r ()

Bind a CFG to its handle.

Computes postdominator information.

exitExecution :: IsSymInterface sym => ExitCode -> OverrideSim p sym ext rtp args r a

Exit from the current execution by ignoring the continuation and immediately returning an aborted execution result.

getOverrideArgs :: OverrideSim p sym ext rtp args ret (RegMap sym args)

Return override arguments.

overrideError :: IsSymInterface sym => SimErrorReason -> OverrideSim p sym ext rtp args res a

Add a failed assertion. This aborts execution along the current evaluation path, and adds a proof obligation ensuring that we can't get here in the first place.

overrideAbort :: AbortExecReason -> OverrideSim p sym ext rtp args res a

Abort the current thread of execution for the given reason. Unlike overrideError, this operation will not add proof obligation, even if the given abort reason is due to an assertion failure. Use overrideError instead if a proof obligation should be generated.

symbolicBranch

Arguments

:: IsSymInterface sym

=> Pred sym

Predicate to branch on

-> RegMap sym then_args

argument values for the then branch

-> OverrideSim p sym ext rtp then_args res a

then branch

-> Maybe Position

optional location for then branch

-> RegMap sym else_args

argument values for the else branch

-> OverrideSim p sym ext rtp else_args res a

else branch

-> Maybe Position

optional location for else branch

-> OverrideSim p sym ext rtp args res a

Perform a symbolic branch on the given predicate. If we can determine that the predicate must be either true or false, we will exeucte only the "then" or the "else" branch. Otherwise, both branches will be executed and the results merged when a value is returned from the override. NOTE! this means the code following this symbolic branch may be executed more than once; in particular, side effects may happen more than once.

In order to ensure that pushabortmux bookeeping is done properly, all symbolic values that will be used in the branches should be inserted into the RegMap argument of this function, and retrieved in the branches using the getOverrideArgs function. Otherwise mux errors may later occur, which will be very confusing. In other words, don't directly use symbolic values computed before calling this function; you must instead first put them into the RegMap and get them out again later.

symbolicBranches

Arguments

:: forall p sym ext rtp args new_args res a. IsSymInterface sym

=> RegMap sym new_args

argument values for the branches

-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)]

Branches to consider

-> OverrideSim p sym ext rtp args res a

Perform a series of symbolic branches. This operation will evaluate a series of branches, one for each element of the list. The semantics of this construct is that the predicates are evaluated in order, until the first one that evaluates true; this branch will be the taken branch. In other words, this operates like a chain of if-then-else statements; later branches assume that earlier branches were not taken.

If no predicate is true, the construct will abort with a VariantOptionsExhausted reason. If you wish to report an error condition instead, you should add a final default case with a true predicate that calls overrideError. As with symbolicBranch, be aware that code following this operation may be called several times, and side effects may occur more than once.

As with symbolicBranch, any symbolic values needed by the branches should be placed into the RegMap argument and retrieved when needed. See the comment on symbolicBranch.

nondetBranches

Arguments

:: forall p sym ext rtp args new_args res a. IsSymInterface sym

=> RegMap sym new_args

argument values for the branches

-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)]

Branches to consider

-> OverrideSim p sym ext rtp args res a

Non-deterministically choose among several feasible branches.

Unlike symbolicBranches, this function does not take only the first branch with a predicate that evaluates to true; instead it takes all branches with predicates that are not syntactically false (or cannot be proved unreachable with path satisfiability checking, if enabled). Each branch will not assume that other branches weren't taken.

As with symbolicBranch, any symbolic values needed by the branches should be placed into the RegMap argument and retrieved when needed. See the comment on symbolicBranch.

Operationally, this works by by numbering all of the branches from 0 to n, inventing a symbolic integer variable z, and adding z = i (where i ranges from 0 to n) to the branch condition for each branch, and calling symbolicBranches on the result. Even though each branch given to symbolicBranches assumes earlier branches are not taken, each branch condition has the form (z = i) and p, so the negation ~((z = i) and p) is equivalent to (z != i) or ~p, so later branches don't assume the negation of the branch condition of earlier branches (i.e., ~p).

overrideReturn :: KnownRepr TypeRepr res => RegValue sym res -> OverrideSim p sym ext rtp args res a

overrideReturn' :: RegEntry sym res -> OverrideSim p sym ext rtp args res a

Function calls

callFnVal

Arguments

:: (IsExprBuilder sym, IsSyntaxExtension ext)

=> FnVal sym args ret

Function to call

-> RegMap sym args

Arguments to the function

-> OverrideSim p sym ext rtp a r (RegEntry sym ret)

Call a function with the given arguments.

callFnVal'

Arguments

:: (IsExprBuilder sym, IsSyntaxExtension ext)

=> FnVal sym args ret

Function to call

-> Assignment (RegValue' sym) args

Arguments to the function

-> OverrideSim p sym ext rtp a r (RegValue sym ret)

Call a function with the given arguments. Provide the arguments as an Assignment instead of as a RegMap.

callCFG

Arguments

:: IsSyntaxExtension ext

=> CFG ext blocks init ret

Function to run

-> RegMap sym init

Arguments to the function

-> OverrideSim p sym ext rtp a r (RegEntry sym ret)

Call a control flow graph from OverrideSim.

Note that this computes the postdominator information, so there is some performance overhead in the call.

callBlock

Arguments

:: IsSyntaxExtension ext

=> CFG ext blocks init ret

Function to run

-> BlockID blocks args

Block to run

-> RegMap sym args

Arguments to the block

-> OverrideSim p sym ext rtp a r (RegEntry sym ret)

Call a block of a control flow graph from OverrideSim.

Note that this computes the postdominator information, so there is some performance overhead in the call.

callOverride :: FnHandle args ret -> Override p sym ext args ret -> RegMap sym args -> OverrideSim p sym ext rtp a r (RegEntry sym ret)

Call an override in a new call frame.

Global variables

readGlobal

Arguments

:: IsSymInterface sym

=> GlobalVar tp

global variable

-> OverrideSim p sym ext rtp args ret (RegValue sym tp)

current value

Read a particular global variable from the global variable state.

writeGlobal

Arguments

:: GlobalVar tp

global variable

-> RegValue sym tp

new value

-> OverrideSim p sym ext rtp args ret ()

Set the value of a particular global variable.

readGlobals :: OverrideSim p sym ext rtp args ret (SymGlobalState sym)

Read the whole sym global state.

writeGlobals :: SymGlobalState sym -> OverrideSim p sym ext rtp args ret ()

Overwrite the whole sym global state

modifyGlobal

Arguments

:: IsSymInterface sym

=> GlobalVar tp

global variable to modify

-> (RegValue sym tp -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))

modification action

-> OverrideSim p sym ext rtp args ret a

Run an action to compute the new value of a global.

References

newRef

Arguments

:: IsSymInterface sym

=> TypeRepr tp

Type of the reference cell

-> RegValue sym tp

Initial value of the cell

-> OverrideSim p sym ext rtp args ret (RefCell tp)

Create a new reference cell.

newEmptyRef

Arguments

:: TypeRepr tp

Type of the reference cell

-> OverrideSim p sym ext rtp args ret (RefCell tp)

Create a new reference cell with no contents.

readRef

Arguments

:: IsSymInterface sym

=> RefCell tp

Reference cell to read

-> OverrideSim p sym ext rtp args ret (RegValue sym tp)

Read the current value of a reference cell.

writeRef

Arguments

:: IsSymInterface sym

=> RefCell tp

Reference cell to write

-> RegValue sym tp

Value to write into the cell

-> OverrideSim p sym ext rtp args ret ()

Write a value into a reference cell.

modifyRef

Arguments

:: IsSymInterface sym

=> RefCell tp

Reference cell to modify

-> (RegValue sym tp -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))

modification action

-> OverrideSim p sym ext rtp args ret a

readMuxTreeRef

Arguments

:: IsSymInterface sym

=> TypeRepr tp

-> MuxTree sym (RefCell tp)

Reference cell to read

-> OverrideSim p sym ext rtp args ret (RegValue sym tp)

Read the current value of a mux tree of reference cells.

writeMuxTreeRef

Arguments

:: IsSymInterface sym

=> TypeRepr tp

-> MuxTree sym (RefCell tp)

Reference cell to write

-> RegValue sym tp

Value to write into the cell

-> OverrideSim p sym ext rtp args ret ()

Write a value into a mux tree of reference cells.

Function bindings

data FnBinding p sym ext where

A pair containing a handle and the state associated to execute it.

Constructors

FnBinding :: FnHandle args ret -> FnState p sym ext args ret -> FnBinding p sym ext

fnBindingsFromList :: [FnBinding p sym ext] -> FunctionBindings p sym ext

Build a map of function bindings from a list of handle/binding pairs.

registerFnBinding :: FnBinding p sym ext -> OverrideSim p sym ext rtp a r ()

data AnyFnBindings ext

This quantifies over function bindings that can work for any symbolic interface.

Constructors

AnyFnBindings (forall p sym. IsSymInterface sym => [FnBinding p sym ext])

Overrides

mkOverride :: KnownRepr TypeRepr ret => FunctionName -> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret)) -> Override p sym ext args ret

Create an override from a statically inferrable return type and definition using OverrideSim.

mkOverride' :: FunctionName -> TypeRepr ret -> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret)) -> Override p sym ext args ret

Create an override from an explicit return type and definition using OverrideSim.

Intrinsic implementations

type IntrinsicImpl p sym ext args ret = IsSymInterface sym => FnHandle args ret -> Override p sym ext args ret

mkIntrinsic

Arguments

:: forall p sym ext args ret. CurryAssignmentClass args

=> (forall r. Proxy r -> sym -> CurryAssignment args (RegEntry sym) (OverrideSim p sym ext r args ret (RegValue sym ret)))

Override implementation, given a proxy value to fix the type, a reference to the symbolic engine, and a curried arguments

-> FnHandle args ret

-> Override p sym ext args ret

Make an IntrinsicImpl from an explicit implementation

useIntrinsic :: FnHandle args ret -> (FnHandle args ret -> Override p sym ext args ret) -> FnBinding p sym ext

Typed overrides

data TypedOverride p sym ext args ret

An action in OverrideSim, together with TypeReprs for its arguments and return values. This type is used across several frontends to define overrides for built-in functions, e.g., malloc in the LLVM frontend.

For maximal reusability, frontends may define TypedOverrides that are polymorphic in (any of) p, sym, and ext.

Constructors

TypedOverride

Fields

• typedOverrideHandler :: forall rtp args' ret'. Assignment (RegValue' sym) args -> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
• typedOverrideArgs :: CtxRepr args
• typedOverrideRet :: TypeRepr ret

data SomeTypedOverride p sym ext

A TypedOverride with the type parameters args, ret existentially quantified

Constructors

forall args ret. SomeTypedOverride (TypedOverride p sym ext args ret)

runTypedOverride :: FunctionName -> TypedOverride p sym ext args ret -> Override p sym ext args ret

Create an override from a TypedOverride.

Re-exports

data Override p sym ext (args :: Ctx CrucibleType) ret

A definition of a function's semantics, given as a Haskell action.