Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Jul 30, 2024
2 parents 2dc34ac + e5a921f commit 97f8612
Show file tree
Hide file tree
Showing 50 changed files with 97,685 additions and 2 deletions.
2 changes: 1 addition & 1 deletion booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -495,7 +495,7 @@ respond stateVar request =
(Right newPreds, _) ->
if all (== Pattern.Predicate TrueBool) newPreds
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)

Expand Down
73,985 changes: 73,985 additions & 0 deletions booster/test/rpc-integration/resources/implies-issue-3941.kore
View file

Large diffs are not rendered by default.

2,685 changes: 2,685 additions & 0 deletions booster/test/rpc-integration/resources/implies.kore
View file

Large diffs are not rendered by default.

5,381 changes: 5,381 additions & 0 deletions booster/test/rpc-integration/resources/implies2.kore
View file

Large diffs are not rendered by default.

11 changes: 11 additions & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"jsonrpc": "2.0",
"id": 61298,
"error": {
"code": 4,
"data": {
"error": "match remainder: Map:update(VarS:SortMap{}, \"0\", \"0\") == Map:update(\n VarS:SortMap{},\n \"0\",\n chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))\n), \"\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL...truncated\" == buf(\n \"32\",\n chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))\n)"
},
"message": "Implication check error"
}
}
7,065 changes: 7,065 additions & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/response-001.json
View file

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/state-001.send
View file

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-0->1.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc":"2.0","id":"4420705104-001","result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}}
25 changes: 25 additions & 0 deletions booster/test/rpc-integration/test-implies/response-0->T.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"jsonrpc": "2.0",
"id": "4420703856-001",
"error": {
"code": 2,
"data": [
{
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
},
"error": "Pattern must contain at least one term"
}
],
"message": "Could not verify pattern"
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-0->T.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc":"2.0","id":"4420703856-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}}
11 changes: 11 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->0.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"jsonrpc": "2.0",
"id": "4420567456-001",
"error": {
"code": 4,
"data": {
"error": "match remainder: \"0\" == x:SortInt{}"
},
"message": "Implication check error"
}
}
86 changes: 86 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->0.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
{
"jsonrpc": "2.0",
"id": "4420567456-001",
"result": {
"valid": false,
"implication": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Implies",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"condition": {
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
}
}
}
25 changes: 25 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->T.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"jsonrpc": "2.0",
"id": "4420498928-001",
"error": {
"code": 2,
"data": [
{
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
},
"error": "Pattern must contain at least one term"
}
],
"message": "Could not verify pattern"
}
}
62 changes: 62 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->T.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
{
"jsonrpc": "2.0",
"id": "4420498928-001",
"result": {
"valid": true,
"implication": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Implies",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "X",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
},
"condition": {
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
}
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-X->X.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc":"2.0","id":"4420580224-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-fail-0->X.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc":"2.0","id":"4420705104-001","result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}}
96 changes: 96 additions & 0 deletions booster/test/rpc-integration/test-implies/response-fail-X->Y.booster-dev
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
{
"jsonrpc": "2.0",
"id": "4420575472-001",
"result": {
"valid": true,
"implication": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Implies",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "EVar",
"name": "y",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
},
"condition": {
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "y",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
]
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
}
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-fail-X->Y.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc":"2.0","id":"4420575472-001","error":{"code":4,"data":{"context":["LHS: Configx:SortInt{}","RHS: Configy:SortInt{}","existentials: []"],"error":"The RHS must not have free variables not present in the LHS: Configy"},"message":"Implication check error"}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-0->1.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420705104-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-0->T.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420703856-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "Top", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->0.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420567456-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->T.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420498928-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "X", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "Top", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->X.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420580224-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-fail-0->X.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420705104-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-fail-X->Y.send
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"jsonrpc": "2.0", "id": "4420575472-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "y", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}
Loading

0 comments on commit 97f8612

Please sign in to comment.