From b2bade8ce62e5f3add32d87e98244ceb31790f9f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 24 Nov 2023 10:42:17 +0100 Subject: [PATCH] Add optional unknown predicate into "execute" response (#3697) Add `"unknown-predicate"` as an optional field to `"execute"` JSON-RPC response. The intention is to change servers' response on encountering `ErrorDecidePredicateUnknwon`, i.e. when Z3 returns Unknwon while checking a rewrite rule's side condition. The current behavior is to return `SmtSolverError` even if progress was made. I.e. we could have made 100 rewrite steps and only get Unknown during step 101. Instead, we should return the state before the error, and the predicate that Z3 had trouble deciding. This way, the client will be able to make an informed decision about that to do next and/or report the problematic predicate to the user, so that they can add lemmas if appropriate. Unfortunately, altering `kore-rpc` itself is quite difficult. therefore I will implement a prototype of this in `Proxy.hs` of `kore-rpc-booster`. The type and docs need to be update here though. --------- Co-authored-by: Jost Berthold --- docs/2022-07-18-JSON-RPC-Server-API.md | 20 +++++++++++++++++++- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 1 + kore/src/Kore/JsonRpc.hs | 7 +++++++ 3 files changed, 27 insertions(+), 1 deletion(-) diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 6f5e2b5ac0..8678725b7f 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -142,7 +142,25 @@ This response has no additional fields. ##### `"reason": "aborted"` Execution reached a state that the server cannot handle. -This response has no additional fields. +The `unknown-predicate` field MAY contain a predicate that could not be decided by the server's constraint solver. + +```json +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "state": { + "term": {"format":"KORE", "version":1, "term":{}}, + "predicate": {"format":"KORE", "version":1, "term":{}}, + "substitution": {"format":"KORE", "version":1, "term":{}}, + }, + "depth": 2, + "reason": "aborted", + "unknown-predicate": {"format":"KORE", "version":1, "term":{}} + "logs": [] + } +} +``` ##### `"reason": "cut-point-rule"` Execution was about to perform a rewrite with a rule whose label is one of the `cut-point-rules` labels/IDs of the request. diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 73809a59c4..81340a5460 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -134,6 +134,7 @@ data ExecuteResult = ExecuteResult , nextStates :: Maybe [ExecuteState] , rule :: Maybe Text , logs :: Maybe [LogEntry] + , unknownPredicate :: Maybe KoreJson } deriving stock (Generic, Show, Eq) deriving diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index fc59af03d7..b08d24209c 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -226,6 +226,7 @@ respond serverState moduleName runSMT = , rule = Nothing , nextStates = Nothing , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } GraphTraversal.GotStuck _n @@ -241,6 +242,7 @@ respond serverState moduleName runSMT = , rule = Nothing , nextStates = Nothing , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } GraphTraversal.GotStuck _n @@ -256,6 +258,7 @@ respond serverState moduleName runSMT = , rule = Nothing , nextStates = Nothing , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } GraphTraversal.Stopped [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules}] @@ -271,6 +274,7 @@ respond serverState moduleName runSMT = , nextStates = Just $ map (patternToExecState sort . Exec.rpcProgState) nexts , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } | Just rule <- containsLabelOrRuleId rules terminalRules -> Right $ @@ -282,6 +286,7 @@ respond serverState moduleName runSMT = , rule , nextStates = Nothing , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } | otherwise -> Right $ @@ -294,6 +299,7 @@ respond serverState moduleName runSMT = , nextStates = Just $ map (patternToExecState sort . Exec.rpcProgState) nexts , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } GraphTraversal.TimedOut Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules} @@ -307,6 +313,7 @@ respond serverState moduleName runSMT = , rule = Nothing , nextStates = Nothing , logs = mkLogs mbDuration rules + , unknownPredicate = Nothing } -- these are programmer errors result@GraphTraversal.Aborted{} ->