This issue was originally found in the process of developing our own type system. To aid reproducability, I have designed a test case that replicates the issue against one of checker framework's built-in checkers.
import org.checkerframework.checker.tainting.qual.*;
interface AComparable<T extends @Untainted Object> {
int compareTo(T other);
}import org.checkerframework.checker.tainting.qual.*;
class AComparator {
public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
return null;
}
}Eclipse solution, complete with the ant buildfile used, is available here: bounds_type_incompatible_testcase.zip
Running these two files through checker with the TaintingChecker enabled, we get:
Buildfile: C:\eclipse-workspace\checkertests\ant.xml
clean:
[delete] Deleting directory C:\eclipse-workspace\checkertests\build
check-labels:
[mkdir] Created dir: C:\eclipse-workspace\checkertests\build\classes
[jsr308.javac] C:\eclipse-workspace\checkertests\ant.xml:24: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
[jsr308.javac] Compiling 2 source files to C:\eclipse-workspace\checkertests\build\classes
[jsr308.javac] javac 1.8.0-jsr308-2.4.0
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<?>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<?>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<?>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<? extends @Untainted Object super T>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] C:\eclipse-workspace\checkertests\src\AComparator.java:4: error: [bound.type.incompatible] incompatible bounds in wildcard
[jsr308.javac] public <T extends @Untainted AComparable<@Untainted ? super T>> T doSomething() {
[jsr308.javac] ^
[jsr308.javac] type: ? extends @Untainted Object super T extends @Tainted AComparable<?>
[jsr308.javac] upper bound: @Untainted Object
[jsr308.javac] lower bound: T[ extends @Tainted AComparable<?[ extends @Untainted Object super T]> super @Untainted Void]
[jsr308.javac] 10 errors
BUILD FAILED
C:\eclipse-workspace\checkertests\ant.xml:24: Compile failed; see the compiler error output for details.
Total time: 15 seconds
I have debugged into checker code to try and identify the root cause. (Note: this debugging took place on my own type system, not on the TaintChecker, however I will try to adapt the conclusions.)
My chain of thought is:
-
The logic that checks and reports the 'bound.type.incompatible' error is working correctly, but off an incorrectly annotated method type. Specifically, some (recursive) parts of the bounds of the return type are marked @Tainted when they should be @Untainted. This leads the checker to identify a conflict between a lower bound of Tainted and upper bound of Untainted, because Tainted is not a subtype of Untainted.
-
The method is incorrectly annotated because some annotations were not been applied to the (recursive) type variable bounds where they should be, and have been defaulted instead (e.g. to @Tainted).
Specifically, AnnotatedTypeFactory.fromMember(methodTree) returns:
T extends @Untainted AComparable<? extends @Untainted Object super T[ extends AComparable<? extends Object super T[ ... (recurses) ... ]>.
Note that in the result of fromMember(), the AComparable and Object are not annotated in the recursions. These end up being defaulted in getAnnotatedType() to something silly like @Tainted.
-
I do not fully understand the logic that applies the annotations from code. My only observation is that when the bounds on the return type are created for the first time (due to a getUpperBound() call somewhere deep in the code, which triggers lazy-initialisation), the bounds do not have any annotations. (This is appears to be by design.) The annotations are then not added later on.
Note: I notice this account does not completely explain the output above for Taint checker. Taint checker seems to assign Object @Untainted and AComparable @Tainted in subsequent recursions, which is different to my type system, where both types attract the default qualifier in those subsequent recursions. I do not know enough about TaintChecker to understand why this is.
Thanks in advance for any help. Would be interested in your thoughts on whether this issue can be easily fixed or whether I am better off finding a work around.
This issue was originally found in the process of developing our own type system. To aid reproducability, I have designed a test case that replicates the issue against one of checker framework's built-in checkers.
Eclipse solution, complete with the ant buildfile used, is available here: bounds_type_incompatible_testcase.zip
Running these two files through checker with the TaintingChecker enabled, we get:
I have debugged into checker code to try and identify the root cause. (Note: this debugging took place on my own type system, not on the TaintChecker, however I will try to adapt the conclusions.)
My chain of thought is:
The logic that checks and reports the 'bound.type.incompatible' error is working correctly, but off an incorrectly annotated method type. Specifically, some (recursive) parts of the bounds of the return type are marked
@Taintedwhen they should be@Untainted. This leads the checker to identify a conflict between a lower bound of Tainted and upper bound of Untainted, because Tainted is not a subtype of Untainted.The method is incorrectly annotated because some annotations were not been applied to the (recursive) type variable bounds where they should be, and have been defaulted instead (e.g. to
@Tainted).Specifically, AnnotatedTypeFactory.fromMember(methodTree) returns:
T extends @Untainted AComparable<? extends @Untainted Object super T[ extends AComparable<? extends Object super T[ ... (recurses) ... ]>.Note that in the result of fromMember(), the AComparable and Object are not annotated in the recursions. These end up being defaulted in getAnnotatedType() to something silly like
@Tainted.I do not fully understand the logic that applies the annotations from code. My only observation is that when the bounds on the return type are created for the first time (due to a getUpperBound() call somewhere deep in the code, which triggers lazy-initialisation), the bounds do not have any annotations. (This is appears to be by design.) The annotations are then not added later on.
Note: I notice this account does not completely explain the output above for Taint checker. Taint checker seems to assign Object
@Untaintedand AComparable@Taintedin subsequent recursions, which is different to my type system, where both types attract the default qualifier in those subsequent recursions. I do not know enough about TaintChecker to understand why this is.Thanks in advance for any help. Would be interested in your thoughts on whether this issue can be easily fixed or whether I am better off finding a work around.