diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 749ca6a40d..af72368375 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -1,6 +1,7 @@ package org.usvm.api import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort import org.usvm.UExpr @@ -12,13 +13,14 @@ import org.usvm.machine.types.mkFakeValue fun mockMethodCall( scope: TsStepScope, method: EtsMethodSignature, + resultType: EtsType = method.returnType, ) { scope.doWithState { val result: UExpr<*> - if (method.returnType is EtsVoidType) { + if (resultType is EtsVoidType) { result = ctx.mkUndefinedValue() } else { - val sort = ctx.typeToSort(method.returnType) + val sort = ctx.typeToSort(resultType) result = when (sort) { is UAddressSort -> makeSymbolicRefUntyped() 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 ad115efdaf..9f622f2e62 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -9,8 +9,10 @@ import org.usvm.StateCollectionStrategy import org.usvm.UMachine import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget -import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher +import org.usvm.machine.call.TsNoUnknownCallModels +import org.usvm.machine.call.TsProfileUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallModelProvider import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -42,13 +44,18 @@ class TsMachine( private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, - unknownCallDispatcher: TsUnknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, + unknownCallDispatcher: TsUnknownCallDispatcher? = null, + unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, ) : UMachine() { private val graph = TsGraph(scene) private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) - private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer, unknownCallDispatcher) + private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( + tsOptions.unknownCallProfile, + unknownCallModelProvider, + ) + 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/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 6776638408..09c3e66594 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,7 +1,11 @@ package org.usvm.machine +import org.usvm.machine.call.TsUnknownCallProfile +import org.usvm.machine.call.TsUnknownCallProfiles + data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, + val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index e8369f039a..bb99b6ec90 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt @@ -64,12 +64,12 @@ enum class TsUnknownCallFailureReason { /** Handles TypeScript calls that could not be executed by the regular call pipeline. */ fun interface TsUnknownCallDispatcher { - fun dispatch(scope: TsStepScope, call: TsUnknownCall) + fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome } /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { - override fun dispatch(scope: TsStepScope, call: TsUnknownCall) { + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { val isUnresolvedConstructor = call.failureReason == TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND && call.callee.name == CONSTRUCTOR_NAME @@ -81,7 +81,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { methodResult = TsMethodResult.Success.MockedCall(receiver, call.callee) newStmt(call.callSite) } - return + return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN } when (call.failureReason) { @@ -94,6 +94,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { -> { mockMethodCall(scope, call.callee) scope.doWithState { newStmt(call.callSite) } + return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN } TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, @@ -106,6 +107,7 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { -> { val falseExpr = scope.calcOnState { ctx.falseExpr } scope.assert(falseExpr) + return TsUnknownCallOutcome.PATH_STOPPED } } } @@ -119,7 +121,7 @@ internal fun TsUnknownCallDispatcher.dispatch( callee: EtsMethodSignature = call.callee, resolvedReceiver: UExpr<*>? = null, resolvedArguments: List?> = List(call.args.size) { null }, -) { +): TsUnknownCallOutcome { require(resolvedArguments.size == call.args.size) { "Expected ${call.args.size} resolved argument slots, got ${resolvedArguments.size}" } @@ -129,7 +131,7 @@ internal fun TsUnknownCallDispatcher.dispatch( is EtsPtrCallExpr -> call.ptr else -> null } - dispatch( + return dispatch( scope, TsUnknownCall( callee = callee, 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 new file mode 100644 index 0000000000..de5f229419 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -0,0 +1,111 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsClassSignature +import org.usvm.api.mockMethodCall +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.newStmt + +/** The externally observable decision made for a call that could not be executed normally. */ +enum class TsUnknownCallOutcome { + MODEL_APPLIED, + FRESH_SYMBOLIC_RETURN, + PATH_STOPPED, +} + +/** Controls whether the dispatcher asks the configured model provider to handle a call. */ +enum class TsUnknownCallModelLookup { + DISABLED, + ENABLED, +} + +/** + * Selects what happens when model lookup is disabled or no model applies. + * + * [FRESH_SYMBOLIC_RETURN] creates a new symbolic value of the call expression's result type and advances past the + * call. It deliberately ignores all callee side effects and exceptions, so it is an opaque continuation rather than + * a semantic model of the callee. + */ +enum class TsResidualCallPolicy { + STOP_PATH, + FRESH_SYMBOLIC_RETURN, +} + +/** Independently configures model lookup and the fallback for residual calls. */ +data class TsUnknownCallProfile( + val modelLookup: TsUnknownCallModelLookup, + val residualPolicy: TsResidualCallPolicy, + val residualOverrides: Map = emptyMap(), +) { + internal fun residualPolicyFor(call: TsUnknownCall): TsResidualCallPolicy = + residualOverrides[call.callee.enclosingClass] ?: residualPolicy +} + +/** Ready-to-use profiles for the four supported model/fallback combinations. */ +object TsUnknownCallProfiles { + val STOP_ALL = TsUnknownCallProfile( + modelLookup = TsUnknownCallModelLookup.DISABLED, + residualPolicy = TsResidualCallPolicy.STOP_PATH, + ) + val FRESH_SYMBOLIC_FOR_ALL = TsUnknownCallProfile( + modelLookup = TsUnknownCallModelLookup.DISABLED, + residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + val MODELS_THEN_STOP = TsUnknownCallProfile( + modelLookup = TsUnknownCallModelLookup.ENABLED, + residualPolicy = TsResidualCallPolicy.STOP_PATH, + ) + val MODELS_THEN_FRESH_SYMBOLIC = TsUnknownCallProfile( + modelLookup = TsUnknownCallModelLookup.ENABLED, + residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) +} + +/** The result of asking a model provider to handle one unknown call. */ +enum class TsUnknownCallModelApplication { + APPLIED, + NOT_APPLICABLE, +} + +/** + * 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 + * successor states. The deterministic registry and concrete model implementations are introduced separately. + */ +fun interface TsUnknownCallModelProvider { + fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication +} + +/** Empty provider used until an explicit model registry is configured. */ +object TsNoUnknownCallModels : TsUnknownCallModelProvider { + override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication = + TsUnknownCallModelApplication.NOT_APPLICABLE +} + +/** Applies the selected model/fallback profile to every residual call. */ +class TsProfileUnknownCallDispatcher( + private val profile: TsUnknownCallProfile, + private val modelProvider: TsUnknownCallModelProvider, +) : TsUnknownCallDispatcher { + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + if (profile.modelLookup == TsUnknownCallModelLookup.ENABLED && + modelProvider.apply(scope, call) == TsUnknownCallModelApplication.APPLIED + ) { + return TsUnknownCallOutcome.MODEL_APPLIED + } + + return when (profile.residualPolicyFor(call)) { + 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 + } + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt b/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt index 67dedf94f3..d81ef71629 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt @@ -20,6 +20,7 @@ import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher import org.usvm.util.getResourcePath import kotlin.test.assertFalse import kotlin.test.assertIs @@ -178,6 +179,7 @@ class CallFallbackBaselineTest { options = machineOptions, tsOptions = tsOptions, machineObserver = ReachabilityObserver(), + unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, ).use { machine -> machine.analyze(listOf(method), listOf(initialTarget)) .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } diff --git a/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt b/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt index ee1efcbf05..b874547060 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt @@ -12,6 +12,7 @@ import org.usvm.UMachineOptions import org.usvm.api.checkers.UnreachableCodeDetector import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher import org.usvm.util.getResourcePath @TestInstance(PER_CLASS) @@ -48,7 +49,14 @@ class UnreachableCodeDetectorTest { fun testUnreachableCodeWithMockedCallsInside() { val observer = UnreachableCodeDetector() val tsOptions = TsOptions(interproceduralAnalysis = false) - val machine = TsMachine(scene, options, tsOptions, observer, observer) + val machine = TsMachine( + scene, + options, + tsOptions, + observer, + observer, + TsCompatibilityUnknownCallDispatcher, + ) val methods = scene.projectClasses .flatMap { it.methods } .filter { it.name == "unreachableCodeWithCallsInside" } 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 fb71f6263e..a6c3b33bb0 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 @@ -17,11 +17,14 @@ import org.usvm.PathSelectionStrategy import org.usvm.SolverType 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.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.newStmt import org.usvm.util.getResourcePath import kotlin.test.assertEquals import kotlin.test.assertFalse @@ -38,6 +41,112 @@ class TsUnknownCallDispatcherTest { ) private val fullScene = EtsScene(listOf(sourceFile)) + @Test + fun `profiles select model lookup independently from residual fallback`() { + val cases = listOf( + ProfileCase( + profile = TsUnknownCallProfiles.STOP_ALL, + withoutModel = ProfileResult( + reachesReturn = false, + outcome = TsUnknownCallOutcome.PATH_STOPPED, + ), + withModel = ProfileResult( + reachesReturn = false, + outcome = TsUnknownCallOutcome.PATH_STOPPED, + ), + ), + ProfileCase( + profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + withoutModel = ProfileResult( + reachesReturn = true, + outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, + ), + withModel = ProfileResult( + reachesReturn = true, + outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, + ), + ), + ProfileCase( + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + withoutModel = ProfileResult( + reachesReturn = false, + outcome = TsUnknownCallOutcome.PATH_STOPPED, + ), + withModel = ProfileResult( + reachesReturn = true, + outcome = TsUnknownCallOutcome.MODEL_APPLIED, + ), + ), + ProfileCase( + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + withoutModel = ProfileResult( + reachesReturn = true, + outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, + ), + withModel = ProfileResult( + reachesReturn = true, + outcome = TsUnknownCallOutcome.MODEL_APPLIED, + ), + ), + ) + + cases.forEach { case -> + assertEquals(case.withoutModel, runProfile(case.profile, TsNoUnknownCallModels), case.profile.toString()) + assertEquals(case.withModel, runProfile(case.profile, ApplyingModelProvider), case.profile.toString()) + } + } + + @Test + fun `TsOptions profile configures the machine dispatcher`() { + assertEquals(TsUnknownCallProfiles.MODELS_THEN_STOP, TsOptions().unknownCallProfile) + assertTrue(TsOptions().unknownCallProfile.residualOverrides.isEmpty()) + + assertFalse(reachesReturn("declaredMethodWithoutBodyContinues")) + assertTrue( + reachesReturn( + "declaredMethodWithoutBodyContinues", + tsOptions = TsOptions(unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL), + ) + ) + } + + @Test + fun `explicit family override replaces the profile residual fallback`() { + val family = method(fullScene, "declaredMethodWithoutBodyContinues") + .cfg + .stmts + .mapNotNull { it.callExpr } + .single { it.callee.name == "external" } + .callee + .enclosingClass + val profile = TsUnknownCallProfiles.STOP_ALL.copy( + residualOverrides = mapOf( + family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + ) + + assertTrue( + reachesReturn( + "declaredMethodWithoutBodyContinues", + tsOptions = TsOptions(unknownCallProfile = profile), + ) + ) + } + + @Test + fun `fresh symbolic return uses the source call result type`() { + val dispatcher = RecordingResultSortDispatcher( + TsProfileUnknownCallDispatcher( + TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + TsNoUnknownCallModels, + ) + ) + + assertTrue(reachesReturn("overloadedDeclaredMethodWithoutBodyContinues", dispatcher = dispatcher)) + assertTrue(dispatcher.resultSortMatches.isNotEmpty()) + assertTrue(dispatcher.resultSortMatches.all { it }) + } + @Test fun `inventoried unknown calls use normalized compatibility dispatch`() { val cases = listOf( @@ -232,16 +341,18 @@ class TsUnknownCallDispatcherTest { methodName: String, scene: EtsScene = fullScene, tsOptions: TsOptions = TsOptions(), - dispatcher: TsUnknownCallDispatcher, + dispatcher: TsUnknownCallDispatcher? = null, + modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, className: String = "CallFallbackBaseline", ): Boolean = returnStatement(scene, methodName, className) in - reachedStatements(methodName, scene, tsOptions, dispatcher, className) + reachedStatements(methodName, scene, tsOptions, dispatcher, modelProvider, className) private fun reachedStatements( methodName: String, scene: EtsScene, tsOptions: TsOptions, - dispatcher: TsUnknownCallDispatcher, + dispatcher: TsUnknownCallDispatcher?, + modelProvider: TsUnknownCallModelProvider, className: String, ): Set { val method = method(scene, methodName, className) @@ -255,6 +366,7 @@ class TsUnknownCallDispatcherTest { tsOptions = tsOptions, machineObserver = ReachabilityObserver(), unknownCallDispatcher = dispatcher, + unknownCallModelProvider = modelProvider, ).use { machine -> machine.analyze(listOf(method), listOf(initialTarget)) .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } @@ -288,16 +400,73 @@ class TsUnknownCallDispatcherTest { val calls = mutableListOf() val receiverIsAssociatedFunction = mutableListOf() - override fun dispatch(scope: TsStepScope, call: TsUnknownCall) { + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { calls += call val receiver = call.receiver?.resolved as? UConcreteHeapRef receiverIsAssociatedFunction += receiver?.let { resolved -> scope.calcOnState { associatedFunction[resolved] != null } } - TsCompatibilityUnknownCallDispatcher.dispatch(scope, call) + return TsCompatibilityUnknownCallDispatcher.dispatch(scope, call) + } + } + + private fun runProfile( + profile: TsUnknownCallProfile, + modelProvider: TsUnknownCallModelProvider, + ): ProfileResult { + val dispatcher = RecordingOutcomeDispatcher(TsProfileUnknownCallDispatcher(profile, modelProvider)) + val reachesReturn = reachesReturn( + "declaredMethodWithoutBodyContinues", + dispatcher = dispatcher, + ) + return ProfileResult(reachesReturn, dispatcher.outcomes.single()) + } + + private class RecordingOutcomeDispatcher( + private val delegate: TsUnknownCallDispatcher, + ) : TsUnknownCallDispatcher { + val outcomes = mutableListOf() + + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome = + delegate.dispatch(scope, call).also(outcomes::add) + } + + private class RecordingResultSortDispatcher( + private val delegate: TsUnknownCallDispatcher, + ) : TsUnknownCallDispatcher { + val resultSortMatches = mutableListOf() + + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + val outcome = delegate.dispatch(scope, call) + if (outcome == TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN) { + resultSortMatches += scope.calcOnState { + val result = methodResult as TsMethodResult.Success.MockedCall + result.value.sort == ctx.typeToSort(call.resultType) + } + } + return outcome } } + private object ApplyingModelProvider : TsUnknownCallModelProvider { + override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { + mockMethodCall(scope, call.callee, call.resultType) + scope.doWithState { newStmt(call.callSite) } + return TsUnknownCallModelApplication.APPLIED + } + } + + private data class ProfileCase( + val profile: TsUnknownCallProfile, + val withoutModel: ProfileResult, + val withModel: ProfileResult, + ) + + private data class ProfileResult( + val reachesReturn: Boolean, + val outcome: TsUnknownCallOutcome, + ) + private data class Case( val methodName: String, val reasons: List, diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 78aaaa09cf..6da4e92b79 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -27,6 +27,7 @@ import org.usvm.api.TsTest import org.usvm.api.TsTestValue import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsCompatibilityUnknownCallDispatcher import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults @@ -361,7 +362,12 @@ abstract class TsMethodTestRunner : TestRunner List = { method, options -> val tsMachineOptions = TsOptions() - TsMachine(scene, options, tsMachineOptions).use { machine -> + TsMachine( + scene, + options, + tsMachineOptions, + unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, + ).use { machine -> val states = machine.analyze(listOf(method)) val resolved = states.map { state -> val resolver = TsTestResolver()