diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md new file mode 100644 index 000000000..ac73bcc1b --- /dev/null +++ b/usvm-ts-pbt/DESIGN.md @@ -0,0 +1,200 @@ +# Kotlin–TypeScript fast-check integration + +This document describes the internal boundary between Kotlin and the private Node adapter. For the public property +API and CLI examples, see [README.md](README.md). + +## Design goals + +- Kotlin owns property definitions, validation, registries, orchestration, and public results. +- Node is a thin adapter around fast-check and direct TypeScript loading. +- The JSON exchange is one request and one response from the same packaged distribution; it has no persistence or + compatibility negotiation. +- Failures are typed without exposing runtime-dependent Node stack traces. +- A blocked or noisy child process cannot hang the JVM or exhaust unbounded memory. + +## Components and dependencies + +```mermaid +flowchart LR + subgraph Kotlin + Caller[Backend caller] + CLI[FastCheckCli] + Registry[PropertyRegistry] + Model[Property model and validation] + Backend[FastCheckBackend] + Process[FastCheckProcessClient] + Projection[FastCheckProjectionClient] + end + + subgraph Node_adapter[Private Node adapter] + ExecutionCLI[execution-cli.ts] + ProjectionCLI[projection-cli.ts] + Execute[execute-property.ts] + Domains[project-domain.ts] + EntryPoints[entry-point.ts] + Values[js-value.ts] + Diagnostics[diagnostics.ts] + end + + FastCheck[fast-check] + Tsx[tsx] + UserTS[User TypeScript source] + + CLI --> Registry + CLI --> Backend + Caller --> Backend + Registry --> Model + Backend --> Model + Backend --> Process + Process --> ExecutionCLI + Projection --> ProjectionCLI + ExecutionCLI --> Execute + Execute --> Domains + Execute --> EntryPoints + Execute --> Values + ProjectionCLI --> Domains + Diagnostics --> ExecutionCLI + Diagnostics --> Domains + Diagnostics --> EntryPoints + Domains --> FastCheck + Execute --> FastCheck + EntryPoints --> Tsx + Tsx --> UserTS +``` + +| Component | Responsibility | +| --- | --- | +| Kotlin model and validation | Define one backend-neutral property and reject invalid structure before execution. | +| Registry and CLI | Select Kotlin-defined properties and turn user options into a run configuration. | +| `FastCheckBackend` | Validate examples, resolve source roots, and create the adapter request. | +| `FastCheckProcessClient` | Supervise Node with coroutines, bounded I/O, hard deadlines, and response validation. | +| `execution-cli.ts` | Read one JSON request, protect protocol stdout from user logging, and write one response. | +| `execute-property.ts` | Build the fast-check property, run it, and translate `RunDetails` into the common result. | +| `project-domain.ts` | Translate domain descriptors into real `fc.Arbitrary` instances. | +| `entry-point.ts` | Resolve exactly one module below a source root and invoke its typed export through `tsx`. | +| Value and diagnostic modules | Preserve JavaScript values losslessly and define adapter-emitted diagnostic identifiers. | + +`projection-cli.ts` is the smaller sampling path used by `FastCheckProjectionClient`. It shares domain and value +translation with property execution but does not load or call user predicates. + +## Boundary contract + +```mermaid +flowchart LR + Definition[PropertyDefinition] --> Validate[Kotlin validation] + Validate --> Request[Execution request] + Request --> Node[One Node process] + Node --> Arbitraries[Domains to arbitraries] + Arbitraries --> Check[fc.check] + SourceRoots[Source roots] --> Load[tsx module loading] + Load --> Check + Check --> Response[Success or diagnostic response] + Response --> Verify[Kotlin response validation] + Verify --> Result[PropertyRunResult or PbtBackendException] +``` + +The execution request contains `manifest`, `sourceRoots`, optional `seed` and `replayPath`, `numRuns`, +`timeoutMillis`, and tagged `examples`. A response is either: + +```text +{ status: "ok", result: PropertyRunResult } +{ status: "error", diagnostics: [{ kind, code, message, path }] } +``` + +There is intentionally no request ID, operation name, schema version, protocol version, backend ID, or backend +version. The exchange is private, one-shot, and produced and consumed by the same build. Adding compatibility +metadata would create branches that no supported workflow uses. + +Kotlin validates trusted model objects and examples early so callers get local errors. Node validates the decoded +JSON again because the process boundary must not trust malformed input. Diagnostic codes have one owner per +language: `PbtDiagnosticCode.kt` for Kotlin and `diagnostics.ts` for Node. Node also sends the diagnostic category, +so Kotlin never infers error meaning from code prefixes. + +## One property run + +```mermaid +sequenceDiagram + participant Caller + participant Backend as FastCheckBackend + participant Client as ProcessClient + participant Node as execution-cli.ts + participant FC as fast-check + participant TS as User predicate + + Caller->>Backend: run(property, configuration) + Backend->>Backend: validate property, roots, and examples + Backend->>Client: check(request) + Client->>Node: start process and write JSON + par concurrent process I/O + Client->>Node: drain stdout + and + Client->>Node: drain stderr + end + Node->>Node: validate request and resolve entry points + Node->>FC: check(property, parameters) + loop generation, replay, examples, shrinking + FC->>TS: predicate(values) + TS-->>FC: boolean or Promise + end + FC-->>Node: RunDetails + Node-->>Client: one JSON response + Client->>Client: validate exit, size, shape, category, and property ID + Client-->>Backend: PropertyRunResult + Backend-->>Caller: PropertyRunResult +``` + +Input order is preserved from `PropertyDefinition.inputs` to the positional TypeScript arguments. If either the +predicate or precondition is asynchronous, the adapter uses `fc.asyncProperty`; otherwise it uses `fc.property`. +A false precondition becomes `fc.pre(false)`, leaving skip accounting to fast-check. + +## Results, errors, and timeouts + +```mermaid +flowchart TD + Check[Property execution] --> Held{Outcome} + Held -->|held| Success[SUCCESS result] + Held -->|falsified| Failure[FAILURE result with counterexample] + Held -->|fast-check timeout| TimeoutResult[FAILURE result with timeout details] + Held -->|typed adapter error| Diagnostic[Error response with explicit category] + Diagnostic --> Exception[PbtBackendException] + Held -->|unexpected Node failure| Exit[Non-zero exit or invalid response] + Exit --> Transport[PROCESS_FAILURE or PROTOCOL_ERROR] + Held -->|hard JVM deadline| Kill[Terminate, then force-kill] + Kill --> HardTimeout[TIMEOUT exception] +``` + +Falsification and a timeout cleanly reported by fast-check are completed property results. Invalid input, +entry-point failures, process failures, malformed responses, and the JVM hard timeout are infrastructure +exceptions. + +The execution client starts stdout, stderr, and stdin work concurrently on the coroutine I/O dispatcher. Requests +and stdout are limited to 4 MiB; stderr is limited to 64 KiB. These are transport safety bounds, not property-policy +limits. The hard deadline is the property timeout plus two seconds for transport, followed by a 250 ms graceful +shutdown before force-kill. The only run-control maximum is `2^31 - 1` milliseconds because Node timers use signed +32-bit delays; runs, examples, and replay paths have no arbitrary count or length caps. + +## Runtime packaging + +Gradle installs pinned adapter dependencies, compiles only the private adapter, and packages `dist/src` plus its +runtime dependencies in the application distribution. User TypeScript stays as source. During repository tests, +Gradle passes the adapter directory through a JVM system property; an installed distribution resolves it next to +the application libraries. Node.js 18.18 or newer is required, and runtime archives carry an OS/architecture +classifier because `tsx` depends on a native esbuild package. + +## Testing boundaries + +- TypeScript unit tests cover value encoding, domain projection, source-root containment, entry-point contracts, + fast-check behavior, and the one-document CLI boundary. +- Kotlin unit tests cover the property model, registry, CLI selection, example membership, and response validation. +- Process tests use tiny temporary Node programs only for transport behavior that is difficult to force through + fast-check: startup failure, non-zero exit, malformed output, explicit diagnostic categories, and hard timeout. +- Backend integration tests execute real uncompiled TypeScript through the packaged adapter, including replay, + shrinking, explicit examples, preconditions, async predicates, and timeouts. + +## Non-goals + +- Persisting requests or results, or supporting old wire formats. +- Discovering properties by scanning TypeScript source roots. +- Compiling user TypeScript as part of the PBT workflow. +- Reimplementing generation, replay, skip accounting, or shrinking in Kotlin. +- Recording coverage or other per-run artifacts in this change. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 174b20733..ffb531deb 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -1,27 +1,10 @@ # USVM TypeScript property-based testing `usvm-ts-pbt` is the Kotlin-owned integration layer for concrete property-based testing backends and USVM. -Kotlin defines each property once; fast-check is the first replaceable concrete backend. - -## Architecture - -```text -Kotlin PropertyDefinition - | - +--> versioned PropertyManifest - | - +--> PBT projection ----------> private fast-check Node adapter - | - +--> symbolic projection -----> USVM (#351) -``` - -Kotlin owns property identity, ordered inputs, domain semantics, TypeScript entry-point references, validation, -capability aggregation, and later orchestration. Common Kotlin code never contains `fc.Arbitrary` or another -backend-native generator type. +Kotlin defines each property once; fast-check is the first concrete backend. -Predicate and precondition bodies remain exported TypeScript functions. Kotlin refers to each function by a -normalized project-relative module path, export name, and synchronous or asynchronous execution kind. Issue #347 -validates and serializes those references but does not load or execute the functions. +See [DESIGN.md](DESIGN.md) for component responsibilities, Kotlin–TypeScript data flow, process supervision, and +runtime packaging. ## Kotlin property model @@ -31,7 +14,11 @@ val property = PropertyDefinition( inputs = listOf( PropertyInput( name = "values", - domain = ArrayDomain(IntegerDomain(-100, 100), minLength = 0, maxLength = 20), + domain = ArrayDomain( + element = IntegerDomain(min = -100, max = 100), + minLength = 0, + maxLength = 20, + ), ), ), predicate = TypeScriptEntryPoint( @@ -39,12 +26,16 @@ val property = PropertyDefinition( exportName = "reverseTwicePreservesValues", ), ) - -val manifest = property.toManifest() ``` -Input order is significant because TypeScript parameters are positional. Names are unique and are retained in -diagnostics and artifacts. +Input order is significant because TypeScript parameters are positional. The referenced function remains in the +user's TypeScript source tree: + +```typescript +export function reverseTwicePreservesValues(values: number[]): boolean { + return values.toReversed().toReversed().every((value, index) => value === values[index]); +} +``` | Domain | Semantics and defaults | | ---------------- | -------------------------------------------------------------------------------------------------- | @@ -57,73 +48,86 @@ diagnostics and artifacts. | `TupleDomain` | Non-empty ordered recursive domains | | `ArrayDomain` | Recursive element domain; defaults to length `0..10` | -`PropertyDomain` describes a set of allowed inputs. `JsConcreteValue` describes one concrete JavaScript value used as a -constant or returned sample; it is unrelated to JacoDB IR values. Its tagged encoding preserves `undefined`, -`null`, NaN, both infinities, and the raw IEEE-754 bits of finite numbers, including negative zero. Protocol -samples also use recursive tagged arrays so tuple and array values cross JSON without losing nested special -values. `ConstantDomain` still rejects composite values. +`JsConcreteValue` is a lossless tagged representation used for examples and counterexamples. It preserves +`undefined`, `null`, NaN, infinities, negative zero, and nested arrays. -## Manifest and capability are separate +## Execute a property -`PropertyManifest` is schema-versioned engine-neutral data. It contains property semantics and TypeScript -entry-point references, but no backend name, fast-check configuration, seed, replay path, shrink data, coverage, -or USVM expression. +`FastCheckBackend` accepts TypeScript source roots and loads `.ts` entry points directly. User projects do not +need a separate TypeScript compilation step or a path to the private adapter. -`ProjectionCapability` is a backend-and-version-specific report with `EXACT`, `APPROXIMATE`, or `UNSUPPORTED` -level and stable diagnostics. Recursive composition selects the least capable child. A concrete projection that -is supported while the selected USVM projection is unsupported is classified by the pipeline as `CONCRETE_ONLY`; -that classification is not stored in the manifest. +```kotlin +val backend = FastCheckBackend( + sourceRoots = listOf(Path.of("/workspace/packages/core/src")), +) -## Private fast-check adapter +val result = backend.run( + property = property, + configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 1_000, + timeoutMillis = 30_000, + ), +) +``` -`fast-check-adapter` is a private TypeScript module pinned to fast-check 4.9.0. Gradle compiles it with `tsc` into -an ignored `dist` directory before Kotlin integration tests run. The adapter recursively reconstructs real -`fc.Arbitrary` objects from common domain descriptors. Kotlin invokes the compiled one-shot `sample` operation -over one JSON request on stdin and one JSON response on stdout. The adapter does not discover properties, load -predicates, run campaigns, select USVM, or orchestrate the pipeline. +The defaults are 100 successful runs and a 60-second timeout. Configuration also supports replay paths and +positional explicit examples. `PropertyRunResult` contains the property ID, status, actual seed, replay path, +counterexample, run/skip/shrink counts, failure details, and elapsed time. -Both manifest and protocol versions start at `1`. Kotlin validates outgoing request sizes and verifies process -exit status, JSON shape, protocol version, request identity, sample shape, and typed backend diagnostics. +Predicate falsification and a timeout reported by fast-check are normal `FAILURE` results. Invalid input, +entry-point, process, and transport failures throw `PbtBackendException`. -## Extension rules +Synchronous entry points must return a boolean directly. Asynchronous entry points must return an awaitable that +resolves to a boolean. A false precondition is passed to fast-check as a skipped input. Generation, replay, explicit +examples, checking, and shrinking retain fast-check semantics. -- A new PBT backend consumes the common manifest and implements projection/capability reporting. Existing - `PropertyDefinition` instances and USVM code must not change for already-supported domains. -- A new common domain needs explicit Kotlin semantics and validation, serialization, a capability decision from - every backend, and conformance tests. -- A backend-specific extension must be namespaced and must be reported as unsupported by backends that do not - implement it. -- Backend-native arbitrary objects, arbitrary TypeScript closures, silent approximation, and backend defaults in - the common model are rejected extension mechanisms. +## Registries and CLI + +The CLI loads Kotlin property registries through `ServiceLoader`: + +```kotlin +class ExamplePropertyRegistryProvider : PropertyRegistryProvider { + override val registryId: String = "example" + + override fun load(): PropertyRegistry = PropertyRegistry( + listOf(arrayReverseTwiceProperty, anotherProperty), + ) +} +``` + +Register the provider in +`META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider` using its fully qualified class name. Put the +provider JAR on the application classpath, then run: + +```shell +java -cp '/opt/usvm-ts-pbt/lib/*:/workspace/example-properties.jar' \ + org.usvm.ts.pbt.cli.FastCheckCliKt \ + --source-root /workspace/packages/core/src \ + --registry example \ + --property array.reverse-twice \ + --seed 42 \ + --num-runs 1000 +``` + +Use `--help` for the complete option list. `--source-root` and `--registry` are repeatable. Without `--registry`, +all providers run in registry-ID order; without `--property`, all selected properties run in registry order. +Replay paths and explicit examples require exactly one selected property. + +The CLI writes a JSON array of results to stdout. Exit code `0` means every property succeeded, `1` means at least +one property failed, and `2` means a CLI, registry, validation, backend, or transport error. Exit-code-2 diagnostics +are written as one JSON object to stderr. ## Verification -Requires JDK 11, Node.js 18.18 or newer, npm, and the repository Gradle wrapper. The full Gradle check installs and -compiles the pinned private adapter, runs its compiled Node tests, runs Kotlin/Node protocol tests, and retains the -native `ts-frontend` baseline from #346. +Requires JDK 11, Node.js 18.18 or newer, npm, and the repository Gradle wrapper. ```shell npm ci --prefix usvm-ts-pbt/fast-check-adapter --ignore-scripts -npm run build --prefix usvm-ts-pbt/fast-check-adapter npm test --prefix usvm-ts-pbt/fast-check-adapter env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ - ./gradlew --no-daemon :usvm-ts-pbt:test - -env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ - ./gradlew --no-daemon :usvm-ts-pbt:clean :usvm-ts-pbt:check + ./gradlew --no-daemon :usvm-ts-pbt:check ``` -To substitute a local JacoDB checkout, add -`-PuseLocalJacodb=/absolute/path/to/jacodb` to the Gradle command. - -## Issue boundaries - -- #348 loads TypeScript entry points and executes Kotlin definitions through `fc.check`. -- #349 records backend-neutral per-property coverage. -- #350 maps entry points and coverage locations to EtsIR. -- #351 projects common domains and preconditions into USVM. -- #352 searches for property violations with USVM. -- #353 replays USVM witnesses and delegates shrinking to a capable PBT backend. -- #354 assembles the Kotlin-orchestrated end-to-end pipeline. -- #355–#357 build runtime hints, benchmarks, and evaluation on backend-identified artifacts. +To substitute a local JacoDB checkout, add `-PuseLocalJacodb=/absolute/path/to/jacodb` to the Gradle command. diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts index 56503aa6b..aa7bcd608 100644 --- a/usvm-ts-pbt/build.gradle.kts +++ b/usvm-ts-pbt/build.gradle.kts @@ -1,18 +1,35 @@ plugins { id("usvm.kotlin-conventions") kotlin("plugin.serialization") version Versions.kotlin + application } dependencies { implementation(project(":usvm-ts")) implementation(Libs.jacodb_ets) + implementation(Libs.clikt) implementation(Libs.kotlinx_serialization_json) testImplementation(Libs.logback) } val fastCheckAdapterDir = layout.projectDirectory.dir("fast-check-adapter") -val npmExecutable = if (System.getProperty("os.name").lowercase().contains("windows")) "npm.cmd" else "npm" +val fastCheckRuntimeProperty = "org.usvm.ts.pbt.fastcheck.runtime" +val hostOperatingSystem = System.getProperty("os.name").lowercase() +val hostPlatform = when { + hostOperatingSystem.contains("mac") -> "darwin" + hostOperatingSystem.contains("linux") -> "linux" + hostOperatingSystem.contains("windows") -> "win32" + else -> error("Unsupported fast-check runtime operating system: $hostOperatingSystem") +} +val hostArchitecture = when (val architecture = System.getProperty("os.arch").lowercase()) { + "aarch64", "arm64" -> "arm64" + "amd64", "x86_64" -> "x64" + "x86", "i386", "i686" -> "ia32" + else -> error("Unsupported fast-check runtime architecture: $architecture") +} +val fastCheckRuntimeClassifier = "$hostPlatform-$hostArchitecture" +val npmExecutable = if (hostPlatform == "win32") "npm.cmd" else "npm" val installFastCheckAdapter = tasks.register("installFastCheckAdapter") { workingDir(fastCheckAdapterDir) @@ -21,11 +38,24 @@ val installFastCheckAdapter = tasks.register("installFastCheckAdapter") { fastCheckAdapterDir.file("package.json"), fastCheckAdapterDir.file("package-lock.json"), ) + inputs.property("runtimeClassifier", fastCheckRuntimeClassifier) outputs.dir(fastCheckAdapterDir.dir("node_modules")) } -val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { +val verifyFastCheckAdapterRuntime = tasks.register("verifyFastCheckAdapterRuntime") { dependsOn(installFastCheckAdapter) + val nativeRuntime = fastCheckAdapterDir.dir("node_modules/@esbuild/$fastCheckRuntimeClassifier") + + inputs.dir(nativeRuntime) + doLast { + check(nativeRuntime.asFile.isDirectory) { + "Missing esbuild runtime for $fastCheckRuntimeClassifier at ${nativeRuntime.asFile}" + } + } +} + +val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { + dependsOn(verifyFastCheckAdapterRuntime) workingDir(fastCheckAdapterDir) commandLine(npmExecutable, "run", "build") inputs.files( @@ -38,6 +68,14 @@ val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { outputs.dir(fastCheckAdapterDir.dir("dist")) } +tasks.named("distZip") { + archiveClassifier.set(fastCheckRuntimeClassifier) +} + +tasks.named("distTar") { + archiveClassifier.set(fastCheckRuntimeClassifier) +} + val testFastCheckAdapter = tasks.register("testFastCheckAdapter") { dependsOn(buildFastCheckAdapter) workingDir(fastCheckAdapterDir) @@ -47,6 +85,7 @@ val testFastCheckAdapter = tasks.register("testFastCheckAdapter") { tasks.test { dependsOn(buildFastCheckAdapter) + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) } tasks.check { @@ -56,3 +95,31 @@ tasks.check { tasks.clean { delete(fastCheckAdapterDir.dir("dist")) } + +application { + mainClass = "org.usvm.ts.pbt.cli.FastCheckCliKt" + applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +tasks.named("run") { + systemProperty(fastCheckRuntimeProperty, fastCheckAdapterDir.asFile.absolutePath) +} + +distributions { + main { + contents { + into("lib/fast-check-adapter") { + from(fastCheckAdapterDir) + include("dist/src/**") + include("node_modules/**") + include("package.json") + } + } + } +} + +listOf("run", "startScripts", "installDist", "distZip", "distTar").forEach { taskName -> + tasks.named(taskName) { + dependsOn(buildFastCheckAdapter) + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/package-lock.json b/usvm-ts-pbt/fast-check-adapter/package-lock.json index c1e53b916..40e9135b5 100644 --- a/usvm-ts-pbt/fast-check-adapter/package-lock.json +++ b/usvm-ts-pbt/fast-check-adapter/package-lock.json @@ -8,7 +8,8 @@ "name": "@usvm/fast-check-adapter", "version": "0.1.0", "dependencies": { - "fast-check": "4.9.0" + "fast-check": "4.9.0", + "tsx": "4.23.12" }, "devDependencies": { "@types/node": "18.19.130", @@ -18,6 +19,422 @@ "node": ">=18.18.0" } }, + "node_modules/@esbuild/aix-ppc64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.28.2.tgz", + "integrity": "sha512-XExcO+dvLKvVtNTibSTBej1NCAbaGhWn9Ww1ZPx80qsahhPFe/8jgWP0IchNe0F3HwkU7n8ejhH8bjonqht8mQ==", + "cpu": [ + "ppc64" + ], + "license": "MIT", + "optional": true, + "os": [ + "aix" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.28.2.tgz", + "integrity": "sha512-kXXoiPVVGQcnIYGOeaovwOURpniDBpSq4A03qkQ+BMQqtGG6HYap3xne9C1O1yo4TR3qxlCX5IqqmX6fFo2Lqg==", + "cpu": [ + "arm" + ], + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.28.2.tgz", + "integrity": "sha512-5YfKeeI8qWfBZIX+u2xZC3Zlb3Os/gLS2sbEKM+I4ZOcsWmHS2WLysCcQZDAFRslDUU5Oiq44gf6PYN1vGwG5A==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.28.2.tgz", + "integrity": "sha512-O387ite7SzUyCcy3JQX4P4bLtEA7bLLkx+esve5JHnyYfNTxcVpXZo9jhdB0lTKN44gztELTdU7nS8Nr16Fs1Q==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.28.2.tgz", + "integrity": "sha512-n4KqkOQrraxHJcgjM1RvwbigfQKIKJVpM7xp+KsxiyUSrRdIXnt73VhrPAx0fV44hgfmIVKjxMN9J1t5jySVkw==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.28.2.tgz", + "integrity": "sha512-uq6suIWYP37qzGddBKPw5QEQPi6HiLGsO7UmkpfyaYNQ3D+rN6w6WfwH+nuqcGXWvawGwxOEroO4YGnFh95azw==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.28.2.tgz", + "integrity": "sha512-n+I0BTSRIoy+d6RPKnEVwql5UwBJolytvY4mAOIEJorKlqgPII8ix6slVVrfZ5Tnj7glIZvloylbB/EJPMWEXw==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.28.2.tgz", + "integrity": "sha512-78XJTJkvPs0kz2w61301PJjXl4g7q3JqiYMZ/M/yVI73EHBrCRTgkhu9oqG7vPqq+a/yadEW8aD+agKlk5xrmg==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.28.2.tgz", + "integrity": "sha512-XlDnu2q5yoqems+xay6wSAcg9DDD7K9RLKZEBOMZm3ckNpJBvOX20tSfby8KfrrhINDyv9V2YVZKY/SpoGJI8w==", + "cpu": [ + "arm" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.28.2.tgz", + "integrity": "sha512-pW4AC0P3it8c7do9MVM4p51FzHzdM/TZrerurgRcHJ2WTa1VQ1CIq18xncfpBJw4ojkiZZrKW2yIBWBP92j6Ug==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ia32": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.28.2.tgz", + "integrity": "sha512-CYbnj78HsIeA+DhgUKgFCfvNsTHFhMMrinUrMZpDXJXKN8T3XViTZ/+wtHeVxEWY8ewSzTFN+nRmSwO2tZaLUQ==", + "cpu": [ + "ia32" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-loong64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.28.2.tgz", + "integrity": "sha512-buwkd8nsph4R+ajRvw0qM5Hja/TXQow3ptzWO2EbG/cqcIkHloRrdlBtQlshyYGTNFvfkfJ5tpPLVkY4DtsPfQ==", + "cpu": [ + "loong64" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-mips64el": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.28.2.tgz", + "integrity": "sha512-ZVykbDyk7519VwiNb9Lcj9m8XM6v5V9uKPvrEMkkEedVewf+0itkhahp4HDpgERXhwLRpWFypsGbG/J8s0QjJA==", + "cpu": [ + "mips64el" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ppc64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.28.2.tgz", + "integrity": "sha512-CAXl+Dtd9UUuJd8pKKdwh6MLm3MUMiqMPmhZ3tTSXPqfyQ3vDl6R5hZdZ/kYojK4ofXtdfSv1tFq8XzWx3heNQ==", + "cpu": [ + "ppc64" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-riscv64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.28.2.tgz", + "integrity": "sha512-GeXCej4IQtU1B+QlDV8W/RRvbzI3O/Stss+/bCXv4lZls5WGRtu2a+3JkA3i4qIUlMXpcHebWpF8AkJhATowuA==", + "cpu": [ + "riscv64" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-s390x": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.28.2.tgz", + "integrity": "sha512-3H1weTYZPxt/WOhByszQZybS9w5lKzUn1FDMsgEChbHWQwHYQQRfBxgCcZvPhjHfKyJjIievvMmEUawJrdY9Dg==", + "cpu": [ + "s390x" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.28.2.tgz", + "integrity": "sha512-4xTZr1FUmSoQW4XIWmit3tzQrUTZM+N3P0XV8xROKYF50XfI7xeO90+1bZvNwxIufQ9hDQVRJH5YhgPVF8A/HQ==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-arm64/-/netbsd-arm64-0.28.2.tgz", + "integrity": "sha512-sSATRjPeDBg3pdgHoQfoYBob11Kk1FGa9lui5RIHZCoCkJa9QKlvl3/vKz2usCmYYjs7ymJR/2Nnsqe+Hjt5nw==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.28.2.tgz", + "integrity": "sha512-lqnzCV+mM0gIADaKihiCg6ifgfU2L3h5E33rNQBN1Y4MaVGnzryzmvvf7UHxprpQdE8hpqLolJ9Rl+SkIRDpyw==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-arm64/-/openbsd-arm64-0.28.2.tgz", + "integrity": "sha512-AL2qJILH7lNjrDmCQDvdxMfAUIv8KMNZOvrwAQ8i8//ntL9FflhOyMJ8OZSMBb8/AWXe3/5v5S20y3zCoZWKoQ==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.28.2.tgz", + "integrity": "sha512-QtiuPytchRyC4rwUKhexJdQKvDuZ6hWloi3igqPQNUJCS1/v9EiO3UTOXR6A3FoMo4fnAKbWJdqaIwhOzh8qEw==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openharmony-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/openharmony-arm64/-/openharmony-arm64-0.28.2.tgz", + "integrity": "sha512-WkhYDmpTjLvGlScA1rwjRUmhl4k8oXR3cIbtqWmELgU/dFeHHlEllxDvdWcNJV9rbzCexB5vz8gtNewWLgCT7Q==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "openharmony" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/sunos-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.28.2.tgz", + "integrity": "sha512-GPMSkTOtMnv2U2F8gxe4Io6qmVs+YKyp832Etqqxr0hFngmXQ3rzwytelm3GIn7T4VviRUlf3sOgBOiTdvaf7g==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "sunos" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-arm64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.28.2.tgz", + "integrity": "sha512-PIhhEkE9uPBleRBrQEJpUn7MBnibZzbGzYWPmY3x+YoVg/95zbjB4CxPPOQ8l5tYYM4mMaCthF8/1DIfBQQyWQ==", + "cpu": [ + "arm64" + ], + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-ia32": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.28.2.tgz", + "integrity": "sha512-YmJbfTlvU7Sdn9BB+4PRES4oB6pxgS37MAONj+hBr/cpXS1aBPKXxNnDbu+QCWPj0o9dgyxeq79g6c5P8KeuYA==", + "cpu": [ + "ia32" + ], + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-x64": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.28.2.tgz", + "integrity": "sha512-5ebpxr3nWMzrL/rnUI755Jkuee0bHL/Gq0WTF9lvcpv73wAp5eu8MfBUgWK9bhWvZjj7yX8etf/8tI8Ney695g==", + "cpu": [ + "x64" + ], + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, "node_modules/@types/node": { "version": "18.19.130", "resolved": "https://registry.npmjs.org/@types/node/-/node-18.19.130.tgz", @@ -28,6 +445,47 @@ "undici-types": "~5.26.4" } }, + "node_modules/esbuild": { + "version": "0.28.2", + "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.28.2.tgz", + "integrity": "sha512-HKVLS8dvII+xoKW9kmqxbRKrnWEXfJJr/FZhhJmiqIB0e053QNYFqOBouTMO/k5sID4MvCiUCvv8b9M4h32wIA==", + "hasInstallScript": true, + "license": "MIT", + "bin": { + "esbuild": "bin/esbuild" + }, + "engines": { + "node": ">=18" + }, + "optionalDependencies": { + "@esbuild/aix-ppc64": "0.28.2", + "@esbuild/android-arm": "0.28.2", + "@esbuild/android-arm64": "0.28.2", + "@esbuild/android-x64": "0.28.2", + "@esbuild/darwin-arm64": "0.28.2", + "@esbuild/darwin-x64": "0.28.2", + "@esbuild/freebsd-arm64": "0.28.2", + "@esbuild/freebsd-x64": "0.28.2", + "@esbuild/linux-arm": "0.28.2", + "@esbuild/linux-arm64": "0.28.2", + "@esbuild/linux-ia32": "0.28.2", + "@esbuild/linux-loong64": "0.28.2", + "@esbuild/linux-mips64el": "0.28.2", + "@esbuild/linux-ppc64": "0.28.2", + "@esbuild/linux-riscv64": "0.28.2", + "@esbuild/linux-s390x": "0.28.2", + "@esbuild/linux-x64": "0.28.2", + "@esbuild/netbsd-arm64": "0.28.2", + "@esbuild/netbsd-x64": "0.28.2", + "@esbuild/openbsd-arm64": "0.28.2", + "@esbuild/openbsd-x64": "0.28.2", + "@esbuild/openharmony-arm64": "0.28.2", + "@esbuild/sunos-x64": "0.28.2", + "@esbuild/win32-arm64": "0.28.2", + "@esbuild/win32-ia32": "0.28.2", + "@esbuild/win32-x64": "0.28.2" + } + }, "node_modules/fast-check": { "version": "4.9.0", "resolved": "https://registry.npmjs.org/fast-check/-/fast-check-4.9.0.tgz", @@ -50,6 +508,20 @@ "node": ">=12.17.0" } }, + "node_modules/fsevents": { + "version": "2.3.3", + "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.3.tgz", + "integrity": "sha512-5xoDfX+fL7faATnagmWPpbFtwh/R77WmMMqqHGS65C3vvB0YHrgF+B1YmZ3441tMj5n63k0212XNoJwzlhffQw==", + "hasInstallScript": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": "^8.16.0 || ^10.6.0 || >=11.0.0" + } + }, "node_modules/pure-rand": { "version": "8.4.2", "resolved": "https://registry.npmjs.org/pure-rand/-/pure-rand-8.4.2.tgz", @@ -66,6 +538,24 @@ ], "license": "MIT" }, + "node_modules/tsx": { + "version": "4.23.12", + "resolved": "https://registry.npmjs.org/tsx/-/tsx-4.23.12.tgz", + "integrity": "sha512-FDf4L4sYzKtzWYhU/Xm0AQFdTjdIxNo9ElTf2mxXM6k8YMHXzYUe4yODVaXP4V9uMFbVg8c0qyBccK2OOxb45Q==", + "license": "MIT", + "dependencies": { + "esbuild": "~0.28.0" + }, + "bin": { + "tsx": "dist/cli.mjs" + }, + "engines": { + "node": ">=18.0.0" + }, + "optionalDependencies": { + "fsevents": "~2.3.3" + } + }, "node_modules/typescript": { "version": "5.9.2", "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.2.tgz", diff --git a/usvm-ts-pbt/fast-check-adapter/package.json b/usvm-ts-pbt/fast-check-adapter/package.json index 96a9d74f7..c0c905634 100644 --- a/usvm-ts-pbt/fast-check-adapter/package.json +++ b/usvm-ts-pbt/fast-check-adapter/package.json @@ -9,10 +9,11 @@ "build": "tsc --project tsconfig.json", "pretest": "npm run build", "test": "npm run test:compiled", - "test:compiled": "node --test dist/test/js-value.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js" + "test:compiled": "node --test dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js" }, "dependencies": { - "fast-check": "4.9.0" + "fast-check": "4.9.0", + "tsx": "4.23.12" }, "devDependencies": { "@types/node": "18.19.130", diff --git a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts b/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts new file mode 100644 index 000000000..e1ab704f4 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts @@ -0,0 +1,58 @@ +export type AdapterDiagnosticKind = 'invalid-request' | 'entry-point'; + +export interface AdapterDiagnosticDescriptor { + readonly kind: AdapterDiagnosticKind; + readonly code: string; +} + +const invalidRequest = (code: string): AdapterDiagnosticDescriptor => ({ + kind: 'invalid-request', + code, +}); + +const entryPoint = (code: string): AdapterDiagnosticDescriptor => ({ + kind: 'entry-point', + code, +}); + +/** Stable diagnostics emitted by the Node adapter and consumed by Kotlin. */ +export const adapterDiagnostic = { + protocolJsonInvalid: invalidRequest('protocol.json.invalid'), + protocolRequestInvalid: invalidRequest('protocol.request.invalid'), + protocolSeedInvalid: invalidRequest('protocol.seed.invalid'), + protocolReplayPathInvalid: invalidRequest('protocol.replay-path.invalid'), + protocolExamplesInvalid: invalidRequest('protocol.examples.invalid'), + protocolExamplesArity: invalidRequest('protocol.examples.arity'), + protocolManifestInvalid: invalidRequest('protocol.manifest.invalid'), + protocolManifestInputInvalid: invalidRequest('protocol.manifest.input.invalid'), + protocolEntryPointInvalid: invalidRequest('protocol.entrypoint.invalid'), + sourceRootInvalid: invalidRequest('source-root.invalid'), + domainInvalid: invalidRequest('domain.invalid'), + domainKindUnknown: invalidRequest('domain.kind.unknown'), + domainOptionalNil: invalidRequest('domain.optional.nil'), + domainTupleEmpty: invalidRequest('domain.tuple.empty'), + domainNumberAllowNaNInvalid: invalidRequest('domain.number.allow-nan.invalid'), + domainNumberBoundNaN: invalidRequest('domain.number.bound.nan'), + domainNumberBounds: invalidRequest('domain.number.bounds'), + domainNumberNaNBounded: invalidRequest('domain.number.nan-bounded'), + domainNumberEmpty: invalidRequest('domain.number.empty'), + domainIntegerBounds: invalidRequest('domain.integer.bounds'), + domainLengthInvalid: invalidRequest('domain.length.invalid'), + jsValueInvalid: invalidRequest('js-value.invalid'), + jsValueBooleanInvalid: invalidRequest('js-value.boolean.invalid'), + jsValueStringInvalid: invalidRequest('js-value.string.invalid'), + jsValueArrayInvalid: invalidRequest('js-value.array.invalid'), + jsValueKindUnknown: invalidRequest('js-value.kind.unknown'), + jsValueTypeUnsupported: invalidRequest('js-value.type.unsupported'), + jsNumberInvalid: invalidRequest('js-number.invalid'), + jsNumberEncodingInvalid: invalidRequest('js-number.encoding.invalid'), + jsNumberKindUnknown: invalidRequest('js-number.kind.unknown'), + entryPointExportNotFound: entryPoint('entrypoint.export.not-found'), + entryPointExportNotFunction: entryPoint('entrypoint.export.not-function'), + entryPointModuleOutsideRoot: entryPoint('entrypoint.module.outside-root'), + entryPointModuleNotFound: entryPoint('entrypoint.module.not-found'), + entryPointModuleAmbiguous: entryPoint('entrypoint.module.ambiguous'), + entryPointModuleImportFailed: entryPoint('entrypoint.module.import-failed'), + entryPointExecutionKindMismatch: entryPoint('entrypoint.execution-kind.mismatch'), + entryPointResultInvalid: entryPoint('entrypoint.result.invalid'), +} as const; diff --git a/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts b/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts new file mode 100644 index 000000000..3cf32a460 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts @@ -0,0 +1,243 @@ +import { realpath, stat } from 'node:fs/promises'; +import path from 'node:path'; +import { pathToFileURL } from 'node:url'; +import { tsImport } from 'tsx/esm/api'; +import { adapterDiagnostic } from './diagnostics.js'; +import type { JsConcreteValue } from './js-value.js'; +import { ProtocolError, protocolError } from './js-value.js'; + +export type ExecutionKind = 'sync' | 'async'; + +export interface TypeScriptEntryPointReference { + module: string; + exportName: string; + executionKind: ExecutionKind; +} + +export interface LoadedEntryPoint { + executionKind: ExecutionKind; + invoke(args: JsConcreteValue[]): boolean | Promise; +} + +type EntryPointFunction = (...args: JsConcreteValue[]) => unknown; + +export async function loadEntryPoint( + reference: TypeScriptEntryPointReference, + sourceRoots: string[], + referencePath: string, +): Promise { + const modulePath = await resolveModule(reference.module, sourceRoots, referencePath); + const moduleNamespace = await importTypeScriptModule(modulePath, referencePath); + + if (!(reference.exportName in moduleNamespace)) { + throw protocolError( + adapterDiagnostic.entryPointExportNotFound, + `TypeScript module ${reference.module} does not export ${reference.exportName}`, + `${referencePath}.exportName`, + ); + } + + const exportedValue = moduleNamespace[reference.exportName]; + if (typeof exportedValue !== 'function') { + throw protocolError( + adapterDiagnostic.entryPointExportNotFunction, + `TypeScript export ${reference.exportName} is not a function`, + `${referencePath}.exportName`, + ); + } + + const entryPoint = exportedValue as EntryPointFunction; + + return { + executionKind: reference.executionKind, + invoke: buildInvocation(entryPoint, reference.executionKind, referencePath), + }; +} + +async function resolveModule( + module: string, + sourceRoots: string[], + referencePath: string, +): Promise { + if (sourceRoots.length === 0) { + throw protocolError( + adapterDiagnostic.sourceRootInvalid, + 'At least one TypeScript source root is required', + 'sourceRoots', + ); + } + + const matches: string[] = []; + for (let index = 0; index < sourceRoots.length; index += 1) { + const sourceRoot = sourceRoots[index]; + + if (sourceRoot === undefined || !path.isAbsolute(sourceRoot)) { + throw protocolError( + adapterDiagnostic.sourceRootInvalid, + 'TypeScript source roots must be absolute paths', + `sourceRoots[${index}]`, + ); + } + + const realSourceRoot = await requireDirectory(sourceRoot, index); + const candidate = path.resolve(realSourceRoot, module); + + if (!isWithin(candidate, realSourceRoot)) { + throw protocolError( + adapterDiagnostic.entryPointModuleOutsideRoot, + `TypeScript module ${module} escapes source root ${realSourceRoot}`, + `${referencePath}.module`, + ); + } + + const realCandidate = await realpathOrUndefined(candidate); + if (realCandidate === undefined) continue; + + if (!isWithin(realCandidate, realSourceRoot)) { + throw protocolError( + adapterDiagnostic.entryPointModuleOutsideRoot, + `TypeScript module ${module} resolves outside source root ${realSourceRoot}`, + `${referencePath}.module`, + ); + } + + const candidateStat = await stat(realCandidate); + if (candidateStat.isFile()) matches.push(realCandidate); + } + + if (matches.length === 0) { + throw protocolError( + adapterDiagnostic.entryPointModuleNotFound, + `TypeScript module ${module} was not found in any source root`, + `${referencePath}.module`, + ); + } + + if (matches.length > 1) { + throw protocolError( + adapterDiagnostic.entryPointModuleAmbiguous, + `TypeScript module ${module} exists in multiple source roots`, + `${referencePath}.module`, + ); + } + + return matches[0] as string; +} + +async function requireDirectory(sourceRoot: string, index: number): Promise { + let realSourceRoot: string; + try { + realSourceRoot = await realpath(sourceRoot); + } catch { + throw protocolError( + adapterDiagnostic.sourceRootInvalid, + `TypeScript source root does not exist: ${sourceRoot}`, + `sourceRoots[${index}]`, + ); + } + + if (!(await stat(realSourceRoot)).isDirectory()) { + throw protocolError( + adapterDiagnostic.sourceRootInvalid, + `TypeScript source root is not a directory: ${sourceRoot}`, + `sourceRoots[${index}]`, + ); + } + + return realSourceRoot; +} + +async function realpathOrUndefined(candidate: string): Promise { + try { + return await realpath(candidate); + } catch (error: unknown) { + if (isNodeError(error) && (error.code === 'ENOENT' || error.code === 'ENOTDIR')) return undefined; + + throw error; + } +} + +async function importTypeScriptModule( + modulePath: string, + referencePath: string, +): Promise> { + try { + return await tsImport(pathToFileURL(modulePath).href, import.meta.url) as Record; + } catch (error: unknown) { + if (error instanceof ProtocolError) throw error; + + const message = error instanceof Error ? error.message : String(error); + + throw protocolError( + adapterDiagnostic.entryPointModuleImportFailed, + `Failed to import TypeScript module: ${message}`, + `${referencePath}.module`, + ); + } +} + +function buildInvocation( + entryPoint: EntryPointFunction, + executionKind: ExecutionKind, + referencePath: string, +): (args: JsConcreteValue[]) => boolean | Promise { + if (executionKind === 'sync') { + return (args: JsConcreteValue[]): boolean => { + const result = entryPoint(...args); + + if (isThenable(result)) { + void Promise.resolve(result).catch(() => undefined); + throw protocolError( + adapterDiagnostic.entryPointExecutionKindMismatch, + 'A synchronous entry point returned an awaitable value', + `${referencePath}.executionKind`, + ); + } + + return requireBoolean(result, referencePath); + }; + } + + return async (args: JsConcreteValue[]): Promise => { + const result = entryPoint(...args); + + if (!isThenable(result)) { + throw protocolError( + adapterDiagnostic.entryPointExecutionKindMismatch, + 'An asynchronous entry point returned a direct value', + `${referencePath}.executionKind`, + ); + } + + return requireBoolean(await result, referencePath); + }; +} + +function requireBoolean(result: unknown, referencePath: string): boolean { + if (typeof result !== 'boolean') { + throw protocolError( + adapterDiagnostic.entryPointResultInvalid, + 'A property entry point must return a boolean', + `${referencePath}.result`, + ); + } + + return result; +} + +function isThenable(value: unknown): value is PromiseLike { + if (value === null) return false; + if (typeof value !== 'object' && typeof value !== 'function') return false; + + return typeof (value as { then?: unknown }).then === 'function'; +} + +function isWithin(candidate: string, root: string): boolean { + const relative = path.relative(root, candidate); + + return relative === '' || (!relative.startsWith(`..${path.sep}`) && relative !== '..' && !path.isAbsolute(relative)); +} + +function isNodeError(error: unknown): error is NodeJS.ErrnoException { + return error instanceof Error && 'code' in error; +} diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts new file mode 100644 index 000000000..a21ea2379 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -0,0 +1,391 @@ +import { performance } from 'node:perf_hooks'; +import fc from 'fast-check'; +import type { Parameters, RunDetails } from 'fast-check'; +import { + adapterDiagnostic, + type AdapterDiagnosticDescriptor, +} from './diagnostics.js'; +import { + type ExecutionKind, + loadEntryPoint, + type LoadedEntryPoint, + type TypeScriptEntryPointReference, +} from './entry-point.js'; +import { + decodeJsValue, + encodeJsValue, + type JsConcreteValue, + ProtocolError, + protocolError, + type TaggedJsValue, +} from './js-value.js'; +import { projectDomain } from './project-domain.js'; + +export interface PropertyManifestInput { + name: string; + domain: unknown; +} + +export interface PropertyManifestWire { + propertyId: string; + inputs: PropertyManifestInput[]; + predicate: TypeScriptEntryPointReference; + precondition?: TypeScriptEntryPointReference; +} + +export interface FastCheckExecutionRequest { + manifest: PropertyManifestWire; + sourceRoots: string[]; + seed?: number; + replayPath?: string; + numRuns: number; + timeoutMillis: number; + examples: TaggedJsValue[][]; +} + +export interface FastCheckFailureDetails { + kind: 'property' | 'timeout'; + errorName: string; + message: string; +} + +export interface FastCheckRunResult { + propertyId: string; + status: 'success' | 'failure'; + seed: number; + replayPath: string | null; + counterexample: TaggedJsValue[] | null; + numRuns: number; + numSkips: number; + numShrinks: number; + failure: FastCheckFailureDetails | null; + executionTimeMillis: number; +} + +export interface FastCheckExecutionSuccess { + status: 'ok'; + result: FastCheckRunResult; +} + +export async function executeProperty(requestValue: unknown): Promise { + const request = validateRequest(requestValue); + const startedAt = performance.now(); + + const predicate = await loadEntryPoint(request.manifest.predicate, request.sourceRoots, 'manifest.predicate'); + const precondition = request.manifest.precondition === undefined + ? undefined + : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition'); + + const arbitrary = fc.tuple( + ...request.manifest.inputs.map((input, index) => + projectDomain(input.domain, `manifest.inputs[${index}].domain`)), + ); + const property = buildProperty(arbitrary, predicate, precondition); + const parameters = buildParameters(request); + + const details = await Promise.resolve(fc.check(property, parameters)); + + if (details.errorInstance instanceof ProtocolError) throw details.errorInstance; + + return { + status: 'ok', + result: toRunResult( + request.manifest.propertyId, + details, + Math.max(0, Math.round(performance.now() - startedAt)), + ), + }; +} + +function buildProperty( + arbitrary: fc.Arbitrary, + predicate: LoadedEntryPoint, + precondition: LoadedEntryPoint | undefined, +): fc.IProperty<[unknown[]]> | fc.IAsyncProperty<[unknown[]]> { + const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async'; + + if (asynchronous) { + return fc.asyncProperty(arbitrary, async (values: unknown[]): Promise => { + const argumentsList = values as JsConcreteValue[]; + + if (precondition !== undefined && !(await precondition.invoke(argumentsList))) fc.pre(false); + + return await predicate.invoke(argumentsList); + }); + } + + return fc.property(arbitrary, (values: unknown[]): boolean => { + const argumentsList = values as JsConcreteValue[]; + + if (precondition !== undefined && !precondition.invoke(argumentsList)) fc.pre(false); + + return predicate.invoke(argumentsList) as boolean; + }); +} + +function buildParameters(request: FastCheckExecutionRequest): Parameters<[unknown[]]> { + const decodedExamples = request.examples.map((example, exampleIndex) => { + if (example.length !== request.manifest.inputs.length) { + throw protocolError( + adapterDiagnostic.protocolExamplesArity, + `Explicit example ${exampleIndex} has ${example.length} values, expected ${request.manifest.inputs.length}`, + `examples[${exampleIndex}]`, + ); + } + + const values = example.map((value, valueIndex) => + decodeJsValue(value, `examples[${exampleIndex}][${valueIndex}]`)); + + return [values] as [unknown[]]; + }); + + const parameters: Parameters<[unknown[]]> = { + numRuns: request.numRuns, + timeout: request.timeoutMillis, + interruptAfterTimeLimit: request.timeoutMillis, + markInterruptAsFailure: true, + examples: decodedExamples, + }; + + if (request.seed !== undefined) parameters.seed = request.seed; + if (request.replayPath !== undefined) parameters.path = request.replayPath; + + return parameters; +} + +function toRunResult( + propertyId: string, + details: RunDetails<[unknown[]]>, + executionTimeMillis: number, +): FastCheckRunResult { + const counterexampleValues = details.counterexample?.[0]; + const counterexample = counterexampleValues === undefined + ? null + : counterexampleValues.map(encodeJsValue); + const failure = details.failed ? failureDetails(details) : null; + + return { + propertyId, + status: details.failed ? 'failure' : 'success', + seed: details.seed, + replayPath: details.counterexamplePath, + counterexample, + numRuns: details.numRuns, + numSkips: details.numSkips, + numShrinks: details.numShrinks, + failure, + executionTimeMillis, + }; +} + +function failureDetails(details: RunDetails<[unknown[]]>): FastCheckFailureDetails { + const error = details.errorInstance; + const timeout = (details.interrupted && details.counterexample === null) || isFastCheckTimeout(error); + + if (error instanceof Error) { + return { + kind: timeout ? 'timeout' : 'property', + errorName: error.name || 'Error', + message: error.message || 'Property execution failed', + }; + } + + if (timeout) { + return { + kind: 'timeout', + errorName: 'TimeoutError', + message: 'Property execution exceeded the configured timeout', + }; + } + + return { + kind: 'property', + errorName: 'PropertyFailure', + message: details.counterexample === null + ? 'Property could not satisfy its precondition within the skip limit' + : 'Property predicate returned false', + }; +} + +function isFastCheckTimeout(error: unknown): boolean { + return error instanceof Error && error.message.startsWith('Property timeout:'); +} + +function validateRequest(value: unknown): FastCheckExecutionRequest { + const request = requireRecord( + value, + adapterDiagnostic.protocolRequestInvalid, + 'Request must be a JSON object', + 'request', + ); + + const validSourceRoots = Array.isArray(request.sourceRoots) + && request.sourceRoots.length > 0 + && request.sourceRoots.every((root) => typeof root === 'string'); + + const validRunCount = Number.isInteger(request.numRuns) + && (request.numRuns as number) >= 1; + + const validTimeout = Number.isInteger(request.timeoutMillis) + && (request.timeoutMillis as number) >= 1 + && (request.timeoutMillis as number) <= MAX_TIMER_DELAY_MILLIS; + + const validExamples = Array.isArray(request.examples); + + if (!validSourceRoots || !validRunCount || !validTimeout || !validExamples) { + throw protocolError( + adapterDiagnostic.protocolRequestInvalid, + 'Source roots, run count, timeout, or examples are invalid', + 'request', + ); + } + + if (request.seed !== undefined && !isSignedInt(request.seed)) { + throw protocolError( + adapterDiagnostic.protocolSeedInvalid, + 'Seed must be a signed 32-bit integer', + 'seed', + ); + } + + const invalidReplayPath = request.replayPath !== undefined && typeof request.replayPath !== 'string'; + if (invalidReplayPath) { + throw protocolError( + adapterDiagnostic.protocolReplayPathInvalid, + 'Replay path is invalid', + 'replayPath', + ); + } + + const manifest = validateManifest(request.manifest); + const rawExamples = request.examples as unknown[]; + const examples = rawExamples.map((example: unknown, index: number) => { + if (!Array.isArray(example)) { + throw protocolError( + adapterDiagnostic.protocolExamplesInvalid, + 'Each explicit example must be an array', + `examples[${index}]`, + ); + } + + return example as TaggedJsValue[]; + }); + + const validated: FastCheckExecutionRequest = { + manifest, + sourceRoots: request.sourceRoots as string[], + numRuns: request.numRuns as number, + timeoutMillis: request.timeoutMillis as number, + examples, + }; + + if (request.seed !== undefined) validated.seed = request.seed as number; + if (request.replayPath !== undefined) validated.replayPath = request.replayPath as string; + + return validated; +} + +function validateManifest(value: unknown): PropertyManifestWire { + const manifest = requireRecord( + value, + adapterDiagnostic.protocolManifestInvalid, + 'Manifest must be an object', + 'manifest', + ); + + const valid = typeof manifest.propertyId === 'string' + && manifest.propertyId.length > 0 + && Array.isArray(manifest.inputs) + && manifest.inputs.length > 0; + if (!valid) { + throw protocolError( + adapterDiagnostic.protocolManifestInvalid, + 'Manifest identity or inputs are invalid', + 'manifest', + ); + } + + const rawInputs = manifest.inputs as unknown[]; + const inputs = rawInputs.map((value: unknown, index: number): PropertyManifestInput => { + const input = requireRecord( + value, + adapterDiagnostic.protocolManifestInputInvalid, + 'Property input must be an object', + `manifest.inputs[${index}]`, + ); + + if (typeof input.name !== 'string' || !('domain' in input)) { + throw protocolError( + adapterDiagnostic.protocolManifestInputInvalid, + 'Property input requires a name and domain', + `manifest.inputs[${index}]`, + ); + } + + return { name: input.name, domain: input.domain }; + }); + + const validated: PropertyManifestWire = { + propertyId: manifest.propertyId as string, + inputs, + predicate: validateEntryPoint(manifest.predicate, 'manifest.predicate'), + }; + + if (manifest.precondition !== undefined) { + validated.precondition = validateEntryPoint(manifest.precondition, 'manifest.precondition'); + } + + return validated; +} + +function validateEntryPoint(value: unknown, entryPath: string): TypeScriptEntryPointReference { + const entryPoint = requireRecord( + value, + adapterDiagnostic.protocolEntryPointInvalid, + 'Entry point must be an object', + entryPath, + ); + + const executionKind = entryPoint.executionKind; + const valid = typeof entryPoint.module === 'string' + && entryPoint.module.length > 0 + && typeof entryPoint.exportName === 'string' + && entryPoint.exportName.length > 0 + && (executionKind === 'sync' || executionKind === 'async'); + if (!valid) { + throw protocolError( + adapterDiagnostic.protocolEntryPointInvalid, + 'Entry point reference is invalid', + entryPath, + ); + } + + return { + module: entryPoint.module as string, + exportName: entryPoint.exportName as string, + executionKind: executionKind as ExecutionKind, + }; +} + +function requireRecord( + value: unknown, + diagnostic: AdapterDiagnosticDescriptor, + message: string, + path: string, +): Record { + if (value === null || typeof value !== 'object' || Array.isArray(value)) { + throw protocolError(diagnostic, message, path); + } + + return value as Record; +} + +function isSignedInt(value: unknown): value is number { + return typeof value === 'number' + && Number.isInteger(value) + && value >= -0x80000000 + && value <= 0x7fffffff; +} + +// Node timers use signed 32-bit millisecond delays; larger values are clamped to one millisecond. +const MAX_TIMER_DELAY_MILLIS = 2 ** 31 - 1; diff --git a/usvm-ts-pbt/fast-check-adapter/src/execution-cli.ts b/usvm-ts-pbt/fast-check-adapter/src/execution-cli.ts new file mode 100644 index 000000000..59caaf711 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/execution-cli.ts @@ -0,0 +1,73 @@ +import { adapterDiagnostic } from './diagnostics.js'; +import { executeProperty, type FastCheckExecutionSuccess } from './execute-property.js'; +import { ProtocolError, protocolError } from './js-value.js'; +import type { ProtocolDiagnostic } from './js-value.js'; + +interface FastCheckExecutionFailure { + status: 'error'; + diagnostics: ProtocolDiagnostic[]; +} + +const writeProtocolOutput = process.stdout.write.bind(process.stdout) as typeof process.stdout.write; +process.stdout.write = process.stderr.write.bind(process.stderr) as typeof process.stdout.write; + +let response: FastCheckExecutionSuccess | FastCheckExecutionFailure; +try { + const request = parseRequest(await readStdin()); + + response = await executeProperty(request); +} catch (error: unknown) { + if (!(error instanceof ProtocolError)) throw error; + + response = protocolErrorResponse(error); +} + +await writeResponse(response); +process.exit(0); + +async function readStdin(): Promise { + process.stdin.setEncoding('utf8'); + + let input = ''; + for await (const chunk of process.stdin) input += chunk; + + return input; +} + +function parseRequest(input: string): unknown { + try { + return JSON.parse(input) as unknown; + } catch { + throw protocolError( + adapterDiagnostic.protocolJsonInvalid, + 'Standard input is not valid JSON', + 'request', + ); + } +} + +function protocolErrorResponse(error: ProtocolError): FastCheckExecutionFailure { + return { + status: 'error', + diagnostics: [{ + kind: error.kind, + code: error.code, + message: error.diagnosticMessage, + path: error.path, + }], + }; +} + +async function writeResponse(response: FastCheckExecutionSuccess | FastCheckExecutionFailure): Promise { + const document = `${JSON.stringify(response)}\n`; + + await new Promise((resolve, reject) => { + writeProtocolOutput(document, (error?: Error | null) => { + if (error !== undefined && error !== null) { + reject(error); + } else { + resolve(); + } + }); + }); +} diff --git a/usvm-ts-pbt/fast-check-adapter/src/js-value.ts b/usvm-ts-pbt/fast-check-adapter/src/js-value.ts index 781ad8ae6..39d3a400b 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/js-value.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/js-value.ts @@ -1,3 +1,9 @@ +import { + adapterDiagnostic, + type AdapterDiagnosticDescriptor, + type AdapterDiagnosticKind, +} from './diagnostics.js'; + export type JsConcreteValue = | undefined | null @@ -20,45 +26,75 @@ export type TaggedJsValue = | ({ kind: 'number' } & TaggedJsNumber) | { kind: 'array'; elements: TaggedJsValue[] }; +export interface ProtocolDiagnostic { + kind: AdapterDiagnosticKind; + code: string; + message: string; + path: string; +} + export class ProtocolError extends Error { constructor( - readonly code: string, + diagnostic: AdapterDiagnosticDescriptor, readonly diagnosticMessage: string, readonly path: string, ) { - super(`${code}: ${diagnosticMessage}`); + super(`${diagnostic.code}: ${diagnosticMessage}`); this.name = 'ProtocolError'; + this.kind = diagnostic.kind; + this.code = diagnostic.code; } + + readonly kind: AdapterDiagnosticKind; + readonly code: string; } export function decodeJsValue(value: unknown, path = 'value'): JsConcreteValue { - requireObject(value, 'js-value.invalid', 'Tagged JavaScript value must be an object', path); + requireObject(value, adapterDiagnostic.jsValueInvalid, 'Tagged JavaScript value must be an object', path); + switch (value.kind) { case 'undefined': return undefined; + case 'null': return null; + case 'boolean': if (typeof value.value !== 'boolean') { - throw protocolError('js-value.boolean.invalid', 'Boolean value must contain a boolean', path); + throw protocolError( + adapterDiagnostic.jsValueBooleanInvalid, + 'Boolean value must contain a boolean', + path, + ); } + return value.value; + case 'string': if (typeof value.value !== 'string') { - throw protocolError('js-value.string.invalid', 'String value must contain a string', path); + throw protocolError( + adapterDiagnostic.jsValueStringInvalid, + 'String value must contain a string', + path, + ); } + return value.value; + case 'number': return decodeJsNumber(value, path); + case 'array': if (!Array.isArray(value.elements)) { - throw protocolError('js-value.array.invalid', 'Array value must contain elements', path); + throw protocolError(adapterDiagnostic.jsValueArrayInvalid, 'Array value must contain elements', path); } + return value.elements.map((element: unknown, index: number) => decodeJsValue(element, `${path}.elements[${index}]`)); + default: throw protocolError( - 'js-value.kind.unknown', + adapterDiagnostic.jsValueKindUnknown, `Unknown JavaScript value kind: ${String(value.kind)}`, path, ); @@ -72,37 +108,52 @@ export function encodeJsValue(value: unknown): TaggedJsValue { if (typeof value === 'string') return { kind: 'string', value }; if (typeof value === 'number') return { kind: 'number', ...encodeJsNumber(value) }; if (Array.isArray(value)) return { kind: 'array', elements: value.map(encodeJsValue) }; + throw protocolError( - 'js-value.type.unsupported', + adapterDiagnostic.jsValueTypeUnsupported, `Unsupported JavaScript value type: ${typeof value}`, 'value', ); } export function decodeJsNumber(taggedNumber: unknown, path = 'number'): number { - requireObject(taggedNumber, 'js-number.invalid', 'Tagged JavaScript number must be an object', path); + requireObject( + taggedNumber, + adapterDiagnostic.jsNumberInvalid, + 'Tagged JavaScript number must be an object', + path, + ); + switch (taggedNumber.value) { case 'finite': if (typeof taggedNumber.bits !== 'string' || !/^[0-9a-f]{16}$/.test(taggedNumber.bits)) { throw protocolError( - 'js-number.encoding.invalid', + adapterDiagnostic.jsNumberEncodingInvalid, 'Finite JavaScript numbers require sixteen lowercase hexadecimal digits', path, ); } + return bitsToDouble(taggedNumber.bits); + case 'nan': requireNoBits(taggedNumber, path); + return Number.NaN; + case 'positive-infinity': requireNoBits(taggedNumber, path); + return Number.POSITIVE_INFINITY; + case 'negative-infinity': requireNoBits(taggedNumber, path); + return Number.NEGATIVE_INFINITY; + default: throw protocolError( - 'js-number.kind.unknown', + adapterDiagnostic.jsNumberKindUnknown, `Unknown JavaScript number kind: ${String(taggedNumber.value)}`, path, ); @@ -113,40 +164,53 @@ export function encodeJsNumber(value: number): TaggedJsNumber { if (Number.isNaN(value)) return { value: 'nan' }; if (value === Number.POSITIVE_INFINITY) return { value: 'positive-infinity' }; if (value === Number.NEGATIVE_INFINITY) return { value: 'negative-infinity' }; + return { value: 'finite', bits: doubleToBits(value) }; } -export function protocolError(code: string, message: string, path: string): ProtocolError { - return new ProtocolError(code, message, path); +export function protocolError( + diagnostic: AdapterDiagnosticDescriptor, + message: string, + path: string, +): ProtocolError { + return new ProtocolError(diagnostic, message, path); } function bitsToDouble(bits: string): number { const buffer = new ArrayBuffer(8); const view = new DataView(buffer); + view.setBigUint64(0, BigInt(`0x${bits}`), false); + return view.getFloat64(0, false); } function doubleToBits(value: number): string { const buffer = new ArrayBuffer(8); const view = new DataView(buffer); + view.setFloat64(0, value, false); + return view.getBigUint64(0, false).toString(16).padStart(16, '0'); } function requireNoBits(taggedNumber: Record, path: string): void { if (taggedNumber.bits !== undefined) { - throw protocolError('js-number.encoding.invalid', 'Non-finite JavaScript numbers must not contain bits', path); + throw protocolError( + adapterDiagnostic.jsNumberEncodingInvalid, + 'Non-finite JavaScript numbers must not contain bits', + path, + ); } } function requireObject( value: unknown, - code: string, + diagnostic: AdapterDiagnosticDescriptor, message: string, path: string, ): asserts value is Record { if (value === null || typeof value !== 'object' || Array.isArray(value)) { - throw protocolError(code, message, path); + throw protocolError(diagnostic, message, path); } } diff --git a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts index 954ab21f1..0e421c764 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts @@ -1,4 +1,5 @@ import fc from 'fast-check'; +import { adapterDiagnostic } from './diagnostics.js'; import { decodeJsNumber, decodeJsValue, @@ -6,9 +7,6 @@ import { protocolError, } from './js-value.js'; -export const FAST_CHECK_BACKEND_ID = 'fast-check'; -export const FAST_CHECK_BACKEND_VERSION = '4.9.0'; - export interface ProjectionDiagnostic { code: string; message: string; @@ -16,8 +14,6 @@ export interface ProjectionDiagnostic { } export interface ProjectionCapability { - backendId: string; - backendVersion: string; level: 'exact' | 'unsupported'; diagnostics: ProjectionDiagnostic[]; } @@ -26,45 +22,64 @@ type DomainRecord = Record; export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary { requireDomainObject(domain, path); + switch (domain.kind) { case 'boolean': return fc.boolean(); + case 'integer': validateIntegerDomain(domain, path); + return fc.integer({ min: domain.min, max: domain.max }); + case 'number': return projectNumber(domain, path); + case 'string': validateLengths(domain, path); + return fc.array(fc.integer({ min: 0, max: 0xffff }), { minLength: domain.minLength, maxLength: domain.maxLength, }).map((units) => units.map((unit) => String.fromCharCode(unit)).join('')); + case 'constant': return fc.constant(decodeJsValue(domain.value, `${path}.value`)); + case 'optional': { const nil = decodeJsValue(domain.nil, `${path}.nil`); + if (nil !== undefined && nil !== null) { - throw protocolError('domain.optional.nil', 'Optional nil must be null or undefined', `${path}.nil`); + throw protocolError( + adapterDiagnostic.domainOptionalNil, + 'Optional nil must be null or undefined', + `${path}.nil`, + ); } + return fc.option(projectDomain(domain.value, `${path}.value`), { nil }); } + case 'tuple': if (!Array.isArray(domain.elements) || domain.elements.length === 0) { - throw protocolError('domain.tuple.empty', 'Tuple domain must contain elements', path); + throw protocolError(adapterDiagnostic.domainTupleEmpty, 'Tuple domain must contain elements', path); } + return fc.tuple(...domain.elements.map( (element: unknown, index: number) => projectDomain(element, `${path}.elements[${index}]`), )); + case 'array': validateLengths(domain, path); + return fc.array(projectDomain(domain.element, `${path}.element`), { minLength: domain.minLength, maxLength: domain.maxLength, }); + default: throw protocolError( - 'domain.kind.unknown', + adapterDiagnostic.domainKindUnknown, `Unknown property domain kind: ${String(domain.kind)}`, path, ); @@ -74,17 +89,15 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary { if (typeof domain.allowNaN !== 'boolean') { - throw protocolError('domain.number.allow-nan.invalid', 'allowNaN must be a boolean', `${path}.allowNaN`); + throw protocolError( + adapterDiagnostic.domainNumberAllowNaNInvalid, + 'allowNaN must be a boolean', + `${path}.allowNaN`, + ); } + const min = decodeJsNumber(domain.min, `${path}.min`); const max = decodeJsNumber(domain.max, `${path}.max`); + if (Number.isNaN(min) || Number.isNaN(max)) { - throw protocolError('domain.number.bound.nan', 'Number bounds must not be NaN', path); + throw protocolError(adapterDiagnostic.domainNumberBoundNaN, 'Number bounds must not be NaN', path); } + if (min > max) { - throw protocolError('domain.number.bounds', 'Number minimum exceeds maximum', path); + throw protocolError(adapterDiagnostic.domainNumberBounds, 'Number minimum exceeds maximum', path); } + const bounded = min !== Number.NEGATIVE_INFINITY || max !== Number.POSITIVE_INFINITY; + if (bounded && domain.allowNaN) { - throw protocolError('domain.number.nan-bounded', 'Bounded number domains must exclude NaN', `${path}.allowNaN`); + throw protocolError( + adapterDiagnostic.domainNumberNaNBounded, + 'Bounded number domains must exclude NaN', + `${path}.allowNaN`, + ); } const finiteMin = min === Number.NEGATIVE_INFINITY ? -Number.MAX_VALUE : min; const finiteMax = max === Number.POSITIVE_INFINITY ? Number.MAX_VALUE : max; const arbitraries: fc.Arbitrary[] = []; + if (finiteMin <= finiteMax) { arbitraries.push(fc.double({ min: finiteMin, @@ -123,6 +150,7 @@ function projectNumber(domain: DomainRecord, path: string): fc.Arbitrary noDefaultInfinity: true, })); } + if (domain.allowNaN) arbitraries.push(fc.constant(Number.NaN)); if (min === Number.NEGATIVE_INFINITY) arbitraries.push(fc.constant(Number.NEGATIVE_INFINITY)); if (max === Number.POSITIVE_INFINITY) arbitraries.push(fc.constant(Number.POSITIVE_INFINITY)); @@ -130,8 +158,9 @@ function projectNumber(domain: DomainRecord, path: string): fc.Arbitrary const [first, ...rest] = arbitraries; if (first === undefined) { - throw protocolError('domain.number.empty', 'Number domain does not contain any values', path); + throw protocolError(adapterDiagnostic.domainNumberEmpty, 'Number domain does not contain any values', path); } + return rest.length === 0 ? first : fc.oneof(first, ...rest); } @@ -146,8 +175,13 @@ function validateIntegerDomain( && domain.min >= -0x80000000 && domain.max <= 0x7fffffff && domain.min <= domain.max; + if (!valid) { - throw protocolError('domain.integer.bounds', 'Integer bounds must be an inclusive signed 32-bit range', path); + throw protocolError( + adapterDiagnostic.domainIntegerBounds, + 'Integer bounds must be an inclusive signed 32-bit range', + path, + ); } } @@ -161,13 +195,14 @@ function validateLengths( && Number.isInteger(domain.maxLength) && domain.minLength >= 0 && domain.minLength <= domain.maxLength; + if (!valid) { - throw protocolError('domain.length.invalid', 'Domain length bounds are invalid', path); + throw protocolError(adapterDiagnostic.domainLengthInvalid, 'Domain length bounds are invalid', path); } } function requireDomainObject(domain: unknown, path: string): asserts domain is DomainRecord { if (domain === null || typeof domain !== 'object' || Array.isArray(domain)) { - throw protocolError('domain.invalid', 'Property domain must be an object', path); + throw protocolError(adapterDiagnostic.domainInvalid, 'Property domain must be an object', path); } } diff --git a/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts b/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts index 06e8af735..d38a1bd53 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts @@ -1,143 +1,127 @@ import fc from 'fast-check'; +import { adapterDiagnostic } from './diagnostics.js'; import { encodeJsValue, ProtocolError, protocolError, } from './js-value.js'; -import type { TaggedJsValue } from './js-value.js'; +import type { ProtocolDiagnostic, TaggedJsValue } from './js-value.js'; import { projectDomain } from './project-domain.js'; -const PROTOCOL_VERSION = 1; - interface FastCheckProjectionRequest { - protocolVersion: 1; - requestId: string; - operation: 'sample'; seed: number; numSamples: number; domains: unknown[]; } interface FastCheckProjectionSuccess { - protocolVersion: 1; - requestId: string; status: 'ok'; samples: TaggedJsValue[][]; } interface FastCheckProjectionFailure { - protocolVersion: 1; - requestId?: string; status: 'error'; - diagnostics: Array<{ - code: string; - message: string; - path: string; - }>; + diagnostics: ProtocolDiagnostic[]; } type FastCheckProjectionWireResponse = FastCheckProjectionSuccess | FastCheckProjectionFailure; -let parsedRequest: unknown = undefined; let response: FastCheckProjectionWireResponse; try { const input = await readStdin(); + let parsedRequest: unknown; + try { parsedRequest = JSON.parse(input) as unknown; } catch { - throw protocolError('protocol.json.invalid', 'Standard input is not valid JSON', 'request'); + throw protocolError( + adapterDiagnostic.protocolJsonInvalid, + 'Standard input is not valid JSON', + 'request', + ); } + const request = validateRequest(parsedRequest); const arbitrary = fc.tuple( ...request.domains.map((domain, index) => projectDomain(domain, `domains[${index}]`)), ); + const tuples = fc.sample(arbitrary, { seed: request.seed, numRuns: request.numSamples, }); + response = { - protocolVersion: PROTOCOL_VERSION, - requestId: request.requestId, status: 'ok', samples: tuples.map((tuple) => tuple.map(encodeJsValue)), }; } catch (error: unknown) { - response = protocolErrorResponse(error, parsedRequest); + response = protocolErrorResponse(error); } process.stdout.write(`${JSON.stringify(response)}\n`); async function readStdin(): Promise { process.stdin.setEncoding('utf8'); + let input = ''; for await (const chunk of process.stdin) input += chunk; + return input; } -function validateRequest(request: unknown): FastCheckProjectionRequest { - if (!isRecord(request)) { - throw protocolError('protocol.request.invalid', 'Request must be a JSON object', 'request'); - } - if (request.protocolVersion !== PROTOCOL_VERSION) { - throw protocolError( - 'protocol.version.unsupported', - `Unsupported protocol version: ${String(request.protocolVersion)}`, - 'protocolVersion', - ); - } - if (request.operation !== 'sample') { - throw protocolError( - 'protocol.operation.unsupported', - `Unsupported protocol operation: ${String(request.operation)}`, - 'operation', - ); - } - const valid = typeof request.requestId === 'string' - && request.requestId.length > 0 - && typeof request.seed === 'number' +function validateRequest(value: unknown): FastCheckProjectionRequest { + const request = requireRecord(value); + + const validSeed = typeof request.seed === 'number' && Number.isInteger(request.seed) && request.seed >= -0x80000000 - && request.seed <= 0x7fffffff - && typeof request.numSamples === 'number' + && request.seed <= 0x7fffffff; + + const validSampleCount = typeof request.numSamples === 'number' && Number.isInteger(request.numSamples) - && request.numSamples >= 1 - && request.numSamples <= 10_000 - && Array.isArray(request.domains) - && request.domains.length > 0; - if (!valid) { + && request.numSamples >= 1; + + const hasDomains = Array.isArray(request.domains) && request.domains.length > 0; + + if (!validSeed || !validSampleCount || !hasDomains) { throw protocolError( - 'protocol.request.invalid', - 'Request requires a non-empty ID and domains, an Int seed, and numSamples in 1..10000', + adapterDiagnostic.protocolRequestInvalid, + 'Request requires domains, an Int seed, and a positive numSamples', 'request', ); } + return { - protocolVersion: PROTOCOL_VERSION, - requestId: request.requestId as string, - operation: 'sample', seed: request.seed as number, numSamples: request.numSamples as number, domains: request.domains as unknown[], }; } -function protocolErrorResponse(error: unknown, request: unknown): FastCheckProjectionFailure { +function protocolErrorResponse(error: unknown): FastCheckProjectionFailure { const protocolFailure = error instanceof ProtocolError ? error : undefined; - const result: FastCheckProjectionFailure = { - protocolVersion: PROTOCOL_VERSION, + const fallback = adapterDiagnostic.protocolRequestInvalid; + + return { status: 'error', diagnostics: [{ - code: protocolFailure?.code ?? 'protocol.request.invalid', + kind: protocolFailure?.kind ?? fallback.kind, + code: protocolFailure?.code ?? fallback.code, message: protocolFailure?.diagnosticMessage ?? (error instanceof Error ? error.message : String(error)), path: protocolFailure?.path ?? 'request', }], }; - if (isRecord(request) && typeof request.requestId === 'string') { - result.requestId = request.requestId; - } - return result; } -function isRecord(value: unknown): value is Record { - return value !== null && typeof value === 'object' && !Array.isArray(value); +function requireRecord(value: unknown): Record { + if (value === null || typeof value !== 'object' || Array.isArray(value)) { + throw protocolError( + adapterDiagnostic.protocolRequestInvalid, + 'Request must be a JSON object', + 'request', + ); + } + + return value as Record; } diff --git a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts new file mode 100644 index 000000000..58d11dc5d --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts @@ -0,0 +1,224 @@ +import assert from 'node:assert/strict'; +import { mkdtemp, mkdir, realpath, rm, symlink, writeFile } from 'node:fs/promises'; +import { tmpdir } from 'node:os'; +import path from 'node:path'; +import test from 'node:test'; +import { ProtocolError } from '../src/js-value.js'; +import { loadEntryPoint } from '../src/entry-point.js'; + +test('loads and invokes a TypeScript function directly from a source root', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + await mkdir(path.join(sourceRoot, 'properties'), { recursive: true }); + await writeFile( + path.join(sourceRoot, 'properties', 'positive.ts'), + 'export function isPositive(value: number): boolean { return value > 0; }\n', + ); + + const loaded = await loadEntryPoint( + { + module: 'properties/positive.ts', + exportName: 'isPositive', + executionKind: 'sync', + }, + [sourceRoot], + 'predicate', + ); + + assert.equal(loaded.invoke([1]), true); + assert.equal(loaded.invoke([-1]), false); + }); +}); + +test('loads and invokes an asynchronous TypeScript function', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + await mkdir(sourceRoot); + await writeFile( + path.join(sourceRoot, 'async.ts'), + 'export async function predicate(value: boolean): Promise { return value; }\n', + ); + + const loaded = await loadEntryPoint( + { module: 'async.ts', exportName: 'predicate', executionKind: 'async' }, + [sourceRoot], + 'predicate', + ); + + assert.equal(await loaded.invoke([true]), true); + }); +}); + +test('rejects missing and ambiguous modules with distinct diagnostics', async () => { + await withWorkspace(async (workspace) => { + const firstRoot = path.join(workspace, 'first'); + const secondRoot = path.join(workspace, 'second'); + + await mkdir(firstRoot); + await mkdir(secondRoot); + + await assertProtocolError( + loadEntryPoint( + { module: 'missing.ts', exportName: 'predicate', executionKind: 'sync' }, + [firstRoot], + 'predicate', + ), + 'entrypoint.module.not-found', + 'predicate.module', + ); + + await writeFile(path.join(firstRoot, 'duplicate.ts'), 'export function predicate() { return true; }\n'); + await writeFile(path.join(secondRoot, 'duplicate.ts'), 'export function predicate() { return true; }\n'); + + await assertProtocolError( + loadEntryPoint( + { module: 'duplicate.ts', exportName: 'predicate', executionKind: 'sync' }, + [firstRoot, secondRoot], + 'predicate', + ), + 'entrypoint.module.ambiguous', + 'predicate.module', + ); + }); +}); + +test('reports a candidate below a regular file as a missing module', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + await mkdir(sourceRoot); + await writeFile(path.join(sourceRoot, 'file.ts'), 'export function predicate() { return true; }\n'); + + await assertProtocolError( + loadEntryPoint( + { module: 'file.ts/nested.ts', exportName: 'predicate', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ), + 'entrypoint.module.not-found', + 'predicate.module', + ); + }); +}); + +test('rejects a module whose symlink escapes its source root', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + const outside = path.join(workspace, 'outside.ts'); + + await mkdir(sourceRoot); + await writeFile(outside, 'export function predicate() { return true; }\n'); + await symlink(outside, path.join(sourceRoot, 'escape.ts')); + + await assertProtocolError( + loadEntryPoint( + { module: 'escape.ts', exportName: 'predicate', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ), + 'entrypoint.module.outside-root', + 'predicate.module', + ); + }); +}); + +test('rejects missing and non-function exports', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + await mkdir(sourceRoot); + await writeFile(path.join(sourceRoot, 'exports.ts'), 'export const value = 42;\n'); + + await assertProtocolError( + loadEntryPoint( + { module: 'exports.ts', exportName: 'missing', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ), + 'entrypoint.export.not-found', + 'predicate.exportName', + ); + + await assertProtocolError( + loadEntryPoint( + { module: 'exports.ts', exportName: 'value', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ), + 'entrypoint.export.not-function', + 'predicate.exportName', + ); + }); +}); + +test('enforces declared execution kind and boolean results', async () => { + await withWorkspace(async (workspace) => { + const sourceRoot = path.join(workspace, 'src'); + await mkdir(sourceRoot); + await writeFile( + path.join(sourceRoot, 'contracts.ts'), + [ + 'export async function returnsPromise(): Promise { return true; }', + 'export function returnsDirectly(): boolean { return true; }', + 'export function returnsNumber(): number { return 1; }', + ].join('\n'), + ); + + const declaredSync = await loadEntryPoint( + { module: 'contracts.ts', exportName: 'returnsPromise', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ); + + assert.throws( + () => declaredSync.invoke([]), + (error: unknown) => isProtocolError(error, 'entrypoint.execution-kind.mismatch'), + ); + + const declaredAsync = await loadEntryPoint( + { module: 'contracts.ts', exportName: 'returnsDirectly', executionKind: 'async' }, + [sourceRoot], + 'predicate', + ); + + await assertProtocolError( + Promise.resolve(declaredAsync.invoke([])), + 'entrypoint.execution-kind.mismatch', + 'predicate.executionKind', + ); + + const nonBoolean = await loadEntryPoint( + { module: 'contracts.ts', exportName: 'returnsNumber', executionKind: 'sync' }, + [sourceRoot], + 'predicate', + ); + + assert.throws( + () => nonBoolean.invoke([]), + (error: unknown) => isProtocolError(error, 'entrypoint.result.invalid'), + ); + }); +}); + +async function withWorkspace(block: (workspace: string) => Promise): Promise { + const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-entry-point-'))); + + try { + await block(workspace); + } finally { + await rm(workspace, { recursive: true, force: true }); + } +} + +async function assertProtocolError( + promise: Promise, + code: string, + errorPath: string, +): Promise { + await assert.rejects( + promise, + (error: unknown) => isProtocolError(error, code) && error.path === errorPath, + ); +} + +function isProtocolError(error: unknown, code: string): error is ProtocolError { + return error instanceof ProtocolError && error.code === code; +} diff --git a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts new file mode 100644 index 000000000..ab1f69877 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -0,0 +1,189 @@ +import assert from 'node:assert/strict'; +import { mkdtemp, mkdir, realpath, rm, writeFile } from 'node:fs/promises'; +import { tmpdir } from 'node:os'; +import path from 'node:path'; +import test from 'node:test'; +import { encodeJsValue } from '../src/js-value.js'; +import { + executeProperty, + type FastCheckExecutionRequest, + type FastCheckRunResult, +} from '../src/execute-property.js'; + +test('executes a synchronous TypeScript predicate with deterministic success details', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'alwaysTrue'); + + const first = await executeProperty(request); + const second = await executeProperty(request); + + assert.equal(first.status, 'ok'); + assert.equal(first.result.status, 'success'); + assert.equal(first.result.seed, 42); + assert.equal(first.result.numRuns, 20); + assert.equal(first.result.counterexample, null); + assert.deepEqual(semanticResult(first.result), semanticResult(second.result)); + }); +}); + +test('returns a shrunk counterexample and replays it with the reported seed and path', async () => { + await withPropertyModule(async (sourceRoot) => { + const first = await executeProperty(executionRequest(sourceRoot, 'isNegative')); + + assert.equal(first.result.status, 'failure'); + assert.equal(first.result.failure?.kind, 'property'); + assert.ok(first.result.counterexample); + assert.ok(first.result.replayPath); + + const replay = await executeProperty({ + ...executionRequest(sourceRoot, 'isNegative'), + replayPath: first.result.replayPath, + seed: first.result.seed, + }); + + assert.deepEqual(replay.result.counterexample, first.result.counterexample); + assert.equal(replay.result.replayPath, first.result.replayPath); + }); +}); + +test('supports asynchronous predicates and preconditions', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'asyncAlwaysTrue', { + predicateExecutionKind: 'async', + precondition: { + module: 'properties.ts', + exportName: 'asyncIsOne', + executionKind: 'async', + }, + inputDomain: { kind: 'integer', min: 0, max: 1 }, + }); + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'success'); + assert.equal(response.result.numRuns, 20); + assert.ok(response.result.numSkips > 0); + }); +}); + +test('executes explicit examples through the same predicate', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'isNotSeven'); + request.examples = [[encodeJsValue(7)]]; + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'failure'); + assert.deepEqual(response.result.counterexample, [encodeJsValue(7)]); + }); +}); + +test('reports asynchronous predicate timeout as a structured timeout failure', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'neverCompletes', { + predicateExecutionKind: 'async', + }); + request.timeoutMillis = 20; + request.numRuns = 1; + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'failure'); + assert.equal(response.result.failure?.kind, 'timeout'); + }); +}); + +test('keeps a counterexample classified as a property failure when shrinking is interrupted', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'slowFailure', { + inputDomain: { + kind: 'array', + element: { kind: 'integer', min: -100, max: 100 }, + minLength: 50, + maxLength: 100, + }, + }); + request.timeoutMillis = 40; + request.numRuns = 100; + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'failure'); + assert.ok(response.result.counterexample); + assert.equal(response.result.failure?.kind, 'property'); + }); +}); + +interface RequestOverrides { + predicateExecutionKind?: 'sync' | 'async'; + precondition?: FastCheckExecutionRequest['manifest']['precondition']; + inputDomain?: unknown; +} + +function executionRequest( + sourceRoot: string, + predicateExport: string, + overrides: RequestOverrides = {}, +): FastCheckExecutionRequest { + const manifest: FastCheckExecutionRequest['manifest'] = { + propertyId: `example.${predicateExport}`, + inputs: [{ + name: 'value', + domain: overrides.inputDomain ?? { kind: 'integer', min: -10, max: 10 }, + }], + predicate: { + module: 'properties.ts', + exportName: predicateExport, + executionKind: overrides.predicateExecutionKind ?? 'sync', + }, + }; + + if (overrides.precondition !== undefined) manifest.precondition = overrides.precondition; + + return { + manifest, + sourceRoots: [sourceRoot], + seed: 42, + numRuns: 20, + timeoutMillis: 1_000, + examples: [], + }; +} + +async function withPropertyModule(block: (sourceRoot: string) => Promise): Promise { + const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execute-property-'))); + const sourceRoot = path.join(workspace, 'src'); + + await mkdir(sourceRoot); + await writeFile( + path.join(sourceRoot, 'properties.ts'), + [ + 'export function alwaysTrue(_value: number): boolean { return true; }', + 'export function isNegative(value: number): boolean { return value < 0; }', + 'export async function asyncAlwaysTrue(_value: number): Promise { return true; }', + 'export async function asyncIsOne(value: number): Promise { return value === 1; }', + 'export function isNotSeven(value: number): boolean { return value !== 7; }', + 'export function slowFailure(_value: number[]): boolean {', + ' const deadline = Date.now() + 10;', + ' while (Date.now() < deadline) {}', + ' return false;', + '}', + 'export async function neverCompletes(_value: number): Promise {', + ' await new Promise(() => undefined);', + ' return true;', + '}', + ].join('\n'), + ); + + try { + await block(sourceRoot); + } finally { + await rm(workspace, { recursive: true, force: true }); + } +} + +function semanticResult(result: FastCheckRunResult): Omit { + const { executionTimeMillis: _executionTimeMillis, ...semantic } = result; + + return semantic; +} diff --git a/usvm-ts-pbt/fast-check-adapter/test/execution-cli.test.ts b/usvm-ts-pbt/fast-check-adapter/test/execution-cli.test.ts new file mode 100644 index 000000000..3c147cce0 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/execution-cli.test.ts @@ -0,0 +1,142 @@ +import assert from 'node:assert/strict'; +import { spawn } from 'node:child_process'; +import { mkdtemp, realpath, rm, writeFile } from 'node:fs/promises'; +import { tmpdir } from 'node:os'; +import path from 'node:path'; +import type { Readable } from 'node:stream'; +import { fileURLToPath } from 'node:url'; +import test from 'node:test'; +import type { ProtocolDiagnostic } from '../src/js-value.js'; + +const cliPath = fileURLToPath(new URL('../src/execution-cli.js', import.meta.url)); + +test('execution CLI emits one successful response document', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execution-cli-'))); + try { + await writeFile(sourceRoot + '/property.ts', 'export function predicate(value: boolean) { return value; }\n'); + + const invocation = await invokeCli(JSON.stringify(executionRequest(sourceRoot))); + const response = JSON.parse(invocation.stdout) as Record; + + assert.equal(invocation.timedOut, false); + assert.equal(invocation.exitCode, 0); + assert.equal(invocation.stderr, ''); + assert.equal(invocation.stdout.trim().split('\n').length, 1); + assert.equal(response.status, 'ok'); + assert.equal('protocolVersion' in response, false); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + +test('execution CLI reports malformed JSON without crashing', async () => { + const invocation = await invokeCli('{not-json'); + const response = JSON.parse(invocation.stdout) as ExecutionErrorResponse; + + assert.equal(invocation.exitCode, 0); + assert.equal(invocation.stderr, ''); + assert.equal(response.status, 'error'); + assert.equal(response.diagnostics[0]?.kind, 'invalid-request'); + assert.equal(response.diagnostics[0]?.code, 'protocol.json.invalid'); +}); + +test('execution CLI keeps user logging outside the protocol response', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execution-cli-'))); + try { + await writeFile( + sourceRoot + '/property.ts', + "console.log('module log');\n" + + "export function predicate(value: boolean) { console.log('predicate log'); return value; }\n", + ); + + const invocation = await invokeCli(JSON.stringify(executionRequest(sourceRoot))); + + assert.equal(invocation.timedOut, false); + assert.equal(invocation.exitCode, 0); + assert.equal(invocation.stdout.trim().split('\n').length, 1); + assert.equal((JSON.parse(invocation.stdout) as Record).status, 'ok'); + assert.match(invocation.stderr, /module log/); + assert.match(invocation.stderr, /predicate log/); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + +test('execution CLI exits after writing a response when user code leaves an open handle', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execution-cli-'))); + try { + await writeFile( + sourceRoot + '/property.ts', + 'export function predicate(value: boolean) { setInterval(() => undefined, 1_000); return value; }\n', + ); + + const invocation = await invokeCli(JSON.stringify(executionRequest(sourceRoot))); + + assert.equal(invocation.timedOut, false); + assert.equal(invocation.exitCode, 0); + assert.equal((JSON.parse(invocation.stdout) as Record).status, 'ok'); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + +interface ExecutionErrorResponse { + status: string; + diagnostics: ProtocolDiagnostic[]; +} + +interface CliInvocation { + exitCode: number | null; + stdout: string; + stderr: string; + timedOut: boolean; +} + +async function invokeCli(input: string, timeoutMillis = 3_000): Promise { + const child = spawn(process.execPath, [cliPath], { stdio: ['pipe', 'pipe', 'pipe'] }); + + let timedOut = false; + const timeout = setTimeout(() => { + timedOut = true; + child.kill(); + }, timeoutMillis); + + child.stdin.end(input); + + try { + const [exitCode, stdout, stderr] = await Promise.all([ + new Promise((resolve, reject) => { + child.once('error', reject); + child.once('close', (code) => resolve(code)); + }), + collect(child.stdout), + collect(child.stderr), + ]); + + return { exitCode, stdout, stderr, timedOut }; + } finally { + clearTimeout(timeout); + } +} + +async function collect(stream: Readable): Promise { + const chunks: Buffer[] = []; + for await (const chunk of stream) chunks.push(Buffer.from(chunk)); + + return Buffer.concat(chunks).toString('utf8'); +} + +function executionRequest(sourceRoot: string): Record { + return { + manifest: { + propertyId: 'example.cli', + inputs: [{ name: 'value', domain: { kind: 'constant', value: { kind: 'boolean', value: true } } }], + predicate: { module: 'property.ts', exportName: 'predicate', executionKind: 'sync' }, + }, + sourceRoots: [sourceRoot], + seed: 42, + numRuns: 1, + timeoutMillis: 1_000, + examples: [], + }; +} diff --git a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts index 3ae1be60b..eb2a86f43 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts @@ -8,6 +8,7 @@ import { test('bounded integers use a real fast-check arbitrary', () => { const samples = sample({ kind: 'integer', min: -3, max: 7 }); + assert.ok(samples.every( (value) => typeof value === 'number' && Number.isInteger(value) && value >= -3 && value <= 7, )); @@ -15,6 +16,7 @@ test('bounded integers use a real fast-check arbitrary', () => { test('strings are arbitrary UTF-16 code-unit sequences with declared lengths', () => { const samples = sample({ kind: 'string', minLength: 2, maxLength: 4 }); + assert.ok(samples.every( (value) => typeof value === 'string' && value.length >= 2 && value.length <= 4, )); @@ -44,6 +46,7 @@ test('bounded numbers exclude NaN and values outside their inclusive bounds', () max: taggedNumber(2.5), allowNaN: false, }); + assert.ok(samples.every( (value) => typeof value === 'number' && !Number.isNaN(value) && value >= -1.5 && value <= 2.5, )); @@ -54,6 +57,7 @@ test('singleton infinity ranges project without an empty finite arbitrary', () = [{ value: 'negative-infinity' }, Number.NEGATIVE_INFINITY], [{ value: 'positive-infinity' }, Number.POSITIVE_INFINITY], ]; + for (const [bound, expected] of bounds) { const samples = sample({ kind: 'number', @@ -61,6 +65,7 @@ test('singleton infinity ranges project without an empty finite arbitrary', () = max: bound, allowNaN: false, }); + assert.ok(samples.every((value) => value === expected)); } }); @@ -130,8 +135,6 @@ test('fast-check capability is exact for supported recursive domains', () => { maxLength: 2, }), { - backendId: 'fast-check', - backendVersion: '4.9.0', level: 'exact', diagnostics: [], }, @@ -140,11 +143,10 @@ test('fast-check capability is exact for supported recursive domains', () => { test('unknown domain kinds are rejected and reported as unsupported', () => { assert.throws(() => projectDomain({ kind: 'object' }), /domain\.kind\.unknown/); + assert.deepEqual( projectionCapability({ kind: 'object' }, 'inputs[0].domain'), { - backendId: 'fast-check', - backendVersion: '4.9.0', level: 'unsupported', diagnostics: [{ code: 'domain.kind.unknown', @@ -162,6 +164,8 @@ function sample(domain: unknown, numRuns = 100): unknown[] { function taggedNumber(value: number): { value: 'finite'; bits: string } { const buffer = new ArrayBuffer(8); const view = new DataView(buffer); + view.setFloat64(0, value, false); + return { value: 'finite', bits: view.getBigUint64(0, false).toString(16).padStart(16, '0') }; } diff --git a/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts b/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts index 6f46a8756..7b0b4bbc7 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts @@ -3,26 +3,18 @@ import { spawn } from 'node:child_process'; import type { Readable } from 'node:stream'; import { fileURLToPath } from 'node:url'; import test from 'node:test'; -import type { TaggedJsValue } from '../src/js-value.js'; +import type { ProtocolDiagnostic, TaggedJsValue } from '../src/js-value.js'; const cliPath = fileURLToPath(new URL('../src/projection-cli.js', import.meta.url)); interface SuccessResponse { - protocolVersion: number; - requestId: string; status: 'ok'; samples: TaggedJsValue[][]; } interface ErrorResponse { - protocolVersion: number; - requestId?: string; status: 'error'; - diagnostics: Array<{ - code: string; - message: string; - path: string; - }>; + diagnostics: ProtocolDiagnostic[]; } type WireResponse = SuccessResponse | ErrorResponse; @@ -34,11 +26,8 @@ interface InvocationResult { response: WireResponse | undefined; } -test('sample response echoes request identity and returns deterministic tagged values', async () => { +test('sample response returns deterministic tagged values', async () => { const request = { - protocolVersion: 1, - requestId: 'sample-1', - operation: 'sample', seed: 42, numSamples: 4, domains: [{ kind: 'integer', min: -1, max: 1 }], @@ -53,8 +42,6 @@ test('sample response echoes request identity and returns deterministic tagged v assert.equal(first.stderr, ''); assert.equal(first.stdout.trim().split('\n').length, 1); assert.deepEqual(firstResponse, secondResponse); - assert.equal(firstResponse.protocolVersion, 1); - assert.equal(firstResponse.requestId, 'sample-1'); assert.equal(firstResponse.status, 'ok'); if (firstResponse.status !== 'ok') assert.fail('Expected a successful response'); assert.equal(firstResponse.samples.length, 4); @@ -67,67 +54,34 @@ interface ProtocolErrorCase { name: string; input: unknown; code: string; - requestId: string; path: string; } const protocolErrorCases: ProtocolErrorCase[] = [ - { - name: 'unsupported protocol version', - input: { - protocolVersion: 2, - requestId: 'wrong-version', - operation: 'sample', - seed: 1, - numSamples: 1, - domains: [{ kind: 'boolean' }], - }, - code: 'protocol.version.unsupported', - requestId: 'wrong-version', - path: 'protocolVersion', - }, - { - name: 'unsupported operation', - input: { - protocolVersion: 1, - requestId: 'wrong-operation', - operation: 'check', - seed: 1, - numSamples: 1, - domains: [{ kind: 'boolean' }], - }, - code: 'protocol.operation.unsupported', - requestId: 'wrong-operation', - path: 'operation', - }, { name: 'invalid request', input: { - protocolVersion: 1, - requestId: '', - operation: 'sample', seed: 1.5, numSamples: 0, domains: [], }, code: 'protocol.request.invalid', - requestId: '', path: 'request', }, ]; -for (const { name, input, code, requestId, path } of protocolErrorCases) { +for (const { name, input, code, path } of protocolErrorCases) { test(`${name} returns a typed protocol error`, async () => { const result = await invokeCli(JSON.stringify(input)); const response = requireResponse(result); + assert.equal(result.exitCode, 0); assert.equal(response.status, 'error'); if (response.status !== 'error') assert.fail('Expected an error response'); assert.deepEqual(response, { - protocolVersion: 1, - requestId, status: 'error', diagnostics: [{ + kind: 'invalid-request', code, message: response.diagnostics[0]?.message, path, @@ -143,16 +97,17 @@ test('malformed JSON produces one clean protocol error document', async () => { assert.equal(result.exitCode, 0); assert.equal(result.stderr, ''); assert.equal(result.stdout.trim().split('\n').length, 1); - assert.equal(response.protocolVersion, 1); assert.equal(response.status, 'error'); if (response.status !== 'error') assert.fail('Expected an error response'); + assert.equal(response.diagnostics[0]?.kind, 'invalid-request'); assert.equal(response.diagnostics[0]?.code, 'protocol.json.invalid'); - assert.ok(!('requestId' in response)); }); async function invokeCli(input: string): Promise { const child = spawn(process.execPath, [cliPath], { stdio: ['pipe', 'pipe', 'pipe'] }); + child.stdin.end(input); + const [exitCode, stdout, stderr] = await Promise.all([ new Promise((resolve, reject) => { child.once('error', reject); @@ -161,22 +116,26 @@ async function invokeCli(input: string): Promise { collect(child.stdout), collect(child.stderr), ]); + let response: WireResponse | undefined; try { response = JSON.parse(stdout) as WireResponse; } catch { response = undefined; } + return { exitCode, stdout, stderr, response }; } async function collect(stream: Readable): Promise { const chunks: Buffer[] = []; for await (const chunk of stream) chunks.push(Buffer.from(chunk)); + return Buffer.concat(chunks).toString('utf8'); } function requireResponse(result: InvocationResult): WireResponse { assert.ok(result.response, `CLI did not return JSON: ${result.stdout}`); + return result.response; } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt new file mode 100644 index 000000000..fac25f84f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt @@ -0,0 +1,57 @@ +package org.usvm.ts.pbt + +/** Stable identifiers for diagnostics created on the Kotlin side of the PBT boundary. */ +internal object PbtDiagnosticCode { + const val CLI_ARGUMENT_INVALID = "cli.argument.invalid" + const val CLI_EXAMPLES_INVALID = "cli.examples.invalid" + const val CLI_NUM_RUNS_INVALID = "cli.num-runs.invalid" + const val CLI_PROPERTY_EMPTY = "cli.property.empty" + const val CLI_PROPERTY_INVALID = "cli.property.invalid" + const val CLI_PROPERTY_UNKNOWN = "cli.property.unknown" + const val CLI_REGISTRY_EMPTY = "cli.registry.empty" + const val CLI_REGISTRY_ID_DUPLICATE = "cli.registry.id.duplicate" + const val CLI_REGISTRY_ID_INVALID = "cli.registry.id.invalid" + const val CLI_REGISTRY_UNKNOWN = "cli.registry.unknown" + const val CLI_SINGLE_PROPERTY_REQUIRED = "cli.single-property.required" + const val CLI_SOURCE_ROOT_REQUIRED = "cli.source-root.required" + const val CLI_TIMEOUT_INVALID = "cli.timeout.invalid" + + const val REGISTRY_PROPERTY_ID_DUPLICATE = "registry.property-id.duplicate" + const val REGISTRY_PROPERTY_INVALID = "registry.property.invalid" + const val REGISTRY_PROVIDER_LOAD_FAILED = "registry.provider.load.failed" + + const val BACKEND_EXAMPLES_ARITY = "backend.examples.arity" + const val BACKEND_EXAMPLES_DOMAIN = "backend.examples.domain" + const val BACKEND_EXAMPLES_VALUE_INVALID = "backend.examples.value.invalid" + const val BACKEND_PROCESS_FAILED = "backend.process.failed" + const val BACKEND_PROCESS_INTERRUPTED = "backend.process.interrupted" + const val BACKEND_PROCESS_READ_FAILED = "backend.process.read.failed" + const val BACKEND_PROCESS_START_FAILED = "backend.process.start.failed" + const val BACKEND_PROCESS_TIMEOUT = "backend.process.timeout" + const val BACKEND_PROCESS_WRITE_FAILED = "backend.process.write.failed" + const val BACKEND_REQUEST_TOO_LARGE = "backend.request.too-large" + const val BACKEND_RESPONSE_EMPTY = "backend.response.empty" + const val BACKEND_RESPONSE_INVALID = "backend.response.invalid" + const val BACKEND_RESPONSE_TOO_LARGE = "backend.response.too-large" + const val BACKEND_RUNTIME_NOT_FOUND = "backend.runtime.not-found" + + const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid" + const val SOURCE_ROOT_INVALID = "source-root.invalid" + + const val PROPERTY_ID_INVALID = "property.id.invalid" + const val PROPERTY_INPUTS_EMPTY = "property.inputs.empty" + const val INPUT_NAME_DUPLICATE = "input.name.duplicate" + const val INPUT_NAME_INVALID = "input.name.invalid" + const val DOMAIN_ARRAY_LENGTH = "domain.array.length" + const val DOMAIN_CONSTANT_UNSUPPORTED = "domain.constant.unsupported" + const val DOMAIN_INTEGER_BOUNDS = "domain.integer.bounds" + const val DOMAIN_NUMBER_BOUND_NAN = "domain.number.bound.nan" + const val DOMAIN_NUMBER_BOUNDS = "domain.number.bounds" + const val DOMAIN_NUMBER_NAN_BOUNDED = "domain.number.nan-bounded" + const val DOMAIN_OPTIONAL_NIL = "domain.optional.nil" + const val DOMAIN_STRING_LENGTH = "domain.string.length" + const val DOMAIN_TUPLE_EMPTY = "domain.tuple.empty" + const val ENTRY_POINT_EXPORT_INVALID = "entrypoint.export.invalid" + const val ENTRY_POINT_MODULE_INVALID = "entrypoint.module.invalid" + const val JS_NUMBER_ENCODING_INVALID = "js-number.encoding.invalid" +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt index 2537881a7..a35007c37 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt @@ -41,22 +41,16 @@ data class CapabilityDiagnostic( ) /** - * Reports whether one backend version can represent a property domain. + * Reports whether a property domain can be represented by an execution backend. * - * @property backendId stable backend identifier - * @property backendVersion backend version used to evaluate support * @property level semantic fidelity of the projection * @property diagnostics limitations that explain a non-exact [level] */ data class ProjectionCapability( - val backendId: String, - val backendVersion: String, val level: ProjectionLevel, val diagnostics: List = emptyList(), ) { init { - require(backendId.isNotBlank()) { "Backend ID must not be blank" } - require(backendVersion.isNotBlank()) { "Backend version must not be blank" } require(level == ProjectionLevel.EXACT || diagnostics.isNotEmpty()) { "A non-exact projection requires at least one diagnostic" } @@ -65,20 +59,14 @@ data class ProjectionCapability( /** Combines domain-level [capabilities] into one deterministic backend capability report. */ fun aggregateProjectionCapabilities( - backendId: String, - backendVersion: String, capabilities: List, ): ProjectionCapability { - require(capabilities.all { it.backendId == backendId && it.backendVersion == backendVersion }) { - "All projection capabilities must belong to $backendId $backendVersion" - } val level = capabilities.maxOfOrNull { it.level } ?: ProjectionLevel.EXACT val diagnostics = capabilities .flatMap(ProjectionCapability::diagnostics) .sortedWith(compareBy(CapabilityDiagnostic::path, CapabilityDiagnostic::code)) + return ProjectionCapability( - backendId = backendId, - backendVersion = backendVersion, level = level, diagnostics = diagnostics, ) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt new file mode 100644 index 000000000..818e7aef6 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt @@ -0,0 +1,107 @@ +package org.usvm.ts.pbt.backend + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId + +/** Executes validated Kotlin property definitions through one concrete PBT engine. */ +interface PropertyBasedTestingBackend { + /** Executes [property] with [configuration] and returns a structured property result. */ + fun run( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + ): PropertyRunResult +} + +/** Backend-neutral controls for one concrete property run. */ +data class PropertyRunConfiguration( + val seed: Int? = null, + val replayPath: String? = null, + val numRuns: Int = DEFAULT_NUM_RUNS, + val timeoutMillis: Long = DEFAULT_TIMEOUT_MILLIS, + val examples: List> = emptyList(), +) { + init { + require(numRuns > 0) { "Number of runs must be positive" } + require(timeoutMillis > 0) { "Timeout must be positive" } + require(timeoutMillis <= MAX_TIMEOUT_MILLIS) { + "Timeout exceeds the maximum delay supported by Node timers" + } + } + + companion object { + const val DEFAULT_NUM_RUNS = 100 + const val DEFAULT_TIMEOUT_MILLIS = 60_000L + + /** Node timers use signed 32-bit millisecond delays. */ + val MAX_TIMEOUT_MILLIS: Long = Int.MAX_VALUE.toLong() + } +} + +/** Whether the predicate held for every value executed by the backend. */ +@Serializable +enum class PropertyRunStatus { + @SerialName("success") + SUCCESS, + + @SerialName("failure") + FAILURE, +} + +/** Stable classification of a completed property failure. */ +@Serializable +enum class PropertyFailureKind { + @SerialName("property") + PROPERTY, + + @SerialName("timeout") + TIMEOUT, +} + +/** Stable failure details that exclude runtime-dependent Node stack traces. */ +@Serializable +data class PropertyFailureDetails( + val kind: PropertyFailureKind, + val errorName: String, + val message: String, +) { + init { + require(errorName.isNotBlank()) { "Failure error name must not be blank" } + require(message.isNotBlank()) { "Failure message must not be blank" } + } +} + +/** Structured outcome of one concrete property run. */ +@Serializable +data class PropertyRunResult( + val propertyId: PropertyId, + val status: PropertyRunStatus, + val seed: Int, + val replayPath: String?, + val counterexample: List?, + val numRuns: Int, + val numSkips: Int, + val numShrinks: Int, + val failure: PropertyFailureDetails?, + val executionTimeMillis: Long, +) { + init { + require(numRuns >= 0) { "Run count must not be negative" } + require(numSkips >= 0) { "Skip count must not be negative" } + require(numShrinks >= 0) { "Shrink count must not be negative" } + require(executionTimeMillis >= 0) { "Execution time must not be negative" } + + when (status) { + PropertyRunStatus.SUCCESS -> { + require(counterexample == null) { "A successful run must not contain a counterexample" } + require(failure == null) { "A successful run must not contain failure details" } + } + + PropertyRunStatus.FAILURE -> { + requireNotNull(failure) { "A failed run requires failure details" } + } + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt new file mode 100644 index 000000000..d08b44a84 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckCli.kt @@ -0,0 +1,326 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.Serializable +import kotlinx.serialization.SerializationException +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.registry.DuplicatePropertyIdException +import org.usvm.ts.pbt.registry.PropertyRegistry +import org.usvm.ts.pbt.registry.PropertyRegistryProvider +import org.usvm.ts.pbt.registry.UnknownPropertyIdException +import org.usvm.ts.pbt.validation.InvalidPropertyDefinitionException +import java.io.IOException +import java.nio.file.Files +import java.nio.file.Path +import java.util.ServiceConfigurationError +import java.util.ServiceLoader +import kotlin.system.exitProcess + +/** Kotlin command-line orchestrator for service-loaded property registries and fast-check. */ +class FastCheckCli( + private val providers: List? = null, + private val backendFactory: (List) -> PropertyBasedTestingBackend = { sourceRoots -> + FastCheckBackend(sourceRoots) + }, + private val output: Appendable = System.out, + private val errors: Appendable = System.err, +) { + /** Runs the requested properties and returns the process exit code without terminating the JVM. */ + fun run(args: Array): Int = try { + when (val parsed = parseCliOptions(args)) { + is CliParseResult.Help -> { + output.appendLine(parsed.text) + + EXIT_SUCCESS + } + + is CliParseResult.Success -> { + execute(parsed.options) + } + } + } catch (error: CliUsageException) { + reportError(error.code, error.message.orEmpty(), error.path) + + EXIT_ERROR + } catch (error: DuplicatePropertyIdException) { + reportError( + code = PbtDiagnosticCode.REGISTRY_PROPERTY_ID_DUPLICATE, + message = error.message.orEmpty(), + path = "properties", + propertyId = error.propertyId.value, + ) + + EXIT_ERROR + } catch (error: UnknownPropertyIdException) { + reportError( + code = PbtDiagnosticCode.CLI_PROPERTY_UNKNOWN, + message = error.message.orEmpty(), + path = "property", + propertyId = error.propertyId.value, + ) + + EXIT_ERROR + } catch (error: InvalidPropertyDefinitionException) { + reportError( + code = PbtDiagnosticCode.REGISTRY_PROPERTY_INVALID, + message = error.message.orEmpty(), + path = error.result.diagnostics.firstOrNull()?.path, + ) + + EXIT_ERROR + } catch (error: PbtBackendException) { + reportError( + code = error.code, + message = error.message.orEmpty(), + path = error.path, + propertyId = error.propertyId, + kind = error.kind.name.lowercase(), + ) + + EXIT_ERROR + } catch (error: ServiceConfigurationError) { + reportError( + code = PbtDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, + message = error.message.orEmpty(), + path = "registry", + ) + + EXIT_ERROR + } catch (error: IllegalArgumentException) { + reportError( + code = PbtDiagnosticCode.CLI_ARGUMENT_INVALID, + message = error.message.orEmpty(), + ) + + EXIT_ERROR + } + + private fun execute(options: CliOptions): Int { + val selectedProviders = selectProviders(options.registryIds) + val registry = PropertyRegistry.combine(selectedProviders.map(::loadRegistry)) + val properties = selectProperties(registry, options.propertyId) + + requireSinglePropertyForRunScopedControls(options, properties.size) + + val examples = options.examplesFile?.let(::loadExamples).orEmpty() + val configuration = PropertyRunConfiguration( + seed = options.seed, + replayPath = options.replayPath, + numRuns = options.numRuns, + timeoutMillis = options.timeoutMillis, + examples = examples, + ) + + val backend = backendFactory(options.sourceRoots) + val results = properties.map { property -> backend.run(property, configuration) } + + output.appendLine(PropertyManifestJson.json.encodeToString(results)) + + val hasPropertyFailure = results.any { result -> result.status == PropertyRunStatus.FAILURE } + return if (hasPropertyFailure) { + EXIT_PROPERTY_FAILURE + } else { + EXIT_SUCCESS + } + } + + private fun selectProperties( + registry: PropertyRegistry, + propertyId: PropertyId?, + ): List { + if (propertyId != null) return listOf(registry[propertyId]) + + val properties = registry.properties + if (properties.isEmpty()) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_PROPERTY_EMPTY, + message = "Selected registries contain no properties", + path = "registry", + ) + } + + return properties + } + + @Suppress("TooGenericExceptionCaught") + private fun loadRegistry(registration: ProviderRegistration): PropertyRegistry = try { + registration.provider.load() + } catch (error: InvalidPropertyDefinitionException) { + throw error + } catch (error: DuplicatePropertyIdException) { + throw error + } catch (error: RuntimeException) { + throw providerFailure(registration.id, error) + } catch (error: LinkageError) { + throw providerFailure(registration.id, error) + } + + private fun requireSinglePropertyForRunScopedControls(options: CliOptions, propertyCount: Int) { + val usesRunScopedControls = options.replayPath != null || options.examplesFile != null + + if (usesRunScopedControls && propertyCount != 1) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_SINGLE_PROPERTY_REQUIRED, + message = "Replay paths and explicit examples require exactly one selected property", + path = "property", + ) + } + } + + private fun selectProviders(registryIds: List): List { + val availableProviders = (providers ?: loadProviders()).map(::registerProvider) + val orderedProviders = validateProviders(availableProviders.sortedBy(ProviderRegistration::id)) + + if (registryIds.isEmpty()) return orderedProviders + + val requestedIds = registryIds.toSet() + val availableIds = orderedProviders.map(ProviderRegistration::id).toSet() + val unknown = requestedIds.minus(availableIds).minOrNull() + + if (unknown != null) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_REGISTRY_UNKNOWN, + message = "Unknown registry ID $unknown; available IDs: ${availableIds.sorted().joinToString()}", + path = "registry", + ) + } + + return orderedProviders.filter { registration -> registration.id in requestedIds } + } + + private fun validateProviders( + orderedProviders: List, + ): List { + orderedProviders.forEach { registration -> validateProviderId(registration.id) } + validateUniqueProviderIds(orderedProviders) + + if (orderedProviders.isEmpty()) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_REGISTRY_EMPTY, + message = "No PropertyRegistryProvider services were found", + path = "registry", + ) + } + + return orderedProviders + } + + private fun validateProviderId(providerId: String) { + if (!REGISTRY_ID_REGEX.matches(providerId)) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_REGISTRY_ID_INVALID, + message = "Invalid registry ID: $providerId", + path = "registry", + ) + } + } + + private fun validateUniqueProviderIds(orderedProviders: List) { + val duplicateRegistryId = orderedProviders + .groupBy(ProviderRegistration::id) + .filterValues { duplicates -> duplicates.size > 1 } + .keys + .minOrNull() + + if (duplicateRegistryId != null) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_REGISTRY_ID_DUPLICATE, + message = "Duplicate registry ID: $duplicateRegistryId", + path = "registry", + ) + } + } + + @Suppress("TooGenericExceptionCaught") + private fun registerProvider(provider: PropertyRegistryProvider): ProviderRegistration = try { + ProviderRegistration( + id = provider.registryId, + provider = provider, + ) + } catch (error: RuntimeException) { + throw providerFailure(provider.javaClass.name, error) + } catch (error: LinkageError) { + throw providerFailure(provider.javaClass.name, error) + } + + private fun providerFailure(providerName: String, cause: Throwable) = CliUsageException( + code = PbtDiagnosticCode.REGISTRY_PROVIDER_LOAD_FAILED, + message = "Property registry provider $providerName failed: ${cause.message}", + path = "registry", + cause = cause, + ) + + private fun loadExamples(path: Path): List> = try { + PropertyManifestJson.json.decodeFromString(Files.readString(path)) + } catch (error: IOException) { + throw invalidExamples(path, error) + } catch (error: SerializationException) { + throw invalidExamples(path, error) + } + + private fun invalidExamples(path: Path, cause: Exception) = CliUsageException( + code = PbtDiagnosticCode.CLI_EXAMPLES_INVALID, + message = "Cannot read explicit examples from $path: ${cause.message}", + path = "examples", + cause = cause, + ) + + private fun reportError( + code: String, + message: String, + path: String? = null, + propertyId: String? = null, + kind: String? = null, + ) { + val diagnostic = CliDiagnostic( + code = code, + message = message, + path = path, + propertyId = propertyId, + kind = kind, + ) + + errors.appendLine(PropertyManifestJson.json.encodeToString(diagnostic)) + } + + private companion object { + const val EXIT_SUCCESS = 0 + const val EXIT_PROPERTY_FAILURE = 1 + const val EXIT_ERROR = 2 + + val REGISTRY_ID_REGEX = Regex("[A-Za-z0-9][A-Za-z0-9._/-]*") + + fun loadProviders(): List = ServiceLoader + .load(PropertyRegistryProvider::class.java) + .toList() + } +} + +/** Process entry point used by Gradle application and installed distributions. */ +fun main(args: Array) { + exitProcess(FastCheckCli().run(args)) +} + +@Serializable +private data class CliDiagnostic( + val code: String, + val message: String, + val path: String? = null, + val propertyId: String? = null, + val kind: String? = null, +) + +private data class ProviderRegistration( + val id: String, + val provider: PropertyRegistryProvider, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt new file mode 100644 index 000000000..b6075c901 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/cli/FastCheckOptions.kt @@ -0,0 +1,158 @@ +package org.usvm.ts.pbt.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.core.CliktError +import com.github.ajalt.clikt.core.PrintHelpMessage +import com.github.ajalt.clikt.core.parse +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.multiple +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.int +import com.github.ajalt.clikt.parameters.types.long +import com.github.ajalt.clikt.parameters.types.path +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.model.PropertyId +import java.nio.file.Path + +internal sealed interface CliParseResult { + data class Success(val options: CliOptions) : CliParseResult + + data class Help(val text: String) : CliParseResult +} + +internal data class CliOptions( + val sourceRoots: List, + val registryIds: List, + val propertyId: PropertyId?, + val seed: Int?, + val replayPath: String?, + val numRuns: Int, + val timeoutMillis: Long, + val examplesFile: Path?, +) + +internal class CliUsageException( + val code: String, + message: String, + val path: String? = null, + cause: Throwable? = null, +) : IllegalArgumentException(message, cause) + +internal fun parseCliOptions(args: Array): CliParseResult { + val parser = FastCheckOptionsParser() + + return try { + parser.parse(args) + + CliParseResult.Success(parser.options) + } catch (help: PrintHelpMessage) { + CliParseResult.Help(parser.getFormattedHelp(help).orEmpty()) + } catch (error: CliktError) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_ARGUMENT_INVALID, + message = error.message ?: "Invalid command line arguments", + cause = error, + ) + } +} + +private class FastCheckOptionsParser : CliktCommand(name = "usvm-ts-pbt") { + private val sourceRoots by option( + "--source-root", + help = "TypeScript source root; repeat for multiple roots", + ).path().multiple() + + private val registryIds by option( + "--registry", + help = "Property registry ID; defaults to all registries", + ).multiple() + + private val propertyIdText by option( + "--property", + help = "Property ID; defaults to every selected property", + ) + + private val seed by option( + "--seed", + help = "Signed fast-check seed", + ).int() + + private val replayPath by option( + "--path", + help = "Replay path returned by an earlier failure", + ) + + private val numRuns by option( + "--num-runs", + help = "Number of successful runs", + ).int().default(PropertyRunConfiguration.DEFAULT_NUM_RUNS) + + private val timeoutMillis by option( + "--timeout-ms", + help = "Property timeout in milliseconds", + ).long().default(PropertyRunConfiguration.DEFAULT_TIMEOUT_MILLIS) + + private val examplesFile by option( + "--examples", + help = "JSON file with positional tagged examples", + ).path() + + lateinit var options: CliOptions + private set + + override fun run() { + requireSourceRoots() + requirePositiveRunControls() + + options = CliOptions( + sourceRoots = sourceRoots, + registryIds = registryIds, + propertyId = propertyIdText?.let(::parsePropertyId), + seed = seed, + replayPath = replayPath, + numRuns = numRuns, + timeoutMillis = timeoutMillis, + examplesFile = examplesFile, + ) + } + + private fun requireSourceRoots() { + if (sourceRoots.isEmpty()) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_SOURCE_ROOT_REQUIRED, + message = "At least one --source-root is required", + path = "sourceRoot", + ) + } + } + + private fun requirePositiveRunControls() { + if (numRuns <= 0) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_NUM_RUNS_INVALID, + message = "--num-runs must be positive", + path = "numRuns", + ) + } + + if (timeoutMillis !in 1..PropertyRunConfiguration.MAX_TIMEOUT_MILLIS) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_TIMEOUT_INVALID, + message = "--timeout-ms must be in 1..${PropertyRunConfiguration.MAX_TIMEOUT_MILLIS}", + path = "timeoutMillis", + ) + } + } +} + +private fun parsePropertyId(value: String): PropertyId = try { + PropertyId(value) +} catch (error: IllegalArgumentException) { + throw CliUsageException( + code = PbtDiagnosticCode.CLI_PROPERTY_INVALID, + message = error.message.orEmpty(), + path = "property", + cause = error, + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt new file mode 100644 index 000000000..66158dbe6 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -0,0 +1,172 @@ +package org.usvm.ts.pbt.fastcheck + +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.JsNumberKind +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.validation.requireValid +import org.usvm.ts.pbt.validation.validatePropertyDefinition +import java.io.IOException +import java.nio.file.Files +import java.nio.file.Path + +/** Executes Kotlin-owned property definitions with fast-check over a private TypeScript bridge. */ +class FastCheckBackend( + sourceRoots: List, + nodeExecutable: String = "node", + adapterEntryPoint: Path = FastCheckRuntime.executionEntryPoint(), +) : PropertyBasedTestingBackend { + private val sourceRoots = canonicalizeSourceRoots(sourceRoots) + private val client = FastCheckProcessClient( + nodeExecutable = nodeExecutable, + adapterEntryPoint = adapterEntryPoint, + ) + + override fun run( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + ): PropertyRunResult { + requireValid(validatePropertyDefinition(property)) + validateConfiguration(property, configuration) + + return client.check( + FastCheckExecutionRequest( + manifest = property.toManifest(), + sourceRoots = sourceRoots.map(Path::toString), + seed = configuration.seed, + replayPath = configuration.replayPath, + numRuns = configuration.numRuns, + timeoutMillis = configuration.timeoutMillis, + examples = configuration.examples, + ), + ) + } + + private fun validateConfiguration( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + ) { + validateExamples(property, configuration) + } + + private fun validateExamples( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + ) { + configuration.examples.forEachIndexed { index, example -> + if (example.size != property.inputs.size) { + throw invalidRequest( + code = PbtDiagnosticCode.BACKEND_EXAMPLES_ARITY, + message = "Explicit example $index has ${example.size} values, expected ${property.inputs.size}", + property = property, + path = "examples[$index]", + ) + } + + example.forEachIndexed { valueIndex, value -> + val path = "examples[$index][$valueIndex]" + + validateExampleValue( + property = property, + value = value, + path = path, + ) + + if (value !in property.inputs[valueIndex].domain) { + throw invalidRequest( + code = PbtDiagnosticCode.BACKEND_EXAMPLES_DOMAIN, + message = "Explicit example does not belong to the declared input domain", + property = property, + path = path, + ) + } + } + } + } + + private fun validateExampleValue( + property: PropertyDefinition, + value: JsConcreteValue, + path: String, + ) { + if (value is JsConcreteValue.Number && !hasValidEncoding(value)) { + throw invalidRequest( + code = PbtDiagnosticCode.BACKEND_EXAMPLES_VALUE_INVALID, + message = "Explicit example contains an invalid tagged JavaScript number", + property = property, + path = path, + ) + } + + if (value is JsConcreteValue.Array) { + value.elements.forEachIndexed { index, element -> + validateExampleValue( + property = property, + value = element, + path = "$path.elements[$index]", + ) + } + } + } + + private fun hasValidEncoding(value: JsConcreteValue.Number): Boolean = when (value.number.value) { + JsNumberKind.FINITE -> value.number.bits?.matches(FINITE_NUMBER_BITS_REGEX) == true + else -> value.number.bits == null + } + + private fun invalidRequest( + code: String, + message: String, + property: PropertyDefinition, + path: String, + ) = PbtBackendException( + kind = BackendErrorKind.INVALID_REQUEST, + code = code, + message = message, + propertyId = property.id.value, + path = path, + ) + + companion object { + private val FINITE_NUMBER_BITS_REGEX = Regex("[0-9a-f]{16}") + + private fun canonicalizeSourceRoots(sourceRoots: List): List { + if (sourceRoots.isEmpty()) { + throw PbtBackendException( + kind = BackendErrorKind.INVALID_REQUEST, + code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + message = "At least one TypeScript source root is required", + path = "sourceRoots", + ) + } + + return sourceRoots.mapIndexed(::canonicalizeSourceRoot).distinct() + } + + private fun canonicalizeSourceRoot(index: Int, sourceRoot: Path): Path = try { + sourceRoot.toRealPath().also { realPath -> + if (!Files.isDirectory(realPath)) { + throw PbtBackendException( + kind = BackendErrorKind.INVALID_REQUEST, + code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + message = "TypeScript source root is not a directory: $sourceRoot", + path = "sourceRoots[$index]", + ) + } + } + } catch (error: IOException) { + throw PbtBackendException( + kind = BackendErrorKind.INVALID_REQUEST, + code = PbtDiagnosticCode.SOURCE_ROOT_INVALID, + message = "Cannot resolve TypeScript source root $sourceRoot: ${error.message}", + path = "sourceRoots[$index]", + cause = error, + ) + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt new file mode 100644 index 000000000..7b7e507f6 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt @@ -0,0 +1,54 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.model.JsConcreteValue + +@Serializable +internal data class FastCheckExecutionRequest( + val manifest: PropertyManifest, + val sourceRoots: List, + val seed: Int? = null, + val replayPath: String? = null, + val numRuns: Int, + val timeoutMillis: Long, + val examples: List> = emptyList(), +) + +@Serializable +internal data class FastCheckExecutionWireResponse( + val status: String, + val result: PropertyRunResult? = null, + val diagnostics: List = emptyList(), +) + +/** Infrastructure categories that remain distinct from a falsified property result. */ +@Serializable +enum class BackendErrorKind { + @SerialName("invalid-request") + INVALID_REQUEST, + + @SerialName("entry-point") + ENTRY_POINT, + + @SerialName("process-failure") + PROCESS_FAILURE, + + @SerialName("protocol-error") + PROTOCOL_ERROR, + + @SerialName("timeout") + TIMEOUT, +} + +/** Typed failure at the concrete backend boundary. */ +class PbtBackendException( + val kind: BackendErrorKind, + val code: String, + message: String, + val propertyId: String? = null, + val path: String? = null, + cause: Throwable? = null, +) : RuntimeException(message, cause) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt new file mode 100644 index 000000000..187417291 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt @@ -0,0 +1,346 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.coroutines.CancellationException +import kotlinx.coroutines.CoroutineDispatcher +import kotlinx.coroutines.Deferred +import kotlinx.coroutines.Dispatchers +import kotlinx.coroutines.async +import kotlinx.coroutines.runBlocking +import kotlinx.coroutines.runInterruptible +import kotlinx.coroutines.supervisorScope +import kotlinx.coroutines.withTimeoutOrNull +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.PropertyId +import java.io.ByteArrayOutputStream +import java.io.IOException +import java.io.InputStream +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** Supervised one-shot transport for the private fast-check execution bridge. */ +internal class FastCheckProcessClient( + private val nodeExecutable: String = "node", + private val adapterEntryPoint: Path, + private val transportGraceMillis: Long = DEFAULT_TRANSPORT_GRACE_MILLIS, + private val shutdownGraceMillis: Long = DEFAULT_SHUTDOWN_GRACE_MILLIS, + private val ioDispatcher: CoroutineDispatcher = Dispatchers.IO, +) { + /** Executes one request and exposes only a fully validated common result. */ + fun check(request: FastCheckExecutionRequest): PropertyRunResult = try { + runBlocking { checkSuspending(request) } + } catch (error: InterruptedException) { + Thread.currentThread().interrupt() + + throw backendError( + kind = BackendErrorKind.PROCESS_FAILURE, + code = PbtDiagnosticCode.BACKEND_PROCESS_INTERRUPTED, + message = "Interrupted while waiting for the fast-check adapter", + request = request, + cause = error, + ) + } + + private suspend fun checkSuspending(request: FastCheckExecutionRequest): PropertyRunResult = supervisorScope { + val encodedRequest = encodeRequest(request) + + val process = startAdapter(request) + val stdout = async(ioDispatcher) { process.inputStream.readBounded(MAX_STDOUT_BYTES) } + val stderr = async(ioDispatcher) { process.errorStream.readBounded(MAX_STDERR_BYTES) } + val writer = async(ioDispatcher) { + process.outputStream.bufferedWriter(Charsets.UTF_8).use { output -> + output.write(encodedRequest) + } + } + + try { + awaitProcess(process, request) + + awaitIo( + task = writer, + operation = "writing the fast-check request", + failureCode = PbtDiagnosticCode.BACKEND_PROCESS_WRITE_FAILED, + request = request, + ) + + val stdoutText = awaitIo( + task = stdout, + operation = "reading fast-check stdout", + failureCode = PbtDiagnosticCode.BACKEND_PROCESS_READ_FAILED, + request = request, + ) + val stderrText = awaitIo( + task = stderr, + operation = "reading fast-check stderr", + failureCode = PbtDiagnosticCode.BACKEND_PROCESS_READ_FAILED, + request = request, + ) + + validateProcessExit(process, stderrText, request) + validateStdout(stdoutText, request) + + val response = decodeResponse(stdoutText.text, request) + + decodeSuccessfulResponse(response, request) + } finally { + if (process.isAlive) terminate(process) + } + } + + private fun encodeRequest(request: FastCheckExecutionRequest): String { + val encodedRequest = PropertyManifestJson.json.encodeToString(request) + + if (encodedRequest.toByteArray(Charsets.UTF_8).size > MAX_REQUEST_BYTES) { + throw backendError( + kind = BackendErrorKind.INVALID_REQUEST, + code = PbtDiagnosticCode.BACKEND_REQUEST_TOO_LARGE, + message = "fast-check request exceeds $MAX_REQUEST_BYTES bytes", + request = request, + ) + } + + return encodedRequest + } + + private suspend fun awaitProcess(process: Process, request: FastCheckExecutionRequest) { + val hardTimeoutMillis = safeAdd(request.timeoutMillis, transportGraceMillis) + val exitCode = withTimeoutOrNull(hardTimeoutMillis) { + runInterruptible(ioDispatcher) { process.waitFor() } + } + + if (exitCode == null) { + terminate(process) + + throw backendError( + kind = BackendErrorKind.TIMEOUT, + code = PbtDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = "fast-check adapter exceeded the ${request.timeoutMillis} ms timeout", + request = request, + ) + } + } + + private fun validateProcessExit( + process: Process, + stderr: BoundedText, + request: FastCheckExecutionRequest, + ) { + if (process.exitValue() != 0) { + val detail = stderr.text.trim().ifEmpty { "no stderr" } + + throw backendError( + kind = BackendErrorKind.PROCESS_FAILURE, + code = PbtDiagnosticCode.BACKEND_PROCESS_FAILED, + message = "fast-check adapter exited with code ${process.exitValue()}: $detail", + request = request, + ) + } + } + + private fun validateStdout(stdout: BoundedText, request: FastCheckExecutionRequest) { + if (stdout.exceeded) { + throw backendError( + kind = BackendErrorKind.PROTOCOL_ERROR, + code = PbtDiagnosticCode.BACKEND_RESPONSE_TOO_LARGE, + message = "fast-check adapter stdout exceeds $MAX_STDOUT_BYTES bytes", + request = request, + ) + } + + if (stdout.text.isBlank()) { + throw backendError( + kind = BackendErrorKind.PROTOCOL_ERROR, + code = PbtDiagnosticCode.BACKEND_RESPONSE_EMPTY, + message = "fast-check adapter returned an empty response", + request = request, + ) + } + } + + private fun startAdapter(request: FastCheckExecutionRequest): Process = try { + ProcessBuilder(nodeExecutable, adapterEntryPoint.toString()).start() + } catch (error: IOException) { + throw backendError( + kind = BackendErrorKind.PROCESS_FAILURE, + code = PbtDiagnosticCode.BACKEND_PROCESS_START_FAILED, + message = "Failed to start fast-check adapter: ${error.message}", + request = request, + cause = error, + ) + } + + private suspend fun awaitIo( + task: Deferred, + operation: String, + failureCode: String, + request: FastCheckExecutionRequest, + ): T = try { + task.await() + } catch (error: CancellationException) { + throw error + } catch (error: IOException) { + throw backendError( + kind = BackendErrorKind.PROCESS_FAILURE, + code = failureCode, + message = "Failed while $operation: ${error.message}", + request = request, + cause = error, + ) + } + + private fun decodeResponse( + stdout: String, + request: FastCheckExecutionRequest, + ): FastCheckExecutionWireResponse = try { + PropertyManifestJson.json.decodeFromString(stdout) + } catch (error: IllegalArgumentException) { + throw backendError( + kind = BackendErrorKind.PROTOCOL_ERROR, + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + message = "fast-check adapter returned invalid JSON: ${error.message}", + request = request, + cause = error, + ) + } + + private fun throwNodeDiagnostic( + response: FastCheckExecutionWireResponse, + request: FastCheckExecutionRequest, + ): Nothing { + val diagnostic = response.diagnostics.firstOrNull() + ?: throw invalidResponse( + message = "fast-check error response has no diagnostic", + request = request, + ) + + throw backendError( + kind = diagnostic.kind, + code = diagnostic.code, + message = diagnostic.message, + request = request, + path = diagnostic.path, + ) + } + + private fun decodeSuccessfulResponse( + response: FastCheckExecutionWireResponse, + request: FastCheckExecutionRequest, + ): PropertyRunResult { + if (response.status == "error") throwNodeDiagnostic(response, request) + + if (response.status != "ok") { + throw invalidResponse( + message = "Unknown fast-check response status: ${response.status}", + request = request, + ) + } + + val result = response.result ?: throw invalidResponse( + message = "Successful response has no result", + request = request, + ) + + validateResultIdentity(result, request) + + return result + } + + private fun validateResultIdentity( + result: PropertyRunResult, + request: FastCheckExecutionRequest, + ) { + try { + PropertyId(result.propertyId.value) + } catch (error: IllegalArgumentException) { + throw backendError( + kind = BackendErrorKind.PROTOCOL_ERROR, + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + message = "fast-check result property ID is invalid: ${error.message}", + request = request, + cause = error, + ) + } + + if (result.propertyId.value != request.manifest.propertyId) { + throw invalidResponse( + message = "fast-check result property does not match the request", + request = request, + ) + } + } + + private fun invalidResponse( + message: String, + request: FastCheckExecutionRequest, + ): PbtBackendException = backendError( + kind = BackendErrorKind.PROTOCOL_ERROR, + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, + message = message, + request = request, + ) + + private fun backendError( + kind: BackendErrorKind, + code: String, + message: String, + request: FastCheckExecutionRequest, + path: String? = null, + cause: Throwable? = null, + ) = PbtBackendException( + kind = kind, + code = code, + message = message, + propertyId = request.manifest.propertyId, + path = path, + cause = cause, + ) + + private fun terminate(process: Process) { + process.destroy() + + if (!process.waitFor(shutdownGraceMillis, TimeUnit.MILLISECONDS)) { + process.destroyForcibly() + process.waitFor() + } + } + + private companion object { + const val MAX_REQUEST_BYTES = 4 * 1024 * 1024 + const val MAX_STDOUT_BYTES = 4 * 1024 * 1024 + const val MAX_STDERR_BYTES = 64 * 1024 + const val DEFAULT_TRANSPORT_GRACE_MILLIS = 2_000L + const val DEFAULT_SHUTDOWN_GRACE_MILLIS = 250L + } +} + +private data class BoundedText(val text: String, val exceeded: Boolean) + +private fun InputStream.readBounded(limit: Int): BoundedText { + val output = ByteArrayOutputStream(minOf(limit, DEFAULT_BUFFER_SIZE)) + val buffer = ByteArray(DEFAULT_BUFFER_SIZE) + var exceeded = false + + while (true) { + val read = read(buffer) + if (read < 0) break + + val remaining = limit - output.size() + + if (remaining > 0) output.write(buffer, 0, minOf(read, remaining)) + if (read > remaining) exceeded = true + } + + return BoundedText( + text = output.toString(Charsets.UTF_8), + exceeded = exceeded, + ) +} + +private fun safeAdd(left: Long, right: Long): Long = if (left > Long.MAX_VALUE - right) { + Long.MAX_VALUE +} else { + left + right +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt index 1ce5ce3ac..e40beccc2 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt @@ -2,6 +2,7 @@ package org.usvm.ts.pbt.fastcheck import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString +import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifestJson import java.io.IOException import java.nio.file.Path @@ -15,38 +16,27 @@ import java.util.concurrent.Executors */ class FastCheckProjectionClient( private val nodeExecutable: String = "node", - private val adapterEntryPoint: Path, + private val adapterEntryPoint: Path = FastCheckRuntime.projectionEntryPoint(), ) { /** Projects the requested domains to fast-check and returns the generated samples. */ fun sample(request: FastCheckProjectionRequest): FastCheckProjectionResponse { validateRequest(request) + val response = decodeResponse(invokeAdapter(request)) - validateResponseIdentity(request, response) + throwBackendError(response) validateSuccessfulResponse(request, response) + return FastCheckProjectionResponse( - protocolVersion = response.protocolVersion, - requestId = requireNotNull(response.requestId), samples = response.samples, ) } - private fun validateResponseIdentity( - request: FastCheckProjectionRequest, - response: FastCheckProjectionWireResponse, - ) { - if (response.protocolVersion != FAST_CHECK_PROTOCOL_VERSION || response.requestId != request.requestId) { - throw FastCheckProjectionException( - code = "backend.response.mismatch", - message = "fast-check response identity does not match the request", - ) - } - } - private fun throwBackendError(response: FastCheckProjectionWireResponse) { if (response.status == "error") { val diagnostic = response.diagnostics.firstOrNull() ?: invalidResponse("fast-check error response does not contain a diagnostic") + throw FastCheckProjectionException( code = diagnostic.code, message = diagnostic.message, @@ -59,11 +49,13 @@ class FastCheckProjectionClient( request: FastCheckProjectionRequest, response: FastCheckProjectionWireResponse, ) { - if (response.status != "ok" || response.samples.size != request.numSamples || - response.samples.any { it.size != request.domains.size } - ) { + val hasExpectedStatus = response.status == "ok" + val hasExpectedSampleCount = response.samples.size == request.numSamples + val hasExpectedArity = response.samples.all { it.size == request.domains.size } + + if (!hasExpectedStatus || !hasExpectedSampleCount || !hasExpectedArity) { throw FastCheckProjectionException( - code = "backend.response.invalid", + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, message = "fast-check adapter returned an invalid successful response", ) } @@ -75,25 +67,30 @@ class FastCheckProjectionClient( val stderr = errorReaderExecutor.submit { process.errorStream.bufferedReader(Charsets.UTF_8).use { reader -> reader.readText() } } + try { process.outputStream.bufferedWriter(Charsets.UTF_8).use { writer -> writer.write(PropertyManifestJson.json.encodeToString(request)) } + val stdout = process.inputStream.bufferedReader(Charsets.UTF_8).use { reader -> reader.readText() } val exitCode = process.waitFor() val stderrText = stderr.get() + if (exitCode != 0) { throw FastCheckProjectionException( - code = "backend.process.failed", + code = PbtDiagnosticCode.BACKEND_PROCESS_FAILED, message = "fast-check adapter exited with code $exitCode: ${stderrText.trim()}", ) } + if (stdout.isBlank()) { throw FastCheckProjectionException( - code = "backend.response.empty", + code = PbtDiagnosticCode.BACKEND_RESPONSE_EMPTY, message = "fast-check adapter returned an empty response", ) } + return stdout } finally { errorReaderExecutor.shutdownNow() @@ -104,7 +101,7 @@ class FastCheckProjectionClient( ProcessBuilder(nodeExecutable, adapterEntryPoint.toString()).start() } catch (error: IOException) { throw FastCheckProjectionException( - code = "backend.process.start.failed", + code = PbtDiagnosticCode.BACKEND_PROCESS_START_FAILED, message = "Failed to start fast-check adapter: ${error.message}", cause = error, ) @@ -114,32 +111,27 @@ class FastCheckProjectionClient( PropertyManifestJson.json.decodeFromString(stdout) } catch (error: IllegalArgumentException) { throw FastCheckProjectionException( - code = "backend.response.invalid", + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, message = "fast-check adapter returned invalid JSON: ${error.message}", cause = error, ) } private fun invalidResponse(message: String): Nothing = throw FastCheckProjectionException( - code = "backend.response.invalid", + code = PbtDiagnosticCode.BACKEND_RESPONSE_INVALID, message = message, ) private fun validateRequest(request: FastCheckProjectionRequest) { - val valid = request.requestId.isNotEmpty() && - request.operation == "sample" && - request.numSamples in 1..MAX_SAMPLES && - request.domains.isNotEmpty() - if (!valid) { + val hasValidSampleCount = request.numSamples > 0 + val hasDomains = request.domains.isNotEmpty() + + if (!hasValidSampleCount || !hasDomains) { throw FastCheckProjectionException( - code = "protocol.request.invalid", - message = "Request requires a non-empty ID and domains, operation sample, and numSamples in 1..10000", + code = PbtDiagnosticCode.PROTOCOL_REQUEST_INVALID, + message = "Request requires domains and a positive numSamples", path = "request", ) } } - - private companion object { - const val MAX_SAMPLES = 10_000 - } } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt index 33900a462..2a8f5bab6 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt @@ -4,14 +4,9 @@ import kotlinx.serialization.Serializable import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDomain -const val FAST_CHECK_PROTOCOL_VERSION = 1 - -/** One versioned request sent from Kotlin to the private fast-check adapter process. */ +/** One request sent from Kotlin to the private fast-check adapter process. */ @Serializable data class FastCheckProjectionRequest( - val protocolVersion: Int = FAST_CHECK_PROTOCOL_VERSION, - val requestId: String, - val operation: String = "sample", val seed: Int, val numSamples: Int, val domains: List, @@ -19,15 +14,11 @@ data class FastCheckProjectionRequest( /** Validated samples returned by fast-check in positional input order. */ data class FastCheckProjectionResponse( - val protocolVersion: Int, - val requestId: String, val samples: List>, ) @Serializable internal data class FastCheckProjectionWireResponse( - val protocolVersion: Int, - val requestId: String? = null, val status: String, val samples: List> = emptyList(), val diagnostics: List = emptyList(), @@ -35,6 +26,7 @@ internal data class FastCheckProjectionWireResponse( @Serializable internal data class FastCheckProtocolDiagnostic( + val kind: BackendErrorKind, val code: String, val message: String, val path: String? = null, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt new file mode 100644 index 000000000..32e95af37 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt @@ -0,0 +1,50 @@ +package org.usvm.ts.pbt.fastcheck + +import org.usvm.ts.pbt.PbtDiagnosticCode +import java.nio.file.Files +import java.nio.file.Path + +/** Locates the private fast-check runtime in development and installed distributions. */ +internal object FastCheckRuntime { + fun executionEntryPoint(): Path = locateEntryPoint(EXECUTION_CLI) + + fun projectionEntryPoint(): Path = locateEntryPoint(PROJECTION_CLI) + + private fun locateEntryPoint(fileName: String): Path { + val candidates = runtimeDirectories().map { runtimeDirectory -> + runtimeDirectory.resolve(ENTRY_POINT_DIRECTORY).resolve(fileName) + } + + return candidates.firstOrNull(Files::isRegularFile) + ?: throw PbtBackendException( + kind = BackendErrorKind.INVALID_REQUEST, + code = PbtDiagnosticCode.BACKEND_RUNTIME_NOT_FOUND, + message = "Cannot locate built fast-check adapter; checked $candidates", + ) + } + + private fun runtimeDirectories(): List = listOfNotNull( + configuredRuntimeDirectory(), + installedRuntimeDirectory(), + ).distinct() + + private fun configuredRuntimeDirectory(): Path? = System.getProperty(RUNTIME_DIRECTORY_PROPERTY) + ?.takeIf(String::isNotBlank) + ?.let(Path::of) + ?.toAbsolutePath() + ?.normalize() + + private fun installedRuntimeDirectory(): Path? { + val location = FastCheckRuntime::class.java.protectionDomain.codeSource?.location ?: return null + val codePath = runCatching { Path.of(location.toURI()) }.getOrNull() ?: return null + val libraryDirectory = if (Files.isDirectory(codePath)) codePath else codePath.parent ?: return null + + return libraryDirectory.resolve(INSTALLED_RUNTIME_DIRECTORY) + } + + private const val RUNTIME_DIRECTORY_PROPERTY = "org.usvm.ts.pbt.fastcheck.runtime" + private const val ENTRY_POINT_DIRECTORY = "dist/src" + private const val EXECUTION_CLI = "execution-cli.js" + private const val PROJECTION_CLI = "projection-cli.js" + private const val INSTALLED_RUNTIME_DIRECTORY = "fast-check-adapter" +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt index 26fe1886d..48e52ecbb 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt @@ -11,16 +11,13 @@ import org.usvm.ts.pbt.validation.requireValid import org.usvm.ts.pbt.validation.validatePropertyDefinition import org.usvm.ts.pbt.validation.validatePropertyManifest -const val PROPERTY_MANIFEST_SCHEMA_VERSION = 1 - /** - * Versioned transport representation of a validated [PropertyDefinition]. + * Transport representation of a validated [PropertyDefinition]. * * The manifest is the boundary shared with replaceable concrete PBT adapters and later symbolic projections. */ @Serializable data class PropertyManifest( - val schemaVersion: Int = PROPERTY_MANIFEST_SCHEMA_VERSION, val propertyId: String, val inputs: List, val predicate: TypeScriptEntryPoint, @@ -37,7 +34,7 @@ fun PropertyDefinition.toManifest(): PropertyManifest { ) } -/** Strict JSON codec for versioned property manifests. */ +/** Strict JSON codec for property manifests. */ object PropertyManifestJson { val json = Json { classDiscriminator = "kind" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt index dd53ce094..74384e18c 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt @@ -60,6 +60,7 @@ data class JsNumber( companion object { fun finite(value: Double): JsNumber { require(value.isFinite()) { "Use a tagged representation for non-finite JavaScript numbers" } + return JsNumber( value = JsNumberKind.FINITE, bits = value @@ -107,6 +108,11 @@ sealed interface JsConcreteValue { /** Ordered recursively tagged elements of one concrete JavaScript array. */ data class Array(val elements: List) : JsConcreteValue + + companion object { + /** Creates a lossless tagged value from any ECMAScript binary64 number. */ + fun number(value: Double): Number = Number(JsNumber.fromDouble(value)) + } } /** JSON serializer for the tagged [JsConcreteValue] wire representation. */ @@ -116,6 +122,7 @@ object JsConcreteValueSerializer : KSerializer { override fun serialize(encoder: Encoder, value: JsConcreteValue) { val jsonEncoder = encoder as? JsonEncoder ?: throw SerializationException("JsConcreteValue supports JSON serialization only") + jsonEncoder.encodeJsonElement( buildJsonObject { when (value) { @@ -147,6 +154,7 @@ object JsConcreteValueSerializer : KSerializer { val elements = value.elements.map { element -> jsonEncoder.json.encodeToJsonElement(JsConcreteValueSerializer, element) } + val jsonElements = JsonArray(elements) put("kind", "array") @@ -160,7 +168,9 @@ object JsConcreteValueSerializer : KSerializer { override fun deserialize(decoder: Decoder): JsConcreteValue { val jsonDecoder = decoder as? JsonDecoder ?: throw SerializationException("JsConcreteValue supports JSON deserialization only") + val value = jsonDecoder.decodeJsonElement().jsonObject + return when (val kind = value.requiredString("kind")) { "undefined" -> JsConcreteValue.Undefined "null" -> JsConcreteValue.Null @@ -176,6 +186,7 @@ object JsConcreteValueSerializer : KSerializer { private fun deserializeBoolean(value: JsonObject): JsConcreteValue.Boolean { val booleanValue = value["value"]?.jsonPrimitive?.booleanOrNull ?: throw SerializationException("Boolean JsConcreteValue requires a boolean value") + return JsConcreteValue.Boolean(booleanValue) } @@ -188,6 +199,7 @@ private fun deserializeNumber(value: JsonObject): JsConcreteValue.Number { "negative-infinity" -> JsNumberKind.NEGATIVE_INFINITY else -> throw SerializationException("Unknown JavaScript number kind: $numberKindName") } + val bits = value["bits"]?.jsonPrimitive?.content val number = JsNumber(value = numberKind, bits = bits) @@ -197,6 +209,7 @@ private fun deserializeNumber(value: JsonObject): JsConcreteValue.Number { private fun deserializeArray(jsonDecoder: JsonDecoder, value: JsonObject): JsConcreteValue.Array { val jsonElements = value["elements"]?.jsonArray ?: throw SerializationException("Array JsConcreteValue requires elements") + val elements = jsonElements.map { element -> jsonDecoder.json.decodeFromJsonElement(JsConcreteValueSerializer, element) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt index f7a927077..8ca1bd3c9 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt @@ -70,3 +70,47 @@ data class ArrayDomain( val minLength: Int = 0, val maxLength: Int = DEFAULT_MAX_ARRAY_LENGTH, ) : PropertyDomain + +/** Returns whether [value] belongs to this domain, including recursive tuple and array constraints. */ +operator fun PropertyDomain.contains(value: JsConcreteValue): Boolean = when (this) { + BooleanDomain -> value is JsConcreteValue.Boolean + is IntegerDomain -> value is JsConcreteValue.Number && value.isIntegerIn(this) + is NumberDomain -> value is JsConcreteValue.Number && value.isNumberIn(this) + is StringDomain -> value is JsConcreteValue.String && value.value.length in minLength..maxLength + is ConstantDomain -> value == this.value + is OptionalDomain -> value == nil || value in this.value + is TupleDomain -> + value is JsConcreteValue.Array && + value.elements.size == elements.size && + value.elements.zip(elements).all { (element, domain) -> element in domain } + + is ArrayDomain -> + value is JsConcreteValue.Array && + value.elements.size in minLength..maxLength && + value.elements.all { elementValue -> elementValue in element } +} + +private fun JsConcreteValue.Number.isIntegerIn(domain: IntegerDomain): Boolean { + val value = validDoubleOrNull() ?: return false + + // fc.integer can generate positive zero but never the distinct binary64 value negative zero. + val isGeneratedInteger = value.isFinite() && !value.isNegativeZero() && value % 1.0 == 0.0 + + return isGeneratedInteger && value in domain.min.toDouble()..domain.max.toDouble() +} + +private fun JsConcreteValue.Number.isNumberIn(domain: NumberDomain): Boolean { + if (number.value == JsNumberKind.NAN) return domain.allowNaN + + val value = validDoubleOrNull() ?: return false + val minimum = runCatching(domain.min::toDouble).getOrNull() ?: return false + val maximum = runCatching(domain.max::toDouble).getOrNull() ?: return false + + return value in minimum..maximum +} + +private fun JsConcreteValue.Number.validDoubleOrNull(): Double? = runCatching(::toDouble).getOrNull() + +private fun Double.isNegativeZero(): Boolean = toRawBits() == NEGATIVE_ZERO_BITS + +private val NEGATIVE_ZERO_BITS = Double.fromBits(Long.MIN_VALUE).toRawBits() diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistry.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistry.kt new file mode 100644 index 000000000..4e0a11dde --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistry.kt @@ -0,0 +1,66 @@ +package org.usvm.ts.pbt.registry + +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.validation.requireValid +import org.usvm.ts.pbt.validation.validatePropertyDefinition + +/** Ordered collection of validated Kotlin property definitions with unique stable IDs. */ +class PropertyRegistry(properties: List) { + val properties: List = properties.toList() + + private val propertiesById: Map + + init { + this.properties.forEach { property -> + requireValid(validatePropertyDefinition(property)) + } + + rejectDuplicateIds(this.properties) + + propertiesById = this.properties.associateBy(PropertyDefinition::id) + } + + /** Returns the property identified by [id], or reports all IDs available in this registry. */ + operator fun get(id: PropertyId): PropertyDefinition = propertiesById[id] + ?: throw UnknownPropertyIdException( + propertyId = id, + availablePropertyIds = properties.map(PropertyDefinition::id), + ) + + companion object { + /** Combines registries in input order and validates IDs across registry boundaries. */ + fun combine(registries: List): PropertyRegistry = PropertyRegistry( + registries.flatMap(PropertyRegistry::properties), + ) + } +} + +/** Thrown when the same property ID occurs at multiple registry positions. */ +class DuplicatePropertyIdException( + val propertyId: PropertyId, + val positions: List, +) : IllegalArgumentException( + "Duplicate property ID ${propertyId.value} at positions ${positions.joinToString()}", +) + +/** Thrown when a caller selects a property that is absent from a registry. */ +class UnknownPropertyIdException( + val propertyId: PropertyId, + val availablePropertyIds: List, +) : NoSuchElementException( + "Unknown property ID ${propertyId.value}; available IDs: ${availablePropertyIds.joinToString()}", +) + +private fun rejectDuplicateIds(properties: List) { + val positionsById = properties + .mapIndexed { index, property -> property.id to index } + .groupBy(keySelector = Pair::first, valueTransform = Pair::second) + + val duplicate = positionsById + .filterValues { positions -> positions.size > 1 } + .minByOrNull { (id, _) -> id.value } + ?: return + + throw DuplicatePropertyIdException(duplicate.key, duplicate.value) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryProvider.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryProvider.kt new file mode 100644 index 000000000..a29416cd1 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryProvider.kt @@ -0,0 +1,10 @@ +package org.usvm.ts.pbt.registry + +/** Service-loaded source of one named Kotlin property registry for the command-line runner. */ +interface PropertyRegistryProvider { + /** Stable CLI identifier used to select this registry. */ + val registryId: String + + /** Builds the registry after the provider has been selected. */ + fun load(): PropertyRegistry +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt index 00078b005..aa85b7c48 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt @@ -1,6 +1,6 @@ package org.usvm.ts.pbt.validation -import org.usvm.ts.pbt.manifest.PROPERTY_MANIFEST_SCHEMA_VERSION +import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain @@ -51,21 +51,12 @@ fun validatePropertyDefinition(definition: PropertyDefinition): PropertyValidati ) fun validatePropertyManifest(manifest: PropertyManifest): PropertyValidationResult { - val diagnostics = mutableListOf() - if (manifest.schemaVersion != PROPERTY_MANIFEST_SCHEMA_VERSION) { - diagnostics += diagnostic( - code = "manifest.schema.unsupported", - message = "Unsupported property manifest schema version: ${manifest.schemaVersion}", - path = "schemaVersion", - ) - } - diagnostics += validateProperty( + return validateProperty( propertyId = manifest.propertyId, inputs = manifest.inputs, predicate = manifest.predicate, precondition = manifest.precondition, - ).diagnostics - return diagnostics.toResult() + ) } fun requireValid(result: PropertyValidationResult) { @@ -82,20 +73,36 @@ private fun validateProperty( ): PropertyValidationResult { val diagnostics = mutableListOf() if (!isCanonicalPropertyId(propertyId)) { - diagnostics += diagnostic("property.id.invalid", "Invalid property ID", "propertyId") + diagnostics += diagnostic( + code = PbtDiagnosticCode.PROPERTY_ID_INVALID, + message = "Invalid property ID", + path = "propertyId", + ) } if (inputs.isEmpty()) { - diagnostics += diagnostic("property.inputs.empty", "A property requires at least one input", "inputs") + diagnostics += diagnostic( + code = PbtDiagnosticCode.PROPERTY_INPUTS_EMPTY, + message = "A property requires at least one input", + path = "inputs", + ) } val firstInputByName = mutableMapOf() inputs.forEachIndexed { index, input -> val path = "inputs[$index]" if (!isJavaScriptIdentifier(input.name)) { - diagnostics += diagnostic("input.name.invalid", "Invalid input name", "$path.name") + diagnostics += diagnostic( + code = PbtDiagnosticCode.INPUT_NAME_INVALID, + message = "Invalid input name", + path = "$path.name", + ) } if (firstInputByName.putIfAbsent(input.name, index) != null) { - diagnostics += diagnostic("input.name.duplicate", "Duplicate input name: ${input.name}", path) + diagnostics += diagnostic( + code = PbtDiagnosticCode.INPUT_NAME_DUPLICATE, + message = "Duplicate input name: ${input.name}", + path = path, + ) } validateDomain(input.domain, "$path.domain", diagnostics) } @@ -117,7 +124,11 @@ private fun validateDomain( is IntegerDomain -> { if (domain.min > domain.max) { - diagnostics += diagnostic("domain.integer.bounds", "Integer minimum exceeds maximum", path) + diagnostics += diagnostic( + code = PbtDiagnosticCode.DOMAIN_INTEGER_BOUNDS, + message = "Integer minimum exceeds maximum", + path = path, + ) } } @@ -129,7 +140,7 @@ private fun validateDomain( validateLengths( minLength = domain.minLength, maxLength = domain.maxLength, - code = "domain.string.length", + code = PbtDiagnosticCode.DOMAIN_STRING_LENGTH, description = "String", path = path, diagnostics = diagnostics, @@ -139,9 +150,9 @@ private fun validateDomain( is ConstantDomain -> { if (domain.value is JsConcreteValue.Array) { diagnostics += diagnostic( - "domain.constant.unsupported", - "Constant domains support JavaScript primitives only", - path, + code = PbtDiagnosticCode.DOMAIN_CONSTANT_UNSUPPORTED, + message = "Constant domains support JavaScript primitives only", + path = path, ) } validateJsConcreteValue(domain.value, "$path.value", diagnostics) @@ -149,9 +160,9 @@ private fun validateDomain( is OptionalDomain -> { if (domain.nil != JsConcreteValue.Undefined && domain.nil != JsConcreteValue.Null) { diagnostics += diagnostic( - "domain.optional.nil", - "Optional nil must be null or undefined", - "$path.nil", + code = PbtDiagnosticCode.DOMAIN_OPTIONAL_NIL, + message = "Optional nil must be null or undefined", + path = "$path.nil", ) } validateJsConcreteValue(domain.nil, "$path.nil", diagnostics) @@ -160,7 +171,11 @@ private fun validateDomain( is TupleDomain -> { if (domain.elements.isEmpty()) { - diagnostics += diagnostic("domain.tuple.empty", "Tuple domain must not be empty", path) + diagnostics += diagnostic( + code = PbtDiagnosticCode.DOMAIN_TUPLE_EMPTY, + message = "Tuple domain must not be empty", + path = path, + ) } domain.elements.forEachIndexed { index, element -> validateDomain(element, "$path.elements[$index]", diagnostics) @@ -171,7 +186,7 @@ private fun validateDomain( validateLengths( minLength = domain.minLength, maxLength = domain.maxLength, - code = "domain.array.length", + code = PbtDiagnosticCode.DOMAIN_ARRAY_LENGTH, description = "Array", path = path, diagnostics = diagnostics, @@ -190,10 +205,18 @@ private fun validateNumberDomain( val maximumEncodingIsValid = validateJsNumber(domain.max, "$path.max", diagnostics) if (domain.min.value == JsNumberKind.NAN) { - diagnostics += diagnostic("domain.number.bound.nan", "Number minimum must not be NaN", "$path.min") + diagnostics += diagnostic( + code = PbtDiagnosticCode.DOMAIN_NUMBER_BOUND_NAN, + message = "Number minimum must not be NaN", + path = "$path.min", + ) } if (domain.max.value == JsNumberKind.NAN) { - diagnostics += diagnostic("domain.number.bound.nan", "Number maximum must not be NaN", "$path.max") + diagnostics += diagnostic( + code = PbtDiagnosticCode.DOMAIN_NUMBER_BOUND_NAN, + message = "Number maximum must not be NaN", + path = "$path.max", + ) } val encodingsAreValid = minimumEncodingIsValid && maximumEncodingIsValid @@ -201,15 +224,19 @@ private fun validateNumberDomain( val boundsCanBeCompared = encodingsAreValid && boundsAreNotNaN val minimumExceedsMaximum = boundsCanBeCompared && domain.min.toDouble() > domain.max.toDouble() if (minimumExceedsMaximum) { - diagnostics += diagnostic("domain.number.bounds", "Number minimum exceeds maximum", path) + diagnostics += diagnostic( + code = PbtDiagnosticCode.DOMAIN_NUMBER_BOUNDS, + message = "Number minimum exceeds maximum", + path = path, + ) } val bounded = domain.min != JsNumber.negativeInfinity() || domain.max != JsNumber.positiveInfinity() if (bounded && domain.allowNaN) { diagnostics += diagnostic( - "domain.number.nan-bounded", - "Bounded number domains must exclude NaN", - "$path.allowNaN", + code = PbtDiagnosticCode.DOMAIN_NUMBER_NAN_BOUNDED, + message = "Bounded number domains must exclude NaN", + path = "$path.allowNaN", ) } } @@ -240,9 +267,9 @@ private fun validateJsNumber( } if (!valid) { diagnostics += diagnostic( - "js-number.encoding.invalid", - "Invalid tagged JavaScript number encoding", - path, + code = PbtDiagnosticCode.JS_NUMBER_ENCODING_INVALID, + message = "Invalid tagged JavaScript number encoding", + path = path, ) } return valid @@ -257,7 +284,11 @@ private fun validateLengths( diagnostics: MutableList, ) { if (minLength < 0 || maxLength < 0 || minLength > maxLength) { - diagnostics += diagnostic(code, "$description length bounds are invalid", path) + diagnostics += diagnostic( + code = code, + message = "$description length bounds are invalid", + path = path, + ) } } @@ -267,10 +298,18 @@ private fun validateEntryPoint( diagnostics: MutableList, ) { if (!isProjectRelativePosixPath(entryPoint.module)) { - diagnostics += diagnostic("entrypoint.module.invalid", "Invalid TypeScript module path", "$path.module") + diagnostics += diagnostic( + code = PbtDiagnosticCode.ENTRY_POINT_MODULE_INVALID, + message = "Invalid TypeScript module path", + path = "$path.module", + ) } if (!isJavaScriptIdentifier(entryPoint.exportName)) { - diagnostics += diagnostic("entrypoint.export.invalid", "Invalid TypeScript export name", "$path.exportName") + diagnostics += diagnostic( + code = PbtDiagnosticCode.ENTRY_POINT_EXPORT_INVALID, + message = "Invalid TypeScript export name", + path = "$path.exportName", + ) } } @@ -318,7 +357,11 @@ private fun MutableList.toResult(): PropertyValidationResu return PropertyValidationResult(orderedDiagnostics) } -private fun diagnostic(code: String, message: String, path: String) = ValidationDiagnostic(code, message, path) +private fun diagnostic(code: String, message: String, path: String) = ValidationDiagnostic( + code = code, + message = message, + path = path, +) private val FINITE_NUMBER_BITS_REGEX = Regex("[0-9a-f]{16}") diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt new file mode 100644 index 000000000..82542885a --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/TestResources.kt @@ -0,0 +1,17 @@ +package org.usvm.ts.pbt + +import java.nio.file.Path + +internal fun testResourcePath(name: String): Path { + val resource = requireNotNull(TestResourceMarker::class.java.getResource(name)) { + "Missing test resource: $name" + } + + require(resource.protocol == "file") { "Test resource is not a regular file-system path: $resource" } + + return Path.of(resource.toURI()) +} + +internal fun testResourcesRoot(): Path = requireNotNull(testResourcePath("/properties").parent) + +private object TestResourceMarker diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt index ea1739bf9..41cc31b06 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt @@ -8,17 +8,13 @@ class ProjectionCapabilityTest { @Test fun `least capable nested projection wins and diagnostics are deterministic`() { val capability = aggregateProjectionCapabilities( - backendId = FAST_CHECK_ID, - backendVersion = FAST_CHECK_VERSION, capabilities = listOf( exact(), - approximate("inputs[1].domain", "domain.string.approximate"), - approximate("inputs[0].domain", "domain.number.approximate"), + approximate(path = "inputs[1].domain", code = "domain.string.approximate"), + approximate(path = "inputs[0].domain", code = "domain.number.approximate"), ), ) - assertEquals(FAST_CHECK_ID, capability.backendId) - assertEquals(FAST_CHECK_VERSION, capability.backendVersion) assertEquals(ProjectionLevel.APPROXIMATE, capability.level) assertEquals( listOf("domain.number.approximate", "domain.string.approximate"), @@ -29,11 +25,9 @@ class ProjectionCapabilityTest { @Test fun `unsupported nested projection wins over approximate projection`() { val capability = aggregateProjectionCapabilities( - backendId = FAST_CHECK_ID, - backendVersion = FAST_CHECK_VERSION, capabilities = listOf( - approximate("inputs[0].domain", "domain.number.approximate"), - unsupported("inputs[1].domain", "domain.object.unsupported"), + approximate(path = "inputs[0].domain", code = "domain.number.approximate"), + unsupported(path = "inputs[1].domain", code = "domain.object.unsupported"), ), ) @@ -44,8 +38,6 @@ class ProjectionCapabilityTest { fun `non exact capability requires a diagnostic reason`() { assertFailsWith { ProjectionCapability( - backendId = FAST_CHECK_ID, - backendVersion = FAST_CHECK_VERSION, level = ProjectionLevel.APPROXIMATE, ) } @@ -57,7 +49,7 @@ class ProjectionCapabilityTest { PropertyCapabilityLevel.CONCRETE_ONLY, classifyPropertyCapability( concrete = exact(), - symbolic = unsupported("predicate", "entrypoint.async", backendId = "usvm"), + symbolic = unsupported(path = "predicate", code = "entrypoint.async"), ), ) } @@ -66,54 +58,55 @@ class ProjectionCapabilityTest { fun `property classification accounts for both projections`() { assertEquals( PropertyCapabilityLevel.EXACT, - classifyPropertyCapability(exact(), exact(backendId = "usvm")), + classifyPropertyCapability(exact(), exact()), ) + assertEquals( PropertyCapabilityLevel.APPROXIMATE, classifyPropertyCapability( exact(), - approximate("inputs[0].domain", "domain.approximate", backendId = "usvm"), + approximate(path = "inputs[0].domain", code = "domain.approximate"), ), ) + assertEquals( PropertyCapabilityLevel.UNSUPPORTED, classifyPropertyCapability( - unsupported("inputs[0].domain", "domain.unsupported"), - exact(backendId = "usvm"), + unsupported(path = "inputs[0].domain", code = "domain.unsupported"), + exact(), ), ) } - private fun exact(backendId: String = FAST_CHECK_ID) = ProjectionCapability( - backendId = backendId, - backendVersion = FAST_CHECK_VERSION, + private fun exact() = ProjectionCapability( level = ProjectionLevel.EXACT, ) private fun approximate( path: String, code: String, - backendId: String = FAST_CHECK_ID, ) = ProjectionCapability( - backendId = backendId, - backendVersion = FAST_CHECK_VERSION, level = ProjectionLevel.APPROXIMATE, - diagnostics = listOf(CapabilityDiagnostic(code, "Approximate projection", path)), + diagnostics = listOf( + CapabilityDiagnostic( + code = code, + message = "Approximate projection", + path = path, + ), + ), ) private fun unsupported( path: String, code: String, - backendId: String = FAST_CHECK_ID, ) = ProjectionCapability( - backendId = backendId, - backendVersion = FAST_CHECK_VERSION, level = ProjectionLevel.UNSUPPORTED, - diagnostics = listOf(CapabilityDiagnostic(code, "Unsupported projection", path)), + diagnostics = listOf( + CapabilityDiagnostic( + code = code, + message = "Unsupported projection", + path = path, + ), + ), ) - - private companion object { - const val FAST_CHECK_ID = "fast-check" - const val FAST_CHECK_VERSION = "4.9.0" - } } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt new file mode 100644 index 000000000..7e17af5bf --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackendTest.kt @@ -0,0 +1,102 @@ +package org.usvm.ts.pbt.backend + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class PropertyBasedTestingBackendTest { + @Test + fun `configuration rejects non-positive run counts and timeouts`() { + assertFailsWith { + PropertyRunConfiguration(numRuns = 0) + } + + assertFailsWith { + PropertyRunConfiguration(timeoutMillis = 0) + } + + assertFailsWith { + PropertyRunConfiguration(timeoutMillis = Int.MAX_VALUE.toLong() + 1) + } + } + + @Test + fun `configuration has no arbitrary run or one-day timeout cap`() { + val configuration = PropertyRunConfiguration( + numRuns = 10_001, + timeoutMillis = 86_400_001, + ) + + assertEquals(10_001, configuration.numRuns) + assertEquals(86_400_001, configuration.timeoutMillis) + } + + @Test + fun `configuration retains tagged positional examples`() { + val examples = listOf( + listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Undefined), + ) + + val configuration = PropertyRunConfiguration( + seed = 42, + replayPath = "1:0", + numRuns = 25, + timeoutMillis = 1_000, + examples = examples, + ) + + assertEquals(examples, configuration.examples) + } + + @Test + fun `success result rejects failure-only fields`() { + assertFailsWith { + successfulResult().copy( + counterexample = listOf(JsConcreteValue.Boolean(false)), + ) + } + + assertFailsWith { + successfulResult().copy( + failure = PropertyFailureDetails( + kind = PropertyFailureKind.PROPERTY, + errorName = "Error", + message = "predicate returned false", + ), + ) + } + } + + @Test + fun `failure result requires failure details`() { + assertFailsWith { + successfulResult().copy(status = PropertyRunStatus.FAILURE) + } + } + + @Test + fun `result rejects negative counters and execution time`() { + assertFailsWith { + successfulResult().copy(numShrinks = -1) + } + + assertFailsWith { + successfulResult().copy(executionTimeMillis = -1) + } + } + + private fun successfulResult() = PropertyRunResult( + propertyId = PropertyId("example.property"), + status = PropertyRunStatus.SUCCESS, + seed = 42, + replayPath = null, + counterexample = null, + numRuns = 100, + numSkips = 0, + numShrinks = 0, + failure = null, + executionTimeMillis = 10, + ) +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt new file mode 100644 index 000000000..dd5a057f3 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/FastCheckCliTest.kt @@ -0,0 +1,345 @@ +package org.usvm.ts.pbt.cli + +import kotlinx.serialization.json.jsonArray +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend +import org.usvm.ts.pbt.backend.PropertyFailureDetails +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.registry.PropertyRegistry +import org.usvm.ts.pbt.registry.PropertyRegistryProvider +import org.usvm.ts.pbt.testResourcesRoot +import java.net.URLClassLoader +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.assertContains +import kotlin.test.assertEquals + +class FastCheckCliTest { + @Test + fun `help describes options declared by the CLI parser`() { + val output = StringBuilder() + val errors = StringBuilder() + + val exitCode = cli( + providers = listOf(provider(registryId = "examples", propertyIds = arrayOf("property"))), + output = output, + errors = errors, + ).run(arrayOf("--help")) + + assertEquals(0, exitCode) + assertEquals("", errors.toString()) + assertContains(output, "TypeScript source root") + assertContains(output, "--examples") + } + + @Test + fun `selects one property and writes a structured success result`() { + val output = StringBuilder() + val errors = StringBuilder() + val cli = cli( + providers = listOf( + provider(registryId = "examples", propertyIds = arrayOf("second", "first")), + ), + output = output, + errors = errors, + ) + + val exitCode = cli.run( + arrayOf( + "--source-root", sourceRoot.toString(), + "--registry", "examples", + "--property", "first", + "--seed", "42", + "--num-runs", "7", + ), + ) + + val results = PropertyManifestJson.json.parseToJsonElement(output.toString()).jsonArray + val result = results.single().jsonObject + + assertEquals(0, exitCode) + assertEquals("", errors.toString()) + assertEquals(1, results.size) + assertEquals("first", result.getValue("propertyId").jsonPrimitive.content) + assertEquals("success", result.getValue("status").jsonPrimitive.content) + } + + @Test + fun `accepts run controls above the former policy caps`() { + val output = StringBuilder() + + val exitCode = cli( + providers = listOf(provider(registryId = "examples", propertyIds = arrayOf("property"))), + output = output, + ).run( + arrayOf( + "--source-root", + sourceRoot.toString(), + "--num-runs", + "10001", + "--timeout-ms", + "86400001", + ), + ) + + assertEquals(0, exitCode) + } + + @Test + fun `runs selected registries in deterministic order and returns one for a property failure`() { + val output = StringBuilder() + val cli = cli( + providers = listOf( + provider(registryId = "z-registry", propertyIds = arrayOf("z-property")), + provider(registryId = "a-registry", propertyIds = arrayOf("passing", "failing")), + ), + output = output, + failures = setOf(PropertyId("failing")), + ) + + val exitCode = cli.run( + arrayOf( + "--source-root", + sourceRoot.toString(), + "--registry", + "a-registry", + ), + ) + + val propertyIds = PropertyManifestJson.json.parseToJsonElement(output.toString()) + .jsonArray + .map { result -> result.jsonObject.getValue("propertyId").jsonPrimitive.content } + + assertEquals(1, exitCode) + assertEquals(listOf("passing", "failing"), propertyIds) + } + + @Test + fun `reports unknown registries and duplicate property ids as CLI errors`() { + val unknownErrors = StringBuilder() + + val unknownExit = cli( + providers = listOf(provider(registryId = "known", propertyIds = arrayOf("property"))), + errors = unknownErrors, + ).run( + arrayOf( + "--source-root", + sourceRoot.toString(), + "--registry", + "missing", + ), + ) + + assertEquals(2, unknownExit) + assertEquals("cli.registry.unknown", diagnosticCode(unknownErrors)) + + val duplicateErrors = StringBuilder() + + val duplicateExit = cli( + providers = listOf( + provider(registryId = "first-registry", propertyIds = arrayOf("shared")), + provider(registryId = "second-registry", propertyIds = arrayOf("shared")), + ), + errors = duplicateErrors, + ).run(arrayOf("--source-root", sourceRoot.toString())) + + assertEquals(2, duplicateExit) + assertEquals("registry.property-id.duplicate", diagnosticCode(duplicateErrors)) + } + + @Test + fun `requires source roots and a single property for replay controls`() { + val missingRootErrors = StringBuilder() + + val missingRootExit = cli( + providers = listOf(provider(registryId = "examples", propertyIds = arrayOf("property"))), + errors = missingRootErrors, + ).run(emptyArray()) + + assertEquals(2, missingRootExit) + assertEquals("cli.source-root.required", diagnosticCode(missingRootErrors)) + + val replayErrors = StringBuilder() + + val replayExit = cli( + providers = listOf( + provider(registryId = "examples", propertyIds = arrayOf("first", "second")), + ), + errors = replayErrors, + ).run( + arrayOf( + "--source-root", + sourceRoot.toString(), + "--path", + "1:0", + ), + ) + + assertEquals(2, replayExit) + assertEquals("cli.single-property.required", diagnosticCode(replayErrors)) + } + + @Test + fun `reports service loading failures as CLI errors`() { + val serviceRoot = Files.createTempDirectory("usvm-invalid-property-service-") + val serviceFile = serviceRoot.resolve( + "META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider", + ) + + Files.createDirectories(serviceFile.parent) + Files.writeString(serviceFile, "missing.InvalidPropertyRegistryProvider\n") + + val errors = StringBuilder() + val thread = Thread.currentThread() + val previousClassLoader = thread.contextClassLoader + + try { + URLClassLoader(arrayOf(serviceRoot.toUri().toURL()), previousClassLoader).use { classLoader -> + thread.contextClassLoader = classLoader + + val exitCode = runCatching { + FastCheckCli(errors = errors).run( + arrayOf("--source-root", sourceRoot.toString()), + ) + }.getOrNull() + + assertEquals(2, exitCode) + assertEquals("registry.provider.load.failed", diagnosticCode(errors)) + } + } finally { + thread.contextClassLoader = previousClassLoader + serviceRoot.toFile().deleteRecursively() + } + } + + @Test + fun `reports provider failures as CLI errors`() { + val errors = StringBuilder() + val failingProvider = object : PropertyRegistryProvider { + override val registryId: String = "failing" + + override fun load(): PropertyRegistry = error("provider failed") + } + + val exitCode = runCatching { + cli( + providers = listOf(failingProvider), + errors = errors, + ).run(arrayOf("--source-root", sourceRoot.toString())) + }.getOrNull() + + assertEquals(2, exitCode) + assertEquals("registry.provider.load.failed", diagnosticCode(errors)) + } + + @Test + fun `reports provider identity and linkage failures as CLI errors`() { + val invalidProviders = listOf( + object : PropertyRegistryProvider { + override val registryId: String + get() = error("registry ID failed") + + override fun load(): PropertyRegistry = error("unreachable") + }, + object : PropertyRegistryProvider { + override val registryId: String = "missing-dependency" + + override fun load(): PropertyRegistry = throw NoClassDefFoundError("provider dependency") + }, + ) + + invalidProviders.forEach { provider -> + val errors = StringBuilder() + + val exitCode = runCatching { + cli( + providers = listOf(provider), + errors = errors, + ).run(arrayOf("--source-root", sourceRoot.toString())) + }.getOrNull() + + assertEquals(2, exitCode) + assertEquals("registry.provider.load.failed", diagnosticCode(errors)) + } + } + + private fun cli( + providers: List, + output: Appendable = StringBuilder(), + errors: Appendable = StringBuilder(), + failures: Set = emptySet(), + ) = FastCheckCli( + providers = providers, + backendFactory = { FakeBackend(failures) }, + output = output, + errors = errors, + ) + + private fun provider(registryId: String, vararg propertyIds: String) = object : PropertyRegistryProvider { + override val registryId: String = registryId + + override fun load(): PropertyRegistry = PropertyRegistry(propertyIds.map(::property)) + } + + private fun property(id: String) = PropertyDefinition( + id = PropertyId(id), + inputs = listOf(PropertyInput(name = "value", domain = BooleanDomain)), + predicate = TypeScriptEntryPoint( + module = "properties.ts", + exportName = "predicate", + ), + ) + + private fun diagnosticCode(errors: StringBuilder): String = PropertyManifestJson.json + .parseToJsonElement(errors.toString()) + .jsonObject + .getValue("code") + .jsonPrimitive + .content + + private class FakeBackend(private val failures: Set) : PropertyBasedTestingBackend { + override fun run( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + ): PropertyRunResult { + val failed = property.id in failures + + return PropertyRunResult( + propertyId = property.id, + status = if (failed) PropertyRunStatus.FAILURE else PropertyRunStatus.SUCCESS, + seed = configuration.seed ?: 123, + replayPath = if (failed) "0" else null, + counterexample = if (failed) listOf(JsConcreteValue.Boolean(false)) else null, + numRuns = configuration.numRuns, + numSkips = 0, + numShrinks = if (failed) 1 else 0, + failure = if (failed) { + PropertyFailureDetails( + kind = PropertyFailureKind.PROPERTY, + errorName = "PropertyFailure", + message = "predicate returned false", + ) + } else { + null + }, + executionTimeMillis = 1, + ) + } + } + + private companion object { + val sourceRoot: Path = testResourcesRoot() + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt new file mode 100644 index 000000000..9eaad1836 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/cli/InstalledDistributionRegistryProvider.kt @@ -0,0 +1,31 @@ +package org.usvm.ts.pbt.cli + +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.registry.PropertyRegistry +import org.usvm.ts.pbt.registry.PropertyRegistryProvider + +class InstalledDistributionRegistryProvider : PropertyRegistryProvider { + override val registryId: String = "distribution-fixture" + + override fun load(): PropertyRegistry = PropertyRegistry( + listOf( + PropertyDefinition( + id = PropertyId("distribution.always-true"), + inputs = listOf( + PropertyInput( + name = "value", + domain = IntegerDomain(min = -10, max = 10), + ), + ), + predicate = TypeScriptEntryPoint( + module = "properties/execution/ExecutionProperties.ts", + exportName = "alwaysTrue", + ), + ), + ), + ) +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt index e4493515a..88cfa2756 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt @@ -12,9 +12,6 @@ import org.usvm.ts.pbt.model.PropertyId import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.TypeScriptEntryPoint import org.usvm.ts.pbt.validation.validatePropertyDefinition -import java.nio.file.Files -import java.nio.file.Path -import kotlin.io.path.absolute import kotlin.test.assertEquals import kotlin.test.assertNotNull import kotlin.test.assertTrue @@ -23,21 +20,24 @@ class ExamplePropertiesTest { @Test fun `four Kotlin property shapes validate serialize and project through fast-check`() { assertNotNull(javaClass.getResource("/properties/examples/PropertyExamples.ts")) - val client = FastCheckProjectionClient(adapterEntryPoint = adapterEntryPoint()) - examples.forEachIndexed { index, definition -> + val client = FastCheckProjectionClient() + + examples.forEach { definition -> assertTrue(validatePropertyDefinition(definition).isValid, definition.id.value) + val manifest = definition.toManifest() + assertEquals(manifest, PropertyManifestJson.decode(PropertyManifestJson.encode(manifest))) val response = client.sample( FastCheckProjectionRequest( - requestId = "example-$index", seed = 42, numSamples = 5, domains = definition.inputs.map(PropertyInput::domain), ), ) + assertEquals(5, response.samples.size) assertTrue(response.samples.all { it.size == definition.inputs.size }) } @@ -77,14 +77,5 @@ class ExamplePropertiesTest { predicate = TypeScriptEntryPoint(MODULE, "reverseTwicePreservesValues"), ), ) - - fun adapterEntryPoint(): Path { - val candidates = listOf( - Path.of("fast-check-adapter/dist/src/projection-cli.js"), - Path.of("usvm-ts-pbt/fast-check-adapter/dist/src/projection-cli.js"), - ).map { it.absolute() } - return candidates.singleOrNull(Files::isRegularFile) - ?: error("Cannot locate fast-check adapter; checked $candidates") - } } } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt new file mode 100644 index 000000000..c618870e7 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackendTest.kt @@ -0,0 +1,270 @@ +package org.usvm.ts.pbt.fastcheck + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.JsNumber +import org.usvm.ts.pbt.model.JsNumberKind +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class FastCheckBackendTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + @Test + fun `executes TypeScript source without a user compilation step`() { + val result = backend.run( + property = property(predicate = "alwaysTrue"), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(20, result.numRuns) + } + + @Test + fun `passes multiple generated inputs to the predicate in declaration order`() { + val definition = property( + predicate = "sumIsCommutative", + domains = listOf( + IntegerDomain(min = -100, max = 100), + IntegerDomain(min = -100, max = 100), + ), + ) + + val result = backend.run(definition, configuration) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + } + + @Test + fun `replays a failing property from its reported seed and path`() { + val first = backend.run( + property = property(predicate = "isNegative"), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.FAILURE, first.status) + assertEquals(PropertyFailureKind.PROPERTY, first.failure?.kind) + assertNotNull(first.counterexample) + val replayPath = assertNotNull(first.replayPath) + + val replay = backend.run( + property = property(predicate = "isNegative"), + configuration = configuration.copy(seed = first.seed, replayPath = replayPath), + ) + + assertEquals(first.counterexample, replay.counterexample) + assertEquals(first.replayPath, replay.replayPath) + } + + @Test + fun `supports asynchronous predicates and preconditions`() { + val definition = property( + predicate = "asyncAlwaysTrue", + predicateKind = ExecutionKind.ASYNC, + precondition = TypeScriptEntryPoint( + module = MODULE, + exportName = "asyncIsOne", + executionKind = ExecutionKind.ASYNC, + ), + domain = IntegerDomain(min = 0, max = 1), + ) + + val result = backend.run(definition, configuration) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertTrue(result.numSkips > 0) + } + + @Test + fun `explicit examples use the normal predicate and shrinking lifecycle`() { + val seven = JsConcreteValue.number(7.0) + + val result = backend.run( + property = property( + predicate = "isNotSeven", + domain = IntegerDomain(min = 0, max = 100), + ), + configuration = configuration.copy(examples = listOf(listOf(seven))), + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(listOf(seven), result.counterexample) + } + + @Test + fun `asynchronous timeout is a structured failure`() { + val result = backend.run( + property = property(predicate = "neverCompletes", predicateKind = ExecutionKind.ASYNC), + configuration = configuration.copy(numRuns = 1, timeoutMillis = 20), + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.TIMEOUT, result.failure?.kind) + } + + @Test + fun `missing entry point is a typed backend error`() { + val error = assertFailsWith { + backend.run( + property = property(predicate = "alwaysTrue").copy( + predicate = TypeScriptEntryPoint( + module = "missing.ts", + exportName = "predicate", + ), + ), + configuration = configuration, + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals("entrypoint.module.not-found", error.code) + } + + @Test + fun `run and timeout controls are not capped by arbitrary policy limits`() { + val error = assertFailsWith { + backend.run( + property = property(predicate = "alwaysTrue").copy( + predicate = TypeScriptEntryPoint( + module = "missing.ts", + exportName = "predicate", + ), + ), + configuration = configuration.copy( + numRuns = 10_001, + timeoutMillis = 86_400_001, + ), + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals("entrypoint.module.not-found", error.code) + } + + @Test + fun `invalid explicit examples are rejected before Node starts`() { + val missingNodeBackend = FastCheckBackend( + sourceRoots = listOf(testResourcesRoot()), + nodeExecutable = "definitely-not-a-node-executable", + ) + + val error = assertFailsWith { + missingNodeBackend.run( + property = property(predicate = "alwaysTrue"), + configuration = configuration.copy(examples = listOf(emptyList())), + ) + } + + assertEquals(BackendErrorKind.INVALID_REQUEST, error.kind) + assertEquals("backend.examples.arity", error.code) + + val invalidNumber = JsConcreteValue.Number( + JsNumber(value = JsNumberKind.FINITE, bits = "invalid"), + ) + val encodingError = assertFailsWith { + missingNodeBackend.run( + property = property(predicate = "alwaysTrue"), + configuration = configuration.copy(examples = listOf(listOf(invalidNumber))), + ) + } + + assertEquals(BackendErrorKind.INVALID_REQUEST, encodingError.kind) + assertEquals("backend.examples.value.invalid", encodingError.code) + assertEquals("examples[0][0]", encodingError.path) + } + + @Test + fun `explicit examples outside recursive domains are rejected before Node starts`() { + val missingNodeBackend = FastCheckBackend( + sourceRoots = listOf(testResourcesRoot()), + nodeExecutable = "definitely-not-a-node-executable", + ) + val definition = property( + predicate = "alwaysTrue", + domain = ArrayDomain( + element = IntegerDomain(min = 0, max = 1), + minLength = 1, + maxLength = 1, + ), + ) + val outOfRangeElement = JsConcreteValue.Array( + elements = listOf(JsConcreteValue.number(2.0)), + ) + + val error = assertFailsWith { + missingNodeBackend.run( + property = definition, + configuration = configuration.copy(examples = listOf(listOf(outOfRangeElement))), + ) + } + + assertEquals(BackendErrorKind.INVALID_REQUEST, error.kind) + assertEquals("backend.examples.domain", error.code) + assertEquals("examples[0][0]", error.path) + } + + @Test + fun `negative zero is rejected for integer domains before Node starts`() { + val missingNodeBackend = FastCheckBackend( + sourceRoots = listOf(testResourcesRoot()), + nodeExecutable = "definitely-not-a-node-executable", + ) + + val error = assertFailsWith { + missingNodeBackend.run( + property = property(predicate = "alwaysTrue"), + configuration = configuration.copy( + examples = listOf(listOf(JsConcreteValue.number(-0.0))), + ), + ) + } + + assertEquals(BackendErrorKind.INVALID_REQUEST, error.kind) + assertEquals("backend.examples.domain", error.code) + assertEquals("examples[0][0]", error.path) + } + + private fun property( + predicate: String, + predicateKind: ExecutionKind = ExecutionKind.SYNC, + precondition: TypeScriptEntryPoint? = null, + domain: PropertyDomain = IntegerDomain(min = -10, max = 10), + domains: List = listOf(domain), + ) = PropertyDefinition( + id = PropertyId("example.$predicate"), + inputs = domains.mapIndexed { index, inputDomain -> + PropertyInput(name = "argument$index", domain = inputDomain) + }, + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = predicate, + executionKind = predicateKind, + ), + precondition = precondition, + ) + + private companion object { + const val MODULE = "properties/execution/ExecutionProperties.ts" + + val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 20, + timeoutMillis = 1_000, + ) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt new file mode 100644 index 000000000..60704169d --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt @@ -0,0 +1,156 @@ +package org.usvm.ts.pbt.fastcheck + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Path +import kotlin.io.path.createTempFile +import kotlin.io.path.deleteIfExists +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class FastCheckProcessClientTest { + @Test + fun `process startup failure is typed`() { + val startup = assertFailsWith { + FastCheckProcessClient( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = Path.of("missing-adapter.mjs"), + ).check(validRequest) + } + + assertEquals(BackendErrorKind.PROCESS_FAILURE, startup.kind) + assertEquals("backend.process.start.failed", startup.code) + } + + @Test + fun `non-zero exit retains stderr`() { + withTemporaryAdapter(source = "process.stderr.write('adapter failed'); process.exit(3)") { client -> + val exit = assertFailsWith { client.check(validRequest) } + + assertEquals(BackendErrorKind.PROCESS_FAILURE, exit.kind) + assertEquals("backend.process.failed", exit.code) + assertTrue(exit.message.orEmpty().contains("adapter failed")) + } + } + + @Test + fun `empty malformed and unknown responses are protocol errors`() { + val cases = listOf( + InvalidResponseCase(script = "", expectedCode = "backend.response.empty"), + InvalidResponseCase( + script = "process.stdout.write('not-json')", + expectedCode = "backend.response.invalid", + ), + InvalidResponseCase( + script = """ + process.stdout.write(JSON.stringify({ + status: 'unknown' + })) + """.trimIndent(), + expectedCode = "backend.response.invalid", + ), + ) + + cases.forEach { case -> + withTemporaryAdapter(source = case.script) { client -> + val error = assertFailsWith { client.check(validRequest) } + + assertEquals(BackendErrorKind.PROTOCOL_ERROR, error.kind) + assertEquals(case.expectedCode, error.code) + } + } + } + + @Test + fun `Node diagnostic category does not depend on code naming`() { + withTemporaryAdapter( + source = """ + process.stdout.write(JSON.stringify({ + status: 'error', + diagnostics: [{ + kind: 'entry-point', + code: 'adapter.module.failure', + message: 'module missing', + path: 'manifest.predicate.module' + }] + })) + """.trimIndent(), + ) { client -> + val error = assertFailsWith { client.check(validRequest) } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals("adapter.module.failure", error.code) + assertEquals("manifest.predicate.module", error.path) + } + } + + @Test + fun `hard timeout terminates a stuck Node process`() { + withTemporaryAdapter( + source = "setInterval(() => undefined, 1000)", + transportGraceMillis = 25, + ) { client -> + val startedAt = System.nanoTime() + val error = assertFailsWith { + client.check(validRequest.copy(timeoutMillis = 25)) + } + val elapsedMillis = (System.nanoTime() - startedAt) / 1_000_000 + + assertEquals(BackendErrorKind.TIMEOUT, error.kind) + assertEquals("backend.process.timeout", error.code) + assertTrue(elapsedMillis < 2_000, "Process timeout took $elapsedMillis ms") + } + } + + private fun withTemporaryAdapter( + source: String, + transportGraceMillis: Long = 2_000, + block: (FastCheckProcessClient) -> Unit, + ) { + val script = createTempFile(prefix = "fast-check-execution-", suffix = ".mjs") + + try { + script.writeText(source) + block( + FastCheckProcessClient( + adapterEntryPoint = script, + transportGraceMillis = transportGraceMillis, + ), + ) + } finally { + script.deleteIfExists() + } + } + + private companion object { + data class InvalidResponseCase( + val script: String, + val expectedCode: String, + ) + + val property = PropertyDefinition( + id = PropertyId("example.property"), + inputs = listOf(PropertyInput(name = "value", domain = BooleanDomain)), + predicate = TypeScriptEntryPoint( + module = "property.ts", + exportName = "predicate", + ), + ) + + val validRequest = FastCheckExecutionRequest( + manifest = property.toManifest(), + sourceRoots = listOf(testResourcesRoot().toString()), + seed = 42, + numRuns = 10, + timeoutMillis = 1_000, + ) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt index e40130316..6b3469e0f 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt @@ -6,9 +6,7 @@ import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDomain -import java.nio.file.Files import java.nio.file.Path -import kotlin.io.path.absolute import kotlin.io.path.createTempFile import kotlin.io.path.deleteIfExists import kotlin.io.path.writeText @@ -17,12 +15,11 @@ import kotlin.test.assertFailsWith import kotlin.test.assertTrue class FastCheckProjectionClientTest { - private val client = FastCheckProjectionClient(adapterEntryPoint = adapterEntryPoint()) + private val client = FastCheckProjectionClient() @Test fun `Kotlin domains produce deterministic tagged fast-check samples`() { val request = FastCheckProjectionRequest( - requestId = "integration-1", seed = 42, numSamples = 20, domains = listOf(IntegerDomain(-10, 10), ArrayDomain(BooleanDomain, 0, 3)), @@ -32,22 +29,10 @@ class FastCheckProjectionClientTest { val second = client.sample(request) assertEquals(first, second) - assertEquals(FAST_CHECK_PROTOCOL_VERSION, first.protocolVersion) - assertEquals("integration-1", first.requestId) assertEquals(20, first.samples.size) first.samples.forEach { sample -> assertConforms(sample, request.domains) } } - @Test - fun `protocol version mismatch is a typed backend error`() { - val error = assertFailsWith { - client.sample(validRequest.copy(protocolVersion = 999)) - } - - assertEquals("protocol.version.unsupported", error.code) - assertEquals("protocolVersion", error.path) - } - @Test fun `invalid request is rejected before starting Node`() { val missingAdapterClient = FastCheckProjectionClient( @@ -67,9 +52,9 @@ class FastCheckProjectionClientTest { val startup = assertFailsWith { FastCheckProjectionClient( nodeExecutable = "definitely-not-a-node-executable", - adapterEntryPoint = adapterEntryPoint(), ).sample(validRequest) } + assertEquals("backend.process.start.failed", startup.code) val exit = assertFailsWith { @@ -77,6 +62,7 @@ class FastCheckProjectionClientTest { adapterEntryPoint = Path.of("missing-adapter.mjs"), ).sample(validRequest) } + assertEquals("backend.process.failed", exit.code) } @@ -86,6 +72,7 @@ class FastCheckProjectionClientTest { val malformed = assertFailsWith { temporaryClient.sample(validRequest) } + assertEquals("backend.response.invalid", malformed.code) } @@ -93,26 +80,8 @@ class FastCheckProjectionClientTest { val empty = assertFailsWith { temporaryClient.sample(validRequest) } - assertEquals("backend.response.empty", empty.code) - } - } - @Test - fun `response identity mismatch is rejected`() { - withTemporaryAdapter( - """ - process.stdout.write(JSON.stringify({ - protocolVersion: 1, - requestId: 'different-request', - status: 'ok', - samples: [] - })) - """.trimIndent(), - ) { temporaryClient -> - val error = assertFailsWith { - temporaryClient.sample(validRequest) - } - assertEquals("backend.response.mismatch", error.code) + assertEquals("backend.response.empty", empty.code) } } @@ -124,8 +93,6 @@ class FastCheckProjectionClientTest { process.stderr.write('x'.repeat(1024 * 1024), () => { clearTimeout(timeout) process.stdout.write(JSON.stringify({ - protocolVersion: 1, - requestId: 'valid-request', status: 'ok', samples: [[{ kind: 'boolean', value: true }]] })) @@ -143,11 +110,15 @@ class FastCheckProjectionClientTest { private fun assertConforms(values: List, domains: List) { assertEquals(domains.size, values.size) + values.zip(domains).forEach { (value, domain) -> when (domain) { is IntegerDomain -> { val number = (value as JsConcreteValue.Number).toDouble() - assertTrue(number % 1.0 == 0.0 && number >= domain.min && number <= domain.max) + val isInteger = number % 1.0 == 0.0 + val isWithinBounds = number >= domain.min && number <= domain.max + + assertTrue(isInteger && isWithinBounds) } is ArrayDomain -> { @@ -169,6 +140,7 @@ class FastCheckProjectionClientTest { private fun withTemporaryAdapter(source: String, block: (FastCheckProjectionClient) -> Unit) { val script = createTempFile(prefix = "fast-check-adapter-", suffix = ".mjs") + try { script.writeText(source) block(FastCheckProjectionClient(adapterEntryPoint = script)) @@ -179,19 +151,9 @@ class FastCheckProjectionClientTest { private companion object { val validRequest = FastCheckProjectionRequest( - requestId = "valid-request", seed = 42, numSamples = 1, domains = listOf(BooleanDomain), ) - - fun adapterEntryPoint(): Path { - val candidates = listOf( - Path.of("fast-check-adapter/dist/src/projection-cli.js"), - Path.of("usvm-ts-pbt/fast-check-adapter/dist/src/projection-cli.js"), - ).map { it.absolute() } - return candidates.singleOrNull(Files::isRegularFile) - ?: error("Cannot locate fast-check adapter; checked $candidates") - } } } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt index 20bf0bbbe..78cde2160 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt @@ -31,7 +31,7 @@ class PropertyManifestTest { } @Test - fun `manifest serializes resolved integer bounds and schema version`() { + fun `manifest serializes resolved integer bounds`() { val definition = PropertyDefinition( id = PropertyId("integer.defaults"), inputs = listOf(PropertyInput("value", IntegerDomain())), @@ -41,7 +41,7 @@ class PropertyManifestTest { val encoded = PropertyManifestJson.encode(definition.toManifest()) assertEquals( - """{"schemaVersion":1,"propertyId":"integer.defaults","inputs":[""" + + """{"propertyId":"integer.defaults","inputs":[""" + """{"name":"value","domain":{"kind":"integer","min":-2147483648,"max":2147483647}}],""" + """"predicate":{"module":"properties/integer.ts","exportName":"holds","executionKind":"sync"}}""", encoded, diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt index 9186a9193..e80f23a99 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt @@ -6,6 +6,13 @@ import org.usvm.ts.pbt.manifest.PropertyManifestJson import kotlin.test.assertEquals class JsConcreteValueTest { + @Test + fun `number factory creates a lossless concrete value`() { + val value = JsConcreteValue.number(-0.0) + + assertEquals((-0.0).toRawBits(), value.toDouble().toRawBits()) + } + @Test fun `special JavaScript numbers keep their semantics through JSON`() { val values = listOf( @@ -18,10 +25,12 @@ class JsConcreteValueTest { values.forEach { value -> val encoded = PropertyManifestJson.json.encodeToString(value) val decoded = PropertyManifestJson.json.decodeFromString(encoded) + assertEquals(value, decoded) } val negativeZero = values.first() as JsConcreteValue.Number + assertEquals((-0.0).toRawBits(), negativeZero.toDouble().toRawBits()) } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt new file mode 100644 index 000000000..114a3c77e --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt @@ -0,0 +1,47 @@ +package org.usvm.ts.pbt.model + +import org.junit.jupiter.api.Test +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class PropertyDomainTest { + @Test + fun `integer membership matches values produced by fast-check integer`() { + val domain = IntegerDomain(min = -1, max = 1) + + assertTrue(JsConcreteValue.number(-1.0) in domain) + assertTrue(JsConcreteValue.number(0.0) in domain) + assertTrue(JsConcreteValue.number(1.0) in domain) + assertFalse(JsConcreteValue.number(-0.0) in domain) + assertFalse(JsConcreteValue.number(0.5) in domain) + assertFalse(JsConcreteValue.number(Double.NaN) in domain) + assertFalse(JsConcreteValue.number(Double.POSITIVE_INFINITY) in domain) + } + + @Test + fun `number membership preserves binary64 special values and inclusive bounds`() { + val zero = NumberDomain( + min = JsNumber.finite(0.0), + max = JsNumber.finite(0.0), + allowNaN = false, + ) + val unbounded = NumberDomain() + + assertTrue(JsConcreteValue.number(0.0) in zero) + assertTrue(JsConcreteValue.number(-0.0) in zero) + assertFalse(JsConcreteValue.number(1.0) in zero) + assertTrue(JsConcreteValue.number(Double.NaN) in unbounded) + assertTrue(JsConcreteValue.number(Double.NEGATIVE_INFINITY) in unbounded) + assertTrue(JsConcreteValue.number(Double.POSITIVE_INFINITY) in unbounded) + } + + @Test + fun `invalid number encodings do not belong to numeric domains`() { + val invalidNumber = JsConcreteValue.Number( + number = JsNumber(value = JsNumberKind.FINITE, bits = "invalid"), + ) + + assertFalse(invalidNumber in IntegerDomain()) + assertFalse(invalidNumber in NumberDomain()) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryTest.kt new file mode 100644 index 000000000..e2d2d1512 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/registry/PropertyRegistryTest.kt @@ -0,0 +1,80 @@ +package org.usvm.ts.pbt.registry + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.validation.InvalidPropertyDefinitionException +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class PropertyRegistryTest { + @Test + fun `registry validates definitions before exposing them`() { + val invalid = property(id = "invalid.property").copy(inputs = emptyList()) + + assertFailsWith { + PropertyRegistry(listOf(invalid)) + } + } + + @Test + fun `registry preserves property order and selects by id`() { + val second = property(id = "second") + val first = property(id = "first") + + val registry = PropertyRegistry(listOf(second, first)) + + assertEquals(listOf(second, first), registry.properties) + assertEquals(first, registry[PropertyId("first")]) + } + + @Test + fun `duplicate property ids report every conflicting position`() { + val error = assertFailsWith { + PropertyRegistry( + listOf( + property(id = "same"), + property(id = "different"), + property(id = "same"), + ), + ) + } + + assertEquals(PropertyId("same"), error.propertyId) + assertEquals(listOf(0, 2), error.positions) + } + + @Test + fun `unknown property id produces an actionable typed error`() { + val registry = PropertyRegistry(listOf(property(id = "known"))) + + val error = assertFailsWith { + registry[PropertyId("missing")] + } + + assertEquals(PropertyId("missing"), error.propertyId) + assertEquals(listOf(PropertyId("known")), error.availablePropertyIds) + } + + @Test + fun `combining registries rejects ids duplicated across registries`() { + val first = PropertyRegistry(listOf(property(id = "shared"))) + val second = PropertyRegistry(listOf(property(id = "shared"))) + + assertFailsWith { + PropertyRegistry.combine(listOf(first, second)) + } + } + + private fun property(id: String) = PropertyDefinition( + id = PropertyId(id), + inputs = listOf(PropertyInput(name = "value", domain = BooleanDomain)), + predicate = TypeScriptEntryPoint( + module = "properties/example.ts", + exportName = "predicate", + ), + ) +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt index b991ef5e7..dde7a5bcc 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt @@ -1,8 +1,6 @@ package org.usvm.ts.pbt.validation import org.junit.jupiter.api.Test -import org.usvm.ts.pbt.manifest.PROPERTY_MANIFEST_SCHEMA_VERSION -import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.JsConcreteValue @@ -93,21 +91,6 @@ class PropertyValidationTest { ) } - @Test - fun `manifest validation rejects unknown schema version`() { - val manifest = PropertyManifest( - schemaVersion = PROPERTY_MANIFEST_SCHEMA_VERSION + 1, - propertyId = "valid.id", - inputs = listOf(PropertyInput("value", IntegerDomain())), - predicate = TypeScriptEntryPoint("properties/value.ts", "holds"), - ) - - assertEquals( - listOf("manifest.schema.unsupported"), - validatePropertyManifest(manifest).diagnostics.map { it.code }, - ) - } - @Test fun `valid definition has no diagnostics`() { assertTrue(validatePropertyDefinition(validDefinition(IntegerDomain(-5, 5))).isValid) diff --git a/usvm-ts-pbt/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider b/usvm-ts-pbt/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider new file mode 100644 index 000000000..40accf414 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/META-INF/services/org.usvm.ts.pbt.registry.PropertyRegistryProvider @@ -0,0 +1 @@ +org.usvm.ts.pbt.cli.InstalledDistributionRegistryProvider diff --git a/usvm-ts-pbt/src/test/resources/properties/execution/ExecutionProperties.ts b/usvm-ts-pbt/src/test/resources/properties/execution/ExecutionProperties.ts new file mode 100644 index 000000000..62aa6b6d1 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/properties/execution/ExecutionProperties.ts @@ -0,0 +1,29 @@ +export function alwaysTrue(_value: number): boolean { + return true; +} + +export function sumIsCommutative(left: number, right: number): boolean { + return left + right === right + left; +} + +export function isNegative(value: number): boolean { + return value < 0; +} + +export async function asyncAlwaysTrue(_value: number): Promise { + return true; +} + +export async function asyncIsOne(value: number): Promise { + return value === 1; +} + +export function isNotSeven(value: number): boolean { + return value !== 7; +} + +export async function neverCompletes(_value: number): Promise { + await new Promise(() => undefined); + + return true; +}