One-line contextual logging of Kore actions (#3837)

Combines #3833 and #3831 - in Kore, implement rendering of oneline logs prefixed with the context stack, in the spirit of #3826 - add `--log-format <standard|oneline|json> (default:oneline)` to `kore-rpc-booster`. - to recover the old behaviour of `-l Rewrite` and friends, use `--log-format standard`, i.e. `kore-rpc-booster --log-format standard -l Rewrite` - if any `--log-context` is passed, the log format is effectively override to be `oneline` - in `booster/tools/booster/Server.hs`, construct a log action to be passed to Kore. If no `--log-context` options are passed, then the old `-l RewriteKore` and fields levels still work with `--log-format standard`. If `--log-context` is passed, then the complete set of proxy-compatible Kore log entries is enabled, and the filtering is done using the glob context filter late in the colog pipeline. Things to do in a follow-up: - json logging is inconsistent, both the interface and the implementation: - to get simplification JSON logs from both Booster and Kore, we currently need to give two options: `kore-rpc-booster --log-format json -l SimplifyJson`, which is not ideal. We need to remove `-l SimplifyJson` and forward the log format to Booster instead. - To implement the previous item in a clean way, we actually need to stop emitting the logs at `SimplifyJson` level and instead render the regular log items as json. - file logging is inconsistent. It is currently not possible to redirect Booster's contextual logs into a file. - the performance of context filtering in Kore is likely terrible, since we match the while log message, as a string, against the glob pattern. There is not penalty if the contextual logging is off however. --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: Jost Berthold <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 7, 2024 · fcaae28 · fcaae28
1 parent 88ef647
commit fcaae28
Show file tree

Hide file tree

Showing 26 changed files with 855 additions and 614 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs
@@ -3,6 +3,7 @@
 module Booster.CLOptions (
     CLOptions (..),
     EquationOptions (..),
+    LogFormat (..),
     clOptionsParser,
     adjustLogLevels,
     versionInfoParser,
@@ -31,6 +32,7 @@ data CLOptions = CLOptions
     , port :: Int
     , logLevels :: [LogLevel]
     , logTimeStamps :: Bool
+    , logFormat :: LogFormat
     , logContexts :: [String]
     , notLogContexts :: [String]
     , simplificationLogFile :: Maybe FilePath
@@ -41,6 +43,18 @@ data CLOptions = CLOptions
     }
     deriving (Show)
 
+data LogFormat
+    = Standard
+    | OneLine
+    | Json
+    deriving (Eq)
+
+instance Show LogFormat where
+    show = \case
+        OneLine -> "oneline"
+        Standard -> "standard"
+        Json -> "json"
+
 clOptionsParser :: Parser CLOptions
 clOptionsParser =
     CLOptions
@@ -82,6 +96,14 @@ clOptionsParser =
                 )
             )
         <*> switch (long "log-timestamps" <> help "Add timestamps to logs")
+        <*> option
+            (eitherReader readLogFormat)
+            ( metavar "LOGFORMAT"
+                <> value OneLine
+                <> long "log-format"
+                <> help "Format to output logs in"
+                <> showDefault
+            )
         <*> many
             ( option
                 str
@@ -143,6 +165,13 @@ clOptionsParser =
             . toPascal
             . fromKebab
 
+    readLogFormat :: String -> Either String LogFormat
+    readLogFormat = \case
+        "oneline" -> Right OneLine
+        "standard" -> Right Standard
+        "json" -> Right Json
+        other -> Left $ other <> ": Unsupported log format"
+
 -- custom log levels that can be selected
 allowedLogLevels :: [(String, String)]
 allowedLogLevels =

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
@@ -39,12 +39,10 @@ import Data.List.Extra (splitOn, takeEnd)
 import Data.Set qualified as Set
 import Data.String (IsString)
 import Data.Text (Text, pack)
-import Data.Text qualified as Text
 import Data.Text.Lazy qualified as LazyText
-import Data.Word (Word64)
 import GHC.Exts (IsString (..))
 import GHC.TypeLits (KnownSymbol, symbolVal)
-import Numeric (showHex)
+import Kore.Util (showHashHex)
 import Prettyprinter (Pretty, pretty)
 
 newtype Logger a = Logger (a -> IO ())
@@ -97,9 +95,6 @@ withContext c = withLogger (\(Logger l) -> Logger $ l . (\(LogMessage ctxt m) ->
 
 newtype TermCtxt = TermCtxt Int
 
-showHashHex :: Int -> Text
-showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ pack $ showHex w64 ""
-
 instance ToLogFormat TermCtxt where
     toTextualLog (TermCtxt hsh) = "term " <> (showHashHex hsh)
 

diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -84,6 +84,7 @@ import Booster.Prettyprinter (renderDefault, renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Util (Bound (..), Flag (..))
 import Kore.JsonRpc.Types.Log qualified as KoreRpcLog
+import Kore.Util (showHashHex)
 
 newtype EquationT io a
     = EquationT (ReaderT EquationConfig (ExceptT EquationFailure (StateT EquationState io)) a)

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/tools/booster/Server.hs b/booster/tools/booster/Server.hs
@@ -20,7 +20,6 @@ import Control.Monad.Logger (
     LoggingT (runLoggingT),
     MonadLoggerIO (askLoggerIO),
     ToLogStr (toLogStr),
-    defaultLoc,
     runNoLoggingT,
  )
 import Control.Monad.Logger qualified as Logger
@@ -37,6 +36,7 @@ import Data.Text.Encoding qualified as Text (decodeUtf8)
 import Options.Applicative
 import System.Clock (
     Clock (..),
+    TimeSpec (..),
     getTime,
  )
 import System.Environment qualified as Env
@@ -72,21 +72,25 @@ import Kore.JsonRpc.Error hiding (Aborted, error)
 import Kore.JsonRpc.Server
 import Kore.JsonRpc.Types (API, HaltReason (..), ReqOrRes (Req, Res))
 import Kore.JsonRpc.Types.Depth (Depth (..))
-import Kore.Log (
+import Kore.Log.BoosterAdaptor (
     ExeName (..),
     KoreLogType (..),
     LogAction (LogAction),
-    LogSomeActionData (..),
     TimestampsSwitch (TimestampsDisable),
     defaultKoreLogOptions,
+    koreSomeEntryLogAction,
+    renderJson,
+    renderOnelinePretty,
+    renderStandardPretty,
     swappableLogger,
     withLogger,
  )
-import Kore.Log qualified as Log
+import Kore.Log.BoosterAdaptor qualified as Log
 import Kore.Log.DebugSolver qualified as Log
 import Kore.Log.Registry qualified as Log
 import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
 import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
+import Kore.Util (extractLogMessageContext)
 import Options.SMT as KoreSMT (KoreSolverOptions (..), Solver (..))
 import Prettyprinter qualified as Pretty
 import Proxy (KoreServer (..), ProxyConfig (..))
@@ -115,6 +119,7 @@ main = do
                     , port
                     , llvmLibraryFile
                     , logLevels
+                    , logFormat
                     , logTimeStamps
                     , logContexts
                     , notLogContexts
@@ -136,6 +141,7 @@ main = do
         (logLevel, customLevels) = adjustLogLevels logLevels
         globPatterns = map (Glob.compile . filter (\c -> not (c == '\'' || c == '"'))) logContexts
         negGlobPatterns = map (Glob.compile . filter (\c -> not (c == '\'' || c == '"'))) notLogContexts
+        contexLoggingEnabled = not (null logContexts) || not (null notLogContexts)
         levelFilter :: Logger.LogSource -> LogLevel -> Bool
         levelFilter _source lvl =
             lvl `elem` customLevels
@@ -145,8 +151,6 @@ main = do
                             && any (flip Glob.match (Text.unpack l)) globPatterns
                     _ -> False
                 || lvl >= logLevel && lvl <= LevelError
-        koreLogExtraLevels =
-            Set.unions $ mapMaybe (`Map.lookup` koreExtraLogs) customLevels
         koreSolverOptions = translateSMTOpts smtOptions
 
     mTimeCache <- if logTimeStamps then Just <$> (newTimeCache "%Y-%m-%d %T") else pure Nothing
@@ -165,39 +169,52 @@ main = do
 
             monadLogger <- askLoggerIO
 
-            koreLogEntriesAsJsonSelector <-
-                if Logger.LevelOther "SimplifyJson" `elem` customLevels
-                    then 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 koreSimplificationLogEntries -> pure (`elem` koreSimplificationLogEntries)
-                    else pure (const False)
+            let koreLogRenderer = case logFormat of
+                    Standard -> renderStandardPretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
+                    OneLine -> renderOnelinePretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
+                    Json -> renderJson (ExeName "") (TimeSpec 0 0) TimestampsDisable
+                koreLogLateFilter = case logFormat of
+                    OneLine ->
+                        if contexLoggingEnabled
+                            then \txt ->
+                                let contextStr = Text.unpack $ extractLogMessageContext txt
+                                 in -- FIXME: likely terrible performance! Use something that does not unpack Text
+                                    not (any (flip Glob.match contextStr) negGlobPatterns)
+                                        && any (flip Glob.match contextStr) globPatterns
+                            else const True
+                    _ -> const True
+
+                koreLogEntries =
+                    if contexLoggingEnabled
+                        then -- context logging: enable all Proxy-required Kore log entries
+                            Set.unions . Map.elems $ koreExtraLogs
+                        else -- no context logging: only enable Kore log entries for the given Proxy log levels
+                            Set.unions . mapMaybe (`Map.lookup` koreExtraLogs) $ customLevels
+
+                koreLogActions :: forall m. MonadIO m => [LogAction m Log.SomeEntry]
+                koreLogActions = [koreLogAction]
+                  where
+                    koreLogAction =
+                        koreSomeEntryLogAction
+                            koreLogRenderer
+                            (const True)
+                            koreLogLateFilter
+                            ( LogAction $ \txt -> liftIO $
+                                case mFileLogger of
+                                    Just fileLogger -> fileLogger $ toLogStr $ txt <> "\n"
+                                    Nothing -> stderrLogger $ toLogStr $ txt <> "\n"
+                            )
 
             liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \_reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
                 let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
                     koreLogOptions =
                         (defaultKoreLogOptions (ExeName "") startTime)
                             { Log.logLevel = coLogLevel
-                            , Log.logEntries = koreLogExtraLevels
+                            , Log.logEntries = koreLogEntries
                             , Log.timestampsSwitch = TimestampsDisable
                             , Log.debugSolverOptions =
                                 Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript)
-                            , Log.logType =
-                                LogSomeAction $
-                                    LogSomeActionData
-                                        { entrySelector = koreLogEntriesAsJsonSelector
-                                        , standardLogAction =
-                                            (LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt)
-                                        , jsonLogAction =
-                                            ( LogAction $ \txt -> liftIO $
-                                                case mFileLogger of
-                                                    Just fileLogger -> fileLogger $ toLogStr $ txt <> "\n"
-                                                    Nothing -> stderrLogger $ toLogStr $ "[SimplifyJson] " <> txt <> "\n"
-                                            )
-                                        }
+                            , Log.logType = LogProxy (mconcat koreLogActions)
                             , Log.logFormat = Log.Standard
                             }
                     srvSettings = serverSettings port "*"