Side-effect annotations

Author: mernst

README.md

@@ -159,6 +159,7 @@ merge conflicts.)
 ```sh
 cd jdk21u
 git pull && \
+git pull ../jdk && \
 git pull https://github.com/openjdk/jdk21u.git && \
 git pull https://github.com/typetools/jdk.git
 ```

src/java.base/share/classes/java/lang/AbstractStringBuilder.java

@@ -35,6 +35,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 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 jdk.internal.math.DoubleToDecimal;
@@ -521,6 +522,7 @@ public int codePointBefore(@Positive int index) {
      *             {@code dst.length}
      *             </ul>
      */
+    @SideEffectsOnly("#3")
     public void getChars(@NonNegative int srcBegin, @NonNegative int srcEnd, char[] dst, @IndexOrHigh({"#3"}) int dstBegin)
     {
         Preconditions.checkFromToIndex(srcBegin, srcEnd, count, Preconditions.SIOOBE_FORMATTER);  // compatible to old version

src/java.base/share/classes/java/lang/String.java

@@ -56,6 +56,7 @@
 import org.checkerframework.common.value.qual.StringVal;
 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;
 
@@ -1787,6 +1788,7 @@ public int codePointBefore(@LTEqLengthOf({"this"}) @Positive int index) {
      *            <li>{@code dstBegin+(srcEnd-srcBegin)} is larger than
      *                {@code dst.length}</ul>
      */
+    @SideEffectsOnly("#3")
     public void getChars(@IndexOrHigh({"this"}) int srcBegin, @IndexOrHigh({"this"}) int srcEnd, char @GuardSatisfied [] dst, @IndexOrHigh({"#3"}) int dstBegin) {
         checkBoundsBeginEnd(srcBegin, srcEnd, length());
         checkBoundsOffCount(dstBegin, srcEnd - srcBegin, dst.length);
@@ -2174,6 +2176,7 @@ private static class CaseInsensitiveComparator
         @java.io.Serial
         private static final long serialVersionUID = 8575799808933029326L;
 
+        @Pure
         public int compare(String s1, String s2) {
             byte[] v1 = s1.value;
             byte[] v2 = s2.value;
@@ -2617,6 +2620,7 @@ public int hashCode() {
      *          {@code endIndex}.
      * @since   21
      */
+    @Pure
     public int indexOf(int ch, int beginIndex, int endIndex) {
         checkBoundsBeginEnd(beginIndex, endIndex, length());
         return isLatin1() ? StringLatin1.indexOf(value, ch, beginIndex, endIndex)
@@ -2781,6 +2785,7 @@ public int indexOf(int ch, int beginIndex, int endIndex) {
      *          {@code endIndex}.
      * @since   21
      */
+    @Pure
     public int indexOf(String str, int beginIndex, int endIndex) {
         if (str.length() == 1) {
             /* Simple optimization, can be omitted without behavioral impact */
@@ -3474,6 +3479,7 @@ public String replace(@GuardSatisfied CharSequence target, @GuardSatisfied CharS
      *
      * @since   21
      */
+    @SideEffectFree
     public String[] splitWithDelimiters(String regex, int limit) {
         return split(regex, limit, true);
     }
@@ -4094,6 +4100,7 @@ public boolean isBlank() {
      *
      * @since 11
      */
+    @SideEffectFree
     public Stream<String> lines() {
         return isLatin1() ? StringLatin1.lines(value) : StringUTF16.lines(value);
     }
@@ -4491,6 +4498,7 @@ public <R> R transform(Function<? super String, ? extends R> f) {
      * @return an IntStream of char values from this sequence
      * @since 9
      */
+    @SideEffectFree
     @Override
     public IntStream chars() {
         return StreamSupport.intStream(
@@ -4511,6 +4519,7 @@ public IntStream chars() {
      * @return an IntStream of Unicode code points from this sequence
      * @since 9
      */
+    @SideEffectFree
     @Override
     public IntStream codePoints() {
         return StreamSupport.intStream(
@@ -5113,6 +5122,7 @@ static String valueOfCodePoint(int codePoint) {
      * @return an {@link Optional} describing the {@linkplain String} instance
      * @since 12
      */
+    @SideEffectFree
     @Override
     public Optional<String> describeConstable() {
         return Optional.of(this);
@@ -5126,6 +5136,7 @@ public Optional<String> describeConstable() {
      * @return the {@linkplain String} instance
      * @since 12
      */
+    @Pure
     @Override
     public String resolveConstantDesc(MethodHandles.Lookup lookup) {
         return this;

src/java.base/share/classes/java/lang/StringBuffer.java

@@ -35,6 +35,7 @@
 import org.checkerframework.common.aliasing.qual.Unique;
 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 java.io.IOException;
@@ -208,6 +209,7 @@ public final class StringBuffer
      *
      * @since 11
      */
+    @SideEffectFree
     @Override
     public synchronized int compareTo(StringBuffer another) {
         return super.compareTo(another);
@@ -219,6 +221,7 @@ public synchronized int compareTo(StringBuffer another) {
         return count;
     }
 
+    @Pure
     @Override
     public synchronized @NonNegative int capacity() {
         return super.capacity();
@@ -252,6 +255,7 @@ public synchronized void setLength(@NonNegative int newLength) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @see        #length()
      */
+    @Pure
     @Override
     public synchronized char charAt(int index) {
         return super.charAt(index);
@@ -261,6 +265,7 @@ public synchronized char charAt(int index) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @since      1.5
      */
+    @Pure
     @Override
     public synchronized int codePointAt(int index) {
         return super.codePointAt(index);
@@ -270,6 +275,7 @@ public synchronized int codePointAt(int index) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @since     1.5
      */
+    @Pure
     @Override
     public synchronized int codePointBefore(int index) {
         return super.codePointBefore(index);
@@ -279,6 +285,7 @@ public synchronized int codePointBefore(int index) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @since     1.5
      */
+    @Pure
     @Override
     public synchronized int codePointCount(int beginIndex, int endIndex) {
         return super.codePointCount(beginIndex, endIndex);
@@ -288,6 +295,7 @@ public synchronized int codePointCount(int beginIndex, int endIndex) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @since     1.5
      */
+    @Pure
     @Override
     public synchronized int offsetByCodePoints(int index, int codePointOffset) {
         return super.offsetByCodePoints(index, codePointOffset);
@@ -296,6 +304,7 @@ public synchronized int offsetByCodePoints(int index, int codePointOffset) {
     /**
      * @throws IndexOutOfBoundsException {@inheritDoc}
      */
+    @SideEffectsOnly("#3")
     @Override
     public synchronized void getChars(int srcBegin, int srcEnd, char[] dst,
                                       @IndexOrHigh({"#3"}) int dstBegin)
@@ -516,6 +525,7 @@ public synchronized StringBuffer replace(int start, int end, String str) {
      * @throws StringIndexOutOfBoundsException {@inheritDoc}
      * @since      1.2
      */
+    @SideEffectFree
     @Override
     public synchronized String substring(int start) {
         return substring(start, count);
@@ -525,6 +535,7 @@ public synchronized String substring(int start) {
      * @throws IndexOutOfBoundsException {@inheritDoc}
      * @since      1.4
      */
+    @SideEffectFree
     @Override
     public synchronized CharSequence subSequence(int start, int end) {
         return super.substring(start, end);
@@ -534,6 +545,7 @@ public synchronized CharSequence subSequence(int start, int end) {
      * @throws StringIndexOutOfBoundsException {@inheritDoc}
      * @since      1.2
      */
+    @SideEffectFree
     @Override
     public synchronized String substring(int start, int end) {
         return super.substring(start, end);
@@ -749,6 +761,7 @@ public synchronized StringBuffer repeat(CharSequence cs, int count) {
         return this;
     }
 
+    @SideEffectFree
     @Override
     @IntrinsicCandidate
     public synchronized String toString(@GuardSatisfied StringBuffer this) {

src/java.base/share/classes/java/lang/StringBuilder.java

@@ -176,6 +176,7 @@ public StringBuilder(CharSequence seq) {
      *
      * @since 11
      */
+    @SideEffectFree
     @Override
     public int compareTo(StringBuilder another) {
         return super.compareTo(another);
@@ -498,6 +499,7 @@ public StringBuilder reverse() {
      *
      * @since 21
      */
+    @SideEffectsOnly("this")
     @Override
     @SideEffectFree
     public StringBuilder repeat(int codePoint, int count) {
@@ -510,12 +512,14 @@ public StringBuilder repeat(int codePoint, int count) {
      *
      * @since 21
      */
+    @SideEffectsOnly("this")
     @Override
     public StringBuilder repeat(CharSequence cs, int count) {
         super.repeat(cs, count);
         return this;
     }
 
+    @SideEffectFree
     @Override
     @IntrinsicCandidate
     public @PolyRegex String toString(@GuardSatisfied @PolyRegex StringBuilder this) {

src/java.base/share/classes/java/lang/StringLatin1.java

@@ -25,6 +25,8 @@
 
 package java.lang;
 
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+
 import java.util.Arrays;
 import java.util.Locale;
 import java.util.Spliterator;
@@ -79,6 +81,7 @@ public static byte[] inflate(byte[] value, int off, int len) {
         return ret;
     }
 
+    @SideEffectsOnly("#3")
     public static void getChars(byte[] value, int srcBegin, int srcEnd, char[] dst, int dstBegin) {
         inflate(value, srcBegin, dst, dstBegin, srcEnd - srcBegin);
     }

src/java.base/share/classes/java/lang/StringUTF16.java

@@ -25,6 +25,8 @@
 
 package java.lang;
 
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+
 import java.util.Arrays;
 import java.util.Locale;
 import java.util.Spliterator;
@@ -247,6 +249,7 @@ static byte[] toBytesSupplementary(int cp) {
     }
 
     @IntrinsicCandidate
+    @SideEffectsOnly("#3")
     public static void getChars(byte[] value, int srcBegin, int srcEnd, char[] dst, int dstBegin) {
         // We need a range check here because 'getChar' has no checks
         if (srcBegin < srcEnd) {

src/java.base/share/classes/java/util/EnumMap.java

@@ -39,7 +39,6 @@
 import org.checkerframework.checker.signedness.qual.UnknownSignedness;
 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;
 

src/java.base/share/classes/jdk/internal/icu/text/Replaceable.java

@@ -37,6 +37,9 @@
 
 package jdk.internal.icu.text;
 
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+
 /**
  * <code>Replaceable</code> is an interface representing a
  * string of characters that supports the replacement of a range of
@@ -117,5 +120,6 @@ public interface Replaceable {
      * @param dstStart the start offset in the destination array.
      * @stable ICU 2.0
      */
+    @SideEffectsOnly("#3")
     void getChars(int srcStart, int srcLimit, char dst[], int dstStart);
 }

src/java.base/share/classes/jdk/internal/icu/text/ReplaceableString.java

@@ -32,6 +32,9 @@
 
 package jdk.internal.icu.text;
 
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+
 /**
  * <code>ReplaceableString</code> is an adapter class that implements the
  * <code>Replaceable</code> API around an ordinary <code>StringBuffer</code>.
@@ -110,6 +113,7 @@ public char charAt(int offset) {
      * @param dstStart the start offset in the destination array.
      * @stable ICU 2.0
      */
+    @SideEffectsOnly("#3")
     public void getChars(int srcStart, int srcLimit, char dst[], int dstStart) {
         if (srcStart != srcLimit) {
             buf.getChars(srcStart, srcLimit, dst, dstStart);