Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Simulator.Profiling

Contents

Profiling data structures

Description

Synopsis

profilingFeature :: ProfilingTable -> EventFilter -> Maybe ProfilingOptions -> IO (GenericExecutionFeature sym)
data ProfilingOptions = ProfilingOptions {
- periodicProfileInterval :: NominalDiffTime
- periodicProfileAction :: ProfilingTable -> IO ()
}
data EventFilter = EventFilter {
- recordProfiling :: Bool
- recordCoverage :: Bool
}
profilingEventFilter :: EventFilter
newProfilingTable :: IO ProfilingTable
recordSolverEvent :: ProfilingTable -> SolverEvent -> IO ()
startRecordingSolverEvents :: IsSymInterface sym => sym -> ProfilingTable -> IO ()
enterEvent :: ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
exitEvent :: ProfilingTable -> FunctionName -> IO ()
inProfilingFrame :: ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO a -> IO a
readMetrics :: ProfilingTable -> IO (Metrics Identity)
data CrucibleProfile = CrucibleProfile {
- crucibleProfileTime :: UTCTime
- crucibleProfileCGEvents :: [CGEvent]
- crucibleProfileSolverEvents :: [SolverEvent]
}
readProfilingState :: ProfilingTable -> IO (UTCTime, [CGEvent], [(UTCTime, SolverEvent)])
writeProfileReport :: FilePath -> String -> String -> ProfilingTable -> IO ()
data CGEvent = CGEvent {
- cgEvent_fnName :: FunctionName
- cgEvent_source :: Maybe Position
- cgEvent_callsite :: Maybe Position
- cgEvent_type :: CGEventType
- cgEvent_blocks :: [String]
- cgEvent_metrics :: Metrics Identity
- cgEvent_time :: UTCTime
- cgEvent_id :: Integer
}
data CGEventType
- = ENTER
- | EXIT
- | BLOCK
- | BRANCH
data ProfilingTable = ProfilingTable {
- callGraphEvents :: IORef (Seq CGEvent)
- eventDedups :: IORef (HashSet EventDedup)
- metrics :: Metrics IORef
- eventIDRef :: IORef Integer
- solverEvents :: IORef (Seq (UTCTime, SolverEvent))
}
newtype Metric p sym ext = Metric {
- runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer
}
data Metrics f = Metrics {
- metricSplits :: f Integer
- metricMerges :: f Integer
- metricAborts :: f Integer
- metricSolverStats :: f Statistics
- metricExtraMetrics :: f (Map Text Integer)
}
symProUIJSON :: String -> String -> ProfilingTable -> IO JSValue
symProUIString :: String -> String -> ProfilingTable -> IO String

Documentation

profilingFeature :: ProfilingTable -> EventFilter -> Maybe ProfilingOptions -> IO (GenericExecutionFeature sym) Source #

This feature will pay attention to function call entry/exit events and track the elapsed time and various other metrics in the given profiling table. The ProfilingOptions can be used to export intermediate profiling data at regular intervals, if desired.

data ProfilingOptions Source #

Constructors

ProfilingOptions
Fields periodicProfileInterval :: NominalDiffTime periodicProfileAction :: ProfilingTable -> IO ()

data EventFilter Source #

Constructors

EventFilter
Fields recordProfiling :: Bool recordCoverage :: Bool

profilingEventFilter :: EventFilter Source #

An EventFilter that enables only Crucible profiling.

newProfilingTable :: IO ProfilingTable Source #

recordSolverEvent :: ProfilingTable -> SolverEvent -> IO () Source #

startRecordingSolverEvents :: IsSymInterface sym => sym -> ProfilingTable -> IO () Source #

enterEvent :: ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO () Source #

exitEvent :: ProfilingTable -> FunctionName -> IO () Source #

inProfilingFrame :: ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO a -> IO a Source #

readMetrics :: ProfilingTable -> IO (Metrics Identity) Source #

data CrucibleProfile Source #

Constructors

CrucibleProfile
Fields crucibleProfileTime :: UTCTime crucibleProfileCGEvents :: [CGEvent] crucibleProfileSolverEvents :: [SolverEvent]

Instances

Instances details

Generic CrucibleProfile Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Associated Types type Rep CrucibleProfile :: Type -> Type # Methods from :: CrucibleProfile -> Rep CrucibleProfile x # to :: Rep CrucibleProfile x -> CrucibleProfile #
Show CrucibleProfile Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods showsPrec :: Int -> CrucibleProfile -> ShowS # show :: CrucibleProfile -> String # showList :: [CrucibleProfile] -> ShowS #
type Rep CrucibleProfile Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling type Rep CrucibleProfile = D1 ('MetaData "CrucibleProfile" "Lang.Crucible.Simulator.Profiling" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) (C1 ('MetaCons "CrucibleProfile" 'PrefixI 'True) (S1 ('MetaSel ('Just "crucibleProfileTime") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UTCTime) :: (S1 ('MetaSel ('Just "crucibleProfileCGEvents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CGEvent]) :: S1 ('MetaSel ('Just "crucibleProfileSolverEvents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SolverEvent]))))

readProfilingState :: ProfilingTable -> IO (UTCTime, [CGEvent], [(UTCTime, SolverEvent)]) Source #

writeProfileReport Source #

Arguments

:: FilePath	File to write
-> String	"name" for the report
-> String	"source" for the report
-> ProfilingTable	profiling data to populate the report
-> IO ()

Write a profiling report file in the JS/JSON format expected by tye symProUI front end.

Profiling data structures

data CGEvent Source #

Constructors

CGEvent
Fields cgEvent_fnName :: FunctionName cgEvent_source :: Maybe Position cgEvent_callsite :: Maybe Position cgEvent_type :: CGEventType cgEvent_blocks :: [String] cgEvent_metrics :: Metrics Identity cgEvent_time :: UTCTime cgEvent_id :: Integer

Instances

Instances details

Generic CGEvent Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Associated Types type Rep CGEvent :: Type -> Type # Methods from :: CGEvent -> Rep CGEvent x # to :: Rep CGEvent x -> CGEvent #
Show CGEvent Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods showsPrec :: Int -> CGEvent -> ShowS # show :: CGEvent -> String # showList :: [CGEvent] -> ShowS #
type Rep CGEvent Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling type Rep CGEvent = D1 ('MetaData "CGEvent" "Lang.Crucible.Simulator.Profiling" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) (C1 ('MetaCons "CGEvent" 'PrefixI 'True) (((S1 ('MetaSel ('Just "cgEvent_fnName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctionName) :: S1 ('MetaSel ('Just "cgEvent_source") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Position))) :: (S1 ('MetaSel ('Just "cgEvent_callsite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Position)) :: S1 ('MetaSel ('Just "cgEvent_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CGEventType))) :: ((S1 ('MetaSel ('Just "cgEvent_blocks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Just "cgEvent_metrics") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Metrics Identity))) :: (S1 ('MetaSel ('Just "cgEvent_time") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UTCTime) :*: S1 ('MetaSel ('Just "cgEvent_id") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))))

data CGEventType Source #

Constructors

ENTER
EXIT
BLOCK
BRANCH

Instances

Instances details

Generic CGEventType Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Associated Types type Rep CGEventType :: Type -> Type # Methods from :: CGEventType -> Rep CGEventType x # to :: Rep CGEventType x -> CGEventType #
Show CGEventType Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods showsPrec :: Int -> CGEventType -> ShowS # show :: CGEventType -> String # showList :: [CGEventType] -> ShowS #
Eq CGEventType Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods (==) :: CGEventType -> CGEventType -> Bool # (/=) :: CGEventType -> CGEventType -> Bool #
Ord CGEventType Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods compare :: CGEventType -> CGEventType -> Ordering # (<) :: CGEventType -> CGEventType -> Bool # (<=) :: CGEventType -> CGEventType -> Bool # (>) :: CGEventType -> CGEventType -> Bool # (>=) :: CGEventType -> CGEventType -> Bool # max :: CGEventType -> CGEventType -> CGEventType # min :: CGEventType -> CGEventType -> CGEventType #
type Rep CGEventType Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling type Rep CGEventType = D1 ('MetaData "CGEventType" "Lang.Crucible.Simulator.Profiling" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) ((C1 ('MetaCons "ENTER" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EXIT" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BLOCK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BRANCH" 'PrefixI 'False) (U1 :: Type -> Type)))

data ProfilingTable Source #

Constructors

ProfilingTable
Fields callGraphEvents :: IORef (Seq CGEvent) eventDedups :: IORef (HashSet EventDedup) metrics :: Metrics IORef eventIDRef :: IORef Integer solverEvents :: IORef (Seq (UTCTime, SolverEvent))

newtype Metric p sym ext Source #

Constructors

Metric
Fields runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer

data Metrics f Source #

Constructors

Metrics
Fields metricSplits :: f Integer metricMerges :: f Integer metricAborts :: f Integer metricSolverStats :: f Statistics metricExtraMetrics :: f (Map Text Integer)

Instances

Instances details

FoldableF Metrics Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> Metrics e -> m # foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Metrics e -> b # foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Metrics e -> b # foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Metrics e -> b # foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Metrics e -> b # toListF :: (forall (tp :: k). f tp -> a) -> Metrics f -> [a] #
FunctorF Metrics Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods fmapF :: (forall (x :: k). f x -> g x) -> Metrics f -> Metrics g #
TraversableF Metrics Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Metrics e -> m (Metrics f) #
Generic (Metrics Identity) Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Associated Types type Rep (Metrics Identity) :: Type -> Type # Methods from :: Metrics Identity -> Rep (Metrics Identity) x # to :: Rep (Metrics Identity) x -> Metrics Identity #
Show (Metrics Identity) Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling Methods showsPrec :: Int -> Metrics Identity -> ShowS # show :: Metrics Identity -> String # showList :: [Metrics Identity] -> ShowS #
type Rep (Metrics Identity) Source #
Instance details Defined in Lang.Crucible.Simulator.Profiling type Rep (Metrics Identity) = D1 ('MetaData "Metrics" "Lang.Crucible.Simulator.Profiling" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) (C1 ('MetaCons "Metrics" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metricSplits") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Identity Integer)) :: S1 ('MetaSel ('Just "metricMerges") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Identity Integer))) :: (S1 ('MetaSel ('Just "metricAborts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Identity Integer)) :: (S1 ('MetaSel ('Just "metricSolverStats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Identity Statistics)) :: S1 ('MetaSel ('Just "metricExtraMetrics") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Identity (Map Text Integer)))))))

symProUIJSON :: String -> String -> ProfilingTable -> IO JSValue Source #

symProUIString :: String -> String -> ProfilingTable -> IO String Source #