Skip to content

Share TypeScript analysis and UTF-16 infrastructure between PBT and Calls - #412

Open
CaelmBleidd wants to merge 1 commit into
caelmbleidd/pbt-382-branch-feedbackfrom
caelmbleidd/shared-ts-engine-infrastructure
Open

CaelmBleidd wants to merge 1 commit into
caelmbleidd/pbt-382-branch-feedbackfrom
caelmbleidd/shared-ts-engine-infrastructure

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 1, 2026 •

Copy link
Copy Markdown
Member

PBT and Calls had diverged at the TypeScript machine boundary: each configured inputs differently, PBT added observation/completion hooks, and its string work duplicated the existing Calls engine. This PR makes those facilities reusable on top of the existing builtin models and exact-coverage stack.

  • Preserve the Calls constructor configuration and sort overrides, add PBT's per-analysis configuration, and run both before the initial solver query. Keep the existing analyze and analyzeWithOutcome entry points.
  • Expose pre-call and completed-assignment observations without replaying an event when a call returns. Report timeout, suppressed interpreter failure, stopped default-dispatcher residual calls, and runtime limitations separately, resetting observations between analyses. Custom dispatchers retain ownership of their own telemetry.
  • Add common bounded UTF-16 string allocation/model decoding to StringStorage. Calls now uses the allocator; the PBT adapter can use the same API. Preserve Calls input snapshots so later heap changes cannot rewrite the original witness.
  • Escape surrogate code units at JSON text/UTF-8 boundaries in the shared manifest codec, Calls outputs/replay and FastCheck clients/CLI. Preserve tagged values and ordinary JsonElement roundtrips. Send dataflow logging to stderr.

Existing string, numeric, Array, Date and Error models remain authoritative. PBT-specific entry guards, property search, observations, feedback scheduling and unfinished campaign/loader changes are outside this PR.

Review order: #391 → #410 → #394 → #409 → this PR. The frontend companion UnitTestBot/jacodb#367 is merged; this PR pins its merge revision 86b07fc9fb. Its #366 catch-binding fix remains a separate open PR. No benchmark or manuscript result is changed.

Validation (local JDK 21):

  • 127 focused Kotlin tests passed across machine completion/hooks, shared string allocation/decoding, UTF-16 JSON, Calls symbolic inputs/models/replay/experiment output, FastCheck clients, and exact branch coverage.
  • All 73 Node adapter tests passed, including both exact coverage and local source closure suites retained in Map exact c8 TypeScript if arms to EtsIR coverage #409.
  • Detekt main/test passed with no findings in usvm-ts, usvm-ts-pbt, usvm-ts-calls, and usvm-ts-fast-check. The one-line ExprUtil change removes inherited implicit-name shadowing reported by that gate.
  • All four modules compiled test sources using the published JacoDB 86b07fc9fb dependency, without local substitution. All 28 completion/hooks/string, UTF-16 JSON, and source-replay tests also passed against that published dependency. The earlier focused tests used a composite JacoDB tree identical to the merged revision.
  • git diff --check passed.

Remote CI for 0f66e4f9 was dispatched manually because the PR base is not main: https://github.com/UnitTestBot/usvm/actions/runs/36856475983. All six CI jobs passed. The unchanged JVM dynamic timeout test failed on the first attempt and passed when that job alone was rerun on the same commit. These checks cover infrastructure behavior; they do not establish new campaign/benchmark outcomes or completion of the PBT feature migration.

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