Move PICO to EISOP

build.gradle

@@ -354,13 +354,14 @@ allprojects { currentProj ->
                 }
                 targetExclude doNotFormat
 
+
                 if (eisopFormatting) {
                     googleJavaFormat(versions.googleJavaFormat).aosp()
                     importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax')
                 } else {
                     googleJavaFormat(versions.googleJavaFormat) // the formatter to apply to Java files
                 }
-                formatAnnotations().addTypeAnnotation("PolyInitialized").addTypeAnnotation("PolyVP").addTypeAnnotation("ReceiverDependentQual")
+                formatAnnotations().addTypeAnnotation("PolyInitialized").addTypeAnnotation("PolyVP").addTypeAnnotation("ReceiverDependentQual").addTypeAnnotation("Immutable").addTypeAnnotation("Readonly").addTypeAnnotation("Mutable").addTypeAnnotation("ReceiverDependentMutable").addTypeAnnotation("PolyMutable")
             }
 
             // Only define a groovyGradle task on the root project, for simplicity in setting the target pattern

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Assignable.java

@@ -0,0 +1,19 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * This annotation is used to exclude the field from the abstract state and means the field can be
+ * reassigned after initialization. It should only annotate on field, not class or method.
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.FIELD})
+@HoldsForDefaultValue
+public @interface Assignable {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Immutable.java

@@ -0,0 +1,83 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
+import org.checkerframework.framework.qual.LiteralKind;
+import org.checkerframework.framework.qual.QualifierForLiterals;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeKind;
+import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UpperBoundFor;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import java.math.BigDecimal;
+import java.math.BigInteger;
+
+/**
+ * {@code @Immutable} is a type qualifier that indicates that the fields of annotated reference
+ * cannot be mutated.
+ *
+ * <p>For usage in PICO, there are three ways to use this annotation: Object creation: the object
+ * created will always be immutable; Annotation on a reference: the object that reference points to
+ * is immutable; Annotation on a class: all instances of that class are immutable.
+ */
+@SubtypeOf({Readonly.class})
+@Documented
+@DefaultQualifierInHierarchy
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@DefaultFor(
+        value = {TypeUseLocation.EXCEPTION_PARAMETER},
+        types = {
+            Enum.class,
+            String.class,
+            Double.class,
+            Boolean.class,
+            Byte.class,
+            Character.class,
+            Float.class,
+            Integer.class,
+            Long.class,
+            Short.class,
+            Number.class,
+            BigDecimal.class,
+            BigInteger.class
+        },
+        typeKinds = {
+            TypeKind.INT,
+            TypeKind.BYTE,
+            TypeKind.SHORT,
+            TypeKind.BOOLEAN,
+            TypeKind.LONG,
+            TypeKind.CHAR,
+            TypeKind.FLOAT,
+            TypeKind.DOUBLE
+        })
+@QualifierForLiterals({LiteralKind.PRIMITIVE, LiteralKind.STRING})
+@UpperBoundFor(
+        typeKinds = {
+            TypeKind.INT, TypeKind.BYTE, TypeKind.SHORT, TypeKind.BOOLEAN,
+            TypeKind.LONG, TypeKind.CHAR, TypeKind.FLOAT, TypeKind.DOUBLE
+        },
+        types = {
+            Enum.class,
+            String.class,
+            Double.class,
+            Boolean.class,
+            Byte.class,
+            Character.class,
+            Float.class,
+            Integer.class,
+            Long.class,
+            Short.class,
+            Number.class,
+            BigDecimal.class,
+            BigInteger.class
+        })
+@HoldsForDefaultValue
+public @interface Immutable {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Mutable.java

@@ -0,0 +1,25 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * {@code @Mutable} is a type qualifier that indicates that the fields of annotated reference can be
+ * mutated through this reference. This is default behavior for all references in Java.
+ *
+ * <p>For usage in PICO, there are three ways to use this annotation: Object creation: the object
+ * created will always be mutable; Annotation on a reference: the object that reference points to is
+ * mutable; Annotation on a class: all instances of that class are mutable.
+ */
+@SubtypeOf({Readonly.class})
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@HoldsForDefaultValue
+public @interface Mutable {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ObjectIdentityMethod.java

@@ -0,0 +1,19 @@
+package org.checkerframework.checker.pico.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated method is an object identity method. An object identity method is a
+ * method that returns the identity of the object it is called on.
+ *
+ * <p>For example, the {@code hashCode} method is an object identity method, because it returns the
+ * identity of the object it is called on.
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+public @interface ObjectIdentityMethod {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOBottom.java

@@ -0,0 +1,30 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TargetLocations;
+import org.checkerframework.framework.qual.TypeKind;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * {@code @PICOBottom} can only be annotated before a type parameter (For example, {@code class
+ * C<@Bottom T extends MutableBox>{}}). This means {@code @PICOBottom} is the lower bound for this
+ * type parameter.
+ *
+ * <p>User can explicitly write {@code @PICOBottom} but it's not necessary because it's
+ * automatically inferred, and we have -AwarnRedundantAnnotations flag to warn about redundant
+ * annotations.
+ */
+@SubtypeOf({Mutable.class, Immutable.class, ReceiverDependentMutable.class, PICOLost.class})
+@DefaultFor(typeKinds = {TypeKind.NULL})
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_PARAMETER})
+@TargetLocations({TypeUseLocation.LOWER_BOUND})
+public @interface PICOBottom {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOLost.java

@@ -0,0 +1,16 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/** Lost means the mutability type of this reference is unknown. This is a subtype of Readonly. */
+@SubtypeOf({Readonly.class})
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+public @interface PICOLost {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PolyMutable.java

@@ -0,0 +1,30 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.framework.qual.PolymorphicQualifier;
+import org.checkerframework.framework.qual.TargetLocations;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * The polymorphic qualifier {@code @PolyMutable} indicates that the mutability type of this
+ * reference can be substituted to {@code @Mutable} or {@code @Immutable} or {@code @RDM}. This is a
+ * polymorphic qualifier that can be used in the type hierarchy.
+ *
+ * <p>{@code @PolyMutable} applies to method parameters, method return type and receiver.
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@PolymorphicQualifier(Readonly.class)
+@TargetLocations({
+    TypeUseLocation.PARAMETER,
+    TypeUseLocation.RECEIVER,
+    TypeUseLocation.RETURN,
+    TypeUseLocation.LOCAL_VARIABLE
+})
+public @interface PolyMutable {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Readonly.java

@@ -0,0 +1,23 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * The top qualifier in the mutability type hierarchy that indicates that the fields of annotated
+ * reference cannot be mutated through this reference but can be mutated through other Aliasing.
+ * This is the default qualifier for local variables and subject to flow-sensitive type refinement.
+ */
+@SubtypeOf({})
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@DefaultFor({TypeUseLocation.LOCAL_VARIABLE, TypeUseLocation.IMPLICIT_UPPER_BOUND})
+public @interface Readonly {}

checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ReceiverDependentMutable.java

@@ -0,0 +1,25 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * {@code @ReceiverDependentMutable} is a type qualifier that indicates that mutability type depends
+ * on the receiver type.
+ *
+ * <p>For usage in PICO, there are three ways to use this annotation: Object creation: the object
+ * created depends on the lhs type; Annotation on a reference: the object that reference depends on
+ * the receiver type; Annotation on a class: the instances can be mutable or immutable.
+ */
+@SubtypeOf(Readonly.class)
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@HoldsForDefaultValue
+public @interface ReceiverDependentMutable {}