Changed the name of the method, enhanced the body, and transferred th…

…e method to NullnessAnnotatedTypeFactory.java to make it local for Nullness-related inference rather than for all checkers. Also added a test case for the corresponding issue in the ainfer-nullness tests.
typetools · Jul 6, 2024 · d7acb57 · d7acb57
1 parent 5b642c3
commit d7acb57
Show file tree

Hide file tree

Showing 6 changed files with 293 additions and 25 deletions.
diff --git a/...ker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/...ker/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,28 +959,37 @@ 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);
     }
   }
 
-  // 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 wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {
+  /**
+   * 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")
-            && !AnnotationUtils.areSameByName(
-                anno,
-                "org.checkerframework.checker.initialization.qual.UnderInitialization(java.lang.Object.class")) {
-          rhsATM.replaceAnnotation(UNDER_INITALIZATION);
+            anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) {
+          rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION);
         }
       }
     }

diff --git a/.../input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava b/.../input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava
@@ -0,0 +1,94 @@
+import org.checkerframework.checker.initialization.qual.*;
+import org.checkerframework.checker.nullness.qual.*;
+
+@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;
+    }
+}
diff --git a/...s/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava b/...s/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava
@@ -0,0 +1,101 @@
+import org.checkerframework.checker.initialization.qual.*;
+import org.checkerframework.checker.nullness.qual.*;
+
+@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;
+    }
+}
diff --git a/checker/tests/ainfer-nullness/non-annotated/Game.java b/checker/tests/ainfer-nullness/non-annotated/Game.java
@@ -0,0 +1,73 @@
+import org.checkerframework.checker.initialization.qual.*;
+import org.checkerframework.checker.nullness.qual.*;
+
+interface Game {
+  void newGame();
+}
+
+class GameImpl implements Game { // package-private
+  private MoveValidator moveValidator;
+
+  public GameImpl(MoveValidator mValidator) {
+    mValidator.setGame(this);
+    moveValidator = mValidator;
+  }
+
+  public GameImpl() {}
+
+  @Override
+  public void newGame() {
+    // Implementation of starting a new game
+  }
+}
+
+interface MoveValidator {
+  void setGame(Game game);
+}
+
+class PlayerDependentMoveValidator implements MoveValidator { // package-private
+  public Game game;
+  private MoveValidator blackMoveValidator = new SimpleMoveValidator();
+
+  @SuppressWarnings({"override.param", "contracts.postcondition"})
+  @Override
+  public void setGame(Game game) {
+    this.game = game;
+  }
+
+  public PlayerDependentMoveValidator() {}
+
+  @SuppressWarnings({"contracts.postcondition", "argument", "method.invocation"})
+  public PlayerDependentMoveValidator(Game game) {
+    this.setGame(game);
+    blackMoveValidator.setGame(game);
+  }
+}
+
+class SimpleMoveValidator implements MoveValidator { // package-private
+  private Game game;
+
+  @SuppressWarnings({"override.param", "contracts.postcondition"})
+  @Override
+  public void setGame(Game game) {
+    this.game = game;
+  }
+
+  public SimpleMoveValidator() {}
+
+  @SuppressWarnings({
+    "purity.not.deterministic.object.creation",
+    "purity" + ".not.sideeffectfree.call",
+    "contracts.postcondition",
+    "return"
+  })
+  public MoveValidator createMoveValidator() {
+    return new PlayerDependentMoveValidator(game);
+  }
+
+  public void test() {
+    PlayerDependentMoveValidator g1 = new PlayerDependentMoveValidator(game);
+    // :: warning: (assignment)
+    this.game = g1.game;
+  }
+}
diff --git a/...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java
@@ -1001,9 +1001,6 @@ protected void updateAnnotationSet(
       return;
     }
 
-    // Update the right-hand side (rhs) annotations if necessary before updating the annotation set
-    atypeFactory.wpiAdjustAnnotationsBeforeUpdate(rhsATM);
-
     AnnotatedTypeMirror atmFromStorage =
         storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);
     updateAtmWithLub(rhsATM, atmFromStorage);

diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -5523,15 +5523,6 @@ 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 wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {}
-
   /**
    * Side-effects the method or constructor annotations to make any desired changes before writing
    * to an annotation file.