Merge branch 'main' into weigl/overop

.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
 

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 [email protected]
+* For bug reports, please use the [issue tracker](https://github.com/KeYProject/key/issues) or send a mail to [email protected]. 
+
+* For discussions, you may want to subscribe and use the mailing list <[email protected]> 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/).
 
 
 

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'

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java

@@ -204,81 +204,49 @@ 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":
         // case "top":
         // 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 -> {
+        }
         }
     }
 

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<Sour
          * @param name The name of this node.
          * @param formatedPathCondition The formated path condition.
          * @param pathConditionChanged Is the path condition changed compared to parent?
-         * @param exceptionalTermination Exceptional termination?
+         * @param terminationKind kind of termination
          * @param branchVerified The branch verified flag.
          */
         public KeYlessTermination(IExecutionNode<?> 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]);
         }
 

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);
             }

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) {

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);

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'
 }
 

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)?
   )

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<String, ProofScriptCommand> commandMap = new HashMap<>();
+    private final Map<String, ProofScriptCommand<?>> commandMap = new HashMap<>();
 
     public ProofScriptCommandApi() {
         initialize();
     }
 
+    @SuppressWarnings("rawtypes")
     private void initialize() {
         ServiceLoader<ProofScriptCommand> 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<ProofScriptCommand> getScriptCommands() {
+    public Collection<ProofScriptCommand<?>> getScriptCommands() {
         return commandMap.values();
     }
 

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();
-    }
 }

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;