diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json index adce093c44..f4fd629e52 100644 --- a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json +++ b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json @@ -58,13 +58,69 @@ ] }, { - "tag": "EVar", - "name": "VarCONTINUATION", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'Hash'pc'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortBinStackOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "LblJUMPI'Unds'EVM'Unds'BinStackOp", + "sorts": [], + "args": [] + } + ] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarCONTINUATION", + "sort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + } + ] } ] } @@ -8757,10 +8813,10 @@ }, { "tag": "rewrite", - "origin": "booster", + "origin": "proxy", "result": { "tag": "success", - "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1" + "rule-id": "0ee7a2c1d6ff36a91ac9e9ed19a2c624ba21b97f4511af22044f6169bb8adfa1" } }, { @@ -8768,7 +8824,7 @@ "origin": "booster", "result": { "tag": "success", - "rule-id": "d40db55be13c107a708382df2ae9cea0d6305bbf5d6804de46250d7076a392e2" + "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1" } } ] diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json index 450e95c271..cc6b3c5d01 100644 --- a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json +++ b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json @@ -58,13 +58,69 @@ ] }, { - "tag": "EVar", - "name": "VarCONTINUATION", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'Hash'pc'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortBinStackOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "LblJUMPI'Unds'EVM'Unds'BinStackOp", + "sorts": [], + "args": [] + } + ] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarCONTINUATION", + "sort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + } + ] } ] } @@ -8749,10 +8805,10 @@ "logs": [ { "tag": "rewrite", - "origin": "booster", + "origin": "proxy", "result": { "tag": "success", - "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1" + "rule-id": "0ee7a2c1d6ff36a91ac9e9ed19a2c624ba21b97f4511af22044f6169bb8adfa1" } }, { @@ -8760,7 +8816,7 @@ "origin": "booster", "result": { "tag": "success", - "rule-id": "d40db55be13c107a708382df2ae9cea0d6305bbf5d6804de46250d7076a392e2" + "rule-id": "20bc9774d59030dcada92e997351315ed198a464546f5b36d67578cfd12938d1" } } ] diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 93ef9b513c..cbf085b7e0 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -412,18 +412,18 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of , koreResult.logs , fallbackLog ] - loopState newLogs = - ( currentDepth + boosterResult.depth + koreResult.depth + loopState incDepth newLogs = + ( currentDepth + boosterResult.depth + koreResult.depth + if incDepth then 1 else 0 , time + bTime + kTime , koreTime + kTime , postProcessLogs <$> combineLogs (accumulatedLogs : newLogs) ) - continueWith newLogs nextState = + continueWith incDepth newLogs nextState = executionLoop logSettings def - (loopState newLogs) + (loopState incDepth newLogs) r{ExecuteRequest.state = nextState} case (boosterResult.reason, koreResult.reason) of (Aborted, res) -> @@ -455,7 +455,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of "kore depth-bound, continuing... (currently at " <> show (currentDepth + boosterResult.depth + koreResult.depth) <> ")" - continueWith [] (execStateToKoreJson koreResult.state) + continueWith False [] (execStateToKoreJson koreResult.state) _ -> do -- otherwise we have hit a different -- HaltReason, at which point we should @@ -471,7 +471,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of case postExecResult of Left (nextState, newLogs) -> do -- simplification revealed that we should actually proceed - continueWith newLogs nextState + continueWith True newLogs nextState Right result -> do logStats ExecuteM (time + bTime + kTime, koreTime + kTime) pure $ @@ -621,32 +621,59 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of second unzip $ partitionEithers simplifiedNexts newLogs = simplifiedStateLogs : logsOnly <> filteredNextLogs - pure $ case reason of + when (length filteredNexts < maybe 0 length nextStates) $ + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage' + (Text.pack ("Pruned #Bottom states: " <> show (length nextStates))) + + case reason of Branching - | null filteredNexts -> - Right - res - { reason = Stuck - , nextStates = Nothing - , logs = combineLogs $ res.logs : simplifiedStateLogs : logsOnly - } - | length filteredNexts == 1 -> + | null filteredNexts -> do + pure $ + Right + res + { reason = Stuck + , nextStates = Nothing + , logs = combineLogs $ res.logs : simplifiedStateLogs : logsOnly + } + | length filteredNexts == 1 -> do -- all but one next states are bottom, execution should proceed - Left (execStateToKoreJson $ head filteredNexts, logsOnly <> filteredNextLogs) + -- Note that we've effectively made a rewrite step here, so we need to + -- extract the rule-id information from the result we proceed with + let onlyNext = head filteredNexts + rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId + proxyRewriteStepLog = + RPCLog.Rewrite + { result = + RPCLog.Success + { rewrittenTerm = Nothing + , substitution = Nothing + , ruleId = rewriteRuleId + } + , origin = RPCLog.Proxy + } + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage' ("Continuing after rewriting with rule " <> rewriteRuleId) + pure $ + Left + ( execStateToKoreJson onlyNext + , logsOnly <> filteredNextLogs <> [Just [proxyRewriteStepLog]] + ) -- otherwise falling through to _otherReason CutPointRule | null filteredNexts -> - Right $ makeVacuous (combineLogs $ res.logs : newLogs) res + pure $ Right $ makeVacuous (combineLogs $ res.logs : newLogs) res _otherReason -> - Right $ - res - { state = simplifiedState - , nextStates = - if null filteredNexts - then Nothing - else Just filteredNexts - , logs = combineLogs $ res.logs : newLogs - } + pure $ + Right $ + res + { state = simplifiedState + , nextStates = + if null filteredNexts + then Nothing + else Just filteredNexts + , logs = combineLogs $ res.logs : newLogs + } data LogSettings = LogSettings { logSuccessfulRewrites :: Maybe Bool