Nullness Type System for key.core

build.gradle

@@ -92,11 +92,11 @@ subprojects {
         //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:1.0.0")
+        implementation("org.jspecify:jspecify:1.0.0")
         testCompileOnly("org.jspecify:jspecify:1.0.0")
         def eisop_version = "3.49.3-eisop1"
-        compileOnly "io.github.eisop:checker-qual:$eisop_version"
-        compileOnly "io.github.eisop:checker-util:$eisop_version"
+        implementation "io.github.eisop:checker-qual:$eisop_version"
+        implementation "io.github.eisop:checker-util:$eisop_version"
         testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
@@ -138,6 +138,10 @@ subprojects {
         systemProperty "key.disregardSettings", "true"
         maxHeapSize = "4g"
 
+        // RAC non-null references.
+        jvmArgs("-javaagent:$rootDir/nonnull-0.1.0-SNAPSHOT-all.jar=VERBOSE,org.key_project,de.uka")
+
+
         forkEvery = 0 //default
         maxParallelForks = 1 // weigl: test on master
     }

key.core.example/src/main/java/org/key_project/Main.java

@@ -23,6 +23,7 @@
 
 import org.key_project.util.collection.ImmutableSet;
 
+import org.jspecify.annotations.NullMarked;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -31,6 +32,7 @@
  *
  * @author Martin Hentschel
  */
+@NullMarked
 public class Main {
     private static final Logger LOGGER = LoggerFactory.getLogger(Main.class);
 
@@ -52,14 +54,12 @@ public static void main(String[] args) {
         }
     }
 
-    /**
-     * sets up the environment with the Java project described by its location
-     *
-     * @param location the Path with the path to the source directory of the Java project
-     *        to be verified
-     * @return the {@KeYEnvironment} that provides the context for all following verification tasks
-     * @throws ProblemLoaderException if the setup fails
-     */
+    /// sets up the environment with the Java project described by its location
+    ///
+    /// @param location the Path with the path to the source directory of the Java project
+    /// to be verified
+    /// @return the [KeYEnvironment] that provides the context for all following verification tasks
+    /// @throws ProblemLoaderException if the setup fails
     private static KeYEnvironment<?> setupEnvironment(Path location) throws ProblemLoaderException {
         List<Path> classPaths = null; // Optionally: Additional specifications for API classes
         Path bootClassPath = null; // Optionally: Different default specifications for Java API
@@ -77,10 +77,8 @@ private static KeYEnvironment<?> setupEnvironment(Path location) throws ProblemL
         newSettings.putAll(MiscTools.getDefaultTacletOptions());
         choiceSettings.setDefaultChoices(newSettings);
         // Load source code
-        KeYEnvironment<?> env =
-            KeYEnvironment.load(location, classPaths, bootClassPath, includes);
+        return KeYEnvironment.load(location, classPaths, bootClassPath, includes);
         // env.getLoadedProof() returns performed proof if a *.proof file is loaded
-        return env;
     }
 
     /**
@@ -93,7 +91,7 @@ private static void proveEnvironmemt(KeYEnvironment<?> env) {
             final List<Contract> proofContracts = getContracts(env);
 
             for (Contract contract : proofContracts) {
-                LOGGER.info("Found contract '" + contract.getDisplayName());
+                LOGGER.info("Found contract '{}'", contract.getDisplayName());
                 proveContract(env, contract);
             }
         } finally {
@@ -166,9 +164,8 @@ private static void proveContract(KeYEnvironment<?> env, Contract contract) {
             env.getUi().getProofControl().startAndWaitForAutoMode(proof);
             // Show proof result
             boolean closed = proof.openGoals().isEmpty();
-            LOGGER.info("Contract '" + contract.getDisplayName() + "' of "
-                + contract.getTarget() + " is " + (closed ? "verified" : "still open")
-                + ".");
+            LOGGER.info("Contract '{}' of {} is {}.", contract.getDisplayName(),
+                contract.getTarget(), closed ? "verified" : "still open");
         } catch (ProofInputException e) {
             LOGGER.error("Exception at {} of {}", contract.getDisplayName(),
                 contract.getTarget());

key.core.example/src/main/java/org/key_project/package-info.java

@@ -0,0 +1,2 @@
+@org.jspecify.annotations.NullMarked
+package org.key_project;

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.proof_references;
 
 import java.util.LinkedHashSet;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.proof.Node;
@@ -174,7 +175,7 @@ public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node
         LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
         if (node != null && analysts != null) {
             for (IProofReferencesAnalyst analyst : analysts) {
-                LinkedHashSet<IProofReference<?>> analystResult =
+                Set<IProofReference<?>> analystResult =
                     analyst.computeReferences(node, services);
                 if (analystResult != null) {
                     merge(result, analystResult);
@@ -190,8 +191,7 @@ public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node
      * @param target The target to add to.
      * @param toAdd The {@link IProofReference}s to add.
      */
-    public static void merge(LinkedHashSet<IProofReference<?>> target,
-            LinkedHashSet<IProofReference<?>> toAdd) {
+    public static void merge(Set<IProofReference<?>> target, Set<IProofReference<?>> toAdd) {
         for (IProofReference<?> reference : toAdd) {
             merge(target, reference);
         }
@@ -203,7 +203,7 @@ public static void merge(LinkedHashSet<IProofReference<?>> target,
      * @param target The target to add to.
      * @param reference The {@link IProofReference} to add.
      */
-    public static void merge(LinkedHashSet<IProofReference<?>> target,
+    public static void merge(Set<IProofReference<?>> target,
             final IProofReference<?> reference) {
         if (!target.add(reference)) {
             // Reference exists before, so merge nodes of both references.

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java

@@ -26,6 +26,8 @@
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.collection.Pair;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Extracts used {@link ClassAxiom} and {@link ClassInvariant}s.
  *
@@ -36,7 +38,8 @@ public class ClassAxiomAndInvariantProofReferencesAnalyst implements IProofRefer
      * {@inheritDoc}
      */
     @Override
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
+    public @Nullable LinkedHashSet<IProofReference<?>> computeReferences(Node node,
+            Services services) {
         String name = MiscTools.getRuleName(node);
         if (name != null
                 && (name.toLowerCase().contains("axiom_for")
@@ -102,7 +105,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
      * @return The {@link KeYJavaType} which provides the proof obligation or {@code null} if it was
      *         not possible to compute it.
      */
-    protected KeYJavaType findProofsKeYJavaType(Services services) {
+    protected @Nullable KeYJavaType findProofsKeYJavaType(Services services) {
         ProofOblInput problem =
             services.getSpecificationRepository().getProofOblInput(services.getProof());
         if (problem != null) {

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java

@@ -12,6 +12,8 @@
 import de.uka.ilkd.key.rule.AbstractContractRuleApp;
 import de.uka.ilkd.key.speclang.Contract;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Extracts used contracts.
  *
@@ -22,7 +24,8 @@ public class ContractProofReferencesAnalyst implements IProofReferencesAnalyst {
      * {@inheritDoc}
      */
     @Override
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
+    public @Nullable LinkedHashSet<IProofReference<?>> computeReferences(Node node,
+            Services services) {
         if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp contractRuleApp) {
             DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java

@@ -3,13 +3,15 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof_references.analyst;
 
-import java.util.LinkedHashSet;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof_references.ProofReferenceUtil;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * <p>
  * Instances of this class are used to compute {@link IProofReference} for a given {@link Node}
@@ -34,5 +36,6 @@ public interface IProofReferencesAnalyst {
      * @return The found {@link IProofReference} or {@code null}/empty set if the applied rule is
      *         not supported.
      */
-    LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services);
+    @Nullable
+    Set<IProofReference<?>> computeReferences(Node node, Services services);
 }

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java

@@ -13,6 +13,8 @@
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Extracts inlined methods.
  *
@@ -23,8 +25,9 @@ public class MethodBodyExpandProofReferencesAnalyst implements IProofReferencesA
      * {@inheritDoc}
      */
     @Override
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
-        if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
+    public @Nullable LinkedHashSet<IProofReference<?>> computeReferences(Node node,
+            Services services) {
+        if (node.getAppliedRuleApp() != null) {
             NodeInfo info = node.getNodeInfo();
             if (info.getActiveStatement() instanceof MethodBodyStatement mbs) {
                 IProgramMethod pm = mbs.getProgramMethod(services);

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -33,6 +33,8 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSLList;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Extracts called methods.
  *
@@ -43,35 +45,32 @@ public class MethodCallProofReferencesAnalyst implements IProofReferencesAnalyst
      * {@inheritDoc}
      */
     @Override
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
+    public @Nullable LinkedHashSet<IProofReference<?>> computeReferences(Node node,
+            Services services) {
         String name = MiscTools.getRuleName(node);
         if (name != null && name.toLowerCase().contains("methodcall")) {
             NodeInfo info = node.getNodeInfo();
-            if (info != null) {
-                if (info.getActiveStatement() instanceof MethodReference) {
-                    ExecutionContext context = extractContext(node, services);
-                    IProofReference<IProgramMethod> reference = createReference(node, services,
-                        context, (MethodReference) info.getActiveStatement());
-                    LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<>();
-                    result.add(reference);
-                    return result;
-                } else if (info.getActiveStatement() instanceof Assignment assignment) {
-                    ExecutionContext context = extractContext(node, services);
-                    LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<>();
-                    for (int i = 0; i < assignment.getChildCount(); i++) {
-                        ProgramElement child = assignment.getChildAt(i);
-                        if (child instanceof MethodReference) {
-                            IProofReference<IProgramMethod> reference =
-                                createReference(node, services, context, (MethodReference) child);
-                            ProofReferenceUtil.merge(result, reference);
-                        }
+            if (info.getActiveStatement() instanceof MethodReference) {
+                ExecutionContext context = extractContext(node, services);
+                IProofReference<IProgramMethod> reference = createReference(node, services,
+                    context, (MethodReference) info.getActiveStatement());
+                LinkedHashSet<IProofReference<?>> result =
+                    new LinkedHashSet<>();
+                result.add(reference);
+                return result;
+            } else if (info.getActiveStatement() instanceof Assignment assignment) {
+                ExecutionContext context = extractContext(node, services);
+                LinkedHashSet<IProofReference<?>> result =
+                    new LinkedHashSet<>();
+                for (int i = 0; i < assignment.getChildCount(); i++) {
+                    ProgramElement child = assignment.getChildAt(i);
+                    if (child instanceof MethodReference) {
+                        IProofReference<IProgramMethod> reference =
+                            createReference(node, services, context, (MethodReference) child);
+                        ProofReferenceUtil.merge(result, reference);
                     }
-                    return result;
-                } else {
-                    return null;
                 }
+                return result;
             } else {
                 return null;
             }

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -20,6 +20,8 @@
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Extracts read and write access to fields ({@link IProgramVariable}) via assignments.
  *
@@ -30,8 +32,9 @@ public class ProgramVariableReferencesAnalyst implements IProofReferencesAnalyst
      * {@inheritDoc}
      */
     @Override
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
-        if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
+    public @Nullable LinkedHashSet<IProofReference<?>> computeReferences(Node node,
+            Services services) {
+        if (node.getAppliedRuleApp() != null) {
             SourceElement statement = node.getNodeInfo().getActiveStatement();
             if (statement instanceof CopyAssignment) {
                 LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/package-info.java

@@ -0,0 +1,8 @@
+/**
+ * @author Alexander Weigl
+ * @version 1 (5/11/25)
+ */
+@NullMarked
+package de.uka.ilkd.key.proof_references.analyst;
+
+import org.jspecify.annotations.NullMarked;

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

@@ -0,0 +1,8 @@
+/**
+ * @author Alexander Weigl
+ * @version 1 (5/11/25)
+ */
+@NullMarked
+package de.uka.ilkd.key.proof_references;
+
+import org.jspecify.annotations.NullMarked;

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

@@ -12,6 +12,8 @@
 
 import org.key_project.util.Strings;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * Default implementation of {@link IProofReference}.
  *
@@ -26,7 +28,7 @@ public class DefaultProofReference<T> implements IProofReference<T> {
     /**
      * The source {@link Proof}.
      */
-    private final Proof source;
+    private final @Nullable Proof source;
 
     /**
      * The target source member.
@@ -45,7 +47,7 @@ public class DefaultProofReference<T> implements IProofReference<T> {
      * @param node Node to access the source {@link Proof} (or null).
      * @param target The target source member.
      */
-    public DefaultProofReference(String kind, Node node, T target) {
+    public DefaultProofReference(String kind, @Nullable Node node, T target) {
         this.kind = kind;
         this.source = node != null ? node.proof() : null;
         this.target = target;
@@ -88,15 +90,15 @@ public String getKind() {
      * {@inheritDoc}
      */
     @Override
-    public Proof getSource() {
+    public @Nullable Proof getSource() {
         return source;
     }
 
     /**
      * {@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.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/package-info.java

@@ -0,0 +1,8 @@
+/**
+ * @author Alexander Weigl
+ * @version 1 (5/11/25)
+ */
+@NullMarked
+package de.uka.ilkd.key.proof_references.reference;
+
+import org.jspecify.annotations.NullMarked;