diff --git a/build.gradle b/build.gradle index 73a9d578bd3..b81bb567907 100644 --- a/build.gradle +++ b/build.gradle @@ -307,7 +307,7 @@ allprojects { googleJavaFormat().aosp() importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax') - formatAnnotations().addTypeAnnotation("PolyInitialized").addTypeAnnotation("PolyVP").addTypeAnnotation("ReceiverDependentQual") + formatAnnotations().addTypeAnnotation("PolyInitialized").addTypeAnnotation("PolyVP").addTypeAnnotation("ReceiverDependentQual").addTypeAnnotation("Immutable").addTypeAnnotation("Readonly").addTypeAnnotation("Mutable").addTypeAnnotation("ReceiverDependentMutable").addTypeAnnotation("PolyMutable") } groovyGradle { diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Assignable.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Assignable.java new file mode 100644 index 00000000000..ca019c41254 --- /dev/null +++ b/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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Immutable.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Immutable.java new file mode 100644 index 00000000000..0f1f3b3a636 --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Mutable.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Mutable.java new file mode 100644 index 00000000000..51f41e3a177 --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ObjectIdentityMethod.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ObjectIdentityMethod.java new file mode 100644 index 00000000000..1cf80c3f7c2 --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOBottom.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOBottom.java new file mode 100644 index 00000000000..03626c92ddc --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOLost.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PICOLost.java new file mode 100644 index 00000000000..6ba23f5219f --- /dev/null +++ b/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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PolyMutable.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/PolyMutable.java new file mode 100644 index 00000000000..ebec38e9501 --- /dev/null +++ b/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. + * + *

{@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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Readonly.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Readonly.java new file mode 100644 index 00000000000..dfefb915387 --- /dev/null +++ b/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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ReceiverDependentMutable.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ReceiverDependentMutable.java new file mode 100644 index 00000000000..60e5fce9cbe --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java b/checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java new file mode 100644 index 00000000000..2fe633864a9 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java @@ -0,0 +1,146 @@ +package org.checkerframework.checker.pico; + +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; + +/** + * This class checks whether a method invocation or field access is valid for object identity + * method. A method invocation is valid if it only depends on abstract state fields. A field access + * is valid if the accessed field is within abstract state. + */ +public class ObjectIdentityMethodEnforcer extends TreePathScanner { + /** The type factory */ + private PICONoInitAnnotatedTypeFactory atypeFactory; + + /** The checker */ + private BaseTypeChecker checker; + + /** + * Create a new ObjectIdentityMethodEnforcer. + * + * @param typeFactory the type factory + * @param checker the checker + */ + private ObjectIdentityMethodEnforcer( + PICONoInitAnnotatedTypeFactory typeFactory, BaseTypeChecker checker) { + this.atypeFactory = typeFactory; + this.checker = checker; + } + + /** + * Check whether a method invocation or field access is valid for object identity method. + * + * @param statement the statement to check + * @param typeFactory the type factory + * @param checker the checker + */ + 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); + } + + /** + * Check whether a method invocation is valid for object identity method. + * + * @param node the method invocation tree + * @param elt the element of the method invocation + */ + private void checkMethod(MethodInvocationTree node, Element elt) { + assert elt instanceof ExecutableElement; + // Doesn't check static method invocation because it doesn't access instance field. + if (ElementUtils.isStatic(elt)) { + return; + } + if (!PICOTypeUtil.isObjectIdentityMethod((ExecutableElement) elt, atypeFactory)) { + // 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); + } + + /** + * Check whether a field access is valid for object identity method. + * + * @param node the field access tree + * @param elt the element of the field access + */ + 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, atypeFactory)) { + // 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. + * + * @param elt the element of the field + * @param typeFactory the type factory + * @return true if the field is in abstract state, false otherwise + */ + private boolean isInAbstractState(Element elt, PICONoInitAnnotatedTypeFactory typeFactory) { + boolean in = true; + if (PICOTypeUtil.isAssignableField(elt, typeFactory)) { + in = false; + } else if (AnnotatedTypes.containsModifier( + typeFactory.getAnnotatedType(elt), atypeFactory.MUTABLE)) { + in = false; + } else if (AnnotatedTypes.containsModifier( + typeFactory.getAnnotatedType(elt), atypeFactory.READONLY)) { + in = false; + } + return in; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOChecker.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOChecker.java new file mode 100644 index 00000000000..818be9ee87e --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOChecker.java @@ -0,0 +1,30 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.initialization.InitializationChecker; +import org.checkerframework.checker.initialization.InitializationVisitor; +import org.checkerframework.common.basetype.BaseTypeChecker; + +import javax.annotation.processing.SupportedOptions; + +/** The PICO checker. */ +@SupportedOptions({"abstractStateOnly", "immutableDefault"}) +public class PICOChecker extends InitializationChecker { + + /** Default constructor for PICOChecker. */ + public PICOChecker() {} + + @Override + public Class getTargetCheckerClass() { + return PICONoInitSubchecker.class; + } + + @Override + public boolean checkPrimitives() { + return true; + } + + @Override + protected InitializationVisitor createSourceVisitor() { + return new PICOInitializationVisitor(this); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationAnnotatedTypeFactory.java new file mode 100644 index 00000000000..e53f8ccafb8 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationAnnotatedTypeFactory.java @@ -0,0 +1,99 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; + +import org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory; +import org.checkerframework.checker.initialization.InitializationChecker; +import org.checkerframework.checker.initialization.InitializationStore; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.flow.CFAbstractStore; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; + +import java.util.Collection; +import java.util.List; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.TypeElement; +import javax.lang.model.util.Elements; + +/** + * The InitializationAnnotatedTypeFactory for the PICO type system. This class is mainly created to + * override getUninitializedFields() method for PICO specific definite assignment check. + */ +public class PICOInitializationAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory { + /** The {@link Mutable} annotation. */ + private final AnnotationMirror MUTABLE; + + /** + * Constructor for PICOInitializationAnnotatedTypeFactory. + * + * @param checker the BaseTypeChecker this visitor works with + */ + public PICOInitializationAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + Elements elements = checker.getElementUtils(); + MUTABLE = AnnotationBuilder.fromClass(elements, Mutable.class); + postInit(); + } + + /** + * {@inheritDoc} + * + *

In @Immutable and @ReceiverDependentMutable class, all fields should be initialized in the + * constructor except for fields explicitly annotated with @Assignable and static fields. + */ + @Override + public List getUninitializedFields( + InitializationStore initStore, + CFAbstractStore targetStore, + TreePath path, + boolean isStatic, + Collection receiverAnnotations) { + List uninitializedFields = + super.getUninitializedFields(initStore, path, isStatic, receiverAnnotations); + + GenericAnnotatedTypeFactory factory = + checker.getTypeFactoryOfSubcheckerOrNull( + ((InitializationChecker) checker).getTargetCheckerClass()); + + if (factory == null) { + throw new BugInCF( + "Did not find target type factory for checker " + + ((InitializationChecker) checker).getTargetCheckerClass()); + } + + // Filter out fields annotated with @Assignable or static fields or fields in @Mutable class + uninitializedFields.removeIf( + var -> { + ClassTree enclosingClass = TreePathUtil.enclosingClass(getPath(var)); + TypeElement typeElement = TreeUtils.elementFromDeclaration(enclosingClass); + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, factory); + // If the class is not annotated with @Immutable or @ReceiverDependentMutable, + // return false + if (bound.hasAnnotation(MUTABLE)) { + return true; + } else { + Element varElement = TreeUtils.elementFromDeclaration(var); + // If the field is annotated with @Assignable, return false + if (PICOTypeUtil.isAssignableField(varElement, this) + || ElementUtils.isStatic(varElement)) { + return true; + } else { + return false; + } + } + }); + return uninitializedFields; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationVisitor.java new file mode 100644 index 00000000000..dfed22ce992 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationVisitor.java @@ -0,0 +1,25 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory; +import org.checkerframework.checker.initialization.InitializationVisitor; +import org.checkerframework.common.basetype.BaseTypeChecker; + +/** + * The InitializationVisitor for the PICO type system. This class is mainly created to override + * createTypeFactory() method for the purpose of using PICOInitializationAnnotatedTypeFactory. + */ +public class PICOInitializationVisitor extends InitializationVisitor { + /** + * Constructor for PICOInitializationVisitor. + * + * @param checker the BaseTypeChecker this visitor works with + */ + public PICOInitializationVisitor(BaseTypeChecker checker) { + super(checker); + } + + @Override + protected InitializationAnnotatedTypeFactory createTypeFactory() { + return new PICOInitializationAnnotatedTypeFactory(checker); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnalysis.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnalysis.java new file mode 100644 index 00000000000..6610a9c483b --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnalysis.java @@ -0,0 +1,44 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.javacutil.AnnotationMirrorSet; + +import javax.lang.model.type.TypeMirror; + +/** + * The analysis class for the immutability type system (serves as factory for the transfer function, + * stores and abstract values. + */ +public class PICONoInitAnalysis + extends CFAbstractAnalysis { + /** + * Create PICONoInitAnalysis. + * + * @param checker the BaseTypeChecker this analysis works with + * @param factory the PICONoInitAnnotatedTypeFactory this analysis works with + */ + public PICONoInitAnalysis(BaseTypeChecker checker, PICONoInitAnnotatedTypeFactory factory) { + super(checker, factory, -1); + } + + @Override + public PICONoInitStore createEmptyStore(boolean sequentialSemantics) { + return new PICONoInitStore(this, sequentialSemantics); + } + + @Override + public PICONoInitStore createCopiedStore(PICONoInitStore picoNoInitStore) { + return new PICONoInitStore(picoNoInitStore); + } + + @Override + public PICONoInitValue createAbstractValue( + AnnotationMirrorSet annotations, TypeMirror underlyingType) { + if (!CFAbstractValue.validateSet(annotations, underlyingType, atypeFactory)) { + return null; + } + return new PICONoInitValue(this, annotations, underlyingType); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnnotatedTypeFactory.java new file mode 100644 index 00000000000..fd09b4eb1cd --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnnotatedTypeFactory.java @@ -0,0 +1,747 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewArrayTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.ParameterizedTypeTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.TypeCastTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; + +import org.checkerframework.checker.initialization.InitializationFieldAccessTreeAnnotator; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PICOBottom; +import org.checkerframework.checker.pico.qual.PICOLost; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.framework.type.ViewpointAdapter; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.DefaultQualifierForUseTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.TypeAnnotator; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; + +import java.lang.annotation.Annotation; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Objects; +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.TypeElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.DeclaredType; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; + +/** + * AnnotatedTypeFactory for PICO. In addition to getting atms, it also propagates and applies + * mutability qualifiers correctly depending on AST locations(e.g. fields, binary trees) or + * methods(toString(), hashCode(), clone(), equals(Object o)) using TreeAnnotators and + * TypeAnnotators. It also applies implicits to method receiver that is not so by default in super + * implementation. + */ +public class PICONoInitAnnotatedTypeFactory + extends GenericAnnotatedTypeFactory< + PICONoInitValue, PICONoInitStore, PICONoInitTransfer, PICONoInitAnalysis> { + /** The @{@link Mutable} annotation. */ + protected final AnnotationMirror MUTABLE = AnnotationBuilder.fromClass(elements, Mutable.class); + + /** The @{@link Immutable} annotation. */ + protected final AnnotationMirror IMMUTABLE = + AnnotationBuilder.fromClass(elements, Immutable.class); + + /** The @{@link Readonly} annotation. */ + protected final AnnotationMirror READONLY = + AnnotationBuilder.fromClass(elements, Readonly.class); + + /** The @{@link ReceiverDependentMutable} annotation. */ + protected final AnnotationMirror RECEIVER_DEPENDENT_MUTABLE = + AnnotationBuilder.fromClass(elements, ReceiverDependentMutable.class); + + /** The @{@link PolyMutable} annotation. */ + protected final AnnotationMirror POLY_MUTABLE = + AnnotationBuilder.fromClass(elements, PolyMutable.class); + + /** The @{@link PICOLost} annotation. */ + protected final AnnotationMirror LOST = AnnotationBuilder.fromClass(elements, PICOLost.class); + + /** The @{@link PICOBottom} annotation. */ + protected final AnnotationMirror BOTTOM = + AnnotationBuilder.fromClass(elements, PICOBottom.class); + + /** + * Create a new PICONoInitAnnotatedTypeFactory. + * + * @param checker the BaseTypeChecker + */ + public PICONoInitAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + addAliasedTypeAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + postInit(); + } + + @Override + protected Set> createSupportedTypeQualifiers() { + return new LinkedHashSet<>( + Arrays.asList( + Readonly.class, + Mutable.class, + PolyMutable.class, + ReceiverDependentMutable.class, + Immutable.class, + PICOLost.class, + PICOBottom.class)); + } + + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new PICOViewpointAdapter(this); + } + + /** Annotators are executed by the added order. Same for Type Annotator */ + @Override + protected TreeAnnotator createTreeAnnotator() { + List annotators = new ArrayList<>(5); + annotators.add(new InitializationFieldAccessTreeAnnotator(this)); + annotators.add(new PICOPropagationTreeAnnotator(this)); + annotators.add(new LiteralTreeAnnotator(this)); + annotators.add(new PICOSuperClauseAnnotator(this)); + annotators.add(new PICOTreeAnnotator(this)); + return new ListTreeAnnotator(annotators); + } + + @Override + protected TypeAnnotator createTypeAnnotator() { + // Adding order is important here. Because internally type annotators are using + // addMissingAnnotations() method, so if one annotator already applied the annotations, the + // others won't apply twice at the same location + return new ListTypeAnnotator( + super.createTypeAnnotator(), + new PICOTypeAnnotator(this), + new PICODefaultForTypeAnnotator(this), + new PICOEnumDefaultAnnotator(this)); + } + + @Override + public QualifierHierarchy createQualifierHierarchy() { + return new PICOQualifierHierarchy(getSupportedTypeQualifiers(), elements, this); + } + + @Override + public ParameterizedExecutableType constructorFromUse(NewClassTree tree) { + boolean hasExplicitAnnos = getExplicitNewClassAnnos(tree).isEmpty(); + ParameterizedExecutableType mType = super.constructorFromUse(tree); + AnnotatedExecutableType method = mType.executableType; + if (hasExplicitAnnos && method.getReturnType().hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + method.getReturnType().replaceAnnotation(MUTABLE); + } + return mType; + } + + /** + * {@inheritDoc} Forbid applying top annotations to type variables if they are used on local + * variables. + */ + @Override + public boolean getShouldDefaultTypeVarLocals() { + return false; + } + + /** + * {@inheritDoc} This covers the case when static fields are used and constructor is accessed as + * an element(regarding applying @Immutable on type declaration to constructor return type). + */ + @Override + public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { + addDefaultForField(this, type, elt); + defaultConstructorReturnToClassBound(this, elt, type); + super.addComputedTypeAnnotations(elt, type); + } + + /** + * Get the PICO viewpoint adapter. + * + * @return PICOViewpointAdapter + */ + public PICOViewpointAdapter getViewpointAdapter() { + return (PICOViewpointAdapter) viewpointAdapter; + } + + /** + * {@inheritDoc} Changes the framework default to @Mutable + * + * @return Mutable default AnnotationMirrorSet + */ + @Override + protected AnnotationMirrorSet getDefaultTypeDeclarationBounds() { + AnnotationMirrorSet frameworkDefault = + new AnnotationMirrorSet(super.getDefaultTypeDeclarationBounds()); + // if (checker.hasOption("immutableDefault")) { + // return replaceAnnotationInHierarchy(frameworkDefault, IMMUTABLE); + // } + return replaceAnnotationInHierarchy(frameworkDefault, IMMUTABLE); + } + + @Override + public AnnotationMirrorSet getTypeDeclarationBounds(TypeMirror type) { + AnnotationMirror mut = getTypeDeclarationBoundForMutability(type); + AnnotationMirrorSet frameworkDefault = super.getTypeDeclarationBounds(type); + if (mut != null) { + frameworkDefault = replaceAnnotationInHierarchy(frameworkDefault, mut); + } + return frameworkDefault; + } + + /** + * Replace the annotation in the hierarchy with the given AnnotationMirrorSet. + * + * @param set The AnnotationMirrorSet to replace the annotation in + * @param mirror The AnnotationMirror to replace with + * @return The replaced AnnotationMirrorSet + */ + private AnnotationMirrorSet replaceAnnotationInHierarchy( + AnnotationMirrorSet set, AnnotationMirror mirror) { + AnnotationMirrorSet result = new AnnotationMirrorSet(set); + AnnotationMirror removeThis = + getQualifierHierarchy().findAnnotationInSameHierarchy(set, mirror); + result.remove(removeThis); + result.add(mirror); + return result; + } + + /** + * Get the upperbound give a TypeMirror 1. If the type is implicitly immutable, + * return @Immutable 2. If the type is an enum, return @Immutable if it has no explicit + * annotation 3. If the type is an array, return @ReceiverDependentMutable 4. Otherwise, return + * null + * + * @param type the type to get the upperbound for + * @return the upperbound for the given type + */ + public AnnotationMirror getTypeDeclarationBoundForMutability(TypeMirror type) { + if (PICOTypeUtil.isImplicitlyImmutableType(toAnnotatedType(type, false))) { + return IMMUTABLE; + } + if (type.getKind() == TypeKind.ARRAY) { + return RECEIVER_DEPENDENT_MUTABLE; // if decided to use vpa for array, return RDM. + } + // IMMUTABLE for enum w/o decl anno + if (type instanceof DeclaredType) { + Element ele = ((DeclaredType) type).asElement(); + if (ele.getKind() == ElementKind.ENUM) { + // TODO refine the logic here for enum + if (!AnnotationUtils.containsSameByName(getDeclAnnotations(ele), MUTABLE) + && !AnnotationUtils.containsSameByName( + getDeclAnnotations(ele), + RECEIVER_DEPENDENT_MUTABLE)) { // no decl anno + return IMMUTABLE; + } + } + } + return null; + } + + @Override + public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) { + // this is still needed with PICOSuperClauseAnnotator. + // maybe just use getAnnotatedType add default anno from class main qual, if no qual present + AnnotatedTypeMirror fromTypeTree = super.getTypeOfExtendsImplements(clause); + if (fromTypeTree.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + ClassTree enclosingClass = TreePathUtil.enclosingClass(getPath(clause)); + // TODO This is a hack but fixed a few crash errors, look what will be the overall + // solution. + if (enclosingClass == null) { + return fromTypeTree; + } else { + AnnotatedTypeMirror enclosing = getAnnotatedType(enclosingClass); + AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY); + fromTypeTree.replaceAnnotation(mainBound); + } + } + return fromTypeTree; + } + + /** + * Add default annotation to the given AnnotatedTypeMirror for the given Element. + * + * @param annotatedTypeFactory the annotated type factory + * @param annotatedTypeMirror the annotated type mirror to add default annotation + * @param element the element to add default annotation + */ + private void addDefaultForField( + AnnotatedTypeFactory annotatedTypeFactory, + AnnotatedTypeMirror annotatedTypeMirror, + Element element) { + if (element != null && element.getKind() == ElementKind.FIELD) { + // If the field is static, apply @Mutable if there is no explicit annotation and the + // field type is @RDM + if (ElementUtils.isStatic(element)) { + // AnnotatedTypeMirror implicitATM = + // annotatedTypeFactory.getAnnotatedType(element); + AnnotatedTypeMirror explicitATM = annotatedTypeFactory.fromElement(element); + AnnotationMirrorSet declBound = + annotatedTypeFactory.getTypeDeclarationBounds(element.asType()); + if (!explicitATM.hasAnnotationInHierarchy(READONLY) + && AnnotationUtils.containsSameByName( + declBound, RECEIVER_DEPENDENT_MUTABLE)) { + if (!PICOTypeUtil.isImplicitlyImmutableType(explicitATM)) { + annotatedTypeMirror.replaceAnnotation(IMMUTABLE); + } else { + annotatedTypeMirror.replaceAnnotation(MUTABLE); + } + } + } else { + // Apply default annotation to instance fields if there is no explicit annotation + AnnotatedTypeMirror explicitATM = annotatedTypeFactory.fromElement(element); + if (!explicitATM.hasAnnotationInHierarchy(READONLY)) { + if (explicitATM instanceof AnnotatedTypeMirror.AnnotatedDeclaredType) { + AnnotatedTypeMirror.AnnotatedDeclaredType adt = + (AnnotatedTypeMirror.AnnotatedDeclaredType) explicitATM; + Element typeElement = adt.getUnderlyingType().asElement(); + + AnnotationMirrorSet enclosingBound = + annotatedTypeFactory.getTypeDeclarationBounds( + Objects.requireNonNull( + ElementUtils.enclosingTypeElement(element)) + .asType()); + AnnotationMirrorSet declBound = + annotatedTypeFactory.getTypeDeclarationBounds(element.asType()); + // Add RDM if Type declaration bound=M and enclosing class Bound=M/RDM + // If the declaration bound is mutable and the enclosing class is also + // mutable, replace the annotation as RDM. + if (AnnotationUtils.containsSameByName(declBound, MUTABLE) + && AnnotationUtils.containsSameByName(enclosingBound, MUTABLE)) { + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDENT_MUTABLE); + } + // If the declaration bound is RDM, replace the annotation as RDM + if (typeElement instanceof TypeElement) { + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfTypeDeclaration( + typeElement, annotatedTypeFactory); + if (bound.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDENT_MUTABLE); + } + } + } else if (explicitATM instanceof AnnotatedTypeMirror.AnnotatedArrayType) { + // If the ATM is array type, apply RMD to array's component type. + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDENT_MUTABLE); + } + } + } + } + } + + /** + * Add default annotation from type declaration to constructor return type if elt is constructor + * and doesn't have explicit annotation(type is actually AnnotatedExecutableType of executable + * element - elt constructor). + * + * @param annotatedTypeFactory the annotated type factory + * @param elt the element to add default annotation + * @param type the type to add default annotation + */ + private void defaultConstructorReturnToClassBound( + AnnotatedTypeFactory annotatedTypeFactory, Element elt, AnnotatedTypeMirror type) { + if (elt.getKind() == ElementKind.CONSTRUCTOR && type instanceof AnnotatedExecutableType) { + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(elt, annotatedTypeFactory); + ((AnnotatedExecutableType) type) + .getReturnType() + .addMissingAnnotations(Arrays.asList(bound.getAnnotationInHierarchy(READONLY))); + } + } + + /** Tree Annotators */ + public static class PICOPropagationTreeAnnotator extends PropagationTreeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOPropagationTreeAnnotator. + * + * @param atypeFactory the type factory + */ + public PICOPropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) atypeFactory; + } + + // + // TODO This is very ugly. Why is array component type from lhs propagates to + // rhs?! + @Override + public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { + AnnotatedTypeMirror componentType = + ((AnnotatedTypeMirror.AnnotatedArrayType) type).getComponentType(); + boolean noExplicitATM = + !componentType.hasAnnotation(picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE); + super.visitNewArray(tree, type); + // if new explicit anno before, but RDM after, the RDM must come from the type + // declaration bound + // however, for type has declaration bound as RDM, its default use is mutable. + if (noExplicitATM + && componentType.hasAnnotation(picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE)) { + // if (checker.hasOption("immutableDefault")) { + // componentType.replaceAnnotation(IMMUTABLE); + // } else + componentType.replaceAnnotation(picoTypeFactory.IMMUTABLE); + } + return null; + } + + @Override + public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { + boolean hasExplicitAnnos = !type.getAnnotations().isEmpty(); + super.visitTypeCast(node, type); + if (!hasExplicitAnnos + && type.hasAnnotation(picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE)) { + // if (checker.hasOption("immutableDefault")) { + // type.replaceAnnotation(IMMUTABLE); + // } else + type.replaceAnnotation(picoTypeFactory.IMMUTABLE); + } + return null; + } + + @Override + public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { + return null; + } + } + + /** Apply defaults for static fields with non-implicitly immutable types. */ + public static class PICOTreeAnnotator extends TreeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOTreeAnnotator. + * + * @param atypeFactory the type factory + */ + public PICOTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) atypeFactory; + } + + /** + * {@inheritDoc} This adds @Immutable annotation to constructor return type if type + * declaration has @Immutable when the constructor is accessed as a tree. + */ + @Override + public Void visitMethod(MethodTree tree, AnnotatedTypeMirror p) { + Element element = TreeUtils.elementFromDeclaration(tree); + picoTypeFactory.defaultConstructorReturnToClassBound(atypeFactory, element, p); + return super.visitMethod(tree, p); + } + + /** {@inheritDoc} This covers the declaration of static fields */ + @Override + public Void visitVariable(VariableTree tree, AnnotatedTypeMirror annotatedTypeMirror) { + VariableElement element = TreeUtils.elementFromDeclaration(tree); + picoTypeFactory.addDefaultForField(atypeFactory, annotatedTypeMirror, element); + return super.visitVariable(tree, annotatedTypeMirror); + } + + @Override + public Void visitBinary(BinaryTree tree, AnnotatedTypeMirror type) { + type.replaceAnnotation(picoTypeFactory.IMMUTABLE); + return null; + } + } + + /** Type Annotators */ + public static class PICOTypeAnnotator extends TypeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOTypeAnnotator. + * + * @param typeFactory the type factory + */ + public PICOTypeAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) typeFactory; + } + + /** + * {@inheritDoc} Applies pre-knowledged defaults that are same with jdk.astub to toString, + * hashCode, equals, clone Object methods. + */ + @Override + public Void visitExecutable(AnnotatedExecutableType t, Void p) { + super.visitExecutable(t, p); + + // Only handle instance methods, not static methods + if (!ElementUtils.isStatic(t.getElement())) { + if (PICOTypeUtil.isMethodOrOverridingMethod(t, "toString()", atypeFactory) + || PICOTypeUtil.isMethodOrOverridingMethod(t, "hashCode()", atypeFactory)) { + assert t.getReceiverType() != null; + t.getReceiverType().replaceAnnotation(picoTypeFactory.READONLY); + } else if (PICOTypeUtil.isMethodOrOverridingMethod( + t, "equals(java.lang.Object)", atypeFactory)) { + assert t.getReceiverType() != null; + t.getReceiverType().replaceAnnotation(picoTypeFactory.READONLY); + t.getParameterTypes().get(0).replaceAnnotation(picoTypeFactory.READONLY); + } + } else { + return null; + } + + // Array decl methods + // Array methods are implemented as JVM native method, so we cannot add that to stubs. + // for now: default array in receiver, parameter and return type to RDM + if (t.getReceiverType() != null) { + if (PICOTypeUtil.isArrayType(t.getReceiverType(), atypeFactory)) { + if (t.toString() + .equals("Object clone(Array this)")) { // Receiver type will not be + // viewpoint adapted: + // SyntheticArrays.replaceReturnType() will rollback the viewpoint adapt + // result. + // Use readonly to allow all invocations. + if (!t.getReceiverType().hasAnnotationInHierarchy(picoTypeFactory.READONLY)) + t.getReceiverType().replaceAnnotation(picoTypeFactory.READONLY); + // The return type will be fixed by SyntheticArrays anyway. + // Qualifiers added here will not have effect. + } + } + } + + return null; + } + } + + /** + * {@inheritDoc} This is for overriding the behavior of DefaultQualifierForUse and use + * PICOQualifierForUseTypeAnnotator. + * + * @return PICOQualifierForUseTypeAnnotator + */ + @Override + protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator() { + return new PICOQualifierForUseTypeAnnotator(this); + } + + /** QualifierForUseTypeAnnotator */ + public static class PICOQualifierForUseTypeAnnotator + extends DefaultQualifierForUseTypeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOQualifierForUseTypeAnnotator. + * + * @param typeFactory the type factory + */ + public PICOQualifierForUseTypeAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) typeFactory; + } + + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Void aVoid) { + + Element element = type.getUnderlyingType().asElement(); + AnnotationMirrorSet annosToApply = getDefaultAnnosForUses(element); + + if (annosToApply.contains(picoTypeFactory.MUTABLE) + || annosToApply.contains(picoTypeFactory.IMMUTABLE)) { + type.addMissingAnnotations(annosToApply); + } + + // Below copied from super.super + // TODO add a function to super.super visitor + if (!type.getTypeArguments().isEmpty()) { + // Only declared types with type arguments might be recursive. + if (visitedNodes.containsKey(type)) { + return visitedNodes.get(type); + } + visitedNodes.put(type, null); + } + Void r = null; + if (type.getEnclosingType() != null) { + scan(type.getEnclosingType(), null); + } + r = scanAndReduce(type.getTypeArguments(), null, r); + return r; + } + } + + /** DefaultForTypeAnnotator */ + public static class PICODefaultForTypeAnnotator extends DefaultForTypeAnnotator { + + /** + * Create a new PICODefaultForTypeAnnotator. + * + * @param typeFactory the type factory + */ + public PICODefaultForTypeAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + } + + /** Also applies implicits to method receiver */ + @Override + public Void visitExecutable(AnnotatedExecutableType t, Void p) { + // TODO The implementation before doesn't work after update. Previously, I scanned the + // method receiver without null check. But even if I check nullness, scanning receiver + // at first caused some tests to fail. Need to investigate the reason. + super.visitExecutable(t, p); + // Also scan the receiver to apply implicit annotation + if (t.getReceiverType() != null) { + return scanAndReduce(t.getReceiverType(), p, null); + } + return null; + } + + @Override + protected Void scan(AnnotatedTypeMirror type, Void p) { + // If underlying type is enum or enum constant, appy @Immutable to type + // PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); + return super.scan(type, p); + } + } + + // TODO Right now, instance method receiver cannot inherit bound annotation from class element, + // and this caused the inconsistency when accessing the type of receiver while visiting the + // method + // and while visiting the variable tree. Implicit annotation can be inserted to method receiver + // via + // extending DefaultForTypeAnnotator; But InheritedFromClassAnnotator cannot be inheritted + // because its constructor is private and I can't override it to also inherit bound annotation + // from class + // element to the declared receiver type of instance methods. To view the details, look at + // ImmutableClass1.java testcase. + // class PICOInheritedFromClassAnnotator extends InheritedFromClassAnnotator {} + /** PICO SuperClause Annotator */ + public static class PICOSuperClauseAnnotator extends TreeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOSuperClauseAnnotator. + * + * @param atypeFactory the type factory + */ + public PICOSuperClauseAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) atypeFactory; + } + + /** + * Check if the given path is a super clause. + * + * @param path the path to check + * @return true if the given path is a super clause, false otherwise + */ + public static boolean isSuperClause(TreePath path) { + if (path == null) { + return false; + } + return TreeUtils.isClassTree(path.getParentPath().getLeaf()); + } + + /** + * Add default annotation from main class to super clause + * + * @param tree the tree to add default annotation + * @param mirror the annotated type mirror to add default annotation + */ + private void addDefaultFromMain(Tree tree, AnnotatedTypeMirror mirror) { + TreePath path = atypeFactory.getPath(tree); + + // only annotates when: + // 1. it's a super clause, AND + // 2. atm OR tree is not annotated + // Note: TreeUtils.typeOf returns no stub or default annotations, but in this scenario + // they are not needed + // Here only explicit annotation on super clause have effect because framework default + // rule is override + if (isSuperClause(path) + && (!mirror.hasAnnotationInHierarchy(picoTypeFactory.READONLY) + || atypeFactory + .getQualifierHierarchy() + .findAnnotationInHierarchy( + TreeUtils.typeOf(tree).getAnnotationMirrors(), + picoTypeFactory.READONLY) + == null)) { + AnnotatedTypeMirror enclosing = + atypeFactory.getAnnotatedType(TreePathUtil.enclosingClass(path)); + AnnotationMirror mainBound = + enclosing.getAnnotationInHierarchy(picoTypeFactory.READONLY); + mirror.replaceAnnotation(mainBound); + } + } + + @Override + public Void visitIdentifier( + IdentifierTree identifierTree, AnnotatedTypeMirror annotatedTypeMirror) { + // super clauses without type param use this + addDefaultFromMain(identifierTree, annotatedTypeMirror); + return super.visitIdentifier(identifierTree, annotatedTypeMirror); + } + + @Override + public Void visitParameterizedType( + ParameterizedTypeTree parameterizedTypeTree, + AnnotatedTypeMirror annotatedTypeMirror) { + // super clauses with type param use this + addDefaultFromMain(parameterizedTypeTree, annotatedTypeMirror); + return super.visitParameterizedType(parameterizedTypeTree, annotatedTypeMirror); + } + } + + /** + * Defaulting only applies the same annotation to all class declarations, and we need this to + * "only default enums" to immutable + */ + public static class PICOEnumDefaultAnnotator extends TypeAnnotator { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new PICOEnumDefaultAnnotator. + * + * @param typeFactory the type factory + */ + public PICOEnumDefaultAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) typeFactory; + } + + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Void aVoid) { + if (PICOTypeUtil.isEnumOrEnumConstant(type)) { + type.addMissingAnnotations(Collections.singleton(picoTypeFactory.IMMUTABLE)); + } + return super.visitDeclared(type, aVoid); + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitStore.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitStore.java new file mode 100644 index 00000000000..b123973939c --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitStore.java @@ -0,0 +1,38 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractStore; + +import java.util.Map; + +/** The store for the immutability type system. */ +public class PICONoInitStore extends CFAbstractStore { + /** The initialized fields. */ + protected Map<@Immutable FieldAccess, PICONoInitValue> initializedFields; + + /** + * Create a new PICONoInitStore. + * + * @param analysis the analysis + * @param sequentialSemantics whether the analysis uses sequential semantics + */ + public PICONoInitStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + } + + /** + * Create a new PICONoInitStore. + * + * @param s the store to copy + */ + public PICONoInitStore(PICONoInitStore s) { + super(s); + if (s.initializedFields != null) { + initializedFields = s.initializedFields; + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitSubchecker.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitSubchecker.java new file mode 100644 index 00000000000..c85af0400b5 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitSubchecker.java @@ -0,0 +1,30 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.initialization.InitializationFieldAccessSubchecker; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeVisitor; + +import java.util.Set; + +/** The PICO subchecker. */ +public class PICONoInitSubchecker extends BaseTypeChecker { + /** Create a new PICONoInitSubchecker. */ + public PICONoInitSubchecker() {} + + @Override + public PICONoInitAnnotatedTypeFactory getTypeFactory() { + return (PICONoInitAnnotatedTypeFactory) super.getTypeFactory(); + } + + @Override + protected Set> getImmediateSubcheckerClasses() { + Set> checkers = super.getImmediateSubcheckerClasses(); + checkers.add(InitializationFieldAccessSubchecker.class); + return checkers; + } + + @Override + protected BaseTypeVisitor createSourceVisitor() { + return new PICONoInitVisitor(this); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitTransfer.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitTransfer.java new file mode 100644 index 00000000000..d00d215f5d3 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitTransfer.java @@ -0,0 +1,49 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.VariableTree; + +import org.checkerframework.dataflow.analysis.RegularTransferResult; +import org.checkerframework.dataflow.analysis.TransferInput; +import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.NullLiteralNode; +import org.checkerframework.framework.flow.CFAbstractTransfer; +import org.checkerframework.javacutil.TreeUtils; + +import javax.lang.model.element.VariableElement; + +/** The transfer function for the immutability type system. */ +public class PICONoInitTransfer + extends CFAbstractTransfer { + /** + * Create a new PICONoInitTransfer. + * + * @param analysis the analysis + */ + public PICONoInitTransfer(PICONoInitAnalysis analysis) { + super(analysis); + } + + @Override + public TransferResult visitAssignment( + AssignmentNode n, TransferInput in) { + if (n.getExpression() instanceof NullLiteralNode + && n.getTarget().getTree() instanceof VariableTree) { + VariableElement varElement = + TreeUtils.elementFromDeclaration((VariableTree) n.getTarget().getTree()); + // Below is for removing false positive warning of bottom illegal write cacused by + // refining field to @Bottom if + // field initializer is null. + // Forbid refinement from null literal in initializer to fields variable tree(identifier + // tree not affected, e.g. + // assigning a field as null in instance methods or constructors) + if (varElement != null && varElement.getKind().isField()) { + PICONoInitStore store = in.getRegularStore(); + PICONoInitValue storeValue = in.getValueOfSubNode(n); + PICONoInitValue value = moreSpecificValue(null, storeValue); + return new RegularTransferResult<>(finishValue(value, store), store); + } + } + return super.visitAssignment(n, in); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitValue.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitValue.java new file mode 100644 index 00000000000..c1444db57e6 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitValue.java @@ -0,0 +1,24 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.javacutil.AnnotationMirrorSet; + +import javax.lang.model.type.TypeMirror; + +/** The abstract value for the immutability type system. */ +public class PICONoInitValue extends CFAbstractValue { + /** + * Create a new PICONoInitValue. + * + * @param analysis the analysis + * @param annotations the annotations + * @param underlyingType the underlying type + */ + public PICONoInitValue( + CFAbstractAnalysis analysis, + AnnotationMirrorSet annotations, + TypeMirror underlyingType) { + super(analysis, annotations, underlyingType); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitVisitor.java new file mode 100644 index 00000000000..d861573fbc9 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitVisitor.java @@ -0,0 +1,585 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.ArrayAccessTree; +import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.CompoundAssignmentTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewArrayTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.Tree.Kind; +import com.sun.source.tree.UnaryTree; +import com.sun.source.tree.VariableTree; + +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.common.basetype.TypeValidator; +import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; + +import java.util.Map; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.TypeElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; + +/** The visitor for the immutability type system. */ +public class PICONoInitVisitor extends BaseTypeVisitor { + /** whether to only check observational purity */ + protected final boolean abstractStateOnly; + + /** + * Create a new PICONoInitVisitor. + * + * @param checker the checker + */ + public PICONoInitVisitor(BaseTypeChecker checker) { + super(checker); + abstractStateOnly = checker.hasOption("abstractStateOnly"); + } + + @Override + protected TypeValidator createTypeValidator() { + return new PICOValidator(checker, this, atypeFactory); + } + + @Override + protected void checkConstructorResult( + AnnotatedExecutableType constructorType, ExecutableElement constructorElement) {} + + // This method is for validating usage of mutability qualifier is conformable to element + // declaration, + // Ugly thing here is that declarationType is not the result of calling the other method - + // PICOTypeUtil#getBoundTypeOfTypeDeclaration. Instead it's the result of calling + // ATF#getAnnotatedType(Element). + // Why it works is that PICOTypeUtil#getBoundTypeOfTypeDeclaration and + // ATF#getAnnotatedType(Element) has + // the same effect most of the time except on java.lang.Object. We need to be careful when + // modifying + // PICOTypeUtil#getBoundTypeOfTypeDeclaration so that it has the same behaviour as + // ATF#getAnnotatedType(Element) + // (at least for types other than java.lang.Object) + @Override + public boolean isValidUse( + AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { + + // FIXME workaround for poly anno, remove after fix substitutable poly and add poly vp rules + if (useType.hasAnnotation(atypeFactory.POLY_MUTABLE)) { + return true; + } + + AnnotationMirror declared = declarationType.getAnnotationInHierarchy(atypeFactory.READONLY); + AnnotationMirror used = useType.getAnnotationInHierarchy(atypeFactory.READONLY); + + return isAdaptedSubtype(used, declared); + } + + @Override + public boolean isValidUse(AnnotatedArrayType type, Tree tree) { + // You don't need adapted subtype if the decl bound is guaranteed to be RDM. + // That simply means that any use is valid except bottom. + AnnotationMirror used = type.getAnnotationInHierarchy(atypeFactory.READONLY); + return !AnnotationUtils.areSame(used, atypeFactory.BOTTOM); + } + + /** + * Check if the lhs is adapted subtype of rhs. + * + * @param lhs the lhs annotation + * @param rhs the rhs annotation + * @return true if lhs is adapted subtype of rhs, false otherwise + */ + private boolean isAdaptedSubtype(AnnotationMirror lhs, AnnotationMirror rhs) { + PICOViewpointAdapter vpa = atypeFactory.getViewpointAdapter(); + AnnotationMirror adapted = vpa.combineAnnotationWithAnnotation(lhs, rhs); + return atypeFactory.getQualifierHierarchy().isSubtypeQualifiersOnly(adapted, lhs); + } + + @Override + protected boolean commonAssignmentCheck( + Tree varTree, + ExpressionTree valueExp, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + AnnotatedTypeMirror var = atypeFactory.getAnnotatedTypeLhs(varTree); + assert var != null : "no variable found for tree: " + varTree; + + if (!validateType(varTree, var)) { + return false; + } + + if (varTree instanceof VariableTree) { + VariableElement element = TreeUtils.elementFromDeclaration((VariableTree) varTree); + if (element.getKind() == ElementKind.FIELD && !ElementUtils.isStatic(element)) { + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(varTree, atypeFactory); + // var is singleton, so shouldn't modify var directly. Otherwise, the variable + // tree's type will be + // altered permanently, and other clients who access this type will see the change, + // too. + AnnotatedTypeMirror varAdapted = var.shallowCopy(true); + // Viewpoint adapt varAdapted to the bound. + // PICOInferenceAnnotatedTypeFactory#viewpointAdaptMember() + // mutates varAdapted, so after the below method is called, varAdapted is the result + // adapted to bound + atypeFactory.getViewpointAdapter().viewpointAdaptMember(bound, element, varAdapted); + // Pass varAdapted here as lhs type. + // Caution: cannot pass var directly. Modifying type in PICOInferenceTreeAnnotator# + // visitVariable() will cause wrong type to be gotton here, as on inference side, + // atm is uniquely determined by each element. + return commonAssignmentCheck(varAdapted, valueExp, errorKey, extraArgs); + } + } + + return commonAssignmentCheck(var, valueExp, errorKey, extraArgs); + } + + @Override + protected void checkConstructorInvocation( + AnnotatedDeclaredType invocation, + AnnotatedExecutableType constructor, + NewClassTree newClassTree) { + // TODO Is the copied code really needed? + /*Copied Code Start*/ + AnnotatedDeclaredType returnType = (AnnotatedDeclaredType) constructor.getReturnType(); + // When an interface is used as the identifier in an anonymous class (e.g. new Comparable() + // {}) + // the constructor method will be Object.init() {} which has an Object return type + // When TypeHierarchy attempts to convert it to the supertype (e.g. Comparable) it will + // return + // null from asSuper and return false for the check. Instead, copy the primary annotations + // to the declared type and then do a subtyping check + if (invocation.getUnderlyingType().asElement().getKind().isInterface() + && TypesUtils.isObject(returnType.getUnderlyingType())) { + final AnnotatedDeclaredType retAsDt = invocation.deepCopy(); + retAsDt.replaceAnnotations(returnType.getAnnotations()); + returnType = retAsDt; + } else if (newClassTree.getClassBody() != null) { + // An anonymous class invokes the constructor of its super class, so the underlying + // types of invocation and returnType are not the same. Call asSuper so they are the + // same and the is subtype tests below work correctly + invocation = AnnotatedTypes.asSuper(atypeFactory, invocation, returnType); + } + /*Copied Code End*/ + + // The immutability return qualifier of the constructor (returnType) must be supertype of + // the constructor invocation immutability qualifier(invocation). + if (!atypeFactory + .getQualifierHierarchy() + .isSubtypeQualifiersOnly( + invocation.getAnnotationInHierarchy(atypeFactory.READONLY), + returnType.getAnnotationInHierarchy(atypeFactory.READONLY))) { + checker.reportError( + newClassTree, "constructor.invocation.invalid", invocation, returnType); + } + } + + @Override + public Void visitMethod(MethodTree node, Void p) { + AnnotatedExecutableType executableType = atypeFactory.getAnnotatedType(node); + + if (TreeUtils.isConstructor(node)) { + AnnotatedDeclaredType constructorReturnType = + (AnnotatedDeclaredType) executableType.getReturnType(); + if (constructorReturnType.hasAnnotation(atypeFactory.READONLY) + || constructorReturnType.hasAnnotation(atypeFactory.POLY_MUTABLE)) { + checker.reportError(node, "constructor.return.invalid", constructorReturnType); + return super.visitMethod(node, p); + } + // if no explicit anno it must inherit from class decl so identical + } else { + // Feat: let's just use validator to tell whether the receiver is compatible with bound + // or not + /* + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(node, atypeFactory); + // For non-constructor methods + AnnotatedDeclaredType declareReceiverType = executableType.getReceiverType(); + if (declareReceiverType != null) { + if (bound != null + && !bound.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE) + && !atypeFactory + .getQualifierHierarchy() + .isSubtypeQualifiersOnly( + declareReceiverType.getAnnotationInHierarchy(READONLY), + bound.getAnnotationInHierarchy(READONLY)) + // Below three are allowed on declared receiver types of instance methods in + // either @Mutable class or @Immutable class + && !declareReceiverType.hasAnnotation(READONLY) + && !declareReceiverType.hasAnnotation(POLY_MUTABLE)) { + checker.reportError(node, "method.receiver.incompatible", declareReceiverType, bound); + } + } + */ + } + + flexibleOverrideChecker(node); + + // ObjectIdentityMethod check + if (abstractStateOnly) { + if (PICOTypeUtil.isObjectIdentityMethod(node, atypeFactory)) { + ObjectIdentityMethodEnforcer.check( + atypeFactory.getPath(node.getBody()), atypeFactory, checker); + } + } + return super.visitMethod(node, p); + } + + /** + * Check if the method is flexible overriding. Flexible overriding is allowed if the overriding + * method's return type is a subtype of the overridden method's return type. + * + * @param node the method node + */ + private void flexibleOverrideChecker(MethodTree node) { + // Method overriding checks + // TODO Copied from super, hence has lots of duplicate code with super. We need to + // change the signature of checkOverride() method to also pass ExecutableElement for + // viewpoint adaptation. + ExecutableElement methodElement = TreeUtils.elementFromDeclaration(node); + AnnotatedDeclaredType enclosingType = + (AnnotatedDeclaredType) + atypeFactory.getAnnotatedType(methodElement.getEnclosingElement()); + + Map<@Immutable AnnotatedDeclaredType, ExecutableElement> overriddenMethods = + AnnotatedTypes.overriddenMethods(elements, atypeFactory, methodElement); + for (Map.Entry<@Immutable AnnotatedDeclaredType, ExecutableElement> pair : + overriddenMethods.entrySet()) { + AnnotatedDeclaredType overriddenType = pair.getKey(); + AnnotatedExecutableType overriddenMethod = + AnnotatedTypes.asMemberOf(types, atypeFactory, enclosingType, pair.getValue()); + // Viewpoint adapt super method executable type to current class bound(is this always + // class bound?) + // to allow flexible overriding + atypeFactory + .getViewpointAdapter() + .viewpointAdaptMethod(enclosingType, pair.getValue(), overriddenMethod); + AnnotatedExecutableType overrider = atypeFactory.getAnnotatedType(node); + if (!checkOverride(node, overrider, enclosingType, overriddenMethod, overriddenType)) { + // Stop at the first mismatch; this makes a difference only if + // -Awarns is passed, in which case multiple warnings might be raised on + // the same method, not adding any value. See Issue 373. + break; + } + } + } + + // Disables method overriding checks in BaseTypeVisitor + @Override + protected boolean checkOverride( + MethodTree overriderTree, + AnnotatedDeclaredType overridingType, + AnnotatedExecutableType overridden, + AnnotatedDeclaredType overriddenType) { + return true; + } + + @Override + public Void visitAssignment(AssignmentTree node, Void p) { + ExpressionTree variable = node.getVariable(); + // TODO Question Here, receiver type uses flow refinement. But in commonAssignmentCheck to + // compute lhs type + // , it doesn't. This causes inconsistencies when enforcing immutability and doing subtype + // check. I overrode + // getAnnotatedTypeLhs() to also use flow sensitive refinement, but came across with + // "private access" problem + // on field "computingAnnotatedTypeMirrorOfLHS" + checkAssignment(node, variable); + return super.visitAssignment(node, p); + } + + @Override + public Void visitCompoundAssignment(CompoundAssignmentTree node, Void p) { + ExpressionTree variable = node.getVariable(); + checkAssignment(node, variable); + return super.visitCompoundAssignment(node, p); + } + + @Override + public Void visitUnary(UnaryTree node, Void p) { + if (PICOTypeUtil.isSideEffectingUnaryTree(node)) { + ExpressionTree variable = node.getExpression(); + checkAssignment(node, variable); + } + return super.visitUnary(node, p); + } + + /** + * Check if the assignment is valid. Assignment is not checked if it's in initializer block or + * if it happens in the constructor. + * + * @param tree the assignment node + * @param variable the variable in the assignment + */ + private void checkAssignment(Tree tree, ExpressionTree variable) { + AnnotatedTypeMirror receiverType = atypeFactory.getReceiverType(variable); + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(getCurrentPath()); + if (enclosingMethod != null && TreeUtils.isConstructor(enclosingMethod)) { + // If the enclosing method is constructor, we don't need to check the receiver type + return; + } + if (TreePathUtil.isTopLevelAssignmentInInitializerBlock(getCurrentPath())) { + // If the assignment is in initializer block, we don't need to check the receiver type + return; + } + // Cannot use receiverTree = TreeUtils.getReceiverTree(variable) to determine if it's + // field assignment or not. Because for field assignment with implicit "this", receiverTree + // is null but receiverType is non-null. We still need to check this case. + if (receiverType != null && !allowWrite(receiverType, variable)) { + reportFieldOrArrayWriteError(tree, variable, receiverType); + } + } + + /** + * Helper method to check if the receiver type allows writing. The receiver type must be mutable + * or the field is assignable. If not, return false. + * + * @param receiverType the receiver type + * @param variable the variable in the assignment + * @return true if the receiver type allows writing, false otherwise + */ + private boolean allowWrite(AnnotatedTypeMirror receiverType, ExpressionTree variable) { + if (receiverType.hasAnnotation(atypeFactory.MUTABLE)) { + return true; + } else return PICOTypeUtil.isAssigningAssignableField(variable, atypeFactory); + } + + /** + * Helper method to report field or array write error. + * + * @param tree the node to report the error + * @param variable the variable in the assignment + * @param receiverType the receiver type + */ + private void reportFieldOrArrayWriteError( + Tree tree, ExpressionTree variable, AnnotatedTypeMirror receiverType) { + if (variable.getKind() == Kind.MEMBER_SELECT) { + checker.reportError( + TreeUtils.getReceiverTree(variable), "illegal.field.write", receiverType); + } else if (variable.getKind() == Kind.IDENTIFIER) { + checker.reportError(tree, "illegal.field.write", receiverType); + } else if (variable.getKind() == Kind.ARRAY_ACCESS) { + checker.reportError( + ((ArrayAccessTree) variable).getExpression(), + "illegal.array.write", + receiverType); + } else { + throw new BugInCF("Unknown assignment variable at: ", tree); + } + } + + @Override + public Void visitVariable(VariableTree node, Void p) { + VariableElement element = TreeUtils.elementFromDeclaration(node); + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(element); + if (element.getKind() == ElementKind.FIELD) { + if (type.hasAnnotation(atypeFactory.POLY_MUTABLE)) { + checker.reportError(node, "field.polymutable.forbidden", element); + } + } + return super.visitVariable(node, p); + } + + @Override + public Void visitNewArray(NewArrayTree tree, Void p) { + checkNewArrayCreation(tree); + return super.visitNewArray(tree, p); + } + + /** + * Helper method to check the immutability type on new array creation. Only @Immutable, @Mutable + * and @ReceiverDependentMutable are allowed. + * + * @param tree the tree to check + */ + private void checkNewArrayCreation(Tree tree) { + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); + if (!(type.hasAnnotation(atypeFactory.IMMUTABLE) + || type.hasAnnotation(atypeFactory.MUTABLE) + || type.hasAnnotation(atypeFactory.RECEIVER_DEPENDENT_MUTABLE) + // TODO: allow poly_mutable creation or not? + || type.hasAnnotation(atypeFactory.POLY_MUTABLE))) { + checker.reportError(tree, "array.new.invalid", type); + } + } + + @Override + public Void visitMethodInvocation(MethodInvocationTree node, Void p) { + super.visitMethodInvocation(node, p); + ParameterizedExecutableType mfuPair = atypeFactory.methodFromUse(node); + AnnotatedExecutableType invokedMethod = mfuPair.executableType; + ExecutableElement invokedMethodElement = invokedMethod.getElement(); + // Only check invocability if it's super call, as non-super call is already checked + // by super implementation(of course in both cases, invocability is not checked when + // invoking static methods) + if (!ElementUtils.isStatic(invokedMethodElement) + && TreeUtils.isSuperConstructorCall(node)) { + checkMethodInvocability(invokedMethod, node); + } + return null; + } + + @Override + protected AnnotationMirrorSet getExceptionParameterLowerBoundAnnotations() { + AnnotationMirrorSet result = new AnnotationMirrorSet(); + result.add(atypeFactory.getQualifierHierarchy().getBottomAnnotation(atypeFactory.BOTTOM)); + return result; + } + + @Override + protected AnnotationMirrorSet getThrowUpperBoundAnnotations() { + AnnotationMirrorSet result = new AnnotationMirrorSet(); + result.add(atypeFactory.getQualifierHierarchy().getTopAnnotation(atypeFactory.READONLY)); + return result; + } + + @Override + public void processClassTree(ClassTree tree) { + TypeElement typeElement = TreeUtils.elementFromDeclaration(tree); + // TODO Don't process anonymous class. I'm not even sure if whether + // processClassTree(ClassTree) is called on anonymous class tree + if (typeElement.toString().contains("anonymous")) { + super.processClassTree(tree); + return; + } + // TODO(Aosen): since this is also checking validity, consider whether we can move this to + // PICOValidator + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); + // Class annotation has to be either @Mutable, @ReceiverDependentMutable or @Immutable + // Static class can not be @RDM + if ((!bound.hasAnnotation(atypeFactory.MUTABLE) + && !bound.hasAnnotation(atypeFactory.RECEIVER_DEPENDENT_MUTABLE) + && !bound.hasAnnotation(atypeFactory.IMMUTABLE)) + || (tree.getModifiers().getFlags().contains(Modifier.STATIC) + && bound.hasAnnotation(atypeFactory.RECEIVER_DEPENDENT_MUTABLE))) { + checker.reportError(tree, "class.bound.invalid", bound); + return; // Doesn't process the class tree anymore + } + + // Issue warnings on implicit shallow immutable: + // Condition: + // * Class decl == Immutable or RDM + // * move rdm default error here. see 3.6.3 last part. + // liansun + // * Member is field + // * Member's declared bound == Mutable + // * Member's use anno == null + if (bound.hasAnnotation(atypeFactory.IMMUTABLE) + || bound.hasAnnotation(atypeFactory.RECEIVER_DEPENDENT_MUTABLE)) { + for (Tree member : tree.getMembers()) { + if (member.getKind() == Kind.VARIABLE) { + Element ele = TreeUtils.elementFromTree(member); + assert ele != null; + // fromElement will not apply defaults, if no explicit anno exists in code, + // mirror have no anno + AnnotatedTypeMirror noDefaultMirror = atypeFactory.fromElement(ele); + TypeMirror ty = ele.asType(); + if (ty.getKind() == TypeKind.TYPEVAR) { + ty = TypesUtils.upperBound(ty); + } + if (AnnotationUtils.containsSameByName( + atypeFactory.getTypeDeclarationBounds(ty), atypeFactory.MUTABLE) + && !noDefaultMirror.hasAnnotationInHierarchy(atypeFactory.READONLY)) { + checker.reportError(member, "implicit.shallow.immutable"); + } + } + } + } + super.processClassTree(tree); + } + + /** + * The invoked constructor’s return type adapted to the invoking constructor’s return type must + * be a supertype of the invoking constructor’s return type. Since InitializationChecker does + * not apply any type rules at here, only READONLY hierarchy is checked. + * + * @param superCall the super invocation, e.g., "super()" + * @param errorKey the error key, e.g., "super.invocation.invalid" + */ + @Override + protected void checkThisOrSuperConstructorCall( + MethodInvocationTree superCall, @CompilerMessageKey String errorKey) { + MethodTree enclosingMethod = methodTree; + AnnotatedTypeMirror superType = atypeFactory.getAnnotatedType(superCall); + AnnotatedExecutableType constructorType = atypeFactory.getAnnotatedType(enclosingMethod); + AnnotationMirror superTypeMirror = + superType.getAnnotationInHierarchy(atypeFactory.READONLY); + AnnotationMirror constructorTypeMirror = + constructorType.getReturnType().getAnnotationInHierarchy(atypeFactory.READONLY); + if (!atypeFactory + .getQualifierHierarchy() + .isSubtypeQualifiersOnly(constructorTypeMirror, superTypeMirror)) { + checker.reportError( + superCall, errorKey, constructorTypeMirror, superCall, superTypeMirror); + } + super.checkThisOrSuperConstructorCall(superCall, errorKey); + } + + @Override + protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); + + final TypeKind castTypeKind = castType.getKind(); + if (castTypeKind == TypeKind.DECLARED) { + // Don't issue an error if the mutability annotations are equivalent to the qualifier + // upper bound of the type. + // BaseTypeVisitor#isTypeCastSafe is not used, to be consistent with inference which + // only have mutability qualifiers if inference is supporting FBC in the future, this + // overridden method can be removed. + AnnotatedDeclaredType castDeclared = (AnnotatedDeclaredType) castType; + AnnotationMirror bound = + qualifierHierarchy.findAnnotationInHierarchy( + atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()), + atypeFactory.READONLY); + assert bound != null; + + if (AnnotationUtils.areSame( + castDeclared.getAnnotationInHierarchy(atypeFactory.READONLY), bound)) { + return true; + } + } + + return super.isTypeCastSafe(castType, exprType); + } + + @Override + protected boolean commonAssignmentCheck( + AnnotatedTypeMirror varType, + AnnotatedTypeMirror valueType, + Tree valueTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + // TODO: WORKAROUND: anonymous class handling + if (TypesUtils.isAnonymous(valueType.getUnderlyingType())) { + AnnotatedTypeMirror newValueType = varType.deepCopy(); + newValueType.replaceAnnotation( + valueType.getAnnotationInHierarchy(atypeFactory.READONLY)); + valueType = newValueType; + } + return super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOQualifierHierarchy.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOQualifierHierarchy.java new file mode 100644 index 00000000000..fdddd689e3b --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOQualifierHierarchy.java @@ -0,0 +1,40 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.pico.qual.PICOBottom; +import org.checkerframework.checker.pico.qual.PICOLost; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.type.NoElementQualifierHierarchy; + +import java.lang.annotation.Annotation; +import java.util.Collection; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; + +/** A qualifier hierarchy for the PICO checker. */ +public class PICOQualifierHierarchy extends NoElementQualifierHierarchy { + + /** + * Creates a PICOQualifierHierarchy from the given classes. + * + * @param qualifierClasses classes of annotations that are the qualifiers + * @param elements element utils + * @param atypeFactory the associated type factory + */ + public PICOQualifierHierarchy( + Collection> qualifierClasses, + Elements elements, + GenericAnnotatedTypeFactory atypeFactory) { + super(qualifierClasses, elements, atypeFactory); + } + + @Override + public boolean isSubtypeQualifiers(AnnotationMirror subAnno, AnnotationMirror superAnno) { + // Lost is not reflexive and the only subtype is Bottom + if (atypeFactory.areSameByClass(superAnno, PICOLost.class) + && !atypeFactory.areSameByClass(subAnno, PICOBottom.class)) { + return false; + } + return super.isSubtypeQualifiers(subAnno, superAnno); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOTypeUtil.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOTypeUtil.java new file mode 100644 index 00000000000..ac8b0314a9a --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOTypeUtil.java @@ -0,0 +1,455 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.UnaryTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; +import com.sun.tools.javac.code.Symbol; + +import org.checkerframework.checker.pico.qual.Assignable; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.ObjectIdentityMethod; +import org.checkerframework.framework.qual.DefaultFor; +import org.checkerframework.framework.qual.TypeKind; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; + +import java.util.HashSet; +import java.util.Iterator; +import java.util.Map; +import java.util.Set; + +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.TypeElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.DeclaredType; + +/** Utility methods for the PICO Checker. */ +public class PICOTypeUtil { + /** Set of side-effecting unary operators. */ + private static final Set sideEffectingUnaryOperators; + + static { + sideEffectingUnaryOperators = new HashSet<>(); + sideEffectingUnaryOperators.add(Tree.Kind.POSTFIX_INCREMENT); + sideEffectingUnaryOperators.add(Tree.Kind.PREFIX_INCREMENT); + sideEffectingUnaryOperators.add(Tree.Kind.POSTFIX_DECREMENT); + sideEffectingUnaryOperators.add(Tree.Kind.PREFIX_DECREMENT); + } + + /** Make constructor private for util class. */ + private PICOTypeUtil() {} + + /** + * Determine if Typekind is one of the @DefaultFor typeKinds in @Immutable annotation. + * + * @param atm AnnotatedTypeMirror to be checked + * @return true if TypeKind is one of the @DefaultFor typeKinds in @Immutable annotation, false + * otherwise + */ + private static boolean isInTypeKindsOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { + DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + for (TypeKind typeKind : defaultFor.typeKinds()) { + if (typeKind.name().equals(atm.getKind().name())) return true; + } + return false; + } + + /** + * Determine if Type is one of the @DefaultFor types in @Immutable annotation. + * + * @param atm AnnotatedTypeMirror to be checked + * @return true if Type is one of the @DefaultFor types in @Immutable annotation, false + * otherwise + */ + private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { + if (!atm.getKind().name().equals(TypeKind.DECLARED.name())) { + return false; + } + DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + Class[] types = defaultFor.types(); + String fqn = TypesUtils.getQualifiedName((DeclaredType) atm.getUnderlyingType()); + for (Class type : types) { + if (type.getCanonicalName().contentEquals(fqn)) { + return true; + } + } + return false; + } + + /** + * Determine if the underlying type is implicitly immutable. This method is consistent with the + * types and typeKinds that are in @DefaultFor in the definition of @Immutable qualifier. + * + * @param atm AnnotatedTypeMirror to be checked + * @return true if the underlying type is implicitly immutable, false otherwise + */ + public static boolean isImplicitlyImmutableType(AnnotatedTypeMirror atm) { + return isInTypeKindsOfDefaultForOfImmutable(atm) || isInTypesOfDefaultForOfImmutable(atm); + } + + /** + * Returns the bound of type declaration enclosing the node. If no annotation exists on type + * declaration, bound is defaulted to @Mutable instead of having empty annotations. This method + * simply gets/defaults annotation on bounds of classes, but doesn't validate the correctness of + * the annotation. They are validated in {@link PICONoInitVisitor#processClassTree(ClassTree)} + * method. + * + * @param node tree whose enclosing type declaration's bound annotation is to be extracted + * @param atypeFactory pico type factory + * @return annotation on the bound of enclosing type declaration + */ + public static AnnotatedTypeMirror getBoundTypeOfEnclosingTypeDeclaration( + Tree node, AnnotatedTypeFactory atypeFactory) { + TypeElement typeElement = null; + if (node instanceof MethodTree) { + MethodTree methodTree = (MethodTree) node; + ExecutableElement element = TreeUtils.elementFromDeclaration(methodTree); + typeElement = ElementUtils.enclosingTypeElement(element); + } else if (node instanceof VariableTree) { + VariableTree variableTree = (VariableTree) node; + VariableElement variableElement = TreeUtils.elementFromDeclaration(variableTree); + assert variableElement != null && variableElement.getKind().isField(); + typeElement = ElementUtils.enclosingTypeElement(variableElement); + } + + if (typeElement != null) { + return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); + } + + return null; + } + + /** + * Returns the bound of type declaration enclosing the element. If no annotation exists on type + * declaration, bound is defaulted to @Mutable instead of having empty annotations. This method + * simply gets/defaults annotation on bounds of classes, but doesn't validate the correctness of + * the annotation. They are validated in {@link PICONoInitVisitor#processClassTree(ClassTree)} + * method. + * + * @param element element whose enclosing type declaration's bound annotation is to be extracted + * @param atypeFactory pico type factory + * @return annotation on the bound of enclosing type declaration + */ + public static AnnotatedTypeMirror getBoundTypeOfEnclosingTypeDeclaration( + Element element, AnnotatedTypeFactory atypeFactory) { + TypeElement typeElement = ElementUtils.enclosingTypeElement(element); + if (typeElement != null) { + return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); + } + return null; + } + + /** + * Returns the bound of type declaration. If no annotation exists on type declaration, bound is + * defaulted to @Mutable instead of having empty annotations. This method simply gets/defaults + * annotation on bounds of classes, but doesn't validate the correctness of the annotation. They + * are validated in {@link PICONoInitVisitor#processClassTree(ClassTree)} method. + * + * @param element type declaration whose bound annotation is to be extracted + * @param atypeFactory pico type factory + * @return annotation on the bound of type declaration + */ + public static AnnotatedTypeMirror getBoundTypeOfTypeDeclaration( + Element element, AnnotatedTypeFactory atypeFactory) { + // Reads bound annotation from source code or stub files + // Implicitly immutable types have @Immutable in its bound + // All other elements that are: not implicitly immutable types specified in definition of + // @Immutable qualifier; + // Or has no bound annotation on its type element declaration either in source tree or stub + // file(jdk.astub) have @Mutable in its bound + return atypeFactory.getAnnotatedType(element); + + // It's a bit strange that bound annotations on implicilty immutable types + // are not specified in the stub file. For implicitly immutable types, having bounds in stub + // file suppresses type cast warnings, because in base implementation, it checks cast type + // is whether + // from element itself. If yes, no matter what the casted type is, the warning is + // suppressed, which is + // also not wanted. BUT, they are applied @Immutable as their bounds CORRECTLY, because we + // have TypeAnnotator! + + // TODO This method doesn't have logic of handling anonymous class! We should implement it, + // maybe in different + // places, at some time. + } + + /** + * Helper method to determine a method using method name. + * + * @param methodType AnnotatedExecutableType of the method + * @param methodName Name of the method + * @param annotatedTypeFactory AnnotatedTypeFactory + * @return whether the method is the method or override a method + */ + public static boolean isMethodOrOverridingMethod( + AnnotatedExecutableType methodType, + String methodName, + AnnotatedTypeFactory annotatedTypeFactory) { + return isMethodOrOverridingMethod( + methodType.getElement(), methodName, annotatedTypeFactory); + } + + /** + * Helper method to determine if a method is the target method or overriding the target method. + * + * @param executableElement ExecutableElement of the method + * @param methodName Name of the method + * @param annotatedTypeFactory AnnotatedTypeFactory + * @return whether the method is the method or override a method + */ + public static boolean isMethodOrOverridingMethod( + ExecutableElement executableElement, + String methodName, + AnnotatedTypeFactory annotatedTypeFactory) { + // Check if it is the target method + if (executableElement.toString().contentEquals(methodName)) return true; + // Check if it is overriding the target method + // Because AnnotatedTypes.overriddenMethods returns all the methods overriden in the class + // hierarchy, we need to + // iterate over the set to check if it's overriding corresponding methods specifically in + // java.lang.Object class + Iterator> overriddenMethods = + AnnotatedTypes.overriddenMethods( + annotatedTypeFactory.getElementUtils(), + annotatedTypeFactory, + executableElement) + .entrySet() + .iterator(); + while (overriddenMethods.hasNext()) { + if (overriddenMethods.next().getValue().toString().contentEquals(methodName)) { + return true; + } + } + return false; + } + + /** + * Determine if the type is enum or enum constant. + * + * @param annotatedTypeMirror The annotated type mirror to check + * @return true if the type is enum or enum constant, false otherwise + */ + public static boolean isEnumOrEnumConstant(AnnotatedTypeMirror annotatedTypeMirror) { + Element element = + ((AnnotatedDeclaredType) annotatedTypeMirror).getUnderlyingType().asElement(); + return element != null + && (element.getKind() == ElementKind.ENUM_CONSTANT + || element.getKind() == ElementKind.ENUM); + } + + /** + * Check if a field is final or not. + * + * @param variableElement The field element + * @return true if the field is final, false otherwise + */ + public static boolean isFinalField(Element variableElement) { + assert variableElement instanceof VariableElement; + return ElementUtils.isFinal(variableElement); + } + + /** + * Check if a field is assignable. A field is assignable if it is static and not final, or has + * explicit @Assignable + * + * @param variableElement The field element + * @param provider The annotation provider + * @return true if the field is assignable + */ + public static boolean isAssignableField(Element variableElement, AnnotationProvider provider) { + if (!(variableElement instanceof VariableElement)) { + return false; + } + boolean hasExplicitAssignableAnnotation = + provider.getDeclAnnotation(variableElement, Assignable.class) != null; + if (!ElementUtils.isStatic(variableElement)) { + // Instance fields must have explicit @Assignable annotation to be assignable + return hasExplicitAssignableAnnotation; + } else { + // If there is explicit @Assignable annotation on static fields, then it's assignable; + // If there isn't, + // and the static field is not final, we treat it as if it's assignable field. + return hasExplicitAssignableAnnotation || !isFinalField(variableElement); + } + } + + /** + * Check if a field is @ReceiverDependantAssignable. Static fields always returns false. + * + * @param variableElement The field element + * @param provider The annotation provider + * @return true if the field is @ReceiverDependantAssignable + */ + public static boolean isReceiverDependantAssignable( + Element variableElement, AnnotationProvider provider) { + assert variableElement instanceof VariableElement; + if (ElementUtils.isStatic(variableElement)) { + // Static fields can never be @ReceiverDependantAssignable! + return false; + } + return !isAssignableField(variableElement, provider) && !isFinalField(variableElement); + } + + /** + * Check if a field has one and only one assignability qualifier. Only the following + * combinations are valid: + * + *

1. Explicit @Assignable 2. Final field 3. @ReceiverDependentAssignable, where there is no + * explicit annotation in the source code + * + * @param field The field element + * @param provider The annotation provider + * @return true if the field has one and only one assignability qualifier + */ + public static boolean hasOneAndOnlyOneAssignabilityQualifier( + VariableElement field, AnnotationProvider provider) { + boolean valid = false; + if (isAssignableField(field, provider) + && !isFinalField(field) + && !isReceiverDependantAssignable(field, provider)) { + valid = true; + } else if (!isAssignableField(field, provider) + && isFinalField(field) + && !isReceiverDependantAssignable(field, provider)) { + valid = true; + } else if (!isAssignableField(field, provider) + && !isFinalField(field) + && isReceiverDependantAssignable(field, provider)) { + assert !ElementUtils.isStatic(field); + valid = true; + } + return valid; + } + + /** + * Check if a field is a field that can be assigned to. A field is assignable if it is static + * and not final, or has explicit @Assignable + * + * @param tree The tree of the field + * @param provider The annotation provider + * @return true if the field is assignable + */ + public static boolean isAssigningAssignableField( + ExpressionTree tree, AnnotationProvider provider) { + Element fieldElement = TreeUtils.elementFromUse(tree); + if (fieldElement == null) return false; + return isAssignableField(fieldElement, provider); + } + + /** + * check if a tree is in static scope. + * + * @param treePath TreePath + * @return true if the tree is in static scope, false otherwise + */ + public static boolean inStaticScope(TreePath treePath) { + boolean in = false; + if (TreePathUtil.isTreeInStaticScope(treePath)) { + in = true; + // Exclude case in which enclosing class is static + ClassTree classTree = TreePathUtil.enclosingClass(treePath); + if (classTree != null + && classTree.getModifiers().getFlags().contains(Modifier.STATIC)) { + in = false; + } + } + return in; + } + + /** + * Check if a unary tree is side-effecting. + * + * @param tree UnaryTree + * @return true if the unary tree is side-effecting, false otherwise + */ + public static boolean isSideEffectingUnaryTree(final UnaryTree tree) { + return sideEffectingUnaryOperators.contains(tree.getKind()); + } + + /** + * !! Experimental !! + * + *

CF's isAnonymous cannot recognize some anonymous classes with annotation on new clause. + * This one hopefully will provide a workaround when the class tree is available. + * + *

This will work if an anonymous class decl tree is always a child node of a {@code + * NewClassTree}. i.e. an anonymous class declaration is always inside a new clause. + * + * @param tree a class decl tree. + * @param atypeFactory used to get the path. Any factory should be ok. + * @return whether the class decl tree is of an anonymous class + */ + public static boolean isAnonymousClassTree(ClassTree tree, AnnotatedTypeFactory atypeFactory) { + TreePath path = atypeFactory.getPath(tree); + Tree parent = path.getParentPath().getLeaf(); + return parent instanceof NewClassTree && ((NewClassTree) parent).getClassBody() != null; + } + + /** + * !! Experimental !! Check whether the type is actually an array. + * + * @param type AnnotatedDeclaredType + * @param typeFactory any AnnotatedTypeFactory + * @return true if the type is array + */ + public static boolean isArrayType( + AnnotatedDeclaredType type, AnnotatedTypeFactory typeFactory) { + Element ele = + typeFactory.getProcessingEnv().getTypeUtils().asElement(type.getUnderlyingType()); + + // If it is a user-declared "Array" class without package, a class / source file should be + // there. + // Otherwise, it is the java inner type. + return ele instanceof Symbol.ClassSymbol + && ElementUtils.getQualifiedName(ele).equals("Array") + && ((Symbol.ClassSymbol) ele).classfile == null + && ((Symbol.ClassSymbol) ele).sourcefile == null; + } + + /** + * Check if a method is an object identity method. + * + * @param node MethodTree of the method + * @param annotatedTypeFactory AnnotatedTypeFactory + * @return true if the method is an object identity method + */ + public static boolean isObjectIdentityMethod( + MethodTree node, AnnotatedTypeFactory annotatedTypeFactory) { + ExecutableElement element = TreeUtils.elementFromDeclaration(node); + return isObjectIdentityMethod(element, annotatedTypeFactory); + } + + /** + * Check if a method is an object identity method. + * + * @param executableElement ExecutableElement of the method + * @param annotatedTypeFactory AnnotatedTypeFactory + * @return whether this method is an object identity method + */ + public static boolean isObjectIdentityMethod( + ExecutableElement executableElement, AnnotatedTypeFactory annotatedTypeFactory) { + return annotatedTypeFactory.getDeclAnnotation(executableElement, ObjectIdentityMethod.class) + != null + || isMethodOrOverridingMethod(executableElement, "hashCode()", annotatedTypeFactory) + || isMethodOrOverridingMethod( + executableElement, "equals(java.lang.Object)", annotatedTypeFactory); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOValidator.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOValidator.java new file mode 100644 index 00000000000..88ecf0ac1c1 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOValidator.java @@ -0,0 +1,168 @@ +package org.checkerframework.checker.pico; + +import com.sun.source.tree.Tree; +import com.sun.source.tree.Tree.Kind; +import com.sun.source.tree.VariableTree; + +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeValidator; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; + +import java.util.Objects; + +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; + +/** + * Enforce correct usage of immutability and assignability qualifiers. TODO @PolyMutable is only + * used on constructor/method parameters or method return + */ +public class PICOValidator extends BaseTypeValidator { + /** The type factory for the PICO checker */ + private final PICONoInitAnnotatedTypeFactory picoTypeFactory = + (PICONoInitAnnotatedTypeFactory) atypeFactory; + + /** + * Create a new PICOValidator. + * + * @param checker the checker + * @param visitor the visitor + * @param atypeFactory the type factory + */ + public PICOValidator( + BaseTypeChecker checker, + BaseTypeVisitor visitor, + AnnotatedTypeFactory atypeFactory) { + super(checker, visitor, atypeFactory); + } + + @Override + public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { + checkStaticReceiverDependentMutableError(type, tree); + checkImplicitlyImmutableTypeError(type, tree); + checkOnlyOneAssignabilityModifierOnField(tree); + + return super.visitDeclared(type, tree); + } + + @Override + protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType( + AnnotatedTypeMirror type, Tree tree) { + // check top annotations in extends/implements clauses + if ((tree.getKind() == Kind.IDENTIFIER || tree.getKind() == Kind.PARAMETERIZED_TYPE) + && PICONoInitAnnotatedTypeFactory.PICOSuperClauseAnnotator.isSuperClause( + atypeFactory.getPath(tree))) { + return true; + } + // allow RDM on mutable fields with enclosing class bounded with mutable + if (tree instanceof VariableTree) { + VariableElement element = TreeUtils.elementFromDeclaration((VariableTree) tree); + if (element.getKind() == ElementKind.FIELD + && ElementUtils.enclosingTypeElement(element) != null) { + @Immutable AnnotationMirrorSet enclosingBound = + atypeFactory.getTypeDeclarationBounds( + Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)) + .asType()); + + @Immutable AnnotationMirrorSet declaredBound = + atypeFactory.getTypeDeclarationBounds(type.getUnderlyingType()); + + if (AnnotationUtils.containsSameByName(declaredBound, picoTypeFactory.MUTABLE) + && type.hasAnnotation(picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE) + && AnnotationUtils.containsSameByName( + enclosingBound, picoTypeFactory.MUTABLE)) { + return false; + } + } + } + // COPY from SUPER + if (type.getKind() != TypeKind.DECLARED && !type.getKind().isPrimitive()) { + return true; + } + // Do not call super because BaseTypeValidator will don't check local variable declaration + return !TreeUtils.isExpressionTree(tree) || TreeUtils.isTypeTree(tree); + } + + @Override + public Void visitArray(AnnotatedArrayType type, Tree tree) { + checkStaticReceiverDependentMutableError(type, tree); + // Array can not be implicitly immutable + return super.visitArray(type, tree); + } + + @Override + public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) { + checkImplicitlyImmutableTypeError(type, tree); + checkOnlyOneAssignabilityModifierOnField(tree); + return super.visitPrimitive(type, tree); + } + + /** + * Check that static fields do not have receiver-dependent mutable type. + * + * @param type the type to check + * @param tree the tree to check + */ + private void checkStaticReceiverDependentMutableError(AnnotatedTypeMirror type, Tree tree) { + if (!type.isDeclaration() // variables in static contexts and static fields use class + // decl as enclosing type + && PICOTypeUtil.inStaticScope(visitor.getCurrentPath()) + && !"" + .contentEquals( + Objects.requireNonNull( + TreePathUtil.enclosingClass( + visitor.getCurrentPath())) + .getSimpleName()) + // Exclude @RDM usages in anonymous classes + && type.hasAnnotation(picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE)) { + reportValidityResult("static.receiverdependentmutable.forbidden", type, tree); + } + } + + /** + * Check that implicitly immutable type has immutable or bottom type. Dataflow might refine + * immutable type to {@code @Bottom} (see RefineFromNull.java), so we accept @Bottom as a valid + * qualifier for implicitly immutable types. + * + * @param type the type to check + * @param tree the tree to check + */ + private void checkImplicitlyImmutableTypeError(AnnotatedTypeMirror type, Tree tree) { + if (PICOTypeUtil.isImplicitlyImmutableType(type) + && !type.hasAnnotation(picoTypeFactory.IMMUTABLE) + && !type.hasAnnotation(picoTypeFactory.BOTTOM)) { + reportInvalidAnnotationsOnUse(type, tree); + } + } + + /** + * Ensures the well-formdness in terms of assignability on a field. This covers both instance + * fields and static fields. + * + * @param tree the tree to check + */ + private void checkOnlyOneAssignabilityModifierOnField(Tree tree) { + if (tree.getKind() == Kind.VARIABLE) { + VariableTree variableTree = (VariableTree) tree; + VariableElement variableElement = TreeUtils.elementFromDeclaration(variableTree); + if (!PICOTypeUtil.hasOneAndOnlyOneAssignabilityQualifier( + variableElement, atypeFactory)) { + checker.reportError( + variableElement, "assignability.declaration.invalid", variableElement); + isValid = false; + } + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOViewpointAdapter.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOViewpointAdapter.java new file mode 100644 index 00000000000..8c3c4313755 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOViewpointAdapter.java @@ -0,0 +1,56 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; + +import javax.lang.model.element.AnnotationMirror; + +/** A {@link AbstractViewpointAdapter} for the PICO checker. */ +public class PICOViewpointAdapter extends AbstractViewpointAdapter { + /** The PICO type factory. */ + private PICONoInitAnnotatedTypeFactory picoTypeFactory; + + /** + * Create a new {@link PICOViewpointAdapter}. + * + * @param atypeFactory the type factory + */ + public PICOViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + picoTypeFactory = (PICONoInitAnnotatedTypeFactory) atypeFactory; + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + return atm.getAnnotationInHierarchy(picoTypeFactory.READONLY); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (AnnotationUtils.areSame(declaredAnnotation, picoTypeFactory.READONLY)) { + return picoTypeFactory.READONLY; + } else if (AnnotationUtils.areSame(declaredAnnotation, picoTypeFactory.MUTABLE)) { + return picoTypeFactory.MUTABLE; + } else if (AnnotationUtils.areSame(declaredAnnotation, picoTypeFactory.IMMUTABLE)) { + return picoTypeFactory.IMMUTABLE; + } else if (AnnotationUtils.areSame(declaredAnnotation, picoTypeFactory.BOTTOM)) { + return picoTypeFactory.BOTTOM; + } else if (AnnotationUtils.areSame(declaredAnnotation, picoTypeFactory.POLY_MUTABLE)) { + return picoTypeFactory.POLY_MUTABLE; + } else if (AnnotationUtils.areSame( + declaredAnnotation, picoTypeFactory.RECEIVER_DEPENDENT_MUTABLE)) { + // @Readonly |> @ReceiverDependentMutable = @Lost + if (AnnotationUtils.areSame(receiverAnnotation, picoTypeFactory.READONLY)) { + return picoTypeFactory.LOST; + } else { + return receiverAnnotation; + } + } else { + throw new BugInCF("Unknown declared modifier: " + declaredAnnotation); + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/jdk.astub b/checker/src/main/java/org/checkerframework/checker/pico/jdk.astub new file mode 100644 index 00000000000..cbfdf929bdd --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/jdk.astub @@ -0,0 +1,355 @@ +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ObjectIdentityMethod; +import java.util.Collection; + +package java.lang; + +@ReceiverDependentMutable +class Iterable { + @PolyMutable Iterator iterator(@PolyMutable Iterable this); +} + +class AssertionError { + AssertionError(@Readonly Object var0); +} + +class RuntimeException { + RuntimeException(String var0, Throwable var1); +} + +@ReceiverDependentMutable +class Object { + @ReceiverDependentMutable Object(); + Class getClass(@Readonly Object this); + String toString(@Readonly Object this); + int hashCode(@Readonly Object this); + boolean equals(@Readonly Object this, @Readonly Object var1); + @ReceiverDependentMutable Object clone(@ReceiverDependentMutable Object this); + @ObjectIdentityMethod + final native Class getClass(); +} + +class String { + int length(@Immutable String this); + char charAt(@Immutable String this, int var1); + String replace(@Readonly CharSequence target, @Readonly CharSequence replacement); + boolean contains(@Readonly CharSequence s); + String substring(@Immutable String this, int var1); + String substring(@Immutable String this, int var1, int var2); + String toString(@Immutable String this); + boolean equals(@Immutable Object var1); + boolean contentEquals(@Readonly CharSequence var1); + static String valueOf(@Readonly Object var0); + static String format(String var0, @Readonly Object @Readonly ... var1); + static String format(@Readonly Locale l, String format, @Readonly Object @Readonly ... var1); +} + +class StringBuilder { + StringBuilder append(@Readonly Object var1); +} + +class StringBuffer { + int length(@Readonly StringBuffer this); + int capacity(@Readonly StringBuffer this); + StringBuffer append(@Readonly Object obj); + String substring(@Readonly StringBuffer this, int start); + CharSequence subSequence(@Readonly StringBuffer this, int start, int end); + String substring(@Readonly StringBuffer this, int start, int end); + int indexOf(@Readonly StringBuffer this, String str); + int indexOf(@Readonly StringBuffer this, String str, int fromIndex); + int lastIndexOf(@Readonly StringBuffer this, String str); + int lastIndexOf(@Readonly StringBuffer this, String str, int fromIndex); +} + +@ReceiverDependentMutable +class Throwable { + String getMessage(@ReceiverDependentMutable Throwable this); + String getLocalizedMessage(@ReceiverDependentMutable Throwable this); + Throwable getCause(@ReceiverDependentMutable Throwable this); + void printStackTrace(@ReceiverDependentMutable Throwable this); + void printStackTrace(@ReceiverDependentMutable Throwable this, PrintStream var1); + void printStackTrace(@ReceiverDependentMutable Throwable this, Throwable.PrintStreamOrWriter var1); +} + +@ReceiverDependentMutable +interface CharSequence { + int length(@Readonly CharSequence this); + char charAt(@Readonly CharSequence this, int index); + CharSequence subSequence(@Readonly CharSequence this, int start, int end); + public default IntStream chars(@Readonly CharSequence this); + public default IntStream codePoints(@Readonly CharSequence this); +} + +@ReceiverDependentMutable +class RuntimeException { + @ReceiverDependentMutable RuntimeException(@Readonly Throwable var1); + @ReceiverDependentMutable RuntimeException(String var1, @Readonly Throwable var2, boolean var3, boolean var4); +} + +@ReceiverDependentMutable +class IndexOutOfBoundsException {} + +@Immutable +class Enum> { + @Immutable Enum(String name, int ordinal); + int ordinal(@Immutable Enum this); +} + +@ReceiverDependentMutable +interface Cloneable {} + +@ReceiverDependentMutable +interface Comparable {} + +package java.util; + +@ReceiverDependentMutable +class Collection { + Iterator iterator(); + boolean addAll(@Mutable Collections this, Collection c); + boolean add(@Mutable Collections this, E e); +} + +@ReceiverDependentMutable +class Properties { + @Readonly Object put(@Immutable Object key, @Readonly Object value); +} + +@ReceiverDependentMutable +interface Iterator { + boolean hasNext(@Readonly Iterator this); + @Immutable E next(); +} + +@ReceiverDependentMutable +class Date { + @ReceiverDependentMutable Date(); + @ReceiverDependentMutable Date(long var1); + int getHours(@Readonly Date this); + long getTime(@Readonly Date this); +} + +@ReceiverDependentMutable +interface Collection { + boolean contains(@Readonly Collection this, @Readonly Object o); +} + +@ReceiverDependentMutable +public abstract class AbstractCollection implements Collection { + public abstract int size(@Readonly AbstractCollection this); + public boolean contains(@Readonly Object o); +} + +@ReceiverDependentMutable +class ArrayList { + @ReceiverDependentMutable ArrayList(); + @ReceiverDependentMutable ArrayList(@Readonly Collection var1); + boolean add(@Mutable ArrayList this, E var1); + boolean addAll(@Mutable ArrayList this, @Readonly Collection c); + E get(@Readonly ArrayList this, int index); + int size(@Readonly ArrayList this); + boolean isEmpty(@Readonly ArrayList this); + boolean contains(@Readonly ArrayList this, @Readonly Object o); + int indexOf(@Readonly ArrayList this, @Readonly Object o); + int lastIndexOf(@Readonly ArrayList this, @Readonly Object o); + Iterator iterator(@Readonly ArrayList this); +} + +@ReceiverDependentMutable +interface List { + int size(@Readonly List this); + boolean isEmpty(@Readonly List this); + Iterator iterator(@Readonly List this); + Object[] toArray(@Readonly List this); + T[] toArray(@Readonly List this, T[] a); + boolean containsAll(@Readonly List this, @Readonly Collection c); + E get(@Readonly List this, int index); + boolean contains(@Readonly List this, @Readonly Object o); + boolean remove(@Readonly Object o); + boolean removeAll(@Readonly Collection c); + boolean addAll(@Readonly Collection c); + boolean addAll(int index, @Readonly Collection c); + int indexOf(@Readonly List this, @Readonly Object o); + int lastIndexOf(@Readonly List this, @Readonly Object o); + ListIterator listIterator(@Readonly List this); + ListIterator listIterator(@Readonly List this, int index); +} + +@ReceiverDependentMutable +class AbstractList { + @ReceiverDependentMutable AbstractList(); + void add(@Mutable AbstractList this, int var1, E var2); +} + +@ReceiverDependentMutable +interface Set { + int size(@Readonly Set this); + boolean isEmpty(@Readonly Set this); + boolean contains(@Readonly Set this, @Readonly Object var1); + Iterator iterator(@Readonly Set this); + Object[] toArray(@Readonly Set this); + T[] toArray(@Readonly Set this, T[] a); + boolean containsAll(@Readonly Set this, @Readonly Collection c); + boolean remove(@Readonly Object o); + boolean addAll(@Readonly Collection c); +} + +@ReceiverDependentMutable +class HashSet { + @ReceiverDependentMutable HashSet(); + @ReceiverDependentMutable HashSet(@Readonly Collection var1); + boolean contains(@Readonly HashSet this, @Readonly Object var1); + boolean remove(@Readonly Object var1); +} + +class LinkedHashSet { + LinkedHashSet(@Immutable Collection var0); +} + +@ReceiverDependentMutable +interface Map { + int size(@Readonly Map this); + boolean isEmpty(@Readonly Map this); + boolean containsKey(@Readonly Map this, @Readonly Object var1); + boolean containsValue(@Readonly Map this, @Readonly Object value); + V get(@Readonly Map this, @Immutable Object key); + V remove(@Readonly Object key); + void putAll(@Readonly Map m); + Set keySet(@Readonly Map this); + Collection values(@Readonly Map this); + Set> entrySet(@Readonly Map< K, V> this); +} + +@ReceiverDependentMutable +class HashMap { + @ReceiverDependentMutable HashMap(); + @ReceiverDependentMutable HashMap(@Readonly Map var1); + V get(@Readonly HashMap this, @Readonly Object key); + boolean containsKey(@Readonly HashMap this, @Readonly Object key); + boolean containsValue(@Readonly HashMap this, @Readonly Object value); +} + +class Collections { + static @Immutable List unmodifiableList(@Readonly List list); + static @Immutable List singletonList(@Readonly T var0); + static @Immutable Set singleton(T var0); + @Immutable List emptyList(); +} + +class StringJoiner { + StringJoiner(@Readonly CharSequence delimiter); + StringJoiner(@Readonly CharSequence delimiter, @Readonly CharSequence prefix, @Readonly CharSequence suffix); + StringJoiner add(@Readonly CharSequence newElement); +} + +class Arrays { + static @Immutable List asList(T @Readonly ... var0); + static String toString(int @Readonly [] var0); + static boolean equals(float @Readonly [] var0, float @Readonly [] var1); + static boolean equals(double @Readonly [] var0, double @Readonly [] var1); + static boolean equals(byte @Readonly [] var0, byte @Readonly [] var1); + static T[] copyOf(T @Readonly [] original, int newLength); +} + +class Objects { + static int hashCode(@Readonly Object o); + static boolean equals(@Readonly Object a, @Readonly Object b); +} + +@ReceiverDependentMutable +class Stack { + E peek(@ReceiverDependentMutable Stack this); + boolean empty(@ReceiverDependentMutable Stack this); +} + +@ReceiverDependentMutable +class Vector { + boolean isEmpty(@Readonly Vector this); +} + +@ReceiverDependentMutable +class Hashtable { + V get(@Readonly Hashtable this, @Readonly Object key); + boolean containsKey(@Readonly Hashtable this, @Readonly Object key); +} + +package java.util.logging; +class Logger { + void log(@Readonly Level level, String msg, @Readonly Throwable thrown); +} + +package java.util.regex; +class Pattern { + Matcher matcher(@Readonly CharSequence input); + static boolean matches(String regex, @Readonly CharSequence input); + String[] split(@Readonly CharSequence input, int limit); + String[] split(@Readonly CharSequence input); + static final int countChars(@Readonly CharSequence seq, int index, int lengthInCodePoints); + static final int countCodePoints(@Readonly CharSequence seq); +} + +package java.util.concurrent; +class ExecutionException { + ExecutionException(@Readonly Throwable var0); +} + +package java.io; + +@ReceiverDependentMutable +class PrintStream { + void print(PrintStream this, int var1); + void print(PrintStream this, String var1); + PrintStream printf(PrintStream this, String var1, @Readonly Object @Readonly ... var2); + PrintStream format(String format, @Readonly Object @Readonly ... args); +} + +@ReceiverDependentMutable +class PrintWriter { + PrintWriter printf(@ReceiverDependentMutable PrintWriter this, String var1, @Readonly Object @Readonly ... var2); +} + +@ReceiverDependentMutable +class File { + @ReceiverDependentMutable File(@Readonly File parent, String child); + boolean isFile(@Readonly File this); + String[] list(@Readonly File this); + String getPath(@Readonly File this); + long length(@Readonly File this); + String getName(@Readonly File this); +} + +@ReceiverDependentMutable +class FileInputStream { + @ReceiverDependentMutable FileInputStream(@Readonly File file); +} + +class ObjectOutputStream { + void writeObject(@Readonly Object obj); +} + +@ReceiverDependentMutable +interface Serializable {} + +package java.awt; + +@ReceiverDependentMutable +class Container { + void add(@Readonly Component comp, @Readonly Object constraints); +} + +package javax.lang.model.element; + +interface Name { + boolean contentEquals(@Readonly CharSequence var1); +} + +@ReceiverDependentMutable +interface AnnotationMirror {} + +package javax.lang.model.type; +interface TypeMirror { + @Immutable List getAnnotationMirrors(); +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/messages.properties b/checker/src/main/java/org/checkerframework/checker/pico/messages.properties new file mode 100644 index 00000000000..6272e151f4d --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/messages.properties @@ -0,0 +1,15 @@ +constructor.invocation.invalid=Cannot not instantiate type: %s out of constructor: %s +constructor.return.invalid=Invalid constructor return type: %s +method.receiver.incompatible=Incompatible method receiver: %s with bound of type: %s +class.bound.invalid=Invalid class bound: %s +subclass.bound.incompatible=Incompatible subclass bound: %s +illegal.field.write=Cannot write field via receiver: %s +illegal.array.write=Cannot write array via receiver: %s +static.receiverdependentmutable.forbidden=%s is forbidden in static context +array.new.invalid=Invalid new array type: %s +field.polymutable.forbidden=Field %s cannot be @PolyMutable +assignability.declaration.invalid=Only one assignability qualifier is allowed on %s +object.identity.method.invocation.invalid=Cannot invoke non-object identity method %s from object identity context! +object.identity.field.access.invalid=Object identity context cannot reference non abstract state field %s! +object.identity.static.field.access.forbidden=Object identity context cannot reference static field %s! +implicit.shallow.immutable=Write an explicit mutable qualifier if wants to exclude the field from the abstract state! Otherwise change the class mutability of this object ! diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/PICOImmutabilityTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/PICOImmutabilityTest.java new file mode 100644 index 00000000000..3f6d1723117 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/PICOImmutabilityTest.java @@ -0,0 +1,28 @@ +package org.checkerframework.checker.test.junit; + +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized; + +import java.io.File; +import java.util.List; + +/** JUnit tests for the PICO Checker. */ +public class PICOImmutabilityTest extends CheckerFrameworkPerDirectoryTest { + /** + * Create a PICOImmutabilityTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public PICOImmutabilityTest(List testFiles) { + super(testFiles, org.checkerframework.checker.pico.PICOChecker.class, "pico-immutability"); + } + + /** + * Returns the test files for the PICO Checker. The test files are in the + * "tests/pico-immutability" directory. + */ + @Parameterized.Parameters + public static String[] getTestDirs() { + return new String[] {"pico-immutability"}; + } +} diff --git a/checker/tests/pico-immutability/Arrays.java b/checker/tests/pico-immutability/Arrays.java new file mode 100644 index 00000000000..1fe7c0fdbd0 --- /dev/null +++ b/checker/tests/pico-immutability/Arrays.java @@ -0,0 +1,60 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class Arrays { + Object[] o = new String[] {""}; + + // TODO static array + + void test1(String @Immutable [] array) { + // :: error: (illegal.array.write) + array[0] = "something"; + } + + void test2() { + // :: error: (array.new.invalid) + int[] a = new int @Readonly [] {1, 2}; + } + + void test3(String[] array) { + // :: error: (illegal.array.write) + array[0] = "something"; + } + + void test4(@Immutable String @Mutable [] p) { + Object[] l = p; // By default, array type is @Readonly(local variable); Object class is by + // default @Mutable. So assignment should not typecheck + } + + void test5(@Immutable Integer @Mutable [] p) { + // :: error: (assignment.type.incompatible) + @Mutable Object @Readonly [] l = p; + } + + void test6(double @Readonly [] a1, double @Readonly [] a2) { + java.util.Arrays.equals(a1, a2); + } + + void test7() { + @Readonly Object[] f = new String @Immutable [] {"HELLO"}; + } + + public double @ReceiverDependentMutable [] @Mutable [] test() { + double @ReceiverDependentMutable [] @Mutable [] C = + new double @ReceiverDependentMutable [0] @Mutable [0]; + for (@Immutable int i = 0; i < 0; i++) { + for (@Immutable int j = 0; j < 0; j++) { + // Array C's main modifier is @ReceiverDependentMutable, so mutating C is not + // allowed + // :: error: (illegal.array.write) + C[i] = new double @Mutable [] {1.0}; + // But C[i] is double @Mutable [](mutable array of double elements), so mutating + // C[i] is ALLOWED + C[i][j] = 1.0; + } + } + return C; + } +} diff --git a/checker/tests/pico-immutability/AssignabilityAnnotation.java b/checker/tests/pico-immutability/AssignabilityAnnotation.java new file mode 100644 index 00000000000..6b1cd127f0a --- /dev/null +++ b/checker/tests/pico-immutability/AssignabilityAnnotation.java @@ -0,0 +1,27 @@ +import org.checkerframework.checker.pico.qual.Assignable; +import org.checkerframework.checker.pico.qual.Immutable; + +public class AssignabilityAnnotation { + int a; + @Assignable int b; + final int c; + // :: error: (assignability.declaration.invalid) + final @Assignable int d; + final @Immutable Object io = null; + @Immutable Object io2; + @Assignable @Immutable Object io3; + static final @Immutable Object io4 = null; + static @Assignable @Immutable Object io5; + // :: error: (assignability.declaration.invalid) + final @Assignable @Immutable Object o = null; + // :: error: (assignability.declaration.invalid) + static final @Assignable @Immutable Object o2 = null; + + // Fields are initialized here to prevent initailization errors + AssignabilityAnnotation() { + a = 1; + c = 1; + d = 1; + io2 = new Object(); + } +} diff --git a/checker/tests/pico-immutability/Builder.java b/checker/tests/pico-immutability/Builder.java new file mode 100644 index 00000000000..b715bc55b1f --- /dev/null +++ b/checker/tests/pico-immutability/Builder.java @@ -0,0 +1,252 @@ +import org.checkerframework.checker.pico.qual.Mutable; + +// Example taken from https://webagam.com/pages/2020/05/27/immutable-objects-with-builder-pattern/ +// TODO this seems to be a good exmaple for fix the behavior for the interaction between PICO and +// initialization checker +public class Builder { + public static class NoBuilderEmployee { + private String id; + private String name; + private String department; + private String organization; + private String email; + + public NoBuilderEmployee( + String id, String name, String department, String organization, String email) { + this.id = id; + this.name = name; + this.department = department; + this.organization = organization; + this.email = email; + } + + public String getId() { + return id; + } + + public String getName() { + return name; + } + + public String getDepartment() { + return department; + } + + public String getOrganization() { + return organization; + } + + public String getEmail() { + return email; + } + + public static void main(String args[]) { + String id = "xyz123"; + String name = "user1"; + String department = "HR"; + String organization = "webagam Comp"; + String email = "user1@webagam.com"; + + NoBuilderEmployee emp = + new NoBuilderEmployee(id, name, organization, department, email); + } + } + + public static class InnerClassBuilderEmployee { + private String id; + private String name; + private String department; + private String organization; + private String email; + + private InnerClassBuilderEmployee( + String id, String name, String department, String organization, String email) { + this.id = id; + this.name = name; + this.department = department; + this.organization = organization; + this.email = email; + } + + public String getId() { + return id; + } + + public String getName() { + return name; + } + + public String getDepartment() { + return department; + } + + public String getOrganization() { + return organization; + } + + public String getEmail() { + return email; + } + + public static @Mutable class InnerClassBuilder { + + private String id; + private String name; + private String department; + private String organization; + private String email; + + public InnerClassBuilder withId(String id) { + this.id = id; + return this; + } + + public InnerClassBuilder withName(String name) { + this.name = name; + return this; + } + + public InnerClassBuilder withDepartment(String department) { + this.department = department; + return this; + } + + public InnerClassBuilder withOrganization(String organization) { + this.organization = organization; + return this; + } + + public InnerClassBuilder withEmail(String email) { + this.email = email; + return this; + } + + public InnerClassBuilderEmployee build() { + return new InnerClassBuilderEmployee(id, name, department, organization, email); + } + } + + public static void main(String args[]) { + String id = "xyz123"; + String name = "user1"; + String department = "HR"; + String organization = "webagam Comp"; + String email = "user1@webagam.com"; + InnerClassBuilderEmployee emp = + new InnerClassBuilderEmployee.InnerClassBuilder() + .withId(id) + .withName(name) + .withDepartment(department) + .withOrganization(organization) + .withEmail(email) + .build(); + } + } + + // This kind of builder pattern is not supported and will require the help of uniqueness + // property + public static class ModernBuilderEmployee { + private String id; + private String name; + private String department; + private String organization; + private String email; + + private void setId(String id) { + // :: error: (illegal.field.write) + this.id = id; + } + + private void setName(String name) { + // :: error: (illegal.field.write) + this.name = name; + } + + private void setDepartment(String department) { + // :: error: (illegal.field.write) + this.department = department; + } + + private void setOrganization(String organization) { + // :: error: (illegal.field.write) + this.organization = organization; + } + + private void setEmail(String email) { + // :: error: (illegal.field.write) + this.email = email; + } + + // :: error: (initialization.fields.uninitialized) + private ModernBuilderEmployee() {} + + public String getId() { + return id; + } + + public String getName() { + return name; + } + + public String getDepartment() { + return department; + } + + public String getOrganization() { + return organization; + } + + public String getEmail() { + return email; + } + + public static @Mutable class ModernBuilder { + ModernBuilderEmployee emp = new ModernBuilderEmployee(); + + public ModernBuilder withId(String id) { + emp.setId(id); + return this; + } + + public ModernBuilder withName(String name) { + emp.setName(name); + return this; + } + + public ModernBuilder withDepartment(String department) { + emp.setDepartment(department); + return this; + } + + public ModernBuilder withOrganization(String organization) { + emp.setOrganization(organization); + return this; + } + + public ModernBuilder withEmail(String email) { + emp.setEmail(email); + return this; + } + + public ModernBuilderEmployee build() { + return emp; + } + } + + public static void main(String args[]) { + String id = "xyz123"; + String name = "user1"; + String department = "HR"; + String organization = "webagam Comp"; + String email = "user1@webagam.com"; + ModernBuilderEmployee.ModernBuilder builder = new ModernBuilderEmployee.ModernBuilder(); + ModernBuilderEmployee emp = + builder.withId(id) + .withName(name) + .withDepartment(department) + .withOrganization(organization) + .withEmail(email) + .build(); + } + } +} diff --git a/checker/tests/pico-immutability/CastTest.java b/checker/tests/pico-immutability/CastTest.java new file mode 100644 index 00000000000..7ebfe21bafa --- /dev/null +++ b/checker/tests/pico-immutability/CastTest.java @@ -0,0 +1,24 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; + +public class CastTest { + void foo(Object o) { + // No cast.unsafe + String s1 = (@Immutable String) o; + // No cast.unsafe + String s2 = (String) o; + // :: error: (type.invalid.annotations.on.use) + String s3 = (@Mutable String) o; + } + + @Override + public Object clone() throws CloneNotSupportedException { + CastTest oe = (CastTest) super.clone(); + return oe; + } + + @Override + public String toString() { + return super.toString(); + } +} diff --git a/checker/tests/pico-immutability/ClassAnnotation.java b/checker/tests/pico-immutability/ClassAnnotation.java new file mode 100644 index 00000000000..a481dc6e342 --- /dev/null +++ b/checker/tests/pico-immutability/ClassAnnotation.java @@ -0,0 +1,232 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +/** + * This test case aims to showing the validity of annotation class, type use, inheritance and object + * creation. + */ +/* @Immutable */ +public class ClassAnnotation { + /* @Immutable */ interface ImmutableInterfaceImplict {} + + @Immutable interface ImmutableInterfaceExplict {} + + @Mutable interface MutableInterface {} + + @ReceiverDependentMutable interface RDMInterface {} + + // :: error: class.bound.invalid + @Readonly interface ReadonlyInterface {} + + // :: error: class.bound.invalid + @PolyMutable interface PolyMutableInterface {} + + /* @Immutable */ abstract class ImmutableAbstractClassImplict {} + + @Immutable abstract class ImmutableAbstractClassExplicit {} + + @Mutable abstract class MutableAbstractClass {} + + @ReceiverDependentMutable abstract class RDMAbstractClass {} + + // :: error: class.bound.invalid + @Readonly abstract class ReadonlyAbstractClass {} + + // :: error: class.bound.invalid + @PolyMutable abstract class PolyMutableAbstractClass {} + + /* @Immutable */ class ImmutableClassImplict { + + /* @Immutable */ ImmutableClassImplict() {} + + @Immutable ImmutableClassImplict(int i) {} + + // :: error: (type.invalid.annotations.on.use) + @Mutable ImmutableClassImplict(String str) {} + + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable ImmutableClassImplict(char ch) {} + + // when not annotated explictly, default annotations of is inherited from declaration + void method1(/* @Immutable */ ImmutableClassImplict this) {} + + void method2(@Immutable ImmutableClassImplict this) {} + + // @Immutable + void method3(@Readonly ImmutableClassImplict this) {} + + void method4(@PolyMutable ImmutableClassImplict this) {} + + // :: error: (type.invalid.annotations.on.use) + void method5(@ReceiverDependentMutable ImmutableClassImplict this) {} + + // :: error: (type.invalid.annotations.on.use) + void method6(@Mutable ImmutableClassImplict this) {} + } + + @Immutable class ImmutableClassExplicit {} + + @Mutable class MutableClass { + /* @Mutable */ MutableClass() {} + + // :: error: (type.invalid.annotations.on.use) + @Immutable MutableClass(int i) {} + + @Mutable MutableClass(String str) {} + + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable MutableClass(char ch) {} + + // when not annotated explictly, default annotations of is inherited from declaration + void method1(/* @Mutable */ MutableClass this) {} + + // :: error: (type.invalid.annotations.on.use) + void method2(@Immutable MutableClass this) {} + + void method3(@Readonly MutableClass this) {} + + void method4(@PolyMutable MutableClass this) {} + + // :: error: (type.invalid.annotations.on.use) + void method5(@ReceiverDependentMutable MutableClass this) {} + + void method6(@Mutable MutableClass this) {} + } + + @ReceiverDependentMutable class RDMClass { + /* @RDM */ RDMClass() {} + + @Immutable RDMClass(int i) {} + + @Mutable RDMClass(String str) {} + + @ReceiverDependentMutable RDMClass(char ch) {} + + // when not annotated explictly, default annotations of is inherited from declaration + void method1(/* @RDM */ RDMClass this) {} + + void method2(@Immutable RDMClass this) {} + + void method3(@Readonly RDMClass this) {} + + void method4(@PolyMutable RDMClass this) {} + + void method5(@ReceiverDependentMutable RDMClass this) {} + + void method6(@Mutable RDMClass this) {} + } + + // :: error: class.bound.invalid + @ReceiverDependentMutable static class RDMStaticClass {} + + // :: error: class.bound.invalid + @Readonly class ReadonlyClass {} + + // :: error: class.bound.invalid + @PolyMutable class PolyMutableClass {} + + void testObjectCreation() { + // Default to @Immutable for RDM class constructor without annotation + @Immutable RDMClass rdmClass = new RDMClass(); + @Mutable MutableClass mutableClass = new MutableClass(); + @Immutable ImmutableClassExplicit immutableClassExplicit = new ImmutableClassExplicit(); + new /* @Immutable */ ImmutableClassImplict(); + new @Immutable ImmutableClassImplict(); + // :: error: constructor.invocation.invalid + new @Mutable ImmutableClassImplict(); + new /* @Immutable */ ImmutableClassExplicit(); + new @Immutable ImmutableClassExplicit(); + // :: error: constructor.invocation.invalid + new @Mutable ImmutableClassExplicit(); + new /* @Mutable */ MutableClass(); + // :: error: constructor.invocation.invalid + new @Immutable MutableClass(); + new @Mutable MutableClass(); + @Immutable Object obj = new /* @Immutable */ RDMClass(); + new @Immutable RDMClass(); + new @Mutable RDMClass(); + new @ReceiverDependentMutable RDMClass(); + // Constructor return is @Immutable + new /* @Immutable */ RDMClass(1); + new @Immutable RDMClass(1); + // :: error: constructor.invocation.invalid + new @Mutable RDMClass(1); + // :: error: constructor.invocation.invalid + new @ReceiverDependentMutable RDMClass(1); + // Constructor return is @Mutable + new /* @Mutable */ RDMClass("str"); + new @Mutable RDMClass("str"); + // :: error: constructor.invocation.invalid + new @Immutable RDMClass("str"); + // :: error: constructor.invocation.invalid + new @ReceiverDependentMutable RDMClass("str"); + // Constructor return is @ReceiverDependentMutable + new /* @RDM */ RDMClass('c'); + new @Immutable RDMClass('c'); + new @Mutable RDMClass('c'); + new @ReceiverDependentMutable RDMClass('c'); + // :: error: constructor.invocation.invalid + new @PolyMutable ImmutableClassImplict(); + // :: error: constructor.invocation.invalid + new @Readonly ImmutableClassImplict(); + // :: error: constructor.invocation.invalid + new @PolyMutable ImmutableClassExplicit(); + // :: error: constructor.invocation.invalid + new @Readonly ImmutableClassExplicit(); + // :: error: constructor.invocation.invalid + new @PolyMutable MutableClass(); + // :: error: constructor.invocation.invalid + new @Readonly MutableClass(); + // TODO :: error: constructor.invocation.invalid + new @PolyMutable RDMClass(); + // :: error: constructor.invocation.invalid + new @Readonly RDMClass(); + } + + // Subclassing check + class ImmutableChildClassGood1 extends @ReceiverDependentMutable RDMClass {} + + class ImmutableChildClassGood2 extends ImmutableClassExplicit {} + + class ImmutableChildClassGood3 + implements ImmutableInterfaceExplict, @ReceiverDependentMutable RDMInterface {} + + // TODO Make the superclass's bound implicit works + // :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) + class ImmutableChildClassBad1 extends @Mutable MutableClass {} + + // :: error: (declaration.inconsistent.with.implements.clause) + class ImmutableChildClassBad2 implements @Mutable MutableInterface {} + + @Mutable class MutableChildClassGood1 extends @ReceiverDependentMutable RDMClass {} + + @Mutable class MutableChildClassGood2 extends @Mutable MutableClass {} + + @Mutable class MutableChildClassGood3 + implements @Mutable MutableInterface, @ReceiverDependentMutable RDMInterface {} + + // :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) + @Mutable class MutableChildClassBad1 extends @Immutable ImmutableClassExplicit {} + + // :: error: (declaration.inconsistent.with.implements.clause) + @Mutable class MutableChildClassBad2 implements @Immutable ImmutableInterfaceExplict {} + + @ReceiverDependentMutable class RDMChildClassGood1 extends @ReceiverDependentMutable RDMClass {} + + @ReceiverDependentMutable class RDMChildClassGood2 implements @ReceiverDependentMutable RDMInterface {} + + // :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) + @ReceiverDependentMutable class RDMChildClassBad1 extends @Immutable ImmutableClassExplicit {} + + // :: error: (declaration.inconsistent.with.implements.clause) + @ReceiverDependentMutable class RDMChildClassBad2 implements @Immutable ImmutableInterfaceExplict {} + + // :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) + @ReceiverDependentMutable class RDMChildClassBad3 extends @Mutable MutableClass {} + + // :: error: (declaration.inconsistent.with.implements.clause) + @ReceiverDependentMutable class RDMChildClassBad4 implements @Mutable MutableInterface {} +} diff --git a/checker/tests/pico-immutability/CloneTest.java b/checker/tests/pico-immutability/CloneTest.java new file mode 100644 index 00000000000..6a7f115d126 --- /dev/null +++ b/checker/tests/pico-immutability/CloneTest.java @@ -0,0 +1,95 @@ +// clone() method proposal: +// 1. Let overriding check in type declaration with @Mutable and @Immutable +// bound more flexible. +// In the overriding clone() method in those two type declarations, +// as long as declared receiver and return type are the same as bound, +// overriding check passes. For example, @Mutable class can override clone() +// method as @Mutable Object clone(@Mutable A this) while @Immutable class +// can override to @Immutable Object clone(@Immutable B this). But +// @ReceiverDependentMutable class should keep the exact same signature as that +// in jdk.astub, because both @Mutable and @Immutable might be the client. +// Overriding to either @Mutable or @Immutable may cause existing client to break. + +// 2. clone() method has the same defaulted mechanism as other instance methods +// (Remove the special handling of clone() method) + +// 3. There is still need to specially handle super.clone() invocation, because @Immutable +// object's @RDA @Mutable field and @RDA @Readonly field are not guaranteed to be @Immutable +// so there might be use cases to clone those fields and reassign them to the cloned copy. + +// 3.1 As of method signature of clone() method in terms of initialization qualifiers, +// I would keep method return @Initialized. It's common that overriding method call the constructor +// and returns a new @Initialized cloned copy. Chaning clone() method return to @UnderInitialization +// just for special handling for super invocations doesn't make much sense. +// But this requires us to disable subtype checking of return type in terms of initialization +// hierarchy. + +// ======================== Outdated =======================// +// 3.1 Assigning field in cloned copy is an indication of mutable object. Because +// @Immutable objects can not be modified, so no need to deeply clone it. So let's +// treat reassigning cloned object as sign of @Mutable object, thus don't need special +// handling for super.clone()'s result(i.e. no @UnderInitialization staff for the super +// clone() invocation result). + +// 3.2 @Immutable classes' clone() method should either: 1) directly call new +// instance creation and all the initialization steps are finished after constructor +// returns. This is also consistent with the case where objectsa are finished initialization +// after constructor returns and no furthur modification is allowed outside constructor. +// 2) doesn't override clone() method(by default shallow copies receiver object which +// makes sense) +// ======================== Outdated =======================// +// @skip-test +public class CloneTest { + // @Initialized return type + public Object clone() { + AbstractDistribution copy = + (AbstractDistribution) super.clone(); // returns @UnderInitialization object + // Allow reassigning since copy is @UnderInitialization + if (this.randomGenerator != null) + copy.randomGenerator = (RandomEngine) this.randomGenerator.clone(); + // Disable subtype checking in terms of initialization hierarchy. Since + // @UnderInitialization is not + // subtype of @Initialized + return copy; + } + + public Object clone() { + return new Algebra(property.tolerance()); + } + + public Object clone() { + BooleanArrayList clone = new BooleanArrayList((boolean[]) elements.clone()); + // clone finished being initialized, so later instance method call to mutate the state of + // clone makes clone to be @Mutable. This is different from super.clone() extends + // initialization + // scope + clone.setSizeRaw(size); + return clone; + } + + public Object clone() { + return partFromTo(0, size - 1); + } + + public AbstractShortList partFromTo(int from, int to) { + int length = to - from + 1; + ShortArrayList part = new ShortArrayList(length); + part.addAllOfFromTo(this, from, to); + return part; + } + + public boolean removeAll(CloneProblem other) throws CloneNotSupportedException { + if (true) { + CloneProblem l = (CloneProblem) other.overridenClone(); + // Gets method invocation invalid error + l.foo(); + } + return true; + } + + public Object overridenClone() { + return null; + } + + void foo() {} +} diff --git a/checker/tests/pico-immutability/EnumTest.java b/checker/tests/pico-immutability/EnumTest.java new file mode 100644 index 00000000000..f0bbaa5ae2d --- /dev/null +++ b/checker/tests/pico-immutability/EnumTest.java @@ -0,0 +1,49 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class EnumTest { + enum Kind { + SOME; // Enum constant is also @Immutable + } + + // Shouldn't get warning. Implicitly applied @Immutable + Kind defKind; + // Enum is implicitly @Immutable, so using explicit @Immutable is allowed + @Immutable Kind kind; + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable Kind invalidKind; + // :: error: (type.invalid.annotations.on.use) + @Mutable Kind invalidKind2; + // no error now + @Readonly Kind invalidKind3; + + // :: error: (initialization.fields.uninitialized) + EnumTest() { + // Kind.SOME should be @Immutable + kind = Kind.SOME; + } + + void foo(/*immutable*/ MyEnum e) { + // :: error: (type.invalid.annotations.on.use) + @Mutable MyEnum mutableRef; + @Immutable MyEnum immutableRef = e; + + @Mutable MutableEnum mutEnumMutRef = MutableEnum.M1; + // :: error: (type.invalid.annotations.on.use) + @Immutable MutableEnum mutEnumImmRef; + } + + /*immutable*/ + private static enum MyEnum { + T1, + T2; + } + + @Mutable // TODO Should we issue error here? Do we allow mutable enum? + private static enum MutableEnum { + M1, + M2; + } +} diff --git a/checker/tests/pico-immutability/FactoryPattern.java b/checker/tests/pico-immutability/FactoryPattern.java new file mode 100644 index 00000000000..05a2a6896ff --- /dev/null +++ b/checker/tests/pico-immutability/FactoryPattern.java @@ -0,0 +1,19 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; + +public class FactoryPattern { + public @Immutable FactoryPattern() {} + + @PolyMutable Object createObject(@Readonly FactoryPattern this) { + return new @PolyMutable Object(); + } + + static void test() { + @Immutable FactoryPattern factory = new @Immutable FactoryPattern(); + // Both typecheck in new PICO + @Mutable Object mo = factory.createObject(); + @Immutable Object imo = factory.createObject(); + } +} diff --git a/checker/tests/pico-immutability/Generics.java b/checker/tests/pico-immutability/Generics.java new file mode 100644 index 00000000000..eb4b31215d0 --- /dev/null +++ b/checker/tests/pico-immutability/Generics.java @@ -0,0 +1,79 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +import java.util.Date; + +public class Generics { + @Mutable static class MutableBox {} + + @Immutable static class ImmutableClass { + + // :: error: (implicit.shallow.immutable) + MutableBox implicit = new MutableBox(); + + @Mutable MutableBox explicit = new MutableBox(); + } + + @Immutable static class ImmutableGenericEx { + + T t; + + @Immutable ImmutableGenericEx(T t) { + this.t = t; + } + } + + @Immutable static class ImmutableGenericIm { + // :: error: (implicit.shallow.immutable) + T t; // RDA + + @Immutable ImmutableGenericIm(T t) { + this.t = t; + } + } + + void test() { + @Immutable ImmutableGenericIm t = new ImmutableGenericIm(new MutableBox()); + // :: error: (illegal.field.write) + t.t = new MutableBox(); + } + + @Immutable class Wrapper { + T t; + + @Immutable Wrapper(T t) { + this.t = t; + } + } + + void test1() { + @Mutable Object arg = new @Mutable Object(); + @Immutable Wrapper<@Mutable Object> wrapper = new @Immutable Wrapper<@Mutable Object>(arg); + /*Since t is not in the abstract state, we can get a mutable object out of an immutable + object. This is just like we have mutable elements in immutable list, those mutable + elements are not in the abstract state of the list*/ + @Mutable Object mo = wrapper.t; + } + + void test2() { + @Mutable Date md = new @Mutable Date(); + @Readonly Date spy = md; + @Immutable Wrapper<@Readonly Date> victim = new @Immutable Wrapper<@Readonly Date>(spy); + /*Same argument as above*/ + md.setTime(123L); + } + + interface MIt { + E next(); + } + + void raw() { + @Mutable MIt raw = null; + + // Using optimictic uninferred type arguments, so it is + // allowed + // :: error: (assignment.type.incompatible) + @Immutable Object ro = raw.next(); + } +} diff --git a/checker/tests/pico-immutability/HashCodeSafetyExample.java b/checker/tests/pico-immutability/HashCodeSafetyExample.java new file mode 100644 index 00000000000..38bb611dd78 --- /dev/null +++ b/checker/tests/pico-immutability/HashCodeSafetyExample.java @@ -0,0 +1,42 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; + +import java.util.HashMap; +import java.util.Map; + +public class HashCodeSafetyExample { + public static void main(String[] args) { + A a = new A(); + HashMap m = new @Mutable HashMap<>(); + m.put(a, "hello"); + System.out.println("HashCode before: " + a.hashCode()); + // :: error: (illegal.field.write) + a.isIn = true; + System.out.println("HashCode after: " + a.hashCode()); + System.out.println(m.get(a)); + m.put(new A(), "WORLD"); + System.out.println("Iterating entries:"); + // Even though using object a whose hashcode is mutated returns null, + // iterating over entryset did return correct mapping between keys and values, + // which is strange and looks like inconsistency. + for (Map.Entry entry : m.entrySet()) { + System.out.println("key: " + entry.getKey()); + System.out.println("value: " + entry.getValue()); + } + } +} + +@Immutable class A { + boolean isIn = false; + + @Override + public int hashCode() { + return isIn ? 1 : 0; + } + + @Override + public boolean equals(Object obj) { + // No cast.unsafe + return isIn == ((A) obj).isIn; + } +} diff --git a/checker/tests/pico-immutability/ImmutableClass.java b/checker/tests/pico-immutability/ImmutableClass.java new file mode 100644 index 00000000000..8ec3e828466 --- /dev/null +++ b/checker/tests/pico-immutability/ImmutableClass.java @@ -0,0 +1,75 @@ +import org.checkerframework.checker.pico.qual.Assignable; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class ImmutableClass { + + @Readonly Object readonlyField; + @ReceiverDependentMutable Object rdmField; + @Immutable Object immutableField; + + @Immutable ImmutableClass(@Immutable Object immutableObject) { + this.readonlyField = immutableObject; + this.rdmField = immutableObject; + this.immutableField = immutableObject; + } + + // ok + @Immutable class ImmutableClass2 { + @Immutable ImmutableClass2() {} + } + + // ok + @Immutable class ImmutableClass3 { + @Immutable ImmutableClass3() {} + } + + // ok + @Immutable class ImmutableClass4 { + @Immutable ImmutableClass4() {} + } + + // ok + @Immutable class ImmutableClass5 { + @Immutable ImmutableClass5() {} + } + + @Immutable class ImmutableClass6 { + @Immutable ImmutableClass6() {} + } + + @Immutable class ImmutableClass7 { + @Immutable ImmutableClass7() {} + + // Should NOT have warnings for type parameter with non-immutable upper bound + // if the type parameter is declared on generic method(?) + S foo(@Immutable ImmutableClass7 this) { + return null; + } + } + + @Immutable class A { + @Assignable T t; + + @Immutable A(T t) { + this.t = t; + } + } + + @Immutable class ImmutableClass8 extends A<@Mutable Object> { + @Immutable ImmutableClass8() { + super(new @Mutable Object()); + } + + void foo(@Immutable ImmutableClass8 this) { + /*This is acceptable. t is not in the abstract state of + the entire object because T has upper bound @Readonly*/ + @Mutable Object mo = this.t; + // Be default, we can't assign to t; But with the assignability dimension, + // we can do that now by annotating @Assignable to t + this.t = new @Mutable Object(); + } + } +} diff --git a/checker/tests/pico-immutability/ImmutableList.java b/checker/tests/pico-immutability/ImmutableList.java new file mode 100644 index 00000000000..7a48437ee96 --- /dev/null +++ b/checker/tests/pico-immutability/ImmutableList.java @@ -0,0 +1,58 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +// The situations of creating immutable lists, sets, hashmaps are similar. +// If they are called add/put operations, then they can't be immutable. So, +// it's important to initialize their contents when calling constructors. +// One general solution is to create local mutable lists, sets or hashmaps, +// add contents into them and pass it to a wrapper object that is immutable. +// See ImmutableListProblem(Object o1, Object o2, Object o3) for example. +@Immutable public class ImmutableList { + + List list; + + @Immutable ImmutableList() { + list = new @Immutable ArrayList(); + // :: error: (method.invocation.invalid) + list.add("hi"); // Any add() operation after list is constructed forbids the list to be + // immutable + } + + @Immutable ImmutableList(Object o1) { + // One way to construct and immutable list is to pass the contents to the constructor + list = new @Immutable ArrayList(Arrays.asList("hi")); + } + + @Immutable ImmutableList(Object o1, Object o2) { + // Another way is to use Arrays.asList() + list = Arrays.asList("hi"); + } + + @Immutable ImmutableList(Object o1, Object o2, Object o3) { + List localList = new @Mutable ArrayList(); + localList.add("hi"); + localList.add("how"); + localList.add("are"); + localList.add("you"); + // Third way is to create a local mutable list, and wrap it with the immutable list but has + // the same content as the mutable list + list = new @Immutable ArrayList(localList); + } + + @Immutable List createImmutableList(@Readonly ImmutableList this) { + List localList = new @Mutable ArrayList(); + localList.add("hi"); + localList.add("how"); + localList.add("are"); + localList.add("you"); + // After initializing, forcably cast @Mutable list into @Immutable as long as no @Mutable + // aliases exist + // :: warning: (cast.unsafe) + return (@Immutable List) localList; + } +} diff --git a/checker/tests/pico-immutability/ImplicitMutable.java b/checker/tests/pico-immutability/ImplicitMutable.java new file mode 100644 index 00000000000..58cae31e3cb --- /dev/null +++ b/checker/tests/pico-immutability/ImplicitMutable.java @@ -0,0 +1,43 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +/** + * This test checks that PICO issues error for implicit mutable fields in @Immutable and @RDM class. + */ +public class ImplicitMutable { + @Mutable class MutableClass {} + + @Immutable class ExplicitImmutableClass { + // :: error: (implicit.shallow.immutable) + MutableClass implicitMutableField; + @Mutable MutableClass explicitMutableField; + + ExplicitImmutableClass() { + implicitMutableField = new MutableClass(); + explicitMutableField = new MutableClass(); + } + } + + class ImplicitImmutableClass { + // :: error: (implicit.shallow.immutable) + MutableClass implicitMutableField; + @Mutable MutableClass explicitMutableField; + + ImplicitImmutableClass() { + implicitMutableField = new MutableClass(); + explicitMutableField = new MutableClass(); + } + } + + @ReceiverDependentMutable class RDMClass { + // :: error: (implicit.shallow.immutable) + MutableClass implicitMutableField; + @Mutable MutableClass explicitMutableField; + + RDMClass() { + implicitMutableField = new MutableClass(); + explicitMutableField = new MutableClass(); + } + } +} diff --git a/checker/tests/pico-immutability/LocalVariableRefinement.java b/checker/tests/pico-immutability/LocalVariableRefinement.java new file mode 100644 index 00000000000..7dd82e82ac1 --- /dev/null +++ b/checker/tests/pico-immutability/LocalVariableRefinement.java @@ -0,0 +1,42 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +public class LocalVariableRefinement { + static class Acceptor { + static void accept1(@Mutable Object o) {} + + static void accept2(@Immutable Object o) {} + } + + void test1() { + // Should we allow propagation of @Bottom towards declared type? + // We should, otherwise, refined type is always top(lub with top is top) + @Readonly Object rowNames = null; + // TODO Should we give warning here because of refined @Bottom? It will warn if we enforce + // forbidding @Bottom in Validator => We don't warn @Bottom anymore, it's internal qualifier + // now, and internal usage is always valid + Acceptor.accept1(rowNames); + Acceptor.accept2(rowNames); + } + + void test2() { + String s = null; + Acceptor.accept1(s); + Acceptor.accept2(s); + } + + void test3(@Readonly Object o) { + @Readonly Object lo = o; + // :: error: (argument.type.incompatible) + Acceptor.accept1(lo); + // :: error: (argument.type.incompatible) + Acceptor.accept2(lo); + } + + // TODO revisit this method + void foo() { + @Readonly Object o = new @Immutable Object(); + o = new @Mutable Object(); + } +} diff --git a/checker/tests/pico-immutability/ObjectMethods.java b/checker/tests/pico-immutability/ObjectMethods.java new file mode 100644 index 00000000000..346566c5b82 --- /dev/null +++ b/checker/tests/pico-immutability/ObjectMethods.java @@ -0,0 +1,156 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class ObjectMethods { + // Don't have any warnings now + @Override + public int hashCode() { + return super.hashCode(); + } + + @Override + public boolean equals(Object o) { + return super.equals(o); + } + + @Override + protected Object clone() throws CloneNotSupportedException { + return super.clone(); + } + + @Override + public String toString() { + return super.toString(); + } +} + +@Immutable class ObjectMethods2 { + + @Immutable ObjectMethods2() {} + + @Override + public int hashCode() { + return super.hashCode(); + } + + @Override + public boolean equals(Object o) { + return super.equals(o); + } + + @Override + protected @Immutable Object clone(@Immutable ObjectMethods2 this) + throws CloneNotSupportedException { + return super.clone(); + } + + @Override + public String toString() { + return super.toString(); + } +} + +@ReceiverDependentMutable class ObjectMethods3 { + + @ReceiverDependentMutable ObjectMethods3() {} + + @Override + public int hashCode() { + return super.hashCode(); + } + + @Override + public boolean equals(Object o) { + return super.equals(o); + } + + @Override + protected @ReceiverDependentMutable Object clone(@ReceiverDependentMutable ObjectMethods3 this) + throws CloneNotSupportedException { + return super.clone(); + } + + @Override + public String toString() { + return super.toString(); + } +} + +class ObjectMethods4 { + @Override + public int hashCode(@Readonly ObjectMethods4 this) { + return super.hashCode(); + } + + @Override + public boolean equals(@Readonly ObjectMethods4 this, @Readonly Object o) { + return super.equals(o); + } + + @Override + protected Object clone(@Readonly ObjectMethods4 this) throws CloneNotSupportedException { + // :: error: (method.invocation.invalid) :: error: (return.type.incompatible) + return super.clone(); + } + + @Override + public String toString(@Readonly ObjectMethods4 this) { + return super.toString(); + } +} + +@Immutable class ObjectMethods5 { + + @Immutable ObjectMethods5() {} + + @Override + public int hashCode(@Readonly ObjectMethods5 this) { + return super.hashCode(); + } + + @Override + public boolean equals(@Readonly ObjectMethods5 this, @Readonly Object o) { + return super.equals(o); + } + + @Override + protected @Immutable Object clone(@Readonly ObjectMethods5 this) + throws CloneNotSupportedException { + // :: warning: (cast.unsafe) :: error: (method.invocation.invalid) + return (@Immutable Object) super.clone(); + } + + @Override + public String toString(@Readonly ObjectMethods5 this) { + return super.toString(); + } +} + +@ReceiverDependentMutable class ObjectMethods6 { + + @Immutable ObjectMethods6() {} + + @Override + public int hashCode(@Readonly ObjectMethods6 this) { + return super.hashCode(); + } + + @Override + public boolean equals(@Readonly ObjectMethods6 this, @Readonly Object o) { + return super.equals(o); + } + + @Override + protected @ReceiverDependentMutable Object clone(@Readonly ObjectMethods6 this) + throws CloneNotSupportedException { + // No cast.unsafe + // :: error: (method.invocation.invalid) + return (@ReceiverDependentMutable Object) super.clone(); + } + + @Override + public String toString(@Readonly ObjectMethods6 this) { + return super.toString(); + } +} diff --git a/checker/tests/pico-immutability/Operators.java b/checker/tests/pico-immutability/Operators.java new file mode 100644 index 00000000000..0bca77f737c --- /dev/null +++ b/checker/tests/pico-immutability/Operators.java @@ -0,0 +1,56 @@ +import org.checkerframework.checker.pico.qual.Readonly; + +// I am not sure why this test case exist previous but adding here first. +public class Operators { + // :: error: (initialization.field.uninitialized) + @Readonly Object o; + + String testBinaryOperator() { + return "Object is: " + o; + } + + void testUnaryOperator() { + int result = +1; + int a = result--; + int b = result++; + result = -result; + System.out.println(result); + boolean success = false; + System.out.println(success); + Integer i = 0; + i += 2; + } + + class A { + int size() { + return 0; + } + } + + void foo(A a) { + double mean1 = mean(a); + } + + static double mean(A a) { + return sum(a) / a.size(); + } + + static double sum(A a) { + return 1.0; + } + + class UnaryAndCompoundAssignment { + + int counter = 0; + + public void next(@Readonly UnaryAndCompoundAssignment this) { + int lcouter = 0; + lcouter++; + // :: error: (illegal.field.write) + counter++; + lcouter += 5; + // :: error: (illegal.field.write) + counter += 5; + } + } +} diff --git a/checker/tests/pico-immutability/OverrideEquals.java b/checker/tests/pico-immutability/OverrideEquals.java new file mode 100644 index 00000000000..bb9c7d730d3 --- /dev/null +++ b/checker/tests/pico-immutability/OverrideEquals.java @@ -0,0 +1,50 @@ +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +public class OverrideEquals { + class OverrideEqualsInner extends A { + @Override + void foo(@Readonly Object o) {} + + @Override + public boolean equals(Object o) { + return super.equals(o); + } + + @Override + public Object clone() { + try { + return super.clone(); + } catch (CloneNotSupportedException exc) { + throw new InternalError(); // should never happen since we are cloneable + } + } + } + + class SubOverrideEquals extends OverrideEquals { + @Override + public boolean equals(@Readonly Object o) { + return super.equals(new @Mutable Object()); + } + } + + class ThrowableOverridingError extends Throwable { + + @Override + public String getMessage() { + return super.getMessage(); + } + } + + class Test extends Throwable { + @Override + public String getMessage(@Readonly Test this) { + // :: error: (method.invocation.invalid) + return super.getMessage(); + } + } + + class A { + void foo(@Readonly Object o) {} + } +} diff --git a/checker/tests/pico-immutability/PICOInitialization.java b/checker/tests/pico-immutability/PICOInitialization.java new file mode 100644 index 00000000000..a3945f7be47 --- /dev/null +++ b/checker/tests/pico-immutability/PICOInitialization.java @@ -0,0 +1,118 @@ +import org.checkerframework.checker.pico.qual.Assignable; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +// Initialization check only applies to possible non-assignable field, i.e. field in @RDM and +// @Immutable class without explict @Assignable annotation. Javac will handle final field +// initialization. +public class PICOInitialization { + + @ReceiverDependentMutable class RDMClassInitialized { + final @Immutable Object f1; + @Immutable Object f2; + final @ReceiverDependentMutable Object f3; + @ReceiverDependentMutable Object f4; + + @Mutable Object f5; + @Readonly Object f6; + @Assignable @Immutable Object f7; + @Assignable @ReceiverDependentMutable Object f8; + @Assignable @Mutable Object f9; + @Assignable @Readonly Object f10; + + @ReceiverDependentMutable RDMClassInitialized() { + f1 = new @Immutable Object(); + f2 = new @Immutable Object(); + f3 = new @ReceiverDependentMutable Object(); + f4 = new @ReceiverDependentMutable Object(); + f5 = new @Mutable Object(); + f6 = new @Immutable Object(); + } + } + + @ReceiverDependentMutable class RDMClassUninitalized { + final @Immutable Object f1; + @Immutable Object f2; + final @ReceiverDependentMutable Object f3; + @ReceiverDependentMutable Object f4; + + @Mutable Object f5; + @Readonly Object f6; + @Assignable @Immutable Object f7; + @Assignable @ReceiverDependentMutable Object f8; + @Assignable @Mutable Object f9; + @Assignable @Readonly Object f10; + + // :: error: (initialization.fields.uninitialized) + @ReceiverDependentMutable RDMClassUninitalized() { + f1 = new @Immutable Object(); + f2 = new @Immutable Object(); + f3 = new @ReceiverDependentMutable Object(); + } + } + + @Immutable class ImmutableClassInitialized { + final @Immutable Object f1; + @Immutable Object f2; + final @ReceiverDependentMutable Object f3; + @ReceiverDependentMutable Object f4; + + @Mutable Object f5; + @Readonly Object f6; + @Assignable @Immutable Object f7; + @Assignable @ReceiverDependentMutable Object f8; + @Assignable @Mutable Object f9; + @Assignable @Readonly Object f10; + + @Immutable ImmutableClassInitialized() { + f1 = new @Immutable Object(); + f2 = new @Immutable Object(); + f3 = new @Immutable Object(); + f4 = new @Immutable Object(); + f5 = new @Mutable Object(); + f6 = new @Immutable Object(); + } + } + + @Immutable class ImmutableClassUninitalized { + final @Immutable Object f1; + @Immutable Object f2; + final @ReceiverDependentMutable Object f3; + @ReceiverDependentMutable Object f4; + + @Mutable Object f5; + @Readonly Object f6; + @Assignable @Immutable Object f7; + @Assignable @ReceiverDependentMutable Object f8; + @Assignable @Mutable Object f9; + @Assignable @Readonly Object f10; + + // :: error: (initialization.fields.uninitialized) + @Immutable ImmutableClassUninitalized() { + f1 = new @Immutable Object(); + f2 = new @Immutable Object(); + f3 = new @Immutable Object(); + } + } + + @Mutable class MutableClassAssignableNoCheck { + final @Immutable Object f1; + @Immutable Object f2; + final @ReceiverDependentMutable Object f3; + @ReceiverDependentMutable Object f4; + + @Mutable Object f5; + @Readonly Object f6; + @Assignable @Immutable Object f7; + @Assignable @ReceiverDependentMutable Object f8; + @Assignable @Mutable Object f9; + @Assignable @Readonly Object f10; + + @Mutable MutableClassAssignableNoCheck() { + f1 = new @Immutable Object(); + f3 = new @Mutable Object(); + } + } +} diff --git a/checker/tests/pico-immutability/PICOTypeUseLocation.java b/checker/tests/pico-immutability/PICOTypeUseLocation.java new file mode 100644 index 00000000000..78ed77ad440 --- /dev/null +++ b/checker/tests/pico-immutability/PICOTypeUseLocation.java @@ -0,0 +1,36 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class PICOTypeUseLocation { + // :: error: (type.invalid.conflicting.annos) + @Readonly @Immutable Object field; + // :: error: (type.invalid.conflicting.annos) + String @Readonly @Immutable [] array; + // In the abstract state + int implicitImmutableInt; + @Immutable int validInt; + // If you want to exclude primitive(including boxed primitive) and String from + // abstract state, use @Readonly to do this, but not @Mutable, because they can't + // be mutated conceptually. + // :: error: (type.invalid.annotations.on.use) + @Readonly int implicitOverridenInt; + // :: error: (type.invalid.annotations.on.use) + @Mutable int invalidInt; + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable int invalidInt2; + + // :: error: (initialization.fields.uninitialized) + PICOTypeUseLocation() {} + + // :: error: (type.invalid.annotations.on.location) :: error: (invalid.polymorphic.qualifier) + class PICOTypeUseLocationFail<@PolyMutable T, S extends @PolyMutable Object> { + // :: error: (type.invalid.annotations.on.location) :: error: (constructor.return.invalid) + @PolyMutable PICOTypeUseLocationFail() {} + + // :: error: (super.invocation.invalid) :: error: (constructor.return.invalid) + @Readonly PICOTypeUseLocationFail(int a) {} + } +} diff --git a/checker/tests/pico-immutability/PolyMutableTest.java b/checker/tests/pico-immutability/PolyMutableTest.java new file mode 100644 index 00000000000..92845c5a040 --- /dev/null +++ b/checker/tests/pico-immutability/PolyMutableTest.java @@ -0,0 +1,132 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class PolyMutableTest { + @Mutable private static class MutableClass { + int field = 0; + } + + @ReceiverDependentMutable private class RDMHolder { + + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable MutableClass field = new MutableClass(); + @Mutable MutableClass mutableField = new MutableClass(); + + public @PolyMutable MutableClass getField(@PolyMutable RDMHolder this) { + return field; + } + + public void setField(@Mutable RDMHolder this, MutableClass field) { + this.field = field; + } + + void asImmutable(@Immutable RDMHolder r) { + // :: error: (illegal.field.write) + r.field.field = 1; + // :: error: (illegal.field.write) + r.getField().field = 1; + // :: error: (method.invocation.invalid) + r.setField(new MutableClass()); + } + } + + @Immutable private static class ImmutableHolder { + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependentMutable MutableClass field = new MutableClass(); + + public @PolyMutable MutableClass getField(@PolyMutable ImmutableHolder this) { + return field; + } + } + + void foo(A a) { + // Having parentheis here causes StackOverFlowError + // It causes ((MemberSelectTree) methodInvocation.getMethodSelect()).getExpression() + // in TypeArgInferenceUtil to return a ParenthesizedTree instead of MethodInvocationTree + (a.subtract()).multiply(); + } + + class A { + A subtract() { + return this; + } + + A multiply() { + return this; + } + + @ReceiverDependentMutable Object read(@Readonly A this, @PolyMutable Object p) { + return new @ReceiverDependentMutable Object(); + } + } + + @PolyMutable Object bar(@PolyMutable A a) { + // Typecheck now. Only when the declared type is @PolyMutable, after viewpoint adadptation, + // it becomes @SubsitutablePolyMutable, and then will be resolved by QualifierPolymorphism + // Note: viewpoint adaptation(ATF) happens before QualfierPolymorphism(GATF) in current + // implementation + @PolyMutable Object result = a.read(new @Immutable Object()); + return result; + } + + @ReceiverDependentMutable class B { + @PolyMutable B getObject(@Mutable B this) { + return null; + } + + @PolyMutable B getSecondObject(@PolyMutable B this) { + return null; + } + + @PolyMutable B getThirdObject(@Mutable B this) { + return null; + } + + @Immutable B getForthObject(@Mutable B this) { + return this.getThirdObject(); + } + + void test1(@Mutable B mb) { + @Mutable Object l = mb.getObject(); + @Immutable Object r = mb.getObject(); + } + + void test2(@Mutable B mb) { + @Mutable Object l = mb.getSecondObject(); + // TODO Should be poly.invocation.error something... + // :: error: (assignment.type.incompatible) + @Immutable Object r = mb.getSecondObject(); + } + + void test3(@Immutable B imb) { + // TODO Should be poly.invocation.error something... + // :: error: (assignment.type.incompatible) + @Mutable Object l = imb.getSecondObject(); + @Immutable Object r = imb.getSecondObject(); + } + + void test4(@Mutable B b) { + // This correctly typechecks + @Immutable Object r = b.getObject().getThirdObject(); + } + + // TODO Poly return type used on poly receiver. This is not yet implemented yet in CF + void test5(@Mutable B b) { + // TODO Should typecheck. + // :: error: (assignment.type.incompatible) + @Immutable Object r = b.getSecondObject().getSecondObject(); + } + } + + class PolyMutableOnConstructorParameters { + @Immutable PolyMutableOnConstructorParameters(@PolyMutable Object o) {} + + void test(String[] args) { + @Immutable PolyMutableOnConstructorParameters o1 = + new @Immutable PolyMutableOnConstructorParameters(new @Immutable Object()); + } + } +} diff --git a/checker/tests/pico-immutability/RDMClass.java b/checker/tests/pico-immutability/RDMClass.java new file mode 100644 index 00000000000..9e1b8b31e50 --- /dev/null +++ b/checker/tests/pico-immutability/RDMClass.java @@ -0,0 +1,36 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +@ReceiverDependentMutable public class RDMClass { + @ReceiverDependentMutable RDMClass() {} + + @Immutable RDMClass(int dummy) {} + + @Mutable RDMClass(boolean dummy) {} + + void RDMMethod(@ReceiverDependentMutable RDMClass this) {} + + void ImmutableMethod(@Immutable RDMClass this) {} + + void MutableMethod(@Mutable RDMClass this) {} + + void testMethodInvocation() { + RDMClass immutInstance1 = new @Immutable RDMClass(); + RDMClass immutInstance2 = new @Immutable RDMClass(1); + // :: error: (constructor.invocation.invalid) + RDMClass immutInstance3 = new @Immutable RDMClass(true); + RDMClass mutInstance1 = new @Mutable RDMClass(); + // :: error: (constructor.invocation.invalid) + RDMClass mutInstance2 = new @Mutable RDMClass(1); + RDMClass mutInstance3 = new @Mutable RDMClass(true); + immutInstance1.ImmutableMethod(); + // :: error: (method.invocation.invalid) + immutInstance1.MutableMethod(); + immutInstance1.RDMMethod(); + // :: error: (method.invocation.invalid) + mutInstance1.ImmutableMethod(); + mutInstance1.MutableMethod(); + mutInstance1.RDMMethod(); + } +} diff --git a/checker/tests/pico-immutability/RDMClassConstructor.java b/checker/tests/pico-immutability/RDMClassConstructor.java new file mode 100644 index 00000000000..7d3f859adf6 --- /dev/null +++ b/checker/tests/pico-immutability/RDMClassConstructor.java @@ -0,0 +1,64 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public @ReceiverDependentMutable class RDMClassConstructor { + + @Readonly Object readonlyField; + @ReceiverDependentMutable Object rdmField; + @Immutable Object immutableField; + + // :: error: (initialization.fields.uninitialized) + @ReceiverDependentMutable RDMClassConstructor( + @Mutable Object mutableObject, + @ReceiverDependentMutable Object rdmObject, + @Immutable Object immutableObject) {} + + @ReceiverDependentMutable RDMClassConstructor( + @ReceiverDependentMutable Object rdmObject, @Immutable Object immutableObject) { + this.readonlyField = rdmObject; + this.readonlyField = immutableObject; + + this.rdmField = rdmObject; + // :: error: (assignment.type.incompatible) + this.rdmField = immutableObject; + + // :: error: (assignment.type.incompatible) + this.immutableField = rdmObject; + this.immutableField = immutableObject; + } + + void invokeConstructor( + @Readonly Object readonlyObejct, + @Mutable Object mutableObject, + @ReceiverDependentMutable Object rdmObject, + @Immutable Object immutableObject) { + new @Mutable RDMClassConstructor(mutableObject, immutableObject); + // :: error: (argument.type.incompatible) + new @Mutable RDMClassConstructor(readonlyObejct, immutableObject); + // :: error: (argument.type.incompatible) + new @Mutable RDMClassConstructor(rdmObject, immutableObject); + // :: error: (argument.type.incompatible) + new @Mutable RDMClassConstructor(immutableObject, immutableObject); + + new @ReceiverDependentMutable RDMClassConstructor(rdmObject, immutableObject); + // :: error: (argument.type.incompatible) + new @ReceiverDependentMutable RDMClassConstructor(readonlyObejct, immutableObject); + // :: error: (argument.type.incompatible) + new @ReceiverDependentMutable RDMClassConstructor(mutableObject, immutableObject); + // :: error: (argument.type.incompatible) + new @ReceiverDependentMutable RDMClassConstructor(immutableObject, immutableObject); + + new @Immutable RDMClassConstructor(immutableObject, immutableObject); + // :: error: (argument.type.incompatible) + new @Immutable RDMClassConstructor(readonlyObejct, immutableObject); + // :: error: (argument.type.incompatible) + new @Immutable RDMClassConstructor(mutableObject, immutableObject); + // :: error: (argument.type.incompatible) + new @Immutable RDMClassConstructor(rdmObject, immutableObject); + + // :: error: (argument.type.incompatible) :: error: (constructor.invocation.invalid) + new @Readonly RDMClassConstructor(readonlyObejct, immutableObject); + } +} diff --git a/checker/tests/pico-immutability/RDMClassUse.java b/checker/tests/pico-immutability/RDMClassUse.java new file mode 100644 index 00000000000..30079eec6bb --- /dev/null +++ b/checker/tests/pico-immutability/RDMClassUse.java @@ -0,0 +1,75 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +import java.util.ArrayList; + +public class RDMClassUse { + @ReceiverDependentMutable class Person { + + protected String name; + protected int age; + protected @ReceiverDependentMutable ArrayList friends; + + public @ReceiverDependentMutable Person( + String name, int age, @ReceiverDependentMutable ArrayList friends) { + this.name = name; + this.age = age; + this.friends = friends; + } + + public String getName(@Readonly Person this) { + return name; + } + + public void setName(@Mutable Person this, String newName) { + name = newName; + } + + public int getAge(@Readonly Person this) { + return age; + } + + public @ReceiverDependentMutable ArrayList getFriends( + @ReceiverDependentMutable Person this) { + return friends; + } + } + + void testImmutability() { + String name = "tamier"; + int age = 24; + @Immutable ArrayList friends = new @Immutable ArrayList(); + @Immutable Person p = new @Immutable Person(name, age, friends); + String newName = "newName"; + // :: error: (method.invocation.invalid) + p.setName(newName); + // :: error: (method.invocation.invalid) + p.friends.add("newFriend"); + // :: error: (method.invocation.invalid) + p.getFriends().add("newFriend"); + // :: error: (illegal.field.write) + p.name = newName; + // :: error: (illegal.field.write) + p.age = 27; + } + + void testMutability() { + String name = "tamier"; + int age = 24; + @Mutable ArrayList friends = new @Mutable ArrayList(); + @Mutable Person p = new @Mutable Person(name, age, friends); + String newName = "newName"; + // Allow because p is @Mutable + p.setName(newName); + // Allow because p is @Mutable + p.friends.add("newFriend"); + // Allow because p is @Mutable + p.getFriends().add("newFriend"); + // Allow because p is @Mutable + p.name = newName; + // Allow because p is @Mutable + p.age = 27; + } +} diff --git a/checker/tests/pico-immutability/RGB.java b/checker/tests/pico-immutability/RGB.java new file mode 100644 index 00000000000..b844e4d7b17 --- /dev/null +++ b/checker/tests/pico-immutability/RGB.java @@ -0,0 +1,76 @@ +import org.checkerframework.checker.initialization.qual.UnknownInitialization; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +// Inspire by: https://docs.oracle.com/javase/tutorial/essential/concurrency/imstrat.html +// Allow both mutable and immutable instance creation +// Allow having getters and setters, don't need to remove them +// fields don't need to be declared with "final" +// Don't need defensive copy(even though not applicable in this example) +// Aosen: I don't think this test adding much interest aspect of PICO rules, we can remove this if +// desired. +@ReceiverDependentMutable public class RGB { + + // Values must be between 0 and 255. + private int red; + private int green; + private int blue; + private String name; + + private void check(@UnknownInitialization @Readonly RGB this, int red, int green, int blue) { + if (red < 0 || red > 255 || green < 0 || green > 255 || blue < 0 || blue > 255) { + throw new IllegalArgumentException(); + } + } + + public RGB(int red, int green, int blue, String name) { + check(red, green, blue); + this.red = red; + this.green = green; + this.blue = blue; + this.name = name; + } + + public void set(@Mutable RGB this, int red, int green, int blue, String name) { + check(red, green, blue); + synchronized (this) { + this.red = red; + this.green = green; + this.blue = blue; + this.name = name; + } + } + + public synchronized int getRGB(@Readonly RGB this) { + return ((red << 16) | (green << 8) | blue); + } + + public synchronized String getName(@Readonly RGB this) { + return name; + } + + public synchronized void invert(@Mutable RGB this) { + red = 255 - red; + green = 255 - green; + blue = 255 - blue; + name = "Inverse of " + name; + } + + public static void main(String[] args) { + @Immutable RGB immutable = new @Immutable RGB(0, 0, 0, "black"); + // :: error: (method.invocation.invalid) + immutable.set(1, 1, 1, "what"); + // :: error: (method.invocation.invalid) + immutable.invert(); + immutable.getName(); + immutable.getRGB(); + + @Mutable RGB mutable = new @Mutable RGB(255, 255, 255, "white"); + mutable.set(1, 1, 1, "what"); + mutable.invert(); + mutable.getName(); + mutable.getRGB(); + } +} diff --git a/checker/tests/pico-immutability/RawTypeTest.java b/checker/tests/pico-immutability/RawTypeTest.java new file mode 100644 index 00000000000..08e93d6f6ae --- /dev/null +++ b/checker/tests/pico-immutability/RawTypeTest.java @@ -0,0 +1,80 @@ +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +import java.util.AbstractList; +import java.util.ArrayList; +import java.util.Iterator; + +public class RawTypeTest { + // :: error: (initialization.field.uninitialized) + private ArrayList list; + + protected void foo() { + for (Iterator i = list.iterator(); i.hasNext(); ) { + // Iterator is raw type here. After JDK1.5, it're represented as if there is type + // argument + // "? extends @Mutable Object"(a range of types below @Mutable Object), which is passed + // to + // type parameter "E extends @Readonly Object"(one fixtd type below @Readonly Object). + // Since + // any type under @Mutable Object is below @Readonly Object, "? extends @Mutable Object" + // is + // a valid type argument. foo() method expects a @Mutable A receiver, like above, + // "? extends @Mutable Object" is a valid actual receiver(subtype of @Mutable Object) so + // the + // method invocation typechecks + ((A) i.next()).foo(); + } + } + + interface A { + + public void foo(); + } + + public @Mutable abstract class RawList extends AbstractList { + + // What method does it override? + // What should be the type if no type parameter on class declaration + @Override + @SuppressWarnings("unchecked") + public boolean add(Object o) { + return super.add(o); + } + + @Override + @SuppressWarnings("unchecked") + public void add(int i, Object o) { + super.add(i, o); + } + + @Override + @SuppressWarnings("unchecked") + public Object set(int i, Object o) { + return super.set(i, o); + } + } + + @Mutable abstract class MyList extends AbstractList { + + @Override + public E get(@Readonly MyList this, int i) { + return null; + } + + @Override + public boolean add(E e) { + return super.add(e); + } + + @Override + public void add(int i, E e) { + super.add(i, e); + } + + @Override + public E set(int i, E e) { + return super.set(i, e); + } + } +} diff --git a/checker/tests/pico-immutability/ReimStudy.java b/checker/tests/pico-immutability/ReimStudy.java new file mode 100644 index 00000000000..d4ab25f80f8 --- /dev/null +++ b/checker/tests/pico-immutability/ReimStudy.java @@ -0,0 +1,75 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +import java.util.Date; + +public @ReceiverDependentMutable class ReimStudy { + // :: error: (initialization.field.uninitialized) + @ReceiverDependentMutable Date date; + + @ReceiverDependentMutable Date getDate(@ReceiverDependentMutable ReimStudy this) { + return this.date; + } + + @SuppressWarnings({"deprecation"}) + void cellSetHours(@Mutable ReimStudy this) { + // ReIm argues that viewpoint adapting to lhs(@Mutable here) trasmits the context to current + // "this" via below type rules: + // q(this-cellSetHours) <: q(md) |> q(this-getDate) Which is q(this-cellSetHours) <: + // @Mutable |> @PolyImmutable = @Mutable + // And it gives an counterexample that if we adapt to the receiver of the method invocation, + // we get a not-useful constraint: + // q(this-cellSetHours) <: q(this-cellSetHours) |> q(this-getDate) Which is + // q(this-cellSetHours) <: q(this-cellSetHours) + + // But in fact, we can still transmit that mutability context into current "this" even + // without adapting to lhs. + // q(this-cellSetHours) |> q(ret-getDate) <: q(md) which becomes q(this-cellSetHours) <: + // @Mutable. It still can make current "this" + // to be mutable. + // Truly, viewpoint adaptation to receiver doesn't impose additional constraint on receiver. + // But this makes sense. Because poly + // means that it can be substited by any qualifiers including poly itself. That's exactly + // the purpose of method with poly "this" - + // invocable on all possible types. ReIm also suffers this "not-useful" contraint problem on + // return type adaptation: + // q(md) |> q(ret-getDate) <: q(md) which becomes q(md) <: q(md). So there is no reason for + // ReIm to argue against this "seems-like" + // trivial constraint + @Mutable Date md = this.getDate(); + md.setHours(1); + } + + @SuppressWarnings({"deprecation"}) + void cellGetHours(@Readonly ReimStudy this) { + // In receiver viewpoint adaptation: + // q(this-cellGetHours) |> @PolyImmutable <: @Readonly => q(this-cellGetHours) <: @Readonly + // So cellGetHours is invocable on any types of receiver. + // In inference, if we prefer top(@Readonly), it still infers current "this" to @Readonly. + // :: error: (method.invocation.invalid) + @Readonly Date rd = this.getDate(); + int hour = rd.getHours(); + } + + @ReceiverDependentMutable class DateCell2 { + // :: error: (initialization.field.uninitialized) + @Immutable Date imdate; + + @Immutable Date getImmutableDate(@PolyMutable DateCell2 this) { + return this.imdate; + } + + /*Not allowed in ReIm. But allowed in PICO*/ + void test1(@Mutable DateCell2 this) { + @Immutable Date imd = this.getImmutableDate(); + } + + void test2(@Immutable DateCell2 this) { + @Immutable DateCell2 waht = new @Immutable DateCell2(); + @Immutable Date imd = this.getImmutableDate(); + } + } +} diff --git a/checker/tests/pico-immutability/StaticTest.java b/checker/tests/pico-immutability/StaticTest.java new file mode 100644 index 00000000000..eba8d341cca --- /dev/null +++ b/checker/tests/pico-immutability/StaticTest.java @@ -0,0 +1,27 @@ +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +public class StaticTest { + // :: error: (static.receiverdependentmutable.forbidden) + static @ReceiverDependentMutable Object rmdField = new @ReceiverDependentMutable Object(); + + static { + // :: error: (static.receiverdependentmutable.forbidden) + @Readonly Object rdmObject = (@ReceiverDependentMutable Object) rmdField; + // :: error: (static.receiverdependentmutable.forbidden) + new @ReceiverDependentMutable Object(); + } + + // :: error: (static.receiverdependentmutable.forbidden) + static @ReceiverDependentMutable Object staticMethod( + // :: error: (static.receiverdependentmutable.forbidden) + @ReceiverDependentMutable Object rdmObject) { + return rmdField; + } + + // :: error: (static.receiverdependentmutable.forbidden) + static void foo(T p) { + // :: error: (static.receiverdependentmutable.forbidden) + p = null; + } +} diff --git a/checker/tests/pico-immutability/SuperClassTest.java b/checker/tests/pico-immutability/SuperClassTest.java new file mode 100644 index 00000000000..0c1c7ca9578 --- /dev/null +++ b/checker/tests/pico-immutability/SuperClassTest.java @@ -0,0 +1,154 @@ +import org.checkerframework.checker.initialization.qual.NotOnlyInitialized; +import org.checkerframework.checker.initialization.qual.UnderInitialization; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +import java.util.Date; + +public class SuperClassTest { + @ReceiverDependentMutable class SuperClass { + @ReceiverDependentMutable Date p; + + @Immutable SuperClass(@Immutable Date p) { + this.p = p; + } + + void maliciouslyModifyDate(@Mutable SuperClass this) { + p.setTime(2L); + } + } + + @Mutable class SubClass extends SuperClass { + @Mutable SubClass() { + // :: error: (super.invocation.invalid) + super(new @Immutable Date(1L)); + } + + void test(String[] args) { + @Mutable SubClass victim = new @Mutable SubClass(); + victim.maliciouslyModifyDate(); + } + } + + @ReceiverDependentMutable class AnotherSubClass extends SuperClass { + @ReceiverDependentMutable AnotherSubClass() { + // :: error: (super.invocation.invalid) + super(new @Immutable Date(1L)); + } + + void test(String[] args) { + @Mutable SubClass victim = new @Mutable SubClass(); + victim.maliciouslyModifyDate(); + } + } + + @ReceiverDependentMutable class Thief { + @NotOnlyInitialized @ReceiverDependentMutable SuperClass2 victimCaptured; + + @ReceiverDependentMutable Thief(@UnderInitialization @ReceiverDependentMutable SuperClass2 victimCaptured) { + this.victimCaptured = victimCaptured; + } + } + + @ReceiverDependentMutable class SuperClass2 { + @ReceiverDependentMutable Date p; + @NotOnlyInitialized @ReceiverDependentMutable Thief thief; + + @Mutable SuperClass2(@Mutable Date p) { + this.p = p; + // "this" escapes constructor and gets captured by thief + this.thief = new @Mutable Thief(this); + } + } + + @Immutable class SubClass2 extends SuperClass2 { + @Immutable SubClass2() { + // This is not ok any more + // :: error: (super.invocation.invalid) + super(new @Mutable Date()); + } + } + + @ReceiverDependentMutable class AnotherSubClass2 extends SuperClass2 { + @ReceiverDependentMutable AnotherSubClass2() { + // This is not ok any more + // :: error: (super.invocation.invalid) + super(new @Mutable Date()); + } + } + + @ReceiverDependentMutable class SuperClass3 { + @ReceiverDependentMutable Date p; + + @ReceiverDependentMutable SuperClass3(@ReceiverDependentMutable Date p) { + this.p = p; + } + } + + @Mutable class SubClass3 extends SuperClass3 { + @Mutable SubClass3() { + super(new @Mutable Date(1L)); + } + } + + @Immutable class AnotherSubClass3 extends SuperClass3 { + @Immutable AnotherSubClass3() { + super(new @Immutable Date(1L)); + } + } + + @ReceiverDependentMutable class ThirdSubClass3 extends SuperClass3 { + @ReceiverDependentMutable ThirdSubClass3() { + super(new @ReceiverDependentMutable Date(1L)); + } + } + + @ReceiverDependentMutable class SuperMethodInvocation { + @ReceiverDependentMutable Object f; + + @ReceiverDependentMutable SuperMethodInvocation() { + this.f = new @ReceiverDependentMutable Object(); + } + + void foo(@Mutable SuperMethodInvocation this) { + this.f = new @Mutable Object(); + } + } + + @Immutable class Subclass extends SuperMethodInvocation { + + @Immutable Subclass() { + // TODO Still need to investigate if it's proper to allow such reassignment + // We may as well say "f is alreayd initializaed" so f can't be reassigned. + // The way to implement it is to check @UnderInitialization(SuperMethodInvocation.class) + // and f is within the class hierarchy range Object.class ~ SuperMethodInvocation.class, + // so forbid reassigning it. + this.f = new @Immutable Object(); + } + + // Yes, the overriding method can be contravariant(going to supertype) in terms of + // receiver and formal parameters. This ensures that all the existing method invocation + // won't break just because maybe some days later, the method is overriden in the + // subclass :) + @Override + void foo(@Readonly Subclass this) { + // But this super method invocation definitely shouldn't typecheck. "super" has the same + // mutability as the declared "this" parameter. Because the declared receiver can now + // be passed in @Immutable objects, if we allowed this super invocation, then its + // abstract + // state will be changed and immutability guarantee will be compromised. So, we still + // retain the standard/default typechecking rules for calling super method using "super" + // :: error: (method.invocation.invalid) + super.foo(); + } + + void test(String[] args) { + // Example that illustrates the point above is here: calling foo() method will alter the + // abstract state of sub object, which should be @Immutable + @Immutable Subclass sub = new @Immutable Subclass(); + sub.foo(); + } + } +} diff --git a/checker/tests/pico-immutability/SupportedBuilderPattern.java b/checker/tests/pico-immutability/SupportedBuilderPattern.java new file mode 100644 index 00000000000..5262df6b574 --- /dev/null +++ b/checker/tests/pico-immutability/SupportedBuilderPattern.java @@ -0,0 +1,54 @@ +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.PolyMutable; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +import java.util.Date; + +// TODO Understand polymutable creation +@ReceiverDependentMutable public class SupportedBuilderPattern { + private final int id; + private String address; + private @Immutable Date date; + + private @ReceiverDependentMutable SupportedBuilderPattern(Builder builder) { + this.id = builder.id; + this.address = builder.address; + this.date = builder.date; + } + + public static @Mutable class Builder { + private final int id; + private String address; + private @Immutable Date date; + + public Builder(int id) { + this.id = id; + } + + public Builder withAddress(String address) { + this.address = address; + return this; + } + + public Builder withDate(@Immutable Date date) { + this.date = date; + return this; + } + + public @PolyMutable SupportedBuilderPattern build() { + return new @PolyMutable SupportedBuilderPattern(this); + } + } + + class Test { + void test(String[] args) { + SupportedBuilderPattern.@Mutable Builder builder = + new SupportedBuilderPattern.Builder(0); + @Mutable SupportedBuilderPattern msbp = + builder.withAddress("10 King St.").withDate(new @Immutable Date()).build(); + @Immutable SupportedBuilderPattern imsbp = + builder.withAddress("1 Lester St.").withDate(new @Immutable Date()).build(); + } + } +} diff --git a/checker/tests/pico-immutability/Transitive.java b/checker/tests/pico-immutability/Transitive.java new file mode 100644 index 00000000000..8fdaed5d261 --- /dev/null +++ b/checker/tests/pico-immutability/Transitive.java @@ -0,0 +1,44 @@ +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; + +public class Transitive { + + @Mutable static class A { + B b; + + public B getB() { + return b; + } + } + + @Mutable static class B { + int field = 0; + C c; + + public C getC() { + return c; + } + } + + @Mutable static class C { + int field = 0; + } + + static class Caller { + void test(@Readonly A a) { + // :: error: (illegal.field.write) + a.b.field = 1; + // :: error: (method.invocation.invalid) + a.getB().field = 1; + + // :: error: (illegal.field.write) + a.b.c.field = 1; + // :: error: (method.invocation.invalid) + a.getB().getC().field = 1; + // :: error: (method.invocation.invalid) + a.b.getC().field = 1; + // :: error: (method.invocation.invalid) + a.getB().c.field = 1; + } + } +} diff --git a/checker/tests/pico-immutability/ViewpointAdaptationRules.java b/checker/tests/pico-immutability/ViewpointAdaptationRules.java new file mode 100644 index 00000000000..ff43e4cc918 --- /dev/null +++ b/checker/tests/pico-immutability/ViewpointAdaptationRules.java @@ -0,0 +1,148 @@ +import org.checkerframework.checker.pico.qual.Assignable; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Mutable; +import org.checkerframework.checker.pico.qual.Readonly; +import org.checkerframework.checker.pico.qual.ReceiverDependentMutable; + +@ReceiverDependentMutable public class ViewpointAdaptationRules { + + @Assignable @Readonly Object assignableReadonlyField; + @ReceiverDependentMutable Object rdmField; + @Immutable Object immutableField; + @Assignable @Mutable Object assingableMuatbleField; + + @ReceiverDependentMutable ViewpointAdaptationRules( + @Readonly Object readonlyObject, + @ReceiverDependentMutable Object rdmObject, + @Immutable Object immutableObject, + @Mutable Object muatbleObject) { + this.assignableReadonlyField = readonlyObject; + this.rdmField = rdmObject; + this.immutableField = immutableObject; + this.assingableMuatbleField = muatbleObject; + } + + void mutatableReceiver( + @Mutable ViewpointAdaptationRules this, + @Mutable Object mutableObject, + @Immutable Object immutableObject, + @Readonly Object readonlyObject) { + this.assignableReadonlyField = mutableObject; + this.rdmField = mutableObject; + // :: error: (assignment.type.incompatible) + this.immutableField = mutableObject; + this.assingableMuatbleField = mutableObject; + + this.assignableReadonlyField = immutableObject; + // :: error: (assignment.type.incompatible) + this.rdmField = immutableObject; // The field is adapted to mutable + this.immutableField = immutableObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = immutableObject; + + this.assignableReadonlyField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.rdmField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.immutableField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = readonlyObject; + } + + void receiverDependentMutableReceiver( + @ReceiverDependentMutable ViewpointAdaptationRules this, + @Mutable Object mutableObject, + @ReceiverDependentMutable Object rdmObject, + @Immutable Object immutableObject, + @Readonly Object readonlyObject) { + + this.assignableReadonlyField = mutableObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = mutableObject; // The field is still RDM and can not be assigned to mutable + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = mutableObject; + this.assingableMuatbleField = mutableObject; + + this.assignableReadonlyField = rdmObject; + // :: error: (illegal.field.write) + this.rdmField = rdmObject; // can not write to it as it is non assignable + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = rdmObject; // can not write to it as it is non assignable + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = rdmObject; + + this.assignableReadonlyField = immutableObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = immutableObject; + // :: error: (illegal.field.write) + this.immutableField = immutableObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = immutableObject; + + this.assignableReadonlyField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = readonlyObject; + } + + void ImmutableReceiver( + @Immutable ViewpointAdaptationRules this, + @Mutable Object mutableObject, + @Immutable Object immutableObject, + @Readonly Object readonlyObject) { + this.assignableReadonlyField = mutableObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = mutableObject; // The field is adapted to Immutable + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = mutableObject; + this.assingableMuatbleField = mutableObject; + + this.assignableReadonlyField = immutableObject; + // :: error: (illegal.field.write) + this.rdmField = immutableObject; + // :: error: (illegal.field.write) + this.immutableField = immutableObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = immutableObject; + + this.assignableReadonlyField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = readonlyObject; + } + + void ReadonlyReceiver( + @Readonly ViewpointAdaptationRules this, + @Mutable Object mutableObject, + @Immutable Object immutableObject, + @Readonly Object readonlyObject) { + this.assignableReadonlyField = mutableObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = mutableObject; // Field is adpated to PICOLost + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = mutableObject; + this.assingableMuatbleField = mutableObject; + + this.assignableReadonlyField = immutableObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = immutableObject; + // :: error: (illegal.field.write) + this.immutableField = immutableObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = immutableObject; + + this.assignableReadonlyField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.rdmField = readonlyObject; + // :: error: (assignment.type.incompatible) :: error: (illegal.field.write) + this.immutableField = readonlyObject; + // :: error: (assignment.type.incompatible) + this.assingableMuatbleField = readonlyObject; + } +} diff --git a/framework/src/main/java/org/jmlspecs/annotation/Readonly.java b/framework/src/main/java/org/jmlspecs/annotation/Readonly.java new file mode 100644 index 00000000000..d89edf46816 --- /dev/null +++ b/framework/src/main/java/org/jmlspecs/annotation/Readonly.java @@ -0,0 +1,10 @@ +package org.jmlspecs.annotation; + +import java.lang.annotation.Documented; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; + +/** Defines the 'readonly' JML annotation */ +@Retention(RetentionPolicy.RUNTIME) +@Documented +public @interface Readonly {}