Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix crash in ajava-based WPI related to captures (#5335)
- Loading branch information
Showing
7 changed files
with
232 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
40 changes: 40 additions & 0 deletions
40
...t/java/org/checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"}; | ||
} | ||
} |
37 changes: 37 additions & 0 deletions
37
.../checkerframework/checker/test/junit/ainferrunners/AinferNullnessAjavaValidationTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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/"}; | ||
} | ||
} |
57 changes: 57 additions & 0 deletions
57
checker/tests/ainfer-index/non-annotated/Dataset6Crash.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} | ||
} | ||
} |
6 changes: 6 additions & 0 deletions
6
checker/tests/ainfer-index/non-annotated/TypeVarAssignment.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
public class TypeVarAssignment<T, S extends T> { | ||
T t; | ||
void foo(S s) { | ||
t = s; | ||
} | ||
} |
32 changes: 32 additions & 0 deletions
32
checker/tests/ainfer-nullness/non-annotated/NullTypeVarTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters