Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Simulator.RecordAndReplay

Synopsis

class HasRecordState p r sym ext rtp | p -> r sym ext rtp where
- recordState :: Lens' p (RecordState r sym ext rtp)
data RecordState p sym ext rtp
mkRecordState :: HandleAllocator -> IO (RecordState p sym ext rtp)
class HasReplayState p r sym ext rtp | p -> r sym ext rtp where
- replayState :: Lens' p (ReplayState r sym ext rtp)
data ReplayState p sym ext rtp
mkReplayState :: HandleAllocator -> RecordedTrace sym -> IO (ReplayState p sym ext rtp)
recordTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)). (IsExprBuilder sym, HasRecordState p p sym ext rtp) => SimState p sym ext rtp f args -> IO (Maybe (SymNat sym))
replayTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)). (IsExprBuilder sym, HasReplayState p p sym ext rtp) => SimState p sym ext rtp f args -> IO (Maybe (SymNat sym))
data RecordedTrace sym
getRecordedTrace :: IsExprBuilder sym => SymGlobalState sym -> RecordState p sym ext rtp -> sym -> (Pred sym -> IO Bool) -> IO (RecordedTrace sym)
recordFeature :: (HasRecordState p p sym ext rtp, IsExprBuilder sym) => ExecutionFeature p sym ext rtp
replayFeature :: (HasReplayState p p sym ext rtp, IsExprBuilder sym) => Bool -> ExecutionFeature p sym ext rtp
initialTrace :: forall p1 sym1 ext1 rtp1 p2 sym2 ext2 rtp2 f. Functor f => (RecordedTrace sym1 -> f (RecordedTrace sym2)) -> ReplayState p1 sym1 ext1 rtp1 -> f (ReplayState p2 sym2 ext2 rtp2)
traceGlobal :: forall p1 sym ext1 rtp1 p2 ext2 rtp2 f. Functor f => (GlobalVar TraceType -> f (GlobalVar TraceType)) -> ReplayState p1 sym ext1 rtp1 -> f (ReplayState p2 sym ext2 rtp2)
emptyRecordedTrace :: sym -> IO (RecordedTrace sym)

Documentation

class HasRecordState p r sym ext rtp | p -> r sym ext rtp where Source #

A class for Crucible personality types p which contain a RecordState. This execution feature is polymorphic over RecordState so that downstream users can supply their own personality types that extend RecordState further.

Methods

recordState :: Lens' p (RecordState r sym ext rtp) Source #

Instances

Instances details

HasRecordState (RecordState p sym ext rtp) p sym ext rtp Source #
Instance details Defined in Lang.Crucible.Simulator.RecordAndReplay Methods recordState :: Lens' (RecordState p sym ext rtp) (RecordState p sym ext rtp) Source #

data RecordState p sym ext rtp Source #

Type parameters:

p: see cruciblePersonality
sym: instance of IsSymInterface
ext: language extension, see Lang.Crucible.CFG.Extension
rtp: type of the simulator return value

Instances

Instances details

HasRecordState (RecordState p sym ext rtp) p sym ext rtp Source #
Instance details Defined in Lang.Crucible.Simulator.RecordAndReplay Methods recordState :: Lens' (RecordState p sym ext rtp) (RecordState p sym ext rtp) Source #

mkRecordState :: HandleAllocator -> IO (RecordState p sym ext rtp) Source #

Constructor for RecordState

class HasReplayState p r sym ext rtp | p -> r sym ext rtp where Source #

A class for Crucible personality types p which contain a ReplayState. This execution feature is polymorphic over ReplayState so that downstream users can supply their own personality types that extend ReplayState further.

Methods

replayState :: Lens' p (ReplayState r sym ext rtp) Source #

Instances

Instances details

HasReplayState (ReplayState p sym ext rtp) p sym ext rtp Source #
Instance details Defined in Lang.Crucible.Simulator.RecordAndReplay Methods replayState :: Lens' (ReplayState p sym ext rtp) (ReplayState p sym ext rtp) Source #

data ReplayState p sym ext rtp Source #

Type parameters:

p: see cruciblePersonality
sym: instance of IsSymInterface
ext: language extension, see Lang.Crucible.CFG.Extension
rtp: type of the simulator return value

Instances

Instances details

HasReplayState (ReplayState p sym ext rtp) p sym ext rtp Source #
Instance details Defined in Lang.Crucible.Simulator.RecordAndReplay Methods replayState :: Lens' (ReplayState p sym ext rtp) (ReplayState p sym ext rtp) Source #

mkReplayState :: HandleAllocator -> RecordedTrace sym -> IO (ReplayState p sym ext rtp) Source #

Constructor for ReplayState

recordTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)). (IsExprBuilder sym, HasRecordState p p sym ext rtp) => SimState p sym ext rtp f args -> IO (Maybe (SymNat sym)) Source #

Get the length of the currently recorded trace

replayTraceLength :: forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType)). (IsExprBuilder sym, HasReplayState p p sym ext rtp) => SimState p sym ext rtp f args -> IO (Maybe (SymNat sym)) Source #

Get the length of the trace being replayed

data RecordedTrace sym Source #

A trace from recordFeature, processed and ready for consumption by replayFeature.

getRecordedTrace Source #

Arguments

:: IsExprBuilder sym
=> SymGlobalState sym
-> RecordState p sym ext rtp
-> sym
-> (Pred sym -> IO Bool)	Evaluation for booleans, usually a `GroundEvalFn`
-> IO (RecordedTrace sym)

Obtain a RecordedTrace after execution.

This currently requires concretizing the trace, because there is no efficient reverse operation for SymSequence.

recordFeature :: (HasRecordState p p sym ext rtp, IsExprBuilder sym) => ExecutionFeature p sym ext rtp Source #

An ExecutionFeature to record traces.

During execution this logs program locations to a Crucible global variable. After execution, this variable may be read with getRecordedTrace and the RecordedTrace can be passed to replayFeature to "replay" it, i.e., to abort all branches that deviate from it.

If this is not called with InitialState before any other ExecState, it may throw a TraceGlobalNotDefined exception.

replayFeature Source #

Arguments

:: (HasReplayState p p sym ext rtp, IsExprBuilder sym)
=> Bool	Whether to stop at the end of the trace. If this is `True` and execution has exhausted the trace, then any further execution will be aborted via `InfeasibleBranch`.
-> ExecutionFeature p sym ext rtp

An ExecutionFeature to replay traces recorded with recordFeature.

Branches that deviate from the given trace will be aborted with InfeasibleBranch.

If this is not called with InitialState before any other ExecState, it may throw a TraceGlobalNotDefined exception.

initialTrace :: forall p1 sym1 ext1 rtp1 p2 sym2 ext2 rtp2 f. Functor f => (RecordedTrace sym1 -> f (RecordedTrace sym2)) -> ReplayState p1 sym1 ext1 rtp1 -> f (ReplayState p2 sym2 ext2 rtp2) Source #

traceGlobal :: forall p1 sym ext1 rtp1 p2 ext2 rtp2 f. Functor f => (GlobalVar TraceType -> f (GlobalVar TraceType)) -> ReplayState p1 sym ext1 rtp1 -> f (ReplayState p2 sym ext2 rtp2) Source #

emptyRecordedTrace :: sym -> IO (RecordedTrace sym) Source #