Skip to content

Commit

Permalink
Add integration tests from #3960
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Oct 17, 2024
1 parent ad8a7ff commit 1987f36
Show file tree
Hide file tree
Showing 35 changed files with 241,713 additions and 6,500 deletions.
60,439 changes: 60,439 additions & 0 deletions booster/test/rpc-integration/resources/3934-smt.kore
View file

Large diffs are not rendered by default.

156,444 changes: 156,444 additions & 0 deletions booster/test/rpc-integration/resources/issue3764-vacuous-branch.kore
View file

Large diffs are not rendered by default.

169 changes: 169 additions & 0 deletions booster/test/rpc-integration/resources/remainder-predicates.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,169 @@
module REMAINDER-PREDICATES
imports INT
imports BOOL

syntax State ::= test1Init()
| test1State1()
| test1State2()
| test1State3()

| test2Init()
| test2State1()
| test2State2()
| test2State3()

| test3Init()
| test3State1()
| test3State2()
| test3State3()

| test4Init()
| test4State1()
| test4State2()
| test4State3()
| test4State4()

| test5Init()
| test5State1()
| test5State2()
| test5State3()
| test5State4()
| test5State5()

| test6Init()
| test6State1()
| test6State2()
| test6State3()
| test6State4()
| test6State5()

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

////////////////////////////////////////////////////////////////////////////////
/// two rules apply with UNSAT remainder predicate, no further rules apply. //
/// Results in 2 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test1-init]: <k> test1Init() => test1State1() ... </k>
<int> _ => ?_X </int>

rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
<int> X </int>
requires X >Int 0

rule [test1-1-3]: <k> test1State1() => test1State3() ... </k>
<int> X </int>
requires X <=Int 0

////////////////////////////////////////////////////////////////////////////////
/// two rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// no further rules apply. //
/// Results in 2 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
<int> _ => ?_X </int>

rule [test2-1-2]: <k> test2State1() => test2State2() ... </k>
<int> X </int>
requires X >Int 0

rule [test2-1-3]: <k> test2State1() => test2State3() ... </k>
<int> X </int>
requires X <Int 0

////////////////////////////////////////////////////////////////////////////////
/// two rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// but the are no further rules to apply. //
/// Results in 2 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
<int> _ => ?_X </int>

rule [test3-1-2]: <k> test3State1() => test3State2() ... </k>
<int> X </int>
requires X >Int 0

rule [test3-1-3]: <k> test3State1() => test3State3() ... </k>
<int> X </int>
requires X <Int 0

////////////////////////////////////////////////////////////////////////////////
/// two hight-priorty rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// one further regular rule applies, //
/// whose requires clause explicitly completes the space. //
/// Results in 3 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
<int> _ => ?_X </int>

rule [test4-1-2]: <k> test4State1() => test4State2() ... </k>
<int> X </int>
requires X >Int 0
[priority(49)]

rule [test4-1-3]: <k> test4State1() => test4State3() ... </k>
<int> X </int>
requires X <Int 0
[priority(49)]

rule [test4-1-4]: <k> test4State1() => test4State4() ... </k>
<int> X </int>
requires X ==Int 0


////////////////////////////////////////////////////////////////////////////////
/// two hight-priorty rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// one rule at a lower priority applies unconditionally, which means that //
/// that the remainder is False. Rule test5-1-5 is unreachable. //
/// Results in 3 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test5-init]: <k> test5Init() => test5State1() ... </k>
<int> _ => ?_X </int>

rule [test5-1-2]: <k> test5State1() => test5State2() ... </k>
<int> X </int>
requires X >Int 0 [priority(48)]

rule [test5-1-3]: <k> test5State1() => test5State3() ... </k>
<int> X </int>
requires X <Int 0 [priority(48)]

rule [test5-1-4]: <k> test5State1() => test5State4() ... </k>
[priority(49)]

rule [test5-1-5]: <k> test5State1() => test5State5() ... </k>
<int> X </int>
requires X ==Int 0

////////////////////////////////////////////////////////////////////////////////
/// two hight-priorty rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// two rule at a lower priority applies unconditionally. //
/// Results in 4 branches. //
////////////////////////////////////////////////////////////////////////////////
rule [test6-init]: <k> test6Init() => test6State1() ... </k>
<int> _ => ?_X </int>

rule [test6-1-2]: <k> test6State1() => test6State2() ... </k>
<int> X </int>
requires X >Int 0 [priority(48)]

rule [test6-1-3]: <k> test6State1() => test6State3() ... </k>
<int> X </int>
requires X <Int 0 [priority(48)]

rule [test6-1-4]: <k> test6State1() => test6State4() ... </k>
[priority(49)]

rule [test6-1-5]: <k> test6State1() => test6State5() ... </k>
[priority(49)]

// to produce input state:
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
// then edit state-test1Init.json to substitute test1State1() for test1Init()

endmodule
4 changes: 4 additions & 0 deletions booster/test/rpc-integration/resources/remainder-predicates.kompile
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
echo "kompiling remainder-predicates.k"
kompile --backend haskell remainder-predicates.k
cp remainder-predicates-kompiled/definition.kore remainder-predicates.kore
rm -r remainder-predicates-kompiled
62 changes: 57 additions & 5 deletions booster/test/rpc-integration/resources/use-path-condition-in-equations.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,17 +10,29 @@ module USE-PATH-CONDITION-IN-EQUATIONS
| test2State1()
| test2State2()

| test3Init()
| test3State1()
| test3State2()

| test4Init()
| test4State1()
| test4State2()
| test4State3()

syntax Int ::= test1F ( Int ) [function, total, no-evaluators]
| test2F ( Int ) [function, total, no-evaluators]
| test3F ( Int ) [function, total]
| test4F ( Int ) [function, total]

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

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

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

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

/////////////////////////////////////////////////////////////////////////////////
// Exactly like test2, but the function now has actual evaluators, rather than //
// a simplification-based semantics. Using the SMT solver Booster determines //
// that the condition of rule test3-1-2 is False. //
// Result kore-rpc-booster: //
// Stuck at depth in state test3State1() //
// after applying rules test3-init . //
/////////////////////////////////////////////////////////////////////////////////
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
<int> _ => ?X </int>
ensures ?X ==Int 42

rule [test3-1-2]: <k> test3State1() => test3State2() ... </k>
<int> X </int>
requires test3F(X) >Int 0

rule [test3F-zero-if-x-positive]: test3F(X:Int) => 0 requires X >Int 0
rule [test3F-one-if-not-x-nonpositive]: test3F(X:Int) => 1 requires X <=Int 0

/////////////////////////////////////////////////////////////////////////////////
// Similar to test3, but now there are two rules. Using the solver, Booster //
// determines that the condition of rule test4-1-2 is False. //
// Result: //
// Stuck at depth 2 in state test2State3() //
/////////////////////////////////////////////////////////////////////////////////
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
<int> _ => ?X </int>
ensures ?X ==Int 42

rule [test4-1-2]: <k> test4State1() => test4State2() ... </k>
<int> X </int>
requires test4F(X) >Int 0

rule [test4-1-3]: <k> test4State1() => test4State3() ... </k>
<int> X </int>
requires test4F(X) <=Int 0


rule [test4F-zero-if-x-positive]: test4F(X:Int) => 0 requires X >Int 0
rule [test4F-one-if-not-x-nonpositive]: test4F(X:Int) => 1 requires X <=Int 0

// to produce input state:
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
// then edit state-test1Init.json to substitute test1State1() for test1Init()
Expand Down
Loading

0 comments on commit 1987f36

Please sign in to comment.