Switch exhaustiveness by rewriting

[stephan-herrmann]

From scanning the code I could not find an implementation for this from JLS 14.11.1.1. Exhaustive Switch Blocks:

A set of case elements, P, covers a type T if one of the following cases applies:
[...]

• P rewrites to a set Q and Q covers T.

With more details in this paragraph.

@mpalat @srikanth-sankaran had you noticed this JLS paragraph during your work on enhanced switches? Has the above been implemented and I just looked in the wrong places?

[stephan-herrmann]

FWIW, the question arose when I just looked up the definition of "exhaustive" while working my way through https://bugs.openjdk.org/browse/JDK-8357464
Also I recall some discussions about intricacies of this feature on compiler-dev@openjdk, so if we're in need of advanced test cases I could probably dig out at least some.

[srikanth-sankaran]

@srikanth-sankaran had you noticed this JLS paragraph during your work on enhanced switches?

No, not that I recall.

[srikanth-sankaran]

Assigning to Manoj as he requested to work in this.

[mpalat]

@mpalat @srikanth-sankaran had you noticed this JLS paragraph during your work on enhanced switches? Has the above been implemented and I just looked in the wrong places?

@stephan-herrmann Yes, please see comment where this is mentioned. I remember using a graph based design while doing this with a visitor pattern. And essentially this graph based check captures the reduction leading to an implicit rewrite. Some this code has been rewritten/improved later (not implying that any bug was introduced - just that the code has changed). That said, I have got one case - actually an opposite case - where the lack of exhaustiveness is not being reported - in the process of checking. will put a PR for the same against this issue anyway.

[srikanth-sankaran]

Some this code has been rewritten/improved later

The record pattern exhaustiveness analysis code was simplified but was not rewritten or improved. I didn't understand it well enough :) It seemed to be doing something profound and seemed to be working, so I decided not to tinker with it beyond obvious boiler plate elimination.

See #3458 and #3172, commit 9096700

This gives you a commit you can quickly check for any bug injection.

[stephan-herrmann]

@mpalat @srikanth-sankaran had you noticed this JLS paragraph during your work on enhanced switches? Has the above been implemented and I just looked in the wrong places?

@stephan-herrmann Yes, please see comment where this is mentioned. I remember using a graph based design while doing this with a visitor pattern. And essentially this graph based check captures the reduction leading to an implicit rewrite. Some this code has been rewritten/improved later (not implying that any bug was introduced - just that the code has changed). That said, I have got one case - actually an opposite case - where the lack of exhaustiveness is not being reported - in the process of checking. will put a PR for the same against this issue anyway.

@mpalat it's good news we're not blank on this feature.

Do you think you could sprinkle the code with references to JLS, so uninitiated people like myself have a chance to understand, review, modify this implementation?