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 <[email protected]>
runtimeverification · Nov 24, 2023 · b2bade8 · b2bade8
1 parent 2f90bbf
commit b2bade8
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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{} ->