Lang.Crucible.Simulator.EvalStmt

This module provides functions for evaluating Crucible statements.

High-level evaluation

singleStepCrucible

Arguments

:: (IsSymInterface sym, IsSyntaxExtension ext)

=> Int

Current verbosity

-> ExecState p sym ext rtp

-> IO (ExecState p sym ext rtp)

Run a single step of the Crucible symbolic simulator.

executeCrucible

Arguments

:: forall p sym ext rtp. (IsSymInterface sym, IsSyntaxExtension ext)

=> [ExecutionFeature p sym ext rtp]

Execution features to install

-> ExecState p sym ext rtp

Execution state to begin executing

-> IO (ExecResult p sym ext rtp)

Given a SimState and an execution continuation, apply the continuation and execute the resulting computation until completion.

This function is responsible for catching AbortExecReason exceptions and UserError exceptions and invoking the errorHandler contained in the state.

newtype ExecutionFeature p sym ext rtp

An execution feature represents a computation that is allowed to intercept the processing of execution states to perform additional processing at each intermediate state. A list of execution features is accepted by executeCrucible. After each step of the simulator, the execution features are consulted, each in turn. After all the execution features have run, the main simulator code is executed to advance the simulator one step.

If an execution feature wishes to make changes to the execution state before further execution happens, the return value can be used to return a modified state. If this happens, the current stack of execution features is abandoned and a fresh step starts over immediately from the top of the execution features. In essence, each execution feature can preempt all following execution features and the main simulator loop. In other words, the main simulator only gets reached if every execution feature returns Nothing. It is important, therefore, that execution features make only a bounded number of modification in a row, or the main simulator loop will be starved out.

Constructors

ExecutionFeature

Fields

• runExecutionFeature :: ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)

newtype GenericExecutionFeature sym

A generic execution feature is an execution feature that is agnostic to the execution environment, and is therefore polymorphic over the p, ext and rtp variables.

Constructors

GenericExecutionFeature

Fields

• runGenericExecutionFeature :: forall p ext rtp. (IsSymInterface sym, IsSyntaxExtension ext) => ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)

data ExecutionFeatureResult p sym ext rtp where

This datatype indicates the possible results that an execution feature can have.

Constructors

ExecutionFeatureNoChange :: ExecutionFeatureResult p sym ext rtp

This execution feature result indicates that no state changes were made.

ExecutionFeatureModifiedState :: ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp

This execution feature indicates that the state was modified but not changed in an "essential" way. For example, internal bookkeeping datastructures for the execution feature might be modified, but the state is not transitioned to a fundamentally different state.

When this result is returned, later execution features in the installed stack will be executed, until the main simulator loop is encountered. Contrast with the "new state" result.

ExecutionFeatureNewState :: ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp

This execution feature result indicates that the state was modified in an essential way that transforms it into new state altogether. When this result is returned, it preempts any later execution features and the main simulator loop and instead returns to the head of the execution feature stack.

NOTE: In particular, the execution feature will encounter the state again before the simulator loop. It is therefore very important that the execution feature be prepared to immediately encounter the same state again and make significant execution progress on it, or ignore it so it makes it to the main simulator loop. Otherwise, the execution feature will loop back to itself infinitely, starving out useful work.

genericToExecutionFeature :: (IsSymInterface sym, IsSyntaxExtension ext) => GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp

timeoutFeature :: NominalDiffTime -> IO (GenericExecutionFeature sym)

This feature will terminate the execution of a crucible simulator with a TimeoutResult after a given interval of wall-clock time has elapsed.

Lower-level evaluation operations

dispatchExecState

Arguments

:: (IsSymInterface sym, IsSyntaxExtension ext)

=> IO Int

Action to query the current verbosity

-> ExecState p sym ext rtp

Current execution state of the simulator

-> (ExecResult p sym ext rtp -> IO z)

Final continuation for results

-> (forall f a. ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z)

Intermediate continuation for running states

-> IO z

Given an ExecState, examine it and either enter the continuation for final results, or construct the appropriate ExecCont for continuing the computation and enter the provided intermediate continuation.

advanceCrucibleState :: (IsSymInterface sym, IsSyntaxExtension ext) => ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)

Run the given ExecCont on the given SimState, being careful to catch any simulator abort exceptions that are thrown and dispatch them to the abort handler.

evalReg :: Monad m => Reg ctx tp -> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)

Retrieve the value of a register.

evalReg' :: Monad m => Reg ctx tp -> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)

Retrieve the value of a register, returning a RegEntry.

evalExpr

Arguments

:: forall p sym ext ctx tp rtp blocks r. (IsSymInterface sym, IsSyntaxExtension ext)

=> Int

current verbosity

-> Expr ext ctx tp

-> ReaderT (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)

Evaluate an expression.

evalArgs :: Monad m => Assignment (Reg ctx) args -> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)

Evaluate the actual arguments for a function call or block transfer.

evalJumpTarget

Arguments

:: (IsSymInterface sym, Monad m)

=> JumpTarget blocks ctx

Jump target to evaluate

-> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (ResolvedJump sym blocks)

Resolve the arguments for a jump.

evalSwitchTarget

Arguments

:: (IsSymInterface sym, Monad m)

=> SwitchTarget blocks ctx tp

Switch target to evaluate

-> RegEntry sym tp

Value inside the variant

-> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (ResolvedJump sym blocks)

Resolve the arguments for a switch target.

stepStmt

Arguments

:: forall p sym ext rtp blocks r ctx ctx'. (IsSymInterface sym, IsSyntaxExtension ext)

=> Int

Current verbosity

-> Stmt ext ctx ctx'

Statement to evaluate

-> StmtSeq ext blocks r ctx'

Remaining statements in the block

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

Evaluation operation for evaluating a single straight-line statement of the Crucible evaluator.

This is allowed to throw user exceptions or SimError.

stepTerm

Arguments

:: forall p sym ext rtp blocks r ctx. (IsSymInterface sym, IsSyntaxExtension ext)

=> Int

Verbosity

-> TermStmt blocks r ctx

Terminating statement to evaluate

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

Evaluation operation for evaluating a single block-terminator statement of the Crucible evaluator.

This is allowed to throw user exceptions or SimError.

stepBasicBlock

Arguments

:: (IsSymInterface sym, IsSyntaxExtension ext)

=> Int

Current verbosity

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

Main evaluation operation for running a single step of basic block evaluation.

This is allowed to throw user exceptions or SimError.

readRef :: IsSymBackend sym bak => bak -> IntrinsicTypes sym -> TypeRepr tp -> MuxTree sym (RefCell tp) -> SymGlobalState sym -> IO (RegValue sym tp)

Read from a reference cell.

alterRef :: IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> MuxTree sym (RefCell tp) -> PartExpr (Pred sym) (RegValue sym tp) -> SymGlobalState sym -> IO (SymGlobalState sym)

Update a reference cell with a new value. Writing an unassigned value resets the reference cell to an uninitialized state.