diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt index 06242ca2d5..17328a48d2 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/EntryRelationRefutationTest.kt @@ -1,5 +1,7 @@ package org.usvm.ts.pbt.inference +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.Json import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert @@ -7,6 +9,7 @@ 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.CapabilityDiagnostic import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel import org.usvm.ts.pbt.backend.PropertyRunConfiguration @@ -52,6 +55,23 @@ import kotlin.time.Duration class EntryRelationRefutationTest { private val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + @Test + fun `unknown call in original admission retains its reason before the auxiliary target`() { + val inference = observe(predicate = "reflexive", precondition = "sliceAdmission") + val equality = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + + val refutation = refute(inference, equality) + val restored = Json.decodeFromString>(Json.encodeToString(refutation.diagnostics)) + + assertEquals(UsvmEntryRefutationStatus.UNSUPPORTED, refutation.status) + assertNull(refutation.inputs) + val diagnostic = restored.single { it.code == "usvm.unknown-call.path-stopped" } + assertTrue("Array::slice" in diagnostic.message, diagnostic.message) + assertTrue("reason=PARTIAL_APPROXIMATION" in diagnostic.message, diagnostic.message) + assertTrue(diagnostic.path.contains("EntryRelations.ts:39:"), diagnostic.path) + assertEquals(refutation.diagnostics, restored) + } + @Test fun `an auxiliary equality refutation is confirmed while the complete original property holds`() { val inference = observe(predicate = "reflexive") 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 c2a7417fc0..6c0c1f6af2 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 @@ -33,3 +33,8 @@ export function throwing(left: number, right: number): boolean { if (left > right) throw new Error('original fault'); return true; } + +export function sliceAdmission(left: number, right: number): boolean { + const values = [left, right]; + return values.slice().length === 2; +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt index 994f9eee79..46f802c3c9 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRelationRefutationSearch.kt @@ -12,6 +12,7 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsMachineAnalysisResult import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsEntryPointGuardOutcome import org.usvm.machine.state.TsState @@ -200,6 +201,10 @@ internal open class UsvmRelationRefutationObserver : TsInterpreterObserver { override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { runtimeLimitations.onRuntimeFeatureLimitation(event) } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + runtimeLimitations.onUnknownCall(event) + } } private fun resolveInputs( diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt index 1318a16ec1..120de8f535 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserver.kt @@ -1,7 +1,10 @@ package org.usvm.ts.pbt.usvm +import org.jacodb.ets.model.EtsStmt import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallOutcome import org.usvm.ts.pbt.backend.CapabilityDiagnostic /** Retains a bounded sample of distinct model boundaries without keeping live engine objects. */ @@ -13,22 +16,28 @@ internal class UsvmRuntimeLimitationObserver : TsInterpreterObserver { get() = limitations.toList() + if (truncated) listOf(TRUNCATED_DIAGNOSTIC) else emptyList() override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { - val location = event.statement.location - val origin = location.origin - val path = if (origin != null) { - // EtsIR origins use zero-based positions; diagnostics use ordinary editor coordinates. - "${origin.fileName}:${origin.startLine + 1}:${origin.startColumn + 1}-" + - "${origin.endLine + 1}:${origin.endColumn + 1}" - } else { - val method = location.method.signature - val source = method.enclosingClass.file.fileName - "$source#${method.name}[${location.index}]" - } val diagnostic = CapabilityDiagnostic( code = "usvm.runtime.${event.reason.name.lowercase().replace('_', '-')}", message = "${event.reason.name}: ${event.detail}; statement: ${event.statement}", - path = path, + path = event.statement.diagnosticPath(), + ) + record(diagnostic) + } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + if (event.outcome == TsUnknownCallOutcome.MODEL_APPLIED) return + + val outcome = event.outcome.name.lowercase().replace('_', '-') + val diagnostic = CapabilityDiagnostic( + code = "usvm.unknown-call.$outcome", + message = "${event.outcome.name}: ${event.callee}; reason=${event.failureReason.name}; " + + "statement: ${event.callSite}", + path = event.callSite.diagnosticPath(), ) + record(diagnostic) + } + + private fun record(diagnostic: CapabilityDiagnostic) { if (diagnostic in limitations) return if (limitations.size < MAX_DIAGNOSTICS) { @@ -47,3 +56,16 @@ internal class UsvmRuntimeLimitationObserver : TsInterpreterObserver { ) } } + +private fun EtsStmt.diagnosticPath(): String { + val origin = location.origin + if (origin != null) { + // EtsIR origins use zero-based positions; diagnostics use ordinary editor coordinates. + return "${origin.fileName}:${origin.startLine + 1}:${origin.startColumn + 1}-" + + "${origin.endLine + 1}:${origin.endColumn + 1}" + } + + val method = location.method.signature + val source = method.enclosingClass.file.fileName + return "$source#${method.name}[${location.index}]" +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt index bee127d202..70d4e5c7d4 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -1,5 +1,7 @@ package org.usvm.ts.pbt.usvm +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.Json import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert @@ -34,6 +36,30 @@ import kotlin.test.assertTrue import kotlin.time.Duration class UsvmPropertySearcherTest { + @Test + fun `unknown call diagnostics survive public result serialization`() { + assertUnknownCallDiagnostic( + predicate = "unsupportedSliceProperty", + callee = "Array::slice", + reason = "PARTIAL_APPROXIMATION", + sourceLine = 154, + ) + assertUnknownCallDiagnostic( + predicate = "unsupportedTypedArrayProperty", + callee = "Float64Array::constructor", + reason = "RECEIVER_CLASS_NOT_FOUND", + sourceLine = 158, + ) + } + + @Test + fun `an applied call model does not introduce an unknown call limitation`() { + val result = search(manifest(predicateExport = "modeledAbsoluteProperty")) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + assertTrue(result.diagnostics.none { it.code.startsWith("usvm.unknown-call.") }, result.diagnostics.toString()) + } + @Test fun `reports when no violation is reachable`() { val manifest = manifest(predicateExport = "validProperty") @@ -355,6 +381,19 @@ class UsvmPropertySearcherTest { assertNull(result.inputs) } + private fun assertUnknownCallDiagnostic(predicate: String, callee: String, reason: String, sourceLine: Int) { + val result = search(manifest(predicateExport = predicate)) + val restored = Json.decodeFromString(Json.encodeToString(result)) + + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, restored.status) + val diagnostic = restored.diagnostics.single { it.code == "usvm.unknown-call.path-stopped" } + assertTrue(callee in diagnostic.message, diagnostic.message) + assertTrue("reason=$reason" in diagnostic.message, diagnostic.message) + assertTrue("PATH_STOPPED" in diagnostic.message, diagnostic.message) + assertTrue(diagnostic.path.contains("UsvmPropertySearchFixture.ts:$sourceLine:"), diagnostic.path) + assertEquals(result.diagnostics, restored.diagnostics) + } + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( manifest = manifest, mapping = mapper.map(manifest), diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt index 1711e96f47..ac94899d55 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmRuntimeLimitationObserverTest.kt @@ -11,10 +11,71 @@ import org.jacodb.ets.model.EtsUndefinedType import org.junit.jupiter.api.Test import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallDecision +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallFailureReason import kotlin.test.assertEquals import kotlin.test.assertTrue class UsvmRuntimeLimitationObserverTest { + @Test + fun `unknown call fallbacks retain their decisions without treating applied models as limitations`() { + val observer = UsvmRuntimeLimitationObserver() + val statement = event(detail = "unused", withOrigin = true).statement + val stopped = TsUnknownCallEvent( + callSite = statement, + callee = statement.location.method.signature.copy(name = "missing"), + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.STOP_PATH), + ) + val fresh = stopped.copy( + callSite = event(detail = "unused", withOrigin = false).statement, + decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + ) + + observer.onUnknownCall(stopped.copy(decision = TsUnknownCallDecision.ModelApplied(modelId = "modeled"))) + assertTrue(observer.diagnostics.isEmpty()) + repeat(times = 100) { observer.onUnknownCall(stopped) } + observer.onUnknownCall(fresh) + + val diagnostics = observer.diagnostics + assertEquals(2, diagnostics.size) + assertEquals("usvm.unknown-call.path-stopped", diagnostics[0].code) + assertEquals("original.ts:3:5-3:12", diagnostics[0].path) + assertTrue("Example::missing" in diagnostics[0].message) + assertTrue("reason=METHOD_BODY_UNAVAILABLE" in diagnostics[0].message) + assertEquals("usvm.unknown-call.fresh-symbolic-return", diagnostics[1].code) + assertEquals("generated.ts#example[0]", diagnostics[1].path) + assertTrue("FRESH_SYMBOLIC_RETURN" in diagnostics[1].message) + } + + @Test + fun `unknown calls share the existing distinct diagnostic bound with runtime limits`() { + val observer = UsvmRuntimeLimitationObserver() + val first = event(detail = "first", withOrigin = false) + observer.onRuntimeFeatureLimitation(first) + val retained = observer.diagnostics.single() + val callee = first.statement.location.method.signature + + repeat(times = 100) { index -> + observer.onUnknownCall( + TsUnknownCallEvent( + callSite = first.statement, + callee = callee.copy(name = "missing$index"), + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.STOP_PATH), + ), + ) + } + + val diagnostics = observer.diagnostics + assertEquals(65, diagnostics.size) + assertEquals(retained, diagnostics.first()) + assertEquals("usvm.runtime.diagnostics-truncated", diagnostics.last().code) + assertEquals(diagnostics.size, diagnostics.distinct().size) + } + @Test fun `deduplicates identical events and retains the original statement location`() { val observer = UsvmRuntimeLimitationObserver() diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts index f196473103..2202fc02d9 100644 --- a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -148,3 +148,17 @@ export function optionalNumberArrayMutationProperty(values: (number | undefined) values[0] = undefined; return old !== 2; } + +export function unsupportedSliceProperty(value: number): boolean { + const values = [value]; + return values.slice().length === 1; +} + +export function unsupportedTypedArrayProperty(value: number): boolean { + const values = new Float64Array(1); + return values[0] === value; +} + +export function modeledAbsoluteProperty(value: number): boolean { + return Math.abs(value) >= 0; +}