[TS] Support the jacodb native TS parser (jacodb#361) in usvm-ts-pbt

CaelmBleidd · CaelmBleidd · commit fa39061524d4 · 2026-07-06T10:28:53.000+03:00
- follow the frontends' compare-to-zero truthiness idiom in the concrete
  interpreter: both ArkAnalyzer and the jacodb ts-frontend lower `if (x)` to
  `x != 0`, which differs from JS loose (in)equality for non-number operands
  ([] != 0 is false in JS, yet [] is truthy); compare-to-zero on a non-number
  now means ToBoolean
- whitelist two more confirmed engine divergences found by running the
  differential oracle under the second frontend: the NaN hole of the same
  idiom (undefined treated as truthy via ToNumber(undefined) != 0) and the
  doubly-ambiguous transitiveCoercionNoTypes
- add an opt-in composite-build switch (-PuseLocalJacodb[=&lt;path&gt;]) for
  substituting a locally built jacodb
- document the compatibility check (docs/ts-pbt/04)

Full usvm-ts-pbt suite is green under both EtsIR providers.
diff --git a/docs/ts-pbt/04-jacodb-native-parser-compat.md b/docs/ts-pbt/04-jacodb-native-parser-compat.md
@@ -0,0 +1,57 @@
+# Compatibility with the jacodb native TS parser (jacodb PR #361)
+
+> Research note. Date: 2026-07-06.
+
+## 1. Status: fully compatible
+
+jacodb PR #361 (`caelmbleidd/ts_native_parser`) adds `jacodb-ets/ts-frontend` — a
+TypeScript-compiler-based EtsIR producer replacing ArkAnalyzer — and reworks
+`LoadEtsFile.kt`: the provider is selected by `ETS_IR_PROVIDER`
+(`ts-frontend` (default) | `arkanalyzer`), with `ETS_FRONTEND_DIR` pointing at the
+built frontend (`npm run build` → `dist/index.js`; the CLI is flag-compatible with
+`serializeArkIR`). The `loadEtsFileAutoConvert`-family signatures are unchanged, so
+**usvm-ts-pbt requires no code changes**.
+
+Verified end-to-end: usvm built with the PR-branch jacodb substituted via the new
+opt-in composite build (`./gradlew -PuseLocalJacodb=<path> ...`, see
+`settings.gradle.kts`), full usvm-ts-pbt suite (29 tests incl. the differential
+oracle and hybrid e2e) is green under **both** providers.
+
+## 2. Findings from cross-frontend differential testing
+
+Running the same differential oracle under the second frontend immediately
+yielded new results — cross-frontend differential testing is itself a method:
+
+1. **The compare-to-zero truthiness idiom is ambiguous IR.** Both frontends lower
+   `if (x)` to the ConditionExpr `x != 0` — byte-identical to a genuine
+   source-level `x != 0` loose comparison. The two differ in JS for non-number
+   operands (`[] != 0` is *false*, yet `[]` is truthy; `undefined != 0` is *true*,
+   yet `undefined` is falsy). The concrete interpreter now follows the idiom
+   contract (compare-to-zero on a non-number operand = ToBoolean), documented in
+   `EtsConcreteInterpreter`.
+   *Feedback for #361: a dedicated truthiness ConditionExpr op would remove the
+   ambiguity.*
+2. **The engine falls into the NaN hole of the same idiom**: it evaluates
+   `x != 0` numerically, so for `x = undefined` it derives
+   `ToNumber(undefined) = NaN != 0 → true` and treats `undefined` as *truthy*
+   (`And.andOfUnknown(0, undefined)`: engine 21, JS 0). Whitelisted; engine issue.
+3. `TypeCoercion.transitiveCoercionNoTypes` is doubly ambiguous: a genuine
+   `c != 0` comparison (idiom-indistinguishable) plus the engine's non-JS `&&`
+   on references; JS gives 2, engine 1, concrete 4. Whitelisted.
+
+## 3. How to run against the native parser
+
+```bash
+cd <jacodb>/jacodb-ets/ts-frontend && npm install && npm run build
+cd <usvm>
+export ETS_IR_PROVIDER=ts-frontend
+export ETS_FRONTEND_DIR=<jacodb>/jacodb-ets/ts-frontend
+./gradlew -PuseLocalJacodb=<jacodb> :usvm-ts-pbt:test
+```
+
+(The `ARKANALYZER_DIR`-gated tests still require the variable to be *set* until
+the enabling condition is made provider-aware; its value is unused by the native
+provider.) Once #361 is merged and usvm bumps the jacodb pin, `-PuseLocalJacodb`
+becomes unnecessary and the native parser works out of the box — including for the
+open-source-corpus benchmark infrastructure, which eliminates the per-file
+ArkAnalyzer/Node round-trip fragility on large corpora.
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -56,18 +56,23 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
 // Actually, relative path is enough, but there is a bug in IDEA when the path is a symlink.
 // As a workaround, we convert it to a real absolute path.
 // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
-// val jacodbPath = file("jacodb").takeIf { it.exists() }
-//     ?: file("../jacodb").takeIf { it.exists() }
-//     ?: error("Local JacoDB directory not found")
-// includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
-//     dependencySubstitution {
-//         all {
-//             val requested = requested
-//             if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
-//                 val targetProject = ":${requested.module}"
-//                 useTarget(project(targetProject))
-//                 logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
-//             }
-//         }
-//     }
-// }
+// Opt-in local JacoDB substitution: -PuseLocalJacodb[=<path>] (default: ./jacodb or ../jacodb)
+if (extra.has("useLocalJacodb")) {
+    val prop = extra.get("useLocalJacodb")?.toString()
+    val jacodbPath = prop?.takeIf { it.isNotBlank() && it != "true" }?.let { file(it) }
+        ?: file("jacodb").takeIf { it.exists() }
+        ?: file("../jacodb").takeIf { it.exists() }
+        ?: error("Local JacoDB directory not found")
+    includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
+        dependencySubstitution {
+            all {
+                val requested = requested
+                if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
+                    val targetProject = ":${requested.module}"
+                    useTarget(project(targetProject))
+                    logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
+                }
+            }
+        }
+    }
+}
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/EtsConcreteInterpreter.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/EtsConcreteInterpreter.kt
@@ -265,9 +265,29 @@ class EtsConcreteInterpreter(
                 VNumber((a ushr b).toDouble())
             }
 
-            // Binary: relational
-            is EtsEqExpr -> VBool(JsSemantics.looseEq(eval(e.left, frame), eval(e.right, frame)))
-            is EtsNotEqExpr -> VBool(!JsSemantics.looseEq(eval(e.left, frame), eval(e.right, frame)))
+            // Binary: relational.
+            //
+            // NOTE on the compare-to-zero idiom: both frontends (ArkAnalyzer and the
+            // jacodb ts-frontend) lower `if (x)` to the ConditionExpr `x != 0`, which
+            // is NOT equivalent to JS loose inequality for non-number operands
+            // (`[] != 0` is false in JS, yet `[]` is truthy). The IR is ambiguous:
+            // a genuine source-level `x != 0` produces the same shape. We follow the
+            // IR contract: compare-to-zero on a non-number operand means ToBoolean.
+            is EtsEqExpr ->
+                if (isZeroConstant(e.right)) {
+                    val l = eval(e.left, frame)
+                    if (l is VNumber) VBool(l.value == 0.0) else VBool(!JsSemantics.truthy(l))
+                } else {
+                    VBool(JsSemantics.looseEq(eval(e.left, frame), eval(e.right, frame)))
+                }
+
+            is EtsNotEqExpr ->
+                if (isZeroConstant(e.right)) {
+                    val l = eval(e.left, frame)
+                    if (l is VNumber) VBool(l.value != 0.0) else VBool(JsSemantics.truthy(l))
+                } else {
+                    VBool(!JsSemantics.looseEq(eval(e.left, frame), eval(e.right, frame)))
+                }
             is EtsStrictEqExpr -> VBool(JsSemantics.strictEq(eval(e.left, frame), eval(e.right, frame)))
             is EtsStrictNotEqExpr -> VBool(!JsSemantics.strictEq(eval(e.left, frame), eval(e.right, frame)))
             is EtsLtExpr -> VBool(JsSemantics.lt(eval(e.left, frame), eval(e.right, frame)))
@@ -302,6 +322,9 @@ class EtsConcreteInterpreter(
         private fun parameterIndexOfLocal(frame: Frame, name: String): Int? =
             frame.method.parameters.firstOrNull { it.name == name }?.index
 
+        private fun isZeroConstant(e: EtsEntity): Boolean =
+            e is EtsNumberConstant && e.value == 0.0
+
         private inline fun numeric(
             left: EtsEntity,
             right: EtsEntity,
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt
@@ -67,6 +67,15 @@ class ConcreteVsSymbolicDifferentialTest {
      *   relational operators per sort pair (`Lt.onBool = !lhs && rhs`, see
      *   TsBinaryOperator.Lt) instead of the JS ToNumber coercion, so e.g.
      *   `false < 0.0` is reported `true` while JS gives `0 < 0 === false`.
+     * - `And.andOfUnknown`: frontends lower `if (x)` to the idiom `x != 0`; the
+     *   engine evaluates it numerically, so for `x = undefined` it gets
+     *   `ToNumber(undefined) = NaN != 0 -> true` while `undefined` is falsy in JS
+     *   (the NaN hole of the compare-to-zero truthiness contract).
+     * - `TypeCoercion.transitiveCoercionNoTypes`: doubly ambiguous — the *genuine*
+     *   source-level `c != 0` loose comparison is indistinguishable in the IR from
+     *   the truthiness idiom (the concrete interpreter follows the idiom contract),
+     *   and the engine's `&&` on references diverges from JS anyway
+     *   (JS gives 2, engine 1, concrete 4).
      *
      * NOTE: requires the CI-pinned ArkAnalyzer (`neo/2025-09-03`). Older/newer AA
      * builds may emit a different if-successor order in the DTO, which inverts
@@ -75,6 +84,8 @@ class ConcreteVsSymbolicDifferentialTest {
     private val knownEngineDivergences: Set<String> = setOf(
         "Add.addUnknownValues",
         "Less.lessUnknown",
+        "And.andOfUnknown",
+        "TypeCoercion.transitiveCoercionNoTypes",
     )
 
     private fun runDifferential(resourcePath: String, className: String): Verdict {
