Realize generic navigation structure

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java

@@ -32,6 +32,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
      * A {@link Map} mapping from relevant variables for the condition to their runtime equivalent
      * in KeY
      */
-    private Map<SVSubstitute, SVSubstitute> variableNamingMap;
+    private Map<SyntaxElement, SyntaxElement> variableNamingMap;
 
     /**
      * The list of parameter variables of the method that contains the associated breakpoint
@@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node,
      *
      * @return the cloned map
      */
-    private Map<SVSubstitute, SVSubstitute> getOldMap() {
-        Map<SVSubstitute, SVSubstitute> oldMap = new HashMap<>();
-        for (Entry<SVSubstitute, SVSubstitute> svSubstituteSVSubstituteEntry : getVariableNamingMap()
+    private Map<SyntaxElement, SyntaxElement> getOldMap() {
+        Map<SyntaxElement, SyntaxElement> oldMap = new HashMap<>();
+        for (Entry<SyntaxElement, SyntaxElement> svSubstituteSVSubstituteEntry : getVariableNamingMap()
                 .entrySet()) {
             Entry<?, ?> oldEntry = svSubstituteSVSubstituteEntry;
-            if (oldEntry.getKey() instanceof SVSubstitute
-                    && oldEntry.getValue() instanceof SVSubstitute) {
-                oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue());
+            if (oldEntry.getKey() instanceof SyntaxElement
+                    && oldEntry.getValue() instanceof SyntaxElement) {
+                oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue());
             }
         }
         return oldMap;
@@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop
      * @param oldMap the oldMap variableNamings
      */
     private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope,
-            Map<SVSubstitute, SVSubstitute> oldMap, RuleApp ruleApp) {
+            Map<SyntaxElement, SyntaxElement> oldMap, RuleApp ruleApp) {
         // look for renamings KeY did
         boolean found = false;
         // get current renaming tables
@@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                         .getHashMap().entrySet()) {
                     Entry<?, ?> entry = value;
                     if (entry.getKey() instanceof LocationVariable
-                            && entry.getValue() instanceof SVSubstitute) {
+                            && entry.getValue() instanceof SyntaxElement) {
                         if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name()))
                                 .equals(varForCondition.name())
                                 && ((LocationVariable) entry.getKey()).name().toString()
@@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                             // add new value
                             toKeep.add((LocationVariable) entry.getValue());
                             getVariableNamingMap().put(varForCondition,
-                                (SVSubstitute) entry.getValue());
+                                (SyntaxElement) entry.getValue());
                             found = true;
                             break;
                         } else if (inScope && ((LocationVariable) entry.getKey()).name()
@@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                             // add new value
                             toKeep.add((LocationVariable) entry.getValue());
                             getVariableNamingMap().put(varForCondition,
-                                (SVSubstitute) entry.getValue());
+                                (SyntaxElement) entry.getValue());
                             found = true;
                             break;
                         }
@@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
     protected void refreshVarMaps(RuleApp ruleApp, Node node) {
         boolean inScope = isInScope(node);
         // collect old values
-        Map<SVSubstitute, SVSubstitute> oldMap = getOldMap();
+        Map<SyntaxElement, SyntaxElement> oldMap = getOldMap();
         // put values into map which have to be replaced
         for (ProgramVariable varForCondition : getVarsForCondition()) {
             // put global variables only done when a variable is instantiated by
@@ -498,14 +499,14 @@ public Set<LocationVariable> getToKeep() {
     /**
      * @return the variableNamingMap
      */
-    public Map<SVSubstitute, SVSubstitute> getVariableNamingMap() {
+    public Map<SyntaxElement, SyntaxElement> getVariableNamingMap() {
         return variableNamingMap;
     }
 
     /**
      * @param variableNamingMap the variableNamingMap to set
      */
-    public void setVariableNamingMap(Map<SVSubstitute, SVSubstitute> variableNamingMap) {
+    public void setVariableNamingMap(Map<SyntaxElement, SyntaxElement> variableNamingMap) {
         this.variableNamingMap = variableNamingMap;
     }
 

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

@@ -5,6 +5,8 @@
 
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+import org.key_project.logic.SyntaxElement;
+
 /**
  * Comment element of Java source code.
  */
@@ -71,4 +73,14 @@ public boolean equals(Object o) {
         }
         return (getText().equals(cmp.getText()));
     }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+
+    @Override
+    public SyntaxElement getChild(int n) {
+        throw new IndexOutOfBoundsException("Comment has no children");
+    }
 }

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

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java;
 
+import org.key_project.logic.SyntaxElement;
+
 /**
  * Non terminal program element. taken from COMPOST and changed to achieve an immutable structure
  */
@@ -25,4 +27,8 @@ public interface NonTerminalProgramElement extends ProgramElement {
      */
     ProgramElement getChildAt(int index);
 
+    @Override
+    default SyntaxElement getChild(int n) {
+        return getChildAt(n);
+    }
 }

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

@@ -4,15 +4,16 @@
 package de.uka.ilkd.key.java;
 
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
+
+import org.key_project.logic.SyntaxElement;
 
 /**
  * A source element is a piece of syntax. It does not necessarily have a semantics, at least none
  * that is machinable, for instance a {@link recoder.java.Comment}. taken from RECODER and changed
  * to achieve an immutable structure
  */
 
-public interface SourceElement extends SVSubstitute {
+public interface SourceElement extends SyntaxElement {
 
 
     /**

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

@@ -3,9 +3,12 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java;
 
+import org.key_project.logic.TerminalSyntaxElement;
+
 /**
  * Terminal program element. taken from COMPOST and changed to achieve an immutable structure
  */
 
-public interface TerminalProgramElement extends ProgramElement {
+public interface TerminalProgramElement extends ProgramElement, TerminalSyntaxElement {
+
 }

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

@@ -163,7 +163,7 @@ public SourceElement getFirstElement() {
 
     @Override
     public SourceElement getLastElement() {
-        return getChildAt(getChildCount() - 1).getLastElement();
+        return getChildAt(this.getChildCount() - 1).getLastElement();
     }
 
 

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

@@ -4,16 +4,16 @@
 package de.uka.ilkd.key.java.declaration;
 
 import de.uka.ilkd.key.java.JavaProgramElement;
-import de.uka.ilkd.key.java.TerminalProgramElement;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.ExtList;
 
 /**
  * Modifier. taken from COMPOST and changed to achieve an immutable structure
  */
 
-public abstract class Modifier extends JavaProgramElement implements TerminalProgramElement {
+public abstract class Modifier extends JavaProgramElement {
 
     /**
      * Modifier.
@@ -56,4 +56,14 @@ public String getText() {
     public void visit(Visitor v) {
         v.performActionOnModifier(this);
     }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+
+    @Override
+    public SyntaxElement getChild(int n) {
+        throw new IndexOutOfBoundsException(getClass() + " " + this + " has no children");
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java

@@ -31,13 +31,13 @@ public class Instanceof extends TypeOperator {
 
     public Instanceof(ExtList children) {
         super(children);
-        assert getChildCount() == 2 : "not 2 children but " + getChildCount();
+        assert this.getChildCount() == 2 : "not 2 children but " + this.getChildCount();
     }
 
 
     public Instanceof(Expression unaryChild, TypeReference typeref) {
         super(unaryChild, typeref);
-        assert getChildCount() == 2 : "not 2 children but " + getChildCount();
+        assert this.getChildCount() == 2 : "not 2 children but " + this.getChildCount();
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java

@@ -99,7 +99,7 @@ public SourceElement getFirstElementIncludingBlocks() {
 
     @Override
     public SourceElement getLastElement() {
-        return getChildAt(getChildCount() - 1).getLastElement();
+        return getChildAt(this.getChildCount() - 1).getLastElement();
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java

@@ -7,7 +7,7 @@
 
 import org.key_project.util.collection.ImmutableArray;
 
-public interface IForUpdates extends de.uka.ilkd.key.java.TerminalProgramElement {
+public interface IForUpdates extends de.uka.ilkd.key.java.NonTerminalProgramElement {
 
     int size();
 

key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java

@@ -4,11 +4,11 @@
 package de.uka.ilkd.key.java.statement;
 
 import de.uka.ilkd.key.java.LoopInitializer;
-import de.uka.ilkd.key.java.TerminalProgramElement;
+import de.uka.ilkd.key.java.NonTerminalProgramElement;
 
 import org.key_project.util.collection.ImmutableArray;
 
-public interface ILoopInit extends TerminalProgramElement {
+public interface ILoopInit extends NonTerminalProgramElement {
 
     int size();
 

key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java

@@ -107,7 +107,7 @@ public ImmutableArray<ProgramPrefix> getPrefixElements() {
     @Override
     public PosInProgram getFirstActiveChildPos() {
         return getStatementCount() == 0 ? PosInProgram.TOP
-                : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+                : PosInProgram.TOP.down(this.getChildCount() - 1).down(0);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java

@@ -53,7 +53,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext,
         this.execContext = execContext;
 
         firstActiveChildPos =
-            body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+            body.isEmpty() ? PosInProgram.TOP
+                    : PosInProgram.TOP.down(getChildCount() - 1).down(0);
 
         Debug.assertTrue(execContext != null, "methodframe: executioncontext missing");
         Debug.assertTrue(body != null, "methodframe: body missing");
@@ -78,7 +79,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext,
         this.execContext = execContext;
 
         firstActiveChildPos =
-            body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+            body.isEmpty() ? PosInProgram.TOP
+                    : PosInProgram.TOP.down(getChildCount() - 1).down(0);
 
 
         Debug.assertTrue(execContext != null, "methodframe: executioncontext missing");

key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java

@@ -137,7 +137,7 @@ public SourceElement getFirstElement() {
 
 
     public SourceElement getLastElement() {
-        return getChildAt(getChildCount() - 1).getLastElement();
+        return getChildAt(this.getChildCount() - 1).getLastElement();
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java

@@ -8,6 +8,7 @@
 import de.uka.ilkd.key.pp.PrettyPrinter;
 
 import org.key_project.logic.Program;
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.EqualsModProofIrrelevancy;
 
 import org.slf4j.Logger;
@@ -128,4 +129,18 @@ public int hashCodeModProofIrrelevancy() {
         }
         return hashCode;
     }
+
+    @Override
+    public int getChildCount() {
+        if (prg == null || this == EMPTY_JAVABLOCK)
+            return 0;
+        return 1;
+    }
+
+    @Override
+    public SyntaxElement getChild(int n) {
+        if (n == 0)
+            return prg;
+        throw new IndexOutOfBoundsException("JavaBlock " + this + " has only one child");
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java

@@ -18,6 +18,8 @@
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 
+import org.key_project.logic.SyntaxElement;
+
 /**
  * A type that implement this interface can be used in all java programs instead of an expression or
  * statement. For example class SchemaVariable implements this interface to be able to stand for
@@ -26,4 +28,9 @@
 public interface ProgramConstruct extends Expression, Statement, ILoopInit, IForUpdates, IGuard,
         Label, TerminalProgramElement, ExpressionStatement, TypeReference, IProgramVariable,
         IProgramMethod, Branch, IExecutionContext, MethodName {
+    @Override
+    SyntaxElement getChild(int n);
+
+    @Override
+    int getChildCount();
 }

key.core/src/main/java/de/uka/ilkd/key/logic/Term.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.Visitor;
@@ -43,7 +42,7 @@
  * supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
  */
 public interface Term
-        extends SVSubstitute, Sorted, TermEqualsModProperty, org.key_project.logic.Term {
+        extends Sorted, TermEqualsModProperty, org.key_project.logic.Term {
     @Override
     Operator op();
 

key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java

@@ -40,7 +40,7 @@ public ProgramVariable exceptionVariable() {
      * {@inheritDoc}
      */
     @Override
-    public ProgramVariable getChild(int i) {
+    public ProgramVariable getTLChild(int i) {
         if (i == 0) {
             return exceptionVariable();
         }
@@ -51,7 +51,7 @@ public ProgramVariable getChild(int i) {
      * {@inheritDoc}
      */
     @Override
-    public int getChildCount() {
+    public int getTLChildCount() {
         return 1;
     }