From f9667400ef44148596197e816e31bc1593513f5c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 00:03:56 +0300 Subject: [PATCH 1/6] [TS PBT] Align property execution semantics --- usvm-ts-pbt/DESIGN.md | 24 +- usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md | 94 +++++++ usvm-ts-pbt/README.md | 14 +- .../fast-check-adapter/src/diagnostics.ts | 2 + .../src/execute-property.ts | 82 ++++-- .../fast-check-adapter/src/project-domain.ts | 16 +- .../test/entry-point.test.ts | 20 ++ .../test/execute-property.test.ts | 230 +++++++++++----- .../test/project-domain.test.ts | 23 ++ .../ts/pbt/backend/ProjectionCapability.kt | 6 +- .../backend/PropertyBasedTestingBackend.kt | 22 +- .../usvm/ts/pbt/model/PropertyDefinition.kt | 6 +- .../PropertyBasedTestingBackendTest.kt | 29 +++ .../PropertyExecutionContractTest.kt | 246 ++++++++++++++++++ .../contract/PropertyExecutionContract.ts | 76 ++++++ 15 files changed, 773 insertions(+), 117 deletions(-) create mode 100644 usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt create mode 100644 usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md index 0e40b6057..72ef50064 100644 --- a/usvm-ts-pbt/DESIGN.md +++ b/usvm-ts-pbt/DESIGN.md @@ -10,6 +10,8 @@ API and CLI examples, see [README.md](README.md). - Per-property source coverage is an optional backend capability collected by Kotlin through an isolated c8 run. - A backend-neutral Kotlin mapping layer connects manifests and source coverage to EtsIR without changing the declarative property model. +- One [property execution contract](PROPERTY_EXECUTION_CONTRACT.md) defines concrete, replay, projection, and + symbolic-search semantics. - 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. @@ -111,12 +113,11 @@ sequenceDiagram 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. -Each callback receives its own recursive clone of the generated arguments. This keeps predicate and precondition -mutations from changing fast-check's retained sample or leaking from one callback into the other during shrinking -and replay, while preserving aliases and cycles within one invocation. +The normative behavior is defined by the [property execution contract](PROPERTY_EXECUTION_CONTRACT.md). +Mechanically, input order is preserved from `PropertyDefinition.inputs` to positional TypeScript arguments. If +either entry point 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. One `structuredClone` isolates each +fast-check invocation; the precondition and predicate then receive that same clone in sequence. ## Results, errors, and timeouts @@ -125,8 +126,9 @@ flowchart TD Check[Property execution] --> Held{Outcome} Held -->|held| Success[SUCCESS result] Held -->|falsified| Failure[FAILURE result with counterexample] + Held -->|discard budget exhausted| Discarded[FAILURE with PRECONDITION_EXHAUSTED] Held -->|fast-check timeout| TimeoutResult[FAILURE result with timeout details] - Held -->|typed adapter error| Diagnostic[Error response with explicit category] + Held -->|precondition or 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] @@ -134,9 +136,9 @@ flowchart TD 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. +Falsification, discard-budget exhaustion, and a timeout cleanly reported by fast-check are completed results with +distinct failure kinds. Only falsification is a candidate property violation. Invalid input, entry-point contract +failures, process failures, malformed responses, and the JVM hard timeout are infrastructure exceptions. Coverage collection failures use the separate `COVERAGE` infrastructure category. Stable diagnostics distinguish an unsupported backend or Node runtime, unavailable runtime version, missing collector, missing or malformed @@ -281,6 +283,8 @@ classifier because `tsx` depends on a native esbuild package. 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. +- Shared contract fixtures cover precondition admission, discard and errors; predicate violations and errors; + special values; aliases; mutation isolation; shrinking; and replay through observable outcomes. - Coverage golden tests assert literal TypeScript statement and branch outcomes for successful and falsified runs, cross-property isolation, scope and glob filtering, and source-map/report diagnostics. - Mapping golden tests load stable TypeScript fixtures through the native frontend and cover predicate, diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md new file mode 100644 index 000000000..f5d5adcc6 --- /dev/null +++ b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md @@ -0,0 +1,94 @@ +# Property execution contract + +This document is the normative contract shared by concrete execution, replay, shrinking, domain projection, and +symbolic property search. Backend-specific documents may describe mechanics, but they must not redefine these +semantics. + +## Inputs and one invocation + +Inputs follow the ordered Kotlin `PropertyDefinition.inputs` domains and the tagged `JsConcreteValue` encoding. +Argument order is preserved. `undefined`, `null`, UTF-16 strings, NaN, both infinities, negative zero, and nested +arrays retain their JavaScript meaning. + +Every predicate attempt receives an isolated input graph. Concrete generation, explicit examples, replay, and +each shrinking attempt must not observe mutation left by another attempt. Aliases and cycles already present in +one backend input graph are preserved inside that invocation. The tagged wire representation is a value tree and +does not create reference identity between independently encoded nodes. + +When a property has a precondition, the precondition and predicate run sequentially over the same isolated graph. +This matches symbolic execution, where both functions observe one state. A supported precondition is pure, so it +does not change that graph. + +## Precondition + +A supported precondition is a pure boolean function of its inputs. + +| Completion | Meaning | +| --------------------- | --------------------------------------------------------------------------------- | +| `true` | Admit the input and invoke the predicate. | +| `false` | Discard the input without invoking the predicate. | +| Escaping exception | Property-definition or execution error; never a discard or counterexample. | +| Non-boolean result | Property-definition or execution error; never a discard or counterexample. | +| Unsupported execution | Report unsupported explicitly; do not substitute different execution semantics. | + +If a concrete run exhausts fast-check's discard budget, it completes with +`PropertyFailureKind.PRECONDITION_EXHAUSTED`. This is not a property violation and has no counterexample. + +Synchronous preconditions are the initial shared concrete and symbolic subset. Existing asynchronous concrete +preconditions retain their JavaScript meaning; symbolic projection and search report them as unsupported. + +## Predicate + +A predicate returns a boolean. + +| Completion | Meaning | +| ------------------ | ------------------------------------------------------------------------------ | +| `true` | The property holds for this invocation. | +| `false` | Candidate property violation. | +| Escaping exception | Candidate property violation, including an escaping assertion exception. | +| Non-boolean result | Property-definition or execution error; never a candidate property violation. | + +An expected exception belongs inside the property: the predicate catches it, checks it, and returns a boolean. +Asynchronous predicates remain available to the concrete backend and unsupported by symbolic execution until the +symbolic engine can preserve their meaning. + +## Mutation and external state + +Predicate-local mutation of supported input values is allowed. The invocation boundary isolates it from other +generated samples, explicit examples, replay, and shrinking while retaining aliases inside the current graph. + +Precondition purity is an author obligation. The initial contract does not include a purity analyzer, heap +snapshotting, rollback of arbitrary side effects, mutable objects beyond the supported value model, or persistent +external or module state. Properties that depend on those behaviors are outside the supported subset. + +## Projection and search classifications + +Projection is always relative to the complete declared Kotlin input domain: + +| Level | Required interpretation | +| ------------- | ------------------------------------------------------------------------------------------------------ | +| `EXACT` | The projected values have exactly the declared domain semantics. | +| `APPROXIMATE` | Diagnostics state whether the projection over-approximates, under-approximates, or combines both. | +| `UNSUPPORTED` | The backend cannot preserve the declared semantics and must not silently execute a different property. | + +An over-approximation may produce candidates outside the declared domain; they require concrete validation. An +under-approximation omits declared inputs, so an unsuccessful search cannot establish that the property holds. +Every retained approximation must document its direction and limitation in a capability diagnostic. + +Only predicate `false` and escaping predicate exceptions are candidate violations. Timeout, unsupported +execution, solver uncertainty, input-resolution failure, tool failure, and discard-budget exhaustion are neither +violations nor proof that the property holds. A bounded search with no candidate reports only that no violation +was reached within that search. + +## Implementation and regression points + +- `fast-check-adapter/src/execute-property.ts` applies this contract to generation, explicit examples, replay, and + shrinking through the existing fast-check invocation. +- `fast-check-adapter/src/project-domain.ts` projects the declared Kotlin domains for concrete execution. +- USVM projection and search implementations consume the same manifest and mapping artifacts and must link to + this contract when their dependent changes are integrated. +- `src/test/resources/properties/contract/PropertyExecutionContract.ts` is the shared observable fixture for + concrete and symbolic contract regressions. + +Replay remains ordinary concrete execution with the reported seed and path. It does not introduce a separate +property runner or alternate callback semantics. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 5f01f441a..6219768fd 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -51,6 +51,9 @@ export function reverseTwicePreservesValues(values: number[]): boolean { `JsConcreteValue` is a lossless tagged representation used for examples and counterexamples. It preserves `undefined`, `null`, NaN, infinities, negative zero, and nested arrays. +The normative behavior of inputs, preconditions, predicates, mutation isolation, projection, search, and replay is +defined once in the [property execution contract](PROPERTY_EXECUTION_CONTRACT.md). + ## Execute a property `FastCheckBackend` accepts TypeScript source roots and loads `.ts` entry points directly. User projects do not @@ -75,12 +78,13 @@ The defaults are 100 successful runs and a 60-second timeout. Configuration also positional explicit examples. `PropertyRunResult` contains the property ID, status, actual seed, replay path, counterexample, run/skip/shrink counts, failure details, elapsed time, and optional per-property coverage. -Predicate falsification and a timeout reported by fast-check are normal `FAILURE` results. Invalid input, -entry-point, process, and transport failures throw `PbtBackendException`. +Predicate falsification, discard-budget exhaustion, and a timeout reported by fast-check are completed `FAILURE` +results with distinct `PropertyFailureKind` values. Only `PROPERTY` denotes a candidate violation; +`PRECONDITION_EXHAUSTED` and `TIMEOUT` do not. Invalid input, entry-point contract, process, and transport failures +throw `PbtBackendException`. -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. +Generation, replay, explicit examples, checking, and shrinking use the same invocation path and follow the +[property execution contract](PROPERTY_EXECUTION_CONTRACT.md). ## Per-property TypeScript coverage diff --git a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts b/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts index e1ab704f4..145b2d57b 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/diagnostics.ts @@ -31,6 +31,7 @@ export const adapterDiagnostic = { domainKindUnknown: invalidRequest('domain.kind.unknown'), domainOptionalNil: invalidRequest('domain.optional.nil'), domainTupleEmpty: invalidRequest('domain.tuple.empty'), + domainConstantUnsupported: invalidRequest('domain.constant.unsupported'), domainNumberAllowNaNInvalid: invalidRequest('domain.number.allow-nan.invalid'), domainNumberBoundNaN: invalidRequest('domain.number.bound.nan'), domainNumberBounds: invalidRequest('domain.number.bounds'), @@ -55,4 +56,5 @@ export const adapterDiagnostic = { entryPointModuleImportFailed: entryPoint('entrypoint.module.import-failed'), entryPointExecutionKindMismatch: entryPoint('entrypoint.execution-kind.mismatch'), entryPointResultInvalid: entryPoint('entrypoint.result.invalid'), + entryPointPreconditionThrew: entryPoint('entrypoint.precondition.threw'), } as const; diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts index 0b562d5cb..a11e5a39d 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -37,6 +37,7 @@ export interface FastCheckExecutionRequest { manifest: PropertyManifestWire; sourceRoots: string[]; seed?: number; + /** Replay follows the same invocation contract as generation and shrinking. */ replayPath?: string; numRuns: number; timeoutMillis: number; @@ -44,7 +45,7 @@ export interface FastCheckExecutionRequest { } export interface FastCheckFailureDetails { - kind: 'property' | 'timeout'; + kind: 'property' | 'precondition-exhausted' | 'timeout'; errorName: string; message: string; } @@ -106,19 +107,63 @@ function buildProperty( if (asynchronous) { return fc.asyncProperty(arbitrary, async (values: JsConcreteValue[]): Promise => { - if (precondition !== undefined && !(await precondition.invoke(cloneArguments(values)))) fc.pre(false); + const invocationValues = cloneArguments(values); + if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) fc.pre(false); - return await predicate.invoke(cloneArguments(values)); + return await predicate.invoke(invocationValues); }); } return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => { - if (precondition !== undefined && !precondition.invoke(cloneArguments(values))) fc.pre(false); + const invocationValues = cloneArguments(values); + if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) fc.pre(false); - return predicate.invoke(cloneArguments(values)) as boolean; + return predicate.invoke(invocationValues) as boolean; }); } +async function invokePrecondition( + precondition: LoadedEntryPoint, + values: JsConcreteValue[], +): Promise { + try { + return await precondition.invoke(values); + } catch (error: unknown) { + throw classifyPreconditionError(error); + } +} + +function invokeSynchronousPrecondition( + precondition: LoadedEntryPoint, + values: JsConcreteValue[], +): boolean { + try { + return precondition.invoke(values) as boolean; + } catch (error: unknown) { + throw classifyPreconditionError(error); + } +} + +function classifyPreconditionError(error: unknown): ProtocolError { + if (error instanceof ProtocolError) return error; + + return protocolError( + adapterDiagnostic.entryPointPreconditionThrew, + `Property precondition threw ${describeThrownValue(error)}`, + 'manifest.precondition', + ); +} + +function describeThrownValue(value: unknown): string { + if (value instanceof Error) { + const name = value.name || 'Error'; + + return value.message.length === 0 ? name : `${name}: ${value.message}`; + } + + return `a non-Error value: ${String(value)}`; +} + async function checkProperty( property: fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]>, parameters: Parameters<[JsConcreteValue[]]>, @@ -139,28 +184,9 @@ async function checkProperty( } } -/** - * User callbacks must not mutate fast-check's sample, which it retains for shrinking and replay. - * A shared clone map preserves aliases and cycles within one invocation while isolating separate invocations. - */ +/** See [the contract](../../PROPERTY_EXECUTION_CONTRACT.md) for the invocation and isolation rules. */ function cloneArguments(values: JsConcreteValue[]): JsConcreteValue[] { - return cloneArray(values, new Map()); -} - -function cloneArray( - value: JsConcreteValue[], - clones: Map, -): JsConcreteValue[] { - const existing = clones.get(value); - if (existing !== undefined) return existing; - - const clone: JsConcreteValue[] = []; - clones.set(value, clone); - for (const element of value) { - clone.push(Array.isArray(element) ? cloneArray(element, clones) : element); - } - - return clone; + return structuredClone(values); } function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConcreteValue[]]> { @@ -240,8 +266,8 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail if (details.counterexample === null) { return { - kind: 'property', - errorName: 'PropertyFailure', + kind: 'precondition-exhausted', + errorName: 'PreconditionExhausted', message: 'Property could not satisfy its precondition within the skip limit', }; } 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 391993901..1743ab083 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts @@ -21,6 +21,7 @@ export interface ProjectionCapability { type DomainRecord = Record; +/** See [the contract](../../PROPERTY_EXECUTION_CONTRACT.md) for projection fidelity requirements. */ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary { requireDomainObject(domain, path); @@ -44,8 +45,19 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary units.map((unit) => String.fromCharCode(unit)).join('')); - case 'constant': - return fc.constant(decodeJsValue(domain.value, `${path}.value`)); + case 'constant': { + const value = decodeJsValue(domain.value, `${path}.value`); + + if (Array.isArray(value)) { + throw protocolError( + adapterDiagnostic.domainConstantUnsupported, + 'Constant domains support JavaScript primitives only', + path, + ); + } + + return fc.constant(value); + } case 'optional': { const nil = decodeJsValue(domain.nil, `${path}.nil`); 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 index 58d11dc5d..c309c9f70 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts @@ -3,6 +3,7 @@ import { mkdtemp, mkdir, realpath, rm, symlink, writeFile } from 'node:fs/promis import { tmpdir } from 'node:os'; import path from 'node:path'; import test from 'node:test'; +import { fileURLToPath } from 'node:url'; import { ProtocolError } from '../src/js-value.js'; import { loadEntryPoint } from '../src/entry-point.js'; @@ -198,6 +199,22 @@ test('enforces declared execution kind and boolean results', async () => { }); }); +test('preserves aliases in one supported invocation graph', async () => { + const loaded = await loadEntryPoint( + { + module: CONTRACT_MODULE, + exportName: 'preservesNestedArrayAlias', + executionKind: 'sync', + }, + [CONTRACT_SOURCE_ROOT], + 'manifest.predicate', + ); + const sharedElement = [1]; + const aliasedValue = [sharedElement, sharedElement]; + + assert.equal(loaded.invoke([aliasedValue]), true); +}); + async function withWorkspace(block: (workspace: string) => Promise): Promise { const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-entry-point-'))); @@ -222,3 +239,6 @@ async function assertProtocolError( function isProtocolError(error: unknown, code: string): error is ProtocolError { return error instanceof ProtocolError && error.code === code; } + +const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); +const CONTRACT_MODULE = 'properties/contract/PropertyExecutionContract.ts'; 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 index 802922207..a9c179099 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -3,7 +3,8 @@ 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 { fileURLToPath } from 'node:url'; +import { encodeJsValue, ProtocolError } from '../src/js-value.js'; import { executeProperty, type FastCheckExecutionRequest, @@ -66,7 +67,7 @@ test('supports asynchronous predicates and preconditions', async () => { }); }); -test('reports exhausted preconditions as a property failure without a counterexample', async () => { +test('classifies exhausted preconditions separately from property violations', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'alwaysTrue', { precondition: { @@ -81,8 +82,8 @@ test('reports exhausted preconditions as a property failure without a counterexa assert.equal(response.result.status, 'failure'); assert.equal(response.result.counterexample, null); - assert.equal(response.result.failure?.kind, 'property'); - assert.equal(response.result.failure?.errorName, 'PropertyFailure'); + assert.equal(response.result.failure?.kind, 'precondition-exhausted'); + assert.equal(response.result.failure?.errorName, 'PreconditionExhausted'); assert.equal( response.result.failure?.message, 'Property could not satisfy its precondition within the skip limit', @@ -90,6 +91,111 @@ test('reports exhausted preconditions as a property failure without a counterexa }); }); +test('reports a throwing precondition as an execution error instead of a counterexample', async () => { + const request = contractExecutionRequest('alwaysTrue', { + preconditionExport: 'throwingPrecondition', + }); + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.precondition.threw' + && error.path === 'manifest.precondition' + && error.diagnosticMessage === 'Property precondition threw a non-Error value: precondition exploded', + ); +}); + +test('reports a non-boolean precondition as an entry-point contract error', async () => { + const request = contractExecutionRequest('alwaysTrue', { + preconditionExport: 'nonBooleanPrecondition', + }); + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.result.invalid' + && error.path === 'manifest.precondition.result', + ); +}); + +test('keeps false, throwing, and assertion predicates classified as property violations', async () => { + for (const predicateExport of ['falsePredicate', 'throwingPredicate', 'assertionPredicate']) { + const response = await executeProperty(contractExecutionRequest(predicateExport)); + + assert.equal(response.result.status, 'failure'); + assert.equal(response.result.failure?.kind, 'property'); + assert.ok(response.result.counterexample); + } +}); + +test('reports a non-boolean predicate as an entry-point contract error', async () => { + await assert.rejects( + executeProperty(contractExecutionRequest('nonBooleanPredicate')), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.result.invalid' + && error.path === 'manifest.predicate.result', + ); +}); + +test('preserves positional special values through one invocation', async () => { + const request = contractExecutionRequest('recognizesSpecialValues', { + inputDomains: [ + constantDomain(undefined), + constantDomain(null), + constantDomain(-0), + constantDomain(Number.NaN), + constantDomain(Number.POSITIVE_INFINITY), + constantDomain(Number.NEGATIVE_INFINITY), + ], + }); + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'success'); +}); + +test('isolates predicate mutation between explicit examples and generated samples', async () => { + const request = contractExecutionRequest('isolatesPredicateMutation', { + inputDomains: [{ + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }], + }); + request.examples = [[encodeJsValue([1])]]; + request.numRuns = 2; + + const response = await executeProperty(request); + + assert.equal(response.result.status, 'success'); + assert.equal(response.result.numRuns, 2); +}); + +test('shrinks and replays the unmodified sample after predicate-local mutation', async () => { + const arrayDomain = { + kind: 'array', + element: { kind: 'integer', min: -10, max: 10 }, + minLength: 1, + maxLength: 3, + }; + const request = contractExecutionRequest('mutatesAndFails', { + inputDomains: [arrayDomain], + }); + + const first = await executeProperty(request); + const replay = await executeProperty({ + ...request, + replayPath: first.result.replayPath ?? undefined, + seed: first.result.seed, + }); + + assert.equal(first.result.status, 'failure'); + assert.ok(first.result.numShrinks > 0); + assert.notDeepEqual(first.result.counterexample, [encodeJsValue([999])]); + assert.deepEqual(replay.result.counterexample, first.result.counterexample); +}); + test('executes explicit examples through the same predicate', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'isNotSeven'); @@ -142,7 +248,17 @@ test('reports the original nested array when the predicate mutates its invocatio await withPropertyModule(async (sourceRoot) => { const originalValue = [[1]]; const request = executionRequest(sourceRoot, 'mutatesNestedArrayToObject', { - inputDomain: { kind: 'constant', value: encodeJsValue(originalValue) }, + inputDomain: { + kind: 'array', + element: { + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }, + minLength: 1, + maxLength: 1, + }, }); const response = await executeProperty(request); @@ -156,7 +272,12 @@ test('reports and replays the original array when the predicate creates a cycle' await withPropertyModule(async (sourceRoot) => { const originalValue = [1]; const request = executionRequest(sourceRoot, 'mutatesArrayToCycle', { - inputDomain: { kind: 'constant', value: encodeJsValue(originalValue) }, + inputDomain: { + kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, + minLength: 1, + maxLength: 1, + }, }); const first = await executeProperty(request); @@ -174,41 +295,6 @@ test('reports and replays the original array when the predicate creates a cycle' }); }); -test('isolates predicate input from recursive array mutation in the precondition', async () => { - await withPropertyModule(async (sourceRoot) => { - const request = executionRequest(sourceRoot, 'receivesOriginalNestedArray', { - precondition: { - module: 'properties.ts', - exportName: 'mutatesNestedArrayAndAccepts', - executionKind: 'sync', - }, - inputDomain: { kind: 'constant', value: encodeJsValue([[1]]) }, - }); - - const response = await executeProperty(request); - - assert.equal(response.result.status, 'success'); - }); -}); - -test('isolates asynchronous predicate input from recursive array mutation in the precondition', async () => { - await withPropertyModule(async (sourceRoot) => { - const request = executionRequest(sourceRoot, 'asyncReceivesOriginalNestedArray', { - predicateExecutionKind: 'async', - precondition: { - module: 'properties.ts', - exportName: 'asyncMutatesNestedArrayAndAccepts', - executionKind: 'async', - }, - inputDomain: { kind: 'constant', value: encodeJsValue([[1]]) }, - }); - - const response = await executeProperty(request); - - assert.equal(response.result.status, 'success'); - }); -}); - test('preserves non-Error thrown values including falsy primitives', async () => { await withPropertyModule(async (sourceRoot) => { const cases = ['boom', '', 0, false, null, undefined] as const; @@ -231,6 +317,7 @@ interface RequestOverrides { predicateExecutionKind?: 'sync' | 'async'; precondition?: FastCheckExecutionRequest['manifest']['precondition']; inputDomain?: unknown; + inputDomains?: unknown[]; } function executionRequest( @@ -238,12 +325,12 @@ function executionRequest( predicateExport: string, overrides: RequestOverrides = {}, ): FastCheckExecutionRequest { + const inputDomains = overrides.inputDomains ?? [ + overrides.inputDomain ?? { kind: 'integer', min: -10, max: 10 }, + ]; const manifest: FastCheckExecutionRequest['manifest'] = { propertyId: `example.${predicateExport}`, - inputs: [{ - name: 'value', - domain: overrides.inputDomain ?? { kind: 'integer', min: -10, max: 10 }, - }], + inputs: inputDomains.map((domain, index) => ({ name: `argument${index}`, domain })), predicate: { module: 'properties.ts', exportName: predicateExport, @@ -263,6 +350,36 @@ function executionRequest( }; } +interface ContractRequestOverrides { + preconditionExport?: string; + inputDomains?: unknown[]; +} + +function contractExecutionRequest( + predicateExport: string, + overrides: ContractRequestOverrides = {}, +): FastCheckExecutionRequest { + const requestOverrides: RequestOverrides = {}; + if (overrides.inputDomains !== undefined) requestOverrides.inputDomains = overrides.inputDomains; + + const request = executionRequest(CONTRACT_SOURCE_ROOT, predicateExport, requestOverrides); + request.manifest.predicate.module = CONTRACT_MODULE; + + if (overrides.preconditionExport !== undefined) { + request.manifest.precondition = { + module: CONTRACT_MODULE, + exportName: overrides.preconditionExport, + executionKind: 'sync', + }; + } + + return request; +} + +function constantDomain(value: unknown): unknown { + return { kind: 'constant', value: encodeJsValue(value) }; +} + 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'); @@ -316,27 +433,10 @@ export function mutatesArrayToCycle(value: unknown[]): boolean { return false; } -export function mutatesNestedArrayAndAccepts(value: unknown[][]): boolean { - value[0]![0] = {}; - - return true; -} - -export function receivesOriginalNestedArray(value: unknown[][]): boolean { - return value[0]?.[0] === 1; -} - -export async function asyncMutatesNestedArrayAndAccepts(value: unknown[][]): Promise { - value[0]![0] = {}; - - return true; -} - -export async function asyncReceivesOriginalNestedArray(value: unknown[][]): Promise { - return value[0]?.[0] === 1; -} - export function throwsInput(value: unknown): never { throw value; } `.trimStart(); + +const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); +const CONTRACT_MODULE = 'properties/contract/PropertyExecutionContract.ts'; 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 eb2a86f43..28d2c26c7 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 @@ -157,6 +157,29 @@ test('unknown domain kinds are rejected and reported as unsupported', () => { ); }); +test('constant domains reject composite values consistently with the Kotlin model', () => { + const domain = { + kind: 'constant', + value: { + kind: 'array', + elements: [{ kind: 'number', value: 'finite', bits: '3ff0000000000000' }], + }, + }; + + assert.throws(() => projectDomain(domain), /domain\.constant\.unsupported/); + assert.deepEqual( + projectionCapability(domain, 'inputs[0].domain'), + { + level: 'unsupported', + diagnostics: [{ + code: 'domain.constant.unsupported', + message: 'Constant domains support JavaScript primitives only', + path: 'inputs[0].domain', + }], + }, + ); +}); + function sample(domain: unknown, numRuns = 100): unknown[] { return fc.sample(projectDomain(domain), { seed: 42, numRuns }); } 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 d16949243..5772b997a 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 @@ -5,7 +5,7 @@ enum class ProjectionLevel { /** Every value produced by the backend has the declared Kotlin domain semantics. */ EXACT, - /** The backend can run the domain, but its values differ from the declared semantics. */ + /** The backend can run the domain, with diagnostics stating each over- or under-approximation. */ APPROXIMATE, /** The backend cannot project the domain. */ @@ -17,7 +17,7 @@ enum class PropertyCapabilityLevel { /** Both concrete and symbolic projections preserve the declared property semantics. */ EXACT, - /** Both projections are available, but at least one is approximate. */ + /** Both projections are available, but at least one has a documented directional approximation. */ APPROXIMATE, /** Concrete PBT execution is available, but symbolic execution is not. */ @@ -44,7 +44,7 @@ data class CapabilityDiagnostic( * Reports whether a property domain can be represented by an execution backend. * * @property level semantic fidelity of the projection - * @property diagnostics limitations that explain a non-exact [level] + * @property diagnostics limitations and directions that explain a non-exact [level] */ data class ProjectionCapability( val level: ProjectionLevel, 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 index 4e666df08..94f433c8f 100644 --- 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 @@ -44,7 +44,7 @@ data class PropertyRunConfiguration( } } -/** Whether the predicate held for every value executed by the backend. */ +/** Completion status; inspect [PropertyFailureKind] before interpreting a failure as a property violation. */ @Serializable enum class PropertyRunStatus { @SerialName("success") @@ -57,9 +57,15 @@ enum class PropertyRunStatus { /** Stable classification of a completed property failure. */ @Serializable enum class PropertyFailureKind { + /** A predicate returned false or let an exception escape for one admitted input. */ @SerialName("property") PROPERTY, + /** No generated or explicit input was admitted before the backend skip limit was exhausted. */ + @SerialName("precondition-exhausted") + PRECONDITION_EXHAUSTED, + + /** The concrete backend reported its configured time limit; this is not a property violation. */ @SerialName("timeout") TIMEOUT, } @@ -107,7 +113,19 @@ data class PropertyRunResult( } PropertyRunStatus.FAILURE -> { - requireNotNull(failure) { "A failed run requires failure details" } + val failureDetails = requireNotNull(failure) { "A failed run requires failure details" } + + when (failureDetails.kind) { + PropertyFailureKind.PROPERTY -> { + requireNotNull(counterexample) { "A property violation requires a counterexample" } + } + + PropertyFailureKind.PRECONDITION_EXHAUSTED, + PropertyFailureKind.TIMEOUT, + -> require(counterexample == null) { + "A non-violation failure must not contain a counterexample" + } + } } } } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt index b9234fba9..01b548b25 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt @@ -22,10 +22,12 @@ value class PropertyId private constructor(val value: String) { /** * Backend-independent Kotlin definition of one property. * + * Invocation semantics are defined in `usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md`. + * * @property id stable identity of the property * @property inputs ordered domains matching positional TypeScript parameters - * @property predicate TypeScript function that must hold for generated inputs - * @property precondition optional TypeScript function that filters inputs before evaluation + * @property predicate boolean TypeScript function that must hold for admitted inputs + * @property precondition optional pure boolean TypeScript function that admits or discards inputs */ @Serializable data class PropertyDefinition( 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 index 1ea7658c3..fcd53c2dd 100644 --- 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 @@ -76,6 +76,35 @@ class PropertyBasedTestingBackendTest { } } + @Test + fun `property violation requires a counterexample`() { + assertFailsWith { + successfulResult().copy( + status = PropertyRunStatus.FAILURE, + failure = PropertyFailureDetails( + kind = PropertyFailureKind.PROPERTY, + errorName = "PropertyFailure", + message = "predicate returned false", + ), + ) + } + } + + @Test + fun `non-violation failure rejects a counterexample`() { + assertFailsWith { + successfulResult().copy( + status = PropertyRunStatus.FAILURE, + counterexample = listOf(JsConcreteValue.Boolean(false)), + failure = PropertyFailureDetails( + kind = PropertyFailureKind.PRECONDITION_EXHAUSTED, + errorName = "PreconditionExhausted", + message = "discard budget exhausted", + ), + ) + } + } + @Test fun `failure details preserve an empty thrown value message`() { val details = PropertyFailureDetails( diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt new file mode 100644 index 000000000..bddbe22c6 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt @@ -0,0 +1,246 @@ +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.ConstantDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +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.assertNotEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyExecutionContractTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + @Test + fun `true precondition admits the input`() { + val result = backend.run( + property = property( + predicate = "alwaysTrue", + precondition = "truePrecondition", + ), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(0, result.numSkips) + } + + @Test + fun `false precondition exhaustion is not a property violation`() { + val result = backend.run( + property = property( + predicate = "alwaysTrue", + precondition = "falsePrecondition", + ), + configuration = configuration.copy(numRuns = 1), + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PRECONDITION_EXHAUSTED, result.failure?.kind) + assertEquals("PreconditionExhausted", result.failure?.errorName) + assertNull(result.counterexample) + } + + @Test + fun `throwing and non-boolean preconditions are execution errors`() { + val cases = listOf( + ContractErrorCase( + exportName = "throwingPrecondition", + expectedCode = "entrypoint.precondition.threw", + expectedPath = "manifest.precondition", + ), + ContractErrorCase( + exportName = "nonBooleanPrecondition", + expectedCode = "entrypoint.result.invalid", + expectedPath = "manifest.precondition.result", + ), + ) + + cases.forEach { case -> + val error = assertFailsWith { + backend.run( + property = property( + predicate = "alwaysTrue", + precondition = case.exportName, + ), + configuration = configuration, + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals(case.expectedCode, error.code) + assertEquals(case.expectedPath, error.path) + } + } + + @Test + fun `false throwing and assertion predicates are property violations`() { + listOf("falsePredicate", "throwingPredicate", "assertionPredicate").forEach { predicate -> + val result = backend.run( + property = property(predicate = predicate), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PROPERTY, result.failure?.kind) + assertNotNull(result.counterexample) + } + } + + @Test + fun `non-boolean predicate is an execution error`() { + val error = assertFailsWith { + backend.run( + property = property(predicate = "nonBooleanPredicate"), + configuration = configuration, + ) + } + + assertEquals(BackendErrorKind.ENTRY_POINT, error.kind) + assertEquals("entrypoint.result.invalid", error.code) + assertEquals("manifest.predicate.result", error.path) + } + + @Test + fun `a predicate may catch and classify an expected exception`() { + val result = backend.run( + property = property(predicate = "catchesExpectedException"), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + } + + @Test + fun `special values retain their identity and argument order`() { + val domains = listOf( + ConstantDomain(value = JsConcreteValue.Undefined), + ConstantDomain(value = JsConcreteValue.Null), + ConstantDomain(value = JsConcreteValue.number(-0.0)), + ConstantDomain(value = JsConcreteValue.number(Double.NaN)), + ConstantDomain(value = JsConcreteValue.number(Double.POSITIVE_INFINITY)), + ConstantDomain(value = JsConcreteValue.number(Double.NEGATIVE_INFINITY)), + ) + + val result = backend.run( + property = property( + predicate = "recognizesSpecialValues", + domains = domains, + ), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + } + + @Test + fun `predicate mutation is isolated between examples and generated samples`() { + val original = JsConcreteValue.Array( + elements = listOf(JsConcreteValue.number(1.0)), + ) + val domain = ArrayDomain( + element = IntegerDomain(min = 1, max = 1), + minLength = 1, + maxLength = 1, + ) + + val result = backend.run( + property = property( + predicate = "isolatesPredicateMutation", + domains = listOf(domain), + ), + configuration = configuration.copy( + numRuns = 2, + examples = listOf(listOf(original)), + ), + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(2, result.numRuns) + } + + @Test + fun `shrinking and replay retain the input before predicate mutation`() { + val domain = ArrayDomain( + element = IntegerDomain(min = -10, max = 10), + minLength = 1, + maxLength = 3, + ) + val definition = property( + predicate = "mutatesAndFails", + domains = listOf(domain), + ) + + val first = backend.run( + property = definition, + configuration = configuration, + ) + val counterexample = assertNotNull(first.counterexample) + val replayPath = assertNotNull(first.replayPath) + val replay = backend.run( + property = definition, + configuration = configuration.copy( + seed = first.seed, + replayPath = replayPath, + ), + ) + + assertEquals(PropertyRunStatus.FAILURE, first.status) + assertTrue(first.numShrinks > 0) + assertNotEquals( + JsConcreteValue.Array(elements = listOf(JsConcreteValue.number(999.0))), + counterexample.single(), + ) + assertEquals(counterexample, replay.counterexample) + } + + private fun property( + predicate: String, + precondition: String? = null, + domains: List = listOf(IntegerDomain(min = 0, max = 0)), + ): PropertyDefinition = PropertyDefinition( + id = PropertyId("contract.$predicate"), + inputs = domains.mapIndexed { index, domain -> + PropertyInput(name = "argument$index", domain = domain) + }, + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = predicate, + ), + precondition = precondition?.let { exportName -> + TypeScriptEntryPoint( + module = MODULE, + exportName = exportName, + ) + }, + ) + + private data class ContractErrorCase( + val exportName: String, + val expectedCode: String, + val expectedPath: String, + ) + + private companion object { + const val MODULE = "properties/contract/PropertyExecutionContract.ts" + + val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 5, + timeoutMillis = 1_000, + ) + } +} diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts new file mode 100644 index 000000000..0f8e5ee7a --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -0,0 +1,76 @@ +export function alwaysTrue(_value: number): boolean { + return true; +} + +export function truePrecondition(_value: number): boolean { + return true; +} + +export function falsePrecondition(_value: number): boolean { + return false; +} + +export function throwingPrecondition(_value: number): boolean { + throw 'precondition exploded'; +} + +export function nonBooleanPrecondition(_value: number): number { + return 1; +} + +export function falsePredicate(_value: number): boolean { + return false; +} + +export function throwingPredicate(_value: number): boolean { + throw 'predicate exploded'; +} + +export function assertionPredicate(_value: number): boolean { + throw 'AssertionError: contract assertion'; +} + +export function nonBooleanPredicate(_value: number): number { + return 1; +} + +export function catchesExpectedException(_value: number): boolean { + try { + throw 'expected'; + } catch (error: unknown) { + return error === 'expected'; + } +} + +export function recognizesSpecialValues( + missing: undefined, + empty: null, + negativeZero: number, + notANumber: number, + positiveInfinity: number, + negativeInfinity: number, +): boolean { + return missing === undefined + && empty === null + && Object.is(negativeZero, -0) + && Number.isNaN(notANumber) + && positiveInfinity === Number.POSITIVE_INFINITY + && negativeInfinity === Number.NEGATIVE_INFINITY; +} + +export function preservesNestedArrayAlias(values: number[][]): boolean { + return values.length === 2 && values[0] === values[1]; +} + +export function isolatesPredicateMutation(value: number[]): boolean { + const pristine = value.length === 1 && value[0] === 1; + value[0] = 2; + + return pristine; +} + +export function mutatesAndFails(value: number[]): boolean { + value[0] = 999; + + return false; +} From 39ef99dd7baa0e8ea9ed21eb751b014b441e3947 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 15:53:16 +0300 Subject: [PATCH 2/6] [TS PBT] Stabilize process transport fixtures --- .../org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt | 1 - .../org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt | 2 -- 2 files changed, 3 deletions(-) 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 index 2d7addcfb..dc95a3f9a 100644 --- 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 @@ -357,7 +357,6 @@ class FastCheckProcessClientTest { } })) """.trimIndent(), - transportGraceMillis = 100, ) { client -> val result = client.check(validRequest.copy(timeoutMillis = 100)) 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 444dc50ce..0da8bd89f 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 @@ -203,7 +203,6 @@ class FastCheckProjectionClientTest { """.trimIndent(), transportLimits = transportLimits( maxStdoutBytes = 1_024, - wallClockTimeoutMillis = 250, shutdownGraceMillis = 500, ), ) { temporaryClient -> @@ -273,7 +272,6 @@ class FastCheckProjectionClientTest { process.exit(0) """.trimIndent(), transportLimits = transportLimits( - wallClockTimeoutMillis = 250, shutdownGraceMillis = 500, ), ) { temporaryClient -> From f12f8f8090027000733a05461b993f430cc0963f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 16:23:03 +0300 Subject: [PATCH 3/6] [TS PBT] Clarify downstream symbolic integration --- usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md index f5d5adcc6..e91f20c26 100644 --- a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md +++ b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md @@ -85,10 +85,10 @@ was reached within that search. - `fast-check-adapter/src/execute-property.ts` applies this contract to generation, explicit examples, replay, and shrinking through the existing fast-check invocation. - `fast-check-adapter/src/project-domain.ts` projects the declared Kotlin domains for concrete execution. -- USVM projection and search implementations consume the same manifest and mapping artifacts and must link to - this contract when their dependent changes are integrated. -- `src/test/resources/properties/contract/PropertyExecutionContract.ts` is the shared observable fixture for - concrete and symbolic contract regressions. +- Downstream USVM projection and search implementations consume the same manifest and mapping artifacts and must + link to this contract when their dependent changes are integrated. +- `src/test/resources/properties/contract/PropertyExecutionContract.ts` provides concrete regression coverage; + downstream symbolic integration extends the same fixture with symbolic assertions. Replay remains ordinary concrete execution with the reported seed and path. It does not introduce a separate property runner or alternate callback semantics. From 66c069f317be14bcc495bb1bd0cdb71a92b9ddad Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 17 Sep 2026 23:12:27 +0300 Subject: [PATCH 4/6] [TS PBT] Preserve contract errors during shrinking --- .../src/execute-property.ts | 60 +++++++++++--- .../test/execute-property.test.ts | 83 ++++++++++++++++++- .../contract/PropertyExecutionContract.ts | 24 ++++++ 3 files changed, 156 insertions(+), 11 deletions(-) diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts index a11e5a39d..7da45a94a 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -81,11 +81,13 @@ export async function executeProperty(requestValue: unknown): Promise projectDomain(input.domain, `manifest.inputs[${index}].domain`)), ); - const property = buildProperty(arbitrary, predicate, precondition); + const contractErrors: ContractErrorState = { first: undefined }; + const property = buildProperty(arbitrary, predicate, precondition, contractErrors); const parameters = buildParameters(request); const details = await checkProperty(property, parameters, request.replayPath); + if (contractErrors.first !== undefined) throw contractErrors.first; if (details.errorInstance instanceof ProtocolError) throw details.errorInstance; return { @@ -102,24 +104,62 @@ function buildProperty( arbitrary: fc.Arbitrary, predicate: LoadedEntryPoint, precondition: LoadedEntryPoint | undefined, + contractErrors: ContractErrorState, ): fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]> { const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async'; if (asynchronous) { - return fc.asyncProperty(arbitrary, async (values: JsConcreteValue[]): Promise => { + return fc.asyncProperty(arbitrary, (values: JsConcreteValue[]): Promise => preserveAsyncContractError( + contractErrors, + async () => { + const invocationValues = cloneArguments(values); + if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) fc.pre(false); + + return await predicate.invoke(invocationValues); + }, + )); + } + + return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => preserveContractError( + contractErrors, + () => { const invocationValues = cloneArguments(values); - if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) fc.pre(false); + if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) fc.pre(false); + + return predicate.invoke(invocationValues) as boolean; + }, + )); +} + +interface ContractErrorState { + first: ProtocolError | undefined; +} + +function preserveContractError(state: ContractErrorState, invocation: () => T): T { + if (state.first !== undefined) throw state.first; + + try { + return invocation(); + } catch (error: unknown) { + if (error instanceof ProtocolError) state.first ??= error; - return await predicate.invoke(invocationValues); - }); + throw error; } +} - return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => { - const invocationValues = cloneArguments(values); - if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) fc.pre(false); +async function preserveAsyncContractError( + state: ContractErrorState, + invocation: () => Promise, +): Promise { + if (state.first !== undefined) throw state.first; - return predicate.invoke(invocationValues) as boolean; - }); + try { + return await invocation(); + } catch (error: unknown) { + if (error instanceof ProtocolError) state.first ??= error; + + throw error; + } } async function invokePrecondition( 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 index a9c179099..8aa633da9 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -137,6 +137,82 @@ test('reports a non-boolean predicate as an entry-point contract error', async ( ); }); +test('preserves synchronous contract errors when shrinking reaches a regular violation', async () => { + const cases = [ + { + predicateExport: 'falsePredicate', + preconditionExport: 'throwingWhenPositivePrecondition', + expectedCode: 'entrypoint.precondition.threw', + expectedPath: 'manifest.precondition', + }, + { + predicateExport: 'nonBooleanWhenPositivePredicate', + expectedCode: 'entrypoint.result.invalid', + expectedPath: 'manifest.predicate.result', + }, + ]; + + for (const contractCase of cases) { + const request = contractExecutionRequest(contractCase.predicateExport, { + inputDomains: [{ kind: 'integer', min: 0, max: 100 }], + ...(contractCase.preconditionExport === undefined + ? {} + : { preconditionExport: contractCase.preconditionExport }), + }); + request.examples = [[encodeJsValue(100)]]; + request.numRuns = 1; + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === contractCase.expectedCode + && error.path === contractCase.expectedPath, + ); + } +}); + +test('preserves asynchronous contract errors when shrinking reaches a regular violation', async () => { + const cases = [ + { + predicateExport: 'falsePredicate', + preconditionExport: 'asyncThrowingWhenPositivePrecondition', + preconditionExecutionKind: 'async' as const, + expectedCode: 'entrypoint.precondition.threw', + expectedPath: 'manifest.precondition', + }, + { + predicateExport: 'asyncNonBooleanWhenPositivePredicate', + predicateExecutionKind: 'async' as const, + expectedCode: 'entrypoint.result.invalid', + expectedPath: 'manifest.predicate.result', + }, + ]; + + for (const contractCase of cases) { + const request = contractExecutionRequest(contractCase.predicateExport, { + inputDomains: [{ kind: 'integer', min: 0, max: 100 }], + ...(contractCase.predicateExecutionKind === undefined + ? {} + : { predicateExecutionKind: contractCase.predicateExecutionKind }), + ...(contractCase.preconditionExport === undefined + ? {} + : { preconditionExport: contractCase.preconditionExport }), + ...(contractCase.preconditionExecutionKind === undefined + ? {} + : { preconditionExecutionKind: contractCase.preconditionExecutionKind }), + }); + request.examples = [[encodeJsValue(100)]]; + request.numRuns = 1; + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === contractCase.expectedCode + && error.path === contractCase.expectedPath, + ); + } +}); + test('preserves positional special values through one invocation', async () => { const request = contractExecutionRequest('recognizesSpecialValues', { inputDomains: [ @@ -352,6 +428,8 @@ function executionRequest( interface ContractRequestOverrides { preconditionExport?: string; + preconditionExecutionKind?: 'sync' | 'async'; + predicateExecutionKind?: 'sync' | 'async'; inputDomains?: unknown[]; } @@ -361,6 +439,9 @@ function contractExecutionRequest( ): FastCheckExecutionRequest { const requestOverrides: RequestOverrides = {}; if (overrides.inputDomains !== undefined) requestOverrides.inputDomains = overrides.inputDomains; + if (overrides.predicateExecutionKind !== undefined) { + requestOverrides.predicateExecutionKind = overrides.predicateExecutionKind; + } const request = executionRequest(CONTRACT_SOURCE_ROOT, predicateExport, requestOverrides); request.manifest.predicate.module = CONTRACT_MODULE; @@ -369,7 +450,7 @@ function contractExecutionRequest( request.manifest.precondition = { module: CONTRACT_MODULE, exportName: overrides.preconditionExport, - executionKind: 'sync', + executionKind: overrides.preconditionExecutionKind ?? 'sync', }; } diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts index 0f8e5ee7a..b27e492c3 100644 --- a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -18,6 +18,22 @@ export function nonBooleanPrecondition(_value: number): number { return 1; } +export function throwingWhenPositivePrecondition(value: number): boolean { + if (value > 0) { + throw 'positive precondition'; + } + + return true; +} + +export async function asyncThrowingWhenPositivePrecondition(value: number): Promise { + if (value > 0) { + throw 'positive async precondition'; + } + + return true; +} + export function falsePredicate(_value: number): boolean { return false; } @@ -34,6 +50,14 @@ export function nonBooleanPredicate(_value: number): number { return 1; } +export function nonBooleanWhenPositivePredicate(value: number): number | boolean { + return value > 0 ? 42 : false; +} + +export async function asyncNonBooleanWhenPositivePredicate(value: number): Promise { + return value > 0 ? 42 : false; +} + export function catchesExpectedException(_value: number): boolean { try { throw 'expected'; From b2f778626fe47119bc0f558bac6ee54591f49427 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 18 Sep 2026 00:01:04 +0300 Subject: [PATCH 5/6] [TS PBT] Preserve exception origins in property results --- .../src/execute-property.ts | 48 ++++++++----------- .../test/execute-property.test.ts | 42 ++++++++++++++++ .../PropertyExecutionContractTest.kt | 33 +++++++++++++ .../contract/PropertyExecutionContract.ts | 36 ++++++++++++++ 4 files changed, 131 insertions(+), 28 deletions(-) diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts index 7da45a94a..7b952dfdd 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -195,13 +195,17 @@ function classifyPreconditionError(error: unknown): ProtocolError { } function describeThrownValue(value: unknown): string { - if (value instanceof Error) { - const name = value.name || 'Error'; + try { + if (value instanceof Error) { + const name = String(value.name || 'Error'); - return value.message.length === 0 ? name : `${name}: ${value.message}`; - } + return value.message.length === 0 ? name : `${name}: ${value.message}`; + } - return `a non-Error value: ${String(value)}`; + return `a non-Error value: ${String(value)}`; + } catch { + return 'an unprintable value'; + } } async function checkProperty( @@ -247,7 +251,6 @@ function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConc const parameters: Parameters<[JsConcreteValue[]]> = { numRuns: request.numRuns, - timeout: request.timeoutMillis, interruptAfterTimeLimit: request.timeoutMillis, markInterruptAsFailure: true, examples: decodedExamples, @@ -285,22 +288,20 @@ function toRunResult( } function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFailureDetails { - const error = details.errorInstance; - const timeout = (details.interrupted && details.counterexample === null) || isFastCheckTimeout(error); - - if (error instanceof Error) { + if (details.interrupted && details.counterexample === null) { return { - kind: timeout ? 'timeout' : 'property', - errorName: error.name || 'Error', - message: error.message || 'Property execution failed', + kind: 'timeout', + errorName: 'TimeoutError', + message: 'Property execution exceeded the configured timeout', }; } - if (timeout) { + const error = details.errorInstance; + if (error instanceof Error) { return { - kind: 'timeout', - errorName: 'TimeoutError', - message: 'Property execution exceeded the configured timeout', + kind: 'property', + errorName: error.name || 'Error', + message: error.message || 'Property execution failed', }; } @@ -319,17 +320,9 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail }; } -function isFastCheckTimeout(error: unknown): boolean { - return hasFastCheckMessagePrefix(error, FAST_CHECK_TIMEOUT_PREFIX); -} - +/** The pinned fast-check version exposes invalid replay paths only through a stable message prefix. */ function isFastCheckReplayFailure(error: unknown): boolean { - return hasFastCheckMessagePrefix(error, FAST_CHECK_REPLAY_FAILURE_PREFIX); -} - -/** The pinned fast-check version exposes these two failure categories only through stable message prefixes. */ -function hasFastCheckMessagePrefix(error: unknown, prefix: string): boolean { - return error instanceof Error && error.message.startsWith(prefix); + return error instanceof Error && error.message.startsWith(FAST_CHECK_REPLAY_FAILURE_PREFIX); } function validateRequest(value: unknown): FastCheckExecutionRequest { @@ -513,4 +506,3 @@ function isSignedInt(value: unknown): value is number { const MAX_TIMER_DELAY_MILLIS = 2 ** 31 - 1; const REPLAY_PATH_PATTERN = /^\d+(?::\d+)*$/; const FAST_CHECK_REPLAY_FAILURE_PREFIX = 'Unable to replay,'; -const FAST_CHECK_TIMEOUT_PREFIX = 'Property timeout:'; 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 index 8aa633da9..c50c7fa2f 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -118,6 +118,47 @@ test('reports a non-boolean precondition as an entry-point contract error', asyn ); }); +test('keeps unprintable precondition exceptions classified as execution errors', async () => { + const cases = [ + { exportName: 'throwingOpaquePrecondition', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingOpaquePrecondition', executionKind: 'async' as const }, + { exportName: 'throwingUnprintableErrorPrecondition', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingUnprintableErrorPrecondition', executionKind: 'async' as const }, + { exportName: 'throwingUnprintableNamePrecondition', executionKind: 'sync' as const }, + ]; + + for (const { exportName, executionKind } of cases) { + const request = contractExecutionRequest('alwaysTrue', { + preconditionExport: exportName, + preconditionExecutionKind: executionKind, + }); + + await assert.rejects( + executeProperty(request), + (error: unknown) => error instanceof ProtocolError + && error.code === 'entrypoint.precondition.threw' + && error.path === 'manifest.precondition', + ); + } +}); + +test('keeps timeout-shaped predicate exceptions classified as property violations', async () => { + const cases = [ + { exportName: 'throwingTimeoutMessagePredicate', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingTimeoutMessagePredicate', executionKind: 'async' as const }, + ]; + + for (const { exportName, executionKind } of cases) { + const request = contractExecutionRequest(exportName, { predicateExecutionKind: executionKind }); + + const response = await executeProperty(request); + + assert.equal(response.result.failure?.kind, 'property'); + assert.ok(response.result.counterexample); + assert.equal(response.result.failure?.message, 'Property timeout: exceeded limit of 20 milliseconds'); + } +}); + test('keeps false, throwing, and assertion predicates classified as property violations', async () => { for (const predicateExport of ['falsePredicate', 'throwingPredicate', 'assertionPredicate']) { const response = await executeProperty(contractExecutionRequest(predicateExport)); @@ -296,6 +337,7 @@ test('reports asynchronous predicate timeout as a structured timeout failure', a assert.equal(response.result.status, 'failure'); assert.equal(response.result.failure?.kind, 'timeout'); + assert.equal(response.result.counterexample, null); }); }); diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt index bddbe22c6..dc4fcc5eb 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt @@ -6,6 +6,7 @@ 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.ConstantDomain +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.PropertyDefinition @@ -62,6 +63,16 @@ class PropertyExecutionContractTest { expectedCode = "entrypoint.precondition.threw", expectedPath = "manifest.precondition", ), + ContractErrorCase( + exportName = "throwingOpaquePrecondition", + expectedCode = "entrypoint.precondition.threw", + expectedPath = "manifest.precondition", + ), + ContractErrorCase( + exportName = "throwingUnprintableErrorPrecondition", + expectedCode = "entrypoint.precondition.threw", + expectedPath = "manifest.precondition", + ), ContractErrorCase( exportName = "nonBooleanPrecondition", expectedCode = "entrypoint.result.invalid", @@ -114,6 +125,28 @@ class PropertyExecutionContractTest { assertEquals("manifest.predicate.result", error.path) } + @Test + fun `timeout-shaped predicate exceptions are property violations`() { + val cases = listOf( + "throwingTimeoutMessagePredicate" to ExecutionKind.SYNC, + "asyncThrowingTimeoutMessagePredicate" to ExecutionKind.ASYNC, + ) + + cases.forEach { (exportName, executionKind) -> + val definition = property(predicate = exportName) + + val result = backend.run( + property = definition.copy(predicate = definition.predicate.copy(executionKind = executionKind)), + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PROPERTY, result.failure?.kind) + assertNotNull(result.counterexample) + assertEquals("Property timeout: exceeded limit of 20 milliseconds", result.failure?.message) + } + } + @Test fun `a predicate may catch and classify an expected exception`() { val result = backend.run( diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts index b27e492c3..d87831de5 100644 --- a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -14,6 +14,34 @@ export function throwingPrecondition(_value: number): boolean { throw 'precondition exploded'; } +export function throwingOpaquePrecondition(_value: number): boolean { + throw Object.create(null); +} + +export async function asyncThrowingOpaquePrecondition(value: number): Promise { + return throwingOpaquePrecondition(value); +} + +export function throwingUnprintableErrorPrecondition(_value: number): boolean { + const error = new Error(); + Object.defineProperty(error, 'message', { + get() { throw new Error('message getter failed'); }, + }); + + throw error; +} + +export async function asyncThrowingUnprintableErrorPrecondition(value: number): Promise { + return throwingUnprintableErrorPrecondition(value); +} + +export function throwingUnprintableNamePrecondition(_value: number): boolean { + const error = new Error(); + Object.defineProperty(error, 'name', { value: Object.create(null) }); + + throw error; +} + export function nonBooleanPrecondition(_value: number): number { return 1; } @@ -42,6 +70,14 @@ export function throwingPredicate(_value: number): boolean { throw 'predicate exploded'; } +export function throwingTimeoutMessagePredicate(_value: number): boolean { + throw new Error('Property timeout: exceeded limit of 20 milliseconds'); +} + +export async function asyncThrowingTimeoutMessagePredicate(value: number): Promise { + return throwingTimeoutMessagePredicate(value); +} + export function assertionPredicate(_value: number): boolean { throw 'AssertionError: contract assertion'; } From 0ecfda69a6bebe6d21411190d4a65055edd1d5b1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 13:21:03 +0300 Subject: [PATCH 6/6] [TS PBT] Preserve hostile predicate failures --- .../fast-check-adapter/src/entry-point.ts | 29 ++++++++++-- .../src/execute-property.ts | 44 ++++++++++++++----- .../test/entry-point.test.ts | 20 --------- .../test/execute-property.test.ts | 24 ++++++++++ .../PropertyExecutionContractTest.kt | 10 ----- .../contract/PropertyExecutionContract.ts | 30 ++++++++----- 6 files changed, 100 insertions(+), 57 deletions(-) diff --git a/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts b/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts index 3cf32a460..d12173cc7 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/entry-point.ts @@ -19,6 +19,13 @@ export interface LoadedEntryPoint { invoke(args: JsConcreteValue[]): boolean | Promise; } +/** Keeps user-thrown values distinct from adapter contract errors across external runners. */ +export class EntryPointInvocationError extends Error { + constructor(readonly thrownValue: unknown) { + super('Property entry point threw'); + } +} + type EntryPointFunction = (...args: JsConcreteValue[]) => unknown; export async function loadEntryPoint( @@ -183,7 +190,7 @@ function buildInvocation( ): (args: JsConcreteValue[]) => boolean | Promise { if (executionKind === 'sync') { return (args: JsConcreteValue[]): boolean => { - const result = entryPoint(...args); + const result = invokeEntryPoint(entryPoint, args); if (isThenable(result)) { void Promise.resolve(result).catch(() => undefined); @@ -199,7 +206,7 @@ function buildInvocation( } return async (args: JsConcreteValue[]): Promise => { - const result = entryPoint(...args); + const result = invokeEntryPoint(entryPoint, args); if (!isThenable(result)) { throw protocolError( @@ -209,10 +216,26 @@ function buildInvocation( ); } - return requireBoolean(await result, referencePath); + return requireBoolean(await resolveEntryPoint(result), referencePath); }; } +function invokeEntryPoint(entryPoint: EntryPointFunction, args: JsConcreteValue[]): unknown { + try { + return entryPoint(...args); + } catch (error: unknown) { + throw new EntryPointInvocationError(error); + } +} + +async function resolveEntryPoint(result: PromiseLike): Promise { + try { + return await result; + } catch (error: unknown) { + throw new EntryPointInvocationError(error); + } +} + function requireBoolean(result: unknown, referencePath: string): boolean { if (typeof result !== 'boolean') { throw protocolError( diff --git a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts index 7b952dfdd..1fbca31b1 100644 --- a/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-pbt/fast-check-adapter/src/execute-property.ts @@ -6,6 +6,7 @@ import { type AdapterDiagnosticDescriptor, } from './diagnostics.js'; import { + EntryPointInvocationError, type ExecutionKind, loadEntryPoint, type LoadedEntryPoint, @@ -187,9 +188,11 @@ function invokeSynchronousPrecondition( function classifyPreconditionError(error: unknown): ProtocolError { if (error instanceof ProtocolError) return error; + const thrownValue = error instanceof EntryPointInvocationError ? error.thrownValue : error; + return protocolError( adapterDiagnostic.entryPointPreconditionThrew, - `Property precondition threw ${describeThrownValue(error)}`, + `Property precondition threw ${describeThrownValue(thrownValue)}`, 'manifest.precondition', ); } @@ -296,15 +299,6 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail }; } - const error = details.errorInstance; - if (error instanceof Error) { - return { - kind: 'property', - errorName: error.name || 'Error', - message: error.message || 'Property execution failed', - }; - } - if (details.counterexample === null) { return { kind: 'precondition-exhausted', @@ -313,13 +307,39 @@ function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFail }; } + const error = details.errorInstance instanceof EntryPointInvocationError + ? details.errorInstance.thrownValue + : details.errorInstance; + return { kind: 'property', - errorName: 'ThrownValue', - message: String(error), + ...describePropertyFailure(error), }; } +function describePropertyFailure(value: unknown): Pick { + try { + if (value instanceof Error) { + return { + errorName: typeof value.name === 'string' && value.name.length > 0 ? value.name : 'Error', + message: typeof value.message === 'string' && value.message.length > 0 + ? value.message + : 'Property execution failed', + }; + } + + return { + errorName: 'ThrownValue', + message: String(value), + }; + } catch { + return { + errorName: 'ThrownValue', + message: 'An unprintable value', + }; + } +} + /** The pinned fast-check version exposes invalid replay paths only through a stable message prefix. */ function isFastCheckReplayFailure(error: unknown): boolean { return error instanceof Error && error.message.startsWith(FAST_CHECK_REPLAY_FAILURE_PREFIX); 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 index c309c9f70..58d11dc5d 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/entry-point.test.ts @@ -3,7 +3,6 @@ import { mkdtemp, mkdir, realpath, rm, symlink, writeFile } from 'node:fs/promis import { tmpdir } from 'node:os'; import path from 'node:path'; import test from 'node:test'; -import { fileURLToPath } from 'node:url'; import { ProtocolError } from '../src/js-value.js'; import { loadEntryPoint } from '../src/entry-point.js'; @@ -199,22 +198,6 @@ test('enforces declared execution kind and boolean results', async () => { }); }); -test('preserves aliases in one supported invocation graph', async () => { - const loaded = await loadEntryPoint( - { - module: CONTRACT_MODULE, - exportName: 'preservesNestedArrayAlias', - executionKind: 'sync', - }, - [CONTRACT_SOURCE_ROOT], - 'manifest.predicate', - ); - const sharedElement = [1]; - const aliasedValue = [sharedElement, sharedElement]; - - assert.equal(loaded.invoke([aliasedValue]), true); -}); - async function withWorkspace(block: (workspace: string) => Promise): Promise { const workspace = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-entry-point-'))); @@ -239,6 +222,3 @@ async function assertProtocolError( function isProtocolError(error: unknown, code: string): error is ProtocolError { return error instanceof ProtocolError && error.code === code; } - -const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); -const CONTRACT_MODULE = 'properties/contract/PropertyExecutionContract.ts'; 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 index c50c7fa2f..c4f98a1bc 100644 --- a/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-pbt/fast-check-adapter/test/execute-property.test.ts @@ -159,6 +159,30 @@ test('keeps timeout-shaped predicate exceptions classified as property violation } }); +test('keeps hostile predicate exceptions classified as property violations', async () => { + const cases = [ + { exportName: 'throwingOpaquePrecondition', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingOpaquePrecondition', executionKind: 'async' as const }, + { exportName: 'throwingUnprintableErrorPrecondition', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingUnprintableErrorPrecondition', executionKind: 'async' as const }, + { exportName: 'throwingUnprintableNamePrecondition', executionKind: 'sync' as const }, + { exportName: 'throwingFastCheckBrandedPredicate', executionKind: 'sync' as const }, + { exportName: 'asyncThrowingFastCheckBrandedPredicate', executionKind: 'async' as const }, + { exportName: 'throwingHostileProxyPredicate', executionKind: 'sync' as const }, + ]; + + for (const { exportName, executionKind } of cases) { + const request = contractExecutionRequest(exportName, { predicateExecutionKind: executionKind }); + + const response = await executeProperty(request); + + assert.equal(response.result.failure?.kind, 'property'); + assert.ok(response.result.counterexample); + assert.equal(typeof response.result.failure?.errorName, 'string'); + assert.equal(typeof response.result.failure?.message, 'string'); + } +}); + test('keeps false, throwing, and assertion predicates classified as property violations', async () => { for (const predicateExport of ['falsePredicate', 'throwingPredicate', 'assertionPredicate']) { const response = await executeProperty(contractExecutionRequest(predicateExport)); diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt index dc4fcc5eb..8bbeba15b 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt @@ -147,16 +147,6 @@ class PropertyExecutionContractTest { } } - @Test - fun `a predicate may catch and classify an expected exception`() { - val result = backend.run( - property = property(predicate = "catchesExpectedException"), - configuration = configuration, - ) - - assertEquals(PropertyRunStatus.SUCCESS, result.status) - } - @Test fun `special values retain their identity and argument order`() { val domains = listOf( diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts index d87831de5..9ee8c432b 100644 --- a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -78,6 +78,24 @@ export async function asyncThrowingTimeoutMessagePredicate(value: number): Promi return throwingTimeoutMessagePredicate(value); } +export function throwingFastCheckBrandedPredicate(_value: number): boolean { + throw { + footprint: Symbol.for('fast-check/PreconditionFailure'), + interruptExecution: false, + }; +} + +export async function asyncThrowingFastCheckBrandedPredicate(value: number): Promise { + return throwingFastCheckBrandedPredicate(value); +} + +export function throwingHostileProxyPredicate(_value: number): boolean { + throw new Proxy({}, { + get() { throw new Error('property access failed'); }, + getPrototypeOf() { throw new Error('prototype access failed'); }, + }); +} + export function assertionPredicate(_value: number): boolean { throw 'AssertionError: contract assertion'; } @@ -94,14 +112,6 @@ export async function asyncNonBooleanWhenPositivePredicate(value: number): Promi return value > 0 ? 42 : false; } -export function catchesExpectedException(_value: number): boolean { - try { - throw 'expected'; - } catch (error: unknown) { - return error === 'expected'; - } -} - export function recognizesSpecialValues( missing: undefined, empty: null, @@ -118,10 +128,6 @@ export function recognizesSpecialValues( && negativeInfinity === Number.NEGATIVE_INFINITY; } -export function preservesNestedArrayAlias(values: number[][]): boolean { - return values.length === 2 && values[0] === values[1]; -} - export function isolatesPredicateMutation(value: number[]): boolean { const pristine = value.length === 1 && value[0] === 1; value[0] = 2;