From 912cbe60b6f55a264112baf8110c86746c726fb5 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 27 May 2024 15:25:29 +0200 Subject: [PATCH] Increase timestamp resolution (#3893) This PR: - customizes the default timestamp caching mechanism provided by the `fast-logger` package, allowing finer granularity - adds `--timestamp-format` CLI argument to `booster-dev` and `kore-rpc-booster`, with two possible values: `pretty` and `nanoseconds`. `pretty` is the default. --------- Co-authored-by: Sam Balco --- booster/library/Booster/CLOptions.hs | 29 ++++++++++++++++++++ booster/library/Booster/Util.hs | 40 ++++++++++++++++++++++++++++ booster/package.yaml | 2 ++ booster/tools/booster/Server.hs | 8 ++++-- dev-tools/booster-dev/Server.hs | 21 ++++++++++++--- 5 files changed, 94 insertions(+), 6 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index f9739c8692..e7dec2ab8d 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -5,6 +5,7 @@ module Booster.CLOptions ( CLOptions (..), EquationOptions (..), LogFormat (..), + TimestampFormat (..), clOptionsParser, adjustLogLevels, levelToContext, @@ -40,6 +41,7 @@ data CLOptions = CLOptions , port :: Int , logLevels :: [LogLevel] , logTimeStamps :: Bool + , timeStampsFormat :: TimestampFormat , logFormat :: LogFormat , logContexts :: [ContextFilter] , logFile :: Maybe FilePath @@ -63,6 +65,16 @@ instance Show LogFormat where Standard -> "standard" Json -> "json" +data TimestampFormat + = Pretty + | Nanoseconds + deriving (Eq, Enum) + +instance Show TimestampFormat where + show = \case + Pretty -> "pretty" + Nanoseconds -> "nanoseconds" + clOptionsParser :: Parser CLOptions clOptionsParser = CLOptions @@ -104,6 +116,17 @@ clOptionsParser = ) ) <*> switch (long "log-timestamps" <> help "Add timestamps to logs") + <*> option + (eitherReader readTimeStampFormat) + ( metavar "TIMESTAMPFORMAT" + <> value Pretty + <> long "timestamp-format" + <> help + ( "Format to output log timestamps in. Available formats: " + <> intercalate ", " (map show $ enumFrom (toEnum @TimestampFormat 0)) + ) + <> showDefault + ) <*> option (eitherReader readLogFormat) ( metavar "LOGFORMAT" @@ -178,6 +201,12 @@ clOptionsParser = "json" -> Right Json other -> Left $ other <> ": Unsupported log format" + readTimeStampFormat :: String -> Either String TimestampFormat + readTimeStampFormat = \case + "pretty" -> Right Pretty + "nanoseconds" -> Right Nanoseconds + other -> Left $ other <> ": Unsupported timestamp format" + readCellName :: String -> Either String Text readCellName input | null input = diff --git a/booster/library/Booster/Util.hs b/booster/library/Booster/Util.hs index 17ec4dc336..e742bd0be7 100644 --- a/booster/library/Booster/Util.hs +++ b/booster/library/Booster/Util.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveLift #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} module Booster.Util ( @@ -11,18 +12,25 @@ module Booster.Util ( constructorName, handleOutput, withFastLogger, + newTimeCache, + pattern PrettyTimestamps, + pattern NoPrettyTimestamps, ) where +import Control.AutoUpdate (defaultUpdateSettings, mkAutoUpdate, updateAction, updateFreq) import Control.DeepSeq (NFData (..)) import Control.Exception (bracket, catch, throwIO) import Control.Monad.Logger.CallStack qualified as Log import Data.ByteString (ByteString) import Data.ByteString.Char8 qualified as BS +import Data.Coerce (coerce) import Data.Data import Data.Either (fromRight) import Data.Hashable (Hashable) import Data.Map qualified as Map import Data.Maybe (fromMaybe) +import Data.Time.Clock.System (SystemTime (..), getSystemTime, systemToUTCTime) +import Data.Time.Format import GHC.Generics (Generic) import Language.Haskell.TH.Syntax (Lift) import System.Directory (removeFile) @@ -163,3 +171,35 @@ withFastLogger mFormattedTime (Just fp) log' = handleExists e | isDoesNotExistError e = return () | otherwise = throwIO e + +{- | Make 'IO' action which get cached formatted local time. +Use this to avoid the cost of frequently time formatting by caching an +auto updating formatted time, this cache update every 100 microseconds. + +Borrowed almost verbatim from the fast-logger package: https://hackage.haskell.org/package/fast-logger-3.2.3/docs/src/System.Log.FastLogger.Date.html#newTimeCache, but the timestamp resolution and the actions to get and format the time are tweaked. +-} +newTimeCache :: Flag "PrettyTimestamp" -> IO (IO FormattedTime) +newTimeCache prettyTimestamp = + mkAutoUpdate + defaultUpdateSettings{updateFreq = 100} + { updateAction = formatSystemTime prettyTimestamp <$> getSystemTime + } + +pattern PrettyTimestamps, NoPrettyTimestamps :: Flag "PrettyTimestamp" +pattern PrettyTimestamps = Flag True +pattern NoPrettyTimestamps = Flag False + +-- | Format time either as a human-readable date and time or as nanoseconds +formatSystemTime :: Flag "PrettyTimestamp" -> SystemTime -> ByteString +formatSystemTime prettyTimestamp = + let formatString = BS.unpack "%Y-%m-%dT%H:%M:%S.%6Q" + formatter = + if coerce prettyTimestamp + then formatTime defaultTimeLocale formatString . systemToUTCTime + else show . toNanoSeconds + in BS.pack . formatter + where + toNanoSeconds :: SystemTime -> Integer + toNanoSeconds MkSystemTime{systemSeconds, systemNanoseconds} = + fromIntegral @_ @Integer systemSeconds * (10 :: Integer) ^ (9 :: Integer) + + fromIntegral @_ @Integer systemNanoseconds diff --git a/booster/package.yaml b/booster/package.yaml index 35d09733d2..210d9e0bef 100644 --- a/booster/package.yaml +++ b/booster/package.yaml @@ -60,6 +60,7 @@ library: - aeson-pretty - array - attoparsec + - auto-update - base - binary - bytestring @@ -98,6 +99,7 @@ library: - text - transformers - unix + - time - unliftio - unordered-containers source-dirs: library diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 35aac79d79..8a3a669214 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -48,7 +48,6 @@ import System.Clock ( import System.Environment qualified as Env import System.Exit import System.IO (hPutStrLn, stderr) -import System.Log.FastLogger (newTimeCache) import Booster.CLOptions import Booster.Definition.Attributes.Base ( @@ -134,6 +133,7 @@ main = do , logLevels , logFormat , logTimeStamps + , timeStampsFormat , logContexts , logFile , smtOptions @@ -161,8 +161,12 @@ main = do lvl `elem` customLevels || lvl >= logLevel && lvl <= LevelError koreSolverOptions = translateSMTOpts smtOptions + timestampFlag = case timeStampsFormat of + Pretty -> Booster.PrettyTimestamps + Nanoseconds -> Booster.NoPrettyTimestamps - mTimeCache <- if logTimeStamps then Just <$> (newTimeCache "%Y-%m-%d %T") else pure Nothing + mTimeCache <- + if logTimeStamps then Just <$> Booster.newTimeCache timestampFlag else pure Nothing Booster.withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do flip runLoggingT (handleOutput stderrLogger) . Logger.filterLogger levelFilter $ do diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs index 9d19b50eae..2d96f21fc5 100644 --- a/dev-tools/booster-dev/Server.hs +++ b/dev-tools/booster-dev/Server.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternSynonyms #-} + {- | Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause @@ -19,7 +21,6 @@ import Data.Maybe (fromMaybe, isNothing) import Data.Text (Text, unpack) import Data.Text.Encoding qualified as Text import Options.Applicative -import System.Log.FastLogger (newTimeCache) import Booster.CLOptions import Booster.Definition.Base (KoreDefinition (..)) @@ -33,7 +34,13 @@ import Booster.Log.Context qualified as Booster.Log import Booster.SMT.Interface qualified as SMT import Booster.Syntax.ParsedKore (loadDefinition) import Booster.Trace -import Booster.Util (handleOutput, withFastLogger) +import Booster.Util ( + handleOutput, + newTimeCache, + withFastLogger, + pattern NoPrettyTimestamps, + pattern PrettyTimestamps, + ) import Kore.JsonRpc.Error qualified as RpcError import Kore.JsonRpc.Server @@ -47,6 +54,7 @@ main = do , logLevels , logContexts , logTimeStamps + , timeStampsFormat , logFormat , llvmLibraryFile , smtOptions @@ -88,6 +96,7 @@ main = do (adjustLogLevels logLevels) logContexts logTimeStamps + timeStampsFormat logFormat where withLlvmLib libFile m = case libFile of @@ -117,11 +126,15 @@ runServer :: (LogLevel, [LogLevel]) -> [Booster.Log.ContextFilter] -> Bool -> + TimestampFormat -> LogFormat -> IO () -runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLevel, customLevels) logContexts logTimeStamps logFormat = +runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat = do - mTimeCache <- if logTimeStamps then Just <$> (newTimeCache "%Y-%m-%d %T") else pure Nothing + let timestampFlag = case timeStampsFormat of + Pretty -> PrettyTimestamps + Nanoseconds -> NoPrettyTimestamps + mTimeCache <- if logTimeStamps then Just <$> newTimeCache timestampFlag else pure Nothing withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do let boosterContextLogger = case logFormat of