eisop / checker-framework

Pluggable type-checking for Java
https://eisop.github.io/
Other
15 stars 16 forks source link

Improve `CFValue` well-formedness checks #536

Open wmdietl opened 1 year ago

wmdietl commented 1 year ago

534 disabled a seemingly size comparison in CFAbstractValue.

Re-enable this check, try to reproduce the Guava failure, minimize a test, and fix the issue. There are a few other well-formedness checks in CFValue classes that we should strengthen.

wmdietl commented 1 year ago

The stacktrace from the Guava failure:

[WARNING] /__w/1/guava/guava/src/com/google/common/escape/Platform.java:[39,26] [type.argument.type.incompatible] incompatible type argument for type parameter T of ThreadLocal.
  found   : @Initialized @NonNull char @Initialized @NonNull []
  required: [extends @Initialized @Nullable Object super null (NullType)]
[WARNING]   ; The Checker Framework crashed.  Please report the crash.
  Checker: class org.checkerframework.common.value.ValueChecker
  Visitor: class org.checkerframework.common.value.ValueVisitor
  Compilation unit: /__w/1/guava/guava/src/com/google/common/hash/FarmHashFingerprint64.java
  Last visited tree at line 47 column 1:
  final class FarmHashFingerprint64 extends AbstractNonStreamingHashFunction {
  Exception: java.lang.NullPointerException: Cannot invoke "org.checkerframework.framework.flow.CFValue.getAnnotations()" because "value" is null; java.lang.NullPointerException: Cannot invoke "org.checkerframework.framework.flow.CFValue.getAnnotations()" because "value" is null
    at org.checkerframework.common.value.ValueTransfer.isIntRange(ValueTransfer.java:415)
    at org.checkerframework.common.value.ValueTransfer.isIntRangeOrIntegralUnknownVal(ValueTransfer.java:438)
    at org.checkerframework.common.value.ValueTransfer.calculateNumericalBinaryOp(ValueTransfer.java:803)
    at org.checkerframework.common.value.ValueTransfer.visitNumericalSubtraction(ValueTransfer.java:950)
    at org.checkerframework.common.value.ValueTransfer.visitNumericalSubtraction(ValueTransfer.java:75)
    at org.checkerframework.dataflow.cfg.node.NumericalSubtractionNode.accept(NumericalSubtractionNode.java:33)
    at org.checkerframework.dataflow.analysis.AbstractAnalysis.callTransferFunction(AbstractAnalysis.java:356)
    at org.checkerframework.dataflow.analysis.ForwardAnalysisImpl.callTransferFunction(ForwardAnalysisImpl.java:391)
    at org.checkerframework.dataflow.analysis.ForwardAnalysisImpl.performAnalysisBlock(ForwardAnalysisImpl.java:133)
    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:1541)
    at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1436)
    at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1895)
    at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:421)
    at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:550)
    at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:188)
    at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:860)
    at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:60)
    at org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:89)
    at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1113)
    at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:564)
    at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:557)
    at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:193)
    at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:854)
    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:1394)
    at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1351)
    at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:946)
    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)
/__w/1/guava/guava/src/com/google/common/hash/FarmHashFingerprint64.java:[88,18] [shift.unsigned] UNSIGNED_RIGHT_SHIFT operation on a signed value
  lhs: @Signed long
  rhs: @SignednessGlb long