diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index e65ae84670..9dc1181e72 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -39,6 +39,9 @@ interface TsUnknownCallModel { val additionalSceneFiles: List get() = emptyList() + /** Model-owned invariants may require stopping a prefix instead of inventing a helper result. */ + fun residualPolicy(state: TsState, call: TsUnknownCall): TsResidualCallPolicy? = null + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index f27af0a0fc..0bb7dd13dd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -35,7 +35,7 @@ class TsModelUnknownCallDispatcher( private val observer: TsInterpreterObserver? = null, ) : TsUnknownCallModelDispatcher { override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - val application = scope.calcOnState { + val (application, residualPolicy) = scope.calcOnState { val catalog = this@TsModelUnknownCallDispatcher.models val hasDirectTarget = catalog.select(call) != null // A direct target retains precedence even when its model rejects the call or is already active. @@ -45,22 +45,24 @@ class TsModelUnknownCallDispatcher( TsDateEtsIrModelFamily.canonicalModelCall(this, call) ?: call } - catalog.apply(this, modelCall) + val residualPolicy = catalog.select(modelCall)?.residualPolicy(this, modelCall) ?: fallback + catalog.apply(this, modelCall) to residualPolicy } return when (application) { - is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) - TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call) + is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application, residualPolicy) + TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call, residualPolicy) } } private fun applyFallback( scope: TsStepScope, call: TsUnknownCall, + residualPolicy: TsResidualCallPolicy, ): TsUnknownCallOutcome { - val decision = TsUnknownCallDecision.ResidualFallback(fallback) + val decision = TsUnknownCallDecision.ResidualFallback(residualPolicy) - when (fallback) { + when (residualPolicy) { TsResidualCallPolicy.STOP_PATH -> { val stoppedState = scope.calcOnState { this } val falseExpr = stoppedState.ctx.falseExpr @@ -78,7 +80,7 @@ class TsModelUnknownCallDispatcher( } } - reportFallback(call) + reportFallback(call, residualPolicy) return decision.outcome } @@ -86,18 +88,19 @@ class TsModelUnknownCallDispatcher( scope: TsStepScope, call: TsUnknownCall, application: TsUnknownCallModelApplication.Applied, + residualPolicy: TsResidualCallPolicy, ): TsUnknownCallOutcome { val residualGuard = application.execution.residualGuard // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone // inherits both the constraints and their solver models. val freshResidualResult = if ( - residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { makeFreshUnknownCallResult(scope, call.resultType) } else { null } - val stoppedResidualState = if (residualGuard != null && fallback == TsResidualCallPolicy.STOP_PATH) { + val stoppedResidualState = if (residualGuard != null && residualPolicy == TsResidualCallPolicy.STOP_PATH) { scope.checkSat(residualGuard) } else { null @@ -126,7 +129,7 @@ class TsModelUnknownCallDispatcher( ) }.toMutableList() - if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { guardedStateChanges += residualGuard to { setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) newStmt(call.callSite) @@ -150,7 +153,7 @@ class TsModelUnknownCallDispatcher( observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(application.modelId))) } if (freshResidualApplied || stoppedResidualIsSatisfiable) { - reportFallback(call) + reportFallback(call, residualPolicy) } return when { @@ -164,14 +167,14 @@ class TsModelUnknownCallDispatcher( private fun stoppedPathReason(call: TsUnknownCall): String = "Unknown call ${call.callee} at ${call.callSite.location}: reason=${call.failureReason}" - private fun reportFallback(call: TsUnknownCall) { - if (fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + private fun reportFallback(call: TsUnknownCall, residualPolicy: TsResidualCallPolicy) { + if (residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { logger.debug { "Unknown call ${call.callee} at ${call.callSite.location}: " + - "fallback=$fallback, reason=${call.failureReason}" + "fallback=$residualPolicy, reason=${call.failureReason}" } } - observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ResidualFallback(fallback))) + observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ResidualFallback(residualPolicy))) } private fun modelStateChange( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 75d3f52035..7f92822687 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -16,6 +16,7 @@ import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel @@ -388,6 +389,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName = "requireDense", arity = 1, implementation = TsDenseArrayPrimitives::requireDense, + unsupportedCallPolicy = TsResidualCallPolicy.STOP_PATH, ), primitiveModel( methodName = "prepareOwnSlots", @@ -476,6 +478,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName: String, arity: Int, implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + unsupportedCallPolicy: TsResidualCallPolicy? = null, ): TsUnknownCallModel = TsPrimitiveUnknownCallModel( idPrefix = "ts.array.primitive", methodName = methodName, @@ -485,6 +488,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass }, owningModelIds = { sourceModelIds }, implementation = implementation, + unsupportedCallPolicy = unsupportedCallPolicy, ) private fun growArray( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt index b4b51067d7..1e0776d54d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt @@ -2,6 +2,7 @@ package org.usvm.machine.call.intrinsic import org.jacodb.ets.model.EtsClassSignature import org.usvm.UExpr +import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel @@ -19,6 +20,7 @@ internal class TsPrimitiveUnknownCallModel( private val sourceClassSignature: () -> EtsClassSignature, private val owningModelIds: () -> Set, private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + private val unsupportedCallPolicy: TsResidualCallPolicy? = null, ) : TsUnknownCallModel { override val id: String = "$idPrefix.$methodName" override val target = TsUnknownCallTarget( @@ -28,11 +30,7 @@ internal class TsPrimitiveUnknownCallModel( ) override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { - val helperOwnerMatches = call.callee.enclosingClass == helperClassSignature() - val callerSignature = call.callSite.location.method.signature - val sourceCallerMatches = callerSignature.enclosingClass == sourceClassSignature() - val sourceModelIsActive = owningModelIds().any(state::isUnknownCallModelActive) - if (!helperOwnerMatches || !sourceCallerMatches || !sourceModelIsActive) return null + if (!ownsHelperCall(state, call)) return null if (call.receiver != null || call.arguments.size != arity) { return null @@ -41,4 +39,15 @@ internal class TsPrimitiveUnknownCallModel( val inputs = call.arguments.map { argument -> argument.resolved ?: return null } return implementation(state, inputs) } + + override fun residualPolicy(state: TsState, call: TsUnknownCall): TsResidualCallPolicy? = + unsupportedCallPolicy.takeIf { ownsHelperCall(state, call) } + + private fun ownsHelperCall(state: TsState, call: TsUnknownCall): Boolean { + val helperOwnerMatches = call.callee.enclosingClass == helperClassSignature() + val callerSignature = call.callSite.location.method.signature + val sourceCallerMatches = callerSignature.enclosingClass == sourceClassSignature() + val sourceModelIsActive = owningModelIds().any(state::isUnknownCallModelActive) + return helperOwnerMatches && sourceCallerMatches && sourceModelIsActive + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt index f726b1e785..434d42d9cb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt @@ -1,7 +1,13 @@ package org.usvm.machine.call +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Test @@ -17,11 +23,16 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.expr.extractInt +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.memory.URegisterStackLValue import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath import org.usvm.util.jsString +import org.usvm.util.mkArrayLengthLValue import java.nio.file.Path import kotlin.io.path.readText import kotlin.test.assertEquals @@ -291,6 +302,46 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { assertTrue(limitations.any { it.reason == TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_DELETE }) } + @Test + fun `rejected reduce invariant retains callback mutation as a stopped prefix in fresh mode`() { + val events = mutableListOf() + val prefixLengths = mutableListOf() + var callbackReturns = 0 + val observer = object : TsInterpreterObserver { + override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + val isCallbackReturn = stmt is EtsReturnStmt && + stmt.location.method.name.startsWith(ANONYMOUS_METHOD_PREFIX) + if (isCallbackReturn) callbackReturns++ + } + + override fun onPathStopped(state: TsState, reason: String) { + val receiver = state.memory.read(URegisterStackLValue(state.ctx.addressSort, idx = 1)) + .asExpr(state.ctx.addressSort) + val arrayType = EtsArrayType(EtsStringType, dimensions = 1) + val length = state.memory.read(mkArrayLengthLValue(receiver, arrayType)) + prefixLengths += state.models.first().eval(length).extractInt() + } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val analysis = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions.copy(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + observer = observer, + ).use { machine -> machine.analyzeWithMetadata(listOf(method("reduceShrink"))) } + + assertTrue(analysis.states.isEmpty()) + assertTrue(analysis.unsupportedCall) + assertEquals(listOf(0), prefixLengths) + assertEquals(expected = 1, actual = callbackReturns) + val invariantEvent = events.single { it.callee.name == "requireDense" } + assertEquals(TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH), invariantEvent.decision) + } + @Test fun `own slot deletion revokes dense reduction and slice models`() { discoverProperties( diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt index dd75e7400d..2419d8b3fe 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt @@ -12,6 +12,7 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath import kotlin.test.Test +import kotlin.test.assertEquals import kotlin.test.assertTrue import kotlin.time.Duration @@ -38,6 +39,27 @@ class TsPrimitiveOwnerBoundaryTest { assertForeignHelperResidual("foreignStringRange") } + @Test + fun `foreign invariant declaration retains the configured fresh fallback`() { + val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" } + .methods + .single { it.name == "foreignDense" } + val observer = RecordingObserver() + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + assertEquals(expected = 1, actual = states.size) + assertEquals( + expected = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + actual = observer.events.single().decision, + ) + } + private fun assertForeignHelperResidual(methodName: String) { val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" } .methods diff --git a/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts index 0a63e2cd47..63d51693bb 100644 --- a/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts +++ b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts @@ -6,6 +6,7 @@ declare class StringModelPrimitives { declare class ArrayModelPrimitives { static grow(values: number[], length: number): void; + static requireDense(values: number[]): void; } export class ForeignPrimitiveHelpers { @@ -26,4 +27,10 @@ export class ForeignPrimitiveHelpers { ArrayModelPrimitives.grow(values, 2); return values.length; } + + foreignDense(): number { + const values = [1]; + ArrayModelPrimitives.requireDense(values); + return values.length; + } }