Guide how to add Checker to existing huge code base.

[MarcinOrlowski]

I am trying to plug-in Checker to existing massive project. Tons of Java source files etc, so it is physically impossible to annotate whole code base at once. So my first idea was to enable Checker in Gradle, then annotate all the soucre the way that would make Checker transparent. So I added

configure<CheckerFrameworkExtension> {
  checkers = listOf(
    "org.checkerframework.checker.nullness.NullnessChecker",
  )
  extraJavacArgs = listOf(
    "-AsuppressWarnings=initialization",
  )
  excludeTests = true
}

and then I wanted to make my sources compilable despite not being annotated properly. I read the docs and found that while by default @NonNull applies, I can override this with @DefaultQualifier annotation, so I annotated all the classes with:

@DefaultQualifier(value = Nullable.class, locations = TypeUseLocation.OTHERWISE)
public class XXX {
....

but this is still not making Checker transparent as I am still facing errors like:

error: [dereference.of.nullable] dereference of possibly-null reference hex
HexModel model = hex.getModel();

So at this point I'd appreciate any assistance that would help me make my code compile w/o detailed annotations as apparently I am missing something here in my actions.

[mernst]

The Nullness Checker is issuing a warning because

• a null pointer exception is possible,
• per section 3.1, "What the Nullness Checker checks", the Nullness Checker warns you about possible null pointer exceptions, and
• you have not suppressed the warning using any of the mechanisms described in chapter 32, "Suppressing warnings".

There are tips for getting started with the Nullness Checker in section 3.6, "Tips for getting started".
There are general tips for getting started with the Checker Framework in section 2.4.2, "How to get started annotating legacy code".

I mention these sections of the manual because you didn't mention having read them, and they recommend a rather different approach than the one you have chosen.
In general, we recommend sticking with the given defaulting scheme. Work class-by-class or module-by-module, incrementally checking more and more code. (Do this by either running the Checker Framework on only a subset of your codebase, or by suppressing warnings in parts of your codebase.)

[MarcinOrlowski]

Thanks for you reply. I actually checked the docs and read what I believed was related to my needs, but it is quite a chance that not knowing the stuff too well, I'd skip important things not even realizing. Anyway, before I plant @SuppressWarnings(allcheckers) around I tried to use -A flag:

  extraJavacArgs = listOf(
    "-AsuppressWarnings=initialization,allcheckers",
  )

but this made Checker crash:

$ ./gradlew build
[....]
error: SourceChecker.typeProcess: unexpected Throwable (AssertionError) while processing logisim-evolution/src/main/java/com/cburch/logisim/fpga/gui/FPGAClockPanel.java; message: case visitor is implemented in SwitchBuilder
; The Checker Framework crashed.  Please report the crash.
Compilation unit: logisim-evolution/src/main/java/com/cburch/logisim/fpga/gui/FPGAClockPanel.java
Last visited tree at line 30 column 1:
public class FPGAClockPanel extends JPanel implements ActionListener, LocaleListener {
Exception: java.lang.AssertionError: case visitor is implemented in SwitchBuilder; java.lang.AssertionError: case visitor is implemented in SwitchBuilder
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitCase(CFGTranslationPhaseOne.java:2202)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitCase(CFGTranslationPhaseOne.java:197)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCCase.accept(JCTree.java:1307)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:109)
at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:117)
at jdk.compiler/com.sun.source.util.TreeScanner.visitSwitchExpression(TreeScanner.java:352)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCSwitchExpression.accept(JCTree.java:1338)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitBinary(CFGTranslationPhaseOne.java:1823)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitBinary(CFGTranslationPhaseOne.java:197)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:2114)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitReturn(CFGTranslationPhaseOne.java:2933)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitReturn(CFGTranslationPhaseOne.java:197)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCReturn.accept(JCTree.java:1665)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitBlock(CFGTranslationPhaseOne.java:2061)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.visitBlock(CFGTranslationPhaseOne.java:197)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:1059)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:60)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.process(CFGTranslationPhaseOne.java:427)
at org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne.process(CFGTranslationPhaseOne.java:466)
at org.checkerframework.framework.flow.CFCFGBuilder.build(CFCFGBuilder.java:73)
at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1494)
at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1402)
at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1840)
at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:414)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:482)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:190)
...
...
...
Process 'Gradle Worker Daemon 1' finished with non-zero exit value 143

Not sure it is my fault or not, but if anyone interested reproducing, then here's my test branch:
https://github.com/MarcinOrlowski/logisim-evolution/tree/checkersframework-test

I will be investigating my setup further, but any hints appreciated.

[MarcinOrlowski]

It seems that if you use switch expressions, then there's still no point trying to use Checker (issue first reported 2019)

• Dataflow support for switch expressions #2373

[mernst]

@MarcinOrlowski As of today's release, the Checker Framework won't crash when encountering Java 17 switch expressions. We expect full support for them in a Dec 17 release.