Hotfix more logging tweaks (#3954)

* include `hook <NAME>` log contexts in `-l Simplify` and `-l SimplifySuccess` * log timing statistics with a log context `proxy,timing` <summary> Example JSON output for `--log-context proxy` <details> ``` {"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""} {"context":["proxy"],"message":"Starting RPC server"} {"context":["proxy"],"message":"Processing request 4"} {"context":["proxy"],"message":"Starting execute request"} {"context":["proxy"],"message":"Booster Aborted at Depth {getNat = 10}"} {"context":["proxy"],"message":"Simplifying booster state and falling back to Kore"} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":34017.38,"method":"SimplifyM","time":43152.727999999996}} {"context":["proxy"],"message":"Executing fall-back request"} {"context":["proxy","timing","kore"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":37633.786}} {"context":["proxy","abort"],"message":"Booster aborted, kore yields Branching"} {"context":["proxy"],"message":"Kore Branching at Depth {getNat = 0}"} {"context":["proxy"],"message":"Simplifying state in Branching result"} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":33663.381,"method":"SimplifyM","time":43049.642}} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":33558.555,"method":"SimplifyM","time":42640.443}} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":34078.823,"method":"SimplifyM","time":43215.810999999994}} {"context":["proxy","abort","detail"],"message":"Kore simplification: Diff (< before - > after)\n<syntactic difference only>"} {"context":["proxy","timing"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":51747.152}} {"context":["proxy"],"message":"Server shutting down"} {"context":["proxy","timing"],"message":[["ExecuteM",{"average":51747.152,"count":1,"kore-average":37633.786,"kore-max":37633.786,"kore-total":37633.786,"max-val":51747.152,"min-val":51747.152,"stddev":0,"total":51747.152}],["SimplifyM",{"average":43014.655999999995,"count":4,"kore-average":33829.53475,"kore-max":34078.823,"kore-total":135318.139,"max-val":43215.810999999994,"min-val":42640.443,"stddev":224.0460894407471,"total":172058.62399999998}]]} ``` </details> Example text output: (as before) <details> ``` [proxy] Processing request 4 [proxy] Starting execute request [proxy] Booster Aborted at Depth {getNat = 10} [proxy] Simplifying booster state and falling back to Kore [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.907ms (33.585ms kore time) [proxy] Executing fall-back request [proxy][timing][kore] Kore fall-back in 37.303ms [proxy][abort] Booster aborted, kore yields Branching [proxy] Kore Branching at Depth {getNat = 0} [proxy] Simplifying state in Branching result [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.253ms (32.774ms kore time) [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 41.732ms (32.446ms kore time) [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.379ms (33.301ms kore time) [proxy][abort][detail] Kore simplification: Diff (< before - > after) <syntactic difference only> [proxy][timing] Performed ExecuteM in 50.100ms (37.303ms kore time) [proxy] Server shutting down [proxy][timing] --------------------------- RPC request time statistics --------------------------- ExecuteM: Requests: 1 Total time: 50.100ms Average time per request: 50.100ms (+- 0.0μs), range [50.100ms, 50.100ms] Total time in kore-rpc code: 37.303ms Average time per request in kore-rpc code: 37.303ms, max 37.303ms SimplifyM: Requests: 4 Total time: 0.17s Average time per request: 42.318ms (+- 0.418ms), range [41.732ms, 42.907ms] Total time in kore-rpc code: 0.13s Average time per request in kore-rpc code: 33.027ms, max 33.585ms ``` </details> </summary> --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · Jun 21, 2024 · ac6c535 · ac6c535
1 parent fb59a84
commit ac6c535
Show file tree

Hide file tree

Showing 8 changed files with 91 additions and 37 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs
@@ -244,14 +244,14 @@ levelToContext =
         [
             ( "Simplify"
             ,
-                [ [ctxt| booster|kore>function*|simplification*,success|failure|abort|detail |]
+                [ [ctxt| booster|kore>function*|simplification*|hook*,success|failure|abort|detail |]
                 , [ctxt| booster|kore>function*|simplification*,match,failure|abort |]
                 ]
             )
         ,
             ( "SimplifySuccess"
             ,
-                [ [ctxt| booster|kore>function*|simplification*,success|detail |]
+                [ [ctxt| booster|kore>function*|simplification*|hook*,success|detail |]
                 ]
             )
         ,

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
@@ -19,6 +19,7 @@ module Booster.Log (
     jsonLogger,
     textLogger,
     withContext,
+    withContexts,
     withKorePatternContext,
     withPatternContext,
     withRuleContext,
@@ -83,6 +84,10 @@ instance ToLogFormat Text where
     toTextualLog t = t
     toJSONLog t = String t
 
+instance ToLogFormat String where
+    toTextualLog = pack
+    toJSONLog = String . pack
+
 instance ToLogFormat Term where
     toTextualLog t = renderOneLineText $ pretty t
     toJSONLog t = toJSON $ addHeader $ externaliseTerm t
@@ -141,6 +146,10 @@ logPretty = logMessage . renderOneLineText . pretty
 withContext :: LoggerMIO m => SimpleContext -> m a -> m a
 withContext c = withContext_ (CLNullary c)
 
+withContexts :: LoggerMIO m => [SimpleContext] -> m a -> m a
+withContexts [] m = m
+withContexts cs m = foldr withContext m cs
+
 withContext_ :: LoggerMIO m => CLContext -> m a -> m a
 withContext_ c =
     withLogger

diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
diff --git a/booster/test/rpc-integration/test-log-simplify-json/test.sh b/booster/test/rpc-integration/test-log-simplify-json/test.sh
@@ -8,7 +8,7 @@ echo "client=$client"
 echo "dir=$dir"
 echo "arguments=$*"
 
-diff="git diff --no-index"
+diff="git --no-pager diff --no-index"
 # remove "--regenerate" and tweak $diff if it is present
 
 regenerate () {

diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs
@@ -49,7 +49,7 @@ import Kore.Log qualified
 import Kore.Syntax.Definition (SentenceAxiom)
 import Kore.Syntax.Json.Types qualified as KoreJson
 import SMT qualified
-import Stats (StatsVar, addStats, microsWithUnit, timed)
+import Stats (MethodTiming (..), StatsVar, addStats, microsWithUnit, timed)
 
 data KoreServer = KoreServer
     { serverState :: MVar.MVar Kore.ServerState
@@ -64,7 +64,7 @@ data KoreServer = KoreServer
     }
 
 data ProxyConfig = ProxyConfig
-    { statsVar :: Maybe StatsVar
+    { statsVar :: StatsVar
     , forceFallback :: Maybe Depth
     , boosterState :: MVar.MVar Booster.ServerState
     , fallbackReasons :: [HaltReason]
@@ -83,7 +83,7 @@ respondEither ::
     Respond (API 'Req) m (API 'Res) ->
     Respond (API 'Req) m (API 'Res) ->
     Respond (API 'Req) m (API 'Res)
-respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case req of
+respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
     Execute execReq
         | isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout ->
             loggedKore ExecuteM req
@@ -252,21 +252,10 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
         logStats method (time, time)
         pure result
 
-    logStats method (time, koreTime)
-        | Just v <- statsVar = do
-            addStats v method time koreTime
-            Booster.Log.withContext CtxProxy $
-                Booster.Log.logMessage' $
-                    Text.pack $
-                        unwords
-                            [ "Performed"
-                            , show method
-                            , "in"
-                            , microsWithUnit time
-                            , "(" <> microsWithUnit koreTime <> " kore time)"
-                            ]
-        | otherwise =
-            pure ()
+    logStats method (time, koreTime) = do
+        let timing = MethodTiming{method, time, koreTime}
+        addStats cfg.statsVar timing
+        Booster.Log.withContexts [CtxProxy, CtxTiming] $ Booster.Log.logMessage timing
 
     handleExecute ::
         LogSettings ->
@@ -397,11 +386,17 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 , assumeStateDefined = Just True
                                                 }
                                         )
-                            when (isJust statsVar) $ do
-                                Booster.Log.withContext CtxProxy $
-                                    Booster.Log.logMessage $
-                                        Text.pack $
-                                            "Kore fall-back in " <> microsWithUnit kTime
+                            Booster.Log.withContexts [CtxProxy, CtxTiming, CtxKore] $
+                                Booster.Log.logMessage $
+                                    WithJsonMessage
+                                        ( toJSON
+                                            MethodTiming
+                                                { method = ExecuteM
+                                                , time = kTime
+                                                , koreTime = kTime
+                                                }
+                                        )
+                                        ("Kore fall-back in " <> microsWithUnit kTime)
                             case kResult of
                                 Right (Execute koreResult) -> do
                                     let

diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE QuasiQuotes #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 
 {- |
@@ -13,7 +14,6 @@ import Control.DeepSeq (force)
 import Control.Exception (AsyncException (UserInterrupt), evaluate, handleJust)
 import Control.Monad (forM_, unless, void)
 import Control.Monad.Catch (bracket)
-import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class (MonadIO (liftIO))
 import Control.Monad.Logger (
     LogLevel (..),
@@ -58,7 +58,7 @@ import Booster.GlobalState
 import Booster.JsonRpc qualified as Booster
 import Booster.LLVM.Internal (mkAPI, withDLib)
 import Booster.Log hiding (withLogger)
-import Booster.Log.Context qualified
+import Booster.Log.Context qualified as Ctxt
 import Booster.Pattern.Base (Predicate (..))
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..))
@@ -149,6 +149,7 @@ main = do
         logContextsWithcustomLevelContexts =
             logContexts
                 <> concatMap (\case LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels
+                <> [[Ctxt.ctxt| *>timing |] | printStats]
         contextLoggingEnabled = not (null logContextsWithcustomLevelContexts)
         koreSolverOptions = translateSMTOpts smtOptions
         timestampFlag = case timeStampsFormat of
@@ -177,7 +178,7 @@ main = do
                                     ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
                                     )
                                     ctxt
-                          in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts
+                          in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts
                        )
 
             koreLogEntries =
@@ -194,7 +195,7 @@ main = do
                 flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) ->
                     alwaysDisplay
                         || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts
-                            in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts
+                            in any (flip Ctxt.mustMatch ctxt) logContextsWithcustomLevelContexts
 
             runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a
             runBoosterLogger = flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT
@@ -303,7 +304,7 @@ main = do
                                 , mSMTOptions = if boosterSMT then smtOptions else Nothing
                                 , addedModules = mempty
                                 }
-                statsVar <- if printStats then Just <$> Stats.newStats else pure Nothing
+                statsVar <- Stats.newStats
 
                 writeGlobalEquationOptions equationOptions
 
@@ -343,8 +344,9 @@ main = do
                     interruptHandler _ =
                         runBoosterLogger . Booster.Log.withContext CtxProxy $ do
                             Booster.Log.logMessage' @_ @Text "Server shutting down"
-                            whenJust statsVar $ \var ->
-                                liftIO (Stats.finaliseStats var) >>= Booster.Log.logMessage'
+                            ( liftIO (Stats.finaliseStats statsVar)
+                                    >>= Booster.Log.withContext CtxTiming . Booster.Log.logMessage
+                                )
                             liftIO exitSuccess
                 handleJust isInterrupt interruptHandler $ runBoosterLogger server
   where

diff --git a/booster/tools/booster/Stats.hs b/booster/tools/booster/Stats.hs
@@ -6,13 +6,15 @@ module Stats (
     microsWithUnit,
     RequestStats (..),
     StatsVar,
+    MethodTiming (..),
 ) where
 
 import Control.Concurrent.MVar (MVar, modifyMVar_, newMVar, readMVar)
 import Control.Monad.IO.Class (MonadIO (liftIO))
 import Data.Aeson
 import Data.Map (Map)
 import Data.Map qualified as Map
+import Data.Text (pack)
 import Deriving.Aeson
 import GHC.Generics ()
 import Prettyprinter
@@ -108,14 +110,29 @@ singleStats' x korePart =
 
 type StatsVar = MVar (Map APIMethod (Stats' Double))
 
+-- helper type mainly for json logging
+data MethodTiming a = MethodTiming {method :: APIMethod, time :: a, koreTime :: a}
+    deriving stock (Eq, Show, Generic)
+    deriving
+        (ToJSON, FromJSON)
+        via CustomJSON '[FieldLabelModifier '[CamelToKebab]] (MethodTiming a)
+
+instance ToLogFormat (MethodTiming Double) where
+    toTextualLog mt =
+        pack $
+            printf
+                "Performed %s in %s (%s kore time)"
+                (show mt.method)
+                (microsWithUnit mt.time)
+                (microsWithUnit mt.koreTime)
+    toJSONLog = toJSON
+
 addStats ::
     MonadIO m =>
     MVar (Map APIMethod (Stats' Double)) ->
-    APIMethod ->
-    Double ->
-    Double ->
+    MethodTiming Double ->
     m ()
-addStats statVar method time koreTime =
+addStats statVar MethodTiming{method, time, koreTime} =
     liftIO . modifyMVar_ statVar $
         pure . Map.insertWith (<>) method (singleStats' time koreTime)
 

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -47,6 +47,7 @@ data SimpleContext
     | CtxDetail
     | CtxSubstitution
     | CtxDepth
+    | CtxTiming
     | -- standard log levels
       CtxError
     | CtxWarn