diff --git a/.github/workflows/update_symbex_oracles.yml b/.github/workflows/update_symbex_oracles.yml index bdc55edd5b2..6e6070a383c 100644 --- a/.github/workflows/update_symbex_oracles.yml +++ b/.github/workflows/update_symbex_oracles.yml @@ -24,7 +24,7 @@ jobs: distribution: 'temurin' - name: Build with Gradle - uses: gradle/gradle-build-action@v2.3.3 + uses: gradle/gradle-build-action@v2 with: arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test diff --git a/README.md b/README.md index 5d7b54a62bb..8c7d1ef4cc4 100644 --- a/README.md +++ b/README.md @@ -2,14 +2,25 @@ [![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQL](https://github.com/KeYProject/key/actions/workflows/codeql.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/codeql.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml) -This repository contains the interactive theorem prover "KeY" for the verification of Java programs. +This repository is the home of the interactive theorem prover KeY for formal verification and analysis of Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a library e.g. for symbolic program execution, first order reasoning, or test case generation. -You can find more information about KeY on https://key-project.org or use the -documentation in the companion repository [key-docs](https://github.com/KeYProject/key-docs). -The content of the latter is also available as HTML version under https://keyproject.github.io/key-docs/. +For more information, refer to -The current version of KeY is 2.10.0, licensed under GPL v2. +* [The KeY homepage](https://key-project.org) +* [The KeY book](https://www.key-project.org/thebook2/) +* [The KeY developer documentation](https://keyproject.github.io/key-docs/) +* KeY's success stories: + * [Severe bug discovered in JDK sorting routine (TimSort)](http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/), + * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4), + * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/) +The current version of KeY is 2.12.0, licensed under GPL v2. + + +Feel free to use the project templates to get started using KeY: +* [For Verification Projects](https://github.com/KeYProject/verification-project-template) +* [Using as a Library](https://github.com/KeYProject/key-java-example) +* [Using as a Symbolic Execution Backend](https://github.com/KeYProject/key-symbex-example) ## Requirements @@ -85,7 +96,13 @@ Assuming you are in the directory of this README file, you can create a runnable # Issues and Bug Reports -If you encounter problems, please send a message to support@key-project.org +* For bug reports, please use the [issue tracker](https://github.com/KeYProject/key/issues) or send a mail to support@key-project.org. + +* For discussions, you may want to subscribe and use the mailing list or use [GitHub discussions](https://github.com/KeYProject/key/discussions). + +# Contributing to KeY + +Feel free to submit [pull requests](https://github.com/KeYProject/key/pulls) via GitHub. Pull requests are assessed using automatic tests, formatting and static source checkers, as well as a manual review by one of the developers. More guidelines and documentation for the KeY development can be found under [key-docs](https://keyproject.github.io/key-docs/devel/). diff --git a/build.gradle b/build.gradle index b5f73b66e36..ca72be8edcc 100644 --- a/build.gradle +++ b/build.gradle @@ -21,7 +21,7 @@ plugins { // id "com.github.ben-manes.versions" version "0.39.0" // Code formatting - id "com.diffplug.spotless" version "6.20.0" + id "com.diffplug.spotless" version "6.22.0" } // Configure this project for use inside IntelliJ: @@ -78,7 +78,7 @@ subprojects { } dependencies { - implementation("org.slf4j:slf4j-api:2.0.7") + implementation("org.slf4j:slf4j-api:2.0.9") testImplementation("ch.qos.logback:logback-classic:1.4.11") //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java index ea49e8bd3b3..94addf6468f 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java @@ -204,47 +204,23 @@ private void checkFlows() { @Override public void startElement(String uri, String localName, String qName, Attributes attributes) { - switch (localName) { - case "sourcedompair": - case "source": - startSources(); - break; - case "sinkdompair": - case "sink": - startSinks(); - break; - case "category": // TODO: different semantics in "domains" and "sinkdompair" + case "sourcedompair", "source" -> startSources(); + case "sinkdompair", "sink" -> startSinks(); + case "category" -> // TODO: different semantics in "domains" and "sinkdompair" setCategory(attributes); - break; - case "assign": - assignHandle(attributes); - break; + case "assign" -> assignHandle(attributes); + // case "domainassignment": - case "domains": - startDomains(); - break; - case "domain": - putDomain(attributes); - break; - case "assignable": - setAssignable(attributes); - break; - case "field": - putField(attributes); - break; - case "parameter": - putParam(attributes); - break; - case "returnvalue": - putReturn(attributes); - break; - case "flowrelation": - startFlow(); - break; - case "flow": - putFlow(attributes); - break; + case "domains" -> startDomains(); + case "domain" -> putDomain(attributes); + case "assignable" -> setAssignable(attributes); + case "field" -> putField(attributes); + case "parameter" -> putParam(attributes); + case "returnvalue" -> putReturn(attributes); + case "flowrelation" -> startFlow(); + case "flow" -> putFlow(attributes); + // a lot of elements without their own semantics // case "riflspec": // case "attackerio": @@ -252,33 +228,25 @@ public void startElement(String uri, String localName, String qName, Attributes // case "bottom": // case "source": // case "sink": - case "dompair": // TODO - // case "domainhierarchy": - case "flowpair": // TODO - // case "flowpolicy": - default: + // TODO + // case "domainhierarchy": + // TODO + // case "flowpolicy": + default -> { + } } } @Override public void endElement(String uri, String localName, String qName) { switch (localName) { - case "assignable": - unsetAssignable(); - break; - case "category": - unsetCategory(); - break; - case "domains": - checkDomains(); - break; - case "domainassignment": - checkDomainAssignmentsWithFlows(); - break; - case "flowrelation": - checkFlows(); - break; - default: + case "assignable" -> unsetAssignable(); + case "category" -> unsetCategory(); + case "domains" -> checkDomains(); + case "domainassignment" -> checkDomainAssignmentsWithFlows(); + case "flowrelation" -> checkFlows(); + default -> { + } } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java index 4a0e30d57b9..b49e9b3751b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java @@ -408,7 +408,7 @@ public void startElement(String uri, String localName, String qName, Attributes * {@inheritDoc} */ @Override - public void endElement(String uri, String localName, String qName) throws SAXException { + public void endElement(String uri, String localName, String qName) { if (isConstraint(uri, localName, qName)) { // Nothing to do. } else if (isCallStateVariable(uri, localName, qName)) { @@ -1823,7 +1823,7 @@ public static class KeYlessTermination extends AbstractKeYlessExecutionNode parent, String name, @@ -2887,7 +2887,7 @@ public static class KeYlessVariable extends AbstractKeYlessExecutionElement /** * Constructor. * - * @param parentVariable The parent {@link IExecutionValue} if available. + * @param parentValue The parent {@link IExecutionValue} if available. * @param isArrayIndex The is array flag. * @param arrayIndexString The array index. * @param name The name. @@ -3026,7 +3026,7 @@ public IExecutionNode getTarget() { /** * Sets the source. * - * @param target The source to set. + * @param source The source to set. */ public void setSource(IExecutionNode source) { this.source = source; @@ -3159,7 +3159,7 @@ public IExecutionVariable getVariable() { * {@inheritDoc} */ @Override - public IExecutionVariable[] getChildVariables() throws ProofInputException { + public IExecutionVariable[] getChildVariables() { return childVariables.toArray(new IExecutionVariable[0]); } @@ -3216,7 +3216,7 @@ public void addConstraint(IExecutionConstraint constraint) { * {@inheritDoc} */ @Override - public IExecutionConstraint[] getConstraints() throws ProofInputException { + public IExecutionConstraint[] getConstraints() { return constraints.toArray(new IExecutionConstraint[0]); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java index deaa769c55d..bfb10ac3e91 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java @@ -119,8 +119,7 @@ protected void updateRelevantLocations(final ProgramElement read, if (relevantElement != null) { Location normalizedElement = normalizeAlias(services, relevantElement, info); relevantLocations.add(normalizedElement); - } else if (read instanceof NonTerminalProgramElement) { - NonTerminalProgramElement ntpe = (NonTerminalProgramElement) read; + } else if (read instanceof NonTerminalProgramElement ntpe) { for (int i = 0; i < ntpe.getChildCount(); i++) { updateRelevantLocations(ntpe.getChildAt(i), relevantLocations, info, services); } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java index db6f015b607..de0aaf772bb 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java @@ -430,24 +430,12 @@ private boolean checkBraces(final StringBuilder buf) { int edged = 0; for (int i = 0; i < buf.length(); i++) { switch (buf.charAt(i)) { - case '{': - curly++; - break; - case '}': - curly--; - break; - case '(': - round++; - break; - case ')': - round--; - break; - case '[': - edged++; - break; - case ']': - edged--; - break; + case '{' -> curly++; + case '}' -> curly--; + case '(' -> round++; + case ')' -> round--; + case '[' -> edged++; + case ']' -> edged--; } } if (curly == 0 && round == 0 && edged == 0) { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java index 00effd2f09e..92b17312e1a 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java @@ -234,18 +234,16 @@ public OracleTerm generateOracle(Term term, boolean initialSelect) { OracleTerm left = generateOracle(term.sub(0), initialSelect); OracleTerm right = generateOracle(term.sub(1), initialSelect); String javaOp = ops.get(op); + return switch (javaOp) { + case EQUALS -> eq(left, right); + case AND -> and(left, right); + case OR -> or(left, right); + default -> + // Todo wiesler: What is this for? No field nor method of OracleBinTerm has any + // usages + new OracleBinTerm(javaOp, left, right); + }; - switch (javaOp) { - case EQUALS: - return eq(left, right); - case AND: - return and(left, right); - case OR: - return or(left, right); - } - - // Todo wiesler: What is this for? No field nor method of OracleBinTerm has any usages - return new OracleBinTerm(javaOp, left, right); } // negation else if (op == Junctor.NOT) { OracleTerm sub = generateOracle(term.sub(0), initialSelect); diff --git a/key.core/build.gradle b/key.core/build.gradle index be5910e7747..62895ba3c50 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -18,8 +18,8 @@ dependencies { javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' antlr group: 'org.antlr', name: 'antlr', version: '3.5.3' // use ANTLR version 3 - antlr4 "org.antlr:antlr4:4.13.0" - api "org.antlr:antlr4-runtime:4.13.0" + antlr4 "org.antlr:antlr4:4.13.1" + api "org.antlr:antlr4-runtime:4.13.1" //implementation group: 'com.google.guava', name: 'guava', version: '28.1-jre' } diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 8851ba9cebc..926780ad4c4 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -36,7 +36,7 @@ decls problem : - ( PROBLEM LBRACE a=term RBRACE + ( PROBLEM LBRACE ( t=termorseq ) RBRACE | CHOOSECONTRACT (chooseContract=string_value SEMI)? | PROOFOBLIGATION (proofObligation=string_value SEMI)? ) diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java b/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java index 543efa937d2..bd23b64bc18 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java @@ -17,12 +17,13 @@ * @version 1 (21.04.17) */ public class ProofScriptCommandApi { - private final Map commandMap = new HashMap<>(); + private final Map> commandMap = new HashMap<>(); public ProofScriptCommandApi() { initialize(); } + @SuppressWarnings("rawtypes") private void initialize() { ServiceLoader loader = ServiceLoader.load(ProofScriptCommand.class); loader.forEach(psc -> commandMap.put(psc.getName(), psc)); @@ -35,7 +36,7 @@ private void initialize() { * * @return a collection of proof script commands */ - public Collection getScriptCommands() { + public Collection> getScriptCommands() { return commandMap.values(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java b/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java index 6e9995109b1..1f4573e5f3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java @@ -7,7 +7,6 @@ import de.uka.ilkd.key.java.declaration.TypeDeclaration; import de.uka.ilkd.key.java.declaration.TypeDeclarationContainer; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.pp.PrettyPrinter; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -242,10 +241,4 @@ public void visit(Visitor v) { } - /** toString */ - public String toString() { - PrettyPrinter pp = PrettyPrinter.purePrinter(); - pp.print(this); - return pp.result(); - } } 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 f8d3d329ac0..0d3b0f3f3e0 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 @@ -83,10 +83,6 @@ public static MethodFrame getInnermostMethodFrame(ProgramElement pe, Services se final MethodFrame result = new JavaASTVisitor(pe, services) { private MethodFrame res; - protected void doAction(ProgramElement node) { - node.visit(this); - } - protected void doDefaultAction(SourceElement node) { if (node instanceof MethodFrame && res == null) { res = (MethodFrame) node; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index e82ce386636..8e21443c5ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -57,17 +57,17 @@ /** * Objects of this class can be used to transform an AST returned by the recoder library to the * corresponding yet immutable KeY data structures. - * + *

* Call the method process() to convert an arbitrary object. - * + *

* The method callConvert is used to perform a run-time dispatch upon the parameters. - * + *

* The actual conversion is done in convert-methods which must be declared public due to the used * reflection method lookup function. - * + *

* There is a general method {@link #callConvert(recoder.java.ProgramElement)} that does the job in * general. Several special cases must be treated separately. - * + *

* This code used to be part of {@link Recoder2KeY} and has been 'out-sourced'. * * @author mattias ulbrich @@ -216,10 +216,10 @@ private boolean isParsingLibs() { /** * convert a recoder ProgramElement to a corresponding KeY data structure entity. - * + *

* Almost always the returned type carries the same Classname but in a KeY rather than a recoder * package. - * + *

* Determines the right convert method using reflection * * @param pe the recoder.java.JavaProgramElement to be converted, not null. @@ -304,7 +304,7 @@ protected Object callConvert(recoder.java.ProgramElement pe) throws ConvertExcep /** * iterate over all children and call convert upon them. Gather the resulting KeY structures in * an ExtList. - * + *

* In addition to the child ast-branches, all comments are gathered also. * * @param pe the NonTerminalProgramElement that needs its children before being converted @@ -396,32 +396,24 @@ private PositionInfo positionInfo(recoder.java.SourceElement se) { * @return a literal constant representing the value of p_er */ private Literal getLiteralFor(recoder.service.ConstantEvaluator.EvaluationResult p_er) { - switch (p_er.getTypeCode()) { - case recoder.service.ConstantEvaluator.BOOLEAN_TYPE: - return BooleanLiteral.getBooleanLiteral(p_er.getBoolean()); - case recoder.service.ConstantEvaluator.CHAR_TYPE: - return new CharLiteral(p_er.getChar()); - case recoder.service.ConstantEvaluator.DOUBLE_TYPE: - return new DoubleLiteral(p_er.getDouble()); - case recoder.service.ConstantEvaluator.FLOAT_TYPE: - return new FloatLiteral(p_er.getFloat()); - case recoder.service.ConstantEvaluator.BYTE_TYPE: - return new IntLiteral(p_er.getByte()); - case recoder.service.ConstantEvaluator.SHORT_TYPE: - return new IntLiteral(p_er.getShort()); - case recoder.service.ConstantEvaluator.INT_TYPE: - return new IntLiteral(p_er.getInt()); - case recoder.service.ConstantEvaluator.LONG_TYPE: - return new LongLiteral(p_er.getLong()); - case recoder.service.ConstantEvaluator.STRING_TYPE: - if (p_er.getString() == null) { - return NullLiteral.NULL; + return switch (p_er.getTypeCode()) { + case recoder.service.ConstantEvaluator.BOOLEAN_TYPE -> BooleanLiteral.getBooleanLiteral(p_er.getBoolean()); + case recoder.service.ConstantEvaluator.CHAR_TYPE -> new CharLiteral(p_er.getChar()); + case recoder.service.ConstantEvaluator.DOUBLE_TYPE -> new DoubleLiteral(p_er.getDouble()); + case recoder.service.ConstantEvaluator.FLOAT_TYPE -> new FloatLiteral(p_er.getFloat()); + case recoder.service.ConstantEvaluator.BYTE_TYPE -> new IntLiteral(p_er.getByte()); + case recoder.service.ConstantEvaluator.SHORT_TYPE -> new IntLiteral(p_er.getShort()); + case recoder.service.ConstantEvaluator.INT_TYPE -> new IntLiteral(p_er.getInt()); + case recoder.service.ConstantEvaluator.LONG_TYPE -> new LongLiteral(p_er.getLong()); + case recoder.service.ConstantEvaluator.STRING_TYPE -> { + if (p_er.getString() == null) { + yield NullLiteral.NULL; + } + yield new StringLiteral("\"" + p_er.getString() + "\""); } - return new StringLiteral("\"" + p_er.getString() + "\""); - default: - throw new ConvertException( - "Don't know how to handle type " + p_er.getTypeCode() + " of " + p_er); - } + default -> throw new ConvertException( + "Don't know how to handle type " + p_er.getTypeCode() + " of " + p_er); + }; } @@ -464,9 +456,9 @@ private ProgramVariable find(String name, ImmutableList fields) { /** * The default procedure. - * + *

* It iterates over all children, calls convert upon them - * + *

* collect all children, convert them. Create a new instance of the corresponding KeY class and * call its constructor with the list of children. * @@ -567,7 +559,7 @@ private String getKeYName(Class recod /** * determines the right standard constructor of the KeYClass. - * + *

* Use a cache to only look up classes once. * * @param recoderClass the Class of the recoder AST object diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 8a0ff3c8dce..1b0a1f4c1bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -185,12 +185,6 @@ public MethodFrame convert(de.uka.ilkd.key.java.recoderext.RMethodCallStatement (StatementBlock) callConvert(l.getBody())); } - public LoopScopeBlock convert(de.uka.ilkd.key.java.recoderext.LoopScopeBlock l) { - return new LoopScopeBlock( - (de.uka.ilkd.key.logic.op.IProgramVariable) callConvert(l.getIndexPV()), - (StatementBlock) callConvert(l.getBody())); - } - /** * translate method body statements. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java index 7cdd80bb1ec..ff1a653287a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java @@ -23,18 +23,11 @@ public abstract class Operator extends JavaNonTerminalProgramElement implements Expression, ExpressionContainer { - - - /** - * Children. - */ protected final ImmutableArray children; - /** * Relative positioning of the operator. */ - public static final int PREFIX = 0; public static final int INFIX = 1; public static final int POSTFIX = 2; @@ -123,37 +116,25 @@ public boolean isLeftAssociative() { } public SourceElement getFirstElement() { - switch (getNotation()) { - case INFIX: - case POSTFIX: - return children.get(0).getFirstElement(); - case PREFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, POSTFIX -> children.get(0).getFirstElement(); + default -> this; + }; } @Override public SourceElement getFirstElementIncludingBlocks() { - switch (getNotation()) { - case INFIX: - case POSTFIX: - return children.get(0).getFirstElementIncludingBlocks(); - case PREFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, POSTFIX -> children.get(0).getFirstElementIncludingBlocks(); + default -> this; + }; } public SourceElement getLastElement() { - switch (getNotation()) { - case INFIX: - case PREFIX: - return children.get(getArity() - 1).getLastElement(); - case POSTFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, PREFIX -> children.get(getArity() - 1).getLastElement(); + default -> this; + }; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java index 23d197a71fe..f2f60d7b999 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java @@ -33,29 +33,6 @@ public ParenthesizedExpression(Expression child) { super(child); } - /** - * Returns the number of children of this node. - * - * @return an int giving the number of children of this node - */ - public int getChildCount() { - return (children != null) ? children.size() : 0; - } - - /** - * 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) { - if (children != null) { - return children.get(index); - } - throw new ArrayIndexOutOfBoundsException(); - } - /** * Get arity. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java index a758c9d87c3..ebf7131ff37 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java @@ -36,7 +36,7 @@ public CharLiteral(char charVal) { * the Java 8 Language Specification: chars written directly (like 'a', '0', 'Z'), Java escape * chars (like '\n', '\r'), and octal Unicode escapes (like '\040'). Note that unicode escapes * in hexadecimal form are processed earlier and don't have to be handled here. - * + *

* Note that the char must be enclosed in single-quotes. * * @param children an ExtList with all children(comments). May contain: Comments @@ -94,7 +94,7 @@ public String getValueString() { * 'a', '0', 'Z'), Java escape chars (like '\n', '\r'), and octal Unicode escapes (like '\040'). * Note that unicode escapes in hexadecimal form are processed earlier and don't have to be * handled by this method. - * + *

* This method does not check the length of the literal for validity. * * @param sourceStr the String containing the literal surrounded by single-quotes @@ -116,37 +116,20 @@ protected char parseFromString(final String sourceStr) { * 3. octal Unicode escape like '\040' */ if (valStr.charAt(0) == '\\') { - switch (valStr.charAt(1)) { - case 'b': - return '\b'; - case 't': - return '\t'; - case 'n': - return '\n'; - case 'f': - return '\f'; - case 'r': - return '\r'; - case '\"': - return '\"'; - case '\'': - return '\''; - case '\\': - return '\\'; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - return (char) Integer.parseInt(valStr.substring(1), 8); - case 'u': - return (char) Integer.parseInt(valStr.substring(2), 16); - default: - throw new NumberFormatException("Invalid char: " + sourceStr); - } + return switch (valStr.charAt(1)) { + case 'b' -> '\b'; + case 't' -> '\t'; + case 'n' -> '\n'; + case 'f' -> '\f'; + case 'r' -> '\r'; + case '\"' -> '\"'; + case '\'' -> '\''; + case '\\' -> '\\'; + case '0', '1', '2', '3', '4', '5', '6', '7' -> (char) Integer + .parseInt(valStr.substring(1), 8); + case 'u' -> (char) Integer.parseInt(valStr.substring(2), 16); + default -> throw new NumberFormatException("Invalid char: " + sourceStr); + }; } else { return valStr.charAt(0); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java index 3958ed20807..31b4797f03f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java @@ -5,7 +5,6 @@ import de.uka.ilkd.key.logic.op.SchemaVariable; -import recoder.java.SourceElement; import recoder.java.SourceVisitor; public class ExecCtxtSVWrapper extends ExecutionContext implements KeYRecoderExtension, SVWrapper { @@ -37,10 +36,6 @@ public SchemaVariable getSV() { return sv; } - public SourceElement getFirstElement() { - return this; - } - public ExecutionContext deepClone() { return new ExecCtxtSVWrapper(sv); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java index bf2a57d60cd..576e3d8d0dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java @@ -6,9 +6,7 @@ import de.uka.ilkd.key.logic.op.SchemaVariable; import recoder.java.Expression; -import recoder.java.ExpressionContainer; import recoder.java.LoopInitializer; -import recoder.java.NonTerminalProgramElement; import recoder.java.SourceVisitor; import recoder.java.StatementContainer; import recoder.java.expression.Literal; @@ -48,15 +46,6 @@ public ExpressionSVWrapper(SchemaVariable sv) { public void makeParentRoleValid() { } - /** - * Get AST parent. - * - * @return the non terminal program element. - */ - public NonTerminalProgramElement getASTParent() { - return expressionParent; - } - /** * sets the schema variable of sort statement @@ -73,24 +62,6 @@ public SchemaVariable getSV() { } - /** - * Get expression container. - * - * @return the expression container. - */ - public ExpressionContainer getExpressionContainer() { - return expressionParent; - } - - /** - * Set expression container. - * - * @param c an expression container. - */ - public void setExpressionContainer(ExpressionContainer c) { - expressionParent = c; - } - // don't think we need it public void accept(SourceVisitor v) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java index 4de44319c30..87c826ea835 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java @@ -28,7 +28,7 @@ * The Java DL requires some implicit fields, that are available in each Java class. The name of the * implicit fields is usually enclosed between two angle brackets. To access the fields in a uniform * way, they are added as usual fields to the classes, in particular this allows us to parse them in - * more easier. For further information see also + * easier. For further information see also *

    *
  • {@link ImplicitFieldAdder}
  • *
  • {@link CreateObjectBuilder}
  • @@ -43,7 +43,7 @@ public abstract class RecoderModelTransformer extends TwoPassTransformation { protected final TransformerCache cache; /** - * creates a transormder for the recoder model + * creates a transformer for the recoder model * * @param services the CrossReferenceServiceConfiguration to access model information * @param cache a cache object that stores information which is needed by and common to many @@ -67,45 +67,32 @@ public Expression getDefaultValue(Type type) { if (type instanceof ClassType || type instanceof ArrayType) { return new NullLiteral(); } else if (type instanceof PrimitiveType) { - switch (type.getName()) { - case "boolean": - return new BooleanLiteral(false); - case "byte": - case "short": - case "int": - case "\\bigint": - return new IntLiteral(0); - case "long": - return new LongLiteral(0); - case "\\real": - return new RealLiteral(); - case "char": - return new CharLiteral((char) 0); - case "float": - return new FloatLiteral(0.0F); - case "double": - return new DoubleLiteral(0.0D); - case "\\locset": - return EmptySetLiteral.INSTANCE; - case "\\seq": - return EmptySeqLiteral.INSTANCE; - case "\\set": - return new DLEmbeddedExpression("emptySet", Collections.emptyList()); - case "\\free": - return new DLEmbeddedExpression("atom", Collections.emptyList()); - case "\\map": - return EmptyMapLiteral.INSTANCE; - default: - if (type.getName().startsWith("\\dl_")) { - // The default value of a type is resolved later, then we know the Sort of the - // type - return new DLEmbeddedExpression( - "\\dl_DEFAULT_VALUE_" + type.getName().substring(4), - Collections.emptyList()); + return switch (type.getName()) { + case "boolean" -> new BooleanLiteral(false); + case "byte", "short", "int", "\\bigint" -> new IntLiteral(0); + case "long" -> new LongLiteral(0); + case "\\real" -> new RealLiteral(); + case "char" -> new CharLiteral((char) 0); + case "float" -> new FloatLiteral(0.0F); + case "double" -> new DoubleLiteral(0.0D); + case "\\locset" -> EmptySetLiteral.INSTANCE; + case "\\seq" -> EmptySeqLiteral.INSTANCE; + case "\\set" -> new DLEmbeddedExpression("emptySet", Collections.emptyList()); + case "\\free" -> new DLEmbeddedExpression("atom", Collections.emptyList()); + case "\\map" -> EmptyMapLiteral.INSTANCE; + default -> { + if (type.getName().startsWith("\\dl_")) { + // The default value of a type is resolved later, then we know the Sort of the + // type + yield new DLEmbeddedExpression( + "\\dl_DEFAULT_VALUE_" + type.getName().substring(4), + Collections.emptyList()); + } + Debug.fail("makeImplicitMembersExplicit: unknown primitive type" + type); + yield null; } - } + }; } - Debug.fail("makeImplicitMembersExplicit: unknown primitive type" + type); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java index 33e1bdc01ea..cd2d6630b33 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java @@ -54,24 +54,6 @@ public NonTerminalProgramElement getASTParent() { } - /** - * Get expression container. - * - * @return the expression container. - */ - public ExpressionContainer getExpressionContainer() { - return expressionParent; - } - - /** - * Set expression container. - * - * @param c an expression container. - */ - public void setExpressionContainer(ExpressionContainer c) { - expressionParent = c; - } - // don't think we need it public void accept(SourceVisitor v) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java index b0cd9859efe..c4797a78e2a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java @@ -38,12 +38,6 @@ public int getArity() { } - @Override - public int getPrecedence() { - return 0; - } - - @Override public int getNotation() { return PREFIX; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java index 8fd2827d609..9e4758638bd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java @@ -76,15 +76,6 @@ public ProgramElement getChildAt(int index) { throw new ArrayIndexOutOfBoundsException(); } - /** - * Get reference prefix. - * - * @return the reference prefix. - */ - public ReferencePrefix getReferencePrefix() { - return prefix; - } - /** * Get reference prefix. * @@ -105,16 +96,6 @@ public ReferencePrefix setReferencePrefix(ReferencePrefix rp) { } - /** - * Get the number of type references in this container. - * - * @return the number of type references. - */ - - public int getTypeReferenceCount() { - return (prefix instanceof TypeReference) ? 1 : 0; - } - /** * Return the type reference at the specified index in this node's "virtual" type reference * array. @@ -130,15 +111,6 @@ public TypeReference getTypeReferenceAt(int index) { throw new ArrayIndexOutOfBoundsException(); } - /** - * Get the number of expressions in this container. - * - * @return the number of expressions. - */ - public int getExpressionCount() { - return (prefix instanceof Expression) ? 1 : 0; - } - /** * Return the expression at the specified index in this node's "virtual" expression array. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java index 49cf1d19e0b..609ecaf1d38 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java @@ -50,10 +50,6 @@ public Do(Expression guard, Statement body, PositionInfo pos) { super(guard, body, pos); } - public SourceElement getLastElement() { - return this; - } - /** * Is checked before iteration. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java index 2ac2ec578c6..165a48b1190 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java @@ -14,8 +14,6 @@ import de.uka.ilkd.key.java.declaration.ImplicitFieldSpecification; import de.uka.ilkd.key.java.declaration.VariableSpecification; import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramConstant; /** * The DeclarationProgramVariableCollector collects all top level declared program variables @@ -71,12 +69,4 @@ public void performActionOnImplicitFieldSpecification(ImplicitFieldSpecification addVariable(x.getProgramVariable()); } - public void performActionOnLocationVariable(LocationVariable x) { - performActionOnProgramVariable(x); - } - - public void performActionOnProgramConstant(ProgramConstant x) { - performActionOnProgramVariable(x); - } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java index a5a36c0c8a1..a8a738e456f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java @@ -38,14 +38,6 @@ public ProgramReplaceVisitor(ProgramElement root, Services services, SVInstantia svinsts = svi; } - /** - * the action that is performed just before leaving the node the last time - */ - @Override - protected void doAction(ProgramElement node) { - node.visit(this); - } - /** starts the walker */ @Override public void start() { @@ -68,11 +60,6 @@ public ProgramElement result() { return result; } - @Override - public String toString() { - return stack.peek().toString(); - } - /** * the implemented default action is called if a program element is, and if it has children all * its children too are left unchanged diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java index 5348f863eee..c2a9364d08d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java @@ -76,9 +76,9 @@ public CharListLDT(TermServices services) { // ------------------------------------------------------------------------- private String translateCharTerm(Term t) { - char charVal = 0; - int intVal = 0; - String result = printlastfirst(t.sub(0)).toString(); + char charVal; + int intVal; + String result = printLastFirst(t.sub(0)).toString(); try { intVal = Integer.parseInt(result); charVal = (char) intVal; @@ -93,11 +93,11 @@ private String translateCharTerm(Term t) { } - private StringBuffer printlastfirst(Term t) { + private StringBuffer printLastFirst(Term t) { if (t.op().arity() == 0) { return new StringBuffer(); } else { - return printlastfirst(t.sub(0)).append(t.op().name().toString()); + return printLastFirst(t.sub(0)).append(t.op().name().toString()); } } @@ -250,12 +250,10 @@ public Type getType(Term t) { @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { // This is not very elegant; but seqConcat is actually in the SeqLDT. - case "add": + if (operationName.equals("add")) { return services.getNamespaces().functions().lookup("seqConcat"); - default: - return null; } + return null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java index b30515b750e..3c9113b467e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java @@ -155,47 +155,29 @@ public Term translateLiteral(Literal lit, Services services) { @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "neg": - return getNeg(); + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "neg" -> getNeg(); // Floating point extensions with "\fp_" - case "nan": - return getIsNaN(); - case "zero": - return getIsZero(); - case "infinite": - return getIsInfinite(); - case "nice": - return getIsNice(); - case "abs": - return getAbs(); - case "negative": - return getIsNegative(); - case "positive": - return getIsPositive(); - case "subnormal": - return getIsSubnormal(); - case "normal": - return getIsNormal(); - } - return null; + case "nan" -> getIsNaN(); + case "zero" -> getIsZero(); + case "infinite" -> getIsInfinite(); + case "nice" -> getIsNice(); + case "abs" -> getAbs(); + case "negative" -> getIsNegative(); + case "positive" -> getIsPositive(); + case "subnormal" -> getIsSubnormal(); + case "normal" -> getIsNormal(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java index 8c694458b75..f4ea89fc7d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java @@ -156,46 +156,28 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "neg": - return getNeg(); + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "neg" -> getNeg(); // Floating point extensions with "\fp_" - case "nan": - return getIsNaN(); - case "zero": - return getIsZero(); - case "infinite": - return getIsInfinite(); - case "nice": - return getIsNice(); - case "abs": - return getAbs(); - case "negative": - return getIsNegative(); - case "positive": - return getIsPositive(); - case "subnormal": - return getIsSubnormal(); - case "normal": - return getIsNormal(); - } - return null; + case "nan" -> getIsNaN(); + case "zero" -> getIsZero(); + case "infinite" -> getIsInfinite(); + case "nice" -> getIsNice(); + case "abs" -> getAbs(); + case "negative" -> getIsNegative(); + case "positive" -> getIsPositive(); + case "subnormal" -> getIsSubnormal(); + case "normal" -> getIsNormal(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java index 644ea234ab7..1df2ea60b98 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java @@ -718,29 +718,19 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Nullable @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "mod": - return getMod(); - case "neg": - return getNeg(); - } - return null; + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "mod" -> getMod(); + case "neg" -> getNeg(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java index b91db6fce27..c8fc40887f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java @@ -213,17 +213,12 @@ public Type getType(Term t) { @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { - case "add": - return getUnion(); - case "sub": - return getSetMinus(); - case "mul": - return getIntersect(); - case "le": - return getSubset(); - default: - return null; - } + return switch (operationName) { + case "add" -> getUnion(); + case "sub" -> getSetMinus(); + case "mul" -> getIntersect(); + case "le" -> getSubset(); + default -> null; + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java index a78f133ef49..34487d51677 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java @@ -104,8 +104,6 @@ public Function getSeqDef() { /** * Placeholder for the sequence of values observed through the execution of an enhanced for * loop. Follows David Cok's proposal to adapt JML to Java5. - * - * @return */ public Function getValues() { return values; @@ -167,12 +165,10 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { - case "add": + if (operationName.equals("add")) { return getSeqConcat(); - default: - return null; } + return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java index 02bf571c002..9a4a79019f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java @@ -134,14 +134,11 @@ public String toString() { */ @Override public Object getChild(int i) { - switch (i) { - case 0: - return getId(); - case 1: - return beforeIds; - default: - return null; - } + return switch (i) { + case 0 -> getId(); + case 1 -> beforeIds; + default -> null; + }; } /** 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 028e69af9f8..a61b890cf76 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 @@ -369,11 +369,6 @@ public ProgramVariableSort() { super(new Name("Variable")); } - @Override - public boolean canStandFor(Term t) { - return t.op() instanceof ProgramVariable; - } - @Override protected boolean canStandFor(ProgramElement pe, Services services) { ProgramVariable accessedField = null; @@ -464,11 +459,6 @@ protected SimpleExpressionSort(Name n) { super(n); } - @Override - public boolean canStandFor(Term t) { - return true; - } - @Override protected boolean canStandFor(ProgramElement pe, Services services) { if (pe instanceof Negative) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java index 2756439fa64..35d358ca81d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java @@ -4,9 +4,9 @@ package de.uka.ilkd.key.macros.scripts; import java.io.File; -import java.io.StringReader; import java.util.Deque; import java.util.LinkedList; +import java.util.Objects; import java.util.Optional; import java.util.function.Consumer; import javax.annotation.Nonnull; @@ -16,7 +16,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.macros.scripts.meta.ValueInjector; -import de.uka.ilkd.key.parser.DefaultTermParser; +import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.proof.Goal; @@ -26,13 +26,13 @@ import org.key_project.util.collection.ImmutableList; +import org.antlr.v4.runtime.CharStreams; + /** * @author Alexander Weigl * @version 1 (28.03.17) */ public class EngineState { - private final static DefaultTermParser PARSER = new DefaultTermParser(); - // private final Map arbitraryVariables = new HashMap<>(); private final Proof proof; private final AbbrevMap abbrevMap = new AbbrevMap(); /** @@ -159,20 +159,16 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { int childCount = node.childrenCount(); switch (childCount) { - case 0: + case 0 -> { result = getGoal(proof.openGoals(), node); - if (!checkAutomatic || result.isAutomatic()) { + if (!checkAutomatic || Objects.requireNonNull(result).isAutomatic()) { // We found our goal break loop; } node = choices.pollLast(); - break; - - case 1: - node = node.child(0); - break; - - default: + } + case 1 -> node = node.child(0); + default -> { Node next = null; for (int i = 0; i < childCount; i++) { Node child = node.child(i); @@ -186,31 +182,39 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { } assert next != null; node = next; - break; + } } } return result; } + public Term toTerm(String string, Sort sort) throws ParserException, ScriptException { - StringReader reader = new StringReader(string); + final var io = getKeyIO(); + var term = io.parseExpression(string); + if (sort == null || term.sort().equals(sort)) + return term; + else + throw new IllegalStateException( + "Unexpected sort for term: " + term + ". Expected: " + sort); + } + + @Nonnull + private KeyIO getKeyIO() throws ScriptException { Services services = proof.getServices(); - return PARSER.parse(reader, sort, services, - getFirstOpenAutomaticGoal().getLocalNamespaces(), abbrevMap); + KeyIO io = new KeyIO(services, getFirstOpenAutomaticGoal().getLocalNamespaces()); + io.setAbbrevMap(abbrevMap); + return io; } - public Sort toSort(String sortName) throws ParserException, ScriptException { + public Sort toSort(String sortName) throws ScriptException { return (getFirstOpenAutomaticGoal() == null ? getProof().getServices().getNamespaces() : getFirstOpenAutomaticGoal().getLocalNamespaces()).sorts().lookup(sortName); } - public Sequent toSequent(String sequent) throws ParserException, ScriptException { - StringReader reader = new StringReader(sequent); - Services services = proof.getServices(); - - return PARSER.parseSeq(reader, services, - getFirstOpenAutomaticGoal().getLocalNamespaces(), getAbbreviations()); + public Sequent toSequent(String sequent) throws ScriptException { + return getKeyIO().parseSequent(CharStreams.fromString(sequent)); } public int getMaxAutomaticSteps() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java index 22261286d39..4f4c84298b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java @@ -110,69 +110,62 @@ public ParsedCommand parseCommand() throws IOException, ScriptException { } switch (c) { - case -1: - if (sb.length() > 0 || key != null || !result.isEmpty()) { + case -1 -> { + if (!sb.isEmpty() || key != null || !result.isEmpty()) { throw new ScriptException("Trailing characters at end of script (missing ';'?)", getLocation()); } return null; - case '=': + } + case '=' -> { switch (state) { - case IN_ID: + case IN_ID -> { state = State.AFTER_EQ; key = sb.toString(); sb.setLength(0); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: - exc(c); } - break; - case ' ': - case '\t': - case '\n': + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> exc(c); + } + } + case ' ', '\t', '\n' -> { switch (state) { - case IN_ID: + case IN_ID -> { state = State.INIT; result.put("#" + (impCounter++), sb.toString()); sb.setLength(0); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_UNQUOTE: + } + case IN_QUOTE -> sb.append((char) c); + case IN_UNQUOTE -> { state = State.INIT; result.put(key, sb.toString()); sb.setLength(0); - break; - case IN_COMMENT: + } + case IN_COMMENT -> { if (c == '\n') { state = stateBeforeComment; } - break; - default: - break; } - break; - case '\r': - break; - case '"': - case '\'': + default -> { + } + } + } + case '\r' -> { + } + case '"', '\'' -> { switch (state) { - case INIT: + case INIT -> { state = State.IN_QUOTE; stringInitChar = c; key = "#" + (impCounter++); - break; - case AFTER_EQ: + } + case AFTER_EQ -> { state = State.IN_QUOTE; stringInitChar = c; - break; - case IN_QUOTE: + } + case IN_QUOTE -> { if (stringInitChar == c) { state = State.INIT; result.put(key, sb.toString()); @@ -180,75 +173,62 @@ public ParsedCommand parseCommand() throws IOException, ScriptException { } else { sb.append((char) c); } - break; - case IN_COMMENT: - break; - default: - exc(c); } - break; - case '#': + case IN_COMMENT -> { + } + default -> exc(c); + } + } + case '#' -> { switch (state) { - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> { stateBeforeComment = state; state = State.IN_COMMENT; } - break; - case ';': + } + } + case ';' -> { switch (state) { - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - case IN_ID: - result.put("#" + (impCounter++), sb.toString()); - break; - case INIT: - break; - case IN_UNQUOTE: - result.put(key, sb.toString()); - break; - default: - exc(c); + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT, INIT -> { + } + case IN_ID -> result.put("#" + (impCounter++), sb.toString()); + case IN_UNQUOTE -> result.put(key, sb.toString()); + default -> exc(c); } if (state != State.IN_COMMENT && state != State.IN_QUOTE) { result.put(LITERAL_KEY, cmdBuilder.toString().trim()); var end = getLocation(); return new ParsedCommand(result, start, end); } - break; - default: + } + default -> { switch (state) { - case INIT: - case IN_ID: + case INIT, IN_ID -> { state = State.IN_ID; // fallthru intended! if (!isIDChar(c)) { exc(c); } sb.append((char) c); - break; - case IN_UNQUOTE: - case AFTER_EQ: + } + case IN_UNQUOTE, AFTER_EQ -> { state = State.IN_UNQUOTE; if (!isIDChar(c)) { exc(c); } sb.append((char) c); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: + } + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> { assert false; } + } + } } if (state != State.IN_COMMENT) { cmdBuilder.append((char) c); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java index e4cca9e09dc..0fb1b181bad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java @@ -104,15 +104,9 @@ private Goal findGoalWith(Function filter, Function g } switch (childCount) { - case 0: - node = choices.pollLast(); - break; - - case 1: - node = node.child(0); - break; - - default: + case 0 -> node = choices.pollLast(); + case 1 -> node = node.child(0); + default -> { Node next = null; for (int i = 0; i < childCount; i++) { Node child = node.child(i); @@ -126,7 +120,7 @@ private Goal findGoalWith(Function filter, Function g } assert next != null; node = next; - break; + } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java index ef30a1b4954..a94da0c5e24 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java @@ -31,7 +31,7 @@ public class ValueInjector { * T --> StringConverter * */ - private final Map converters = new HashMap<>(); + private final Map, StringConverter> converters = new HashMap<>(); /** * Injects the given {@code arguments} in the {@code obj}. For more details see @@ -163,7 +163,7 @@ private void injectIntoField(ProofScriptArgument meta, Map ar if (meta.isRequired()) { throw new ArgumentRequiredException(String.format( "Argument %s:%s is required, but %s was given. " + "For comamnd class: '%s'", - meta.getName(), meta.getField().getType(), val, meta.getCommand().getClass()), + meta.getName(), meta.getField().getType(), null, meta.getCommand().getClass()), meta); } } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java index 11522dc0664..c429e1fb7b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java @@ -4,8 +4,10 @@ package de.uka.ilkd.key.nparser; import java.net.URI; -import java.net.URL; -import java.util.*; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.LinkedHashMap; +import java.util.Map; import javax.annotation.Nonnull; import de.uka.ilkd.key.java.Position; @@ -25,7 +27,7 @@ * * @author Alexander Weigl * @version 1 (12/5/19) - * @see #run(Token, CharStream, IProofFileParser, URL) + * @see #run(Token, CharStream, IProofFileParser, URI) */ public class ProofReplayer { /** @@ -63,7 +65,7 @@ public static void run(@Nonnull Token token, CharStream input, IProofFileParser * Replays the proof behind the given {@code input}. This method uses the {@link KeYLexer} to * lex input stream, and parse them manually by consuming the tokens. It singals to the given * {@link IProofFileParser} at start or end of an expr. - * + *

    * Avoid the usage of a parser, avoids also the construction of an ASTs. * * @param input a valid input stream @@ -82,12 +84,11 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi while (true) { int type = stream.LA(1); // current token type switch (type) { - case KeYLexer.LPAREN: + case KeYLexer.LPAREN -> { // expected "(" ["string"] stream.consume(); // consume the "(" Token idToken = stream.LT(1); // element id IProofFileParser.ProofElementID cur = proofSymbolElementId.get(idToken.getText()); - if (cur == null) { Location loc = new Location(source, Position.fromToken(idToken).offsetLine(startLine - 1)); @@ -95,7 +96,6 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi loc); } stream.consume(); - String arg = null; int pos = idToken.getLine() + startLine; if (stream.LA(1) == KeYLexer.STRING_LITERAL) { @@ -104,19 +104,18 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi arg = unescape(arg.substring(1, arg.length() - 1)); stream.consume();// throw string away } - prl.beginExpr(cur, arg); stack.push(cur); posStack.push(pos); - break; - case KeYLexer.RPAREN: + } + case KeYLexer.RPAREN -> { prl.endExpr(stack.pop(), posStack.pop()); stream.consume(); - break; - case KeYLexer.EOF: + } + case KeYLexer.EOF -> { return; - default: - stream.consume(); + } + default -> stream.consume(); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 166759d3401..96efe5ff2e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -128,9 +128,6 @@ public static String trimJavaBlock(String raw) { /** * Given a raw modality string, this method determines the operator name. - * - * @param raw - * @return */ public static String operatorOfJavaBlock(String raw) { if (raw.startsWith("\\<")) { @@ -542,7 +539,7 @@ private LogicVariable bindVar(LogicVariable v) { } private void bindVar() { - namespaces().setVariables(new Namespace(variables())); + namespaces().setVariables(new Namespace<>(variables())); } private Term toZNotation(String literal, Namespace functions) { @@ -802,27 +799,15 @@ private String unescapeString(String string) { for (int i = 0; i < chars.length; i++) { if (chars[i] == '\\' && i < chars.length - 1) { switch (chars[++i]) { - case 'n': - sb.append("\n"); - break; - case 'f': - sb.append("\f"); - break; - case 'r': - sb.append("\r"); - break; - case 't': - sb.append("\t"); - break; - case 'b': - sb.append("\b"); - break; - case ':': - sb.append("\\:"); - break; // this is so in KeY ... - default: - sb.append(chars[i]); - break; // this more relaxed than before, \a becomes a ... + case 'n' -> sb.append("\n"); + case 'f' -> sb.append("\f"); + case 'r' -> sb.append("\r"); + case 't' -> sb.append("\t"); + case 'b' -> sb.append("\b"); + case ':' -> sb.append("\\:"); + // this is so in KeY ... + default -> sb.append(chars[i]); + // this more relaxed than before, \a becomes a ... } } else { sb.append(chars[i]); @@ -983,7 +968,7 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex Term t = accept(ctx.primitive_term()); if (ctx.LGUILLEMETS() != null) { ImmutableArray labels = accept(ctx.label()); - if (labels.size() > 0) { + if (!labels.isEmpty()) { t = getServices().getTermBuilder().addLabel(t, labels); } } @@ -993,7 +978,7 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex @Override public ImmutableArray visitLabel(KeYParser.LabelContext ctx) { List labels = mapOf(ctx.single_label()); - return new ImmutableArray(labels); + return new ImmutableArray<>(labels); } @Override @@ -1778,11 +1763,6 @@ private boolean isImplicitHeap(Term t) { /** * Guard for {@link #replaceHeap0(Term, Term, ParserRuleContext)} to protect the double * application of {@code @heap}. - * - * @param term - * @param heap - * @param ctx - * @return */ private Term replaceHeap(Term term, Term heap, ParserRuleContext ctx) { if (explicitHeap.contains(term)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java index ea6003f58ba..e8d199938e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java @@ -7,8 +7,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.logic.NamespaceSet; -import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; @@ -19,7 +18,7 @@ * @author weigl */ public class ProblemFinder extends ExpressionBuilder { - private @Nullable Term problemTerm; + private @Nullable Sequent problem; private @Nullable String chooseContract; private @Nullable String proofObligation; @@ -59,11 +58,21 @@ public Term visitProblem(KeYParser.ProblemContext ctx) { } } if (ctx.PROBLEM() != null) { - problemTerm = accept(ctx.term()); + problem = accept(ctx.termorseq()); } return null; } + @Override + public Sequent visitTermorseq(KeYParser.TermorseqContext ctx) { + var obj = super.visitTermorseq(ctx); + if (obj instanceof Sequent s) + return s; + if (obj instanceof Term t) + return Sequent.createSuccSequent(new Semisequent(new SequentFormula(t))); + return null; + } + @Nullable public String getChooseContract() { return chooseContract; @@ -75,7 +84,7 @@ public String getProofObligation() { } @Nullable - public Term getProblemTerm() { - return problemTerm; + public Sequent getProblem() { + return problem; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 4e18e476295..dbb441e2069 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -93,11 +93,7 @@ public Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { axiomMode = true; } ChoiceExpr choices = accept(ctx.choices); - if (choices != null) { - this.requiredChoices = choices; - } else { - this.requiredChoices = ChoiceExpr.TRUE; - } + this.requiredChoices = Objects.requireNonNullElse(choices, ChoiceExpr.TRUE); List seq = mapOf(ctx.taclet()); topLevelTaclets.addAll(seq); disableJavaSchemaMode(); @@ -310,22 +306,14 @@ private Object evaluateVarcondArgument(ArgumentType expectedType, Object prevVal return prevValue; // previous value is of suitable type, we do not re-evaluate } - switch (expectedType) { - case TYPE_RESOLVER: - return buildTypeResolver(ctx); - case SORT: - return visitSortId(ctx.term().getText(), ctx.term()); - case JAVA_TYPE: - return getOrCreateJavaType(ctx.term().getText(), ctx); - case VARIABLE: - return varId(ctx, ctx.getText()); - case STRING: - return ctx.getText(); - case TERM: - return accept(ctx.term()); - } - assert false; - return null; + return switch (expectedType) { + case TYPE_RESOLVER -> buildTypeResolver(ctx); + case SORT -> visitSortId(ctx.term().getText(), ctx.term()); + case JAVA_TYPE -> getOrCreateJavaType(ctx.term().getText(), ctx); + case VARIABLE -> varId(ctx, ctx.getText()); + case STRING -> ctx.getText(); + case TERM -> accept(ctx.term()); + }; } private Sort visitSortId(String text, ParserRuleContext ctx) { @@ -367,7 +355,7 @@ private KeYJavaType getOrCreateJavaType(String sortId, ParserRuleContext ctx) { if (t != null) { return t; } - return new KeYJavaType((Sort) visitSortId(sortId, ctx)); + return new KeYJavaType(visitSortId(sortId, ctx)); } @@ -504,19 +492,19 @@ private TacletBuilder createTacletBuilderFor(Object find, int applicationRest if (find == null) { return new NoFindTacletBuilder(); } else if (find instanceof Term) { - return new RewriteTacletBuilder().setFind((Term) find) + return new RewriteTacletBuilder<>().setFind((Term) find) .setApplicationRestriction(applicationRestriction); } else if (find instanceof Sequent findSeq) { if (findSeq.isEmpty()) { return new NoFindTacletBuilder(); - } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().size() == 0) { + } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().isEmpty()) { Term findFma = findSeq.antecedent().get(0).formula(); AntecTacletBuilder b = new AntecTacletBuilder(); b.setFind(findFma); b.setIgnoreTopLevelUpdates( (applicationRestriction & RewriteTaclet.IN_SEQUENT_STATE) == 0); return b; - } else if (findSeq.antecedent().size() == 0 && findSeq.succedent().size() == 1) { + } else if (findSeq.antecedent().isEmpty() && findSeq.succedent().size() == 1) { Term findFma = findSeq.succedent().get(0).formula(); SuccTacletBuilder b = new SuccTacletBuilder(); b.setFind(findFma); @@ -663,7 +651,7 @@ public Object visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) s = accept(ctx.sortId()); } - for (String id : ids) { + for (String id : Objects.requireNonNull(ids)) { declareSchemaVariable(ctx, id, s, makeVariableSV, makeSkolemTermSV, makeTermLabelSV, mods); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 770e765f810..bb55bca0593 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -1801,50 +1801,21 @@ public static String escapeHTML(String text, boolean escapeWhitespace) { for (int i = 0, sz = text.length(); i < sz; i++) { char c = text.charAt(i); switch (c) { - case '<': - sb.append("<"); - break; - case '>': - sb.append(">"); - break; - case '&': - sb.append("&"); - break; - case '\"': - sb.append("""); - break; - case '\'': - sb.append("'"); - break; - case '(': - sb.append("("); - break; - case ')': - sb.append(")"); - break; - case '#': - sb.append("#"); - break; - case '+': - sb.append("+"); - break; - case '-': - sb.append("-"); - break; - case '%': - sb.append("%"); - break; - case ';': - sb.append(";"); - break; - case '\n': - sb.append(escapeWhitespace ? "
    " : c); - break; - case ' ': - sb.append(escapeWhitespace ? " " : c); - break; - default: - sb.append(c); + case '<' -> sb.append("<"); + case '>' -> sb.append(">"); + case '&' -> sb.append("&"); + case '\"' -> sb.append("""); + case '\'' -> sb.append("'"); + case '(' -> sb.append("("); + case ')' -> sb.append(")"); + case '#' -> sb.append("#"); + case '+' -> sb.append("+"); + case '-' -> sb.append("-"); + case '%' -> sb.append("%"); + case ';' -> sb.append(";"); + case '\n' -> sb.append(escapeWhitespace ? "
    " : c); + case ' ' -> sb.append(escapeWhitespace ? " " : c); + default -> sb.append(c); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java index 8fe89ed03cb..63e268c1108 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java @@ -259,37 +259,19 @@ public enum MarkType { MARK_END_JAVA_BLOCK, } - public static final class Mark { - public final MarkType type; - public final int parameter; - - public Mark(MarkType type, int parameter) { - this.type = type; - this.parameter = parameter; - } + public record Mark(MarkType type, int parameter) { } /** - * Utility class for stack entries containing the position table and the position of the start - * of the subterm in the result. - */ - private static class StackEntry { - final PositionTable posTbl; - final int p; - - StackEntry(PositionTable posTbl, int p) { - this.posTbl = posTbl; - this.p = p; - } - - PositionTable posTbl() { - return posTbl; - } + * Utility class for stack entries containing the position table and the position of the start + * of the subterm in the result. + */ + private record StackEntry(PositionTable posTbl, int p) { int pos() { - return p; + return p; + } } - } /** * A {@link de.uka.ilkd.key.util.pp.Backend} which puts its result in a StringBuffer and builds @@ -381,7 +363,7 @@ public void mark(Mark pair) { // MU refactored this using enums which makes it a little less ugly // and more flexible. switch (markType) { - case MARK_START_SUB: + case MARK_START_SUB -> { if (parameter == -1) { // no parameter means subterms in normal order posTbl.setStart(count() - pos); @@ -391,21 +373,16 @@ public void mark(Mark pair) { } stack.push(new StackEntry(posTbl, pos)); pos = count(); - break; - - case MARK_END_SUB: + } + case MARK_END_SUB -> { StackEntry se = stack.peek(); stack.pop(); pos = se.pos(); se.posTbl().setEnd(count() - pos, posTbl); posTbl = se.posTbl(); - break; - - case MARK_MOD_POS_TBL: - need_modPosTable = true; - break; - - case MARK_START_TERM: + } + case MARK_MOD_POS_TBL -> need_modPosTable = true; + case MARK_START_TERM -> { // This is sent by startTerm if (need_modPosTable) { posTbl = new ModalityPositionTable(parameter); @@ -413,42 +390,26 @@ public void mark(Mark pair) { posTbl = new PositionTable(parameter); } need_modPosTable = false; - break; - - case MARK_START_FIRST_STMT: - firstStmtStart = count() - pos; - break; - - case MARK_END_FIRST_STMT: + } + case MARK_START_FIRST_STMT -> firstStmtStart = count() - pos; + case MARK_END_FIRST_STMT -> { if (posTbl instanceof ModalityPositionTable) { Range firstStmtRange = new Range(firstStmtStart, count() - pos); ((ModalityPositionTable) posTbl).setFirstStatementRange(firstStmtRange); } - break; - - case MARK_START_UPDATE: - updateStarts.push(count()); - break; - - case MARK_END_UPDATE: + } + case MARK_START_UPDATE -> updateStarts.push(count()); + case MARK_END_UPDATE -> { int updateStart = updateStarts.pop(); initPosTbl.addUpdateRange(new Range(updateStart, count())); - break; - case MARK_START_KEYWORD: - keywordStarts.push(count()); - break; - case MARK_END_KEYWORD: - initPosTbl.addKeywordRange(new Range(keywordStarts.pop(), count())); - break; - case MARK_START_JAVA_BLOCK: - javaBlockStarts.push(count()); - break; - case MARK_END_JAVA_BLOCK: - initPosTbl.addJavaBlockRange(new Range(javaBlockStarts.pop(), count())); - break; - - default: - LOGGER.error("Unexpected mark: {}", markType); + } + case MARK_START_KEYWORD -> keywordStarts.push(count()); + case MARK_END_KEYWORD -> initPosTbl + .addKeywordRange(new Range(keywordStarts.pop(), count())); + case MARK_START_JAVA_BLOCK -> javaBlockStarts.push(count()); + case MARK_END_JAVA_BLOCK -> initPosTbl + .addJavaBlockRange(new Range(javaBlockStarts.pop(), count())); + default -> LOGGER.error("Unexpected mark: {}", markType); } } } 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 b5ed1c6fc32..bcf1e0932ea 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 @@ -185,27 +185,28 @@ protected void printOperator(Operator x, String symbol) { if (children != null) { l.beginC(); switch (x.getArity()) { - case 2: + case 2 -> { children.get(0).visit(this); l.print(" "); l.print(symbol); l.brk(); children.get(1).visit(this); - break; - case 1: + } + case 1 -> { switch (x.getNotation()) { - case Operator.PREFIX: + case Operator.PREFIX -> { l.print(symbol); children.get(0).visit(this); - break; - case Operator.POSTFIX: + } + case Operator.POSTFIX -> { children.get(0).visit(this); l.print(symbol); - break; - default: - break; + } + default -> { + } } } + } l.end(); } } @@ -654,7 +655,7 @@ public void performActionOnCompilationUnit(CompilationUnit x) { if (hasPackageSpec) { performActionOnPackageSpecification(x.getPackageSpecification()); } - boolean hasImports = (x.getImports() != null) && (x.getImports().size() > 0); + boolean hasImports = (x.getImports() != null) && (!x.getImports().isEmpty()); if (hasImports) { if (hasPackageSpec) { l.nl(); @@ -1010,10 +1011,6 @@ public void performActionOnFor(For x, boolean includeBody) { IForUpdates upd = x.getIForUpdates(); if (upd != null) { upd.visit(this); - if (upd instanceof ProgramSV) { - - } else { - } } endMultilineBracket(); @@ -1691,7 +1688,7 @@ public void performActionOnElse(Else x) { } private void printCaseBody(ImmutableArray body) { - if (body != null && body.size() > 0) { + if (body != null && !body.isEmpty()) { for (int i = 0; i < body.size(); i++) { Statement statement = body.get(i); if (statement instanceof StatementBlock) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 77079a74da7..436675686ce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -249,6 +249,14 @@ public Proof(String name, Term problem, String header, InitConfig initConfig, Fi this.proofFile = proofFile; } + public Proof(String name, Sequent problem, String header, InitConfig initConfig, + File proofFile) { + this(name, problem, initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), + initConfig); + problemHeader = header; + this.proofFile = proofFile; + } + public Proof(String name, Term problem, String header, InitConfig initConfig) { this(name, Sequent.createSuccSequent( diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 1d4ab8e5aac..b561e08094e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -9,7 +9,7 @@ import javax.annotation.Nonnull; import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.nparser.ChoiceInformation; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.nparser.ProblemInformation; @@ -37,7 +37,7 @@ * obligation. */ public final class KeYUserProblemFile extends KeYFile implements ProofOblInput { - private Term problemTerm = null; + private Sequent problem = null; // ------------------------------------------------------------------------- // constructors @@ -133,8 +133,8 @@ public void readProblem() throws ProofInputException { readRules(); try { - problemTerm = getProblemFinder().getProblemTerm(); - if (problemTerm == null) { + problem = getProblemFinder().getProblem(); + if (problem == null) { boolean chooseDLContract = chooseContract() != null; boolean proofObligation = getProofObligation() != null; if (!chooseDLContract && !proofObligation) { @@ -160,12 +160,12 @@ public String getProofObligation() { @Override public ProofAggregate getPO() throws ProofInputException { - assert problemTerm != null; + assert problem != null; String name = name(); ProofSettings settings = getPreferences(); initConfig.setSettings(settings); return ProofAggregate.createProofAggregate( - new Proof(name, problemTerm, getParseContext().getProblemHeader() + "\n", initConfig, + new Proof(name, problem, getParseContext().getProblemHeader() + "\n", initConfig, file.file()), name); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 79d75ee0677..1f6c342dedc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -747,8 +747,8 @@ private ReplayResult replayProof(Proof proof) { : proof.root(); } catch (Exception e) { - if (parserResult == null || parserResult.getErrors() == null - || parserResult.getErrors().isEmpty() || replayer == null + if (parserResult == null || parserResult.errors() == null + || parserResult.errors().isEmpty() || replayer == null || replayResult == null || replayResult.getErrors() == null || replayResult.getErrors().isEmpty()) { // this exception was something unexpected @@ -756,8 +756,8 @@ private ReplayResult replayProof(Proof proof) { } } finally { if (parserResult != null) { - status = parserResult.getStatus(); - errors.addAll(parserResult.getErrors()); + status = parserResult.status(); + errors.addAll(parserResult.errors()); } status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n") + (replayResult != null ? replayResult.getStatus() diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 0f1f4b1d260..9e9645a271d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -24,13 +24,13 @@ * be processed by {@link IntermediateProofReplayer}. This approach is more flexible than direct * parsing; for instance, it is capable of dealing with merge rule applications. *

    - * + *

    * The returned intermediate proof closely resembles the structure of the parsed proof file. * Specifically, branch nodes are explicitly stored and, as in the proof file, have exactly one * child (or zero in the case of an empty proof). The first node, that is also the main returned * result, is a branch node with the identifier "dummy ID" that is present in every proof. *

    - * + *

    * Example for parsed intermediate proof: *

    * @@ -48,11 +48,11 @@ * > ... * *

    - * + *

    * Note that the last open goal in an unfinished proof is not represented by a node in the * intermediate representation (since no rule has been applied on the goal yet). *

    - * + *

    * The results of the parser may be obtained by calling {@link #getResult()}. * * @author Dominic Scheurer @@ -60,7 +60,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser { /* + The proof object for storing meta information */ - private Proof proof = null; + private final Proof proof; /* + Open Branches */ private final ArrayDeque stack = new ArrayDeque<>(); @@ -70,7 +70,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser /* + State information that is returned after parsing */ private BranchNodeIntermediate root = null; // the "dummy ID" branch - private NodeIntermediate currNode = null; + private NodeIntermediate currNode; private final LinkedList errors = new LinkedList<>(); /** @@ -78,15 +78,13 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser */ public IntermediatePresentationProofFileParser(Proof proof) { this.proof = proof; - this.currNode = this.root; } @Override @SuppressWarnings("unchecked") public void beginExpr(ProofElementID eid, String str) { switch (eid) { - case BRANCH: // branch - { + case BRANCH -> { final BranchNodeIntermediate newNode = new BranchNodeIntermediate(str); if (root == null) { @@ -99,37 +97,31 @@ public void beginExpr(ProofElementID eid, String str) { currNode = newNode; } } - break; - - case RULE: // rule (taclet) - { - final AppNodeIntermediate newNode = new AppNodeIntermediate(); - currNode.addChild(newNode); - currNode = newNode; - } - + case RULE -> { // rule (taclet) + { + final AppNodeIntermediate newNode = new AppNodeIntermediate(); + currNode.addChild(newNode); + currNode = newNode; + } ruleInfo = new TacletInformation(str); - break; - - case FORMULA: // formula + } + case FORMULA -> { // formula final int formula = Integer.parseInt(str); if (insideBuiltinIfInsts()) { ((BuiltinRuleInformation) ruleInfo).currIfInstFormula = formula; } else { ruleInfo.currFormula = formula; } - break; - - case TERM: // term + } + case TERM -> { // term final PosInTerm pos = PosInTerm.parseReverseString(str); if (insideBuiltinIfInsts()) { ((BuiltinRuleInformation) ruleInfo).currIfInstPosInTerm = pos; } else { ruleInfo.currPosInTerm = pos; } - break; - - case INSTANTIATION: // inst + } + case INSTANTIATION -> // inst { TacletInformation tacletInfo = (TacletInformation) ruleInfo; if (tacletInfo.loadedInsts == null) { @@ -137,138 +129,97 @@ public void beginExpr(ProofElementID eid, String str) { } tacletInfo.loadedInsts.add(str); } - break; - - case RULESET: // heuristics - break; - - case ASSUMES_FORMULA_IN_SEQUENT: // ifseqformula + case RULESET -> { + } // heuristics + case ASSUMES_FORMULA_IN_SEQUENT -> // ifseqformula { TacletInformation tacletInfo = (TacletInformation) ruleInfo; tacletInfo.ifSeqFormulaList = tacletInfo.ifSeqFormulaList.append(str); } - break; - - case ASSUMES_FORMULA_DIRECT: // ifdirectformula + case ASSUMES_FORMULA_DIRECT -> // ifdirectformula { TacletInformation tacletInfo = (TacletInformation) ruleInfo; tacletInfo.ifDirectFormulaList = tacletInfo.ifDirectFormulaList.append(str); } - break; - - case KeY_USER: // UserLog + case KeY_USER -> { // UserLog if (proof.userLog == null) { proof.userLog = new ArrayList<>(); } proof.userLog.add(str); - break; - - case KeY_VERSION: // Version log + } + case KeY_VERSION -> { // Version log if (proof.keyVersionLog == null) { proof.keyVersionLog = new ArrayList<>(); } proof.keyVersionLog.add(str); - break; - - case KeY_SETTINGS: // ProofSettings - loadPreferences(str); - break; - - case BUILT_IN_RULE: // BuiltIn rules - { - final AppNodeIntermediate newNode = new AppNodeIntermediate(); - currNode.addChild(newNode); - currNode = newNode; } - + case KeY_SETTINGS -> // ProofSettings + loadPreferences(str); + case BUILT_IN_RULE -> { // BuiltIn rules + { + final AppNodeIntermediate newNode = new AppNodeIntermediate(); + currNode.addChild(newNode); + currNode = newNode; + } ruleInfo = new BuiltinRuleInformation(str); - break; - - case CONTRACT: // contract - ((BuiltinRuleInformation) ruleInfo).currContract = str; - break; - - case MODALITY: + } + case CONTRACT -> ((BuiltinRuleInformation) ruleInfo).currContract = str; + case MODALITY -> // (additional information which can be used in external tools such as proof management) ((BuiltinRuleInformation) ruleInfo).currContractModality = str; - break; - - case ASSUMES_INST_BUILT_IN: // ifInst (for built in rules) + case ASSUMES_INST_BUILT_IN -> { // ifInst (for built in rules) BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; - if (builtinInfo.builtinIfInsts == null) { builtinInfo.builtinIfInsts = ImmutableSLList.nil(); } builtinInfo.currIfInstFormula = 0; builtinInfo.currIfInstPosInTerm = PosInTerm.getTopLevel(); - break; - - case NEW_NAMES: // newnames + } + case NEW_NAMES -> { final String[] newNames = str.split(","); ruleInfo.currNewNames = ImmutableSLList.nil(); for (String newName : newNames) { ruleInfo.currNewNames = ruleInfo.currNewNames.append(new Name(newName)); } - break; - - case AUTOMODE_TIME: // autoModeTime + } + case AUTOMODE_TIME -> { try { proof.addAutoModeTime(Long.parseLong(str)); - } catch (NumberFormatException e) { - /* ignore */ + } catch (NumberFormatException ignore) { } - break; - - case MERGE_PROCEDURE: // merge procedure + } + case MERGE_PROCEDURE -> // merge procedure ((BuiltinRuleInformation) ruleInfo).currMergeProc = str; - break; - - case NUMBER_MERGE_PARTNERS: // number of merge partners + case NUMBER_MERGE_PARTNERS -> // number of merge partners ((BuiltinRuleInformation) ruleInfo).currNrPartners = Integer.parseInt(str); - break; - - case MERGE_NODE: // corresponding merge node id + case MERGE_NODE -> // corresponding merge node id ((BuiltinRuleInformation) ruleInfo).currCorrespondingMergeNodeId = Integer.parseInt(str); - break; - - case MERGE_ID: // merge node id + case MERGE_ID -> // merge node id ((BuiltinRuleInformation) ruleInfo).currMergeNodeId = Integer.parseInt(str); - break; - - case MERGE_DIST_FORMULA: // distinguishing formula for merges + case MERGE_DIST_FORMULA -> // distinguishing formula for merges ((BuiltinRuleInformation) ruleInfo).currDistFormula = str; - break; - - case MERGE_PREDICATE_ABSTRACTION_LATTICE_TYPE: // type of predicate - // abstraction lattice + case MERGE_PREDICATE_ABSTRACTION_LATTICE_TYPE -> { // type of predicate + // abstraction lattice try { ((BuiltinRuleInformation) ruleInfo).currPredAbstraLatticeType = (Class) Class.forName(str); } catch (ClassNotFoundException e) { errors.add(e); } - break; - - case MERGE_ABSTRACTION_PREDICATES: - ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = str; - break; - - case MERGE_USER_CHOICES: - ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; - break; - - case NOTES: + } + case MERGE_ABSTRACTION_PREDICATES -> ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = + str; + case MERGE_USER_CHOICES -> ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; + case NOTES -> { ruleInfo.notes = str; if (currNode != null) { ((AppNodeIntermediate) currNode).setNotes(ruleInfo.notes); } - break; - case SOLVERTYPE: - ((BuiltinRuleInformation) ruleInfo).solver = str; - break; - default: - break; + } + case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str; + default -> { + } } } @@ -276,41 +227,33 @@ public void beginExpr(ProofElementID eid, String str) { @Override public void endExpr(ProofElementID eid, int lineNr) { switch (eid) { - case BRANCH: // branch - currNode = stack.pop(); - break; - - case USER_INTERACTION: // userinteraction + case BRANCH -> currNode = stack.pop(); + case USER_INTERACTION -> { if (currNode != null) { ((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true); } - break; - - case PROOF_SCRIPT: // proof script node + } + case PROOF_SCRIPT -> { if (currNode != null) { ((AppNodeIntermediate) currNode).setScriptRuleApplication(true); } - break; - - case RULE: // rule (taclet) + } + case RULE -> { // rule (taclet) ((AppNodeIntermediate) currNode).setIntermediateRuleApp(constructTacletApp()); ((AppNodeIntermediate) currNode).getIntermediateRuleApp().setLineNr(lineNr); - break; - - case BUILT_IN_RULE: // BuiltIn rules + } + case BUILT_IN_RULE -> { // BuiltIn rules ((AppNodeIntermediate) currNode).setIntermediateRuleApp(constructBuiltInApp()); ((AppNodeIntermediate) currNode).getIntermediateRuleApp().setLineNr(lineNr); - break; - - case ASSUMES_INST_BUILT_IN: // ifInst (for built in rules) + } + case ASSUMES_INST_BUILT_IN -> { // ifInst (for built in rules) BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; builtinInfo.builtinIfInsts = builtinInfo.builtinIfInsts.append(new Pair<>( builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm)); - break; - - default: - break; + } + default -> { + } } } @@ -356,33 +299,24 @@ private TacletAppIntermediate constructTacletApp() { */ private BuiltInAppIntermediate constructBuiltInApp() { BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; - BuiltInAppIntermediate result = null; - - if (builtinInfo.currRuleName.equals("MergeRule")) { - result = - new MergeAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, - builtinInfo.currPosInTerm), - builtinInfo.currMergeNodeId, builtinInfo.currMergeProc, - builtinInfo.currNrPartners, builtinInfo.currNewNames, - builtinInfo.currDistFormula, builtinInfo.currPredAbstraLatticeType, - builtinInfo.currAbstractionPredicates, builtinInfo.currUserChoices); - } else if (builtinInfo.currRuleName.equals("CloseAfterMerge")) { - result = new MergePartnerAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.currCorrespondingMergeNodeId, builtinInfo.currNewNames); - } else if (builtinInfo.currRuleName.equals("SMTRule")) { - result = new SMTAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.solver); - } else { - result = new BuiltInAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.currContract, builtinInfo.currContractModality, - builtinInfo.builtinIfInsts, builtinInfo.currNewNames); - } - - return result; + return switch (builtinInfo.currRuleName) { + case "MergeRule" -> new MergeAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currMergeNodeId, builtinInfo.currMergeProc, + builtinInfo.currNrPartners, builtinInfo.currNewNames, + builtinInfo.currDistFormula, builtinInfo.currPredAbstraLatticeType, + builtinInfo.currAbstractionPredicates, builtinInfo.currUserChoices); + case "CloseAfterMerge" -> new MergePartnerAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currCorrespondingMergeNodeId, builtinInfo.currNewNames); + case "SMTRule" -> new SMTAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.solver); + default -> new BuiltInAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currContract, builtinInfo.currContractModality, + builtinInfo.builtinIfInsts, builtinInfo.currNewNames); + }; } /** @@ -411,7 +345,7 @@ private boolean insideBuiltinIfInsts() { */ private static abstract class RuleInformation { /* + General Information */ - protected String currRuleName = null; + protected String currRuleName; protected int currFormula = 0; protected PosInTerm currPosInTerm = PosInTerm.getTopLevel(); protected ImmutableList currNewNames = null; @@ -477,29 +411,8 @@ public BuiltinRuleInformation(String ruleName) { * * @author Dominic Scheurer */ - public static class Result { - private final List errors; - private final String status; - private BranchNodeIntermediate parsedResult = null; - - public Result(List errors, String status, BranchNodeIntermediate parsedResult) { - this.errors = errors; - this.status = status; - this.parsedResult = parsedResult; - } - - public List getErrors() { - return errors; - } - - public String getStatus() { - return status; - } - - public BranchNodeIntermediate getParsedResult() { - return parsedResult; - } - + public record Result(List errors, String status, + BranchNodeIntermediate parsedResult) { } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index b6a1c17b6a5..e0f791f1f3a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -130,7 +130,7 @@ public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, this.loader = loader; queue.addFirst( - new Pair<>(proof.root(), parserResult.getParsedResult())); + new Pair<>(proof.root(), parserResult.parsedResult())); } /** 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 9e795b0fff1..12b9d7030d1 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 @@ -229,10 +229,9 @@ public Instantiator(final Term formula, final Goal goal, final Services services public Instantiation instantiate() { final Term update = extractUpdate(); final Term target = extractUpdateTarget(); - if (!(target.op() instanceof Modality)) { + if (!(target.op() instanceof Modality modality)) { return null; } - final Modality modality = (Modality) target.op(); final JavaStatement statement = getFirstStatementInPrefixWithAtLeastOneApplicableContract(modality, target.javaBlock(), goal); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java index da69483d8c2..c48cb977213 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java @@ -93,25 +93,20 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service if (!proxy1 && !proxy2) { // This is the standard case where no proxy sorts are involved - switch (mode) { - case SAME: - return fstSort == sndSort; - case NOT_SAME: - return fstSort != sndSort; - case IS_SUBTYPE: - return fstSort.extendsTrans(sndSort); - case STRICT_SUBTYPE: - return fstSort != sndSort && fstSort.extendsTrans(sndSort); - case NOT_IS_SUBTYPE: - return !fstSort.extendsTrans(sndSort); - case DISJOINTMODULONULL: - return checkDisjointness(fstSort, sndSort, services); - } + return switch (mode) { + case SAME -> fstSort == sndSort; + case NOT_SAME -> fstSort != sndSort; + case IS_SUBTYPE -> fstSort.extendsTrans(sndSort); + case STRICT_SUBTYPE -> fstSort != sndSort && fstSort.extendsTrans(sndSort); + case NOT_IS_SUBTYPE -> !fstSort.extendsTrans(sndSort); + case DISJOINTMODULONULL -> checkDisjointness(fstSort, sndSort, services); + }; } else { switch (mode) { - case SAME: + case SAME -> { return fstSort == sndSort; - case IS_SUBTYPE: + } + case IS_SUBTYPE -> { if (proxy2) { return false; } @@ -124,7 +119,8 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service } } return false; - case STRICT_SUBTYPE: + } + case STRICT_SUBTYPE -> { if (proxy2) { return false; } @@ -137,14 +133,13 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service } } return false; - - case NOT_SAME: - case DISJOINTMODULONULL: - case NOT_IS_SUBTYPE: + } + case NOT_SAME, DISJOINTMODULONULL, NOT_IS_SUBTYPE -> { // There are cases where - based on the bounds - true could be returned. // Implement them if needed. There is the Null type to consider as subtype. return false; } + } } assert false : "All cases should have been covered"; @@ -266,21 +261,14 @@ private boolean checkDisjointness(Sort fstSort, Sort sndSort, Services services) @Override public String toString() { - switch (mode) { - case SAME: - return "\\same(" + fst + ", " + snd + ")"; - case NOT_SAME: - return "\\not\\same(" + fst + ", " + snd + ")"; - case IS_SUBTYPE: - return "\\sub(" + fst + ", " + snd + ")"; - case STRICT_SUBTYPE: - return "\\strict\\sub(" + fst + ", " + snd + ")"; - case NOT_IS_SUBTYPE: - return "\\not\\sub(" + fst + ", " + snd + ")"; - case DISJOINTMODULONULL: - return "\\disjointModuloNull(" + fst + ", " + snd + ")"; - default: - return "invalid type comparison mode"; - } + return switch (mode) { + case SAME -> "\\same(" + fst + ", " + snd + ")"; + case NOT_SAME -> "\\not\\same(" + fst + ", " + snd + ")"; + case IS_SUBTYPE -> "\\sub(" + fst + ", " + snd + ")"; + case STRICT_SUBTYPE -> "\\strict\\sub(" + fst + ", " + snd + ")"; + case NOT_IS_SUBTYPE -> "\\not\\sub(" + fst + ", " + snd + ")"; + case DISJOINTMODULONULL -> "\\disjointModuloNull(" + fst + ", " + snd + ")"; + default -> "invalid type comparison mode"; + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java index 3b5e9535ba9..20eaae2941d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java @@ -114,10 +114,6 @@ public Statement getTheLoop() { return theLoop; } - public String toString() { - return stack.peek().toString(); - } - public void performActionOnMethodFrame(MethodFrame x) { if (lastMethodFrameBeforeLoop == depth()) { IProgramVariable res = x.getProgramVariable(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java index 165f846a38e..ac2ced2ca92 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java @@ -23,22 +23,16 @@ interface Query { /** * Stores the result from the z3 solver. - * - * @param s */ void setResult(String s); /** * Returns the command that is to be handed over to the z3 solver. - * - * @return */ String getQuery(); /** * Returns the stored result. - * - * @return */ String getResult(); } @@ -671,29 +665,15 @@ public class ModelExtractor { public void addFunction(SMTFunction f) { - if (f.getDomainSorts().size() == 0) { + if (f.getDomainSorts().isEmpty()) { switch (f.getImageSort().getId()) { - case SMTObjTranslator.HEAP_SORT: - heaps.add(f); - break; - case SMTObjTranslator.FIELD_SORT: - fields.add(f); - break; - case SMTObjTranslator.LOCSET_SORT: - locsets.add(f); - break; - case SMTObjTranslator.OBJECT_SORT: - objects.add(f); - break; - case SMTObjTranslator.BINT_SORT: - ints.add(f); - break; - case SMTObjTranslator.SEQ_SORT: - seqs.add(f); - break; - default: - bools.add(f); - break; + case SMTObjTranslator.HEAP_SORT -> heaps.add(f); + case SMTObjTranslator.FIELD_SORT -> fields.add(f); + case SMTObjTranslator.LOCSET_SORT -> locsets.add(f); + case SMTObjTranslator.OBJECT_SORT -> objects.add(f); + case SMTObjTranslator.BINT_SORT -> ints.add(f); + case SMTObjTranslator.SEQ_SORT -> seqs.add(f); + default -> bools.add(f); } } else if (f.getDomainSorts().size() == 2) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java index fa2cb4ba435..230b578750a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java @@ -670,25 +670,19 @@ private void generateWellFormedAssertions() throws IllegalFormulaException { SMTTerm selectArr = SMTTerm.call(selectFunction, h, o, arr); SMTTerm typeReq; switch (single) { - case "int": - case "char": - case "byte": - typeReq = SMTTerm.call(getIsFunction(sorts.get(BINT_SORT)), selectArr); - break; - case "java.lang.Object": - typeReq = SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); - break; - case "boolean": - typeReq = SMTTerm.call(getIsFunction(SMTSort.BOOL), selectArr); - break; - default: + case "int", "char", "byte" -> typeReq = + SMTTerm.call(getIsFunction(sorts.get(BINT_SORT)), selectArr); + case "java.lang.Object" -> typeReq = + SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); + case "boolean" -> typeReq = SMTTerm.call(getIsFunction(SMTSort.BOOL), selectArr); + default -> { typeReq = SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); Sort singleSort = services.getJavaInfo().getKeYJavaType(single).getSort(); addTypePredicate(singleSort); SMTFunction tps = getTypePredicate(singleSort.name().toString()); SMTTerm selectObjArr = castTermIfNecessary(selectArr, sorts.get(OBJECT_SORT)); typeReq = typeReq.and(SMTTerm.call(tps, selectObjArr)); - break; + } } assertion4 = assertion4.and(premise.implies(typeReq)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index fb52a52373b..5754a602046 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -48,11 +48,6 @@ public SMTRuleApp replacePos(PosInOccurrence newPos) { return new SMTRuleApp(RULE, newPos, ifInsts, successfulSolverName); } - @Override - public boolean complete() { - return true; - } - public String getTitle() { return title; } @@ -61,11 +56,6 @@ public String getSuccessfulSolverName() { return successfulSolverName; } - @Override - public PosInOccurrence posInOccurrence() { - return pio; - } - @Override public BuiltInRule rule() { return RULE; diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index 044152bb3a1..0201e0772eb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -290,17 +290,12 @@ private void interruptionOccurred(Throwable e) { ReasonOfInterruption reason = getReasonOfInterruption(); setReasonOfInterruption(ReasonOfInterruption.Exception, e); switch (reason) { - case Exception: - case NoInterruption: + case Exception, NoInterruption -> { setReasonOfInterruption(ReasonOfInterruption.Exception, e); listener.processInterrupted(this, problem, e); - break; - case Timeout: - listener.processTimeout(this, problem); - break; - case User: - listener.processUser(this, problem); - break; + } + case Timeout -> listener.processTimeout(this, problem); + case User -> listener.processUser(this, problem); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java index 49d56f94742..ffc1b7c272c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java @@ -33,7 +33,7 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx } switch (sc.getState()) { - case WAIT_FOR_RESULT: + case WAIT_FOR_RESULT -> { if (msg.equals("unsat")) { sc.setFinalResult(SMTSolverResult.createValidResult(getName())); pipe.sendMessage("(exit)"); @@ -50,21 +50,17 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx sc.setState(WAIT_FOR_DETAILS); pipe.sendMessage("(exit)"); } - - break; - - case WAIT_FOR_DETAILS: - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - break; - - case WAIT_FOR_QUERY: + } + case WAIT_FOR_DETAILS -> { + } + // Currently we rely on the solver to terminate after receiving "(exit)". If this does + // not work in future, it may be that we have to forcibly close the pipe. + case WAIT_FOR_QUERY -> { if (!msg.equals("success")) { getQuery().messageIncoming(pipe, msg); } - break; - - case WAIT_FOR_MODEL: + } + case WAIT_FOR_MODEL -> { if (msg.equals("endmodel")) { if (getQuery() != null && getQuery().getState() == ModelExtractor.DEFAULT) { getQuery().getModel().setEmpty(false); @@ -75,9 +71,8 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx sc.setState(WAIT_FOR_DETAILS); } } - break; - default: - throw new IllegalStateException("Unexpected value: " + sc.getState()); + } + default -> throw new IllegalStateException("Unexpected value: " + sc.getState()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java index f03a9624079..0a8b9a8c1f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java @@ -32,7 +32,7 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx } switch (sc.getState()) { - case WAIT_FOR_RESULT: + case WAIT_FOR_RESULT -> { if (msg.equals("unsat")) { sc.setFinalResult(SMTSolverResult.createValidResult(getName())); // TODO: proof production is currently completely disabled, since it does not work @@ -55,16 +55,15 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx pipe.sendMessage("(exit)\n"); sc.setState(WAIT_FOR_DETAILS); } - break; - - case WAIT_FOR_DETAILS: - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - // if (msg.equals("success")) { - // pipe.sendMessage("(exit)"); - // pipe.close(); - // } - break; + } + case WAIT_FOR_DETAILS -> { + } + // Currently we rely on the solver to terminate after receiving "(exit)". If this does + // not work in future, it may be that we have to forcibly close the pipe. + // if (msg.equals("success")) { + // pipe.sendMessage("(exit)"); + // pipe.close(); + // } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java index 6b28cb74ff3..d3e8cabd6aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java @@ -291,12 +291,10 @@ public static SMTTerms terms(List terms) { */ public SMTTerm unaryOp(SMTTermUnaryOp.Op op) { - switch (op) { - case NOT: - return this.not(); - default: - return new SMTTermUnaryOp(op, this); - } + return switch (op) { + case NOT -> this.not(); + default -> new SMTTermUnaryOp(op, this); + }; } public SMTTerm sign(boolean pol) { @@ -326,51 +324,29 @@ public SMTTerm not() { } public SMTTerm multOp(SMTTermMultOp.Op op, SMTTerm t) { - - switch (op) { - case AND: - return this.and(t); - case OR: - return this.or(t); - case IMPLIES: - return this.implies(t); - case IFF: - return this.iff(t); - case EQUALS: - return this.equal(t); - case LT: - return this.lt(t); - case LTE: - return this.lte(t); - case DIV: - return this.div(t); - case GT: - return this.gt(t); - case GTE: - return this.gte(t); - case MINUS: - return this.minus(t); - case MUL: - return this.mul(t); - case PLUS: - return this.plus(t); - case REM: - return this.rem(t); - - default: - return defaultMultOp(op, t); + return switch (op) { + case AND -> this.and(t); + case OR -> this.or(t); + case IMPLIES -> this.implies(t); + case IFF -> this.iff(t); + case EQUALS -> this.equal(t); + case LT -> this.lt(t); + case LTE -> this.lte(t); + case DIV -> this.div(t); + case GT -> this.gt(t); + case GTE -> this.gte(t); + case MINUS -> this.minus(t); + case MUL -> this.mul(t); + case PLUS -> this.plus(t); + case REM -> this.rem(t); + default -> defaultMultOp(op, t); // TODO implement bitvec cases if necessary // throw new // RuntimeException("Unexpected: binOp as arg for the method binOp(): "+op); - } + }; } - /** - * @param op - * @param f - * @return - */ private SMTTerm defaultMultOp(SMTTermMultOp.Op op, SMTTerm f) { List args = this.toList(); args.add(f); @@ -721,26 +697,18 @@ public SMTTerm minus(SMTTerm right) { } public SMTTerm quant(SMTTermQuant.Quant quant, List bindVars) { - switch (quant) { - case FORALL: - return this.forall(bindVars); - case EXISTS: - return this.exists(bindVars); - default: - return this; - } + return switch (quant) { + case FORALL -> this.forall(bindVars); + case EXISTS -> this.exists(bindVars); + }; } public SMTTerm quant(SMTTermQuant.Quant quant, List bindVars, List> pats) { - switch (quant) { - case FORALL: - return this.forall(bindVars, pats); - case EXISTS: - return this.exists(bindVars, pats); - default: - return this; - } + return switch (quant) { + case FORALL -> this.forall(bindVars, pats); + case EXISTS -> this.exists(bindVars, pats); + }; } public SMTTerm forall(List bindVars) { @@ -941,12 +909,7 @@ public String toString() { @Override public String toString(int nestPos) { - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } - - return tab + "true"; + return " ".repeat(Math.max(0, nestPos)) + "true"; } @Override @@ -1041,12 +1004,7 @@ public String toString() { @Override public String toString(int nestPos) { - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } - - return tab + "false"; + return " ".repeat(Math.max(0, nestPos)) + "false"; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java index 698991eb9ad..90000511b0a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java @@ -6,6 +6,7 @@ import java.util.HashMap; import java.util.LinkedList; import java.util.List; +import java.util.Map; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -19,8 +20,8 @@ public class SMTTermBinOp extends SMTTerm { private static final Logger LOGGER = LoggerFactory.getLogger(SMTTermBinOp.class); - private static HashMap bvSymbols; - private static HashMap intSymbols; + private static Map bvSymbols; + private static Map intSymbols; public enum OpProperty { NONE, LEFTASSOC, RIGHTASSOC, FULLASSOC, CHAINABLE, PAIRWISE @@ -52,28 +53,15 @@ public SMTTermBinOp(Op operator, SMTTerm left, SMTTerm right) { } public static OpProperty getProperty(SMTTermBinOp.Op op) { - - - switch (op) { - case AND: - case OR: - case PLUS: - case MUL: - return OpProperty.FULLASSOC; - case MINUS: - case XOR: - case DIV: - return OpProperty.LEFTASSOC; - case IMPLIES: - return OpProperty.RIGHTASSOC; - case EQUALS: - /* case LT: case LTE: case GT: case GTE: */ return OpProperty.CHAINABLE; - case DISTINCT: - return OpProperty.PAIRWISE; - default: - return OpProperty.NONE; - } - + return switch (op) { + case AND, OR, PLUS, MUL -> OpProperty.FULLASSOC; + case MINUS, XOR, DIV -> OpProperty.LEFTASSOC; + case IMPLIES -> OpProperty.RIGHTASSOC; + case EQUALS -> + /* case LT: case LTE: case GT: case GTE: */ OpProperty.CHAINABLE; + case DISTINCT -> OpProperty.PAIRWISE; + default -> OpProperty.NONE; + }; } private static void initMaps() { @@ -169,33 +157,22 @@ public List getVars() { /** {@inheritDoc} */ @Override public SMTSort sort() { + return switch (operator) { + case PLUS, MINUS, MUL, DIV, REM, BVASHR, BVSHL, BVSMOD, BVSREM -> { + if (!left.sort().equals(right.sort())) { - switch (operator) { - case PLUS: - case MINUS: - case MUL: - case DIV: - case REM: - case BVASHR: - case BVSHL: - case BVSMOD: - case BVSREM: - if (!left.sort().equals(right.sort())) { - - String error = "Unexpected: binary operation with two diff. arg sorts"; - error += "\n"; - error += this.toSting() + "\n"; - error += "Left sort: " + left.sort() + "\n"; - error += "Right sort: " + right.sort() + "\n"; - throw new RuntimeException(error); + String error = "Unexpected: binary operation with two diff. arg sorts"; + error += "\n"; + error += this.toSting() + "\n"; + error += "Left sort: " + left.sort() + "\n"; + error += "Right sort: " + right.sort() + "\n"; + throw new RuntimeException(error); + } + yield left.sort(); } - - - return left.sort(); - default: - return SMTSort.BOOL; - } + default -> SMTSort.BOOL; + }; } /** {@inheritDoc} */ @@ -241,8 +218,6 @@ public SMTTerm replace(SMTTermCall a, SMTTerm b) { /** {@inheritDoc} */ @Override public SMTTerm instantiate(SMTTermVariable a, SMTTerm b) { - // return new TermBinOp(operator, (Term) left.instantiate(a, b), (Term) right.instantiate(a, - // b)); //TODO return left.instantiate(a, b).binOp(operator, right.instantiate(a, b)); } @@ -358,10 +333,8 @@ public boolean isChainableBinOp(SMTTerm t) { public String toString(int nestPos) { LOGGER.warn("Warning: somehow a binop was created. {}", this.getOperator()); - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } + StringBuilder tab = new StringBuilder(); + tab.append(" ".repeat(Math.max(0, nestPos))); String symbol = getSymbol(operator, left); @@ -405,7 +378,7 @@ public String toString(int nestPos) { if (this.operator.equals(Op.AND)) { List chainStrings = checkChainable(nestPos, args); - if (chainStrings.size() == 1 && args.size() == 0) { + if (chainStrings.size() == 1 && args.isEmpty()) { return tab + chainStrings.get(0); } for (String s : chainStrings) { @@ -470,11 +443,6 @@ private List extractChain(int start, List args, List ops, return chain; } - /** - * @param nestPos - * @param args - * @return - */ private List checkChainable(int nestPos, List args) { List ops = new LinkedList<>(); List> chains = searchChains(args, ops); @@ -492,12 +460,9 @@ private List checkChainable(int nestPos, List args) { return chainStrings; } - /** - * @return - */ private String getSymbol(Op operator, SMTTerm first) { boolean isInt = first.sort().equals(SMTSort.INT) && first.sort().getBitSize() == -1; - String symbol = null; + String symbol; if (isInt) { symbol = intSymbols.get(operator); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java index 69d7c4ed77f..8442bcf81c7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java @@ -35,58 +35,45 @@ public enum Op { BVSLE, BVSGT, BVSGE, BVSDIV; public SMTTerm getIdem() { - switch (this) { - case AND: - return SMTTerm.TRUE; - case OR: - return SMTTerm.FALSE; - default: - throw new RuntimeException( - "Unexpected: getIdem() is only app. to the Operators 'AND' and 'OR': " + this); - } + return switch (this) { + case AND -> SMTTerm.TRUE; + case OR -> SMTTerm.FALSE; + default -> throw new RuntimeException( + "Unexpected: getIdem() is only app. to the Operators 'AND' and 'OR': " + this); + }; } public Op sign(boolean pol) { - switch (this) { - case AND: - if (pol) { - return this; + return switch (this) { + case AND -> { + if (pol) { + yield this; + } + yield OR; } - return OR; - case OR: - if (pol) { - return this; + case OR -> { + if (pol) { + yield this; + } + yield AND; } - return AND; - default: - throw new RuntimeException( - "Unexpected: sign(Boolean pol) is only app. to the Operators 'AND' and 'OR': " - + this); - } + default -> throw new RuntimeException( + "Unexpected: sign(Boolean pol) is only app. to the Operators 'AND' and 'OR': " + + this); + }; } } public static OpProperty getProperty(SMTTermMultOp.Op op) { - switch (op) { - case AND: - case OR: - case PLUS: - case MUL: - return OpProperty.FULLASSOC; - case MINUS: - case XOR: - case DIV: - return OpProperty.LEFTASSOC; - case IMPLIES: - return OpProperty.RIGHTASSOC; - case IFF: - case EQUALS: - /* case LT: case LTE: case GT: case GTE: */ return OpProperty.CHAINABLE; - case DISTINCT: - return OpProperty.PAIRWISE; - default: - return OpProperty.NONE; - } + return switch (op) { + case AND, OR, PLUS, MUL -> OpProperty.FULLASSOC; + case MINUS, XOR, DIV -> OpProperty.LEFTASSOC; + case IMPLIES -> OpProperty.RIGHTASSOC; + case IFF, EQUALS -> + /* case LT: case LTE: case GT: case GTE: */ OpProperty.CHAINABLE; + case DISTINCT -> OpProperty.PAIRWISE; + default -> OpProperty.NONE; + }; } private static void initMaps() { @@ -223,32 +210,23 @@ public List getVars() { @Override public SMTSort sort() { - switch (operator) { - case PLUS: - case MINUS: - case MUL: - case DIV: - case REM: - case BVASHR: - case BVSHL: - case BVSMOD: - case BVSREM: - case BVSDIV: - // Sanity check - if (subs.size() > 1) { - if (!subs.get(0).sort().equals(subs.get(1).sort())) { - String error = "Unexpected: binary operation with two diff. arg sorts"; - error += "\n"; - error += this.toSting() + "\n"; - error += "First sort: " + subs.get(0).sort() + "\n"; - error += "Second sort: " + subs.get(1).sort() + "\n"; - throw new RuntimeException(error); + return switch (operator) { + case PLUS, MINUS, MUL, DIV, REM, BVASHR, BVSHL, BVSMOD, BVSREM, BVSDIV -> { + // Sanity check + if (subs.size() > 1) { + if (!subs.get(0).sort().equals(subs.get(1).sort())) { + String error = "Unexpected: binary operation with two diff. arg sorts"; + error += "\n"; + error += this.toSting() + "\n"; + error += "First sort: " + subs.get(0).sort() + "\n"; + error += "Second sort: " + subs.get(1).sort() + "\n"; + throw new RuntimeException(error); + } } + yield subs.get(0).sort(); } - return subs.get(0).sort(); - default: - return SMTSort.BOOL; - } + default -> SMTSort.BOOL; + }; } /** {@inheritDoc} */ @@ -494,7 +472,7 @@ public String toString(int nestPos) { StringBuilder buff = new StringBuilder(); buff.append(tab); - if (subs.size() == 0) { + if (subs.isEmpty()) { throw new RuntimeException("Unexpected: Empty args for TermLogicalOp "); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java index 70e9f1018ec..60379932f39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java @@ -18,20 +18,21 @@ public enum Quant { FORALL, EXISTS; public Quant sign(boolean pol) { - switch (this) { - case FORALL: - if (pol) { - return this; + return switch (this) { + case FORALL -> { + if (pol) { + yield this; + } + yield EXISTS; } - return EXISTS; - case EXISTS: - if (pol) { - return this; + case EXISTS -> { + if (pol) { + yield this; + } + yield FORALL; } - return FORALL; - default: - throw new RuntimeException("Unexpected: Quant in neg() : " + this); - } + default -> throw new RuntimeException("Unexpected: Quant in neg() : " + this); + }; } } @@ -96,7 +97,7 @@ public List> getPats() { } /** - * @param pat the pat to set + * @param pats the pat to set */ public void setPats(List> pats) { this.pats = pats; @@ -231,13 +232,13 @@ public SMTTerm instantiate(SMTTermVariable a, SMTTerm b) { } if (newVars.size() < bindVars.size()) - /** + /* * 1. Some SMT solvers like Z3 requires patterns to contains all binded variables 2. * Some terms of the patterns can contains more that one variable 3. Instantiation of * quantified variables should can destroy the well-sortedness of patterns term. Because * of 1-3 and for simplicity, we just drop the entry pattern its the quantifier is * instantiated. - **/ + */ { return sub.instantiate(a, b).quant(quant, newVars); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java index bd128a76fd9..e4cbc209461 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java @@ -198,17 +198,12 @@ public String toString(int nestPos) { tab = tab.append(" "); } - switch (operator) { - case NOT: - return tab + "(not" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - case BVNOT: - return tab + "(bvnot" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - case BVNEG: - return tab + "(bvneg" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - default: - throw new RuntimeException("Unexpected: supported unaryOp={NOT}"); - } - + return switch (operator) { + case NOT -> tab + "(not" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + case BVNOT -> tab + "(bvnot" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + case BVNEG -> tab + "(bvneg" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + default -> throw new RuntimeException("Unexpected: supported unaryOp={NOT}"); + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java index e4f7d6d2637..b6842eda8e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java @@ -69,6 +69,8 @@ public SExpr handle(MasterHandler trans, Term term) throws SMTTranslationExcepti HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); Operator op = term.op(); + trans.addSort(((SortedOperator) op).sort()); + if (op == heapLDT.getArr()) { trans.introduceSymbol("arr"); return trans.handleAsFunctionCall("arr", term); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java index 9feef77f363..cbc58e552f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java @@ -14,7 +14,6 @@ import java.util.Map.Entry; import java.util.Properties; import java.util.Set; -import javax.annotation.Nullable; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; @@ -28,10 +27,10 @@ /** * Instances of this class are the controlling units of the translation. They control how the * translation is delegated to different {@link SMTHandler}s and collects the translations. - * + *

    * It keeps track of the actual translation of an expression but collects also the declarations and * axioms that occur during the translation. - * + *

    * It has measures to ensure that symbols are defined and axiomatized at most once. This allows us * to add these entries on the fly and on demand. * @@ -40,9 +39,6 @@ */ public class MasterHandler { - /** the services object associated with this particular translation */ - private final Services services; - /** Exceptions that occur during translation */ private final List exceptions = new ArrayList<>(); @@ -86,9 +82,8 @@ public class MasterHandler { * @param handlerOptions arbitrary String options for the handlers to process * @throws IOException if the handlers cannot be loaded */ - public MasterHandler(Services services, SMTSettings settings, @Nullable String[] handlerNames, + public MasterHandler(Services services, SMTSettings settings, String[] handlerNames, String[] handlerOptions) throws IOException { - this.services = services; getTranslationState().putAll(settings.getNewSettings().getMap()); handlers = SMTHandlerServices.getInstance().getFreshHandlers(services, handlerNames, handlerOptions, this); @@ -96,7 +91,7 @@ public MasterHandler(Services services, SMTSettings settings, @Nullable String[] /** * Copy toplevel declarations and axioms from a collection of snippets directly and make all - * named declarations (name.decl) and axioms (name.axioms) + * named declarations (name.decls), axioms (name.axioms) and deps (name.deps) * * @param snippets */ @@ -113,7 +108,7 @@ public void addDeclarationsAndAxioms(Properties snippets) { for (Entry en : snippets.entrySet()) { String key = (String) en.getKey(); - if (key.endsWith(".decls") || key.endsWith(".axioms")) { + if (key.endsWith(".decls") || key.endsWith(".axioms") || key.endsWith(".deps")) { translationState.put(key, en.getValue()); } } @@ -121,7 +116,7 @@ public void addDeclarationsAndAxioms(Properties snippets) { /** * This interface is used for routines that can be used to flexibly introduce function symbols. - * + *

    * An instance can be stored in the {@link #translationState} with a key suffixed with ".intro". * It is then invoked when a symbol is to be introduced. */ @@ -132,11 +127,11 @@ public interface SymbolIntroducer { /** * Translate a single term to an SMTLib S-Expression. - * + *

    * This method may modify the state of the handler (by adding symbols e.g.). - * + *

    * It tries to find a {@link SMTHandler} that can deal with the argument and delegates to that. - * + *

    * A default translation is triggered if no handler can be found. * * @param problem the non-null term to translate @@ -154,14 +149,16 @@ public SExpr translate(Term problem) { for (SMTHandler smtHandler : handlers) { Capability response = smtHandler.canHandle(problem); switch (response) { - case YES_THIS_INSTANCE: + case YES_THIS_INSTANCE -> { // handle this but do not cache. return smtHandler.handle(this, problem); - case YES_THIS_OPERATOR: + } + case YES_THIS_OPERATOR -> { // handle it and cache it for future instances of the op. handlerMap.put(problem.op(), smtHandler); return smtHandler.handle(this, problem); } + } } return handleAsUnknownValue(problem); @@ -173,14 +170,14 @@ public SExpr translate(Term problem) { /** * Translate a single term to an SMTLib S-Expression. - * + *

    * The result is ensured to have the SExpr-Type given as argument. If the type coercion fails, * then the translation falls back to translating the argument as an unknown function. - * + *

    * This method may modify the state of the handler (by adding symbols e.g.). - * + *

    * It tries to find a {@link SMTHandler} that can deal with the argument and delegates to that. - * + *

    * A default translation is triggered if no handler can be found. * * @param problem the non-null term to translate @@ -223,7 +220,7 @@ private SExpr handleAsUnknownValue(Term problem) { /** * Treats the given term as a function call. - * + *

    * This means that an expression of the form * *

    @@ -242,7 +239,7 @@ SExpr handleAsFunctionCall(String functionName, Term term) {
     
         /**
          * Treats the given term as a function call.
    -     *
    +     * 

    * This means that an expression of the form * *

    diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
    index 636e081efff..dbbf995a716 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
    @@ -54,14 +54,11 @@ private SExprs() {
          * @return an SExpr equivalent to the conjunction of the clauses.
          */
         public static SExpr and(List clauses) {
    -        switch (clauses.size()) {
    -        case 0:
    -            return TRUE;
    -        case 1:
    -            return clauses.get(0);
    -        default:
    -            return new SExpr("and", Type.BOOL, clauses);
    -        }
    +        return switch (clauses.size()) {
    +        case 0 -> TRUE;
    +        case 1 -> clauses.get(0);
    +        default -> new SExpr("and", Type.BOOL, clauses);
    +        };
         }
     
         /**
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
    index d29de5ae414..22a92cf034b 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
    @@ -63,9 +63,7 @@ public Term translate(Taclet taclet) throws SMTTranslationException {
             return quantify(skeleton, variables);
         }
     
    -    private Term quantify(Term smt, Map variables)
    -            throws SMTTranslationException {
    -
    +    private Term quantify(Term smt, Map variables) {
             if (variables.isEmpty()) {
                 return smt;
             }
    @@ -102,7 +100,7 @@ private Term variablify(Term term, Map variables)
             }
     
             List qvars = new ArrayList<>();
    -        if (op instanceof Quantifier q) {
    +        if (op instanceof Quantifier) {
                 for (QuantifiableVariable boundVar : term.boundVars()) {
                     if (boundVar instanceof SchemaVariable sv) {
                         LogicVariable lv =
    @@ -116,7 +114,7 @@ private Term variablify(Term term, Map variables)
             }
     
             if (changes) {
    -            ImmutableArray bvars = new ImmutableArray(qvars);
    +            var bvars = new ImmutableArray<>(qvars);
                 return services.getTermFactory().createTerm(op, subs, bvars, null, term.getLabels());
             } else {
                 return term;
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
    index 4311a2ac092..2b636e81103 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
    @@ -3,11 +3,7 @@
      * SPDX-License-Identifier: GPL-2.0-only */
     package de.uka.ilkd.key.smt.newsmt2;
     
    -import java.util.HashMap;
    -import java.util.LinkedHashMap;
    -import java.util.LinkedList;
    -import java.util.List;
    -import java.util.Properties;
    +import java.util.*;
     
     import de.uka.ilkd.key.java.Services;
     import de.uka.ilkd.key.logic.Term;
    @@ -21,10 +17,10 @@ public class SumProdHandler implements SMTHandler {
         private Function bsumOp, bprodOp;
     
         // key is the term to identify the bsum, value is the name used for that function.
    -    private final HashMap usedBsumTerms = new LinkedHashMap();
    +    private final Map usedBsumTerms = new LinkedHashMap<>();
     
         // key is the term to identify the bprod, value is the name used for that function.
    -    private final HashMap usedBprodTerms = new LinkedHashMap();
    +    private final Map usedBprodTerms = new LinkedHashMap<>();
     
         @Override
         public void init(MasterHandler masterHandler, Services services, Properties handlerSnippets,
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
    index 6af2aa727ce..dabb6ca7ad6 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
    @@ -51,12 +51,6 @@ public ContractPO createProofObl(InitConfig initConfig) {
             return new FunctionalBlockContractPO(initConfig, this);
         }
     
    -    @Override
    -    public ProofOblInput createProofObl(InitConfig initConfig, Contract contract) {
    -        assert contract instanceof FunctionalBlockContract;
    -        return new FunctionalBlockContractPO(initConfig, (FunctionalBlockContract) contract);
    -    }
    -
         @Override
         public ProofOblInput createProofObl(InitConfig initConfig, Contract contract,
                 boolean supportSymbolicExecutionAPI) {
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
    index 134711d1d30..ff2ae281ed4 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
    @@ -581,20 +581,16 @@ private static void replaceVariable(ProgramVariable var, Expression init,
                 Map preReplacementMap, Map postReplacementMap,
                 LoopContractImpl r, Services services) {
             switch (ReplaceTypes.fromClass(init.getClass())) {
    -        case PROGRAM_VARIABLE:
    -            replaceVariable(var, (ProgramVariable) init, preReplacementMap, postReplacementMap, r,
    -                services);
    -            break;
    -        case ABSTRACT_INTEGER_LITERAL:
    -            replaceVariable(var, (AbstractIntegerLiteral) init, preReplacementMap,
    -                postReplacementMap, r, services);
    -            break;
    -        case EMPTY_SEQ_LITERAL:
    -            replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap, postReplacementMap, r,
    -                services);
    -            break;
    -        default:
    -            throw new AssertionError();
    +        case PROGRAM_VARIABLE -> replaceVariable(var, (ProgramVariable) init, preReplacementMap,
    +            postReplacementMap, r,
    +            services);
    +        case ABSTRACT_INTEGER_LITERAL -> replaceVariable(var, (AbstractIntegerLiteral) init,
    +            preReplacementMap,
    +            postReplacementMap, r, services);
    +        case EMPTY_SEQ_LITERAL -> replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap,
    +            postReplacementMap, r,
    +            services);
    +        default -> throw new AssertionError();
             }
         }
     
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
    index 65c03d0b2b0..f7e22b22022 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
    @@ -148,17 +148,13 @@ private Map getReplaceMap(Map atPres, Servic
     
         private static Class latticeTypeFromString(
                 String latticeTypeStr) {
    -        switch (latticeTypeStr) {
    -        case "simple":
    -            return SimplePredicateAbstractionLattice.class;
    -        case "conjunctive":
    -            return ConjunctivePredicateAbstractionLattice.class;
    -        case "disjunctive":
    -            return DisjunctivePredicateAbstractionLattice.class;
    -        default:
    -            throw new RuntimeException(
    -                "PredicateAbstractionMergeContract: Unexpected lattice type: " + latticeTypeStr);
    -        }
    +        return switch (latticeTypeStr) {
    +        case "simple" -> SimplePredicateAbstractionLattice.class;
    +        case "conjunctive" -> ConjunctivePredicateAbstractionLattice.class;
    +        case "disjunctive" -> DisjunctivePredicateAbstractionLattice.class;
    +        default -> throw new RuntimeException(
    +            "PredicateAbstractionMergeContract: Unexpected lattice type: " + latticeTypeStr);
    +        };
         }
     
     }
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
    index afa088210c4..a9bb592cbb0 100644
    --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
    +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
    @@ -17,9 +17,9 @@
     /**
      * This class is used to resolve arithmetic operations to {@link SLExpression}s. These are overladed
      * for different primitive types.
    - *
    + * 

    * It delegates to the {@link JMLOperatorHandler}s registered in the class. - * + *

    * Numeric promotion plays into it, too. * * @author Alexander Weigl @@ -175,23 +175,16 @@ public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) final var l = left.getTerm(); final var r = right.getTerm(); if (l.sort() == ldt.targetSort() && r.sort() == ldt.targetSort()) { - switch (op) { - case ADD: - case BITWISE_OR: - return new SLExpression(tb.union(l, r)); - case SUBTRACT: - return new SLExpression(tb.setMinus(l, r)); - case BITWISE_AND: - return new SLExpression(tb.intersect(l, r)); - case LT: - return new SLExpression(tb.subset(l, r)); - case LTE: - return new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r))); - case GT: - return new SLExpression(tb.subset(r, l)); - case GTE: - return new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r))); - } + return switch (op) { + case ADD, BITWISE_OR -> new SLExpression(tb.union(l, r)); + case SUBTRACT -> new SLExpression(tb.setMinus(l, r)); + case BITWISE_AND -> new SLExpression(tb.intersect(l, r)); + case LT -> new SLExpression(tb.subset(l, r)); + case LTE -> new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r))); + case GT -> new SLExpression(tb.subset(r, l)); + case GTE -> new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r))); + default -> null; + }; } return null; } @@ -208,21 +201,19 @@ public BinaryBooleanHandler(Services services) { @Nullable @Override - public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) - throws SLTranslationException { + public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) { if ((left.getTerm().sort() == sortBoolean || left.getTerm().sort() == Sort.FORMULA) && (right.getTerm().sort() == sortBoolean || right.getTerm().sort() == Sort.FORMULA)) { final var t1 = tb.convertToFormula(left.getTerm()); final var t2 = tb.convertToFormula(right.getTerm()); - switch (op) { - case BITWISE_AND: - return new SLExpression(tb.and(t1, t2)); - case BITWISE_OR: - return new SLExpression(tb.or(t1, t2)); - case BITWISE_XOR: - return new SLExpression(tb.or(tb.and(t1, tb.not(t2)), tb.and(tb.not(t1), t2))); - } + return switch (op) { + case BITWISE_AND -> new SLExpression(tb.and(t1, t2)); + case BITWISE_OR -> new SLExpression(tb.or(t1, t2)); + case BITWISE_XOR -> new SLExpression( + tb.or(tb.and(t1, tb.not(t2)), tb.and(tb.not(t1), t2))); + default -> null; + }; } return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index ba37105c5c1..44f3d4a8087 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -41,59 +41,34 @@ public static JMLModifier modifierFromToken(Token token) { return null; } - switch (token.getType()) { - case JmlLexer.ABSTRACT: - return JMLModifier.ABSTRACT; - case JmlLexer.FINAL: - return JMLModifier.FINAL; - case JmlLexer.GHOST: - return JMLModifier.GHOST; - case JmlLexer.HELPER: - return JMLModifier.HELPER; - case JmlLexer.INSTANCE: - return JMLModifier.INSTANCE; - case JmlLexer.MODEL: - return JMLModifier.MODEL; - case JmlLexer.NON_NULL: - return JMLModifier.NON_NULL; - case JmlLexer.NULLABLE: - return JMLModifier.NULLABLE; - case JmlLexer.NULLABLE_BY_DEFAULT: - return JMLModifier.NULLABLE_BY_DEFAULT; - case JmlLexer.PRIVATE: - return JMLModifier.PRIVATE; - case JmlLexer.PROTECTED: - return JMLModifier.PROTECTED; - case JmlLexer.PUBLIC: - return JMLModifier.PUBLIC; - case JmlLexer.PURE: - return JMLModifier.PURE; - case JmlLexer.STRICTLY_PURE: - return JMLModifier.STRICTLY_PURE; - case JmlLexer.SPEC_PROTECTED: - return JMLModifier.SPEC_PROTECTED; - case JmlLexer.SPEC_PUBLIC: - return JMLModifier.SPEC_PUBLIC; - case JmlLexer.STATIC: - return JMLModifier.STATIC; - case JmlLexer.TWO_STATE: - return JMLModifier.TWO_STATE; - case JmlLexer.NO_STATE: - return JMLModifier.NO_STATE; - case JmlLexer.SPEC_JAVA_MATH: - return JMLModifier.SPEC_JAVA_MATH; - case JmlLexer.SPEC_SAFE_MATH: - return JMLModifier.SPEC_SAFE_MATH; - case JmlLexer.SPEC_BIGINT_MATH: - return JMLModifier.SPEC_BIGINT_MATH; - case JmlLexer.CODE_JAVA_MATH: - return JMLModifier.CODE_JAVA_MATH; - case JmlLexer.CODE_SAFE_MATH: - return JMLModifier.CODE_SAFE_MATH; - case JmlLexer.CODE_BIGINT_MATH: - return JMLModifier.CODE_BIGINT_MATH; - } - throw new IllegalStateException("Illegal token is given"); + return switch (token.getType()) { + case JmlLexer.ABSTRACT -> JMLModifier.ABSTRACT; + case JmlLexer.FINAL -> JMLModifier.FINAL; + case JmlLexer.GHOST -> JMLModifier.GHOST; + case JmlLexer.HELPER -> JMLModifier.HELPER; + case JmlLexer.INSTANCE -> JMLModifier.INSTANCE; + case JmlLexer.MODEL -> JMLModifier.MODEL; + case JmlLexer.NON_NULL -> JMLModifier.NON_NULL; + case JmlLexer.NULLABLE -> JMLModifier.NULLABLE; + case JmlLexer.NULLABLE_BY_DEFAULT -> JMLModifier.NULLABLE_BY_DEFAULT; + case JmlLexer.PRIVATE -> JMLModifier.PRIVATE; + case JmlLexer.PROTECTED -> JMLModifier.PROTECTED; + case JmlLexer.PUBLIC -> JMLModifier.PUBLIC; + case JmlLexer.PURE -> JMLModifier.PURE; + case JmlLexer.STRICTLY_PURE -> JMLModifier.STRICTLY_PURE; + case JmlLexer.SPEC_PROTECTED -> JMLModifier.SPEC_PROTECTED; + case JmlLexer.SPEC_PUBLIC -> JMLModifier.SPEC_PUBLIC; + case JmlLexer.STATIC -> JMLModifier.STATIC; + case JmlLexer.TWO_STATE -> JMLModifier.TWO_STATE; + case JmlLexer.NO_STATE -> JMLModifier.NO_STATE; + case JmlLexer.SPEC_JAVA_MATH -> JMLModifier.SPEC_JAVA_MATH; + case JmlLexer.SPEC_SAFE_MATH -> JMLModifier.SPEC_SAFE_MATH; + case JmlLexer.SPEC_BIGINT_MATH -> JMLModifier.SPEC_BIGINT_MATH; + case JmlLexer.CODE_JAVA_MATH -> JMLModifier.CODE_JAVA_MATH; + case JmlLexer.CODE_SAFE_MATH -> JMLModifier.CODE_SAFE_MATH; + case JmlLexer.CODE_BIGINT_MATH -> JMLModifier.CODE_BIGINT_MATH; + default -> throw new IllegalStateException("Illegal token is given"); + }; } @Override @@ -130,24 +105,16 @@ private Behavior getBehavior(Token behavior) { if (behavior == null) { return Behavior.NONE; // lightweight specification } - - switch (behavior.getType()) { - case JmlLexer.BEHAVIOR: - return Behavior.BEHAVIOR; - case JmlLexer.NORMAL_BEHAVIOR: - return Behavior.NORMAL_BEHAVIOR; - case JmlLexer.BREAK_BEHAVIOR: - return Behavior.BREAK_BEHAVIOR; - case JmlLexer.EXCEPTIONAL_BEHAVIOUR: - return Behavior.EXCEPTIONAL_BEHAVIOR; - case JmlLexer.MODEL_BEHAVIOUR: - return Behavior.MODEL_BEHAVIOR; - case JmlLexer.RETURN_BEHAVIOR: - return Behavior.RETURN_BEHAVIOR; - case JmlLexer.CONTINUE_BEHAVIOR: - return Behavior.CONTINUE_BEHAVIOR; - } - throw new IllegalStateException("No behavior is given"); + return switch (behavior.getType()) { + case JmlLexer.BEHAVIOR -> Behavior.BEHAVIOR; + case JmlLexer.NORMAL_BEHAVIOR -> Behavior.NORMAL_BEHAVIOR; + case JmlLexer.BREAK_BEHAVIOR -> Behavior.BREAK_BEHAVIOR; + case JmlLexer.EXCEPTIONAL_BEHAVIOUR -> Behavior.EXCEPTIONAL_BEHAVIOR; + case JmlLexer.MODEL_BEHAVIOUR -> Behavior.MODEL_BEHAVIOR; + case JmlLexer.RETURN_BEHAVIOR -> Behavior.RETURN_BEHAVIOR; + case JmlLexer.CONTINUE_BEHAVIOR -> Behavior.CONTINUE_BEHAVIOR; + default -> throw new IllegalStateException("No behavior is given"); + }; } @Override @@ -174,7 +141,7 @@ public Object visitSpec_body(JmlParser.Spec_bodyContext ctx) { @Override public Name[] visitTargetHeap(JmlParser.TargetHeapContext ctx) { - if (ctx == null || ctx.SPECIAL_IDENT().size() == 0) { + if (ctx == null || ctx.SPECIAL_IDENT().isEmpty()) { return new Name[] { HeapLDT.BASE_HEAP_NAME }; } Name[] heaps = new Name[ctx.SPECIAL_IDENT().size()]; @@ -445,7 +412,7 @@ public Object visitClass_axiom(JmlParser.Class_axiomContext ctx) { @Override public Object visitField_declaration(JmlParser.Field_declarationContext ctx) { - assert mods.size() > 0; + assert !mods.isEmpty(); TextualJMLFieldDecl inv = new TextualJMLFieldDecl(mods, ctx); constructs = constructs.append(inv); return null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index a5873acb47e..b8a497afa50 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -1702,18 +1702,15 @@ public Object visitSequenceFuncs(JmlParser.SequenceFuncsContext ctx) { final Term t2 = e2.getTerm(); final Term t1 = e1.getTerm(); - switch (ctx.op.getType()) { - case JmlLexer.SEQCONCAT: - return termFactory.seqConcat(t1, t2); - case JmlLexer.SEQGET: - return termFactory.seqGet(t1, t2); - case JmlLexer.INDEXOF: - return termFactory.createIndexOf(t1, t2); - default: - raiseError(ctx, "Unexpected syntax case."); - } - raiseError(ctx, "Unknown operator: %s", ctx.op); - return null; + return switch (ctx.op.getType()) { + case JmlLexer.SEQCONCAT -> termFactory.seqConcat(t1, t2); + case JmlLexer.SEQGET -> termFactory.seqGet(t1, t2); + case JmlLexer.INDEXOF -> termFactory.createIndexOf(t1, t2); + default -> { + raiseError(ctx, "Unknown operator: %s", ctx.op); + yield null; + } + }; } @Override @@ -1738,42 +1735,37 @@ public SLExpression visitSpecquantifiedexpression( guard = a.getTerm(); } SLExpression expr = - ctx.expression().size() == 2 ? accept(ctx.expression(1)) : accept(ctx.expression(0)); + ctx.expression().size() == 2 ? accept(ctx.expression(1)) : accept(ctx.expression(0)); resolverManager.popLocalVariablesNamespace(); assert guard != null; guard = tb.convertToFormula(guard); assert expr != null; final Term body = expr.getTerm(); - switch (ctx.quantifier().start.getType()) { - case JmlLexer.FORALL: - return termFactory.forall(guard, body, declVars.first, declVars.second, nullable, - expr.getType()); - case JmlLexer.EXISTS: - return termFactory.exists(guard, body, declVars.first, declVars.second, nullable, - expr.getType()); - case JmlLexer.MAX: - return termFactory.quantifiedMax(guard, body, declVars.first, nullable, - declVars.second); - case JmlLexer.MIN: - return termFactory.quantifiedMin(guard, body, declVars.first, nullable, - declVars.second); - case JmlLexer.NUM_OF: - KeYJavaType kjtInt = - services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT); - return termFactory.quantifiedNumOf(guard, body, declVars.first, nullable, - declVars.second, kjtInt); - case JmlLexer.SUM: - return termFactory.quantifiedSum(declVars.first, nullable, declVars.second, guard, body, - expr.getType()); - case JmlLexer.PRODUCT: - return termFactory.quantifiedProduct(declVars.first, nullable, declVars.second, guard, - body, expr.getType()); - default: - raiseError(ctx, "Unexpected syntax case."); - } - raiseError(ctx, "Unexpected syntax case."); - return null; + return switch (ctx.quantifier().start.getType()) { + case JmlLexer.FORALL -> termFactory.forall(guard, body, declVars.first, declVars.second, nullable, + expr.getType()); + case JmlLexer.EXISTS -> termFactory.exists(guard, body, declVars.first, declVars.second, nullable, + expr.getType()); + case JmlLexer.MAX -> termFactory.quantifiedMax(guard, body, declVars.first, nullable, + declVars.second); + case JmlLexer.MIN -> termFactory.quantifiedMin(guard, body, declVars.first, nullable, + declVars.second); + case JmlLexer.NUM_OF -> { + KeYJavaType kjtInt = + services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT); + yield termFactory.quantifiedNumOf(guard, body, declVars.first, nullable, + declVars.second, kjtInt); + } + case JmlLexer.SUM -> termFactory.quantifiedSum(declVars.first, nullable, declVars.second, guard, body, + expr.getType()); + case JmlLexer.PRODUCT -> termFactory.quantifiedProduct(declVars.first, nullable, declVars.second, guard, + body, expr.getType()); + default -> { + raiseError(ctx, "Unexpected syntax case."); + yield null; + } + }; } @Override @@ -1903,8 +1895,7 @@ public KeYJavaType visitTypespec(JmlParser.TypespecContext ctx) { try { javaInfo.readJavaBlock("{" + fullName + " k;}"); t = javaInfo.getKeYJavaType(fullName); - } catch (Exception e) { - t = null; + } catch (Exception ignored) { } } return t; @@ -1961,9 +1952,7 @@ public LogicVariable visitQuantifiedvariabledeclarator( } else { fullName.append(t.getFullName()); } - for (int i = 0; i < dim; i++) { - fullName.append("[]"); - } + fullName.append("[]".repeat(dim)); varType = javaInfo.getKeYJavaType(fullName.toString()); } else { varType = t; @@ -2132,14 +2121,9 @@ private void insertSimpleClause(String type, LocationVariable heap, Term t, ContractClauses.Clauses free, ContractClauses.Clauses redundantly) { switch (subType(type)) { - case FREE: - contractClauses.add(free, heap, t); - break; - case REDUNDANT: - contractClauses.add(redundantly, heap, t); - break; - default: - contractClauses.add(none, heap, t); + case FREE -> contractClauses.add(free, heap, t); + case REDUNDANT -> contractClauses.add(redundantly, heap, t); + default -> contractClauses.add(none, heap, t); } } @@ -2531,19 +2515,10 @@ public LocationVariable[] visitTargetHeap(JmlParser.TargetHeapContext ctx) { for (int i = 0; i < ctx.SPECIAL_IDENT().size(); i++) { String heapName = ctx.SPECIAL_IDENT(i).getText(); switch (heapName) { - case "": - case "": - heaps[i] = getPermissionHeap(); - break; - case "": - case "": - heaps[i] = getSavedHeap(); - break; - case "": - heaps[i] = getBaseHeap(); - break; - default: - heaps[i] = heapLDT.getHeapForName(new Name(heapName)); + case "", "" -> heaps[i] = getPermissionHeap(); + case "", "" -> heaps[i] = getSavedHeap(); + case "" -> heaps[i] = getBaseHeap(); + default -> heaps[i] = heapLDT.getHeapForName(new Name(heapName)); } } return heaps; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java index 174706502cd..65ed989a381 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java @@ -35,11 +35,10 @@ public abstract class SLResolverManager { private final boolean useLocalVarsAsImplicitReceivers; private final TermBuilder tb; - private ImmutableList> /* ParsableVariable */ - localVariablesNamespaces = ImmutableSLList.nil(); + private ImmutableList> localVariablesNamespaces = + ImmutableSLList.nil(); - private final Map kjts = - new LinkedHashMap<>(); + private final Map kjts = new LinkedHashMap<>(); // ------------------------------------------------------------------------- // constructors @@ -122,8 +121,7 @@ private SLExpression resolveImplicit(String name, SLParameters parameters) // (e.g. for static attributes or static methods) if (specInClass != null) { SLExpression receiver = new SLExpression(specInClass); - SLExpression result = resolveExplicit(receiver, name, parameters); - return result; + return resolveExplicit(receiver, name, parameters); } return null; @@ -152,7 +150,7 @@ private SLExpression resolveExplicit(SLExpression receiver, String name, SLParam */ private SLExpression resolveIt(SLExpression receiver, String name, SLParameters parameters) throws SLTranslationException { - SLExpression result = null; + SLExpression result; if (receiver != null) { result = resolveExplicit(receiver, name, parameters); @@ -181,7 +179,6 @@ private SLExpression resolveIt(SLExpression receiver, String name, SLParameters * @param name name of the property * @param parameters actual parameters of the property call, or null * @return corresponding term, type or collection if successful, null otherwise - * @throws SLTranslationException */ public SLExpression resolve(SLExpression receiver, String name, SLParameters parameters) throws SLTranslationException { @@ -203,8 +200,7 @@ public SLExpression resolve(SLExpression receiver, String name, SLParameters par * Pushes a new, empty namespace onto the stack. */ public void pushLocalVariablesNamespace() { - // FIXME: This breaks the generics of namespaces. - Namespace ns = new Namespace(); + var ns = new Namespace(); localVariablesNamespaces = localVariablesNamespaces.prepend(ns); } @@ -213,8 +209,7 @@ public void pushLocalVariablesNamespace() { * Puts a local variable into the topmost namespace on the stack */ public void putIntoTopLocalVariablesNamespace(ParsableVariable pv, KeYJavaType kjt) { - // FIXME: This breaks the generics of Namespaces. - ((Namespace) localVariablesNamespaces.head()).addSafely(pv); + localVariablesNamespaces.head().addSafely(pv); kjts.put(pv, kjt); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index 25611a27205..d6c8d662444 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -124,32 +124,32 @@ protected Feature setupGlobalF(Feature dispatcher) { final Feature methodSpecF; final String methProp = strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY); - if (methProp.equals(StrategyProperties.METHOD_CONTRACT)) { - methodSpecF = methodSpecFeature(longConst(-20)); - } else if (methProp.equals(StrategyProperties.METHOD_EXPAND)) { - methodSpecF = methodSpecFeature(inftyConst()); - } else if (methProp.equals(StrategyProperties.METHOD_NONE)) { - methodSpecF = methodSpecFeature(inftyConst()); - } else { + switch (methProp) { + case StrategyProperties.METHOD_CONTRACT -> methodSpecF = methodSpecFeature(longConst(-20)); + case StrategyProperties.METHOD_EXPAND -> methodSpecF = methodSpecFeature(inftyConst()); + case StrategyProperties.METHOD_NONE -> methodSpecF = methodSpecFeature(inftyConst()); + default -> { methodSpecF = null; assert false; } + } final String queryProp = strategyProperties.getProperty(StrategyProperties.QUERY_OPTIONS_KEY); final Feature queryF; - if (queryProp.equals(StrategyProperties.QUERY_ON)) { - queryF = querySpecFeature(new QueryExpandCost(200, 1, 1, false)); - } else if (queryProp.equals(StrategyProperties.QUERY_RESTRICTED)) { + switch (queryProp) { + case StrategyProperties.QUERY_ON -> queryF = + querySpecFeature(new QueryExpandCost(200, 1, 1, false)); + case StrategyProperties.QUERY_RESTRICTED -> // All tests in the example directory pass with this strategy. // Hence, the old query_on strategy is obsolete. queryF = querySpecFeature(new QueryExpandCost(500, 0, 1, true)); - } else if (queryProp.equals(StrategyProperties.QUERY_OFF)) { - queryF = querySpecFeature(inftyConst()); - } else { + case StrategyProperties.QUERY_OFF -> queryF = querySpecFeature(inftyConst()); + default -> { queryF = null; assert false; } + } final Feature depSpecF; final String depProp = strategyProperties.getProperty(StrategyProperties.DEP_OPTIONS_KEY); @@ -383,56 +383,39 @@ private RuleSetDispatchFeature setupCostComputationF() { strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY); switch (methProp) { - case StrategyProperties.METHOD_CONTRACT: + case StrategyProperties.METHOD_CONTRACT -> /* * If method treatment by contracts is chosen, this does not mean that method expansion * is disabled. The original cost was 200 and is now increased to 2000 in order to * repress method expansion stronger when method treatment by contracts is chosen. */ bindRuleSet(d, "method_expand", longConst(2000)); - break; - case StrategyProperties.METHOD_EXPAND: - bindRuleSet(d, "method_expand", longConst(100)); - break; - case StrategyProperties.METHOD_NONE: - bindRuleSet(d, "method_expand", inftyConst()); - break; - default: - throw new RuntimeException("Unexpected strategy property " + methProp); + case StrategyProperties.METHOD_EXPAND -> bindRuleSet(d, "method_expand", longConst(100)); + case StrategyProperties.METHOD_NONE -> bindRuleSet(d, "method_expand", inftyConst()); + default -> throw new RuntimeException("Unexpected strategy property " + methProp); } final String mpsProp = strategyProperties.getProperty(StrategyProperties.MPS_OPTIONS_KEY); switch (mpsProp) { - case StrategyProperties.MPS_MERGE: + case StrategyProperties.MPS_MERGE -> /* * For this case, we use a special feature, since deleting merge points should only be * done after a merge rule application. */ bindRuleSet(d, "merge_point", DeleteMergePointRuleFeature.INSTANCE); - break; - case StrategyProperties.MPS_SKIP: - bindRuleSet(d, "merge_point", longConst(-5000)); - break; - case StrategyProperties.MPS_NONE: - bindRuleSet(d, "merge_point", inftyConst()); - break; - default: - throw new RuntimeException("Unexpected strategy property " + methProp); + case StrategyProperties.MPS_SKIP -> bindRuleSet(d, "merge_point", longConst(-5000)); + case StrategyProperties.MPS_NONE -> bindRuleSet(d, "merge_point", inftyConst()); + default -> throw new RuntimeException("Unexpected strategy property " + methProp); } final String queryAxProp = strategyProperties.getProperty(StrategyProperties.QUERYAXIOM_OPTIONS_KEY); switch (queryAxProp) { - case StrategyProperties.QUERYAXIOM_ON: - bindRuleSet(d, "query_axiom", longConst(-3000)); - break; - case StrategyProperties.QUERYAXIOM_OFF: - bindRuleSet(d, "query_axiom", inftyConst()); - break; - default: - throw new RuntimeException("Unexpected strategy property " + queryAxProp); + case StrategyProperties.QUERYAXIOM_ON -> bindRuleSet(d, "query_axiom", longConst(-3000)); + case StrategyProperties.QUERYAXIOM_OFF -> bindRuleSet(d, "query_axiom", inftyConst()); + default -> throw new RuntimeException("Unexpected strategy property " + queryAxProp); } if (classAxiomApplicationEnabled()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java index 7919f201d07..9c8de611c8b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java @@ -5,7 +5,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.inst.SVInstantiations.UpdateLabelPair; @@ -19,15 +18,6 @@ public class NonDuplicateAppModPositionFeature extends NonDuplicateAppFeature { public static final Feature INSTANCE = new NonDuplicateAppModPositionFeature(); - @Override - public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal) { - if (!app.ifInstsComplete()) { - return true; - } - - return noDuplicateFindTaclet(app, pos, goal); - } - @Override protected boolean comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java index a0e6ed622d5..947180e9da8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java @@ -42,12 +42,10 @@ protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) { * @param sort2 */ protected boolean compare(final Sort sort1, final Sort sort2) { - switch (comparator) { - case SUBSORT: + if (comparator == SUBSORT) { return sort1.extendsTrans(sort2); - default: - return false; } + return false; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java index 4438935d470..2030daafa5c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java @@ -99,30 +99,28 @@ private Term breakDownEq(Term var, BigInteger lit, int pow, TermServices service if ((pow % 2 == 0)) { // the even case - - switch (lit.signum()) { - case -1: - // no solutions - return tb.ff(); - case 0: - // exactly one solution - return tb.equals(var, zero); - case 1: - final BigInteger r = root(lit, pow); - if (power(r, pow).equals(lit)) { - // two solutions - final Term rTerm = tb.zTerm(r.toString()); - final Term rNegTerm = tb.zTerm(r.negate().toString()); - return tb.or(tb.or(tb.lt(var, rNegTerm), tb.gt(var, rTerm)), - tb.and(tb.gt(var, rNegTerm), tb.lt(var, rTerm))); - } else { - // no solution - return tb.ff(); + return switch (lit.signum()) { + case -1 -> // no solutions + tb.ff(); + case 0 -> // exactly one solution + tb.equals(var, zero); + case 1 -> { + final BigInteger r = root(lit, pow); + if (power(r, pow).equals(lit)) { + // two solutions + final Term rTerm = tb.zTerm(r.toString()); + final Term rNegTerm = tb.zTerm(r.negate().toString()); + yield tb.or(tb.or(tb.lt(var, rNegTerm), tb.gt(var, rTerm)), + tb.and(tb.gt(var, rNegTerm), tb.lt(var, rTerm))); + } else { + // no solution + yield tb.ff(); + } } - } + default -> null; + }; } else { // the odd case - final BigInteger r = root(lit, pow); if (power(r, pow).equals(lit)) { // one solution @@ -133,60 +131,49 @@ private Term breakDownEq(Term var, BigInteger lit, int pow, TermServices service return tb.ff(); } } - - assert false; // unreachable - return null; } private Term breakDownGeq(Term var, BigInteger lit, int pow, TermServices services) { if ((pow % 2 == 0)) { // the even case - switch (lit.signum()) { - case -1: - case 0: - // the inequation is no restriction - return tb.ff(); - case 1: - final BigInteger r = rootRoundingUpwards(lit, pow); - final Term rTerm = tb.zTerm(r.toString()); - final Term rNegTerm = tb.zTerm(r.negate().toString()); - return tb.or(tb.leq(var, rNegTerm), tb.geq(var, rTerm)); - } + return switch (lit.signum()) { + case -1, 0 -> // the inequation is no restriction + tb.ff(); + case 1 -> { + final BigInteger r = rootRoundingUpwards(lit, pow); + final Term rTerm = tb.zTerm(r.toString()); + final Term rNegTerm = tb.zTerm(r.negate().toString()); + yield tb.or(tb.leq(var, rNegTerm), tb.geq(var, rTerm)); + } + default -> throw new IllegalStateException("Unexpected value: " + lit.signum()); + }; } else { // the odd case - return tb.geq(var, tb.zTerm(rootRoundingUpwards(lit, pow).toString())); } - - assert false; // unreachable - return null; } private Term breakDownLeq(Term var, BigInteger lit, int pow, TermServices services) { if ((pow % 2 == 0)) { // the even case - switch (lit.signum()) { - case -1: - // no solutions - return tb.ff(); - case 0: - return tb.equals(var, tb.zero()); - case 1: - final BigInteger r = root(lit, pow); - final Term rTerm = tb.zTerm(r.toString()); - final Term rNegTerm = tb.zTerm(r.negate().toString()); - return tb.and(tb.geq(var, rNegTerm), tb.leq(var, rTerm)); - } + return switch (lit.signum()) { + case -1 -> // no solutions + tb.ff(); + case 0 -> tb.equals(var, tb.zero()); + case 1 -> { + final BigInteger r = root(lit, pow); + final Term rTerm = tb.zTerm(r.toString()); + final Term rNegTerm = tb.zTerm(r.negate().toString()); + yield tb.and(tb.geq(var, rNegTerm), tb.leq(var, rTerm)); + } + default -> throw new IllegalStateException("Unexpected value: " + lit.signum()); + }; } else { // the odd case - return tb.leq(var, tb.zTerm(root(lit, pow).toString())); } - - assert false; // unreachable - return null; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java index 237622b58fa..b98c32a8df0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java @@ -69,8 +69,7 @@ private Term translateReplaceAndAddTerm(TacletGoalTemplate template, Term find, replace = TacletSections.REPLACE.getDefaultValue(services); } - Term term = tb.imp(tb.equals(find, replace), add); - return term; + return tb.imp(tb.equals(find, replace), add); } /** @@ -105,29 +104,23 @@ private Term translateReplaceAndAddFormula(TacletGoalTemplate template, Term fin assert polarity == 0 || add == TacletSections.ADD.getDefaultValue(services) : "add() commands not allowed in polarity rules (syntactically forbidden)"; - Term term = tb.imp(translateEquivalence(find, replace, polarity, services), add); - return term; + return tb.imp(translateEquivalence(find, replace, polarity, services), add); } private Term translateEquivalence(Term find, Term replace, int polarity, TermServices services) { TermBuilder tb = services.getTermBuilder(); - switch (polarity) { - case 0: - return tb.equals(find, replace); - case 1: - return tb.imp(replace, find); - case -1: - return tb.imp(find, replace); - default: - throw new IllegalArgumentException(); - } + return switch (polarity) { + case 0 -> tb.equals(find, replace); + case 1 -> tb.imp(replace, find); + case -1 -> tb.imp(find, replace); + default -> throw new IllegalArgumentException(); + }; } private Term translateReplaceAndAddSequent(TacletGoalTemplate template, int type, TermServices services) { - TermBuilder tb = services.getTermBuilder(); Sequent replace = null; if (template instanceof AntecSuccTacletGoalTemplate) { @@ -144,8 +137,7 @@ private Term translateReplaceAndAddSequent(TacletGoalTemplate template, int type if (rep == null) { rep = TacletSections.REPLACE.getDefaultValue(services); } - Term term = tb.or(rep, add); - return term; + return tb.or(rep, add); } /** @@ -215,7 +207,7 @@ public Term translate(Taclet taclet, TermServices services) throws IllegalTaclet /** * Retrieve the "find" Term from a FindTaclet. - * + *

    * Originally, this simply calls {@link FindTaclet#find()}. Overriding classes may choose to * garnish the result with additional information. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java index 8ae2adfa0bd..5fe559c193a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java @@ -54,7 +54,7 @@ public UserDefinedSymbols(UserDefinedSymbols parent) { this.referenceNamespaces = parent.referenceNamespaces; } - private void addUserDefiniedSymbol(T symbol, Set set, + private void addUserDefinedSymbol(T symbol, Set set, Namespace excludeNamespace) { if (!contains(symbol, set)) { if (symbol instanceof SchemaVariable @@ -74,11 +74,11 @@ private boolean contains(T symbol, Set set) { } public void addFunction(Function symbol) { - addUserDefiniedSymbol(symbol, usedExtraFunctions, referenceNamespaces.functions()); + addUserDefinedSymbol(symbol, usedExtraFunctions, referenceNamespaces.functions()); } public void addPredicate(Function symbol) { - addUserDefiniedSymbol(symbol, usedExtraPredicates, referenceNamespaces.functions()); + addUserDefinedSymbol(symbol, usedExtraPredicates, referenceNamespaces.functions()); } public void addSort(Named symbol) { @@ -89,17 +89,18 @@ public void addSort(Named symbol) { addSort(parentSort); } } - addUserDefiniedSymbol(sort, usedExtraSorts, referenceNamespaces.sorts()); + addUserDefinedSymbol(sort, usedExtraSorts, referenceNamespaces.sorts()); } } public void addVariable(QuantifiableVariable symbol) { - addUserDefiniedSymbol(symbol, usedExtraVariables, referenceNamespaces.variables()); + addUserDefinedSymbol(symbol, usedExtraVariables, referenceNamespaces.variables()); } + @SuppressWarnings({ "rawtypes", "unchecked" }) public void addSchemaVariable(SchemaVariable symbol) { // FIXME: This breaks the generics of namespace - addUserDefiniedSymbol(symbol, usedSchemaVariables, + addUserDefinedSymbol(symbol, usedSchemaVariables, (Namespace) referenceNamespaces.variables()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java index 42c58beb19a..5eeecfc3891 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java @@ -59,9 +59,11 @@ */ public final class MiscTools { - /** Pattern to parse URL scheme (capture group 1) and scheme specific part (group 2). */ + /** + * Pattern to parse URL scheme (capture group 1) and scheme specific part (group 2). + */ private static final Pattern URL_PATTERN = - Pattern.compile("(^[a-zA-Z][a-zA-Z0-9\\+\\-\\.]*):(.*)"); + Pattern.compile("(^[a-zA-Z][a-zA-Z0-9+\\-.]*):(.*)"); private MiscTools() { } @@ -362,12 +364,11 @@ public static Name toValidVariableName(String s) { /** * Join the string representations of a collection of objects into onw string. The individual * elements are separated by a delimiter. - * + *

    * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null collection * @param delimiter a non-null string which is put between the elements. - * * @return the concatenation of all string representations separated by the delimiter */ public static String join(Iterable collection, String delimiter) { @@ -377,12 +378,11 @@ public static String join(Iterable collection, String delimiter) { /** * Join the string representations of an array of objects into one string. The individual * elements are separated by a delimiter. - * + *

    * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null array of objects * @param delimiter a non-null string which is put between the elements. - * * @return the concatenation of all string representations separated by the delimiter */ public static String join(Object[] collection, String delimiter) { @@ -392,13 +392,12 @@ public static String join(Object[] collection, String delimiter) { /** * Takes a string and returns a string which is potentially shorter and contains a * sub-collection of the original characters. - * + *

    * All alphabetic characters (A-Z and a-z) are copied to the result while all other characters * are removed. * * @param string an arbitrary string * @return a string which is a sub-structure of the original character sequence - * * @author Mattias Ulbrich */ public static /* @ non_null @ */ String filterAlphabetic(/* @ non_null @ */ String string) { @@ -420,9 +419,6 @@ public static boolean containsWholeWord(String s, String word) { /** * There are different kinds of JML markers. See Section 4.4 "Annotation markers" of the JML * reference manual. - * - * @param comment - * @return */ public static boolean isJMLComment(String comment) { return Strings.isJMLComment(comment); @@ -733,31 +729,32 @@ public static Optional extractURI(DataLocation loc) { } try { - switch (loc.getType()) { - case "URL": // URLDataLocation - return Optional.of(((URLDataLocation) loc).url().toURI()); - case "ARCHIVE": // ArchiveDataLocation - // format: "ARCHIVE:?" - ArchiveDataLocation adl = (ArchiveDataLocation) loc; - - // extract item name and zip file - int qmindex = adl.toString().lastIndexOf('?'); - String itemName = adl.toString().substring(qmindex + 1); - ZipFile zip = adl.getFile(); - - // use special method to ensure that path separators are correct - return Optional.of(getZipEntryURI(zip, itemName)); - case "FILE": // DataFileLocation - // format: "FILE:" - return Optional.of(((DataFileLocation) loc).getFile().toURI()); - default: // SpecDataLocation - // format "://" - // wrap into URN to ensure URI encoding is correct (no spaces!) - return Optional.empty(); - } + return switch (loc.getType()) { + case "URL" -> // URLDataLocation + Optional.of(((URLDataLocation) loc).url().toURI()); + case "ARCHIVE" -> { // ArchiveDataLocation + // format: "ARCHIVE:?" + ArchiveDataLocation adl = (ArchiveDataLocation) loc; + + // extract item name and zip file + int qmindex = adl.toString().lastIndexOf('?'); + String itemName = adl.toString().substring(qmindex + 1); + ZipFile zip = adl.getFile(); + + // use special method to ensure that path separators are correct + yield Optional.of(getZipEntryURI(zip, itemName)); + } + case "FILE" -> // DataFileLocation + // format: "FILE:" + Optional.of(((DataFileLocation) loc).getFile().toURI()); + default -> // SpecDataLocation + // format "://" + // wrap into URN to ensure URI encoding is correct (no spaces!) + Optional.empty(); + }; } catch (URISyntaxException | IOException e) { throw new IllegalArgumentException( - "The given DataLocation can not be converted into a valid URI: " + loc, e); + "The given DataLocation can not be converted into a valid URI: " + loc, e); } } @@ -844,7 +841,7 @@ public static URI getURIFromTokenSource(String source) { *

* * - * + *

* A NullPointerException is thrown if null is given. If the input is "", ".", or a relative * path in general, the path is resolved against the current working directory (see system * property "user.dir") consistently to the behaviour of {@link Paths#get(String, String...)}. @@ -867,16 +864,16 @@ public static URL parseURL(final String input) throws MalformedURLException { schemeSpecPart = m.group(2); } switch (scheme) { - case "URL": + case "URL" -> { // schemeSpecPart actually contains a URL again return new URL(schemeSpecPart); - case "ARCHIVE": + } + case "ARCHIVE" -> { // format: "ARCHIVE:?" // extract item name and zip file int qmindex = schemeSpecPart.lastIndexOf('?'); String zipName = schemeSpecPart.substring(0, qmindex); String itemName = schemeSpecPart.substring(qmindex + 1); - try { ZipFile zip = new ZipFile(zipName); // use special method to ensure that path separators are correct @@ -887,15 +884,18 @@ public static URL parseURL(final String input) throws MalformedURLException { me.initCause(e); throw me; } - case "FILE": + } + case "FILE" -> { // format: "FILE:" Path path = Paths.get(schemeSpecPart).toAbsolutePath().normalize(); return path.toUri().toURL(); - case "": + } + case "" -> { // only file/path without protocol Path p = Paths.get(input).toAbsolutePath().normalize(); return p.toUri().toURL(); - default: + } + default -> { // may still be Windows path starting with : if (scheme.length() == 1) { // TODO: Theoretically, a protocol with only a single letter is allowed. @@ -907,5 +907,6 @@ public static URL parseURL(final String input) throws MalformedURLException { // if this also fails, there is an unknown protocol -> MalformedURLException return new URL(input); } + } } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java index 06f8d3ce048..b8dbbaf79b3 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java @@ -5,7 +5,6 @@ import java.io.File; import java.io.IOException; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Paths; import java.util.Map; @@ -29,7 +28,7 @@ * {@code generateRunAllProofs}. *

* The considered proof collections files are configured statically in - * {@link #collections}. + * {@link ProofCollections}. * * @author Alexander Weigl * @version 1 (6/14/20) @@ -57,41 +56,60 @@ public static void main(String[] args) throws IOException { for (var col : collections) { for (RunAllProofsTestUnit unit : col.createRunAllProofsTestUnits()) { - createUnitClass(col, unit); + createUnitClass(unit); } } } + // "import de.uka.ilkd.key.util.NamedRunner;\n" + + // "import de.uka.ilkd.key.util.TestName;\n" + + // "@org.junit.experimental.categories.Category(org.key_project.util.testcategories.ProofTestCategory.class)\n" + // + + // "@RunWith(NamedRunner.class)\n" + private static final String TEMPLATE_CONTENT = - "package $packageName;\n" + "\n" + "import org.junit.*;\n" + - // "import de.uka.ilkd.key.util.NamedRunner;\n" + - // "import de.uka.ilkd.key.util.TestName;\n" + - "import org.junit.rules.Timeout;\n" + "import org.junit.runner.RunWith;\n" + "\n" + - // "@org.junit.experimental.categories.Category(org.key_project.util.testcategories.ProofTestCategory.class)\n" - // + - // "@RunWith(NamedRunner.class)\n" + - "public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest {\n" - + "\n" + " public static final String STATISTIC_FILE = \"$statisticsFile\";\n\n" - + " @Before public void setUp() {\n" + " this.baseDirectory = \"$baseDirectory\";\n" - + " this.statisticsFile = STATISTIC_FILE;\n" + " this.name = \"$name\";\n" - + " this.reloadEnabled = $reloadEnabled;\n" + " this.tempDir = \"$tempDir\";\n" - + "\n" + " this.globalSettings = \"$keySettings\";\n" - + " this.localSettings = \"$localSettings\";\n" + " }\n" + "\n" + " $timeout\n" - + "\n" + " $methods\n" + "\n" + "}\n"; + """ + /* 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 $packageName; + + import org.junit.jupiter.api.*; + import static org.junit.jupiter.api.Assertions.*; + + public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest { + public static final String STATISTIC_FILE = "$statisticsFile"; + + { // initialize during construction + this.baseDirectory = "$baseDirectory"; + this.statisticsFile = STATISTIC_FILE; + this.name = "$name"; + this.reloadEnabled = $reloadEnabled; + this.tempDir = "$tempDir"; + + this.globalSettings = "$keySettings"; + this.localSettings = "$localSettings"; + } + + $timeout + $methods + } + """; /** * Generates the test classes for the given proof collection, and writes the * java files. * - * @param col - * @param unit + * @param unit a group of proof collection units * @throws IOException if the file is not writable */ - private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit unit) + private static void createUnitClass(RunAllProofsTestUnit unit) throws IOException { String packageName = "de.uka.ilkd.key.proof.runallproofs.gen"; String name = unit.getTestName(); - String className = name.replaceAll("\\.java", "").replaceAll("\\.key", "") + String className = '_' + name // avoids name clashes, i.e., group "switch" + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") .replaceAll("[^a-zA-Z0-9]+", "_"); ProofCollectionSettings settings = unit.getSettings(); @@ -126,7 +144,9 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un for (TestFile file : unit.getTestFiles()) { File keyFile = file.getKeYFile(); - String testName = keyFile.getName().replaceAll("\\.java", "").replaceAll("\\.key", "") + String testName = keyFile.getName() + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") .replaceAll("[^a-zA-Z0-9]+", "_"); if (usedMethodNames.contains(testName)) { @@ -139,26 +159,18 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un methods.append("\n"); methods.append("@Test(").append(to).append(")") // .append("@TestName(\"").append(keyFile.getName()).append("\")") - .append("public void test").append(testName).append("() throws Exception {\n"); + .append("void test").append(testName).append("() throws Exception {\n"); // "// This tests is based on").append(keyFile.getAbsolutePath()).append("\n"); switch (file.getTestProperty()) { - case PROVABLE: - methods.append("assertProvability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case NOTPROVABLE: - methods.append("assertUnProvability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case LOADABLE: - methods.append("assertLoadability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case NOTLOADABLE: - methods.append("assertUnLoadability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; + case PROVABLE -> methods.append("assertProvability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case NOTPROVABLE -> methods.append("assertUnProvability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case LOADABLE -> methods.append("assertLoadability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case NOTLOADABLE -> methods.append("assertUnLoadability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); } methods.append("}"); } @@ -174,7 +186,7 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un m.appendTail(sb); File folder = new File(outputFolder, packageName.replace('.', '/')); folder.mkdirs(); - Files.write(Paths.get(folder.getAbsolutePath(), className + ".java"), - sb.toString().getBytes(StandardCharsets.UTF_8)); + Files.writeString(Paths.get(folder.getAbsolutePath(), className + ".java"), + sb.toString()); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java index 1c913abe7f1..c5d44556514 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java @@ -86,29 +86,24 @@ public TestResult runTest(JunitXmlWriter xml) throws Exception { ForkMode forkMode = settings.getForkMode(); switch (forkMode) { - case PERGROUP: - testResults = ForkedTestFileRunner.processTestFiles(testFiles, getTempDir()); - break; - - case NOFORK: + case PERGROUP -> testResults = + ForkedTestFileRunner.processTestFiles(testFiles, getTempDir()); + case NOFORK -> { testResults = new ArrayList<>(); for (TestFile testFile : testFiles) { TestResult testResult = testFile.runKey(); testResults.add(testResult); } - break; - - case PERFILE: + } + case PERFILE -> { testResults = new ArrayList<>(); for (TestFile testFile : testFiles) { TestResult testResult = ForkedTestFileRunner.processTestFile(testFile, getTempDir()); testResults.add(testResult); } - break; - - default: - throw new RuntimeException("Unexpected value for fork mode: " + forkMode); + } + default -> throw new RuntimeException("Unexpected value for fork mode: " + forkMode); } if (verbose) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/CreateTacletForTests.java b/key.core/src/test/java/de/uka/ilkd/key/rule/CreateTacletForTests.java index 840bfad629b..3a9cc9ae76e 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/CreateTacletForTests.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/CreateTacletForTests.java @@ -244,7 +244,8 @@ public void setUp() throws IOException { String test1 = "\\predicates {A; B; } (A -> B) -> (!(!(A -> B)))"; Term t_test1 = null; try { - t_test1 = io.load(test1).loadDeclarations().loadProblem().getProblemTerm(); + t_test1 = io.load(test1).loadDeclarations().loadProblem().getProblem().succedent() + .get(0).formula(); } catch (Exception e) { LOGGER.error("Parser Error or Input Error", e); fail("Parser Error"); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java index 81fa4059cd2..6987844858d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java @@ -59,7 +59,8 @@ public class MasterHandlerTest { * If this variable is set when running this test class, then those cases with expected result * "weak_valid" will raise an exception unless they can be proved using the solver. *

- * Otherwise a "timeout" or "unknown" is accepted. This can be used to deal with test cases that + * Otherwise, a "timeout" or "unknown" is accepted. This can be used to deal with test cases + * that * should verify but do not yet do so. *

* (Default false) @@ -99,77 +100,67 @@ public static List data() } } catch (Exception e) { LOGGER.error("Error reading {}", file, e); + // make sure faulty test cases fail + throw e; } } return result; } - public static class TestData { - public final String name; - public final Path path; - private final String translation; - private final LineProperties props; - - public TestData(String name, Path path, LineProperties props, String translation) { - this.name = name; - this.path = path; - this.translation = translation; - this.props = props; - } - + public record TestData(String name, Path path, LineProperties props, String translation) { @Nullable - public static TestData create(Path path) throws IOException, ProblemLoaderException { - var name = path.getFileName().toString(); - var props = new LineProperties(); - try (BufferedReader reader = Files.newBufferedReader(path)) { - props.read(reader); - } + public static TestData create(Path path) throws IOException, ProblemLoaderException { + var name = path.getFileName().toString(); + var props = new LineProperties(); + try (BufferedReader reader = Files.newBufferedReader(path)) { + props.read(reader); + } - if ("ignore".equals(props.get("state"))) { - LOGGER.info("Test case has been marked ignore"); - return null; - } + if ("ignore".equals(props.get("state"))) { + LOGGER.info("Test case has been marked ignore"); + return null; + } - List sources = props.getLines("sources"); - List lines = new ArrayList<>(props.getLines("KeY")); + List sources = props.getLines("sources"); + List lines = new ArrayList<>(props.getLines("KeY")); - if (!sources.isEmpty()) { - Path srcDir = Files.createTempDirectory("SMT_key_" + name); - Path tmpSrc = srcDir.resolve("src.java"); - Files.write(tmpSrc, sources); - lines.add(0, "\\javaSource \"" + srcDir + "\";\n"); - } + if (!sources.isEmpty()) { + Path srcDir = Files.createTempDirectory("SMT_key_" + name); + Path tmpSrc = srcDir.resolve("src.java"); + Files.write(tmpSrc, sources); + lines.add(0, "\\javaSource \"" + srcDir + "\";\n"); + } - Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key"); - Files.write(tmpKey, lines); + Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key"); + Files.write(tmpKey, lines); - KeYEnvironment env = KeYEnvironment.load(tmpKey.toFile()); + KeYEnvironment env = KeYEnvironment.load(tmpKey.toFile()); - Proof proof = env.getLoadedProof(); - Sequent sequent = proof.root().sequent(); + Proof proof = env.getLoadedProof(); + Sequent sequent = proof.root().sequent(); - SMTSettings settings = new DefaultSMTSettings(proof.getSettings().getSMTSettings(), - ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(), - proof.getSettings().getNewSMTSettings(), proof); + SMTSettings settings = new DefaultSMTSettings(proof.getSettings().getSMTSettings(), + ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(), + proof.getSettings().getNewSMTSettings(), proof); - String updates = props.get("smt-settings"); - if (updates != null) { - Properties map = new Properties(); - map.load(new StringReader(updates)); - settings.getNewSettings().readSettings(map); - } + String updates = props.get("smt-settings"); + if (updates != null) { + Properties map = new Properties(); + map.load(new StringReader(updates)); + settings.getNewSettings().readSettings(map); + } - ModularSMTLib2Translator translator = new ModularSMTLib2Translator(); - var translation = - translator.translateProblem(sequent, env.getServices(), settings).toString(); - return new TestData(name, path, props, translation); - } + ModularSMTLib2Translator translator = new ModularSMTLib2Translator(); + var translation = + translator.translateProblem(sequent, env.getServices(), settings).toString(); + return new TestData(name, path, props, translation); + } - @Override - public String toString() { - return name; + @Override + public String toString() { + return name; + } } - } @ParameterizedTest @MethodSource("data") @@ -178,7 +169,7 @@ public void testTranslation(TestData data) throws Exception { Path tmpSmt = Files.createTempFile("SMT_key_" + data.name, ".smt2"); // FIXME This is beyond Java 8: add as soon as switched to Java 11: // Files.writeString(tmpSmt, translation); - Files.write(tmpSmt, data.translation.getBytes(StandardCharsets.UTF_8)); + Files.writeString(tmpSmt, data.translation); LOGGER.info("SMT2 for {} saved in: {}", data.name, tmpSmt); } @@ -223,16 +214,11 @@ public void testZ3(TestData data) throws Exception { try { String lookFor = null; switch (expectation) { - case "valid": - lookFor = "unsat"; - break; - case "fail": - lookFor = "(sat|timeout)"; - break; - case "irrelevant": - break; - default: - fail("Unexpected expectation: " + expectation); + case "valid" -> lookFor = "unsat"; + case "fail" -> lookFor = "(sat|timeout)"; + case "irrelevant" -> { + } + default -> fail("Unexpected expectation: " + expectation); } if (lookFor != null) { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/heap2.props b/key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/heap2.props new file mode 100644 index 00000000000..4f0e7c0184c --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/heap2.props @@ -0,0 +1,39 @@ +### Comment + +Related to issue #3267. + +### KeY + +\functions { int[][] n; long[] i_arr_2; int j_0; int a_0; int i_0; int start; } + +\problem { + (j_0 = a_0 & + a_0 >= 0 & + a_0 < n.length & + n[i_0][j_0] >= 0 & + i_arr_2[i_0] >= 1 & + i_0 < n.length & + i_0 >= 0 & + (\forall int i; + ( i < n.length & i >= 0 + -> \forall int j; (j < n.length & j >= 0 -> (n[i][j] = 0 <-> j = i))))) +-> + !(n[i_0][j_0] = -1 & + j_0 = i_0 & + (!n[i_0][a_0] = -1 + & ( !a_0 = start + -> i_arr_2[i_0] < i_arr_2[i_0] + n[i_0][j_0]) + & !i_arr_2[i_0] + n[i_0][j_0] = -1)) +} + +### contains.1 + +(declare-const sort_Field T) + +### contains.2 + +(declare-fun fieldIdentifier (U) Int) + +### expected + +valid \ No newline at end of file diff --git a/key.ui/build.gradle b/key.ui/build.gradle index d428bc07994..8ef828baee5 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -20,7 +20,7 @@ dependencies { implementation project(":key.core.symbolic_execution") implementation project(":key.removegenerics") - api 'com.miglayout:miglayout-swing:11.1' + api 'com.miglayout:miglayout-swing:11.2' //logging implementation used by the slf4j implementation 'ch.qos.logback:logback-classic:1.4.11' diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java index f96ad58769c..72bc9e54fd0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java @@ -805,9 +805,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { public void enableWhenProofLoaded(final Action a) { a.setEnabled(getSelectedProof() != null); addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { - } @Override public void selectedProofChanged(KeYSelectionEvent e) { @@ -824,9 +821,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { public void enableWhenProofLoaded(final javax.swing.AbstractButton a) { a.setEnabled(getSelectedProof() != null); addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { - } @Override public void selectedProofChanged(KeYSelectionEvent e) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java index bd2cc4cb37f..957bd2192ed 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java @@ -221,15 +221,15 @@ private void findNext() { nextOne = null; while (nextOne == null) { switch (currentPos) { - case POS_START: + case POS_START -> { currentPos = POS_LEAVES; if (selectedNode != null) { nodeIt = selectedNode.leavesIterator(); } else { nodeIt = null; } - break; - case POS_LEAVES: + } + case POS_LEAVES -> { if (nodeIt == null || !nodeIt.hasNext()) { currentPos = POS_GOAL_LIST; if (!proof.openGoals().isEmpty()) { @@ -240,16 +240,15 @@ private void findNext() { } else { nextOne = proof.getOpenGoal(nodeIt.next()); } - break; - - case POS_GOAL_LIST: + } + case POS_GOAL_LIST -> { if (goalIt == null || !goalIt.hasNext()) { // no more items return; } else { nextOne = goalIt.next(); } - break; + } } } } @@ -278,14 +277,10 @@ public void remove() { */ public void defaultSelection() { Goal g = null; - Goal firstG = null; Iterator it = new DefaultSelectionIterator(); while (g == null && it.hasNext()) { g = it.next(); - if (firstG == null) { - firstG = g; - } } /* @@ -295,11 +290,7 @@ public void defaultSelection() { if (g != null) { setSelectedGoal(g); } else { - if (firstG != null) { - setSelectedGoal(firstG); - } else { - setSelectedNode(proof.root().leavesIterator().next()); - } + setSelectedNode(proof.root().leavesIterator().next()); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java index d6a624842e3..c37783fb436 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java @@ -59,24 +59,12 @@ public static void configureLogging(@Nullable Integer verbosity) { var filter = new ThresholdFilter(); consoleAppender.addFilter(filter); switch (verbosity.byteValue()) { - case Verbosity.TRACE: - filter.setLevel("TRACE"); - break; - case Verbosity.DEBUG: - filter.setLevel("DEBUG"); - break; - case Verbosity.INFO: - filter.setLevel("INFO"); - break; - case Verbosity.NORMAL: - filter.setLevel("ERROR"); - break; - case Verbosity.SILENT: - filter.setLevel("OFF"); - break; - default: - filter.setLevel("WARN"); - break; + case Verbosity.TRACE -> filter.setLevel("TRACE"); + case Verbosity.DEBUG -> filter.setLevel("DEBUG"); + case Verbosity.INFO -> filter.setLevel("INFO"); + case Verbosity.NORMAL -> filter.setLevel("ERROR"); + case Verbosity.SILENT -> filter.setLevel("OFF"); + default -> filter.setLevel("WARN"); } filter.start(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java index b9fd8ba04ad..0439c08fd52 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java @@ -81,19 +81,13 @@ private static void run() { continue; } switch (thread.getState()) { - case NEW: - case RUNNABLE: - anyProgress = true; - break; - case WAITING: - case BLOCKED: - case TIMED_WAITING: - case TERMINATED: + case NEW, RUNNABLE -> anyProgress = true; + case WAITING, BLOCKED, TIMED_WAITING, TERMINATED -> { if (thread.getName().equals("AWT-EventQueue-0") && EventQueue.getCurrentEvent() == null) { anyProgress = true; // nothing to do } - break; + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java index 93971de9bbd..465e335ccaa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java @@ -8,10 +8,12 @@ import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; +import java.io.Serial; import java.util.ArrayList; import java.util.EventObject; import java.util.List; import java.util.WeakHashMap; +import javax.annotation.Nonnull; import javax.swing.*; import javax.swing.event.ListDataEvent; import javax.swing.event.ListDataListener; @@ -44,9 +46,8 @@ public class GoalList extends JList implements TabPanel { public static final Icon GOAL_LIST_ICON = IconFontSwing .buildIcon(FontAwesomeSolid.FLAG_CHECKERED, MainWindow.TAB_ICON_SIZE); - /** - * - */ + + @Serial private static final long serialVersionUID = 1632264315383703798L; private final static ImageIcon keyIcon = IconFactory.keyHole(20, 20); private final static Icon disabledGoalIcon = IconFactory.keyHoleInteractive(20, 20); @@ -110,6 +111,7 @@ public void mouseReleased(MouseEvent e) { KeYGuiExtension.KeyboardShortcuts.GOAL_LIST); } + @Nonnull @Override public String getTitle() { return "Goals"; @@ -120,6 +122,7 @@ public Icon getIcon() { return GOAL_LIST_ICON; } + @Nonnull @Override public JComponent getComponent() { return new JScrollPane(this); @@ -177,11 +180,6 @@ private void unregister() { } } - public void removeNotify() { // not used? - // unregister(); - // super.removeNotify(); - } - private KeYMediator mediator() { return mediator; } @@ -236,6 +234,7 @@ private String seqToString(Sequent seq) { } private static class GoalListModel extends AbstractListModel { + @Serial private static final long serialVersionUID = 3754243473284250930L; /** * listens to the proof @@ -282,7 +281,7 @@ public boolean isAttentive() { } /** - * Sets whether this object should respond to changes in the the proof immediately. + * Sets whether this object should respond to changes in the proof immediately. */ private void setAttentive(boolean b) { if ((b != attentive) && (proof != null) && !proof.isDisposed()) { @@ -332,6 +331,7 @@ public Goal getElementAt(int i) { class GoalListProofTreeListener implements ProofTreeListener, java.io.Serializable { + @Serial private static final long serialVersionUID = 3090011700136463120L; private boolean pruningInProcess; @@ -370,7 +370,7 @@ public void proofPruned(ProofTreeEvent e) { } /** - * invoked if the list of goals changed (goals were added, removed etc. + * invoked if the list of goals changed (goals were added, removed etc.) */ public void proofGoalRemoved(ProofTreeEvent e) { if (pruningInProcess) { @@ -408,9 +408,6 @@ public void proofStructureChanged(ProofTreeEvent e) { add(e.getSource().openGoals()); } - @Override - public void notesChanged(ProofTreeEvent e) { - } } } @@ -420,10 +417,7 @@ public void notesChanged(ProofTreeEvent e) { * @author Richard Bubel */ private final class DisableSingleGoal extends DisableGoal { - - /** - * - */ + @Serial private static final long serialVersionUID = -2035187175105625072L; DisableSingleGoal() { @@ -472,10 +466,7 @@ public void actionPerformed(ActionEvent e) { * @author Richard Bubel */ private final class DisableOtherGoals extends DisableGoal { - - /** - * - */ + @Serial private static final long serialVersionUID = 4077876260098617901L; DisableOtherGoals() { @@ -535,9 +526,8 @@ public void valueChanged(ListSelectionEvent e) { } private class GoalListGUIListener implements GUIListener, java.io.Serializable { - /** - * - */ + + @Serial private static final long serialVersionUID = -1826501525753975124L; /** @@ -607,10 +597,7 @@ public void autoModeStopped(ProofEvent e) { * used to prevent the display of goals that appear closed for the present user constraint. */ private class SelectingGoalListModel extends AbstractListModel { - - /** - * - */ + @Serial private static final long serialVersionUID = 7395134147866131926L; private final GoalListModel delegate; /** @@ -661,9 +648,8 @@ protected void setProof(Proof p) { private boolean isHiddenGoal(final Goal goal) { return proof != null - && /* - * that afterwards should always be false as goals exist only for open nodes - */goal.node().isClosed(); + && // that afterwards should always be false as goals exist only for open nodes + goal.node().isClosed(); } private void setup() { @@ -766,10 +752,9 @@ public void contentsChanged(ListDataEvent e) { updateDelegateSize(); - final int changeBegin = begin; final int changeEnd = end - 1; - if (changeEnd >= changeBegin) { - fireContentsChanged(this, changeBegin, changeEnd); + if (changeEnd >= begin) { + fireContentsChanged(this, begin, changeEnd); } } @@ -794,10 +779,9 @@ public void intervalRemoved(ListDataEvent e) { updateDelegateSize(); - final int remBegin = begin; final int remEnd = begin + (oldSize - entries.size()) - 1; - if (remEnd >= remBegin) { - fireIntervalRemoved(this, remBegin, remEnd); + if (remEnd >= begin) { + fireIntervalRemoved(this, begin, remEnd); } } } @@ -805,10 +789,7 @@ public void intervalRemoved(ListDataEvent e) { } private class IconCellRenderer extends DefaultListCellRenderer implements java.io.Serializable { - - /** - * - */ + @Serial private static final long serialVersionUID = -8178991338906184819L; public IconCellRenderer() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java index a10c18b86b0..2f24be1750a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java @@ -67,11 +67,6 @@ public Collection getPanels(@Nonnull MainWindow window, public void selectedNodeChanged(KeYSelectionEvent e) { panel.setGoal(mediator.getSelectedGoal()); } - - @Override - public void selectedProofChanged(KeYSelectionEvent e) { - - } }); /* @@ -192,7 +187,7 @@ private void applyRule(RuleApp ruleApp) { TacletApp tacletApp = (TacletApp) ruleApp; ImmutableSet seq = ImmutableSet.singleton(tacletApp); pc.selectedTaclet(seq, lastGoal); - } catch (ClassCastException e) { + } catch (ClassCastException ignored) { } } else { @@ -459,17 +454,16 @@ public void addPropertyChangeListener(String propertyName, PropertyChangeListene public void processChar(char c) { switch (c) { - case '\u001B': // escape + case '\u001B' -> // escape reset(); - break; - case '\b': + case '\b' -> { if (currentPrefix.length() <= 1) { setCurrentPrefix(""); } else { setCurrentPrefix(currentPrefix.substring(0, currentPrefix.length() - 1)); } - break; - default: + } + default -> { if ('0' <= c && c <= '9') { setCurrentPos(c - '0'); } @@ -477,6 +471,7 @@ public void processChar(char c) { setCurrentPrefix(currentPrefix + c); } } + } } public int getCurrentPos() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java index 1582d72d09c..b90981570f4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java @@ -95,8 +95,6 @@ public final class StrategySelectionView extends JPanel implements TabPanel { * Observe changes on {@link #mediator}. */ private final KeYSelectionListener mediatorListener = new KeYSelectionListener() { - public void selectedNodeChanged(KeYSelectionEvent e) { - } public void selectedProofChanged(KeYSelectionEvent e) { refresh(e.getSource().getSelectedProof()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index f4541f12a73..b14de3dc315 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.actions.ExitMainAction; import de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion; import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; @@ -51,6 +52,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import sun.misc.Signal; /** * Implementation of {@link UserInterfaceControl} which controls the {@link MainWindow} with the @@ -74,6 +76,19 @@ public WindowUserInterfaceControl(MainWindow mainWindow) { completions.add(new BlockContractInternalCompletion(mainWindow)); completions.add(new BlockContractExternalCompletion(mainWindow)); completions.add(MergeRuleCompletion.INSTANCE); + try { + Signal.handle(new Signal("INT"), sig -> { + if (getMediator().isInAutoMode()) { + LOGGER.warn("Caught SIGINT, stopping automode..."); + getMediator().getUI().getProofControl().stopAutoMode(); + } else { + LOGGER.warn("Caught SIGINT, exiting..."); + new ExitMainAction(mainWindow).exitMainWithoutInteraction(); + } + }); + } catch (Exception e) { + // the above is optional functionality and may not work on every OS + } } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index 5ca7a9175c2..e90f2a7267d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java @@ -11,7 +11,6 @@ import java.io.File; import java.io.IOException; import java.net.URI; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Paths; import java.util.Optional; @@ -240,7 +239,7 @@ private JPanel createButtonPanel(final URI sourceURI, final JTextPane textPane, // workaround for #1641: replace "\n" with system dependent line separators when // saving String text = textPane.getText().replace("\n", System.lineSeparator()); - Files.write(sourceFile.toPath(), text.getBytes(StandardCharsets.UTF_8)); + Files.writeString(sourceFile.toPath(), text); } catch (IOException ioe) { String message = "Cannot write to file:\n" + ioe.getMessage(); JOptionPane.showMessageDialog(parent, message); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java index 7678105608f..871225b47fa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java @@ -41,8 +41,6 @@ public SaveBundleAction(MainWindow mainWindow) { // react to changes of proof selection mainWindow.getMediator().addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) {} @Override public void selectedProofChanged(KeYSelectionEvent e) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java index f867c0a5a7d..6dae2505c25 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java @@ -117,15 +117,12 @@ public String getColumnName(int column) { @Override public Object getValueAt(int rowIndex, int columnIndex) { - switch (columnIndex) { - case 0: - return colorData.get(rowIndex).property.getKey(); - case 1: - return colorData.get(rowIndex).property.getDescription(); - case 2: - return colorData.get(rowIndex).color; - } - return ""; + return switch (columnIndex) { + case 0 -> colorData.get(rowIndex).property.getKey(); + case 1 -> colorData.get(rowIndex).property.getDescription(); + case 2 -> colorData.get(rowIndex).color; + default -> ""; + }; } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java index e7d1f7d4b55..1b709394453 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java @@ -26,9 +26,8 @@ * @version 1 (08.04.19) */ public class ExtensionManager extends SettingsPanel implements SettingsProvider { - private static final long serialVersionUID = 6682677093231975786L; private static final ExtensionSettings EXTENSION_SETTINGS = new ExtensionSettings(); - private HashMap map; + private HashMap> map; private String keywords = ""; public ExtensionManager() { @@ -91,7 +90,7 @@ private void refresh() { }); } - private String getSupportLabel(Extension it) { + private String getSupportLabel(Extension it) { return "Provides: " + (it.supportsContextMenu() ? "ContextMenu " : "") + (it.supportsLeftPanel() ? "LeftPanel " : "") + (it.supportsMainMenu() ? "MainMenu " : "") diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java index 84d4cbb6071..845879559c4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java @@ -5,6 +5,7 @@ import java.util.Collections; import java.util.List; +import javax.annotation.Nonnull; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; @@ -18,21 +19,17 @@ * @version 1 (16.04.19) */ public abstract class ContextMenuAdapter implements KeYGuiExtension.ContextMenu { + @Nonnull @Override - public final List getContextActions(KeYMediator mediator, ContextMenuKind kind, - Object underlyingObject) { - switch ((DefaultContextMenuKind) kind) { - case PROOF_LIST: - return getContextActions(mediator, kind, (Proof) underlyingObject); - case PROOF_TREE: - return getContextActions(mediator, kind, (Node) underlyingObject); - case TACLET_INFO: - return getContextActions(mediator, kind, (Rule) underlyingObject); - case SEQUENT_VIEW: - return getContextActions(mediator, kind, (PosInSequent) underlyingObject); - default: - throw new IllegalArgumentException("unexpected kind"); - } + public final List getContextActions(@Nonnull KeYMediator mediator, + @Nonnull ContextMenuKind kind, + @Nonnull Object underlyingObject) { + return switch ((DefaultContextMenuKind) kind) { + case PROOF_LIST -> getContextActions(mediator, kind, (Proof) underlyingObject); + case PROOF_TREE -> getContextActions(mediator, kind, (Node) underlyingObject); + case TACLET_INFO -> getContextActions(mediator, kind, (Rule) underlyingObject); + case SEQUENT_VIEW -> getContextActions(mediator, kind, (PosInSequent) underlyingObject); + }; } public List getContextActions(KeYMediator mediator, ContextMenuKind kind, diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java index b30186412f1..47227814fe8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java @@ -27,7 +27,7 @@ public PropertyEntry> forbiddenClasses() { } - public void setForbiddenClass(Class type, boolean activated) { + public void setForbiddenClass(Class type, boolean activated) { String text = type.getName(); Collection classes = getForbiddenClasses(); if (activated) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java index 55f500be85c..1dc26a2ab93 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java @@ -5,6 +5,7 @@ import java.awt.event.KeyAdapter; import java.awt.event.KeyEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.List; import java.util.Properties; @@ -24,6 +25,7 @@ * @version 1 (09.05.19) */ public class ShortcutSettings extends SimpleSettingsPanel implements SettingsProvider { + @Serial private static final long serialVersionUID = -7609149706562761596L; private final JTable tblShortcuts = new JTable(); private ShortcutsTableModel modelShortcuts; @@ -147,6 +149,7 @@ public void applySettings(MainWindow window) { } private static class ShortcutsTableModel extends AbstractTableModel { + @Serial private static final long serialVersionUID = -2854179933936417703L; private static final String[] COLUMNS = new String[] { "Name", "Description", "Shortcut" }; private final List actionName; @@ -178,20 +181,23 @@ public String getColumnName(int column) { @Override public Object getValueAt(int rowIndex, int columnIndex) { switch (columnIndex) { - case 0: + case 0 -> { return actionName.get(rowIndex) // remove common package prefixes .replaceAll("([a-z]\\w*\\.)*", ""); - case 1: + } + case 1 -> { Action a = actions.get(rowIndex); if (a == null) { return ""; } Object val = a.getValue(Action.SHORT_DESCRIPTION); return val != null ? val.toString() : ""; - case 2: + } + case 2 -> { return shortcut.get(rowIndex); } + } return ""; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java index 871a2ad2d3d..cf21eccce45 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java @@ -5,6 +5,7 @@ import java.awt.*; import java.awt.event.ActionEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.Collection; import java.util.Comparator; @@ -55,10 +56,11 @@ /** * The menu shown by a {@link CurrentGoalViewListener} when the user clicks on a * {@link CurrentGoalView}, i.e. when the user clicks on the sequent. - * + *

* Shows all {@link Taclet}s that are applicable at a selected position. */ public final class CurrentGoalViewMenu extends SequentViewMenu { + @Serial private static final long serialVersionUID = 8151230546928796116L; private static final String INTRODUCE_AXIOM_TACLET_NAME = "introduceAxiom"; @@ -537,23 +539,19 @@ public void actionPerformed(ActionEvent e) { PosInOccurrence occ = getPos().getPosInOccurrence(); switch (((JMenuItem) e.getSource()).getText()) { - case DISABLE_ABBREVIATION: + case DISABLE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { mediator.getNotationInfo().getAbbrevMap().setEnabled(occ.subTerm(), false); getSequentView().printSequent(); } - - break; - - case ENABLE_ABBREVIATION: + } + case ENABLE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { mediator.getNotationInfo().getAbbrevMap().setEnabled(occ.subTerm(), true); getSequentView().printSequent(); } - - break; - - case CREATE_ABBREVIATION: + } + case CREATE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { // trim string, otherwise window gets too large (bug #1430) final String oldTerm = occ.subTerm().toString(); @@ -580,10 +578,8 @@ public void actionPerformed(ActionEvent e) { JOptionPane.INFORMATION_MESSAGE); } } - - break; - - case CHANGE_ABBREVIATION: + } + case CHANGE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { String abbreviation = (String) JOptionPane.showInputDialog(new JFrame(), "Enter abbreviation for term: \n" + occ.subTerm().toString(), @@ -608,11 +604,8 @@ public void actionPerformed(ActionEvent e) { JOptionPane.INFORMATION_MESSAGE); } } - - break; - - default: - super.actionPerformed(e); + } + default -> super.actionPerformed(e); } } } @@ -621,9 +614,8 @@ public void actionPerformed(ActionEvent e) { static class FocussedRuleApplicationMenuItem extends JMenuItem { private static final String APPLY_RULES_AUTOMATICALLY_HERE = "Apply rules automatically here"; - /** - * - */ + + @Serial private static final long serialVersionUID = -6486650015103963268L; public FocussedRuleApplicationMenuItem() { @@ -732,7 +724,7 @@ public LinkedHashMap score(TacletApp o1) { final Taclet taclet1 = o1.taclet(); - map.put("closing", taclet1.goalTemplates().size() == 0 ? -1 : 1); + map.put("closing", taclet1.goalTemplates().isEmpty() ? -1 : 1); boolean calc = false; for (RuleSet rs : taclet1.getRuleSets()) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java index 9b0bc588f3c..0c406e6241f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.nodeviews; +import java.io.Serial; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -22,10 +23,7 @@ * easier access to the Taclet if the item has been selected */ class DefaultTacletMenuItem extends JMenuItem implements TacletMenuItem { - - /** - * - */ + @Serial private static final long serialVersionUID = -5537139155045230424L; private final TacletApp connectedTo; @@ -114,20 +112,11 @@ protected static StringBuilder ascii2html(String sb) { int sbl = asb.length(); for (int i = 0; i < sbl; i++) { switch (asb.charAt(i)) { - case '<': - nsb.append("<"); - break; - case '>': - nsb.append(">"); - break; - case '&': - nsb.append("&"); - break; - case '\n': - nsb.append("
"); - break; - default: - nsb.append(asb.charAt(i)); + case '<' -> nsb.append("<"); + case '>' -> nsb.append(">"); + case '&' -> nsb.append("&"); + case '\n' -> nsb.append("
"); + default -> nsb.append(asb.charAt(i)); } } return nsb; @@ -141,11 +130,6 @@ private static String removeEmptyLines(String string) { return string.replaceAll("(?m)^[ \t]*\r?\n|\n$", ""); } - /* - * (non-Javadoc) - * - * @see de.uka.ilkd.key.gui.TacletMenuItem#connectedTo() - */ @Override public TacletApp connectedTo() { return connectedTo; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java index aec9d295d2a..91149a652f7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java @@ -5,8 +5,10 @@ import java.awt.*; import java.awt.event.ItemEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.List; +import java.util.Objects; import java.util.regex.Matcher; import java.util.regex.Pattern; import javax.annotation.Nonnull; @@ -25,7 +27,7 @@ */ public class SequentViewSearchBar extends SearchBar { - + @Serial private static final long serialVersionUID = 9102464983776181771L; public static final ColorSettings.ColorProperty SEARCH_HIGHLIGHT_COLOR_1 = ColorSettings.define("[sequentSearchBar]highlight_1", "", new Color(0, 140, 255, 178)); @@ -100,24 +102,22 @@ public void createUI() { searchModeBox.addItemListener(e -> { if (e.getStateChange() == ItemEvent.SELECTED) { // search always does a repaint, therefore don't force update in setFilter - switch ((SearchMode) searchModeBox.getSelectedItem()) { - case HIDE: + switch ((SearchMode) Objects.requireNonNull(searchModeBox.getSelectedItem())) { + case HIDE -> { sequentView.setFilter(new HideSequentPrintFilter( sequentView.getLogicPrinter(), regExpCheckBox.isSelected()), false); search(); - break; - case REGROUP: + } + case REGROUP -> { sequentView.setFilter(new RegroupSequentPrintFilter( sequentView.getLogicPrinter(), regExpCheckBox.isSelected()), false); search(); - break; - case HIGHLIGHT: + } + case HIGHLIGHT -> { sequentView.setFilter(new IdentitySequentPrintFilter(), false); search(); - break; - default: - sequentView.setFilter(new IdentitySequentPrintFilter(), true); - break; + } + default -> sequentView.setFilter(new IdentitySequentPrintFilter(), true); } } }); @@ -178,7 +178,7 @@ public boolean search(@Nonnull String search) { sequentView.printSequent(); - if (sequentView == null || sequentView.getText() == null || search.equals("") + if (sequentView == null || sequentView.getText() == null || search.isEmpty() || !this.isVisible()) { return true; } @@ -198,17 +198,17 @@ public boolean search(@Nonnull String search) { return false; } - Matcher m = p.matcher(sequentView.getText().replace("\u00A0", "\u0020")); + Matcher m = p.matcher(sequentView.getText().replace("\u00A0", " ")); - boolean loopEnterd = false; + boolean loopEntered = false; while (m.find()) { int foundAt = m.start(); Object highlight = sequentView.getColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get()); searchResults.add(new Pair<>(foundAt, highlight)); sequentView.paintHighlight(new Range(foundAt, m.end()), highlight); - loopEnterd = true; + loopEntered = true; } - return loopEnterd; + return loopEntered; } /** @@ -219,7 +219,7 @@ public boolean search(@Nonnull String search) { public void searchFor(String searchTerm) { if (regExpCheckBox.isSelected()) { // https://stackoverflow.com/questions/60160/how-to-escape-text-for-regular-expression-in-java - String escaped = searchTerm.replaceAll("[-\\[\\]{}()*+?.,\\\\\\\\^$|#\\\\s]", "\\\\$0"); + String escaped = searchTerm.replaceAll("[-\\[\\]{}()*+?.,\\\\^$|#s]", "\\\\$0"); searchField.setText(escaped); } else { searchField.setText(searchTerm); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java index 27fc959e3f4..645a539f746 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java @@ -76,14 +76,11 @@ public int getColumnCount() { @Override public String getColumnName(int column) { - switch (column) { - case 0: - return "Goal"; - case 1: - return "Reference"; - default: - return "??"; - } + return switch (column) { + case 0 -> "Goal"; + case 1 -> "Reference"; + default -> "??"; + }; } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java index 21aacdbdfee..83b0971547e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java @@ -19,7 +19,7 @@ /** * Proof-of-concept implementation of a textual sequent comparison. - * + *

* This class provides a frame which allows the user to display a in-place comparison of two * sequents. The comparison happens on the pretty-printed text only, no sophisticated tree * comparison. The algorithm is taken from a google library. @@ -29,15 +29,10 @@ */ public class ProofDiffFrame extends JFrame { - - private static final long serialVersionUID = -1593379776744771923L; - /** * The action to show a new frame of this class. Is used in {@link MainWindow}. */ public static class Action extends MainWindowAction { - - private static final long serialVersionUID = -1745515272350810787L; private final MainWindow mainWindow; public Action(MainWindow mainWindow) { @@ -166,7 +161,7 @@ private void setSelectedNode() { /** * Initiate a diff calculation and set the content of the text area. - * + *

* It uses the result of {@link diff_match_patch#diff_main(String, String, boolean)} and html * markup to show the text. */ @@ -177,7 +172,7 @@ private void showDiff() { try { int toNo; String toText = to.getText(); - if (toText.length() == 0) { + if (toText.isEmpty()) { throw new IllegalArgumentException( "At least the second proof node must be specified"); } else { @@ -186,7 +181,7 @@ private void showDiff() { } String fromText = from.getText(); - if (fromText.length() == 0) { + if (fromText.isEmpty()) { sFrom = getProofNodeText(getParent(toNo)); } else { int fromNo = Integer.parseInt(fromText); @@ -209,25 +204,23 @@ private void showDiff() { sb.append("

");
         for (Diff diff : diffs) {
             switch (diff.operation) {
-            case EQUAL:
-                sb.append(toHtml(diff.text));
-                break;
-            case DELETE:
+            case EQUAL -> sb.append(toHtml(diff.text));
+            case DELETE -> {
                 if (onlySpaces(diff.text)) {
                     sb.append(diff.text);
                 } else {
                     sb.append("").append(toHtml(diff.text))
                             .append("");
                 }
-                break;
-            case INSERT:
+            }
+            case INSERT -> {
                 if (onlySpaces(diff.text)) {
                     sb.append(diff.text);
                 } else {
                     sb.append("").append(toHtml(diff.text))
                             .append("");
                 }
-                break;
+            }
             }
         }
         sb.append("
"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 13a8bb0d6eb..7ce51ee87d4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -214,7 +214,7 @@ private JButton getStopButton() { public void setModus(Modus m) { modus = m; switch (modus) { - case SOLVERS_DONE: + case SOLVERS_DONE -> { stopButton.setText("Discard"); if (applyButton != null) { applyButton.setEnabled(true); @@ -222,14 +222,13 @@ public void setModus(Modus m) { if (focusButton != null) { focusButton.setEnabled(true); } - break; - case SOLVERS_RUNNING: + } + case SOLVERS_RUNNING -> { stopButton.setText("Stop"); if (applyButton != null) { applyButton.setEnabled(false); } - break; - + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java index b2c81872507..7dc063f6bc3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java @@ -206,12 +206,14 @@ public void launcherStopped(SolverLauncher launcher, Collection probl private void applyResults() { KeYMediator mediator = MainWindow.getInstance().getMediator(); - // To ensure that the next goal is selected correctly, do not fully stop the interface here! - mediator.stopInterface(false); + // ensure that the goal closing does not lag the UI + mediator.stopInterface(true); try { new ProofSMTApplyUserAction(mediator, smtProof, problems).actionPerformed(null); } finally { - mediator.startInterface(false); + mediator.startInterface(true); + // switch to new open goal + mediator.getSelectionModel().defaultSelection(); } } @@ -377,19 +379,20 @@ private float calculateRemainingTime(InternSMTProblem problem) { private boolean refreshProgessOfProblem(InternSMTProblem problem) { SolverState state = problem.solver.getState(); - switch (state) { - case Running: - running(problem); - return true; - case Stopped: - stopped(problem); - return false; - case Waiting: - waiting(problem); - return true; - - } - return true; + return switch (state) { + case Running -> { + running(problem); + yield true; + } + case Stopped -> { + stopped(problem); + yield false; + } + case Waiting -> { + waiting(problem); + yield true; + } + }; } @@ -454,24 +457,17 @@ private void interrupted(InternSMTProblem problem) { int x = problem.getSolverIndex(); int y = problem.getProblemIndex(); switch (reason) { - case Exception: + case Exception -> { progressModel.setProgress(0, x, y); progressModel.setTextColor(RED.get(), x, y); progressModel.setText("Exception!", x, y); - - - break; - case NoInterruption: - throw new RuntimeException("This position should not be reachable!"); - - case Timeout: + } + case NoInterruption -> throw new RuntimeException("This position should not be reachable!"); + case Timeout -> { progressModel.setProgress(0, x, y); progressModel.setText("Timeout.", x, y); - - break; - case User: - progressModel.setText("Interrupted by user.", x, y); - break; + } + case User -> progressModel.setText("Interrupted by user.", x, y); } } @@ -578,11 +574,12 @@ private String finalizePath(String path, SMTSolver solver, Goal goal) { public static String computeSolverTypeWarningMessage(SolverType type) { - String message = "You are using a version of " + type.getName() - + " which has not been tested for this version of KeY.\nIt can therefore be that" - + " errors occur that would not occur\nusing the following version or higher:\n" + - type.getMinimumSupportedVersion(); - return message; + return (""" + You are using a version of %s which has not been tested for this version of KeY. + It can therefore be that errors occur that would not occur + using the following version or higher: + %s""") + .formatted(type.getName(), type.getMinimumSupportedVersion()); } private class ProgressDialogListenerImpl implements ProgressDialogListener { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java index 4b7abca4070..81dda805d8e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java @@ -7,7 +7,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; -import java.util.ResourceBundle; import javax.swing.*; import de.uka.ilkd.key.core.Main; @@ -28,22 +27,79 @@ * @version 1 (08.04.19) */ public class SMTSettingsProvider extends SettingsPanel implements SettingsProvider { - // de/uka/ilkd/key/gui/smt/settings/messages.xml - public static final ResourceBundle BUNDLE = - ResourceBundle.getBundle("de.uka.ilkd.key.gui.smt.settings.messages"); - - public static final String PROGRESS_MODE_USER = "PROGRESS_MODE_USER"; - public static final String PROGRESS_MODE_CLOSE = "PROGRESS_MODE_CLOSE"; - public static final String PROGRESS_MODE_CLOSE_FIRST = "PROGRESS_MODE_CLOSE_FIRST"; - private static final String INFO_BOUND = "infoBound"; - private static final String INFO_SAVE_TO_FILE_PANEL = "infoSaveToFilePanel"; - private static final String INFO_PROGRESS_MODE_BOX = "infoProgressModeBox"; - private static final String INFO_CHECK_FOR_SUPPORT = "infoCheckForSupport"; - private static final String INFO_MAX_PROCESSES = "infoMaxProcesses"; - private static final String INFO_TIMEOUT_FIELD = "infoTimeoutField"; + public static final String PROGRESS_MODE_USER = + "Progress dialog remains open after executing solvers"; + public static final String PROGRESS_MODE_CLOSE = + "Close progress dialog after all solvers have finished"; + public static final String PROGRESS_MODE_CLOSE_FIRST = + "Close progress dialog after the first solver has finished"; + public static final String INFO_BOUND = + "Bitvector size for this type. Use a value larger than 0."; + public static final String INFO_SAVE_TO_FILE_PANEL = + """ + Activate this option to store the translations that are handed over to the externals solvers: + 1. Choose the folder. + 2. Specify the filename: + %s: the solver's name + %d: date + %t: time + %i: the goal's number + Example: /home/translations/%d_%t_%i_%s.txt" + Remark: After every restart of KeY this option\ + is deactivated."""; - private final JTextField saveToFilePanel; + public static final String INFO_SOLVER_NAME = + """ + There are two ways to make supported provers applicable for KeY: + 1. Specify the absolute path of the prover in the field 'Command'. + 2. Change the environment variable $PATH of your system, so that it + refers to the installed prover. In that case you must specify the name of the solver in 'Command'"""; + public static final String INFO_PROGRESS_MODE_BOX = + """ + 1. Option: The progress dialog remains open after executing the solvers so that the user\ + can decide whether he wants to accept the results. + 2. Option: The progress dialog is closed once the external provers have done their work or the time limit\ + has been exceeded."""; + public static final String INFO_CHECK_FOR_SUPPORT = + """ + If this option is activated, each time before a solver is started\ + it is checked whether the version of that solver is supported. If the version is not supported, a warning is\ + presented in the progress dialog."""; + public static final String INFO_MAX_PROCESSES = + "Maximal number or processes that are allowed to run concurrently"; + public static final String INFO_TIMEOUT_FIELD = + """ + Timeout for the external solvers in seconds. Fractions of a second are allowed. Example: 6.5 + """; + public static final String INFO_SOLVER_COMMAND = """ + The command for the solver. + + Either you specify the absolute path of your solver or just the command for starting it. + In the latter case you have to modify the PATH-variable of your system. + Please note that you also have to specify the filename extension. + For example: z3.exe"""; + + public static final String INFO_SOLVER_PARAMETERS = + """ + In this field you can specify which parameters are passed to the \ + solver when the solver is started. Note that the default parameters are crucial for a stable run of the\ + solver."""; + + public static final String INFO_SOLVER_SUPPORT = + """ + For the KeY system only some particular versions of this solver + have been tested. It is highly recommended to use those versions, because otherwise it is not guaranteed that + the connection to this solver is stable. + If you want to check whether the installed solver is supported, please click on the button below."""; + public static final String SOLVER_SUPPORTED = "Version of solver is supported."; + public static final String SOLVER_MAY_SUPPORTED = "Version of solver may not be supported."; + public static final String SOLVER_UNSUPPORTED = "Support has not been checked, yet."; + public static final String INFO_SOLVER_TIMEOUT = + "Overrides timeout for this solver. Values in seconds. If value <= 0, global timeout is used."; + public static final String INFO_SOLVER_INFO = "Information about this solver."; + + private final JTextField saveToFilePanel; private final JComboBox progressModeBox; private final JSpinner maxProcesses; private final JSpinner timeoutField; @@ -121,12 +177,12 @@ public void applySettings(MainWindow window) { private JSpinner createLocSetBoundField() { return addNumberField("Locset bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setLocsetBound(e.longValue())); + INFO_BOUND, e -> settings.setLocsetBound(e.longValue())); } private JSpinner createMaxProcesses() { return addNumberField("Concurrent processes:", 0, Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_MAX_PROCESSES), + INFO_MAX_PROCESSES, e -> settings.setMaxConcurrentProcesses(e.intValue())); } @@ -134,7 +190,7 @@ private JSpinner createTimeoutField() { // Use doubles so that the formatter doesn't make every entered String into integers. // [see NumberFormatter#stringToValue()]. JSpinner timeoutSpinner = addNumberField("Timeout:", 0.0, (double) Long.MAX_VALUE, 1, - BUNDLE.getString(INFO_TIMEOUT_FIELD), + INFO_TIMEOUT_FIELD, e -> settings.setTimeout((long) Math.floor(e.doubleValue() * 1000))); // Set the editor so that entered Strings only have three decimal places. JSpinner.NumberEditor editor = new JSpinner.NumberEditor(timeoutSpinner, "#.###"); @@ -146,21 +202,21 @@ private JSpinner createTimeoutField() { private JSpinner createIntBoundField() { return addNumberField("Integer bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setIntBound(e.longValue())); + INFO_BOUND, e -> settings.setIntBound(e.longValue())); } private JSpinner createSeqBoundField() { return addNumberField("Seq bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setSeqBound(e.longValue())); + INFO_BOUND, e -> settings.setSeqBound(e.longValue())); } private JSpinner createObjectBoundField() { return addNumberField("Object bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setObjectBound(e.longValue())); + INFO_BOUND, e -> settings.setObjectBound(e.longValue())); } private JComboBox getProgressModeBox() { - return addComboBox("", BUNDLE.getString(INFO_PROGRESS_MODE_BOX), 0, + return addComboBox("", INFO_PROGRESS_MODE_BOX, 0, e -> settings.setModeOfProgressDialog( ProgressMode.values()[progressModeBox.getSelectedIndex()]), getProgressMode(ProgressMode.USER), getProgressMode(ProgressMode.CLOSE)); @@ -168,7 +224,7 @@ private JComboBox getProgressModeBox() { private JCheckBox createSolverSupportCheck() { return addCheckBox("Check for support when a solver is started", - BUNDLE.getString(INFO_CHECK_FOR_SUPPORT), false, + INFO_CHECK_FOR_SUPPORT, false, e -> settings.setCheckForSupport(solverSupportCheck.isSelected())); } @@ -180,20 +236,16 @@ private JCheckBox createEnableOnLoad() { private JTextField getSaveToFilePanel() { return addFileChooserPanel("Store translation to file:", "", - BUNDLE.getString(INFO_SAVE_TO_FILE_PANEL), true, + INFO_SAVE_TO_FILE_PANEL, true, e -> settings.setPathForSMTTranslation(saveToFilePanel.getText())); } private String getProgressMode(ProgressMode index) { - switch (index) { - case USER: - return BUNDLE.getString(PROGRESS_MODE_USER); - case CLOSE: - return BUNDLE.getString(PROGRESS_MODE_CLOSE); - case CLOSE_FIRST: - return BUNDLE.getString(PROGRESS_MODE_CLOSE_FIRST); - } - return ""; + return switch (index) { + case USER -> PROGRESS_MODE_USER; + case CLOSE -> PROGRESS_MODE_CLOSE; + case CLOSE_FIRST -> PROGRESS_MODE_CLOSE_FIRST; + }; } public void setSmtSettings(ProofIndependentSMTSettings settings) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java index e65252b3c60..baea011a54d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java @@ -13,22 +13,13 @@ import de.uka.ilkd.key.settings.ProofIndependentSMTSettings; import de.uka.ilkd.key.smt.solvertypes.SolverType; -import static de.uka.ilkd.key.gui.smt.settings.SMTSettingsProvider.BUNDLE; - /** * @author Alexander Weigl * @version 1 (08.04.19) */ class SolverOptions extends SettingsPanel implements SettingsProvider { - private static final String INFO_SOLVER_NAME = "infoSolverName"; - private static final String INFO_SOLVER_PARAMETERS = "infoSolverParameters"; - private static final String INFO_SOLVER_COMMAND = "infoSolverCommand"; - private static final String INFO_SOLVER_SUPPORT = "infoSolverSupport"; - private static final String INFO_SOLVER_INFO = "SOLVER_INFO"; - private static final String[] SOLVER_SUPPORT_TEXT = { BUNDLE.getString("SOLVER_SUPPORTED"), - BUNDLE.getString("SOLVER_MAY_SUPPORTED"), BUNDLE.getString("SOLVER_UNSUPPORTED") }; - private static final String INFO_SOLVER_TIMEOUT = "SOLVER_TIMEOUT"; - + private static final String[] SOLVER_SUPPORT_TEXT = { SMTSettingsProvider.SOLVER_SUPPORTED, + SMTSettingsProvider.SOLVER_MAY_SUPPORTED, SMTSettingsProvider.SOLVER_UNSUPPORTED }; private static final int SOLVER_SUPPORTED = 0; private static final int SOLVER_NOT_SUPPOTED = 1; @@ -58,12 +49,7 @@ public SolverOptions(SolverType solverType) { } private static String versionInfo(String info, String versionString) { - String builder = info + - " " + - "(" + - versionString + - ")"; - return builder; + return info + " " + "(" + versionString + ")"; } protected JButton createDefaultButton() { @@ -90,9 +76,9 @@ private String getSolverSupportText() { private JTextArea createSolverInformation() { String info = solverType.getInfo(); - if (info != null && !info.equals("")) { + if (info != null && !info.isEmpty()) { JTextArea solverInfo = - addTextAreaWithoutScroll("Info", info, BUNDLE.getString(INFO_SOLVER_INFO), null); + addTextAreaWithoutScroll("Info", info, SMTSettingsProvider.INFO_SOLVER_INFO, null); solverInfo.setLineWrap(true); solverInfo.setWrapStyleWord(true); solverInfo.setEditable(false); @@ -111,7 +97,8 @@ private JTextArea createSolverInformation() { protected JTextField createSolverSupported() { JTextField txt = addTextField("Support", getSolverSupportText(), - BUNDLE.getString(INFO_SOLVER_SUPPORT) + createSupportedVersionText(), emptyValidator()); + SMTSettingsProvider.INFO_SOLVER_SUPPORT + createSupportedVersionText(), + emptyValidator()); txt.setEditable(false); return txt; } @@ -126,7 +113,7 @@ private JSpinner createSolverTimeout() { // Use floor rounding to be consistent with the value that will be set for the timeout. editor.getFormat().setRoundingMode(RoundingMode.FLOOR); jsp.setEditor(editor); - addTitledComponent("Timeout", jsp, BUNDLE.getString(INFO_SOLVER_TIMEOUT)); + addTitledComponent("Timeout", jsp, SMTSettingsProvider.INFO_SOLVER_TIMEOUT); return jsp; } @@ -143,13 +130,13 @@ protected JButton createCheckSupportButton() { protected JTextField createSolverParameters() { return addTextField("Parameters", solverType.getSolverParameters(), - BUNDLE.getString(INFO_SOLVER_PARAMETERS), e -> { + SMTSettingsProvider.INFO_SOLVER_PARAMETERS, e -> { }); } public JTextField createSolverCommand() { return addTextField("Command", solverType.getSolverCommand(), - BUNDLE.getString(INFO_SOLVER_COMMAND), e -> { + SMTSettingsProvider.INFO_SOLVER_COMMAND, e -> { }); } @@ -178,7 +165,7 @@ protected JTextField createSolverInstalled() { protected JTextField createSolverName() { JTextField txt = addTextField("Name", solverType.getName(), - BUNDLE.getString(INFO_SOLVER_NAME), emptyValidator()); + SMTSettingsProvider.INFO_SOLVER_NAME, emptyValidator()); txt.setEditable(false); return txt; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index f8a45d9613c..2eb275be4c5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -5,6 +5,7 @@ import java.awt.Color; import java.beans.PropertyChangeListener; +import java.io.Serial; import java.util.*; import java.util.regex.Pattern; import javax.swing.text.*; @@ -16,15 +17,16 @@ /** * This document performs syntax highlighting when strings are inserted. However, only inserting the * whole String at once is supported, otherwise the syntax highlighting will be faulty. - * + *

* Note that tab characters have to be replaced by spaces before inserting into the document. - * + *

* The document currently only works when newlines are represented by "\n"! * * @author Wolfram Pfeifer */ public class JavaDocument extends DefaultStyledDocument { + @Serial private static final long serialVersionUID = -1856296532743892931L; // highlighting colors (same as in HTMLSyntaxHighlighter of SequentView for consistency) @@ -56,7 +58,7 @@ public class JavaDocument extends DefaultStyledDocument { * COMMENT (/* ... */), JML (/*@ ... */ ), ... */ private enum Mode { - /** parser is currently inside a String */ + /* parser is currently inside a String */ // STRING, // currently not in use /** parser is currently inside normal java code */ NORMAL, @@ -125,7 +127,7 @@ private enum CommentState { * Stores the Java keywords which have to be highlighted. The list is taken from * * https://docs.oracle.com/javase/tutorial/java/nutsandbolts/_keywords.html . - * + *

* To add additional keywords, simply add them to the array. Note that the keywords must not * contain any of the characters defined by the DELIM regex. */ @@ -140,7 +142,7 @@ private enum CommentState { /** * Stores the JML keywords which have to be highlighted. - * + *

* To add additional keywords, simply add them to the array. Note that the keywords must not * contain any of the characters defined by the DELIM regex. */ @@ -200,7 +202,7 @@ private enum CommentState { /** the style of annotations */ private final SimpleAttributeSet annotation = new SimpleAttributeSet(); - /** the style of strings */ + /* the style of strings */ // private SimpleAttributeSet string = new SimpleAttributeSet(); /** default style */ @@ -441,61 +443,26 @@ private void checkDelimiter(char c) { private void processChar(char strChar) throws BadLocationException { switch (strChar) { - case ('@'): - checkAt(); - break; - case '\n': - checkLinefeed(); - break; - case '\t': // all tabs should have been replaced earlier! - case ' ': - checkSpaceTab(strChar); - break; - case '*': - checkStar(); - break; - case '/': - checkSlash(); - break; - case '"': - checkQuote(); - break; + case ('@') -> checkAt(); + case '\n' -> checkLinefeed(); + // all tabs should have been replaced earlier! + case '\t', ' ' -> checkSpaceTab(strChar); + case '*' -> checkStar(); + case '/' -> checkSlash(); + case '"' -> checkQuote(); + // keyword delimiters: +-*/(){}[]%!^~.;?:&|<>="'\n(space) - case '+': - case '-': - checkPlusMinus(strChar); - break; + case '+', '-' -> checkPlusMinus(strChar); + // case '*': // case '/': - case '(': - case ')': - case '[': - case ']': - case '{': - case '}': - case '%': - case '!': - case '^': - case '~': - case '&': - case '|': - case '.': - case ':': - case ';': - case '?': - case '<': - case '>': - case '=': - case '\'': + case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', '>', '=', '\'' -> // case ' ': // case '"': // case '\'': // case '\n': checkDelimiter(strChar); - break; - default: - checkOther(strChar); - break; + default -> checkOther(strChar); } } diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties b/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties deleted file mode 100644 index f1dda118031..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties +++ /dev/null @@ -1,48 +0,0 @@ -PROGRESS_MODE_USER=Progress dialog remains open after executing solvers -PROGRESS_MODE_CLOSE=Close progress dialog after all solvers have finished -PROGRESS_MODE_CLOSE_FIRST=Close progress dialog after the first solver has finished -infoBound=Bitvector size for this type. Use a value larger than 0. -infoSaveToFilePanel=Activate this option to store the translations \ - that are handed over to the externals solvers: \n\ - 1. Choose the folder.\n\ - 2. Specify the filename:\n\ - \t%s: the solver's name\n\ - \t%d: date\n\ - \t%t: time\n\ - \t%i: the goal's number\n\ - \n\ - Example: /home/translations/%d_%t_%i_%s.txt"\n\ - \n\ - Remark: After every restart of KeY this option\ - is deactivated. -infoProgressModeBox=1. Option: The progress dialog remains open after executing the solvers so that the user\ - can decide whether he wants to accept the results.\n\ - \n\ - 2. Option: The progress dialog is closed once the external provers have done their work or the time limit\ - has been exceeded. -infoCheckForSupport=If this option is activated, each time before a solver is started\ - it is checked whether the version of that solver is supported. If the version is not supported, a warning is\ - presented in the progress dialog. -infoMaxProcesses=Maximal number or processes that are allowed to run concurrently -infoTimeoutField=Timeout for the external solvers in seconds. Fractions of a second are allowed. Example: 6.5 -infoSolverName=There are two ways to make supported provers applicable for KeY:\n\ - 1. Specify the absolute path of the prover in the field 'Command'.\n\ - 2. Change the environment variable $PATH of your system, so that it\n\ - refers to the installed prover. In that case you must specify the name of the solver in 'Command' -infoSolverParameters=In this field you can specify which parameters are passed to the \ - solver when the solver is started. Note that the default parameters are crucial for a stable run of the\ - solver. -infoSolverCommand=The command for the solver.\ - Either you specify the absolute path of your solver or just the command for starting it.\ - In the latter case you have to modify the PATH-variable of your system.\ - Please note that you also have to specify the filename extension.\n\ - For example: z3.exe -infoSolverSupport=For the KeY system only some particular versions of this solver \ - have been tested. It is highly recommended to use those versions, because otherwise it is not guaranteed that\ - the connection to this solver is stable.\ -If you want to check whether the installed solver is supported, please click on the button below. -SOLVER_SUPPORTED=Version of solver is supported. -SOLVER_MAY_SUPPORTED=Version of solver may not be supported. -SOLVER_UNSUPPORTED=Support has not been checked, yet. -SOLVER_TIMEOUT=Overrides timeout for this solver. Values in seconds. If value <= 0, global timeout is used. -SOLVER_INFO=Information about this solver. \ No newline at end of file diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java index afda9851da6..e46442f4f2e 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java @@ -43,8 +43,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { updateEnable(mainWindow); } - @Override - public void selectedNodeChanged(KeYSelectionEvent e) {} }); updateEnable(mainWindow); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index a850e742f56..6d445482155 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -385,8 +385,8 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en lastTouchedNode = lastGoal != null ? lastGoal.node() : proof.root(); } catch (Exception e) { - if (parserResult == null || parserResult.getErrors() == null - || parserResult.getErrors().isEmpty() || + if (parserResult == null || parserResult.errors() == null + || parserResult.errors().isEmpty() || replayer == null || replayResult == null || replayResult.getErrors() == null || replayResult.getErrors().isEmpty()) { // this exception was something unexpected @@ -395,8 +395,8 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en } finally { String status = ""; if (parserResult != null) { - status = parserResult.getStatus(); - errors.addAll(parserResult.getErrors()); + status = parserResult.status(); + errors.addAll(parserResult.errors()); } status += (status.isEmpty() ? "" : "\n\n") + (replayResult != null ? replayResult.getStatus() diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java index 46f448e727a..38931951162 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java @@ -52,7 +52,7 @@ public static DependencyGraph buildGraph(List proofEntri // get current node and root of proof Proof proof = line.proof; DependencyNode currentNode = graph.getNodeByName(proof.name().toString()); - BranchNodeIntermediate node = line.parseResult.getParsedResult(); + BranchNodeIntermediate node = line.parseResult.parsedResult(); // collect all contracts the current proof refers to Services services = proof.getServices(); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java index 4b1eedc1e27..171056afa64 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java @@ -6,7 +6,6 @@ import java.io.IOException; import java.lang.reflect.Method; import java.net.URL; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Path; import java.util.Map; @@ -56,7 +55,7 @@ public static void print(CheckerData data, Path target) throws IOException { data.print("Generating html report ..."); try { String output = st.render(); - Files.write(target, output.getBytes(StandardCharsets.UTF_8)); + Files.writeString(target, output); data.print("Report generated at " + target.normalize()); } catch (IOException e) { data.print("Unable to generate report: " + e.getMessage()); @@ -69,6 +68,7 @@ public static void print(CheckerData data, Path target) throws IOException { * @return the ST object for rendering the HTML report * @throws IOException if an error occurs accessing the StringTemplate resources */ + @SuppressWarnings("rawtypes") private static ST prepareStringTemplate() throws IOException { ClassLoader classLoader = HTMLReport.class.getClassLoader(); URL url = classLoader.getResource("report/html"); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java index dbda182e018..1c9837d03d3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java @@ -91,11 +91,6 @@ protected Void doInBackground() { return null; } - @Override - protected void done() { - - } - /** * @return the proof sliced by this worker */ diff --git a/recoder/build.gradle b/recoder/build.gradle index b2dec80b0e4..2c88419e168 100644 --- a/recoder/build.gradle +++ b/recoder/build.gradle @@ -3,7 +3,7 @@ description "Fork of the Recoder -- a parser/ast for Java with extensions for Ke def headerFile = "$rootDir/gradle/header-recoder" dependencies { - implementation 'org.ow2.asm:asm:9.5' + implementation 'org.ow2.asm:asm:9.6' implementation 'org.beanshell:bsh:2.0b5' implementation 'net.sf.retrotranslator:retrotranslator-runtime:1.2.9' implementation 'net.sf.retrotranslator:retrotranslator-transformer:1.2.9' diff --git a/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java b/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java index c120fbabcf7..a9e8e43a386 100644 --- a/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java +++ b/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java @@ -723,26 +723,17 @@ static int translateType(PrimitiveType t, NameInfo ni) { } static PrimitiveType translateType(int t, NameInfo ni) { - switch (t) { - case INT_TYPE: - return ni.getIntType(); - case BOOLEAN_TYPE: - return ni.getBooleanType(); - case LONG_TYPE: - return ni.getLongType(); - case FLOAT_TYPE: - return ni.getFloatType(); - case DOUBLE_TYPE: - return ni.getDoubleType(); - case BYTE_TYPE: - return ni.getByteType(); - case CHAR_TYPE: - return ni.getCharType(); - case SHORT_TYPE: - return ni.getShortType(); - default: - return null; - } + return switch (t) { + case INT_TYPE -> ni.getIntType(); + case BOOLEAN_TYPE -> ni.getBooleanType(); + case LONG_TYPE -> ni.getLongType(); + case FLOAT_TYPE -> ni.getFloatType(); + case DOUBLE_TYPE -> ni.getDoubleType(); + case BYTE_TYPE -> ni.getByteType(); + case CHAR_TYPE -> ni.getCharType(); + case SHORT_TYPE -> ni.getShortType(); + default -> null; + }; } /** @@ -750,94 +741,57 @@ static PrimitiveType translateType(int t, NameInfo ni) { */ static void promoteNumericTypeToInt(ConstantEvaluator.EvaluationResult res) { switch (res.getTypeCode()) { - case BYTE_TYPE: - res.setInt(res.getByte()); - break; - case CHAR_TYPE: - res.setInt(res.getChar()); - break; - case SHORT_TYPE: - res.setInt(res.getShort()); - break; + case BYTE_TYPE -> res.setInt(res.getByte()); + case CHAR_TYPE -> res.setInt(res.getChar()); + case SHORT_TYPE -> res.setInt(res.getShort()); } } /** * Asumes that both values are widened to at least int type. This is done by - * {@link #promoteNumericType}. Ensures that both values have equal types, or throws an + * {@link #promoteNumericTypeToInt(EvaluationResult)}. Ensures that both values have equal + * types, or throws an * exception if this is not possible given the set of allowed transformations. */ static void matchTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { switch (lhs.getTypeCode()) { - case INT_TYPE: + case INT_TYPE -> { switch (rhs.getTypeCode()) { - case LONG_TYPE: - lhs.setLong(lhs.getInt()); - break; - case FLOAT_TYPE: - lhs.setFloat(lhs.getInt()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getInt()); - break; + case LONG_TYPE -> lhs.setLong(lhs.getInt()); + case FLOAT_TYPE -> lhs.setFloat(lhs.getInt()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getInt()); } - break; - case LONG_TYPE: + } + case LONG_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setLong(rhs.getInt()); - break; - case FLOAT_TYPE: - lhs.setFloat(lhs.getLong()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getLong()); - break; + case INT_TYPE -> rhs.setLong(rhs.getInt()); + case FLOAT_TYPE -> lhs.setFloat(lhs.getLong()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getLong()); } - break; - case FLOAT_TYPE: + } + case FLOAT_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setFloat(rhs.getInt()); - break; - case LONG_TYPE: - rhs.setFloat(rhs.getLong()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getFloat()); - break; + case INT_TYPE -> rhs.setFloat(rhs.getInt()); + case LONG_TYPE -> rhs.setFloat(rhs.getLong()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getFloat()); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setDouble(rhs.getInt()); - break; - case LONG_TYPE: - rhs.setDouble(rhs.getLong()); - break; - case FLOAT_TYPE: - rhs.setDouble(rhs.getFloat()); - break; + case INT_TYPE -> rhs.setDouble(rhs.getInt()); + case LONG_TYPE -> rhs.setDouble(rhs.getLong()); + case FLOAT_TYPE -> rhs.setDouble(rhs.getFloat()); } - break; - case STRING_TYPE: + } + case STRING_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setString(String.valueOf(rhs.getInt())); - break; - case LONG_TYPE: - rhs.setString(String.valueOf(rhs.getLong())); - break; - case FLOAT_TYPE: - rhs.setString(String.valueOf(rhs.getFloat())); - break; - case DOUBLE_TYPE: - rhs.setString(String.valueOf(rhs.getDouble())); - break; + case INT_TYPE -> rhs.setString(String.valueOf(rhs.getInt())); + case LONG_TYPE -> rhs.setString(String.valueOf(rhs.getLong())); + case FLOAT_TYPE -> rhs.setString(String.valueOf(rhs.getFloat())); + case DOUBLE_TYPE -> rhs.setString(String.valueOf(rhs.getDouble())); } - break; + } } // if the rules above did not produce equal types, // something is wrong, e.g. boolean + non-boolean, @@ -857,9 +811,9 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { int value; switch (lhs.getTypeCode()) { - case INT_TYPE: + case INT_TYPE -> { switch (rhs.getTypeCode()) { - case BYTE_TYPE: + case BYTE_TYPE -> { value = lhs.getInt(); if (Byte.MIN_VALUE <= value && value <= Byte.MAX_VALUE) { lhs.setByte((byte) value); @@ -867,7 +821,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, rhs.setInt(rhs.getByte()); } return; - case CHAR_TYPE: + } + case CHAR_TYPE -> { value = lhs.getInt(); if (Character.MIN_VALUE <= value && value <= Character.MAX_VALUE) { lhs.setChar((char) value); @@ -875,7 +830,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, rhs.setInt(rhs.getChar()); } return; - case SHORT_TYPE: + } + case SHORT_TYPE -> { value = lhs.getInt(); if (Short.MIN_VALUE <= value && value <= Short.MAX_VALUE) { lhs.setShort((short) value); @@ -884,8 +840,9 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case BYTE_TYPE: + } + } + case BYTE_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Byte.MIN_VALUE <= value && value <= Byte.MAX_VALUE) { @@ -895,8 +852,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case SHORT_TYPE: + } + case SHORT_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Short.MIN_VALUE <= value && value <= Short.MAX_VALUE) { @@ -906,8 +863,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case CHAR_TYPE: + } + case CHAR_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Character.MIN_VALUE <= value && value <= Character.MAX_VALUE) { @@ -917,7 +874,7 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; + } } matchTypes(lhs, rhs); } @@ -930,37 +887,41 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, static void matchConditionalTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { switch (lhs.getTypeCode()) { - case BYTE_TYPE: + case BYTE_TYPE -> { switch (rhs.getTypeCode()) { - case SHORT_TYPE: // byte x short -> short x short + case SHORT_TYPE -> { // byte x short -> short x short lhs.setShort(lhs.getByte()); return; - case CHAR_TYPE: // byte x char -> int x int + } + case CHAR_TYPE -> { // byte x char -> int x int promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; - case CHAR_TYPE: - switch (rhs.getTypeCode()) { - case BYTE_TYPE: // char x byte, char x short -> int x int - case SHORT_TYPE: + } + } + case CHAR_TYPE -> { + switch (rhs.getTypeCode()) { // char x byte, char x short -> int x int + case BYTE_TYPE, SHORT_TYPE -> { promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; - case SHORT_TYPE: + } + } + case SHORT_TYPE -> { switch (rhs.getTypeCode()) { - case BYTE_TYPE: // short x byte -> short x short + case BYTE_TYPE -> { // short x byte -> short x short rhs.setShort(rhs.getByte()); return; - case CHAR_TYPE: // short x char -> int x int + } + case CHAR_TYPE -> { // short x char -> int x int promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; + } + } } matchAssignmentTypes(lhs, rhs); } @@ -975,31 +936,15 @@ static String parseJavaString(String text) { } else { i += 1; switch (text.charAt(i)) { - case 'b': - buf.append('\b'); - break; - case 't': - buf.append('\t'); - break; - case 'n': - buf.append('\n'); - break; - case 'f': - buf.append('\f'); - break; - case 'r': - buf.append('\r'); - break; - case '\"': - buf.append('\"'); - break; - case '\'': - buf.append('\''); - break; - case '\\': - buf.append('\\'); - break; - case 'u': + case 'b' -> buf.append('\b'); + case 't' -> buf.append('\t'); + case 'n' -> buf.append('\n'); + case 'f' -> buf.append('\f'); + case 'r' -> buf.append('\r'); + case '\"' -> buf.append('\"'); + case '\'' -> buf.append('\''); + case '\\' -> buf.append('\\'); + case 'u' -> { // skip an arbitrary number of u's i += 1; while (text.charAt(i) == 'u') { @@ -1008,24 +953,16 @@ static String parseJavaString(String text) { // the following must be a 4-digit hex value buf.append((char) Integer.parseInt(text.substring(i, i + 4), 16)); i += 4; - break; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': + } + case '0', '1', '2', '3', '4', '5', '6', '7' -> { int j = i + 1; while (j < len && text.charAt(j) >= '0' && text.charAt(j) <= '7') { j += 1; } buf.append((char) Integer.parseInt(text.substring(i, j), 8)); i = j; - break; - default: - throw new ModelException("Bad character representation: " + text); + } + default -> throw new ModelException("Bad character representation: " + text); } } } @@ -1041,160 +978,76 @@ static void doPrimitiveTypeCast(int newType, ConstantEvaluator.EvaluationResult throw new ModelException("Cast not allowed"); } switch (oldType) { - case BYTE_TYPE: + case BYTE_TYPE -> { switch (newType) { - case SHORT_TYPE: - res.setShort(res.getByte()); - return; - case CHAR_TYPE: - res.setChar((char) res.getByte()); - return; - case INT_TYPE: - res.setInt(res.getByte()); - return; - case LONG_TYPE: - res.setLong(res.getByte()); - return; - case FLOAT_TYPE: - res.setFloat(res.getByte()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getByte()); - return; + case SHORT_TYPE -> res.setShort(res.getByte()); + case CHAR_TYPE -> res.setChar((char) res.getByte()); + case INT_TYPE -> res.setInt(res.getByte()); + case LONG_TYPE -> res.setLong(res.getByte()); + case FLOAT_TYPE -> res.setFloat(res.getByte()); + case DOUBLE_TYPE -> res.setDouble(res.getByte()); } - break; - case SHORT_TYPE: + } + case SHORT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getShort()); - return; - case CHAR_TYPE: - res.setChar((char) res.getShort()); - return; - case INT_TYPE: - res.setInt(res.getShort()); - return; - case LONG_TYPE: - res.setLong(res.getShort()); - return; - case FLOAT_TYPE: - res.setFloat(res.getShort()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getShort()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getShort()); + case CHAR_TYPE -> res.setChar((char) res.getShort()); + case INT_TYPE -> res.setInt(res.getShort()); + case LONG_TYPE -> res.setLong(res.getShort()); + case FLOAT_TYPE -> res.setFloat(res.getShort()); + case DOUBLE_TYPE -> res.setDouble(res.getShort()); } - break; - case CHAR_TYPE: + } + case CHAR_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getChar()); - return; - case SHORT_TYPE: - res.setShort((short) res.getChar()); - return; - case INT_TYPE: - res.setInt(res.getChar()); - return; - case LONG_TYPE: - res.setLong(res.getChar()); - return; - case FLOAT_TYPE: - res.setFloat(res.getChar()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getChar()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getChar()); + case SHORT_TYPE -> res.setShort((short) res.getChar()); + case INT_TYPE -> res.setInt(res.getChar()); + case LONG_TYPE -> res.setLong(res.getChar()); + case FLOAT_TYPE -> res.setFloat(res.getChar()); + case DOUBLE_TYPE -> res.setDouble(res.getChar()); } - break; - case INT_TYPE: + } + case INT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getInt()); - return; - case SHORT_TYPE: - res.setShort((short) res.getInt()); - return; - case CHAR_TYPE: - res.setChar((char) res.getInt()); - return; - case LONG_TYPE: - res.setLong(res.getInt()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getInt()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getInt()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getInt()); + case SHORT_TYPE -> res.setShort((short) res.getInt()); + case CHAR_TYPE -> res.setChar((char) res.getInt()); + case LONG_TYPE -> res.setLong(res.getInt()); + case FLOAT_TYPE -> res.setFloat((float) res.getInt()); + case DOUBLE_TYPE -> res.setDouble(res.getInt()); } - break; - case LONG_TYPE: + } + case LONG_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getLong()); - return; - case SHORT_TYPE: - res.setShort((short) res.getLong()); - return; - case CHAR_TYPE: - res.setChar((char) res.getLong()); - return; - case INT_TYPE: - res.setInt((int) res.getLong()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getLong()); - return; - case DOUBLE_TYPE: - res.setDouble((double) res.getLong()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getLong()); + case SHORT_TYPE -> res.setShort((short) res.getLong()); + case CHAR_TYPE -> res.setChar((char) res.getLong()); + case INT_TYPE -> res.setInt((int) res.getLong()); + case FLOAT_TYPE -> res.setFloat((float) res.getLong()); + case DOUBLE_TYPE -> res.setDouble((double) res.getLong()); } - break; - case FLOAT_TYPE: + } + case FLOAT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getFloat()); - return; - case SHORT_TYPE: - res.setShort((short) res.getFloat()); - return; - case CHAR_TYPE: - res.setChar((char) res.getFloat()); - return; - case INT_TYPE: - res.setInt((int) res.getFloat()); - return; - case LONG_TYPE: - res.setLong((long) res.getFloat()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getFloat()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getFloat()); + case SHORT_TYPE -> res.setShort((short) res.getFloat()); + case CHAR_TYPE -> res.setChar((char) res.getFloat()); + case INT_TYPE -> res.setInt((int) res.getFloat()); + case LONG_TYPE -> res.setLong((long) res.getFloat()); + case DOUBLE_TYPE -> res.setDouble(res.getFloat()); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getDouble()); - return; - case SHORT_TYPE: - res.setShort((short) res.getDouble()); - return; - case CHAR_TYPE: - res.setChar((char) res.getDouble()); - return; - case INT_TYPE: - res.setInt((int) res.getDouble()); - return; - case LONG_TYPE: - res.setLong((long) res.getDouble()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getDouble()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getDouble()); + case SHORT_TYPE -> res.setShort((short) res.getDouble()); + case CHAR_TYPE -> res.setChar((char) res.getDouble()); + case INT_TYPE -> res.setInt((int) res.getDouble()); + case LONG_TYPE -> res.setLong((long) res.getDouble()); + case FLOAT_TYPE -> res.setFloat((float) res.getDouble()); } - break; + } } } @@ -1327,12 +1180,11 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati BinaryBooleanOperation bbo = null; switch (op.getArity()) { - case 1: // unary operations + case 1 -> { // unary operations if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; } - if (op instanceof Positive) { uno = POSITIVE; } else if (op instanceof Negative) { @@ -1342,8 +1194,8 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati } else if (op instanceof LogicalNot) { ubo = LOGICAL_NOT; } - break; - case 2: // binary operations + } + case 2 -> { // binary operations if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; } @@ -1355,7 +1207,7 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati * would be stored locally and res would be reused for the rhs call. However, * performance is not critical here. */ - rhs = new ConstantEvaluator.EvaluationResult(); + rhs = new EvaluationResult(); // evaluate right-hand side; finish if not constant if (!isCompileTimeConstant(op.getExpressionAt(1), rhs)) { return false; @@ -1365,7 +1217,6 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati // widen the remaining types to match both argument types matchTypes(lhs, rhs); - if (op instanceof ComparativeOperator) { if (op instanceof Equals) { bbo = EQUALS; @@ -1411,8 +1262,8 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati } else if (op instanceof LogicalOr) { bbo = LOGICAL_OR; } - break; - case 3: + } + case 3 -> { // this must be the conditional (?:) if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; @@ -1427,136 +1278,70 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati if (!isCompileTimeConstant(op.getExpressionAt(1), lhs)) { return false; } - rhs = new ConstantEvaluator.EvaluationResult(); + rhs = new EvaluationResult(); if (!isCompileTimeConstant(op.getExpressionAt(2), rhs)) { return false; } matchConditionalTypes(lhs, rhs); - switch (lhs.getTypeCode()) { // matches type of rhs - case BOOLEAN_TYPE: - res.setBoolean(cond ? lhs.getBoolean() : rhs.getBoolean()); - break; - case BYTE_TYPE: - res.setByte(cond ? lhs.getByte() : rhs.getByte()); - break; - case SHORT_TYPE: - res.setShort(cond ? lhs.getShort() : rhs.getShort()); - break; - case CHAR_TYPE: - res.setChar(cond ? lhs.getChar() : rhs.getChar()); - break; - case INT_TYPE: - res.setInt(cond ? lhs.getInt() : rhs.getInt()); - break; - case LONG_TYPE: - res.setLong(cond ? lhs.getLong() : rhs.getLong()); - break; - case FLOAT_TYPE: - res.setFloat(cond ? lhs.getFloat() : rhs.getFloat()); - break; - case DOUBLE_TYPE: - res.setDouble(cond ? lhs.getDouble() : rhs.getDouble()); - break; - case STRING_TYPE: - res.setString(cond ? lhs.getString() : rhs.getString()); - break; + case BOOLEAN_TYPE -> res.setBoolean(cond ? lhs.getBoolean() : rhs.getBoolean()); + case BYTE_TYPE -> res.setByte(cond ? lhs.getByte() : rhs.getByte()); + case SHORT_TYPE -> res.setShort(cond ? lhs.getShort() : rhs.getShort()); + case CHAR_TYPE -> res.setChar(cond ? lhs.getChar() : rhs.getChar()); + case INT_TYPE -> res.setInt(cond ? lhs.getInt() : rhs.getInt()); + case LONG_TYPE -> res.setLong(cond ? lhs.getLong() : rhs.getLong()); + case FLOAT_TYPE -> res.setFloat(cond ? lhs.getFloat() : rhs.getFloat()); + case DOUBLE_TYPE -> res.setDouble(cond ? lhs.getDouble() : rhs.getDouble()); + case STRING_TYPE -> res.setString(cond ? lhs.getString() : rhs.getString()); } return true; } + } if (bno != null) { switch (lhs.getTypeCode()) { - case BOOLEAN_TYPE: - lhs.setBoolean(bno.eval(lhs.getBoolean(), rhs.getBoolean())); - break; - case INT_TYPE: - lhs.setInt(bno.eval(lhs.getInt(), rhs.getInt())); - break; - case LONG_TYPE: - lhs.setLong(bno.eval(lhs.getLong(), rhs.getLong())); - break; - case FLOAT_TYPE: - lhs.setFloat(bno.eval(lhs.getFloat(), rhs.getFloat())); - break; - case DOUBLE_TYPE: - lhs.setDouble(bno.eval(lhs.getDouble(), rhs.getDouble())); - break; - case STRING_TYPE: - lhs.setString(bno.eval(lhs.getString(), rhs.getString())); - break; + case BOOLEAN_TYPE -> lhs.setBoolean(bno.eval(lhs.getBoolean(), rhs.getBoolean())); + case INT_TYPE -> lhs.setInt(bno.eval(lhs.getInt(), rhs.getInt())); + case LONG_TYPE -> lhs.setLong(bno.eval(lhs.getLong(), rhs.getLong())); + case FLOAT_TYPE -> lhs.setFloat(bno.eval(lhs.getFloat(), rhs.getFloat())); + case DOUBLE_TYPE -> lhs.setDouble(bno.eval(lhs.getDouble(), rhs.getDouble())); + case STRING_TYPE -> lhs.setString(bno.eval(lhs.getString(), rhs.getString())); } return true; } if (bbo != null) { switch (lhs.getTypeCode()) { - case BOOLEAN_TYPE: - lhs.setBoolean(bbo.eval(lhs.getBoolean(), rhs.getBoolean())); - break; - case INT_TYPE: - lhs.setBoolean(bbo.eval(lhs.getInt(), rhs.getInt())); - break; - case LONG_TYPE: - lhs.setBoolean(bbo.eval(lhs.getLong(), rhs.getLong())); - break; - case FLOAT_TYPE: - lhs.setBoolean(bbo.eval(lhs.getFloat(), rhs.getFloat())); - break; - case DOUBLE_TYPE: - lhs.setBoolean(bbo.eval(lhs.getDouble(), rhs.getDouble())); - break; - case STRING_TYPE: - lhs.setBoolean(bbo.eval(lhs.getString(), rhs.getString())); - break; + case BOOLEAN_TYPE -> lhs.setBoolean(bbo.eval(lhs.getBoolean(), rhs.getBoolean())); + case INT_TYPE -> lhs.setBoolean(bbo.eval(lhs.getInt(), rhs.getInt())); + case LONG_TYPE -> lhs.setBoolean(bbo.eval(lhs.getLong(), rhs.getLong())); + case FLOAT_TYPE -> lhs.setBoolean(bbo.eval(lhs.getFloat(), rhs.getFloat())); + case DOUBLE_TYPE -> lhs.setBoolean(bbo.eval(lhs.getDouble(), rhs.getDouble())); + case STRING_TYPE -> lhs.setBoolean(bbo.eval(lhs.getString(), rhs.getString())); } return true; } if (uno != null) { switch (res.getTypeCode()) { - case BOOLEAN_TYPE: - res.setBoolean(uno.eval(res.getBoolean())); - break; - case INT_TYPE: - res.setInt(uno.eval(res.getInt())); - break; - case LONG_TYPE: - res.setLong(uno.eval(res.getLong())); - break; - case FLOAT_TYPE: - res.setFloat(uno.eval(res.getFloat())); - break; - case DOUBLE_TYPE: - res.setDouble(uno.eval(res.getDouble())); - break; - case STRING_TYPE: - res.setString(uno.eval(res.getString())); - break; + case BOOLEAN_TYPE -> res.setBoolean(uno.eval(res.getBoolean())); + case INT_TYPE -> res.setInt(uno.eval(res.getInt())); + case LONG_TYPE -> res.setLong(uno.eval(res.getLong())); + case FLOAT_TYPE -> res.setFloat(uno.eval(res.getFloat())); + case DOUBLE_TYPE -> res.setDouble(uno.eval(res.getDouble())); + case STRING_TYPE -> res.setString(uno.eval(res.getString())); } return true; } if (ubo != null) { switch (res.getTypeCode()) { - case BOOLEAN_TYPE: - res.setBoolean(ubo.eval(res.getBoolean())); - break; - case INT_TYPE: - res.setBoolean(ubo.eval(res.getInt())); - break; - case LONG_TYPE: - res.setBoolean(ubo.eval(res.getLong())); - break; - case FLOAT_TYPE: - res.setBoolean(ubo.eval(res.getFloat())); - break; - case DOUBLE_TYPE: - res.setBoolean(ubo.eval(res.getDouble())); - break; - case STRING_TYPE: - res.setBoolean(ubo.eval(res.getString())); - break; + case BOOLEAN_TYPE -> res.setBoolean(ubo.eval(res.getBoolean())); + case INT_TYPE -> res.setBoolean(ubo.eval(res.getInt())); + case LONG_TYPE -> res.setBoolean(ubo.eval(res.getLong())); + case FLOAT_TYPE -> res.setBoolean(ubo.eval(res.getFloat())); + case DOUBLE_TYPE -> res.setBoolean(ubo.eval(res.getDouble())); + case STRING_TYPE -> res.setBoolean(ubo.eval(res.getString())); } return true; } @@ -1627,43 +1412,29 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati return false; } switch (vtype) { - case BOOLEAN_TYPE: - res.setBoolean(Integer.parseInt(val) != 0); - break; - case BYTE_TYPE: - res.setByte((byte) Integer.parseInt(val)); - break; - case SHORT_TYPE: - res.setShort((short) Integer.parseInt(val)); - break; - case CHAR_TYPE: - res.setChar((char) Integer.parseInt(val)); - break; - case INT_TYPE: - res.setInt(Integer.parseInt(val)); - break; - case LONG_TYPE: - res.setLong(Long.parseLong(val)); - break; - case FLOAT_TYPE: + case BOOLEAN_TYPE -> res.setBoolean(Integer.parseInt(val) != 0); + case BYTE_TYPE -> res.setByte((byte) Integer.parseInt(val)); + case SHORT_TYPE -> res.setShort((short) Integer.parseInt(val)); + case CHAR_TYPE -> res.setChar((char) Integer.parseInt(val)); + case INT_TYPE -> res.setInt(Integer.parseInt(val)); + case LONG_TYPE -> res.setLong(Long.parseLong(val)); + case FLOAT_TYPE -> { if (val.equals("NaN")) { // may occur in byte code?! res.setFloat(Float.NaN); } else { res.setFloat(Float.valueOf(val)); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { if (val.equals("NaN")) { // may occur in byte code?! res.setDouble(Double.NaN); } else { res.setDouble(Double.valueOf(val)); } - break; - case STRING_TYPE: - res.setString(val); - break; + } + case STRING_TYPE -> res.setString(val); } return true; } diff --git a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java index 9814b29c124..cd48ec0e173 100644 --- a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java @@ -31,23 +31,16 @@ protected DefaultProgramModelInfo(ServiceConfiguration config) { super(config); } - // TODO move to where it belongs ?! - private static void removeRange(List list, int from) { - for (int i = list.size() - 1; i >= from; i--) { - list.remove(i); + private static void removeRange(List list, int from) { + if (list.size() > from) { + list.subList(from, list.size()).clear(); } } - // TODO move to where it belongs ?! - private static void removeRange(List list, int from, int to) { - // TODO improve speed! - if (from > to) { - to ^= from ^= to ^= from; - } - int cnt = to - from; - while (cnt-- > 0) { - list.remove(from); - } + private static void removeRange(List list, int from, int to) { + int start = Math.min(from, to); + int end = Math.max(from, to); + list.subList(start, end).clear(); } final ChangeHistory getChangeHistory() { @@ -118,9 +111,7 @@ public List getSubtypes(ClassType ct) { } int s = ctce.subtypes.size(); List result = new ArrayList<>(s); - for (ClassType subct : ctce.subtypes) { - result.add(subct); - } + result.addAll(ctce.subtypes); return result; } @@ -184,13 +175,12 @@ private void computeAllFields(ClassType ct, ClassTypeCacheEntry ctce) { if (fl == null) { continue; } - int fs = fl.size(); add_fields: for (Field f : fl) { if (isVisibleFor(f, ct)) { String fname = f.getName(); for (int k = 0; k < result_size; k++) { Field rf = result.get(k); - if (rf.getName() == fname) { + if (Objects.equals(rf.getName(), fname)) { continue add_fields; } } @@ -234,7 +224,6 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { if (ml == null) { continue; } - int ms = ml.size(); add_methods: for (Method m : ml) { // if (m.isPublic() || m.isProtected() || c == ct || // (!m.isPrivate() && c.getPackage() == ct.getPackage())) { @@ -264,7 +253,7 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { String mname = m.getName(); for (int k = 0; k < result_size; k++) { Method rm = result.get(k); - if (rm.getName() == mname) { + if (Objects.equals(rm.getName(), mname)) { List rsig = rm.getSignature(); if (rsig.equals(msig)) { // skip this method: we already had it @@ -282,18 +271,11 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { } private Type makeParameterizedType(TypeArgument ta) { - Type bt = null; - switch (ta.getWildcardMode()) { - case Super: - case Any: - bt = getNameInfo().getJavaLangObject(); - break; - case None: - case Extends: - bt = getBaseType(ta); - break; - } - if (ta.getTypeArguments() == null || ta.getTypeArguments().size() == 0) { + Type bt = switch (ta.getWildcardMode()) { + case Super, Any -> getNameInfo().getJavaLangObject(); + case None, Extends -> getBaseType(ta); + }; + if (ta.getTypeArguments() == null || ta.getTypeArguments().isEmpty()) { return bt; } return new ParameterizedType((ClassType) bt, ta.getTypeArguments()); @@ -329,7 +311,6 @@ private void computeAllMemberTypes(ClassType ct, ClassTypeCacheEntry ctce) { if (cl == null) { continue; } - int cs = cl.size(); add_ClassTypes: for (ClassType hc : cl) { // hc == ct may occur as it is admissible for a member class // to extend its parent class @@ -337,7 +318,7 @@ private void computeAllMemberTypes(ClassType ct, ClassTypeCacheEntry ctce) { String cname = hc.getName(); for (int k = 0; k < result_size; k++) { ClassType rc = result.get(k); - if (rc.getName() == cname) { + if (Objects.equals(rc.getName(), cname)) { continue add_ClassTypes; } } @@ -444,8 +425,7 @@ public boolean isWidening(Type from, Type to) { if (to instanceof ClassType) { return isWidening((ClassType) from, (ClassType) to); } else { - return (from instanceof NullType) - && (to instanceof ArrayType || to instanceof TypeParameter); + return from instanceof NullType && to instanceof ArrayType; } } else if (from instanceof PrimitiveType) { if (to instanceof PrimitiveType) { @@ -509,7 +489,7 @@ public boolean isSupertype(ClassType a, ClassType b) { return isSubtype(b, a); } - private final boolean paramMatches(Type ta, Type tb, boolean allowAutoboxing) { + private boolean paramMatches(Type ta, Type tb, boolean allowAutoboxing) { if (ta == tb) { return true; } @@ -585,7 +565,7 @@ private ClassType getClassTypeFromTypeParameter(TypeParameter tp, int i) { return t; } - private final boolean internalIsCompatibleSignature(List a, List b, + private boolean internalIsCompatibleSignature(List a, List b, boolean allowAutoboxing, boolean isVarArgMethod) { int s = b.size(); int n = a.size(); @@ -896,9 +876,7 @@ private void internalFilterApplicableMethods(List list, String name, private List replaceTypeArguments(List methodSig, List typeArguments, Method m) { List res = new ArrayList<>(methodSig.size()); - for (Type type : methodSig) { - res.add(type); - } + res.addAll(methodSig); for (int l = 0; l < m.getTypeParameters().size(); l++) { TypeParameter tp = m.getTypeParameters().get(l); for (int k = 0; k < methodSig.size(); k++) { @@ -1025,7 +1003,7 @@ private List internalGetMostSpecificMethods(ClassType ct, String name, List signature, List meths, List typeArgs, ClassType context) { Debug.assertNonnull(ct, name, signature); - boolean allowJava5 = Boolean.valueOf( + boolean allowJava5 = Boolean.parseBoolean( getServiceConfiguration().getProjectSettings().getProperty(PropertyNames.JAVA_5)); List result; @@ -1059,13 +1037,13 @@ public List doThreePhaseFilter(List methods, List 0) { + if (!result.isEmpty()) { return result; } result.addAll(applicableMethods); // result is empty at this point filterMostSpecificMethodsPhase2(result); - if (result.size() > 0) { + if (!result.isEmpty()) { return result; } result.addAll(applicableMethods); // once again, result is empty @@ -1084,7 +1062,6 @@ public void reset() { /** * Takes an (Array|Class)Type and adds type arguments to it. * - * @return * @throws AssertionError if t is neither a Class or Array Type * @throws ClassCastException if t is an array type with a primitive type as base type. */ diff --git a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java index 8842e3a81a8..89f5265b610 100644 --- a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java @@ -89,7 +89,6 @@ static boolean isPartOf(ProgramElement pe, Class c) { /** * looks for the next variable scope that is a parent of the given element * - * @param pe a program element * @return the outer variable scope of the program element or null */ private static VariableScope findOuterVariableScope(VariableScope ts) { @@ -160,7 +159,7 @@ private static LoopStatement findInnermostLoop(Statement s) { /** * Initializes the new service; called by the configuration. * - * @param config the configuration this services becomes part of. + * @param cfg the configuration this services becomes part of. */ public void initialize(ServiceConfiguration cfg) { super.initialize(cfg); @@ -198,8 +197,6 @@ protected NameInfo getNameInfo() { /** * Change notification callback method. - * - * @param config the configuration this services becomes part of. */ public void modelChanged(ChangeHistoryEvent changes) { List changed = changes.getChanges(); diff --git a/recoder/src/main/java/recoder/util/OptionManager.java b/recoder/src/main/java/recoder/util/OptionManager.java index 390b7f318a9..004b6036bca 100644 --- a/recoder/src/main/java/recoder/util/OptionManager.java +++ b/recoder/src/main/java/recoder/util/OptionManager.java @@ -117,10 +117,8 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } Object optval = null; switch (descr.type) { - case SIMPLE: - optval = TRUE; - break; - case SWITCH: + case SIMPLE -> optval = TRUE; + case SWITCH -> { if ("on".equals(sval)) { optval = ON; } else if ("off".equals(sval)) { @@ -128,8 +126,8 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } else { throw new IllegalOptionValueException(opt, sval); } - break; - case BOOL: + } + case BOOL -> { if ("true".equals(sval)) { optval = TRUE; } else if ("false".equals(sval)) { @@ -137,17 +135,15 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } else { throw new IllegalOptionValueException(opt, sval); } - break; - case NUM: + } + case NUM -> { try { optval = Integer.valueOf(sval); } catch (NumberFormatException nfe) { throw new IllegalOptionValueException(opt, sval); } - break; - case STRING: - optval = sval; - break; + } + case STRING -> optval = sval; } Debug.assertNonnull(optval); descr.values.addElement(optval); @@ -168,7 +164,7 @@ public String[] parseArgs(String[] args) // check if all mandatory arguments have been set for (Enumeration mand = mandatories.elements(); mand.hasMoreElements();) { OptionDescription descr = (OptionDescription) mand.nextElement(); - if (descr.values.size() == 0) { + if (descr.values.isEmpty()) { throw new MissingArgumentException(descr.shortOpt); } } @@ -332,7 +328,7 @@ public String getStringVal(String opt, String defaultVal) { /** * describes a single command line option. */ - private static class OptionDescription { + public static class OptionDescription { int type; int multiplicity;