search

biddyweb / checker-framework

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

Crash in CFCFGBuilder: ArrayType must be represented by AnnotatedArrayType #419

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Here's the repro:

=== Test.java ===
import org.checkerframework.checker.nullness.qual.*;

class Test {
  <T> @NonNull T verifyNotNull(@Nullable T o) {
    return o;
  }
  interface Pair<A, B> {
    @Nullable A getFirst();
  }
  void m(Pair<String[], int[]> p) {
    for (String s : verifyNotNull(p.getFirst())) {
    }
  }
}
===

$ ~/jsr308/checker-framework-1.8.11/checker/bin/javac -version 
-AprintErrorStack -processor 
org.checkerframework.checker.nullness.NullnessChecker Test.java

javac 1.8.0-jsr308-1.8.11
error: SourceChecker.typeProcess: unexpected Throwable (AssertionError) while 
processing Test.java; message: ArrayType must be represented by 
AnnotatedArrayType
  Compilation unit: Test.java
  Exception: java.lang.AssertionError: ArrayType must be represented by AnnotatedArrayType; Stack trace: org.checkerframework.framework.flow.CFCFGBuilder$CFCFGTranslationPhaseOne.visitEnhancedForLoop(CFCFGBuilder.java:322)
  org.checkerframework.framework.flow.CFCFGBuilder$CFCFGTranslationPhaseOne.visitEnhancedForLoop(CFCFGBuilder.java:101)
  com.sun.tools.javac.tree.JCTree$JCEnhancedForLoop.accept(JCTree.java:1043)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
  org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:3178)
  org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:1392)
  com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:918)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
  org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.process(CFGBuilder.java:1517)
  org.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.process(CFGBuilder.java:1538)
  org.checkerframework.framework.flow.CFCFGBuilder.run(CFCFGBuilder.java:92)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:661)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:653)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:599)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:846)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:813)
  org.checkerframework.checker.nullness.NullnessAnnotatedTypeFactory.annotateImplicit(NullnessAnnotatedTypeFactory.java:167)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:797)
  org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:624)
  org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1683)
  org.checkerframework.checker.initialization.InitializationVisitor.visitClass(InitializationVisitor.java:291)
  org.checkerframework.checker.initialization.InitializationVisitor.visitClass(InitializationVisitor.java:57)
  com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
  org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
  org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:828)
  org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:442)
  org.checkerframework.framework.source.AggregateChecker.typeProcess(AggregateChecker.java:123)
  org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:205)
  com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
  com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
  com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
  com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
  com.sun.tools.javac.main.Main.compile(Main.java:523)
  com.sun.tools.javac.main.Main.compile(Main.java:381)
  com.sun.tools.javac.main.Main.compile(Main.java:370)
  com.sun.tools.javac.main.Main.compile(Main.java:361)
  com.sun.tools.javac.Main.compile(Main.java:56)
  com.sun.tools.javac.Main.main(Main.java:42)
1 error

Original issue reported on code.google.com by cus...@google.com on 23 Mar 2015 at 3:37

GoogleCodeExporter commented 9 years ago 
Hi Liam,

thanks for the report.
I cannot reproduce the issue with the current trunk version. Are you using the 
last release I assume?

I guess this issue was caused by not correctly inferring a type argument for 
verifyNotNull, which then confused the CFG generation for enhanced-for.
Jonathan recently pushed many improvements to type arg inference.

With trunk, I get:

Issue419.java:5: error: [return.type.incompatible] incompatible types in return.
    return o;
           ^
  found   : T[ extends @Initialized @Nullable Object super @FBCBottom @Nullable Void]
  required: T[ extends @Initialized @NonNull Object super @FBCBottom @NonNull Void]
1 error

Which seems like the right error, as your verify method doesn't verify anything 
:-)

Can you by any chance try running with the trunk version? Other things might 
break and we would appreciate the feedback before the next release.

Original comment by wdi...@gmail.com on 23 Mar 2015 at 10:40

GoogleCodeExporter commented 9 years ago 
Hi Werner,

Yes, this was with the 1.8.11 release. The error produced by trunk looks good 
to me, I realize the repro code is silly in a few ways :)

I'm testing against trunk now, and will let you know once I have results.

Thanks!

Original comment by cus...@google.com on 24 Mar 2015 at 9:46

GoogleCodeExporter commented 9 years ago 
I added the test case to make sure the issue doesn't return.
https://code.google.com/p/checker-framework/source/detail?r=3f2c6bccbbf05716b7cd
bf28c9fedeb18e718271

Thanks,
cu, WMD.

Original comment by wdi...@gmail.com on 25 Mar 2015 at 9:35