[TS] One-command measurement pipeline for open-source TS projects

CaelmBleidd · CaelmBleidd · commit b1b910e77424 · 2026-07-08T12:08:24.000+03:00
./run-project.sh &lt;git-url | corpus-name | local-path&gt; [--include dir]
[--modes ...] [--commit sha] does the whole loop: clone, build the jacodb
ts-frontend if missing, run the hybrid analyzer over all ablation modes
with per-file fault isolation, aggregate, and write per-mode JSON reports,
a summary table and a per-method CSV under results/&lt;name&gt;/.

Demo on loiane/javascript-datastructures-algorithms (src/, 307 methods,
670 branch edges): PBT-only 62.5% branches in 1.7s; symbolic-only 57.2%
in 427s; hybrid 75.1% in 243s (84/251 residual targets reached).
diff --git a/usvm-ts-pbt/benchmarks/README.md b/usvm-ts-pbt/benchmarks/README.md
@@ -1,58 +1,78 @@
 # Benchmark infrastructure: hybrid analysis on open-source TypeScript
 
 Batch experiments for the hybrid PBT + targeted symbolic execution pipeline
-over an open-source TS corpus, using the **native TS parser from jacodb**
+over open-source TS projects, using the **native TS parser from jacodb**
 (`jacodb-ets/ts-frontend`, jacodb PR #361) as the EtsIR provider.
 
-## 1. One-time setup
+## TL;DR — one command per project
 
 ```bash
-# 1. Build the jacodb ts-frontend (from the jacodb checkout on the PR #361 branch):
-cd <jacodb>/jacodb-ets/ts-frontend && npm install && npm run build
+# by URL: clones into corpus/, analyzes, aggregates, writes reports
+./run-project.sh https://github.com/TheAlgorithms/TypeScript.git --include maths
 
-# 2. Fetch the corpus (defined in corpus.json, pinned commits):
-./fetch-corpus.sh          # requires git + jq; clones into benchmarks/corpus/
+# 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 <target> --modes PBT_ONLY,HYBRID --max-files 40 --target-timeout 5
 ```
 
-Until jacodb PR #361 is merged and the usvm dependency pin is bumped, substitute
-the local jacodb build via the opt-in composite build flag `-PuseLocalJacodb=<path>`.
+The script does everything end-to-end:
+
+1. resolves the project (clone by URL / corpus name / local path; `--commit <sha>`
+   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/<name>/`:
+   - `<name>-<MODE>.json` — full machine-readable report per mode
+     (per-method coverage, coverage timelines, per-target wall time,
+     hint/fallback attribution, unsupported-execution counters),
+   - `<name>-summary.md` — the mode-comparison table,
+   - `<name>.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
 
-## 2. Running experiments
+The underlying CLI offers finer control:
 
 ```bash
 export ETS_IR_PROVIDER=ts-frontend
 export ETS_FRONTEND_DIR=<jacodb>/jacodb-ets/ts-frontend
-export ARKANALYZER_DIR=<pinned-arkanalyzer>   # only needed for provider=arkanalyzer
 
 ./gradlew -PuseLocalJacodb=<jacodb> :usvm-ts-pbt:runHybrid --args="\
-    usvm-ts-pbt/benchmarks/corpus/TheAlgorithms-TypeScript/maths \
-    --recursive \
+    <dir-or-file.ts> --recursive \
     --modes PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS \
     --pbt-iterations 1000 --target-timeout 10 \
-    --out usvm-ts-pbt/benchmarks/results/maths"
-```
-
-This produces one `HybridReport` JSON per mode: `<out>-<MODE>.json`.
-Paths are resolved relative to the repository root (the `runHybrid` working dir).
-
-Per-file isolation: frontend/load failures and per-method analysis failures are
-counted and logged, never abort the batch (honest-numbers principle: the reports
-carry `unsupported`/failure counters).
+    --out results/my-run"
 
-## 3. Aggregation
-
-```bash
-python3 aggregate.py results/maths-*.json --csv results/maths.csv
+python3 aggregate.py results/my-run-*.json --csv results/my-run.csv
 ```
 
-Prints a markdown mode-comparison table (branch/stmt coverage, PBT failures,
-targets reached/replay-confirmed/fallbacks, wall time) and optionally a
-per-method CSV for plots. Raw JSON reports retain full coverage timelines and
-per-target attribution for the paper's ablation analysis.
+See `./gradlew :usvm-ts-pbt:runHybrid --args=""` for the full option list
+(`--class`, `--method`, `--exclude`, `--seed`, `--no-fallback`, ...).
 
-## 4. Corpus policy
+## Interpreting the numbers
 
-`corpus.json` pins each project to a commit. Preferred projects: 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 `Unsupported` at call sites and are reported, not guessed.
+- **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/corpus.json b/usvm-ts-pbt/benchmarks/corpus.json
@@ -22,7 +22,7 @@
       "url": "https://github.com/loiane/javascript-datastructures-algorithms.git",
       "commit": "e8ee8f9b8a07589533c4243a210d4cea7b090b10",
       "include": [
-        "src/ts"
+        "src"
       ],
       "excludePatterns": [
         ".test.ts",
diff --git a/usvm-ts-pbt/benchmarks/run-project.sh 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 <git-url | local-path | corpus-name> [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/<name>/.
+#
+# 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 <subdir>       analyze only this subdirectory of the project (repeatable)
+#   --modes <M1,M2,...>      ablation modes (default: PBT_ONLY,SYMBOLIC_ONLY,HYBRID,HYBRID_WITH_HINTS)
+#   --pbt-iterations <n>     PBT budget per method (default: 1000)
+#   --target-timeout <sec>   per-target symbolic timeout (default: 10)
+#   --max-files <n>          cap the number of files (default: unlimited)
+#   --seed <n>               PBT seed (default: 0)
+#   --commit <sha>           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"
