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/Bottom.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Bottom.java new file mode 100644 index 00000000000..e78f305c738 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Bottom.java @@ -0,0 +1,29 @@ +package org.checkerframework.checker.pico.qual; + +import org.checkerframework.framework.qual.DefaultFor; +import org.checkerframework.framework.qual.SubtypeOf; +import org.checkerframework.framework.qual.TargetLocations; +import org.checkerframework.framework.qual.TypeKind; +import org.checkerframework.framework.qual.TypeUseLocation; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * {@code @Bottom} can only be annotated before a type parameter (For example, {@code class + * C<@Bottom T extends MutableBox>{}}). This means {@code @Bottom} is the lower bound for this type + * parameter. + * + *

User can explicitly write {@code @Bottom} but it's not necessary because it's automatically + * inferred, and we have -AwarnRedundantAnnotations flag to warn about redundant annotations. + */ +@SubtypeOf({Mutable.class, Immutable.class, ReceiverDependentMutable.class, Lost.class}) +@DefaultFor(typeKinds = {TypeKind.NULL}) +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_PARAMETER}) +@TargetLocations({TypeUseLocation.LOWER_BOUND}) +public @interface Bottom {} 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/Lost.java b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Lost.java new file mode 100644 index 00000000000..bcc1eea3b25 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/Lost.java @@ -0,0 +1,12 @@ +package org.checkerframework.checker.pico.qual; + +import org.checkerframework.framework.qual.SubtypeOf; + +import java.lang.annotation.*; + +/** Lost means the mutability type of this reference is unknown. This is a subtype of Readonly. */ +@SubtypeOf({Readonly.class}) +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +public @interface Lost {} 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..a11dcdd72de --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/pico/qual/ObjectIdentityMethod.java @@ -0,0 +1,12 @@ +package org.checkerframework.checker.pico.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD}) +public @interface ObjectIdentityMethod {} 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..adc64c4d1fc --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/ObjectIdentityMethodEnforcer.java @@ -0,0 +1,110 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY; + +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.MemberSelectTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.Tree; +import com.sun.source.util.TreePath; +import com.sun.source.util.TreePathScanner; + +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreeUtils; + +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; + +public class ObjectIdentityMethodEnforcer extends TreePathScanner { + + private PICONoInitAnnotatedTypeFactory typeFactory; + private BaseTypeChecker checker; + + private ObjectIdentityMethodEnforcer( + PICONoInitAnnotatedTypeFactory typeFactory, BaseTypeChecker checker) { + this.typeFactory = typeFactory; + this.checker = checker; + } + + // Main entry + public static void check( + TreePath statement, + PICONoInitAnnotatedTypeFactory typeFactory, + BaseTypeChecker checker) { + if (statement == null) return; + ObjectIdentityMethodEnforcer asfchecker = + new ObjectIdentityMethodEnforcer(typeFactory, checker); + asfchecker.scan(statement, null); + } + + @Override + public Void visitMethodInvocation(MethodInvocationTree node, Void aVoid) { + Element elt = TreeUtils.elementFromUse(node); + checkMethod(node, elt); + return super.visitMethodInvocation(node, aVoid); + } + + private void checkMethod(MethodInvocationTree node, Element elt) { + assert elt instanceof ExecutableElement; + if (ElementUtils.isStatic(elt)) { + return; // Doesn't check static method invocation because it doesn't access instance + // field + } + if (!PICOTypeUtil.isObjectIdentityMethod((ExecutableElement) elt, typeFactory)) { + // Report warning since invoked method is not only dependent on abstract state fields, + // but we + // don't know whether this method invocation's result flows into the hashcode or not. + checker.reportWarning(node, "object.identity.method.invocation.invalid", elt); + } + } + + @Override + public Void visitIdentifier(IdentifierTree node, Void aVoid) { + Element elt = TreeUtils.elementFromUse(node); + checkField(node, elt); + return super.visitIdentifier(node, aVoid); + } + + @Override + public Void visitMemberSelect(MemberSelectTree node, Void aVoid) { + Element elt = TreeUtils.elementFromUse(node); + checkField(node, elt); + return super.visitMemberSelect(node, aVoid); + } + + private void checkField(Tree node, Element elt) { + if (elt == null) return; + if (elt.getSimpleName().contentEquals("this") + || elt.getSimpleName().contentEquals("super")) { + return; + } + if (elt.getKind() == ElementKind.FIELD) { + if (ElementUtils.isStatic(elt)) { + checker.reportWarning(node, "object.identity.static.field.access.forbidden", elt); + } else { + if (!isInAbstractState(elt, typeFactory)) { + // Report warning since accessed field is not within abstract state + checker.reportWarning(node, "object.identity.field.access.invalid", elt); + } + } + } + } + + // Deeply test if a field is in abstract state or not. For composite types: array component, + // type arguments, upper bound of type parameter uses are also checked. + private boolean isInAbstractState(Element elt, PICONoInitAnnotatedTypeFactory typeFactory) { + boolean in = true; + if (PICOTypeUtil.isAssignableField(elt, typeFactory)) { + in = false; + } else if (AnnotatedTypes.containsModifier(typeFactory.getAnnotatedType(elt), MUTABLE)) { + in = false; + } else if (AnnotatedTypes.containsModifier(typeFactory.getAnnotatedType(elt), READONLY)) { + in = false; + } + return in; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/pico/PICOAnnotationMirrorHolder.java b/checker/src/main/java/org/checkerframework/checker/pico/PICOAnnotationMirrorHolder.java new file mode 100644 index 00000000000..bdc5d445cdc --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOAnnotationMirrorHolder.java @@ -0,0 +1,38 @@ +package org.checkerframework.checker.pico; + +import org.checkerframework.checker.pico.qual.Bottom; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Lost; +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 org.checkerframework.framework.source.SourceChecker; +import org.checkerframework.javacutil.AnnotationBuilder; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; + +/** A holder class that holds AnnotationMirrors that are shared by PICO and PICOInfer. */ +public class PICOAnnotationMirrorHolder { + + public static AnnotationMirror READONLY; + public static AnnotationMirror MUTABLE; + public static AnnotationMirror POLY_MUTABLE; + public static AnnotationMirror RECEIVER_DEPENDENT_MUTABLE; + public static AnnotationMirror IMMUTABLE; + public static AnnotationMirror LOST; + public static AnnotationMirror BOTTOM; + + public static void init(SourceChecker checker) { + Elements elements = checker.getElementUtils(); + READONLY = AnnotationBuilder.fromClass(elements, Readonly.class); + MUTABLE = AnnotationBuilder.fromClass(elements, Mutable.class); + POLY_MUTABLE = AnnotationBuilder.fromClass(elements, PolyMutable.class); + RECEIVER_DEPENDENT_MUTABLE = + AnnotationBuilder.fromClass(elements, ReceiverDependentMutable.class); + IMMUTABLE = AnnotationBuilder.fromClass(elements, Immutable.class); + LOST = AnnotationBuilder.fromClass(elements, Lost.class); + BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class); + } +} 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..c106ac22197 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOChecker.java @@ -0,0 +1,44 @@ +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; + +@SupportedOptions({"abstractStateOnly", "immutableDefault"}) +public class PICOChecker extends InitializationChecker { + + public PICOChecker() {} + + @Override + public Class getTargetCheckerClass() { + return PICONoInitSubchecker.class; + } + + @Override + public void initChecker() { + super.initChecker(); + PICOAnnotationMirrorHolder.init(this); + } + + @Override + public boolean checkPrimitives() { + return true; + } + + @Override + protected boolean shouldAddShutdownHook() { + return super.shouldAddShutdownHook(); + } + + @Override + protected void shutdownHook() { + super.shutdownHook(); + } + + @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..343d374bde8 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOInitializationAnnotatedTypeFactory.java @@ -0,0 +1,97 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; + +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.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.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; + +/** + * 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 { + /** + * Constructor for PICOInitializationAnnotatedTypeFactory. + * + * @param checker the BaseTypeChecker this visitor works with + */ + public PICOInitializationAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + 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 (PICOTypeUtilnested.isAssignableField(varElement, this) + || ElementUtils.isStatic(varElement)) { + return true; + } else { + return false; + } + } + }); + return uninitializedFields; + } + + // TODO this is a hack for calling static class method for lambda expression, consider remove + // with refactor of PICOTypeUtil + public static class PICOTypeUtilnested extends PICOTypeUtil {} +} 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..e35376c7b5b --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnalysis.java @@ -0,0 +1,39 @@ +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 { + + 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..642093dcb05 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitAnnotatedTypeFactory.java @@ -0,0 +1,550 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.IMMUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.RECEIVER_DEPENDENT_MUTABLE; + +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.Bottom; +import org.checkerframework.checker.pico.qual.Immutable; +import org.checkerframework.checker.pico.qual.Lost; +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 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.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.Set; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +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. + */ +// TODO Use @Immutable for classes that extends those predefined immutable classess like String or +// Number and explicitly annotated classes with @Immutable on its declaration +public class PICONoInitAnnotatedTypeFactory + extends GenericAnnotatedTypeFactory< + PICONoInitValue, PICONoInitStore, PICONoInitTransfer, PICONoInitAnalysis> { + + public PICONoInitAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + postInit(); + // PICO aliasing is not implemented correctly remove for now + // addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + } + + @Override + protected Set> createSupportedTypeQualifiers() { + return new LinkedHashSet<>( + Arrays.asList( + Readonly.class, + Mutable.class, + PolyMutable.class, + ReceiverDependentMutable.class, + Immutable.class, + Lost.class, + Bottom.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) { + PICOTypeUtil.addDefaultForField(this, type, elt); + PICOTypeUtil.defaultConstructorReturnToClassBound(this, elt, type); + super.addComputedTypeAnnotations(elt, type); + } + + 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; + } + + /** Tree Annotators */ + public static class PICOPropagationTreeAnnotator extends PropagationTreeAnnotator { + public PICOPropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(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(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(RECEIVER_DEPENDENT_MUTABLE)) { + // if (checker.hasOption("immutableDefault")) { + // componentType.replaceAnnotation(IMMUTABLE); + // } else + componentType.replaceAnnotation(IMMUTABLE); + } + return null; + } + + @Override + public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { + boolean hasExplicitAnnos = !type.getAnnotations().isEmpty(); + super.visitTypeCast(node, type); + if (!hasExplicitAnnos && type.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + // if (checker.hasOption("immutableDefault")) { + // type.replaceAnnotation(IMMUTABLE); + // } else + type.replaceAnnotation(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 { + public PICOTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(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); + PICOTypeUtil.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); + PICOTypeUtil.addDefaultForField(atypeFactory, annotatedTypeMirror, element); + return super.visitVariable(tree, annotatedTypeMirror); + } + + @Override + public Void visitBinary(BinaryTree tree, AnnotatedTypeMirror type) { + type.replaceAnnotation(IMMUTABLE); + return null; + } + } + + /** Type Annotators */ + public static class PICOTypeAnnotator extends TypeAnnotator { + + public PICOTypeAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + } + + /** + * 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(READONLY); + } else if (PICOTypeUtil.isMethodOrOverridingMethod( + t, "equals(java.lang.Object)", atypeFactory)) { + assert t.getReceiverType() != null; + t.getReceiverType().replaceAnnotation(READONLY); + t.getParameterTypes().get(0).replaceAnnotation(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(READONLY)) + t.getReceiverType().replaceAnnotation(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); + } + + public static class PICOQualifierForUseTypeAnnotator + extends DefaultQualifierForUseTypeAnnotator { + + public PICOQualifierForUseTypeAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + } + + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Void aVoid) { + + Element element = type.getUnderlyingType().asElement(); + AnnotationMirrorSet annosToApply = getDefaultAnnosForUses(element); + + if (annosToApply.contains(MUTABLE) || annosToApply.contains(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; + } + } + + public static class PICODefaultForTypeAnnotator extends DefaultForTypeAnnotator { + + 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 {} + public static class PICOSuperClauseAnnotator extends TreeAnnotator { + + public PICOSuperClauseAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + public static boolean isSuperClause(TreePath path) { + if (path == null) { + return false; + } + return TreeUtils.isClassTree(path.getParentPath().getLeaf()); + } + + 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(READONLY) + || atypeFactory + .getQualifierHierarchy() + .findAnnotationInHierarchy( + TreeUtils.typeOf(tree).getAnnotationMirrors(), + READONLY) + == null)) { + AnnotatedTypeMirror enclosing = + atypeFactory.getAnnotatedType(TreePathUtil.enclosingClass(path)); + AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(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); + } + } + + public static class PICOEnumDefaultAnnotator extends TypeAnnotator { + // Defaulting only applies the same annotation to all class declarations + // We need this to "only default enums" to immutable + + public PICOEnumDefaultAnnotator(AnnotatedTypeFactory typeFactory) { + super(typeFactory); + } + + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Void aVoid) { + if (PICOTypeUtil.isEnumOrEnumConstant(type)) { + type.addMissingAnnotations(Collections.singleton(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..6f57cbd10ee --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitStore.java @@ -0,0 +1,26 @@ +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; + +public class PICONoInitStore extends CFAbstractStore { + + protected Map<@Immutable FieldAccess, PICONoInitValue> initializedFields; + + public PICONoInitStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + } + + 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..aa12f4e747d --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitSubchecker.java @@ -0,0 +1,28 @@ +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; + +public class PICONoInitSubchecker extends BaseTypeChecker { + 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..824fa9f4cb3 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitTransfer.java @@ -0,0 +1,44 @@ +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; + +public class PICONoInitTransfer + extends CFAbstractTransfer { + + 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..25936e51271 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitValue.java @@ -0,0 +1,16 @@ +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; + +public class PICONoInitValue extends CFAbstractValue { + 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..890cffe5ce2 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICONoInitVisitor.java @@ -0,0 +1,567 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.BOTTOM; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.IMMUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.POLY_MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.RECEIVER_DEPENDENT_MUTABLE; +import static org.checkerframework.javacutil.TreePathUtil.isTopLevelAssignmentInInitializerBlock; + +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.TypeElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; + +public class PICONoInitVisitor extends BaseTypeVisitor { + /** whether to only check observational purity */ + protected final boolean abstractStateOnly; + + 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(POLY_MUTABLE)) { + return true; + } + + AnnotationMirror declared = declarationType.getAnnotationInHierarchy(READONLY); + AnnotationMirror used = useType.getAnnotationInHierarchy(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(READONLY); + return !AnnotationUtils.areSame(used, BOTTOM); + } + + 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, 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(READONLY), + returnType.getAnnotationInHierarchy(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(READONLY) + || constructorReturnType.hasAnnotation(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); + } + + 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 (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) { + // One pico side, if the receiver is mutable, we allow assigning/reassigning. Because if + // the field is declared as final, Java compiler will catch that, and we couldn't have + // reached this + // point + if (receiverType.hasAnnotation(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(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(IMMUTABLE) + || type.hasAnnotation(MUTABLE) + || type.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE) + // TODO: allow poly_mutable creation or not? + || type.hasAnnotation(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(BOTTOM)); + return result; + } + + @Override + protected AnnotationMirrorSet getThrowUpperBoundAnnotations() { + AnnotationMirrorSet result = new AnnotationMirrorSet(); + result.add(atypeFactory.getQualifierHierarchy().getTopAnnotation(READONLY)); + return result; + } + + @Override + public void processClassTree(ClassTree node) { + TypeElement typeElement = TreeUtils.elementFromDeclaration(node); + // 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(node); + return; + } + + AnnotatedTypeMirror bound = + PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); + // Class annotation has to be either @Mutable, @ReceiverDependentMutable or @Immutable + if (!bound.hasAnnotation(MUTABLE) + && !bound.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE) + && !bound.hasAnnotation(IMMUTABLE)) { + checker.reportError(node, "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(IMMUTABLE) || bound.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + for (Tree member : node.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), MUTABLE) + && !noDefaultMirror.hasAnnotationInHierarchy(READONLY)) { + checker.reportError(member, "implicit.shallow.immutable"); + } + } + } + } + super.processClassTree(node); + } + + /** + * 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(READONLY); + AnnotationMirror constructorTypeMirror = + constructorType.getReturnType().getAnnotationInHierarchy(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()), + READONLY); + assert bound != null; + + if (AnnotationUtils.areSame(castDeclared.getAnnotationInHierarchy(READONLY), bound)) { + return true; + } + } + + return super.isTypeCastSafe(castType, exprType); + } + + @Override + protected boolean commonAssignmentCheck( + AnnotatedTypeMirror varType, + AnnotatedTypeMirror valueType, + Tree valueTree, + String errorKey, + Object... extraArgs) { + // TODO: WORKAROUND: anonymous class handling + if (TypesUtils.isAnonymous(valueType.getUnderlyingType())) { + AnnotatedTypeMirror newValueType = varType.deepCopy(); + newValueType.replaceAnnotation(valueType.getAnnotationInHierarchy(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..d2fb0a7bb6f --- /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.Bottom; +import org.checkerframework.checker.pico.qual.Lost; +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, Lost.class) + && !atypeFactory.areSameByClass(subAnno, Bottom.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..d4b785a06c4 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOTypeUtil.java @@ -0,0 +1,577 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.IMMUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.RECEIVER_DEPENDENT_MUTABLE; + +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.AnnotatedArrayType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Objects; +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; +import javax.lang.model.type.TypeMirror; + +public class PICOTypeUtil { + + 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); + } + + /** + * 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; + } + + public static List getBoundTypesOfDirectSuperTypes( + TypeElement current, AnnotatedTypeFactory atypeFactory) { + List boundsOfSupers = new ArrayList<>(); + TypeMirror supertypecls; + try { + supertypecls = current.getSuperclass(); + } catch (Symbol.CompletionFailure cf) { + // Copied from ElementUtils#getSuperTypes(Elements, TypeElement) + // Looking up a supertype failed. This sometimes happens + // when transitive dependencies are not on the classpath. + // As javac didn't complain, let's also not complain. + // TODO: Use an expanded ErrorReporter to output a message. + supertypecls = null; + } + + if (supertypecls != null && !supertypecls.getKind().name().equals(TypeKind.NONE.name())) { + TypeElement supercls = (TypeElement) ((DeclaredType) supertypecls).asElement(); + boundsOfSupers.add(getBoundTypeOfTypeDeclaration(supercls, atypeFactory)); + } + + for (TypeMirror supertypeitf : current.getInterfaces()) { + TypeElement superitf = (TypeElement) ((DeclaredType) supertypeitf).asElement(); + boundsOfSupers.add(getBoundTypeOfTypeDeclaration(superitf, atypeFactory)); + } + return boundsOfSupers; + } + + public static AnnotatedTypeMirror getBoundTypeOfTypeDeclaration( + ClassTree classTree, AnnotatedTypeFactory atypeFactory) { + TypeElement typeElement = TreeUtils.elementFromDeclaration(classTree); + return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); + } + + /** + * 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. + } + + public static AnnotatedTypeMirror getBoundTypeOfTypeDeclaration( + TypeMirror typeMirror, AnnotatedTypeFactory atypeFactory) { + return getBoundTypeOfTypeDeclaration(TypesUtils.getTypeElement(typeMirror), atypeFactory); + } + + /** Helper method to determine a method using method name */ + public static boolean isMethodOrOverridingMethod( + AnnotatedExecutableType methodType, + String methodName, + AnnotatedTypeFactory annotatedTypeFactory) { + return isMethodOrOverridingMethod( + methodType.getElement(), methodName, annotatedTypeFactory); + } + + 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; + } + + public static 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 AnnotatedDeclaredType) { + AnnotatedDeclaredType adt = (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 = + getBoundTypeOfTypeDeclaration( + typeElement, annotatedTypeFactory); + if (bound.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE)) { + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDENT_MUTABLE); + } + } + } else if (explicitATM instanceof AnnotatedArrayType) { + // If the ATM is array type, apply RMD to array's component type. + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDENT_MUTABLE); + } + } + } + } + } + + /** + * 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); + } + + public static boolean isEnumOrEnumConstant(TypeMirror type) { + if (!(type instanceof DeclaredType)) { + return false; + } + Element element = ((DeclaredType) type).asElement(); + return element != null + && (element.getKind() == ElementKind.ENUM_CONSTANT + || element.getKind() == ElementKind.ENUM); + } + + /** + * 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) + */ + public static 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))); + } + } + + /** + * 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); + } + + public static boolean isEnclosedByAnonymousClass(Tree tree, AnnotatedTypeFactory atypeFactory) { + TreePath path = atypeFactory.getPath(tree); + if (path != null) { + ClassTree classTree = TreePathUtil.enclosingClass(path); + return classTree != null; + } + return false; + } + + public static AnnotatedDeclaredType getBoundOfEnclosingAnonymousClass( + Tree tree, AnnotatedTypeFactory atypeFactory) { + TreePath path = atypeFactory.getPath(tree); + if (path == null) { + return null; + } + AnnotatedDeclaredType enclosingType = null; + Tree newclassTree = TreePathUtil.enclosingOfKind(path, Tree.Kind.NEW_CLASS); + if (newclassTree != null) { + enclosingType = (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(newclassTree); + } + return enclosingType; + } + + 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; + } + + 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; + } + + public static boolean isObjectIdentityMethod( + MethodTree node, AnnotatedTypeFactory annotatedTypeFactory) { + ExecutableElement element = TreeUtils.elementFromDeclaration(node); + return isObjectIdentityMethod(element, annotatedTypeFactory); + } + + public static boolean isObjectIdentityMethod( + ExecutableElement executableElement, AnnotatedTypeFactory annotatedTypeFactory) { + return hasObjectIdentityMethodDeclAnnotation(executableElement, annotatedTypeFactory) + || isMethodOrOverridingMethod(executableElement, "hashCode()", annotatedTypeFactory) + || isMethodOrOverridingMethod( + executableElement, "equals(java.lang.Object)", annotatedTypeFactory); + } + + private static boolean hasObjectIdentityMethodDeclAnnotation( + ExecutableElement element, AnnotatedTypeFactory annotatedTypeFactory) { + return annotatedTypeFactory.getDeclAnnotation(element, ObjectIdentityMethod.class) != null; + } +} 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..97b2e088631 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOValidator.java @@ -0,0 +1,170 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.BOTTOM; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.IMMUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.RECEIVER_DEPENDENT_MUTABLE; + +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 { + 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, MUTABLE) + && type.hasAnnotation(RECEIVER_DEPENDENT_MUTABLE) + && AnnotationUtils.containsSameByName(enclosingBound, 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) { + // Element element; + // if (type instanceof AnnotatedDeclaredType) element = + // ((AnnotatedDeclaredType)type).getUnderlyingType().asElement(); + // else if (type instanceof AnnotatedArrayType) element = + // ((AnnotatedArrayType)type).; + //// AnnotatedTypeMirror explicitATM = atypeFactory.fromElement(element); + // AnnotationMirrorSet declBound = + // atypeFactory.getTypeDeclarationBounds(element.asType()); + 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(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(IMMUTABLE) + && !type.hasAnnotation(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, "one.assignability.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..c3aac57379b --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/pico/PICOViewpointAdapter.java @@ -0,0 +1,64 @@ +package org.checkerframework.checker.pico; + +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.BOTTOM; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.IMMUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.LOST; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.POLY_MUTABLE; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.READONLY; +import static org.checkerframework.checker.pico.PICOAnnotationMirrorHolder.RECEIVER_DEPENDENT_MUTABLE; + +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; +import javax.lang.model.element.Element; +import javax.lang.model.type.TypeKind; + +public class PICOViewpointAdapter extends AbstractViewpointAdapter { + + public PICOViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + @Override + protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { + if (!(type.getKind() == TypeKind.DECLARED || type.getKind() == TypeKind.ARRAY)) { + return false; + } + return super.shouldAdaptMember(type, element); + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + return atm.getAnnotationInHierarchy(READONLY); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (AnnotationUtils.areSame(declaredAnnotation, READONLY)) { + return READONLY; + } else if (AnnotationUtils.areSame(declaredAnnotation, MUTABLE)) { + return MUTABLE; + } else if (AnnotationUtils.areSame(declaredAnnotation, IMMUTABLE)) { + return IMMUTABLE; + } else if (AnnotationUtils.areSame(declaredAnnotation, BOTTOM)) { + return BOTTOM; + } else if (AnnotationUtils.areSame(declaredAnnotation, POLY_MUTABLE)) { + return POLY_MUTABLE; + } else if (AnnotationUtils.areSame(declaredAnnotation, RECEIVER_DEPENDENT_MUTABLE)) { + // @Readonly |> @ReceiverDependentMutable = @Lost + if (AnnotationUtils.areSame(receiverAnnotation, READONLY)) { + return 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..3040c4d67ff --- /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 { + Iterator iterator(@Readonly 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..c6229a03c77 --- /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 +one.assignability.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 !