From 20eab92c36ef1e829596a9fd2575964fe6a905a9 Mon Sep 17 00:00:00 2001
From: Nada Amin <namin@alum.mit.edu>
Date: Mon, 29 Jun 2026 01:10:22 -0400
Subject: [PATCH] non-empty fallthrough

---
 examples/switchFallthrough.dfy     | 18 ++++++++++++
 examples/switchFallthrough.dfy.gen | 18 ++++++++++++
 examples/switchFallthrough.ts      | 24 ++++++++++++++++
 tools/src/extract.ts               | 44 ++++++++++++++++++------------
 4 files changed, 87 insertions(+), 17 deletions(-)

diff --git a/examples/switchFallthrough.dfy b/examples/switchFallthrough.dfy
index 68c86a2..e8010d2 100644
--- a/examples/switchFallthrough.dfy
+++ b/examples/switchFallthrough.dfy
@@ -30,3 +30,21 @@ method collect(items: seq<Item>) returns (res: seq<int>)
   }
   return out;
 }
+
+method score(tag: Tag) returns (res: int)
+  ensures (res >= 0)
+{
+  var r := 0;
+  match tag {
+    case a =>
+      r := (r + 1);
+      r := (r + 10);
+    case b =>
+      r := (r + 10);
+    case c =>
+      r := (r + 100);
+    case skip =>
+
+  }
+  return r;
+}
diff --git a/examples/switchFallthrough.dfy.gen b/examples/switchFallthrough.dfy.gen
index 68c86a2..e8010d2 100644
--- a/examples/switchFallthrough.dfy.gen
+++ b/examples/switchFallthrough.dfy.gen
@@ -30,3 +30,21 @@ method collect(items: seq<Item>) returns (res: seq<int>)
   }
   return out;
 }
+
+method score(tag: Tag) returns (res: int)
+  ensures (res >= 0)
+{
+  var r := 0;
+  match tag {
+    case a =>
+      r := (r + 1);
+      r := (r + 10);
+    case b =>
+      r := (r + 10);
+    case c =>
+      r := (r + 100);
+    case skip =>
+
+  }
+  return r;
+}
diff --git a/examples/switchFallthrough.ts b/examples/switchFallthrough.ts
index 101acfd..3ddc6b2 100644
--- a/examples/switchFallthrough.ts
+++ b/examples/switchFallthrough.ts
@@ -5,6 +5,8 @@
  * - Stacked `case "a": case "b": case "c": body` — the leading labels have no
  *   statements and fall through, so all three share the body (the `match` gets
  *   an arm per label).
+ * - A *non-empty* case with no trailing break/return also falls through: its
+ *   statements run, then control continues into the next case (`score`).
  * - The body is a `{ … break }` block; that `break` is the *switch* exit and is
  *   dropped, NOT emitted as a `break` of the enclosing `while`. A `break` inside
  *   a nested loop would be kept. See the switch handling in extract.ts.
@@ -39,3 +41,25 @@ export function collect(items: Item[]): number[] {
   }
   return out;
 }
+
+// Non-empty fall-through: "a" runs `r += 1`, then continues into "b" (`r += 10`);
+// "b" stops at its break. Mirrors partial-json-parser's `strip`, where a complete
+// "number" token falls into the "string" handling.
+export function score(tag: Tag): number {
+  //@ verify
+  //@ ensures \result >= 0
+  let r = 0;
+  switch (tag) {
+    case "a":
+      r = r + 1;
+    case "b":
+      r = r + 10;
+      break;
+    case "c":
+      r = r + 100;
+      break;
+    case "skip":
+      break;
+  }
+  return r;
+}
diff --git a/tools/src/extract.ts b/tools/src/extract.ts
index 56eba5c..46f832a 100644
--- a/tools/src/extract.ts
+++ b/tools/src/extract.ts
@@ -1581,25 +1581,35 @@ function extractStmts(stmts: Node[]): RawStmt[] {
       //      nested loop stays put.
       const stripExitBreaks = (b: RawStmt[]) => b.filter(st => st.kind !== "break");
       const isExit = (st: RawStmt | undefined) => !!st && ["break", "return", "throw", "continue"].includes(st.kind);
-      let fallthrough: string[] = [];
-      for (const clause of s.getClauses()) {
-        if (Node.isCaseClause(clause)) {
-          const label = clause.getExpression().getText().replace(/^["']|["']$/g, "");
-          if (clause.getStatements().length === 0) { fallthrough.push(label); continue; }
-          const raw = extractStmts(clause.getStatements());
-          if (!isExit(raw[raw.length - 1]))
-            throw new Error(`switch case "${label}" at line ${line}: a non-empty case must end with break/return/throw; fall-through into the next case is not supported`);
-          const body = stripExitBreaks(raw);
-          for (const l of fallthrough) cases.push({ label: l, body });
-          cases.push({ label, body });
-          fallthrough = [];
-        } else {
-          defaultBody = stripExitBreaks(extractStmts(clause.getStatements()));
-          for (const l of fallthrough) cases.push({ label: l, body: defaultBody });
-          fallthrough = [];
+      // Resolve JS fall-through positionally: a clause's effective body is its
+      // own statements concatenated with each following clause's statements up
+      // to and including the first clause that ends in break/return/throw (or
+      // the switch end). This covers both empty stacked labels (`case A: case
+      // B: body`) and a *non-empty* case that falls through (`case A: sA; case
+      // B: ...`) — the stripped breaks are the switch exits.
+      const clauseInfos = s.getClauses().map(clause => {
+        const stmts = extractStmts(clause.getStatements());
+        return {
+          label: Node.isCaseClause(clause)
+            ? clause.getExpression().getText().replace(/^["']|["']$/g, "")
+            : null,
+          stmts,
+          exits: isExit(stmts[stmts.length - 1]),
+        };
+      });
+      const fallThroughBody = (start: number): RawStmt[] => {
+        let body: RawStmt[] = [];
+        for (let j = start; j < clauseInfos.length; j++) {
+          body = body.concat(clauseInfos[j]!.stmts);
+          if (clauseInfos[j]!.exits) break;
         }
+        return stripExitBreaks(body);
+      };
+      for (let i = 0; i < clauseInfos.length; i++) {
+        const c = clauseInfos[i]!;
+        if (c.label === null) defaultBody = fallThroughBody(i);
+        else cases.push({ label: c.label, body: fallThroughBody(i) });
       }
-      for (const l of fallthrough) cases.push({ label: l, body: [] });
       result.push({ kind: "switch", expr: switchExpr, discriminant, cases, defaultBody, line });
       continue;
     }