Implement logging of applied equations as JSON in Kore

booster/tools/booster/Proxy.hs

@@ -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
@@ -104,27 +103,12 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                             fromMaybe (error $ "Module " <> show m <> " not found") $
                                 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
+    Implies impliesReq ->
+        loggedKore
+            ImpliesM
+            ( Implies
+                impliesReq
+            )
     Simplify simplifyReq ->
         liftIO (getTime Monotonic) >>= handleSimplify simplifyReq . Just
     AddModule _ -> do
@@ -175,8 +159,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
@@ -194,13 +176,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 =
@@ -289,7 +264,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 ->
@@ -369,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
@@ -416,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
@@ -644,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/Server.hs

@@ -123,8 +123,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
@@ -189,9 +190,13 @@ main = do
 
                     mvarLogAction <- newMVar actualLogAction
                     let logAction = swappableLogger mvarLogAction
+                        koreSimplificationLogHandle =
+                            if Logger.LevelOther "SimplifyJson" `elem` logLevels
+                                then Just simplificationLogHandle
+                                else Nothing
 
                     kore@KoreServer{runSMT} <-
-                        mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
+                        mkKoreServer koreSimplificationLogHandle Log.LoggerEnv{logAction} clOPts koreSolverOptions
 
                     boosterState <-
                         liftIO $
@@ -368,8 +373,9 @@ 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 [email protected]{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
+mkKoreServer ::
+    Maybe IO.Handle -> Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
+mkKoreServer simplificationLogHandle [email protected]{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         [email protected]{internedTextCache} <-
             GlobalMain.deserializeDefinition
@@ -386,6 +392,7 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
                         { serializedModules = Map.singleton (ModuleName mainModuleName) sd
                         , receivedModules = mempty
                         , loadedDefinition
+                        , simplificationLogHandle = simplificationLogHandle
                         }
 
         pure $

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

@@ -41,6 +41,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 (..))
@@ -147,8 +148,10 @@ main = do
             Set.unions $ mapMaybe (`Map.lookup` koreExtraLogs) customLevels
         koreSolverOptions = translateSMTOpts smtOptions
 
+    let simplificationLogHandle = if Log.LevelOther "SimplifyJson" `elem` logLevels then Just IO.stderr else Nothing
+
     Logger.runStderrLoggingT $ Logger.filterLogger levelFilter $ do
-        liftIO $ forM_ eventlogEnabledUserEvents $ \t -> do
+        liftIO . forM_ eventlogEnabledUserEvents $ \t -> do
             putStrLn $ "Tracing " <> show t
             enableCustomUserEvent t
 
@@ -170,8 +173,8 @@ main = do
             withLogger reportDirectory koreLogOptions $ \actualLogAction -> do
                 mvarLogAction <- newMVar actualLogAction
                 let logAction = swappableLogger mvarLogAction
-
-                kore@KoreServer{runSMT} <- mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
+                kore@KoreServer{runSMT} <-
+                    mkKoreServer simplificationLogHandle Log.LoggerEnv{logAction} clOPts koreSolverOptions
                 runLoggingT (Logger.logInfoNS "proxy" "Starting RPC server") monadLogger
 
                 let koreRespond :: Respond (API 'Req) (LoggingT IO) (API 'Res)
@@ -253,8 +256,9 @@ 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 [email protected]{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
+mkKoreServer ::
+    Maybe IO.Handle -> Log.LoggerEnv IO -> CLOptions -> KoreSMT.KoreSolverOptions -> IO KoreServer
+mkKoreServer simplificationLogHandle [email protected]{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         [email protected]{internedTextCache} <-
             GlobalMain.deserializeDefinition
@@ -271,6 +275,7 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
                         { serializedModules = Map.singleton (ModuleName mainModuleName) sd
                         , receivedModules = mempty
                         , loadedDefinition
+                        , simplificationLogHandle = simplificationLogHandle
                         }
 
         pure $

kore/app/rpc/Main.hs

@@ -182,6 +182,7 @@ koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do
                     { serializedModules = Map.singleton mainModuleName sd
                     , loadedDefinition
                     , receivedModules = mempty
+                    , simplificationLogHandle = Nothing
                     }
     GlobalMain.clockSomethingIO "Executing" $
         -- wrap the call to runServer in the logger monad

kore/src/Kore/Equation/Application.hs

@@ -23,13 +23,13 @@ import Control.Monad (
     (>=>),
  )
 import Control.Monad.Reader (asks)
-import Control.Monad.State (modify)
-import Data.Bifunctor
+import Data.Aeson qualified as JSON
+import Data.ByteString.Char8 qualified as BS
 import Data.Map.Strict (
     Map,
  )
 import Data.Map.Strict qualified as Map
-import Data.Sequence ((|>))
+import Data.Maybe (fromJust)
 import Data.Set (
     Set,
  )
@@ -89,6 +89,7 @@ import Kore.Internal.TermLike (
     TermLike,
  )
 import Kore.Internal.TermLike qualified as TermLike
+import Kore.JsonRpc.Types.Log qualified as KoreRpcLog
 import Kore.Log.DecidePredicateUnknown (
     OnDecidePredicateUnknown (..),
     srcLoc,
@@ -104,7 +105,6 @@ import Kore.Rewrite.SMT.Evaluator qualified as SMT
 import Kore.Rewrite.Substitution qualified as Substitution
 import Kore.Simplify.Simplify (
     Simplifier,
-    SimplifierTrace (..),
     liftSimplifier,
  )
 import Kore.Simplify.Simplify qualified as Simplifier
@@ -257,14 +257,37 @@ applyEquation ::
     Equation RewritingVariableName ->
     Pattern RewritingVariableName ->
     Simplifier (OrPattern RewritingVariableName)
-applyEquation _ term equation result = do
+applyEquation _ _term equation result = do
     let results = OrPattern.fromPattern result
     debugApplyEquation equation result
-    doTracing <- liftSimplifier $ asks Simplifier.tracingEnabled
-    when doTracing $
-        modify $
-            second (|> SimplifierTrace term (Attribute.uniqueId $ attributes equation) result)
+    simplificationLogHandle <- liftSimplifier $ asks Simplifier.simplificationLogHandle
+    when
+        (isJust simplificationLogHandle)
+        (liftIO $ emitEquationTrace (fromJust simplificationLogHandle))
     pure results
+  where
+    -- emit the equation trace directly to the provided handle.
+    -- we intentionally omit the terms and only emit the unique id.
+    emitEquationTrace handle =
+        BS.hPutStrLn
+            handle
+            ( BS.toStrict . JSON.encode $
+                mkLogEntry (Attribute.uniqueId $ attributes equation)
+            )
+
+    mkLogEntry :: Attribute.UniqueId -> KoreRpcLog.LogEntry
+    mkLogEntry equationId =
+        KoreRpcLog.Simplification
+            { originalTerm = Nothing
+            , originalTermIndex = Nothing
+            , result =
+                KoreRpcLog.Success
+                    { rewrittenTerm = Nothing
+                    , substitution = Nothing
+                    , ruleId = fromMaybe "UNKNOWN" (Attribute.getUniqueId equationId)
+                    }
+            , origin = KoreRpcLog.KoreRpc
+            }
 
 {- | Use a 'MatchResult' to instantiate an 'Equation'.
 

kore/src/Kore/Exec.hs

@@ -228,6 +228,7 @@ import SMT (
 import System.Exit (
     ExitCode (..),
  )
+import System.IO qualified as IO
 
 -- | Semantic rule used during execution.
 type Rewrite = RewriteRule RewritingVariableName
@@ -456,6 +457,8 @@ rpcExec ::
     Step.EnableAssumeInitialDefined ->
     -- | whether tracing is enabled
     Bool ->
+    -- | optional simplification trace output handle
+    Maybe IO.Handle ->
     -- | The main module
     SerializedModule ->
     -- | additional labels/rule names for stopping
@@ -469,6 +472,7 @@ rpcExec
     enableMA
     assumeInitialDefined
     tracingEnabled
+    simplificationTraceHandle
     SerializedModule
         { sortGraph
         , overloadGraph
@@ -495,7 +499,13 @@ rpcExec
       where
         simplifierRun
             | tracingEnabled =
-                fmap snd . evalSimplifierLogged verifiedModule' sortGraph overloadGraph metadataTools equations
+                evalSimplifierLogged
+                    simplificationTraceHandle
+                    verifiedModule'
+                    sortGraph
+                    overloadGraph
+                    metadataTools
+                    equations
             | otherwise =
                 evalSimplifier verifiedModule' sortGraph overloadGraph metadataTools equations