Add Optional annotations for primitive numeric Optional wrappers

mernst · web-flow · commit 2e95e326158c · 2023-10-21T08:47:22.000-07:00
diff --git a/src/java.base/share/classes/java/util/OptionalDouble.java b/src/java.base/share/classes/java/util/OptionalDouble.java
@@ -27,9 +27,13 @@
 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.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;
@@ -62,9 +66,9 @@
  *
  * @since 1.8
  */
-@AnnotatedFor({"lock", "nullness"})
+@AnnotatedFor({"lock", "nullness", "optional"})
 @jdk.internal.ValueBased
-public final class OptionalDouble {
+public final @NonNull class OptionalDouble {
     /**
      * Common instance for {@code empty()}.
      */
@@ -120,7 +124,8 @@ private OptionalDouble(double value) {
      * @param value the value to describe
      * @return an {@code OptionalDouble} with the value present
      */
-    public static OptionalDouble of(double value) {
+    @SideEffectFree
+    public static @Present OptionalDouble of(double value) {
         return new OptionalDouble(value);
     }
 
@@ -134,7 +139,8 @@ public static OptionalDouble of(double value) {
      * @return the value described by this {@code OptionalDouble}
      * @throws NoSuchElementException if no value is present
      */
-    public double getAsDouble() {
+    @Pure
+    public double getAsDouble(@Present OptionalDouble this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -146,6 +152,8 @@ public double getAsDouble() {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @Pure
+    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
     public boolean isPresent() {
         return isPresent;
     }
@@ -158,6 +166,7 @@ public boolean isPresent() {
      * @since   11
      */
     @Pure
+    @EnsuresQualifierIf(result = false, expression = "this", qualifier = Present.class)
     public boolean isEmpty() {
         return !isPresent;
     }
@@ -212,6 +221,7 @@ public void ifPresentOrElse(DoubleConsumer action, Runnable emptyAction) {
      * @return the optional value as a {@code DoubleStream}
      * @since 9
      */
+    @SideEffectFree
     public DoubleStream stream() {
         if (isPresent) {
             return DoubleStream.of(value);
@@ -253,7 +263,9 @@ public double orElseGet(DoubleSupplier supplier) {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
-    public double orElseThrow() {
+    @Pure
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    public double orElseThrow(@Present OptionalDouble this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -277,6 +289,7 @@ public double orElseThrow() {
      * @throws NullPointerException if no value is present and the exception
      *         supplying function is {@code null}
      */
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
     public<X extends Throwable> double orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (isPresent) {
             return value;
@@ -320,6 +333,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @Pure
     @Override
     public int hashCode() {
         return isPresent ? Double.hashCode(value) : 0;
diff --git a/src/java.base/share/classes/java/util/OptionalInt.java b/src/java.base/share/classes/java/util/OptionalInt.java
@@ -27,9 +27,12 @@
 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.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;
@@ -62,9 +65,9 @@
  *
  * @since 1.8
  */
-@AnnotatedFor({"lock", "nullness"})
+@AnnotatedFor({"lock", "nullness", "optional"})
 @jdk.internal.ValueBased
-public final class OptionalInt {
+public final @NonNull class OptionalInt {
     /**
      * Common instance for {@code empty()}.
      */
@@ -120,7 +123,8 @@ private OptionalInt(int value) {
      * @param value the value to describe
      * @return an {@code OptionalInt} with the value present
      */
-    public static OptionalInt of(int value) {
+    @SideEffectFree
+    public static @Present OptionalInt of(int value) {
         return new OptionalInt(value);
     }
 
@@ -134,7 +138,8 @@ public static OptionalInt of(int value) {
      * @return the value described by this {@code OptionalInt}
      * @throws NoSuchElementException if no value is present
      */
-    public int getAsInt() {
+    @Pure
+    public int getAsInt(@Present OptionalInt this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -146,6 +151,8 @@ public int getAsInt() {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @Pure
+    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
     public boolean isPresent() {
         return isPresent;
     }
@@ -158,6 +165,7 @@ public boolean isPresent() {
      * @since   11
      */
     @Pure
+    @EnsuresQualifierIf(result = false, expression = "this", qualifier = Present.class)
     public boolean isEmpty() {
         return !isPresent;
     }
@@ -211,6 +219,7 @@ public void ifPresentOrElse(IntConsumer action, Runnable emptyAction) {
      * @return the optional value as an {@code IntStream}
      * @since 9
      */
+    @SideEffectFree
     public IntStream stream() {
         if (isPresent) {
             return IntStream.of(value);
@@ -252,7 +261,9 @@ public int orElseGet(IntSupplier supplier) {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
-    public int orElseThrow() {
+    @Pure
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    public int orElseThrow(@Present OptionalInt this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -276,6 +287,7 @@ public int orElseThrow() {
      * @throws NullPointerException if no value is present and the exception
      *         supplying function is {@code null}
      */
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
     public<X extends Throwable> int orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (isPresent) {
             return value;
@@ -318,6 +330,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @Pure
     @Override
     public int hashCode() {
         return isPresent ? Integer.hashCode(value) : 0;
diff --git a/src/java.base/share/classes/java/util/OptionalLong.java b/src/java.base/share/classes/java/util/OptionalLong.java
@@ -27,9 +27,12 @@
 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.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.LongConsumer;
 import java.util.function.LongSupplier;
@@ -62,9 +65,9 @@
  *
  * @since 1.8
  */
-@AnnotatedFor({"lock", "nullness"})
+@AnnotatedFor({"lock", "nullness", "optional"})
 @jdk.internal.ValueBased
-public final class OptionalLong {
+public final @NonNull class OptionalLong {
     /**
      * Common instance for {@code empty()}.
      */
@@ -120,7 +123,8 @@ private OptionalLong(long value) {
      * @param value the value to describe
      * @return an {@code OptionalLong} with the value present
      */
-    public static OptionalLong of(long value) {
+    @SideEffectFree
+    public static @Present OptionalLong of(long value) {
         return new OptionalLong(value);
     }
 
@@ -134,7 +138,8 @@ public static OptionalLong of(long value) {
      * @return the value described by this {@code OptionalLong}
      * @throws NoSuchElementException if no value is present
      */
-    public long getAsLong() {
+    @Pure
+    public long getAsLong(@Present OptionalLong this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -146,6 +151,8 @@ public long getAsLong() {
      *
      * @return {@code true} if a value is present, otherwise {@code false}
      */
+    @Pure
+    @EnsuresQualifierIf(result = true, expression = "this", qualifier = Present.class)
     public boolean isPresent() {
         return isPresent;
     }
@@ -158,6 +165,7 @@ public boolean isPresent() {
      * @since   11
      */
     @Pure
+    @EnsuresQualifierIf(result = false, expression = "this", qualifier = Present.class)
     public boolean isEmpty() {
         return !isPresent;
     }
@@ -211,6 +219,7 @@ public void ifPresentOrElse(LongConsumer action, Runnable emptyAction) {
      * @return the optional value as an {@code LongStream}
      * @since 9
      */
+    @SideEffectFree
     public LongStream stream() {
         if (isPresent) {
             return LongStream.of(value);
@@ -252,7 +261,9 @@ public long orElseGet(LongSupplier supplier) {
      * @throws NoSuchElementException if no value is present
      * @since 10
      */
-    public long orElseThrow() {
+    @Pure
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
+    public long orElseThrow(@Present OptionalLong this) {
         if (!isPresent) {
             throw new NoSuchElementException("No value present");
         }
@@ -276,6 +287,7 @@ public long orElseThrow() {
      * @throws NullPointerException if no value is present and the exception
      *         supplying function is {@code null}
      */
+    @EnsuresQualifier(expression = "this", qualifier = Present.class)
     public<X extends Throwable> long orElseThrow(Supplier<? extends X> exceptionSupplier) throws X {
         if (isPresent) {
             return value;
@@ -318,6 +330,7 @@ public boolean equals(@Nullable Object obj) {
      * @return hash code value of the present value or {@code 0} if no value is
      *         present
      */
+    @Pure
     @Override
     public int hashCode() {
         return isPresent ? Long.hashCode(value) : 0;
