diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 953e7ddb10..b22416e09c 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 dist/test/external-witness.test.js" + "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/compiler-local-capture.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 dist/test/external-witness.test.js" }, "dependencies": { "@jridgewell/trace-mapping": "0.3.31", 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 82a9319a5e..4c3c8ff842 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 @@ -7,6 +7,7 @@ import { register } from 'tsx/esm/api'; import { adapterDiagnostic } from './diagnostics.js'; import type { JsConcreteValue } from './js-value.js'; import { ProtocolError, protocolError } from './js-value.js'; +import type { CompilerNumericLocalBinding } from './observe-property.js'; // Each adapter process uses one explicit resolver configuration for all nested imports. let registeredConfig: string | undefined; @@ -60,14 +61,30 @@ export function isNamedCheckFailure(value: unknown): value is NamedCheckFailure return value !== null && typeof value === 'object' && namedCheckFailures.has(value); } -type EntryPointFunction = (...args: JsConcreteValue[]) => unknown; +type EntryPointFunction = (...args: unknown[]) => unknown; + +export interface CompilerNumericLocalCapture { + binding: CompilerNumericLocalBinding; + observe(nodeId: number, localName: string, value: unknown): void; +} export async function loadEntryPoint( reference: TypeScriptEntryPointReference, sourceRoots: string[], referencePath: string, tsconfig?: string, + compilerCapture?: CompilerNumericLocalCapture, ): Promise { + if (compilerCapture !== undefined) { + const binding = compilerCapture.binding; + const validAbi = binding.producer === 'usvm-kotlin-dsl-v1' && binding.abi === 'numeric-local-callback-v1' + && binding.predicateExportName === reference.exportName + && binding.companionExportName === reference.checkResultExportName && reference.executionKind === 'sync'; + if (!validAbi) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, + 'Compiler local callback ABI does not match the selected predicate and companion', `${referencePath}.compilerLocal`); + } + } registerTypeScriptLoader(tsconfig); const modulePath = await resolveModule(reference.module, sourceRoots, referencePath); const moduleNamespace = await importTypeScriptModule(modulePath, referencePath); @@ -101,7 +118,12 @@ export async function loadEntryPoint( return { executionKind: 'sync', invoke: (args) => { - const result = invokeEntryPoint(companion as EntryPointFunction, args); + if (compilerCapture !== undefined && companion.length !== args.length + 1) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, + 'Compiler local companion has an incompatible callback signature', `${referencePath}.compilerLocal`); + } + const companionArgs = compilerCapture === undefined ? args : [...args, compilerCapture.observe]; + const result = invokeEntryPoint(companion as EntryPointFunction, companionArgs); if (result === null || typeof result !== 'object' || isThenable(result)) { throw protocolError(adapterDiagnostic.entryPointResultInvalid, 'A generated companion must return a check outcome', `${referencePath}.result`); @@ -324,7 +346,7 @@ function buildInvocation( }; } -function invokeEntryPoint(entryPoint: EntryPointFunction, args: JsConcreteValue[]): unknown { +function invokeEntryPoint(entryPoint: EntryPointFunction, args: unknown[]): unknown { try { return entryPoint(...args); } catch (error: unknown) { 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 17dbe45e0e..9990a1ded0 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 @@ -30,6 +30,7 @@ import { type ObservationArtifact, type ObservationPointRequest, type ObservationRequest, + type CompilerNumericLocalBinding, } from './observe-property.js'; export interface PropertyManifestInput { @@ -121,7 +122,14 @@ export async function executeProperty(requestValue: unknown): Promise recorder!.captureCompilerLocal(nodeId, localName, value), + }; + const predicate = await loadEntryPoint( + request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig, compilerCapture, + ); const precondition = request.manifest.precondition === undefined ? undefined : await loadEntryPoint(request.manifest.precondition, request.sourceRoots, 'manifest.precondition', request.tsconfig); @@ -791,6 +799,9 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi } else if (point.inputIndex !== undefined) { throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Only argument points may name an input index', path); } + if (point.compilerLocal !== undefined) { + validatedPoint.compilerLocal = validateCompilerLocal(point.compilerLocal, validatedPoint, manifest, sources, path); + } return validatedPoint; }); @@ -802,8 +813,9 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi assertion.id === point.assertionId && samePoint(assertion.testedCall, point.callSite) && assertion.operands.some((operand) => operand.id === point.operandId && samePoint(operand.source, point.source))) ?? false); + const compilerPoints = points.filter((point) => point.compilerLocal !== undefined); if (points.length === 0 || uniquePoints.size !== points.length || uniqueSources.size !== sources.length - || !allSourcesPresent || !allPointsBound) { + || !allSourcesPresent || !allPointsBound || compilerPoints.length > 1) { throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Observation points must bind to declared assertion operands and selected source hashes', 'observationRequest'); } @@ -818,6 +830,39 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi }; } +function validateCompilerLocal( + value: unknown, point: ObservationPointRequest, manifest: PropertyManifestWire, + sources: Array<{ module: string; sha256: string }>, path: string, +): CompilerNumericLocalBinding { + const binding = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, + 'Compiler local binding must be an object', `${path}.compilerLocal`); + const predicateAssignment = validateSourcePoint(binding.predicateAssignment, `${path}.compilerLocal.predicateAssignment`); + const companionAssignment = validateSourcePoint(binding.companionAssignment, `${path}.compilerLocal.companionAssignment`); + const source = sources.find((source) => source.module === manifest.predicate.module); + const valid = binding.producer === 'usvm-kotlin-dsl-v1' && binding.abi === 'numeric-local-callback-v1' + && binding.programId === manifest.propertyId && Number.isInteger(binding.nodeId) && (binding.nodeId as number) >= 0 + && typeof binding.localName === 'string' && /^[A-Za-z_$][A-Za-z0-9_$]*$/.test(binding.localName) + && binding.predicateExportName === manifest.predicate.exportName + && binding.companionExportName === manifest.predicate.checkResultExportName + && manifest.predicate.checkResultExportName !== undefined && manifest.predicate.executionKind === 'sync' + && predicateAssignment.module === manifest.predicate.module && companionAssignment.module === manifest.predicate.module + && point.source.module === manifest.predicate.module && point.callSite.module === manifest.predicate.module + && !samePoint(predicateAssignment, companionAssignment) + && typeof binding.sourceSha256 === 'string' && /^[0-9a-f]{64}$/.test(binding.sourceSha256) + && source?.sha256 === binding.sourceSha256 && binding.occurrence === 0 && point.kind === 'return'; + if (!valid) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, + 'Compiler local identity, callback ABI or selected source does not match', `${path}.compilerLocal`); + } + + return { + producer: binding.producer as string, abi: binding.abi as string, programId: binding.programId as string, + nodeId: binding.nodeId as number, localName: binding.localName as string, + predicateExportName: binding.predicateExportName as string, companionExportName: binding.companionExportName as string, + predicateAssignment, companionAssignment, sourceSha256: binding.sourceSha256 as string, occurrence: 0, + }; +} + function samePoint(left: PropertySourcePointWire | undefined, right: PropertySourcePointWire): boolean { return left !== undefined && left.module === right.module && left.line === right.line && left.column === right.column; 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..8bf19f952f 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 @@ -14,6 +14,22 @@ export interface ObservationPointRequest { callSite: SourcePoint; kind: 'entry-argument' | 'argument' | 'return' | 'intermediate' | 'pre' | 'post'; inputIndex?: number; + compilerLocal?: CompilerNumericLocalBinding; +} + +/** Authority comes from the retained compiler program, not these source coordinates alone. */ +export interface CompilerNumericLocalBinding { + producer: string; + abi: string; + programId: string; + nodeId: number; + localName: string; + predicateExportName: string; + companionExportName: string; + predicateAssignment: SourcePoint; + companionAssignment: SourcePoint; + sourceSha256: string; + occurrence: number; } export interface SourcePoint { @@ -123,6 +139,22 @@ export class ObservationRecorder { return this.artifact; } + get compilerLocalBinding(): CompilerNumericLocalBinding | undefined { + return this.request.points.find((point) => point.compilerLocal !== undefined)?.compilerLocal; + } + + captureCompilerLocal(nodeId: number, localName: string, value: unknown): void { + const context = contexts.getStore(); + const point = this.request.points.find((point) => point.compilerLocal !== undefined); + if (context?.recorder !== this || point === undefined) return; + + const binding = point.compilerLocal!; + const identityMatches = nodeId === binding.nodeId && localName === binding.localName; + const reason = !identityMatches ? 'compiler-local-identity-mismatch' + : typeof value !== 'number' ? 'compiler-local-numeric-required' : undefined; + this.capturePoint(context.invocation, point, value, reason); + } + run( values: unknown[], phase: InvocationRecord['phase'], @@ -172,8 +204,8 @@ export class ObservationRecorder { point(record: InvocationRecord, pointId: string, value: unknown): void { const point = this.pointsById.get(pointId); - // Entry snapshots belong to the adapter; user callbacks cannot replace or repeat them. - if (point?.kind === 'entry-argument') return; + // Adapter entry snapshots and compiler callbacks own these points; public hooks cannot replace them. + if (point?.kind === 'entry-argument' || point?.compilerLocal !== undefined) return; if (point === undefined) { this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); @@ -183,7 +215,7 @@ export class ObservationRecorder { this.capturePoint(record, point, value); } - private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown): void { + private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown, unsupportedReason?: string): void { if (record.points.length >= this.request.maxPointsPerInvocation) { this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); @@ -198,9 +230,10 @@ export class ObservationRecorder { callSite: point.callSite, kind: point.kind, ...(point.inputIndex === undefined ? {} : { inputIndex: point.inputIndex }), + ...(point.compilerLocal === undefined ? {} : { compilerLocal: point.compilerLocal }), occurrence: record.points.filter((event) => event.pointId === point.id).length, eventOrdinal: record.points.length, - value: this.snapshot(value), + value: unsupportedReason === undefined ? this.snapshot(value) : { status: 'unsupported', reason: unsupportedReason }, }); if (this.reservedArtifactBytes() > this.request.maxBytes) { record.points.pop(); diff --git a/usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts new file mode 100644 index 0000000000..6d8d9d2f6d --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts @@ -0,0 +1,188 @@ +import assert from 'node:assert/strict'; +import { createHash } from 'node:crypto'; +import { mkdtemp, realpath, rm, writeFile } from 'node:fs/promises'; +import { tmpdir } from 'node:os'; +import path from 'node:path'; +import test from 'node:test'; +import { executeProperty } from '../src/execute-property.js'; +import { encodeJsValue, ProtocolError } from '../src/js-value.js'; +import type { CompilerNumericLocalBinding, ObservationPointRequest } from '../src/observe-property.js'; + +async function fixture( + run: (request: ReturnType, root: string) => Promise, + callback = "observer?.(4, 'result', result);", + withCallbackParameter = true, +): Promise { + const root = await realpath(await mkdtemp(path.join(tmpdir(), 'pbt-compiler-local-'))); + const parameter = withCallbackParameter ? ', observer?: (node: number, local: string, value: unknown) => void' : ''; + const source = ` + let calls = 0; + function underlying(value: number): number { + calls += 1; + const hook = (globalThis as any)[Symbol.for('org.usvm.ts.pbt.observe')]; + hook?.('result', 999); + return value; + } + export function predicate(value: number): boolean { + calls = 0; + const result = underlying(value); + return (result === value || (result !== result && value !== value)) && calls === 1; + } + export function companion(value: number${parameter}) { + calls = 0; + const result = underlying(value); + ${callback} + return { passed: (result === value || (result !== result && value !== value)) && calls === 1, + checkId: '', actual: true, expected: true }; + } + `; + await writeFile(path.join(root, 'generated.ts'), source); + const hash = createHash('sha256').update(source).digest('hex'); + try { + await run(buildRequest(root, hash), root); + } finally { + await rm(root, { recursive: true, force: true }); + } +} + +function buildRequest(root: string, hash: string) { + const callSite = { module: 'generated.ts', line: 10, column: 22 }; + const source = { module: 'generated.ts', line: 11, column: 14 }; + const binding: CompilerNumericLocalBinding = { + producer: 'usvm-kotlin-dsl-v1', abi: 'numeric-local-callback-v1', programId: 'compiler.local', + nodeId: 4, localName: 'result', predicateExportName: 'predicate', companionExportName: 'companion', + predicateAssignment: { module: 'generated.ts', line: 10, column: 7 }, + companionAssignment: { module: 'generated.ts', line: 15, column: 7 }, + sourceSha256: hash, occurrence: 0, + }; + const result: ObservationPointRequest = { + id: 'result', assertionId: 'identity', operandId: 'result', source, callSite, kind: 'return', compilerLocal: binding, + }; + const input: ObservationPointRequest = { + id: 'input', assertionId: 'identity', operandId: 'input', source, callSite, kind: 'entry-argument', inputIndex: 0, + }; + + return { + manifest: { + propertyId: 'compiler.local', + predicate: { module: 'generated.ts', exportName: 'predicate', executionKind: 'sync', checkResultExportName: 'companion' }, + inputs: [{ name: 'value', domain: { kind: 'integer', min: 1, max: 10 } }], + assertions: [{ id: 'identity', source, testedCall: callSite, operands: [{ id: 'result', source }, { id: 'input', source }] }], + }, + sourceRoots: [root], examples: [[encodeJsValue(7)]], seed: 42, numRuns: 2, timeoutMillis: 5000, + observationRequest: { + points: [result, input], sources: [{ module: 'generated.ts', sha256: hash }], + maxInvocations: 8, maxPointsPerInvocation: 4, maxArrayElements: 2, maxBytes: 65_536, + }, + }; +} + +test('declared compiler callback captures the computed result and public hooks cannot replace it', async () => { + await fixture(async (request) => { + const result = (await executeProperty(request)).result; + + assert.equal(result.status, 'success'); + assert.equal(result.observations?.buildStatus, 'unverified'); + for (const invocation of result.observations!.invocations) { + const value = invocation.points.filter((event) => event.pointId === 'result'); + const input = invocation.points.find((event) => event.pointId === 'input'); + + assert.equal(value.length, 1); + assert.deepEqual(value[0]?.value.value, input?.value.value); + assert.deepEqual(value[0]?.compilerLocal, request.observationRequest.points[0]?.compilerLocal); + assert.equal(value[0]?.occurrence, 0); + assert.ok(value[0]!.eventOrdinal > input!.eventOrdinal); + } + }); +}); + +test('missing callback remains missing even when original code invokes the public hook', async () => { + await fixture(async (request) => { + const result = (await executeProperty(request)).result; + + assert.equal(result.status, 'success'); + assert.ok(result.observations!.invocations.every((invocation) => + invocation.points.every((event) => event.pointId !== 'result'))); + }, ''); +}); + +test('compiler callback snapshots preserve NaN signed zero and infinities', async () => { + await fixture(async (request) => { + const values = [Number.NaN, -0, Number.NEGATIVE_INFINITY, Number.POSITIVE_INFINITY]; + const selected = { ...request, manifest: { ...request.manifest, inputs: [{ name: 'value', domain: { + kind: 'number', min: { value: 'negative-infinity' }, max: { value: 'positive-infinity' }, allowNaN: true, + } }] }, examples: values.map((value) => [encodeJsValue(value)]), numRuns: values.length + 2 }; + + const result = (await executeProperty(selected)).result; + const explicit = result.observations!.invocations.filter((invocation) => invocation.phase === 'explicit'); + + assert.equal(result.status, 'success'); + assert.equal(explicit.length, values.length); + assert.deepEqual(explicit.map((invocation) => invocation.points.find((event) => event.pointId === 'result')?.value.value), + values.map(encodeJsValue)); + }); +}); + +test('wrong compiler receipt and unsupported numeric value preserve the original oracle and record unavailable points', async () => { + const cases = [ + ["observer?.(5, 'result', result);", 'compiler-local-identity-mismatch'], + ["observer?.(4, 'other', result);", 'compiler-local-identity-mismatch'], + ["observer?.(4, 'result', 'unsupported');", 'compiler-local-numeric-required'], + ]; + for (const [callback, reason] of cases) { + await fixture(async (request) => { + const result = (await executeProperty(request)).result; + const events = result.observations!.invocations.flatMap((invocation) => + invocation.points.filter((event) => event.pointId === 'result')); + + assert.equal(result.status, 'success'); + assert.ok(events.length > 0); + assert.ok(events.every((event) => event.value.status === 'unsupported' && event.value.reason === reason)); + }, callback); + } +}); + +test('repeated compiler callback receipts keep occurrence identity', async () => { + await fixture(async (request) => { + const result = (await executeProperty(request)).result; + const events = result.observations!.invocations[0]!.points.filter((event) => event.pointId === 'result'); + + assert.equal(result.status, 'success'); + assert.deepEqual(events.map((event) => event.occurrence), [0, 1]); + }, "observer?.(4, 'result', result); observer?.(4, 'result', result);"); +}); + +test('compiler declaration validates ABI producer program exports source occurrence and kind', async () => { + await fixture(async (request) => { + const point = request.observationRequest.points[0]!; + const binding = point.compilerLocal!; + const invalidBindings = [ + { ...binding, producer: 'arbitrary-source' }, { ...binding, abi: 'other-callback' }, + { ...binding, programId: 'other-property' }, { ...binding, predicateExportName: 'other' }, + { ...binding, companionExportName: 'other' }, { ...binding, sourceSha256: '0'.repeat(64) }, + { ...binding, occurrence: 1 }, { ...binding, predicateAssignment: binding.companionAssignment }, + ]; + const invalidPoints: ObservationPointRequest[] = [ + ...invalidBindings.map((compilerLocal) => ({ ...point, compilerLocal })), + { ...point, kind: 'intermediate' }, + ]; + for (const selected of invalidPoints) { + await assert.rejects(executeProperty({ ...request, observationRequest: { + ...request.observationRequest, points: [selected, request.observationRequest.points[1]], + } }), (error: unknown) => error instanceof ProtocolError && error.code === 'protocol.request.invalid'); + } + }); +}); + +test('changed selected source and incompatible companion signature cannot supply capture', async () => { + await fixture(async (request, root) => { + await writeFile(path.join(root, 'generated.ts'), 'export function predicate() { return true; }'); + + await assert.rejects(executeProperty(request), (error: unknown) => + error instanceof ProtocolError && error.code === 'entrypoint.source-hash.mismatch'); + }); + await fixture(async (request) => { + await assert.rejects(executeProperty(request), (error: unknown) => + error instanceof ProtocolError && error.code === 'protocol.request.invalid'); + }, '', false); +}); 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 091e90f890..e7a4bcc1eb 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,10 +11,12 @@ import org.usvm.ts.pbt.backend.WitnessEvidenceDelta import org.usvm.ts.pbt.backend.WitnessReplayConfiguration import org.usvm.ts.pbt.backend.WitnessReplayDeadline import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.ExecutionKind import org.usvm.ts.pbt.model.JsConcreteValue 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.CompilerNumericLocalBinding import org.usvm.ts.pbt.observation.ObservationPointKind import org.usvm.ts.pbt.observation.PropertyObservationRequest import org.usvm.ts.pbt.validation.requireValid @@ -128,9 +130,28 @@ class FastCheckBackend( } } val hashesValid = request.sources.all { source -> source.sha256.matches(SHA256_REGEX) } + val compilerPoints = request.points.filter { it.compilerLocal != null } + val compilerLocalsValid = compilerPoints.size <= 1 && compilerPoints.all { point -> + val binding = requireNotNull(point.compilerLocal) + val module = property.predicate.module + val predicate = binding.predicateAssignment + val companion = binding.companionAssignment + + binding.producer == CompilerNumericLocalBinding.PRODUCER && + binding.abi == CompilerNumericLocalBinding.ABI && binding.programId == property.id.value && + binding.nodeId >= 0 && binding.localName.matches(Regex("[A-Za-z_$][A-Za-z0-9_$]*")) && + binding.predicateExportName == property.predicate.exportName && + binding.companionExportName == property.predicate.checkResultExportName && + property.predicate.executionKind == ExecutionKind.SYNC && + predicate.module == module && companion.module == module && predicate != companion && + predicate.line > 0 && predicate.column > 0 && companion.line > 0 && companion.column > 0 && + point.source.module == module && point.callSite.module == module && + binding.sourceSha256 == sourceByModule[module]?.sha256 && + binding.occurrence == 0 && point.kind == ObservationPointKind.RETURN + } val validRequest = validLimits && request.points.isNotEmpty() && allSourcesPresent && - allPointsBound && allInputIndexesValid && hashesValid + allPointsBound && allInputIndexesValid && hashesValid && compilerLocalsValid if (!validRequest) { throw invalidRequest( diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCaptureTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCaptureTest.kt new file mode 100644 index 0000000000..87d93ecef2 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCaptureTest.kt @@ -0,0 +1,177 @@ +package org.usvm.ts.pbt.dsl + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +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.inference.ScalarObservationPair +import org.usvm.ts.pbt.inference.ScalarRelationLimitation +import org.usvm.ts.pbt.inference.ScalarRelationStatus +import org.usvm.ts.pbt.inference.ScalarRelationTemplate +import org.usvm.ts.pbt.inference.inferScalarRelations +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.ObservationValueStatus +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class DslNumericLocalCaptureTest { + @TempDir + lateinit var root: Path + + @Test + fun `real frontend retains original predicate and companion shared assignments`() { + val compiled = compile() + val binding = assertNotNull(compiled.numericLocalCapture).binding + + val file = loadEtsFileAutoConvert(root.resolve("generated.ts"), provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + val mapping = PropertyEtsMapper(scene, sourceRoots = listOf(root)).map(compiled.definition.toManifest()) + val predicate = mapping.predicate.targets.single().method + val owner = assertNotNull(predicate.enclosingClass) + val companion = owner.methods.single { it.name == binding.companionExportName } + + assertEquals(EtsMappingStatus.EXACT, mapping.predicate.status) + listOf(predicate, companion).forEach { method -> + val selected = method.cfg.instructions.filterIsInstance().filter { assignment -> + (assignment.lhv as? EtsLocal)?.name == binding.localName + } + + assertEquals(1, selected.size) + } + } + + @Test + fun `native generation captures the compiler local and entry input for shared inference`() { + val compiled = compile() + val capture = assertNotNull(compiled.numericLocalCapture) + + val result = FastCheckBackend(sourceRoots = listOf(root)).run( + compiled.definition, + configuration(capture), + ) + val observations = assertNotNull(result.observations) + val inference = inferScalarRelations( + compiled.definition, + observations, + listOf(ScalarObservationPair(capture.result, capture.input)), + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.status) + assertEquals(ObservationBuildStatus.UNVERIFIED, observations.buildStatus) + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + assertEquals(ScalarRelationStatus.SAMPLED, equality.status) + assertTrue(equality.distinctGenerationInputs.size >= 2) + observations.invocations.forEach { invocation -> + val value = invocation.points.single { it.pointId == capture.result.id } + val input = invocation.points.single { it.pointId == capture.input.id } + + assertEquals(capture.binding, value.compilerLocal) + assertEquals(ObservationValueStatus.CAPTURED, value.value.status) + assertEquals(input.value.value, value.value.value) + assertEquals(0, value.occurrence) + assertTrue(input.eventOrdinal < value.eventOrdinal) + } + } + + @Test + fun `ordinary predicate and diagnostic companion reuse one computed value across checks`() { + val compiled = compile() + val ordinary = compiled.definition.copy( + predicate = compiled.definition.predicate.copy(checkResultExportName = null), + ) + val backend = FastCheckBackend(sourceRoots = listOf(root)) + + val diagnosticResult = backend.run( + compiled.definition, + configuration(assertNotNull(compiled.numericLocalCapture)) + ) + val ordinaryResult = backend.run(ordinary, PropertyRunConfiguration(seed = 42, numRuns = 8)) + + assertEquals(PropertyRunStatus.SUCCESS, diagnosticResult.status) + assertEquals(PropertyRunStatus.SUCCESS, ordinaryResult.status) + } + + @Test + fun `repeated nested and mismatched compiler receipts cannot supply sampled guidance`() { + val compiled = compile() + val capture = assertNotNull(compiled.numericLocalCapture) + val run = FastCheckBackend(sourceRoots = listOf(root)).run(compiled.definition, configuration(capture)) + val original = assertNotNull(run.observations) + val pairs = listOf(ScalarObservationPair(capture.result, capture.input)) + val repeatedInvocations = original.invocations.map { invocation -> + val value = invocation.points.single { it.pointId == capture.result.id } + + invocation.copy(points = invocation.points + value.copy(occurrence = 1)) + } + val nestedInvocations = original.invocations.map { it.copy(parentInvocationId = 1) } + val wrongNodeInvocations = original.invocations.map { invocation -> + val points = invocation.points.map { event -> + if (event.compilerLocal == null) { + event + } else { + event.copy(compilerLocal = capture.binding.copy(nodeId = capture.binding.nodeId + 1)) + } + } + + invocation.copy(points = points) + } + + val cases = listOf( + original.copy(invocations = repeatedInvocations) to ScalarRelationLimitation.REPEATED_POINT, + original.copy(invocations = nestedInvocations) to ScalarRelationLimitation.UNSUPPORTED_CONTEXT, + original.copy(invocations = wrongNodeInvocations) to ScalarRelationLimitation.POINT_IDENTITY_MISMATCH, + ) + cases.forEach { (observations, limitation) -> + val inference = inferScalarRelations(compiled.definition, observations, pairs) + + assertTrue(inference.relations.all { it.status == ScalarRelationStatus.UNSUPPORTED }) + assertTrue(inference.relations.all { limitation in it.limitations }) + } + } + + private fun configuration(capture: CompiledDslNumericLocalCapture): PropertyRunConfiguration = + PropertyRunConfiguration(seed = 42, numRuns = 8, observationRequest = capture.observationRequest()) + + private fun compile(): CompiledDslProperty { + val source = """ + let calls = 0; + export function reset(value: number): number { calls = 0; return value; } + export function counted(value: number): number { calls += 1; return value; } + export function count(value: number): number { return calls; } + """.trimIndent() + Files.writeString(root.resolve("calls.ts"), source) + val program = defineProperty(id = "dsl.local-capture") { + val reset = function<(Double) -> Double>(module = "calls.ts", exportName = "reset") + val counted = function<(Double) -> Double>(module = "calls.ts", exportName = "counted") + val count = function<(Double) -> Double>(module = "calls.ts", exportName = "count") + val input by int(min = 1, max = 4) + val initial by value(reset(input)) + val result by value(counted(initial)) + + check(name = "bound") { result lessOrEqual input } + check(name = "identity") { result equalTo input } + check(name = "once") { count(input) equalTo 1 } + } + val compiled = PropertyTypeScriptCompiler().compile( + program = program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + Files.writeString(root.resolve("generated.ts"), compiled.typeScript) + + return compiled + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt new file mode 100644 index 0000000000..0ef91f053a --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt @@ -0,0 +1,109 @@ +package org.usvm.ts.pbt.dsl + +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.observation.CompilerNumericLocalBinding +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 java.security.MessageDigest + +/** Opt-in result of one numeric direct call, compared with one original input by a named check. */ +data class DslNumericLocalCapture(val localName: String, val checkName: String) + +/** Retains compiler-owned point identity and both selected original assertion operands without running the property. */ +data class CompiledDslNumericLocalCapture( + val binding: CompilerNumericLocalBinding, + val result: PropertyObservationPoint, + val input: PropertyObservationPoint, +) { + fun observationRequest(): PropertyObservationRequest { + val source = PropertyObservationSource( + module = binding.predicateAssignment.module, + sha256 = binding.sourceSha256 + ) + + return PropertyObservationRequest(points = listOf(result, input), sources = listOf(source)) + } +} + +internal data class SelectedDslNumericLocalCapture( + val local: PropertyLocal, + val check: NamedPropertyCheck, + val input: PropertyExpressionTerm.Input, + val resultOperandIndex: Int, + val inputOperandIndex: Int, +) + +internal fun DslProperty.selectNumericLocalCapture(request: DslNumericLocalCapture): SelectedDslNumericLocalCapture { + val local = locals.singleOrNull { it.name == request.localName } + requireNotNull(local) { "Unknown shared local: ${request.localName}" } + require(local.expression.type == PropertyValueType.NUMBER && local.expression.term is PropertyExpressionTerm.Call) { + "Numeric local capture supports only a direct function call" + } + val check = checks.singleOrNull { it.name == request.checkName } + requireNotNull(check) { "Unknown named check: ${request.checkName}" } + val comparison = check.expression.term as? PropertyExpressionTerm.Operation + require(comparison != null && comparison.operator in setOf("===", "<=")) { + "Numeric local capture requires a direct === or <= named check" + } + val localOperands = comparison.arguments.withIndex().filter { (_, node) -> + (node.term as? PropertyExpressionTerm.Local)?.name == local.name + } + require(localOperands.size == 1) { "The selected local must be exactly one direct check operand" } + val resultIndex = localOperands.single().index + val inputIndex = 1 - resultIndex + val inputNode = comparison.arguments[inputIndex] + val input = inputNode.term as? PropertyExpressionTerm.Input + require(input != null && inputNode.type == PropertyValueType.NUMBER) { + "The other check operand must be one original numeric input" + } + + return SelectedDslNumericLocalCapture(local, check, input, resultIndex, inputIndex) +} + +internal fun SelectedDslNumericLocalCapture.compileCapture( + definition: PropertyDefinition, + typeScript: String, + predicateAssignment: PropertySourcePoint, + companionAssignment: PropertySourcePoint, +): CompiledDslNumericLocalCapture { + val hash = MessageDigest.getInstance("SHA-256").digest(typeScript.toByteArray()) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val binding = CompilerNumericLocalBinding( + producer = CompilerNumericLocalBinding.PRODUCER, + abi = CompilerNumericLocalBinding.ABI, + programId = definition.id.value, + nodeId = local.expression.id, + localName = local.name, + predicateExportName = definition.predicate.exportName, + companionExportName = requireNotNull(definition.predicate.checkResultExportName), + predicateAssignment = predicateAssignment, + companionAssignment = companionAssignment, + sourceSha256 = hash, + occurrence = 0, + ) + val assertion = definition.assertions.single { it.id == check.name } + val callSite = requireNotNull(assertion.testedCall) + val result = PropertyObservationPoint( + id = "dsl-result:${local.name}:${check.name}", + assertionId = assertion.id, + operandId = "operand-$resultOperandIndex", + source = assertion.operands[resultOperandIndex].source, + callSite = callSite, + kind = ObservationPointKind.RETURN, + compilerLocal = binding, + ) + val inputPoint = PropertyObservationPoint( + id = "dsl-input:${input.name}:${check.name}", + assertionId = assertion.id, + operandId = "operand-$inputOperandIndex", + source = assertion.operands[inputOperandIndex].source, + callSite = callSite, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = definition.inputs.indexOfFirst { it.name == input.name }, + ) + + return CompiledDslNumericLocalCapture(binding, result, inputPoint) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt index 10820352af..eae82c7bc8 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt @@ -19,6 +19,7 @@ data class CompiledDslProperty( val definition: PropertyDefinition, val typeScript: String, val expressionLocations: Map>, + val numericLocalCapture: CompiledDslNumericLocalCapture? = null, ) /** One expression occurrence in generated TypeScript; columns are one-based UTF-16 and end-exclusive. */ @@ -34,7 +35,16 @@ class PropertyTypeScriptCompiler { generatedModule: String, resolveModule: (String) -> String, ): CompiledDslProperty { - val emitter = PropertyEmitter(program, generatedModule, resolveModule) + return compile(program, generatedModule, resolveModule, numericLocalCapture = null) + } + + fun compile( + program: DslProperty, + generatedModule: String, + resolveModule: (String) -> String, + numericLocalCapture: DslNumericLocalCapture?, + ): CompiledDslProperty { + val emitter = PropertyEmitter(program, generatedModule, resolveModule, numericLocalCapture) return emitter.compile() } } @@ -43,12 +53,17 @@ private class PropertyEmitter( private val program: DslProperty, private val module: String, private val resolveModule: (String) -> String, + numericLocalCapture: DslNumericLocalCapture?, ) { + private val capture = numericLocalCapture?.let { program.selectNumericLocalCapture(it) } private val source = StringBuilder() private val functions = linkedMapOf() private val expressionLocations = mutableMapOf>() private val assertions = mutableListOf() private var line = 1 + private var predicateAssignment: PropertySourcePoint? = null + private var companionAssignment: PropertySourcePoint? = null + private var capturedCall: PropertySourcePoint? = null fun compile(): CompiledDslProperty { allExpressions().forEach(::collectFunctions) @@ -84,7 +99,15 @@ private class PropertyEmitter( assertions = assertions, ) val locations = expressionLocations.mapValues { (_, ranges) -> ranges.toList() } - return CompiledDslProperty(program, definition, source.toString(), locations) + val typeScript = source.toString() + val localCapture = capture?.compileCapture( + definition, + typeScript, + predicateAssignment = requireNotNull(predicateAssignment), + companionAssignment = requireNotNull(companionAssignment), + ) + + return CompiledDslProperty(program, definition, typeScript, locations, localCapture) } private fun emitPredicate(parameters: String, diagnostic: Boolean) { @@ -94,14 +117,34 @@ private class PropertyEmitter( } else { "boolean" } - appendLine("export function $name($parameters): $resultType {") - program.locals.forEach { local -> appendValue(local.name, local.expression) } + val callback = if (diagnostic && capture != null) { + ", __usvmObserve?: (nodeId: number, localName: string, value: number) => void" + } else { + "" + } + appendLine("export function $name($parameters$callback): $resultType {") + program.locals.forEach { local -> emitLocal(local, diagnostic) } program.checks.forEachIndexed { index, check -> emitCheck(check, index, diagnostic) } val success = if (diagnostic) "{ passed: true, checkId: '', actual: true, expected: true }" else "true" appendLine(" return $success;") appendLine("}") } + private fun emitLocal(local: PropertyLocal, diagnostic: Boolean) { + val assignment = PropertySourcePoint(module = module, line = line, column = " ".length + 1) + appendValue(local.name, local.expression) + if (local != capture?.local) return + + if (diagnostic) { + companionAssignment = assignment + val arguments = "${local.expression.id}, ${quote(local.name)}, ${local.name}" + appendLine(" if (__usvmObserve !== undefined) __usvmObserve($arguments);") + } else { + predicateAssignment = assignment + capturedCall = expressionLocations.getValue(local.expression.id).last().start + } + } + private fun emitCheck(check: NamedPropertyCheck, index: Int, diagnostic: Boolean) { val indentation = if (diagnostic) " " else " " if (diagnostic) appendLine(" try {") @@ -125,7 +168,14 @@ private class PropertyEmitter( appendLine("${indentation}const $expected = true;") condition = actual val location = expressionLocations.getValue(check.expression.id).last().start - operands = listOf(PropertyOperand(id = "condition", source = location)) + operands = if (check.name == capture?.check?.name) { + (term as PropertyExpressionTerm.Operation).arguments.mapIndexed { operandIndex, node -> + val operandLocation = expressionLocations.getValue(node.id).last().start + PropertyOperand(id = "operand-$operandIndex", source = operandLocation) + } + } else { + listOf(PropertyOperand(id = "condition", source = location)) + } } val failure = if (diagnostic) { "{ passed: false, checkId: ${quote(check.name)}, actual: $actual, expected: $expected }" @@ -136,7 +186,13 @@ private class PropertyEmitter( record(check.expression, column = indentation.length + "if (!(".length + 1, length = condition.length) appendLine("${indentation}if (!($condition)) return $failure;") if (!diagnostic) { - assertions += PropertyAssertion(id = check.name, source = point, operands = operands) + val testedCall = capturedCall.takeIf { check.name == capture?.check?.name } + assertions += PropertyAssertion( + id = check.name, + source = point, + testedCall = testedCall, + operands = operands, + ) } else { appendLine(" } catch (__usvmError) {") val identity = quote(check.name) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt index 91a3b3a03c..588c4e499c 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt @@ -186,7 +186,8 @@ private fun ScalarObservationPair.isAssertionPair(property: PropertyDefinition): internal fun PropertyPointEvent.matches(point: PropertyObservationPoint): Boolean = assertionId == point.assertionId && operandId == point.operandId && source == point.source && - callSite == point.callSite && kind == point.kind && inputIndex == point.inputIndex && occurrence == 0 + callSite == point.callSite && kind == point.kind && inputIndex == point.inputIndex && occurrence == 0 && + compilerLocal == point.compilerLocal private fun PropertyPointEvent.isNumber(): Boolean { val number = value.value as? JsConcreteValue.Number ?: return false diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/CompilerNumericLocalBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/CompilerNumericLocalBinding.kt new file mode 100644 index 0000000000..5aedba706d --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/observation/CompilerNumericLocalBinding.kt @@ -0,0 +1,25 @@ +package org.usvm.ts.pbt.observation + +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.model.PropertySourcePoint + +/** Compiler-owned point transport; selected source bytes do not verify its executable build or imports. */ +@Serializable +data class CompilerNumericLocalBinding( + val producer: String, + val abi: String, + val programId: String, + val nodeId: Int, + val localName: String, + val predicateExportName: String, + val companionExportName: String, + val predicateAssignment: PropertySourcePoint, + val companionAssignment: PropertySourcePoint, + val sourceSha256: String, + val occurrence: Int, +) { + companion object { + const val PRODUCER = "usvm-kotlin-dsl-v1" + const val ABI = "numeric-local-callback-v1" + } +} 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..62d4febbf7 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 @@ -16,6 +16,7 @@ data class PropertyObservationPoint( val callSite: PropertySourcePoint, val kind: ObservationPointKind, val inputIndex: Int? = null, + val compilerLocal: CompilerNumericLocalBinding? = null, ) /** Location and role of a recorded operand value. */ @@ -173,6 +174,7 @@ data class PropertyPointEvent( val eventOrdinal: Int, val inputIndex: Int? = null, val value: PropertyObservationValue, + val compilerLocal: CompilerNumericLocalBinding? = null, ) /** One original callback invocation and its bounded point events. */ diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt new file mode 100644 index 0000000000..c1bb8d8f6d --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt @@ -0,0 +1,107 @@ +package org.usvm.ts.pbt.dsl + +import org.junit.jupiter.api.Test +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class DslNumericLocalCompilerTest { + @Test + fun `capture is opt in and its receipt identifies both generated assignments`() { + val program = program() + val compiler = PropertyTypeScriptCompiler() + + val ordinary = compiler.compile(program, generatedModule = "generated.ts", resolveModule = { "./$it" }) + val compiled = compiler.compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "identity"), + ) + val capture = assertNotNull(compiled.numericLocalCapture) + val binding = capture.binding + val lines = compiled.typeScript.lines() + val hash = MessageDigest.getInstance("SHA-256").digest(compiled.typeScript.toByteArray()) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) } + + assertNull(ordinary.numericLocalCapture) + assertTrue("__usvmObserve" !in ordinary.typeScript) + assertEquals(hash, binding.sourceSha256) + assertEquals(program.id.value, binding.programId) + assertEquals(program.locals.single().expression.id, binding.nodeId) + assertEquals("__usvmPredicate", binding.predicateExportName) + assertEquals("__usvmCheckResult", binding.companionExportName) + listOf(binding.predicateAssignment, binding.companionAssignment).forEach { point -> + assertTrue(lines[point.line - 1].startsWith(" const result = ")) + } + val predicate = compiled.typeScript.substringBefore("export function __usvmCheckResult") + assertTrue("__usvmObserve" !in predicate) + assertTrue(binding.predicateAssignment.line < binding.companionAssignment.line) + assertEquals(0, binding.occurrence) + assertEquals(capture.result.callSite, compiled.definition.assertions.first().testedCall) + assertEquals(capture.binding, capture.result.compilerLocal) + assertEquals(0, capture.input.inputIndex) + val callSite = capture.result.callSite + assertTrue(lines[callSite.line - 1].substring(callSite.column - 1).endsWith("(input);")) + } + + @Test + fun `unsupported local and check shapes are rejected instead of silently broadening capture`() { + val requests = listOf( + DslNumericLocalCapture(localName = "missing", checkName = "identity"), + DslNumericLocalCapture(localName = "result", checkName = "missing"), + DslNumericLocalCapture(localName = "result", checkName = "nested"), + ) + requests.forEach { request -> + assertFailsWith { + PropertyTypeScriptCompiler().compile( + program(), + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = request, + ) + } + } + val arithmetic = defineProperty(id = "dsl.arithmetic") { + val input by int() + val result by value(input + 1) + + check(name = "identity") { result equalTo input } + } + + assertFailsWith { + PropertyTypeScriptCompiler().compile( + arithmetic, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "identity"), + ) + } + } + + @Test + fun `a shared declaration after a check is rejected rather than hoisted`() { + assertFailsWith { + defineProperty(id = "dsl.no-hoisting") { + val identity = function<(Double) -> Double>(module = "identity.ts", exportName = "identity") + val input by int() + + check(name = "first") { input equalTo input } + @Suppress("UNUSED_VARIABLE") + val late by value(identity(input)) + } + } + } + + private fun program(): DslProperty = defineProperty(id = "dsl.local-capture") { + val identity = function<(Double) -> Double>(module = "identity.ts", exportName = "identity") + val input by int() + val result by value(identity(input)) + + check(name = "identity") { result equalTo input } + check(name = "nested") { (result equalTo input) and (input equalTo input) } + } +}