Improve JSON logging (#3858)

This PR does the following:

* aligns JSON logs across the two backends
* removes implifyjson logs in favour of contextual JSON logging
* adds a custom syntax for `--log-context` also removing
`--no-log-context` (see the docs/logging.md change for details)
* switches the ceil analysis to contextual logs

---------

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

Author: goodlyrottenapple

booster/library/Booster/CLOptions.hs

@@ -22,6 +22,7 @@ import Text.Casing (fromHumps, fromKebab, toKebab, toPascal)
 import Text.Read (readMaybe)
 
 import Booster.GlobalState (EquationOptions (..))
+import Booster.Log.Context (ContextFilter, readContextFilter)
 import Booster.SMT.Interface (SMTOptions (..), defaultSMTOptions)
 import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr)
 
@@ -33,8 +34,7 @@ data CLOptions = CLOptions
     , logLevels :: [LogLevel]
     , logTimeStamps :: Bool
     , logFormat :: LogFormat
-    , logContexts :: [String]
-    , notLogContexts :: [String]
+    , logContexts :: [ContextFilter]
     , simplificationLogFile :: Maybe FilePath
     , smtOptions :: Maybe SMTOptions
     , equationOptions :: EquationOptions
@@ -106,23 +106,14 @@ clOptionsParser =
             )
         <*> many
             ( option
-                str
+                (eitherReader readContextFilter)
                 ( metavar "CONTEXT"
                     <> long "log-context"
                     <> short 'c'
                     <> help
                         "Log context"
                 )
             )
-        <*> many
-            ( option
-                str
-                ( metavar "CONTEXT"
-                    <> long "not-log-context"
-                    <> help
-                        "Not in log context"
-                )
-            )
         <*> optional
             ( strOption
                 ( metavar "JSON_LOG_FILE"
@@ -186,7 +177,6 @@ allowedLogLevels =
     , ("Depth", "Log the current depth of the state")
     , ("SMT", "Log the SMT-solver interactions")
     , ("ErrorDetails", "Log error conditions with extensive details")
-    , ("Ceil", "Log results of the ceil analysis")
     ]
 
 -- Partition provided log levels into standard and custom ones, and

booster/library/Booster/Definition/Attributes/Base.hs

@@ -46,6 +46,8 @@ module Booster.Definition.Attributes.Base (
 ) where
 
 import Control.DeepSeq (NFData (..))
+import Data.Aeson (ToJSON (..))
+import Data.Aeson qualified as JSON
 import Data.ByteString (ByteString)
 import Data.Data (Data)
 import Data.Hashable (Hashable)
@@ -111,6 +113,9 @@ instance Pretty NotPreservesDefinednessReason where
     pretty = \case
         UndefinedSymbol name -> "non-total symbol " <> (pretty $ Text.decodeUtf8 $ Util.decodeLabel' name)
 
+instance ToJSON NotPreservesDefinednessReason where
+    toJSON (UndefinedSymbol n) = JSON.String $ Text.decodeUtf8 n
+
 type Label = Text
 
 newtype UniqueId = UniqueId {getUniqueId :: Text}

booster/library/Booster/Definition/Ceil.hs

@@ -74,7 +74,11 @@ instance Pretty ComputeCeilSummary where
                         ]
 
 computeCeilsDefinition ::
-    LoggerMIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary])
+    LoggerMIO io =>
+    MonadLoggerIO io =>
+    Maybe LLVM.API ->
+    KoreDefinition ->
+    io (KoreDefinition, [ComputeCeilSummary])
 computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
     (rewriteTheory', ceilSummaries) <-
         runWriterT $
@@ -89,6 +93,7 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
 
 computeCeilRule ::
     LoggerMIO io =>
+    MonadLoggerIO io =>
     Maybe LLVM.API ->
     KoreDefinition ->
     RewriteRule.RewriteRule "Rewrite" ->

booster/library/Booster/JsonRpc.hs

@@ -96,6 +96,7 @@ import Kore.Syntax.Json.Types qualified as Syntax
 respond ::
     forall m.
     LoggerMIO m =>
+    Log.MonadLoggerIO m =>
     MVar ServerState ->
     Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res)
 respond stateVar =
@@ -302,7 +303,6 @@ respond stateVar =
                             Right
                                 (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term), [])
                     | otherwise -> do
-                        Log.logInfoNS "booster" "Simplifying predicates"
                         unless (null ps.unsupported) $ do
                             withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
                                 logMessage ("ignoring unsupported predicate parts" :: Text)

booster/library/Booster/Log.hs

@@ -5,32 +5,19 @@
 
 module Booster.Log (module Booster.Log) where
 
-import Booster.Definition.Attributes.Base
-import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef)
-import Booster.Pattern.Base (
-    Pattern (..),
-    Predicate (..),
-    Term (..),
-    TermAttributes (hash),
-    pattern AndTerm,
- )
-import Booster.Prettyprinter (renderOneLineText)
-import Booster.Syntax.Json (KorePattern, prettyPattern)
+import Control.Monad (when)
 import Control.Monad.IO.Class
-import Control.Monad.Logger (
-    LogLevel (..),
-    MonadLogger,
-    MonadLoggerIO (askLoggerIO),
-    NoLoggingT,
-    ToLogStr (toLogStr),
-    defaultLoc,
- )
+import Control.Monad.Logger qualified
 import Control.Monad.Trans.Class qualified as Trans
 import Control.Monad.Trans.Except (ExceptT (..))
 import Control.Monad.Trans.Maybe (MaybeT (..))
 import Control.Monad.Trans.Reader (ReaderT (..), ask, withReaderT)
 import Control.Monad.Trans.State (StateT (..))
 import Control.Monad.Trans.State.Strict qualified as Strict
+import Data.Aeson (ToJSON (..), Value (..), (.=))
+import Data.Aeson.Encode.Pretty (Config (confIndent), Indent (Spaces), encodePretty')
+import Data.Aeson.Key qualified as Key
+import Data.Aeson.Types (object)
 import Data.Coerce (coerce)
 import Data.Data (Proxy (..))
 import Data.Hashable qualified
@@ -42,15 +29,28 @@ import Data.Text (Text, pack)
 import Data.Text.Lazy qualified as LazyText
 import GHC.Exts (IsString (..))
 import GHC.TypeLits (KnownSymbol, symbolVal)
-import Kore.Util (showHashHex)
 import Prettyprinter (Pretty, pretty)
 
+import Booster.Definition.Attributes.Base
+import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef)
+import Booster.Pattern.Base (
+    Pattern (..),
+    Predicate (..),
+    Term (..),
+    TermAttributes (hash),
+    pattern AndTerm,
+ )
+import Booster.Prettyprinter (renderOneLineText)
+import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
+import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Kore.JsonRpc.Types (rpcJsonConfig)
+import Kore.Util (showHashHex)
+
 newtype Logger a = Logger (a -> IO ())
 
 class ToLogFormat a where
     toTextualLog :: a -> Text
-
--- toJSONLog :: a -> Value
+    toJSONLog :: a -> Value
 
 data LogContext = forall a. ToLogFormat a => LogContext a
 
@@ -60,7 +60,7 @@ instance IsString LogContext where
 data LogMessage where
     LogMessage :: ToLogFormat a => [LogContext] -> a -> LogMessage
 
-class MonadLoggerIO m => LoggerMIO m where
+class MonadIO m => LoggerMIO m where
     getLogger :: m (Logger LogMessage)
     default getLogger :: (Trans.MonadTrans t, LoggerMIO n, m ~ t n) => m (Logger LogMessage)
     getLogger = Trans.lift getLogger
@@ -78,7 +78,7 @@ instance LoggerMIO m => LoggerMIO (StateT s m) where
 instance LoggerMIO m => LoggerMIO (Strict.StateT s m) where
     withLogger modL (Strict.StateT m) = Strict.StateT $ \s -> withLogger modL $ m s
 
-instance MonadIO m => LoggerMIO (NoLoggingT m) where
+instance MonadIO m => LoggerMIO (Control.Monad.Logger.NoLoggingT m) where
     getLogger = pure $ Logger $ \_ -> pure ()
     withLogger _ = id
 
@@ -97,22 +97,25 @@ newtype TermCtxt = TermCtxt Int
 
 instance ToLogFormat TermCtxt where
     toTextualLog (TermCtxt hsh) = "term " <> (showHashHex hsh)
+    toJSONLog (TermCtxt hsh) = object ["term" .= showHashHex hsh]
+
+newtype HookCtxt = HookCtxt Text
 
--- toJSONLog (TermCtxt hsh) = object [ "term" .= hsh ]
+instance ToLogFormat HookCtxt where
+    toTextualLog (HookCtxt h) = "hook " <> h
+    toJSONLog (HookCtxt h) = object ["hook" .= h]
 
 instance ToLogFormat Term where
     toTextualLog t = renderOneLineText $ pretty t
-
--- toJSONLog t = toJSON $ externaliseTerm t
+    toJSONLog t = toJSON $ addHeader $ externaliseTerm t
 
 instance ToLogFormat Text where
     toTextualLog t = t
-
--- toJSONLog t = String t
+    toJSONLog t = String t
 
 withTermContext :: LoggerMIO m => Term -> m a -> m a
 withTermContext t@(Term attrs _) m = withContext (LogContext $ TermCtxt attrs.hash) $ do
-    withContext "detail" $ logMessage t
+    withContext "kore-term" $ logMessage t
     m
 
 withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
@@ -122,22 +125,29 @@ withPatternContext Pattern{term, constraints} m =
 
 instance ToLogFormat KorePattern where
     toTextualLog = prettyPattern
+    toJSONLog p = toJSON p
 
 newtype KorePatternCtxt = KorePatternCtxt KorePattern
 
 instance ToLogFormat KorePatternCtxt where
     toTextualLog (KorePatternCtxt t) = "term " <> (showHashHex $ Data.Hashable.hash $ prettyPattern t)
+    toJSONLog (KorePatternCtxt t) = object ["term" .= (showHashHex $ Data.Hashable.hash $ prettyPattern t)]
 
 instance KnownSymbol k => ToLogFormat (RewriteRule k) where
     toTextualLog RewriteRule{attributes} =
         LazyText.toStrict $
             (LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k))
                 <> " "
                 <> maybe "UNKNOWN" (LazyText.take 7 . LazyText.fromStrict . coerce) attributes.uniqueId
+    toJSONLog RewriteRule{attributes} =
+        object
+            [ (Key.fromText $ LazyText.toStrict $ LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k))
+                .= ((maybe "UNKNOWN" coerce attributes.uniqueId) :: Text)
+            ]
 
 withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a
 withKorePatternContext t m = withContext (LogContext $ KorePatternCtxt t) $ do
-    withContext "detail" $ logMessage t
+    withContext "kore-term" $ logMessage t
     m
 
 withRuleContext :: KnownSymbol tag => LoggerMIO m => RewriteRule tag -> m a -> m a
@@ -149,16 +159,47 @@ withRuleContext rule m = withContext (LogContext rule) $ do
         loc -> loc
     m
 
-newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a}
-    deriving newtype (Applicative, Functor, Monad, MonadIO, MonadLogger, MonadLoggerIO)
+data WithJsonMessage where
+    WithJsonMessage :: ToLogFormat a => Value -> a -> WithJsonMessage
+
+instance ToLogFormat WithJsonMessage where
+    toTextualLog (WithJsonMessage _ a) = toTextualLog a
+    toJSONLog (WithJsonMessage v _) = v
 
-instance MonadLoggerIO m => LoggerMIO (LoggerT m) where
+newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a}
+    deriving newtype
+        ( Applicative
+        , Functor
+        , Monad
+        , MonadIO
+        , Control.Monad.Logger.MonadLogger
+        , Control.Monad.Logger.MonadLoggerIO
+        )
+
+instance MonadIO m => LoggerMIO (LoggerT m) where
     getLogger = LoggerT ask
     withLogger modL (LoggerT m) = LoggerT $ withReaderT modL m
 
-runLogger :: MonadLoggerIO m => LoggerT m a -> m a
-runLogger (LoggerT m) = do
-    l <- askLoggerIO
-    runReaderT m $ Logger $ \(LogMessage ctxts msg) ->
-        let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts
-         in l defaultLoc "" (LevelOther logLevel) $ toLogStr $ toTextualLog msg
+textLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
+textLogger l = Logger $ \(LogMessage ctxts msg) ->
+    let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts
+     in l $
+            "["
+                <> (Control.Monad.Logger.toLogStr logLevel)
+                <> "] "
+                <> (Control.Monad.Logger.toLogStr $ toTextualLog msg)
+                <> "\n"
+
+jsonLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
+jsonLogger l = Logger $ \(LogMessage ctxts msg) ->
+    let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts
+     in liftIO $
+            l $
+                ( Control.Monad.Logger.toLogStr $
+                    encodePretty' rpcJsonConfig{confIndent = Spaces 0} $
+                        object ["context" .= ctxt, "message" .= toJSONLog msg]
+                )
+                    <> "\n"
+
+filterLogger :: (LogMessage -> Bool) -> Logger LogMessage -> Logger LogMessage
+filterLogger p (Logger l) = Logger $ \m -> when (p m) $ l m

booster/library/Booster/Log/Context.hs

@@ -0,0 +1,81 @@
+module Booster.Log.Context (ContextFilter, mustMatch, readContextFilter, readMatch) 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.List.Extra (replace)
+
+data ContextFilterSingle
+    = Exact BS.ByteString
+    | Prefix BS.ByteString
+    | Suffix BS.ByteString
+    | Infix BS.ByteString
+    | Negate ContextFilterSingle
+    deriving (Show)
+
+data ContextFilter
+    = First [ContextFilterSingle]
+    | ThenDirectChild [ContextFilterSingle] ContextFilter
+    | ThenChild [ContextFilterSingle] ContextFilter
+    | Last [ContextFilterSingle]
+    deriving (Show)
+
+reserved :: String
+reserved = "|*!>,."
+
+stringP :: A.Parser BS.ByteString
+stringP = A.takeWhile1 (not . (`elem` reserved))
+
+singleP :: A.Parser ContextFilterSingle
+singleP =
+    A.char '!' *> A.skipSpace *> (Negate <$> singleP)
+        <|> A.char '*' *> (Infix <$> stringP) <* A.char '*'
+        -- we want to allow * being parsed as `Suffix ""` so we allow the empty string via `takeWhile`
+        <|> A.char '*' *> (Suffix . BS.dropWhileEnd isSpace <$> A.takeWhile (not . (`elem` reserved)))
+        <|> Prefix . BS.dropWhile isSpace <$> stringP <* A.char '*'
+        <|> Exact . BS.strip <$> stringP
+
+orP :: A.Parser [ContextFilterSingle]
+orP = singleP `A.sepBy` (A.char '|')
+
+contextFilterP :: A.Parser ContextFilter
+contextFilterP =
+    A.skipSpace
+        *> ( ThenChild <$> (orP <* A.skipSpace <* A.char '>') <*> contextFilterP
+                <|> ThenDirectChild <$> (orP <* A.skipSpace <* A.char ',') <*> contextFilterP
+                <|> Last <$> (orP <* A.skipSpace <* A.char '.')
+                <|> First <$> orP
+           )
+
+readContextFilter :: String -> Either String ContextFilter
+readContextFilter =
+    A.parseOnly (contextFilterP <* A.skipSpace <* A.endOfInput) . BS.pack . replace "\"" ""
+
+matchSingle :: ContextFilterSingle -> BS.ByteString -> Bool
+matchSingle (Exact c) s = c == s
+matchSingle (Prefix c) s = BS.isPrefixOf c s
+matchSingle (Suffix c) s = BS.isSuffixOf c s
+matchSingle (Infix c) s = BS.isInfixOf c s
+matchSingle (Negate c) s = not $ matchSingle c s
+
+mustMatch :: ContextFilter -> [BS.ByteString] -> Bool
+mustMatch (First cs) [] = any (flip matchSingle "") cs
+mustMatch (First cs) (x : _) = any (flip matchSingle x) cs
+mustMatch (Last cs) [x] = any (flip matchSingle x) cs
+mustMatch Last{} _ = False
+mustMatch (_ `ThenDirectChild` _) [] = False
+mustMatch (cs `ThenDirectChild` css) (x : xs) =
+    any (flip matchSingle x) cs && mustMatch css xs
+mustMatch (_ `ThenChild` _) [] = False
+mustMatch (cs `ThenChild` css) (x : xs) =
+    any (flip matchSingle x) cs && mayMatch css xs
+
+mayMatch :: ContextFilter -> [BS.ByteString] -> Bool
+mayMatch c [] = mustMatch c []
+mayMatch c (x : xs) = mustMatch c (x : xs) || mayMatch c xs
+
+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