From 57a4fd1485e68c4ae051fe7c7f4026a9722cfe4b Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 22 Aug 2026 19:41:02 +0300 Subject: [PATCH 1/2] [TS PBT] Establish native frontend integration baseline --- .github/workflows/ci.yml | 3 ++ build.gradle.kts | 1 + settings.gradle.kts | 1 + usvm-ts-pbt/README.md | 39 +++++++++++++++ usvm-ts-pbt/build.gradle.kts | 10 ++++ .../org/usvm/ts/pbt/FrontendBaselineTest.kt | 49 +++++++++++++++++++ .../resources/baseline/FrontendBaseline.ts | 7 +++ 7 files changed, 110 insertions(+) create mode 100644 usvm-ts-pbt/README.md create mode 100644 usvm-ts-pbt/build.gradle.kts create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/FrontendBaselineTest.kt create mode 100644 usvm-ts-pbt/src/test/resources/baseline/FrontendBaseline.ts diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0802421971..9bea4645b4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -159,6 +159,9 @@ jobs: - name: Run TS tests run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check + - name: Run TS PBT integration baseline + run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check + - name: Upload Gradle reports if: (!cancelled()) uses: actions/upload-artifact@v4 diff --git a/build.gradle.kts b/build.gradle.kts index 8223024eeb..362cef9363 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -21,6 +21,7 @@ tasks.register("validateProjectList") { project(":usvm-jvm-instrumentation"), project(":usvm-python"), project(":usvm-ts"), + project(":usvm-ts-pbt"), project(":usvm-ts-dataflow"), ) diff --git a/settings.gradle.kts b/settings.gradle.kts index a408cda64d..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") diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md new file mode 100644 index 0000000000..231ebbd139 --- /dev/null +++ b/usvm-ts-pbt/README.md @@ -0,0 +1,39 @@ +# USVM TypeScript property-based testing + +This module is the integration baseline for the fast-check and symbolic-execution pipeline tracked by +[issue #346](https://github.com/UnitTestBot/usvm/issues/346). It currently contains only the native TypeScript frontend +smoke test; property execution is introduced by later issues in epic #345. + +## Prerequisites + +- JDK 11 (the version used by the USVM TypeScript CI job). +- Gradle 8.11 through the repository's `./gradlew` wrapper. +- Node.js 18.18 or newer on `PATH`; JacoDB `neo` uses Node.js 20.20.2. + +The module resolves JacoDB `neo` commit `9ea33879c9`. The published `jacodb-ets` artifact bundles the native +`ts-frontend` runtime and matching TypeScript libraries, so the focused check needs neither ArkAnalyzer nor +`npm install`. + +## Focused check + +```shell +env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ + ./gradlew --no-daemon :usvm-ts-pbt:clean :usvm-ts-pbt:check +``` + +The smoke test loads `FrontendBaseline.ts`, finds `absoluteValue` in EtsIR, and verifies its source origins. + +## Local JacoDB checkout + +For frontend development, substitute a local JacoDB `neo` checkout: + +```shell +env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ + ./gradlew --no-daemon -PuseLocalJacodb=/absolute/path/to/jacodb \ + :usvm-ts-pbt:clean :usvm-ts-pbt:check +``` + +The composite build installs and builds `jacodb-ets/ts-frontend` through its Gradle tasks. `ETS_FRONTEND_DIR`, +`ETS_FRONTEND_SCRIPT`, and `NODE_EXECUTABLE` remain available as JacoDB runtime overrides when testing an already +built frontend directly. Use a regular JacoDB clone rather than a linked worktree: JacoDB's Git hooks Gradle plugin +currently requires a `.git` directory. diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts new file mode 100644 index 0000000000..4393ff574c --- /dev/null +++ b/usvm-ts-pbt/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("usvm.kotlin-conventions") +} + +dependencies { + implementation(project(":usvm-ts")) + implementation(Libs.jacodb_ets) + + testImplementation(Libs.logback) +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/FrontendBaselineTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/FrontendBaselineTest.kt new file mode 100644 index 0000000000..65f10fadbe --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/FrontendBaselineTest.kt @@ -0,0 +1,49 @@ +package org.usvm.ts.pbt + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsSourceSpan +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class FrontendBaselineTest { + @Test + fun `native frontend loads a TypeScript method with source origins`() { + val source = resourcePath("/baseline/FrontendBaseline.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val method = EtsScene(listOf(file)).projectClasses + .flatMap { it.methods } + .single { it.name == "absoluteValue" } + + assertTrue(method.cfg.stmts.isNotEmpty(), "absoluteValue must have a non-empty CFG") + + val origins = method.cfg.stmts.mapNotNull { it.location.origin } + assertTrue(origins.isNotEmpty(), "absoluteValue statements must retain source origins") + origins.forEach(::assertValidOrigin) + } + + private fun assertValidOrigin(origin: EtsSourceSpan) { + assertTrue( + origin.fileName.endsWith("FrontendBaseline.ts"), + "Unexpected source file: ${origin.fileName}", + ) + assertTrue(origin.startOffset >= 0, "Start offset must be non-negative: $origin") + assertTrue(origin.endOffset >= origin.startOffset, "Offsets must be ordered: $origin") + assertTrue(origin.startLine >= 0, "Start line must be non-negative: $origin") + assertTrue(origin.startColumn >= 0, "Start column must be non-negative: $origin") + assertTrue(origin.endLine >= origin.startLine, "Lines must be ordered: $origin") + if (origin.endLine == origin.startLine) { + assertTrue(origin.endColumn >= origin.startColumn, "Columns must be ordered: $origin") + } + assertTrue(origin.nodeKind.isNotBlank(), "TypeScript node kind must be present: $origin") + } + + private fun resourcePath(name: String): Path { + val resource = assertNotNull(javaClass.getResource(name), "Missing test resource $name") + return Paths.get(resource.toURI()) + } +} diff --git a/usvm-ts-pbt/src/test/resources/baseline/FrontendBaseline.ts b/usvm-ts-pbt/src/test/resources/baseline/FrontendBaseline.ts new file mode 100644 index 0000000000..07b6f7fc9b --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/baseline/FrontendBaseline.ts @@ -0,0 +1,7 @@ +export function absoluteValue(value: number): number { + if (value < 0) { + return -value; + } + + return value; +} From 18d781e1840e4fd50557309e7e275bf303c516ef Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 22 Aug 2026 19:58:25 +0300 Subject: [PATCH 2/2] [TS PBT] Isolate native frontend CI --- .github/workflows/ci.yml | 26 +++++++++++++++++++++++--- usvm-ts-pbt/README.md | 30 +++++++++--------------------- 2 files changed, 32 insertions(+), 24 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9bea4645b4..13f9f2912a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -159,9 +159,6 @@ jobs: - name: Run TS tests run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check - - name: Run TS PBT integration baseline - run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check - - name: Upload Gradle reports if: (!cancelled()) uses: actions/upload-artifact@v4 @@ -170,6 +167,29 @@ jobs: path: '**/build/reports/' retention-days: 1 + ci-ts-pbt: + runs-on: ubuntu-24.04 + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Setup Java JDK + uses: actions/setup-java@v4 + with: + java-version: ${{ env.JAVA }} + distribution: ${{ env.JAVA_DISTRIBUTION }} + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + + - name: Set up Node + uses: actions/setup-node@v4 + with: + node-version: 22 + + - name: Run TS PBT integration baseline + run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check + lint: runs-on: ubuntu-latest steps: diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 231ebbd139..2194743127 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -1,39 +1,27 @@ # USVM TypeScript property-based testing -This module is the integration baseline for the fast-check and symbolic-execution pipeline tracked by -[issue #346](https://github.com/UnitTestBot/usvm/issues/346). It currently contains only the native TypeScript frontend -smoke test; property execution is introduced by later issues in epic #345. +`usvm-ts-pbt` is the integration baseline for the fast-check and symbolic-execution pipeline tracked by +[issue #346](https://github.com/UnitTestBot/usvm/issues/346). Property execution is introduced by later issues. -## Prerequisites +## Design -- JDK 11 (the version used by the USVM TypeScript CI job). -- Gradle 8.11 through the repository's `./gradlew` wrapper. -- Node.js 18.18 or newer on `PATH`; JacoDB `neo` uses Node.js 20.20.2. +- TypeScript is parsed by the repository's default JacoDB native `ts-frontend`; ArkAnalyzer is not required. +- The module follows the repository-wide JacoDB dependency without a separate version pin. +- The smoke test loads a TypeScript method into EtsIR and verifies its CFG and `EtsSourceSpan` origins. -The module resolves JacoDB `neo` commit `9ea33879c9`. The published `jacodb-ets` artifact bundles the native -`ts-frontend` runtime and matching TypeScript libraries, so the focused check needs neither ArkAnalyzer nor -`npm install`. +## Run -## Focused check +Requires JDK 11, Node.js 18.18 or newer, and the repository's Gradle wrapper. ```shell env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ ./gradlew --no-daemon :usvm-ts-pbt:clean :usvm-ts-pbt:check ``` -The smoke test loads `FrontendBaseline.ts`, finds `absoluteValue` in EtsIR, and verifies its source origins. - -## Local JacoDB checkout - -For frontend development, substitute a local JacoDB `neo` checkout: +To substitute a local JacoDB checkout: ```shell env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ ./gradlew --no-daemon -PuseLocalJacodb=/absolute/path/to/jacodb \ :usvm-ts-pbt:clean :usvm-ts-pbt:check ``` - -The composite build installs and builds `jacodb-ets/ts-frontend` through its Gradle tasks. `ETS_FRONTEND_DIR`, -`ETS_FRONTEND_SCRIPT`, and `NODE_EXECUTABLE` remain available as JacoDB runtime overrides when testing an already -built frontend directly. Use a regular JacoDB clone rather than a linked worktree: JacoDB's Git hooks Gradle plugin -currently requires a `.git` directory.