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 9990a1ded0..568181c3f1 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 @@ -833,6 +833,21 @@ 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`); @@ -846,10 +861,9 @@ function validateCompilerLocal( && binding.companionExportName === manifest.predicate.checkResultExportName && manifest.predicate.checkResultExportName !== undefined && manifest.predicate.executionKind === 'sync' && predicateAssignment.module === manifest.predicate.module && companionAssignment.module === manifest.predicate.module - && point.source.module === manifest.predicate.module && point.callSite.module === manifest.predicate.module && !samePoint(predicateAssignment, companionAssignment) && typeof binding.sourceSha256 === 'string' && /^[0-9a-f]{64}$/.test(binding.sourceSha256) - && source?.sha256 === binding.sourceSha256 && binding.occurrence === 0 && point.kind === 'return'; + && 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`); 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 caf4e4de24..7fe1101436 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,10 +3,11 @@ 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 { CompilerNumericLocalBinding } from './observe-property.js'; import { inWitnessSupport } from './witness-support.js'; export interface WitnessBinding { @@ -16,11 +17,19 @@ 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; @@ -68,7 +77,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. */ @@ -78,6 +95,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) { @@ -102,6 +124,12 @@ export async function executeWitness(value: unknown): Promise).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 @@ -151,6 +179,10 @@ export async function executeWitness(value: unknown): 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]; @@ -288,12 +329,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'; @@ -301,7 +349,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)); @@ -309,6 +357,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 @@ -341,12 +412,17 @@ function validateOperation(value: unknown, arity: number): WitnessOperation { && 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 && validEntryRelation && (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/test/compiler-local-capture.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/compiler-local-capture.test.ts index 6d8d9d2f6d..789a67bef7 100644 --- 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 @@ -4,6 +4,7 @@ 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'; @@ -186,3 +187,85 @@ test('changed selected source and incompatible companion signature cannot supply 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/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 d6312881f9..c3788346f3 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 @@ -310,6 +310,11 @@ internal class FastCheckWitnessCoordinator( 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/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/EntryRelationRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt index 25f8700d1d..06242ca2d5 100644 --- 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 @@ -172,6 +172,25 @@ class EntryRelationRefutationTest { 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() 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/ExternalWitness.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt index 7be38678cc..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 @@ -5,6 +5,7 @@ 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. */ @@ -27,6 +28,23 @@ data class WitnessEntryRelation( } } +/** 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( @@ -49,6 +67,7 @@ data class WitnessTarget( val binding: WitnessBinding? = null, val expectedOutcome: WitnessOracleOutcome? = null, val entryRelation: WitnessEntryRelation? = null, + val dslNumericLocalRelation: WitnessDslNumericLocalRelation? = null, ) { init { require(id.isNotBlank()) @@ -57,6 +76,10 @@ data class WitnessTarget( 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/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 index 043fb45e79..1d07374c01 100644 --- 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 @@ -16,6 +16,7 @@ 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 @@ -120,7 +121,9 @@ internal fun bindEntryRelation( } val target = predicate.targets.singleOrNull() ?: return unsupported(reason = "entry-ambiguous", message = "Exactly one original entry point is required") - if (target.bindings.inputs.size != manifest.inputs.size) { + 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) 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 index b73dc0d242..65aa57d0f3 100644 --- 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 @@ -3,24 +3,11 @@ 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.jacodb.ets.model.EtsType import org.usvm.SolverType -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.backend.ProjectionLevel @@ -31,34 +18,22 @@ 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 -import java.util.concurrent.CancellationException -/** Outcomes of an auxiliary relation search, independently of the original property's truth. */ -enum class UsvmEntryRefutationStatus { - REFUTATION_REACHED, - NO_REFUTATION_REACHED, - PRECONDITION_REJECTED, - PROPERTY_ERROR, - TIMEOUT, - SOLVER_UNKNOWN, - UNSUPPORTED, - INCOMPLETE, - ENGINE_FAILURE, - FAILED_INPUT_RESOLUTION, -} +/** 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: UsvmEntryRefutationStatus, + val status: UsvmRelationRefutationStatus, val inputs: List?, val capability: UsvmPropertyProjectionCapability, val diagnostics: List, val timedOut: Boolean = false, ) { init { - require(status != UsvmEntryRefutationStatus.REFUTATION_REACHED || inputs != null) + require(status != UsvmRelationRefutationStatus.REFUTATION_REACHED || inputs != null) require(inputs == null || binding.status == EtsMappingStatus.EXACT) } } @@ -68,20 +43,12 @@ data class UsvmEntryRelationRefutation( * The standalone machine uses the supplied timeout; the campaign owns its shared deadline and cancellation. */ class UsvmEntryRelationRefuter( - private val scene: EtsScene, + scene: EtsScene, machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), - private val tsOptions: TsOptions = TsOptions(), + tsOptions: TsOptions = TsOptions(), projectionOptions: UsvmProjectionOptions = 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), - ) + private val search = UsvmRelationRefutationSearch(scene, machineOptions, tsOptions, projectionOptions) fun refute( manifest: PropertyManifest, @@ -91,176 +58,50 @@ class UsvmEntryRelationRefuter( relation: ScalarRelation, ): UsvmEntryRelationRefutation { val binding = bindEntryRelation(manifest, mapping, inference, relation) - val capability = UsvmProjectionCapabilityResolver(scene).resolve( - manifest = manifest, - mapping = mapping, - concreteCapability = concreteCapability, - options = projectionOptions, - ) + 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 = UsvmEntryRefutationStatus.UNSUPPORTED, + status = UsvmRelationRefutationStatus.UNSUPPORTED, inputs = null, capability = capability, diagnostics = capability.symbolic.diagnostics, ) } - val predicate = requireNotNull(mapping.predicate.exactTargetOrNull()) - val precondition = mapping.precondition?.exactTargetOrNull() - val target = TsTarget(location = null) - val runtimeLimitations = UsvmRuntimeLimitationObserver() - val observer = EntryRefutationObserver(predicate.method, target, runtimeLimitations) - 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(target), - configureInitialState = { _, state -> - projection = projector.configure( - state = state, - inputs = manifest.inputs, - bindings = predicate.bindings.inputs, - generator = manifest.generator, - ) - state.pathConstraints += binding.targets.single().negatedRelation(state, projection) - if (precondition != null) { - state.prependBooleanEntryPointGuard( - guard = precondition.method, - arguments = projection.inputs.map(UsvmProjectedInput::value), - ) - } - }, - ) - val reached = observer.reached - val extraction = reached?.let { state -> - resolveInputs(state, manifest, projection, shapes) - } - val status = when { - extraction?.isFailure == true -> UsvmEntryRefutationStatus.FAILED_INPUT_RESOLUTION - extraction?.isSuccess == true -> UsvmEntryRefutationStatus.REFUTATION_REACHED - else -> classifyUnreached( - analysis, - solverUnknown = observer.solverUnknown, - runtimeLimited = runtimeLimitations.diagnostics.isNotEmpty(), - ) - } - val diagnostics = buildList { - addAll(capability.symbolic.diagnostics) - addAll(runtimeLimitations.diagnostics) - analysis.unsupportedPaths.forEach { message -> - val diagnostic = CapabilityDiagnostic( - code = "usvm.entry-refutation.unsupported", - message = message, - path = "precondition", - ) - add(diagnostic) - } - val failure = extraction?.exceptionOrNull() - if (failure != null) { - val diagnostic = CapabilityDiagnostic( - code = "usvm.entry-refutation.extraction", - message = failure.toString(), - path = "inputs", - ) - add(diagnostic) - } - } - - UsvmEntryRelationRefutation( - inference = inference, - binding = binding, - status = status, - inputs = extraction?.getOrNull(), - capability = capability, - diagnostics = diagnostics, - timedOut = analysis.timedOut, - ) - } - } -} - -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, -): UsvmEntryRefutationStatus { - val guardError = analysis.states.any { it.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR } - val guardRejected = analysis.states.any { it.entryPointGuardOutcome == TsEntryPointGuardOutcome.REJECTED } - - return when { - guardError -> UsvmEntryRefutationStatus.PROPERTY_ERROR - analysis.timedOut -> UsvmEntryRefutationStatus.TIMEOUT - solverUnknown -> UsvmEntryRefutationStatus.SOLVER_UNKNOWN - runtimeLimited || analysis.unsupportedCall || analysis.unsupportedPaths.isNotEmpty() -> { - UsvmEntryRefutationStatus.UNSUPPORTED - } - analysis.engineFailed -> UsvmEntryRefutationStatus.ENGINE_FAILURE - analysis.stopReason != TsAnalysisStopReason.EXHAUSTED -> UsvmEntryRefutationStatus.INCOMPLETE - guardRejected -> UsvmEntryRefutationStatus.PRECONDITION_REJECTED - else -> UsvmEntryRefutationStatus.NO_REFUTATION_REACHED + 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 target: TsTarget, - private val runtimeLimitations: UsvmRuntimeLimitationObserver, -) : TsInterpreterObserver { - var reached: TsState? = null - private set - - var solverUnknown: Boolean = false - private set - - override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { - runtimeLimitations.onRuntimeFeatureLimitation(event) + 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 = scope.calcOnState { - !entryPointGuardActive && entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && callStack.size == 1 - } + val admittedEntry = isAdmittedRoot(scope) if (reached != null || !firstEntryStatement || !admittedEntry) return - val candidate = scope.calcOnState { clone() } - 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 - } + admittedPointReached = true + consider(scope.calcOnState { clone() }) } } 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 + } +}