From e3179ec8896680af3bb43c897577ea3b9b971188 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 00:03:56 +0300 Subject: [PATCH 1/8] [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 0e40b60571..72ef500643 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 0000000000..f5d5adcc6d --- /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 5f01f441a0..6219768fd5 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 e1ab704f4c..145b2d57bc 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 0b562d5cb1..a11e5a39db 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 3919939017..1743ab0834 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 58d11dc5df..c309c9f703 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 802922207e..a9c179099e 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 eb2a86f435..28d2c26c7c 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 d169492430..5772b997aa 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 4e666df086..94f433c8f1 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 b9234fba98..01b548b25e 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 1ea7658c33..fcd53c2dd5 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 0000000000..bddbe22c6d --- /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 0000000000..0f8e5ee7af --- /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 bf594d57e47eaf7ea93b5e0e5064d684d1f6ebd3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 15:53:16 +0300 Subject: [PATCH 2/8] [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 2d7addcfba..dc95a3f9a6 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 444dc50cef..0da8bd89f3 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 174af1a0002fe11e60f7fc2d87bbbf62f38e0014 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 16:23:03 +0300 Subject: [PATCH 3/8] [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 f5d5adcc6d..e91f20c26b 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 b05597352ea439e232a9d617029df5d8b8e6af90 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 17 Sep 2026 23:12:27 +0300 Subject: [PATCH 4/8] [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 a11e5a39db..7da45a94a9 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 a9c179099e..8aa633da9a 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 0f8e5ee7af..b27e492c34 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 1a46c28f5f03cf151d29f0c81e9bdd8059209c7d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 18 Sep 2026 00:01:04 +0300 Subject: [PATCH 5/8] [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 7da45a94a9..7b952dfdd3 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 8aa633da9a..c50c7fa2f5 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 bddbe22c6d..dc4fcc5eb2 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 b27e492c34..d87831de55 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 4949a160cecb78ac7f57dcd1f91554015d5dda94 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 09:51:30 +0300 Subject: [PATCH 6/8] [TS PBT] Integrate USVM property execution contract --- usvm-ts-pbt/DESIGN.md | 21 +- usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md | 8 +- usvm-ts-pbt/README.md | 25 + usvm-ts-pbt/build.gradle.kts | 1 + .../org/usvm/ts/pbt/PbtDiagnosticCode.kt | 20 + .../ts/pbt/usvm/UsvmCandidateInputResolver.kt | 178 +++++++ .../usvm/ts/pbt/usvm/UsvmDomainProjector.kt | 393 ++++++++++++++++ .../usvm/UsvmProjectionCapabilityResolver.kt | 352 ++++++++++++++ .../usvm/ts/pbt/usvm/UsvmProjectionModel.kt | 30 ++ .../usvm/ts/pbt/usvm/UsvmPropertyProjector.kt | 310 ++++++++++++ .../ts/pbt/usvm/UsvmPropertySearchModel.kt | 54 +++ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 441 ++++++++++++++++++ .../usvm/PropertyExecutionConformanceTest.kt | 263 +++++++++++ .../usvm/UsvmCollectionDomainProjectorTest.kt | 175 +++++++ .../usvm/UsvmInitialStateConfigurationTest.kt | 110 +++++ .../usvm/UsvmPreconditionProjectionTest.kt | 124 +++++ .../pbt/usvm/UsvmProjectionCapabilityTest.kt | 208 +++++++++ .../pbt/usvm/UsvmProjectionConformanceTest.kt | 48 ++ .../ts/pbt/usvm/UsvmPropertySearcherTest.kt | 231 +++++++++ .../pbt/usvm/UsvmScalarDomainProjectorTest.kt | 245 ++++++++++ .../contract/PropertyExecutionContract.ts | 12 + .../resources/usvm/UsvmCapabilityFixture.ts | 31 ++ .../resources/usvm/UsvmPreconditionFixture.ts | 27 ++ .../usvm/UsvmPropertySearchFixture.ts | 71 +++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 72 ++- .../kotlin/org/usvm/machine/TsMethodCall.kt | 14 + .../usvm/machine/interpreter/TsInterpreter.kt | 109 ++++- .../kotlin/org/usvm/machine/state/TsState.kt | 15 + .../org/usvm/machine/state/TsStateUtils.kt | 23 + 29 files changed, 3578 insertions(+), 33 deletions(-) create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md index 72ef500643..f4c18201ee 100644 --- a/usvm-ts-pbt/DESIGN.md +++ b/usvm-ts-pbt/DESIGN.md @@ -245,6 +245,21 @@ useful separation is preserved: declarative receiver/argument/result positions a values, and condition interpretation is distinct from position resolution. The TypeScript mapper expresses this with EtsIR-specific binding and mapping records and has no dependency on `usvm-jvm` or the taint-analysis module. +## USVM projection and property search + +The existing projection path configures `TsMachine`'s initial state from exact mapper bindings and declared Kotlin +domains. The existing search path prepends a mapped synchronous precondition to the predicate entry point. Guard +completion is explicit in `TsState`: false terminates a rejected path, while an exception or non-boolean result +terminates an error path. Neither path can reach the predicate target. + +Predicate false paths are re-solved on a cloned terminal state before target propagation, so the ordinary terminal +state is not rewritten. Predicate exceptions reach the same candidate target. Runtime non-boolean entry-point +results are property errors regardless of their TypeScript return annotation. A residual call that stops a path is +unsupported, while ordinary unsatisfiable path pruning is not an engine failure. Timeout, solver uncertainty, +interpreter failure, and candidate-input resolution failure retain separate search outcomes. Candidate extraction +reads the projected input state with the terminal model, so predicate-local array mutation does not rewrite the +reported input. + ## Process supervision `FastCheckProcessTransport` writes stdin and drains stdout and stderr concurrently. This is necessary because each @@ -284,7 +299,9 @@ classifier because `tsx` depends on a native esbuild package. - 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. + special values; aliases; mutation isolation; shrinking; and replay through observable outcomes. One focused JVM + conformance test executes the same classification fixture through the real FastCheck and USVM paths, including + literal and never return annotations and replay of a pre-mutation USVM candidate. - 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, @@ -297,5 +314,5 @@ classifier because `tsx` depends on a native esbuild package. - 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. -- Constructing symbolic inputs or executing mapped properties in USVM. +- General purity analysis, arbitrary mutable-object projection, and persistent state across property invocations. - Combining backend source coverage with future EtsIR replay coverage. diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md index e91f20c26b..83aa9c856a 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. -- 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. +- `UsvmPropertyProjector` and `UsvmPropertySearcher` apply this contract to the existing USVM projection and search + paths. `PropertyExecutionConformanceTest` runs the same TypeScript fixture through `FastCheckBackend` and USVM. +- `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 6219768fd5..fdd4bc0997 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -204,6 +204,31 @@ Stable mapping diagnostics include `mapping.entry-point.unmapped`, `mapping.entr separately from mapping provenance and backend diagnostics are copied without reinterpretation. +## USVM projection and property search + +`UsvmProjectionCapabilityResolver` compares the declared domains with the exact EtsIR parameter bindings. +Booleans, bounded integers and numbers, supported primitive constants, optionals, bounded tuples, and bounded +arrays are projected by `UsvmDomainProjector`. Strings are an explicit over-approximation: USVM constrains their +type and UTF-16 length but not their contents. Nested arrays, incompatible EtsIR types, and collections above +`UsvmProjectionOptions.maxSymbolicCollectionLength` are unsupported with stable diagnostics. + +`UsvmPropertyProjector` executes a mapped synchronous precondition over projected inputs. It reports accepted and +rejected domains separately; a reachable exception or non-boolean result is `PROPERTY_ERROR`, solver uncertainty is +`SOLVER_UNKNOWN`, and async, non-exact, or unsupported residual-call execution is `UNSUPPORTED`. + +`UsvmPropertySearcher` evaluates the mapped precondition and predicate in one symbolic state. A false precondition +is `PRECONDITION_REJECTED` when it excludes the complete projected domain. A precondition exception or non-boolean +result is `PROPERTY_ERROR`. Predicate `false` and escaping predicate exceptions are `VIOLATION_REACHED`, while a +non-boolean predicate is `PROPERTY_ERROR`. Timeout, solver uncertainty, unsupported execution, engine failure, and +input-resolution failure retain distinct statuses and are never treated as proof or as violations. + +The shared fixture in `src/test/resources/properties/contract/PropertyExecutionContract.ts` is executed by both +`FastCheckBackend` and the USVM projection/search path. It covers precondition admission, rejection, exception and +non-boolean results, plus false, throwing, literal-boolean-typed, never-typed, and non-boolean predicates. A shared +mutation regression also verifies that a USVM candidate is reconstructed from the input before predicate mutation +and reproduces through fast-check. Special values, alias preservation, mutation isolation, shrinking, and replay +remain covered at the concrete invocation boundary. + ## Registries and CLI The CLI loads Kotlin property registries through `ServiceLoader`: diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts index afc82d9f47..a76e672747 100644 --- a/usvm-ts-pbt/build.gradle.kts +++ b/usvm-ts-pbt/build.gradle.kts @@ -7,6 +7,7 @@ plugins { } dependencies { + implementation(project(":usvm-core")) implementation(project(":usvm-ts")) implementation(Libs.jacodb_ets) implementation(Libs.clikt) 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 index 65dbf5170d..a31d8463a9 100644 --- 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 @@ -61,6 +61,26 @@ internal object PbtDiagnosticCode { const val MAPPING_STATEMENT_AMBIGUOUS = "mapping.statement.ambiguous" const val MAPPING_STATEMENT_UNMAPPED = "mapping.statement.unmapped" + const val USVM_DOMAIN_ARRAY_NESTED_UNSUPPORTED = "usvm.domain.array.nested.unsupported" + const val USVM_DOMAIN_COLLECTION_TOO_LARGE = "usvm.domain.collection.too-large" + const val USVM_DOMAIN_STRING_APPROXIMATE = "usvm.domain.string.approximate" + const val USVM_DOMAIN_TYPE_UNSUPPORTED = "usvm.domain.type.unsupported" + const val USVM_ENGINE_FAILURE = "usvm.engine.failure" + const val USVM_EXECUTION_UNSUPPORTED = "usvm.execution.unsupported" + const val USVM_INPUT_BINDING_UNAVAILABLE = "usvm.input.binding.unavailable" + const val USVM_INPUT_RESOLUTION_FAILED = "usvm.input.resolution.failed" + const val USVM_MAPPING_PROPERTY_ID_MISMATCH = "usvm.mapping.property-id.mismatch" + const val USVM_PRECONDITION_ASYNC = "usvm.precondition.async" + const val USVM_PRECONDITION_BINDING_UNAVAILABLE = "usvm.precondition.binding.unavailable" + const val USVM_PRECONDITION_MAPPING_NON_EXACT = "usvm.precondition.mapping.non-exact" + const val USVM_PRECONDITION_MAPPING_UNAVAILABLE = "usvm.precondition.mapping.unavailable" + const val USVM_PRECONDITION_RESULT_NON_BOOLEAN = "usvm.precondition.result.non-boolean" + const val USVM_PRECONDITION_THREW = "usvm.precondition.threw" + const val USVM_PREDICATE_ASYNC = "usvm.predicate.async" + const val USVM_PREDICATE_MAPPING_NON_EXACT = "usvm.predicate.mapping.non-exact" + const val USVM_PREDICATE_RESULT_NON_BOOLEAN = "usvm.predicate.result.non-boolean" + const val USVM_SOLVER_UNKNOWN = "usvm.solver.unknown" + const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid" const val SOURCE_ROOT_INVALID = "source-root.invalid" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt new file mode 100644 index 0000000000..1e7a584632 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt @@ -0,0 +1,178 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.isTrue +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.extractDouble +import org.usvm.machine.expr.extractInt +import org.usvm.machine.expr.toConcreteBoolValue +import org.usvm.machine.state.TsState +import org.usvm.sizeSort +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +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.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +internal class UsvmCandidateInputResolver { + fun resolve( + state: TsState, + declaredInputs: List, + projection: UsvmDeclaredDomainProjection, + ): List { + require(declaredInputs.size == projection.inputs.size) + val initialState = projection.initialState.clone() + initialState.models = state.models + + return declaredInputs.zip(projection.inputs).map { (input, projected) -> + resolveValue( + state = initialState, + domain = input.domain, + etsType = projected.etsType, + value = projected.value, + ) + } + } + + private fun resolveValue( + state: TsState, + domain: PropertyDomain, + etsType: EtsType, + value: UExpr, + ): JsConcreteValue = with(state.ctx) { + if (value.isFakeObject()) { + return@with resolveFakeValue(state, domain, etsType, value) + } + + when (domain) { + BooleanDomain -> JsConcreteValue.Boolean( + state.models.single().eval(value.asExpr(boolSort)).toConcreteBoolValue(), + ) + + is IntegerDomain, is NumberDomain -> JsConcreteValue.number( + state.models.single().eval(value.asExpr(fp64Sort)).extractDouble(), + ) + + is StringDomain -> resolveString(state, value) + is ConstantDomain -> domain.value + is OptionalDomain -> resolveOptional(state, domain, etsType, value) + is TupleDomain -> resolveTuple(state, domain, etsType, value) + is ArrayDomain -> resolveArray(state, domain, etsType as EtsArrayType, value) + } + } + + private fun resolveFakeValue( + state: TsState, + domain: PropertyDomain, + etsType: EtsType, + value: UConcreteHeapRef, + ): JsConcreteValue = with(state.ctx) { + val model = state.models.single() + val fakeType = value.getFakeType(state.memory) + val selected = when { + model.eval(fakeType.boolTypeExpr).isTrue -> value.extractBool(state.memory) + model.eval(fakeType.fpTypeExpr).isTrue -> value.extractFp(state.memory) + model.eval(fakeType.refTypeExpr).isTrue -> value.extractRef(state.memory) + else -> error("Cannot resolve the selected fake-object type") + } + + resolveValue(state, domain, etsType, selected) + } + + private fun resolveOptional( + state: TsState, + domain: OptionalDomain, + etsType: EtsType, + value: UExpr, + ): JsConcreteValue = with(state.ctx) { + if (value.sort == addressSort) { + val ref = value.asExpr(addressSort) + val nil = when (domain.nil) { + JsConcreteValue.Null -> mkTsNullValue() + JsConcreteValue.Undefined -> mkUndefinedValue() + else -> error("Optional nil must be null or undefined") + } + if (state.models.single().eval(mkHeapRefEq(ref, nil)).isTrue) { + return@with domain.nil + } + } + + val nestedType = (etsType as org.jacodb.ets.model.EtsUnionType).types.first { type -> + UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type) + } + + resolveValue(state, domain.value, nestedType, value) + } + + private fun resolveString(state: TsState, value: UExpr): JsConcreteValue.String = with(state.ctx) { + val ref = state.models.single().eval(value.asExpr(addressSort)) as? UConcreteHeapRef + ?: error("Symbolic string reference did not resolve to a concrete heap reference") + val concrete = getStringConstantValue(ref) + ?: error("Symbolic string contents are unavailable") + + JsConcreteValue.String(concrete) + } + + private fun resolveTuple( + state: TsState, + domain: TupleDomain, + etsType: EtsType, + value: UExpr, + ): JsConcreteValue.Array = with(state.ctx) { + val ref = state.models.single().eval(value.asExpr(addressSort)) as UConcreteHeapRef + val elementTypes = when (etsType) { + is EtsTupleType -> etsType.types + is EtsArrayType -> List(domain.elements.size) { etsType.elementType } + else -> error("Unsupported tuple EtsIR type $etsType") + } + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val elements = domain.elements.zip(elementTypes).mapIndexed { index, (elementDomain, elementType) -> + val lValue = mkArrayIndexLValue(addressSort, ref, mkBv(index), arrayType) + val element = state.memory.read(lValue) + + resolveValue(state, elementDomain, elementType, element) + } + + JsConcreteValue.Array(elements) + } + + private fun resolveArray( + state: TsState, + domain: ArrayDomain, + etsType: EtsArrayType, + value: UExpr, + ): JsConcreteValue.Array = with(state.ctx) { + val ref = state.models.single().eval(value.asExpr(addressSort)) as UConcreteHeapRef + val lengthLValue = mkArrayLengthLValue(ref, etsType) + val length = state.models.single() + .eval(state.memory.read(lengthLValue).asExpr(sizeSort)) + .extractInt() + val elementSort = typeToSort(arrayDescriptorOf(etsType).let { it as EtsArrayType }.elementType) + val elements = (0 until length).map { index -> + val element = if (elementSort is TsUnresolvedSort) { + state.memory.read(mkArrayIndexLValue(addressSort, ref, mkBv(index), etsType)) + } else { + state.memory.read(mkArrayIndexLValue(elementSort, ref, mkBv(index), etsType)) + } + + resolveValue(state, domain.element, etsType.elementType, element) + } + + JsConcreteValue.Array(elements) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt new file mode 100644 index 0000000000..3f70b7b6e5 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -0,0 +1,393 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UAddressSort +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.api.initializeArrayLength +import org.usvm.api.makeSymbolicPrimitive +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.machine.types.mkFakeValue +import org.usvm.sizeSort +import org.usvm.ts.pbt.mapping.EtsInputBinding +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +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.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkRegisterStackLValue + +/** One symbolic input written to the mapped EtsIR stack slot. */ +data class UsvmProjectedInput( + val inputName: String, + val path: String, + val stackSlot: Int, + val etsType: EtsType, + val value: UExpr, +) + +/** Constraints created exclusively from declared Kotlin property domains. */ +data class UsvmDeclaredDomainProjection( + val inputs: List, + val initialState: TsState, +) + +/** Materializes declared property domains in a real USVM TypeScript initial state. */ +class UsvmDomainProjector( + private val options: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + fun configure( + state: TsState, + inputs: List, + bindings: List, + ): UsvmDeclaredDomainProjection { + require(inputs.size == bindings.size) { + "Property input count ${inputs.size} does not match EtsIR binding count ${bindings.size}" + } + + val preparedInputs = inputs.zip(bindings).mapIndexed { index, (input, binding) -> + require(input.name == binding.propertyInputName) { + "Property input ${input.name} does not match EtsIR binding ${binding.propertyInputName}" + } + + val path = "inputs[$index].domain" + val capability = UsvmProjectionCapabilityResolver().domainCapabilityForProjector( + domain = input.domain, + etsType = binding.parameter.type, + path = path, + options = options, + ) + + PreparedInput(input, binding, path, capability) + } + preparedInputs.forEach { prepared -> + require(prepared.capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { + prepared.capability.diagnostics.joinToString { diagnostic -> diagnostic.message } + } + } + + val projectedInputs = preparedInputs.map { prepared -> + val input = prepared.input + val binding = prepared.binding + val path = prepared.path + + val value = Materializer(state).materialize(input.domain, binding.parameter.type) + writeStackValue(state, binding.stackSlot, value) + + UsvmProjectedInput( + inputName = input.name, + path = path, + stackSlot = binding.stackSlot, + etsType = binding.parameter.type, + value = value, + ) + } + + return UsvmDeclaredDomainProjection( + inputs = projectedInputs, + initialState = state.clone(), + ) + } + + private data class PreparedInput( + val input: PropertyInput, + val binding: EtsInputBinding, + val path: String, + val capability: org.usvm.ts.pbt.backend.ProjectionCapability, + ) + + private inner class Materializer(private val state: TsState) { + fun materialize(domain: PropertyDomain, etsType: EtsType): UExpr = when (domain) { + BooleanDomain -> state.makeSymbolicPrimitive(state.ctx.boolSort) + is IntegerDomain -> materializeInteger(domain) + is NumberDomain -> materializeNumber(domain) + is StringDomain -> materializeString(domain) + is ConstantDomain -> materializeConstant(domain.value) + is OptionalDomain -> materializeOptional(domain, etsType) + is TupleDomain -> materializeTuple(domain, etsType) + is ArrayDomain -> materializeArray(domain, etsType as EtsArrayType) + } + + private fun materializeInteger(domain: IntegerDomain): UExpr = with(state.ctx) { + val value = state.makeSymbolicPrimitive(fp64Sort) + val rounded = mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = value, + ) + val negativeZero = mkAnd(mkFpIsZeroExpr(value), mkFpIsNegativeExpr(value)) + val minimum = mkFp(domain.min.toDouble(), fp64Sort) + val maximum = mkFp(domain.max.toDouble(), fp64Sort) + val isNumber = mkFpIsNaNExpr(value).not() + val isIntegral = mkFpEqualExpr(value, rounded) + val meetsMinimum = mkFpGreaterOrEqualExpr(value, minimum) + val meetsMaximum = mkFpLessOrEqualExpr(value, maximum) + + state.pathConstraints += mkAnd( + isNumber, + isIntegral, + negativeZero.not(), + meetsMinimum, + meetsMaximum, + ) + + value + } + + private fun materializeNumber(domain: NumberDomain): UExpr = with(state.ctx) { + val value = state.makeSymbolicPrimitive(fp64Sort) + val minimum = mkFp(domain.min.toDouble(), fp64Sort) + val maximum = mkFp(domain.max.toDouble(), fp64Sort) + val meetsMinimum = mkFpGreaterOrEqualExpr(value, minimum) + val meetsMaximum = mkFpLessOrEqualExpr(value, maximum) + val insideBounds = mkAnd(meetsMinimum, meetsMaximum) + val constraint = if (domain.allowNaN) { + mkOr(mkFpIsNaNExpr(value), insideBounds) + } else { + insideBounds + } + + state.pathConstraints += constraint + + value + } + + private fun materializeString(domain: StringDomain): UConcreteHeapRef = with(state.ctx) { + val value = state.memory.allocConcrete(EtsStringType) + val stringArrayType = EtsArrayType(EtsStringType, dimensions = 1) + val descriptor = arrayDescriptorOf(stringArrayType) + val length = state.makeSymbolicPrimitive(sizeSort) + val minimumLength = mkBv(domain.minLength) + val maximumLength = mkBv(domain.maxLength) + val meetsMinimum = mkBvSignedGreaterOrEqualExpr(length, minimumLength) + val meetsMaximum = mkBvSignedLessOrEqualExpr(length, maximumLength) + + state.memory.initializeArrayLength(value, descriptor, sizeSort, length) + state.pathConstraints += mkAnd(meetsMinimum, meetsMaximum) + + value + } + + private fun materializeConstant(value: JsConcreteValue): UExpr = with(state.ctx) { + when (value) { + is JsConcreteValue.Boolean -> mkBool(value.value) + is JsConcreteValue.Number -> mkFp(value.toDouble(), fp64Sort) + is JsConcreteValue.String -> state.mkInitializedStringConstant(value.value) + JsConcreteValue.Null -> mkTsNullValue() + JsConcreteValue.Undefined -> mkUndefinedValue() + is JsConcreteValue.Array -> error("Array constants are not valid property-domain primitives") + } + } + + private fun materializeOptional( + domain: OptionalDomain, + etsType: EtsType, + ): UExpr = with(state.ctx) { + val unionType = etsType as EtsUnionType + val nestedType = unionType.types.first { type -> + UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type) + } + val nestedValue = materialize(domain.value, nestedType) + val nilValue = materializeConstant(domain.nil) + val chooseValue = state.makeSymbolicPrimitive(boolSort) + + if (nestedValue.sort == nilValue.sort) { + return@with sameSortIte(chooseValue, nestedValue, nilValue) + } + + val fakeValue = state.mkFakeValue( + scope = null, + boolValue = nestedValue.asOptionalBool(), + fpValue = nestedValue.asOptionalFp(), + refValue = (nestedValue.asOptionalRef() ?: nilValue.asOptionalRef()), + ) + val fakeType = fakeValue.getFakeType(state.memory) + val nestedTypeExpr = when (nestedValue.sort) { + boolSort -> fakeType.boolTypeExpr + fp64Sort -> fakeType.fpTypeExpr + addressSort -> fakeType.refTypeExpr + else -> error("Unsupported optional value sort ${nestedValue.sort}") + } + val nilTypeExpr = when (nilValue.sort) { + boolSort -> fakeType.boolTypeExpr + fp64Sort -> fakeType.fpTypeExpr + addressSort -> fakeType.refTypeExpr + else -> error("Unsupported optional nil sort ${nilValue.sort}") + } + + state.pathConstraints += mkEq(nestedTypeExpr, chooseValue) + state.pathConstraints += mkEq(nilTypeExpr, chooseValue.not()) + + fakeValue + } + + private fun materializeTuple( + domain: TupleDomain, + etsType: EtsType, + ): UConcreteHeapRef = with(state.ctx) { + val elementTypes = when (etsType) { + is EtsTupleType -> etsType.types + is EtsArrayType -> List(domain.elements.size) { etsType.elementType } + else -> error("Unsupported tuple EtsIR type $etsType") + } + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val descriptor = arrayDescriptorOf(arrayType) + val array = state.memory.allocConcrete(descriptor) + + state.memory.initializeArrayLength(array, descriptor, sizeSort, mkBv(domain.elements.size)) + domain.elements.zip(elementTypes).forEachIndexed { index, (elementDomain, elementType) -> + val element = box(materialize(elementDomain, elementType)) + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = mkBv(index), + type = arrayType, + ) + + state.memory.write(lValue, element, guard = trueExpr) + } + + array + } + + private fun materializeArray( + domain: ArrayDomain, + etsType: EtsArrayType, + ): UConcreteHeapRef = with(state.ctx) { + val descriptor = arrayDescriptorOf(etsType) + val array = state.memory.allocConcrete(descriptor) + val length = state.makeSymbolicPrimitive(sizeSort) + val minimumLength = mkBv(domain.minLength) + val maximumLength = mkBv(domain.maxLength) + val meetsMinimum = mkBvSignedGreaterOrEqualExpr(length, minimumLength) + val meetsMaximum = mkBvSignedLessOrEqualExpr(length, maximumLength) + + state.memory.initializeArrayLength(array, descriptor, sizeSort, length) + state.pathConstraints += mkAnd(meetsMinimum, meetsMaximum) + + repeat(domain.maxLength) { index -> + val element = materialize(domain.element, etsType.elementType) + val guard = mkBvSignedLessExpr(mkBv(index), length) + + writeArrayElement(array, etsType, index, element, guard) + } + + array + } + + private fun writeArrayElement( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + index: Int, + value: UExpr, + guard: UBoolExpr, + ) = with(state.ctx) { + val descriptor = arrayDescriptorOf(arrayType) as EtsArrayType + val elementSort = typeToSort(descriptor.elementType) + if (elementSort is TsUnresolvedSort) { + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = mkBv(index), + type = arrayType, + ) + + state.memory.write(lValue, box(value), guard) + } else { + writeArrayElementWithKnownSort(array, arrayType, index, value, guard, elementSort) + } + } + + private fun writeArrayElementWithKnownSort( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + index: Int, + value: UExpr, + guard: UBoolExpr, + sort: USort, + ) = with(state.ctx) { + when (sort) { + boolSort -> { + val lValue = mkArrayIndexLValue(boolSort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(boolSort), guard) + } + + fp64Sort -> { + val lValue = mkArrayIndexLValue(fp64Sort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(fp64Sort), guard) + } + + addressSort -> { + val lValue = mkArrayIndexLValue(addressSort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(addressSort), guard) + } + + else -> error("Unsupported projected array element sort $sort") + } + } + + private fun box(value: UExpr): UConcreteHeapRef = with(state.ctx) { + if (value is UConcreteHeapRef && value.isFakeObject()) return@with value + + state.mkFakeValue( + scope = null, + boolValue = value.asOptionalBool(), + fpValue = value.asOptionalFp(), + refValue = value.asOptionalRef(), + ) + } + + private fun UExpr.asOptionalBool(): UExpr? = + takeIf { sort == state.ctx.boolSort }?.asExpr(state.ctx.boolSort) + + private fun UExpr.asOptionalFp(): UExpr? = + takeIf { sort == state.ctx.fp64Sort }?.asExpr(state.ctx.fp64Sort) + + private fun UExpr.asOptionalRef(): UExpr? = + takeIf { sort == state.ctx.addressSort }?.asExpr(state.ctx.addressSort) + + @Suppress("UNCHECKED_CAST") + private fun sameSortIte( + condition: UBoolExpr, + trueValue: UExpr, + falseValue: UExpr, + ): UExpr = state.ctx.mkIte( + condition, + trueValue as UExpr, + falseValue as UExpr, + ) + } +} + +private fun writeStackValue(state: TsState, stackSlot: Int, value: UExpr): Unit = with(state.ctx) { + require(value.sort == boolSort || value.sort == fp64Sort || value.sort == addressSort) { + "Unsupported projected stack sort ${value.sort}" + } + + val lValue = mkRegisterStackLValue(value.sort, stackSlot) + + state.memory.write(lValue, value.cast(), guard = trueExpr) + state.saveSortForLocal(stackSlot, value.sort) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt new file mode 100644 index 0000000000..1e183a0d35 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt @@ -0,0 +1,352 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanLiteralType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberLiteralType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringLiteralType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.aggregateProjectionCapabilities +import org.usvm.ts.pbt.backend.classifyPropertyCapability +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +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.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain + +/** Calculates USVM fidelity without constructing or mutating a symbolic state. */ +class UsvmProjectionCapabilityResolver { + fun resolve( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + options: UsvmProjectionOptions = UsvmProjectionOptions(), + ): UsvmPropertyProjectionCapability { + val predicateCapability = entryPointCapability( + mapping = mapping.predicate, + path = "predicate", + nonExactCode = PbtDiagnosticCode.USVM_PREDICATE_MAPPING_NON_EXACT, + ) + val predicateTarget = mapping.predicate.exactTargetOrNull() + val predicateExecutionCapability = if (manifest.predicate.executionKind == ExecutionKind.SYNC) { + exact() + } else { + unsupported( + code = PbtDiagnosticCode.USVM_PREDICATE_ASYNC, + message = "Asynchronous TypeScript predicates are not supported by USVM search", + path = "predicate", + ) + } + val inputCapabilities = manifest.inputs.mapIndexed { index, input -> + val path = "inputs[$index].domain" + val parameterType = predicateTarget + ?.bindings + ?.inputs + ?.getOrNull(index) + ?.parameter + ?.type + val capability = if (parameterType == null) { + unsupported( + code = PbtDiagnosticCode.USVM_INPUT_BINDING_UNAVAILABLE, + message = "An exact EtsIR input binding is required", + path = path, + ) + } else { + domainCapabilityForProjector(input.domain, parameterType, path, options) + } + + UsvmInputProjectionCapability( + inputName = input.name, + path = path, + capability = capability, + ) + } + val preconditionCapability = preconditionCapability(manifest, mapping, options) + val propertyIdCapability = if (mapping.propertyId.value == manifest.propertyId) { + exact() + } else { + unsupported( + code = PbtDiagnosticCode.USVM_MAPPING_PROPERTY_ID_MISMATCH, + message = "The property manifest and EtsIR mapping artifact have different IDs", + path = "propertyId", + ) + } + val symbolicComponents = buildList { + add(propertyIdCapability) + add(predicateCapability) + add(predicateExecutionCapability) + addAll(inputCapabilities.map { it.capability }) + add(preconditionCapability) + } + val symbolicCapability = aggregateProjectionCapabilities(symbolicComponents) + + return UsvmPropertyProjectionCapability( + inputs = inputCapabilities, + precondition = preconditionCapability, + symbolic = symbolicCapability, + property = classifyPropertyCapability(concreteCapability, symbolicCapability), + ) + } + + private fun preconditionCapability( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + options: UsvmProjectionOptions, + ): ProjectionCapability { + val declaredPrecondition = manifest.precondition ?: return exact() + if (declaredPrecondition.executionKind == ExecutionKind.ASYNC) { + return unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_ASYNC, + message = "Asynchronous TypeScript preconditions are not supported by USVM projection", + path = "precondition", + ) + } + + val mappedPrecondition = mapping.precondition + ?: return unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_MAPPING_UNAVAILABLE, + message = "The declared precondition has no EtsIR mapping", + path = "precondition", + ) + val mappingCapability = entryPointCapability( + mapping = mappedPrecondition, + path = "precondition", + nonExactCode = PbtDiagnosticCode.USVM_PRECONDITION_MAPPING_NON_EXACT, + ) + val target = mappedPrecondition.exactTargetOrNull() + ?: return mappingCapability + val inputCapabilities = manifest.inputs.mapIndexed { index, input -> + val parameterType = target.bindings.inputs + .getOrNull(index) + ?.parameter + ?.type + + if (parameterType == null) { + unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_BINDING_UNAVAILABLE, + message = "An exact EtsIR precondition input binding is required", + path = "precondition", + ) + } else { + domainCapabilityForProjector(input.domain, parameterType, "inputs[$index].domain", options) + } + } + + return aggregateProjectionCapabilities(listOf(mappingCapability) + inputCapabilities) + } + + private fun entryPointCapability( + mapping: EtsMappingResult, + path: String, + nonExactCode: String, + ): ProjectionCapability = if (mapping.status == EtsMappingStatus.EXACT && mapping.targets.size == 1) { + exact() + } else { + unsupported( + code = nonExactCode, + message = "USVM projection requires exactly one EtsIR target, got ${mapping.status}", + path = path, + ) + } + + internal fun domainCapabilityForProjector( + domain: PropertyDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (!domainCompatibilityForProjector(domain, etsType)) { + return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED, + message = "Domain ${domain::class.simpleName} cannot be projected into EtsIR type $etsType", + path = path, + ) + } + + return when (domain) { + BooleanDomain, is IntegerDomain, is NumberDomain -> exact() + is StringDomain -> approximateString(path) + is ConstantDomain -> constantCapability(domain.value, path) + is OptionalDomain -> domainCapabilityForProjector( + domain = domain.value, + etsType = nestedOptionalType(domain, etsType), + path = "$path.value", + options = options, + ) + + is TupleDomain -> tupleCapability(domain, etsType, path, options) + is ArrayDomain -> arrayCapability(domain, etsType, path, options) + } + } + + private fun tupleCapability( + domain: TupleDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (domain.elements.size > options.maxSymbolicCollectionLength) { + return collectionTooLarge(domain.elements.size, options, path) + } + + val elementTypes = when (etsType) { + is EtsTupleType -> etsType.types + is EtsArrayType -> List(domain.elements.size) { etsType.elementType } + else -> return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED, + message = "Tuple domain requires an EtsIR tuple or array type", + path = path, + ) + } + val elementCapabilities = domain.elements.mapIndexed { index, element -> + domainCapabilityForProjector(element, elementTypes[index], "$path.elements[$index]", options) + } + + return aggregateProjectionCapabilities(elementCapabilities) + } + + private fun arrayCapability( + domain: ArrayDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (domain.maxLength > options.maxSymbolicCollectionLength) { + return collectionTooLarge(domain.maxLength, options, path) + } + if ((etsType as EtsArrayType).elementType is EtsArrayType) { + return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_ARRAY_NESTED_UNSUPPORTED, + message = "Nested EtsIR arrays are not supported by the current TypeScript heap model", + path = path, + ) + } + + val elementType = etsType.elementType + + return domainCapabilityForProjector(domain.element, elementType, "$path.element", options) + } + + private fun collectionTooLarge( + actualLength: Int, + options: UsvmProjectionOptions, + path: String, + ) = unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_COLLECTION_TOO_LARGE, + message = "Collection length $actualLength exceeds the symbolic cap " + + options.maxSymbolicCollectionLength, + path = path, + ) + + internal fun domainCompatibilityForProjector(domain: PropertyDomain, etsType: EtsType): Boolean = when (domain) { + BooleanDomain -> etsType == EtsBooleanType || etsType is EtsBooleanLiteralType + is IntegerDomain, is NumberDomain -> etsType == EtsNumberType || etsType is EtsNumberLiteralType + is StringDomain -> etsType == EtsStringType || etsType is EtsStringLiteralType + is ConstantDomain -> isConstantCompatible(domain.value, etsType) + is OptionalDomain -> isOptionalCompatible(domain, etsType) + is TupleDomain -> when (etsType) { + is EtsTupleType -> { + etsType.types.size == domain.elements.size && + domain.elements.zip(etsType.types).all { (element, elementType) -> + domainCompatibilityForProjector(element, elementType) + } + } + + is EtsArrayType -> { + etsType.dimensions == 1 && + domain.elements.all { domainCompatibilityForProjector(it, etsType.elementType) } + } + + else -> false + } + + is ArrayDomain -> { + etsType is EtsArrayType && + etsType.dimensions == 1 && + domainCompatibilityForProjector(domain.element, etsType.elementType) + } + } + + private fun isConstantCompatible(value: JsConcreteValue, etsType: EtsType): Boolean = when (value) { + is JsConcreteValue.Boolean -> etsType == EtsBooleanType || etsType is EtsBooleanLiteralType + is JsConcreteValue.Number -> etsType == EtsNumberType || etsType is EtsNumberLiteralType + is JsConcreteValue.String -> etsType == EtsStringType || etsType is EtsStringLiteralType + JsConcreteValue.Null -> etsType == EtsNullType + JsConcreteValue.Undefined -> etsType == EtsUndefinedType + is JsConcreteValue.Array -> false + } + + private fun isOptionalCompatible(domain: OptionalDomain, etsType: EtsType): Boolean { + val union = etsType as? EtsUnionType ?: return false + val nilType = nilType(domain.nil) ?: return false + + return union.types.any { it == nilType } && + union.types.any { domainCompatibilityForProjector(domain.value, it) } + } + + private fun nestedOptionalType(domain: OptionalDomain, etsType: EtsType): EtsType { + val union = etsType as EtsUnionType + + return union.types.first { domainCompatibilityForProjector(domain.value, it) } + } + + private fun nilType(nil: JsConcreteValue): EtsType? = when (nil) { + JsConcreteValue.Null -> EtsNullType + JsConcreteValue.Undefined -> EtsUndefinedType + else -> null + } + + private fun constantCapability(value: JsConcreteValue, path: String): ProjectionCapability = when (value) { + is JsConcreteValue.String -> approximateString(path) + else -> exact() + } + + private fun approximateString(path: String): ProjectionCapability { + val diagnostic = CapabilityDiagnostic( + code = PbtDiagnosticCode.USVM_DOMAIN_STRING_APPROXIMATE, + message = "Over-approximation: USVM constrains string type and length, " + + "but leaves UTF-16 contents unconstrained", + path = path, + ) + + return ProjectionCapability( + level = ProjectionLevel.APPROXIMATE, + diagnostics = listOf(diagnostic), + ) + } + + private fun unsupported(code: String, message: String, path: String): ProjectionCapability { + val diagnostic = CapabilityDiagnostic(code = code, message = message, path = path) + + return ProjectionCapability( + level = ProjectionLevel.UNSUPPORTED, + diagnostics = listOf(diagnostic), + ) + } + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) +} + +internal fun EtsMappingResult.exactTargetOrNull(): EtsEntryPointTarget? = + targets.singleOrNull()?.takeIf { status == EtsMappingStatus.EXACT } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt new file mode 100644 index 0000000000..8cbb6d46c4 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt @@ -0,0 +1,30 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.PropertyCapabilityLevel + +/** Bounds resource usage while recursively materializing symbolic property inputs. */ +data class UsvmProjectionOptions( + val maxSymbolicCollectionLength: Int = 10, +) { + init { + require(maxSymbolicCollectionLength >= 0) { + "Maximum symbolic collection length must be non-negative" + } + } +} + +/** Capability of one ordered property input at its stable manifest path. */ +data class UsvmInputProjectionCapability( + val inputName: String, + val path: String, + val capability: ProjectionCapability, +) + +/** Combined concrete and symbolic execution capability for one property. */ +data class UsvmPropertyProjectionCapability( + val inputs: List, + val precondition: ProjectionCapability, + val symbolic: ProjectionCapability, + val property: PropertyCapabilityLevel, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt new file mode 100644 index 0000000000..b8e9910946 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt @@ -0,0 +1,310 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact + +/** Overall result of projecting and evaluating one declared precondition. */ +enum class UsvmPreconditionStatus { + ACCEPTED, + REJECTED, + PROPERTY_ERROR, + TIMEOUT, + SOLVER_UNKNOWN, + UNSUPPORTED, + ENGINE_FAILURE, +} + +/** Capability and terminal states satisfying a declared mapped precondition. */ +data class UsvmPreconditionResult( + val capability: UsvmPropertyProjectionCapability, + val status: UsvmPreconditionStatus, + val acceptedStates: List, + val diagnostics: List, +) { + init { + if (status == UsvmPreconditionStatus.ACCEPTED) { + require(acceptedStates.isNotEmpty()) { "An accepted precondition requires at least one state" } + } else { + require(acceptedStates.isEmpty()) { "Only an accepted precondition can expose states" } + } + } +} + +/** Orchestrates declared-domain materialization and mapped TypeScript precondition execution. */ +class UsvmPropertyProjector( + private val scene: EtsScene, + private val machineOptions: UMachineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + ), + private val tsOptions: TsOptions = TsOptions(), + private val projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val capabilityResolver = UsvmProjectionCapabilityResolver() + private val domainProjector = UsvmDomainProjector(projectionOptions) + + fun analyzePrecondition( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + ): UsvmPreconditionResult { + requireNotNull(manifest.precondition) { "Precondition analysis requires a declared precondition" } + + val capability = capabilityResolver.resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + val capabilityDiagnostics = capability.symbolic.diagnostics + if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { + return result( + capability = capability, + status = UsvmPreconditionStatus.UNSUPPORTED, + diagnostics = capabilityDiagnostics, + ) + } + + val preconditionTarget = mapping.precondition?.exactTargetOrNull() + ?: return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "An exact precondition target was unavailable after capability validation", + path = "precondition", + ), + ) + val execution = analyzePreconditionTarget(manifest, preconditionTarget) + + return classifyPreconditionAnalysis(capability, execution) + } + + private fun analyzePreconditionTarget( + manifest: PropertyManifest, + preconditionTarget: EtsEntryPointTarget, + ): UsvmPreconditionExecution = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + ).use { machine -> + val analysis = machine.analyzeWithMetadata( + methods = listOf(preconditionTarget.method), + configureInitialState = { method, state -> + check(method == preconditionTarget.method) { + "Unexpected precondition initial state for ${method.signature}" + } + + domainProjector.configure( + state = state, + inputs = manifest.inputs, + bindings = preconditionTarget.bindings.inputs, + ) + }, + ) + val canResolve = !analysis.timedOut && analysis.states.isNotEmpty() && analysis.states.all { state -> + val methodResult = state.methodResult as? TsMethodResult.Success + methodResult != null && methodResult.value.sort == state.ctx.boolSort + } + val resolutions = if (canResolve) { + analysis.states.map(::retainTruePreconditionState) + } else { + emptyList() + } + + UsvmPreconditionExecution(analysis, resolutions) + } + + private fun classifyPreconditionAnalysis( + capability: UsvmPropertyProjectionCapability, + execution: UsvmPreconditionExecution, + ): UsvmPreconditionResult { + val analysis = execution.analysis + val failure = classifyPreconditionFailure(capability, analysis) + if (failure != null) { + return failure + } + + val capabilityDiagnostics = capability.symbolic.diagnostics + val resolutions = execution.resolutions + if (resolutions.any { it is PreconditionStateResolution.SolverUnknown }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.SOLVER_UNKNOWN, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a precondition result", + path = "precondition.result", + ), + ) + } + val acceptedStates = resolutions.mapNotNull { resolution -> + (resolution as? PreconditionStateResolution.Accepted)?.state + } + val status = if (acceptedStates.isEmpty()) { + UsvmPreconditionStatus.REJECTED + } else { + UsvmPreconditionStatus.ACCEPTED + } + + return result( + capability = capability, + status = status, + acceptedStates = acceptedStates, + diagnostics = capabilityDiagnostics, + ) + } + + private fun classifyPreconditionFailure( + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPreconditionResult? { + val capabilityDiagnostics = capability.symbolic.diagnostics + val terminalStates = analysis.states + if (terminalStates.any { state -> state.methodResult is TsMethodResult.TsException }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.PROPERTY_ERROR, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, + message = "The precondition has a reachable escaping exception", + path = "precondition", + ), + ) + } + if (terminalStates.any { state -> state.methodResult !is TsMethodResult.Success }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Precondition analysis terminated without a method result", + path = "precondition", + ), + ) + } + val nonBooleanResult = terminalStates.any { state -> + val methodResult = state.methodResult as TsMethodResult.Success + methodResult.value.sort != state.ctx.boolSort + } + if (nonBooleanResult) { + return result( + capability = capability, + status = UsvmPreconditionStatus.PROPERTY_ERROR, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, + message = "The precondition returned a non-boolean symbolic value", + path = "precondition.result", + ), + ) + } + if (analysis.unsupportedCall) { + return result( + capability = capability, + status = UsvmPreconditionStatus.UNSUPPORTED, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, + message = "The symbolic engine encountered an unsupported precondition call", + path = "precondition", + ), + ) + } + if (analysis.engineFailed) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The symbolic engine could not execute every reachable precondition path", + path = "precondition", + ), + ) + } + if (analysis.timedOut) { + return result( + capability = capability, + status = UsvmPreconditionStatus.TIMEOUT, + diagnostics = capabilityDiagnostics, + ) + } + if (terminalStates.isEmpty()) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Precondition analysis produced no terminal states", + path = "precondition", + ), + ) + } + + return null + } + + private fun retainTruePreconditionState(state: TsState): PreconditionStateResolution { + val result = state.methodResult as TsMethodResult.Success + val returnValue = with(state.ctx) { + result.value.asExpr(boolSort) + } + val acceptedState = state.clone() + acceptedState.pathConstraints += returnValue + val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints) + + return when (solverResult) { + is USatResult -> { + acceptedState.models = listOf(solverResult.model) + PreconditionStateResolution.Accepted(acceptedState) + } + + is UUnsatResult -> PreconditionStateResolution.Rejected + is UUnknownResult -> PreconditionStateResolution.SolverUnknown + } + } + + private fun result( + capability: UsvmPropertyProjectionCapability, + status: UsvmPreconditionStatus, + diagnostics: List, + acceptedStates: List = emptyList(), + ) = UsvmPreconditionResult( + capability = capability, + status = status, + acceptedStates = acceptedStates, + diagnostics = diagnostics, + ) + + private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( + code = code, + message = message, + path = path, + ) +} + +private data class UsvmPreconditionExecution( + val analysis: TsMachineAnalysisResult, + val resolutions: List, +) + +private sealed interface PreconditionStateResolution { + data class Accepted(val state: TsState) : PreconditionStateResolution + data object Rejected : PreconditionStateResolution + data object SolverUnknown : PreconditionStateResolution +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt new file mode 100644 index 0000000000..8b3c531817 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -0,0 +1,54 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId + +/** Terminal outcome of one USVM property-violation search. */ +enum class UsvmPropertySearchStatus { + VIOLATION_REACHED, + NO_VIOLATION_REACHED, + PRECONDITION_REJECTED, + PROPERTY_ERROR, + TIMEOUT, + SOLVER_UNKNOWN, + UNSUPPORTED, + ENGINE_FAILURE, + FAILED_INPUT_RESOLUTION, +} + +/** Supported ways in which a mapped predicate can violate its property. */ +enum class UsvmPropertyViolationTarget { + PREDICATE_FALSE, + UNEXPECTED_EXCEPTION, + ASSERTION_FAILURE, +} + +/** Backend-neutral result of searching one mapped TypeScript property with USVM. */ +data class UsvmPropertySearchResult( + val propertyId: PropertyId, + val status: UsvmPropertySearchStatus, + val target: UsvmPropertyViolationTarget?, + val inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, +) { + init { + when (status) { + UsvmPropertySearchStatus.VIOLATION_REACHED -> { + requireNotNull(target) { "A reached violation requires its target" } + requireNotNull(inputs) { "A resolved violation requires candidate inputs" } + } + + UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION -> { + requireNotNull(target) { "An input-resolution failure requires its reached target" } + require(inputs == null) { "An input-resolution failure cannot contain candidate inputs" } + } + + else -> { + require(target == null) { "A result without a violation cannot contain a target" } + require(inputs == null) { "A result without a violation cannot contain candidate inputs" } + } + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt new file mode 100644 index 0000000000..9522aedb42 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -0,0 +1,441 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.targets.TsTarget +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsEntryPointGuardOutcome +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.state.prependBooleanEntryPointGuard +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult +import org.usvm.statistics.UMachineObserver +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.PropertyId + +/** Searches mapped TypeScript predicates for concrete property violations with USVM. */ +class UsvmPropertySearcher( + private val scene: EtsScene, + machineOptions: UMachineOptions = UMachineOptions(), + private val tsOptions: TsOptions = TsOptions(), + private val projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val machineOptions = machineOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL) + private val capabilityResolver = UsvmProjectionCapabilityResolver() + private val domainProjector = UsvmDomainProjector(projectionOptions) + private val inputResolver = UsvmCandidateInputResolver() + + fun search( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + ): UsvmPropertySearchResult { + val capability = capabilityResolver.resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + val capabilityDiagnostics = capability.symbolic.diagnostics + if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.UNSUPPORTED, + capability = capability, + diagnostics = capabilityDiagnostics, + ) + } + + val predicate = mapping.predicate.exactTargetOrNull() + ?: return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "An exact predicate target was unavailable after capability validation", + path = "predicate", + ), + ) + val precondition = mapping.precondition?.exactTargetOrNull() + val execution = executeSearch(manifest, predicate, precondition) + val terminalFailure = classifyTerminalFailure( + manifest = manifest, + capability = capability, + analysis = execution.analysis, + ) + if (terminalFailure != null) { + return terminalFailure + } + + val violationState = execution.observer.violationStates.firstOrNull() + ?: return noViolationResult( + manifest = manifest, + capability = capability, + analysis = execution.analysis, + observer = execution.observer, + ) + + return violationResult( + manifest = manifest, + capability = capability, + violationState = violationState, + projection = execution.projection, + ) + } + + private fun executeSearch( + manifest: PropertyManifest, + predicate: EtsEntryPointTarget, + precondition: EtsEntryPointTarget?, + ): UsvmSearchExecution { + lateinit var projection: UsvmDeclaredDomainProjection + val target = UsvmViolationTsTarget() + val observer = UsvmViolationObserver(target) + val analysis = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = observer, + ).use { machine -> + machine.analyzeWithMetadata( + methods = listOf(predicate.method), + targets = listOf(target), + configureInitialState = { method, state -> + check(method == predicate.method) + projection = domainProjector.configure( + state = state, + inputs = manifest.inputs, + bindings = predicate.bindings.inputs, + ) + if (precondition != null) { + state.prependBooleanEntryPointGuard( + guard = precondition.method, + arguments = projection.inputs.map(UsvmProjectedInput::value), + ) + } + }, + ) + } + + return UsvmSearchExecution( + analysis = analysis, + observer = observer, + projection = projection, + ) + } + + private fun classifyTerminalFailure( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPropertySearchResult? { + val preconditionFailure = classifyPreconditionFailure(manifest, capability, analysis) + if (preconditionFailure != null) { + return preconditionFailure + } + + val capabilityDiagnostics = capability.symbolic.diagnostics + val predicateContractError = analysis.states.any { state -> + val methodResult = state.methodResult as? TsMethodResult.Success + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + methodResult != null && + methodResult.value.sort != state.ctx.boolSort + } + if (predicateContractError) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.PROPERTY_ERROR, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PREDICATE_RESULT_NON_BOOLEAN, + message = "The predicate returned a non-boolean symbolic value", + path = "predicate.result", + ), + ) + } + val missingPredicateResult = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + state.methodResult == TsMethodResult.NoCall + } + if (missingPredicateResult) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Predicate analysis terminated without a method result", + path = "predicate", + ), + ) + } + if (analysis.unsupportedCall) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.UNSUPPORTED, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, + message = "The symbolic engine encountered an unsupported property call", + path = "predicate", + ), + ) + } + if (analysis.engineFailed) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The symbolic engine could not execute every reachable property path", + path = "predicate", + ), + ) + } + + return null + } + + private fun classifyPreconditionFailure( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPropertySearchResult? { + val capabilityDiagnostics = capability.symbolic.diagnostics + val preconditionError = analysis.states.firstOrNull { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR + } + ?: return null + val diagnostic = when (preconditionError.methodResult) { + is TsMethodResult.TsException -> diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, + message = "The precondition has a reachable escaping exception", + path = "precondition", + ) + + is TsMethodResult.Success -> diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, + message = "The precondition returned a non-boolean symbolic value", + path = "precondition.result", + ) + + TsMethodResult.NoCall -> diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The precondition guard terminated without a method result", + path = "precondition", + ) + } + val status = if (preconditionError.methodResult == TsMethodResult.NoCall) { + UsvmPropertySearchStatus.ENGINE_FAILURE + } else { + UsvmPropertySearchStatus.PROPERTY_ERROR + } + + return result( + manifest = manifest, + status = status, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic, + ) + } + + private fun noViolationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + observer: UsvmViolationObserver, + ): UsvmPropertySearchResult { + val capabilityDiagnostics = capability.symbolic.diagnostics + val predicateCompleted = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + state.methodResult is TsMethodResult.Success + } + val preconditionRejected = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.REJECTED + } + val status = when { + analysis.timedOut -> UsvmPropertySearchStatus.TIMEOUT + observer.solverUnknown -> UsvmPropertySearchStatus.SOLVER_UNKNOWN + predicateCompleted -> UsvmPropertySearchStatus.NO_VIOLATION_REACHED + preconditionRejected -> UsvmPropertySearchStatus.PRECONDITION_REJECTED + else -> UsvmPropertySearchStatus.ENGINE_FAILURE + } + val diagnostics = when (status) { + UsvmPropertySearchStatus.SOLVER_UNKNOWN -> capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a predicate result", + path = "predicate.result", + ) + + UsvmPropertySearchStatus.ENGINE_FAILURE -> capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Property search produced no classified terminal state", + path = "predicate", + ) + + else -> capabilityDiagnostics + } + + return result( + manifest = manifest, + status = status, + capability = capability, + diagnostics = diagnostics, + ) + } + + private fun violationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + violationState: TsState, + projection: UsvmDeclaredDomainProjection, + ): UsvmPropertySearchResult { + val capabilityDiagnostics = capability.symbolic.diagnostics + val violationTarget = classifyViolation(violationState) + val inputs = runCatching { + inputResolver.resolve(violationState, manifest.inputs, projection) + }.getOrElse { failure -> + val diagnostic = CapabilityDiagnostic( + code = PbtDiagnosticCode.USVM_INPUT_RESOLUTION_FAILED, + message = failure.message ?: "Failed to resolve symbolic property inputs", + path = "inputs", + ) + + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, + target = violationTarget, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic, + ) + } + + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.VIOLATION_REACHED, + target = violationTarget, + inputs = inputs, + capability = capability, + diagnostics = capabilityDiagnostics, + ) + } + + private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( + code = code, + message = message, + path = path, + ) + + private fun classifyViolation(state: TsState): UsvmPropertyViolationTarget { + return when (val result = state.methodResult) { + is TsMethodResult.Success -> { + UsvmPropertyViolationTarget.PREDICATE_FALSE + } + + is TsMethodResult.TsException -> { + val message = with(state.ctx) { + val ref = state.models.single().eval(result.value) as? org.usvm.UConcreteHeapRef + ref?.takeIf(::isAllocatedConcreteHeapRef)?.let(::getStringConstantValue) + } + if (message?.contains("AssertionError") == true) { + UsvmPropertyViolationTarget.ASSERTION_FAILURE + } else { + UsvmPropertyViolationTarget.UNEXPECTED_EXCEPTION + } + } + + TsMethodResult.NoCall -> { + error("Reached a violation target without a predicate result") + } + } + } + + private fun result( + manifest: PropertyManifest, + status: UsvmPropertySearchStatus, + capability: UsvmPropertyProjectionCapability, + diagnostics: List, + target: UsvmPropertyViolationTarget? = null, + inputs: List? = null, + ) = UsvmPropertySearchResult( + propertyId = PropertyId(manifest.propertyId), + status = status, + target = target, + inputs = inputs, + capability = capability, + diagnostics = diagnostics, + ) +} + +private data class UsvmSearchExecution( + val analysis: TsMachineAnalysisResult, + val observer: UsvmViolationObserver, + val projection: UsvmDeclaredDomainProjection, +) + +private class UsvmViolationTsTarget : TsTarget(location = null) + +private class UsvmViolationObserver( + private val target: UsvmViolationTsTarget, +) : UMachineObserver { + private val mutableViolationStates = mutableListOf() + + val violationStates: List + get() = mutableViolationStates + + var solverUnknown: Boolean = false + private set + + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + if ( + !stateReachable || + state.entryPointGuardActive || + state.entryPointGuardOutcome != TsEntryPointGuardOutcome.NONE + ) { + return + } + + when (val result = state.methodResult) { + is TsMethodResult.TsException -> recordViolation(state) + is TsMethodResult.Success -> with(state.ctx) { + val returnValue = result.value.takeIf { it.sort == boolSort }?.asExpr(boolSort) ?: return@with + val candidateState = state.clone() + candidateState.pathConstraints += returnValue.not() + val solverResult = solver().check(candidateState.pathConstraints) + + when (solverResult) { + is USatResult -> { + candidateState.models = listOf(solverResult.model) + recordViolation(candidateState) + } + + is UUnsatResult -> Unit + is UUnknownResult -> solverUnknown = true + } + } + + TsMethodResult.NoCall -> Unit + } + } + + private fun recordViolation(state: TsState) { + target.propagate(state) + mutableViolationStates += state + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt new file mode 100644 index 0000000000..8c4aa193a9 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt @@ -0,0 +1,263 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +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.fastcheck.BackendErrorKind +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +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.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.testResourcePath +import org.usvm.ts.pbt.testResourcesRoot +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class PropertyExecutionConformanceTest { + @Test + fun `shared preconditions have the same concrete projection and search classification`() { + val cases = listOf( + ContractCase("truePrecondition", ContractOutcome.HOLDS), + ContractCase("falsePrecondition", ContractOutcome.PRECONDITION_REJECTED), + ContractCase( + exportName = "throwingPrecondition", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.precondition.threw", + path = "manifest.precondition", + ), + ), + ContractCase( + exportName = "nonBooleanPrecondition", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.result.invalid", + path = "manifest.precondition.result", + ), + ), + ) + + cases.forEach { case -> + val property = property( + predicateExport = "alwaysTrue", + preconditionExport = case.exportName, + ) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteOutcome = concreteOutcome(property, case.expectedBackendError) + val projectionOutcome = projectionOutcome( + projector.analyzePrecondition(manifest, mapping, exactCapability), + ) + val searchOutcome = searchOutcome( + searcher.search(manifest, mapping, exactCapability), + ) + + assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") + assertEquals(case.expected, projectionOutcome, "${case.exportName}: projection") + assertEquals(case.expected, searchOutcome, "${case.exportName}: search") + } + } + + @Test + fun `shared predicates have the same concrete and search classification`() { + val cases = listOf( + ContractCase("falsePredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("throwingPredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("literalFalsePredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("literalTruePredicate", ContractOutcome.HOLDS), + ContractCase("neverPredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase( + exportName = "nonBooleanPredicate", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.result.invalid", + path = "manifest.predicate.result", + ), + ), + ) + + cases.forEach { case -> + val property = property(predicateExport = case.exportName) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteOutcome = concreteOutcome(property, case.expectedBackendError) + val searchOutcome = searchOutcome( + searcher.search(manifest, mapping, exactCapability), + ) + + assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") + assertEquals(case.expected, searchOutcome, "${case.exportName}: search") + } + } + + @Test + fun `symbolic candidates retain inputs from before predicate mutation`() { + val domain = ArrayDomain( + element = IntegerDomain(min = 1, max = 1), + minLength = 1, + maxLength = 1, + ) + val property = property( + predicateExport = "mutatesAndFails", + domain = domain, + ) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteResult = backend.run(property, configuration) + val searchResult = searcher.search(manifest, mapping, exactCapability) + + val expectedInput = JsConcreteValue.Array( + elements = listOf(JsConcreteValue.number(1.0)), + ) + val symbolicInputs = assertNotNull(searchResult.inputs) + assertEquals(PropertyFailureKind.PROPERTY, concreteResult.failure?.kind) + assertEquals(listOf(expectedInput), concreteResult.counterexample) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, searchResult.status) + assertEquals(listOf(expectedInput), symbolicInputs) + assertTrue(symbolicInputs.single() in domain) + + val replay = backend.run( + property = property, + configuration = configuration.copy( + numRuns = 1, + examples = listOf(symbolicInputs), + ), + ) + + assertEquals(PropertyFailureKind.PROPERTY, replay.failure?.kind) + assertEquals(symbolicInputs, replay.counterexample) + } + + private fun concreteOutcome( + property: PropertyDefinition, + expectedBackendError: BackendErrorExpectation?, + ): ContractOutcome = try { + val result = backend.run(property, configuration) + + when (result.status) { + PropertyRunStatus.SUCCESS -> ContractOutcome.HOLDS + PropertyRunStatus.FAILURE -> when (result.failure?.kind) { + PropertyFailureKind.PROPERTY -> ContractOutcome.PREDICATE_VIOLATION + PropertyFailureKind.PRECONDITION_EXHAUSTED -> ContractOutcome.PRECONDITION_REJECTED + PropertyFailureKind.TIMEOUT, null -> error("Unexpected concrete result: $result") + } + } + } catch (failure: PbtBackendException) { + val expected = checkNotNull(expectedBackendError) { + "Unexpected concrete backend error: ${failure.kind}/${failure.code} at ${failure.path}" + } + + assertEquals(BackendErrorKind.ENTRY_POINT, failure.kind) + assertEquals(expected.code, failure.code) + assertEquals(expected.path, failure.path) + + ContractOutcome.PROPERTY_ERROR + } + + private fun projectionOutcome(result: UsvmPreconditionResult): ContractOutcome = when (result.status) { + UsvmPreconditionStatus.ACCEPTED -> ContractOutcome.HOLDS + UsvmPreconditionStatus.REJECTED -> ContractOutcome.PRECONDITION_REJECTED + UsvmPreconditionStatus.PROPERTY_ERROR -> ContractOutcome.PROPERTY_ERROR + else -> error("Unexpected projection result: $result") + } + + private fun searchOutcome(result: UsvmPropertySearchResult): ContractOutcome = when (result.status) { + UsvmPropertySearchStatus.VIOLATION_REACHED -> ContractOutcome.PREDICATE_VIOLATION + UsvmPropertySearchStatus.NO_VIOLATION_REACHED -> ContractOutcome.HOLDS + UsvmPropertySearchStatus.PRECONDITION_REJECTED -> ContractOutcome.PRECONDITION_REJECTED + UsvmPropertySearchStatus.PROPERTY_ERROR -> ContractOutcome.PROPERTY_ERROR + else -> error("Unexpected search result: $result") + } + + private fun property( + predicateExport: String, + preconditionExport: String? = null, + domain: org.usvm.ts.pbt.model.PropertyDomain = IntegerDomain(min = 0, max = 0), + ) = PropertyDefinition( + id = PropertyId("contract.$predicateExport.${preconditionExport ?: "none"}"), + inputs = listOf( + PropertyInput( + name = "value", + domain = domain, + ), + ), + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = predicateExport, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = MODULE, + exportName = exportName, + ) + }, + ) + + private data class ContractCase( + val exportName: String, + val expected: ContractOutcome, + val expectedBackendError: BackendErrorExpectation? = null, + ) + + private data class BackendErrorExpectation( + val code: String, + val path: String, + ) + + private enum class ContractOutcome { + HOLDS, + PRECONDITION_REJECTED, + PREDICATE_VIOLATION, + PROPERTY_ERROR, + } + + companion object { + private const val MODULE = "PropertyExecutionContract.ts" + + private val exactCapability = ProjectionCapability(level = ProjectionLevel.EXACT) + private val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 1, + timeoutMillis = 1_000, + ) + private val fixtureDirectory = testResourcesRoot().resolve("properties/contract") + private val backend = FastCheckBackend(sourceRoots = listOf(fixtureDirectory)) + private lateinit var mapper: PropertyEtsMapper + private lateinit var projector: UsvmPropertyProjector + private lateinit var searcher: UsvmPropertySearcher + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/properties/contract/$MODULE") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + + mapper = PropertyEtsMapper( + scene = scene, + sourceRoots = listOf(fixtureDirectory), + ) + projector = UsvmPropertyProjector(scene) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt new file mode 100644 index 0000000000..b18601d748 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt @@ -0,0 +1,175 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmCollectionDomainProjectorTest { + @Test + fun `array length and every active element satisfy their recursive domains`() { + val domain = ArrayDomain( + element = IntegerDomain(min = -1, max = 1), + minLength = 1, + maxLength = 2, + ) + + assertTrue(acceptsArray(domain, length = 1, elements = listOf(-1.0))) + assertTrue(acceptsArray(domain, length = 2, elements = listOf(-1.0, 1.0))) + assertFalse(acceptsArray(domain, length = 0, elements = emptyList())) + assertFalse(acceptsArray(domain, length = 3, elements = listOf(0.0, 0.0))) + assertFalse(acceptsArray(domain, length = 2, elements = listOf(0.0, 2.0))) + } + + @Test + fun `tuple has exact length and positional recursive domains`() { + val domain = TupleDomain(listOf(IntegerDomain(min = 2, max = 4), BooleanDomain)) + + assertTrue(acceptsTuple(domain, number = 3.0, boolean = true, length = 2)) + assertTrue(acceptsTuple(domain, number = 4.0, boolean = false, length = 2)) + assertFalse(acceptsTuple(domain, number = 1.0, boolean = true, length = 2)) + assertFalse(acceptsTuple(domain, number = 3.0, boolean = true, length = 1)) + } + + @Test + fun `oversized arrays are rejected before materialization`() { + val domain = ArrayDomain(IntegerDomain(), maxLength = 3) + val manifest = manifest(domain, exportName = "acceptsNumberArray") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + val projector = UsvmDomainProjector( + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 2), + ) + + assertFailsWith { + analyze(target.method) { state -> + projector.configure(state, manifest.inputs, target.bindings.inputs) + } + } + } + + private fun acceptsArray(domain: ArrayDomain, length: Int, elements: List): Boolean { + val manifest = manifest(domain, exportName = "acceptsNumberArray") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return runCatchingAnalyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val array = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(array, arrayType)) + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + elements.forEachIndexed { index, element -> + val lValue = mkArrayIndexLValue(fp64Sort, array, mkBv(index), arrayType) + val projectedElement = state.memory.read(lValue) + + state.pathConstraints += mkEq(projectedElement, mkFp(element, fp64Sort)) + } + } + } + } + + private fun acceptsTuple( + domain: TupleDomain, + number: Double, + boolean: Boolean, + length: Int, + ): Boolean { + val manifest = manifest(domain, exportName = "acceptsNumberBooleanTuple") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return runCatchingAnalyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val tuple = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(tuple, arrayType)) + val numberBox = state.memory.read( + mkArrayIndexLValue(addressSort, tuple, mkBv(0), arrayType), + ) as UConcreteHeapRef + val booleanBox = state.memory.read( + mkArrayIndexLValue(addressSort, tuple, mkBv(1), arrayType), + ) as UConcreteHeapRef + + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + state.pathConstraints += mkEq(numberBox.extractFp(state.memory), mkFp(number, fp64Sort)) + state.pathConstraints += mkEq(booleanBox.extractBool(state.memory), mkBool(boolean)) + } + } + } + + private fun manifest(domain: PropertyDomain, exportName: String) = PropertyManifest( + propertyId = "usvm.collection.$exportName", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + ), + ) + + private fun runCatchingAnalyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ): Boolean = runCatching { analyze(method, configure) }.isSuccess + + private fun analyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ) { + TsMachine( + scene = scene, + options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { _, state -> configure(state) }, + ) + } + } + + companion object { + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private val projector = UsvmDomainProjector() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt new file mode 100644 index 0000000000..c9a988ef7b --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt @@ -0,0 +1,110 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmInitialStateConfigurationTest { + @Test + fun `initial state configuration participates in the first solver model`() { + val source = testResourcePath("/mapping/PropertyMappingFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + val method = scene.projectClasses + .flatMap { etsClass -> etsClass.methods } + .single { candidate -> candidate.name == "isPositive" } + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL) + + val states = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { configuredMethod, state -> + assertEquals(method, configuredMethod) + + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + state.pathConstraints += mkFpEqualExpr(input, mkFp(7.0, fp64Sort)) + } + }, + ) + } + + assertTrue(states.isNotEmpty()) + states.forEach { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + val evaluated = state.models.single().eval(input) + + assertEquals(mkFp(7.0, fp64Sort), evaluated) + } + } + } + + @Test + fun `ordinary constraint pruning is not reported as an engine failure`() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + val manifest = PropertyManifest( + propertyId = "usvm.constraint-pruning", + inputs = listOf( + PropertyInput( + name = "value", + domain = ArrayDomain( + element = IntegerDomain(min = 0, max = 0), + minLength = 2, + maxLength = 2, + ), + ), + ), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = "acceptsNumberArray", + ), + ) + val mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + val predicate = requireNotNull(mapper.map(manifest).predicate.exactTargetOrNull()) + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL) + + val analysis = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(maxArraySize = 1), + ).use { machine -> + machine.analyzeWithMetadata( + methods = listOf(predicate.method), + configureInitialState = { _, state -> + UsvmDomainProjector().configure( + state = state, + inputs = manifest.inputs, + bindings = predicate.bindings.inputs, + ) + }, + ) + } + + assertEquals(emptyList(), analysis.states) + assertFalse(analysis.engineFailed) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt new file mode 100644 index 0000000000..ab0348c037 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt @@ -0,0 +1,124 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.isTrue +import org.usvm.machine.state.TsMethodResult +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class UsvmPreconditionProjectionTest { + @Test + fun `mapped precondition retains only satisfiable true states inside the declared domain`() { + val manifest = manifest(preconditionExport = "isPositive") + val mapping = mapper.map(manifest) + + val result = projector.analyzePrecondition(manifest, mapping, exact()) + + assertEquals(ProjectionLevel.EXACT, result.capability.symbolic.level) + assertEquals(UsvmPreconditionStatus.ACCEPTED, result.status) + assertTrue(result.acceptedStates.isNotEmpty()) + result.acceptedStates.forEach { state -> + assertTrue(state.methodResult is TsMethodResult.Success) + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + val value = state.models.single().eval(input) + + assertTrue(mkFpGreaterExpr(value, mkFp(0.0, fp64Sort)).isTrue) + assertTrue(mkFpLessOrEqualExpr(value, mkFp(3.0, fp64Sort)).isTrue) + } + } + } + + @Test + fun `false-only states are rejected and unsupported exception construction is explicit`() { + val falseManifest = manifest(preconditionExport = "alwaysFalse") + val throwingManifest = manifest(preconditionExport = "acceptsNonPositiveOrThrows") + + val falseResult = projector.analyzePrecondition(falseManifest, mapper.map(falseManifest), exact()) + val throwingResult = projector.analyzePrecondition(throwingManifest, mapper.map(throwingManifest), exact()) + + assertEquals(emptyList(), falseResult.acceptedStates) + assertEquals(UsvmPreconditionStatus.REJECTED, falseResult.status) + assertEquals(emptyList(), throwingResult.acceptedStates) + assertEquals(UsvmPreconditionStatus.UNSUPPORTED, throwingResult.status) + assertTrue(throwingResult.diagnostics.any { it.code == "usvm.execution.unsupported" }) + } + + @Test + fun `async preconditions are unsupported and non-boolean preconditions are property errors`() { + val asyncManifest = manifest( + preconditionExport = "asyncIsPositive", + executionKind = ExecutionKind.ASYNC, + ) + val nonBooleanManifest = manifest(preconditionExport = "returnsNumber") + + val asyncResult = projector.analyzePrecondition(asyncManifest, mapper.map(asyncManifest), exact()) + val nonBooleanResult = projector.analyzePrecondition( + nonBooleanManifest, + mapper.map(nonBooleanManifest), + exact(), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, asyncResult.capability.precondition.level) + assertEquals(UsvmPreconditionStatus.UNSUPPORTED, asyncResult.status) + assertEquals(emptyList(), asyncResult.acceptedStates) + assertEquals(ProjectionLevel.EXACT, nonBooleanResult.capability.precondition.level) + assertEquals(UsvmPreconditionStatus.PROPERTY_ERROR, nonBooleanResult.status) + assertEquals(emptyList(), nonBooleanResult.acceptedStates) + assertTrue(nonBooleanResult.diagnostics.any { it.code == "usvm.precondition.result.non-boolean" }) + } + + private fun manifest( + preconditionExport: String, + executionKind: ExecutionKind = ExecutionKind.SYNC, + ) = PropertyManifest( + propertyId = "usvm.precondition.$preconditionExport.${executionKind.name.lowercase()}", + inputs = listOf( + PropertyInput( + name = "value", + domain = IntegerDomain(min = -2, max = 3), + ), + ), + predicate = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = "predicate", + ), + precondition = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = preconditionExport, + executionKind = executionKind, + ), + ) + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private lateinit var projector: UsvmPropertyProjector + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmPreconditionFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + projector = UsvmPropertyProjector(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt new file mode 100644 index 0000000000..5ba1249988 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt @@ -0,0 +1,208 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCapabilityLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +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.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import kotlin.test.assertEquals + +class UsvmProjectionCapabilityTest { + @Test + fun `reports scalar fidelity and type mismatches`() { + val cases = listOf( + Case(BooleanDomain, "acceptsBoolean", ProjectionLevel.EXACT, emptyList()), + Case(IntegerDomain(min = -2, max = 3), "acceptsNumber", ProjectionLevel.EXACT, emptyList()), + Case(NumberDomain(allowNaN = false), "acceptsNumber", ProjectionLevel.EXACT, emptyList()), + Case(StringDomain(maxLength = 4), "acceptsString", ProjectionLevel.APPROXIMATE, listOf("inputs[0].domain")), + Case( + ConstantDomain(JsConcreteValue.Boolean(value = true)), + "acceptsBoolean", + ProjectionLevel.EXACT, + emptyList(), + ), + Case(IntegerDomain(), "acceptsString", ProjectionLevel.UNSUPPORTED, listOf("inputs[0].domain")), + ) + + cases.forEach { case -> + val capability = resolve(case.domain, case.exportName) + + assertEquals(case.level, capability.symbolic.level, case.exportName) + assertEquals(case.diagnosticPaths, capability.symbolic.diagnostics.map { it.path }, case.exportName) + } + } + + @Test + fun `recursive domains inherit the least capable nested projection`() { + val optional = resolve( + domain = OptionalDomain(IntegerDomain(min = 0, max = 5)), + exportName = "acceptsOptionalNumber", + ) + val tuple = resolve( + domain = TupleDomain(listOf(IntegerDomain(), StringDomain(maxLength = 3))), + exportName = "acceptsTuple", + ) + val array = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 4), + exportName = "acceptsNumberArray", + ) + val oversizedArray = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 11), + exportName = "acceptsNumberArray", + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 10), + ) + + assertEquals(ProjectionLevel.EXACT, optional.symbolic.level) + assertEquals(ProjectionLevel.APPROXIMATE, tuple.symbolic.level) + assertEquals(listOf("inputs[0].domain.elements[1]"), tuple.symbolic.diagnostics.map { it.path }) + assertEquals(ProjectionLevel.EXACT, array.symbolic.level) + assertEquals(ProjectionLevel.UNSUPPORTED, oversizedArray.symbolic.level) + assertEquals(listOf("inputs[0].domain"), oversizedArray.symbolic.diagnostics.map { it.path }) + } + + @Test + fun `reports unsupported mapping and execution boundaries without classifying property errors`() { + val manifest = manifest(IntegerDomain(), predicateExport = "acceptsNumber") + val mapping = mapper.map(manifest) + val nonExactMapping = mapping.copy( + predicate = mapping.predicate.copy( + status = EtsMappingStatus.UNMAPPED, + targets = emptyList(), + diagnostics = listOf( + EtsMappingDiagnostic( + code = "test.mapping.unmapped", + message = "Synthetic unmapped predicate", + ), + ), + ), + ) + val asyncPreconditionManifest = manifest( + domain = IntegerDomain(), + predicateExport = "acceptsNumber", + preconditionExport = "acceptsNumber", + preconditionExecutionKind = ExecutionKind.ASYNC, + ) + val nonBooleanPreconditionManifest = manifest( + domain = IntegerDomain(), + predicateExport = "acceptsNumber", + preconditionExport = "returnsNumber", + ) + + val nonExact = resolver.resolve(manifest, nonExactMapping, exact()) + val async = resolver.resolve( + asyncPreconditionManifest, + mapper.map(asyncPreconditionManifest), + exact(), + ) + val nonBoolean = resolver.resolve( + nonBooleanPreconditionManifest, + mapper.map(nonBooleanPreconditionManifest), + exact(), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, nonExact.symbolic.level) + assertEquals( + "predicate", + nonExact.symbolic.diagnostics.single { it.code == "usvm.predicate.mapping.non-exact" }.path, + ) + assertEquals(ProjectionLevel.UNSUPPORTED, async.precondition.level) + assertEquals("precondition", async.precondition.diagnostics.single().path) + assertEquals(ProjectionLevel.EXACT, nonBoolean.precondition.level) + assertEquals(emptyList(), nonBoolean.precondition.diagnostics) + } + + @Test + fun `derives concrete only from a supported concrete projection`() { + val capability = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 11), + exportName = "acceptsNumberArray", + concreteCapability = exact(), + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 10), + ) + + assertEquals(PropertyCapabilityLevel.CONCRETE_ONLY, capability.property) + } + + private fun resolve( + domain: org.usvm.ts.pbt.model.PropertyDomain, + exportName: String, + concreteCapability: ProjectionCapability = exact(), + options: UsvmProjectionOptions = UsvmProjectionOptions(), + ): UsvmPropertyProjectionCapability { + val manifest = manifest(domain, predicateExport = exportName) + + return resolver.resolve( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = concreteCapability, + options = options, + ) + } + + private fun manifest( + domain: org.usvm.ts.pbt.model.PropertyDomain, + predicateExport: String, + preconditionExport: String? = null, + preconditionExecutionKind: ExecutionKind = ExecutionKind.SYNC, + ) = PropertyManifest( + propertyId = "usvm.capability.$predicateExport", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = predicateExport, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + executionKind = preconditionExecutionKind, + ) + }, + ) + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) + + private data class Case( + val domain: org.usvm.ts.pbt.model.PropertyDomain, + val exportName: String, + val level: ProjectionLevel, + val diagnosticPaths: List, + ) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private val resolver = UsvmProjectionCapabilityResolver() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + + mapper = PropertyEtsMapper( + scene = EtsScene(listOf(file)), + sourceRoots = listOf(source.parent), + ) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt new file mode 100644 index 0000000000..bca45b6dca --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt @@ -0,0 +1,48 @@ +package org.usvm.ts.pbt.usvm + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.fastcheck.FastCheckProjectionClient +import org.usvm.ts.pbt.fastcheck.FastCheckProjectionRequest +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsNumber +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.contains +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class UsvmProjectionConformanceTest { + @Test + fun `fast-check samples satisfy the same domains used by USVM constraint tests`() { + val domains = listOf( + IntegerDomain(min = -5, max = 7), + NumberDomain( + min = JsNumber.finite(-1.5), + max = JsNumber.finite(2.5), + allowNaN = false, + ), + OptionalDomain(IntegerDomain(min = 1, max = 3)), + TupleDomain(listOf(IntegerDomain(min = 2, max = 4), BooleanDomain)), + ArrayDomain(IntegerDomain(min = -1, max = 1), minLength = 1, maxLength = 3), + ) + val response = FastCheckProjectionClient().sample( + FastCheckProjectionRequest( + seed = 351, + numSamples = 50, + domains = domains, + ), + ) + + assertEquals(50, response.samples.size) + response.samples.forEach { sample -> + assertEquals(domains.size, sample.size) + sample.zip(domains).forEach { (value, domain) -> + assertTrue(value in domain, "$value is outside $domain") + } + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt new file mode 100644 index 0000000000..676e70b781 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -0,0 +1,231 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +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.OptionalDomain +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.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.testResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class UsvmPropertySearcherTest { + @Test + fun `reports when no violation is reachable`() { + val manifest = manifest(predicateExport = "validProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + assertEquals(PropertyId(manifest.propertyId), result.propertyId) + assertNull(result.target) + assertNull(result.inputs) + } + + @Test + fun `finds false predicate and resolves a candidate input`() { + val manifest = manifest(predicateExport = "violatedProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertEquals(listOf(JsConcreteValue.number(2.0)), result.inputs) + } + + @Test + fun `applies mapped precondition before searching the predicate`() { + val manifest = manifest( + predicateExport = "signedOneProperty", + preconditionExport = "positive", + ) + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(listOf(JsConcreteValue.number(1.0)), result.inputs) + } + + @Test + fun `distinguishes rejected and exceptional preconditions from predicate violations`() { + val rejected = manifest( + predicateExport = "violatedProperty", + preconditionExport = "falsePrecondition", + ) + val exceptional = manifest( + predicateExport = "violatedProperty", + preconditionExport = "throwingPrecondition", + ) + + val rejectedResult = search(rejected) + val exceptionalResult = search(exceptional) + + assertEquals(UsvmPropertySearchStatus.PRECONDITION_REJECTED, rejectedResult.status) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, exceptionalResult.status) + assertNull(rejectedResult.target) + assertNull(exceptionalResult.target) + assertTrue(exceptionalResult.diagnostics.any { it.code == "usvm.precondition.threw" }) + } + + @Test + fun `supports relational predicates with multiple calls`() { + val manifest = manifest(predicateExport = "relationalProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertNotNull(result.inputs) + } + + @Test + fun `classifies unexpected exceptions and supported assertion failures`() { + val unexpected = search(manifest(predicateExport = "unexpectedException")) + val assertion = search(manifest(predicateExport = "assertionFailure")) + + assertEquals(UsvmPropertyViolationTarget.UNEXPECTED_EXCEPTION, unexpected.target) + assertEquals(UsvmPropertyViolationTarget.ASSERTION_FAILURE, assertion.target) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, unexpected.status) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, assertion.status) + } + + @Test + fun `preserves a reached target when symbolic input resolution fails`() { + val manifest = manifest( + predicateExport = "falseStringProperty", + domain = StringDomain(minLength = 0, maxLength = 3), + ) + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertNull(result.inputs) + assertTrue(result.diagnostics.any { it.code == "usvm.input.resolution.failed" }) + } + + @Test + fun `resolves candidates for common Kotlin domains`() { + val cases = listOf( + "falseBooleanProperty" to BooleanDomain, + "falseOptionalProperty" to OptionalDomain(IntegerDomain(min = -1, max = 1)), + "falseTupleProperty" to TupleDomain( + listOf(IntegerDomain(min = -1, max = 1), BooleanDomain), + ), + "falseNestedTupleProperty" to TupleDomain( + listOf(OptionalDomain(IntegerDomain(min = -1, max = 1)), BooleanDomain), + ), + "falseArrayProperty" to ArrayDomain( + element = IntegerDomain(min = -1, max = 1), + minLength = 1, + maxLength = 3, + ), + ) + + cases.forEach { (predicateExport, domain) -> + val result = search(manifest(predicateExport = predicateExport, domain = domain)) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, predicateExport) + assertTrue(assertNotNull(result.inputs).single() in domain, predicateExport) + } + } + + @Test + fun `reports async predicates as unsupported and non-boolean predicates as property errors`() { + val async = manifest( + predicateExport = "asyncValidProperty", + executionKind = ExecutionKind.ASYNC, + ) + val nonBoolean = manifest(predicateExport = "nonBooleanProperty") + + val asyncResult = search(async) + val nonBooleanResult = search(nonBoolean) + + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, asyncResult.status) + assertTrue(asyncResult.diagnostics.any { it.code == "usvm.predicate.async" }) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, nonBooleanResult.status) + assertTrue(nonBooleanResult.diagnostics.any { it.code == "usvm.predicate.result.non-boolean" }) + } + + @Test + fun `distinguishes timeout from exhausted search`() { + val manifest = manifest(predicateExport = "validProperty") + val zeroTimeoutSearcher = UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions(timeout = Duration.ZERO), + ) + + val result = zeroTimeoutSearcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + + assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) + } + + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + + private fun manifest( + predicateExport: String, + preconditionExport: String? = null, + executionKind: ExecutionKind = ExecutionKind.SYNC, + domain: PropertyDomain = IntegerDomain(min = -3, max = 3), + ) = PropertyManifest( + propertyId = "usvm.search.$predicateExport.${executionKind.name.lowercase()}", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmPropertySearchFixture.ts", + exportName = predicateExport, + executionKind = executionKind, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = "UsvmPropertySearchFixture.ts", + exportName = exportName, + ) + }, + ) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private lateinit var searcher: UsvmPropertySearcher + private lateinit var scene: EtsScene + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmPropertySearchFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt new file mode 100644 index 0000000000..2c9415833d --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt @@ -0,0 +1,245 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +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.JsNumber +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmScalarDomainProjectorTest { + @Test + fun `bounded integer accepts exactly integral non-negative-zero values inside inclusive bounds`() { + val domain = IntegerDomain(min = -2, max = 3) + + listOf(-2.0, 0.0, 3.0).forEach { value -> + assertTrue(acceptsNumber(domain, value), "Expected $value to be accepted") + } + listOf(-3.0, 4.0, 0.5, Double.NaN, Double.POSITIVE_INFINITY, -0.0).forEach { value -> + assertFalse(acceptsNumber(domain, value), "Expected $value to be rejected") + } + } + + @Test + fun `number bounds and NaN policy use shared JavaScript number semantics`() { + val bounded = NumberDomain( + min = JsNumber.finite(-1.5), + max = JsNumber.finite(2.5), + allowNaN = false, + ) + val unboundedWithNaN = NumberDomain(allowNaN = true) + + assertTrue(acceptsNumber(bounded, -1.5)) + assertTrue(acceptsNumber(bounded, 2.5)) + assertFalse(acceptsNumber(bounded, -1.6)) + assertFalse(acceptsNumber(bounded, 2.6)) + assertFalse(acceptsNumber(bounded, Double.NaN)) + assertTrue(acceptsNumber(unboundedWithNaN, Double.NaN)) + } + + @Test + fun `primitive constants admit only their declared JavaScript value`() { + val booleanDomain = ConstantDomain(JsConcreteValue.Boolean(value = true)) + val numberDomain = ConstantDomain(JsConcreteValue.number(7.25)) + + assertTrue(acceptsBoolean(booleanDomain, value = true)) + assertFalse(acceptsBoolean(booleanDomain, value = false)) + assertTrue(acceptsNumber(numberDomain, value = 7.25)) + assertFalse(acceptsNumber(numberDomain, value = 7.0)) + } + + @Test + fun `optional number admits its nested domain or exactly undefined`() { + val domain = OptionalDomain( + value = IntegerDomain(min = 1, max = 3), + nil = JsConcreteValue.Undefined, + ) + + assertTrue( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.fpTypeExpr, mkFpEqualExpr(value.extractFp(state.memory), mkFp(2.0, fp64Sort))) + } + }, + ) + assertTrue( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.refTypeExpr, mkHeapRefEq(value.extractRef(state.memory), mkUndefinedValue())) + } + }, + ) + assertFalse( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.fpTypeExpr, mkFpEqualExpr(value.extractFp(state.memory), mkFp(4.0, fp64Sort))) + } + }, + ) + assertFalse( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.refTypeExpr, mkHeapRefEq(value.extractRef(state.memory), mkTsNullValue())) + } + }, + ) + } + + @Test + fun `string projection constrains inclusive UTF-16 length bounds`() { + val domain = StringDomain(minLength = 1, maxLength = 3) + + assertTrue(acceptsStringLength(domain, length = 1)) + assertTrue(acceptsStringLength(domain, length = 3)) + assertFalse(acceptsStringLength(domain, length = 0)) + assertFalse(acceptsStringLength(domain, length = 4)) + } + + private fun acceptsNumber(domain: PropertyDomain, value: Double): Boolean = acceptsScalar( + domain = domain, + exportName = "acceptsNumber", + ) { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + + mkEq(input, mkFp(value, fp64Sort)) + } + } + + private fun acceptsBoolean(domain: PropertyDomain, value: Boolean): Boolean = acceptsScalar( + domain = domain, + exportName = "acceptsBoolean", + ) { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(boolSort, 1)).asExpr(boolSort) + + mkEq(input, mkBool(value)) + } + } + + private fun acceptsOptional( + domain: OptionalDomain, + constraint: (TsState, UsvmDeclaredDomainProjection) -> UBoolExpr, + ): Boolean { + val manifest = manifest(domain, exportName = "acceptsOptionalNumber") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + state.pathConstraints += constraint(state, projection) + } + } + + private fun acceptsStringLength(domain: StringDomain, length: Int): Boolean { + val manifest = manifest(domain, exportName = "acceptsString") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val value = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsStringType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(value, arrayType)) + + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + } + } + } + + private fun acceptsScalar( + domain: PropertyDomain, + exportName: String, + constraint: (TsState) -> UBoolExpr, + ): Boolean { + val manifest = manifest(domain, exportName) + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + projector.configure(state, manifest.inputs, target.bindings.inputs) + state.pathConstraints += constraint(state) + } + } + + private fun analyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ): Boolean = runCatching { + TsMachine( + scene = scene, + options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { _, state -> configure(state) }, + ) + } + }.isSuccess + + private fun manifest(domain: PropertyDomain, exportName: String) = PropertyManifest( + propertyId = "usvm.scalar.$exportName", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + ), + ) + + companion object { + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private val projector = UsvmDomainProjector() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + } + } +} 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 d87831de55..0104805361 100644 --- a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -94,6 +94,18 @@ export async function asyncNonBooleanWhenPositivePredicate(value: number): Promi return value > 0 ? 42 : false; } +export function literalFalsePredicate(_value: number): false { + return false; +} + +export function literalTruePredicate(_value: number): true { + return true; +} + +export function neverPredicate(_value: number): never { + throw 'never predicate exploded'; +} + export function catchesExpectedException(_value: number): boolean { try { throw 'expected'; diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts new file mode 100644 index 0000000000..75c59dd333 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts @@ -0,0 +1,31 @@ +export function acceptsBoolean(value: boolean): boolean { + return value; +} + +export function acceptsNumber(value: number): boolean { + return value > 0; +} + +export function acceptsString(value: string): boolean { + return value.length > 0; +} + +export function acceptsOptionalNumber(value: number | undefined): boolean { + return value === undefined || value > 0; +} + +export function acceptsTuple(value: [number, string]): boolean { + return value.length === 2; +} + +export function acceptsNumberBooleanTuple(value: [number, boolean]): boolean { + return value !== undefined; +} + +export function acceptsNumberArray(value: number[]): boolean { + return value.length > 0; +} + +export function returnsNumber(value: number): number { + return value; +} diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts new file mode 100644 index 0000000000..5d7e1aa6d7 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts @@ -0,0 +1,27 @@ +export function predicate(value: number): boolean { + return value !== 0; +} + +export function isPositive(value: number): boolean { + return value > 0; +} + +export function alwaysFalse(_value: number): boolean { + return false; +} + +export function acceptsNonPositiveOrThrows(value: number): boolean { + if (value > 0) { + throw new Error("positive"); + } + + return true; +} + +export async function asyncIsPositive(value: number): Promise { + return value > 0; +} + +export function returnsNumber(value: number): number { + return value; +} diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts new file mode 100644 index 0000000000..d19ce7f06a --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -0,0 +1,71 @@ +export function validProperty(value: number): boolean { + return value === value; +} + +export function violatedProperty(value: number): boolean { + return value !== 2; +} + +export function positive(value: number): boolean { + return value > 0; +} + +export function signedOneProperty(value: number): boolean { + return value !== 1 && value !== -1; +} + +export function falsePrecondition(_value: number): boolean { + return false; +} + +export function throwingPrecondition(_value: number): boolean { + throw "precondition"; +} + +function identity(value: number): number { + return value; +} + +export function relationalProperty(value: number): boolean { + return identity(value) === identity(value + 1); +} + +export function unexpectedException(_value: number): boolean { + throw "unexpected"; +} + +export function assertionFailure(_value: number): boolean { + throw "AssertionError: expected non-zero"; +} + +export function falseStringProperty(_value: string): boolean { + return false; +} + +export function falseBooleanProperty(_value: boolean): boolean { + return false; +} + +export function falseOptionalProperty(_value: number | undefined): boolean { + return false; +} + +export function falseTupleProperty(_value: [number, boolean]): boolean { + return false; +} + +export function falseNestedTupleProperty(_value: [number | undefined, boolean]): boolean { + return false; +} + +export function falseArrayProperty(_value: number[]): boolean { + return false; +} + +export function nonBooleanProperty(value: number): number { + return value; +} + +export async function asyncValidProperty(value: number): Promise { + return value === value; +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 3d6b394f33..f37bc411a9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -11,8 +11,10 @@ import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget import org.usvm.machine.call.TsNoUnknownCallModels import org.usvm.machine.call.TsProfileUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallModelProvider +import org.usvm.machine.call.TsUnknownCallOutcome import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -38,6 +40,14 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} +/** Terminal states together with structured stop metadata for one TypeScript analysis. */ +data class TsMachineAnalysisResult( + val states: List, + val timedOut: Boolean, + val unsupportedCall: Boolean, + val engineFailed: Boolean, +) + class TsMachine( private val scene: EtsScene, override val options: UMachineOptions, @@ -56,21 +66,41 @@ class TsMachine( modelProvider = unknownCallModelProvider, observer = observer, ) + private val failureTrackingUnknownCallDispatcher = FailureTrackingUnknownCallDispatcher( + delegate = resolvedUnknownCallDispatcher, + ) private val interpreter = TsInterpreter( ctx = ctx, graph = graph, options = tsOptions, observer = observer, - unknownCallDispatcher = resolvedUnknownCallDispatcher, + unknownCallDispatcher = failureTrackingUnknownCallDispatcher, ) private val cfgStatistics = CfgStatisticsImpl(graph) fun analyze( methods: List, targets: List = emptyList(), - ): List { + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): List = analyzeWithMetadata( + methods = methods, + targets = targets, + configureInitialState = configureInitialState, + ).states + + fun analyzeWithMetadata( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): TsMachineAnalysisResult { + interpreter.resetStepFailure() + failureTrackingUnknownCallDispatcher.reset() val initialStates = mutableMapOf() - methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + methods.forEach { method -> + initialStates[method] = interpreter.getInitialState(method, targets) { + configureInitialState(method, this) + } + } val methodsToTrackCoverage = when (options.coverageZone) { @@ -124,6 +154,7 @@ class TsMachine( val stepsStatistics = StepsStatistics() + var timedOut = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -135,7 +166,15 @@ class TsMachine( ) override fun shouldStop(): Boolean { + if (options.timeout <= kotlin.time.Duration.ZERO) { + timedOut = true + return true + } + val result = strategy.shouldStop() + if (result && timeStatistics.runningTime >= options.timeout) { + timedOut = true + } if (result) { logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } @@ -170,10 +209,35 @@ class TsMachine( stopStrategy = stopStrategy ) - return statesCollector.collectedStates + return TsMachineAnalysisResult( + states = statesCollector.collectedStates, + timedOut = timedOut, + unsupportedCall = failureTrackingUnknownCallDispatcher.pathStopped, + engineFailed = interpreter.stepFailed, + ) } override fun close() { components.close() } } + +private class FailureTrackingUnknownCallDispatcher( + private val delegate: TsUnknownCallDispatcher, +) : TsUnknownCallDispatcher { + var pathStopped: Boolean = false + private set + + override fun dispatch(scope: org.usvm.machine.interpreter.TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + val outcome = delegate.dispatch(scope, call) + if (outcome == TsUnknownCallOutcome.PATH_STOPPED) { + pathStopped = true + } + + return outcome + } + + fun reset() { + pathStopped = false + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt index e8f2ec65aa..524adf40c8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt @@ -61,3 +61,17 @@ class TsConcreteMethodCallStmt( return "concrete ${callee.signature.enclosingClass.name}::${callee.name}" } } + +/** Resumes the original entry point only when an auxiliary boolean guard returned true. */ +class TsEntryPointGuardResultStmt( + val entryPoint: EtsStmt, +) : EtsStmt { + override val location: EtsStmtLocation + get() = entryPoint.location + + override fun accept(visitor: EtsStmt.Visitor): R { + error("Auxiliary instruction") + } + + override fun toString(): String = "entry-point guard result" +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 0bf9f180b4..1ee6a18555 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -24,6 +24,7 @@ import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType @@ -45,6 +46,7 @@ import org.usvm.forkblacklists.UForkBlackList import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext +import org.usvm.machine.TsEntryPointGuardResultStmt import org.usvm.machine.TsGraph import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsOptions @@ -61,6 +63,7 @@ import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.expr.readGlobal import org.usvm.machine.expr.writeGlobal +import org.usvm.machine.state.TsEntryPointGuardOutcome import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt @@ -99,13 +102,19 @@ class TsInterpreter( ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() + internal var stepFailed: Boolean = false + private set + + internal fun resetStepFailure() { + stepFailed = false + } override fun step(state: TsState): StepResult { val stmt = state.lastStmt val scope = StepScope(state, forkBlackList) val result = state.methodResult - if (result is TsMethodResult.TsException) { + if (result is TsMethodResult.TsException && stmt !is TsEntryPointGuardResultStmt) { // TODO catch processing scope.doWithState { val returnSite = callStack.pop() @@ -132,6 +141,7 @@ class TsInterpreter( when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) + is TsEntryPointGuardResultStmt -> visitEntryPointGuardResult(scope, stmt) is EtsIfStmt -> visitIfStmt(scope, stmt) is EtsReturnStmt -> visitReturnStmt(scope, stmt) is EtsAssignStmt -> visitAssignStmt(scope, stmt) @@ -146,6 +156,7 @@ class TsInterpreter( } } } catch (e: Exception) { + stepFailed = true logger.error { "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { " $it" }}" } @@ -155,6 +166,45 @@ class TsInterpreter( return scope.stepResult() } + private fun visitEntryPointGuardResult( + scope: TsStepScope, + stmt: TsEntryPointGuardResultStmt, + ) = with(ctx) { + val result = scope.calcOnState { methodResult } + if (result !is TsMethodResult.Success) { + scope.doWithState { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.ERROR + callStack.pop() + } + return@with + } + val guard = result.value.takeIf { it.sort == boolSort }?.asExpr(boolSort) + if (guard == null) { + scope.doWithState { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.ERROR + callStack.pop() + } + return@with + } + + scope.fork( + condition = guard, + blockOnTrueState = { + methodResult = TsMethodResult.NoCall + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.NONE + newStmt(stmt.entryPoint) + }, + blockOnFalseState = { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.REJECTED + callStack.pop() + }, + ) + } + private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) = with(ctx) { val instance = stmt.instance @@ -708,7 +758,11 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + configureState: TsState.() -> Unit = {}, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -742,33 +796,40 @@ class TsInterpreter( } val parameterType = param.type - if (parameterType is EtsRefType) run { - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + if (parameterType is EtsRefType) { + run { + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) - if (parameterType is EtsArrayType) { - state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) + if (parameterType is EtsArrayType) { + state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) - val lengthLValue = mkArrayLengthLValue(ref, parameterType) - val length = state.memory.read(lengthLValue).asExpr(sizeSort) - state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + val lengthLValue = mkArrayLengthLValue(ref, parameterType) + val length = state.memory.read(lengthLValue).asExpr(sizeSort) + state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) - return@run - } + return@run + } - val resolvedParameterType = graph.hierarchy.classesForType(parameterType) + // Tuple inputs are materialized as fixed-size arrays by domain-aware initial-state configurators. + if (parameterType is EtsTupleType) { + return@run + } - if (resolvedParameterType.isEmpty()) { - logger.error("Cannot resolve class for parameter type: $parameterType") - return@run // TODO should be an error - } + val resolvedParameterType = graph.hierarchy.classesForType(parameterType) + + if (resolvedParameterType.isEmpty()) { + logger.error("Cannot resolve class for parameter type: $parameterType") + return@run // TODO should be an error + } - // Because of structural equality in TS we cannot determine the exact type - // Therefore, we create information about the fields the type must consist - val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) } - val auxiliaryType = EtsUnionType(types) // TODO error - state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) + // Because of structural equality in TS we cannot determine the exact type + // Therefore, we create information about the fields the type must consist + val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) } + val auxiliaryType = EtsUnionType(types) // TODO error + state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) + } } if (parameterType == EtsNullType) { state.pathConstraints += mkHeapRefEq(ref, mkTsNullValue()) @@ -798,6 +859,8 @@ class TsInterpreter( } } + state.configureState() + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 172da63294..c133b954be 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -36,6 +36,13 @@ import org.usvm.targets.UTargetsSet import org.usvm.util.mkFieldLValue import org.usvm.util.type +/** Observable completion of an auxiliary entry-point guard. */ +enum class TsEntryPointGuardOutcome { + NONE, + REJECTED, + ERROR, +} + /** * [lValuesToAllocatedFakeObjects] contains records of l-values that were allocated with newly created fake objects. * It is important for result interpreters to be able to restore the order of fake objects allocation and @@ -74,6 +81,12 @@ class TsState( */ var dfltObjectFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), + /** True while an auxiliary entry-point guard or one of its callees is executing. */ + var entryPointGuardActive: Boolean = false, + + /** Terminal guard outcome; [TsEntryPointGuardOutcome.NONE] also covers predicate execution. */ + var entryPointGuardOutcome: TsEntryPointGuardOutcome = TsEntryPointGuardOutcome.NONE, + /** * Maps string values to their corresponding heap references that were allocated for string constants. * This tracks which string constants have been initialized in this particular state to avoid @@ -293,6 +306,8 @@ class TsState( boundThis = boundThis, dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, + entryPointGuardActive = entryPointGuardActive, + entryPointGuardOutcome = entryPointGuardOutcome, stringConstantAllocatedRefs = stringConstantAllocatedRefs, ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index 09ac543689..c884ada0ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -4,6 +4,8 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt import org.usvm.UExpr import org.usvm.USort +import org.usvm.machine.TsEntryPointGuardResultStmt +import org.usvm.util.type val TsState.lastStmt: EtsStmt get() = currentStatement @@ -27,6 +29,27 @@ fun TsState.returnValue(valueToReturn: UExpr) { } } +/** Executes [guard] over [arguments] before resuming this state's original entry point. */ +fun TsState.prependBooleanEntryPointGuard( + guard: EtsMethod, + arguments: List>, +) { + require(!entryPointGuardActive) { "An entry-point guard is already active" } + require(arguments.size == guard.parameters.size) { + "Expected ${guard.parameters.size} guard arguments, got ${arguments.size}" + } + + val originalEntryPoint = currentStatement + val receiver = memory.allocConcrete(requireNotNull(guard.enclosingClass).type) + val actualArguments = listOf(receiver) + arguments + + pushSortsForActualArguments(actualArguments) + callStack.push(guard, TsEntryPointGuardResultStmt(originalEntryPoint)) + memory.stack.push(actualArguments.toTypedArray(), guard.localsCount) + entryPointGuardActive = true + newStmt(guard.cfg.instructions.first()) +} + inline val EtsMethod.parametersWithThisCount: Int get() = parameters.size + 1 From bc2e33a7a05465722bdff6cba7230d7a6a5643da Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 15:52:52 +0300 Subject: [PATCH 7/8] [TS PBT] Simplify USVM property execution flow --- .../usvm/ts/pbt/usvm/UsvmDomainProjector.kt | 33 ++--- .../usvm/ts/pbt/usvm/UsvmPropertyProjector.kt | 115 ++++++------------ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 101 +++++++-------- 3 files changed, 92 insertions(+), 157 deletions(-) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt index 3f70b7b6e5..4ba065068f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -39,9 +39,6 @@ import org.usvm.util.mkRegisterStackLValue /** One symbolic input written to the mapped EtsIR stack slot. */ data class UsvmProjectedInput( - val inputName: String, - val path: String, - val stackSlot: Int, val etsType: EtsType, val value: UExpr, ) @@ -65,7 +62,8 @@ class UsvmDomainProjector( "Property input count ${inputs.size} does not match EtsIR binding count ${bindings.size}" } - val preparedInputs = inputs.zip(bindings).mapIndexed { index, (input, binding) -> + val pairedInputs = inputs.zip(bindings) + pairedInputs.forEachIndexed { index, (input, binding) -> require(input.name == binding.propertyInputName) { "Property input ${input.name} does not match EtsIR binding ${binding.propertyInputName}" } @@ -77,27 +75,17 @@ class UsvmDomainProjector( path = path, options = options, ) - - PreparedInput(input, binding, path, capability) - } - preparedInputs.forEach { prepared -> - require(prepared.capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { - prepared.capability.diagnostics.joinToString { diagnostic -> diagnostic.message } + require(capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { + capability.diagnostics.joinToString { diagnostic -> diagnostic.message } } } - val projectedInputs = preparedInputs.map { prepared -> - val input = prepared.input - val binding = prepared.binding - val path = prepared.path - - val value = Materializer(state).materialize(input.domain, binding.parameter.type) + val materializer = Materializer(state) + val projectedInputs = pairedInputs.map { (input, binding) -> + val value = materializer.materialize(input.domain, binding.parameter.type) writeStackValue(state, binding.stackSlot, value) UsvmProjectedInput( - inputName = input.name, - path = path, - stackSlot = binding.stackSlot, etsType = binding.parameter.type, value = value, ) @@ -109,13 +97,6 @@ class UsvmDomainProjector( ) } - private data class PreparedInput( - val input: PropertyInput, - val binding: EtsInputBinding, - val path: String, - val capability: org.usvm.ts.pbt.backend.ProjectionCapability, - ) - private inner class Materializer(private val state: TsState) { fun materialize(domain: PropertyDomain, etsType: EtsType): UExpr = when (domain) { BooleanDomain -> state.makeSymbolicPrimitive(state.ctx.boolSort) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt index b8e9910946..1988e35667 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt @@ -73,12 +73,10 @@ class UsvmPropertyProjector( concreteCapability = concreteCapability, options = projectionOptions, ) - val capabilityDiagnostics = capability.symbolic.diagnostics if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { return result( capability = capability, status = UsvmPreconditionStatus.UNSUPPORTED, - diagnostics = capabilityDiagnostics, ) } @@ -86,21 +84,21 @@ class UsvmPropertyProjector( ?: return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "An exact precondition target was unavailable after capability validation", path = "precondition", ), ) - val execution = analyzePreconditionTarget(manifest, preconditionTarget) - return classifyPreconditionAnalysis(capability, execution) + return analyzePreconditionTarget(manifest, preconditionTarget, capability) } private fun analyzePreconditionTarget( manifest: PropertyManifest, preconditionTarget: EtsEntryPointTarget, - ): UsvmPreconditionExecution = TsMachine( + capability: UsvmPropertyProjectionCapability, + ): UsvmPreconditionResult = TsMachine( scene = scene, options = machineOptions, tsOptions = tsOptions, @@ -119,44 +117,45 @@ class UsvmPropertyProjector( ) }, ) - val canResolve = !analysis.timedOut && analysis.states.isNotEmpty() && analysis.states.all { state -> - val methodResult = state.methodResult as? TsMethodResult.Success - methodResult != null && methodResult.value.sort == state.ctx.boolSort - } - val resolutions = if (canResolve) { - analysis.states.map(::retainTruePreconditionState) - } else { - emptyList() - } - UsvmPreconditionExecution(analysis, resolutions) + classifyPreconditionAnalysis(capability, analysis) } private fun classifyPreconditionAnalysis( capability: UsvmPropertyProjectionCapability, - execution: UsvmPreconditionExecution, + analysis: TsMachineAnalysisResult, ): UsvmPreconditionResult { - val analysis = execution.analysis val failure = classifyPreconditionFailure(capability, analysis) if (failure != null) { return failure } - val capabilityDiagnostics = capability.symbolic.diagnostics - val resolutions = execution.resolutions - if (resolutions.any { it is PreconditionStateResolution.SolverUnknown }) { - return result( - capability = capability, - status = UsvmPreconditionStatus.SOLVER_UNKNOWN, - diagnostics = capabilityDiagnostics + diagnostic( - code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, - message = "The solver could not classify a precondition result", - path = "precondition.result", - ), - ) - } - val acceptedStates = resolutions.mapNotNull { resolution -> - (resolution as? PreconditionStateResolution.Accepted)?.state + val acceptedStates = mutableListOf() + for (state in analysis.states) { + val methodResult = state.methodResult as TsMethodResult.Success + val returnValue = with(state.ctx) { + methodResult.value.asExpr(boolSort) + } + val acceptedState = state.clone() + acceptedState.pathConstraints += returnValue + + when (val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints)) { + is USatResult -> { + acceptedState.models = listOf(solverResult.model) + acceptedStates += acceptedState + } + + is UUnsatResult -> Unit + is UUnknownResult -> return result( + capability = capability, + status = UsvmPreconditionStatus.SOLVER_UNKNOWN, + additionalDiagnostic = diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a precondition result", + path = "precondition.result", + ), + ) + } } val status = if (acceptedStates.isEmpty()) { UsvmPreconditionStatus.REJECTED @@ -168,7 +167,6 @@ class UsvmPropertyProjector( capability = capability, status = status, acceptedStates = acceptedStates, - diagnostics = capabilityDiagnostics, ) } @@ -176,13 +174,12 @@ class UsvmPropertyProjector( capability: UsvmPropertyProjectionCapability, analysis: TsMachineAnalysisResult, ): UsvmPreconditionResult? { - val capabilityDiagnostics = capability.symbolic.diagnostics val terminalStates = analysis.states if (terminalStates.any { state -> state.methodResult is TsMethodResult.TsException }) { return result( capability = capability, status = UsvmPreconditionStatus.PROPERTY_ERROR, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, message = "The precondition has a reachable escaping exception", path = "precondition", @@ -193,7 +190,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Precondition analysis terminated without a method result", path = "precondition", @@ -208,7 +205,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.PROPERTY_ERROR, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, message = "The precondition returned a non-boolean symbolic value", path = "precondition.result", @@ -219,7 +216,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.UNSUPPORTED, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, message = "The symbolic engine encountered an unsupported precondition call", path = "precondition", @@ -230,7 +227,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "The symbolic engine could not execute every reachable precondition path", path = "precondition", @@ -241,14 +238,13 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.TIMEOUT, - diagnostics = capabilityDiagnostics, ) } if (terminalStates.isEmpty()) { return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Precondition analysis produced no terminal states", path = "precondition", @@ -259,36 +255,16 @@ class UsvmPropertyProjector( return null } - private fun retainTruePreconditionState(state: TsState): PreconditionStateResolution { - val result = state.methodResult as TsMethodResult.Success - val returnValue = with(state.ctx) { - result.value.asExpr(boolSort) - } - val acceptedState = state.clone() - acceptedState.pathConstraints += returnValue - val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints) - - return when (solverResult) { - is USatResult -> { - acceptedState.models = listOf(solverResult.model) - PreconditionStateResolution.Accepted(acceptedState) - } - - is UUnsatResult -> PreconditionStateResolution.Rejected - is UUnknownResult -> PreconditionStateResolution.SolverUnknown - } - } - private fun result( capability: UsvmPropertyProjectionCapability, status: UsvmPreconditionStatus, - diagnostics: List, acceptedStates: List = emptyList(), + additionalDiagnostic: CapabilityDiagnostic? = null, ) = UsvmPreconditionResult( capability = capability, status = status, acceptedStates = acceptedStates, - diagnostics = diagnostics, + diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), ) private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( @@ -297,14 +273,3 @@ class UsvmPropertyProjector( path = path, ) } - -private data class UsvmPreconditionExecution( - val analysis: TsMachineAnalysisResult, - val resolutions: List, -) - -private sealed interface PreconditionStateResolution { - data class Accepted(val state: TsState) : PreconditionStateResolution - data object Rejected : PreconditionStateResolution - data object SolverUnknown : PreconditionStateResolution -} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 9522aedb42..9038f2d17f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -50,13 +50,11 @@ class UsvmPropertySearcher( concreteCapability = concreteCapability, options = projectionOptions, ) - val capabilityDiagnostics = capability.symbolic.diagnostics if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { return result( manifest = manifest, status = UsvmPropertySearchStatus.UNSUPPORTED, capability = capability, - diagnostics = capabilityDiagnostics, ) } @@ -65,36 +63,19 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "An exact predicate target was unavailable after capability validation", path = "predicate", ), ) val precondition = mapping.precondition?.exactTargetOrNull() - val execution = executeSearch(manifest, predicate, precondition) - val terminalFailure = classifyTerminalFailure( - manifest = manifest, - capability = capability, - analysis = execution.analysis, - ) - if (terminalFailure != null) { - return terminalFailure - } - - val violationState = execution.observer.violationStates.firstOrNull() - ?: return noViolationResult( - manifest = manifest, - capability = capability, - analysis = execution.analysis, - observer = execution.observer, - ) - return violationResult( + return executeSearch( manifest = manifest, + predicate = predicate, + precondition = precondition, capability = capability, - violationState = violationState, - projection = execution.projection, ) } @@ -102,17 +83,19 @@ class UsvmPropertySearcher( manifest: PropertyManifest, predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, - ): UsvmSearchExecution { + capability: UsvmPropertyProjectionCapability, + ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() val observer = UsvmViolationObserver(target) - val analysis = TsMachine( + + return TsMachine( scene = scene, options = machineOptions, tsOptions = tsOptions, machineObserver = observer, ).use { machine -> - machine.analyzeWithMetadata( + val analysis = machine.analyzeWithMetadata( methods = listOf(predicate.method), targets = listOf(target), configureInitialState = { method, state -> @@ -130,13 +113,30 @@ class UsvmPropertySearcher( } }, ) - } + val terminalFailure = classifyTerminalFailure( + manifest = manifest, + capability = capability, + analysis = analysis, + ) + if (terminalFailure != null) { + return@use terminalFailure + } - return UsvmSearchExecution( - analysis = analysis, - observer = observer, - projection = projection, - ) + val violationState = observer.violationStates.firstOrNull() + ?: return@use noViolationResult( + manifest = manifest, + capability = capability, + analysis = analysis, + observer = observer, + ) + + violationResult( + manifest = manifest, + capability = capability, + violationState = violationState, + projection = projection, + ) + } } private fun classifyTerminalFailure( @@ -149,7 +149,6 @@ class UsvmPropertySearcher( return preconditionFailure } - val capabilityDiagnostics = capability.symbolic.diagnostics val predicateContractError = analysis.states.any { state -> val methodResult = state.methodResult as? TsMethodResult.Success state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && @@ -161,7 +160,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.PROPERTY_ERROR, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PREDICATE_RESULT_NON_BOOLEAN, message = "The predicate returned a non-boolean symbolic value", path = "predicate.result", @@ -177,7 +176,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Predicate analysis terminated without a method result", path = "predicate", @@ -189,7 +188,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.UNSUPPORTED, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, message = "The symbolic engine encountered an unsupported property call", path = "predicate", @@ -201,7 +200,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "The symbolic engine could not execute every reachable property path", path = "predicate", @@ -217,7 +216,6 @@ class UsvmPropertySearcher( capability: UsvmPropertyProjectionCapability, analysis: TsMachineAnalysisResult, ): UsvmPropertySearchResult? { - val capabilityDiagnostics = capability.symbolic.diagnostics val preconditionError = analysis.states.firstOrNull { state -> state.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR } @@ -251,7 +249,7 @@ class UsvmPropertySearcher( manifest = manifest, status = status, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic, + additionalDiagnostic = diagnostic, ) } @@ -261,7 +259,6 @@ class UsvmPropertySearcher( analysis: TsMachineAnalysisResult, observer: UsvmViolationObserver, ): UsvmPropertySearchResult { - val capabilityDiagnostics = capability.symbolic.diagnostics val predicateCompleted = analysis.states.any { state -> state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && state.methodResult is TsMethodResult.Success @@ -276,27 +273,27 @@ class UsvmPropertySearcher( preconditionRejected -> UsvmPropertySearchStatus.PRECONDITION_REJECTED else -> UsvmPropertySearchStatus.ENGINE_FAILURE } - val diagnostics = when (status) { - UsvmPropertySearchStatus.SOLVER_UNKNOWN -> capabilityDiagnostics + diagnostic( + val additionalDiagnostic = when (status) { + UsvmPropertySearchStatus.SOLVER_UNKNOWN -> diagnostic( code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, message = "The solver could not classify a predicate result", path = "predicate.result", ) - UsvmPropertySearchStatus.ENGINE_FAILURE -> capabilityDiagnostics + diagnostic( + UsvmPropertySearchStatus.ENGINE_FAILURE -> diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Property search produced no classified terminal state", path = "predicate", ) - else -> capabilityDiagnostics + else -> null } return result( manifest = manifest, status = status, capability = capability, - diagnostics = diagnostics, + additionalDiagnostic = additionalDiagnostic, ) } @@ -306,7 +303,6 @@ class UsvmPropertySearcher( violationState: TsState, projection: UsvmDeclaredDomainProjection, ): UsvmPropertySearchResult { - val capabilityDiagnostics = capability.symbolic.diagnostics val violationTarget = classifyViolation(violationState) val inputs = runCatching { inputResolver.resolve(violationState, manifest.inputs, projection) @@ -322,7 +318,7 @@ class UsvmPropertySearcher( status = UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, target = violationTarget, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic, + additionalDiagnostic = diagnostic, ) } @@ -332,7 +328,6 @@ class UsvmPropertySearcher( target = violationTarget, inputs = inputs, capability = capability, - diagnostics = capabilityDiagnostics, ) } @@ -370,25 +365,19 @@ class UsvmPropertySearcher( manifest: PropertyManifest, status: UsvmPropertySearchStatus, capability: UsvmPropertyProjectionCapability, - diagnostics: List, target: UsvmPropertyViolationTarget? = null, inputs: List? = null, + additionalDiagnostic: CapabilityDiagnostic? = null, ) = UsvmPropertySearchResult( propertyId = PropertyId(manifest.propertyId), status = status, target = target, inputs = inputs, capability = capability, - diagnostics = diagnostics, + diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), ) } -private data class UsvmSearchExecution( - val analysis: TsMachineAnalysisResult, - val observer: UsvmViolationObserver, - val projection: UsvmDeclaredDomainProjection, -) - private class UsvmViolationTsTarget : TsTarget(location = null) private class UsvmViolationObserver( From 1beacb7c9bbbab8157f4dc09b12c295ae8bb17ff Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 17 Sep 2026 23:30:13 +0300 Subject: [PATCH 8/8] [TS PBT] Address symbolic search review findings --- usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md | 4 +- usvm-ts-pbt/README.md | 19 +- .../org/usvm/ts/pbt/PbtDiagnosticCode.kt | 2 + .../usvm/UsvmProjectionCapabilityResolver.kt | 56 +++- .../usvm/ts/pbt/usvm/UsvmPropertyProjector.kt | 275 ------------------ .../ts/pbt/usvm/UsvmPropertySearchModel.kt | 9 + .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 36 ++- .../usvm/PropertyExecutionConformanceTest.kt | 15 +- .../usvm/UsvmPreconditionProjectionTest.kt | 124 -------- .../ts/pbt/usvm/UsvmPreconditionSearchTest.kt | 98 +++++++ .../pbt/usvm/UsvmProjectionCapabilityTest.kt | 28 ++ .../ts/pbt/usvm/UsvmPropertySearcherTest.kt | 41 +++ .../resources/usvm/UsvmCapabilityFixture.ts | 24 ++ .../usvm/UsvmPropertySearchFixture.ts | 32 ++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 33 ++- 15 files changed, 334 insertions(+), 462 deletions(-) delete mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt delete mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md index 83aa9c856a..561bc8030f 100644 --- a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md +++ b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md @@ -85,8 +85,8 @@ 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. -- `UsvmPropertyProjector` and `UsvmPropertySearcher` apply this contract to the existing USVM projection and search - paths. `PropertyExecutionConformanceTest` runs the same TypeScript fixture through `FastCheckBackend` and USVM. +- `UsvmPropertySearcher` applies this contract to USVM domain projection and search in one execution path. + `PropertyExecutionConformanceTest` runs the same TypeScript fixture through `FastCheckBackend` and USVM. - `src/test/resources/properties/contract/PropertyExecutionContract.ts` is the shared observable fixture for concrete and symbolic contract regressions. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index fdd4bc0997..595b06e020 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -207,23 +207,22 @@ backend diagnostics are copied without reinterpretation. ## USVM projection and property search `UsvmProjectionCapabilityResolver` compares the declared domains with the exact EtsIR parameter bindings. -Booleans, bounded integers and numbers, supported primitive constants, optionals, bounded tuples, and bounded -arrays are projected by `UsvmDomainProjector`. Strings are an explicit over-approximation: USVM constrains their -type and UTF-16 length but not their contents. Nested arrays, incompatible EtsIR types, and collections above -`UsvmProjectionOptions.maxSymbolicCollectionLength` are unsupported with stable diagnostics. - -`UsvmPropertyProjector` executes a mapped synchronous precondition over projected inputs. It reports accepted and -rejected domains separately; a reachable exception or non-boolean result is `PROPERTY_ERROR`, solver uncertainty is -`SOLVER_UNKNOWN`, and async, non-exact, or unsupported residual-call execution is `UNSUPPORTED`. +Booleans, bounded integers and numbers, supported primitive constants, primitive optionals, bounded tuples, and +bounded arrays are projected by `UsvmDomainProjector`. Strings are an explicit over-approximation: USVM constrains +their type and UTF-16 length but not their contents. Optional reference domains, nested arrays, incompatible EtsIR +types, and collections above `UsvmProjectionOptions.maxSymbolicCollectionLength` are unsupported with stable +diagnostics. `UsvmPropertySearcher` evaluates the mapped precondition and predicate in one symbolic state. A false precondition is `PRECONDITION_REJECTED` when it excludes the complete projected domain. A precondition exception or non-boolean result is `PROPERTY_ERROR`. Predicate `false` and escaping predicate exceptions are `VIOLATION_REACHED`, while a non-boolean predicate is `PROPERTY_ERROR`. Timeout, solver uncertainty, unsupported execution, engine failure, and -input-resolution failure retain distinct statuses and are never treated as proof or as violations. +input-resolution failure retain distinct statuses and are never treated as proof. A reached target and any resolved +inputs remain attached when another explored path ends with unsupported execution or an engine failure. TypeScript +exception handlers are unsupported until the symbolic interpreter can preserve catch semantics. The shared fixture in `src/test/resources/properties/contract/PropertyExecutionContract.ts` is executed by both -`FastCheckBackend` and the USVM projection/search path. It covers precondition admission, rejection, exception and +`FastCheckBackend` and the single USVM search path. It covers precondition admission, rejection, exception and non-boolean results, plus false, throwing, literal-boolean-typed, never-typed, and non-boolean predicates. A shared mutation regression also verifies that a USVM candidate is reconstructed from the input before predicate mutation and reproduces through fast-check. Special values, alias preservation, mutation isolation, shrinking, and replay 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 index a31d8463a9..75bb755c80 100644 --- 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 @@ -63,9 +63,11 @@ internal object PbtDiagnosticCode { const val USVM_DOMAIN_ARRAY_NESTED_UNSUPPORTED = "usvm.domain.array.nested.unsupported" const val USVM_DOMAIN_COLLECTION_TOO_LARGE = "usvm.domain.collection.too-large" + const val USVM_DOMAIN_OPTIONAL_REFERENCE_UNSUPPORTED = "usvm.domain.optional-reference.unsupported" const val USVM_DOMAIN_STRING_APPROXIMATE = "usvm.domain.string.approximate" const val USVM_DOMAIN_TYPE_UNSUPPORTED = "usvm.domain.type.unsupported" const val USVM_ENGINE_FAILURE = "usvm.engine.failure" + const val USVM_EXCEPTION_HANDLER_UNSUPPORTED = "usvm.exception-handler.unsupported" const val USVM_EXECUTION_UNSUPPORTED = "usvm.execution.unsupported" const val USVM_INPUT_BINDING_UNAVAILABLE = "usvm.input.binding.unavailable" const val USVM_INPUT_RESOLUTION_FAILED = "usvm.input.resolution.failed" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt index 1e183a0d35..f1337fa67b 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt @@ -3,6 +3,7 @@ package org.usvm.ts.pbt.usvm import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType @@ -49,14 +50,15 @@ class UsvmProjectionCapabilityResolver { nonExactCode = PbtDiagnosticCode.USVM_PREDICATE_MAPPING_NON_EXACT, ) val predicateTarget = mapping.predicate.exactTargetOrNull() - val predicateExecutionCapability = if (manifest.predicate.executionKind == ExecutionKind.SYNC) { - exact() - } else { - unsupported( + val predicateExecutionCapability = when { + manifest.predicate.executionKind == ExecutionKind.ASYNC -> unsupported( code = PbtDiagnosticCode.USVM_PREDICATE_ASYNC, message = "Asynchronous TypeScript predicates are not supported by USVM search", path = "predicate", ) + + predicateTarget?.method?.hasExceptionHandler() == true -> unsupportedExceptionHandler("predicate") + else -> exact() } val inputCapabilities = manifest.inputs.mapIndexed { index, input -> val path = "inputs[$index].domain" @@ -136,6 +138,11 @@ class UsvmProjectionCapabilityResolver { ) val target = mappedPrecondition.exactTargetOrNull() ?: return mappingCapability + val exceptionHandlerCapability = if (target.method.hasExceptionHandler()) { + unsupportedExceptionHandler("precondition") + } else { + exact() + } val inputCapabilities = manifest.inputs.mapIndexed { index, input -> val parameterType = target.bindings.inputs .getOrNull(index) @@ -153,7 +160,9 @@ class UsvmProjectionCapabilityResolver { } } - return aggregateProjectionCapabilities(listOf(mappingCapability) + inputCapabilities) + return aggregateProjectionCapabilities( + listOf(mappingCapability, exceptionHandlerCapability) + inputCapabilities, + ) } private fun entryPointCapability( @@ -188,12 +197,20 @@ class UsvmProjectionCapabilityResolver { BooleanDomain, is IntegerDomain, is NumberDomain -> exact() is StringDomain -> approximateString(path) is ConstantDomain -> constantCapability(domain.value, path) - is OptionalDomain -> domainCapabilityForProjector( - domain = domain.value, - etsType = nestedOptionalType(domain, etsType), - path = "$path.value", - options = options, - ) + is OptionalDomain -> if (domain.value.isReferenceDomain()) { + unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_OPTIONAL_REFERENCE_UNSUPPORTED, + message = "Optional reference domains are not supported by the TypeScript heap model", + path = path, + ) + } else { + domainCapabilityForProjector( + domain = domain.value, + etsType = nestedOptionalType(domain, etsType), + path = "$path.value", + options = options, + ) + } is TupleDomain -> tupleCapability(domain, etsType, path, options) is ArrayDomain -> arrayCapability(domain, etsType, path, options) @@ -259,6 +276,12 @@ class UsvmProjectionCapabilityResolver { path = path, ) + private fun unsupportedExceptionHandler(path: String) = unsupported( + code = PbtDiagnosticCode.USVM_EXCEPTION_HANDLER_UNSUPPORTED, + message = "TypeScript exception handlers are not supported by symbolic execution", + path = path, + ) + internal fun domainCompatibilityForProjector(domain: PropertyDomain, etsType: EtsType): Boolean = when (domain) { BooleanDomain -> etsType == EtsBooleanType || etsType is EtsBooleanLiteralType is IntegerDomain, is NumberDomain -> etsType == EtsNumberType || etsType is EtsNumberLiteralType @@ -348,5 +371,16 @@ class UsvmProjectionCapabilityResolver { private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) } +private fun EtsMethod.hasExceptionHandler(): Boolean = cfg.stmts.any { statement -> + statement.location.origin?.nodeKind == "TryStatement" +} + +private fun PropertyDomain.isReferenceDomain(): Boolean = when (this) { + is StringDomain, is TupleDomain, is ArrayDomain -> true + is ConstantDomain -> value is JsConcreteValue.String || value is JsConcreteValue.Array + is OptionalDomain -> value.isReferenceDomain() + BooleanDomain, is IntegerDomain, is NumberDomain -> false +} + internal fun EtsMappingResult.exactTargetOrNull(): EtsEntryPointTarget? = targets.singleOrNull()?.takeIf { status == EtsMappingStatus.EXACT } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt deleted file mode 100644 index 1988e35667..0000000000 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt +++ /dev/null @@ -1,275 +0,0 @@ -package org.usvm.ts.pbt.usvm - -import io.ksmt.utils.asExpr -import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.model.EtsType -import org.usvm.StateCollectionStrategy -import org.usvm.UMachineOptions -import org.usvm.machine.TsMachine -import org.usvm.machine.TsMachineAnalysisResult -import org.usvm.machine.TsOptions -import org.usvm.machine.state.TsMethodResult -import org.usvm.machine.state.TsState -import org.usvm.solver.USatResult -import org.usvm.solver.UUnknownResult -import org.usvm.solver.UUnsatResult -import org.usvm.ts.pbt.PbtDiagnosticCode -import org.usvm.ts.pbt.backend.CapabilityDiagnostic -import org.usvm.ts.pbt.backend.ProjectionCapability -import org.usvm.ts.pbt.backend.ProjectionLevel -import org.usvm.ts.pbt.manifest.PropertyManifest -import org.usvm.ts.pbt.mapping.EtsEntryPointTarget -import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact - -/** Overall result of projecting and evaluating one declared precondition. */ -enum class UsvmPreconditionStatus { - ACCEPTED, - REJECTED, - PROPERTY_ERROR, - TIMEOUT, - SOLVER_UNKNOWN, - UNSUPPORTED, - ENGINE_FAILURE, -} - -/** Capability and terminal states satisfying a declared mapped precondition. */ -data class UsvmPreconditionResult( - val capability: UsvmPropertyProjectionCapability, - val status: UsvmPreconditionStatus, - val acceptedStates: List, - val diagnostics: List, -) { - init { - if (status == UsvmPreconditionStatus.ACCEPTED) { - require(acceptedStates.isNotEmpty()) { "An accepted precondition requires at least one state" } - } else { - require(acceptedStates.isEmpty()) { "Only an accepted precondition can expose states" } - } - } -} - -/** Orchestrates declared-domain materialization and mapped TypeScript precondition execution. */ -class UsvmPropertyProjector( - private val scene: EtsScene, - private val machineOptions: UMachineOptions = UMachineOptions( - stateCollectionStrategy = StateCollectionStrategy.ALL, - ), - private val tsOptions: TsOptions = TsOptions(), - private val projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), -) { - private val capabilityResolver = UsvmProjectionCapabilityResolver() - private val domainProjector = UsvmDomainProjector(projectionOptions) - - fun analyzePrecondition( - manifest: PropertyManifest, - mapping: PropertyEtsMappingArtifact, - concreteCapability: ProjectionCapability, - ): UsvmPreconditionResult { - requireNotNull(manifest.precondition) { "Precondition analysis requires a declared precondition" } - - val capability = capabilityResolver.resolve( - manifest = manifest, - mapping = mapping, - concreteCapability = concreteCapability, - options = projectionOptions, - ) - if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { - return result( - capability = capability, - status = UsvmPreconditionStatus.UNSUPPORTED, - ) - } - - val preconditionTarget = mapping.precondition?.exactTargetOrNull() - ?: return result( - capability = capability, - status = UsvmPreconditionStatus.ENGINE_FAILURE, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, - message = "An exact precondition target was unavailable after capability validation", - path = "precondition", - ), - ) - - return analyzePreconditionTarget(manifest, preconditionTarget, capability) - } - - private fun analyzePreconditionTarget( - manifest: PropertyManifest, - preconditionTarget: EtsEntryPointTarget, - capability: UsvmPropertyProjectionCapability, - ): UsvmPreconditionResult = TsMachine( - scene = scene, - options = machineOptions, - tsOptions = tsOptions, - ).use { machine -> - val analysis = machine.analyzeWithMetadata( - methods = listOf(preconditionTarget.method), - configureInitialState = { method, state -> - check(method == preconditionTarget.method) { - "Unexpected precondition initial state for ${method.signature}" - } - - domainProjector.configure( - state = state, - inputs = manifest.inputs, - bindings = preconditionTarget.bindings.inputs, - ) - }, - ) - - classifyPreconditionAnalysis(capability, analysis) - } - - private fun classifyPreconditionAnalysis( - capability: UsvmPropertyProjectionCapability, - analysis: TsMachineAnalysisResult, - ): UsvmPreconditionResult { - val failure = classifyPreconditionFailure(capability, analysis) - if (failure != null) { - return failure - } - - val acceptedStates = mutableListOf() - for (state in analysis.states) { - val methodResult = state.methodResult as TsMethodResult.Success - val returnValue = with(state.ctx) { - methodResult.value.asExpr(boolSort) - } - val acceptedState = state.clone() - acceptedState.pathConstraints += returnValue - - when (val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints)) { - is USatResult -> { - acceptedState.models = listOf(solverResult.model) - acceptedStates += acceptedState - } - - is UUnsatResult -> Unit - is UUnknownResult -> return result( - capability = capability, - status = UsvmPreconditionStatus.SOLVER_UNKNOWN, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, - message = "The solver could not classify a precondition result", - path = "precondition.result", - ), - ) - } - } - val status = if (acceptedStates.isEmpty()) { - UsvmPreconditionStatus.REJECTED - } else { - UsvmPreconditionStatus.ACCEPTED - } - - return result( - capability = capability, - status = status, - acceptedStates = acceptedStates, - ) - } - - private fun classifyPreconditionFailure( - capability: UsvmPropertyProjectionCapability, - analysis: TsMachineAnalysisResult, - ): UsvmPreconditionResult? { - val terminalStates = analysis.states - if (terminalStates.any { state -> state.methodResult is TsMethodResult.TsException }) { - return result( - capability = capability, - status = UsvmPreconditionStatus.PROPERTY_ERROR, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, - message = "The precondition has a reachable escaping exception", - path = "precondition", - ), - ) - } - if (terminalStates.any { state -> state.methodResult !is TsMethodResult.Success }) { - return result( - capability = capability, - status = UsvmPreconditionStatus.ENGINE_FAILURE, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, - message = "Precondition analysis terminated without a method result", - path = "precondition", - ), - ) - } - val nonBooleanResult = terminalStates.any { state -> - val methodResult = state.methodResult as TsMethodResult.Success - methodResult.value.sort != state.ctx.boolSort - } - if (nonBooleanResult) { - return result( - capability = capability, - status = UsvmPreconditionStatus.PROPERTY_ERROR, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, - message = "The precondition returned a non-boolean symbolic value", - path = "precondition.result", - ), - ) - } - if (analysis.unsupportedCall) { - return result( - capability = capability, - status = UsvmPreconditionStatus.UNSUPPORTED, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, - message = "The symbolic engine encountered an unsupported precondition call", - path = "precondition", - ), - ) - } - if (analysis.engineFailed) { - return result( - capability = capability, - status = UsvmPreconditionStatus.ENGINE_FAILURE, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, - message = "The symbolic engine could not execute every reachable precondition path", - path = "precondition", - ), - ) - } - if (analysis.timedOut) { - return result( - capability = capability, - status = UsvmPreconditionStatus.TIMEOUT, - ) - } - if (terminalStates.isEmpty()) { - return result( - capability = capability, - status = UsvmPreconditionStatus.ENGINE_FAILURE, - additionalDiagnostic = diagnostic( - code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, - message = "Precondition analysis produced no terminal states", - path = "precondition", - ), - ) - } - - return null - } - - private fun result( - capability: UsvmPropertyProjectionCapability, - status: UsvmPreconditionStatus, - acceptedStates: List = emptyList(), - additionalDiagnostic: CapabilityDiagnostic? = null, - ) = UsvmPreconditionResult( - capability = capability, - status = status, - acceptedStates = acceptedStates, - diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), - ) - - private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( - code = code, - message = message, - path = path, - ) -} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt index 8b3c531817..192f8ae6a5 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -45,6 +45,15 @@ data class UsvmPropertySearchResult( require(inputs == null) { "An input-resolution failure cannot contain candidate inputs" } } + UsvmPropertySearchStatus.PROPERTY_ERROR, + UsvmPropertySearchStatus.UNSUPPORTED, + UsvmPropertySearchStatus.ENGINE_FAILURE, + -> { + require(inputs == null || target != null) { + "Resolved candidate inputs require their reached target" + } + } + else -> { require(target == null) { "A result without a violation cannot contain a target" } require(inputs == null) { "A result without a violation cannot contain candidate inputs" } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 9038f2d17f..2a00cb839f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -113,29 +113,33 @@ class UsvmPropertySearcher( } }, ) + val violationState = observer.violationStates.firstOrNull { state -> + state.methodResult is TsMethodResult.Success + } ?: observer.violationStates.firstOrNull() + val candidate = violationState?.let { state -> + violationResult( + manifest = manifest, + capability = capability, + violationState = state, + projection = projection, + ) + } val terminalFailure = classifyTerminalFailure( manifest = manifest, capability = capability, analysis = analysis, ) if (terminalFailure != null) { - return@use terminalFailure + return@use terminalFailure.withCandidate(candidate) } - val violationState = observer.violationStates.firstOrNull() - ?: return@use noViolationResult( + candidate + ?: noViolationResult( manifest = manifest, capability = capability, analysis = analysis, observer = observer, ) - - violationResult( - manifest = manifest, - capability = capability, - violationState = violationState, - projection = projection, - ) } } @@ -378,6 +382,18 @@ class UsvmPropertySearcher( ) } +private fun UsvmPropertySearchResult.withCandidate( + candidate: UsvmPropertySearchResult?, +): UsvmPropertySearchResult { + if (candidate == null) return this + + return copy( + target = candidate.target, + inputs = candidate.inputs, + diagnostics = (diagnostics + candidate.diagnostics).distinct(), + ) +} + private class UsvmViolationTsTarget : TsTarget(location = null) private class UsvmViolationObserver( diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt index 8c4aa193a9..be529c822b 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt @@ -31,7 +31,7 @@ import kotlin.test.assertTrue class PropertyExecutionConformanceTest { @Test - fun `shared preconditions have the same concrete projection and search classification`() { + fun `shared preconditions have the same concrete and search classification`() { val cases = listOf( ContractCase("truePrecondition", ContractOutcome.HOLDS), ContractCase("falsePrecondition", ContractOutcome.PRECONDITION_REJECTED), @@ -62,15 +62,11 @@ class PropertyExecutionConformanceTest { val mapping = mapper.map(manifest) val concreteOutcome = concreteOutcome(property, case.expectedBackendError) - val projectionOutcome = projectionOutcome( - projector.analyzePrecondition(manifest, mapping, exactCapability), - ) val searchOutcome = searchOutcome( searcher.search(manifest, mapping, exactCapability), ) assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") - assertEquals(case.expected, projectionOutcome, "${case.exportName}: projection") assertEquals(case.expected, searchOutcome, "${case.exportName}: search") } } @@ -173,13 +169,6 @@ class PropertyExecutionConformanceTest { ContractOutcome.PROPERTY_ERROR } - private fun projectionOutcome(result: UsvmPreconditionResult): ContractOutcome = when (result.status) { - UsvmPreconditionStatus.ACCEPTED -> ContractOutcome.HOLDS - UsvmPreconditionStatus.REJECTED -> ContractOutcome.PRECONDITION_REJECTED - UsvmPreconditionStatus.PROPERTY_ERROR -> ContractOutcome.PROPERTY_ERROR - else -> error("Unexpected projection result: $result") - } - private fun searchOutcome(result: UsvmPropertySearchResult): ContractOutcome = when (result.status) { UsvmPropertySearchStatus.VIOLATION_REACHED -> ContractOutcome.PREDICATE_VIOLATION UsvmPropertySearchStatus.NO_VIOLATION_REACHED -> ContractOutcome.HOLDS @@ -242,7 +231,6 @@ class PropertyExecutionConformanceTest { private val fixtureDirectory = testResourcesRoot().resolve("properties/contract") private val backend = FastCheckBackend(sourceRoots = listOf(fixtureDirectory)) private lateinit var mapper: PropertyEtsMapper - private lateinit var projector: UsvmPropertyProjector private lateinit var searcher: UsvmPropertySearcher @JvmStatic @@ -256,7 +244,6 @@ class PropertyExecutionConformanceTest { scene = scene, sourceRoots = listOf(fixtureDirectory), ) - projector = UsvmPropertyProjector(scene) searcher = UsvmPropertySearcher(scene) } } diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt deleted file mode 100644 index ab0348c037..0000000000 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt +++ /dev/null @@ -1,124 +0,0 @@ -package org.usvm.ts.pbt.usvm - -import io.ksmt.utils.asExpr -import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.EtsIrProvider -import org.jacodb.ets.utils.loadEtsFileAutoConvert -import org.junit.jupiter.api.BeforeAll -import org.junit.jupiter.api.Test -import org.usvm.isTrue -import org.usvm.machine.state.TsMethodResult -import org.usvm.ts.pbt.backend.ProjectionCapability -import org.usvm.ts.pbt.backend.ProjectionLevel -import org.usvm.ts.pbt.manifest.PropertyManifest -import org.usvm.ts.pbt.mapping.PropertyEtsMapper -import org.usvm.ts.pbt.model.ExecutionKind -import org.usvm.ts.pbt.model.IntegerDomain -import org.usvm.ts.pbt.model.PropertyInput -import org.usvm.ts.pbt.model.TypeScriptEntryPoint -import org.usvm.ts.pbt.testResourcePath -import org.usvm.util.mkRegisterStackLValue -import kotlin.test.assertEquals -import kotlin.test.assertTrue - -class UsvmPreconditionProjectionTest { - @Test - fun `mapped precondition retains only satisfiable true states inside the declared domain`() { - val manifest = manifest(preconditionExport = "isPositive") - val mapping = mapper.map(manifest) - - val result = projector.analyzePrecondition(manifest, mapping, exact()) - - assertEquals(ProjectionLevel.EXACT, result.capability.symbolic.level) - assertEquals(UsvmPreconditionStatus.ACCEPTED, result.status) - assertTrue(result.acceptedStates.isNotEmpty()) - result.acceptedStates.forEach { state -> - assertTrue(state.methodResult is TsMethodResult.Success) - with(state.ctx) { - val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) - val value = state.models.single().eval(input) - - assertTrue(mkFpGreaterExpr(value, mkFp(0.0, fp64Sort)).isTrue) - assertTrue(mkFpLessOrEqualExpr(value, mkFp(3.0, fp64Sort)).isTrue) - } - } - } - - @Test - fun `false-only states are rejected and unsupported exception construction is explicit`() { - val falseManifest = manifest(preconditionExport = "alwaysFalse") - val throwingManifest = manifest(preconditionExport = "acceptsNonPositiveOrThrows") - - val falseResult = projector.analyzePrecondition(falseManifest, mapper.map(falseManifest), exact()) - val throwingResult = projector.analyzePrecondition(throwingManifest, mapper.map(throwingManifest), exact()) - - assertEquals(emptyList(), falseResult.acceptedStates) - assertEquals(UsvmPreconditionStatus.REJECTED, falseResult.status) - assertEquals(emptyList(), throwingResult.acceptedStates) - assertEquals(UsvmPreconditionStatus.UNSUPPORTED, throwingResult.status) - assertTrue(throwingResult.diagnostics.any { it.code == "usvm.execution.unsupported" }) - } - - @Test - fun `async preconditions are unsupported and non-boolean preconditions are property errors`() { - val asyncManifest = manifest( - preconditionExport = "asyncIsPositive", - executionKind = ExecutionKind.ASYNC, - ) - val nonBooleanManifest = manifest(preconditionExport = "returnsNumber") - - val asyncResult = projector.analyzePrecondition(asyncManifest, mapper.map(asyncManifest), exact()) - val nonBooleanResult = projector.analyzePrecondition( - nonBooleanManifest, - mapper.map(nonBooleanManifest), - exact(), - ) - - assertEquals(ProjectionLevel.UNSUPPORTED, asyncResult.capability.precondition.level) - assertEquals(UsvmPreconditionStatus.UNSUPPORTED, asyncResult.status) - assertEquals(emptyList(), asyncResult.acceptedStates) - assertEquals(ProjectionLevel.EXACT, nonBooleanResult.capability.precondition.level) - assertEquals(UsvmPreconditionStatus.PROPERTY_ERROR, nonBooleanResult.status) - assertEquals(emptyList(), nonBooleanResult.acceptedStates) - assertTrue(nonBooleanResult.diagnostics.any { it.code == "usvm.precondition.result.non-boolean" }) - } - - private fun manifest( - preconditionExport: String, - executionKind: ExecutionKind = ExecutionKind.SYNC, - ) = PropertyManifest( - propertyId = "usvm.precondition.$preconditionExport.${executionKind.name.lowercase()}", - inputs = listOf( - PropertyInput( - name = "value", - domain = IntegerDomain(min = -2, max = 3), - ), - ), - predicate = TypeScriptEntryPoint( - module = "UsvmPreconditionFixture.ts", - exportName = "predicate", - ), - precondition = TypeScriptEntryPoint( - module = "UsvmPreconditionFixture.ts", - exportName = preconditionExport, - executionKind = executionKind, - ), - ) - - private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) - - companion object { - private lateinit var mapper: PropertyEtsMapper - private lateinit var projector: UsvmPropertyProjector - - @JvmStatic - @BeforeAll - fun loadFixture() { - val source = testResourcePath("/usvm/UsvmPreconditionFixture.ts") - val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) - val scene = EtsScene(listOf(file)) - mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) - projector = UsvmPropertyProjector(scene) - } - } -} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt new file mode 100644 index 0000000000..045fa83315 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt @@ -0,0 +1,98 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class UsvmPreconditionSearchTest { + @Test + fun `mapped precondition restricts the declared domain before predicate search`() { + val result = search(manifest(preconditionExport = "isPositive")) + + assertEquals(ProjectionLevel.EXACT, result.capability.symbolic.level) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + + @Test + fun `false precondition is rejected and unsupported calls remain explicit`() { + val rejected = search(manifest(preconditionExport = "alwaysFalse")) + val unsupported = search(manifest(preconditionExport = "acceptsNonPositiveOrThrows")) + + assertEquals(UsvmPropertySearchStatus.PRECONDITION_REJECTED, rejected.status) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, unsupported.status) + assertTrue(unsupported.diagnostics.any { it.code == "usvm.execution.unsupported" }) + } + + @Test + fun `async and non-boolean preconditions retain distinct classifications`() { + val async = search( + manifest( + preconditionExport = "asyncIsPositive", + executionKind = ExecutionKind.ASYNC, + ), + ) + val nonBoolean = search(manifest(preconditionExport = "returnsNumber")) + + assertEquals(ProjectionLevel.UNSUPPORTED, async.capability.precondition.level) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, async.status) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, nonBoolean.status) + assertTrue(nonBoolean.diagnostics.any { it.code == "usvm.precondition.result.non-boolean" }) + } + + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + + private fun manifest( + preconditionExport: String, + executionKind: ExecutionKind = ExecutionKind.SYNC, + ) = PropertyManifest( + propertyId = "usvm.precondition.$preconditionExport.${executionKind.name.lowercase()}", + inputs = listOf( + PropertyInput( + name = "value", + domain = IntegerDomain(min = -2, max = 3), + ), + ), + predicate = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = "predicate", + ), + precondition = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = preconditionExport, + executionKind = executionKind, + ), + ) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private lateinit var searcher: UsvmPropertySearcher + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmPreconditionFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt index 5ba1249988..37332d3c06 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt @@ -80,6 +80,34 @@ class UsvmProjectionCapabilityTest { assertEquals(listOf("inputs[0].domain"), oversizedArray.symbolic.diagnostics.map { it.path }) } + @Test + fun `optional references and exception handlers are unsupported`() { + val optionalArray = resolve( + domain = OptionalDomain(ArrayDomain(IntegerDomain(), minLength = 1, maxLength = 1)), + exportName = "acceptsOptionalNumberArray", + ) + val caughtDirect = resolve(IntegerDomain(), "catchesDirectThrow") + val caughtHelper = resolve(IntegerDomain(), "catchesHelperThrow") + val preconditionManifest = manifest( + domain = IntegerDomain(), + predicateExport = "acceptsNumber", + preconditionExport = "catchesDirectThrow", + ) + val caughtPrecondition = resolver.resolve( + manifest = preconditionManifest, + mapping = mapper.map(preconditionManifest), + concreteCapability = exact(), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, optionalArray.symbolic.level) + assertEquals("usvm.domain.optional-reference.unsupported", optionalArray.symbolic.diagnostics.single().code) + assertEquals(ProjectionLevel.UNSUPPORTED, caughtDirect.symbolic.level) + assertEquals("usvm.exception-handler.unsupported", caughtDirect.symbolic.diagnostics.single().code) + assertEquals(ProjectionLevel.UNSUPPORTED, caughtHelper.symbolic.level) + assertEquals(ProjectionLevel.UNSUPPORTED, caughtPrecondition.precondition.level) + assertEquals("usvm.exception-handler.unsupported", caughtPrecondition.precondition.diagnostics.single().code) + } + @Test fun `reports unsupported mapping and execution boundaries without classifying property errors`() { val manifest = manifest(IntegerDomain(), predicateExport = "acceptsNumber") diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt index 676e70b781..9ab687d465 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -12,6 +12,7 @@ import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain +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 @@ -125,6 +126,46 @@ class UsvmPropertySearcherTest { assertTrue(result.diagnostics.any { it.code == "usvm.input.resolution.failed" }) } + @Test + fun `preserves a reached violation when another path is unsupported`() { + val result = search( + manifest( + predicateExport = "mixedUnsupportedProperty", + domain = IntegerDomain(min = 0, max = 1), + ), + ) + + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertEquals(listOf(JsConcreteValue.number(0.0)), result.inputs) + assertTrue(result.diagnostics.any { it.code == "usvm.execution.unsupported" }) + } + + @Test + fun `reports exception handlers and optional collections as unsupported`() { + val caughtDirect = search(manifest(predicateExport = "caughtDirectProperty")) + val caughtHelper = search(manifest(predicateExport = "caughtHelperProperty")) + val optionalArray = search( + manifest( + predicateExport = "optionalArrayProperty", + domain = OptionalDomain( + ArrayDomain( + element = ConstantDomain(JsConcreteValue.number(2.0)), + minLength = 1, + maxLength = 1, + ), + ), + ), + ) + + listOf(caughtDirect, caughtHelper).forEach { result -> + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, result.status) + assertTrue(result.diagnostics.any { it.code == "usvm.exception-handler.unsupported" }) + } + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, optionalArray.status) + assertTrue(optionalArray.diagnostics.any { it.code == "usvm.domain.optional-reference.unsupported" }) + } + @Test fun `resolves candidates for common Kotlin domains`() { val cases = listOf( diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts index 75c59dd333..b252f65a86 100644 --- a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts @@ -26,6 +26,30 @@ export function acceptsNumberArray(value: number[]): boolean { return value.length > 0; } +export function acceptsOptionalNumberArray(value: number[] | undefined): boolean { + return value === undefined || value.length > 0; +} + +export function catchesDirectThrow(_value: number): boolean { + try { + throw "expected"; + } catch { + return true; + } +} + +export function catchesHelperThrow(value: number): boolean { + try { + return throwingHelper(value); + } catch { + return true; + } +} + +function throwingHelper(_value: number): boolean { + throw "expected"; +} + export function returnsNumber(value: number): number { return value; } diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts index d19ce7f06a..b29d48000c 100644 --- a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -62,6 +62,38 @@ export function falseArrayProperty(_value: number[]): boolean { return false; } +export function mixedUnsupportedProperty(value: number): boolean { + if (value === 0) { + return false; + } + + return Math.sin(value) > 0; +} + +export function caughtDirectProperty(_value: number): boolean { + try { + throw "expected"; + } catch { + return true; + } +} + +export function caughtHelperProperty(value: number): boolean { + try { + return throwingHelper(value); + } catch { + return true; + } +} + +function throwingHelper(_value: number): boolean { + throw "expected"; +} + +export function optionalArrayProperty(value: number[] | undefined): boolean { + return value === undefined || value[0] === 2; +} + export function nonBooleanProperty(value: number): number { return value; } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index f37bc411a9..3d685ec766 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -11,10 +11,11 @@ import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget import org.usvm.machine.call.TsNoUnknownCallModels import org.usvm.machine.call.TsProfileUnknownCallDispatcher -import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelProvider -import org.usvm.machine.call.TsUnknownCallOutcome import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -61,20 +62,18 @@ class TsMachine( private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) + private val failureTrackingUnknownCallObserver = FailureTrackingUnknownCallObserver(observer) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( profile = tsOptions.unknownCallProfile, modelProvider = unknownCallModelProvider, - observer = observer, - ) - private val failureTrackingUnknownCallDispatcher = FailureTrackingUnknownCallDispatcher( - delegate = resolvedUnknownCallDispatcher, + observer = failureTrackingUnknownCallObserver, ) private val interpreter = TsInterpreter( ctx = ctx, graph = graph, options = tsOptions, observer = observer, - unknownCallDispatcher = failureTrackingUnknownCallDispatcher, + unknownCallDispatcher = resolvedUnknownCallDispatcher, ) private val cfgStatistics = CfgStatisticsImpl(graph) @@ -94,7 +93,7 @@ class TsMachine( configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, ): TsMachineAnalysisResult { interpreter.resetStepFailure() - failureTrackingUnknownCallDispatcher.reset() + failureTrackingUnknownCallObserver.reset() val initialStates = mutableMapOf() methods.forEach { method -> initialStates[method] = interpreter.getInitialState(method, targets) { @@ -212,7 +211,7 @@ class TsMachine( return TsMachineAnalysisResult( states = statesCollector.collectedStates, timedOut = timedOut, - unsupportedCall = failureTrackingUnknownCallDispatcher.pathStopped, + unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, engineFailed = interpreter.stepFailed, ) } @@ -222,19 +221,21 @@ class TsMachine( } } -private class FailureTrackingUnknownCallDispatcher( - private val delegate: TsUnknownCallDispatcher, -) : TsUnknownCallDispatcher { +private class FailureTrackingUnknownCallObserver( + private val delegate: TsInterpreterObserver?, +) : TsInterpreterObserver { var pathStopped: Boolean = false private set - override fun dispatch(scope: org.usvm.machine.interpreter.TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - val outcome = delegate.dispatch(scope, call) - if (outcome == TsUnknownCallOutcome.PATH_STOPPED) { + override fun onUnknownCall(event: TsUnknownCallEvent) { + val decision = event.decision + val stopsPath = decision is TsUnknownCallDecision.ResidualFallback && + decision.policy == TsResidualCallPolicy.STOP_PATH + if (stopsPath) { pathStopped = true } - return outcome + delegate?.onUnknownCall(event) } fun reset() {