Skip to content

Commit bb7b134

Browse files
jbertholdjberthold
authored
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 ```
1 parent e7409dc commit bb7b134

File tree

4 files changed

+340
-7
lines changed

4 files changed

+340
-7
lines changed

‎dev-tools/package.yaml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,24 @@ executables:
103103
- text
104104
ghc-options:
105105
- -rtsopts
106+
process-logs:
107+
source-dirs: process-logs
108+
main: Main.hs
109+
dependencies:
110+
- aeson
111+
- aeson-pretty
112+
- base
113+
- bytestring
114+
- containers
115+
- directory
116+
- filepath
117+
- hs-backend-booster
118+
- kore-rpc-types
119+
- optparse-applicative
120+
- text
121+
- time
122+
ghc-options:
123+
- -rtsopts
106124
time-profile:
107125
source-dirs: time-profile
108126
main: Main.hs

‎dev-tools/process-logs/Main.hs‎

Lines changed: 317 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,317 @@
1+
{- | Log processing utility
2+
3+
Copyright : (c) Runtime Verification, 2024
4+
License : BSD-3-Clause
5+
-}
6+
module Main (
7+
main,
8+
) where
9+
10+
import Control.Monad (unless)
11+
import Data.Aeson qualified as JSON
12+
import Data.Aeson.Encode.Pretty qualified as JSON
13+
import Data.ByteString.Char8 qualified as BSS
14+
import Data.ByteString.Lazy.Char8 qualified as BS
15+
import Data.Either (partitionEithers)
16+
import Data.Foldable (toList)
17+
import Data.List (foldl', maximumBy, sortBy)
18+
import Data.Map (Map)
19+
import Data.Map qualified as Map
20+
import Data.Maybe (mapMaybe)
21+
import Data.Ord (Down (..), comparing)
22+
import Data.Sequence (Seq (..))
23+
import Data.Sequence qualified as Seq
24+
import Data.Time.Clock
25+
import Data.Time.Clock.System (systemToUTCTime)
26+
import Options.Applicative
27+
import System.Exit
28+
import Text.Printf
29+
30+
import Booster.Log.Context (ContextFilter, mustMatch, readContextFilter)
31+
import Kore.JsonRpc.Types (rpcJsonConfig)
32+
import Kore.JsonRpc.Types.ContextLog
33+
34+
-- reads log file in json-format from stdin (or a single given file)
35+
-- applies the command
36+
-- outputs resulting log file or resulting data to stdout or a given file
37+
main :: IO ()
38+
main = do
39+
Options{cmd, input, output} <- execParser parse
40+
(errors, inputJson) <-
41+
partitionEithers
42+
. map JSON.eitherDecode
43+
. BS.lines
44+
<$> maybe BS.getContents BS.readFile input
45+
unless (null errors) $ do
46+
putStrLn "JSON parse errors in log file:"
47+
mapM_ putStrLn errors
48+
exitWith (ExitFailure 1)
49+
let writeOut = maybe BS.putStrLn BS.writeFile output . BS.unlines
50+
writeOut $ process cmd inputJson
51+
52+
data Options = Options
53+
{ cmd :: Command
54+
, input :: Maybe FilePath
55+
, output :: Maybe FilePath
56+
}
57+
deriving (Show)
58+
59+
data Command
60+
= -- | filter a log file, output to stdout. Same options as for the server
61+
Filter [ContextFilter]
62+
| -- | find repeated rule/equation contexts in lines
63+
FindRecursions
64+
| -- | compute total times spent on applying certain rules/equations (top-level)
65+
TimesPerRule
66+
deriving (Show)
67+
68+
parse :: ParserInfo Options
69+
parse =
70+
info
71+
(parseOpts <**> helper)
72+
(fullDesc <> progDesc "log-processing utility for json context logs")
73+
where
74+
parseOpts =
75+
Options
76+
<$> commandParser
77+
<*> optional
78+
( strOption
79+
( long "input-file"
80+
<> short 'i'
81+
<> metavar "INPUTFILE"
82+
<> help "take input from a file instead of stdin"
83+
)
84+
)
85+
<*> optional
86+
( strOption
87+
( long "output-file"
88+
<> short 'o'
89+
<> metavar "OUTPUTFILE"
90+
<> help "write output to a file instead of stdout"
91+
)
92+
)
93+
commandParser =
94+
subparser $
95+
( command
96+
"filter"
97+
( info
98+
((Filter <$> many parseContextFilter) <**> helper)
99+
(progDesc "filter log file with given contexts (space separated)")
100+
)
101+
)
102+
<> ( command
103+
"find-recursions"
104+
( info
105+
(pure FindRecursions <**> helper)
106+
(progDesc "find repeated contexts in log lines")
107+
)
108+
)
109+
<> ( command
110+
"times-per-rule"
111+
( info
112+
(pure TimesPerRule <**> helper)
113+
(progDesc "compute total times spent per (top-level) rule/equation")
114+
)
115+
)
116+
117+
parseContextFilter =
118+
argument
119+
(eitherReader readContextFilter)
120+
( metavar "CONTEXT"
121+
<> help "Log context"
122+
)
123+
124+
------------------------------------------------------------
125+
126+
process :: Command -> [LogLine] -> [BS.ByteString]
127+
process (Filter filters) =
128+
map encodeLogLine . filterLines filters
129+
process FindRecursions =
130+
(heading <>) . map renderResult . findRecursions
131+
where
132+
heading =
133+
[ "| Context | Longest | Count | Prefix"
134+
, "|----------------------- | ------- | ----- |-----------"
135+
]
136+
renderResult (ctx, (pfx, len, cnt)) =
137+
BS.pack $ printf "| %22s | %7d | %5d | %s" (show ctx) len cnt (showCtx pfx)
138+
139+
showCtx = concatMap (show . (: []))
140+
process TimesPerRule =
141+
(heading <>) . map renderResult . ruleStatistics
142+
where
143+
heading =
144+
[ "| Rule/Equation | Success | Failure | Abort"
145+
, "|----------------------- | ------------------- | ------------------- | -------------------"
146+
]
147+
renderResult :: (IdContext, RuleStats) -> BS.ByteString
148+
renderResult (ctx, stats) =
149+
BS.pack $
150+
printf
151+
"| %22s | %10.6fs (%5d) | %10.6fs (%5d) | %10.6fs (%5d)"
152+
(show ctx)
153+
stats.tSuccess
154+
stats.nSuccess
155+
stats.tFailure
156+
stats.nFailure
157+
stats.tAbort
158+
stats.nAbort
159+
160+
encodeLogLine :: LogLine -> BS.ByteString
161+
encodeLogLine = JSON.encodePretty' rpcJsonConfig{JSON.confIndent = JSON.Spaces 0}
162+
163+
------------------------------------------------------------
164+
filterLines :: [ContextFilter] -> [LogLine] -> [LogLine]
165+
filterLines filters = filter keepLine
166+
where
167+
keepLine LogLine{context} =
168+
let cs = map (BSS.pack . show) $ toList context
169+
in matchesAFilter cs
170+
matchesAFilter :: [BSS.ByteString] -> Bool
171+
matchesAFilter x = any (flip mustMatch x) filters
172+
173+
------------------------------------------------------------
174+
lineRecursion :: LogLine -> Maybe (CLContext, ([CLContext], Int))
175+
lineRecursion LogLine{context}
176+
| null repeatedContexts = Nothing
177+
| otherwise = Just (maxRepeatC, (prefix, count + 1))
178+
where
179+
repeatedContexts = rr context
180+
rr Seq.Empty = []
181+
rr (c :<| cs)
182+
| CLWithId (c') <- c -- only contexts with ID (rules, equations, hooks)
183+
, isRuleCtx c'
184+
, repeats > 0 =
185+
(c, repeats) : rr cs
186+
| otherwise = rr cs
187+
where
188+
repeats = length $ Seq.filter (== c) cs
189+
190+
(maxRepeatC, count) = maximumBy (comparing snd) repeatedContexts
191+
192+
prefix = takeWhile (/= maxRepeatC) $ toList context
193+
194+
isRuleCtx :: IdContext -> Bool
195+
isRuleCtx CtxFunction{} = True
196+
isRuleCtx CtxSimplification{} = True
197+
isRuleCtx CtxRewrite{} = True
198+
isRuleCtx _ = False
199+
200+
findRecursions :: [LogLine] -> [(CLContext, ([CLContext], Int, Int))]
201+
findRecursions ls = Map.assocs resultMap
202+
where
203+
recursions =
204+
[(ctx, (pfx, cnt, 1)) | (ctx, (pfx, cnt)) <- mapMaybe lineRecursion ls]
205+
maxAndCount ::
206+
([CLContext], Int, Int) ->
207+
([CLContext], Int, Int) ->
208+
([CLContext], Int, Int)
209+
maxAndCount (pfx1, len1, cnt1) (pfx2, len2, cnt2)
210+
| len1 >= len2 =
211+
(pfx1, len1, cnt1 + cnt2)
212+
| otherwise =
213+
(pfx2, len2, cnt1 + cnt2)
214+
resultMap =
215+
foldl' (\m (ctx, item) -> Map.insertWith maxAndCount ctx item m) mempty recursions
216+
217+
------------------------------------------------------------
218+
-- rule statistics
219+
220+
ruleStatistics :: [LogLine] -> [(IdContext, RuleStats)]
221+
ruleStatistics =
222+
sortBy (comparing (Down . allTimes . snd))
223+
. Map.assocs
224+
. ruleStats
225+
where
226+
allTimes :: RuleStats -> Double
227+
allTimes stats = stats.tSuccess + stats.tFailure + stats.tAbort
228+
229+
data RuleStats = RuleStats
230+
{ -- counts of:
231+
nSuccess :: !Int -- successful application
232+
, nFailure :: !Int -- failure to apply
233+
, nAbort :: !Int -- failure, leading to abort
234+
, -- total times for these categories
235+
tSuccess :: !Double
236+
, tFailure :: !Double
237+
, tAbort :: !Double
238+
}
239+
deriving stock (Eq, Ord, Show)
240+
241+
instance Monoid RuleStats where
242+
mempty = RuleStats 0 0 0 0 0 0
243+
244+
instance Semigroup RuleStats where
245+
rStats1 <> rStats2 =
246+
RuleStats
247+
{ nSuccess = rStats1.nSuccess + rStats2.nSuccess
248+
, nFailure = rStats1.nFailure + rStats2.nFailure
249+
, nAbort = rStats1.nAbort + rStats2.nAbort
250+
, tSuccess = rStats1.tSuccess + rStats2.tSuccess
251+
, tFailure = rStats1.tFailure + rStats2.tFailure
252+
, tAbort = rStats1.tAbort + rStats2.tAbort
253+
}
254+
255+
ruleStats :: [LogLine] -> Map IdContext RuleStats
256+
ruleStats = Map.fromListWith (<>) . collect
257+
where
258+
collect [] = []
259+
collect (l@LogLine{context} : ls)
260+
| Seq.null rulePart -- no rule involved?
261+
=
262+
collect ls
263+
| otherwise =
264+
let (outcome, rest) = fromCtxSpan (prefix :|> ruleCtx) (l : ls)
265+
in (ruleId, outcome) : collect rest
266+
where
267+
(prefix, rulePart) = Seq.breakl interesting context
268+
(ruleCtx, ruleId) = case rulePart of
269+
hd :<| _rest
270+
| c@(CLWithId c') <- hd -> (c, c')
271+
| CLNullary{} <- hd -> error "no rule head found"
272+
Seq.Empty -> error "no rule head found"
273+
274+
-- only contexts with ID (rules, equations, hooks)
275+
interesting CLNullary{} = False
276+
interesting (CLWithId c') = isRuleCtx c'
277+
278+
fromCtxSpan :: Seq CLContext -> [LogLine] -> (RuleStats, [LogLine])
279+
fromCtxSpan prefix ls
280+
| null prefixLines =
281+
error "Should have at least one line with the prefix" -- see above
282+
| otherwise =
283+
(mkOutcome (head prefixLines) (last prefixLines), rest)
284+
where
285+
len = Seq.length prefix
286+
287+
hasPrefix :: LogLine -> Bool
288+
hasPrefix = (== prefix) . Seq.take len . (.context)
289+
290+
(prefixLines, rest) = span hasPrefix ls
291+
292+
mkOutcome :: LogLine -> LogLine -> RuleStats
293+
mkOutcome startLine endLine =
294+
let time =
295+
maybe
296+
1
297+
realToFrac
298+
( diffUTCTime
299+
<$> fmap systemToUTCTime endLine.timestamp
300+
<*> fmap systemToUTCTime startLine.timestamp
301+
)
302+
in case Seq.drop len endLine.context of
303+
CLNullary CtxSuccess :<| _ ->
304+
RuleStats 1 0 0 time 0 0
305+
-- rewrite failures
306+
_ :|> CLNullary CtxFailure ->
307+
RuleStats 0 1 0 0 time 0
308+
_ :|> CLNullary CtxIndeterminate ->
309+
RuleStats 0 0 1 0 0 time
310+
-- equation failures
311+
_ :|> CLNullary CtxContinue ->
312+
RuleStats 0 1 0 0 time 0
313+
_ :|> CLNullary CtxBreak ->
314+
RuleStats 0 0 1 0 0 time
315+
other ->
316+
-- case not covered...
317+
error $ "Unexpected last context " <> show other

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,7 @@ instance FromJSON CLMessage where
182182
parseJSON (JSON.String msg) = pure $ CLText msg
183183
parseJSON obj@JSON.Object{} = pure $ CLValue obj
184184
parseJSON arr@JSON.Array{} = pure $ CLValue arr
185+
parseJSON JSON.Null = pure $ CLValue JSON.Null
185186
parseJSON other =
186187
JSON.typeMismatch "Object, array, or string" other
187188

@@ -234,6 +235,6 @@ instance ToJSON LogLine where
234235
where
235236
formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime
236237

237-
-- same format as the one used in Booster.Util
238+
-- similar to the one used in Booster.Util, but not setting a length for the sub-second digits
238239
timestampFormat :: String
239-
timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q"
240+
timestampFormat = "%Y-%m-%dT%H:%M:%S%Q"

‎kore/src/Kore/Log/DebugAppliedRewriteRules.hs‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -71,11 +71,8 @@ instance Entry DebugAppliedRewriteRules where
7171
"failed to apply " <> pretty (length appliedRewriteRules) <> " rewrite rules"
7272
| otherwise =
7373
"applied " <> pretty (length appliedRewriteRules) <> " rewrite rules"
74-
oneLineJson DebugAppliedRewriteRules{appliedRewriteRules}
75-
| null appliedRewriteRules = Json.Null
76-
| otherwise =
77-
Json.toJSON $
78-
"applied " <> show (length appliedRewriteRules) <> " rewrite rules"
74+
oneLineJson DebugAppliedRewriteRules{appliedRewriteRules} =
75+
Json.toJSON $ "applied " <> show (length appliedRewriteRules) <> " rewrite rules"
7976
oneLineContextDoc DebugAppliedRewriteRules{appliedRewriteRules}
8077
| null appliedRewriteRules =
8178
single CtxFailure

0 commit comments

Comments
 (0)