crucible-0.7: src/Lang/Crucible/Simulator/EvalStmt.hs
-----------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.Simulator.EvalStmt
-- Description : Provides functions for evaluating statements.
-- Copyright : (c) Galois, Inc 2013-2018
-- License : BSD3
-- Maintainer : Joe Hendrix <jhendrix@galois.com>
-- Stability : provisional
--
-- This module provides functions for evaluating Crucible statements.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.EvalStmt
( -- * High-level evaluation
singleStepCrucible
, executeCrucible
, ExecutionFeature(..)
, GenericExecutionFeature(..)
, ExecutionFeatureResult(..)
, genericToExecutionFeature
, timeoutFeature
-- * Lower-level evaluation operations
, dispatchExecState
, advanceCrucibleState
, evalReg
, evalReg'
, evalExpr
, evalArgs
, evalJumpTarget
, evalSwitchTarget
, stepStmt
, stepTerm
, stepBasicBlock
, readRef
, alterRef
) where
import qualified Control.Exception as Ex
import Control.Lens
import Control.Monad (foldM, when)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader (ReaderT(..), withReaderT)
import Data.Maybe (fromMaybe)
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.TraversableFC
import qualified Data.Text as Text
import Data.Time.Clock
import System.IO
import System.IO.Error as Ex
import Prettyprinter
import What4.Config
import What4.Interface
import What4.InterpretedFloatingPoint (freshFloatConstant)
import What4.Partial
import What4.ProgramLoc
import Lang.Crucible.Backend
import Lang.Crucible.CFG.Core
import Lang.Crucible.CFG.Extension
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Simulator.CallFrame
import Lang.Crucible.Simulator.Evaluation
import Lang.Crucible.Simulator.ExecutionTree
import Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes)
import Lang.Crucible.Simulator.GlobalState
import Lang.Crucible.Simulator.Operations
import Lang.Crucible.Simulator.RegMap
import Lang.Crucible.Simulator.SimError
import Lang.Crucible.Utils.MuxTree
-- | Retrieve the value of a register.
evalReg ::
Monad m =>
Reg ctx tp ->
ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg r = (`regVal` r) <$> view (stateCrucibleFrame.frameRegs)
-- | Retrieve the value of a register, returning a 'RegEntry'.
evalReg' ::
Monad m =>
Reg ctx tp ->
ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' r = (`regVal'` r) <$> view (stateCrucibleFrame.frameRegs)
evalLogFn ::
Int {- current verbosity -} ->
CrucibleState p sym ext rtp blocks r ctx ->
Int {- verbosity level of the message -} ->
String ->
IO ()
evalLogFn verb s n msg = do
let h = s^.stateContext.to printHandle
if verb >= n then
do hPutStr h msg
hFlush h
else
return ()
-- | Evaluate an expression.
evalExpr :: 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)
evalExpr verb (App a) = ReaderT $ \s ->
do let iteFns = s^.stateIntrinsicTypes
let simCtx = s^.stateContext
let logFn = evalLogFn verb s
r <- withBackend simCtx $ \bak ->
evalApp bak iteFns logFn
(extensionEval (extensionImpl (s^.stateContext)) bak iteFns logFn s)
(\r -> runReaderT (evalReg r) s)
a
return $! r
evalArgs' :: forall sym ctx args.
RegMap sym ctx ->
Ctx.Assignment (Reg ctx) args ->
RegMap sym args
evalArgs' m0 args = RegMap (fmapFC (getEntry m0) args)
where getEntry :: RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
getEntry (RegMap m) r = m Ctx.! regIndex r
{-# NOINLINE evalArgs' #-}
-- | Evaluate the actual arguments for a function call or block transfer.
evalArgs ::
Monad m =>
Ctx.Assignment (Reg ctx) args ->
ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs args = ReaderT $ \s -> return $! evalArgs' (s^.stateCrucibleFrame.frameRegs) args
{-# INLINE evalArgs #-}
-- | Resolve the arguments for a jump.
evalJumpTarget ::
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx {- ^ Jump target to evaluate -} ->
ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (ResolvedJump sym blocks)
evalJumpTarget (JumpTarget tgt _ a) = ResolvedJump tgt <$> evalArgs a
-- | Resolve the arguments for a switch target.
evalSwitchTarget ::
(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)
evalSwitchTarget (SwitchTarget tgt _tp a) x =
do xs <- evalArgs a
return (ResolvedJump tgt (assignReg' x xs))
-- | Update a reference cell with a new value. Writing an unassigned
-- value resets the reference cell to an uninitialized state.
alterRef ::
IsSymInterface sym =>
sym ->
IntrinsicTypes sym ->
TypeRepr tp ->
MuxTree sym (RefCell tp) ->
PartExpr (Pred sym) (RegValue sym tp) ->
SymGlobalState sym ->
IO (SymGlobalState sym)
alterRef sym iTypes tpr rs newv globs = foldM upd globs (viewMuxTree rs)
where
f p a b = liftIO $ muxRegForType sym iTypes tpr p a b
upd gs (r,p) =
do let oldv = lookupRef r globs
z <- mergePartial sym f p newv oldv
return (gs & updateRef r z)
-- | Read from a reference cell.
readRef ::
IsSymBackend sym bak =>
bak ->
IntrinsicTypes sym ->
TypeRepr tp ->
MuxTree sym (RefCell tp) ->
SymGlobalState sym ->
IO (RegValue sym tp)
readRef bak iTypes tpr rs globs =
do let sym = backendGetSym bak
let vs = map (\(r,p) -> (p,lookupRef r globs)) (viewMuxTree rs)
let f p a b = liftIO $ muxRegForType sym iTypes tpr p a b
pv <- mergePartials sym f vs
let msg = ReadBeforeWriteSimError "Attempted to read uninitialized reference cell"
readPartExpr bak pv msg
-- | Evaluation operation for evaluating a single straight-line
-- statement of the Crucible evaluator.
--
-- This is allowed to throw user exceptions or 'SimError'.
stepStmt :: 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)
stepStmt verb stmt rest =
do ctx <- view stateContext
let sym = ctx^.ctxSymInterface
let iTypes = ctxIntrinsicTypes ctx
globals <- view (stateTree.actFrame.gpGlobals)
let continueWith :: forall rtp' blocks' r' c f a.
(SimState p sym ext rtp' f a -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c)) ->
ExecCont p sym ext rtp' f a
continueWith f = withReaderT f (checkConsTerm verb)
withBackend ctx $ \bak ->
case stmt of
NewRefCell tpr x ->
do let halloc = simHandleAllocator ctx
v <- evalReg x
r <- liftIO $ freshRefCell halloc tpr
continueWith $
(stateTree . actFrame . gpGlobals %~ insertRef sym r v) .
(stateCrucibleFrame %~ extendFrame (ReferenceRepr tpr) (toMuxTree sym r) rest)
NewEmptyRefCell tpr ->
do let halloc = simHandleAllocator ctx
r <- liftIO $ freshRefCell halloc tpr
continueWith $
stateCrucibleFrame %~ extendFrame (ReferenceRepr tpr) (toMuxTree sym r) rest
ReadRefCell x ->
do RegEntry (ReferenceRepr tpr) rs <- evalReg' x
v <- liftIO $ readRef bak iTypes tpr rs globals
continueWith $
stateCrucibleFrame %~ extendFrame tpr v rest
WriteRefCell x y ->
do RegEntry (ReferenceRepr tpr) rs <- evalReg' x
newv <- justPartExpr sym <$> evalReg y
globals' <- liftIO $ alterRef sym iTypes tpr rs newv globals
continueWith $
(stateTree . actFrame . gpGlobals .~ globals') .
(stateCrucibleFrame . frameStmts .~ rest)
DropRefCell x ->
do RegEntry (ReferenceRepr tpr) rs <- evalReg' x
globals' <- liftIO $ alterRef sym iTypes tpr rs Unassigned globals
continueWith $
(stateTree . actFrame . gpGlobals .~ globals') .
(stateCrucibleFrame . frameStmts .~ rest)
ReadGlobal global_var -> do
case lookupGlobal global_var globals of
Nothing ->
do let msg = ReadBeforeWriteSimError $ "Attempt to read undefined global " ++ show global_var
liftIO $ addFailedAssertion bak msg
Just v ->
continueWith $
(stateCrucibleFrame %~ extendFrame (globalType global_var) v rest)
WriteGlobal global_var local_reg ->
do v <- evalReg local_reg
continueWith $
(stateTree . actFrame . gpGlobals %~ insertGlobal global_var v) .
(stateCrucibleFrame . frameStmts .~ rest)
FreshConstant bt mnm ->
do let nm = fromMaybe emptySymbol mnm
v <- liftIO $ freshConstant sym nm bt
continueWith $ stateCrucibleFrame %~ extendFrame (baseToType bt) v rest
FreshFloat fi mnm ->
do let nm = fromMaybe emptySymbol mnm
v <- liftIO $ freshFloatConstant sym nm fi
continueWith $ stateCrucibleFrame %~ extendFrame (FloatRepr fi) v rest
FreshNat mnm ->
do let nm = fromMaybe emptySymbol mnm
v <- liftIO $ freshNat sym nm
continueWith $ stateCrucibleFrame %~ extendFrame NatRepr v rest
SetReg tp e ->
do v <- evalExpr verb e
continueWith $ stateCrucibleFrame %~ extendFrame tp v rest
ExtendAssign estmt -> do
do let tp = appType estmt
estmt' <- traverseFC evalReg' estmt
ReaderT $ \s ->
do (v,s') <- liftIO $ extensionExec (extensionImpl ctx) estmt' s
runReaderT
(continueWith $ stateCrucibleFrame %~ extendFrame tp v rest)
s'
CallHandle ret_type fnExpr _types arg_exprs ->
do hndl <- evalReg fnExpr
args <- evalArgs arg_exprs
loc <- liftIO $ getCurrentProgramLoc sym
callFunction hndl args (ReturnToCrucible ret_type rest) loc
Print e ->
do msg <- evalReg e
let msg' = case asString msg of
Just (UnicodeLiteral txt) -> Text.unpack txt
_ -> show (printSymExpr msg)
liftIO $ do
let h = printHandle ctx
hPutStr h msg'
hFlush h
continueWith (stateCrucibleFrame . frameStmts .~ rest)
Assert c_expr msg_expr ->
do c <- evalReg c_expr
msg <- evalReg msg_expr
let err = case asString msg of
Just (UnicodeLiteral txt) -> AssertFailureSimError (Text.unpack txt) ""
_ -> AssertFailureSimError "Symbolic message" (show (printSymExpr msg))
liftIO $ assert bak c err
continueWith (stateCrucibleFrame . frameStmts .~ rest)
Assume c_expr msg_expr ->
do c <- evalReg c_expr
msg <- evalReg msg_expr
let msg' = case asString msg of
Just (UnicodeLiteral txt) -> Text.unpack txt
_ -> show (printSymExpr msg)
liftIO $
do loc <- getCurrentProgramLoc sym
addAssumption bak (GenericAssumption loc msg' c)
continueWith (stateCrucibleFrame . frameStmts .~ rest)
{-# INLINABLE stepTerm #-}
-- | Evaluation operation for evaluating a single block-terminator
-- statement of the Crucible evaluator.
--
-- This is allowed to throw user exceptions or 'SimError'.
stepTerm :: 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)
stepTerm _ (Jump tgt) =
jumpToBlock =<< evalJumpTarget tgt
stepTerm _ (Return arg) =
returnValue =<< evalReg' arg
stepTerm _ (Br c x y) =
do x_jump <- evalJumpTarget x
y_jump <- evalJumpTarget y
p <- evalReg c
conditionalBranch p x_jump y_jump
stepTerm _ (MaybeBranch tp e j n) =
do evalReg e >>= \case
Unassigned -> jumpToBlock =<< evalJumpTarget n
PE p v ->
do j_jump <- evalSwitchTarget j (RegEntry tp v)
n_jump <- evalJumpTarget n
conditionalBranch p j_jump n_jump
stepTerm _ (VariantElim ctx e cases) =
do vs <- evalReg e
jmps <- ctx & Ctx.traverseAndCollect (\i tp ->
case vs Ctx.! i of
VB Unassigned ->
return []
VB (PE p v) ->
do jmp <- evalSwitchTarget (cases Ctx.! i) (RegEntry tp v)
return [(p,jmp)])
variantCases jmps
-- When we make a tail call, we first try to unwind our calling context
-- and replace the currently-active frame with the frame of the new called
-- function. However, this is only successful if there are no pending
-- symbolic merges.
--
-- If there _are_ pending merges we instead treat the tail call as normal
-- call-then-return sequence, pushing a new call frame on the top of our
-- current context (rather than replacing it). The TailReturnToCrucible
-- return handler tells the simulator to immediately invoke another return
-- in the caller, which is still present on the stack in this scenario.
stepTerm _ (TailCall fnExpr _types arg_exprs) =
do cl <- evalReg fnExpr
args <- evalArgs arg_exprs
ctx <- view (stateTree.actContext)
sym <- view stateSymInterface
loc <- liftIO $ getCurrentProgramLoc sym
case unwindContext ctx of
Just vfv -> tailCallFunction cl args vfv loc
Nothing -> callFunction cl args TailReturnToCrucible loc
stepTerm _ (ErrorStmt msg) =
do msg' <- evalReg msg
simCtx <- view stateContext
withBackend simCtx $ \bak -> liftIO $
case asString msg' of
Just (UnicodeLiteral txt) ->
addFailedAssertion bak
$ GenericSimError $ Text.unpack txt
Nothing -> addFailedAssertion bak
$ GenericSimError $ show (printSymExpr msg')
-- | Checks whether the StmtSeq is a Cons or a Term,
-- to give callers another chance to jump into Crucible's control flow
checkConsTerm ::
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int {- ^ Current verbosity -} ->
ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
checkConsTerm verb =
do cf <- view stateCrucibleFrame
case cf^.frameStmts of
ConsStmt _ _ _ -> stepBasicBlock verb
TermStmt _ _ -> continue (RunBlockEnd (cf^.frameBlockID))
-- | Main evaluation operation for running a single step of
-- basic block evaluation.
--
-- This is allowed to throw user exceptions or 'SimError'.
stepBasicBlock ::
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int {- ^ Current verbosity -} ->
ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepBasicBlock verb =
do ctx <- view stateContext
let sym = ctx^.ctxSymInterface
let h = printHandle ctx
cf <- view stateCrucibleFrame
case cf^.frameStmts of
ConsStmt pl stmt rest ->
do liftIO $
do setCurrentProgramLoc sym pl
let sz = regMapSize (cf^.frameRegs)
when (verb >= 4) $ ppStmtAndLoc h (frameHandle cf) pl (ppStmt sz stmt)
stepStmt verb stmt rest
TermStmt pl termStmt -> do
do liftIO $
do setCurrentProgramLoc sym pl
when (verb >= 4) $ ppStmtAndLoc h (frameHandle cf) pl (pretty termStmt)
stepTerm verb termStmt
ppStmtAndLoc :: Handle -> SomeHandle -> ProgramLoc -> Doc ann -> IO ()
ppStmtAndLoc h sh pl stmt = do
hPrint h $
vcat [ viaShow sh <> pretty ':'
, indent 2 (stmt <+> pretty "%" <+> ppNoFileName (plSourceLoc pl)) ]
hFlush h
performStateRun ::
(IsSymInterface sym, IsSyntaxExtension ext) =>
RunningStateInfo blocks ctx ->
Int {- ^ Current verbosity -} ->
ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
performStateRun info verb = case info of
RunPostBranchMerge bid -> continue (RunBlockStart bid)
_ -> stepBasicBlock verb
----------------------------------------------------------------------
-- ExecState manipulations
-- | 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.
dispatchExecState ::
(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
dispatchExecState getVerb exst kresult k =
case exst of
ResultState res ->
kresult res
InitialState simctx globals ah ret cont ->
do st <- initSimState simctx globals ah ret
k cont st
AbortState rsn st ->
let (AH handler) = st^.abortHandler in
k (handler rsn) st
OverrideState ovr st ->
k (overrideHandler ovr) st
SymbolicBranchState p a_frame o_frame tgt st ->
k (performIntraFrameSplit p a_frame o_frame tgt) st
ControlTransferState resumption st ->
k (performControlTransfer resumption) st
BranchMergeState tgt st ->
k (performIntraFrameMerge tgt) st
UnwindCallState vfv ar st ->
k (resumeValueFromValueAbort vfv ar) st
CallState retHandler frm st ->
k (performFunctionCall retHandler frm) st
TailCallState vfv frm st ->
k (performTailCall vfv frm) st
ReturnState fnm vfv ret st ->
k (performReturn fnm vfv ret) st
RunningState info st ->
do v <- getVerb
k (performStateRun info v) st
{-# INLINE dispatchExecState #-}
-- | 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.
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)
advanceCrucibleState m st =
Ex.catches (runReaderT m st)
[ Ex.Handler $ \(e::AbortExecReason) ->
runAbortHandler e st
, Ex.Handler $ \(e::Ex.IOException) ->
if Ex.isUserError e then
runGenericErrorHandler (Ex.ioeGetErrorString e) st
else
Ex.throwIO e
]
-- | Run a single step of the Crucible symbolic simulator.
singleStepCrucible ::
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int {- ^ Current verbosity -} ->
ExecState p sym ext rtp ->
IO (ExecState p sym ext rtp)
singleStepCrucible verb exst =
dispatchExecState
(return verb)
exst
(return . ResultState)
advanceCrucibleState
-- | This datatype indicates the possible results that an execution feature
-- can have.
data ExecutionFeatureResult p sym ext rtp where
-- | This execution feature result indicates that no state changes were
-- made.
ExecutionFeatureNoChange :: 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.
ExecutionFeatureModifiedState ::
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.
ExecutionFeatureNewState ::
ExecState p sym ext rtp -> ExecutionFeatureResult 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.
newtype ExecutionFeature p sym ext rtp =
ExecutionFeature
{ runExecutionFeature :: ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)
}
-- | 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.
newtype GenericExecutionFeature sym =
GenericExecutionFeature
{ runGenericExecutionFeature :: forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)
}
genericToExecutionFeature ::
(IsSymInterface sym, IsSyntaxExtension ext) =>
GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp
genericToExecutionFeature (GenericExecutionFeature f) = ExecutionFeature f
-- | 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.
executeCrucible :: 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)
executeCrucible execFeatures exst0 =
do let cfg = getConfiguration . view ctxSymInterface . execStateContext $ exst0
verbOpt <- getOptionSetting verbosity cfg
let loop exst =
dispatchExecState
(fromInteger <$> getOpt verbOpt)
exst
return
(\m st -> knext =<< advanceCrucibleState m st)
applyExecutionFeature feat m = \exst ->
runExecutionFeature feat exst >>= \case
ExecutionFeatureNoChange -> m exst
ExecutionFeatureModifiedState exst' -> m exst'
ExecutionFeatureNewState exst' -> knext exst'
knext = foldr applyExecutionFeature loop execFeatures
knext exst0
-- | This feature will terminate the execution of a crucible simulator
-- with a @TimeoutResult@ after a given interval of wall-clock time
-- has elapsed.
timeoutFeature ::
NominalDiffTime ->
IO (GenericExecutionFeature sym)
timeoutFeature timeout =
do startTime <- getCurrentTime
let deadline = addUTCTime timeout startTime
return $ GenericExecutionFeature $ \exst ->
case exst of
ResultState _ -> return ExecutionFeatureNoChange
_ ->
do now <- getCurrentTime
if deadline >= now then
return ExecutionFeatureNoChange
else
return (ExecutionFeatureNewState (ResultState (TimeoutResult exst)))