Update to EISOP 3.42-eisop1 from 3.41-eisop1 (eisop#9)

Ao-senXiong · Apr 21, 2024 · c160ca7 · c160ca7
2 parents f1cf8b9 + 2408d94
commit c160ca7
Show file tree

Hide file tree

Showing 237 changed files with 2,340 additions and 1,872 deletions.
diff --git a/src/java.base/share/classes/java/util/Optional.java b/src/java.base/share/classes/java/util/Optional.java
@@ -28,14 +28,17 @@
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
+import org.checkerframework.checker.optional.qual.EnsuresPresent;
 import org.checkerframework.checker.optional.qual.EnsuresPresentIf;
+import org.checkerframework.checker.optional.qual.OptionalCreator;
+import org.checkerframework.checker.optional.qual.OptionalEliminator;
+import org.checkerframework.checker.optional.qual.OptionalPropagator;
 import org.checkerframework.checker.optional.qual.Present;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.CFComment;
 import org.checkerframework.framework.qual.Covariant;
-import org.checkerframework.framework.qual.EnsuresQualifier;
 
 import java.util.function.Consumer;
 import java.util.function.Function;
@@ -109,6 +112,7 @@
      * @param <T> The type of the non-existent value
      * @return an empty {@code Optional}
      */
+    @OptionalCreator
     @Pure
     public static<T> Optional<T> empty() {
         @SuppressWarnings("unchecked")
@@ -136,6 +140,7 @@ private Optional(@NonNull T value) {
      * @return an {@code Optional} with the value present
      * @throws NullPointerException if value is {@code null}
      */
+    @OptionalCreator
     @SideEffectFree
     public static <T> @Present Optional<T> of(@NonNull T value) {
         return new Optional<>(Objects.requireNonNull(value));
@@ -150,6 +155,7 @@ private Optional(@NonNull T value) {
      * @return an {@code Optional} with a present value if the specified value
      *         is non-{@code null}, otherwise an empty {@code Optional}
      */
+    @OptionalCreator
     @SideEffectFree
     @SuppressWarnings("unchecked")
     public static <T> Optional<@NonNull T> ofNullable(@Nullable T value) {
@@ -167,6 +173,7 @@ private Optional(@NonNull T value) {
      * @return the non-{@code null} value described by this {@code Optional}
      * @throws NoSuchElementException if no value is present
      */
+    @OptionalEliminator
     @Pure
     public @NonNull T get(@Present Optional<T> this) {
         if (value == null) {
@@ -180,6 +187,7 @@ private Optional(@NonNull T value) {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @OptionalEliminator
     @Pure
     @EnsuresPresentIf(result = true, expression = "this")
     public boolean isPresent() {
@@ -207,6 +215,7 @@ public boolean isEmpty() {
      * @throws NullPointerException if value is present and the given action is
      *         {@code null}
      */
+    @OptionalEliminator
     public void ifPresent(Consumer<? super T> action) {
         if (value != null) {
             action.accept(value);
@@ -225,6 +234,7 @@ public void ifPresent(Consumer<? super T> action) {
      *         action is {@code null}.
      * @since 9
      */
+    @OptionalEliminator
     public void ifPresentOrElse(Consumer<? super T> action, Runnable emptyAction) {
         if (value != null) {
             action.accept(value);
@@ -244,6 +254,7 @@ public void ifPresentOrElse(Consumer<? super T> action, Runnable emptyAction) {
      *         given predicate, otherwise an empty {@code Optional}
      * @throws NullPointerException if the predicate is {@code null}
      */
+    @OptionalPropagator
     public Optional<T> filter(Predicate<? super T> predicate) {
         Objects.requireNonNull(predicate);
         if (!isPresent()) {
@@ -286,6 +297,7 @@ public Optional<T> filter(Predicate<? super T> predicate) {
      *         present, otherwise an empty {@code Optional}
      * @throws NullPointerException if the mapping function is {@code null}
      */
+    @OptionalPropagator
     public <U> Optional<U> map(Function<? super T, ? extends @Nullable U> mapper) {
         Objects.requireNonNull(mapper);
         if (!isPresent()) {
@@ -314,6 +326,7 @@ public <U> Optional<U> map(Function<? super T, ? extends @Nullable U> mapper) {
      * @throws NullPointerException if the mapping function is {@code null} or
      *         returns a {@code null} result
      */
+    @OptionalPropagator
     public <U> Optional<U> flatMap(Function<? super T, ? extends Optional<? extends U>> mapper) {
         Objects.requireNonNull(mapper);
         if (!isPresent()) {
@@ -338,6 +351,7 @@ public <U> Optional<U> flatMap(Function<? super T, ? extends Optional<? extends
      *         produces a {@code null} result
      * @since 9
      */
+    @OptionalPropagator
     public Optional<T> or(Supplier<? extends Optional<? extends T>> supplier) {
         Objects.requireNonNull(supplier);
         if (isPresent()) {
@@ -381,6 +395,7 @@ public Stream<T> stream() {
      *        May be {@code null}.
      * @return the value, if present, otherwise {@code other}
      */
+    @OptionalEliminator
     @Pure
     public @PolyNull T orElse(@PolyNull T other) {
         return value != null ? value : other;
@@ -396,6 +411,7 @@ public Stream<T> stream() {
      * @throws NullPointerException if no value is present and the supplying
      *         function is {@code null}
      */
+    @OptionalEliminator
     public @PolyNull T orElseGet(Supplier<? extends @PolyNull T> supplier) {
         return value != null ? value : supplier.get();
     }
@@ -408,8 +424,9 @@ public Stream<T> stream() {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
+    @OptionalEliminator
     @Pure
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @EnsuresPresent("this")
     public @NonNull T orElseThrow(@Present Optional<T> this) {
         if (value == null) {
             throw new NoSuchElementException("No value present");
@@ -436,7 +453,8 @@ public Stream<T> stream() {
      */
     @CFComment({"optional: orElseThrow(Supplier) does not throw NoSuchElementException, so its receiver is @MaybePresent.",
                 "Contrast with orElseThrow(), defined just above, whose receiver is @Present."})
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @EnsuresPresent("this")
+    @OptionalEliminator
     public <X extends Throwable> @NonNull T orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (value != null) {
             return value;
@@ -477,6 +495,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @OptionalEliminator
     @Pure
     @Override
     public int hashCode() {

diff --git a/src/java.base/share/classes/java/util/OptionalDouble.java b/src/java.base/share/classes/java/util/OptionalDouble.java
@@ -27,13 +27,14 @@
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.optional.qual.EnsuresPresent;
+import org.checkerframework.checker.optional.qual.EnsuresPresentIf;
+import org.checkerframework.checker.optional.qual.OptionalCreator;
+import org.checkerframework.checker.optional.qual.OptionalEliminator;
 import org.checkerframework.checker.optional.qual.Present;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
-import org.checkerframework.framework.qual.EnsuresQualifier;
-import org.checkerframework.framework.qual.EnsuresQualifierIf;
-
 
 import java.util.function.DoubleConsumer;
 import java.util.function.DoubleSupplier;
@@ -103,6 +104,7 @@ private OptionalDouble() {
      *
      *  @return an empty {@code OptionalDouble}.
      */
+    @OptionalCreator
     @SideEffectFree
     public static OptionalDouble empty() {
         return EMPTY;
@@ -124,6 +126,7 @@ private OptionalDouble(double value) {
      * @param value the value to describe
      * @return an {@code OptionalDouble} with the value present
      */
+    @OptionalCreator
     @SideEffectFree
     public static @Present OptionalDouble of(double value) {
         return new OptionalDouble(value);
@@ -139,6 +142,7 @@ private OptionalDouble(double value) {
      * @return the value described by this {@code OptionalDouble}
      * @throws NoSuchElementException if no value is present
      */
+    @OptionalEliminator
     @Pure
     public double getAsDouble(@Present OptionalDouble this) {
         if (!isPresent) {
@@ -152,8 +156,9 @@ public double getAsDouble(@Present OptionalDouble this) {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @OptionalEliminator
     @Pure
-    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
+    @EnsuresPresentIf(result = true, expression = "this")
     public boolean isPresent() {
         return isPresent;
     }
@@ -166,7 +171,7 @@ public boolean isPresent() {
      * @since   11
      */
     @Pure
-    @EnsuresQualifierIf(result = false, expression = "this", qualifier = Present.class)
+    @EnsuresPresentIf(result = false, expression = "this")
     public boolean isEmpty() {
         return !isPresent;
     }
@@ -179,6 +184,7 @@ public boolean isEmpty() {
      * @throws NullPointerException if value is present and the given action is
      *         {@code null}
      */
+    @OptionalEliminator
     public void ifPresent(DoubleConsumer action) {
         if (isPresent) {
             action.accept(value);
@@ -197,6 +203,7 @@ public void ifPresent(DoubleConsumer action) {
      *         action is {@code null}.
      * @since 9
      */
+    @OptionalEliminator
     public void ifPresentOrElse(DoubleConsumer action, Runnable emptyAction) {
         if (isPresent) {
             action.accept(value);
@@ -237,6 +244,7 @@ public DoubleStream stream() {
      * @param other the value to be returned, if no value is present
      * @return the value, if present, otherwise {@code other}
      */
+    @OptionalEliminator
     public double orElse(double other) {
         return isPresent ? value : other;
     }
@@ -251,6 +259,7 @@ public double orElse(double other) {
      * @throws NullPointerException if no value is present and the supplying
      *         function is {@code null}
      */
+    @OptionalEliminator
     public double orElseGet(DoubleSupplier supplier) {
         return isPresent ? value : supplier.getAsDouble();
     }
@@ -263,8 +272,9 @@ public double orElseGet(DoubleSupplier supplier) {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
+    @OptionalEliminator
     @Pure
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @EnsuresPresent("this")
     public double orElseThrow(@Present OptionalDouble this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
@@ -289,7 +299,8 @@ public double orElseThrow(@Present OptionalDouble this) {
      * @throws NullPointerException if no value is present and the exception
      *         supplying function is {@code null}
      */
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @OptionalEliminator
+    @EnsuresPresent("this")
     public<X extends Throwable> double orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (isPresent) {
             return value;
@@ -333,6 +344,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @OptionalEliminator
     @Pure
     @Override
     public int hashCode() {

diff --git a/src/java.base/share/classes/java/util/OptionalInt.java b/src/java.base/share/classes/java/util/OptionalInt.java
@@ -27,12 +27,14 @@
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.optional.qual.EnsuresPresent;
+import org.checkerframework.checker.optional.qual.EnsuresPresentIf;
+import org.checkerframework.checker.optional.qual.OptionalCreator;
+import org.checkerframework.checker.optional.qual.OptionalEliminator;
 import org.checkerframework.checker.optional.qual.Present;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
-import org.checkerframework.framework.qual.EnsuresQualifier;
-import org.checkerframework.framework.qual.EnsuresQualifierIf;
 
 import java.util.function.IntConsumer;
 import java.util.function.IntSupplier;
@@ -102,6 +104,7 @@ private OptionalInt() {
      *
      * @return an empty {@code OptionalInt}
      */
+    @OptionalCreator
     @SideEffectFree
     public static OptionalInt empty() {
         return EMPTY;
@@ -123,6 +126,7 @@ private OptionalInt(int value) {
      * @param value the value to describe
      * @return an {@code OptionalInt} with the value present
      */
+    @OptionalCreator
     @SideEffectFree
     public static @Present OptionalInt of(int value) {
         return new OptionalInt(value);
@@ -138,6 +142,7 @@ private OptionalInt(int value) {
      * @return the value described by this {@code OptionalInt}
      * @throws NoSuchElementException if no value is present
      */
+    @OptionalEliminator
     @Pure
     public int getAsInt(@Present OptionalInt this) {
         if (!isPresent) {
@@ -151,8 +156,9 @@ public int getAsInt(@Present OptionalInt this) {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @OptionalEliminator
     @Pure
-    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
+    @EnsuresPresentIf(result = true, expression = "this")
     public boolean isPresent() {
         return isPresent;
     }
@@ -165,7 +171,7 @@ public boolean isPresent() {
      * @since   11
      */
     @Pure
-    @EnsuresQualifierIf(result = false, expression = "this", qualifier = Present.class)
+    @EnsuresPresentIf(result = false, expression = "this")
     public boolean isEmpty() {
         return !isPresent;
     }
@@ -178,6 +184,7 @@ public boolean isEmpty() {
      * @throws NullPointerException if value is present and the given action is
      *         {@code null}
      */
+    @OptionalEliminator
     public void ifPresent(IntConsumer action) {
         if (isPresent) {
             action.accept(value);
@@ -196,6 +203,7 @@ public void ifPresent(IntConsumer action) {
      *         action is {@code null}.
      * @since 9
      */
+    @OptionalEliminator
     public void ifPresentOrElse(IntConsumer action, Runnable emptyAction) {
         if (isPresent) {
             action.accept(value);
@@ -235,6 +243,7 @@ public IntStream stream() {
      * @param other the value to be returned, if no value is present
      * @return the value, if present, otherwise {@code other}
      */
+    @OptionalEliminator
     public int orElse(int other) {
         return isPresent ? value : other;
     }
@@ -249,6 +258,7 @@ public int orElse(int other) {
      * @throws NullPointerException if no value is present and the supplying
      *         function is {@code null}
      */
+    @OptionalEliminator
     public int orElseGet(IntSupplier supplier) {
         return isPresent ? value : supplier.getAsInt();
     }
@@ -261,8 +271,9 @@ public int orElseGet(IntSupplier supplier) {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
+    @OptionalEliminator
     @Pure
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @EnsuresPresent("this")
     public int orElseThrow(@Present OptionalInt this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
@@ -287,7 +298,8 @@ public int orElseThrow(@Present OptionalInt this) {
      * @throws NullPointerException if no value is present and the exception
      *         supplying function is {@code null}
      */
-    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    @EnsuresPresent("this")
+    @OptionalEliminator
     public<X extends Throwable> int orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (isPresent) {
             return value;
@@ -330,6 +342,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @OptionalEliminator
     @Pure
     @Override
     public int hashCode() {