From ec5f1fe00444e8248b86dc2e67cf880f925f436d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 01:17:59 +0300 Subject: [PATCH] [TS PBT] Focus original searches with observed entry argument relations --- .../src/execute-property.ts | 4 +- .../src/observe-property.ts | 22 +- .../test/execute-property.test.ts | 28 ++ .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 5 +- .../pbt/inference/EntryRelationSearchTest.kt | 333 ++++++++++++++++++ .../properties/inference/EntryRelations.ts | 15 + .../ts/pbt/inference/InferScalarRelations.kt | 3 +- .../usvm/ts/pbt/inference/ScalarRelation.kt | 2 + .../ts/pbt/observation/PropertyObservation.kt | 4 + .../ts/pbt/usvm/UsvmEntryRelationBinding.kt | 149 ++++++++ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 45 +++ 11 files changed, 604 insertions(+), 6 deletions(-) create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt 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 f4b8714dba..a8ad7eed20 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 @@ -761,7 +761,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); } @@ -773,7 +773,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`); 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 e6bac1b8c8..d6706080ef 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,7 +12,7 @@ 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; } @@ -153,6 +153,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 +172,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) { + // Entry snapshots belong to the adapter; user callbacks cannot replace or repeat them. + if (point?.kind === 'entry-argument') 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): void { + if (record.points.length >= this.request.maxPointsPerInvocation) { this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints); return; 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 5a434b96f0..53572c248f 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 @@ -175,6 +175,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/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 3fc53edcbf..44709e0f73 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 @@ -10,6 +10,7 @@ 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.ObservationPointKind import org.usvm.ts.pbt.observation.PropertyObservationRequest import org.usvm.ts.pbt.validation.requireValid import org.usvm.ts.pbt.validation.validatePropertyDefinition @@ -86,7 +87,9 @@ 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 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..2f6c5278c9 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationSearchTest.kt @@ -0,0 +1,333 @@ +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 `an infeasible focus is a scoped no-finding rather than an engine failure`() { + val property = property( + exportName = "reflexive", + leftDomain = IntegerDomain(min = 0, max = 1), + rightDomain = IntegerDomain(min = 2, max = 3), + ) + 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(EtsMappingStatus.EXACT, focused.binding.status) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, focused.search?.status) + } + + @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/resources/properties/inference/EntryRelations.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts new file mode 100644 index 0000000000..36dfdb76b4 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts @@ -0,0 +1,15 @@ +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; +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt index 803a33ebba..b3a20ea138 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/InferScalarRelations.kt @@ -54,6 +54,7 @@ fun inferScalarRelations( omittedInvocations = omittedInvocations, droppedInvocations = observations.droppedInvocations, droppedPoints = observations.droppedPoints, + property = property, ) } @@ -179,7 +180,7 @@ private fun ScalarObservationPair.isAssertionPair(property: PropertyDefinition): leftOperand?.source == left.source && rightOperand?.source == right.source } -private fun PropertyPointEvent.matches(point: PropertyObservationPoint): Boolean = +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 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 index ecb293afd5..c4bce5984b 100644 --- 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 @@ -1,6 +1,7 @@ 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.model.PropertyId import org.usvm.ts.pbt.observation.ObservationBuildStatus import org.usvm.ts.pbt.observation.PropertyInvocationObservation @@ -73,4 +74,5 @@ data class ScalarRelationInference( val omittedInvocations: Int, val droppedInvocations: Int, val droppedPoints: Int, + val property: PropertyDefinition, ) 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..14d782f8e6 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 @@ -21,6 +21,10 @@ data class PropertyObservationPoint( /** 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, 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..2dd734bed3 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationBinding.kt @@ -0,0 +1,149 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsNumberType +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.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.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, +) + +/** 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") + if (target.bindings.inputs.size != manifest.inputs.size) { + 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/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 10bf82289f..42f9768e2b 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 @@ -23,8 +23,12 @@ import org.usvm.ts.pbt.PbtDiagnosticCode 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.inference.ScalarRelationTemplate 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.PropertyId @@ -46,6 +50,28 @@ class UsvmPropertySearcher( manifest: PropertyManifest, mapping: PropertyEtsMappingArtifact, concreteCapability: ProjectionCapability, + ): UsvmPropertySearchResult = search(manifest, mapping, concreteCapability, focus = null) + + /** Restricts this query to NOT(sampled input relation), retaining the original precondition and oracle. */ + 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 { search(manifest, mapping, concreteCapability, focus = it) } + + return UsvmEntryRelationSearchResult(binding, inference, search) + } + + private fun search( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + focus: UsvmEntryRelationBinding?, ): UsvmPropertySearchResult { val capability = capabilityResolver.resolve( manifest = manifest, @@ -79,6 +105,7 @@ class UsvmPropertySearcher( predicate = predicate, precondition = precondition, capability = capability, + focus = focus, ) } @@ -87,6 +114,7 @@ class UsvmPropertySearcher( predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, capability: UsvmPropertyProjectionCapability, + focus: UsvmEntryRelationBinding?, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() @@ -111,6 +139,18 @@ class UsvmPropertySearcher( bindings = predicate.bindings.inputs, generator = manifest.generator, ) + if (focus != null) { + with(state.ctx) { + val left = projection.inputs[focus.leftInputIndex].value.asExpr(fp64Sort) + val right = projection.inputs[focus.rightInputIndex].value.asExpr(fp64Sort) + val hypothesis = when (focus.relation.template) { + ScalarRelationTemplate.STRICT_EQUAL -> mkFpEqualExpr(left, right) + ScalarRelationTemplate.LESS_OR_EQUAL -> mkFpLessOrEqualExpr(left, right) + } + + state.pathConstraints += hypothesis.not() + } + } if (precondition != null) { state.prependBooleanEntryPointGuard( guard = precondition.method, @@ -139,6 +179,11 @@ class UsvmPropertySearcher( return@use terminalFailure.withCandidate(candidate) } + val focusInfeasible = focus != null && analysis.infeasibleEntryPoints.isNotEmpty() + if (focusInfeasible) { + return@use result(manifest, UsvmPropertySearchStatus.NO_VIOLATION_REACHED, capability) + } + candidate ?: noViolationResult( manifest = manifest,