From def31908c3e5ff6c041d5f537e18ff0dbe975056 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 6 Aug 2024 14:29:59 +0200 Subject: [PATCH] Remove `"log-timing"` and `"log-fallbacks"` RPC log options (#4015) This options are unused and all ther use cases are subsumed by the `-l Timing` and `-l Aborts` non-RPC log option. --- booster/library/Booster/JsonRpc.hs | 37 +- ...ks-and-failed-and-successful-rewrites.json | 9 - ...nal-log-fallbacks-and-failed-rewrites.json | 8 - ...al-constraints-terminal-log-fallbacks.json | 7 - ...ks-and-failed-and-successful-rewrites.json | 408 ------------------ ...nal-log-fallbacks-and-failed-rewrites.json | 299 ------------- ...al-constraints-terminal-log-fallbacks.json | 290 ------------- .../test-logTiming/response-c.json | 105 ----- .../test-logTiming/state-c.execute | 1 - .../rpc-integration/test-logTiming/test.sh | 32 -- booster/tools/booster/Proxy.hs | 126 +----- docs/2022-07-18-JSON-RPC-Server-API.md | 31 +- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 4 - kore/src/Kore/JsonRpc.hs | 85 ++-- scripts/performance-tests-kevm.sh | 1 + test/rpc-server/logTiming/definition.kore | 1 - test/rpc-server/logTiming/params.json | 3 - test/rpc-server/logTiming/response.golden | 1 - test/rpc-server/logTiming/state.json | 85 ---- test/rpc-server/runTests.py | 77 ---- 20 files changed, 51 insertions(+), 1559 deletions(-) delete mode 100644 booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json delete mode 100644 booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json delete mode 100644 booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json delete mode 100644 booster/test/rpc-integration/test-logTiming/response-c.json delete mode 120000 booster/test/rpc-integration/test-logTiming/state-c.execute delete mode 100755 booster/test/rpc-integration/test-logTiming/test.sh delete mode 120000 test/rpc-server/logTiming/definition.kore delete mode 100644 test/rpc-server/logTiming/params.json delete mode 100644 test/rpc-server/logTiming/response.golden delete mode 100644 test/rpc-server/logTiming/state.json diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 11a0399f2c..85172ffbcc 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -39,7 +39,6 @@ import Data.Text.Encoding qualified as Text import GHC.Records import Numeric.Natural import Prettyprinter (comma, hsep, punctuate, (<+>)) -import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs) import Booster.CLOptions (RewriteOptions (..)) import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId) @@ -111,7 +110,6 @@ respond stateVar request = | isJust req.movingAverageStepTimeout -> pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String) RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, rewriteOpts) -> Booster.Log.withContext CtxExecute $ do - start <- liftIO $ getTime Monotonic -- internalise given constrained term let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term @@ -137,7 +135,6 @@ respond stateVar request = (fromMaybe False) [ req.logSuccessfulRewrites , req.logFailedRewrites - , req.logFallbacks ] -- apply the given substitution before doing anything else let substPat = @@ -174,14 +171,7 @@ respond stateVar request = result <- performRewrite rewriteConfig substPat SMT.finaliseSolver solver - stop <- liftIO $ getTime Monotonic - let duration = - if fromMaybe False req.logTiming - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ execResponse duration req result substitution unsupported + pure $ execResponse req result substitution unsupported RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar @@ -244,14 +234,8 @@ respond stateVar request = "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions) pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxSimplify $ do - start <- liftIO $ getTime Monotonic let internalised = runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term - let mkTraces duration - | Just True <- req.logTiming = - Just [ProcessingTime (Just Booster) duration] - | otherwise = - Nothing solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions @@ -325,13 +309,10 @@ respond stateVar request = (Left something, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something SMT.finaliseSolver solver - stop <- liftIO $ getTime Monotonic - let duration = - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - mkSimplifyResponse state = + let mkSimplifyResponse state = RpcTypes.Simplify - RpcTypes.SimplifyResult{state, logs = mkTraces duration} + RpcTypes.SimplifyResult{state, logs = Nothing} pure $ second mkSimplifyResponse result RpcTypes.GetModel req -> withModule req._module $ \case (_, _, Nothing, _) -> do @@ -615,13 +596,12 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} = } execResponse :: - Maybe Double -> RpcTypes.ExecuteRequest -> (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) -> Map Variable Term -> [Syntax.KorePattern] -> Either ErrorObj (RpcTypes.API 'RpcTypes.Res) -execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = case rr of +execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of RewriteBranch p nexts -> Right $ RpcTypes.Execute @@ -727,12 +707,9 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c (logSuccessfulRewrites, logFailedRewrites) ) traces - timingLog = - fmap (ProcessingTime $ Just Booster) mbDuration - in case (timingLog, traceLogs) of - (Nothing, []) -> Nothing - (Nothing, xs@(_ : _)) -> Just xs - (Just t, xs) -> Just (t : xs) + in case traceLogs of + [] -> Nothing + xs@(_ : _) -> Just xs toExecState :: Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState diff --git a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json b/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json deleted file mode 100644 index 1c289c24b2..0000000000 --- a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json +++ /dev/null @@ -1,9 +0,0 @@ -{ - "log-fallbacks": true, - "log-failed-rewrites": true, - "log-successful-rewrites": true, - "terminal-rules": [ - "TEST.EG", - "TEST.FG" - ] -} diff --git a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json b/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json deleted file mode 100644 index 878b131fb9..0000000000 --- a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "log-fallbacks": true, - "log-failed-rewrites": true, - "terminal-rules": [ - "TEST.EG", - "TEST.FG" - ] -} diff --git a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json b/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json deleted file mode 100644 index ab7d6d7b62..0000000000 --- a/booster/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json +++ /dev/null @@ -1,7 +0,0 @@ -{ - "log-fallbacks": true, - "terminal-rules": [ - "TEST.EG", - "TEST.FG" - ] -} diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json deleted file mode 100644 index 636fbf109d..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json +++ /dev/null @@ -1,408 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "Uncertain about a condition in rule", - "rule-id": "e7fa1c1f1a257fd5aff0f449a4ca861b20fd7eec75f8707158d197716b5a019e" - } - }, - { - "tag": "rewrite", - "origin": "kore-rpc", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "fallback", - "reason": "Uncertain about a condition in rule", - "fallback-rule-id": "e7fa1c1f1a257fd5aff0f449a4ca861b20fd7eec75f8707158d197716b5a019e", - "origin": "proxy", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "jnit" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "recovery-depth": 1, - "recovery-rule-ids": [ - "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - ], - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json deleted file mode 100644 index a49aeafc0f..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json +++ /dev/null @@ -1,299 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "Uncertain about a condition in rule", - "rule-id": "e7fa1c1f1a257fd5aff0f449a4ca861b20fd7eec75f8707158d197716b5a019e" - } - }, - { - "tag": "fallback", - "reason": "Uncertain about a condition in rule", - "fallback-rule-id": "e7fa1c1f1a257fd5aff0f449a4ca861b20fd7eec75f8707158d197716b5a019e", - "origin": "proxy", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "jnit" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "recovery-depth": 1, - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json deleted file mode 100644 index 0d186dc284..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json +++ /dev/null @@ -1,290 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "fallback", - "reason": "UNKNOWN: log-failed-rewrites not enabled", - "fallback-rule-id": "UNKNOWN: log-failed-rewrites not enabled", - "origin": "proxy", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "jnit" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "recovery-depth": 1, - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-logTiming/response-c.json b/booster/test/rpc-integration/test-logTiming/response-c.json deleted file mode 100644 index 4762a753b4..0000000000 --- a/booster/test/rpc-integration/test-logTiming/response-c.json +++ /dev/null @@ -1,105 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 3, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "processing-time" - }, - { - "tag": "processing-time", - "component": "booster" - }, - { - "tag": "processing-time", - "component": "kore-rpc" - }, - { - "tag": "processing-time", - "component": "booster" - }, - { - "tag": "processing-time", - "component": "kore-rpc" - } - ] - } -} diff --git a/booster/test/rpc-integration/test-logTiming/state-c.execute b/booster/test/rpc-integration/test-logTiming/state-c.execute deleted file mode 120000 index c2827031f7..0000000000 --- a/booster/test/rpc-integration/test-logTiming/state-c.execute +++ /dev/null @@ -1 +0,0 @@ -../resources/a-to-f/state-c.json \ No newline at end of file diff --git a/booster/test/rpc-integration/test-logTiming/test.sh b/booster/test/rpc-integration/test-logTiming/test.sh deleted file mode 100755 index cccafdffe7..0000000000 --- a/booster/test/rpc-integration/test-logTiming/test.sh +++ /dev/null @@ -1,32 +0,0 @@ -#!/usr/bin/env bash - -set -exuo pipefail - -# using variables from runDirectoryTest.sh - -echo "client=$client" -echo "dir=$dir" -echo "arguments=$*" - -diff="git diff --no-index -" -# remove "--regenerate" and tweak $diff if it is present - -client_args="" -for arg in $*; do - case "$arg" in - --regenerate) - echo "Re-generating expectation files" - diff="tee" - ;; - *) - client_args+=" $arg" - ;; - esac -done - -# execute with logging (to a stuck state), compare with time fields removed -echo "Running a request which gets stuck, with logTiming enabled" -${client} \ - execute $dir/state-c.execute ${client_args} -O log-timing=true | \ - jq 'del(.result.logs[].time)' | \ - ${diff} $dir/response-c.json diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 5691a2f16c..24644120ce 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -23,14 +23,12 @@ import Data.Aeson.Text (encodeToLazyText) import Data.Aeson.Types (Value (..)) import Data.Bifunctor (second) import Data.Either (partitionEithers) -import Data.List.NonEmpty qualified as NonEmpty import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, mapMaybe) +import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing) import Data.Text (Text) import Data.Text qualified as Text import Data.Text.Lazy (toStrict) import Network.JSONRPC -import System.Clock (Clock (Monotonic), TimeSpec, diffTimeSpec, getTime, toNanoSecs) import Booster.Definition.Base (KoreDefinition) import Booster.JsonRpc as Booster (ServerState (..), execStateToKoreJson, toExecState) @@ -92,16 +90,14 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of LogSettings { logSuccessfulRewrites = execReq.logSuccessfulRewrites , logFailedRewrites = execReq.logFailedRewrites - , logFallbacks = execReq.logFallbacks - , logTiming = execReq.logTiming } - in liftIO (getTime Monotonic) >>= \start -> do + in do bState <- liftIO $ MVar.readMVar boosterState let m = fromMaybe bState.defaultMain execReq._module def = fromMaybe (error $ "Module " <> show m <> " not found") $ Map.lookup m bState.definitions - handleExecute logSettings def start execReq + handleExecute logSettings def execReq Implies ImpliesRequest{assumeDefined} | fromMaybe False assumeDefined -> do -- try the booster end-point first @@ -123,7 +119,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of logStats ImpliesM (koreTime, koreTime) pure koreRes Simplify simplifyReq -> - liftIO (getTime Monotonic) >>= handleSimplify simplifyReq . Just + handleSimplify simplifyReq AddModule _ -> do -- execute in booster first, assuming that kore won't throw an -- error if booster did not. The response is empty anyway. @@ -168,8 +164,8 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of Cancel -> pure $ Left $ ErrorObj "Cancel not supported" (-32601) Null where - handleSimplify :: SimplifyRequest -> Maybe TimeSpec -> m (Either ErrorObj (API 'Res)) - handleSimplify simplifyReq mbStart = do + handleSimplify :: SimplifyRequest -> m (Either ErrorObj (API 'Res)) + handleSimplify simplifyReq = do -- execute in booster first, then in kore. Log the difference (boosterResult, boosterTime) <- Stats.timed $ booster (Simplify simplifyReq) @@ -199,16 +195,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of fromMaybe "" $ diffBy def boosterRes.state.term koreRes.state.term in Text.pack ("Kore simplification: Diff (< before - > after)\n" <> diff) - stop <- liftIO $ getTime Monotonic - let timing - | Just start <- mbStart - , fromMaybe False simplifyReq.logTiming = - Just - [ RPCLog.ProcessingTime - Nothing - (fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9) - ] - | otherwise = Nothing -- NOTE: we do not include simplification logs into the response pure . Right . Simplify $ SimplifyResult @@ -216,8 +202,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of , logs = postProcessLogs <$> combineLogs - [ timing - , boosterRes.logs + [ boosterRes.logs , koreRes.logs ] } @@ -260,29 +245,10 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of handleExecute :: LogSettings -> KoreDefinition -> - TimeSpec -> ExecuteRequest -> m (Either ErrorObj (API 'Res)) - handleExecute logSettings def start execReq = do - execRes <- executionLoop logSettings def (0, 0.0, 0.0, Nothing) execReq - if (fromMaybe False logSettings.logTiming) - then traverse (addTimeLog start) execRes - else pure execRes - - addTimeLog :: TimeSpec -> API 'Res -> m (API 'Res) - addTimeLog start res = do - stop <- liftIO (getTime Monotonic) - let duration = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - pure $ case res of - Execute result -> - let result' :: ExecuteResult - result' = - result - { reason = result.reason - , logs = combineLogs [Just [RPCLog.ProcessingTime Nothing duration], result.logs] - } - in Execute result' - other -> other + handleExecute logSettings def execReq = do + executionLoop logSettings def (0, 0.0, 0.0, Nothing) execReq postProcessLogs :: [RPCLog.LogEntry] -> [RPCLog.LogEntry] postProcessLogs !logs = map RPCLog.logEntryEraseTerms logs @@ -321,7 +287,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of Booster.Log.logMessage $ Text.pack $ "Forced simplification at " <> show (currentDepth + boosterResult.depth) - simplifyResult <- simplifyExecuteState logSettings r._module def boosterResult.state + simplifyResult <- simplifyExecuteState r._module def boosterResult.state case simplifyResult of Left logsOnly -> do -- state was simplified to \bottom, return vacuous @@ -363,7 +329,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of Booster.Log.logMessage ("Simplifying booster state and falling back to Kore" :: Text) simplifyResult <- if cfg.simplifyBeforeFallback - then simplifyExecuteState logSettings r._module def boosterResult.state + then simplifyExecuteState r._module def boosterResult.state else pure $ Right (boosterResult.state, Nothing) case simplifyResult of Left logsOnly -> do @@ -400,17 +366,12 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of case kResult of Right (Execute koreResult) -> do let - fallbackLog = - if fromMaybe False logSettings.logFallbacks - then Just [mkFallbackLogEntry boosterResult koreResult] - else Nothing accumulatedLogs = combineLogs [ rpcLogs , boosterResult.logs , boosterStateSimplificationLogs , koreResult.logs - , fallbackLog ] loopState incDepth newLogs = ( currentDepth + boosterResult.depth + koreResult.depth + if incDepth then 1 else 0 @@ -485,7 +446,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of [ rpcLogs , boosterResult.logs , map RPCLog.logEntryEraseTerms <$> result.logs - , fallbackLog ] } -- can only be an error at this point @@ -525,23 +485,19 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of -- If the state simplifies to bottom, only the logs are returned, -- otherwise the logs and the simplified state (after splitting it -- into term and predicates by an internal trivial execute call). - -- - -- Only the timing logs will be returned (if requested by the top-level). simplifyExecuteState :: - LogSettings -> Maybe Text -> KoreDefinition -> ExecuteState -> m (Either (Maybe [RPCLog.LogEntry]) (ExecuteState, Maybe [RPCLog.LogEntry])) simplifyExecuteState - LogSettings{logTiming} mbModule def s = do Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Simplifying execution state" simplResult <- - handleSimplify (toSimplifyRequest s) Nothing + handleSimplify (toSimplifyRequest s) case simplResult of -- This request should not fail, as the only possible -- failure mode would be malformed or invalid kore @@ -587,7 +543,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of SimplifyRequest { state = execStateToKoreJson state , _module = mbModule - , logTiming } -- used for post-exec simplification returns either a state to @@ -604,7 +559,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of | otherwise = do Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Simplifying state in " <> show reason <> " result" - simplified <- simplifyExecuteState logSettings mbModule def state + simplified <- simplifyExecuteState mbModule def state case simplified of Left logsOnly -> do -- state simplified to \bottom, return vacuous @@ -615,7 +570,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of simplifiedNexts <- maybe (pure []) - (mapM $ simplifyExecuteState logSettings mbModule def) + (mapM $ simplifyExecuteState mbModule def) nextStates let (logsOnly, (filteredNexts, filteredNextLogs)) = second unzip $ partitionEithers simplifiedNexts @@ -681,8 +636,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of data LogSettings = LogSettings { logSuccessfulRewrites :: Maybe Bool , logFailedRewrites :: Maybe Bool - , logFallbacks :: Maybe Bool - , logTiming :: Maybe Bool } -- | Combine multiple, possibly empty/non-existent (Nothing) lists of logs into one @@ -699,54 +652,3 @@ makeVacuous newLogs execState = , rule = Nothing , logs = combineLogs [execState.logs, newLogs] } - -mkFallbackLogEntry :: ExecuteResult -> ExecuteResult -> RPCLog.LogEntry -mkFallbackLogEntry boosterResult koreResult = - let boosterRewriteFailureLog = filter isRewriteFailureLogEntry . fromMaybe [] $ boosterResult.logs - lastBoosterRewriteLogEntry = case boosterRewriteFailureLog of - [] -> Nothing - xs -> Just $ last xs - fallbackRuleId = - case lastBoosterRewriteLogEntry of - Nothing -> "UNKNOWN" - Just logEntry -> fromMaybe "UNKNOWN" $ getRewriteFailureRuleId logEntry - fallbackReason = - case lastBoosterRewriteLogEntry of - Nothing -> "UNKNOWN" - Just logEntry -> fromMaybe "UNKNOWN" $ getRewriteFailureReason logEntry - koreRewriteSuccessLog = filter isRewriteSuccessLogEntry . fromMaybe [] $ koreResult.logs - koreRuleIds = mapMaybe getRewriteSuccessRuleId koreRewriteSuccessLog - in RPCLog.Fallback - { originalTerm = Just $ execStateToKoreJson boosterResult.state - , rewrittenTerm = Just $ execStateToKoreJson koreResult.state - , reason = fallbackReason - , fallbackRuleId = fallbackRuleId - , recoveryRuleIds = NonEmpty.nonEmpty koreRuleIds - , recoveryDepth = koreResult.depth - , origin = RPCLog.Proxy - } - where - isRewriteFailureLogEntry :: RPCLog.LogEntry -> Bool - isRewriteFailureLogEntry = \case - RPCLog.Rewrite{result = RPCLog.Failure{}} -> True - _ -> False - - isRewriteSuccessLogEntry :: RPCLog.LogEntry -> Bool - isRewriteSuccessLogEntry = \case - RPCLog.Rewrite{result = RPCLog.Success{}} -> True - _ -> False - - getRewriteFailureReason :: RPCLog.LogEntry -> Maybe Text - getRewriteFailureReason = \case - RPCLog.Rewrite{result = RPCLog.Failure{reason}} -> Just reason - _ -> Nothing - - getRewriteFailureRuleId :: RPCLog.LogEntry -> Maybe Text - getRewriteFailureRuleId = \case - RPCLog.Rewrite{result = RPCLog.Failure{_ruleId}} -> _ruleId - _ -> Nothing - - getRewriteSuccessRuleId :: RPCLog.LogEntry -> Maybe Text - getRewriteSuccessRuleId = \case - RPCLog.Rewrite{result = RPCLog.Success{ruleId}} -> Just ruleId - _ -> Nothing diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 9bbf7cefeb..91e72b5f09 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -37,7 +37,6 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess }, "log-successful-rewrites": true, "log-failed-rewrites": true, - "log-timing": true } } ``` @@ -301,30 +300,6 @@ If any logging is enabled, the optional `logs` field will be returned containing where `origin` is one of `kore-rpc`, `booster` or `llvm`. The order of the trace messages in the `logs` array is the order the backend attempted and applied the rules and should allow for visualisation/reconstruction of the steps the backend took. The `original-term-index` is referencing the JSON KORE format and is 0 indexed. The above traces will be emitted when `log-successful-rewrites` and `log-failed-rewrites` are set to true respectively. Not all backends may support both message types. -When `log-timing` is set to `true`, the response to `execute`, `simplify` and `implies` requests will contain information about the wall-clock time spent in different components (`kore-rpc`, `booster`, `proxy`) or overall (without qualifying `component`) while processing the request. - -```json -{ - "tag": "processing-time", - "time": 69.12 -}, -{ - "tag": "processing-time", - "component": "kore-rpc", - "time": 12.34 -}, -{ - "tag": "processing-time", - "component": "booster", - "time": 56.78 -} -``` -The number in the `time` field of an entry represents time in seconds. - -When no component is given, the time (`69.12` in the example) is the overall wall-clock time spent processing the request, including the given component timings (which are optional). There should be at most one log object without `component` in the list of `logs`. In contrast, log entries with `component` may be repeated (in case there were several entries into the component). - -Not all backends support logging processing time, and some won't have the different components featured as `origin` here. - ## Implies ### Request: @@ -338,13 +313,12 @@ Not all backends support logging processing time, and some won't have the differ "antecedent": {"format": "KORE", "version": 1, "term": {}}, "consequent": {"format": "KORE", "version": 1, "term": {}}, "module": "MODULE-NAME", - "log-timing": true, "assume-defined": false } } ``` -Optional parameters: `module` (main module name), `log-timing`, `assume-defined`. +Optional parameters: `module` (main module name), `assume-defined`. The `assume-defined` flag defaults to `false`. When set to `true`, the server uses the new simplified implication check in booster, which makes the assumption that the antecedent and consequent are bot defined, i.e. don't simplify to `#Bottom`. @@ -436,12 +410,11 @@ indicating that the program configuration can be rewritten further => `satisfiab "params": { "state": {"format": "KORE", "version": 1, "term": {}}, "module": "MODULE-NAME", - "log-timing": true } } ``` -Optional parameters: `module` (main module name), `log-timing` +Optional parameters: `module` (main module name) ### Error Response: diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index dc7086bce0..fdc578778c 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -46,8 +46,6 @@ data ExecuteRequest = ExecuteRequest , assumeStateDefined :: !(Maybe Bool) , logSuccessfulRewrites :: !(Maybe Bool) , logFailedRewrites :: !(Maybe Bool) - , logFallbacks :: !(Maybe Bool) - , logTiming :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) deriving @@ -59,7 +57,6 @@ data ImpliesRequest = ImpliesRequest , consequent :: !KoreJson , _module :: !(Maybe Text) , assumeDefined :: !(Maybe Bool) - , logTiming :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) deriving @@ -69,7 +66,6 @@ data ImpliesRequest = ImpliesRequest data SimplifyRequest = SimplifyRequest { state :: KoreJson , _module :: !(Maybe Text) - , logTiming :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) deriving diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 1f54c929db..31eeed710b 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -117,7 +117,6 @@ import Log qualified import Network.JSONRPC (fromId) import Prelude.Kore import SMT qualified -import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs) respond :: forall m. @@ -145,9 +144,7 @@ respond reqId serverState moduleName runSMT = , assumeStateDefined , stepTimeout , logSuccessfulRewrites - , logTiming } -> withMainModule (coerce _module) $ \serializedModule lemmas -> do - start <- liftIO $ getTime Monotonic case verifyIn serializedModule state of Left Error{errorError, errorContext} -> pure $ @@ -180,14 +177,7 @@ respond reqId serverState moduleName runSMT = verifiedPattern ) - stop <- liftIO $ getTime Monotonic - let duration = - if (fromMaybe False logTiming) - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ buildResult duration (TermLike.termLikeSort verifiedPattern) traversalResult + pure $ buildResult (TermLike.termLikeSort verifiedPattern) traversalResult where toStopLabels :: Maybe [Text] -> Maybe [Text] -> Exec.StopLabels toStopLabels cpRs tRs = @@ -204,32 +194,29 @@ respond reqId serverState moduleName runSMT = Set.fromList $ concat [[Left ruleLabel, Right ruleId] | Exec.RuleTrace{ruleId, ruleLabel} <- toList rules] in either unLabel getUniqueId <$> Set.lookupMin (requestSet `Set.intersection` ruleSet) - mkLogs mbDuration rules - | isJust mbDuration - || fromMaybe False logSuccessfulRewrites = + mkLogs rules + | fromMaybe False logSuccessfulRewrites = Just . concat $ - maybe [] (\t -> [ProcessingTime (Just KoreRpc) t]) mbDuration - : [ [ Rewrite - { result = - Success - { rewrittenTerm = Nothing - , substitution = Nothing - , ruleId = fromMaybe "UNKNOWN" $ getUniqueId ruleId - } - , origin = KoreRpc + [ [ Rewrite + { result = + Success + { rewrittenTerm = Nothing + , substitution = Nothing + , ruleId = fromMaybe "UNKNOWN" $ getUniqueId ruleId } - | fromMaybe False logSuccessfulRewrites - ] - | Exec.RuleTrace{ruleId} <- toList rules - ] + , origin = KoreRpc + } + | fromMaybe False logSuccessfulRewrites + ] + | Exec.RuleTrace{ruleId} <- toList rules + ] | otherwise = Nothing buildResult :: - Maybe Double -> TermLike.Sort -> GraphTraversal.TraversalResult (Exec.RpcExecState RewritingVariableName) -> Either ErrorObj (API 'Res) - buildResult mbDuration sort = \case + buildResult sort = \case GraphTraversal.Ended [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState = result, rpcRules = rules}] -> -- Actually not "ended" but out of instructions. @@ -242,7 +229,7 @@ respond reqId serverState moduleName runSMT = , reason = if Just (Depth depth) == maxDepth then DepthBound else Stuck , rule = Nothing , nextStates = Nothing - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } GraphTraversal.GotStuck @@ -258,7 +245,7 @@ respond reqId serverState moduleName runSMT = , reason = Stuck , rule = Nothing , nextStates = Nothing - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } GraphTraversal.GotStuck @@ -274,7 +261,7 @@ respond reqId serverState moduleName runSMT = , reason = Vacuous , rule = Nothing , nextStates = Nothing - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } GraphTraversal.Stopped @@ -290,7 +277,7 @@ respond reqId serverState moduleName runSMT = , rule , nextStates = Just $ map (patternToExecState False sort . Exec.rpcProgState) nexts - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } | Just rule <- containsLabelOrRuleId rules terminalRules -> @@ -302,7 +289,7 @@ respond reqId serverState moduleName runSMT = , reason = TerminalRule , rule , nextStates = Nothing - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } | otherwise -> @@ -315,7 +302,7 @@ respond reqId serverState moduleName runSMT = , rule = Nothing , nextStates = Just $ map (patternToExecState True sort . Exec.rpcProgState) nexts - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } GraphTraversal.TimedOut @@ -329,7 +316,7 @@ respond reqId serverState moduleName runSMT = , reason = Timeout , rule = Nothing , nextStates = Nothing - , logs = mkLogs mbDuration rules + , logs = mkLogs rules , unknownPredicate = Nothing } -- these are programmer errors @@ -408,8 +395,7 @@ respond reqId serverState moduleName runSMT = a ||| b = \v -> a v || b v -- Step StepRequest{} -> pure $ Right $ Step $ StepResult [] - Implies ImpliesRequest{antecedent, consequent, _module, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do - start <- liftIO $ getTime Monotonic + Implies ImpliesRequest{antecedent, consequent, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do case PatternVerifier.runPatternVerifier (verifierContext serializedModule) verify of Left Error{errorError, errorContext} -> pure $ @@ -438,15 +424,7 @@ respond reqId serverState moduleName runSMT = leftPatt rightPatt existentialVars - stop <- liftIO $ getTime Monotonic - let timeLog = - ProcessingTime - (Just KoreRpc) - (fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9) - allLogs = - if (fromMaybe False logTiming) - then Just [timeLog] - else Nothing + let allLogs = Nothing pure $ buildResult allLogs sort result where verify = do @@ -495,8 +473,7 @@ respond reqId serverState moduleName runSMT = in ImpliesResult jsonTerm False (Just jsonCond) logs Claim.NotImpliedStuck Nothing -> ImpliesResult jsonTerm False (Just . renderCond sort $ Condition.bottom) logs - Simplify SimplifyRequest{state, _module, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do - start <- liftIO $ getTime Monotonic + Simplify SimplifyRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do case verifyIn serializedModule state of Left Error{errorError, errorContext} -> pure $ @@ -518,15 +495,7 @@ respond reqId serverState moduleName runSMT = . evalInSimplifierContext serializedModule $ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt - stop <- liftIO $ getTime Monotonic - let timeLog = - ProcessingTime - (Just KoreRpc) - (fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9) - allLogs = - if (fromMaybe False logTiming) - then Just [timeLog] - else Nothing + let allLogs = Nothing pure $ Right $ Simplify diff --git a/scripts/performance-tests-kevm.sh b/scripts/performance-tests-kevm.sh index 2ca4ec2df3..e0f2c27563 100755 --- a/scripts/performance-tests-kevm.sh +++ b/scripts/performance-tests-kevm.sh @@ -107,6 +107,7 @@ feature_shell "cd kevm-pyk && poetry run pytest src/tests/integration/test_prove mkdir -p $SCRIPT_DIR/logs # use special options if given, but restore KORE_RPC_OPTS afterwards +FEATURE_SERVER_OPTS=${FEATURE_SERVER_OPTS:-''} if [ ! -z "${FEATURE_SERVER_OPTS}" ]; then echo "Using special options '${FEATURE_SERVER_OPTS}' via KORE_RPC_OPTS" if [ ! -z "${KORE_RPC_OPTS:-}" ]; then diff --git a/test/rpc-server/logTiming/definition.kore b/test/rpc-server/logTiming/definition.kore deleted file mode 120000 index bf27cbb489..0000000000 --- a/test/rpc-server/logTiming/definition.kore +++ /dev/null @@ -1 +0,0 @@ -../resources/a-to-f/definition.kore \ No newline at end of file diff --git a/test/rpc-server/logTiming/params.json b/test/rpc-server/logTiming/params.json deleted file mode 100644 index 84b6939be6..0000000000 --- a/test/rpc-server/logTiming/params.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "log-timing": true -} diff --git a/test/rpc-server/logTiming/response.golden b/test/rpc-server/logTiming/response.golden deleted file mode 100644 index 77f9f40e57..0000000000 --- a/test/rpc-server/logTiming/response.golden +++ /dev/null @@ -1 +0,0 @@ -{"jsonrpc":"2.0","id":1,"result":{"reason":"stuck","depth":3,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"f"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}}}} diff --git a/test/rpc-server/logTiming/state.json b/test/rpc-server/logTiming/state.json deleted file mode 100644 index 5fe8d19406..0000000000 --- a/test/rpc-server/logTiming/state.json +++ /dev/null @@ -1,85 +0,0 @@ -{ - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "LblinitGeneratedTopCell", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'Unds'Map'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'Stop'Map", - "sorts": [], - "args": [] - }, - { - "tag": "App", - "name": "Lbl'UndsPipe'-'-GT-Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortKConfigVar", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortKConfigVar", - "args": [] - }, - "value": "$PGM" - } - ] - }, - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "c" - } - ] - } - ] - } - ] - } - ] - } -} diff --git a/test/rpc-server/runTests.py b/test/rpc-server/runTests.py index 14f2f856b2..fad1992984 100644 --- a/test/rpc-server/runTests.py +++ b/test/rpc-server/runTests.py @@ -280,81 +280,4 @@ def runTest(def_path, req, resp_golden_path, smt_tactic = None): req = rpc_request_id1("get-model", params) runTest(get_model_def_path, req, resp_golden_path) -print("Running test for log-timing") - -dir_path = "./logTiming/" -def_path = dir_path + "definition.kore" -with subprocess.Popen(f"{SERVER} {def_path} --module TEST --server-port {PORT} --log-level {server_log_level[VERBOSITY]}".split()) as process: - with socket.socket(socket.AF_INET, socket.SOCK_STREAM) as s: - while True: - try: - s.connect((HOST, PORT)) - debug("Connected to server...") - break - except: - pass - try: - with open(dir_path + "state.json", 'r') as state_json: - state = json.loads(state_json.read()) - - info(f"- test with time logging enabled") - params_execute = json.loads('{ "log-timing": true }') - params_execute["state"] = state - debug(f"Request data: '{params_execute}'") - req_execute = rpc_request_id1("execute", params_execute) - s.sendall(req_execute) - resp = recv_all(s) - debug(f"Received '{resp}'") - respStr = str(resp, "utf-8") - debug(f"Received '{respStr}'") - respJson = json.loads(respStr) - # check expected fields successively: - if respJson["result"] is None: - info(f"Cannot find expected path .result in response '{respJson}'") - exit(1) - elif respJson["result"]["logs"] is None: - info(f"Cannot find expected path .result.logs[] in response '{respJson}'") - exit(1) - elif respJson["result"]["logs"][0]["time"] is None: - info(f"Cannot find expected path .result.logs[0].time in response '{respJson}'") - exit(1) - else: # expect result.logs[].timing to be a list containing a singleton 2-element list - timeValue = respJson["result"]["logs"][0]["time"] - if not timeValue > 0.0: - info(f'Received time value {timeValue} is invalid') - exit(1) - else: - info(f"Test with time logging {green}passed{endgreen}") - - info(f"- test with time logging explicitly disabled") - params_execute = {} - params_execute["state"] = state - debug(f"Request data: '{params_execute}'") - req_execute = rpc_request_id1("execute", params_execute) - s.sendall(req_execute) - resp = recv_all(s) - debug(f"Received '{resp}'") - name = "time logging disabled" - checkGolden(resp, dir_path + "response.golden") - # run a (trivial) simplify request with logTiming - info("- trivial simplification with time logging") - params_simplify = json.loads('{"log-timing": true}') - params_simplify["state"] = state - req_simplify = rpc_request_id1("simplify", params_simplify) - s.sendall(req_simplify) - resp = recv_all(s) - debug(f"Received '{resp}'") - try: - time = json.loads(str(resp, "utf-8"))["result"]["logs"][0]["time"] - except: - info("Cannot find expected path .result.logs[].time in response") - exit(1) - if not time > 0.0: - info(f"Received time value {time} is invalid") - exit(1) - else: - info(f"Simplification test with time logging {green}passed{endgreen}") - finally: - process.kill() - print("That's all, folks")