diff --git a/checker/build.gradle b/checker/build.gradle
index 168606ab59d..97c29dd64ab 100644
--- a/checker/build.gradle
+++ b/checker/build.gradle
@@ -726,6 +726,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'
diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java
new file mode 100644
index 00000000000..5eb1d8c5e1b
--- /dev/null
+++ b/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.
+ *
+ *
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 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"};
+ }
+}
diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaValidationTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaValidationTest.java
new file mode 100644
index 00000000000..d9e747a3110
--- /dev/null
+++ b/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 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/"};
+ }
+}
diff --git a/checker/tests/ainfer-index/non-annotated/Dataset6Crash.java b/checker/tests/ainfer-index/non-annotated/Dataset6Crash.java
new file mode 100644
index 00000000000..9ebc71e441e
--- /dev/null
+++ b/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 Iterator limit(final Iterator extends T> base, final CountingPredicate
+ super T> filter) {
+ return new Iterator() {
+
+ 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 {
+ public boolean apply(int i, T next) {
+ return false;
+ }
+ }
+}
diff --git a/checker/tests/ainfer-index/non-annotated/TypeVarAssignment.java b/checker/tests/ainfer-index/non-annotated/TypeVarAssignment.java
new file mode 100644
index 00000000000..c30a27ec384
--- /dev/null
+++ b/checker/tests/ainfer-index/non-annotated/TypeVarAssignment.java
@@ -0,0 +1,6 @@
+public class TypeVarAssignment {
+T t;
+void foo(S s) {
+ t = s;
+ }
+}
diff --git a/checker/tests/ainfer-nullness/non-annotated/NullTypeVarTest.java b/checker/tests/ainfer-nullness/non-annotated/NullTypeVarTest.java
new file mode 100644
index 00000000000..8c1be238396
--- /dev/null
+++ b/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 indentStrings;
+
+ private final String INDENT_STR_ONE_LEVEL = " ";
+
+ public NullTypeVarTest() {
+ indentStrings = new ArrayList();
+ 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;
+ }
+}
diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java
index 4909aef108a..0ae8e58eb1d 100644
--- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java
+++ b/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(