UnitTestBot · CaelmBleidd · Jul 5, 2026 · Jul 5, 2026 · Jul 5, 2026 · Jul 5, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -149,10 +149,16 @@ jobs:
           cd $DEST_DIR
 
           npm install
+          # Transitively hoisted @types/node >= 24 uses TypeScript syntax that the
+          # ArkAnalyzer toolchain cannot parse; pin a compatible version. Both
+          # --no-save packages must be installed in one command: each `npm install`
+          # re-resolves the tree and drops previous --no-save additions
+          # (ohos-typescript is installed --no-save by the postinstall script).
+          npm install --no-save @types/node@22 arktools/lib/ohos-typescript-4.9.5-r4-OpenHarmony-v5.0.0-Release.tgz
           npm run build
 
       - name: Run TS tests
-        run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check
+        run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check :usvm-ts-pbt:check
 
       - name: Upload Gradle reports
         if: (!cancelled())

diff --git a/build.gradle.kts b/build.gradle.kts
@@ -22,6 +22,7 @@ tasks.register("validateProjectList") {
             project(":usvm-python"),
             project(":usvm-ts"),
             project(":usvm-ts-dataflow"),
+            project(":usvm-ts-pbt"),
         )
 
         // Gather the actual subprojects from the current root project.

diff --git a/detekt/baselines/usvm-ts-pbt-Main.yml b/detekt/baselines/usvm-ts-pbt-Main.yml
@@ -0,0 +1,87 @@
+<?xml version="1.0" ?>
+<SmellBaseline>
+  <ManuallySuppressedIssues></ManuallySuppressedIssues>
+  <CurrentIssues>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}")</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame)))</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(left, frame))</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(right, frame))</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(left, frame)</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(op(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame))).toDouble())</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(right, frame)</ID>
+    <ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(target)</ID>
+    <ID>BracesOnWhenStatements:ConstantMiner.kt$MinedConstants.Companion$when</ID>
+    <ID>BracesOnWhenStatements:Conversions.kt$when</ID>
+    <ID>BracesOnWhenStatements:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$when</ID>
+    <ID>BracesOnWhenStatements:Generators.kt$InputGenerator$when</ID>
+    <ID>BracesOnWhenStatements:Intrinsics.kt$Intrinsics$when</ID>
+    <ID>BracesOnWhenStatements:JsSemantics.kt$JsSemantics$when</ID>
+    <ID>BracesOnWhenStatements:Main.kt$when</ID>
+    <ID>BracesOnWhenStatements:PbtPhase.kt$PbtPhase$when</ID>
+    <ID>EmptyFunctionBlock:CoverageTracker.kt$CoverageTracker${}</ID>
+    <ID>Filename:ConstantMiner.kt$org.usvm.ts.pbt.gen.ConstantMiner.kt</ID>
+    <ID>Filename:Generators.kt$org.usvm.ts.pbt.gen.Generators.kt</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println( " ${m.method}: stmt=%.1f%%, branch=%.1f%% (pbt: %s, symbolic: %s), %d ms".format( m.stmtCoverage * 100, m.branchCoverage * 100, m.pbt?.let { "${it.executions} runs, ${it.failures.size} failures" } ?: "-", m.symbolic?.let { "${it.reached}/${it.targets.size} targets" } ?: "-", m.totalWallMs, ) )</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println("Analyzing ${methods.size} method(s) in mode $mode...")</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println("Loading ${files.size} file(s) via ArkAnalyzer...")</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println("Report written to $out")</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println("Unknown option: ${args[i]}\n$USAGE")</ID>
+    <ID>ForbiddenMethodCall:Main.kt$println(USAGE)</ID>
+    <ID>LoopWithTooManyJumpStatements:PbtPhase.kt$PbtPhase$while</ID>
+    <ID>MagicNumber:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$31</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$0.0</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$0.6</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$10</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$100</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$1000</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$1001</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$101</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$11</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$1e6</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$3</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$4</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$5</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$6</ID>
+    <ID>MagicNumber:Generators.kt$InputGenerator$8</ID>
+    <ID>MagicNumber:Intrinsics.kt$Intrinsics$9007199254740991.0</ID>
+    <ID>MagicNumber:JsSemantics.kt$JsSemantics$0xFFFFFFFFL</ID>
+    <ID>MagicNumber:JsSemantics.kt$JsSemantics$16</ID>
+    <ID>MagicNumber:JsSemantics.kt$JsSemantics$1e21</ID>
+    <ID>MagicNumber:JsSemantics.kt$JsSemantics$8</ID>
+    <ID>MagicNumber:JsSemantics.kt$JsSemantics$9.007199254740992E15</ID>
+    <ID>MagicNumber:Main.kt$100</ID>
+    <ID>MagicNumber:Main.kt$20</ID>
+    <ID>MagicNumber:Main.kt$2_000</ID>
+    <ID>MagicNumber:PbtPhase.kt$PbtPhase$100</ID>
+    <ID>MagicNumber:SymbolicPhase.kt$SymbolicPhase$1_000_000</ID>
+    <ID>MatchingDeclarationName:ConstantMiner.kt$MinedConstants</ID>
+    <ID>MatchingDeclarationName:Generators.kt$InputGenerator</ID>
+    <ID>MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$)</ID>
+    <ID>MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw typeError("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}")</ID>
+    <ID>MaximumLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$ </ID>
+    <ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VNamespace(e.name)</ID>
+    <ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VString(array.value[i.toInt()].toString())</ID>
+    <ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VUndefined</ID>
+    <ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw UnsupportedFeatureSignal("global ref: ${e.name}")</ID>
+    <ID>MultiLineIfElse:Generators.kt$InputGenerator$genAny(depth)</ID>
+    <ID>MultiLineIfElse:Generators.kt$InputGenerator$generate(type.types[random.nextInt(type.types.size)], depth)</ID>
+    <ID>MultiLineIfElse:Generators.kt$InputGenerator$random.nextDouble(-1e6, 1e6)</ID>
+    <ID>MultiLineIfElse:Generators.kt$InputGenerator$random.nextInt(-100, 101) + random.nextDouble()</ID>
+    <ID>MultiLineIfElse:JsSemantics.kt$JsSemantics$d.toLong().toString()</ID>
+    <ID>MultiLineIfElse:JsSemantics.kt$JsSemantics$java.math.BigDecimal(d).toBigInteger().toString()</ID>
+    <ID>MultiLineIfElse:PbtPhase.kt$PbtPhase$args</ID>
+    <ID>NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List&lt;VValue&gt;): VValue</ID>
+    <ID>NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame)</ID>
+    <ID>NestedBlockDepth:Shrinker.kt$Shrinker$fun shrink(args: List&lt;VValue&gt;, stillFails: (List&lt;VValue&gt;) -&gt; Boolean): List&lt;VValue&gt;</ID>
+    <ID>NoMultipleSpaces:Generators.kt$InputGenerator$ </ID>
+    <ID>SwallowedException:EtsConcreteInterpreter.kt$EtsConcreteInterpreter$e: StackOverflowError</ID>
+    <ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun evalCall(expr: EtsCallExpr, frame: Frame): VValue</ID>
+    <ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List&lt;VValue&gt;): VValue</ID>
+    <ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame)</ID>
+    <ID>TooGenericExceptionCaught:SymbolicPhase.kt$SymbolicPhase$e: Throwable</ID>
+    <ID>UnderscoresInNumericLiterals:Intrinsics.kt$Intrinsics$9007199254740991.0</ID>
+    <ID>Wrapping:Generators.kt$InputGenerator$;</ID>
+    <ID>Wrapping:Intrinsics.kt$Intrinsics$(</ID>
+    <ID>Wrapping:Intrinsics.kt$Intrinsics$;</ID>
+  </CurrentIssues>
+</SmellBaseline>
diff --git a/detekt/baselines/usvm-ts-pbt-Test.yml b/detekt/baselines/usvm-ts-pbt-Test.yml
@@ -0,0 +1,27 @@
+<?xml version="1.0" ?>
+<SmellBaseline>
+  <ManuallySuppressedIssues></ManuallySuppressedIssues>
+  <CurrentIssues>
+    <ID>ArgumentListWrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
+    <ID>ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = hints, hintFallback = false, )</ID>
+    <ID>ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = pbt.typeProfiler.toHints(), )</ID>
+    <ID>BracesOnWhenStatements:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$when</ID>
+    <ID>CommentSpacing:LoadEts.kt$//-----------------------------------------------------------------------------</ID>
+    <ID>ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println(" MISMATCH: $it")</ID>
+    <ID>ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
+    <ID>ForbiddenMethodCall:HybridE2eTest.kt$HybridE2eTest$println( "[ablation] with hints: steps=${withHints.steps}, reached=${withHints.reached}, " + "wallMs=${withHints.wallMs}; without: steps=${withoutHints.steps}, " + "reached=${withoutHints.reached}, wallMs=${withoutHints.wallMs}" )</ID>
+    <ID>ImportOrdering:ConcreteInterpreterDslTest.kt$import org.jacodb.ets.dsl.add import org.jacodb.ets.dsl.and import org.jacodb.ets.dsl.const import org.jacodb.ets.dsl.eqq import org.jacodb.ets.dsl.gt import org.jacodb.ets.dsl.local import org.jacodb.ets.dsl.lt import org.jacodb.ets.dsl.mul import org.jacodb.ets.dsl.neg import org.jacodb.ets.dsl.param import org.jacodb.ets.dsl.program import org.jacodb.ets.dsl.sub import org.jacodb.ets.dsl.toBlockCfg import org.jacodb.ets.dsl.ProgramBuilder import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.toEtsBlockCfg import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test</ID>
+    <ID>MaxLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
+    <ID>MaximumLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$ </ID>
+    <ID>MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$compared++</ID>
+    <ID>MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$mismatches += "$ctx: concrete threw ${result.value}, symbolic returned ${test.returnValue}"</ID>
+    <ID>NestedBlockDepth:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$private fun runDifferential(resourcePath: String, className: String): Verdict</ID>
+    <ID>NoMultipleSpaces:JsSemanticsTest.kt$JsSemanticsTest$ </ID>
+    <ID>SwallowedException:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$e: Throwable</ID>
+    <ID>UnderscoresInNumericLiterals:HybridE2eTest.kt$HybridE2eTest$49382.0</ID>
+    <ID>UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295.0</ID>
+    <ID>UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295L</ID>
+    <ID>Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$(</ID>
+    <ID>Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$;</ID>
+  </CurrentIssues>
+</SmellBaseline>
diff --git a/docs/ts-pbt/00-project-state.md b/docs/ts-pbt/00-project-state.md
@@ -0,0 +1,106 @@
+# Project state: hybrid PBT + symbolic execution for TS (handoff document)
+
+> Last updated: 2026-07-08. **Read this first** when resuming work.
+> Context: prototype for the PhD "Гибридные методы анализа динамических
+> языков программирования" and the accompanying paper.
+
+## 1. Branch map (all pushed to origin)
+
+| Branch | Purpose | Contents |
+|---|---|---|
+| `caelmbleidd/ts_pbt` (**PR #341**) | The PBT/hybrid prototype | `usvm-ts-pbt` module, minimal usvm-ts extensions that belong to the feature (input type hints in `getInitialState`, `TsTestResolver` promotion + `resolveInputs`), benchmark infra, research notes `docs/ts-pbt/0*` |
+| `caelmbleidd/pbt_article` | The paper | = ts_pbt + `docs/ts-pbt/paper/` (acmart LaTeX; `latexmk -pdf main.tex`) |
+| `caelmbleidd/ts-interpreter-fixes` | Engine fixes, **kept separate from PBT by agreement** (base: master @ dab6d432) | mock unresolved virtual calls instead of killing the state; inc/dec unary expressions in TsExprResolver |
+
+Policy: PBT work goes to `ts_pbt`; engine (usvm-ts machine) fixes go ONLY to
+`ts-interpreter-fixes`; paper text goes to `pbt_article` (rebase it on ts_pbt
+as needed). Never mix engine fixes into ts_pbt.
+
+## 2. Current results (reproducible via benchmarks/run-project.sh)
+
+TheAlgorithms/TypeScript `maths` (62 methods, 264 branch edges, seed 0,
+pbt-iterations 1000, target-timeout 10 s, ts-frontend provider):
+
+| Mode | Branch % | Wall s | Notes |
+|---|---|---|---|
+| PBT only | 78.0 | 6.3 | |
+| Symbolic only | 63.1 → 64.7 | ~306 | second number = with the inc/dec engine fix |
+| Hybrid | **83.0** | 156 | 13/58 residual targets reached |
+| Hybrid + hints | 83.0 | 307 | 45 fallbacks (residual is engine-hard, hints can't help there) |
+
+loiane/javascript-datastructures-algorithms `src` (307 methods, 670 edges):
+PBT 62.5% @ 1.7 s; symbolic-only 57.2% @ 427 s; hybrid **75.1%** @ 243 s.
+Known issue there: replay-confirmed ≈ 0 for instance methods (see backlog).
+
+History: hybrid on maths was 64% before the engine mock-fix + interpreter
+extensions (notes 02/03 tell the diagnosis story — useful for the paper).
+
+## 3. In-flight / external dependencies
+
+- **usvm PR #341** (ts_pbt): CI was fixed (validateProjectList + @types/node
+  pin for the AA build + `:usvm-ts-pbt:check` in ci-ts) but the run was NOT
+  re-verified after the last force-pushes — check `gh pr checks 341`.
+- **jacodb PR #361** (native ts-frontend): usvm-ts-pbt is verified compatible
+  (note 04). Until merged + usvm pin bump, use
+  `./gradlew -PuseLocalJacodb=<jacodb-checkout>` and `ETS_IR_PROVIDER=ts-frontend`.
+- Local toolchain expectations: pinned ArkAnalyzer build (`neo/2025-09-03`)
+  at `~/Programming/arkanalyzer-neo-2025-09-03`; jacodb checkout with the
+  ts-frontend at `~/Programming/jacodb` (branch `caelmbleidd/ts_native_parser`).
+
+## 4. Backlog
+
+**PBT side (ts_pbt):**
+1. Replay confirmation for instance methods: solver-synthesized `this`
+   objects rarely replay (TsClass -> VObject decode gaps) — investigate on
+   the datastructures corpus (`replay-confirmed: 1` out of 84 reached).
+2. Project-level scenes (load whole project instead of per-file) to resolve
+   cross-file imports — the largest `Unsupported` bucket on real corpora.
+3. Symbolic->PBT feedback loop: reached inputs as seeds for a mutation round.
+4. Fallback budgeting for type hints (skip the retry when the hinted run
+   timed out rather than proved UNSAT) — motivated by the ablation numbers.
+5. Mutation-based bug seeding over `org.jacodb.ets.dsl` for a mutation-score
+   experiment (paper).
+
+**Engine side (ts-interpreter-fixes only):**
+1. Unbounded recursion `StrictEq.resolveFakeObject <-> resolveBinaryOperator`
+   (stack overflow on fake-object comparisons; seen on corpus runs).
+2. The NaN hole of the compare-to-zero truthiness idiom: engine evaluates
+   `x != 0` numerically, so `undefined` becomes truthy (note 04 §2);
+   candidate fix: `mkTruthyExpr` for compare-to-zero on non-fp operands.
+3. `+` on references is approximated numerically (`null + {}` -> NaN instead
+   of string concat) — differential finding, whitelisted.
+4. Lt/logical operators on mixed fake-object sorts (whitelisted findings).
+5. Strings: `TsTestStateResolver` returns placeholder strings -> lossy replay.
+
+**Front-end findings to report upstream:**
+- ArkAnalyzer lowers `const old = x++` as `x := x + 1; old := x` (old gets the
+  NEW value) — lowering bug, documented in the ts-interpreter-fixes sample.
+- The `if (x)` -> `x != 0` idiom is ambiguous IR (indistinguishable from a
+  genuine loose comparison); suggested a dedicated truthiness ConditionExpr
+  for jacodb #361.
+
+## 5. Docs index
+
+- `usvm-ts-pbt/README.md` — module overview, architecture, env, pitfalls.
+- `usvm-ts-pbt/benchmarks/README.md` — one-command measurement pipeline.
+- `docs/ts-pbt/01-arkanalyzer-and-ets-ir.md` — front ends, EtsIR contract.
+- `docs/ts-pbt/02-concrete-interpreter-and-differential-findings.md` —
+  interpreter design; AA successor-order drift (the branch-inversion story).
+- `docs/ts-pbt/03-hybrid-pipeline.md` — pipeline, usvm-ts touch points,
+  stop/collect race, first corpus numbers.
+- `docs/ts-pbt/04-jacodb-native-parser-compat.md` — ts-frontend compat,
+  truthiness-idiom ambiguity, how to run with the native parser.
+- `docs/ts-pbt/paper/` (branch `pbt_article`) — the paper; numbers in
+  Table 1 come from `benchmarks/results/maths2-*.json`-style runs.
+
+## 6. Quick sanity commands
+
+```bash
+export ARKANALYZER_DIR=~/Programming/arkanalyzer-neo-2025-09-03
+./gradlew :usvm-ts-pbt:test --rerun-tasks          # 29 tests, expect 0 failures
+./gradlew :usvm-ts:test --rerun-tasks              # 422+ tests, expect 0 failures
+cd usvm-ts-pbt/benchmarks && ./run-project.sh TheAlgorithms-TypeScript --include maths
+```
+
+Remember `--rerun-tasks` whenever env vars (providers) change — Gradle does
+not track them.