Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

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 |]
                 ]
             )
         ,

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

booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden

@@ -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 () {

booster/test/rpc-integration/test-log-simplify-json/test.sh

@@ -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

booster/tools/booster/Proxy.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

booster/tools/booster/Server.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)
 

booster/tools/booster/Stats.hs

@@ -47,6 +47,7 @@ data SimpleContext
     | CtxDetail
     | CtxSubstitution
     | CtxDepth
+    | CtxTiming
     | -- standard log levels
       CtxError
     | CtxWarn