-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.Profiling
-- Description      : Profiling support for the simulator
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.Profiling
  ( profilingFeature
  , ProfilingOptions(..)
  , EventFilter(..)
  , profilingEventFilter
  , newProfilingTable
  , recordSolverEvent
  , startRecordingSolverEvents
  , enterEvent
  , exitEvent
  , inProfilingFrame
  , readMetrics
  , CrucibleProfile(..)
  , readProfilingState
  , writeProfileReport

    -- * Profiling data structures
  , CGEvent(..)
  , CGEventType(..)
  , ProfilingTable(..)
  , Lang.Crucible.Simulator.ExecutionTree.Metric(..)
  , Metrics(..)
  , symProUIJSON
  , symProUIString
  ) where

import qualified Control.Exception as Ex
import           Control.Lens
import           Control.Monad ((<=<), when)
import           Data.Foldable (toList)
import           Data.Hashable
import           Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import           Data.IORef
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Parameterized.TraversableF
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Time.Clock
import           Data.Time.Clock.POSIX
import           Data.Time.Format
import           System.IO (withFile, IOMode(..), hPutStrLn)
import           Text.JSON
import           GHC.Generics (Generic)


import           What4.FunctionName
import           What4.Interface
import           What4.ProgramLoc
import           What4.SatResult

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.Simulator.CallFrame
import           Lang.Crucible.Simulator.EvalStmt
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.Operations


data Metrics f =
  Metrics
  { forall (f :: Type -> Type). Metrics f -> f Integer
metricSplits   :: f Integer
  , forall (f :: Type -> Type). Metrics f -> f Integer
metricMerges   :: f Integer
  , forall (f :: Type -> Type). Metrics f -> f Integer
metricAborts   :: f Integer
  , forall (f :: Type -> Type). Metrics f -> f Statistics
metricSolverStats :: f Statistics
  , forall (f :: Type -> Type). Metrics f -> f (Map Text Integer)
metricExtraMetrics :: f (Map Text Integer)
  }

deriving instance Show (Metrics Identity)
deriving instance Generic (Metrics Identity)

traverseF_metrics :: Applicative m =>
  (forall s. e s -> m (f s)) ->
  Metrics e -> m (Metrics f)
traverseF_metrics :: forall (m :: Type -> Type) (e :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
traverseF_metrics forall s. e s -> m (f s)
h (Metrics e Integer
x1 e Integer
x2 e Integer
x3 e Statistics
x4 e (Map Text Integer)
x5) =
  f Integer
-> f Integer
-> f Integer
-> f Statistics
-> f (Map Text Integer)
-> Metrics f
forall (f :: Type -> Type).
f Integer
-> f Integer
-> f Integer
-> f Statistics
-> f (Map Text Integer)
-> Metrics f
Metrics (f Integer
 -> f Integer
 -> f Integer
 -> f Statistics
 -> f (Map Text Integer)
 -> Metrics f)
-> m (f Integer)
-> m (f Integer
      -> f Integer -> f Statistics -> f (Map Text Integer) -> Metrics f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e Integer -> m (f Integer)
forall s. e s -> m (f s)
h e Integer
x1 m (f Integer
   -> f Integer -> f Statistics -> f (Map Text Integer) -> Metrics f)
-> m (f Integer)
-> m (f Integer
      -> f Statistics -> f (Map Text Integer) -> Metrics f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e Integer -> m (f Integer)
forall s. e s -> m (f s)
h e Integer
x2 m (f Integer -> f Statistics -> f (Map Text Integer) -> Metrics f)
-> m (f Integer)
-> m (f Statistics -> f (Map Text Integer) -> Metrics f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e Integer -> m (f Integer)
forall s. e s -> m (f s)
h e Integer
x3 m (f Statistics -> f (Map Text Integer) -> Metrics f)
-> m (f Statistics) -> m (f (Map Text Integer) -> Metrics f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e Statistics -> m (f Statistics)
forall s. e s -> m (f s)
h e Statistics
x4 m (f (Map Text Integer) -> Metrics f)
-> m (f (Map Text Integer)) -> m (Metrics f)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e (Map Text Integer) -> m (f (Map Text Integer))
forall s. e s -> m (f s)
h e (Map Text Integer)
x5

instance FunctorF Metrics where
  fmapF :: forall (f :: Type -> Type) (g :: Type -> Type).
(forall x. f x -> g x) -> Metrics f -> Metrics g
fmapF = (forall s. f s -> g s) -> Metrics f -> Metrics g
forall {k} (t :: (k -> Type) -> Type) (e :: k -> Type)
       (f :: k -> Type).
TraversableF t =>
(forall (s :: k). e s -> f s) -> t e -> t f
fmapFDefault
instance FoldableF Metrics where
  foldMapF :: forall m (e :: Type -> Type).
Monoid m =>
(forall s. e s -> m) -> Metrics e -> m
foldMapF = (forall s. e s -> m) -> Metrics e -> m
forall {k} (t :: (k -> Type) -> Type) m (e :: k -> Type).
(TraversableF t, Monoid m) =>
(forall (s :: k). e s -> m) -> t e -> m
foldMapFDefault
instance TraversableF Metrics where
  traverseF :: forall (m :: Type -> Type) (e :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
traverseF = (forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
forall (m :: Type -> Type) (e :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
traverseF_metrics

metricsToJSON :: Metrics Identity -> UTCTime -> JSValue
metricsToJSON :: Metrics Identity -> UTCTime -> JSValue
metricsToJSON Metrics Identity
m UTCTime
time = JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject ([(String, JSValue)] -> JSObject JSValue)
-> [(String, JSValue)] -> JSObject JSValue
forall a b. (a -> b) -> a -> b
$
    [ (String
"time", UTCTime -> JSValue
utcTimeToJSON UTCTime
time)
    , (String
"allocs", Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Integer -> JSValue) -> Integer -> JSValue
forall a b. (a -> b) -> a -> b
$ Statistics -> Integer
statAllocs (Statistics -> Integer) -> Statistics -> Integer
forall a b. (a -> b) -> a -> b
$ Statistics
solverStats )
    , (String
"paths", Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Integer -> JSValue) -> Integer -> JSValue
forall a b. (a -> b) -> a -> b
$ Identity Integer -> Integer
forall a. Identity a -> a
runIdentity (Identity Integer -> Integer) -> Identity Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Metrics Identity -> Identity Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricSplits Metrics Identity
m )
    , (String
"merge-count", Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Integer -> JSValue) -> Integer -> JSValue
forall a b. (a -> b) -> a -> b
$ Identity Integer -> Integer
forall a. Identity a -> a
runIdentity (Identity Integer -> Integer) -> Identity Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Metrics Identity -> Identity Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricMerges Metrics Identity
m )
    , (String
"abort-count", Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Integer -> JSValue) -> Integer -> JSValue
forall a b. (a -> b) -> a -> b
$ Identity Integer -> Integer
forall a. Identity a -> a
runIdentity (Identity Integer -> Integer) -> Identity Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Metrics Identity -> Identity Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricAborts Metrics Identity
m )
    , (String
"non-linear-count", Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Integer -> JSValue) -> Integer -> JSValue
forall a b. (a -> b) -> a -> b
$ Statistics -> Integer
statNonLinearOps (Statistics -> Integer) -> Statistics -> Integer
forall a b. (a -> b) -> a -> b
$ Statistics
solverStats )
    ] [(String, JSValue)] -> [(String, JSValue)] -> [(String, JSValue)]
forall a. [a] -> [a] -> [a]
++ [ (Text -> String
Text.unpack Text
k, Integer -> JSValue
forall a. JSON a => a -> JSValue
showJSON Integer
v)
         | (Text
k, Integer
v) <- Map Text Integer -> [(Text, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Text Integer -> [(Text, Integer)])
-> Map Text Integer -> [(Text, Integer)]
forall a b. (a -> b) -> a -> b
$ Identity (Map Text Integer) -> Map Text Integer
forall a. Identity a -> a
runIdentity (Identity (Map Text Integer) -> Map Text Integer)
-> Identity (Map Text Integer) -> Map Text Integer
forall a b. (a -> b) -> a -> b
$ Metrics Identity -> Identity (Map Text Integer)
forall (f :: Type -> Type). Metrics f -> f (Map Text Integer)
metricExtraMetrics Metrics Identity
m ]
    where
      solverStats :: Statistics
solverStats = Identity Statistics -> Statistics
forall a. Identity a -> a
runIdentity (Identity Statistics -> Statistics)
-> Identity Statistics -> Statistics
forall a b. (a -> b) -> a -> b
$ Metrics Identity -> Identity Statistics
forall (f :: Type -> Type). Metrics f -> f Statistics
metricSolverStats Metrics Identity
m


data CGEventType = ENTER | EXIT | BLOCK | BRANCH
 deriving (Int -> CGEventType -> ShowS
[CGEventType] -> ShowS
CGEventType -> String
(Int -> CGEventType -> ShowS)
-> (CGEventType -> String)
-> ([CGEventType] -> ShowS)
-> Show CGEventType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CGEventType -> ShowS
showsPrec :: Int -> CGEventType -> ShowS
$cshow :: CGEventType -> String
show :: CGEventType -> String
$cshowList :: [CGEventType] -> ShowS
showList :: [CGEventType] -> ShowS
Show,CGEventType -> CGEventType -> Bool
(CGEventType -> CGEventType -> Bool)
-> (CGEventType -> CGEventType -> Bool) -> Eq CGEventType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CGEventType -> CGEventType -> Bool
== :: CGEventType -> CGEventType -> Bool
$c/= :: CGEventType -> CGEventType -> Bool
/= :: CGEventType -> CGEventType -> Bool
Eq,Eq CGEventType
Eq CGEventType =>
(CGEventType -> CGEventType -> Ordering)
-> (CGEventType -> CGEventType -> Bool)
-> (CGEventType -> CGEventType -> Bool)
-> (CGEventType -> CGEventType -> Bool)
-> (CGEventType -> CGEventType -> Bool)
-> (CGEventType -> CGEventType -> CGEventType)
-> (CGEventType -> CGEventType -> CGEventType)
-> Ord CGEventType
CGEventType -> CGEventType -> Bool
CGEventType -> CGEventType -> Ordering
CGEventType -> CGEventType -> CGEventType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CGEventType -> CGEventType -> Ordering
compare :: CGEventType -> CGEventType -> Ordering
$c< :: CGEventType -> CGEventType -> Bool
< :: CGEventType -> CGEventType -> Bool
$c<= :: CGEventType -> CGEventType -> Bool
<= :: CGEventType -> CGEventType -> Bool
$c> :: CGEventType -> CGEventType -> Bool
> :: CGEventType -> CGEventType -> Bool
$c>= :: CGEventType -> CGEventType -> Bool
>= :: CGEventType -> CGEventType -> Bool
$cmax :: CGEventType -> CGEventType -> CGEventType
max :: CGEventType -> CGEventType -> CGEventType
$cmin :: CGEventType -> CGEventType -> CGEventType
min :: CGEventType -> CGEventType -> CGEventType
Ord,(forall x. CGEventType -> Rep CGEventType x)
-> (forall x. Rep CGEventType x -> CGEventType)
-> Generic CGEventType
forall x. Rep CGEventType x -> CGEventType
forall x. CGEventType -> Rep CGEventType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CGEventType -> Rep CGEventType x
from :: forall x. CGEventType -> Rep CGEventType x
$cto :: forall x. Rep CGEventType x -> CGEventType
to :: forall x. Rep CGEventType x -> CGEventType
Generic)

data CGEvent =
  CGEvent
  { CGEvent -> FunctionName
cgEvent_fnName   :: FunctionName
  , CGEvent -> Maybe Position
cgEvent_source   :: Maybe Position
  , CGEvent -> Maybe Position
cgEvent_callsite :: Maybe Position
  , CGEvent -> CGEventType
cgEvent_type     :: CGEventType
  , CGEvent -> [String]
cgEvent_blocks   :: [String]
  , CGEvent -> Metrics Identity
cgEvent_metrics  :: Metrics Identity
  , CGEvent -> UTCTime
cgEvent_time     :: UTCTime
  , CGEvent -> Integer
cgEvent_id       :: Integer
  }
 deriving (Int -> CGEvent -> ShowS
[CGEvent] -> ShowS
CGEvent -> String
(Int -> CGEvent -> ShowS)
-> (CGEvent -> String) -> ([CGEvent] -> ShowS) -> Show CGEvent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CGEvent -> ShowS
showsPrec :: Int -> CGEvent -> ShowS
$cshow :: CGEvent -> String
show :: CGEvent -> String
$cshowList :: [CGEvent] -> ShowS
showList :: [CGEvent] -> ShowS
Show, (forall x. CGEvent -> Rep CGEvent x)
-> (forall x. Rep CGEvent x -> CGEvent) -> Generic CGEvent
forall x. Rep CGEvent x -> CGEvent
forall x. CGEvent -> Rep CGEvent x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CGEvent -> Rep CGEvent x
from :: forall x. CGEvent -> Rep CGEvent x
$cto :: forall x. Rep CGEvent x -> CGEvent
to :: forall x. Rep CGEvent x -> CGEvent
Generic)

-- FIXME... figure out why the UI seems to want this in milliseconds...
utcTimeToJSON :: UTCTime -> JSValue
utcTimeToJSON :: UTCTime -> JSValue
utcTimeToJSON UTCTime
t =
  Double -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Double
1e3 Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational (Rational -> Double) -> Rational -> Double
forall a b. (a -> b) -> a -> b
$ POSIXTime -> Rational
forall a. Real a => a -> Rational
toRational (POSIXTime -> Rational) -> POSIXTime -> Rational
forall a b. (a -> b) -> a -> b
$ UTCTime -> POSIXTime
utcTimeToPOSIXSeconds UTCTime
t) :: Double)

cgEventTypeToJSON :: CGEventType -> JSValue
cgEventTypeToJSON :: CGEventType -> JSValue
cgEventTypeToJSON CGEventType
ENTER = String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"ENTER"
cgEventTypeToJSON CGEventType
EXIT  = String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"EXIT"
cgEventTypeToJSON CGEventType
BLOCK  = String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"BLOCK"
cgEventTypeToJSON CGEventType
BRANCH  = String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"BRANCH"

cgEventToJSON :: CGEvent -> JSValue
cgEventToJSON :: CGEvent -> JSValue
cgEventToJSON CGEvent
ev = JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject ([(String, JSValue)] -> JSObject JSValue)
-> [(String, JSValue)] -> JSObject JSValue
forall a b. (a -> b) -> a -> b
$
    [ (String
"function", Text -> JSValue
forall a. JSON a => a -> JSValue
showJSON (Text -> JSValue) -> Text -> JSValue
forall a b. (a -> b) -> a -> b
$ FunctionName -> Text
functionName (FunctionName -> Text) -> FunctionName -> Text
forall a b. (a -> b) -> a -> b
$ CGEvent -> FunctionName
cgEvent_fnName CGEvent
ev)
    , (String
"type", CGEventType -> JSValue
cgEventTypeToJSON (CGEvent -> CGEventType
cgEvent_type CGEvent
ev))
    , (String
"metrics", Metrics Identity -> UTCTime -> JSValue
metricsToJSON (CGEvent -> Metrics Identity
cgEvent_metrics CGEvent
ev) (CGEvent -> UTCTime
cgEvent_time CGEvent
ev))
    ]
    [(String, JSValue)] -> [(String, JSValue)] -> [(String, JSValue)]
forall a. [a] -> [a] -> [a]
++
    (case CGEvent -> Maybe Position
cgEvent_source CGEvent
ev of
      Maybe Position
Nothing -> []
      Just Position
p -> [(String
"source", Position -> JSValue
positionToJSON Position
p)])
    [(String, JSValue)] -> [(String, JSValue)] -> [(String, JSValue)]
forall a. [a] -> [a] -> [a]
++
    (case CGEvent -> Maybe Position
cgEvent_callsite CGEvent
ev of
      Maybe Position
Nothing -> []
      Just Position
p -> [(String
"callsite", Position -> JSValue
positionToJSON Position
p)])
    [(String, JSValue)] -> [(String, JSValue)] -> [(String, JSValue)]
forall a. [a] -> [a] -> [a]
++
    (case CGEvent -> [String]
cgEvent_blocks CGEvent
ev of
      [] -> []
      [String]
xs -> [(String
"blocks", [String] -> JSValue
forall a. JSON a => a -> JSValue
showJSON [String]
xs)])

positionToJSON :: Position -> JSValue
positionToJSON :: Position -> JSValue
positionToJSON Position
p = String -> JSValue
forall a. JSON a => a -> JSValue
showJSON (String -> JSValue) -> String -> JSValue
forall a b. (a -> b) -> a -> b
$ Position -> String
forall a. Show a => a -> String
show (Position -> String) -> Position -> String
forall a b. (a -> b) -> a -> b
$ Position
p

solverEventToJSON :: (UTCTime, SolverEvent) -> JSValue
solverEventToJSON :: (UTCTime, SolverEvent) -> JSValue
solverEventToJSON (UTCTime
time, SolverEvent
ev) =
   case SolverEvent
ev of
     SolverStartSATQuery SolverStartSATQuery
ssq -> UTCTime -> SolverStartSATQuery -> JSValue
startSATQueryToJSON UTCTime
time SolverStartSATQuery
ssq
     SolverEndSATQuery SolverEndSATQuery
esq -> UTCTime -> SolverEndSATQuery -> JSValue
endSATQueryToJSON UTCTime
time SolverEndSATQuery
esq

startSATQueryToJSON :: UTCTime -> SolverStartSATQuery -> JSValue
startSATQueryToJSON :: UTCTime -> SolverStartSATQuery -> JSValue
startSATQueryToJSON UTCTime
time SolverStartSATQuery
ssq = JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject
  [ (String
"type", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"start")
  , (String
"time", UTCTime -> JSValue
utcTimeToJSON UTCTime
time)
  , (String
"part", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"solver")
  , (String
"solver", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON (String -> JSValue) -> String -> JSValue
forall a b. (a -> b) -> a -> b
$ SolverStartSATQuery -> String
satQuerySolverName SolverStartSATQuery
ssq)
  , (String
"description", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON (String -> JSValue) -> String -> JSValue
forall a b. (a -> b) -> a -> b
$ SolverStartSATQuery -> String
satQueryReason SolverStartSATQuery
ssq)
  ]

endSATQueryToJSON :: UTCTime -> SolverEndSATQuery -> JSValue
endSATQueryToJSON :: UTCTime -> SolverEndSATQuery -> JSValue
endSATQueryToJSON UTCTime
time SolverEndSATQuery
esq = JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject ([(String, JSValue)] -> JSObject JSValue)
-> [(String, JSValue)] -> JSObject JSValue
forall a b. (a -> b) -> a -> b
$
  [ (String
"type", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"finish")
  , (String
"time", UTCTime -> JSValue
utcTimeToJSON UTCTime
time)
  ] [(String, JSValue)] -> [(String, JSValue)] -> [(String, JSValue)]
forall a. [a] -> [a] -> [a]
++
  case (SolverEndSATQuery -> SatResult () ()
satQueryResult SolverEndSATQuery
esq) of
    Sat{} -> [(String
"sat", Bool -> JSValue
forall a. JSON a => a -> JSValue
showJSON Bool
True)]
    Unsat{} -> [(String
"sat", Bool -> JSValue
forall a. JSON a => a -> JSValue
showJSON Bool
False)]
    Unknown{} -> []


callGraphJSON :: UTCTime -> Metrics Identity -> Seq CGEvent -> JSValue
callGraphJSON :: UTCTime -> Metrics Identity -> Seq CGEvent -> JSValue
callGraphJSON UTCTime
now Metrics Identity
m Seq CGEvent
evs = JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject
  [ (String
"type", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"callgraph")
  , (String
"events", [JSValue] -> JSValue
JSArray [JSValue]
allEvs)
  ]

 where
 allEvs :: [JSValue]
allEvs = (CGEvent -> JSValue) -> [CGEvent] -> [JSValue]
forall a b. (a -> b) -> [a] -> [b]
map CGEvent -> JSValue
cgEventToJSON (Seq CGEvent -> [CGEvent]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq CGEvent
evs [CGEvent] -> [CGEvent] -> [CGEvent]
forall a. [a] -> [a] -> [a]
++ UTCTime -> Metrics Identity -> Seq CGEvent -> [CGEvent]
closingEvents UTCTime
now Metrics Identity
m Seq CGEvent
evs)


symProUIString :: String -> String -> ProfilingTable -> IO String
symProUIString :: String -> String -> ProfilingTable -> IO String
symProUIString String
nm String
source ProfilingTable
tbl =
  do JSValue
js <- String -> String -> ProfilingTable -> IO JSValue
symProUIJSON String
nm String
source ProfilingTable
tbl
     String -> IO String
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (String
"data.receiveData("String -> ShowS
forall a. [a] -> [a] -> [a]
++ JSValue -> String
forall a. JSON a => a -> String
encode JSValue
js String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
");")


symProUIJSON :: String -> String -> ProfilingTable -> IO JSValue
symProUIJSON :: String -> String -> ProfilingTable -> IO JSValue
symProUIJSON String
nm String
source ProfilingTable
tbl =
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl
     Seq CGEvent
evs <- IORef (Seq CGEvent) -> IO (Seq CGEvent)
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl)
     Seq (UTCTime, SolverEvent)
solverEvs <- IORef (Seq (UTCTime, SolverEvent))
-> IO (Seq (UTCTime, SolverEvent))
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (Seq (UTCTime, SolverEvent))
solverEvents ProfilingTable
tbl)
     JSValue -> IO JSValue
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (JSValue -> IO JSValue) -> JSValue -> IO JSValue
forall a b. (a -> b) -> a -> b
$ [JSValue] -> JSValue
JSArray ([JSValue] -> JSValue) -> [JSValue] -> JSValue
forall a b. (a -> b) -> a -> b
$
       [ JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject ([(String, JSValue)] -> JSObject JSValue)
-> [(String, JSValue)] -> JSObject JSValue
forall a b. (a -> b) -> a -> b
$ UTCTime -> [(String, JSValue)]
metadata UTCTime
now
       , UTCTime -> Metrics Identity -> Seq CGEvent -> JSValue
callGraphJSON UTCTime
now Metrics Identity
m Seq CGEvent
evs
       , JSObject JSValue -> JSValue
JSObject (JSObject JSValue -> JSValue) -> JSObject JSValue -> JSValue
forall a b. (a -> b) -> a -> b
$ [(String, JSValue)] -> JSObject JSValue
forall a. [(String, a)] -> JSObject a
toJSObject ([(String, JSValue)] -> JSObject JSValue)
-> [(String, JSValue)] -> JSObject JSValue
forall a b. (a -> b) -> a -> b
$ Seq (UTCTime, SolverEvent) -> [(String, JSValue)]
forall {t :: Type -> Type}.
Foldable t =>
t (UTCTime, SolverEvent) -> [(String, JSValue)]
solver_calls Seq (UTCTime, SolverEvent)
solverEvs
       ]
 where
 solver_calls :: t (UTCTime, SolverEvent) -> [(String, JSValue)]
solver_calls t (UTCTime, SolverEvent)
evs  =
   [ (String
"type", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"solver-calls")
   , (String
"events", [JSValue] -> JSValue
JSArray ([JSValue] -> JSValue) -> [JSValue] -> JSValue
forall a b. (a -> b) -> a -> b
$ ((UTCTime, SolverEvent) -> JSValue)
-> [(UTCTime, SolverEvent)] -> [JSValue]
forall a b. (a -> b) -> [a] -> [b]
map (UTCTime, SolverEvent) -> JSValue
solverEventToJSON ([(UTCTime, SolverEvent)] -> [JSValue])
-> [(UTCTime, SolverEvent)] -> [JSValue]
forall a b. (a -> b) -> a -> b
$ t (UTCTime, SolverEvent) -> [(UTCTime, SolverEvent)]
forall a. t a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList t (UTCTime, SolverEvent)
evs)
   ]

 metadata :: UTCTime -> [(String, JSValue)]
metadata UTCTime
now =
   [ (String
"type", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"metadata")
   , (String
"form", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"")
   , (String
"name", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
nm)
   , (String
"source", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
source)
   , (String
"time", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON (String -> JSValue) -> String -> JSValue
forall a b. (a -> b) -> a -> b
$ TimeLocale -> String -> UTCTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
rfc822DateFormat UTCTime
now)
   , (String
"version", String -> JSValue
forall a. JSON a => a -> JSValue
showJSON String
"1")
   ]

data ProfilingTable =
  ProfilingTable
  { ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents :: IORef (Seq CGEvent)
  , ProfilingTable -> IORef (HashSet EventDedup)
eventDedups :: IORef (HashSet EventDedup)
  , ProfilingTable -> Metrics IORef
metrics :: Metrics IORef
  , ProfilingTable -> IORef Integer
eventIDRef :: IORef Integer
  , ProfilingTable -> IORef (Seq (UTCTime, SolverEvent))
solverEvents :: IORef (Seq (UTCTime, SolverEvent))
  }

data EventFilter =
  EventFilter
  { EventFilter -> Bool
recordProfiling :: Bool
  , EventFilter -> Bool
recordCoverage :: Bool
  }

-- | An `EventFilter` that enables only Crucible profiling.
profilingEventFilter :: EventFilter
profilingEventFilter :: EventFilter
profilingEventFilter = EventFilter
  { recordProfiling :: Bool
recordProfiling = Bool
True
  , recordCoverage :: Bool
recordCoverage = Bool
False
  }

data CrucibleProfile =
  CrucibleProfile
  { CrucibleProfile -> UTCTime
crucibleProfileTime :: UTCTime
  , CrucibleProfile -> [CGEvent]
crucibleProfileCGEvents :: [CGEvent]
  , CrucibleProfile -> [SolverEvent]
crucibleProfileSolverEvents :: [SolverEvent]
  } deriving (Int -> CrucibleProfile -> ShowS
[CrucibleProfile] -> ShowS
CrucibleProfile -> String
(Int -> CrucibleProfile -> ShowS)
-> (CrucibleProfile -> String)
-> ([CrucibleProfile] -> ShowS)
-> Show CrucibleProfile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CrucibleProfile -> ShowS
showsPrec :: Int -> CrucibleProfile -> ShowS
$cshow :: CrucibleProfile -> String
show :: CrucibleProfile -> String
$cshowList :: [CrucibleProfile] -> ShowS
showList :: [CrucibleProfile] -> ShowS
Show, (forall x. CrucibleProfile -> Rep CrucibleProfile x)
-> (forall x. Rep CrucibleProfile x -> CrucibleProfile)
-> Generic CrucibleProfile
forall x. Rep CrucibleProfile x -> CrucibleProfile
forall x. CrucibleProfile -> Rep CrucibleProfile x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CrucibleProfile -> Rep CrucibleProfile x
from :: forall x. CrucibleProfile -> Rep CrucibleProfile x
$cto :: forall x. Rep CrucibleProfile x -> CrucibleProfile
to :: forall x. Rep CrucibleProfile x -> CrucibleProfile
Generic)

data EventDedup =
    BlockDedup FunctionName String
  | BranchDedup FunctionName [String]
  deriving (EventDedup -> EventDedup -> Bool
(EventDedup -> EventDedup -> Bool)
-> (EventDedup -> EventDedup -> Bool) -> Eq EventDedup
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EventDedup -> EventDedup -> Bool
== :: EventDedup -> EventDedup -> Bool
$c/= :: EventDedup -> EventDedup -> Bool
/= :: EventDedup -> EventDedup -> Bool
Eq, (forall x. EventDedup -> Rep EventDedup x)
-> (forall x. Rep EventDedup x -> EventDedup) -> Generic EventDedup
forall x. Rep EventDedup x -> EventDedup
forall x. EventDedup -> Rep EventDedup x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EventDedup -> Rep EventDedup x
from :: forall x. EventDedup -> Rep EventDedup x
$cto :: forall x. Rep EventDedup x -> EventDedup
to :: forall x. Rep EventDedup x -> EventDedup
Generic)

instance Hashable EventDedup

readProfilingState :: ProfilingTable -> IO (UTCTime, [CGEvent], [(UTCTime, SolverEvent)])
readProfilingState :: ProfilingTable -> IO (UTCTime, [CGEvent], [(UTCTime, SolverEvent)])
readProfilingState ProfilingTable
tbl =
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl
     Seq CGEvent
cgevs <- IORef (Seq CGEvent) -> IO (Seq CGEvent)
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl)
     Seq (UTCTime, SolverEvent)
sevs  <- IORef (Seq (UTCTime, SolverEvent))
-> IO (Seq (UTCTime, SolverEvent))
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (Seq (UTCTime, SolverEvent))
solverEvents ProfilingTable
tbl)
     (UTCTime, [CGEvent], [(UTCTime, SolverEvent)])
-> IO (UTCTime, [CGEvent], [(UTCTime, SolverEvent)])
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (UTCTime
now, Seq CGEvent -> [CGEvent]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq CGEvent
cgevs [CGEvent] -> [CGEvent] -> [CGEvent]
forall a. [a] -> [a] -> [a]
++ UTCTime -> Metrics Identity -> Seq CGEvent -> [CGEvent]
closingEvents UTCTime
now Metrics Identity
m Seq CGEvent
cgevs, Seq (UTCTime, SolverEvent) -> [(UTCTime, SolverEvent)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (UTCTime, SolverEvent)
sevs)

openEventFrames :: Seq CGEvent -> [CGEvent]
openEventFrames :: Seq CGEvent -> [CGEvent]
openEventFrames = [CGEvent] -> Seq CGEvent -> [CGEvent]
go []
 where
 go :: [CGEvent] -> Seq CGEvent -> [CGEvent]
 go :: [CGEvent] -> Seq CGEvent -> [CGEvent]
go [CGEvent]
xs Seq CGEvent
Seq.Empty = [CGEvent]
xs
 go [CGEvent]
xs (CGEvent
e Seq.:<| Seq CGEvent
es) =
   case CGEvent -> CGEventType
cgEvent_type CGEvent
e of
     CGEventType
ENTER -> [CGEvent] -> Seq CGEvent -> [CGEvent]
go (CGEvent
eCGEvent -> [CGEvent] -> [CGEvent]
forall a. a -> [a] -> [a]
:[CGEvent]
xs) Seq CGEvent
es
     CGEventType
EXIT  -> [CGEvent] -> Seq CGEvent -> [CGEvent]
go ([CGEvent] -> [CGEvent]
forall a. HasCallStack => [a] -> [a]
tail [CGEvent]
xs) Seq CGEvent
es
     CGEventType
_     -> [CGEvent] -> Seq CGEvent -> [CGEvent]
go [CGEvent]
xs Seq CGEvent
es

openToCloseEvent :: UTCTime -> Metrics Identity -> CGEvent -> CGEvent
openToCloseEvent :: UTCTime -> Metrics Identity -> CGEvent -> CGEvent
openToCloseEvent UTCTime
now Metrics Identity
m CGEvent
cge =
  CGEvent
cge
  { cgEvent_type = EXIT
  , cgEvent_metrics = m
  , cgEvent_time = now
  }

closingEvents :: UTCTime -> Metrics Identity -> Seq CGEvent -> [CGEvent]
closingEvents :: UTCTime -> Metrics Identity -> Seq CGEvent -> [CGEvent]
closingEvents UTCTime
now Metrics Identity
m = (CGEvent -> CGEvent) -> [CGEvent] -> [CGEvent]
forall a b. (a -> b) -> [a] -> [b]
map (UTCTime -> Metrics Identity -> CGEvent -> CGEvent
openToCloseEvent UTCTime
now Metrics Identity
m) ([CGEvent] -> [CGEvent])
-> (Seq CGEvent -> [CGEvent]) -> Seq CGEvent -> [CGEvent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq CGEvent -> [CGEvent]
openEventFrames

newProfilingTable :: IO ProfilingTable
newProfilingTable :: IO ProfilingTable
newProfilingTable =
  do Metrics IORef
m <- IORef Integer
-> IORef Integer
-> IORef Integer
-> IORef Statistics
-> IORef (Map Text Integer)
-> Metrics IORef
forall (f :: Type -> Type).
f Integer
-> f Integer
-> f Integer
-> f Statistics
-> f (Map Text Integer)
-> Metrics f
Metrics (IORef Integer
 -> IORef Integer
 -> IORef Integer
 -> IORef Statistics
 -> IORef (Map Text Integer)
 -> Metrics IORef)
-> IO (IORef Integer)
-> IO
     (IORef Integer
      -> IORef Integer
      -> IORef Statistics
      -> IORef (Map Text Integer)
      -> Metrics IORef)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0
                  IO
  (IORef Integer
   -> IORef Integer
   -> IORef Statistics
   -> IORef (Map Text Integer)
   -> Metrics IORef)
-> IO (IORef Integer)
-> IO
     (IORef Integer
      -> IORef Statistics -> IORef (Map Text Integer) -> Metrics IORef)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0
                  IO
  (IORef Integer
   -> IORef Statistics -> IORef (Map Text Integer) -> Metrics IORef)
-> IO (IORef Integer)
-> IO
     (IORef Statistics -> IORef (Map Text Integer) -> Metrics IORef)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0
                  IO (IORef Statistics -> IORef (Map Text Integer) -> Metrics IORef)
-> IO (IORef Statistics)
-> IO (IORef (Map Text Integer) -> Metrics IORef)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Statistics -> IO (IORef Statistics)
forall a. a -> IO (IORef a)
newIORef Statistics
zeroStatistics
                  IO (IORef (Map Text Integer) -> Metrics IORef)
-> IO (IORef (Map Text Integer)) -> IO (Metrics IORef)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Map Text Integer -> IO (IORef (Map Text Integer))
forall a. a -> IO (IORef a)
newIORef Map Text Integer
forall k a. Map k a
Map.empty
                        -- TODO: Find the actual custom metrics and
                        -- initialize them to zero.  Needs a change in
                        -- the Crux API; currently 'newProfilingTable'
                        -- is called before the custom metrics are set
                        -- up.  For now, the extra metrics are missing
                        -- from the very earliest events in the log;
                        -- the JS front end works around this by
                        -- assuming that any missing value is a zero.
     IORef (Seq CGEvent)
evs <- Seq CGEvent -> IO (IORef (Seq CGEvent))
forall a. a -> IO (IORef a)
newIORef Seq CGEvent
forall a. Monoid a => a
mempty
     IORef (HashSet EventDedup)
dedups <- HashSet EventDedup -> IO (IORef (HashSet EventDedup))
forall a. a -> IO (IORef a)
newIORef HashSet EventDedup
forall a. Monoid a => a
mempty
     IORef Integer
idref <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0
     IORef (Seq (UTCTime, SolverEvent))
solverevs <- Seq (UTCTime, SolverEvent)
-> IO (IORef (Seq (UTCTime, SolverEvent)))
forall a. a -> IO (IORef a)
newIORef Seq (UTCTime, SolverEvent)
forall a. Monoid a => a
mempty
     let tbl :: ProfilingTable
tbl = IORef (Seq CGEvent)
-> IORef (HashSet EventDedup)
-> Metrics IORef
-> IORef Integer
-> IORef (Seq (UTCTime, SolverEvent))
-> ProfilingTable
ProfilingTable IORef (Seq CGEvent)
evs IORef (HashSet EventDedup)
dedups Metrics IORef
m IORef Integer
idref IORef (Seq (UTCTime, SolverEvent))
solverevs
     ProfilingTable -> IO ProfilingTable
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ProfilingTable
tbl

recordSolverEvent :: ProfilingTable -> SolverEvent -> IO ()
recordSolverEvent :: ProfilingTable -> SolverEvent -> IO ()
recordSolverEvent ProfilingTable
tbl SolverEvent
ev = do
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Seq (UTCTime, SolverEvent)
xs <- IORef (Seq (UTCTime, SolverEvent))
-> IO (Seq (UTCTime, SolverEvent))
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (Seq (UTCTime, SolverEvent))
solverEvents ProfilingTable
tbl)
     IORef (Seq (UTCTime, SolverEvent))
-> Seq (UTCTime, SolverEvent) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (ProfilingTable -> IORef (Seq (UTCTime, SolverEvent))
solverEvents ProfilingTable
tbl) (Seq (UTCTime, SolverEvent)
xs Seq (UTCTime, SolverEvent)
-> (UTCTime, SolverEvent) -> Seq (UTCTime, SolverEvent)
forall a. Seq a -> a -> Seq a
Seq.|> (UTCTime
now,SolverEvent
ev))

startRecordingSolverEvents ::
  IsSymInterface sym =>
  sym ->
  ProfilingTable ->
  IO ()
startRecordingSolverEvents :: forall sym. IsSymInterface sym => sym -> ProfilingTable -> IO ()
startRecordingSolverEvents sym
sym ProfilingTable
tbl =
  sym -> Maybe (SolverEvent -> IO ()) -> IO ()
forall sym.
IsExprBuilder sym =>
sym -> Maybe (SolverEvent -> IO ()) -> IO ()
setSolverLogListener sym
sym ((SolverEvent -> IO ()) -> Maybe (SolverEvent -> IO ())
forall a. a -> Maybe a
Just (ProfilingTable -> SolverEvent -> IO ()
recordSolverEvent ProfilingTable
tbl))

nextEventID :: ProfilingTable -> IO Integer
nextEventID :: ProfilingTable -> IO Integer
nextEventID ProfilingTable
tbl =
  do Integer
i <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef Integer
eventIDRef ProfilingTable
tbl)
     IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (ProfilingTable -> IORef Integer
eventIDRef ProfilingTable
tbl) (Integer -> IO ()) -> Integer -> IO ()
forall a b. (a -> b) -> a -> b
$! (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
     Integer -> IO Integer
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
i

dedupEvent :: ProfilingTable -> EventDedup -> IO () -> IO ()
dedupEvent :: ProfilingTable -> EventDedup -> IO () -> IO ()
dedupEvent ProfilingTable
tbl EventDedup
evt IO ()
f =
  do HashSet EventDedup
seen <- IORef (HashSet EventDedup) -> IO (HashSet EventDedup)
forall a. IORef a -> IO a
readIORef (ProfilingTable -> IORef (HashSet EventDedup)
eventDedups ProfilingTable
tbl)
     Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ EventDedup -> HashSet EventDedup -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member EventDedup
evt HashSet EventDedup
seen) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       do IORef (HashSet EventDedup) -> HashSet EventDedup -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (ProfilingTable -> IORef (HashSet EventDedup)
eventDedups ProfilingTable
tbl) (EventDedup -> HashSet EventDedup -> HashSet EventDedup
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert EventDedup
evt HashSet EventDedup
seen)
          IO ()
f

inProfilingFrame ::
  ProfilingTable ->
  FunctionName ->
  Maybe ProgramLoc ->
  IO a ->
  IO a
inProfilingFrame :: forall a.
ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO a -> IO a
inProfilingFrame ProfilingTable
tbl FunctionName
nm Maybe ProgramLoc
mloc IO a
action =
  IO () -> IO () -> IO a -> IO a
forall a b c. IO a -> IO b -> IO c -> IO c
Ex.bracket_
    (ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
enterEvent ProfilingTable
tbl FunctionName
nm Maybe ProgramLoc
mloc)
    (ProfilingTable -> FunctionName -> IO ()
exitEvent ProfilingTable
tbl FunctionName
nm)
    IO a
action

enterEvent ::
  ProfilingTable ->
  FunctionName ->
  Maybe ProgramLoc ->
  IO ()
enterEvent :: ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
enterEvent ProfilingTable
tbl FunctionName
nm Maybe ProgramLoc
callLoc =
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl
     Integer
i <- ProfilingTable -> IO Integer
nextEventID ProfilingTable
tbl
     let p :: Maybe Position
p = (ProgramLoc -> Position) -> Maybe ProgramLoc -> Maybe Position
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ProgramLoc -> Position
plSourceLoc Maybe ProgramLoc
callLoc
     IORef (Seq CGEvent) -> (Seq CGEvent -> Seq CGEvent) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl) (Seq CGEvent -> CGEvent -> Seq CGEvent
forall a. Seq a -> a -> Seq a
Seq.|> FunctionName
-> Maybe Position
-> Maybe Position
-> CGEventType
-> [String]
-> Metrics Identity
-> UTCTime
-> Integer
-> CGEvent
CGEvent FunctionName
nm Maybe Position
forall a. Maybe a
Nothing Maybe Position
p CGEventType
ENTER [] Metrics Identity
m UTCTime
now Integer
i)

readMetrics :: ProfilingTable -> IO (Metrics Identity)
readMetrics :: ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl = (forall s. IORef s -> IO (Identity s))
-> Metrics IORef -> IO (Metrics Identity)
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
traverseF (Identity s -> IO (Identity s)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Identity s -> IO (Identity s))
-> (s -> Identity s) -> s -> IO (Identity s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Identity s
forall a. a -> Identity a
Identity (s -> IO (Identity s))
-> (IORef s -> IO s) -> IORef s -> IO (Identity s)
forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< IORef s -> IO s
forall a. IORef a -> IO a
readIORef) (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)

exitEvent ::
  ProfilingTable ->
  FunctionName ->
  IO ()
exitEvent :: ProfilingTable -> FunctionName -> IO ()
exitEvent ProfilingTable
tbl FunctionName
nm =
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- (forall s. IORef s -> IO (Identity s))
-> Metrics IORef -> IO (Metrics Identity)
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall s. e s -> m (f s)) -> Metrics e -> m (Metrics f)
traverseF (Identity s -> IO (Identity s)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Identity s -> IO (Identity s))
-> (s -> Identity s) -> s -> IO (Identity s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Identity s
forall a. a -> Identity a
Identity (s -> IO (Identity s))
-> (IORef s -> IO s) -> IORef s -> IO (Identity s)
forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< IORef s -> IO s
forall a. IORef a -> IO a
readIORef) (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)
     Integer
i <- ProfilingTable -> IO Integer
nextEventID ProfilingTable
tbl
     IORef (Seq CGEvent) -> (Seq CGEvent -> Seq CGEvent) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl) (Seq CGEvent -> CGEvent -> Seq CGEvent
forall a. Seq a -> a -> Seq a
Seq.|> FunctionName
-> Maybe Position
-> Maybe Position
-> CGEventType
-> [String]
-> Metrics Identity
-> UTCTime
-> Integer
-> CGEvent
CGEvent FunctionName
nm Maybe Position
forall a. Maybe a
Nothing Maybe Position
forall a. Maybe a
Nothing CGEventType
EXIT [] Metrics Identity
m UTCTime
now Integer
i)

blockEvent ::
  ProfilingTable ->
  FunctionName ->
  Maybe ProgramLoc ->
  Some (BlockID blocks) ->
  IO ()
blockEvent :: forall (blocks :: Ctx (Ctx CrucibleType)).
ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> Some (BlockID blocks)
-> IO ()
blockEvent ProfilingTable
tbl FunctionName
nm Maybe ProgramLoc
callLoc Some (BlockID blocks)
blk =
  ProfilingTable -> EventDedup -> IO () -> IO ()
dedupEvent ProfilingTable
tbl (FunctionName -> String -> EventDedup
BlockDedup FunctionName
nm (Some (BlockID blocks) -> String
forall a. Show a => a -> String
show Some (BlockID blocks)
blk)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl
     Integer
i <- ProfilingTable -> IO Integer
nextEventID ProfilingTable
tbl
     let p :: Maybe Position
p = (ProgramLoc -> Position) -> Maybe ProgramLoc -> Maybe Position
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ProgramLoc -> Position
plSourceLoc Maybe ProgramLoc
callLoc
     IORef (Seq CGEvent) -> (Seq CGEvent -> Seq CGEvent) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl)
       (Seq CGEvent -> CGEvent -> Seq CGEvent
forall a. Seq a -> a -> Seq a
Seq.|> FunctionName
-> Maybe Position
-> Maybe Position
-> CGEventType
-> [String]
-> Metrics Identity
-> UTCTime
-> Integer
-> CGEvent
CGEvent FunctionName
nm Maybe Position
forall a. Maybe a
Nothing Maybe Position
p CGEventType
BLOCK [Some (BlockID blocks) -> String
forall a. Show a => a -> String
show Some (BlockID blocks)
blk] Metrics Identity
m UTCTime
now Integer
i)

branchEvent ::
  ProfilingTable ->
  FunctionName ->
  Maybe ProgramLoc ->
  [Some (BlockID blocks)] ->
  IO ()
branchEvent :: forall (blocks :: Ctx (Ctx CrucibleType)).
ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> [Some (BlockID blocks)]
-> IO ()
branchEvent ProfilingTable
tbl FunctionName
nm Maybe ProgramLoc
callLoc [Some (BlockID blocks)]
blks =
  ProfilingTable -> EventDedup -> IO () -> IO ()
dedupEvent ProfilingTable
tbl (FunctionName -> [String] -> EventDedup
BranchDedup FunctionName
nm ((Some (BlockID blocks) -> String)
-> [Some (BlockID blocks)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Some (BlockID blocks) -> String
forall a. Show a => a -> String
show [Some (BlockID blocks)]
blks)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
  do UTCTime
now <- IO UTCTime
getCurrentTime
     Metrics Identity
m <- ProfilingTable -> IO (Metrics Identity)
readMetrics ProfilingTable
tbl
     Integer
i <- ProfilingTable -> IO Integer
nextEventID ProfilingTable
tbl
     let p :: Maybe Position
p = (ProgramLoc -> Position) -> Maybe ProgramLoc -> Maybe Position
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ProgramLoc -> Position
plSourceLoc Maybe ProgramLoc
callLoc
     IORef (Seq CGEvent) -> (Seq CGEvent -> Seq CGEvent) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (ProfilingTable -> IORef (Seq CGEvent)
callGraphEvents ProfilingTable
tbl)
       (Seq CGEvent -> CGEvent -> Seq CGEvent
forall a. Seq a -> a -> Seq a
Seq.|> FunctionName
-> Maybe Position
-> Maybe Position
-> CGEventType
-> [String]
-> Metrics Identity
-> UTCTime
-> Integer
-> CGEvent
CGEvent FunctionName
nm Maybe Position
forall a. Maybe a
Nothing Maybe Position
p CGEventType
BRANCH ((Some (BlockID blocks) -> String)
-> [Some (BlockID blocks)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Some (BlockID blocks) -> String
forall a. Show a => a -> String
show [Some (BlockID blocks)]
blks) Metrics Identity
m UTCTime
now Integer
i)


updateProfilingTable ::
  IsExprBuilder sym =>
  ProfilingTable ->
  EventFilter ->
  ExecState p sym ext rtp ->
  IO ()
updateProfilingTable :: forall sym p ext rtp.
IsExprBuilder sym =>
ProfilingTable -> EventFilter -> ExecState p sym ext rtp -> IO ()
updateProfilingTable ProfilingTable
tbl EventFilter
filt ExecState p sym ext rtp
exst = do
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (EventFilter -> Bool
recordProfiling EventFilter
filt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let sym :: sym
sym = ExecState p sym ext rtp -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext ExecState p sym ext rtp
exst SimContext p sym ext
-> Getting sym (SimContext p sym ext) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimContext p sym ext) sym
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface
    Statistics
stats <- sym -> IO Statistics
forall sym. IsExprBuilder sym => sym -> IO Statistics
getStatistics sym
sym
    IORef Statistics -> Statistics -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Metrics IORef -> IORef Statistics
forall (f :: Type -> Type). Metrics f -> f Statistics
metricSolverStats (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)) Statistics
stats

    case ExecState p sym ext rtp -> Maybe (SomeSimState p sym ext rtp)
forall p sym ext r.
ExecState p sym ext r -> Maybe (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext rtp
exst of
      Just (SomeSimState SimState p sym ext rtp f args
simst) -> do
        let extraMetrics :: Map Text (Metric p sym ext)
extraMetrics = ExecState p sym ext rtp -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext ExecState p sym ext rtp
exst SimContext p sym ext
-> Getting
     (Map Text (Metric p sym ext))
     (SimContext p sym ext)
     (Map Text (Metric p sym ext))
-> Map Text (Metric p sym ext)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map Text (Metric p sym ext))
  (SimContext p sym ext)
  (Map Text (Metric p sym ext))
forall p sym ext (f :: Type -> Type).
Functor f =>
(Map Text (Metric p sym ext) -> f (Map Text (Metric p sym ext)))
-> SimContext p sym ext -> f (SimContext p sym ext)
profilingMetrics
        Map Text Integer
extraMetricValues <- (Metric p sym ext -> IO Integer)
-> Map Text (Metric p sym ext) -> IO (Map Text Integer)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Map Text a -> f (Map Text b)
traverse (\Metric p sym ext
m -> Metric p sym ext
-> forall rtp f (args :: Maybe (Ctx CrucibleType)).
   SimState p sym ext rtp f args -> IO Integer
forall p sym ext.
Metric p sym ext
-> forall rtp f (args :: Maybe (Ctx CrucibleType)).
   SimState p sym ext rtp f args -> IO Integer
runMetric Metric p sym ext
m SimState p sym ext rtp f args
simst) Map Text (Metric p sym ext)
extraMetrics
        IORef (Map Text Integer) -> Map Text Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Metrics IORef -> IORef (Map Text Integer)
forall (f :: Type -> Type). Metrics f -> f (Map Text Integer)
metricExtraMetrics (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)) Map Text Integer
extraMetricValues
      Maybe (SomeSimState p sym ext rtp)
Nothing ->
        -- We can't poll custom metrics at the VERY beginning or end of
        -- execution because 'ResultState' and 'InitialState' have no
        -- 'SimState' values. This is probably fine---we still get to
        -- poll them before and after the top-level function being
        -- simulated, since it gets a 'CallState' and 'ReturnState' like
        -- any other function.
        () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

    case ExecState p sym ext rtp
exst of
      InitialState SimContext p sym ext
_ SymGlobalState sym
_ AbortHandler p sym ext (RegEntry sym ret)
_ TypeRepr ret
_ ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
_ ->
        ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
enterEvent ProfilingTable
tbl FunctionName
startFunctionName Maybe ProgramLoc
forall a. Maybe a
Nothing
      CallState ReturnHandler ret p sym ext rtp f a
_rh ResolvedCall p sym ext ret
call SimState p sym ext rtp f a
st ->
        ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
enterEvent ProfilingTable
tbl (ResolvedCall p sym ext ret -> FunctionName
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> FunctionName
resolvedCallName ResolvedCall p sym ext ret
call) (SimState p sym ext rtp f a
stSimState p sym ext rtp f a
-> Getting
     (Maybe ProgramLoc) (SimState p sym ext rtp f a) (Maybe ProgramLoc)
-> Maybe ProgramLoc
forall s a. s -> Getting a s a -> a
^.Getting
  (Maybe ProgramLoc) (SimState p sym ext rtp f a) (Maybe ProgramLoc)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(Maybe ProgramLoc -> f2 (Maybe ProgramLoc))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateLocation)
      ReturnState FunctionName
nm ValueFromValue p sym ext rtp ret
_ RegEntry sym ret
_ SimState p sym ext rtp f a
_ ->
        ProfilingTable -> FunctionName -> IO ()
exitEvent ProfilingTable
tbl FunctionName
nm
      TailCallState ValueFromValue p sym ext rtp ret
_ ResolvedCall p sym ext ret
call SimState p sym ext rtp f a
st ->
        do ProfilingTable -> FunctionName -> IO ()
exitEvent ProfilingTable
tbl (SimState p sym ext rtp f a
stSimState p sym ext rtp f a
-> Getting FunctionName (SimState p sym ext rtp f a) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext rtp f a
 -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> SimState p sym ext rtp f a
-> Const FunctionName (SimState p sym ext rtp f a)
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 a
  -> Const FunctionName (ActiveTree p sym ext rtp f a))
 -> SimState p sym ext rtp f a
 -> Const FunctionName (SimState p sym ext rtp f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> ActiveTree p sym ext rtp f a
    -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> Getting FunctionName (SimState p sym ext rtp f a) FunctionName
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext f a -> Const FunctionName (TopFrame sym ext f a))
-> ActiveTree p sym ext rtp f a
-> Const FunctionName (ActiveTree p sym ext rtp f a)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext f a
  -> Const FunctionName (TopFrame sym ext f a))
 -> ActiveTree p sym ext rtp f a
 -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> TopFrame sym ext f a
    -> Const FunctionName (TopFrame sym ext f a))
-> (FunctionName -> Const FunctionName FunctionName)
-> ActiveTree p sym ext rtp f a
-> Const FunctionName (ActiveTree p sym ext rtp f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimFrame sym ext f a -> Const FunctionName (SimFrame sym ext f a))
-> TopFrame sym ext f a
-> Const FunctionName (TopFrame sym ext f a)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((SimFrame sym ext f a
  -> Const FunctionName (SimFrame sym ext f a))
 -> TopFrame sym ext f a
 -> Const FunctionName (TopFrame sym ext f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> SimFrame sym ext f a
    -> Const FunctionName (SimFrame sym ext f a))
-> (FunctionName -> Const FunctionName FunctionName)
-> TopFrame sym ext f a
-> Const FunctionName (TopFrame sym ext f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(FunctionName -> Const FunctionName FunctionName)
-> SimFrame sym ext f a
-> Const FunctionName (SimFrame sym ext f a)
forall sym ext f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(FunctionName -> f2 FunctionName)
-> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)
frameFunctionName)
           ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO ()
enterEvent ProfilingTable
tbl (ResolvedCall p sym ext ret -> FunctionName
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> FunctionName
resolvedCallName ResolvedCall p sym ext ret
call) (SimState p sym ext rtp f a
stSimState p sym ext rtp f a
-> Getting
     (Maybe ProgramLoc) (SimState p sym ext rtp f a) (Maybe ProgramLoc)
-> Maybe ProgramLoc
forall s a. s -> Getting a s a -> a
^.Getting
  (Maybe ProgramLoc) (SimState p sym ext rtp f a) (Maybe ProgramLoc)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(Maybe ProgramLoc -> f2 (Maybe ProgramLoc))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateLocation)
      SymbolicBranchState{} ->
        IORef Integer -> (Integer -> Integer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Metrics IORef -> IORef Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricSplits (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)) Integer -> Integer
forall a. Enum a => a -> a
succ
      AbortState{} ->
        IORef Integer -> (Integer -> Integer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Metrics IORef -> IORef Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricAborts (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)) Integer -> Integer
forall a. Enum a => a -> a
succ
      UnwindCallState ValueFromValue p sym ext rtp r
_ AbortedResult sym ext
_ SimState p sym ext rtp f a
st ->
        ProfilingTable -> FunctionName -> IO ()
exitEvent ProfilingTable
tbl (SimState p sym ext rtp f a
stSimState p sym ext rtp f a
-> Getting FunctionName (SimState p sym ext rtp f a) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext rtp f a
 -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> SimState p sym ext rtp f a
-> Const FunctionName (SimState p sym ext rtp f a)
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 a
  -> Const FunctionName (ActiveTree p sym ext rtp f a))
 -> SimState p sym ext rtp f a
 -> Const FunctionName (SimState p sym ext rtp f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> ActiveTree p sym ext rtp f a
    -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> Getting FunctionName (SimState p sym ext rtp f a) FunctionName
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext f a -> Const FunctionName (TopFrame sym ext f a))
-> ActiveTree p sym ext rtp f a
-> Const FunctionName (ActiveTree p sym ext rtp f a)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext f a
  -> Const FunctionName (TopFrame sym ext f a))
 -> ActiveTree p sym ext rtp f a
 -> Const FunctionName (ActiveTree p sym ext rtp f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> TopFrame sym ext f a
    -> Const FunctionName (TopFrame sym ext f a))
-> (FunctionName -> Const FunctionName FunctionName)
-> ActiveTree p sym ext rtp f a
-> Const FunctionName (ActiveTree p sym ext rtp f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimFrame sym ext f a -> Const FunctionName (SimFrame sym ext f a))
-> TopFrame sym ext f a
-> Const FunctionName (TopFrame sym ext f a)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((SimFrame sym ext f a
  -> Const FunctionName (SimFrame sym ext f a))
 -> TopFrame sym ext f a
 -> Const FunctionName (TopFrame sym ext f a))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> SimFrame sym ext f a
    -> Const FunctionName (SimFrame sym ext f a))
-> (FunctionName -> Const FunctionName FunctionName)
-> TopFrame sym ext f a
-> Const FunctionName (TopFrame sym ext f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(FunctionName -> Const FunctionName FunctionName)
-> SimFrame sym ext f a
-> Const FunctionName (SimFrame sym ext f a)
forall sym ext f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(FunctionName -> f2 FunctionName)
-> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)
frameFunctionName)
      BranchMergeState CrucibleBranchTarget f args
tgt SimState p sym ext rtp f args
st ->
        Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (CrucibleBranchTarget f args
-> SimState p sym ext rtp f args -> Bool
forall f (args :: Maybe (Ctx CrucibleType)) p sym ext root.
CrucibleBranchTarget f args
-> SimState p sym ext root f args -> Bool
isMergeState CrucibleBranchTarget f args
tgt SimState p sym ext rtp f args
st)
             (IORef Integer -> (Integer -> Integer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Metrics IORef -> IORef Integer
forall (f :: Type -> Type). Metrics f -> f Integer
metricMerges (ProfilingTable -> Metrics IORef
metrics ProfilingTable
tbl)) Integer -> Integer
forall a. Enum a => a -> a
succ)
      ExecState p sym ext rtp
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (EventFilter -> Bool
recordCoverage EventFilter
filt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    case ExecState p sym ext rtp
exst of
      ControlTransferState ControlResumption p sym ext rtp f
res SimState p sym ext rtp f ('Just a)
st ->
        let funcName :: FunctionName
funcName = SimState p sym ext rtp f ('Just a)
stSimState p sym ext rtp f ('Just a)
-> Getting
     FunctionName (SimState p sym ext rtp f ('Just a)) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext rtp f ('Just a)
 -> Const FunctionName (ActiveTree p sym ext rtp f ('Just a)))
-> SimState p sym ext rtp f ('Just a)
-> Const FunctionName (SimState p sym ext rtp f ('Just a))
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 a)
  -> Const FunctionName (ActiveTree p sym ext rtp f ('Just a)))
 -> SimState p sym ext rtp f ('Just a)
 -> Const FunctionName (SimState p sym ext rtp f ('Just a)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> ActiveTree p sym ext rtp f ('Just a)
    -> Const FunctionName (ActiveTree p sym ext rtp f ('Just a)))
-> Getting
     FunctionName (SimState p sym ext rtp f ('Just a)) FunctionName
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext f ('Just a)
 -> Const FunctionName (TopFrame sym ext f ('Just a)))
-> ActiveTree p sym ext rtp f ('Just a)
-> Const FunctionName (ActiveTree p sym ext rtp f ('Just a))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext f ('Just a)
  -> Const FunctionName (TopFrame sym ext f ('Just a)))
 -> ActiveTree p sym ext rtp f ('Just a)
 -> Const FunctionName (ActiveTree p sym ext rtp f ('Just a)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> TopFrame sym ext f ('Just a)
    -> Const FunctionName (TopFrame sym ext f ('Just a)))
-> (FunctionName -> Const FunctionName FunctionName)
-> ActiveTree p sym ext rtp f ('Just a)
-> Const FunctionName (ActiveTree p sym ext rtp f ('Just a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimFrame sym ext f ('Just a)
 -> Const FunctionName (SimFrame sym ext f ('Just a)))
-> TopFrame sym ext f ('Just a)
-> Const FunctionName (TopFrame sym ext f ('Just a))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((SimFrame sym ext f ('Just a)
  -> Const FunctionName (SimFrame sym ext f ('Just a)))
 -> TopFrame sym ext f ('Just a)
 -> Const FunctionName (TopFrame sym ext f ('Just a)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> SimFrame sym ext f ('Just a)
    -> Const FunctionName (SimFrame sym ext f ('Just a)))
-> (FunctionName -> Const FunctionName FunctionName)
-> TopFrame sym ext f ('Just a)
-> Const FunctionName (TopFrame sym ext f ('Just a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(FunctionName -> Const FunctionName FunctionName)
-> SimFrame sym ext f ('Just a)
-> Const FunctionName (SimFrame sym ext f ('Just a))
forall sym ext f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(FunctionName -> f2 FunctionName)
-> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)
frameFunctionName in
        case ControlResumption p sym ext rtp f
res of
          ContinueResumption (ResolvedJump BlockID blocks args
blk RegMap sym args
_) ->
            ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> Some (BlockID blocks)
-> IO ()
forall (blocks :: Ctx (Ctx CrucibleType)).
ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> Some (BlockID blocks)
-> IO ()
blockEvent ProfilingTable
tbl FunctionName
funcName (SimState p sym ext rtp f ('Just a)
stSimState p sym ext rtp f ('Just a)
-> Getting
     (Maybe ProgramLoc)
     (SimState p sym ext rtp f ('Just a))
     (Maybe ProgramLoc)
-> Maybe ProgramLoc
forall s a. s -> Getting a s a -> a
^.Getting
  (Maybe ProgramLoc)
  (SimState p sym ext rtp f ('Just a))
  (Maybe ProgramLoc)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(Maybe ProgramLoc -> f2 (Maybe ProgramLoc))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateLocation) (BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks args
blk)
          CheckMergeResumption (ResolvedJump BlockID blocks args
blk RegMap sym args
_) ->
            ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> Some (BlockID blocks)
-> IO ()
forall (blocks :: Ctx (Ctx CrucibleType)).
ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> Some (BlockID blocks)
-> IO ()
blockEvent ProfilingTable
tbl FunctionName
funcName (SimState p sym ext rtp f ('Just a)
stSimState p sym ext rtp f ('Just a)
-> Getting
     (Maybe ProgramLoc)
     (SimState p sym ext rtp f ('Just a))
     (Maybe ProgramLoc)
-> Maybe ProgramLoc
forall s a. s -> Getting a s a -> a
^.Getting
  (Maybe ProgramLoc)
  (SimState p sym ext rtp f ('Just a))
  (Maybe ProgramLoc)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(Maybe ProgramLoc -> f2 (Maybe ProgramLoc))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateLocation) (BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks args
blk)
          ControlResumption p sym ext rtp f
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
      RunningState (RunBlockEnd Some (BlockID blocks)
_) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st ->
        let funcName :: FunctionName
funcName = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
stSimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     FunctionName
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (SimState p sym ext rtp (CrucibleLang blocks r) ('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 (CrucibleLang blocks r) ('Just args)
  -> Const
       FunctionName
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> Const
         FunctionName
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> Getting
     FunctionName
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     FunctionName
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (CrucibleLang blocks r) ('Just args)
  -> Const
       FunctionName
       (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
    -> Const
         FunctionName
         (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> (FunctionName -> Const FunctionName FunctionName)
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((SimFrame sym ext (CrucibleLang blocks r) ('Just args)
  -> Const
       FunctionName
       (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
 -> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      FunctionName
      (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> ((FunctionName -> Const FunctionName FunctionName)
    -> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
    -> Const
         FunctionName
         (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> (FunctionName -> Const FunctionName FunctionName)
-> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(FunctionName -> Const FunctionName FunctionName)
-> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     FunctionName
     (SimFrame sym ext (CrucibleLang blocks r) ('Just args))
forall sym ext f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(FunctionName -> f2 FunctionName)
-> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)
frameFunctionName in
        case SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
stSimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (StmtSeq ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (StmtSeq ext blocks r args)
-> StmtSeq ext blocks r args
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('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 (CrucibleLang blocks r) ('Just args)
  -> Const
       (StmtSeq ext blocks r args)
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((StmtSeq ext blocks r args
     -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> Const
         (StmtSeq ext blocks r args)
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> Getting
     (StmtSeq ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (StmtSeq ext blocks r args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (CrucibleLang blocks r) ('Just args)
  -> Const
       (StmtSeq ext blocks r args)
       (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((StmtSeq ext blocks r args
     -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
    -> Const
         (StmtSeq ext blocks r args)
         (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> (StmtSeq ext blocks r args
    -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((SimFrame sym ext (CrucibleLang blocks r) ('Just args)
  -> Const
       (StmtSeq ext blocks r args)
       (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
 -> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (TopFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> ((StmtSeq ext blocks r args
     -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
    -> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
    -> Const
         (StmtSeq ext blocks r args)
         (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> (StmtSeq ext blocks r args
    -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(CallFrame sym ext blocks r args
 -> Const
      (StmtSeq ext blocks r args) (CallFrame sym ext blocks r args))
-> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (SimFrame sym ext (CrucibleLang blocks r) ('Just args))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType)
       (blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
 -> f (CallFrame sym ext blocks' r' args'))
-> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
-> f (SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
crucibleSimFrame((CallFrame sym ext blocks r args
  -> Const
       (StmtSeq ext blocks r args) (CallFrame sym ext blocks r args))
 -> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
 -> Const
      (StmtSeq ext blocks r args)
      (SimFrame sym ext (CrucibleLang blocks r) ('Just args)))
-> ((StmtSeq ext blocks r args
     -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
    -> CallFrame sym ext blocks r args
    -> Const
         (StmtSeq ext blocks r args) (CallFrame sym ext blocks r args))
-> (StmtSeq ext blocks r args
    -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
-> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
-> Const
     (StmtSeq ext blocks r args)
     (SimFrame sym ext (CrucibleLang blocks r) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(StmtSeq ext blocks r args
 -> Const (StmtSeq ext blocks r args) (StmtSeq ext blocks r args))
-> CallFrame sym ext blocks r args
-> Const
     (StmtSeq ext blocks r args) (CallFrame sym ext blocks r args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts of
          TermStmt ProgramLoc
loc TermStmt blocks r args
term
            | Just [Some (BlockID blocks)]
blocks <- TermStmt blocks r args -> Maybe [Some (BlockID blocks)]
forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks TermStmt blocks r args
term,
              [Some (BlockID blocks)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (BlockID blocks)]
blocks Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 ->
                ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> [Some (BlockID blocks)]
-> IO ()
forall (blocks :: Ctx (Ctx CrucibleType)).
ProfilingTable
-> FunctionName
-> Maybe ProgramLoc
-> [Some (BlockID blocks)]
-> IO ()
branchEvent ProfilingTable
tbl FunctionName
funcName (ProgramLoc -> Maybe ProgramLoc
forall a. a -> Maybe a
Just ProgramLoc
loc) [Some (BlockID blocks)]
blocks
          StmtSeq ext blocks r args
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
      ExecState p sym ext rtp
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

isMergeState ::
  CrucibleBranchTarget f args ->
  SimState p sym ext root f args ->
  Bool
isMergeState :: forall f (args :: Maybe (Ctx CrucibleType)) p sym ext root.
CrucibleBranchTarget f args
-> SimState p sym ext root f args -> Bool
isMergeState CrucibleBranchTarget f args
tgt SimState p sym ext root f args
st =
  case SimState p sym ext root f args
stSimState p sym ext root f args
-> Getting
     (ValueFromFrame p sym ext root f)
     (SimState p sym ext root f args)
     (ValueFromFrame p sym ext root f)
-> ValueFromFrame p sym ext root f
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext root f args
 -> Const
      (ValueFromFrame p sym ext root f)
      (ActiveTree p sym ext root f args))
-> SimState p sym ext root f args
-> Const
     (ValueFromFrame p sym ext root f) (SimState p sym ext root f 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 root f args
  -> Const
       (ValueFromFrame p sym ext root f)
       (ActiveTree p sym ext root f args))
 -> SimState p sym ext root f args
 -> Const
      (ValueFromFrame p sym ext root f) (SimState p sym ext root f args))
-> ((ValueFromFrame p sym ext root f
     -> Const
          (ValueFromFrame p sym ext root f)
          (ValueFromFrame p sym ext root f))
    -> ActiveTree p sym ext root f args
    -> Const
         (ValueFromFrame p sym ext root f)
         (ActiveTree p sym ext root f args))
-> Getting
     (ValueFromFrame p sym ext root f)
     (SimState p sym ext root f args)
     (ValueFromFrame p sym ext root f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(ValueFromFrame p sym ext root f
 -> Const
      (ValueFromFrame p sym ext root f)
      (ValueFromFrame p sym ext root f))
-> ActiveTree p sym ext root f args
-> Const
     (ValueFromFrame p sym ext root f)
     (ActiveTree p sym ext root f 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 of
    VFFBranch ValueFromFrame p sym ext root f
_ctx FrameIdentifier
_assume_frame ProgramLoc
_loc Pred sym
_p VFFOtherPath p sym ext root f args
other_branch CrucibleBranchTarget f args
tgt'
      | Just args :~: args
Refl <- CrucibleBranchTarget f args
-> CrucibleBranchTarget f args -> Maybe (args :~: args)
forall (a :: Maybe (Ctx CrucibleType))
       (b :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f a
-> CrucibleBranchTarget f b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality CrucibleBranchTarget f args
tgt CrucibleBranchTarget f args
tgt' ->
          case VFFOtherPath p sym ext root f args
other_branch of
            VFFActivePath{} -> Bool
False
            VFFCompletePath{} -> Bool
True
    VFFPartial ValueFromFrame p sym ext root f
_ctx ProgramLoc
_loc Pred sym
_p AbortedResult sym ext
_ar PendingPartialMerges
NeedsToBeAborted -> Bool
True
    ValueFromFrame p sym ext root f
_ -> Bool
False


data ProfilingOptions =
  ProfilingOptions
  { ProfilingOptions -> POSIXTime
periodicProfileInterval :: NominalDiffTime
  , ProfilingOptions -> ProfilingTable -> IO ()
periodicProfileAction   :: ProfilingTable -> IO ()
  }


-- | Write a profiling report file in the JS/JSON format expected by tye symProUI front end.
writeProfileReport ::
  FilePath {- ^ File to write -} ->
  String {- ^ "name" for the report -} ->
  String {- ^ "source" for the report -} ->
  ProfilingTable {- ^ profiling data to populate the report -} ->
  IO ()
writeProfileReport :: String -> String -> String -> ProfilingTable -> IO ()
writeProfileReport String
fp String
name String
source ProfilingTable
tbl =
   String -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. String -> IOMode -> (Handle -> IO r) -> IO r
withFile String
fp IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> Handle -> String -> IO ()
hPutStrLn Handle
h (String -> IO ()) -> IO String -> IO ()
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> String -> ProfilingTable -> IO String
symProUIString String
name String
source ProfilingTable
tbl

-- | 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.
profilingFeature ::
  ProfilingTable ->
  EventFilter ->
  Maybe ProfilingOptions ->
  IO (GenericExecutionFeature sym)

profilingFeature :: forall sym.
ProfilingTable
-> EventFilter
-> Maybe ProfilingOptions
-> IO (GenericExecutionFeature sym)
profilingFeature ProfilingTable
tbl EventFilter
filt Maybe ProfilingOptions
Nothing =
  GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GenericExecutionFeature sym -> IO (GenericExecutionFeature sym))
-> GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a b. (a -> b) -> a -> b
$ (forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall sym.
(forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
GenericExecutionFeature ((forall p ext rtp.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> GenericExecutionFeature sym)
-> (forall p ext rtp.
    (IsSymInterface sym, IsSyntaxExtension ext) =>
    ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext rtp
exst -> ProfilingTable -> EventFilter -> ExecState p sym ext rtp -> IO ()
forall sym p ext rtp.
IsExprBuilder sym =>
ProfilingTable -> EventFilter -> ExecState p sym ext rtp -> IO ()
updateProfilingTable ProfilingTable
tbl EventFilter
filt ExecState p sym ext rtp
exst IO ()
-> IO (ExecutionFeatureResult p sym ext rtp)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. IO a -> IO b -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> 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

profilingFeature ProfilingTable
tbl EventFilter
filt (Just ProfilingOptions
profOpts) =
  do UTCTime
startTime <- IO UTCTime
getCurrentTime
     IORef UTCTime
stateRef <- UTCTime -> IO (IORef UTCTime)
forall a. a -> IO (IORef a)
newIORef (UTCTime -> UTCTime
computeNextState UTCTime
startTime)
     GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IORef UTCTime -> GenericExecutionFeature sym
feat IORef UTCTime
stateRef)

 where
 feat :: IORef UTCTime -> GenericExecutionFeature sym
feat IORef UTCTime
stateRef = (forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall sym.
(forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
GenericExecutionFeature ((forall p ext rtp.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> GenericExecutionFeature sym)
-> (forall p ext rtp.
    (IsSymInterface sym, IsSyntaxExtension ext) =>
    ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext rtp
exst ->
        do ProfilingTable -> EventFilter -> ExecState p sym ext rtp -> IO ()
forall sym p ext rtp.
IsExprBuilder sym =>
ProfilingTable -> EventFilter -> ExecState p sym ext rtp -> IO ()
updateProfilingTable ProfilingTable
tbl EventFilter
filt ExecState p sym ext rtp
exst
           UTCTime
deadline <- IORef UTCTime -> IO UTCTime
forall a. IORef a -> IO a
readIORef IORef UTCTime
stateRef
           UTCTime
now <- IO UTCTime
getCurrentTime
           if UTCTime
deadline UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
now then
             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
           else
             do ProfilingOptions -> ProfilingTable -> IO ()
periodicProfileAction ProfilingOptions
profOpts ProfilingTable
tbl
                IORef UTCTime -> UTCTime -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef UTCTime
stateRef (UTCTime -> UTCTime
computeNextState UTCTime
now)
                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

 computeNextState :: UTCTime -> UTCTime
 computeNextState :: UTCTime -> UTCTime
computeNextState UTCTime
lastOutputTime = POSIXTime -> UTCTime -> UTCTime
addUTCTime (ProfilingOptions -> POSIXTime
periodicProfileInterval ProfilingOptions
profOpts) UTCTime
lastOutputTime