Add count-aborts binary (#3911)

Add `count-aborts` binary which can count aborts via `count-aborts
file_1 ... file_n`, producing a simple table.
The files expected as input to this tool are produced by the booster via
`--log-format json --log-file <file>`.

---------

Co-authored-by: github-actions <[email protected]>

Author: goodlyrottenapple

dev-tools/count-aborts/Main.hs

@@ -0,0 +1,41 @@
+{- | Stand-alone parser executable for testing and profiling
+
+Copyright   : (c) Runtime Verification, 2022
+License     : BSD-3-Clause
+-}
+module Main (
+    main,
+) where
+
+import Control.Monad (foldM, forM_)
+import Data.Aeson (decode)
+import Data.ByteString.Lazy.Char8 qualified as BS
+import Data.List (foldl', sortOn)
+import Data.Map qualified as Map
+import Data.Maybe (fromMaybe)
+import Data.Ord (Down (..))
+import Data.Text (unpack)
+import System.Environment (getArgs)
+import Types
+
+{- | Utility for parsing and extracting information from context logs,
+   produced by running the booster binary with `--log-format json --log-file <path>`.
+   This tool collects the number of aborts for each rewrite rule and displays the informantion in a table.
+   Call via `count-aborts <path_1> ... <path_n>`
+-}
+main :: IO ()
+main =
+    getArgs >>= \case
+        files
+            | "-h" `elem` files || "--help" `elem` files -> do
+                putStrLn
+                    "This tool parses the JSON contextual logs, collects the number of aborts for each rewrite rule and displays the informantion in a table."
+                putStrLn "Call via `count-aborts <path_1> ... <path_n>`"
+                putStrLn
+                    "To produce the correct context logs, run kore-rpc-booster with `--log-format json --log-file <file>`"
+            | otherwise -> do
+                let countContexts m f = foldl' (foldl' countAborts) m . map decode . BS.lines <$> BS.readFile f
+                (counts, rIdTorLoc) <- foldM countContexts mempty files
+                forM_ (sortOn (Down . snd) $ Map.toList counts) $ \(k, v) -> do
+                    let (rType, rLoc) = fromMaybe ("-", "-") $ Map.lookup k rIdTorLoc
+                    putStrLn $ unpack rType <> " " <> unpack k <> " | " <> unpack rLoc <> " | " <> show v

dev-tools/count-aborts/Types.hs

@@ -0,0 +1,39 @@
+module Types (module Types) where
+
+import Data.Aeson (FromJSON (..), Value (..))
+import Data.Aeson.Key (toString)
+import Data.Aeson.KeyMap (toList)
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Data.Sequence (Seq (..))
+import Data.Text (Text, pack)
+import GHC.Generics (Generic)
+
+data Context = Plain Text | Ref Text Text deriving (Eq, Ord)
+
+instance FromJSON Context where
+    parseJSON (String t) = pure $ Plain t
+    parseJSON (Object o) | [(k, String v)] <- toList o = pure $ Ref (pack $ toString k) v
+    parseJSON _ = fail "Invalid context"
+
+data LogMessage = LogMessage
+    { context :: Seq Context
+    , message :: Value
+    }
+    deriving (Generic, FromJSON)
+
+countAborts ::
+    (Map Text Int, Map Text (Text, Text)) -> LogMessage -> (Map Text Int, Map Text (Text, Text))
+countAborts maps@(countMap, ruleMap) LogMessage{context, message} = case context of
+    (_ :|> Ref "rewrite" ruleId :|> Plain "match" :|> Plain "abort") -> increment ruleId
+    (_ :|> Ref "rewrite" ruleId :|> Plain "abort") -> increment ruleId
+    (_ :|> Ref "function" ruleId :|> Plain "failure" :|> Plain "break") -> increment ruleId
+    (_ :|> Ref "simplification" ruleId :|> Plain "failure" :|> Plain "break") -> increment ruleId
+    (_ :|> Ref "function" ruleId :|> Plain "match" :|> Plain "failure" :|> Plain "break") -> increment ruleId
+    (_ :|> Ref "simplification" ruleId :|> Plain "match" :|> Plain "failure" :|> Plain "break") -> increment ruleId
+    (_ :|> Ref "rewrite" ruleId :|> Plain "detail") | String ruleLoc <- message -> (countMap, Map.insert ruleId ("rewrite", ruleLoc) ruleMap)
+    (_ :|> Ref "function" ruleId :|> Plain "detail") | String ruleLoc <- message -> (countMap, Map.insert ruleId ("function", ruleLoc) ruleMap)
+    (_ :|> Ref "simplification" ruleId :|> Plain "detail") | String ruleLoc <- message -> (countMap, Map.insert ruleId ("simplification", ruleLoc) ruleMap)
+    _ -> maps
+  where
+    increment rid = (Map.alter (maybe (Just 1) (Just . (+ 1))) rid countMap, ruleMap)

dev-tools/package.yaml

@@ -89,6 +89,19 @@ executables:
       - transformers
     ghc-options:
       - -rtsopts
+  count-aborts:
+    source-dirs: count-aborts
+    main: Main.hs
+    dependencies:
+      - aeson
+      - base
+      - bytestring
+      - containers
+      - directory
+      - filepath
+      - text
+    ghc-options:
+      - -rtsopts
   parsetest-binary:
     source-dirs: parsetest-binary
     main: ParsetestBinary.hs