Fix WPI Non-Termination Issue with @UnknownInitialization Annotations

checker-qual-android/build.gradle

@@ -19,7 +19,19 @@ task copySources(type: Copy) {
 
   into file(layout.buildDirectory.dir("generated/sources/main/java"))
 
-  fileMode(0555)
+  filePermissions {
+    user {
+      read = true
+      write = true
+      execute = true
+    }
+    group {
+      read = true
+      write = true
+      execute = true
+    }
+    other.read = true
+  }
 }
 
 sourceSets {

checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java

@@ -34,7 +34,7 @@
  * @checker_framework.manual #defaults Default qualifier for unannotated types
  */
 @Documented
-@Retention(RetentionPolicy.SOURCE)
+@Retention(RetentionPolicy.RUNTIME)
 @Target({
   ElementType.PACKAGE,
   ElementType.TYPE,

checker/build.gradle

@@ -813,6 +813,9 @@ task ainferNullnessGenerateJaifs(type: Test) {
     delete('tests/ainfer-nullness/annotated/TwoCtorGenericAbstract.java')
     delete('tests/ainfer-nullness/annotated/TypeVarReturnAnnotated.java')
 
+    //This test shouldn't be expected to work without the input .ajava file.
+    delete('tests/ainfer-nullness/annotated/WPIUnknownInitializationLoopTest.java')
+
     // Inserting annotations from .jaif files in-place.
     String jaifsDir = 'tests/ainfer-nullness/inference-output';
     List<File> jaifs = fileTree(jaifsDir).matching {
@@ -1079,4 +1082,3 @@ publishing {
 signing {
   sign publishing.publications.checker
 }
-

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

@@ -50,6 +50,7 @@
 import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.dataflow.util.NodeUtils;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
+import org.checkerframework.framework.qual.TypeUseLocation;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFormatter;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -938,6 +939,8 @@ public boolean isImmutable(TypeMirror type) {
   @Override
   public void wpiAdjustForUpdateField(
       Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) {
+    // Adjust initialization annotations first
+    wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.FIELD);
     // Synthetic variable names contain "#". Ignore them.
     if (!rhsATM.hasPrimaryAnnotation(Nullable.class) || fieldName.contains("#")) {
       return;
@@ -956,11 +959,42 @@ public void wpiAdjustForUpdateField(
   // then change rhs to @Nullable
   @Override
   public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) {
+    // Adjust initialization annotations first
+    wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.OTHERWISE);
     if (rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class)) {
       rhsATM.replaceAnnotation(NULLABLE);
     }
   }
 
+  /**
+   * Changes the type of {@code rhsATM} when assigned to any pseudo-assignment, for use by
+   * whole-program inference.
+   *
+   * <p>If {@code rhsATM} is Nullable or MonotonicNonNull and has the UnknownInitialization
+   * annotation, replace it with {@code UnknownInitialization(java.lang.Object.class)}. This ensures
+   * that if there is a constructor where the type hasn't been initialized, its effect is
+   * considered. Otherwise, whole-program inference might get stuck in a loop.
+   *
+   * @param rhsATM the type of the right-hand side of the pseudo-assignment, which is side-effected
+   *     by this method
+   * @param defLoc the location where the annotation will be added. It is either a FIELD or a
+   *     non-field (OTHERWISE).
+   */
+  public void wpiAdjustInitializationAnnotations(
+      AnnotatedTypeMirror rhsATM, TypeUseLocation defLoc) {
+    // defLoc is defined to be used in the future if needed to differentiate between field and
+    // non-field locations
+    if ((rhsATM.hasPrimaryAnnotation(Nullable.class)
+        || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) {
+      for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
+        if (AnnotationUtils.areSameByName(
+            anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) {
+          rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION);
+        }
+      }
+    }
+  }
+
   @Override
   public boolean wpiShouldInferTypesForReceivers() {
     // All receivers must be non-null, or the dereference involved in

checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java

@@ -22,13 +22,15 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.TreeUtils;
 
 /** The transfer function for the Optional Checker. */
 public class OptionalTransfer extends CFTransfer {
 
+  /** The {@link OptionalAnnotatedTypeFactory} instance for this transfer class. */
+  private final OptionalAnnotatedTypeFactory optionalTypeFactory;
+
   /** The @{@link Present} annotation. */
   private final AnnotationMirror PRESENT;
 
@@ -38,20 +40,17 @@ public class OptionalTransfer extends CFTransfer {
   /** The element for java.util.Optional.ifPresentOrElse(), or null. */
   private final @Nullable ExecutableElement optionalIfPresentOrElse;
 
-  /** The type factory associated with this transfer function. */
-  private final AnnotatedTypeFactory atypeFactory;
-
   /**
    * Create an OptionalTransfer.
    *
    * @param analysis the Optional Checker instance
    */
   public OptionalTransfer(CFAbstractAnalysis<CFValue, CFStore, CFTransfer> analysis) {
     super(analysis);
-    atypeFactory = analysis.getTypeFactory();
-    Elements elements = atypeFactory.getElementUtils();
+    optionalTypeFactory = (OptionalAnnotatedTypeFactory) analysis.getTypeFactory();
+    Elements elements = optionalTypeFactory.getElementUtils();
     PRESENT = AnnotationBuilder.fromClass(elements, Present.class);
-    ProcessingEnvironment env = atypeFactory.getProcessingEnv();
+    ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv();
     optionalIfPresent = TreeUtils.getMethod("java.util.Optional", "ifPresent", 1, env);
     optionalIfPresentOrElse =
         TreeUtils.getMethodOrNull("java.util.Optional", "ifPresentOrElse", 2, env);
@@ -70,7 +69,7 @@ public CFStore initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode>
       LambdaExpressionTree lambdaTree = cfgLambda.getLambdaTree();
       List<? extends VariableTree> lambdaParams = lambdaTree.getParameters();
       if (lambdaParams.size() == 1) {
-        TreePath lambdaPath = atypeFactory.getPath(lambdaTree);
+        TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree);
         Tree lambdaParent = lambdaPath.getParentPath().getLeaf();
         if (lambdaParent.getKind() == Tree.Kind.METHOD_INVOCATION) {
           MethodInvocationTree invok = (MethodInvocationTree) lambdaParent;

checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava

@@ -0,0 +1,91 @@
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
+interface Game {
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    void newGame();
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
+class // package-private
+GameImpl implements // package-private
+Game {
+
+    private  MoveValidator moveValidator;
+
+    @org.checkerframework.dataflow.qual.Impure
+    public GameImpl(MoveValidator mValidator) {
+        mValidator.setGame(this);
+        moveValidator = mValidator;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public GameImpl() {
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public void newGame( // package-private
+    GameImpl this) {
+        // Implementation of starting a new game
+    }
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
+interface MoveValidator {
+
+    @org.checkerframework.dataflow.qual.Impure
+    void setGame( MoveValidator this,  Game game);
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
+class // package-private
+PlayerDependentMoveValidator implements // package-private
+MoveValidator {
+
+    private  Game game;
+
+    private  MoveValidator blackMoveValidator = new SimpleMoveValidator();
+
+    @org.checkerframework.dataflow.qual.Impure
+    public void setGame( // package-private
+    PlayerDependentMoveValidator this,  Game game) {
+        this.game = game;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public PlayerDependentMoveValidator() {
+    }
+
+    @org.checkerframework.dataflow.qual.Impure
+    public PlayerDependentMoveValidator( Game game) {
+        this.setGame(game);
+        blackMoveValidator.setGame(game);
+    }
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
+class // package-private
+SimpleMoveValidator implements // package-private
+MoveValidator {
+
+    private  Game game;
+
+    @org.checkerframework.dataflow.qual.Impure
+    public void setGame( // package-private
+    SimpleMoveValidator this,  Game game) {
+        this.game = game;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public SimpleMoveValidator() {
+    }
+
+    @org.checkerframework.dataflow.qual.Pure
+    public  MoveValidator createMoveValidator() {
+        return new PlayerDependentMoveValidator(game);
+    }
+        public void test(){
+        PlayerDependentMoveValidator g1 =
+                new PlayerDependentMoveValidator(game);
+        this.game = g1.game;
+    }
+}

checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava

@@ -0,0 +1,98 @@
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+interface Game {
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    void newGame();
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+class // package-private
+GameImpl implements // package-private
+Game {
+
+    private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.MonotonicNonNull MoveValidator moveValidator;
+
+    @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.moveValidator" })
+    @org.checkerframework.dataflow.qual.Impure
+    public GameImpl(MoveValidator mValidator) {
+        mValidator.setGame(this);
+        moveValidator = mValidator;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public GameImpl() {
+    }
+
+    @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.moveValidator" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class)
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public void newGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
+    GameImpl this) {
+        // Implementation of starting a new game
+    }
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+interface MoveValidator {
+
+    @org.checkerframework.dataflow.qual.Impure
+    void setGame(@org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game);
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+class // package-private
+PlayerDependentMoveValidator implements // package-private
+MoveValidator {
+
+    private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game;
+
+    private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull MoveValidator blackMoveValidator = new SimpleMoveValidator();
+
+    @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.game" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class)
+    @org.checkerframework.dataflow.qual.Impure
+    public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
+    PlayerDependentMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) {
+        this.game = game;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public PlayerDependentMoveValidator() {
+    }
+
+    @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "#1" })
+    @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
+    @org.checkerframework.dataflow.qual.Impure
+    public PlayerDependentMoveValidator(@org.checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) {
+        this.setGame(game);
+        blackMoveValidator.setGame(game);
+    }
+}
+
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+class // package-private
+SimpleMoveValidator implements // package-private
+MoveValidator {
+
+    private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.MonotonicNonNull Game game;
+
+    @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
+    @org.checkerframework.dataflow.qual.Impure
+    public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
+    SimpleMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.NonNull Game game) {
+        this.game = game;
+    }
+
+    @org.checkerframework.dataflow.qual.SideEffectFree
+    public SimpleMoveValidator() {
+    }
+
+    @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
+    @org.checkerframework.dataflow.qual.Pure
+    public @org.checkerframework.checker.initialization.qual.UnderInitialization(PlayerDependentMoveValidator.class) @org.checkerframework.checker.nullness.qual.NonNull MoveValidator createMoveValidator() {
+        return new PlayerDependentMoveValidator(game);
+    }
+        public void test(){
+        PlayerDependentMoveValidator g1 =
+                new PlayerDependentMoveValidator(game);
+        this.game = g1.game;
+    }
+}