Control flow analysis for exhaustive pattern-switch statement

[Brian Goetz]

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>