From 1b0c6db228df720ba41d75423a8841d291734cba Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Wed, 20 Mar 2019 11:57:24 -0400 Subject: [PATCH 01/23] adapt pico to CF and CFI master --- src/main/java/pico/inference/PICOInferenceVisitor.java | 6 ++++-- .../java/pico/inference/PICOVariableAnnotator.java | 10 +++++----- .../java/pico/inference/solver/PICOSolverEngine.java | 4 ++-- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 0a0d390..b851714 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -27,6 +27,7 @@ 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; @@ -418,7 +419,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 +430,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. 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; } From b73d0c04b3ba1033d0847cbf20e5c6879d75e70a Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Thu, 28 Mar 2019 14:26:09 -0400 Subject: [PATCH 02/23] fix pico per changes in upstream CF and CFI --- .../inference/PICOInferenceRealTypeFactory.java | 4 +++- .../pico/inference/PICOInferenceVisitor.java | 16 +++------------- .../pico/typecheck/PICOAnnotatedTypeFactory.java | 10 ++++++---- src/main/java/pico/typecheck/PICOVisitor.java | 8 +++----- 4 files changed, 15 insertions(+), 23 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index 1157e2d..3c247ea 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -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(); } diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index b851714..c8bb53c 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -23,7 +23,7 @@ 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; @@ -167,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) { @@ -622,9 +614,9 @@ 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 @@ -819,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/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 77bef15..406a935 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -84,7 +84,9 @@ public class PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory public PICOAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); postInit(); - addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + if (READONLY != null) { + addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); + } } @Override @@ -240,11 +242,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 diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 5249ae4..5696178 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -26,7 +26,7 @@ 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; @@ -131,8 +131,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)) { @@ -382,9 +380,9 @@ 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 From 896d9c424892bc86cb486205749485d68a6fe078 Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Tue, 2 Apr 2019 12:11:02 -0400 Subject: [PATCH 03/23] remove incorrect aliasing and unnecessary method check --- .../typecheck/PICOAnnotatedTypeFactory.java | 6 +-- src/main/java/pico/typecheck/PICOVisitor.java | 48 ------------------- 2 files changed, 3 insertions(+), 51 deletions(-) diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 406a935..3a43805 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -84,9 +84,9 @@ public class PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory public PICOAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); postInit(); - if (READONLY != null) { - addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); - } + // PICO aliasing is not implemented correctly + // remove for now +// addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY); } @Override diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 5696178..e0dbd13 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -393,54 +393,6 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { 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; From 8b3a4443d774a4085a5415961b8f84f9c31fbde7 Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Thu, 18 Apr 2019 18:22:29 -0400 Subject: [PATCH 04/23] remove wrong test diagnostic --- testinput/typecheck/DiamondTreeProblem.java | 3 --- 1 file changed, 3 deletions(-) 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<>(); } From f0341b807b1bf900dff9ea276791bdc8181928e3 Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Thu, 18 Apr 2019 18:26:34 -0400 Subject: [PATCH 05/23] adapt to upstream changes --- src/main/java/pico/inference/PICOInferenceVisitor.java | 6 +++--- src/main/java/pico/typecheck/PICOVisitor.java | 4 +--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index c8bb53c..83dedd6 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -185,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); @@ -194,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) { diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index e0dbd13..4587458 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -154,7 +154,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(); @@ -181,9 +181,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 From c327e41c4442c09024291674acf200382a5be9e9 Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Wed, 24 Apr 2019 12:39:19 -0400 Subject: [PATCH 06/23] fix extends and implements check --- .../typecheck/PICOAnnotatedTypeFactory.java | 29 ------ .../java/pico/typecheck/PICOTypeUtil.java | 29 ------ src/main/java/pico/typecheck/PICOVisitor.java | 92 ++++++++----------- testinput/typecheck/CompatabilityBEI1.java | 8 +- testinput/typecheck/CompatabilityBEI2.java | 12 +-- .../ReceiverTypeOutsideConstructor.java | 10 +- 6 files changed, 53 insertions(+), 127 deletions(-) diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 3a43805..db6dd28 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -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; @@ -415,31 +411,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 diff --git a/src/main/java/pico/typecheck/PICOTypeUtil.java b/src/main/java/pico/typecheck/PICOTypeUtil.java index abaff17..8d32462 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; @@ -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/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 4587458..45ec4d1 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -450,63 +450,47 @@ 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; - } - } - return true; - } - - 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; - } - } + + @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); + } + } + } } } 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/CompatabilityBEI2.java index 065c652..166d479 100644 --- a/testinput/typecheck/CompatabilityBEI2.java +++ b/testinput/typecheck/CompatabilityBEI2.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) @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) @ReceiverDependantMutable abstract class R implements ImmutableInterface<@ReceiverDependantMutable Object> {} diff --git a/testinput/typecheck/ReceiverTypeOutsideConstructor.java b/testinput/typecheck/ReceiverTypeOutsideConstructor.java index 9c63d14..62eb1e6 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) @ReceiverDependantMutable class ARDMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.extends.clause) @Mutable class AMS extends A {} -// :: error: (subclass.bound.incompatible) +// :: error: (declaration.inconsistent.with.extends.clause) class AUNKS extends A {} // ReceiverDependantMutable class @@ -103,10 +103,10 @@ 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) @ReceiverDependantMutable class CRDMS extends C {} // :: error: (super.constructor.invocation.incompatible) From d1801677a380d7dc47f2d19fe5f8ca90cde33419 Mon Sep 17 00:00:00 2001 From: Baorui Zhou Date: Tue, 30 Apr 2019 11:33:37 -0400 Subject: [PATCH 07/23] tweak travis build script --- .travis-build.sh | 34 ++++++++-------------------------- 1 file changed, 8 insertions(+), 26 deletions(-) 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) From 9a70a425e630d7e8bccccd3962580bf60b2494f3 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Tue, 2 Jul 2019 21:55:58 -0400 Subject: [PATCH 08/23] Remove useless separators. --- testinput/typecheck/SuperClass.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/testinput/typecheck/SuperClass.java b/testinput/typecheck/SuperClass.java index 3c71c82..d857b7d 100644 --- a/testinput/typecheck/SuperClass.java +++ b/testinput/typecheck/SuperClass.java @@ -26,7 +26,7 @@ class SubClass extends SuperClass{ public static void main(String[] args) { @Mutable SubClass victim = new @Mutable SubClass(); - victim.maliciouslyModifyDate();; + victim.maliciouslyModifyDate(); } } @@ -39,6 +39,6 @@ class AnotherSubClass extends SuperClass{ public static void main(String[] args) { @Mutable SubClass victim = new @Mutable SubClass(); - victim.maliciouslyModifyDate();; + victim.maliciouslyModifyDate(); } } From 6fe2e8d4be0903fe6a18af770479066d26037891 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Wed, 10 Jul 2019 16:36:06 -0400 Subject: [PATCH 09/23] Unify the name of test files. --- build.gradle | 2 +- ...lityInferenceTest.java => ImmutabilityInferenceTests.java} | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) rename src/test/java/pico/{ImmutabilityInferenceTest.java => ImmutabilityInferenceTests.java} (91%) diff --git a/build.gradle b/build.gradle index c41e6d1..ac276e0 100644 --- a/build.gradle +++ b/build.gradle @@ -79,7 +79,7 @@ afterEvaluate { // Create a task for each JUnit test class whose name is the same as the JUnit class name. sourceSets.test.allJava.filter { it.path.contains("${picoPath}/src/test/java") }.forEach { file -> String junitClassName = file.name.replaceAll(".java", "") - String testName = junitClassName.replaceAll("Test", "") + String testName = junitClassName.replaceAll("Tests", "") tasks.create(name: "${junitClassName}", type: Test) { description "Run ${testName} tests." include "**/${name}.class" diff --git a/src/test/java/pico/ImmutabilityInferenceTest.java b/src/test/java/pico/ImmutabilityInferenceTests.java similarity index 91% rename from src/test/java/pico/ImmutabilityInferenceTest.java rename to src/test/java/pico/ImmutabilityInferenceTests.java index 59b88a8..d8fcc90 100644 --- a/src/test/java/pico/ImmutabilityInferenceTest.java +++ b/src/test/java/pico/ImmutabilityInferenceTests.java @@ -13,9 +13,9 @@ import pico.inference.PICOInferenceChecker; import pico.inference.solver.PICOSolverEngine; -public class ImmutabilityInferenceTest extends CFInferenceTest { +public class ImmutabilityInferenceTests extends CFInferenceTest { - public ImmutabilityInferenceTest(File testFile) { + public ImmutabilityInferenceTests(File testFile) { super(testFile, PICOInferenceChecker.class, "", "-Anomsgtext", "-Astubs=src/main/java/pico/typecheck/jdk.astub", "-d", "testdata/inference/inferrable"); } From 7ba8f20daee35bb64d48dcad0223cfa0639fc252 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Wed, 24 Jul 2019 19:41:48 -0400 Subject: [PATCH 10/23] Fix typo. --- src/main/java/pico/typecheck/PICOValidator.java | 2 +- src/main/java/pico/typecheck/PICOVisitor.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 45ec4d1..f018e93 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -86,7 +86,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 From d186ece87a62b53682dd3e10aeafa0923cbc540a Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Wed, 24 Jul 2019 19:47:27 -0400 Subject: [PATCH 11/23] Fix typo. --- src/main/java/pico/typecheck/PICOVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index f018e93..1e46d0c 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -101,7 +101,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); From ccda9f0cdedba4e20dbda2dc646a998e3ffb0924 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Thu, 25 Jul 2019 20:29:39 -0400 Subject: [PATCH 12/23] Fix typo. --- src/main/java/pico/typecheck/PICOViewpointAdapter.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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()); } } // From 2dd8b63eccad06ce95b84f2ca8ba3fa683b821b6 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Sat, 27 Jul 2019 00:10:30 -0400 Subject: [PATCH 13/23] Complete the messages. --- src/main/java/pico/typecheck/messages.properties | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/java/pico/typecheck/messages.properties b/src/main/java/pico/typecheck/messages.properties index 105fe05..9040ed2 100644 --- a/src/main/java/pico/typecheck/messages.properties +++ b/src/main/java/pico/typecheck/messages.properties @@ -1,8 +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 +method.receiver.incompatible=Incompatible method receiver: %s +class.bound.invalid=Invalid class bound: %s +subclass.bound.incompatible=Incompatible subclass bound: %s super.constructor.invocation.incompatible=Subclass constructor: %s is not compatible with super class constructor: %s illegal.field.write=Cannot write field via receiver: %s illegal.array.write=Cannot write array via receiver: %s From 5cd4f4d5c24c81546116d672d805d754bc1c0cd8 Mon Sep 17 00:00:00 2001 From: Weitian Xing <13183370+xingweitian@users.noreply.github.com> Date: Sun, 28 Jul 2019 10:52:37 -0400 Subject: [PATCH 14/23] Use all dirs and jar file to fix the issue that "messages.properties" cannot be found. (#1) --- check.sh | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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" From c76583d057948b3cf4f41b3739affde0587d656e Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Sun, 28 Jul 2019 13:59:03 -0400 Subject: [PATCH 15/23] Tweaks. --- build.gradle | 2 +- ...lityInferenceTests.java => ImmutabilityInferenceTest.java} | 4 ++-- ...lityTypecheckTests.java => ImmutabilityTypecheckTest.java} | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) rename src/test/java/pico/{ImmutabilityInferenceTests.java => ImmutabilityInferenceTest.java} (91%) rename src/test/java/pico/{ImmutabilityTypecheckTests.java => ImmutabilityTypecheckTest.java} (83%) diff --git a/build.gradle b/build.gradle index ac276e0..c41e6d1 100644 --- a/build.gradle +++ b/build.gradle @@ -79,7 +79,7 @@ afterEvaluate { // Create a task for each JUnit test class whose name is the same as the JUnit class name. sourceSets.test.allJava.filter { it.path.contains("${picoPath}/src/test/java") }.forEach { file -> String junitClassName = file.name.replaceAll(".java", "") - String testName = junitClassName.replaceAll("Tests", "") + String testName = junitClassName.replaceAll("Test", "") tasks.create(name: "${junitClassName}", type: Test) { description "Run ${testName} tests." include "**/${name}.class" diff --git a/src/test/java/pico/ImmutabilityInferenceTests.java b/src/test/java/pico/ImmutabilityInferenceTest.java similarity index 91% rename from src/test/java/pico/ImmutabilityInferenceTests.java rename to src/test/java/pico/ImmutabilityInferenceTest.java index d8fcc90..59b88a8 100644 --- a/src/test/java/pico/ImmutabilityInferenceTests.java +++ b/src/test/java/pico/ImmutabilityInferenceTest.java @@ -13,9 +13,9 @@ import pico.inference.PICOInferenceChecker; import pico.inference.solver.PICOSolverEngine; -public class ImmutabilityInferenceTests extends CFInferenceTest { +public class ImmutabilityInferenceTest extends CFInferenceTest { - public ImmutabilityInferenceTests(File testFile) { + public ImmutabilityInferenceTest(File testFile) { super(testFile, PICOInferenceChecker.class, "", "-Anomsgtext", "-Astubs=src/main/java/pico/typecheck/jdk.astub", "-d", "testdata/inference/inferrable"); } 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"); } From c4daeb9d810573c7fbb91e0cff70fdb0ebd091b0 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Mon, 29 Jul 2019 20:05:59 -0400 Subject: [PATCH 16/23] Use the correct error key. --- testinput/typecheck/OnlyOneModifierIsUse.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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; } From 67e4661eb7072e1eb5e0e0dbabe23a48e9ac6d56 Mon Sep 17 00:00:00 2001 From: Weitian Xing <13183370+xingweitian@users.noreply.github.com> Date: Sun, 18 Aug 2019 17:18:02 -0400 Subject: [PATCH 17/23] Fix typo (CompatabilityBEI2.java -> CompatibilityBEI2.java) and make CompatibilityBEI2.java pass. (#8) Make CompatibilityBEI2.java pass. --- .../{CompatabilityBEI2.java => CompatibilityBEI2.java} | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename testinput/typecheck/{CompatabilityBEI2.java => CompatibilityBEI2.java} (88%) diff --git a/testinput/typecheck/CompatabilityBEI2.java b/testinput/typecheck/CompatibilityBEI2.java similarity index 88% rename from testinput/typecheck/CompatabilityBEI2.java rename to testinput/typecheck/CompatibilityBEI2.java index 166d479..440de14 100644 --- a/testinput/typecheck/CompatabilityBEI2.java +++ b/testinput/typecheck/CompatibilityBEI2.java @@ -43,10 +43,10 @@ abstract class O implements CharSequence {} @Immutable interface ImmutableInterface {} -// :: error: (declaration.inconsistent.with.implements.clause) +// :: 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: (declaration.inconsistent.with.implements.clause) +// :: error: (declaration.inconsistent.with.implements.clause) :: error: (type.argument.type.incompatible) @ReceiverDependantMutable abstract class R implements ImmutableInterface<@ReceiverDependantMutable Object> {} From 4c581c29e88d43a6527992c5cde3495c8c9fc07a Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Mon, 9 Sep 2019 20:38:14 -0400 Subject: [PATCH 18/23] Update. --- .../pico/inference/PICOInferenceAnnotatedTypeFactory.java | 6 +++--- .../java/pico/inference/PICOInferenceRealTypeFactory.java | 7 ++----- src/main/java/pico/inference/PICOInferenceVisitor.java | 2 +- src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java | 5 ++--- src/main/java/pico/typecheck/PICOVisitor.java | 2 +- 5 files changed, 9 insertions(+), 13 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index 386a4de..cf79e02 100644 --- a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java @@ -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.PICODefaultTypeAnnotator; import pico.typecheck.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; @@ -69,10 +69,10 @@ public TreeAnnotator createTreeAnnotator() { @Override protected TypeAnnotator createTypeAnnotator() { - // Reuse PICOImplicitsTypeAnnotator even in inference mode. Because the type annotator's implementation + // Reuse PICODefaultTypeAnnotator 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 PICODefaultTypeAnnotator(this)); } @Override diff --git a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index 3c247ea..6d5ea34 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -1,7 +1,5 @@ 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; @@ -11,7 +9,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; @@ -31,7 +28,7 @@ import com.sun.source.tree.Tree; -import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator; +import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultTypeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOTreeAnnotator; import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator; @@ -109,7 +106,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 PICODefaultTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 83dedd6..297a2e8 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -621,7 +621,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { // 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; diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index db6dd28..4eadedd 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -2,7 +2,6 @@ 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; @@ -138,7 +137,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 PICODefaultTypeAnnotator(this)); typeAnnotators.add(new CommitmentTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } @@ -463,7 +462,7 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { public static class PICOImplicitsTypeAnnotator extends ImplicitsTypeAnnotator { - public PICOImplicitsTypeAnnotator(AnnotatedTypeFactory typeFactory) { + public PICODefaultTypeAnnotator(AnnotatedTypeFactory typeFactory) { super(typeFactory); } diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 1e46d0c..8f111bb 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -385,7 +385,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { // 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; From 1c62ec2dabb5f7ac37fd5afc597825ee27bf44e9 Mon Sep 17 00:00:00 2001 From: xingweitian Date: Fri, 6 Sep 2019 21:47:37 -0400 Subject: [PATCH 19/23] Update. --- .../PICOInferenceAnnotatedTypeFactory.java | 4 +-- .../PICOInferenceRealTypeFactory.java | 30 ++++++++-------- .../typecheck/PICOAnnotatedTypeFactory.java | 36 +++++++++---------- src/main/java/pico/typecheck/PICOChecker.java | 2 +- .../java/pico/typecheck/PICOTypeUtil.java | 30 ++++++++-------- src/main/java/qual/Bottom.java | 4 --- src/main/java/qual/Immutable.java | 9 ++--- src/main/java/qual/Readonly.java | 1 - 8 files changed, 56 insertions(+), 60 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index cf79e02..d56c9b5 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; @@ -62,7 +62,7 @@ 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)); } diff --git a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index 6d5ea34..11563fd 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -16,7 +16,7 @@ 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.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator; @@ -81,7 +81,7 @@ protected AbstractViewpointAdapter createViewpointAdapter() { protected TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( new PICOPropagationTreeAnnotator(this), - new ImplicitsTreeAnnotator(this), + new LiteralTreeAnnotator(this), new PICOTreeAnnotator(this)); } @@ -125,19 +125,19 @@ public boolean getShouldDefaultTypeVarLocals() { } // 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 +// 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) { diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index 4eadedd..c84be72 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -33,11 +33,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; @@ -77,7 +77,7 @@ public class PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory PICOStore, PICOTransfer, PICOAnalysis> { public PICOAnnotatedTypeFactory(BaseTypeChecker checker) { - super(checker, true); + super(checker); postInit(); // PICO aliasing is not implemented correctly // remove for now @@ -111,7 +111,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)); } @@ -182,19 +182,19 @@ 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 - } +// @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. @@ -460,7 +460,7 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { } - public static class PICOImplicitsTypeAnnotator extends ImplicitsTypeAnnotator { + public static class PICODefaultTypeAnnotator extends DefaultForTypeAnnotator { public PICODefaultTypeAnnotator(AnnotatedTypeFactory typeFactory) { super(typeFactory); 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 8d32462..a8ac812 100644 --- a/src/main/java/pico/typecheck/PICOTypeUtil.java +++ b/src/main/java/pico/typecheck/PICOTypeUtil.java @@ -13,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; @@ -63,27 +63,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()) { + private static boolean isInTypeKindsOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { + DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + for (TypeKind typeKind : defaultFor.typeKinds()) { if (typeKind.name() == atm.getKind().name()) return true; } return false; } - private static boolean isInTypeNamesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) { + private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { if (atm.getKind().name() != 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; } @@ -91,8 +91,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) + return isInTypeKindsOfDefaultForOfImmutable(atm) + || isInTypesOfDefaultForOfImmutable(atm) || isEnumOrEnumConstant(atm); } diff --git a/src/main/java/qual/Bottom.java b/src/main/java/qual/Bottom.java index cf17cd4..17eab30 100644 --- a/src/main/java/qual/Bottom.java +++ b/src/main/java/qual/Bottom.java @@ -2,21 +2,17 @@ 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 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..f48960a 100644 --- a/src/main/java/qual/Immutable.java +++ b/src/main/java/qual/Immutable.java @@ -1,7 +1,8 @@ package qual; -import org.checkerframework.framework.qual.ImplicitFor; +import org.checkerframework.framework.qual.DefaultFor; import org.checkerframework.framework.qual.LiteralKind; +import org.checkerframework.framework.qual.QualifierForLiterals; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.qual.TypeKind; @@ -14,13 +15,13 @@ import java.math.BigInteger; @SubtypeOf({Readonly.class}) +@QualifierForLiterals({LiteralKind.PRIMITIVE, LiteralKind.STRING}) @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 }) 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; From fd1ccc57ee095756f009d3eb84f3da37331f66e8 Mon Sep 17 00:00:00 2001 From: lnsun Date: Thu, 21 Nov 2019 17:24:21 -0500 Subject: [PATCH 20/23] resolve lnsun cherry commit conflict, related to api update --- .../PICOInferenceAnnotatedTypeFactory.java | 8 +++--- .../PICOInferenceRealTypeFactory.java | 24 +++++------------ .../pico/inference/PICOInferenceVisitor.java | 2 +- .../typecheck/PICOAnnotatedTypeFactory.java | 25 +++++------------- .../java/pico/typecheck/PICOTypeUtil.java | 26 +++++++++---------- src/main/java/qual/Bottom.java | 6 +---- src/main/java/qual/Immutable.java | 4 +-- 7 files changed, 33 insertions(+), 62 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index d56c9b5..5ffdc69 100644 --- a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java @@ -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.PICODefaultTypeAnnotator; +import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator; import pico.typecheck.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; @@ -69,10 +69,10 @@ public TreeAnnotator createTreeAnnotator() { @Override protected TypeAnnotator createTypeAnnotator() { - // Reuse PICODefaultTypeAnnotator 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 PICODefaultTypeAnnotator(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 11563fd..f159883 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -1,5 +1,7 @@ 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; @@ -16,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.LiteralTreeAnnotator; 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; @@ -28,7 +30,8 @@ import com.sun.source.tree.Tree; -import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultTypeAnnotator; +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; @@ -106,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 PICODefaultTypeAnnotator(this)); + typeAnnotators.add(new PICODefaultForTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } @@ -124,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 297a2e8..83c37eb 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -535,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) diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index c84be72..77e5c98 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -2,6 +2,7 @@ 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; @@ -137,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 PICODefaultTypeAnnotator(this)); + typeAnnotators.add(new PICODefaultForTypeAnnotator(this)); typeAnnotators.add(new CommitmentTypeAnnotator(this)); return new ListTypeAnnotator(typeAnnotators); } @@ -182,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. @@ -388,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) { @@ -460,9 +447,9 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) { } - public static class PICODefaultTypeAnnotator extends DefaultForTypeAnnotator { + public static class PICODefaultForTypeAnnotator extends DefaultForTypeAnnotator { - public PICODefaultTypeAnnotator(AnnotatedTypeFactory typeFactory) { + public PICODefaultForTypeAnnotator(AnnotatedTypeFactory typeFactory) { super(typeFactory); } @@ -492,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/PICOTypeUtil.java b/src/main/java/pico/typecheck/PICOTypeUtil.java index a8ac812..994f1d8 100644 --- a/src/main/java/pico/typecheck/PICOTypeUtil.java +++ b/src/main/java/pico/typecheck/PICOTypeUtil.java @@ -63,27 +63,27 @@ public class PICOTypeUtil { sideEffectingUnaryOperators.add(Tree.Kind.PREFIX_DECREMENT); } - private static boolean isInTypeKindsOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { + private static boolean isInTypesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) { DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); assert defaultFor != null; + assert defaultFor.typeKinds() != null; for (TypeKind typeKind : defaultFor.typeKinds()) { - if (typeKind.name() == atm.getKind().name()) return true; + if (typeKind.name().equals(atm.getKind().name())) return true; } return false; } - private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) { - if (atm.getKind().name() != TypeKind.DECLARED.name()) { + private static boolean isInTypeNamesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) { + if (!atm.getKind().name().equals(TypeKind.DECLARED.name())) { return false; } - DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class); - assert defaultFor != null; - Class[] types = defaultFor.types(); + DefaultFor implicitFor = Immutable.class.getAnnotation(DefaultFor.class); + assert implicitFor != null; + assert implicitFor.types() != null; + Class[] typeNames = implicitFor.types(); String fqn = TypesUtils.getQualifiedName((DeclaredType) atm.getUnderlyingType()).toString(); - for (Class type : types) { - if (type.getCanonicalName().contentEquals(fqn)) { - return true; - } + for (int i = 0; i < typeNames.length; i++) { + if (typeNames[i].getCanonicalName().toString().contentEquals(fqn)) return true; } return false; } @@ -91,8 +91,8 @@ private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) /**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 isInTypeKindsOfDefaultForOfImmutable(atm) - || isInTypesOfDefaultForOfImmutable(atm) + return isInTypesOfImplicitForOfImmutable(atm) + || isInTypeNamesOfImplicitForOfImmutable(atm) || isEnumOrEnumConstant(atm); } diff --git a/src/main/java/qual/Bottom.java b/src/main/java/qual/Bottom.java index 17eab30..5306a1b 100644 --- a/src/main/java/qual/Bottom.java +++ b/src/main/java/qual/Bottom.java @@ -1,10 +1,6 @@ package qual; -import org.checkerframework.framework.qual.DefaultFor; -import org.checkerframework.framework.qual.DefaultInUncheckedCodeFor; -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.Retention; diff --git a/src/main/java/qual/Immutable.java b/src/main/java/qual/Immutable.java index f48960a..b5e542b 100644 --- a/src/main/java/qual/Immutable.java +++ b/src/main/java/qual/Immutable.java @@ -1,8 +1,8 @@ package qual; import org.checkerframework.framework.qual.DefaultFor; -import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.QualifierForLiterals; +import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.qual.TypeKind; @@ -15,7 +15,6 @@ import java.math.BigInteger; @SubtypeOf({Readonly.class}) -@QualifierForLiterals({LiteralKind.PRIMITIVE, LiteralKind.STRING}) @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @@ -24,4 +23,5 @@ BigDecimal.class, BigInteger.class}, typeKinds = { TypeKind.INT, TypeKind.BYTE, TypeKind.SHORT, TypeKind.BOOLEAN, TypeKind.LONG, TypeKind.CHAR, TypeKind.FLOAT, TypeKind.DOUBLE }) +@QualifierForLiterals({ LiteralKind.PRIMITIVE, LiteralKind.STRING}) public @interface Immutable {} From a3894e918ae6a702bf13b9c1b513485fcff71f64 Mon Sep 17 00:00:00 2001 From: lnsun Date: Thu, 21 Nov 2019 17:40:09 -0500 Subject: [PATCH 21/23] typo --- src/main/java/pico/inference/PICOInferenceVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 83c37eb..34be4ae 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -553,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)) { From 981f6a4de84c1312ab7e773881495360d1c84126 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Mon, 29 Jul 2019 20:03:08 -0400 Subject: [PATCH 22/23] Implement super constructor call check. Replace the error key "super.constructor.invocation.incompatible" with "super.invocation.invalid". Tweaks test files to pass the test. --- .../pico/inference/PICOInferenceVisitor.java | 2 +- src/main/java/pico/typecheck/PICOVisitor.java | 29 +++++++++++++++++++ .../java/pico/typecheck/messages.properties | 1 - ...ructorInvocationInSubclassConstructor.java | 2 +- testinput/typecheck/AssignableExample.java | 2 +- .../ReceiverTypeOutsideConstructor.java | 18 ++++++------ testinput/typecheck/SuperClass.java | 4 +-- testinput/typecheck/SuperClass2.java | 4 +-- 8 files changed, 45 insertions(+), 17 deletions(-) diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 34be4ae..61bc4a3 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -642,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); diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index 8f111bb..fa4d37d 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,6 +22,7 @@ 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; @@ -493,4 +495,31 @@ protected void checkExtendsImplements(ClassTree classTree) { } } } + + /** + * 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. + * + * @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) { + TreePath path = atypeFactory.getPath(superCall); + MethodTree enclosingMethod = TreeUtils.enclosingMethod(path); + 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); + } + super.checkThisOrSuperConstructorCall(superCall, errorKey); + } } diff --git a/src/main/java/pico/typecheck/messages.properties b/src/main/java/pico/typecheck/messages.properties index 9040ed2..db36cfa 100644 --- a/src/main/java/pico/typecheck/messages.properties +++ b/src/main/java/pico/typecheck/messages.properties @@ -3,7 +3,6 @@ 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 -super.constructor.invocation.incompatible=Subclass constructor: %s is not compatible with super class constructor: %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/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/ReceiverTypeOutsideConstructor.java b/testinput/typecheck/ReceiverTypeOutsideConstructor.java index 62eb1e6..7162e32 100644 --- a/testinput/typecheck/ReceiverTypeOutsideConstructor.java +++ b/testinput/typecheck/ReceiverTypeOutsideConstructor.java @@ -31,13 +31,13 @@ class A { @Immutable class AIMS extends A {} -// :: error: (declaration.inconsistent.with.extends.clause) +// :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) @ReceiverDependantMutable class ARDMS extends A {} -// :: error: (declaration.inconsistent.with.extends.clause) +// :: error: (declaration.inconsistent.with.extends.clause) :: error: (super.invocation.invalid) @Mutable class AMS extends A {} -// :: error: (declaration.inconsistent.with.extends.clause) +// :: 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 @@ -106,13 +106,13 @@ class C { // :: error: (declaration.inconsistent.with.extends.clause) @Immutable class CIMS extends C {} -// :: error: (declaration.inconsistent.with.extends.clause) +// :: 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 d857b7d..c55d9f3 100644 --- a/testinput/typecheck/SuperClass.java +++ b/testinput/typecheck/SuperClass.java @@ -20,7 +20,7 @@ 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)); } @@ -33,7 +33,7 @@ public static void main(String[] args) { @ReceiverDependantMutable class AnotherSubClass extends SuperClass{ @ReceiverDependantMutable AnotherSubClass(){ - // :: error: (super.constructor.invocation.incompatible) + // :: error: (super.invocation.invalid) super(new @Immutable Date(1L)); } 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()); } } From 584d1388a8fdccfe9c31d4dd039d105581b5dca5 Mon Sep 17 00:00:00 2001 From: xingweitian <13183370+xingweitian@users.noreply.github.com> Date: Sun, 18 Aug 2019 22:56:16 -0400 Subject: [PATCH 23/23] Improve code and javadoc. --- src/main/java/pico/typecheck/PICOVisitor.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index fa4d37d..e8478ea 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -498,7 +498,8 @@ protected void checkExtendsImplements(ClassTree classTree) { /** * 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. + * 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" @@ -506,8 +507,7 @@ protected void checkExtendsImplements(ClassTree classTree) { @Override protected void checkThisOrSuperConstructorCall( MethodInvocationTree superCall, @CompilerMessageKey String errorKey) { - TreePath path = atypeFactory.getPath(superCall); - MethodTree enclosingMethod = TreeUtils.enclosingMethod(path); + MethodTree enclosingMethod = visitorState.getMethodTree(); AnnotatedTypeMirror superType = atypeFactory.getAnnotatedType(superCall); AnnotatedExecutableType constructorType = atypeFactory.getAnnotatedType(enclosingMethod); AnnotationMirror superTypeMirror = superType.getAnnotationInHierarchy(READONLY);