| Copyright | (c) Galois Inc 2019 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Simulator.PathSplitting
Description
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).
Synopsis
- data WorkItem p sym ext rtp = forall f args.WorkItem {
- workItemPred :: Pred sym
- workItemLoc :: ProgramLoc
- workItemFrame :: PausedFrame p sym ext rtp f
- workItemState :: SimState p sym ext rtp f ('Just args)
- workItemAssumes :: AssumptionState sym
- type WorkList p sym ext rtp = IORef (Seq (WorkItem p sym ext rtp))
- queueWorkItem :: WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO ()
- dequeueWorkItem :: WorkList p sym ext rtp -> IO (Maybe (WorkItem p sym ext rtp))
- restoreWorkItem :: IsSymInterface sym => WorkItem p sym ext rtp -> IO (ExecState p sym ext rtp)
- pathSplittingFeature :: IsSymInterface sym => WorkList p sym ext rtp -> ExecutionFeature 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))
Documentation
data WorkItem p sym ext rtp Source #
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.
Constructors
| forall f args. WorkItem | |
Fields
| |
type WorkList p sym ext rtp = IORef (Seq (WorkItem p sym ext rtp)) Source #
A WorkList represents a sequence of WorkItems that still
need to be explored.
queueWorkItem :: WorkItem p sym ext rtp -> WorkList p sym ext rtp -> IO () Source #
Put a work item onto the front of the work list.
dequeueWorkItem :: WorkList p sym ext rtp -> IO (Maybe (WorkItem p sym ext rtp)) Source #
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.
restoreWorkItem :: IsSymInterface sym => WorkItem p sym ext rtp -> IO (ExecState p sym ext rtp) Source #
Given a work item, restore the simulator state so that it is ready to resume exploring the path that it represents.
pathSplittingFeature :: IsSymInterface sym => WorkList p sym ext rtp -> ExecutionFeature p sym ext rtp Source #
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.
executeCrucibleDFSPaths Source #
Arguments
| :: forall p sym ext rtp. (IsSymInterface sym, IsSyntaxExtension ext) | |
| => [ExecutionFeature p sym ext rtp] | Execution features to install |
| -> ExecState p sym ext rtp | Execution state to begin executing |
| -> (ExecResult p sym ext rtp -> IO Bool) | Path result continuation, return |
| -> IO (Word64, Seq (WorkItem p sym ext rtp)) |
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.