[TS PBT] Establish a clean integration baseline

.github/workflows/ci.yml

@@ -167,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:

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"),
         )
 

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")

usvm-ts-pbt/README.md

@@ -0,0 +1,27 @@
+# USVM TypeScript property-based testing
+
+`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.
+
+## Design
+
+- 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.
+
+## Run
+
+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
+```
+
+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
+```

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)
+}

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())
+    }
+}

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;
+}