[TS Calls] Add reproducible unknown-call census

usvm-ts/build.gradle.kts

@@ -8,6 +8,7 @@ import kotlin.time.Duration
 
 plugins {
     id("usvm.kotlin-conventions")
+    kotlin("plugin.serialization") version Versions.kotlin
 }
 
 dependencies {
@@ -21,6 +22,7 @@ dependencies {
     implementation(Libs.ksmt_cvc5)
     implementation(Libs.ksmt_symfpu)
     implementation(Libs.ksmt_runner)
+    implementation(Libs.kotlinx_serialization_json)
 
     testImplementation(Libs.mockk)
     testImplementation(Libs.junit_jupiter_params)
@@ -32,6 +34,14 @@ dependencies {
     testImplementation("org.burningwave:core:12.62.7")
 }
 
+tasks.register<JavaExec>("runUnknownCallCensus") {
+    group = "verification"
+    description = "Runs or summarizes the TypeScript unknown-call census."
+    workingDir(rootProject.projectDir)
+    classpath = sourceSets.main.get().runtimeClasspath
+    mainClass.set("org.usvm.census.UnknownCallCensusCliKt")
+}
+
 val generateSdkIR by tasks.registering {
     group = "build"
     description = "Generates SDK IR using ArkAnalyzer."

usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md

@@ -0,0 +1,44 @@
+# Finite development model selection
+
+Selection was frozen on 2026-09-19 before any held-out TS Calls evaluation. This is a development decision from a three-project pilot, not evidence that the selected models improve coverage.
+
+## Evidence used
+
+- Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`.
+- The frozen development manifest in `development-corpus.json` and the primary `EMPTY_FRESH` census at tool commit `c1e07845c393374f743220dfe7febb4bc208c3b4`, tree `bc524f2b9ba451b378db1bce362722a7b534c931`. It analyzed 97 entry functions from three pinned projects: 45 completed, 36 ended with explicit partial-analysis diagnostics, 16 reached the 30-second method timeout, and none ended with a boundary tool error. It observed 7,002 repeated events at 36 stable source sites in 26 containing functions.
+- The sample covered 11 source files in TheAlgorithms/TypeScript, 37 in javascript-datastructures-algorithms, and 14 in typescript-collections. Stable sites were distributed 9, 7, and 20 across those projects. This replaces the obsolete lexicographic/BFS run, whose result is diagnostic only and is excluded from selection evidence.
+- Stable-source-site prevalence rather than repeated loop-event totals. The largest groups were iterator `Symbol.iterator` and `next` (4 sites each), `Error` construction (4), `Object.keys` (3), iterator `has` (3), and the project callback `Heap.compare` (3). Built-in array `pop` occurred at one source site; no built-in `Array.shift` site was observed. The 1,918 repeated `pop` events and 3,630 repeated `FactoryDictionary.defaultFactoryFunction` events arise from repeated exploration and must not be read as independent prevalence observations.
+
+The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. The 36 partial analyses, 16 timeouts, three-project scope, and omitted call-resolution candidate tails limit prevalence interpretation. Additional development projects must be pinned before their results are inspected; held-out projects remain separate and cannot influence model selection.
+
+## Decision
+
+The finite modeled set is exactly:
+
+```text
+ts.array.pop
+ts.array.shift
+```
+
+The control set is empty. Both existing models were implemented before this census and are retained as the bounded EtsIR-body and symbolic-memory-intrinsic mechanism pair from #368. They must not be described as census-selected. Their common experiment domain is the narrow dense, ordinary, mutable one-dimensional array domain in the #368 audit. Calls outside that admitted domain remain residual.
+
+No new model family is admitted for the pilot:
+
+- Application callbacks and dispatch limitations such as `BSTreeKV.compare` require shared call-resolution work, not optional treatment models.
+- The corrected array `pop` observation confirms one development source site for the already selected mechanism. It does not retrospectively make that pre-census model census-selected.
+- Iterator `next` needs stateful iterator representation and completion/alias validation.
+- `Array.isArray` has one stable development site and still needs proven target provenance plus rank/proxy bounds.
+- The remaining scattered standard calls do not establish both prevalence and a reviewed bounded semantic contract.
+
+This is an acceptable no-new-family result. A later family requires a separate bounded implementation task, original-JavaScript validation, and a refrozen model set before held-out outcomes are inspected.
+
+## Content identity
+
+At accepted #380 source `3134d06515bca61ba2a357a67697ac8620b0e420`:
+
+- `ArrayModels.ts` source SHA-256: `9f40d3abce58e3412a0206eabd9fdb0547e12c2ebd832ce48b260b3339518e26`.
+- `TsArrayShiftIntrinsicModel.kt` SHA-256: `ff6dd634cf660c83e203b82c927a28e88859f0bc6b9f24bec2fa97d738dc9e11`.
+
+The accepted run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, `CLOSEST_TO_UNCOVERED_RANDOM`, no coverage-based early stop, a 900-second project budget, and a 30-second method budget. A class qualified when it had at least one ordinary method with at least eight IR statements. Up to 40 classes and 40 methods were selected per project by stable seeded ranks and class round-robin. The raw artifact SHA-256 is `a091dff2d393e131a83e76cc71af51dd38dcd821e2e01ee007cfe8aa56ab6c08`; the generated and standalone-regenerated summaries are byte-identical with SHA-256 `7c59fbfa09af54de1e74ed65f4c762629013688d109305a970b421ee32781d00`; the manifest SHA-256 is `4adba5861339782e1f514f01525561a67aa9f01a6abe914b3d371ff77e1c1bbb`.
+
+Run metadata records `unknownCallModelSelection` as `NONE`. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented.

usvm-ts/experiments/unknown-call-census/README.md

@@ -0,0 +1,21 @@
+# TypeScript unknown-call development census
+
+This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` entry files, excludes declarations and common test suffixes, and excludes synthetic anonymous and initializer entry methods. A class is eligible when it contains at least `minMethodsPerClass` methods with at least `minStatementsPerMethod` IR statements. That threshold qualifies the class but does not discard its shorter ordinary methods. Eligible classes and their methods are ordered by stable SHA-256 ranks derived from the manifest seed and repository-relative identities. Methods are then taken round-robin across the selected classes, so `maxMethods` does not collapse the sample onto the first large class. The execution scene retains every loaded support file. Unknown calls reached inside nested source functions retain their actual containing-function identity.
+
+The three-project manifest is a reproducible development pilot, not the final corpus. Extend it by pinning additional projects and changing the seed or limits before inspecting their census results. Freeze that expanded development manifest before using it to revise the model catalog. Keep held-out evaluation projects in a separate manifest and never use their outcomes to choose models or tune these thresholds.
+
+The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Search uses `CLOSEST_TO_UNCOVERED_RANDOM` with the manifest seed and does not stop merely because the entry method reaches 100% statement coverage. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. A stable source site can contain multiple lowered IR calls; raw records retain the statement index and callee identity. Method results distinguish analysis that returned normally from partial analysis stopped by an engine or recording failure; a normal return does not claim exhaustive behavior outside the configured budgets and engine semantics. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected.
+
+Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in `development-corpus.json`, then run:
+
+```sh
+./gradlew :usvm-ts:runUnknownCallCensus --args='census --manifest usvm-ts/experiments/unknown-call-census/development-corpus.json --checkout-root /absolute/path/to/checkouts --output /absolute/path/to/results'
+```
+
+The command refuses a checkout whose Git `HEAD` differs from the manifest or whose working tree contains tracked or untracked changes. It creates `raw.jsonl` without overwriting prior evidence, writes records incrementally, and creates `summary.json`. Use a new output directory for every run. Regenerate the summary without rerunning symbolic execution using:
+
+```sh
+./gradlew :usvm-ts:runUnknownCallCensus --args='summarize --input /absolute/path/to/results/raw.jsonl --output /absolute/path/to/results/summary.json'
+```
+
+`EMPTY_STOP` can be added as a separate profile when stopping-site counts are needed. Do not combine its counts with the primary `EMPTY_FRESH` profile.

usvm-ts/experiments/unknown-call-census/development-corpus.json

@@ -0,0 +1,78 @@
+{
+  "schemaVersion": 2,
+  "projects": [
+    {
+      "id": "the-algorithms-typescript",
+      "repository": "https://github.com/TheAlgorithms/TypeScript.git",
+      "revision": "19b4ced86c99815f142d4a46a028f55487b8038a",
+      "path": "TheAlgorithms-TypeScript",
+      "license": "MIT",
+      "licenseFile": "LICENSE",
+      "include": [
+        "maths",
+        "search",
+        "sorts",
+        "bit_manipulation",
+        "dynamic_programming"
+      ],
+      "includeSuffixes": [
+        ".ts"
+      ],
+      "excludeSuffixes": [
+        ".test.ts",
+        ".spec.ts",
+        ".d.ts"
+      ]
+    },
+    {
+      "id": "javascript-datastructures-algorithms",
+      "repository": "https://github.com/loiane/javascript-datastructures-algorithms.git",
+      "revision": "e8ee8f9b8a07589533c4243a210d4cea7b090b10",
+      "path": "javascript-datastructures-algorithms",
+      "license": "MIT",
+      "licenseFile": "LICENSE",
+      "include": [
+        "src"
+      ],
+      "includeSuffixes": [
+        ".ts"
+      ],
+      "excludeSuffixes": [
+        ".test.ts",
+        ".spec.ts",
+        ".d.ts"
+      ]
+    },
+    {
+      "id": "typescript-collections",
+      "repository": "https://github.com/basarat/typescript-collections.git",
+      "revision": "309bb1b6955b403b212309531607b8d17df152e5",
+      "path": "typescript-collections",
+      "license": "MIT",
+      "licenseFile": "LICENSE",
+      "include": [
+        "src/lib"
+      ],
+      "includeSuffixes": [
+        ".ts"
+      ],
+      "excludeSuffixes": [
+        ".test.ts",
+        ".spec.ts",
+        ".d.ts"
+      ]
+    }
+  ],
+  "profiles": [
+    "EMPTY_FRESH"
+  ],
+  "randomSeed": 0,
+  "limits": {
+    "projectTimeoutSeconds": 900,
+    "methodTimeoutSeconds": 30,
+    "maxClasses": 40,
+    "maxMethods": 40,
+    "minMethodsPerClass": 1,
+    "minStatementsPerMethod": 8
+  }
+}

usvm-ts/src/main/kotlin/org/usvm/census/CensusMethodSelection.kt

@@ -0,0 +1,98 @@
+package org.usvm.census
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
+import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME
+import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
+import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
+import java.nio.file.Path
+
+internal fun selectCensusMethods(
+    manifest: UnknownCallCensusManifest,
+    project: UnknownCallCensusProject,
+    projectRoot: Path,
+    loadedFiles: LoadedProjectFiles,
+): CensusMethodSelection {
+    val candidateFiles = loadedFiles.files.asSequence()
+        .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) }
+        .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) }
+        .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) }
+        .distinctBy { (_, fileName) -> fileName }
+        .sortedBy { (_, fileName) -> fileName }
+        .map { (file, _) -> file }
+        .toList()
+
+    val eligibleClasses = candidateFiles
+        .flatMap { file -> file.allClasses }
+        .map { clazz ->
+            val classId = classId(project.id, projectRoot, clazz.signature, loadedFiles.pathsBySignature)
+            val methods = clazz.methods
+                .asSequence()
+                .filterNot { method -> method.cfg.stmts.isEmpty() }
+                .filterNot { method -> method.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
+                .filterNot { method -> method.name == DEFAULT_ARK_METHOD_NAME }
+                .filterNot { method -> method.name == INSTANCE_INIT_METHOD_NAME }
+                .filterNot { method -> method.name == STATIC_INIT_METHOD_NAME }
+                .sortedWith(
+                    compareBy(
+                        { method ->
+                            stableSelectionRank(
+                                seed = manifest.randomSeed,
+                                identity = functionId(
+                                    project.id,
+                                    projectRoot,
+                                    method.signature,
+                                    loadedFiles.pathsBySignature,
+                                ),
+                            )
+                        },
+                        { method ->
+                            functionId(
+                                project.id,
+                                projectRoot,
+                                method.signature,
+                                loadedFiles.pathsBySignature,
+                            )
+                        },
+                    )
+                )
+                .toList()
+
+            SelectedClass(classId = classId, methods = methods)
+        }
+        .filter { selectedClass ->
+            selectedClass.methods.count { method ->
+                method.cfg.stmts.size >= manifest.limits.minStatementsPerMethod
+            } >= manifest.limits.minMethodsPerClass
+        }
+
+    val selectedClasses = eligibleClasses
+        .sortedWith(
+            compareBy(
+                { selectedClass -> stableSelectionRank(manifest.randomSeed, selectedClass.classId) },
+                SelectedClass::classId,
+            )
+        )
+        .take(manifest.limits.maxClasses)
+    val selectedMethods = roundRobin(selectedClasses.map(SelectedClass::methods))
+        .take(manifest.limits.maxMethods)
+
+    return CensusMethodSelection(
+        candidateFiles = candidateFiles.size,
+        eligibleClasses = eligibleClasses.size,
+        selectedClasses = selectedClasses.size,
+        methods = selectedMethods,
+    )
+}
+
+private data class SelectedClass(
+    val classId: String,
+    val methods: List<EtsMethod>,
+)
+
+internal data class CensusMethodSelection(
+    val candidateFiles: Int,
+    val eligibleClasses: Int,
+    val selectedClasses: Int,
+    val methods: List<EtsMethod>,
+)