diff --git a/usvm-ts-fast-check/DESIGN.md b/usvm-ts-fast-check/DESIGN.md index 7acd3fe165..78956d7ecf 100644 --- a/usvm-ts-fast-check/DESIGN.md +++ b/usvm-ts-fast-check/DESIGN.md @@ -79,6 +79,29 @@ JSON again because the process boundary must not trust malformed input. Diagnost language: `FastCheckDiagnosticCode.kt` for Kotlin and `diagnostics.ts` for Node. Node also sends the diagnostic category, so Kotlin never infers error meaning from code prefixes. +## Bounded property observations + +`PropertyRunConfiguration.observationRequest` opts into one observation artifact on the run result. Each requested +point names an assertion operand and its call site. The adapter records each callback invocation's original input, +precondition admission, predicate outcome, and phase. `invocation.input` is captured automatically at the callback +boundary. Named argument, return, intermediate, pre, and post operand points need explicit +`observePoint(id, value)` hook in the selected TypeScript source. The hook returns the same value. Repeated hits at one +static point have zero-based `occurrence` values and invocation-local `eventOrdinal` values. + +The request bounds invocations (at most 64), points per invocation (at most 8), array elements (at most 64), and +artifact bytes (at most 65,536). Dropped invocations and points are counted. A snapshot refuses proxies, accessors, +sparse arrays, nonstandard array prototypes, extra array properties, aliases, cycles, unsupported object types, and +arrays beyond the declared depth or element bound. Such values have an explicit `unsupported` status rather than a +fabricated concrete value. Byte-limited values have `truncated` status. Snapshot time is reported as +`captureTimeMillis`; it measures capture work, not end-to-end runtime overhead. + +Before importing the predicate, the adapter checks SHA-256 bytes of every selected source module in the request. +`verifiedSources` identifies only those selected modules. The build status remains `unverified`: the adapter does not +verify transpiled output, the loader, or transitive imports. Observation phases come from fast-check arbitrary +generation and shrink calls, explicit example identity, and replay requests. An `unknown` phase must not be treated +as a fresh independent sample. Observation is empirical and does not make an assertion sound or prove that a +recorded point is semantically relevant to a failure. + ## One property run ```mermaid diff --git a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts index 145b2d57bc..37be28fd61 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts @@ -54,6 +54,7 @@ export const adapterDiagnostic = { entryPointModuleNotFound: entryPoint('entrypoint.module.not-found'), entryPointModuleAmbiguous: entryPoint('entrypoint.module.ambiguous'), entryPointModuleImportFailed: entryPoint('entrypoint.module.import-failed'), + entryPointSourceHashMismatch: entryPoint('entrypoint.source-hash.mismatch'), entryPointExecutionKindMismatch: entryPoint('entrypoint.execution-kind.mismatch'), entryPointResultInvalid: entryPoint('entrypoint.result.invalid'), entryPointPreconditionThrew: entryPoint('entrypoint.precondition.threw'), diff --git a/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts b/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts index d12173cc76..1f4ff2f6fc 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/entry-point.ts @@ -1,4 +1,5 @@ -import { realpath, stat } from 'node:fs/promises'; +import { createHash } from 'node:crypto'; +import { readFile, realpath, stat } from 'node:fs/promises'; import path from 'node:path'; import { pathToFileURL } from 'node:url'; import { tsImport } from 'tsx/esm/api'; @@ -61,6 +62,23 @@ export async function loadEntryPoint( }; } +/** Verifies one selected source module's exact bytes before importing user code. */ +export async function verifySourceHash( + module: string, + expectedSha256: string, + sourceRoots: string[], +): Promise { + const modulePath = await resolveModule(module, sourceRoots, 'observationRequest.sources'); + const actual = createHash('sha256').update(await readFile(modulePath)).digest('hex'); + if (actual !== expectedSha256) { + throw protocolError( + adapterDiagnostic.entryPointSourceHashMismatch, + `Selected TypeScript source changed: ${module}`, + 'observationRequest.sources', + ); + } +} + async function resolveModule( module: string, sourceRoots: string[], diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts index 5451d23632..37964a31f0 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts @@ -9,6 +9,7 @@ import { EntryPointInvocationError, type ExecutionKind, loadEntryPoint, + verifySourceHash, type LoadedEntryPoint, type TypeScriptEntryPointReference, } from './entry-point.js'; @@ -20,7 +21,14 @@ import { protocolError, type TaggedJsValue, } from './js-value.js'; -import { buildPropertyArbitrary, validateJointGenerator } from './property-arbitrary.js'; +import { buildPropertyArbitrary, PhaseTrackingArbitrary, validateJointGenerator } from './property-arbitrary.js'; +import { + installObservationHook, + ObservationRecorder, + type ObservationArtifact, + type ObservationPointRequest, + type ObservationRequest, +} from './observe-property.js'; export interface PropertyManifestInput { name: string; @@ -65,6 +73,7 @@ export interface FastCheckExecutionRequest { numRuns: number; timeoutMillis: number; examples: TaggedJsValue[][]; + observationRequest?: ObservationRequest; } export interface FastCheckFailureDetails { @@ -84,6 +93,7 @@ export interface FastCheckRunResult { numShrinks: number; failure: FastCheckFailureDetails | null; executionTimeMillis: number; + observations?: ObservationArtifact; } export interface FastCheckExecutionSuccess { @@ -95,15 +105,30 @@ export async function executeProperty(requestValue: unknown): Promise request.replayPath === undefined + ? tracker?.phaseOf(values) ?? 'unknown' + : 'replay'; + const property = buildProperty(arbitrary, predicate, precondition, contractErrors, recorder, phaseOf); + const parameters = buildParameters(request, tracker); const details = await checkProperty(property, parameters, request.replayPath); @@ -116,6 +141,7 @@ export async function executeProperty(requestValue: unknown): Promise 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', ): fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]> { const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async'; @@ -132,10 +160,10 @@ function buildProperty( return fc.asyncProperty(arbitrary, (values: JsConcreteValue[]): Promise => preserveAsyncContractError( contractErrors, async () => { - const invocationValues = cloneArguments(values); - if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) fc.pre(false); + const result = await invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)); + if (result === null) fc.pre(false); - return await predicate.invoke(invocationValues); + return result; }, )); } @@ -143,14 +171,74 @@ function buildProperty( return fc.property(arbitrary, (values: JsConcreteValue[]): boolean => preserveContractError( contractErrors, () => { - const invocationValues = cloneArguments(values); - if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) fc.pre(false); + const result = invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)) as boolean | null; + if (result === null) fc.pre(false); - return predicate.invoke(invocationValues) as boolean; + return result; }, )); } +/** One invocation boundary; #353 exact replay uses the same shape after integration. */ +function invokePropertyOnce( + values: JsConcreteValue[], + predicate: LoadedEntryPoint, + precondition: LoadedEntryPoint | undefined, + recorder: ObservationRecorder | undefined, + phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', +): boolean | null | Promise { + const invocationValues = cloneArguments(values); + const invoke = (): boolean | null | Promise => { + if (predicate.executionKind === 'async' || precondition?.executionKind === 'async') { + return (async () => { + try { + if (precondition !== undefined && !(await invokePrecondition(precondition, invocationValues))) { + recorder?.finish('rejected', 'skipped'); + + return null; + } + } catch (error: unknown) { + recorder?.finish('threw', 'threw'); + throw error; + } + + try { + const result = await predicate.invoke(invocationValues); + recorder?.finish('admitted', result ? 'holds' : 'false'); + + return result; + } catch (error: unknown) { + recorder?.finish('admitted', 'threw'); + throw error; + } + })(); + } + + try { + if (precondition !== undefined && !invokeSynchronousPrecondition(precondition, invocationValues)) { + recorder?.finish('rejected', 'skipped'); + + return null; + } + } catch (error: unknown) { + recorder?.finish('threw', 'threw'); + throw error; + } + + try { + const result = predicate.invoke(invocationValues) as boolean; + recorder?.finish('admitted', result ? 'holds' : 'false'); + + return result; + } catch (error: unknown) { + recorder?.finish('admitted', 'threw'); + throw error; + } + }; + + return recorder === undefined ? invoke() : recorder.run(values, phase, invoke); +} + interface ContractErrorState { first: ProtocolError | undefined; } @@ -255,7 +343,10 @@ function cloneArguments(values: JsConcreteValue[]): JsConcreteValue[] { return structuredClone(values); } -function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConcreteValue[]]> { +function buildParameters( + request: FastCheckExecutionRequest, + tracker: PhaseTrackingArbitrary | undefined, +): Parameters<[JsConcreteValue[]]> { const decodedExamples = request.examples.map((example, exampleIndex): [JsConcreteValue[]] => { if (example.length !== request.manifest.inputs.length) { throw protocolError( @@ -267,6 +358,7 @@ function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConc const values = example.map((value, valueIndex) => decodeJsValue(value, `examples[${exampleIndex}][${valueIndex}]`)); + tracker?.markExplicit(values); if (request.manifest.generator !== undefined) { const [array, index] = values; if (!Array.isArray(array) || typeof index !== 'number' || !Number.isInteger(index) @@ -299,6 +391,7 @@ function toRunResult( propertyId: string, details: RunDetails<[JsConcreteValue[]]>, executionTimeMillis: number, + observations: ObservationArtifact | undefined, ): FastCheckRunResult { const counterexampleValues = details.counterexample?.[0]; const counterexample = counterexampleValues === undefined @@ -306,7 +399,7 @@ function toRunResult( : counterexampleValues.map(encodeJsValue); const failure = details.failed ? failureDetails(details) : null; - return { + const result: FastCheckRunResult = { propertyId, status: details.failed ? 'failure' : 'success', seed: details.seed, @@ -318,6 +411,9 @@ function toRunResult( failure, executionTimeMillis, }; + if (observations !== undefined) result.observations = observations; + + return result; } function failureDetails(details: RunDetails<[JsConcreteValue[]]>): FastCheckFailureDetails { @@ -446,6 +542,9 @@ function validateRequest(value: unknown): FastCheckExecutionRequest { if (request.seed !== undefined) validated.seed = request.seed as number; if (request.replayPath !== undefined) validated.replayPath = request.replayPath as string; + if (request.observationRequest !== undefined) { + validated.observationRequest = validateObservationRequest(request.observationRequest, manifest); + } return validated; } @@ -592,6 +691,89 @@ function validateSourcePoint(value: unknown, path: string): PropertySourcePointW return { module: point.module, line: point.line as number, column: point.column as number }; } +function validateObservationRequest(value: unknown, manifest: PropertyManifestWire): ObservationRequest { + const request = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, + 'Observation request must be an object', 'observationRequest'); + const validLimits = Number.isInteger(request.maxInvocations) && (request.maxInvocations as number) >= 1 + && (request.maxInvocations as number) <= 64 + && Number.isInteger(request.maxPointsPerInvocation) && (request.maxPointsPerInvocation as number) >= 1 + && (request.maxPointsPerInvocation as number) <= 8 + && Number.isInteger(request.maxArrayElements) && (request.maxArrayElements as number) >= 1 + && (request.maxArrayElements as number) <= 64 + && Number.isInteger(request.maxBytes) && (request.maxBytes as number) >= 1024 + && (request.maxBytes as number) <= 65_536; + if (!validLimits || !Array.isArray(request.points) || !Array.isArray(request.sources)) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid observation bounds', 'observationRequest'); + } + + const sources = request.sources.map((value: unknown, index: number) => { + const source = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, + 'Observation source must be an object', `observationRequest.sources[${index}]`); + if (typeof source.module !== 'string' || typeof source.sha256 !== 'string' + || !/^[0-9a-f]{64}$/.test(source.sha256)) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid source hash', `observationRequest.sources[${index}]`); + } + + return { module: source.module, sha256: source.sha256 }; + }); + const points = request.points.map((value: unknown, index: number) => { + const path = `observationRequest.points[${index}]`; + const point = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, 'Point must be an object', path); + if (typeof point.id !== 'string' || typeof point.assertionId !== 'string' + || typeof point.operandId !== 'string' + || !['argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid point identity', path); + } + + const validatedPoint: ObservationPointRequest = { + id: point.id, + assertionId: point.assertionId, + operandId: point.operandId, + source: validateSourcePoint(point.source, `${path}.source`), + callSite: validateSourcePoint(point.callSite, `${path}.callSite`), + kind: point.kind as ObservationPointRequest['kind'], + }; + if (point.kind === 'argument') { + if (!Number.isInteger(point.inputIndex) || (point.inputIndex as number) < 0 + || (point.inputIndex as number) >= manifest.inputs.length) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid argument index', `${path}.inputIndex`); + } + validatedPoint.inputIndex = point.inputIndex as number; + } else if (point.inputIndex !== undefined) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Only argument points may name an input index', path); + } + + return validatedPoint; + }); + const uniqueSources = new Set(sources.map((source) => source.module)); + const uniquePoints = new Set(points.map((point) => point.id)); + const allSourcesPresent = uniqueSources.has(manifest.predicate.module) + && points.every((point) => uniqueSources.has(point.source.module)); + const allPointsBound = points.every((point) => manifest.assertions?.some((assertion) => + assertion.id === point.assertionId && samePoint(assertion.testedCall, point.callSite) + && assertion.operands.some((operand) => + operand.id === point.operandId && samePoint(operand.source, point.source))) ?? false); + if (points.length === 0 || uniquePoints.size !== points.length || uniqueSources.size !== sources.length + || !allSourcesPresent || !allPointsBound) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, + 'Observation points must bind to declared assertion operands and selected source hashes', 'observationRequest'); + } + + return { + points, + sources, + maxInvocations: request.maxInvocations as number, + maxPointsPerInvocation: request.maxPointsPerInvocation as number, + maxArrayElements: request.maxArrayElements as number, + maxBytes: request.maxBytes as number, + }; +} + +function samePoint(left: PropertySourcePointWire | undefined, right: PropertySourcePointWire): boolean { + return left !== undefined && left.module === right.module + && left.line === right.line && left.column === right.column; +} + function validateEntryPoint(value: unknown, entryPath: string): TypeScriptEntryPointReference { const entryPoint = requireRecord( value, diff --git a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts new file mode 100644 index 0000000000..099c8b42f0 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts @@ -0,0 +1,230 @@ +import { AsyncLocalStorage } from 'node:async_hooks'; +import { randomUUID } from 'node:crypto'; +import { performance } from 'node:perf_hooks'; +import { types } from 'node:util'; +import { encodeJsValue, type TaggedJsValue } from './js-value.js'; + +export interface ObservationPointRequest { + id: string; + assertionId: string; + operandId: string; + source: SourcePoint; + callSite: SourcePoint; + kind: 'argument' | 'return' | 'intermediate' | 'pre' | 'post'; + inputIndex?: number; +} + +export interface SourcePoint { + module: string; + line: number; + column: number; +} + +export interface ObservationSource { + module: string; + sha256: string; +} + +export interface ObservationRequest { + points: ObservationPointRequest[]; + sources: ObservationSource[]; + maxInvocations: number; + maxPointsPerInvocation: number; + maxArrayElements: number; + maxBytes: number; +} + +export interface ObservationValue { + status: 'captured' | 'unsupported' | 'truncated'; + value?: TaggedJsValue; + reason?: string; +} + +interface InvocationRecord { + invocationId: number; + parentInvocationId: null; + callSite: SourcePoint | null; + origin: 'fast-check'; + phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown'; + input: ObservationValue; + admission: 'pending' | 'admitted' | 'rejected' | 'threw'; + outcome: 'pending' | 'holds' | 'false' | 'threw' | 'skipped'; + points: Array & { + pointId: string; + occurrence: number; + eventOrdinal: number; + value: ObservationValue; + }>; +} + +export interface ObservationArtifact { + propertyId: string; + runId: string; + verifiedSources: ObservationSource[]; + buildStatus: 'unverified'; + invocations: InvocationRecord[]; + droppedInvocations: number; + droppedPoints: number; + captureTimeMillis: number; +} + +interface ObservationContext { + recorder: ObservationRecorder; + invocation: InvocationRecord; +} + +const contexts = new AsyncLocalStorage(); +const hookSymbol = Symbol.for('org.usvm.ts.pbt.observe'); + +/** Explicit hook observes a computed value and returns the identical value. */ +export function installObservationHook(): void { + Object.defineProperty(globalThis, hookSymbol, { + configurable: true, + value: (pointId: string, value: unknown): unknown => { + const context = contexts.getStore(); + context?.recorder.point(context.invocation, pointId, value); + + return value; + }, + }); +} + +export class ObservationRecorder { + private readonly artifact: ObservationArtifact; + private readonly pointsById: Map; + + constructor(propertyId: string, private readonly request: ObservationRequest) { + this.pointsById = new Map(request.points.map((point) => [point.id, point])); + this.artifact = { + propertyId, + runId: randomUUID(), + verifiedSources: request.sources, + buildStatus: 'unverified', + invocations: [], + droppedInvocations: 0, + droppedPoints: 0, + captureTimeMillis: 0, + }; + } + + get result(): ObservationArtifact { + this.artifact.captureTimeMillis = Math.round(this.artifact.captureTimeMillis); + + return this.artifact; + } + + run( + values: unknown[], + phase: InvocationRecord['phase'], + invocation: () => T, + ): T { + if (this.artifact.invocations.length >= this.request.maxInvocations) { + this.artifact.droppedInvocations += 1; + + return invocation(); + } + + const record: InvocationRecord = { + invocationId: this.artifact.invocations.length, + parentInvocationId: null, + callSite: this.request.points[0]?.callSite ?? null, + origin: 'fast-check', + phase, + input: this.snapshot(values), + admission: 'pending', + outcome: 'pending', + points: [], + }; + this.artifact.invocations.push(record); + if (this.artifactBytes() > this.request.maxBytes) { + this.artifact.invocations.pop(); + this.artifact.droppedInvocations += 1; + + return invocation(); + } + + return contexts.run({ recorder: this, invocation: record }, invocation); + } + + finish(admission: InvocationRecord['admission'], outcome: InvocationRecord['outcome']): void { + const record = contexts.getStore()?.invocation; + if (record !== undefined) { + record.admission = admission; + record.outcome = outcome; + } + } + + point(record: InvocationRecord, pointId: string, value: unknown): void { + const point = this.pointsById.get(pointId); + if (point === undefined || record.points.length >= this.request.maxPointsPerInvocation) { + this.artifact.droppedPoints += 1; + + return; + } + + record.points.push({ + pointId: point.id, + assertionId: point.assertionId, + operandId: point.operandId, + source: point.source, + callSite: point.callSite, + kind: point.kind, + ...(point.inputIndex === undefined ? {} : { inputIndex: point.inputIndex }), + occurrence: record.points.filter((event) => event.pointId === point.id).length, + eventOrdinal: record.points.length, + value: this.snapshot(value), + }); + if (this.artifactBytes() > this.request.maxBytes) { + record.points.pop(); + this.artifact.droppedPoints += 1; + } + } + + private snapshot(value: unknown): ObservationValue { + const startedAt = performance.now(); + try { + const reason = unsafeReason(value, this.request.maxArrayElements, new WeakSet(), 0); + if (reason !== undefined) return { status: 'unsupported', reason }; + + const tagged = encodeJsValue(value); + const bytes = Buffer.byteLength(JSON.stringify(tagged), 'utf8'); + if (this.artifactBytes() + bytes > this.request.maxBytes) { + return { status: 'truncated', reason: 'byte-budget' }; + } + + return { status: 'captured', value: tagged }; + } finally { + this.artifact.captureTimeMillis += performance.now() - startedAt; + } + } + + private artifactBytes(): number { + return Buffer.byteLength(JSON.stringify(this.artifact), 'utf8'); + } +} + +function unsafeReason(value: unknown, maxArrayElements: number, seen: WeakSet, depth: number): string | undefined { + if (value === null || value === undefined || ['boolean', 'string', 'number'].includes(typeof value)) return undefined; + if (types.isProxy(value)) return 'proxy'; + if (!Array.isArray(value)) return 'unsupported-type'; + if (depth >= 4) return 'depth-limit'; + if (Object.getPrototypeOf(value) !== Array.prototype) return 'array-prototype'; + if (seen.has(value)) return 'alias-or-cycle'; + if (value.length > maxArrayElements) return 'array-element-limit'; + + seen.add(value); + const descriptors = Object.getOwnPropertyDescriptors(value); + if (Object.keys(descriptors).some((key) => key !== 'length' && !/^(0|[1-9]\d*)$/.test(key))) { + return 'array-extra-property'; + } + for (let index = 0; index < value.length; index += 1) { + const descriptor = descriptors[String(index)]; + if (descriptor === undefined) return 'sparse-array'; + if (!('value' in descriptor)) return 'accessor'; + + const reason = unsafeReason(descriptor.value, maxArrayElements, seen, depth + 1); + if (reason !== undefined) return reason; + } + + return undefined; +} diff --git a/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts b/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts index cdbd82ceb2..b21a133320 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts @@ -26,6 +26,45 @@ export function buildPropertyArbitrary(manifest: PropertyManifestWire): fc.Arbit }); } +/** Tracks fast-check's own generate/shrink calls by value identity, including cloned values. */ +export class PhaseTrackingArbitrary extends fc.Arbitrary { + private readonly phases = new WeakMap(); + private readonly explicit = new WeakSet(); + + constructor(private readonly delegate: fc.Arbitrary) { + super(); + } + + markExplicit(values: JsConcreteValue[]): void { + this.explicit.add(values); + } + + phaseOf(values: JsConcreteValue[]): 'generation' | 'shrink' | 'explicit' | 'unknown' { + return this.phases.get(values) ?? (this.explicit.has(values) ? 'explicit' : 'unknown'); + } + + generate(mrng: fc.Random, biasFactor: number | undefined): fc.Value { + return this.tag(this.delegate.generate(mrng, biasFactor), 'generation'); + } + + canShrinkWithoutContext(value: unknown): value is JsConcreteValue[] { + return this.delegate.canShrinkWithoutContext(value); + } + + shrink(value: JsConcreteValue[], context: unknown): fc.Stream> { + return this.delegate.shrink(value, context).map((entry) => this.tag(entry, 'shrink')); + } + + private tag(entry: fc.Value, phase: 'generation' | 'shrink'): fc.Value { + return new fc.Value(entry.value_, entry.context, () => { + const values = entry.value; + this.phases.set(values, phase); + + return values; + }); + } +} + /** Checks the declared domains before a dependent arbitrary can sample outside either one. */ export function validateJointGenerator(manifest: PropertyManifestWire): void { const generator = manifest.generator; diff --git a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts index f8e6bdd80c..8dbea1794f 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts @@ -1,10 +1,12 @@ import assert from 'node:assert/strict'; +import { createHash } from 'node:crypto'; 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 { fileURLToPath } from 'node:url'; import { tsImport } from 'tsx/esm/api'; +import { installObservationHook, ObservationRecorder, type ObservationRequest } from '../src/observe-property.js'; import { encodeJsValue, ProtocolError } from '../src/js-value.js'; import { executeProperty, @@ -101,6 +103,175 @@ test('rejects array-index manifests that conflict with declared input domains be }); }); +test('bounded explicit observation preserves special values and refuses proxies, accessors, and aliases', () => { + const request: ObservationRequest = { + points: [{ + id: 'result', + assertionId: 'assertion', + operandId: 'result', + source: { module: 'property.ts', line: 1, column: 1 }, + callSite: { module: 'property.ts', line: 1, column: 1 }, + kind: 'intermediate', + }], + sources: [{ module: 'property.ts', sha256: 'a'.repeat(64) }], + maxInvocations: 2, + maxPointsPerInvocation: 4, + maxArrayElements: 4, + maxBytes: 65_536, + }; + const recorder = new ObservationRecorder('property', request); + installObservationHook(); + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')] as + (pointId: string, value: unknown) => unknown; + const proxy = new Proxy([1], {}); + let getterCalls = 0; + const accessor = [1]; + Object.defineProperty(accessor, '0', { get: () => { getterCalls += 1; return 1; } }); + const shared = [1]; + + recorder.run([Number.NaN, -0], 'unknown', () => { + assert.equal(hook('result', Number.POSITIVE_INFINITY), Number.POSITIVE_INFINITY); + assert.equal(hook('result', proxy), proxy); + assert.equal(hook('result', accessor), accessor); + hook('result', [shared, shared]); + }); + hook('result', 7); + + const [first] = recorder.result.invocations; + assert.ok(first); + assert.deepEqual(first.input.value, { kind: 'array', elements: [ + { kind: 'number', value: 'nan' }, + { kind: 'number', value: 'finite', bits: '8000000000000000' }, + ] }); + assert.deepEqual(first.points.map((event) => event.value.status), + ['captured', 'unsupported', 'unsupported', 'unsupported']); + assert.deepEqual(first.points.slice(1).map((event) => event.value.reason), + ['proxy', 'accessor', 'alias-or-cycle']); + assert.equal(getterCalls, 0); + assert.equal(recorder.result.invocations.length, 1); +}); + +test('observation limits report dropped invocations and points without changing returned values', () => { + const request: ObservationRequest = { + points: [{ + id: 'point', assertionId: 'assertion', operandId: 'point', + source: { module: 'property.ts', line: 1, column: 1 }, + callSite: { module: 'property.ts', line: 1, column: 1 }, + kind: 'intermediate', + }], + sources: [{ module: 'property.ts', sha256: 'a'.repeat(64) }], + maxInvocations: 1, + maxPointsPerInvocation: 1, + maxArrayElements: 2, + maxBytes: 1024, + }; + const recorder = new ObservationRecorder('property', request); + installObservationHook(); + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')] as + (pointId: string, value: unknown) => unknown; + + recorder.run([1], 'unknown', () => { + const large = 'x'.repeat(2048); + assert.equal(hook('point', large), large); + hook('point', 4); + }); + recorder.run([2], 'unknown', () => hook('point', 5)); + + assert.equal(recorder.result.invocations[0]?.input.status, 'captured'); + assert.equal(recorder.result.invocations[0]?.points[0]?.value.status, 'truncated'); + assert.equal(recorder.result.droppedPoints, 1); + assert.equal(recorder.result.droppedInvocations, 1); +}); + +test('repeated point occurrences and a numeric tested return stay distinct from predicate outcome', async () => { + await withPropertyModule(async (sourceRoot) => { + const baselineRequest = executionRequest(sourceRoot, 'repeatedPoint'); + baselineRequest.examples = [[encodeJsValue(2)]]; + baselineRequest.numRuns = 1; + const point = { module: 'properties.ts', line: 1, column: 1 }; + baselineRequest.manifest.assertions = [{ + id: 'loop-result', source: point, testedCall: point, + operands: [{ id: 'input', source: point }, { id: 'step', source: point }, + { id: 'tested-return', source: point }], + }]; + const observedRequest: FastCheckExecutionRequest = { + ...baselineRequest, + observationRequest: { + points: [ + { id: 'input', assertionId: 'loop-result', operandId: 'input', source: point, callSite: point, + kind: 'argument', inputIndex: 0 }, + { id: 'step', assertionId: 'loop-result', operandId: 'step', source: point, callSite: point, + kind: 'intermediate' }, + { id: 'tested-return', assertionId: 'loop-result', operandId: 'tested-return', + source: point, callSite: point, kind: 'return' }, + ], + sources: [{ module: 'properties.ts', sha256: createHash('sha256').update(PROPERTY_MODULE_SOURCE).digest('hex') }], + maxInvocations: 64, maxPointsPerInvocation: 8, maxArrayElements: 16, maxBytes: 65_536, + }, + }; + + const baseline = await executeProperty(baselineRequest); + const observed = await executeProperty(observedRequest); + + const { observations, ...observedResult } = observed.result; + assert.deepEqual(semanticResult(observedResult), semanticResult(baseline.result)); + assert.ok(observations); + const first = observations.invocations[0]; + assert.ok(first); + assert.equal(first.phase, 'explicit'); + assert.equal(first.outcome, 'false'); + assert.deepEqual(first.points.map((event) => [event.pointId, event.occurrence, event.eventOrdinal]), [ + ['input', 0, 0], ['step', 0, 1], ['step', 1, 2], ['step', 2, 3], ['tested-return', 0, 4], + ]); + assert.deepEqual(first.points.map((event) => event.value.value), [ + encodeJsValue(2), encodeJsValue(0), encodeJsValue(1), encodeJsValue(3), encodeJsValue(42), + ]); + }); +}); + +test('observation preserves mutation, special values, throws, and short-circuit outcomes', async () => { + await withPropertyModule(async (sourceRoot) => { + const nestedArray = { kind: 'array', element: { kind: 'array', + element: { kind: 'integer', min: 1, max: 1 }, minLength: 1, maxLength: 1 }, + minLength: 1, maxLength: 1 }; + const cases = [ + { exportName: 'mutatesNestedArrayToObject', domain: nestedArray }, + { exportName: 'throwsInput', domain: constantDomain('thrown-value') }, + { exportName: 'recognizesNegativeZero', domain: constantDomain(-0) }, + { exportName: 'shortCircuitsObservation', domain: constantDomain(1) }, + ]; + const point = { module: 'properties.ts', line: 1, column: 1 }; + const sourceHash = createHash('sha256').update(PROPERTY_MODULE_SOURCE).digest('hex'); + + for (const entry of cases) { + const baselineRequest = executionRequest(sourceRoot, entry.exportName, { inputDomain: entry.domain }); + baselineRequest.numRuns = 1; + baselineRequest.manifest.assertions = [{ id: 'case', source: point, testedCall: point, + operands: [{ id: 'side-effect', source: point }] }]; + const observedRequest: FastCheckExecutionRequest = { + ...baselineRequest, + observationRequest: { + points: [{ id: 'side-effect', assertionId: 'case', operandId: 'side-effect', + source: point, callSite: point, kind: 'intermediate' }], + sources: [{ module: 'properties.ts', sha256: sourceHash }], + maxInvocations: 64, maxPointsPerInvocation: 8, maxArrayElements: 16, maxBytes: 65_536, + }, + }; + + const baseline = await executeProperty(baselineRequest); + const observed = await executeProperty(observedRequest); + + const { observations, ...observedResult } = observed.result; + assert.deepEqual(semanticResult(observedResult), semanticResult(baseline.result), entry.exportName); + assert.ok(observations); + assert.equal(observations.invocations[0]?.input.status, 'captured'); + if (entry.exportName === 'shortCircuitsObservation') { + assert.equal(observations.invocations[0]?.points.length, 0); + } + } + }); +}); + test('executes a synchronous TypeScript predicate with deterministic success details', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'alwaysTrue'); @@ -455,6 +626,29 @@ test('reports asynchronous predicate timeout as a structured timeout failure', a }); }); +test('an interrupted asynchronous observation keeps an explicit pending state', async () => { + await withPropertyModule(async (sourceRoot) => { + const request = executionRequest(sourceRoot, 'neverCompletes', { predicateExecutionKind: 'async' }); + const point = { module: 'properties.ts', line: 1, column: 1 }; + request.manifest.assertions = [{ id: 'timeout', source: point, testedCall: point, + operands: [{ id: 'unreached', source: point }] }]; + request.observationRequest = { + points: [{ id: 'unreached', assertionId: 'timeout', operandId: 'unreached', + source: point, callSite: point, kind: 'intermediate' }], + sources: [{ module: 'properties.ts', sha256: createHash('sha256').update(PROPERTY_MODULE_SOURCE).digest('hex') }], + maxInvocations: 1, maxPointsPerInvocation: 1, maxArrayElements: 4, maxBytes: 4096, + }; + request.timeoutMillis = 20; + request.numRuns = 1; + + const result = await executeProperty(request); + + assert.equal(result.result.failure?.kind, 'timeout'); + assert.equal(result.result.observations?.invocations[0]?.admission, 'pending'); + assert.equal(result.result.observations?.invocations[0]?.outcome, 'pending'); + }); +}); + test('keeps a counterexample classified as a property failure when shrinking is interrupted', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'slowFailure', { @@ -673,6 +867,31 @@ export function mutatesArrayToCycle(value: unknown[]): boolean { export function throwsInput(value: unknown): never { throw value; } + +export function recognizesNegativeZero(value: number): boolean { + return Object.is(value, -0); +} + +export function shortCircuitsObservation(_value: number): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')]; + const skipped = false && typeof hook === 'function' && Boolean((hook as (id: string, value: number) => number)('side-effect', 1)); + + return skipped === false; +} + +export function repeatedPoint(value: number): boolean { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')]; + if (typeof hook === 'function') (hook as (id: string, result: number) => void)('input', value); + let total = 0; + for (let index = 0; index < 3; index += 1) { + total += index; + if (typeof hook === 'function') (hook as (id: string, result: number) => void)('step', total); + } + const testedReturn = (() => 42)(); + if (typeof hook === 'function') (hook as (id: string, result: number) => void)('tested-return', testedReturn); + + return value !== 2; +} `.trimStart(); const CONTRACT_SOURCE_ROOT = fileURLToPath(new URL('../../../src/test/resources/', import.meta.url)); diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt index 88b794cbd6..f23558924a 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt @@ -25,6 +25,7 @@ internal object FastCheckDiagnosticCode { const val BACKEND_EXAMPLES_ARITY = "backend.examples.arity" const val BACKEND_EXAMPLES_DOMAIN = "backend.examples.domain" const val BACKEND_EXAMPLES_VALUE_INVALID = "backend.examples.value.invalid" + const val BACKEND_OBSERVATION_INVALID = "backend.observation.invalid" const val BACKEND_PROCESS_FAILED = "backend.process.failed" const val BACKEND_PROCESS_INTERRUPTED = "backend.process.interrupted" const val BACKEND_PROCESS_READ_FAILED = "backend.process.read.failed" diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 9a4d539a17..58e2d85749 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -11,6 +11,7 @@ import org.usvm.ts.pbt.model.JsNumberKind import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.accepts import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.observation.PropertyObservationRequest import org.usvm.ts.pbt.validation.requireValid import org.usvm.ts.pbt.validation.validatePropertyDefinition import java.io.IOException @@ -52,6 +53,7 @@ class FastCheckBackend( numRuns = configuration.numRuns, timeoutMillis = configuration.timeoutMillis, examples = configuration.examples, + observationRequest = configuration.observationRequest, coverageRequest = configuration.coverageRequest, ) @@ -63,6 +65,45 @@ class FastCheckBackend( configuration: PropertyRunConfiguration, ) { validateExamples(property, configuration) + configuration.observationRequest?.let { validateObservationRequest(property, it) } + } + + private fun validateObservationRequest(property: PropertyDefinition, request: PropertyObservationRequest) { + val validLimits = request.maxInvocations in 1..MAX_OBSERVED_INVOCATIONS && + request.maxPointsPerInvocation in 1..MAX_OBSERVED_POINTS && + request.maxArrayElements in 1..MAX_OBSERVED_ARRAY_ELEMENTS && + request.maxBytes in MIN_OBSERVED_BYTES..MAX_OBSERVED_BYTES + val sourceByModule = request.sources.associateBy { it.module } + val allSourcesPresent = property.predicate.module in sourceByModule && + request.points.all { point -> point.source.module in sourceByModule } + val allPointsBound = request.points.all { point -> + property.assertions.any { assertion -> + assertion.id == point.assertionId && assertion.testedCall == point.callSite && + assertion.operands.any { operand -> + operand.id == point.operandId && operand.source == point.source + } + } + } + val allInputIndexesValid = request.points.all { point -> + if (point.kind == org.usvm.ts.pbt.observation.ObservationPointKind.ARGUMENT) { + point.inputIndex in property.inputs.indices + } else { + point.inputIndex == null + } + } + val hashesValid = request.sources.all { source -> source.sha256.matches(SHA256_REGEX) } + + val validRequest = validLimits && request.points.isNotEmpty() && allSourcesPresent && + allPointsBound && allInputIndexesValid && hashesValid + + if (!validRequest) { + throw invalidRequest( + code = FastCheckDiagnosticCode.BACKEND_OBSERVATION_INVALID, + message = "Observation request has invalid limits, source hashes, or assertion bindings", + property = property, + path = "observationRequest", + ) + } } private fun validateExamples( @@ -160,6 +201,12 @@ class FastCheckBackend( const val FAST_CHECK_BACKEND_ID = "fast-check" private val FINITE_NUMBER_BITS_REGEX = Regex("[0-9a-f]{16}") + private val SHA256_REGEX = Regex("[0-9a-f]{64}") + private const val MAX_OBSERVED_INVOCATIONS = 64 + private const val MAX_OBSERVED_POINTS = 8 + private const val MAX_OBSERVED_ARRAY_ELEMENTS = 64 + private const val MAX_OBSERVED_BYTES = 65_536 + private const val MIN_OBSERVED_BYTES = 1024 private fun canonicalizeSourceRoots(sourceRoots: List): List { if (sourceRoots.isEmpty()) { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt index 2002aaa046..5a9d1caa16 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt @@ -7,6 +7,7 @@ import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyRunResult import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.PropertyObservationRequest @Serializable internal data class FastCheckExecutionRequest( @@ -17,6 +18,7 @@ internal data class FastCheckExecutionRequest( val numRuns: Int, val timeoutMillis: Long, val examples: List> = emptyList(), + val observationRequest: PropertyObservationRequest? = null, @Transient val coverageRequest: PropertyCoverageRequest? = null, ) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt index a0439768f4..9282da18f1 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt @@ -5,6 +5,7 @@ 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.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.ArrayDomain @@ -18,13 +19,134 @@ import org.usvm.ts.pbt.model.PropertyOperand import org.usvm.ts.pbt.model.PropertySourceIdentity import org.usvm.ts.pbt.model.PropertySourcePoint import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationAdmission +import org.usvm.ts.pbt.observation.ObservationOutcome +import org.usvm.ts.pbt.observation.ObservationPhase +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationRequest +import org.usvm.ts.pbt.observation.PropertyObservationSource import org.usvm.ts.pbt.testResourcesRoot import java.nio.file.Files +import java.nio.file.Path import java.security.MessageDigest import kotlin.test.assertEquals import kotlin.test.assertNotNull +import kotlin.test.assertTrue class RealSuiteRegistrationTest { + @Test + fun `original callback yields bounded input intermediate and outcome observations`() { + val source = testResourcesRoot().resolve(MODULE) + val hash = sourceHash(source) + val definition = property( + exportName = "originalUniqueOracle", + sourceIdentity = PropertySourceIdentity( + sourceSha256 = hash, + buildSha256 = hash, + buildScope = "direct TypeScript source input", + ), + ) + val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + val values = JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0), JsConcreteValue.number(1.0))) + + val result = backend.run( + property = definition, + configuration = PropertyRunConfiguration( + numRuns = 1, + examples = listOf(listOf(values)), + observationRequest = observationRequest(definition, hash), + ), + ) + val correct = property( + exportName = "correctUniqueOracle", + sourceIdentity = definition.sourceIdentity, + ) + val correctResult = backend.run( + property = correct, + configuration = PropertyRunConfiguration( + numRuns = 1, + examples = listOf(listOf(values)), + observationRequest = observationRequest(correct, hash), + ), + ) + + val artifact = assertNotNull(result.observations) + val invocation = artifact.invocations.first() + val correctInvocation = assertNotNull(correctResult.observations).invocations.first() + assertEquals(ObservationPhase.EXPLICIT, invocation.phase) + assertEquals(ObservationAdmission.ADMITTED, invocation.admission) + assertEquals(ObservationOutcome.THREW, invocation.outcome) + assertEquals(ObservationValueStatus.CAPTURED, invocation.input.status) + assertEquals(listOf("input-array", "filtered-array"), invocation.points.map { it.pointId }) + assertEquals(values, invocation.points[0].value.value) + assertEquals(values, invocation.points[1].value.value) + assertEquals(ObservationOutcome.HOLDS, correctInvocation.outcome) + assertEquals( + JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0))), + correctInvocation.points[1].value.value, + ) + assertEquals(0, artifact.droppedPoints) + assertTrue(artifact.captureTimeMillis >= 0) + assertTrue(artifact.invocations.drop(1).all { it.phase == ObservationPhase.SHRINK }) + + val replayPath = assertNotNull(result.replayPath) + val replay = backend.run( + property = definition, + configuration = PropertyRunConfiguration( + seed = result.seed, + replayPath = replayPath, + numRuns = 1, + examples = listOf(listOf(values)), + observationRequest = observationRequest(definition, hash), + ), + ) + + assertTrue(assertNotNull(replay.observations).invocations.all { it.phase == ObservationPhase.REPLAY }) + + val generated = backend.run( + property = correct, + configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 3, + observationRequest = observationRequest(correct, hash), + ), + ) + + assertTrue(assertNotNull(generated.observations).invocations.all { it.phase == ObservationPhase.GENERATION }) + } + + @Test + fun `changed selected source is rejected before import`() { + val original = testResourcesRoot().resolve(MODULE) + val hash = sourceHash(original) + val root = Files.createTempDirectory("pbt-observation-stale-") + val changed = root.resolve(MODULE) + Files.createDirectories(changed.parent) + Files.writeString(changed, Files.readString(original) + "\n// changed\n") + val definition = property(exportName = "originalUniqueOracle", sourceIdentity = null) + + try { + val error = kotlin.test.assertFailsWith { + FastCheckBackend(sourceRoots = listOf(root)).run( + property = definition, + configuration = PropertyRunConfiguration( + numRuns = 1, + observationRequest = observationRequest(definition, hash), + ), + ) + } + + assertEquals("entrypoint.source-hash.mismatch", error.code) + } finally { + Files.delete(changed) + Files.delete(changed.parent) + Files.delete(changed.parent.parent) + Files.delete(root) + } + } + @Test fun `original fast-check uniqueness oracle retains its assertion and failure`() { val source = testResourcesRoot().resolve(MODULE) @@ -59,7 +181,7 @@ class RealSuiteRegistrationTest { assertEquals("fast-check.array-bias.unique", manifest.propertyId) assertEquals("no-duplicates", manifest.assertions.single().id) assertEquals( - listOf("filtered-array", "expected-set-size"), + listOf("input-array", "filtered-array", "expected-set-size"), manifest.assertions.single().operands.map(PropertyOperand::id), ) assertEquals(sourceHash, manifest.sourceIdentity?.sourceSha256) @@ -70,35 +192,80 @@ class RealSuiteRegistrationTest { assertEquals(PropertyRunStatus.SUCCESS, passed.status) } - private fun property(exportName: String, sourceIdentity: PropertySourceIdentity?) = PropertyDefinition( - id = PropertyId("fast-check.array-bias.unique"), - inputs = listOf( - PropertyInput( - name = "values", - domain = ArrayDomain(IntegerDomain(min = 0, max = 10), minLength = 0, maxLength = 8), - generatorId = "fast-check.array-integers", + private fun property(exportName: String, sourceIdentity: PropertySourceIdentity?): PropertyDefinition { + val correct = exportName == "correctUniqueOracle" + + return PropertyDefinition( + id = PropertyId("fast-check.array-bias.unique"), + inputs = listOf( + PropertyInput( + name = "values", + domain = ArrayDomain(IntegerDomain(min = 0, max = 10), minLength = 0, maxLength = 8), + generatorId = "fast-check.array-integers", + ), ), - ), - predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName), - assertions = listOf( - PropertyAssertion( - id = "no-duplicates", - source = PropertySourcePoint(module = MODULE, line = 18, column = 5), - testedCall = PropertySourcePoint(module = MODULE, line = 17, column = 22), - operands = listOf( - PropertyOperand( - id = "filtered-array", - source = PropertySourcePoint(module = MODULE, line = 18, column = 12), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName), + assertions = listOf( + PropertyAssertion( + id = "no-duplicates", + source = PropertySourcePoint(module = MODULE, line = if (correct) 34 else 20, column = 5), + testedCall = PropertySourcePoint( + module = MODULE, + line = if (correct) 31 else 18, + column = if (correct) 26 else 22, ), - PropertyOperand( - id = "expected-set-size", - source = PropertySourcePoint(module = MODULE, line = 18, column = 34), + operands = listOf( + PropertyOperand( + id = "input-array", + source = PropertySourcePoint(module = MODULE, line = if (correct) 30 else 16, column = 5), + ), + PropertyOperand( + id = "filtered-array", + source = PropertySourcePoint(module = MODULE, line = if (correct) 32 else 19, column = 5), + ), + PropertyOperand( + id = "expected-set-size", + source = PropertySourcePoint(module = MODULE, line = if (correct) 34 else 20, column = 35), + ), ), ), ), - ), - sourceIdentity = sourceIdentity, - ) + sourceIdentity = sourceIdentity, + ) + } + + private fun observationRequest(definition: PropertyDefinition, hash: String): PropertyObservationRequest { + val assertion = definition.assertions.single() + val input = assertion.operands.first() + val filtered = assertion.operands[1] + + return PropertyObservationRequest( + points = listOf( + PropertyObservationPoint( + id = input.id, + assertionId = assertion.id, + operandId = input.id, + source = input.source, + callSite = requireNotNull(assertion.testedCall), + kind = ObservationPointKind.ARGUMENT, + inputIndex = 0, + ), + PropertyObservationPoint( + id = filtered.id, + assertionId = assertion.id, + operandId = filtered.id, + source = filtered.source, + callSite = requireNotNull(assertion.testedCall), + kind = ObservationPointKind.INTERMEDIATE, + ), + ), + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)), + ) + } + + private fun sourceHash(path: Path): String = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(path)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } private companion object { const val MODULE = "properties/real/ArrayArbitraryProperty.ts" diff --git a/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts b/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts index 45f9bfadac..2e97082119 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts +++ b/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts @@ -13,8 +13,10 @@ export function expect(value: T[]): { toHaveLength(expected: number): void } } export function originalUniqueAssertion(arr: number[]): void { + observePoint('input-array', arr); const removeDuplicates = (values: number[]) => [...values]; const filtered = removeDuplicates(arr); + observePoint('filtered-array', filtered); expect(filtered).toHaveLength(new Set(filtered).size); } @@ -25,9 +27,17 @@ export function originalUniqueOracle(values: number[]): boolean { } export function correctUniqueOracle(values: number[]): boolean { + observePoint('input-array', values); const filtered = [...new Set(values)]; + observePoint('filtered-array', filtered); expect(filtered).toHaveLength(new Set(filtered).size); return true; } + +function observePoint(id: string, value: T): T { + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')]; + + return typeof hook === 'function' ? (hook as (pointId: string, value: T) => T)(id, value) : value; +} 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 94f433c8f1..268682aabe 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 @@ -5,6 +5,8 @@ import kotlinx.serialization.Serializable import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.PropertyObservationArtifact +import org.usvm.ts.pbt.observation.PropertyObservationRequest /** Executes validated Kotlin property definitions through one concrete PBT engine. */ interface PropertyBasedTestingBackend { @@ -26,6 +28,7 @@ data class PropertyRunConfiguration( val timeoutMillis: Long = DEFAULT_TIMEOUT_MILLIS, val examples: List> = emptyList(), val coverageRequest: PropertyCoverageRequest? = null, + val observationRequest: PropertyObservationRequest? = null, ) { init { require(numRuns > 0) { "Number of runs must be positive" } @@ -96,6 +99,7 @@ data class PropertyRunResult( val failure: PropertyFailureDetails?, val executionTimeMillis: Long, val coverage: PropertyCoverageArtifact? = null, + val observations: PropertyObservationArtifact? = null, ) { init { require(numRuns >= 0) { "Run count must not be negative" } @@ -105,6 +109,9 @@ data class PropertyRunResult( require(coverage == null || coverage.propertyId == propertyId) { "Coverage property ID must match the run result" } + require(observations == null || observations.propertyId == propertyId) { + "Observation property ID must match the run result" + } when (status) { PropertyRunStatus.SUCCESS -> { diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt new file mode 100644 index 0000000000..a32f2d6bf5 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/PropertyObservation.kt @@ -0,0 +1,199 @@ +package org.usvm.ts.pbt.observation + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertySourcePoint + +/** One explicit point tied to an original assertion and operand. */ +@Serializable +data class PropertyObservationPoint( + val id: String, + val assertionId: String, + val operandId: String, + val source: PropertySourcePoint, + val callSite: PropertySourcePoint, + val kind: ObservationPointKind, + val inputIndex: Int? = null, +) + +/** Location and role of a recorded operand value. */ +@Serializable +enum class ObservationPointKind { + @SerialName("argument") + ARGUMENT, + + @SerialName("return") + RETURN, + + @SerialName("intermediate") + INTERMEDIATE, + + @SerialName("pre") + PRE, + + @SerialName("post") + POST, +} + +/** Whether a value could be represented within the observation bounds. */ +@Serializable +enum class ObservationValueStatus { + @SerialName("captured") + CAPTURED, + + @SerialName("unsupported") + UNSUPPORTED, + + @SerialName("truncated") + TRUNCATED, +} + +/** Runtime that produced the observed invocation. */ +@Serializable +enum class ObservationOrigin { + @SerialName("fast-check") + FAST_CHECK, + + @SerialName("solver") + SOLVER, + + @SerialName("returned-seed") + RETURNED_SEED, + + @SerialName("returned-neighborhood") + RETURNED_NEIGHBORHOOD, +} + +/** Fast-check activity that produced the invocation input. */ +@Serializable +enum class ObservationPhase { + @SerialName("generation") + GENERATION, + + @SerialName("explicit") + EXPLICIT, + + @SerialName("shrink") + SHRINK, + + @SerialName("replay") + REPLAY, + + @SerialName("unknown") + UNKNOWN, +} + +/** Precondition result for an observed invocation. */ +@Serializable +enum class ObservationAdmission { + @SerialName("pending") + PENDING, + + @SerialName("admitted") + ADMITTED, + + @SerialName("rejected") + REJECTED, + + @SerialName("threw") + THREW, +} + +/** Predicate result for an observed invocation. */ +@Serializable +enum class ObservationOutcome { + @SerialName("pending") + PENDING, + + @SerialName("holds") + HOLDS, + + @SerialName("false") + FALSE, + + @SerialName("threw") + THREW, + + @SerialName("skipped") + SKIPPED, +} + +/** Verification status of executable build provenance. */ +@Serializable +enum class ObservationBuildStatus { + @SerialName("unverified") + UNVERIFIED, + + @SerialName("verified") + VERIFIED, +} + +/** Exact bytes of a selected module, not a claim about transitive imports or transpilation. */ +@Serializable +data class PropertyObservationSource( + val module: String, + val sha256: String, +) + +/** Bounded opt-in capture for explicit points inside the original TypeScript callback. */ +@Serializable +data class PropertyObservationRequest( + val points: List, + val sources: List, + val maxInvocations: Int = 64, + val maxPointsPerInvocation: Int = 8, + val maxArrayElements: Int = 16, + val maxBytes: Int = 65_536, +) + +/** A value unavailable to observation remains distinct from JavaScript null or undefined. */ +@Serializable +data class PropertyObservationValue( + val status: ObservationValueStatus, + val value: JsConcreteValue? = null, + val reason: String? = null, +) + +/** One captured point, bound to the declared original assertion. */ +@Serializable +data class PropertyPointEvent( + val pointId: String, + val assertionId: String, + val operandId: String, + val source: PropertySourcePoint, + val callSite: PropertySourcePoint, + val kind: ObservationPointKind, + val occurrence: Int, + val eventOrdinal: Int, + val inputIndex: Int? = null, + val value: PropertyObservationValue, +) + +/** One original callback invocation and its bounded point events. */ +@Serializable +data class PropertyInvocationObservation( + val invocationId: Int, + val parentInvocationId: Int? = null, + val callSite: PropertySourcePoint? = null, + val origin: ObservationOrigin, + val phase: ObservationPhase, + val input: PropertyObservationValue, + val admission: ObservationAdmission, + val outcome: ObservationOutcome, + val points: List, +) + +/** Optional artifact: unknown phase is not independent random evidence. */ +@Serializable +data class PropertyObservationArtifact( + val propertyId: PropertyId, + val runId: String, + val verifiedSources: List, + val buildStatus: ObservationBuildStatus, + val invocations: List, + val droppedInvocations: Int, + val droppedPoints: Int, + val captureTimeMillis: Long, +) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt index 78cde21604..ed8290b3f9 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt @@ -43,7 +43,8 @@ class PropertyManifestTest { assertEquals( """{"propertyId":"integer.defaults","inputs":[""" + """{"name":"value","domain":{"kind":"integer","min":-2147483648,"max":2147483647}}],""" + - """"predicate":{"module":"properties/integer.ts","exportName":"holds","executionKind":"sync"}}""", + """"predicate":{"module":"properties/integer.ts","exportName":"holds","executionKind":"sync"},""" + + """"assertions":[]}""", encoded, ) }