search

lovubuntu / checker-framework

Automatically exported from code.google.com/p/checker-framework
0 stars 0 forks source link

Crash in TypeHierarchy.isSubtype #313

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
This is a contrived example, but if nothing else the error message isn't very 
helpful:

=== Test.java ===
import checkers.nullness.quals.*;

class Test {
  class A<@NonNull T extends @Nullable Object> {}

  <@NonNull X extends @Nullable Object> void m() {
    new A<X>();
  }
}
===

$ ~/jsr308/checker-framework-1.7.5/binary/javac -version -AprintErrorStack 
-processor checkers.nullness.NullnessChecker Test.java
javac 1.8.0-jsr308-1.7.5
error: Found exception during TypeHierarchy.isSubtype of @NonNull X extends 
@Initialized @Nullable Object and @Initialized @NonNull @Nullable Object
  Compilation unit: Test.java
  Exception: java.lang.AssertionError: Found invalid number of annotations on lhsBase @Initialized @NonNull @Nullable Object; comparing lhs: @Initialized @NonNull @Nullable Object rhs: @NonNull X extends @Initialized @Nullable Object; expected number: 2; Stack trace: checkers.types.TypeHierarchy.isSubtypeImpl(TypeHierarchy.java:282)
  checkers.types.TypeHierarchy.isSubtype(TypeHierarchy.java:87)
  checkers.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:1512)
  checkers.basetype.BaseTypeVisitor.checkTypeArguments(BaseTypeVisitor.java:1605)
  checkers.basetype.BaseTypeValidator.visitParameterizedType(BaseTypeValidator.java:288)
  checkers.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:118)
  checkers.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:40)

Original issue reported on code.google.com by cus...@google.com on 2 Apr 2014 at 3:20

GoogleCodeExporter commented 9 years ago 
Thank you for the example and the report.  Work has started on this issue.  

That particular message is an internal failure that is useful for debugging 
framework issues.  If you are interested here is an explanation of the message. 

Type systems have a notion of "hierarchy width".  "Hierarchy width" is the 
number of annotations that should ever appear on a type.  And, to be clear, by 
"appear" I don't necessarily mean written explicitly.  In most cases the 
annotations are inferred/defaulted by the type system. 

In the case of the Nullness type system, the hierarchy width is 2.  (There 
should always be an Freedom Before Commit (initialization) annotation and a 
Nullness annotation. 
http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#in
itialization-checker

Therefore, for the Nullness type system, we always expect two annotations on 
any given Java type after the type has been created.   

In the above case, when verifying that X can indeed be an argument to T there 
is a call:
TypeHierarchy.isSubtype( annotationsOnX, annotationsOnUpperBoundOfT)

Unfortunately it seems that the set of annotations being constructed for T has 
3 (rather than 2 annotations): @Initialized @NonNull @Nullable.   

The type should be either @NonNull and @Nullable, it should not have both.  

Thank you.

Original comment by Jonathan...@gmail.com on 2 Apr 2014 at 5:50

GoogleCodeExporter commented 9 years ago 
Thanks for the explanation. It sounds like the error message is fine, it just 
isn't something an end user is expected to respond to. Thanks for looking into 
it.

Original comment by cus...@google.com on 2 Apr 2014 at 6:16

GoogleCodeExporter commented 9 years ago

Original comment by Jonathan...@gmail.com on 8 Apr 2015 at 10:25

GoogleCodeExporter commented 9 years ago

Original comment by jtha...@cs.washington.edu on 18 Apr 2015 at 6:42