Basic Nullness Checker configuration

.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:

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
@@ -71,6 +75,19 @@ 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.6")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2'
@@ -80,8 +97,6 @@ subprojects {
         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.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/util/SymbolicExecutionUtil.java

@@ -4141,7 +4141,7 @@ public static boolean lazyComputeIsAdditionalBranchVerified(Node node) {
             Set<Term> additinalPredicates =
                 AbstractOperationPO.getAdditionalUninterpretedPredicates(node.proof());
             // Check if node can be treated as verified/closed
-            if (!CollectionUtil.isEmpty(additinalPredicates)) {
+            if (additinalPredicates != null && !additinalPredicates.isEmpty()) {
                 boolean verified = true;
                 Iterator<Node> leafsIter = node.leavesIterator();
                 while (verified && leafsIter.hasNext()) {

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java

@@ -55,7 +55,7 @@ public String getDescription() {
 
     @Override
     public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) {
-        if (goals == null || goals.head() == null || goals.head().node() == null
+        if (goals == null || goals.isEmpty() || goals.head().node() == null
                 || goals.head().node().parent() == null) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java

@@ -51,7 +51,7 @@ public String getDescription() {
 
     @Override
     public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) {
-        if (goals == null || goals.head() == null || goals.head().node() == null
+        if (goals == null || goals.isEmpty() || goals.head().node() == null
                 || goals.head().node().parent() == null) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java

@@ -52,7 +52,7 @@ public String getDescription() {
 
     @Override
     public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) {
-        if (goals == null || goals.head() == null) {
+        if (goals == null || goals.isEmpty()) {
             return false;
         }
         if (posInOcc == null || posInOcc.subTerm() == null) {

key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java

@@ -66,7 +66,12 @@ private void linkSymbExecVarsToCopies() {
     private void linkStateVarsToCopies(StateVars ifVars, StateVars seVars, Map<Term, Term> map) {
         final Iterator<Term> ifVarsIt = ifVars.termList.iterator();
         for (final Term symbTerm : seVars.termList) {
-            final Term ifTerm = ifVarsIt.next();
+            final Term ifTerm;
+            if (ifVarsIt.hasNext()) {
+                ifTerm = ifVarsIt.next();
+            } else {
+                ifTerm = null;
+            }
             if (symbTerm != null) {
                 map.put(symbTerm, ifTerm);
             }

key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java

@@ -1061,7 +1061,9 @@ public ProgramVariable getAttribute(final String attributeName, Sort s) {
      */
     public ProgramVariable getCanonicalFieldProgramVariable(String fieldName, KeYJavaType kjt) {
         ImmutableList<ProgramVariable> allAttributes = getAllAttributes(fieldName, kjt, false);
-        if (kjt.getJavaType() instanceof ArrayType) {
+        if (allAttributes.isEmpty()) {
+            return null;
+        } else if (kjt.getJavaType() instanceof ArrayType) {
             return allAttributes.head();
         } else {
             return allAttributes.reverse().head();

key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
-
 import java.util.List;
 import java.util.Objects;
 

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -24,6 +24,7 @@
 import org.antlr.v4.runtime.misc.ParseCancellationException;
 import org.antlr.v4.runtime.tree.TerminalNode;
 import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -37,6 +38,7 @@
  * @author Alexander Weigl
  * @version 1 (19.08.19)
  */
+@NullMarked
 public final class ParsingFacade {
     private static final Logger LOGGER = LoggerFactory.getLogger(ParsingFacade.class);
 

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java

@@ -22,8 +22,8 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.Named;
 import org.key_project.logic.sort.Sort;
-import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableSet;
+import org.key_project.util.collection.Immutables;
 
 import org.antlr.v4.runtime.Token;
 import org.slf4j.Logger;
@@ -147,9 +147,9 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
             Name sortName = new Name(sortId);
 
             ImmutableSet<Sort> ext = sortExt == null ? ImmutableSet.empty()
-                    : DefaultImmutableSet.fromCollection(sortExt);
+                    : Immutables.createSetFrom(sortExt);
             ImmutableSet<Sort> oneOf = sortOneOf == null ? ImmutableSet.empty()
-                    : DefaultImmutableSet.fromCollection(sortOneOf);
+                    : Immutables.createSetFrom(sortOneOf);
 
             // attention: no expand to java.lang here!
             Sort existingSort = sorts().lookup(sortName);

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -27,11 +27,7 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
-import org.key_project.util.collection.DefaultImmutableSet;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.collection.ImmutableSet;
-import org.key_project.util.collection.Pair;
+import org.key_project.util.collection.*;
 
 import antlr.RecognitionException;
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -740,7 +736,7 @@ public Object visitAddrules(KeYParser.AddrulesContext ctx) {
     @Override
     public ImmutableSet<SchemaVariable> visitAddprogvar(KeYParser.AddprogvarContext ctx) {
         final Collection<? extends SchemaVariable> accept = accept(ctx.pvs);
-        return ImmutableSet.fromSet(new HashSet<>(Objects.requireNonNull(accept)));
+        return Immutables.<SchemaVariable>createSetFrom(Objects.requireNonNull(accept));
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/parser/ParserException.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.parser;
 
-
 import de.uka.ilkd.key.util.parsing.HasLocation;
 
 import org.jspecify.annotations.Nullable;