Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Realize generic navigation structure #3472

Merged
merged 14 commits into from
Jun 26, 2024
2 changes: 1 addition & 1 deletion gradle/wrapper/gradle-wrapper.properties
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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()
Expand All @@ -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()
Expand All @@ -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;
}
Expand All @@ -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
Expand Down Expand Up @@ -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;
}

Expand Down
12 changes: 12 additions & 0 deletions key.core/src/main/java/de/uka/ilkd/key/java/Comment.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@

import de.uka.ilkd.key.java.visitor.Visitor;

import org.key_project.logic.SyntaxElement;

/**
* Comment element of Java source code.
*/
Expand Down Expand Up @@ -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");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand All @@ -25,4 +27,8 @@ public interface NonTerminalProgramElement extends ProgramElement {
*/
ProgramElement getChildAt(int index);

@Override
default SyntaxElement getChild(int n) {
return getChildAt(n);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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 {


/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

}
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ public SourceElement getFirstElement() {

@Override
public SourceElement getLastElement() {
return getChildAt(getChildCount() - 1).getLastElement();
return getChildAt(this.getChildCount() - 1).getLastElement();
}


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ public SourceElement getFirstElementIncludingBlocks() {

@Override
public SourceElement getLastElement() {
return getChildAt(getChildCount() - 1).getLastElement();
return getChildAt(this.getChildCount() - 1).getLastElement();
}


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand All @@ -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");
Expand Down
Original file line number Diff 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
15 changes: 15 additions & 0 deletions key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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();
}
3 changes: 1 addition & 2 deletions key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ public ProgramVariable exceptionVariable() {
* {@inheritDoc}
*/
@Override
public ProgramVariable getChild(int i) {
public ProgramVariable getTLChild(int i) {
if (i == 0) {
return exceptionVariable();
}
Expand All @@ -51,7 +51,7 @@ public ProgramVariable getChild(int i) {
* {@inheritDoc}
*/
@Override
public int getChildCount() {
public int getTLChildCount() {
return 1;
}

Expand Down
Loading
Loading