nullness-specifying some more classes

with Werner and Alexander
KeYProject · Jun 27, 2023 · c880594 · c880594
1 parent 28ee001
commit c880594
Show file tree

Hide file tree

Showing 5 changed files with 40 additions and 27 deletions.
diff --git a/key.util/src/main/java/org/key_project/util/ExtList.java b/key.util/src/main/java/org/key_project/util/ExtList.java
@@ -15,7 +15,7 @@
  * Has facilities to get elements of a certain type ({@link #get(Class)}, {@link #collect(Class)}).
  */
 @NullMarked
-public class ExtList extends LinkedList<Object> {
+public final class ExtList extends LinkedList<Object> {
 
     private static final long serialVersionUID = 9182017368310263908L;
 

diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java
@@ -1,24 +1,28 @@
 package org.key_project.util.collection;
 
+import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
 import java.util.*;
 import java.util.function.Function;
 import java.util.function.Predicate;
 import java.util.stream.Collector;
 import java.util.stream.Stream;
 import java.util.stream.StreamSupport;
-import javax.annotation.Nonnull;
 
 /**
  * List interface to be implemented by non-destructive lists
  */
-public interface ImmutableList<T> extends Iterable<T>, java.io.Serializable {
+@NullMarked
+public interface ImmutableList<T extends @Nullable Object> extends Iterable<T>, java.io.Serializable {
 
     /**
      * Returns a Collector that accumulates the input elements into a new ImmutableList.
      *
      * @return a Collector that accumulates the input elements into a new ImmutableList.
      */
-    static <T> Collector<T, List<T>, ImmutableList<T>> collector() {
+    static <T extends @Nullable Object> Collector<T, List<T>, ImmutableList<T>> collector() {
         return Collector.of(LinkedList::new, List::add, (list1, list2) -> {
             list1.addAll(list2);
             return list1;
@@ -31,7 +35,7 @@ static <T> Collector<T, List<T>, ImmutableList<T>> collector() {
      * @param list a List.
      * @return an ImmutableList containing the same elements as the specified list.
      */
-    static <T> ImmutableList<T> fromList(Collection<T> list) {
+    static <T extends @Nullable Object> ImmutableList<T> fromList(Collection<T> list) {
         ImmutableList<T> result = ImmutableSLList.nil();
 
         for (T el : list) {
@@ -47,7 +51,7 @@ static <T> ImmutableList<T> fromList(Collection<T> list) {
      * @return empty immutable list.
      * @param <T> the entry type of the list.
      */
-    static <T> ImmutableList<T> of() {
+    static <T extends @Nullable Object> ImmutableList<T> of() {
         return ImmutableSLList.nil();
     }
 
@@ -58,7 +62,7 @@ static <T> ImmutableList<T> of() {
      * @return singleton immutable list.
      * @param <T> the entry type of the list.
      */
-    static <T> ImmutableList<T> of(T e1) {
+    static <T extends @Nullable Object> ImmutableList<T> of(T e1) {
         return ImmutableSLList.singleton(e1);
     }
 
@@ -71,7 +75,7 @@ static <T> ImmutableList<T> of(T e1) {
      * @return (e1, e2) as immutable list
      * @param <T> the entry type of the list.
      */
-    static <T> ImmutableList<T> of(T e1, T e2) {
+    static <T extends @Nullable Object> ImmutableList<T> of(T e1, T e2) {
         return ImmutableSLList.singleton(e2).prepend(e1);
     }
 
@@ -85,7 +89,7 @@ static <T> ImmutableList<T> of(T e1, T e2) {
      * @return (e1, e2, e3) as immutable list
      * @param <T> the entry type of the list.
      */
-    static <T> ImmutableList<T> of(T e1, T e2, T e3) {
+    static <T extends @Nullable Object> ImmutableList<T> of(T e1, T e2, T e3) {
         return ImmutableSLList.singleton(e3).prepend(e2).prepend(e1);
     }
 
@@ -97,7 +101,7 @@ static <T> ImmutableList<T> of(T e1, T e2, T e3) {
      * @return (e1, e2, e3, ...) as immutable list
      * @param <T> the entry type of the list.
      */
-    static <T> ImmutableList<T> of(T... es) {
+    static <T extends @Nullable Object> ImmutableList<T> of(T... es) {
         ImmutableList<T> result = ImmutableSLList.nil();
         for (int i = es.length - 1; i >= 0; i--) {
             result = result.prepend(es[i]);
@@ -178,15 +182,15 @@ static <T> ImmutableList<T> of(T... es) {
     /**
      * @return <T> the first element in list
      */
-    T head();
+    @Nullable T head();
 
     /**
      * return true if predicate is fullfilled for at least one element
      *
      * @param predicate the predicate
      * @return true if predicate is fullfilled for at least one element
      */
-    boolean exists(Predicate<T> predicate);
+    boolean exists(Predicate<? super T> predicate);
 
     /**
      * @return IList<T> tail of list
@@ -224,6 +228,7 @@ static <T> ImmutableList<T> of(T... es) {
     /**
      * @return true iff the list is empty
      */
+    @EnsuresNonNullIf(expression = {"head()"}, result = false)
     boolean isEmpty();
 
     /**
@@ -243,12 +248,12 @@ static <T> ImmutableList<T> of(T... es) {
     /**
      * Convert the list to a Java array (O(n))
      */
-    <S> S[] toArray(S[] array);
+    <S extends @Nullable Object> S[] toArray(S[] array);
 
     /**
      * Convert the list to a Java array (O(n))
      */
-    <S> S[] toArray(Class<S> type);
+    <S extends @Nullable Object> S[] toArray(Class<S> type);
 
 
     /**
@@ -283,7 +288,7 @@ default List<T> toList() {
      *
      * @returns the filtered list
      */
-    default @Nonnull ImmutableList<T> filter(@Nonnull Predicate<T> predicate) {
+    default ImmutableList<T> filter(Predicate<? super T> predicate) {
         return Immutables.filter(this, predicate);
     }
 
@@ -295,15 +300,15 @@ default List<T> toList() {
      * @param function a non-interfering, stateless function to apply to each element
      * @return the mapped list of the same length as this
      */
-    default <R> ImmutableList<R> map(Function<T, R> function) {
+    default <R extends @Nullable Object> ImmutableList<R> map(Function<? super T, R> function) {
         return Immutables.map(this, function);
     }
 
     /**
      * @param other prefix to check for
      * @return whether this list starts with the elements of the provided prefix
      */
-    default boolean hasPrefix(ImmutableList<T> other) {
+    default boolean hasPrefix(ImmutableList<? extends T> other) {
         if (other.size() > this.size()) {
             return false;
         }
@@ -324,7 +329,7 @@ default boolean hasPrefix(ImmutableList<T> other) {
      * @return new list with the prefix removed
      * @throws IllegalArgumentException if the provided prefix is not a prefix of this list
      */
-    default ImmutableList<T> stripPrefix(ImmutableList<T> prefix) {
+    default ImmutableList<T> stripPrefix(ImmutableList<? extends T> prefix) {
         if (prefix.isEmpty()) {
             return this;
         }
@@ -348,7 +353,9 @@ default T last() {
         while (!remainder.tail().isEmpty()) {
             remainder = remainder.tail();
         }
-        return remainder.head();
+        T result = remainder.head();
+        assert result != null : "@AssumeAssertion(nullness): this should never be null";
+        return result;
     }
 
 }
diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java
@@ -259,7 +259,7 @@ public ImmutableList<S> prependReverse(ImmutableList<S> list) {
          * @return true if predicate is fullfilled for at least one element
          */
         @Override
-        public boolean exists(Predicate<S> predicate) {
+        public boolean exists(Predicate<? super S> predicate) {
             ImmutableList<S> list = this;
             while (!list.isEmpty()) {
                 if (predicate.test(list.head())) {
@@ -584,7 +584,7 @@ public boolean contains(S obj) {
          * @return true if predicate is fullfilled for at least one element
          */
         @Override
-        public boolean exists(Predicate<S> predicate) {
+        public boolean exists(Predicate<? super S> predicate) {
             return false;
         }
 

diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java
@@ -1,5 +1,8 @@
 package org.key_project.util.collection;
 
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
 import java.util.HashSet;
 import java.util.Set;
 import java.util.function.Function;
@@ -13,7 +16,7 @@
  *
  * @author Mattias Ulbrich
  */
-@SuppressWarnings("nullness")
+@NullMarked
 public final class Immutables {
 
     private Immutables() {
@@ -61,7 +64,7 @@ public static <T> boolean isDuplicateFree(ImmutableList<T> list) {
      * The implementation uses a hash set internally and thus runs in O(n).
      *
      * It reuses as much created datastructure as possible. In particular, if the list is already
-     * duplicate-fre, it does not allocate new memory (well, only temporarily) and returns the
+     * duplicate-free, it does not allocate new memory (well, only temporarily) and returns the
      * argument.
      *
      * Sidenote: Would that not make a nice KeY-Verification condition? Eat your own dogfood.
@@ -88,6 +91,7 @@ public static <T> ImmutableList<T> removeDuplicates(ImmutableList<T> list) {
 
         while (!stack.isEmpty()) {
             ImmutableList<T> top = stack.head();
+            assert !top.isEmpty() : "@AssumeAssertion(nullness)";
             T element = top.head();
             stack = stack.tail();
             if (alreadySeen.contains(element)) {
@@ -100,6 +104,7 @@ public static <T> ImmutableList<T> removeDuplicates(ImmutableList<T> list) {
 
         while (!stack.isEmpty()) {
             ImmutableList<T> top = stack.head();
+            assert !top.isEmpty() : "@AssumeAssertion(nullness)";
             T element = top.head();
             stack = stack.tail();
             if (!alreadySeen.contains(element)) {
@@ -165,11 +170,11 @@ public static <T> ImmutableList<T> createListFrom(Iterable<T> iterable) {
      *
      * @returns the filtered list
      */
-    public static <T> ImmutableList<T> filter(ImmutableList<T> ts, Predicate<T> predicate) {
+    public static <T extends @Nullable Object> ImmutableList<T> filter(ImmutableList<T> ts, Predicate<? super T> predicate) {
         // This must be a loop. A tail recursive implementation is not optimised
         // by the compiler and quickly leads to a stack overlow.
         ImmutableList<T> acc = ImmutableSLList.nil();
-        while (ts.size() > 0) {
+        while (!ts.isEmpty()) {
             T hd = ts.head();
             if (predicate.test(hd)) {
                 acc = acc.prepend(hd);
@@ -188,11 +193,11 @@ public static <T> ImmutableList<T> filter(ImmutableList<T> ts, Predicate<T> pred
      * @param function a non-interfering, stateless function to apply to each element
      * @return the mapped list of the same length as this
      */
-    public static <T, R> ImmutableList<R> map(ImmutableList<T> ts, Function<T, R> function) {
+    public static <T extends @Nullable Object, R extends @Nullable Object> ImmutableList<R> map(ImmutableList<T> ts, Function<? super T, R> function) {
         // This must be a loop. A tail recursive implementation is not optimised
         // by the compiler and quickly leads to a stack overlow.
         ImmutableList<R> acc = ImmutableSLList.nil();
-        while (ts.size() > 0) {
+        while (!ts.isEmpty()) {
             T hd = ts.head();
             acc = acc.prepend(function.apply(hd));
             ts = ts.tail();

diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java
@@ -745,6 +745,7 @@ public static boolean exists(File file) {
         return file != null ? file.toString() : null;
     }
 
+    @SuppressWarnings("nullness")
     public static @Nullable URI toURI(@Nullable URL url) {
         try {
             if (url != null) {