Skip to content

Commit 2c9ad50

Browse files
geo2ageo2a
committed
Add integration tests from #3960 
1 parent 27ce3ce commit 2c9ad50

35 files changed

+241713
-6500
lines changed

‎booster/test/rpc-integration/resources/3934-smt.kore

+60,439
Large diffs are not rendered by default.

‎booster/test/rpc-integration/resources/issue3764-vacuous-branch.kore

+156,444
Large diffs are not rendered by default.

‎booster/test/rpc-integration/resources/remainder-predicates.k

+169
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
module REMAINDER-PREDICATES
2+
imports INT
3+
imports BOOL
4+
5+
syntax State ::= test1Init()
6+
| test1State1()
7+
| test1State2()
8+
| test1State3()
9+
10+
| test2Init()
11+
| test2State1()
12+
| test2State2()
13+
| test2State3()
14+
15+
| test3Init()
16+
| test3State1()
17+
| test3State2()
18+
| test3State3()
19+
20+
| test4Init()
21+
| test4State1()
22+
| test4State2()
23+
| test4State3()
24+
| test4State4()
25+
26+
| test5Init()
27+
| test5State1()
28+
| test5State2()
29+
| test5State3()
30+
| test5State4()
31+
| test5State5()
32+
33+
| test6Init()
34+
| test6State1()
35+
| test6State2()
36+
| test6State3()
37+
| test6State4()
38+
| test6State5()
39+
40+
configuration <k> $PGM:State ~> .K </k>
41+
<int> 0:Int </int>
42+
43+
////////////////////////////////////////////////////////////////////////////////
44+
/// two rules apply with UNSAT remainder predicate, no further rules apply. //
45+
/// Results in 2 branches. //
46+
////////////////////////////////////////////////////////////////////////////////
47+
rule [test1-init]: <k> test1Init() => test1State1() ... </k>
48+
<int> _ => ?_X </int>
49+
50+
rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
51+
<int> X </int>
52+
requires X >Int 0
53+
54+
rule [test1-1-3]: <k> test1State1() => test1State3() ... </k>
55+
<int> X </int>
56+
requires X <=Int 0
57+
58+
////////////////////////////////////////////////////////////////////////////////
59+
/// two rules apply with SAT remainder predicate, //
60+
/// have to consider the remainder branch where X ==Int 0, //
61+
/// no further rules apply. //
62+
/// Results in 2 branches. //
63+
////////////////////////////////////////////////////////////////////////////////
64+
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
65+
<int> _ => ?_X </int>
66+
67+
rule [test2-1-2]: <k> test2State1() => test2State2() ... </k>
68+
<int> X </int>
69+
requires X >Int 0
70+
71+
rule [test2-1-3]: <k> test2State1() => test2State3() ... </k>
72+
<int> X </int>
73+
requires X <Int 0
74+
75+
////////////////////////////////////////////////////////////////////////////////
76+
/// two rules apply with SAT remainder predicate, //
77+
/// have to consider the remainder branch where X ==Int 0, //
78+
/// but the are no further rules to apply. //
79+
/// Results in 2 branches. //
80+
////////////////////////////////////////////////////////////////////////////////
81+
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
82+
<int> _ => ?_X </int>
83+
84+
rule [test3-1-2]: <k> test3State1() => test3State2() ... </k>
85+
<int> X </int>
86+
requires X >Int 0
87+
88+
rule [test3-1-3]: <k> test3State1() => test3State3() ... </k>
89+
<int> X </int>
90+
requires X <Int 0
91+
92+
////////////////////////////////////////////////////////////////////////////////
93+
/// two hight-priorty rules apply with SAT remainder predicate, //
94+
/// have to consider the remainder branch where X ==Int 0, //
95+
/// one further regular rule applies, //
96+
/// whose requires clause explicitly completes the space. //
97+
/// Results in 3 branches. //
98+
////////////////////////////////////////////////////////////////////////////////
99+
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
100+
<int> _ => ?_X </int>
101+
102+
rule [test4-1-2]: <k> test4State1() => test4State2() ... </k>
103+
<int> X </int>
104+
requires X >Int 0
105+
[priority(49)]
106+
107+
rule [test4-1-3]: <k> test4State1() => test4State3() ... </k>
108+
<int> X </int>
109+
requires X <Int 0
110+
[priority(49)]
111+
112+
rule [test4-1-4]: <k> test4State1() => test4State4() ... </k>
113+
<int> X </int>
114+
requires X ==Int 0
115+
116+
117+
////////////////////////////////////////////////////////////////////////////////
118+
/// two hight-priorty rules apply with SAT remainder predicate, //
119+
/// have to consider the remainder branch where X ==Int 0, //
120+
/// one rule at a lower priority applies unconditionally, which means that //
121+
/// that the remainder is False. Rule test5-1-5 is unreachable. //
122+
/// Results in 3 branches. //
123+
////////////////////////////////////////////////////////////////////////////////
124+
rule [test5-init]: <k> test5Init() => test5State1() ... </k>
125+
<int> _ => ?_X </int>
126+
127+
rule [test5-1-2]: <k> test5State1() => test5State2() ... </k>
128+
<int> X </int>
129+
requires X >Int 0 [priority(48)]
130+
131+
rule [test5-1-3]: <k> test5State1() => test5State3() ... </k>
132+
<int> X </int>
133+
requires X <Int 0 [priority(48)]
134+
135+
rule [test5-1-4]: <k> test5State1() => test5State4() ... </k>
136+
[priority(49)]
137+
138+
rule [test5-1-5]: <k> test5State1() => test5State5() ... </k>
139+
<int> X </int>
140+
requires X ==Int 0
141+
142+
////////////////////////////////////////////////////////////////////////////////
143+
/// two hight-priorty rules apply with SAT remainder predicate, //
144+
/// have to consider the remainder branch where X ==Int 0, //
145+
/// two rule at a lower priority applies unconditionally. //
146+
/// Results in 4 branches. //
147+
////////////////////////////////////////////////////////////////////////////////
148+
rule [test6-init]: <k> test6Init() => test6State1() ... </k>
149+
<int> _ => ?_X </int>
150+
151+
rule [test6-1-2]: <k> test6State1() => test6State2() ... </k>
152+
<int> X </int>
153+
requires X >Int 0 [priority(48)]
154+
155+
rule [test6-1-3]: <k> test6State1() => test6State3() ... </k>
156+
<int> X </int>
157+
requires X <Int 0 [priority(48)]
158+
159+
rule [test6-1-4]: <k> test6State1() => test6State4() ... </k>
160+
[priority(49)]
161+
162+
rule [test6-1-5]: <k> test6State1() => test6State5() ... </k>
163+
[priority(49)]
164+
165+
// to produce input state:
166+
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
167+
// then edit state-test1Init.json to substitute test1State1() for test1Init()
168+
169+
endmodule

‎booster/test/rpc-integration/resources/remainder-predicates.kompile

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
echo "kompiling remainder-predicates.k"
2+
kompile --backend haskell remainder-predicates.k
3+
cp remainder-predicates-kompiled/definition.kore remainder-predicates.kore
4+
rm -r remainder-predicates-kompiled

‎booster/test/rpc-integration/resources/use-path-condition-in-equations.k

+57-5
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,29 @@ module USE-PATH-CONDITION-IN-EQUATIONS
1010
| test2State1()
1111
| test2State2()
1212

13+
| test3Init()
14+
| test3State1()
15+
| test3State2()
16+
17+
| test4Init()
18+
| test4State1()
19+
| test4State2()
20+
| test4State3()
21+
1322
syntax Int ::= test1F ( Int ) [function, total, no-evaluators]
1423
| test2F ( Int ) [function, total, no-evaluators]
24+
| test3F ( Int ) [function, total]
25+
| test4F ( Int ) [function, total]
1526

1627
configuration <k> $PGM:State ~> .K </k>
1728
<int> 0:Int </int>
1829

1930
////////////////////////////////////////////////////////////////////////////////
2031
// Here the simplification's side condition is syntactically present //
21-
// in the path condition and is not checked. //
22-
// Result: Stuck at depth 2 in state test1State2() //
23-
// after applying rules test1-init,test1-1-2 //
32+
// in the path condition and is not checked. //
33+
// Result //
34+
// Stuck at depth 2 in state test1State2() //
35+
// after applying rules test1-init,test1-1-2 //
2436
////////////////////////////////////////////////////////////////////////////////
2537
rule [test1-init]: <k> test1Init() => test1State1() ... </k>
2638
<int> _ => ?X </int>
@@ -33,8 +45,7 @@ module USE-PATH-CONDITION-IN-EQUATIONS
3345
rule [test1F-simplify]: test1F(X:Int) => X requires X ==Int 42 [simplification]
3446

3547
////////////////////////////////////////////////////////////////////////////////
36-
// Here the simplification's side condition is implied by the path condition, //
37-
// but we need an SMT solver to establish that. //
48+
// Here the simplification's side condition is implied by the path condition. //
3849
// Result: Stuck at depth 2 in state test2State2(), //
3950
// after applying rules test2-init, test2-1-2. //
4051
////////////////////////////////////////////////////////////////////////////////
@@ -48,6 +59,47 @@ module USE-PATH-CONDITION-IN-EQUATIONS
4859

4960
rule [test2F-simplify]: test2F(X:Int) => X requires X >Int 0 [simplification]
5061

62+
/////////////////////////////////////////////////////////////////////////////////
63+
// Exactly like test2, but the function now has actual evaluators, rather than //
64+
// a simplification-based semantics. Using the SMT solver Booster determines //
65+
// that the condition of rule test3-1-2 is False. //
66+
// Result kore-rpc-booster: //
67+
// Stuck at depth in state test3State1() //
68+
// after applying rules test3-init . //
69+
/////////////////////////////////////////////////////////////////////////////////
70+
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
71+
<int> _ => ?X </int>
72+
ensures ?X ==Int 42
73+
74+
rule [test3-1-2]: <k> test3State1() => test3State2() ... </k>
75+
<int> X </int>
76+
requires test3F(X) >Int 0
77+
78+
rule [test3F-zero-if-x-positive]: test3F(X:Int) => 0 requires X >Int 0
79+
rule [test3F-one-if-not-x-nonpositive]: test3F(X:Int) => 1 requires X <=Int 0
80+
81+
/////////////////////////////////////////////////////////////////////////////////
82+
// Similar to test3, but now there are two rules. Using the solver, Booster //
83+
// determines that the condition of rule test4-1-2 is False. //
84+
// Result: //
85+
// Stuck at depth 2 in state test2State3() //
86+
/////////////////////////////////////////////////////////////////////////////////
87+
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
88+
<int> _ => ?X </int>
89+
ensures ?X ==Int 42
90+
91+
rule [test4-1-2]: <k> test4State1() => test4State2() ... </k>
92+
<int> X </int>
93+
requires test4F(X) >Int 0
94+
95+
rule [test4-1-3]: <k> test4State1() => test4State3() ... </k>
96+
<int> X </int>
97+
requires test4F(X) <=Int 0
98+
99+
100+
rule [test4F-zero-if-x-positive]: test4F(X:Int) => 0 requires X >Int 0
101+
rule [test4F-one-if-not-x-nonpositive]: test4F(X:Int) => 1 requires X <=Int 0
102+
51103
// to produce input state:
52104
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
53105
// then edit state-test1Init.json to substitute test1State1() for test1Init()

0 commit comments

Comments
 (0)