Skip to content

main-eisop crash in TernaryUnspecVsNoQualifier #159

@cpovirk

Description

@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);
 

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions