diff --git a/.travis-build.sh b/.travis-build.sh index 014ec81..1a9c977 100755 --- a/.travis-build.sh +++ b/.travis-build.sh @@ -10,47 +10,29 @@ export CHECKERFRAMEWORK=$JSR308/checker-framework export PATH=$AFU/scripts:$JAVA_HOME/bin:$PATH #default value is opprop. REPO_SITE may be set to other value for travis test purpose. -export REPO_SITE=topnessman +export REPO_SITE=baoruiz echo "------ Downloading everthing from REPO_SITE: $REPO_SITE ------" -# Clone annotation-tools (Annotation File Utilities) -if [ -d $JSR308/annotation-tools ] ; then - (cd $JSR308/annotation-tools && git pull) -else - (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/annotation-tools.git) -fi - -# Clone stubparser -if [ -d $JSR308/stubparser ] ; then - (cd $JSR308/stubparser && git pull) -else - (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/stubparser.git) -fi # Clone checker-framework if [ -d $JSR308/checker-framework ] ; then - (cd $JSR308/checker-framework && git checkout pico-dependant-copy && git pull) + (cd $JSR308/checker-framework && git checkout pull-pico-changes && git pull) else - # ViewpointAdapter changes are not yet merged to master, so we depend on pico-dependant branch - (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/checker-framework.git) + (cd $JSR308 && git clone -b pull-pico-changes --depth 1 https://github.com/"$REPO_SITE"/checker-framework.git) fi # Clone checker-framework-inference if [ -d $JSR308/checker-framework-inference ] ; then - (cd $JSR308/checker-framework-inference && git checkout pico-dependant-copy && git pull) + (cd $JSR308/checker-framework-inference && git checkout pull-pico-changes && git pull) else - # Again we depend on pico-dependant branch - (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git) + (cd $JSR308 && git clone -b pull-pico-changes --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git) fi -# Build annotation-tools (and jsr308-langtools) -(cd $JSR308/annotation-tools/ && ./.travis-build-without-test.sh) -# Build stubparser -(cd $JSR308/stubparser/ && mvn package -Dmaven.test.skip=true) # Build checker-framework, with downloaded jdk -(cd $JSR308/checker-framework && ant -f checker/build.xml dist-downloadjdk) +(cd $JSR308/checker-framework && ./.travis-build-without-test.sh downloadjdk) + # Build checker-framework-inference -(cd $JSR308/checker-framework-inference && gradle dist) # This step needs to be manually in $CFI executed due to path problems +(cd $JSR308/checker-framework-inference && ./gradlew dist) # Build PICO (cd $JSR308/immutability && ./gradlew build) 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/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index 386a4de..5ffdc69 100644 --- a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java @@ -20,7 +20,7 @@ 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.treeannotator.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; @@ -28,7 +28,7 @@ import org.checkerframework.framework.type.typeannotator.TypeAnnotator; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator; +import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator; import pico.typecheck.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; @@ -62,17 +62,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 @@ -235,7 +235,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/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index 1157e2d..f159883 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -11,7 +11,6 @@ import java.util.List; import java.util.Set; -import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; @@ -19,8 +18,8 @@ import org.checkerframework.framework.qual.RelevantJavaTypes; 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; @@ -31,7 +30,8 @@ import com.sun.source.tree.Tree; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator; +import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator; +import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOTreeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator; @@ -55,7 +55,9 @@ public class PICOInferenceRealTypeFactory extends BaseAnnotatedTypeFactory { 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); + } postInit(); } @@ -82,7 +84,7 @@ protected AbstractViewpointAdapter createViewpointAdapter() { protected TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( new PICOPropagationTreeAnnotator(this), - new ImplicitsTreeAnnotator(this), + new LiteralTreeAnnotator(this), new PICOTreeAnnotator(this)); } @@ -107,7 +109,7 @@ 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)); return new ListTypeAnnotator(typeAnnotators); } @@ -125,21 +127,6 @@ 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); diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 0a0d390..61bc4a3 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -23,10 +23,11 @@ import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; 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; @@ -166,14 +167,6 @@ public boolean validateTypeOf(Tree tree) { // 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) { @@ -192,7 +185,7 @@ 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) { if (infer) { AnnotationMirror constructorReturn = extractVarAnnot(constructor.getReturnType()); mainIsSubtype(invocation, constructorReturn, "constructor.invocation.invalid", newClassTree); @@ -201,10 +194,10 @@ protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, A if (!atypeFactory.getTypeHierarchy().isSubtype(invocation, returnType)) { checker.report(Result.failure( "constructor.invocation.invalid", invocation, returnType), newClassTree); - return false; + return; } } - return super.checkConstructorInvocation(invocation, constructor, newClassTree); + super.checkConstructorInvocation(invocation, constructor, newClassTree); } private AnnotationMirror extractVarAnnot(final AnnotatedTypeMirror atm) { @@ -418,7 +411,7 @@ 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); @@ -429,7 +422,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. @@ -541,7 +535,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) @@ -559,7 +553,7 @@ private boolean isInitializingObject(ExpressionTree variable) { } MethodTree enclosingMethod = TreeUtils.enclosingMethod(treePath); - // No possibility of initialiazing object if the assignment is not within constructor or method(both MethodTree) + // 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)) { @@ -620,14 +614,14 @@ private void checkNewInstanceCreation(Tree node) { @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; @@ -648,7 +642,7 @@ protected void checkMethodInvocability(AnnotatedExecutableType method, MethodInv // , otherwise it will cause inference result not typecheck checker.report( Result.failure( - "super.constructor.invocation.incompatible", subClassConstructorReturnType, superClassConstructorReturnType), node); + "super.invocation.invalid", subClassConstructorReturnType, superClassConstructorReturnType), node); } } super.checkMethodInvocability(method, node); @@ -817,8 +811,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)) { diff --git a/src/main/java/pico/inference/PICOVariableAnnotator.java b/src/main/java/pico/inference/PICOVariableAnnotator.java index 65893b2..3971845 100644 --- a/src/main/java/pico/inference/PICOVariableAnnotator.java +++ b/src/main/java/pico/inference/PICOVariableAnnotator.java @@ -69,7 +69,7 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) { // Insert @Immutable VarAnnot directly to enum bound if (PICOTypeUtil.isEnumOrEnumConstant(bound)) { - boundSlot = createConstant(IMMUTABLE); + boundSlot = slotManager.createConstantSlot(IMMUTABLE); classType.addAnnotation(slotManager.getAnnotation(boundSlot)); classDeclAnnos.put(classElement, boundSlot); return; @@ -80,7 +80,7 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) { // Have source tree if (bound.isAnnotatedInHierarchy(READONLY)) { // Have bound annotation -> convert to equivalent ConstantSlot - boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY)); + boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY)); } else { // No existing annotation -> create new VariableSlot boundSlot = createVariable(treeToLocation(classTree)); @@ -89,15 +89,15 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) { // No source tree: bytecode classes if (bound.isAnnotatedInHierarchy(READONLY)) { // Have bound annotation in stub file - boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY)); + boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY)); } else { // No stub file if (PICOTypeUtil.isImplicitlyImmutableType(classType)) { // Implicitly immutable - boundSlot = createConstant(IMMUTABLE); + boundSlot = slotManager.createConstantSlot(IMMUTABLE); } else { // None of the above applies: use conservative @Mutable - boundSlot = createConstant(MUTABLE); + boundSlot = slotManager.createConstantSlot(MUTABLE); } } } diff --git a/src/main/java/pico/inference/solver/PICOSolverEngine.java b/src/main/java/pico/inference/solver/PICOSolverEngine.java index 213a809..8fb26bc 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; @@ -28,7 +28,7 @@ public class PICOSolverEngine extends SolverEngine { 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); + writeInferenceResult("pico-inference-result.txt", ((DefaultInferenceResult)result).varIdToAnnotation); } return result; } diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 77bef15..77e5c98 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -34,11 +34,11 @@ 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.DefaultForTypeAnnotator; import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator; import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; import org.checkerframework.framework.type.typeannotator.PropagationTypeAnnotator; @@ -50,13 +50,9 @@ import org.checkerframework.javacutil.TreeUtils; 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; @@ -82,9 +78,11 @@ public class PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory PICOStore, PICOTransfer, PICOAnalysis> { 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 @@ -114,7 +112,7 @@ protected ViewpointAdapter createViewpointAdapter() { protected TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( new PICOPropagationTreeAnnotator(this), - new ImplicitsTreeAnnotator(this), + new LiteralTreeAnnotator(this), new CommitmentTreeAnnotator(this), new PICOTreeAnnotator(this)); } @@ -140,7 +138,7 @@ 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 CommitmentTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } @@ -185,20 +183,6 @@ public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror 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. @@ -240,11 +224,11 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { /**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); + 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.methodType; + AnnotatedExecutableType methodType = pair.executableType; AnnotatedTypeMirror returnType = methodType.getReturnType(); if (returnType.hasAnnotation(POLY_MUTABLE)) { // Only substitute polymutable but not other qualifiers! Missing the if statement @@ -391,7 +375,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. We use addMissingAnnotations because we want to respect existing annotation on type*/ private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) { @@ -413,31 +397,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 @@ -488,9 +447,9 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { } - public static class PICOImplicitsTypeAnnotator extends ImplicitsTypeAnnotator { + public static class PICODefaultForTypeAnnotator extends DefaultForTypeAnnotator { - public PICOImplicitsTypeAnnotator(AnnotatedTypeFactory typeFactory) { + public PICODefaultForTypeAnnotator(AnnotatedTypeFactory typeFactory) { super(typeFactory); } @@ -520,7 +479,7 @@ 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. 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/PICOTypeUtil.java b/src/main/java/pico/typecheck/PICOTypeUtil.java index abaff17..994f1d8 100644 --- a/src/main/java/pico/typecheck/PICOTypeUtil.java +++ b/src/main/java/pico/typecheck/PICOTypeUtil.java @@ -6,7 +6,6 @@ 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; @@ -14,7 +13,7 @@ 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 org.checkerframework.framework.qual.DefaultFor; import org.checkerframework.framework.qual.TypeKind; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -65,23 +64,23 @@ public class PICOTypeUtil { } 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; + DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + assert defaultFor.typeKinds() != 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()) { + if (!atm.getKind().name().equals(TypeKind.DECLARED.name())) { return false; } - ImplicitFor implicitFor = Immutable.class.getAnnotation(ImplicitFor.class); + DefaultFor implicitFor = Immutable.class.getAnnotation(DefaultFor.class); assert implicitFor != null; - assert implicitFor.typeNames() != null; - Class[] typeNames = implicitFor.typeNames(); + assert implicitFor.types() != null; + Class[] typeNames = implicitFor.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; @@ -399,34 +398,6 @@ 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; - } - } - } - - 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)); - } - } - } - public static boolean isSideEffectingUnaryTree(final UnaryTree tree) { return sideEffectingUnaryOperators.contains(tree.getKind()); } diff --git a/src/main/java/pico/typecheck/PICOValidator.java b/src/main/java/pico/typecheck/PICOValidator.java index 9e042bf..d776200 100644 --- a/src/main/java/pico/typecheck/PICOValidator.java +++ b/src/main/java/pico/typecheck/PICOValidator.java @@ -59,7 +59,7 @@ private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, } } - /**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)) { diff --git a/src/main/java/pico/typecheck/PICOViewpointAdapter.java b/src/main/java/pico/typecheck/PICOViewpointAdapter.java index fdb3d4d..392bfe3 100644 --- a/src/main/java/pico/typecheck/PICOViewpointAdapter.java +++ b/src/main/java/pico/typecheck/PICOViewpointAdapter.java @@ -57,7 +57,7 @@ protected AnnotationMirror combineAnnotationWithAnnotation(AnnotationMirror rece } 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()); } } // diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 5249ae4..e8478ea 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -8,6 +8,7 @@ import static pico.typecheck.PICOAnnotationMirrorHolder.READONLY; import static pico.typecheck.PICOAnnotationMirrorHolder.RECEIVER_DEPENDANT_MUTABLE; +import com.sun.source.util.TreePath; import java.util.HashMap; import java.util.HashSet; import java.util.List; @@ -21,12 +22,13 @@ import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; +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; @@ -86,7 +88,7 @@ public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclar // 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 +// // of doing this using any existing 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 @@ -101,7 +103,7 @@ public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclar return true; } // At this point, element type can only be @Mutable or @Immutable. Otherwise, it's a problem in - // PICOVisitor#processorClassTree(ClassTree) + // PICOVisitor#processClassTree(ClassTree) assert AnnotationUtils.areSame(declared, MUTABLE) || AnnotationUtils.areSame(declared, IMMUTABLE); AnnotationMirror used = useType.getAnnotationInHierarchy(READONLY); @@ -131,8 +133,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)) { @@ -156,7 +156,7 @@ protected void commonAssignmentCheck( } @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(); @@ -183,9 +183,7 @@ protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, A if (!atypeFactory.getTypeHierarchy().isSubtype(invocation, returnType, READONLY)) { checker.report(Result.failure( "constructor.invocation.invalid", invocation, returnType), newClassTree); - return false; } - return true; } @Override @@ -382,67 +380,19 @@ private void checkNewInstanceCreation(Tree node) { @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; @@ -502,63 +452,74 @@ public void processClassTree(ClassTree node) { checker.report(Result.failure("class.bound.invalid", bound), node); return;// Doesn't process the class tree anymore } - if (!checkCompatabilityBetweenBoundAndSuperClassesBounds(node, typeElement, bound)) { - return; - } - - 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 continue if bound check - // passed. Reaching here already means having passed bound check. 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; - } + + @Override + protected void checkExtendsImplements(ClassTree classTree) { + if (TypesUtils.isAnonymous(TreeUtils.typeOf(classTree))) { + // Don't check extends clause on anonymous classes. + return; } - return true; + + AnnotationMirror classAnnot = + atypeFactory.getAnnotatedType(classTree).getAnnotationInHierarchy(READONLY); + + Tree extendsClause = classTree.getExtendsClause(); + if (extendsClause != null) { + AnnotationMirror extAnnot = atypeFactory.fromTypeTree(extendsClause).getAnnotationInHierarchy(READONLY); + if (extAnnot != null && !AnnotationUtils.areSame(extAnnot, classAnnot)) { + checker.report( + Result.failure( + "declaration.inconsistent.with.extends.clause", + classAnnot, + extAnnot), + extendsClause); + } + + } + + List implementsClauses = classTree.getImplementsClause(); + if (implementsClauses != null) { + for (Tree impl : implementsClauses) { + AnnotationMirror implAnnot = atypeFactory.fromTypeTree(impl).getAnnotationInHierarchy(READONLY); + if (implAnnot != null && !AnnotationUtils.areSame(implAnnot, classAnnot)) { + checker.report( + Result.failure( + "declaration.inconsistent.with.implements.clause", + classAnnot, + implAnnot), + impl); + } + } + } } - 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; - } - } - - 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; - } - } + /** + * 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 = visitorState.getMethodTree(); + 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.report( + Result.failure(errorKey, constructorTypeMirror, superCall, superTypeMirror), + superCall); } - return true; + super.checkThisOrSuperConstructorCall(superCall, errorKey); } } 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..5306a1b 100644 --- a/src/main/java/qual/Bottom.java +++ b/src/main/java/qual/Bottom.java @@ -1,22 +1,14 @@ 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.TypeUseLocation; +import org.checkerframework.framework.qual.*; import java.lang.annotation.Documented; -import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; @SubtypeOf({Mutable.class, Immutable.class, PolyMutable.class, ReceiverDependantMutable.class}) @DefaultFor({ TypeUseLocation.LOWER_BOUND }) -@ImplicitFor(literals = {LiteralKind.NULL}) @Documented @Retention(RetentionPolicy.RUNTIME) // Stop allowing any explicit usage of @Bottom qualifier in source. As it causes difficulty to diff --git a/src/main/java/qual/Immutable.java b/src/main/java/qual/Immutable.java index eb66e07..b5e542b 100644 --- a/src/main/java/qual/Immutable.java +++ b/src/main/java/qual/Immutable.java @@ -1,6 +1,7 @@ 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; @@ -17,10 +18,10 @@ @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}) public @interface Immutable {} diff --git a/src/main/java/qual/Readonly.java b/src/main/java/qual/Readonly.java index f80ef75..17ce4b5 100644 --- a/src/main/java/qual/Readonly.java +++ b/src/main/java/qual/Readonly.java @@ -1,7 +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; diff --git a/src/test/java/pico/ImmutabilityTypecheckTests.java b/src/test/java/pico/ImmutabilityTypecheckTest.java similarity index 83% rename from src/test/java/pico/ImmutabilityTypecheckTests.java rename to src/test/java/pico/ImmutabilityTypecheckTest.java index a07d004..41482b6 100644 --- a/src/test/java/pico/ImmutabilityTypecheckTests.java +++ b/src/test/java/pico/ImmutabilityTypecheckTest.java @@ -9,8 +9,8 @@ import java.util.ArrayList; import java.util.List; -public class ImmutabilityTypecheckTests extends CheckerFrameworkPerFileTest { - public ImmutabilityTypecheckTests(File testFile) { +public class ImmutabilityTypecheckTest extends CheckerFrameworkPerFileTest { + public ImmutabilityTypecheckTest(File testFile) { super(testFile, PICOChecker.class, "", "-Anomsgtext", "-Anocheckjdk", "-d", "testTmp/typecheck"); } 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/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..7f079b6 100644 --- a/testinput/typecheck/CompatabilityBEI1.java +++ b/testinput/typecheck/CompatabilityBEI1.java @@ -32,18 +32,18 @@ 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) +// :: error: (declaration.inconsistent.with.implements.clause) @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) +// :: error: (declaration.inconsistent.with.extends.clause) @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 75% rename from testinput/typecheck/CompatabilityBEI2.java rename to testinput/typecheck/CompatibilityBEI2.java index 065c652..440de14 100644 --- a/testinput/typecheck/CompatabilityBEI2.java +++ b/testinput/typecheck/CompatibilityBEI2.java @@ -25,28 +25,28 @@ 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) +// :: error: (declaration.inconsistent.with.implements.clause) @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) +// :: error: (declaration.inconsistent.with.extends.clause) @Immutable class N extends @ReceiverDependantMutable ArrayList<@Immutable Object> {} abstract class O implements CharSequence {} @Immutable interface ImmutableInterface {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.implements.clause) :: error: (type.argument.type.incompatible) @Mutable abstract class P implements ImmutableInterface<@Mutable Object> {} @Immutable abstract class Q implements ImmutableInterface<@Immutable Object> {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.implements.clause) :: error: (type.argument.type.incompatible) @ReceiverDependantMutable abstract class R implements ImmutableInterface<@ReceiverDependantMutable Object> {} 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/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/ReceiverTypeOutsideConstructor.java b/testinput/typecheck/ReceiverTypeOutsideConstructor.java index 9c63d14..7162e32 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: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) @ReceiverDependantMutable class ARDMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) @Mutable class AMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.extends.clause) :: 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: (declaration.inconsistent.with.extends.clause) @Immutable class CIMS extends C {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.extends.clause) :: 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()); } }