This document details the API and working of the kore-rpc
, kore-rpc-booster
and booster-dev
executables. Running
kore-rpc <DEFINITION>.kore --module <MODULE> --server-port <PORT>
will parse the <DEFINITION>.kore
file with <MODULE>
as the main module and then launch a JSON RPC server on port <PORT>
.
The server runs over sockets and can be interacted with by sending JSON RPC messages. Note that the server listens over raw sockets and doesn't use a high(er)-level protocol like HTTP. The server sends responses as single line strings, with \n
used as the message delimiter. The server allows for bidirectional communication and once opened, a socket connection can be maintained throughout the session. However, this is not strictly necessary as all the API functions (except for cancel
and add-module
) are pure. Also note that the server uses the id
of the request message as the id
of the response, which allows the client to link responses back to their requests. It is therefore important to always send a unique id
with each request witin the current socket session.
{
"jsonrpc": "2.0",
"id": 1,
"method": "execute",
"params": {
"max-depth": 4,
"assume-state-defined": true,
"cut-point-rules": ["rule1"],
"terminal-rules": ["ruleFoo"],
"moving-average-step-timeout": true,
"step-timeout": 1234,
"module": "MODULE-NAME",
"state": {
"format": "KORE",
"version": 1,
"term": {}
},
"log-successful-rewrites": true,
"log-failed-rewrites": true,
}
}
Optional parameters: max-depth
, cut-point-rules
, terminal-rules
, moving-average-step-timeout
, step-timeout
(timeout is in milliseconds), module
(main module name), assume-state-defined
(description follows) and all the log-*
options, which default to false if unspecified.
If assume-state-defined
is set to true
, the all sub-terms of state
will be assumed to be defined before attempting rewrite rules.
Note: id
can be an int or a string and each message must have a new id
. The response objects have the same id as the message.
The request parameters for simplification logs are deprecated. The servers will not return simplification logs in future.
{
"params": {
"log-successful-simplifications": true,
"log-failed-simplifications": true
}
}
If the message is malformed, e.g. the state is not serialized properly, the server will return
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": {
"max-depth": 1,
"cut-point-rules": ["rule1"],
"terminal-rules": ["ruleFoo"],
"state": {
"format": "KORE",
"version": 1,
"term": {}
}
},
"code": -32602,
"message": "Invalid params"
}
}
If the verification of the state
pattern fails, the following error is returned:
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": [
{
"context": [
"symbol or alias \'Lbl\'-LT-\'generatedTop\'-GT-\'\' (<unknown location>)","symbol or alias \'Lbl\'-LT-\'k\'-GT-\'\' (<unknown location>)","symbol or alias \'kseq\' (<unknown location>)","symbol or alias \'inj\' (<unknown location>)","symbol or alias \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' (<unknown location>)"
],
"error": "Head \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' not defined."
}
],
"code": 2,
"message": "Could not verify pattern"
}
}
All correct responses have a result containing a reason
, with one of the following values:
"reason": "branching"
"reason": "stuck"
"reason": "depth-bound"
"reason": "cut-point-rule"
"reason": "terminal-rule"
"reason": "vacuous"
"reason": "timeout"
"reason": "aborted"
and a field state
which contains the state reached (including optional predicate
and substitution
), as well as a field depth
indicating the execution depth (i.e., number of rewrite steps.
{
"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": 1,
"reason": "stuck",
"logs": []
}
}
The reason
field provides information about why the execution stopped.
Depending on the given reason
, additional fields may be present.
Execution reached a state where no rewrite rule could be applied. This response has no additional fields.
Execution reached the max-depth
bound provided in the request
This response has no additional fields.
Execution was stopped because a rewrite step took longer than the step-timeout
provided in the request (either in absolute time for a single step, or as a moving average value).
This response has no additional fields.
Execution reached a state that the server cannot handle.
The unknown-predicate
field MAY contain a predicate that could not be decided by the server's constraint solver.
{
"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": []
}
}
Execution was about to perform a rewrite with a rule whose label is one of the cut-point-rules
labels/IDs of the request.
An additional rule
field indicates which of the cut-point-rules
labels/IDs led to stopping.
An additional next-states
field contains the next state (which stems from the RHS of this rule) in a singleton list.
{
"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": "cut-point-rule",
"rule": "rule1",
"next-states": [
{
"term": {"format": "KORE", "version": 1, "term": {}},
"predicate": {"format":"KORE", "version":1, "term":{}},
"substitution": {"format":"KORE", "version":1, "term":{}},
}
],
"logs": []
}
}
Execution performed a rewrite with a rule whose label is one of the terminal-rules
labels/IDs of the request.
An additional rule
field indicates which of the terminal-rule
labels or IDs led to terminating the execution:
{
"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": 1,
"reason": "terminal-rule",
"rule": "ruleFoo",
"logs": []
}
}
Execution reached a state where, most likely because of ensured side conditions, the configuration became equivalent to \bottom
.
The state
field contains this last configuration, no additional fields are present.
More than one rewrite rule has applied (possibly because of splitting the state and adding branching conditions)
An additional next-states
field contains all following states of the branch point.
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"reason": "branching",
"depth": 0,
"state": <T><k> a ~> . </k> <val> X </val></T>
"next-states": [
{
"term": <T><k> c ~> . </k> <val> X </val></T>,
"predicate": #Not (X #Equals 0),
"rule-id": "6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d",
"rule-predicate": #Not (X #Equals 0),
"rule-substitution": {...}
},
{
"term": <T><k> b ~> . </k> <val> 0 </val></T>,
"rule-id": "79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b",
"rule-predicate": X #Equals 0,
"substitution": V #Equals X #And X #Equals 0 #And ...
}
]
}
}
(note, in the example above theconfiguation and conditions have been pretty printed for clarity. The actual response would contain a {"format":"KORE", "version":1, "term":{...}}
JSON term.)
- It is possible that some of the
next-states
in abranching
result have not actually taken rewrite steps. If one of the branches is stuck because of the added (branching) side condition,next-states
will also contain this branch, with a term identical to the one instate
and the branching condition added to the priorpredicate
fromterm
.
Rationale: The branching should be indicated to the user. A subsequentexecute
step starting from this stuckstate
will of course immediately reportstuck
. branching
results are preferred tocut-point-rule
andterminal-rule
results. That means, if execution reaches a branch with one of the applying rules having a label/ID fromcut-point-rules
orterminal-rules
, the response will bebranching
.
Rationale: The branching information must be provided, assuming the client will re-execute on each branch.- The
rule-predicate
term is a subterm of thepredicate
response and signals the requires clause predicate that was undecidable and thus caused branching. Note that variables insiderule-predicate
may not always be present in the configuration, as they may have been simplified away. rule-substitution
is the substitution of the internal variables of the rules LHS with terms in the configuration before the rewrite. This data is purely for diagnostic purposes and should not be used for any reasoning as it contains interal variable names from the applied rule. Thesubstitution
field on the other hand is returned when the backend infers a new equality for some of the variables present in the configuration, e.g. when the backend splits on the conditionX == 0
, it addsX == 0
into the substitution field in the response.
If any logging is enabled, the optional logs
field will be returned containing an array of objects of the following structure:
{
"tag": "rewrite",
"origin": "kore-rpc",
"result": {
"tag": "success",
"rule-id": "7aa41f364663373c0dc6613c939af530caa55b28f158986657981ee1d8d93fcb",
}
}
{
"tag": "rewrite",
"origin": "kore-rpc",
"result": {
"tag": "failure",
"rule-id": "f6e4ebb55eec38bc4c83677e31cf2a40a72f5f943b2ea1b613049c92af92125c",
"reason": "..."
}
}
where origin
is one of kore-rpc
, booster
or llvm
. The order of the trace messages in the logs
array is the order the backend attempted and applied the rules and should allow for visualisation/reconstruction of the steps the backend took. The original-term-index
is referencing the JSON KORE format and is 0 indexed. The above traces will be emitted when log-successful-rewrites
and log-failed-rewrites
are set to true respectively. Not all backends may support both message types.
{
"jsonrpc": "2.0",
"id": 1,
"method": "implies",
"params": {
"antecedent": {"format": "KORE", "version": 1, "term": {}},
"consequent": {"format": "KORE", "version": 1, "term": {}},
"module": "MODULE-NAME",
"assume-defined": false
}
}
Optional parameters: module
(main module name), assume-defined
.
The assume-defined
flag defaults to false
. When set to true
, the server uses the new simplified implication check in booster, which makes the assumption that the antecedent and consequent are bot defined, i.e. don't simplify to #Bottom
.
Errors in decoding the antecedent
or consequent
terms are reported similar as for execute.
Other errors are specific to the implication checker and what it supports. These errors are reported as Implication check error
(also see below):
- Currently, terms that do not simplify to a singleton pattern are not supported. Unsupported terms are typically those which have an
\or
at the top level.
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": {
"context": [
"LHS: \\and{SortK{}}( /* term: */ /* D Spa */ \\or{SortK{}}( /* Fl Fn D Sfa */ Configa:SortK{}, /* Spa */ \\not{SortK{}}( /* Fl Fn D Sfa */ Configa:SortK{} ) ), \\and{SortK{}}( /* predicate: */ /* D Sfa */ \\top{SortK{}}(), /* substitution: */ \\top{SortK{}}() ))"
],
"error": "Term does not simplify to a singleton pattern"
}
"code": 4,
"message": "Implication check error"
}
}
- The
antecedent
term must not have free variables that are used as existentials in theconsequent
. - The
consequent
term must not have free variables that are not also free in theantecedent
. - The
antecedent
term must be function-like. antecedent
andconsequent
must have the same sort.
The endpoint simplifies antecedent
and consequent
terms and checks whether the implication holds. The simplified implication is returned (as a KORE term) in field implication
.
If the implication holds, valid
is true
and condition
contains a witness, in the form of a predicate and a substitution which unifies the simplified antecedent and the consequent with existential quantifiers removed. The condition.substitution
will contain a witnessing value for each existentially quantified variable of the RHS.
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"implication": {"format": "KORE", "version": 1, "term": {}},
"valid": true,
"condition": {
"substitution": {"format": "KORE", "version": 1, "term": {}},
"predicate": {"format": "KORE", "version": 1, "term": {}}
},
"logs": []
}
}
If the implication cannot be shown to hold, valid
is false.
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"implication": {"format": "KORE", "version": 1, "term": {}},
"valid": false,
"logs": []
}
}
In some cases, a unifier condition
for the implication can still be provided, although the implication cannot be shown to be true.
The endpoint implements the following specification:
Consequent is ⊥ | Consequent is ⊤ | Consequent is a regular pattern | |
---|---|---|---|
Antecedent is ⊥ | valid = true condition = ⊥ | valid = true condition = ⊥ | valid = true condition = ⊥ |
Antecedent is ⊤ | error: The check implication step expects the antecedent term to be function-like. | error: The check implication step expects the antecedent term to be function-like. | error: The check implication step expects the antecedent term to be function-like. |
Antecedent is a regular pattern | valid = false condition = ⊥ | valid = true condition = ⊤ | see below |
In case both antecedent and consequent are regular configurations without undefined partial function applications or contradictory path conditions, the implies endpoint should implement the following behaviour:
- implication doesn't hold and the two terms do not unify,
indicating that the program configuration can be rewritten further =>
valid = False
andcondition
is omitted - implication doesn't hold and the two terms unify, indicating that the configuration is stuck =>
valid = False
andcondition /= \\bottom
{
"jsonrpc": "2.0",
"id": 1,
"method": "simplify",
"params": {
"state": {"format": "KORE", "version": 1, "term": {}},
"module": "MODULE-NAME",
}
}
Optional parameters: module
(main module name)
Same as for execute
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"state": {"format": "KORE", "version": 1, "term": {}},
"logs": []
}
}
- Allows extending the current rule-set of the RPC server by sending textual KORE definition of a module to the server.
- The server computes the SHA256 hash of the unparsed module string and saves the internalised module under this key, returning this ID in the response
- The optional
name-as-id
parameter allows the user to refer to the module by the name as well as the hashed ID. - The IDs and original names are not disjoint for ease of implementation. the
m
pre-pended to the hash is necessary to make the name a valid kore identifier.
{
"jsonrpc": "2.0",
"id": 1,
"method": "add-module",
"params": {
"module": "module MODULE-NAME endmodule []",
"name-as-id": true
}
}
module
is a module represented in textual KORE format. The module may import modules that have been loaded or added earliername-as-id
is an optional argument which adds the module to the module map under the module name as well as the its ID.
If the textual KORE in module
is syntactically wrong, the response will use the error code
Could not parse pattern
with the parse error in the data
field (also see below).
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": ":21:286: unexpected token TokenIdent \\"hasDomainValues\\"\\n",
"code": 1,
"message": "Could not parse pattern"
}
}
If two dfferent modules with the same name and name-as-id: true
are sent, the second request will fail with a Duplicate module name
error
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": 8,
"message": "Duplicate module name"
}
}
However, if the modules are sent twice with name-as-id: false
or without name-as-id
, the second request will succeed.
THe request will also succeed in case the same module is sent multiple times, irrespective of the value of name-as-id
.
Other errors, for instance, using an unknown sort or symbol, will be reported with the error code
Could not verify pattern
and a more specific error message in the data
field.
Responds with the name of the added module if successful.
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"module": "`m<sha256_of_given_module>"
}
}
The module ID m<sha256_of_given_module>
can now be used in subsequent requests to the server by passing "module": "m<sha256_of_given_module>"
.
A get-model
request aims to find a variable substitution that satisfies all predicates in the provided state
, or else responds that it is not valid. The request may also fail to obtain an answer.
Note that only the predicates in the provided state
are checked.
A predicate in matching logic is a construct that can only evaluate to \top
or \bottom
. Most ML connectives (with the exception of \and
and \or
) constitute predicates.
If the provided state
does not contain any predicates, the endpoint will respond with Unknown
(to avoid misunderstandings).
{
"jsonrpc": "2.0",
"id": 1,
"method": "get-model",
"params": {
"state": {"format": "KORE", "version": 1, "term": {}},
"module": "MODULE-NAME"
}
}
Optional parameters: module
(main module name)
same as for execute
{
"jsonrpc":"2.0",
"id":1,
"result":{
"valid": "Sat",
"substitution": {"format": "KORE", "version": 1, "term": {}}
}
Optional fields: substitution
(filled when valid = is-valid
)
The valid
field can have the following values:
"valid": "Sat"
:
The predicates can be satisfied. The fieldsubstitution
must be present, and provides a substitution that fulfils all predicates in the suppliedstate
. Exception: if the predicates are trivially satisfied without any variable assignments, the trivial (empty)substitution
is omitted."valid": "Unsat"
:
The predicates are known to not be valid. Thesubstitution
field is omitted."valid": "Unknown"
:
The backend was unable to decide whether or not there is a satisfying substitution, or the provided tern did not contain any predicates. Thesubstitution
field is omitted.
{"jsonrpc": "2.0", "method": "cancel"}
none
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": -32000,
"message": "Request cancelled"
}
}
The server uses the JSON RPC spec way of returning errors. Namely, the returned object will be of the form
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": 2,
"message": "Could not verify pattern",
"data": {}
}
}
The kore-rpc specific error messages will use error codes in the range -32000 to -32099 and are listed for individual calls above as well as collected below for convenience.
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.
A catch all when the backend throws an error, e.g. an assertion violation or an IO runtime error.
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).
The backend currently does not support the requested function.
With multiple backends, there might not be full feature parity between the different servers. If the current backend does support the given function but doesnt support some optional parameters, it will throw -32003 Unsupported option
for the given parameter instead of -32601 Not implemented
.
This error wraps the internal error thrown when parsing the received plain text module.
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": ":21:286: unexpected token TokenIdent \\"hasDomainValues\\"\\n",
"code": 1,
"message": "Could not parse pattern"
}
}
This error wraps the internal error thrown when validating the received pattern against the loaded definition file.
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": 2,
"message": "Could not verify pattern",
"data": {
"context": ["\\top (<unknown location>)","sort 'IntSort' (<unknown location>)","(<unknown location>)"],
"error": "Sort 'IntSort' not defined."
}
}
}
This error wraps the internal error thrown when a module with the given name can not be found.
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"data": "MODULE-NAME",
"code": 3,
"message": "Could not find module"
}
}
This error wraps an error message from the internal implication check routine, in case the input data is inconsistent or otherwise unsuitable for the check.
{
"jsonrpc":"2.0",
"id":1,
"error": {
"code": 4,
"message": "Implication check error",
"data": {
"context": [
"/* Sfa */ \\mu{}( Config@A:SortK{}, /* Sfa */ Config@A:SortK{} )"
],
"error": "The check implication step expects the antecedent term to be function-like."
}
}
}
Error returned when the SMT solver crashes or is unable to discharge a goal.
{
"jsonrpc": "2.0",
"id": 1,
"error": {
"code": 5,
"message": "Smt solver error",
"data": {
"term": {
"format": "KORE",
"version": 1,
"term": {}
},
"error": "(incomplete (theory arithmetic))",
}
}
}
The two errors above indicate that the execute endpoint ended up in an erroneous/inconsistent state and the returned error message is should be included in the bug report.
The module could not be parsed or is invalid (e.g. contains new symbols)
A module with the same name is already loaded on the server