Skip to content

[TS] Route thrown exceptions into catch blocks - #463

Open
CaelmBleidd wants to merge 11 commits into
mainfrom
caelmbleidd/ts-427-catch-routing
Open

CaelmBleidd wants to merge 11 commits into
mainfrom
caelmbleidd/ts-427-catch-routing

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 2, 2026 •

Copy link
Copy Markdown
Member

Current stacked revision

  • Base: 127ecb5df35366c550a32725cf4e6af25208f673. Head: 253e55a72435c5c0aa7cf996b36f1ee745d15c83. The rebased issue-specific implementation remains linear; the final commit only replaces duplicate test-side Node process handling with the shared helper.
  • On the current head, TsCatchRoutingTest passed (1/1), detektTest, and git diff --check passed using local JacoDB [TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399. detektMain passed on the preceding implementation head 2d655b84.
  • CI for this exact head is not attached; pinned core correctness and AI code hygiene my-review passes found no actionable defects. Older results below are historical.

Closes #427.

Change

  • Route a thrown value through the exception-directed CFG edge to the nearest catch block.
  • Keep the current stack frame until the catch binding reads the thrown value. If no handler exists, unwind to the caller and check its call site for a handler.
  • Preserve unresolved throw expressions as unresolved instead of inventing an undefined exception.
  • Pin JacoDB to 7a2cda3bfd9175ba11a60e47ff4a32e6e3e209e2 from [TS] Preserve exceptional CFG edges for try/catch jacodb#393, which supplies exceptional CFG edges and CaughtExceptionRef.

Verification

  • Focused Exceptions and TsCatchRoutingTest passed with a clean local composite build of that exact JacoDB commit.
  • TsCatchRoutingTest uses ordinary analyzeWithOutcome, requires EXHAUSTED with no unsupported paths, checks both conditional branches, catch bindings, nested catch and rethrow, and exceptions from a callee. Generated witnesses replay in Node.js.
  • Full :usvm-ts:test: 1105 tests, 0 failures/errors, 143 skipped. The final rethrow regression was then run separately and passed.
  • Local :usvm-ts:detektMain and :usvm-ts:detektTest pass with zero findings. Full CI run 37080042969 passed all six jobs on head e0bc56ad09df3af083772057992e5feb683c2a17.
  • A pinned my-review hygiene pass on 2d655b84 found duplicate Node process handling; 253e55a7 removes it without changing catch-specific script assertions. The repository pre-commit hook invokes a missing checkLicense task, so this follow-up commit bypassed that hook after the focused test, Detekt, and git diff --check passed.

Stack

Implement supported string equality cases and preserve explicit unsupported outcomes for unbacked symbolic witnesses. Reuse shared Node replay tests.
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/ts-422-string-value-equality branch from 7927e93 to 127ecb5 Compare October 3, 2026 05:21
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/ts-427-catch-routing branch from e0bc56a to 2d655b8 Compare October 3, 2026 05:28
Keep catch witness assertions and use the shared Node process harness.
@CaelmBleidd
CaelmBleidd marked this pull request as ready for review October 3, 2026 06:44
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/ts-422-string-value-equality branch from e5527a3 to 7217c2a Compare October 4, 2026 19:51
Base automatically changed from caelmbleidd/ts-422-string-value-equality to main October 5, 2026 12:37
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.

2 participants