Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
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 :: Maybe (Ctx CrucibleType)). SimState p sym ext rtp f args -> IO Integer
}
data Metrics (f :: Type -> Type) = 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

Instance details

Defined in Lang.Crucible.Simulator.Profiling

type Rep CrucibleProfile = D1 ('MetaData "CrucibleProfile" "Lang.Crucible.Simulator.Profiling" "crucible-0.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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]))))

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.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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

Instance details

Defined in Lang.Crucible.Simulator.Profiling

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

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

Instance details

Defined in Lang.Crucible.Simulator.Profiling

type Rep CGEventType = D1 ('MetaData "CGEventType" "Lang.Crucible.Simulator.Profiling" "crucible-0.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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)))

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.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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 #

Some kind of Integer to be collected during execution.

Type parameters:

p: see cruciblePersonality
sym: instance of IsSymInterface
ext: language extension, see Lang.Crucible.CFG.Extension

Constructors

Metric
Fields runMetric :: forall rtp f (args :: Maybe (Ctx CrucibleType)). SimState p sym ext rtp f args -> IO Integer

data Metrics (f :: Type -> Type) Source #

Constructors

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