diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 34faf3df14..311c42e3f5 100644 --- 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 index 8223024eeb..8f611c8543 100644 --- 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 new file mode 100644 index 0000000000..0f1807e20d --- /dev/null +++ b/detekt/baselines/usvm-ts-pbt-Main.yml @@ -0,0 +1,87 @@ + + + + + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}") + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame))) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(left, frame)) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(right, frame)) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(left, frame) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(op(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame))).toDouble()) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(right, frame) + ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(target) + BracesOnWhenStatements:ConstantMiner.kt$MinedConstants.Companion$when + BracesOnWhenStatements:Conversions.kt$when + BracesOnWhenStatements:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$when + BracesOnWhenStatements:Generators.kt$InputGenerator$when + BracesOnWhenStatements:Intrinsics.kt$Intrinsics$when + BracesOnWhenStatements:JsSemantics.kt$JsSemantics$when + BracesOnWhenStatements:Main.kt$when + BracesOnWhenStatements:PbtPhase.kt$PbtPhase$when + EmptyFunctionBlock:CoverageTracker.kt$CoverageTracker${} + Filename:ConstantMiner.kt$org.usvm.ts.pbt.gen.ConstantMiner.kt + Filename:Generators.kt$org.usvm.ts.pbt.gen.Generators.kt + 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, ) ) + ForbiddenMethodCall:Main.kt$println("Analyzing ${methods.size} method(s) in mode $mode...") + ForbiddenMethodCall:Main.kt$println("Loading ${files.size} file(s) via ArkAnalyzer...") + ForbiddenMethodCall:Main.kt$println("Report written to $out") + ForbiddenMethodCall:Main.kt$println("Unknown option: ${args[i]}\n$USAGE") + ForbiddenMethodCall:Main.kt$println(USAGE) + LoopWithTooManyJumpStatements:PbtPhase.kt$PbtPhase$while + MagicNumber:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$31 + MagicNumber:Generators.kt$InputGenerator$0.0 + MagicNumber:Generators.kt$InputGenerator$0.6 + MagicNumber:Generators.kt$InputGenerator$10 + MagicNumber:Generators.kt$InputGenerator$100 + MagicNumber:Generators.kt$InputGenerator$1000 + MagicNumber:Generators.kt$InputGenerator$1001 + MagicNumber:Generators.kt$InputGenerator$101 + MagicNumber:Generators.kt$InputGenerator$11 + MagicNumber:Generators.kt$InputGenerator$1e6 + MagicNumber:Generators.kt$InputGenerator$3 + MagicNumber:Generators.kt$InputGenerator$4 + MagicNumber:Generators.kt$InputGenerator$5 + MagicNumber:Generators.kt$InputGenerator$6 + MagicNumber:Generators.kt$InputGenerator$8 + MagicNumber:Intrinsics.kt$Intrinsics$9007199254740991.0 + MagicNumber:JsSemantics.kt$JsSemantics$0xFFFFFFFFL + MagicNumber:JsSemantics.kt$JsSemantics$16 + MagicNumber:JsSemantics.kt$JsSemantics$1e21 + MagicNumber:JsSemantics.kt$JsSemantics$8 + MagicNumber:JsSemantics.kt$JsSemantics$9.007199254740992E15 + MagicNumber:Main.kt$100 + MagicNumber:Main.kt$20 + MagicNumber:Main.kt$2_000 + MagicNumber:PbtPhase.kt$PbtPhase$100 + MagicNumber:SymbolicPhase.kt$SymbolicPhase$1_000_000 + MatchingDeclarationName:ConstantMiner.kt$MinedConstants + MatchingDeclarationName:Generators.kt$InputGenerator + MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$) + MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw typeError("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}") + MaximumLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$ + MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VNamespace(e.name) + MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VString(array.value[i.toInt()].toString()) + MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VUndefined + MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw UnsupportedFeatureSignal("global ref: ${e.name}") + MultiLineIfElse:Generators.kt$InputGenerator$genAny(depth) + MultiLineIfElse:Generators.kt$InputGenerator$generate(type.types[random.nextInt(type.types.size)], depth) + MultiLineIfElse:Generators.kt$InputGenerator$random.nextDouble(-1e6, 1e6) + MultiLineIfElse:Generators.kt$InputGenerator$random.nextInt(-100, 101) + random.nextDouble() + MultiLineIfElse:JsSemantics.kt$JsSemantics$d.toLong().toString() + MultiLineIfElse:JsSemantics.kt$JsSemantics$java.math.BigDecimal(d).toBigInteger().toString() + MultiLineIfElse:PbtPhase.kt$PbtPhase$args + NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List<VValue>): VValue + NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame) + NestedBlockDepth:Shrinker.kt$Shrinker$fun shrink(args: List<VValue>, stillFails: (List<VValue>) -> Boolean): List<VValue> + NoMultipleSpaces:Generators.kt$InputGenerator$ + SwallowedException:EtsConcreteInterpreter.kt$EtsConcreteInterpreter$e: StackOverflowError + ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun evalCall(expr: EtsCallExpr, frame: Frame): VValue + ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List<VValue>): VValue + ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame) + TooGenericExceptionCaught:SymbolicPhase.kt$SymbolicPhase$e: Throwable + UnderscoresInNumericLiterals:Intrinsics.kt$Intrinsics$9007199254740991.0 + Wrapping:Generators.kt$InputGenerator$; + Wrapping:Intrinsics.kt$Intrinsics$( + Wrapping:Intrinsics.kt$Intrinsics$; + + diff --git a/detekt/baselines/usvm-ts-pbt-Test.yml b/detekt/baselines/usvm-ts-pbt-Test.yml new file mode 100644 index 0000000000..cb0ac5472e --- /dev/null +++ b/detekt/baselines/usvm-ts-pbt-Test.yml @@ -0,0 +1,27 @@ + + + + + ArgumentListWrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}") + ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = hints, hintFallback = false, ) + ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = pbt.typeProfiler.toHints(), ) + BracesOnWhenStatements:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$when + CommentSpacing:LoadEts.kt$//----------------------------------------------------------------------------- + ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println(" MISMATCH: $it") + ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}") + 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}" ) + 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 + MaxLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}") + MaximumLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$ + MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$compared++ + MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$mismatches += "$ctx: concrete threw ${result.value}, symbolic returned ${test.returnValue}" + NestedBlockDepth:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$private fun runDifferential(resourcePath: String, className: String): Verdict + NoMultipleSpaces:JsSemanticsTest.kt$JsSemanticsTest$ + SwallowedException:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$e: Throwable + UnderscoresInNumericLiterals:HybridE2eTest.kt$HybridE2eTest$49382.0 + UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295.0 + UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295L + Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$( + Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$; + + diff --git a/docs/ts-pbt/00-project-state.md b/docs/ts-pbt/00-project-state.md new file mode 100644 index 0000000000..81abb7ed47 --- /dev/null +++ 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=` 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. diff --git a/docs/ts-pbt/01-arkanalyzer-and-ets-ir.md b/docs/ts-pbt/01-arkanalyzer-and-ets-ir.md new file mode 100644 index 0000000000..950e5dd74f --- /dev/null +++ b/docs/ts-pbt/01-arkanalyzer-and-ets-ir.md @@ -0,0 +1,358 @@ +# ArkAnalyzer, the EtsIR, and how USVM-TS is wired to them + +> Research note for the **Property-Based Testing (PBT) for ArkTS/TS** effort. +> Branch: `caelmbleidd/ts_pbt`. Date: 2026-06-19. +> +> Goal of this document: explain *what ArkAnalyzer is*, *how this repository +> depends on it*, *what the IR looks like*, and *whether we should keep relying +> on it or write our own `.ts`/`.js` front-end* that produces the same IR. + +--- + +## 1. TL;DR + +* `usvm-ts` (the symbolic execution engine for ArkTS/TS) does **not** parse + TypeScript itself. It consumes an already-lowered, three-address, + basic-block IR called **EtsIR**, exposed as Kotlin classes + (`EtsScene` / `EtsFile` / `EtsMethod` / `EtsStmt` …) from the external + library **`jacodb-ets`**. +* That IR is produced by **ArkAnalyzer** — a *TypeScript/Node.js* static + analysis framework for ArkTS/OpenHarmony. ArkAnalyzer parses the source, + lowers it to its own "ArkIR", and **serializes it to JSON**. `jacodb-ets` + then **deserializes the JSON** into `EtsFileDto` and **lifts** it to the + `EtsFile` model. +* The full pipeline is therefore: + + ``` + *.ts / *.ets / *.js + │ ArkAnalyzer (Node): src/save/serializeArkIR.js + ▼ + EtsIR JSON (one *.ts.json per source file) + │ jacodb-ets: EtsFileDto.loadFromJson() (kotlinx.serialization) + ▼ + EtsFileDto (1:1 mirror of the JSON) + │ jacodb-ets: EtsFileDto.toEtsFile() / EtsMethodBuilder + ▼ + EtsFile / EtsScene ← "the IR you see in the project" + │ usvm-ts: TsMachine / TsInterpreter / TsExprResolver + ▼ + symbolic execution → TsTest (org.usvm.api.TsTest) + ``` + +* **Recommendation (see §6):** for PBT we should build our **own front-end** + `.ts`/`.js → EtsIR`, because ArkAnalyzer is a heavyweight, version-coupled, + per-file-subprocess external dependency that is tuned for ArkTS/OHOS (not + plain JS) and is opaque/hard to control. We can target the exact same IR + contract so that all of `usvm-ts` keeps working unchanged. + +--- + +## 2. What is ArkAnalyzer? + +**ArkAnalyzer** (sometimes written "Ark Analyzer") is an open-source static +analysis framework for **ArkTS** — the application language of Huawei's +**OpenHarmony / HarmonyOS**. ArkTS is a constrained dialect of TypeScript. + +* Upstream: `https://gitcode.com/openharmony-sig/arkanalyzer` (OpenHarmony SIG). +* It is written **in TypeScript** and runs on **Node.js**. +* It builds an SSA-ish, Jimple-like **three-address IR** ("ArkIR") out of TS + sources: `ArkFile`, `ArkClass`, `ArkMethod`, `ArkAssignStmt`, + `ArkInstanceInvokeExpr`, etc. It also resolves imports/exports, models + namespaces, decorators, and ships handling for the OHOS SDK. It can run + **type inference** over the IR. + +### The fork we actually use + +This project does **not** use upstream ArkAnalyzer directly. It uses a +**fork maintained by `Lipen`** (a jacodb maintainer) that is kept in lock-step +with jacodb's deserializer: + +* Fork: `https://gitcode.com/Lipen/arkanalyzer` (mirror: `gitee.com/Lipenx/arkanalyzer`). +* You must checkout a branch named `neo/` that matches the current + jacodb DTO schema. The version coupling is real: the JSON schema emitted by + ArkAnalyzer must match the `*Dto` classes in `jacodb-ets`. +* CI currently pins branch **`neo/2025-09-03`** (see `.github/workflows/ci.yml`). + `jacodb-ets/ARKANALYZER.md` mentions `neo/2025-02-24`; `usvm-ts-dataflow/README.md` + mentions `neo/2024-10-31`. **These drift over time** — always read CI for the + source of truth. + +### The serializer entry point + +The relevant script is **`src/save/serializeArkIR.ts`** (built to +`out/src/save/serializeArkIR.js`): + +```text +Usage: serializeArkIR [options] + -p, --project input is a project directory + -t, --infer-types [times] run type inference N times over the IR + -v, --verbose + -e, --entrypoints (load entrypoints; used in jacodb's generateEtsIR) +``` + +* Single file: `node out/src/save/serializeArkIR.js sample.ts sample.json` +* Whole project: `node out/src/save/serializeArkIR.js -p project etsir` + (mirrors the source tree, every file becomes `*.ts.json`). + +There is also `src/usvm/inferTypes.ts`, a wrapper that combines serialization +with USVM's *own* type inference (`usvm-dataflow-ts`). + +--- + +## 3. How **this repository** connects to ArkAnalyzer + +There are three connection points. + +### 3.1 Test-time auto-conversion (the main path for `usvm-ts`) + +The test base class `usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt` +loads `.ts` resources via `loadEtsFileAutoConvert(...)` / +`loadEtsProjectAutoConvert(...)` from **`jacodb-ets`** +(`org.jacodb.ets.utils.LoadEtsFile`). That function: + +1. reads env vars + * `ARKANALYZER_DIR` (default `arkanalyzer`) + * `SERIALIZE_SCRIPT_PATH` (default `out/src/save/serializeArkIR.js`) + * `NODE_EXECUTABLE` (default `node`) +2. spawns a subprocess roughly: + `node $ARKANALYZER_DIR/out/src/save/serializeArkIR.js -t 1 -v` + (a temp file for a single file, a temp dir for a project), +3. deserializes the resulting JSON with `EtsFileDto.loadFromJson(stream)`, +4. lifts it with `etsFileDto.toEtsFile()`. + +So **every test that loads a `.ts` file shells out to Node and runs +ArkAnalyzer on the fly.** The `.ts` sources live under +`usvm-ts/src/test/resources/samples/**`; the JSON is transient (temp files). + +### 3.2 SDK IR generation (Gradle task) + +`usvm-ts/build.gradle.kts` defines `generateSdkIR`, which runs +`serializeArkIR.js -p ets etsir` over the OpenHarmony SDK (`*.d.ts`) to produce +committed/cached IR for the SDK. Requires `ARKANALYZER_DIR` to be set. +`usvm-ts-dataflow/build.gradle.kts` has an analogous task. + +### 3.3 CI provisioning + +`.github/workflows/ci.yml` (the TS job): + +* sets up Node 22, +* `git clone --depth=1 --branch neo/2025-09-03 https://gitcode.com/Lipen/arkanalyzer arkanalyzer` + (with up to 10 retries — the remote is flaky), +* `npm install && npm run build`, +* exports `ARKANALYZER_DIR=$(realpath arkanalyzer)`, +* then `./gradlew :usvm-ts:check :usvm-ts-dataflow:check`. + +### 3.4 Dependency coordinates + +* `buildSrc/src/main/kotlin/Dependencies.kt`: jacodb pinned at commit + `b17013382a` (JitPack group `com.github.UnitTestBot.jacodb`), artifact + `jacodb-ets`. +* The `jacodb-ets` sources used for this analysis live on the jacodb branch + `lipen/dev` (commit `e02e6fdf…`), module `jacodb-ets/`. + +--- + +## 4. The EtsIR contract (what a producer must emit) + +The JSON boundary is the set of `*Dto` classes in +`org.jacodb.ets.dto` (`jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/`). +kotlinx.serialization is configured with a **class discriminator field `"_"`** +(`@JsonClassDiscriminator("_")`), and each variant has a `@SerialName`. So in +the JSON, a statement looks like `{"_":"AssignStmt","left":{…},"right":{…}}`. + +### 4.1 Top-level structure (`Model.kt`, `Signatures.kt`, `Cfg.kt`) + +``` +EtsFileDto + signature: { projectName, fileName } + namespaces: [ NamespaceDto ] // nested classes/namespaces + classes: [ ClassDto ] + importInfos / exportInfos // module resolution + +ClassDto + signature: { name, declaringFile, declaringNamespace? } + modifiers: Int (bitmask) // EtsModifiers + decorators, category, typeParameters? + superClassName?, implementedInterfaceNames + fields: [ FieldDto ] + methods: [ MethodDto ] + +MethodDto + signature: { declaringClass, name, parameters:[{name,type,isOptional,isRest}], returnType } + modifiers, decorators, typeParameters? + body?: { locals: [LocalDto], cfg: { blocks: [ BasicBlockDto ] } } + +BasicBlockDto + id, successors:[Int], predecessors:[Int]?, stmts:[StmtDto] +``` + +**Control flow is encoded structurally**: there is no `Goto`/`Switch` statement. +A block lists its successor block ids. An `IfStmt` block has exactly two +successors (true branch first, then false). This is a CFG-of-basic-blocks, not +an AST. + +### 4.2 Statements (`Stmts.kt`) — only 7 kinds + +| `_` (SerialName) | Payload | +|---|---| +| `NopStmt` | — | +| `AssignStmt` | `left: Value`, `right: Value` | +| `CallStmt` | `expr: CallExpr` | +| `ReturnVoidStmt` | — | +| `ReturnStmt` | `arg: Value` | +| `ThrowStmt` | `arg: Value` | +| `IfStmt` | `condition: ConditionExpr` | +| `RawStmt` | escape hatch: `kind` + `extra` (raw JSON) | + +### 4.3 Values / expressions (`Values.kt`) + +* **Immediates:** `Local{name,type}`, `Constant{value:String,type}`. + ⚠️ **All constants are strings** (`"3.14"`, `"true"`, `"hello"`) tagged with a + `type` (`NumberType`/`BooleanType`/`StringType`/…). There are no typed numeric + constants in the DTO yet (there is a long commented-out block in `Values.kt` + describing the intended future split). +* **Exprs:** `NewExpr`, `NewArrayExpr`, `DeleteExpr`, `AwaitExpr`, `YieldExpr`, + `TypeOfExpr`, `InstanceOfExpr`, `CastExpr`, `UnopExpr{op}`, `BinopExpr{op}`, + `ConditionExpr{op}`, and calls `InstanceCallExpr` / `StaticCallExpr` / + `PtrCallExpr` (each carries a `MethodSignature` + `args`). +* **Refs:** `ThisRef`, `ParameterRef{index}`, `CaughtExceptionRef`, + `GlobalRef{name,ref?}`, `ClosureFieldRef`, `ArrayRef{array,index}`, + `InstanceFieldRef{instance,field}`, `StaticFieldRef{field}`. +* Operators are **strings** (`Ops.kt`): unary `+ - ! ~ ++ --`; binary + `+ - * / % ** << >> >>> & | ^ && || ??`; relational `== != === !== < <= > >= in`. +* `RawValue` escape hatch mirrors `RawStmt`. + +### 4.4 Types (`Types.kt`) + +`AnyType`, `UnknownType`, `GenericType`, `AliasType`, `LexicalEnvType`, +`EnumValueType`, `VoidType`, `NeverType`, `UnionType`, `IntersectionType`, +primitives (`BooleanType`, `NumberType`, `StringType`, `NullType`, +`UndefinedType`, `LiteralType`), `ClassType`, `UnclearReferenceType`, +`ArrayType{elementType,dimensions}`, `TupleType`, `FunctionType`. Plus +`RawType`. The `-t` flag controls how well these get filled in vs left +`UnknownType`/`UnclearReferenceType`. + +### 4.5 The DTO → model lift (`Convert.kt`, `EtsMethodBuilder`) + +`toEtsFile()` is **not a trivial 1:1 copy**. The `EtsMethodBuilder`: + +* re-establishes strict **three-address form**: nested sub-expressions are + flattened into fresh temporaries (`_tmp0`, `_tmp1`, … via `ensureLocal`), +* maps operator strings to concrete typed classes (`"+" → EtsAddExpr`, + `"==" → EtsEqExpr`, …), +* attaches `EtsStmtLocation`s and builds the linear/block CFG + (`EtsBlockCfg`). + +**Key takeaway for a custom producer:** the JSON we emit must *already* be +basic-block-structured and *roughly* three-address (one operation per +statement, operands are immediates/refs). ArkAnalyzer does the genuinely hard +lowering (AST → 3AC → CFG); `toEtsFile` only does the final normalization. So a +replacement front-end has to reproduce that lowering, not just a syntax tree. + +--- + +## 5. How the IR is used downstream (relevance to PBT) + +* `usvm-ts` walks `EtsMethod.cfg`, resolving each `EtsStmt` /`EtsExpr` in + `TsInterpreter` / `TsExprResolver`, and emits `org.usvm.api.TsTest`: + `{ method, before/after parameter states, returnValue, trace }`, where values + are `TsTestValue` (`TsNumber`, `TsString`, `TsBoolean`, `TsClass`, `TsArray`, + `TsNull`, `TsUndefined`, exceptions, …). +* For PBT this matters: the engine already gives us concrete input models and + return values per path. A PBT loop wants to (a) *obtain IR for a generated or + given program* cheaply and repeatably, and (b) round-trip + generate→lower→execute→check at high throughput. Spawning Node per program is + the obvious bottleneck and correctness risk. + +--- + +## 6. Is ArkAnalyzer suitable for us? Should we write our own parser? + +### 6.1 What ArkAnalyzer gives us (pros) + +* It already works end-to-end; `usvm-ts` consumes its output directly. +* It does the hard parts: TS parsing, AST → 3-address lowering, CFG + construction, import/export & namespace resolution, decorators, the OHOS SDK, + and type inference. +* The Lipen fork is kept consistent with jacodb's DTOs. + +### 6.2 Pain points (cons) + +* **Heavyweight external dependency:** Node + npm + cloning a *specific fork and + branch*. Setup is fragile (CI retries the clone up to 10×). +* **Version coupling:** the AA branch must match the jacodb DTO schema; the + "supported branch" drifts (`neo/2024-10-31` → `2025-02-24` → `2025-09-03`). +* **Per-file subprocess at test time:** each `.ts` load shells out to Node. + Slow, IO-heavy, timeout-prone; bad fit for PBT's many-runs loop. +* **Tuned for ArkTS/OHOS, not plain JS:** `.js` support is unclear/untested + here; behavior follows ArkTS semantics. +* **Known gaps/bugs:** e.g. unary plus is unsupported + (`samples/operators/UnaryPlus.kt` is `@Disabled`, AA issue #737). +* **Opaque & uncontrollable:** lowering decisions (temp naming, CFG shape, + constants-as-strings) are dictated externally. For PBT — where we want to + *generate* programs and/or IR and tightly control the surface we exercise — + this is a liability. + +### 6.3 Conclusion + +**Keep ArkAnalyzer as the reference/oracle, but build our own front-end** that +produces the same EtsIR contract. Reasons: throughput, hermetic builds, control +over the supported language subset, and the ability to generate/round-trip IR +for PBT without a Node round-trip per case. Because we target the *same* IR +(`EtsFileDto` JSON, or the `EtsFile` model directly), **all of `usvm-ts` +continues to work unchanged**, and we can differentially test our front-end +against ArkAnalyzer on overlapping inputs. + +--- + +## 7. Options for our own `.ts`/`.js` → EtsIR front-end + +Two output targets: + +* **(T-JSON)** emit `EtsFileDto`-shaped JSON → reuse `jacodb-ets` + `loadFromJson` + `toEtsFile` unchanged. Lowest integration risk; lets + `toEtsFile` do the final 3AC normalization for us. +* **(T-MODEL)** build the `EtsFile`/`EtsMethod` model directly in JVM and skip + JSON entirely. Best for throughput / no-Node, but we must reproduce what + `EtsMethodBuilder` does (3AC, CFG, op→class mapping). + +Parser/lowering technology choices: + +| Approach | Parsing | Lowering (AST→3AC+CFG) | Node needed? | Notes | +|---|---|---|---|---| +| **A. Our serializer (Node + `typescript` API)** | TS compiler API | we write it in TS | yes, but *our* code | Drop-in replacement for `serializeArkIR`; reuses jacodb deserializer. Still per-file Node. | +| **B. GraalJS + TS compiler on JVM** | run `typescript` in-process via GraalJS | in TS or Kotlin | no external Node | Hermetic, in-JVM; heavier runtime, GraalJS setup. | +| **C. JVM-native TS/JS parser** (swc/oxc/tree-sitter binding, or ANTLR grammar) | native/JVM | Kotlin | no | We own the whole pipeline; most work but best long-term control. | +| **D. Hand-written parser for a subset** | Kotlin | Kotlin | no | Smallest scope; ideal if PBT only needs a language subset initially. | + +These are not mutually exclusive — e.g. start with **D** (a controlled subset +that maps cleanly onto the 7 statement kinds and the value/expr set above), +build the IR model directly (**T-MODEL**), and differentially validate against +ArkAnalyzer (the **A**/existing path) on the overlap. + +### Open questions to settle before implementation (see §8) + +1. Output target: **T-JSON** (reuse jacodb lift) vs **T-MODEL** (direct model)? +2. Parser tech: **A/B/C/D** above? +3. Language scope: which `.ts`/`.js` subset first (the union/intersection of + what `usvm-ts` already supports and what PBT will generate)? +4. Type information: do we need types up front, or lean on `UnknownType` + + USVM's own inference (`usvm-dataflow-ts`)? + +--- + +## 8. Appendix: quick reference + +* IR producer (external): `arkanalyzer/out/src/save/serializeArkIR.js` +* IR consumer (lib): `jacodb-ets` + * deserialize: `org.jacodb.ets.dto.EtsFileDto.loadFromJson` + * lift: `org.jacodb.ets.dto.toEtsFile` / `EtsMethodBuilder` (`Convert.kt`) + * auto-convert util: `org.jacodb.ets.utils.LoadEtsFile` + (`loadEtsFileAutoConvert`, `loadEtsProjectAutoConvert`, `generateEtsIR`) + * DTO package: `org.jacodb.ets.dto.{Model,Stmts,Values,Types,Signatures,Cfg,Ops,Convert}` + * model package: `org.jacodb.ets.model.{Scene,File,Class,Method,Stmt,Value,Expr,Type,...}` +* In-repo wiring: + * tests: `usvm-ts/.../util/TsMethodTestRunner.kt`, `util/LoadEts.kt` + * SDK task: `usvm-ts/build.gradle.kts` → `generateSdkIR` + * CI: `.github/workflows/ci.yml` (ArkAnalyzer fork `Lipen/arkanalyzer`, branch `neo/2025-09-03`) + * env vars: `ARKANALYZER_DIR`, `SERIALIZE_SCRIPT_PATH`, `NODE_EXECUTABLE` +* PBT-relevant output: `org.usvm.api.TsTest` + `TsTestValue` diff --git a/docs/ts-pbt/02-concrete-interpreter-and-differential-findings.md b/docs/ts-pbt/02-concrete-interpreter-and-differential-findings.md new file mode 100644 index 0000000000..be629c6073 --- /dev/null +++ b/docs/ts-pbt/02-concrete-interpreter-and-differential-findings.md @@ -0,0 +1,67 @@ +# Concrete EtsIR interpreter + differential-testing findings + +> Research note for the hybrid PBT + symbolic execution effort. +> Module: `usvm-ts-pbt`. Date: 2026-07-02. + +## 1. What was built + +`usvm-ts-pbt` (new Gradle module) contains the first *concrete* interpreter for EtsIR +(`org.usvm.ts.pbt.interpreter.EtsConcreteInterpreter`): + +* JS value universe `VValue` (`VNumber/VBool/VString/VNull/VUndefined/VObject/VArray/VNamespace`), + reference semantics for objects/arrays; +* full ECMAScript coercions in `JsSemantics` (ToNumber/ToString/ToPrimitive/ToInt32, + loose/strict equality, relational ops, `typeof`, `in`); +* statement walker over `EtsBlockCfg` (convention: **first if-successor = true branch** — + the *model-level* contract after the jacodb lift, see §3); +* calls: static + virtual dispatch by name over the class hierarchy (mirrors + `TsInterpreter.visitVirtualMethodCall`), intrinsics registry (`Math`, `Number`, + `console`/`Logger` no-ops, array/string methods) — anything unknown yields + `ExecutionResult.Unsupported`, never a silently wrong value; +* outcomes: `Returned / Threw / Diverged (budget) / Unsupported`. + +`TsTestResolver` + `ObjectClass` were promoted from usvm-ts *test* sources to *main*, +so symbolic states can be converted to concrete inputs outside tests +(`org.usvm.util.TsTestResolver`, unchanged package). + +## 2. Differential oracle + +`ConcreteVsSymbolicDifferentialTest`: every input model produced by `TsMachine` +(via `TsTestResolver`) is replayed on the concrete interpreter; return values must +match. 7 sample suites (Add, Less, Neg, And, Equality, Truthy, TypeCoercion): +**~100 compared executions, 1 confirmed divergence** (whitelisted, see below). + +## 3. Finding A: ArkAnalyzer if-successor order drift (critical) + +* DTO contract: AA serializes if-successors as **(false, true)**; jacodb's + `EtsMethodBuilder` (`Convert.kt`) reverses them, so the *model* (`EtsBlockCfg`) + uses **(true, false)** — which is what `TsInterpreter.visitIfStmt` assumes. +* The local AA checkout (`lipen/usvm` branch) emits a **different order** than the + CI-pinned `neo/2025-09-03`. After the lift this **inverts every branch** of every + method: this was the real cause of the "pre-existing" local usvm-ts test failures + (`Add`: violated invariants; reachability: "unreachable stmt reached"). +* Fix used here: a dedicated worktree `~/Programming/arkanalyzer-neo-2025-09-03` + (built from the CI-pinned branch); run all TS tests with + `ARKANALYZER_DIR=~/Programming/arkanalyzer-neo-2025-09-03`. +* Lesson for the paper (methodology): the concrete interpreter + differential suite + detected a *frontend contract violation* end-to-end within hours — this is an + argument for the triple-oracle setup (concrete IR interpreter vs symbolic engine + vs production JS engine). + +Beware Gradle test caching: changing `ARKANALYZER_DIR` does **not** invalidate test +tasks; use `--rerun-tasks` when switching AA versions. + +## 4. Finding B: usvm-ts `+` approximation on references + +For reference operands usvm-ts resolves `+` numerically, so `null + {}` becomes +fp `NaN`; JS applies ToPrimitive + string concatenation +(`null + {} === "null[object Object]"`). Consequently in +`Add.addUnknownValues(null, {})` the engine follows the `res != res` (NaN) branch, +which is concretely unreachable, and reports return `NaN` where JS returns `42`. +Whitelisted in the differential suite as a known engine approximation. + +## 5. Environment requirements + +* `ARKANALYZER_DIR` → CI-pinned AA build (`neo/2025-09-03`), see §3. +* Solver: YICES (same as usvm-ts test config). +* usvm-ts-pbt test resources include `usvm-ts/src/test/resources` (read-only reuse). diff --git a/docs/ts-pbt/03-hybrid-pipeline.md b/docs/ts-pbt/03-hybrid-pipeline.md new file mode 100644 index 0000000000..cdc9a0f5fe --- /dev/null +++ b/docs/ts-pbt/03-hybrid-pipeline.md @@ -0,0 +1,101 @@ +# Hybrid pipeline: PBT -> targeted symbolic execution with type feedback + +> Research note. Module: `usvm-ts-pbt`. Date: 2026-07-03. + +## 1. Pipeline (implemented, all tests green) + +``` +EtsScene (jacodb-ets, ArkAnalyzer neo/2025-09-03) + │ + ├─ Phase 1: PbtPhase (org.usvm.ts.pbt.hybrid) + │ EtsConcreteInterpreter × InputGenerator(seeded, constant-mined) + │ → CoverageTracker (stmt + branch edges), TypeProfiler, failures + Shrinker + │ + ├─ Handoff: CoverageTracker.uncoveredBranches() + │ + ├─ Phase 2: SymbolicPhase — per uncovered edge (I, S): + │ TsReachabilityTarget chain InitialPoint(entry)→Intermediate(I)→Final(S), + │ TsMachine(TARGETED, stopOnTargetsReached, YICES, per-target timeout), + │ TsOptions.inputTypeHints ← TypeProfiler (HYBRID_WITH_HINTS mode), + │ hint-free fallback on failure, + │ state captured at propagation time (ReachingStateCaptor), + │ inputs via TsTestResolver.resolveInputs (new, works for non-terminated states), + │ concrete replay confirms the edge → merged into CoverageTracker + │ + └─ HybridAnalyzer → HybridReport (JSON) / CLI (report.Main) +``` + +Modes: `PBT_ONLY | SYMBOLIC_ONLY | HYBRID | HYBRID_WITH_HINTS` (ablation-ready). + +## 2. usvm-ts changes (minimal, reviewed) + +1. `TsInputTypeHints.kt` (new): `TsHintType` enum + method-keyed hint map. +2. `TsOptions.inputTypeHints` (default `EMPTY` — zero behavior change). +3. `TsInterpreter.getInitialState`: for `TsUnresolvedSort` parameters, after + `mkFakeValue`, `applyParameterTypeHints` asserts a disjunction over the fake + object's type discriminators (`fpTypeExpr`/`boolTypeExpr`/`refTypeExpr`) and + refines the ref slot (`null`/`undefined`/string-type/not-nullish) — an + *unsound-by-design* prune with orchestrator-level fallback. +4. `TsTestResolver.resolveInputs` (new): before-state resolution only, usable for + states captured mid-execution. +5. `TsTestResolver` + `ObjectClass` promoted from test to main sources. + +## 3. Engineering findings worth writing up + +* **stop/collect race in targeted mode**: `stopOnTargetsReached` halts the machine + when the target tree is removed — at *propagation* time — while both + `TargetsReachedStatesCollector` and `CoveredNewStatesCollector` only collect + *terminated* states; additionally, in `TsMachine` the collector observes + *before* the `machineObserver` (`ReachabilityObserver`), so at termination the + `reachedTerminal` flag is not yet set. Consequence: `REACHED_TARGET` collection + effectively never yields states in this configuration. Fix: capture the state + at propagation time (custom `UMachineObserver` placed after + `ReachabilityObserver`) and resolve *inputs only* from its model. +* **Steps are the wrong metric for the hints ablation on micro-benchmarks**: with + `useSolverForForks = true` infeasible discriminator forks are pruned eagerly, so + machine steps stay equal; hints save *solver work* (visible as wall time / + solver calls on larger corpora). The CLI reports wall time per target. +* **PBT constant mining is strong**: equality guards against literal constants + (`x === 1234567`) are covered by mining the method body; the symbolic phase is + needed for *arithmetic* relations (`x * 2 === 98764` → engine synthesizes + `x = 49382`, confirmed by concrete replay). + +## 4. End-to-end status + +* `HybridSamples.magic`: PBT 3/4 edges, symbolic reaches the arithmetic branch, + replay confirms, 100% branch coverage. Input `x = 49382` recovered from the model. +* `HybridSamples.crashy`: PBT finds the out-of-bounds throw, shrinker minimizes + to `([], 0)`. +* CLI: `./gradlew :usvm-ts-pbt:runHybrid --args=" [--mode ...] [--out report.json]"` + (requires `ARKANALYZER_DIR` → pinned AA build; paths absolute or relative to repo root). + +## 5. First corpus run (usvm-ts samples/operators, HYBRID_WITH_HINTS) + +`--pbt-iterations 500 --target-timeout 10`, 90 methods, total wall ~6 s: + +* branch coverage 524/720 = **72.8%**, stmt coverage 1660/1974 = **84.1%**, + 44/90 methods at 100% branches; +* PBT: 29052 executions, 3500 `Unsupported` (bigint, `delete`, `in`-operator + paths — honestly excluded, not guessed); +* symbolic: 275 targets, 80 reached, 25 replay-confirmed, 195 hint-fallbacks. + Most unreached targets are the samples' *intentionally unreachable* branches + (`return -1; // unreachable`) — i.e. correct behavior, and a natural + connection to the UnreachableCodeDetector use-case; +* observed engine issue: unbounded mutual recursion + `StrictEq.resolveFakeObject ↔ resolveBinaryOperator` on some fake-object + comparisons (logged stack overflows; states killed) — differential/corpus + finding #3 for the engine maintainers. + +Improvement backlog (paper experiments): raise replay-confirmation rate +(fake-object input resolution), distinguish "infeasible" from "timeout" per +target, add solver-time metric for the hints ablation. + +## 6. Test suite map (usvm-ts-pbt) + +* `JsSemanticsTest` — ECMAScript coercion corner cases. +* `ConcreteInterpreterDslTest` — interpreter over DSL-built EtsIR (no ArkAnalyzer). +* `ConcreteVsSymbolicDifferentialTest` — differential oracle vs TsMachine + (7 sample suites; 1 whitelisted engine divergence). +* `PbtPhaseTest` — coverage, shrinking, type profiles, seed reproducibility. +* `HybridE2eTest` — full pipeline + hints ablation harness. +* `HybridAnalyzerTest` — 4 modes, JSON round-trip. diff --git a/docs/ts-pbt/04-jacodb-native-parser-compat.md b/docs/ts-pbt/04-jacodb-native-parser-compat.md new file mode 100644 index 0000000000..b41269c50b --- /dev/null +++ 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= ...`, 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-ets/ts-frontend && npm install && npm run build +cd +export ETS_IR_PROVIDER=ts-frontend +export ETS_FRONTEND_DIR=/jacodb-ets/ts-frontend +./gradlew -PuseLocalJacodb= :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 index 428d679fce..4d0fb4c829 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -33,6 +33,7 @@ include("usvm-jvm:usvm-jvm-api") include("usvm-jvm:usvm-jvm-test-api") include("usvm-jvm:usvm-jvm-util") include("usvm-ts") +include("usvm-ts-pbt") include("usvm-util") include("usvm-jvm-instrumentation") include("usvm-sample-language") @@ -55,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[=] (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/README.md b/usvm-ts-pbt/README.md new file mode 100644 index 0000000000..837d1182f8 --- /dev/null +++ b/usvm-ts-pbt/README.md @@ -0,0 +1,91 @@ +# usvm-ts-pbt: hybrid PBT + targeted symbolic execution for TypeScript/ArkTS + +A research prototype combining dynamic and static analysis at the EtsIR level +(the ArkIR of the jacodb toolchain): a property-based-testing phase executes +the method concretely on random inputs, and the uncovered branch edges are +handed to the usvm-ts symbolic engine as reachability targets. Runtime type +profiles observed by the dynamic phase prune the type dimension of the +symbolic search (fake-object discriminators), with an automatic hint-free +fallback. + +> Start here, then see `docs/ts-pbt/00-project-state.md` (repo root) for the +> current branch map, results, and backlog, and `docs/ts-pbt/01..04-*.md` for +> the research notes. + +## Architecture map + +``` +org.usvm.ts.pbt +├── interpreter/ the first *concrete* interpreter for EtsIR +│ ├── VValue.kt JS value universe (+VFunction, VMap, VSet) +│ ├── JsSemantics.kt ECMAScript coercions (ToNumber/ToString/equality/...) +│ ├── EtsConcreteInterpreter.kt CFG walker; first if-successor = true branch +│ ├── CallResolver.kt static/virtual/ptr_call resolution, fn aliases +│ ├── Intrinsics.kt Math/Number/Array-HOFs/Map/Set/strings registry +│ └── ExecutionResult.kt Returned | Threw | Diverged | Unsupported +├── gen/ type-driven input generators (+constant mining), Shrinker +├── coverage/ CoverageTracker: stmt + branch-EDGE coverage, timelines +├── hybrid/ PbtPhase, SymbolicPhase (targets, capture, replay), +│ TypeProfiler, HybridAnalyzer (4 ablation modes) +├── report/ JSON reports (kotlinx-serialization), TsTestValue<->VValue, +│ Main.kt — the batch CLI +└── benchmarks/ corpus + one-command pipeline (see benchmarks/README.md) +``` + +Key design invariants: + +- **Honesty**: anything unmodeled is `Unsupported` (never a silently wrong + value); `Unsupported`/`Diverged` are excluded from PBT verdicts and counted + in reports. +- **Replay as ground truth**: a branch is credited to the symbolic phase only + if the solver-synthesized inputs replay it concretely. +- **One machine run per symbolic target** (`TargetsReachedStopStrategy` waits + for ALL targets; batching lets one infeasible branch eat the whole budget). +- **The reaching state is captured at target-propagation time** by our own + observer (the stock REACHED_TARGET collector misses it — see note 03 §3); + inputs come from `TsTestResolver.resolveInputs` (works for non-terminated + states). +- **Compare-to-zero idiom**: both front ends lower `if (x)` to `x != 0`; + the interpreter treats compare-to-zero on a non-number as ToBoolean + (see note 04 §2 — the IR is ambiguous by design). + +## Environment + +| What | Value | +|---|---| +| ArkAnalyzer (provider 1) | build of the **CI-pinned branch** `neo/2025-09-03`; `export ARKANALYZER_DIR=...`. Do NOT use other branches: if-successor order drifts and silently inverts every branch (note 02 §3) | +| jacodb ts-frontend (provider 2, default for benchmarks) | jacodb PR #361 branch; `npm install && npm run build` in `jacodb-ets/ts-frontend`; `export ETS_IR_PROVIDER=ts-frontend ETS_FRONTEND_DIR=/jacodb-ets/ts-frontend`; substitute jacodb via `./gradlew -PuseLocalJacodb= ...` until the pin is bumped | +| Solver | YICES (bundled via ksmt) | +| JDK | detekt requires <= 21 locally (`JAVA_HOME= ./gradlew detektMain`) | + +**Gradle pitfall**: changing `ARKANALYZER_DIR`/`ETS_IR_PROVIDER` does *not* +invalidate test tasks — use `--rerun-tasks` when switching providers. + +## Running + +```bash +# tests (29): unit, differential oracle vs TsMachine, hybrid e2e, ablation +ARKANALYZER_DIR= ./gradlew :usvm-ts-pbt:test + +# one method / one file +./gradlew :usvm-ts-pbt:runHybrid --args="/File.ts --mode HYBRID_WITH_HINTS --out report.json" + +# a whole open-source project, all ablation modes, aggregated: +cd usvm-ts-pbt/benchmarks && ./run-project.sh [--include dir] +``` + +## Differential-test whitelist policy + +`ConcreteVsSymbolicDifferentialTest` replays every input model the engine +produces; mismatches FAIL the build unless whitelisted in +`knownEngineDivergences` with a root-cause comment. Only add entries after +manually confirming against ECMAScript semantics that the divergence is an +engine/front-end issue (current entries: `+` on references, Lt on mixed +fake-object sorts, the NaN hole of the truthiness idiom — see notes 02/04). + +## What is intentionally out of scope (v1) + +Generators/`yield`, async/Promise, closures capturing mutable state, BigInt, +cross-file imports under per-file scenes (all reported as `Unsupported`), +string constraints in the symbolic phase (engine limitation: placeholder +strings, lossy replay). diff --git a/usvm-ts-pbt/benchmarks/.gitignore b/usvm-ts-pbt/benchmarks/.gitignore new file mode 100644 index 0000000000..9d416116f7 --- /dev/null +++ b/usvm-ts-pbt/benchmarks/.gitignore @@ -0,0 +1,2 @@ +corpus/ +results/ diff --git a/usvm-ts-pbt/benchmarks/README.md b/usvm-ts-pbt/benchmarks/README.md new file mode 100644 index 0000000000..6e7f6d3931 --- /dev/null +++ b/usvm-ts-pbt/benchmarks/README.md @@ -0,0 +1,78 @@ +# Benchmark infrastructure: hybrid analysis on open-source TypeScript + +Batch experiments for the hybrid PBT + targeted symbolic execution pipeline +over open-source TS projects, using the **native TS parser from jacodb** +(`jacodb-ets/ts-frontend`, jacodb PR #361) as the EtsIR provider. + +## TL;DR — one command per project + +```bash +# by URL: clones into corpus/, analyzes, aggregates, writes reports +./run-project.sh https://github.com/TheAlgorithms/TypeScript.git --include maths + +# by corpus name (already cloned) or by local path +./run-project.sh typescript-algorithms --include src +./run-project.sh ~/work/my-ts-project + +# narrower/faster runs +./run-project.sh --modes PBT_ONLY,HYBRID --max-files 40 --target-timeout 5 +``` + +The script does everything end-to-end: + +1. resolves the project (clone by URL / corpus name / local path; `--commit ` + for reproducibility), +2. builds `ts-frontend` if missing (`JACODB_DIR`, default `~/Programming/jacodb`), +3. runs the hybrid analyzer over all requested ablation modes + (default: `PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS`) with per-file + fault isolation, +4. aggregates and writes everything under `results//`: + - `-.json` — full machine-readable report per mode + (per-method coverage, coverage timelines, per-target wall time, + hint/fallback attribution, unsupported-execution counters), + - `-summary.md` — the mode-comparison table, + - `.csv` — per-method rows for plotting. + +Until jacodb PR #361 is merged and the usvm dependency pin is bumped, the local +jacodb build is substituted automatically via `-PuseLocalJacodb=$JACODB_DIR`. + +## Pinned corpus + +`corpus.json` pins reference projects to commits; `./fetch-corpus.sh` clones them +(requires `git` + `jq`). Preferred projects are algorithm-style repositories +(self-contained functions, arithmetic- and branch-rich) — analyzable per-file at +the EtsIR level without cross-module resolution. Cross-file imports resolve to +honest `Unsupported` at call sites and are reported, never guessed. + +## Manual (advanced) invocation + +The underlying CLI offers finer control: + +```bash +export ETS_IR_PROVIDER=ts-frontend +export ETS_FRONTEND_DIR=/jacodb-ets/ts-frontend + +./gradlew -PuseLocalJacodb= :usvm-ts-pbt:runHybrid --args="\ + --recursive \ + --modes PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS \ + --pbt-iterations 1000 --target-timeout 10 \ + --out results/my-run" + +python3 aggregate.py results/my-run-*.json --csv results/my-run.csv +``` + +See `./gradlew :usvm-ts-pbt:runHybrid --args=""` for the full option list +(`--class`, `--method`, `--exclude`, `--seed`, `--no-fallback`, ...). + +## Interpreting the numbers + +- **Branch %** counts covered branch *edges* `(if, successor)` — the handoff + granularity of the hybrid pipeline. +- **Unsupported** counts PBT executions that hit constructs the concrete + interpreter does not model (generators, cross-file imports under per-file + scenes, exotic intrinsics). They are excluded from pass/fail verdicts. +- **Reached / Replay OK** — symbolic targets reached, and those whose + solver-synthesized inputs were *confirmed by concrete replay* (the ground + truth for crediting a branch to the symbolic phase). +- **Fallbacks** — hint-free retries after an unsuccessful hinted run: the + measured price of the (deliberately unsound) type-hint pruning. diff --git a/usvm-ts-pbt/benchmarks/aggregate.py b/usvm-ts-pbt/benchmarks/aggregate.py new file mode 100644 index 0000000000..e24a4c113c --- /dev/null +++ b/usvm-ts-pbt/benchmarks/aggregate.py @@ -0,0 +1,96 @@ +#!/usr/bin/env python3 +"""Aggregate hybrid-analyzer reports into a mode-comparison table. + +Usage: + python3 aggregate.py report-prefix-*.json [--csv out.csv] + +Reads one or more HybridReport JSON files (one per analysis mode) and prints a +markdown comparison table; optionally writes per-method rows as CSV for plotting +(coverage timelines are preserved in the raw reports). +""" +import argparse +import csv +import json +import sys +from pathlib import Path + + +def load(path): + with open(path) as f: + return json.load(f) + + +def summarize(report): + ms = report["methods"] + tb = sum(m["totalBranches"] for m in ms) + cb = sum(m["coveredBranches"] for m in ms) + ts = sum(m["totalStmts"] for m in ms) + cs = sum(m["coveredStmts"] for m in ms) + targets = [t for m in ms if m.get("symbolic") for t in m["symbolic"]["targets"]] + pbt_failures = sum(len(m["pbt"]["failures"]) for m in ms if m.get("pbt")) + unsupported = sum(m["pbt"]["unsupported"] for m in ms if m.get("pbt")) + return { + "mode": report["config"]["mode"], + "methods": len(ms), + "branchCov": 100.0 * cb / tb if tb else 100.0, + "stmtCov": 100.0 * cs / ts if ts else 100.0, + "full100": sum(1 for m in ms if m["branchCoverage"] == 1.0), + "pbtFailures": pbt_failures, + "unsupported": unsupported, + "targets": len(targets), + "reached": sum(1 for t in targets if t["reached"]), + "replayOk": sum(1 for t in targets if t["replayConfirmed"]), + "fallbacks": sum(1 for t in targets if t["fallbackUsed"]), + "targetWallMs": sum(t["wallMs"] for t in targets), + "wallS": sum(m["totalWallMs"] for m in ms) / 1000.0, + } + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("reports", nargs="+") + ap.add_argument("--csv", help="write per-method rows to this CSV") + args = ap.parse_args() + + reports = [load(p) for p in args.reports] + rows = [summarize(r) for r in reports] + + cols = [ + ("mode", "Mode"), ("methods", "Methods"), ("branchCov", "Branch %"), + ("stmtCov", "Stmt %"), ("full100", "100% methods"), ("pbtFailures", "PBT failures"), + ("unsupported", "Unsupported"), ("targets", "Targets"), ("reached", "Reached"), + ("replayOk", "Replay OK"), ("fallbacks", "Fallbacks"), + ("targetWallMs", "Target wall ms"), ("wallS", "Total wall s"), + ] + print("| " + " | ".join(h for _, h in cols) + " |") + print("|" + "---|" * len(cols)) + for row in rows: + cells = [] + for key, _ in cols: + v = row[key] + cells.append(f"{v:.1f}" if isinstance(v, float) else str(v)) + print("| " + " | ".join(cells) + " |") + + if args.csv: + with open(args.csv, "w", newline="") as f: + w = csv.writer(f) + w.writerow(["mode", "method", "totalBranches", "coveredBranches", + "branchCoverage", "stmtCoverage", "wallMs", + "pbtExecutions", "pbtFailures", "targets", "targetsReached"]) + for r in reports: + mode = r["config"]["mode"] + for m in r["methods"]: + targets = m["symbolic"]["targets"] if m.get("symbolic") else [] + w.writerow([ + mode, m["method"], m["totalBranches"], m["coveredBranches"], + f'{m["branchCoverage"]:.4f}', f'{m["stmtCoverage"]:.4f}', + m["totalWallMs"], + m["pbt"]["executions"] if m.get("pbt") else 0, + len(m["pbt"]["failures"]) if m.get("pbt") else 0, + len(targets), sum(1 for t in targets if t["reached"]), + ]) + print(f"\nCSV written to {args.csv}", file=sys.stderr) + + +if __name__ == "__main__": + main() diff --git a/usvm-ts-pbt/benchmarks/corpus.json b/usvm-ts-pbt/benchmarks/corpus.json new file mode 100644 index 0000000000..7f8a7155b4 --- /dev/null +++ b/usvm-ts-pbt/benchmarks/corpus.json @@ -0,0 +1,34 @@ +{ + "description": "Open-source TypeScript corpus for the hybrid PBT + symbolic execution experiments. Projects are pinned to specific commits for reproducibility. Algorithm-style repositories are preferred: self-contained functions with rich arithmetic/branching are analyzable at the EtsIR level without full cross-module resolution.", + "projects": [ + { + "name": "TheAlgorithms-TypeScript", + "url": "https://github.com/TheAlgorithms/TypeScript.git", + "commit": "19b4ced86c99815f142d4a46a028f55487b8038a", + "include": [ + "maths", + "search", + "sorts", + "bit_manipulation", + "dynamic_programming" + ], + "excludePatterns": [ + ".test.ts", + ".d.ts" + ] + }, + { + "name": "typescript-algorithms", + "url": "https://github.com/loiane/javascript-datastructures-algorithms.git", + "commit": "e8ee8f9b8a07589533c4243a210d4cea7b090b10", + "include": [ + "src" + ], + "excludePatterns": [ + ".test.ts", + ".spec.ts", + ".d.ts" + ] + } + ] +} diff --git a/usvm-ts-pbt/benchmarks/fetch-corpus.sh b/usvm-ts-pbt/benchmarks/fetch-corpus.sh new file mode 100755 index 0000000000..18e6313973 --- /dev/null +++ b/usvm-ts-pbt/benchmarks/fetch-corpus.sh @@ -0,0 +1,25 @@ +#!/usr/bin/env bash +# Fetches the open-source TS corpus defined in corpus.json into benchmarks/corpus/. +# Requires: git, jq. +set -euo pipefail + +cd "$(dirname "$0")" +mkdir -p corpus + +jq -c '.projects[]' corpus.json | while read -r project; do + name=$(jq -r '.name' <<< "$project") + url=$(jq -r '.url' <<< "$project") + commit=$(jq -r '.commit' <<< "$project") + + if [[ -d "corpus/$name" ]]; then + echo "[skip] corpus/$name already exists" + continue + fi + + echo "[clone] $name ($url @ $commit)" + git clone --filter=blob:none "$url" "corpus/$name" + git -C "corpus/$name" checkout --quiet "$commit" + echo "[ok] corpus/$name @ $(git -C "corpus/$name" rev-parse --short HEAD)" +done + +echo "Corpus ready under $(pwd)/corpus" diff --git a/usvm-ts-pbt/benchmarks/run-project.sh b/usvm-ts-pbt/benchmarks/run-project.sh new file mode 100755 index 0000000000..34122cb326 --- /dev/null +++ b/usvm-ts-pbt/benchmarks/run-project.sh @@ -0,0 +1,136 @@ +#!/usr/bin/env bash +# End-to-end measurement pipeline for one open-source TypeScript project. +# +# ./run-project.sh [options] +# +# Does everything: clone (if needed) -> build ts-frontend (if needed) -> +# run the hybrid analyzer in all requested ablation modes -> aggregate -> +# write reports and a summary table under results//. +# +# Examples: +# ./run-project.sh https://github.com/TheAlgorithms/TypeScript.git --include maths +# ./run-project.sh TheAlgorithms-TypeScript --include sorts --modes PBT_ONLY,HYBRID +# ./run-project.sh ~/my/local/ts-project +# +# Options: +# --include analyze only this subdirectory of the project (repeatable) +# --modes ablation modes (default: PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS) +# --pbt-iterations PBT budget per method (default: 1000) +# --target-timeout per-target symbolic timeout (default: 10) +# --max-files cap the number of files (default: unlimited) +# --seed PBT seed (default: 0) +# --commit checkout this commit after cloning (reproducibility) +# +# Environment (auto-detected when possible): +# JACODB_DIR jacodb checkout with jacodb-ets/ts-frontend (default: ~/Programming/jacodb) +# ETS_FRONTEND_DIR built ts-frontend (default: $JACODB_DIR/jacodb-ets/ts-frontend) +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +REPO_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)" +CORPUS_DIR="$SCRIPT_DIR/corpus" +RESULTS_DIR="$SCRIPT_DIR/results" + +# ---------------------------------------------------------------- arguments +[[ $# -ge 1 ]] || { grep '^#' "$0" | head -30; exit 1; } +TARGET="$1"; shift + +INCLUDES=() +MODES="PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS" +PBT_ITERATIONS=1000 +TARGET_TIMEOUT=10 +MAX_FILES=0 +SEED=0 +COMMIT="" + +while [[ $# -gt 0 ]]; do + case "$1" in + --include) INCLUDES+=("$2"); shift 2 ;; + --modes) MODES="$2"; shift 2 ;; + --pbt-iterations) PBT_ITERATIONS="$2"; shift 2 ;; + --target-timeout) TARGET_TIMEOUT="$2"; shift 2 ;; + --max-files) MAX_FILES="$2"; shift 2 ;; + --seed) SEED="$2"; shift 2 ;; + --commit) COMMIT="$2"; shift 2 ;; + *) echo "Unknown option: $1"; exit 1 ;; + esac +done + +# ---------------------------------------------------------------- resolve project +if [[ -d "$TARGET" ]]; then + PROJECT_DIR="$(cd "$TARGET" && pwd)" + NAME="$(basename "$PROJECT_DIR")" +elif [[ "$TARGET" == http* || "$TARGET" == git@* ]]; then + NAME="$(basename "$TARGET" .git)" + PROJECT_DIR="$CORPUS_DIR/$NAME" + if [[ ! -d "$PROJECT_DIR" ]]; then + echo "[clone] $TARGET -> $PROJECT_DIR" + git clone --filter=blob:none "$TARGET" "$PROJECT_DIR" + fi + if [[ -n "$COMMIT" ]]; then + git -C "$PROJECT_DIR" checkout --quiet "$COMMIT" + fi + echo "[project] $NAME @ $(git -C "$PROJECT_DIR" rev-parse --short HEAD)" +elif [[ -d "$CORPUS_DIR/$TARGET" ]]; then + NAME="$TARGET" + PROJECT_DIR="$CORPUS_DIR/$NAME" +else + echo "Not a directory, URL, or known corpus name: $TARGET" + exit 1 +fi + +# ---------------------------------------------------------------- toolchain +JACODB_DIR="${JACODB_DIR:-$HOME/Programming/jacodb}" +ETS_FRONTEND_DIR="${ETS_FRONTEND_DIR:-$JACODB_DIR/jacodb-ets/ts-frontend}" + +if [[ ! -f "$ETS_FRONTEND_DIR/dist/index.js" ]]; then + if [[ -f "$ETS_FRONTEND_DIR/package.json" ]]; then + echo "[build] ts-frontend at $ETS_FRONTEND_DIR" + (cd "$ETS_FRONTEND_DIR" && npm install && npm run build) + else + echo "ts-frontend not found: $ETS_FRONTEND_DIR (set ETS_FRONTEND_DIR or JACODB_DIR)" + exit 1 + fi +fi + +# ---------------------------------------------------------------- inputs +ANALYZE_DIRS=() +if [[ ${#INCLUDES[@]} -gt 0 ]]; then + for inc in "${INCLUDES[@]}"; do ANALYZE_DIRS+=("$PROJECT_DIR/$inc"); done +else + ANALYZE_DIRS=("$PROJECT_DIR") +fi + +OUT_DIR="$RESULTS_DIR/$NAME" +mkdir -p "$OUT_DIR" + +EXTRA_ARGS=() +[[ "$MAX_FILES" != "0" ]] && EXTRA_ARGS+=("--max-files" "$MAX_FILES") + +# ---------------------------------------------------------------- run +export ETS_IR_PROVIDER=ts-frontend +export ETS_FRONTEND_DIR + +for dir in "${ANALYZE_DIRS[@]}"; do + suffix="" + [[ ${#ANALYZE_DIRS[@]} -gt 1 || ${#INCLUDES[@]} -gt 0 ]] && suffix="-$(basename "$dir")" + out_prefix="$OUT_DIR/$NAME$suffix" + + echo "[analyze] $dir" + (cd "$REPO_ROOT" && ./gradlew -q "-PuseLocalJacodb=$JACODB_DIR" :usvm-ts-pbt:runHybrid --args="\ + $dir --recursive \ + --modes $MODES \ + --pbt-iterations $PBT_ITERATIONS \ + --target-timeout $TARGET_TIMEOUT \ + --seed $SEED \ + ${EXTRA_ARGS[*]:-} \ + --out $out_prefix" 2>&1 | grep -vE "^\[|WARN|INFO|ERROR| at | org\.|Exception") + + echo + echo "== Summary: $NAME$suffix ==" + python3 "$SCRIPT_DIR/aggregate.py" "$out_prefix"-*.json --csv "$out_prefix.csv" \ + | tee "$out_prefix-summary.md" + echo +done + +echo "Reports: $OUT_DIR" diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts new file mode 100644 index 0000000000..74153cd39b --- /dev/null +++ b/usvm-ts-pbt/build.gradle.kts @@ -0,0 +1,39 @@ +plugins { + id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin +} + +dependencies { + implementation(project(":usvm-core")) + implementation(project(":usvm-ts")) + + implementation(Libs.jacodb_core) + implementation(Libs.jacodb_ets) + + implementation(Libs.kotlinx_serialization_json) + + implementation(Libs.ksmt_yices) + + testImplementation(Libs.junit_jupiter_params) + testImplementation(Libs.logback) +} + +// Reuse the usvm-ts test samples (read-only) for differential and end-to-end tests. +sourceSets { + test { + resources { + srcDir(rootDir.resolve("usvm-ts").resolve("src").resolve("test").resolve("resources")) + } + } +} + +// CLI for batch experiments: ./gradlew :usvm-ts-pbt:runHybrid --args="file.ts --mode HYBRID" +val runHybrid by tasks.registering(JavaExec::class) { + group = "application" + description = "Runs the hybrid PBT + symbolic analyzer CLI." + mainClass.set("org.usvm.ts.pbt.report.MainKt") + classpath = sourceSets["main"].runtimeClasspath + workingDir = rootDir + // Propagate the ArkAnalyzer location for .ts -> EtsIR conversion + System.getenv("ARKANALYZER_DIR")?.let { environment("ARKANALYZER_DIR", it) } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/CoverageTracker.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/CoverageTracker.kt new file mode 100644 index 0000000000..0fdd4f8b15 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/CoverageTracker.kt @@ -0,0 +1,126 @@ +package org.usvm.ts.pbt.coverage + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.usvm.ts.pbt.interpreter.ExecutionListener +import org.usvm.ts.pbt.interpreter.VValue +import java.util.IdentityHashMap + +/** + * Statement + branch coverage shared by both phases of the hybrid analysis. + * + * A branch is an edge `(ifStmt, takenSuccessor)`. Identity semantics are used + * for [EtsStmt] keys (statements are unique objects within a loaded scene). + */ +class CoverageTracker( + /** The coverage zone: entry method + (optionally) other tracked methods. */ + methods: List, +) : ExecutionListener { + + data class BranchEdge(val ifStmt: EtsIfStmt, val successor: EtsStmt) + + data class UncoveredBranch(val method: EtsMethod, val edge: BranchEdge) + + data class Sample( + val elapsedMs: Long, + val phase: String, + val coveredStmts: Int, + val coveredBranches: Int, + ) + + private val zone: List = methods.filter { it.cfg.stmts.isNotEmpty() } + + val allStmts: Set = run { + val set = newIdentitySet() + zone.forEach { set.addAll(it.cfg.stmts) } + set + } + + val allBranches: Set = buildSet { + for (method in zone) { + for (stmt in method.cfg.stmts) { + if (stmt is EtsIfStmt) { + method.cfg.successors(stmt).forEach { succ -> add(BranchEdge(stmt, succ)) } + } + } + } + } + + private val coveredStmts = newIdentitySet() + private val coveredBranches = mutableSetOf() + private val timelineSamples = mutableListOf() + + private val startNanos = System.nanoTime() + + /** Label attributed to coverage recorded via listener callbacks. */ + var phase: String = "pbt" + + val coveredStmtCount: Int get() = coveredStmts.size + val coveredBranchCount: Int get() = coveredBranches.size + val timeline: List get() = timelineSamples + + fun stmtCoverage(): Double = + if (allStmts.isEmpty()) 1.0 else coveredStmts.size.toDouble() / allStmts.size + + fun branchCoverage(): Double = + if (allBranches.isEmpty()) 1.0 else coveredBranches.size.toDouble() / allBranches.size + + fun isCovered(edge: BranchEdge): Boolean = edge in coveredBranches + + /** The worklist for the symbolic phase: branch edges never taken. */ + fun uncoveredBranches(): List { + val methodOf = IdentityHashMap() + zone.forEach { m -> m.cfg.stmts.forEach { methodOf[it] = m } } + return allBranches + .filter { it !in coveredBranches } + .mapNotNull { edge -> methodOf[edge.ifStmt]?.let { UncoveredBranch(it, edge) } } + } + + fun uncoveredStmts(): List = allStmts.filter { it !in coveredStmts } + + // -- ExecutionListener -------------------------------------------------- + + override fun onStmt(stmt: EtsStmt) { + if (stmt in allStmts && coveredStmts.add(stmt)) { + recordSample() + } + } + + override fun onBranch(ifStmt: EtsIfStmt, taken: EtsStmt, condition: Boolean) { + if (ifStmt in allStmts && coveredBranches.add(BranchEdge(ifStmt, taken))) { + recordSample() + } + } + + override fun onMethodEnter(method: EtsMethod, thisValue: VValue, args: List) {} + + /** Merge a symbolic-phase trace (e.g. `state.pathNode.allStatements`) as covered. */ + fun mergeTrace(stmts: List) { + var newCoverage = false + for (stmt in stmts) { + if (stmt in allStmts && coveredStmts.add(stmt)) newCoverage = true + } + // Recover branch edges from consecutive pairs + for ((a, b) in stmts.zipWithNext()) { + if (a is EtsIfStmt && a in allStmts && coveredBranches.add(BranchEdge(a, b))) { + newCoverage = true + } + } + if (newCoverage) recordSample() + } + + private fun recordSample() { + timelineSamples += Sample( + elapsedMs = (System.nanoTime() - startNanos) / 1_000_000, + phase = phase, + coveredStmts = coveredStmts.size, + coveredBranches = coveredBranches.size, + ) + } + + private companion object { + fun newIdentitySet(): MutableSet = + java.util.Collections.newSetFromMap(IdentityHashMap()) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/ConstantMiner.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/ConstantMiner.kt new file mode 100644 index 0000000000..d8148ed3cc --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/ConstantMiner.kt @@ -0,0 +1,60 @@ +package org.usvm.ts.pbt.gen + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsUnaryExpr + +/** + * Mines number/string literals from a method body (a classic PBT trick: + * biasing generated inputs towards program constants and their neighbourhood + * dramatically improves the odds of hitting comparison branches). + */ +data class MinedConstants( + val numbers: List, + val strings: List, +) { + companion object { + fun of(method: EtsMethod): MinedConstants { + val numbers = linkedSetOf() + val strings = linkedSetOf() + + fun visit(e: EtsEntity) { + when (e) { + is EtsNumberConstant -> numbers += e.value + is EtsStringConstant -> strings += e.value + is EtsBinaryExpr -> { + visit(e.left) + visit(e.right) + } + + is EtsUnaryExpr -> visit(e.arg) + is EtsCastExpr -> visit(e.arg) + is EtsInstanceOfExpr -> visit(e.arg) + is EtsNewArrayExpr -> visit(e.size) + else -> Unit + } + } + + for (stmt in method.cfg.stmts) { + when (stmt) { + is EtsAssignStmt -> visit(stmt.rhv) + is EtsIfStmt -> visit(stmt.condition) + is EtsReturnStmt -> stmt.returnValue?.let { visit(it) } + is EtsCallStmt -> stmt.expr.args.forEach { visit(it) } + else -> Unit + } + } + return MinedConstants(numbers.toList(), strings.toList()) + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Generators.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Generators.kt new file mode 100644 index 0000000000..394fe2e24c --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Generators.kt @@ -0,0 +1,132 @@ +package org.usvm.ts.pbt.gen + +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.ts.pbt.interpreter.VArray +import org.usvm.ts.pbt.interpreter.VBool +import org.usvm.ts.pbt.interpreter.VNull +import org.usvm.ts.pbt.interpreter.VNumber +import org.usvm.ts.pbt.interpreter.VObject +import org.usvm.ts.pbt.interpreter.VString +import org.usvm.ts.pbt.interpreter.VUndefined +import org.usvm.ts.pbt.interpreter.VValue +import kotlin.random.Random + +/** + * Type-driven random input generation for an [EtsMethod], biased with + * constants mined from the method body. + */ +class InputGenerator( + private val scene: EtsScene, + private val method: EtsMethod, + private val random: Random, +) { + private val mined = MinedConstants.of(method) + + private val interestingNumbers: List = buildList { + add(0.0); add(-0.0); add(1.0); add(-1.0) + add(Double.NaN); add(Double.POSITIVE_INFINITY); add(Double.NEGATIVE_INFINITY) + add(Double.MAX_VALUE); add(Double.MIN_VALUE) + for (c in mined.numbers) { + add(c); add(c + 1); add(c - 1) + } + } + + private val interestingStrings: List = buildList { + add(""); add("0"); add("a"); add(" ") + addAll(mined.strings) + } + + fun generateArgs(): List = + method.parameters.map { generate(it.type, depth = 0) } + + /** `this` instance for the enclosing class (instance methods). */ + fun generateThis(): VValue { + val cls = method.enclosingClass ?: return VUndefined + return instantiate(cls, depth = 0) + } + + fun generate(type: EtsType, depth: Int): VValue = when (type) { + is EtsNumberType -> genNumber() + is EtsBooleanType -> VBool(random.nextBoolean()) + is EtsStringType -> genString() + is EtsNullType -> VNull + is EtsUndefinedType -> VUndefined + + is EtsArrayType -> genArray(type.elementType, depth) + + is EtsClassType -> { + val cls = scene.projectAndSdkClasses.firstOrNull { it.signature == type.signature } + ?: scene.projectAndSdkClasses.firstOrNull { it.name == type.signature.name } + if (cls != null) instantiate(cls, depth) else VObject(null) + } + + is EtsUnionType -> + if (type.types.isEmpty()) genAny(depth) + else generate(type.types[random.nextInt(type.types.size)], depth) + + is EtsAnyType, is EtsUnknownType -> genAny(depth) + + else -> genAny(depth) // unclear refs, generics, aliases: fall back to the full mix + } + + private fun genAny(depth: Int): VValue = when (random.nextInt(if (depth < 2) 8 else 6)) { + 0 -> genNumber() + 1 -> VBool(random.nextBoolean()) + 2 -> genString() + 3 -> VNull + 4 -> VUndefined + 5 -> genNumber() // numbers are twice as likely: the dominant type in practice + 6 -> genArray(EtsUnknownType, depth + 1) + else -> VObject(null, mutableMapOf()) + } + + fun genNumber(): VNumber = when (random.nextInt(4)) { + 0 -> VNumber(interestingNumbers[random.nextInt(interestingNumbers.size)]) + 1 -> VNumber(random.nextInt(-10, 11).toDouble()) + 2 -> VNumber(random.nextInt(-1000, 1001).toDouble()) + else -> VNumber( + // Random double, occasionally non-integral + if (random.nextBoolean()) random.nextDouble(-1e6, 1e6) + else random.nextInt(-100, 101) + random.nextDouble() + ) + } + + fun genString(): VString = when (random.nextInt(3)) { + 0 -> VString(interestingStrings[random.nextInt(interestingStrings.size)]) + 1 -> VString(random.nextInt(-100, 101).toString()) // numeric strings matter for coercions + else -> VString( + (1..random.nextInt(1, 6)) + .map { "abcxyz01"[random.nextInt(8)] } + .joinToString("") + ) + } + + private fun genArray(elementType: EtsType, depth: Int): VArray { + var size = 0 + while (size < 8 && random.nextDouble() < 0.6) size++ // geometric + return VArray(MutableList(size) { generate(elementType, depth + 1) }) + } + + private fun instantiate(cls: EtsClass, depth: Int): VObject { + val fields = mutableMapOf() + if (depth < 3) { + for (field in cls.fields) { + fields[field.name] = generate(field.type, depth + 1) + } + } + return VObject(cls, fields) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Shrinker.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Shrinker.kt new file mode 100644 index 0000000000..0ef30da464 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/gen/Shrinker.kt @@ -0,0 +1,88 @@ +package org.usvm.ts.pbt.gen + +import org.usvm.ts.pbt.interpreter.VArray +import org.usvm.ts.pbt.interpreter.VBool +import org.usvm.ts.pbt.interpreter.VNumber +import org.usvm.ts.pbt.interpreter.VObject +import org.usvm.ts.pbt.interpreter.VString +import org.usvm.ts.pbt.interpreter.VUndefined +import org.usvm.ts.pbt.interpreter.VValue +import kotlin.math.abs +import kotlin.math.floor + +/** + * Greedy per-parameter shrinking: repeatedly try simpler candidate values, + * keep any replacement under which the property still fails, until a fixpoint + * or the budget is exhausted. + */ +class Shrinker( + private val maxAttempts: Int = 500, +) { + /** + * @param stillFails re-runs the property with the candidate inputs; + * `true` = the failure is preserved. + */ + fun shrink(args: List, stillFails: (List) -> Boolean): List { + var current = args + var attempts = 0 + var progress = true + + while (progress && attempts < maxAttempts) { + progress = false + for (i in current.indices) { + for (candidate in candidates(current[i])) { + if (attempts++ >= maxAttempts) return current + val next = current.toMutableList().also { it[i] = candidate } + if (stillFails(next)) { + current = next + progress = true + break + } + } + } + } + return current + } + + private fun candidates(v: VValue): List = when (v) { + is VNumber -> buildList { + if (v.value != 0.0 || v.value.isNaN()) add(VNumber(0.0)) + if (v.value.isNaN() || v.value.isInfinite()) add(VNumber(1.0)) + if (v.value.isFinite() && v.value != floor(v.value)) add(VNumber(floor(v.value))) + if (v.value.isFinite() && abs(v.value) > 1) add(VNumber(v.value / 2)) + if (v.value < 0 && v.value.isFinite()) add(VNumber(-v.value)) + }.filter { it != v } + + is VString -> buildList { + if (v.value.isNotEmpty()) { + add(VString("")) + add(VString(v.value.substring(0, v.value.length / 2))) + add(VString(v.value.drop(1))) + } + }.filter { it != v } + + is VBool -> if (v.value) listOf(VBool(false)) else emptyList() + + is VArray -> buildList { + if (v.elements.isNotEmpty()) { + add(VArray(mutableListOf())) + add(VArray(v.elements.subList(0, v.elements.size / 2).toMutableList())) + add(VArray(v.elements.subList(1, v.elements.size).toMutableList())) + } + } + + is VObject -> buildList { + if (v.fields.isNotEmpty()) { + // Try emptying the fields, then undefined-ing them one by one + add(VObject(v.cls, mutableMapOf())) + for (key in v.fields.keys) { + val reduced = v.fields.toMutableMap() + reduced[key] = VUndefined + add(VObject(v.cls, reduced)) + } + } + } + + else -> emptyList() // VNull/VUndefined/VNamespace are already minimal + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzer.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzer.kt new file mode 100644 index 0000000000..e3b9b022d8 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzer.kt @@ -0,0 +1,168 @@ +package org.usvm.ts.pbt.hybrid + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.usvm.machine.TsInputTypeHints +import org.usvm.ts.pbt.coverage.CoverageTracker +import org.usvm.ts.pbt.report.ConfigEcho +import org.usvm.ts.pbt.report.FailureReport +import org.usvm.ts.pbt.report.HybridReport +import org.usvm.ts.pbt.report.MethodReport +import org.usvm.ts.pbt.report.PbtReport +import org.usvm.ts.pbt.report.SymbolicReport +import org.usvm.ts.pbt.report.TargetReport +import org.usvm.ts.pbt.report.TimelinePoint +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +private val logger = KotlinLogging.logger {} + +enum class AnalysisMode { + /** Only random testing at the IR level. */ + PBT_ONLY, + + /** Only targeted symbolic execution (every branch is a target). */ + SYMBOLIC_ONLY, + + /** PBT first, then targeted symbolic execution on the leftovers. */ + HYBRID, + + /** [HYBRID] + observed-type hints from the PBT phase feed the symbolic phase. */ + HYBRID_WITH_HINTS, +} + +data class HybridConfig( + val mode: AnalysisMode = AnalysisMode.HYBRID_WITH_HINTS, + val seed: Long = 0L, + val pbtMaxIterations: Int = 2_000, + val pbtTimeBudget: Duration = 30.seconds, + val perTargetTimeout: Duration = 20.seconds, + val hintFallback: Boolean = true, + val shrink: Boolean = true, + val interproceduralAnalysis: Boolean = true, +) + +/** + * The orchestrator of the hybrid analysis pipeline: + * `PBT (concrete, coverage + type profiles) -> targeted symbolic execution -> replay`. + */ +class HybridAnalyzer( + private val scene: EtsScene, + private val config: HybridConfig = HybridConfig(), +) { + fun analyze(methods: List): HybridReport { + val reports = methods.map { analyzeMethod(it) } + return HybridReport( + config = ConfigEcho( + mode = config.mode.name, + seed = config.seed, + pbtMaxIterations = config.pbtMaxIterations, + pbtTimeBudgetMs = config.pbtTimeBudget.inWholeMilliseconds, + perTargetTimeoutMs = config.perTargetTimeout.inWholeMilliseconds, + hintFallback = config.hintFallback, + ), + methods = reports, + ) + } + + fun analyzeMethod(method: EtsMethod): MethodReport { + logger.info { "analyzing ${method.signature} in mode ${config.mode}" } + val start = System.nanoTime() + val coverage = CoverageTracker(listOf(method)) + + var pbtReport: PbtReport? = null + var hints = TsInputTypeHints.EMPTY + + if (config.mode != AnalysisMode.SYMBOLIC_ONLY) { + val pbtStart = System.nanoTime() + val pbt = PbtPhase( + scene = scene, + method = method, + coverage = coverage, + seed = config.seed, + maxIterations = config.pbtMaxIterations, + timeBudget = config.pbtTimeBudget, + shrink = config.shrink, + ).run() + + pbtReport = PbtReport( + executions = pbt.stats.executions, + returned = pbt.stats.returned, + threw = pbt.stats.threw, + diverged = pbt.stats.diverged, + unsupported = pbt.stats.unsupported, + wallMs = (System.nanoTime() - pbtStart) / 1_000_000, + failures = pbt.failures.map { failure -> + FailureReport( + description = failure.description, + args = failure.args.map { it.toString() }, + shrunkArgs = failure.shrunkArgs.map { it.toString() }, + ) + }, + ) + + if (config.mode == AnalysisMode.HYBRID_WITH_HINTS) { + hints = pbt.typeProfiler.toHints() + } + } + + var symbolicReport: SymbolicReport? = null + + if (config.mode != AnalysisMode.PBT_ONLY) { + val symStart = System.nanoTime() + val symbolic = SymbolicPhase( + scene = scene, + method = method, + coverage = coverage, + hints = hints, + hintFallback = config.hintFallback, + perTargetTimeout = config.perTargetTimeout, + interproceduralAnalysis = config.interproceduralAnalysis, + ).run() + + symbolicReport = SymbolicReport( + targets = symbolic.outcomes.map { outcome -> + TargetReport( + branch = "${outcome.branch.ifStmt} -> ${outcome.branch.successor}", + reached = outcome.reached, + wallMs = outcome.wallMs, + steps = outcome.steps.toLong(), + hintsUsed = outcome.hintsUsed, + fallbackUsed = outcome.fallbackUsed, + replayConfirmed = outcome.replayConfirmed, + inputs = outcome.inputs?.parameters?.map { it.toString() }, + ) + }, + reached = symbolic.reachedCount, + wallMs = (System.nanoTime() - symStart) / 1_000_000, + ) + } + + val typeProfile: Map> = when { + hints != TsInputTypeHints.EMPTY -> + hints.byMethod[TsInputTypeHints.keyOf(method)] + ?.mapValues { (_, tags) -> tags.map { it.name }.sorted() } + .orEmpty() + + else -> emptyMap() + } + + return MethodReport( + method = method.signature.toString(), + totalStmts = coverage.allStmts.size, + totalBranches = coverage.allBranches.size, + coveredStmts = coverage.coveredStmtCount, + coveredBranches = coverage.coveredBranchCount, + stmtCoverage = coverage.stmtCoverage(), + branchCoverage = coverage.branchCoverage(), + timeline = coverage.timeline.map { + TimelinePoint(it.elapsedMs, it.phase, it.coveredStmts, it.coveredBranches) + }, + pbt = pbtReport, + symbolic = symbolicReport, + typeProfile = typeProfile, + totalWallMs = (System.nanoTime() - start) / 1_000_000, + ) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/PbtPhase.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/PbtPhase.kt new file mode 100644 index 0000000000..7804a938d0 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/PbtPhase.kt @@ -0,0 +1,147 @@ +package org.usvm.ts.pbt.hybrid + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.usvm.ts.pbt.coverage.CoverageTracker +import org.usvm.ts.pbt.gen.InputGenerator +import org.usvm.ts.pbt.gen.Shrinker +import org.usvm.ts.pbt.interpreter.EtsConcreteInterpreter +import org.usvm.ts.pbt.interpreter.ExecutionListener +import org.usvm.ts.pbt.interpreter.ExecutionResult +import org.usvm.ts.pbt.interpreter.VValue +import kotlin.random.Random +import kotlin.time.Duration +import kotlin.time.TimeSource + +private val logger = KotlinLogging.logger {} + +/** After this many executions that are *all* [ExecutionResult.Unsupported], give up on the method. */ +private const val UNSUPPORTED_BAILOUT_THRESHOLD = 25 + +/** + * The property (oracle) checked for every concrete execution. + * The default property is "the method does not throw". + */ +fun interface PbtProperty { + /** @return `null` if the property holds, otherwise a failure description. */ + fun check(args: List, result: ExecutionResult): String? + + companion object { + val NO_CRASH = PbtProperty { _, result -> + if (result is ExecutionResult.Threw) "unexpected throw: ${result.value}" else null + } + } +} + +data class PbtFailure( + val args: List, + val shrunkArgs: List, + val description: String, +) + +data class PbtStats( + val executions: Int, + val returned: Int, + val threw: Int, + val diverged: Int, + val unsupported: Int, + val elapsedMs: Long, +) + +class PbtResult( + val failures: List, + val stats: PbtStats, + val typeProfiler: TypeProfiler, +) + +/** + * Phase 1 of the hybrid analysis: random (property-based) testing of a method + * on the EtsIR level via the concrete interpreter, with coverage feedback. + */ +class PbtPhase( + private val scene: EtsScene, + private val method: EtsMethod, + private val coverage: CoverageTracker, + private val seed: Long = 0L, + private val maxIterations: Int = 2_000, + private val timeBudget: Duration = Duration.INFINITE, + private val property: PbtProperty = PbtProperty.NO_CRASH, + private val shrink: Boolean = true, +) { + fun run(): PbtResult { + val random = Random(seed) + val generator = InputGenerator(scene, method, random) + val interpreter = EtsConcreteInterpreter(scene) + val profiler = TypeProfiler() + val listener = ExecutionListener.composite(listOf(coverage, profiler)) + + val failures = mutableListOf() + val seenFailureKeys = mutableSetOf() + + var returned = 0 + var threw = 0 + var diverged = 0 + var unsupported = 0 + var executions = 0 + + val start = TimeSource.Monotonic.markNow() + coverage.phase = "pbt" + + while (executions < maxIterations && start.elapsedNow() < timeBudget) { + // Stop early once everything is covered — the symbolic phase has nothing to add + if (coverage.branchCoverage() == 1.0 && coverage.stmtCoverage() == 1.0) break + + // Bail out if the method is dominated by unmodeled constructs: + // burning the whole budget on Unsupported executions is pointless. + if (executions >= UNSUPPORTED_BAILOUT_THRESHOLD && unsupported == executions) break + + val thisValue = generator.generateThis() + val args = generator.generateArgs() + executions++ + + val result = interpreter.execute(method, thisValue, args, listener) + when (result) { + is ExecutionResult.Returned -> returned++ + is ExecutionResult.Threw -> threw++ + is ExecutionResult.Diverged -> diverged++ + is ExecutionResult.Unsupported -> { + unsupported++ + logger.debug { "unsupported: ${result.reason}" } + } + } + + if (result is ExecutionResult.Unsupported || result is ExecutionResult.Diverged) continue + + val violation = property.check(args, result) ?: continue + + // Deduplicate failures by their description (e.g. throw site + kind) + if (!seenFailureKeys.add(violation)) continue + + val shrunk = if (shrink) { + Shrinker().shrink(args) { candidate -> + val r = interpreter.execute(method, thisValue, candidate) + r !is ExecutionResult.Unsupported && r !is ExecutionResult.Diverged && + property.check(candidate, r) != null + } + } else args + + failures += PbtFailure(args, shrunk, violation) + } + + val stats = PbtStats( + executions = executions, + returned = returned, + threw = threw, + diverged = diverged, + unsupported = unsupported, + elapsedMs = start.elapsedNow().inWholeMilliseconds, + ) + logger.info { + "PBT phase for ${method.name}: $stats, " + + "stmt=${"%.1f".format(coverage.stmtCoverage() * 100)}%, " + + "branch=${"%.1f".format(coverage.branchCoverage() * 100)}%" + } + return PbtResult(failures, stats, profiler) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/SymbolicPhase.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/SymbolicPhase.kt new file mode 100644 index 0000000000..b1ad90f5ce --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/SymbolicPhase.kt @@ -0,0 +1,248 @@ +package org.usvm.ts.pbt.hybrid + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsParametersState +import org.usvm.api.targets.ReachabilityObserver +import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.api.targets.TsTarget +import org.usvm.machine.TsInputTypeHints +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.statistics.CompositeUMachineObserver +import org.usvm.statistics.StepsStatistics +import org.usvm.statistics.UMachineObserver +import org.usvm.ts.pbt.coverage.CoverageTracker +import org.usvm.ts.pbt.interpreter.EtsConcreteInterpreter +import org.usvm.ts.pbt.interpreter.ExecutionListener +import org.usvm.ts.pbt.interpreter.ExecutionResult +import org.usvm.ts.pbt.interpreter.VUndefined +import org.usvm.ts.pbt.report.toVValueOrNull +import org.usvm.util.TsTestResolver +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +private val logger = KotlinLogging.logger {} + +/** + * Construction of reachability target chains for uncovered branches. + * + * For an uncovered edge `(I, S)` the chain is + * `InitialPoint(entry) -> IntermediatePoint(I) -> FinalPoint(S)`; + * `ReachabilityObserver` advances a state through the chain as the + * corresponding statements are executed. + */ +object TargetBuilder { + fun forBranch(method: EtsMethod, branch: CoverageTracker.BranchEdge): TsTarget { + val root: TsTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + root.addChild(TsReachabilityTarget.IntermediatePoint(branch.ifStmt)) + .addChild(TsReachabilityTarget.FinalPoint(branch.successor)) + return root + } +} + +/** + * Captures the first state whose target set contains a reached terminal target. + * + * Note: the machine's own `TargetsReachedStatesCollector` only inspects + * *terminated* states, and `stopOnTargetsReached` halts the machine as soon as + * the target tree is fully removed — usually *before* the reaching state gets a + * chance to terminate. Capturing at propagation time avoids the race. This + * observer must be placed *after* [ReachabilityObserver] in the composite. + */ +private class ReachingStateCaptor : UMachineObserver { + var captured: TsState? = null + private set + + private fun check(state: TsState) { + if (captured == null && state.targets.reachedTerminal.isNotEmpty()) { + captured = state + } + } + + override fun onState(parent: TsState, forks: Sequence) { + check(parent) + forks.forEach { check(it) } + } + + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + if (stateReachable) check(state) + } +} + +data class TargetOutcome( + val branch: CoverageTracker.BranchEdge, + val reached: Boolean, + val wallMs: Long, + val steps: ULong, + val hintsUsed: Boolean, + val fallbackUsed: Boolean, + /** Input valuation extracted from the reaching state, when resolvable. */ + val inputs: TsParametersState?, + val replayConfirmed: Boolean, +) + +class SymbolicPhaseResult( + val outcomes: List, +) { + val reachedCount: Int get() = outcomes.count { it.reached } +} + +/** + * Phase 2 of the hybrid analysis: for every branch the PBT phase failed to cover, + * run the usvm-ts machine in targeted mode, extract concrete inputs from the + * reaching state, and replay them on the concrete interpreter to confirm + * (and merge) the coverage. + * + * One machine run per target: `TargetsReachedStopStrategy` only stops when *all* + * targets are reached, so batching would let a single infeasible branch consume + * the whole time budget. + */ +class SymbolicPhase( + private val scene: EtsScene, + private val method: EtsMethod, + private val coverage: CoverageTracker, + private val hints: TsInputTypeHints = TsInputTypeHints.EMPTY, + private val hintFallback: Boolean = true, + private val perTargetTimeout: Duration = 20.seconds, + private val interproceduralAnalysis: Boolean = true, +) { + fun run(): SymbolicPhaseResult { + coverage.phase = "symbolic" + val outcomes = mutableListOf() + + for (uncovered in coverage.uncoveredBranches()) { + if (coverage.isCovered(uncovered.edge)) continue // covered by an earlier target's replay + + val useHints = hints != TsInputTypeHints.EMPTY + var outcome = attemptTarget(uncovered, if (useHints) hints else TsInputTypeHints.EMPTY) + + if (!outcome.reached && useHints && hintFallback) { + logger.info { "target not reached with hints, falling back: ${uncovered.edge}" } + val fallback = attemptTarget(uncovered, TsInputTypeHints.EMPTY) + outcome = fallback.copy( + wallMs = outcome.wallMs + fallback.wallMs, + fallbackUsed = true, + ) + } + outcomes += outcome + } + return SymbolicPhaseResult(outcomes) + } + + private fun attemptTarget( + uncovered: CoverageTracker.UncoveredBranch, + hints: TsInputTypeHints, + ): TargetOutcome { + val start = System.nanoTime() + val stepsStats = StepsStatistics() + val captor = ReachingStateCaptor() + + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + stopOnTargetsReached = true, + exceptionsPropagation = true, + timeout = perTargetTimeout, + solverType = SolverType.YICES, + ) + val tsOptions = TsOptions( + interproceduralAnalysis = interproceduralAnalysis, + inputTypeHints = hints, + ) + + val target = TargetBuilder.forBranch(uncovered.method, uncovered.edge) + + try { + TsMachine( + scene, + options, + tsOptions, + // Order matters: the captor must observe *after* target propagation + machineObserver = CompositeUMachineObserver(ReachabilityObserver(), captor, stepsStats), + ).use { machine -> + machine.analyze(listOf(method), listOf(target)) + } + } catch (e: Throwable) { + // e.g. UNSAT initial constraints under too-restrictive hints + logger.warn { "symbolic run failed for ${uncovered.edge}: $e" } + } + + val wallMs = (System.nanoTime() - start) / 1_000_000 + val hintsUsed = hints != TsInputTypeHints.EMPTY + val state = captor.captured + ?: return TargetOutcome( + branch = uncovered.edge, + reached = false, + wallMs = wallMs, + steps = stepsStats.totalSteps, + hintsUsed = hintsUsed, + fallbackUsed = false, + inputs = null, + replayConfirmed = false, + ) + + val inputs = try { + TsTestResolver().resolveInputs(method, state) + } catch (e: Throwable) { + logger.warn { "input resolution failed for ${uncovered.edge}: $e" } + null + } + + val replayConfirmed = inputs?.let { replay(it, uncovered.edge) } ?: false + if (!replayConfirmed) { + // Fall back to the symbolic trace for coverage accounting + mergeSymbolicTrace(state) + } + + return TargetOutcome( + branch = uncovered.edge, + reached = true, + wallMs = wallMs, + steps = stepsStats.totalSteps, + hintsUsed = hintsUsed, + fallbackUsed = false, + inputs = inputs, + replayConfirmed = replayConfirmed, + ) + } + + /** Replay extracted inputs concretely; returns true if the target edge was actually taken. */ + private fun replay(inputs: TsParametersState, edge: CoverageTracker.BranchEdge): Boolean { + val classResolver = { name: String -> + scene.projectAndSdkClasses.firstOrNull { it.name == name } + } + val thisValue = inputs.thisInstance?.toVValueOrNull(classResolver) ?: VUndefined + val args = inputs.parameters.map { + it.toVValueOrNull(classResolver) ?: return false + } + + var edgeTaken = false + val probe = object : ExecutionListener { + override fun onBranch(ifStmt: EtsIfStmt, taken: EtsStmt, condition: Boolean) { + if (ifStmt == edge.ifStmt && taken == edge.successor) edgeTaken = true + } + } + + val interpreter = EtsConcreteInterpreter(scene) + val result = interpreter.execute( + method, + thisValue, + args, + ExecutionListener.composite(listOf(coverage, probe)), + ) + if (result is ExecutionResult.Unsupported) return false + return edgeTaken + } + + private fun mergeSymbolicTrace(state: TsState) { + val trace: List = state.pathNode.allStatements.toList().asReversed() + coverage.mergeTrace(trace) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/TypeProfiler.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/TypeProfiler.kt new file mode 100644 index 0000000000..3a53ca1682 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/hybrid/TypeProfiler.kt @@ -0,0 +1,51 @@ +package org.usvm.ts.pbt.hybrid + +import org.jacodb.ets.model.EtsMethod +import org.usvm.machine.TsHintType +import org.usvm.machine.TsInputTypeHints +import org.usvm.ts.pbt.interpreter.ExecutionListener +import org.usvm.ts.pbt.interpreter.VArray +import org.usvm.ts.pbt.interpreter.VBool +import org.usvm.ts.pbt.interpreter.VNamespace +import org.usvm.ts.pbt.interpreter.VNull +import org.usvm.ts.pbt.interpreter.VNumber +import org.usvm.ts.pbt.interpreter.VObject +import org.usvm.ts.pbt.interpreter.VString +import org.usvm.ts.pbt.interpreter.VUndefined +import org.usvm.ts.pbt.interpreter.VValue + +/** + * Records the runtime types of method inputs observed during the concrete (PBT) + * phase. The result feeds the symbolic phase as [TsInputTypeHints]. + * + * NOTE: profiles reflect the *generator's* type distribution for the entry method + * (every generated type shows up). Their pruning power comes from methods whose + * parameters have declared/inferable structure, and from *call-site* profiles of + * transitively invoked methods, where observed types reflect actual data flow. + */ +class TypeProfiler : ExecutionListener { + + private val observed = mutableMapOf>>() + + override fun onMethodEnter(method: EtsMethod, thisValue: VValue, args: List) { + val perParam = observed.getOrPut(TsInputTypeHints.keyOf(method)) { mutableMapOf() } + args.forEachIndexed { i, arg -> + perParam.getOrPut(i) { mutableSetOf() } += tagOf(arg) + } + } + + fun toHints(): TsInputTypeHints = + TsInputTypeHints(observed.mapValues { (_, m) -> m.mapValues { (_, s) -> s.toSet() } }) + + companion object { + fun tagOf(v: VValue): TsHintType = when (v) { + is VNumber -> TsHintType.NUMBER + is VBool -> TsHintType.BOOLEAN + is VString -> TsHintType.STRING + VNull -> TsHintType.NULL + VUndefined -> TsHintType.UNDEFINED + is VArray -> TsHintType.ARRAY + else -> TsHintType.OBJECT // objects, namespaces, functions, maps, sets + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/CallResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/CallResolver.kt new file mode 100644 index 0000000000..4d202ee1f1 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/CallResolver.kt @@ -0,0 +1,118 @@ +package org.usvm.ts.pbt.interpreter + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME + +/** + * Concrete callee resolution over an [EtsScene]. + * + * Mirrors (in a simplified form) the name-based virtual dispatch of + * `org.usvm.machine.interpreter.TsInterpreter.visitVirtualMethodCall`: + * the runtime class of the receiver is looked up first, then its ancestors. + */ +internal class CallResolver(private val scene: EtsScene) { + + private val classesByName: Map> by lazy { + (scene.projectClasses + scene.sdkClasses).groupBy { it.name } + } + + fun classByName(name: String): EtsClass? = classesByName[name]?.firstOrNull() + + fun classBySignature(signature: EtsClassSignature): EtsClass? { + val candidates = classesByName[signature.name] ?: return null + return candidates.firstOrNull { it.signature == signature } ?: candidates.firstOrNull() + } + + /** Resolve an instance method by name on [cls], walking the superclass chain. */ + fun resolveInstanceMethod(cls: EtsClass, name: String): EtsMethod? { + var current: EtsClass? = cls + val visited = mutableSetOf() + while (current != null && visited.add(current.name)) { + current.methods.firstOrNull { it.name == name && it.cfg.stmts.isNotEmpty() } + ?.let { return it } + current = current.superClass?.let { classBySignature(it) } + } + return null + } + + /** Resolve a static call target (including free functions in the default class). */ + fun resolveStaticMethod(callee: EtsMethodSignature): EtsMethod? { + val className = callee.enclosingClass.name + val candidates = if (className.isBlank() || className == DEFAULT_ARK_CLASS_NAME) { + // Free function: search default classes across the scene files + classesByName[DEFAULT_ARK_CLASS_NAME].orEmpty() + } else { + classesByName[className].orEmpty() + } + for (cls in candidates) { + cls.methods.firstOrNull { it.name == callee.name && it.cfg.stmts.isNotEmpty() } + ?.let { return it } + } + // Last resort: a unique method with this name anywhere in the project + val global = scene.projectClasses + .flatMap { it.methods } + .filter { it.name == callee.name && it.cfg.stmts.isNotEmpty() } + return global.singleOrNull() + } + + /** + * Variable-name -> method aliases for function values. + * + * Front ends lower `const f = (...) => ...` into an anonymous method + * (`%AM0$...`) plus an assignment `f := %AM0$...` (a local of a + * [EtsFunctionType] whose signature points to the actual method) inside the + * file-initializer (`%dflt::%dflt`). A later `ptr_call f(...)` carries only + * the *variable* name in its callee signature; this map recovers the target. + */ + private val functionAliases: Map by lazy { + val aliases = mutableMapOf() + for (cls in scene.projectClasses) { + if (cls.name != DEFAULT_ARK_CLASS_NAME) continue + val fileInit = cls.methods.firstOrNull { it.name == DEFAULT_ARK_METHOD_NAME } ?: continue + for (stmt in fileInit.cfg.stmts) { + if (stmt !is EtsAssignStmt) continue + val lhv = stmt.lhv as? EtsLocal ?: continue + val rhv = stmt.rhv as? EtsLocal ?: continue + val fnType = rhv.type as? EtsFunctionType ?: continue + val target = cls.methods.firstOrNull { it.name == fnType.signature.name } + ?: classByName(fnType.signature.enclosingClass.name) + ?.methods?.firstOrNull { it.name == fnType.signature.name } + if (target != null && target.cfg.stmts.isNotEmpty()) { + aliases.putIfAbsent(lhv.name, target) + } + } + } + aliases + } + + /** Resolve a `ptr_call` target: by function-value alias, then by literal name. */ + fun resolveFunctionPointer(callee: EtsMethodSignature): EtsMethod? = + functionAliases[callee.name] ?: resolveStaticMethod(callee) + + /** The method behind a file-level `const f = (...) => ...` binding, if any. */ + fun functionAliasFor(name: String): EtsMethod? = functionAliases[name] + + /** + * Resolve the method behind a [EtsFunctionType]-typed value (a function literal: + * the type signature carries the anonymous method name and its declaring class). + */ + fun methodByFunctionType(type: EtsFunctionType): EtsMethod? { + val sig = type.signature + if (sig.name.isBlank()) return null + val declared = classBySignature(sig.enclosingClass) + ?.methods?.firstOrNull { it.name == sig.name && it.cfg.stmts.isNotEmpty() } + if (declared != null) return declared + return scene.projectClasses + .flatMap { it.methods } + .filter { it.name == sig.name && it.cfg.stmts.isNotEmpty() } + .singleOrNull() + } +} 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 new file mode 100644 index 0000000000..0067fe2050 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/EtsConcreteInterpreter.kt @@ -0,0 +1,626 @@ +package org.usvm.ts.pbt.interpreter + +import org.jacodb.ets.model.EtsAddExpr +import org.jacodb.ets.model.EtsAndExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBitAndExpr +import org.jacodb.ets.model.EtsBitNotExpr +import org.jacodb.ets.model.EtsBitOrExpr +import org.jacodb.ets.model.EtsBitXorExpr +import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsDivExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsEqExpr +import org.jacodb.ets.model.EtsExpExpr +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsGlobalRef +import org.jacodb.ets.model.EtsGtEqExpr +import org.jacodb.ets.model.EtsGtExpr +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLValue +import org.jacodb.ets.model.EtsLeftShiftExpr +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsLtEqExpr +import org.jacodb.ets.model.EtsLtExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsMulExpr +import org.jacodb.ets.model.EtsNegExpr +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsNotEqExpr +import org.jacodb.ets.model.EtsNotExpr +import org.jacodb.ets.model.EtsNullConstant +import org.jacodb.ets.model.EtsNullishCoalescingExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsOrExpr +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPostDecExpr +import org.jacodb.ets.model.EtsPostIncExpr +import org.jacodb.ets.model.EtsPreDecExpr +import org.jacodb.ets.model.EtsPreIncExpr +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRemExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsRightShiftExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStrictEqExpr +import org.jacodb.ets.model.EtsStrictNotEqExpr +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsSubExpr +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsTypeOfExpr +import org.jacodb.ets.model.EtsUnaryPlusExpr +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedConstant +import org.jacodb.ets.model.EtsUnsignedRightShiftExpr +import org.jacodb.ets.model.EtsVoidExpr +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import kotlin.math.floor + +/** + * A concrete (non-symbolic) interpreter for EtsIR. + * + * Executes an [EtsMethod] CFG with concrete [VValue] inputs — the execution + * vehicle of the PBT phase of the hybrid analysis. Anything the interpreter + * does not model is surfaced as [ExecutionResult.Unsupported], never as a + * silently wrong value. + */ +class EtsConcreteInterpreter( + private val scene: EtsScene, + private val limits: ExecutionLimits = ExecutionLimits(), +) { + private val resolver = CallResolver(scene) + + fun execute( + method: EtsMethod, + thisValue: VValue = VUndefined, + args: List = emptyList(), + listener: ExecutionListener = ExecutionListener.NONE, + ): ExecutionResult { + val execution = Execution(listener) + return try { + ExecutionResult.Returned(execution.runMethod(method, thisValue, args)) + } catch (e: JsThrowSignal) { + ExecutionResult.Threw(e.value) + } catch (e: UnsupportedFeatureSignal) { + ExecutionResult.Unsupported(e.reason) + } catch (e: BudgetExceededSignal) { + ExecutionResult.Diverged(e.reason) + } catch (e: StackOverflowError) { + ExecutionResult.Diverged("JVM stack overflow (deep recursion)") + } + } + + private class Frame( + val method: EtsMethod, + val thisValue: VValue, + val args: List, + val locals: MutableMap = mutableMapOf(), + ) + + private inner class Execution(val listener: ExecutionListener) { + var steps: Long = 0 + var callDepth: Int = 0 + val statics: MutableMap> = mutableMapOf() + + fun runMethod(method: EtsMethod, thisValue: VValue, args: List): VValue { + if (callDepth >= limits.maxCallDepth) { + throw BudgetExceededSignal("max call depth ${limits.maxCallDepth} exceeded at ${method.name}") + } + val stmts = method.cfg.stmts + if (stmts.isEmpty()) { + throw UnsupportedFeatureSignal("method without body: ${method.signature}") + } + + callDepth++ + listener.onMethodEnter(method, thisValue, args) + try { + val frame = Frame(method, thisValue, args) + var pc: EtsStmt? = stmts.first() + + while (pc != null) { + if (++steps > limits.maxSteps) { + throw BudgetExceededSignal("step budget ${limits.maxSteps} exceeded") + } + listener.onStmt(pc) + + when (val stmt = pc) { + is EtsNopStmt -> pc = next(method, stmt) + + is EtsAssignStmt -> { + val value = eval(stmt.rhv, frame) + assign(stmt.lhv, value, frame) + pc = next(method, stmt) + } + + is EtsCallStmt -> { + evalCall(stmt.expr, frame) + pc = next(method, stmt) + } + + is EtsIfStmt -> { + val condition = JsSemantics.truthy(eval(stmt.condition, frame)) + val successors = method.cfg.successors(stmt).toList() + if (successors.size != 2) { + throw UnsupportedFeatureSignal( + "if-stmt with ${successors.size} successors: $stmt" + ) + } + // Ordered: first = true branch, second = false branch + val taken = if (condition) successors[0] else successors[1] + listener.onBranch(stmt, taken, condition) + pc = taken + } + + is EtsReturnStmt -> { + val result = stmt.returnValue?.let { eval(it, frame) } ?: VUndefined + listener.onMethodExit(method, result) + return result + } + + is EtsThrowStmt -> { + throw JsThrowSignal(eval(stmt.exception, frame)) + } + + else -> throw UnsupportedFeatureSignal("statement kind: ${stmt::class.simpleName} ($stmt)") + } + } + + // CFG ended without an explicit return + listener.onMethodExit(method, VUndefined) + return VUndefined + } finally { + callDepth-- + } + } + + private fun next(method: EtsMethod, stmt: EtsStmt): EtsStmt? = + method.cfg.successors(stmt).firstOrNull() + + // --------------------------------------------------------------- + // Expression evaluation + // --------------------------------------------------------------- + + fun eval(e: EtsEntity, frame: Frame): VValue = when (e) { + // Immediates + is EtsLocal -> frame.locals[e.name] + ?: frame.args.getOrNull(parameterIndexOfLocal(frame, e.name) ?: -1) + ?: functionValueOf(e) + ?: VUndefined + + is EtsNumberConstant -> VNumber(e.value) + is EtsStringConstant -> VString(e.value) + is EtsBooleanConstant -> VBool(e.value) + EtsNullConstant -> VNull + EtsUndefinedConstant -> VUndefined + + // Refs + is EtsThis -> frame.thisValue + is EtsParameterRef -> frame.args.getOrElse(e.index) { VUndefined } + is EtsArrayAccess -> readArray(eval(e.array, frame), eval(e.index, frame)) + is EtsInstanceFieldRef -> readField(eval(e.instance, frame), e.field.name) + is EtsStaticFieldRef -> readStaticField(e) + is EtsGlobalRef -> + if (e.name in Intrinsics.NAMESPACES) VNamespace(e.name) + else throw UnsupportedFeatureSignal("global ref: ${e.name}") + + // Allocation + is EtsNewExpr -> newObject(e) + is EtsNewArrayExpr -> { + val size = JsSemantics.toNumber(eval(e.size, frame)) + if (size.isNaN() || size < 0 || size != floor(size)) { + throw JsThrowSignal(VString("RangeError: Invalid array length")) + } + VArray(MutableList(size.toInt()) { VUndefined }) + } + + // Unary + is EtsNotExpr -> VBool(!JsSemantics.truthy(eval(e.arg, frame))) + is EtsNegExpr -> VNumber(-JsSemantics.toNumber(eval(e.arg, frame))) + is EtsUnaryPlusExpr -> VNumber(JsSemantics.toNumber(eval(e.arg, frame))) + is EtsBitNotExpr -> VNumber(JsSemantics.toInt32(eval(e.arg, frame)).inv().toDouble()) + is EtsTypeOfExpr -> VString(JsSemantics.typeOf(eval(e.arg, frame))) + is EtsVoidExpr -> { + eval(e.arg, frame) + VUndefined + } + + is EtsPreIncExpr -> incDec(e.arg, frame, delta = 1.0, returnNew = true) + is EtsPreDecExpr -> incDec(e.arg, frame, delta = -1.0, returnNew = true) + is EtsPostIncExpr -> incDec(e.arg, frame, delta = 1.0, returnNew = false) + is EtsPostDecExpr -> incDec(e.arg, frame, delta = -1.0, returnNew = false) + + is EtsCastExpr -> eval(e.arg, frame) + is EtsInstanceOfExpr -> VBool(instanceOf(eval(e.arg, frame), e)) + + // Binary: arithmetic + is EtsAddExpr -> JsSemantics.add(eval(e.left, frame), eval(e.right, frame)) + is EtsSubExpr -> numeric(e.left, e.right, frame) { a, b -> a - b } + is EtsMulExpr -> numeric(e.left, e.right, frame) { a, b -> a * b } + is EtsDivExpr -> numeric(e.left, e.right, frame) { a, b -> a / b } + is EtsRemExpr -> numeric(e.left, e.right, frame) { a, b -> a % b } + is EtsExpExpr -> numeric(e.left, e.right, frame) { a, b -> Math.pow(a, b) } + + // Binary: bitwise / shifts + is EtsBitAndExpr -> int32(e.left, e.right, frame) { a, b -> a and b } + is EtsBitOrExpr -> int32(e.left, e.right, frame) { a, b -> a or b } + is EtsBitXorExpr -> int32(e.left, e.right, frame) { a, b -> a xor b } + is EtsLeftShiftExpr -> int32(e.left, e.right, frame) { a, b -> a shl (b and 31) } + is EtsRightShiftExpr -> int32(e.left, e.right, frame) { a, b -> a shr (b and 31) } + is EtsUnsignedRightShiftExpr -> { + val a = JsSemantics.toUint32(eval(e.left, frame)) + val b = JsSemantics.toInt32(eval(e.right, frame)) and 31 + VNumber((a ushr b).toDouble()) + } + + // 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))) + is EtsLtEqExpr -> VBool(JsSemantics.le(eval(e.left, frame), eval(e.right, frame))) + is EtsGtExpr -> VBool(JsSemantics.gt(eval(e.left, frame), eval(e.right, frame))) + is EtsGtEqExpr -> VBool(JsSemantics.ge(eval(e.left, frame), eval(e.right, frame))) + is EtsInExpr -> VBool(JsSemantics.inOp(eval(e.left, frame), eval(e.right, frame))) + + // Binary: logical (operands are pre-flattened locals in 3AC, eager evaluation is safe) + is EtsAndExpr -> { + val l = eval(e.left, frame) + if (JsSemantics.truthy(l)) eval(e.right, frame) else l + } + + is EtsOrExpr -> { + val l = eval(e.left, frame) + if (JsSemantics.truthy(l)) l else eval(e.right, frame) + } + + is EtsNullishCoalescingExpr -> { + val l = eval(e.left, frame) + if (l == VNull || l == VUndefined) eval(e.right, frame) else l + } + + // Calls + is EtsCallExpr -> evalCall(e, frame) + + else -> throw UnsupportedFeatureSignal("expression kind: ${e::class.simpleName} ($e)") + } + + /** A local that was never assigned may actually be a named parameter. */ + 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 + + /** + * A local of a function type that was never assigned is a function + * *literal reference*: its type signature names the lowered method + * (e.g. `factorial := %AM0$%dflt` in the file initializer). + */ + private fun functionValueOf(e: EtsLocal): VValue? { + val fnType = e.type as? EtsFunctionType ?: return null + val method = resolver.methodByFunctionType(fnType) + ?: resolver.resolveFunctionPointer(fnType.signature) + ?: resolver.functionAliasFor(e.name) + ?: return null + return VFunction(method) + } + + private inline fun numeric( + left: EtsEntity, + right: EtsEntity, + frame: Frame, + op: (Double, Double) -> Double, + ): VNumber = VNumber(op(JsSemantics.toNumber(eval(left, frame)), JsSemantics.toNumber(eval(right, frame)))) + + private inline fun int32( + left: EtsEntity, + right: EtsEntity, + frame: Frame, + op: (Int, Int) -> Int, + ): VNumber = VNumber(op(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame))).toDouble()) + + private fun incDec(arg: EtsEntity, frame: Frame, delta: Double, returnNew: Boolean): VValue { + if (arg !is EtsLocal) { + throw UnsupportedFeatureSignal("inc/dec on non-local: $arg") + } + val old = JsSemantics.toNumber(eval(arg, frame)) + val new = old + delta + frame.locals[arg.name] = VNumber(new) + return VNumber(if (returnNew) new else old) + } + + private fun instanceOf(v: VValue, e: EtsInstanceOfExpr): Boolean { + val typeName = when (val t = e.checkType) { + is EtsClassType -> t.signature.name + is EtsUnclearRefType -> t.name + else -> return false + } + return when (v) { + is VArray -> typeName == "Array" + is VMap -> typeName == "Map" + is VSet -> typeName == "Set" + is VFunction -> typeName == "Function" + is VObject -> { + var cls = v.cls + val visited = mutableSetOf() + while (cls != null && visited.add(cls.name)) { + if (cls.name == typeName) return true + cls = cls.superClass?.let { resolver.classBySignature(it) } + } + typeName == "Object" + } + + else -> false + } + } + + // --------------------------------------------------------------- + // Heap access + // --------------------------------------------------------------- + + private fun readArray(array: VValue, index: VValue): VValue = when (array) { + is VArray -> { + val i = JsSemantics.toNumber(index) + if (i == floor(i) && i >= 0 && i < array.elements.size) array.elements[i.toInt()] else VUndefined + } + + is VString -> { + val i = JsSemantics.toNumber(index) + if (i == floor(i) && i >= 0 && i < array.value.length) VString(array.value[i.toInt()].toString()) + else VUndefined + } + + VNull, VUndefined -> throw typeError("cannot read index of ${JsSemantics.toStringJs(array)}") + + is VObject -> array.fields[JsSemantics.toStringJs(index)] ?: VUndefined + + else -> VUndefined + } + + private fun readField(instance: VValue, name: String): VValue = when (instance) { + is VObject -> instance.fields[name] ?: VUndefined + is VArray -> if (name == "length") VNumber(instance.elements.size.toDouble()) else VUndefined + is VString -> if (name == "length") VNumber(instance.value.length.toDouble()) else VUndefined + is VMap -> if (name == "size") VNumber(instance.entries.size.toDouble()) else VUndefined + is VSet -> if (name == "size") VNumber(instance.elements.size.toDouble()) else VUndefined + is VNamespace -> Intrinsics.namespaceField(instance.name, name) + ?: throw UnsupportedFeatureSignal("namespace field: ${instance.name}.$name") + + VNull, VUndefined -> + throw typeError("cannot read property '$name' of ${JsSemantics.toStringJs(instance)}") + + else -> VUndefined + } + + private fun readStaticField(ref: EtsStaticFieldRef): VValue { + val className = ref.field.enclosingClass.name + Intrinsics.namespaceField(className, ref.field.name)?.let { return it } + return statics[className]?.get(ref.field.name) ?: VUndefined + } + + private fun newObject(e: EtsNewExpr): VValue { + val typeName = when (val t = e.type) { + is EtsClassType -> t.signature.name + is EtsUnclearRefType -> t.name + else -> null + } + val cls = when (val t = e.type) { + is EtsClassType -> resolver.classBySignature(t.signature) + is EtsUnclearRefType -> resolver.classByName(t.name) + else -> null + } + if (cls == null) { + // Built-in containers are not scene classes + when (typeName) { + "Array" -> return VArray() + "Map" -> return VMap() + "Set" -> return VSet() + } + } + return VObject(cls) + } + + private fun assign(lhv: EtsLValue, value: VValue, frame: Frame) { + when (lhv) { + is EtsLocal -> frame.locals[lhv.name] = value + + is EtsArrayAccess -> { + val target = eval(lhv.array, frame) + val i = JsSemantics.toNumber(eval(lhv.index, frame)) + when (target) { + is VArray -> { + if (i != floor(i) || i < 0) return // JS silently allows sparse/weird keys; skip + val idx = i.toInt() + while (target.elements.size <= idx) target.elements.add(VUndefined) + target.elements[idx] = value + } + + is VObject -> target.fields[JsSemantics.numberToString(i)] = value + + VNull, VUndefined -> throw typeError("cannot set index of ${JsSemantics.toStringJs(target)}") + + else -> Unit // writes to primitives are silently ignored in JS + } + } + + is EtsInstanceFieldRef -> { + when (val target = eval(lhv.instance, frame)) { + is VObject -> target.fields[lhv.field.name] = value + + 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) + } + + VNull, VUndefined -> + throw typeError("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}") + + else -> Unit + } + } + + is EtsStaticFieldRef -> { + statics.getOrPut(lhv.field.enclosingClass.name) { mutableMapOf() }[lhv.field.name] = value + } + + else -> throw UnsupportedFeatureSignal("assignment target: ${lhv::class.simpleName} ($lhv)") + } + } + + // --------------------------------------------------------------- + // Calls + // --------------------------------------------------------------- + + fun evalCall(expr: EtsCallExpr, frame: Frame): VValue { + val args = expr.args.map { eval(it, frame) } + + return when (expr) { + is EtsInstanceCallExpr -> { + val receiver = eval(expr.instance, frame) + val name = expr.callee.name + + if (receiver is VNamespace) { + return Intrinsics.callNamespace(receiver.name, name, args) + ?: throw UnsupportedFeatureSignal("intrinsic: ${receiver.name}.$name") + } + + // Namespace receiver referenced by its bare local name (Math, console, ...) + if (receiver == VUndefined && expr.instance.name in Intrinsics.NAMESPACES) { + return Intrinsics.callNamespace(expr.instance.name, name, args) + ?: throw UnsupportedFeatureSignal("intrinsic: ${expr.instance.name}.$name") + } + + if (receiver == VNull || receiver == VUndefined) { + throw typeError("cannot call '$name' of ${JsSemantics.toStringJs(receiver)}") + } + + if (receiver is VObject && receiver.cls != null) { + val callee = resolver.resolveInstanceMethod(receiver.cls, name) + if (callee != null) { + return runMethod(callee, receiver, padArgs(callee, args)) + } + } + + // Constructors of classes outside the scene. + if (name == CONSTRUCTOR_NAME) { + when (receiver) { + is VObject -> { + // e.g. `new Error(msg)`: model as record initialization + args.firstOrNull()?.let { receiver.fields["message"] = it } + return receiver + } + + is VArray -> { + // `new Array(n)` / `new Array(a, b, ...)` + if (args.size == 1 && args[0] is VNumber) { + val n = (args[0] as VNumber).value + if (n == floor(n) && n >= 0) { + receiver.elements.clear() + repeat(n.toInt()) { receiver.elements.add(VUndefined) } + } else { + throw JsThrowSignal(VString("RangeError: Invalid array length")) + } + } else { + receiver.elements.clear() + receiver.elements.addAll(args) + } + return receiver + } + + is VMap, is VSet -> { + if (args.isEmpty() || args[0] == VUndefined || args[0] == VNull) return receiver + if (receiver is VSet && args[0] is VArray) { + (args[0] as VArray).elements.forEach { receiver.elements.add(it) } + return receiver + } + throw UnsupportedFeatureSignal("iterable constructor argument for Map/Set") + } + + else -> Unit + } + } + + Intrinsics.callInstance(receiver, name, args, ::invokeFunction) + ?: throw UnsupportedFeatureSignal( + "instance method: $name on ${receiver::class.simpleName}" + ) + } + + is EtsStaticCallExpr -> { + val className = expr.callee.enclosingClass.name + + Intrinsics.callNamespace(className, expr.callee.name, args)?.let { return it } + Intrinsics.callConversion(expr.callee.name, args)?.let { return it } + + val callee = resolver.resolveStaticMethod(expr.callee) + ?: throw UnsupportedFeatureSignal("static callee not found: ${expr.callee}") + runMethod(callee, VUndefined, padArgs(callee, args)) + } + + is EtsPtrCallExpr -> { + // Prefer the dynamic function value held by the pointer local + val ptrValue = eval(expr.ptr, frame) + if (ptrValue is VFunction) { + runMethod(ptrValue.method, ptrValue.thisValue, padArgs(ptrValue.method, args)) + } else { + val callee = resolver.resolveFunctionPointer(expr.callee) + if (callee != null) { + runMethod(callee, frame.thisValue, padArgs(callee, args)) + } else { + Intrinsics.callConversion(expr.callee.name, args) + ?: throw UnsupportedFeatureSignal("ptr call: ${expr.callee.name}") + } + } + } + + else -> throw UnsupportedFeatureSignal("call kind: ${expr::class.simpleName}") + } + } + + private fun padArgs(callee: EtsMethod, args: List): List { + if (args.size >= callee.parameters.size) return args + return args + List(callee.parameters.size - args.size) { VUndefined } + } + + /** Host callback for higher-order intrinsics (`arr.map(f)`, `map.forEach(f)`, ...). */ + private fun invokeFunction(fn: VFunction, args: List): VValue = + runMethod(fn.method, fn.thisValue, padArgs(fn.method, args)) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionListener.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionListener.kt new file mode 100644 index 0000000000..490587675d --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionListener.kt @@ -0,0 +1,35 @@ +package org.usvm.ts.pbt.interpreter + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt + +/** + * Observation hooks for concrete execution. + * Coverage tracking and runtime type profiling are implemented as listeners. + */ +interface ExecutionListener { + fun onMethodEnter(method: EtsMethod, thisValue: VValue, args: List) {} + fun onMethodExit(method: EtsMethod, result: VValue) {} + fun onStmt(stmt: EtsStmt) {} + fun onBranch(ifStmt: EtsIfStmt, taken: EtsStmt, condition: Boolean) {} + + companion object { + val NONE: ExecutionListener = object : ExecutionListener {} + + fun composite(listeners: List): ExecutionListener = + object : ExecutionListener { + override fun onMethodEnter(method: EtsMethod, thisValue: VValue, args: List) = + listeners.forEach { it.onMethodEnter(method, thisValue, args) } + + override fun onMethodExit(method: EtsMethod, result: VValue) = + listeners.forEach { it.onMethodExit(method, result) } + + override fun onStmt(stmt: EtsStmt) = + listeners.forEach { it.onStmt(stmt) } + + override fun onBranch(ifStmt: EtsIfStmt, taken: EtsStmt, condition: Boolean) = + listeners.forEach { it.onBranch(ifStmt, taken, condition) } + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionResult.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionResult.kt new file mode 100644 index 0000000000..43bf0990ab --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/ExecutionResult.kt @@ -0,0 +1,52 @@ +package org.usvm.ts.pbt.interpreter + +/** + * Outcome of one concrete execution of an [org.jacodb.ets.model.EtsMethod]. + * + * The default PBT property is "the result is not [Threw]". + * [Diverged] and [Unsupported] are *neither* a pass nor a failure: they are + * reported separately so that the experiment numbers stay honest. + */ +sealed interface ExecutionResult { + data class Returned(val value: VValue) : ExecutionResult + + /** A JS-level `throw` (including modeled TypeErrors, e.g. field access on undefined). */ + data class Threw(val value: VValue) : ExecutionResult + + /** Execution exceeded [ExecutionLimits] (step budget / call depth). */ + data class Diverged(val reason: String) : ExecutionResult + + /** The interpreter hit an IR construct or intrinsic it does not model. */ + data class Unsupported(val reason: String) : ExecutionResult +} + +data class ExecutionLimits( + val maxSteps: Long = 100_000, + val maxCallDepth: Int = 64, +) + +/** Internal control-flow signal: JS `throw`. */ +internal class JsThrowSignal(val value: VValue) : RuntimeException() { + override fun fillInStackTrace(): Throwable = this +} + +/** Internal control-flow signal: unsupported IR construct. */ +internal class UnsupportedFeatureSignal(val reason: String) : RuntimeException(reason) { + override fun fillInStackTrace(): Throwable = this +} + +/** Internal control-flow signal: execution budget exceeded. */ +internal class BudgetExceededSignal(val reason: String) : RuntimeException(reason) { + override fun fillInStackTrace(): Throwable = this +} + +internal fun typeError(message: String): JsThrowSignal = + JsThrowSignal( + VObject( + cls = null, + fields = mutableMapOf( + "name" to VString("TypeError"), + "message" to VString(message), + ), + ) + ) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/Intrinsics.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/Intrinsics.kt new file mode 100644 index 0000000000..f7fd78afb9 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/Intrinsics.kt @@ -0,0 +1,466 @@ +package org.usvm.ts.pbt.interpreter + +import kotlin.math.abs +import kotlin.math.ceil +import kotlin.math.floor +import kotlin.math.round +import kotlin.math.sqrt + +/** + * Built-in functions/fields the concrete interpreter models. + * + * The registry covers exactly what the usvm-ts sample suite and its call + * approximations use (`Number.isNaN`, `Math.floor`, array methods, `console`/`Logger` + * no-ops, ...). A miss returns `null` and the caller reports [ExecutionResult.Unsupported] — + * we never silently return a wrong value. + */ +internal object Intrinsics { + + val NAMESPACES: Set = setOf("Math", "Number", "Boolean", "String", "console", "Logger", "JSON", "Object") + + /** Host callback for invoking a first-class function value (HOF callbacks). */ + fun interface FunctionInvoker { + fun invoke(fn: VFunction, args: List): VValue + } + + /** Call on a namespace object: `Math.floor(x)`, `Number.isNaN(x)`, `console.log(...)`. */ + fun callNamespace(namespace: String, method: String, args: List): VValue? = when (namespace) { + "console", "Logger" -> VUndefined // logging is a no-op + + "Math" -> { + val x = args.getOrElse(0) { VUndefined } + val n = JsSemantics.toNumber(x) + when (method) { + "floor" -> VNumber(floor(n)) + "ceil" -> VNumber(ceil(n)) + "round" -> VNumber(floor(n + 0.5)) // JS rounds .5 towards +Infinity + "trunc" -> VNumber(kotlin.math.truncate(n)) + "abs" -> VNumber(abs(n)) + "sqrt" -> VNumber(sqrt(n)) + "cbrt" -> VNumber(kotlin.math.cbrt(n)) + "sign" -> VNumber(if (n.isNaN()) Double.NaN else kotlin.math.sign(n)) + "log" -> VNumber(kotlin.math.ln(n)) + "log2" -> VNumber(kotlin.math.log2(n)) + "log10" -> VNumber(kotlin.math.log10(n)) + "log1p" -> VNumber(kotlin.math.ln1p(n)) + "exp" -> VNumber(kotlin.math.exp(n)) + "expm1" -> VNumber(kotlin.math.expm1(n)) + "sin" -> VNumber(kotlin.math.sin(n)) + "cos" -> VNumber(kotlin.math.cos(n)) + "tan" -> VNumber(kotlin.math.tan(n)) + "asin" -> VNumber(kotlin.math.asin(n)) + "acos" -> VNumber(kotlin.math.acos(n)) + "atan" -> VNumber(kotlin.math.atan(n)) + "sinh" -> VNumber(kotlin.math.sinh(n)) + "cosh" -> VNumber(kotlin.math.cosh(n)) + "tanh" -> VNumber(kotlin.math.tanh(n)) + "max" -> VNumber(args.map { JsSemantics.toNumber(it) }.maxOrNull() ?: Double.NEGATIVE_INFINITY) + "min" -> VNumber(args.map { JsSemantics.toNumber(it) }.minOrNull() ?: Double.POSITIVE_INFINITY) + "hypot" -> VNumber(sqrt(args.sumOf { val v = JsSemantics.toNumber(it); v * v })) + "atan2" -> VNumber( + kotlin.math.atan2(n, JsSemantics.toNumber(args.getOrElse(1) { VUndefined })) + ) + + "pow" -> VNumber( + Math.pow(n, JsSemantics.toNumber(args.getOrElse(1) { VUndefined })) + ) + + else -> null + } + } + + "Number" -> { + val x = args.getOrElse(0) { VUndefined } + when (method) { + "isNaN" -> VBool(x is VNumber && x.value.isNaN()) + "isFinite" -> VBool(x is VNumber && x.value.isFinite()) + "isInteger" -> VBool(x is VNumber && x.value.isFinite() && x.value == floor(x.value)) + "isSafeInteger" -> VBool( + x is VNumber && x.value.isFinite() && x.value == floor(x.value) && + abs(x.value) <= 9007199254740991.0 + ) + + "parseFloat" -> VNumber(JsSemantics.stringToNumber(JsSemantics.toStringJs(x))) + "parseInt" -> parseIntJs(args) + else -> null + } + } + + "Object" -> when (method) { + "keys" -> when (val o = args.getOrElse(0) { VUndefined }) { + is VObject -> VArray(o.fields.keys.map { VString(it) as VValue }.toMutableList()) + is VArray -> VArray(o.elements.indices.map { VString(it.toString()) as VValue }.toMutableList()) + else -> VArray() + } + + "values" -> when (val o = args.getOrElse(0) { VUndefined }) { + is VObject -> VArray(o.fields.values.toMutableList()) + is VArray -> VArray(o.elements.toMutableList()) + else -> VArray() + } + + else -> null + } + + else -> null + } + + private fun parseIntJs(args: List): VNumber { + val s = JsSemantics.toStringJs(args.getOrElse(0) { VUndefined }).trim() + val radix = args.getOrNull(1)?.let { JsSemantics.toInt32(it) }?.takeIf { it != 0 } ?: 10 + var i = 0 + var sign = 1 + if (i < s.length && (s[i] == '+' || s[i] == '-')) { + if (s[i] == '-') sign = -1 + i++ + } + var body = s.substring(i) + var r = radix + if ((r == 16 || args.getOrNull(1) == null) && (body.startsWith("0x") || body.startsWith("0X"))) { + body = body.substring(2) + r = 16 + } + val digits = body.takeWhile { Character.digit(it, r) >= 0 } + if (digits.isEmpty()) return VNumber(Double.NaN) + var acc = 0.0 + for (c in digits) acc = acc * r + Character.digit(c, r) + return VNumber(sign * acc) + } + + /** Constant field on a namespace object: `Number.MAX_VALUE`, `Math.PI`. */ + fun namespaceField(namespace: String, field: String): VValue? = when (namespace) { + "Number" -> when (field) { + "MAX_VALUE" -> VNumber(Double.MAX_VALUE) + "MIN_VALUE" -> VNumber(Double.MIN_VALUE) + "MAX_SAFE_INTEGER" -> VNumber(9007199254740991.0) + "MIN_SAFE_INTEGER" -> VNumber(-9007199254740991.0) + "NaN" -> VNumber(Double.NaN) + "POSITIVE_INFINITY" -> VNumber(Double.POSITIVE_INFINITY) + "NEGATIVE_INFINITY" -> VNumber(Double.NEGATIVE_INFINITY) + "EPSILON" -> VNumber(Math.ulp(1.0)) + else -> null + } + + "Math" -> when (field) { + "PI" -> VNumber(Math.PI) + "E" -> VNumber(Math.E) + else -> null + } + + else -> null + } + + /** Free-function-style conversions: `Number(x)`, `Boolean(x)`, `String(x)`. */ + fun callConversion(name: String, args: List): VValue? { + val x = args.getOrElse(0) { VUndefined } + return when (name) { + "Number" -> VNumber(if (args.isEmpty()) 0.0 else JsSemantics.toNumber(x)) + "Boolean" -> VBool(args.isNotEmpty() && JsSemantics.truthy(x)) + "String" -> VString(if (args.isEmpty()) "" else JsSemantics.toStringJs(x)) + "isNaN" -> VBool(JsSemantics.toNumber(x).isNaN()) + "parseFloat" -> VNumber(JsSemantics.stringToNumber(JsSemantics.toStringJs(x))) + else -> null + } + } + + /** Instance method on a concrete receiver value: `arr.push(x)`, `n.toString()`. */ + fun callInstance( + receiver: VValue, + method: String, + args: List, + invoker: FunctionInvoker, + ): VValue? { + // Universal methods + when (method) { + "toString" -> return VString(JsSemantics.toStringJs(receiver)) + "valueOf" -> return JsSemantics.toPrimitive(receiver) + } + return when (receiver) { + is VArray -> callArrayMethod(receiver, method, args) + ?: callArrayHof(receiver, method, args, invoker) + + is VString -> callStringMethod(receiver, method, args) + is VMap -> callMapMethod(receiver, method, args, invoker) + is VSet -> callSetMethod(receiver, method, args, invoker) + else -> null + } + } + + private fun callArrayHof( + arr: VArray, + method: String, + args: List, + invoker: FunctionInvoker, + ): VValue? { + val fn = args.getOrNull(0) as? VFunction + fun call(vararg a: VValue): VValue = invoker.invoke(fn!!, a.toList()) + + return when (method) { + "map" -> { + fn ?: return null + VArray(arr.elements.mapIndexed { i, e -> call(e, VNumber(i.toDouble()), arr) }.toMutableList()) + } + + "filter" -> { + fn ?: return null + VArray( + arr.elements.filterIndexed { i, e -> + JsSemantics.truthy(call(e, VNumber(i.toDouble()), arr)) + }.toMutableList() + ) + } + + "forEach" -> { + fn ?: return null + arr.elements.forEachIndexed { i, e -> call(e, VNumber(i.toDouble()), arr) } + VUndefined + } + + "some" -> { + fn ?: return null + VBool(arr.elements.withIndex().any { (i, e) -> JsSemantics.truthy(call(e, VNumber(i.toDouble()), arr)) }) + } + + "every" -> { + fn ?: return null + VBool(arr.elements.withIndex().all { (i, e) -> JsSemantics.truthy(call(e, VNumber(i.toDouble()), arr)) }) + } + + "find" -> { + fn ?: return null + arr.elements.withIndex() + .firstOrNull { (i, e) -> JsSemantics.truthy(call(e, VNumber(i.toDouble()), arr)) } + ?.value ?: VUndefined + } + + "findIndex" -> { + fn ?: return null + VNumber( + arr.elements.withIndex() + .indexOfFirst { (i, e) -> JsSemantics.truthy(call(e, VNumber(i.toDouble()), arr)) } + .toDouble() + ) + } + + "reduce" -> { + fn ?: return null + var acc: VValue + var start: Int + if (args.size >= 2) { + acc = args[1] + start = 0 + } else { + if (arr.elements.isEmpty()) { + throw JsThrowSignal(VString("TypeError: Reduce of empty array with no initial value")) + } + acc = arr.elements[0] + start = 1 + } + for (i in start until arr.elements.size) { + acc = call(acc, arr.elements[i], VNumber(i.toDouble()), arr) + } + acc + } + + "sort" -> { + val comparator: Comparator = if (fn != null) { + Comparator { a, b -> + val r = JsSemantics.toNumber(call(a, b)) + if (r.isNaN()) 0 else r.compareTo(0.0) + } + } else { + // Default JS sort: by ToString, undefined last + Comparator { a, b -> JsSemantics.toStringJs(a).compareTo(JsSemantics.toStringJs(b)) } + } + arr.elements.sortWith(comparator) + arr + } + + else -> null + } + } + + private fun callMapMethod( + map: VMap, + method: String, + args: List, + invoker: FunctionInvoker, + ): VValue? { + fun key(v: VValue): VValue = if (v is VNumber && v.value == 0.0) VNumber(0.0) else v // normalize -0 + val k = key(args.getOrElse(0) { VUndefined }) + return when (method) { + "get" -> map.entries[k] ?: VUndefined + "set" -> { + map.entries[k] = args.getOrElse(1) { VUndefined } + map + } + + "has" -> VBool(k in map.entries) + "delete" -> VBool(map.entries.remove(k) != null) + "clear" -> { + map.entries.clear() + VUndefined + } + + "keys" -> VArray(map.entries.keys.toMutableList()) + "values" -> VArray(map.entries.values.toMutableList()) + "forEach" -> { + val fn = args.getOrNull(0) as? VFunction ?: return null + for ((kk, v) in map.entries.entries.toList()) { + invoker.invoke(fn, listOf(v, kk, map)) + } + VUndefined + } + + else -> null + } + } + + private fun callSetMethod( + set: VSet, + method: String, + args: List, + invoker: FunctionInvoker, + ): VValue? { + fun key(v: VValue): VValue = if (v is VNumber && v.value == 0.0) VNumber(0.0) else v + val k = key(args.getOrElse(0) { VUndefined }) + return when (method) { + "add" -> { + set.elements.add(k) + set + } + + "has" -> VBool(k in set.elements) + "delete" -> VBool(set.elements.remove(k)) + "clear" -> { + set.elements.clear() + VUndefined + } + + "values", "keys" -> VArray(set.elements.toMutableList()) + "forEach" -> { + val fn = args.getOrNull(0) as? VFunction ?: return null + for (e in set.elements.toList()) { + invoker.invoke(fn, listOf(e, e, set)) + } + VUndefined + } + + else -> null + } + } + + private fun callArrayMethod(arr: VArray, method: String, args: List): VValue? = when (method) { + "push" -> { + arr.elements.addAll(args) + VNumber(arr.elements.size.toDouble()) + } + + "pop" -> if (arr.elements.isEmpty()) VUndefined else arr.elements.removeAt(arr.elements.size - 1) + + "shift" -> if (arr.elements.isEmpty()) VUndefined else arr.elements.removeAt(0) + + "unshift" -> { + arr.elements.addAll(0, args) + VNumber(arr.elements.size.toDouble()) + } + + "fill" -> { + val value = args.getOrElse(0) { VUndefined } + for (i in arr.elements.indices) arr.elements[i] = value + arr + } + + "join" -> { + val sep = args.getOrNull(0)?.let { JsSemantics.toStringJs(it) } ?: "," + VString(arr.elements.joinToString(sep) { el -> + if (el == VNull || el == VUndefined) "" else JsSemantics.toStringJs(el) + }) + } + + "slice" -> { + val size = arr.elements.size + fun clamp(raw: Double, default: Int): Int { + if (raw.isNaN()) return 0 + val i = raw.toInt() + return when { + args.isEmpty() -> default + i < 0 -> maxOf(size + i, 0) + else -> minOf(i, size) + } + } + + val start = args.getOrNull(0)?.let { clamp(JsSemantics.toNumber(it), 0) } ?: 0 + val end = args.getOrNull(1)?.let { clamp(JsSemantics.toNumber(it), size) } ?: size + VArray(if (start < end) arr.elements.subList(start, end).toMutableList() else mutableListOf()) + } + + "concat" -> { + val result = arr.elements.toMutableList() + for (a in args) { + if (a is VArray) result.addAll(a.elements) else result.add(a) + } + VArray(result) + } + + "indexOf" -> { + val target = args.getOrElse(0) { VUndefined } + VNumber(arr.elements.indexOfFirst { JsSemantics.strictEq(it, target) }.toDouble()) + } + + "includes" -> { + val target = args.getOrElse(0) { VUndefined } + // `includes` uses SameValueZero: NaN is found, unlike indexOf + VBool(arr.elements.any { el -> + JsSemantics.strictEq(el, target) || + (el is VNumber && target is VNumber && el.value.isNaN() && target.value.isNaN()) + }) + } + + "reverse" -> { + arr.elements.reverse() + arr + } + + else -> null + } + + private fun callStringMethod(s: VString, method: String, args: List): VValue? = when (method) { + "charAt" -> { + val i = JsSemantics.toNumber(args.getOrElse(0) { VNumber(0.0) }).toInt() + VString(if (i in s.value.indices) s.value[i].toString() else "") + } + + "indexOf" -> VNumber( + s.value.indexOf(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined })).toDouble() + ) + + "includes" -> VBool(s.value.contains(JsSemantics.toStringJs(args.getOrElse(0) { VUndefined }))) + + "toUpperCase" -> VString(s.value.uppercase()) + "toLowerCase" -> VString(s.value.lowercase()) + "trim" -> VString(s.value.trim()) + + "concat" -> VString(s.value + args.joinToString("") { JsSemantics.toStringJs(it) }) + + "slice", "substring" -> { + val len = s.value.length + fun idx(v: VValue?, default: Int): Int { + if (v == null) return default + val d = JsSemantics.toNumber(v) + if (d.isNaN()) return 0 + val i = d.toInt() + return if (method == "slice" && i < 0) maxOf(len + i, 0) else i.coerceIn(0, len) + } + + var start = idx(args.getOrNull(0), 0) + var end = idx(args.getOrNull(1), len) + if (method == "substring" && start > end) { + val t = start; start = end; end = t + } + VString(if (start < end) s.value.substring(start, end) else "") + } + + else -> null + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/JsSemantics.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/JsSemantics.kt new file mode 100644 index 0000000000..20e4bd5e0b --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/JsSemantics.kt @@ -0,0 +1,199 @@ +package org.usvm.ts.pbt.interpreter + +import kotlin.math.abs +import kotlin.math.floor +import kotlin.math.truncate + +/** + * Concrete JS (ECMAScript) semantics for the values of [VValue]. + * + * The symbolic counterparts (and the source of truth for what usvm-ts models) are + * `org.usvm.machine.operator.TsBinaryOperator`, `TsUnaryOperator` and `mkTruthyExpr`. + * Divergences between this implementation and the symbolic one are caught by the + * differential test suite and whitelisted explicitly. + */ +object JsSemantics { + + // ToBoolean + fun truthy(v: VValue): Boolean = when (v) { + is VBool -> v.value + is VNumber -> v.value != 0.0 && !v.value.isNaN() + is VString -> v.value.isNotEmpty() + VNull, VUndefined -> false + is VObject, is VArray, is VNamespace, is VFunction, is VMap, is VSet -> true + } + + // ToNumber + fun toNumber(v: VValue): Double = when (v) { + is VNumber -> v.value + is VBool -> if (v.value) 1.0 else 0.0 + is VString -> stringToNumber(v.value) + VNull -> 0.0 + VUndefined -> Double.NaN + is VObject, is VArray, is VNamespace, is VFunction, is VMap, is VSet -> toNumber(toPrimitive(v)) + } + + fun stringToNumber(s: String): Double { + val t = s.trim() + if (t.isEmpty()) return 0.0 + return when { + t == "Infinity" || t == "+Infinity" -> Double.POSITIVE_INFINITY + t == "-Infinity" -> Double.NEGATIVE_INFINITY + t.startsWith("0x") || t.startsWith("0X") -> + t.substring(2).toLongOrNull(16)?.toDouble() ?: Double.NaN + + t.startsWith("0o") || t.startsWith("0O") -> + t.substring(2).toLongOrNull(8)?.toDouble() ?: Double.NaN + + t.startsWith("0b") || t.startsWith("0B") -> + t.substring(2).toLongOrNull(2)?.toDouble() ?: Double.NaN + + else -> t.toDoubleOrNull() ?: Double.NaN + } + } + + // ToString + fun toStringJs(v: VValue): String = when (v) { + is VString -> v.value + is VNumber -> numberToString(v.value) + is VBool -> v.value.toString() + VNull -> "null" + VUndefined -> "undefined" + is VArray -> v.elements.joinToString(",") { el -> + if (el == VNull || el == VUndefined) "" else toStringJs(el) + } + + is VObject, is VNamespace, is VMap, is VSet -> "[object Object]" + + is VFunction -> "function ${v.method.name}() { [code] }" + } + + /** + * JS `Number::toString` approximation. Exact for integral values with |x| < 2^53 + * and the special values; for other doubles falls back to Kotlin's shortest + * representation, which matches JS in the common range but differs in exponent + * formatting corner cases (whitelisted in the differential suite). + */ + fun numberToString(d: Double): String = when { + d.isNaN() -> "NaN" + d == Double.POSITIVE_INFINITY -> "Infinity" + d == Double.NEGATIVE_INFINITY -> "-Infinity" + d == 0.0 -> "0" // covers -0.0 as well + d == floor(d) && abs(d) < 1e21 -> { + if (abs(d) <= 9.007199254740992E15) d.toLong().toString() + else java.math.BigDecimal(d).toBigInteger().toString() + } + + else -> d.toString() + } + + // ToPrimitive (hint: number/default). Plain objects have no user-defined valueOf in our model. + fun toPrimitive(v: VValue): VValue = when (v) { + is VArray -> VString(toStringJs(v)) + is VObject, is VNamespace, is VFunction, is VMap, is VSet -> VString(toStringJs(v)) + else -> v + } + + // ToInt32 / ToUint32 + fun toInt32(v: VValue): Int { + val d = toNumber(v) + if (d.isNaN() || d.isInfinite()) return 0 + return truncate(d).toLong().toInt() + } + + fun toUint32(v: VValue): Long { + return toInt32(v).toLong() and 0xFFFFFFFFL + } + + // Addition: string concatenation if either primitive is a string + fun add(a: VValue, b: VValue): VValue { + val pa = toPrimitive(a) + val pb = toPrimitive(b) + return if (pa is VString || pb is VString) { + VString(toStringJs(pa) + toStringJs(pb)) + } else { + VNumber(toNumber(pa) + toNumber(pb)) + } + } + + // Strict equality (===) + fun strictEq(a: VValue, b: VValue): Boolean = when { + a is VNumber && b is VNumber -> a.value == b.value // NaN != NaN, +0 == -0 + a is VString && b is VString -> a.value == b.value + a is VBool && b is VBool -> a.value == b.value + a == VNull && b == VNull -> true + a == VUndefined && b == VUndefined -> true + a is VObject && b is VObject -> a === b + a is VArray && b is VArray -> a === b + a is VNamespace && b is VNamespace -> a == b + a is VFunction && b is VFunction -> a === b + a is VMap && b is VMap -> a === b + a is VSet && b is VSet -> a === b + else -> false + } + + // Loose equality (==), ES2015 7.2.12 + fun looseEq(a: VValue, b: VValue): Boolean = when { + sameTypeCategory(a, b) -> strictEq(a, b) + (a == VNull && b == VUndefined) || (a == VUndefined && b == VNull) -> true + a is VNumber && b is VString -> a.value == stringToNumber(b.value) + a is VString && b is VNumber -> stringToNumber(a.value) == b.value + a is VBool -> looseEq(VNumber(toNumber(a)), b) + b is VBool -> looseEq(a, VNumber(toNumber(b))) + (a is VNumber || a is VString) && isObjectLike(b) -> looseEq(a, toPrimitive(b)) + isObjectLike(a) && (b is VNumber || b is VString) -> looseEq(toPrimitive(a), b) + else -> false + } + + private fun isObjectLike(v: VValue): Boolean = + v is VObject || v is VArray || v is VNamespace || v is VFunction || v is VMap || v is VSet + + private fun sameTypeCategory(a: VValue, b: VValue): Boolean = when (a) { + is VNumber -> b is VNumber + is VString -> b is VString + is VBool -> b is VBool + VNull -> b == VNull + VUndefined -> b == VUndefined + is VObject, is VArray, is VNamespace, is VFunction, is VMap, is VSet -> isObjectLike(b) + } + + // Relational (<, <=, >, >=): both string -> lexicographic, else numeric (NaN -> false) + private fun relational(a: VValue, b: VValue, cmp: (Int) -> Boolean, numCmp: (Double, Double) -> Boolean): Boolean { + val pa = toPrimitive(a) + val pb = toPrimitive(b) + return if (pa is VString && pb is VString) { + cmp(pa.value.compareTo(pb.value)) + } else { + val na = toNumber(pa) + val nb = toNumber(pb) + if (na.isNaN() || nb.isNaN()) false else numCmp(na, nb) + } + } + + fun lt(a: VValue, b: VValue): Boolean = relational(a, b, { it < 0 }, { x, y -> x < y }) + fun le(a: VValue, b: VValue): Boolean = relational(a, b, { it <= 0 }, { x, y -> x <= y }) + fun gt(a: VValue, b: VValue): Boolean = relational(a, b, { it > 0 }, { x, y -> x > y }) + fun ge(a: VValue, b: VValue): Boolean = relational(a, b, { it >= 0 }, { x, y -> x >= y }) + + // typeof + fun typeOf(v: VValue): String = when (v) { + is VNumber -> "number" + is VBool -> "boolean" + is VString -> "string" + VUndefined -> "undefined" + VNull -> "object" + is VFunction -> "function" + is VObject, is VArray, is VNamespace, is VMap, is VSet -> "object" + } + + // `in` operator + fun inOp(key: VValue, container: VValue): Boolean = when (container) { + is VObject -> toStringJs(key) in container.fields + is VArray -> { + val idx = toNumber(key) + idx == floor(idx) && idx >= 0 && idx < container.elements.size + } + + else -> false + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/VValue.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/VValue.kt new file mode 100644 index 0000000000..d67041e5cb --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/interpreter/VValue.kt @@ -0,0 +1,71 @@ +package org.usvm.ts.pbt.interpreter + +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsMethod + +/** + * A concrete runtime value of the EtsIR interpreter, mirroring the JS value universe + * supported by usvm-ts (`org.usvm.api.TsTestValue`). + * + * [VObject] and [VArray] intentionally use *identity* equality (JS reference semantics). + */ +sealed interface VValue + +data class VNumber(val value: Double) : VValue { + override fun toString(): String = "VNumber($value)" +} + +data class VBool(val value: Boolean) : VValue + +data class VString(val value: String) : VValue + +data object VNull : VValue + +data object VUndefined : VValue + +class VObject( + /** Declaring class, if the object is an instance of a scene class; `null` for plain records. */ + val cls: EtsClass?, + val fields: MutableMap = mutableMapOf(), +) : VValue { + override fun toString(): String = "VObject(${cls?.name ?: ""}, $fields)" +} + +class VArray( + val elements: MutableList = mutableListOf(), +) : VValue { + override fun toString(): String = "VArray($elements)" +} + +/** + * An intrinsic namespace object (`Math`, `console`, `Number`, `Logger`, ...). + * Appears as the receiver of intrinsic calls; behaves as a plain object otherwise. + */ +data class VNamespace(val name: String) : VValue + +/** + * A first-class function value: an arrow function / function expression lowered + * by the front end into an anonymous method. Passed around as callbacks + * (`arr.map(f)`) and invoked via `ptr_call`. + */ +class VFunction( + val method: EtsMethod, + /** Captured `this`, when the function was obtained from an instance context. */ + val thisValue: VValue = VUndefined, +) : VValue { + override fun toString(): String = "VFunction(${method.name})" +} + +/** A JS `Map` with SameValueZero keys (primitives by value, heap entities by identity). */ +class VMap( + val entries: LinkedHashMap = LinkedHashMap(), +) : VValue { + override fun toString(): String = "VMap($entries)" +} + +/** A JS `Set` with SameValueZero elements. */ +class VSet( + val elements: LinkedHashSet = LinkedHashSet(), +) : VValue { + override fun toString(): String = "VSet($elements)" +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Conversions.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Conversions.kt new file mode 100644 index 0000000000..e255c47446 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Conversions.kt @@ -0,0 +1,87 @@ +package org.usvm.ts.pbt.report + +import org.jacodb.ets.model.EtsClass +import org.usvm.api.TsTestValue +import org.usvm.ts.pbt.interpreter.VArray +import org.usvm.ts.pbt.interpreter.VBool +import org.usvm.ts.pbt.interpreter.VFunction +import org.usvm.ts.pbt.interpreter.VMap +import org.usvm.ts.pbt.interpreter.VNamespace +import org.usvm.ts.pbt.interpreter.VNull +import org.usvm.ts.pbt.interpreter.VSet +import org.usvm.ts.pbt.interpreter.VNumber +import org.usvm.ts.pbt.interpreter.VObject +import org.usvm.ts.pbt.interpreter.VString +import org.usvm.ts.pbt.interpreter.VUndefined +import org.usvm.ts.pbt.interpreter.VValue + +/** + * Placeholder emitted by `org.usvm.util.TsTestResolver` for symbolic strings it + * cannot concretize. Values carrying it cannot be replayed faithfully. + */ +const val SYMBOLIC_STRING_PLACEHOLDER: String = "String construction is not yet implemented" + +/** + * Convert a symbolic-phase test value ([TsTestValue], extracted from a usvm-ts model) + * into a concrete interpreter value. + * + * @return `null` if the value cannot be represented faithfully (then the replay + * must be skipped and coverage recovered from the symbolic trace instead). + */ +fun TsTestValue.toVValueOrNull(classResolver: (String) -> EtsClass? = { null }): VValue? { + return when (this) { + is TsTestValue.TsNumber -> VNumber(number) + is TsTestValue.TsBoolean -> VBool(value) + is TsTestValue.TsString -> + if (value == SYMBOLIC_STRING_PLACEHOLDER) null else VString(value) + + TsTestValue.TsNull -> VNull + TsTestValue.TsUndefined -> VUndefined + + is TsTestValue.TsArray<*> -> { + val elements = values.map { it.toVValueOrNull(classResolver) ?: return null } + VArray(elements.toMutableList()) + } + + is TsTestValue.TsClass -> { + val fields = mutableMapOf() + for ((k, v) in properties) { + fields[k] = v.toVValueOrNull(classResolver) ?: return null + } + VObject(classResolver(name), fields) + } + + // Unknowns, BigInt, exceptions: not replayable + else -> null + } +} + +/** Convert a concrete interpreter value into the reporting format shared with usvm-ts. */ +fun VValue.toTsTestValue(): TsTestValue = when (this) { + is VNumber -> TsTestValue.TsNumber.TsDouble(value) + is VBool -> TsTestValue.TsBoolean(value) + is VString -> TsTestValue.TsString(value) + VNull -> TsTestValue.TsNull + VUndefined -> TsTestValue.TsUndefined + is VArray -> TsTestValue.TsArray(elements.map { it.toTsTestValue() }) + is VObject -> TsTestValue.TsClass( + name = cls?.name ?: "Object", + properties = fields.mapValues { (_, v) -> v.toTsTestValue() }, + ) + + is VNamespace -> TsTestValue.TsClass(name = name, properties = emptyMap()) + + is VFunction -> TsTestValue.TsClass(name = "Function", properties = emptyMap()) + + is VMap -> TsTestValue.TsClass( + name = "Map", + properties = entries.entries.withIndex().associate { (i, e) -> + "entry$i" to TsTestValue.TsArray(listOf(e.key.toTsTestValue(), e.value.toTsTestValue())) + }, + ) + + is VSet -> TsTestValue.TsClass( + name = "Set", + properties = elements.withIndex().associate { (i, e) -> "element$i" to e.toTsTestValue() }, + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/HybridReport.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/HybridReport.kt new file mode 100644 index 0000000000..a855b4b87c --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/HybridReport.kt @@ -0,0 +1,93 @@ +package org.usvm.ts.pbt.report + +import kotlinx.serialization.Serializable +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.Json + +/** + * Machine-readable report of one hybrid analysis run — the raw material for + * the experimental section (coverage timelines, per-target attribution, + * hint ablation data, honesty counters). + */ +@Serializable +data class HybridReport( + val config: ConfigEcho, + val methods: List, +) { + companion object { + private val json = Json { prettyPrint = true } + fun encode(report: HybridReport): String = json.encodeToString(report) + fun decode(text: String): HybridReport = json.decodeFromString(text) + } +} + +@Serializable +data class ConfigEcho( + val mode: String, + val seed: Long, + val pbtMaxIterations: Int, + val pbtTimeBudgetMs: Long, + val perTargetTimeoutMs: Long, + val hintFallback: Boolean, +) + +@Serializable +data class MethodReport( + val method: String, + val totalStmts: Int, + val totalBranches: Int, + val coveredStmts: Int, + val coveredBranches: Int, + val stmtCoverage: Double, + val branchCoverage: Double, + val timeline: List, + val pbt: PbtReport?, + val symbolic: SymbolicReport?, + val typeProfile: Map>, + val totalWallMs: Long, +) + +@Serializable +data class TimelinePoint( + val elapsedMs: Long, + val phase: String, + val coveredStmts: Int, + val coveredBranches: Int, +) + +@Serializable +data class PbtReport( + val executions: Int, + val returned: Int, + val threw: Int, + val diverged: Int, + val unsupported: Int, + val wallMs: Long, + val failures: List, +) + +@Serializable +data class FailureReport( + val description: String, + val args: List, + val shrunkArgs: List, +) + +@Serializable +data class SymbolicReport( + val targets: List, + val reached: Int, + val wallMs: Long, +) + +@Serializable +data class TargetReport( + val branch: String, + val reached: Boolean, + val wallMs: Long, + val steps: Long, + val hintsUsed: Boolean, + val fallbackUsed: Boolean, + val replayConfirmed: Boolean, + val inputs: List?, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Main.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Main.kt new file mode 100644 index 0000000000..f18cfe2c8e --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/report/Main.kt @@ -0,0 +1,217 @@ +package org.usvm.ts.pbt.report + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.ts.pbt.hybrid.AnalysisMode +import org.usvm.ts.pbt.hybrid.HybridAnalyzer +import org.usvm.ts.pbt.hybrid.HybridConfig +import java.nio.file.Path +import kotlin.io.path.ExperimentalPathApi +import kotlin.io.path.Path +import kotlin.io.path.extension +import kotlin.io.path.isDirectory +import kotlin.io.path.pathString +import kotlin.io.path.walk +import kotlin.io.path.writeText +import kotlin.system.exitProcess +import kotlin.time.Duration.Companion.seconds + +private val logger = KotlinLogging.logger {} + +private const val USAGE = """ +Usage: hybrid-analyzer [options] + +Corpus selection: + --recursive walk subdirectories for .ts files + --exclude skip files whose path contains the substring (repeatable); + defaults always applied: .d.ts, node_modules, .test.ts, .spec.ts + --max-files cap the number of analyzed files + --class only methods of this class + --method only methods with this name + +Analysis: + --modes comma-separated analysis modes to run over the same corpus + (PBT_ONLY | SYMBOLIC_ONLY | HYBRID | HYBRID_WITH_HINTS); + default: HYBRID_WITH_HINTS + --seed PBT random seed (default: 0) + --pbt-iterations PBT iteration budget per method (default: 2000) + --target-timeout per-target symbolic timeout (default: 20) + --no-fallback disable the hint-free fallback run + +Output: + --out report path prefix; per mode: -.json + (default: hybrid-report) + +EtsIR provider is selected by the jacodb loader (ETS_IR_PROVIDER=ts-frontend|arkanalyzer +with ETS_FRONTEND_DIR / ARKANALYZER_DIR respectively). +""" + +private class Options(args: Array) { + val input: Path = Path(args[0]) + var recursive = false + val excludes = mutableListOf(".d.ts", "node_modules", ".test.ts", ".spec.ts") + var maxFiles = Int.MAX_VALUE + var classFilter: String? = null + var methodFilter: String? = null + var modes: List = listOf(AnalysisMode.HYBRID_WITH_HINTS) + var seed = 0L + var pbtIterations = 2_000 + var targetTimeoutSec = 20 + var hintFallback = true + var outPrefix = "hybrid-report" + + init { + var i = 1 + while (i < args.size) { + when (args[i]) { + "--recursive" -> recursive = true + "--exclude" -> excludes += args[++i] + "--max-files" -> maxFiles = args[++i].toInt() + "--class" -> classFilter = args[++i] + "--method" -> methodFilter = args[++i] + "--modes" -> modes = args[++i].split(',').map { AnalysisMode.valueOf(it.trim()) } + "--mode" -> modes = listOf(AnalysisMode.valueOf(args[++i])) // backward compat + "--seed" -> seed = args[++i].toLong() + "--pbt-iterations" -> pbtIterations = args[++i].toInt() + "--target-timeout" -> targetTimeoutSec = args[++i].toInt() + "--no-fallback" -> hintFallback = false + "--out" -> outPrefix = args[++i].removeSuffix(".json") + else -> { + println("Unknown option: ${args[i]}\n$USAGE") + exitProcess(1) + } + } + i++ + } + } +} + +@OptIn(ExperimentalPathApi::class) +private fun collectFiles(opts: Options): List { + val files = when { + !opts.input.isDirectory() -> listOf(opts.input) + opts.recursive -> opts.input.walk().filter { it.extension == "ts" }.toList() + else -> opts.input.toFile().listFiles().orEmpty().map { it.toPath() }.filter { it.extension == "ts" } + } + return files + .filter { path -> opts.excludes.none { path.pathString.contains(it) } } + .sorted() + .take(opts.maxFiles) +} + +/** + * Synthetic methods that must not be analyzed as entry points. Anonymous + * arrow-function methods (`%AM0$...`) are *kept*: `export const f = (...) => ...` + * is the dominant style in real TS corpora. + */ +private val SYNTHETIC_METHOD_NAMES = setOf("%dflt", "%instInit", "%statInit", "constructor") + +private fun selectMethods(scene: EtsScene, opts: Options): List = + scene.projectClasses + .asSequence() + .filter { opts.classFilter == null || it.name == opts.classFilter } + .flatMap { it.methods } + .filter { it.cfg.stmts.isNotEmpty() } + .filter { it.name !in SYNTHETIC_METHOD_NAMES } + .filter { opts.methodFilter == null || it.name == opts.methodFilter } + .toList() + +fun main(args: Array) { + if (args.isEmpty()) { + println(USAGE) + exitProcess(1) + } + val opts = Options(args) + + val files = collectFiles(opts) + println("Corpus: ${files.size} file(s)") + + // Load every file into its own scene, isolating frontend failures per file. + val scenes = mutableListOf>() + var loadFailures = 0 + for (file in files) { + try { + scenes += file to EtsScene(listOf(loadEtsFileAutoConvert(file))) + } catch (e: Throwable) { + loadFailures++ + logger.warn { "failed to load $file: ${e.message?.take(200)}" } + } + } + println("Loaded ${scenes.size} file(s), $loadFailures load failure(s)") + + for (mode in opts.modes) { + val config = HybridConfig( + mode = mode, + seed = opts.seed, + pbtMaxIterations = opts.pbtIterations, + perTargetTimeout = opts.targetTimeoutSec.seconds, + hintFallback = opts.hintFallback, + ) + + val methodReports = mutableListOf() + var analysisFailures = 0 + + for ((file, scene) in scenes) { + val methods = selectMethods(scene, opts) + for (method in methods) { + try { + methodReports += HybridAnalyzer(scene, config).analyzeMethod(method) + } catch (e: Throwable) { + analysisFailures++ + logger.warn { "analysis failed for ${method.signature} in $file: ${e.message?.take(200)}" } + } + } + } + + val report = HybridReport( + config = ConfigEcho( + mode = mode.name, + seed = opts.seed, + pbtMaxIterations = opts.pbtIterations, + pbtTimeBudgetMs = config.pbtTimeBudget.inWholeMilliseconds, + perTargetTimeoutMs = config.perTargetTimeout.inWholeMilliseconds, + hintFallback = opts.hintFallback, + ), + methods = methodReports, + ) + + val outPath = Path("${opts.outPrefix}-${mode.name}.json") + outPath.writeText(HybridReport.encode(report)) + + printSummary(mode.name, report, analysisFailures) + println("Report written to $outPath\n") + } +} + +private fun printSummary(mode: String, report: HybridReport, analysisFailures: Int) { + val ms = report.methods + if (ms.isEmpty()) { + println("[$mode] no methods analyzed ($analysisFailures analysis failures)") + return + } + val totalBranches = ms.sumOf { it.totalBranches } + val coveredBranches = ms.sumOf { it.coveredBranches } + val totalStmts = ms.sumOf { it.totalStmts } + val coveredStmts = ms.sumOf { it.coveredStmts } + val failures = ms.sumOf { it.pbt?.failures?.size ?: 0 } + val unsupported = ms.sumOf { it.pbt?.unsupported ?: 0 } + val targets = ms.flatMap { it.symbolic?.targets.orEmpty() } + val wallMs = ms.sumOf { it.totalWallMs } + + println("[$mode] methods=${ms.size} (analysis failures: $analysisFailures)") + println( + " branch coverage: $coveredBranches/$totalBranches (%.1f%%), stmt: $coveredStmts/$totalStmts (%.1f%%)" + .format( + if (totalBranches > 0) 100.0 * coveredBranches / totalBranches else 100.0, + if (totalStmts > 0) 100.0 * coveredStmts / totalStmts else 100.0, + ) + ) + println( + " pbt failures: $failures, unsupported executions: $unsupported; " + + "symbolic targets: ${targets.size}, reached: ${targets.count { it.reached }}, " + + "replay-confirmed: ${targets.count { it.replayConfirmed }}, " + + "fallbacks: ${targets.count { it.fallbackUsed }}; wall: ${wallMs / 1000.0}s" + ) +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzerTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzerTest.kt new file mode 100644 index 0000000000..8b288b06fa --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridAnalyzerTest.kt @@ -0,0 +1,73 @@ +package org.usvm.ts.pbt.hybrid + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertNotNull +import org.junit.jupiter.api.Assertions.assertNull +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.condition.EnabledIfEnvironmentVariable +import org.usvm.ts.pbt.report.HybridReport +import org.usvm.ts.pbt.util.getResourcePath +import kotlin.time.Duration.Companion.seconds + +@EnabledIfEnvironmentVariable(named = "ARKANALYZER_DIR", matches = ".+") +class HybridAnalyzerTest { + + private val scene: EtsScene by lazy { + EtsScene(listOf(loadEtsFileAutoConvert(getResourcePath("/pbt/HybridSamples.ts")))) + } + + private fun method(name: String): EtsMethod = + scene.projectAndSdkClasses.single { it.name == "HybridSamples" } + .methods.single { it.name == name } + + private fun config(mode: AnalysisMode) = HybridConfig( + mode = mode, + seed = 42L, + pbtMaxIterations = 1_000, + perTargetTimeout = 20.seconds, + ) + + @Test + fun `all four modes produce consistent reports on magic`() { + val m = method("magic") + + val pbtOnly = HybridAnalyzer(scene, config(AnalysisMode.PBT_ONLY)).analyzeMethod(m) + assertNotNull(pbtOnly.pbt) + assertNull(pbtOnly.symbolic) + assertEquals(0.75, pbtOnly.branchCoverage, 1e-9) + + val symbolicOnly = HybridAnalyzer(scene, config(AnalysisMode.SYMBOLIC_ONLY)).analyzeMethod(m) + assertNull(symbolicOnly.pbt) + assertNotNull(symbolicOnly.symbolic) + assertEquals(1.0, symbolicOnly.branchCoverage, 1e-9) + + val hybrid = HybridAnalyzer(scene, config(AnalysisMode.HYBRID)).analyzeMethod(m) + assertEquals(1.0, hybrid.branchCoverage, 1e-9) + // PBT covered 3 of 4 edges, so only one symbolic target remains + assertEquals(1, hybrid.symbolic!!.targets.size) + assertTrue(hybrid.symbolic!!.targets.single().reached) + assertTrue(hybrid.symbolic!!.targets.none { it.hintsUsed }) + + val hybridHints = HybridAnalyzer(scene, config(AnalysisMode.HYBRID_WITH_HINTS)).analyzeMethod(m) + assertEquals(1.0, hybridHints.branchCoverage, 1e-9) + assertTrue(hybridHints.typeProfile.isNotEmpty()) { "type profile must be reported" } + } + + @Test + fun `report json round-trip`() { + val report = HybridAnalyzer(scene, config(AnalysisMode.HYBRID_WITH_HINTS)) + .analyze(listOf(method("magic"), method("crashy"))) + + val text = HybridReport.encode(report) + val decoded = HybridReport.decode(text) + assertEquals(report, decoded) + + val crashy = decoded.methods.single { "crashy" in it.method } + assertTrue(crashy.pbt!!.failures.isNotEmpty()) { "crashy failures must be serialized" } + assertTrue(decoded.methods.all { it.timeline.isNotEmpty() }) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridE2eTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridE2eTest.kt new file mode 100644 index 0000000000..6a16c7a04f --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/HybridE2eTest.kt @@ -0,0 +1,110 @@ +package org.usvm.ts.pbt.hybrid + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.condition.EnabledIfEnvironmentVariable +import org.usvm.machine.TsHintType +import org.usvm.machine.TsInputTypeHints +import org.usvm.ts.pbt.coverage.CoverageTracker +import org.usvm.ts.pbt.util.getResourcePath + +@EnabledIfEnvironmentVariable(named = "ARKANALYZER_DIR", matches = ".+") +class HybridE2eTest { + + private val scene: EtsScene by lazy { + EtsScene(listOf(loadEtsFileAutoConvert(getResourcePath("/pbt/HybridSamples.ts")))) + } + + private fun method(name: String): EtsMethod = + scene.projectAndSdkClasses.single { it.name == "HybridSamples" } + .methods.single { it.name == name } + + @Test + fun `hybrid pipeline reaches the magic branch and confirms it by replay`() { + val m = method("magic") + val coverage = CoverageTracker(listOf(m)) + + // Phase 1: PBT + val pbt = PbtPhase(scene, m, coverage, seed = 42L, maxIterations = 2_000).run() + assertEquals(0.75, coverage.branchCoverage(), 1e-9) { "PBT must leave only the magic branch" } + + // Phase 2: targeted symbolic execution on the leftovers + val symbolic = SymbolicPhase( + scene, m, coverage, + hints = pbt.typeProfiler.toHints(), + ).run() + + assertEquals(1, symbolic.outcomes.size) + val outcome = symbolic.outcomes.single() + assertTrue(outcome.reached) { "symbolic phase must reach the magic branch" } + assertTrue(outcome.replayConfirmed) { "the synthesized input must replay concretely" } + assertEquals(1.0, coverage.branchCoverage(), 1e-9) { "hybrid coverage must be complete" } + + // The synthesized input is the actual solution of x * 2 === 98764 + val inputs = outcome.inputs!! + val x = inputs.parameters.first() + assertEquals( + 49382.0, + (x as org.usvm.api.TsTestValue.TsNumber).number, + 1e-9, + ) + } + + @Test + fun `type hints reduce symbolic effort on untyped parameters`() { + val m = method("manyUntyped") + + data class Run(val steps: ULong, val reached: Int, val wallMs: Long) + + fun runSymbolicOnly(hints: TsInputTypeHints): Run { + val coverage = CoverageTracker(listOf(m)) + // No PBT: target every branch from scratch, measure total steps + val result = SymbolicPhase( + scene, m, coverage, + hints = hints, + hintFallback = false, + ).run() + return Run( + steps = result.outcomes.sumOf { it.steps }, + reached = result.outcomes.count { it.reached }, + wallMs = result.outcomes.sumOf { it.wallMs }, + ) + } + + val numberHints = TsInputTypeHints( + mapOf( + TsInputTypeHints.keyOf(m) to mapOf( + 0 to setOf(TsHintType.NUMBER), + 1 to setOf(TsHintType.NUMBER), + 2 to setOf(TsHintType.NUMBER), + ), + ), + ) + + val withHints = runSymbolicOnly(numberHints) + val withoutHints = runSymbolicOnly(TsInputTypeHints.EMPTY) + + // NOTE: machine *steps* are typically equal in both modes on micro-fixtures: + // with `useSolverForForks` infeasible discriminator forks are pruned eagerly, + // so hints shift the cost into solver calls, visible as wall time on + // larger corpora (measured by the CLI experiments, not asserted here). + println( + "[ablation] with hints: steps=${withHints.steps}, reached=${withHints.reached}, " + + "wallMs=${withHints.wallMs}; without: steps=${withoutHints.steps}, " + + "reached=${withoutHints.reached}, wallMs=${withoutHints.wallMs}" + ) + + // All branches are number-reachable, so hints must not lose any of them + assertTrue(withHints.reached >= withoutHints.reached) { + "hinted run must reach at least as many branches" + } + assertTrue(withHints.reached > 0) { "hinted run must reach some branches" } + assertTrue(withHints.steps <= withoutHints.steps) { + "hints must not increase the search effort: ${withHints.steps} > ${withoutHints.steps}" + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/PbtPhaseTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/PbtPhaseTest.kt new file mode 100644 index 0000000000..40a0003e0e --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/hybrid/PbtPhaseTest.kt @@ -0,0 +1,85 @@ +package org.usvm.ts.pbt.hybrid + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.condition.EnabledIfEnvironmentVariable +import org.usvm.machine.TsHintType +import org.usvm.machine.TsInputTypeHints +import org.usvm.ts.pbt.coverage.CoverageTracker +import org.usvm.ts.pbt.interpreter.VArray +import org.usvm.ts.pbt.interpreter.VNumber +import org.usvm.ts.pbt.util.getResourcePath + +@EnabledIfEnvironmentVariable(named = "ARKANALYZER_DIR", matches = ".+") +class PbtPhaseTest { + + private val scene: EtsScene by lazy { + EtsScene(listOf(loadEtsFileAutoConvert(getResourcePath("/pbt/HybridSamples.ts")))) + } + + private fun method(name: String): EtsMethod = + scene.projectAndSdkClasses.single { it.name == "HybridSamples" } + .methods.single { it.name == name } + + @Test + fun `magic branch is not covered by pbt but the rest is`() { + val m = method("magic") + val coverage = CoverageTracker(listOf(m)) + val result = PbtPhase(scene, m, coverage, seed = 42L, maxIterations = 2_000).run() + + assertTrue(result.stats.executions > 0) + assertTrue(coverage.branchCoverage() < 1.0) { "magic branch should stay uncovered" } + + val uncovered = coverage.uncoveredBranches() + // Exactly the true-successor of `if (x * 2 === 98764)` should remain + assertEquals(1, uncovered.size) { + "expected exactly the magic branch to be uncovered, got: $uncovered" + } + // Everything else is covered: 3 of 4 branch edges + assertEquals(0.75, coverage.branchCoverage(), 1e-9) + } + + @Test + fun `crash is found and shrunk`() { + val m = method("crashy") + val coverage = CoverageTracker(listOf(m)) + val result = PbtPhase(scene, m, coverage, seed = 7L, maxIterations = 2_000).run() + + assertTrue(result.failures.isNotEmpty()) { "the out-of-bounds crash should be found" } + val failure = result.failures.first() + // Shrunk arguments: empty array and index 0 form the minimal failing input + val arr = failure.shrunkArgs[0] + val idx = failure.shrunkArgs[1] + assertTrue(arr is VArray && arr.elements.isEmpty()) { "shrunk array should be empty: $arr" } + assertTrue(idx is VNumber && (idx.value == 0.0 || idx.value.isNaN())) { + "shrunk index should be minimal: $idx" + } + } + + @Test + fun `type profile records observed parameter types`() { + val m = method("anyParam") + val coverage = CoverageTracker(listOf(m)) + val result = PbtPhase(scene, m, coverage, seed = 1L, maxIterations = 500).run() + + val hints: TsInputTypeHints = result.typeProfiler.toHints() + val observed = hints.forParameter(m, 0) + assertTrue(!observed.isNullOrEmpty()) { "type profile for parameter 0 must not be empty" } + assertTrue(TsHintType.NUMBER in observed!!) { "numbers must be observed among $observed" } + } + + @Test + fun `pbt runs are reproducible by seed`() { + val m = method("magic") + fun coveredWithSeed(seed: Long): Pair { + val coverage = CoverageTracker(listOf(m)) + PbtPhase(scene, m, coverage, seed = seed, maxIterations = 100).run() + return coverage.coveredStmtCount to coverage.coveredBranchCount + } + assertEquals(coveredWithSeed(123L), coveredWithSeed(123L)) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteInterpreterDslTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteInterpreterDslTest.kt new file mode 100644 index 0000000000..4274bbbb12 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteInterpreterDslTest.kt @@ -0,0 +1,153 @@ +package org.usvm.ts.pbt.interpreter + +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 + +class ConcreteInterpreterDslTest { + + private fun buildMethod( + name: String, + paramCount: Int, + block: ProgramBuilder.() -> Unit, + ): EtsMethod { + val prog = program(block) + val method = EtsMethodImpl( + signature = EtsMethodSignature( + enclosingClass = EtsClassSignature( + name = "Test", + file = EtsFileSignature(projectName = "TestP", fileName = "Test.ts"), + ), + name = name, + parameters = (0 until paramCount).map { EtsMethodParameter(it, "p$it", EtsUnknownType) }, + returnType = EtsUnknownType, + ), + ) + method.body.cfg = prog.toBlockCfg().toEtsBlockCfg(method) + return method + } + + private val emptyScene = EtsScene(emptyList()) + private val interpreter = EtsConcreteInterpreter(emptyScene) + + private fun run(method: EtsMethod, vararg args: VValue): ExecutionResult = + interpreter.execute(method, VUndefined, args.toList()) + + @Test + fun `abs function branches correctly`() { + val abs = buildMethod("abs", 1) { + val x = local("x") + assign(x, param(0)) + ifStmt(lt(x, const(0.0))) { + ret(neg(x)) + } + ret(x) + } + assertEquals(ExecutionResult.Returned(VNumber(5.0)), run(abs, VNumber(-5.0))) + assertEquals(ExecutionResult.Returned(VNumber(7.0)), run(abs, VNumber(7.0))) + // abs(undefined): undefined < 0 is false -> returns undefined unchanged + assertEquals(ExecutionResult.Returned(VUndefined), run(abs, VUndefined)) + } + + @Test + fun `loop computes sum and terminates`() { + // sum = 0; i = 0; while (i < n) { sum += i; i += 1 }; return sum + val sum = buildMethod("sum", 1) { + val n = local("n") + val i = local("i") + val s = local("s") + assign(n, param(0)) + assign(i, const(0.0)) + assign(s, const(0.0)) + label("head") + ifStmt(lt(i, n)) { + assign(s, add(s, i)) + assign(i, add(i, const(1.0))) + goto("head") + } + ret(s) + } + assertEquals(ExecutionResult.Returned(VNumber(45.0)), run(sum, VNumber(10.0))) + assertEquals(ExecutionResult.Returned(VNumber(0.0)), run(sum, VNumber(0.0))) + } + + @Test + fun `infinite loop diverges by step budget`() { + val loop = buildMethod("loop", 0) { + label("head") + ifStmt(eqq(const(1.0), const(1.0))) { + goto("head") + } + ret(const(0.0)) + } + val result = EtsConcreteInterpreter(emptyScene, ExecutionLimits(maxSteps = 1000)).execute(loop) + assertTrue(result is ExecutionResult.Diverged) + } + + @Test + fun `js coercion in arithmetic`() { + // return p0 * 2 - p1 + val f = buildMethod("f", 2) { + val r = local("r") + assign(r, sub(mul(param(0), const(2.0)), param(1))) + ret(r) + } + // "3" * 2 - true = 6 - 1 = 5 + assertEquals(ExecutionResult.Returned(VNumber(5.0)), run(f, VString("3"), VBool(true))) + // undefined -> NaN + val r = run(f, VUndefined, VNumber(0.0)) + assertTrue(((r as ExecutionResult.Returned).value as VNumber).value.isNaN()) + } + + @Test + fun `branch listener records edges`() { + val f = buildMethod("g", 1) { + val x = local("x") + assign(x, param(0)) + ifStmt(and(gt(x, const(0.0)), lt(x, const(10.0)))) { + ret(const(1.0)) + } + ret(const(0.0)) + } + val edges = mutableListOf>() + val conditions = mutableListOf() + val listener = object : ExecutionListener { + override fun onBranch(ifStmt: EtsIfStmt, taken: EtsStmt, condition: Boolean) { + edges += ifStmt to taken + conditions += condition + } + } + interpreter.execute(f, VUndefined, listOf(VNumber(5.0)), listener) + assertTrue(conditions.isNotEmpty()) + assertTrue(conditions.last()) // 0 < 5 < 10 -> true branch taken + + conditions.clear() + interpreter.execute(f, VUndefined, listOf(VNumber(-1.0)), listener) + assertTrue(conditions.contains(false)) + } +} 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 new file mode 100644 index 0000000000..8e71db8bdc --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt @@ -0,0 +1,198 @@ +package org.usvm.ts.pbt.interpreter + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.condition.EnabledIfEnvironmentVariable +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.CsvSource +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.ts.pbt.report.SYMBOLIC_STRING_PLACEHOLDER +import org.usvm.ts.pbt.report.toVValueOrNull +import org.usvm.ts.pbt.util.getResourcePath +import org.usvm.util.TsTestResolver +import kotlin.time.Duration.Companion.seconds + +/** + * Differential oracle: for every input model the *symbolic* engine produces, + * the *concrete* interpreter must compute the same result. + * + * Skipped (not failed) cases: non-replayable inputs (symbolic string placeholders), + * `Unsupported`/`Diverged` concrete outcomes. The test requires zero mismatches + * and at least one successfully compared execution per method suite. + */ +@EnabledIfEnvironmentVariable(named = "ARKANALYZER_DIR", matches = ".+") +class ConcreteVsSymbolicDifferentialTest { + + private fun loadScene(resourcePath: String): EtsScene { + val file = loadEtsFileAutoConvert(getResourcePath(resourcePath)) + return EtsScene(listOf(file)) + } + + private fun symbolicTests(scene: EtsScene, method: EtsMethod): List { + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + exceptionsPropagation = true, + timeout = 60.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = kotlin.time.Duration.INFINITE, + typeOperationsTimeout = kotlin.time.Duration.INFINITE, + ) + return TsMachine(scene, options, TsOptions()).use { machine -> + val states = machine.analyze(listOf(method)) + states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + data class Verdict(val compared: Int, val skipped: Int, val mismatches: List) + + /** + * Known divergences between the symbolic engine and precise JS semantics, + * confirmed by manual analysis. Keyed by "ClassName.methodName". + * + * These are *engine* issues, i.e. differential-testing findings: + * - `Add.addUnknownValues`: for reference operands usvm-ts approximates `+` + * numerically (e.g. `null + {}` becomes fp NaN), while JS applies ToPrimitive + * and string concatenation (`null + {} === "null[object Object]"`), so the + * engine follows the `res != res` (NaN) branch that is concretely unreachable. + * - `Less.lessUnknown`: for mixed-type fake-object operands the engine resolves + * 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 + * every branch after the jacodb lift (observed with `lipen/usvm`). + */ + private val knownEngineDivergences: Set = setOf( + "Add.addUnknownValues", + "Less.lessUnknown", + "And.andOfUnknown", + "TypeCoercion.transitiveCoercionNoTypes", + ) + + private fun runDifferential(resourcePath: String, className: String): Verdict { + val scene = loadScene(resourcePath) + val cls = scene.projectAndSdkClasses.single { it.name == className } + val methods = cls.methods.filter { + !it.name.startsWith("%") && it.name != "constructor" && it.cfg.stmts.isNotEmpty() + } + val interpreter = EtsConcreteInterpreter(scene) + val classResolver = { name: String -> scene.projectAndSdkClasses.firstOrNull { it.name == name } } + + var compared = 0 + var skipped = 0 + val mismatches = mutableListOf() + + for (method in methods) { + if ("$className.${method.name}" in knownEngineDivergences) { + skipped++ + continue + } + val tests = try { + symbolicTests(scene, method) + } catch (e: Throwable) { + // e.g. NotImplementedError for BigInt-typed parameters + skipped++ + continue + } + for (test in tests) { + val ctx = "${method.name}(${test.before.parameters})" + + val thisValue = test.before.thisInstance?.toVValueOrNull(classResolver) ?: VUndefined + val args = test.before.parameters.map { + it.toVValueOrNull(classResolver) ?: run { skipped++; return@map null } + } + if (args.any { it == null }) continue + @Suppress("UNCHECKED_CAST") + val result = interpreter.execute(method, thisValue, args as List) + + when (result) { + is ExecutionResult.Unsupported, is ExecutionResult.Diverged -> skipped++ + is ExecutionResult.Threw -> + if (test.returnValue is TsTestValue.TsException) compared++ + else mismatches += "$ctx: concrete threw ${result.value}, symbolic returned ${test.returnValue}" + + is ExecutionResult.Returned -> { + if (test.returnValue is TsTestValue.TsException) { + mismatches += "$ctx: concrete returned ${result.value}, symbolic threw ${test.returnValue}" + } else if (matches(test.returnValue, result.value)) { + compared++ + } else if (containsPlaceholder(test.returnValue)) { + skipped++ + } else { + mismatches += "$ctx: symbolic=${test.returnValue}, concrete=${result.value}" + } + } + } + } + } + return Verdict(compared, skipped, mismatches) + } + + private fun containsPlaceholder(v: TsTestValue): Boolean = when (v) { + is TsTestValue.TsString -> v.value == SYMBOLIC_STRING_PLACEHOLDER + is TsTestValue.TsArray<*> -> v.values.any { containsPlaceholder(it) } + is TsTestValue.TsClass -> v.properties.values.any { containsPlaceholder(it) } + else -> false + } + + private fun matches(expected: TsTestValue, actual: VValue): Boolean = when (expected) { + is TsTestValue.TsNumber -> + actual is VNumber && (expected.number == actual.value || + (expected.number.isNaN() && actual.value.isNaN())) + + is TsTestValue.TsBoolean -> actual is VBool && expected.value == actual.value + is TsTestValue.TsString -> actual is VString && expected.value == actual.value + TsTestValue.TsNull -> actual == VNull + TsTestValue.TsUndefined -> actual == VUndefined + + is TsTestValue.TsArray<*> -> + actual is VArray && expected.values.size == actual.elements.size && + expected.values.zip(actual.elements).all { (e, a) -> matches(e, a) } + + is TsTestValue.TsClass -> + actual is VObject && expected.properties.all { (k, v) -> + matches(v, actual.fields[k] ?: VUndefined) + } + + else -> false + } + + @ParameterizedTest + @CsvSource( + "/samples/operators/Add.ts, Add", + "/samples/operators/Less.ts, Less", + "/samples/operators/Neg.ts, Neg", + "/samples/operators/And.ts, And", + "/samples/operators/Equality.ts, Equality", + "/samples/lang/Truthy.ts, Truthy", + "/samples/lang/TypeCoercion.ts, TypeCoercion", + ) + fun differential(resourcePath: String, className: String) { + val verdict = runDifferential(resourcePath, className) + println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}") + verdict.mismatches.forEach { println(" MISMATCH: $it") } + assertTrue(verdict.compared > 0) { "no successfully compared executions for $className" } + assertTrue(verdict.mismatches.isEmpty()) { + "differential mismatches for $className:\n" + verdict.mismatches.joinToString("\n") + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/JsSemanticsTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/JsSemanticsTest.kt new file mode 100644 index 0000000000..8e3acbe9c9 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/JsSemanticsTest.kt @@ -0,0 +1,124 @@ +package org.usvm.ts.pbt.interpreter + +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test + +class JsSemanticsTest { + + @Test + fun truthiness() { + assertFalse(JsSemantics.truthy(VNumber(0.0))) + assertFalse(JsSemantics.truthy(VNumber(-0.0))) + assertFalse(JsSemantics.truthy(VNumber(Double.NaN))) + assertTrue(JsSemantics.truthy(VNumber(-1.5))) + assertFalse(JsSemantics.truthy(VString(""))) + assertTrue(JsSemantics.truthy(VString("0"))) + assertFalse(JsSemantics.truthy(VNull)) + assertFalse(JsSemantics.truthy(VUndefined)) + assertTrue(JsSemantics.truthy(VObject(null))) + assertTrue(JsSemantics.truthy(VArray())) // [] is truthy! + } + + @Test + fun toNumberCoercions() { + assertEquals(0.0, JsSemantics.toNumber(VNull)) + assertTrue(JsSemantics.toNumber(VUndefined).isNaN()) + assertEquals(1.0, JsSemantics.toNumber(VBool(true))) + assertEquals(0.0, JsSemantics.toNumber(VString(""))) + assertEquals(0.0, JsSemantics.toNumber(VString(" "))) + assertEquals(42.0, JsSemantics.toNumber(VString(" 42 "))) + assertEquals(255.0, JsSemantics.toNumber(VString("0xFF"))) + assertTrue(JsSemantics.toNumber(VString("12abc")).isNaN()) + assertEquals(Double.POSITIVE_INFINITY, JsSemantics.toNumber(VString("Infinity"))) + // [] -> "" -> 0 ; [5] -> "5" -> 5 ; [1,2] -> "1,2" -> NaN + assertEquals(0.0, JsSemantics.toNumber(VArray())) + assertEquals(5.0, JsSemantics.toNumber(VArray(mutableListOf(VNumber(5.0))))) + assertTrue(JsSemantics.toNumber(VArray(mutableListOf(VNumber(1.0), VNumber(2.0)))).isNaN()) + assertTrue(JsSemantics.toNumber(VObject(null)).isNaN()) + } + + @Test + fun numberToStringMatchesJs() { + assertEquals("1", JsSemantics.numberToString(1.0)) + assertEquals("0", JsSemantics.numberToString(-0.0)) + assertEquals("-7", JsSemantics.numberToString(-7.0)) + assertEquals("1.5", JsSemantics.numberToString(1.5)) + assertEquals("NaN", JsSemantics.numberToString(Double.NaN)) + assertEquals("Infinity", JsSemantics.numberToString(Double.POSITIVE_INFINITY)) + assertEquals("-Infinity", JsSemantics.numberToString(Double.NEGATIVE_INFINITY)) + assertEquals("100000", JsSemantics.numberToString(1e5)) + } + + @Test + fun addOperator() { + // number + string -> concatenation + assertEquals(VString("12"), JsSemantics.add(VNumber(1.0), VString("2"))) + // undefined + 1 -> NaN + val r = JsSemantics.add(VUndefined, VNumber(1.0)) + assertTrue((r as VNumber).value.isNaN()) + // null + 1 -> 1 + assertEquals(VNumber(1.0), JsSemantics.add(VNull, VNumber(1.0))) + // [1] + [2] -> "12" + assertEquals( + VString("12"), + JsSemantics.add(VArray(mutableListOf(VNumber(1.0))), VArray(mutableListOf(VNumber(2.0)))), + ) + // {} + {} -> "[object Object][object Object]" + assertEquals( + VString("[object Object][object Object]"), + JsSemantics.add(VObject(null), VObject(null)), + ) + } + + @Test + fun looseEquality() { + assertTrue(JsSemantics.looseEq(VString(""), VNumber(0.0))) // "" == 0 + assertTrue(JsSemantics.looseEq(VNull, VUndefined)) // null == undefined + assertFalse(JsSemantics.looseEq(VNull, VNumber(0.0))) // null != 0 + assertTrue(JsSemantics.looseEq(VBool(true), VNumber(1.0))) // true == 1 + assertTrue(JsSemantics.looseEq(VString("1"), VBool(true))) // "1" == true + assertFalse(JsSemantics.looseEq(VNumber(Double.NaN), VNumber(Double.NaN))) + // [0] == false (array -> "0" -> 0, false -> 0) + assertTrue(JsSemantics.looseEq(VArray(mutableListOf(VNumber(0.0))), VBool(false))) + } + + @Test + fun strictEquality() { + assertFalse(JsSemantics.strictEq(VNumber(Double.NaN), VNumber(Double.NaN))) + assertTrue(JsSemantics.strictEq(VNumber(0.0), VNumber(-0.0))) + assertFalse(JsSemantics.strictEq(VString("1"), VNumber(1.0))) + val a = VArray() + assertTrue(JsSemantics.strictEq(a, a)) + assertFalse(JsSemantics.strictEq(VArray(), VArray())) + } + + @Test + fun relationalOperators() { + assertTrue(JsSemantics.ge(VNull, VNumber(0.0))) // null >= 0 (!) + assertFalse(JsSemantics.gt(VNull, VNumber(0.0))) // null > 0 -> false + assertFalse(JsSemantics.lt(VUndefined, VNumber(1.0))) // NaN comparison + assertTrue(JsSemantics.lt(VString("a"), VString("b"))) + assertTrue(JsSemantics.lt(VString("10"), VString("9"))) // lexicographic! + assertTrue(JsSemantics.lt(VString("10"), VNumber(90.0))) // numeric + } + + @Test + fun int32Conversions() { + assertEquals(0, JsSemantics.toInt32(VNumber(Double.NaN))) + assertEquals(0, JsSemantics.toInt32(VNumber(Double.POSITIVE_INFINITY))) + assertEquals(-1, JsSemantics.toInt32(VNumber(4294967295.0))) // 2^32-1 -> -1 + assertEquals(1, JsSemantics.toInt32(VNumber(1.9))) + assertEquals(-1, JsSemantics.toInt32(VNumber(-1.9))) + assertEquals(4294967295L, JsSemantics.toUint32(VNumber(-1.0))) + } + + @Test + fun typeofOperator() { + assertEquals("number", JsSemantics.typeOf(VNumber(1.0))) + assertEquals("object", JsSemantics.typeOf(VNull)) + assertEquals("undefined", JsSemantics.typeOf(VUndefined)) + assertEquals("object", JsSemantics.typeOf(VArray())) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/LoadEts.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/LoadEts.kt new file mode 100644 index 0000000000..cecb8f4b73 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/LoadEts.kt @@ -0,0 +1,120 @@ +package org.usvm.ts.pbt.util + +import mu.KotlinLogging +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsScene +import java.nio.file.Path +import kotlin.io.path.ExperimentalPathApi +import kotlin.io.path.extension +import kotlin.io.path.inputStream +import kotlin.io.path.relativeTo +import kotlin.io.path.walk + +private val logger = KotlinLogging.logger {} + +/** + * Load an [EtsFileDto] from a resource file. + * + * For example, `resources/ets/sample.json` can be loaded with: + * ``` + * val dto: EtsFileDto = loadEtsFileDtoFromResource("/ets/sample.json") + * ``` + */ +fun loadEtsFileDtoFromResource(jsonPath: String): EtsFileDto { + logger.debug { "Loading EtsIR from resource: '$jsonPath'" } + require(jsonPath.endsWith(".json")) { "File must have a '.json' extension: '$jsonPath'" } + getResourceStream(jsonPath).use { stream -> + return EtsFileDto.loadFromJson(stream) + } +} + +/** + * Load an [EtsFile] from a resource file. + * + * For example, `resources/ets/sample.json` can be loaded with: + * ``` + * val file: EtsFile = loadEtsFileFromResource("/ets/sample.json") + * ``` + */ +fun loadEtsFileFromResource(jsonPath: String): EtsFile { + val etsFileDto = loadEtsFileDtoFromResource(jsonPath) + return etsFileDto.toEtsFile() +} + +/** + * Load multiple [EtsFile]s from a resource directory. + * + * For example, all files in `resources/project/` can be loaded with: + * ``` + * val files: Sequence = loadMultipleEtsFilesFromResourceDirectory("/project") + * ``` + */ +@OptIn(ExperimentalPathApi::class) +fun loadMultipleEtsFilesFromResourceDirectory(dirPath: String): Sequence { + val rootPath = getResourcePath(dirPath) + return rootPath.walk().filter { it.extension == "json" }.map { path -> + loadEtsFileFromResource("$dirPath/${path.relativeTo(rootPath)}") + } +} + +fun loadMultipleEtsFilesFromMultipleResourceDirectories( + dirPaths: List, +): Sequence { + return dirPaths.asSequence().flatMap { loadMultipleEtsFilesFromResourceDirectory(it) } +} + +fun loadEtsProjectFromResources( + prefix: String, + modules: List, +): EtsScene { + logger.info { "Loading Ets project from '$prefix/' with ${modules.size} modules: $modules" } + val dirPaths = modules.map { "$prefix/$it" } + val files = loadMultipleEtsFilesFromMultipleResourceDirectories(dirPaths).toList() + logger.info { "Loaded ${files.size} files" } + return EtsScene(files) +} + +//----------------------------------------------------------------------------- + +/** + * Load an [EtsFileDto] from a file. + * + * For example, `data/sample.json` can be loaded with: + * ``` + * val dto: EtsFileDto = loadEtsFileDto(Path("data/sample.json")) + * ``` + */ +fun loadEtsFileDto(path: Path): EtsFileDto { + require(path.extension == "json") { "File must have a '.json' extension: $path" } + path.inputStream().use { stream -> + return EtsFileDto.loadFromJson(stream) + } +} + +/** + * Load an [EtsFile] from a file. + * + * For example, `data/sample.json` can be loaded with: + * ``` + * val file: EtsFile = loadEtsFile(Path("data/sample.json")) + * ``` + */ +fun loadEtsFile(path: Path): EtsFile { + val etsFileDto = loadEtsFileDto(path) + return etsFileDto.toEtsFile() +} + +/** + * Load multiple [EtsFile]s from a directory. + * + * For example, all files in `data` can be loaded with: + * ``` + * val files: Sequence = loadMultipleEtsFilesFromDirectory(Path("data")) + * ``` + */ +@OptIn(ExperimentalPathApi::class) +fun loadMultipleEtsFilesFromDirectory(dirPath: Path): Sequence { + return dirPath.walk().filter { it.extension == "json" }.map { loadEtsFile(it) } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/Resources.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/Resources.kt new file mode 100644 index 0000000000..f28b3377cd --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/util/Resources.kt @@ -0,0 +1,23 @@ +package org.usvm.ts.pbt.util + +import mu.KotlinLogging +import java.io.InputStream +import java.nio.file.Path +import kotlin.io.path.toPath + +private val logger = KotlinLogging.logger {} + +fun getResourcePathOrNull(res: String): Path? { + require(res.startsWith("/")) { "Resource path must start with '/': '$res'" } + return object {}::class.java.getResource(res)?.toURI()?.toPath() +} + +fun getResourcePath(res: String): Path { + return getResourcePathOrNull(res) ?: error("Resource not found: '$res'") +} + +fun getResourceStream(res: String): InputStream { + require(res.startsWith("/")) { "Resource path must start with '/': '$res'" } + return object {}::class.java.getResourceAsStream(res) + ?: error("Resource not found: '$res'") +} diff --git a/usvm-ts-pbt/src/test/resources/pbt/HybridSamples.ts b/usvm-ts-pbt/src/test/resources/pbt/HybridSamples.ts new file mode 100644 index 0000000000..0fe6eb5280 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/pbt/HybridSamples.ts @@ -0,0 +1,49 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class HybridSamples { + // Random testing covers everything except the magic branch; + // the targeted symbolic phase must reach it. The condition is arithmetic + // (solution x = 49382) so that constant mining cannot guess it directly. + magic(x: number): number { + if (x * 2 === 98764) { + return 42; + } + if (x > 0) { + return 1; + } + return 0; + } + + // PBT should find the crash and shrink the inputs. + crashy(a: number[], i: number): number { + if (i >= 0 && i < a.length) { + return a[i]; + } + throw new Error("index out of bounds"); + } + + // The hint-sensitive case: with an untyped parameter the engine builds a + // fake object; the observed-type profile { NUMBER } should prune the search. + // Deliberately arithmetic-only: usvm-ts string support is too weak for + // `typeof x === "number"`-style guards. + anyParam(x): number { + if (x * 2 === 84) { + return 1; + } + return 2; + } + + // Three untyped parameters: without hints the engine explores up to 3^3 + // discriminator combinations of the fake objects; with { NUMBER } hints + // for all three, exactly one. + manyUntyped(a, b, c): number { + if (a + b + c === 30000) { + if (a * 2 === b && b * 3 === c) { + return 1; + } + return 2; + } + return 3; + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInputTypeHints.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInputTypeHints.kt new file mode 100644 index 0000000000..c5f8b5592b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInputTypeHints.kt @@ -0,0 +1,42 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsMethod + +/** + * Runtime type tags observed for input values during a concrete (e.g. PBT) phase. + * Used to constrain the symbolic search over dynamically-typed inputs. + */ +enum class TsHintType { + NUMBER, + BOOLEAN, + STRING, + NULL, + UNDEFINED, + OBJECT, + ARRAY, +} + +/** + * Observed input type profiles: method key -> (parameter index -> observed type tags). + * + * When a parameter's declared type is unresolved (any/unknown/union), the interpreter + * normally creates a *fake object* whose type discriminators are unconstrained, + * which multiplies the search space. Hints restrict the discriminators to the + * observed set (see `TsInterpreter.getInitialState`). + * + * The hints are an *unsound* optimization by design: a fallback run without hints + * is expected at the orchestration level when a target is not reached with them. + */ +data class TsInputTypeHints( + val byMethod: Map>> = emptyMap(), +) { + fun forParameter(method: EtsMethod, index: Int): Set? = + byMethod[keyOf(method)]?.get(index)?.takeIf { it.isNotEmpty() } + + companion object { + val EMPTY = TsInputTypeHints() + + /** The single canonical key shared by hint producers and consumers. */ + fun keyOf(method: EtsMethod): String = method.signature.toString() + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 6776638408..92211937bc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -4,4 +4,10 @@ data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, + /** + * Observed input type profiles from a dynamic (e.g. PBT) phase. + * Restrict fake-object type discriminators for unresolved parameters. + * [TsInputTypeHints.EMPTY] preserves the default behavior. + */ + val inputTypeHints: TsInputTypeHints = TsInputTypeHints.EMPTY, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 850f97e9de..b69ad2c8d8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -34,7 +34,9 @@ import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.callExpr import org.usvm.StepResult import org.usvm.StepScope +import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.UInterpreter import org.usvm.UIteExpr import org.usvm.api.evalTypeEquals @@ -48,6 +50,7 @@ import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsGraph +import org.usvm.machine.TsHintType import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsOptions import org.usvm.machine.TsVirtualMethodCallStmt @@ -781,11 +784,17 @@ class TsInterpreter( // If the parameter type is unresolved, we create a fake object for it val bool = mkRegisterReading(idx, boolSort) val fp = mkRegisterReading(idx, fp64Sort) - val ref = mkRegisterReading(idx, addressSort) - val fakeObject = state.mkFakeValue(null, bool, fp, ref) + val refReading = mkRegisterReading(idx, addressSort) + val fakeObject = state.mkFakeValue(null, bool, fp, refReading) val lValue = mkRegisterStackLValue(addressSort, idx) state.memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr) state.saveSortForLocal(idx, addressSort) + + // Observed-type hints from a dynamic phase (if any) restrict the + // fake object's type discriminators, pruning the type search space. + options.inputTypeHints.forParameter(method, i)?.let { hints -> + applyParameterTypeHints(state, fakeObject, refReading, hints) + } } else { state.saveSortForLocal(idx, parameterSort) } @@ -798,6 +807,69 @@ class TsInterpreter( state } + /** + * Constrain the type discriminators of an input fake object according to the + * type tags observed during a dynamic (e.g. PBT) phase. + * + * This is a deliberately *unsound* pruning: callers are expected to fall back + * to a hint-free run when a target is not reached under hints (or when the + * initial constraints become unsatisfiable). + */ + private fun applyParameterTypeHints( + state: TsState, + fakeObject: UConcreteHeapRef, + refReading: UHeapRef, + hints: Set, + ): Unit = with(ctx) { + val fakeType = fakeObject.getFakeType(state.memory) + + val refHints = hints.intersect(REF_HINTS) + + // 1. Restrict the discriminator to the observed value kinds. + val allowedDiscriminators = buildList { + if (TsHintType.NUMBER in hints) add(fakeType.fpTypeExpr) + if (TsHintType.BOOLEAN in hints) add(fakeType.boolTypeExpr) + if (refHints.isNotEmpty()) add(fakeType.refTypeExpr) + } + if (allowedDiscriminators.isEmpty()) return@with + state.pathConstraints += mkOr(allowedDiscriminators) + + // 2. Refine the ref slot under the ref discriminator. + if (refHints.isNotEmpty()) { + val refCases = refHints.map { hint -> + when (hint) { + TsHintType.NULL -> mkHeapRefEq(refReading, mkTsNullValue()) + TsHintType.UNDEFINED -> mkHeapRefEq(refReading, mkUndefinedValue()) + TsHintType.STRING -> mkAnd( + mkNot(mkHeapRefEq(refReading, mkTsNullValue())), + mkNot(mkHeapRefEq(refReading, mkUndefinedValue())), + state.memory.types.evalTypeEquals(refReading, EtsStringType), + ) + + // For objects/arrays the discriminator restriction is the main prune; + // we only exclude null/undefined here. + TsHintType.OBJECT, TsHintType.ARRAY -> mkAnd( + mkNot(mkHeapRefEq(refReading, mkTsNullValue())), + mkNot(mkHeapRefEq(refReading, mkUndefinedValue())), + ) + + else -> error("Non-ref hint in ref cases: $hint") + } + } + state.pathConstraints += mkImplies(fakeType.refTypeExpr, mkOr(refCases)) + } + } + + private companion object { + private val REF_HINTS = setOf( + TsHintType.STRING, + TsHintType.NULL, + TsHintType.UNDEFINED, + TsHintType.OBJECT, + TsHintType.ARRAY, + ) + } + // TODO: expand with interpreter implementation private val EtsStmt.nextStmt: EtsStmt? get() = graph.successors(this).firstOrNull() diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt similarity index 100% rename from usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt rename to usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt similarity index 96% rename from usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt rename to usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt index 3e81ed3d14..28f4608d5d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt @@ -87,6 +87,23 @@ class TsTestResolver { return TsTest(method, before, after, result, trace = emptyList()) } + /** + * Resolve only the *input* valuation (`this` + parameters) of a state. + * + * Unlike [resolve], this also works for states that have not terminated yet + * (e.g. states captured at the moment they reach a symbolic execution target), + * where no method result is available. + */ + fun resolveInputs(method: EtsMethod, state: TsState): TsParametersState = with(state.ctx) { + val model = state.models.first() + val memory = state.memory + + prepareForResolve(state) + + val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects) + return beforeMemoryScope.withMode(ResolveMode.MODEL) { resolveState() } + } + private fun prepareForResolve(state: TsState) { state.lValuesToAllocatedFakeObjects.forEach { (lValue, fakeObject) -> when (lValue) {