From e16aa76a669852f0615b299867b75a704718ae7c Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Fri, 24 Oct 2025 22:23:58 +0200 Subject: [PATCH 1/2] fixes #3670 --- key.core/src/main/antlr4/KeYLexer.g4 | 3 +- key.core/src/main/antlr4/KeYParser.g4 | 3 +- .../declaration/EnumClassDeclaration.java | 77 +++++-------------- .../key/nparser/builder/TacletPBuilder.java | 5 +- .../varexp/ConstructorBasedBuilder.java | 12 ++- .../varexp/TacletBuilderManipulators.java | 8 +- .../conditions/EnumConstantCondition.java | 64 +++++++++++---- .../rule/conditions/EnumTypeCondition.java | 5 ++ .../rule/metaconstruct/EnumConstantValue.java | 41 ++++------ .../key/java/JavaRedux/java/lang/Enum.java | 8 +- .../de/uka/ilkd/key/proof/rules/java5.key | 41 ++++++---- .../key/gui/sourceview/KeYEditorLexer.java | 4 +- 12 files changed, 141 insertions(+), 130 deletions(-) diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 544c9371a42..d5ae1ae7fa4 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/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'; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index f111efcedec..4ec7931821c 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -663,7 +663,6 @@ 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 @@ -671,7 +670,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | ISARRAYLENGTH | IS_ABSTRACT_OR_INTERFACE | IS_FINAL - | ENUM_CONST + | ISENUMCONST | FINAL | STATIC | ISLOCALVARIABLE diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java index b77ce9abccf..c393297cda1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java +++ b/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.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import org.key_project.util.ExtList; +import org.key_project.util.collection.Pair; import recoder.java.declaration.EnumConstantDeclaration; /** @@ -23,16 +24,20 @@ * 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 constants = new ArrayList<>(); + private final Map> constants = new HashMap<>(); /** * create a new EnumClassDeclaration that describes an enum defintion. It merely wraps a @@ -48,9 +53,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 +82,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 +92,13 @@ 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; - } - } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 7964520a468..f381f431222 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -546,9 +546,9 @@ public Object visitVarexp(KeYParser.VarexpContext ctx) { String name = ctx.varexpId().getText(); List arguments = ctx.varexp_argument(); List suitableManipulators = - TacletBuilderManipulators.getConditionBuildersFor(name); + TacletBuilderManipulators.getConditionBuildersFor(name); List parameters = - ctx.parameter.stream().map(Token::getText).collect(Collectors.toList()); + ctx.parameter.stream().map(Token::getText).collect(Collectors.toList()); boolean applied = false; Object[] argCache = new Object[arguments.size()]; for (TacletBuilderCommand manipulator : suitableManipulators) { @@ -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; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java index a5353a2ef01..41b0ff7360f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java @@ -9,8 +9,12 @@ import java.util.List; 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 clazz; private final boolean negationSupported; @@ -54,8 +58,14 @@ public VariableCondition build(Object[] arguments, List 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)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 7d7d102e5c3..c11f5ccac39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/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 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 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 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, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java index 4578382c936..18209300895 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java @@ -5,15 +5,22 @@ 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.jspecify.annotations.Nullable; 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; /** @@ -22,17 +29,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 +51,49 @@ 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 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 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 + ")"; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java index e5a729c17f2..371bd071c5f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java @@ -19,9 +19,14 @@ /** * 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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java index 1a3c882c9fd..6b9add75467 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java @@ -5,21 +5,29 @@ import de.uka.ilkd.key.java.KeYJavaASTFactory; import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.declaration.ClassDeclaration; import de.uka.ilkd.key.java.declaration.EnumClassDeclaration; import de.uka.ilkd.key.java.expression.literal.IntLiteral; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.AbstractTermTransformer; +import de.uka.ilkd.key.logic.op.IProgramVariable; +import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.rule.conditions.EnumConstantCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; +import org.key_project.logic.op.Function; import org.key_project.logic.op.Operator; +import org.key_project.util.collection.Pair; /** * resolve a program variable to an integer literal. * - * If the PV is a enum constant, its index in the enum constant array is returned. If the PC is a - * reference to the nextToCreate field than the number of enum constants is returned. + * If the PV is a enum constant field constant, its index in the enum constant array is returned. + * This is the ordinal of the enum constant. * * @author mulbrich */ @@ -39,33 +47,14 @@ public EnumConstantValue() { */ public JTerm transform(JTerm term, SVInstantiations svInst, Services services) { term = term.sub(0); - Operator op = term.op(); - if (op instanceof ProgramVariable pv) { - int value; - - // String varname = pv.getProgramElementName().getProgramName(); - - if (false) {// varname.endsWith(ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE)) {//TODO - // - if (pv.getContainerType().getJavaType() instanceof EnumClassDeclaration ecd) { - value = ecd.getNumberOfConstants(); - } else { - throw new IllegalArgumentException(term + " is not in an enum type."); - } - } else { - // enum constant - value = EnumClassDeclaration.indexOf(pv); - if (value == -1) { - throw new IllegalArgumentException(term + " is not an enum constant"); - } - } - - final IntLiteral valueLiteral = KeYJavaASTFactory.intLiteral(value); - term = services.getTypeConverter().convertToLogicElement(valueLiteral); + @Nullable Pair enConst = EnumConstantCondition.resolveEnumFieldConstant(term, services); + if(enConst == null) { + return term; } - return term; + int ordinal = enConst.first; + return services.getTermBuilder().zTerm(ordinal); } } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java index 2f822fc942a..7e26e6449c7 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java @@ -5,9 +5,13 @@ public abstract class Enum extends java.lang.Object implements java.lang.Comparable, java.io.Serializable { - public final java.lang.String name(); - public final int ordinal(); + + /*@ public normal_behavior + @ ensures \result == \dl_enumOrdinal(this); + @ assignable \strictly_nothing; + @*/ + public /*@ helper */ final int ordinal(); protected Enum(java.lang.String arg0, int arg1); public final java.lang.Class getDeclaringClass(); public static java.lang.Enum valueOf(java.lang.Class arg0, java.lang.String arg1); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key index 5db23d9e9d7..be5fdb7f59a 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key @@ -3,10 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ \sorts { - \generic E; + \generic E \extends java.lang.Object; \generic G; } +\functions { + int enumOrdinal(java.lang.Object); +} + \schemaVariables { \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal; \program Type #ty; @@ -25,7 +29,8 @@ \formula post, inv; - \term E e; + \term Field e; + \term Field e1, e2; } /*** @@ -72,25 +77,29 @@ *** Enumerations ***/ \rules(programRules:Java) { - /* XXX - enumConstantByIndex { - \assumes(wellFormed(heap) ==>) - \find( e ) - \sameUpdateLevel - \varcond(\enumConstant(e)) - \replacewith( E::(#enumconstantvalue(e)) ) + enumConstantEq { + \find( E::final(null, e1) = E::final(null, e2) ) + \varcond(\isEnumConst(E, e1), \isEnumConst(E, e2)) + \replacewith( e1 = e2 ) \heuristics(simplify) }; + enumConstantNull { + \find( E::final(null, e) = null ) + \varcond(\isEnumConst(E, e)) + \replacewith( false ) + \heuristics(simplify) + }; enumOrdinalToIndex { - \find( #fieldref(e, "ordinal") ) - \varcond(\isEnumType(E)) - \add(e = E::(#fieldref(e, "ordinal")) ==> ) + \find( enumOrdinal(E::final(null, e)) ) + \varcond(\isEnumConst(E, e)) + \replacewith( #enumconstantvalue(e) ) + \heuristics(simplify) }; +} - } - +/* \rules(programRules:Java,initialisation:disableStaticInitialisation) { enumNextToCreateConstant { @@ -114,5 +123,5 @@ \replacewith( #enumconstantvalue(#nc) ) \heuristics(simplify) }; - */ -} + + }*/ diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java index 3240e1d3bdd..0304b2bc924 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java @@ -105,8 +105,8 @@ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { addAll(KEYWORDS2, MODALOPERATOR, PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, SKOLEMTERM, SKOLEMFORMULA, TERMLABEL, VARIABLES, VARIABLE, APPLY_UPDATE_ON_RIGID, DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, DROP_EFFECTLESS_STORES, - SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, FREELABELIN, HASSORT, FIELDTYPE, FINAL, - ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, + SIMPLIFY_IF_THEN_ELSE_UPDATE, ISENUMCONST, FREELABELIN, HASSORT, FIELDTYPE, FINAL, + ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, ISMODELFIELD, ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, From b3556018a5e8372152c9db322f1a2db686aea93c Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Fri, 24 Oct 2025 22:33:48 +0200 Subject: [PATCH 2/2] spotlessing --- .../java/declaration/EnumClassDeclaration.java | 12 +++++++----- .../key/nparser/builder/TacletPBuilder.java | 4 ++-- .../varexp/ConstructorBasedBuilder.java | 9 +++++---- .../varexp/TacletBuilderManipulators.java | 6 +++--- .../rule/conditions/EnumConstantCondition.java | 11 +++++++---- .../key/rule/conditions/EnumTypeCondition.java | 5 +++-- .../rule/metaconstruct/EnumConstantValue.java | 18 ++++++------------ 7 files changed, 33 insertions(+), 32 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java index c393297cda1..64bf18797ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java @@ -10,11 +10,11 @@ import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.IProgramVariable; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; 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; /** @@ -37,7 +37,8 @@ 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 Map> constants = new HashMap<>(); + private final Map> constants = + new HashMap<>(); /** * create a new EnumClassDeclaration that describes an enum defintion. It merely wraps a @@ -98,7 +99,8 @@ public int getNumberOfConstants() { * @return a pair of (index, program variable) of the enum constant with the given name or null * if there is no such constant */ - public @Nullable Pair<@NonNull Integer, @NonNull IProgramVariable> getConstant(String fieldName) { + public @Nullable Pair<@NonNull Integer, @NonNull IProgramVariable> getConstant( + String fieldName) { return constants.get(fieldName); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index f381f431222..c5d77b94862 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -546,9 +546,9 @@ public Object visitVarexp(KeYParser.VarexpContext ctx) { String name = ctx.varexpId().getText(); List arguments = ctx.varexp_argument(); List suitableManipulators = - TacletBuilderManipulators.getConditionBuildersFor(name); + TacletBuilderManipulators.getConditionBuildersFor(name); List parameters = - ctx.parameter.stream().map(Token::getText).collect(Collectors.toList()); + ctx.parameter.stream().map(Token::getText).collect(Collectors.toList()); boolean applied = false; Object[] argCache = new Object[arguments.size()]; for (TacletBuilderCommand manipulator : suitableManipulators) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java index 41b0ff7360f..b35352cfc0a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java @@ -9,6 +9,7 @@ import java.util.List; import org.key_project.prover.rules.VariableCondition; + import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -59,13 +60,13 @@ public VariableCondition build(Object[] arguments, List parameters, bool } catch (InstantiationException | IllegalAccessException | InvocationTargetException | IllegalArgumentException ignored) { LOGGER.debug("Constructor " + constructor - + " does not match the given arguments for VariableCondition " + clazz - + ". Trying next constructor."); + + " does not match the given arguments for VariableCondition " + clazz + + ". Trying next constructor."); } } throw new RuntimeException( - "No matching constructor found for VariableCondition " + clazz + " with args " - + Arrays.toString(args)); + "No matching constructor found for VariableCondition " + clazz + " with args " + + Arrays.toString(args)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index c11f5ccac39..dd7f7c29094 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -260,8 +260,8 @@ public VariableCondition build(Object[] arguments, List 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 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, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java index 18209300895..773fdfdc7d7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java @@ -13,7 +13,6 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import org.jspecify.annotations.Nullable; import org.key_project.logic.SyntaxElement; import org.key_project.logic.Term; import org.key_project.logic.op.Function; @@ -22,6 +21,8 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; + /** * ensures that the given instantiation for the schemavariable denotes a constant of an enum type. @@ -52,7 +53,8 @@ public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations s if (var == reference) { // try to find the enum constant field - @Nullable Pair field = resolveEnumFieldConstant(subst, services); + @Nullable + Pair field = resolveEnumFieldConstant(subst, services); if (field == null) return false; @@ -66,8 +68,9 @@ public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations s } // also used in EnumConstantValue - public static @Nullable Pair resolveEnumFieldConstant(Object obj, Services services) { - if(obj instanceof Term term) { + public static @Nullable Pair 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() diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java index 371bd071c5f..9eca109a9a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java @@ -20,8 +20,9 @@ * 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. + * handled by {@link EnumConstantCondition} that checks type and constant field in one + * varcond. + * Should be removed soon. * * @author mulbrich * @since 2006-12-14 diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java index 6b9add75467..9b1e0f0636f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java @@ -3,26 +3,18 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.metaconstruct; -import de.uka.ilkd.key.java.KeYJavaASTFactory; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.java.declaration.ClassDeclaration; -import de.uka.ilkd.key.java.declaration.EnumClassDeclaration; -import de.uka.ilkd.key.java.expression.literal.IntLiteral; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.AbstractTermTransformer; import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.rule.conditions.EnumConstantCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; -import org.key_project.logic.op.Function; -import org.key_project.logic.op.Operator; import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; + /** * resolve a program variable to an integer literal. * @@ -48,8 +40,10 @@ public EnumConstantValue() { public JTerm transform(JTerm term, SVInstantiations svInst, Services services) { term = term.sub(0); - @Nullable Pair enConst = EnumConstantCondition.resolveEnumFieldConstant(term, services); - if(enConst == null) { + @Nullable + Pair enConst = + EnumConstantCondition.resolveEnumFieldConstant(term, services); + if (enConst == null) { return term; }