diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index f5e94b961aa..504c102ccef 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/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 prefix = b.getPrefixElements(); + ImmutableArray prefix = + b.getPrefixElements(); result = CollectionUtil.count(prefix, element1 -> element1 instanceof MethodFrame); } @@ -4008,7 +4009,8 @@ public static Pair 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) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java index 1d7ac9e704f..055e2de59e9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java +++ b/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(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java index 0523878dbb1..1ea632ff8a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java +++ b/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 branches depending on the value * of expression */ - 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); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java b/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java index 04a941a8159..2a8bf62914a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java +++ b/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()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java index 304e085d9f5..219b700d76d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java +++ b/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; @@ -144,12 +144,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) { @@ -158,7 +158,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { pos = srcPrefixLength - getPrefixLength(); - ProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); + PossibleProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); relPos = firstActiveStatement.getFirstActiveChildPos(); @@ -177,8 +177,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); @@ -210,7 +211,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(); @@ -248,7 +249,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 @@ -289,10 +290,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) { final IntIterator it = currentPrefix.getFirstActiveChildPos().iterator(); @@ -315,8 +317,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(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java index bf47856cf72..2719106183b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java +++ b/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 computePrefixElements( - ImmutableArray b, - ProgramPrefix current) { - final ArrayList prefix = new ArrayList<>(); + public static ImmutableArray computePrefixElements( + PossibleProgramPrefix current) { + final ArrayList prefix = new ArrayList<>(); prefix.add(current); while (current.hasNextPrefixElement()) { @@ -157,7 +156,6 @@ public static ImmutableArray 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 getPrefixElements() { - return computePrefixElements(body, this); + public ImmutableArray getPrefixElements() { + return computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java new file mode 100644 index 00000000000..e41c7bfbd9c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java @@ -0,0 +1,200 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.statement; + +import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; + +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableArray; + +public class ActiveCase extends SwitchBranch implements PossibleProgramPrefix { + /** + * Body. + */ + protected final ImmutableArray body; + + private final MethodFrame innerMostMethodFrame; + + private final int prefixLength; + + public ActiveCase() { + this.body = null; + prefixLength = 0; + innerMostMethodFrame = null; + } + + public ActiveCase(Statement[] body) { + this.body = new ImmutableArray<>(body); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public ActiveCase(ImmutableArray body) { + this.body = body; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Constructor for the transformation of COMPOST ASTs to KeY. + * + * @param children the children of this AST element as KeY classes. May contain: Comments, + * several of Statement (as the statements for Default) + */ + public ActiveCase(ExtList children) { + super(children); + this.body = new ImmutableArray<>(children.collect(Statement.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Constructor for the transformation of COMPOST ASTs to KeY. + * + * @param children the children of this AST element as KeY classes. May contain: Comments a + * Statement (as the statement following case) Must NOT contain: an Expression indicating + * the condition of the case as there are classes that are Expression and Statement, so + * they might get mixed up. Use the second parameter of this constructor for the + * expression. + */ + public ActiveCase(ExtList children, PositionInfo pos) { + super(children, pos); + this.body = new ImmutableArray<>(children.collect(Statement.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Returns the number of children of this node. + * + * @return an int giving the number of children of this node + */ + public int getChildCount() { + int result = 0; + if (body != null) { + result += body.size(); + } + return result; + } + + /** + * Returns the child at the specified index in this node's "virtual" child array + * + * @param index an index into this node's "virtual" child array + * @return the program element at the given position + * @exception ArrayIndexOutOfBoundsException if index is out of bounds + */ + public ProgramElement getChildAt(int index) { + int len; + if (body != null) { + len = body.size(); + if (len > index) { + return body.get(index); + } + } + throw new ArrayIndexOutOfBoundsException(); + } + + @Override + public SourceElement getFirstElement() { + if (body.isEmpty()) + return this; + return body.get(0); + } + + /** + * Get the number of statements in this container. + * + * @return the number of statements. + */ + public int getStatementCount() { + return (body != null) ? body.size() : 0; + } + + /* + * Return the statement at the specified index in this node's "virtual" statement array. + * + * @param index an index for a statement. + * + * @return the statement with the given index. + * + * @exception ArrayIndexOutOfBoundsException if index is out of bounds. + */ + public Statement getStatementAt(int index) { + if (body != null) { + return body.get(index); + } + throw new ArrayIndexOutOfBoundsException(); + } + + /** + * The body may be empty (null), to define a fall-through. Attaching an {@link EmptyStatement} + * would create a single ";". + */ + public ImmutableArray getBody() { + return body; + } + + /** + * calls the corresponding method of a visitor in order to perform some action/transformation on + * this element + * + * @param v the Visitor + */ + public void visit(Visitor v) { + v.performActionOnActiveCase(this); + } + + @Override + public boolean isPrefix() { + return body != null && !body.isEmpty(); + } + + @Override + public boolean hasNextPrefixElement() { + return body != null && !body.isEmpty() && body.get(0) instanceof PossibleProgramPrefix; + } + + @Override + public PossibleProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (PossibleProgramPrefix) body.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; + } + + @Override + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return body.isEmpty() ? PosInProgram.TOP : PosInProgram.ZERO; + } + + @Override + public int getPrefixLength() { + return prefixLength; + } + + @Override + public MethodFrame getInnerMostMethodFrame() { + return innerMostMethodFrame; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java index ea185f532f1..2b85893c4f4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java @@ -24,6 +24,11 @@ public BranchStatement() { } + public BranchStatement(PositionInfo pos) { + super(pos); + } + + /** * Constructor for the transformation of COMPOST ASTs to KeY. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java index 8fe123b94cd..066cc65970d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java @@ -16,7 +16,7 @@ * Case. * */ -public class Case extends BranchImp implements ExpressionContainer { +public class Case extends SwitchBranch implements ExpressionContainer { /** * Expression. @@ -81,7 +81,7 @@ public Case(ExtList children, Expression expr, PositionInfo pos) { public Case(Expression expr, ImmutableArray body, PositionInfo pi, List comments) { - super(pi, comments); + super(new ExtList(comments.toArray()), pi); this.expression = expr; this.body = body; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java index faa6ae4c7f1..14203ecc881 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java @@ -5,10 +5,7 @@ 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.ProgramElement; -import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.visitor.Visitor; import org.key_project.util.ExtList; @@ -18,7 +15,7 @@ * Default. * */ -public class Default extends BranchImp { +public class Default extends SwitchBranch { /** * Body. @@ -56,7 +53,7 @@ public Default(ExtList children) { } public Default(ImmutableArray body, PositionInfo pi, List comments) { - super(pi, comments); + super(new ExtList(comments.toArray()), pi); this.body = body; } @@ -73,6 +70,11 @@ public int getChildCount() { return result; } + @Override + public SourceElement getFirstElement() { + return body.get(0); + } + /** * Returns the child at the specified index in this node's "virtual" child array * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java index 4fd74ad01cd..968c29fc29b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.ast.*; 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 org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -17,7 +17,7 @@ import org.jspecify.annotations.NonNull; -public class Exec extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Exec extends BranchStatement implements StatementContainer, PossibleProgramPrefix { private final StatementBlock body; private final ImmutableArray branches; private final MethodFrame innerMostMethodFrame; @@ -102,20 +102,20 @@ public Exec(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -130,8 +130,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } @NonNull diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java index 1551974266e..a45fe5a458a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java @@ -7,8 +7,8 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.ProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -17,7 +17,7 @@ * Labeled statement. */ public class LabeledStatement extends JavaStatement - implements StatementContainer, NamedProgramElement, ProgramPrefix { + implements StatementContainer, NamedProgramElement, PossibleProgramPrefix { /** * Name. @@ -99,10 +99,11 @@ public LabeledStatement(Label id, Statement statement, PositionInfo pos) { @Override public boolean hasNextPrefixElement() { - if (body instanceof ProgramPrefix) { + if (body instanceof PossibleProgramPrefix) { if (body instanceof StatementBlock) { return !((StatementBlock) body).isEmpty() - && ((StatementBlock) body).getStatementAt(0) instanceof ProgramPrefix; + && ((StatementBlock) body) + .getStatementAt(0) instanceof PossibleProgramPrefix; } return true; } @@ -110,9 +111,9 @@ public boolean hasNextPrefixElement() { } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) (body instanceof StatementBlock + return (PossibleProgramPrefix) (body instanceof StatementBlock ? ((StatementBlock) body).getStatementAt(0) : body); } else { @@ -121,16 +122,16 @@ public ProgramPrefix getNextPrefixElement() { } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { if (body instanceof StatementBlock) { - return StatementBlock.computePrefixElements(((StatementBlock) body).getBody(), this); - } else if (body instanceof ProgramPrefix) { - return StatementBlock.computePrefixElements(new ImmutableArray<>(body), this); + return StatementBlock.computePrefixElements(this); + } else if (body instanceof PossibleProgramPrefix) { + return StatementBlock.computePrefixElements(this); } return new ImmutableArray<>(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java index 94766986997..cf1e948dfe2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java @@ -23,7 +23,7 @@ import de.uka.ilkd.key.java.ast.expression.Expression; 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.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; @@ -39,7 +39,7 @@ * @author Dominic Scheurer */ public final class LoopScopeBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { @Nullable private final IProgramVariable indexPV; @@ -105,14 +105,13 @@ public LoopScopeBlock(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() - && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException( "No next prefix element " + this); @@ -120,10 +119,8 @@ public ProgramPrefix getNextPrefixElement() { } @Override - public ProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() - ? getNextPrefixElement().getLastPrefixElement() - : this; + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @Override @@ -137,8 +134,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java index 72d35726034..85c050c24d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.ast.reference.IExecutionContext; 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.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.util.Debug; @@ -21,7 +21,7 @@ * The statement inserted by KeY if a method call is executed. */ public class MethodFrame extends JavaStatement - implements StatementContainer, ProgramPrefix { + implements StatementContainer, PossibleProgramPrefix { /** * result @@ -118,20 +118,20 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext, @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -146,8 +146,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } public PosInProgram getFirstActiveChildPos() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java index a434d0835b1..ed676ad186a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java @@ -5,9 +5,15 @@ import java.util.List; +import de.uka.ilkd.key.java.ProgramPrefixUtil; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.literal.Literal; +import de.uka.ilkd.key.java.ast.reference.MetaClassReference; import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; +import de.uka.ilkd.key.logic.op.ProgramVariable; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -17,7 +23,7 @@ */ public class Switch extends BranchStatement - implements ExpressionContainer, VariableScope, TypeScope { + implements ExpressionContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Branches. @@ -31,7 +37,9 @@ public class Switch extends BranchStatement protected final Expression expression; + private final int prefixLength; + private final MethodFrame innerMostMethodFrame; /** * Switch. @@ -40,6 +48,8 @@ public class Switch extends BranchStatement public Switch() { this.branches = null; this.expression = null; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -52,6 +62,8 @@ public Switch() { public Switch(Expression e) { this.branches = null; this.expression = e; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -66,6 +78,26 @@ public Switch(Expression e) { public Switch(Expression e, Branch[] branches) { this.branches = new ImmutableArray<>(branches); this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public Switch(Expression e, ImmutableArray branches) { + this.branches = branches; + this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public Switch(PositionInfo pos, Expression e, Branch[] branches) { + super(pos); + this.branches = new ImmutableArray<>(branches); + this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } /** @@ -77,8 +109,11 @@ public Switch(Expression e, Branch[] branches) { public Switch(ExtList children) { super(children); - this.expression = children.get(Expression.class); + this.expression = children.removeFirstOccurrence(Expression.class); this.branches = new ImmutableArray<>(children.collect(Branch.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } public Switch(PositionInfo pi, List c, Expression expr, @@ -86,6 +121,9 @@ public Switch(PositionInfo pi, List c, Expression expr, super(pi, c); this.expression = expr; this.branches = branches; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } @@ -204,6 +242,13 @@ public ImmutableArray getBranchList() { return branches; } + @Override + public SourceElement getFirstElement() { + if (branches.isEmpty()) + return this; + return branches.get(0); + } + /** * calls the corresponding method of a visitor in order to perform some action/transformation on * this element @@ -214,4 +259,65 @@ public ImmutableArray getBranchList() { public void visit(Visitor v) { v.performActionOnSwitch(this); } + + @Override + public boolean isPrefix() { + return !branches.isEmpty() && expressionWithoutSideffects(); + } + + @Override + public boolean hasNextPrefixElement() { + return !branches.isEmpty() && branches.get(0) instanceof PossibleProgramPrefix; + } + + @Override + public PossibleProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (PossibleProgramPrefix) branches.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() + ? ((PossibleProgramPrefix) branches.get(0)).getLastPrefixElement() + : this; + } + + @Override + public int getPrefixLength() { + return prefixLength; + } + + @Override + public MethodFrame getInnerMostMethodFrame() { + return innerMostMethodFrame; + } + + @Override + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(); + } + + /** + * The method checks whether the expression in the synchronized prefix is either a local + * variable or a meta class reference (as local variables of this type are not supported by KeY, + * see return value for {@link MetaClassReference#getKeYJavaType(Services, ExecutionContext)}. + * + * @return true iff the above stated condition holds. + */ + private boolean expressionWithoutSideffects() { + return (expression instanceof ProgramVariable && !((ProgramVariable) expression).isMember()) + || (expression instanceof MetaClassReference) || expression instanceof Literal; + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return branches.isEmpty() ? PosInProgram.TOP + : (expressionWithoutSideffects() + ? PosInProgram.ONE + : PosInProgram.TOP); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java new file mode 100644 index 00000000000..2b0a42694cd --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java @@ -0,0 +1,22 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.statement; + +import de.uka.ilkd.key.java.ast.PositionInfo; + +import org.key_project.util.ExtList; + +public abstract class SwitchBranch extends BranchImp { + public SwitchBranch() { + super(); + } + + public SwitchBranch(ExtList children) { + super(children); + } + + public SwitchBranch(ExtList children, PositionInfo pos) { + super(children, pos); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..155ac228e01 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java @@ -0,0 +1,59 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.statement; + +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.SourceData; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.rule.MatchConditions; + +public class SwitchBranchSVWrapper extends SwitchBranch { + private final ProgramSV sv; + + public SwitchBranchSVWrapper(ProgramSV sv) { + this.sv = sv; + } + + public ProgramSV getSv() { + return sv; + } + + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public void visit(Visitor v) { + + } + + @Override + public int getStatementCount() { + return 0; + } + + @Override + public Statement getStatementAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public String toString() { + return sv.toString(); + } + + @Override + public MatchConditions match(SourceData source, MatchConditions matchCond) { + return sv.match(source, matchCond); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java index cea5771d8ca..a1309fc80c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.java.ast.reference.MetaClassReference; 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.logic.op.ProgramVariable; import org.key_project.util.ExtList; @@ -23,7 +23,7 @@ */ public class SynchronizedBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { /** * Expression. @@ -103,22 +103,27 @@ public SynchronizedBlock(PositionInfo pi, List c, Expression expr, Stat this.prefixLength = prefixLength; } + @Override + public boolean isPrefix() { + return expressionWithoutSideffects(); + } + @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -133,8 +138,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java index 17b9c49a716..25a2db99ad5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.ast.*; 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 org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -21,7 +21,7 @@ * * @author AutoDoc */ -public class Try extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Try extends BranchStatement implements StatementContainer, PossibleProgramPrefix { private final StatementBlock body; private final ImmutableArray branches; @@ -110,20 +110,20 @@ public Try(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -138,8 +138,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index e79746808de..d03c483cef7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -363,6 +363,22 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + ExtList changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + PositionInfo pi = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pi = PositionInfo.UNDEFINED; + } + addChild(new ActiveCase(changeList, pi)); + changed(); + } else { + doDefaultAction(x); + } + } + // eee @Override public void performActionOnCase(Case x) { @@ -1227,13 +1243,22 @@ ProgramElement createNewElement(ExtList changeList) { @Override public void performActionOnSwitch(Switch x) { - DefaultAction def = new DefaultAction(x) { - @Override - ProgramElement createNewElement(ExtList changeList) { - return new Switch(changeList); + var changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + var pos = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pos = PositionInfo.UNDEFINED; } - }; - def.doAction(x); + Expression expr = changeList.removeFirstOccurrence(Expression.class); + var branches = changeList.collect(SwitchBranch.class); + changeList.clear(); + var sw = new Switch(pos, expr, branches); + addChild(sw); + changed(); + } else { + doDefaultAction(x); + } } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index fb6a24e4824..67be8213b18 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -268,6 +268,11 @@ public void performActionOnCase(Case x) { doDefaultAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + doDefaultAction(x); + } + @Override public void performActionOnCatch(Catch x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index 0b77f3cb88c..b96a51243ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java @@ -10,12 +10,7 @@ import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; -import de.uka.ilkd.key.java.ast.statement.Exec; -import de.uka.ilkd.key.java.ast.statement.LabeledStatement; -import de.uka.ilkd.key.java.ast.statement.LoopScopeBlock; -import de.uka.ilkd.key.java.ast.statement.MethodFrame; -import de.uka.ilkd.key.java.ast.statement.SynchronizedBlock; -import de.uka.ilkd.key.java.ast.statement.Try; +import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation; @@ -58,30 +53,36 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte if (!prefixPos.hasNext()) { body = createWrapperBody(context, putIn, suffix); - // special case labeled statement as a label must not be + // special case labeled statement as a label need not be // succeeded by a statement block if (context instanceof LabeledStatement) { body = createLabeledStatementWrapper((LabeledStatement) context, body); + } else if (context instanceof ActiveCase ac) { + body = createActiveCaseWrapper(ac, (StatementBlock) body); } return body; } else { body = wrap((JavaNonTerminalProgramElement) next, putIn, prefixPos, prefixDepth, prefix, suffix); - if (context instanceof StatementBlock) { - return createStatementBlockWrapper((StatementBlock) context, body); - } else if (context instanceof Try) { - return createTryStatementWrapper((StatementBlock) body, (Try) context); - } else if (context instanceof MethodFrame) { - return createMethodFrameWrapper((MethodFrame) context, (StatementBlock) body); - } else if (context instanceof LabeledStatement) { - return createLabeledStatementWrapper((LabeledStatement) context, body); - } else if (context instanceof LoopScopeBlock) { - return createLoopScopeBlockWrapper((LoopScopeBlock) context, (StatementBlock) body); - } else if (context instanceof SynchronizedBlock) { - return createSynchronizedBlockWrapper((SynchronizedBlock) context, + if (context instanceof StatementBlock block) { + return createStatementBlockWrapper(block, body); + } else if (context instanceof Try t) { + return createTryStatementWrapper(t, (StatementBlock) body); + } else if (context instanceof MethodFrame mf) { + return createMethodFrameWrapper(mf, (StatementBlock) body); + } else if (context instanceof LabeledStatement ls) { + return createLabeledStatementWrapper(ls, body); + } else if (context instanceof LoopScopeBlock lsb) { + return createLoopScopeBlockWrapper(lsb, (StatementBlock) body); + } else if (context instanceof SynchronizedBlock sb) { + return createSynchronizedBlockWrapper(sb, (StatementBlock) body); - } else if (context instanceof Exec) { - return createExecStatementWrapper((StatementBlock) body, (Exec) context); + } else if (context instanceof Exec e) { + return createExecStatementWrapper(e, (StatementBlock) body); + } else if (context instanceof Switch sw) { + return createSwitchWrapper(sw, (ActiveCase) body); + } else if (context instanceof ActiveCase ac) { + return createActiveCaseWrapper(ac, (Statement) body); } else { throw new RuntimeException( new UnexpectedException("Unexpected block type: " + context.getClass())); @@ -91,7 +92,7 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte /** * inserts the content of the statement block putIn and adds succeeding children of - * the innermost non terminal element (usually statement block) in the context. + * the innermost non-terminal element (usually statement block) in the context. * * @param wrapper * the JavaNonTerminalProgramElement with the context that has to be wrapped @@ -146,7 +147,7 @@ private final StatementBlock createWrapperBody(JavaNonTerminalProgramElement wra /** * Replaces the first statement in the wrapper block. The replacement is optimized as it just * returns the replacement block if it is the only child of the statement block to be - * constructed and the chld is a statementblock too. + * constructed and the child is a statementblock too. * * @param wrapper * the StatementBlock where to replace the first statement @@ -170,11 +171,31 @@ protected StatementBlock createStatementBlockWrapper(StatementBlock wrapper, } } - protected Try createTryStatementWrapper(StatementBlock body, Try old) { + protected Try createTryStatementWrapper(Try old, StatementBlock body) { return new Try(body, old.getBranchList()); } - protected Exec createExecStatementWrapper(StatementBlock body, Exec old) { + protected ActiveCase createActiveCaseWrapper(ActiveCase old, Statement body) { + var stmts = old.getBody().toArray(new Statement[0]); + if (body instanceof StatementBlock bodyBlock) { + if (stmts[0] instanceof StatementBlock sb && !sb.isEmpty()) { + stmts[0] = bodyBlock; + } else { + stmts = bodyBlock.getBody().toArray(new Statement[0]); + } + } else { + stmts[0] = body; + } + return new ActiveCase(stmts); + } + + protected Switch createSwitchWrapper(Switch old, ActiveCase body) { + var branches = old.getBranchList().toArray(new Branch[0]); + branches[0] = body; + return new Switch(old.getExpression(), branches); + } + + protected Exec createExecStatementWrapper(Exec old, StatementBlock body) { return new Exec(body, old.getBranchList()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index e5299c49298..fd8d71e6848 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -304,6 +304,8 @@ public interface Visitor { void performActionOnCase(Case x); + void performActionOnActiveCase(ActiveCase x); + void performActionOnCatch(Catch x); void performActionOnDefault(Default x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java index 65a00e3eeaf..4bf41d4d2de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java @@ -29,9 +29,9 @@ public MethodStackInfo(ProgramElement element) { */ public ImmutableList getMethodStack() { ImmutableList list = ImmutableSLList.nil(); - if (element instanceof ProgramPrefix) { - final ImmutableArray prefix = - ((ProgramPrefix) element).getPrefixElements(); + if (element instanceof PossibleProgramPrefix) { + final ImmutableArray prefix = + ((PossibleProgramPrefix) element).getPrefixElements(); for (int i = prefix.size() - 1; i >= 0; i--) { if (prefix.get(i) instanceof MethodFrame frame) { IProgramMethod method = frame.getProgramMethod(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java b/key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java similarity index 79% rename from key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java rename to key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java index 4ce2b84489b..c670be00847 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java @@ -12,7 +12,9 @@ * this interface is implemented by program elements that may be matched by the inactive program * prefix */ -public interface ProgramPrefix extends NonTerminalProgramElement { +public interface PossibleProgramPrefix extends NonTerminalProgramElement { + + default boolean isPrefix() { return true; } /** return true if there is a next prefix element */ boolean hasNextPrefixElement(); @@ -21,15 +23,15 @@ public interface ProgramPrefix extends NonTerminalProgramElement { * return the next prefix element if no next prefix element is available an * IndexOutOfBoundsException is thrown */ - ProgramPrefix getNextPrefixElement(); + PossibleProgramPrefix getNextPrefixElement(); /** return the last prefix element */ - ProgramPrefix getLastPrefixElement(); + PossibleProgramPrefix getLastPrefixElement(); /** * returns an array with all prefix elements starting at this element */ - ImmutableArray getPrefixElements(); + ImmutableArray getPrefixElements(); /** returns the position of the first active child */ PosInProgram getFirstActiveChildPos(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 4e644442ee7..4c4cf3ea95a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -225,7 +225,7 @@ public abstract class ProgramSVSort extends SortImpl { public static final ProgramSVSort ARRAYPOSTDECL = new ArrayPostDeclarationSort(); - public static final ProgramSVSort SWITCH = new SwitchSVSort(); + public static final ProgramSVSort SWITCH_BRANCH = new SwitchBranchSVSort(); public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE = new ConstantProgramVariableSort(new Name("ConstantPrimitiveTypeVariable"), false); @@ -1195,15 +1195,12 @@ protected boolean canStandFor(ProgramElement check, Services services) { } } - private static final class SwitchSVSort extends ProgramSVSort { - - public SwitchSVSort() { - super(new Name("Switch")); - } + private static final class SwitchBranchSVSort extends ProgramSVSort { + public SwitchBranchSVSort() { super(new Name("SwitchBranch")); } @Override protected boolean canStandFor(ProgramElement pe, Services services) { - return (pe instanceof Switch); + return (pe instanceof Case) || (pe instanceof Default); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 5551e134e2d..dbc771a6225 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -20,8 +20,8 @@ import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.ProgramPrefix; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -854,7 +854,8 @@ public void performActionOnClassInitializer(ClassInitializer x) { protected void performActionOnStatement(SourceElement s) { layouter.beginRelativeC(0); - boolean validStatement = !(s instanceof CatchAllStatement || s instanceof ProgramPrefix + boolean validStatement = !(s instanceof CatchAllStatement + || (s instanceof PossibleProgramPrefix pre && pre.isPrefix()) || s instanceof TypeDeclarationContainer); if (validStatement) { markStart(s); @@ -1779,6 +1780,16 @@ public void performActionOnDefault(Default x) { printCaseBody(x.getBody()); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + if (!x.isPrefix()) + markStart(x); + layouter.keyWord("active-case").print(":"); + printCaseBody(x.getBody()); + if (!x.isPrefix()) + markEnd(x); + } + @Override public void performActionOnFinally(Finally x) { layouter.print(" "); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index 81f41480bb1..c47de939af7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.java.ast.SourceElement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.LocationVariable; @@ -192,7 +192,7 @@ public static SourceElement computeActiveStatement(SourceElement firstStatement) // TODO: unify with MiscTools getActiveStatement if (firstStatement != null) { activeStatement = firstStatement; - while ((activeStatement instanceof ProgramPrefix) + while ((activeStatement instanceof PossibleProgramPrefix pre && pre.isPrefix()) && !(activeStatement instanceof StatementBlock)) { activeStatement = activeStatement.getFirstElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java index 2e2124aa46e..c3b62f01182 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.*; @@ -318,7 +318,7 @@ private ImmutableList getJavaTacletList( HashMap> map, ProgramElement pe, PrefixOccurrences prefixOccurrences) { ImmutableList res = ImmutableSLList.nil(); - if (pe instanceof ProgramPrefix nt) { + if (pe instanceof PossibleProgramPrefix nt) { int next = prefixOccurrences.occurred(pe); if (next < nt.getChildCount()) { return getJavaTacletList(map, nt.getChildAt(next), prefixOccurrences); @@ -583,7 +583,8 @@ private static class PrefixOccurrences { */ static final Class[] prefixClasses = new Class[] { StatementBlock.class, LabeledStatement.class, Try.class, - MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class }; + MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class, + Switch.class, ActiveCase.class }; /** * number of prefix types @@ -599,7 +600,7 @@ private static class PrefixOccurrences { * fields to indicate the position of the next relevant child (the next possible prefix * element or real statement */ - static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0 }; + static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0, 1, 0 }; PrefixOccurrences() { reset(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index 790dafb48d8..1379fd756db 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Goal; @@ -291,7 +291,8 @@ private static ExecutionContext extractExecutionContext(final MethodFrame frame) private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract( final JModality modality, final Goal goal) { SourceElement element = modality.programBlock().program().getFirstElement(); - while ((element instanceof ProgramPrefix || element instanceof CatchAllStatement) + while ((element instanceof PossibleProgramPrefix pre && pre.isPrefix() + || element instanceof CatchAllStatement) && !(element instanceof StatementBlock && ((StatementBlock) element).isEmpty())) { if (element instanceof StatementBlock && hasApplicableContracts(services, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index 9a1a248c4e6..9056d54686f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -19,7 +19,7 @@ import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; @@ -407,7 +407,7 @@ private Pair, Statement> findLoopLabel( Optional