Add PICO annotation

.gitignore

@@ -16,3 +16,5 @@ NashornProfile.txt
 **/JTreport/**
 **/JTwork/**
 /src/utils/LogCompilation/target/
+
+*.class

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,7 @@
 "EnsuresNonNullIf(expression={\"list()\",\"list(FilenameFilter)\",\"listFiles()\",\"listFiles(FilenameFilter)\",\"listFiles(FileFilter)\"}, result=true)\""
 })
 @AnnotatedFor({"index", "initialization", "interning", "lock", "nullness"})
-public class File
+@ReceiverDependentMutable public 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,7 +72,7 @@
  * @since   1.0
  */
 @AnnotatedFor({"index", "initialization", "mustcall", "nullness"})
-public class FileInputStream extends InputStream
+public @ReceiverDependentMutable class FileInputStream extends InputStream
 {
     private static final int DEFAULT_BUFFER_SIZE = 8192;
 
@@ -147,7 +149,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/IOException.java

@@ -26,6 +26,7 @@
 package java.io;
 
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 /**
@@ -80,7 +81,7 @@ public IOException(@Nullable String message) {
      *
      * @since 1.6
      */
-    public IOException(@Nullable String message, @Nullable Throwable cause) {
+    public IOException(@Nullable String message, @Nullable @Readonly Throwable cause) {
         super(message, cause);
     }
 
@@ -98,7 +99,7 @@ public IOException(@Nullable String message, @Nullable Throwable cause) {
      *
      * @since 1.6
      */
-    public IOException(@Nullable Throwable cause) {
+    public IOException(@Nullable @Readonly Throwable cause) {
         super(cause);
     }
 }

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,5 @@
  *      <cite>Java Object Serialization Specification</cite></a>
  * @since   1.1
  */
-public interface Serializable {
+public @ReceiverDependentMutable 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;

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

@@ -26,6 +26,7 @@
 package java.lang;
 
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
@@ -79,7 +80,7 @@ private AssertionError(@Nullable String detailMessage) {
      * @see   Throwable#getCause()
      */
     @SideEffectFree
-    public AssertionError(@Nullable Object detailMessage) {
+    public AssertionError(@Nullable @Readonly Object detailMessage) {
         this(String.valueOf(detailMessage));
         if (detailMessage instanceof Throwable)
             initCause((Throwable) detailMessage);

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

@@ -32,9 +32,12 @@
 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.framework.qual.AnnotatedFor;
+import org.checkerframework.framework.qual.DefaultQualifierForUse;
 
 import java.util.NoSuchElementException;
 import java.util.Objects;
@@ -68,7 +71,7 @@
  */
 
 @AnnotatedFor({"lock", "nullness", "index"})
-public interface CharSequence {
+@ReceiverDependentMutable public interface CharSequence {
 
     /**
      * Returns the length of this character sequence.  The length is the number

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

@@ -32,6 +32,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
 import org.checkerframework.checker.nullness.qual.UnknownKeyFor;
+import org.checkerframework.checker.pico.qual.Readonly;
 import org.checkerframework.checker.signature.qual.CanonicalName;
 import org.checkerframework.checker.signature.qual.ClassGetName;
 import org.checkerframework.checker.signature.qual.ClassGetSimpleName;
@@ -223,7 +224,7 @@
             "meaning, but are unrelated by the Java type hierarchy.",
             "@Covariant makes Class<@NonNull String> a subtype of Class<@Nullable String>."})
 @AnnotatedFor({"index", "interning", "lock", "nullness", "signature"})
-@Covariant({0})
+@Covariant(0)
 public final @Interned class Class<@UnknownKeyFor T> implements java.io.Serializable,
                               GenericDeclaration,
                               Type,
@@ -719,7 +720,7 @@ public Void run() {
     @Pure
     @EnsuresNonNullIf(expression={"#1"}, result=true)
     @IntrinsicCandidate
-    public native boolean isInstance(@GuardSatisfied Class<T> this, @Nullable Object obj);
+    public native boolean isInstance(@GuardSatisfied Class<T> this, @Nullable @Readonly Object obj);
 
 
     /**

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> {
+@ReceiverDependentMutable public interface Comparable<T extends @NonNull @Readonly 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;