Skip to content

Commit 055c77b

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents a6f5646 + 47f2ac8 commit 055c77b

File tree

15 files changed

+604
-162
lines changed

15 files changed

+604
-162
lines changed

‎booster/library/Booster/CLOptions.hs

Lines changed: 28 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,8 @@ allowedLogLevels =
236236
( "EquationWarnings"
237237
, "Log warnings indicating soft-violations of conditions, i.e. exceeding the equation recursion/iteration limit "
238238
)
239+
, ("TimeProfile", "Logs for timing analysis")
240+
, ("Timing", "Formerly --print-stats")
239241
]
240242

241243
levelToContext :: Map Text [ContextFilter]
@@ -244,49 +246,64 @@ levelToContext =
244246
[
245247
( "Simplify"
246248
,
247-
[ [ctxt| booster|kore>function*|simplification*|hook*,success|failure|abort|detail |]
248-
, [ctxt| booster|kore>function*|simplification*,match,failure|abort |]
249+
[ [ctxt| request*,booster|kore>function*|simplification*|hook*,success|failure|abort|detail |]
250+
, [ctxt| request*,booster|kore>function*|simplification*,match,failure|abort |]
249251
]
250252
)
251253
,
252254
( "SimplifySuccess"
253255
,
254-
[ [ctxt| booster|kore>function*|simplification*|hook*,success|detail |]
256+
[ [ctxt| request*,booster|kore>function*|simplification*|hook*,success|detail |]
255257
]
256258
)
257259
,
258260
( "Rewrite"
259261
,
260-
[ [ctxt| booster|kore>rewrite*,success|failure|abort|detail |]
261-
, [ctxt| booster|kore>rewrite*,match|definedness|constraint,failure|abort |]
262+
[ [ctxt| request*,booster|kore>rewrite*,success|failure|abort|detail |]
263+
, [ctxt| request*,booster|kore>rewrite*,match|definedness|constraint,failure|abort |]
262264
]
263265
)
264266
,
265267
( "RewriteSuccess"
266268
,
267-
[ [ctxt| booster|kore>rewrite*,success|detail |]
269+
[ [ctxt| request*,booster|kore>rewrite*,success|detail |]
268270
]
269271
)
270272
,
271273
( "SMT"
272274
,
273-
[ [ctxt| booster|kore>smt |]
275+
[ [ctxt| request*,booster|kore>smt |]
274276
]
275277
)
276278
,
277279
( "Aborts"
278280
,
279-
[ [ctxt| booster>rewrite*,detail. |]
280-
, [ctxt| booster>rewrite*,match|definedness|constraint,abort. |]
281+
[ [ctxt| request*,booster>rewrite*,detail. |]
282+
, [ctxt| request*,booster>rewrite*,match|definedness|constraint,abort. |]
281283
, [ctxt| proxy. |]
282284
, [ctxt| proxy,abort. |]
283-
, [ctxt| booster>failure,abort |]
285+
, [ctxt| request*,booster>failure,abort |]
284286
]
285287
)
286288
,
287289
( "EquationWarnings"
288290
,
289-
[ [ctxt| booster>(simplification *|function *)>warning |]
291+
[ [ctxt| request*,booster>(simplification *|function *)>warning |]
292+
]
293+
)
294+
,
295+
( "TimeProfile"
296+
,
297+
[ [ctxt| request*,booster|kore>rewrite*,success|failure|abort|detail |]
298+
, [ctxt| request*,booster|kore>rewrite*,match|definedness|condition,failure|abort |]
299+
, [ctxt| request*,booster|kore>function*|simplification*,success|failure|abort|detail |]
300+
, [ctxt| request*,booster|kore>function*|simplification*,match,failure|abort |]
301+
]
302+
)
303+
,
304+
( "Timing"
305+
,
306+
[ [ctxt| *>timing |]
290307
]
291308
)
292309
]

‎booster/library/Booster/Log.hs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ import Data.Maybe (fromMaybe)
4848
import Data.Set qualified as Set
4949
import Data.Text (Text, pack)
5050
import Data.Text.Encoding (decodeUtf8)
51+
import Network.JSONRPC qualified as JSONRPC
5152
import Prettyprinter (Pretty, pretty)
5253
import System.Log.FastLogger (FormattedTime)
5354
import UnliftIO (MonadUnliftIO)
@@ -222,6 +223,10 @@ instance ContextFor Symbol where
222223
withContextFor s =
223224
withContext_ (CLWithId . CtxHook $ maybe "not-hooked" decodeUtf8 s.attributes.hook)
224225

226+
instance ContextFor (JSONRPC.Id) where
227+
withContextFor r =
228+
withContext_ (CLWithId . CtxRequest $ pack $ JSONRPC.fromId r)
229+
225230
parseRuleId :: RewriteRule tag -> CL.UniqueId
226231
parseRuleId = fromMaybe CL.UNKNOWN . CL.parseUId . coerce . (.attributes.uniqueId)
227232

‎booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden

Lines changed: 72 additions & 72 deletions
Large diffs are not rendered by default.

‎booster/tools/booster/Server.hs

Lines changed: 14 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
{-# LANGUAGE FlexibleContexts #-}
2-
{-# LANGUAGE QuasiQuotes #-}
32
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
43

54
{- |
@@ -35,6 +34,7 @@ import Data.Set qualified as Set
3534
import Data.Text (Text)
3635
import Data.Text qualified as Text
3736
import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
37+
import Network.JSONRPC qualified as JSONRPC
3838
import Options.Applicative
3939
import System.Clock (
4040
Clock (..),
@@ -137,8 +137,7 @@ main = do
137137
}
138138
, proxyOptions =
139139
ProxyOptions
140-
{ printStats
141-
, forceFallback
140+
{ forceFallback
142141
, boosterSMT
143142
, fallbackReasons
144143
, simplifyAtEnd
@@ -149,7 +148,6 @@ main = do
149148
logContextsWithcustomLevelContexts =
150149
logContexts
151150
<> concatMap (\case LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels
152-
<> [[Ctxt.ctxt| *>timing |] | printStats]
153151
contextLoggingEnabled = not (null logContextsWithcustomLevelContexts)
154152
koreSolverOptions = translateSMTOpts smtOptions
155153
timestampFlag = case timeStampsFormat of
@@ -312,10 +310,11 @@ main = do
312310
Booster.Log.withContext CtxProxy $
313311
Booster.Log.logMessage' ("Starting RPC server" :: Text)
314312

315-
let koreRespond, boosterRespond :: Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res)
316-
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
317-
boosterRespond =
318-
Booster.Log.withContext CtxBooster
313+
let koreRespond, boosterRespond :: JSONRPC.Id -> Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res)
314+
koreRespond reqId = Kore.respond (fromId reqId) kore.serverState (ModuleName kore.mainModule) runSMT
315+
boosterRespond reqId =
316+
Booster.Log.withContextFor reqId
317+
. Booster.Log.withContext CtxBooster
319318
. Booster.respond boosterState
320319

321320
proxyConfig =
@@ -332,9 +331,10 @@ main = do
332331
jsonRpcServer
333332
srvSettings
334333
( \rawReq req ->
335-
runBoosterLogger $
336-
logRequestId (fromId $ getReqId rawReq)
337-
>> Proxy.respondEither proxyConfig boosterRespond koreRespond req
334+
let reqId = getReqId rawReq
335+
in runBoosterLogger $
336+
logRequestId reqId
337+
>> Proxy.respondEither proxyConfig (boosterRespond reqId) (koreRespond reqId) req
338338
)
339339
[ Kore.handleDecidePredicateUnknown
340340
, Booster.handleSmtError
@@ -362,7 +362,7 @@ main = do
362362
Booster.Log.withContext CtxProxy $
363363
Booster.Log.logMessage' $
364364
Text.pack $
365-
"Processing request " <> rid
365+
"Processing request " <> fromId rid
366366

367367
isInterrupt :: AsyncException -> Maybe ()
368368
isInterrupt UserInterrupt = Just ()
@@ -405,9 +405,7 @@ data CLProxyOptions = CLProxyOptions
405405
}
406406

407407
data ProxyOptions = ProxyOptions
408-
{ printStats :: Bool
409-
-- ^ print timing statistics per request and on shutdown
410-
, forceFallback :: Maybe Depth
408+
{ forceFallback :: Maybe Depth
411409
-- ^ force fallback every n-steps
412410
, boosterSMT :: Bool
413411
-- ^ whether to use an SMT solver in booster code (but keeping kore-rpc's SMT solver)
@@ -432,11 +430,7 @@ clProxyOptionsParser =
432430
where
433431
parseProxyOptions =
434432
ProxyOptions
435-
<$> switch
436-
( long "print-stats"
437-
<> help "(development) Print timing information per request and on shutdown"
438-
)
439-
<*> optional
433+
<$> optional
440434
( option
441435
(Depth <$> auto)
442436
( metavar "INTERIM_SIMPLIFICATION"

‎cabal.project

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,10 @@ source-repository-package
1515
type: git
1616
location: https://github.com/goodlyrottenapple/tasty-test-reporter.git
1717
tag: b704130545aa3925a8487bd3e92f1dd5ce0512e2
18+
19+
source-repository-package
20+
type: git
21+
location: https://github.com/goodlyrottenapple/profiteur.git
22+
tag: 7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465
23+
24+
constraints: profiteur +embed-data-files

‎dev-tools/kore-rpc-dev/Server.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -233,12 +233,12 @@ main = do
233233
Booster.Log.withContext CtxKore $
234234
Booster.Log.logMessage' ("Starting RPC server" :: Text.Text)
235235

236-
let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res)
237-
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
236+
let koreRespond :: Id -> Respond (API 'Req) (LoggerT IO) (API 'Res)
237+
koreRespond reqId = Kore.respond (fromId reqId) kore.serverState (ModuleName kore.mainModule) runSMT
238238
server =
239239
jsonRpcServer
240240
srvSettings
241-
(const $ runBoosterLogger . respond koreRespond)
241+
(\rawReq -> runBoosterLogger . respond (koreRespond $ getReqId rawReq))
242242
[Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
243243
interruptHandler _ = do
244244
when (logLevel >= LevelInfo) $

‎dev-tools/package.yaml

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,23 @@ executables:
103103
- text
104104
ghc-options:
105105
- -rtsopts
106+
time-profile:
107+
source-dirs: time-profile
108+
main: Main.hs
109+
dependencies:
110+
- aeson
111+
- base
112+
- bytestring
113+
- containers
114+
- directory
115+
- filepath
116+
- kore-rpc-types
117+
- profiteur
118+
- text
119+
- unordered-containers
120+
- vector
121+
ghc-options:
122+
- -rtsopts
106123
parsetest-binary:
107124
source-dirs: parsetest-binary
108125
main: ParsetestBinary.hs

‎dev-tools/time-profile/Main.hs

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
{- | Stand-alone parser executable for extracting timing information from JSON context logs
2+
3+
Copyright : (c) Runtime Verification, 2022
4+
License : BSD-3-Clause
5+
-}
6+
module Main (
7+
main,
8+
) where
9+
10+
import Data.Aeson (decode)
11+
import Data.ByteString.Lazy.Char8 qualified as BS
12+
import Data.Maybe (mapMaybe)
13+
import Profiteur
14+
import Profiteur.Main (writeReport)
15+
import System.Environment (getArgs)
16+
import System.IO qualified as IO
17+
18+
{- | Utility for parsing and extracting timing information from context logs,
19+
produced by running the booster binary with `-l TimeProfile --log-format json --log-timestamps --timestamp-format nanosecond`.
20+
This tool collects the timing per each context level and uses the profiteur library to generate an HTML report of the timing information
21+
Call via `timing <path>.log`
22+
-}
23+
main :: IO ()
24+
main =
25+
getArgs >>= \case
26+
files
27+
| "-h" `elem` files || "--help" `elem` files -> do
28+
putStrLn
29+
"This tool parses the JSON contextual logs with timestamps and generates a time profile."
30+
putStrLn "Call via `time-profile <path>.log`"
31+
putStrLn
32+
"To produce the correct context logs, run kore-rpc-booster with `-l TimeProfile --log-format json --log-timestamps --timestamp-format nanosecond`"
33+
[profFile] -> do
34+
logs <- mapMaybe decode . BS.lines <$> BS.readFile profFile
35+
36+
let (timings, ruleMap) = case logs of
37+
m : ms -> collectTiming mempty m ms
38+
[] -> mempty
39+
timing = foldr (((<>)) . fmap (,Count 1) . computeTimes) (TimeMap mempty) timings
40+
htmlFile = profFile ++ ".html"
41+
IO.withBinaryFile htmlFile IO.WriteMode $ \h -> do
42+
-- produce a timing map mirroring the context levels, roughly:
43+
-- main -> request n -> kore|booster -> execute|simplify|implies -> term rid -> rewrite id|simplification id|equation id -> success|failure
44+
writeReport h profFile $ toNodeMap timing ruleMap
45+
46+
let htmlAggregateFile = profFile ++ ".aggregate.html"
47+
IO.withBinaryFile htmlAggregateFile IO.WriteMode $ \h -> do
48+
writeReport h profFile $
49+
-- produce an agregate profile of all the number and total time spent trying each rewrite rule. The structure is:
50+
-- main -> request n -> rewrite id -> kore|booster
51+
toNodeMap (aggregateRewriteRules aggregateRewriteRulesPerRequest timing) ruleMap
52+
53+
let htmlAggregateFile2 = profFile ++ ".aggregate2.html"
54+
IO.withBinaryFile htmlAggregateFile2 IO.WriteMode $ \h -> do
55+
writeReport h profFile $
56+
-- produce an agregate profile of all the number and total time spent trying each rewrite rule. The structure is:
57+
-- main -> request n -> kore|booster -> rewrite id
58+
toNodeMap (aggregateRewriteRules aggregateRewriteRulesPerRequest2 timing) ruleMap
59+
_ -> error "invalid arguments"

0 commit comments

Comments
 (0)