diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java index 9cb5828fe09..4dc7de9ac21 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java @@ -14,6 +14,9 @@ import com.sun.source.util.TreePath; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; +import org.checkerframework.checker.initialization.qual.Initialized; +import org.checkerframework.checker.initialization.qual.UnderInitialization; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.checkerframework.checker.nullness.NullnessChecker; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; @@ -28,6 +31,8 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; +import org.plumelib.util.ArraysPlume; import java.lang.annotation.Annotation; import java.util.ArrayList; @@ -39,6 +44,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeMirror; /* NO-AFU import org.checkerframework.common.wholeprograminference.WholeProgramInference; @@ -290,6 +296,163 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { return null; } + @Override + protected void reportCommonAssignmentError( + AnnotatedTypeMirror varType, + AnnotatedTypeMirror valueType, + Tree valueTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + FoundRequired pair = FoundRequired.of(valueType, varType); + String valueTypeString = pair.found; + String varTypeString = pair.required; + + // If the stored value of valueTree is wrong, we still do not report an error + // if all necessary fields of valueTree are initialized in the store before the assignment. + + InitializationStore initStoreBefore = atypeFactory.getStoreBefore(commonAssignmentTree); + + // We can't check if all necessary fields are initialized without a store. + if (initStoreBefore == null) { + super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs); + return; + } + + // We only track field initialization for the current receiver. + if (!valueTree.toString().equals("this")) { + super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs); + return; + } + + // If the required type is @Initialized and the value type is not final, + // we always need to report an error. + if (varType.getAnnotation(Initialized.class) != null + && !ElementUtils.isFinal( + TypesUtils.getTypeElement(valueType.getUnderlyingType()))) { + super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs); + return; + } + + // Otherwise, we check if there are any uninitialized fields and only report the error + // if this is the case. + GenericAnnotatedTypeFactory targetFactory = + checker.getTypeFactoryOfSubcheckerOrNull( + ((InitializationChecker) checker).getTargetCheckerClass()); + List uninitializedFields = + atypeFactory.getUninitializedFields( + initStoreBefore, + targetFactory.getStoreBefore(commonAssignmentTree), + getCurrentPath(), + false, + Collections.emptyList()); + uninitializedFields.removeAll(initializedFields); + + if (!uninitializedFields.isEmpty()) { + StringJoiner fieldsString = new StringJoiner(", "); + for (VariableTree f : uninitializedFields) { + fieldsString.add(f.getName()); + } + checker.reportError( + commonAssignmentTree, + errorKey, + ArraysPlume.concatenate(extraArgs, valueTypeString, varTypeString)); + } + } + + @Override + protected void reportMethodInvocabilityError( + MethodInvocationTree node, AnnotatedTypeMirror found, AnnotatedTypeMirror expected) { + // We only track field initialization for the current receiver. + if (!TreeUtils.isSelfAccess(node)) { + super.reportMethodInvocabilityError(node, found, expected); + return; + } + + GenericAnnotatedTypeFactory targetFactory = + checker.getTypeFactoryOfSubcheckerOrNull( + ((InitializationChecker) checker).getTargetCheckerClass()); + List uninitializedFields = + atypeFactory.getUninitializedFields( + atypeFactory.getStoreBefore(node), + targetFactory.getStoreBefore(node), + getCurrentPath(), + false, + Collections.emptyList()); + uninitializedFields.removeAll(initializedFields); + + AnnotationMirror init = expected.getAnnotation(Initialized.class); + AnnotationMirror unknownInit = expected.getAnnotation(UnknownInitialization.class); + AnnotationMirror underInit = expected.getAnnotation(UnderInitialization.class); + + // If the actual receiver type (found) is not a subtype of expected, + // we still do not report an error if all necessary fields are initialized in the store + // before the method call. + + // Find the frame for which the receiver must be initialized to discharge this error: + // * If the expected type is @UnknownInitialization(A) or @UnderInitialization(A), the frame + // is A. + // * If the expected type is @Initialized and the receiver type is final, the frame + // is the receiver type. + // * Otherwise, this error cannot be discharged and is reported by the super method. + TypeMirror frame; + if (unknownInit != null) { + frame = atypeFactory.getTypeFrameFromAnnotation(unknownInit); + } else if (underInit != null) { + frame = atypeFactory.getTypeFrameFromAnnotation(underInit); + } else if (init != null + && ElementUtils.isFinal(TypesUtils.getTypeElement(expected.getUnderlyingType()))) { + frame = expected.getUnderlyingType(); + } else { + if (!uninitializedFields.isEmpty()) { + reportMethodInvocabilityErrorWithUninitializedFields( + node, found, expected, uninitializedFields); + } else { + super.reportMethodInvocabilityError(node, found, expected); + } + return; + } + + TypeMirror underlyingReceiverType = atypeFactory.getReceiverType(node).getUnderlyingType(); + if (!atypeFactory + .getProcessingEnv() + .getTypeUtils() + .isSubtype(frame, underlyingReceiverType)) { + super.reportMethodInvocabilityError(node, found, expected); + return; + } + + if (!uninitializedFields.isEmpty()) { + reportMethodInvocabilityErrorWithUninitializedFields( + node, found, expected, uninitializedFields); + } + } + + /** + * Report a method invocability error with uninitialized fields. + * + * @param node the AST node at which to report the error + * @param found the actual type of the receiver + * @param expected the expected type of the receiver + * @param uninitializedFields the list of uninitialized fields + */ + private void reportMethodInvocabilityErrorWithUninitializedFields( + MethodInvocationTree node, + AnnotatedTypeMirror found, + AnnotatedTypeMirror expected, + List uninitializedFields) { + StringJoiner fieldsString = new StringJoiner(", "); + for (VariableTree f : uninitializedFields) { + fieldsString.add(f.getName()); + } + checker.reportError( + node, + "initialization.method.invocation.invalid", + TreeUtils.elementFromUse(node), + fieldsString.toString(), + found.toString(), + expected.toString()); + } + /** * Returns the full list of annotations on the receiver. * diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/messages.properties b/checker/src/main/java/org/checkerframework/checker/initialization/messages.properties index 89a7cd980de..d093aca68c1 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/initialization/messages.properties @@ -6,3 +6,4 @@ initialization.invalid.field.type=initialization annotations are not allowed on initialization.field.uninitialized=the default constructor does not initialize field %s initialization.fields.uninitialized=the constructor does not initialize fields: %s initialization.static.field.uninitialized=static field %s not initialized +initialization.method.invocation.invalid= call to %s not allowed on the given receiver uninitialized fields in this class: %s. %nfound : %s%nrequired: %s diff --git a/checker/tests/initialization/Issue1120.java b/checker/tests/initialization/Issue1120.java index 3cb2358100c..78dd820de8c 100644 --- a/checker/tests/initialization/Issue1120.java +++ b/checker/tests/initialization/Issue1120.java @@ -22,7 +22,7 @@ final class Issue1120Sub extends Issue1120Super { Issue1120Sub(int i) { // this is @UnderInitialization(A.class) this.party(); - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) this.bar(); g = new Object(); } diff --git a/checker/tests/initialization/Issue905.java b/checker/tests/initialization/Issue905.java index dda7b6e8d0a..6cb523e2468 100644 --- a/checker/tests/initialization/Issue905.java +++ b/checker/tests/initialization/Issue905.java @@ -8,7 +8,7 @@ public class Issue905 { Issue905() { // this should be @UnderInitialization(Object.class), so this call should be forbidden. - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) baz(); mBar = ""; } diff --git a/checker/tests/initialization/RawMethodInvocation.java b/checker/tests/initialization/RawMethodInvocation.java index 8aa9117238d..a114daf881d 100644 --- a/checker/tests/initialization/RawMethodInvocation.java +++ b/checker/tests/initialization/RawMethodInvocation.java @@ -40,7 +40,7 @@ void init_ab(@UnknownInitialization RawMethodInvocation this) { RawMethodInvocation(long constructor_escapes_raw) { a = ""; - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) nonRawMethod(); b = ""; } diff --git a/checker/tests/initialization/RawTypesInit.java b/checker/tests/initialization/RawTypesInit.java index ec828c2c8d1..89c9056be5e 100644 --- a/checker/tests/initialization/RawTypesInit.java +++ b/checker/tests/initialization/RawTypesInit.java @@ -11,9 +11,9 @@ class Bad { @NonNull String field; public Bad() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) this.init(); // error - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) init(); // error this.field = "field"; // valid @@ -163,7 +163,7 @@ class AllFieldsSetInInitializer { public AllFieldsSetInInitializer() { elapsedMillis = 0; - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) nonRawMethod(); // error startTime = 0; // :: error: (method.invocation.invalid) @@ -174,7 +174,7 @@ public AllFieldsSetInInitializer() { // :: error: (initialization.fields.uninitialized) public AllFieldsSetInInitializer(boolean b) { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) nonRawMethod(); // error } diff --git a/checker/tests/initialization/TypeFrames2.java b/checker/tests/initialization/TypeFrames2.java index 0b328a56614..846dd790797 100644 --- a/checker/tests/initialization/TypeFrames2.java +++ b/checker/tests/initialization/TypeFrames2.java @@ -7,7 +7,7 @@ class A { @NonNull String a; public A() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) this.foo(); a = ""; this.foo(); @@ -22,7 +22,7 @@ class B extends A { public B() { super(); this.foo(); - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) this.bar(); b = ""; this.bar(); diff --git a/checker/tests/initialization/TypeFrames3.java b/checker/tests/initialization/TypeFrames3.java index 1a411dd4af4..f0a4fcb5381 100644 --- a/checker/tests/initialization/TypeFrames3.java +++ b/checker/tests/initialization/TypeFrames3.java @@ -10,7 +10,7 @@ public TypeFrames3(boolean dummy) { } public TypeFrames3(int dummy) { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) foo(); f = new Object(); } diff --git a/checker/tests/nullness-initialization/FieldInit.java b/checker/tests/nullness-initialization/FieldInit.java index eb1ec8d773d..73413fb9116 100644 --- a/checker/tests/nullness-initialization/FieldInit.java +++ b/checker/tests/nullness-initialization/FieldInit.java @@ -1,5 +1,5 @@ public class FieldInit { - // :: error: (argument.type.incompatible) :: error: (method.invocation.invalid) + // :: error: (argument.type.incompatible) :: error: (initialization.method.invocation.invalid) String f = init(this); String init(FieldInit o) { diff --git a/checker/tests/nullness-initialization/FlowConstructor.java b/checker/tests/nullness-initialization/FlowConstructor.java index dbaea5c0fef..7e98b77e1bd 100644 --- a/checker/tests/nullness-initialization/FlowConstructor.java +++ b/checker/tests/nullness-initialization/FlowConstructor.java @@ -21,7 +21,7 @@ public FlowConstructor(int p) { public FlowConstructor(double p) { a = "m"; - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) nonRawMethod(); // error b = "n"; } diff --git a/checker/tests/nullness-initialization/Issue1590a.java b/checker/tests/nullness-initialization/Issue1590a.java index f4de70f5f5a..a0471e43e88 100644 --- a/checker/tests/nullness-initialization/Issue1590a.java +++ b/checker/tests/nullness-initialization/Issue1590a.java @@ -6,7 +6,7 @@ public class Issue1590a { // :: error: (initialization.fields.uninitialized) public Issue1590a() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) init(); } diff --git a/checker/tests/nullness-initialization/MethodInvocation.java b/checker/tests/nullness-initialization/MethodInvocation.java index 5625f95e9ca..adc30fcd1e5 100644 --- a/checker/tests/nullness-initialization/MethodInvocation.java +++ b/checker/tests/nullness-initialization/MethodInvocation.java @@ -6,7 +6,7 @@ public class MethodInvocation { String s; public MethodInvocation() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) a(); b(); c(); @@ -14,7 +14,7 @@ public MethodInvocation() { } public MethodInvocation(boolean p) { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) a(); // still not okay to be initialized s = "abc"; } diff --git a/checker/tests/nullness-initialization/RawTypesBounded.java b/checker/tests/nullness-initialization/RawTypesBounded.java index 1edb3c1f12e..8ba68c7ceea 100644 --- a/checker/tests/nullness-initialization/RawTypesBounded.java +++ b/checker/tests/nullness-initialization/RawTypesBounded.java @@ -10,9 +10,9 @@ class Bad { @NonNull String field; public Bad() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) this.init(); // error - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) init(); // error this.field = "field"; // valid diff --git a/checker/tests/nullness-initialization/Simple2.java b/checker/tests/nullness-initialization/Simple2.java index dbeb07b9b0e..e46e1dabfd4 100644 --- a/checker/tests/nullness-initialization/Simple2.java +++ b/checker/tests/nullness-initialization/Simple2.java @@ -5,7 +5,7 @@ public class Simple2 { @NonNull String f; public Simple2() { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) test(); f = "abc"; diff --git a/checker/tests/nullness-initialization/java8/lambda/ReceiversLambda.java b/checker/tests/nullness-initialization/java8/lambda/ReceiversLambda.java index 5f43e8df2d1..9df24462abe 100644 --- a/checker/tests/nullness-initialization/java8/lambda/ReceiversLambda.java +++ b/checker/tests/nullness-initialization/java8/lambda/ReceiversLambda.java @@ -13,9 +13,9 @@ interface FunctionRT { class ReceiverTest { - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) FunctionRT f1 = s -> this.toString(); - // :: error: (method.invocation.invalid) + // :: error: (initialization.method.invocation.invalid) FunctionRT f2 = s -> super.toString(); // :: error: (nullness.on.receiver)