From 2d7f6beba8beee9de56b1a5af5e933bca0fdec80 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 11:15:20 +0300 Subject: [PATCH] Generate native integer neighborhoods from returned inputs --- .../fast-check-adapter/package.json | 2 +- .../fast-check-adapter/src/diagnostics.ts | 2 + .../src/execute-property.ts | 36 +++- .../src/observe-property.ts | 12 +- .../src/returned-input-generation.ts | 113 ++++++++++ .../test/returned-input-generation.test.ts | 148 +++++++++++++ .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 1 + .../fastcheck/FastCheckExecutionProtocol.kt | 2 + .../ReturnedIntegerGenerationTest.kt | 197 ++++++++++++++++++ .../properties/inference/ReturnedIntegers.ts | 11 + .../backend/PropertyBasedTestingBackend.kt | 1 + .../ts/pbt/backend/ReturnedInputGeneration.kt | 23 ++ .../ts/pbt/observation/PropertyObservation.kt | 9 + 13 files changed, 548 insertions(+), 9 deletions(-) create mode 100644 usvm-ts-fast-check/fast-check-adapter/src/returned-input-generation.ts create mode 100644 usvm-ts-fast-check/fast-check-adapter/test/returned-input-generation.test.ts create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ReturnedIntegerGenerationTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/inference/ReturnedIntegers.ts create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ReturnedInputGeneration.kt diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 3fcbf35f61..49005817fb 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package.json +++ b/usvm-ts-fast-check/fast-check-adapter/package.json @@ -9,7 +9,7 @@ "build": "tsc --project tsconfig.json", "pretest": "npm run build", "test": "npm run test:compiled", - "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js" + "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/returned-input-generation.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js dist/test/class-coverage-source.test.js" }, "dependencies": { "@jridgewell/trace-mapping": "0.3.31", 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 fba52cc37a..bfaa9addb0 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts @@ -19,6 +19,8 @@ const entryPoint = (code: string): AdapterDiagnosticDescriptor => ({ export const adapterDiagnostic = { protocolJsonInvalid: invalidRequest('protocol.json.invalid'), protocolRequestInvalid: invalidRequest('protocol.request.invalid'), + returnedGenerationInvalid: invalidRequest('generation.returned.invalid'), + returnedGenerationUnsupported: invalidRequest('generation.returned.unsupported'), protocolSeedInvalid: invalidRequest('protocol.seed.invalid'), protocolReplayPathInvalid: invalidRequest('protocol.replay-path.invalid'), protocolExamplesInvalid: invalidRequest('protocol.examples.invalid'), 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 a8ad7eed20..5838c136c9 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 @@ -22,10 +22,16 @@ import { protocolError, type TaggedJsValue, } from './js-value.js'; -import { buildPropertyArbitrary, PhaseTrackingArbitrary, validateJointGenerator } from './property-arbitrary.js'; +import { PhaseTrackingArbitrary, validateJointGenerator } from './property-arbitrary.js'; +import { + buildReturnedInputGeneration, + validateReturnedInputGeneration, + type ReturnedInputGeneration, +} from './returned-input-generation.js'; import { installObservationHook, ObservationRecorder, + type ReturnedInputMetadata, type ObservationArtifact, type ObservationPointRequest, type ObservationRequest, @@ -76,6 +82,7 @@ export interface FastCheckExecutionRequest { timeoutMillis: number; examples: TaggedJsValue[][]; observationRequest?: ObservationRequest; + returnedInputGeneration?: ReturnedInputGeneration; } export interface FastCheckFailureDetails { @@ -126,13 +133,16 @@ 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 property = buildProperty( + arbitrary, predicate, precondition, contractErrors, recorder, phaseOf, generation.metadataOf, + ); const parameters = buildParameters(request, tracker); const details = await checkProperty(property, parameters, request.replayPath); @@ -158,6 +168,7 @@ function buildProperty( contractErrors: ContractErrorState, recorder: ObservationRecorder | undefined, phaseOf: (values: JsConcreteValue[]) => 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', + metadataOf: (values: JsConcreteValue[]) => ReturnedInputMetadata | undefined, ): fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]> { const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async'; let selectedCheckId: string | undefined; @@ -166,7 +177,9 @@ function buildProperty( return fc.asyncProperty(arbitrary, (values: JsConcreteValue[]): Promise => preserveAsyncContractError( contractErrors, async () => { - const result = await invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)); + const result = await invokePropertyOnce( + values, predicate, precondition, recorder, phaseOf(values), metadataOf(values), + ); if (result === null) fc.pre(false); return result; @@ -179,7 +192,9 @@ function buildProperty( () => { let result: boolean | null; try { - result = invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)) as boolean | null; + result = invokePropertyOnce( + values, predicate, precondition, recorder, phaseOf(values), metadataOf(values), + ) as boolean | null; } catch (error: unknown) { if (isNamedCheckFailure(error)) { selectedCheckId ??= error.checkId; @@ -202,6 +217,7 @@ function invokePropertyOnce( precondition: LoadedEntryPoint | undefined, recorder: ObservationRecorder | undefined, phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', + metadata?: ReturnedInputMetadata, ): boolean | null | Promise { const invocationValues = cloneArguments(values); const invoke = (): boolean | null | Promise => { @@ -252,7 +268,7 @@ function invokePropertyOnce( } }; - return recorder === undefined ? invoke() : recorder.run(values, phase, invoke); + return recorder === undefined ? invoke() : recorder.run(values, phase, invoke, metadata); } function predicateExceptionOutcome(error: unknown): 'false' | 'threw' { @@ -586,6 +602,14 @@ function validateRequest(value: unknown): FastCheckExecutionRequest { validated.observationRequest = validateObservationRequest(request.observationRequest, manifest); } + if (request.returnedInputGeneration !== undefined) { + if (validated.observationRequest === undefined) { + throw protocolError(adapterDiagnostic.returnedGenerationInvalid, + 'Returned generation requires bounded observations for lineage', 'returnedInputGeneration'); + } + validated.returnedInputGeneration = validateReturnedInputGeneration(request.returnedInputGeneration, manifest); + } + return validated; } 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 index d6706080ef..86bbd52ba9 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts @@ -42,11 +42,17 @@ export interface ObservationValue { reason?: string; } +export interface ReturnedInputMetadata { + origin: 'returned-seed' | 'returned-neighborhood'; + returnedInput: { seedId: string; sourceRunId: string; sourceInvocationId: number }; +} + interface InvocationRecord { invocationId: number; parentInvocationId: null; callSite: SourcePoint | null; - origin: 'fast-check'; + origin: 'fast-check' | ReturnedInputMetadata['origin']; + returnedInput?: ReturnedInputMetadata['returnedInput']; phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown'; input: ObservationValue; admission: 'pending' | 'admitted' | 'rejected' | 'threw'; @@ -127,6 +133,7 @@ export class ObservationRecorder { values: unknown[], phase: InvocationRecord['phase'], invocation: () => T, + metadata?: ReturnedInputMetadata, ): T { if (this.artifact.invocations.length >= this.request.maxInvocations) { this.artifact.droppedInvocations = incrementCounter(this.artifact.droppedInvocations); @@ -138,7 +145,8 @@ export class ObservationRecorder { invocationId: this.artifact.invocations.length, parentInvocationId: null, callSite: this.request.points[0]?.callSite ?? null, - origin: 'fast-check', + origin: metadata?.origin ?? 'fast-check', + ...(metadata === undefined ? {} : { returnedInput: metadata.returnedInput }), phase, input: this.snapshot(values), admission: 'pending', diff --git a/usvm-ts-fast-check/fast-check-adapter/src/returned-input-generation.ts b/usvm-ts-fast-check/fast-check-adapter/src/returned-input-generation.ts new file mode 100644 index 0000000000..535e02b842 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/returned-input-generation.ts @@ -0,0 +1,113 @@ +import fc from 'fast-check'; +import { adapterDiagnostic } from './diagnostics.js'; +import type { PropertyManifestWire } from './execute-property.js'; +import { decodeJsValue, type JsConcreteValue, type TaggedJsValue, protocolError } from './js-value.js'; +import type { ReturnedInputMetadata } from './observe-property.js'; +import { buildPropertyArbitrary } from './property-arbitrary.js'; + +export interface ReturnedInputSeed { + id: string; + inputs: TaggedJsValue[]; + sourceRunId: string; + sourceInvocationId: number; +} + +export interface ReturnedInputGeneration { + seeds: ReturnedInputSeed[]; + radius: number; +} + +/** Reject unsupported support instead of replacing a joint or non-integer generator. */ +export function validateReturnedInputGeneration(value: unknown, manifest: PropertyManifestWire): ReturnedInputGeneration { + const request = asRecord(value); + const validRequest = request !== undefined && Array.isArray(request.seeds) + && request.seeds.length >= 1 && request.seeds.length <= MAX_SEEDS + && Number.isInteger(request.radius) && (request.radius as number) >= 1 && (request.radius as number) <= MAX_RADIUS; + if (!validRequest) throw invalid('Expected 1..8 returned seeds and integer radius 1..1024'); + + const integerSupport = manifest.generator === undefined + && manifest.inputs.length >= 1 && manifest.inputs.length <= MAX_INPUTS + && manifest.inputs.every((input) => asRecord(input.domain)?.kind === 'integer'); + if (!integerSupport) { + throw protocolError(adapterDiagnostic.returnedGenerationUnsupported, + 'Returned generation supports only independent integer inputs', 'returnedInputGeneration'); + } + + // Reuse ordinary projection validation before reading the supported integer bounds. + buildPropertyArbitrary(manifest); + const ids = new Set(); + const seeds = (request.seeds as unknown[]).map((value): ReturnedInputSeed => { + const seed = asRecord(value); + const validSeed = seed !== undefined && identifier(seed.id) && identifier(seed.sourceRunId) + && Number.isSafeInteger(seed.sourceInvocationId) && (seed.sourceInvocationId as number) >= 0 + && Array.isArray(seed.inputs) && seed.inputs.length === manifest.inputs.length; + if (!validSeed) throw invalid('A returned seed requires identity, source invocation and the original input arity'); + if (ids.has(seed.id as string)) throw invalid('Returned seed IDs must be unique'); + ids.add(seed.id as string); + + const inputs = seed.inputs as TaggedJsValue[]; + inputs.forEach((tagged, index) => { + const number = decodeJsValue(tagged, `returnedInputGeneration.seeds.inputs[${index}]`); + const domain = asRecord(manifest.inputs[index]?.domain)!; + const inSupport = typeof number === 'number' && Number.isInteger(number) && !Object.is(number, -0) + && number >= (domain.min as number) && number <= (domain.max as number); + if (!inSupport) throw invalid('Returned seed is outside the original integer support'); + }); + + return { id: seed.id as string, inputs, sourceRunId: seed.sourceRunId as string, + sourceInvocationId: seed.sourceInvocationId as number }; + }); + + return { seeds, radius: request.radius as number }; +} + +/** Native oneof/tuple/integer supply generation and shrinking; the original branch retains half the probability. */ +export function buildReturnedInputGeneration(manifest: PropertyManifestWire, request?: ReturnedInputGeneration): { + arbitrary: fc.Arbitrary; + metadataOf(values: JsConcreteValue[]): ReturnedInputMetadata | undefined; +} { + const original = buildPropertyArbitrary(manifest); + const metadata = new WeakMap(); + if (request === undefined) return { arbitrary: original, metadataOf: () => undefined }; + + const returned = request.seeds.map((seed) => { + const numbers = seed.inputs.map((value) => decodeJsValue(value) as number); + const components = numbers.map((number, index) => { + const domain = asRecord(manifest.inputs[index]?.domain)!; + const min = Math.max(domain.min as number, number - request.radius); + const max = Math.min(domain.max as number, number + request.radius); + + return fc.integer({ min, max }); + }); + + return fc.tuple(...components).map((values): JsConcreteValue[] => { + const exactSeed = values.every((number, index) => Object.is(number, numbers[index])); + metadata.set(values, { + origin: exactSeed ? 'returned-seed' : 'returned-neighborhood', + returnedInput: { seedId: seed.id, sourceRunId: seed.sourceRunId, sourceInvocationId: seed.sourceInvocationId }, + }); + + return values; + }); + }); + + return { arbitrary: fc.oneof(original, fc.oneof(...returned)), metadataOf: (values) => metadata.get(values) }; +} + +function identifier(value: unknown): value is string { + return typeof value === 'string' && value.length > 0 && value.length <= MAX_IDENTIFIER_LENGTH; +} + +function asRecord(value: unknown): Record | undefined { + return value !== null && typeof value === 'object' && !Array.isArray(value) + ? value as Record : undefined; +} + +function invalid(message: string): Error { + return protocolError(adapterDiagnostic.returnedGenerationInvalid, message, 'returnedInputGeneration'); +} + +const MAX_SEEDS = 8; +const MAX_INPUTS = 8; +const MAX_RADIUS = 1024; +const MAX_IDENTIFIER_LENGTH = 128; diff --git a/usvm-ts-fast-check/fast-check-adapter/test/returned-input-generation.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/returned-input-generation.test.ts new file mode 100644 index 0000000000..6407215434 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/returned-input-generation.test.ts @@ -0,0 +1,148 @@ +import assert from 'node:assert/strict'; +import test from 'node:test'; +import fc from 'fast-check'; +import { encodeJsValue, ProtocolError, type JsConcreteValue } from '../src/js-value.js'; +import type { PropertyManifestWire } from '../src/execute-property.js'; +import { PhaseTrackingArbitrary } from '../src/property-arbitrary.js'; +import { buildReturnedInputGeneration, validateReturnedInputGeneration } from '../src/returned-input-generation.js'; + +const manifest = (min = 0, max = 100): PropertyManifestWire => ({ + propertyId: 'test.returned', + inputs: [{ name: 'value', domain: { kind: 'integer', min, max } }], + predicate: { module: 'property.ts', exportName: 'holds', executionKind: 'sync' }, +}); +const request = (seed = 8) => ({ + radius: 2, + seeds: [{ id: 'returned-1', inputs: [encodeJsValue(seed)], sourceRunId: 'source-run', sourceInvocationId: 3 }], +}); + +test('ordinary generation is never relabelled by equality with a returned seed', () => { + const property = manifest(0, 0); + const generation = buildReturnedInputGeneration(property, validateReturnedInputGeneration(request(0), property)); + const tracker = new PhaseTrackingArbitrary(generation.arbitrary); + + const values: JsConcreteValue[][] = []; + + fc.assert(fc.property(tracker, (value) => { + assert.equal(tracker.phaseOf(value), 'generation'); + values.push(value); + + return true; + }), { seed: 42, numRuns: 40 }); + + assert.ok(values.every((value) => value[0] === 0)); + assert.ok(values.some((value) => generation.metadataOf(value) === undefined)); + assert.ok(values.some((value) => generation.metadataOf(value)?.origin === 'returned-seed')); +}); + +test('fast-check Value clone reads preserve the selected generation lineage and phase', () => { + const property = manifest(); + const generation = buildReturnedInputGeneration(property, validateReturnedInputGeneration(request(), property)); + const tracker = new PhaseTrackingArbitrary(generation.arbitrary); + const entries: Array> = []; + const generate = tracker.generate.bind(tracker); + tracker.generate = (random, bias) => { + const entry = generate(random, bias); + entries.push(entry); + + return entry; + }; + + fc.sample(tracker, { seed: 42, numRuns: 40 }); + + for (const entry of entries) { + assert.equal(entry.hasToBeCloned, true); + const first = entry.value; + const second = entry.value; + assert.deepEqual(first, second); + assert.deepEqual(generation.metadataOf(first), generation.metadataOf(second)); + assert.equal(tracker.phaseOf(first), 'generation'); + assert.equal(tracker.phaseOf(second), 'generation'); + } + assert.ok(entries.some((entry) => generation.metadataOf(entry.value)?.returnedInput.seedId === 'returned-1')); + assert.ok(entries.some((entry) => generation.metadataOf(entry.value) === undefined)); +}); + +test('native generation and shrinking retain branch lineage and bounded support', () => { + const property = manifest(); + const generation = buildReturnedInputGeneration(property, validateReturnedInputGeneration(request(), property)); + const feedbackOnly = generation.arbitrary.filter((values) => generation.metadataOf(values) !== undefined); + const tracker = new PhaseTrackingArbitrary(feedbackOnly); + const evidence: Array<{ phase: string; origin: string | undefined; input: number }> = []; + + const result = fc.check(fc.property(tracker, (values) => { + const metadata = generation.metadataOf(values); + const input = values[0] as number; + assert.equal(metadata?.returnedInput.seedId, 'returned-1'); + assert.equal(metadata?.returnedInput.sourceRunId, 'source-run'); + assert.equal(metadata?.returnedInput.sourceInvocationId, 3); + assert.ok(input >= 6 && input <= 10); + evidence.push({ phase: tracker.phaseOf(values), origin: metadata?.origin, input }); + + return input < 9; + }), { seed: 42, numRuns: 32 }); + + assert.equal(result.failed, true); + assert.ok(evidence.some((entry) => entry.phase === 'generation' && entry.origin === 'returned-neighborhood')); + assert.ok(evidence.some((entry) => entry.phase === 'shrink' && entry.origin === 'returned-neighborhood')); + assert.ok(evidence.every((entry) => entry.origin !== undefined)); +}); + +test('integer neighborhoods clip at both signed 32-bit support boundaries without overflow', () => { + for (const seed of [-2147483648, 2147483647]) { + const property = manifest(-2147483648, 2147483647); + const generation = buildReturnedInputGeneration(property, + validateReturnedInputGeneration({ ...request(seed), radius: 1024 }, property)); + const feedbackOnly = generation.arbitrary.filter((values) => generation.metadataOf(values) !== undefined); + + const values = fc.sample(feedbackOnly, { seed: 42, numRuns: 32 }); + + assert.ok(values.every(([value]) => typeof value === 'number' + && Number.isInteger(value) && Math.abs(value - seed) <= 1024 + && value >= -2147483648 && value <= 2147483647)); + assert.ok(values.some(([value]) => value !== seed)); + } +}); + +test('unsupported joint and binary64 domains cannot silently replace their original generator', () => { + const number = manifest(); + number.inputs[0]!.domain = { kind: 'number', min: encodeJsValue(0), max: encodeJsValue(100), allowNaN: false }; + const joint = manifest(); + joint.generator = { kind: 'array-index', id: 'joint', arrayInputIndex: 0, indexInputIndex: 1 }; + + const empty = manifest(); + empty.inputs = []; + const oversized = manifest(); + oversized.inputs = Array.from({ length: 9 }, (_, index) => ({ + name: `input${index}`, domain: { kind: 'integer', min: 0, max: 100 }, + })); + + for (const property of [number, joint, empty, oversized]) { + assert.throws(() => validateReturnedInputGeneration(request(), property), + (error: unknown) => error instanceof ProtocolError && error.code === 'generation.returned.unsupported'); + } +}); + +test('seed IDs bounds support arity and radius are validated at the native boundary', () => { + const property = manifest(); + const seed = request().seeds[0]!; + const invalid = [ + { ...request(), radius: 0 }, + { ...request(), radius: 1025 }, + { ...request(), radius: 1.5 }, + { ...request(), seeds: [] }, + { ...request(), seeds: [seed, seed] }, + { ...request(), seeds: [{ ...seed, sourceInvocationId: -1 }] }, + { ...request(), seeds: [{ ...seed, inputs: [] }] }, + request(-1), + request(101), + request(-0), + request(Number.NaN), + request(Number.POSITIVE_INFINITY), + ]; + + for (const value of invalid) { + assert.throws(() => validateReturnedInputGeneration(value, property), + (error: unknown) => error instanceof ProtocolError && error.code === 'generation.returned.invalid'); + } +}); 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 44709e0f73..cda786e03a 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 @@ -56,6 +56,7 @@ class FastCheckBackend( timeoutMillis = configuration.timeoutMillis, examples = configuration.examples, observationRequest = configuration.observationRequest, + returnedInputGeneration = configuration.returnedInputGeneration, coverageRequest = configuration.coverageRequest, ) 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 53246a08fc..111ce6ab8d 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 @@ -5,6 +5,7 @@ import kotlinx.serialization.Serializable import kotlinx.serialization.Transient import org.usvm.ts.pbt.backend.PropertyCoverageRequest import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.ReturnedInputGeneration import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.observation.PropertyObservationRequest @@ -20,6 +21,7 @@ internal data class FastCheckExecutionRequest( val timeoutMillis: Long, val examples: List> = emptyList(), val observationRequest: PropertyObservationRequest? = null, + val returnedInputGeneration: ReturnedInputGeneration? = null, @Transient val coverageRequest: PropertyCoverageRequest? = null, ) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ReturnedIntegerGenerationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ReturnedIntegerGenerationTest.kt new file mode 100644 index 0000000000..5c639ed0c2 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ReturnedIntegerGenerationTest.kt @@ -0,0 +1,197 @@ +package org.usvm.ts.pbt.inference + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.ReturnedInputGeneration +import org.usvm.ts.pbt.backend.ReturnedInputSeed +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +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.PropertyAssertion +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.PropertyOperand +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.observation.ObservationAdmission +import org.usvm.ts.pbt.observation.ObservationOrigin +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.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.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class ReturnedIntegerGenerationTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + private val inputs = listOf(JsConcreteValue.number(500.0), JsConcreteValue.number(900.0)) + private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 16, observationRequest = observations()) + + @Test + fun `native admitted passing input changes fresh generation without changing support or oracle`() { + val property = property() + val confirmed = backend.run(property, configuration.copy(numRuns = 1, examples = listOf(inputs))) + val source = assertNotNull(confirmed.observations) + val invocation = source.invocations.first() + assertEquals(PropertyRunStatus.SUCCESS, confirmed.status) + assertEquals(ObservationAdmission.ADMITTED, invocation.admission) + assertEquals(ObservationOutcome.HOLDS, invocation.outcome) + val returned = ReturnedInputSeed( + id = "admitted-passing-seed", + inputs = inputs, + sourceRunId = source.runId, + sourceInvocationId = invocation.invocationId, + ) + + val control = backend.run(property, configuration) + val run = backend.run( + property, + configuration.copy(returnedInputGeneration = ReturnedInputGeneration(seeds = listOf(returned), radius = 2)), + ) + val artifact = assertNotNull(run.observations) + val ordinary = artifact.invocations.filter { it.origin == ObservationOrigin.FAST_CHECK } + val descendants = artifact.invocations.filter { it.origin == ObservationOrigin.RETURNED_NEIGHBORHOOD } + val feedback = artifact.invocations.filter { it.returnedInput != null } + + assertEquals(PropertyRunStatus.SUCCESS, run.status) + assertTrue(ordinary.isNotEmpty()) + assertTrue(descendants.any { it.admission == ObservationAdmission.ADMITTED }) + assertTrue(artifact.invocations.any { it.admission == ObservationAdmission.REJECTED }) + assertTrue(feedback.all { it.phase == ObservationPhase.GENERATION }) + assertTrue(feedback.all { it.returnedInput?.sourceRunId == source.runId }) + assertTrue(feedback.all { it.returnedInput?.seedId == returned.id }) + assertTrue(feedback.all { it.returnedInput?.sourceInvocationId == invocation.invocationId }) + assertTrue(descendants.all { it.input.value != JsConcreteValue.Array(inputs) }) + assertTrue(artifact.invocations.all { sample -> + val values = (sample.input.value as JsConcreteValue.Array).elements + values.zip(property.inputs).all { (value, input) -> value in input.domain } + }) + assertTrue(feedback.all { sample -> + val values = (sample.input.value as JsConcreteValue.Array).elements + .map { (it as JsConcreteValue.Number).toDouble() } + values[0] in 498.0..502.0 && values[1] in 898.0..902.0 + }) + assertTrue(assertNotNull(control.observations).invocations.all { it.returnedInput == null }) + assertTrue(artifact.invocations.map { it.input } != control.observations?.invocations?.map { it.input }) + assertEquals(0, artifact.droppedInvocations) + assertEquals(0, artifact.droppedPoints) + + val feedbackOnly = artifact.copy(invocations = feedback) + val inference = inferScalarRelations(property, feedbackOnly, listOf(ScalarObservationPair(LEFT, RIGHT))) + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + assertEquals(ScalarRelationStatus.INSUFFICIENT, order.status) + assertTrue(order.distinctGenerationInputs.isEmpty()) + assertTrue(order.evidence.isNotEmpty()) + } + + @Test + fun `returned native shrink and replay preserve correlation and the original failing input`() { + val returned = ReturnedInputSeed( + id = "seed", + inputs = inputs, + sourceRunId = "previous-native-run", + sourceInvocationId = 0, + ) + val configuration = configuration.copy( + numRuns = 64, + returnedInputGeneration = ReturnedInputGeneration(seeds = listOf(returned), radius = 2), + ) + val property = property().copy(predicate = TypeScriptEntryPoint(module = MODULE, exportName = "failsNearby")) + + val failure = backend.run(property, configuration) + val replay = backend.run(property, configuration.copy(seed = failure.seed, replayPath = failure.replayPath)) + + assertEquals(PropertyRunStatus.FAILURE, failure.status) + assertEquals(failure.counterexample, replay.counterexample) + val original = assertNotNull(failure.observations).invocations + assertTrue(original.any { it.phase == ObservationPhase.SHRINK && it.returnedInput?.seedId == returned.id }) + assertTrue(assertNotNull(replay.observations).invocations.all { it.phase == ObservationPhase.REPLAY }) + assertTrue(replay.observations?.invocations?.any { it.returnedInput?.seedId == returned.id } == true) + } + + @Test + fun `unsupported numeric domains and invalid seed support fail explicitly`() { + val returned = ReturnedInputSeed(id = "seed", inputs = inputs, sourceRunId = "previous", sourceInvocationId = 0) + val returnedConfiguration = configuration.copy( + returnedInputGeneration = ReturnedInputGeneration(seeds = listOf(returned)), + ) + val unsupported = property().copy( + inputs = property().inputs.map { it.copy(domain = NumberDomain()) }, + ) + + val error = assertFailsWith { backend.run(unsupported, returnedConfiguration) } + val missingObservations = assertFailsWith { + backend.run(property(), returnedConfiguration.copy(observationRequest = null)) + } + val invalid = assertFailsWith { + backend.run( + property(), + returnedConfiguration.copy( + returnedInputGeneration = ReturnedInputGeneration( + seeds = listOf(returned.copy(inputs = listOf(JsConcreteValue.number(-1.0), inputs[1])))), + ), + ) + } + + assertEquals("generation.returned.unsupported", error.code) + assertEquals("generation.returned.invalid", missingObservations.code) + assertEquals("generation.returned.invalid", invalid.code) + } + + private fun property(): PropertyDefinition = PropertyDefinition( + id = PropertyId("test.returned-integers"), + inputs = listOf( + PropertyInput(name = "left", domain = IntegerDomain(min = 0, max = 1000)), + PropertyInput(name = "right", domain = IntegerDomain(min = 0, max = 1000)), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "holds"), + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "admitted"), + assertions = listOf( + PropertyAssertion( + id = "check", + source = CALL, + testedCall = CALL, + operands = listOf( + PropertyOperand(id = LEFT.operandId, source = LEFT.source), + PropertyOperand(id = RIGHT.operandId, source = RIGHT.source), + ), + ), + ), + ) + + private fun observations(): PropertyObservationRequest { + val hash = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(testResourcesRoot().resolve(MODULE))) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)) + + return PropertyObservationRequest(points = listOf(LEFT, RIGHT), sources = sources) + } + + private companion object { + const val MODULE = "properties/inference/ReturnedIntegers.ts" + val CALL = PropertySourcePoint(module = MODULE, line = 6, column = 5) + val LEFT = PropertyObservationPoint( + id = "left", + assertionId = "check", + operandId = "left", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + val RIGHT = LEFT.copy(id = "right", operandId = "right", inputIndex = 1) + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/inference/ReturnedIntegers.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/ReturnedIntegers.ts new file mode 100644 index 0000000000..b99609b771 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/inference/ReturnedIntegers.ts @@ -0,0 +1,11 @@ +export function admitted(left: number, right: number): boolean { + return left % 2 === 0 && right >= 0; +} + +export function holds(left: number, right: number): boolean { + return left >= 0 && right <= 1000; +} + +export function failsNearby(left: number, right: number): boolean { + return left !== 498; +} 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 566ad6afd4..1496a407b0 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 @@ -29,6 +29,7 @@ data class PropertyRunConfiguration( val examples: List> = emptyList(), val coverageRequest: PropertyCoverageRequest? = null, val observationRequest: PropertyObservationRequest? = null, + val returnedInputGeneration: ReturnedInputGeneration? = null, ) { init { require(numRuns > 0) { "Number of runs must be positive" } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ReturnedInputGeneration.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ReturnedInputGeneration.kt new file mode 100644 index 0000000000..724e9a909b --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ReturnedInputGeneration.kt @@ -0,0 +1,23 @@ +package org.usvm.ts.pbt.backend + +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.model.JsConcreteValue + +/** Caller-selected input and lineage; this DTO does not certify confirmation by the original oracle. */ +@Serializable +data class ReturnedInputSeed( + val id: String, + val inputs: List, + val sourceRunId: String, + val sourceInvocationId: Int, +) + +/** + * Bounded native integer neighborhoods, mixed equally with the unchanged original generator. + * Requires bounded observation capture to retain lineage; seed admission is the caller's responsibility. + */ +@Serializable +data class ReturnedInputGeneration( + val seeds: List, + val radius: Int = 1, +) 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 index 14d782f8e6..063aa8e77f 100644 --- 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 @@ -175,6 +175,14 @@ data class PropertyPointEvent( val value: PropertyObservationValue, ) +/** Caller-owned provenance of the returned seed selected by the native generation branch. */ +@Serializable +data class ReturnedInputLineage( + val seedId: String, + val sourceRunId: String, + val sourceInvocationId: Int, +) + /** One original callback invocation and its bounded point events. */ @Serializable data class PropertyInvocationObservation( @@ -187,6 +195,7 @@ data class PropertyInvocationObservation( val admission: ObservationAdmission, val outcome: ObservationOutcome, val points: List, + val returnedInput: ReturnedInputLineage? = null, ) /** Optional artifact: unknown phase is not independent random evidence. */