Skip to content

Stop UNSUSPEND from restoring switches to JCSwitch nodes#417

Draft
fabiomadge wants to merge 1 commit into
step-1/graceful-skip-and-charfrom
step-2a/suppress-switch-restoration
Draft

Stop UNSUSPEND from restoring switches to JCSwitch nodes#417
fabiomadge wants to merge 1 commit into
step-1/graceful-skip-and-charfrom
step-2a/suppress-switch-restoration

Conversation

@fabiomadge
Copy link
Copy Markdown
Collaborator

@fabiomadge fabiomadge commented May 20, 2026

Step 2a of PLAN.md §3 — switch desugaring suppression.

Resolves (partially)

Summary

Suspenders rewrote JCSwitch/JCSwitchExpression to JCIf/JCConditional before LOWER and reversed the rewrite after. The reversal left JavaToLaurelCompiler with JCSwitchExpression nodes it has no case for, throwing JavaViolationException at the expression-translation default arm. This PR drops the UNSUSPEND-direction restoration so the if/conditional shape survives to translation, and fixes three latent bugs in the SUSPEND rewrites that the round-trip used to mask.

What's in this PR

1. Drop UNSUSPEND restoration. visitIf/visitConditional no longer call switchFromIf/switchExpressionFromConditional. The dead helpers (switchFromIf, switchExpressionFromConditional, their per-direction selector/cases extractors) are deleted. RECORD-flag restoration in visitClassDef and assert-marker restoration in visitIf stay — those need to be symmetrical.

2. Fix latent bug: switch-expression empty-cases base case. The recursion produced a false literal as falsepart, which only mattered once translation actually consumed the conditional. LOWER sees the type mismatch (e.g. int vs boolean) and inserts coercion casts JavaToLaurelCompiler doesn't accept. Restructured to locate the default case explicitly (arrow form allows it anywhere in the list) and use its body as the innermost falsepart, eliminating the placeholder.

3. Fix latent bug: switch-statement default-not-last. switchToIf produced an if-cascade in source order, so default not last lowered to else if (true) { ... } making every later case unreachable — a silent miscompile. Partition non-default cases from the default before building the cascade, with the default body in the trailing else.

4. Fix latent bug: selector evaluated multiple times. switchToIf and switchExpressionToConditional inlined the selector expression into every generated equality test. switch (foo()) { case 0 -> ...; case 1 -> ...; } lowered to if (foo() == 0) ... else if (foo() == 1) ... — multiple evaluations of foo(), costing precision in verification for impure selectors. Hoist into a fresh local ($switchSelectorN) and reference it from each case. For switch expressions, the result is a synthesized JCTree.LetExpr; JavaToLaurelCompiler#convertExpression gains a case that lowers it to a Laurel block (which is a StmtExpr usable in expression position).

5. Renames-aware LetExpr handling. The LetExpr arm in convertExpression inlines JCVariableDecl translation rather than delegating to convertStatement — so the var-decl initializer goes through the renames-aware convertExpression path. Without this, a switch expression inside a postcondition lambda (where the lambda param is renamed to "result") would lower the hoisted-selector's initializer with the original lambda-param name and Strata would see an unbound identifier. SwitchInPostcondition is a regression test.

What flips, what doesn't

Switches.java stays @JVerifyTest(skip = "...") because two of its eleven methods use case null on int @Nullable [], which depends on Step 9. The fixture's source-anchored ^^^^^^^^^^^^ markers also assume the _Bad methods all run their check (and fail) — but the case null methods skip via Step 1's catch instead, so the markers don't fire.

Forms switchToIf can't encode (case-statement groups, non-literal labels, pattern guards, case null) still fall through to LOWER, which mutates them into shapes the translator doesn't accept; those surface as method-level skips via Step 1's per-method catch in JavaToLaurelCompiler. Step 2b will replace those skips with diagnostic-quality refusals at SUSPEND time per PLAN.md §3.

On the LetExpr arm scope

LetExpr is also emitted by javac's Lower for boxed compound-assign, boxed postops, switch-on-string, and pattern-matching switches (verified by reading Lower.java directly). All of those require features JVerify doesn't support yet, blocking those paths before LetExpr would reach the new arm. Today, only Suspenders-synthesized LetExpr reaches it. If a future feature flip enables one of those upstream paths, the broad arm consumes those LetExprs too — which is semantically correct (a LetExpr is a block-with-final-expression) but is a silent scope expansion worth being aware of.

Base branch

Targets #416 (step-1/graceful-skip-and-char). Step 2a's safety net (refused forms surface as method skips, not class-level aborts) is provided by Step 1's catch — without it the test suite would surface red where I want green-skipped. Will rebase onto main once #416 lands.

Test plan

  • ./gradlew :verifier:test passes — 115 / 0 / 72 (was 113 / 0 / 72 on Step 1, +SwitchDesugaring, +SwitchInPostcondition).
  • No new uncaught JavaViolationException stack traces in test output.
  • No green → red transitions.
  • SwitchDesugaring.java covers arrow-form switches end-to-end (statements, expressions, with default in any position, char selector, block body, non-exhaustive, non-trivial selector for hoist coverage, Bad assertion).
  • SwitchInPostcondition.java is a regression test for the lambda-param rename leak through LetExpr's VarDef initializer.

@fabiomadge fabiomadge force-pushed the step-2a/suppress-switch-restoration branch 3 times, most recently from 23343f8 to 8d1a691 Compare May 20, 2026 15:04
Suspenders rewrote JCSwitch/JCSwitchExpression to JCIf/JCConditional
before LOWER and reversed the rewrite after. The reversal left
JavaToLaurelCompiler with JCSwitchExpression nodes it has no case for,
throwing JavaViolationException at the expression-translation default
arm.

Drop the visitIf/visitConditional UNSUSPEND arms that called the
restoration helpers (switchFromIf, switchExpressionFromConditional, and
their per-direction selector/cases extractors) and delete the helpers.
RECORD-flag restoration in visitClassDef stays, as does assert-marker
restoration in visitIf.

Without the round-trip masking edge cases, three latent bugs in the
SUSPEND rewrites surface and need fixing:

1. switchExpressionToConditional's empty-cases base case produced a
   `false` literal as falsepart, which only mattered once translation
   actually consumed the conditional. LOWER sees the type mismatch (e.g.
   int vs boolean) and inserts coercion casts JavaToLaurelCompiler
   doesn't accept. Restructure to locate the default case explicitly
   (arrow form allows it anywhere in the list) and use its body as the
   innermost falsepart.

2. switchToIf produced an if-cascade in source order, so `default` not
   last lowered to `else if (true) { ... }` making every later case
   unreachable — a silent miscompile. Partition before recursing.

3. The selector expression was inlined into every generated equality
   test, evaluating side-effecting selectors multiple times. Hoist into
   a fresh local ($switchSelectorN) and reference it from each case.
   For switch expressions, the result is a JCTree.LetExpr; add a case
   in JavaToLaurelCompiler#convertExpression that lowers it to a Laurel
   block (which is a StmtExpr usable in expression position). The arm
   handles JCVariableDecl defs through a renames-aware path so a switch
   expression inside a postcondition lambda doesn't lose the lambda
   param's rename to "result".

Step 2a of PLAN.md §3. Step 2b will follow with diagnostic-quality
refusals for forms switchToIf can't encode (case-statement groups,
non-literal labels, pattern guards, case null) — those currently fall
through to LOWER and surface as method-level skips via Step 1's catch.

Tests:
  SwitchDesugaring covers arrow-form expressions and statements
    (with/without default, default-not-last, block-body, non-exhaustive,
    char selector, non-trivial selector for hoist coverage, Bad case).
  SwitchInPostcondition is a regression test for the lambda-param
    rename leak through the LetExpr's VarDef initializer.
  Switches.java stays @JVerifyTest(skip = "..."): the two case-null
    methods need Step 9 before the full fixture flips.
  Full suite: 115 / 0 / 72 (was 113 / 0 / 72; +SwitchDesugaring,
    +SwitchInPostcondition).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant