Fixes to simplification diff, request statistics, process-logs (#3992)

* Add some context lines to simplification diff 
* compute request statistics in seconds (and output in seconds in the
json format)
* Make `process-logs` fail immediately on parse errors, and process
lines incrementally (less heap)

Author: jberthold

booster/library/Booster/JsonRpc/Utils.hs

@@ -224,12 +224,15 @@ methodOfRpcCall = \case
 renderDiff :: BS.ByteString -> BS.ByteString -> Maybe String
 renderDiff first second
     | first == second = Nothing
-renderDiff first second = unsafePerformIO . withTempDir $ \dir -> do
+    | otherwise = renderDiff' ["-w"] first second
+
+renderDiff' :: [String] -> BS.ByteString -> BS.ByteString -> Maybe String
+renderDiff' diffOptions first second = unsafePerformIO . withTempDir $ \dir -> do
     let path1 = dir </> "diff_file1.txt"
         path2 = dir </> "diff_file2.txt"
     BS.writeFile path1 first
     BS.writeFile path2 second
-    (result, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] ""
+    (result, str, _) <- readProcessWithExitCode "diff" (diffOptions <> [path1, path2]) ""
     case result of
         ExitSuccess -> pure Nothing
         ExitFailure 1 -> pure $ Just str
@@ -240,7 +243,7 @@ renderDiff first second = unsafePerformIO . withTempDir $ \dir -> do
 -- This uses the `pretty` instance for a textual diff.
 diffBy :: Internal.KoreDefinition -> KorePattern -> KorePattern -> Maybe String
 diffBy def pat1 pat2 =
-    renderDiff (internalise pat1) (internalise pat2)
+    renderDiff' ["-c", "-w"] (internalise pat1) (internalise pat2)
   where
     renderBS :: TermOrPredicates -> BS.ByteString
     renderBS (Predicates ps) =

booster/tools/booster/Proxy.hs

@@ -49,7 +49,7 @@ import Kore.Log qualified
 import Kore.Syntax.Definition (SentenceAxiom)
 import Kore.Syntax.Json.Types qualified as KoreJson
 import SMT qualified
-import Stats (MethodTiming (..), StatsVar, addStats, microsWithUnit, timed)
+import Stats (MethodTiming (..), StatsVar, addStats, secWithUnit, timed)
 
 data KoreServer = KoreServer
     { serverState :: MVar.MVar Kore.ServerState
@@ -396,7 +396,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                                 , koreTime = kTime
                                                 }
                                         )
-                                        ("Kore fall-back in " <> microsWithUnit kTime)
+                                        ("Kore fall-back in " <> secWithUnit kTime)
                             case kResult of
                                 Right (Execute koreResult) -> do
                                     let

booster/tools/booster/Stats.hs

@@ -3,7 +3,7 @@ module Stats (
     addStats,
     finaliseStats,
     timed,
-    microsWithUnit,
+    secWithUnit,
     RequestStats (..),
     StatsVar,
     MethodTiming (..),
@@ -25,7 +25,7 @@ import Booster.Log
 import Booster.Prettyprinter
 import Kore.JsonRpc.Types (APIMethod)
 
--- server statistics
+-- | Statistics for duration measurement time series (in seconds)
 data RequestStats a = RequestStats
     { count :: Int
     , average :: a
@@ -60,31 +60,30 @@ instance (Floating a, PrintfArg a, Ord a) => Pretty (RequestStats a) where
                 <+> withUnit stats.koreMax
             ]
       where
-        withUnit = pretty . microsWithUnit
+        withUnit = pretty . secWithUnit
 
-microsWithUnit :: (Floating a, Ord a, PrintfArg a) => a -> String
-microsWithUnit x
-    | x > 10 ** 5 = printf "%.2fs" $ x / 10 ** 6
-    | x > 10 ** 2 = printf "%.3fms" $ x / 10 ** 3
-    | otherwise = printf "%.1fμs" x
+secWithUnit :: (Floating a, Ord a, PrintfArg a) => a -> String
+secWithUnit x
+    | x > 0.1 = printf "%.2fs" x
+    | x > 0.0001 = printf "%.3fms" $ x * 10 ** 3
+    | otherwise = printf "%.1fμs" $ x * 10 ** 6
 
 -- internal helper type
--- all values are in microseconds
-data Stats' a = Stats'
+-- all values are in seconds
+data Stats' = Stats'
     { count :: Int
-    , total :: a
-    , squares :: a
-    , maxVal :: a
-    , minVal :: a
-    , koreTotal :: a
-    , koreMax :: a
+    , total :: Double
+    , squares :: Double
+    , maxVal :: Double
+    , minVal :: Double
+    , koreTotal :: Double
+    , koreMax :: Double
     }
 
-instance (Ord a, Num a) => Semigroup (Stats' a) where
+instance Semigroup Stats' where
     (<>) = addStats'
 
-{-# SPECIALIZE addStats' :: Stats' Double -> Stats' Double -> Stats' Double #-}
-addStats' :: (Ord a, Num a) => Stats' a -> Stats' a -> Stats' a
+addStats' :: Stats' -> Stats' -> Stats'
 addStats' stats1 stats2 =
     Stats'
         { count = stats1.count + stats2.count
@@ -96,7 +95,7 @@ addStats' stats1 stats2 =
         , koreMax = max stats1.koreMax stats2.koreMax
         }
 
-singleStats' :: Num a => a -> a -> Stats' a
+singleStats' :: Double -> Double -> Stats'
 singleStats' x korePart =
     Stats'
         { count = 1
@@ -108,43 +107,44 @@ singleStats' x korePart =
         , koreMax = korePart
         }
 
-type StatsVar = MVar (Map APIMethod (Stats' Double))
+type StatsVar = MVar (Map APIMethod Stats')
 
 -- helper type mainly for json logging
-data MethodTiming a = MethodTiming {method :: APIMethod, time :: a, koreTime :: a}
+data MethodTiming = MethodTiming {method :: APIMethod, time :: Double, koreTime :: Double}
     deriving stock (Eq, Show, Generic)
     deriving
         (ToJSON, FromJSON)
-        via CustomJSON '[FieldLabelModifier '[CamelToKebab]] (MethodTiming a)
+        via CustomJSON '[FieldLabelModifier '[CamelToKebab]] MethodTiming
 
-instance ToLogFormat (MethodTiming Double) where
+instance ToLogFormat MethodTiming where
     toTextualLog mt =
         pack $
             printf
                 "Performed %s in %s (%s kore time)"
                 (show mt.method)
-                (microsWithUnit mt.time)
-                (microsWithUnit mt.koreTime)
+                (secWithUnit mt.time)
+                (secWithUnit mt.koreTime)
     toJSONLog = toJSON
 
 addStats ::
     MonadIO m =>
-    MVar (Map APIMethod (Stats' Double)) ->
-    MethodTiming Double ->
+    MVar (Map APIMethod Stats') ->
+    MethodTiming ->
     m ()
 addStats statVar MethodTiming{method, time, koreTime} =
     liftIO . modifyMVar_ statVar $
         pure . Map.insertWith (<>) method (singleStats' time koreTime)
 
-newStats :: MonadIO m => m (MVar (Map APIMethod (Stats' Double)))
+newStats :: MonadIO m => m (MVar (Map APIMethod Stats'))
 newStats = liftIO $ newMVar Map.empty
 
+-- returns time taken by the given action (in seconds)
 timed :: MonadIO m => m a -> m (a, Double)
 timed action = do
     start <- liftIO $ getTime Monotonic
     result <- action
     stop <- liftIO $ getTime Monotonic
-    let time = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1000.0
+    let time = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 10 ** 9
     pure (result, time)
 
 newtype FinalStats = FinalStats (Map APIMethod (RequestStats Double))
@@ -164,10 +164,10 @@ instance ToLogFormat FinalStats where
     toTextualLog = renderText . pretty
     toJSONLog = toJSON
 
-finaliseStats :: MVar (Map APIMethod (Stats' Double)) -> IO FinalStats
+finaliseStats :: MVar (Map APIMethod Stats') -> IO FinalStats
 finaliseStats var = FinalStats . Map.map finalise <$> readMVar var
   where
-    finalise :: Floating a => Stats' a -> RequestStats a
+    finalise :: Stats' -> RequestStats Double
     finalise Stats'{count, total, squares, maxVal, minVal, koreTotal, koreMax} =
         let average = total / fromIntegral count
             stddev = sqrt $ squares / fromIntegral count - average * average

dev-tools/process-logs/Main.hs

@@ -7,12 +7,10 @@ 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)
@@ -24,7 +22,6 @@ 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)
@@ -37,17 +34,15 @@ import Kore.JsonRpc.Types.ContextLog
 main :: IO ()
 main = do
     Options{cmd, input, output} <- execParser parse
-    (errors, inputJson) <-
-        partitionEithers
-            . map JSON.eitherDecode
+    inputData <-
+        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
+    writeOut $ process cmd $ stopOnErrors inputData
+  where
+    stopOnErrors :: [Either String LogLine] -> [LogLine]
+    stopOnErrors = map (either (error . ("JSON parse error: " <>)) id)
 
 data Options = Options
     { cmd :: Command