fixes #3670: KeY does not know that enum constants are non-null

key.core/src/main/antlr4/KeYLexer.g4

@@ -116,7 +116,6 @@ DISJOINTMODULONULL  : '\\disjointModuloNull';
 DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries';
 DROP_EFFECTLESS_STORES : '\\dropEffectlessStores';
 SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate';
-ENUM_CONST : '\\enumConstant';
 FREELABELIN : '\\freeLabelIn';
 HASSORT : '\\hasSort';
 FIELDTYPE : '\\fieldType';
@@ -127,7 +126,7 @@ HASSUBFORMULAS : '\\hasSubFormulas';
 ISARRAY:'\\isArray';
 ISARRAYLENGTH:'\\isArrayLength';
 ISCONSTANT: '\\isConstant';
-ISENUMTYPE:'\\isEnumType';
+ISENUMCONST:'\\isEnumConst';
 ISINDUCTVAR:'\\isInductVar';
 ISLOCALVARIABLE : '\\isLocalVariable';
 ISOBSERVER : '\\isObserver';

key.core/src/main/antlr4/KeYParser.g4

@@ -663,15 +663,14 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
   | DIFFERENTFIELDS
   | SIMPLIFY_IF_THEN_ELSE_UPDATE
   | CONTAINS_ASSIGNMENT
-  | ISENUMTYPE
   | ISTHISREFERENCE
   | STATICMETHODREFERENCE
   | ISREFERENCEARRAY
   | ISARRAY
   | ISARRAYLENGTH
   | IS_ABSTRACT_OR_INTERFACE
   | IS_FINAL
-  | ENUM_CONST
+  | ISENUMCONST
   | FINAL
   | STATIC
   | ISLOCALVARIABLE

key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java

@@ -3,17 +3,18 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.declaration;
 
-import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 
-import de.uka.ilkd.key.java.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.abstraction.Type;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.logic.op.ProgramVariable;
 
 import org.key_project.util.ExtList;
+import org.key_project.util.collection.Pair;
 
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 import recoder.java.declaration.EnumConstantDeclaration;
 
 /**
@@ -23,16 +24,21 @@
  * In addition the programvariables that represent enum constants are memorized. Thus this class is
  * able to have queries on the enum constants.
  *
+ * mulbrich: Update 2025 (a mere 19 years later):
+ * Updated from the old heap model to the new one.
+ *
  * @author mulbrich
- * @since 2006-12-10
+ * @since 2006-12-10, updated 2025-10-24 by MU
  */
 
 public class EnumClassDeclaration extends ClassDeclaration {
 
     /**
      * store the program variables which represent the enum constants
+     * in a lookup map from name to (ordinal index, program variable)
      */
-    private final List<IProgramVariable> constants = new ArrayList<>();
+    private final Map<String, Pair<@NonNull Integer, @NonNull IProgramVariable>> constants =
+        new HashMap<>();
 
     /**
      * create a new EnumClassDeclaration that describes an enum defintion. It merely wraps a
@@ -48,9 +54,11 @@ public EnumClassDeclaration(ExtList children, ProgramElementName fullName, boole
 
         super(children, fullName, isLibrary);
 
+        int ordinal = 0;
         for (EnumConstantDeclaration ecd : enumConstantDeclarations) {
             String constName = ecd.getEnumConstantSpecification().getName();
-            constants.add(findAttr(constName));
+            constants.put(constName, new Pair<>(ordinal, findAttr(constName)));
+            ordinal++;
         }
     }
 
@@ -75,33 +83,6 @@ private IProgramVariable findAttr(String fieldName) {
             fieldName + " is not an attribute of " + this.getFullName());
     }
 
-    /*
-     * is pv a enum constant of THIS enum?
-     */
-    private boolean isLocalEnumConstant(IProgramVariable pv) {
-        for (IProgramVariable cnst : constants) {
-            if (cnst.equals(pv)) {
-                return true;
-            }
-        }
-        return false;
-    }
-
-    /**
-     * get the index of the program variable amongst the enumconstants of THIS enum.
-     *
-     * @param pv PV to look up
-     * @return -1 if not found, otherwise the 0-based index.
-     */
-    private int localIndexOf(ProgramVariable pv) {
-        for (int i = 0; i < constants.size(); i++) {
-            if (constants.get(i).equals(pv)) {
-                return i;
-            }
-        }
-        return -1;
-    }
-
     /**
      * get the number of defined enum constants in this type.
      *
@@ -112,30 +93,14 @@ public int getNumberOfConstants() {
     }
 
     /**
-     * check whether a PV is an enum constant of any enum type.
+     * get the constant with the given name, including its ordinal index.
      *
-     * @param attribute ProgramVariable to check.
-     * @return true iff attribute is an enum constant.
+     * @param fieldName the name of the enum constant
+     * @return a pair of (index, program variable) of the enum constant with the given name or null
+     *         if there is no such constant
      */
-    public static boolean isEnumConstant(IProgramVariable attribute) {
-        KeYJavaType kjt = attribute.getKeYJavaType();
-        Type type = kjt.getJavaType();
-        if (type instanceof EnumClassDeclaration) {
-            return ((EnumClassDeclaration) type).isLocalEnumConstant(attribute);
-        } else {
-            return false;
-        }
+    public @Nullable Pair<@NonNull Integer, @NonNull IProgramVariable> getConstant(
+            String fieldName) {
+        return constants.get(fieldName);
     }
-
-    // TODO DOC
-    public static int indexOf(ProgramVariable attribute) {
-        KeYJavaType kjt = attribute.getKeYJavaType();
-        Type type = kjt.getJavaType();
-        if (type instanceof EnumClassDeclaration) {
-            return ((EnumClassDeclaration) type).localIndexOf(attribute);
-        } else {
-            return -1;
-        }
-    }
-
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -582,6 +582,7 @@ private boolean applyManipulator(boolean negated, Object[] args,
             manipulator.apply(peekTBuilder(), args, parameters, negated);
             return true;
         } catch (Throwable e) {
+            LOGGER.debug("Unexpected exception while producing variable condition", e);
             return false;
         }
     }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java

@@ -10,7 +10,12 @@
 
 import org.key_project.prover.rules.VariableCondition;
 
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 public class ConstructorBasedBuilder extends AbstractConditionBuilder {
+
+    private static final Logger LOGGER = LoggerFactory.getLogger(ConstructorBasedBuilder.class);
     private final Class<? extends VariableCondition> clazz;
     private final boolean negationSupported;
 
@@ -54,8 +59,14 @@ public VariableCondition build(Object[] arguments, List<String> parameters, bool
                 return (VariableCondition) constructor.newInstance(args);
             } catch (InstantiationException | IllegalAccessException | InvocationTargetException
                     | IllegalArgumentException ignored) {
+                LOGGER.debug("Constructor " + constructor
+                    + " does not match the given arguments for VariableCondition " + clazz
+                    + ". Trying next constructor.");
             }
         }
-        throw new RuntimeException();
+
+        throw new RuntimeException(
+            "No matching constructor found for VariableCondition " + clazz + " with args "
+                + Arrays.toString(args));
     }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java

@@ -228,7 +228,7 @@ public void apply(TacletBuilder<?> tb, Object[] arguments, List<String> paramete
     public static final AbstractConditionBuilder FINAL =
         new ConstructorBasedBuilder("final", FinalReferenceCondition.class, SV);
     public static final AbstractConditionBuilder ENUM_CONST =
-        new ConstructorBasedBuilder("isEnumConst", EnumConstantCondition.class, SV);
+        new ConstructorBasedBuilder("isEnumConst", EnumConstantCondition.class, SORT, SV);
     public static final AbstractConditionBuilder LOCAL_VARIABLE =
         new ConstructorBasedBuilder("isLocalVariable", LocalVariableCondition.class, SV);
     public static final AbstractConditionBuilder ARRAY_LENGTH =
@@ -260,8 +260,8 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
                 return new TypeCondition((TypeResolver) arguments[0], !negated, non_null);
             }
         };
-    public static final AbstractConditionBuilder ENUM_TYPE =
-        new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV);
+    // public static final AbstractConditionBuilder ENUM_TYPE =
+    // new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV);
     public static final AbstractConditionBuilder CONTAINS_ASSIGNMENT =
         new ConstructorBasedBuilder("containsAssignment", ContainsAssignmentCondition.class, SV);
     public static final AbstractConditionBuilder FIELD_TYPE =
@@ -377,7 +377,7 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
             FREE_3, FREE_4, FINAL_TYPE,
             FREE_5, NEW_TYPE_OF, NEW_DEPENDING_ON, FREE_LABEL_IN_VARIABLE, DIFFERENT, FINAL,
             ENUM_CONST, LOCAL_VARIABLE, ARRAY_LENGTH, ARRAY, REFERENCE_ARRAY, MAY_EXPAND_METHOD_2,
-            MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, ENUM_TYPE,
+            MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, /* ENUM_TYPE, */
             CONTAINS_ASSIGNMENT, FIELD_TYPE, STATIC_REFERENCE, DIFFERENT_FIELDS, SAME_OBSERVER,
             applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS,
             STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE,

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java

@@ -5,15 +5,23 @@
 
 
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.declaration.EnumClassDeclaration;
-import de.uka.ilkd.key.java.reference.FieldReference;
-import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
+import de.uka.ilkd.key.logic.sort.GenericSort;
 import de.uka.ilkd.key.rule.VariableConditionAdapter;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
 import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.Term;
+import org.key_project.logic.op.Function;
+import org.key_project.logic.op.Operator;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.logic.sort.Sort;
+import org.key_project.util.collection.Pair;
+
+import org.jspecify.annotations.Nullable;
 
 
 /**
@@ -22,17 +30,20 @@
  * @author mulbrich
  * @since 2006-12-04
  * @version 2006-12-11
+ * @version 2025-10-24 Refactored for the "new" heap model.
  */
 public final class EnumConstantCondition extends VariableConditionAdapter {
 
     private final SchemaVariable reference;
+    private final GenericSort typeReference;
 
     /**
      * the static reference condition checks if a suggested instantiation for a schema variable
      * denotes a reference to an enum constant.
      */
-    public EnumConstantCondition(SchemaVariable reference) {
+    public EnumConstantCondition(GenericSort typeReference, SchemaVariable reference) {
         this.reference = reference;
+        this.typeReference = typeReference;
     }
 
 
@@ -41,27 +52,51 @@ public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations s
             Services services) {
 
         if (var == reference) {
-            // new ObjectInspector(var).setVisible(true);
-            // new ObjectInspector(subst).setVisible(true);
-            ProgramVariable progvar;
-
-            if (subst instanceof FieldReference) {
-                progvar = ((FieldReference) subst).getProgramVariable();
-            } else if (subst instanceof JTerm && ((JTerm) subst).op() instanceof ProgramVariable) {
-                progvar = (ProgramVariable) ((JTerm) subst).op();
-            } else {
+            // try to find the enum constant field
+            @Nullable
+            Pair<Integer, IProgramVariable> field = resolveEnumFieldConstant(subst, services);
+            if (field == null)
                 return false;
-            }
-
-            return EnumClassDeclaration.isEnumConstant(progvar);
 
+            // if there is such a field, check that its type is the right enum type
+            KeYJavaType containerType = ((ProgramVariable) field.second).getContainerType();
+            Sort typeInst = svInst.getGenericSortInstantiations().getInstantiation(typeReference);
+            return containerType.getSort() == typeInst;
         }
+
         return true;
     }
 
+    // also used in EnumConstantValue
+    public static @Nullable Pair<Integer, IProgramVariable> resolveEnumFieldConstant(Object obj,
+            Services services) {
+        if (obj instanceof Term term) {
+            Operator op = term.op();
+            if (op instanceof Function func && func.isUnique()
+                    && func.sort() == services.getTypeConverter().getHeapLDT().getFieldSort()
+                    && func.name().toString().contains("::")) {
+                String funcName = func.name().toString();
+                int colon = funcName.indexOf("::$");
+                if (colon == -1) {
+                    return null;
+                }
+                String sortName = funcName.substring(0, colon);
+                String fieldName = funcName.substring(colon + 3);
+                KeYJavaType kjt = services.getJavaInfo().getKeYJavaType(sortName);
+                if (kjt == null || !(kjt.getJavaType() instanceof EnumClassDeclaration)) {
+                    return null;
+                }
+                EnumClassDeclaration ecd = (EnumClassDeclaration) kjt.getJavaType();
+                return ecd.getConstant(fieldName);
+            }
+        }
+        return null;
+    }
+
+
 
     @Override
     public String toString() {
-        return "\\enumConstant(" + reference + ")";
+        return "\\isEnumConst(" + typeReference + ", " + reference + ")";
     }
 }

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java

@@ -19,9 +19,15 @@
 /**
  * This variable condition checks if a type is an enum type.
  *
+ * @deprecated As of 2025, this varcond is no longer needed, its functionality is currently
+ *             handled by {@link EnumConstantCondition} that checks type and constant field in one
+ *             varcond.
+ *             Should be removed soon.
+ *
  * @author mulbrich
  * @since 2006-12-14
  */
+@Deprecated
 public final class EnumTypeCondition extends VariableConditionAdapter {
     private static final Logger LOGGER = LoggerFactory.getLogger(EnumTypeCondition.class);