Concolic for TypeScript#341
Draft
CaelmBleidd wants to merge 10 commits into
Draft
Conversation
Prepare usvm-ts for hybrid (concrete + symbolic) analysis: - add TsInputTypeHints / TsHintType and TsOptions.inputTypeHints: observed-type profiles from a dynamic phase restrict fake-object type discriminators for parameters with unresolved types in getInitialState (an unsound prune with an orchestrator-level hint-free fallback; default EMPTY keeps behavior unchanged) - add TsTestResolver.resolveInputs to resolve the input valuation of states that have not terminated yet (e.g. captured at target propagation time) - move TsTestResolver and ObjectClass from test to main sources so that external drivers can extract concrete inputs from symbolic states
A research prototype combining dynamic and static analysis of TS at the EtsIR level: - the first concrete EtsIR interpreter (full ECMAScript coercion semantics, calls/objects/arrays/intrinsics; anything unmodeled is reported as Unsupported, never a silently wrong value) - PBT phase: type-driven input generators biased by constants mined from the method body, online statement + branch-edge coverage, failure deduplication and greedy shrinking, runtime type profiling - symbolic phase: for every branch edge left uncovered by PBT, a TsReachabilityTarget chain is built and TsMachine runs in TARGETED mode (one machine run per target); the reaching state is captured at target propagation time, its inputs are extracted from the SMT model and replayed on the concrete interpreter to confirm the edge - observed-type hints from the PBT phase feed TsOptions.inputTypeHints, pruning fake-object discriminators, with an automatic hint-free fallback - HybridAnalyzer orchestrator with 4 ablation modes (PBT_ONLY, SYMBOLIC_ONLY, HYBRID, HYBRID_WITH_HINTS), JSON reports and a CLI for batch experiments - test suite: JS semantics unit tests, DSL-built IR interpreter tests, a differential oracle replaying TsMachine-produced inputs concretely, PBT phase tests, end-to-end hybrid tests and a hints ablation harness
ArkAnalyzer/EtsIR pipeline overview, concrete interpreter design and differential-testing findings (AA if-successor order drift, engine `+` approximation on references, targeted-mode stop/collect race), and the hybrid pipeline description with first corpus numbers.
There was a problem hiding this comment.
Pull request overview
Introduces a hybrid analysis pipeline for TypeScript/ArkTS combining a concrete EtsIR interpreter (for PBT + coverage + type profiling) with targeted symbolic execution, plus an “observed input type hints” mechanism to prune fake-object discriminator search during symbolic initialization.
Changes:
- Add
usvm-ts-pbtmodule implementing a concrete EtsIR interpreter, PBT phase, hybrid orchestrator, reporting CLI, and a dedicated test suite. - Extend
usvm-tswithTsInputTypeHints/TsOptions.inputTypeHintsand interpreter-side hint application for unresolved parameters. - Add
TsTestResolver.resolveInputsto extract input valuations from non-terminated states (for target-reaching state capture + replay).
Reviewed changes
Copilot reviewed 35 out of 37 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt | Add input-only model resolution for mid-execution states. |
| usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt | Add helper to synthesize an Object class for resolution. |
| usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt | Add inputTypeHints option plumbing with default EMPTY. |
| usvm-ts/src/main/kotlin/org/usvm/machine/TsInputTypeHints.kt | Define hint types and method/parameter-index keyed hint map. |
| usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | Apply observed-type hints to constrain fake-object discriminators. |
| usvm-ts-pbt/src/test/resources/pbt/HybridSamples.ts | Add fixtures for hybrid/PBT/hints end-to-end scenarios. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/Resources.kt | Add resource path/stream helpers for tests. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/LoadEts.kt | Add EtsIR loading helpers for resources and filesystem. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/JsSemanticsTest.kt | Unit tests for concrete JS coercion/ops semantics. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt | Differential oracle: symbolic model replay vs concrete interpreter. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteInterpreterDslTest.kt | Interpreter tests over DSL-built EtsIR (no ArkAnalyzer). |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/PbtPhaseTest.kt | Tests for PBT coverage, shrinking, profiling, determinism. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridE2eTest.kt | End-to-end hybrid pipeline + hints ablation harness. |
| usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzerTest.kt | Analyzer modes + report JSON round-trip tests. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Main.kt | CLI entrypoint for batch hybrid experiments and JSON output. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/HybridReport.kt | Serializable report schema for experiments and tooling. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Conversions.kt | Convert between symbolic TsTestValue and concrete VValue. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/VValue.kt | Define concrete runtime value universe for interpreter. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/JsSemantics.kt | Implement concrete JS semantics (coercions, ops, typeof, in). |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/Intrinsics.kt | Model built-in namespaces and selected methods/fields. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionResult.kt | Define execution outcomes + internal control-flow signals. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionListener.kt | Listener hooks for coverage/profiling and composition. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/EtsConcreteInterpreter.kt | Implement CFG-walking concrete interpreter over EtsIR. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/CallResolver.kt | Concrete name-based dispatch over scene hierarchy. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/TypeProfiler.kt | Record runtime input type tags and export to hints. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/SymbolicPhase.kt | Target uncovered edges, capture reaching state, resolve inputs, replay/merge coverage. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/PbtPhase.kt | PBT loop with generator, shrinker, coverage and profiling. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzer.kt | Orchestrate phases across modes; emit report model. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Shrinker.kt | Greedy shrinker for failure minimization. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Generators.kt | Type-driven random input generation with mined constants. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/ConstantMiner.kt | Mine numeric/string literals from method bodies to bias generators. |
| usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/CoverageTracker.kt | Statement + branch-edge coverage and trace merge support. |
| usvm-ts-pbt/build.gradle.kts | Add new module build config + runHybrid CLI task. |
| settings.gradle.kts | Register usvm-ts-pbt Gradle module. |
| docs/ts-pbt/03-hybrid-pipeline.md | Document implemented hybrid pipeline and findings. |
| docs/ts-pbt/02-concrete-interpreter-and-differential-findings.md | Document concrete interpreter + differential findings. |
| docs/ts-pbt/01-arkanalyzer-and-ets-ir.md | Document ArkAnalyzer/EtsIR wiring and methodology notes. |
Comments suppressed due to low confidence (1)
usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt:100
resolveInputsassumesstate.modelsis non-empty (state.models.first()), butUState.modelsis explicitly allowed to be empty (e.g. when forking without a solver). For mid-execution states this will throwNoSuchElementExceptionand makes the new API fragile. Compute a model from the currentpathConstraintswhen missing (and optionally cache it back intostate.models) so input resolution works regardless of solver-for-forks configuration.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+429
to
+433
| is VArray -> if (lhv.field.name == "length") { | ||
| val n = JsSemantics.toNumber(value).toInt() | ||
| while (target.elements.size > n) target.elements.removeAt(target.elements.size - 1) | ||
| while (target.elements.size < n) target.elements.add(VUndefined) | ||
| } |
Comment on lines
+3
to
+8
| import mu.KotlinLogging | ||
| import java.io.InputStream | ||
| import java.nio.file.Path | ||
| import kotlin.io.path.toPath | ||
|
|
||
| private val logger = KotlinLogging.logger {} |
The engine resolves relational operators on mixed-type fake-object operands per sort pair (Lt.onBool = !lhs && rhs) instead of the JS ToNumber coercion, so e.g. `false < 0.0` is reported true while JS gives `0 < 0 === false`. The divergence surfaces nondeterministically depending on which input models the machine samples, making the suite flaky without the whitelist entry.
- register usvm-ts-pbt in validateProjectList (the lint job failure) - pin @types/node@22 when building ArkAnalyzer in ci-ts: a transitively hoisted @types/node >= 24 uses TypeScript syntax the AA toolchain cannot parse; both --no-save packages (ohos-typescript is installed --no-save by the AA postinstall script) must go in a single npm install invocation, because every npm install re-resolves the tree and drops previous --no-save additions - run :usvm-ts-pbt:check in the ci-ts job - add detekt baselines for the new module
- 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[=<path>]) 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.
- pinned corpus definition (corpus.json) + fetch script: algorithm-style open-source TS projects, analyzable per-file at the EtsIR level - batch CLI: recursive corpus walking with exclude patterns, per-file and per-method fault isolation, multi-mode ablation runs (PBT_ONLY, SYMBOLIC_ONLY, HYBRID, HYBRID_WITH_HINTS) over the same corpus, one machine-readable report per mode, aggregate summaries - keep anonymous arrow-function methods (%AM...) as entry points: `export const f = (...) => ...` is the dominant style in real corpora - bail out of the PBT loop early when a method is dominated by unmodeled constructs (first 25 executions all Unsupported) - aggregate.py: markdown mode-comparison table + per-method CSV First campaign (TheAlgorithms/TypeScript maths, 62 methods, 264 branch edges, native ts-frontend): PBT-only 61.0% branches in 5.2s; symbolic-only 34.8% in 182.7s; hybrid 64.0% in 135s; hints on this corpus reach the same targets and expose the fallback cost (95 fallbacks) on an infeasible-dominated residual.
Driven by an Unsupported-reason histogram over the open-source corpus: - first-class functions (VFunction): arrow-function locals resolved via their FunctionType signature and file-initializer aliases; ptr_call dispatches through the dynamic function value (recursion of `const f = (...) => ...` now works) - higher-order array intrinsics with real callback invocation: map, filter, forEach, reduce, some, every, find, findIndex, sort - JS Map/Set (VMap/VSet) with SameValueZero keys: get/set/has/delete/ clear/keys/values/forEach, size - `new Array/Map/Set` constructors; Array(n) sizing - extended Math (log/log2/log10/exp/sign/trig/hypot/atan2/...), Number.parseInt/isSafeInteger, Object.keys/values
./run-project.sh <git-url | corpus-name | local-path> [--include dir] [--modes ...] [--commit sha] does the whole loop: clone, build the jacodb ts-frontend if missing, run the hybrid analyzer over all ablation modes with per-file fault isolation, aggregate, and write per-mode JSON reports, a summary table and a per-method CSV under results/<name>/. Demo on loiane/javascript-datastructures-algorithms (src/, 307 methods, 670 branch edges): PBT-only 62.5% branches in 1.7s; symbolic-only 57.2% in 427s; hybrid 75.1% in 243s (84/251 residual targets reached).
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
There was a problem hiding this comment.
detekt found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.
usvm-ts-pbt/README.md: architecture map, design invariants (honesty, replay-as-ground-truth, one-run-per-target, capture-at-propagation, the compare-to-zero idiom contract), environment table with the known pitfalls (pinned ArkAnalyzer build, provider env vars vs Gradle task caching), the differential-test whitelist policy and the v1 scope boundaries. docs/ts-pbt/00-project-state.md: the read-me-first handoff - branch map and the branch-separation policy (PBT vs engine fixes vs paper), current reproducible results, in-flight PRs and toolchain expectations, the prioritized backlog (PBT side, engine side, upstream frontend findings) and the docs index.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.