-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.PathSplitting
-- Description      : Support for implementing path splitting
-- Copyright        : (c) Galois, Inc 2019
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides an execution feature that converts symbolic
-- branches into path splitting by pushing unexplored paths onto a
-- worklist instead of performing eager path merging (the default
-- behavior).
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.PathSplitting
  ( WorkItem(..)
  , WorkList
  , queueWorkItem
  , dequeueWorkItem
  , restoreWorkItem
  , pathSplittingFeature
  , executeCrucibleDFSPaths
  ) where

import           Control.Lens ( (^.) )
import           Control.Monad.Reader
import           Data.IORef
import           Data.Sequence( Seq )
import qualified Data.Sequence as Seq
import           Data.Word

import           What4.Interface
import           What4.ProgramLoc

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Extension
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.EvalStmt
import           Lang.Crucible.Simulator.Operations


-- | A `WorkItem` represents a suspended symbolic execution path that
--   can later be resumed.  It captures all the relevant context that
--   is required to recreate the simulator state at the point when
--   the path was suspended.
data WorkItem p sym ext rtp =
  forall f args.
  WorkItem
  { -- | The predicate we branched on to generate this work item
    forall p sym ext rtp. WorkItem p sym ext rtp -> Pred sym
workItemPred  :: Pred sym
    -- | The location of the symbolic branch
  , forall p sym ext rtp. WorkItem p sym ext rtp -> ProgramLoc
workItemLoc   :: ProgramLoc
    -- | The paused execution frame
  , ()
workItemFrame :: PausedFrame p sym ext rtp f
    -- | The overall execution state of this path
  , ()
workItemState :: SimState p sym ext rtp f ('Just args)
    -- | The assumption state of the symbolic backend when we suspended this work item
  , forall p sym ext rtp. WorkItem p sym ext rtp -> AssumptionState sym
workItemAssumes :: AssumptionState sym
  }

-- | A `WorkList` represents a sequence of `WorkItems` that still
--   need to be explored.
type WorkList p sym ext rtp = IORef (Seq (WorkItem p sym ext rtp))

-- | Put a work item onto the front of the work list.
queueWorkItem :: WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO ()
queueWorkItem :: forall p sym ext rtp.
WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO ()
queueWorkItem WorkItem p sym ext rtp
i WorkList p sym ext rtp
wl = WorkList p sym ext rtp
-> (Seq (WorkItem p sym ext rtp)
    -> (Seq (WorkItem p sym ext rtp), ()))
-> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' WorkList p sym ext rtp
wl (\Seq (WorkItem p sym ext rtp)
xs -> (WorkItem p sym ext rtp
i WorkItem p sym ext rtp
-> Seq (WorkItem p sym ext rtp) -> Seq (WorkItem p sym ext rtp)
forall a. a -> Seq a -> Seq a
Seq.<| Seq (WorkItem p sym ext rtp)
xs, ()))

-- | Pull a work item off the front of the work list, if there are any left.
--   When used with `queueWorkItem`, this function uses the work list as a stack
--   and will explore paths in a depth-first manner.
dequeueWorkItem :: WorkList p sym ext rtp -> IO (Maybe (WorkItem p sym ext rtp))
dequeueWorkItem :: forall p sym ext rtp.
WorkList p sym ext rtp -> IO (Maybe (WorkItem p sym ext rtp))
dequeueWorkItem WorkList p sym ext rtp
wl =
  WorkList p sym ext rtp
-> (Seq (WorkItem p sym ext rtp)
    -> (Seq (WorkItem p sym ext rtp), Maybe (WorkItem p sym ext rtp)))
-> IO (Maybe (WorkItem p sym ext rtp))
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' WorkList p sym ext rtp
wl ((Seq (WorkItem p sym ext rtp)
  -> (Seq (WorkItem p sym ext rtp), Maybe (WorkItem p sym ext rtp)))
 -> IO (Maybe (WorkItem p sym ext rtp)))
-> (Seq (WorkItem p sym ext rtp)
    -> (Seq (WorkItem p sym ext rtp), Maybe (WorkItem p sym ext rtp)))
-> IO (Maybe (WorkItem p sym ext rtp))
forall a b. (a -> b) -> a -> b
$ \Seq (WorkItem p sym ext rtp)
xs ->
     case Seq (WorkItem p sym ext rtp) -> ViewL (WorkItem p sym ext rtp)
forall a. Seq a -> ViewL a
Seq.viewl Seq (WorkItem p sym ext rtp)
xs of
       ViewL (WorkItem p sym ext rtp)
Seq.EmptyL   -> (Seq (WorkItem p sym ext rtp)
xs,  Maybe (WorkItem p sym ext rtp)
forall a. Maybe a
Nothing)
       WorkItem p sym ext rtp
i Seq.:< Seq (WorkItem p sym ext rtp)
xs' -> (Seq (WorkItem p sym ext rtp)
xs', WorkItem p sym ext rtp -> Maybe (WorkItem p sym ext rtp)
forall a. a -> Maybe a
Just WorkItem p sym ext rtp
i)

-- | Given a work item, restore the simulator state so that it is ready to resume
--   exploring the path that it represents.
restoreWorkItem ::
  IsSymInterface sym =>
  WorkItem p sym ext rtp ->
  IO (ExecState p sym ext rtp)
restoreWorkItem :: forall sym p ext rtp.
IsSymInterface sym =>
WorkItem p sym ext rtp -> IO (ExecState p sym ext rtp)
restoreWorkItem (WorkItem Pred sym
branchPred ProgramLoc
loc PausedFrame p sym ext rtp f
frm SimState p sym ext rtp f ('Just args)
st AssumptionState sym
assumes) =
  do let sym :: sym
sym = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting sym (SimState p sym ext rtp f ('Just args)) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f ('Just args)) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateSymInterface
     let simCtx :: SimContext p sym ext
simCtx = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f ('Just args))
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^. Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp f ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecState p sym ext rtp))
-> IO (ExecState p sym ext rtp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (ExecState p sym ext rtp))
 -> IO (ExecState p sym ext rtp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecState p sym ext rtp))
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      do sym -> ProgramLoc -> IO ()
forall sym. IsExprBuilder sym => sym -> ProgramLoc -> IO ()
setCurrentProgramLoc sym
sym ProgramLoc
loc
         bak -> AssumptionState sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> AssumptionState sym -> IO ()
restoreAssumptionState bak
bak AssumptionState sym
assumes
         bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> Maybe ProgramLoc -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
BranchCondition ProgramLoc
loc (PausedFrame p sym ext rtp f -> Maybe ProgramLoc
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
pausedLoc PausedFrame p sym ext rtp f
frm) Pred sym
branchPred)
         let ctx :: ValueFromFrame p sym ext rtp f
ctx = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
-> ValueFromFrame p sym ext rtp f
forall s a. s -> Getting a s a -> a
^. (ActiveTree p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (ActiveTree p sym ext rtp f ('Just args)))
-> SimState p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp f ('Just args)
  -> Const
       (ValueFromFrame p sym ext rtp f)
       (ActiveTree p sym ext rtp f ('Just args)))
 -> SimState p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (SimState p sym ext rtp f ('Just args)))
-> ((ValueFromFrame p sym ext rtp f
     -> Const
          (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
    -> ActiveTree p sym ext rtp f ('Just args)
    -> Const
         (ValueFromFrame p sym ext rtp f)
         (ActiveTree p sym ext rtp f ('Just args)))
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValueFromFrame p sym ext rtp f
 -> Const
      (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
-> ActiveTree p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (ActiveTree p sym ext rtp f ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(ValueFromFrame p sym ext root f1
 -> f2 (ValueFromFrame p sym ext root f1))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args)
actContext
         ReaderT
  (SimState p sym ext rtp f ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp f ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f
-> ReaderT
     (SimState p sym ext rtp f ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym p ext rtp f g (ba :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f -> ExecCont p sym ext rtp g ba
resumeFrame PausedFrame p sym ext rtp f
frm ValueFromFrame p sym ext rtp f
ctx) SimState p sym ext rtp f ('Just args)
st

-- | The path splitting execution feature always selects the \"true\" branch
--   of a symbolic branch to explore first, and pushes the \"false\" branch
--   onto the front of the given work list.  With this feature enabled,
--   a single path will be explored with no symbolic branching until it is finished,
--   and all remaining unexplored paths will be suspended in the work list, where
--   they can be later resumed.
pathSplittingFeature ::
  IsSymInterface sym =>
  WorkList p sym ext rtp ->
  ExecutionFeature p sym ext rtp
pathSplittingFeature :: forall sym p ext rtp.
IsSymInterface sym =>
WorkList p sym ext rtp -> ExecutionFeature p sym ext rtp
pathSplittingFeature WorkList p sym ext rtp
wl = (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall a b. (a -> b) -> a -> b
$ \case
  SymbolicBranchState Pred sym
p PausedFrame p sym ext rtp f
trueFrame PausedFrame p sym ext rtp f
falseFrame CrucibleBranchTarget f postdom_args
_bt SimState p sym ext rtp f ('Just args)
st ->
    SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend (SimState p sym ext rtp f ('Just args)
stSimState p sym ext rtp f ('Just args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f ('Just args))
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp f ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (ExecutionFeatureResult p sym ext rtp))
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    do let sym :: sym
sym = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting sym (SimState p sym ext rtp f ('Just args)) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f ('Just args)) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateSymInterface
       Pred sym
pnot <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
p
       GoalCollector
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (Pred sym) SimError)
assumes <- bak
-> IO
     (GoalCollector
        (CrucibleAssumptions (SymExpr sym))
        (LabeledPred (Pred sym) SimError))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (AssumptionState sym)
saveAssumptionState bak
bak
       ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym

       let wi :: WorkItem p sym ext rtp
wi = WorkItem
                { workItemPred :: Pred sym
workItemPred  = Pred sym
pnot
                , workItemLoc :: ProgramLoc
workItemLoc   = ProgramLoc
loc
                , workItemFrame :: PausedFrame p sym ext rtp f
workItemFrame = PausedFrame p sym ext rtp f -> PausedFrame p sym ext rtp f
forall p sym ext rtp g.
PausedFrame p sym ext rtp g -> PausedFrame p sym ext rtp g
forgetPostdomFrame PausedFrame p sym ext rtp f
falseFrame
                , workItemState :: SimState p sym ext rtp f ('Just args)
workItemState = SimState p sym ext rtp f ('Just args)
st
                , workItemAssumes :: GoalCollector
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (Pred sym) SimError)
workItemAssumes = GoalCollector
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (Pred sym) SimError)
assumes
                }
       WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO ()
forall p sym ext rtp.
WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO ()
queueWorkItem WorkItem p sym ext rtp
wi WorkList p sym ext rtp
wl

       bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> Maybe ProgramLoc -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
BranchCondition ProgramLoc
loc (PausedFrame p sym ext rtp f -> Maybe ProgramLoc
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
pausedLoc PausedFrame p sym ext rtp f
trueFrame) Pred sym
p)

       let ctx :: ValueFromFrame p sym ext rtp f
ctx = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
-> ValueFromFrame p sym ext rtp f
forall s a. s -> Getting a s a -> a
^. (ActiveTree p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (ActiveTree p sym ext rtp f ('Just args)))
-> SimState p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp f ('Just args)
  -> Const
       (ValueFromFrame p sym ext rtp f)
       (ActiveTree p sym ext rtp f ('Just args)))
 -> SimState p sym ext rtp f ('Just args)
 -> Const
      (ValueFromFrame p sym ext rtp f)
      (SimState p sym ext rtp f ('Just args)))
-> ((ValueFromFrame p sym ext rtp f
     -> Const
          (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
    -> ActiveTree p sym ext rtp f ('Just args)
    -> Const
         (ValueFromFrame p sym ext rtp f)
         (ActiveTree p sym ext rtp f ('Just args)))
-> Getting
     (ValueFromFrame p sym ext rtp f)
     (SimState p sym ext rtp f ('Just args))
     (ValueFromFrame p sym ext rtp f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValueFromFrame p sym ext rtp f
 -> Const
      (ValueFromFrame p sym ext rtp f) (ValueFromFrame p sym ext rtp f))
-> ActiveTree p sym ext rtp f ('Just args)
-> Const
     (ValueFromFrame p sym ext rtp f)
     (ActiveTree p sym ext rtp f ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(ValueFromFrame p sym ext root f1
 -> f2 (ValueFromFrame p sym ext root f1))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args)
actContext
       ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNewState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> IO (ExecState p sym ext rtp)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  (SimState p sym ext rtp f ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp f ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f
-> ReaderT
     (SimState p sym ext rtp f ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym p ext rtp f g (ba :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f -> ExecCont p sym ext rtp g ba
resumeFrame (PausedFrame p sym ext rtp f -> PausedFrame p sym ext rtp f
forall p sym ext rtp g.
PausedFrame p sym ext rtp g -> PausedFrame p sym ext rtp g
forgetPostdomFrame PausedFrame p sym ext rtp f
trueFrame) ValueFromFrame p sym ext rtp f
ctx) SimState p sym ext rtp f ('Just args)
st

  ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange


-- | This function executes a state using the path splitting execution
--   feature.  Each time a path is completed, the given result
--   continuation is executed on it. If the continuation returns
--   'True', additional paths will be executed; otherwise, we exit early
--   and exploration stops.
--
--   If exploration continues, the next work item will be
--   popped of the front of the work list and will be executed in turn.
--   If a timeout result is encountered, we instead stop executing paths early.
--   The return value of this function is the number of paths that were
--   completed, and a list of remaining paths (if any) that were not
--   explored due to timeout or early exit.
executeCrucibleDFSPaths :: 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 -} ->
  (ExecResult p sym ext rtp -> IO Bool)
    {- ^ Path result continuation, return 'True' to explore more paths -} ->
  IO (Word64, Seq (WorkItem p sym ext rtp))
executeCrucibleDFSPaths :: forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO Bool)
-> IO (Word64, Seq (WorkItem p sym ext rtp))
executeCrucibleDFSPaths [ExecutionFeature p sym ext rtp]
execFeatures ExecState p sym ext rtp
exst0 ExecResult p sym ext rtp -> IO Bool
cont =
  do IORef (Seq (WorkItem p sym ext rtp))
wl <- Seq (WorkItem p sym ext rtp)
-> IO (IORef (Seq (WorkItem p sym ext rtp)))
forall a. a -> IO (IORef a)
newIORef Seq (WorkItem p sym ext rtp)
forall a. Seq a
Seq.empty
     IORef Word64
cnt <- Word64 -> IO (IORef Word64)
forall a. a -> IO (IORef a)
newIORef (Word64
1::Word64)
     let feats :: [ExecutionFeature p sym ext rtp]
feats = [ExecutionFeature p sym ext rtp]
execFeatures [ExecutionFeature p sym ext rtp]
-> [ExecutionFeature p sym ext rtp]
-> [ExecutionFeature p sym ext rtp]
forall a. [a] -> [a] -> [a]
++ [IORef (Seq (WorkItem p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall sym p ext rtp.
IsSymInterface sym =>
WorkList p sym ext rtp -> ExecutionFeature p sym ext rtp
pathSplittingFeature IORef (Seq (WorkItem p sym ext rtp))
wl]
     IORef (Seq (WorkItem p sym ext rtp))
-> IORef Word64
-> [ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> IO (Word64, Seq (WorkItem p sym ext rtp))
go IORef (Seq (WorkItem p sym ext rtp))
wl IORef Word64
cnt [ExecutionFeature p sym ext rtp]
feats ExecState p sym ext rtp
exst0

 where
 go :: IORef (Seq (WorkItem p sym ext rtp))
-> IORef Word64
-> [ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> IO (Word64, Seq (WorkItem p sym ext rtp))
go IORef (Seq (WorkItem p sym ext rtp))
wl IORef Word64
cnt [ExecutionFeature p sym ext rtp]
feats ExecState p sym ext rtp
exst =
   do ExecResult p sym ext rtp
res <- [ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
executeCrucible [ExecutionFeature p sym ext rtp]
feats ExecState p sym ext rtp
exst
      Bool
goOn <- ExecResult p sym ext rtp -> IO Bool
cont ExecResult p sym ext rtp
res
      case ExecResult p sym ext rtp
res of
        TimeoutResult ExecState p sym ext rtp
_ ->
           do Seq (WorkItem p sym ext rtp)
xs <- IORef (Seq (WorkItem p sym ext rtp))
-> IO (Seq (WorkItem p sym ext rtp))
forall a. IORef a -> IO a
readIORef IORef (Seq (WorkItem p sym ext rtp))
wl
              Word64
i  <- IORef Word64 -> IO Word64
forall a. IORef a -> IO a
readIORef IORef Word64
cnt
              (Word64, Seq (WorkItem p sym ext rtp))
-> IO (Word64, Seq (WorkItem p sym ext rtp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Word64
i,Seq (WorkItem p sym ext rtp)
xs)

        ExecResult p sym ext rtp
_ | Bool -> Bool
not Bool
goOn ->
           do Seq (WorkItem p sym ext rtp)
xs <- IORef (Seq (WorkItem p sym ext rtp))
-> IO (Seq (WorkItem p sym ext rtp))
forall a. IORef a -> IO a
readIORef IORef (Seq (WorkItem p sym ext rtp))
wl
              Word64
i  <- IORef Word64 -> IO Word64
forall a. IORef a -> IO a
readIORef IORef Word64
cnt
              (Word64, Seq (WorkItem p sym ext rtp))
-> IO (Word64, Seq (WorkItem p sym ext rtp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Word64
i,Seq (WorkItem p sym ext rtp)
xs)

          | Bool
otherwise ->
             IORef (Seq (WorkItem p sym ext rtp))
-> IO (Maybe (WorkItem p sym ext rtp))
forall p sym ext rtp.
WorkList p sym ext rtp -> IO (Maybe (WorkItem p sym ext rtp))
dequeueWorkItem IORef (Seq (WorkItem p sym ext rtp))
wl IO (Maybe (WorkItem p sym ext rtp))
-> (Maybe (WorkItem p sym ext rtp)
    -> IO (Word64, Seq (WorkItem p sym ext rtp)))
-> IO (Word64, Seq (WorkItem p sym ext rtp))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               Maybe (WorkItem p sym ext rtp)
Nothing ->
                 do Word64
i <- IORef Word64 -> IO Word64
forall a. IORef a -> IO a
readIORef IORef Word64
cnt
                    (Word64, Seq (WorkItem p sym ext rtp))
-> IO (Word64, Seq (WorkItem p sym ext rtp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Word64
i, Seq (WorkItem p sym ext rtp)
forall a. Monoid a => a
mempty)

               Just WorkItem p sym ext rtp
wi ->
                 do IORef Word64 -> (Word64 -> Word64) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Word64
cnt Word64 -> Word64
forall a. Enum a => a -> a
succ
                    WorkItem p sym ext rtp -> IO (ExecState p sym ext rtp)
forall sym p ext rtp.
IsSymInterface sym =>
WorkItem p sym ext rtp -> IO (ExecState p sym ext rtp)
restoreWorkItem WorkItem p sym ext rtp
wi IO (ExecState p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (Word64, Seq (WorkItem p sym ext rtp)))
-> IO (Word64, Seq (WorkItem p sym ext rtp))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef (Seq (WorkItem p sym ext rtp))
-> IORef Word64
-> [ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> IO (Word64, Seq (WorkItem p sym ext rtp))
go IORef (Seq (WorkItem p sym ext rtp))
wl IORef Word64
cnt [ExecutionFeature p sym ext rtp]
feats