JSON-RPC for driving symbolic execution

[goodlyrottenapple]

This is a proposal to switch to using the JSON RPC protocol to talk with kore-repl/kore-exec. The main proposed change would be to remove the current REPL and replace it with a JSON RPC server which would handle the "core" functionality of the current REPL, namely all the functionality such as step/stepf, config, select, etc. excluding any complex commands like piping or appending to file, which would instead be delegated to a new REPL. This new REPL could be written in Haskell or any potentially any other language, e.g. Python, and would simply be a JSON RPC client together with the REPL parser pretty printer, etc. This REPL could potentially live in the K framework repo and thus have better access to higher level functionality such as the pretty printing of kore ASTs back into K (since config in the current REPL returns a kore AST). A potential advantage of this approach is a common interface for both a REPL and the summarizer to interact with the haskell backend.

Propsed features

• new REPL should mirror the current REPL functionality
• have built in pretty printing of K terms (discussed in #1890, #2797)
• should be interruptible/cancellable #1691
• have state diffing built in

Questions

• What language to use for the new REPL and which repo to put it in?
• Could the LLVM backend also have a JSON RPC interface? Would this make sense?

Edit: 12 July 2022

We met and discussed that we need the following:

• [x] #3143
• [x] #3144
• [x] #3148
• [x] #3146

The step request will just be a particular case of the execute request. The execute request will also return the branching states etc. together with the parent node of the branch.

The check-implication request can just expose the current check implication procedure we have, with some minimal changes.

[goodlyrottenapple]

Implementation details

We could use servant-jsonrpc to pull out the current functionality of the REPL into the following API

type Step   = JsonRpc "step"   Int Text [Int] 

The Step method expects an Int argument and either returns a Text error or a list of new states in case of branching. Maybe instead of [Int] we should return a hash of the state as it appears in the summarizer?? Or return both?

type Stepf  = JsonRpc "stepf"  Int Text [Int] 
type Select = JsonRpc "select" Int Text ()

Should Select take the hash instead? Or maybe have two selects, one with an int and the other with a hash?

type Config = JsonRpc "config" Int Text Text

Not sure whether Config should return a structured type or just dump the kore state as text.

type Cancel = JsonRpcNotification "cancel" ()

Should cancel the current operation, most likely to be used with Step(f)

type RpcAPI = Step :<|> Stepf :<|> Select :<|> Config :<|> Cancel

This RPC server would essentially be the same stateful interpreter that we currently have, as we want to avoid the startup cost of reloading the current file for each individual command, as is currently the case for the KSummarizer. However, since we want to add a cancel operation, we would probably? have to tweak the code to be able to handle the Cancel. Probably best to implement the server to run two threads, the worker thread that does one computation at a time and the server thread that buffers the messages and sends back responses.

[goodlyrottenapple]

Actually I found a different library https://hackage.haskell.org/package/json-rpc-1.0.4/docs/Network-JSONRPC.html which may be more suited if we want to support bi-directional communication, e.g. when having debugging enabled. The servant-jsonrpc library assumes a client-server architecture, where the client always initiates a request and then waits for the response. However, we might want to add an RPC function to e.g. enable debugging or tracing information. Then, instead of the client waiting on a response to an "enable debugging info" message, the server should instead start sending individual debug messages to the client whenever the execution of e.g. step calls for it. This would change the server into a sort of pub-sub configuration rather than a straightforward client-server. I believe the json-rpc library mentioned above supports both models.... @ana-pantilie @ehildenb is this something you can see we might want to support?

[goodlyrottenapple]

Here is the proposed API implementation agnostic view:

Messages from client to the kore-exec JSON RPC server

Method name	Parameters	Return type	Message type	Notes
step	Int	[Int]	regular	The step method expects an Int argument and either returns a Text error or a list of new states in case of branching. Maybe instead of [Int] we should return a [Hash] of the states as they appear in the summarizer?? Or return both?
stepf	Int	[Int]	regular
select	Int	()	regular	Should Select take the hash instead? Or maybe have two selects, one with an int and the other with a hash?
config	Int	Text	regular	Not sure whether Config should return a structured type or just dump the kore state as text.
cancel			notification	Should cancel the current operation, most likely to be used with step(f)
log_subscribe	[Text]	()	regular (pub-sub)	Subscribe to the log messages passed in via the parameter, e.g. ["DebugAttemptEquation", "DebugApplyEquation"]. Should return an empty response on success or a Text error if e.g. no such message type exists.
log_unsubscribe	[Text]		regular (pub-sub)	opposite of log_subscribe

Messages from the kore-exec JSON RPC server to the client

Method name	Parameters	Return type	Message type	Notes
log_message	LogType		notification	LogType should look something like {"type": "DebugAttemptEquation", "message": "..." }

Message type explanation

Message type	Description
regular	Regular JSON RPC request message, where the client should expect a response. See https://www.jsonrpc.org/specification#request_object
notification	JSON RPC notification message, where the receiver does not send a response back. See https://www.jsonrpc.org/specification#request_object
pub-sub	A regular or notification JSON RPC message from the subscriber to the publisher, which may result in the publisher sending notification messages back to the subscriber. E.g. see https://geth.ethereum.org/docs/rpc/pubsub

[ehildenb]

Messages the backend can receive:

Execute

"state": KORE_TERM
"action": "execute"
OPTIONAL: "max-depth": DEPTH
OPTIONAL: "halt-patterns": [KORE_HALT_PATTERN ...]

This should execute until either (i) a branch is hit, (ii) the entire term gets stuck, (iii) the max-depth bound is reached, or (iv) one of the halt-patterns matches. If halt-patterns are not supplied, they should not be checked.

The response should be:

"state": KORE_TERM
"reason": REASON_FOR_HALTING

Where KORE_TERM is the final term, and REASON_FOR_HALTING is one of:

{ "reason": "branching", "depth": DEPTH }
{ "reason": "stuck", "depth": DEPTH }
{ "reason": "depth-bound" }
{ "reason": "pattern-match", "depth": DEPTH, "matches": [ { "pattern": INT_INDEX_OF_PATTERN_THAT_MATCHED, "substitution": MATCHING_SUBSTITUTION } ] }

One step symbolic execution

"state": KORE_TERM
"action": "step"

Response should be:

"states": [ {"state": KORE_TERM, "depth": DEPTH, "condition": NEW_PATH_CONDITION_ALONG_THAT_EXECUTION } ... ]

Where it is expected that DEPTH will be either 0 or 1. 0 will correspond to stuck turns, 1 to terms that could take a step. If no branching occurs, it should return a singleton with NEW_PATH_CONDITIONAL_ALNG_THAT_EXECUTION being #Top. If part of the term gets stuck (like a remainder that doesn't make any more progress), then DEPTH==0 and NEW_PATH_CONDITION_ALONG_THAT_EXECUTION should be the remainder that it got stuck with.

Implication Checking

"antecedent": KORE_TERM
"consequent": KORE_TERM

Result:

"satisfiable": true/false
OPTIONAL: "substitution": MATCHING_SUBSTITUTION

If implifiaction checking results in #Bottom, no need for a substitution. If it does not, we need the substitution which causes matching to work.

Term Simplification

"state": KORE_TERM

Result:

"state": KORE_TERM_SIMPLIFIED

[ehildenb]

rule <k> X:Int => a ... </k> requires X <Int 3

call: {"step": "<k> Y:Int </k>"}
result: [
{ term: "<k> Y </k>", "condition": "notBool X <Int 3", "depth": 0 },
{ term: "<k> a </k>", "condition": "X <Int 3", "depth": 1 }
]

[ehildenb]

Let's make the architecture so that there is one main server thread which accepts/sends requests. Add a cancel command which can cancel a given command running.

[ehildenb]

Let's make sure that each call which triggers simplification (simplify, step, execute-to-branch) can optionally take a list of axioms (semantic rules with some specific priority) and simplification lemmas (simplification rules).

[ehildenb]

Let's allow specifying a list of patterns to execute-to-branch which will be checked every step of execution. If the one of the patterns matches the current term, then halt execution and return the current state. If no pattern is supplied, it should be no efficiency difference from original implementation.

We also change the return of execute-to-branch to have a reason instead of a boolean branching. The reason will be one of stuck, branching, pattern-match(N) (where N is the index of the pattern that matched).

[ana-pantilie]

Preliminaries

Semantic rule/rewrite rule:

• in K rule <k> A => B ... </k> <otherCell> C => D </otherCell> ....., rules which when applied actually do semantic steps
• in Kore\\rewrites(LHS, RHS), in Matching Logic ∀x.φ → •∃z.ψ
• Haskell representation: https://github.com/runtimeverification/haskell-backend/blob/b06757e252ee01fdd5ab8f07de2910711997d845/kore/src/Kore/Rewrite/RulePattern.hs#L194

Function rules (function definition rules and simplification rules):

• in K, rule funcSymbol(...) => _, funcSymbol will have the [function] attribute in its syntax declaration; if you add [simplification] to the rule declaration it becomes a simplification rule; by default it's a function definition
• in Kore, \\implies(requires, \\equals(LHS, RHS)), that's why we call them equations
• Haskell rep: https://github.com/runtimeverification/haskell-backend/blob/b06757e252ee01fdd5ab8f07de2910711997d845/kore/src/Kore/Equation/Equation.hs#L121

Server start-up

The configuration looks like:

data KoreRpcServerOptions =
   KoreRpcServerOptions
       { definitionFileName :: FilePath
        , mainModuleName :: ModuleName
        , koreSolverOptions :: KoreSolverOptions
        , koreLogOptions :: KoreLogOptions
        , version :: _
       }

Start-up will load and initialize the definition, meaning it will basically do the same thing as https://github.com/runtimeverification/haskell-backend/blob/22b637981b4b5ff86963fe9fbc8322e7b65b26ed/kore/app/exec/Main.hs#L662 until line 665. This only does syntactical validation of the kore definition but it doesn't internalize the definition. Our first blocker is that we run the simplifier initialization as part of the action which actually executes the Kore pattern, so that needs to be separated and stored some way globally in order for the worker thread to have access to it each time it reads a request.

[ana-pantilie]

Next steps:

• review https://github.com/runtimeverification/haskell-backend/pull/3068
• see if it's possible to restrict to one session
• initialize server by spawning SMT process and initializing and internalizing the definition, basically doing everything up until https://github.com/runtimeverification/haskell-backend/blob/dea085939a1c1005fb3216f7e7a0890c3e34a3a6/kore/app/exec/Main.hs#L695 and using the simplifier init function from above PR

[goodlyrottenapple]

from @nishantjr:

We noticed while looking at the logs, that when executing up to a branch point, the backend may be calculating the states immediately after the branch point as well. If that's the case, could the JSON RPC also return those states? We'd like to change the result of the execute action from:

"state": KORE_TERM
"reason": REASON_FOR_HALTING

Where KORE_TERM is the final term, and REASON_FOR_HALTING is one of:

{ "reason": "branching", "depth": DEPTH }
{ "reason": "stuck", "depth": DEPTH }
{ "reason": "depth-bound" }
{ "reason": "pattern-match", "depth": DEPTH, "matches": [ { "pattern": INT_INDEX_OF_PATTERN_THAT_MATCHED, "substitution": MATCHING_SUBSTITUTION } ] }

to:

"state": KORE_TERM
"reason": REASON_FOR_HALTING

Where KORE_TERM is the final term, and REASON_FOR_HALTING is one of:

{ "reason": "branching", "depth": DEPTH, "post-branch-states": [ { "state": POST_BRANCH_STATE, "depth": POST_BRANCH_DEPTH, ...]}
{ "reason": "stuck", "depth": DEPTH }
{ "reason": "depth-bound" }
{ "reason": "pattern-match", "depth": DEPTH, "matches": [ { "pattern": INT_INDEX_OF_PATTERN_THAT_MATCHED, "substitution": MATCHING_SUBSTITUTION } ] }

[ehildenb]

No need for frontend or LLVM backend support here, we already have good textual/binary format for frontend/backend talknig to each other.

Maybe later we need it, and we can add it then. Currently we only need pyk/haskell-backend to talk to each other.

[ehildenb]

We actually don't need support for patterns in execute-to-branch anymore, instead we can support cut-point-rules and terminal-rules.

cut-point-rules is a set of string rule labels/identifiers (like rule [my-rule-name]: ....), which if one of these rules applies, we want the state before the rule applied to be returned. terminal-rules is a set of string rule labels/identifiers (like rule [my-rule-name]: ...) which if one of these rules applies, we want the state after the rule applied to be returned.

[ana-pantilie]

We met and discussed that we need the following:

• [ ] New minimized executor
• [ ] New minimized simplifier

The check-implication request can just expose the current check implication procedure we have, with some minimal changes.

[radumereuta]

Prioritize merging an API. We can do refactoring later. We should unblock other teams first.

[ana-pantilie]

Meeting discussion with @goodlyrottenapple:

• check implication should return true/false and an optional substitution and predicate
• return dummy responses for each command
• prioritize wrapping up the API
• write docs for API, add to PR

Future work:

• https://github.com/runtimeverification/haskell-backend/issues/3148 is highest priority after getting the API merged
• discuss with Pyk team about giving us examples

[ana-pantilie]

@goodlyrottenapple just export types from the Kore JSON module.

[ana-pantilie]

Next step as of today: additional testing, and look at check-implication. @ana-pantilie please ask what is needed for this end-point.