diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index d0caedf7c6..4d0d4fa6b2 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/input-export.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/input-export.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": { "@bcoe/v8-coverage": "1.0.2", 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 d76d669de4..957dbac60f 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 @@ -31,6 +31,7 @@ import { type ObservationArtifact, type ObservationPointRequest, type ObservationRequest, + type CompilerNumericLocalBinding, } from './observe-property.js'; import { InputExportRecorder, validateInputExportRequest, type InputExportArtifact, type InputExportRequest } from './input-export.js'; @@ -136,7 +137,14 @@ export async function executeProperty(requestValue: unknown, coverage?: Executio await verifySourceHash(source.module, source.sha256, request.sourceRoots); } - const predicate = await loadEntryPoint(request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig); + const compilerBinding = recorder?.compilerLocalBinding; + const compilerCapture = compilerBinding === undefined ? undefined : { + binding: compilerBinding, + observe: (nodeId: number, localName: string, value: unknown) => 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); @@ -839,7 +847,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi 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)) { + || !['entry-argument', 'argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) { throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid point identity', path); } @@ -851,7 +859,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi callSite: validateSourcePoint(point.callSite, `${path}.callSite`), kind: point.kind as ObservationPointRequest['kind'], }; - if (point.kind === 'argument') { + if (point.kind === 'argument' || point.kind === 'entry-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`); @@ -860,6 +868,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; }); @@ -871,8 +882,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 (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'); } @@ -887,6 +899,53 @@ 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 = validateCompilerLocalBinding(value, manifest, sources, path); + const originalPoint = point.kind === 'return' && point.source.module === manifest.predicate.module + && point.callSite.module === manifest.predicate.module; + if (!originalPoint) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, + 'Compiler local requires an original return point', `${path}.compilerLocal`); + } + + return binding; +} + +export function validateCompilerLocalBinding( + value: unknown, 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 + && !samePoint(predicateAssignment, companionAssignment) + && typeof binding.sourceSha256 === 'string' && /^[0-9a-f]{64}$/.test(binding.sourceSha256) + && source?.sha256 === binding.sourceSha256 && binding.occurrence === 0; + 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/external-witness.ts b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts index 754fc51dfe..811fb8b257 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/external-witness.ts @@ -3,11 +3,12 @@ import { performance } from 'node:perf_hooks'; import fc from 'fast-check'; import { adapterDiagnostic } from './diagnostics.js'; import { EntryPointInvocationError, isNamedCheckFailure, loadEntryPoint, sourceHashMatches, type LoadedEntryPoint } from './entry-point.js'; -import { describeNamedCheckFailure, describePropertyFailure, invokePropertyOnce, validateRequest, type FastCheckFailureDetails } from './execute-property.js'; +import { describeNamedCheckFailure, describePropertyFailure, invokePropertyOnce, validateCompilerLocalBinding, validateRequest, type FastCheckFailureDetails } from './execute-property.js'; import { decodeJsValue, encodeJsValue, ProtocolError, protocolError, type JsConcreteValue, type TaggedJsValue } from './js-value.js'; import { buildPropertyArbitrary } from './property-arbitrary.js'; import { stringifyProtocolJson } from './protocol-json.js'; import type { ExecutionCoverage } from './execution-coverage.js'; +import type { CompilerNumericLocalBinding } from './observe-property.js'; import { inWitnessSupport } from './witness-support.js'; export interface WitnessBinding { @@ -17,11 +18,24 @@ export interface WitnessBinding { occurrence: number; } +interface DslNumericLocalRelation { + compiler: CompilerNumericLocalBinding; + inputIndex: number; + resultIsLeft: boolean; + template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL'; +} + export interface WitnessTarget { id: string; role: 'PROPERTY' | 'COVERAGE' | 'HYPOTHESIS'; binding?: WitnessBinding; expectedOutcome?: 'FALSE' | 'THREW'; + dslNumericLocalRelation?: DslNumericLocalRelation; + entryRelation?: { + leftInputIndex: number; + rightInputIndex: number; + template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL'; + }; } export interface WitnessEvent { @@ -64,7 +78,15 @@ export interface WitnessExecutionSuccess { witnessReduction?: WitnessReduction; } -interface WitnessContext { events: WitnessEvent[]; active: boolean; contractError?: string } +interface WitnessContext { + events: WitnessEvent[]; + active: boolean; + contractError?: string; + compilerTarget: WitnessTarget | undefined; + compilerInput: number | undefined; + compilerCallbacks: number; + compilerDiagnostic?: string; +} const contexts = new AsyncLocalStorage(); /** A passive hook: evaluate the original guard/relation first; return its boolean without substituting an oracle. */ @@ -74,6 +96,11 @@ export function installWitnessHook(): void { value: (pointId: string, contextId: string, revision: string, guard: boolean, holds: boolean): boolean => { const context = contexts.getStore(); if (context?.active) { + const protectedBinding = context.compilerTarget?.binding; + const compilerPoint = protectedBinding?.pointId === pointId && protectedBinding.contextId === contextId + && protectedBinding.revision === revision; + if (compilerPoint) return holds; + const valid = [pointId, contextId, revision].every((value) => typeof value === 'string' && value.length > 0) && typeof guard === 'boolean' && typeof holds === 'boolean'; if (!valid || context.events.length >= 256) { @@ -98,6 +125,12 @@ export async function executeWitness(value: unknown, coverage?: ExecutionCoverag const operation = validateOperation((value as Record).witness, request.manifest.inputs.length); const identity = { witnessPropertyId: request.manifest.propertyId, witnessTarget: operation.target }; const target = operation.target; + const compilerRelation = target.dslNumericLocalRelation; + if (compilerRelation !== undefined) { + compilerRelation.compiler = validateCompilerLocalBinding( + compilerRelation.compiler, request.manifest, operation.sources, 'witness.target.dslNumericLocalRelation', + ); + } const declaredCheck = request.manifest.assertions?.some((check) => check.id === target.id) === true; const diagnosticCheck = request.manifest.predicate.checkResultExportName !== undefined && declaredCheck; const originalCheckObservation = operation.mode === 'replay' && target.binding === undefined @@ -147,6 +180,10 @@ export async function executeWitness(value: unknown, coverage?: ExecutionCoverag } const predicate = await loadEntryPoint( request.manifest.predicate, request.sourceRoots, 'manifest.predicate', request.tsconfig, + compilerRelation === undefined ? undefined : { + binding: compilerRelation.compiler, + observe: captureCompilerLocal, + }, ); const precondition = request.manifest.precondition === undefined ? undefined : await loadEntryPoint( @@ -246,13 +283,35 @@ async function replayOnce( diagnosticCheck: boolean, coverage?: ExecutionCoverage, ): Promise { - const context: WitnessContext = { events: [], active: false }; + const localRelation = target.dslNumericLocalRelation; + const localInput = localRelation === undefined ? undefined : values[localRelation.inputIndex]; + const context: WitnessContext = { + events: [], active: false, compilerCallbacks: 0, + compilerTarget: localRelation === undefined ? undefined : target, + compilerInput: typeof localInput === 'number' ? localInput : undefined, + }; const result: WitnessNativeReplay = { admission: 'ADMITTED', outcome: 'HOLDS', targetMatched: false, events: context.events, runtimeVersion: process.version, }; + if (localRelation !== undefined && typeof localInput !== 'number') { + return { ...result, admission: 'UNKNOWN', outcome: 'UNKNOWN', diagnostic: 'compiler-local-numeric-required' }; + } + const relation = target.entryRelation; + const left = relation === undefined ? undefined : values[relation.leftInputIndex]; + const right = relation === undefined ? undefined : values[relation.rightInputIndex]; + if (relation !== undefined && (typeof left !== 'number' || typeof right !== 'number')) { + return { ...result, admission: 'UNKNOWN', outcome: 'UNKNOWN', diagnostic: 'entry-relation-numeric-required' }; + } + const entryEvent: WitnessEvent | undefined = relation === undefined ? undefined : { + binding: target.binding!, guard: true, + holds: relation.template === 'STRICT_EQUAL' ? left === right : (left as number) <= (right as number), + }; try { const holds = await contexts.run(context, () => invokePropertyOnce( - values, predicate, precondition, undefined, 'replay', coverage, () => { context.active = true; }, + values, predicate, precondition, undefined, 'replay', coverage, () => { + context.active = true; + if (entryEvent !== undefined) context.events.push(entryEvent); + }, )); if (holds === null) { result.admission = 'PRECONDITION_REJECTED'; @@ -273,12 +332,19 @@ async function replayOnce( result.diagnostic = error instanceof ProtocolError ? error.code : describePropertyFailure(error).message; } } + context.active = false; if (context.contractError !== undefined) { result.admission = 'ERROR'; result.outcome = 'ERROR'; result.diagnostic = context.contractError; } + const requiresCompilerPoint = localRelation !== undefined && result.admission === 'ADMITTED'; + const validCompilerPoint = !requiresCompilerPoint + || context.compilerCallbacks === 1 && context.compilerDiagnostic === undefined; + if (!validCompilerPoint) { + result.diagnostic = context.compilerDiagnostic ?? 'compiler-local-point-missing'; + } const event = target.binding === undefined ? undefined : context.events.find((entry) => sameBinding(entry.binding, target.binding as WitnessBinding)); const propertyFailed = result.outcome === 'FALSE' || result.outcome === 'THREW'; @@ -286,7 +352,7 @@ async function replayOnce( const checkMatched = diagnosticCheck ? result.failure?.checkId === target.id : result.failure?.checkId === undefined || result.failure.checkId === target.id; - result.targetMatched = result.admission === 'ADMITTED' && (target.role === 'PROPERTY' + result.targetMatched = validCompilerPoint && result.admission === 'ADMITTED' && (target.role === 'PROPERTY' ? propertyFailed && checkMatched && (target.expectedOutcome === undefined || target.expectedOutcome === result.outcome) && (target.binding === undefined || (guardedEvent && !event.holds)) : guardedEvent && (target.role === 'COVERAGE' || !event.holds)); @@ -294,6 +360,29 @@ async function replayOnce( return result; } +/** Only the callback passed to the selected companion can produce this protected event. */ +function captureCompilerLocal(nodeId: number, localName: string, value: unknown): void { + const context = contexts.getStore(); + const target = context?.compilerTarget; + const relation = target?.dslNumericLocalRelation; + if (context === undefined || !context.active || relation === undefined) return; + + context.compilerCallbacks += 1; + const valid = context.compilerCallbacks === 1 && nodeId === relation.compiler.nodeId + && localName === relation.compiler.localName && typeof value === 'number' && context.compilerInput !== undefined; + if (!valid) { + context.compilerDiagnostic = 'compiler-local-callback-mismatch'; + + return; + } + const left = relation.resultIsLeft ? value : context.compilerInput; + const right = relation.resultIsLeft ? context.compilerInput : value; + context.events.push({ + binding: target!.binding!, guard: true, + holds: relation.template === 'STRICT_EQUAL' ? left === right : (left as number) <= (right as number), + }); +} + export function sameTarget(actual: WitnessNativeReplay, expected: WitnessNativeReplay): boolean { return actual.admission === 'ADMITTED' && actual.targetMatched && actual.outcome === expected.outcome && actual.failure?.checkId === expected.failure?.checkId @@ -319,12 +408,24 @@ function validateOperation(value: unknown, arity: number): WitnessOperation { && typeof binding.contextId === 'string' && binding.contextId.length > 0 && typeof binding.revision === 'string' && binding.revision.length > 0 && Number.isInteger(binding.occurrence) && binding.occurrence >= 0); + const relation = target?.entryRelation; + const validEntryRelation = relation === undefined || (relation !== null && typeof relation === 'object' + && !Array.isArray(relation) && target?.role === 'HYPOTHESIS' + && binding?.contextId === 'original-entry' && binding.occurrence === 0 + && Number.isInteger(relation.leftInputIndex) && relation.leftInputIndex >= 0 && relation.leftInputIndex < arity + && Number.isInteger(relation.rightInputIndex) && relation.rightInputIndex >= 0 && relation.rightInputIndex < arity + && ['STRICT_EQUAL', 'LESS_OR_EQUAL'].includes(relation.template)); + const local = target?.dslNumericLocalRelation; + const validLocal = local === undefined || (local !== null && typeof local === 'object' && !Array.isArray(local) + && relation === undefined && target?.role === 'HYPOTHESIS' && binding?.contextId === 'original-compiler-local' + && binding.occurrence === 0 && Number.isInteger(local.inputIndex) && local.inputIndex >= 0 && local.inputIndex < arity + && typeof local.resultIsLeft === 'boolean' && ['STRICT_EQUAL', 'LESS_OR_EQUAL'].includes(local.template)); const valid = operation !== undefined && ['replay', 'reduce'].includes(operation.mode) && Array.isArray(operation.inputs) && operation.inputs.length === arity && typeof target?.id === 'string' && target.id.length > 0 && ['PROPERTY', 'COVERAGE', 'HYPOTHESIS'].includes(target.role) && (target.expectedOutcome === undefined || ['FALSE', 'THREW'].includes(target.expectedOutcome)) - && validBinding && (target.role === 'PROPERTY' || binding !== undefined) + && validBinding && validEntryRelation && validLocal && (target.role === 'PROPERTY' || binding !== undefined) && Array.isArray(operation.sources) && operation.sources.length > 0 && operation.sources.every((source) => source !== null && typeof source === 'object' && typeof source.module === 'string' && typeof source.sha256 === 'string' && /^[0-9a-f]{64}$/.test(source.sha256)); 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 a4385769ff..577628e6c3 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 @@ -12,8 +12,24 @@ export interface ObservationPointRequest { operandId: string; source: SourcePoint; callSite: SourcePoint; - kind: 'argument' | 'return' | 'intermediate' | 'pre' | 'post'; + 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'], @@ -153,6 +185,12 @@ export class ObservationRecorder { return invocation(); } + for (const point of this.request.points) { + if (point.kind === 'entry-argument') { + this.capturePoint(record, point, values[point.inputIndex!]); + } + } + return contexts.run({ recorder: this, invocation: record }, invocation); } @@ -166,7 +204,19 @@ export class ObservationRecorder { point(record: InvocationRecord, pointId: string, value: unknown): void { const point = this.pointsById.get(pointId); - if (point === undefined || record.points.length >= this.request.maxPointsPerInvocation) { + // 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); + + return; + } + + this.capturePoint(record, point, value); + } + + 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); return; @@ -180,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..789a67bef7 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts @@ -0,0 +1,271 @@ +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 { executeWitness, type WitnessTarget } from '../src/external-witness.js'; +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); +}); + +function witnessRequest(request: ReturnType, input = 7) { + const target: WitnessTarget = { + id: 'compiler-result', role: 'HYPOTHESIS', + binding: { pointId: 'compiler-result', contextId: 'original-compiler-local', revision: 'v1', occurrence: 0 }, + dslNumericLocalRelation: { + compiler: request.observationRequest.points[0]!.compilerLocal!, + inputIndex: 0, resultIsLeft: true, template: 'STRICT_EQUAL', + }, + }; + + return { ...request, witness: { + mode: 'replay', target, inputs: [encodeJsValue(input)], sources: request.observationRequest.sources, + } }; +} + +test('compiler witness callback compares original numeric snapshots with JavaScript semantics', async () => { + await fixture(async (request) => { + for (const input of [Number.NaN, -0, Number.NEGATIVE_INFINITY, Number.POSITIVE_INFINITY]) { + const initial = witnessRequest(request, input); + const selected = { ...initial, manifest: { ...initial.manifest, inputs: [{ name: 'value', domain: { + kind: 'number', min: { value: 'negative-infinity' }, max: { value: 'positive-infinity' }, allowNaN: true, + } }] } }; + + const replay = (await executeWitness(selected)).witnessReplay; + + assert.equal(replay?.outcome, 'HOLDS'); + assert.equal(replay?.targetMatched, Number.isNaN(input)); + assert.deepEqual(replay?.events.map((event) => event.binding), [initial.witness.target.binding]); + } + }); +}); + +test('missing wrong repeated and nonnumeric compiler witness receipts retain the original oracle', async () => { + const callbacks = [ + '', "observer?.(5, 'result', result);", "observer?.(4, 'other', result);", + "observer?.(4, 'result', 'unsupported');", + "observer?.(4, 'result', result); observer?.(4, 'result', result);", + ]; + for (const callback of callbacks) { + await fixture(async (request) => { + const replay = (await executeWitness(witnessRequest(request))).witnessReplay; + + assert.equal(replay?.outcome, 'HOLDS'); + assert.equal(replay?.admission, 'ADMITTED'); + assert.equal(replay?.targetMatched, false); + assert.ok(replay?.diagnostic?.startsWith('compiler-local-')); + }, callback); + } +}); + +test('public witness hook cannot impersonate the compiler callback', async () => { + await fixture(async (request) => { + const replay = (await executeWitness(witnessRequest(request))).witnessReplay; + + assert.equal(replay?.outcome, 'HOLDS'); + assert.equal(replay?.targetMatched, false); + assert.deepEqual(replay?.events, []); + assert.equal(replay?.diagnostic, 'compiler-local-point-missing'); + }, `(globalThis as any)[Symbol.for('org.usvm.ts.pbt.witness')]?.( + 'compiler-result', 'original-compiler-local', 'v1', true, false);`); +}); + +test('compiler witness validates input index direction context and declared compiler authority', async () => { + await fixture(async (request) => { + const initial = witnessRequest(request); + const target = initial.witness.target; + const local = target.dslNumericLocalRelation!; + const badTargets = [ + { ...target, dslNumericLocalRelation: { ...local, inputIndex: 1 } }, + { ...target, dslNumericLocalRelation: { ...local, resultIsLeft: 'true' } }, + { ...target, dslNumericLocalRelation: { ...local, template: 'COERCING_EQUAL' } }, + { ...target, binding: { ...target.binding!, contextId: 'helper' } }, + { ...target, dslNumericLocalRelation: { ...local, compiler: { ...local.compiler, producer: 'source-line' } } }, + { ...target, dslNumericLocalRelation: { ...local, compiler: { ...local.compiler, sourceSha256: '0'.repeat(64) } } }, + ]; + for (const changed of badTargets) { + await assert.rejects(executeWitness({ ...initial, witness: { ...initial.witness, target: changed } }), + (error: unknown) => error instanceof ProtocolError && error.code === 'protocol.request.invalid'); + } + }); +}); 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 2312164a46..fcc206a589 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 @@ -188,6 +188,34 @@ test('bounded explicit observation preserves special values and refuses proxies, assert.equal(recorder.result.invocations.length, 1); }); +test('entry arguments are adapter snapshots before user code and cannot be replaced through the hook', () => { + const source = { module: 'property.ts', line: 1, column: 1 }; + const recorder = new ObservationRecorder('property', { + points: ['left', 'right'].map((id, inputIndex) => ({ + id, assertionId: 'original', operandId: id, source, callSite: source, + kind: 'entry-argument', inputIndex, + })), + sources: [{ module: 'property.ts', sha256: 'a'.repeat(64) }], + maxInvocations: 1, maxPointsPerInvocation: 2, maxArrayElements: 2, maxBytes: 65_536, + }); + installObservationHook(); + const hook = (globalThis as Record)[Symbol.for('org.usvm.ts.pbt.observe')] as + (pointId: string, value: unknown) => unknown; + const inputs = [Number.NaN, -0]; + + recorder.run(inputs, 'generation', () => { + inputs[0] = 7; + hook('left', 42); + hook('right', Number.POSITIVE_INFINITY); + }); + + const invocation = recorder.result.invocations[0]!; + assert.deepEqual(invocation.points.map((event) => event.value.value), [encodeJsValue(Number.NaN), encodeJsValue(-0)]); + assert.deepEqual(invocation.points.map((event) => event.occurrence), [0, 0]); + assert.equal(recorder.result.buildStatus, 'unverified'); + assert.equal(recorder.result.droppedPoints, 0); +}); + test('observation limits report dropped invocations and points without changing returned values', () => { const request: ObservationRequest = { points: [{ diff --git a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts index 644e2f9019..902045ce62 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts @@ -11,6 +11,103 @@ const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../../. const module = 'properties/witness/ExternalWitness.ts'; const sha256 = createHash('sha256').update(await readFile(path.join(root, module))).digest('hex'); const binding = (pointId: string) => ({ pointId, contextId: 'original', revision: 'v1', occurrence: 0 }); +const entryModule = 'properties/inference/EntryRelations.ts'; +const entryHash = createHash('sha256').update(await readFile(path.join(root, entryModule))).digest('hex'); + +function entryRequest( + left: number, right: number, template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL' = 'LESS_OR_EQUAL', predicate = 'always', +) { + const target: WitnessTarget = { + id: 'entry-relation', role: 'HYPOTHESIS', + binding: { pointId: 'entry-relation', contextId: 'original-entry', revision: entryHash, occurrence: 0 }, + entryRelation: { leftInputIndex: 0, rightInputIndex: 1, template }, + }; + const domain = { kind: 'number', min: { value: 'negative-infinity' }, max: { value: 'positive-infinity' }, allowNaN: true }; + + return { + manifest: { + propertyId: 'witness.entry', predicate: { module: entryModule, exportName: predicate, executionKind: 'sync' }, + inputs: [{ name: 'left', domain }, { name: 'right', domain }], assertions: [], + }, + sourceRoots: [root], examples: [], numRuns: 1, timeoutMillis: 5000, + witness: { + mode: 'replay', target, inputs: [encodeJsValue(left), encodeJsValue(right)], + sources: [{ module: entryModule, sha256: entryHash }], + }, + }; +} + +test('adapter-owned entry comparisons retain JavaScript NaN signed-zero and infinity semantics', async () => { + const cases = [ + [-0, 0, 'STRICT_EQUAL', true], + [Number.NaN, Number.NaN, 'STRICT_EQUAL', false], + [Number.POSITIVE_INFINITY, Number.POSITIVE_INFINITY, 'STRICT_EQUAL', true], + [Number.NEGATIVE_INFINITY, Number.POSITIVE_INFINITY, 'LESS_OR_EQUAL', true], + [Number.POSITIVE_INFINITY, Number.NEGATIVE_INFINITY, 'LESS_OR_EQUAL', false], + [Number.NaN, 0, 'LESS_OR_EQUAL', false], + ] as const; + + for (const [left, right, template, holds] of cases) { + const replay = (await executeWitness(entryRequest(left, right, template))).witnessReplay; + + assert.equal(replay?.outcome, 'HOLDS'); + assert.equal(replay?.events[0]?.holds, holds); + assert.equal(replay?.targetMatched, !holds); + } +}); + +test('entry refutation snapshots precede callback mutation and only admitted inputs receive an event', async () => { + const mutation = (await executeWitness(entryRequest(80, 0, 'LESS_OR_EQUAL', 'entryMutation'))).witnessReplay; + const rejected = entryRequest(80, 0); + const guarded = { ...rejected, manifest: { + ...rejected.manifest, precondition: { module: entryModule, exportName: 'ordered', executionKind: 'sync' }, + } }; + + const skipped = (await executeWitness(guarded)).witnessReplay; + + assert.equal(mutation?.outcome, 'HOLDS'); + assert.equal(mutation?.events[0]?.holds, false); + assert.equal(mutation?.targetMatched, true); + assert.equal(skipped?.admission, 'PRECONDITION_REJECTED'); + assert.equal(skipped?.targetMatched, false); + assert.deepEqual(skipped?.events, []); +}); + +test('native reduction retains the same admitted entry relation and holding original oracle', async () => { + const initial = entryRequest(80, 0); + const domain = { kind: 'integer', min: 0, max: 100 }; + const selected = { ...initial, manifest: { + ...initial.manifest, inputs: [{ name: 'left', domain }, { name: 'right', domain }], + } }; + const expected = (await executeWitness(selected)).witnessReplay; + + const reduced = (await executeWitness({ ...selected, witness: { ...selected.witness, mode: 'reduce', expected } })).witnessReduction; + const final = (await executeWitness({ ...selected, witness: { ...selected.witness, inputs: reduced?.inputs } })).witnessReplay; + + assert.equal(reduced?.status, 'EXHAUSTED'); + assert.ok((reduced?.acceptedShrinks ?? 0) > 0); + assert.deepEqual(reduced?.inputs, [encodeJsValue(1), encodeJsValue(0)]); + assert.equal(final?.outcome, 'HOLDS'); + assert.equal(final?.targetMatched, true); + assert.deepEqual(final?.events[0]?.binding, initial.witness.target.binding); +}); + +test('entry target indices templates context and occurrence are validated before execution', async () => { + const original = entryRequest(80, 0); + const target = original.witness.target; + const cases = [ + { ...target, entryRelation: { ...target.entryRelation!, leftInputIndex: -1 } }, + { ...target, entryRelation: { ...target.entryRelation!, rightInputIndex: 2 } }, + { ...target, entryRelation: { ...target.entryRelation!, template: 'COERCING_EQUAL' } }, + { ...target, binding: { ...target.binding!, contextId: 'helper' } }, + { ...target, binding: { ...target.binding!, occurrence: 1 } }, + ]; + + for (const selected of cases) { + await assert.rejects(executeWitness({ ...original, witness: { ...original.witness, target: selected } }), + (error: unknown) => error instanceof ProtocolError && error.code === 'protocol.request.invalid'); + } +}); function request(predicate: string, target: WitnessTarget = { id: predicate, role: 'PROPERTY' }, inputs = [encodeJsValue(80)]) { return { 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 f795c89bab..f6a7b6442c 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 @@ -15,10 +15,13 @@ import org.usvm.ts.pbt.backend.WitnessReplayConfiguration import org.usvm.ts.pbt.backend.WitnessReplayDeadline import org.usvm.ts.pbt.coverage.captureCoverageIdentity 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 import org.usvm.ts.pbt.validation.validatePropertyDefinition @@ -181,16 +184,37 @@ class FastCheckBackend( } } val allInputIndexesValid = request.points.all { point -> - if (point.kind == org.usvm.ts.pbt.observation.ObservationPointKind.ARGUMENT) { + val isArgument = point.kind == ObservationPointKind.ARGUMENT || + point.kind == ObservationPointKind.ENTRY_ARGUMENT + if (isArgument) { point.inputIndex in property.inputs.indices } else { point.inputIndex == null } } 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 && allSourcesPresent && - allPointsBound && allInputIndexesValid && hashesValid + allPointsBound && allInputIndexesValid && hashesValid && compilerLocalsValid if (!validRequest) { throw invalidRequest( diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index fc8d6b189d..42f83e21bf 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt @@ -336,6 +336,18 @@ internal class FastCheckWitnessCoordinator( if (!inputs.hasWitnessEncoding()) return WitnessReplayStatus.UNREPRESENTABLE_INPUT if (!inDeclaredSupport(property, inputs)) return WitnessReplayStatus.DOMAIN_REJECTED + val entryRelation = candidate.target.entryRelation + if (entryRelation != null) { + val numericInputs = inputs.getOrNull(entryRelation.leftInputIndex) is JsConcreteValue.Number && + inputs.getOrNull(entryRelation.rightInputIndex) is JsConcreteValue.Number + if (!numericInputs) return WitnessReplayStatus.UNSUPPORTED_REPLAY + } + + val localRelation = candidate.target.dslNumericLocalRelation + if (localRelation != null && inputs.getOrNull(localRelation.inputIndex) !is JsConcreteValue.Number) { + return WitnessReplayStatus.UNSUPPORTED_REPLAY + } + val sourceModules = candidate.sources.mapTo(hashSetOf()) { source -> source.module } val requiredModules = listOfNotNull(property.predicate.module, property.precondition?.module) val validSources = candidate.sources.all { source -> source.sha256.matches(SHA256_REGEX) } && 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-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRefutationTest.kt new file mode 100644 index 0000000000..256d8ea97d --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRefutationTest.kt @@ -0,0 +1,260 @@ +package org.usvm.ts.pbt.inference + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReductionStatus +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.dsl.defineProperty +import org.usvm.ts.pbt.dsl.invoke +import org.usvm.ts.pbt.dsl.lessOrEqual +import org.usvm.ts.pbt.dsl.notEqualTo +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmDslNumericLocalRefutation +import org.usvm.ts.pbt.usvm.UsvmDslNumericLocalRefuter +import org.usvm.ts.pbt.usvm.UsvmRelationRefutationStatus +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.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class DslNumericLocalRefutationTest { + @TempDir + lateinit var root: Path + + @Test + fun `sampled equality is refuted after the store while both full original replays hold`() { + val fixture = prepare() + + val refutation = fixture.refute() + assertEquals( + UsvmRelationRefutationStatus.REFUTATION_REACHED, + refutation.status, + refutation.diagnostics.toString(), + ) + val candidate = refutation.captureWitness() + val native = backend().confirmWitness(fixture.compiled.definition, candidate, REPLAY) + + assertEquals(listOf(417.0), refutation.inputs?.map { (it as JsConcreteValue.Number).toDouble() }) + assertEquals(ObservationBuildStatus.UNVERIFIED, fixture.inference.buildStatus) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.HOLDS, native.reducedReplay?.outcome) + assertEquals(candidate.target.binding, native.contextualRefutations.single().binding) + } + + @Test + fun `complete original named check failure takes priority over the local hypothesis`() { + val fixture = prepare(delta = "+ 1") + + val refutation = fixture.refute() + val native = backend().confirmWitness(fixture.compiled.definition, refutation.captureWitness(), REPLAY) + + assertEquals(UsvmRelationRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.FALSE, native.originalReplay?.outcome) + assertEquals("bound", native.originalReplay?.failure?.checkId) + assertEquals(WitnessOracleOutcome.FALSE, native.reducedReplay?.outcome) + assertTrue(native.contextualRefutations.isNotEmpty()) + } + + @Test + fun `original input on the left preserves the direction of a non symmetric numeric relation`() { + val fixture = prepare() + val order = fixture.inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val reversed = order.copy( + pair = ScalarObservationPair(order.pair.right, order.pair.left), + evidence = order.evidence.map { it.copy(left = it.right, right = it.left) }, + ) + val inference = fixture.inference.copy(relations = listOf(reversed)) + val selected = fixture.copy(inference = inference, relation = reversed) + + val refutation = selected.refute() + val native = backend().confirmWitness(fixture.compiled.definition, refutation.captureWitness(), REPLAY) + + assertEquals(false, refutation.binding.targets.single().resultIsLeft) + assertEquals(UsvmRelationRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + } + + @Test + fun `native shrinking retains the local relation and complete original oracle`() { + val fixture = prepare(condition = "input >= 417 && input <= 420") + val inputs = listOf(JsConcreteValue.number(value = 420.0)) + val candidate = fixture.refute().captureWitness().copy(inputs = inputs) + + val native = backend().confirmWitness(fixture.compiled.definition, candidate, REPLAY) + + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessReductionStatus.EXHAUSTED, native.reduction.status) + assertTrue(native.reduction.acceptedShrinks > 0) + assertEquals(listOf(JsConcreteValue.number(value = 417.0)), native.reduction.inputs) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.HOLDS, native.reducedReplay?.outcome) + assertTrue(assertNotNull(native.reducedReplay).targetMatched) + } + + @Test + fun `original admission excludes the only local refutation and exhausted search returns no candidate`() { + val fixture = prepare(excludeRefutation = true) + + val refutation = fixture.refute() + + assertEquals(UsvmRelationRefutationStatus.NO_REFUTATION_REACHED, refutation.status) + assertNull(refutation.inputs) + } + + @Test + fun `an exhausted auxiliary prefix does not execute an unsupported original suffix`() { + val fixture = prepare(condition = "false", sparseSuffix = true) + + val refutation = fixture.refute() + + assertEquals(UsvmRelationRefutationStatus.NO_REFUTATION_REACHED, refutation.status) + assertTrue(refutation.diagnostics.isEmpty()) + assertNull(refutation.inputs) + } + + @Test + fun `runtime limitation before the selected store and timeout remain distinct from exhaustion`() { + val fixture = prepare(sparsePrefix = true) + val limited = fixture.refute() + val refuter = UsvmDslNumericLocalRefuter( + fixture.scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = Duration.ZERO), + ) + + val timeout = refuter.refute(fixture.compiled, fixture.mapping, CONCRETE, fixture.inference, fixture.relation) + + assertEquals(UsvmRelationRefutationStatus.UNSUPPORTED, limited.status) + assertTrue(limited.diagnostics.any { it.code == "usvm.runtime.array-index-growth" }) + assertNull(limited.inputs) + assertEquals(UsvmRelationRefutationStatus.TIMEOUT, timeout.status) + assertTrue(timeout.timedOut) + assertNull(timeout.inputs) + } + + @Test + fun `a changed compiler receipt cannot confirm the target and retains the full original outcome`() { + val fixture = prepare() + val candidate = fixture.refute().captureWitness() + val target = assertNotNull(candidate.target.dslNumericLocalRelation) + val wrong = target.copy(compiler = target.compiler.copy(nodeId = target.compiler.nodeId + 1)) + val changed = candidate.copy(target = candidate.target.copy(dslNumericLocalRelation = wrong)) + + val native = backend().confirmWitness(fixture.compiled.definition, changed, REPLAY) + + assertEquals(WitnessReplayStatus.TARGET_MISMATCH, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + assertEquals(false, native.originalReplay?.targetMatched) + assertEquals(candidate.inputs, native.candidate.inputs) + assertTrue(native.contextualRefutations.isEmpty()) + } + + private fun Fixture.refute(): UsvmDslNumericLocalRefutation = UsvmDslNumericLocalRefuter(scene).refute( + compiled, + mapping, + CONCRETE, + inference, + relation, + ) + + private fun backend(): FastCheckBackend = FastCheckBackend(sourceRoots = listOf(root)) + + private fun prepare( + delta: String = "- 1", + excludeRefutation: Boolean = false, + sparsePrefix: Boolean = false, + condition: String = "input === 417", + sparseSuffix: Boolean = false, + ): Fixture { + val prefix = if (sparsePrefix) "const cache: number[] = []; cache[1001] = input;" else "" + val source = """ + export function transform(input: number): number { + $prefix + if ($condition) return input $delta; + return input; + } + export function suffix(input: number): number { + const cache: number[] = []; + cache[1001] = input; + return input; + } + """.trimIndent() + Files.writeString(root.resolve("functions.ts"), source) + val program = defineProperty(id = "dsl.local-refutation") { + val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform") + val suffix = function<(Double) -> Double>(module = "functions.ts", exportName = "suffix") + val input by int(min = 0, max = 1000) + if (excludeRefutation) assume { input notEqualTo 417 } + val result by value(transform(input)) + + check(name = "bound") { result lessOrEqual input } + if (sparseSuffix) check(name = "suffix") { suffix(result) lessOrEqual input } + } + val compiled = PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + Files.writeString(root.resolve("generated.ts"), compiled.typeScript) + val capture = assertNotNull(compiled.numericLocalCapture) + val hash = MessageDigest.getInstance("SHA-256").digest(source.toByteArray()) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val request = capture.observationRequest().let { request -> + request.copy(sources = request.sources + PropertyObservationSource(module = "functions.ts", sha256 = hash)) + } + val observation = backend().run( + compiled.definition, + PropertyRunConfiguration(seed = 42, numRuns = 8, observationRequest = request), + ) + val inference = inferScalarRelations( + compiled.definition, + assertNotNull(observation.observations), + listOf(ScalarObservationPair(capture.result, capture.input)), + ) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val scene = loadEtsProjectAutoConvert(root, provider = EtsIrProvider.TS_FRONTEND) + val mapping = PropertyEtsMapper(scene, sourceRoots = listOf(root)).map(compiled.definition.toManifest()) + + return Fixture(compiled, scene, mapping, inference, relation) + } + + private data class Fixture( + val compiled: CompiledDslProperty, + val scene: EtsScene, + val mapping: PropertyEtsMappingArtifact, + val inference: ScalarRelationInference, + val relation: ScalarRelation, + ) + + private companion object { + val CONCRETE = ProjectionCapability(level = ProjectionLevel.EXACT) + val REPLAY = WitnessReplayConfiguration(timeoutMillis = 15_000, validationReserveMillis = 3_000) + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt new file mode 100644 index 0000000000..ffc44cc7a0 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt @@ -0,0 +1,397 @@ +package org.usvm.ts.pbt.inference + +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.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.dsl.defineProperty +import org.usvm.ts.pbt.dsl.equalTo +import org.usvm.ts.pbt.dsl.invoke +import org.usvm.ts.pbt.dsl.lessOrEqual +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyPointEvent +import org.usvm.ts.pbt.usvm.bindDslNumericLocalRelation +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.assertSame +import kotlin.test.assertTrue + +class DslNumericLocalRelationTest { + @TempDir + lateinit var root: Path + + @Test + fun `compiler program and actual native receipt bind the result after its original numeric store`() { + val fixture = prepare() + val capture = assertNotNull(fixture.compiled.numericLocalCapture) + + val binding = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(ScalarRelationStatus.SAMPLED, fixture.relation.status) + assertEquals(EtsMappingStatus.EXACT, binding.status, binding.diagnostics.toString()) + assertEquals(ObservationBuildStatus.UNVERIFIED, fixture.inference.buildStatus) + assertEquals(capture.binding, binding.targets.single().compiler) + assertEquals("result", binding.targets.single().local.name) + assertEquals(0, binding.targets.single().inputIndex) + } + + @Test + fun `forged local ABI node kind and wrapper cannot become compiler authority through a source hash`() { + val fixture = prepare() + val compiled = fixture.compiled + val capture = assertNotNull(compiled.numericLocalCapture) + val badBindings = listOf( + capture.binding.copy(localName = "other"), + capture.binding.copy(abi = "other-callback"), + capture.binding.copy(nodeId = capture.binding.nodeId + 1), + capture.binding.copy(occurrence = 1), + capture.binding.copy(predicateAssignment = capture.binding.companionAssignment), + ) + val badCaptures = badBindings.map { binding -> + capture.copy(binding = binding, result = capture.result.copy(compilerLocal = binding)) + } + capture.copy(result = capture.result.copy(kind = ObservationPointKind.INTERMEDIATE)) + val badPrograms = badCaptures.map { compiled.copy(numericLocalCapture = it) } + listOf( + compiled.copy(typeScript = compiled.typeScript.replace("const result =", "let result =")), + compiled.copy(resolvedModules = emptyMap()), + ) + + badPrograms.forEach { changed -> + val binding = bindDslNumericLocalRelation(changed, fixture.mapping, fixture.inference, fixture.relation) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertTrue(binding.targets.isEmpty()) + assertEquals("usvm.dsl-local.compiler-mismatch", binding.diagnostics.single().code) + } + } + + @Test + fun `the selected original input can precede the result in a relation`() { + val fixture = prepare() + val original = fixture.relation + val evidence = original.evidence.map { it.copy(left = it.right, right = it.left) } + val reversed = original.copy( + pair = ScalarObservationPair(original.pair.right, original.pair.left), + evidence = evidence + ) + val inference = fixture.inference.copy(relations = listOf(reversed)) + + val binding = bindDslNumericLocalRelation(fixture.compiled, fixture.mapping, inference, reversed) + + assertEquals(EtsMappingStatus.EXACT, binding.status) + assertEquals(false, binding.targets.single().resultIsLeft) + } + + @Test + fun `swapped input parameters wrong names and wrong stack slots cannot activate an exact point`() { + val fixture = prepare() + val entry = fixture.mapping.predicate.targets.single() + val inputs = entry.bindings.inputs + val first = inputs[0] + val second = inputs[1] + val invalidInputs = listOf( + inputs.reversed(), + listOf(first.copy(stackSlot = second.stackSlot), second), + listOf(first.copy(parameter = second.parameter), second), + listOf(first.copy(propertyInputName = second.propertyInputName), second), + ) + + invalidInputs.forEach { changed -> + val target = entry.copy(bindings = entry.bindings.copy(inputs = changed)) + val predicate = fixture.mapping.predicate.copy(targets = listOf(target)) + val mapping = fixture.mapping.copy(predicate = predicate) + + val binding = bindDslNumericLocalRelation(fixture.compiled, mapping, fixture.inference, fixture.relation) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertEquals("usvm.dsl-local.input-mismatch", binding.diagnostics.single().code) + assertTrue(binding.targets.isEmpty()) + } + } + + @Test + fun `repeated nested out of order wrong context and unavailable receipts cannot activate exact guidance`() { + val fixture = prepare() + val relation = fixture.relation + val repeated = relation.copy( + evidence = relation.evidence.map { evidence -> + val duplicate = evidence.left.copy(occurrence = 1) + val invocation = evidence.invocation.copy(points = evidence.invocation.points + duplicate) + + evidence.copy(invocation = invocation) + } + ) + val nested = relation.copy( + evidence = relation.evidence.map { evidence -> + evidence.copy(invocation = evidence.invocation.copy(parentInvocationId = 1)) + } + ) + val wrongContext = relation.copy( + evidence = relation.evidence.map { evidence -> + val original = assertNotNull(evidence.invocation.callSite) + val invocation = evidence.invocation.copy(callSite = original.copy(line = original.line + 1)) + + evidence.copy(invocation = invocation) + } + ) + val wrongInput = relation.copy( + evidence = relation.evidence.map { evidence -> + val input = evidence.invocation.input.copy( + value = JsConcreteValue.Array(listOf(JsConcreteValue.number(-1.0))) + ) + + evidence.copy(invocation = evidence.invocation.copy(input = input)) + } + ) + val unavailable = relation.changedResult { event -> + event.copy(value = event.value.copy(status = ObservationValueStatus.UNSUPPORTED, value = null)) + } + val wrongTime = relation.changedResult { event -> event.copy(eventOrdinal = 0) } + val wrongLocal = relation.changedResult { event -> + val compiler = assertNotNull(event.compilerLocal) + + event.copy(compilerLocal = compiler.copy(localName = "other")) + } + + listOf(repeated, nested, wrongContext, wrongInput, unavailable, wrongTime, wrongLocal).forEach { changed -> + val inference = fixture.inference.copy(relations = listOf(changed)) + + val binding = bindDslNumericLocalRelation(fixture.compiled, fixture.mapping, inference, changed) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertTrue(binding.targets.isEmpty()) + } + } + + @Test + fun `changed selected wrapper or helper source cannot activate a stale challenge`() { + val fixture = prepare() + val generated = root.resolve("generated.ts") + Files.writeString(generated, fixture.compiled.typeScript + "\n// changed selected source\n") + + val staleWrapper = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + Files.writeString(generated, fixture.compiled.typeScript) + Files.writeString( + root.resolve("functions.ts"), + "export function transform(input: number): number { return input; }" + ) + val staleHelper = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(EtsMappingStatus.UNSUPPORTED, staleWrapper.status) + assertEquals(EtsMappingStatus.UNSUPPORTED, staleHelper.status) + assertTrue(staleWrapper.diagnostics.any { it.code == "usvm.dsl-local.source-stale" }) + assertTrue(staleHelper.diagnostics.any { it.code == "usvm.dsl-local.source-stale" }) + } + + @Test + fun `ambiguous entries and missing source remain distinct from an exact point`() { + val fixture = prepare() + val predicate = fixture.mapping.predicate + val diagnostic = EtsMappingDiagnostic(code = "test.ambiguous-entry", message = "Two original entries") + val ambiguousPredicate = EtsMappingResult( + status = EtsMappingStatus.AMBIGUOUS, + targets = predicate.targets + predicate.targets, + diagnostics = listOf(diagnostic), + ) + val ambiguousMapping = fixture.mapping.copy(predicate = ambiguousPredicate) + + val ambiguous = bindDslNumericLocalRelation( + fixture.compiled, + ambiguousMapping, + fixture.inference, + fixture.relation + ) + Files.delete(root.resolve("generated.ts")) + val missing = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(EtsMappingStatus.AMBIGUOUS, ambiguous.status) + assertEquals(2, ambiguous.targets.size) + assertEquals(EtsMappingStatus.UNMAPPED, missing.status) + assertTrue(missing.targets.isEmpty()) + } + + @Test + fun `native compiler observations keep a stronger equality and exclude the original order only`() { + val fixture = prepare() + + val selected = selectScalarGuidance(fixture.inference, fixture.compiled) + + assertSame(fixture.inference, selected.inference) + assertEquals(ScalarRelationTemplate.STRICT_EQUAL, selected.candidates.single().relation.template) + assertEquals(ScalarGuidanceRelevance.KNOWN_DSL_CHECK, selected.candidates.single().relevance) + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, selected.excluded.single().relation.template) + assertEquals(ScalarGuidanceExclusionReason.ORIGINAL_CHECK, selected.excluded.single().reason) + assertEquals(ObservationBuildStatus.UNVERIFIED, selected.inference.buildStatus) + } + + @Test + fun `an original equality excludes both equality and its weaker orders over the same captured operands`() { + val fixture = prepare(originalEquality = true) + val relations = fixture.inference.relations + val reversed = relations.map { relation -> + relation.copy( + pair = ScalarObservationPair(relation.pair.right, relation.pair.left), + evidence = relation.evidence.map { it.copy(left = it.right, right = it.left) }, + ) + } + val inference = fixture.inference.copy(relations = relations + reversed) + + val selected = selectScalarGuidance(inference, fixture.compiled) + + assertTrue(selected.candidates.isEmpty()) + assertEquals(4, selected.excluded.size) + assertTrue(selected.excluded.all { it.reason == ScalarGuidanceExclusionReason.ORIGINAL_CHECK }) + assertTrue(selected.excluded.all { it.relevance == ScalarGuidanceRelevance.KNOWN_DSL_CHECK }) + assertEquals(inference.relations, selected.excluded.map { it.relation }) + } + + @Test + fun `forged retained program source or point metadata cannot establish original formula relevance`() { + val fixture = prepare() + val compiled = fixture.compiled + val capture = assertNotNull(compiled.numericLocalCapture) + val fake = capture.copy(result = capture.result.copy(operandId = "unrelated")) + val variants = listOf( + compiled.copy(numericLocalCapture = fake), + compiled.copy(typeScript = compiled.typeScript + "// changed source"), + compiled.copy(resolvedModules = emptyMap()), + compiled.copy(program = compiled.program.copy(checks = emptyList())), + ) + for (changed in variants) { + val selected = selectScalarGuidance(fixture.inference, changed) + + assertEquals(2, selected.candidates.size) + assertTrue(selected.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(selected.excluded.isEmpty()) + } + val changedPoints = fixture.inference.relations.map { relation -> + relation.copy(pair = relation.pair.copy(left = relation.pair.left.copy(id = "other-result"))) + } + val relabeled = selectScalarGuidance(fixture.inference.copy(relations = changedPoints), compiled) + assertTrue(relabeled.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(relabeled.excluded.isEmpty()) + + val staleSources = fixture.inference.sources.map { it.copy(sha256 = "0".repeat(n = 64)) } + val stale = selectScalarGuidance(fixture.inference.copy(sources = staleSources), compiled) + assertTrue(stale.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + } + + private fun ScalarRelation.changedResult( + change: (PropertyPointEvent) -> PropertyPointEvent, + ): ScalarRelation { + val changed = evidence.map { evidence -> + val result = change(evidence.left) + val points = evidence.invocation.points.map { event -> if (event == evidence.left) result else event } + + evidence.copy(left = result, invocation = evidence.invocation.copy(points = points)) + } + + return copy(evidence = changed) + } + + private fun prepare(originalEquality: Boolean = false): Fixture { + val compiled = compile(originalEquality) + val capture = assertNotNull(compiled.numericLocalCapture) + val sources = capture.observationRequest().sources + source(module = "functions.ts") + val request = capture.observationRequest().copy(sources = sources) + val observation = FastCheckBackend(sourceRoots = listOf(root)).run( + compiled.definition, + PropertyRunConfiguration(seed = 42, numRuns = 8, observationRequest = request), + ) + val inference = inferScalarRelations( + compiled.definition, + assertNotNull(observation.observations), + listOf(ScalarObservationPair(capture.result, capture.input)), + ) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val files = listOf("functions.ts", "generated.ts").map { module -> + loadEtsFileAutoConvert(root.resolve(module), provider = EtsIrProvider.TS_FRONTEND) + } + val scene = EtsScene(files) + val mapping = PropertyEtsMapper(scene, sourceRoots = listOf(root)).map(compiled.definition.toManifest()) + + return Fixture(compiled, mapping, inference, relation) + } + + private fun source(module: String): PropertyObservationSource { + val hash = MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(root.resolve(module))) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + + return PropertyObservationSource(module, hash) + } + + private fun compile(originalEquality: Boolean): CompiledDslProperty { + val source = """ + export function transform(input: number): number { + if (input === 417) return input - 1; + return input; + } + """.trimIndent() + Files.writeString(root.resolve("functions.ts"), source) + val program = defineProperty(id = "dsl.local-relation") { + val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform") + val input by int(min = 0, max = 1000) + val other by int(min = 0, max = 1000) + val result by value(transform(input)) + + check(name = "bound") { + if (originalEquality) result equalTo input else result lessOrEqual input + } + check(name = "other-input") { other lessOrEqual 1000 } + } + val compiled = PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + Files.writeString(root.resolve("generated.ts"), compiled.typeScript) + + return compiled + } + + private data class Fixture( + val compiled: CompiledDslProperty, + val mapping: PropertyEtsMappingArtifact, + val inference: ScalarRelationInference, + val relation: ScalarRelation, + ) +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt new file mode 100644 index 0000000000..06242ca2d5 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt @@ -0,0 +1,273 @@ +package org.usvm.ts.pbt.inference + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +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.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.PropertyDomain +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.observation.ObservationBuildStatus +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 org.usvm.ts.pbt.usvm.UsvmEntryRefutationStatus +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefutation +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefuter +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import java.nio.file.Files +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class EntryRelationRefutationTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + @Test + fun `an auxiliary equality refutation is confirmed while the complete original property holds`() { + val inference = observe(predicate = "reflexive") + val relation = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val manifest = inference.property.toManifest() + val focused = UsvmPropertySearcher(scene).searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference, + relation, + ) + + val refutation = refute(inference, relation) + val candidate = refutation.captureWitness() + val native = backend.confirmWitness(inference.property, candidate, CONFIGURATION) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, focused.search?.status) + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(EtsMappingStatus.EXACT, refutation.binding.status) + assertEquals(WitnessRole.HYPOTHESIS, candidate.target.role) + assertEquals(ObservationBuildStatus.UNVERIFIED, refutation.inference.buildStatus) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.HOLDS, native.reducedReplay?.outcome) + assertEquals(refutation.inputs, native.candidate.inputs) + assertEquals(candidate.target.binding, native.contextualRefutations.single().binding) + } + + @Test + fun `an original oracle violation has priority over a confirmed entry hypothesis refutation`() { + val cases = listOf("ordered" to WitnessOracleOutcome.FALSE, "throwing" to WitnessOracleOutcome.THREW) + for ((predicate, outcome) in cases) { + val inference = observe(predicate = predicate) + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + val refutation = refute(inference, order) + val native = backend.confirmWitness(inference.property, refutation.captureWitness(), CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, native.status, native.diagnostic) + assertEquals(outcome, native.originalReplay?.outcome) + assertTrue(assertNotNull(native.originalReplay).targetMatched) + assertTrue(native.contextualRefutations.isNotEmpty()) + } + } + + @Test + fun `the complete original precondition can reject every proposed refutation`() { + val inference = observe(predicate = "reflexive", precondition = "ordered") + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + val refutation = refute(inference, order) + + assertEquals(UsvmEntryRefutationStatus.PRECONDITION_REJECTED, refutation.status) + assertNull(refutation.inputs) + } + + @Test + fun `a runtime bound inside original admission remains unsupported rather than absence of refutations`() { + val inference = observe(predicate = "reflexive", precondition = "sparseAdmission") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + + val refutation = refute(inference, equality) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, refutation.status) + assertNull(refutation.inputs) + assertTrue(refutation.diagnostics.any { it.code == "usvm.runtime.array-index-growth" }) + } + + @Test + fun `same entry equality can be refuted by NaN while the original property still holds`() { + val points = listOf(LEFT, RIGHT.copy(inputIndex = 0)) + val inference = observe(predicate = "always", leftDomain = NumberDomain(), points = points, seed = 2) + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + + val refutation = refute(inference, equality) + val native = backend.confirmWitness(inference.property, refutation.captureWitness(), CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + val first = assertNotNull(refutation.inputs).first() as JsConcreteValue.Number + assertTrue(first.toDouble().isNaN()) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + } + + @Test + fun `stale observation sources cannot activate a challenge and stale native sources preserve the candidate`() { + val inference = observe(predicate = "reflexive") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val stale = listOf(PropertyObservationSource(module = MODULE, sha256 = "0".repeat(n = 64))) + + val staleBinding = refute(inference.copy(sources = stale), equality) + val refutation = refute(inference, equality) + val candidate = refutation.captureWitness().copy(sources = stale) + val native = backend.confirmWitness(inference.property, candidate, CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, staleBinding.status) + assertNull(staleBinding.inputs) + assertEquals(WitnessReplayStatus.SOURCE_MISMATCH, native.status) + assertEquals(refutation.inputs, native.candidate.inputs) + } + + @Test + fun `a timed out auxiliary search is not an exhausted relation`() { + val inference = observe(predicate = "reflexive") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val limited = UsvmEntryRelationRefuter( + scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = Duration.ZERO), + ) + val manifest = inference.property.toManifest() + + val refutation = limited.refute(manifest, mapper.map(manifest), CONCRETE, inference, equality) + + assertEquals(UsvmEntryRefutationStatus.TIMEOUT, refutation.status) + assertTrue(refutation.timedOut) + assertNull(refutation.inputs) + } + + @Test + fun `swapped positional slots cannot activate an entry auxiliary target`() { + val inference = observe(predicate = "reflexive") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val manifest = inference.property.toManifest() + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + val inputs = target.bindings.inputs + val swapped = inputs.mapIndexed { index, input -> input.copy(stackSlot = inputs[1 - index].stackSlot) } + val changedTarget = target.copy(bindings = target.bindings.copy(inputs = swapped)) + val changed = mapping.copy(predicate = mapping.predicate.copy(targets = listOf(changedTarget))) + + val refutation = UsvmEntryRelationRefuter(scene).refute(manifest, changed, CONCRETE, inference, equality) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, refutation.status) + assertEquals("usvm.entry-relation.slots-mismatch", refutation.binding.diagnostics.single().code) + assertNull(refutation.inputs) + } + + private fun refute(inference: ScalarRelationInference, relation: ScalarRelation): UsvmEntryRelationRefutation { + val manifest = inference.property.toManifest() + + return UsvmEntryRelationRefuter(scene).refute(manifest, mapper.map(manifest), CONCRETE, inference, relation) + } + + private fun observe( + predicate: String, + precondition: String? = null, + leftDomain: PropertyDomain = IntegerDomain(min = 0, max = 2), + points: List = listOf(LEFT, RIGHT), + seed: Int = 1, + ): ScalarRelationInference { + val property = PropertyDefinition( + id = PropertyId("entry.auxiliary"), + inputs = listOf( + PropertyInput(name = "left", domain = leftDomain), + PropertyInput(name = "right", domain = IntegerDomain(min = 0, max = 2)), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = predicate), + precondition = precondition?.let { TypeScriptEntryPoint(module = MODULE, exportName = it) }, + assertions = listOf( + PropertyAssertion( + id = "original", + source = CALL, + testedCall = CALL, + operands = points.map { PropertyOperand(id = it.operandId, source = it.source) }, + ), + ), + ) + + val result = backend.run( + property, + PropertyRunConfiguration( + seed = seed, + numRuns = 2, + observationRequest = PropertyObservationRequest(points = points, sources = sources), + ), + ) + + return inferScalarRelations( + property, + assertNotNull(result.observations), + listOf(ScalarObservationPair(points[0], points[1])) + ) + } + + companion object { + private const val MODULE = "properties/inference/EntryRelations.ts" + private val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + private val LEFT = PropertyObservationPoint( + id = "left", + assertionId = "original", + operandId = "left", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + private val RIGHT = LEFT.copy(id = "right", operandId = "right", inputIndex = 1) + private val CONCRETE = ProjectionCapability(level = ProjectionLevel.EXACT) + private val CONFIGURATION = WitnessReplayConfiguration(timeoutMillis = 15_000, validationReserveMillis = 3_000) + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private lateinit var sources: List + + @JvmStatic + @BeforeAll + fun loadFixture() { + val root = testResourcesRoot() + val source = root.resolve(MODULE) + val bytes = Files.readAllBytes(source) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) } + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)) + scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + mapper = PropertyEtsMapper(scene, sourceRoots = listOf(root, source.parent)) + } + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt new file mode 100644 index 0000000000..bb1a84150b --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt @@ -0,0 +1,336 @@ +package org.usvm.ts.pbt.inference + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.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.PropertyDomain +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.observation.ObservationBuildStatus +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 org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import org.usvm.ts.pbt.usvm.UsvmPropertyViolationTarget +import java.nio.file.Files +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class EntryRelationSearchTest { + @Test + fun `different native input observations guide the same independent original oracle`() { + val property = property(exportName = "independent") + val forward = capture(property, seed = 10) + val backward = capture(property, seed = 6, pair = ScalarObservationPair(RIGHT, LEFT)) + val manifest = property.toManifest() + + for ((inference, expectedRight) in listOf(forward to 0.0, backward to 2.0)) { + val relation = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val focused = searcher.searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference, + relation, + ) + + assertEquals(ScalarRelationStatus.SAMPLED, relation.status) + assertEquals(EtsMappingStatus.EXACT, focused.binding.status, focused.binding.diagnostics.toString()) + assertEquals(ObservationBuildStatus.UNVERIFIED, focused.inference.buildStatus) + val result = assertNotNull(focused.search, focused.binding.diagnostics.toString()) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + val inputs = assertNotNull(result.inputs) + val values = inputs.map { (it as JsConcreteValue.Number).toDouble() } + assertEquals(listOf(1.0, expectedRight), values) + val bound = focused.binding.targets.single() + assertEquals(bound.leftInputIndex + 1, bound.left.stackSlot) + assertEquals(bound.rightInputIndex + 1, bound.right.stackSlot) + + val replay = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())).run( + property, + PropertyRunConfiguration(seed = 1, numRuns = 1, examples = listOf(inputs)), + ) + + assertEquals(PropertyRunStatus.FAILURE, replay.status) + } + } + + @Test + fun `refuting an input equality is not itself an original property failure`() { + val property = property(exportName = "reflexive") + val inference = capture(property) + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val manifest = property.toManifest() + + val focused = searcher.searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference, + equality, + ) + val unfocused = searcher.search(manifest, mapper.map(manifest), CONCRETE) + + assertEquals(ScalarRelationStatus.SAMPLED, equality.status) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, focused.search?.status) + assertNull(focused.search?.inputs) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, unfocused.status) + assertEquals(inference.runId, focused.inference.runId) + } + + @Test + fun `domain implied entry order is retained for audit and cannot activate focused search`() { + val property = property( + exportName = "reflexive", + leftDomain = IntegerDomain(min = 0, max = 1), + rightDomain = IntegerDomain(min = 2, max = 3), + ) + val inference = capture(property) + val order = inference.domainImpliedRelations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val manifest = property.toManifest() + + val focused = searcher.searchFocusedOnEntryRelation(manifest, mapper.map(manifest), CONCRETE, inference, order) + + assertEquals(ScalarRelationStatus.SAMPLED, order.status) + assertEquals(2, order.distinctGenerationInputs.size) + assertTrue(order.evidence.all { it.holds }) + assertTrue(inference.relations.none { it.template == ScalarRelationTemplate.LESS_OR_EQUAL }) + assertEquals(EtsMappingStatus.UNSUPPORTED, focused.binding.status) + assertNull(focused.search) + } + + @Test + fun `the original precondition still rejects a focused hypothesis refutation`() { + val property = property().copy(precondition = TypeScriptEntryPoint(module = MODULE, exportName = "ordered")) + val inference = capture(property) + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val manifest = property.toManifest() + + val focused = searcher.searchFocusedOnEntryRelation(manifest, mapper.map(manifest), CONCRETE, inference, order) + + assertEquals(ScalarRelationStatus.SAMPLED, order.status) + assertEquals(UsvmPropertySearchStatus.PRECONDITION_REJECTED, focused.search?.status) + assertNull(focused.search?.inputs) + } + + @Test + fun `focused comparison uses JavaScript NaN semantics without replacing the original oracle`() { + val domain = NumberDomain() + val property = property( + exportName = "reflexive", + leftDomain = domain, + rightDomain = IntegerDomain(min = 1, max = 1), + ) + val inference = capture(property, seed = 2) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val manifest = property.toManifest() + + val focused = searcher.searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference, + relation, + ) + + assertEquals(ScalarRelationStatus.SAMPLED, relation.status) + val result = assertNotNull(focused.search) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + val left = assertNotNull(result.inputs).first() as JsConcreteValue.Number + assertTrue(left.toDouble().isNaN()) + } + + @Test + fun `changed support precondition source and ordinary argument labels cannot activate focus`() { + val property = property() + val inference = capture(property) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val manifest = property.toManifest() + val changed = listOf( + manifest.copy(inputs = manifest.inputs.map { it.copy(domain = IntegerDomain(min = -1, max = 1)) }), + manifest.copy(precondition = TypeScriptEntryPoint(module = MODULE, exportName = "nonNegative")), + ) + + for (other in changed) { + val result = searcher.searchFocusedOnEntryRelation(other, mapper.map(other), CONCRETE, inference, relation) + + assertEquals(EtsMappingStatus.UNSUPPORTED, result.binding.status) + assertNull(result.search) + } + + val ordinary = relation.copy(pair = relation.pair.copy(left = LEFT.copy(kind = ObservationPointKind.ARGUMENT))) + val staleSource = PropertyObservationSource(module = MODULE, sha256 = "0".repeat(n = 64)) + val stale = inference.copy(sources = listOf(staleSource)) + val ordinaryResult = searcher.searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference.copy(relations = listOf(ordinary)), + ordinary, + ) + val staleResult = searcher.searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + stale, + relation, + ) + + assertNull(ordinaryResult.search) + assertNull(staleResult.search) + val ordinaryDiagnostic = ordinaryResult.binding.diagnostics.single().code + val staleDiagnostic = staleResult.binding.diagnostics.single().code + assertTrue(ordinaryDiagnostic.endsWith("point-unsupported")) + assertTrue(staleDiagnostic.endsWith("source-mismatch")) + } + + @Test + fun `invalid indices mismatched snapshots nested contexts and ambiguous entries cannot guide search`() { + val property = property() + val inference = capture(property) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + val first = relation.evidence.first() + val wrongValue = first.left.copy(value = first.left.value.copy(value = JsConcreteValue.number(99.0))) + val nested = first.invocation.copy(parentInvocationId = 0) + val invalid = listOf( + relation.copy(pair = relation.pair.copy(left = LEFT.copy(inputIndex = 99))), + relation.copy(evidence = listOf(first.copy(left = wrongValue))), + relation.copy(evidence = listOf(first.copy(invocation = nested))), + ) + + for (candidate in invalid) { + val result = searcher.searchFocusedOnEntryRelation( + manifest, + mapping, + CONCRETE, + inference.copy(relations = listOf(candidate)), + candidate, + ) + + assertEquals(EtsMappingStatus.UNSUPPORTED, result.binding.status) + assertNull(result.search) + } + + val ambiguousPredicate = mapping.predicate.copy( + status = EtsMappingStatus.AMBIGUOUS, + diagnostics = listOf(EtsMappingDiagnostic(code = "test.ambiguous", message = "Two frontend candidates")), + ) + val ambiguousMapping = mapping.copy(predicate = ambiguousPredicate) + + val ambiguous = searcher.searchFocusedOnEntryRelation( + manifest, + ambiguousMapping, + CONCRETE, + inference, + relation, + ) + + assertEquals(EtsMappingStatus.UNSUPPORTED, ambiguous.binding.status) + assertNull(ambiguous.search) + assertEquals("usvm.entry-relation.entry-ambiguous", ambiguous.binding.diagnostics.single().code) + } + + private fun capture( + property: PropertyDefinition, + seed: Int = 1, + pair: ScalarObservationPair = ScalarObservationPair(LEFT, RIGHT), + ): ScalarRelationInference { + val result = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())).run( + property, + PropertyRunConfiguration( + seed = seed, + numRuns = 2, + observationRequest = PropertyObservationRequest(points = listOf(LEFT, RIGHT), sources = sources), + ), + ) + val observations = assertNotNull(result.observations) + + return inferScalarRelations(property, observations, listOf(pair)) + } + + private fun property( + exportName: String = "ordered", + leftDomain: PropertyDomain = IntegerDomain(min = 0, max = 2), + rightDomain: PropertyDomain = IntegerDomain(min = 0, max = 2), + ) = PropertyDefinition( + id = PropertyId("entry.relation"), + inputs = listOf( + PropertyInput(name = "left", domain = leftDomain), + PropertyInput(name = "right", domain = rightDomain), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName), + assertions = listOf( + PropertyAssertion( + id = "original", + source = CALL, + testedCall = CALL, + operands = listOf( + PropertyOperand(LEFT.operandId, LEFT.source), + PropertyOperand(RIGHT.operandId, RIGHT.source), + ), + ), + ), + ) + + companion object { + private const val MODULE = "properties/inference/EntryRelations.ts" + private val CALL = PropertySourcePoint(module = MODULE, line = 2, column = 5) + private val LEFT = PropertyObservationPoint( + id = "left", + assertionId = "original", + operandId = "left", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + private val RIGHT = LEFT.copy(id = "right", operandId = "right", inputIndex = 1) + private val CONCRETE = ProjectionCapability(level = ProjectionLevel.EXACT) + private lateinit var sources: List + private lateinit var mapper: PropertyEtsMapper + private lateinit var searcher: UsvmPropertySearcher + + @JvmStatic + @BeforeAll + fun loadFixture() { + val root = testResourcesRoot() + val source = root.resolve(MODULE) + val bytes = Files.readAllBytes(source) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)) + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(root, source.parent)) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt new file mode 100644 index 0000000000..f43f7245ef --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/ScalarRelationCaptureTest.kt @@ -0,0 +1,102 @@ +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.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.model.IntegerDomain +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.PropertySourceIdentity +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationBuildStatus +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.assertNotNull +import kotlin.test.assertTrue + +class ScalarRelationCaptureTest { + @Test + fun `original FastCheck generation observations supply a numeric order hypothesis`() { + val source = testResourcesRoot().resolve(MODULE) + val hash = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(source)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val callSite = PropertySourcePoint(module = MODULE, line = 3, column = 43) + val input = PropertyObservationPoint( + id = "input", + assertionId = "non-negative", + operandId = "input", + source = PropertySourcePoint(module = MODULE, line = 2, column = 11), + callSite = callSite, + kind = ObservationPointKind.ARGUMENT, + inputIndex = 0, + ) + val result = PropertyObservationPoint( + id = "result", + assertionId = "non-negative", + operandId = "result", + source = PropertySourcePoint(module = MODULE, line = 3, column = 11), + callSite = callSite, + kind = ObservationPointKind.RETURN, + ) + val property = PropertyDefinition( + id = PropertyId("test.magnitude"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -1, max = 0))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "nonNegativeMagnitude"), + assertions = listOf( + PropertyAssertion( + id = "non-negative", + source = PropertySourcePoint(module = MODULE, line = 5, column = 5), + testedCall = callSite, + operands = listOf( + PropertyOperand(id = input.operandId, source = input.source), + PropertyOperand(id = result.operandId, source = result.source), + ), + ), + ), + sourceIdentity = PropertySourceIdentity( + sourceSha256 = hash, + buildSha256 = hash, + buildScope = "direct TypeScript source; executable build unverified", + ), + ) + val sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)) + val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + val run = backend.run( + property, + PropertyRunConfiguration( + seed = 42, + numRuns = 16, + observationRequest = PropertyObservationRequest(points = listOf(input, result), sources = sources), + ), + ) + val observations = assertNotNull(run.observations) + val inference = inferScalarRelations(property, observations, listOf(ScalarObservationPair(input, result))) + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + assertEquals(PropertyRunStatus.SUCCESS, run.status) + assertEquals(sources, inference.sources) + assertEquals(ObservationBuildStatus.UNVERIFIED, inference.buildStatus) + assertEquals(ScalarRelationStatus.REFUTED, equality.status) + assertEquals(ScalarRelationStatus.SAMPLED, order.status) + assertEquals(2, order.distinctGenerationInputs.size) + assertTrue(order.evidence.all { it.holds }) + } + + private companion object { + const val MODULE = "properties/inference/ScalarRelations.ts" + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts new file mode 100644 index 0000000000..c2a7417fc0 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts @@ -0,0 +1,35 @@ +export function ordered(left: number, right: number): boolean { + return left <= right; +} + +export function reflexive(left: number, right: number): boolean { + return left === left; +} + +export function nonNegative(left: number, right: number): boolean { + return left >= 0; +} + +export function independent(left: number, right: number): boolean { + return left !== 1; +} + +export function always(left: number, right: number): boolean { + return true; +} + +export function sparseAdmission(left: number, right: number): boolean { + const cache: number[] = []; + cache[9] = left; + return right === right; +} + +export function entryMutation(left: number, right: number): boolean { + left = right; + return left === right; +} + +export function throwing(left: number, right: number): boolean { + if (left > right) throw new Error('original fault'); + return true; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts new file mode 100644 index 0000000000..a98ee3e085 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/inference/ScalarRelations.ts @@ -0,0 +1,12 @@ +export function nonNegativeMagnitude(value: number): boolean { + const input = observePoint('input', value); + const result = observePoint('result', Math.abs(input)); + + return result >= 0; +} + +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/DslNumericLocalWitnessCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/DslNumericLocalWitnessCapture.kt new file mode 100644 index 0000000000..dc356fe31f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/DslNumericLocalWitnessCapture.kt @@ -0,0 +1,44 @@ +package org.usvm.ts.pbt.backend + +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmDslNumericLocalRefutation +import org.usvm.ts.pbt.usvm.UsvmRelationRefutationStatus + +/** Captures the original input and compiler point; executable build identity remains unverified. */ +fun UsvmDslNumericLocalRefutation.captureWitness( + sources: List = inference.sources, +): ExternalWitnessCandidate { + val reached = status == UsvmRelationRefutationStatus.REFUTATION_REACHED || + status == UsvmRelationRefutationStatus.FAILED_INPUT_RESOLUTION + require(reached) { "A numeric local witness requires a reached auxiliary target" } + + val selected = binding.targets.single() + val relation = selected.relation + val left = relation.pair.left + val right = relation.pair.right + val targetId = "${left.assertionId}:${left.id}:${relation.template}:${right.id}" + val property = inference.property + val revision = property.witnessManifestSha256() + val target = WitnessTarget( + id = targetId, + role = WitnessRole.HYPOTHESIS, + binding = WitnessBinding( + pointId = targetId, + contextId = WitnessDslNumericLocalRelation.CONTEXT_ID, + revision = revision, + ), + dslNumericLocalRelation = WitnessDslNumericLocalRelation( + compiler = selected.compiler, + inputIndex = selected.inputIndex, + resultIsLeft = selected.resultIsLeft, + template = relation.template, + ), + ) + + return property.captureWitness( + inputs = inputs, + target = target, + sources = sources, + provenance = "usvm:dsl-local-refutation:${inference.runId}:${inference.buildStatus}:$status", + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt new file mode 100644 index 0000000000..e525371c29 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt @@ -0,0 +1,39 @@ +package org.usvm.ts.pbt.backend + +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmEntryRefutationStatus +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefutation + +/** The exact entry transport binding is independent of the still-unverified executable body. */ +fun UsvmEntryRelationRefutation.captureWitness( + sources: List = inference.sources, +): ExternalWitnessCandidate { + val reached = status == UsvmEntryRefutationStatus.REFUTATION_REACHED || + status == UsvmEntryRefutationStatus.FAILED_INPUT_RESOLUTION + require(reached) { "An entry relation witness requires a reached auxiliary target" } + + val selected = binding.targets.single() + val relation = selected.relation + val left = relation.pair.left + val right = relation.pair.right + val targetId = "${left.assertionId}:${left.id}:${relation.template}:${right.id}" + val property = inference.property + val revision = property.witnessManifestSha256() + val target = WitnessTarget( + id = targetId, + role = WitnessRole.HYPOTHESIS, + binding = WitnessBinding( + pointId = targetId, + contextId = WitnessEntryRelation.CONTEXT_ID, + revision = revision, + ), + entryRelation = WitnessEntryRelation(selected.leftInputIndex, selected.rightInputIndex, relation.template), + ) + + return property.captureWitness( + inputs = inputs, + target = target, + sources = sources, + provenance = "usvm:entry-refutation:${inference.runId}:${inference.buildStatus}:$status", + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt index 8600ed1326..8a44303b0a 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt @@ -1,15 +1,50 @@ package org.usvm.ts.pbt.backend import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.inference.ScalarRelationTemplate import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.CompilerNumericLocalBinding import org.usvm.ts.pbt.observation.PropertyObservationSource /** Auxiliary witnesses are useful evidence even when the complete original oracle holds. */ @Serializable enum class WitnessRole { PROPERTY, COVERAGE, HYPOTHESIS } +/** Adapter-owned comparison of two original numeric inputs, before the original callback runs. */ +@Serializable +data class WitnessEntryRelation( + val leftInputIndex: Int, + val rightInputIndex: Int, + val template: ScalarRelationTemplate, +) { + init { + require(leftInputIndex >= 0 && rightInputIndex >= 0) + } + + companion object { + const val CONTEXT_ID = "original-entry" + } +} + +/** Explicit companion callback, comparing one stored numeric result with an original input snapshot. */ +@Serializable +data class WitnessDslNumericLocalRelation( + val compiler: CompilerNumericLocalBinding, + val inputIndex: Int, + val resultIsLeft: Boolean, + val template: ScalarRelationTemplate, +) { + init { + require(inputIndex >= 0) + } + + companion object { + const val CONTEXT_ID = "original-compiler-local" + } +} + /** Exact executable hook binding supplied by a producer, never inferred from a source line. */ @Serializable data class WitnessBinding( @@ -31,10 +66,20 @@ data class WitnessTarget( val role: WitnessRole = WitnessRole.PROPERTY, val binding: WitnessBinding? = null, val expectedOutcome: WitnessOracleOutcome? = null, + val entryRelation: WitnessEntryRelation? = null, + val dslNumericLocalRelation: WitnessDslNumericLocalRelation? = null, ) { init { require(id.isNotBlank()) require(role == WitnessRole.PROPERTY || binding != null) + if (entryRelation != null) { + require(role == WitnessRole.HYPOTHESIS) + require(binding?.contextId == WitnessEntryRelation.CONTEXT_ID && binding.occurrence == 0) + } + if (dslNumericLocalRelation != null) { + require(entryRelation == null && role == WitnessRole.HYPOTHESIS) + require(binding?.contextId == WitnessDslNumericLocalRelation.CONTEXT_ID && binding.occurrence == 0) + } require( expectedOutcome == null || expectedOutcome == WitnessOracleOutcome.FALSE || expectedOutcome == WitnessOracleOutcome.THREW 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..32f503d415 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt @@ -0,0 +1,124 @@ +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) +} + +internal fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try { + val capture = requireNotNull(numericLocalCapture) + val regenerated = PropertyTypeScriptCompiler().compile( + program, + generatedModule = definition.predicate.module, + resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } }, + numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId), + ) + + definition == regenerated.definition && typeScript == regenerated.typeScript && + numericLocalCapture == regenerated.numericLocalCapture +} catch (_: IllegalArgumentException) { + false +} 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..5872d67026 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,9 @@ data class CompiledDslProperty( val definition: PropertyDefinition, val typeScript: String, val expressionLocations: Map>, + val numericLocalCapture: CompiledDslNumericLocalCapture? = null, + /** Retains import decisions so a point consumer can reproduce this compiler output from the original program. */ + val resolvedModules: Map = emptyMap(), ) /** One expression occurrence in generated TypeScript; columns are one-based UTF-16 and end-exclusive. */ @@ -34,7 +37,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,17 +55,27 @@ 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 resolvedModules = 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) functions.forEach { (function, alias) -> val path = resolveModule(function.module) + val previous = resolvedModules.putIfAbsent(function.module, path) + require(capture == null || previous == null || previous == path) { + "A captured program requires one stable import resolution per module" + } appendLine("import { ${function.exportName} as $alias } from ${quote(path)};") } val parameters = program.inputs.joinToString { input -> @@ -84,7 +106,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, resolvedModules.toMap()) } private fun emitPredicate(parameters: String, diagnostic: Boolean) { @@ -94,14 +124,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 +175,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 +193,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/DomainImpliedScalarRelation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelation.kt new file mode 100644 index 0000000000..e403866d39 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelation.kt @@ -0,0 +1,90 @@ +package org.usvm.ts.pbt.inference + +import org.usvm.ts.pbt.model.ConstantDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.observation.ObservationPointKind + +/** Only adapter-owned entry points can turn declared input support into a fact about an observed value. */ +internal fun ScalarRelation.isDomainImplied(property: PropertyDefinition): Boolean { + if (status != ScalarRelationStatus.SAMPLED || evidence.isEmpty()) return false + + val points = listOf(pair.left, pair.right) + val entryArguments = points.all { point -> point.kind == ObservationPointKind.ENTRY_ARGUMENT } + if (!entryArguments) return false + + val leftIndex = pair.left.inputIndex ?: return false + val rightIndex = pair.right.inputIndex ?: return false + val leftDomain = property.inputs.getOrNull(leftIndex)?.domain ?: return false + val rightDomain = property.inputs.getOrNull(rightIndex)?.domain ?: return false + val leftBounds = leftDomain.numericBounds() ?: return false + val rightBounds = rightDomain.numericBounds() ?: return false + val snapshotsMatch = evidence.all { sample -> + val input = sample.invocation.input.value as? JsConcreteValue.Array + val left = sample.left.value.value + val right = sample.right.value.value + + val identitiesMatch = sample.left.matches(pair.left) && sample.right.matches(pair.right) + val originalInputsMatch = left == input?.elements?.getOrNull(leftIndex) && + right == input?.elements?.getOrNull(rightIndex) + val leftInDomain = left != null && left in leftDomain + val rightInDomain = right != null && right in rightDomain + + identitiesMatch && originalInputsMatch && leftInDomain && rightInDomain + } + if (!snapshotsMatch) return false + + if (leftIndex == rightIndex) return true + + return when (template) { + ScalarRelationTemplate.STRICT_EQUAL -> { + leftBounds.minimum == leftBounds.maximum && rightBounds.minimum == rightBounds.maximum && + leftBounds.minimum == rightBounds.minimum + } + + ScalarRelationTemplate.LESS_OR_EQUAL -> leftBounds.maximum <= rightBounds.minimum + } +} + +private data class NumericBounds(val minimum: Double, val maximum: Double) + +/** Bounds are useful only when every allowed value is a number and NaN is excluded. */ +private fun PropertyDomain.numericBounds(): NumericBounds? = when (this) { + is IntegerDomain -> { + val minimum = min.toDouble() + val maximum = max.toDouble() + + if (min <= max) NumericBounds(minimum, maximum) else null + } + + is NumberDomain -> { + val validEncoding = min.hasValidEncoding() && max.hasValidEncoding() + if (allowNaN || !validEncoding) { + null + } else { + val minimum = min.toDouble() + val maximum = max.toDouble() + val ordered = !minimum.isNaN() && !maximum.isNaN() && minimum <= maximum + + if (ordered) NumericBounds(minimum, maximum) else null + } + } + + is ConstantDomain -> { + val number = value as? JsConcreteValue.Number + val validEncoding = number?.number?.hasValidEncoding() == true + if (!validEncoding) { + null + } else { + val scalar = requireNotNull(number).toDouble() + + if (scalar.isNaN()) null else NumericBounds(scalar, scalar) + } + } + + else -> null +} 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 new file mode 100644 index 0000000000..588c4e499c --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt @@ -0,0 +1,220 @@ +package org.usvm.ts.pbt.inference + +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +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.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyInvocationObservation +import org.usvm.ts.pbt.observation.PropertyObservationArtifact +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyPointEvent + +/** + * Evaluates only explicitly selected assertion operand pairs, in selection order. + * + * At least two distinct original admitted generation inputs and two observed value pairs are + * required for sample agreement. Replay, shrinking and solver evidence can refute a relation, + * but cannot increase independent support. Repeated points and nested contexts are unsupported. + * + * Only selected module hashes are available for provenance; a declared predicate source hash + * is checked when present. Executable build status is carried through without promotion. + * + * Sampled relations already implied by declared numeric input domains are separated only for + * adapter-owned entry arguments. Arbitrary point labels never establish original-input identity. + * Original formulas and preconditions are not inspected; retained relations remain empirical. + */ +fun inferScalarRelations( + property: PropertyDefinition, + observations: PropertyObservationArtifact, + pairs: List, + maxPairs: Int = 16, + maxInvocations: Int = 64, +): ScalarRelationInference { + require(maxPairs > 0) { "maxPairs must be positive" } + require(maxInvocations > 0) { "maxInvocations must be positive" } + require(property.id == observations.propertyId) { "Observation property does not match the selected property" } + + val distinctPairs = pairs.distinct() + val selectedPairs = distinctPairs.take(maxPairs) + val invocations = observations.invocations.take(maxInvocations) + val omittedInvocations = observations.invocations.size - invocations.size + val relations = selectedPairs.flatMap { pair -> + evaluatePair(property, observations, pair, invocations, omittedInvocations) + } + + val (domainImplied, retained) = relations.partition { relation -> relation.isDomainImplied(property) } + + return ScalarRelationInference( + propertyId = property.id, + runId = observations.runId, + sources = observations.verifiedSources, + buildStatus = observations.buildStatus, + relations = retained, + omittedPairs = distinctPairs.size - selectedPairs.size, + omittedInvocations = omittedInvocations, + droppedInvocations = observations.droppedInvocations, + droppedPoints = observations.droppedPoints, + property = property, + domainImpliedRelations = domainImplied, + ) +} + +private fun evaluatePair( + property: PropertyDefinition, + observations: PropertyObservationArtifact, + pair: ScalarObservationPair, + invocations: List, + omittedInvocations: Int, +): List { + val limitations = linkedSetOf() + val validPair = pair.isAssertionPair(property) + val verifiedModules = observations.verifiedSources.map { it.module }.toSet() + val selectedModules = setOf(pair.left.source.module, pair.right.source.module, pair.left.callSite.module) + val expectedSourceHash = property.sourceIdentity?.sourceSha256 + val predicateSource = observations.verifiedSources.singleOrNull { it.module == property.predicate.module } + val propertySourceMatches = expectedSourceHash == null || predicateSource?.sha256 == expectedSourceHash + val sourcesPresent = verifiedModules.containsAll(selectedModules) && propertySourceMatches + + if (!validPair) limitations += ScalarRelationLimitation.INVALID_PAIR + if (!sourcesPresent) limitations += ScalarRelationLimitation.SOURCE_MISMATCH + if (omittedInvocations > 0) limitations += ScalarRelationLimitation.INVOCATION_LIMIT + if (observations.droppedInvocations > 0 || observations.droppedPoints > 0) { + limitations += ScalarRelationLimitation.INCOMPLETE_CAPTURE + } + + val matched = if (validPair && sourcesPresent) { + invocations.mapNotNull { invocation -> numericPair(invocation, pair, limitations) } + } else { + emptyList() + } + val generationEvidence = matched.filter { (invocation, _, _) -> invocation.isIndependentGeneration() } + val distinctInputs = generationEvidence.mapNotNull { (invocation, _, _) -> invocation.input.value }.toSet() + val distinctValues = generationEvidence.map { (_, left, right) -> + left.numericSupportValue() to right.numericSupportValue() + }.toSet() + + if (distinctInputs.size < MINIMUM_DISTINCT_SUPPORT) { + limitations += ScalarRelationLimitation.INSUFFICIENT_DISTINCT_INPUTS + } + if (generationEvidence.isNotEmpty() && distinctValues.size < MINIMUM_DISTINCT_SUPPORT) { + limitations += ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR + } + + return ScalarRelationTemplate.entries.map { template -> + val evidence = matched.map { (invocation, left, right) -> + val leftNumber = (left.value.value as JsConcreteValue.Number).toDouble() + val rightNumber = (right.value.value as JsConcreteValue.Number).toDouble() + val holds = when (template) { + ScalarRelationTemplate.STRICT_EQUAL -> leftNumber == rightNumber + ScalarRelationTemplate.LESS_OR_EQUAL -> leftNumber <= rightNumber + } + + ScalarRelationEvidence(invocation, left, right, holds) + } + val refuted = evidence.any { !it.holds } + val unsupported = limitations.any { it in UNSUPPORTED_LIMITATIONS } + val status = when { + refuted -> ScalarRelationStatus.REFUTED + matched.isEmpty() && unsupported -> ScalarRelationStatus.UNSUPPORTED + limitations.isNotEmpty() -> ScalarRelationStatus.INSUFFICIENT + else -> ScalarRelationStatus.SAMPLED + } + + ScalarRelation(pair, template, status, evidence, distinctInputs, limitations.toSet()) + } +} + +private fun numericPair( + invocation: PropertyInvocationObservation, + pair: ScalarObservationPair, + limitations: MutableSet, +): Triple? { + if (invocation.admission != ObservationAdmission.ADMITTED) return null + + val complete = invocation.outcome in COMPLETE_OUTCOMES + if (!complete) { + limitations += ScalarRelationLimitation.INCOMPLETE_INVOCATION + return null + } + val supportedContext = invocation.parentInvocationId == null && invocation.callSite == pair.left.callSite + if (!supportedContext) { + limitations += ScalarRelationLimitation.UNSUPPORTED_CONTEXT + return null + } + + val leftEvents = invocation.points.filter { it.pointId == pair.left.id } + val rightEvents = invocation.points.filter { it.pointId == pair.right.id } + if (leftEvents.isEmpty() || rightEvents.isEmpty()) { + limitations += ScalarRelationLimitation.MISSING_POINT + return null + } + if (leftEvents.size != 1 || rightEvents.size != 1) { + limitations += ScalarRelationLimitation.REPEATED_POINT + return null + } + + val left = leftEvents.single() + val right = rightEvents.single() + val identitiesMatch = left.matches(pair.left) && right.matches(pair.right) + if (!identitiesMatch) { + limitations += ScalarRelationLimitation.POINT_IDENTITY_MISMATCH + return null + } + val numeric = left.isNumber() && right.isNumber() + if (!numeric) { + limitations += ScalarRelationLimitation.UNSUPPORTED_VALUE + return null + } + + return Triple(invocation, left, right) +} + +private fun ScalarObservationPair.isAssertionPair(property: PropertyDefinition): Boolean { + if (left.id == right.id || left.operandId == right.operandId) return false + if (left.assertionId != right.assertionId || left.callSite != right.callSite) return false + + val assertion = property.assertions.singleOrNull { it.id == left.assertionId } ?: return false + val leftOperand = assertion.operands.singleOrNull { it.id == left.operandId } + val rightOperand = assertion.operands.singleOrNull { it.id == right.operandId } + + return assertion.testedCall == left.callSite && + leftOperand?.source == left.source && rightOperand?.source == right.source +} + +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 && + compilerLocal == point.compilerLocal + +private fun PropertyPointEvent.isNumber(): Boolean { + val number = value.value as? JsConcreteValue.Number ?: return false + + return value.status == ObservationValueStatus.CAPTURED && number.number.hasValidEncoding() +} + +private fun PropertyPointEvent.numericSupportValue(): Double { + val number = (value.value as JsConcreteValue.Number).toDouble() + + // Strict numeric equality treats both signed zeros as the same value. + return if (number == 0.0) 0.0 else number +} + +private fun PropertyInvocationObservation.isIndependentGeneration(): Boolean = + origin == ObservationOrigin.FAST_CHECK && phase == ObservationPhase.GENERATION && + input.status == ObservationValueStatus.CAPTURED && input.value != null + +private const val MINIMUM_DISTINCT_SUPPORT = 2 +private val COMPLETE_OUTCOMES = setOf(ObservationOutcome.HOLDS, ObservationOutcome.FALSE, ObservationOutcome.THREW) + +private val UNSUPPORTED_LIMITATIONS = setOf( + ScalarRelationLimitation.INVALID_PAIR, + ScalarRelationLimitation.SOURCE_MISMATCH, + ScalarRelationLimitation.MISSING_POINT, + ScalarRelationLimitation.REPEATED_POINT, + ScalarRelationLimitation.POINT_IDENTITY_MISMATCH, + ScalarRelationLimitation.UNSUPPORTED_VALUE, + ScalarRelationLimitation.UNSUPPORTED_CONTEXT, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt new file mode 100644 index 0000000000..b36d5f8b0f --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/ScalarRelation.kt @@ -0,0 +1,82 @@ +package org.usvm.ts.pbt.inference + +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.ObservationBuildStatus +import org.usvm.ts.pbt.observation.PropertyInvocationObservation +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyPointEvent + +/** An explicitly selected pair of assertion operands, each evaluated once per invocation. */ +data class ScalarObservationPair( + val left: PropertyObservationPoint, + val right: PropertyObservationPoint, +) + +/** Numeric JavaScript comparisons; no mathematical-real or coercing comparison is inferred. */ +@Serializable +enum class ScalarRelationTemplate { + STRICT_EQUAL, + LESS_OR_EQUAL, +} + +/** Sample agreement is empirical evidence, never an invariant or permission to prune a path. */ +enum class ScalarRelationStatus { + SAMPLED, + REFUTED, + INSUFFICIENT, + UNSUPPORTED, +} + +/** Reasons an invocation or selection cannot supply complete numeric evidence. */ +enum class ScalarRelationLimitation { + INVALID_PAIR, + SOURCE_MISMATCH, + MISSING_POINT, + REPEATED_POINT, + POINT_IDENTITY_MISMATCH, + UNSUPPORTED_VALUE, + UNSUPPORTED_CONTEXT, + INCOMPLETE_INVOCATION, + INSUFFICIENT_DISTINCT_INPUTS, + CONSTANT_OBSERVED_PAIR, + INVOCATION_LIMIT, + INCOMPLETE_CAPTURE, +} + +/** Exact same-invocation point values, retaining origin, phase, input and event identities. */ +data class ScalarRelationEvidence( + val invocation: PropertyInvocationObservation, + val left: PropertyPointEvent, + val right: PropertyPointEvent, + val holds: Boolean, +) + +/** Evaluation of one template for one selected pair, including every observed contradiction. */ +data class ScalarRelation( + val pair: ScalarObservationPair, + val template: ScalarRelationTemplate, + val status: ScalarRelationStatus, + val evidence: List, + val distinctGenerationInputs: Set, + val limitations: Set, +) + +/** Bounded, property-scoped results preserving selected-source and executable-build provenance. */ +data class ScalarRelationInference( + val propertyId: PropertyId, + val runId: String, + val sources: List, + val buildStatus: ObservationBuildStatus, + val relations: List, + val omittedPairs: Int, + val omittedInvocations: Int, + val droppedInvocations: Int, + val droppedPoints: Int, + val property: PropertyDefinition, + /** Sampled entry relations already implied by declared numeric input support, retained for audit. */ + val domainImpliedRelations: List = emptyList(), +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt new file mode 100644 index 0000000000..8018e7e713 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt @@ -0,0 +1,127 @@ +package org.usvm.ts.pbt.inference + +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyExpressionTerm +import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput +import org.usvm.ts.pbt.dsl.selectNumericLocalCapture +import org.usvm.ts.pbt.observation.ObservationPointKind + +/** KNOWN_DSL_CHECK identifies a direct original check, not a proved relation or executable body. */ +enum class ScalarGuidanceRelevance { KNOWN_DSL_CHECK, UNKNOWN } + +/** Selection decisions preserve each excluded relation and its original evidence. */ +enum class ScalarGuidanceExclusionReason { + NOT_SAMPLED, + DOMAIN_IMPLIED, + TAUTOLOGY, + DUPLICATE, + ORIGINAL_CHECK, + CANDIDATE_LIMIT, +} + +/** An empirical candidate whose exact symbolic support still needs a consumer's binding checks. */ +data class ScalarGuidanceCandidate(val relation: ScalarRelation, val relevance: ScalarGuidanceRelevance) + +/** An unselected relation; exclusion never removes it from the original inference. */ +data class ScalarGuidanceExclusion( + val relation: ScalarRelation, + val reason: ScalarGuidanceExclusionReason, + val relevance: ScalarGuidanceRelevance, +) + +/** Retains the complete original inference, including contradictory, insufficient and excluded evidence. */ +data class ScalarGuidanceSelection( + val inference: ScalarRelationInference, + val candidates: List, + val excluded: List, +) + +/** One bounded selection before USVM. The campaign decides whether UNKNOWN relevance may guide its search. */ +fun selectScalarGuidance( + inference: ScalarRelationInference, + compiled: CompiledDslProperty? = null, + maxCandidates: Int = 16, +): ScalarGuidanceSelection { + require(maxCandidates > 0) { "maxCandidates must be positive" } + + val original = originalCheck(inference, compiled) + val candidates = mutableListOf() + val excluded = mutableListOf() + for (relation in inference.relations) { + val known = original?.contains(relation.pair) == true + val relevance = if (known) ScalarGuidanceRelevance.KNOWN_DSL_CHECK else ScalarGuidanceRelevance.UNKNOWN + val duplicate = candidates.any { candidate -> candidate.relation.sameComparison(relation) } + val sampled = relation.status == ScalarRelationStatus.SAMPLED && relation.limitations.isEmpty() + val restatesOriginal = known && original?.implies(relation) == true + val reason = when { + !sampled -> ScalarGuidanceExclusionReason.NOT_SAMPLED + restatesOriginal -> ScalarGuidanceExclusionReason.ORIGINAL_CHECK + duplicate -> ScalarGuidanceExclusionReason.DUPLICATE + candidates.size >= maxCandidates -> ScalarGuidanceExclusionReason.CANDIDATE_LIMIT + else -> null + } + + if (reason == null) { + candidates += ScalarGuidanceCandidate(relation, relevance) + } else { + excluded += ScalarGuidanceExclusion(relation, reason, relevance) + } + } + for (relation in inference.domainImpliedRelations) { + val sameOriginalInput = relation.pair.left.kind == ObservationPointKind.ENTRY_ARGUMENT && + relation.pair.right.kind == ObservationPointKind.ENTRY_ARGUMENT && + relation.pair.left.inputIndex != null && relation.pair.left.inputIndex == relation.pair.right.inputIndex + val reason = if (sameOriginalInput) { + ScalarGuidanceExclusionReason.TAUTOLOGY + } else { + ScalarGuidanceExclusionReason.DOMAIN_IMPLIED + } + excluded += ScalarGuidanceExclusion(relation, reason, relevance = ScalarGuidanceRelevance.UNKNOWN) + } + + return ScalarGuidanceSelection(inference, candidates, excluded) +} + +private data class OriginalScalarCheck(val pair: ScalarObservationPair, val operator: String) { + fun contains(candidate: ScalarObservationPair): Boolean = candidate == pair || + candidate.left == pair.right && candidate.right == pair.left + + fun implies(relation: ScalarRelation): Boolean = operator == "===" || + operator == "<=" && relation.template == ScalarRelationTemplate.LESS_OR_EQUAL && relation.pair == pair +} + +private fun originalCheck( + inference: ScalarRelationInference, + compiled: CompiledDslProperty?, +): OriginalScalarCheck? { + if (compiled == null) return null + + val sameProperty = compiled.definition == inference.property && compiled.definition.id == inference.propertyId + if (!sameProperty) return null + if (!compiled.isReproducibleCompilerOutput()) return null + + val capture = compiled.numericLocalCapture ?: return null + val source = inference.sources.singleOrNull { it.module == compiled.definition.predicate.module } + if (source?.sha256 != capture.binding.sourceSha256) return null + + val request = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId) + val selected = compiled.program.selectNumericLocalCapture(request) + val comparison = selected.check.expression.term as PropertyExpressionTerm.Operation + val pair = if (selected.resultOperandIndex == 0) { + ScalarObservationPair(capture.result, capture.input) + } else { + ScalarObservationPair(capture.input, capture.result) + } + + return OriginalScalarCheck(pair, comparison.operator) +} + +private fun ScalarRelation.sameComparison(other: ScalarRelation): Boolean { + if (template != other.template) return false + + val reversed = template == ScalarRelationTemplate.STRICT_EQUAL && + pair.left == other.pair.right && pair.right == other.pair.left + + return pair == other.pair || reversed +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt index 8787c9e4c9..dd93babb40 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt @@ -19,6 +19,7 @@ import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.TypeScriptEntryPoint import java.util.IdentityHashMap @@ -240,19 +241,6 @@ internal class EtsEntryPointResolver( return modulePaths.any(filePaths::contains) } - private fun EtsMethod.bindingParameters(): EtsBindingParameters { - // The frontend lifts arrow-function captures into one leading lexical-environment parameter. - // It is not a source argument; the interpreter recognizes the same parameter by its semantic type. - val hiddenClosure = parameters.firstOrNull()?.takeIf { parameter -> - parameter.type is EtsLexicalEnvType - } - - return EtsBindingParameters( - lexicalEnvironment = hiddenClosure, - inputs = if (hiddenClosure == null) parameters else parameters.drop(1), - ) - } - private fun EtsMethod.bindingsFor( manifest: PropertyManifest, parameters: EtsBindingParameters, @@ -261,13 +249,7 @@ internal class EtsEntryPointResolver( signature = signature.enclosingClass, typeParameters = requireNotNull(enclosingClass).typeParameters, ) - val inputBindings = manifest.inputs.zip(parameters.inputs).map { (input, parameter) -> - EtsInputBinding( - propertyInputName = input.name, - parameter = parameter, - stackSlot = parameter.index + RECEIVER_STACK_SLOTS, - ) - } + val inputBindings = inputBindingsFor(manifest.inputs) return EtsEntryPointBindings( receiver = EtsReceiverBinding( @@ -286,6 +268,27 @@ internal class EtsEntryPointResolver( } } +/** The same positional transport used by the entry mapper and consumers of its mapping artifacts. */ +internal fun EtsMethod.inputBindingsFor(inputs: List): List = + inputs.zip(bindingParameters().inputs).map { (input, parameter) -> + EtsInputBinding( + propertyInputName = input.name, + parameter = parameter, + stackSlot = parameter.index + RECEIVER_STACK_SLOTS, + ) + } + +private fun EtsMethod.bindingParameters(): EtsBindingParameters { + // The frontend lifts arrow-function captures into one leading lexical-environment parameter. + // It is not a source argument; the interpreter recognizes the same parameter by its semantic type. + val hiddenClosure = parameters.firstOrNull()?.takeIf { parameter -> parameter.type is EtsLexicalEnvType } + + return EtsBindingParameters( + lexicalEnvironment = hiddenClosure, + inputs = if (hiddenClosure == null) parameters else parameters.drop(1), + ) +} + private data class EtsBindingParameters( val lexicalEnvironment: EtsMethodParameter?, val inputs: List, 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 a32f2d6bf5..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,11 +16,16 @@ 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. */ @Serializable enum class ObservationPointKind { + /** Captured by the adapter from the original input vector before invoking user code. */ + @SerialName("entry-argument") + ENTRY_ARGUMENT, + @SerialName("argument") ARGUMENT, @@ -169,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/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt new file mode 100644 index 0000000000..236f1158e0 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt @@ -0,0 +1,239 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.inference.ScalarRelationStatus +import org.usvm.ts.pbt.inference.matches +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.EtsInputBinding +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.mapping.SourceLocationNormalizer +import org.usvm.ts.pbt.mapping.inputBindingsFor +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.observation.CompilerNumericLocalBinding +import java.io.IOException +import java.nio.file.Files +import java.nio.file.InvalidPathException +import java.nio.file.Path +import java.security.MessageDigest + +/** Exact only for this compiler-owned post-store point; executable body/build provenance stays independent. */ +data class UsvmDslNumericLocalBinding( + val method: EtsMethod, + val assignment: EtsAssignStmt, + val companionAssignment: EtsAssignStmt, + val local: EtsLocal, + val inputIndex: Int, + val input: EtsInputBinding, + val resultIsLeft: Boolean, + val compiler: CompilerNumericLocalBinding, + val relation: ScalarRelation, +) + +/** Binds the retained compiler program and a complete native receipt to one original post-store point. */ +fun bindDslNumericLocalRelation( + compiled: CompiledDslProperty, + mapping: PropertyEtsMappingArtifact, + inference: ScalarRelationInference, + relation: ScalarRelation, +): EtsMappingResult { + val sameProperty = inference.property == compiled.definition && inference.propertyId == compiled.program.id && + mapping.propertyId == compiled.definition.id + if (!sameProperty) return unbound(reason = "property-mismatch", message = "The original property changed") + + val capture = compiled.numericLocalCapture + if (capture == null || !compiled.isReproducibleCompilerOutput()) { + return unbound( + reason = "compiler-mismatch", + message = "The retained program must reproduce the compiler output" + ) + } + val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED && + relation.limitations.isEmpty() && relation.evidence.isNotEmpty() + if (!sampled) return unbound(reason = "not-sampled", message = "A complete sampled relation is required") + + val resultIsLeft = relation.pair.left == capture.result && relation.pair.right == capture.input + val resultIsRight = relation.pair.right == capture.result && relation.pair.left == capture.input + if (!resultIsLeft && !resultIsRight) { + return unbound(reason = "pair-mismatch", message = "The selected compiler result and original input must match") + } + val inputIndex = requireNotNull(capture.input.inputIndex) + val receiptsMatch = relation.evidence.all { evidence -> + val original = evidence.invocation.input.value as? JsConcreteValue.Array + val result = if (resultIsLeft) evidence.left else evidence.right + val input = if (resultIsLeft) evidence.right else evidence.left + val resultEvents = evidence.invocation.points.filter { it.pointId == capture.result.id } + val inputEvents = evidence.invocation.points.filter { it.pointId == capture.input.id } + + evidence.invocation.parentInvocationId == null && evidence.invocation.callSite == capture.result.callSite && + resultEvents.singleOrNull() == result && inputEvents.singleOrNull() == input && + result.matches(capture.result) && input.matches(capture.input) && + result.value.value is JsConcreteValue.Number && input.value.value is JsConcreteValue.Number && + input.value.value == original?.elements?.getOrNull(inputIndex) && input.eventOrdinal < result.eventOrdinal + } + val pinnedSource = inference.sources.singleOrNull { it.module == compiled.definition.predicate.module } + if (!receiptsMatch || pinnedSource?.sha256 != capture.binding.sourceSha256) { + return unbound( + reason = "receipt-mismatch", + message = "Compiler receipt, original input or selected source changed" + ) + } + + val predicateMapping = mapping.predicate + val unavailableEntry = predicateMapping.status == EtsMappingStatus.UNMAPPED || + predicateMapping.status == EtsMappingStatus.UNSUPPORTED + if (unavailableEntry) { + return EtsMappingResult( + predicateMapping.status, + targets = emptyList(), + diagnostics = predicateMapping.diagnostics + ) + } + val inputBindingsMatch = predicateMapping.targets.all { entry -> + val expected = entry.method.inputBindingsFor(compiled.definition.inputs) + + expected.size == compiled.definition.inputs.size && entry.bindings.inputs == expected + } + if (!inputBindingsMatch) { + return unbound(reason = "input-mismatch", message = "The original positional input bindings changed") + } + val locations = SourceLocationNormalizer(mapping.provenance.sourceRoots.map(Path::of)) + val module = compiled.definition.predicate.module + val paths = try { + locations.sourcePathCandidates(module).filter(Files::isRegularFile) + } catch (_: InvalidPathException) { + return unbound(reason = "source-unmapped", message = "The generated module path is unavailable") + } + if (paths.isEmpty()) { + return unbound( + reason = "source-unmapped", + message = "The generated source file is missing", + status = EtsMappingStatus.UNMAPPED + ) + } + val candidates = predicateMapping.targets.flatMap { entry -> + entry.bindCompilerStores(compiled, relation, resultIsLeft, paths, locations) + } + if (candidates.isEmpty()) { + return unbound( + reason = "store-unmapped", + message = "The original predicate and companion require their declared numeric local stores", + status = EtsMappingStatus.UNMAPPED, + ) + } + val ambiguous = paths.size != 1 || candidates.size != 1 || predicateMapping.status == EtsMappingStatus.AMBIGUOUS + if (ambiguous) { + val diagnostic = + diagnostic(reason = "store-ambiguous", message = "Several generated sources, entries or stores match") + + return EtsMappingResult(EtsMappingStatus.AMBIGUOUS, targets = candidates, diagnostics = listOf(diagnostic)) + } + val sourceMatches = compiled.matchesPinnedSources(inference, locations, generatedSource = paths.single()) + if (!sourceMatches) { + return unbound(reason = "source-stale", message = "The generated source no longer matches the original program") + } + + return EtsMappingResult(EtsMappingStatus.EXACT, targets = candidates) +} + +private fun EtsEntryPointTarget.bindCompilerStores( + compiled: CompiledDslProperty, + relation: ScalarRelation, + resultIsLeft: Boolean, + paths: List, + locations: SourceLocationNormalizer, +): List { + val capture = requireNotNull(compiled.numericLocalCapture) + val inputIndex = requireNotNull(capture.input.inputIndex) + val input = bindings.inputs.getOrNull(inputIndex) + val validEntry = method.name == capture.binding.predicateExportName && + bindings.inputs.size == compiled.definition.inputs.size && input?.parameter?.type == EtsNumberType + if (!validEntry) return emptyList() + + val owner = method.enclosingClass + val companionMethods = owner?.methods.orEmpty().filter { companion -> + companion.name == capture.binding.companionExportName && + companion.parameters.lastOrNull()?.name == "__usvmObserve" && + companion.parameters.size == method.parameters.size + 1 + } + val originals = method.storesAt(capture.binding.predicateAssignment, capture.binding.localName, paths, locations) + val companions = companionMethods.flatMap { companion -> + companion.storesAt(capture.binding.companionAssignment, capture.binding.localName, paths, locations) + } + + return originals.flatMap { assignment -> + companions.map { companion -> + UsvmDslNumericLocalBinding( + method = method, + assignment = assignment, + companionAssignment = companion, + local = assignment.lhv as EtsLocal, + inputIndex = inputIndex, + input = requireNotNull(input), + resultIsLeft = resultIsLeft, + compiler = capture.binding, + relation = relation, + ) + } + } +} + +private fun CompiledDslProperty.matchesPinnedSources( + inference: ScalarRelationInference, + locations: SourceLocationNormalizer, + generatedSource: Path, +): Boolean = try { + val selectedSourcesMatch = inference.sources.all { source -> + val paths = locations.sourcePathCandidates(source.module).filter(Files::isRegularFile) + val path = paths.singleOrNull() + val hash = path?.let { file -> + MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(file)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + } + + hash == source.sha256 + } + + selectedSourcesMatch && Files.readString(generatedSource) == typeScript +} catch (_: IOException) { + false +} catch (_: InvalidPathException) { + false +} + +private fun EtsMethod.storesAt( + point: PropertySourcePoint, + localName: String, + paths: List, + locations: SourceLocationNormalizer, +): List = cfg.instructions.filterIsInstance().filter { assignment -> + val local = assignment.lhv as? EtsLocal + val origin = assignment.location.origin + val pathsMatch = origin != null && locations.sourcePathCandidates(origin.fileName).any { it in paths } + + local != null && local.name == localName && local.type == EtsNumberType && origin != null && pathsMatch && + origin.startLine == point.line - 1 && origin.startColumn == point.column - 1 +} + +private fun unbound( + reason: String, + message: String, + status: EtsMappingStatus = EtsMappingStatus.UNSUPPORTED, +): EtsMappingResult { + val diagnostic = diagnostic(reason, message) + + return EtsMappingResult(status = status, targets = emptyList(), diagnostics = listOf(diagnostic)) +} + +private fun diagnostic(reason: String, message: String): EtsMappingDiagnostic = + EtsMappingDiagnostic(code = "usvm.dsl-local.$reason", message = message) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalRefuter.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalRefuter.kt new file mode 100644 index 0000000000..45c3e56ef0 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalRefuter.kt @@ -0,0 +1,125 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsScene +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.machine.TsOptions +import org.usvm.machine.expr.TsSimpleValueResolver +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.inference.ScalarRelationTemplate +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue + +/** An auxiliary candidate at one compiler-owned store; native replay decides the complete original outcome. */ +data class UsvmDslNumericLocalRefutation( + val inference: ScalarRelationInference, + val binding: EtsMappingResult, + val status: UsvmRelationRefutationStatus, + val inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, + val timedOut: Boolean = false, +) { + init { + require(status != UsvmRelationRefutationStatus.REFUTATION_REACHED || inputs != null) + require(inputs == null || binding.status == EtsMappingStatus.EXACT) + } +} + +/** Searches domain AND original admission AND NOT(relation) immediately after the selected original store. */ +class UsvmDslNumericLocalRefuter( + scene: EtsScene, + machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + tsOptions: TsOptions = TsOptions(), + projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val search = UsvmRelationRefutationSearch(scene, machineOptions, tsOptions, projectionOptions) + + fun refute( + compiled: CompiledDslProperty, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + inference: ScalarRelationInference, + relation: ScalarRelation, + ): UsvmDslNumericLocalRefutation { + val manifest = compiled.definition.toManifest() + val binding = bindDslNumericLocalRelation(compiled, mapping, inference, relation) + val capability = search.capability(manifest, mapping, concreteCapability) + val unsupported = binding.status != EtsMappingStatus.EXACT || + capability.symbolic.level == ProjectionLevel.UNSUPPORTED + if (unsupported) { + return UsvmDslNumericLocalRefutation( + inference = inference, + binding = binding, + status = UsvmRelationRefutationStatus.UNSUPPORTED, + inputs = null, + capability = capability, + diagnostics = capability.symbolic.diagnostics, + ) + } + val observer = NumericLocalRefutationObserver(binding.targets.single()) + val result = search.search(manifest, mapping, capability, observer) + + return UsvmDslNumericLocalRefutation( + inference = inference, + binding = binding, + status = result.status, + inputs = result.inputs, + capability = result.capability, + diagnostics = result.diagnostics, + timedOut = result.timedOut, + ) + } +} + +private class NumericLocalRefutationObserver( + private val binding: UsvmDslNumericLocalBinding, +) : UsvmRelationRefutationObserver() { + override fun onAssignmentCompleted( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope, + ) { + val selectedStore = stmt === binding.assignment && isAdmittedRoot(scope) + if (!selectedStore || reached != null) return + + admittedPointReached = true + val value = binding.local.accept(simpleValueResolver) + val candidate = scope.calcOnState { clone() } + with(candidate.ctx) { + if (value == null || value.sort != fp64Sort) { + pointDiagnostics += CapabilityDiagnostic( + code = "usvm.dsl-local.sort-unsupported", + message = "The selected numeric local has an unsupported symbolic representation", + path = binding.compiler.localName, + ) + } else { + val original = projection.inputs[binding.inputIndex].value.asExpr(fp64Sort) + val stored = value.asExpr(fp64Sort) + val left = if (binding.resultIsLeft) stored else original + val right = if (binding.resultIsLeft) original else stored + val hypothesis = when (binding.relation.template) { + ScalarRelationTemplate.STRICT_EQUAL -> mkFpEqualExpr(left, right) + ScalarRelationTemplate.LESS_OR_EQUAL -> mkFpLessOrEqualExpr(left, right) + } + candidate.pathConstraints += hypothesis.not() + consider(candidate) + } + + // The interpreter still advances this completed assignment before collecting its step result. + // A false path ends this auxiliary prefix there; the complete suffix is checked natively. + scope.doWithState { pathConstraints += falseExpr } + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt new file mode 100644 index 0000000000..1d07374c01 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt @@ -0,0 +1,170 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsNumberType +import org.usvm.UBoolExpr +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.inference.ScalarRelationStatus +import org.usvm.ts.pbt.inference.ScalarRelationTemplate +import org.usvm.ts.pbt.inference.matches +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsInputBinding +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.mapping.inputBindingsFor +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.ObservationPointKind +import java.io.IOException +import java.nio.file.Files +import java.nio.file.InvalidPathException +import java.nio.file.Path +import java.security.MessageDigest + +/** Exact only for adapter-owned root input snapshots, independently of the executable body build. */ +data class UsvmEntryRelationBinding( + val leftInputIndex: Int, + val rightInputIndex: Int, + val left: EtsInputBinding, + val right: EtsInputBinding, + val relation: ScalarRelation, +) + +internal fun UsvmEntryRelationBinding.negatedRelation( + state: TsState, + projection: UsvmDeclaredDomainProjection, +): UBoolExpr = with(state.ctx) { + val leftValue = projection.inputs[leftInputIndex].value.asExpr(fp64Sort) + val rightValue = projection.inputs[rightInputIndex].value.asExpr(fp64Sort) + val hypothesis = when (relation.template) { + ScalarRelationTemplate.STRICT_EQUAL -> mkFpEqualExpr(leftValue, rightValue) + ScalarRelationTemplate.LESS_OR_EQUAL -> mkFpLessOrEqualExpr(leftValue, rightValue) + } + + hypothesis.not() +} + +/** An explicitly focused original-property search; no-finding does not exhaust the original domain. */ +data class UsvmEntryRelationSearchResult( + val binding: EtsMappingResult, + val inference: ScalarRelationInference, + val search: UsvmPropertySearchResult?, +) + +internal fun bindEntryRelation( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + inference: ScalarRelationInference, + relation: ScalarRelation, +): EtsMappingResult { + val sameProperty = inference.property.toManifest() == manifest && + inference.propertyId == mapping.propertyId && inference.propertyId.value == manifest.propertyId + if (!sameProperty) { + return unsupported(reason = "property-mismatch", message = "Property definition or declared support changed") + } + + val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED && + relation.limitations.isEmpty() + if (!sampled) { + return unsupported(reason = "not-sampled", message = "A sampled relation from this inference is required") + } + + val points = listOf(relation.pair.left, relation.pair.right) + val entrySnapshots = points.all { point -> + point.kind == ObservationPointKind.ENTRY_ARGUMENT && point.inputIndex in manifest.inputs.indices && + point.source.module == manifest.predicate.module && point.callSite.module == manifest.predicate.module + } + if (!entrySnapshots) { + return unsupported(reason = "point-unsupported", message = "Only adapter-owned root entry arguments are bound") + } + + val snapshotsMatch = relation.evidence.all { evidence -> + val input = evidence.invocation.input.value as? JsConcreteValue.Array + val events = listOf(evidence.left, evidence.right) + val eventsMatch = events.zip(points).all { (event, point) -> + val index = event.inputIndex + event.matches(point) && index != null && event.value.value is JsConcreteValue.Number && + event.value.value == input?.elements?.getOrNull(index) + } + + eventsMatch && evidence.invocation.parentInvocationId == null && + evidence.invocation.callSite == relation.pair.left.callSite + } + if (!snapshotsMatch) { + return unsupported(reason = "snapshot-mismatch", message = "Entry values do not match original input snapshots") + } + + val sourceMatches = try { + sourceMatches(manifest, mapping, inference) + } catch (_: IOException) { + false + } catch (_: InvalidPathException) { + false + } + if (!sourceMatches) { + return unsupported( + reason = "source-mismatch", + message = "The selected predicate source is missing, ambiguous or stale", + ) + } + + val predicate = mapping.predicate + if (predicate.status != EtsMappingStatus.EXACT) { + return unsupported( + reason = "entry-${predicate.status.name.lowercase()}", + message = "The original entry point must map exactly", + ) + } + val target = predicate.targets.singleOrNull() + ?: return unsupported(reason = "entry-ambiguous", message = "Exactly one original entry point is required") + val expectedInputs = target.method.inputBindingsFor(manifest.inputs) + val inputsMatch = expectedInputs.size == manifest.inputs.size && target.bindings.inputs == expectedInputs + if (!inputsMatch) { + return unsupported(reason = "slots-mismatch", message = "Original inputs do not match the entry slots") + } + val leftIndex = requireNotNull(points[0].inputIndex) + val rightIndex = requireNotNull(points[1].inputIndex) + val left = target.bindings.inputs[leftIndex] + val right = target.bindings.inputs[rightIndex] + if (left.parameter.type != EtsNumberType || right.parameter.type != EtsNumberType) { + return unsupported(reason = "type-unsupported", message = "Both entry slots must have the numeric EtsIR type") + } + + val binding = UsvmEntryRelationBinding(leftIndex, rightIndex, left, right, relation) + + return EtsMappingResult( + status = EtsMappingStatus.EXACT, + targets = listOf(binding), + ) +} + +private fun sourceMatches( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + inference: ScalarRelationInference, +): Boolean { + val module = manifest.predicate.module + val source = inference.sources.singleOrNull { it.module == module } ?: return false + val paths = mapping.provenance.sourceRoots.map { root -> Path.of(root).resolve(module).normalize() } + val existing = paths.filter(Files::isRegularFile).map(Path::toRealPath).distinct() + val path = existing.singleOrNull() ?: return false + val bytes = Files.readAllBytes(path) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + + return source.sha256 == hash +} + +private fun unsupported(reason: String, message: String): EtsMappingResult { + val diagnostic = EtsMappingDiagnostic(code = "usvm.entry-relation.$reason", message = message) + + return EtsMappingResult( + status = EtsMappingStatus.UNSUPPORTED, + targets = emptyList(), + diagnostics = listOf(diagnostic), + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt new file mode 100644 index 0000000000..65aa57d0f3 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt @@ -0,0 +1,107 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.machine.TsOptions +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue + +/** Source bridge for the entry-only name; it does not retain the old enum's JVM binary identity. */ +typealias UsvmEntryRefutationStatus = UsvmRelationRefutationStatus + +/** Reaches an admitted original input that refutes a sample; the original oracle still needs native execution. */ +data class UsvmEntryRelationRefutation( + val inference: ScalarRelationInference, + val binding: EtsMappingResult, + val status: UsvmRelationRefutationStatus, + val inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, + val timedOut: Boolean = false, +) { + init { + require(status != UsvmRelationRefutationStatus.REFUTATION_REACHED || inputs != null) + require(inputs == null || binding.status == EtsMappingStatus.EXACT) + } +} + +/** + * Searches domain AND original admission AND NOT(entry relation), without negating the original oracle. + * The standalone machine uses the supplied timeout; the campaign owns its shared deadline and cancellation. + */ +class UsvmEntryRelationRefuter( + scene: EtsScene, + machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + tsOptions: TsOptions = TsOptions(), + projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val search = UsvmRelationRefutationSearch(scene, machineOptions, tsOptions, projectionOptions) + + fun refute( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + inference: ScalarRelationInference, + relation: ScalarRelation, + ): UsvmEntryRelationRefutation { + val binding = bindEntryRelation(manifest, mapping, inference, relation) + val capability = search.capability(manifest, mapping, concreteCapability) + val unsupported = binding.status != EtsMappingStatus.EXACT || + capability.symbolic.level == ProjectionLevel.UNSUPPORTED + if (unsupported) { + return UsvmEntryRelationRefutation( + inference = inference, + binding = binding, + status = UsvmRelationRefutationStatus.UNSUPPORTED, + inputs = null, + capability = capability, + diagnostics = capability.symbolic.diagnostics, + ) + } + val predicate = requireNotNull(mapping.predicate.exactTargetOrNull()) + val observer = EntryRefutationObserver(predicate.method, binding.targets.single()) + val result = search.search(manifest, mapping, capability, observer) + + return UsvmEntryRelationRefutation( + inference = inference, + binding = binding, + status = result.status, + inputs = result.inputs, + capability = result.capability, + diagnostics = result.diagnostics, + timedOut = result.timedOut, + ) + } +} + +private class EntryRefutationObserver( + private val predicate: EtsMethod, + private val binding: UsvmEntryRelationBinding, +) : UsvmRelationRefutationObserver() { + override fun configureProjection(state: TsState, projection: UsvmDeclaredDomainProjection) { + super.configureProjection(state, projection) + state.pathConstraints += binding.negatedRelation(state, projection) + } + + override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + val firstEntryStatement = stmt === predicate.cfg.instructions.first() + val admittedEntry = isAdmittedRoot(scope) + if (reached != null || !firstEntryStatement || !admittedEntry) return + + admittedPointReached = true + consider(scope.calcOnState { clone() }) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 17e5941de7..e3410d6459 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -25,8 +25,11 @@ import org.usvm.ts.pbt.backend.CapabilityDiagnostic import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.EtsMappingStatus import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId @@ -62,6 +65,41 @@ class UsvmPropertySearcher( deadlineReached: (() -> Boolean)? = null, coverageFeedback: UsvmCoverageFeedback? = null, completedInputLimit: Int = 0, + ): UsvmPropertySearchResult = searchWithFocus( + manifest, + mapping, + concreteCapability, + focus = null, + deadlineReached, + coverageFeedback, + completedInputLimit, + ) + + /** Restricts one query to NOT(sampled entry relation); the ordinary search remains unrestricted. */ + fun searchFocusedOnEntryRelation( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + inference: ScalarRelationInference, + relation: ScalarRelation, + ): UsvmEntryRelationSearchResult { + val binding = bindEntryRelation(manifest, mapping, inference, relation) + val focus = if (binding.status == EtsMappingStatus.EXACT) binding.targets.single() else null + val search = focus?.let { + searchWithFocus(manifest, mapping, concreteCapability, focus = it) + } + + return UsvmEntryRelationSearchResult(binding, inference, search) + } + + private fun searchWithFocus( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + focus: UsvmEntryRelationBinding?, + deadlineReached: (() -> Boolean)? = null, + coverageFeedback: UsvmCoverageFeedback? = null, + completedInputLimit: Int = 0, ): UsvmPropertySearchResult { require(completedInputLimit >= 0) { "Completed input limit must not be negative" } val capability = capabilityResolver.resolve( @@ -111,6 +149,7 @@ class UsvmPropertySearcher( deadlineReached = deadlineReached ?: this.deadlineReached, guidance = guidance, completedInputLimit = completedInputLimit, + focus = focus, ).copy(edgeGuidance = guidance?.snapshot()) } @@ -122,6 +161,7 @@ class UsvmPropertySearcher( deadlineReached: (() -> Boolean)?, guidance: UsvmEdgeGuidance?, completedInputLimit: Int, + focus: UsvmEntryRelationBinding?, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val completedInputs = linkedSetOf() @@ -181,6 +221,9 @@ class UsvmPropertySearcher( bindings = predicate.bindings.inputs, generator = manifest.generator, ) + if (focus != null) { + state.pathConstraints += focus.negatedRelation(state, projection) + } if (precondition != null) { state.prependBooleanEntryPointGuard( guard = precondition.method, @@ -200,14 +243,10 @@ class UsvmPropertySearcher( projection = projection, ) } - val terminalFailure = classifyTerminalFailure( - manifest = manifest, - capability = capability, - analysis = analysis, - ) val runtimeDiagnostics = runtimeLimitations.diagnostics - val searchResult = terminalFailure?.withCandidate(candidate) + val searchResult = classifyTerminalFailure(manifest, capability, analysis)?.withCandidate(candidate) ?: candidate + ?: infeasibleFocusedEntry(focus, analysis, manifest, capability) ?: noViolationResult( manifest = manifest, capability = capability, @@ -224,6 +263,20 @@ class UsvmPropertySearcher( } } + private fun infeasibleFocusedEntry( + focus: UsvmEntryRelationBinding?, + analysis: TsMachineAnalysisResult, + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + ): UsvmPropertySearchResult? { + val focusInfeasible = focus != null && analysis.infeasibleEntryPoints.isNotEmpty() + return if (focusInfeasible) { + result(manifest, UsvmPropertySearchStatus.NO_VIOLATION_REACHED, capability) + } else { + null + } + } + private fun completedOutcome(violation: TsState?): WitnessOracleOutcome = when { violation?.methodResult is TsMethodResult.TsException -> WitnessOracleOutcome.THREW violation != null -> WitnessOracleOutcome.FALSE diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt new file mode 100644 index 0000000000..6ad76dee7e --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt @@ -0,0 +1,239 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.targets.TsTarget +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsEntryPointGuardOutcome +import org.usvm.machine.state.TsState +import org.usvm.machine.state.prependBooleanEntryPointGuard +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +import java.util.concurrent.CancellationException + +/** Auxiliary search outcomes, independently of the original property's truth. */ +enum class UsvmRelationRefutationStatus { + REFUTATION_REACHED, + NO_REFUTATION_REACHED, + PRECONDITION_REJECTED, + PROPERTY_ERROR, + TIMEOUT, + SOLVER_UNKNOWN, + UNSUPPORTED, + INCOMPLETE, + ENGINE_FAILURE, + FAILED_INPUT_RESOLUTION, +} + +internal data class UsvmRelationRefutationSearchResult( + val status: UsvmRelationRefutationStatus, + val inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, + val timedOut: Boolean, +) + +/** Shared machine lifecycle; entry and post-store triggers keep their own point semantics. */ +internal class UsvmRelationRefutationSearch( + private val scene: EtsScene, + machineOptions: UMachineOptions, + private val tsOptions: TsOptions, + projectionOptions: UsvmProjectionOptions, +) { + private val machineOptions = machineOptions.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnTargetsReached = true, + stopOnCoverage = 0, + ) + private val projectionOptions = projectionOptions.copy( + maxSymbolicCollectionLength = minOf(projectionOptions.maxSymbolicCollectionLength, tsOptions.maxArraySize), + maxSymbolicStringLength = minOf(projectionOptions.maxSymbolicStringLength, tsOptions.maxArraySize), + ) + + fun capability( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + ): UsvmPropertyProjectionCapability = UsvmProjectionCapabilityResolver(scene).resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + + fun search( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + capability: UsvmPropertyProjectionCapability, + observer: UsvmRelationRefutationObserver, + ): UsvmRelationRefutationSearchResult { + val predicate = requireNotNull(mapping.predicate.exactTargetOrNull()) + val precondition = mapping.precondition?.exactTargetOrNull() + val shapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain }) + val projector = UsvmDomainProjector(projectionOptions, shapes) + lateinit var projection: UsvmDeclaredDomainProjection + + return TsMachine( + scene = shapes.scene, + options = machineOptions, + tsOptions = tsOptions, + observer = observer, + ).use { machine -> + val analysis = machine.analyzeWithMetadata( + methods = listOf(predicate.method), + targets = listOf(observer.target), + configureInitialState = { _, state -> + projection = projector.configure( + state = state, + inputs = manifest.inputs, + bindings = predicate.bindings.inputs, + generator = manifest.generator, + ) + observer.configureProjection(state, projection) + if (precondition != null) { + state.prependBooleanEntryPointGuard( + guard = precondition.method, + arguments = projection.inputs.map(UsvmProjectedInput::value), + ) + } + }, + ) + val extraction = observer.reached?.let { state -> resolveInputs(state, manifest, projection, shapes) } + val status = when { + extraction?.isFailure == true -> UsvmRelationRefutationStatus.FAILED_INPUT_RESOLUTION + extraction?.isSuccess == true -> UsvmRelationRefutationStatus.REFUTATION_REACHED + else -> classifyUnreached( + analysis, + solverUnknown = observer.solverUnknown, + runtimeLimited = observer.diagnostics.isNotEmpty(), + admittedPointReached = observer.admittedPointReached, + ) + } + val diagnostics = buildList { + addAll(capability.symbolic.diagnostics) + addAll(observer.diagnostics) + analysis.unsupportedPaths.forEach { message -> + val diagnostic = CapabilityDiagnostic( + code = "usvm.relation-refutation.unsupported", + message = message, + path = "original-prefix", + ) + add(diagnostic) + } + val failure = extraction?.exceptionOrNull() + if (failure != null) { + val diagnostic = CapabilityDiagnostic( + code = "usvm.relation-refutation.extraction", + message = failure.toString(), + path = "inputs", + ) + add(diagnostic) + } + } + + UsvmRelationRefutationSearchResult( + status = status, + inputs = extraction?.getOrNull(), + capability = capability, + diagnostics = diagnostics, + timedOut = analysis.timedOut, + ) + } + } +} + +internal open class UsvmRelationRefutationObserver : TsInterpreterObserver { + val target = TsTarget(location = null) + protected lateinit var projection: UsvmDeclaredDomainProjection + protected val pointDiagnostics = mutableListOf() + private val runtimeLimitations = UsvmRuntimeLimitationObserver() + + val diagnostics: List + get() = runtimeLimitations.diagnostics + pointDiagnostics + + var reached: TsState? = null + private set + + var solverUnknown: Boolean = false + private set + + var admittedPointReached: Boolean = false + protected set + + open fun configureProjection(state: TsState, projection: UsvmDeclaredDomainProjection) { + this.projection = projection + } + + protected fun isAdmittedRoot(scope: TsStepScope): Boolean = scope.calcOnState { + !entryPointGuardActive && entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && callStack.size == 1 + } + + protected fun consider(candidate: TsState) { + when (val result = candidate.ctx.solver().check(candidate.pathConstraints)) { + is USatResult -> { + candidate.models = listOf(result.model) + target.propagate(candidate) + reached = candidate + } + + is UUnknownResult -> solverUnknown = true + is UUnsatResult -> Unit + } + } + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + runtimeLimitations.onRuntimeFeatureLimitation(event) + } +} + +private fun resolveInputs( + state: TsState, + manifest: PropertyManifest, + projection: UsvmDeclaredDomainProjection, + shapes: PlainObjectInputShapes, +): Result> = try { + Result.success(UsvmCandidateInputResolver(shapes).resolve(state, manifest.inputs, projection)) +} catch (cancelled: CancellationException) { + throw cancelled +} catch (failure: IllegalStateException) { + Result.failure(failure) +} catch (failure: IllegalArgumentException) { + Result.failure(failure) +} + +private fun classifyUnreached( + analysis: TsMachineAnalysisResult, + solverUnknown: Boolean, + runtimeLimited: Boolean, + admittedPointReached: Boolean, +): UsvmRelationRefutationStatus { + val guardError = analysis.states.any { it.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR } + val guardRejected = analysis.states.any { it.entryPointGuardOutcome == TsEntryPointGuardOutcome.REJECTED } + + return when { + guardError -> UsvmRelationRefutationStatus.PROPERTY_ERROR + analysis.timedOut -> UsvmRelationRefutationStatus.TIMEOUT + solverUnknown -> UsvmRelationRefutationStatus.SOLVER_UNKNOWN + runtimeLimited || analysis.unsupportedCall || analysis.unsupportedPaths.isNotEmpty() -> { + UsvmRelationRefutationStatus.UNSUPPORTED + } + analysis.engineFailed -> UsvmRelationRefutationStatus.ENGINE_FAILURE + analysis.stopReason != TsAnalysisStopReason.EXHAUSTED -> UsvmRelationRefutationStatus.INCOMPLETE + guardRejected && !admittedPointReached -> UsvmRelationRefutationStatus.PRECONDITION_REJECTED + else -> UsvmRelationRefutationStatus.NO_REFUTATION_REACHED + } +} 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..c30aaef989 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt @@ -0,0 +1,130 @@ +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 `captured program rejects inconsistent module decisions instead of claiming reproducible identity`() { + val program = defineProperty(id = "dsl.unstable-imports") { + val first = function<(Double) -> Double>(module = "helpers.ts", exportName = "first") + val second = function<(Double) -> Double>(module = "helpers.ts", exportName = "second") + val input by int() + val result by value(first(input)) + + check(name = "bound") { result lessOrEqual input } + check(name = "other") { second(input) lessOrEqual input } + } + var resolutions = 0 + + assertFailsWith { + PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./helper-${resolutions++}.ts" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + } + } + + @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) } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt new file mode 100644 index 0000000000..17818cd643 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt @@ -0,0 +1,339 @@ +package org.usvm.ts.pbt.inference + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.ConstantDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.JsNumber +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyAssertion +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.PropertyOperand +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.ObservationBuildStatus +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.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyInvocationObservation +import org.usvm.ts.pbt.observation.PropertyObservationArtifact +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyObservationValue +import org.usvm.ts.pbt.observation.PropertyPointEvent +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class DomainImpliedScalarRelationTest { + @Test + fun `separated inclusive integer domains remove only the already guaranteed order`() { + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + + val result = infer(property, samples) + + val implied = result.domainImpliedRelations.single() + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, implied.template) + assertEquals(ScalarRelationStatus.SAMPLED, implied.status) + assertEquals(samples, implied.evidence.map { it.invocation }) + assertEquals(2, implied.distinctGenerationInputs.size) + assertEquals(ScalarRelationStatus.REFUTED, result.relations.single().status) + assertEquals(SOURCES, result.sources) + assertEquals(property, result.property) + val selected = selectScalarGuidance(result) + val excludedOrder = selected.excluded.single { it.relation == implied } + assertEquals(ScalarGuidanceExclusionReason.DOMAIN_IMPLIED, excludedOrder.reason) + } + + @Test + fun `touching interval endpoints imply order but overlapping intervals do not`() { + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + val touching = property(IntegerDomain(min = 0, max = 2), IntegerDomain(min = 2, max = 3)) + val overlapping = property(IntegerDomain(min = 0, max = 3), IntegerDomain(min = 2, max = 3)) + + val touchingResult = infer(touching, samples) + val overlappingResult = infer(overlapping, samples) + + assertEquals(1, touchingResult.domainImpliedRelations.size) + assertTrue(overlappingResult.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, overlappingResult.order().status) + } + + @Test + fun `same original numeric input makes both templates redundant when NaN is excluded`() { + val right = RIGHT.copy(inputIndex = 0) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + val aliasSamples = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 0, max = 1)) + + val result = infer(property, aliasSamples, pair = ScalarObservationPair(LEFT, right)) + + assertTrue(result.relations.isEmpty()) + assertEquals(ScalarRelationTemplate.entries.toSet(), result.domainImpliedRelations.map { it.template }.toSet()) + assertTrue(result.domainImpliedRelations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + @Test + fun `guidance reuses domain facts and keeps NaN capable reflexive comparisons as unknown candidates`() { + val pair = ScalarObservationPair(LEFT, RIGHT.copy(inputIndex = 0)) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + val snapshots = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + val integers = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 0, max = 1)) + val numbers = property(NumberDomain(), IntegerDomain(min = 0, max = 1)) + val tautologies = infer(integers, snapshots, pair) + val nanCapable = infer(numbers, snapshots, pair) + + val excluded = selectScalarGuidance(tautologies) + val retained = selectScalarGuidance(nanCapable) + + assertTrue(excluded.candidates.isEmpty()) + assertEquals(tautologies.domainImpliedRelations, excluded.excluded.map { it.relation }) + assertTrue(excluded.excluded.all { it.reason == ScalarGuidanceExclusionReason.TAUTOLOGY }) + assertEquals(nanCapable.relations, retained.candidates.map { it.relation }) + assertTrue(retained.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(retained.excluded.isEmpty()) + } + + @Test + fun `ordinary argument labels never establish input identity even when every sample matches`() { + val left = LEFT.copy(kind = ObservationPointKind.ARGUMENT) + val right = RIGHT.copy(kind = ObservationPointKind.ARGUMENT) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + val ordinary = samples.map { invocation -> + invocation.copy(points = invocation.points.map { it.copy(kind = ObservationPointKind.ARGUMENT) }) + } + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + + val result = infer(property, ordinary, pair = ScalarObservationPair(left, right)) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + + @Test + fun `changed snapshots invalid indices and observations outside domains are retained`() { + val first = sample(id = 0, left = 0.0, right = 2.0) + val second = sample(id = 1, left = 1.0, right = 3.0) + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val differentInput = first.copy(input = captured(inputs(left = 1.0, right = 2.0))) + val snapshotResult = infer(property, listOf(differentInput, second)) + val outsideDomain = infer(property, listOf(first, sample(id = 1, left = 2.0, right = 3.0))) + val invalidPoint = LEFT.copy(inputIndex = 99) + val invalidSamples = listOf(first, second).map { invocation -> + invocation.copy(points = listOf(invocation.points.first().copy(inputIndex = 99), invocation.points.last())) + } + val invalidIndex = infer(property, invalidSamples, pair = ScalarObservationPair(invalidPoint, RIGHT)) + + for (result in listOf(snapshotResult, outsideDomain, invalidIndex)) { + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + } + + @Test + fun `NaN enabled domains cannot guarantee either comparison`() { + val property = property(NumberDomain(), IntegerDomain(min = 2, max = 3)) + val samples = listOf(sample(id = 0, left = 0.0, right = 2.0), sample(id = 1, left = 1.0, right = 3.0)) + + val result = infer(property, samples) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertEquals(ScalarRelationStatus.SAMPLED, result.order().status) + } + + @Test + fun `NaN allowed on an aliased original input prevents reflexivity filtering`() { + val property = property(NumberDomain(), NumberDomain()) + val right = RIGHT.copy(inputIndex = 0) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + val aliases = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + + val result = infer(property, aliases, pair = ScalarObservationPair(LEFT, right)) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + @Test + fun `binary64 bounds signed zero and infinities use numeric JavaScript ordering`() { + val negativeInfinity = Double.NEGATIVE_INFINITY + val positiveInfinity = Double.POSITIVE_INFINITY + val exactBoundary = 9_007_199_254_740_992.0 + val roundedBoundary = 9_007_199_254_740_993.0 + val cases = listOf( + property(numberDomain(min = -0.0, max = 0.0), numberDomain(min = 0.0, max = 1.0)) to listOf( + sample(id = 0, left = -0.0, right = 0.0), + sample(id = 1, left = 0.0, right = 1.0), + ), + property( + numberDomain(min = negativeInfinity, max = -1.0), + numberDomain(min = 0.0, max = positiveInfinity), + ) to listOf( + sample(id = 0, left = negativeInfinity, right = 0.0), + sample(id = 1, left = -1.0, right = positiveInfinity), + ), + property( + numberDomain(min = exactBoundary, max = roundedBoundary), + numberDomain(min = exactBoundary, max = positiveInfinity), + ) to listOf( + sample(id = 0, left = exactBoundary, right = exactBoundary), + sample(id = 1, left = exactBoundary, right = positiveInfinity), + ), + ) + + for ((property, samples) in cases) { + val result = infer(property, samples) + + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, result.domainImpliedRelations.single().template) + } + } + + @Test + fun `numeric constants participate in ordering but optional and malformed supports do not`() { + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 0.0, right = 1.0)) + val constant = ConstantDomain(JsConcreteValue.number(0.0)) + val right = IntegerDomain(min = 0, max = 1) + val numeric = property(constant, right) + val optional = property(OptionalDomain(constant), right) + val invalid = property(IntegerDomain(min = 1, max = 0), right) + + assertEquals(1, infer(numeric, samples).domainImpliedRelations.size) + assertTrue(infer(optional, samples).domainImpliedRelations.isEmpty()) + assertTrue(infer(invalid, samples).domainImpliedRelations.isEmpty()) + } + + @Test + fun `contradictions and insufficient or incomplete evidence never disappear into domain filtering`() { + val property = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 2, max = 3)) + val first = sample(id = 0, left = 0.0, right = 2.0) + val second = sample(id = 1, left = 1.0, right = 3.0) + val refuted = infer(property, listOf(first, second, sample(id = 2, left = 3.0, right = 2.0))) + val insufficient = infer(property, listOf(first)) + val dropped = artifact(listOf(first, second)).copy(droppedInvocations = 1) + val incomplete = inferScalarRelations(property, dropped, listOf(PAIR)) + + assertEquals(ScalarRelationStatus.REFUTED, refuted.order().status) + assertEquals(ScalarRelationStatus.INSUFFICIENT, insufficient.order().status) + assertEquals(ScalarRelationStatus.INSUFFICIENT, incomplete.order().status) + assertTrue(listOf(refuted, insufficient, incomplete).all { it.domainImpliedRelations.isEmpty() }) + } + + @Test + fun `unrepresented preconditions and original properties do not remove empirical relations`() { + val property = property(IntegerDomain(min = 0, max = 3), IntegerDomain(min = 0, max = 3)).copy( + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "ordered"), + ) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + + val result = infer(property, samples) + + assertTrue(result.domainImpliedRelations.isEmpty()) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + } + + private fun infer( + property: PropertyDefinition, + samples: List, + pair: ScalarObservationPair = PAIR, + ): ScalarRelationInference = inferScalarRelations(property, artifact(samples), listOf(pair)) + + private fun ScalarRelationInference.order(): ScalarRelation = + relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + private fun property(left: PropertyDomain, right: PropertyDomain): PropertyDefinition = PropertyDefinition( + id = ID, + inputs = listOf(PropertyInput(name = "left", domain = left), PropertyInput(name = "right", domain = right)), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "holds"), + 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 sample(id: Int, left: Double, right: Double): PropertyInvocationObservation = + PropertyInvocationObservation( + invocationId = id, + callSite = CALL, + origin = ObservationOrigin.FAST_CHECK, + phase = ObservationPhase.GENERATION, + input = captured(inputs(left, right)), + admission = ObservationAdmission.ADMITTED, + outcome = ObservationOutcome.HOLDS, + points = listOf(event(LEFT, left, ordinal = 0), event(RIGHT, right, ordinal = 1)), + ) + + private fun event(point: PropertyObservationPoint, number: Double, ordinal: Int): PropertyPointEvent = + PropertyPointEvent( + pointId = point.id, + assertionId = point.assertionId, + operandId = point.operandId, + source = point.source, + callSite = point.callSite, + kind = point.kind, + inputIndex = point.inputIndex, + occurrence = 0, + eventOrdinal = ordinal, + value = captured(JsConcreteValue.number(number)), + ) + + private fun inputs(left: Double, right: Double): JsConcreteValue = + JsConcreteValue.Array(listOf(JsConcreteValue.number(left), JsConcreteValue.number(right))) + + private fun captured(value: JsConcreteValue): PropertyObservationValue = + PropertyObservationValue(status = ObservationValueStatus.CAPTURED, value = value) + + private fun artifact(samples: List) = PropertyObservationArtifact( + propertyId = ID, + runId = "domain-filter", + verifiedSources = SOURCES, + buildStatus = ObservationBuildStatus.UNVERIFIED, + invocations = samples, + droppedInvocations = 0, + droppedPoints = 0, + captureTimeMillis = 0, + ) + + private fun numberDomain(min: Double, max: Double) = NumberDomain( + min = JsNumber.fromDouble(min), + max = JsNumber.fromDouble(max), + allowNaN = false, + ) + + private companion object { + const val MODULE = "property.ts" + val ID = PropertyId("test.domain-filter") + val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + 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) + val PAIR = ScalarObservationPair(LEFT, RIGHT) + val SOURCES = listOf(PropertyObservationSource(module = MODULE, sha256 = "a".repeat(64))) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt new file mode 100644 index 0000000000..d74b74d517 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt @@ -0,0 +1,437 @@ +package org.usvm.ts.pbt.inference + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.JsNumber +import org.usvm.ts.pbt.model.JsNumberKind +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.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.ObservationBuildStatus +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.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyInvocationObservation +import org.usvm.ts.pbt.observation.PropertyObservationArtifact +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyObservationValue +import org.usvm.ts.pbt.observation.PropertyPointEvent +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertSame +import kotlin.test.assertTrue + +class InferScalarRelationsTest { + @Test + fun `two and four value supports yield empirical relations without a large minimum`() { + for (supportSize in listOf(2, 4)) { + val samples = (0 until supportSize).map { index -> invocation(index, index.toDouble(), index.toDouble()) } + + val result = infer(samples) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertEquals(supportSize, result.relations.first().distinctGenerationInputs.size) + assertEquals(ObservationBuildStatus.UNVERIFIED, result.buildStatus) + assertEquals(SOURCES, result.sources) + } + } + + @Test + fun `duplicate generation inputs and replay shrink solver samples do not manufacture support`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val samples = listOf( + sample, + sample.copy(invocationId = 1), + invocation(id = 2, left = 1.0, right = 1.0).copy(phase = ObservationPhase.REPLAY), + invocation(id = 3, left = 2.0, right = 2.0).copy(phase = ObservationPhase.SHRINK), + invocation(id = 4, left = 3.0, right = 3.0).copy(origin = ObservationOrigin.SOLVER), + invocation(id = 5, left = 4.0, right = 4.0).copy(phase = ObservationPhase.EXPLICIT), + invocation(id = 6, left = 5.0, right = 5.0).copy(phase = ObservationPhase.UNKNOWN), + ) + + val result = infer(samples).relations.first() + + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertEquals(1, result.distinctGenerationInputs.size) + assertEquals(7, result.evidence.size) + assertTrue(ScalarRelationLimitation.INSUFFICIENT_DISTINCT_INPUTS in result.limitations) + } + + @Test + fun `later correlated witnesses retain the refuted relation and exact evidence`() { + val original = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + + for (phase in listOf(ObservationPhase.REPLAY, ObservationPhase.SHRINK)) { + val witness = invocation(id = 2, left = 1.0, right = 0.0).copy(phase = phase) + val result = infer(original + witness) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.REFUTED }) + assertEquals(2, result.relations.first().distinctGenerationInputs.size) + val contradiction = result.relations.first().evidence.single { !it.holds } + assertEquals(witness, contradiction.invocation) + assertEquals(witness.points.first().eventOrdinal, contradiction.left.eventOrdinal) + } + + val solver = invocation(id = 3, left = 1.0, right = 0.0).copy(origin = ObservationOrigin.SOLVER) + assertTrue(infer(original + solver).relations.all { it.status == ScalarRelationStatus.REFUTED }) + } + + @Test + fun `rejected inputs neither support nor refute a relation`() { + val rejected = invocation(id = 2, left = 1.0, right = 0.0).copy(admission = ObservationAdmission.REJECTED) + val original = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + + val result = infer(original + rejected) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.SAMPLED }) + assertEquals(2, result.relations.first().evidence.size) + } + + @Test + fun `points from different invocations are never paired`() { + val leftOnly = invocation(id = 0, left = 0.0, right = 0.0).let { it.copy(points = it.points.take(1)) } + val rightOnly = invocation(id = 1, left = 1.0, right = 1.0).let { it.copy(points = it.points.drop(1)) } + + val result = infer(listOf(leftOnly, rightOnly)).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(result.evidence.isEmpty()) + assertTrue(ScalarRelationLimitation.MISSING_POINT in result.limitations) + } + + @Test + fun `rare contexts keep independent evidence separate`() { + val first = invocation(id = 0, left = 0.0, right = 0.0) + val otherSite = CALL.copy(line = 100) + val elsewhere = invocation(id = 1, left = 1.0, right = 1.0).copy(callSite = otherSite) + val nested = invocation(id = 2, left = 2.0, right = 2.0).copy(parentInvocationId = 0) + + val result = infer(listOf(first, elsewhere, nested)).relations.first() + + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertEquals(1, result.distinctGenerationInputs.size) + assertTrue(ScalarRelationLimitation.UNSUPPORTED_CONTEXT in result.limitations) + } + + @Test + fun `changed assertion operand source callsite and repeated occurrence cannot supply evidence`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val left = sample.points.first() + val changed = listOf( + left.copy(assertionId = "another"), + left.copy(operandId = "another"), + left.copy(source = left.source.copy(line = 99)), + left.copy(callSite = CALL.copy(column = 99)), + left.copy(kind = ObservationPointKind.POST), + left.copy(inputIndex = 99), + left.copy(occurrence = 1), + ) + + for (event in changed) { + val result = infer(listOf(sample.copy(points = listOf(event, sample.points.last())))).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(ScalarRelationLimitation.POINT_IDENTITY_MISMATCH in result.limitations) + } + + val repeated = sample.copy(points = sample.points + left.copy(occurrence = 1, eventOrdinal = 2)) + assertTrue(ScalarRelationLimitation.REPEATED_POINT in infer(listOf(repeated)).relations.first().limitations) + } + + @Test + fun `non numeric truncated and malformed numeric values remain unsupported`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val values = listOf( + captured(JsConcreteValue.Null), + captured(JsConcreteValue.Undefined), + captured(JsConcreteValue.String("0")), + captured(JsConcreteValue.Boolean(true)), + PropertyObservationValue(status = ObservationValueStatus.TRUNCATED, reason = "byte-budget"), + captured(JsConcreteValue.Number(JsNumber(value = JsNumberKind.FINITE, bits = "not-bits"))), + ) + + for (value in values) { + val points = listOf(sample.points.first().copy(value = value), sample.points.last()) + val result = infer(listOf(sample.copy(points = points))).relations.first() + + assertEquals(ScalarRelationStatus.UNSUPPORTED, result.status) + assertTrue(ScalarRelationLimitation.UNSUPPORTED_VALUE in result.limitations) + } + } + + @Test + fun `numeric equality and order preserve NaN infinities signed zero and binary64 rounding`() { + val cases = listOf( + Triple(Double.NaN, Double.NaN, false), + Triple(-0.0, 0.0, true), + Triple(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY, true), + Triple(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY, true), + Triple(9_007_199_254_740_992.0, 9_007_199_254_740_993.0, true), + ) + + for ((left, right, expected) in cases) { + val relations = infer(listOf(invocation(id = 0, left = left, right = right))).relations + + assertTrue(relations.all { it.evidence.single().holds == expected }) + } + + val ordered = infer(listOf(invocation(id = 0, left = Double.NEGATIVE_INFINITY, right = 0.0))).relations + assertEquals(false, ordered.first().evidence.single().holds) + assertEquals(true, ordered.last().evidence.single().holds) + } + + @Test + fun `constant observed pairs are not promoted by unrelated changing inputs`() { + val first = invocation(id = 0, left = 1.0, right = 1.0) + val second = invocation(id = 1, left = 1.0, right = 1.0).copy(input = captured(input(2.0))) + + val result = infer(listOf(first, second)).relations.first() + + assertEquals(2, result.distinctGenerationInputs.size) + assertEquals(ScalarRelationStatus.INSUFFICIENT, result.status) + assertTrue(ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR in result.limitations) + } + + @Test + fun `self pairs unrelated points and missing source hashes stay unsupported`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val unrelated = RIGHT.copy(assertionId = "other") + val pairs = listOf(ScalarObservationPair(LEFT, LEFT), ScalarObservationPair(LEFT, unrelated)) + + val result = inferScalarRelations(PROPERTY, artifact(listOf(sample)), pairs) + + assertTrue(result.relations.all { ScalarRelationLimitation.INVALID_PAIR in it.limitations }) + val noSources = artifact(listOf(sample)).copy(verifiedSources = emptyList()) + val sourceResult = inferScalarRelations(PROPERTY, noSources, listOf(PAIR)).relations.first() + assertTrue(ScalarRelationLimitation.SOURCE_MISMATCH in sourceResult.limitations) + } + + @Test + fun `limits and deduplication are deterministic and preserve omitted evidence diagnostics`() { + val samples = (0..3).map { invocation(it, it.toDouble(), it.toDouble()) } + val observations = artifact(samples).copy(droppedInvocations = 2, droppedPoints = 3) + + val result = inferScalarRelations( + property = PROPERTY, + observations = observations, + pairs = listOf(PAIR, PAIR, ScalarObservationPair(RIGHT, LEFT)), + maxPairs = 1, + maxInvocations = 2, + ) + + assertEquals(2, result.relations.size) + assertEquals(1, result.omittedPairs) + assertEquals(2, result.omittedInvocations) + assertEquals(2, result.droppedInvocations) + assertEquals(3, result.droppedPoints) + assertTrue(result.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(result.relations.all { ScalarRelationLimitation.INVOCATION_LIMIT in it.limitations }) + } + + @Test + fun `empty pending and dropped capture report insufficient evidence`() { + val sample = invocation(id = 0, left = 0.0, right = 0.0) + val samples = listOf(sample, invocation(id = 1, left = 1.0, right = 1.0)) + val incomplete = artifact(samples).copy(droppedPoints = 1) + + val emptyResult = infer(emptyList()) + val pendingResult = infer(listOf(sample.copy(outcome = ObservationOutcome.PENDING))) + val droppedResult = inferScalarRelations(PROPERTY, incomplete, listOf(PAIR)) + + assertTrue(emptyResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(pendingResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(droppedResult.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(droppedResult.relations.all { ScalarRelationLimitation.INCOMPLETE_CAPTURE in it.limitations }) + } + + @Test + fun `selected source hashes are checked against property identity when declared`() { + val sourceIdentity = PropertySourceIdentity( + sourceSha256 = "b".repeat(64), + buildSha256 = "c".repeat(64), + buildScope = "test", + ) + val property = PROPERTY.copy(sourceIdentity = sourceIdentity) + val observations = artifact(listOf(invocation(id = 0, left = 0.0, right = 0.0))) + + val result = inferScalarRelations(property, observations, listOf(PAIR)) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.UNSUPPORTED }) + assertTrue(result.relations.all { ScalarRelationLimitation.SOURCE_MISMATCH in it.limitations }) + } + + @Test + fun `signed zeros alone do not count as numeric diversity`() { + val samples = listOf(invocation(id = 0, left = -0.0, right = -0.0), invocation(id = 1, left = 0.0, right = 0.0)) + + val result = infer(samples) + + assertTrue(result.relations.all { it.status == ScalarRelationStatus.INSUFFICIENT }) + assertTrue(result.relations.all { ScalarRelationLimitation.CONSTANT_OBSERVED_PAIR in it.limitations }) + assertEquals(2, result.relations.first().distinctGenerationInputs.size) + } + + @Test + fun `property identity and positive bounds are required`() { + val observations = artifact(emptyList()) + + assertFailsWith { + inferScalarRelations(PROPERTY, observations.copy(propertyId = PropertyId("other")), listOf(PAIR)) + } + assertFailsWith { + inferScalarRelations(PROPERTY, observations, listOf(PAIR), maxPairs = 0) + } + assertFailsWith { + inferScalarRelations(PROPERTY, observations, listOf(PAIR), maxInvocations = 0) + } + } + + @Test + fun `guidance selection removes symmetric equality duplicates without merging temporal identities`() { + val samples = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val observations = artifact(samples) + val reversed = ScalarObservationPair(RIGHT, LEFT) + val inference = inferScalarRelations(PROPERTY, observations, listOf(PAIR, reversed)) + + val selected = selectScalarGuidance(inference) + + assertSame(inference, selected.inference) + assertEquals(3, selected.candidates.size) + assertTrue(selected.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertEquals(ScalarGuidanceExclusionReason.DUPLICATE, selected.excluded.single().reason) + assertEquals(reversed, selected.excluded.single().relation.pair) + assertEquals(ScalarRelationTemplate.STRICT_EQUAL, selected.excluded.single().relation.template) + val duplicateEvidence = selected.excluded.single().relation.evidence + assertEquals(samples, duplicateEvidence.map { it.invocation }) + + val equality = selected.candidates.first().relation + val later = equality.copy(pair = equality.pair.copy(right = RIGHT.copy(kind = ObservationPointKind.POST))) + val differentTimes = inference.copy(relations = listOf(equality, later)) + assertEquals(2, selectScalarGuidance(differentTimes).candidates.size) + } + + @Test + fun `empty finite and contradicted evidence gives no guidance without losing the original artifact`() { + val samples = listOf(invocation(id = 0, left = 1.0, right = 1.0)) + val insufficient = infer(samples) + val contradicted = infer(samples + invocation(id = 1, left = 1.0, right = 0.0)) + + for (inference in listOf(infer(emptyList()), insufficient, contradicted)) { + val selected = selectScalarGuidance(inference) + + assertSame(inference, selected.inference) + assertTrue(selected.candidates.isEmpty()) + assertEquals(inference.relations, selected.excluded.map { it.relation }) + assertTrue(selected.excluded.all { it.reason == ScalarGuidanceExclusionReason.NOT_SAMPLED }) + } + } + + @Test + fun `guidance candidates are bounded in original selection order and overflow evidence is retained`() { + val samples = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val inference = infer(samples) + + val selected = selectScalarGuidance(inference, maxCandidates = 1) + + assertEquals(inference.relations.first(), selected.candidates.single().relation) + assertEquals(inference.relations.last(), selected.excluded.single().relation) + assertEquals(ScalarGuidanceExclusionReason.CANDIDATE_LIMIT, selected.excluded.single().reason) + assertFailsWith { selectScalarGuidance(inference, maxCandidates = 0) } + } + + private fun infer(samples: List): ScalarRelationInference = + inferScalarRelations(PROPERTY, artifact(samples), listOf(PAIR)) + + private fun invocation(id: Int, left: Double, right: Double): PropertyInvocationObservation = + PropertyInvocationObservation( + invocationId = id, + callSite = CALL, + origin = ObservationOrigin.FAST_CHECK, + phase = ObservationPhase.GENERATION, + input = captured(input(left)), + admission = ObservationAdmission.ADMITTED, + outcome = ObservationOutcome.HOLDS, + points = listOf(event(LEFT, left, ordinal = 0), event(RIGHT, right, ordinal = 1)), + ) + + private fun event(point: PropertyObservationPoint, number: Double, ordinal: Int): PropertyPointEvent = + PropertyPointEvent( + pointId = point.id, + assertionId = point.assertionId, + operandId = point.operandId, + source = point.source, + callSite = point.callSite, + kind = point.kind, + inputIndex = point.inputIndex, + occurrence = 0, + eventOrdinal = ordinal, + value = captured(JsConcreteValue.number(number)), + ) + + private fun artifact(samples: List): PropertyObservationArtifact = + PropertyObservationArtifact( + propertyId = PROPERTY.id, + runId = "sample-run", + verifiedSources = SOURCES, + buildStatus = ObservationBuildStatus.UNVERIFIED, + invocations = samples, + droppedInvocations = 0, + droppedPoints = 0, + captureTimeMillis = 0, + ) + + private fun input(number: Double): JsConcreteValue = JsConcreteValue.Array(listOf(JsConcreteValue.number(number))) + + private fun captured(value: JsConcreteValue): PropertyObservationValue = + PropertyObservationValue(status = ObservationValueStatus.CAPTURED, value = value) + + private companion object { + const val MODULE = "property.ts" + val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + val LEFT = PropertyObservationPoint( + id = "input", + assertionId = "check", + operandId = "input", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ARGUMENT, + inputIndex = 0, + ) + val RIGHT = PropertyObservationPoint( + id = "result", + assertionId = "check", + operandId = "result", + source = CALL.copy(column = 2), + callSite = CALL, + kind = ObservationPointKind.RETURN, + ) + val PAIR = ScalarObservationPair(LEFT, RIGHT) + val SOURCES = listOf(PropertyObservationSource(module = MODULE, sha256 = "a".repeat(64))) + val PROPERTY = PropertyDefinition( + id = PropertyId("test.numeric"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 3))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "check"), + 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), + ), + ), + ), + ) + } +}