Fix WPI Non-Termination Issue with @UnknownInitialization Annotations

checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java

@@ -961,6 +961,30 @@ public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) {
     }
   }
 
+  // For all assignments, If rhsmATM is Nullable or MonotonicNonNull and has
+  // the UnknownInitialization annotation, and if the annotation is not
+  // UnknownInitialization(java.lang.Object.class), replace it with
+  // UnknownInitialization(java.lang.Object.class). This is because there is
+  // likely a constructor where it hasn't been initialized, and we haven't
+  // considered its effect. Otherwise, WPI might get stuck in a loop.
+  @Override
+  public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {
+    if ((rhsATM.hasPrimaryAnnotation(Nullable.class)
+        || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) {
+      for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
+        if (AnnotationUtils.areSameByName(
+                anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization")
+            && !anno.getAnnotationType()
+                .toString()
+                .equals(
+                    "@org"
+                        + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) {
+          rhsATM.replaceAnnotation(UNDER_INITALIZATION);
+        }
+      }
+    }
+  }
+
   @Override
   public boolean wpiShouldInferTypesForReceivers() {
     // All receivers must be non-null, or the dereference involved in

docs/manual/contributors.tex

@@ -36,6 +36,7 @@
 Di Wang,
 Dilraj Singh,
 Dmitriy Shepelev,
+Erfan Arvan,
 Eric Spishak,
 Ethan Koenig,
 Farzan Mirshekari,

framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java

@@ -1001,6 +1001,10 @@ protected void updateAnnotationSet(
       return;
     }
 
+    // Update Initialization Annotations in WPI. It is only applied to
+    // Nullness-related qualifiers' inference to prevent possible loops.
+    atypeFactory.wpiAdjustForInitializationAnnotations(rhsATM);
+
     AnnotatedTypeMirror atmFromStorage =
         storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);
     updateAtmWithLub(rhsATM, atmFromStorage);

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -5523,6 +5523,15 @@ public boolean wpiShouldInferTypesForReceivers() {
     return true;
   }
 
+  /**
+   * Changes the type of {@code rhsATM} when being assigned to anything, for use by whole-program
+   * inference. The default implementation does nothing.
+   *
+   * @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this
+   *     method
+   */
+  public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {}
+
   /**
    * Side-effects the method or constructor annotations to make any desired changes before writing
    * to an annotation file.