Add PICO annotation

src/java.base/share/classes/java/io/File.java

@@ -30,11 +30,14 @@
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.lock.qual.ReleasesNoLocks;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.checker.regex.qual.Regex;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.CFComment;
+import org.checkerframework.framework.qual.DefaultQualifierForUse;
 
 import java.net.URI;
 import java.net.URL;
@@ -162,7 +165,8 @@
 "EnsuresNonNullIf(expression={\"list()\",\"list(FilenameFilter)\",\"listFiles()\",\"listFiles(FilenameFilter)\",\"listFiles(FileFilter)\"}, result=true)\""
 })
 @AnnotatedFor({"index", "initialization", "interning", "lock", "nullness"})
-public class File
+@DefaultQualifierForUse(Readonly.class)
+public @ReceiverDependentMutable class File
     implements Serializable, Comparable<File>
 {
 

src/java.base/share/classes/java/io/FileInputStream.java

@@ -31,6 +31,8 @@
 import org.checkerframework.checker.index.qual.LTLengthOf;
 import org.checkerframework.checker.index.qual.NonNegative;
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 import java.nio.channels.FileChannel;
@@ -70,6 +72,7 @@
  * @since   1.0
  */
 @AnnotatedFor({"index", "initialization", "mustcall", "nullness"})
+@ReceiverDependentMutable
 public class FileInputStream extends InputStream
 {
     private static final int DEFAULT_BUFFER_SIZE = 8192;
@@ -147,7 +150,7 @@ public FileInputStream(String name) throws FileNotFoundException {
      * @see        java.io.File#getPath()
      * @see        java.lang.SecurityManager#checkRead(java.lang.String)
      */
-    public FileInputStream(File file) throws FileNotFoundException {
+    public @ReceiverDependentMutable FileInputStream(@Readonly File file) throws FileNotFoundException {
         String name = (file != null ? file.getPath() : null);
         @SuppressWarnings("removal")
         SecurityManager security = System.getSecurityManager();

src/java.base/share/classes/java/io/ObjectOutputStream.java

@@ -30,6 +30,7 @@
 import org.checkerframework.checker.index.qual.NonNegative;
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.checker.signedness.qual.PolySigned;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
@@ -354,7 +355,7 @@ public void useProtocolVersion(int version) throws IOException {
      * @throws  IOException Any exception thrown by the underlying
      *          OutputStream.
      */
-    public final void writeObject(@Nullable Object obj) throws IOException {
+    public final void writeObject(@Readonly @Nullable Object obj) throws IOException {
         if (enableOverride) {
             writeObjectOverride(obj);
             return;

src/java.base/share/classes/java/io/PrintStream.java

@@ -34,6 +34,8 @@
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
 import org.checkerframework.checker.mustcall.qual.NotOwning;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
 import org.checkerframework.checker.signedness.qual.PolySigned;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.CFComment;
@@ -75,7 +77,7 @@
 
 @CFComment({"lock: TODO: Should parameters be @GuardSatisfied, or is the default of @GuardedBy({}) appropriate? (@GuardedBy({}) is more conservative.)"})
 @AnnotatedFor({"formatter", "i18n", "index", "initialization", "lock", "mustcall", "nullness", "signedness"})
-public class PrintStream extends FilterOutputStream
+public @ReceiverDependentMutable class PrintStream extends FilterOutputStream
     implements Appendable, Closeable
 {
 
@@ -888,7 +890,7 @@ public void print(@GuardSatisfied PrintStream this, @Nullable String s) {
      * @param      obj   The {@code Object} to be printed
      * @see        java.lang.Object#toString()
      */
-    public void print(@GuardSatisfied PrintStream this, @Nullable Object obj) {
+    public void print(@GuardSatisfied PrintStream this, @Nullable @Readonly Object obj) {
         write(String.valueOf(obj));
     }
 
@@ -1058,7 +1060,7 @@ public void println(@GuardSatisfied PrintStream this, @Nullable @Localized Strin
      *
      * @param x  The {@code Object} to be printed.
      */
-    public void println(@GuardSatisfied PrintStream this, @Nullable Object x) {
+    public void println(@GuardSatisfied PrintStream this, @Nullable @Readonly Object x) {
         String s = String.valueOf(x);
         if (getClass() == PrintStream.class) {
             // need to apply String.valueOf again since first invocation
@@ -1118,7 +1120,7 @@ public void println(@GuardSatisfied PrintStream this, @Nullable Object x) {
      */
     @CFComment({"lock/nullness: The vararg arrays can actually be null, but let's not annotate them because passing null is bad style; see whether this annotation is useful."})
     @FormatMethod
-    public @NotOwning PrintStream printf(@GuardSatisfied PrintStream this, String format, @Nullable Object ... args) {
+    public @NotOwning PrintStream printf(@GuardSatisfied PrintStream this, String format, @Nullable @Readonly Object ... args) {
         return format(format, args);
     }
 
@@ -1171,7 +1173,7 @@ public void println(@GuardSatisfied PrintStream this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @NotOwning PrintStream printf(@GuardSatisfied PrintStream this, @Nullable Locale l, String format, @Nullable Object ... args) {
+    public @NotOwning PrintStream printf(@GuardSatisfied PrintStream this, @Nullable Locale l, String format, @Nullable @Readonly Object ... args) {
         return format(l, format, args);
     }
 
@@ -1277,7 +1279,7 @@ public void println(@GuardSatisfied PrintStream this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @NotOwning PrintStream format(@GuardSatisfied PrintStream this, @Nullable Locale l, String format, @Nullable Object ... args) {
+    public @NotOwning PrintStream format(@GuardSatisfied PrintStream this, @Nullable Locale l, String format, @Nullable @Readonly Object ... args) {
         try {
             synchronized (this) {
                 ensureOpen();

src/java.base/share/classes/java/io/PrintWriter.java

@@ -32,6 +32,9 @@
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
+
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 import java.util.Objects;
@@ -68,7 +71,7 @@
  */
 
 @AnnotatedFor({"formatter", "index", "initialization", "lock", "mustcall", "nullness"})
-public class PrintWriter extends Writer {
+public @ReceiverDependentMutable class PrintWriter extends Writer {
 
     /**
      * The underlying character-output stream of this
@@ -705,7 +708,7 @@ public void print(@GuardSatisfied PrintWriter this, @Nullable String s) {
      * @param      obj   The {@code Object} to be printed
      * @see        java.lang.Object#toString()
      */
-    public void print(@GuardSatisfied PrintWriter this, @Nullable Object obj) {
+    public void print(@GuardSatisfied PrintWriter this, @Nullable @Readonly Object obj) {
         write(String.valueOf(obj));
     }
 
@@ -841,7 +844,7 @@ public void println(@GuardSatisfied PrintWriter this, @Nullable String x) {
      *
      * @param x  The {@code Object} to be printed.
      */
-    public void println(@GuardSatisfied PrintWriter this, @Nullable Object x) {
+    public void println(@GuardSatisfied PrintWriter this, @Nullable @Readonly Object x) {
         String s = String.valueOf(x);
         synchronized (lock) {
             print(s);
@@ -894,7 +897,7 @@ public void println(@GuardSatisfied PrintWriter this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @MustCallAlias PrintWriter printf(@GuardSatisfied @MustCallAlias PrintWriter this, String format, @Nullable Object ... args) {
+    public @MustCallAlias PrintWriter printf(@GuardSatisfied @MustCallAlias PrintWriter this, String format, @Nullable @Readonly Object ... args) {
         return format(format, args);
     }
 
@@ -948,7 +951,7 @@ public void println(@GuardSatisfied PrintWriter this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @MustCallAlias PrintWriter printf(@GuardSatisfied @MustCallAlias PrintWriter this, @Nullable Locale l, String format, @Nullable Object ... args) {
+    public @MustCallAlias PrintWriter printf(@GuardSatisfied @MustCallAlias PrintWriter this, @Nullable Locale l, String format, @Nullable @Readonly Object ... args) {
         return format(l, format, args);
     }
 
@@ -993,7 +996,7 @@ public void println(@GuardSatisfied PrintWriter this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @MustCallAlias PrintWriter format(@GuardSatisfied @MustCallAlias PrintWriter this, String format, @Nullable Object ... args) {
+    public @MustCallAlias PrintWriter format(@GuardSatisfied @MustCallAlias PrintWriter this, String format, @Nullable @Readonly Object ... args) {
         try {
             synchronized (lock) {
                 ensureOpen();
@@ -1054,7 +1057,7 @@ public void println(@GuardSatisfied PrintWriter this, @Nullable Object x) {
      * @since  1.5
      */
     @FormatMethod
-    public @MustCallAlias PrintWriter format(@GuardSatisfied @MustCallAlias PrintWriter this, @Nullable Locale l, String format, @Nullable Object ... args) {
+    public @MustCallAlias PrintWriter format(@GuardSatisfied @MustCallAlias PrintWriter this, @Nullable Locale l, String format, @Nullable @Readonly Object ... args) {
         try {
             synchronized (lock) {
                 ensureOpen();

src/java.base/share/classes/java/io/Serializable.java

@@ -24,6 +24,7 @@
  */
 
 package java.io;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
 
 /**
  * Serializability of a class is enabled by the class implementing the
@@ -190,5 +191,6 @@
  *      <cite>Java Object Serialization Specification</cite></a>
  * @since   1.1
  */
+@ReceiverDependentMutable
 public interface Serializable {
 }

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

@@ -33,6 +33,7 @@
 import org.checkerframework.checker.interning.qual.UsesObjectEquals;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Mutable;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
@@ -68,7 +69,7 @@
  * @since       1.5
  */
 @AnnotatedFor({"index", "initialization", "interning", "lock", "nullness"})
-abstract @UsesObjectEquals class AbstractStringBuilder implements Appendable, CharSequence {
+abstract @UsesObjectEquals @Mutable class AbstractStringBuilder implements Appendable, CharSequence {
     /**
      * The value is used for character storage.
      */

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

@@ -32,10 +32,13 @@
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;
 import org.checkerframework.checker.nonempty.qual.NonEmpty;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
+import org.checkerframework.checker.pico.qual.Readonly;
 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.DefaultQualifierForUse;
 
 import java.util.NoSuchElementException;
 import java.util.Objects;
@@ -69,7 +72,8 @@
  */
 
 @AnnotatedFor({"lock", "nullness", "index"})
-public interface CharSequence {
+@DefaultQualifierForUse(Readonly.class)
+public @ReceiverDependentMutable interface CharSequence {
 
     /**
      * Returns the length of this character sequence.  The length is the number

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

@@ -25,6 +25,7 @@
 
 package java.lang;
 
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 /**
@@ -52,5 +53,5 @@
  * @since   1.0
  */
 @AnnotatedFor({"nullness"})
-public interface Cloneable {
+public @ReceiverDependentMutable interface Cloneable {
 }

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

@@ -27,6 +27,8 @@
 
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.CFComment;
@@ -110,7 +112,7 @@
  * @since 1.2
  */
 @AnnotatedFor({"lock", "nullness", "index"})
-public interface Comparable<T extends @NonNull Object> {
+public @ReceiverDependentMutable interface Comparable<T extends @NonNull Object> {
     /**
      * Compares this object with the specified object for order.  Returns a
      * negative integer, zero, or a positive integer as this object is less
@@ -148,5 +150,5 @@ public interface Comparable<T extends @NonNull Object> {
      */
     @CFComment("nullness: arguments may NOT be null")
     @Pure
-    public int compareTo(@GuardSatisfied Comparable<T> this, @NonNull T o);
+    public int compareTo(@Readonly @GuardSatisfied Comparable<T> this, @NonNull T o);
 }

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

@@ -26,6 +26,7 @@
 package java.lang;
 
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
@@ -39,7 +40,7 @@
  * @since 1.0
  */
 @AnnotatedFor({"nullness"})
-public class IndexOutOfBoundsException extends RuntimeException {
+public @ReceiverDependentMutable class IndexOutOfBoundsException extends RuntimeException {
     @java.io.Serial
     private static final long serialVersionUID = 234122996006267687L;
 

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

@@ -34,6 +34,8 @@
 import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
+import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;
 import org.checkerframework.checker.signedness.qual.UnknownSignedness;
 import org.checkerframework.checker.tainting.qual.Untainted;
 import org.checkerframework.common.aliasing.qual.Unique;
@@ -55,13 +57,15 @@
  */
 @AnnotatedFor({"aliasing", "guieffect", "index", "lock", "nullness"})
 @PolyUIType
+@ReceiverDependentMutable
 public class Object {
 
     /**
      * Constructs a new object.
      */
     @Pure
     @IntrinsicCandidate
+    @ReceiverDependentMutable
     public @Unique @Untainted Object() {}
 
     /**
@@ -87,7 +91,7 @@ public class Object {
     @SafeEffect
     @Pure
     @IntrinsicCandidate
-    public final native Class<? extends @MustCall() Object> getClass(@PolyUI @GuardSatisfied @UnknownInitialization @UnknownSignedness Object this);
+    public final native Class<? extends @MustCall() Object> getClass(@Readonly @PolyUI @GuardSatisfied @UnknownInitialization @UnknownSignedness Object this);
 
     /**
      * Returns a hash code value for the object. This method is
@@ -124,7 +128,7 @@ public class Object {
      */
     @Pure
     @IntrinsicCandidate
-    public native int hashCode(@GuardSatisfied @UnknownSignedness Object this);
+    public native int hashCode(@Readonly @GuardSatisfied @UnknownSignedness Object this);
 
     /**
      * Indicates whether some other object is "equal to" this one.
@@ -186,7 +190,7 @@ public class Object {
      */
     @Pure
     @EnsuresNonNullIf(expression="#1", result=true)
-    public boolean equals(@GuardSatisfied Object this, @GuardSatisfied @Nullable Object obj) {
+    public boolean equals(@Readonly @GuardSatisfied Object this, @Readonly @GuardSatisfied @Nullable Object obj) {
         return (this == obj);
     }
 
@@ -253,7 +257,7 @@ public boolean equals(@GuardSatisfied Object this, @GuardSatisfied @Nullable Obj
      */
     @SideEffectFree
     @IntrinsicCandidate
-    protected native Object clone(@GuardSatisfied Object this) throws CloneNotSupportedException;
+    protected native @ReceiverDependentMutable Object clone(@ReceiverDependentMutable @GuardSatisfied Object this) throws CloneNotSupportedException;
 
     /**
      * Returns a string representation of the object.
@@ -284,7 +288,7 @@ public boolean equals(@GuardSatisfied Object this, @GuardSatisfied @Nullable Obj
     "that differs according to ==, and @Deterministic requires that the results of",
     "two calls of the method are ==."})
     @SideEffectFree
-    public String toString(@GuardSatisfied Object this) {
+    public String toString(@Readonly @GuardSatisfied Object this) {
         return getClass().getName() + "@" + Integer.toHexString(hashCode());
     }