From bb7b134e45a001a2aaf4db889cea9fb068df344c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 9 Jul 2024 20:47:07 +1000 Subject: [PATCH] Start of a log processing tool (#3969) First version so we get a baseline for additional code to add later. ## Supported commands: ### `filter CONTEXT_FILTER [CONTEXT_FILTER]` filters the log on stdin or given in file option `-i` ``` $ .build/kore/bin/process-logs filter "proxy>timing." "proxy." -i log-with-timestamps.json {"timestamp":"2024-07-05T02:04:09.646316","context":["proxy"],"message":"Loading definition from ./definition.kore, main module \"MX-WASM\""} {"timestamp":"2024-07-05T02:04:16.971803","context":["proxy"],"message":"Starting RPC server"} {"timestamp":"2024-07-05T02:05:32.49184","context":["proxy"],"message":"Processing request 1"} {"timestamp":"2024-07-05T02:05:32.49184","context":["proxy"],"message":"Starting execute request"} {"timestamp":"2024-07-05T02:05:43.138762","context":["proxy"],"message":"Booster Stuck at Depth {getNat = 0}"} {"timestamp":"2024-07-05T02:05:43.138762","context":["proxy"],"message":"Simplifying booster state and falling back to Kore"} {"timestamp":"2024-07-05T02:05:43.138762","context":["proxy"],"message":"Simplifying execution state"} {"timestamp":"2024-07-05T02:07:00.127314","context":["proxy","timing"],"message":{"kore-time":7.205059572e7,"method":"SimplifyM","time":7.6988472523e7}} {"timestamp":"2024-07-05T02:07:00.481663","context":["proxy"],"message":"Executing fall-back request"} {"timestamp":"2024-07-05T02:08:13.156571","context":["proxy"],"message":"kore depth-bound, continuing... (currently at Depth {getNat = 1})"} {"timestamp":"2024-07-05T02:08:13.156571","context":["proxy"],"message":"Iterating execute request at Depth {getNat = 1}"} {"timestamp":"2024-07-05T02:09:34.92357","context":["proxy"],"message":"Server shutting down"} {"timestamp":"2024-07-05T02:09:34.92357","context":["proxy","timing"],"message":[["SimplifyM",{"average":7.6988472523e7,"count":1,"kore-average":7.205059572e7,"kore-max":7.205059572e7,"kore-total":7.205059572e7,"max-val":7.6988472523e7,"min-val":7.6988472523e7,"stddev":0,"total":7.6988472523e7}]]} ``` ### `find-recursions` Searches contexts for repeated rules/equations, outputs the maximum recursion count found, and a count of recursions for the rule/equation. ``` $ .build/kore/bin/process-logs find-recursions -i 120+426-simplify-server-new.log | Context | Longest | Count | Prefix |----------------------- | ------- | ----- |----------- | simplification 7d63500 | 2 | 26 | [request 1][kore][simplify][term d20f3f8][simplification b7ec79f][constraint][term 49a7309][term 68c0d1e] | simplification a0d171b | 2 | 4 | [request 1][booster][simplify][term 47a0b9a][term 5a2ca39][simplification b7ec79f][constraint][term c609cc3][simplification 7d63500][constraint][term d547132] | simplification b473543 | 2 | 2 | [request 1][kore][simplify][term d20f3f8][simplification 9fb2d01][constraint][term 3dabef4][term 1a59fb7][simplification e9253cd][constraint][term b2ad8ae][term b28272e][term a61320e][term 4235d4e][term f508bee][term f4925ee][term f4099ee][term f870b2e][term f8ea60e][term f76100e][term f76c34e][term e130fee][term e10212e][term e13614e][term e1329ee][term 66ebb55][function 4e91c9a][constraint][term f829f67][term af7fb3c][term ac31e7f][simplification e30a82a][constraint][term 4a8e686] | simplification d36bc83 | 2 | 32 | [request 1][kore][simplify][term d20f3f8][simplification b7ec79f][constraint][term 2d166e3][function 806f1ac][constraint][term 91d5b62][term 7526e8d][term c648a18] | simplification d87d499 | 2 | 4 | [request 1][kore][simplify][term d20f3f8][simplification 9fb2d01][constraint][term 3dabef4][term 1a59fb7][simplification e9253cd][constraint][term a33da02] | simplification e9253cd | 2 | 36 | [request 1][kore][simplify][term d20f3f8][simplification 9fb2d01][constraint][term 3dabef4][term 1a59fb7] ``` ### `times-per-rule` Counts and sums up time (if timestamps present) spent using a certain rule/equation at the top level (rewrite or simplify), outputs a sorted list of rules by descending time. NB no split between `kore` and `booster`, the log would have to be filtered beforehand to get that. ``` $ .build/kore/bin/process-logs times-per-rule -i log-with-timestamps.json | Rule/Equation | Success | Failure | Abort |----------------------- | ------------------- | ------------------- | ------------------- | rewrite 589c3c2 | 2.709139s ( 1) | 0.000000s ( 7) | 0.000000s ( 1) | rewrite 8560c71 | 1.461561s ( 1) | 0.000000s ( 8) | 0.000000s ( 0) | rewrite 69d07db | 1.371660s ( 1) | 0.000000s ( 7) | 0.000000s ( 0) | rewrite b8c34b7 | 1.317183s ( 1) | 0.000000s ( 9) | 0.000000s ( 0) | rewrite b3ed6e6 | 1.314000s ( 1) | 0.000000s ( 9) | 0.000000s ( 0) | rewrite 49dfc9d | 1.304301s ( 1) | 0.000000s ( 9) | 0.000000s ( 0) | rewrite 84d9ca4 | 0.229139s ( 1) | 0.000000s ( 10) | 0.000000s ( 0) | function UNKNOWN | 0.172207s ( 2) | 0.042539s ( 5582) | 0.000000s ( 0) | simplification 0e3f267 | 0.000000s ( 0) | 0.087230s ( 6) | 0.000000s ( 0) | simplification cc7577b | 0.000000s ( 0) | 0.056554s ( 6) | 0.000000s ( 0) | simplification 3cbbedc | 0.000000s ( 0) | 0.036781s ( 6) | 0.000000s ( 0) | function c078f16 | 0.000000s ( 0) | 0.036355s ( 2) | 0.000000s ( 0) | simplification 99e34a2 | 0.000000s ( 0) | 0.033110s ( 95) | 0.000000s ( 0) | rewrite e952dcd | 0.026578s ( 1) | 0.000000s ( 10) | 0.000000s ( 0) | function 8b92687 | 0.000000s ( 0) | 0.013105s ( 1) | 0.000000s ( 0) | simplification a916a71 | 0.000000s ( 0) | 0.008408s ( 65) | 0.000000s ( 0) | simplification bab86d4 | 0.000000s ( 0) | 0.007228s ( 65) | 0.000000s ( 0) | simplification 756dd4f | 0.000000s ( 0) | 0.006819s ( 190) | 0.000000s ( 0) | rewrite 952a852 | 0.000000s ( 0) | 0.006759s ( 9) | 0.000000s ( 0) ... many more lines of output ``` --- dev-tools/package.yaml | 18 + dev-tools/process-logs/Main.hs | 317 ++++++++++++++++++ .../src/Kore/JsonRpc/Types/ContextLog.hs | 5 +- kore/src/Kore/Log/DebugAppliedRewriteRules.hs | 7 +- 4 files changed, 340 insertions(+), 7 deletions(-) create mode 100644 dev-tools/process-logs/Main.hs diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index 2957bc79fc..1b72058abd 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -103,6 +103,24 @@ executables: - text ghc-options: - -rtsopts + process-logs: + source-dirs: process-logs + main: Main.hs + dependencies: + - aeson + - aeson-pretty + - base + - bytestring + - containers + - directory + - filepath + - hs-backend-booster + - kore-rpc-types + - optparse-applicative + - text + - time + ghc-options: + - -rtsopts time-profile: source-dirs: time-profile main: Main.hs diff --git a/dev-tools/process-logs/Main.hs b/dev-tools/process-logs/Main.hs new file mode 100644 index 0000000000..03c89b5c50 --- /dev/null +++ b/dev-tools/process-logs/Main.hs @@ -0,0 +1,317 @@ +{- | Log processing utility + +Copyright : (c) Runtime Verification, 2024 +License : BSD-3-Clause +-} +module Main ( + main, +) where + +import Control.Monad (unless) +import Data.Aeson qualified as JSON +import Data.Aeson.Encode.Pretty qualified as JSON +import Data.ByteString.Char8 qualified as BSS +import Data.ByteString.Lazy.Char8 qualified as BS +import Data.Either (partitionEithers) +import Data.Foldable (toList) +import Data.List (foldl', maximumBy, sortBy) +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Maybe (mapMaybe) +import Data.Ord (Down (..), comparing) +import Data.Sequence (Seq (..)) +import Data.Sequence qualified as Seq +import Data.Time.Clock +import Data.Time.Clock.System (systemToUTCTime) +import Options.Applicative +import System.Exit +import Text.Printf + +import Booster.Log.Context (ContextFilter, mustMatch, readContextFilter) +import Kore.JsonRpc.Types (rpcJsonConfig) +import Kore.JsonRpc.Types.ContextLog + +-- reads log file in json-format from stdin (or a single given file) +-- applies the command +-- outputs resulting log file or resulting data to stdout or a given file +main :: IO () +main = do + Options{cmd, input, output} <- execParser parse + (errors, inputJson) <- + partitionEithers + . map JSON.eitherDecode + . BS.lines + <$> maybe BS.getContents BS.readFile input + unless (null errors) $ do + putStrLn "JSON parse errors in log file:" + mapM_ putStrLn errors + exitWith (ExitFailure 1) + let writeOut = maybe BS.putStrLn BS.writeFile output . BS.unlines + writeOut $ process cmd inputJson + +data Options = Options + { cmd :: Command + , input :: Maybe FilePath + , output :: Maybe FilePath + } + deriving (Show) + +data Command + = -- | filter a log file, output to stdout. Same options as for the server + Filter [ContextFilter] + | -- | find repeated rule/equation contexts in lines + FindRecursions + | -- | compute total times spent on applying certain rules/equations (top-level) + TimesPerRule + deriving (Show) + +parse :: ParserInfo Options +parse = + info + (parseOpts <**> helper) + (fullDesc <> progDesc "log-processing utility for json context logs") + where + parseOpts = + Options + <$> commandParser + <*> optional + ( strOption + ( long "input-file" + <> short 'i' + <> metavar "INPUTFILE" + <> help "take input from a file instead of stdin" + ) + ) + <*> optional + ( strOption + ( long "output-file" + <> short 'o' + <> metavar "OUTPUTFILE" + <> help "write output to a file instead of stdout" + ) + ) + commandParser = + subparser $ + ( command + "filter" + ( info + ((Filter <$> many parseContextFilter) <**> helper) + (progDesc "filter log file with given contexts (space separated)") + ) + ) + <> ( command + "find-recursions" + ( info + (pure FindRecursions <**> helper) + (progDesc "find repeated contexts in log lines") + ) + ) + <> ( command + "times-per-rule" + ( info + (pure TimesPerRule <**> helper) + (progDesc "compute total times spent per (top-level) rule/equation") + ) + ) + + parseContextFilter = + argument + (eitherReader readContextFilter) + ( metavar "CONTEXT" + <> help "Log context" + ) + +------------------------------------------------------------ + +process :: Command -> [LogLine] -> [BS.ByteString] +process (Filter filters) = + map encodeLogLine . filterLines filters +process FindRecursions = + (heading <>) . map renderResult . findRecursions + where + heading = + [ "| Context | Longest | Count | Prefix" + , "|----------------------- | ------- | ----- |-----------" + ] + renderResult (ctx, (pfx, len, cnt)) = + BS.pack $ printf "| %22s | %7d | %5d | %s" (show ctx) len cnt (showCtx pfx) + + showCtx = concatMap (show . (: [])) +process TimesPerRule = + (heading <>) . map renderResult . ruleStatistics + where + heading = + [ "| Rule/Equation | Success | Failure | Abort" + , "|----------------------- | ------------------- | ------------------- | -------------------" + ] + renderResult :: (IdContext, RuleStats) -> BS.ByteString + renderResult (ctx, stats) = + BS.pack $ + printf + "| %22s | %10.6fs (%5d) | %10.6fs (%5d) | %10.6fs (%5d)" + (show ctx) + stats.tSuccess + stats.nSuccess + stats.tFailure + stats.nFailure + stats.tAbort + stats.nAbort + +encodeLogLine :: LogLine -> BS.ByteString +encodeLogLine = JSON.encodePretty' rpcJsonConfig{JSON.confIndent = JSON.Spaces 0} + +------------------------------------------------------------ +filterLines :: [ContextFilter] -> [LogLine] -> [LogLine] +filterLines filters = filter keepLine + where + keepLine LogLine{context} = + let cs = map (BSS.pack . show) $ toList context + in matchesAFilter cs + matchesAFilter :: [BSS.ByteString] -> Bool + matchesAFilter x = any (flip mustMatch x) filters + +------------------------------------------------------------ +lineRecursion :: LogLine -> Maybe (CLContext, ([CLContext], Int)) +lineRecursion LogLine{context} + | null repeatedContexts = Nothing + | otherwise = Just (maxRepeatC, (prefix, count + 1)) + where + repeatedContexts = rr context + rr Seq.Empty = [] + rr (c :<| cs) + | CLWithId (c') <- c -- only contexts with ID (rules, equations, hooks) + , isRuleCtx c' + , repeats > 0 = + (c, repeats) : rr cs + | otherwise = rr cs + where + repeats = length $ Seq.filter (== c) cs + + (maxRepeatC, count) = maximumBy (comparing snd) repeatedContexts + + prefix = takeWhile (/= maxRepeatC) $ toList context + +isRuleCtx :: IdContext -> Bool +isRuleCtx CtxFunction{} = True +isRuleCtx CtxSimplification{} = True +isRuleCtx CtxRewrite{} = True +isRuleCtx _ = False + +findRecursions :: [LogLine] -> [(CLContext, ([CLContext], Int, Int))] +findRecursions ls = Map.assocs resultMap + where + recursions = + [(ctx, (pfx, cnt, 1)) | (ctx, (pfx, cnt)) <- mapMaybe lineRecursion ls] + maxAndCount :: + ([CLContext], Int, Int) -> + ([CLContext], Int, Int) -> + ([CLContext], Int, Int) + maxAndCount (pfx1, len1, cnt1) (pfx2, len2, cnt2) + | len1 >= len2 = + (pfx1, len1, cnt1 + cnt2) + | otherwise = + (pfx2, len2, cnt1 + cnt2) + resultMap = + foldl' (\m (ctx, item) -> Map.insertWith maxAndCount ctx item m) mempty recursions + +------------------------------------------------------------ +-- rule statistics + +ruleStatistics :: [LogLine] -> [(IdContext, RuleStats)] +ruleStatistics = + sortBy (comparing (Down . allTimes . snd)) + . Map.assocs + . ruleStats + where + allTimes :: RuleStats -> Double + allTimes stats = stats.tSuccess + stats.tFailure + stats.tAbort + +data RuleStats = RuleStats + { -- counts of: + nSuccess :: !Int -- successful application + , nFailure :: !Int -- failure to apply + , nAbort :: !Int -- failure, leading to abort + , -- total times for these categories + tSuccess :: !Double + , tFailure :: !Double + , tAbort :: !Double + } + deriving stock (Eq, Ord, Show) + +instance Monoid RuleStats where + mempty = RuleStats 0 0 0 0 0 0 + +instance Semigroup RuleStats where + rStats1 <> rStats2 = + RuleStats + { nSuccess = rStats1.nSuccess + rStats2.nSuccess + , nFailure = rStats1.nFailure + rStats2.nFailure + , nAbort = rStats1.nAbort + rStats2.nAbort + , tSuccess = rStats1.tSuccess + rStats2.tSuccess + , tFailure = rStats1.tFailure + rStats2.tFailure + , tAbort = rStats1.tAbort + rStats2.tAbort + } + +ruleStats :: [LogLine] -> Map IdContext RuleStats +ruleStats = Map.fromListWith (<>) . collect + where + collect [] = [] + collect (l@LogLine{context} : ls) + | Seq.null rulePart -- no rule involved? + = + collect ls + | otherwise = + let (outcome, rest) = fromCtxSpan (prefix :|> ruleCtx) (l : ls) + in (ruleId, outcome) : collect rest + where + (prefix, rulePart) = Seq.breakl interesting context + (ruleCtx, ruleId) = case rulePart of + hd :<| _rest + | c@(CLWithId c') <- hd -> (c, c') + | CLNullary{} <- hd -> error "no rule head found" + Seq.Empty -> error "no rule head found" + + -- only contexts with ID (rules, equations, hooks) + interesting CLNullary{} = False + interesting (CLWithId c') = isRuleCtx c' + + fromCtxSpan :: Seq CLContext -> [LogLine] -> (RuleStats, [LogLine]) + fromCtxSpan prefix ls + | null prefixLines = + error "Should have at least one line with the prefix" -- see above + | otherwise = + (mkOutcome (head prefixLines) (last prefixLines), rest) + where + len = Seq.length prefix + + hasPrefix :: LogLine -> Bool + hasPrefix = (== prefix) . Seq.take len . (.context) + + (prefixLines, rest) = span hasPrefix ls + + mkOutcome :: LogLine -> LogLine -> RuleStats + mkOutcome startLine endLine = + let time = + maybe + 1 + realToFrac + ( diffUTCTime + <$> fmap systemToUTCTime endLine.timestamp + <*> fmap systemToUTCTime startLine.timestamp + ) + in case Seq.drop len endLine.context of + CLNullary CtxSuccess :<| _ -> + RuleStats 1 0 0 time 0 0 + -- rewrite failures + _ :|> CLNullary CtxFailure -> + RuleStats 0 1 0 0 time 0 + _ :|> CLNullary CtxIndeterminate -> + RuleStats 0 0 1 0 0 time + -- equation failures + _ :|> CLNullary CtxContinue -> + RuleStats 0 1 0 0 time 0 + _ :|> CLNullary CtxBreak -> + RuleStats 0 0 1 0 0 time + other -> + -- case not covered... + error $ "Unexpected last context " <> show other diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs index bd5ae93b74..7d382a5261 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs @@ -182,6 +182,7 @@ instance FromJSON CLMessage where parseJSON (JSON.String msg) = pure $ CLText msg parseJSON obj@JSON.Object{} = pure $ CLValue obj parseJSON arr@JSON.Array{} = pure $ CLValue arr + parseJSON JSON.Null = pure $ CLValue JSON.Null parseJSON other = JSON.typeMismatch "Object, array, or string" other @@ -234,6 +235,6 @@ instance ToJSON LogLine where where formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime --- same format as the one used in Booster.Util +-- similar to the one used in Booster.Util, but not setting a length for the sub-second digits timestampFormat :: String -timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q" +timestampFormat = "%Y-%m-%dT%H:%M:%S%Q" diff --git a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs index eba576062d..9f02c1bbe2 100644 --- a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs +++ b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs @@ -71,11 +71,8 @@ instance Entry DebugAppliedRewriteRules where "failed to apply " <> pretty (length appliedRewriteRules) <> " rewrite rules" | otherwise = "applied " <> pretty (length appliedRewriteRules) <> " rewrite rules" - oneLineJson DebugAppliedRewriteRules{appliedRewriteRules} - | null appliedRewriteRules = Json.Null - | otherwise = - Json.toJSON $ - "applied " <> show (length appliedRewriteRules) <> " rewrite rules" + oneLineJson DebugAppliedRewriteRules{appliedRewriteRules} = + Json.toJSON $ "applied " <> show (length appliedRewriteRules) <> " rewrite rules" oneLineContextDoc DebugAppliedRewriteRules{appliedRewriteRules} | null appliedRewriteRules = single CtxFailure