Fix crash in ajava-based WPI related to captures

checker/build.gradle

@@ -706,6 +706,52 @@ task ainferIndexAjavaTest(dependsOn: 'shadowJar', group: 'Verification') {
     outputs.upToDateWhen { false }
 }
 
+task ainferNullnessGenerateAjava(type: Test) {
+    description 'Internal task.  Users should run ainferNullnessAjavaTest instead.  This type-checks the ainfer-nullness files with -Ainfer=ajava to generate ajava files.'
+
+    dependsOn(compileTestJava)
+    doFirst {
+        delete("tests/ainfer-nullness/annotated")
+        delete("${buildDir}/ainfer-nullness/")
+    }
+    outputs.upToDateWhen { false }
+    include '**/AinferNullnessAjavaTest.class'
+    testLogging {
+        // Always run the tests
+        outputs.upToDateWhen { false }
+
+        // Show the found unexpected diagnostics and the expected diagnostics not found.
+        exceptionFormat "full"
+        events "passed", "skipped", "failed"
+    }
+
+    doLast {
+        copyNonannotatedToAnnotatedDirectory("ainfer-nullness")
+    }
+}
+
+task ainferNullnessValidateAjava(type: Test) {
+    description 'Internal task.  Users should run ainferNullnessAjavaTest instead.  This re-type-checks the ainfer-nullness files using the ajava files generated by ainferNullnessGenerateAjava'
+
+    dependsOn(ainferNullnessGenerateAjava)
+    outputs.upToDateWhen { false }
+    include '**/AinferNullnessAjavaValidationTest.class'
+    testLogging {
+        // Always run the tests
+        outputs.upToDateWhen { false }
+
+        // Show the found unexpected diagnostics and the expected diagnostics not found.
+        exceptionFormat "full"
+        events "passed", "skipped", "failed"
+    }
+}
+
+task ainferNullnessAjavaTest(dependsOn: 'shadowJar', group: 'Verification') {
+    description 'Run tests for whole-program inference using ajava files and the Nullness Checker'
+    dependsOn(ainferNullnessValidateAjava)
+    outputs.upToDateWhen { false }
+}
+
 task ainferNullnessGenerateJaifs(type: Test) {
     description 'Internal task.  Users should run ainferNullnessJaifTest instead.  This type-checks the ainfer-nullness files with -Ainfer=jaifs to generate .jaif files'
 

checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java

@@ -0,0 +1,40 @@
+package org.checkerframework.checker.test.junit.ainferrunners;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.nullness.NullnessChecker;
+import org.checkerframework.framework.test.AinferGeneratePerDirectoryTest;
+import org.junit.experimental.categories.Category;
+import org.junit.runners.Parameterized.Parameters;
+
+/**
+ * Tests whole-program inference with the aid of ajava files. This test is the first pass on the
+ * test data, which generates the ajava files. This specific test suite is designed to elicit
+ * problems with ajava parsing that only occur when the Nullness Checker is run.
+ *
+ * <p>IMPORTANT: The errors captured in the tests located in tests/ainfer-index/ are not relevant.
+ * The meaning of this test class is to test if the generated ajava files are similar to the
+ * expected ones. The errors on .java files must be ignored.
+ */
+@Category(AinferNullnessAjavaTest.class)
+public class AinferNullnessAjavaTest extends AinferGeneratePerDirectoryTest {
+
+  /**
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public AinferNullnessAjavaTest(List<File> testFiles) {
+    super(
+        testFiles,
+        NullnessChecker.class,
+        "ainfer-nullness/non-annotated",
+        "-Anomsgtext",
+        "-Ainfer=ajava",
+        // "-Aajava=tests/ainfer-nullness/input-annotation-files/",
+        "-Awarns");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"ainfer-nullness/non-annotated"};
+  }
+}

checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaValidationTest.java

@@ -0,0 +1,37 @@
+package org.checkerframework.checker.test.junit.ainferrunners;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.nullness.NullnessChecker;
+import org.checkerframework.framework.test.AinferValidatePerDirectoryTest;
+import org.junit.experimental.categories.Category;
+import org.junit.runners.Parameterized.Parameters;
+
+/**
+ * Tests whole-program type inference with ajava files. This test is the second pass, which ensures
+ * that with the ajava files in place, the errors that those annotations remove are no longer
+ * issued.
+ */
+@Category(AinferNullnessAjavaTest.class)
+public class AinferNullnessAjavaValidationTest extends AinferValidatePerDirectoryTest {
+
+  /**
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public AinferNullnessAjavaValidationTest(List<File> testFiles) {
+    super(
+        testFiles,
+        NullnessChecker.class,
+        "nullness",
+        "ainfer-nullness/annotated",
+        AinferNullnessAjavaTest.class,
+        "-Anomsgtext",
+        ajavaArgFromFiles(testFiles, "nullness"),
+        "-Awarns");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"ainfer-nullness/annotated/"};
+  }
+}

checker/tests/ainfer-index/non-annotated/Dataset6Crash.java

@@ -0,0 +1,57 @@
+// Test case for a WPI crash caused by mismatches between captured type variables
+// and the declared type of a field: in particular, the issue is that base.next()
+// the next field actually have slightly different types: base.next()'s type is
+// a capture that extends T.
+
+import java.util.Iterator;
+
+public class Dataset6Crash {
+
+  public static <T> Iterator<T> limit(final Iterator<? extends T> base, final CountingPredicate<?
+      super T> filter) {
+    return new Iterator<T>() {
+
+      private T next;
+
+      private boolean end;
+
+      private int index = 0;
+
+      public boolean hasNext() {
+        return true;
+      }
+
+      public T next() {
+        fetch();
+        T r = next;
+        next = null;
+        return r;
+      }
+
+      private void fetch() {
+        if (next == null && !end) {
+          if (base.hasNext()) {
+            next = base.next();
+            if (!filter.apply(index++, next)) {
+              next = null;
+              end = true;
+            }
+          } else {
+            end = true;
+          }
+        }
+      }
+
+      public void remove() {
+        throw new UnsupportedOperationException();
+      }
+    };
+  }
+
+
+  private static class CountingPredicate<T> {
+    public boolean apply(int i, T next) {
+      return false;
+    }
+  }
+}

checker/tests/ainfer-index/non-annotated/TypeVarAssignment.java

@@ -0,0 +1,6 @@
+public class TypeVarAssignment<T, S extends T>  {
+T t;
+void foo(S s) {
+  t = s;
+  }
+}

checker/tests/ainfer-nullness/non-annotated/NullTypeVarTest.java

@@ -0,0 +1,32 @@
+// A test that the interaction between type variables and null types
+// is handled correctly in WPI, based on the indentString variable
+// in
+// https://github.com/plume-lib/bcel-util/blob/master/src/main/java/org/plumelib/bcelutil/SimpleLog.java
+
+import java.util.List;
+import java.util.ArrayList;
+
+public class NullTypeVarTest {
+
+  // :: warning: assignment
+  private String indentString = null;
+
+  private List<String> indentStrings;
+
+  private final String INDENT_STR_ONE_LEVEL = "  ";
+
+  public NullTypeVarTest() {
+    indentStrings = new ArrayList<String>();
+    indentStrings.add("");
+  }
+
+  private String getIndentString(int indentLevel) {
+    if (indentString == null) {
+      for (int i = indentStrings.size(); i <= indentLevel; i++) {
+        indentStrings.add(indentStrings.get(i - 1) + INDENT_STR_ONE_LEVEL);
+      }
+      indentString = indentStrings.get(indentLevel);
+    }
+    return indentString;
+  }
+}

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

@@ -793,26 +793,6 @@ protected void updateAnnotationSet(
       return;
     }
 
-    // If the rhsATM and the lhsATM have different kinds (which can happen e.g. when
-    // an array type is substituted for a type parameter), do not attempt to update
-    // the inferred type, because this method is written with the assumption
-    // that rhsATM and lhsATM are the same kind.
-    if (rhsATM.getKind() != lhsATM.getKind()) {
-      // The one difference in kinds situation that this method can account for is the RHS being
-      // a literal null expression.
-      if (!(rhsATM instanceof AnnotatedNullType)) {
-        if (showWpiFailedInferences) {
-          printFailedInferenceDebugMessage(
-              "type structure mismatch, so cannot transfer inferred type"
-                  + "to declared type.\nDeclared type kind: "
-                  + rhsATM.getKind()
-                  + "\nInferred type kind: "
-                  + lhsATM.getKind());
-        }
-        return;
-      }
-    }
-
     AnnotatedTypeMirror atmFromStorage =
         storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);
     updateAtmWithLub(rhsATM, atmFromStorage);
@@ -858,6 +838,20 @@ private void printFailedInferenceDebugMessage(String reason) {
    */
   private void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMirror ajavaATM) {
 
+    if (sourceCodeATM.getKind() != ajavaATM.getKind()) {
+      // Ignore null types: passing them to asSuper causes a crash, as they cannot be
+      // substituted for type variables. If sourceCodeATM is a null type, only the primary
+      // annotation will be considered anyway, so there is no danger of recursing into
+      // typevar bounds.
+      if (sourceCodeATM.getKind() != TypeKind.NULL) {
+        // This can happen e.g. when recursing into the bounds of a type variable:
+        // the bound on sourceCodeATM might be a declared type (such as T), while
+        // the ajavaATM might be a typevar (such as S extends T), or vice-versa. In
+        // that case, use asSuper to make the two ATMs fully-compatible.
+        sourceCodeATM = AnnotatedTypes.asSuper(this.atypeFactory, sourceCodeATM, ajavaATM);
+      }
+    }
+
     switch (sourceCodeATM.getKind()) {
       case TYPEVAR:
         updateAtmWithLub(