Skip to content

Commit bc49fae

Browse files
jbertholdjberthold
authored
[3143] Modifications to the JSON-RPC API for execute request (#3192)
* Modifications to the JSON-RPC API description To accommodate the requirements on the future `execute` implementation, the API description was modified in the following way: In the response to an `execute` request: * added current `state` field * added `rule` field (optional, filled for `cut-point-rule` or `terminal-rule`) * renamed `states` to `next-states` (optional, filled for `branching` or `cut-point-rule`) * avoid repetition of the `depth` field See #3143 for additional information. * 3143 adapt JSON RPC server code to modified response * 3143 behaviour-preserving extensions to GraphTraversal * Draft code implementing rpc execute request * Included predicate and substitution into execution state We continue to have a duplicate field name (`state` containing `state`) but this is more consistent with other endpoint data than renaming to `term`. * modify Aborted result to return the entire queue * draft implementation of rpc execute * omit true predicates in output * turn execute/step test into execute/zero-steps to make it pass * prettypretty * Add internal server error to error codes list * rename state->term in ExecuteState record * represent substitutions as #And( #Equals , ..) * fix comment: left-fold not right-fold
1 parent e936e5b commit bc49fae

File tree

13 files changed

+389
-102
lines changed

13 files changed

+389
-102
lines changed

‎docs/2022-07-18-JSON-RPC-Server-API.md‎

Lines changed: 88 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess
2323
"id": 1,
2424
"method": "execute",
2525
"params": {
26-
"max-depth": 1,
26+
"max-depth": 4,
2727
"cut-point-rules": ["rule1"],
2828
"terminal-rules": ["ruleFoo"],
2929
"state": {
@@ -87,52 +87,106 @@ If the verification of the `state` pattern fails, the following error is returne
8787

8888
### Correct Response:
8989

90+
All correct responses have a result containing a `reason`, with one of the following values:
91+
* `"reason: "branching"`
92+
* `"reason: "stuck"`
93+
* `"reason: "depth-bound"`
94+
* `"reason: "cut-point-rule"`
95+
* `"reason: "terminal-rule"`
96+
97+
A field `state` contains the state reached (including optional `predicate` and `substitution`), a field `depth` indicates the execution depth.
98+
9099
```json
91100
{
92101
"jsonrpc": "2.0",
93102
"id": 1,
94103
"result": {
95-
"states": [
96-
{
97-
"state": {"format":"KORE", "version":1, "term":{}},
98-
"depth": 1
99-
}
100-
],
101-
"reason": "final-state"
104+
"state": {
105+
"term": {"format":"KORE", "version":1, "term":{}},
106+
"predicate": {"format":"KORE", "version":1, "term":{}},
107+
"substitution": {"format":"KORE", "version":1, "term":{}},
108+
},
109+
"depth": 1
110+
"reason": "stuck"
102111
}
103112
}
104113
```
105114

106115
The above will be also be the same for:
107-
* `"reason": "stuck"`
108116
* `"reason": "depth-bound"`
109-
* `"reason": "cut-point-rule"`
110-
* `"reason": "terminal-rule"`
117+
118+
119+
If `"reason": "terminal-rule"`, an additional `rule` field indicates which of the `terminal-rule` labels or IDs led to terminating the execution:
111120

112121
```json
113122
{
114123
"jsonrpc": "2.0",
115124
"id": 1,
116125
"result": {
117-
"states": [
126+
"state": {
127+
"term": {"format":"KORE", "version":1, "term":{}},
128+
"predicate": {"format":"KORE", "version":1, "term":{}},
129+
"substitution": {"format":"KORE", "version":1, "term":{}},
130+
},
131+
"depth": 1,
132+
"reason": "terminal-rule",
133+
"rule": "ruleFoo"
134+
}
135+
}
136+
```
137+
138+
139+
If `"reason": "branching"`, an additional `next-states` field contains all following states of the branch point.
140+
```json
141+
{
142+
"jsonrpc": "2.0",
143+
"id": 1,
144+
"result": {
145+
"state": {
146+
"term": {"format":"KORE", "version":1, "term":{}},
147+
"predicate": {"format":"KORE", "version":1, "term":{}},
148+
"substitution": {"format":"KORE", "version":1, "term":{}},
149+
},
150+
"depth": 2,
151+
"reason": "branching",
152+
"next-states": [
118153
{
119-
"state": {"format": "KORE", "version": 1, "term": {}},
120-
"depth": 5,
121-
"condition": {
122-
"substitution": {"format": "KORE", "version": 1, "term": {}},
123-
"predicate": {"format": "KORE", "version": 1, "term": {}}
124-
}
154+
"term": {"format": "KORE", "version": 1, "term": {}},
155+
"predicate": {"format":"KORE", "version":1, "term":{}},
156+
"substitution": {"format":"KORE", "version":1, "term":{}},
125157
},
126158
{
127-
"state": {"format": "KORE", "version": 1, "term": {}},
128-
"depth": 5,
129-
"condition": {
130-
"substitution": {"format": "KORE", "version": 1, "term": {}},
131-
"predicate": {"format": "KORE", "version": 1, "term": {}}
132-
}
159+
"term": {"format": "KORE", "version": 1, "term": {}},
160+
"predicate": {"format":"KORE", "version":1, "term":{}},
161+
"substitution": {"format":"KORE", "version":1, "term":{}},
162+
}
163+
]
164+
}
165+
}
166+
```
167+
168+
If `"reason": "cut-point-rule"`, the `next-states` field contains the next state (if any) in a list. The `rule` field indicates which rule led to stopping.
169+
170+
```json
171+
{
172+
"jsonrpc": "2.0",
173+
"id": 1,
174+
"result": {
175+
"state": {
176+
"term": {"format":"KORE", "version":1, "term":{}},
177+
"predicate": {"format":"KORE", "version":1, "term":{}},
178+
"substitution": {"format":"KORE", "version":1, "term":{}},
179+
},
180+
"depth": 2,
181+
"reason": "cut-point-rule",
182+
"rule": "rule1",
183+
"next-states": [
184+
{
185+
"term": {"format": "KORE", "version": 1, "term": {}},
186+
"predicate": {"format":"KORE", "version":1, "term":{}},
187+
"substitution": {"format":"KORE", "version":1, "term":{}},
133188
}
134-
],
135-
"reason": "branching"
189+
]
136190
}
137191
}
138192
```
@@ -247,7 +301,7 @@ The server uses the JSON RPC spec way of returning errors. Namely, the returned
247301

248302
```json
249303
{
250-
"jsonrpc": "2.0",
304+
"jsonrpc": "2.0",
251305
"id": 1,
252306
"error": {
253307
"code": -32002,
@@ -261,15 +315,15 @@ The kore-rpc specific error messages will use error codes in the range -32000 to
261315

262316
## -32001 Cancel request unsupported in batch mode
263317

264-
Due tot he way that cancel is implemented, we do not allow a cancel message within batch mode. This message should never occur if batch mode is not used.
318+
Due to the way that cancel is implemented, we do not allow a cancel message within batch mode. This message should never occur if batch mode is not used.
265319

266320
## -32002 Could not verify KORE pattern
267321

268322
This error wraps the internal error thrown when validating the received pattern agains the loaded definition file.
269323

270324
```json
271325
{
272-
"jsonrpc": "2.0",
326+
"jsonrpc": "2.0",
273327
"id": 1,
274328
"error": {
275329
"code": -32002,
@@ -280,4 +334,8 @@ This error wraps the internal error thrown when validating the received pattern
280334
}
281335
}
282336
}
283-
```
337+
```
338+
339+
## -32032 Internal server error
340+
341+
This error indicates an internal problem with the server implementation. Its data is not expected to be processed by a client (other than including it in a bug report).

‎kore/src/Kore/Exec.hs‎

Lines changed: 100 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Expose concrete execution as a library
1010
-}
1111
module Kore.Exec (
1212
exec,
13+
rpcExec,
1314
search,
1415
prove,
1516
proveWithRepl,
@@ -37,6 +38,7 @@ import Control.Monad (
3738
(>=>),
3839
)
3940
import Control.Monad.Trans.Maybe (runMaybeT)
41+
import Data.Bifunctor (second)
4042
import Data.Coerce (
4143
coerce,
4244
)
@@ -289,12 +291,15 @@ exec
289291
execStrategy
290292
(ExecDepth 0, Start $ Pattern.fromTermLike initialTerm)
291293
>>= \case
292-
GraphTraversal.Ended results -> pure results
293-
GraphTraversal.GotStuck n results -> do
294-
when (n == 0 && any (notStuck . snd) results) $
294+
GraphTraversal.Ended results ->
295+
pure results
296+
GraphTraversal.GotStuck _ results ->
297+
pure results
298+
GraphTraversal.Stopped results nexts -> do
299+
when (null nexts) $
295300
forM_ depthLimit warnDepthLimitExceeded
296301
pure results
297-
GraphTraversal.Aborted _ results -> do
302+
GraphTraversal.Aborted results -> do
298303
pure results
299304

300305
let (depths, finalConfigs) = unzip finals
@@ -348,8 +353,8 @@ exec
348353
)
349354
toTransitionResult prior [] =
350355
case snd prior of
351-
Start _ -> GraphTraversal.Stopped [prior]
352-
Rewritten _ -> GraphTraversal.Stopped [prior]
356+
Start _ -> GraphTraversal.Stop prior []
357+
Rewritten _ -> GraphTraversal.Stop prior []
353358
Remaining _ -> GraphTraversal.Stuck prior
354359
Kore.Rewrite.Bottom -> GraphTraversal.Stuck prior
355360
toTransitionResult _prior [next] =
@@ -361,8 +366,95 @@ exec
361366
toTransitionResult prior (s : ss) =
362367
GraphTraversal.Branch prior (s :| ss)
363368

364-
notStuck :: ProgramState a -> Bool
365-
notStuck = isJust . extractProgramState
369+
{- | Version of @kore-exec@ suitable for the JSON RPC server. Cannot
370+
execute across branches, supports a depth limit, returns the raw
371+
traversal result for the RPC server to extract response elements.
372+
373+
TODO modify to implement stopping on given rule IDs/labels
374+
-}
375+
rpcExec ::
376+
Limit Natural ->
377+
-- | The main module
378+
SerializedModule ->
379+
-- | The input pattern
380+
TermLike VariableName ->
381+
SMT
382+
( GraphTraversal.TraversalResult
383+
(ExecDepth, ProgramState (Pattern VariableName))
384+
)
385+
rpcExec
386+
depthLimit
387+
SerializedModule
388+
{ sortGraph
389+
, overloadGraph
390+
, metadataTools
391+
, verifiedModule
392+
, rewrites = Initialized{rewriteRules}
393+
, equations
394+
}
395+
(mkRewritingTerm -> initialTerm) =
396+
evalSimplifier verifiedModule' sortGraph overloadGraph metadataTools equations $
397+
fmap (second $ fmap getRewritingPattern)
398+
<$> GraphTraversal.graphTraversal
399+
Strategy.LeafOrBranching
400+
Strategy.DepthFirst
401+
(Limit 2) -- breadth limit 2 because we never go beyond a branch
402+
transit
403+
Limit.Unlimited
404+
execStrategy
405+
(ExecDepth 0, Start $ Pattern.fromTermLike initialTerm)
406+
where
407+
verifiedModule' =
408+
IndexedModule.mapAliasPatterns
409+
(Builtin.internalize metadataTools)
410+
verifiedModule
411+
412+
execStrategy :: [GraphTraversal.Step Prim]
413+
execStrategy =
414+
Limit.takeWithin depthLimit $
415+
[Begin, Simplify, Rewrite, Simplify] :
416+
repeat [Begin, Rewrite, Simplify]
417+
418+
transit ::
419+
GraphTraversal.TState
420+
Prim
421+
(ExecDepth, ProgramState (Pattern RewritingVariableName)) ->
422+
Simplifier.Simplifier
423+
( GraphTraversal.TransitionResult
424+
( GraphTraversal.TState
425+
Prim
426+
(ExecDepth, ProgramState (Pattern RewritingVariableName))
427+
)
428+
)
429+
transit =
430+
GraphTraversal.simpleTransition
431+
( trackExecDepth . profTransitionRule $
432+
transitionRule (groupRewritesByPriority rewriteRules) All
433+
)
434+
toTransitionResult
435+
436+
-- TODO modify to implement stopping on given rule IDs/labels
437+
toTransitionResult ::
438+
(ExecDepth, ProgramState p) ->
439+
[(ExecDepth, ProgramState p)] ->
440+
( GraphTraversal.TransitionResult
441+
(ExecDepth, ProgramState p)
442+
)
443+
toTransitionResult prior [] =
444+
case snd prior of
445+
Remaining _ -> GraphTraversal.Stuck prior
446+
Kore.Rewrite.Bottom -> GraphTraversal.Stuck prior
447+
-- returns `Final` to signal that no instructions were left.
448+
Start _ -> GraphTraversal.Final prior
449+
Rewritten _ -> GraphTraversal.Final prior
450+
toTransitionResult _prior [next] =
451+
case snd next of
452+
Start _ -> GraphTraversal.Continuing next
453+
Rewritten _ -> GraphTraversal.Continuing next
454+
Remaining _ -> GraphTraversal.Stuck next
455+
Kore.Rewrite.Bottom -> GraphTraversal.Stuck next
456+
toTransitionResult prior (s : ss) =
457+
GraphTraversal.Branch prior (s :| ss)
366458

367459
-- | Modify a 'TransitionRule' to track the depth of the execution graph.
368460
trackExecDepth ::

0 commit comments

Comments
 (0)