From 47ca0c6a8d053b244ee389742190aa7b5821e7a6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 25 May 2026 21:42:23 -0700 Subject: [PATCH 1/4] Add side effect annotations --- .../share/classes/java/lang/Math.java | 135 +++++++++++++- .../share/classes/java/lang/StrictMath.java | 175 ++++++++++++++++++ .../share/classes/java/math/BigInteger.java | 45 ++++- .../classes/java/util/AbstractCollection.java | 2 + .../share/classes/java/util/AbstractList.java | 6 + .../java/util/AbstractSequentialList.java | 3 + .../share/classes/java/util/ArrayDeque.java | 4 + .../share/classes/java/util/ArrayList.java | 11 +- .../share/classes/java/util/Arrays.java | 18 ++ .../share/classes/java/util/BitSet.java | 3 + .../share/classes/java/util/Collections.java | 26 ++- .../classes/java/util/ComparableTimSort.java | 2 + .../classes/java/util/DualPivotQuicksort.java | 13 ++ .../share/classes/java/util/HashSet.java | 1 - .../classes/java/util/LinkedHashSet.java | 5 + .../share/classes/java/util/LinkedList.java | 7 + .../share/classes/java/util/List.java | 8 +- .../share/classes/java/util/ListIterator.java | 2 + .../share/classes/java/util/NavigableSet.java | 5 + .../java/util/ReverseOrderDequeView.java | 9 + .../java/util/ReverseOrderListView.java | 4 + .../java/util/ReverseOrderSortedSetView.java | 5 + .../java/util/SequencedCollection.java | 5 + .../share/classes/java/util/Set.java | 12 ++ .../share/classes/java/util/SortedSet.java | 5 + .../share/classes/java/util/TreeSet.java | 6 + .../share/classes/java/util/Vector.java | 3 +- .../java/util/concurrent/BlockingDeque.java | 4 +- .../concurrent/ConcurrentLinkedDeque.java | 4 + .../concurrent/ConcurrentSkipListSet.java | 10 + .../util/concurrent/CopyOnWriteArrayList.java | 12 ++ .../util/concurrent/LinkedBlockingDeque.java | 4 + 32 files changed, 543 insertions(+), 11 deletions(-) diff --git a/src/java.base/share/classes/java/lang/Math.java b/src/java.base/share/classes/java/lang/Math.java index ed9a8899556fc..42a9057dd7db2 100644 --- a/src/java.base/share/classes/java/lang/Math.java +++ b/src/java.base/share/classes/java/lang/Math.java @@ -191,6 +191,7 @@ private Math() {} * @return the sine of the argument. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double sin(double a) { return StrictMath.sin(a); // default impl. delegates to StrictMath @@ -210,6 +211,7 @@ public static double sin(double a) { * @return the cosine of the argument. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double cos(double a) { return StrictMath.cos(a); // default impl. delegates to StrictMath @@ -229,6 +231,7 @@ public static double cos(double a) { * @return the tangent of the argument. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double tan(double a) { return StrictMath.tan(a); // default impl. delegates to StrictMath @@ -249,6 +252,7 @@ public static double tan(double a) { * @return the arc sine of the argument. */ @Pure + @StaticallyExecutable public static double asin(double a) { return StrictMath.asin(a); // default impl. delegates to StrictMath } @@ -268,6 +272,7 @@ public static double asin(double a) { * @return the arc cosine of the argument. */ @Pure + @StaticallyExecutable public static double acos(double a) { return StrictMath.acos(a); // default impl. delegates to StrictMath } @@ -290,6 +295,7 @@ public static double acos(double a) { * @return the arc tangent of the argument. */ @Pure + @StaticallyExecutable public static double atan(double a) { return StrictMath.atan(a); // default impl. delegates to StrictMath } @@ -305,6 +311,7 @@ public static double atan(double a) { * @since 1.2 */ @Pure + @StaticallyExecutable public static double toRadians(double angdeg) { return angdeg * DEGREES_TO_RADIANS; } @@ -322,6 +329,7 @@ public static double toRadians(double angdeg) { * @since 1.2 */ @Pure + @StaticallyExecutable public static double toDegrees(double angrad) { return angrad * RADIANS_TO_DEGREES; } @@ -345,6 +353,7 @@ public static double toDegrees(double angrad) { * where e is the base of the natural logarithms. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double exp(double a) { return StrictMath.exp(a); // default impl. delegates to StrictMath @@ -371,6 +380,7 @@ public static double exp(double a) { * {@code a}. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double log(double a) { return StrictMath.log(a); // default impl. delegates to StrictMath @@ -400,6 +410,7 @@ public static double log(double a) { * @since 1.5 */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double log10(double a) { return StrictMath.log10(a); // default impl. delegates to StrictMath @@ -427,6 +438,7 @@ public static double log10(double a) { * If the argument is NaN or less than zero, the result is NaN. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double sqrt(double a) { return StrictMath.sqrt(a); // default impl. delegates to StrictMath @@ -464,6 +476,7 @@ public static double sqrt(double a) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double cbrt(double a) { return StrictMath.cbrt(a); } @@ -491,6 +504,7 @@ public static double cbrt(double a) { * {@code f2}. */ @Pure + @StaticallyExecutable public static double IEEEremainder(double f1, double f2) { return StrictMath.IEEEremainder(f1, f2); // delegate to StrictMath } @@ -518,6 +532,7 @@ public static double IEEEremainder(double f1, double f2) { * the argument and is equal to a mathematical integer. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double ceil(double a) { return StrictMath.ceil(a); // default impl. delegates to StrictMath @@ -543,6 +558,7 @@ public static double ceil(double a) { * and is equal to a mathematical integer. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double floor(double a) { return StrictMath.floor(a); // default impl. delegates to StrictMath @@ -568,6 +584,7 @@ public static double floor(double a) { * equal to a mathematical integer. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double rint(double a) { return StrictMath.rint(a); // default impl. delegates to StrictMath @@ -635,6 +652,7 @@ public static double rint(double a) { * (x, y) in Cartesian coordinates. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double atan2(double y, double x) { return StrictMath.atan2(y, x); // default impl. delegates to StrictMath @@ -774,6 +792,7 @@ public static double atan2(double y, double x) { * @return the value {@code a}{@code b}. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double pow(double a, double b) { return StrictMath.pow(a, b); // default impl. delegates to StrictMath @@ -800,6 +819,7 @@ public static double pow(double a, double b) { * @see java.lang.Integer#MIN_VALUE */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static int round(float a) { int intBits = Float.floatToRawIntBits(a); @@ -851,6 +871,7 @@ public static int round(float a) { * @see java.lang.Long#MIN_VALUE */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static long round(double a) { long longBits = Double.doubleToRawLongBits(a); @@ -919,7 +940,6 @@ private static final class RandomNumberGeneratorHolder { * @see #nextDown(double) * @see Random#nextDouble() */ - @Pure public static double random() { return RandomNumberGeneratorHolder.randomNumberGenerator.nextDouble(); } @@ -934,6 +954,8 @@ public static double random() { * @throws ArithmeticException if the result overflows an int * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static int addExact(int x, int y) { int r = x + y; @@ -954,6 +976,8 @@ public static int addExact(int x, int y) { * @throws ArithmeticException if the result overflows a long * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static long addExact(long x, long y) { long r = x + y; @@ -974,6 +998,8 @@ public static long addExact(long x, long y) { * @throws ArithmeticException if the result overflows an int * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static int subtractExact(int x, int y) { int r = x - y; @@ -995,6 +1021,8 @@ public static int subtractExact(int x, int y) { * @throws ArithmeticException if the result overflows a long * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static long subtractExact(long x, long y) { long r = x - y; @@ -1016,6 +1044,8 @@ public static long subtractExact(long x, long y) { * @throws ArithmeticException if the result overflows an int * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static int multiplyExact(int x, int y) { long r = (long)x * (long)y; @@ -1035,6 +1065,8 @@ public static int multiplyExact(int x, int y) { * @throws ArithmeticException if the result overflows a long * @since 9 */ + @Pure + @StaticallyExecutable public static long multiplyExact(long x, int y) { return multiplyExact(x, (long)y); } @@ -1049,6 +1081,8 @@ public static long multiplyExact(long x, int y) { * @throws ArithmeticException if the result overflows a long * @since 1.8 */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static long multiplyExact(long x, long y) { long r = x * y; @@ -1088,6 +1122,8 @@ public static long multiplyExact(long x, long y) { * @jls 15.17.2 Division Operator / * @since 18 */ + @Pure + @StaticallyExecutable public static int divideExact(int x, int y) { int q = x / y; if ((x & y & q) >= 0) { @@ -1118,6 +1154,8 @@ public static int divideExact(int x, int y) { * @jls 15.17.2 Division Operator / * @since 18 */ + @Pure + @StaticallyExecutable public static long divideExact(long x, long y) { long q = x / y; if ((x & y & q) >= 0) { @@ -1151,6 +1189,8 @@ public static long divideExact(long x, long y) { * @see #floorDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int floorDivExact(int x, int y) { final int q = x / y; if ((x & y & q) >= 0) { @@ -1188,6 +1228,8 @@ public static int floorDivExact(int x, int y) { * @see #floorDiv(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long floorDivExact(long x, long y) { final long q = x / y; if ((x & y & q) >= 0) { @@ -1225,6 +1267,8 @@ public static long floorDivExact(long x, long y) { * @see #ceilDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilDivExact(int x, int y) { final int q = x / y; if ((x & y & q) >= 0) { @@ -1262,6 +1306,8 @@ public static int ceilDivExact(int x, int y) { * @see #ceilDiv(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDivExact(long x, long y) { final long q = x / y; if ((x & y & q) >= 0) { @@ -1285,6 +1331,8 @@ public static long ceilDivExact(long x, long y) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static int incrementExact(int a) { if (a == Integer.MAX_VALUE) { throw new ArithmeticException("integer overflow"); @@ -1304,6 +1352,8 @@ public static int incrementExact(int a) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static long incrementExact(long a) { if (a == Long.MAX_VALUE) { throw new ArithmeticException("long overflow"); @@ -1323,6 +1373,8 @@ public static long incrementExact(long a) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static int decrementExact(int a) { if (a == Integer.MIN_VALUE) { throw new ArithmeticException("integer overflow"); @@ -1342,6 +1394,8 @@ public static int decrementExact(int a) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static long decrementExact(long a) { if (a == Long.MIN_VALUE) { throw new ArithmeticException("long overflow"); @@ -1361,6 +1415,8 @@ public static long decrementExact(long a) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static int negateExact(int a) { if (a == Integer.MIN_VALUE) { throw new ArithmeticException("integer overflow"); @@ -1380,6 +1436,8 @@ public static int negateExact(int a) { * @since 1.8 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static long negateExact(long a) { if (a == Long.MIN_VALUE) { throw new ArithmeticException("long overflow"); @@ -1397,6 +1455,8 @@ public static long negateExact(long a) { * @throws ArithmeticException if the {@code argument} overflows an int * @since 1.8 */ + @Pure + @StaticallyExecutable public static int toIntExact(long value) { if ((int)value != value) { throw new ArithmeticException("integer overflow"); @@ -1412,6 +1472,8 @@ public static int toIntExact(long value) { * @return the result * @since 9 */ + @Pure + @StaticallyExecutable public static long multiplyFull(int x, int y) { return (long)x * (long)y; } @@ -1427,6 +1489,8 @@ public static long multiplyFull(int x, int y) { * @since 9 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static long multiplyHigh(long x, long y) { // Use technique from section 8-2 of Henry S. Warren, Jr., // Hacker's Delight (2nd ed.) (Addison Wesley, 2013), 173-174. @@ -1455,6 +1519,8 @@ public static long multiplyHigh(long x, long y) { * @since 18 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static long unsignedMultiplyHigh(long x, long y) { // Compute via multiplyHigh() to leverage the intrinsic long result = Math.multiplyHigh(x, y); @@ -1499,6 +1565,8 @@ public static long unsignedMultiplyHigh(long x, long y) { * @see #floor(double) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int floorDiv(int x, int y) { final int q = x / y; // if the signs are different and modulo not zero, round down @@ -1533,6 +1601,8 @@ public static int floorDiv(int x, int y) { * @see #floor(double) * @since 9 */ + @Pure + @StaticallyExecutable public static long floorDiv(long x, int y) { return floorDiv(x, (long)y); } @@ -1562,6 +1632,8 @@ public static long floorDiv(long x, int y) { * @see #floor(double) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long floorDiv(long x, long y) { final long q = x / y; // if the signs are different and modulo not zero, round down @@ -1610,6 +1682,8 @@ public static long floorDiv(long x, long y) { * @see #floorDiv(int, int) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int floorMod(int x, int y) { final int r = x % y; // if the signs are different and modulo not zero, adjust result @@ -1641,6 +1715,8 @@ public static int floorMod(int x, int y) { * @see #floorDiv(long, int) * @since 9 */ + @Pure + @StaticallyExecutable public static int floorMod(long x, int y) { // Result cannot overflow the range of int. return (int)floorMod(x, (long)y); @@ -1668,6 +1744,8 @@ public static int floorMod(long x, int y) { * @see #floorDiv(long, long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long floorMod(long x, long y) { final long r = x % y; // if the signs are different and modulo not zero, adjust result @@ -1713,6 +1791,8 @@ public static long floorMod(long x, long y) { * @see #ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilDiv(int x, int y) { final int q = x / y; // if the signs are the same and modulo not zero, round up @@ -1747,6 +1827,8 @@ public static int ceilDiv(int x, int y) { * @see #ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDiv(long x, int y) { return ceilDiv(x, (long)y); } @@ -1776,6 +1858,8 @@ public static long ceilDiv(long x, int y) { * @see #ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDiv(long x, long y) { final long q = x / y; // if the signs are the same and modulo not zero, round up @@ -1824,6 +1908,8 @@ public static long ceilDiv(long x, long y) { * @see #ceilDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilMod(int x, int y) { final int r = x % y; // if the signs are the same and modulo not zero, adjust result @@ -1855,6 +1941,8 @@ public static int ceilMod(int x, int y) { * @see #ceilDiv(long, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilMod(long x, int y) { // Result cannot overflow the range of int. return (int)ceilMod(x, (long)y); @@ -1882,6 +1970,8 @@ public static int ceilMod(long x, int y) { * @see #ceilDiv(long, long) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilMod(long x, long y) { final long r = x % y; // if the signs are the same and modulo not zero, adjust result @@ -1907,6 +1997,7 @@ public static long ceilMod(long x, long y) { * @see Math#absExact(int) */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static @NonNegative int abs(int a) { return (a < 0) ? -a : a; @@ -1931,6 +2022,7 @@ public static long ceilMod(long x, long y) { * @since 15 */ @Pure + @StaticallyExecutable public static int absExact(int a) { if (a == Integer.MIN_VALUE) throw new ArithmeticException( @@ -1955,6 +2047,7 @@ public static int absExact(int a) { * @see Math#absExact(long) */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static @NonNegative long abs(long a) { return (a < 0) ? -a : a; @@ -1979,6 +2072,7 @@ public static int absExact(int a) { * @since 15 */ @Pure + @StaticallyExecutable public static long absExact(long a) { if (a == Long.MIN_VALUE) throw new ArithmeticException( @@ -2008,6 +2102,7 @@ public static long absExact(long a) { * @return the absolute value of the argument. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static float abs(float a) { // Convert to bit field form, zero the sign bit, and convert back @@ -2035,6 +2130,7 @@ public static float abs(float a) { * @return the absolute value of the argument. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double abs(double a) { // Convert to bit field form, zero the sign bit, and convert back @@ -2156,6 +2252,7 @@ public static double max(double a, double b) { * @return the smaller of {@code a} and {@code b}. */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static @PolyLowerBound int min(@PolyLowerBound int a, @PolyLowerBound int b) { return (a <= b) ? a : b; @@ -2262,6 +2359,8 @@ public static double min(double a, double b) { * * @since 21 */ + @Pure + @StaticallyExecutable public static int clamp(long value, int min, int max) { if (min > max) { throw new IllegalArgumentException(min + " > " + max); @@ -2283,6 +2382,8 @@ public static int clamp(long value, int min, int max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static long clamp(long value, long min, long max) { if (min > max) { throw new IllegalArgumentException(min + " > " + max); @@ -2310,6 +2411,8 @@ public static long clamp(long value, long min, long max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static double clamp(double value, double min, double max) { // This unusual condition allows keeping only one branch // on common path when min < max and neither of them is NaN. @@ -2351,6 +2454,8 @@ public static double clamp(double value, double min, double max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static float clamp(float value, float min, float max) { // This unusual condition allows keeping only one branch // on common path when min < max and neither of them is NaN. @@ -2423,6 +2528,8 @@ public static float clamp(float value, float min, float max) { * @since 9 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static double fma(double a, double b, double c) { /* * Infinity and NaN arithmetic is not quite the same with two @@ -2537,6 +2644,8 @@ public static double fma(double a, double b, double c) { * @since 9 */ @IntrinsicCandidate + @Pure + @StaticallyExecutable public static float fma(float a, float b, float c) { if (Float.isFinite(a) && Float.isFinite(b) && Float.isFinite(c)) { if (a == 0.0 || b == 0.0) { @@ -2579,6 +2688,7 @@ public static float fma(float a, float b, float c) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double ulp(double d) { int exp = getExponent(d); @@ -2627,6 +2737,7 @@ public static double ulp(double d) { * @since 1.5 */ @Pure + @StaticallyExecutable public static float ulp(float f) { int exp = getExponent(f); @@ -2669,6 +2780,7 @@ public static float ulp(float f) { * @since 1.5 */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double signum(double d) { return (d == 0.0 || Double.isNaN(d))?d:copySign(1.0, d); @@ -2692,6 +2804,7 @@ public static double signum(double d) { * @since 1.5 */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static float signum(float f) { return (f == 0.0f || Float.isNaN(f))?f:copySign(1.0f, f); @@ -2723,6 +2836,7 @@ public static float signum(float f) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double sinh(double x) { return StrictMath.sinh(x); } @@ -2752,6 +2866,7 @@ public static double sinh(double x) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double cosh(double x) { return StrictMath.cosh(x); } @@ -2793,6 +2908,7 @@ public static double cosh(double x) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double tanh(double x) { return StrictMath.tanh(x); } @@ -2824,6 +2940,7 @@ public static double tanh(double x) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double hypot(double x, double y) { return StrictMath.hypot(x, y); } @@ -2863,6 +2980,7 @@ public static double hypot(double x, double y) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double expm1(double x) { return StrictMath.expm1(x); } @@ -2901,6 +3019,7 @@ public static double expm1(double x) { * @since 1.5 */ @Pure + @StaticallyExecutable public static double log1p(double x) { return StrictMath.log1p(x); } @@ -2925,6 +3044,7 @@ public static double log1p(double x) { * @since 1.6 */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static double copySign(double magnitude, double sign) { return Double.longBitsToDouble((Double.doubleToRawLongBits(sign) & @@ -2954,6 +3074,7 @@ public static double copySign(double magnitude, double sign) { * @since 1.6 */ @Pure + @StaticallyExecutable @IntrinsicCandidate public static float copySign(float magnitude, float sign) { return Float.intBitsToFloat((Float.floatToRawIntBits(sign) & @@ -2982,6 +3103,7 @@ public static float copySign(float magnitude, float sign) { * @since 1.6 */ @Pure + @StaticallyExecutable public static int getExponent(float f) { /* * Bitwise convert f to integer, mask out exponent bits, shift @@ -3011,6 +3133,7 @@ public static int getExponent(float f) { * @since 1.6 */ @Pure + @StaticallyExecutable public static int getExponent(double d) { /* * Bitwise convert d to long, mask out exponent bits, shift @@ -3062,6 +3185,7 @@ public static int getExponent(double d) { * @since 1.6 */ @Pure + @StaticallyExecutable public static double nextAfter(double start, double direction) { /* * The cases: @@ -3147,6 +3271,7 @@ public static double nextAfter(double start, double direction) { * @since 1.6 */ @Pure + @StaticallyExecutable public static float nextAfter(float start, double direction) { /* * The cases: @@ -3221,6 +3346,7 @@ public static float nextAfter(float start, double direction) { * @since 1.6 */ @Pure + @StaticallyExecutable public static double nextUp(double d) { // Use a single conditional and handle the likely cases first. if (d < Double.POSITIVE_INFINITY) { @@ -3261,6 +3387,7 @@ public static double nextUp(double d) { * @since 1.6 */ @Pure + @StaticallyExecutable public static float nextUp(float f) { // Use a single conditional and handle the likely cases first. if (f < Float.POSITIVE_INFINITY) { @@ -3300,6 +3427,8 @@ public static float nextUp(float f) { * infinity. * @since 1.8 */ + @Pure + @StaticallyExecutable public static double nextDown(double d) { if (Double.isNaN(d) || d == Double.NEGATIVE_INFINITY) return d; @@ -3340,6 +3469,8 @@ public static double nextDown(double d) { * infinity. * @since 1.8 */ + @Pure + @StaticallyExecutable public static float nextDown(float f) { if (Float.isNaN(f) || f == Float.NEGATIVE_INFINITY) return f; @@ -3383,6 +3514,7 @@ public static float nextDown(float f) { * @since 1.6 */ @Pure + @StaticallyExecutable public static double scalb(double d, int scaleFactor) { /* * When scaling up, it does not matter what order the @@ -3471,6 +3603,7 @@ public static double scalb(double d, int scaleFactor) { * @since 1.6 */ @Pure + @StaticallyExecutable public static float scalb(float f, int scaleFactor) { // magnitude of a power of two so large that scaling a finite // nonzero value by it would be guaranteed to over or diff --git a/src/java.base/share/classes/java/lang/StrictMath.java b/src/java.base/share/classes/java/lang/StrictMath.java index 434a066d222d1..004c84384ddfc 100644 --- a/src/java.base/share/classes/java/lang/StrictMath.java +++ b/src/java.base/share/classes/java/lang/StrictMath.java @@ -153,6 +153,8 @@ private StrictMath() {} * @param a an angle, in radians. * @return the sine of the argument. */ + @Pure + @StaticallyExecutable public static double sin(double a) { return FdLibm.Sin.compute(a); } @@ -167,6 +169,8 @@ public static double sin(double a) { * @param a an angle, in radians. * @return the cosine of the argument. */ + @Pure + @StaticallyExecutable public static double cos(double a) { return FdLibm.Cos.compute(a); } @@ -181,6 +185,8 @@ public static double cos(double a) { * @param a an angle, in radians. * @return the tangent of the argument. */ + @Pure + @StaticallyExecutable public static double tan(double a) { return FdLibm.Tan.compute(a); } @@ -196,6 +202,8 @@ public static double tan(double a) { * @param a the value whose arc sine is to be returned. * @return the arc sine of the argument. */ + @Pure + @StaticallyExecutable public static double asin(double a) { return FdLibm.Asin.compute(a); } @@ -211,6 +219,8 @@ public static double asin(double a) { * @param a the value whose arc cosine is to be returned. * @return the arc cosine of the argument. */ + @Pure + @StaticallyExecutable public static double acos(double a) { return FdLibm.Acos.compute(a); } @@ -229,6 +239,8 @@ public static double acos(double a) { * @param a the value whose arc tangent is to be returned. * @return the arc tangent of the argument. */ + @Pure + @StaticallyExecutable public static double atan(double a) { return FdLibm.Atan.compute(a); } @@ -242,6 +254,8 @@ public static double atan(double a) { * @return the measurement of the angle {@code angdeg} * in radians. */ + @Pure + @StaticallyExecutable public static double toRadians(double angdeg) { return Math.toRadians(angdeg); } @@ -257,6 +271,8 @@ public static double toRadians(double angdeg) { * @return the measurement of the angle {@code angrad} * in degrees. */ + @Pure + @StaticallyExecutable public static double toDegrees(double angrad) { return Math.toDegrees(angrad); } @@ -276,6 +292,8 @@ public static double toDegrees(double angrad) { * @return the value e{@code a}, * where e is the base of the natural logarithms. */ + @Pure + @StaticallyExecutable public static double exp(double a) { return FdLibm.Exp.compute(a); } @@ -297,6 +315,8 @@ public static double exp(double a) { * @return the value ln {@code a}, the natural logarithm of * {@code a}. */ + @Pure + @StaticallyExecutable public static double log(double a) { return FdLibm.Log.compute(a); } @@ -321,6 +341,8 @@ public static double log(double a) { * @return the base 10 logarithm of {@code a}. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double log10(double a) { return FdLibm.Log10.compute(a); } @@ -341,6 +363,8 @@ public static double log10(double a) { * @param a a value. * @return the positive square root of {@code a}. */ + @Pure + @StaticallyExecutable @IntrinsicCandidate public static double sqrt(double a) { return FdLibm.Sqrt.compute(a); @@ -369,6 +393,8 @@ public static double sqrt(double a) { * @return the cube root of {@code a}. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double cbrt(double a) { return FdLibm.Cbrt.compute(a); } @@ -395,6 +421,8 @@ public static double cbrt(double a) { * @return the remainder when {@code f1} is divided by * {@code f2}. */ + @Pure + @StaticallyExecutable public static double IEEEremainder(double f1, double f2) { return FdLibm.IEEEremainder.compute(f1, f2); } @@ -417,6 +445,8 @@ public static double IEEEremainder(double f1, double f2) { * floating-point value that is greater than or equal to * the argument and is equal to a mathematical integer. */ + @Pure + @StaticallyExecutable public static double ceil(double a) { return floorOrCeil(a, -0.0, 1.0, 1.0); } @@ -436,6 +466,8 @@ public static double ceil(double a) { * floating-point value that less than or equal to the argument * and is equal to a mathematical integer. */ + @Pure + @StaticallyExecutable public static double floor(double a) { return floorOrCeil(a, -1.0, 0.0, -1.0); } @@ -448,6 +480,8 @@ public static double floor(double a) { * @param positiveBoundary result for values in (0, 1) * @param sign the sign of the result */ + @Pure + @StaticallyExecutable private static double floorOrCeil(double a, double negativeBoundary, double positiveBoundary, @@ -501,6 +535,8 @@ private static double floorOrCeil(double a, * equal to a mathematical integer. * @author Joseph D. Darcy */ + @Pure + @StaticallyExecutable public static double rint(double a) { /* * If the absolute value of a is not less than 2^52, it @@ -583,6 +619,8 @@ public static double rint(double a) { * in polar coordinates that corresponds to the point * (x, y) in Cartesian coordinates. */ + @Pure + @StaticallyExecutable public static double atan2(double y, double x) { return FdLibm.Atan2.compute(y, x); } @@ -717,6 +755,8 @@ public static double atan2(double y, double x) { * @param b the exponent. * @return the value {@code a}{@code b}. */ + @Pure + @StaticallyExecutable public static double pow(double a, double b) { return FdLibm.Pow.compute(a, b); } @@ -740,6 +780,8 @@ public static double pow(double a, double b) { * @see java.lang.Integer#MAX_VALUE * @see java.lang.Integer#MIN_VALUE */ + @Pure + @StaticallyExecutable public static int round(float a) { return Math.round(a); } @@ -764,6 +806,8 @@ public static int round(float a) { * @see java.lang.Long#MAX_VALUE * @see java.lang.Long#MIN_VALUE */ + @Pure + @StaticallyExecutable public static long round(double a) { return Math.round(a); } @@ -810,6 +854,8 @@ public static double random() { * @see Math#addExact(int,int) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int addExact(int x, int y) { return Math.addExact(x, y); } @@ -825,6 +871,8 @@ public static int addExact(int x, int y) { * @see Math#addExact(long,long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long addExact(long x, long y) { return Math.addExact(x, y); } @@ -840,6 +888,8 @@ public static long addExact(long x, long y) { * @see Math#subtractExact(int,int) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int subtractExact(int x, int y) { return Math.subtractExact(x, y); } @@ -855,6 +905,8 @@ public static int subtractExact(int x, int y) { * @see Math#subtractExact(long,long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long subtractExact(long x, long y) { return Math.subtractExact(x, y); } @@ -870,6 +922,8 @@ public static long subtractExact(long x, long y) { * @see Math#multiplyExact(int,int) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int multiplyExact(int x, int y) { return Math.multiplyExact(x, y); } @@ -885,6 +939,8 @@ public static int multiplyExact(int x, int y) { * @see Math#multiplyExact(long,int) * @since 9 */ + @Pure + @StaticallyExecutable public static long multiplyExact(long x, int y) { return Math.multiplyExact(x, y); } @@ -900,6 +956,8 @@ public static long multiplyExact(long x, int y) { * @see Math#multiplyExact(long,long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long multiplyExact(long x, long y) { return Math.multiplyExact(x, y); } @@ -927,6 +985,8 @@ public static long multiplyExact(long x, long y) { * @see Math#divideExact(int,int) * @since 18 */ + @Pure + @StaticallyExecutable public static int divideExact(int x, int y) { return Math.divideExact(x, y); } @@ -954,6 +1014,8 @@ public static int divideExact(int x, int y) { * @see Math#divideExact(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long divideExact(long x, long y) { return Math.divideExact(x, y); } @@ -984,6 +1046,8 @@ public static long divideExact(long x, long y) { * @see Math#floorDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int floorDivExact(int x, int y) { return Math.floorDivExact(x, y); } @@ -1014,6 +1078,8 @@ public static int floorDivExact(int x, int y) { * @see Math#floorDiv(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long floorDivExact(long x, long y) { return Math.floorDivExact(x, y); } @@ -1044,6 +1110,8 @@ public static long floorDivExact(long x, long y) { * @see Math#ceilDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilDivExact(int x, int y) { return Math.ceilDivExact(x, y); } @@ -1074,6 +1142,8 @@ public static int ceilDivExact(int x, int y) { * @see Math#ceilDiv(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDivExact(long x, long y) { return Math.ceilDivExact(x, y); } @@ -1090,6 +1160,7 @@ public static long ceilDivExact(long x, long y) { * @since 14 */ @Pure + @StaticallyExecutable public static int incrementExact(int a) { return Math.incrementExact(a); } @@ -1106,6 +1177,7 @@ public static int incrementExact(int a) { * @since 14 */ @Pure + @StaticallyExecutable public static long incrementExact(long a) { return Math.incrementExact(a); } @@ -1122,6 +1194,7 @@ public static long incrementExact(long a) { * @since 14 */ @Pure + @StaticallyExecutable public static int decrementExact(int a) { return Math.decrementExact(a); } @@ -1138,6 +1211,7 @@ public static int decrementExact(int a) { * @since 14 */ @Pure + @StaticallyExecutable public static long decrementExact(long a) { return Math.decrementExact(a); } @@ -1154,6 +1228,7 @@ public static long decrementExact(long a) { * @since 14 */ @Pure + @StaticallyExecutable public static int negateExact(int a) { return Math.negateExact(a); } @@ -1170,6 +1245,7 @@ public static int negateExact(int a) { * @since 14 */ @Pure + @StaticallyExecutable public static long negateExact(long a) { return Math.negateExact(a); } @@ -1184,6 +1260,8 @@ public static long negateExact(long a) { * @see Math#toIntExact(long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int toIntExact(long value) { return Math.toIntExact(value); } @@ -1197,6 +1275,8 @@ public static int toIntExact(long value) { * @see Math#multiplyFull(int,int) * @since 9 */ + @Pure + @StaticallyExecutable public static long multiplyFull(int x, int y) { return Math.multiplyFull(x, y); } @@ -1212,6 +1292,8 @@ public static long multiplyFull(int x, int y) { * @see Math#multiplyHigh(long,long) * @since 9 */ + @Pure + @StaticallyExecutable public static long multiplyHigh(long x, long y) { return Math.multiplyHigh(x, y); } @@ -1227,6 +1309,8 @@ public static long multiplyHigh(long x, long y) { * @see Math#unsignedMultiplyHigh(long,long) * @since 18 */ + @Pure + @StaticallyExecutable public static long unsignedMultiplyHigh(long x, long y) { return Math.unsignedMultiplyHigh(x, y); } @@ -1251,6 +1335,8 @@ public static long unsignedMultiplyHigh(long x, long y) { * @see Math#floor(double) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int floorDiv(int x, int y) { return Math.floorDiv(x, y); } @@ -1275,6 +1361,8 @@ public static int floorDiv(int x, int y) { * @see Math#floor(double) * @since 9 */ + @Pure + @StaticallyExecutable public static long floorDiv(long x, int y) { return Math.floorDiv(x, y); } @@ -1299,6 +1387,8 @@ public static long floorDiv(long x, int y) { * @see Math#floor(double) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long floorDiv(long x, long y) { return Math.floorDiv(x, y); } @@ -1327,6 +1417,8 @@ public static long floorDiv(long x, long y) { * @see StrictMath#floorDiv(int, int) * @since 1.8 */ + @Pure + @StaticallyExecutable public static int floorMod(int x, int y) { return Math.floorMod(x , y); } @@ -1355,6 +1447,8 @@ public static int floorMod(int x, int y) { * @see StrictMath#floorDiv(long, int) * @since 9 */ + @Pure + @StaticallyExecutable public static int floorMod(long x, int y) { return Math.floorMod(x , y); } @@ -1383,6 +1477,8 @@ public static int floorMod(long x, int y) { * @see StrictMath#floorDiv(long, long) * @since 1.8 */ + @Pure + @StaticallyExecutable public static long floorMod(long x, long y) { return Math.floorMod(x, y); } @@ -1407,6 +1503,8 @@ public static long floorMod(long x, long y) { * @see Math#ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilDiv(int x, int y) { return Math.ceilDiv(x, y); } @@ -1431,6 +1529,8 @@ public static int ceilDiv(int x, int y) { * @see Math#ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDiv(long x, int y) { return Math.ceilDiv(x, y); } @@ -1455,6 +1555,8 @@ public static long ceilDiv(long x, int y) { * @see Math#ceil(double) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilDiv(long x, long y) { return Math.ceilDiv(x, y); } @@ -1483,6 +1585,8 @@ public static long ceilDiv(long x, long y) { * @see StrictMath#ceilDiv(int, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilMod(int x, int y) { return Math.ceilMod(x , y); } @@ -1511,6 +1615,8 @@ public static int ceilMod(int x, int y) { * @see StrictMath#ceilDiv(long, int) * @since 18 */ + @Pure + @StaticallyExecutable public static int ceilMod(long x, int y) { return Math.ceilMod(x , y); } @@ -1539,6 +1645,8 @@ public static int ceilMod(long x, int y) { * @see StrictMath#ceilDiv(long, long) * @since 18 */ + @Pure + @StaticallyExecutable public static long ceilMod(long x, long y) { return Math.ceilMod(x, y); } @@ -1558,6 +1666,8 @@ public static long ceilMod(long x, long y) { * @return the absolute value of the argument. * @see Math#absExact(int) */ + @Pure + @StaticallyExecutable public static int abs(int a) { return Math.abs(a); } @@ -1582,6 +1692,8 @@ public static int abs(int a) { * @since 15 */ @Pure + @Pure + @StaticallyExecutable public static int absExact(int a) { return Math.absExact(a); } @@ -1601,6 +1713,8 @@ public static int absExact(int a) { * @return the absolute value of the argument. * @see Math#absExact(long) */ + @Pure + @StaticallyExecutable public static long abs(long a) { return Math.abs(a); } @@ -1625,6 +1739,7 @@ public static long abs(long a) { * @since 15 */ @Pure + @StaticallyExecutable public static long absExact(long a) { return Math.absExact(a); } @@ -1649,6 +1764,8 @@ public static long absExact(long a) { * @param a the argument whose absolute value is to be determined * @return the absolute value of the argument. */ + @Pure + @StaticallyExecutable public static float abs(float a) { return Math.abs(a); } @@ -1673,6 +1790,8 @@ public static float abs(float a) { * @param a the argument whose absolute value is to be determined * @return the absolute value of the argument. */ + @Pure + @StaticallyExecutable public static double abs(double a) { return Math.abs(a); } @@ -1846,6 +1965,8 @@ public static double min(double a, double b) { * * @since 21 */ + @Pure + @StaticallyExecutable public static int clamp(long value, int min, int max) { return Math.clamp(value, min, max); } @@ -1864,6 +1985,8 @@ public static int clamp(long value, int min, int max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static long clamp(long value, long min, long max) { return Math.clamp(value, min, max); } @@ -1888,6 +2011,8 @@ public static long clamp(long value, long min, long max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static double clamp(double value, double min, double max) { return Math.clamp(value, min, max); } @@ -1912,6 +2037,8 @@ public static double clamp(double value, double min, double max) { * * @since 21 */ + @Pure + @StaticallyExecutable public static float clamp(float value, float min, float max) { return Math.clamp(value, min, max); } @@ -1966,6 +2093,8 @@ public static float clamp(float value, float min, float max) { * * @since 9 */ + @Pure + @StaticallyExecutable public static double fma(double a, double b, double c) { return Math.fma(a, b, c); } @@ -2020,6 +2149,8 @@ public static double fma(double a, double b, double c) { * * @since 9 */ + @Pure + @StaticallyExecutable public static float fma(float a, float b, float c) { return Math.fma(a, b, c); } @@ -2047,6 +2178,8 @@ public static float fma(float a, float b, float c) { * @author Joseph D. Darcy * @since 1.5 */ + @Pure + @StaticallyExecutable public static double ulp(double d) { return Math.ulp(d); } @@ -2074,6 +2207,8 @@ public static double ulp(double d) { * @author Joseph D. Darcy * @since 1.5 */ + @Pure + @StaticallyExecutable public static float ulp(float f) { return Math.ulp(f); } @@ -2095,6 +2230,8 @@ public static float ulp(float f) { * @author Joseph D. Darcy * @since 1.5 */ + @Pure + @StaticallyExecutable public static double signum(double d) { return Math.signum(d); } @@ -2116,6 +2253,8 @@ public static double signum(double d) { * @author Joseph D. Darcy * @since 1.5 */ + @Pure + @StaticallyExecutable public static float signum(float f) { return Math.signum(f); } @@ -2143,6 +2282,8 @@ public static float signum(float f) { * @return The hyperbolic sine of {@code x}. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double sinh(double x) { return FdLibm.Sinh.compute(x); } @@ -2169,6 +2310,8 @@ public static double sinh(double x) { * @return The hyperbolic cosine of {@code x}. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double cosh(double x) { return FdLibm.Cosh.compute(x); } @@ -2202,6 +2345,8 @@ public static double cosh(double x) { * @return The hyperbolic tangent of {@code x}. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double tanh(double x) { return FdLibm.Tanh.compute(x); } @@ -2228,6 +2373,8 @@ public static double tanh(double x) { * without intermediate overflow or underflow * @since 1.5 */ + @Pure + @StaticallyExecutable public static double hypot(double x, double y) { return FdLibm.Hypot.compute(x, y); } @@ -2258,6 +2405,8 @@ public static double hypot(double x, double y) { * @return the value e{@code x} - 1. * @since 1.5 */ + @Pure + @StaticallyExecutable public static double expm1(double x) { return FdLibm.Expm1.compute(x); } @@ -2291,6 +2440,8 @@ public static double expm1(double x) { * log of {@code x} + 1 * @since 1.5 */ + @Pure + @StaticallyExecutable public static double log1p(double x) { return FdLibm.Log1p.compute(x); } @@ -2307,6 +2458,8 @@ public static double log1p(double x) { * and the sign of {@code sign}. * @since 1.6 */ + @Pure + @StaticallyExecutable public static double copySign(double magnitude, double sign) { return Math.copySign(magnitude, (Double.isNaN(sign)?1.0d:sign)); } @@ -2323,6 +2476,8 @@ public static double copySign(double magnitude, double sign) { * and the sign of {@code sign}. * @since 1.6 */ + @Pure + @StaticallyExecutable public static float copySign(float magnitude, float sign) { return Math.copySign(magnitude, (Float.isNaN(sign)?1.0f:sign)); } @@ -2340,6 +2495,8 @@ public static float copySign(float magnitude, float sign) { * @return the unbiased exponent of the argument * @since 1.6 */ + @Pure + @StaticallyExecutable public static int getExponent(float f) { return Math.getExponent(f); } @@ -2358,6 +2515,8 @@ public static int getExponent(float f) { * @return the unbiased exponent of the argument * @since 1.6 */ + @Pure + @StaticallyExecutable public static int getExponent(double d) { return Math.getExponent(d); } @@ -2401,6 +2560,8 @@ public static int getExponent(double d) { * direction of {@code direction}. * @since 1.6 */ + @Pure + @StaticallyExecutable public static double nextAfter(double start, double direction) { return Math.nextAfter(start, direction); } @@ -2443,6 +2604,8 @@ public static double nextAfter(double start, double direction) { * direction of {@code direction}. * @since 1.6 */ + @Pure + @StaticallyExecutable public static float nextAfter(float start, double direction) { return Math.nextAfter(start, direction); } @@ -2472,6 +2635,8 @@ public static float nextAfter(float start, double direction) { * infinity. * @since 1.6 */ + @Pure + @StaticallyExecutable public static double nextUp(double d) { return Math.nextUp(d); } @@ -2501,6 +2666,8 @@ public static double nextUp(double d) { * infinity. * @since 1.6 */ + @Pure + @StaticallyExecutable public static float nextUp(float f) { return Math.nextUp(f); } @@ -2530,6 +2697,8 @@ public static float nextUp(float f) { * infinity. * @since 1.8 */ + @Pure + @StaticallyExecutable public static double nextDown(double d) { return Math.nextDown(d); } @@ -2559,6 +2728,8 @@ public static double nextDown(double d) { * infinity. * @since 1.8 */ + @Pure + @StaticallyExecutable public static float nextDown(float f) { return Math.nextDown(f); } @@ -2590,6 +2761,8 @@ public static float nextDown(float f) { * @return {@code d} × 2{@code scaleFactor} * @since 1.6 */ + @Pure + @StaticallyExecutable public static double scalb(double d, int scaleFactor) { return Math.scalb(d, scaleFactor); } @@ -2621,6 +2794,8 @@ public static double scalb(double d, int scaleFactor) { * @return {@code f} × 2{@code scaleFactor} * @since 1.6 */ + @Pure + @StaticallyExecutable public static float scalb(float f, int scaleFactor) { return Math.scalb(f, scaleFactor); } diff --git a/src/java.base/share/classes/java/math/BigInteger.java b/src/java.base/share/classes/java/math/BigInteger.java index 1d78e687e02e9..4ca8d668e3070 100644 --- a/src/java.base/share/classes/java/math/BigInteger.java +++ b/src/java.base/share/classes/java/math/BigInteger.java @@ -887,6 +887,7 @@ private static BigInteger largePrime(int bitLength, int certainty, Random rnd) { * exhaustion of available heap space, or could run for a long time. * @since 1.5 */ + @SideEffectFree public BigInteger nextProbablePrime() { if (this.signum < 0) throw new ArithmeticException("start < 0: " + this); @@ -1202,6 +1203,7 @@ private static void reportOverflow() { * @param val value of the BigInteger to return. * @return a BigInteger with the specified value. */ + @SideEffectFree public static BigInteger valueOf(long val) { // If -MAX_CONSTANT < val < MAX_CONSTANT, return stashed constant if (val == 0) @@ -1341,6 +1343,7 @@ private static BigInteger valueOf(int[] val) { * @param val value to be added to this BigInteger. * @return {@code this + val} */ + @SideEffectFree public BigInteger add(BigInteger val) { if (val.signum == 0) return this; @@ -1543,6 +1546,7 @@ private static int[] subtract(int[] big, long val) { * @param val value to be subtracted from this BigInteger. * @return {@code this - val} */ + @SideEffectFree public BigInteger subtract(BigInteger val) { if (val.signum == 0) return this; @@ -1601,6 +1605,7 @@ private static int[] subtract(int[] big, int[] little) { * @param val value to be multiplied by this BigInteger. * @return {@code this * val} */ + @SideEffectFree public BigInteger multiply(BigInteger val) { return multiply(val, false, false, 0); } @@ -1625,6 +1630,7 @@ public BigInteger multiply(BigInteger val) { * @see #multiply * @since 19 */ + @SideEffectFree public BigInteger parallelMultiply(BigInteger val) { return multiply(val, false, true, 0); } @@ -2427,6 +2433,7 @@ private BigInteger squareToomCook3(boolean parallel, int depth) { * @return {@code this / val} * @throws ArithmeticException if {@code val} is zero. */ + @SideEffectFree public BigInteger divide(BigInteger val) { if (val.mag.length < BURNIKEL_ZIEGLER_THRESHOLD || mag.length - val.mag.length < BURNIKEL_ZIEGLER_OFFSET) { @@ -2464,6 +2471,7 @@ private BigInteger divideKnuth(BigInteger val) { * is the final element. * @throws ArithmeticException if {@code val} is zero. */ + @SideEffectFree public BigInteger[] divideAndRemainder(BigInteger val) { if (val.mag.length < BURNIKEL_ZIEGLER_THRESHOLD || mag.length - val.mag.length < BURNIKEL_ZIEGLER_OFFSET) { @@ -2493,6 +2501,7 @@ private BigInteger[] divideAndRemainderKnuth(BigInteger val) { * @return {@code this % val} * @throws ArithmeticException if {@code val} is zero. */ + @SideEffectFree public BigInteger remainder(BigInteger val) { if (val.mag.length < BURNIKEL_ZIEGLER_THRESHOLD || mag.length - val.mag.length < BURNIKEL_ZIEGLER_OFFSET) { @@ -2552,6 +2561,7 @@ private BigInteger[] divideAndRemainderBurnikelZiegler(BigInteger val) { * @throws ArithmeticException {@code exponent} is negative. (This would * cause the operation to yield a non-integer value.) */ + @SideEffectFree public BigInteger pow(int exponent) { if (exponent < 0) { throw new ArithmeticException("Negative exponent"); @@ -2685,6 +2695,7 @@ public BigInteger pow(int exponent) { * {@code sqrt(-1)}.) * @since 9 */ + @SideEffectFree public BigInteger sqrt() { if (this.signum < 0) { throw new ArithmeticException("Negative BigInteger"); @@ -2708,6 +2719,7 @@ public BigInteger sqrt() { * @see #sqrt() * @since 9 */ + @SideEffectFree public BigInteger[] sqrtAndRemainder() { BigInteger s = sqrt(); BigInteger r = this.subtract(s.square()); @@ -2723,6 +2735,7 @@ public BigInteger[] sqrtAndRemainder() { * @param val value with which the GCD is to be computed. * @return {@code GCD(abs(this), abs(val))} */ + @SideEffectFree public BigInteger gcd(BigInteger val) { if (val.signum == 0) return this.abs(); @@ -2804,6 +2817,7 @@ private static int bitLength(int[] val, int len) { * * @return {@code abs(this)} */ + @SideEffectFree public BigInteger abs() { return (signum >= 0 ? this : this.negate()); } @@ -2813,6 +2827,7 @@ public BigInteger abs() { * * @return {@code -this} */ + @SideEffectFree public BigInteger negate() { return new BigInteger(this.mag, -this.signum); } @@ -2823,6 +2838,7 @@ public BigInteger negate() { * @return -1, 0 or 1 as the value of this BigInteger is negative, zero or * positive. */ + @Pure public @IntRange(from = -1, to = 1) int signum() { return this.signum; } @@ -2839,6 +2855,7 @@ public BigInteger negate() { * @throws ArithmeticException {@code m} ≤ 0 * @see #remainder */ + @SideEffectFree public BigInteger mod(BigInteger m) { if (m.signum <= 0) throw new ArithmeticException("BigInteger: modulus not positive"); @@ -2860,6 +2877,7 @@ public BigInteger mod(BigInteger m) { * prime to {@code m}. * @see #modInverse */ + @SideEffectFree public BigInteger modPow(BigInteger exponent, BigInteger m) { if (m.signum <= 0) throw new ArithmeticException("BigInteger: modulus not positive"); @@ -3421,6 +3439,7 @@ private BigInteger mod2(int p) { * has no multiplicative inverse mod m (that is, this BigInteger * is not relatively prime to m). */ + @SideEffectFree public BigInteger modInverse(BigInteger m) { if (m.signum != 1) throw new ArithmeticException("BigInteger: modulus not positive"); @@ -3455,6 +3474,7 @@ public BigInteger modInverse(BigInteger m) { * @return {@code this << n} * @see #shiftRight */ + @SideEffectFree public BigInteger shiftLeft(int n) { if (signum == 0) return ZERO; @@ -3526,6 +3546,7 @@ private static void shiftLeftImplWorker(int[] newArr, int[] oldArr, int newIdx, * @return {@code this >> n} * @see #shiftLeft */ + @SideEffectFree public BigInteger shiftRight(int n) { if (signum == 0) return ZERO; @@ -3623,6 +3644,7 @@ int[] javaIncrement(int[] val) { * @param val value to be AND'ed with this BigInteger. * @return {@code this & val} */ + @SideEffectFree public BigInteger and(BigInteger val) { int[] result = new int[Math.max(intLength(), val.intLength())]; for (int i=0; i < result.length; i++) @@ -3640,6 +3662,7 @@ public BigInteger and(BigInteger val) { * @param val value to be OR'ed with this BigInteger. * @return {@code this | val} */ + @SideEffectFree public BigInteger or(BigInteger val) { int[] result = new int[Math.max(intLength(), val.intLength())]; for (int i=0; i < result.length; i++) @@ -3657,6 +3680,7 @@ public BigInteger or(BigInteger val) { * @param val value to be XOR'ed with this BigInteger. * @return {@code this ^ val} */ + @SideEffectFree public BigInteger xor(BigInteger val) { int[] result = new int[Math.max(intLength(), val.intLength())]; for (int i=0; i < result.length; i++) @@ -3673,6 +3697,7 @@ public BigInteger xor(BigInteger val) { * * @return {@code ~this} */ + @SideEffectFree public BigInteger not() { int[] result = new int[intLength()]; for (int i=0; i < result.length; i++) @@ -3691,6 +3716,7 @@ public BigInteger not() { * @param val value to be complemented and AND'ed with this BigInteger. * @return {@code this & ~val} */ + @SideEffectFree public BigInteger andNot(BigInteger val) { int[] result = new int[Math.max(intLength(), val.intLength())]; for (int i=0; i < result.length; i++) @@ -3711,6 +3737,7 @@ public BigInteger andNot(BigInteger val) { * @return {@code true} if and only if the designated bit is set. * @throws ArithmeticException {@code n} is negative. */ + @Pure public boolean testBit(int n) { if (n < 0) throw new ArithmeticException("Negative bit address"); @@ -3797,6 +3824,7 @@ public BigInteger flipBit(int n) { * * @return index of the rightmost one bit in this BigInteger. */ + @Pure public int getLowestSetBit() { int lsb = lowestSetBitPlusTwo - 2; if (lsb == -2) { // lowestSetBit not initialized yet @@ -3828,6 +3856,7 @@ public int getLowestSetBit() { * @return number of bits in the minimal two's-complement * representation of this BigInteger, excluding a sign bit. */ + @Pure public int bitLength() { int n = bitLengthPlusOne - 1; if (n == -1) { // bitLength not initialized yet @@ -3862,6 +3891,7 @@ public int bitLength() { * @return number of bits in the two's complement representation * of this BigInteger that differ from its sign bit. */ + @Pure public int bitCount() { int bc = bitCountPlusOne - 1; if (bc == -1) { // bitCount not initialized yet @@ -3932,6 +3962,7 @@ public boolean isProbablePrime(int certainty) { * @return -1, 0 or 1 as this BigInteger is numerically less than, equal * to, or greater than {@code val}. */ + @Pure public @IntRange(from = -1, to = 1) int compareTo(BigInteger val) { if (signum == val.signum) { return switch (signum) { @@ -4053,7 +4084,6 @@ public boolean equals(@Nullable Object x) { * {@code val}. If they are equal, either may be returned. */ @Pure - @StaticallyExecutable public BigInteger min(BigInteger val) { return (compareTo(val) < 0 ? this : val); } @@ -4066,7 +4096,6 @@ public BigInteger min(BigInteger val) { * {@code val}. If they are equal, either may be returned. */ @Pure - @StaticallyExecutable public BigInteger max(BigInteger val) { return (compareTo(val) > 0 ? this : val); } @@ -4079,6 +4108,7 @@ public BigInteger max(BigInteger val) { * * @return hash code for this BigInteger. */ + @Pure public int hashCode() { int hashCode = 0; @@ -4105,6 +4135,7 @@ public int hashCode() { * @see Character#forDigit * @see #BigInteger(java.lang.String, int) */ + @SideEffectFree public String toString(@IntRange(from = 2, to = 36) int radix) { if (signum == 0) return "0"; @@ -4299,6 +4330,7 @@ private static BigInteger getRadixConversionCache(@IntRange(from = 2, to = 36) i * @see Character#forDigit * @see #BigInteger(java.lang.String) */ + @SideEffectFree public String toString() { return toString(10); } @@ -4317,6 +4349,7 @@ public String toString() { * this BigInteger. * @see #BigInteger(byte[]) */ + @SideEffectFree public byte[] toByteArray() { int byteLen = bitLength()/8 + 1; byte[] byteArray = new byte[byteLen]; @@ -4350,6 +4383,7 @@ public byte[] toByteArray() { * @see #intValueExact() * @jls 5.1.3 Narrowing Primitive Conversion */ + @Pure public @PolyValue int intValue(@PolyValue BigInteger this) { int result = 0; result = getInt(0); @@ -4372,6 +4406,7 @@ public byte[] toByteArray() { * @see #longValueExact() * @jls 5.1.3 Narrowing Primitive Conversion */ + @Pure public @PolyValue long longValue(@PolyValue BigInteger this) { long result = 0; @@ -4396,6 +4431,7 @@ public byte[] toByteArray() { * @return this BigInteger converted to a {@code float}. * @jls 5.1.3 Narrowing Primitive Conversion */ + @Pure public @PolyValue float floatValue(@PolyValue BigInteger this) { if (signum == 0) { return 0.0f; @@ -4481,6 +4517,7 @@ public byte[] toByteArray() { * @return this BigInteger converted to a {@code double}. * @jls 5.1.3 Narrowing Primitive Conversion */ + @Pure public @PolyValue double doubleValue(@PolyValue BigInteger this) { if (signum == 0) { return 0.0; @@ -4979,6 +5016,7 @@ private byte[] magSerializedForm() { * @see BigInteger#longValue * @since 1.8 */ + @Pure public long longValueExact() { if (mag.length <= 2 && bitLength() <= 63) return longValue(); @@ -4998,6 +5036,7 @@ public long longValueExact() { * @see BigInteger#intValue * @since 1.8 */ + @Pure public int intValueExact() { if (mag.length <= 1 && bitLength() <= 31) return intValue(); @@ -5017,6 +5056,7 @@ public int intValueExact() { * @see BigInteger#shortValue * @since 1.8 */ + @Pure public short shortValueExact() { if (mag.length <= 1 && bitLength() <= 31) { int value = intValue(); @@ -5038,6 +5078,7 @@ public short shortValueExact() { * @see BigInteger#byteValue * @since 1.8 */ + @Pure public byte byteValueExact() { if (mag.length <= 1 && bitLength() <= 31) { int value = intValue(); diff --git a/src/java.base/share/classes/java/util/AbstractCollection.java b/src/java.base/share/classes/java/util/AbstractCollection.java index d38628827e01a..03bb5ecee7c84 100644 --- a/src/java.base/share/classes/java/util/AbstractCollection.java +++ b/src/java.base/share/classes/java/util/AbstractCollection.java @@ -29,6 +29,7 @@ import org.checkerframework.checker.index.qual.NonNegative; import org.checkerframework.checker.index.qual.PolyGrowShrink; import org.checkerframework.checker.lock.qual.GuardSatisfied; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; import org.checkerframework.checker.nullness.qual.Nullable; @@ -276,6 +277,7 @@ private static T[] finishToArray(T[] r, Iterator it) { * @throws IllegalArgumentException {@inheritDoc} * @throws IllegalStateException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public boolean add(@GuardSatisfied AbstractCollection this, E e) { diff --git a/src/java.base/share/classes/java/util/AbstractList.java b/src/java.base/share/classes/java/util/AbstractList.java index 7997e85e864b4..055d63ec90b76 100644 --- a/src/java.base/share/classes/java/util/AbstractList.java +++ b/src/java.base/share/classes/java/util/AbstractList.java @@ -160,6 +160,7 @@ public boolean add(@GuardSatisfied AbstractList this, E e) { * @throws IllegalArgumentException {@inheritDoc} * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(@GuardSatisfied AbstractList this, @IndexFor({"this"}) int index, E element) { @@ -179,6 +180,7 @@ public E set(@GuardSatisfied AbstractList this, @IndexFor({"this"}) int index * @throws IllegalArgumentException {@inheritDoc} * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@GuardSatisfied AbstractList this, @IndexOrHigh({"this"}) int index, E element) { @@ -495,6 +497,7 @@ public void set(E e) { } } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(E e) { @@ -834,6 +837,7 @@ protected SubList(SubList parent, int fromIndex, int toIndex) { this.modCount = root.modCount; } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -855,6 +859,7 @@ public int size() { return size; } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(int index, E element) { @@ -963,6 +968,7 @@ public void set(E e) { i.set(e); } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(E e) { diff --git a/src/java.base/share/classes/java/util/AbstractSequentialList.java b/src/java.base/share/classes/java/util/AbstractSequentialList.java index a8932d5d6673d..a2e54d995b55e 100644 --- a/src/java.base/share/classes/java/util/AbstractSequentialList.java +++ b/src/java.base/share/classes/java/util/AbstractSequentialList.java @@ -28,6 +28,7 @@ import org.checkerframework.checker.index.qual.CanShrink; import org.checkerframework.checker.index.qual.PolyGrowShrink; import org.checkerframework.checker.lock.qual.GuardSatisfied; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; @@ -125,6 +126,7 @@ public E get(@GuardSatisfied AbstractSequentialList this, int index) { * @throws IllegalArgumentException {@inheritDoc} * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(@GuardSatisfied AbstractSequentialList this, int index, E element) { @@ -158,6 +160,7 @@ public E set(@GuardSatisfied AbstractSequentialList this, int index, E elemen * @throws IllegalArgumentException {@inheritDoc} * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@GuardSatisfied AbstractSequentialList this, int index, E element) { diff --git a/src/java.base/share/classes/java/util/ArrayDeque.java b/src/java.base/share/classes/java/util/ArrayDeque.java index 56490f9810600..d2ed0d7f20792 100644 --- a/src/java.base/share/classes/java/util/ArrayDeque.java +++ b/src/java.base/share/classes/java/util/ArrayDeque.java @@ -302,6 +302,7 @@ static final E nonNullElementAt(@PolyNull @PolySigned Object[] es, int i) { * @param e the element to add * @throws NullPointerException if the specified element is null */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(@GuardSatisfied ArrayDeque this, E e) { @@ -321,6 +322,7 @@ public void addFirst(@GuardSatisfied ArrayDeque this, E e) { * @param e the element to add * @throws NullPointerException if the specified element is null */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(@GuardSatisfied ArrayDeque this, E e) { @@ -435,6 +437,7 @@ public E removeLast(@GuardSatisfied @NonEmpty @CanShrink ArrayDeque this) { /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getFirst(@GuardSatisfied @NonEmpty ArrayDeque this) { E e = elementAt(elements, head); @@ -446,6 +449,7 @@ public E getFirst(@GuardSatisfied @NonEmpty ArrayDeque this) { /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getLast(@GuardSatisfied @NonEmpty ArrayDeque this) { final Object[] es = elements; diff --git a/src/java.base/share/classes/java/util/ArrayList.java b/src/java.base/share/classes/java/util/ArrayList.java index 1ec69c77e7020..278259f8c43b1 100644 --- a/src/java.base/share/classes/java/util/ArrayList.java +++ b/src/java.base/share/classes/java/util/ArrayList.java @@ -473,6 +473,7 @@ public E get(@GuardSatisfied ArrayList this, @NonNegative int index) { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getFirst() { if (size == 0) { @@ -488,6 +489,7 @@ public E getFirst() { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getLast() { int last = size - 1; @@ -507,6 +509,7 @@ public E getLast() { * @return the element previously at the specified position * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(@GuardSatisfied ArrayList this, @NonNegative int index, E element) { @@ -521,6 +524,7 @@ public E set(@GuardSatisfied ArrayList this, @NonNegative int index, E elemen * bytecode size under 35 (the -XX:MaxInlineSize default value), * which helps when add(E) is called in a C1-compiled loop. */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") private void add(E e, Object[] elementData, int s) { if (s == elementData.length) @@ -535,7 +539,6 @@ private void add(E e, Object[] elementData, int s) { * @param e element to be appended to this list * @return {@code true} (as specified by {@link Collection#add}) */ - // @SideEffectsOnly("this") @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") @@ -554,6 +557,7 @@ public boolean add(@GuardSatisfied ArrayList this, E e) { * @param element element to be inserted * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@GuardSatisfied ArrayList this, @NonNegative int index, E element) { @@ -575,6 +579,7 @@ public void add(@GuardSatisfied ArrayList this, @NonNegative int index, E ele * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E element) { @@ -586,6 +591,7 @@ public void addFirst(E element) { * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E element) { @@ -1236,6 +1242,7 @@ public void set(E e) { } } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(E e) { @@ -1318,6 +1325,7 @@ private SubList(SubList parent, int fromIndex, int toIndex) { this.modCount = parent.modCount; } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(@NonNegative int index, E element) { @@ -1341,6 +1349,7 @@ public E get(@NonNegative int index) { return size; } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@NonNegative int index, E element) { diff --git a/src/java.base/share/classes/java/util/Arrays.java b/src/java.base/share/classes/java/util/Arrays.java index 37f0a44ea8a8a..0d1be156ee7e4 100644 --- a/src/java.base/share/classes/java/util/Arrays.java +++ b/src/java.base/share/classes/java/util/Arrays.java @@ -121,6 +121,7 @@ private Arrays() {} * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(int[] a) { DualPivotQuicksort.sort(a, 0, 0, a.length); } @@ -144,6 +145,7 @@ public static void sort(int[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(int[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, 0, fromIndex, toIndex); @@ -159,6 +161,7 @@ public static void sort(int[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHig * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(long[] a) { DualPivotQuicksort.sort(a, 0, 0, a.length); } @@ -182,6 +185,7 @@ public static void sort(long[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(long[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, 0, fromIndex, toIndex); @@ -197,6 +201,7 @@ public static void sort(long[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHi * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(short[] a) { DualPivotQuicksort.sort(a, 0, a.length); } @@ -220,6 +225,7 @@ public static void sort(short[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(short[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, fromIndex, toIndex); @@ -235,6 +241,7 @@ public static void sort(short[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrH * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(char[] a) { DualPivotQuicksort.sort(a, 0, a.length); } @@ -258,6 +265,7 @@ public static void sort(char[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(char[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, fromIndex, toIndex); @@ -273,6 +281,7 @@ public static void sort(char[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHi * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(byte[] a) { DualPivotQuicksort.sort(a, 0, a.length); } @@ -296,6 +305,7 @@ public static void sort(byte[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(byte[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, fromIndex, toIndex); @@ -319,6 +329,7 @@ public static void sort(byte[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHi * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(float[] a) { DualPivotQuicksort.sort(a, 0, 0, a.length); } @@ -350,6 +361,7 @@ public static void sort(float[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(float[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, 0, fromIndex, toIndex); @@ -373,6 +385,7 @@ public static void sort(float[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrH * * @param a the array to be sorted */ + // @SideEffectsOnly("#1") public static void sort(double[] a) { DualPivotQuicksort.sort(a, 0, 0, a.length); } @@ -404,6 +417,7 @@ public static void sort(double[] a) { * @throws ArrayIndexOutOfBoundsException * if {@code fromIndex < 0} or {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(double[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); DualPivotQuicksort.sort(a, 0, fromIndex, toIndex); @@ -1060,6 +1074,7 @@ static final class LegacyMergeSort { * ordering of the array elements is found to violate the * {@link Comparable} contract */ + // @SideEffectsOnly("#1") public static void sort(@PolyInterned @PolyNull Object[] a) { if (LegacyMergeSort.userRequested) legacyMergeSort(a); @@ -1125,6 +1140,7 @@ private static void legacyMergeSort(Object[] a) { * not mutually comparable (for example, strings and * integers). */ + // @SideEffectsOnly("#1") public static void sort(@PolyInterned @PolyNull Object[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex) { rangeCheck(a.length, fromIndex, toIndex); if (LegacyMergeSort.userRequested) @@ -1249,6 +1265,7 @@ private static void swap(@UnknownSignedness Object[] x, int a, int b) { * @throws IllegalArgumentException (optional) if the comparator is * found to violate the {@link Comparator} contract */ + // @SideEffectsOnly("#1") public static void sort(@PolyNull @UnknownSignedness T[] a, @Nullable Comparator c) { if (c == null) { sort(a); @@ -1321,6 +1338,7 @@ private static void legacyMergeSort(T[] a, @Nullable Comparator c * @throws ArrayIndexOutOfBoundsException if {@code fromIndex < 0} or * {@code toIndex > a.length} */ + // @SideEffectsOnly("#1") public static void sort(T[] a, @IndexOrHigh({"#1"}) int fromIndex, @IndexOrHigh({"#1"}) int toIndex, Comparator c) { if (c == null) { diff --git a/src/java.base/share/classes/java/util/BitSet.java b/src/java.base/share/classes/java/util/BitSet.java index 8341dfa7249d0..7d9f820493654 100644 --- a/src/java.base/share/classes/java/util/BitSet.java +++ b/src/java.base/share/classes/java/util/BitSet.java @@ -548,6 +548,7 @@ public void set(@GuardSatisfied BitSet this, @NonNegative int fromIndex, @NonNeg * @throws IndexOutOfBoundsException if the specified index is negative * @since 1.0 */ + // @SideEffectsOnly("#1") public void clear(@GuardSatisfied BitSet this, @NonNegative int bitIndex) { if (bitIndex < 0) throw new IndexOutOfBoundsException("bitIndex < 0: " + bitIndex); @@ -573,6 +574,7 @@ public void clear(@GuardSatisfied BitSet this, @NonNegative int bitIndex) { * larger than {@code toIndex} * @since 1.4 */ + // @SideEffectsOnly("#1") public void clear(@GuardSatisfied BitSet this, @NonNegative int fromIndex, @NonNegative int toIndex) { checkRange(fromIndex, toIndex); @@ -616,6 +618,7 @@ public void clear(@GuardSatisfied BitSet this, @NonNegative int fromIndex, @NonN * * @since 1.4 */ + // @SideEffectsOnly("#1") public void clear(@GuardSatisfied BitSet this) { while (wordsInUse > 0) words[--wordsInUse] = 0; diff --git a/src/java.base/share/classes/java/util/Collections.java b/src/java.base/share/classes/java/util/Collections.java index 18a66f0ef8e61..8dc86ceea7187 100644 --- a/src/java.base/share/classes/java/util/Collections.java +++ b/src/java.base/share/classes/java/util/Collections.java @@ -45,10 +45,10 @@ import org.checkerframework.common.value.qual.StaticallyExecutable; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; -// import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.CFComment; import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; +// import org.checkerframework.dataflow.qual.SideEffectsOnly; import java.io.IOException; import java.io.ObjectInputStream; @@ -167,6 +167,7 @@ private Collections() { * found to violate the {@link Comparable} contract * @see List#sort(Comparator) */ + // @SideEffectsOnly("#1") public static > void sort(List list) { list.sort(null); } @@ -201,6 +202,7 @@ public static > void sort(List list) { * @see List#sort(Comparator) */ @SuppressWarnings({"unchecked", "rawtypes"}) + // @SideEffectsOnly("#1") public static void sort(List list, @Nullable Comparator c) { list.sort(c); } @@ -899,6 +901,8 @@ private static void rotate2(List list, int distance) { * its list-iterator does not support the {@code set} operation. * @since 1.4 */ + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public static boolean replaceAll(List list, @Nullable T oldVal, T newVal) { boolean result = false; int size = list.size(); @@ -1281,11 +1285,13 @@ public void addLast(E e) { throw new UnsupportedOperationException(); } + @EnsuresNonEmpty("this") @Pure public E getFirst() { return sc().getFirst(); } + @EnsuresNonEmpty("this") @Pure public E getLast() { return sc().getLast(); @@ -1617,6 +1623,7 @@ static class UnmodifiableList extends UnmodifiableCollection @Pure public E get(int index) {return list.get(index);} + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -2969,6 +2976,7 @@ public int hashCode() { public E get(int index) { synchronized (mutex) {return list.get(index);} } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -4131,6 +4139,7 @@ static class CheckedList @Pure public int lastIndexOf(Object o) { return list.lastIndexOf(o); } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -6468,6 +6477,7 @@ public static boolean disjoint(Collection c1, Collection c2) { * @since 1.5 */ @SafeVarargs + // @SideEffectsOnly("#1") public static boolean addAll(@GuardSatisfied Collection c, T... elements) { boolean result = false; for (T element : elements) @@ -6537,6 +6547,8 @@ private static class SetFromMap extends AbstractSet @Pure @EnsuresNonEmptyIf(result = true, expression = "this") public boolean contains(@UnknownSignedness Object o) { return m.containsKey(o); } + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean remove(@UnknownSignedness Object o) { return m.remove(o) != null; } @EnsuresNonEmpty("this") public boolean add(E e) { return m.put(e, Boolean.TRUE) == null; } @@ -6552,7 +6564,11 @@ private static class SetFromMap extends AbstractSet public boolean equals(Object o) { return o == this || s.equals(o); } @Pure public boolean containsAll(Collection c) {return s.containsAll(c);} + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean removeAll(Collection c) {return s.removeAll(c);} + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean retainAll(Collection c) {return s.retainAll(c);} // addAll is the only inherited implementation @@ -6662,9 +6678,7 @@ private SequencedMap map() { public void addFirst(E e) { map().putFirst(e, Boolean.TRUE); } public void addLast(E e) { map().putLast(e, Boolean.TRUE); } - @Pure public E getFirst() { return nsee(map().firstEntry()); } - @Pure public E getLast() { return nsee(map().lastEntry()); } public E removeFirst() { return nsee(map().pollFirstEntry()); } public E removeLast() { return nsee(map().pollLastEntry()); } @@ -6728,6 +6742,8 @@ static class AsLIFOQueue extends AbstractQueue @Pure @EnsuresNonEmptyIf(result = true, expression = "this") public boolean contains(@UnknownSignedness Object o) { return q.contains(o); } + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean remove(@UnknownSignedness Object o) { return q.remove(o); } @SideEffectFree public Iterator iterator() { return q.iterator(); } @@ -6738,7 +6754,11 @@ static class AsLIFOQueue extends AbstractQueue public String toString() { return q.toString(); } @Pure public boolean containsAll(Collection c) { return q.containsAll(c); } + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean removeAll(Collection c) { return q.removeAll(c); } + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean retainAll(Collection c) { return q.retainAll(c); } // We use inherited addAll; forwarding addAll would be wrong diff --git a/src/java.base/share/classes/java/util/ComparableTimSort.java b/src/java.base/share/classes/java/util/ComparableTimSort.java index 4910fffe7f4e3..ac562b868a91f 100644 --- a/src/java.base/share/classes/java/util/ComparableTimSort.java +++ b/src/java.base/share/classes/java/util/ComparableTimSort.java @@ -45,6 +45,7 @@ */ @AnnotatedFor({"index", "interning"}) @UsesObjectEquals class ComparableTimSort { +class ComparableTimSort { /** * This is the minimum sized sequence that will be merged. Shorter * sequences will be lengthened by calling binarySort. If the entire @@ -181,6 +182,7 @@ private ComparableTimSort(Object[] a, Object[] work, int workBase, int workLen) * @param workLen usable size of work array * @since 1.8 */ + // @SideEffectsOnly("#1") static void sort(Object[] a, @IndexOrHigh({"#1"}) int lo, @IndexOrHigh({"#1"}) int hi, Object[] work, int workBase, int workLen) { assert a != null && lo >= 0 && lo <= hi && hi <= a.length; diff --git a/src/java.base/share/classes/java/util/DualPivotQuicksort.java b/src/java.base/share/classes/java/util/DualPivotQuicksort.java index 191adf8e6f68b..66794e9d5ef66 100644 --- a/src/java.base/share/classes/java/util/DualPivotQuicksort.java +++ b/src/java.base/share/classes/java/util/DualPivotQuicksort.java @@ -158,6 +158,7 @@ private static int getDepth(int parallelism, int size) { * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(int[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { int size = high - low; @@ -181,6 +182,7 @@ static void sort(int[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexO * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(Sorter sorter, int[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; @@ -912,6 +914,7 @@ private static void mergeParts(Merger merger, int[] dst, int k, * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(long[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { int size = high - low; @@ -935,6 +938,7 @@ static void sort(long[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @Index * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#2") static void sort(Sorter sorter, long[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; @@ -1659,6 +1663,7 @@ private static void mergeParts(Merger merger, long[] dst, int k, * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(byte[] a, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { if (high - low > MIN_BYTE_COUNTING_SORT_SIZE) { countingSort(a, low, high); @@ -1747,6 +1752,7 @@ private static void countingSort(byte[] a, @IndexOrHigh({"#1"}) int low, @IndexO * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(char[] a, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { if (high - low > MIN_SHORT_OR_CHAR_COUNTING_SORT_SIZE) { countingSort(a, low, high); @@ -1765,6 +1771,7 @@ static void sort(char[] a, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) in * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(char[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; @@ -2066,6 +2073,7 @@ private static void countingSort(char[] a, @IndexOrHigh({"#1"}) int low, @IndexO * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(short[] a, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { if (high - low > MIN_SHORT_OR_CHAR_COUNTING_SORT_SIZE) { countingSort(a, low, high); @@ -2084,6 +2092,7 @@ static void sort(short[] a, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) i * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(short[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; @@ -2401,6 +2410,7 @@ private static void countingSort(short[] a, @IndexOrHigh({"#1"}) int low, @Index * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(float[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { /* * Phase 1. Count the number of negative zero -0.0f, @@ -2476,6 +2486,7 @@ static void sort(float[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @Inde * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#2") static void sort(Sorter sorter, float[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; @@ -3207,6 +3218,7 @@ private static void mergeParts(Merger merger, float[] dst, int k, * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#1") static void sort(double[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { /* * Phase 1. Count the number of negative zero -0.0d, @@ -3282,6 +3294,7 @@ static void sort(double[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @Ind * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ + // @SideEffectsOnly("#2") static void sort(Sorter sorter, double[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; diff --git a/src/java.base/share/classes/java/util/HashSet.java b/src/java.base/share/classes/java/util/HashSet.java index 756747e1afd26..2eaa148d90155 100644 --- a/src/java.base/share/classes/java/util/HashSet.java +++ b/src/java.base/share/classes/java/util/HashSet.java @@ -248,7 +248,6 @@ public boolean contains(@GuardSatisfied HashSet this, @GuardSatisfied @Nullab * @return {@code true} if this set did not already contain the specified * element */ - // @SideEffectsOnly("this") @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") diff --git a/src/java.base/share/classes/java/util/LinkedHashSet.java b/src/java.base/share/classes/java/util/LinkedHashSet.java index 755512641f681..668655c77eed5 100644 --- a/src/java.base/share/classes/java/util/LinkedHashSet.java +++ b/src/java.base/share/classes/java/util/LinkedHashSet.java @@ -25,6 +25,7 @@ package java.util; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.dataflow.qual.Deterministic; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; @@ -249,6 +250,7 @@ LinkedHashMap map() { * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { @@ -263,6 +265,7 @@ public void addFirst(E e) { * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { @@ -275,6 +278,7 @@ public void addLast(E e) { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getFirst() { return map().sequencedKeySet().getFirst(); @@ -286,6 +290,7 @@ public E getFirst() { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getLast() { return map().sequencedKeySet().getLast(); diff --git a/src/java.base/share/classes/java/util/LinkedList.java b/src/java.base/share/classes/java/util/LinkedList.java index 6740c068eb551..5c19476e59b46 100644 --- a/src/java.base/share/classes/java/util/LinkedList.java +++ b/src/java.base/share/classes/java/util/LinkedList.java @@ -272,6 +272,7 @@ E unlink(Node x) { * @return the first element in this list * @throws NoSuchElementException if this list is empty */ + @EnsuresNonEmpty("this") @Pure public E getFirst(@GuardSatisfied @NonEmpty LinkedList this) { final Node f = first; @@ -286,6 +287,7 @@ public E getFirst(@GuardSatisfied @NonEmpty LinkedList this) { * @return the last element in this list * @throws NoSuchElementException if this list is empty */ + @EnsuresNonEmpty("this") @Pure public E getLast(@GuardSatisfied @NonEmpty LinkedList this) { final Node l = last; @@ -329,6 +331,7 @@ public E removeLast(@GuardSatisfied @NonEmpty @CanShrink LinkedList this) { * * @param e the element to add */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(@GuardSatisfied LinkedList this, E e) { @@ -342,6 +345,7 @@ public void addFirst(@GuardSatisfied LinkedList this, E e) { * * @param e the element to add */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(@GuardSatisfied LinkedList this, E e) { @@ -547,6 +551,7 @@ public E get(@GuardSatisfied LinkedList this, @NonNegative int index) { * @return the element previously at the specified position * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(@GuardSatisfied LinkedList this, @NonNegative int index, E element) { @@ -566,6 +571,7 @@ public E set(@GuardSatisfied LinkedList this, @NonNegative int index, E eleme * @param element element to be inserted * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@GuardSatisfied LinkedList this, @NonNegative int index, E element) { @@ -1627,6 +1633,7 @@ public void add(int index, E element) { rlist.add(index, element); } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { diff --git a/src/java.base/share/classes/java/util/List.java b/src/java.base/share/classes/java/util/List.java index d67a63db81e1c..673cc619b144b 100644 --- a/src/java.base/share/classes/java/util/List.java +++ b/src/java.base/share/classes/java/util/List.java @@ -298,9 +298,9 @@ public interface List extends SequencedCollection { * prevents it from being added to this list */ @ReleasesNoLocks + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") - @EnsuresNonEmpty("this") boolean add(@GuardSatisfied List this, E e); /** @@ -649,6 +649,7 @@ default void sort(Comparator c) { * @throws IndexOutOfBoundsException if the index is out of range * ({@code index < 0 || index >= size()}) */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") E set(@GuardSatisfied List this, @IndexFor({"this"}) int index, E element); @@ -673,6 +674,7 @@ default void sort(Comparator c) { * ({@code index < 0 || index > size()}) */ @ReleasesNoLocks + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void add(@GuardSatisfied List this, @IndexOrHigh({"this"}) int index, E element); @@ -861,6 +863,7 @@ default Spliterator spliterator() { * @throws UnsupportedOperationException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addFirst(E e) { @@ -877,6 +880,7 @@ default void addFirst(E e) { * @throws UnsupportedOperationException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addLast(E e) { @@ -893,6 +897,7 @@ default void addLast(E e) { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure default E getFirst() { if (this.isEmpty()) { @@ -912,6 +917,7 @@ default E getFirst() { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure default E getLast() { if (this.isEmpty()) { diff --git a/src/java.base/share/classes/java/util/ListIterator.java b/src/java.base/share/classes/java/util/ListIterator.java index ec6b6e863346c..53d8043f5ddbc 100644 --- a/src/java.base/share/classes/java/util/ListIterator.java +++ b/src/java.base/share/classes/java/util/ListIterator.java @@ -28,6 +28,7 @@ import org.checkerframework.checker.index.qual.GTENegativeOne; import org.checkerframework.checker.index.qual.NonNegative; import org.checkerframework.checker.lock.qual.GuardSatisfied; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; import org.checkerframework.checker.nonempty.qual.NonEmpty; import org.checkerframework.dataflow.qual.Pure; @@ -218,6 +219,7 @@ public interface ListIterator extends Iterator { * @throws IllegalArgumentException if some aspect of this element * prevents it from being added to this list */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void add(@GuardSatisfied ListIterator this, E e); diff --git a/src/java.base/share/classes/java/util/NavigableSet.java b/src/java.base/share/classes/java/util/NavigableSet.java index fd6b8d14e497f..16a8bd03012fc 100644 --- a/src/java.base/share/classes/java/util/NavigableSet.java +++ b/src/java.base/share/classes/java/util/NavigableSet.java @@ -39,6 +39,7 @@ import org.checkerframework.checker.lock.qual.GuardSatisfied; import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.CFComment; @@ -111,6 +112,7 @@ public interface NavigableSet extends SortedSet { * @throws NullPointerException if the specified element is null * and this set does not permit null elements */ + @Pure @Nullable E lower(E e); /** @@ -125,6 +127,7 @@ public interface NavigableSet extends SortedSet { * @throws NullPointerException if the specified element is null * and this set does not permit null elements */ + @Pure @Nullable E floor(E e); /** @@ -139,6 +142,7 @@ public interface NavigableSet extends SortedSet { * @throws NullPointerException if the specified element is null * and this set does not permit null elements */ + @Pure @Nullable E ceiling(E e); /** @@ -153,6 +157,7 @@ public interface NavigableSet extends SortedSet { * @throws NullPointerException if the specified element is null * and this set does not permit null elements */ + @Pure @Nullable E higher(E e); /** diff --git a/src/java.base/share/classes/java/util/ReverseOrderDequeView.java b/src/java.base/share/classes/java/util/ReverseOrderDequeView.java index 19702f274b3db..6bc23f2df49fa 100644 --- a/src/java.base/share/classes/java/util/ReverseOrderDequeView.java +++ b/src/java.base/share/classes/java/util/ReverseOrderDequeView.java @@ -25,6 +25,8 @@ package java.util; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; +import org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver; import org.checkerframework.dataflow.qual.SideEffectFree; import java.util.function.Consumer; @@ -72,11 +74,16 @@ public Spliterator spliterator() { // ========== Collection ========== + @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean add(E e) { base.addFirst(e); return true; } + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean addAll(Collection c) { boolean modified = false; for (E e : c) { @@ -218,11 +225,13 @@ public E element() { return base.getLast(); } + @EnsuresNonEmpty("this") @Pure public E getFirst() { return base.getLast(); } + @EnsuresNonEmpty("this") @Pure public E getLast() { return base.getFirst(); diff --git a/src/java.base/share/classes/java/util/ReverseOrderListView.java b/src/java.base/share/classes/java/util/ReverseOrderListView.java index 1ec525c8d1a2f..7ed04e6560af7 100644 --- a/src/java.base/share/classes/java/util/ReverseOrderListView.java +++ b/src/java.base/share/classes/java/util/ReverseOrderListView.java @@ -25,6 +25,7 @@ package java.util; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; @@ -173,6 +174,9 @@ public Spliterator spliterator() { // ========== Collection ========== + @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean add(E e) { checkModifiable(); base.add(0, e); diff --git a/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java b/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java index be4109cac72e8..dcc66c7b377fc 100644 --- a/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java +++ b/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java @@ -25,6 +25,8 @@ package java.util; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; +import org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver; import org.checkerframework.dataflow.qual.SideEffectFree; import java.util.function.Consumer; @@ -125,6 +127,9 @@ public Spliterator spliterator() { // ========== Collection ========== + @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public boolean add(E e) { base.add(e); return true; diff --git a/src/java.base/share/classes/java/util/SequencedCollection.java b/src/java.base/share/classes/java/util/SequencedCollection.java index a424be88c5806..4494106fdb293 100644 --- a/src/java.base/share/classes/java/util/SequencedCollection.java +++ b/src/java.base/share/classes/java/util/SequencedCollection.java @@ -25,6 +25,7 @@ package java.util; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; @@ -108,6 +109,7 @@ public interface SequencedCollection extends Collection { * @throws UnsupportedOperationException if this collection implementation * does not support this operation */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addFirst(E e) { @@ -128,6 +130,7 @@ default void addFirst(E e) { * @throws UnsupportedOperationException if this collection implementation * does not support this operation */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addLast(E e) { @@ -146,6 +149,7 @@ default void addLast(E e) { * @return the retrieved element * @throws NoSuchElementException if this collection is empty */ + @EnsuresNonEmpty("this") @Pure default E getFirst() { return this.iterator().next(); @@ -163,6 +167,7 @@ default E getFirst() { * @return the retrieved element * @throws NoSuchElementException if this collection is empty */ + @EnsuresNonEmpty("this") @Pure default E getLast() { return this.reversed().iterator().next(); diff --git a/src/java.base/share/classes/java/util/Set.java b/src/java.base/share/classes/java/util/Set.java index 54ac68a1f87d1..3b7ca3c4c8826 100644 --- a/src/java.base/share/classes/java/util/Set.java +++ b/src/java.base/share/classes/java/util/Set.java @@ -279,6 +279,8 @@ public interface Set extends Collection { * prevents it from being added to this set */ @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") boolean add(@GuardSatisfied Set this, E e); @@ -303,6 +305,8 @@ public interface Set extends Collection { * @throws UnsupportedOperationException if the {@code remove} operation * is not supported by this set */ + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") boolean remove(@GuardSatisfied Set this, @UnknownSignedness Object o); @@ -353,6 +357,8 @@ public interface Set extends Collection { * @see #add(Object) */ @EnsuresNonEmptyIf(result = true, expression = "this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") boolean addAll(@GuardSatisfied Set this, Collection c); /** @@ -376,6 +382,8 @@ public interface Set extends Collection { * or if the specified collection is null * @see #remove(Object) */ + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") boolean retainAll(@GuardSatisfied Set this, Collection c); /** @@ -399,6 +407,8 @@ public interface Set extends Collection { * @see #remove(Object) * @see #contains(Object) */ + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") boolean removeAll(@GuardSatisfied Set this, Collection c); /** @@ -408,6 +418,8 @@ public interface Set extends Collection { * @throws UnsupportedOperationException if the {@code clear} method * is not supported by this set */ + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") void clear(@GuardSatisfied Set this); diff --git a/src/java.base/share/classes/java/util/SortedSet.java b/src/java.base/share/classes/java/util/SortedSet.java index e10b5935e9573..2be79895d49ef 100644 --- a/src/java.base/share/classes/java/util/SortedSet.java +++ b/src/java.base/share/classes/java/util/SortedSet.java @@ -26,6 +26,7 @@ package java.util; import org.checkerframework.checker.lock.qual.GuardSatisfied; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.checker.nonempty.qual.NonEmpty; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.qual.Pure; @@ -293,6 +294,7 @@ public Comparator getComparator() { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addFirst(E e) { @@ -310,6 +312,7 @@ default void addFirst(E e) { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") default void addLast(E e) { @@ -325,6 +328,7 @@ default void addLast(E e) { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure default E getFirst() { return this.first(); @@ -339,6 +343,7 @@ default E getFirst() { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure default E getLast() { return this.last(); diff --git a/src/java.base/share/classes/java/util/TreeSet.java b/src/java.base/share/classes/java/util/TreeSet.java index 9f6529637419a..b055c98102bbe 100644 --- a/src/java.base/share/classes/java/util/TreeSet.java +++ b/src/java.base/share/classes/java/util/TreeSet.java @@ -457,6 +457,7 @@ public E last(@GuardSatisfied @NonEmpty TreeSet this) { * does not permit null elements * @since 1.6 */ + @Pure public @Nullable E lower(E e) { return m.lowerKey(e); } @@ -468,6 +469,7 @@ public E last(@GuardSatisfied @NonEmpty TreeSet this) { * does not permit null elements * @since 1.6 */ + @Pure public @Nullable E floor(E e) { return m.floorKey(e); } @@ -479,6 +481,7 @@ public E last(@GuardSatisfied @NonEmpty TreeSet this) { * does not permit null elements * @since 1.6 */ + @Pure public @Nullable E ceiling(E e) { return m.ceilingKey(e); } @@ -490,6 +493,7 @@ public E last(@GuardSatisfied @NonEmpty TreeSet this) { * does not permit null elements * @since 1.6 */ + @Pure public @Nullable E higher(E e) { return m.higherKey(e); } @@ -522,6 +526,7 @@ public E last(@GuardSatisfied @NonEmpty TreeSet this) { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { @@ -536,6 +541,7 @@ public void addFirst(E e) { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { diff --git a/src/java.base/share/classes/java/util/Vector.java b/src/java.base/share/classes/java/util/Vector.java index 83d13368bd24f..e6ad52044e20c 100644 --- a/src/java.base/share/classes/java/util/Vector.java +++ b/src/java.base/share/classes/java/util/Vector.java @@ -815,6 +815,7 @@ public synchronized E get(@GuardSatisfied Vector this, @NonNegative int index * ({@code index < 0 || index >= size()}) * @since 1.2 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public synchronized E set(@GuardSatisfied Vector this, @NonNegative int index, E element) { @@ -845,7 +846,6 @@ private void add(E e, Object[] elementData, int s) { * @return {@code true} (as specified by {@link Collection#add}) * @since 1.2 */ - // @SideEffectsOnly("this") @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") @@ -883,6 +883,7 @@ public boolean remove(@GuardSatisfied @CanShrink Vector this, @GuardSatisfied * ({@code index < 0 || index > size()}) * @since 1.2 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(@GuardSatisfied Vector this, @NonNegative int index, E element) { diff --git a/src/java.base/share/classes/java/util/concurrent/BlockingDeque.java b/src/java.base/share/classes/java/util/concurrent/BlockingDeque.java index 5f626cc338dbf..1053664f403a4 100644 --- a/src/java.base/share/classes/java/util/concurrent/BlockingDeque.java +++ b/src/java.base/share/classes/java/util/concurrent/BlockingDeque.java @@ -232,6 +232,7 @@ public interface BlockingDeque extends BlockingQueue< * @throws NullPointerException if the specified element is null * @throws IllegalArgumentException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void addFirst(E e); @@ -249,6 +250,7 @@ public interface BlockingDeque extends BlockingQueue< * @throws NullPointerException if the specified element is null * @throws IllegalArgumentException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void addLast(E e); @@ -488,9 +490,9 @@ boolean offerLast(E e, long timeout, TimeUnit unit) * @throws IllegalArgumentException if some property of the specified * element prevents it from being added to this deque */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") - @EnsuresNonEmpty("this") boolean add(E e); /** diff --git a/src/java.base/share/classes/java/util/concurrent/ConcurrentLinkedDeque.java b/src/java.base/share/classes/java/util/concurrent/ConcurrentLinkedDeque.java index ce2d2a01ebd73..194c51b91fbdc 100644 --- a/src/java.base/share/classes/java/util/concurrent/ConcurrentLinkedDeque.java +++ b/src/java.base/share/classes/java/util/concurrent/ConcurrentLinkedDeque.java @@ -843,6 +843,7 @@ private void initHeadTail(Node h, Node t) { * * @throws NullPointerException if the specified element is null */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { @@ -858,6 +859,7 @@ public void addFirst(E e) { * * @throws NullPointerException if the specified element is null */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { @@ -929,6 +931,7 @@ public boolean offerLast(E e) { /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getFirst(@NonEmpty ConcurrentLinkedDeque this) { return screenNullResult(peekFirst()); @@ -937,6 +940,7 @@ public E getFirst(@NonEmpty ConcurrentLinkedDeque this) { /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getLast(@NonEmpty ConcurrentLinkedDeque this) { return screenNullResult(peekLast()); diff --git a/src/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.java b/src/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.java index b9bd22662ded4..d9ef6c3e3c871 100644 --- a/src/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.java +++ b/src/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.java @@ -378,6 +378,7 @@ public boolean removeAll(Collection this) { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { throw new UnsupportedOperationException(); } @@ -464,6 +471,9 @@ public void addFirst(E e) { * @throws UnsupportedOperationException always * @since 21 */ + @EnsuresNonEmpty("this") + // @SideEffectsOnly("this") + @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { throw new UnsupportedOperationException(); } diff --git a/src/java.base/share/classes/java/util/concurrent/CopyOnWriteArrayList.java b/src/java.base/share/classes/java/util/concurrent/CopyOnWriteArrayList.java index 00dc6b4eecd45..03e5369e1ed7b 100644 --- a/src/java.base/share/classes/java/util/concurrent/CopyOnWriteArrayList.java +++ b/src/java.base/share/classes/java/util/concurrent/CopyOnWriteArrayList.java @@ -440,6 +440,7 @@ public E get(int index) { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getFirst() { Object[] es = getArray(); @@ -455,6 +456,7 @@ public E getFirst() { * @throws NoSuchElementException {@inheritDoc} * @since 21 */ + @EnsuresNonEmpty("this") @Pure public E getLast() { Object[] es = getArray(); @@ -470,6 +472,7 @@ public E getLast() { * * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -514,6 +517,7 @@ public boolean add(E e) { * * @throws IndexOutOfBoundsException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void add(int index, E element) { @@ -542,6 +546,7 @@ public void add(int index, E element) { * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { @@ -553,6 +558,7 @@ public void addFirst(E e) { * * @since 21 */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { @@ -1528,6 +1534,7 @@ public boolean equals(Object o) { return !it.hasNext(); } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { @@ -1549,6 +1556,7 @@ public E get(int index) { } } + @EnsuresNonEmpty("this") @Pure public E getFirst() { synchronized (lock) { @@ -1559,6 +1567,7 @@ public E getFirst() { } } + @EnsuresNonEmpty("this") @Pure public E getLast() { synchronized (lock) { @@ -2184,6 +2193,7 @@ public E get(int i) { } } + @EnsuresNonEmpty("this") @Pure public E getFirst() { synchronized (lock) { @@ -2195,6 +2205,7 @@ public E getFirst() { } } + @EnsuresNonEmpty("this") @Pure public E getLast() { synchronized (lock) { @@ -2277,6 +2288,7 @@ public void sort(Comparator c) { base.sort(Collections.reverseOrder(c)); } + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public E set(int index, E element) { diff --git a/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java b/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java index f928042e2d12e..5caaae6800f5d 100644 --- a/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java +++ b/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java @@ -333,6 +333,7 @@ void unlink(@CanShrink LinkedBlockingDeque this, Node x) { * @throws IllegalStateException if this deque is full * @throws NullPointerException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addFirst(E e) { @@ -344,6 +345,7 @@ public void addFirst(E e) { * @throws IllegalStateException if this deque is full * @throws NullPointerException {@inheritDoc} */ + @EnsuresNonEmpty("this") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") public void addLast(E e) { @@ -592,6 +594,7 @@ public E takeLast(@GuardSatisfied @CanShrink LinkedBlockingDeque this) throws /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getFirst(@NonEmpty LinkedBlockingDeque this) { E x = peekFirst(); @@ -602,6 +605,7 @@ public E getFirst(@NonEmpty LinkedBlockingDeque this) { /** * @throws NoSuchElementException {@inheritDoc} */ + @EnsuresNonEmpty("this") @Pure public E getLast(@NonEmpty LinkedBlockingDeque this) { E x = peekLast(); From 4fd7c3e4fc86e992de9f296fa2212f336db5c35d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 25 May 2026 22:03:56 -0700 Subject: [PATCH 2/4] Fixes --- src/java.base/share/classes/java/util/ComparableTimSort.java | 2 +- src/java.base/share/classes/java/util/DualPivotQuicksort.java | 2 +- src/java.base/share/classes/java/util/ListIterator.java | 4 ++-- src/java.base/share/classes/java/util/TreeMap.java | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/java.base/share/classes/java/util/ComparableTimSort.java b/src/java.base/share/classes/java/util/ComparableTimSort.java index ac562b868a91f..3bd6a8ba36ea4 100644 --- a/src/java.base/share/classes/java/util/ComparableTimSort.java +++ b/src/java.base/share/classes/java/util/ComparableTimSort.java @@ -44,7 +44,7 @@ * @author Josh Bloch */ @AnnotatedFor({"index", "interning"}) -@UsesObjectEquals class ComparableTimSort { +@UsesObjectEquals class ComparableTimSort { /** * This is the minimum sized sequence that will be merged. Shorter diff --git a/src/java.base/share/classes/java/util/DualPivotQuicksort.java b/src/java.base/share/classes/java/util/DualPivotQuicksort.java index 66794e9d5ef66..5e982d8b86c50 100644 --- a/src/java.base/share/classes/java/util/DualPivotQuicksort.java +++ b/src/java.base/share/classes/java/util/DualPivotQuicksort.java @@ -182,7 +182,7 @@ static void sort(int[] a, int parallelism, @IndexOrHigh({"#1"}) int low, @IndexO * @param low the index of the first element, inclusive, to be sorted * @param high the index of the last element, exclusive, to be sorted */ - // @SideEffectsOnly("#1") + // @SideEffectsOnly("#2") static void sort(Sorter sorter, int[] a, int bits, @IndexOrHigh({"#1"}) int low, @IndexOrHigh({"#1"}) int high) { while (true) { int end = high - 1, size = high - low; diff --git a/src/java.base/share/classes/java/util/ListIterator.java b/src/java.base/share/classes/java/util/ListIterator.java index 53d8043f5ddbc..d87daa97194e5 100644 --- a/src/java.base/share/classes/java/util/ListIterator.java +++ b/src/java.base/share/classes/java/util/ListIterator.java @@ -32,10 +32,10 @@ import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; import org.checkerframework.checker.nonempty.qual.NonEmpty; import org.checkerframework.dataflow.qual.Pure; -// import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.CFComment; import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; +// import org.checkerframework.dataflow.qual.SideEffectsOnly; /** * An iterator for lists that allows the programmer @@ -219,7 +219,7 @@ public interface ListIterator extends Iterator { * @throws IllegalArgumentException if some aspect of this element * prevents it from being added to this list */ - @EnsuresNonEmpty("this") + @CFComment("Not @EnsuresNonEmpty(this) because this adds *before* the cursor." // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void add(@GuardSatisfied ListIterator this, E e); diff --git a/src/java.base/share/classes/java/util/TreeMap.java b/src/java.base/share/classes/java/util/TreeMap.java index e11638f940254..a0bbfe7827266 100644 --- a/src/java.base/share/classes/java/util/TreeMap.java +++ b/src/java.base/share/classes/java/util/TreeMap.java @@ -347,7 +347,7 @@ public boolean containsValue(@GuardSatisfied TreeMap this, @GuardSatisfied */ // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") - public V putFirst(K k, V v) { + public V putFirst(K k, V v) { throw new UnsupportedOperationException(); } From 7b82ab1a0bccb1c010a73e0ea4aeacb12e0e6630 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 26 May 2026 07:32:50 -0700 Subject: [PATCH 3/4] Fix --- src/java.base/share/classes/java/util/ListIterator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java.base/share/classes/java/util/ListIterator.java b/src/java.base/share/classes/java/util/ListIterator.java index d87daa97194e5..f90196023af63 100644 --- a/src/java.base/share/classes/java/util/ListIterator.java +++ b/src/java.base/share/classes/java/util/ListIterator.java @@ -219,7 +219,7 @@ public interface ListIterator extends Iterator { * @throws IllegalArgumentException if some aspect of this element * prevents it from being added to this list */ - @CFComment("Not @EnsuresNonEmpty(this) because this adds *before* the cursor." + @CFComment("Not @EnsuresNonEmpty(this) because this adds *before* the cursor.") // @SideEffectsOnly("this") @DoesNotUnrefineReceiver("modifiability") void add(@GuardSatisfied ListIterator this, E e); From 2a483d403c9d954172bb04405efb3c7f54428195 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 26 May 2026 07:55:39 -0700 Subject: [PATCH 4/4] Fix imports --- src/java.base/share/classes/java/lang/StrictMath.java | 1 - .../share/classes/java/util/ReverseOrderDequeView.java | 2 +- .../share/classes/java/util/ReverseOrderSortedSetView.java | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/java.base/share/classes/java/lang/StrictMath.java b/src/java.base/share/classes/java/lang/StrictMath.java index 004c84384ddfc..638c454e17677 100644 --- a/src/java.base/share/classes/java/lang/StrictMath.java +++ b/src/java.base/share/classes/java/lang/StrictMath.java @@ -1692,7 +1692,6 @@ public static int abs(int a) { * @since 15 */ @Pure - @Pure @StaticallyExecutable public static int absExact(int a) { return Math.absExact(a); diff --git a/src/java.base/share/classes/java/util/ReverseOrderDequeView.java b/src/java.base/share/classes/java/util/ReverseOrderDequeView.java index 6bc23f2df49fa..9c8c6c3c3d6b4 100644 --- a/src/java.base/share/classes/java/util/ReverseOrderDequeView.java +++ b/src/java.base/share/classes/java/util/ReverseOrderDequeView.java @@ -26,8 +26,8 @@ package java.util; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; -import org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; import java.util.function.Consumer; import java.util.function.IntFunction; diff --git a/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java b/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java index dcc66c7b377fc..4c32525c02e26 100644 --- a/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java +++ b/src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java @@ -26,8 +26,8 @@ package java.util; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; -import org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; import java.util.function.Consumer; import java.util.function.IntFunction;