Starting move PICO to EISOP

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/Bottom.java

@@ -0,0 +1,29 @@
+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 @Bottom} can only be annotated before a type parameter (For example, {@code class
+ * C<@Bottom T extends MutableBox>{}}). This means {@code @Bottom} is the lower bound for this type
+ * parameter.
+ *
+ * <p>User can explicitly write {@code @Bottom} 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, Lost.class})
+@DefaultFor(typeKinds = {TypeKind.NULL})
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_PARAMETER})
+@TargetLocations({TypeUseLocation.LOWER_BOUND})
+public @interface Bottom {}

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/Lost.java

@@ -0,0 +1,12 @@
+package org.checkerframework.checker.pico.qual;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+import java.lang.annotation.*;
+
+/** 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 Lost {}

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

@@ -0,0 +1,26 @@
+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})
+// @DefaultFor({ TypeUseLocation.EXCEPTION_PARAMETER })
+@HoldsForDefaultValue
+public @interface Mutable {}

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

@@ -0,0 +1,12 @@
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+public @interface ObjectIdentityMethod {}

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,26 @@
+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})
+// @DefaultFor({ TypeUseLocation.FIELD })
+@HoldsForDefaultValue
+public @interface ReceiverDependentMutable {}

checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java

@@ -0,0 +1,110 @@
+package org.checkerframework.checker.pico;
+
+import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE;
+import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY;
+
+import com.sun.source.tree.IdentifierTree;
+import com.sun.source.tree.MemberSelectTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.util.TreePath;
+import com.sun.source.util.TreePathScanner;
+
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.util.AnnotatedTypes;
+import org.checkerframework.javacutil.ElementUtils;
+import org.checkerframework.javacutil.TreeUtils;
+
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+
+public class ObjectIdentityMethodEnforcer extends TreePathScanner<Void, Void> {
+
+    private PICONoInitAnnotatedTypeFactory typeFactory;
+    private BaseTypeChecker checker;
+
+    private ObjectIdentityMethodEnforcer(
+            PICONoInitAnnotatedTypeFactory typeFactory, BaseTypeChecker checker) {
+        this.typeFactory = typeFactory;
+        this.checker = checker;
+    }
+
+    // Main entry
+    public static void check(
+            TreePath statement,
+            PICONoInitAnnotatedTypeFactory typeFactory,
+            BaseTypeChecker checker) {
+        if (statement == null) return;
+        ObjectIdentityMethodEnforcer asfchecker =
+                new ObjectIdentityMethodEnforcer(typeFactory, checker);
+        asfchecker.scan(statement, null);
+    }
+
+    @Override
+    public Void visitMethodInvocation(MethodInvocationTree node, Void aVoid) {
+        Element elt = TreeUtils.elementFromUse(node);
+        checkMethod(node, elt);
+        return super.visitMethodInvocation(node, aVoid);
+    }
+
+    private void checkMethod(MethodInvocationTree node, Element elt) {
+        assert elt instanceof ExecutableElement;
+        if (ElementUtils.isStatic(elt)) {
+            return; // Doesn't check static method invocation because it doesn't access instance
+            // field
+        }
+        if (!PICOTypeUtil.isObjectIdentityMethod((ExecutableElement) elt, typeFactory)) {
+            // Report warning since invoked method is not only dependent on abstract state fields,
+            // but we
+            // don't know whether this method invocation's result flows into the hashcode or not.
+            checker.reportWarning(node, "object.identity.method.invocation.invalid", elt);
+        }
+    }
+
+    @Override
+    public Void visitIdentifier(IdentifierTree node, Void aVoid) {
+        Element elt = TreeUtils.elementFromUse(node);
+        checkField(node, elt);
+        return super.visitIdentifier(node, aVoid);
+    }
+
+    @Override
+    public Void visitMemberSelect(MemberSelectTree node, Void aVoid) {
+        Element elt = TreeUtils.elementFromUse(node);
+        checkField(node, elt);
+        return super.visitMemberSelect(node, aVoid);
+    }
+
+    private void checkField(Tree node, Element elt) {
+        if (elt == null) return;
+        if (elt.getSimpleName().contentEquals("this")
+                || elt.getSimpleName().contentEquals("super")) {
+            return;
+        }
+        if (elt.getKind() == ElementKind.FIELD) {
+            if (ElementUtils.isStatic(elt)) {
+                checker.reportWarning(node, "object.identity.static.field.access.forbidden", elt);
+            } else {
+                if (!isInAbstractState(elt, typeFactory)) {
+                    // Report warning since accessed field is not within abstract state
+                    checker.reportWarning(node, "object.identity.field.access.invalid", elt);
+                }
+            }
+        }
+    }
+
+    // Deeply test if a field is in abstract state or not. For composite types: array component,
+    // type arguments, upper bound of type parameter uses are also checked.
+    private boolean isInAbstractState(Element elt, PICONoInitAnnotatedTypeFactory typeFactory) {
+        boolean in = true;
+        if (PICOTypeUtil.isAssignableField(elt, typeFactory)) {
+            in = false;
+        } else if (AnnotatedTypes.containsModifier(typeFactory.getAnnotatedType(elt), MUTABLE)) {
+            in = false;
+        } else if (AnnotatedTypes.containsModifier(typeFactory.getAnnotatedType(elt), READONLY)) {
+            in = false;
+        }
+        return in;
+    }
+}