Skip to content

Commit ad12fe2

Browse files
unp1unp1
committed
If reading the value of two locations (o,f) and (u,f) has different values then o != u
Some heap simplification rules rely in their assumes on the fact that two objects are different, i.e., \assumes (==> o = u). this change makes it more likely for that formula to be actually present
1 parent 370caf3 commit ad12fe2

4 files changed

Lines changed: 130 additions & 0 deletions

File tree

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99

1010
import de.uka.ilkd.key.ldt.HeapLDT;
1111
import de.uka.ilkd.key.ldt.LocSetLDT;
12+
import de.uka.ilkd.key.logic.op.Equality;
1213
import de.uka.ilkd.key.proof.Goal;
1314
import de.uka.ilkd.key.proof.Proof;
1415
import de.uka.ilkd.key.rule.BuiltInRule;
@@ -180,6 +181,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
180181
final int pullOutHeapSize = getHeapSizeBound();
181182
bindRuleSet(d, "pull_out_heap",
182183
pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize));
184+
bindRuleSet(d, "derive_inequality", longConst(-2000));
183185
bindRuleSet(d, "simplify_heap_high_costs", inftyConst());
184186

185187
bindRuleSet(d, "javaIntegerSemantics",
@@ -491,6 +493,19 @@ protected Feature setupApprovalF() {
491493
private RuleSetDispatchFeature setupApprovalDispatcher() {
492494
final RuleSetDispatchFeature d = new RuleSetDispatchFeature();
493495

496+
// Only derive a disequality that is not known yet. The same disequality follows from
497+
// every location the two objects read differently, so a duplicate-application check does
498+
// not recognise those derivations as duplicates: their instantiations differ while their
499+
// conclusion does not. Comparing the conclusion against the succedent does.
500+
final TermBuffer succedentFormula = new TermBuffer();
501+
final TermBuffer firstObject = new TermBuffer();
502+
final TermBuffer secondObject = new TermBuffer();
503+
bindRuleSet(d, "derive_inequality",
504+
let(firstObject, instOf("o"), let(secondObject, instOf("o2"),
505+
sum(succedentFormula, SequentFormulasGenerator.succedent(),
506+
not(applyTF(succedentFormula,
507+
or(opSub(Equality.EQUALS, eq(firstObject), eq(secondObject)),
508+
opSub(Equality.EQUALS, eq(secondObject), eq(firstObject)))))))));
494509
bindRuleSet(d, "inReachableStateImplication", NonDuplicateAppModPositionFeature.INSTANCE);
495510
bindRuleSet(d, "limitObserver", NonDuplicateAppModPositionFeature.INSTANCE);
496511
bindRuleSet(d, "partialInvAxiom", NonDuplicateAppModPositionFeature.INSTANCE);

‎key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -534,6 +534,21 @@
534534
\heuristics(simplify_select_elim_store)
535535
};
536536

537+
\lemma
538+
differentValuesForSameHeapAndFieldImplyDifferentObjects {
539+
\schemaVar \term Heap h;
540+
\schemaVar \term Object o, o2;
541+
\schemaVar \term Field f;
542+
\schemaVar \term beta x;
543+
544+
\assumes(select<[beta]>(h, o, f) = x ==>)
545+
\find(==> select<[beta]>(h, o2, f) = x)
546+
547+
\add(==> o = o2)
548+
549+
\heuristics(derive_inequality)
550+
};
551+
537552
dismissNonSelectedField {
538553
\schemaVar \term Heap h;
539554
\schemaVar \term Object o, u;

‎key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -273,6 +273,7 @@
273273
hide_auxiliary_eq;
274274
hide_auxiliary_eq_const;
275275
simplify_heap_high_costs;
276+
derive_inequality;
276277

277278
// chrisg: pattern-based automation rules
278279
auto_induction;

‎key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
\profile "Java Profile";
2+
3+
\settings {
4+
"Choice" : {
5+
"JavaCard" : "JavaCard:off",
6+
"Strings" : "Strings:on",
7+
"assertions" : "assertions:safe",
8+
"bigint" : "bigint:on",
9+
"finalFields" : "finalFields:immutable",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation:disableStaticInitialisation",
12+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"permissions" : "permissions:off",
20+
"programRules" : "programRules:Java",
21+
"reach" : "reach:on",
22+
"runtimeExceptions" : "runtimeExceptions:ban",
23+
"sequences" : "sequences:on",
24+
"soundDefaultContracts" : "soundDefaultContracts:on"
25+
},
26+
"Labels" : {
27+
"UseOriginLabels" : true
28+
},
29+
"NewSMT" : {
30+
31+
},
32+
"SMTSettings" : {
33+
"SelectedTaclets" : [
34+
35+
],
36+
"UseBuiltUniqueness" : false,
37+
"explicitTypeHierarchy" : false,
38+
"instantiateHierarchyAssumptions" : true,
39+
"integersMaximum" : 2147483645,
40+
"integersMinimum" : -2147483645,
41+
"invariantForall" : false,
42+
"maxGenericSorts" : 2,
43+
"useConstantsForBigOrSmallIntegers" : true,
44+
"useUninterpretedMultiplication" : true
45+
},
46+
"Strategy" : {
47+
"ActiveStrategy" : "Modular JavaDL Strategy",
48+
"MaximumNumberOfAutomaticApplications" : 20000,
49+
"Timeout" : -1,
50+
"options" : {
51+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
52+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
53+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
54+
"DEP_OPTIONS_KEY" : "DEP_ON",
55+
"HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL",
56+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
57+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
58+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
59+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
60+
"OSS_OPTIONS_KEY" : "OSS_ON",
61+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
62+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
63+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
64+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
65+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
66+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
67+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
68+
"TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST",
69+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
70+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
71+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
72+
"VBT_PHASE" : "VBT_SYM_EX"
73+
}
74+
}
75+
}
76+
77+
78+
79+
\proofObligation
80+
//
81+
{
82+
"class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
83+
"name" : "differentValuesForSameHeapAndFieldImplyDifferentObjects"
84+
}
85+
86+
\proof {
87+
(keyLog "0" (keyUser "bubel" ) (keyVersion "05e3502a91ab2e6abbe38d72dd4c959321fc29a5"))
88+
89+
(autoModeTime "37")
90+
91+
(branch "dummy ID"
92+
(rule "impRight" (formula "1"))
93+
(rule "orRight" (formula "2"))
94+
(rule "notRight" (formula "3"))
95+
(rule "eqSymm" (formula "2"))
96+
(rule "applyEq" (formula "3") (term "1,0") (ifseqformula "2"))
97+
(rule "close" (formula "3") (ifseqformula "1"))
98+
)
99+
}

0 commit comments

Comments
 (0)