Skip to content

Commit 8b5115f

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 820cd05 + 74322a5 commit 8b5115f

12 files changed

+3565
-4
lines changed

‎booster/library/Booster/Syntax/Json/Internalise.hs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -573,6 +573,11 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
573573
else case sortOfTerm v of
574574
Internal.SortInt ->
575575
pure [BoolPred $ Internal.Predicate $ Internal.NotBool $ Internal.EqualsInt (Internal.Var k) v]
576+
Internal.SortK ->
577+
pure
578+
[ BoolPred . Internal.Predicate . Internal.NotBool $
579+
Internal.EqualsK (Internal.Var k) v
580+
]
576581
otherSort ->
577582
pure
578583
[ BoolPred $
@@ -630,6 +635,9 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
630635
pure [SubstitutionPred x t]
631636
(Internal.SortInt, _, _) ->
632637
pure [BoolPred $ Internal.Predicate $ Internal.EqualsInt a b]
638+
(Internal.SortK, _, _) ->
639+
-- already SortK, so we must not apply the KSeq wrapper pattern
640+
pure [BoolPred $ Internal.Predicate $ Internal.EqualsK a b]
633641
(otherSort, _, _) ->
634642
pure
635643
[ BoolPred $

‎booster/test/rpc-integration/resources/subk.k

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module SUBK
2+
imports BOOL
3+
imports K-EQUAL
4+
5+
syntax State ::= "ping" [token]
6+
| "pong" [token]
7+
| "peng" [token]
8+
9+
configuration <k> $PGM:State ~> .K </k>
10+
<x> .K </x>
11+
12+
syntax State ::= f ( State ) [function]
13+
14+
syntax K ::= inK ( State) [function, total]
15+
16+
rule f(ping) => ping
17+
rule f(pong) => pong
18+
// f is not total
19+
20+
rule inK(STATE) => STATE ~> .K
21+
22+
rule [ping]: <k> ping => f(pong) ... </k>
23+
<x> X </x>
24+
requires notBool (X ==K inK(ping))
25+
26+
rule [pong]: <k> pong => f(ping) ... </k>
27+
<x> X </x>
28+
requires notBool (X ==K inK(pong))
29+
30+
endmodule

‎booster/test/rpc-integration/resources/subk.kore

Lines changed: 2284 additions & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-subk/README.md

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
Tests involving K sequences
2+
---------------------------
3+
4+
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.
5+
In addition, the rewrite rules use a partial identity function on states, such that all rewrites will fall back to kore-rpc.
6+
7+
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.
8+
9+
* `sortk-var-branch.execute`: branches on whether the additional cell contains `ping` or not. If it contains `ping`, the state is stuck.
10+
* `sortk-stuck.execute`: the additional cell is initialised with `pong`. Therefore, the rule `pong => ping` cannot be applied, the result is stuck.
11+
* `sortk-equal.simplify`: simplify request for a predicate involving `==K` on arguments of sort `K`.
12+
13+
* `not-subsort.execute`: expects an error saying that `SortK` is not subsort of `SortKItem`.

‎booster/test/rpc-integration/test-subsorts/response-not-subsort.json renamed to ‎booster/test/rpc-integration/test-subk/response-not-subsort.json

File renamed without changes.

‎booster/test/rpc-integration/test-subk/response-sortk-equal.json

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"state": {
6+
"format": "KORE",
7+
"version": 1,
8+
"term": {
9+
"tag": "Not",
10+
"sort": {
11+
"tag": "SortApp",
12+
"name": "SortGeneratedTopCell",
13+
"args": []
14+
},
15+
"arg": {
16+
"tag": "Equals",
17+
"argSort": {
18+
"tag": "SortApp",
19+
"name": "SortK",
20+
"args": []
21+
},
22+
"sort": {
23+
"tag": "SortApp",
24+
"name": "SortGeneratedTopCell",
25+
"args": []
26+
},
27+
"first": {
28+
"tag": "App",
29+
"name": "kseq",
30+
"sorts": [],
31+
"args": [
32+
{
33+
"tag": "App",
34+
"name": "inj",
35+
"sorts": [
36+
{
37+
"tag": "SortApp",
38+
"name": "SortState",
39+
"args": []
40+
},
41+
{
42+
"tag": "SortApp",
43+
"name": "SortKItem",
44+
"args": []
45+
}
46+
],
47+
"args": [
48+
{
49+
"tag": "EVar",
50+
"sort": {
51+
"tag": "SortApp",
52+
"name": "SortState",
53+
"args": []
54+
},
55+
"name": "STATE1"
56+
}
57+
]
58+
},
59+
{
60+
"tag": "App",
61+
"name": "dotk",
62+
"sorts": [],
63+
"args": []
64+
}
65+
]
66+
},
67+
"second": {
68+
"tag": "App",
69+
"name": "kseq",
70+
"sorts": [],
71+
"args": [
72+
{
73+
"tag": "App",
74+
"name": "inj",
75+
"sorts": [
76+
{
77+
"tag": "SortApp",
78+
"name": "SortState",
79+
"args": []
80+
},
81+
{
82+
"tag": "SortApp",
83+
"name": "SortKItem",
84+
"args": []
85+
}
86+
],
87+
"args": [
88+
{
89+
"tag": "DV",
90+
"value": "init",
91+
"sort": {
92+
"tag": "SortApp",
93+
"name": "SortState",
94+
"args": []
95+
}
96+
}
97+
]
98+
},
99+
{
100+
"tag": "App",
101+
"name": "dotk",
102+
"sorts": [],
103+
"args": []
104+
}
105+
]
106+
}
107+
}
108+
}
109+
}
110+
}
111+
}

‎booster/test/rpc-integration/test-subk/response-sortk-stuck.json

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "stuck",
6+
"depth": 1,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "App",
13+
"name": "Lbl'-LT-'generatedTop'-GT-'",
14+
"sorts": [],
15+
"args": [
16+
{
17+
"tag": "App",
18+
"name": "Lbl'-LT-'k'-GT-'",
19+
"sorts": [],
20+
"args": [
21+
{
22+
"tag": "App",
23+
"name": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "inj",
29+
"sorts": [
30+
{
31+
"tag": "SortApp",
32+
"name": "SortState",
33+
"args": []
34+
},
35+
{
36+
"tag": "SortApp",
37+
"name": "SortKItem",
38+
"args": []
39+
}
40+
],
41+
"args": [
42+
{
43+
"tag": "DV",
44+
"sort": {
45+
"tag": "SortApp",
46+
"name": "SortState",
47+
"args": []
48+
},
49+
"value": "pong"
50+
}
51+
]
52+
},
53+
{
54+
"tag": "App",
55+
"name": "dotk",
56+
"sorts": [],
57+
"args": []
58+
}
59+
]
60+
}
61+
]
62+
},
63+
{
64+
"tag": "App",
65+
"name": "Lbl'-LT-'x'-GT-'",
66+
"sorts": [],
67+
"args": [
68+
{
69+
"tag": "App",
70+
"name": "kseq",
71+
"sorts": [],
72+
"args": [
73+
{
74+
"tag": "App",
75+
"name": "inj",
76+
"sorts": [
77+
{
78+
"tag": "SortApp",
79+
"name": "SortState",
80+
"args": []
81+
},
82+
{
83+
"tag": "SortApp",
84+
"name": "SortKItem",
85+
"args": []
86+
}
87+
],
88+
"args": [
89+
{
90+
"tag": "DV",
91+
"sort": {
92+
"tag": "SortApp",
93+
"name": "SortState",
94+
"args": []
95+
},
96+
"value": "pong"
97+
}
98+
]
99+
},
100+
{
101+
"tag": "App",
102+
"name": "dotk",
103+
"sorts": [],
104+
"args": []
105+
}
106+
]
107+
}
108+
]
109+
},
110+
{
111+
"tag": "App",
112+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
113+
"sorts": [],
114+
"args": [
115+
{
116+
"tag": "EVar",
117+
"name": "COUNTER",
118+
"sort": {
119+
"tag": "SortApp",
120+
"name": "SortInt",
121+
"args": []
122+
}
123+
}
124+
]
125+
}
126+
]
127+
}
128+
}
129+
}
130+
}
131+
}

0 commit comments

Comments
 (0)