Skip to content

Commit 4866a09

Browse files
unp1unp1
committed
Add update-simplification performance regression tests to runAllProofs
A new 'updateSimplificationPerformance' group with straight-line code and unrolled bounded loops. These symbolically execute long programs with many parallel updates, the case that stresses \dropEffectlessElementaries. They close quickly with the targeted update simplification but degrade quadratically without it -- straightline_10000 in particular proves in ~45s here but explodes if the quadratic behaviour returns, acting as a regression canary.
1 parent e3c974d commit 4866a09

7 files changed

Lines changed: 46373 additions & 0 deletions

File tree

‎key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,25 @@ public static ProofCollection automaticJavaDL() throws IOException {
166166
performancePOConstruction.provable(
167167
"performance-test/Test(Test__f1(int)).JML_normal_behavior_operation_contract.0.key");
168168

169+
// Symbolic-execution performance: straight-line code and (unrolled) bounded loops execute
170+
// a long program with many parallel updates, which stresses the update-simplification
171+
// machinery (\dropEffectlessElementaries). These close quickly with the targeted update
172+
// simplification but degrade quadratically without it; straightline_10000 in particular is
173+
// a regression canary -- fast as is, but it explodes if the quadratic behaviour returns.
174+
var updateSimplificationPerformance = c.group("updateSimplificationPerformance");
175+
updateSimplificationPerformance
176+
.provable("performance-test/updateSimplification/straightline_1000.key");
177+
updateSimplificationPerformance
178+
.provable("performance-test/updateSimplification/straightline_4000.key");
179+
updateSimplificationPerformance
180+
.provable("performance-test/updateSimplification/straightline_8000.key");
181+
updateSimplificationPerformance
182+
.provable("performance-test/updateSimplification/straightline_10000.key");
183+
updateSimplificationPerformance
184+
.provable("performance-test/updateSimplification/loop_2000.key");
185+
updateSimplificationPerformance
186+
.provable("performance-test/updateSimplification/loop_5000.key");
187+
169188

170189
// Tests for rule application restrictions
171190
var g = c.group("applicationRestrictions");

‎key.ui/examples/performance-test/updateSimplification/loop_2000.key‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/**
2+
@provable automatic
3+
Fixed-bound while loop, fully UNROLLED B times (LOOP_EXPAND).
4+
bound 2000, expected sum 1999000.
5+
GENERATED by claude-tools/key-synth-bench/gen_synth.py - do not edit by hand.
6+
*/
7+
\settings {
8+
"[Labels]UseOriginLabels=true
9+
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
10+
[SMTSettings]invariantForall=false
11+
[Strategy]ActiveStrategy=JavaCardDLStrategy
12+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
13+
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
14+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
15+
[Choice]DefaultChoices=assertions-assertions\\:on , intRules-intRules\\:arithmeticSemanticsIgnoringOF , initialisation-initialisation\\:disableStaticInitialisation , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , permissions-permissions\\:off , moreSeqRules-moreSeqRules\\:on , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , javaLoopTreatment-javaLoopTreatment\\:efficient , floatRules-floatRules\\:strictfpOnly , methodExpansion-methodExpansion\\:noRestrictions
16+
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
17+
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
18+
[SMTSettings]UseBuiltUniqueness=false
19+
[SMTSettings]explicitTypeHierarchy=false
20+
[SMTSettings]instantiateHierarchyAssumptions=true
21+
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
22+
[SMTSettings]SelectedTaclets=
23+
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
24+
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
25+
[Strategy]MaximumNumberOfAutomaticApplications=10000000
26+
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
27+
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
28+
[SMTSettings]useConstantsForBigOrSmallIntegers=true
29+
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
30+
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
31+
[Strategy]Timeout=-1
32+
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
33+
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
34+
[SMTSettings]useUninterpretedMultiplication=true
35+
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
36+
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
37+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
38+
[SMTSettings]maxGenericSorts=2
39+
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
40+
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
41+
[SMTSettings]integersMinimum=-2147483645
42+
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
43+
[SMTSettings]integersMaximum=2147483645
44+
"
45+
}
46+
47+
\programVariables {
48+
int i;
49+
int k;
50+
}
51+
52+
\problem {
53+
\<{
54+
i = 0;
55+
k = 0;
56+
while (k < 2000) {
57+
i = i + k;
58+
k = k + 1;
59+
}
60+
}\> i = 1999000
61+
}

‎key.ui/examples/performance-test/updateSimplification/loop_5000.key‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/**
2+
@provable automatic
3+
Fixed-bound while loop, fully UNROLLED B times (LOOP_EXPAND).
4+
bound 5000, expected sum 12497500.
5+
GENERATED by claude-tools/key-synth-bench/gen_synth.py - do not edit by hand.
6+
*/
7+
\settings {
8+
"[Labels]UseOriginLabels=true
9+
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
10+
[SMTSettings]invariantForall=false
11+
[Strategy]ActiveStrategy=JavaCardDLStrategy
12+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
13+
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
14+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
15+
[Choice]DefaultChoices=assertions-assertions\\:on , intRules-intRules\\:arithmeticSemanticsIgnoringOF , initialisation-initialisation\\:disableStaticInitialisation , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , permissions-permissions\\:off , moreSeqRules-moreSeqRules\\:on , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , javaLoopTreatment-javaLoopTreatment\\:efficient , floatRules-floatRules\\:strictfpOnly , methodExpansion-methodExpansion\\:noRestrictions
16+
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
17+
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
18+
[SMTSettings]UseBuiltUniqueness=false
19+
[SMTSettings]explicitTypeHierarchy=false
20+
[SMTSettings]instantiateHierarchyAssumptions=true
21+
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
22+
[SMTSettings]SelectedTaclets=
23+
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
24+
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
25+
[Strategy]MaximumNumberOfAutomaticApplications=10000000
26+
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
27+
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
28+
[SMTSettings]useConstantsForBigOrSmallIntegers=true
29+
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
30+
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
31+
[Strategy]Timeout=-1
32+
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
33+
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
34+
[SMTSettings]useUninterpretedMultiplication=true
35+
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
36+
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
37+
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
38+
[SMTSettings]maxGenericSorts=2
39+
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
40+
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
41+
[SMTSettings]integersMinimum=-2147483645
42+
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
43+
[SMTSettings]integersMaximum=2147483645
44+
"
45+
}
46+
47+
\programVariables {
48+
int i;
49+
int k;
50+
}
51+
52+
\problem {
53+
\<{
54+
i = 0;
55+
k = 0;
56+
while (k < 5000) {
57+
i = i + k;
58+
k = k + 1;
59+
}
60+
}\> i = 12497500
61+
}

0 commit comments

Comments
 (0)