Skip to content

Commit 73fbce6

Browse files
goodlyrottenapplerv-jenkins
goodlyrottenapple
and
rv-jenkins
authored
Add timestampts to JSON logs (#3925)
Fixes #3894 --------- Co-authored-by: rv-jenkins <admin@runtimeverification.com>
1 parent bcbaf63 commit 73fbce6

File tree

10 files changed

+113
-143
lines changed

10 files changed

+113
-143
lines changed

‎booster/library/Booster/Log.hs‎

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,10 @@ import Booster.Prettyprinter (renderOneLineText)
4444
import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
4545
import Booster.Syntax.Json.Externalise (externaliseTerm)
4646
import Booster.Util (Flag (..))
47+
import Data.Text.Encoding (decodeUtf8)
4748
import Kore.JsonRpc.Types (rpcJsonConfig)
4849
import Kore.Util (showHashHex)
50+
import System.Log.FastLogger (FormattedTime)
4951
import UnliftIO (MonadUnliftIO)
5052

5153
newtype Logger a = Logger (a -> IO ())
@@ -192,24 +194,32 @@ instance MonadIO m => LoggerMIO (LoggerT m) where
192194
getLogger = LoggerT ask
193195
withLogger modL (LoggerT m) = LoggerT $ withReaderT modL m
194196

195-
textLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
197+
textLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage
196198
textLogger l = Logger $ \(LogMessage _ ctxts msg) ->
197199
let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts
198-
in l $
199-
"["
200+
in l $ \mTime ->
201+
( case mTime of
202+
Nothing -> mempty
203+
Just t -> Control.Monad.Logger.toLogStr t <> " "
204+
)
205+
<> "["
200206
<> (Control.Monad.Logger.toLogStr logLevel)
201207
<> "] "
202208
<> (Control.Monad.Logger.toLogStr $ toTextualLog msg)
203209
<> "\n"
204210

205-
jsonLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
211+
jsonLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage
206212
jsonLogger l = Logger $ \(LogMessage _ ctxts msg) ->
207213
let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts
208214
in liftIO $
209-
l $
215+
l $ \mTime ->
210216
( Control.Monad.Logger.toLogStr $
211217
encodePretty' rpcJsonConfig{confIndent = Spaces 0} $
212-
object ["context" .= ctxt, "message" .= toJSONLog msg]
218+
object $
219+
["context" .= ctxt, "message" .= toJSONLog msg]
220+
<> case mTime of
221+
Nothing -> []
222+
Just t -> ["timestamp" .= decodeUtf8 t]
213223
)
214224
<> "\n"
215225

‎booster/library/Booster/Util.hs‎

Lines changed: 16 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module Booster.Util (
1010
Flag (..),
1111
Bound (..),
1212
constructorName,
13-
handleOutput,
1413
withFastLogger,
1514
newTimeCache,
1615
pattern PrettyTimestamps,
@@ -20,32 +19,27 @@ module Booster.Util (
2019
import Control.AutoUpdate (defaultUpdateSettings, mkAutoUpdate, updateAction, updateFreq)
2120
import Control.DeepSeq (NFData (..))
2221
import Control.Exception (bracket, catch, throwIO)
23-
import Control.Monad.Logger.CallStack qualified as Log
2422
import Data.ByteString (ByteString)
2523
import Data.ByteString.Char8 qualified as BS
26-
import Data.Char (toLower)
2724
import Data.Coerce (coerce)
2825
import Data.Data
2926
import Data.Either (fromRight)
3027
import Data.Hashable (Hashable)
3128
import Data.Map qualified as Map
3229
import Data.Maybe (fromMaybe)
33-
import Data.Text qualified as Text
3430
import Data.Time.Clock.System (SystemTime (..), getSystemTime, systemToUTCTime)
3531
import Data.Time.Format
3632
import GHC.Generics (Generic)
3733
import Language.Haskell.TH.Syntax (Lift)
3834
import System.Directory (removeFile)
3935
import System.IO.Error (isDoesNotExistError)
4036
import System.Log.FastLogger (
41-
FastLogger,
4237
LogStr,
4338
LogType,
4439
LogType' (..),
4540
defaultBufSize,
4641
newFastLogger,
4742
newTimedFastLogger,
48-
toLogStr,
4943
)
5044
import System.Log.FastLogger.Types (FormattedTime)
5145

@@ -133,34 +127,25 @@ encodeLabel = BS.concatMap encodeChar
133127
encodeChar c = fromMaybe (BS.singleton c) $ Map.lookup c encodeMap
134128

135129
-------------------------------------------------------------------
136-
-- logging helpers, some are adapted from monad-logger-aeson
137-
handleOutput ::
138-
FastLogger ->
139-
Log.Loc ->
140-
Log.LogSource ->
141-
Log.LogLevel ->
142-
Log.LogStr ->
143-
IO ()
144-
handleOutput stderrLogger _loc src level msg =
145-
stderrLogger $ prettySrc <> prettyLevel <> " " <> msg <> "\n"
146-
where
147-
prettySrc = if Text.null src then mempty else "[" <> toLogStr src <> "]"
148-
prettyLevel = case level of
149-
Log.LevelOther t -> "[" <> toLogStr t <> "]"
150-
Log.LevelInfo -> mempty
151-
_ -> "[" <> (toLogStr $ BS.pack $ map toLower $ drop 5 $ show level) <> "]"
152-
153-
newFastLoggerMaybeWithTime :: Maybe (IO FormattedTime) -> LogType -> IO (LogStr -> IO (), IO ())
154-
newFastLoggerMaybeWithTime = \case
155-
Nothing -> newFastLogger
156-
Just formattedTime -> \typ -> do
130+
-- logging helpers
131+
132+
newFastLoggerMaybeWithTime ::
133+
Maybe (IO FormattedTime) -> LogType -> IO ((Maybe FormattedTime -> LogStr) -> IO (), IO ())
134+
newFastLoggerMaybeWithTime mTimer typ = case mTimer of
135+
Nothing -> do
136+
(logger, cleanup) <- newFastLogger typ
137+
pure (\mkMsg -> logger $ mkMsg Nothing, cleanup)
138+
Just formattedTime -> do
157139
(logger, cleanup) <- newTimedFastLogger formattedTime typ
158-
pure (\msg -> logger (\time -> toLogStr time <> " " <> msg), cleanup)
140+
pure (\mkMsg -> logger $ mkMsg . Just, cleanup)
159141

160142
withFastLogger ::
161143
Maybe (IO FormattedTime) ->
162144
Maybe FilePath ->
163-
(FastLogger -> Maybe FastLogger -> IO a) ->
145+
( ((Maybe FormattedTime -> LogStr) -> IO ()) ->
146+
Maybe ((Maybe FormattedTime -> LogStr) -> IO ()) ->
147+
IO a
148+
) ->
164149
IO a
165150
withFastLogger mFormattedTime Nothing log' =
166151
let typStderr = LogStderr defaultBufSize
@@ -170,7 +155,7 @@ withFastLogger mFormattedTime (Just fp) log' =
170155
typFile = LogFileNoRotate fp defaultBufSize
171156
in bracket (newFastLoggerMaybeWithTime mFormattedTime typStderr) snd $ \(loggerStderr, _) -> do
172157
removeFileIfExists fp
173-
bracket (newFastLogger typFile) snd $ \(loggerFile, _) ->
158+
bracket (newFastLoggerMaybeWithTime mFormattedTime typFile) snd $ \(loggerFile, _) ->
174159
log' loggerStderr (Just loggerFile)
175160
where
176161
removeFileIfExists :: FilePath -> IO ()
@@ -200,7 +185,7 @@ pattern NoPrettyTimestamps = Flag False
200185
-- | Format time either as a human-readable date and time or as nanoseconds
201186
formatSystemTime :: Flag "PrettyTimestamp" -> SystemTime -> ByteString
202187
formatSystemTime prettyTimestamp =
203-
let formatString = BS.unpack "%Y-%m-%dT%H:%M:%S.%6Q"
188+
let formatString = "%Y-%m-%dT%H:%M:%S%6Q"
204189
formatter =
205190
if coerce prettyTimestamp
206191
then formatTime defaultTimeLocale formatString . systemToUTCTime

‎booster/tools/booster/Server.hs‎

Lines changed: 8 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,9 @@ import Control.Monad.Extra (whenJust)
1717
import Control.Monad.IO.Class (MonadIO (liftIO))
1818
import Control.Monad.Logger (
1919
LogLevel (..),
20-
ToLogStr (toLogStr),
2120
runNoLoggingT,
2221
)
2322
import Control.Monad.Trans.Reader (runReaderT)
24-
import Data.Aeson (Value (Null))
2523
import Data.Aeson qualified as JSON
2624
import Data.Bifunctor (bimap)
2725
import Data.Coerce (coerce)
@@ -40,7 +38,6 @@ import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
4038
import Options.Applicative
4139
import System.Clock (
4240
Clock (..),
43-
TimeSpec (..),
4441
getTime,
4542
)
4643
import System.Environment qualified as Env
@@ -84,7 +81,6 @@ import Kore.JsonRpc.Types.Depth (Depth (..))
8481
import Kore.Log.BoosterAdaptor (
8582
ExeName (..),
8683
KoreLogType (..),
87-
LogAction (LogAction),
8884
TimestampsSwitch (TimestampsDisable),
8985
defaultKoreLogOptions,
9086
koreSomeEntryLogAction,
@@ -168,14 +164,12 @@ main = do
168164
enableCustomUserEvent t
169165

170166
let koreLogRenderer = case logFormat of
171-
Standard -> Just . renderStandardPretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
172-
OneLine -> renderOnelinePretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
173-
Json -> renderJson (ExeName "") (TimeSpec 0 0) TimestampsDisable
174-
koreLogEarlyFilter = case logFormat of
175-
Json -> \l@(Log.SomeEntry ctxt e) ->
176-
Log.oneLineJson e /= Null && koreFilterContext (ctxt <> [l])
177-
OneLine -> \l@(Log.SomeEntry ctxt _) -> koreFilterContext $ ctxt <> [l]
167+
Standard -> renderStandardPretty
168+
OneLine -> renderOnelinePretty
169+
Json -> renderJson
170+
koreLogFilter = case logFormat of
178171
Standard -> const True
172+
_ -> \l@(Log.SomeEntry ctxt _) -> not (Log.isEmpty l) && koreFilterContext (ctxt <> [l])
179173
koreFilterContext ctxt =
180174
not contextLoggingEnabled
181175
|| ( let contextStrs =
@@ -205,19 +199,14 @@ main = do
205199
runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a
206200
runBoosterLogger = flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT
207201

208-
koreLogActions :: forall m. MonadIO m => [LogAction m Log.SomeEntry]
202+
koreLogActions :: forall m. MonadIO m => [Log.LogAction m Log.SomeEntry]
209203
koreLogActions = [koreLogAction]
210204
where
211205
koreLogAction =
212206
koreSomeEntryLogAction
213207
koreLogRenderer
214-
koreLogEarlyFilter
215-
(const True)
216-
( LogAction $ \txt -> liftIO $
217-
case mFileLogger of
218-
Just fileLogger -> fileLogger $ toLogStr $ txt <> "\n"
219-
Nothing -> stderrLogger $ toLogStr $ txt <> "\n"
220-
)
208+
koreLogFilter
209+
(fromMaybe stderrLogger mFileLogger)
221210

222211
runBoosterLogger $
223212
Booster.Log.withContext "proxy" $

‎dev-tools/booster-dev/Server.hs‎

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import Control.Exception (evaluate)
1212
import Control.Monad (forM_, when)
1313
import Control.Monad.Logger (runNoLoggingT)
1414
import Control.Monad.Logger qualified as Log
15-
import Control.Monad.Logger.CallStack (LogLevel (LevelError))
15+
import Control.Monad.Logger.CallStack (LogLevel)
1616
import Control.Monad.Trans.Reader (runReaderT)
1717
import Data.Conduit.Network (serverSettings)
1818
import Data.Map (Map)
@@ -35,7 +35,6 @@ import Booster.SMT.Interface qualified as SMT
3535
import Booster.Syntax.ParsedKore (loadDefinition)
3636
import Booster.Trace
3737
import Booster.Util (
38-
handleOutput,
3938
newTimeCache,
4039
withFastLogger,
4140
pattern NoPrettyTimestamps,
@@ -130,7 +129,7 @@ runServer ::
130129
TimestampFormat ->
131130
LogFormat ->
132131
IO ()
133-
runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat =
132+
runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat =
134133
do
135134
let timestampFlag = case timeStampsFormat of
136135
Pretty -> PrettyTimestamps
@@ -157,19 +156,12 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLeve
157156
, mSMTOptions
158157
, addedModules = mempty
159158
}
160-
flip Log.runLoggingT (handleOutput stderrLogger) . Log.filterLogger levelFilter $
161-
jsonRpcServer
162-
srvSettings
163-
( const $
164-
flip runReaderT filteredBoosterContextLogger
165-
. Booster.Log.unLoggerT
166-
. Booster.Log.withContext "booster"
167-
. respond stateVar
168-
)
169-
[handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]
170-
where
171-
levelFilter :: Log.LogSource -> LogLevel -> Bool
172-
levelFilter _source lvl =
173-
lvl `elem` customLevels
174-
|| lvl >= logLevel && lvl <= LevelError
175-
srvSettings = serverSettings port "*"
159+
jsonRpcServer
160+
(serverSettings port "*")
161+
( const $
162+
flip runReaderT filteredBoosterContextLogger
163+
. Booster.Log.unLoggerT
164+
. Booster.Log.withContext "booster"
165+
. respond stateVar
166+
)
167+
[handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]

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

Lines changed: 8 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ import Control.Monad.Catch (bracket)
1616
import Control.Monad.IO.Class (MonadIO (liftIO))
1717
import Control.Monad.Logger (
1818
LogLevel (..),
19-
ToLogStr (toLogStr),
2019
)
2120
import Control.Monad.Trans.Reader (runReaderT)
2221
import Data.Aeson.Types (Value (..))
@@ -33,7 +32,6 @@ import Network.JSONRPC
3332
import Options.Applicative
3433
import System.Clock (
3534
Clock (..),
36-
TimeSpec (..),
3735
getTime,
3836
)
3937
import System.Exit
@@ -61,7 +59,6 @@ import Kore.JsonRpc.Types
6159
import Kore.Log.BoosterAdaptor (
6260
ExeName (..),
6361
KoreLogType (..),
64-
LogAction (LogAction),
6562
TimestampsSwitch (TimestampsDisable),
6663
defaultKoreLogOptions,
6764
koreSomeEntryLogAction,
@@ -174,18 +171,16 @@ main = do
174171
let koreLogActions ::
175172
forall m.
176173
MonadIO m =>
177-
[LogAction m Log.SomeEntry]
174+
[Log.LogAction m Log.SomeEntry]
178175
koreLogActions = [koreLogAction]
179176
where
180177
koreLogRenderer = case logFormat of
181-
Standard -> Just . renderStandardPretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
182-
OneLine -> renderOnelinePretty (ExeName "") (TimeSpec 0 0) TimestampsDisable
183-
Json -> renderJson (ExeName "") (TimeSpec 0 0) TimestampsDisable
184-
koreLogEarlyFilter = case logFormat of
185-
Json -> \l@(Log.SomeEntry ctxt e) ->
186-
Log.oneLineJson e /= Null && koreFilterContext (ctxt <> [l])
187-
OneLine -> \l@(Log.SomeEntry ctxt _) -> koreFilterContext $ ctxt <> [l]
178+
Standard -> renderStandardPretty
179+
OneLine -> renderOnelinePretty
180+
Json -> renderJson
181+
koreLogFilter = case logFormat of
188182
Standard -> const True
183+
_ -> \l@(Log.SomeEntry ctxt _) -> not (Log.isEmpty l) && koreFilterContext (ctxt <> [l])
189184
koreFilterContext ctxt =
190185
null logContextsWithcustomLevelContexts
191186
|| ( let contextStrs =
@@ -199,13 +194,8 @@ main = do
199194
koreLogAction =
200195
koreSomeEntryLogAction
201196
koreLogRenderer
202-
koreLogEarlyFilter
203-
(const True)
204-
( LogAction $ \txt -> liftIO $
205-
case mFileLogger of
206-
Just fileLogger -> fileLogger $ toLogStr $ txt <> "\n"
207-
Nothing -> stderrLogger $ toLogStr $ txt <> "\n"
208-
)
197+
koreLogFilter
198+
(fromMaybe stderrLogger mFileLogger)
209199

210200
coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
211201
koreLogOptions =

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -303,6 +303,7 @@ rpcJsonConfig =
303303
, "moving-average-step-timeout"
304304
, "code"
305305
, "data"
306+
, "timestamp"
306307
, "context"
307308
, "message"
308309
]

‎kore/src/Kore/Equation/DebugEquation.hs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -345,6 +345,8 @@ newtype DebugEquation = DebugEquation (Equation RewritingVariableName)
345345
instance Entry DebugTermContext where
346346
entrySeverity _ = Debug
347347

348+
isEmpty DebugTermContext{} = True
349+
348350
oneLineDoc DebugTermContext{} = mempty
349351

350352
oneLineContextDoc (DebugTermContext term) =
@@ -355,6 +357,7 @@ instance Entry DebugTermContext where
355357
[ "term" JSON..= showHashHex (hash term)
356358
]
357359

360+
oneLineJson :: DebugTermContext -> JSON.Value
358361
oneLineJson DebugTermContext{} =
359362
JSON.Null
360363

0 commit comments

Comments
 (0)