Merge branch 'main' into copy-referenced-action

.github/dependabot.yml

@@ -5,7 +5,19 @@
 
 version: 2
 updates:
-  - package-ecosystem: "gradle" # See documentation for possible values
-    directory: "/" # Location of package manifests
+  - package-ecosystem: "gradle"
+    directory: "/"
     schedule:
-      interval: "weekly"
+      interval: "monthly"
+    groups:
+      gradle-deps:
+        patterns:
+          - "*"      
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "monthly"
+    groups:
+      github-actions-deps:
+        patterns:
+          - "*"

.github/dlsmt.sh

@@ -1,6 +1,6 @@
 # No shebang!
 
-## Weigl's little helper to download SMT-solvers. 
+## Weigl's little helper to download SMT-solvers.
 # SPDX-License-Identifier: GPL-2.0-or-later
 
 # This script is meant to be executed inside an Github Action to download the SMT-solver. 
@@ -27,6 +27,7 @@
 mkdir smt-solvers
 cd smt-solvers
 
+set -x # exit on error
 
 #################################################
 echo "::group::{install z3}"
@@ -36,7 +37,10 @@ if readlink -f */bin/z3; then
   echo "::notice::{Z3 found. Caching works! Skip installation}"
 else 
   echo "Download Z3"
-  gh release download --skip-existing -p 'z3-*-x64-glibc-*.zip' -R Z3Prover/z3
+  rm z3-*.zip
+  # gh release download --skip-existing -p 'z3-*-x64-glibc-2.35.zip' -R Z3Prover/z3
+  ## pin to a release
+  wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-x64-glibc-2.35.zip
   unzip -n z3*.zip
   rm z3-*-x64-glibc-*.zip  
 fi
@@ -51,14 +55,19 @@ echo "::endgroup::"
 
 #################################################
 echo "::group::{install cvc5}"
-if -f cvc5-Linux; then 
-  echo "::notice::{Z3 found. Caching works! Skip installation}"
+if -f cvc5-Linux-static/bin/cvc5; then
+  echo "::notice::{CVC5 found. Caching works! Skip installation}"
 else 
   echo "Install CVC5"
-  gh release download --skip-existing -p 'cvc5-Linux' -R cvc5/cvc5  
+  # does not work anymore
+  # gh release download --skip-existing -p 'cvc5-Linux' -R cvc5/cvc5
+
+  wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip
+  unzip cvc5-Linux-static.zip
+  rm cvc5-Linux-static.zip
 fi 
 
-CVC5=$(readlink -f cvc5-Linux)
+CVC5=$(readlink -f cvc5-Linux-static/bin/cvc5)
 echo "CVC5 installed and added to path: CVC5"
 chmod u+x $CVC5
 echo $(dirname $CVC5) >> $GITHUB_PATH

.github/pull_request_template.md

@@ -2,8 +2,8 @@
 Thanks for submitting this pull request for KeY.
 Since the project has a strict review policy, please make the
 reviewer's job easier by providing the necessary information
-in the text below. The comments may remain since they will be
-invisible when showing the PR.
+in the text below. The comments can be deleted, but may also 
+remain since they will be invisible when showing the PR.
 -->
 
 ## Related Issue
@@ -17,26 +17,48 @@ This pull request addresses #.
 <!-- Please give a brief description of what behaviour changes and 
      why it should be changed. -->
 
+## Plan
+
+<!-- If this pull request is not yet finished, but has open jobs,
+     please list them here. It helps others to estimate the state of this
+     PR. This list can and should be adapted as the PR develops.
+     Items should be crossed out when finished, not deleted.
+     
+     Remove the section if the PR was finished at submission time.
+     The following items are examples:
+-->
+* [ ] Implement feature 1
+* [ ] Implement feature 2
+* [ ] Code cleanup
+* [ ] Document the changes
+
 ## Type of pull request
 
-<!--- What types of changes does your code introduce? Put an `x` in the box(es) that apply: -->
+<!--- What types of changes does your code introduce? 
+      Delete those lines that do not apply.      
+-->
 
-- [ ] Bug fix (non-breaking change which fixes an issue)
-- [ ] Refactoring (behaviour should not change or only minimally change)
-- [ ] New feature (non-breaking change which adds functionality)
-- [ ] Breaking change (fix or feature that would cause existing functionality to change)
-- [ ] There are changes to the (Java) code
-- [ ] There are changes to the taclet rule base
-- [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
-- [ ] Other: 
+- Bug fix (non-breaking change which fixes an issue)
+- Refactoring (behaviour should not change or only minimally change)
+- New feature (non-breaking change which adds functionality)
+- Breaking change (fix or feature that would cause existing functionality to change)
+- There are changes to the (Java) code
+- There are changes to the taclet rule base
+- There are changes to the deployment/CI infrastructure (gradle, github, ...)
+- Other: 
 
 ## Ensuring quality
+
+<!--- How did you make sure that the proposed change improves the code base? 
+      Delete those lines that do not apply.
+      Please make an effort to delete as few lines as possible. :-)
+-->
 
-- [ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
-- [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
-- [ ] I added new test case(s) for new functionality.
-- [ ] I have tested the feature as follows: ...
-- [ ] I have checked that runtime performance has not deteriorated.
+- I made sure that introduced/changed code is well documented (javadoc and inline comments).
+- I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
+- I added new test case(s) for new functionality.
+- I have tested the feature as follows: ...
+- I have checked that runtime performance has not deteriorated.
 
 ## Additional information and contact(s)
 

.github/workflows/code_quality.yml

@@ -9,6 +9,22 @@ on:
       - 'KeY-*'
 
 jobs:
+  checkerFramework:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up JDK 21
+        uses: actions/setup-java@v3
+        with:
+          java-version: 21
+          distribution: 'corretto'
+          cache: 'gradle'
+      - name: Build with Gradle
+        uses: gradle/gradle-build-action@v2.4.2
+        with:
+          arguments: -DENABLE_NULLNESS=true compileTest
+
+
   qodana:
     runs-on: ubuntu-latest
     steps:

README.md

@@ -20,7 +20,7 @@ The current version of KeY is 2.12.2, 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)
+* [Using as a Symbolic Execution Backend](https://github.com/KeYProject/symbex-java-example)
 
 ## Requirements
 

build.gradle

@@ -22,6 +22,9 @@ plugins {
 
     // Code formatting
     id "com.diffplug.spotless" version "6.25.0"
+
+    // EISOP Checker Framework
+    id "org.checkerframework" version "0.6.28"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -53,6 +56,7 @@ subprojects {
     apply plugin: "com.diffplug.spotless"
     apply plugin: "checkstyle"
     apply plugin: "pmd"
+    apply plugin: "org.checkerframework"
 
     group = rootProject.group
     version = rootProject.version
@@ -70,18 +74,29 @@ subprojects {
     }
 
     dependencies {
+        implementation("org.slf4j:slf4j-api:2.0.13")
         implementation("org.slf4j:slf4j-api:2.0.12")
+        testImplementation("ch.qos.logback:logback-classic:1.4.8")
+
+        //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
+        //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
+
+        compileOnly("org.jspecify:jspecify:0.3.0")
+        testCompileOnly("org.jspecify:jspecify:0.3.0")
+        def eisop_version = "3.42.0-eisop2"
+        compileOnly "io.github.eisop:checker-qual:$eisop_version"
+        compileOnly "io.github.eisop:checker-util:$eisop_version"
+        testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
+        checkerFramework "io.github.eisop:checker:$eisop_version"
 
-        testImplementation("ch.qos.logback:logback-classic:1.5.3")
+        testImplementation("ch.qos.logback:logback-classic:1.5.6")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2'
         testImplementation project(':key.util')
 
         testCompileOnly 'junit:junit:4.13.2'
         testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2'
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2'
-
-        implementation("org.jspecify:jspecify:0.3.0")
     }
 
     tasks.withType(JavaCompile) {
@@ -346,6 +361,19 @@ subprojects {
         }
     }
 
+//    checkerFramework {
+//        checkers = [
+//            "org.checkerframework.checker.nullness.NullnessChecker",
+//        ]
+//        extraJavacArgs = [
+//            "-AonlyDefs=^org\\.key_project\\.util",
+//            "-Xmaxerrs", "10000",
+//            "-Astubs=$projectDir/src/main/checkerframework",
+//            "-Werror",
+//            "-Aversion",
+//        ]
+//    }
+
     afterEvaluate { // required so project.description is non-null as set by sub build.gradle
         publishing {
             publications {

key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key

@@ -41,11 +41,11 @@
 
 \javaSource "%%JAVA_SOURCE%%";
 
-\proofObligation "#Proof Obligation Settings
-name=%%PO_NAME%%
-contract=%%PO_NAME%%
-class=de.uka.ilkd.key.informationflow.po.InfFlowContractPO
-";
+\proofObligation {
+	"name": "%%PO_NAME%%",
+	"contract": "%%PO_NAME%%",
+	"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
+ }
 
 \proofScript "macro 'infflow-autopilot';"
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java

@@ -384,7 +384,7 @@ public static boolean containsSequentFormulasToRefactor(TermLabelState state) {
         @SuppressWarnings("unchecked")
         Set<SequentFormula> sfSet =
             (Set<SequentFormula>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
-        return !CollectionUtil.isEmpty(sfSet);
+        return sfSet != null && !sfSet.isEmpty();
     }
 
     /**

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java

@@ -26,6 +26,7 @@
 import de.uka.ilkd.key.pp.PrettyPrinter;
 import de.uka.ilkd.key.proof.init.AbstractOperationPO;
 import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.speclang.PositionedString;
 import de.uka.ilkd.key.speclang.jml.translation.Context;
 import de.uka.ilkd.key.speclang.njml.JmlIO;
@@ -263,14 +264,17 @@ public String getPrecondition() {
 
     /**
      * {@inheritDoc}
+     *
+     * @return
      */
     @Override
-    public void fillSaveProperties(Properties properties) {
-        super.fillSaveProperties(properties);
-        properties.setProperty("method", getProgramMethodSignature(getProgramMethod(), true));
+    public Configuration createLoaderConfig() {
+        var c = super.createLoaderConfig();
+        c.set("method", getProgramMethodSignature(getProgramMethod(), true));
         if (getPrecondition() != null && !getPrecondition().isEmpty()) {
-            properties.setProperty("precondition", getPrecondition());
+            c.set("precondition", getPrecondition());
         }
+        return c;
     }
 
     /**
@@ -294,34 +298,19 @@ public static String getProgramMethodSignature(IProgramMethod pm, boolean includ
         return x.result();
     }
 
-    /**
-     * Instantiates a new proof obligation with the given settings.
-     *
-     * @param initConfig The already load {@link InitConfig}.
-     * @param properties The settings of the proof obligation to instantiate.
-     * @return The instantiated proof obligation.
-     * @throws IOException Occurred Exception.
-     */
-    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
-            throws IOException {
-        return new LoadedPOContainer(new ProgramMethodPO(initConfig, getName(properties),
-            getProgramMethod(initConfig, properties), getPrecondition(properties),
-            isAddUninterpretedPredicate(properties), isAddSymbolicExecutionLabel(properties)));
-    }
-
     /**
      * Searches the {@link IProgramMethod} defined by the given {@link Properties}.
      *
-     * @param initConfig The already load {@link InitConfig}.
+     * @param initConfig The already loaded {@link InitConfig}.
      * @param properties The settings of the proof obligation to instantiate.
      * @return The found {@link IProgramMethod}.
      * @throws IOException Occurred Exception if it was not possible to find the
      *         {@link IProgramMethod}.
      */
-    public static IProgramMethod getProgramMethod(InitConfig initConfig, Properties properties)
+    public static IProgramMethod getProgramMethod(InitConfig initConfig, Configuration properties)
             throws IOException {
         // Get container class and method signature
-        String value = properties.getProperty("method");
+        String value = properties.getString("method");
         if (value == null) {
             throw new IOException("Property \"method\" is not defined.");
         }
@@ -380,8 +369,8 @@ public static IProgramMethod getProgramMethod(InitConfig initConfig, Properties
      * @param properties The proof obligation settings to read from.
      * @return The precondition or {@code null} if not available.
      */
-    public static String getPrecondition(Properties properties) {
-        return properties.getProperty("precondition");
+    public static String getPrecondition(Configuration properties) {
+        return properties.getString("precondition");
     }
 
     @Override