Skip to content

Commit c32da1e

Browse files
DrodtDrodt
committed
Add proof settings to float files; use correct strategy factory for macros
1 parent c0b1a62 commit c32da1e

File tree

7 files changed

+305
-11
lines changed

7 files changed

+305
-11
lines changed

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@
4747
import de.uka.ilkd.key.speclang.Contract;
4848
import de.uka.ilkd.key.speclang.OperationContract;
4949
import de.uka.ilkd.key.strategy.JavaCardDLStrategyFactory;
50+
import de.uka.ilkd.key.strategy.ModularJavaDLStrategyFactory;
5051
import de.uka.ilkd.key.strategy.Strategy;
5152
import de.uka.ilkd.key.strategy.StrategyProperties;
5253
import de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor;
@@ -4325,7 +4326,7 @@ public static void initializeStrategy(SymbolicExecutionTreeBuilder builder) {
43254326
new SymbolicExecutionStrategy.Factory().create(proof, strategyProperties));
43264327
} else {
43274328
proof.setActiveStrategy(
4328-
new JavaCardDLStrategyFactory().create(proof, strategyProperties));
4329+
new ModularJavaDLStrategyFactory().create(proof, strategyProperties));
43294330
}
43304331
}
43314332

‎key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java‎

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,7 @@
1212
import de.uka.ilkd.key.proof.Goal;
1313
import de.uka.ilkd.key.proof.Proof;
1414
import de.uka.ilkd.key.proof.init.ProofOblInput;
15-
import de.uka.ilkd.key.strategy.JavaCardDLStrategyFactory;
16-
import de.uka.ilkd.key.strategy.RuleAppCostCollector;
17-
import de.uka.ilkd.key.strategy.Strategy;
18-
import de.uka.ilkd.key.strategy.StrategyProperties;
15+
import de.uka.ilkd.key.strategy.*;
1916

2017
import org.key_project.logic.Name;
2118
import org.key_project.prover.proof.ProofGoal;
@@ -136,10 +133,10 @@ public Name name() {
136133
String name = ruleApp.rule().name().toString();
137134
if ((admittedRuleNames.contains(name) || name.startsWith(INF_FLOW_UNFOLD_PREFIX))
138135
&& ruleApplicationInContextAllowed(ruleApp, pio, goal)) {
139-
JavaCardDLStrategyFactory strategyFactory = new JavaCardDLStrategyFactory();
140-
Strategy<@NonNull Goal> javaDlStrategy =
136+
ModularJavaDLStrategyFactory strategyFactory = new ModularJavaDLStrategyFactory();
137+
Strategy<@NonNull Goal> dlStrategy =
141138
strategyFactory.create(goal.proof(), new StrategyProperties());
142-
RuleAppCost costs = javaDlStrategy.computeCost(ruleApp, pio, goal, mState);
139+
RuleAppCost costs = dlStrategy.computeCost(ruleApp, pio, goal, mState);
143140
if ("orLeft".equals(name)) {
144141
costs = costs.add(NumberRuleAppCost.create(100));
145142
}

‎key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,16 +77,16 @@ private RuleSetDispatchFeature setupCostComputationF() {
7777
final RuleSetDispatchFeature d = new RuleSetDispatchFeature();
7878

7979
bindRuleSet(d, "closure", -15000);
80-
bindRuleSet(d, "alpha", -7000);
80+
bindRuleSet(d, "alpha", print("alpha", longConst(-7000)));
8181
bindRuleSet(d, "delta", -6000);
8282
bindRuleSet(d, "simplify_boolean", -200);
8383

8484
final Feature findDepthFeature =
8585
FindDepthFeature.getInstance();
8686

8787
bindRuleSet(d, "concrete",
88-
add(longConst(-11000),
89-
ScaleFeature.createScaled(findDepthFeature, 10.0)));
88+
print("Concrete", add(longConst(-11000),
89+
ScaleFeature.createScaled(findDepthFeature, 10.0))));
9090
bindRuleSet(d, "simplify", -4500);
9191
bindRuleSet(d, "simplify_enlarging", -2000);
9292
bindRuleSet(d, "simplify_ENLARGING", -1900);

‎key.ui/examples/redux/arrays/Arrays.copyOf.float.key‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,77 @@
1+
\settings // Proof-Settings-Config-File
2+
{
3+
"Choice" : {
4+
"JavaCard" : "JavaCard:off",
5+
"Strings" : "Strings:on",
6+
"assertions" : "assertions:on",
7+
"bigint" : "bigint:on",
8+
"finalFields" : "finalFields:immutable",
9+
"floatRules" : "floatRules:strictfpOnly",
10+
"initialisation" : "initialisation:disableStaticInitialisation",
11+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
12+
"integerSimplificationRules" : "integerSimplificationRules:full",
13+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
14+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
15+
"methodExpansion" : "methodExpansion:modularOnly",
16+
"modelFields" : "modelFields:showSatisfiability",
17+
"moreSeqRules" : "moreSeqRules:off",
18+
"permissions" : "permissions:off",
19+
"programRules" : "programRules:Java",
20+
"reach" : "reach:on",
21+
"runtimeExceptions" : "runtimeExceptions:allow",
22+
"sequences" : "sequences:on",
23+
"soundDefaultContracts" : "soundDefaultContracts:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "Modular JavaDL Strategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
68+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
69+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
70+
"VBT_PHASE" : "VBT_SYM_EX"
71+
}
72+
}
73+
}
74+
175
\javaSource "./src";
276

377
\chooseContract "Arrays[Arrays::copyOf([F,int)].JML normal_behavior operation contract.0";

‎key.ui/examples/redux/arrays/Arrays.copyOfRange.float.key‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,77 @@
1+
\settings // Proof-Settings-Config-File
2+
{
3+
"Choice" : {
4+
"JavaCard" : "JavaCard:off",
5+
"Strings" : "Strings:on",
6+
"assertions" : "assertions:on",
7+
"bigint" : "bigint:on",
8+
"finalFields" : "finalFields:immutable",
9+
"floatRules" : "floatRules:strictfpOnly",
10+
"initialisation" : "initialisation:disableStaticInitialisation",
11+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
12+
"integerSimplificationRules" : "integerSimplificationRules:full",
13+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
14+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
15+
"methodExpansion" : "methodExpansion:modularOnly",
16+
"modelFields" : "modelFields:showSatisfiability",
17+
"moreSeqRules" : "moreSeqRules:off",
18+
"permissions" : "permissions:off",
19+
"programRules" : "programRules:Java",
20+
"reach" : "reach:on",
21+
"runtimeExceptions" : "runtimeExceptions:allow",
22+
"sequences" : "sequences:on",
23+
"soundDefaultContracts" : "soundDefaultContracts:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "Modular JavaDL Strategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
68+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
69+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
70+
"VBT_PHASE" : "VBT_SYM_EX"
71+
}
72+
}
73+
}
74+
175
\javaSource "./src";
276

377
\chooseContract "Arrays[Arrays::copyOfRange([F,int,int)].JML normal_behavior operation contract.0";

‎key.ui/examples/redux/arrays/Arrays.fill.float.key‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,77 @@
1+
\settings // Proof-Settings-Config-File
2+
{
3+
"Choice" : {
4+
"JavaCard" : "JavaCard:off",
5+
"Strings" : "Strings:on",
6+
"assertions" : "assertions:on",
7+
"bigint" : "bigint:on",
8+
"finalFields" : "finalFields:immutable",
9+
"floatRules" : "floatRules:strictfpOnly",
10+
"initialisation" : "initialisation:disableStaticInitialisation",
11+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
12+
"integerSimplificationRules" : "integerSimplificationRules:full",
13+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
14+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
15+
"methodExpansion" : "methodExpansion:modularOnly",
16+
"modelFields" : "modelFields:showSatisfiability",
17+
"moreSeqRules" : "moreSeqRules:off",
18+
"permissions" : "permissions:off",
19+
"programRules" : "programRules:Java",
20+
"reach" : "reach:on",
21+
"runtimeExceptions" : "runtimeExceptions:allow",
22+
"sequences" : "sequences:on",
23+
"soundDefaultContracts" : "soundDefaultContracts:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "Modular JavaDL Strategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
68+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
69+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
70+
"VBT_PHASE" : "VBT_SYM_EX"
71+
}
72+
}
73+
}
74+
175
\javaSource "./src";
276

377
\chooseContract "Arrays[Arrays::fill([F,float)].JML normal_behavior operation contract.0";

‎key.ui/examples/redux/arrays/Arrays.fillFromTo.float.key‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,77 @@
1+
\settings // Proof-Settings-Config-File
2+
{
3+
"Choice" : {
4+
"JavaCard" : "JavaCard:off",
5+
"Strings" : "Strings:on",
6+
"assertions" : "assertions:on",
7+
"bigint" : "bigint:on",
8+
"finalFields" : "finalFields:immutable",
9+
"floatRules" : "floatRules:strictfpOnly",
10+
"initialisation" : "initialisation:disableStaticInitialisation",
11+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
12+
"integerSimplificationRules" : "integerSimplificationRules:full",
13+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
14+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
15+
"methodExpansion" : "methodExpansion:modularOnly",
16+
"modelFields" : "modelFields:showSatisfiability",
17+
"moreSeqRules" : "moreSeqRules:off",
18+
"permissions" : "permissions:off",
19+
"programRules" : "programRules:Java",
20+
"reach" : "reach:on",
21+
"runtimeExceptions" : "runtimeExceptions:allow",
22+
"sequences" : "sequences:on",
23+
"soundDefaultContracts" : "soundDefaultContracts:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "Modular JavaDL Strategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
68+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
69+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
70+
"VBT_PHASE" : "VBT_SYM_EX"
71+
}
72+
}
73+
}
74+
175
\javaSource "./src";
276

377
\chooseContract "Arrays[Arrays::fill([F,int,int,float)].JML normal_behavior operation contract.0";

0 commit comments

Comments
 (0)