Control flow analysis for exhaustive pattern-switch statement
Brian Goetz
brian.goetz at oracle.com
Thu Feb 3 16:35:13 UTC 2022
Thanks Tagir for digging into this. This is good analysis.
The decision to require completeness of enhanced switches was taken
relatively late, so its quite possible we have left something out. And
in the next round, when nested patterns come along, we need to formalize
totality and remainder, which also intersects with this problem. So
this is timely.
On 2/3/2022 12:41 AM, Tagir Valeev wrote:
> Hello!
>
> JLS requires (14.11.2) that the new "enhanced" switch statement (not
> expressions) must be exhaustive. In particular, for the switch over
> sealed abstract type, it's required to list all the permitted subtypes
> or provide a total/default branch. This is good. However, this means
> that from CFG point of view exactly one switch branch must always be
> visited. This is indeed so if we take a look at the bytecode: the
> synthetic default branch throws IncompatibleClassChangeError(). But
> compiler ignores this fact and refuses to compile the code like this
> (tried 18-ea+33-2077):
>
> sealed interface Parent {}
> record A() implements Parent {}
> record B() implements Parent {}
>
> void test(Parent p) {
> int x;
> switch (p) {
> case A a -> x = 1;
> case B b -> x = 2;
> }
> System.out.println(x); // error: variable x might not have been initialized
> }
>
> I think this is a mistake that should be corrected: in this code, `x`
> should be considered as definitely assigned.
Agreed. This is exactly why we have "remainder"; the set { A, B } is
total on Parent, with remainder; the remainder includes all novel
subclasses of Parent that were born after test(Parent) was compiled.
Our goal is that for a switch (or other pattern match construct) where
the pattern(s) are total on the target, is that you cannot arrive at the
statement after the switch without one of the branches being taken. In
the case of the remainder (e.g., a late-breaking C class), the switch
will complete abruptly, so the correct characterization of your "exactly
one" is that "if the switch completes normally, exactly one branch was
visited." Then we arrange for the switch to complete abruptly in case
of remainder. (Remainder also includes things like Box(null) in a case
Box(Bag(String s)); we had a long thread about the interesting shape of
remainder sets last summer, and this topic will soon return, hopefully
with the aid of more mathematical formalism.)
> I understand that the same reasoning does not apply for switch over
> enums, as for compatibility reasons, default behavior is to do
> nothing. However, for patterns, uninitialized `x` cannot appear after
> the switch, even if we recompile the sealed interface separately
> adding one more inheritor.
Slight correction: *statement* switches over enums. We've carved out a
place where the only switches that are not total, are *statement*
switches over the legacy types with the legacy switch labels. In that
case, DU analysis picks up some of the slack.
(It is still on our "to be considered" list whether it is worth it to
allow statement switches to be explicitly marked as total to engage
greater typechecking, or whether we want to embark on the decade-long
path of warning increasingly loudly on non-total switches until we
eventually make them illegal.)
> I try to understand what's written in 16.2.9 regarding this [1].
> Unfortunately, its current state looks confusing to me. Sorry if I'm
> missing something, as I'm not very experienced in reading chapter 16
> of JLS. Nevertheless, it says:
>
> V is [un]assigned after a switch statement (14.11) iff all of the
> following are true:
> ...
> Original spec:
> - If there is no default label in the switch block, or if the switch
> block ends with a switch label followed by the } separator, then V is
> [un]assigned after the selector expression.
> Preview spec:
> - If the switch block covers the type of the selector expression, or
> if the switch block ends with a switch label followed by the }
> separator, then V is [un]assigned after the selector expression.
>
> It looks strange that "no default label" (~= non-exhaustive) was
> replaced with "covers the type" (= exhaustive). Was negation lost
> somewhere? In current state it looks like, all exhaustive switches
> (which is almost all switches), including ones with `default` branch
> cannot definitely assign a variable, which contradicts the previous
> state.
>
> If negation is actually lost, then the sample above should compile, as
> it's exhaustive.
I'll take a read-through of the spec (or more likely, Gavin will beat me
to it) and respond more completely at that point.
Thanks,
-Brian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20220203/8229055f/attachment.htm>
More information about the amber-spec-experts
mailing list