diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md index 0e40b60571..f4c18201ee 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 @@ -243,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 @@ -281,6 +298,10 @@ 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. 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, @@ -293,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 new file mode 100644 index 0000000000..561bc8030f --- /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. +- `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. + +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..595b06e020 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 @@ -200,6 +204,30 @@ 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, 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. 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 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 +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/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..7b952dfdd3 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; } @@ -80,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 { @@ -101,22 +104,108 @@ 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 => { - if (precondition !== undefined && !(await precondition.invoke(cloneArguments(values)))) fc.pre(false); + 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 && !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(cloneArguments(values)); - }); + throw error; } +} - return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => { - if (precondition !== undefined && !precondition.invoke(cloneArguments(values))) fc.pre(false); +async function preserveAsyncContractError( + state: ContractErrorState, + invocation: () => Promise, +): Promise { + if (state.first !== undefined) throw state.first; - return predicate.invoke(cloneArguments(values)) as boolean; - }); + try { + return await invocation(); + } catch (error: unknown) { + if (error instanceof ProtocolError) state.first ??= error; + + throw error; + } +} + +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 { + try { + if (value instanceof Error) { + const name = String(value.name || 'Error'); + + return value.message.length === 0 ? name : `${name}: ${value.message}`; + } + + return `a non-Error value: ${String(value)}`; + } catch { + return 'an unprintable value'; + } } async function checkProperty( @@ -139,28 +228,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[]]> { @@ -181,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, @@ -219,29 +288,27 @@ 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', }; } 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', }; } @@ -253,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 { @@ -447,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/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..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 @@ -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,228 @@ 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 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)); + + 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 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: [ + 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'); @@ -114,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); }); }); @@ -142,7 +366,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 +390,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 +413,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 +435,7 @@ interface RequestOverrides { predicateExecutionKind?: 'sync' | 'async'; precondition?: FastCheckExecutionRequest['manifest']['precondition']; inputDomain?: unknown; + inputDomains?: unknown[]; } function executionRequest( @@ -238,12 +443,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 +468,41 @@ function executionRequest( }; } +interface ContractRequestOverrides { + preconditionExport?: string; + preconditionExecutionKind?: 'sync' | 'async'; + predicateExecutionKind?: 'sync' | 'async'; + inputDomains?: unknown[]; +} + +function contractExecutionRequest( + predicateExport: string, + overrides: ContractRequestOverrides = {}, +): 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; + + if (overrides.preconditionExport !== undefined) { + request.manifest.precondition = { + module: CONTRACT_MODULE, + exportName: overrides.preconditionExport, + executionKind: overrides.preconditionExecutionKind ?? '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 +556,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/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt index 65dbf5170d..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 @@ -61,6 +61,28 @@ 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_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" + 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/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/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..4ba065068f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -0,0 +1,374 @@ +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 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 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}" + } + + val path = "inputs[$index].domain" + val capability = UsvmProjectionCapabilityResolver().domainCapabilityForProjector( + domain = input.domain, + etsType = binding.parameter.type, + path = path, + options = options, + ) + require(capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { + capability.diagnostics.joinToString { diagnostic -> diagnostic.message } + } + } + + 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( + etsType = binding.parameter.type, + value = value, + ) + } + + return UsvmDeclaredDomainProjection( + inputs = projectedInputs, + initialState = state.clone(), + ) + } + + 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..f1337fa67b --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt @@ -0,0 +1,386 @@ +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 +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 = 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" + 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 exceptionHandlerCapability = if (target.method.hasExceptionHandler()) { + unsupportedExceptionHandler("precondition") + } else { + exact() + } + 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, exceptionHandlerCapability) + 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 -> 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) + } + } + + 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, + ) + + 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 + 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) +} + +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/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/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt new file mode 100644 index 0000000000..192f8ae6a5 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -0,0 +1,63 @@ +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" } + } + + 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 new file mode 100644 index 0000000000..2a00cb839f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -0,0 +1,446 @@ +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, + ) + if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.UNSUPPORTED, + capability = capability, + ) + } + + val predicate = mapping.predicate.exactTargetOrNull() + ?: return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + additionalDiagnostic = diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "An exact predicate target was unavailable after capability validation", + path = "predicate", + ), + ) + val precondition = mapping.precondition?.exactTargetOrNull() + + return executeSearch( + manifest = manifest, + predicate = predicate, + precondition = precondition, + capability = capability, + ) + } + + private fun executeSearch( + manifest: PropertyManifest, + predicate: EtsEntryPointTarget, + precondition: EtsEntryPointTarget?, + capability: UsvmPropertyProjectionCapability, + ): UsvmPropertySearchResult { + lateinit var projection: UsvmDeclaredDomainProjection + val target = UsvmViolationTsTarget() + val observer = UsvmViolationObserver(target) + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = observer, + ).use { machine -> + val analysis = 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), + ) + } + }, + ) + 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.withCandidate(candidate) + } + + candidate + ?: noViolationResult( + manifest = manifest, + capability = capability, + analysis = analysis, + observer = observer, + ) + } + } + + private fun classifyTerminalFailure( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPropertySearchResult? { + val preconditionFailure = classifyPreconditionFailure(manifest, capability, analysis) + if (preconditionFailure != null) { + return preconditionFailure + } + + 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, + additionalDiagnostic = 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, + additionalDiagnostic = 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, + additionalDiagnostic = 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, + additionalDiagnostic = 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 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, + additionalDiagnostic = diagnostic, + ) + } + + private fun noViolationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + observer: UsvmViolationObserver, + ): UsvmPropertySearchResult { + 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 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 -> diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Property search produced no classified terminal state", + path = "predicate", + ) + + else -> null + } + + return result( + manifest = manifest, + status = status, + capability = capability, + additionalDiagnostic = additionalDiagnostic, + ) + } + + private fun violationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + violationState: TsState, + projection: UsvmDeclaredDomainProjection, + ): UsvmPropertySearchResult { + 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, + additionalDiagnostic = diagnostic, + ) + } + + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.VIOLATION_REACHED, + target = violationTarget, + inputs = inputs, + capability = capability, + ) + } + + 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, + target: UsvmPropertyViolationTarget? = null, + inputs: List? = null, + additionalDiagnostic: CapabilityDiagnostic? = null, + ) = UsvmPropertySearchResult( + propertyId = PropertyId(manifest.propertyId), + status = status, + target = target, + inputs = inputs, + capability = capability, + diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), + ) +} + +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( + 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/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/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 -> 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..dc4fcc5eb2 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/PropertyExecutionContractTest.kt @@ -0,0 +1,279 @@ +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.ExecutionKind +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 = "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", + 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 `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( + 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/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..be529c822b --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt @@ -0,0 +1,250 @@ +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 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 searchOutcome = searchOutcome( + searcher.search(manifest, mapping, exactCapability), + ) + + assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") + 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 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 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), + ) + 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/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 new file mode 100644 index 0000000000..37332d3c06 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt @@ -0,0 +1,236 @@ +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 `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") + 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..9ab687d465 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -0,0 +1,272 @@ +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.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.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 `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( + "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 new file mode 100644 index 0000000000..0104805361 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -0,0 +1,148 @@ +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 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; +} + +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; +} + +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'; +} + +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 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'; + } 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; +} 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..b252f65a86 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts @@ -0,0 +1,55 @@ +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 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/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..b29d48000c --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -0,0 +1,103 @@ +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 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; +} + +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..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,7 +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.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.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult @@ -38,6 +41,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, @@ -51,10 +62,11 @@ 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, + observer = failureTrackingUnknownCallObserver, ) private val interpreter = TsInterpreter( ctx = ctx, @@ -68,9 +80,26 @@ class TsMachine( 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() + failureTrackingUnknownCallObserver.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 +153,7 @@ class TsMachine( val stepsStatistics = StepsStatistics() + var timedOut = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -135,7 +165,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 +208,37 @@ class TsMachine( stopStrategy = stopStrategy ) - return statesCollector.collectedStates + return TsMachineAnalysisResult( + states = statesCollector.collectedStates, + timedOut = timedOut, + unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, + engineFailed = interpreter.stepFailed, + ) } override fun close() { components.close() } } + +private class FailureTrackingUnknownCallObserver( + private val delegate: TsInterpreterObserver?, +) : TsInterpreterObserver { + var pathStopped: Boolean = false + private set + + override fun onUnknownCall(event: TsUnknownCallEvent) { + val decision = event.decision + val stopsPath = decision is TsUnknownCallDecision.ResidualFallback && + decision.policy == TsResidualCallPolicy.STOP_PATH + if (stopsPath) { + pathStopped = true + } + + delegate?.onUnknownCall(event) + } + + 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