Skip to content

Commit 05966cc

Browse files
unp1unp1
authored
Enable KeY to distinguish between classes of same name in different packages (#3805)
2 parents fed02b1 + b54300e commit 05966cc

11 files changed

Lines changed: 293 additions & 7 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java‎

Lines changed: 41 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ public class KeYJPMapping {
4545
* maps a recoder programelement (or something similar, e.g. Type)
4646
* to the KeY-equivalent
4747
*/
48-
private final HashMap<ResolvedType, KeYJavaType> typeMap;
48+
private final HashMap<ResolvedTypeWrapper, KeYJavaType> typeMap;
4949
private final Map<KeYJavaType, ResolvedType> typeMapRev;
5050

5151
/**
@@ -99,7 +99,7 @@ public KeYJavaType resolvedTypeToKeY(ResolvedType pe, JavaService converter) {
9999
@Nullable
100100
public KeYJavaType resolvedTypeToKeY(ResolvedType pe, boolean processOnDemand,
101101
JavaService converter) {
102-
var type = typeMap.get(pe);
102+
var type = typeMap.get(new ResolvedTypeWrapper(pe));
103103

104104
if (processOnDemand && type == null && pe.isReferenceType()) {
105105
try {
@@ -147,7 +147,7 @@ public void put(Node node, ProgramElement value) {
147147
}
148148

149149
public void put(ResolvedType rec, KeYJavaType key) {
150-
var formerValue = typeMap.putIfAbsent(rec, key);
150+
var formerValue = typeMap.putIfAbsent(new ResolvedTypeWrapper(rec), key);
151151
if (formerValue != null && !Objects.equals(formerValue, key))
152152
LOGGER.error("Duplicate registration of kjt: {}, former kjt: {}", key, formerValue);
153153
var formerType = typeMapRev.putIfAbsent(key, rec);
@@ -242,7 +242,44 @@ public void setParsingLibraries(boolean parsingLibraries) {
242242

243243
public void registerType(ResolvedType ref, KeYJavaType kjt) {
244244
LOGGER.trace("Registered {} // {}", ref, kjt);
245-
this.typeMap.put(ref, kjt);
245+
this.typeMap.put(new ResolvedTypeWrapper(ref), kjt);
246246
this.typeMapRev.put(kjt, ref);
247247
}
248+
249+
/**
250+
* Equals and hashcode of resolved types do not consider the fully qualified name or the
251+
* position in the AST
252+
* Hence, classes with same name that occur in different packages are not distinguished.
253+
*/
254+
private static final class ResolvedTypeWrapper {
255+
private final ResolvedType resolvedType;
256+
257+
public ResolvedTypeWrapper(ResolvedType resolvedType) {
258+
this.resolvedType = resolvedType;
259+
}
260+
261+
@Override
262+
public boolean equals(Object o) {
263+
if (o instanceof ResolvedTypeWrapper other) {
264+
final boolean eq = resolvedType.equals(other.resolvedType);
265+
if (eq && resolvedType.isReferenceType()) {
266+
if (!other.resolvedType.isReferenceType()) {
267+
return false; // should not be reachable as then eq is false, but ...
268+
}
269+
return resolvedType.asReferenceType().getQualifiedName()
270+
.equals(other.resolvedType.asReferenceType().getQualifiedName());
271+
}
272+
return eq;
273+
}
274+
return false;
275+
}
276+
277+
@Override
278+
public int hashCode() {
279+
return resolvedType.hashCode() + (resolvedType.isReferenceType()
280+
? resolvedType.asReferenceType().getQualifiedName().hashCode()
281+
: 0);
282+
}
283+
284+
}
248285
}

‎key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2263,6 +2263,30 @@ private SchemaVariable lookupSchemaVariable(String name, Node context) {
22632263
private record FullVariableDeclarator(
22642264
VariableDeclarator decl, ClassOrInterfaceDeclaration container, boolean isFinal,
22652265
boolean isStatic, boolean isModel, boolean isGhost) {
2266+
@Override
2267+
public boolean equals(Object o) {
2268+
if (o == null || getClass() != o.getClass())
2269+
return false;
2270+
FullVariableDeclarator that = (FullVariableDeclarator) o;
2271+
final boolean generatedEquals = isFinal == that.isFinal && isModel == that.isModel &&
2272+
isGhost == that.isGhost &&
2273+
isStatic == that.isStatic &&
2274+
Objects.equals(decl, that.decl) &&
2275+
Objects.equals(container, that.container);
2276+
2277+
if (!generatedEquals) {
2278+
return false;
2279+
}
2280+
return container != null ? Objects.equals(container.getFullyQualifiedName(),
2281+
that.container.getFullyQualifiedName()) : generatedEquals;
2282+
}
2283+
2284+
@Override
2285+
public int hashCode() {
2286+
return Objects.hash(decl, container,
2287+
container != null ? container.getFullyQualifiedName() : 17, isFinal, isStatic,
2288+
isModel, isGhost);
2289+
}
22662290
}
22672291

22682292
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1020,7 +1020,8 @@ pm, kjt, new Private(), preContract, representsFromContract,
10201020
JTerm mbyFromContract =
10211021
fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null;
10221022
final ClassAxiom modelMethodContractAxiom = new ContractAxiom(
1023-
"Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm,
1023+
"Contract axiom for " + pm.getName() + " in " + kjt.getFullName(),
1024+
pm,
10241025
kjt, new Private(), preFromContract, freePreFromContract,
10251026
postFromContract, freePostFromContract, mbyFromContract, atPreVars,
10261027
selfVar, resultVar, paramVars);

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -990,6 +990,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
990990
g.provable("standard_key/java_dl/switch/large_switch.key");
991991

992992

993+
// tests that KeY can deal with identical classes in different packages
994+
g.provable("standard_key/java_dl/identical_classes/pkgA_inc.key");
995+
g.provable("standard_key/java_dl/identical_classes/pkgB_inc.key");
996+
993997
g = c.group("redux");
994998
g.provable("redux/arrays/Arrays.copyOf.key");
995999
g.provable("redux/arrays/Arrays.copyOf.float.key");

‎key.ui/examples/standard_key/java_dl/identical_classes/README‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Test that KeY can distinguish identical classes in different packages

‎key.ui/examples/standard_key/java_dl/identical_classes/pkgA/A.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package pkgA;
2+
3+
public class A {
4+
//@ public static invariant COUNT >= 0;
5+
public static int COUNT;
6+
7+
/*@ public normal_behavior
8+
ensures \result == (COUNT == \old(COUNT) + 1);
9+
model two_state static boolean monInc();
10+
*/
11+
12+
/*@ public normal_behavior
13+
@ ensures monInc();
14+
@*/
15+
public static void inc() {
16+
COUNT++;
17+
}
18+
}

‎key.ui/examples/standard_key/java_dl/identical_classes/pkgA_inc.key‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
\profile "Java Profile";
2+
3+
\settings {
4+
"Choice" : {
5+
"JavaCard" : "JavaCard:off",
6+
"Strings" : "Strings:on",
7+
"assertions" : "assertions:on",
8+
"bigint" : "bigint:on",
9+
"finalFields" : "finalFields:onHeap",
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:noRestriction",
17+
"modelFields" : "modelFields:showSatisfiability",
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" : 50000,
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_DELAYED",
54+
"DEP_OPTIONS_KEY" : "DEP_ON",
55+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
56+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
57+
"MPS_OPTIONS_KEY" : "MPS_SKIP",
58+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
59+
"OSS_OPTIONS_KEY" : "OSS_ON",
60+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
61+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
62+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
63+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
64+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
65+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
66+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
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+
75+
76+
\javaSource ".";
77+
78+
\proofObligation
79+
//
80+
{
81+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
82+
"contract" : "pkgA.A[pkgA.A::inc()].JML normal_behavior operation contract.0",
83+
"name" : "pkgA.A[pkgA.A::inc()].JML normal_behavior operation contract.0"
84+
}

‎key.ui/examples/standard_key/java_dl/identical_classes/pkgB/A.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package pkgB;
2+
3+
public class A {
4+
//@ public static invariant COUNT >= 0;
5+
public static int COUNT;
6+
7+
/*@ public normal_behavior
8+
ensures \result == (COUNT == \old(COUNT) + 1);
9+
model two_state static boolean monInc();
10+
*/
11+
12+
/*@ public normal_behavior
13+
@ ensures monInc();
14+
@*/
15+
public static void inc() {
16+
COUNT++;
17+
}
18+
}

‎key.ui/examples/standard_key/java_dl/identical_classes/pkgB_inc.key‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
\profile "Java Profile";
2+
3+
\settings {
4+
"Choice" : {
5+
"JavaCard" : "JavaCard:off",
6+
"Strings" : "Strings:on",
7+
"assertions" : "assertions:on",
8+
"bigint" : "bigint:on",
9+
"finalFields" : "finalFields:onHeap",
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:noRestriction",
17+
"modelFields" : "modelFields:showSatisfiability",
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" : 50000,
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_DELAYED",
54+
"DEP_OPTIONS_KEY" : "DEP_ON",
55+
"LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
56+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
57+
"MPS_OPTIONS_KEY" : "MPS_SKIP",
58+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
59+
"OSS_OPTIONS_KEY" : "OSS_ON",
60+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
61+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
62+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
63+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
64+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
65+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
66+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
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+
75+
76+
\javaSource ".";
77+
78+
\proofObligation
79+
//
80+
{
81+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
82+
"contract" : "pkgB.A[pkgB.A::inc()].JML normal_behavior operation contract.0",
83+
"name" : "pkgB.A[pkgB.A::inc()].JML normal_behavior operation contract.0"
84+
}

‎key.ui/src/main/resources/logback.xml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
<configuration>
2+
<!-- disables logback configuration messages on start up, see #1725 -->
3+
<statusListener class="ch.qos.logback.core.status.NopStatusListener" />
4+
5+
<appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
6+
<file>key.log</file>
7+
<append>false</append>
8+
<encoder>
9+
<pattern>%-10relative %-5level %-15thread %-25logger{5} %msg %ex%n</pattern>
10+
</encoder>
11+
</appender>
12+
13+
<root level="INFO">
14+
<appender-ref ref="STDOUT"/>
15+
</root>
16+
</configuration>

0 commit comments

Comments
 (0)