Dataflow support for switch expressions

[michaelhixson]

I am trying to use switch expressions, which is a new preview feature in Java 12. My application depends on NullAway, which is a compiler plugin that depends on the Checker Framework's dataflow library. When I try to compile code that includes a switch expression, NullAway propagates an exception thrown by the dataflow library, causing compilation to fail.

The problematic section of the source code being compiled looks like this:

public static void main(String[] args) {
  String s = switch (args.length) {
    case 0 -> null;
    case 1 -> args[0];
    default -> { throw new IllegalArgumentException("invalid args"); }
  };

  System.out.println(s);
}

The root cause of the error that is thrown is this, from the stack trace that NullAway prints:

[ERROR]   Caused by: java.lang.AssertionError: case visitor is implemented in SwitchBuilder
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitCase(CFGBuilder.java:3381)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitCase(CFGBuilder.java:1416)
[ERROR]         at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCCase.accept(JCTree.java:1293)
[ERROR]         at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
[ERROR]         at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:106)
[ERROR]         at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:114)
[ERROR]         at jdk.compiler/com.sun.source.util.TreeScanner.visitSwitchExpression(TreeScanner.java:354)
[ERROR]         at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCSwitchExpression.accept(JCTree.java:1325)
[ERROR]         at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.translateAssignment(CFGBuilder.java:2687)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitVariable(CFGBuilder.java:4766)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitVariable(CFGBuilder.java:1416)
[ERROR]         at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept(JCTree.java:980)
[ERROR]         at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:82)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:3258)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.visitBlock(CFGBuilder.java:1416)
[ERROR]         at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:1038)
[ERROR]         at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:56)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder$CFGTranslationPhaseOne.process(CFGBuilder.java:1571)
[ERROR]         at shadow.checkerframework.dataflow.cfg.CFGBuilder.build(CFGBuilder.java:255)
[ERROR]         at com.uber.nullaway.dataflow.DataFlow$2.load(DataFlow.java:124)
[ERROR]         at com.uber.nullaway.dataflow.DataFlow$2.load(DataFlow.java:94)
[ERROR]         at com.google.common.cache.LocalCache$LoadingValueReference.loadFuture(LocalCache.java:3528)
[ERROR]         at com.google.common.cache.LocalCache$Segment.loadSync(LocalCache.java:2277)
[ERROR]         at com.google.common.cache.LocalCache$Segment.lockedGetOrLoad(LocalCache.java:2154)
[ERROR]         at com.google.common.cache.LocalCache$Segment.get(LocalCache.java:2044)
[ERROR]         ... 110 more

That's pointing to this part of the dataflow library:

checker-framework/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java

Lines 3382 to 3385 in 0e5541c

	@Override
	public Node visitCase(CaseTree tree, Void p) {
	throw new AssertionError("case visitor is implemented in SwitchBuilder");
	}

I originally filed this issue in NullAway's issue tracker, but the maintainer suggested that it was an upstream issue with the dataflow library so I should also file it here. I wanted to produce a test case that used dataflow directly without NullAway to share with you, but I couldn't figure out how.

[lazaroclapp]

Note that both Checker Framework and NullAway are missing support for switch expressions. But adding it to the later in a clean way would be much easier after having it in the former :)

[wmdietl]

Thanks for reporting this issue!
The Checker Framework currently builds on a Java 8 javac and we have a version that mostly works with javac 9 to 11.
Java 12 is the first in a while that added a new AST node, right? I'm not sure what the best way is to add support for such Java 12 AST nodes while being usable with an older compiler that doesn't have it.
error-prone similarly currently works with Java 8 - 11, I think. What is NullAway's plan for supporting Java 12?

[lazaroclapp]

@msridhar for the more authoritative answer. AFAIK, we are focusing on Java 8 for our internal codebase (at Uber), and intend to remain compatible with that version for the foreseeable future. We are aiming to support Java 11 (uber/NullAway#259), and would probably not mind supporting Java 12 if we could.

[michaelhixson]

error-prone similarly currently works with Java 8 - 11, I think.

There is an issue tracking Java 12+ compatibility issues here: google/error-prone#1106

It looks like external contributors figured out fixes for most/all of the issues. I don't know if Google plans to merge any of those fixes.

For what it's worth, as a user of Error Prone, when I upgraded my application to Java 12 I only had to disable one exception-throwing bug pattern. It even tolerated switch expressions, though IIRC its "unnecessary parentheses" bug pattern got confused and suggested removing the parens after the switch keyword. That said, I wouldn't be surprised if more extensive use of switch expressions would make it throw exceptions.

Also, in case it helps you all calculate the level of urgency / non-urgency of supporting switch expressions, I believe they are targeted to graduate out of preview in Java 13, which will be released 6 months from now in September, 2019. See: https://mail.openjdk.java.net/pipermail/amber-dev/2019-March/004126.html

Edit: Switch expressions will still be a preview feature in Java 13, so they will probably not graduate out of preview until Java 14, which will be released in March, 2020.

[msridhar]

Core NullAway works fine (AFAIK) on Java 11. If supporting Java 12 is not a huge burden, and it doesn't break backward compatibility, we'd be happy to do it. I haven't thought carefully through what it takes to support the switch expression on the NullAway side, but at a high level it seems like a fancier conditional expression so it shouldn't be too hard? As it seems now, the trickiest change would be in the CFG construction in Checker Dataflow, as this does introduce some new control flow. Maybe the existing switch logic can be reused? Also not sure about backward compatibility.

[wmdietl]

Update on this: adapting the CFG construction itself shouldn't be too hard, but it requires depending on the new jdk.compiler/com.sun.source.util.TreeScanner.visitSwitchExpression(TreeScanner.java:354) visit method and corresponding SwitchExpressionTree.
I don't see a simple way to keep compatible with Java < 12 and at the same time supporting this preview feature.
Any suggestions?

Removing the AssertionError in visitCase also doesn't help, as then no node for the switch is created and other parts break.

So I would suggest that once typetools merges https://github.com/eisop/checker-framework and supports Java 9 - 12, we can look into backwards-incompatible support for Java 12 preview and Java 13+ in eisop.

[michaelhixson]

Removing the AssertionError in visitCase also doesn't help, as then no node for the switch is created and other parts break.

What breaks?

Removing the overridden visitCase implementation from my local copy of dataflow allows my switch-expression-containing project to compile. From my perspective that's an improvement over not compiling because of an uncaught AssertionError. Do you think removing that override is not a reasonable short-term fix?

[msridhar]

I think conditionally removing the AssertionErroron JDK 12+ is a reasonable workaround if you're getting useful results otherwise.

As to a medium- to longer-term fix that maintains backward compatibility, the only way I see to do it is to use a pre-processor. raydac/java-comment-preprocessor seems to be maintained and has a Gradle plugin (example). They have an example showing how to conditionally include code for different Java versions here. I think it's worth experimenting with this tool as a way to get backward-compatible support, as this kind of thing will come up again for other new language features. @wmdietl thoughts?

[msridhar]

There is also the Manifold Preprocessor which is cool since it runs as a Javac plugin. But it doesn't put the preprocessor directives in comments, so the Manifold IDE plugin is required to prevent the IDE from showing syntax errors.

[wmdietl]

@michaelhixson Our goal is to provide sound handling for all Java constructs. These assertion errors help us make sure that we correctly handle all possible ASTs. We could explore adding a flag that allows ignoring these issues.

@msridhar Thanks for mentioning these two projects! After a quick look, I think I would prefer using java-comment-preprocessor, as it stays valid Java source (at least hopefully).
I'm working on a branch that supports Java 13 and experiments with this. More soon.

[msridhar]

@wmdietl Agreed re: keeping valid Java source. Even so, things will be a bit janky since the un-pre-processed source code won't compile and will likely show errors in an IDE. So probably the pre-processor will have to run before you can start hacking the code. But then the code might look modified according to Git? There really are some advantages to having a language with a built-in macro system...

[msridhar]

FWIW, Google Java Format just added support for JDK 14 constructs while maintaining backward compatibility through a bit of subclassing and clever reflection:

google/google-java-format@4ddb914#diff-c96edae3736870de40b2ab8b0657014dR157-R169

From what I can tell, a single GJF jar built using JDK14 should still run fine all the way back to JDK 8. In order to format the JDK14 constructs, you need to be running GJF on JDK14, but that seems like a reasonable compromise.

@wmdietl perhaps a similar approach could be used here, to avoid a pre-processor?

[wmdietl]

@msridhar Thanks for the pointer! I'll take a look whether something like that would work.
I can see how this might work for CFG construction, where we could have subclasses for e.g. Java 14.
I'm a bit doubtful for type visitors, because we would want logic in BaseTypeVisitor to handle switch expressions. But we can't reflectively load different subclasses of BTV, as the different type checkers extend that class. So I'm not sure how we could do this.

[msridhar]

Yes that’s true. Even just having CFG construction being more compatible could be helpful for now, for other projects relying on dataflow. Fixing BaseTypeVisitor may still be most easily solved with some kind of pre-processing.

[pentlander]

Seems like backward compat could be solved using a multi-release jar: https://openjdk.java.net/jeps/238

[mernst]

Yes, that may work. If you are interested in setting that up, we would gladly accept a pull request. Thanks!

[pentlander]

Cool I'll take a look this week to see what's involved.

[mernst]

Great, thanks!

[pentlander]

Would you be willing to accept a PR that sets up the multi-release jar that just has a stub method for the visitSwitchExpression case in the BaseTypeVisitor? After looking, I realized I have no idea what the code for the visitor implementation should actually look like lol. If not, I'll need a decent amount of coaching and iteration to get it working if someone is willing to babysit me.

[mernst]

That is OK. The multi-release jar is a rather different task than handling switch statements, so splitting them into different tasks makes sense.

[msridhar]

@mernst was this fixed by #4677?

[mernst]

@mernst was this fixed by #4677?

No, it was not. From the changelog:

Partial support for JDK 16. You can run the Checker Framework on a JDK 16 JVM.
You can pass the --release 16 command-line argument to the compiler. New
syntax, such as records and switch expressions, is not yet type-checked; that
will be added in a future release. Thanks to Neil Brown for the JDK 16 support.

[msridhar]

Ok, thanks! I saw some changes to CFG construction in that PR related to switches, so I thought that maybe the CFGs at least would accurately represent switch expressions, even if full type checking is not yet supported.

[mernst]

@msridhar The CFG construction treats switch statements a bit specially, and it also asserts that case appears only within a switch statement. That is not true in Java 16, since case can appear within a switch expression. It will take a little bit of work to handle the new syntax in the dataflow framework.

[TomBeckett]

@mernst Has there been any movement on support for switch statements?

[mernst]

We are working on it (currently evaluating a couple of different implementation strategies). Assistance is always welcome.

[smillst]

As of release 3.20.0, The dataflow framework does not crash on switch expressions, but they are not analyzed. We are working on implementing the analysis.

[fprochazka]

@smillst do you have an issue I could subscribe to, please?

[mernst]

@fprochazka The issue that is mentioned immediately before your comment, #4982, adds support for switch expressions. It has already been merged. Release 3.20.0 will occur today.

[fprochazka]

Now I understand, thanks!