Add report errors with uninitialized-fields message

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<VariableTree> 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<VariableTree> 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<VariableTree> 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.
      *

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

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();
     }

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 = "";
     }

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 = "";
     }

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
         }
 

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();

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();
     }

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) {

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";
     }

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();
     }
 

checker/tests/nullness-initialization/MethodInvocation.java

@@ -6,15 +6,15 @@ public class MethodInvocation {
     String s;
 
     public MethodInvocation() {
-        // :: error: (method.invocation.invalid)
+        // :: error: (initialization.method.invocation.invalid)
         a();
         b();
         c();
         s = "abc";
     }
 
     public MethodInvocation(boolean p) {
-        // :: error: (method.invocation.invalid)
+        // :: error: (initialization.method.invocation.invalid)
         a(); // still not okay to be initialized
         s = "abc";
     }

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

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";

checker/tests/nullness-initialization/java8/lambda/ReceiversLambda.java

@@ -13,9 +13,9 @@ interface FunctionRT<T extends @Nullable Object, R> {
 
 class ReceiverTest {
 
-    // :: error: (method.invocation.invalid)
+    // :: error: (initialization.method.invocation.invalid)
     FunctionRT<String, String> f1 = s -> this.toString();
-    // :: error: (method.invocation.invalid)
+    // :: error: (initialization.method.invocation.invalid)
     FunctionRT<String, String> f2 = s -> super.toString();
 
     // :: error: (nullness.on.receiver)