From b57c44fa27f994d325745c1798e7427738d4a812 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 23:42:24 +0300 Subject: [PATCH] Select bounded scalar guidance and retain excluded relation evidence --- .../inference/DslNumericLocalRelationTest.kt | 78 ++++++++++- .../usvm/ts/pbt/dsl/DslNumericLocalCapture.kt | 15 +++ .../ts/pbt/inference/SelectScalarGuidance.kt | 127 ++++++++++++++++++ .../ts/pbt/usvm/UsvmDslNumericLocalBinding.kt | 18 +-- .../DomainImpliedScalarRelationTest.kt | 26 ++++ .../pbt/inference/InferScalarRelationsTest.kt | 54 ++++++++ 6 files changed, 297 insertions(+), 21 deletions(-) create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt index 3188a5e071..ffc44cc7a0 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt @@ -10,6 +10,7 @@ import org.usvm.ts.pbt.dsl.CompiledDslProperty import org.usvm.ts.pbt.dsl.DslNumericLocalCapture import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler import org.usvm.ts.pbt.dsl.defineProperty +import org.usvm.ts.pbt.dsl.equalTo import org.usvm.ts.pbt.dsl.invoke import org.usvm.ts.pbt.dsl.lessOrEqual import org.usvm.ts.pbt.fastcheck.FastCheckBackend @@ -31,6 +32,7 @@ import java.nio.file.Path import java.security.MessageDigest import kotlin.test.assertEquals import kotlin.test.assertNotNull +import kotlin.test.assertSame import kotlin.test.assertTrue class DslNumericLocalRelationTest { @@ -246,6 +248,72 @@ class DslNumericLocalRelationTest { assertTrue(missing.targets.isEmpty()) } + @Test + fun `native compiler observations keep a stronger equality and exclude the original order only`() { + val fixture = prepare() + + val selected = selectScalarGuidance(fixture.inference, fixture.compiled) + + assertSame(fixture.inference, selected.inference) + assertEquals(ScalarRelationTemplate.STRICT_EQUAL, selected.candidates.single().relation.template) + assertEquals(ScalarGuidanceRelevance.KNOWN_DSL_CHECK, selected.candidates.single().relevance) + assertEquals(ScalarRelationTemplate.LESS_OR_EQUAL, selected.excluded.single().relation.template) + assertEquals(ScalarGuidanceExclusionReason.ORIGINAL_CHECK, selected.excluded.single().reason) + assertEquals(ObservationBuildStatus.UNVERIFIED, selected.inference.buildStatus) + } + + @Test + fun `an original equality excludes both equality and its weaker orders over the same captured operands`() { + val fixture = prepare(originalEquality = true) + val relations = fixture.inference.relations + val reversed = relations.map { relation -> + relation.copy( + pair = ScalarObservationPair(relation.pair.right, relation.pair.left), + evidence = relation.evidence.map { it.copy(left = it.right, right = it.left) }, + ) + } + val inference = fixture.inference.copy(relations = relations + reversed) + + val selected = selectScalarGuidance(inference, fixture.compiled) + + assertTrue(selected.candidates.isEmpty()) + assertEquals(4, selected.excluded.size) + assertTrue(selected.excluded.all { it.reason == ScalarGuidanceExclusionReason.ORIGINAL_CHECK }) + assertTrue(selected.excluded.all { it.relevance == ScalarGuidanceRelevance.KNOWN_DSL_CHECK }) + assertEquals(inference.relations, selected.excluded.map { it.relation }) + } + + @Test + fun `forged retained program source or point metadata cannot establish original formula relevance`() { + val fixture = prepare() + val compiled = fixture.compiled + val capture = assertNotNull(compiled.numericLocalCapture) + val fake = capture.copy(result = capture.result.copy(operandId = "unrelated")) + val variants = listOf( + compiled.copy(numericLocalCapture = fake), + compiled.copy(typeScript = compiled.typeScript + "// changed source"), + compiled.copy(resolvedModules = emptyMap()), + compiled.copy(program = compiled.program.copy(checks = emptyList())), + ) + for (changed in variants) { + val selected = selectScalarGuidance(fixture.inference, changed) + + assertEquals(2, selected.candidates.size) + assertTrue(selected.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(selected.excluded.isEmpty()) + } + val changedPoints = fixture.inference.relations.map { relation -> + relation.copy(pair = relation.pair.copy(left = relation.pair.left.copy(id = "other-result"))) + } + val relabeled = selectScalarGuidance(fixture.inference.copy(relations = changedPoints), compiled) + assertTrue(relabeled.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(relabeled.excluded.isEmpty()) + + val staleSources = fixture.inference.sources.map { it.copy(sha256 = "0".repeat(n = 64)) } + val stale = selectScalarGuidance(fixture.inference.copy(sources = staleSources), compiled) + assertTrue(stale.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + } + private fun ScalarRelation.changedResult( change: (PropertyPointEvent) -> PropertyPointEvent, ): ScalarRelation { @@ -259,8 +327,8 @@ class DslNumericLocalRelationTest { return copy(evidence = changed) } - private fun prepare(): Fixture { - val compiled = compile() + private fun prepare(originalEquality: Boolean = false): Fixture { + val compiled = compile(originalEquality) val capture = assertNotNull(compiled.numericLocalCapture) val sources = capture.observationRequest().sources + source(module = "functions.ts") val request = capture.observationRequest().copy(sources = sources) @@ -290,7 +358,7 @@ class DslNumericLocalRelationTest { return PropertyObservationSource(module, hash) } - private fun compile(): CompiledDslProperty { + private fun compile(originalEquality: Boolean): CompiledDslProperty { val source = """ export function transform(input: number): number { if (input === 417) return input - 1; @@ -304,7 +372,9 @@ class DslNumericLocalRelationTest { val other by int(min = 0, max = 1000) val result by value(transform(input)) - check(name = "bound") { result lessOrEqual input } + check(name = "bound") { + if (originalEquality) result equalTo input else result lessOrEqual input + } check(name = "other-input") { other lessOrEqual 1000 } } val compiled = PropertyTypeScriptCompiler().compile( diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt index 0ef91f053a..32f503d415 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCapture.kt @@ -107,3 +107,18 @@ internal fun SelectedDslNumericLocalCapture.compileCapture( return CompiledDslNumericLocalCapture(binding, result, inputPoint) } + +internal fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try { + val capture = requireNotNull(numericLocalCapture) + val regenerated = PropertyTypeScriptCompiler().compile( + program, + generatedModule = definition.predicate.module, + resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } }, + numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId), + ) + + definition == regenerated.definition && typeScript == regenerated.typeScript && + numericLocalCapture == regenerated.numericLocalCapture +} catch (_: IllegalArgumentException) { + false +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt new file mode 100644 index 0000000000..8018e7e713 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/inference/SelectScalarGuidance.kt @@ -0,0 +1,127 @@ +package org.usvm.ts.pbt.inference + +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyExpressionTerm +import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput +import org.usvm.ts.pbt.dsl.selectNumericLocalCapture +import org.usvm.ts.pbt.observation.ObservationPointKind + +/** KNOWN_DSL_CHECK identifies a direct original check, not a proved relation or executable body. */ +enum class ScalarGuidanceRelevance { KNOWN_DSL_CHECK, UNKNOWN } + +/** Selection decisions preserve each excluded relation and its original evidence. */ +enum class ScalarGuidanceExclusionReason { + NOT_SAMPLED, + DOMAIN_IMPLIED, + TAUTOLOGY, + DUPLICATE, + ORIGINAL_CHECK, + CANDIDATE_LIMIT, +} + +/** An empirical candidate whose exact symbolic support still needs a consumer's binding checks. */ +data class ScalarGuidanceCandidate(val relation: ScalarRelation, val relevance: ScalarGuidanceRelevance) + +/** An unselected relation; exclusion never removes it from the original inference. */ +data class ScalarGuidanceExclusion( + val relation: ScalarRelation, + val reason: ScalarGuidanceExclusionReason, + val relevance: ScalarGuidanceRelevance, +) + +/** Retains the complete original inference, including contradictory, insufficient and excluded evidence. */ +data class ScalarGuidanceSelection( + val inference: ScalarRelationInference, + val candidates: List, + val excluded: List, +) + +/** One bounded selection before USVM. The campaign decides whether UNKNOWN relevance may guide its search. */ +fun selectScalarGuidance( + inference: ScalarRelationInference, + compiled: CompiledDslProperty? = null, + maxCandidates: Int = 16, +): ScalarGuidanceSelection { + require(maxCandidates > 0) { "maxCandidates must be positive" } + + val original = originalCheck(inference, compiled) + val candidates = mutableListOf() + val excluded = mutableListOf() + for (relation in inference.relations) { + val known = original?.contains(relation.pair) == true + val relevance = if (known) ScalarGuidanceRelevance.KNOWN_DSL_CHECK else ScalarGuidanceRelevance.UNKNOWN + val duplicate = candidates.any { candidate -> candidate.relation.sameComparison(relation) } + val sampled = relation.status == ScalarRelationStatus.SAMPLED && relation.limitations.isEmpty() + val restatesOriginal = known && original?.implies(relation) == true + val reason = when { + !sampled -> ScalarGuidanceExclusionReason.NOT_SAMPLED + restatesOriginal -> ScalarGuidanceExclusionReason.ORIGINAL_CHECK + duplicate -> ScalarGuidanceExclusionReason.DUPLICATE + candidates.size >= maxCandidates -> ScalarGuidanceExclusionReason.CANDIDATE_LIMIT + else -> null + } + + if (reason == null) { + candidates += ScalarGuidanceCandidate(relation, relevance) + } else { + excluded += ScalarGuidanceExclusion(relation, reason, relevance) + } + } + for (relation in inference.domainImpliedRelations) { + val sameOriginalInput = relation.pair.left.kind == ObservationPointKind.ENTRY_ARGUMENT && + relation.pair.right.kind == ObservationPointKind.ENTRY_ARGUMENT && + relation.pair.left.inputIndex != null && relation.pair.left.inputIndex == relation.pair.right.inputIndex + val reason = if (sameOriginalInput) { + ScalarGuidanceExclusionReason.TAUTOLOGY + } else { + ScalarGuidanceExclusionReason.DOMAIN_IMPLIED + } + excluded += ScalarGuidanceExclusion(relation, reason, relevance = ScalarGuidanceRelevance.UNKNOWN) + } + + return ScalarGuidanceSelection(inference, candidates, excluded) +} + +private data class OriginalScalarCheck(val pair: ScalarObservationPair, val operator: String) { + fun contains(candidate: ScalarObservationPair): Boolean = candidate == pair || + candidate.left == pair.right && candidate.right == pair.left + + fun implies(relation: ScalarRelation): Boolean = operator == "===" || + operator == "<=" && relation.template == ScalarRelationTemplate.LESS_OR_EQUAL && relation.pair == pair +} + +private fun originalCheck( + inference: ScalarRelationInference, + compiled: CompiledDslProperty?, +): OriginalScalarCheck? { + if (compiled == null) return null + + val sameProperty = compiled.definition == inference.property && compiled.definition.id == inference.propertyId + if (!sameProperty) return null + if (!compiled.isReproducibleCompilerOutput()) return null + + val capture = compiled.numericLocalCapture ?: return null + val source = inference.sources.singleOrNull { it.module == compiled.definition.predicate.module } + if (source?.sha256 != capture.binding.sourceSha256) return null + + val request = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId) + val selected = compiled.program.selectNumericLocalCapture(request) + val comparison = selected.check.expression.term as PropertyExpressionTerm.Operation + val pair = if (selected.resultOperandIndex == 0) { + ScalarObservationPair(capture.result, capture.input) + } else { + ScalarObservationPair(capture.input, capture.result) + } + + return OriginalScalarCheck(pair, comparison.operator) +} + +private fun ScalarRelation.sameComparison(other: ScalarRelation): Boolean { + if (template != other.template) return false + + val reversed = template == ScalarRelationTemplate.STRICT_EQUAL && + pair.left == other.pair.right && pair.right == other.pair.left + + return pair == other.pair || reversed +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt index 18e85f9d17..236f1158e0 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt @@ -5,8 +5,7 @@ import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNumberType import org.usvm.ts.pbt.dsl.CompiledDslProperty -import org.usvm.ts.pbt.dsl.DslNumericLocalCapture -import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.dsl.isReproducibleCompilerOutput import org.usvm.ts.pbt.inference.ScalarRelation import org.usvm.ts.pbt.inference.ScalarRelationInference import org.usvm.ts.pbt.inference.ScalarRelationStatus @@ -212,21 +211,6 @@ private fun CompiledDslProperty.matchesPinnedSources( false } -private fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try { - val capture = requireNotNull(numericLocalCapture) - val regenerated = PropertyTypeScriptCompiler().compile( - program, - generatedModule = definition.predicate.module, - resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } }, - numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId), - ) - - definition == regenerated.definition && typeScript == regenerated.typeScript && - numericLocalCapture == regenerated.numericLocalCapture -} catch (_: IllegalArgumentException) { - false -} - private fun EtsMethod.storesAt( point: PropertySourcePoint, localName: String, diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt index 47fefa6a5b..17818cd643 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/DomainImpliedScalarRelationTest.kt @@ -47,6 +47,9 @@ class DomainImpliedScalarRelationTest { assertEquals(ScalarRelationStatus.REFUTED, result.relations.single().status) assertEquals(SOURCES, result.sources) assertEquals(property, result.property) + val selected = selectScalarGuidance(result) + val excludedOrder = selected.excluded.single { it.relation == implied } + assertEquals(ScalarGuidanceExclusionReason.DOMAIN_IMPLIED, excludedOrder.reason) } @Test @@ -79,6 +82,29 @@ class DomainImpliedScalarRelationTest { assertTrue(result.domainImpliedRelations.all { it.status == ScalarRelationStatus.SAMPLED }) } + @Test + fun `guidance reuses domain facts and keeps NaN capable reflexive comparisons as unknown candidates`() { + val pair = ScalarObservationPair(LEFT, RIGHT.copy(inputIndex = 0)) + val samples = listOf(sample(id = 0, left = 0.0, right = 0.0), sample(id = 1, left = 1.0, right = 1.0)) + val snapshots = samples.map { invocation -> + invocation.copy(points = listOf(invocation.points.first(), invocation.points.last().copy(inputIndex = 0))) + } + val integers = property(IntegerDomain(min = 0, max = 1), IntegerDomain(min = 0, max = 1)) + val numbers = property(NumberDomain(), IntegerDomain(min = 0, max = 1)) + val tautologies = infer(integers, snapshots, pair) + val nanCapable = infer(numbers, snapshots, pair) + + val excluded = selectScalarGuidance(tautologies) + val retained = selectScalarGuidance(nanCapable) + + assertTrue(excluded.candidates.isEmpty()) + assertEquals(tautologies.domainImpliedRelations, excluded.excluded.map { it.relation }) + assertTrue(excluded.excluded.all { it.reason == ScalarGuidanceExclusionReason.TAUTOLOGY }) + assertEquals(nanCapable.relations, retained.candidates.map { it.relation }) + assertTrue(retained.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertTrue(retained.excluded.isEmpty()) + } + @Test fun `ordinary argument labels never establish input identity even when every sample matches`() { val left = LEFT.copy(kind = ObservationPointKind.ARGUMENT) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt index 815a89dd56..d74b74d517 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/inference/InferScalarRelationsTest.kt @@ -28,6 +28,7 @@ import org.usvm.ts.pbt.observation.PropertyObservationValue import org.usvm.ts.pbt.observation.PropertyPointEvent import kotlin.test.assertEquals import kotlin.test.assertFailsWith +import kotlin.test.assertSame import kotlin.test.assertTrue class InferScalarRelationsTest { @@ -295,6 +296,59 @@ class InferScalarRelationsTest { } } + @Test + fun `guidance selection removes symmetric equality duplicates without merging temporal identities`() { + val samples = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val observations = artifact(samples) + val reversed = ScalarObservationPair(RIGHT, LEFT) + val inference = inferScalarRelations(PROPERTY, observations, listOf(PAIR, reversed)) + + val selected = selectScalarGuidance(inference) + + assertSame(inference, selected.inference) + assertEquals(3, selected.candidates.size) + assertTrue(selected.candidates.all { it.relevance == ScalarGuidanceRelevance.UNKNOWN }) + assertEquals(ScalarGuidanceExclusionReason.DUPLICATE, selected.excluded.single().reason) + assertEquals(reversed, selected.excluded.single().relation.pair) + assertEquals(ScalarRelationTemplate.STRICT_EQUAL, selected.excluded.single().relation.template) + val duplicateEvidence = selected.excluded.single().relation.evidence + assertEquals(samples, duplicateEvidence.map { it.invocation }) + + val equality = selected.candidates.first().relation + val later = equality.copy(pair = equality.pair.copy(right = RIGHT.copy(kind = ObservationPointKind.POST))) + val differentTimes = inference.copy(relations = listOf(equality, later)) + assertEquals(2, selectScalarGuidance(differentTimes).candidates.size) + } + + @Test + fun `empty finite and contradicted evidence gives no guidance without losing the original artifact`() { + val samples = listOf(invocation(id = 0, left = 1.0, right = 1.0)) + val insufficient = infer(samples) + val contradicted = infer(samples + invocation(id = 1, left = 1.0, right = 0.0)) + + for (inference in listOf(infer(emptyList()), insufficient, contradicted)) { + val selected = selectScalarGuidance(inference) + + assertSame(inference, selected.inference) + assertTrue(selected.candidates.isEmpty()) + assertEquals(inference.relations, selected.excluded.map { it.relation }) + assertTrue(selected.excluded.all { it.reason == ScalarGuidanceExclusionReason.NOT_SAMPLED }) + } + } + + @Test + fun `guidance candidates are bounded in original selection order and overflow evidence is retained`() { + val samples = listOf(invocation(id = 0, left = 0.0, right = 0.0), invocation(id = 1, left = 1.0, right = 1.0)) + val inference = infer(samples) + + val selected = selectScalarGuidance(inference, maxCandidates = 1) + + assertEquals(inference.relations.first(), selected.candidates.single().relation) + assertEquals(inference.relations.last(), selected.excluded.single().relation) + assertEquals(ScalarGuidanceExclusionReason.CANDIDATE_LIMIT, selected.excluded.single().reason) + assertFailsWith { selectScalarGuidance(inference, maxCandidates = 0) } + } + private fun infer(samples: List): ScalarRelationInference = inferScalarRelations(PROPERTY, artifact(samples), listOf(PAIR))