[23] JEP 455 - Exhaustiveness of Switch

[mpalat]

Ref -https://cr.openjdk.org/~abimpoudis/instanceof/jep455-20240424/specs/instanceof-jls.html#jls-14.11

Since primitives can also make a switch enhanced the exhaustiveness rules have changes in conjunction with https://cr.openjdk.org/~abimpoudis/instanceof/jep455-20240424/specs/instanceof-jls.html#jls-5.7.2 - the unconditionally exact

[stephan-herrmann]

According to 14.11.1.1 a switch is exhaustive when (only listing cases relevant for primitives, my numbering):

1. CE contains a pattern that is unconditional (14.30.3) for T.
2. The type T is boolean or Boolean and CE contains both the constant true and the constant false.
3. CE contains a type pattern with a primitive type P, and T is the wrapper class for the primitive type W, and the conversion from type W to type P is unconditionally exact (5.7.2).

ad (2)

Most directly, (2) is implemented in SwitchStatement.resolve() in the check lambda:

• we are comparing two ResolvedCases: c and otherResolvedCase
• when their constants are not equal (con.equals(c2))
• and when the type is boolean, then they must be one true and one false constant
• at this point we set this.switchBits |= Exhaustive :heavy_check_mark:

ad (3)

Next, (3) is implemented in Pattern.coversType(), when the conversion route is one of

• UNBOXING_CONVERSION: conversion is T -> W, where W -> P is identity
• UNBOXING_AND_WIDENING_PRIMITIVE_CONVERSION: here both conversions are explicit / non-trivial
  • in this case we additionally need to check if W -> P is unconditionally exact
  • this is delegated to BaseTypeBinding.isExactWidening()
    • in this method 16 conversions are enumerated, which correspond to the 16 ɛ entries in the table in https://bugs.openjdk.org/browse/JDK-8288476
    • to double-check the slightly tricky correlation to JLS:
    • the quoted paragraph delegates to §5.7.2 ("Unconditionally Exact Testing Conversions") which further delegates to "exact widening primitive conversion", which in §5.1.2 is defined enumerating 4 cases:
      • from an integral type to another integral type
        • byte -> short, byte -> int, byte -> long
        • char -> int, char -> long
        • short -> int, short -> long
        • int -> long
      • from byte, short, or char to a floating-point type
        • byte -> float, byte -> double
        • short -> float, short -> double
        • char -> float, char -> double
      • from int to double
      • from float to double -- TOTAL: 16
    • the listing concerning integral types furthermore relies on:
      • the definition of "integral types": byte, short, int, long, and char (see intro of §4):
      • the fact that char and byte are in no widening relation either way (see first listing in §5.1.2).
• q.e.d. :heavy_check_mark:

ad (1)

Final for (1) §14.30.3 has this:

A pattern p is said to be unconditional for a type T if every value of type T matches p, so that pattern matching requires no action at run time. It is defined as follows:

• A type pattern that declares a pattern variable of a type S is unconditional for a type T if there is a testing conversion that is unconditionally exact (5.7.2) from |T| to |S|.

This is implemented by the remaining branches of Pattern.coversType(), where we see all four bullets from §5.7.2, corresponding to our PrimitiveConversionRoutes:

• an identity conversion
  • = IDENTITY_CONVERSION
• an exact widening primitive conversion
  • WIDENING_PRIMITIVE_CONVERSION && BaseTypeBinding.isExactWidening() (see above)
• a widening reference conversion
  • no primitive conversion, but type.isSubtypeOf(this.resolvedType)
• a boxing conversion
  • BOXING_CONVERSION
• a boxing conversion followed by a widening reference conversion
  • BOXING_CONVERSION_AND_WIDENING_REFERENCE_CONVERSION

Furthermore, to avoid that isSubtypeOf() is applied to byte<->char situations, that case explicitly returns false from WIDENING_AND_NARROWING_PRIMITIVE_CONVERSION.

:heavy_check_mark:

summary

Case (2) directly sets SwitchStatement.Exhaustive during SwitchStatement.resolve()

Cases (1) and (3) are implemented in Pattern.coversType() which then is called from CaseStatement.resolveCasePattern() and upon true this will also set SwitchStatement.Exhaustive.

The difference is due to the fact that in most cases involving primitives exhaustiveness has to be established by a single type pattern (no interaction with other patterns in this regard), but only for boolean two constants achieve the same.

I believe I'm done here :heavy_check_mark:

[stephan-herrmann]

Resolved with #2878