From 3fa8f1d7f80473aea9781ebd321e716b068ab6f2 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 | 3 +- .../key/java/ast/statement/ActiveCase.java | 122 ++++++++++++++++++ .../uka/ilkd/key/java/ast/statement/Case.java | 2 +- .../ilkd/key/java/ast/statement/Default.java | 2 +- .../ilkd/key/java/ast/statement/Switch.java | 10 +- .../key/java/ast/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 | 11 ++ .../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 +- .../recoder/java/statement/SwitchBranch.java | 33 +++++ 17 files changed, 252 insertions(+), 29 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/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 0523878dbb1..6b70e319843 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 @@ -2484,8 +2484,7 @@ public static SuperReference superReference() { * @return a new {@link Switch} block that executes branches depending on the value * of expression */ - public static Switch switchBlock(final Expression expression, final Branch[] branches) { - + public static Switch switchBlock(final Expression expression, final SwitchBranch[] branches) { return new Switch(expression, branches); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java new file mode 100644 index 00000000000..b255b0ab4ac --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/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/ast/statement/Case.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java index 8fe123b94cd..02c8b9e4f60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java @@ -16,7 +16,7 @@ * Case. * */ -public class Case extends BranchImp implements ExpressionContainer { +public class Case extends SwitchBranch implements ExpressionContainer { /** * Expression. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java index faa6ae4c7f1..1a126a9cc8f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java @@ -18,7 +18,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/ast/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java index a434d0835b1..92439bfaedf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java @@ -23,7 +23,7 @@ public class Switch extends BranchStatement * Branches. */ - protected final ImmutableArray branches; + protected final ImmutableArray branches; /** * Expression. @@ -63,7 +63,7 @@ public Switch(Expression e) { * a branch array */ - public Switch(Expression e, Branch[] branches) { + public Switch(Expression e, SwitchBranch[] branches) { this.branches = new ImmutableArray<>(branches); this.expression = e; } @@ -78,7 +78,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)); } public Switch(PositionInfo pi, List c, Expression expr, @@ -187,7 +187,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); } @@ -200,7 +200,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/ast/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java new file mode 100644 index 00000000000..574f9f138c4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/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 e79746808de..87399eb13ab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -363,6 +363,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 fb6a24e4824..67be8213b18 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -268,6 +268,11 @@ public void performActionOnCase(Case x) { doDefaultAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + doDefaultAction(x); + } + @Override public void performActionOnCatch(Catch x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index 0b77f3cb88c..b3fcc7b069a 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 @@ -67,18 +67,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); @@ -146,7 +146,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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index e5299c49298..fd8d71e6848 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -304,6 +304,8 @@ public interface Visitor { void performActionOnCase(Case x); + void performActionOnActiveCase(ActiveCase x); + void performActionOnCatch(Catch x); void performActionOnDefault(Default x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 4e644442ee7..5df3d85b788 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 @@ -227,6 +227,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); @@ -1207,6 +1209,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 5551e134e2d..fa6dfbc7500 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 @@ -1779,6 +1779,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) { layouter.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 dea977c4653..d37955f9787 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 @@ -134,11 +134,11 @@ private If mkIfNullCheck(Services services, ProgramVariable var, Statement elseB */ private ChangeBreakResult changeBreaks(Switch sw, Break b, boolean noNewBreak) { int n = sw.getBranchCount(); - Branch[] branches = new Branch[n]; + SwitchBranch[] branches = new SwitchBranch[n]; for (int i = 0; i < n; i++) { final var branch = recChangeBreaks(sw.getBranchAt(i), b, noNewBreak); noNewBreak = branch.noNewBreak; - branches[i] = (Branch) branch.result; + branches[i] = (SwitchBranch) branch.result; } return new ChangeBreakResult(KeYJavaASTFactory.switchBlock(sw.getExpression(), branches), noNewBreak); 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 7e647439b0d..b5517f0ef23 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 @@ -4000,6 +4000,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); } @@ -4043,6 +4045,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 97257fcb1b2..fa4dd8ab20a 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 @@ -57,6 +57,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; @@ -1412,10 +1413,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 c8f575d4bc3..5017f284275 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 @@ -98,7 +98,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/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 9601b0c45af3a5b41d152d79d5abf25b010769e9 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 --- .../uka/ilkd/key/java/ast/StatementBlock.java | 2 +- .../key/java/ast/statement/ActiveCase.java | 66 +- .../uka/ilkd/key/java/ast/statement/Exec.java | 2 +- .../java/ast/statement/LabeledStatement.java | 4 +- .../java/ast/statement/LoopScopeBlock.java | 2 +- .../key/java/ast/statement/MethodFrame.java | 2 +- .../ilkd/key/java/ast/statement/Switch.java | 56 +- .../key/java/ast/statement/SwitchBranch.java | 4 + .../java/ast/statement/SynchronizedBlock.java | 2 +- .../uka/ilkd/key/java/ast/statement/Try.java | 2 +- .../ilkd/key/java/recoderext/ActiveCase.java | 209 ++++++ .../recoderext/SchemaJavaProgramFactory.java | 618 ++++++++++++++++++ .../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 +- .../prover/rules/SwitchBranchSVWrapper.java | 74 +++ .../recoder/java/statement/SwitchBranch.java | 4 + 18 files changed, 1102 insertions(+), 27 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/recoderext/SchemaJavaProgramFactory.java create mode 100644 key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java index bf47856cf72..97fa68783d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java @@ -322,7 +322,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/ast/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java index b255b0ab4ac..ab3ed1d5267 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java @@ -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/ast/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java index 4fd74ad01cd..d27b58ebb1e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java @@ -131,7 +131,7 @@ public MethodFrame getInnerMostMethodFrame() { @Override public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + return StatementBlock.computePrefixElements(this); } @NonNull diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java index 1551974266e..0392aa5e543 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java @@ -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/ast/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java index 94766986997..e1cb935d7c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java @@ -138,7 +138,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/ast/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java index 72d35726034..0fa3796d456 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java @@ -147,7 +147,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/ast/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java index 92439bfaedf..18281770d02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java @@ -8,6 +8,8 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.ProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -17,7 +19,7 @@ */ public class Switch extends BranchStatement - implements ExpressionContainer, VariableScope, TypeScope { + implements ExpressionContainer, VariableScope, TypeScope, ProgramPrefix { /** * Branches. @@ -31,7 +33,9 @@ public class Switch extends BranchStatement protected final Expression expression; + private final int prefixLength; + private final MethodFrame innerMostMethodFrame; /** * Switch. @@ -40,6 +44,8 @@ public class Switch extends BranchStatement public Switch() { this.branches = null; this.expression = null; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -52,6 +58,8 @@ public Switch() { public Switch(Expression e) { this.branches = null; this.expression = e; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -66,6 +74,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(); } /** @@ -79,6 +90,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(); } public Switch(PositionInfo pi, List c, Expression expr, @@ -214,4 +228,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/ast/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java index 574f9f138c4..71c9e3a538d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java @@ -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/ast/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java index cea5771d8ca..009ddf66522 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java @@ -134,7 +134,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/ast/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java index 17b9c49a716..b7aeb68c314 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java @@ -139,7 +139,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/recoderext/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java new file mode 100644 index 00000000000..75510a8957a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java @@ -0,0 +1,209 @@ +/* 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.*; +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 new file mode 100644 index 00000000000..738105894a8 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java @@ -0,0 +1,618 @@ +/* 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 java.io.IOException; +import java.io.Reader; +import java.util.List; + +import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.parser.schemajava.ParseException; +import de.uka.ilkd.key.parser.schemajava.SchemaJavaParser; + +import org.key_project.logic.Name; + +import recoder.ParserException; +import recoder.convenience.TreeWalker; +import recoder.java.*; +import recoder.java.SourceElement.Position; +import recoder.java.declaration.ConstructorDeclaration; +import recoder.java.declaration.FieldDeclaration; +import recoder.java.declaration.MemberDeclaration; +import recoder.java.declaration.MethodDeclaration; +import recoder.java.declaration.ParameterDeclaration; +import recoder.java.declaration.TypeDeclaration; +import recoder.java.reference.MethodReference; +import recoder.java.reference.ReferencePrefix; +import recoder.java.reference.TypeReference; +import recoder.list.generic.ASTArrayList; +import recoder.list.generic.ASTList; + +public class SchemaJavaProgramFactory extends JavaProgramFactory { + + protected Namespace svns; + + /** + * Protected constructor - use {@link #getInstance} instead. + */ + protected SchemaJavaProgramFactory() {} + + /** + * The singleton instance of the program factory. + */ + private static final SchemaJavaProgramFactory theFactory = new SchemaJavaProgramFactory(); + + /** + * Returns the single instance of this class. + */ + public static JavaProgramFactory getInstance() { + return theFactory; + } + + /** + * Create an {@link ImplicitIdentifier}. + */ + public ImplicitIdentifier createImplicitIdentifier(String text) { + return new ImplicitIdentifier(text); + } + + @Override + public Identifier createIdentifier(String text) { + return new ExtendedIdentifier(text); + } + + public SpecialReferenceWrapper createThisReference(TypeReference typeRef, Expression var) { + return new SpecialReferenceWrapper(typeRef, (ReferencePrefix) var); + } + + public RMethodCallStatement createRMethodCallStatement(ProgramVariableSVWrapper resVar, + ExecutionContext esvw, Statement st) { + return new RMethodCallStatement(resVar, esvw, st); + } + + public LoopScopeBlock createLoopScopeBlock() { + return new LoopScopeBlock(); + } + + + public RMethodBodyStatement createRMethodBodyStatement(TypeReference typeRef, + ProgramVariableSVWrapper resVar, MethodReference mr) { + return new RMethodBodyStatement(typeRef, resVar, mr); + } + + public RKeYMetaConstruct createRKeYMetaConstruct() { + return new RKeYMetaConstruct(); + } + + public RKeYMetaConstructExpression createRKeYMetaConstructExpression() { + return new RKeYMetaConstructExpression(); + } + + + public RKeYMetaConstructType createRKeYMetaConstructType() { + return new RKeYMetaConstructType(); + } + + public ContextStatementBlock createContextStatementBlock(TypeSVWrapper typeRef, + MethodSignatureSVWrapper pm, ExpressionSVWrapper var) { + return new ContextStatementBlock(typeRef, pm, var); + } + + public ContextStatementBlock createContextStatementBlock(ExecCtxtSVWrapper ec) { + return new ContextStatementBlock(ec); + } + + /** + * Create a {@link PassiveExpression}. + */ + public PassiveExpression createPassiveExpression(Expression e) { + return new PassiveExpression(e); + } + + public MergePointStatement createMergePointStatement() { + return new MergePointStatement(); + } + + public MergePointStatement createMergePointStatement(Expression e) { + return new MergePointStatement(e); + } + + public ActiveCase createActiveCase() { + return new ActiveCase(); + } + + /** + * Create a {@link PassiveExpression}. + */ + public PassiveExpression createPassiveExpression() { + return new PassiveExpression(); + } + + public static void throwSortInvalid(SchemaVariable sv, String s) throws ParseException { + throw new ParseException("Sort of declared schema variable " + sv.name().toString() + " " + + sv.sort().name().toString() + " does not comply with expected type " + s + + " in Java program."); + } + + + public boolean lookupSchemaVariableType(String s, ProgramSVSort sort) { + if (svns == null) { + return false; + } + SchemaVariable n = svns.lookup(new Name(s)); + if (n instanceof SchemaVariable) { + return n.sort() == sort; + } + return false; + } + + + public SchemaVariable lookupSchemaVariable(String s) throws ParseException { + SchemaVariable sv = null; + SchemaVariable n = svns.lookup(new Name(s)); + if (n instanceof SchemaVariable) { + sv = n; + } else { + throw new ParseException("Schema variable not declared: " + s); + } + return sv; + } + + public StatementSVWrapper getStatementSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Statement"); + } + + return new StatementSVWrapper(sv); + } + + public ExpressionSVWrapper getExpressionSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Expression"); + } + return new ExpressionSVWrapper(sv); + } + + + public LabelSVWrapper getLabelSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Label"); + } + return new LabelSVWrapper(sv); + } + + public MethodSignatureSVWrapper getMethodSignatureSVWrapper(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "MethodSignature"); + } + return new MethodSignatureSVWrapper(sv); + } + + public JumpLabelSVWrapper getJumpLabelSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV) || sv.sort() != ProgramSVSort.LABEL) { + throwSortInvalid(sv, "Label"); + } + return new JumpLabelSVWrapper(sv); + } + + public TypeSVWrapper getTypeSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Type"); + } + return new TypeSVWrapper(sv); + } + + public ExecCtxtSVWrapper getExecutionContextSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Type"); + } + return new ExecCtxtSVWrapper(sv); + } + + public ProgramVariableSVWrapper getProgramVariableSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Program Variable"); + } + return new ProgramVariableSVWrapper(sv); + } + + public CatchSVWrapper getCatchSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Catch"); + } + return new CatchSVWrapper(sv); + } + + public CcatchSVWrapper getCcatchSV(String s) throws ParseException { + SchemaVariable sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "Ccatch"); + } + 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. + */ + private static final SchemaJavaParser parser = new SchemaJavaParser(System.in); + + private static final Position ZERO_POSITION = new Position(0, 0); + + private static void attachComment(Comment c, ProgramElement pe) { + ProgramElement dest = pe; + if (!c.isPrefixed()) { + NonTerminalProgramElement ppe = dest.getASTParent(); + int i = 0; + if (ppe != null) { + for (; ppe.getChildAt(i) != dest; i++) { + } + } + if (i == 0) { // before syntactical parent + c.setPrefixed(true); + } else { + dest = ppe.getChildAt(i - 1); + while (dest instanceof NonTerminalProgramElement) { + ppe = (NonTerminalProgramElement) dest; + i = ppe.getChildCount(); + if (i == 0) { + break; + } + dest = ppe.getChildAt(i - 1); + } + } + } + if (c instanceof SingleLineComment && c.isPrefixed()) { + Position p = dest.getFirstElement().getRelativePosition(); + if (p.getLine() < 1) { + p.setLine(1); + dest.getFirstElement().setRelativePosition(p); + } + } + ASTList cml = dest.getComments(); + if (cml == null) { + dest.setComments(cml = new ASTArrayList<>()); + } + cml.add(c); + } + + /** + * Perform post work on the created element. Creates parent links and assigns comments. + */ + private static void postWork(ProgramElement pe) { + List comments = SchemaJavaParser.getComments(); + int commentIndex = 0; + int commentCount = comments.size(); + Position cpos = ZERO_POSITION; + Comment current = null; + if (commentIndex < commentCount) { + current = comments.get(commentIndex); + cpos = current.getFirstElement().getStartPosition(); + } + TreeWalker tw = new TreeWalker(pe); + while (tw.next()) { + pe = tw.getProgramElement(); + if (pe instanceof NonTerminalProgramElement) { + ((NonTerminalProgramElement) pe).makeParentRoleValid(); + } + if (pe.getFirstElement() != null) { + Position pos = pe.getFirstElement().getStartPosition(); + while ((commentIndex < commentCount) && pos.compareTo(cpos) > 0) { + attachComment(current, pe); + commentIndex += 1; + if (commentIndex < commentCount) { + current = comments.get(commentIndex); + cpos = current.getFirstElement().getStartPosition(); + } + } + } + } + if (commentIndex < commentCount) { + while (pe.getASTParent() != null) { + pe = pe.getASTParent(); + } + ASTList cml = pe.getComments(); + if (cml == null) { + pe.setComments(cml = new ASTArrayList<>()); + } + do { + current = comments.get(commentIndex); + current.setPrefixed(false); + cml.add(current); + commentIndex += 1; + } while (commentIndex < commentCount); + } + } + + /** + * Parse a {@link CompilationUnit} from the given reader. + */ + @Override + public CompilationUnit parseCompilationUnit(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + CompilationUnit res = SchemaJavaParser.CompilationUnit(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + } + } + + /** + * Parse a {@link TypeDeclaration} from the given reader. + */ + @Override + public TypeDeclaration parseTypeDeclaration(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + TypeDeclaration res = SchemaJavaParser.TypeDeclaration(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link FieldDeclaration} from the given reader. + */ + @Override + public FieldDeclaration parseFieldDeclaration(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + FieldDeclaration res = SchemaJavaParser.FieldDeclaration(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link MethodDeclaration} from the given reader. + */ + @Override + public MethodDeclaration parseMethodDeclaration(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + MethodDeclaration res = SchemaJavaParser.MethodDeclaration(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link MemberDeclaration} from the given reader. + */ + @Override + public MemberDeclaration parseMemberDeclaration(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + MemberDeclaration res = SchemaJavaParser.ClassBodyDeclaration(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link ParameterDeclaration} from the given reader. + */ + @Override + public ParameterDeclaration parseParameterDeclaration(Reader in) + throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + ParameterDeclaration res = SchemaJavaParser.FormalParameter(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link ConstructorDeclaration} from the given reader. + */ + @Override + public ConstructorDeclaration parseConstructorDeclaration(Reader in) + throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + ConstructorDeclaration res = SchemaJavaParser.ConstructorDeclaration(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link TypeReference} from the given reader. + */ + @Override + public TypeReference parseTypeReference(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + TypeReference res = SchemaJavaParser.ResultType(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse an {@link Expression} from the given reader. + */ + @Override + public Expression parseExpression(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + Expression res = SchemaJavaParser.Expression(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse some {@link Statement}s from the given reader. + */ + @Override + public ASTList parseStatements(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + ASTList res = SchemaJavaParser.GeneralizedStatements(); + for (Statement re : res) { + postWork(re); + } + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(); + pe.initCause(e); + throw pe; + } + + } + } + + /** + * Parse a {@link StatementBlock} from the given string. + */ + @Override + public StatementBlock parseStatementBlock(Reader in) throws IOException, ParserException { + synchronized (parser) { + try { + SchemaJavaParser.initialize(in); + StatementBlock res = SchemaJavaParser.StartBlock(); + postWork(res); + return res; + } catch (ParseException e) { + ParserException pe = new ParserException(e.getMessage()); + pe.initCause(e); + throw pe; + } + + } + } + + + + public void setSVNamespace(Namespace ns) { + svns = ns; + } + + public CcatchReturnParameterDeclaration createCcatchReturnParameterDeclaration() { + return new CcatchReturnParameterDeclaration(); + } + + public CcatchReturnValParameterDeclaration createCcatchReturnValParameterDeclaration( + ParameterDeclaration p) { + return new CcatchReturnValParameterDeclaration(p); + } + + public CcatchBreakParameterDeclaration createCcatchBreakParameterDeclaration() { + return new CcatchBreakParameterDeclaration(); + } + + public CcatchBreakLabelParameterDeclaration createCcatchBreakLabelParameterDeclaration( + Identifier label) { + return new CcatchBreakLabelParameterDeclaration(label); + } + + public CcatchBreakWildcardParameterDeclaration createCcatchBreakWildcardParameterDeclaration() { + return new CcatchBreakWildcardParameterDeclaration(); + } + + public CcatchContinueParameterDeclaration createCcatchContinueParameterDeclaration() { + return new CcatchContinueParameterDeclaration(); + } + + public CcatchContinueLabelParameterDeclaration createCcatchContinueLabelParameterDeclaration( + Identifier label) { + return new CcatchContinueLabelParameterDeclaration(label); + } + + public CcatchContinueWildcardParameterDeclaration createCcatchContinueWildcardParameterDeclaration() { + return new CcatchContinueWildcardParameterDeclaration(); + } + + public Ccatch createCcatch() { + return new Ccatch(); + } + + public Exec createExec() { + return new Exec(); + } +} 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 5df3d85b788..bd10892c947 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 @@ -227,7 +227,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); @@ -1209,8 +1209,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 2e2124aa46e..ba4ac6faa49 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 @@ -583,7 +583,8 @@ private static class PrefixOccurrences { */ static final Class[] prefixClasses = new Class[] { StatementBlock.class, LabeledStatement.class, Try.class, - MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class }; + MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class, + Switch.class, ActiveCase.class }; /** * number of prefix types @@ -599,7 +600,7 @@ private static class PrefixOccurrences { * fields to indicate the position of the next relevant child (the next possible prefix * element or real statement */ - static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0 }; + static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0, 1, 0 }; PrefixOccurrences() { reset(); diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj index b5517f0ef23..3e210b0ea5c 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 @@ -2358,7 +2358,6 @@ ExpressionSVWrapper ExpressionSV() : } } - CatchSVWrapper CatchSV() : { } @@ -2379,6 +2378,16 @@ CcatchSVWrapper CcatchSV() : } } +SwitchBranchSVWrapper SwitchBranchSV() : +{ +} +{ + + { + return factory.getSwitchBranchSV(token.image); + } +} + Assignment AssignmentOperator() : { Assignment result; @@ -3987,6 +3996,10 @@ Switch SwitchStatement() : } "(" expr = Expression() ")" "{" + ( + { SwitchBranchSVWrapper sbsv; } sbsv=SwitchBranchSV() + { branches.add(sbsv); } + | ( branch = SwitchLabel() { stats = new ASTArrayList(); @@ -4007,7 +4020,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 fa4dd8ab20a..bbf136765d3 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 @@ -57,7 +57,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; @@ -1412,18 +1412,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/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..d97b30f723c --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/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/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 db4921a8eb278e053508b1c88b4e80e3e749de28 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 14 Mar 2024 09:07:21 +0100 Subject: [PATCH 3/8] Spotless --- .../org/key_project/prover/rules/SwitchBranchSVWrapper.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java index d97b30f723c..e15f939025c 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/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 acb40a471e23607aa9a131d3c50176a8cb3f4d6d 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 --- .../ilkd/key/java/ast/statement/Switch.java | 27 ++++++++- .../ast/statement/SwitchBranchSVWrapper.java | 56 +++++++++++++++++++ .../recoderext/SchemaJavaProgramFactory.java | 2 +- .../ilkd/key/logic/sort/ProgramSVSort.java | 16 +----- .../key/parser/schemajava/SchemaJavaParser.jj | 2 +- .../de/uka/ilkd/key/proof/rules/javaRules.key | 24 ++++---- .../prover/rules/SwitchBranchSVWrapper.java | 11 ++-- 7 files changed, 104 insertions(+), 34 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java index 18281770d02..1c7a5cfe029 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java @@ -11,9 +11,14 @@ 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. */ @@ -218,6 +223,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 @@ -264,8 +275,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/ast/statement/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..53fb4ec8678 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/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/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/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index bd10892c947..4c4cf3ea95a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -225,9 +225,7 @@ public abstract class ProgramSVSort extends SortImpl { public static final ProgramSVSort ARRAYPOSTDECL = new ArrayPostDeclarationSort(); - public static final ProgramSVSort SWITCH = new SwitchSVSort(); - - public static final ProgramSVSort SWITCH_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); @@ -1197,18 +1195,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 3e210b0ea5c..7a707ad5d55 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 @@ -3997,7 +3997,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 bbf136765d3..09d21bd6815 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 @@ -59,7 +59,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; @@ -1413,9 +1412,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 { @@ -1439,16 +1438,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 { @@ -1457,11 +1456,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 ------------------------------------------// diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java index e15f939025c..c9228bc3aeb 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/SwitchBranchSVWrapper.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/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; } From b5eb2bc52e0df6316f171a441946c190591a6f6c 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 +- .../java/de/uka/ilkd/key/java/JavaTools.java | 9 +-- .../uka/ilkd/key/java/ProgramPrefixUtil.java | 4 +- .../key/java/ast/ContextStatementBlock.java | 28 ++++----- .../uka/ilkd/key/java/ast/StatementBlock.java | 28 +++++---- .../key/java/ast/statement/ActiveCase.java | 36 +++++++++--- .../java/ast/statement/BranchStatement.java | 6 ++ .../ilkd/key/java/ast/statement/Default.java | 5 ++ .../uka/ilkd/key/java/ast/statement/Exec.java | 14 ++--- .../java/ast/statement/LabeledStatement.java | 18 +++--- .../java/ast/statement/LoopScopeBlock.java | 19 +++--- .../key/java/ast/statement/MethodFrame.java | 14 ++--- .../ilkd/key/java/ast/statement/Switch.java | 58 +++++++++++++------ .../java/ast/statement/SynchronizedBlock.java | 19 +++--- .../uka/ilkd/key/java/ast/statement/Try.java | 14 ++--- .../key/java/visitor/CreatingASTVisitor.java | 38 ++++++++---- .../key/java/visitor/ProgramContextAdder.java | 43 +++++++++++--- .../uka/ilkd/key/logic/MethodStackInfo.java | 6 +- ...Prefix.java => PossibleProgramPrefix.java} | 10 ++-- .../de/uka/ilkd/key/pp/PrettyPrinter.java | 7 ++- .../java/de/uka/ilkd/key/proof/NodeInfo.java | 2 +- .../de/uka/ilkd/key/proof/TacletIndex.java | 2 +- .../rule/AbstractAuxiliaryContractRule.java | 8 ++- .../ilkd/key/rule/LoopScopeInvariantRule.java | 10 ++-- .../key/rule/UseOperationContractRule.java | 14 ++++- .../rule/conditions/IsLabeledCondition.java | 4 +- .../feature/ThrownExceptionFeature.java | 11 ++-- .../de/uka/ilkd/key/proof/rules/javaRules.key | 41 +++++++++++-- .../java_dl/switch/SwitchWithBlock.java | 18 ++++++ 29 files changed, 327 insertions(+), 163 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 f5e94b961aa..b3b2c4b868c 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -1691,7 +1691,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); } @@ -4008,7 +4008,7 @@ public static Pair computeSecondStatement( blocks.addFirst((StatementBlock) firstStatement); } SourceElement lastStatement = null; - while (firstStatement instanceof ProgramPrefix && lastStatement != firstStatement) { + while (firstStatement instanceof PossibleProgramPrefix && lastStatement != firstStatement) { lastStatement = firstStatement; firstStatement = firstStatement.getFirstElementIncludingBlocks(); if (lastStatement instanceof MethodFrame) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java index 1d7ac9e704f..bcb064ab39c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java @@ -15,7 +15,7 @@ import de.uka.ilkd.key.java.visitor.CreatingASTVisitor; import de.uka.ilkd.key.java.visitor.JavaASTVisitor; import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; @@ -36,13 +36,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 04a941a8159..2a8bf62914a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java @@ -4,7 +4,7 @@ package de.uka.ilkd.key.java; import de.uka.ilkd.key.java.ast.statement.MethodFrame; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; public class ProgramPrefixUtil { @@ -26,7 +26,7 @@ public MethodFrame getInnerMostMethodFrame() { } } - public static ProgramPrefixInfo computeEssentials(ProgramPrefix prefix) { + public static ProgramPrefixInfo computeEssentials(PossibleProgramPrefix prefix) { int length = 1; MethodFrame mf = (MethodFrame) (prefix instanceof MethodFrame ? prefix : null); while (prefix.hasNextPrefixElement()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java index 304e085d9f5..c31769533ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.java.ast.statement.MethodFrame; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -144,12 +144,12 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { ExecutionContext lastExecutionContext = null; - final ProgramPrefix prefix; + final PossibleProgramPrefix prefix; int pos = -1; PosInProgram relPos = PosInProgram.TOP; - if (src instanceof ProgramPrefix) { - prefix = (ProgramPrefix) src; + if (src instanceof PossibleProgramPrefix) { + prefix = (PossibleProgramPrefix) src; final int srcPrefixLength = prefix.getPrefixLength(); if (getPrefixLength() > srcPrefixLength) { @@ -158,7 +158,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { pos = srcPrefixLength - getPrefixLength(); - ProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); + PossibleProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); relPos = firstActiveStatement.getFirstActiveChildPos(); @@ -177,7 +177,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); } } @@ -210,8 +210,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(); @@ -247,8 +247,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 @@ -289,10 +289,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(); @@ -315,8 +315,8 @@ private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInPr return prefixEnd; } - private static ProgramPrefix getPrefixElementAt(ProgramPrefix prefix, int i) { - ProgramPrefix current = prefix; + private static PossibleProgramPrefix getPrefixElementAt(PossibleProgramPrefix prefix, int i) { + PossibleProgramPrefix current = prefix; for (int pos = 0; pos < i; pos++) { current = current.getNextPrefixElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java index 97fa68783d1..f1c3dbadeae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java @@ -15,8 +15,7 @@ import de.uka.ilkd.key.java.ast.statement.MethodFrame; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.util.Debug; import org.key_project.util.ExtList; @@ -31,7 +30,7 @@ * Statement block. taken from COMPOST and changed to achieve an immutable structure */ public class StatementBlock extends JavaStatement implements StatementContainer, - TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix { + TypeDeclarationContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Body. @@ -143,10 +142,10 @@ public boolean equals(Object o) { /** * computes the prefix elements for the given array of statment block */ - public static ImmutableArray computePrefixElements( + public static ImmutableArray computePrefixElements( ImmutableArray b, - ProgramPrefix current) { - final ArrayList prefix = new ArrayList<>(); + PossibleProgramPrefix current) { + final ArrayList prefix = new ArrayList<>(); prefix.add(current); while (current.hasNextPrefixElement()) { @@ -290,23 +289,28 @@ public SourceElement getFirstElementIncludingBlocks() { } } + @Override + public boolean isPrefix() { + return !isEmpty(); + } + @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && (body.get(0) instanceof ProgramPrefix); + return !body.isEmpty() && (body.get(0) instanceof PossibleProgramPrefix); } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.get(0); + return (PossibleProgramPrefix) body.get(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() ? ((ProgramPrefix) body.get(0)).getLastPrefixElement() : this; + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? ((PossibleProgramPrefix) body.get(0)).getLastPrefixElement() : this; } @Override @@ -321,7 +325,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/ast/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java index ab3ed1d5267..ab1604ff595 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java @@ -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/ast/statement/BranchStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java index ea185f532f1..ccc5c514697 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.java.ast.NonTerminalProgramElement; import de.uka.ilkd.key.java.ast.PositionInfo; +import de.uka.ilkd.key.java.PositionInfo; import org.key_project.util.ExtList; /** @@ -24,6 +25,11 @@ public BranchStatement() { } + public BranchStatement(PositionInfo pos) { + super(pos); + } + + /** * Constructor for the transformation of COMPOST ASTs to KeY. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java index 1a126a9cc8f..092c4496ad0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java @@ -73,6 +73,11 @@ public int getChildCount() { return result; } + @Override + public SourceElement getFirstElement() { + return body.get(0); + } + /** * Returns the child at the specified index in this node's "virtual" child array * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java index d27b58ebb1e..968c29fc29b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -17,7 +17,7 @@ import org.jspecify.annotations.NonNull; -public class Exec extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Exec extends BranchStatement implements StatementContainer, PossibleProgramPrefix { private final StatementBlock body; private final ImmutableArray branches; private final MethodFrame innerMostMethodFrame; @@ -102,20 +102,20 @@ public Exec(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -130,7 +130,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/ast/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java index 0392aa5e543..58fac67fd09 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java @@ -8,7 +8,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 @@ * Labeled statement. */ 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/ast/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java index e1cb935d7c6..cf1e948dfe2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java @@ -23,7 +23,7 @@ import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; @@ -39,7 +39,7 @@ * @author Dominic Scheurer */ public final class LoopScopeBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { @Nullable private final IProgramVariable indexPV; @@ -105,14 +105,13 @@ public LoopScopeBlock(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() - && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException( "No next prefix element " + this); @@ -120,10 +119,8 @@ public ProgramPrefix getNextPrefixElement() { } @Override - public ProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() - ? getNextPrefixElement().getLastPrefixElement() - : this; + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @Override @@ -137,7 +134,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/ast/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java index 0fa3796d456..85c050c24d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.ast.reference.IExecutionContext; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.util.Debug; @@ -21,7 +21,7 @@ * The statement inserted by KeY if a method call is executed. */ public class MethodFrame extends JavaStatement - implements StatementContainer, ProgramPrefix { + implements StatementContainer, PossibleProgramPrefix { /** * result @@ -118,20 +118,20 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext, @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -146,7 +146,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/ast/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java index 1c7a5cfe029..9cb4055cc81 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java @@ -9,28 +9,24 @@ import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; -import de.uka.ilkd.key.logic.op.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. @@ -76,7 +72,24 @@ public Switch(Expression e) { * 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); @@ -93,8 +106,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(); @@ -206,7 +219,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); } @@ -219,7 +232,7 @@ public SwitchBranch getBranchAt(int index) { * * @return the array wrapper of the branches */ - public ImmutableArray getBranchList() { + public ImmutableArray getBranchList() { return branches; } @@ -240,23 +253,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; } @@ -271,7 +291,7 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { return StatementBlock.computePrefixElements(this); } @@ -284,7 +304,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/ast/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java index 009ddf66522..a1309fc80c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.java.ast.reference.MetaClassReference; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.ProgramVariable; import org.key_project.util.ExtList; @@ -23,7 +23,7 @@ */ public class SynchronizedBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { /** * Expression. @@ -103,22 +103,27 @@ public SynchronizedBlock(PositionInfo pi, List c, Expression expr, Stat this.prefixLength = prefixLength; } + @Override + public boolean isPrefix() { + return expressionWithoutSideffects(); + } + @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -133,7 +138,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/ast/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java index b7aeb68c314..25a2db99ad5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Try.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -21,7 +21,7 @@ * * @author AutoDoc */ -public class Try extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Try extends BranchStatement implements StatementContainer, PossibleProgramPrefix { private final StatementBlock body; private final ImmutableArray branches; @@ -110,20 +110,20 @@ public Try(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -138,7 +138,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 87399eb13ab..d03c483cef7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -365,13 +365,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 @@ -1238,13 +1243,22 @@ ProgramElement createNewElement(ExtList changeList) { @Override public void performActionOnSwitch(Switch x) { - DefaultAction def = new DefaultAction(x) { - @Override - ProgramElement createNewElement(ExtList changeList) { - return new Switch(changeList); + var changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + var pos = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pos = PositionInfo.UNDEFINED; } - }; - def.doAction(x); + Expression expr = changeList.removeFirstOccurrence(Expression.class); + var branches = changeList.collect(SwitchBranch.class); + changeList.clear(); + var sw = new Switch(pos, expr, branches); + addChild(sw); + changed(); + } else { + doDefaultAction(x); + } } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index b3fcc7b069a..f83bc452153 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 @@ -58,10 +58,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 { @@ -70,7 +72,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) { @@ -80,9 +82,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())); } @@ -91,7 +98,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 @@ -170,11 +177,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 65a00e3eeaf..4bf41d4d2de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java @@ -29,9 +29,9 @@ public MethodStackInfo(ProgramElement element) { */ public ImmutableList getMethodStack() { ImmutableList list = ImmutableSLList.nil(); - if (element instanceof ProgramPrefix) { - final ImmutableArray prefix = - ((ProgramPrefix) element).getPrefixElements(); + if (element instanceof PossibleProgramPrefix) { + final ImmutableArray prefix = + ((PossibleProgramPrefix) element).getPrefixElements(); for (int i = prefix.size() - 1; i >= 0; i--) { if (prefix.get(i) instanceof MethodFrame frame) { IProgramMethod method = frame.getProgramMethod(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java b/key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java similarity index 79% rename from key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java rename to key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java index 4ce2b84489b..041a9b40942 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 fa6dfbc7500..93bf440ace0 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 @@ -21,7 +21,8 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.JTerm; 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; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -854,7 +855,7 @@ public void performActionOnClassInitializer(ClassInitializer x) { protected void performActionOnStatement(SourceElement s) { layouter.beginRelativeC(0); - boolean validStatement = !(s instanceof CatchAllStatement || s instanceof ProgramPrefix + boolean validStatement = !(s instanceof CatchAllStatement || (s instanceof PossibleProgramPrefix pre && pre.isPrefix()) || s instanceof TypeDeclarationContainer); if (validStatement) { markStart(s); @@ -1781,8 +1782,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 81f41480bb1..387c610bc2b 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 @@ -192,7 +192,7 @@ public static SourceElement computeActiveStatement(SourceElement firstStatement) // TODO: unify with MiscTools getActiveStatement if (firstStatement != null) { activeStatement = firstStatement; - while ((activeStatement instanceof ProgramPrefix) + while ((activeStatement instanceof PossibleProgramPrefix pre && pre.isPrefix()) && !(activeStatement instanceof StatementBlock)) { activeStatement = activeStatement.getFirstElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java index ba4ac6faa49..887099e288a 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 @@ -318,7 +318,7 @@ private ImmutableList getJavaTacletList( HashMap> map, ProgramElement pe, PrefixOccurrences prefixOccurrences) { ImmutableList res = ImmutableSLList.nil(); - if (pe instanceof ProgramPrefix nt) { + if (pe instanceof PossibleProgramPrefix nt) { int next = prefixOccurrences.occurred(pe); if (next < nt.getChildCount()) { return getJavaTacletList(map, nt.getChildAt(next), prefixOccurrences); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index 790dafb48d8..1485ad47157 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 @@ -11,8 +11,10 @@ import de.uka.ilkd.key.java.ast.reference.ExecutionContext; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.ldt.JavaDLTheory; -import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.PosInOccurrence; +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.*; import de.uka.ilkd.key.proof.Goal; @@ -291,7 +293,7 @@ private static ExecutionContext extractExecutionContext(final MethodFrame frame) private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract( final JModality modality, final Goal goal) { SourceElement element = modality.programBlock().program().getFirstElement(); - while ((element instanceof ProgramPrefix || element instanceof CatchAllStatement) + while ((element instanceof PossibleProgramPrefix pre && pre.isPrefix() || element instanceof CatchAllStatement) && !(element instanceof StatementBlock && ((StatementBlock) element).isEmpty())) { if (element instanceof StatementBlock && hasApplicableContracts(services, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index 9a1a248c4e6..640da30894b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -19,7 +19,10 @@ import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PosInOccurrence; +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; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; @@ -407,9 +410,8 @@ private Pair, Statement> findLoopLabel( Optional