typetools / typetools/checker-framework

-AcheckCastElementType triggers BugInCF on various casts

Open
#3,028 2 comments 0 reactions 1 assignee View on GitHub

@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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.