From 9e98143d43ffd4f122d63c11ae17f6acb730ded9 Mon Sep 17 00:00:00 2001 From: Drodt Date: Tue, 12 Mar 2024 15:23:49 +0100 Subject: [PATCH 1/8] Modify switch rule; add active-case syntax element --- .../uka/ilkd/key/java/KeYJavaASTFactory.java | 33 +-- .../ilkd/key/java/Recoder2KeYConverter.java | 2 +- .../key/java/SchemaRecoder2KeYConverter.java | 5 + .../ilkd/key/java/recoderext/ActiveCase.java | 206 ++++++++++++++++++ .../recoderext/SchemaJavaProgramFactory.java | 4 + .../recoderext/SourceVisitorExtended.java | 4 + .../ilkd/key/java/statement/ActiveCase.java | 122 +++++++++++ .../de/uka/ilkd/key/java/statement/Case.java | 2 +- .../uka/ilkd/key/java/statement/Default.java | 2 +- .../uka/ilkd/key/java/statement/Switch.java | 10 +- .../ilkd/key/java/statement/SwitchBranch.java | 18 ++ .../key/java/visitor/CreatingASTVisitor.java | 11 + .../ilkd/key/java/visitor/JavaASTVisitor.java | 5 + .../key/java/visitor/ProgramContextAdder.java | 26 +-- .../de/uka/ilkd/key/java/visitor/Visitor.java | 2 + .../ilkd/key/logic/sort/ProgramSVSort.java | 20 +- .../de/uka/ilkd/key/pp/PrettyPrinter.java | 6 + .../key/rule/metaconstruct/SwitchToIf.java | 4 +- .../key/parser/schemajava/SchemaJavaParser.jj | 10 + .../de/uka/ilkd/key/proof/rules/javaRules.key | 14 +- .../gui/nodeviews/HTMLSyntaxHighlighter.java | 2 +- .../java/recoder/java/statement/Case.java | 17 +- .../java/recoder/java/statement/Default.java | 12 +- .../java/recoder/java/statement/Switch.java | 6 +- .../recoder/java/statement/SwitchBranch.java | 33 +++ 25 files changed, 477 insertions(+), 99 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java create mode 100644 recoder/src/main/java/recoder/java/statement/SwitchBranch.java 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 2473def2307..dfa43620471 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 @@ -31,36 +31,7 @@ import de.uka.ilkd.key.java.reference.ThisReference; import de.uka.ilkd.key.java.reference.TypeRef; import de.uka.ilkd.key.java.reference.TypeReference; -import de.uka.ilkd.key.java.statement.Branch; -import de.uka.ilkd.key.java.statement.Break; -import de.uka.ilkd.key.java.statement.Case; -import de.uka.ilkd.key.java.statement.Catch; -import de.uka.ilkd.key.java.statement.Continue; -import de.uka.ilkd.key.java.statement.Default; -import de.uka.ilkd.key.java.statement.Do; -import de.uka.ilkd.key.java.statement.Else; -import de.uka.ilkd.key.java.statement.EmptyStatement; -import de.uka.ilkd.key.java.statement.EnhancedFor; -import de.uka.ilkd.key.java.statement.Finally; -import de.uka.ilkd.key.java.statement.For; -import de.uka.ilkd.key.java.statement.ForUpdates; -import de.uka.ilkd.key.java.statement.Guard; -import de.uka.ilkd.key.java.statement.IForUpdates; -import de.uka.ilkd.key.java.statement.IGuard; -import de.uka.ilkd.key.java.statement.ILoopInit; -import de.uka.ilkd.key.java.statement.If; -import de.uka.ilkd.key.java.statement.LabeledStatement; -import de.uka.ilkd.key.java.statement.LoopInit; -import de.uka.ilkd.key.java.statement.MethodBodyStatement; -import de.uka.ilkd.key.java.statement.MethodFrame; -import de.uka.ilkd.key.java.statement.Return; -import de.uka.ilkd.key.java.statement.Switch; -import de.uka.ilkd.key.java.statement.SynchronizedBlock; -import de.uka.ilkd.key.java.statement.Then; -import de.uka.ilkd.key.java.statement.Throw; -import de.uka.ilkd.key.java.statement.TransactionStatement; -import de.uka.ilkd.key.java.statement.Try; -import de.uka.ilkd.key.java.statement.While; +import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.VariableNamer; import de.uka.ilkd.key.logic.op.IProgramMethod; @@ -2333,7 +2304,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) { final Switch block = new Switch(expression, branches); return block; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 6da669c3ea4..1760b88a966 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -382,7 +382,7 @@ private ExtList collectChildrenAndComments(recoder.java.ProgramElement pe) { * @param se the sourcelement to extract from, not null * @return the newly created PositionInfo */ - private PositionInfo positionInfo(recoder.java.SourceElement se) { + protected PositionInfo positionInfo(recoder.java.SourceElement se) { var relPos = se.getRelativePosition(); var startPos = Position.fromSEPosition(se.getStartPosition()); var endPos = Position.fromSEPosition(se.getEndPosition()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 1b0a1f4c1bc..abd70e58020 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -202,6 +202,11 @@ public MethodBodyStatement convert(de.uka.ilkd.key.java.recoderext.RMethodBodySt return new MethodBodyStatement(tr, resVar, convert(l.getMethodReference())); } + public ActiveCase convert(de.uka.ilkd.key.java.recoderext.ActiveCase ac) { + ExtList children = collectChildren(ac); + return new ActiveCase(children, positionInfo(ac)); + } + /** * translate Context statement blocks */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java new file mode 100644 index 00000000000..7d73379f8f1 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java @@ -0,0 +1,206 @@ +package de.uka.ilkd.key.java.recoderext; + +import recoder.java.*; +import recoder.java.statement.EmptyStatement; +import recoder.java.statement.SwitchBranch; +import recoder.list.generic.ASTList; + +public class ActiveCase extends SwitchBranch { + /** + * serialization id + */ + private static final long serialVersionID = /*TODO*/ 0; + + /** + * Body. + */ + protected ASTList body; + + /** + * ActiveCase. + */ + public ActiveCase() { + super(); + } + + /** + * ActiveCase. + */ + public ActiveCase(ASTList body) { + setBody(body); + makeParentRoleValid(); + } + + /** + * Case. + * + * @param proto a case. + */ + + protected ActiveCase(ActiveCase proto) { + super(proto); + if (proto.body != null) { + body = proto.body.deepClone(); + } + makeParentRoleValid(); + } + + /** + * Deep clone. + * + * @return the object. + */ + + public ActiveCase deepClone() { + return new ActiveCase(this); + } + + /** + * Make parent role valid. + */ + + public void makeParentRoleValid() { + super.makeParentRoleValid(); + if (body != null) { + for (Statement statement : body) { + statement.setStatementContainer(this); + } + } + } + + /** + * 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 + * @throws 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); + } + index -= len; + } + throw new ArrayIndexOutOfBoundsException(); + } + + public int getChildPositionCode(ProgramElement child) { + // role 0 (IDX): body + if (body != null) { + int index = body.indexOf(child); + if (index >= 0) { + return (index << 4); + } + } + return -1; + } + + /** + * Replace a single child in the current node. The child to replace is matched by identity and + * hence must be known exactly. The replacement element can be null - in that case, the child is + * effectively removed. The parent role of the new child is validated, while the parent link of + * the replaced child is left untouched. + * + * @param p the old child. + * @param q the new child. + * @return true if a replacement has occured, false otherwise. + * @throws ClassCastException if the new child cannot take over the role of the old one. + */ + + public boolean replaceChild(ProgramElement p, ProgramElement q) { + int count; + if (p == null) { + throw new NullPointerException(); + } + count = (body == null) ? 0 : body.size(); + for (int i = 0; i < count; i++) { + if (body.get(i) == p) { + if (q == null) { + body.remove(i); + } else { + Statement r = (Statement) q; + body.set(i, r); + r.setStatementContainer(this); + } + return true; + } + } + return false; + } + + /** + * 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 ASTList getBody() { + return body; + } + + /** + * Set body. + * + * @param list a statement mutable list. + */ + + public void setBody(ASTList list) { + body = list; + } + + public void accept(SourceVisitor v) { + if (v instanceof SourceVisitorExtended e) { + e.visitActiveCase(this); + } else { + throw new IllegalStateException( + "Method 'accept' not implemented in " + "ActiveCase"); + } + } + + public SourceElement getLastElement() { + if (body == null || body.size() == 0) { + return this; + } + return body.get(body.size() - 1).getLastElement(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java index a66418df167..945efd28101 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java @@ -121,6 +121,10 @@ public MergePointStatement createMergePointStatement(Expression e) { return new MergePointStatement(e); } + public ActiveCase createActiveCase() { + return new ActiveCase(); + } + /** * Create a {@link PassiveExpression}. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java index 52f3c417cc9..a05e76ed200 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java @@ -13,6 +13,10 @@ */ public class SourceVisitorExtended extends SourceVisitor { + public void visitActiveCase(ActiveCase x) { + // default do nothing + } + public void visitCatchAll(CatchAllStatement x) { // default do nothing } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java new file mode 100644 index 00000000000..b255b0ab4ac --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java @@ -0,0 +1,122 @@ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.PositionInfo; +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.visitor.Visitor; +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableArray; + +public class ActiveCase extends SwitchBranch { + /** + * Body. + */ + protected final ImmutableArray body; + + public ActiveCase() { + this.body = null; + } + + public ActiveCase(Statement[] body) { + this.body = new ImmutableArray<>(body); + } + + /** + * 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)); + } + + /** + * 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)); + } + + /** + * 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(); + } + + /** + * 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); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java index c1c9535b626..de361fb1c14 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java @@ -13,7 +13,7 @@ * Case. * */ -public class Case extends BranchImp implements ExpressionContainer { +public class Case extends SwitchBranch implements ExpressionContainer { /** * Expression. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java index 6536464ed76..55612a1dbc9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java @@ -14,7 +14,7 @@ * Default. * */ -public class Default extends BranchImp { +public class Default extends SwitchBranch { /** * Body. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java index 3816e6f9282..679959831da 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java @@ -20,7 +20,7 @@ public class Switch extends BranchStatement * Branches. */ - protected final ImmutableArray branches; + protected final ImmutableArray branches; /** * Expression. @@ -57,7 +57,7 @@ public Switch(Expression e) { * @param branches a branch array */ - public Switch(Expression e, Branch[] branches) { + public Switch(Expression e, SwitchBranch[] branches) { this.branches = new ImmutableArray<>(branches); this.expression = e; } @@ -71,7 +71,7 @@ public Switch(Expression e, Branch[] branches) { public Switch(ExtList children) { super(children); this.expression = children.get(Expression.class); - this.branches = new ImmutableArray<>(children.collect(Branch.class)); + this.branches = new ImmutableArray<>(children.collect(SwitchBranch.class)); } @@ -171,7 +171,7 @@ public int getBranchCount() { * @exception ArrayIndexOutOfBoundsException if index is out of bounds. */ - public Branch getBranchAt(int index) { + public SwitchBranch getBranchAt(int index) { if (branches != null) { return branches.get(index); } @@ -184,7 +184,7 @@ public Branch getBranchAt(int index) { * * @return the array wrapper of the branches */ - public ImmutableArray getBranchList() { + public ImmutableArray getBranchList() { return branches; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java new file mode 100644 index 00000000000..574f9f138c4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java @@ -0,0 +1,18 @@ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.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/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index 65b0d55d833..00d3528ec92 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 @@ -358,6 +358,17 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new ActiveCase(changeList); + } + }; + def.doAction(x); + } + // eee @Override public void performActionOnCase(Case x) { 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 ea6541b536f..40bad726f29 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 @@ -261,6 +261,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 589b1cb9d4d..ce574d5c9fa 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 @@ -68,18 +68,18 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte } 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((StatementBlock) body, t); + } 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); @@ -144,7 +144,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 * @param replacement the StatementBlock that replaces the first statement of the block 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 c6c6af93afa..4f95f12591a 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 @@ -300,6 +300,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/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 3f1c22dbb25..421fdeecd4c 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 @@ -31,14 +31,7 @@ import de.uka.ilkd.key.java.expression.operator.NewArray; import de.uka.ilkd.key.java.expression.operator.adt.*; import de.uka.ilkd.key.java.reference.*; -import de.uka.ilkd.key.java.statement.Catch; -import de.uka.ilkd.key.java.statement.Ccatch; -import de.uka.ilkd.key.java.statement.For; -import de.uka.ilkd.key.java.statement.ForUpdates; -import de.uka.ilkd.key.java.statement.Guard; -import de.uka.ilkd.key.java.statement.LoopInit; -import de.uka.ilkd.key.java.statement.MethodBodyStatement; -import de.uka.ilkd.key.java.statement.Switch; +import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.Namespace; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; @@ -253,6 +246,8 @@ public abstract class ProgramSVSort extends SortImpl { public static final ProgramSVSort SWITCH = new SwitchSVSort(); + public static final ProgramSVSort SWITCH_CASE = new SwitchCaseSVSort(); + public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE = new ConstantProgramVariableSort(new Name("ConstantPrimitiveTypeVariable"), false); @@ -1233,6 +1228,15 @@ protected boolean canStandFor(ProgramElement pe, Services services) { } } + private static final class SwitchCaseSVSort extends ProgramSVSort { + public SwitchCaseSVSort() { super(new Name("SwitchCase"));} + + @Override + protected boolean canStandFor(ProgramElement pe, Services services) { + return (pe instanceof Case) || (pe instanceof Default); + } + } + private static final class MultipleVariableDeclarationSort extends ProgramSVSort { public MultipleVariableDeclarationSort() { 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 bcf1e0932ea..f6cb84a28eb 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 @@ -1741,6 +1741,12 @@ public void performActionOnDefault(Default x) { printCaseBody(x.getBody()); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + l.keyWord("active-case").print(":"); + printCaseBody(x.getBody()); + } + @Override public void performActionOnFinally(Finally x) { l.print(" "); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java index a5b3b90f827..fc3e6d16354 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java @@ -131,9 +131,9 @@ private If mkIfNullCheck(Services services, ProgramVariable var, Statement elseB */ private Switch changeBreaks(Switch sw, Break b) { int n = sw.getBranchCount(); - Branch[] branches = new Branch[n]; + SwitchBranch[] branches = new SwitchBranch[n]; for (int i = 0; i < n; i++) { - branches[i] = (Branch) recChangeBreaks(sw.getBranchAt(i), b); + branches[i] = (SwitchBranch) recChangeBreaks(sw.getBranchAt(i), b); } return KeYJavaASTFactory.switchBlock(sw.getExpression(), branches); } diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj index ad2080d6403..c3f92232190 100644 --- a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj +++ b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj @@ -4001,6 +4001,8 @@ Switch SwitchStatement() : { if (branch instanceof Case) { ((Case)branch).setBody(stats); + } else if (branch instanceof ActiveCase) { + ((ActiveCase) branch).setBody(stats); } else { ((Default)branch).setBody(stats); } @@ -4044,6 +4046,14 @@ Branch SwitchLabel() : { result = factory.createDefault(); setPrefixInfo(result); + } + ":" + ) + | + ( "active-case" + { + result = factory.createActiveCase(); + setPrefixInfo(result); } ":" ) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 0c8a422441c..a4482ae8773 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -66,6 +66,7 @@ \program [list] Expression #elist; \program [list] SimpleExpression #selist; \program [list] Catch #cs; + \program [list] SwitchCase #cases; \program Switch #sw; \program Label #lb, #lb0, #lb1, #innerLabel, #outerLabel; @@ -1402,10 +1403,15 @@ // --------------- switch-statements ------------------------------------------// - switch { - \find(\modality{#allmodal}{.. #sw ...}\endmodality (post)) - \replacewith(\modality{#allmodal}{.. #switch-to-if(#sw) ...}\endmodality (post)) - \heuristics(simplify_prog) + //switch { + // \find(\modality{#allmodal}{.. #sw ...}\endmodality (post)) + // \replacewith(\modality{#allmodal}{.. #switch-to-if(#sw) ...}\endmodality (post)) + // \heuristics(simplify_prog) + //}; + + switchDefault { + \find(\modality{#allmodal}{.. switch (#se) {default: #slist} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist} ...}\endmodality (post)) }; // --------------- labels and blocks ------------------------------------------// diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java index 60e39e626d3..e0bf2b50a76 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java @@ -92,7 +92,7 @@ public class HTMLSyntaxHighlighter { "char", "long", "short", "byte", "\\Qmethod-frame\\E", "\\Qloop-scope\\E", "boolean", "exec", "ccatch", "\\Q\\Return\\E", "\\Q\\Break\\E", "\\Q\\Continue\\E", "final", - "volatile", "assert", "default" }; + "volatile", "assert", "default", "\\Qactive-case\\E" }; public final static String JAVA_KEYWORDS_REGEX = concat("|", Arrays.asList(JAVA_KEYWORDS)); diff --git a/recoder/src/main/java/recoder/java/statement/Case.java b/recoder/src/main/java/recoder/java/statement/Case.java index 4b1038841ac..8c5efaba445 100644 --- a/recoder/src/main/java/recoder/java/statement/Case.java +++ b/recoder/src/main/java/recoder/java/statement/Case.java @@ -13,7 +13,7 @@ * @author AutoDoc */ -public class Case extends Branch implements ExpressionContainer { +public class Case extends SwitchBranch implements ExpressionContainer { /** * serialization id @@ -107,21 +107,6 @@ public void makeParentRoleValid() { } } - @Override - public Switch getParent() { - return (Switch) parent; - } - - /** - * Set parent. - * - * @param parent a switch. - */ - - public void setParent(Switch parent) { - this.parent = parent; - } - /** * Returns the number of children of this node. * diff --git a/recoder/src/main/java/recoder/java/statement/Default.java b/recoder/src/main/java/recoder/java/statement/Default.java index ba7fd371277..c8df334d1c7 100644 --- a/recoder/src/main/java/recoder/java/statement/Default.java +++ b/recoder/src/main/java/recoder/java/statement/Default.java @@ -16,7 +16,7 @@ * @author AutoDoc */ -public class Default extends Branch { +public class Default extends SwitchBranch { /** * serialization id @@ -71,16 +71,6 @@ public Default deepClone() { return new Default(this); } - /** - * Set parent. - * - * @param parent a switch. - */ - - public void setParent(Switch parent) { - this.parent = parent; - } - /** * Make parent role valid. */ diff --git a/recoder/src/main/java/recoder/java/statement/Switch.java b/recoder/src/main/java/recoder/java/statement/Switch.java index d4a9c582ad6..4a6c76bb177 100644 --- a/recoder/src/main/java/recoder/java/statement/Switch.java +++ b/recoder/src/main/java/recoder/java/statement/Switch.java @@ -182,11 +182,7 @@ public void makeParentRoleValid() { if (branches != null) { for (int i = branches.size() - 1; i >= 0; i -= 1) { Branch b = branches.get(i); - if (b instanceof Case) { - ((Case) b).setParent(this); - } else { - ((Default) b).setParent(this); - } + ((SwitchBranch) b).setParent(this); } } } diff --git a/recoder/src/main/java/recoder/java/statement/SwitchBranch.java b/recoder/src/main/java/recoder/java/statement/SwitchBranch.java new file mode 100644 index 00000000000..78e0137784e --- /dev/null +++ b/recoder/src/main/java/recoder/java/statement/SwitchBranch.java @@ -0,0 +1,33 @@ +package recoder.java.statement; + +public abstract class SwitchBranch extends Branch { + + public SwitchBranch() { + super(); + } + + /** + * Branch. + * + * @param proto a branch. + */ + + protected SwitchBranch(SwitchBranch proto) { + super(proto); + } + + @Override + public Switch getParent() { + return (Switch) parent; + } + + /** + * Set parent. + * + * @param parent a switch. + */ + + public void setParent(Switch parent) { + this.parent = parent; + } +} From cbcdcf2e702b2c8e986d86d4eb6ac4cdf0b7b2e6 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 14 Mar 2024 09:06:55 +0100 Subject: [PATCH 2/8] More Switch rules; extend parser --- .../key/java/SchemaRecoder2KeYConverter.java | 5 +- .../de/uka/ilkd/key/java/StatementBlock.java | 4 +- .../ilkd/key/java/recoderext/ActiveCase.java | 7 +- .../recoderext/SchemaJavaProgramFactory.java | 8 ++ .../recoderext/SwitchBranchSVWrapper.java | 74 +++++++++++++++++++ .../ilkd/key/java/statement/ActiveCase.java | 66 ++++++++++++++++- .../de/uka/ilkd/key/java/statement/Exec.java | 2 +- .../key/java/statement/LabeledStatement.java | 4 +- .../key/java/statement/LoopScopeBlock.java | 2 +- .../ilkd/key/java/statement/MethodFrame.java | 2 +- .../uka/ilkd/key/java/statement/Switch.java | 56 +++++++++++++- .../ilkd/key/java/statement/SwitchBranch.java | 4 + .../key/java/statement/SynchronizedBlock.java | 2 +- .../de/uka/ilkd/key/java/statement/Try.java | 2 +- .../ilkd/key/logic/sort/ProgramSVSort.java | 6 +- .../de/uka/ilkd/key/proof/TacletIndex.java | 5 +- .../key/parser/schemajava/SchemaJavaParser.jj | 18 ++++- .../de/uka/ilkd/key/proof/rules/javaRules.key | 53 +++++++++++-- .../recoder/java/statement/SwitchBranch.java | 4 + 19 files changed, 293 insertions(+), 31 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index abd70e58020..6caff0b9fba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -270,12 +270,15 @@ public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.CcatchSVWrapper sv } public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.ProgramVariableSVWrapper svw) { + return svw.getSV(); + } + public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { return svw.getSV(); } /** - * for some reason the this and super references have to be treated differently here. + * for some reason the {@code this} and {@code super} references have to be treated differently here. */ @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java index 6d0c95695c8..9b882eb5812 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java @@ -86,7 +86,7 @@ public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) { /** computes the prefix elements for the given array of statment block */ public static ImmutableArray computePrefixElements( - ImmutableArray b, ProgramPrefix current) { + ProgramPrefix current) { final ArrayList prefix = new ArrayList<>(); prefix.add(current); @@ -272,7 +272,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return computePrefixElements(body, this); + return computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java index 7d73379f8f1..75510a8957a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java @@ -1,3 +1,6 @@ +/* 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.recoderext; import recoder.java.*; @@ -9,7 +12,7 @@ public class ActiveCase extends SwitchBranch { /** * serialization id */ - private static final long serialVersionID = /*TODO*/ 0; + private static final long serialVersionID = /* TODO */ 0; /** * Body. @@ -193,7 +196,7 @@ public void accept(SourceVisitor v) { e.visitActiveCase(this); } else { throw new IllegalStateException( - "Method 'accept' not implemented in " + "ActiveCase"); + "Method 'accept' not implemented in " + "ActiveCase"); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java index 945efd28101..738105894a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java @@ -244,6 +244,14 @@ public CcatchSVWrapper getCcatchSV(String s) throws ParseException { return new CcatchSVWrapper(sv); } + public SwitchBranchSVWrapper getSwitchBranchSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "SwitchCase"); + } + return new SwitchBranchSVWrapper(sv); + } + /** * For internal reuse and synchronization. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..d97b30f723c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java @@ -0,0 +1,74 @@ +package de.uka.ilkd.key.java.recoderext; + +import de.uka.ilkd.key.logic.op.SchemaVariable; +import recoder.java.ProgramElement; +import recoder.java.SourceVisitor; +import recoder.java.Statement; +import recoder.java.statement.SwitchBranch; + +public class SwitchBranchSVWrapper extends SwitchBranch implements KeYRecoderExtension, SVWrapper { + private static final long serialVersionUID = -1; + protected SchemaVariable sv; + + public SwitchBranchSVWrapper(SchemaVariable sv) { + this.sv = sv; + } + + /** + * sets the schema variable of sort statement + * + * @param sv the SchemaVariable + */ + @Override + public void setSV(SchemaVariable sv) { + this.sv = sv; + } + + /** + * returns a String name of this meta construct. + */ + @Override + public SchemaVariable getSV() { + return sv; + } + + @Override + public void accept(SourceVisitor v) { + + } + + public SwitchBranchSVWrapper deepClone() { + return new SwitchBranchSVWrapper(sv); + } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public int getChildPositionCode(ProgramElement child) { + return 0; + } + + @Override + public boolean replaceChild(ProgramElement p, ProgramElement q) { + return false; + } + + @Override + public int getStatementCount() { + return 0; + } + + @Override + public Statement getStatementAt(int index) { + throw new IndexOutOfBoundsException(); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java index b255b0ab4ac..ab3ed1d5267 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java @@ -1,24 +1,37 @@ +/* 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.statement; -import de.uka.ilkd.key.java.PositionInfo; -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.ProgramPrefix; + import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; -public class ActiveCase extends SwitchBranch { +public class ActiveCase extends SwitchBranch implements ProgramPrefix { /** * 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(); } /** @@ -30,6 +43,9 @@ public ActiveCase(Statement[] body) { 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(); } /** @@ -44,6 +60,9 @@ public ActiveCase(ExtList children) { 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(); } /** @@ -119,4 +138,43 @@ public ImmutableArray getBody() { public void visit(Visitor v) { v.performActionOnActiveCase(this); } + + @Override + public boolean hasNextPrefixElement() { + return body != null && !body.isEmpty() && body.get(0) instanceof ProgramPrefix; + } + + @Override + public ProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (ProgramPrefix) body.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public ProgramPrefix 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/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java index 32774cb8f19..e7d1e02d664 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java @@ -121,7 +121,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java index 7a8fffc97ca..16323cab7b5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java @@ -128,9 +128,9 @@ public ProgramPrefix getLastPrefixElement() { @Override public ImmutableArray getPrefixElements() { if (body instanceof StatementBlock) { - return StatementBlock.computePrefixElements(((StatementBlock) body).getBody(), this); + return StatementBlock.computePrefixElements(this); } else if (body instanceof ProgramPrefix) { - return StatementBlock.computePrefixElements(new ImmutableArray<>(body), this); + return StatementBlock.computePrefixElements(this); } return new ImmutableArray<>(this); } 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 index 90b373e1438..d8c4744ce57 100644 --- 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 @@ -101,7 +101,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } @Override 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 index ede5682ff23..c0e1040163c 100644 --- 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 @@ -121,7 +121,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } public PosInProgram getFirstActiveChildPos() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java index 679959831da..69ef54ed8bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java @@ -5,6 +5,8 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.ProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -14,7 +16,7 @@ */ public class Switch extends BranchStatement - implements ExpressionContainer, VariableScope, TypeScope { + implements ExpressionContainer, VariableScope, TypeScope, ProgramPrefix { /** * Branches. @@ -28,7 +30,9 @@ public class Switch extends BranchStatement protected final Expression expression; + private final int prefixLength; + private final MethodFrame innerMostMethodFrame; /** * Switch. @@ -37,6 +41,8 @@ public class Switch extends BranchStatement public Switch() { this.branches = null; this.expression = null; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -48,6 +54,8 @@ public Switch() { public Switch(Expression e) { this.branches = null; this.expression = e; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -60,6 +68,9 @@ public Switch(Expression e) { public Switch(Expression e, SwitchBranch[] branches) { this.branches = new ImmutableArray<>(branches); this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } /** @@ -72,6 +83,9 @@ public Switch(ExtList children) { super(children); this.expression = children.get(Expression.class); this.branches = new ImmutableArray<>(children.collect(SwitchBranch.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } @@ -197,4 +211,44 @@ public ImmutableArray getBranchList() { public void visit(Visitor v) { v.performActionOnSwitch(this); } + + @Override + public boolean hasNextPrefixElement() { + return !branches.isEmpty() && branches.get(0) instanceof ProgramPrefix; + } + + @Override + public ProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (ProgramPrefix) branches.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public ProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? ((ProgramPrefix) branches.get(0)).getLastPrefixElement() + : this; + } + + @Override + public int getPrefixLength() { + return prefixLength; + } + + @Override + public MethodFrame getInnerMostMethodFrame() { + return innerMostMethodFrame; + } + + @Override + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return branches.isEmpty() ? PosInProgram.TOP : PosInProgram.ZERO; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java index 574f9f138c4..71c9e3a538d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java @@ -1,6 +1,10 @@ +/* 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.statement; import de.uka.ilkd.key.java.PositionInfo; + import org.key_project.util.ExtList; public abstract class SwitchBranch extends BranchImp { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java index 492cfc5b683..0ee1cd5d2a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java @@ -117,7 +117,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } /** 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 index 9011234e233..8bafec72a74 100644 --- 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 @@ -127,7 +127,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } 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 421fdeecd4c..773c472e275 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 @@ -246,7 +246,7 @@ public abstract class ProgramSVSort extends SortImpl { public static final ProgramSVSort SWITCH = new SwitchSVSort(); - public static final ProgramSVSort SWITCH_CASE = new SwitchCaseSVSort(); + public static final ProgramSVSort SWITCH_CASE = new SwitchBranchSVSort(); public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE = new ConstantProgramVariableSort(new Name("ConstantPrimitiveTypeVariable"), false); @@ -1228,8 +1228,8 @@ protected boolean canStandFor(ProgramElement pe, Services services) { } } - private static final class SwitchCaseSVSort extends ProgramSVSort { - public SwitchCaseSVSort() { super(new Name("SwitchCase"));} + private static final class SwitchBranchSVSort extends ProgramSVSort { + public SwitchBranchSVSort() { super(new Name("SwitchBranch")); } @Override protected boolean canStandFor(ProgramElement pe, Services services) { 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 8778f5a217b..5c2d97d2a93 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 @@ -558,7 +558,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 @@ -574,7 +575,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 = new int[] { 0, 1, 0, 1, 1, 1, 0 }; + static final int[] nextChild = new int[] { 0, 1, 0, 1, 1, 1, 0, 1, 0 }; PrefixOccurrences() { reset(); diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj index c3f92232190..82b2f0f4c3d 100644 --- a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj +++ b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj @@ -2359,7 +2359,6 @@ ExpressionSVWrapper ExpressionSV() : } } - CatchSVWrapper CatchSV() : { } @@ -2380,6 +2379,16 @@ CcatchSVWrapper CcatchSV() : } } +SwitchBranchSVWrapper SwitchBranchSV() : +{ +} +{ + + { + return factory.getSwitchBranchSV(token.image); + } +} + Assignment AssignmentOperator() : { Assignment result; @@ -3988,6 +3997,10 @@ Switch SwitchStatement() : } "(" expr = Expression() ")" "{" + ( + { SwitchBranchSVWrapper sbsv; } sbsv=SwitchBranchSV() + { branches.add(sbsv); } + | ( branch = SwitchLabel() { stats = new ASTArrayList(); @@ -4008,7 +4021,8 @@ Switch SwitchStatement() : } branches.add(branch); } - )* + ) + )* "}" diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index a4482ae8773..daef7efdf1e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -66,7 +66,7 @@ \program [list] Expression #elist; \program [list] SimpleExpression #selist; \program [list] Catch #cs; - \program [list] SwitchCase #cases; + \program [list] SwitchBranch #cases; \program Switch #sw; \program Label #lb, #lb0, #lb1, #innerLabel, #outerLabel; @@ -1402,18 +1402,57 @@ // --------------- switch-statements ------------------------------------------// - - //switch { - // \find(\modality{#allmodal}{.. #sw ...}\endmodality (post)) - // \replacewith(\modality{#allmodal}{.. #switch-to-if(#sw) ...}\endmodality (post)) - // \heuristics(simplify_prog) - //}; + switchUnfold { + \find(\modality{#allmodal}{.. switch (#nse) {#cases} ...}\endmodality (post)) + \varcond(\newTypeOf(#v0, #nse)) + \replacewith(\modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; switch (#se) {#cases} ...}\endmodality (post)) + }; switchDefault { \find(\modality{#allmodal}{.. switch (#se) {default: #slist} ...}\endmodality (post)) \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist} ...}\endmodality (post)) }; + emptySwitch { + \find(\modality{#allmodal}{.. switch (#se) {active-case:} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. ...}\endmodality (post)) + }; + + switchReturnNoValue { + \find(\modality{#allmodal}{.. switch (#se) {active-case: return; #slist} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. return; ...}\endmodality (post)) + }; + + switchReturn { + \find(\modality{#allmodal}{.. switch (#se) {active-case: return #se0; #slist} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. return #se0; ...}\endmodality (post)) + }; + + switchCase { + \find(==> \modality{#allmodal}{.. switch (#se) {case #se0: #slist #cases} ...}\endmodality (post)) + "#se equals #se0": + \replacewith(==> \modality{#allmodal}{.. switch (#se) {active-case: #slist #cases} ...}\endmodality (post)) \add(#se = #se0 ==>); + "#se not equals #se0": + \replacewith(==> \modality{#allmodal}{.. switch (#se) {#cases} ...}\endmodality (post)) \add(!(#se = #se0) ==>) + }; + + switchFallThrough { + \find(\modality{#allmodal}{.. switch (#se) {active-case: case #se0: #slist #cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist #cases} ...}\endmodality (post)) + }; + + switchFallThroughDefault { + \find(\modality{#allmodal}{.. switch (#se) {active-case: default: #slist} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist} ...}\endmodality (post)) + }; + + switchBreak { + \find(\modality{#allmodal}{.. switch (#se) {active-case: break; #slist #cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. ...}\endmodality (post)) + }; + + // Labeled break? + // --------------- labels and blocks ------------------------------------------// diff --git a/recoder/src/main/java/recoder/java/statement/SwitchBranch.java b/recoder/src/main/java/recoder/java/statement/SwitchBranch.java index 78e0137784e..290c00d5186 100644 --- a/recoder/src/main/java/recoder/java/statement/SwitchBranch.java +++ b/recoder/src/main/java/recoder/java/statement/SwitchBranch.java @@ -1,3 +1,7 @@ +/* This file was part of the RECODER library and protected by the LGPL. + * This file is part of KeY since 2021 - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package recoder.java.statement; public abstract class SwitchBranch extends Branch { From 214e52c0b6ad2d5a293c119e3b006b633afd8416 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 14 Mar 2024 09:07:21 +0100 Subject: [PATCH 3/8] Spotless --- .../java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java | 3 ++- .../uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 6caff0b9fba..5a50cd41e34 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -278,7 +278,8 @@ public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrap } /** - * for some reason the {@code this} and {@code super} references have to be treated differently here. + * for some reason the {@code this} and {@code super} references have to be treated differently + * here. */ @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java index d97b30f723c..e15f939025c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java @@ -1,6 +1,10 @@ +/* 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.recoderext; import de.uka.ilkd.key.logic.op.SchemaVariable; + import recoder.java.ProgramElement; import recoder.java.SourceVisitor; import recoder.java.Statement; From 77fc421fe7990da7857d8529cc98a86f11a167e2 Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 18 Mar 2024 08:08:52 +0100 Subject: [PATCH 4/8] Fix parsing and rules --- .../key/java/SchemaRecoder2KeYConverter.java | 4 +- .../recoderext/SchemaJavaProgramFactory.java | 2 +- .../recoderext/SwitchBranchSVWrapper.java | 11 ++-- .../uka/ilkd/key/java/statement/Switch.java | 29 +++++++++- .../java/statement/SwitchBranchSVWrapper.java | 56 +++++++++++++++++++ .../ilkd/key/logic/sort/ProgramSVSort.java | 16 +----- .../key/parser/schemajava/SchemaJavaParser.jj | 2 +- .../de/uka/ilkd/key/proof/rules/javaRules.key | 24 ++++---- 8 files changed, 108 insertions(+), 36 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 5a50cd41e34..33feb42d19b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -273,8 +273,8 @@ public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.ProgramVariableSVW return svw.getSV(); } - public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { - return svw.getSV(); + public SwitchBranchSVWrapper convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { + return new SwitchBranchSVWrapper(svw.getSV()); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java index 738105894a8..2611d51662a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java @@ -249,7 +249,7 @@ public SwitchBranchSVWrapper getSwitchBranchSV(String s) throws ParseException { if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "SwitchCase"); } - return new SwitchBranchSVWrapper(sv); + return new SwitchBranchSVWrapper((ProgramSV) sv); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java index e15f939025c..c9228bc3aeb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java @@ -3,8 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.logic.op.SchemaVariable; import recoder.java.ProgramElement; import recoder.java.SourceVisitor; import recoder.java.Statement; @@ -12,9 +13,9 @@ public class SwitchBranchSVWrapper extends SwitchBranch implements KeYRecoderExtension, SVWrapper { private static final long serialVersionUID = -1; - protected SchemaVariable sv; + protected ProgramSV sv; - public SwitchBranchSVWrapper(SchemaVariable sv) { + public SwitchBranchSVWrapper(ProgramSV sv) { this.sv = sv; } @@ -25,14 +26,14 @@ public SwitchBranchSVWrapper(SchemaVariable sv) { */ @Override public void setSV(SchemaVariable sv) { - this.sv = sv; + this.sv = (ProgramSV) sv; } /** * returns a String name of this meta construct. */ @Override - public SchemaVariable getSV() { + public ProgramSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java index 69ef54ed8bc..99e7eb4678f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java @@ -4,13 +4,20 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.reference.ExecutionContext; +import de.uka.ilkd.key.java.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.op.ProgramSV; +import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; +import java.util.LinkedList; + /** * Switch. */ @@ -202,6 +209,12 @@ 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 @@ -247,8 +260,22 @@ public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } + /** + * 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); + } + @Override public PosInProgram getFirstActiveChildPos() { - return branches.isEmpty() ? PosInProgram.TOP : PosInProgram.ZERO; + return branches.isEmpty() ? PosInProgram.TOP : (expressionWithoutSideffects() + ? PosInProgram.ONE + : PosInProgram.TOP); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..53fb4ec8678 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java @@ -0,0 +1,56 @@ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.SourceData; +import de.uka.ilkd.key.java.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/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 773c472e275..53002372dfb 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 @@ -244,9 +244,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_CASE = new SwitchBranchSVSort(); + public static final ProgramSVSort SWITCH_BRANCH = new SwitchBranchSVSort(); public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE = new ConstantProgramVariableSort(new Name("ConstantPrimitiveTypeVariable"), false); @@ -1216,18 +1214,6 @@ protected boolean canStandFor(ProgramElement check, Services services) { } } - private static final class SwitchSVSort extends ProgramSVSort { - - public SwitchSVSort() { - super(new Name("Switch")); - } - - @Override - protected boolean canStandFor(ProgramElement pe, Services services) { - return (pe instanceof Switch); - } - } - private static final class SwitchBranchSVSort extends ProgramSVSort { public SwitchBranchSVSort() { super(new Name("SwitchBranch")); } diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj index 82b2f0f4c3d..e1c70cb0a0f 100644 --- a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj +++ b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj @@ -3998,7 +3998,7 @@ Switch SwitchStatement() : "(" expr = Expression() ")" "{" ( - { SwitchBranchSVWrapper sbsv; } sbsv=SwitchBranchSV() + { SwitchBranchSVWrapper sbsv; } "case:" sbsv=SwitchBranchSV() { branches.add(sbsv); } | ( branch = SwitchLabel() diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index daef7efdf1e..5d6ebee5b4e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -68,7 +68,6 @@ \program [list] Catch #cs; \program [list] SwitchBranch #cases; - \program Switch #sw; \program Label #lb, #lb0, #lb1, #innerLabel, #outerLabel; \program NonSimpleMethodReference #nsmr; \program NonModelMethodBody #mb; @@ -1403,9 +1402,9 @@ // --------------- switch-statements ------------------------------------------// switchUnfold { - \find(\modality{#allmodal}{.. switch (#nse) {#cases} ...}\endmodality (post)) + \find(\modality{#allmodal}{.. switch (#nse) {case: #cases} ...}\endmodality (post)) \varcond(\newTypeOf(#v0, #nse)) - \replacewith(\modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; switch (#se) {#cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; switch (#se) {case: #cases} ...}\endmodality (post)) }; switchDefault { @@ -1429,16 +1428,16 @@ }; switchCase { - \find(==> \modality{#allmodal}{.. switch (#se) {case #se0: #slist #cases} ...}\endmodality (post)) + \find(==> \modality{#allmodal}{.. switch (#se) {case #se0: #slist case: #cases} ...}\endmodality (post)) "#se equals #se0": - \replacewith(==> \modality{#allmodal}{.. switch (#se) {active-case: #slist #cases} ...}\endmodality (post)) \add(#se = #se0 ==>); + \replacewith(==> \modality{#allmodal}{.. switch (#se) {active-case: #slist case: #cases} ...}\endmodality (post)) \add(#se = #se0 ==>); "#se not equals #se0": - \replacewith(==> \modality{#allmodal}{.. switch (#se) {#cases} ...}\endmodality (post)) \add(!(#se = #se0) ==>) + \replacewith(==> \modality{#allmodal}{.. switch (#se) {case: #cases} ...}\endmodality (post)) \add(!(#se = #se0) ==>) }; switchFallThrough { - \find(\modality{#allmodal}{.. switch (#se) {active-case: case #se0: #slist #cases} ...}\endmodality (post)) - \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist #cases} ...}\endmodality (post)) + \find(\modality{#allmodal}{.. switch (#se) {active-case: case #se0: #slist case: #cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. switch (#se) {active-case: #slist case: #cases} ...}\endmodality (post)) }; switchFallThroughDefault { @@ -1447,11 +1446,14 @@ }; switchBreak { - \find(\modality{#allmodal}{.. switch (#se) {active-case: break; #slist #cases} ...}\endmodality (post)) - \replacewith(\modality{#allmodal}{.. ...}\endmodality (post)) + \find(\modality{#allmodal}{.. switch (#se) {active-case: break; #slist case: #cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. ...}\endmodality (post)) }; - // Labeled break? + switchBreakLabel { + \find(\modality{#allmodal}{.. switch (#se) {active-case: break #lb; #slist case: #cases} ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. break #lb; ...}\endmodality (post)) + }; // --------------- labels and blocks ------------------------------------------// From e40c75d713a3051359ec3dd76a48ac0109b3488b Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 27 Mar 2024 14:35:53 +0100 Subject: [PATCH 5/8] Fix switch rules and construction --- .../util/SymbolicExecutionUtil.java | 4 +- .../ilkd/key/java/ContextStatementBlock.java | 28 ++++----- .../java/de/uka/ilkd/key/java/JavaTools.java | 10 ++-- .../uka/ilkd/key/java/ProgramPrefixUtil.java | 4 +- .../key/java/SchemaRecoder2KeYConverter.java | 4 +- .../de/uka/ilkd/key/java/StatementBlock.java | 26 ++++---- .../ilkd/key/java/statement/ActiveCase.java | 36 ++++++++--- .../key/java/statement/BranchStatement.java | 6 ++ .../uka/ilkd/key/java/statement/Default.java | 6 ++ .../de/uka/ilkd/key/java/statement/Exec.java | 14 ++--- .../key/java/statement/LabeledStatement.java | 18 +++--- .../key/java/statement/LoopScopeBlock.java | 14 ++--- .../ilkd/key/java/statement/MethodFrame.java | 14 ++--- .../uka/ilkd/key/java/statement/Switch.java | 59 +++++++++++++------ .../key/java/statement/SynchronizedBlock.java | 19 +++--- .../de/uka/ilkd/key/java/statement/Try.java | 14 ++--- .../key/java/visitor/CreatingASTVisitor.java | 38 ++++++++---- .../key/java/visitor/ProgramContextAdder.java | 55 +++++++++++------ .../uka/ilkd/key/logic/MethodStackInfo.java | 6 +- ...Prefix.java => PossibleProgramPrefix.java} | 10 ++-- .../de/uka/ilkd/key/pp/PrettyPrinter.java | 8 ++- .../java/de/uka/ilkd/key/proof/NodeInfo.java | 4 +- .../de/uka/ilkd/key/proof/TacletIndex.java | 4 +- .../rule/AbstractAuxiliaryContractRule.java | 6 +- .../ilkd/key/rule/LoopScopeInvariantRule.java | 4 +- .../key/rule/UseOperationContractRule.java | 6 +- .../rule/conditions/IsLabeledCondition.java | 6 +- .../feature/ThrownExceptionFeature.java | 6 +- .../de/uka/ilkd/key/proof/rules/javaRules.key | 41 +++++++++++-- .../java_dl/switch/SwitchWithBlock.java | 18 ++++++ 30 files changed, 316 insertions(+), 172 deletions(-) rename key.core/src/main/java/de/uka/ilkd/key/logic/{ProgramPrefix.java => PossibleProgramPrefix.java} (79%) create mode 100644 key.ui/examples/standard_key/java_dl/switch/SwitchWithBlock.java 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 64d688993cb..8cbd13de4c1 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 @@ -1639,7 +1639,7 @@ 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); } @@ -3919,7 +3919,7 @@ public static Pair computeSecondStatement(RuleApp ruleAp 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/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java index 408d81bbdb1..5aba7edec1a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.IntIterator; 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; @@ -165,12 +165,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 (patternPrefixLength > srcPrefixLength) { @@ -179,7 +179,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { pos = srcPrefixLength - patternPrefixLength; - ProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); + PossibleProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); relPos = firstActiveStatement.getFirstActiveChildPos(); @@ -198,7 +198,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { start = relPos.get(relPos.depth() - 1); if (relPos.depth() > 1) { - firstActiveStatement = (ProgramPrefix) PosInProgram.getProgramAt(relPos.up(), + firstActiveStatement = (PossibleProgramPrefix) PosInProgram.getProgramAt(relPos.up(), firstActiveStatement); } } @@ -235,8 +235,8 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { * position */ private MatchConditions makeContextInfoComplete(MatchConditions matchCond, SourceData newSource, - ProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src, - Services services) { + PossibleProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src, + Services services) { final SVInstantiations instantiations = matchCond.getInstantiations(); final ExecutionContext lastExecutionContext = instantiations.getExecutionContext(); @@ -266,8 +266,8 @@ private MatchConditions makeContextInfoComplete(MatchConditions matchCond, Sourc * @return the inner most execution context */ private MatchConditions matchInnerExecutionContext(MatchConditions matchCond, - final Services services, ExecutionContext lastExecutionContext, - final ProgramPrefix prefix, int pos, final ProgramElement src) { + final Services services, ExecutionContext lastExecutionContext, + final PossibleProgramPrefix prefix, int pos, final ProgramElement src) { // partial context instantiation @@ -305,10 +305,10 @@ 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(); @@ -331,8 +331,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/JavaTools.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java index 0d3b0f3f3e0..ffdfc250145 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 @@ -4,13 +4,14 @@ package de.uka.ilkd.key.java; import de.uka.ilkd.key.java.reference.ExecutionContext; +import de.uka.ilkd.key.java.statement.ActiveCase; import de.uka.ilkd.key.java.statement.CatchAllStatement; import de.uka.ilkd.key.java.statement.LabeledStatement; import de.uka.ilkd.key.java.statement.MethodFrame; 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; @@ -30,13 +31,14 @@ 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 { + } 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/ProgramPrefixUtil.java b/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java index f409c13a8dd..056210e3817 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.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/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 33feb42d19b..5a50cd41e34 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -273,8 +273,8 @@ public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.ProgramVariableSVW return svw.getSV(); } - public SwitchBranchSVWrapper convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { - return new SwitchBranchSVWrapper(svw.getSV()); + public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { + return svw.getSV(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java index 9b882eb5812..27d49c29e9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.java.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.util.Debug; import org.key_project.util.ExtList; @@ -22,7 +22,7 @@ */ public class StatementBlock extends JavaStatement implements StatementContainer, - TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix { + TypeDeclarationContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Body. @@ -85,9 +85,9 @@ public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) { } /** computes the prefix elements for the given array of statment block */ - public static ImmutableArray computePrefixElements( - ProgramPrefix current) { - final ArrayList prefix = new ArrayList<>(); + public static ImmutableArray computePrefixElements( + PossibleProgramPrefix current) { + final ArrayList prefix = new ArrayList<>(); prefix.add(current); while (current.hasNextPrefixElement()) { @@ -240,24 +240,28 @@ public SourceElement getFirstElementIncludingBlocks() { } } + @Override + public boolean isPrefix() { + return !isEmpty(); + } @Override public boolean hasNextPrefixElement() { - return body.size() != 0 && (body.get(0) instanceof ProgramPrefix); + return body.size() != 0 && (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 @@ -271,7 +275,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java index ab3ed1d5267..ab1604ff595 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java @@ -6,16 +6,16 @@ import de.uka.ilkd.key.java.*; 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; -public class ActiveCase extends SwitchBranch implements ProgramPrefix { +public class ActiveCase extends SwitchBranch implements PossibleProgramPrefix { /** * Body. */ - protected final ImmutableArray body; + protected final ImmutableArray body; private final MethodFrame innerMostMethodFrame; @@ -34,6 +34,13 @@ public ActiveCase(Statement[] body) { 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. * @@ -96,6 +103,12 @@ public ProgramElement getChildAt(int 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. * @@ -125,7 +138,7 @@ public Statement getStatementAt(int index) { * The body may be empty (null), to define a fall-through. Attaching an {@link EmptyStatement} * would create a single ";". */ - public ImmutableArray getBody() { + public ImmutableArray getBody() { return body; } @@ -139,27 +152,32 @@ 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 ProgramPrefix; + return body != null && !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() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java index 66ee1d7d48e..9247ceae7e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.NonTerminalProgramElement; +import de.uka.ilkd.key.java.PositionInfo; import org.key_project.util.ExtList; /** @@ -20,6 +21,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/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java index 55612a1dbc9..ceb807cb9cf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.java.Statement; import de.uka.ilkd.key.java.visitor.Visitor; @@ -62,6 +63,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/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java index e7d1e02d664..a10bd75928d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; 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; @@ -16,7 +16,7 @@ * * @author AutoDoc */ -public class Exec extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Exec extends BranchStatement implements StatementContainer, PossibleProgramPrefix { /** * Body. @@ -92,20 +92,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; } @@ -120,7 +120,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java index 16323cab7b5..6e4a5d83d06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java @@ -7,7 +7,7 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.logic.ProgramElementName; -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 @@ */ public class LabeledStatement extends JavaStatement - implements StatementContainer, NamedProgramElement, ProgramPrefix { + implements StatementContainer, NamedProgramElement, PossibleProgramPrefix { /** * Name. @@ -99,10 +99,10 @@ 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 +110,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,15 +121,15 @@ 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(this); - } else if (body instanceof ProgramPrefix) { + } 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/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java index d8c4744ce57..5f008505b79 100644 --- 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 @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; 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; @@ -19,7 +19,7 @@ * @author Dominic Scheurer */ public class LoopScopeBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { protected final IProgramVariable indexPV; protected final StatementBlock body; @@ -72,20 +72,20 @@ 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); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -100,7 +100,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } 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 index c0e1040163c..6d632b0152c 100644 --- 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 @@ -7,7 +7,7 @@ import de.uka.ilkd.key.java.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; @@ -18,7 +18,7 @@ * The statement inserted by KeY if a method call is executed. */ public class MethodFrame extends JavaStatement - implements Statement, StatementContainer, ProgramPrefix { + implements Statement, StatementContainer, PossibleProgramPrefix { /** * result @@ -92,20 +92,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; } @@ -120,7 +120,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java index 99e7eb4678f..fa2e84b767b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java @@ -4,32 +4,29 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.expression.Literal; import de.uka.ilkd.key.java.reference.ExecutionContext; import de.uka.ilkd.key.java.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.ProgramSV; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.sort.ProgramSVSort; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; -import java.util.LinkedList; - /** * Switch. */ public class Switch extends BranchStatement - implements ExpressionContainer, VariableScope, TypeScope, ProgramPrefix { + implements ExpressionContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Branches. */ - protected final ImmutableArray branches; + protected final ImmutableArray branches; /** * Expression. @@ -72,7 +69,24 @@ public Switch(Expression e) { * @param branches a branch array */ - public Switch(Expression e, SwitchBranch[] branches) { + 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); @@ -88,8 +102,8 @@ public Switch(Expression e, SwitchBranch[] branches) { public Switch(ExtList children) { super(children); - this.expression = children.get(Expression.class); - this.branches = new ImmutableArray<>(children.collect(SwitchBranch.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(); @@ -192,7 +206,7 @@ public int getBranchCount() { * @exception ArrayIndexOutOfBoundsException if index is out of bounds. */ - public SwitchBranch getBranchAt(int index) { + public Branch getBranchAt(int index) { if (branches != null) { return branches.get(index); } @@ -205,7 +219,7 @@ public SwitchBranch getBranchAt(int index) { * * @return the array wrapper of the branches */ - public ImmutableArray getBranchList() { + public ImmutableArray getBranchList() { return branches; } @@ -225,23 +239,30 @@ public void visit(Visitor v) { v.performActionOnSwitch(this); } + @Override + public boolean isPrefix() { + if (branches.isEmpty()) + System.err.println("Error: empty switch " + expression); + return !branches.isEmpty() && expressionWithoutSideffects(); + } + @Override public boolean hasNextPrefixElement() { - return !branches.isEmpty() && branches.get(0) instanceof ProgramPrefix; + return !branches.isEmpty() && branches.get(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) branches.get(0); + return (PossibleProgramPrefix) branches.get(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() ? ((ProgramPrefix) branches.get(0)).getLastPrefixElement() + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? ((PossibleProgramPrefix) branches.get(0)).getLastPrefixElement() : this; } @@ -256,7 +277,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } @@ -269,7 +290,7 @@ public ImmutableArray getPrefixElements() { */ private boolean expressionWithoutSideffects() { return (expression instanceof ProgramVariable && !((ProgramVariable) expression).isMember()) - || (expression instanceof MetaClassReference); + || (expression instanceof MetaClassReference) || expression instanceof Literal; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java index 0ee1cd5d2a1..33fc58405b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.java.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; @@ -19,7 +19,7 @@ */ public class SynchronizedBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { /** * Expression. @@ -86,22 +86,27 @@ public SynchronizedBlock(ExtList children) { } + @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; } @@ -116,7 +121,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } 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 index 8bafec72a74..c0705286b07 100644 --- 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 @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; 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; @@ -16,7 +16,7 @@ * * @author AutoDoc */ -public class Try extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Try extends BranchStatement implements StatementContainer, PossibleProgramPrefix { /** * Body. @@ -98,20 +98,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; } @@ -126,7 +126,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + 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 00d3528ec92..fce64b82937 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 @@ -360,13 +360,18 @@ ProgramElement createNewElement(ExtList changeList) { @Override public void performActionOnActiveCase(ActiveCase x) { - DefaultAction def = new DefaultAction(x) { - @Override - ProgramElement createNewElement(ExtList changeList) { - return new ActiveCase(changeList); + ExtList changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + PositionInfo pi = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pi = PositionInfo.UNDEFINED; } - }; - def.doAction(x); + addChild(new ActiveCase(changeList, pi)); + changed(); + } else { + doDefaultAction(x); + } } // eee @@ -1220,13 +1225,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/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index ce574d5c9fa..0da55ad7496 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 @@ -5,17 +5,9 @@ import java.rmi.UnexpectedException; -import de.uka.ilkd.key.java.JavaNonTerminalProgramElement; -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.Statement; -import de.uka.ilkd.key.java.StatementBlock; +import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration; -import de.uka.ilkd.key.java.statement.Exec; -import de.uka.ilkd.key.java.statement.LabeledStatement; -import de.uka.ilkd.key.java.statement.LoopScopeBlock; -import de.uka.ilkd.key.java.statement.MethodFrame; -import de.uka.ilkd.key.java.statement.SynchronizedBlock; -import de.uka.ilkd.key.java.statement.Try; +import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.IntIterator; import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation; @@ -59,10 +51,12 @@ 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 { @@ -71,7 +65,7 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte if (context instanceof StatementBlock block) { return createStatementBlockWrapper(block, body); } else if (context instanceof Try t) { - return createTryStatementWrapper((StatementBlock) body, t); + return createTryStatementWrapper(t, (StatementBlock) body); } else if (context instanceof MethodFrame mf) { return createMethodFrameWrapper(mf, (StatementBlock) body); } else if (context instanceof LabeledStatement ls) { @@ -81,9 +75,14 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte } else if (context instanceof SynchronizedBlock sb) { return createSynchronizedBlockWrapper(sb, (StatementBlock) body); - } else if (context instanceof Exec) { - return createExecStatementWrapper((StatementBlock) body, (Exec) context); - } else { + } 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())); } @@ -92,7 +91,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 * around the content of putIn @@ -166,11 +165,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/logic/MethodStackInfo.java b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java index a2f0aa31ffc..382e118eaaf 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 c7881fa958e..fd147e88024 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/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index f6cb84a28eb..16ea533f8e0 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 @@ -17,7 +17,7 @@ import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.AbstractProgramElement; @@ -824,7 +824,7 @@ public void performActionOnClassInitializer(ClassInitializer x) { protected void performActionOnStatement(SourceElement s) { l.beginRelativeC(0); - boolean validStatement = !(s instanceof CatchAllStatement || s instanceof ProgramPrefix); + boolean validStatement = !(s instanceof CatchAllStatement || (s instanceof PossibleProgramPrefix pre && pre.isPrefix())); if (validStatement) { markStart(s); } @@ -1687,7 +1687,7 @@ public void performActionOnElse(Else x) { } } - private void printCaseBody(ImmutableArray body) { + private void printCaseBody(ImmutableArray body) { if (body != null && !body.isEmpty()) { for (int i = 0; i < body.size(); i++) { Statement statement = body.get(i); @@ -1743,8 +1743,10 @@ public void performActionOnDefault(Default x) { @Override public void performActionOnActiveCase(ActiveCase x) { + if (!x.isPrefix()) markStart(x); l.keyWord("active-case").print(":"); printCaseBody(x.getBody()); + if (!x.isPrefix()) markEnd(x); } @Override 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 6e0e4edc6a7..1d1fd06eb0c 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 @@ -13,7 +13,7 @@ import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.java.StatementBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.SequentChangeInfo; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; @@ -191,7 +191,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 5c2d97d2a93..71590e04946 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 @@ -8,7 +8,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; @@ -311,7 +311,7 @@ private ImmutableList getJavaTacletList( HashMap> map, ProgramElement pe, PrefixOccurrences prefixOccurrences) { ImmutableList res = ImmutableSLList.nil(); - if (pe instanceof ProgramPrefix) { + if (pe instanceof PossibleProgramPrefix) { int next = prefixOccurrences.occurred(pe); NonTerminalProgramElement nt = (NonTerminalProgramElement) pe; if (next < nt.getChildCount()) { 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 cf46c48961e..24cf559cf35 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 @@ -18,7 +18,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.Namespace; import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.*; @@ -296,9 +296,7 @@ private static ExecutionContext extractExecutionContext(final MethodFrame frame) private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract( final Modality modality, final Goal goal) { SourceElement element = modality.program().program().getFirstElement(); - while ((element instanceof ProgramPrefix || element instanceof CatchAllStatement) - && !(element instanceof StatementBlock - && ((StatementBlock) element).isEmpty())) { + while ((element instanceof PossibleProgramPrefix pre && pre.isPrefix()) || element instanceof CatchAllStatement) { if (element instanceof StatementBlock && hasApplicableContracts(services, (StatementBlock) element, modality.kind(), goal)) { return (StatementBlock) element; 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 3dc8ef99449..4396108581b 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 @@ -20,7 +20,7 @@ import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; @@ -416,7 +416,7 @@ private Pair, Statement> findLoopLabel(RuleApp ruleApp, While wh Optional