diff --git a/build.gradle b/build.gradle index 9ba9976..f5d66d0 100644 --- a/build.gradle +++ b/build.gradle @@ -46,23 +46,24 @@ repositories { } dependencies { - compile fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar") - compile fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar") + implementation fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar") + implementation fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar") // sat4j solver dependency - compile 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.6' - compile 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.6' + implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.5' + implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.5' // The production code uses the SLF4J logging API at compile time - compile 'org.slf4j:slf4j-api:1.7.30' - + implementation 'org.slf4j:slf4j-api:1.7.29' // CF test lib dependency - testCompile fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar") - testCompile 'junit:junit:4.13.2' + testImplementation fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar") + testImplementation 'junit:junit:4.12' } sourceSets { main { java { srcDirs = ["src/main/java"] + exclude "pico/inference/**" + } resources { @@ -75,6 +76,8 @@ sourceSets { java { // TODO: we shouldn't need source level dependency on CFITest srcDirs = ["src/test/java", "${cfiPath}/tests/checkers/inference/test"] + exclude "pico/ImmutabilityInferenceInitialTypecheckTest.java","pico/ImmutabilityReImInferenceTest.java", + "pico/ImmutabilityInferenceTest.java" } } } diff --git a/check.sh b/check.sh index a6cbccc..f4b2166 100755 --- a/check.sh +++ b/check.sh @@ -10,7 +10,8 @@ export JAVAC=$CF/checker/bin/javac export PICO=$(cd $(dirname "$0") && pwd) # Dependencies -export CLASSPATH=$PICO/build/classes/java/main:$CFI/dist/checker-framework-inference.jar +export CLASSPATH=$PICO/build/classes/java/main:$PICO/build/resources/main:\ +$PICO/build/libs/immutability.jar:$CFI/dist/checker-framework-inference.jar # Command DEBUG="" @@ -35,9 +36,9 @@ done cmd="" if [ "$DEBUG" == "" ]; then - cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}"" + cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}"" else - cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}"" + cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}"" fi eval "$cmd" diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index be280be..6b7fd26 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -2,4 +2,4 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-4.5-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip diff --git a/infer.sh b/infer.sh index 695c80b..20d4edb 100755 --- a/infer.sh +++ b/infer.sh @@ -19,6 +19,8 @@ CHECKER=pico.inference.PICOInferenceChecker SOLVER=pico.inference.solver.PICOSolverEngine +STUBS="src/main/java/pico/inference/jdk.astub" + declare -a ARGS for i in "$@" ; do if [[ $i == "-ds" ]] ; then @@ -38,4 +40,5 @@ IS_HACK=true # Start the inference $CFI/scripts/inference-dev -m ROUNDTRIP --checker "$CHECKER" --solver "$SOLVER" \ --solverArgs="useGraph=false,collectStatistic=true" --hacks="$IS_HACK" \ + --cfArgs="-Astubs=$STUBS" \ -afud ./annotated "${ARGS[@]}" diff --git a/run-dljc.sh b/run-dljc.sh index 87238a7..64b9009 100755 --- a/run-dljc.sh +++ b/run-dljc.sh @@ -9,7 +9,7 @@ export AFU="$JSR308"/annotation-tools/annotation-file-utilities export PATH="$PATH":"$AFU"/scripts export CFI="$JSR308"/checker-framework-inference -export CLASSPATH="$JSR308"/immutability/build/classes/main:$CHECKERFRAMEWORK/dataflow/build:$CHECKERFRAMEWORK/javacutil/build:$CHECKERFRAMEWORK/stubparser/build:$CHECKERFRAMEWORK/framework/build:$CHECKERFRAMEWORK/checker/build:$SOLVER/bin:$CHECKERFRAMEWORK/framework/tests/junit-4.12.jar:$CHECKERFRAMEWORK/framework/tests/hamcrest-core-1.3.jar:$CFI/dist/checker-framework-inference.jar:$CFI/dist/org.ow2.sat4j.core-2.3.4.jar:$CFI/dist/commons-logging-1.2.jar:$CFI/dist/log4j-1.2.16.jar:$JSR308/jsr308-langtools/build/classes:$CLASSPATH +export CLASSPATH="$JSR308"/immutability/build/classes/java/main:$CHECKERFRAMEWORK/dataflow/build:$CHECKERFRAMEWORK/javacutil/build:$CHECKERFRAMEWORK/stubparser/build:$CHECKERFRAMEWORK/framework/build:$CHECKERFRAMEWORK/checker/build:$SOLVER/bin:$CHECKERFRAMEWORK/framework/tests/junit-4.12.jar:$CHECKERFRAMEWORK/framework/tests/hamcrest-core-1.3.jar:$CFI/dist/checker-framework-inference.jar:$CFI/dist/org.ow2.sat4j.core-2.3.4.jar:$CFI/dist/commons-logging-1.2.jar:$CFI/dist/log4j-1.2.16.jar:$JSR308/jsr308-langtools/build/classes:$CLASSPATH #parsing build command of the target program build_cmd="$2" @@ -30,8 +30,9 @@ elif [[ "$1" = "-i" ]] ; then rm -rf logs annotated echo "Cleaning Done." CHECKER="pico.inference.PICOInferenceChecker" +# SOLVER="checkers.inference.solver.DebugSolver" SOLVER="pico.inference.solver.PICOSolverEngine" - running_cmd="python $DLJC/dljc -t inference --checker "${CHECKER}" --cfArgs=\"-AoptimalSolution\" --solver "${SOLVER}" --solverArgs=\"collectStatistic=true,useGraph=false\" --mode ROUNDTRIP -afud $WORKING_DIR/annotated -o logs -- $build_cmd " + running_cmd="python $DLJC/dljc -t inference --checker "${CHECKER}" --cfArgs=\"-AoptimalSolution -Astubs=/home/l82sun/workspace/opprop/immutability/src/main/java/pico/inference/jdk.astub\" --solver "${SOLVER}" --solverArgs=\"collectStatistic=true,useGraph=false\" --guess --stubs="/home/l82sun/workspace/opprop/immutability/src/main/java/pico/inference/jdk.astub" --mode ROUNDTRIP -afud $WORKING_DIR/annotated -o logs -- $build_cmd " else echo "Unknown tool: should be either -t|-i but found: ${1}" exit 1 diff --git a/src/main/java/pico/common/ExtendedViewpointAdapter.java b/src/main/java/pico/common/ExtendedViewpointAdapter.java new file mode 100644 index 0000000..a02de53 --- /dev/null +++ b/src/main/java/pico/common/ExtendedViewpointAdapter.java @@ -0,0 +1,11 @@ +package pico.common; + +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.ViewpointAdapter; + +import javax.lang.model.element.AnnotationMirror; + +public interface ExtendedViewpointAdapter extends ViewpointAdapter { + AnnotatedTypeMirror rawCombineAnnotationWithType(AnnotationMirror anno, AnnotatedTypeMirror type); + AnnotationMirror rawCombineAnnotationWithAnnotation(AnnotationMirror anno, AnnotationMirror type); +} diff --git a/src/main/java/pico/typecheck/PICOTypeUtil.java b/src/main/java/pico/common/PICOTypeUtil.java similarity index 79% rename from src/main/java/pico/typecheck/PICOTypeUtil.java rename to src/main/java/pico/common/PICOTypeUtil.java index abaff17..ddbc296 100644 --- a/src/main/java/pico/typecheck/PICOTypeUtil.java +++ b/src/main/java/pico/common/PICOTypeUtil.java @@ -1,4 +1,4 @@ -package pico.typecheck; +package pico.common; import checkers.inference.InferenceMain; import checkers.inference.SlotManager; @@ -6,15 +6,16 @@ import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; import checkers.inference.util.InferenceUtil; -import com.sun.source.tree.AssignmentTree; 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 org.checkerframework.framework.qual.ImplicitFor; +import com.sun.tools.javac.code.Symbol; +import org.checkerframework.framework.qual.DefaultFor; import org.checkerframework.framework.qual.TypeKind; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -23,9 +24,12 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TypesUtils; +import pico.typecheck.PICOVisitor; import qual.Assignable; import qual.Immutable; import qual.ObjectIdentityMethod; @@ -41,10 +45,12 @@ import javax.lang.model.type.TypeMirror; import java.util.ArrayList; import java.util.Arrays; +import java.util.Collections; 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 static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; @@ -64,27 +70,27 @@ public class PICOTypeUtil { sideEffectingUnaryOperators.add(Tree.Kind.PREFIX_DECREMENT); } - private static boolean isInTypesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) { - ImplicitFor implicitFor = Immutable.class.getAnnotation(ImplicitFor.class); - assert implicitFor != null; - assert implicitFor.types() != null; - for (TypeKind typeKind : implicitFor.types()) { - if (typeKind.name() == atm.getKind().name()) return true; + 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; } - private static boolean isInTypeNamesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) { - if (atm.getKind().name() != TypeKind.DECLARED.name()) { + private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { + if (!atm.getKind().name().equals(TypeKind.DECLARED.name())) { return false; } - ImplicitFor implicitFor = Immutable.class.getAnnotation(ImplicitFor.class); - assert implicitFor != null; - assert implicitFor.typeNames() != null; - Class[] typeNames = implicitFor.typeNames(); + DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + Class[] types = defaultFor.types(); String fqn = TypesUtils.getQualifiedName((DeclaredType) atm.getUnderlyingType()).toString(); - for (int i = 0; i < typeNames.length; i++) { - if (typeNames[i].getCanonicalName().toString().contentEquals(fqn)) return true; + for (Class type : types) { + if (type.getCanonicalName().contentEquals(fqn)) { + return true; + } } return false; } @@ -92,9 +98,8 @@ private static boolean isInTypeNamesOfImplicitForOfImmutable(AnnotatedTypeMirror /**Method to determine if the underlying type is implicitly immutable. This method is consistent * with the types and typeNames that are in @ImplicitFor in the definition of @Immutable qualifier*/ public static boolean isImplicitlyImmutableType(AnnotatedTypeMirror atm) { - return isInTypesOfImplicitForOfImmutable(atm) - || isInTypeNamesOfImplicitForOfImmutable(atm) - || isEnumOrEnumConstant(atm); + return isInTypeKindsOfDefaultForOfImmutable(atm) + || isInTypesOfDefaultForOfImmutable(atm); } /** @@ -115,12 +120,12 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree if (node instanceof MethodTree) { MethodTree methodTree = (MethodTree) node; ExecutableElement element = TreeUtils.elementFromDeclaration(methodTree); - typeElement = ElementUtils.enclosingClass(element); + 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.enclosingClass(variableElement); + typeElement = ElementUtils.enclosingTypeElement(variableElement); } if (typeElement != null) { @@ -131,7 +136,7 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree } public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Element element, AnnotatedTypeFactory atypeFactory) { - TypeElement typeElement = ElementUtils.enclosingClass(element); + TypeElement typeElement = ElementUtils.enclosingTypeElement(element); if (typeElement != null) { return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); } @@ -152,7 +157,7 @@ public static List getBoundTypesOfDirectSuperTypes(TypeEl supertypecls = null; } - if (supertypecls != null && supertypecls.getKind().name() != TypeKind.NONE.name()) { + if (supertypecls != null && !supertypecls.getKind().name().equals(TypeKind.NONE.name())) { TypeElement supercls = (TypeElement) ((DeclaredType) supertypecls).asElement(); boundsOfSupers.add(getBoundTypeOfTypeDeclaration(supercls, atypeFactory)); } @@ -187,6 +192,10 @@ public static AnnotatedDeclaredType getBoundTypeOfTypeDeclaration(TypeElement ty // places, at some time. } + public static AnnotatedDeclaredType getBoundTypeOfTypeDeclaration(TypeMirror typeMirror, AnnotatedTypeFactory atypeFactory) { + return getBoundTypeOfTypeDeclaration(TypesUtils.getTypeElement(typeMirror), atypeFactory); + } + public static boolean isObjectIdentityMethod(MethodTree node, AnnotatedTypeFactory annotatedTypeFactory) { Element element = TreeUtils.elementFromTree(node); @@ -244,6 +253,17 @@ public static void addDefaultForField(AnnotatedTypeFactory annotatedTypeFactory, if (explicitATM instanceof AnnotatedDeclaredType) { AnnotatedDeclaredType adt = (AnnotatedDeclaredType) explicitATM; Element typeElement = adt.getUnderlyingType().asElement(); + + // add RDM if bound=M and enclosingBound=M/RDM + Set enclosingBound = annotatedTypeFactory.getTypeDeclarationBounds( + Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()); + Set declBound = annotatedTypeFactory.getTypeDeclarationBounds(element.asType()); + if (AnnotationUtils.containsSameByName(declBound, MUTABLE)) { + if (AnnotationUtils.containsSameByName(enclosingBound, RECEIVER_DEPENDANT_MUTABLE) || + AnnotationUtils.containsSameByName(enclosingBound, MUTABLE)) { + annotatedTypeMirror.replaceAnnotation(RECEIVER_DEPENDANT_MUTABLE); + } + } if (typeElement instanceof TypeElement) { AnnotatedDeclaredType bound = getBoundTypeOfTypeDeclaration((TypeElement) typeElement, annotatedTypeFactory); if (bound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { @@ -292,7 +312,7 @@ public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am) // Might be null. It's normal. In typechecking side, we use addMissingAnnotations(). Only if // there is existing annotation in code, then here is non-null. Otherwise, VariableAnnotator // hasn't come into the picture yet, so no VarAnnot exists here, which is normal. - Slot shouldBeAppliedTo = slotManager.getVariableSlot(type); + Slot shouldBeAppliedTo = slotManager.getSlot(type); ConstantSlot constant = slotManager.createConstantSlot(am); if (shouldBeAppliedTo == null) { // Here, we are adding VarAnnot that represents @Immutable. There won't be solution for this ConstantSlot for this type, @@ -301,7 +321,7 @@ public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am) // back to the original source code, BUT this ConstantSlot(representing @Immutable) will be used for constraint generation // that affects the solutions for other VariableSlots type.addAnnotation(slotManager.getAnnotation(constant));// Insert Constant VarAnnot that represents @Immutable - type.addAnnotation(am);// Insert real @Immutable. This should be removed if INF-FR only uses VarAnnot +// type.addAnnotation(am);// Insert real @Immutable. This should be removed if INF-FR only uses VarAnnot } else { constraintManager.addEqualityConstraint(shouldBeAppliedTo, constant); } @@ -309,13 +329,13 @@ public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am) /**Check if a field is final or not.*/ public static boolean isFinalField(Element variableElement) { - assert variableElement instanceof VariableElement; + assert variableElement instanceof VariableElement; // FIXME consider rm return ElementUtils.isFinal(variableElement); } /**Check if a field is assignable or not.*/ public static boolean isAssignableField(Element variableElement, AnnotationProvider provider) { - if (!(variableElement instanceof VariableElement)) { + if (!(variableElement instanceof VariableElement)) { // FIXME consider rm return false; } boolean hasExplicitAssignableAnnotation = provider.getDeclAnnotation(variableElement, Assignable.class) != null; @@ -361,7 +381,7 @@ public static boolean isAssigningAssignableField(ExpressionTree node, Annotation public static boolean isEnclosedByAnonymousClass(Tree tree, AnnotatedTypeFactory atypeFactory) { TreePath path = atypeFactory.getPath(tree); if (path != null) { - ClassTree classTree = TreeUtils.enclosingClass(path); + ClassTree classTree = TreePathUtil.enclosingClass(path); return classTree != null && InferenceUtil.isAnonymousClass(classTree); } return false; @@ -373,7 +393,7 @@ public static AnnotatedDeclaredType getBoundOfEnclosingAnonymousClass(Tree tree, return null; } AnnotatedDeclaredType enclosingType = null; - Tree newclassTree = TreeUtils.enclosingOfKind(path, Tree.Kind.NEW_CLASS); + Tree newclassTree = TreePathUtil.enclosingOfKind(path, Tree.Kind.NEW_CLASS); if (newclassTree != null) { enclosingType = (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(newclassTree); } @@ -388,10 +408,10 @@ public static AnnotationMirror createEquivalentVarAnnotOfRealQualifier(final Ann public static boolean inStaticScope(TreePath treePath) { boolean in = false; - if (TreeUtils.isTreeInStaticScope(treePath)) { + if (TreePathUtil.isTreeInStaticScope(treePath)) { in = true; // Exclude case in which enclosing class is static - ClassTree classTree = TreeUtils.enclosingClass(treePath); + ClassTree classTree = TreePathUtil.enclosingClass(treePath); if (classTree != null && classTree.getModifiers().getFlags().contains((Modifier.STATIC))) { in = false; } @@ -399,35 +419,44 @@ public static boolean inStaticScope(TreePath treePath) { return in; } - public static void dragAnnotationFromBoundToExtendsAndImplements(Tree node, - AnnotatedTypeMirror annotatedTypeMirror, - AnnotatedTypeFactory atypeFactory) { - boolean onExtendsOrImplements = false; - ClassTree classTree = null; - TreePath path = atypeFactory.getPath(node); - if (path != null) { - final TreePath parentPath = path.getParentPath(); - if (parentPath != null) { - final Tree parentNode = parentPath.getLeaf(); - if (TreeUtils.isClassTree(parentNode)) { - onExtendsOrImplements = true; - classTree = (ClassTree) parentNode; - } - } - } + public static boolean isSideEffectingUnaryTree(final UnaryTree tree) { + return sideEffectingUnaryOperators.contains(tree.getKind()); + } - if (onExtendsOrImplements) { - // Respect explicitly written annotation still. However, if the there is annotation here, but it's - // inheritted from type element bound, then we still flush them out, because they are not explicit - // usage. - if (annotatedTypeMirror.getExplicitAnnotations().isEmpty()) { - annotatedTypeMirror.replaceAnnotation( - getBoundTypeOfTypeDeclaration(classTree, atypeFactory).getAnnotationInHierarchy(READONLY)); - } - } + /** + * !! 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; } - public static boolean isSideEffectingUnaryTree(final UnaryTree tree) { - return sideEffectingUnaryOperators.contains(tree.getKind()); + /** + * !! 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; } } diff --git a/src/main/java/pico/common/ViewpointAdapterGettable.java b/src/main/java/pico/common/ViewpointAdapterGettable.java new file mode 100644 index 0000000..70ed93a --- /dev/null +++ b/src/main/java/pico/common/ViewpointAdapterGettable.java @@ -0,0 +1,5 @@ +package pico.common; + +public interface ViewpointAdapterGettable { + ExtendedViewpointAdapter getViewpointAdapter(); +} diff --git a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index 386a4de..8106066 100644 --- a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java @@ -11,6 +11,7 @@ import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ClassTree; 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.Tree; @@ -20,24 +21,36 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator; +import org.checkerframework.framework.type.ViewpointAdapter; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; import org.checkerframework.framework.type.typeannotator.TypeAnnotator; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator; -import pico.typecheck.PICOTypeUtil; +import org.checkerframework.javacutil.TreePathUtil; +import pico.common.ExtendedViewpointAdapter; +import pico.common.ViewpointAdapterGettable; +import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator; +import pico.common.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.type.DeclaredType; +import javax.lang.model.type.PrimitiveType; import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; import java.util.Collection; +import java.util.Collections; +import java.util.Set; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; +import static pico.typecheck.PICOAnnotationMirrorHolder.*; +import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; /** * Propagates correct constraints on trees and types using TreeAnnotators and TypeAnnotators. @@ -47,7 +60,7 @@ * type on that type. This ensures that that VariableSlot doesn't enter solver and solver doesn't * give solution to the VariableSlot, and there won't be annotations inserted to implicit locations. */ -public class PICOInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory { +public class PICOInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory implements ViewpointAdapterGettable { public PICOInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, boolean withCombineConstraints, BaseAnnotatedTypeFactory realTypeFactory, InferrableChecker realChecker, SlotManager slotManager, ConstraintManager constraintManager) { super(inferenceChecker, withCombineConstraints, realTypeFactory, realChecker, slotManager, constraintManager); // Always call postInit() at the end of ATF constructor! @@ -62,17 +75,17 @@ public PICOInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, bool // be inserted results anyway). @Override public TreeAnnotator createTreeAnnotator() { - return new ListTreeAnnotator(new ImplicitsTreeAnnotator(this), + return new ListTreeAnnotator(new LiteralTreeAnnotator(this), new PICOInferencePropagationTreeAnnotator(this), new InferenceTreeAnnotator(this, realChecker, realTypeFactory, variableAnnotator, slotManager)); } @Override protected TypeAnnotator createTypeAnnotator() { - // Reuse PICOImplicitsTypeAnnotator even in inference mode. Because the type annotator's implementation + // Reuse PICODefaultForTypeAnnotator even in inference mode. Because the type annotator's implementation // are the same. The only drawback is that naming is not good(doesn't include "Inference"), thus may be // hard to debug - return new ListTypeAnnotator(super.createTypeAnnotator(), new PICOImplicitsTypeAnnotator(this)); + return new ListTypeAnnotator(super.createTypeAnnotator(), new PICODefaultForTypeAnnotator(this)); } @Override @@ -102,7 +115,7 @@ VariableAnnotator getVariableAnnotator() { */ public AnnotatedDeclaredType getSelfType(Tree tree) { TreePath path = getPath(tree); - ClassTree enclosingClass = TreeUtils.enclosingClass(path); + ClassTree enclosingClass = TreePathUtil.enclosingClass(path); if (enclosingClass == null) { // I hope this only happens when tree is a fake tree that // we created, e.g. when desugaring enhanced-for-loops. @@ -111,7 +124,7 @@ public AnnotatedDeclaredType getSelfType(Tree tree) { // "type" is right now VarAnnot inserted to the bound of "enclosingClass" AnnotatedDeclaredType type = getAnnotatedType(enclosingClass); - MethodTree enclosingMethod = TreeUtils.enclosingMethod(path); + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(path); if (enclosingClass.getSimpleName().length() != 0 && enclosingMethod != null) { AnnotatedTypeMirror.AnnotatedDeclaredType methodReceiver; if (TreeUtils.isConstructor(enclosingMethod)) { @@ -129,11 +142,77 @@ public AnnotatedDeclaredType getSelfType(Tree tree) { return type; } + @Override + public ExtendedViewpointAdapter getViewpointAdapter() { + return (ExtendedViewpointAdapter) viewpointAdapter; + } + + @Override + protected Set getDefaultTypeDeclarationBounds() { + return Collections.singleton(MUTABLE); + } + + @Override + public Set getTypeDeclarationBounds(TypeMirror type) { + // Get the VarAnnot on the class decl + // This factory is only invoked on inference, so no need to provide concrete anno for type-check + if (type instanceof PrimitiveType) { + return Collections.singleton(slotManager.getAnnotation(slotManager.getSlot(IMMUTABLE))); + } + if (type.getKind() == TypeKind.ARRAY) { + // WORKAROUND: return RDM will cause issues with new clauses + return Collections.singleton(slotManager.getAnnotation(slotManager.getSlot(READONLY))); + } +// AnnotatedTypeMirror atm = toAnnotatedType(type, true); +// if (atm instanceof AnnotatedDeclaredType && ((AnnotatedDeclaredType) atm).getTypeArguments().size() > 0) { +// // Workaround for types with type arguments. +// // annotateElementFromStore can only get the original type with type param. +// // But this method only needs the top annotation. +// // Note: class bound cache is a private field of annotator. +// +// atm = PICOTypeUtil.getBoundTypeOfTypeDeclaration(TypesUtils.getTypeElement(type), this); +// } else { +// getVariableAnnotator().annotateElementFromStore(getProcessingEnv().getTypeUtils().asElement(type), atm); +// } +// +// if (atm.hasAnnotation(VarAnnot.class)) { +// return atm.getAnnotations(); +// } + AnnotationMirror am = ((PICOVariableAnnotator) variableAnnotator).getClassDeclAnno(getProcessingEnv().getTypeUtils().asElement(type)); + if (am != null) { + return Collections.singleton(am); + } + + // if reaching this point and still no anno: not annotated from slot manager + // maybe should read from stub file. + // if implicit: return immutable slot + + // implicit + if (PICOTypeUtil.isImplicitlyImmutableType(toAnnotatedType(type, false))) { + return Collections.singleton(slotManager.getAnnotation(slotManager.getSlot(IMMUTABLE))); + } + + // get stub & default from element. +// return stubTypes.getAnnotatedTypeMirror(TypesUtils.getTypeElement(type)).getAnnotations(); + return Collections.singleton( + slotManager.getAnnotation(slotManager.getSlot(super.getTypeDeclarationBounds(type).iterator().next()))); + } + class PICOInferencePropagationTreeAnnotator extends PropagationTreeAnnotator { public PICOInferencePropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); } + @Override + public Void visitMethodInvocation(MethodInvocationTree methodInvocationTree, AnnotatedTypeMirror mirror) { + // This is a workaround for implicit types. + // Implicit types in lib method get defaulted to mutable. + // Implicit immutable classes cannot be annotated in stub files, annotations were ignored. + // Find the cause, annotate implicit immutable classes in stub, and remove this method. + applyImmutableIfImplicitlyImmutable(mirror); + return super.visitMethodInvocation(methodInvocationTree, mirror); + } + @Override public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { // Below is copied from super @@ -214,6 +293,10 @@ public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { return null; // Above is copied from super + + // We have a problem with the annotation. + // During inference it get defaulted annotation for component types inside dataflow and cache that. + // The assignment context have only constant slots. } /**Add immutable to the result type of a binary operation if the result type is implicitly immutable*/ @@ -235,7 +318,7 @@ public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { return super.visitTypeCast(node, type); } - /**Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are not guaranteed + /**Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are not guaranteed to always have immutable annotation. If this happens, we manually add immutable to type. */ private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) { if (PICOTypeUtil.isImplicitlyImmutableType(type)) { diff --git a/src/main/java/pico/inference/PICOInferenceChecker.java b/src/main/java/pico/inference/PICOInferenceChecker.java index d211fab..75915fc 100644 --- a/src/main/java/pico/inference/PICOInferenceChecker.java +++ b/src/main/java/pico/inference/PICOInferenceChecker.java @@ -1,11 +1,6 @@ package pico.inference; -import checkers.inference.BaseInferrableChecker; -import checkers.inference.InferenceAnnotatedTypeFactory; -import checkers.inference.InferenceChecker; -import checkers.inference.InferenceVisitor; -import checkers.inference.InferrableChecker; -import checkers.inference.SlotManager; +import checkers.inference.*; import checkers.inference.model.ConstraintManager; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.source.SupportedOptions; @@ -14,7 +9,7 @@ /** * Main entry class */ -@SupportedOptions({"upcast", "anycast", "comparablecast", "optimalSolution"}) +@SupportedOptions({"upcast", "anycast", "comparablecast", "optimalSolution", "useOptimisticUncheckedDefaults"}) public class PICOInferenceChecker extends BaseInferrableChecker { @Override @@ -24,7 +19,7 @@ public void initChecker() { } @Override - public BaseAnnotatedTypeFactory createRealTypeFactory() { + public BaseInferenceRealTypeFactory createRealTypeFactory(boolean infer) { return new PICOInferenceRealTypeFactory(this, true); } diff --git a/src/main/java/pico/inference/PICOInferenceExtendedViewpointAdapter.java b/src/main/java/pico/inference/PICOInferenceExtendedViewpointAdapter.java new file mode 100644 index 0000000..3df3cd5 --- /dev/null +++ b/src/main/java/pico/inference/PICOInferenceExtendedViewpointAdapter.java @@ -0,0 +1,37 @@ +package pico.inference; + +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import pico.common.ExtendedViewpointAdapter; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; + +public class PICOInferenceExtendedViewpointAdapter extends PICOInferenceViewpointAdapter implements ExtendedViewpointAdapter { + + public PICOInferenceExtendedViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + /** + * (Extended behaviour) viewpoint adapt super clause to its class declaration. Class declaration acts like receiver. + * @param classType class declaration itself + * @param superEle element of extends / implements clause + * @param superType type of extends / implements clause + */ + public void viewpointAdaptSuperClause(AnnotatedTypeMirror.AnnotatedDeclaredType classType, Element superEle, AnnotatedTypeMirror.AnnotatedDeclaredType superType) { +// AnnotatedTypeMirror adapted = combineTypeWithType(classType, superType); + AnnotationMirror adapted = combineAnnotationWithAnnotation(extractAnnotationMirror(classType), extractAnnotationMirror(superType)); + superType.replaceAnnotation(adapted); + + } + + public AnnotatedTypeMirror rawCombineAnnotationWithType(AnnotationMirror anno, AnnotatedTypeMirror type) { + return combineAnnotationWithType(anno, type); + } + + @Override + public AnnotationMirror rawCombineAnnotationWithAnnotation(AnnotationMirror anno, AnnotationMirror type) { + return combineAnnotationWithAnnotation(anno, type); + } +} diff --git a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index 1157e2d..248346b 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -1,48 +1,56 @@ package pico.inference; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; - 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.type.DeclaredType; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; +import javax.lang.model.util.Elements; +import checkers.inference.BaseInferenceRealTypeFactory; +import com.sun.tools.javac.tree.JCTree; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.RelevantJavaTypes; +import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AbstractViewpointAdapter; import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; -import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.PropagationTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.TypeAnnotator; +import org.checkerframework.framework.type.typeannotator.*; +import org.checkerframework.framework.util.defaults.QualifierDefaults; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import com.sun.source.tree.Tree; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOTreeAnnotator; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator; -import pico.typecheck.PICOTypeUtil; +import pico.common.ExtendedViewpointAdapter; +import pico.common.ViewpointAdapterGettable; +import pico.typecheck.PICOAnnotatedTypeFactory; +import pico.common.PICOTypeUtil; import pico.typecheck.PICOViewpointAdapter; import qual.Bottom; import qual.Immutable; import qual.Mutable; +import qual.PolyMutable; import qual.Readonly; import qual.ReceiverDependantMutable; +import static pico.typecheck.PICOAnnotationMirrorHolder.*; + /** * PICOInferenceRealTypeFactory exists because: 1)PICOAnnotatedTypeFactory is not subtype of * BaseAnnotatedTypeFactory. 2) In inference side, PICO only supports reduced version of @@ -51,11 +59,19 @@ * to InitializationAnnotatedTypeFactory as if there is only one mutability qualifier hierarchy. * This class has lots of copied code from PICOAnnotatedTypeFactory. The two should be in sync. */ -public class PICOInferenceRealTypeFactory extends BaseAnnotatedTypeFactory { +public class PICOInferenceRealTypeFactory extends BaseInferenceRealTypeFactory implements ViewpointAdapterGettable { + + private static final List IMMUTABLE_ALIASES = Arrays.asList( + "com.google.errorprone.annotations.Immutable", + "edu.cmu.cs.glacier.qual.Immutable"); public PICOInferenceRealTypeFactory(BaseTypeChecker checker, boolean useFlow) { super(checker, useFlow); - addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + if (READONLY != null) { + addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + } +// IMMUTABLE_ALIASES.forEach(anno -> addAliasedAnnotation(anno, IMMUTABLE)); + postInit(); } @@ -64,6 +80,7 @@ public PICOInferenceRealTypeFactory(BaseTypeChecker checker, boolean useFlow) { protected Set> createSupportedTypeQualifiers() { return new LinkedHashSet>( Arrays.asList( + PolyMutable.class, Readonly.class, Mutable.class, ReceiverDependantMutable.class, @@ -81,9 +98,10 @@ protected AbstractViewpointAdapter createViewpointAdapter() { @Override protected TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new PICOPropagationTreeAnnotator(this), - new ImplicitsTreeAnnotator(this), - new PICOTreeAnnotator(this)); + new PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator(this), + new LiteralTreeAnnotator(this), + new PICOAnnotatedTypeFactory.PICOSuperClauseAnnotator(this), + new PICOAnnotatedTypeFactory.PICOTreeAnnotator(this)); } // TODO Refactor super class to remove this duplicate code @@ -99,19 +117,43 @@ protected TypeAnnotator createTypeAnnotator() { // annotated. typeAnnotators.add( new IrrelevantTypeAnnotator( - this, getQualifierHierarchy().getTopAnnotations(), classes)); + this, getQualifierHierarchy().getTopAnnotations())); } typeAnnotators.add(new PropagationTypeAnnotator(this)); /*Copied code ends*/ // 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 - typeAnnotators.add(new PICOTypeAnnotator(this)); - typeAnnotators.add(new PICOImplicitsTypeAnnotator(this)); + typeAnnotators.add(new PICOAnnotatedTypeFactory.PICOTypeAnnotator(this)); + typeAnnotators.add(new PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator(this)); + typeAnnotators.add(new PICOAnnotatedTypeFactory.PICOEnumDefaultAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } - /** TODO If the dataflow refines the type as bottom, should we allow such a refinement? If we allow it, + @Override + protected QualifierDefaults createQualifierDefaults() { + QualifierDefaults defaults = super.createQualifierDefaults(); + Elements elements = checker.getElementUtils(); + + // The optimistic flag only change the rules of unchecked defaults. + // To enable optimistic default, the user should both enable conservative for bytecode ONLY, + // and pass the optimistic flag to override the default of the conservative. + // i.e. -AuseConservativeDefaultsForUncheckedCode=bytecode (or -AuseDefaultsForUncheckedCode=bytecode) + // -AuseOptimisticUncheckedDefaults + if (checker.hasOption("useOptimisticUncheckedDefaults")) { + defaults.addUncheckedCodeDefaults(AnnotationBuilder.fromClass(elements, Bottom.class), new TypeUseLocation[]{ + TypeUseLocation.LOWER_BOUND, TypeUseLocation.RETURN, TypeUseLocation.FIELD + }); + defaults.addUncheckedCodeDefaults(AnnotationBuilder.fromClass(elements, Readonly.class), new TypeUseLocation[]{ + TypeUseLocation.UPPER_BOUND, TypeUseLocation.PARAMETER + }); + } + + return defaults; + + } + + /* TODO If the dataflow refines the type as bottom, should we allow such a refinement? If we allow it, PICOValidator will give an error if it begins to enforce @Bottom is not used*/ /* @Override protected void applyInferredAnnotations(AnnotatedTypeMirror type, PICOValue as) { @@ -125,26 +167,11 @@ public boolean getShouldDefaultTypeVarLocals() { return false; } - // Copied from PICOAnnotatedTypeFactory - @Override - protected void annotateInheritedFromClass(AnnotatedTypeMirror type, Set fromClass) { - // If interitted from class element is @Mutable or @Immutable, then apply this annotation to the usage type - if (fromClass.contains(MUTABLE) || fromClass.contains(IMMUTABLE)) { - super.annotateInheritedFromClass(type, fromClass); - return; - } - // If interitted from class element is @ReceiverDependantMutable, then don't apply and wait for @Mutable - // (default qualifier in hierarchy to be applied to the usage type). This is to avoid having @ReceiverDependantMutable - // on type usages as a default behaviour. By default, @Mutable is better used as the type for usages that - // don't have explicit annotation. - return;// Don't add annotations from class element - } - @Override public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { PICOTypeUtil.addDefaultForField(this, type, elt); PICOTypeUtil.defaultConstructorReturnToClassBound(this, elt, type); - PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); +// PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); super.addComputedTypeAnnotations(elt, type); } @@ -181,4 +208,65 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { return result; } + + @Override + protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator() { + return new PICOAnnotatedTypeFactory.PICOQualifierForUseTypeAnnotator(this); + } + + @Override + public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) { + // add default anno from class main qual, if no qual present + AnnotatedTypeMirror enclosing = getAnnotatedType(TreePathUtil.enclosingClass(getPath(clause))); + + // workaround for anonymous class. + // TypesUtils::isAnonymous won't work when annotation presents on new class tree! + // by reaching this line TypesUtils::isAnonymous is already not working: it shouldn't check anonymous class! + if(getPath(clause).getParentPath().getLeaf() instanceof JCTree.JCNewClass) { + enclosing = getAnnotatedType(getPath(clause).getParentPath().getLeaf()); + + } + AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY); + AnnotatedTypeMirror fromTypeTree = this.getAnnotatedTypeFromTypeTree(clause); + if (!fromTypeTree.isAnnotatedInHierarchy(READONLY)) { + fromTypeTree.addAnnotation(mainBound); + } + + // for FBC quals +// Set bound = this.getTypeDeclarationBounds(fromTypeTree.getUnderlyingType()); +// fromTypeTree.addMissingAnnotations(bound); + return fromTypeTree; + } + + public ExtendedViewpointAdapter getViewpointAdapter() { + return (ExtendedViewpointAdapter) viewpointAdapter; + } + + @Override + protected Set getDefaultTypeDeclarationBounds() { + return Collections.singleton(MUTABLE); + } + + @Override + public Set getTypeDeclarationBounds(TypeMirror type) { + // TODO too awkward. maybe overload isImplicitlyImmutableType + if (PICOTypeUtil.isImplicitlyImmutableType(toAnnotatedType(type, false))) { + return Collections.singleton(IMMUTABLE); + } + if (type.getKind() == TypeKind.ARRAY) { + return Collections.singleton(READONLY); // 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) { + if (!AnnotationUtils.containsSameByName(getDeclAnnotations(ele), MUTABLE) && + !AnnotationUtils.containsSameByName(getDeclAnnotations(ele), RECEIVER_DEPENDANT_MUTABLE)) { // no decl anno + return Collections.singleton(IMMUTABLE); + } + } + } + return super.getTypeDeclarationBounds(type); + } } diff --git a/src/main/java/pico/inference/PICOInferenceValidator.java b/src/main/java/pico/inference/PICOInferenceValidator.java index 7f6bc09..5460a39 100644 --- a/src/main/java/pico/inference/PICOInferenceValidator.java +++ b/src/main/java/pico/inference/PICOInferenceValidator.java @@ -5,23 +5,20 @@ import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.source.Result; 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.TreeUtils; -import pico.typecheck.PICOTypeUtil; +import pico.common.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.VariableElement; -import static pico.typecheck.PICOAnnotationMirrorHolder.BOTTOM; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; -import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; +import java.util.Set; + +import static pico.typecheck.PICOAnnotationMirrorHolder.*; /** * Generates constraints based on PICO constraint-based well-formedness rules in infer mode. @@ -37,6 +34,19 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { checkStaticReceiverDependantMutableError(type, tree); checkImplicitlyImmutableTypeError(type, tree); checkOnlyOneAssignabilityModifierOnField(tree); +// AnnotatedDeclaredType defaultType = +// (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(type.getUnderlyingType().asElement()); +// // TODO for defaulted super clause: should top anno be checked? (see shouldCheckTopLevelDeclaredOrPrimitiveType()) +// if (defaultType.getAnnotationInHierarchy(READONLY) == null && !PICOTypeUtil.isEnumOrEnumConstant(defaultType)) { +// defaultType = defaultType.deepCopy(); +// defaultType.replaceAnnotation(MUTABLE); +// } +// +// if (!visitor.isValidUse(defaultType, type, tree)) { +// reportInvalidAnnotationsOnUse(type, tree); +// } + // main != READONLY -> main |> bound <: main + ((PICOInferenceVisitor) visitor).mainCannotInferTo(type, POLY_MUTABLE, "cannot.infer.poly", tree); return super.visitDeclared(type, tree); } @@ -52,15 +62,27 @@ public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) { return super.visitPrimitive(type, tree); } + @Override + protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(AnnotatedTypeMirror type, Tree tree) { + if (TreeUtils.isLocalVariable(tree)) { + return true; + } + return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree); + } + private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) { - if (PICOTypeUtil.inStaticScope(visitor.getCurrentPath())) { - if (infer) { - ((PICOInferenceVisitor)visitor).mainIsNot(type, RECEIVER_DEPENDANT_MUTABLE, "static.receiverdependantmutable.forbidden", tree); - } else { - if (type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { - reportValidityResult("static.receiverdependantmutable.forbidden", type, tree); - } - } + // Static inner class is considered within the static scope. + // Added condition to ensure not class decl. + if (PICOTypeUtil.inStaticScope(visitor.getCurrentPath()) && !type.isDeclaration()) { +// if (infer) { +// ((PICOInferenceVisitor)visitor).mainIsNot(type, RECEIVER_DEPENDANT_MUTABLE, "static.receiverdependantmutable.forbidden", tree); +// } else { +// if (type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { +// reportValidityResult("static.receiverdependantmutable.forbidden", type, tree); +// } +// } + ((InferenceVisitor)visitor).mainIsNot(type, RECEIVER_DEPENDANT_MUTABLE, "static.receiverdependantmutable.forbidden", tree); + // TODO set isValid or move to visitor } } @@ -73,7 +95,8 @@ private void checkImplicitlyImmutableTypeError(AnnotatedTypeMirror type, Tree tr new AnnotationMirror[]{READONLY, MUTABLE, RECEIVER_DEPENDANT_MUTABLE, BOTTOM}, "type.invalid.annotations.on.use", tree); } else { - if (!type.hasAnnotation(IMMUTABLE)) { + // FIXME workaround for typecheck. How should inference handle BOTTOM? + if (!type.hasAnnotation(IMMUTABLE) && !type.hasAnnotation(BOTTOM)) { reportInvalidAnnotationsOnUse(type, tree); } } @@ -97,7 +120,20 @@ private void checkOnlyOneAssignabilityModifierOnField(Tree tree) { } private void reportFieldMultipleAssignabilityModifiersError(VariableElement field) { - checker.report(Result.failure("one.assignability.invalid", field), field); + checker.reportError(field, "one.assignability.invalid", field); isValid = false; } + + private void checkLocalVariableDefaults(AnnotatedDeclaredType type, Tree tree) { + Set bounds = + atypeFactory.getTypeDeclarationBounds(type.getUnderlyingType()); + + AnnotatedDeclaredType elemType = type.deepCopy(); + elemType.clearAnnotations(); + elemType.addAnnotations(bounds); + + if (!visitor.isValidUse(elemType, type, tree)) { + reportInvalidAnnotationsOnUse(type, tree); + } + } } diff --git a/src/main/java/pico/inference/PICOInferenceViewpointAdapter.java b/src/main/java/pico/inference/PICOInferenceViewpointAdapter.java index 9386d88..38a7fda 100644 --- a/src/main/java/pico/inference/PICOInferenceViewpointAdapter.java +++ b/src/main/java/pico/inference/PICOInferenceViewpointAdapter.java @@ -1,15 +1,18 @@ package pico.inference; +import checkers.inference.InferenceMain; import checkers.inference.util.InferenceViewpointAdapter; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; -import pico.typecheck.PICOTypeUtil; +import pico.common.ExtendedViewpointAdapter; +import pico.common.PICOTypeUtil; +import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.type.TypeKind; -public class PICOInferenceViewpointAdapter extends InferenceViewpointAdapter{ +public class PICOInferenceViewpointAdapter extends InferenceViewpointAdapter implements ExtendedViewpointAdapter { public PICOInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); @@ -28,6 +31,33 @@ protected AnnotatedTypeMirror combineAnnotationWithType(AnnotationMirror receive if (PICOTypeUtil.isImplicitlyImmutableType(declared)) { return declared; } + // workaround + if (InferenceMain.isHackMode()) { + if (extractAnnotationMirror(declared) == null) { + return declared; + } + } + return super.combineAnnotationWithType(receiverAnnotation, declared); } + + @Override + public AnnotatedTypeMirror rawCombineAnnotationWithType(AnnotationMirror anno, AnnotatedTypeMirror type) { + return combineAnnotationWithType(anno, type); + } + + @Override + public AnnotationMirror rawCombineAnnotationWithAnnotation(AnnotationMirror anno, AnnotationMirror type) { + return rawCombineAnnotationWithAnnotation(anno, type); + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + // since the introduction of vp-is-valid rules, real am may be used? + AnnotationMirror am = super.extractAnnotationMirror(atm); + if (am == null) { // if failed, try to get real am + am = atm.getAnnotationInHierarchy(READONLY); + } + return am; + } } diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 0a0d390..0322100 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -1,39 +1,15 @@ package pico.inference; -import static pico.typecheck.PICOAnnotationMirrorHolder.BOTTOM; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; -import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; - -import java.util.Arrays; -import java.util.HashSet; -import java.util.Iterator; -import java.util.List; -import java.util.Map; -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.ExecutableElement; -import javax.lang.model.element.TypeElement; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeKind; - -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.framework.source.Result; -import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedMethodType; -import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.util.AnnotatedTypes; -import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.BugInCF; -import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.Pair; -import org.checkerframework.javacutil.TreeUtils; - +import checkers.inference.InferenceChecker; +import checkers.inference.InferenceMain; +import checkers.inference.InferenceValidator; +import checkers.inference.InferenceVisitor; +import checkers.inference.SlotManager; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.Constraint; +import checkers.inference.model.ConstraintManager; +import checkers.inference.model.Slot; +import checkers.inference.qual.VarAnnot; import com.sun.source.tree.AnnotationTree; import com.sun.source.tree.ArrayAccessTree; import com.sun.source.tree.AssignmentTree; @@ -50,20 +26,39 @@ import com.sun.source.tree.UnaryTree; import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +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.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TypesUtils; +import pico.common.ExtendedViewpointAdapter; +import pico.common.ViewpointAdapterGettable; +import pico.common.PICOTypeUtil; -import checkers.inference.InferenceChecker; -import checkers.inference.InferenceMain; -import checkers.inference.InferenceValidator; -import checkers.inference.InferenceVisitor; -import checkers.inference.SlotManager; -import checkers.inference.model.ConstantSlot; -import checkers.inference.model.Constraint; -import checkers.inference.model.ConstraintManager; -import checkers.inference.model.EqualityConstraint; -import checkers.inference.model.InequalityConstraint; -import checkers.inference.model.Slot; -import checkers.inference.model.SubtypeConstraint; -import pico.typecheck.PICOTypeUtil; +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 java.util.Arrays; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import static pico.typecheck.PICOAnnotationMirrorHolder.*; /** * Generate constraints based on the PICO constraint-based type rules in infer mode. Has typecheck @@ -82,37 +77,112 @@ protected InferenceValidator createTypeValidator() { @Override public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { - if (infer) { - mainIsNot(declarationType, READONLY, "type.invalid.annotations.on.use", tree); - addMutableImmutableRdmIncompatibleConstraints(declarationType, useType); + // FIXME workaround for typecheck BOTTOM + if (useType.hasAnnotation(BOTTOM)) { return true; - } else { - AnnotationMirror declared = declarationType.getAnnotationInHierarchy(READONLY); - if (AnnotationUtils.areSame(declared, RECEIVER_DEPENDANT_MUTABLE)) { - return true; - } - assert AnnotationUtils.areSame(declared, MUTABLE) || AnnotationUtils.areSame(declared, IMMUTABLE); + } - AnnotationMirror used = useType.getAnnotationInHierarchy(READONLY); - if (AnnotationUtils.areSame(declared, MUTABLE) && - !(AnnotationUtils.areSame(used, IMMUTABLE) || AnnotationUtils.areSame(used, RECEIVER_DEPENDANT_MUTABLE))) { - return true; - } + // skip base check during inference + if (infer && !declarationType.hasAnnotation(VarAnnot.class)) { + return true; + } - if (AnnotationUtils.areSame(declared, IMMUTABLE) && - !(AnnotationUtils.areSame(used, MUTABLE) || AnnotationUtils.areSame(used, RECEIVER_DEPENDANT_MUTABLE))) { - return true; + // allow RDM on mutable fields with enclosing class bounded with mutable + if (tree instanceof VariableTree && !useType.isDeclaration()) { + VariableElement element = TreeUtils.elementFromDeclaration((VariableTree)tree); + if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingTypeElement(element) != null) { + // assert only 1 bound exists + AnnotationMirror enclosingBound = + extractVarAnnot(PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(element, atypeFactory)); +// atypeFactory.getTypeDeclarationBounds( +// Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()).iterator().next(); + + // if enclosing bound == mutable -> (RDM or Mutable usable on mutable-bounded fields) + // else -> adaptedSubtype + // would be helpful if the solver is SMT and supports "ite" operation + if (infer) { + final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + + // cannot use RDM on mutable-bounded fields in immutable classes + // for mutable enclosing class: allow RDM/Mutable on mutable-bounded fields + constraintManager.addImplicationConstraint( + Collections.singletonList( // if decl bound is mutable + constraintManager.createEqualityConstraint(slotManager.getSlot(enclosingBound), + slotManager.getSlot(MUTABLE)) + ), + createRDMOnMutableFieldConstraint(useType, extractVarAnnot(declarationType))); + // for other enclosing class: use adaptedSubtype + constraintManager.addImplicationConstraint( + Collections.singletonList( // if decl bound is mutable + constraintManager.createInequalityConstraint(slotManager.getSlot(enclosingBound), + slotManager.getSlot(MUTABLE)) + ), + createAdaptedSubtypeConstraint(useType, declarationType)); + return true; // always proceed on inference + } + // type-check + return AnnotationUtils.areSame(enclosingBound, MUTABLE) ? + ifAnnoIsThenMainIsOneOf(extractVarAnnot(declarationType), MUTABLE, useType, + new AnnotationMirror[]{MUTABLE, RECEIVER_DEPENDANT_MUTABLE}) : + isAdaptedSubtype(useType, declarationType); +// if(declarationType.hasAnnotation(MUTABLE) +// && useType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) +// && AnnotationUtils.containsSameByName(enclosingBound, MUTABLE)) { +// return true; +// } } - return false; } + return isAdaptedSubtype(useType, declarationType); + } + + /** + * constraint: lhs |> rhs <: lhs + * equal to decl:immutable => use:immutable || decl:mutable => use:mutable + * @param lhs left value of adaption, typically use + * @param rhs right value of adaption, typically declaration + * @return true if holds, always true during inference + */ + private boolean isAdaptedSubtype(AnnotatedTypeMirror lhs, AnnotatedTypeMirror rhs) { + if (extractVarAnnot(lhs).equals(extractVarAnnot(rhs))) { + return true; + } + // todo: haifeng we should do the viewpointAdapt in baseTypeValidator.java#visitDeclared 299 function:getTypeDeclarationBounds + ExtendedViewpointAdapter vpa = ((ViewpointAdapterGettable)atypeFactory).getViewpointAdapter(); + AnnotatedTypeMirror adapted = vpa.rawCombineAnnotationWithType(extractVarAnnot(lhs), + rhs); + return mainIsSubtype(adapted, extractVarAnnot(lhs)); + } + + private Constraint createAdaptedSubtypeConstraint(AnnotatedTypeMirror lhs, AnnotatedTypeMirror rhs) { + assert infer; + final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + + ExtendedViewpointAdapter vpa = ((ViewpointAdapterGettable)atypeFactory).getViewpointAdapter(); + AnnotatedTypeMirror adapted = vpa.rawCombineAnnotationWithType(extractVarAnnot(lhs), rhs); + return constraintManager.createSubtypeConstraint( + slotManager.getSlot(adapted), + slotManager.getSlot(lhs) + ); + } + + @Override + public boolean mainIsSubtype(AnnotatedTypeMirror ty, AnnotationMirror mod) { + // TODO push change to cfi + boolean s = super.mainIsSubtype(ty, mod); // execute only once to avoid side-effects + if (!s) { + return atypeFactory.getQualifierHierarchy().isSubtype(ty.getAnnotationInHierarchy(mod), mod); + } + return true; } private void addMutableImmutableRdmIncompatibleConstraints(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType) { final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot declSlot = slotManager.getVariableSlot(declarationType); - Slot useSlot = slotManager.getVariableSlot(useType); + Slot declSlot = slotManager.getSlot(declarationType); + Slot useSlot = slotManager.getSlot(useType); Slot mutable = slotManager.getSlot(MUTABLE); Slot immutable = slotManager.getSlot(IMMUTABLE); Slot rdm = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); @@ -161,24 +231,15 @@ public boolean validateTypeOf(Tree tree) { } return validateType(tree, type); + // extends clause kind = IDENTIFIER. an annotator is added for defaulting } // TODO This might not be correct for infer mode. Maybe returning as it is @Override public boolean validateType(Tree tree, AnnotatedTypeMirror type) { - // basic consistency checks - if (!AnnotatedTypes.isValidType(atypeFactory.getQualifierHierarchy(), type)) { - if (!infer) { - checker.report( - Result.failure("type.invalid", type.getAnnotations(), type.toString()), tree); - return false; - } - } - if (!typeValidator.isValid(type, tree)) { - if (!infer) { + if (!typeValidator.isValid(type, tree)) { // in inference, isValid never return false return false; - } } // The initial purpose of always returning true in validateTypeOf in inference mode // might be that inference we want to generate constraints over all the ast location, @@ -192,25 +253,31 @@ public boolean validateType(Tree tree, AnnotatedTypeMirror type) { } @Override - protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) { + protected void checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) { + AnnotationMirror constructorReturn = extractVarAnnot(constructor.getReturnType()); + mainIsSubtype(invocation, constructorReturn, "constructor.invocation.invalid", newClassTree); + + super.checkConstructorInvocation(invocation, constructor, newClassTree); + } + + private AnnotationMirror extractVarAnnot(final AnnotatedTypeMirror atm) { if (infer) { - AnnotationMirror constructorReturn = extractVarAnnot(constructor.getReturnType()); - mainIsSubtype(invocation, constructorReturn, "constructor.invocation.invalid", newClassTree); - } else { - AnnotatedDeclaredType returnType = (AnnotatedDeclaredType) constructor.getReturnType(); - if (!atypeFactory.getTypeHierarchy().isSubtype(invocation, returnType)) { - checker.report(Result.failure( - "constructor.invocation.invalid", invocation, returnType), newClassTree); - return false; - } + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + return slotManager.getAnnotation(slotManager.getSlot(atm)); } - return super.checkConstructorInvocation(invocation, constructor, newClassTree); + return atm.getAnnotationInHierarchy(READONLY); } - private AnnotationMirror extractVarAnnot(final AnnotatedTypeMirror atm) { - assert infer; - final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - return slotManager.getAnnotation(slotManager.getVariableSlot(atm)); + /** + * Extract the declaration initialization bound of a certain atm. + * Return the slot generated during inference. + * @param atm any AnnotatedDeclaredType + * @return the initialization bound on the class declaration of the type (actual or slot annotation) + */ + private AnnotationMirror extractInitBoundAnno(final AnnotatedDeclaredType atm) { + Element tm = atypeFactory.getProcessingEnv().getTypeUtils().asElement(atm.getUnderlyingType()); + assert tm instanceof TypeElement; + return extractVarAnnot(PICOTypeUtil.getBoundTypeOfTypeDeclaration((TypeElement) tm, atypeFactory)); } @Override @@ -223,13 +290,159 @@ public Void visitVariable(VariableTree node, Void p) { addDeepPreference(type, RECEIVER_DEPENDANT_MUTABLE, 3, node); addDeepPreference(type, IMMUTABLE, 3, node); } + + // if the use is a field and not static, and the bound of the type is mutable: + // allow the use to be rdm or mutable + if (element != null && element.getKind() == ElementKind.FIELD && !ElementUtils.isStatic(element)) { + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(element); + if (type instanceof AnnotatedDeclaredType) { + ifBoundContainsThenMainIsOneOf((AnnotatedDeclaredType) type, MUTABLE, + new AnnotationMirror[]{MUTABLE, RECEIVER_DEPENDANT_MUTABLE}); + } + } + + // Base will skip the rest check if assignment (if presents) get error. + // Make this explicit. + if (element != null && element.getKind() == ElementKind.LOCAL_VARIABLE && node.getInitializer() != null) { + // If not use element, but use the atypeFactory.getAnnotatedTypeLhs, anno will refined to initializer's + // anno even if the use is invalid, such as a @Mutable Immutable local variable. + // This refinement is ignored only here to capture related errors. + AnnotatedTypeMirror useType = atypeFactory.getAnnotatedType(element); + if (useType instanceof AnnotatedDeclaredType) { + AnnotatedTypeMirror boundType = + PICOTypeUtil.getBoundTypeOfTypeDeclaration(useType.getUnderlyingType(), atypeFactory); + if (!isAdaptedSubtype(useType, boundType)) { + checker.reportError(node, "type.invalid.annotations.on.use", useType, boundType); + } + } + } return super.visitVariable(node, p); } + /** + * + * @param mainAtm a field atm + * @param mutBound declaration bound of mutability + * @return (mutBound == RDM) -> (anno(atm) == RDM | anno(atm) == Mutable) + */ + private Constraint createRDMOnMutableFieldConstraint(AnnotatedTypeMirror mainAtm, AnnotationMirror mutBound) { + final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + + Constraint oneOfConst = createMainIsMutableOrRdmConstraint(mainAtm); + + return constraintManager.createImplicationConstraint( + Collections.singletonList(constraintManager.createEqualityConstraint( + slotManager.getSlot(mutBound), + slotManager.getSlot(MUTABLE))), + oneOfConst + ); + } + + private Constraint createMainIsMutableOrRdmConstraint(AnnotatedTypeMirror mainAtm) { + assert infer; + final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + // A || B <-> !A -> B + return constraintManager.createImplicationConstraint( + Collections.singletonList(constraintManager.createInequalityConstraint( + slotManager.getSlot(MUTABLE), + slotManager.getSlot(mainAtm))), + constraintManager.createEqualityConstraint( + slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE), + slotManager.getSlot(mainAtm) + ) + ); + } + + /** + * + * @param atm + * @param contains + * @param oneOf + */ + public boolean ifBoundContainsThenMainIsOneOf(AnnotatedDeclaredType atm, AnnotationMirror contains, + AnnotationMirror[] oneOf) { + + AnnotationMirror boundAnno = extractInitBoundAnno(atm); + return ifAnnoIsThenMainIsOneOf(boundAnno, contains, atm, oneOf); + + } + + public boolean ifAnnoIsThenMainIsOneOf(AnnotationMirror annotation, AnnotationMirror is, + AnnotatedTypeMirror mainAtm, AnnotationMirror[] oneOf) { + // TODO support more annotations + assert oneOf.length == 2: "oneOf.length should be 2"; + if (this.infer) { + final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + Constraint oneOfConst = constraintManager.createImplicationConstraint( + Collections.singletonList(constraintManager.createInequalityConstraint( + slotManager.getSlot(oneOf[0]), + slotManager.getSlot(mainAtm))), + constraintManager.createEqualityConstraint( + slotManager.getSlot(oneOf[1]), + slotManager.getSlot(mainAtm) + ) + ); + + constraintManager.addImplicationConstraint( + Collections.singletonList(constraintManager.createEqualityConstraint( + slotManager.getSlot(annotation), + slotManager.getSlot(is))), + oneOfConst + ); + return true; // always return true on inference + } else { + if (AnnotationUtils.areSameByName(annotation, is)) { + return AnnotationUtils.containsSameByName(Arrays.asList(oneOf), + mainAtm.getAnnotationInHierarchy(READONLY)); + } + } + return true; + } + + /** + * Make the main annotation on {@code atm} cannot infer to given {@code anno}. + * But the written annotation still have effect. + *

+ * A notable use could be poly annotations which could be used by inference if explicitly present, + * but new poly cannot be inferred. + *

+ * @param atm the type which should not inferred to given anno + * @param anno the anno that cannot be inferred to + * @param errorKey this will show only if things goes wrong and result into a error message in type-check. + * @param tree this will show only if things goes wrong and result into a error message in type-check. + */ + public void mainCannotInferTo(AnnotatedTypeMirror atm, AnnotationMirror anno, String errorKey, Tree tree) { + if (infer) { + SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + // should be constant slot if written explicitly in code + if (!(slotManager.getSlot(atm) instanceof ConstantSlot)) { + mainIsNot(atm, anno, errorKey, tree); + } + + } + } + + @Override public Void visitMethod(MethodTree node, Void p) { AnnotatedExecutableType executableType = atypeFactory.getAnnotatedType(node); - AnnotatedDeclaredType bound = PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(node, atypeFactory); + AnnotatedDeclaredType bound; + if (PICOTypeUtil.isEnclosedByAnonymousClass(node, atypeFactory)) { + bound = PICOTypeUtil.getBoundOfEnclosingAnonymousClass(node, atypeFactory); + } else { + bound = PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(node, atypeFactory); + } + assert bound != null; + assert !bound.hasAnnotation(POLY_MUTABLE) : "BOUND CANNOT BE POLY"; + + // cannot infer poly, but can use it for type-check. + mainCannotInferTo(executableType.getReturnType(), POLY_MUTABLE, "cannot.infer.poly", node); + if (executableType.getReceiverType() != null) { + mainCannotInferTo(executableType.getReceiverType(), POLY_MUTABLE, "cannot.infer.poly", node); + } if (TreeUtils.isConstructor(node)) { // Doesn't check anonymous constructor case @@ -238,24 +451,22 @@ public Void visitMethod(MethodTree node, Void p) { } AnnotatedDeclaredType constructorReturnType = (AnnotatedDeclaredType) executableType.getReturnType(); + // Constructor return cannot be @Readonly + mainIsNot(constructorReturnType, READONLY, "constructor.return.invalid", node); + if (infer) { - // Constructor return cannot be @Readonly - mainIsNot(constructorReturnType, READONLY, "constructor.return.invalid", node); ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot boundSlot = slotManager.getVariableSlot(bound); - Slot consRetSlot = slotManager.getVariableSlot(constructorReturnType); + Slot boundSlot = slotManager.getSlot(bound); + Slot consRetSlot = slotManager.getSlot(constructorReturnType); Slot rdmSlot = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); Constraint inequalityConstraint = constraintManager.createInequalityConstraint(boundSlot, rdmSlot); Constraint subtypeConstraint = constraintManager.createSubtypeConstraint(consRetSlot, boundSlot); // bound != @ReceiverDependantMutable -> consRet <: bound - constraintManager.addImplicationConstraint(Arrays.asList(inequalityConstraint), subtypeConstraint); - } else { - if (constructorReturnType.hasAnnotation(READONLY)) { - checker.report(Result.failure("constructor.return.invalid", constructorReturnType), node); - return super.visitMethod(node, p); - } + constraintManager.addImplicationConstraint(Collections.singletonList(inequalityConstraint), subtypeConstraint); + // TODO Add typecheck for this? } + } else { // Additional logic compared to PICOVisitor to prefer declared receiver and parameters // tp be @Readonly in inference results. @@ -265,24 +476,16 @@ public Void visitMethod(MethodTree node, Void p) { // Prefer declared receiver to be @Readonly addDeepPreference(declaredReceiverType, READONLY, 1, node); } - // Prefer all parametes to be @Readonly + // Prefer all parameters to be @Readonly for (AnnotatedTypeMirror ptype : executableType.getParameterTypes()) { addDeepPreference(ptype, READONLY, 1, node); } } // Above is additional preference logic if (declaredReceiverType != null) { - if (infer) { - addMutableImmutableRdmIncompatibleConstraints(bound, declaredReceiverType); - } else { - if (!bound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) - && !atypeFactory.getQualifierHierarchy().isSubtype( - declaredReceiverType.getAnnotationInHierarchy(READONLY), - bound.getAnnotationInHierarchy(READONLY)) - // Below three are allowed on declared receiver types of instance methods in either @Mutable class or @Immutable class - && !declaredReceiverType.hasAnnotation(READONLY)) { - checker.report(Result.failure("method.receiver.incompatible", declaredReceiverType), node); - } + mainIsNot(declaredReceiverType, BOTTOM, "bottom.on.receiver", node); + if (!isAdaptedSubtype(declaredReceiverType, bound)){ + checker.reportError(node, "method.receiver.incompatible", declaredReceiverType); } } } @@ -292,7 +495,22 @@ public Void visitMethod(MethodTree node, Void p) { // TODO Object identity check return super.visitMethod(node, p); } - + /* + * @RDM + * class A { + * + * void foo(T) { + * + * } + * } + * class B extends @Immutable A<@X String> { + * + * @Override + * void foo(@Y String) { // string is compatible to bound of T. Adapt the signature of Class A to the use of class B. + * } + * } + * + * */ private void flexibleOverrideChecker(MethodTree node) { // Method overriding checks // TODO Copied from super, hence has lots of duplicate code with super. We need to @@ -318,7 +536,7 @@ private void flexibleOverrideChecker(MethodTree node) { 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); + atypeFactory.getViewpointAdapter().viewpointAdaptMethod(enclosingType, pair.getValue() , overriddenMethod); // todo: should we cast it? AnnotatedExecutableType overrider = atypeFactory.getAnnotatedType(node); if (!checkOverride(node, overrider, enclosingType, overriddenMethod, overriddenType)) { // Stop at the first mismatch; this makes a difference only if @@ -337,7 +555,8 @@ protected boolean checkOverride( return true; } - protected void checkTypecastSafety(TypeCastTree node, Void p) { + @Override + protected void checkTypecastSafety(TypeCastTree node) { if (!checker.getLintOption("cast:unsafe", true)) { return; } @@ -348,9 +567,9 @@ protected void checkTypecastSafety(TypeCastTree node, Void p) { // the input types to be subtypes according to Java if (!isTypeCastSafe(castType, exprType, node)) { // This is only warning message, so even though enterred this line, it doesn't cause PICOInfer to exit. - checker.report( - Result.warning("cast.unsafe", exprType.toString(true), castType.toString(true)), - node); + // Even if that was an error, PICOInfer would also not exit. + checker.reportWarning(node, + "cast.unsafe", exprType.toString(true), castType.toString(true)); } } @@ -374,7 +593,7 @@ private boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror return isCompatibleCastInInfer(castType, exprType, node); } else { // Typechecking side standard implementation - warns about downcasting - return super.isTypeCastSafe(castType, exprType); + return isTypeCastSafe(castType, exprType); } } @@ -418,10 +637,10 @@ private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedT return true; } else { // Default strategy - comparablecast - final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + final QualifierHierarchy qualHierarchy = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy(); final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - final Slot castSlot = slotManager.getVariableSlot(castType); - final Slot exprSlot = slotManager.getVariableSlot(exprType); + final Slot castSlot = slotManager.getSlot(castType); + final Slot exprSlot = slotManager.getSlot(exprType); if (castSlot instanceof ConstantSlot && exprSlot instanceof ConstantSlot) { ConstantSlot castCSSlot = (ConstantSlot) castSlot; @@ -429,7 +648,8 @@ private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedT // Special handling for case with two ConstantSlots: even though they may not be comparable, // but to infer more program, let this case fall back to "anycast" silently and continue // inference. - return constraintManager.getConstraintVerifier().areComparable(castCSSlot, exprCSSlot); + return qualHierarchy.isSubtype(castCSSlot.getValue(), exprCSSlot.getValue()) + || qualHierarchy.isSubtype(exprCSSlot.getValue(), castCSSlot.getValue()); } else { // But if there is at least on VariableSlot, PICOInfer guarantees that solutions don't include // incomparable casts. @@ -462,6 +682,8 @@ public Void visitUnary(UnaryTree node, Void p) { return super.visitUnary(node, p); } + + private void checkMutation(ExpressionTree node, ExpressionTree variable) { AnnotatedTypeMirror receiverType = atypeFactory.getReceiverType(variable); if(receiverType != null) { @@ -477,6 +699,7 @@ private void checkMutation(ExpressionTree node, ExpressionTree variable) { private void checkAssignableField(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { Element fieldElement = TreeUtils.elementFromUse(node); + assert fieldElement != null; if (fieldElement != null) {//TODO Can this bu null? AnnotatedTypeMirror fieldType = atypeFactory.getAnnotatedType(fieldElement); assert fieldType != null; @@ -484,13 +707,14 @@ private void checkAssignableField(ExpressionTree node, ExpressionTree variable, // Break the combination of readonly receiver + rdm assignable field ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot receiverSlot = slotManager.getVariableSlot(receiverType); - Slot fieldSlot = slotManager.getVariableSlot(fieldType); + Slot receiverSlot = slotManager.getSlot(receiverType); + Slot fieldSlot = slotManager.getSlot(fieldType); Slot readonly = slotManager.getSlot(READONLY); Slot receiver_dependant_mutable = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); Constraint receiverReadOnly = constraintManager.createEqualityConstraint(receiverSlot, readonly); Constraint fieldNotRDM = constraintManager.createInequalityConstraint(fieldSlot, receiver_dependant_mutable); - constraintManager.addImplicationConstraint(Arrays.asList(receiverReadOnly), fieldNotRDM); + // receiver = READONLY + constraintManager.addImplicationConstraint(Collections.singletonList(receiverReadOnly), fieldNotRDM); } else { if (receiverType.hasAnnotation(READONLY) && fieldType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { reportFieldOrArrayWriteError(node, variable, receiverType); @@ -499,7 +723,8 @@ private void checkAssignableField(ExpressionTree node, ExpressionTree variable, } } - private void checkInitializingObject(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { + private void checkInitializingObject(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { // todo: haifeng we only need to do this in one statement + // TODO rm infer after mainIsNot returns bool if (infer) { // Can be anything from mutable, immutable or receiverdependantmutable mainIsNot(receiverType, READONLY, "illegal.field.write", node); @@ -509,8 +734,9 @@ private void checkInitializingObject(ExpressionTree node, ExpressionTree variabl } } } - + // todo: haifeng: the deciding factor seems to be if it is array or not. Not infer. private void checkMutableReceiverCase(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { + // TODO rm infer after mainIs returns bool if (infer) { mainIs(receiverType, MUTABLE, "illegal.field.write", node); } else { @@ -523,11 +749,11 @@ private void checkMutableReceiverCase(ExpressionTree node, ExpressionTree variab // Completely copied from PICOVisitor private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { if (variable.getKind() == Kind.MEMBER_SELECT) { - checker.report(Result.failure("illegal.field.write", receiverType), TreeUtils.getReceiverTree(variable)); + checker.reportError(TreeUtils.getReceiverTree(variable), "illegal.field.write", receiverType); } else if (variable.getKind() == Kind.IDENTIFIER) { - checker.report(Result.failure("illegal.field.write", receiverType), node); + checker.reportError(node, "illegal.field.write", receiverType); } else if (variable.getKind() == Kind.ARRAY_ACCESS) { - checker.report(Result.failure("illegal.array.write", receiverType), ((ArrayAccessTree)variable).getExpression()); + checker.reportError(((ArrayAccessTree)variable).getExpression(), "illegal.array.write", receiverType); } else { throw new BugInCF("Unknown assignment variable at: ", node); } @@ -541,7 +767,7 @@ private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, An * 2) In constructor * 3) In instance method, declared receiver is @UnderInitialized * - * @param node assignment tree that might be initializing an object + * @param variable assignment tree that might be initializing an object * @return true if the assignment tree is initializing an object * * @see #hasUnderInitializationDeclaredReceiver(MethodTree) @@ -553,13 +779,13 @@ private boolean isInitializingObject(ExpressionTree variable) { TreePath treePath = atypeFactory.getPath(variable); if (treePath == null) return false; - if (TreeUtils.enclosingTopLevelBlock(treePath) != null) { + if (TreePathUtil.enclosingTopLevelBlock(treePath) != null) { // In the initialization block => always allow assigning fields! return true; } - MethodTree enclosingMethod = TreeUtils.enclosingMethod(treePath); - // No possibility of initialiazing object if the assignment is not within constructor or method(both MethodTree) + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(treePath); + // No possibility of initializing object if the assignment is not within constructor or method(both MethodTree) if (enclosingMethod == null) return false; // At this point, we already know that this assignment is field assignment within a method if (TreeUtils.isConstructor(enclosingMethod) || hasUnderInitializationDeclaredReceiver(enclosingMethod)) { @@ -606,28 +832,28 @@ public Void visitNewArray(NewArrayTree node, Void p) { private void checkNewInstanceCreation(Tree node) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); - if (infer) { - // Ensure only @Mutable/@Immutable/@ReceiverDependantMutable are inferred on new instance creation - mainIsNoneOf(type, new AnnotationMirror[]{READONLY}, "pico.new.invalid", node); - } else { - if (type.hasAnnotation(READONLY)) { - checker.report(Result.failure("pico.new.invalid", type), node); - } - } + // Ensure only @Mutable/@Immutable/@ReceiverDependantMutable are inferred on new instance creation + mainIsNoneOf(type, new AnnotationMirror[]{READONLY, POLY_MUTABLE}, "pico.new.invalid", node); } // Completely copied from PICOVisitor @Override public Void visitMethodInvocation(MethodInvocationTree node, Void p) { + // issues with getting super for anonymous class - do not check for anonymous classes. + if (TreeUtils.isSuperConstructorCall(node) && + PICOTypeUtil.isAnonymousClassTree(TreePathUtil.enclosingClass(atypeFactory.getPath(node)), atypeFactory)) { + return null; + } + super.visitMethodInvocation(node, p); - ParameterizedMethodType mfuPair = + ParameterizedExecutableType mfuPair = atypeFactory.methodFromUse(node); - AnnotatedExecutableType invokedMethod = mfuPair.methodType; + 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.isSuperCall(node)) { + if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperConstructorCall(node)) { checkMethodInvocability(invokedMethod, node); } return null; @@ -640,15 +866,14 @@ protected void checkMethodInvocability(AnnotatedExecutableType method, MethodInv AnnotatedTypeMirror superClassConstructorReturnType = method.getReturnType(); // In infer mode, InferenceQualifierHierarchy that is internally used should generate subtype constraint between the // below two types GENERALLY(not always) - if (!atypeFactory.getTypeHierarchy().isSubtype(subClassConstructorReturnType, superClassConstructorReturnType)) { + if (!PICOTypeUtil.isEnumOrEnumConstant(subClassConstructorReturnType) && // THIS IS A HECK: java.lang.Enum itself is considered immutable but its subclasses could be other. Update jdk.astub? + !atypeFactory.getTypeHierarchy().isSubtype(subClassConstructorReturnType, superClassConstructorReturnType)) { // Usually the subtyping check returns true. If not, that means subtype constraint doesn't hold between two // ConstantSlots. Previously, InferenceQualifierHierarchy also generates subtype constraint in this case, // then this unsatisfiable constraint is captured by ConstraintManager and ConstraintManager early exits. But // now for two ConstantSlot case, no subtype constraint is generated any more. So we have to report the error // , otherwise it will cause inference result not typecheck - checker.report( - Result.failure( - "super.constructor.invocation.incompatible", subClassConstructorReturnType, superClassConstructorReturnType), node); + checker.reportError(node, "super.invocation.invalid", subClassConstructorReturnType, node, superClassConstructorReturnType); } } super.checkMethodInvocability(method, node); @@ -679,122 +904,108 @@ protected Set getThrowUpperBoundAnnotations() { @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")) { + // Don't process anonymous class. + if (TypesUtils.isAnonymous(TreeUtils.typeOf(node))) { + checkAnonymousImplements(node, PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, atypeFactory)); super.processClassTree(node); return; } AnnotatedDeclaredType bound = PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); - if (infer) { - mainIsNot(bound, READONLY, "class.bound.invalid", node); - if (checker.hasOption("optimalSolution")) { - addPreference(bound, RECEIVER_DEPENDANT_MUTABLE, 2); - addPreference(bound, IMMUTABLE, 2); - } - } else { - // Has to be either @Mutable, @ReceiverDependantMutable or @Immutable, nothing else - if (!bound.hasAnnotation(MUTABLE) && !bound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) && !bound.hasAnnotation(IMMUTABLE)) { - checker.report(Result.failure("class.bound.invalid", bound), node); - return;// Doesn't process the class tree anymore - } - } - - if (!checkCompatabilityBetweenBoundAndSuperClassesBounds(node, typeElement, bound)) { - return; + mainIsNot(bound, READONLY, "class.bound.invalid", node); + mainIsNot(bound, POLY_MUTABLE, "class.bound.invalid", node); + if (checker.hasOption("optimalSolution")) { + addPreference(bound, RECEIVER_DEPENDANT_MUTABLE, 2); + addPreference(bound, IMMUTABLE, 2); } - if (!checkCompatabilityBetweenBoundAndExtendsImplements(node, bound)) { - return; - } - - // Reach this point iff 1) bound annotation is one of mutable, rdm or immutable; - // 2) bound is compatible with bounds on super types. Only then continue processing - // the class tree + checkSuperClauseEquals(node, bound); + // Always reach this point. Do not suppress errors. super.processClassTree(node); } - private boolean checkCompatabilityBetweenBoundAndSuperClassesBounds(ClassTree node, TypeElement typeElement, AnnotatedDeclaredType bound) { - // Must have compatible bound annotation as the direct super types - List superBounds = PICOTypeUtil.getBoundTypesOfDirectSuperTypes(typeElement, atypeFactory); - for (AnnotatedDeclaredType superBound : superBounds) { - if (infer) { - addSameToMutableImmutableConstraints(superBound, bound); + @Override + protected void checkExtendsImplements(ClassTree classTree) { + // do not use CF's checkExtendsImplements which will generate subtype constraints. + // maybe extract a method between class bound and extends/implements annos and override that. + } + + /** + * The base visitor does not use inference method to check! + * This method is required to add the constraints for extends / implements. + * @param node + */ + private void checkAnonymousImplements(ClassTree node, AnnotatedDeclaredType bound) { + // NOTE: this is a workaround for checking bound against extends/implements + // After inferring annotation CF cannot skip the anonymous class, thus necessary + + assert TypesUtils.isAnonymous(TreeUtils.typeOf(node)); + + if (infer) { + Tree superClause; + if (node.getExtendsClause() != null) { + superClause = node.getExtendsClause(); + } else if (node.getImplementsClause() != null) { + // a anonymous class cannot have both extends or implements + assert node.getImplementsClause().size() == 1; // anonymous class only implement 1 interface + superClause = node.getImplementsClause().get(0); + } else { - // If annotation on super bound is @ReceiverDependantMutable, then any valid bound is permitted. - if (superBound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) continue; - // super bound is either @Mutable or @Immutable. Must be the subtype of the corresponding super bound - if (!atypeFactory.getQualifierHierarchy().isSubtype( - bound.getAnnotationInHierarchy(READONLY), superBound.getAnnotationInHierarchy(READONLY))) { - checker.report(Result.failure("subclass.bound.incompatible", bound, superBound), node); - return false; - } + throw new BugInCF("Anonymous class with no extending/implementing clause!"); } + AnnotationMirror superBound = extractInitBoundAnno((AnnotatedDeclaredType) atypeFactory.getAnnotatedType(superClause)); + // anonymous cannot have implement clause, so no "use" anno of super type + mainIsSubtype(bound, superBound); } - return true; } - private boolean checkCompatabilityBetweenBoundAndExtendsImplements(ClassTree node, AnnotatedDeclaredType bound) { - if (infer) { - atypeFactory.getAnnotatedType(node); + + /** + * extends/implements clause use anno is adapted subtype of bound anno + *

Could be subtype, but recall Readonly and Bottom is not usable on class init bound.

+ * @param node + * @param bound + */ + private void checkSuperClauseEquals(ClassTree node, AnnotatedDeclaredType bound) { + if (node.getExtendsClause() != null) { + AnnotatedTypeMirror ext = atypeFactory.getAnnotatedType(node.getExtendsClause()); + boundVsExtImpClause(bound, ext, "extends.bound.incompatible", node.getExtendsClause()); } + for (Tree impTree : node.getImplementsClause()) { + AnnotatedTypeMirror impType = atypeFactory.getAnnotatedType(impTree); + boundVsExtImpClause(bound, impType, "implements.bound.incompatible", impTree); + } + } - boolean hasSame; - Tree ext = node.getExtendsClause(); - if (ext != null) { - AnnotatedTypeMirror extendsType= atypeFactory.getAnnotatedType(ext); - if (infer) { - ((PICOInferenceAnnotatedTypeFactory) atypeFactory).getVariableAnnotator().visit(extendsType, ext); - areEqual(bound, extendsType, "bound.extends.incompatabile", node); - } else { - hasSame = bound.getAnnotations().size() == extendsType.getAnnotations().size() - && AnnotationUtils.areSame(extendsType.getAnnotationInHierarchy(READONLY), - bound.getAnnotationInHierarchy(READONLY)); - if (!hasSame) { - checker.report(Result.failure("bound.extends.incompatabile"), node); - return false; - } - } + + private void boundVsExtImpClause(AnnotatedDeclaredType classBound, AnnotatedTypeMirror superType, String errorKey, Tree tree) { + // atypeFactory.getTypeDeclarationBounds does not work correctly: getting the real annos instead of slots + AnnotatedTypeMirror superBound = + PICOTypeUtil.getBoundTypeOfTypeDeclaration(superType.getUnderlyingType(), atypeFactory); + + if (!isAdaptedSubtype(superType, superBound)) { + checker.reportError(tree, "type.invalid.annotations.on.use", superType, superBound); } - List impls = node.getImplementsClause(); - if (impls != null) { - for (Tree im : impls) { - AnnotatedTypeMirror implementsType = atypeFactory.getAnnotatedType(im); - if (infer) { - ((PICOInferenceAnnotatedTypeFactory) atypeFactory).getVariableAnnotator().visit(implementsType, im); - areEqual(bound, implementsType, "bound.implements.incompatabile", node); - } else { - hasSame = bound.getAnnotations().size() == implementsType.getAnnotations().size() - && AnnotationUtils.areSame(implementsType.getAnnotationInHierarchy(READONLY), - bound.getAnnotationInHierarchy(READONLY)); - if (!hasSame) { - checker.report(Result.failure("bound.implements.incompatabile"), node); - return false; - } - } - } + // the class bound should be a valid "use" of the super. + // consider replace with isValidUse? + if (!isAdaptedSubtype(classBound, superType)) { + checker.reportError(tree, errorKey, classBound, superType); } - return true; } - private void addSameToMutableImmutableConstraints(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType) { - ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); - SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot declSlot = slotManager.getVariableSlot(declarationType); - Slot useSlot = slotManager.getVariableSlot(useType); - Slot mutable = slotManager.getSlot(MUTABLE); - Slot immutable = slotManager.getSlot(IMMUTABLE); - // declType == @Mutable -> useType == @Mutable - Constraint equalityConstraintLHS = constraintManager.createEqualityConstraint(declSlot, mutable); - Constraint equalityConstraintRHS = constraintManager.createEqualityConstraint(useSlot, mutable); - constraintManager.addImplicationConstraint(Arrays.asList(equalityConstraintLHS), equalityConstraintRHS); - // declType == @Immutable -> useType == @Immutable - equalityConstraintLHS = constraintManager.createEqualityConstraint(declSlot, immutable); - equalityConstraintRHS = constraintManager.createEqualityConstraint(useSlot, immutable); - constraintManager.addImplicationConstraint(Arrays.asList(equalityConstraintLHS), equalityConstraintRHS); + + private boolean checkCompatabilityBetweenBoundAndSuperClassesBounds(ClassTree node, TypeElement typeElement, AnnotatedDeclaredType bound) { + // Must have compatible bound annotation as the direct super types + List superBounds = PICOTypeUtil.getBoundTypesOfDirectSuperTypes(typeElement, atypeFactory); + for (AnnotatedDeclaredType superBound : superBounds) { + if (!isAdaptedSubtype(bound, superBound)) { + checker.reportError(node, "subclass.bound.incompatible", bound, superBound); + return false; // do not stop processing if failed + } + } + return true; } /** @@ -809,15 +1020,19 @@ private void addSameToMutableImmutableConstraints(AnnotatedDeclaredType declarat */ @Override protected void commonAssignmentCheck( - Tree varTree, ExpressionTree valueExp, String errorKey) { + 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; - } - - checkAssignability(var, varTree); + // Seems that typecheck does not have this. + // Removing this check will satisfy initial typecheck of inferrable/issue144/ComplicatedTest.java:42, + // where invalid.annotations.on.use is not expected. + // Local variable is flow-sensitive, so when assigned to a type that contradicts with the init bound, + // it still got "refined" + // Maybe updating the flow-sensitive logic to not refined to invalid type? +// if (!validateType(varTree, var)) { +// return; +// } if (varTree instanceof VariableTree) { VariableElement element = TreeUtils.elementFromDeclaration((VariableTree) varTree); @@ -840,4 +1055,20 @@ protected void commonAssignmentCheck( commonAssignmentCheck(var, valueExp, errorKey); } + + @Override + protected void 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.clearAnnotations(); + newValueType.addAnnotation(extractVarAnnot(valueType)); + + valueType = newValueType; + } + super.commonAssignmentCheck(varType, valueType, valueTree, errorKey); + + } } diff --git a/src/main/java/pico/inference/PICOVariableAnnotator.java b/src/main/java/pico/inference/PICOVariableAnnotator.java index 65893b2..4d92a2e 100644 --- a/src/main/java/pico/inference/PICOVariableAnnotator.java +++ b/src/main/java/pico/inference/PICOVariableAnnotator.java @@ -1,17 +1,17 @@ package pico.inference; -import static pico.typecheck.PICOAnnotationMirrorHolder.BOTTOM; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; - import java.util.Arrays; import java.util.List; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.TypeElement; import javax.lang.model.type.TypeKind; +import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.Slot; +import checkers.inference.qual.VarAnnot; +import com.sun.tools.javac.code.Symbol; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -31,7 +31,10 @@ import checkers.inference.model.ConstraintManager; import checkers.inference.model.VariableSlot; import checkers.inference.model.tree.ArtificialExtendsBoundTree; -import pico.typecheck.PICOTypeUtil; +import org.checkerframework.javacutil.TypesUtils; +import pico.common.PICOTypeUtil; + +import static pico.typecheck.PICOAnnotationMirrorHolder.*; public class PICOVariableAnnotator extends VariableAnnotator { @@ -42,84 +45,145 @@ public PICOVariableAnnotator(InferenceAnnotatedTypeFactory typeFactory, Annotate super(typeFactory, realTypeFactory, realChecker, slotManager, constraintManager); } - @Override - protected void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree classTree) { - super.handleClassDeclaration(classType, classTree); - int interfaceIndex = 1; - for(Tree implementsTree : classTree.getImplementsClause()) { - final AnnotatedTypeMirror implementsType = inferenceTypeFactory.getAnnotatedTypeFromTypeTree(implementsTree); - AnnotatedTypeMirror supertype = classType.directSuperTypes().get(interfaceIndex); - assert supertype.getUnderlyingType() == implementsType.getUnderlyingType(); - visit(supertype, implementsTree); - interfaceIndex++; - } - } +// @Override +// protected void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree classTree) { +// super.handleClassDeclaration(classType, classTree); +// int interfaceIndex = 1; +// for(Tree implementsTree : classTree.getImplementsClause()) { +// final AnnotatedTypeMirror implementsType = inferenceTypeFactory.getAnnotatedTypeFromTypeTree(implementsTree); +// AnnotatedTypeMirror supertype = classType.directSupertypes().get(interfaceIndex); +// assert supertype.getUnderlyingType() == implementsType.getUnderlyingType(); +// visit(supertype, implementsTree); +// interfaceIndex++; +// } +// } + +// @Override +// protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) { +// TypeElement classElement = (TypeElement) classType.getUnderlyingType().asElement(); +// if (classDeclAnnos.containsKey(classElement)) { +// classType.addAnnotation(slotManager.getAnnotation(classDeclAnnos.get(classElement))); +// classType.addAnnotation(READONLY); +// return; +// } +// AnnotatedDeclaredType bound = inferenceTypeFactory.fromElement(classElement); +// +// VariableSlot boundSlot; +// +// // Insert @Immutable VarAnnot directly to enum bound +//// if (PICOTypeUtil.isEnumOrEnumConstant(bound)) { +//// boundSlot = slotManager.createConstantSlot(IMMUTABLE); +//// classType.addAnnotation(slotManager.getAnnotation(boundSlot)); +//// classDeclAnnos.put(classElement, boundSlot); +//// return; +//// } +// +// Tree classTree = inferenceTypeFactory.declarationFromElement(classElement); +// if (classTree != null) { +// // Have source tree +// if (bound.isAnnotatedInHierarchy(READONLY)) { +// // Have bound annotation -> convert to equivalent ConstantSlot +// boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY)); +// } else { +// // No existing annotation -> create new VariableSlot +// boundSlot = createVariable(treeToLocation(classTree)); +// } +// } else { +// // No source tree: bytecode classes +// if (bound.isAnnotatedInHierarchy(READONLY)) { +// // Have bound annotation in stub file +// boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY)); +// } else { +// // No stub file +// if (PICOTypeUtil.isImplicitlyImmutableType(classType)) { +// // Implicitly immutable +// boundSlot = slotManager.createConstantSlot(IMMUTABLE); +// } else { +// // None of the above applies: use conservative @Mutable +// boundSlot = slotManager.createConstantSlot(MUTABLE); +// } +// } +// } +// classType.addAnnotation(slotManager.getAnnotation(boundSlot)); +// classDeclAnnos.put(classElement, boundSlot); +// } @Override - protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) { - TypeElement classElement = (TypeElement) classType.getUnderlyingType().asElement(); - if (classDeclAnnos.containsKey(classElement)) { - classType.addAnnotation(slotManager.getAnnotation(classDeclAnnos.get(classElement))); - classType.addAnnotation(READONLY); - return; - } - AnnotatedDeclaredType bound = inferenceTypeFactory.fromElement(classElement); - - VariableSlot boundSlot; - - // Insert @Immutable VarAnnot directly to enum bound - if (PICOTypeUtil.isEnumOrEnumConstant(bound)) { - boundSlot = createConstant(IMMUTABLE); - classType.addAnnotation(slotManager.getAnnotation(boundSlot)); - classDeclAnnos.put(classElement, boundSlot); - return; - } - - Tree classTree = inferenceTypeFactory.declarationFromElement(classElement); - if (classTree != null) { - // Have source tree - if (bound.isAnnotatedInHierarchy(READONLY)) { - // Have bound annotation -> convert to equivalent ConstantSlot - boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY)); - } else { - // No existing annotation -> create new VariableSlot - boundSlot = createVariable(treeToLocation(classTree)); + protected VariableSlot getOrCreateDeclBound(AnnotatedDeclaredType type) { + TypeElement classDecl = (TypeElement) type.getUnderlyingType().asElement(); + + AnnotationMirror declSlot = getClassDeclVarAnnot(classDecl); + if (declSlot == null) { + // if a explicit annotation presents on the class DECL, use that directly + if (type.isDeclaration() && type.isAnnotatedInHierarchy(READONLY) && !type.hasAnnotation(READONLY)) { + VariableSlot constantSlot = (VariableSlot) slotManager.getSlot(type.getAnnotationInHierarchy(READONLY)); +// TypeElement classDecl = (TypeElement) type.getUnderlyingType().asElement(); + super.getOrCreateDeclBound(type); +// // avoid duplicate annos +// type.removeAnnotationInHierarchy(READONLY); + return constantSlot; } - } else { - // No source tree: bytecode classes - if (bound.isAnnotatedInHierarchy(READONLY)) { - // Have bound annotation in stub file - boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY)); - } else { - // No stub file - if (PICOTypeUtil.isImplicitlyImmutableType(classType)) { - // Implicitly immutable - boundSlot = createConstant(IMMUTABLE); - } else { - // None of the above applies: use conservative @Mutable - boundSlot = createConstant(MUTABLE); - } + + // new class tree of an anonymous class is always visited before (enclosing tree). + // slot should be generated then. + // use that slot and avoid generating a new slot. + // push this change to inference IFF the slot on new class have same requirement with class bound + // e.g. existence slot on new class tree? + if (TypesUtils.isAnonymous(type.getUnderlyingType())) { + assert type.hasAnnotation(VarAnnot.class); + return (VariableSlot) slotManager.getSlot(type.getAnnotation(VarAnnot.class)); } } - classType.addAnnotation(slotManager.getAnnotation(boundSlot)); - classDeclAnnos.put(classElement, boundSlot); + return (VariableSlot) super.getOrCreateDeclBound(type); } - // Don't generate subtype constraint between use type and bound type - @Override - protected void handleInstantiationConstraint(AnnotatedTypeMirror.AnnotatedDeclaredType adt, VariableSlot instantiationSlot, Tree tree) { - return; - } +// @Override +// protected void handleExplicitExtends(Tree extendsTree) { +// // PICO cannot use base extends handling: not simply subtype relationship because of RDM +// // Constraints already generated in processClassTree +// } @Override - protected VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, Tree tree) { - if (PICOTypeUtil.isEnumOrEnumConstant(atm)) { - // Don't add new VarAnnot to type use of enum type - PICOTypeUtil.applyConstant(atm, IMMUTABLE); + public void storeElementType(Element element, AnnotatedTypeMirror atm) { + // this method is override the behavior of super.handleClassDeclaration before storing + // find a better way + + Slot slot = slotManager.getSlot(atm); + // do not use potential slot generated on the class decl annotation + // PICO always have a annotation on the class bound, so Existential should always exist + // TODO make VariableAnnotator::getOrCreateDeclBound protected and override that instead of this method + if (element instanceof Symbol.ClassSymbol && slot instanceof ExistentialVariableSlot) { + AnnotationMirror potential = slotManager.getAnnotation(((ExistentialVariableSlot) slot).getPotentialSlot()); + atm.replaceAnnotation(potential); } - return super.addPrimaryVariable(atm, tree); + + // If an explicit bound exists, the annotator will still place a constant slot on the bound, + // which will considered invalid by CF. + // Maybe not putting an anno at all during bound slot generation would be better? + if (atm.hasAnnotation(VarAnnot.class) && atm.isAnnotatedInHierarchy(READONLY)) { + atm.removeAnnotationInHierarchy(READONLY); + } + super.storeElementType(element, atm); } + // Don't generate subtype constraint between use type and bound type +// @Override +// protected void handleInstantiationConstraint(AnnotatedTypeMirror.AnnotatedDeclaredType adt, VariableSlot instantiationSlot, Tree tree) { +// return; +// } + +// @Override +// protected VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, Tree tree) { +//// if (PICOTypeUtil.isEnumOrEnumConstant(atm)) { +//// // Don't add new VarAnnot to type use of enum type +//// PICOTypeUtil.applyConstant(atm, IMMUTABLE); +//// } +// if (atm instanceof AnnotatedTypeMirror.AnnotatedNullType) { +// PICOTypeUtil.applyConstant(atm, BOTTOM); +// } +// return super.addPrimaryVariable(atm, tree); +// } + // Generates inequality constraint between every strict VariableSlot and @Bottom so that @Bottom is not inserted // back to source code, but can be within the internal state because of dataflow refinement @Override @@ -129,6 +193,7 @@ protected VariableSlot createVariable(AnnotationLocation location) { // @Bottom) if (generateBottomInequality) { constraintManager.addInequalityConstraint(varSlot, slotManager.createConstantSlot(BOTTOM)); + constraintManager.addInequalityConstraint(varSlot, slotManager.createConstantSlot(POLY_MUTABLE)); } return varSlot; } @@ -220,11 +285,23 @@ public Void visitWildcard(AnnotatedTypeMirror.AnnotatedWildcardType wildcardType @Override public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { - if (atm.isAnnotatedInHierarchy(varAnnot)) { + if (atm.isAnnotatedInHierarchy(inferenceTypeFactory.getVarAnnot())) { // Happens for binary trees whose atm is implicitly immutable and already handled by // PICOInferencePropagationTreeAnnotator return; } super.handleBinaryTree(atm, binaryTree); } + + public AnnotationMirror getClassDeclAnno(Element ele) { + return getClassDeclVarAnnot((TypeElement) ele); // todo: solved + } + + + @Override + protected void addDeclarationConstraints(Slot declSlot, Slot instanceSlot) { + // RDM-related constraints cannot use subtype. + // Necessary constraints added in visitor instead. + } + } diff --git a/src/main/java/pico/inference/jdk.astub b/src/main/java/pico/inference/jdk.astub new file mode 100644 index 0000000..401c0ce --- /dev/null +++ b/src/main/java/pico/inference/jdk.astub @@ -0,0 +1,334 @@ +import qual.Mutable; +import qual.Immutable; +import qual.ReceiverDependantMutable; +import qual.Readonly; +import qual.ObjectIdentityMethod; +import java.util.Collection; + +package java.lang; + +@ReceiverDependantMutable +class Object { + @ReceiverDependantMutable Object(); + Class getClass(@Readonly Object this); + String toString(@Readonly Object this); + @OnlyDependantOnAbstractStateField + int hashCode(@Readonly Object this); + @OnlyDependantOnAbstractStateField + boolean equals(@Readonly Object this, @Readonly Object var1); + @ReceiverDependantMutable Object clone(@ReceiverDependantMutable 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); + 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); +} + +@ReceiverDependantMutable +class Throwable { + String getMessage(@ReceiverDependantMutable Throwable this); + String getLocalizedMessage(@ReceiverDependantMutable Throwable this); + Throwable getCause(@ReceiverDependantMutable Throwable this); + void printStackTrace(@ReceiverDependantMutable Throwable this); + void printStackTrace(@ReceiverDependantMutable Throwable this, PrintStream var1); + void printStackTrace(@ReceiverDependantMutable Throwable this, Throwable.PrintStreamOrWriter var1); +} + +@ReceiverDependantMutable +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); +} + +@ReceiverDependantMutable +class RuntimeException { + @ReceiverDependantMutable RuntimeException(@Readonly Throwable var1); + @ReceiverDependantMutable RuntimeException(String var1, @Readonly Throwable var2, boolean var3, boolean var4); +} + +@ReceiverDependantMutable +class IndexOutOfBoundsException {} + +@Immutable +class Enum> { + @Immutable Enum(String name, int ordinal); + int ordinal(@Immutable Enum this); +} + +@ReceiverDependantMutable +interface Cloneable {} + +@ReceiverDependantMutable +interface Comparable {} + +package java.util; + +@ReceiverDependantMutable +class Properties { + @Readonly Object put(@Immutable Object key, @Readonly Object value); +} + +interface Iterator {} + +@ReceiverDependantMutable +class Date { + @ReceiverDependantMutable Date(); + @ReceiverDependantMutable Date(long var1); + int getHours(@ReceiverDependantMutable Date this); +} + +@ReceiverDependantMutable +interface Collection { + boolean contains(@Readonly Collection this, @Readonly Object o); +} + +@ReceiverDependantMutable +public abstract class AbstractCollection implements Collection { + public abstract int size(@Readonly AbstractCollection this); +} + +@ReceiverDependantMutable +class ArrayList { + @ReceiverDependantMutable ArrayList(); + @ReceiverDependantMutable ArrayList(@Readonly Collection var1); + boolean add(E var1); + boolean addAll(@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); + void rangeCheck(@Readonly ArrayList this, int index); + Iterator iterator(@Readonly ArrayList this); +} + +@ReceiverDependantMutable +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); +} + +@ReceiverDependantMutable +class AbstractList { + @ReceiverDependantMutable AbstractList(); + void add(@Mutable AbstractList this, int var1, E var2); +} + +@ReceiverDependantMutable +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); +} + +@ReceiverDependantMutable +class HashSet { + @ReceiverDependantMutable HashSet(); + @ReceiverDependantMutable HashSet(@Readonly Collection var1); + boolean contains(@Readonly HashSet this, @Readonly Object var1); + boolean remove(@Readonly Object var1); +} + +@ReceiverDependantMutable +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, @Readonly Object var1); + V remove(@Readonly Object key); + void putAll(@Readonly Map m); + Set keySet(@Readonly Map this); + Collection values(@Readonly Map this); + Set> entrySet(@Readonly Map this); +} + +@ReceiverDependantMutable +class HashMap { + @ReceiverDependantMutable HashMap(); + @ReceiverDependantMutable 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); +} + +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 T[] copyOf(T @Readonly [] original, int newLength); +} + +class Objects { + static int hashCode(@Readonly Object o); + static boolean equals(@Readonly Object a, @Readonly Object b); +} + +@ReceiverDependantMutable +class Stack { + E peek(@ReceiverDependantMutable Stack this); + boolean empty(@ReceiverDependantMutable Stack this); +} + +@ReceiverDependantMutable +class Vector { + boolean isEmpty(@Readonly Vector this); +} + +@ReceiverDependantMutable +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.io; + +@ReceiverDependantMutable +class PrintStream { + void print(@ReceiverDependantMutable PrintStream this, String var1); + PrintStream printf(@ReceiverDependantMutable PrintStream this, String var1, @Readonly Object @Readonly ... var2); + PrintStream format(String format, @Readonly Object @Readonly ... args); +} + +@ReceiverDependantMutable +class PrintWriter { + PrintWriter printf(@ReceiverDependantMutable PrintWriter this, String var1, @Readonly Object @Readonly ... var2); +} + +@ReceiverDependantMutable +class File { + @ReceiverDependantMutable 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); +} + +@ReceiverDependantMutable +class FileInputStream { + @ReceiverDependantMutable FileInputStream(@Readonly File file); +} + +class ObjectOutputStream { + void writeObject(@Readonly Object obj); +} + +@ReceiverDependantMutable +interface Serializable {} + +package org.hibernate; +class Session { + Object get(@Readonly Class clazz, @Readonly Serializable id); +} + +package java.awt; + +@ReceiverDependantMutable +class Container { + void add(@Readonly Component comp, @Readonly Object constraints); +} + +package org.apache.maven.plugin.logging; + +interface Log { + void info(@Readonly Log this, @Readonly CharSequence content); + void info(@Readonly Log this, @Readonly CharSequence content, @Readonly Throwable error); + void info(@Readonly Log this, @Readonly Throwable error); + void debug(@Readonly Log this, @Readonly CharSequence content); + void debug(@Readonly Log this, @Readonly CharSequence content, @Readonly Throwable error); + void debug(@Readonly Log this, @Readonly Throwable error); + void warn(@Readonly Log this, @Readonly CharSequence content); + void warn(@Readonly Log this, @Readonly CharSequence content, @Readonly Throwable error); + void warn(@Readonly Log this, @Readonly Throwable error); + void error(@Readonly Log this, @Readonly CharSequence content); + void error(@Readonly Log this, @Readonly CharSequence content, @Readonly Throwable error); + void error(@Readonly Log this, @Readonly Throwable error); + boolean isInfoEnabled(@Readonly Log this); + boolean isDebugEnabled(@Readonly Log this); + boolean isWarnEnabled(@Readonly Log this); + boolean isErrorEnabled(@Readonly Log this); +} + +package org.apache.commons.io; +class FileUtils { + static long copyFile(@Readonly File input, OutputStream output); +} diff --git a/src/main/java/pico/inference/messages.properties b/src/main/java/pico/inference/messages.properties new file mode 100644 index 0000000..1d0fd13 --- /dev/null +++ b/src/main/java/pico/inference/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 +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.receiverdependantmutable.forbidden=%s is forbidden in static context +pico.new.invalid=Invalid new instance 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! +bound.extends.incompatible=TEST \ No newline at end of file diff --git a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java index 21ac92e..a03ccae 100644 --- a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java +++ b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; +import checkers.inference.model.CombVariableSlot; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; @@ -51,7 +52,7 @@ private boolean isReceiverDependantMutable(ConstantSlot cSlot) { } @Override - public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declared, VariableSlot result) { + public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); resultClauses.add(VectorUtils.asVec( -MathUtils.mapIdToMatrixEntry(declared.getId(), id(READONLY), lattice), @@ -89,7 +90,7 @@ public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declar } @Override - public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, VariableSlot result) { + public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); if (!isReceiverDependantMutable(declared)) { resultClauses.add(VectorUtils.asVec( @@ -116,7 +117,7 @@ public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declar } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declared, VariableSlot result) { + public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); resultClauses.add(VectorUtils.asVec( -MathUtils.mapIdToMatrixEntry(declared.getId(), id(READONLY), lattice), @@ -137,7 +138,7 @@ public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declar } @Override - public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, VariableSlot result) { + public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); if (!isReceiverDependantMutable(declared)) { resultClauses.add(VectorUtils.asVec( diff --git a/src/main/java/pico/inference/solver/PICOSolverEngine.java b/src/main/java/pico/inference/solver/PICOSolverEngine.java index 213a809..5ff0d7d 100644 --- a/src/main/java/pico/inference/solver/PICOSolverEngine.java +++ b/src/main/java/pico/inference/solver/PICOSolverEngine.java @@ -1,6 +1,6 @@ package pico.inference.solver; -import checkers.inference.BaseInferenceResult; +import checkers.inference.DefaultInferenceResult; import checkers.inference.InferenceResult; import checkers.inference.model.Constraint; import checkers.inference.model.Slot; @@ -24,14 +24,14 @@ * to solve constraints */ public class PICOSolverEngine extends SolverEngine { - @Override - public InferenceResult solve(Map configuration, Collection slots, Collection constraints, QualifierHierarchy qualHierarchy, ProcessingEnvironment processingEnvironment) { - InferenceResult result= super.solve(configuration, slots, constraints, qualHierarchy, processingEnvironment); - if (collectStatistics && result.hasSolution()) { - writeInferenceResult("pico-inference-result.txt", ((BaseInferenceResult)result).inferredResults); - } - return result; - } +// @Override +// public InferenceResult solve(Map configuration, Collection slots, Collection constraints, QualifierHierarchy qualHierarchy, ProcessingEnvironment processingEnvironment) { +// InferenceResult result= super.solve(configuration, slots, constraints, qualHierarchy, processingEnvironment); +// if (collectStatistics && result.hasSolution()) { +// writeInferenceResult("pico-inference-result.txt", ((DefaultInferenceResult)result).varIdToAnnotation); +// } +// return result; +// } // TODO: default write into statistic.txt public static void writeInferenceResult(String filename, Map result) { String writePath = new File(new File("").getAbsolutePath()).toString() + File.separator + filename; diff --git a/src/main/java/pico/typecheck/ObjectIdentityMethodEnforcer.java b/src/main/java/pico/typecheck/ObjectIdentityMethodEnforcer.java index fb54dea..6ad8a84 100644 --- a/src/main/java/pico/typecheck/ObjectIdentityMethodEnforcer.java +++ b/src/main/java/pico/typecheck/ObjectIdentityMethodEnforcer.java @@ -7,11 +7,10 @@ import com.sun.source.util.TreePath; import com.sun.source.util.TreePathScanner; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.source.Result; import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; -import qual.Assignable; +import pico.common.PICOTypeUtil; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; @@ -53,7 +52,7 @@ private void checkMethod(MethodInvocationTree node, Element elt) { if (!PICOTypeUtil.isObjectIdentityMethod((ExecutableElement) elt, typeFactory)) { // Report warning since invoked method is not only dependant on abstract state fields, but we // don't know whether this method invocation's result flows into the hashcode or not. - checker.report(Result.warning("object.identity.method.invocation.invalid", elt), node); + checker.reportWarning(node, "object.identity.method.invocation.invalid", elt); } } @@ -78,11 +77,11 @@ private void checkField(Tree node, Element elt) { } if (elt.getKind() == ElementKind.FIELD) { if (ElementUtils.isStatic(elt)) { - checker.report(Result.warning("object.identity.static.field.access.forbidden", elt), node); + 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.report(Result.warning("object.identity.field.access.invalid", elt), node); + checker.reportWarning(node, "object.identity.field.access.invalid", elt); } } } diff --git a/src/main/java/pico/typecheck/PICOAnalysis.java b/src/main/java/pico/typecheck/PICOAnalysis.java index 54cecfa..1230003 100644 --- a/src/main/java/pico/typecheck/PICOAnalysis.java +++ b/src/main/java/pico/typecheck/PICOAnalysis.java @@ -16,8 +16,8 @@ */ public class PICOAnalysis extends CFAbstractAnalysis { - public PICOAnalysis(BaseTypeChecker checker, PICOAnnotatedTypeFactory factory, List> fieldValues) { - super(checker, factory, fieldValues); + public PICOAnalysis(BaseTypeChecker checker, PICOAnnotatedTypeFactory factory) { + super(checker, factory, -1); } @Override diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 77bef15..574c1f1 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -1,16 +1,10 @@ package pico.typecheck; -import static pico.typecheck.PICOAnnotationMirrorHolder.COMMITED; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.POLY_MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; -import static pico.typecheck.PICOAnnotationMirrorHolder.SUBSTITUTABLE_POLY_MUTABLE; - import java.lang.annotation.Annotation; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; @@ -18,10 +12,16 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; -import javax.lang.model.element.ExecutableElement; +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; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.ParameterizedTypeTree; +import com.sun.source.util.TreePath; import org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory; import org.checkerframework.checker.initialization.qual.FBCBottom; import org.checkerframework.checker.initialization.qual.Initialized; @@ -34,41 +34,39 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.framework.type.ViewpointAdapter; -import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; -import org.checkerframework.framework.type.typeannotator.ImplicitsTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.PropagationTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.TypeAnnotator; -import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; +import org.checkerframework.framework.type.typeannotator.*; +import org.checkerframework.framework.util.QualifierKind; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import com.sun.source.tree.BinaryTree; -import com.sun.source.tree.ClassTree; import com.sun.source.tree.ExpressionTree; -import com.sun.source.tree.IdentifierTree; -import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.NewArrayTree; -import com.sun.source.tree.ParameterizedTypeTree; import com.sun.source.tree.Tree; import com.sun.source.tree.TypeCastTree; import com.sun.source.tree.UnaryTree; import com.sun.source.tree.VariableTree; +import pico.common.ExtendedViewpointAdapter; +import pico.common.PICOTypeUtil; +import pico.common.ViewpointAdapterGettable; import qual.Bottom; import qual.Immutable; import qual.Mutable; import qual.PolyMutable; import qual.Readonly; import qual.ReceiverDependantMutable; -import qual.SubstitutablePolyMutable; + +import static pico.typecheck.PICOAnnotationMirrorHolder.*; /** * AnnotatedTypeFactory for PICO. In addition to getting atms, it also propagates and applies mutability @@ -79,12 +77,14 @@ //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 PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory { + PICOStore, PICOTransfer, PICOAnalysis> implements ViewpointAdapterGettable { public PICOAnnotatedTypeFactory(BaseTypeChecker checker) { - super(checker, true); + super(checker); postInit(); - addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + // PICO aliasing is not implemented correctly + // remove for now +// addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); } @Override @@ -95,7 +95,6 @@ protected Set> createSupportedTypeQualifiers() { Mutable.class, PolyMutable.class, ReceiverDependantMutable.class, - SubstitutablePolyMutable.class, Immutable.class, Bottom.class, Initialized.class, @@ -114,8 +113,9 @@ protected ViewpointAdapter createViewpointAdapter() { protected TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( new PICOPropagationTreeAnnotator(this), - new ImplicitsTreeAnnotator(this), + new LiteralTreeAnnotator(this), new CommitmentTreeAnnotator(this), + new PICOSuperClauseAnnotator(this), new PICOTreeAnnotator(this)); } @@ -127,12 +127,12 @@ protected TypeAnnotator createTypeAnnotator() { RelevantJavaTypes relevantJavaTypes = checker.getClass().getAnnotation(RelevantJavaTypes.class); if (relevantJavaTypes != null) { - Class[] classes = relevantJavaTypes.value(); +// Class[] classes = relevantJavaTypes.value(); // Must be first in order to annotated all irrelevant types that are not explicilty // annotated. typeAnnotators.add( new IrrelevantTypeAnnotator( - this, getQualifierHierarchy().getTopAnnotations(), classes)); + this, getQualifierHierarchy().getTopAnnotations())); } typeAnnotators.add(new PropagationTypeAnnotator(this)); /*Copied code ends*/ @@ -140,14 +140,15 @@ protected TypeAnnotator createTypeAnnotator() { // method, so if one annotator already applied the annotations, the others won't apply twice at the // same location typeAnnotators.add(new PICOTypeAnnotator(this)); - typeAnnotators.add(new PICOImplicitsTypeAnnotator(this)); + typeAnnotators.add(new PICODefaultForTypeAnnotator(this)); + typeAnnotators.add(new PICOEnumDefaultAnnotator(this)); typeAnnotators.add(new CommitmentTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } @Override - public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { - return new PICOQualifierHierarchy(factory, (Object[]) null); + public QualifierHierarchy createQualifierHierarchy() { + return new PICOQualifierHierarchy(); } /**Just to transfer the method from super class to package*/ @@ -181,107 +182,114 @@ public boolean getShouldDefaultTypeVarLocals() { public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { PICOTypeUtil.addDefaultForField(this, type, elt); PICOTypeUtil.defaultConstructorReturnToClassBound(this, elt, type); - PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); +// PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); super.addComputedTypeAnnotations(elt, type); } - @Override - protected void annotateInheritedFromClass(AnnotatedTypeMirror type, Set fromClass) { - // If interitted from class element is @Mutable or @Immutable, then apply this annotation to the usage type - if (fromClass.contains(MUTABLE) || fromClass.contains(IMMUTABLE)) { - super.annotateInheritedFromClass(type, fromClass); - return; - } - // If interitted from class element is @ReceiverDependantMutable, then don't apply and wait for @Mutable - // (default qualifier in hierarchy to be applied to the usage type). This is to avoid having @ReceiverDependantMutable - // on type usages as a default behaviour. By default, @Mutable is better used as the type for usages that - // don't have explicit annotation. - return;// Don't add annotations from class element - } - /**This method gets lhs WITH flow sensitive refinement*/ // TODO Should refactor super class to avoid too much duplicate code. // This method is pretty hacky right now. - @Override - public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { - boolean oldComputingAnnotatedTypeMirrorOfLHS = computingAnnotatedTypeMirrorOfLHS; - computingAnnotatedTypeMirrorOfLHS = true; - - AnnotatedTypeMirror result = null; - boolean oldShouldCache = shouldCache; - // Don't cache the result because getAnnotatedType(lhsTree) could - // be called from elsewhere and would expect flow-sensitive type refinements. - shouldCache = false; - switch (lhsTree.getKind()) { - case VARIABLE: - case IDENTIFIER: - case MEMBER_SELECT: - case ARRAY_ACCESS: - result = getAnnotatedType(lhsTree); - break; - default: - if (TreeUtils.isTypeTree(lhsTree)) { - // lhsTree is a type tree at the pseudo assignment of a returned expression to declared return type. - result = getAnnotatedType(lhsTree); - } else { - throw new BugInCF( - "GenericAnnotatedTypeFactory: Unexpected tree passed to getAnnotatedTypeLhs. " - + "lhsTree: " - + lhsTree - + " Tree.Kind: " - + lhsTree.getKind()); - } - } - shouldCache = oldShouldCache; - - computingAnnotatedTypeMirrorOfLHS = oldComputingAnnotatedTypeMirrorOfLHS; - return result; - } - - /**Handles invoking static methods with polymutable on its declaration*/ - @Override - public ParameterizedMethodType methodFromUse(ExpressionTree tree, ExecutableElement methodElt, AnnotatedTypeMirror receiverType) { - ParameterizedMethodType pair = super.methodFromUse(tree, methodElt, receiverType); - // We want to replace polymutable with substitutablepolymutable when we invoke static methods - if (ElementUtils.isStatic(methodElt)) { - AnnotatedExecutableType methodType = pair.methodType; - AnnotatedTypeMirror returnType = methodType.getReturnType(); - if (returnType.hasAnnotation(POLY_MUTABLE)) { - // Only substitute polymutable but not other qualifiers! Missing the if statement - // caused bugs before! - returnType.replaceAnnotation(SUBSTITUTABLE_POLY_MUTABLE); - } - List parameterTypes = methodType.getParameterTypes(); - for (AnnotatedTypeMirror p : parameterTypes) { - if (returnType.hasAnnotation(POLY_MUTABLE)) { - p.replaceAnnotation(SUBSTITUTABLE_POLY_MUTABLE); - } - } - } - return pair; - } +// @Override +// public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { +// boolean oldComputingAnnotatedTypeMirrorOfLHS = computingAnnotatedTypeMirrorOfLHS; +// computingAnnotatedTypeMirrorOfLHS = true; +// +// AnnotatedTypeMirror result; +// boolean oldShouldCache = shouldCache; +// // Don't cache the result because getAnnotatedType(lhsTree) could +// // be called from elsewhere and would expect flow-sensitive type refinements. +// shouldCache = false; +// switch (lhsTree.getKind()) { +// case VARIABLE: +// case IDENTIFIER: +// case MEMBER_SELECT: +// case ARRAY_ACCESS: +// result = getAnnotatedType(lhsTree); +// break; +// default: +// if (TreeUtils.isTypeTree(lhsTree)) { +// // lhsTree is a type tree at the pseudo assignment of a returned expression to declared return type. +// result = getAnnotatedType(lhsTree); +// } else { +// throw new BugInCF( +// "GenericAnnotatedTypeFactory: Unexpected tree passed to getAnnotatedTypeLhs. " +// + "lhsTree: " +// + lhsTree +// + " Tree.Kind: " +// + lhsTree.getKind()); +// } +// } +// shouldCache = oldShouldCache; +// +// computingAnnotatedTypeMirrorOfLHS = oldComputingAnnotatedTypeMirrorOfLHS; +// return result; +// } + +// /**Handles invoking static methods with polymutable on its declaration*/ +// @Override +// public ParameterizedExecutableType methodFromUse(ExpressionTree tree, ExecutableElement methodElt, AnnotatedTypeMirror receiverType) { +// ParameterizedExecutableType pair = super.methodFromUse(tree, methodElt, receiverType); +// // We want to replace polymutable with substitutablepolymutable when we invoke static methods +// if (ElementUtils.isStatic(methodElt)) { +// AnnotatedExecutableType methodType = pair.executableType; +// AnnotatedTypeMirror returnType = methodType.getReturnType(); +// if (returnType.hasAnnotation(POLY_MUTABLE)) { +// // Only substitute polymutable but not other qualifiers! Missing the if statement +// // caused bugs before! +// returnType.replaceAnnotation(SUBSTITUTABLE_POLY_MUTABLE); +// } +// List parameterTypes = methodType.getParameterTypes(); +// for (AnnotatedTypeMirror p : parameterTypes) { +// if (returnType.hasAnnotation(POLY_MUTABLE)) { +// p.replaceAnnotation(SUBSTITUTABLE_POLY_MUTABLE); +// } +// } +// } +// return pair; +// } protected class PICOQualifierHierarchy extends InitializationQualifierHierarchy { - public PICOQualifierHierarchy(MultiGraphFactory f, Object[] arg) { - super(f, arg); - } +// public PICOQualifierHierarchy(MultiGraphFactory f, Object[] arg) { +// super(f, arg); +// } + +// @Override +// public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { +// if (isInitializationAnnotation(subAnno) || isInitializationAnnotation(superAnno)) { +// return this.isSubtypeInitialization(subAnno, superAnno); +// } +// return super.isSubtype(subAnno, superAnno); +// } @Override - public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { + protected boolean isSubtypeWithElements(AnnotationMirror subAnno, QualifierKind subKind, AnnotationMirror superAnno, QualifierKind superKind) { if (isInitializationAnnotation(subAnno) || isInitializationAnnotation(superAnno)) { - return this.isSubtypeInitialization(subAnno, superAnno); + return this.isSubtypeInitialization(subAnno, subKind, superAnno, superKind); } return super.isSubtype(subAnno, superAnno); } +// @Override +// public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) { +// if (isInitializationAnnotation(a1) || isInitializationAnnotation(a2)) { +// return this.leastUpperBoundInitialization(a1, a2); +// } +// return super.leastUpperBound(a1, a2); +// } + @Override - public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) { + protected AnnotationMirror leastUpperBoundWithElements(AnnotationMirror a1, QualifierKind q1, AnnotationMirror a2, QualifierKind q2, QualifierKind lub) { if (isInitializationAnnotation(a1) || isInitializationAnnotation(a2)) { - return this.leastUpperBoundInitialization(a1, a2); + return this.leastUpperBoundInitialization(a1, q1, a2, q2); } return super.leastUpperBound(a1, a2); } + + @Override + protected AnnotationMirror greatestLowerBoundWithElements(AnnotationMirror annotationMirror, QualifierKind qualifierKind, AnnotationMirror annotationMirror1, QualifierKind qualifierKind1, QualifierKind qualifierKind2) { + return null; + } } /**Tree Annotators*/ @@ -289,122 +297,134 @@ public static class PICOPropagationTreeAnnotator extends PropagationTreeAnnotato public PICOPropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); } - - // TODO This is very ugly. Why is array component type from lhs propagates to rhs?! +// +// // TODO This is very ugly. Why is array component type from lhs propagates to rhs?! @Override public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { - // Below is copied from super - assert type.getKind() == TypeKind.ARRAY - : "PropagationTreeAnnotator.visitNewArray: should be an array type"; - AnnotatedTypeMirror componentType = ((AnnotatedTypeMirror.AnnotatedArrayType) type).getComponentType(); - - Collection prev = null; - if (tree.getInitializers() != null && tree.getInitializers().size() != 0) { - // We have initializers, either with or without an array type. - - for (ExpressionTree init : tree.getInitializers()) { - AnnotatedTypeMirror initType = atypeFactory.getAnnotatedType(init); - // initType might be a typeVariable, so use effectiveAnnotations. - Collection annos = initType.getEffectiveAnnotations(); - - prev = (prev == null) ? annos : atypeFactory.getQualifierHierarchy().leastUpperBounds(prev, annos); - } - } else { - prev = componentType.getAnnotations(); + boolean noExplicitATM = false; + if (!componentType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { + noExplicitATM = true; } - - assert prev != null - : "PropagationTreeAnnotator.visitNewArray: violated assumption about qualifiers"; - - Pair context = - atypeFactory.getVisitorState().getAssignmentContext(); - Collection post; - - if (context != null - && context.second != null - && context.second instanceof AnnotatedTypeMirror.AnnotatedArrayType) { - AnnotatedTypeMirror contextComponentType = - ((AnnotatedTypeMirror.AnnotatedArrayType) context.second).getComponentType(); - // Only compare the qualifiers that existed in the array type - // Defaulting wasn't performed yet, so prev might have fewer qualifiers than - // contextComponentType, which would cause a failure. - // TODO: better solution? - boolean prevIsSubtype = true; - for (AnnotationMirror am : prev) { - if (contextComponentType.isAnnotatedInHierarchy(am) - && !atypeFactory.getQualifierHierarchy().isSubtype( - am, contextComponentType.getAnnotationInHierarchy(am))) { - prevIsSubtype = false; - } - } - // TODO: checking conformance of component kinds is a basic sanity check - // It fails for array initializer expressions. Those should be handled nicer. - if (contextComponentType.getKind() == componentType.getKind() - && (prev.isEmpty() - || (!contextComponentType.getAnnotations().isEmpty() - && prevIsSubtype))) { - post = contextComponentType.getAnnotations(); - } else { - // The type of the array initializers is incompatible with the - // context type! - // Somebody else will complain. - post = prev; - } - } else { - // No context is available - simply use what we have. - post = prev; + 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_DEPENDANT_MUTABLE)) { + componentType.replaceAnnotation(MUTABLE); } - - // Below line is the only difference from super implementation - applyImmutableIfImplicitlyImmutable(componentType); - // Above line is the only difference from super implementation - componentType.addMissingAnnotations(post); - return null; - // Above is copied from super + } +// +// /**Add immutable to the result type of a binary operation if the result type is implicitly immutable*/ +// @Override +// public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { +// applyImmutableIfImplicitlyImmutable(type);// Usually there isn't existing annotation on binary trees, but to be safe, run it first +// super.visitBinary(node, type); +// // NullnessPropagationTreeAnnotator says result type of binary tree is always @Initialized. So replace it +// // with COMMITED here. +// applyCommitedIfSupported(atypeFactory, type); +// return null; +// } + +// @Override +// public Void visitUnary(UnaryTree node, AnnotatedTypeMirror type) { +// super.visitUnary(node, type); +// // Same reason as above +// applyCommitedIfSupported(atypeFactory, type); +// return null; +// } +// +// /**Add immutable to the result type of a cast if the result type is implicitly immutable*/ +// @Override +// public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { +// applyImmutableIfImplicitlyImmutable(type);// Must run before calling super method to respect existing annotation +// return super.visitTypeCast(node, type); +// } +// + /**Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are not guaranteed + to always have immutable annotation. If this happens, we manually add immutable to type. We use + addMissingAnnotations because we want to respect existing annotation on type*/ + private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) { + if (PICOTypeUtil.isImplicitlyImmutableType(type)) { + type.addMissingAnnotations(new HashSet<>(Collections.singletonList(IMMUTABLE))); + } } - /**Add immutable to the result type of a binary operation if the result type is implicitly immutable*/ @Override public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { - applyImmutableIfImplicitlyImmutable(type);// Usually there isn't existing annotation on binary trees, but to be safe, run it first - super.visitBinary(node, type); - // NullnessPropagationTreeAnnotator says result type of binary tree is always @Initialized. So replace it - // with COMMITED here. - applyCommitedIfSupported(atypeFactory, type); return null; } - @Override - public Void visitUnary(UnaryTree node, AnnotatedTypeMirror type) { - super.visitUnary(node, type); - // Same reason as above - applyCommitedIfSupported(atypeFactory, type); - return null; +// private void applyCommitedIfSupported(AnnotatedTypeFactory annotatedTypeFactory, AnnotatedTypeMirror type) { +// if (annotatedTypeFactory.isSupportedQualifier(COMMITED)) { +// type.replaceAnnotation(COMMITED); +// } +// } + } + + public ExtendedViewpointAdapter getViewpointAdapter() { + return (ExtendedViewpointAdapter) viewpointAdapter; + } + + @Override + protected Set getDefaultTypeDeclarationBounds() { + Set frameworkDefault = new HashSet<>(super.getDefaultTypeDeclarationBounds()); + return replaceAnnotationInHierarchy(frameworkDefault, MUTABLE); + } + + @Override + public Set getTypeDeclarationBounds(TypeMirror type) { + AnnotationMirror mut = getTypeDeclarationBoundForMutability(type); + Set frameworkDefault = super.getTypeDeclarationBounds(type); + if (mut != null) { + frameworkDefault = replaceAnnotationInHierarchy(frameworkDefault, mut); } + return frameworkDefault; + } - /**Add immutable to the result type of a cast if the result type is implicitly immutable*/ - @Override - public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { - applyImmutableIfImplicitlyImmutable(type);// Must run before calling super method to respect existing annotation - return super.visitTypeCast(node, type); + private Set replaceAnnotationInHierarchy(Set set, AnnotationMirror mirror) { + Set result = new HashSet<>(set); + AnnotationMirror removeThis = getQualifierHierarchy().findAnnotationInSameHierarchy(set, mirror); + result.remove(removeThis); + result.add(mirror); + return result; + } + + public AnnotationMirror getTypeDeclarationBoundForMutability(TypeMirror type) { + // copied from inference real type factory with minor modification + // TODO too awkward. maybe overload isImplicitlyImmutableType + if (PICOTypeUtil.isImplicitlyImmutableType(toAnnotatedType(type, false))) { + return IMMUTABLE; + } + if (type.getKind() == TypeKind.ARRAY) { + return RECEIVER_DEPENDANT_MUTABLE; // if decided to use vpa for array, return RDM. } - /**Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are not guaranteed - to always have immutable annotation. If this happens, we manually add immutable to type. We use - addMissingAnnotations because we want to respect existing annotation on type*/ - private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) { - if (PICOTypeUtil.isImplicitlyImmutableType(type)) { - type.addMissingAnnotations(new HashSet<>(Arrays.asList(IMMUTABLE))); + // IMMUTABLE for enum w/o decl anno + if (type instanceof DeclaredType) { + Element ele = ((DeclaredType) type).asElement(); + if (ele.getKind() == ElementKind.ENUM) { + if (!AnnotationUtils.containsSameByName(getDeclAnnotations(ele), MUTABLE) && + !AnnotationUtils.containsSameByName(getDeclAnnotations(ele), RECEIVER_DEPENDANT_MUTABLE)) { // no decl anno + return IMMUTABLE; + } } } + return null; + } - private void applyCommitedIfSupported(AnnotatedTypeFactory annotatedTypeFactory, AnnotatedTypeMirror type) { - if (annotatedTypeFactory.isSupportedQualifier(COMMITED)) { - type.replaceAnnotation(COMMITED); - } + @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_DEPENDANT_MUTABLE)) { + AnnotatedTypeMirror enclosing = getAnnotatedType(TreePathUtil.enclosingClass(getPath(clause))); + AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY); + fromTypeTree.replaceAnnotation(mainBound); } + return fromTypeTree; } /**Apply defaults for static fields with non-implicitly immutable types*/ @@ -413,31 +433,6 @@ public PICOTreeAnnotator(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); } - @Override - public Void visitIdentifier(IdentifierTree node, AnnotatedTypeMirror annotatedTypeMirror) { - PICOTypeUtil.dragAnnotationFromBoundToExtendsAndImplements(node, annotatedTypeMirror, atypeFactory); - return super.visitIdentifier(node, annotatedTypeMirror); - } - - @Override - public Void visitMemberSelect(MemberSelectTree node, AnnotatedTypeMirror annotatedTypeMirror) { - PICOTypeUtil.dragAnnotationFromBoundToExtendsAndImplements(node, annotatedTypeMirror, atypeFactory); - return super.visitMemberSelect(node, annotatedTypeMirror); - } - - @Override - public Void visitParameterizedType(ParameterizedTypeTree node, AnnotatedTypeMirror annotatedTypeMirror) { - PICOTypeUtil.dragAnnotationFromBoundToExtendsAndImplements(node, annotatedTypeMirror, atypeFactory); - return super.visitParameterizedType(node, annotatedTypeMirror); - } - - @Override - public Void visitClass(ClassTree node, AnnotatedTypeMirror annotatedTypeMirror) { - // Apply @Immutable to enum element's bound - PICOTypeUtil.applyImmutableToEnumAndEnumConstant(annotatedTypeMirror); - return super.visitClass(node, annotatedTypeMirror); - } - // This adds @Immutable annotation to constructor return type if type declaration has @Immutable when the // constructor is accessed as a tree. @Override @@ -454,9 +449,15 @@ public Void visitMethod(MethodTree node, AnnotatedTypeMirror p) { public Void visitVariable(VariableTree node, AnnotatedTypeMirror annotatedTypeMirror) { VariableElement element = TreeUtils.elementFromDeclaration(node); PICOTypeUtil.addDefaultForField(atypeFactory, annotatedTypeMirror, element); - PICOTypeUtil.applyImmutableToEnumAndEnumConstant(annotatedTypeMirror); +// PICOTypeUtil.applyImmutableToEnumAndEnumConstant(annotatedTypeMirror); return super.visitVariable(node, annotatedTypeMirror); } + + @Override + public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { + type.replaceAnnotation(IMMUTABLE); + return null; + } } /**Type Annotators*/ @@ -476,10 +477,31 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { if (!ElementUtils.isStatic(t.getElement())) { if (PICOTypeUtil.isMethodOrOverridingMethod(t, "toString()", typeFactory) || PICOTypeUtil.isMethodOrOverridingMethod(t, "hashCode()", typeFactory)) { - t.getReceiverType().addMissingAnnotations(new HashSet<>(Arrays.asList(READONLY))); + assert t.getReceiverType() != null; + t.getReceiverType().replaceAnnotation(READONLY); } else if (PICOTypeUtil.isMethodOrOverridingMethod(t, "equals(java.lang.Object)", typeFactory)) { - t.getReceiverType().addMissingAnnotations(new HashSet<>(Arrays.asList(READONLY))); - t.getParameterTypes().get(0).addMissingAnnotations(new HashSet<>(Arrays.asList(READONLY))); + assert t.getReceiverType() != null; + t.getReceiverType().replaceAnnotation(READONLY); + t.getParameterTypes().get(0).replaceAnnotation(READONLY); + } + } + + // 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(), typeFactory)) { + switch (t.toString()) { + case "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().isAnnotatedInHierarchy(READONLY)) + t.getReceiverType().replaceAnnotation(READONLY); + // The return type will be fixed by SyntheticArrays anyway. + // Qualifiers added here will not have effect. + break; + } } } @@ -488,9 +510,51 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { } - public static class PICOImplicitsTypeAnnotator extends ImplicitsTypeAnnotator { + @Override + protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator() { + return new PICOQualifierForUseTypeAnnotator(this); + } + + // @DefaultQFU + 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(); + Set 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 PICOImplicitsTypeAnnotator(AnnotatedTypeFactory typeFactory) { + public PICODefaultForTypeAnnotator(AnnotatedTypeFactory typeFactory) { super(typeFactory); } @@ -512,7 +576,7 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { @Override protected Void scan(AnnotatedTypeMirror type, Void p) { // If underlying type is enum or enum constant, appy @Immutable to type - PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); +// PICOTypeUtil.applyImmutableToEnumAndEnumConstant(type); return super.scan(type, p); } } @@ -520,9 +584,72 @@ protected Void scan(AnnotatedTypeMirror type, Void 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 ImplicitsTypeAnnotator; But InheritedFromClassAnnotator cannot be inheritted because its + // 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 overriden + if (isSuperClause(path) && + (!mirror.isAnnotatedInHierarchy(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); +// System.err.println("ANNOT: ADDED DEFAULT FOR: " + mirror); + } + } + + @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/src/main/java/pico/typecheck/PICOAnnotationMirrorHolder.java b/src/main/java/pico/typecheck/PICOAnnotationMirrorHolder.java index e1ef081..478624c 100644 --- a/src/main/java/pico/typecheck/PICOAnnotationMirrorHolder.java +++ b/src/main/java/pico/typecheck/PICOAnnotationMirrorHolder.java @@ -9,7 +9,6 @@ import qual.PolyMutable; import qual.Readonly; import qual.ReceiverDependantMutable; -import qual.SubstitutablePolyMutable; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.util.Elements; @@ -23,7 +22,6 @@ public class PICOAnnotationMirrorHolder { public static AnnotationMirror MUTABLE; public static AnnotationMirror POLY_MUTABLE; public static AnnotationMirror RECEIVER_DEPENDANT_MUTABLE; - public static AnnotationMirror SUBSTITUTABLE_POLY_MUTABLE; public static AnnotationMirror IMMUTABLE; public static AnnotationMirror BOTTOM; public static AnnotationMirror COMMITED; @@ -34,7 +32,6 @@ public static void init(SourceChecker checker) { MUTABLE = AnnotationBuilder.fromClass(elements, Mutable.class); POLY_MUTABLE = AnnotationBuilder.fromClass(elements, PolyMutable.class); RECEIVER_DEPENDANT_MUTABLE = AnnotationBuilder.fromClass(elements, ReceiverDependantMutable.class); - SUBSTITUTABLE_POLY_MUTABLE = AnnotationBuilder.fromClass(elements, SubstitutablePolyMutable.class); IMMUTABLE = AnnotationBuilder.fromClass(elements, Immutable.class); BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class); diff --git a/src/main/java/pico/typecheck/PICOChecker.java b/src/main/java/pico/typecheck/PICOChecker.java index 8338604..6303429 100644 --- a/src/main/java/pico/typecheck/PICOChecker.java +++ b/src/main/java/pico/typecheck/PICOChecker.java @@ -14,7 +14,7 @@ public class PICOChecker extends InitializationChecker { public PICOChecker() { - super(true); + super(); } @Override diff --git a/src/main/java/pico/typecheck/PICOTransfer.java b/src/main/java/pico/typecheck/PICOTransfer.java index db53c31..ffa72df 100644 --- a/src/main/java/pico/typecheck/PICOTransfer.java +++ b/src/main/java/pico/typecheck/PICOTransfer.java @@ -1,7 +1,5 @@ package pico.typecheck; -import com.sun.source.tree.ClassTree; -import com.sun.source.tree.MethodTree; import com.sun.source.tree.VariableTree; import org.checkerframework.checker.initialization.InitializationTransfer; import org.checkerframework.dataflow.analysis.RegularTransferResult; @@ -9,7 +7,6 @@ import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.AssignmentNode; import org.checkerframework.dataflow.cfg.node.NullLiteralNode; -import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.javacutil.TreeUtils; import javax.lang.model.element.VariableElement; @@ -41,9 +38,4 @@ public TransferResult visitAssignment(AssignmentNode n, Tr TransferResult result = super.visitAssignment(n, in); return result; } - - @Override - protected void addFieldValues(PICOStore info, AnnotatedTypeFactory factory, ClassTree classTree, MethodTree methodTree) { - return; - } } diff --git a/src/main/java/pico/typecheck/PICOValidator.java b/src/main/java/pico/typecheck/PICOValidator.java index 9e042bf..e5b697f 100644 --- a/src/main/java/pico/typecheck/PICOValidator.java +++ b/src/main/java/pico/typecheck/PICOValidator.java @@ -6,19 +6,26 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; -import org.checkerframework.framework.source.Result; 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.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; +import pico.common.PICOTypeUtil; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ElementKind; import javax.lang.model.element.VariableElement; -import static pico.typecheck.PICOAnnotationMirrorHolder.BOTTOM; -import static pico.typecheck.PICOAnnotationMirrorHolder.IMMUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; +import java.util.Objects; +import java.util.Set; + +import static pico.typecheck.PICOAnnotationMirrorHolder.*; +import static pico.typecheck.PICOAnnotationMirrorHolder.MUTABLE; /** * Created by mier on 29/09/17. @@ -35,7 +42,41 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { checkStaticReceiverDependantMutableError(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) && + PICOAnnotatedTypeFactory.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) { + Set enclosingBound = + atypeFactory.getTypeDeclarationBounds( + Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()); + + Set declaredBound = + atypeFactory.getTypeDeclarationBounds(type.getUnderlyingType()); + + if(AnnotationUtils.containsSameByName(declaredBound, MUTABLE) + && type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) + && AnnotationUtils.containsSameByName(enclosingBound, MUTABLE)) { + return false; + } + } + } +// if (TreeUtils.isLocalVariable(tree)) { +// return true; +// } + + return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree); } @Override @@ -52,14 +93,15 @@ public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) { } private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) { - if (PICOTypeUtil.inStaticScope(visitor.getCurrentPath()) - && !"".contentEquals(TreeUtils.enclosingClass(visitor.getCurrentPath()).getSimpleName())// Exclude @RDM usages in anonymous classes + 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_DEPENDANT_MUTABLE)) { reportValidityResult("static.receiverdependantmutable.forbidden", type, tree); } } - /**Check that implicitly immutable type has immutable or bottom type. Dataflow might refine immtable type to @Bottom, + /**Check that implicitly immutable type has immutable or bottom type. Dataflow might refine immutable type to @Bottom, * so we accept @Bottom as a valid qualifier for implicitly immutable types*/ private void checkImplicitlyImmutableTypeError(AnnotatedTypeMirror type, Tree tree) { if (PICOTypeUtil.isImplicitlyImmutableType(type) && !type.hasAnnotation(IMMUTABLE) && !type.hasAnnotation(BOTTOM)) { @@ -79,7 +121,7 @@ private void checkOnlyOneAssignabilityModifierOnField(Tree tree) { } private void reportFieldMultipleAssignabilityModifiersError(VariableElement field) { - checker.report(Result.failure("one.assignability.invalid", field), field); + checker.reportError(field, "one.assignability.invalid", field); isValid = false; } } diff --git a/src/main/java/pico/typecheck/PICOViewpointAdapter.java b/src/main/java/pico/typecheck/PICOViewpointAdapter.java index fdb3d4d..3c275fc 100644 --- a/src/main/java/pico/typecheck/PICOViewpointAdapter.java +++ b/src/main/java/pico/typecheck/PICOViewpointAdapter.java @@ -6,7 +6,6 @@ import static pico.typecheck.PICOAnnotationMirrorHolder.POLY_MUTABLE; import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; -import static pico.typecheck.PICOAnnotationMirrorHolder.SUBSTITUTABLE_POLY_MUTABLE; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; @@ -19,11 +18,12 @@ import org.checkerframework.javacutil.BugInCF; import exceptions.UnkownImmutabilityQualifierException; +import pico.common.ExtendedViewpointAdapter; /** * Created by mier on 20/06/17. */ -public class PICOViewpointAdapter extends AbstractViewpointAdapter { +public class PICOViewpointAdapter extends AbstractViewpointAdapter implements ExtendedViewpointAdapter { public PICOViewpointAdapter(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); @@ -53,15 +53,39 @@ protected AnnotationMirror combineAnnotationWithAnnotation(AnnotationMirror rece } else if (AnnotationUtils.areSame(declaredAnnotation, BOTTOM)) { return BOTTOM; } else if (AnnotationUtils.areSame(declaredAnnotation, POLY_MUTABLE)) { - return SUBSTITUTABLE_POLY_MUTABLE; + return POLY_MUTABLE; } else if (AnnotationUtils.areSame(declaredAnnotation, RECEIVER_DEPENDANT_MUTABLE)) { return receiverAnnotation; } else { - throw new BugInCF("Unkown declared modifier: " + declaredAnnotation, new UnkownImmutabilityQualifierException()); + throw new BugInCF("Unknown declared modifier: " + declaredAnnotation, new UnkownImmutabilityQualifierException()); } } // // @Override +// protected AnnotatedTypeMirror combineAnnotationWithType(AnnotationMirror receiverAnnotation, AnnotatedTypeMirror declared) { +// boolean prevRdm = declared.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE); +// AnnotatedTypeMirror raw = super.combineAnnotationWithType(receiverAnnotation, declared); +// if(prevRdm && +// AnnotationUtils.containsSameByName(atypeFactory.getTypeDeclarationBounds(declared.getUnderlyingType()), MUTABLE) +// && (raw.hasAnnotation(IMMUTABLE) || raw.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE))) { +// raw.replaceAnnotation(MUTABLE); +// } +// return raw; +// } + + public AnnotatedTypeMirror rawCombineAnnotationWithType(AnnotationMirror anno, AnnotatedTypeMirror type) { +// System.err.println("VPA: " + anno + " ->" + type); + return combineAnnotationWithType(anno, type); + } + + @Override + public AnnotationMirror rawCombineAnnotationWithAnnotation(AnnotationMirror anno, AnnotationMirror type) { +// System.err.println("VPA: " + anno + " ->" + type); + return combineAnnotationWithAnnotation(anno, type); + } + + // +// @Override // protected AnnotationMirror getModifier(AnnotatedTypeMirror atm, AnnotatedTypeFactory f) { // return atm.getAnnotationInHierarchy(READONLY); // } diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 5249ae4..b79d865 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -12,6 +12,7 @@ import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Set; import javax.lang.model.element.AnnotationMirror; @@ -20,21 +21,23 @@ 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; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.checker.initialization.InitializationVisitor; import org.checkerframework.checker.initialization.qual.UnderInitialization; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.TypeValidator; -import org.checkerframework.framework.source.Result; -import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedMethodType; +import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror; 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.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypesUtils; @@ -51,6 +54,10 @@ import com.sun.source.tree.Tree.Kind; import com.sun.source.tree.UnaryTree; import com.sun.source.tree.VariableTree; +import pico.common.ExtendedViewpointAdapter; +import pico.common.PICOTypeUtil; +import pico.common.ViewpointAdapterGettable; +import qual.Immutable; /** * Created by mier on 20/06/17. @@ -81,31 +88,53 @@ protected TypeValidator createTypeValidator() { // (at least for types other than java.lang.Object) @Override public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { - AnnotationMirror declared = declarationType.getAnnotationInHierarchy(READONLY); - // No need to have special case for java.lang.Object, as it's not by default @Readonly anymore -// if (AnnotationUtils.areSame(declared, atypeFactory.READONLY)) { -// // Special case for java.lang.Object. Usually @Readonly is never used as a bound annotation for a -// // TypeElement. But we want to have @Readonly as the default for java.lang.Object. There is no way -// // of doing this using any exsisting family of @DefaultFor qualifiers, but @ImplicitFor annotation -// // does the trick. But the side effect is, we can't write @ReceiverDependantMutable, which is the -// // correct bound for Object element, in jdk.astub, because otherwise it makes all java.lang.Object -// // to be @ReceiverDependantMutable; Another side effect is here @Readonly is passed into here as -// // the element type for java.lang.Object. So we have to have this special case only for java.lang. -// // Object -// return true; + // FIXME workaround for typecheck BOTTOM + if (useType.hasAnnotation(BOTTOM)) { + return true; + } + // FIXME workaround for poly anno, remove after fix substitutable poly and add poly vp rules + if (useType.hasAnnotation(POLY_MUTABLE)) { + return true; + } + +// // allow RDM on mutable fields with enclosing class bounded with mutable +// if (tree instanceof VariableTree && useType.isDeclaration()) { +// VariableElement element = TreeUtils.elementFromDeclaration((VariableTree)tree); +// if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingClass(element) != null) { +// Set enclosingBound = +// atypeFactory.getTypeDeclarationBounds( +// Objects.requireNonNull(ElementUtils.enclosingClass(element)).asType()); +// +// if(declarationType.hasAnnotation(MUTABLE) +// && useType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) +// && AnnotationUtils.containsSameByName(enclosingBound, MUTABLE)) { +// return true; +// } +// } +// // } - if (AnnotationUtils.areSame(declared, RECEIVER_DEPENDANT_MUTABLE)) { + + AnnotationMirror declared = declarationType.getAnnotationInHierarchy(READONLY); + AnnotationMirror used = useType.getAnnotationInHierarchy(READONLY); + + return isAdaptedSubtype(used, declared); + } + + @Override + public boolean isValidUse(AnnotatedTypeMirror.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); + } + + static private boolean isAnnoValidUse(AnnotationMirror declared, AnnotationMirror used) { + if (AnnotationUtils.areSame(declared, RECEIVER_DEPENDANT_MUTABLE) || AnnotationUtils.areSame(declared, READONLY)) { // Element is declared with @ReceiverDependantMutable bound, any instantiation is allowed. We don't use // a subtype check to validate the correct usage here. Because @Readonly is the super type of // @ReceiverDependantMutable, but it's still considered valid usage. return true; } - // At this point, element type can only be @Mutable or @Immutable. Otherwise, it's a problem in - // PICOVisitor#processorClassTree(ClassTree) - assert AnnotationUtils.areSame(declared, MUTABLE) || AnnotationUtils.areSame(declared, IMMUTABLE); - - AnnotationMirror used = useType.getAnnotationInHierarchy(READONLY); - assert AnnotationUtils.areSame(declared, MUTABLE) || AnnotationUtils.areSame(declared, IMMUTABLE); if (AnnotationUtils.areSame(declared, MUTABLE) && !(AnnotationUtils.areSame(used, IMMUTABLE) || AnnotationUtils.areSame(used, RECEIVER_DEPENDANT_MUTABLE))) { @@ -121,9 +150,15 @@ public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclar return false; } + private boolean isAdaptedSubtype(AnnotationMirror lhs, AnnotationMirror rhs) { + ExtendedViewpointAdapter vpa = ((ViewpointAdapterGettable)atypeFactory).getViewpointAdapter(); + AnnotationMirror adapted = vpa.rawCombineAnnotationWithAnnotation(lhs, rhs); + return atypeFactory.getQualifierHierarchy().isSubtype(adapted, lhs); + } + @Override protected void commonAssignmentCheck( - Tree varTree, ExpressionTree valueExp, String errorKey) { + Tree varTree, ExpressionTree valueExp, String errorKey, Object... extraArgs) { AnnotatedTypeMirror var = atypeFactory.getAnnotatedTypeLhs(varTree); assert var != null : "no variable found for tree: " + varTree; @@ -131,8 +166,6 @@ protected void commonAssignmentCheck( return; } - checkAssignability(var, varTree); - if (varTree instanceof VariableTree) { VariableElement element = TreeUtils.elementFromDeclaration((VariableTree) varTree); if (element.getKind() == ElementKind.FIELD && !ElementUtils.isStatic(element)) { @@ -155,8 +188,10 @@ protected void commonAssignmentCheck( commonAssignmentCheck(var, valueExp, errorKey); } + + @Override - protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) { + protected void checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) { // TODO Is the copied code really needed? /*Copied Code Start*/ AnnotatedDeclaredType returnType = (AnnotatedDeclaredType) constructor.getReturnType(); @@ -178,14 +213,22 @@ protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, A } /*Copied Code End*/ + // TODO fix inference counterpart, not here +// // CF base check disabled by InitializationVisitor +// // if no explicit anno it must inherited from class decl +// AnnotationMirror declAnno = constructor.getReturnType().getAnnotationInHierarchy(READONLY); +// AnnotationMirror useAnno = invocation.getAnnotationInHierarchy(READONLY); +// declAnno = declAnno == null ? MUTABLE : declAnno; +// +// if(useAnno != null && !AnnotationUtils.areSameByName(declAnno, POLY_MUTABLE) && !isAdaptedSubtype(useAnno, declAnno)) { +// checker.reportError(newClassTree, "type.invalid.annotations.on.use", declAnno, useAnno); +// } + // The immutability return qualifier of the constructor (returnType) must be supertype of the // constructor invocation immutability qualifier(invocation). - if (!atypeFactory.getTypeHierarchy().isSubtype(invocation, returnType, READONLY)) { - checker.report(Result.failure( - "constructor.invocation.invalid", invocation, returnType), newClassTree); - return false; + if (!atypeFactory.getQualifierHierarchy().isSubtype(invocation.getAnnotationInHierarchy(READONLY), returnType.getAnnotationInHierarchy(READONLY))) { + checker.reportError(newClassTree, "constructor.invocation.invalid", invocation, returnType); } - return true; } @Override @@ -196,9 +239,13 @@ public Void visitMethod(MethodTree node, Void p) { if (TreeUtils.isConstructor(node)) { AnnotatedDeclaredType constructorReturnType = (AnnotatedDeclaredType) executableType.getReturnType(); if (constructorReturnType.hasAnnotation(READONLY) || constructorReturnType.hasAnnotation(POLY_MUTABLE)) { - checker.report(Result.failure("constructor.return.invalid", constructorReturnType), node); + checker.reportError(node, "constructor.return.invalid", constructorReturnType); return super.visitMethod(node, p); } + // if no explicit anno it must inherit from class decl so identical + // => if not the same must not inherited from class decl + // => no need to check the source of the anno + } else { AnnotatedDeclaredType declareReceiverType = executableType.getReceiverType(); if (declareReceiverType != null) { @@ -210,7 +257,7 @@ public Void visitMethod(MethodTree node, Void p) { // 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.report(Result.failure("method.receiver.incompatible", declareReceiverType), node); + checker.reportError(node,"method.receiver.incompatible", declareReceiverType); } } } @@ -336,11 +383,11 @@ private boolean isInitializingReceiverDependantMutableOrImmutableObject(Annotate private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { if (variable.getKind() == Kind.MEMBER_SELECT) { - checker.report(Result.failure("illegal.field.write", receiverType), TreeUtils.getReceiverTree(variable)); + checker.reportError(TreeUtils.getReceiverTree(variable), "illegal.field.write", receiverType); } else if (variable.getKind() == Kind.IDENTIFIER) { - checker.report(Result.failure("illegal.field.write", receiverType), node); + checker.reportError(node, "illegal.field.write", receiverType); } else if (variable.getKind() == Kind.ARRAY_ACCESS) { - checker.report(Result.failure("illegal.array.write", receiverType), ((ArrayAccessTree)variable).getExpression()); + checker.reportError(((ArrayAccessTree)variable).getExpression(), "illegal.array.write", receiverType); } else { throw new BugInCF("Unknown assignment variable at: ", node); } @@ -349,15 +396,45 @@ private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, An @Override public Void visitVariable(VariableTree node, Void p) { VariableElement element = TreeUtils.elementFromDeclaration(node); - if (element != null && element.getKind() == ElementKind.FIELD) { - AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(element); + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(element); + if (element.getKind() == ElementKind.FIELD) { if (type.hasAnnotation(POLY_MUTABLE)) { - checker.report(Result.failure("field.polymutable.forbidden", element), node); + checker.reportError(node, "field.polymutable.forbidden", element); } } + // When to check: + // bound == Immutable, OR + // not FIELD, OR + // top anno not RDM + // TODO use base cf check methods + AnnotationMirror declAnno = atypeFactory.getTypeDeclarationBoundForMutability(type.getUnderlyingType()); + if (declAnno != null && AnnotationUtils.areSameByName(declAnno, IMMUTABLE) || + element.getKind() != ElementKind.FIELD || + !type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { + checkAndReportInvalidAnnotationOnUse(type, node); + } return super.visitVariable(node, p); } + private void checkAndReportInvalidAnnotationOnUse(AnnotatedTypeMirror type, Tree node) { + AnnotationMirror useAnno = type.getAnnotationInHierarchy(READONLY); + // FIXME rm after poly vp + if (useAnno != null && AnnotationUtils.areSame(useAnno, POLY_MUTABLE)) { + return; + } + if (useAnno != null && !PICOTypeUtil.isImplicitlyImmutableType(type) && type.getKind() != TypeKind.ARRAY) { // TODO: annotate the use instead of using this + AnnotationMirror defaultAnno = MUTABLE; + for (AnnotationMirror anno : atypeFactory.getTypeDeclarationBounds(atypeFactory.getAnnotatedType(node).getUnderlyingType())) { + if (atypeFactory.getQualifierHierarchy().isSubtype(anno, READONLY) && !AnnotationUtils.areSame(anno, READONLY)) { + defaultAnno = anno; + } + } + if (!isAdaptedSubtype(useAnno, defaultAnno)) { + checker.reportError(node, "type.invalid.annotations.on.use", defaultAnno, useAnno); + } + } + } + @Override public Void visitNewClass(NewClassTree node, Void p) { checkNewInstanceCreation(node); @@ -375,77 +452,29 @@ private void checkNewInstanceCreation(Tree node) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); if (!(type.hasAnnotation(IMMUTABLE) || type.hasAnnotation(MUTABLE) || type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) || type.hasAnnotation(POLY_MUTABLE))) { - checker.report(Result.failure("pico.new.invalid", type), node); + checker.reportError(node, "pico.new.invalid", type); } } @Override public Void visitMethodInvocation(MethodInvocationTree node, Void p) { super.visitMethodInvocation(node, p); - ParameterizedMethodType mfuPair = + ParameterizedExecutableType mfuPair = atypeFactory.methodFromUse(node); - AnnotatedExecutableType invokedMethod = mfuPair.methodType; + 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.isSuperCall(node)) { + if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperConstructorCall(node)) { checkMethodInvocability(invokedMethod, node); } return null; } - // TODO Find a better way to inject saveFbcViolatedMethods instead of copying lots of code from super method - @Override - protected void checkMethodInvocability(AnnotatedExecutableType method, MethodInvocationTree node) { - // Check subclass constructor calls the correct super class constructor: mutable calls mutable; immutable - // calls immutable; any calls receiverdependantmutable - if (method.getElement().getKind() == ElementKind.CONSTRUCTOR) { - AnnotatedTypeMirror subClassConstructorReturnType = atypeFactory.getReceiverType(node); - AnnotatedTypeMirror superClassConstructorReturnType = method.getReturnType(); - // superClassConstructorReturnType is already the result of viewpoint adaptation, so subClassConstructorReturnType <: - // superClassConstructorReturnType is enough to determine the super constructor invocation is valid or not - if (!atypeFactory.getTypeHierarchy().isSubtype(subClassConstructorReturnType, superClassConstructorReturnType, READONLY)) { - checker.report( - Result.failure( - "super.constructor.invocation.incompatible", subClassConstructorReturnType, superClassConstructorReturnType), node); - } - return; - } - - /*Copied Code Starts*/ - if (method.getReceiverType() == null) { - // Static methods don't have a receiver. - return; - } - - AnnotatedTypeMirror methodReceiver = method.getReceiverType().getErased(); - AnnotatedTypeMirror treeReceiver = methodReceiver.shallowCopy(false); - AnnotatedTypeMirror rcv = atypeFactory.getReceiverType(node); - - treeReceiver.addAnnotations(rcv.getEffectiveAnnotations()); - - if (!skipReceiverSubtypeCheck(node, methodReceiver, rcv) - && !atypeFactory.getTypeHierarchy().isSubtype(treeReceiver, methodReceiver)) { - checker.report( - Result.failure( - "method.invocation.invalid", - TreeUtils.elementFromUse(node), - treeReceiver.toString(), - methodReceiver.toString()), - node); - /*Difference Starts*/ - if (shouldOutputFbcError) { - saveFbcViolatedMethods(TreeUtils.elementFromUse(node), treeReceiver.toString(), methodReceiver.toString()); - } - /*Different Ends*/ - } - /*Copied Code Ends*/ - } - private void saveFbcViolatedMethods(ExecutableElement method, String actualReceiver, String declaredReceiver) { if (actualReceiver.contains("@UnderInitialization") && declaredReceiver.contains("@Initialized")) { - String key = ElementUtils.enclosingClass(method) + "#" + method; + String key = ElementUtils.enclosingTypeElement(method) + "#" + method; Integer times = fbcViolatedMethods.get(key) == null ? 1 : fbcViolatedMethods.get(key) + 1; fbcViolatedMethods.put(key, times); } @@ -499,66 +528,118 @@ public void processClassTree(ClassTree node) { AnnotatedDeclaredType bound = PICOTypeUtil.getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); // Has to be either @Mutable, @ReceiverDependantMutable or @Immutable, nothing else if (!bound.hasAnnotation(MUTABLE) && !bound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) && !bound.hasAnnotation(IMMUTABLE)) { - checker.report(Result.failure("class.bound.invalid", bound), node); + checker.reportError(node, "class.bound.invalid", bound); return;// Doesn't process the class tree anymore } - if (!checkCompatabilityBetweenBoundAndSuperClassesBounds(node, typeElement, bound)) { - return; - } - if (!checkCompatabilityBetweenBoundAndExtendsImplements(node, bound)) { - return; + // Issue warnings on implicit shallow immutable: + // Condition: + // * Class decl == Immutable + // * Member is field + // * Member's declared bound == Mutable + // * Member's use anno == null + if (bound.hasAnnotation(IMMUTABLE)) { + 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.isAnnotatedInHierarchy(READONLY)) { + checker.reportWarning(member, "implicit.shallow.immutable"); + } + + } + } } - // Reach this point iff 1) bound annotation is one of mutable, rdm or immutable; - // 2) bound is compatible with bounds on super types. Only continue if bound check - // passed. Reaching here already means having passed bound check. +// // field of mutable class cannot use RDM in immutable class +// // Condition: +// // * Class decl == Immutable +// // * Member is field (variable) +// // * Member's declared bound == Mutable +// // * Member's use anno == RDM +// if (bound.hasAnnotation(IMMUTABLE)) { +// for(Tree member : node.getMembers()) { +// if(member.getKind() == Kind.VARIABLE) { +// AnnotatedTypeMirror fieldAtm = atypeFactory.getAnnotatedType(member); +// if (fieldAtm.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE) && +// AnnotationUtils.containsSameByName(atypeFactory.getTypeDeclarationBounds(fieldAtm.getUnderlyingType()), MUTABLE)) { +// checker.reportError(member, "test-key-1"); +// } +// } +// } +// } super.processClassTree(node); } - private boolean checkCompatabilityBetweenBoundAndSuperClassesBounds(ClassTree node, TypeElement typeElement, AnnotatedDeclaredType bound) { - // Must have compatible bound annotation as the direct super types - List superBounds = PICOTypeUtil.getBoundTypesOfDirectSuperTypes(typeElement, atypeFactory); - for (AnnotatedDeclaredType superBound : superBounds) { - // If annotation on super bound is @ReceiverDependantMutable, then any valid bound is permitted. - if (superBound.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) continue; - // super bound is either @Mutable or @Immutable. Must be the subtype of the corresponding super bound - if (!atypeFactory.getQualifierHierarchy().isSubtype( - bound.getAnnotationInHierarchy(READONLY), superBound.getAnnotationInHierarchy(READONLY))) { - checker.report(Result.failure("subclass.bound.incompatible", bound, superBound), node); - return false; - } + /** + * 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() + .isSubtype(constructorTypeMirror, superTypeMirror)) { + checker.reportError(superCall, errorKey, constructorTypeMirror, superCall, superTypeMirror); } - return true; + super.checkThisOrSuperConstructorCall(superCall, errorKey); } - private boolean checkCompatabilityBetweenBoundAndExtendsImplements(ClassTree node, AnnotatedDeclaredType bound) { - boolean hasSame; - Tree ext = node.getExtendsClause(); - if (ext != null) { - AnnotatedTypeMirror extendsType = atypeFactory.getAnnotatedType(ext); - hasSame = bound.getAnnotations().size() == extendsType.getAnnotations().size() - && AnnotationUtils.areSame(extendsType.getAnnotationInHierarchy(READONLY), - bound.getAnnotationInHierarchy(READONLY)); - if (!hasSame) { - checker.report(Result.failure("bound.extends.incompatabile"), node); - return false; - } + @Override + protected CastSafeKind isSafeDowncast( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + Set castAnnos = castType.getEffectiveAnnotations(); + Set exprAnnos = exprType.getEffectiveAnnotations(); + QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); + + if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { + return CastSafeKind.NOT_DOWNCAST; } - List impls = node.getImplementsClause(); - if (impls != null) { - for (Tree im : impls) { - AnnotatedTypeMirror implementsType = atypeFactory.getAnnotatedType(im); - hasSame = bound.getAnnotations().size() == implementsType.getAnnotations().size() - && AnnotationUtils.areSame(implementsType.getAnnotationInHierarchy(READONLY), - bound.getAnnotationInHierarchy(READONLY)); - if (!hasSame) { - checker.report(Result.failure("bound.implements.incompatabile"), node); - return false; - } + final TypeKind castTypeKind = castType.getKind(); + + if (castTypeKind == TypeKind.DECLARED) { + AnnotatedDeclaredType castDeclared = (AnnotatedDeclaredType) castType; + AnnotationMirror bound = + qualifierHierarchy.findAnnotationInHierarchy(atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()), READONLY); + + if (AnnotationUtils.areSame(castDeclared.getAnnotationInHierarchy(READONLY), bound)) { + return CastSafeKind.SAFE; } } - return true; + return CastSafeKind.WARNING; + } + + @Override + protected void 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; + } + super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs); + } } diff --git a/src/main/java/pico/typecheck/jdk.astub b/src/main/java/pico/typecheck/jdk.astub index 9091e38..401c0ce 100644 --- a/src/main/java/pico/typecheck/jdk.astub +++ b/src/main/java/pico/typecheck/jdk.astub @@ -113,6 +113,11 @@ interface Collection { boolean contains(@Readonly Collection this, @Readonly Object o); } +@ReceiverDependantMutable +public abstract class AbstractCollection implements Collection { + public abstract int size(@Readonly AbstractCollection this); +} + @ReceiverDependantMutable class ArrayList { @ReceiverDependantMutable ArrayList(); @@ -214,6 +219,7 @@ class Arrays { 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 T[] copyOf(T @Readonly [] original, int newLength); } class Objects { diff --git a/src/main/java/pico/typecheck/messages.properties b/src/main/java/pico/typecheck/messages.properties index 105fe05..db36cfa 100644 --- a/src/main/java/pico/typecheck/messages.properties +++ b/src/main/java/pico/typecheck/messages.properties @@ -1,9 +1,8 @@ constructor.invocation.invalid=Cannot not instantiate type: %s out of constructor: %s constructor.return.invalid=Invalid constructor return type: %s -method.receiver.incompatible -class.bound.invalid -subclass.bound.incompatible -super.constructor.invocation.incompatible=Subclass constructor: %s is not compatible with super class constructor: %s +method.receiver.incompatible=Incompatible method receiver: %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.receiverdependantmutable.forbidden=%s is forbidden in static context diff --git a/src/main/java/qual/Bottom.java b/src/main/java/qual/Bottom.java index cf17cd4..e6f41e3 100644 --- a/src/main/java/qual/Bottom.java +++ b/src/main/java/qual/Bottom.java @@ -1,22 +1,18 @@ package qual; import org.checkerframework.framework.qual.DefaultFor; -import org.checkerframework.framework.qual.DefaultInUncheckedCodeFor; -import org.checkerframework.framework.qual.ImplicitFor; -import org.checkerframework.framework.qual.LiteralKind; 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; -@SubtypeOf({Mutable.class, Immutable.class, PolyMutable.class, ReceiverDependantMutable.class}) -@DefaultFor({ TypeUseLocation.LOWER_BOUND }) -@ImplicitFor(literals = {LiteralKind.NULL}) +@SubtypeOf({Mutable.class, Immutable.class, ReceiverDependantMutable.class}) +@DefaultFor(value = { TypeUseLocation.LOWER_BOUND }, typeKinds = {TypeKind.NULL}) @Documented @Retention(RetentionPolicy.RUNTIME) // Stop allowing any explicit usage of @Bottom qualifier in source. As it causes difficulty to @@ -26,5 +22,4 @@ // qualifier than @Bottom explicitly on explicit lower bound to have different-than-default type. @Target({}) @TargetLocations({}) -@DefaultInUncheckedCodeFor({TypeUseLocation.RETURN}) public @interface Bottom {} diff --git a/src/main/java/qual/Immutable.java b/src/main/java/qual/Immutable.java index eb66e07..2e79896 100644 --- a/src/main/java/qual/Immutable.java +++ b/src/main/java/qual/Immutable.java @@ -1,10 +1,12 @@ package qual; -import org.checkerframework.framework.qual.ImplicitFor; +import org.checkerframework.framework.qual.DefaultFor; +import org.checkerframework.framework.qual.QualifierForLiterals; import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.qual.TypeKind; +import org.checkerframework.framework.qual.UpperBoundFor; import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; @@ -17,10 +19,20 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -@ImplicitFor(typeNames={Enum.class, String.class, Double.class, Boolean.class, Byte.class, +@DefaultFor(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}, - literals = { LiteralKind.PRIMITIVE, LiteralKind.STRING}, - types = { TypeKind.INT, TypeKind.BYTE, TypeKind.SHORT, TypeKind.BOOLEAN, + 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 + }) public @interface Immutable {} diff --git a/src/main/java/qual/PolyMutable.java b/src/main/java/qual/PolyMutable.java index 54f45ca..48cc878 100644 --- a/src/main/java/qual/PolyMutable.java +++ b/src/main/java/qual/PolyMutable.java @@ -1,6 +1,6 @@ package qual; -import org.checkerframework.framework.qual.SubtypeOf; +import org.checkerframework.framework.qual.PolymorphicQualifier; import java.lang.annotation.Documented; import java.lang.annotation.ElementType; @@ -8,8 +8,8 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -@SubtypeOf(Readonly.class) @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@PolymorphicQualifier(Readonly.class) public @interface PolyMutable {} diff --git a/src/main/java/qual/Readonly.java b/src/main/java/qual/Readonly.java index f80ef75..73c7e06 100644 --- a/src/main/java/qual/Readonly.java +++ b/src/main/java/qual/Readonly.java @@ -1,9 +1,6 @@ package qual; -import org.checkerframework.framework.qual.DefaultInUncheckedCodeFor; -import org.checkerframework.framework.qual.ImplicitFor; import org.checkerframework.framework.qual.SubtypeOf; -import org.checkerframework.framework.qual.TypeUseLocation; import java.lang.annotation.Documented; import java.lang.annotation.ElementType; @@ -15,5 +12,4 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -@DefaultInUncheckedCodeFor({TypeUseLocation.PARAMETER, TypeUseLocation.RECEIVER}) public @interface Readonly {} diff --git a/src/main/java/qual/SubstitutablePolyMutable.java b/src/main/java/qual/SubstitutablePolyMutable.java deleted file mode 100644 index 6620c5c..0000000 --- a/src/main/java/qual/SubstitutablePolyMutable.java +++ /dev/null @@ -1,15 +0,0 @@ -package qual; - -import org.checkerframework.framework.qual.PolymorphicQualifier; - -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; - -@PolymorphicQualifier(Readonly.class) -@Documented -@Retention(RetentionPolicy.RUNTIME) -@Target({}) -public @interface SubstitutablePolyMutable {} diff --git a/src/test/java/pico/ImmutabilityInferenceInitialTypecheckTest.java b/src/test/java/pico/ImmutabilityInferenceInitialTypecheckTest.java new file mode 100644 index 0000000..3d3bcac --- /dev/null +++ b/src/test/java/pico/ImmutabilityInferenceInitialTypecheckTest.java @@ -0,0 +1,22 @@ +package pico; + +import org.checkerframework.framework.test.CheckerFrameworkPerFileTest; +import org.checkerframework.framework.test.TestUtilities; +import org.junit.runners.Parameterized.Parameters; +import pico.inference.PICOInferenceChecker; + +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +public class ImmutabilityInferenceInitialTypecheckTest extends CheckerFrameworkPerFileTest { + public ImmutabilityInferenceInitialTypecheckTest(File testFile) { + super(testFile, PICOInferenceChecker.class, "", "-Anomsgtext", + "-Anocheckjdk", "-d", "testTmp/typecheck"); + } + + @Parameters + public static List getTestFiles(){ + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "typecheck")); + } +} diff --git a/src/test/java/pico/ImmutabilityInferenceTest.java b/src/test/java/pico/ImmutabilityInferenceTest.java index 59b88a8..47e5fdb 100644 --- a/src/test/java/pico/ImmutabilityInferenceTest.java +++ b/src/test/java/pico/ImmutabilityInferenceTest.java @@ -17,13 +17,15 @@ public class ImmutabilityInferenceTest extends CFInferenceTest { public ImmutabilityInferenceTest(File testFile) { super(testFile, PICOInferenceChecker.class, "", - "-Anomsgtext", "-Astubs=src/main/java/pico/typecheck/jdk.astub", "-d", "testdata/inference/inferrable"); + "-Anomsgtext", + "-Astubs=src/main/java/pico/typecheck/jdk.astub", + "-d", "testdata/inference/inferrable"); } @Override public Pair> getSolverNameAndOptions() { - return Pair.> of(PICOSolverEngine.class.getCanonicalName(), - new ArrayList(Arrays.asList("useGraph=false", "collectStatistic=true"))); + return Pair.of(PICOSolverEngine.class.getCanonicalName(), + new ArrayList<>(Arrays.asList("useGraph=false", "collectStatistic=true"))); } @Override @@ -33,8 +35,7 @@ public boolean useHacks() { @Parameters public static List getTestFiles(){ - List testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests(); - testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testinput", "inference/inferrable")); - return testfiles; + //InferenceTestUtilities.findAllSystemTests(); + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "inference/inferrable")); } } diff --git a/src/test/java/pico/ImmutabilityReImInferenceTest.java b/src/test/java/pico/ImmutabilityReImInferenceTest.java new file mode 100644 index 0000000..c72cffa --- /dev/null +++ b/src/test/java/pico/ImmutabilityReImInferenceTest.java @@ -0,0 +1,42 @@ +package pico; + +import checkers.inference.test.CFInferenceTest; +import org.checkerframework.framework.test.TestUtilities; +import org.checkerframework.javacutil.Pair; +import org.junit.Ignore; +import org.junit.runners.Parameterized.Parameters; +import pico.inference.PICOInferenceChecker; +import pico.inference.solver.PICOSolverEngine; + +import java.io.File; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +@SuppressWarnings("initialization") +public class ImmutabilityReImInferenceTest extends CFInferenceTest { + + public ImmutabilityReImInferenceTest(File testFile) { + super(testFile, PICOInferenceChecker.class, "", + "-Anomsgtext", + "-Astubs=src/main/java/pico/inference/jdk.astub", + "-d", "testdata/reiminfer"); + } + + @Override + public Pair> getSolverNameAndOptions() { + return Pair.of(PICOSolverEngine.class.getCanonicalName(), + new ArrayList<>(Arrays.asList("useGraph=false", "collectStatistic=true"))); + } + + @Override + public boolean useHacks() { + return true; + } + + @Parameters + public static List getTestFiles(){ + //InferenceTestUtilities.findAllSystemTests(); + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "reiminfer")); + } +} diff --git a/src/test/java/pico/ImmutabilityTypecheckBaseAllSystemsTest.java b/src/test/java/pico/ImmutabilityTypecheckBaseAllSystemsTest.java new file mode 100644 index 0000000..4ad7223 --- /dev/null +++ b/src/test/java/pico/ImmutabilityTypecheckBaseAllSystemsTest.java @@ -0,0 +1,25 @@ +package pico; + +import org.checkerframework.framework.test.CheckerFrameworkPerFileTest; +import org.checkerframework.framework.test.TestUtilities; +import org.junit.Ignore; +import org.junit.runners.Parameterized.Parameters; +import pico.typecheck.PICOChecker; + +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +@Ignore +public class ImmutabilityTypecheckBaseAllSystemsTest extends CheckerFrameworkPerFileTest { + public ImmutabilityTypecheckBaseAllSystemsTest(File testFile) { + super(testFile, PICOChecker.class, "", "-Anomsgtext", + "-Anocheckjdk", "-d", "testTmp/typecheck"); + } + + @Parameters + public static List getTestFiles(){ + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles( + "../checker-framework/checker/tests", "all-systems")); + } +} diff --git a/src/test/java/pico/ImmutabilityTypecheckTests.java b/src/test/java/pico/ImmutabilityTypecheckExtendedTest.java similarity index 62% rename from src/test/java/pico/ImmutabilityTypecheckTests.java rename to src/test/java/pico/ImmutabilityTypecheckExtendedTest.java index a07d004..dc7017f 100644 --- a/src/test/java/pico/ImmutabilityTypecheckTests.java +++ b/src/test/java/pico/ImmutabilityTypecheckExtendedTest.java @@ -9,16 +9,14 @@ import java.util.ArrayList; import java.util.List; -public class ImmutabilityTypecheckTests extends CheckerFrameworkPerFileTest { - public ImmutabilityTypecheckTests(File testFile) { +public class ImmutabilityTypecheckExtendedTest extends CheckerFrameworkPerFileTest { + public ImmutabilityTypecheckExtendedTest(File testFile) { super(testFile, PICOChecker.class, "", "-Anomsgtext", "-Anocheckjdk", "-d", "testTmp/typecheck"); } @Parameters public static List getTestFiles(){ - List testfiles = new ArrayList<>(); - testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testinput", "typecheck")); - return testfiles; + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "inference/inferrable")); } } diff --git a/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java b/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java new file mode 100644 index 0000000..eb7857a --- /dev/null +++ b/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java @@ -0,0 +1,23 @@ +package pico; + +import org.checkerframework.framework.test.CheckerFrameworkPerFileTest; +import org.checkerframework.framework.test.TestUtilities; +import org.junit.Ignore; +import org.junit.runners.Parameterized.Parameters; +import pico.typecheck.PICOChecker; + +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +public class ImmutabilityTypecheckGlacierTest extends CheckerFrameworkPerFileTest { + public ImmutabilityTypecheckGlacierTest(File testFile) { + super(testFile, PICOChecker.class, "", "-Anomsgtext", + "-Anocheckjdk", "-d", "testTmp/glacier"); + } + + @Parameters + public static List getTestFiles(){ + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "glacier")); + } +} diff --git a/src/test/java/pico/ImmutabilityTypecheckTest.java b/src/test/java/pico/ImmutabilityTypecheckTest.java new file mode 100644 index 0000000..bf054f4 --- /dev/null +++ b/src/test/java/pico/ImmutabilityTypecheckTest.java @@ -0,0 +1,22 @@ +package pico; + +import org.checkerframework.framework.test.CheckerFrameworkPerFileTest; +import org.checkerframework.framework.test.TestUtilities; +import org.junit.runners.Parameterized.Parameters; +import pico.typecheck.PICOChecker; + +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +public class ImmutabilityTypecheckTest extends CheckerFrameworkPerFileTest { + public ImmutabilityTypecheckTest(File testFile) { + super(testFile, PICOChecker.class, "", "-Anomsgtext", + "-Anocheckjdk", "-d", "testTmp/typecheck"); + } + + @Parameters + public static List getTestFiles(){ + return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "typecheck")); + } +} diff --git a/testinput/glacier/ArrayClone.java b/testinput/glacier/ArrayClone.java new file mode 100644 index 0000000..e9a16ab --- /dev/null +++ b/testinput/glacier/ArrayClone.java @@ -0,0 +1,7 @@ +// Change to PICO; array clone adaption. +import qual.*; + +public class ArrayClone { + @Immutable Object @Immutable [] array = new @Immutable Object @Immutable [0]; + @Immutable Object @Immutable [] arrayClone = array.clone(); +} \ No newline at end of file diff --git a/testinput/glacier/ArrayCopy.java b/testinput/glacier/ArrayCopy.java new file mode 100644 index 0000000..ba4e8f4 --- /dev/null +++ b/testinput/glacier/ArrayCopy.java @@ -0,0 +1,18 @@ +// @skip-test +// Typecheck: Failed +// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable. +// strange enough, seems other signatures are got from stubs. +import qual.Immutable; + + +public class ArrayCopy { + public void takeArray(@Immutable Object @Immutable [] array) { + } + + public void passArray() { + @Immutable Object array[] = new @Immutable Object[5]; + + takeArray(array.clone()); + } + +} \ No newline at end of file diff --git a/testinput/glacier/ArrayParameter.java b/testinput/glacier/ArrayParameter.java new file mode 100644 index 0000000..81f77b4 --- /dev/null +++ b/testinput/glacier/ArrayParameter.java @@ -0,0 +1,22 @@ +import qual.*; +import java.util.Arrays; + + +class Array { + public static T[] add(final T @Readonly[] array, final T entry) { + final int s = array.length; + final T[] t = Arrays.copyOf(array, s + 1); + t[s] = entry; + return t; + } +} + + +public class ArrayParameter { + final @Immutable Object @Immutable [] keys = new @Immutable Object @Immutable [0]; + + + public void passArray(@Immutable Object k) { + Array.add(keys, k); + } +} \ No newline at end of file diff --git a/testinput/glacier/Arrays.java b/testinput/glacier/Arrays.java new file mode 100644 index 0000000..3fde23c --- /dev/null +++ b/testinput/glacier/Arrays.java @@ -0,0 +1,21 @@ +package glacier; + +public class Arrays { + int [] intArray; + + public Arrays() { + + } + + public int[] getData() { + return intArray; + } + + public byte[] getByteData() { + return new byte[0]; + } + + public void setData() { + intArray[0] = 42; + } +} \ No newline at end of file diff --git a/testinput/glacier/BooleanSubtyping.java b/testinput/glacier/BooleanSubtyping.java new file mode 100644 index 0000000..dcae5b7 --- /dev/null +++ b/testinput/glacier/BooleanSubtyping.java @@ -0,0 +1,16 @@ +public class BooleanSubtyping { + public enum CellType { + BLANK(3), + NUMBER(0); + + private int value; + private CellType(int value) { + this.value = value; + } + } + + public boolean foo() { + CellType cellType = CellType.BLANK; + return cellType == CellType.NUMBER; + } +} \ No newline at end of file diff --git a/testinput/glacier/ClassGetName.java b/testinput/glacier/ClassGetName.java new file mode 100644 index 0000000..ca11263 --- /dev/null +++ b/testinput/glacier/ClassGetName.java @@ -0,0 +1,6 @@ +public class ClassGetName { + public String foo() { + Number num = null; + return num.getClass().getName(); + } +} \ No newline at end of file diff --git a/testinput/glacier/ClassReturn.java b/testinput/glacier/ClassReturn.java new file mode 100644 index 0000000..25e23b4 --- /dev/null +++ b/testinput/glacier/ClassReturn.java @@ -0,0 +1,9 @@ +// typecheck: OK + + +public class ClassReturn { + public ClassReturn getInstance() { + return new ClassReturn(); + } + +} \ No newline at end of file diff --git a/testinput/glacier/ColorImpl.java b/testinput/glacier/ColorImpl.java new file mode 100644 index 0000000..2ff6a09 --- /dev/null +++ b/testinput/glacier/ColorImpl.java @@ -0,0 +1,18 @@ +// @skip-test +// Typecheck, Inference-TC: Failed +// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable. +// strange enough, seems other signatures are got from stubs. +import java.util.Arrays; +import qual.Immutable; + +public class ColorImpl { + private byte @Immutable [] _rgb; + private byte [] _mutableRgb; + + public int hashCode() { + // This should be OK, but will be an error until we have a @ReadOnly annotation. + Arrays.hashCode(_mutableRgb); + + return Arrays.hashCode(_rgb); + } +} \ No newline at end of file diff --git a/testinput/glacier/CompareTo.java b/testinput/glacier/CompareTo.java new file mode 100644 index 0000000..b1b9a1c --- /dev/null +++ b/testinput/glacier/CompareTo.java @@ -0,0 +1,11 @@ +package glacier; + +public class CompareTo { + + public void foo() { + Object val1 = null; + Object val2 = null; + // Shouldn't give an error. + ((Boolean)val1).compareTo((Boolean)val2); + } +} \ No newline at end of file diff --git a/testinput/glacier/ConflictingAnnotations.java b/testinput/glacier/ConflictingAnnotations.java new file mode 100644 index 0000000..1729ae5 --- /dev/null +++ b/testinput/glacier/ConflictingAnnotations.java @@ -0,0 +1,33 @@ +import qual.*; + +@Immutable class ImmutClass { +} + +@Mutable class MutableClass { +} + +class DefaultMutableClass { +} + +@Immutable interface ImmutInterface { +} + +interface MutableInterface { +} + +public class ConflictingAnnotations { + // ::error: (type.invalid.annotations.on.use) + @Mutable ImmutClass o1; + + // ::error: (type.invalid.annotations.on.use) + @Immutable MutableClass o2; + + // ::error: (type.invalid.annotations.on.use) + @Immutable DefaultMutableClass o3; + + // ::error: (type.invalid.annotations.on.use) + @Mutable ImmutInterface i1; + + // ::error: (type.invalid.annotations.on.use) + @Immutable MutableInterface i2; +} \ No newline at end of file diff --git a/testinput/glacier/ConstructorAssignment.java b/testinput/glacier/ConstructorAssignment.java new file mode 100644 index 0000000..4f9db96 --- /dev/null +++ b/testinput/glacier/ConstructorAssignment.java @@ -0,0 +1,24 @@ +package glacier; + +import qual.Immutable; + +public @Immutable class ConstructorAssignment { + public int x = 3; // static assignment is OK + + ConstructorAssignment() { + x = 4; // constructor assignment is OK + } + + void setX() { + // ::error: (illegal.field.write) + x = 5; + } +} + +class OtherClass { + OtherClass() { + ConstructorAssignment c = new ConstructorAssignment(); + // ::error: (illegal.field.write) + c.x = 6; + } +} \ No newline at end of file diff --git a/testinput/glacier/EnumTest.java b/testinput/glacier/EnumTest.java new file mode 100644 index 0000000..6d0b16a --- /dev/null +++ b/testinput/glacier/EnumTest.java @@ -0,0 +1,19 @@ +package glacier; + +import qual.Immutable; + +@Immutable enum Underline{ + NONE, + SINGLE, + DOUBLE, + SINGLE_ACCOUNTING, + DOUBLE_ACCOUNTING +} + +public class EnumTest { + Underline u; + + public void foo() { + u.ordinal(); + } +} \ No newline at end of file diff --git a/testinput/glacier/EqualsTest.java b/testinput/glacier/EqualsTest.java new file mode 100644 index 0000000..50c6640 --- /dev/null +++ b/testinput/glacier/EqualsTest.java @@ -0,0 +1,23 @@ +// @skip-test +package glacier; + +import qual.*; + +@Immutable public class EqualsTest { + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + return false; + } +} + +class EqualsTest2 { + @Override + // ::error: (override.param.invalid) + public boolean equals(@Immutable Object obj) { + if (this == obj) + return true; + return false; + } +} \ No newline at end of file diff --git a/testinput/glacier/FontImpl.java b/testinput/glacier/FontImpl.java new file mode 100644 index 0000000..82a8f40 --- /dev/null +++ b/testinput/glacier/FontImpl.java @@ -0,0 +1,34 @@ +// Note: PICO defaults the class decal to RDM. Removing errors on line 26 and 30. + +import qual.*; + +@Immutable interface SColor { +} + +@Immutable abstract class AbstractColorAdv implements SColor { +} + +// ::error: (type.invalid.annotations.on.use) +class FI_ColorImpl extends AbstractColorAdv { + // Arguably it would be preferable for this to not be an error. + // ::error: (type.invalid.annotations.on.use) + public static final AbstractColorAdv BLACK = new FI_ColorImpl("#000000"); + + // PICO Note: adding this error. + // ::error: (super.invocation.invalid) + FI_ColorImpl(String fontColor) { + + } +} + +public class FontImpl { + FontImpl(String fontColor) { + // Arguably it would be preferable for this to not be an error. + // Removing error. PICO chose the preferable path. + SColor a = new FI_ColorImpl(fontColor); + + // Arguably it would be preferable for this to not be an error either. + // Removing error. PICO chose the preferable path. + SColor c = fontColor != null ? new FI_ColorImpl(fontColor) : null; + } +} \ No newline at end of file diff --git a/testinput/glacier/ImmutableArray.java b/testinput/glacier/ImmutableArray.java new file mode 100644 index 0000000..631d6b2 --- /dev/null +++ b/testinput/glacier/ImmutableArray.java @@ -0,0 +1,16 @@ +import qual.Immutable; + +@SuppressWarnings("initialization") +@Immutable class ImmutableArray { + private byte @Immutable [] _rgb; + + private String @Immutable [] _strings; + + // Immutable array of mutable objects is mutable. + // PICO allows shallow immutable array. + private java.util.Date @Immutable [] _dates; + + // MaybeMutable array of primitives is mutable. + // PICO allows shallow immutable array. + private int [] _ints; +} \ No newline at end of file diff --git a/testinput/glacier/ImmutableClassMutableInterface.java b/testinput/glacier/ImmutableClassMutableInterface.java new file mode 100644 index 0000000..ab85fb1 --- /dev/null +++ b/testinput/glacier/ImmutableClassMutableInterface.java @@ -0,0 +1,14 @@ +import qual.*; + +@ReceiverDependantMutable +interface ICMI_MutableInterface {}; + +@Immutable public class ImmutableClassMutableInterface implements ICMI_MutableInterface { + public static void bar(ICMI_MutableInterface m) { }; + + public static void foo() { + ImmutableClassMutableInterface x = null; + bar(x); + } + +}; \ No newline at end of file diff --git a/testinput/glacier/ImmutableCollection.java b/testinput/glacier/ImmutableCollection.java new file mode 100644 index 0000000..11833d8 --- /dev/null +++ b/testinput/glacier/ImmutableCollection.java @@ -0,0 +1,11 @@ +// Update to PICO: add AbstractCollection to stub +import qual.Immutable; + +import java.util.*; + +@Immutable +public abstract class ImmutableCollection extends AbstractCollection { + public int getSize() { + return size(); + } +} \ No newline at end of file diff --git a/testinput/glacier/ImmutableConstructorInMutableClass.java b/testinput/glacier/ImmutableConstructorInMutableClass.java new file mode 100644 index 0000000..143e3b5 --- /dev/null +++ b/testinput/glacier/ImmutableConstructorInMutableClass.java @@ -0,0 +1,15 @@ +package glacier; + +import qual.Immutable; + + + +public class ImmutableConstructorInMutableClass { + // :: error: (type.invalid.annotations.on.use) + public @Immutable ImmutableConstructorInMutableClass() { + } + + public void aMethod() { + + } +} \ No newline at end of file diff --git a/testinput/glacier/ImmutableInterfaceClass.java b/testinput/glacier/ImmutableInterfaceClass.java new file mode 100644 index 0000000..1e888fc --- /dev/null +++ b/testinput/glacier/ImmutableInterfaceClass.java @@ -0,0 +1,11 @@ +package glacier; + +import qual.Immutable; + + +@Immutable interface ImmutableInterface { +} + +public @Immutable class ImmutableInterfaceClass implements ImmutableInterface { + +} \ No newline at end of file diff --git a/testinput/glacier/ImmutablePerson.java b/testinput/glacier/ImmutablePerson.java new file mode 100644 index 0000000..e851d4b --- /dev/null +++ b/testinput/glacier/ImmutablePerson.java @@ -0,0 +1,48 @@ +// @skip-test +// Does not apply to PICO: shallow immutable support + +package glacier; + +import qual.Immutable; + +import java.util.Date; + +/* +@Immutable class ImmutableDate { + double secondsSinceEpoch; + + void setSeconds(double s) { + secondsSinceEpoch = s; // Should error! + } +} +public @Immutable class ImmutablePerson { + public ImmutablePerson() { + birthdate = new ImmutableDate(); + + } + + ImmutableDate birthdate; + + public void test() { + + } +} +class Person { + String name; +} +*/ + + +@Immutable public class ImmutablePerson { + // Date is mutable + // :: error: glacier.mutable.invalid + Date birthdate; + + public ImmutablePerson() { + + } + + public void aMethod() { + + } +} \ No newline at end of file diff --git a/testinput/glacier/ImmutablePrimitiveContainer.java b/testinput/glacier/ImmutablePrimitiveContainer.java new file mode 100644 index 0000000..360fb43 --- /dev/null +++ b/testinput/glacier/ImmutablePrimitiveContainer.java @@ -0,0 +1,12 @@ +import qual.Immutable; + +@SuppressWarnings("initialization") +@Immutable +public class ImmutablePrimitiveContainer { + int x; + + public void setX(int x) { + // ::error: (illegal.field.write) + this.x = x; + } +} \ No newline at end of file diff --git a/testinput/glacier/IncorrectUsage.java b/testinput/glacier/IncorrectUsage.java new file mode 100644 index 0000000..d9624f4 --- /dev/null +++ b/testinput/glacier/IncorrectUsage.java @@ -0,0 +1,46 @@ +package glacier; + +import qual.*; + +@Immutable public class IncorrectUsage { + public void okMethod(IncorrectUsage this) { + + } + + public void okMethod2(@Immutable IncorrectUsage this) { + + } + + // PICO Note: adding method.receiver.incompatible + // ::error: (type.invalid.annotations.on.use) ::error: (method.receiver.incompatible) + public void badMethod(@Mutable IncorrectUsage this) { + + } + + // ::error: (type.invalid.annotations.on.use) + public void badMethod2(@Mutable IncorrectUsage obj) { + + } +} + + +class IncorrectUsage2 { + public void okMethod(IncorrectUsage2 this) { + + } + + public void okMethod2(@Mutable IncorrectUsage2 this) { + + } + + // PICO Note: adding method.receiver.incompatible + // ::error: (type.invalid.annotations.on.use) ::error: (method.receiver.incompatible) + public void badMethod(@Immutable IncorrectUsage2 this) { + + } + + // ::error: (type.invalid.annotations.on.use) + public void badMethod2(@Immutable IncorrectUsage2 obj) { + + } +} \ No newline at end of file diff --git a/testinput/glacier/IntArgument.java b/testinput/glacier/IntArgument.java new file mode 100644 index 0000000..b3156ec --- /dev/null +++ b/testinput/glacier/IntArgument.java @@ -0,0 +1,12 @@ +package glacier; + +public class IntArgument { + public void takeInt(int x) { + } + + public void useInt() { + for (int i = 0; i < 10; i++) { + takeInt(i); + } + } +} \ No newline at end of file diff --git a/testinput/glacier/IntReturn.java b/testinput/glacier/IntReturn.java new file mode 100644 index 0000000..e942f3f --- /dev/null +++ b/testinput/glacier/IntReturn.java @@ -0,0 +1,11 @@ +package glacier; + +public class IntReturn { + public int getInt() { + return 42; + } + + public void useInt() { + int x = getInt(); + } +} \ No newline at end of file diff --git a/testinput/glacier/IntegerAssignment.java b/testinput/glacier/IntegerAssignment.java new file mode 100644 index 0000000..681e93f --- /dev/null +++ b/testinput/glacier/IntegerAssignment.java @@ -0,0 +1,11 @@ +package glacier; + +public class IntegerAssignment { + public Integer getInt() { + return 42; + } + + public void useInt() { + Integer i = getInt(); + } +} \ No newline at end of file diff --git a/testinput/glacier/InterfaceField.java b/testinput/glacier/InterfaceField.java new file mode 100644 index 0000000..a9fc1a5 --- /dev/null +++ b/testinput/glacier/InterfaceField.java @@ -0,0 +1,14 @@ +// @skip-test +// Deep immutable + +import qual.Immutable; + +interface IF_AnInterface {}; + +@Immutable interface IF_ImmutableInterface extends IF_AnInterface {}; + +@Immutable public class InterfaceField { + // ::error: (glacier.mutable.invalid) + IF_AnInterface o; + IF_ImmutableInterface o2; +} \ No newline at end of file diff --git a/testinput/glacier/InterfaceSupertype.java b/testinput/glacier/InterfaceSupertype.java new file mode 100644 index 0000000..1c581d0 --- /dev/null +++ b/testinput/glacier/InterfaceSupertype.java @@ -0,0 +1,32 @@ +package glacier; + +import qual.Immutable; + +interface AnInterface { + +} + + +public class InterfaceSupertype { + + public void takeMutable(Object o) { + + } + + public void takeImmutable(Object o) { + + } + + public void doStuff() { + AnInterface obj = null; + + takeMutable(obj); + takeImmutable(obj); + } + + public boolean equals(Object o1,Object o2){ + if(o1==o2) + return true; + return o1!=null ? o1.equals(o2) : false; + } +} \ No newline at end of file diff --git a/testinput/glacier/InvalidAnnotations.java b/testinput/glacier/InvalidAnnotations.java new file mode 100644 index 0000000..40574d1 --- /dev/null +++ b/testinput/glacier/InvalidAnnotations.java @@ -0,0 +1,12 @@ +// @skip-test +// who cares bottom + +import qual.*; + +// ::error: (type.invalid) +@Bottom class InvalidBottom {}; + +public class InvalidAnnotations { + // ::error: (type.invalid) + InvalidBottom b; +} \ No newline at end of file diff --git a/testinput/glacier/InvalidAssignment.java b/testinput/glacier/InvalidAssignment.java new file mode 100644 index 0000000..26eadf7 --- /dev/null +++ b/testinput/glacier/InvalidAssignment.java @@ -0,0 +1,49 @@ +// @skip-test +// jdk stub difference + +package glacier; + +import java.util.Calendar; + +import qual.Immutable; + + +public @Immutable class InvalidAssignment { + class Inner { + public int i; + } + + String s; + // :: error: glacier.mutable.invalid + Calendar c; + // :: error: glacier.mutable.invalid + Inner i; + int x; + + public void setString(String s) { + // :: error: glacier.assignment + this.s = s; + } + + public void setX(int x) { + // :: error: glacier.assignment + this.x = x; + } + + public void setMonth(int month) { + c.set(Calendar.MONTH, month); // No error here; the problem is that d was mutable in the first place. + } + + public void setInner(int i) { + this.i.i = i; // No error here; the problem is that this.i was mutable in the first place. + } +} + +class AnotherClass { + void aMethod() { + InvalidAssignment i = new InvalidAssignment(); + + // ::error: (glacier.assignment) + i.s = "hello"; + } +} \ No newline at end of file diff --git a/testinput/glacier/InvalidImmutableInterfaceClass.java b/testinput/glacier/InvalidImmutableInterfaceClass.java new file mode 100644 index 0000000..214c990 --- /dev/null +++ b/testinput/glacier/InvalidImmutableInterfaceClass.java @@ -0,0 +1,14 @@ +import qual.Immutable; + +import java.lang.Cloneable; + +@Immutable interface IIIC_ImmutableInterface { +} + +// The use of IIIC_ImmutableInterface defaulted to @Mutable. +// So the implement action is valid for the class (implementing a mutable interface) +// But for the type use of IIIC_ImmutableInterface it is invalid. +// :: error: type.invalid.annotations.on.use +public class InvalidImmutableInterfaceClass implements Cloneable, IIIC_ImmutableInterface { + +} \ No newline at end of file diff --git a/testinput/glacier/InvalidTypeArguments.java b/testinput/glacier/InvalidTypeArguments.java new file mode 100644 index 0000000..ff89d06 --- /dev/null +++ b/testinput/glacier/InvalidTypeArguments.java @@ -0,0 +1,39 @@ +import java.util.Collection; +import java.util.Collections; +import java.util.Iterator; + +import qual.Immutable; +import qual.Mutable; + +public class InvalidTypeArguments { + interface MutableObject {} + @Immutable interface ImmutableObject {} + + class Generic {} + Generic mutableObjectGeneric; + Generic immutableObjectGeneric; + + class BogusImmutableGeneric<@Immutable T>{} + // :: error: (type.argument.type.incompatible) + BogusImmutableGeneric mutableObjectBogusImmutableGeneric; + BogusImmutableGeneric immutableObjectBogusImmutableGeneric; + + + class ImmutableGeneric<@Immutable T extends @Immutable Object>{} + // :: error: (type.argument.type.incompatible) + ImmutableGeneric mutableObjectImmutableGeneric; + ImmutableGeneric immutableObjectImmutableGeneric; + + class MutableGeneric<@Mutable T>{} + MutableGeneric mutableObjectMutableGeneric; + // :: error: (type.argument.type.incompatible) + MutableGeneric immutableObjectMutableGeneric; + + public class UnmodifiableCollection { + public Iterator getCellIterator() { + Collection cellCollection = null; + Collections.unmodifiableCollection(cellCollection); + return Collections.unmodifiableCollection(cellCollection).iterator(); + } + } +} \ No newline at end of file diff --git a/testinput/glacier/MapParameters.java b/testinput/glacier/MapParameters.java new file mode 100644 index 0000000..57272de --- /dev/null +++ b/testinput/glacier/MapParameters.java @@ -0,0 +1,13 @@ +// @skip-test +// handling of null + +import java.util.Map; + +public class MapParameters { + public static void takeMap(Map m) {}; + + public void foo() { + Map m = null; + takeMap(m); + } +} \ No newline at end of file diff --git a/testinput/glacier/MethodInvocation.java b/testinput/glacier/MethodInvocation.java new file mode 100644 index 0000000..bc92c5c --- /dev/null +++ b/testinput/glacier/MethodInvocation.java @@ -0,0 +1,14 @@ +package glacier; + +import qual.*; + +@Immutable interface Interface { + public void doStuff(); +} + +public class MethodInvocation { + public void foo() { + Interface i = null; + i.doStuff(); + } +} \ No newline at end of file diff --git a/testinput/glacier/MethodTypeParameters.java b/testinput/glacier/MethodTypeParameters.java new file mode 100644 index 0000000..d9cf90a --- /dev/null +++ b/testinput/glacier/MethodTypeParameters.java @@ -0,0 +1,7 @@ +import qual.Immutable; + +class TypeParameters { + static TypeParameters asImmutableList(@Immutable Object[] elements) { + return null; + } +} \ No newline at end of file diff --git a/testinput/glacier/MutableClassCantHaveImmutableSubclass.java b/testinput/glacier/MutableClassCantHaveImmutableSubclass.java new file mode 100644 index 0000000..3127882 --- /dev/null +++ b/testinput/glacier/MutableClassCantHaveImmutableSubclass.java @@ -0,0 +1,41 @@ +// @skip-test +// + +import qual.Immutable; + + +class Mut { + int y = 3; +} + +// ::error: (glacier.nonfinalmember) +@Immutable class Immut extends Mut { } + +class SafeAbstractSuperclass { + final int x = 3; + final String y = "Hello"; + final Immut i = null; +} + +@Immutable class Immut2 extends SafeAbstractSuperclass { }; + +class UnsafeAbstractSuperclass { + final int x= 3; + String y = "Hello"; // Oops, not final + final Immut i = null; +} + +// ::error: (glacier.nonfinalmember) +@Immutable class Immut3 extends UnsafeAbstractSuperclass { }; + + + + +class UnsafeAbstractSuperclass2 { + final int x = 3; + java.util.Date y = null; + final Immut i = null; +} + +// ::error: (glacier.nonfinalmember) ::error: (glacier.mutablemember) +@Immutable class Immut4 extends UnsafeAbstractSuperclass2 { }; \ No newline at end of file diff --git a/testinput/glacier/NestedGenerics.java b/testinput/glacier/NestedGenerics.java new file mode 100644 index 0000000..644d95d --- /dev/null +++ b/testinput/glacier/NestedGenerics.java @@ -0,0 +1,21 @@ +import java.util.Iterator; + + +interface Predicate { + boolean apply(T var1); + + boolean equals(Object var1); +} + +final class Iterators { + + public static boolean any(Iterator iterator, Predicate predicate) { + //return indexOf(iterator, predicate) != -1; + return true; + } + + public static boolean contains(Iterator iterator, Object element) { + return any(iterator, null); + } + +} \ No newline at end of file diff --git a/testinput/glacier/NullAssignment.java b/testinput/glacier/NullAssignment.java new file mode 100644 index 0000000..c799e9e --- /dev/null +++ b/testinput/glacier/NullAssignment.java @@ -0,0 +1,14 @@ +import qual.Immutable; + +interface NA_AnInterface {}; + + +public class NullAssignment { + public void takeObj(Object o) { + } + + public void foo() { + NA_AnInterface i = null; + takeObj(i); + } +} \ No newline at end of file diff --git a/testinput/glacier/Override.java b/testinput/glacier/Override.java new file mode 100644 index 0000000..6328b5a --- /dev/null +++ b/testinput/glacier/Override.java @@ -0,0 +1,18 @@ +package glacier; + +import qual.Immutable; + + +@Immutable abstract class Superclass { + public abstract void doStuff(int x); +} + +public @Immutable class Override { + + + public Override() { + } + + public void doStuff(int x) { + } +} \ No newline at end of file diff --git a/testinput/glacier/PlainObjects.java b/testinput/glacier/PlainObjects.java new file mode 100644 index 0000000..9b1b1db --- /dev/null +++ b/testinput/glacier/PlainObjects.java @@ -0,0 +1,19 @@ +// @skip-test +// PICO CAN handle null to @Bottom + +import qual.*; + +class PlainObjects { + + public void takeObject(Object o) {}; + public void takeImmutableObject(@Immutable Object o) {}; + + void foo () { + Object o1 = null; + @Immutable Object o2 = null; + + takeObject(o2); + + takeImmutableObject(o1); + } +} \ No newline at end of file diff --git a/testinput/glacier/ReadOnlyClass.java b/testinput/glacier/ReadOnlyClass.java new file mode 100644 index 0000000..8738c71 --- /dev/null +++ b/testinput/glacier/ReadOnlyClass.java @@ -0,0 +1,27 @@ +// @skip-test + +import qual.*; +import java.lang.String; + +// Classes can't be annotated ReadOnly in their declarations; @Readonly is only for method parameters. +// ::error: (glacier.readonly.class) +@Readonly public class ReadOnlyClass { +} + +class ReadOnlyMethodClass { + @Readonly ReadOnlyClass roc; + + int @Readonly [] readOnlyIntArray; + + // ::error: (type.invalid.annotations.on.use) + void takeReadOnlyString(@Readonly String foo) {} + void takeReadOnlyArray(String @Readonly [] foo) { + // ::error: (glacier.assignment.array) + foo[0] = "Hello, world!"; + } + + void takeImmutableArray(String @Immutable [] foo) { + // ::error: (glacier.assignment.array) + foo[0] = "Hello, world!"; + } +} \ No newline at end of file diff --git a/testinput/glacier/ReadOnlyObject.java b/testinput/glacier/ReadOnlyObject.java new file mode 100644 index 0000000..bc4c6f3 --- /dev/null +++ b/testinput/glacier/ReadOnlyObject.java @@ -0,0 +1,13 @@ +// Reason of Change: defaulting difference. + +import qual.*; + +public class ReadOnlyObject { + // PICO defaults the return type of RDM class to mutable. + // But String.valueOf(1) returns immutable. + public @Immutable Object foo() { + Object cat = null; + return true ? String.valueOf(1) : cat; + } + +} \ No newline at end of file diff --git a/testinput/glacier/ResultWrapTest.java b/testinput/glacier/ResultWrapTest.java new file mode 100644 index 0000000..08809e7 --- /dev/null +++ b/testinput/glacier/ResultWrapTest.java @@ -0,0 +1,16 @@ +// @skip-test +// Guess: in glacter @MaybeMutable is super type of @Immutable. So the use of typevar is allowed. + +import qual.Mutable; + +public class ResultWrapTest { + + ResultWrapTest() { + // while visiting this, the return type must be annotated correctly? + } + + static class ResultWrap { + } + + final ResultWrap input = null; +} \ No newline at end of file diff --git a/testinput/glacier/StaticAssignment.java b/testinput/glacier/StaticAssignment.java new file mode 100644 index 0000000..a7bbb8c --- /dev/null +++ b/testinput/glacier/StaticAssignment.java @@ -0,0 +1,22 @@ +// @skip-test +// !!!!!!!!!!!!!!! +// GLOBAL is writable in static. +// removing static will raise error. + +import qual.Immutable; + +@Immutable +public class StaticAssignment { + public static int GLOBAL = 1; // OK, no error here + + StaticAssignment() { + // ::error: (glacier.assignment) + GLOBAL = 2; + } + + public void setStatics () { + // ::error: (glacier.assignment) + GLOBAL = 42; + } + +} \ No newline at end of file diff --git a/testinput/glacier/StringTest.java b/testinput/glacier/StringTest.java new file mode 100644 index 0000000..6f478f3 --- /dev/null +++ b/testinput/glacier/StringTest.java @@ -0,0 +1,10 @@ +package glacier; + +import qual.Immutable; + +import java.lang.String; + +@SuppressWarnings("initialization") +public @Immutable class StringTest { + String s; // no error expected here because String should be treated as if it were declared @Immutable. +} \ No newline at end of file diff --git a/testinput/glacier/Subclassing.java b/testinput/glacier/Subclassing.java new file mode 100644 index 0000000..766b020 --- /dev/null +++ b/testinput/glacier/Subclassing.java @@ -0,0 +1,18 @@ +// @skip-test +// Drop this one: PICO cannot derive from mutable classes + +import qual.Immutable; + +public class Subclassing { }; + +class MutSubclass extends Subclassing { }; + +// OK with the recent change: immutable classes can derive from mutable classes +@Immutable class InvalidImmutSubclass extends Subclassing { }; + + +@Immutable class ImmutableSuper { }; +@Immutable class ImmutableSub extends ImmutableSuper { }; + +// ::error: (glacier.subclass.mutable) +class InvalidMutableSub extends ImmutableSuper { }; \ No newline at end of file diff --git a/testinput/glacier/Transitivity.java b/testinput/glacier/Transitivity.java new file mode 100644 index 0000000..66f2138 --- /dev/null +++ b/testinput/glacier/Transitivity.java @@ -0,0 +1,20 @@ +package glacier; + +import qual.Immutable; + +@SuppressWarnings("initialization") +@Immutable class Inner { + int x; +} + +@SuppressWarnings("initialization") +public @Immutable class Transitivity { + Inner i; + + public Transitivity() { + } + + public void test() { + + } +} \ No newline at end of file diff --git a/testinput/glacier/TransitivityError.java b/testinput/glacier/TransitivityError.java new file mode 100644 index 0000000..75876f2 --- /dev/null +++ b/testinput/glacier/TransitivityError.java @@ -0,0 +1,23 @@ +// @skip-test +// until the defaulting of fields in immutable class is resolved + +package glacier; + +import qual.Immutable; + + +class TE_Inner { + int x; +} + +public @Immutable class TransitivityError { + // :: error: glacier.mutable.invalid + TE_Inner i; + + public TransitivityError() { + } + + public void test() { + + } +} \ No newline at end of file diff --git a/testinput/glacier/TypeParameter.java b/testinput/glacier/TypeParameter.java new file mode 100644 index 0000000..a78fdab --- /dev/null +++ b/testinput/glacier/TypeParameter.java @@ -0,0 +1,32 @@ +// @skip-test +// review glacier's type parameter rule when free + +import qual.Immutable; + +class E { } // Note same name as type parameter, but mutable class. + +@Immutable class TP_Superclass { + private E aField; // Should be OK because we'll make sure E is instantiated with an immutable type. This E is the type parameter, not the class above. + void aMethod() { + + } +} + +@Immutable public class TypeParameter extends TP_Superclass { + private TP_Superclass s; + private TP_Superclass t; + + // ::error: (glacier.typeparameter.mutable) + private TP_Superclass u; + + void aMethod() { + + } +} + +@Immutable class Test { + TypeParameter t1 = null; // OK + + // ::error: (glacier.typeparameter.mutable) + TypeParameter t2 = null; +} \ No newline at end of file diff --git a/testinput/glacier/Unboxing.java b/testinput/glacier/Unboxing.java new file mode 100644 index 0000000..c614fbd --- /dev/null +++ b/testinput/glacier/Unboxing.java @@ -0,0 +1,8 @@ +public class Unboxing { + public void takeNumber(Number n) {}; + + public void passDouble() { + takeNumber(42.0); + } + +}; \ No newline at end of file diff --git a/testinput/glacier/UnmodifiableCollection.java b/testinput/glacier/UnmodifiableCollection.java new file mode 100644 index 0000000..02138b7 --- /dev/null +++ b/testinput/glacier/UnmodifiableCollection.java @@ -0,0 +1,14 @@ +import java.util.Collection; +import java.util.Collections; +import java.util.Iterator; +import java.util.List; + + +interface SCell {}; + +public class UnmodifiableCollection { + public Iterator getCellIterator() { + Collection cellCollection = null; + return Collections.unmodifiableCollection(cellCollection).iterator(); + } +} \ No newline at end of file diff --git a/testinput/glacier/UnmodifiableList.java b/testinput/glacier/UnmodifiableList.java new file mode 100644 index 0000000..578ef86 --- /dev/null +++ b/testinput/glacier/UnmodifiableList.java @@ -0,0 +1,24 @@ +package glacier; + +import java.util.List; + + +class ListProcessor { + static List process(List c) { + // ::warning: [unchecked] unchecked cast + return (List)c; + } +} + +class AClass {} + +public class UnmodifiableList { + private List _list; + + public void foo() { + + //List a = true ? _list : null; + List l = true ? ListProcessor.process(_list) : _list; + //List l = ListProcessor.process(_list); + } +} \ No newline at end of file diff --git a/testinput/glacier/ValidImmutableInterfaceClass.java b/testinput/glacier/ValidImmutableInterfaceClass.java new file mode 100644 index 0000000..784f443 --- /dev/null +++ b/testinput/glacier/ValidImmutableInterfaceClass.java @@ -0,0 +1,11 @@ +package glacier; + +import qual.Immutable; + + +@Immutable interface VIIC_ImmutableInterface { +} + +public @Immutable class ValidImmutableInterfaceClass implements VIIC_ImmutableInterface { + +} \ No newline at end of file diff --git a/testinput/inference/inferrable/BoundsCompatible.java b/testinput/inference/inferrable/BoundsCompatible.java index 6e8daa7..5303c3f 100644 --- a/testinput/inference/inferrable/BoundsCompatible.java +++ b/testinput/inference/inferrable/BoundsCompatible.java @@ -13,5 +13,6 @@ class Level1B extends BoundsCompatible {} @Mutable class Level2A extends Level1A {} -// :: fixable-error: (subclass.bound.incompatible) +// fixable-error subclass.bound.incompatible removed. +// :: fixable-error: (type.invalid.annotations.on.use) :: fixable-error: (super.invocation.invalid) @Immutable class Level2B extends Level1B {} diff --git a/testinput/inference/inferrable/ConstructorInvocationUsingNew.java b/testinput/inference/inferrable/ConstructorInvocationUsingNew.java index 021623e..1b2dee8 100644 --- a/testinput/inference/inferrable/ConstructorInvocationUsingNew.java +++ b/testinput/inference/inferrable/ConstructorInvocationUsingNew.java @@ -9,7 +9,7 @@ public class ConstructorInvocationUsingNew { public static void main(String[] args) { // Handled by PICOInferenceVisito#checkConstructorInvocability - // :: fixable-error: (type.invalid.annotations.on.use) + // :: fixable-error: (type.invalid.annotations.on.use) :: fixable-error: (assignment.type.incompatible) @Immutable ConstructorInvocationUsingNew c = new ConstructorInvocationUsingNew(); } } diff --git a/testinput/inference/inferrable/FixableTypeCast.java b/testinput/inference/inferrable/FixableTypeCast.java index db92554..5845a93 100644 --- a/testinput/inference/inferrable/FixableTypeCast.java +++ b/testinput/inference/inferrable/FixableTypeCast.java @@ -1,6 +1,5 @@ public class FixableTypeCast { void foo(Object o) { - // :: fixable-warning: (cast.unsafe) String s = (String) o; } } diff --git a/testinput/inference/inferrable/RawIterator.java b/testinput/inference/inferrable/RawIterator.java index 1bccc5a..2c349e7 100644 --- a/testinput/inference/inferrable/RawIterator.java +++ b/testinput/inference/inferrable/RawIterator.java @@ -24,7 +24,9 @@ public void build(Collection classes) { // programs that have the below line wouldn't be inferred. One legal use case we discussed // is to cast @Mutable datastructure to @Immutable if we guarantee that @Mutable reference // doesn't leak. So we should continue if incompatible cast happens(@Mutable to @Immutable). - // :: warning: (cast.unsafe) + + // Lian: What is a incompatible cast? It seems good to cast to Immutable if casting to String + // is already vaild. String s = (String)iterator.next(); // But for cast that involves at least one VariableSlot, PICOInfer tends to give solutions diff --git a/testinput/inference/inferrable/StrangeReadonly.java b/testinput/inference/inferrable/StrangeReadonly.java index ef96584..3ff2a46 100644 --- a/testinput/inference/inferrable/StrangeReadonly.java +++ b/testinput/inference/inferrable/StrangeReadonly.java @@ -1,5 +1,6 @@ import java.util.Arrays; import java.util.Comparator; +import qual.*; public class StrangeReadonly { @SuppressWarnings("unchecked") @@ -18,12 +19,12 @@ static void foo() { // And CF right now ignores subtype relationship check(constraint generation on inference // side) and always returns true, i.e. "? extends Object" <: VarAnnot(o1), so typeof(o1) :> @Readonly // wasn't generated and o1 is inferred to @Immutable(select any valid solution). - public int compare(Object o1, Object o2) { + + // Lian: CF now could correctly default the mutable on uses. @Readonly added on parameters. + public int compare(@Readonly Object o1, @Readonly Object o2) { // Before inference, @Mutable is casted to @Immutable; After inference, @Readonly is // casted to @Immutable. - // :: fixable-warning: (cast.unsafe) int i = (Integer) o1; - // :: fixable-warning: (cast.unsafe) int j = (Integer) o2; return 0; } diff --git a/testinput/inference/inferrable/issue144/ComplicatedTest.java b/testinput/inference/inferrable/issue144/ComplicatedTest.java index d3aa0ec..c6a8122 100644 --- a/testinput/inference/inferrable/issue144/ComplicatedTest.java +++ b/testinput/inference/inferrable/issue144/ComplicatedTest.java @@ -38,7 +38,7 @@ void testImmutability() { String name = "tamier"; int age = 24; ArrayList friends = new ArrayList(); - // :: fixable-error: (type.invalid.annotations.on.use) + // :: fixable-error: (constructor.invocation.invalid) Person p = new @Immutable Person(name, age, friends); // :: fixable-error: (method.invocation.invalid) p.getName(); diff --git a/testinput/inference/inferrable/issue144/ConstructorInvocationInSubclassConstructor.java b/testinput/inference/inferrable/issue144/ConstructorInvocationInSubclassConstructor.java index f469dd1..958aaa0 100644 --- a/testinput/inference/inferrable/issue144/ConstructorInvocationInSubclassConstructor.java +++ b/testinput/inference/inferrable/issue144/ConstructorInvocationInSubclassConstructor.java @@ -15,7 +15,7 @@ public class ConstructorInvocationInSubclassConstructor { class SubClass extends ConstructorInvocationInSubclassConstructor { SubClass(Object p) { // Handled by PICOInferenceVisito##checkMethodInvocability - // :: fixable-error: (super.constructor.invocation.incompatible) + // :: fixable-error: (super.invocation.invalid) super(p); } } diff --git a/testinput/inference/inferrable/issue144/RDMConstructor.java b/testinput/inference/inferrable/issue144/RDMConstructor.java index f7bbb2d..c79dec6 100644 --- a/testinput/inference/inferrable/issue144/RDMConstructor.java +++ b/testinput/inference/inferrable/issue144/RDMConstructor.java @@ -16,7 +16,7 @@ class A { public class RDMConstructor { void test1() { - // :: fixable-error: (type.invalid.annotations.on.use) + // :: fixable-error: (type.invalid.annotations.on.use) :: fixable-error: (assignment.type.incompatible) @Immutable A la = new A(); la.toString(); } diff --git a/testinput/reiminfer/CFLTests1.java b/testinput/reiminfer/CFLTests1.java new file mode 100644 index 0000000..c4ce5a2 --- /dev/null +++ b/testinput/reiminfer/CFLTests1.java @@ -0,0 +1,50 @@ + + +class MyA { + String f; +} + +class List{ + Object[] elems; + int count; + List() { + Object[] t = new Object[10]; + this.elems = t; + } + void add(Object m) { + Object[] t = this.elems; + t[count++] = m; + } + Object get(int ind) { + Object[] t = this.elems; + Object p = t[ind]; + return p; + } +} + +class ListClient { + List list; + ListClient(List l) { + this.list = l; + } + Object retrieve() { + List t = this.list; + Object r = t.get(0); + return r; + } +} + +public class CFLTests1 { + public static void main(String[] arg) { + List l1 = new List(); + MyA t = new MyA(); + l1.add(t); + ListClient client = new ListClient(l1); + List l2 = new List(); + MyA i = new MyA(); i.f = "abc"; + l2.add(i); + MyA s = (MyA) client.retrieve(); + MyA j = (MyA) l2.get(0); + String str = s.f; + } +} diff --git a/testinput/reiminfer/CFLTests2.java b/testinput/reiminfer/CFLTests2.java new file mode 100644 index 0000000..4d20033 --- /dev/null +++ b/testinput/reiminfer/CFLTests2.java @@ -0,0 +1,18 @@ +class MyB { + String f; +} + +public class CFLTests2 { + + public static MyB id(MyB p) { + return p; + } + + public static void main(String[] arg) { + MyB b1 = new MyB(); //o1 + MyB b2 = new MyB(); //o2 + + MyB b3 = id(b1); + MyB b4 = id(b2); + } +} diff --git a/testinput/reiminfer/CFLTests3.java b/testinput/reiminfer/CFLTests3.java new file mode 100644 index 0000000..ab1a101 --- /dev/null +++ b/testinput/reiminfer/CFLTests3.java @@ -0,0 +1,25 @@ +class Data { + String d; + public void set(String p) { + this.d = p; + } + + public String get() { + return this.d; + } +} + + +public class CFLTests3 { + public static void main() { + Data data = new Data(); + String s1 = new String("Ana"); + data.set(s1); + String s2 = data.get(); + + Data data2 = new Data(); + String s3 = new String("Antun"); + data2.set(s3); + String s4 = data2.get(); + } +} diff --git a/testinput/reiminfer/CFLTests4.java b/testinput/reiminfer/CFLTests4.java new file mode 100644 index 0000000..7a07a16 --- /dev/null +++ b/testinput/reiminfer/CFLTests4.java @@ -0,0 +1,39 @@ + +public class CFLTests4 { + String[] arr1 = new String[10]; + String[] arr2 = new String[10]; + /* + public CFLTests4() { + arr1 = new String[10]; + arr2 = new String[10]; + } + */ + + public void putInArr1(String s) { + arr1[0] = s; + } + + public void putInArr2(String s) { + arr2[0] = s; + } + + public String getFromArr1() { + return arr1[0]; + } + + public String getFromArr2() { + return arr2[0]; + } + + public static void main(String[] arg) { + CFLTests4 c = new CFLTests4(); + String s1 = new String("Ana"); + String s2 = new String("Antun"); + c.putInArr1(s1); + c.putInArr2(s2); + + String s3 = c.getFromArr1(); + String s4 = c.getFromArr2(); + System.out.println(s3+" "+s4); + } +} diff --git a/testinput/reiminfer/CFLTests5.java b/testinput/reiminfer/CFLTests5.java new file mode 100644 index 0000000..b74f7f1 --- /dev/null +++ b/testinput/reiminfer/CFLTests5.java @@ -0,0 +1,45 @@ + +public class CFLTests5 { + + public void putInArr(String s, String[] arr1) { + arr1[0] = s; + } + /* + public void putInArr2(String s, String[] arr2) { + arr2[0] = s; + } + */ + + public String getFromArr(String[] arr1) { + return arr1[0]; + } + /* + public String getFromArr2(String[] arr2) { + return arr2[0]; + } + */ + + public static void main(String[] arg) { + CFLTests5 c = new CFLTests5(); + String[] arr1 = new String[10]; + String[] arr2 = new String[10]; + + String s1 = new String("Ana"); + String s2 = new String("Antun"); + + c.putInArr(s1,arr1); + c.putInArr(s2,arr2); + + String s3 = c.getFromArr(arr1); + String s4 = c.getFromArr(arr2); + System.out.println(s3+" "+s4); + + String[] arr3 = new String[10]; + String s7 = new String("Pooch"); + arr3[0] = s7; + String s5 = arr3[0]; + String s6 = s5; + + } +} + \ No newline at end of file diff --git a/testinput/reiminfer/CFLTests6.java b/testinput/reiminfer/CFLTests6.java new file mode 100644 index 0000000..5f4c65c --- /dev/null +++ b/testinput/reiminfer/CFLTests6.java @@ -0,0 +1,30 @@ +interface I { + public void set(String p); + public String get(); +} + +class IData implements I { + String d; + public void set(String p) { + this.d = p; + } + + public String get() { + return this.d; + } +} + + +public class CFLTests6 { + public static void main() { + I data = new IData(); + String s1 = new String("Ana"); + data.set(s1); + String s2 = data.get(); + + I data2 = new IData(); + String s3 = new String("Antun"); + data2.set(s3); + String s4 = data2.get(); + } +} diff --git a/testinput/reiminfer/CFLTests7.java b/testinput/reiminfer/CFLTests7.java new file mode 100644 index 0000000..4983976 --- /dev/null +++ b/testinput/reiminfer/CFLTests7.java @@ -0,0 +1,30 @@ +class DD { + String f; +} + + +public class CFLTests7 { + + public static DD dd = new DD(); + + public static String theString; + + public static void main(String[] arg) { + String s1 = new String("Ana"); + String s2 = new String("Antun"); + + theString = s1; + dd.f = s2; + + m(); + n(); + } + + public static void m() { + String s3 = theString; + } + + public static void n() { + String s4 = dd.f; + } +} diff --git a/testinput/reiminfer/CFLTests8.java b/testinput/reiminfer/CFLTests8.java new file mode 100644 index 0000000..110a0f3 --- /dev/null +++ b/testinput/reiminfer/CFLTests8.java @@ -0,0 +1,42 @@ +import java.util.ArrayList; +import java.util.HashMap; + +class MyCrap { + int i; +} + + +public class CFLTests8 { + + static HashMap hashMap = new HashMap(); + + HashMap map = new HashMap(); + ArrayList l = new ArrayList(); + + public void m() { + MyCrap m1 = new MyCrap(); + MyCrap m2 = new MyCrap(); + hashMap.put("Ana",m1); + + map.put("Sweety",m2); + } + + public void n() { + MyCrap m3 = hashMap.get("Ana"); + MyCrap m4 = map.get("Sweety"); + l.add(m4); + } + + public void o() { + MyCrap m5 = l.get(0); + } + + public static void main(String[] args) { + CFLTests8 cfl = new CFLTests8(); + cfl.m(); + cfl.n(); + cfl.o(); + } + + +} diff --git a/testinput/reiminfer/CircularInitialization.java b/testinput/reiminfer/CircularInitialization.java new file mode 100644 index 0000000..cadcce6 --- /dev/null +++ b/testinput/reiminfer/CircularInitialization.java @@ -0,0 +1,35 @@ +class Person { + String name; + Person partner; + + public Person(String name) { + this.name = name; + } + + public void m(Person p) { + this.partner = p; + } +} + +class Couple { + Person husband; + Person wife; + public Couple(Person husband, Person wife) { + this.husband = husband; + this.wife = wife; + } + public void print() { + System.out.println(husband.name+" and "+wife.name); + } +} + +public class CircularInitialization { + public static void main(String[] args) { + Person bob = new Person("Bob"); + Person sally = new Person("Sally"); + bob.m(sally); + sally.m(bob); + Couple c = new Couple(bob,sally); + c.print(); + } +} diff --git a/testinput/reiminfer/ImmutableArrays.java b/testinput/reiminfer/ImmutableArrays.java new file mode 100644 index 0000000..c116d20 --- /dev/null +++ b/testinput/reiminfer/ImmutableArrays.java @@ -0,0 +1,38 @@ +public class ImmutableArrays { + char[] a; + + ImmutableArrays() { + a = new char[10]; + for (int i=0; i<10; i++) { + a[i] = 'a'; + } + //b[0] = 'b'; + } + + void m(StringBuffer b) { + System.out.println(b.toString()); + a[0] = 'a'; + System.out.println(b.toString()); + b.append("ana"); + } + void n() { + char[] b = a; + b[1] = 'b'; + } + + + public static void main(String[] args) { + char[] bb = new char[100]; + bb[5] = 'a'; + ImmutableArrays i = new ImmutableArrays(); + i.m(new StringBuffer("Boza")); + i.n(); + if (i.a[1] == 'b') + System.out.println("AHA"); + else + System.out.println("A-NO"); + // i.a[2] = 'c'; + StringBuffer b = new StringBuffer("Ana"); + System.out.println(i.a[1]+i.a[0]); + } +} diff --git a/testinput/reiminfer/InitMethod.java b/testinput/reiminfer/InitMethod.java new file mode 100644 index 0000000..36c4a48 --- /dev/null +++ b/testinput/reiminfer/InitMethod.java @@ -0,0 +1,30 @@ +class A { + char[] arr; + public A() { + arr = new char[10]; + arr[0] = 'a'; + init("Ana"); + } + + void init(String arg) { + System.out.println(arg); + for (int i=0; i<10; i++) { + System.out.println(arr[i]); + //arr[i] = 'b'; + } + //m(arr); + } + + void m(char[] b) { + b[0]='a'; + } + +} + +public class InitMethod { + public static void main(String[] arg) { + A a = new A(); + a.init("Ana"); + //a.m(a.arr); + } +} diff --git a/testinput/reiminfer/Library.java b/testinput/reiminfer/Library.java new file mode 100644 index 0000000..e6bf73d --- /dev/null +++ b/testinput/reiminfer/Library.java @@ -0,0 +1,16 @@ +import java.util.*; + +public class Library { + + public void foo() { + Set set = new HashSet(); + X a1 = new X(); + set.add(a1); + Set set2 = set; + int size = set2.size(); + } +} + +class X { + String f; +} diff --git a/testinput/reiminfer/LibraryUse.java b/testinput/reiminfer/LibraryUse.java new file mode 100644 index 0000000..13ac96a --- /dev/null +++ b/testinput/reiminfer/LibraryUse.java @@ -0,0 +1,12 @@ +import java.util.*; + +public class LibraryUse { + public static void main(String[] arg) { + ArrayList al = new ArrayList(); + al.add("Boza"); + al.add("Katarina"); + ArrayList al1 = al; + int i = al1.size(); + System.out.println(i); + } +} diff --git a/testinput/reiminfer/Test1.java b/testinput/reiminfer/Test1.java new file mode 100644 index 0000000..8a2b224 --- /dev/null +++ b/testinput/reiminfer/Test1.java @@ -0,0 +1,44 @@ + +class B { + protected StringBuffer name; + + public B(StringBuffer s) { + name = s; + } +} + +class C extends B { + + public C() { + super(new StringBuffer("Ana")); + } + + public void set() { + name.append("Boza"); + } + public String get() { + return name.toString(); + } +} + +class D { + C c = new C(); + public void m() { + c.set(); + } + + public String n() { + return c.get(); + } +} + +public class Test1 { + + public static void main(String[] arg) { + D d = new D(); + d.m(); + d.n(); + + } + +} diff --git a/testinput/reiminfer/Test2.java b/testinput/reiminfer/Test2.java new file mode 100644 index 0000000..393aa07 --- /dev/null +++ b/testinput/reiminfer/Test2.java @@ -0,0 +1,21 @@ + +public class Test2 { + + public static char[] copy(char[] a) { + char[] r = new char[a.length]; + for (int i=0; i < a.length; i++) { + r[i] = a[i]; + } + return r; + } + + public static void main(String[] argc) { + char[] a = new char[5]; + for (int i=0; i<5; i++) + a[i] = 'a'; + char[] r = copy(a); + // System.out.println(r); + //r[0] = 'a'; + } + +} diff --git a/testinput/reiminfer/Test3.java b/testinput/reiminfer/Test3.java new file mode 100644 index 0000000..4ec7b0a --- /dev/null +++ b/testinput/reiminfer/Test3.java @@ -0,0 +1,40 @@ +class F { + char[] arr; +} + +class E { + + char[] arr; + void m() { + arr = new char[5]; + for (int i=0; i<5; i++) { + arr[i] = 10; + } + } + char[] n() { + return arr; + } + void o(F p) { + p.arr = arr; + } +} + + +public class Test3 { + public static E create() { + E e = new E(); + e.m(); + return e; + } + public static void main(String[] argc) { + E d = create(); + // E d = new E(); + // d.m(); + // char[] b = d.n(); + F f = new F(); + d.o(f); + char[] b = f.arr; + b[0] = 'a'; + System.out.println(b[0]); + } +} diff --git a/testinput/reiminfer/Test4.java b/testinput/reiminfer/Test4.java new file mode 100644 index 0000000..d708cbb --- /dev/null +++ b/testinput/reiminfer/Test4.java @@ -0,0 +1,50 @@ +class BB { + int i; +} + +class AA { + char[] arr; + BB f; + AA() { + arr = new char[2]; + f = new BB(); + } + + BB get() { return f; } + + char[] getArray() { return arr; } + + static AA createInstance() { + return new AA(); + } + + + } + + +public class Test4 { + + BB f; + + BB m() { + AA a = AA.createInstance(); + BB bb = a.get(); + f = bb; + return bb; + } + + void n() { + f.i = 0; + } + + static Test4 create() { + return new Test4(); + } + + public static void main(String[] arg) { + Test4 t = create(); + BB bb = t.m(); + t.n(); + // bb.i = 0; + } +} diff --git a/testinput/reiminfer/TheClass.java b/testinput/reiminfer/TheClass.java new file mode 100644 index 0000000..8863c93 --- /dev/null +++ b/testinput/reiminfer/TheClass.java @@ -0,0 +1,72 @@ +import qual.*; + +public class TheClass { + public @PolyMutable String f; + public static String sf; + public Object of = null; + public static int sof = 1; + +// public TheClass() { +// f = "hello"; +// } + +// public TheClass(String p1) { +// this.f = p1; +// } + + public String doSomethingElse( + @PolyMutable TheClass this, + String p1, + Object p2, + int p4) { + String s1 = p1; + String s2 = s1; + String s3 = s2 + " world"; + return s3; + } + + public String doSomething(@Readonly TheClass this){ + String s = doSomethingElse(f, null, 1); + return s; + } + +// public String doMore() { +// String d1 = "hello"; +// TheClass c = new TheClass(); +// f = d1; +// c.f = d1; +// TheClass c2 = new TheClass(); +// c = c2; +// return c.f; +// } + +// public String toString() { +// return f; +// } + +// public boolean equals(Object o) { +// return true; +// } +} + +class AnotherClass extends TheClass { + + +// @Override +// public void doSomething(){ +// String[] localA2 = testArrays2(); +// String[] localA3 = localA2; +// } + + +// String[] fieldA; +// +// public void testArrays() { +// String[] localA = this.fieldA; +// } + +// public String[] testArrays2() { +// return fieldA; +// } + +} diff --git a/testinput/reiminfer/ThisLeak.java b/testinput/reiminfer/ThisLeak.java new file mode 100644 index 0000000..38fdebd --- /dev/null +++ b/testinput/reiminfer/ThisLeak.java @@ -0,0 +1,26 @@ +class AAA { + ThisLeak f; +} + +public class ThisLeak { + private ThisLeak f; + + public void m() { + this.f = this; + System.out.println("Tests leak into field of this"); + } + + public void n(AAA a) { + a.f = this; + System.out.println("Tests leak into field of parameter"); + } + + public static void main(String[] arg) { + ThisLeak tl = new ThisLeak(); + AAA aaa = new AAA(); + tl.m(); + tl.n(aaa); + + } + +} diff --git a/testinput/reiminfer/ThisLeak2.java b/testinput/reiminfer/ThisLeak2.java new file mode 100644 index 0000000..f33defb --- /dev/null +++ b/testinput/reiminfer/ThisLeak2.java @@ -0,0 +1,20 @@ +class Helper { + ThisLeak2 f; +} + +public class ThisLeak2 { + public void m(Helper h) { + n(h); + } + public void n(Helper h) { + ThisLeak2[] arr = new ThisLeak2[1]; + arr[0] = this; + // h.f = this; + } + + public static void main(String[] arg) { + ThisLeak2 tl2 = new ThisLeak2(); + Helper h = new Helper(); + tl2.m(h); + } +} diff --git a/testinput/reiminfer/ThisLeak3.java b/testinput/reiminfer/ThisLeak3.java new file mode 100644 index 0000000..4312529 --- /dev/null +++ b/testinput/reiminfer/ThisLeak3.java @@ -0,0 +1,18 @@ +class ZZZ { + ThisLeak3 f; +} +public class ThisLeak3 { + void m(ZZZ z, ThisLeak3 p) { + z.f = p; + } + + void n(ZZZ z) { + m(z,this); + } + + public static void main(String[] arg) { + ThisLeak3 tl3 = new ThisLeak3(); + ZZZ z = new ZZZ(); + tl3.n(z); + } +} diff --git a/testinput/reiminfer/ThisLeak4.java b/testinput/reiminfer/ThisLeak4.java new file mode 100644 index 0000000..8149c5e --- /dev/null +++ b/testinput/reiminfer/ThisLeak4.java @@ -0,0 +1,24 @@ +public class ThisLeak4 { + + public void n() { + System.out.println("This is n"); + } + + public void o() { + innerClass ic = new innerClass(); + ic.m(); + } + + public static void main(String[] arg) { + ThisLeak4 tl4 = new ThisLeak4(); + tl4.o(); + } + + public class innerClass { + int f; + public void m() { + System.out.println("Boza"); + n(); + } + } +} diff --git a/testinput/reiminfer/ThisLeak5.java b/testinput/reiminfer/ThisLeak5.java new file mode 100644 index 0000000..bc01b4d --- /dev/null +++ b/testinput/reiminfer/ThisLeak5.java @@ -0,0 +1,21 @@ +class Boza { + ThisLeak5 f; + int y; +} +public class ThisLeak5 { + int x; + Boza b; + + public ThisLeak5() { + ThisLeak5 p = this; + + p.b = new Boza(); + p.x = 0; + + int y = p.x; + Boza bb = p.b; + this.b = bb; + this.x = y; + } + +} diff --git a/testinput/reiminfer/ThisLeak6.java b/testinput/reiminfer/ThisLeak6.java new file mode 100644 index 0000000..588e8fe --- /dev/null +++ b/testinput/reiminfer/ThisLeak6.java @@ -0,0 +1,22 @@ +class YYY { + ThisLeak6 f; +} + +public class ThisLeak6 { + int x; + + public ThisLeak6 id() { + return this; + } + + public void m() { + System.out.println("fjdfkjd"); + ThisLeak6 tl6 = id(); + tl6.x = 0; + } + + public void n(YYY y) { + y.f = id(); + } + +} diff --git a/testinput/typecheck/AssignableExample.java b/testinput/typecheck/AssignableExample.java index a7d15d8..40fa3e7 100644 --- a/testinput/typecheck/AssignableExample.java +++ b/testinput/typecheck/AssignableExample.java @@ -28,7 +28,7 @@ void foo2(@Mutable AssignableExample this) { } } -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) @ReceiverDependantMutable class Subclass extends AssignableExample { void bar(@Immutable Subclass this) { // :: error: (illegal.field.write) diff --git a/testinput/typecheck/CompatabilityBEI1.java b/testinput/typecheck/CompatabilityBEI1.java index d9f0963..699310a 100644 --- a/testinput/typecheck/CompatabilityBEI1.java +++ b/testinput/typecheck/CompatabilityBEI1.java @@ -32,18 +32,16 @@ class H extends Object {} @Mutable class I implements @Mutable Cloneable {} -// :: error: (bound.implements.incompatabile) +// :: error: (declaration.inconsistent.with.implements.clause) @Mutable class J implements @Immutable Cloneable {} -// :: error: (bound.implements.incompatabile) @Mutable class K implements @ReceiverDependantMutable Cloneable {} -// :: error: (bound.extends.incompatabile) +// :: error: (declaration.inconsistent.with.extends.clause) @Immutable class L extends @Mutable Object {} @Immutable class M extends @Immutable Object {} -// :: error: (bound.extends.incompatabile) @Immutable class N extends @ReceiverDependantMutable Object {} abstract class O implements CharSequence {} diff --git a/testinput/typecheck/CompatabilityBEI2.java b/testinput/typecheck/CompatibilityBEI2.java similarity index 84% rename from testinput/typecheck/CompatabilityBEI2.java rename to testinput/typecheck/CompatibilityBEI2.java index 065c652..5b06687 100644 --- a/testinput/typecheck/CompatabilityBEI2.java +++ b/testinput/typecheck/CompatibilityBEI2.java @@ -25,28 +25,26 @@ class H extends ArrayList<@Immutable Object> {} @Mutable abstract class I implements @Mutable List<@Immutable Object> {} -// :: error: (bound.implements.incompatabile) +// :: error: (declaration.inconsistent.with.implements.clause) @Mutable abstract class J implements @Immutable List<@Immutable Object> {} -// :: error: (bound.implements.incompatabile) @Mutable abstract class K implements @ReceiverDependantMutable List<@Immutable Object> {} -// :: error: (bound.extends.incompatabile) +// :: error: (declaration.inconsistent.with.extends.clause) @Immutable class L extends @Mutable ArrayList<@Immutable Object> {} @Immutable class M extends @Immutable ArrayList<@Immutable Object> {} -// :: error: (bound.extends.incompatabile) @Immutable class N extends @ReceiverDependantMutable ArrayList<@Immutable Object> {} abstract class O implements CharSequence {} @Immutable interface ImmutableInterface {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) @Mutable abstract class P implements ImmutableInterface<@Mutable Object> {} @Immutable abstract class Q implements ImmutableInterface<@Immutable Object> {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) @ReceiverDependantMutable abstract class R implements ImmutableInterface<@ReceiverDependantMutable Object> {} diff --git a/testinput/typecheck/CopyToCast.java b/testinput/typecheck/CopyToCast.java index ad77909..e1714b6 100644 --- a/testinput/typecheck/CopyToCast.java +++ b/testinput/typecheck/CopyToCast.java @@ -7,9 +7,9 @@ public class CopyToCast { void foo(Object o) { - // :: warning: (cast.unsafe) + // No cast.unsafe String s1 = (@Immutable String) o; - // :: warning: (cast.unsafe) + // No cast.unsafe String s2 = (String) o; // :: error: (type.invalid.annotations.on.use) String s3 = (@Mutable String) o; diff --git a/testinput/typecheck/DateCell.java b/testinput/typecheck/DateCell.java index 1786b6a..a9f19b4 100644 --- a/testinput/typecheck/DateCell.java +++ b/testinput/typecheck/DateCell.java @@ -7,9 +7,9 @@ import java.lang.SuppressWarnings; import java.util.Date; -// :: error: (initialization.fields.uninitialized) @ReceiverDependantMutable public class DateCell { + // :: error: (initialization.field.uninitialized) @ReceiverDependantMutable Date date; @ReceiverDependantMutable Date getDate(@ReceiverDependantMutable DateCell this) { diff --git a/testinput/typecheck/DateCell2.java b/testinput/typecheck/DateCell2.java index 2bb5985..28eb674 100644 --- a/testinput/typecheck/DateCell2.java +++ b/testinput/typecheck/DateCell2.java @@ -7,8 +7,8 @@ import java.util.Date; -// :: error: (initialization.fields.uninitialized) @ReceiverDependantMutable public class DateCell2 { + // :: error: (initialization.field.uninitialized) @Immutable Date imdate; @Immutable Date getImmutableDate(@PolyMutable DateCell2 this) { diff --git a/testinput/typecheck/DeepMutable.java b/testinput/typecheck/DeepMutable.java new file mode 100644 index 0000000..f10ea26 --- /dev/null +++ b/testinput/typecheck/DeepMutable.java @@ -0,0 +1,33 @@ +import qual.*; + +public class DeepMutable { + @Mutable + static class MutableBox {} + + @Immutable + static class ImmutableClass { + + // :: warning: (implicit.shallow.immutable) + MutableBox implicit = new MutableBox(); + + @Mutable MutableBox explicit = new MutableBox(); + } + + @Immutable + static class ImmutableGenericEx { + + T t; + @Immutable ImmutableGenericEx(T t) { + this.t = t; + } + } + + @Immutable + static class ImmutableGenericIm { + // :: warning: (implicit.shallow.immutable) + T t; + @Immutable ImmutableGenericIm(T t) { + this.t = t; + } + } +} \ No newline at end of file diff --git a/testinput/typecheck/DiamondTreeProblem.java b/testinput/typecheck/DiamondTreeProblem.java index 206acf3..f2a4a10 100644 --- a/testinput/typecheck/DiamondTreeProblem.java +++ b/testinput/typecheck/DiamondTreeProblem.java @@ -6,9 +6,6 @@ public class DiamondTreeProblem { void test1() { - // TODO This is WRONG even though test passed! Explicit @Immutable annotation - // on new instance creation is ignored and @Mutable is defaulted! - // :: error: (assignment.type.incompatible) @Immutable List l = new @Immutable ArrayList<>(); } diff --git a/testinput/typecheck/EnumConstantNotAlwaysMutable.java b/testinput/typecheck/EnumConstantNotAlwaysMutable.java index ea48386..0d93073 100644 --- a/testinput/typecheck/EnumConstantNotAlwaysMutable.java +++ b/testinput/typecheck/EnumConstantNotAlwaysMutable.java @@ -18,7 +18,7 @@ public class EnumConstantNotAlwaysMutable { @ReceiverDependantMutable Kind invalidKind; // :: error: (type.invalid.annotations.on.use) @Mutable Kind invalidKind2; - // :: error: (type.invalid.annotations.on.use) + // no error now @Readonly Kind invalidKind3; EnumConstantNotAlwaysMutable() { diff --git a/testinput/typecheck/EnumTests.java b/testinput/typecheck/EnumTests.java new file mode 100644 index 0000000..46fd328 --- /dev/null +++ b/testinput/typecheck/EnumTests.java @@ -0,0 +1,27 @@ +import qual.Immutable; +import qual.Mutable; + +// Enum is now only immutable by default, not implicit +public class EnumTests{ + void foo(/*immutable*/ MyEnum e) { + // :: error: (type.invalid.annotations.on.use) + @Mutable MyEnum mutableRef; + @Immutable MyEnum immutableRef = e; + + @Mutable MutableEnum mutEnumMutRef= MutableEnum.M1; + // :: error: (type.invalid.annotations.on.use) + @Immutable MutableEnum mutEnumImmRef; + } + + /*immutable*/ + private static enum MyEnum { + T1, + T2; + } + + @Mutable + private static enum MutableEnum { + M1, + M2; + } +} \ No newline at end of file diff --git a/testinput/typecheck/ForbidAssignmentCase.java b/testinput/typecheck/ForbidAssignmentCase.java index 69f6557..63f425c 100644 --- a/testinput/typecheck/ForbidAssignmentCase.java +++ b/testinput/typecheck/ForbidAssignmentCase.java @@ -36,6 +36,7 @@ static void ImmutableObjectCaptureMutableObject() { // But allow below: ro.f = new @Immutable Object(); } + static void ImmutableObjectGetMutableAlias() { @Mutable ForbidAssignmentCase mo = new @Mutable ForbidAssignmentCase(); @Readonly ForbidAssignmentCase ro = mo; diff --git a/testinput/typecheck/HashCodeSafetyExample.java b/testinput/typecheck/HashCodeSafetyExample.java index 5486b56..bee5792 100644 --- a/testinput/typecheck/HashCodeSafetyExample.java +++ b/testinput/typecheck/HashCodeSafetyExample.java @@ -16,7 +16,7 @@ public int hashCode() { @Override public boolean equals(Object obj) { - // :: warning: (cast.unsafe) + // No cast.unsafe return isIn == ((A)obj).isIn; } } diff --git a/testinput/typecheck/ImmutableClass1.java b/testinput/typecheck/ImmutableClass1.java index 33d79fd..a22acca 100644 --- a/testinput/typecheck/ImmutableClass1.java +++ b/testinput/typecheck/ImmutableClass1.java @@ -26,16 +26,7 @@ void method4(@PolyMutable ImmutableClass1 this) {} // :: error: (method.receiver.incompatible) :: error: (type.invalid.annotations.on.use) void method5(@Mutable ImmutableClass1 this) {} - // Note: the reason why there is no "type.invalid" error - // TODO Discuss with prof - // Declared receiver type has "different" types from different perspectives: - // when PICOVisitor#visitMethod() is called, "this" is defaulted to @Mutable; - // but when PICOVisitor#visitVariable() is called, "this" inheris @Immutable - // from its class element. So that's why we get "method.receiver.incompatible" - // error becasue method receiver is @Mutable, but we didn't get "type.invalid" - // because @Immutable ImmutableClass1 is the correct usage of ImmutableClass1. - // See comment: https://github.com/opprop/checker-framework/blob/master/framework/src/org/checkerframework/framework/type/AnnotatedTypeFactory.java#L1593 - // for why class bound annotation is not applied to instance method receiver - // :: error: (method.receiver.incompatible) + + // when not annotated explictly, default annotations of is inherited from declaration void method6(ImmutableClass1 this) {} } diff --git a/testinput/typecheck/ImmutableConstructor.java b/testinput/typecheck/ImmutableConstructor.java index 6cdcbca..6b200eb 100644 --- a/testinput/typecheck/ImmutableConstructor.java +++ b/testinput/typecheck/ImmutableConstructor.java @@ -36,13 +36,11 @@ void invokeConstructor(@Readonly ImmutableConstructor this, @Readonly Object ro, @ReceiverDependantMutable Object po, @Immutable Object io) { new @Immutable ImmutableConstructor(io, io); - // :: error: (type.invalid.annotations.on.use) + // :: error: (constructor.invocation.invalid) new @Mutable ImmutableConstructor(mo, io); - // This no longer is error now(?). Because instantiating @Immutable constructor - // as @PolyImmutable(PolymorphicQualifier) automatically resolves @PolyImmutable - // to @Immutable, which might be a good thing - // :: error: (type.invalid.annotations.on.use) + // constructor.invocation.invalid propgates before annotation invalid messages and stops + // :: error: (constructor.invocation.invalid) new @ReceiverDependantMutable ImmutableConstructor(po, io); // :: error: (constructor.invocation.invalid) :: error: (pico.new.invalid) diff --git a/testinput/typecheck/ImplicitAppliesToMethodReceiver.java b/testinput/typecheck/ImplicitAppliesToMethodReceiver.java index 86f523e..7e85fe8 100644 --- a/testinput/typecheck/ImplicitAppliesToMethodReceiver.java +++ b/testinput/typecheck/ImplicitAppliesToMethodReceiver.java @@ -5,6 +5,6 @@ public class ImplicitAppliesToMethodReceiver { void foo() { - double delta = new Double(1.0).doubleValue(); + double delta = Double.valueOf(1.0); } } diff --git a/testinput/typecheck/MethodReceiverNotInhericClassBound.java b/testinput/typecheck/MethodReceiverNotInhericClassBound.java index cb1e7dd..03b1a9c 100644 --- a/testinput/typecheck/MethodReceiverNotInhericClassBound.java +++ b/testinput/typecheck/MethodReceiverNotInhericClassBound.java @@ -4,6 +4,6 @@ @Immutable public class MethodReceiverNotInhericClassBound { - // :: error: (method.receiver.incompatible) - void foo() {} + // :: error: (method.receiver.incompatible) :: error: (type.invalid.annotations.on.use) + void bar(@Mutable MethodReceiverNotInhericClassBound this) {} } diff --git a/testinput/typecheck/MutableConstructor.java b/testinput/typecheck/MutableConstructor.java index 1fac2ef..0609785 100644 --- a/testinput/typecheck/MutableConstructor.java +++ b/testinput/typecheck/MutableConstructor.java @@ -35,9 +35,9 @@ void invokeConstructor(@Mutable Object mo, @ReceiverDependantMutable Object po, // :: error: (argument.type.incompatible) new @Mutable MutableConstructor(mo, po, io); // The same argument as the one in ImmutableConstructor - // :: error: (type.invalid.annotations.on.use) + // :: error: (constructor.invocation.invalid) new @ReceiverDependantMutable MutableConstructor(mo, po, io); - // :: error: (type.invalid.annotations.on.use) + // :: error: (constructor.invocation.invalid) new @Immutable MutableConstructor(mo, io, io); } } diff --git a/testinput/typecheck/NotEveryInstFieldDefaultToRDM.java b/testinput/typecheck/NotEveryInstFieldDefaultToRDM.java index e25d1c3..4923b89 100644 --- a/testinput/typecheck/NotEveryInstFieldDefaultToRDM.java +++ b/testinput/typecheck/NotEveryInstFieldDefaultToRDM.java @@ -7,8 +7,8 @@ public class NotEveryInstFieldDefaultToRDM { // :: error: (assignment.type.incompatible) @ReceiverDependantMutable B b1 = new B(); B b2 = new @ReceiverDependantMutable B(); - C c = new @Mutable C(); - D d = new @Mutable D(); + @Mutable C c = new @Mutable C(); + @Mutable D d = new @Mutable D(); E e = new @Immutable E(); } diff --git a/testinput/typecheck/ObjectIdentityMethodTest.java b/testinput/typecheck/ObjectIdentityMethodTest.java index 04dfb8b..d78080f 100644 --- a/testinput/typecheck/ObjectIdentityMethodTest.java +++ b/testinput/typecheck/ObjectIdentityMethodTest.java @@ -2,7 +2,7 @@ @ReceiverDependantMutable class A { - @Assignable B b; + @Assignable @Mutable B b; @ReceiverDependantMutable A() {} void bar(@Readonly A this) {} } diff --git a/testinput/typecheck/ObjectMethods.java b/testinput/typecheck/ObjectMethods.java index 7b33d7d..08cfa3f 100644 --- a/testinput/typecheck/ObjectMethods.java +++ b/testinput/typecheck/ObjectMethods.java @@ -145,7 +145,7 @@ public boolean equals(@Readonly ObjectMethods6 this, @Readonly Object o) { @Override protected @ReceiverDependantMutable Object clone(@Readonly ObjectMethods6 this) throws CloneNotSupportedException { - // :: warning: (cast.unsafe) + // No cast.unsafe return (@ReceiverDependantMutable Object) super.clone(); } diff --git a/testinput/typecheck/OnlyOneModifierIsUse.java b/testinput/typecheck/OnlyOneModifierIsUse.java index 728eefd..cc167ba 100644 --- a/testinput/typecheck/OnlyOneModifierIsUse.java +++ b/testinput/typecheck/OnlyOneModifierIsUse.java @@ -6,8 +6,8 @@ public class OnlyOneModifierIsUse { - // :: error: (type.invalid) + // :: error: (type.invalid.conflicting.annos) @Readonly @Immutable Object field; - // :: error: (type.invalid) + // :: error: (type.invalid.conflicting.annos) String @Readonly @Immutable [] array; } diff --git a/testinput/typecheck/Planet.java b/testinput/typecheck/Planet.java index f2ae25b..328ed03 100644 --- a/testinput/typecheck/Planet.java +++ b/testinput/typecheck/Planet.java @@ -85,7 +85,9 @@ public String toString() { public static void main(String[] args) { @Immutable Date discoveryDate = new @Immutable Date(); // :: error: (type.invalid.annotations.on.use) - @Mutable Planet mPlanet = new @Mutable Planet(1, "Earth", discoveryDate); + @Mutable Planet mPlanet; + // :: error: (constructor.invocation.invalid) + mPlanet = new @Mutable Planet(1, "Earth", discoveryDate); @Immutable Planet imPlanet = new @Immutable Planet(1, "Earth", discoveryDate); // None of the fields are allowed to be modified on an immutable object // :: error: (illegal.field.write) diff --git a/testinput/typecheck/PolyMutableOnConstructorParameters.java b/testinput/typecheck/PolyMutableOnConstructorParameters.java index d8f774d..a9e8842 100644 --- a/testinput/typecheck/PolyMutableOnConstructorParameters.java +++ b/testinput/typecheck/PolyMutableOnConstructorParameters.java @@ -4,7 +4,7 @@ import qual.PolyMutable; @Immutable -public class PolyMutableOnConstructorParameters { +public class PolyMutableOnConstructorParameters { @Immutable PolyMutableOnConstructorParameters(@PolyMutable Object o) { } diff --git a/testinput/typecheck/Primitive3.java b/testinput/typecheck/Primitive3.java index 8781976..eacb90b 100644 --- a/testinput/typecheck/Primitive3.java +++ b/testinput/typecheck/Primitive3.java @@ -13,7 +13,7 @@ void foo(Word word) { // I reenable type cast safety checking when the cast type is implicitly immutable. // Why should we suppress warning just because cast type is implicitly immutable? // That doesn't make any sense. Am I right? - // :: warning: (cast.unsafe) + // No cast.unsafe params[0] = (String) word.get(0); } } diff --git a/testinput/typecheck/RDMBug.java b/testinput/typecheck/RDMBug.java index 87c5705..897491f 100644 --- a/testinput/typecheck/RDMBug.java +++ b/testinput/typecheck/RDMBug.java @@ -5,9 +5,10 @@ import qual.Mutable; import qual.Readonly; -// :: error: (initialization.fields.uninitialized) @Immutable class RDMBug { + // :: error: (initialization.field.uninitialized) @Mutable Object o; + // :: error: (initialization.field.uninitialized) @Readonly Object o2; void foo(@Immutable RDMBug this) { // :: error: (illegal.field.write) diff --git a/testinput/typecheck/RDMField.java b/testinput/typecheck/RDMField.java new file mode 100644 index 0000000..3312e8a --- /dev/null +++ b/testinput/typecheck/RDMField.java @@ -0,0 +1,48 @@ +import qual.*; + +public class RDMField{ + + @Mutable + private static class MutableClass { + int field = 0; + } + + @ReceiverDependantMutable + private static class RDMHolder { + + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependantMutable MutableClass field = new MutableClass(); + @Mutable MutableClass mutableField = new MutableClass(); + + public @PolyMutable MutableClass getField(@PolyMutable RDMHolder this) { + return field; + } + + public void setField(@Mutable RDMHolder this, MutableClass field) { + this.field = field; + } + + void asImmutable(@Immutable RDMHolder r) { + // :: error: (illegal.field.write) + r.field.field = 1; + // :: error: (illegal.field.write) + r.getField().field = 1; + // :: error: (method.invocation.invalid) + r.setField(new MutableClass()); + } + } + + @Immutable + private static class ImmutableHolder { + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependantMutable MutableClass field = new MutableClass(); + + public @PolyMutable MutableClass getField(@PolyMutable ImmutableHolder this) { + return field; + } + + + + } +} + diff --git a/testinput/typecheck/RDMFieldInst.java b/testinput/typecheck/RDMFieldInst.java new file mode 100644 index 0000000..95bdda5 --- /dev/null +++ b/testinput/typecheck/RDMFieldInst.java @@ -0,0 +1,34 @@ +import qual.*; + +public class RDMFieldInst{ + @Mutable + private static class MutableBox {} + + @Immutable + private static class ImmutableBox {} + + @ReceiverDependantMutable + private static class RDMBox {} + + @Immutable + private static class ImmutableClass { + // :: error: (type.invalid.annotations.on.use) :: error: (initialization.field.uninitialized) + @ReceiverDependantMutable MutableBox mutableBoxInRDM; + } + + @Mutable + private static class MutableClass { + @ReceiverDependantMutable MutableBox mutableBoxInRDM = new MutableBox(); + + @ReceiverDependantMutable RDMBox rdmBoxInRDMnewM = new @Mutable RDMBox(); + // :: error: (assignment.type.incompatible) + @ReceiverDependantMutable RDMBox rdmBoxInRDMnewI = new @Immutable RDMBox(); + // :: error: (assignment.type.incompatible) + @ReceiverDependantMutable RDMBox rdmBoxInRDMnewRDM = new @ReceiverDependantMutable RDMBox(); + // :: error: (type.invalid.annotations.on.use) + @ReceiverDependantMutable ImmutableBox immutableBoxInRDM = new ImmutableBox(); + } + + + +} \ No newline at end of file diff --git a/testinput/typecheck/ReceiverTypeOutsideConstructor.java b/testinput/typecheck/ReceiverTypeOutsideConstructor.java index 9c63d14..c153c83 100644 --- a/testinput/typecheck/ReceiverTypeOutsideConstructor.java +++ b/testinput/typecheck/ReceiverTypeOutsideConstructor.java @@ -31,13 +31,13 @@ class A { @Immutable class AIMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) :: error: (super.invocation.invalid) @ReceiverDependantMutable class ARDMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) :: error: (super.invocation.invalid) @Mutable class AMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) :: error: (super.invocation.invalid) class AUNKS extends A {} // ReceiverDependantMutable class @@ -68,14 +68,14 @@ class B { @Immutable class BIMS extends B {} -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) @ReceiverDependantMutable class BRDMS extends B {} -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) @Mutable class BMS extends B {} // mutable by default(TODO Does this make sense compared to defaulting to receiver-dependant-mutable?) -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) class BUNKS extends B {} // Mutable class @@ -103,16 +103,16 @@ class C { } } -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) @Immutable class CIMS extends C {} -// :: error: (subclass.bound.incompatible) +// :: error: (type.invalid.annotations.on.use) :: error: (super.invocation.invalid) @ReceiverDependantMutable class CRDMS extends C {} -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) @Mutable class CMS extends C {} -// :: error: (super.constructor.invocation.incompatible) +// :: error: (super.invocation.invalid) class CUNKS extends C {} class D { diff --git a/testinput/typecheck/SuperClass.java b/testinput/typecheck/SuperClass.java index 3c71c82..c55d9f3 100644 --- a/testinput/typecheck/SuperClass.java +++ b/testinput/typecheck/SuperClass.java @@ -20,25 +20,25 @@ void maliciouslyModifyDate(@Mutable SuperClass this){ class SubClass extends SuperClass{ @Mutable SubClass(){ - // :: error: (super.constructor.invocation.incompatible) + // :: error: (super.invocation.invalid) super(new @Immutable Date(1L)); } public static void main(String[] args) { @Mutable SubClass victim = new @Mutable SubClass(); - victim.maliciouslyModifyDate();; + victim.maliciouslyModifyDate(); } } @ReceiverDependantMutable class AnotherSubClass extends SuperClass{ @ReceiverDependantMutable AnotherSubClass(){ - // :: error: (super.constructor.invocation.incompatible) + // :: error: (super.invocation.invalid) super(new @Immutable Date(1L)); } public static void main(String[] args) { @Mutable SubClass victim = new @Mutable SubClass(); - victim.maliciouslyModifyDate();; + victim.maliciouslyModifyDate(); } } diff --git a/testinput/typecheck/SuperClass2.java b/testinput/typecheck/SuperClass2.java index 00cfdee..1d5d567 100644 --- a/testinput/typecheck/SuperClass2.java +++ b/testinput/typecheck/SuperClass2.java @@ -35,7 +35,7 @@ public class SuperClass2{ class SubClass2 extends SuperClass2{ @Immutable SubClass2(){ // This is not ok any more - // :: error: (super.constructor.invocation.incompatible) + // :: error: (super.invocation.invalid) super(new @Mutable Date()); } } @@ -44,7 +44,7 @@ class SubClass2 extends SuperClass2{ class AnotherSubClass2 extends SuperClass2{ @ReceiverDependantMutable AnotherSubClass2(){ // This is not ok any more - // :: error: (super.constructor.invocation.incompatible) + // :: error: (super.invocation.invalid) super(new @Mutable Date()); } } diff --git a/testinput/typecheck/Transitive.java b/testinput/typecheck/Transitive.java new file mode 100644 index 0000000..8210ec7 --- /dev/null +++ b/testinput/typecheck/Transitive.java @@ -0,0 +1,46 @@ +import qual.Readonly; + +public class Transitive { + + // class A, B, C are not annotated to test transitive mutability by default. + + static class A { + B b; + + public B getB() { + return b; + } + } + + static class B { + int field = 0; + C c; + + public C getC() { + return c; + } + } + + static class C { + int field = 0; + } + + static class Caller { + void test(@Readonly A a) { + // :: error: (illegal.field.write) + a.b.field = 1; + // :: error: (method.invocation.invalid) + a.getB().field = 1; + + // :: error: (illegal.field.write) + a.b.c.field = 1; + // :: error: (method.invocation.invalid) + a.getB().getC().field = 1; + // :: error: (method.invocation.invalid) + a.b.getC().field = 1; + // :: error: (method.invocation.invalid) + a.getB().c.field = 1; + } + } +} +