Skip to content

Commit

Permalink
Hotfix sortk equality issue (#4074)
Browse files Browse the repository at this point in the history 
Several errors were reported on slack which involve an erroneous
injection `inj{SortK, SortKItem}(_)`.

The reason was within the internalisation of `\equals` by booster:
`equals(A:SortK, B:SortK)` was internalised to `inj{SortK,SortKItem}(A)
~> .K ==K inj{SortK,SortKItem}(B) ~> .K` instead of simply `A ==K B`.

In the investigated case, the problem surfaced when a fallback returned
`#Not (#Equals (_:SortK, _: SortK))`, which then caused a failure when
re-internalising the result to do further execution steps. The added
integration tests do not fully reproduce this crash but cause ill-sorted
output which will be detected if the error is reintroduced.
  • Loading branch information
@jberthold
jberthold authored Nov 22, 2024
1 parent 044df58 commit 74322a5
Show file tree
Hide file tree
Showing 12 changed files with 3,565 additions and 4 deletions.
8 changes: 8 additions & 0 deletions booster/library/Booster/Syntax/Json/Internalise.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -573,6 +573,11 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
else case sortOfTerm v of
Internal.SortInt ->
pure [BoolPred $ Internal.Predicate $ Internal.NotBool $ Internal.EqualsInt (Internal.Var k) v]
Internal.SortK ->
pure
[ BoolPred . Internal.Predicate . Internal.NotBool $
Internal.EqualsK (Internal.Var k) v
]
otherSort ->
pure
[ BoolPred $
Expand Down Expand Up @@ -630,6 +635,9 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
pure [SubstitutionPred x t]
(Internal.SortInt, _, _) ->
pure [BoolPred $ Internal.Predicate $ Internal.EqualsInt a b]
(Internal.SortK, _, _) ->
-- already SortK, so we must not apply the KSeq wrapper pattern
pure [BoolPred $ Internal.Predicate $ Internal.EqualsK a b]
(otherSort, _, _) ->
pure
[ BoolPred $
Expand Down
30 changes: 30 additions & 0 deletions booster/test/rpc-integration/resources/subk.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module SUBK
imports BOOL
imports K-EQUAL

syntax State ::= "ping" [token]
| "pong" [token]
| "peng" [token]

configuration <k> $PGM:State ~> .K </k>
<x> .K </x>

syntax State ::= f ( State ) [function]

syntax K ::= inK ( State) [function, total]

rule f(ping) => ping
rule f(pong) => pong
// f is not total

rule inK(STATE) => STATE ~> .K

rule [ping]: <k> ping => f(pong) ... </k>
<x> X </x>
requires notBool (X ==K inK(ping))

rule [pong]: <k> pong => f(ping) ... </k>
<x> X </x>
requires notBool (X ==K inK(pong))

endmodule
2,284 changes: 2,284 additions & 0 deletions booster/test/rpc-integration/resources/subk.kore
View file

Large diffs are not rendered by default.

13 changes: 13 additions & 0 deletions booster/test/rpc-integration/test-subk/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Tests involving K sequences
---------------------------

The [definition `subk.k`](../resources/subk.k) for these tests rewrites `ping` to `pong` and vice-versa, while checking a second configuration cell to not contain a K sequence with the same state at the head.
In addition, the rewrite rules use a partial identity function on states, such that all rewrites will fall back to kore-rpc.

Interestingly, it is forbidden by `kompile` to use `A ~> .K` as a direct child of `==K`. However, functions that produce this expression are apparently fine.

* `sortk-var-branch.execute`: branches on whether the additional cell contains `ping` or not. If it contains `ping`, the state is stuck.
* `sortk-stuck.execute`: the additional cell is initialised with `pong`. Therefore, the rule `pong => ping` cannot be applied, the result is stuck.
* `sortk-equal.simplify`: simplify request for a predicate involving `==K` on arguments of sort `K`.

* `not-subsort.execute`: expects an error saying that `SortK` is not subsort of `SortKItem`.
0 ...n/test-subsorts/response-not-subsort.json → ...ation/test-subk/response-not-subsort.json
View file
File renamed without changes.
111 changes: 111 additions & 0 deletions booster/test/rpc-integration/test-subk/response-sortk-equal.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"state": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Not",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"arg": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortK",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "EVar",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"name": "STATE1"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
},
"second": {
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"value": "init",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
}
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
}
}
}
}
}
131 changes: 131 additions & 0 deletions booster/test/rpc-integration/test-subk/response-sortk-stuck.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,131 @@
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"reason": "stuck",
"depth": 1,
"state": {
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"value": "pong"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'x'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"value": "pong"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "COUNTER",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
]
}
]
}
}
}
}
}
Loading

0 comments on commit 74322a5

Please sign in to comment.