From 84b127276d15bfb6d05e5b0e9e3b19e24acece4e Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 27 Jun 2023 14:59:10 +0200 Subject: [PATCH] nullness-specifying some more classes with Werner and Alexander --- .../java/org/key_project/util/ExtList.java | 2 +- .../util/collection/ImmutableList.java | 43 +++++++++++-------- .../util/collection/ImmutableSLList.java | 4 +- .../util/collection/Immutables.java | 13 ++++-- .../org/key_project/util/java/IOUtil.java | 1 + 5 files changed, 38 insertions(+), 25 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 index 5ef551fd969..f5836deb338 100644 --- 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 { +public final class ExtList extends LinkedList { 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 index 0b9aaceabe4..aeb853c3a95 100644 --- 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 extends Iterable, java.io.Serializable { +@NullMarked +public interface ImmutableList extends Iterable, 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 Collector, ImmutableList> collector() { + static Collector, ImmutableList> collector() { return Collector.of(LinkedList::new, List::add, (list1, list2) -> { list1.addAll(list2); return list1; @@ -31,7 +35,7 @@ static Collector, ImmutableList> collector() { * @param list a List. * @return an ImmutableList containing the same elements as the specified list. */ - static ImmutableList fromList(Collection list) { + static ImmutableList fromList(Collection list) { ImmutableList result = ImmutableSLList.nil(); for (T el : list) { @@ -47,7 +51,7 @@ static ImmutableList fromList(Collection list) { * @return empty immutable list. * @param the entry type of the list. */ - static ImmutableList of() { + static ImmutableList of() { return ImmutableSLList.nil(); } @@ -58,7 +62,7 @@ static ImmutableList of() { * @return singleton immutable list. * @param the entry type of the list. */ - static ImmutableList of(T e1) { + static ImmutableList of(T e1) { return ImmutableSLList.singleton(e1); } @@ -71,7 +75,7 @@ static ImmutableList of(T e1) { * @return (e1, e2) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T e1, T e2) { + static ImmutableList of(T e1, T e2) { return ImmutableSLList.singleton(e2).prepend(e1); } @@ -85,7 +89,7 @@ static ImmutableList of(T e1, T e2) { * @return (e1, e2, e3) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T e1, T e2, T e3) { + static ImmutableList of(T e1, T e2, T e3) { return ImmutableSLList.singleton(e3).prepend(e2).prepend(e1); } @@ -97,7 +101,7 @@ static ImmutableList of(T e1, T e2, T e3) { * @return (e1, e2, e3, ...) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T... es) { + static ImmutableList of(T... es) { ImmutableList result = ImmutableSLList.nil(); for (int i = es.length - 1; i >= 0; i--) { result = result.prepend(es[i]); @@ -178,7 +182,7 @@ static ImmutableList of(T... es) { /** * @return the first element in list */ - T head(); + @Nullable T head(); /** * return true if predicate is fullfilled for at least one element @@ -186,7 +190,7 @@ static ImmutableList of(T... es) { * @param predicate the predicate * @return true if predicate is fullfilled for at least one element */ - boolean exists(Predicate predicate); + boolean exists(Predicate predicate); /** * @return IList tail of list @@ -224,6 +228,7 @@ static ImmutableList of(T... es) { /** * @return true iff the list is empty */ + @EnsuresNonNullIf(expression = {"head()"}, result = false) boolean isEmpty(); /** @@ -243,12 +248,12 @@ static ImmutableList of(T... es) { /** * Convert the list to a Java array (O(n)) */ - S[] toArray(S[] array); + S[] toArray(S[] array); /** * Convert the list to a Java array (O(n)) */ - S[] toArray(Class type); + S[] toArray(Class type); /** @@ -283,7 +288,7 @@ default List toList() { * * @returns the filtered list */ - default @Nonnull ImmutableList filter(@Nonnull Predicate predicate) { + default ImmutableList filter(Predicate predicate) { return Immutables.filter(this, predicate); } @@ -295,7 +300,7 @@ default List toList() { * @param function a non-interfering, stateless function to apply to each element * @return the mapped list of the same length as this */ - default ImmutableList map(Function function) { + default ImmutableList map(Function function) { return Immutables.map(this, function); } @@ -303,7 +308,7 @@ default ImmutableList map(Function function) { * @param other prefix to check for * @return whether this list starts with the elements of the provided prefix */ - default boolean hasPrefix(ImmutableList other) { + default boolean hasPrefix(ImmutableList other) { if (other.size() > this.size()) { return false; } @@ -324,7 +329,7 @@ default boolean hasPrefix(ImmutableList other) { * @return new list with the prefix removed * @throws IllegalArgumentException if the provided prefix is not a prefix of this list */ - default ImmutableList stripPrefix(ImmutableList prefix) { + default ImmutableList stripPrefix(ImmutableList 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 index e1bab0f04f2..21e9e74f989 100644 --- 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 prependReverse(ImmutableList list) { * @return true if predicate is fullfilled for at least one element */ @Override - public boolean exists(Predicate predicate) { + public boolean exists(Predicate predicate) { ImmutableList 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 predicate) { + public boolean exists(Predicate 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 index b37b1c36729..a3983c31427 100644 --- 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 boolean isDuplicateFree(ImmutableList 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 ImmutableList removeDuplicates(ImmutableList list) { while (!stack.isEmpty()) { ImmutableList 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 ImmutableList removeDuplicates(ImmutableList list) { while (!stack.isEmpty()) { ImmutableList top = stack.head(); + assert !top.isEmpty() : "@AssumeAssertion(nullness)"; T element = top.head(); stack = stack.tail(); if (!alreadySeen.contains(element)) { @@ -165,7 +170,7 @@ public static ImmutableList createListFrom(Iterable iterable) { * * @returns the filtered list */ - public static ImmutableList filter(ImmutableList ts, Predicate predicate) { + public static ImmutableList filter(ImmutableList ts, Predicate predicate) { // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); @@ -188,7 +193,7 @@ public static ImmutableList filter(ImmutableList ts, Predicate 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 ImmutableList map(ImmutableList ts, Function function) { + public static ImmutableList map(ImmutableList ts, Function function) { // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); 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 index fe320f56351..47ab20593c6 100644 --- 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) {