diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index b90fda829..df1ad1961 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -6,12 +6,18 @@ import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsThrowStmt import org.usvm.UBoolExpr +import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.expr.TsSimpleValueResolver import org.usvm.machine.interpreter.TsStepScope import org.usvm.statistics.UInterpreterObserver @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { + /** Called after the profile dispatcher selects an outcome for an unknown call. */ + fun onUnknownCall(event: TsUnknownCallEvent) { + // default empty implementation + } + fun onAssignStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 9f622f2e6..3d6b394f3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -52,10 +52,17 @@ class TsMachine( private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( - tsOptions.unknownCallProfile, - unknownCallModelProvider, + profile = tsOptions.unknownCallProfile, + modelProvider = unknownCallModelProvider, + observer = observer, + ) + private val interpreter = TsInterpreter( + ctx = ctx, + graph = graph, + options = tsOptions, + observer = observer, + unknownCallDispatcher = resolvedUnknownCallDispatcher, ) - private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer, resolvedUnknownCallDispatcher) private val cfgStatistics = CfgStatisticsImpl(graph) fun analyze( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt new file mode 100644 index 000000000..7adf43527 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt @@ -0,0 +1,45 @@ +package org.usvm.machine.call + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsStmt +import org.usvm.machine.TsInterpreterObserver + +private val logger = KotlinLogging.logger {} + +/** Explains why a call reached the residual fallback instead of a semantic model. */ +enum class TsUnknownCallResidualReason { + MODEL_LOOKUP_DISABLED, + MODEL_NOT_APPLICABLE, +} + +/** Describes the model or fallback action selected for one unknown call. */ +sealed interface TsUnknownCallDecision { + data class ModelApplied( + val modelId: String, + ) : TsUnknownCallDecision { + init { + require(modelId.isNotBlank()) { "Applied model ID must not be blank" } + } + } + + data class ResidualFallback( + val policy: TsResidualCallPolicy, + val reason: TsUnknownCallResidualReason, + ) : TsUnknownCallDecision +} + +/** A structured decision reported for one unknown call. */ +data class TsUnknownCallEvent( + val callSite: EtsStmt, + val callee: EtsMethodSignature, + val failureReason: TsUnknownCallFailureReason, + val profile: TsUnknownCallProfile, + val outcome: TsUnknownCallOutcome, + val decision: TsUnknownCallDecision, +) + +internal fun TsInterpreterObserver.onUnknownCallSafely(event: TsUnknownCallEvent) { + runCatching { onUnknownCall(event) } + .onFailure { error -> logger.warn(error) { "Unknown-call observer failed while recording an event" } } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index de5f22941..66e4eeb1f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -2,6 +2,7 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsClassSignature import org.usvm.api.mockMethodCall +import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.newStmt @@ -61,15 +62,24 @@ object TsUnknownCallProfiles { } /** The result of asking a model provider to handle one unknown call. */ -enum class TsUnknownCallModelApplication { - APPLIED, - NOT_APPLICABLE, +sealed interface TsUnknownCallModelApplication { + /** Identifies the semantic model that produced the successor states. */ + data class Applied( + val modelId: String, + ) : TsUnknownCallModelApplication { + init { + require(modelId.isNotBlank()) { "Applied model ID must not be blank" } + } + } + + /** Indicates that the provider has no semantic model for this call. */ + data object NotApplicable : TsUnknownCallModelApplication } /** * Applies semantic models without exposing their lookup or registry implementation to the dispatcher. * - * A provider returning [TsUnknownCallModelApplication.APPLIED] must update the supplied scope with the model's + * A provider returning [TsUnknownCallModelApplication.Applied] must update the supplied scope with the model's * successor states. The deterministic registry and concrete model implementations are introduced separately. */ fun interface TsUnknownCallModelProvider { @@ -79,33 +89,79 @@ fun interface TsUnknownCallModelProvider { /** Empty provider used until an explicit model registry is configured. */ object TsNoUnknownCallModels : TsUnknownCallModelProvider { override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication = - TsUnknownCallModelApplication.NOT_APPLICABLE + TsUnknownCallModelApplication.NotApplicable } /** Applies the selected model/fallback profile to every residual call. */ class TsProfileUnknownCallDispatcher( private val profile: TsUnknownCallProfile, private val modelProvider: TsUnknownCallModelProvider, + private val observer: TsInterpreterObserver? = null, ) : TsUnknownCallDispatcher { override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - if (profile.modelLookup == TsUnknownCallModelLookup.ENABLED && - modelProvider.apply(scope, call) == TsUnknownCallModelApplication.APPLIED - ) { - return TsUnknownCallOutcome.MODEL_APPLIED + val residualReason = when (profile.modelLookup) { + TsUnknownCallModelLookup.DISABLED -> { + TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED + } + + TsUnknownCallModelLookup.ENABLED -> { + when (val application = modelProvider.apply(scope, call)) { + is TsUnknownCallModelApplication.Applied -> { + val event = event( + call = call, + outcome = TsUnknownCallOutcome.MODEL_APPLIED, + decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId), + ) + observer?.onUnknownCallSafely(event) + return TsUnknownCallOutcome.MODEL_APPLIED + } + + TsUnknownCallModelApplication.NotApplicable -> { + TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE + } + } + } } - return when (profile.residualPolicyFor(call)) { + val residualPolicy = profile.residualPolicyFor(call) + val outcome = when (residualPolicy) { + TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + } + val event = event( + call = call, + outcome = outcome, + decision = TsUnknownCallDecision.ResidualFallback( + policy = residualPolicy, + reason = residualReason, + ), + ) + when (residualPolicy) { TsResidualCallPolicy.STOP_PATH -> { val falseExpr = scope.calcOnState { ctx.falseExpr } scope.assert(falseExpr) - TsUnknownCallOutcome.PATH_STOPPED } TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { mockMethodCall(scope, call.callee, call.resultType) scope.doWithState { newStmt(call.callSite) } - TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN } } + + observer?.onUnknownCallSafely(event) + return outcome } + + private fun event( + call: TsUnknownCall, + outcome: TsUnknownCallOutcome, + decision: TsUnknownCallDecision, + ) = TsUnknownCallEvent( + callSite = call.callSite, + callee = call.callee, + failureReason = call.failureReason, + profile = profile.copy(residualOverrides = profile.residualOverrides.toMap()), + outcome = outcome, + decision = decision, + ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index a6c3b33bb..5233e5280 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -1,5 +1,6 @@ package org.usvm.machine.call +import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod @@ -15,18 +16,22 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Test import org.usvm.PathSelectionStrategy import org.usvm.SolverType +import org.usvm.StateCollectionStrategy import org.usvm.UConcreteHeapRef import org.usvm.UMachineOptions import org.usvm.api.mockMethodCall import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.machine.state.newStmt import org.usvm.util.getResourcePath import kotlin.test.assertEquals +import kotlin.test.assertFailsWith import kotlin.test.assertFalse import kotlin.test.assertIs import kotlin.test.assertNotNull @@ -41,6 +46,111 @@ class TsUnknownCallDispatcherTest { ) private val fullScene = EtsScene(listOf(sourceFile)) + @Test + fun `every profile decision is reported through the interpreter observer`() { + val cases = listOf( + ObservationCase( + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = TsNoUnknownCallModels, + outcome = TsUnknownCallOutcome.PATH_STOPPED, + decision = TsUnknownCallDecision.ResidualFallback( + policy = TsResidualCallPolicy.STOP_PATH, + reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, + ), + finalStateCount = 0, + ), + ObservationCase( + profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + modelProvider = TsNoUnknownCallModels, + outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, + decision = TsUnknownCallDecision.ResidualFallback( + policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, + ), + finalStateCount = 1, + ), + ObservationCase( + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + modelProvider = ApplyingModelProvider, + outcome = TsUnknownCallOutcome.MODEL_APPLIED, + decision = TsUnknownCallDecision.ModelApplied(modelId = "applying-model"), + finalStateCount = 1, + ), + ) + + cases.forEach { case -> + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "declaredMethodWithoutBodyContinues", + profile = case.profile, + modelProvider = case.modelProvider, + observer = observer, + ) + + assertEquals(case.finalStateCount, states.size, case.profile.toString()) + val event = observer.events.single() + assertEquals("declaredMethodWithoutBodyContinues", event.callSite.location.method.name) + assertEquals("external", event.callee.name) + assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, event.failureReason) + assertEquals(case.profile, event.profile) + assertEquals(case.outcome, event.outcome) + assertEquals(case.decision, event.decision) + } + } + + @Test + fun `model decision is reported once when the model forks`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = ForkingModelProvider, + observer = observer, + ) + + assertEquals(2, states.size) + val event = observer.events.single() + assertEquals(TsUnknownCallOutcome.MODEL_APPLIED, event.outcome) + } + + @Test + fun `throwing observer cannot change fresh or modeled exploration`() { + val cases = listOf( + ObservationFailureCase( + profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + modelProvider = TsNoUnknownCallModels, + expectedFinalStateCount = 1, + ), + ObservationFailureCase( + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = ForkingModelProvider, + expectedFinalStateCount = 2, + methodName = "modeledUnknownCallForks", + ), + ) + + cases.forEach { case -> + val states = analyzeAllStates( + methodName = case.methodName, + profile = case.profile, + modelProvider = case.modelProvider, + observer = ThrowingUnknownCallObserver, + ) + + assertEquals(case.expectedFinalStateCount, states.size, case.profile.toString()) + } + } + + @Test + fun `applied model decisions require non blank identifiers`() { + assertFailsWith { + TsUnknownCallModelApplication.Applied(modelId = " ") + } + assertFailsWith { + TsUnknownCallDecision.ModelApplied(modelId = "") + } + } + @Test fun `profiles select model lookup independently from residual fallback`() { val cases = listOf( @@ -396,6 +506,24 @@ class TsUnknownCallDispatcherTest { return EtsScene(listOf(filteredFile)) } + private fun analyzeAllStates( + methodName: String, + profile: TsUnknownCallProfile, + modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + observer: TsInterpreterObserver? = null, + ): List { + val method = method(fullScene, methodName) + return TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(unknownCallProfile = profile), + observer = observer, + unknownCallModelProvider = modelProvider, + ).use { machine -> + machine.analyze(listOf(method)) + } + } + private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher { val calls = mutableListOf() val receiverIsAssociatedFunction = mutableListOf() @@ -452,7 +580,38 @@ class TsUnknownCallDispatcherTest { override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { mockMethodCall(scope, call.callee, call.resultType) scope.doWithState { newStmt(call.callSite) } - return TsUnknownCallModelApplication.APPLIED + return TsUnknownCallModelApplication.Applied(modelId = "applying-model") + } + } + + private object ForkingModelProvider : TsUnknownCallModelProvider { + override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { + val result = requireNotNull(call.arguments.single().resolved) + val condition = scope.calcOnState { result.asExpr(ctx.boolSort) } + val completeCall: TsState.() -> Unit = { + methodResult = TsMethodResult.Success.MockedCall(result, call.callee) + newStmt(call.callSite) + } + scope.fork( + condition = condition, + blockOnTrueState = completeCall, + blockOnFalseState = completeCall, + ) + return TsUnknownCallModelApplication.Applied(modelId = "forking-model") + } + } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private object ThrowingUnknownCallObserver : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + error("observer failure") } } @@ -467,6 +626,21 @@ class TsUnknownCallDispatcherTest { val outcome: TsUnknownCallOutcome, ) + private data class ObservationCase( + val profile: TsUnknownCallProfile, + val modelProvider: TsUnknownCallModelProvider, + val outcome: TsUnknownCallOutcome, + val decision: TsUnknownCallDecision, + val finalStateCount: Int, + ) + + private data class ObservationFailureCase( + val profile: TsUnknownCallProfile, + val modelProvider: TsUnknownCallModelProvider, + val expectedFinalStateCount: Int, + val methodName: String = "declaredMethodWithoutBodyContinues", + ) + private data class Case( val methodName: String, val reasons: List, @@ -494,5 +668,12 @@ class TsUnknownCallDispatcherTest { solverTimeout = Duration.INFINITE, typeOperationsTimeout = Duration.INFINITE, ) + + val allStatesMachineOptions = machineOptions.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + stopOnTargetsReached = false, + ) } } diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index 73735195a..c78d4027f 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -14,6 +14,10 @@ declare class ExternalOverloads { static convert(value: string): string; } +declare class ExternalBoolean { + static convert(value: boolean): boolean; +} + class KnownReceiver { known(): number { return 1; @@ -60,6 +64,10 @@ class CallFallbackBaseline { return 101; } + modeledUnknownCallForks(value: boolean): boolean { + return ExternalBoolean.convert(value); + } + anyReceiverWithKnownMethodContinues(receiver: any): number { receiver.known(); return 102;