JSON logging cleanup (#3881)

* Re-add the `test-log-simplify-json` rpc test with a much smaller footprint, as we want to just track the context logging format * Clean up the equation contexts a bit in booster, as we weren't consistently logging messages around functions/equations * Closes #3864 by adding a conversion from the old custom log levels to contextual log filters. * Closes #3866 by removing the SimplifyJson log level which has been replaced by `-l Simplify --log-format json` --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: Georgy Lukyanov <[email protected]>
runtimeverification · May 22, 2024 · e62fba2 · e62fba2
1 parent 8b7ed67
commit e62fba2
Show file tree

Hide file tree

Showing 14 changed files with 4,942 additions and 122 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Booster.CLOptions (
@@ -6,6 +7,7 @@ module Booster.CLOptions (
     LogFormat (..),
     clOptionsParser,
     adjustLogLevels,
+    levelToContext,
     versionInfoParser,
 ) where
 
@@ -22,9 +24,11 @@ import Text.Casing (fromHumps, fromKebab, toKebab, toPascal)
 import Text.Read (readMaybe)
 
 import Booster.GlobalState (EquationOptions (..))
-import Booster.Log.Context (ContextFilter, readContextFilter)
+import Booster.Log.Context (ContextFilter, ctxt, readContextFilter)
 import Booster.SMT.Interface (SMTOptions (..), defaultSMTOptions)
 import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr)
+import Data.Map (Map)
+import Data.Map qualified as Map
 
 data CLOptions = CLOptions
     { definitionFile :: FilePath
@@ -35,7 +39,7 @@ data CLOptions = CLOptions
     , logTimeStamps :: Bool
     , logFormat :: LogFormat
     , logContexts :: [ContextFilter]
-    , simplificationLogFile :: Maybe FilePath
+    , logFile :: Maybe FilePath
     , smtOptions :: Maybe SMTOptions
     , equationOptions :: EquationOptions
     , -- developer options below
@@ -116,10 +120,10 @@ clOptionsParser =
             )
         <*> optional
             ( strOption
-                ( metavar "JSON_LOG_FILE"
-                    <> long "simplification-log-file"
+                ( metavar "LOG_FILE"
+                    <> long "log-file"
                     <> help
-                        "Log file for the JSON simplification logs"
+                        "Log file to output the logs into"
                 )
             )
         <*> parseSMTOptions
@@ -171,14 +175,50 @@ allowedLogLevels =
     , ("RewriteKore", "Log all rewriting in kore-rpc fall-backs")
     , ("RewriteSuccess", "Log successful rewrites (booster and kore-rpc)")
     , ("Simplify", "Log all simplification/evaluation in booster")
-    , ("SimplifyJson", "Log simplification/evaluation in booster as JSON")
     , ("SimplifyKore", "Log all simplification in kore-rpc")
     , ("SimplifySuccess", "Log successful simplifications (booster and kore-rpc)")
     , ("Depth", "Log the current depth of the state")
     , ("SMT", "Log the SMT-solver interactions")
     , ("ErrorDetails", "Log error conditions with extensive details")
     ]
 
+levelToContext :: Map Text [ContextFilter]
+levelToContext =
+    Map.fromList
+        [
+            ( "Simplify"
+            ,
+                [ [ctxt| booster|kore>function*|simplification*,success|failure|abort|detail |]
+                , [ctxt| booster|kore>function*|simplification*,match,failure|abort |]
+                ]
+            )
+        ,
+            ( "SimplifySuccess"
+            ,
+                [ [ctxt| booster|kore>function*|simplification*,success|detail |]
+                ]
+            )
+        ,
+            ( "Rewrite"
+            ,
+                [ [ctxt| booster|kore>rewrite*,success|failure|abort|detail |]
+                , [ctxt| booster|kore>rewrite*,match,failure|abort |]
+                ]
+            )
+        ,
+            ( "RewriteSuccess"
+            ,
+                [ [ctxt| booster|kore>rewrite*,success|detail |]
+                ]
+            )
+        ,
+            ( "SMT"
+            ,
+                [ [ctxt| booster|kore>smt |]
+                ]
+            )
+        ]
+
 -- Partition provided log levels into standard and custom ones, and
 -- select the lowest standard level. Default to 'LevelInfo' if no
 -- standard log level was given.

diff --git a/booster/library/Booster/Log/Context.hs b/booster/library/Booster/Log/Context.hs
@@ -1,25 +1,31 @@
-module Booster.Log.Context (ContextFilter, mustMatch, readContextFilter, readMatch) where
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+
+module Booster.Log.Context (ContextFilter, mustMatch, readContextFilter, readMatch, ctxt) where
 
 import Control.Applicative ((<|>))
 import Data.Attoparsec.ByteString.Char8 qualified as A
 import Data.ByteString.Char8 qualified as BS
 import Data.Char (isSpace)
+import Data.Generics (Data, extQ)
 import Data.List.Extra (replace)
+import Language.Haskell.TH (ExpQ, Lit (StringL), appE, litE, varE)
+import Language.Haskell.TH.Quote (QuasiQuoter (..), dataToExpQ)
 
 data ContextFilterSingle
     = Exact BS.ByteString
     | Prefix BS.ByteString
     | Suffix BS.ByteString
     | Infix BS.ByteString
     | Negate ContextFilterSingle
-    deriving (Show)
+    deriving (Show, Data)
 
 data ContextFilter
     = First [ContextFilterSingle]
     | ThenDirectChild [ContextFilterSingle] ContextFilter
     | ThenChild [ContextFilterSingle] ContextFilter
     | Last [ContextFilterSingle]
-    deriving (Show)
+    deriving (Show, Data)
 
 reserved :: String
 reserved = "|*!>,."
@@ -79,3 +85,21 @@ readMatch :: BS.ByteString -> [BS.ByteString] -> Either String Bool
 readMatch pat' xs = do
     pat <- A.parseOnly (contextFilterP <* A.skipSpace <* A.endOfInput) pat'
     pure $ mustMatch pat xs
+
+ctxt :: QuasiQuoter
+ctxt =
+    QuasiQuoter
+        { quoteExp =
+            dataToExpQ (const Nothing `extQ` handleBS)
+                . either (error . show) id
+                . readContextFilter
+        , quotePat = undefined
+        , quoteType = undefined
+        , quoteDec = undefined
+        }
+  where
+    handleBS :: BS.ByteString -> Maybe ExpQ
+    handleBS x =
+        -- convert the byte string to a string literal
+        -- and wrap it back with BS.pack
+        Just $ appE (varE 'BS.pack) $ litE $ StringL $ BS.unpack x
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -28,7 +28,6 @@ module Booster.Pattern.ApplyEquations (
     evaluateConstraints,
 ) where
 
-import Control.Applicative (Alternative (..))
 import Control.Monad
 import Control.Monad.Extra (fromMaybeM, whenJust)
 import Control.Monad.IO.Class (MonadIO (..))
@@ -45,7 +44,6 @@ import Control.Monad.Trans.Except
 import Control.Monad.Trans.Reader (ReaderT (..), ask, asks, withReaderT)
 import Control.Monad.Trans.State
 import Data.Aeson (object, (.=))
-import Data.Aeson.Text (encodeToLazyText)
 import Data.Bifunctor (bimap)
 import Data.ByteString.Char8 qualified as BS
 import Data.Coerce (coerce)
@@ -62,7 +60,6 @@ import Data.Set qualified as Set
 import Data.Text (Text, pack)
 import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Text
-import Data.Text.Lazy qualified as Text (toStrict)
 import GHC.TypeLits (KnownSymbol)
 import Prettyprinter
 
@@ -82,7 +79,6 @@ import Booster.Prettyprinter (renderDefault, renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Util (Bound (..))
-import Kore.JsonRpc.Types.Log qualified as KoreRpcLog
 import Kore.Util (showHashHex)
 
 newtype EquationT io a
@@ -254,52 +250,6 @@ isMatchFailure _ = False
 isSuccess EquationApplied{} = True
 isSuccess _ = False
 
-{- | Attempt to get an equation's unique id, falling back to it's label or eventually to UNKNOWN.
-  The fallbacks are useful in case of cached equation applications or the ones done via LLVM,
-  as neither of these categories have unique IDs.
--}
-equationRuleIdWithFallbacks :: EquationMetadata -> Text
-equationRuleIdWithFallbacks metadata =
-    fromMaybe "UNKNOWN" (fmap getUniqueId metadata.ruleId <|> metadata.label)
-
-equationTraceToLogEntry :: EquationTrace Term -> KoreRpcLog.LogEntry
-equationTraceToLogEntry = \case
-    EquationApplied _subjectTerm metadata _rewritten ->
-        KoreRpcLog.Simplification
-            { originalTerm
-            , originalTermIndex
-            , origin
-            , result =
-                KoreRpcLog.Success Nothing Nothing _ruleId
-            }
-      where
-        originalTerm = Nothing
-        originalTermIndex = Nothing
-        origin = KoreRpcLog.Booster
-        _ruleId = equationRuleIdWithFallbacks metadata
-    EquationNotApplied _subjectTerm metadata failure ->
-        KoreRpcLog.Simplification
-            { originalTerm
-            , originalTermIndex
-            , origin
-            , result = KoreRpcLog.Failure (failureDescription failure) (Just _ruleId)
-            }
-      where
-        originalTerm = Nothing
-        originalTermIndex = Nothing
-        origin = KoreRpcLog.Booster
-        _ruleId = equationRuleIdWithFallbacks metadata
-
-        failureDescription :: ApplyEquationFailure -> Text.Text
-        failureDescription = \case
-            FailedMatch{} -> "Failed match"
-            IndeterminateMatch -> "IndeterminateMatch"
-            IndeterminateCondition{} -> "IndeterminateCondition"
-            ConditionFalse{} -> "ConditionFalse"
-            EnsuresFalse{} -> "EnsuresFalse"
-            RuleNotPreservingDefinedness -> "RuleNotPreservingDefinedness"
-            MatchConstraintViolated{} -> "MatchConstraintViolated"
-
 startState :: SimplifierCache -> EquationState
 startState cache =
     EquationState
@@ -426,9 +376,7 @@ iterateEquations ::
     Term ->
     EquationT io Term
 iterateEquations direction preference startTerm = do
-    result <- pushRecursion startTerm >>= checkCounter >> go startTerm <* popRecursion
-    when (startTerm /= result) $ withContext "success" $ withTermContext result $ pure ()
-    pure result
+    pushRecursion startTerm >>= checkCounter >> go startTerm <* popRecursion
   where
     checkCounter counter = do
         config <- getConfig
@@ -832,13 +780,15 @@ applyEquations theory handler term = do
     processEquations [] =
         pure term -- nothing to do, term stays the same
     processEquations (eq : rest) = do
-        res <- applyEquation term eq
+        res <- withRuleContext eq $ applyEquation term eq
         emitEquationTrace term eq.attributes.location eq.attributes.ruleLabel eq.attributes.uniqueId res
         handler
-            (\t -> setChanged >> pure t)
+            ( \t -> setChanged >> (withContext (LogContext eq) $ withContext "success" $ withTermContext t $ pure t)
+            )
             (processEquations rest)
-            ( withContext "abort" $
-                logMessage ("Aborting simplification/function evaluation" :: Text) >> pure term
+            ( withContext (LogContext eq) $
+                withContext "abort" $
+                    logMessage ("Aborting simplification/function evaluation" :: Text) >> pure term
             )
             res
 
@@ -861,9 +811,6 @@ emitEquationTrace t loc lbl uid res = do
                 Failure failure -> EquationNotApplied t (EquationMetadata loc lbl uid) failure
         prettyItem = pack . renderDefault . pretty $ newTraceItem
     logOther (LevelOther "Simplify") prettyItem
-    logOther
-        (LevelOther "SimplifyJson")
-        (Text.toStrict . encodeToLazyText $ equationTraceToLogEntry newTraceItem)
     case res of
         Success{} -> logOther (LevelOther "SimplifySuccess") prettyItem
         _ -> pure ()
@@ -875,7 +822,7 @@ applyEquation ::
     Term ->
     RewriteRule tag ->
     EquationT io ApplyEquationResult
-applyEquation term rule = withRuleContext rule $ fmap (either Failure Success) $ runExceptT $ do
+applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do
     -- ensured by internalisation: no existentials in equations
     unless (null rule.existentials) $ do
         withContext "abort" $

diff --git a/booster/library/Booster/Util.hs b/booster/library/Booster/Util.hs
@@ -118,19 +118,13 @@ decodeLabel' orig =
 -- logging helpers, some are adapted from monad-logger-aeson
 handleOutput ::
     FastLogger ->
-    Maybe FastLogger ->
     Log.Loc ->
     Log.LogSource ->
     Log.LogLevel ->
     Log.LogStr ->
     IO ()
-handleOutput stderrLogger mFileLogger loc src level msg =
-    case level of
-        Log.LevelOther "SimplifyJson" ->
-            case mFileLogger of
-                Nothing -> stderrLogger $ "[SimplifyJson] " <> msg <> "\n"
-                Just fileLogger -> fileLogger $ msg <> "\n"
-        _ -> stderrLogger $ Log.defaultLogStr loc src level msg
+handleOutput stderrLogger loc src level msg =
+    stderrLogger $ Log.defaultLogStr loc src level msg
 
 newFastLoggerMaybeWithTime :: Maybe (IO FormattedTime) -> LogType -> IO (LogStr -> IO (), IO ())
 newFastLoggerMaybeWithTime = \case

diff --git a/booster/test/rpc-integration/resources/log-simplify-json.kore b/booster/test/rpc-integration/resources/log-simplify-json.kore