crucible-0.9: src/Lang/Crucible/Simulator/ExecutionTree.hs
-----------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.Simulator.ExecutionTree
-- Description : Data structure the execution state of the simulator
-- Copyright : (c) Galois, Inc 2014-2018
-- License : BSD3
-- Maintainer : Joe Hendrix <jhendrix@galois.com>
-- Stability : provisional
--
-- Execution trees record the state of the simulator as it explores
-- execution paths through a program. This module defines the
-- collection of datatypes that record the state of a running simulator
-- and basic lenses and accessors for these types. See
-- "Lang.Crucible.Simulator.Operations" for the definitions of operations
-- that manipulate these datastructures to drive them through the simulator
-- state machine.
------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-}
module Lang.Crucible.Simulator.ExecutionTree
( -- * GlobalPair
GlobalPair(..)
, gpValue
, gpGlobals
-- * TopFrame
, TopFrame
, crucibleTopFrame
, overrideTopFrame
-- * CrucibleBranchTarget
, CrucibleBranchTarget(..)
, ppBranchTarget
-- * AbortedResult
, AbortedResult(..)
, SomeFrame(..)
, filterCrucibleFrames
, arFrames
, ppExceptionContext
-- * Partial result
, PartialResult(..)
, PartialResultFrame
, partialValue
-- * Execution states
, ExecResult(..)
, ExecState(..)
, ExecCont
, RunningStateInfo(..)
, ResolvedCall(..)
, resolvedCallHandle
, execResultContext
, setExecResultContext
, execStateContext
, setExecStateContext
, execStateSimState
, execResultGlobals
, execStateGlobals
-- * Simulator context trees
-- ** Main context data structures
, ValueFromValue(..)
, ValueFromFrame(..)
, PendingPartialMerges(..)
-- ** Paused Frames
, ResolvedJump(..)
, ControlResumption(..)
, PausedFrame(..)
-- ** Sibling paths
, VFFOtherPath(..)
, FrameRetType
-- ** ReturnHandler
, ReturnHandler(..)
-- * ActiveTree
, ActiveTree(..)
, singletonTree
, activeFrames
, actContext
, actFrame
-- * Simulator context
-- ** Function bindings
, Override(..)
, FnState(..)
, FunctionBindings(..)
-- ** Extensions
, ExtensionImpl(..)
, EvalStmtFunc
, emptyExtensionImpl
-- ** SimContext record
, IsSymInterfaceProof
, SimContext(..)
, Metric(..)
, initSimContext
, withBackend
, ctxSymInterface
, functionBindings
, cruciblePersonality
, profilingMetrics
-- * SimState
, SimState(..)
, SomeSimState(..)
, initSimState
, stateLocation
, AbortHandler(..)
, CrucibleState
-- ** Lenses and accessors
, stateTree
, abortHandler
, stateContext
, stateCrucibleFrame
, stateSymInterface
, stateSolverProof
, stateIntrinsicTypes
, stateOverrideFrame
, stateGlobals
, stateConfiguration
) where
import Control.Lens
import Control.Monad.Reader
import Data.Kind
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import Data.Text (Text)
import System.Exit (ExitCode)
import System.IO
import qualified Prettyprinter as PP
import What4.Config (Config)
import What4.Interface (Pred, getConfiguration)
import What4.FunctionName (FunctionName, startFunctionName)
import What4.ProgramLoc (ProgramLoc, plSourceLoc)
import Lang.Crucible.Backend
( IsSymInterface, IsSymBackend(..), HasSymInterface(..)
, AbortExecReason, SomeBackend(..), FrameIdentifier, Assumptions
)
import Lang.Crucible.CFG.Core (BlockID, CFG, CFGPostdom, StmtSeq)
import Lang.Crucible.CFG.Extension (StmtExtension, ExprExtension)
import Lang.Crucible.FunctionHandle (FnHandleMap, HandleAllocator, mkHandle')
import Lang.Crucible.Simulator.CallFrame
import Lang.Crucible.Simulator.Evaluation (EvalAppFunc)
import Lang.Crucible.Simulator.GlobalState (SymGlobalState)
import Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes)
import Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry)
import Lang.Crucible.Types
------------------------------------------------------------------------
-- GlobalPair
-- | A value of some type @v@ together with a global state.
--
-- Type parameters:
--
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @v@: type of the value
type GlobalPair :: Type -> Type -> Type
data GlobalPair sym v =
GlobalPair
{ _gpValue :: !v
, _gpGlobals :: !(SymGlobalState sym)
}
-- | Access the value stored in the global pair.
gpValue :: Lens (GlobalPair sym u) (GlobalPair sym v) u v
gpValue = lens _gpValue (\s v -> s { _gpValue = v })
-- | Access the globals stored in the global pair.
gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym)
gpGlobals = lens _gpGlobals (\s v -> s { _gpGlobals = v })
------------------------------------------------------------------------
-- TopFrame
-- | The currently-executing frame plus the global state associated with it.
--
-- Type parameters:
--
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
-- - @args@: arguments to this frame (see 'SimFrame')
type TopFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type
type TopFrame sym ext f args = GlobalPair sym (SimFrame sym ext f args)
-- | Access the Crucible call frame inside a 'TopFrame'.
crucibleTopFrame ::
Lens (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
(TopFrame sym ext (CrucibleLang blocks r) ('Just args'))
(CallFrame sym ext blocks r args)
(CallFrame sym ext blocks r args')
crucibleTopFrame = gpValue . crucibleSimFrame
{-# INLINE crucibleTopFrame #-}
overrideTopFrame ::
Lens (TopFrame sym ext (OverrideLang r) ('Just args))
(TopFrame sym ext (OverrideLang r') ('Just args'))
(OverrideFrame sym r args)
(OverrideFrame sym r' args')
overrideTopFrame = gpValue . overrideSimFrame
{-# INLINE overrideTopFrame #-}
------------------------------------------------------------------------
-- AbortedResult
-- | An execution path that was prematurely aborted. Note, an abort
-- does not necessarily indicate an error condition. An execution
-- path might abort because it became infeasible (inconsistent path
-- conditions), because the program called an exit primitive, or
-- because of a true error condition (e.g., a failed assertion).
--
-- Type parameters:
--
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type AbortedResult :: Type -> Type -> Type
data AbortedResult sym ext where
-- | A single aborted execution with the execution state at time of the abort and the reason.
AbortedExec ::
!AbortExecReason ->
!(GlobalPair sym (SimFrame sym ext l args)) ->
AbortedResult sym ext
-- | An aborted execution that was ended by a call to @exit@.
AbortedExit ::
!ExitCode ->
!(GlobalPair sym (SimFrame sym ext l args)) ->
AbortedResult sym ext
-- | Two separate threads of execution aborted after a symbolic branch,
-- possibly for different reasons.
AbortedBranch ::
!ProgramLoc {- The source location of the branching control flow -} ->
!(Pred sym) {- The symbolic condition -} ->
!(AbortedResult sym ext) {- The abort that occurred along the 'true' branch -} ->
!(AbortedResult sym ext) {- The abort that occurred along the 'false' branch -} ->
AbortedResult sym ext
------------------------------------------------------------------------
-- SomeFrame
-- | This represents an execution frame where its frame type
-- and arguments have been hidden.
--
-- The type parameter @f@ is usually 'SimFrame'.
type SomeFrame :: forall fk argk. (fk -> argk -> Type) -> Type
data SomeFrame f = forall l a . SomeFrame !(f l a)
-- | Return the program locations of all the Crucible frames.
filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc
filterCrucibleFrames (SomeFrame (MF f)) = Just (frameProgramLoc f)
filterCrucibleFrames _ = Nothing
-- | Iterate over frames in the result.
arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext))
arFrames h (AbortedExec e p) =
(\(SomeFrame f') -> AbortedExec e (p & gpValue .~ f'))
<$> h (SomeFrame (p^.gpValue))
arFrames h (AbortedExit ec p) =
(\(SomeFrame f') -> AbortedExit ec (p & gpValue .~ f'))
<$> h (SomeFrame (p^.gpValue))
arFrames h (AbortedBranch predicate loc r s) =
AbortedBranch predicate loc <$> arFrames h r
<*> arFrames h s
-- | Print an exception context
ppExceptionContext :: [SomeFrame (SimFrame sym ext)] -> PP.Doc ann
ppExceptionContext [] = mempty
ppExceptionContext frames = PP.vcat (map pp (init frames))
where
pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann
pp (SomeFrame (OF f)) =
PP.pretty "When calling" PP.<+> PP.viaShow (f^.override)
pp (SomeFrame (MF f)) =
PP.pretty "In" PP.<+> PP.viaShow (frameHandle f) PP.<+>
PP.pretty "at" PP.<+> PP.pretty (plSourceLoc (frameProgramLoc f))
pp (SomeFrame (RF nm _v)) =
PP.pretty "While returning value from" PP.<+> PP.viaShow nm
------------------------------------------------------------------------
-- PartialResult
-- | A 'PartialResult' represents the result of a computation that
-- might be only partially defined. If the result is a 'TotalResult',
-- the the result is fully defined; however if it is a
-- 'PartialResult', then some of the computation paths that led to
-- this result aborted for some reason, and the resulting value is
-- only defined if the associated condition is true.
--
-- Type parameters:
--
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @v@: Type of the result of the computation
type PartialResult :: Type -> Type -> Type -> Type
data PartialResult sym ext v
{- | A 'TotalRes' indicates that the the global pair is always defined. -}
= TotalRes !(GlobalPair sym v)
{- | 'PartialRes' indicates that the global pair may be undefined
under some circumstances. The predicate specifies under what
conditions the 'GlobalPair' is defined.
The 'AbortedResult' describes the circumstances under which
the result would be partial.
-}
| PartialRes !ProgramLoc -- location of symbolic branch point
!(Pred sym) -- if true, global pair is defined
!(GlobalPair sym v) -- the value
!(AbortedResult sym ext) -- failure cases (when pred. is false)
-- | Access the value stored in the partial result.
partialValue ::
Lens (PartialResult sym ext u)
(PartialResult sym ext v)
(GlobalPair sym u)
(GlobalPair sym v)
partialValue f (TotalRes x) = TotalRes <$> f x
partialValue f (PartialRes loc p x r) = (\y -> PartialRes loc p y r) <$> f x
{-# INLINE partialValue #-}
-- | The result of resolving a function call.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @ret@: 'CrucibleType' of the return value
type ResolvedCall :: Type -> Type -> Type -> CrucibleType -> Type
data ResolvedCall p sym ext ret where
-- | A resolved function call to an override.
OverrideCall ::
!(Override p sym ext args ret) ->
!(OverrideFrame sym ret args) ->
ResolvedCall p sym ext ret
-- | A resolved function call to a Crucible function.
CrucibleCall ::
!(BlockID blocks args) ->
!(CallFrame sym ext blocks ret args) ->
ResolvedCall p sym ext ret
resolvedCallHandle :: ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle (OverrideCall _ frm) = frm ^. overrideHandle
resolvedCallHandle (CrucibleCall _ frm) = frameHandle frm
------------------------------------------------------------------------
-- ExecResult
-- | Executions that have completed either due to (partial or total)
-- successful completion or by some abort condition.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
type ExecResult :: Type -> Type -> Type -> Type -> Type
data ExecResult p sym ext rtp
= -- | At least one execution path resulted in some return result.
FinishedResult !(SimContext p sym ext) !(PartialResult sym ext rtp)
-- | All execution paths resulted in an abort condition, and there is
-- no result to return.
| AbortedResult !(SimContext p sym ext) !(AbortedResult sym ext)
-- | An execution stopped somewhere in the middle of a run because
-- a timeout condition occurred.
| TimeoutResult !(ExecState p sym ext rtp)
execResultContext :: ExecResult p sym ext r -> SimContext p sym ext
execResultContext (FinishedResult ctx _) = ctx
execResultContext (AbortedResult ctx _) = ctx
execResultContext (TimeoutResult exst) = execStateContext exst
setExecResultContext ::
SimContext p sym ext ->
ExecResult p sym ext r ->
ExecResult p sym ext r
setExecResultContext ctx =
\case
FinishedResult _ x -> FinishedResult ctx x
AbortedResult _ x -> AbortedResult ctx x
TimeoutResult execState -> TimeoutResult (setExecStateContext ctx execState)
execStateContext :: ExecState p sym ext r -> SimContext p sym ext
execStateContext = \case
ResultState res -> execResultContext res
AbortState _ st -> st^.stateContext
UnwindCallState _ _ st -> st^.stateContext
CallState _ _ st -> st^.stateContext
TailCallState _ _ st -> st^.stateContext
ReturnState _ _ _ st -> st^.stateContext
ControlTransferState _ st -> st^.stateContext
RunningState _ st -> st^.stateContext
SymbolicBranchState _ _ _ _ st -> st^.stateContext
OverrideState _ st -> st^.stateContext
BranchMergeState _ st -> st^.stateContext
InitialState stctx _ _ _ _ -> stctx
setExecStateContext ::
SimContext p sym ext ->
ExecState p sym ext r ->
ExecState p sym ext r
setExecStateContext ctx = \case
ResultState res -> ResultState (setExecResultContext ctx res)
AbortState x st -> AbortState x (st & stateContext .~ ctx)
UnwindCallState x y st -> UnwindCallState x y (st & stateContext .~ ctx)
CallState x y st -> CallState x y (st & stateContext .~ ctx)
TailCallState x y st -> TailCallState x y (st & stateContext .~ ctx)
ReturnState x y z st -> ReturnState x y z (st & stateContext .~ ctx)
ControlTransferState x st -> ControlTransferState x (st & stateContext .~ ctx)
RunningState x st -> RunningState x (st & stateContext .~ ctx)
SymbolicBranchState u v x y st -> SymbolicBranchState u v x y (st & stateContext .~ ctx)
OverrideState x st -> OverrideState x (st & stateContext .~ ctx)
BranchMergeState x st -> BranchMergeState x (st & stateContext .~ ctx)
InitialState _ u v x y -> InitialState ctx u v x y
execStateSimState :: ExecState p sym ext r
-> Maybe (SomeSimState p sym ext r)
execStateSimState = \case
ResultState _ -> Nothing
AbortState _ st -> Just (SomeSimState st)
UnwindCallState _ _ st -> Just (SomeSimState st)
CallState _ _ st -> Just (SomeSimState st)
TailCallState _ _ st -> Just (SomeSimState st)
ReturnState _ _ _ st -> Just (SomeSimState st)
ControlTransferState _ st -> Just (SomeSimState st)
RunningState _ st -> Just (SomeSimState st)
SymbolicBranchState _ _ _ _ st -> Just (SomeSimState st)
OverrideState _ st -> Just (SomeSimState st)
BranchMergeState _ st -> Just (SomeSimState st)
InitialState _ _ _ _ _ -> Nothing
abortedGlobals ::
Monad f =>
-- | How to handle 'AbortedBranch'.
--
-- Common options include concretizing the 'Pred' or returning a partial
-- result (e.g., 'Nothing').
(ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) ->
AbortedResult sym ext ->
f (SymGlobalState sym)
abortedGlobals handleBranch =
\case
AbortedExec _ gp -> pure (gp ^. gpGlobals)
AbortedExit _ gp -> pure (gp ^. gpGlobals)
AbortedBranch loc p rl rr -> do
l <- abortedGlobals handleBranch rl
r <- abortedGlobals handleBranch rr
handleBranch loc p l r
-- | Extract the 'SymGlobalState' from an 'ExecResult'.
execResultGlobals ::
Monad f =>
-- | How to handle 'AbortedBranch'.
--
-- Common options include concretizing the 'Pred' or returning a partial
-- result (e.g., 'Nothing').
(SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) ->
ExecResult p sym ext rtp ->
f (SymGlobalState sym)
execResultGlobals handleBranch =
\case
FinishedResult _ctx partial -> pure (partial ^. partialValue . gpGlobals)
TimeoutResult st -> execStateGlobals handleBranch st
AbortedResult simCtx aborted ->
abortedGlobals (handleBranch simCtx) aborted
-- | Extract the 'SymGlobalState' from an 'ExecState'.
execStateGlobals ::
Monad f =>
-- | How to handle 'AbortedBranch'.
--
-- Common options include concretizing the 'Pred' or returning a partial
-- result (e.g., 'Nothing').
(SimContext p sym ext -> ProgramLoc -> Pred sym -> SymGlobalState sym -> SymGlobalState sym -> f (SymGlobalState sym)) ->
ExecState p sym ext rtp ->
f (SymGlobalState sym)
execStateGlobals handleBranch =
\case
AbortState _ st -> pure (st ^. stateGlobals)
BranchMergeState _ st -> pure (st ^. stateGlobals)
CallState _ _ st -> pure (st ^. stateGlobals)
ControlTransferState _ st -> pure (st ^. stateGlobals)
InitialState _ globState _ _ _ -> pure globState
OverrideState _ st -> pure (st ^. stateGlobals)
ResultState r -> execResultGlobals handleBranch r
ReturnState _ _ _ st -> pure (st ^. stateGlobals)
RunningState _ st -> pure (st ^. stateGlobals)
SymbolicBranchState _ _ _ _ st -> pure (st ^. stateGlobals)
TailCallState _ _ st -> pure (st ^. stateGlobals)
UnwindCallState _ _ st -> pure (st ^. stateGlobals)
-----------------------------------------------------------------------
-- ExecState
-- | An 'ExecState' represents an intermediate state of executing a
-- Crucible program. The Crucible simulator executes by transitioning
-- between these different states until it results in a 'ResultState',
-- indicating the program has completed.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
type ExecState :: Type -> Type -> Type -> Type -> Type
data ExecState p sym ext rtp
{- | The 'ResultState' is used to indicate that the program has completed. -}
= ResultState
!(ExecResult p sym ext rtp)
{- | An abort state indicates that the included 'SimState' encountered
an abort event while executing its next step. The state needs to
be unwound to its nearest enclosing branch point and resumed. -}
| forall f a.
AbortState
!AbortExecReason
{- Description of what abort condition occurred -}
!(SimState p sym ext rtp f a)
{- State of the simulator prior to causing the abort condition -}
{- | An unwind call state occurs when we are about to leave the context of a
function call because of an abort. The included @ValueFromValue@ is the
context of the call site we are about to unwind into, and the @AbortedResult@
indicates the reason we are aborting.
-}
| forall f a r.
UnwindCallState
!(ValueFromValue p sym ext rtp r) {- Caller's context -}
!(AbortedResult sym ext) {- Abort causing the stack unwind -}
!(SimState p sym ext rtp f a)
{- | A call state is entered when we are about to make a function call to
the included call frame, which has already resolved the implementation
and arguments to the function.
-}
| forall f a ret.
CallState
!(ReturnHandler ret p sym ext rtp f a)
!(ResolvedCall p sym ext ret)
!(SimState p sym ext rtp f a)
{- | A tail-call state is entered when we are about to make a function call to
the included call frame, and this is the last action we need to take in the
current caller. Note, we can only enter a tail-call state if there are no
pending merge points in the caller. This means that sometimes calls
that appear to be in tail-call position may nonetheless have to be treated
as ordinary calls.
-}
| forall f a ret.
TailCallState
!(ValueFromValue p sym ext rtp ret) {- Calling context to return to -}
!(ResolvedCall p sym ext ret) {- Function to call -}
!(SimState p sym ext rtp f a)
{- | A return state is entered after the final return value of a function
is computed, and just before we resolve injecting the return value
back into the caller's context.
-}
| forall f a ret.
ReturnState
!FunctionName {- Name of the function we are returning from -}
!(ValueFromValue p sym ext rtp ret) {- Caller's context -}
!(RegEntry sym ret) {- Return value -}
!(SimState p sym ext rtp f a)
{- | A running state indicates the included 'SimState' is ready to enter
and execute a Crucible basic block, or to resume a basic block
from a call site. -}
| forall blocks r args.
RunningState
!(RunningStateInfo blocks args)
!(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
{- | A symbolic branch state indicates that the execution needs to
branch on a non-trivial symbolic condition. The included @Pred@
is the condition to branch on. The first @PausedFrame@ is
the path that corresponds to the @Pred@ being true, and the second
is the false branch.
-}
| forall f args postdom_args.
SymbolicBranchState
!(Pred sym) {- predicate to branch on -}
!(PausedFrame p sym ext rtp f) {- true path-}
!(PausedFrame p sym ext rtp f) {- false path -}
!(CrucibleBranchTarget f postdom_args) {- merge point -}
!(SimState p sym ext rtp f ('Just args))
{- | A control transfer state is entered just prior to invoking a
control resumption. Control resumptions are responsible
for transitioning from the end of one basic block to another,
although there are also some intermediate states related to
resolving switch statements.
-}
| forall f a.
ControlTransferState
!(ControlResumption p sym ext rtp f)
!(SimState p sym ext rtp f ('Just a))
{- | An override state indicates the included 'SimState' is prepared to
execute a code override. -}
| forall args ret.
OverrideState
!(Override p sym ext args ret)
{- The override code to execute -}
!(SimState p sym ext rtp (OverrideLang ret) ('Just args))
{- State of the simulator prior to activating the override -}
{- | A branch merge state occurs when the included 'SimState' is
in the process of transferring control to the included 'CrucibleBranchTarget'.
We enter a BranchMergeState every time we need to _check_ if there is a
pending branch, even if no branch is pending. During this process, paths may
have to be merged. If several branches must merge at the same control point,
this state may be entered several times in succession before returning
to a 'RunningState'. -}
| forall f args.
BranchMergeState
!(CrucibleBranchTarget f args)
{- Target of the control-flow transfer -}
!(SimState p sym ext rtp f args)
{- State of the simulator before merging pending branches -}
{- | An initial state indicates the state of a simulator just before execution begins.
It specifies all the initial data necessary to begin simulating. The given
@ExecCont@ will be executed in a fresh @SimState@ representing the default starting
call frame.
-}
| forall ret. rtp ~ RegEntry sym ret =>
InitialState
!(SimContext p sym ext)
{- initial 'SimContext' state -}
!(SymGlobalState sym)
{- state of Crucible global variables -}
!(AbortHandler p sym ext (RegEntry sym ret))
{- initial abort handler -}
!(TypeRepr ret)
{- return type repr -}
!(ExecCont p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
{- Entry continuation -}
-- | An action which will construct an 'ExecState' given a current
-- 'SimState'. Such continuations correspond to a single transition
-- of the simulator transition system.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
-- - @args@: arguments to the current frame (see 'SimFrame')
type ExecCont :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type
type ExecCont p sym ext rtp f args =
ReaderT (SimState p sym ext rtp f args) IO (ExecState p sym ext rtp)
-- | Some additional information attached to a @RunningState@
-- that indicates how we got to this running state.
--
-- Type parameters:
--
-- - @blocks@: types of variables in scope from previous blocks
-- - @args@: arguments to this block
type RunningStateInfo :: Ctx (Ctx CrucibleType) -> Ctx CrucibleType -> Type
data RunningStateInfo blocks args
-- | This indicates that we are now in a @RunningState@ because
-- we transferred execution to the start of a basic block.
= RunBlockStart !(BlockID blocks args)
-- | This indicates that we are in a @RunningState@ because we
-- reached the terminal statement of a basic block.
| RunBlockEnd !(Some (BlockID blocks))
-- | This indicates that we are in a @RunningState@ because we
-- returned from calling the named function.
| RunReturnFrom !FunctionName
-- | This indicates that we are now in a @RunningState@ because
-- we finished branch merging prior to the start of a block.
| RunPostBranchMerge !(BlockID blocks args)
-- | A 'ResolvedJump' is a block label together with a collection of
-- actual arguments that are expected by that block. These data
-- are sufficient to actually transfer control to the named label.
--
-- Type parameters:
--
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @blocks@: types of variables in scope from previous blocks
type ResolvedJump :: Type -> Ctx (Ctx CrucibleType) -> Type
data ResolvedJump sym blocks
= forall args.
ResolvedJump
!(BlockID blocks args)
!(RegMap sym args)
-- | When a path of execution is paused by the symbolic simulator
-- (while it first explores other paths), a 'ControlResumption'
-- indicates what actions must later be taken in order to resume
-- execution of that path.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
type ControlResumption :: Type -> Type -> Type -> Type -> Type -> Type
data ControlResumption p sym ext rtp f where
{- | When resuming a paused frame with a @ContinueResumption@,
no special work needs to be done, simply begin executing
statements of the basic block. -}
ContinueResumption ::
!(ResolvedJump sym blocks) ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
{- | When resuming with a @CheckMergeResumption@, we must check
for the presence of pending merge points before resuming. -}
CheckMergeResumption ::
!(ResolvedJump sym blocks) ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
{- | When resuming a paused frame with a @SwitchResumption@, we must
continue branching to possible alternatives in a variant elimination
statement. In other words, we are still in the process of
transferring control away from the current basic block (which is now
at a final @VariantElim@ terminal statement). -}
SwitchResumption ::
![(Pred sym, ResolvedJump sym blocks)] {- remaining branches -} ->
ControlResumption p sym ext rtp (CrucibleLang blocks r)
{- | When resuming a paused frame with an @OverrideResumption@, we
simply return control to the included thunk, which represents
the remaining computation for the override.
-}
OverrideResumption ::
ExecCont p sym ext rtp (OverrideLang r) ('Just args) ->
!(RegMap sym args) ->
ControlResumption p sym ext rtp (OverrideLang r)
------------------------------------------------------------------------
-- Paused Frame
-- | A 'PausedFrame' represents a path of execution that has been postponed
-- while other paths are explored. It consists of a (potentially partial)
-- 'SimFrame' together with some information about how to resume execution
-- of that frame.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
type PausedFrame :: Type -> Type -> Type -> Type -> Type -> Type
data PausedFrame p sym ext rtp f
= forall old_args.
PausedFrame
{ pausedFrame :: !(PartialResultFrame sym ext f ('Just old_args))
, resume :: !(ControlResumption p sym ext rtp f)
, pausedLoc :: !(Maybe ProgramLoc)
}
-- | This describes the state of the sibling path at a symbolic branch point.
-- A symbolic branch point starts with the sibling in the 'VFFActivePath'
-- state, which indicates that the sibling path still needs to be executed.
-- After the first path to be explored has reached the merge point, the
-- places of the two paths are exchanged, and the completed path is
-- stored in the 'VFFCompletePath' state until the second path also
-- reaches its merge point. The two paths will then be merged,
-- and execution will continue beyond the merge point.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
-- - @args@: arguments to this frame (see 'SimFrame')
type VFFOtherPath :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type
data VFFOtherPath p sym ext ret f args
{- | This corresponds the a path that still needs to be analyzed. -}
= VFFActivePath
!(PausedFrame p sym ext ret f)
{- Other branch we still need to run -}
{- | This is a completed execution path. -}
| VFFCompletePath
!(Assumptions sym)
{- Assumptions that we collected while analyzing the branch -}
!(PartialResultFrame sym ext f args)
{- Result of running the other branch -}
{- | This type contains information about the current state of the exploration
of the branching structure of a program. The 'ValueFromFrame' states correspond
to the structure of symbolic branching that occurs within a single function call.
Type parameters:
- @p@: see 'cruciblePersonality'
- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
- @ext@: language extension, see "Lang.Crucible.CFG.Extension"
- @ret@: global return type of the entire execution
- @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
-}
type ValueFromFrame :: Type -> Type -> Type -> Type -> Type -> Type
data ValueFromFrame p sym ext ret f
{- | We are working on a branch; this could be the first or the second
of both branches (see the 'VFFOtherPath' field). -}
= forall args.
VFFBranch
!(ValueFromFrame p sym ext ret f)
{- The outer context---what to do once we are done with both branches -}
!FrameIdentifier
{- This is the frame identifier in the solver before this branch,
so that when we are done we can pop-off the assumptions we accumulated
while processing the branch -}
!ProgramLoc
{- Program location of the branch point -}
!(Pred sym)
{- Assertion of currently-active branch -}
!(VFFOtherPath p sym ext ret f args)
{- Info about the state of the other branch.
If the other branch is "VFFActivePath", then we still
need to process it; if it is "VFFCompletePath", then
it is finished, and so once we are done then we go back to the
outer context. -}
!(CrucibleBranchTarget f args)
{- Identifies the postdominator where the two branches merge back together -}
{- | We are on a branch where the other branch was aborted before getting
to the merge point. -}
| VFFPartial
!(ValueFromFrame p sym ext ret f)
{- The other context--what to do once we are done with this branch -}
!ProgramLoc
{- Program location of the branch point -}
!(Pred sym)
{- Assertion of currently-active branch -}
!(AbortedResult sym ext)
{- What happened on the other branch -}
!PendingPartialMerges
{- should we abort the (outer) sibling branch when it merges with us? -}
{- | When we are finished with this branch we should return from the function. -}
| VFFEnd
!(ValueFromValue p sym ext ret (FrameRetType f))
-- | Data about whether the surrounding context is expecting a merge to
-- occur or not. If the context sill expects a merge, we need to
-- take some actions to indicate that the merge will not occur;
-- otherwise there is no special work to be done.
type PendingPartialMerges :: Type
data PendingPartialMerges =
{- | Don't indicate an abort condition in the context -}
NoNeedToAbort
{- | Indicate an abort condition in the context when we
get there again. -}
| NeedsToBeAborted
{- | This type contains information about the current state of the exploration
of the branching structure of a program. The 'ValueFromValue' states correspond
to stack call frames in a more traditional simulator environment.
- @p@: see 'cruciblePersonality'
- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
- @ext@: language extension, see "Lang.Crucible.CFG.Extension"
- @ret@: global return type of the entire execution
- @top_return@: return type of the top-most call on the stack.
-}
type ValueFromValue :: Type -> Type -> Type -> Type -> CrucibleType -> Type
data ValueFromValue p sym ext ret top_return
{- | 'VFVCall' denotes a call site in the outer context, and represents
the point to which a function higher on the stack will
eventually return. The three arguments are:
* The context in which the call happened.
* The frame of the caller
* How to modify the current sim frame and resume execution
when we obtain the return value
-}
= forall args caller.
VFVCall
!(ValueFromFrame p sym ext ret caller)
-- The context in which the call happened.
!(SimFrame sym ext caller args)
-- The frame of the caller.
!(ReturnHandler top_return p sym ext ret caller args)
-- How to modify the current sim frame and resume execution
-- when we obtain the return value
{- | A partial value.
The predicate indicates what needs to hold to avoid the partiality.
The "AbortedResult" describes what could go wrong if the predicate
does not hold. -}
| VFVPartial
!(ValueFromValue p sym ext ret top_return)
!ProgramLoc
!(Pred sym)
!(AbortedResult sym ext)
{- | The top return value, indicating the program termination point. -}
| (ret ~ RegEntry sym top_return) => VFVEnd
instance PP.Pretty (ValueFromValue p ext sym root rp) where
pretty = ppValueFromValue
instance PP.Pretty (ValueFromFrame p ext sym ret f) where
pretty = ppValueFromFrame
instance PP.Pretty (VFFOtherPath ctx sym ext r f a) where
pretty (VFFActivePath _) = PP.pretty "active_path"
pretty (VFFCompletePath _ _) = PP.pretty "complete_path"
ppValueFromFrame :: ValueFromFrame p sym ext ret f -> PP.Doc ann
ppValueFromFrame vff =
case vff of
VFFBranch ctx _ _ _ other mp ->
PP.vcat
[ PP.pretty "intra_branch"
, PP.indent 2 (PP.pretty other)
, PP.indent 2 (PP.pretty (ppBranchTarget mp))
, PP.pretty ctx
]
VFFPartial ctx _ _ _ _ ->
PP.vcat
[ PP.pretty "intra_partial"
, PP.pretty ctx
]
VFFEnd ctx ->
PP.pretty ctx
ppValueFromValue :: ValueFromValue p sym ext root tp -> PP.Doc ann
ppValueFromValue vfv =
case vfv of
VFVCall ctx _ _ ->
PP.vcat
[ PP.pretty "call"
, PP.pretty ctx
]
VFVPartial ctx _ _ _ ->
PP.vcat
[ PP.pretty "inter_partial"
, PP.pretty ctx
]
VFVEnd -> PP.pretty "root"
-----------------------------------------------------------------------
-- parentFrames
-- | Return parents frames in reverse order.
parentFrames :: ValueFromFrame p sym ext r a -> [SomeFrame (SimFrame sym ext)]
parentFrames c0 =
case c0 of
VFFBranch c _ _ _ _ _ -> parentFrames c
VFFPartial c _ _ _ _ -> parentFrames c
VFFEnd vfv -> vfvParents vfv
-- | Return parents frames in reverse order.
vfvParents :: ValueFromValue p sym ext r a -> [SomeFrame (SimFrame sym ext)]
vfvParents c0 =
case c0 of
VFVCall c f _ -> SomeFrame f : parentFrames c
VFVPartial c _ _ _ -> vfvParents c
VFVEnd -> []
------------------------------------------------------------------------
-- ReturnHandler
{- | A 'ReturnHandler' indicates what actions to take to resume
executing in a caller's context once a function call has completed and
the return value is available.
Type parameters:
- @ret@: the type of the return value that is expected
- @p@: see 'cruciblePersonality'
- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
- @ext@: language extension, see "Lang.Crucible.CFG.Extension"
- @root@: global return type of the entire computation
- @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang')
- @args@: types of the local variables in scope prior to the call (see 'SimFrame')
-}
type ReturnHandler :: CrucibleType -> Type -> Type -> Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type
data ReturnHandler ret p sym ext root f args where
{- | The 'ReturnToOverride' constructor indicates that the calling
context is primitive code written directly in Haskell.
-}
ReturnToOverride ::
(RegEntry sym ret -> SimState p sym ext root (OverrideLang r) ('Just args) -> IO (ExecState p sym ext root))
{- Remaining override code to run when the return value becomes available -} ->
ReturnHandler ret p sym ext root (OverrideLang r) ('Just args)
{- | The 'ReturnToCrucible' constructor indicates that the calling context is an
ordinary function call position from within a Crucible basic block.
The included 'StmtSeq' is the remaining statements in the basic block to be
executed following the return.
-}
ReturnToCrucible ::
TypeRepr ret {- Type of the return value -} ->
StmtSeq ext blocks r (ctx ::> ret) {- Remaining statements to execute -} ->
ReturnHandler ret p sym ext root (CrucibleLang blocks r) ('Just ctx)
{- | The 'TailReturnToCrucible' constructor indicates that the calling context is a
tail call position from the end of a Crucible basic block. Upon receiving
the return value, that value should be immediately returned in the caller's
context as well.
-}
TailReturnToCrucible ::
(ret ~ r) =>
ReturnHandler ret p sym ext root (CrucibleLang blocks r) ctx
------------------------------------------------------------------------
-- ActiveTree
type PartialResultFrame :: Type -> Type -> Type -> Maybe (Ctx CrucibleType) -> Type
type PartialResultFrame sym ext f args =
PartialResult sym ext (SimFrame sym ext f args)
{- | An active execution tree contains at least one active execution.
The data structure is organized so that the current execution
can be accessed rapidly.
Type parameters:
- @p@: see 'cruciblePersonality'
- @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
- @ext@: language extension, see "Lang.Crucible.CFG.Extension"
- @root@: global return type of the entire computation
- @f@: the frame type of the caller ('CrucibleLang' or 'OverrideLang')
-- - @args@: arguments to the current frame (see 'SimFrame')
-}
type ActiveTree :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type
data ActiveTree p sym ext root f args
= ActiveTree
{ _actContext :: !(ValueFromFrame p sym ext root f)
, _actResult :: !(PartialResultFrame sym ext f args)
}
-- | Create a tree with a single top frame.
singletonTree ::
TopFrame sym ext f args ->
ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree f = ActiveTree { _actContext = VFFEnd VFVEnd
, _actResult = TotalRes f
}
-- | Access the calling context of the currently-active frame
actContext ::
Lens (ActiveTree p sym ext root f args)
(ActiveTree p sym ext root f args)
(ValueFromFrame p sym ext root f)
(ValueFromFrame p sym ext root f)
actContext = lens _actContext (\s v -> s { _actContext = v })
actResult ::
Lens (ActiveTree p sym ext root f args0)
(ActiveTree p sym ext root f args1)
(PartialResult sym ext (SimFrame sym ext f args0))
(PartialResult sym ext (SimFrame sym ext f args1))
actResult = lens _actResult setter
where setter s v = ActiveTree { _actContext = _actContext s
, _actResult = v
}
{-# INLINE actResult #-}
-- | Access the currently-active frame
actFrame ::
Lens (ActiveTree p sym ext root f args)
(ActiveTree p sym ext root f args')
(TopFrame sym ext f args)
(TopFrame sym ext f args')
actFrame = actResult . partialValue
{-# INLINE actFrame #-}
-- | Return the call stack of all active frames, in
-- reverse activation order (i.e., with callees
-- appearing before callers).
activeFrames :: ActiveTree ctx sym ext root a args ->
[SomeFrame (SimFrame sym ext)]
activeFrames (ActiveTree ctx ar) =
SomeFrame (ar^.partialValue^.gpValue) : parentFrames ctx
------------------------------------------------------------------------
-- SimContext
-- | A definition of a function's semantics, given as a Haskell action.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @args@: types of arguments to the override
-- - @ret@: return type of the override
type Override :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type
data Override p sym ext (args :: Ctx CrucibleType) ret
= Override { overrideName :: FunctionName
, overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)
}
-- | State used to indicate what to do when function is called. A function
-- may either be defined by writing a Haskell 'Override' or by giving
-- a Crucible control-flow graph representation.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @args@: argument types
-- - @ret@: return type
type FnState :: Type -> Type -> Type -> Ctx CrucibleType -> CrucibleType -> Type
data FnState p sym ext args ret
= UseOverride !(Override p sym ext args ret)
| forall blocks . UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks)
-- | A map from function handles to their semantics.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type FunctionBindings :: Type -> Type -> Type -> Type
newtype FunctionBindings p sym ext = FnBindings { fnBindings :: FnHandleMap (FnState p sym ext) }
-- | The type of functions that interpret extension statements. These
-- have access to the main simulator state, and can make fairly arbitrary
-- changes to it.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type EvalStmtFunc :: Type -> Type -> Type -> Type
type EvalStmtFunc p sym ext =
forall rtp blocks r ctx tp'.
StmtExtension ext (RegEntry sym) tp' ->
CrucibleState p sym ext rtp blocks r ctx ->
IO (RegValue sym tp', CrucibleState p sym ext rtp blocks r ctx)
-- | In order to start executing a simulator, one must provide an implementation
-- of the extension syntax. This includes an evaluator for the added
-- expression forms, and an evaluator for the added statement forms.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type ExtensionImpl :: Type -> Type -> Type -> Type
data ExtensionImpl p sym ext
= ExtensionImpl
{ extensionEval ::
forall bak rtp blocks r ctx.
IsSymBackend sym bak =>
bak ->
IntrinsicTypes sym ->
(Int -> String -> IO ()) ->
CrucibleState p sym ext rtp blocks r ctx ->
EvalAppFunc sym (ExprExtension ext)
, extensionExec :: EvalStmtFunc p sym ext
}
-- | Trivial implementation for the "empty" extension, which adds no
-- additional syntactic forms.
emptyExtensionImpl :: ExtensionImpl p sym ()
emptyExtensionImpl =
ExtensionImpl
{ extensionEval = \_sym _iTypes _log _f _state -> \case
, extensionExec = \case
}
type IsSymInterfaceProof :: Type -> Type -> Type
type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a
-- | Some kind of 'Integer' to be collected during execution.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type Metric :: Type -> Type -> Type -> Type
newtype Metric p sym ext =
Metric {
runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer
}
-- | Top-level state record for the simulator. The state contained in this record
-- remains persistent across all symbolic simulator actions. In particular, it
-- is not rolled back when the simulator returns previous program points to
-- explore additional paths, etc.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
type SimContext :: Type -> Type -> Type -> Type
data SimContext p sym ext
= SimContext { _ctxBackend :: !(SomeBackend sym)
-- | Class dictionary for @'IsSymInterface' sym@
, ctxSolverProof :: !(forall a . IsSymInterfaceProof sym a)
, ctxIntrinsicTypes :: !(IntrinsicTypes sym)
-- | Allocator for function handles
, simHandleAllocator :: !(HandleAllocator)
-- | Handle to write messages to.
, printHandle :: !Handle
, extensionImpl :: ExtensionImpl p sym ext
, _functionBindings :: !(FunctionBindings p sym ext)
-- | See 'cruciblePersonality'.
, _cruciblePersonality :: !p
, _profilingMetrics :: !(Map Text (Metric p sym ext))
}
-- | Create a new 'SimContext' with the given bindings.
initSimContext ::
IsSymBackend sym bak =>
bak {- ^ Symbolic backend -} ->
IntrinsicTypes sym {- ^ Implementations of intrinsic types -} ->
HandleAllocator {- ^ Handle allocator for creating new function handles -} ->
Handle {- ^ Handle to write output to -} ->
FunctionBindings personality sym ext {- ^ Initial bindings for function handles -} ->
ExtensionImpl personality sym ext {- ^ Semantics for extension syntax -} ->
personality {- ^ Initial value for custom user state -} ->
SimContext personality sym ext
initSimContext bak muxFns halloc h bindings extImpl personality =
SimContext { _ctxBackend = SomeBackend bak
, ctxSolverProof = \a -> a
, ctxIntrinsicTypes = muxFns
, simHandleAllocator = halloc
, printHandle = h
, extensionImpl = extImpl
, _functionBindings = bindings
, _cruciblePersonality = personality
, _profilingMetrics = Map.empty
}
withBackend ::
SimContext personality sym ext ->
(forall bak. IsSymBackend sym bak => bak -> a) ->
a
withBackend ctx f = case _ctxBackend ctx of SomeBackend bak -> f bak
-- | Access the symbolic backend inside a 'SimContext'.
ctxSymInterface :: Getter (SimContext p sym ext) sym
ctxSymInterface = to (\ctx ->
case _ctxBackend ctx of
SomeBackend bak -> backendGetSym bak)
-- | A map from function handles to their semantics.
functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext)
functionBindings = lens _functionBindings (\s v -> s { _functionBindings = v })
-- | Custom state inside the 'SimContext'.
--
-- Crucible itself is entirely polymorphic over @p@. Downstream applications can
-- instantiate it to any sort of state that they would like to associate with a
-- 'SimContext'.
--
-- For example, applications based on
-- [@macaw-symbolic@](https://github.com/GaloisInc/macaw/tree/master/symbolic)
-- can instantiate this to a structure holding enough information to perform
-- incremental code discovery. See @ambient-verifier@'s
-- [@AmbientSimulatorState@](https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Extensions.hs#L1092-1137).
--
-- Code that needs to store some state in the personality but doesn\'t wish to
-- fix a particular type can use the \"classy lenses\" approach, e.g.,
--
-- @
-- class HasFooState p where
-- fooState :: `Lens'` p FooState
-- @
--
-- For examples of this approach, see
--
-- * [@HasMacawLazySimulatorState@](https://github.com/GaloisInc/macaw/blob/cbec559b428fdd194398d07fc08c8c570a1d3bab/symbolic/src/Data/Macaw/Symbolic/MemOps.hs#L385-L394)
-- * [@HasGreaseSimulatorState@](https://github.com/GaloisInc/grease/blob/a50d54d2f414d15974dcf2d21654fbfe3527f0fa/src/Grease/Macaw/SimulatorState.hs#L90-L97)
cruciblePersonality :: Lens' (SimContext p sym ext) p
cruciblePersonality = lens _cruciblePersonality (\s v -> s{ _cruciblePersonality = v })
profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext))
profilingMetrics = lens _profilingMetrics (\s v -> s { _profilingMetrics = v })
------------------------------------------------------------------------
-- SimState
-- | An abort handler indicates to the simulator what actions to take
-- when an abort occurs. Usually, one should simply use the
-- 'defaultAbortHandler' from "Lang.Crucible.Simulator", which
-- unwinds the tree context to the nearest branch point and
-- correctly resumes simulation. However, for some use cases, it
-- may be desirable to take additional or alternate actions on abort
-- events; in which case, the library user may replace the default
-- abort handler with their own.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
newtype AbortHandler p sym ext rtp
= AH { runAH :: forall (l :: Type) args.
AbortExecReason ->
ExecCont p sym ext rtp l args
}
-- | A SimState contains the execution context, an error handler, and
-- the current execution tree. It captures the entire state
-- of the symbolic simulator.
--
-- Type parameters:
--
-- - @p@: see 'cruciblePersonality'
-- - @sym@: instance of 'Lang.Crucible.Backend.IsSymInterface'
-- - @ext@: language extension, see "Lang.Crucible.CFG.Extension"
-- - @rtp@: type of the return value
-- - @f@: the type of the top frame ('CrucibleLang' or 'OverrideLang')
-- - @args@: arguments to the current frame (see 'SimFrame')
type SimState :: Type -> Type -> Type -> Type -> Type -> Maybe (Ctx.Ctx CrucibleType) -> Type
data SimState p sym ext rtp f args
= SimState { _stateContext :: !(SimContext p sym ext)
, _abortHandler :: !(AbortHandler p sym ext rtp)
, _stateTree :: !(ActiveTree p sym ext rtp f args)
}
type SomeSimState :: Type -> Type -> Type -> Type -> Type
data SomeSimState p sym ext rtp =
forall f args. SomeSimState !(SimState p sym ext rtp f args)
-- | A simulator state that is currently executing Crucible instructions.
type CrucibleState p sym ext rtp blocks ret args
= SimState p sym ext rtp (CrucibleLang blocks ret) ('Just args)
-- | Create an initial 'SimState'
initSimState ::
SimContext p sym ext {- ^ initial 'SimContext' state -} ->
SymGlobalState sym {- ^ state of Crucible global variables -} ->
AbortHandler p sym ext (RegEntry sym ret) {- ^ initial abort handler -} ->
TypeRepr ret ->
IO (SimState p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
initSimState ctx globals ah ret =
do let halloc = simHandleAllocator ctx
h <- mkHandle' halloc startFunctionName Ctx.Empty ret
let startFrame = OverrideFrame { _override = startFunctionName
, _overrideHandle = SomeHandle h
, _overrideRegMap = emptyRegMap
}
let startGP = GlobalPair (OF startFrame) globals
return
SimState
{ _stateContext = ctx
, _abortHandler = ah
, _stateTree = singletonTree startGP
}
stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc)
stateLocation = to f
where
f :: SimState p sym ext r f a -> Maybe ProgramLoc
f st = case st^.stateTree . actFrame . gpValue of
MF cf -> Just $! (frameProgramLoc cf)
OF _ -> Nothing
RF _ _ -> Nothing
-- | Access the 'SimContext' inside a 'SimState'
stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext)
stateContext = lens _stateContext (\s v -> s { _stateContext = v })
{-# INLINE stateContext #-}
-- | Access the current abort handler of a state.
abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r)
abortHandler = lens _abortHandler (\s v -> s { _abortHandler = v })
-- | Access the active tree associated with a state.
stateTree ::
Lens (SimState p sym ext rtp f a)
(SimState p sym ext rtp g b)
(ActiveTree p sym ext rtp f a)
(ActiveTree p sym ext rtp g b)
stateTree = lens _stateTree (\s v -> s { _stateTree = v })
{-# INLINE stateTree #-}
-- | Access the Crucible call frame inside a 'SimState'
stateCrucibleFrame ::
Lens (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a))
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
(CallFrame sym ext blocks r a)
(CallFrame sym ext blocks r a')
stateCrucibleFrame = stateTree . actFrame . crucibleTopFrame
{-# INLINE stateCrucibleFrame #-}
-- | Access the override frame inside a 'SimState'
stateOverrideFrame ::
Lens
(SimState p sym ext q (OverrideLang r) ('Just a))
(SimState p sym ext q (OverrideLang r) ('Just a'))
(OverrideFrame sym r a)
(OverrideFrame sym r a')
stateOverrideFrame = stateTree . actFrame . gpValue . overrideSimFrame
-- | Access the globals inside a 'SimState'
stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym)
stateGlobals = stateTree . actFrame . gpGlobals
-- | Get the symbolic interface out of a 'SimState'
stateSymInterface :: Getter (SimState p sym ext r f a) sym
stateSymInterface = stateContext . ctxSymInterface
-- | Get the intrinsic type map out of a 'SimState'
stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym)
stateIntrinsicTypes = stateContext . to ctxIntrinsicTypes
-- | Get the configuration object out of a 'SimState'
stateConfiguration :: Getter (SimState p sym ext r f args) Config
stateConfiguration = to (\s -> stateSolverProof s (getConfiguration (s^.stateSymInterface)))
-- | Provide the 'IsSymInterface' typeclass dictionary from a 'SimState'
stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a)
stateSolverProof s = ctxSolverProof (s^.stateContext)