diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 080242197..13f9f2912 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/build.gradle.kts b/build.gradle.kts index 8223024ee..362cef936 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 a408cda64..4d0fb4c82 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 000000000..219474312 --- /dev/null +++ b/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 +``` diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts new file mode 100644 index 000000000..4393ff574 --- /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 000000000..65f10fadb --- /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 000000000..07b6f7fc9 --- /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; +}