Nullness Type System for key.core

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java

@@ -96,7 +96,7 @@ public Proof getSource() {
      * {@inheritDoc}
      */
     @Override
-    public boolean equals(Object obj) {
+    public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
         if (obj instanceof IProofReference<?> other) {
             return Objects.equals(getKind(), other.getKind())
                     && Objects.equals(getSource(), other.getSource())

key.core.rifl/build.gradle

@@ -1,4 +1,20 @@
 description "Support for the RS3 Information Flow Language (RIFL)"
 dependencies {
     implementation project (":key.core")
-}
+}
+
+checkerFramework {
+    if(System.getProperty("ENABLE_NULLNESS")) {
+        checkers = [
+                "org.checkerframework.checker.nullness.NullnessChecker",
+        ]
+        extraJavacArgs = [
+                //"-AonlyDefs=^org\\.key_project\\.logic",
+                "-Xmaxerrs", "10000",
+                "-Astubs=$rootDir/key.util/src/main/checkerframework${File.pathSeparatorChar}permit-nullness-assertion-exception.astub",
+                "-AstubNoWarnIfNotFound",
+                "-Werror",
+                "-Aversion",
+        ]
+    }
+}

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

@@ -3,11 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.util.rifl;
 
-import java.util.HashMap;
-import java.util.LinkedHashSet;
-import java.util.Map;
+import java.util.*;
 import java.util.Map.Entry;
-import java.util.Set;
 
 import de.uka.ilkd.key.util.rifl.SpecificationEntity.Field;
 import de.uka.ilkd.key.util.rifl.SpecificationEntity.Parameter;
@@ -69,7 +66,8 @@ public String field(recoder.java.declaration.FieldDeclaration fd, Type type) {
 
     @Override
     public String field(String inPackage, String inClass, String name, Type type) {
-        return field2domain.get(new Field(name, inPackage, inClass, type));
+        return Objects.requireNonNull(field2domain.get(new Field(name, inPackage, inClass, type)),
+            "Could not find field");
     }
 
     @Override
@@ -83,8 +81,10 @@ public String parameter(recoder.java.declaration.MethodDeclaration md, int index
     @Override
     public String parameter(String inPackage, String inClass, String methodName,
             String[] paramTypes, int index, Type type) {
-        return param2domain
-                .get(new Parameter(index, methodName, paramTypes, inPackage, inClass, type));
+        return Objects.requireNonNull(
+            param2domain
+                    .get(new Parameter(index, methodName, paramTypes, inPackage, inClass, type)),
+            "Parameter not found");
     }
 
     @Override
@@ -97,7 +97,9 @@ public String returnValue(recoder.java.declaration.MethodDeclaration md, Type ty
     @Override
     public String returnValue(String inPackage, String inClass, String methodName,
             String[] paramTypes, Type type) {
-        return return2domain.get(new ReturnValue(methodName, paramTypes, inPackage, inClass, type));
+        return Objects.requireNonNull(
+            return2domain.get(new ReturnValue(methodName, paramTypes, inPackage, inClass, type)),
+            "Return value not found");
     }
 
     @Override

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

@@ -8,9 +8,13 @@
 
 import de.uka.ilkd.key.util.LinkedHashMap;
 
+import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
+import org.checkerframework.checker.nullness.qual.KeyFor;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.key_project.util.collection.KeYCollections;
 import org.key_project.util.collection.Pair;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import org.xml.sax.Attributes;
@@ -84,10 +88,10 @@ private static String printAttributes(Attributes a) {
     private final Map<String, String> handles2categories = new LinkedHashMap<>();
     private Set<String> domains = new LinkedHashSet<>();
     private Set<Entry<String, String>> flow = new LinkedHashSet<>();
-    private Map<SpecificationEntity, Pair<String, String>> tmpMap = null;
-    private Type type = null;
+    private Map<SpecificationEntity, Pair<String, String>> tmpMap = new HashMap<>();
+    private Type type = Type.SOURCE;
 
-    private String tmpHandle = null;
+    private @MonotonicNonNull String tmpHandle = null;
 
     private String category = DEFAULT_CATEGORY;
 
@@ -96,17 +100,20 @@ public RIFLHandler() {
     }
 
     private void assignHandle(Attributes attributes) {
-        final String handle = attributes.getValue("handle").intern();
+        @SuppressWarnings("keyfor")
+        final @KeyFor("handles2categories") String handle = attributes.getValue("handle").intern();
         final String domain = attributes.getValue("domain").intern();
         Pair<String, String> p = new Pair<>(handle, handles2categories.get(handle));
         categories2domains.put(p, domain);
     }
 
+    @EnsuresNonNull("tmpHandle")
     private void setModifiable(Attributes attributes) {
         assert tmpHandle == null;
         tmpHandle = attributes.getValue("handle");
     }
 
+    @SuppressWarnings("nullness") // uninitialization
     private void unsetModifiable() {
         assert tmpHandle != null;
         tmpHandle = null;
@@ -125,7 +132,10 @@ public SpecificationContainer getSpecification() {
         return new DefaultSpecificationContainer(tmp, flow);
     }
 
-    private void putField(Attributes attributes) {
+    private void putField(Attributes attributes) throws SAXException {
+        if (tmpHandle == null) {
+            throw new SAXException("This element must be in a modifiable element!");
+        }
         final String field = attributes.getValue("name");
         final String clazz = attributes.getValue("class");
         final String packg = attributes.getValue("package");
@@ -134,7 +144,10 @@ private void putField(Attributes attributes) {
         tmpMap.put(se, new Pair<>(tmpHandle, category));
     }
 
-    private void putParam(Attributes attributes) {
+    private void putParam(Attributes attributes) throws SAXException {
+        if (tmpHandle == null) {
+            throw new SAXException("This element must be in a modifiable element!");
+        }
         final String packg = attributes.getValue("package");
         final String clazz = attributes.getValue("class");
         final String method = attributes.getValue("method");
@@ -144,13 +157,16 @@ private void putParam(Attributes attributes) {
         tmpMap.put(se, new Pair<>(tmpHandle, category));
     }
 
-    private void putReturn(Attributes attributes) {
+    private void putReturn(Attributes attributes) throws SAXException {
+        if (tmpHandle == null) {
+            throw new SAXException("This element must be in a modifiable element!");
+        }
         final String packageName = attributes.getValue("package");
         final String className = attributes.getValue("class");
         final String methodName = attributes.getValue("method");
         final SpecificationEntity se = new ReturnValue(methodName, packageName, className, type);
         handles2categories.put(tmpHandle, category);
-        tmpMap.put(se, new Pair<>(tmpHandle, category));
+        tmpMap.put(se, new Pair<String, String>(tmpHandle, category));
     }
 
     private void putFlow(Attributes attributes) {
@@ -196,14 +212,15 @@ private void checkDomainAssignmentsWithFlows() {
          */
     }
 
+    @SuppressWarnings("nullness")
     private void checkFlows() {
         for (var p : categories2domains.entrySet()) {
             assert domains.contains(categories2domains.get(p.getKey()));
         }
     }
 
     @Override
-    public void startElement(String uri, String localName, String qName, Attributes attributes) {
+    public void startElement(String uri, String localName, String qName, Attributes attributes) throws SAXException {
         switch (localName) {
         case "sourcedompair", "source" -> startSources();
         case "sinkdompair", "sink" -> startSinks();

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

@@ -117,7 +117,7 @@ public static File getDefaultSavePath(File origSourcePath) {
 
     private static File getBaseDirPath(File origSourcePath) {
         if (origSourcePath.isFile()) {
-            return origSourcePath.getParentFile();
+            return Objects.requireNonNull(origSourcePath.getParentFile());
         } else {
             return origSourcePath;
         }

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

@@ -13,7 +13,7 @@
  */
 public abstract class SpecificationEntity {
 
-    enum Type {
+    public enum Type {
         SOURCE, SINK
     }
 
@@ -34,7 +34,7 @@ public static final class Field extends SpecificationEntity {
         }
 
         @Override
-        public boolean equals(Object o) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object o) {
             if (super.equals(o) && o instanceof Field) {
                 return name.equals(((Field) o).name);
             } else {
@@ -92,7 +92,7 @@ public static final class Parameter extends SpecificationEntity {
         }
 
         @Override
-        public boolean equals(Object o) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object o) {
             if (super.equals(o) && o instanceof Parameter) {
                 return (methodName.equals(((Parameter) o).methodName)
                         && Arrays.equals(((Parameter) o).paramTypes, paramTypes)
@@ -164,7 +164,7 @@ public static final class ReturnValue extends SpecificationEntity {
         }
 
         @Override
-        public boolean equals(Object o) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object o) {
             if (super.equals(o) && o instanceof ReturnValue) {
                 return (methodName.equals(((ReturnValue) o).methodName)
                         && Arrays.equals(paramTypes, ((ReturnValue) o).paramTypes));
@@ -209,7 +209,7 @@ private SpecificationEntity(String p, String c, Type t) {
     }
 
     @Override
-    public boolean equals(Object o) {
+    public boolean equals(@org.jspecify.annotations.Nullable Object o) {
         if (o instanceof SpecificationEntity) {
             return (inPackage.equals(((SpecificationEntity) o).inPackage)
                     && inClass.equals(((SpecificationEntity) o).inClass)

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

@@ -9,6 +9,7 @@
 
 import de.uka.ilkd.key.util.rifl.SpecificationEntity.Type;
 
+import org.jspecify.annotations.Nullable;
 import recoder.abstraction.ClassType;
 import recoder.java.*;
 import recoder.java.declaration.*;
@@ -49,18 +50,13 @@ private static class JMLFactory {
 
         private final String indentation;
         private final Map<String, Set<Entry<String, Type>>> respects = new HashMap<>();
-        private SpecificationContainer sc;
+        private final SpecificationContainer sc;
 
         JMLFactory(SpecificationContainer sc) {
             indentation = DEFAULT_INDENTATION;
             this.sc = sc;
         }
 
-        @SuppressWarnings("unused")
-        JMLFactory(int indent) {
-            indentation = " ".repeat(indent);
-        }
-
         @SuppressWarnings("unused")
         void addResultToDetermines(Type t) {
             put(DEFAULT_KEY, t, RESULT);
@@ -85,7 +81,7 @@ void addToDetermines(String name, Type t, String key) {
         }
 
         String getRespects(String domain, final Type t) {
-            return getRespects(respects.get(domain), t);
+            return getRespects(Objects.requireNonNull(respects.get(domain)), t);
         }
 
         String getRespects(Set<String> oneRespect) {
@@ -157,13 +153,13 @@ String getSpecification() {
                 sb.append(JML_END);
                 return sb.toString();
             } else {
-                return null;
+                return "";
             }
 
 
         }
 
-        private void put(String key, Entry<String, Type> value) {
+        private void put(@Nullable String key, Entry<String, Type> value) {
             if (key == null) {
                 return;
             }
@@ -206,7 +202,7 @@ private void accessChildren(JavaNonTerminalProgramElement pe) {
         }
     }
 
-    private void addComment(JavaProgramElement se, String comment) {
+    private void addComment(JavaProgramElement se, @Nullable String comment) {
         // remember which methods were specified and generate po files only for them
         if (se instanceof MethodDeclaration) {
             specifiedMethodDeclarations.add((MethodDeclaration) se);

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java

@@ -5,4 +5,7 @@
  * This package contains a transformer from input RIFL files (XML) and
  * original Java files to JML* annotated files.
  */
+@NullMarked
 package de.uka.ilkd.key.util.rifl;
+
+import org.jspecify.annotations.NullMarked;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -1046,7 +1046,7 @@ public String toString() {
          * {@inheritDoc}
          */
         @Override
-        public boolean equals(Object obj) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
             if (obj instanceof ExtractLocationParameter other) {
                 return Objects.equals(arrayIndex, other.arrayIndex)
                         && stateMember == other.stateMember
@@ -1775,7 +1775,7 @@ public Node getGoalNode() {
          * {@inheritDoc}
          */
         @Override
-        public boolean equals(Object obj) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
             if (obj instanceof ExecutionVariableValuePair other) {
                 return isArrayRange()
                         ? (getArrayStartIndex().equals(other.getArrayStartIndex())

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java

@@ -335,7 +335,7 @@ private record ParentDef(Term parent, Node goalNode) {
              * {@inheritDoc}
              */
             @Override
-            public boolean equals(Object obj) {
+            public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
                 if (obj instanceof ParentDef other) {
                     return Objects.equals(parent, other.parent)
                             && Objects.equals(goalNode, other.goalNode);
@@ -369,7 +369,7 @@ private record LocationDef(ProgramVariable programVariable, Term arrayIndex) {
              * {@inheritDoc}
              */
             @Override
-            public boolean equals(Object obj) {
+            public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
                 if (obj instanceof LocationDef other) {
                     return programVariable == other.programVariable
                             && Objects.equals(arrayIndex, other.arrayIndex);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java

@@ -1850,7 +1850,7 @@ public JavaPair(Integer stackSize, ImmutableList<SourceElement> elementsOfIntere
          * {@inheritDoc}
          */
         @Override
-        public boolean equals(Object o) {
+        public boolean equals(@org.jspecify.annotations.Nullable Object o) {
             if (super.equals(o)) {
                 if (o instanceof JavaPair other) {
                     if (second.size() == other.second.size()) {

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

@@ -245,7 +245,7 @@ public int hashCode() {
      * {@inheritDoc}
      */
     @Override
-    public boolean equals(Object obj) {
+    public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
         if (obj instanceof ProgramMethodPO other) {
             return Objects.equals(pm, other.getProgramMethod())
                     && Objects.equals(precondition, other.getPrecondition());

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

@@ -284,7 +284,7 @@ public int hashCode() {
      * {@inheritDoc}
      */
     @Override
-    public boolean equals(Object obj) {
+    public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
         if (obj instanceof ProgramMethodSubsetPO other) {
             return super.equals(obj)
                     && Objects.equals(getStartPosition(), other.getStartPosition())

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java

@@ -97,7 +97,7 @@ public int hashCode() {
      * {@inheritDoc}
      */
     @Override
-    public boolean equals(Object obj) {
+    public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
         if (obj instanceof Access other) {
             return Objects.equals(programVariable, other.getProgramVariable())
                     && Objects.equals(dimensionExpressions, other.getDimensionExpressions());