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 c0b12dad63..caf4e4de24 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 @@ -21,6 +21,11 @@ export interface WitnessTarget { role: 'PROPERTY' | 'COVERAGE' | 'HYPOTHESIS'; binding?: WitnessBinding; expectedOutcome?: 'FALSE' | 'THREW'; + entryRelation?: { + leftInputIndex: number; + rightInputIndex: number; + template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL'; + }; } export interface WitnessEvent { @@ -247,9 +252,22 @@ async function replayOnce( const result: WitnessNativeReplay = { admission: 'ADMITTED', outcome: 'HOLDS', targetMatched: false, events: context.events, runtimeVersion: process.version, }; + const relation = target.entryRelation; + const left = relation === undefined ? undefined : values[relation.leftInputIndex]; + const right = relation === undefined ? undefined : values[relation.rightInputIndex]; + if (relation !== undefined && (typeof left !== 'number' || typeof right !== 'number')) { + return { ...result, admission: 'UNKNOWN', outcome: 'UNKNOWN', diagnostic: 'entry-relation-numeric-required' }; + } + const entryEvent: WitnessEvent | undefined = relation === undefined ? undefined : { + binding: target.binding!, guard: true, + holds: relation.template === 'STRICT_EQUAL' ? left === right : (left as number) <= (right as number), + }; try { const holds = await contexts.run(context, () => invokePropertyOnce( - values, predicate, precondition, undefined, 'replay', () => { context.active = true; }, + values, predicate, precondition, undefined, 'replay', () => { + context.active = true; + if (entryEvent !== undefined) context.events.push(entryEvent); + }, )); if (holds === null) { result.admission = 'PRECONDITION_REJECTED'; @@ -316,12 +334,19 @@ function validateOperation(value: unknown, arity: number): WitnessOperation { && typeof binding.contextId === 'string' && binding.contextId.length > 0 && typeof binding.revision === 'string' && binding.revision.length > 0 && Number.isInteger(binding.occurrence) && binding.occurrence >= 0); + const relation = target?.entryRelation; + const validEntryRelation = relation === undefined || (relation !== null && typeof relation === 'object' + && !Array.isArray(relation) && target?.role === 'HYPOTHESIS' + && binding?.contextId === 'original-entry' && binding.occurrence === 0 + && Number.isInteger(relation.leftInputIndex) && relation.leftInputIndex >= 0 && relation.leftInputIndex < arity + && Number.isInteger(relation.rightInputIndex) && relation.rightInputIndex >= 0 && relation.rightInputIndex < arity + && ['STRICT_EQUAL', 'LESS_OR_EQUAL'].includes(relation.template)); const valid = operation !== undefined && ['replay', 'reduce'].includes(operation.mode) && Array.isArray(operation.inputs) && operation.inputs.length === arity && typeof target?.id === 'string' && target.id.length > 0 && ['PROPERTY', 'COVERAGE', 'HYPOTHESIS'].includes(target.role) && (target.expectedOutcome === undefined || ['FALSE', 'THREW'].includes(target.expectedOutcome)) - && validBinding && (target.role === 'PROPERTY' || binding !== undefined) + && validBinding && validEntryRelation && (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/external-witness.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts index 644e2f9019..902045ce62 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/external-witness.test.ts @@ -11,6 +11,103 @@ const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../../. const module = 'properties/witness/ExternalWitness.ts'; const sha256 = createHash('sha256').update(await readFile(path.join(root, module))).digest('hex'); const binding = (pointId: string) => ({ pointId, contextId: 'original', revision: 'v1', occurrence: 0 }); +const entryModule = 'properties/inference/EntryRelations.ts'; +const entryHash = createHash('sha256').update(await readFile(path.join(root, entryModule))).digest('hex'); + +function entryRequest( + left: number, right: number, template: 'STRICT_EQUAL' | 'LESS_OR_EQUAL' = 'LESS_OR_EQUAL', predicate = 'always', +) { + const target: WitnessTarget = { + id: 'entry-relation', role: 'HYPOTHESIS', + binding: { pointId: 'entry-relation', contextId: 'original-entry', revision: entryHash, occurrence: 0 }, + entryRelation: { leftInputIndex: 0, rightInputIndex: 1, template }, + }; + const domain = { kind: 'number', min: { value: 'negative-infinity' }, max: { value: 'positive-infinity' }, allowNaN: true }; + + return { + manifest: { + propertyId: 'witness.entry', predicate: { module: entryModule, exportName: predicate, executionKind: 'sync' }, + inputs: [{ name: 'left', domain }, { name: 'right', domain }], assertions: [], + }, + sourceRoots: [root], examples: [], numRuns: 1, timeoutMillis: 5000, + witness: { + mode: 'replay', target, inputs: [encodeJsValue(left), encodeJsValue(right)], + sources: [{ module: entryModule, sha256: entryHash }], + }, + }; +} + +test('adapter-owned entry comparisons retain JavaScript NaN signed-zero and infinity semantics', async () => { + const cases = [ + [-0, 0, 'STRICT_EQUAL', true], + [Number.NaN, Number.NaN, 'STRICT_EQUAL', false], + [Number.POSITIVE_INFINITY, Number.POSITIVE_INFINITY, 'STRICT_EQUAL', true], + [Number.NEGATIVE_INFINITY, Number.POSITIVE_INFINITY, 'LESS_OR_EQUAL', true], + [Number.POSITIVE_INFINITY, Number.NEGATIVE_INFINITY, 'LESS_OR_EQUAL', false], + [Number.NaN, 0, 'LESS_OR_EQUAL', false], + ] as const; + + for (const [left, right, template, holds] of cases) { + const replay = (await executeWitness(entryRequest(left, right, template))).witnessReplay; + + assert.equal(replay?.outcome, 'HOLDS'); + assert.equal(replay?.events[0]?.holds, holds); + assert.equal(replay?.targetMatched, !holds); + } +}); + +test('entry refutation snapshots precede callback mutation and only admitted inputs receive an event', async () => { + const mutation = (await executeWitness(entryRequest(80, 0, 'LESS_OR_EQUAL', 'entryMutation'))).witnessReplay; + const rejected = entryRequest(80, 0); + const guarded = { ...rejected, manifest: { + ...rejected.manifest, precondition: { module: entryModule, exportName: 'ordered', executionKind: 'sync' }, + } }; + + const skipped = (await executeWitness(guarded)).witnessReplay; + + assert.equal(mutation?.outcome, 'HOLDS'); + assert.equal(mutation?.events[0]?.holds, false); + assert.equal(mutation?.targetMatched, true); + assert.equal(skipped?.admission, 'PRECONDITION_REJECTED'); + assert.equal(skipped?.targetMatched, false); + assert.deepEqual(skipped?.events, []); +}); + +test('native reduction retains the same admitted entry relation and holding original oracle', async () => { + const initial = entryRequest(80, 0); + const domain = { kind: 'integer', min: 0, max: 100 }; + const selected = { ...initial, manifest: { + ...initial.manifest, inputs: [{ name: 'left', domain }, { name: 'right', domain }], + } }; + const expected = (await executeWitness(selected)).witnessReplay; + + const reduced = (await executeWitness({ ...selected, witness: { ...selected.witness, mode: 'reduce', expected } })).witnessReduction; + const final = (await executeWitness({ ...selected, witness: { ...selected.witness, inputs: reduced?.inputs } })).witnessReplay; + + assert.equal(reduced?.status, 'EXHAUSTED'); + assert.ok((reduced?.acceptedShrinks ?? 0) > 0); + assert.deepEqual(reduced?.inputs, [encodeJsValue(1), encodeJsValue(0)]); + assert.equal(final?.outcome, 'HOLDS'); + assert.equal(final?.targetMatched, true); + assert.deepEqual(final?.events[0]?.binding, initial.witness.target.binding); +}); + +test('entry target indices templates context and occurrence are validated before execution', async () => { + const original = entryRequest(80, 0); + const target = original.witness.target; + const cases = [ + { ...target, entryRelation: { ...target.entryRelation!, leftInputIndex: -1 } }, + { ...target, entryRelation: { ...target.entryRelation!, rightInputIndex: 2 } }, + { ...target, entryRelation: { ...target.entryRelation!, template: 'COERCING_EQUAL' } }, + { ...target, binding: { ...target.binding!, contextId: 'helper' } }, + { ...target, binding: { ...target.binding!, occurrence: 1 } }, + ]; + + for (const selected of cases) { + await assert.rejects(executeWitness({ ...original, witness: { ...original.witness, target: selected } }), + (error: unknown) => error instanceof ProtocolError && error.code === 'protocol.request.invalid'); + } +}); function request(predicate: string, target: WitnessTarget = { id: predicate, role: 'PROPERTY' }, inputs = [encodeJsValue(80)]) { return { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckWitnessCoordinator.kt index 6eca5ffd23..d6312881f9 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 @@ -303,6 +303,13 @@ internal class FastCheckWitnessCoordinator( if (!inputs.hasWitnessEncoding()) return WitnessReplayStatus.UNREPRESENTABLE_INPUT if (!inDeclaredSupport(property, inputs)) return WitnessReplayStatus.DOMAIN_REJECTED + val entryRelation = candidate.target.entryRelation + if (entryRelation != null) { + val numericInputs = inputs.getOrNull(entryRelation.leftInputIndex) is JsConcreteValue.Number && + inputs.getOrNull(entryRelation.rightInputIndex) is JsConcreteValue.Number + if (!numericInputs) return WitnessReplayStatus.UNSUPPORTED_REPLAY + } + val 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/EntryRelationRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt new file mode 100644 index 0000000000..25f8700d1d --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt @@ -0,0 +1,254 @@ +package org.usvm.ts.pbt.inference + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessOracleOutcome +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.PropertyAssertion +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.PropertyOperand +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationRequest +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmEntryRefutationStatus +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefutation +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefuter +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import java.nio.file.Files +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class EntryRelationRefutationTest { + private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + @Test + fun `an auxiliary equality refutation is confirmed while the complete original property holds`() { + val inference = observe(predicate = "reflexive") + val relation = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val manifest = inference.property.toManifest() + val focused = UsvmPropertySearcher(scene).searchFocusedOnEntryRelation( + manifest, + mapper.map(manifest), + CONCRETE, + inference, + relation, + ) + + val refutation = refute(inference, relation) + val candidate = refutation.captureWitness() + val native = backend.confirmWitness(inference.property, candidate, CONFIGURATION) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, focused.search?.status) + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(EtsMappingStatus.EXACT, refutation.binding.status) + assertEquals(WitnessRole.HYPOTHESIS, candidate.target.role) + assertEquals(ObservationBuildStatus.UNVERIFIED, refutation.inference.buildStatus) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + assertEquals(WitnessOracleOutcome.HOLDS, native.reducedReplay?.outcome) + assertEquals(refutation.inputs, native.candidate.inputs) + assertEquals(candidate.target.binding, native.contextualRefutations.single().binding) + } + + @Test + fun `an original oracle violation has priority over a confirmed entry hypothesis refutation`() { + val cases = listOf("ordered" to WitnessOracleOutcome.FALSE, "throwing" to WitnessOracleOutcome.THREW) + for ((predicate, outcome) in cases) { + val inference = observe(predicate = predicate) + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + val refutation = refute(inference, order) + val native = backend.confirmWitness(inference.property, refutation.captureWitness(), CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, native.status, native.diagnostic) + assertEquals(outcome, native.originalReplay?.outcome) + assertTrue(assertNotNull(native.originalReplay).targetMatched) + assertTrue(native.contextualRefutations.isNotEmpty()) + } + } + + @Test + fun `the complete original precondition can reject every proposed refutation`() { + val inference = observe(predicate = "reflexive", precondition = "ordered") + val order = inference.relations.single { it.template == ScalarRelationTemplate.LESS_OR_EQUAL } + + val refutation = refute(inference, order) + + assertEquals(UsvmEntryRefutationStatus.PRECONDITION_REJECTED, refutation.status) + assertNull(refutation.inputs) + } + + @Test + fun `a runtime bound inside original admission remains unsupported rather than absence of refutations`() { + val inference = observe(predicate = "reflexive", precondition = "sparseAdmission") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + + val refutation = refute(inference, equality) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, refutation.status) + assertNull(refutation.inputs) + assertTrue(refutation.diagnostics.any { it.code == "usvm.runtime.array-index-growth" }) + } + + @Test + fun `same entry equality can be refuted by NaN while the original property still holds`() { + val points = listOf(LEFT, RIGHT.copy(inputIndex = 0)) + val inference = observe(predicate = "always", leftDomain = NumberDomain(), points = points, seed = 2) + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + + val refutation = refute(inference, equality) + val native = backend.confirmWitness(inference.property, refutation.captureWitness(), CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.REFUTATION_REACHED, refutation.status) + val first = assertNotNull(refutation.inputs).first() as JsConcreteValue.Number + assertTrue(first.toDouble().isNaN()) + assertEquals(WitnessReplayStatus.CONFIRMED_HYPOTHESIS_REFUTATION, native.status, native.diagnostic) + assertEquals(WitnessOracleOutcome.HOLDS, native.originalReplay?.outcome) + } + + @Test + fun `stale observation sources cannot activate a challenge and stale native sources preserve the candidate`() { + val inference = observe(predicate = "reflexive") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val stale = listOf(PropertyObservationSource(module = MODULE, sha256 = "0".repeat(n = 64))) + + val staleBinding = refute(inference.copy(sources = stale), equality) + val refutation = refute(inference, equality) + val candidate = refutation.captureWitness().copy(sources = stale) + val native = backend.confirmWitness(inference.property, candidate, CONFIGURATION) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, staleBinding.status) + assertNull(staleBinding.inputs) + assertEquals(WitnessReplayStatus.SOURCE_MISMATCH, native.status) + assertEquals(refutation.inputs, native.candidate.inputs) + } + + @Test + fun `a timed out auxiliary search is not an exhausted relation`() { + val inference = observe(predicate = "reflexive") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val limited = UsvmEntryRelationRefuter( + scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = Duration.ZERO), + ) + val manifest = inference.property.toManifest() + + val refutation = limited.refute(manifest, mapper.map(manifest), CONCRETE, inference, equality) + + assertEquals(UsvmEntryRefutationStatus.TIMEOUT, refutation.status) + assertTrue(refutation.timedOut) + assertNull(refutation.inputs) + } + + private fun refute(inference: ScalarRelationInference, relation: ScalarRelation): UsvmEntryRelationRefutation { + val manifest = inference.property.toManifest() + + return UsvmEntryRelationRefuter(scene).refute(manifest, mapper.map(manifest), CONCRETE, inference, relation) + } + + private fun observe( + predicate: String, + precondition: String? = null, + leftDomain: PropertyDomain = IntegerDomain(min = 0, max = 2), + points: List = listOf(LEFT, RIGHT), + seed: Int = 1, + ): ScalarRelationInference { + val property = PropertyDefinition( + id = PropertyId("entry.auxiliary"), + inputs = listOf( + PropertyInput(name = "left", domain = leftDomain), + PropertyInput(name = "right", domain = IntegerDomain(min = 0, max = 2)), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = predicate), + precondition = precondition?.let { TypeScriptEntryPoint(module = MODULE, exportName = it) }, + assertions = listOf( + PropertyAssertion( + id = "original", + source = CALL, + testedCall = CALL, + operands = points.map { PropertyOperand(id = it.operandId, source = it.source) }, + ), + ), + ) + + val result = backend.run( + property, + PropertyRunConfiguration( + seed = seed, + numRuns = 2, + observationRequest = PropertyObservationRequest(points = points, sources = sources), + ), + ) + + return inferScalarRelations( + property, + assertNotNull(result.observations), + listOf(ScalarObservationPair(points[0], points[1])) + ) + } + + companion object { + private const val MODULE = "properties/inference/EntryRelations.ts" + private val CALL = PropertySourcePoint(module = MODULE, line = 1, column = 1) + private val LEFT = PropertyObservationPoint( + id = "left", + assertionId = "original", + operandId = "left", + source = CALL, + callSite = CALL, + kind = ObservationPointKind.ENTRY_ARGUMENT, + inputIndex = 0, + ) + private val RIGHT = LEFT.copy(id = "right", operandId = "right", inputIndex = 1) + private val CONCRETE = ProjectionCapability(level = ProjectionLevel.EXACT) + private val CONFIGURATION = WitnessReplayConfiguration(timeoutMillis = 15_000, validationReserveMillis = 3_000) + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private lateinit var sources: List + + @JvmStatic + @BeforeAll + fun loadFixture() { + val root = testResourcesRoot() + val source = root.resolve(MODULE) + val bytes = Files.readAllBytes(source) + val hash = MessageDigest.getInstance("SHA-256").digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) } + sources = listOf(PropertyObservationSource(module = MODULE, sha256 = hash)) + scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + mapper = PropertyEtsMapper(scene, sourceRoots = listOf(root, source.parent)) + } + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts index 36dfdb76b4..c2a7417fc0 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts +++ b/usvm-ts-fast-check/src/test/resources/properties/inference/EntryRelations.ts @@ -13,3 +13,23 @@ export function nonNegative(left: number, right: number): boolean { export function independent(left: number, right: number): boolean { return left !== 1; } + +export function always(left: number, right: number): boolean { + return true; +} + +export function sparseAdmission(left: number, right: number): boolean { + const cache: number[] = []; + cache[9] = left; + return right === right; +} + +export function entryMutation(left: number, right: number): boolean { + left = right; + return left === right; +} + +export function throwing(left: number, right: number): boolean { + if (left > right) throw new Error('original fault'); + return true; +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt new file mode 100644 index 0000000000..e525371c29 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/EntryRelationWitnessCapture.kt @@ -0,0 +1,39 @@ +package org.usvm.ts.pbt.backend + +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmEntryRefutationStatus +import org.usvm.ts.pbt.usvm.UsvmEntryRelationRefutation + +/** The exact entry transport binding is independent of the still-unverified executable body. */ +fun UsvmEntryRelationRefutation.captureWitness( + sources: List = inference.sources, +): ExternalWitnessCandidate { + val reached = status == UsvmEntryRefutationStatus.REFUTATION_REACHED || + status == UsvmEntryRefutationStatus.FAILED_INPUT_RESOLUTION + require(reached) { "An entry relation witness requires a reached auxiliary target" } + + val selected = binding.targets.single() + val relation = selected.relation + val left = relation.pair.left + val right = relation.pair.right + val targetId = "${left.assertionId}:${left.id}:${relation.template}:${right.id}" + val property = inference.property + val revision = property.witnessManifestSha256() + val target = WitnessTarget( + id = targetId, + role = WitnessRole.HYPOTHESIS, + binding = WitnessBinding( + pointId = targetId, + contextId = WitnessEntryRelation.CONTEXT_ID, + revision = revision, + ), + entryRelation = WitnessEntryRelation(selected.leftInputIndex, selected.rightInputIndex, relation.template), + ) + + return property.captureWitness( + inputs = inputs, + target = target, + sources = sources, + provenance = "usvm:entry-refutation:${inference.runId}:${inference.buildStatus}:$status", + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt index 8600ed1326..7be38678cc 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ExternalWitness.kt @@ -1,6 +1,7 @@ package org.usvm.ts.pbt.backend import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.inference.ScalarRelationTemplate import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId @@ -10,6 +11,22 @@ import org.usvm.ts.pbt.observation.PropertyObservationSource @Serializable enum class WitnessRole { PROPERTY, COVERAGE, HYPOTHESIS } +/** Adapter-owned comparison of two original numeric inputs, before the original callback runs. */ +@Serializable +data class WitnessEntryRelation( + val leftInputIndex: Int, + val rightInputIndex: Int, + val template: ScalarRelationTemplate, +) { + init { + require(leftInputIndex >= 0 && rightInputIndex >= 0) + } + + companion object { + const val CONTEXT_ID = "original-entry" + } +} + /** Exact executable hook binding supplied by a producer, never inferred from a source line. */ @Serializable data class WitnessBinding( @@ -31,10 +48,15 @@ data class WitnessTarget( val role: WitnessRole = WitnessRole.PROPERTY, val binding: WitnessBinding? = null, val expectedOutcome: WitnessOracleOutcome? = null, + val entryRelation: WitnessEntryRelation? = null, ) { init { require(id.isNotBlank()) require(role == WitnessRole.PROPERTY || binding != null) + if (entryRelation != null) { + require(role == WitnessRole.HYPOTHESIS) + require(binding?.contextId == WitnessEntryRelation.CONTEXT_ID && binding.occurrence == 0) + } require( expectedOutcome == null || expectedOutcome == WitnessOracleOutcome.FALSE || expectedOutcome == WitnessOracleOutcome.THREW 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 d97b6763a5..b36d5f8b0f 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,5 +1,6 @@ package org.usvm.ts.pbt.inference +import kotlinx.serialization.Serializable import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId @@ -16,6 +17,7 @@ data class ScalarObservationPair( ) /** Numeric JavaScript comparisons; no mathematical-real or coercing comparison is inferred. */ +@Serializable enum class ScalarRelationTemplate { STRICT_EQUAL, LESS_OR_EQUAL, 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 2dd734bed3..043fb45e79 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 @@ -1,9 +1,13 @@ package org.usvm.ts.pbt.usvm +import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsNumberType +import org.usvm.UBoolExpr +import org.usvm.machine.state.TsState import org.usvm.ts.pbt.inference.ScalarRelation import org.usvm.ts.pbt.inference.ScalarRelationInference import org.usvm.ts.pbt.inference.ScalarRelationStatus +import org.usvm.ts.pbt.inference.ScalarRelationTemplate import org.usvm.ts.pbt.inference.matches import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.manifest.toManifest @@ -29,6 +33,20 @@ data class UsvmEntryRelationBinding( val relation: ScalarRelation, ) +internal fun UsvmEntryRelationBinding.negatedRelation( + state: TsState, + projection: UsvmDeclaredDomainProjection, +): UBoolExpr = with(state.ctx) { + val leftValue = projection.inputs[leftInputIndex].value.asExpr(fp64Sort) + val rightValue = projection.inputs[rightInputIndex].value.asExpr(fp64Sort) + val hypothesis = when (relation.template) { + ScalarRelationTemplate.STRICT_EQUAL -> mkFpEqualExpr(leftValue, rightValue) + ScalarRelationTemplate.LESS_OR_EQUAL -> mkFpLessOrEqualExpr(leftValue, rightValue) + } + + hypothesis.not() +} + /** An explicitly focused original-property search; no-finding does not exhaust the original domain. */ data class UsvmEntryRelationSearchResult( val binding: EtsMappingResult, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt new file mode 100644 index 0000000000..b73dc0d242 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEntryRelationRefuter.kt @@ -0,0 +1,266 @@ +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 +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +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, +} + +/** 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 inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, + val timedOut: Boolean = false, +) { + init { + require(status != UsvmEntryRefutationStatus.REFUTATION_REACHED || inputs != null) + require(inputs == null || binding.status == EtsMappingStatus.EXACT) + } +} + +/** + * Searches domain AND original admission AND NOT(entry relation), without negating the original oracle. + * The standalone machine uses the supplied timeout; the campaign owns its shared deadline and cancellation. + */ +class UsvmEntryRelationRefuter( + private val scene: EtsScene, + machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + private val 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), + ) + + fun refute( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + inference: ScalarRelationInference, + relation: ScalarRelation, + ): UsvmEntryRelationRefutation { + val binding = bindEntryRelation(manifest, mapping, inference, relation) + val capability = UsvmProjectionCapabilityResolver(scene).resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + val unsupported = binding.status != EtsMappingStatus.EXACT || + capability.symbolic.level == ProjectionLevel.UNSUPPORTED + if (unsupported) { + return UsvmEntryRelationRefutation( + inference = inference, + binding = binding, + status = UsvmEntryRefutationStatus.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 + } +} + +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) + } + + 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 + } + 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 + } + } +} 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 c2e809b4a2..9e77f4a11f 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 @@ -26,7 +26,6 @@ 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 @@ -146,16 +145,7 @@ class UsvmPropertySearcher( 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() - } + state.pathConstraints += focus.negatedRelation(state, projection) } if (precondition != null) { state.prependBooleanEntryPointGuard(