Enable KeY to distinguish between classes of same name in different packages

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

@@ -45,7 +45,7 @@ public class KeYJPMapping {
      * maps a recoder programelement (or something similar, e.g. Type)
      * to the KeY-equivalent
      */
-    private final HashMap<ResolvedType, KeYJavaType> typeMap;
+    private final HashMap<ResolvedTypeWrapper, KeYJavaType> typeMap;
     private final Map<KeYJavaType, ResolvedType> typeMapRev;
 
     /**
@@ -99,7 +99,7 @@ public KeYJavaType resolvedTypeToKeY(ResolvedType pe, JavaService converter) {
     @Nullable
     public KeYJavaType resolvedTypeToKeY(ResolvedType pe, boolean processOnDemand,
             JavaService converter) {
-        var type = typeMap.get(pe);
+        var type = typeMap.get(new ResolvedTypeWrapper(pe));
 
         if (processOnDemand && type == null && pe.isReferenceType()) {
             try {
@@ -147,7 +147,7 @@ public void put(Node node, ProgramElement value) {
     }
 
     public void put(ResolvedType rec, KeYJavaType key) {
-        var formerValue = typeMap.putIfAbsent(rec, key);
+        var formerValue = typeMap.putIfAbsent(new ResolvedTypeWrapper(rec), key);
         if (formerValue != null && !Objects.equals(formerValue, key))
             LOGGER.error("Duplicate registration of kjt: {}, former kjt: {}", key, formerValue);
         var formerType = typeMapRev.putIfAbsent(key, rec);
@@ -242,7 +242,44 @@ public void setParsingLibraries(boolean parsingLibraries) {
 
     public void registerType(ResolvedType ref, KeYJavaType kjt) {
         LOGGER.trace("Registered {} // {}", ref, kjt);
-        this.typeMap.put(ref, kjt);
+        this.typeMap.put(new ResolvedTypeWrapper(ref), kjt);
         this.typeMapRev.put(kjt, ref);
     }
+
+    /**
+     * Equals and hashcode of resolved types do not consider the fully qualified name or the
+     * position in the AST
+     * Hence, classes with same name that occur in different packages are not distinguished.
+     */
+    private static final class ResolvedTypeWrapper {
+        private final ResolvedType resolvedType;
+
+        public ResolvedTypeWrapper(ResolvedType resolvedType) {
+            this.resolvedType = resolvedType;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+            if (o instanceof ResolvedTypeWrapper other) {
+                final boolean eq = resolvedType.equals(other.resolvedType);
+                if (eq && resolvedType.isReferenceType()) {
+                    if (!other.resolvedType.isReferenceType()) {
+                        return false; // should not be reachable as then eq is false, but ...
+                    }
+                    return resolvedType.asReferenceType().getQualifiedName()
+                            .equals(other.resolvedType.asReferenceType().getQualifiedName());
+                }
+                return eq;
+            }
+            return false;
+        }
+
+        @Override
+        public int hashCode() {
+            return resolvedType.hashCode() + (resolvedType.isReferenceType()
+                    ? resolvedType.asReferenceType().getQualifiedName().hashCode()
+                    : 0);
+        }
+
+    }
 }

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

@@ -2263,6 +2263,30 @@ private SchemaVariable lookupSchemaVariable(String name, Node context) {
     private record FullVariableDeclarator(
             VariableDeclarator decl, ClassOrInterfaceDeclaration container, boolean isFinal,
             boolean isStatic, boolean isModel, boolean isGhost) {
+        @Override
+        public boolean equals(Object o) {
+            if (o == null || getClass() != o.getClass())
+                return false;
+            FullVariableDeclarator that = (FullVariableDeclarator) o;
+            final boolean generatedEquals = isFinal == that.isFinal && isModel == that.isModel &&
+                    isGhost == that.isGhost &&
+                    isStatic == that.isStatic &&
+                    Objects.equals(decl, that.decl) &&
+                    Objects.equals(container, that.container);
+
+            if (!generatedEquals) {
+                return false;
+            }
+            return container != null ? Objects.equals(container.getFullyQualifiedName(),
+                that.container.getFullyQualifiedName()) : generatedEquals;
+        }
+
+        @Override
+        public int hashCode() {
+            return Objects.hash(decl, container,
+                container != null ? container.getFullyQualifiedName() : 17, isFinal, isStatic,
+                isModel, isGhost);
+        }
     }
 
 }

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

@@ -1020,7 +1020,8 @@ pm, kjt, new Private(), preContract, representsFromContract,
                             JTerm mbyFromContract =
                                 fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null;
                             final ClassAxiom modelMethodContractAxiom = new ContractAxiom(
-                                "Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm,
+                                "Contract axiom for " + pm.getName() + " in " + kjt.getFullName(),
+                                pm,
                                 kjt, new Private(), preFromContract, freePreFromContract,
                                 postFromContract, freePostFromContract, mbyFromContract, atPreVars,
                                 selfVar, resultVar, paramVars);

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

@@ -990,6 +990,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("standard_key/java_dl/switch/large_switch.key");
 
 
+        // tests that KeY can deal with identical classes in different packages
+        g.provable("standard_key/java_dl/identical_classes/pkgA_inc.key");
+        g.provable("standard_key/java_dl/identical_classes/pkgB_inc.key");
+
         g = c.group("redux");
         g.provable("redux/arrays/Arrays.copyOf.key");
         g.provable("redux/arrays/Arrays.copyOf.float.key");

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

@@ -0,0 +1 @@
+Test that KeY can distinguish identical classes in different packages

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

@@ -0,0 +1,18 @@
+package pkgA;
+
+public class A {
+    //@ public static invariant COUNT >= 0;
+    public static int COUNT;
+
+    /*@ public normal_behavior
+        ensures \result == (COUNT == \old(COUNT) + 1);
+        model two_state static boolean monInc();
+     */
+
+    /*@ public normal_behavior
+      @ ensures monInc();
+      @*/
+    public static void inc() {
+        COUNT++;
+    }
+}

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

@@ -0,0 +1,84 @@
+\profile "Java Profile";
+
+\settings { 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:on",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:onHeap",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:noRestriction",
+        "modelFields" : "modelFields:showSatisfiability",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on"
+    },
+    "Labels" : { 
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : { 
+
+    },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : { 
+        "ActiveStrategy" : "Modular JavaDL Strategy",
+        "MaximumNumberOfAutomaticApplications" : 50000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_SKIP",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
+} 
+
+
+\javaSource ".";
+
+\proofObligation 
+// 
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "pkgA.A[pkgA.A::inc()].JML normal_behavior operation contract.0",
+    "name" : "pkgA.A[pkgA.A::inc()].JML normal_behavior operation contract.0"
+}

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

@@ -0,0 +1,18 @@
+package pkgB;
+
+public class A {
+    //@ public static invariant COUNT >= 0;
+    public static int COUNT;
+
+    /*@ public normal_behavior
+        ensures \result == (COUNT == \old(COUNT) + 1);
+        model two_state static boolean monInc();
+     */
+
+    /*@ public normal_behavior
+      @ ensures monInc();
+      @*/
+    public static void inc() {
+        COUNT++;
+    }
+}

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

@@ -0,0 +1,84 @@
+\profile "Java Profile";
+
+\settings { 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:on",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:onHeap",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:noRestriction",
+        "modelFields" : "modelFields:showSatisfiability",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on"
+    },
+    "Labels" : { 
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : { 
+
+    },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : { 
+        "ActiveStrategy" : "Modular JavaDL Strategy",
+        "MaximumNumberOfAutomaticApplications" : 50000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_SKIP",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
+} 
+
+
+\javaSource ".";
+
+\proofObligation 
+// 
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "pkgB.A[pkgB.A::inc()].JML normal_behavior operation contract.0",
+    "name" : "pkgB.A[pkgB.A::inc()].JML normal_behavior operation contract.0"
+}

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

@@ -0,0 +1,16 @@
+<configuration>
+    <!-- disables logback configuration messages on start up, see #1725 -->
+    <statusListener class="ch.qos.logback.core.status.NopStatusListener" />
+
+    <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
+        <file>key.log</file>
+        <append>false</append>
+        <encoder>
+            <pattern>%-10relative %-5level %-15thread %-25logger{5} %msg %ex%n</pattern>
+        </encoder>
+    </appender>
+
+    <root level="INFO">
+        <appender-ref ref="STDOUT"/>
+    </root>
+</configuration>

key.util/build.gradle

@@ -14,10 +14,9 @@ dependencies {
     testFixturesApi("org.junit.jupiter:junit-jupiter-api")
     testFixturesApi("org.junit.jupiter:junit-jupiter-params")
     testFixturesApi("org.assertj:assertj-core:3.27.7")
-    testFixturesApi("ch.qos.logback:logback-classic:1.5.27")
     testFixturesApi("org.jspecify:jspecify:1.0.0")
 
-    testFixturesApi("ch.qos.logback:logback-classic:1.5.27")
+    testFixturesApi("ch.qos.logback:logback-classic:1.5.32")
 
     // test fixtures
     testFixturesApi("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.0")