WPI: decision on whether to infer a type for a type variable should b…

…e made based on explicit annotations (#5618) --------- Co-authored-by: Suzanne Millstein <[email protected]> Co-authored-by: Michael Ernst <[email protected]>
typetools · Mar 1, 2023 · e84e29e · e84e29e
1 parent eebbbf0
commit e84e29e
Show file tree

Hide file tree

Showing 6 changed files with 39 additions and 4 deletions.
diff --git a/checker/build.gradle b/checker/build.gradle
@@ -825,6 +825,7 @@ task ainferNullnessGenerateJaifs(type: Test) {
 
     // JAIF-based WPI does not infer annotations on uses of type variables correctly.
     delete('tests/ainfer-nullness/annotated/TwoCtorGenericAbstract.java')
+    delete('tests/ainfer-nullness/annotated/TypeVarReturnAnnotated.java')
 
     // Inserting annotations from .jaif files in-place.
     String jaifsDir = 'tests/ainfer-nullness/inference-output';

diff --git a/...t/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java b/...t/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java
@@ -28,7 +28,7 @@ public AinferNullnessAjavaTest(List<File> testFiles) {
         NullnessChecker.class,
         "ainfer-nullness/non-annotated",
         "-Ainfer=ajava",
-        // "-Aajava=tests/ainfer-nullness/input-annotation-files/",
+        "-Aajava=tests/ainfer-nullness/input-annotation-files/",
         "-Awarns");
   }
 

diff --git a/...t/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessJaifsTest.java b/...t/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessJaifsTest.java
@@ -20,7 +20,13 @@ public class AinferNullnessJaifsTest extends CheckerFrameworkPerDirectoryTest {
    * @param testFiles the files containing test code, which will be type-checked
    */
   public AinferNullnessJaifsTest(List<File> testFiles) {
-    super(testFiles, NullnessChecker.class, "nullness", "-Ainfer=jaifs", "-Awarns");
+    super(
+        testFiles,
+        NullnessChecker.class,
+        "nullness",
+        "-Ainfer=jaifs",
+        "-Awarns",
+        "-Aajava=tests/ainfer-nullness/input-annotation-files/");
   }
 
   @Parameters

diff --git a/...-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava b/...-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava
@@ -0,0 +1,10 @@
+// Code like this caused WPI to loop infinitely, because the annotation on the return type
+// was only sometimes inferred. Based on an example from
+// https://github.com/dd482IT/cache2k-wpi/blob/0eaa156bdecd617b2aa4c745d0f8844a32609697/cache2k-api/src/main/java/org/cache2k/config/ToggleFeature.java#L73
+@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
+public class TypeVarReturnAnnotated {
+
+    public static <T extends TypeVarReturnAnnotated> @org.checkerframework.checker.initialization.qual.FBCBottom @org.checkerframework.checker.nullness.qual.Nullable T extract() {
+        return null;
+    }
+}
diff --git a/checker/tests/ainfer-nullness/non-annotated/TypeVarReturnAnnotated.java b/checker/tests/ainfer-nullness/non-annotated/TypeVarReturnAnnotated.java
@@ -0,0 +1,9 @@
+// Code like this caused WPI to loop infinitely, because the annotation on the return type
+// was only sometimes inferred. Based on an example from
+// https://github.com/dd482IT/cache2k-wpi/blob/0eaa156bdecd617b2aa4c745d0f8844a32609697/cache2k-api/src/main/java/org/cache2k/config/ToggleFeature.java#L73
+
+public class TypeVarReturnAnnotated {
+  public static <T extends TypeVarReturnAnnotated> T extract() {
+    return null;
+  }
+}
diff --git a/...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java
@@ -857,10 +857,19 @@ protected void updateAnnotationSet(
 
     // For type variables, infer primary annotations for field type use locations, but
     // for other locations only infer primary annotations if they are a super type of the upper
-    // bound.
+    // bound of declaration of the type variable.
     if (defLoc != TypeUseLocation.FIELD && lhsATM instanceof AnnotatedTypeVariable) {
+      AnnotatedTypeVariable lhsTV = (AnnotatedTypeVariable) lhsATM;
       AnnotationMirrorSet upperAnnos =
-          ((AnnotatedTypeVariable) lhsATM).getUpperBound().getEffectiveAnnotations();
+          new AnnotationMirrorSet(lhsTV.getUpperBound().getEffectiveAnnotations());
+      // If the type variable has a primary annotation then it is copied to the upper bound of the
+      // use of the type variable, so remove any annotations that are the same as a primary
+      // annotations.
+      // TODO: this is kind of a hack.  It would be better to look up the type variable declaration
+      // to find the upper bound when there are primary annotations.
+      for (AnnotationMirror primary : lhsTV.getAnnotations()) {
+        upperAnnos.remove(primary);
+      }
       // If the inferred type is a subtype of the upper bounds of the
       // current type in the source code, do nothing.
       if (upperAnnos.size() == rhsATM.getAnnotations().size()