|
| 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 |
0 commit comments