main-eisop crash in TernaryUnspecVsNoQualifier

[cpovirk]

After building the checker (using the JSpecify JDK that uses the old JSpecify package, for the record, as in #156, but I doubt that's relevant), I cloned jspecify as a sibling directory and switched to the samples-google-prototype branch. Then:

$ ../checker-framework/checker/bin/javac -processorpath ../jspecify/build/libs/jspecify-0.0.0-SNAPSHOT.jar:build/libs/jspecify-reference-checker-0.0.0-SNAPSHOT.jar -processor com.google.jspecify.nullness.NullSpecChecker -AcheckImpl -AassumePure -AsuppressWarnings=contracts.conditional.postcondition.false.methodref,contracts.conditional.postcondition.false.override,contracts.conditional.postcondition.true.methodref,contracts.conditional.postcondition.true.override,purity.methodref,purity.overriding,type.anno.before.decl.anno,type.anno.before.modifier -cp ../jspecify/build/libs/jspecify-0.0.0-SNAPSHOT.jar:build/libs/jspecify-reference-checker-0.0.0-SNAPSHOT.jar ../jspecify/samples/TernaryUnspecVsNoQualifier.java
error: Error in AnnotatedTypeMirror.fromExpression(NullSpecAnnotatedTypeFactory, ImmutableList.of(this)): GenericAnnotatedTypeFactory.addComputedTypeAnnotations:  root needs to be set when used on trees; factory: class com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory
  ; The Checker Framework crashed.  Please report the crash.  Version: Checker Framework 3.42.0-eisop3-SNAPSHOT, branch HEAD, 2024-02-06, commit fd74b33, dirty=true. 
  Checker: class com.google.jspecify.nullness.NullSpecChecker
  Visitor: class com.google.jspecify.nullness.NullSpecVisitor
  Compilation unit: ../jspecify/samples/TernaryUnspecVsNoQualifier.java
  Last visited tree at line 25 column 1:
  class TernaryUnspecVsNoQualifier {
  Exception: java.lang.AssertionError: GenericAnnotatedTypeFactory.addComputedTypeAnnotations:  root needs to be set when used on trees; factory: class com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory; java.lang.AssertionError: GenericAnnotatedTypeFactory.addComputedTypeAnnotations:  root needs to be set when used on trees; factory: class com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:2025)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1991)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedTypeFromTypeTree(AnnotatedTypeFactory.java:1556)
        at org.checkerframework.framework.type.SupertypeFinder$SupertypeFindingVisitor.supertypesFromTree(SupertypeFinder.java:352)
        at org.checkerframework.framework.type.SupertypeFinder$SupertypeFindingVisitor.visitDeclared(SupertypeFinder.java:191)
        at org.checkerframework.framework.type.SupertypeFinder.directSupertypes(SupertypeFinder.java:63)
        at org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedDeclaredType.directSupertypes(AnnotatedTypeMirror.java:1137)
        at org.checkerframework.framework.util.AnnotatedTypes.getSuperTypes(AnnotatedTypes.java:646)
        at org.checkerframework.framework.util.AnnotatedTypes.overriddenMethods(AnnotatedTypes.java:667)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.inheritOverriddenDeclAnnos(AnnotatedTypeFactory.java:4358)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getDeclAnnotations(AnnotatedTypeFactory.java:4296)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getDeclAnnotation(AnnotatedTypeFactory.java:4219)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getDeclAnnotation(AnnotatedTypeFactory.java:4197)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getDeclAnnotation(AnnotatedTypeFactory.java:4117)
        at org.checkerframework.framework.util.defaults.QualifierDefaults.defaultsAtDirect(QualifierDefaults.java:765)
        at org.checkerframework.framework.util.defaults.QualifierDefaults.defaultsAt(QualifierDefaults.java:713)
        at org.checkerframework.framework.util.defaults.QualifierDefaults.defaultsAt(QualifierDefaults.java:727)
        at org.checkerframework.framework.util.defaults.QualifierDefaults.applyDefaultsElement(QualifierDefaults.java:855)
        at org.checkerframework.framework.util.defaults.QualifierDefaults.annotate(QualifierDefaults.java:479)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:2292)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1441)
        at com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.getUpperBounds(NullSpecAnnotatedTypeFactory.java:708)
        at com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.nullnessEstablishingPathExists(NullSpecAnnotatedTypeFactory.java:681)
        at com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.isNullExclusiveUnderEveryParameterization(NullSpecAnnotatedTypeFactory.java:621)
        at com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory$NullSpecTypeVariableSubstitutor.substituteTypeVariable(NullSpecAnnotatedTypeFactory.java:855)
        at org.checkerframework.framework.type.TypeVariableSubstitutor$Visitor.visitTypeVariable(TypeVariableSubstitutor.java:173)
        at org.checkerframework.framework.type.TypeVariableSubstitutor$Visitor.visitTypeVariable(TypeVariableSubstitutor.java:82)
        at org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedTypeVariable.accept(AnnotatedTypeMirror.java:1861)
        at org.checkerframework.framework.type.AnnotatedTypeCopier.visit(AnnotatedTypeCopier.java:102)
        at org.checkerframework.framework.type.AnnotatedTypeCopier.visitExecutable(AnnotatedTypeCopier.java:202)
        at org.checkerframework.framework.type.AnnotatedTypeCopier.visitExecutable(AnnotatedTypeCopier.java:44)
        at org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedExecutableType.accept(AnnotatedTypeMirror.java:1265)
        at org.checkerframework.framework.type.AnnotatedTypeCopier.visit(AnnotatedTypeCopier.java:95)
        at org.checkerframework.framework.type.TypeVariableSubstitutor.substitute(TypeVariableSubstitutor.java:34)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.methodFromUse(AnnotatedTypeFactory.java:2591)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.methodFromUse(AnnotatedTypeFactory.java:2503)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.methodFromUse(GenericAnnotatedTypeFactory.java:2298)
        at org.checkerframework.framework.type.TypeFromExpressionVisitor.visitMethodInvocation(TypeFromExpressionVisitor.java:413)
        at org.checkerframework.framework.type.TypeFromExpressionVisitor.visitMethodInvocation(TypeFromExpressionVisitor.java:81)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept(JCTree.java:1666)
        at jdk.compiler/com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:80)
        at org.checkerframework.framework.type.TypeFromTree.fromExpression(TypeFromTree.java:42)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.fromExpression(AnnotatedTypeFactory.java:1843)
        at org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1486)
        at org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:215)
        at org.checkerframework.framework.flow.CFAbstractTransfer.visitMethodInvocation(CFAbstractTransfer.java:999)
        at com.google.jspecify.nullness.NullSpecTransfer.visitMethodInvocation(NullSpecTransfer.java:152)
        at com.google.jspecify.nullness.NullSpecTransfer.visitMethodInvocation(NullSpecTransfer.java:75)
        at org.checkerframework.dataflow.cfg.node.MethodInvocationNode.accept(MethodInvocationNode.java:124)
        at org.checkerframework.dataflow.analysis.AbstractAnalysis.callTransferFunction(AbstractAnalysis.java:356)
        at org.checkerframework.dataflow.analysis.ForwardAnalysisImpl.callTransferFunction(ForwardAnalysisImpl.java:393)
        at org.checkerframework.dataflow.analysis.ForwardAnalysisImpl.performAnalysisBlock(ForwardAnalysisImpl.java:157)
        at org.checkerframework.dataflow.analysis.ForwardAnalysisImpl.performAnalysis(ForwardAnalysisImpl.java:110)
        at org.checkerframework.framework.flow.CFAbstractAnalysis.performAnalysis(CFAbstractAnalysis.java:150)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1623)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1513)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:2100)
        at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:435)
        at com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.preProcessClassTree(NullSpecAnnotatedTypeFactory.java:1684)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:591)
        at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:195)
        at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:808)
        at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:56)
        at org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:89)
        at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1136)
        at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:556)
        at com.google.jspecify.nullness.NullSpecChecker.typeProcess(NullSpecChecker.java:106)
        at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:193)
        at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:828)
        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:1415)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1372)
        at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:972)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:311)
        at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:170)
        at jdk.compiler/com.sun.tools.javac.Main.compile(Main.java:57)
        at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:43)
1 error

I don't immediately see this crash among my results from running the checker on Google's codebase yester (though it's possible that that's only because we were prevented from getting that far by other errors :)). But I see reference to "root needs to be set when used on trees" in the commits referenced from jspecify/checker-framework#11 (also discussed in jspecify/checker-framework#45).

Given that those posts discuss stub files, and given that I hadn't seen the problem inside Google yet, I'd hoped that the problem would go away if I passed -Aignorejdkastub. But I'm seeing it even with that flag.

I do notice inheritOverriddenDeclAnnos in the stack trace, so this seems like more reason to provide a way to skip the inheriting of annotations, as discussed in jspecify/checker-framework#11. Indeed, the error goes away if I make a change similar to jspecify/checker-framework@f3e9f21. (I don't know if the full set of changes is necessary.)

diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index 0dbe8d9f5..34d50389b 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -4268,9 +4268,7 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
 
         AnnotationMirrorSet results = new AnnotationMirrorSet();
         // Retrieving the annotations from the element.
-        // This includes annotations inherited from superclasses, but not superinterfaces or
-        // overridden methods.
-        List<? extends AnnotationMirror> fromEle = elements.getAllAnnotationMirrors(elt);
+        List<? extends AnnotationMirror> fromEle = elt.getAnnotationMirrors();
         for (AnnotationMirror annotation : fromEle) {
             try {
                 results.add(annotation);
@@ -4316,6 +4314,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
      */
     private void inheritOverriddenDeclAnnosFromTypeDecl(
             TypeMirror typeMirror, AnnotationMirrorSet results) {
+        if (true) {
+            return;
+        }
         List<? extends TypeMirror> superTypes = types.directSupertypes(typeMirror);
         for (TypeMirror superType : superTypes) {
             TypeElement elt = TypesUtils.getTypeElement(superType);
@@ -4354,6 +4355,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
      *     the element itself.
      */
     private void inheritOverriddenDeclAnnos(ExecutableElement elt, AnnotationMirrorSet results) {
+        if (true) {
+            return;
+        }
         Map<AnnotatedDeclaredType, ExecutableElement> overriddenMethods =
                 AnnotatedTypes.overriddenMethods(elements, this, elt);
 

[wmdietl]

Thanks for the report!

The smallest I could make the test case is:

import java.util.ArrayList;
import org.jspecify.annotations.NullMarked;

@NullMarked
class Crash<E> extends ArrayList<E> {
    <F> Crash<F> foo() {
        return new Crash<F>();
    }
}

Without the NullMarked it doesn't crash. I'll look into how to fix this crash.

Do you know why this crash doesn't show up in CI? The report only mentions this file with an expected diagnostics were not found.

[cpovirk]

Hmm, I don't remember what it does with crashes....

[wmdietl]

04b8d84, together with the other changes in #165, fixes this issue.
I'm not sure why there is no difference in the conformance tests and no exception showed up in the examples...

When using ./demo instead of the command you give, I can't reproduce the issue even before this change. I'm not sure what's different, but I manually checked that the above commit fixes this test.

[wmdietl]

Fixed by #165.

[cpovirk]

This crash is back (as is #160) as of "Re-instate work-around to type variable bound issue." (I hadn't retested #165 after that commit, so I didn't notice until I went to test #171.)

Your test case above reproduces the failure in main-eisop (at 76b33c9), so I imagine you may have already encountered this as you work to get the tests in the regression subdirectory running.

[wmdietl]

Fixed by #174.