typetools / typetools/checker-framework
-AcheckCastElementType triggers BugInCF on various casts
Open
@smillst is already working on this.
Since Jan 6, 2020.
crash
- Dominant language
- Java
- Stars
- 1.1k
- Forks
- 440
- Avg merge
- 1d 12h
- Merged PRs (30d)
- 134
Description
When I experimented with turning on -AcheckCastElementType, I discovered that it produces crashes on many casts. For example:
$ cat Cast.java
class Cast {
void cast(Object o) {
Cast cast = (Cast) o;
}
}
$ checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker -AcheckCastElementType Cast.java
error: AsSuperVisitor: type is not an erased subtype of supertype.
type: @Initialized @NonNull Object
superType: @Initialized @NonNull Cast
Compilation unit: Cast.java
Last visited tree at line 3 column 17:
Cast cast = (Cast) o;
Exception: java.lang.Throwable; Stack trace: org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:25)
org.checkerframework.framework.type.AsSuperVisitor.errorTypeNotErasedSubtypeOfSuperType(AsSuperVisitor.java:154)
org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:338)
org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:28)
org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:307)
org.checkerframework.framework.type.visitor.AbstractAtmComboVisitor.visit(AbstractAtmComboVisitor.java:57)
org.checkerframework.framework.type.AsSuperVisitor.visit(AsSuperVisitor.java:85)
org.checkerframework.framework.type.AsSuperVisitor.asSuper(AsSuperVisitor.java:67)
org.checkerframework.framework.util.AnnotatedTypes.asSuper(AnnotatedTypes.java:112)
org.checkerframework.framework.util.AnnotatedTypes.castedAsSuper(AnnotatedTypes.java:140)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:465)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:41)
org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:307)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:182)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:158)
org.checkerframework.common.basetype.BaseTypeVisitor.isTypeCastSafe(BaseTypeVisitor.java:1926)
org.checkerframework.common.basetype.BaseTypeVisitor.checkTypecastSafety(BaseTypeVisitor.java:1879)
org.checkerframework.common.basetype.BaseTypeVisitor.visitTypeCast(BaseTypeVisitor.java:1985)
org.checkerframework.checker.initialization.InitializationVisitor.visitTypeCast(InitializationVisitor.java:270)
org.checkerframework.checker.nullness.NullnessVisitor.visitTypeCast(NullnessVisitor.java:428)
org.checkerframework.checker.nullness.NullnessVisitor.visitTypeCast(NullnessVisitor.java:54)
com.sun.tools.javac.tree.JCTree$JCTypeCast.accept(JCTree.java:2022)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:88)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:301)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:167)
com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:90)
com.sun.source.util.TreeScanner.visitVariable(TreeScanner.java:223)
org.checkerframework.framework.source.SourceVisitor.visitVariable(SourceVisitor.java:100)
org.checkerframework.common.basetype.BaseTypeVisitor.visitVariable(BaseTypeVisitor.java:1043)
org.checkerframework.checker.initialization.InitializationVisitor.visitVariable(InitializationVisitor.java:167)
org.checkerframework.checker.initialization.InitializationVisitor.visitVariable(InitializationVisitor.java:52)
com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept(JCTree.java:968)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:88)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:301)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:167)
com.sun.source.util.TreeScanner.scan(TreeScanner.java:105)
com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:248)
com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:1026)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:88)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:301)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:167)
com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:90)
com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:206)
org.checkerframework.framework.source.SourceVisitor.visitMethod(SourceVisitor.java:106)
org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:683)
org.checkerframework.checker.initialization.InitializationVisitor.visitMethod(InitializationVisitor.java:337)
org.checkerframework.checker.initialization.InitializationVisitor.visitMethod(InitializationVisitor.java:52)
com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:898)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:88)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:301)
org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:167)
com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:90)
com.sun.source.util.TreeScanner.scan(TreeScanner.java:105)
com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:113)
com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:187)
org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:94)
org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:384)
org.checkerframework.checker.initialization.InitializationVisitor.processClassTree(InitializationVisitor.java:295)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:339)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:167)
com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:808)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:56)
org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:82)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1020)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:523)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:182)
com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:828)
com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:120)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1404)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1363)
com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:959)
com.sun.tools.javac.main.Main.compile(Main.java:302)
com.sun.tools.javac.main.Main.compile(Main.java:162)
com.sun.tools.javac.Main.compile(Main.java:57)
com.sun.tools.javac.Main.main(Main.java:43)
1 error
Source file and -version -verbose -AprintAllQualifiers output attached. [edit: fixed output to actually use -AcheckCastElementType and thus actually trigger the error]
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.