Add JSON logging to Kore (#3824)

Fixes #3817
Fixes #3815

* the `Entry` type class gets a new `oneLineJson` method. Log entries
will now need to implement this method if they are to be logged as JSON.
The default implementation if just the type constructor name.
* The `DebugAttemptEquation` log entry gets an a `oneLineJson`
implementation that serialised the successful/failed equation
applications in the same form as the Booster, i.e. following the RPC log
format. The terms are not included to keep the log size manageable.
* The `LogSomeAction` constructor of the `LogType` (a filed of
`KoreLogOptions`) is repurposed. Instead of holding one log action, it
now holds two, plus a predicate that specifies which log entries to log
using which action. Then, the `makeKoreLogger1` function uses the
selector function to filter the logs, render them with the appropriate
rendered (json or standard) and log them using the appropriate log
action.
* `booster/Server.hs` is modified to initialize `LogSomeAction` with the
appropriate log actions. If `-l SimplifyJson` log level is activated, we
enable `DebugAttemptEquation` and `DebugApplyEquation` (as before). If
`--simplification-log-file` is passed too, then Kore's simplification
will be redirected there, otherwise they will end-up on stderr.
Booster's simplilfications behave in the same way.
* Finally, `booster/Proxy.hs` does not modify the request parameters
when falling back to Kore or making internal simplify requests. We do
not output logs received form Kore at `-l SimplifJson` anymore: Kore
will now do it itself.

## Example

Put simplification logs into a file
```
kore-rpc-booster def.kore --module DEF --server-port 12341 -l SimplifyJson --simplification-log-file logs.json
```
Or simply to `stderr`:

```
kore-rpc-booster def.kore --module DEF --server-port 12341 -l SimplifyJson
```
where there will be prepended with `[SimplifyJson]`

---------

Co-authored-by: github-actions <[email protected]>

Author: geo2a

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

@@ -25,7 +25,7 @@ import Data.Bifunctor (second)
 import Data.Either (partitionEithers)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map qualified as Map
-import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust, isNothing, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, mapMaybe)
 import Data.Text (Text)
 import Data.Text qualified as Text
 import Data.Text.Lazy (toStrict)
@@ -42,7 +42,6 @@ import Kore.Internal.TermLike (TermLike, VariableName)
 import Kore.JsonRpc qualified as Kore (ServerState)
 import Kore.JsonRpc.Types
 import Kore.JsonRpc.Types qualified as ExecuteRequest (ExecuteRequest (..))
-import Kore.JsonRpc.Types qualified as ImpliesRequest (ImpliesRequest (..))
 import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..))
 import Kore.JsonRpc.Types.Log qualified as RPCLog
 import Kore.Log qualified
@@ -106,26 +105,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                 Map.lookup m bState.definitions
                     handleExecute logSettings def start execReq
     Implies impliesReq -> do
-        koreResult <-
-            loggedKore
-                ImpliesM
-                ( Implies
-                    impliesReq
-                        { ImpliesRequest.logSuccessfulSimplifications =
-                            Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
-                        }
-                )
-        case koreResult of
-            Right (Implies koreRes) -> do
-                -- Kore may have produced simplification logs during rewriting. If so,
-                -- output them Kore at "SimplifyJson" level. Erase terms from the traces.
-                when (isJust koreRes.logs) $ do
-                    outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                        . map RPCLog.logEntryEraseTerms
-                        . fromJust
-                        $ koreRes.logs
-            _ -> pure ()
-        pure koreResult
+        loggedKore ImpliesM (Implies impliesReq)
     Simplify simplifyReq ->
         liftIO (getTime Monotonic) >>= handleSimplify simplifyReq . Just
     AddModule _ -> do
@@ -176,8 +156,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                         Simplify
                             simplifyReq
                                 { SimplifyRequest.state = boosterRes.state
-                                , SimplifyRequest.logSuccessfulSimplifications =
-                                    Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
                                 }
                 (koreResult, koreTime) <- Stats.timed $ kore koreReq
                 case koreResult of
@@ -195,13 +173,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                             diffBy def boosterRes.state.term koreRes.state.term
                                  in Text.pack ("Kore simplification: Diff (< before - > after)\n" <> diff)
                         stop <- liftIO $ getTime Monotonic
-                        -- output simplification traces returned by Kore at "SimplifyJson" level, effectively
-                        -- appending them to Booster's traces. Erase terms from the traces.
-                        when (isJust koreRes.logs) $ do
-                            outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                                . map RPCLog.logEntryEraseTerms
-                                . fromJust
-                                $ koreRes.logs
                         let timing
                                 | Just start <- mbStart
                                 , fromMaybe False simplifyReq.logTiming =
@@ -290,7 +261,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
             other -> other
 
     postProcessLogs :: [RPCLog.LogEntry] -> [RPCLog.LogEntry]
-    postProcessLogs !logs = map RPCLog.logEntryEraseTerms . filter (not . isSimplificationLogEntry) $ logs
+    postProcessLogs !logs = map RPCLog.logEntryEraseTerms logs
 
     executionLoop ::
         LogSettings ->
@@ -373,8 +344,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 { state = execStateToKoreJson simplifiedBoosterState
                                                 , maxDepth = Just $ Depth 1
                                                 , assumeStateDefined = Just True
-                                                , ExecuteRequest.logSuccessfulSimplifications =
-                                                    Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
                                                 }
                                         )
                             when (isJust statsVar) $ do
@@ -420,16 +389,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 Log.logOtherNS "proxy" (Log.LevelOther "Aborts") $
                                                     "kore confirms result " <> Text.pack (show bRes)
 
-                                    -- Kore may have produced simplification logs during rewriting. If so,
-                                    -- output them Kore at "SimplifyJson" level, effectively
-                                    -- appending them to Booster's traces. Erase terms from the traces.
-                                    when (isJust koreResult.logs) $ do
-                                        outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                                            . map RPCLog.logEntryEraseTerms
-                                            . filter isSimplificationLogEntry
-                                            . fromJust
-                                            $ koreResult.logs
-
                                     case koreResult.reason of
                                         DepthBound -> do
                                             -- if we made one step, add the number of
@@ -648,15 +607,6 @@ combineLogs logSources
     | all isNothing logSources = Nothing
     | otherwise = Just $ concat $ catMaybes logSources
 
--- | Log a list of RPCLog items at a certain level
-outputLogsAtLevel :: Log.MonadLogger m => Log.LogLevel -> [RPCLog.LogEntry] -> m ()
-outputLogsAtLevel level = mapM_ (Log.logOtherNS "proxy" level . RPCLog.encodeLogEntryText)
-
-isSimplificationLogEntry :: RPCLog.LogEntry -> Bool
-isSimplificationLogEntry = \case
-    RPCLog.Simplification{} -> True
-    _ -> False
-
 makeVacuous :: Maybe [RPCLog.LogEntry] -> ExecuteResult -> ExecuteResult
 makeVacuous newLogs execState =
     execState

booster/tools/booster/Proxy.hs

@@ -24,6 +24,7 @@ import Control.Monad.Logger (
     runNoLoggingT,
  )
 import Control.Monad.Logger qualified as Logger
+import Data.ByteString qualified as BS
 import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
@@ -33,7 +34,7 @@ import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text qualified as Text
-import Data.Text.Encoding qualified as Text (decodeUtf8)
+import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
 import Options.Applicative
 import System.Clock (
     Clock (..),
@@ -69,8 +70,9 @@ import Kore.JsonRpc.Types (API, HaltReason (..), ReqOrRes (Req, Res))
 import Kore.JsonRpc.Types.Depth (Depth (..))
 import Kore.Log (
     ExeName (..),
-    KoreLogType (LogSomeAction),
+    KoreLogType (..),
     LogAction (LogAction),
+    LogSomeActionData (..),
     TimestampsSwitch (TimestampsDisable),
     defaultKoreLogOptions,
     swappableLogger,
@@ -124,8 +126,9 @@ main = do
         koreSolverOptions = translateSMTOpts smtOptions
 
     Booster.withLogFile simplificationLogFile $ \mLogFileHandle -> do
-        let logLevelToHandle = \case
-                Logger.LevelOther "SimplifyJson" -> fromMaybe IO.stderr mLogFileHandle
+        let simplificationLogHandle = fromMaybe IO.stderr mLogFileHandle
+            logLevelToHandle = \case
+                Logger.LevelOther "SimplifyJson" -> simplificationLogHandle
                 _ -> IO.stderr
 
         Booster.runHandleLoggingT logLevelToHandle . Logger.filterLogger levelFilter $ do
@@ -141,7 +144,16 @@ main = do
 
             monadLogger <- askLoggerIO
 
-            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
+            koreLogEntriesAsJsonSelector <-
+                case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
+                    Nothing -> do
+                        Logger.logWarnNS
+                            "proxy"
+                            "Could not find out which Kore log entries correspond to the SimplifyJson level"
+                        pure (const False)
+                    Just es -> pure (`elem` es)
+
+            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \_reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
                 let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
                     koreLogOptions =
                         (defaultKoreLogOptions (ExeName "") startTime)
@@ -150,11 +162,29 @@ main = do
                             , Log.timestampsSwitch = TimestampsDisable
                             , Log.debugSolverOptions =
                                 Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript)
-                            , Log.logType = LogSomeAction $ LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt
+                            , Log.logType =
+                                LogSomeAction $
+                                    LogSomeActionData
+                                        { entrySelector = koreLogEntriesAsJsonSelector
+                                        , standardLogAction =
+                                            (LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt)
+                                        , jsonLogAction =
+                                            ( LogAction $ \txt ->
+                                                let bytes =
+                                                        Text.encodeUtf8 $
+                                                            if simplificationLogHandle == IO.stderr
+                                                                then "[SimplifyJson] " <> txt <> "\n"
+                                                                else txt <> "\n"
+                                                 in liftIO $ do
+                                                        BS.hPutStr simplificationLogHandle bytes
+                                                        IO.hFlush simplificationLogHandle
+                                            )
+                                        }
+                            , Log.logFormat = Log.Standard
                             }
                     srvSettings = serverSettings port "*"
 
-                withLogger reportDirectory koreLogOptions $ \actualLogAction -> do
+                withLogger koreLogOptions $ \actualLogAction -> do
                     mLlvmLibrary <- maybe (pure Nothing) (fmap Just . mkAPI) mdl
                     definitionsWithCeilSummaries <-
                         liftIO $
@@ -261,16 +291,22 @@ toSeverity LevelOther{} = Nothing
 
 koreExtraLogs :: Map.Map LogLevel Log.EntryTypes
 koreExtraLogs =
-    Map.map (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry)) $
-        Map.fromList
-            [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
-            ,
-                ( LevelOther "RewriteKore"
-                , ["DebugAttemptedRewriteRules", "DebugAppliedLabeledRewriteRule", "DebugAppliedRewriteRules"]
-                )
-            , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
-            , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
-            ]
+    Map.map
+        (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry))
+        logLevelToKoreLogEntryMap
+
+logLevelToKoreLogEntryMap :: Map.Map LogLevel [Text.Text]
+logLevelToKoreLogEntryMap =
+    Map.fromList
+        [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
+        , (LevelOther "SimplifyJson", ["DebugAttemptEquation"])
+        ,
+            ( LevelOther "RewriteKore"
+            , ["DebugAttemptedRewriteRules", "DebugAppliedLabeledRewriteRule", "DebugAppliedRewriteRules"]
+            )
+        , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
+        , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
+        ]
 
 data CLProxyOptions = CLProxyOptions
     { clOptions :: CLOptions
@@ -378,7 +414,8 @@ translateSMTOpts = \case
     translateSExpr (SMT.Atom (SMT.SMTId x)) = KoreSMT.Atom (Text.decodeUtf8 x)
     translateSExpr (SMT.List ss) = KoreSMT.List $ map translateSExpr ss
 
-mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
+mkKoreServer ::
+    Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         sd@GlobalMain.SerializedDefinition{internedTextCache} <-

booster/tools/booster/Server.hs

@@ -24,6 +24,7 @@ import Control.Monad.Logger (
 import Control.Monad.Logger qualified as Log
 import Control.Monad.Logger qualified as Logger
 import Data.Aeson.Types (Value (..))
+import Data.ByteString qualified as BS
 import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
@@ -32,7 +33,7 @@ import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Text qualified as Text
-import Data.Text.Encoding qualified as Text (decodeUtf8)
+import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
 import Network.JSONRPC
 import Options.Applicative
 import System.Clock (
@@ -41,6 +42,7 @@ import System.Clock (
  )
 import System.Exit
 import System.IO (hPutStrLn, stderr)
+import System.IO qualified as IO
 
 import Booster.CLOptions
 import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..))
@@ -154,6 +156,15 @@ main = do
 
         monadLogger <- askLoggerIO
 
+        koreLogEntriesAsJsonSelector <-
+            case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
+                Nothing -> do
+                    Logger.logWarnNS
+                        "proxy"
+                        "Could not find out which Kore log entries correspond to the SimplifyJson level"
+                    pure (const False)
+                Just es -> pure (`elem` es)
+
         let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
             koreLogOptions =
                 (defaultKoreLogOptions (ExeName "") startTime)
@@ -162,16 +173,30 @@ main = do
                     , Log.timestampsSwitch = TimestampsDisable
                     , Log.debugSolverOptions =
                         Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript)
-                    , Log.logType = LogSomeAction $ LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt
+                    , Log.logType =
+                        LogSomeAction $
+                            Log.LogSomeActionData
+                                { entrySelector = koreLogEntriesAsJsonSelector
+                                , standardLogAction =
+                                    (LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt)
+                                , jsonLogAction =
+                                    ( LogAction $ \txt ->
+                                        let bytes = Text.encodeUtf8 $ "[SimplifyJson] " <> txt <> "\n"
+                                         in liftIO $ do
+                                                BS.hPutStr IO.stderr bytes
+                                                IO.hFlush IO.stderr
+                                    )
+                                }
+                    , Log.logFormat = Log.Standard
                     }
             srvSettings = serverSettings port "*"
 
-        liftIO $ void $ withBugReport (ExeName "kore-rpc-dev") BugReportOnError $ \reportDirectory ->
-            withLogger reportDirectory koreLogOptions $ \actualLogAction -> do
+        liftIO $ void $ withBugReport (ExeName "kore-rpc-dev") BugReportOnError $ \_reportDirectory ->
+            withLogger koreLogOptions $ \actualLogAction -> do
                 mvarLogAction <- newMVar actualLogAction
                 let logAction = swappableLogger mvarLogAction
-
-                kore@KoreServer{runSMT} <- mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
+                kore@KoreServer{runSMT} <-
+                    mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
                 runLoggingT (Logger.logInfoNS "proxy" "Starting RPC server") monadLogger
 
                 let koreRespond :: Respond (API 'Req) (LoggingT IO) (API 'Res)
@@ -205,13 +230,22 @@ toSeverity LevelOther{} = Nothing
 
 koreExtraLogs :: Map.Map LogLevel Log.EntryTypes
 koreExtraLogs =
-    Map.map (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry)) $
-        Map.fromList
-            [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
-            , (LevelOther "RewriteKore", ["DebugAttemptedRewriteRules", "DebugAppliedRewriteRules"])
-            , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
-            , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
-            ]
+    Map.map
+        (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry))
+        logLevelToKoreLogEntryMap
+
+logLevelToKoreLogEntryMap :: Map.Map LogLevel [Text.Text]
+logLevelToKoreLogEntryMap =
+    Map.fromList
+        [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
+        , (LevelOther "SimplifyJson", ["DebugAttemptEquation"])
+        ,
+            ( LevelOther "RewriteKore"
+            , ["DebugAttemptedRewriteRules", "DebugAppliedLabeledRewriteRule", "DebugAppliedRewriteRules"]
+            )
+        , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
+        , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
+        ]
 
 newtype CLProxyOptions = CLProxyOptions
     { clOptions :: CLOptions
@@ -253,7 +287,8 @@ translateSMTOpts = \case
     translateSExpr (SMT.Atom (SMT.SMTId x)) = KoreSMT.Atom (Text.decodeUtf8 x)
     translateSExpr (SMT.List ss) = KoreSMT.List $ map translateSExpr ss
 
-mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSMT.KoreSolverOptions -> IO KoreServer
+mkKoreServer ::
+    Log.LoggerEnv IO -> CLOptions -> KoreSMT.KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         sd@GlobalMain.SerializedDefinition{internedTextCache} <-

dev-tools/kore-rpc-dev/Server.hs

@@ -176,6 +176,7 @@ executables:
     dependencies:
       - aeson
       - base
+      - bytestring
       - clock
       - conduit-extra
       - containers