Use typed log context in kore, add optional timestamp (with flexible parsing) (#3967)

Author: jberthold

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

@@ -57,8 +57,8 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
-{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
+{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}

booster/tools/booster/Server.hs

@@ -22,6 +22,7 @@ import Control.Monad.Logger (
 import Control.Monad.Trans.Reader (runReaderT)
 import Data.Aeson qualified as JSON
 import Data.Bifunctor (bimap)
+import Data.ByteString.Char8 qualified as BS
 import Data.Coerce (coerce)
 import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
@@ -176,7 +177,7 @@ main = do
                 not contextLoggingEnabled
                     || ( let contextStrs =
                                 concatMap
-                                    ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
+                                    ( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
                                     )
                                     ctxt
                           in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts
@@ -508,7 +509,7 @@ translateSMTOpts = \case
 mkKoreServer ::
     Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
-    flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext "kore") $ do
+    flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext $ Log.CLNullary CtxKore) $ do
         sd@GlobalMain.SerializedDefinition{internedTextCache} <-
             GlobalMain.deserializeDefinition
                 koreSolverOptions

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

@@ -19,6 +19,7 @@ import Control.Monad.Logger (
  )
 import Control.Monad.Trans.Reader (runReaderT)
 import Data.Aeson.Types (Value (..))
+import Data.ByteString.Char8 qualified as BS
 import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
@@ -187,7 +188,7 @@ main = do
                     null logContextsWithcustomLevelContexts
                         || ( let contextStrs =
                                     concatMap
-                                        ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
+                                        ( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
                                         )
                                         ctxt
                               in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts

kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs

@@ -8,13 +8,18 @@ module Kore.JsonRpc.Types.ContextLog (
     module Kore.JsonRpc.Types.ContextLog,
 ) where
 
+import Control.Applicative ((<|>))
+import Data.Aeson ((.:), (.:?), (.=))
 import Data.Aeson.TH (deriveJSON)
 import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
 import Data.Aeson.Types qualified as JSON
 import Data.Data (Data, toConstr)
 import Data.Sequence (Seq)
 import Data.Text (Text, unpack)
 import Data.Text qualified as Text
+import Data.Time.Clock.System (SystemTime (..), systemToUTCTime, utcToSystemTime)
+import Data.Time.Format (defaultTimeLocale, formatTime, parseTimeM)
+import Text.Read (readMaybe)
 
 data SimpleContext
     = -- component
@@ -30,6 +35,7 @@ data SimpleContext
     | -- mode/phase
       CtxInternalise
     | CtxMatch
+    | CtxUnify
     | CtxDefinedness
     | CtxConstraint
     | CtxSMT
@@ -45,6 +51,7 @@ data SimpleContext
       CtxKoreTerm
     | CtxDetail
     | CtxSubstitution
+    | CtxRemainder
     | CtxDepth
     | CtxTiming
     | -- standard log levels
@@ -183,9 +190,50 @@ instance ToJSON CLMessage where
     toJSON (CLValue value) = value
 
 data LogLine = LogLine
-    { context :: Seq CLContext
+    { timestamp :: Maybe SystemTime
+    , context :: Seq CLContext
     , message :: CLMessage
     }
     deriving stock (Show, Eq)
 
-$(deriveJSON defaultOptions ''LogLine)
+instance FromJSON LogLine where
+    parseJSON = JSON.withObject "LogLine" $ \l ->
+        LogLine
+            <$> (l .:? "timestamp" >>= parseTimestamp)
+            <*> l .: "context"
+            <*> l .: "message"
+
+parseTimestamp :: Maybe JSON.Value -> JSON.Parser (Maybe SystemTime)
+parseTimestamp Nothing = pure Nothing
+parseTimestamp (Just x) =
+    JSON.withScientific "numeric timestamp" (pure . Just . fromNumeric) x
+        <|> JSON.withText "human-readable timestamp" fromString x
+        <|> JSON.withText "nanosecond timestamp" fromNanos x
+  where
+    -- fromNumeric :: Scientific -> SystemTime
+    fromNumeric n =
+        let seconds = truncate n
+            nanos = truncate $ 1e9 * (n - fromIntegral seconds) -- no leap seconds
+         in MkSystemTime seconds nanos
+    fromString s = do
+        utc <- parseTimeM False defaultTimeLocale timestampFormat (Text.unpack s)
+        pure . Just $ utcToSystemTime utc
+    fromNanos s =
+        case readMaybe (Text.unpack s) of
+            Nothing -> fail $ "bad number " <> show s
+            Just (n :: Integer) -> pure . Just $ fromNumeric (fromIntegral n :: Double)
+
+instance ToJSON LogLine where
+    toJSON LogLine{timestamp, context, message} =
+        JSON.object $
+            maybe
+                []
+                (\t -> ["timestamp" .= formatted t])
+                timestamp
+                <> ["context" .= context, "message" .= message]
+      where
+        formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime
+
+-- same format as the one used in Booster.Util
+timestampFormat :: String
+timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q"

kore/src/Kore/Equation/Application.hs

@@ -89,7 +89,7 @@ import Kore.Internal.TermLike (
     TermLike,
  )
 import Kore.Internal.TermLike qualified as TermLike
-import Kore.Log.DebugContext (inContext)
+import Kore.Log.DebugContext (SimpleContext (CtxConstraint), inContext)
 import Kore.Log.DecidePredicateUnknown (
     OnDecidePredicateUnknown (..),
     srcLoc,
@@ -362,7 +362,7 @@ checkRequires ::
     Predicate RewritingVariableName ->
     ExceptT (CheckRequiresError RewritingVariableName) Simplifier ()
 checkRequires onUnknown sideCondition predicate requires =
-    inContext "constraint" $
+    inContext CtxConstraint $
         do
             let requires' = makeAndPredicate predicate requires
                 -- The condition to refute:

kore/src/Kore/Equation/DebugEquation.hs

@@ -36,7 +36,6 @@ import Data.Text (
     Text,
  )
 import Data.Text qualified as Text
-import Data.Vector qualified as Vec
 import Debug
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
@@ -48,7 +47,7 @@ import Kore.Attribute.SourceLocation (
  )
 import Kore.Equation.Equation (Equation (..))
 import Kore.Internal.OrCondition (OrCondition)
-import Kore.Internal.Pattern (Conditional (..), Pattern)
+import Kore.Internal.Pattern (Conditional (..), Pattern, toTermLike)
 import Kore.Internal.Predicate (Predicate)
 import Kore.Internal.SideCondition (SideCondition)
 import Kore.Internal.TermLike (
@@ -294,10 +293,14 @@ instance Entry DebugAttemptEquation where
     helpDoc _ = "log equation application attempts"
 
     oneLineContextDoc = \case
-        _entry@DebugAttemptEquation{} -> ["detail"]
+        _entry@DebugAttemptEquation{} -> single CtxDetail
         (DebugAttemptEquationResult _ result) -> case result of
-            Right Conditional{term} -> ["success", "term " <> (showHashHex $ hash term), "kore-term"]
-            Left{} -> ["failure"]
+            Right Conditional{term} ->
+                [ CLNullary CtxSuccess
+                , CtxTerm `withShortId` showHashHex (hash term)
+                , CLNullary CtxKoreTerm
+                ]
+            Left{} -> single CtxFailure
 
     oneLineDoc (DebugAttemptEquation equation _term) =
         maybe
@@ -310,21 +313,6 @@ instance Entry DebugAttemptEquation where
         Right Conditional{term} -> " " <> unparse term
         Left failure -> " " <> Pretty.pretty (failureDescription failure)
 
-    oneLineContextJson = \case
-        _entry@DebugAttemptEquation{} -> JSON.String "detail"
-        _entry@(DebugAttemptEquationResult _equation result) ->
-            case result of
-                Right Conditional{term} ->
-                    JSON.Array $
-                        Vec.fromList
-                            [ JSON.String "success"
-                            , JSON.object
-                                [ "term" JSON..= showHashHex (hash term)
-                                ]
-                            , JSON.String "kore-term"
-                            ]
-                Left _failure -> JSON.String "failure"
-
     oneLineJson = \case
         _entry@(DebugAttemptEquation equation _term) ->
             JSON.toJSON $ renderDefault (maybe "UNKNOWN" pretty (srcLoc equation))
@@ -350,12 +338,7 @@ instance Entry DebugTermContext where
     oneLineDoc DebugTermContext{} = mempty
 
     oneLineContextDoc (DebugTermContext term) =
-        ["term " <> (showHashHex $ hash term)]
-
-    oneLineContextJson (DebugTermContext term) =
-        JSON.object
-            [ "term" JSON..= showHashHex (hash term)
-            ]
+        [CtxTerm `withShortId` showHashHex (hash term)]
 
     oneLineJson :: DebugTermContext -> JSON.Value
     oneLineJson DebugTermContext{} =
@@ -366,13 +349,7 @@ instance Entry DebugTerm where
 
     oneLineDoc (DebugTerm term) = unparse term
 
-    oneLineContextDoc DebugTerm{} =
-        ["kore-term"]
-
-    oneLineContextJson DebugTerm{} =
-        JSON.toJSON
-            [ "kore-term" :: Text
-            ]
+    oneLineContextDoc DebugTerm{} = single CtxKoreTerm
 
     oneLineJson (DebugTerm term) =
         JSON.toJSON $ Kore.Syntax.Json.fromTermLike (getRewritingTerm term)
@@ -383,18 +360,9 @@ instance Entry DebugEquation where
     oneLineDoc _ = mempty
 
     oneLineContextDoc (DebugEquation equation) =
-        let equationKindTxt = if isSimplification equation then "simplification" else "function"
-         in [ equationKindTxt <> " " <> shortRuleIdText equation
-            ]
-    oneLineContextJson (DebugEquation equation) =
-        let equationKindTxt = if isSimplification equation then "simplification" else "function"
-         in JSON.Array $
-                Vec.fromList
-                    [ JSON.object
-                        [ equationKindTxt
-                            JSON..= ruleIdText equation
-                        ]
-                    ]
+        let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
+         in [equationKind `withId` ruleIdText equation]
+
     oneLineJson _ = JSON.Null
 
 whileDebugTerm ::
@@ -485,7 +453,16 @@ instance Entry DebugApplyEquation where
                 ]
     helpDoc _ = "log equation application successes"
 
-    oneLineJson _ = JSON.Null
+    oneLineContextDoc (DebugApplyEquation equation result) =
+        let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
+         in [ equationKind `withId` ruleIdText equation
+            , CLNullary CtxSuccess
+            , CtxTerm `withShortId` showHashHex (hash result)
+            , CLNullary CtxKoreTerm
+            ]
+
+    oneLineJson (DebugApplyEquation _ result) =
+        JSON.toJSON $ Kore.Syntax.Json.fromTermLike . getRewritingTerm $ toTermLike result
 
 {- | Log when an 'Equation' is actually applied.
 

kore/src/Kore/JsonRpc.hs

@@ -162,24 +162,22 @@ respond reqId serverState moduleName runSMT =
                         traversalResult <-
                             liftIO
                                 ( runSMT (Exec.metadataTools serializedModule) lemmas $
-                                    Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) $
-                                        Log.logWhile (Log.DebugContext "kore") $
-                                            Log.logWhile (Log.DebugContext "execute") $
-                                                Exec.rpcExec
-                                                    (maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
-                                                    (coerce stepTimeout)
-                                                    ( if fromMaybe False movingAverageStepTimeout
-                                                        then EnableMovingAverage
-                                                        else DisableMovingAverage
-                                                    )
-                                                    ( if fromMaybe False assumeStateDefined
-                                                        then EnableAssumeInitialDefined
-                                                        else DisableAssumeInitialDefined
-                                                    )
-                                                    tracingEnabled
-                                                    serializedModule
-                                                    (toStopLabels cutPointRules terminalRules)
-                                                    verifiedPattern
+                                    withContextLog Log.CtxExecute $
+                                        Exec.rpcExec
+                                            (maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
+                                            (coerce stepTimeout)
+                                            ( if fromMaybe False movingAverageStepTimeout
+                                                then EnableMovingAverage
+                                                else DisableMovingAverage
+                                            )
+                                            ( if fromMaybe False assumeStateDefined
+                                                then EnableAssumeInitialDefined
+                                                else DisableAssumeInitialDefined
+                                            )
+                                            tracingEnabled
+                                            serializedModule
+                                            (toStopLabels cutPointRules terminalRules)
+                                            verifiedPattern
                                 )
 
                         stop <- liftIO $ getTime Monotonic
@@ -433,9 +431,7 @@ respond reqId serverState moduleName runSMT =
                     result <-
                         liftIO
                             . runSMT (Exec.metadataTools serializedModule) lemmas
-                            . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
-                            . Log.logWhile (Log.DebugContext "kore")
-                            . Log.logWhile (Log.DebugContext "implies")
+                            . withContextLog Log.CtxImplies
                             . evalInSimplifierContext serializedModule
                             . runExceptT
                             $ Claim.checkSimpleImplication
@@ -518,9 +514,7 @@ respond reqId serverState moduleName runSMT =
                     result <-
                         liftIO
                             . runSMT (Exec.metadataTools serializedModule) lemmas
-                            . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
-                            . Log.logWhile (Log.DebugContext "kore")
-                            . Log.logWhile (Log.DebugContext "simplify")
+                            . withContextLog Log.CtxSimplify
                             . evalInSimplifierContext serializedModule
                             $ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt
 
@@ -616,9 +610,7 @@ respond reqId serverState moduleName runSMT =
                         serializedModule <-
                             liftIO
                                 . runSMT metadataTools lemmas
-                                . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
-                                . Log.logWhile (Log.DebugContext "kore")
-                                . Log.logWhile (Log.DebugContext "add-module")
+                                . withContextLog Log.CtxAddModule
                                 $ Exec.makeSerializedModule newModule
                         internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache
 
@@ -677,9 +669,7 @@ respond reqId serverState moduleName runSMT =
                                 else
                                     liftIO
                                         . runSMT tools lemmas
-                                        . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
-                                        . Log.logWhile (Log.DebugContext "kore")
-                                        . Log.logWhile (Log.DebugContext "get-model")
+                                        . withContextLog Log.CtxGetModel
                                         . SMT.Evaluator.getModelFor tools
                                         $ NonEmpty.fromList preds
 
@@ -706,6 +696,12 @@ respond reqId serverState moduleName runSMT =
         -- this case is only reachable if the cancel appeared as part of a batch request
         Cancel -> pure $ Left cancelUnsupportedInBatchMode
   where
+    withContextLog :: Log.SimpleContext -> SMT.SMT a -> SMT.SMT a
+    withContextLog method =
+        Log.logWhile (Log.DebugContext $ Log.CLWithId $ Log.CtxRequest $ Text.pack reqId)
+            . Log.inContext Log.CtxKore
+            . Log.inContext method
+
     withMainModule module' act = do
         let mainModule = fromMaybe moduleName module'
         ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState