Skip to content

AsSuperVisitor: type is not an erased subtype of supertype. #6069

@rionda

Description

@rionda

Consider the following files MyInterface.java and MyClass.java.

MyInteface.java:

public interface MyInterface {
    Record foo();
}

MyClass.java:

public class MyClass implements MyInterface {

    public MyRecord foo() {
        return new MyRecord(42);
    }

    record MyRecord(int bar) {}

    public static void main(String[] args) {
        MyClass f = new MyClass();
        System.out.println(f.foo());
    }
}

I got the following crash:

$ ./checker-framework-3.35.0/checker/bin/javac -processor Nullness MyClass.java                                                                                                                                                                
error: AsSuperVisitor: type is not an erased subtype of supertype.
  type: MyRecord
  superType: Record
  ; The Checker Framework crashed.  Please report the crash.
  Compilation unit: MyClass.java
  Last visited tree at line 3 column 5:
      public MyRecord foo() {
  Exception: java.lang.Throwable; java.lang.Throwable
        at org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:34)
        at org.checkerframework.framework.type.AsSuperVisitor.errorTypeNotErasedSubtypeOfSuperType(AsSuperVisitor.java:152)
        at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:340)
        at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:28)
        at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:312)
        at org.checkerframework.framework.type.visitor.AbstractAtmComboVisitor.visit(AbstractAtmComboVisitor.java:64)
        at org.checkerframework.framework.type.AsSuperVisitor.visit(AsSuperVisitor.java:105)
        at org.checkerframework.framework.type.AsSuperVisitor.asSuper(AsSuperVisitor.java:86)
        at org.checkerframework.framework.util.AnnotatedTypes.asSuper(AnnotatedTypes.java:118)
        at org.checkerframework.framework.util.AnnotatedTypes.castedAsSuper(AnnotatedTypes.java:145)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitTypeArgs(DefaultTypeHierarchy.java:475)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:447)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:46)
        at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:312)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:156)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:134)
        at org.checkerframework.common.basetype.BaseTypeVisitor$OverrideChecker.checkReturn(BaseTypeVisitor.java:4275)
        at org.checkerframework.common.basetype.BaseTypeVisitor$OverrideChecker.checkOverride(BaseTypeVisitor.java:3937)
        at org.checkerframework.common.basetype.BaseTypeVisitor.checkOverride(BaseTypeVisitor.java:3686)
        at org.checkerframework.common.basetype.BaseTypeVisitor.checkOverride(BaseTypeVisitor.java:3643)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:988)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:183)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:944)
        at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:92)
        at org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:92)
        at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:396)
        at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:183)
        at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:96)
        at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:111)
        at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:119)
        at jdk.compiler/com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:203)
        at org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:98)
        at org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:597)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:543)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:183)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:851)
        at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:66)
        at org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:86)
        at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1030)
        at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:560)
        at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:553)
        at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:188)
        at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:876)
        at jdk.compiler/com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:132)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1408)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1365)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:960)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:317)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:176)
        at jdk.compiler/com.sun.tools.javac.Main.compile(Main.java:64)
        at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:50)
error: AsSuperVisitor: type is not an erased subtype of supertype.
  type: @Initialized @NonNull MyRecord
  superType: @Initialized @NonNull Record
  ; The Checker Framework crashed.  Please report the crash.
  Compilation unit: MyClass.java
  Last visited tree at line 3 column 5:
      public MyRecord foo() {
  Exception: java.lang.Throwable; java.lang.Throwable
        at org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:34)
        at org.checkerframework.framework.type.AsSuperVisitor.errorTypeNotErasedSubtypeOfSuperType(AsSuperVisitor.java:152)
        at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:340)
        at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:28)
        at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:312)
        at org.checkerframework.framework.type.visitor.AbstractAtmComboVisitor.visit(AbstractAtmComboVisitor.java:64)
        at org.checkerframework.framework.type.AsSuperVisitor.visit(AsSuperVisitor.java:105)
        at org.checkerframework.framework.type.AsSuperVisitor.asSuper(AsSuperVisitor.java:86)
        at org.checkerframework.framework.util.AnnotatedTypes.asSuper(AnnotatedTypes.java:118)
        at org.checkerframework.framework.util.AnnotatedTypes.castedAsSuper(AnnotatedTypes.java:145)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitTypeArgs(DefaultTypeHierarchy.java:475)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:447)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:46)
        at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:312)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:156)
        at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:134)
        at org.checkerframework.common.basetype.BaseTypeVisitor$OverrideChecker.checkReturn(BaseTypeVisitor.java:4275)
        at org.checkerframework.common.basetype.BaseTypeVisitor$OverrideChecker.checkOverride(BaseTypeVisitor.java:3937)
        at org.checkerframework.common.basetype.BaseTypeVisitor.checkOverride(BaseTypeVisitor.java:3686)
        at org.checkerframework.common.basetype.BaseTypeVisitor.checkOverride(BaseTypeVisitor.java:3643)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:988)
        at org.checkerframework.checker.initialization.InitializationVisitor.visitMethod(InitializationVisitor.java:335)
        at org.checkerframework.checker.nullness.NullnessVisitor.visitMethod(NullnessVisitor.java:529)
        at org.checkerframework.checker.nullness.NullnessVisitor.visitMethod(NullnessVisitor.java:69)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:944)
        at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:92)
        at org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:92)
        at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:396)
        at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:183)
        at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:96)
        at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:111)
        at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:119)
        at jdk.compiler/com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:203)
        at org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:98)
        at org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:597)
        at org.checkerframework.checker.initialization.InitializationVisitor.processClassTree(InitializationVisitor.java:288)
        at org.checkerframework.checker.nullness.NullnessVisitor.processClassTree(NullnessVisitor.java:593)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:543)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:183)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:851)
        at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:66)
        at org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:86)
        at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1030)
        at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:560)
        at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:188)
        at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:876)
        at jdk.compiler/com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:132)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1408)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1365)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:960)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:317)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:176)
        at jdk.compiler/com.sun.tools.javac.Main.compile(Main.java:64)
        at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:50)
2 errors

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions