Merge branch 'refs/heads/main' into weigl/testgen

* refs/heads/main: Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test repair soundness of assignment2UpdateRules with checked overflows spotless Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design throw an error if choices used in a taclet are not declared correct inRange(..) predicates for overflow check semantics fix creating of branches for overflow checking
KeYProject · Jun 26, 2024 · 80d923b · 80d923b
2 parents a5d6cae + ed267fd
commit 80d923b
Show file tree

Hide file tree

Showing 128 changed files with 939 additions and 320 deletions.
diff --git a/gradle/wrapper/gradle-wrapper.properties b/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
diff --git a/...de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/...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;
     }
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java b/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");
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java b/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);
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java b/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 {
 
 
     /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java b/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 {
+
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java b/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();
     }
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java b/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");
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java b/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();
     }
 
     /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java b/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();
     }
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java b/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();
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java b/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();
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java b/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);
     }
 
     /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java b/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");

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java b/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();
     }
 
     /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java b/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");
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java b/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();
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java b/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();
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java b/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;
     }
-Original file line number
+Diff line change
@@ Expand Up / @@ -137,7 +137,7 @@ public SourceElement getFirstElement() { @@
         public SourceElement getLastElement() {
-            return getChildAt(getChildCount() - 1).getLastElement();
+            return getChildAt(this.getChildCount() - 1).getLastElement();
         }
         /**
@@ Expand Down @@