Handle Switch in Taclets w/o Transformer

build.gradle

@@ -61,7 +61,7 @@ subprojects {
 
     repositories {
         mavenCentral()
-        //maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
+        maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
     }
 
     dependencies {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -1691,7 +1691,8 @@ public static int computeStackSize(RuleApp ruleApp) {
                             JavaProgramElement element = block.program();
                             if (element instanceof StatementBlock) {
                                 StatementBlock b = (StatementBlock) block.program();
-                                ImmutableArray<ProgramPrefix> prefix = b.getPrefixElements();
+                                ImmutableArray<PossibleProgramPrefix> prefix =
+                                    b.getPrefixElements();
                                 result = CollectionUtil.count(prefix,
                                     element1 -> element1 instanceof MethodFrame);
                             }
@@ -4008,7 +4009,8 @@ public static Pair<Integer, SourceElement> computeSecondStatement(
                     blocks.addFirst((StatementBlock) firstStatement);
                 }
                 SourceElement lastStatement = null;
-                while (firstStatement instanceof ProgramPrefix && lastStatement != firstStatement) {
+                while (firstStatement instanceof PossibleProgramPrefix
+                        && lastStatement != firstStatement) {
                     lastStatement = firstStatement;
                     firstStatement = firstStatement.getFirstElementIncludingBlocks();
                     if (lastStatement instanceof MethodFrame) {

key.core/build.gradle

@@ -17,7 +17,7 @@ dependencies {
 
     api project(':key.util')
 
-    def JP_VERSION = "3.28.0-K13.5"
+    def JP_VERSION = "3.28.0-K13.5-switch-SNAPSHOT2"
     api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
     api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
     api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"

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

@@ -15,7 +15,7 @@
 import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
 import de.uka.ilkd.key.java.visitor.JavaASTVisitor;
 import de.uka.ilkd.key.logic.JavaBlock;
-import de.uka.ilkd.key.logic.ProgramPrefix;
+import de.uka.ilkd.key.logic.PossibleProgramPrefix;
 
 import org.key_project.util.ExtList;
 
@@ -36,12 +36,15 @@ public static SourceElement getActiveStatement(JavaBlock jb) {
         assert jb.program() != null;
 
         SourceElement result = jb.program().getFirstElement();
-        while ((result instanceof ProgramPrefix || result instanceof CatchAllStatement)
-                && !(result instanceof StatementBlock && ((StatementBlock) result).isEmpty())) {
+        while ((result instanceof PossibleProgramPrefix pre && pre.isPrefix())
+                || result instanceof CatchAllStatement) {
             if (result instanceof LabeledStatement) {
                 result = ((LabeledStatement) result).getChildAt(1);
             } else if (result instanceof CatchAllStatement) {
                 result = ((CatchAllStatement) result).getBody();
+            } else if (result == result.getFirstElement()
+                    && ((PossibleProgramPrefix) result).isPrefix()) {
+                System.out.println(result);
             } else {
                 result = result.getFirstElement();
             }

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

@@ -33,35 +33,7 @@
 import de.uka.ilkd.key.java.ast.reference.ThisReference;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
-import de.uka.ilkd.key.java.ast.statement.Branch;
-import de.uka.ilkd.key.java.ast.statement.Break;
-import de.uka.ilkd.key.java.ast.statement.Case;
-import de.uka.ilkd.key.java.ast.statement.Catch;
-import de.uka.ilkd.key.java.ast.statement.Continue;
-import de.uka.ilkd.key.java.ast.statement.Default;
-import de.uka.ilkd.key.java.ast.statement.Do;
-import de.uka.ilkd.key.java.ast.statement.Else;
-import de.uka.ilkd.key.java.ast.statement.EmptyStatement;
-import de.uka.ilkd.key.java.ast.statement.EnhancedFor;
-import de.uka.ilkd.key.java.ast.statement.Finally;
-import de.uka.ilkd.key.java.ast.statement.For;
-import de.uka.ilkd.key.java.ast.statement.ForUpdates;
-import de.uka.ilkd.key.java.ast.statement.Guard;
-import de.uka.ilkd.key.java.ast.statement.IForUpdates;
-import de.uka.ilkd.key.java.ast.statement.IGuard;
-import de.uka.ilkd.key.java.ast.statement.ILoopInit;
-import de.uka.ilkd.key.java.ast.statement.If;
-import de.uka.ilkd.key.java.ast.statement.LabeledStatement;
-import de.uka.ilkd.key.java.ast.statement.LoopInit;
-import de.uka.ilkd.key.java.ast.statement.MethodBodyStatement;
-import de.uka.ilkd.key.java.ast.statement.MethodFrame;
-import de.uka.ilkd.key.java.ast.statement.Return;
-import de.uka.ilkd.key.java.ast.statement.Switch;
-import de.uka.ilkd.key.java.ast.statement.SynchronizedBlock;
-import de.uka.ilkd.key.java.ast.statement.Then;
-import de.uka.ilkd.key.java.ast.statement.Throw;
-import de.uka.ilkd.key.java.ast.statement.Try;
-import de.uka.ilkd.key.java.ast.statement.While;
+import de.uka.ilkd.key.java.ast.statement.*;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.VariableNamer;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
@@ -2484,8 +2456,7 @@ public static SuperReference superReference() {
      * @return a new {@link Switch} block that executes <code>branches</code> depending on the value
      *         of <code>expression</code>
      */
-    public static Switch switchBlock(final Expression expression, final Branch[] branches) {
-
+    public static Switch switchBlock(final Expression expression, final SwitchBranch[] branches) {
         return new Switch(expression, branches);
     }
 

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

@@ -4,7 +4,7 @@
 package de.uka.ilkd.key.java;
 
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
-import de.uka.ilkd.key.logic.ProgramPrefix;
+import de.uka.ilkd.key.logic.PossibleProgramPrefix;
 
 public class ProgramPrefixUtil {
 
@@ -26,7 +26,7 @@ public MethodFrame getInnerMostMethodFrame() {
         }
     }
 
-    public static ProgramPrefixInfo computeEssentials(ProgramPrefix prefix) {
+    public static ProgramPrefixInfo computeEssentials(PossibleProgramPrefix prefix) {
         int length = 1;
         MethodFrame mf = (MethodFrame) (prefix instanceof MethodFrame ? prefix : null);
         while (prefix.hasNextPrefixElement()) {

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

@@ -272,6 +272,9 @@ public JTerm convertVariableReference(VariableReference fr, ExecutionContext ec)
         } else if (var.isStatic()) {
             final Function fieldSymbol =
                 heapLDT.getFieldSymbolForPV((LocationVariable) var, services);
+            if (var.isFinal() && FinalHeapResolution.recallIsFinalEnabled()) {
+                return tb.staticFinalDot(var.sort(), fieldSymbol);
+            }
             return tb.staticDot(var.sort(), fieldSymbol);
         } else if (prefix == null) {
             if (var.isMember()) {

key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java

@@ -12,7 +12,7 @@
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
-import de.uka.ilkd.key.logic.ProgramPrefix;
+import de.uka.ilkd.key.logic.PossibleProgramPrefix;
 import de.uka.ilkd.key.rule.MatchConditions;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
@@ -168,12 +168,12 @@ public MatchConditions match(SourceData source, MatchConditions matchCond,
 
         ExecutionContext lastExecutionContext = null;
 
-        final ProgramPrefix prefix;
+        final PossibleProgramPrefix prefix;
         int pos = -1;
         PosInProgram relPos = PosInProgram.TOP;
 
-        if (src instanceof ProgramPrefix) {
-            prefix = (ProgramPrefix) src;
+        if (src instanceof PossibleProgramPrefix) {
+            prefix = (PossibleProgramPrefix) src;
             final int srcPrefixLength = prefix.getPrefixLength();
 
             if (getPrefixLength() > srcPrefixLength) {
@@ -182,7 +182,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond,
 
             pos = srcPrefixLength - getPrefixLength();
 
-            ProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos);
+            PossibleProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos);
 
             relPos = firstActiveStatement.getFirstActiveChildPos();
 
@@ -201,8 +201,9 @@ public MatchConditions match(SourceData source, MatchConditions matchCond,
 
                 start = relPos.get(relPos.depth() - 1);
                 if (relPos.depth() > 1) {
-                    firstActiveStatement = (ProgramPrefix) PosInProgram.getProgramAt(relPos.up(),
-                        firstActiveStatement);
+                    firstActiveStatement =
+                        (PossibleProgramPrefix) PosInProgram.getProgramAt(relPos.up(),
+                            firstActiveStatement);
                 }
             }
             newSource = new SourceData(firstActiveStatement, start, services);
@@ -270,7 +271,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond,
      * position
      */
     private MatchConditions makeContextInfoComplete(MatchConditions matchCond, SourceData newSource,
-            ProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src,
+            PossibleProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src,
             Services services) {
 
         final SVInstantiations instantiations = matchCond.getInstantiations();
@@ -308,7 +309,7 @@ private MatchConditions makeContextInfoComplete(MatchConditions matchCond, Sourc
      */
     private MatchConditions matchInnerExecutionContext(MatchConditions matchCond,
             final Services services, ExecutionContext lastExecutionContext,
-            final ProgramPrefix prefix, int pos, final ProgramElement src) {
+            final PossibleProgramPrefix prefix, int pos, final ProgramElement src) {
 
         // partial context instantiation
 
@@ -349,10 +350,11 @@ private MatchConditions matchInnerExecutionContext(MatchConditions matchCond,
      *        prefix.getPrefixElementAt(pos);
      * @return the PosInProgram of the first element, which is not part of the prefix
      */
-    private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInProgram relPos) {
+    private PosInProgram matchPrefixEnd(final PossibleProgramPrefix prefix, int pos,
+            PosInProgram relPos) {
         PosInProgram prefixEnd = PosInProgram.TOP;
         if (prefix != null) {
-            ProgramPrefix currentPrefix = prefix;
+            PossibleProgramPrefix currentPrefix = prefix;
             int i = 0;
             while (i <= pos) {
                 // concatenate this prefix element's active-child position in one step instead of
@@ -375,8 +377,8 @@ private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInPr
         return prefixEnd;
     }
 
-    private static ProgramPrefix getPrefixElementAt(ProgramPrefix prefix, int i) {
-        ProgramPrefix current = prefix;
+    private static PossibleProgramPrefix getPrefixElementAt(PossibleProgramPrefix prefix, int i) {
+        PossibleProgramPrefix current = prefix;
         for (int pos = 0; pos < i; pos++) {
             current = current.getNextPrefixElement();
         }

key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java

@@ -15,7 +15,7 @@
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
-import de.uka.ilkd.key.logic.ProgramPrefix;
+import de.uka.ilkd.key.logic.PossibleProgramPrefix;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.util.Debug;
 
@@ -31,7 +31,7 @@
  * Statement block. taken from COMPOST and changed to achieve an immutable structure
  */
 public class StatementBlock extends JavaStatement implements StatementContainer,
-        TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix {
+        TypeDeclarationContainer, VariableScope, TypeScope, PossibleProgramPrefix {
 
     /**
      * Body.
@@ -143,10 +143,9 @@ public boolean equals(Object o) {
     /**
      * computes the prefix elements for the given array of statment block
      */
-    public static ImmutableArray<ProgramPrefix> computePrefixElements(
-            ImmutableArray<? extends Statement> b,
-            ProgramPrefix current) {
-        final ArrayList<ProgramPrefix> prefix = new ArrayList<>();
+    public static ImmutableArray<PossibleProgramPrefix> computePrefixElements(
+            PossibleProgramPrefix current) {
+        final ArrayList<PossibleProgramPrefix> prefix = new ArrayList<>();
         prefix.add(current);
 
         while (current.hasNextPrefixElement()) {
@@ -157,7 +156,6 @@ public static ImmutableArray<ProgramPrefix> computePrefixElements(
         return new ImmutableArray<>(prefix);
     }
 
-
     /**
      * Get body.
      *
@@ -290,23 +288,29 @@ public SourceElement getFirstElementIncludingBlocks() {
         }
     }
 
+    @Override
+    public boolean isPrefix() {
+        return !isEmpty();
+    }
+
     @Override
     public boolean hasNextPrefixElement() {
-        return !body.isEmpty() && (body.get(0) instanceof ProgramPrefix);
+        return !body.isEmpty() && (body.get(0) instanceof PossibleProgramPrefix);
     }
 
     @Override
-    public ProgramPrefix getNextPrefixElement() {
+    public PossibleProgramPrefix getNextPrefixElement() {
         if (hasNextPrefixElement()) {
-            return (ProgramPrefix) body.get(0);
+            return (PossibleProgramPrefix) body.get(0);
         } else {
             throw new IndexOutOfBoundsException("No next prefix element " + this);
         }
     }
 
     @Override
-    public ProgramPrefix getLastPrefixElement() {
-        return hasNextPrefixElement() ? ((ProgramPrefix) body.get(0)).getLastPrefixElement() : this;
+    public PossibleProgramPrefix getLastPrefixElement() {
+        return hasNextPrefixElement() ? ((PossibleProgramPrefix) body.get(0)).getLastPrefixElement()
+                : this;
     }
 
     @Override
@@ -321,8 +325,8 @@ public MethodFrame getInnerMostMethodFrame() {
     }
 
     @Override
-    public ImmutableArray<ProgramPrefix> getPrefixElements() {
-        return computePrefixElements(body, this);
+    public ImmutableArray<PossibleProgramPrefix> getPrefixElements() {
+        return computePrefixElements(this);
     }
 
     @Override

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

@@ -6,20 +6,25 @@
 import java.util.ArrayList;
 import java.util.List;
 
+import de.uka.ilkd.key.java.ast.Comment;
+import de.uka.ilkd.key.java.ast.PositionInfo;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.abstraction.Type;
 import de.uka.ilkd.key.logic.JavaDLFieldNames;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
-import org.key_project.util.ExtList;
+import org.key_project.logic.sort.Sort;
+import org.key_project.util.collection.ImmutableArray;
+import org.key_project.util.collection.ImmutableList;
 
 /**
  * This class is used for wrapping an enum into a standard class type.
  *
  * <p>
- * In addition the programvariables that represent enum constants are memorized. Thus this class is
+ * In addition, the programvariables that represent enum constants are memorized. Thus this class is
  * able to have queries on the enum constants.
  *
  * @author mulbrich
@@ -33,27 +38,22 @@ public class EnumClassDeclaration extends ClassDeclaration {
      */
     private final List<IProgramVariable> constants = new ArrayList<>();
 
-    /**
-     * create a new EnumClassDeclaration that describes an enum defintion. It merely wraps a
-     * ClassDeclaration but has memory about which fields have been declared as enum constants.
-     *
-     * @param children
-     *        children in the ast (members)
-     * @param fullName
-     *        of the class/enum
-     * @param isLibrary
-     *        see class constructor
-     */
-    // TODO javaparser
-    public EnumClassDeclaration(
-            ExtList children, ProgramElementName fullName, boolean isLibrary
-    /* , List<EnumConstantDeclaration> enumConstantDeclarations */) {
-        super(children, fullName, isLibrary);
+    public EnumClassDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> modArray,
+            ProgramElementName name, ProgramElementName fullName,
+            ImmutableArray<MemberDeclaration> members, boolean parentIsInterface, boolean isLibrary,
+            Extends extending, Implements implementing, ImmutableList<TextualJMLConstruct> spec,
+            Sort sort) {
+        super(pi, c, modArray, name, fullName, members, parentIsInterface, isLibrary, extending,
+            implementing, false, false, false, spec);
 
-        // for (EnumConstantDeclaration ecd : enumConstantDeclarations) {
-        // String constName = ecd.getEnumConstantSpecification().getName();
-        // constants.add(findAttr(constName));
-        // }
+        for (var m : members) {
+            if (m instanceof FieldDeclaration fd && fd.isFinal() && fd.isStatic() && fd.isPublic()
+                    && fd.getFieldSpecifications().size() == 1) {
+                var fs = fd.getFieldSpecifications().get(0);
+                if (fs.getProgramVariable().sort() == sort)
+                    constants.add(fs.getProgramVariable());
+            }
+        }
     }
 
     /*
@@ -124,8 +124,8 @@ public int getNumberOfConstants() {
     public static boolean isEnumConstant(IProgramVariable attribute) {
         KeYJavaType kjt = attribute.getKeYJavaType();
         Type type = kjt.getJavaType();
-        if (type instanceof EnumClassDeclaration) {
-            return ((EnumClassDeclaration) type).isLocalEnumConstant(attribute);
+        if (type instanceof EnumClassDeclaration ecd) {
+            return ecd.isLocalEnumConstant(attribute);
         } else {
             return false;
         }