diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index 1bc647ca1..9397ad7e9 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -14,6 +14,7 @@ module Booster.JsonRpc ( execStateToKoreJson, ) where +import Control.Applicative ((<|>)) import Control.Concurrent (MVar, newMVar, putMVar, readMVar, takeMVar) import Control.Monad import Control.Monad.IO.Class @@ -97,6 +98,7 @@ respond stateVar = , req.logFailedRewrites , req.logSuccessfulSimplifications , req.logFailedSimplifications + , req.logFallbacks ] result <- performRewrite doTracing def mLlvmLibrary mbDepth cutPoints terminals pat stop <- liftIO $ getTime Monotonic @@ -355,13 +357,19 @@ execResponse mbDuration req (d, traces, rr) = case rr of , nextStates = Nothing , rule = Nothing } - RewriteAborted p -> + RewriteAborted failure p -> do Right $ RpcTypes.Execute RpcTypes.ExecuteResult { reason = RpcTypes.Aborted , depth - , logs + , logs = + let abortRewriteLog = + mkLogRewriteTrace + (logSuccessfulRewrites, logFailedRewrites) + (logSuccessfulSimplifications, logFailedSimplifications) + (RewriteStepFailed failure) + in logs <|> abortRewriteLog , state = toExecState p , nextStates = Nothing , rule = Nothing diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index 83ee891c3..dabad269a 100644 --- a/library/Booster/Pattern/Rewrite.hs +++ b/library/Booster/Pattern/Rewrite.hs @@ -397,7 +397,7 @@ data RewriteResult pat RewriteFinished (Maybe Text) (Maybe UniqueId) pat | -- | unable to handle the current case with this rewriter -- (signalled by exceptions) - RewriteAborted pat + RewriteAborted (RewriteFailed "Rewrite") pat | -- | All applicable rules returned a pattern with a False -- ensures clause RewriteTrivial pat @@ -637,8 +637,8 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa maybe (RewriteTrivial orig) (RewriteTerminal lbl uId) <$> simplifyP p RewriteFinished lbl uId p -> maybe (RewriteTrivial orig) (RewriteFinished lbl uId) <$> simplifyP p - RewriteAborted p -> - maybe (RewriteTrivial orig) RewriteAborted <$> simplifyP p + RewriteAborted reason p -> + maybe (RewriteTrivial orig) (RewriteAborted reason) <$> simplifyP p logTraces = mapM_ (logSimplify . pack . renderDefault . pretty) @@ -719,8 +719,8 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa rewriteTrace $ RewriteStepFailed failure let msg = "Aborted after " <> showCounter counter if wasSimplified - then logRewrite msg >> pure (RewriteAborted pat') - else withSimplified pat' msg (pure . RewriteAborted) + then logRewrite msg >> pure (RewriteAborted failure pat') + else withSimplified pat' msg (pure . RewriteAborted failure) where withSimplified p msg cont = do simplifyP p >>= \case diff --git a/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json new file mode 100644 index 000000000..1c289c24b --- /dev/null +++ b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json @@ -0,0 +1,9 @@ +{ + "log-fallbacks": true, + "log-failed-rewrites": true, + "log-successful-rewrites": true, + "terminal-rules": [ + "TEST.EG", + "TEST.FG" + ] +} diff --git a/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json new file mode 100644 index 000000000..878b131fb --- /dev/null +++ b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json @@ -0,0 +1,8 @@ +{ + "log-fallbacks": true, + "log-failed-rewrites": true, + "terminal-rules": [ + "TEST.EG", + "TEST.FG" + ] +} diff --git a/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json new file mode 100644 index 000000000..ab7d6d7b6 --- /dev/null +++ b/test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json @@ -0,0 +1,7 @@ +{ + "log-fallbacks": true, + "terminal-rules": [ + "TEST.EG", + "TEST.FG" + ] +} diff --git a/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json new file mode 100644 index 000000000..636fbf109 --- /dev/null +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json @@ -0,0 +1,408 @@ +{ + "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/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json new file mode 100644 index 000000000..a49aeafc0 --- /dev/null +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json @@ -0,0 +1,299 @@ +{ + "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/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json new file mode 100644 index 000000000..0d186dc28 --- /dev/null +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal-log-fallbacks.json @@ -0,0 +1,290 @@ +{ + "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/test/rpc-integration/test-logTiming/response-c.json b/test/rpc-integration/test-logTiming/response-c.json index a252eb05b..4762a753b 100644 --- a/test/rpc-integration/test-logTiming/response-c.json +++ b/test/rpc-integration/test-logTiming/response-c.json @@ -88,14 +88,6 @@ "tag": "processing-time", "component": "booster" }, - { - "tag": "processing-time", - "component": "booster" - }, - { - "tag": "processing-time", - "component": "kore-rpc" - }, { "tag": "processing-time", "component": "kore-rpc" diff --git a/test/rpc-integration/test-logTiming/test.sh b/test/rpc-integration/test-logTiming/test.sh index b8c1c1573..71e99f7f2 100755 --- a/test/rpc-integration/test-logTiming/test.sh +++ b/test/rpc-integration/test-logTiming/test.sh @@ -27,5 +27,5 @@ done 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)' | \ + $JQ 'del(.result.logs[].time)' | \ ${diff} $dir/response-c.json diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index 83727698b..f20877861 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -20,7 +20,8 @@ import Data.Aeson.KeyMap qualified as Aeson import Data.Aeson.Types (Value (..)) import Data.Bifunctor (second) import Data.Either (partitionEithers) -import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, mapMaybe) import Data.Text (Text) import Data.Text qualified as Text import Network.JSONRPC @@ -75,6 +76,7 @@ respondEither mbStatsVar booster kore req = case req of , logFailedSimplifications = execReq.logFailedSimplifications , logSuccessfulRewrites = execReq.logSuccessfulRewrites , logFailedRewrites = execReq.logFailedRewrites + , logFallbacks = execReq.logFallbacks , logTiming = execReq.logTiming } in liftIO (getTime Monotonic) >>= \start -> @@ -220,55 +222,59 @@ respondEither mbStatsVar booster kore req = case req of Log.logInfoNS "proxy" . Text.pack $ "Kore fall-back in " <> microsWithUnit kTime case kResult of - Right (Execute koreResult) - | koreResult.reason == DepthBound -> do - -- if we made one step, add the number of - -- steps we have taken to the counter and - -- attempt with booster again - when (koreResult.depth == 0) $ error "Expected kore-rpc to take at least one step" - Log.logInfoNS "proxy" $ - Text.pack $ - "kore depth-bound, continuing... (currently at " - <> show (currentDepth + boosterResult.depth + koreResult.depth) - <> ")" - let accumulatedLogs = - combineLogs - [ rpcLogs - , boosterResult.logs - , boosterStateSimplificationLogs - , koreResult.logs - ] - executionLoop - logSettings - ( currentDepth + boosterResult.depth + koreResult.depth - , time + bTime + kTime - , koreTime + kTime - , accumulatedLogs - ) - r{ExecuteRequest.state = execStateToKoreJson koreResult.state} - | otherwise -> do - -- otherwise we have hit a different - -- HaltReason, at which point we should - -- return, setting the correct depth - Log.logInfoNS "proxy" . Text.pack $ - "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth - logStats ExecuteM (time + bTime + kTime, koreTime + kTime) - pure $ - Right $ - Execute - koreResult - { depth = - currentDepth - + boosterResult.depth - + koreResult.depth - , logs = - combineLogs - [ rpcLogs - , boosterResult.logs - , boosterStateSimplificationLogs - , koreResult.logs - ] - } + Right (Execute koreResult) -> do + let + fallbackLog = + if fromMaybe False logSettings.logFallbacks + then Just [mkFallbackLogEntry boosterResult koreResult] + else Nothing + case koreResult.reason of + DepthBound -> do + -- if we made one step, add the number of + -- steps we have taken to the counter and + -- attempt with booster again + when (koreResult.depth == 0) $ error "Expected kore-rpc to take at least one step" + Log.logInfoNS "proxy" $ + Text.pack $ + "kore depth-bound, continuing... (currently at " + <> show (currentDepth + boosterResult.depth + koreResult.depth) + <> ")" + let accumulatedLogs = + combineLogs + [ rpcLogs + , boosterResult.logs + , boosterStateSimplificationLogs + , koreResult.logs + , fallbackLog + ] + executionLoop + logSettings + ( currentDepth + boosterResult.depth + koreResult.depth + , time + bTime + kTime + , koreTime + kTime + , accumulatedLogs + ) + r{ExecuteRequest.state = execStateToKoreJson koreResult.state} + _ -> do + -- otherwise we have hit a different + -- HaltReason, at which point we should + -- return, setting the correct depth + Log.logInfoNS "proxy" . Text.pack $ + "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth + logStats ExecuteM (time + bTime + kTime, koreTime + kTime) + pure $ + Right $ + Execute + koreResult + { depth = currentDepth + boosterResult.depth + koreResult.depth + , logs = + combineLogs + [ rpcLogs + , boosterResult.logs + , koreResult.logs + , fallbackLog + ] + } -- can only be an error at this point res -> pure res | otherwise -> do @@ -430,6 +436,7 @@ data LogSettings = LogSettings , logFailedSimplifications :: Maybe Bool , logSuccessfulRewrites :: Maybe Bool , logFailedRewrites :: Maybe Bool + , logFallbacks :: Maybe Bool , logTiming :: Maybe Bool } @@ -447,3 +454,54 @@ 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/unit-tests/Test/Booster/Pattern/Rewrite.hs b/unit-tests/Test/Booster/Pattern/Rewrite.hs index ec9669bb5..5ee32de72 100644 --- a/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -280,8 +280,8 @@ runRewrite t = do (counter, _, res) <- runNoLoggingT $ performRewrite False def Nothing Nothing [] [] $ Pattern t [] pure (counter, fmap (.term) res) -aborts :: Term -> IO () -aborts t = runRewrite t >>= (@?= (0, RewriteAborted t)) +aborts :: RewriteFailed "Rewrite" -> Term -> IO () +aborts failure t = runRewrite t >>= (@?= (0, RewriteAborted failure t)) newtype Steps = Steps Natural @@ -294,11 +294,15 @@ canRewrite = testGroup "Can rewrite" [ testCase "Rewrites con1 once, then aborts" $ - rewrites - (Steps 1) - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - RewriteAborted + let startTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + targetTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + in rewrites + (Steps 1) + startTerm + targetTerm + (RewriteAborted (NoRulesForTerm targetTerm)) , testCase "Rewrites con3 twice, branching on con1" $ do let branch1 = ( "con1-f2" @@ -328,10 +332,14 @@ abortsOnErrors :: TestTree abortsOnErrors = testGroup "Aborts rewrite when there is an error" - [ testCase "when there are no rules at all" $ aborts (app con2 [d]) + [ testCase "when there are no rules at all" $ + let term = app con2 [d] in aborts (NoRulesForTerm term) term , testCase "when the term index is None" $ - aborts - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( \and{SomeSort{}}( con1{}( \dv{SomeSort{}}("thing") ), con2{}( \dv{SomeSort{}}("thing") ) ) ), C:SortK{} ) ) |] + let term = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( \and{SomeSort{}}( con1{}( \dv{SomeSort{}}("thing") ), con2{}( \dv{SomeSort{}}("thing") ) ) ), C:SortK{} ) ) |] + in aborts + (TermIndexIsNone term) + term ] callsError :: TestTree @@ -351,9 +359,11 @@ abortsOnFailures = testGroup "Aborts rewrite when the rewriter cannot handle it" [ testCase "when unification is not a match" $ - aborts [trm| con3{}(X:SomeSort{}, \dv{SomeSort{}}("thing")) |] + let term = [trm| con3{}(X:SomeSort{}, \dv{SomeSort{}}("thing")) |] + in aborts (NoRulesForTerm term) term , testCase "when definedness is unclear" $ - aborts [trm| con4{}(\dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing")) |] + let term = [trm| con4{}(\dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing")) |] + in aborts (NoRulesForTerm term) term ] newtype MaxDepth = MaxDepth Natural @@ -363,12 +373,16 @@ supportsDepthControl = testGroup "supports maximum depth control" [ testCase "executes normally when maxDepth > maximum expected" $ - rewritesToDepth - (MaxDepth 42) - (Steps 1) - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - RewriteAborted + let startTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + targetTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + in rewritesToDepth + (MaxDepth 42) + (Steps 1) + startTerm + targetTerm + (RewriteAborted $ NoRulesForTerm targetTerm) , testCase "stops execution after 1 step when maxDepth == 1" $ rewritesToDepth (MaxDepth 1) @@ -425,12 +439,16 @@ supportsCutPoints = [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] ) , testCase "ignores non-matching cut-point labels" $ - rewritesToCutPoint - "otherLabel" - (Steps 1) - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - RewriteAborted + let startTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + targetTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + in rewritesToCutPoint + "otherLabel" + (Steps 1) + startTerm + targetTerm + (RewriteAborted (NoRulesForTerm targetTerm)) , testCase "prefers reporting branches to stopping at label in one branch" $ do let branch1 = ( "con1-f2" @@ -469,12 +487,16 @@ supportsTerminalRules = [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] (RewriteTerminal "con1-f1" Nothing) , testCase "ignores non-matching labels" $ - rewritesToTerminal - "otherLabel" - (Steps 1) - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] - RewriteAborted + let startTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + targetTerm = + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] + in rewritesToTerminal + "otherLabel" + (Steps 1) + startTerm + targetTerm + (RewriteAborted (NoRulesForTerm targetTerm)) ] where rewritesToTerminal :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO ()