Realize generic navigation structure (#3472)

Author: Drodt

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();
     }