Lang.Crucible.Simulator.Operations

Operations corresponding to basic control-flow events on simulator execution trees.

Control-flow operations

continue :: RunningStateInfo blocks a -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)

Immediately transition to a RunningState. On the next execution step, the simulator will interpret the next basic block.

jumpToBlock

Arguments

:: IsSymInterface sym

=> ResolvedJump sym blocks

Jump target and arguments

-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)

Transfer control to the given resolved jump, after first checking for any pending symbolic merges at the destination of the jump.

conditionalBranch

Arguments

:: (IsSymInterface sym, IsSyntaxExtension ext)

=> Pred sym

Predicate to branch on

-> ResolvedJump sym blocks

True branch

-> ResolvedJump sym blocks

False branch

-> ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx)

Perform a conditional branch on the given predicate. If the predicate is symbolic, this will record a symbolic branch state.

variantCases

Arguments

:: IsSymInterface sym

=> [(Pred sym, ResolvedJump sym blocks)]

Variant branches to execute

-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)

Execute the next branch of a sequence of branch cases. These arise from the implementation of the VariantElim construct. The predicates are expected to be mutually disjoint. However, the construct still has well defined semantics even in the case where they overlap; in this case, the first branch with a true Pred is taken. In other words, each branch assumes the negation of all the predicates of branches appearing before it.

In the final default case (corresponding to an empty list of branches), a VariantOptionsExhausted abort will be executed.

returnValue

Arguments

:: forall p sym ext rtp f args. RegEntry sym (FrameRetType f)

return value

-> ExecCont p sym ext rtp f args

Return a value from current Crucible execution.

callFunction

Arguments

:: IsExprBuilder sym

=> FnVal sym args ret

Function handle and any closure variables

-> RegMap sym args

Arguments to the function

-> ReturnHandler ret p sym ext rtp f a

How to modify the caller's scope with the return value

-> ProgramLoc

location of call

-> ExecCont p sym ext rtp f a

tailCallFunction

Arguments

:: FrameRetType f ~ ret

=> FnVal sym args ret

Function handle and any closure variables

-> RegMap sym args

Arguments to the function

-> ValueFromValue p sym ext rtp ret

-> ProgramLoc

location of call

-> ExecCont p sym ext rtp f a

runOverride

Arguments

:: Override p sym ext args ret

Override to execute

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

Immediately transtition to an OverrideState. On the next execution step, the simulator will execute the given override.

runAbortHandler

Arguments

:: AbortExecReason

Description of the abort condition

-> SimState p sym ext rtp f args

Simulator state prior to the abort

-> IO (ExecState p sym ext rtp)

Immediately transition to an AbortState. On the next execution step, the simulator will unwind the SimState and resolve the abort.

runErrorHandler

Arguments

:: SimErrorReason

Description of the error

-> SimState p sym ext rtp f args

Simulator state prior to the abort

-> IO (ExecState p sym ext rtp)

Abort the current thread of execution with an error. This adds a proof obligation that requires the current execution path to be infeasible, and unwids to the nearest branch point to resume.

runGenericErrorHandler

Arguments

:: String

Generic description of the error condition

-> SimState p sym ext rtp f args

Simulator state prior to the abort

-> IO (ExecState p sym ext rtp)

Abort the current thread of execution with an error. This adds a proof obligation that requires the current execution path to be infeasible, and unwids to the nearest branch point to resume.

performIntraFrameMerge

Arguments

:: IsSymInterface sym

=> CrucibleBranchTarget f args

The location of the block we are transferring to

-> ExecCont p sym ext root f args

Perform a single instance of path merging at a join point. This will resume an alternate branch, if it is pending, or merge result values if a completed branch has alread reached this point. If there are no pending merge points at this location, continue executing by transfering control to the given target.

performIntraFrameSplit

Arguments

:: IsSymInterface sym

=> Pred sym

Branch condition

-> PausedFrame p sym ext rtp f

active branch.

-> PausedFrame p sym ext rtp f

other branch.

-> CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType))

Postdominator merge point, where both branches meet again.

-> ExecCont p sym ext rtp f ('Just dc_args)

Branch with a merge point inside this frame.

performFunctionCall :: IsSymInterface sym => ReturnHandler ret p sym ext rtp outer_frame outer_args -> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp outer_frame outer_args

performTailCall :: IsSymInterface sym => ValueFromValue p sym ext rtp ret -> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp f a

performReturn

Arguments

:: IsSymInterface sym

=> FunctionName

Name of the function we are returning from

-> ValueFromValue p sym ext r ret

Context to return to.

-> RegEntry sym ret

Value that is being returned.

-> ExecCont p sym ext r f a

Resolve the return value, and begin executing in the caller's context again.

performControlTransfer :: IsSymInterface sym => ControlResumption p sym ext rtp f -> ExecCont p sym ext rtp f ('Just a)

resumeFrame :: IsSymInterface sym => PausedFrame p sym ext rtp f -> ValueFromFrame p sym ext rtp f -> ExecCont p sym ext rtp g ba

Resume a paused frame.

resumeValueFromValueAbort :: IsSymInterface sym => ValueFromValue p sym ext r ret' -> AbortedResult sym ext -> ExecCont p sym ext r f a

Run rest of execution given a value from value context and an aborted result.

overrideSymbolicBranch

Arguments

:: IsSymInterface sym

=> Pred sym

-> RegMap sym then_args

-> ExecCont p sym ext rtp (OverrideLang r) ('Just then_args)

if branch

-> Maybe Position

optional if branch location

-> RegMap sym else_args

-> ExecCont p sym ext rtp (OverrideLang r) ('Just else_args)

else branch

-> Maybe Position

optional else branch location

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

Resolving calls

data ResolvedCall p sym ext ret where

The result of resolving a function call.

Constructors

OverrideCall :: !(Override p sym ext args ret) -> !(OverrideFrame sym ret args) -> ResolvedCall p sym ext ret

A resolved function call to an override.

CrucibleCall :: !(BlockID blocks args) -> !(CallFrame sym ext blocks ret args) -> ResolvedCall p sym ext ret

A resolved function call to a Crucible function.

data UnresolvableFunction where

This exception is thrown if a FnHandle cannot be resolved to a callable function. This usually indicates a programming error, but might also be used to allow on-demand function loading.

The ProgramLoc argument references the call site for the unresolved function call.

The [SomeFrame] argument is the active call stack at the time of the exception.

Constructors

UnresolvableFunction :: !ProgramLoc -> [SomeFrame (SimFrame sym ext)] -> !(FnHandle args ret) -> UnresolvableFunction

Instances

Exception UnresolvableFunction

Defined in Lang.Crucible.Simulator.Operations

Methods

toException :: UnresolvableFunction -> SomeException

fromException :: SomeException -> Maybe UnresolvableFunction

displayException :: UnresolvableFunction -> String

Show UnresolvableFunction

Defined in Lang.Crucible.Simulator.Operations

Methods

showsPrec :: Int -> UnresolvableFunction -> ShowS

show :: UnresolvableFunction -> String

showList :: [UnresolvableFunction] -> ShowS

resolveCall

Arguments

:: FunctionBindings p sym ext

Map from function handles to semantics

-> FnVal sym args ret

Function handle and any closure variables

-> RegMap sym args

Arguments to the function

-> ProgramLoc

Location of the call

-> [SomeFrame (SimFrame sym ext)]

current call stack (for exceptions)

-> ResolvedCall p sym ext ret

Given a set of function bindings, a function- value (which is possibly a closure) and a collection of arguments, resolve the identity of the function to call, and set it up to be called.

Will throw an UnresolvableFunction exception if the underlying function handle is not found in the FunctionBindings map.

resolvedCallName :: ResolvedCall p sym ext ret -> FunctionName

Abort handlers

abortExecAndLog :: IsSymInterface sym => AbortExecReason -> ExecCont p sym ext rtp f args

Abort the current execution and roll back to the nearest symbolic branch point. When verbosity is 3 or more, a message will be logged indicating the reason for the abort.

The default abort handler calls this function.

abortExec :: IsSymInterface sym => AbortExecReason -> ExecCont p sym ext rtp f args

Abort the current execution and roll back to the nearest symbolic branch point.

defaultAbortHandler :: IsSymInterface sym => AbortHandler p sym ext rtp

The default abort handler calls abortExecAndLog.

Call tree manipulations

pushCallFrame

Arguments

:: ReturnHandler (FrameRetType a) p sym ext r f old_args

What to do with the result of the function

-> SimFrame sym ext a args

The code to run

-> ActiveTree p sym ext r f old_args

-> ActiveTree p sym ext r a args

replaceTailFrame :: forall p sym ext a b c args args'. FrameRetType a ~ FrameRetType c => ActiveTree p sym ext b a args -> SimFrame sym ext c args' -> Maybe (ActiveTree p sym ext b c args')

Replace the given frame with a new frame. Succeeds only if there are no pending symbolic merge points.

isSingleCont :: ValueFromFrame p sym ext root a -> Bool

Returns true if tree contains a single non-aborted execution.

unwindContext :: ValueFromFrame p sym ext root f -> Maybe (ValueFromValue p sym ext root (FrameRetType f))

Attempt to unwind a frame context into a value context. This succeeds only if there are no pending symbolic merges.

extractCurrentPath :: ActiveTree p sym ext ret f args -> ActiveTree p sym ext ret f args

Create a tree that contains just a single path with no branches.

All branch conditions are converted to assertions.

asContFrame :: ActiveTree p sym ext ret f args -> ValueFromFrame p sym ext ret f

Return the context of the current top frame.

forgetPostdomFrame :: PausedFrame p sym ext rtp g -> PausedFrame p sym ext rtp g