From 8661927b36e1233523a991bd3f62126d0794e099 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 23 Aug 2026 01:21:17 +0300 Subject: [PATCH 1/3] [TS Calls] Centralize unknown-call dispatch --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 5 +- .../kotlin/org/usvm/machine/TsMethodCall.kt | 23 +- .../org/usvm/machine/call/TsUnknownCall.kt | 141 +++++++++ .../main/kotlin/org/usvm/machine/expr/Call.kt | 25 +- .../usvm/machine/expr/CallApproximations.kt | 6 +- .../org/usvm/machine/expr/CallStatic.kt | 14 +- .../org/usvm/machine/expr/TsExprResolver.kt | 27 +- .../usvm/machine/interpreter/TsInterpreter.kt | 130 +++++--- .../call/TsUnknownCallDispatcherTest.kt | 298 ++++++++++++++++++ .../baseline/CallFallbackBaseline.ts | 15 + 10 files changed, 630 insertions(+), 54 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt 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 cd7d487192..ad115efdaf 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -9,6 +9,8 @@ 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.TsUnknownCallDispatcher import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -40,12 +42,13 @@ class TsMachine( private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, + unknownCallDispatcher: TsUnknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, ) : 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) + private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer, unknownCallDispatcher) private val cfgStatistics = CfgStatisticsImpl(graph) fun analyze( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt index 49616f7db8..e8f2ec65aa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt @@ -1,12 +1,15 @@ package org.usvm.machine +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsInstanceCallExpr import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStmtLocation import org.usvm.UExpr sealed interface TsMethodCall : EtsStmt { + val call: EtsCallExpr + val resolvedReceiver: UExpr<*>? val instance: UExpr<*> val args: List> val returnSite: EtsStmt @@ -20,17 +23,27 @@ sealed interface TsMethodCall : EtsStmt { } class TsVirtualMethodCallStmt( - val callee: EtsMethodSignature, + override val call: EtsInstanceCallExpr, override val instance: UExpr<*>, override val args: List>, override val returnSite: EtsStmt, ) : TsMethodCall { + override val resolvedReceiver: UExpr<*> + get() = instance + override fun toString(): String { - return "virtual ${callee.enclosingClass.name}::${callee.name}" + return "virtual ${call.callee.enclosingClass.name}::${call.callee.name}" } fun toConcrete(callee: EtsMethod): TsConcreteMethodCallStmt { - return TsConcreteMethodCallStmt(callee, instance, args, returnSite) + return TsConcreteMethodCallStmt( + callee = callee, + call = call, + resolvedReceiver = resolvedReceiver, + instance = instance, + args = args, + returnSite = returnSite, + ) } } @@ -38,6 +51,8 @@ class TsVirtualMethodCallStmt( // and not wrapped in array (if calling a vararg method) class TsConcreteMethodCallStmt( val callee: EtsMethod, + override val call: EtsCallExpr, + override val resolvedReceiver: UExpr<*>?, override val instance: UExpr<*>, override val args: List>, override val returnSite: EtsStmt, 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 new file mode 100644 index 0000000000..bd4fb1611d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt @@ -0,0 +1,141 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UExpr +import org.usvm.api.mockMethodCall +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.newStmt + +/** + * A call that the regular TypeScript execution pipeline could not execute. + * + * Frontend call resolution and the existing built-in approximations run before this boundary. A call reaches the + * dispatcher only after one of those stages cannot continue normally. Successful compatibility approximations such + * as `toString`, `valueOf`, `Math.floor`, and `$r` therefore remain outside this boundary until they are classified + * and migrated as semantic models. Failures that happen while evaluating a callee or allocating its receiver also + * remain pre-call failures and are not dispatched. + */ +data class TsUnknownCall( + val callee: EtsMethodSignature, + val receiver: TsUnknownCallValue?, + val arguments: List, + val resultType: EtsType, + val callSite: EtsStmt, + val failureReason: TsUnknownCallFailureReason, +) + +/** + * Keeps the frontend value and the symbolic value, when the latter was available at the point of failure. + * + * Compatibility behavior deliberately does not resolve missing values eagerly: doing so could evaluate argument + * expressions that the old implementation never evaluated before stopping or mocking the call. + */ +data class TsUnknownCallValue( + val source: EtsValue, + val resolved: UExpr<*>?, +) + +enum class TsUnknownCallFailureReason { + STATIC_METHOD_NOT_FOUND, + NON_REFERENCE_RECEIVER, + RECEIVER_CLASS_NOT_FOUND, + UNSUPPORTED_RECEIVER_TYPE, + VIRTUAL_METHOD_NOT_FOUND, + RECEIVER_TYPE_STREAM_UNAVAILABLE, + ANY_RECEIVER, + NO_SUITABLE_VIRTUAL_TARGET, + POINTER_TARGET_NOT_FOUND, + NON_REFERENCE_POINTER, + METHOD_BODY_UNAVAILABLE, + INTERPROCEDURAL_ANALYSIS_DISABLED, + LOGGING_CALL, +} + +fun interface TsUnknownCallDispatcher { + fun dispatch(scope: TsStepScope, call: TsUnknownCall) +} + +/** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */ +object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { + override fun dispatch(scope: TsStepScope, call: TsUnknownCall) { + val isUnresolvedConstructor = call.failureReason == TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND && + call.callee.name == CONSTRUCTOR_NAME + + if (isUnresolvedConstructor) { + val receiver = requireNotNull(call.receiver?.resolved) { + "An unresolved constructor must have a resolved receiver" + } + scope.doWithState { + methodResult = TsMethodResult.Success.MockedCall(receiver, call.callee) + newStmt(call.callSite) + } + return + } + + when (call.failureReason) { + TsUnknownCallFailureReason.ANY_RECEIVER, + TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, + TsUnknownCallFailureReason.NON_REFERENCE_POINTER, + TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, + TsUnknownCallFailureReason.LOGGING_CALL, + -> { + mockMethodCall(scope, call.callee) + scope.doWithState { newStmt(call.callSite) } + } + + TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, + TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, + TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + TsUnknownCallFailureReason.UNSUPPORTED_RECEIVER_TYPE, + TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, + TsUnknownCallFailureReason.RECEIVER_TYPE_STREAM_UNAVAILABLE, + TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, + -> { + val falseExpr = scope.calcOnState { ctx.falseExpr } + scope.assert(falseExpr) + } + } + } +} + +internal fun TsUnknownCallDispatcher.dispatch( + scope: TsStepScope, + call: EtsCallExpr, + callSite: EtsStmt, + failureReason: TsUnknownCallFailureReason, + callee: EtsMethodSignature = call.callee, + resolvedReceiver: UExpr<*>? = null, + resolvedArguments: List?> = List(call.args.size) { null }, +) { + require(resolvedArguments.size == call.args.size) { + "Expected ${call.args.size} resolved argument slots, got ${resolvedArguments.size}" + } + + val receiverSource = when (call) { + is EtsInstanceCallExpr -> call.instance + is EtsPtrCallExpr -> call.ptr + else -> null + } + dispatch( + scope, + TsUnknownCall( + callee = callee, + receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) }, + arguments = call.args.zip(resolvedArguments) { source, resolved -> + TsUnknownCallValue(source, resolved) + }, + resultType = call.type, + callSite = callSite, + failureReason = failureReason, + ), + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt index 152faf7ad7..fa217414d2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt @@ -3,10 +3,12 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsInstanceCallExpr -import org.jacodb.ets.model.EtsMethodSignature import org.usvm.UExpr import org.usvm.machine.TsContext import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation @@ -48,13 +50,26 @@ internal fun TsExprResolver.handleInstanceCall( val fakeType = resolved.getFakeType(scope) scope.assert(fakeType.refTypeExpr) ?: run { logger.warn { "Calls on non-ref (fake) instance is not supported: $expr" } + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, + resolvedReceiver = resolved, + ) return null } resolved.extractRef(scope) } else { if (resolved.sort != addressSort) { logger.warn { "Calling method on non-ref instance is not yet supported: $expr" } - scope.assert(falseExpr) + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, + resolvedReceiver = resolved, + ) return null } resolved.asExpr(addressSort) @@ -68,18 +83,18 @@ internal fun TsExprResolver.handleInstanceCall( val args = expr.args.map { resolve(it) ?: return null } // Call. - callInstanceMethod(scope, expr.callee, instance, args) + callInstanceMethod(scope, expr, instance, args) } fun TsContext.callInstanceMethod( scope: TsStepScope, - callee: EtsMethodSignature, + call: EtsInstanceCallExpr, instance: UExpr<*>, args: List>, ): UExpr<*>? { // Create the virtual call statement. val virtualCall = TsVirtualMethodCallStmt( - callee = callee, + call = call, instance = instance, args = args, returnSite = scope.calcOnState { lastStmt }, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 4aecbb62eb..0060b4762d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -84,12 +84,12 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } - val instance = scope.calcOnState { resolve(expr.instance)?.asExpr(addressSort) } + val instance = resolve(expr.instance) ?: return TsExprApproximationResult.ResolveFailure - val instanceType = if (isAllocatedConcreteHeapRef(instance)) { + val instanceType = if (instance.sort == addressSort && isAllocatedConcreteHeapRef(instance)) { scope.calcOnState { - memory.typeStreamOf(instance).firstOrNull() ?: expr.instance.type + memory.typeStreamOf(instance.asExpr(addressSort)).firstOrNull() ?: expr.instance.type } } else { expr.instance.type diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt index 4f53b8bea8..89c75972b2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt @@ -9,6 +9,8 @@ import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.UExpr import org.usvm.machine.Constants import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation @@ -48,7 +50,13 @@ internal fun TsExprResolver.handleStaticCall( when (val resolved = resolveStaticMethod(expr.callee)) { is TsResolutionResult.Empty -> { logger.error { "Could not resolve static call: ${expr.callee}" } - scope.assert(falseExpr) ?: return null + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, + ) + return null } is TsResolutionResult.Ambiguous -> { @@ -107,6 +115,8 @@ private fun TsExprResolver.processAmbiguousStaticMethod( val concreteCalls = staticProperties.mapIndexed { index, value -> TsConcreteMethodCallStmt( callee = value, + call = expr, + resolvedReceiver = null, instance = staticInstances[index], args = args, returnSite = scope.calcOnState { lastStmt } @@ -129,6 +139,8 @@ private fun TsExprResolver.processUniqueStaticMethod( val args = expr.args.map { resolve(it) ?: return } val concreteCall = TsConcreteMethodCallStmt( callee = resolved.property, + call = expr, + resolvedReceiver = null, instance = instance, args = args, returnSite = scope.calcOnState { lastStmt }, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 58fa7eca6b..5e08d5f5ff 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -89,11 +89,13 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive -import org.usvm.api.mockMethodCall import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.dispatch import org.usvm.machine.TsContext import org.usvm.machine.TsOptions import org.usvm.machine.interpreter.PromiseState @@ -147,6 +149,7 @@ class TsExprResolver( internal val scope: TsStepScope, internal val options: TsOptions, internal val hierarchy: EtsHierarchy, + internal val unknownCallDispatcher: TsUnknownCallDispatcher, ) : EtsEntity.Visitor?> { val simpleValueResolver: TsSimpleValueResolver = @@ -952,8 +955,16 @@ class TsExprResolver( return mkUndefinedValue() } - val callee = scope.calcOnState { - associatedFunction[ptr] ?: error("No associated methods for ptr: $ptr") + val callee = scope.calcOnState { associatedFunction[ptr] } + if (callee == null) { + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, + resolvedReceiver = ptr, + ) + return null } val resolvedArgs = buildList { callee.closure?.let(::add) @@ -961,13 +972,21 @@ class TsExprResolver( } val concreteCall = TsConcreteMethodCallStmt( callee = callee.method, + call = expr, + resolvedReceiver = ptr, instance = callee.thisInstance ?: ctx.mkUndefinedValue(), args = resolvedArgs, returnSite = scope.calcOnState { lastStmt }, ) scope.doWithState { newStmt(concreteCall) } } else { - mockMethodCall(scope, expr.callee) + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.NON_REFERENCE_POINTER, + resolvedReceiver = ptr, + ) } null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index c17dbfc5d2..5df08a3394 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -28,7 +28,6 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType -import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.callExpr @@ -39,7 +38,6 @@ import org.usvm.UInterpreter import org.usvm.UIteExpr import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray -import org.usvm.api.mockMethodCall import org.usvm.api.targets.TsTarget import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership @@ -51,6 +49,9 @@ import org.usvm.machine.TsGraph import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsOptions import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.TsUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprResolver import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.handleAssignToArrayIndex @@ -93,6 +94,7 @@ class TsInterpreter( private val graph: TsGraph, private val options: TsOptions, private val observer: TsInterpreterObserver? = null, + private val unknownCallDispatcher: TsUnknownCallDispatcher, ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() @@ -154,9 +156,8 @@ class TsInterpreter( private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) = with(ctx) { - // NOTE: USE '.callee' INSTEAD OF '.method' !!! - val instance = stmt.instance + val callee = stmt.call.callee val unwrappedInstance = if (instance.isFakeObject()) { // TODO support primitives calls @@ -176,15 +177,14 @@ class TsInterpreter( val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } - if (stmt.callee.name == CONSTRUCTOR_NAME) { - // Approximate unresolved constructor: - scope.doWithState { - methodResult = TsMethodResult.Success.MockedCall(unwrappedInstance, stmt.callee) - newStmt(stmt.returnSite) - } - return - } - scope.assert(falseExpr) + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) return } if (classes.size > 1) { @@ -192,28 +192,42 @@ class TsInterpreter( // scope.assert(falseExpr) // return for (cls in classes) { - val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } + val suitableMethods = cls.methods.filter { it.name == callee.name } concreteMethods += suitableMethods } } else { val cls = classes.single() - val suitableMethods = cls.methods.filter { it.name == stmt.callee.name } + val suitableMethods = cls.methods.filter { it.name == callee.name } concreteMethods += suitableMethods } } else { logger.warn { - "Could not resolve method: ${stmt.callee} on type: $type" + "Could not resolve method: $callee on type: $type" } - scope.assert(falseExpr) + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.UNSUPPORTED_RECEIVER_TYPE, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) return } } else { - val methods = resolveEtsMethods(stmt.callee) + val methods = resolveEtsMethods(callee) if (methods.isEmpty()) { - if (stmt.callee.name !in listOf("then")) { - logger.warn { "Could not resolve method: ${stmt.callee}" } + if (callee.name !in listOf("then")) { + logger.warn { "Could not resolve method: $callee" } } - scope.assert(falseExpr) + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) return } concreteMethods += methods @@ -224,14 +238,28 @@ class TsInterpreter( } if (possibleTypes !is TypesResult.SuccessfulTypesResult) { - error("TODO") // is it right? + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.RECEIVER_TYPE_STREAM_UNAVAILABLE, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) + return } val possibleTypesSet = possibleTypes.types.toSet() if (possibleTypesSet.singleOrNull() == EtsAnyType) { - mockMethodCall(scope, stmt.callee) - scope.doWithState { newStmt(stmt.returnSite) } + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.ANY_RECEIVER, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) return } @@ -251,8 +279,8 @@ class TsInterpreter( .asSequence() // TODO wrong order, ancestors are unordered .map { graph.hierarchy.getAncestors(it) } - .mapNotNull { it.firstOrNull { it.methods.any { it.name == stmt.callee.name } } } - .map { clazz to it.methods.first { it.name == stmt.callee.name } } + .mapNotNull { it.firstOrNull { it.methods.any { it.name == callee.name } } } + .map { clazz to it.methods.first { it.name == callee.name } } }.toList().take(10) // TODO check it // logger.info { @@ -298,10 +326,16 @@ class TsInterpreter( if (conditionsWithBlocks.isEmpty()) { logger.warn { - "No suitable methods found for call: ${stmt.callee} with instance: $unwrappedInstance" + "No suitable methods found for call: $callee with instance: $unwrappedInstance" } - mockMethodCall(scope, stmt.callee) - scope.doWithState { newStmt(stmt.returnSite) } + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, + resolvedReceiver = unwrappedInstance, + resolvedArguments = stmt.args, + ) return } @@ -317,8 +351,15 @@ class TsInterpreter( val callee = stmt.callee.executableOverloadImplementation() if (callee.signature.enclosingClass.name == "Log") { - mockMethodCall(scope, callee.signature) - scope.doWithState { newStmt(stmt.returnSite) } + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.LOGGING_CALL, + callee = callee.signature, + resolvedReceiver = stmt.resolvedReceiver, + resolvedArguments = stmt.args.takeLast(stmt.call.args.size), + ) return } @@ -327,8 +368,15 @@ class TsInterpreter( // logger.warn { "No entry point for method: $callee, mocking the call" } // If the method doesn't have entry points, // we go through it, we just mock the call - mockMethodCall(scope, callee.signature) - scope.doWithState { newStmt(stmt.returnSite) } + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + callee = callee.signature, + resolvedReceiver = stmt.resolvedReceiver, + resolvedArguments = stmt.args.takeLast(stmt.call.args.size), + ) return } @@ -612,8 +660,12 @@ class TsInterpreter( } if (!options.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { - mockMethodCall(scope, callExpr.callee) - scope.doWithState { newStmt(stmt) } + unknownCallDispatcher.dispatch( + scope = scope, + call = callExpr, + callSite = stmt, + failureReason = TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, + ) return } } @@ -654,7 +706,12 @@ class TsInterpreter( } // intraprocedural analysis - mockMethodCall(scope, stmt.expr.callee) + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.expr, + callSite = stmt, + failureReason = TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, + ) } private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) { @@ -711,6 +768,7 @@ class TsInterpreter( scope = scope, options = options, hierarchy = graph.hierarchy, + unknownCallDispatcher = unknownCallDispatcher, ) fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { 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 new file mode 100644 index 0000000000..f31e3a6853 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -0,0 +1,298 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsVoidType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.UConcreteHeapRef +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.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsUnknownCallDispatcherTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/baseline/CallFallbackBaseline.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val fullScene = EtsScene(listOf(sourceFile)) + + @Test + fun `inventoried unknown calls use normalized compatibility dispatch`() { + val cases = listOf( + Case("declaredMethodWithoutBodyContinues", TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, true), + Case("allocatedReceiverWithoutMethodContinues", TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, true), + Case( + "unresolvedStaticCallPrunes", + TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, + false, + sceneWithout = "ExternalStatic", + ), + Case( + "unresolvedVirtualCallPrunes", + TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, + false, + sceneWithout = "ExternalReceiver", + ), + Case( + "unresolvedAllocatedReceiverCallPrunes", + listOf( + TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + ), + false, + sceneWithout = "ExternalReceiver", + ), + Case("nonReferenceInstanceCallPrunes", TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, false), + Case( + "unresolvedConstructorContinues", + TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + true, + sceneWithout = "ExternalReceiver", + ), + Case("unresolvedAnyPointerCallPrunes", TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, false), + Case("nonReferencePointerCallContinues", TsUnknownCallFailureReason.NON_REFERENCE_POINTER, true), + Case( + "intraproceduralAssignmentCallContinues", + TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, + true, + tsOptions = TsOptions(interproceduralAnalysis = false), + ), + Case( + "intraproceduralCallStatementContinues", + TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, + true, + tsOptions = TsOptions(interproceduralAnalysis = false), + ), + Case("logCallSkipsBody", TsUnknownCallFailureReason.LOGGING_CALL, true), + Case("booleanConverterPrunes", TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, false), + ) + + cases.forEach { case -> + val scene = case.sceneWithout?.let(::sceneWithout) ?: fullScene + val dispatcher = RecordingUnknownCallDispatcher() + + assertEquals( + case.reachesReturn, + reachesReturn(case.methodName, scene, case.tsOptions, dispatcher), + case.methodName, + ) + assertEquals( + case.reasons, + dispatcher.calls.map { it.failureReason }, + case.methodName, + ) + } + } + + @Test + fun `descriptor keeps typed call data without eagerly resolving arguments`() { + val dispatcher = RecordingUnknownCallDispatcher() + val scene = sceneWithout("ExternalStatic") + + assertFalse(reachesReturn("unresolvedStaticCallPrunes", scene, dispatcher = dispatcher)) + + val call = dispatcher.calls.single() + assertEquals("external", call.callee.name) + assertNull(call.receiver) + assertTrue(call.arguments.isEmpty()) + assertIs(call.resultType) + assertEquals("unresolvedStaticCallPrunes", call.callSite.location.method.name) + } + + @Test + fun `descriptor preserves source and resolved values available at dispatch`() { + val dispatcher = RecordingUnknownCallDispatcher() + + assertFalse(reachesReturn("nonReferenceInstanceCallPrunes", dispatcher = dispatcher)) + + val call = dispatcher.calls.single() + val receiver = assertNotNull(call.receiver) + assertEquals("receiver", assertIs(receiver.source).name) + assertNotNull(receiver.resolved) + assertTrue(call.arguments.isEmpty()) + } + + @Test + fun `normally executable and compatibility-approximated calls bypass unknown dispatch`() { + val methods = listOf( + // The native frontend gives this call a concrete executable target despite the legacy baseline name. + "anyReceiverWithKnownMethodContinues", + "loggerCallSkipsBody", + "toStringUsesPlaceholder", + "valueOfReturnsReceiver", + "mathFloorRoundsTowardNegativeInfinity", + "resourceLookupSkipsBody", + ) + + methods.forEach { methodName -> + val dispatcher = RecordingUnknownCallDispatcher() + + assertTrue(reachesReturn(methodName, dispatcher = dispatcher), methodName) + assertTrue(dispatcher.calls.isEmpty(), methodName) + } + } + + @Test + fun `pre-call allocation failures are documented dispatcher exclusions`() { + val dispatcher = RecordingUnknownCallDispatcher() + + assertFalse(reachesReturn("booleanConstructorUsesTruthiness", dispatcher = dispatcher)) + assertTrue(dispatcher.calls.isEmpty()) + } + + @Test + fun `pointer descriptor pairs its source with the resolved function pointer`() { + val dispatcher = RecordingUnknownCallDispatcher() + val pointerCall = method(fullScene, "associatedLoggingPointerContinues", className = "Log") + .cfg.stmts.mapNotNull { it.callExpr } + .filterIsInstance() + .single() + + assertTrue( + reachesReturn( + "associatedLoggingPointerContinues", + dispatcher = dispatcher, + className = "Log", + ) + ) + + val call = dispatcher.calls.single { it.callSite.location.method.name == "associatedLoggingPointerContinues" } + assertEquals(TsUnknownCallFailureReason.LOGGING_CALL, call.failureReason) + assertEquals(pointerCall.ptr, assertNotNull(call.receiver).source) + assertEquals(true, dispatcher.receiverIsAssociatedFunction.single { it != null }) + } + + @Test + fun `descriptor result type comes from the source overload`() { + val dispatcher = RecordingUnknownCallDispatcher() + + assertTrue(reachesReturn("overloadedDeclaredMethodWithoutBodyContinues", dispatcher = dispatcher)) + + val calls = dispatcher.calls.filter { + it.callSite.location.method.name == "overloadedDeclaredMethodWithoutBodyContinues" + } + assertTrue(calls.isNotEmpty()) + assertTrue(calls.all { it.resultType == EtsNumberType }) + assertTrue(calls.any { it.callee.returnType != it.resultType }) + } + + private fun reachesReturn( + methodName: String, + scene: EtsScene = fullScene, + tsOptions: TsOptions = TsOptions(), + dispatcher: TsUnknownCallDispatcher, + className: String = "CallFallbackBaseline", + ): Boolean = returnStatement(scene, methodName, className) in + reachedStatements(methodName, scene, tsOptions, dispatcher, className) + + private fun reachedStatements( + methodName: String, + scene: EtsScene, + tsOptions: TsOptions, + dispatcher: TsUnknownCallDispatcher, + className: String, + ): Set { + val method = method(scene, methodName, className) + val returnStatement = returnStatement(scene, methodName, className) + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + initialTarget.addChild(TsReachabilityTarget.FinalPoint(returnStatement)) + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = ReachabilityObserver(), + unknownCallDispatcher = dispatcher, + ).use { machine -> + machine.analyze(listOf(method), listOf(initialTarget)) + .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } + } + } + + private fun returnStatement(scene: EtsScene, methodName: String, className: String): EtsReturnStmt = + method(scene, methodName, className).cfg.stmts.filterIsInstance().single() + + private fun method( + scene: EtsScene, + methodName: String, + className: String = "CallFallbackBaseline", + ): EtsMethod = scene.projectClasses + .single { it.name == className } + .methods.single { it.name == methodName } + + private fun sceneWithout(className: String): EtsScene { + val filteredFile = EtsFile( + signature = sourceFile.signature, + classes = sourceFile.classes.filterNot { it.name == className }, + namespaces = sourceFile.namespaces, + importInfos = sourceFile.importInfos, + exportInfos = sourceFile.exportInfos, + ) + return EtsScene(listOf(filteredFile)) + } + + private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher { + val calls = mutableListOf() + val receiverIsAssociatedFunction = mutableListOf() + + override fun dispatch(scope: TsStepScope, call: TsUnknownCall) { + calls += call + val receiver = call.receiver?.resolved as? UConcreteHeapRef + receiverIsAssociatedFunction += receiver?.let { resolved -> + scope.calcOnState { associatedFunction[resolved] != null } + } + TsCompatibilityUnknownCallDispatcher.dispatch(scope, call) + } + } + + private data class Case( + val methodName: String, + val reasons: List, + val reachesReturn: Boolean, + val sceneWithout: String? = null, + val tsOptions: TsOptions = TsOptions(), + ) { + constructor( + methodName: String, + reason: TsUnknownCallFailureReason, + reachesReturn: Boolean, + sceneWithout: String? = null, + tsOptions: TsOptions = TsOptions(), + ) : this(methodName, listOf(reason), reachesReturn, sceneWithout, tsOptions) + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index d0a4c13e38..73735195a9 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -9,6 +9,11 @@ declare class ExternalStatic { static external(): void; } +declare class ExternalOverloads { + static convert(value: number): number; + static convert(value: string): string; +} + class KnownReceiver { known(): number { return 1; @@ -30,6 +35,12 @@ class Log { static record(): number { return 999; } + + associatedLoggingPointerContinues(): number { + const callback = () => 999; + callback(); + return 121; + } } class LoggerFacade { @@ -96,6 +107,10 @@ class CallFallbackBaseline { return 108; } + overloadedDeclaredMethodWithoutBodyContinues(): number { + return ExternalOverloads.convert(41); + } + intraproceduralAssignmentCallContinues(): number { const value = this.known(); return value + 108; From 53fbc6076f0e141d398980124f604bbc99614400 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 23 Aug 2026 01:38:11 +0300 Subject: [PATCH 2/3] [TS Calls] Fix Detekt findings --- .../org/usvm/machine/call/TsUnknownCall.kt | 33 +++++++ .../main/kotlin/org/usvm/machine/expr/Call.kt | 1 - .../org/usvm/machine/expr/TsExprResolver.kt | 4 +- .../usvm/machine/interpreter/TsInterpreter.kt | 99 ++++--------------- .../call/TsUnknownCallDispatcherTest.kt | 15 ++- 5 files changed, 64 insertions(+), 88 deletions(-) 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 bd4fb1611d..e8369f039a 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 @@ -10,6 +10,8 @@ import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UExpr import org.usvm.api.mockMethodCall +import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.newStmt @@ -43,6 +45,7 @@ data class TsUnknownCallValue( val resolved: UExpr<*>?, ) +/** Identifies the execution stage that prevented a TypeScript call from continuing normally. */ enum class TsUnknownCallFailureReason { STATIC_METHOD_NOT_FOUND, NON_REFERENCE_RECEIVER, @@ -59,6 +62,7 @@ enum class TsUnknownCallFailureReason { LOGGING_CALL, } +/** Handles TypeScript calls that could not be executed by the regular call pipeline. */ fun interface TsUnknownCallDispatcher { fun dispatch(scope: TsStepScope, call: TsUnknownCall) } @@ -139,3 +143,32 @@ internal fun TsUnknownCallDispatcher.dispatch( ), ) } + +internal fun TsUnknownCallDispatcher.dispatch( + scope: TsStepScope, + call: TsVirtualMethodCallStmt, + failureReason: TsUnknownCallFailureReason, + resolvedReceiver: UExpr<*>, +) = dispatch( + scope = scope, + call = call.call, + callSite = call.returnSite, + failureReason = failureReason, + resolvedReceiver = resolvedReceiver, + resolvedArguments = call.args, +) + +internal fun TsUnknownCallDispatcher.dispatch( + scope: TsStepScope, + call: TsConcreteMethodCallStmt, + failureReason: TsUnknownCallFailureReason, + callee: EtsMethodSignature, +) = dispatch( + scope = scope, + call = call.call, + callSite = call.returnSite, + failureReason = failureReason, + callee = callee, + resolvedReceiver = call.resolvedReceiver, + resolvedArguments = call.args.takeLast(call.call.args.size), +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt index fa217414d2..5aaa33b7b8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt @@ -6,7 +6,6 @@ import org.jacodb.ets.model.EtsInstanceCallExpr import org.usvm.UExpr import org.usvm.machine.TsContext import org.usvm.machine.TsVirtualMethodCallStmt -import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 5e08d5f5ff..66184e3d19 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -93,11 +93,11 @@ import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.TsContext +import org.usvm.machine.TsOptions import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.dispatch -import org.usvm.machine.TsContext -import org.usvm.machine.TsOptions import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.getGlobals diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 5df08a3394..0bf9f180b4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -85,6 +85,7 @@ import org.usvm.util.type import org.usvm.utils.ensureSat private val logger = KotlinLogging.logger {} +private typealias Reason = TsUnknownCallFailureReason typealias TsStepScope = StepScope @@ -177,14 +178,7 @@ class TsInterpreter( val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_CLASS_NOT_FOUND, unwrappedInstance) return } if (classes.size > 1) { @@ -204,14 +198,7 @@ class TsInterpreter( logger.warn { "Could not resolve method: $callee on type: $type" } - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.UNSUPPORTED_RECEIVER_TYPE, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.UNSUPPORTED_RECEIVER_TYPE, unwrappedInstance) return } } else { @@ -220,14 +207,7 @@ class TsInterpreter( if (callee.name !in listOf("then")) { logger.warn { "Could not resolve method: $callee" } } - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, unwrappedInstance) return } concreteMethods += methods @@ -238,28 +218,14 @@ class TsInterpreter( } if (possibleTypes !is TypesResult.SuccessfulTypesResult) { - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.RECEIVER_TYPE_STREAM_UNAVAILABLE, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_TYPE_STREAM_UNAVAILABLE, unwrappedInstance) return } val possibleTypesSet = possibleTypes.types.toSet() if (possibleTypesSet.singleOrNull() == EtsAnyType) { - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.ANY_RECEIVER, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.ANY_RECEIVER, unwrappedInstance) return } @@ -278,9 +244,13 @@ class TsInterpreter( graph.hierarchy.classesForType(clazz as EtsRefType) .asSequence() // TODO wrong order, ancestors are unordered - .map { graph.hierarchy.getAncestors(it) } - .mapNotNull { it.firstOrNull { it.methods.any { it.name == callee.name } } } - .map { clazz to it.methods.first { it.name == callee.name } } + .map { candidate -> graph.hierarchy.getAncestors(candidate) } + .mapNotNull { ancestors -> + ancestors.firstOrNull { ancestor -> + ancestor.methods.any { method -> method.name == callee.name } + } + } + .map { ancestor -> clazz to ancestor.methods.first { method -> method.name == callee.name } } }.toList().take(10) // TODO check it // logger.info { @@ -328,14 +298,7 @@ class TsInterpreter( logger.warn { "No suitable methods found for call: $callee with instance: $unwrappedInstance" } - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, - resolvedReceiver = unwrappedInstance, - resolvedArguments = stmt.args, - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.NO_SUITABLE_VIRTUAL_TARGET, unwrappedInstance) return } @@ -351,15 +314,7 @@ class TsInterpreter( val callee = stmt.callee.executableOverloadImplementation() if (callee.signature.enclosingClass.name == "Log") { - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.LOGGING_CALL, - callee = callee.signature, - resolvedReceiver = stmt.resolvedReceiver, - resolvedArguments = stmt.args.takeLast(stmt.call.args.size), - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.LOGGING_CALL, callee.signature) return } @@ -368,15 +323,7 @@ class TsInterpreter( // logger.warn { "No entry point for method: $callee, mocking the call" } // If the method doesn't have entry points, // we go through it, we just mock the call - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.call, - callSite = stmt.returnSite, - failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, - callee = callee.signature, - resolvedReceiver = stmt.resolvedReceiver, - resolvedArguments = stmt.args.takeLast(stmt.call.args.size), - ) + unknownCallDispatcher.dispatch(scope, stmt, Reason.METHOD_BODY_UNAVAILABLE, callee.signature) return } @@ -660,12 +607,7 @@ class TsInterpreter( } if (!options.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { - unknownCallDispatcher.dispatch( - scope = scope, - call = callExpr, - callSite = stmt, - failureReason = TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, - ) + unknownCallDispatcher.dispatch(scope, callExpr, stmt, Reason.INTERPROCEDURAL_ANALYSIS_DISABLED) return } } @@ -706,12 +648,7 @@ class TsInterpreter( } // intraprocedural analysis - unknownCallDispatcher.dispatch( - scope = scope, - call = stmt.expr, - callSite = stmt, - failureReason = TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, - ) + unknownCallDispatcher.dispatch(scope, stmt.expr, stmt, Reason.INTERPROCEDURAL_ANALYSIS_DISABLED) } private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) { 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 f31e3a6853..eb47f55f60 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 @@ -15,8 +15,8 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Test import org.usvm.PathSelectionStrategy import org.usvm.SolverType -import org.usvm.UMachineOptions import org.usvm.UConcreteHeapRef +import org.usvm.UMachineOptions import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.machine.TsMachine @@ -42,7 +42,11 @@ class TsUnknownCallDispatcherTest { fun `inventoried unknown calls use normalized compatibility dispatch`() { val cases = listOf( Case("declaredMethodWithoutBodyContinues", TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, true), - Case("allocatedReceiverWithoutMethodContinues", TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, true), + Case( + "allocatedReceiverWithoutMethodContinues", + TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, + true, + ), Case( "unresolvedStaticCallPrunes", TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, @@ -166,7 +170,9 @@ class TsUnknownCallDispatcherTest { fun `pointer descriptor pairs its source with the resolved function pointer`() { val dispatcher = RecordingUnknownCallDispatcher() val pointerCall = method(fullScene, "associatedLoggingPointerContinues", className = "Log") - .cfg.stmts.mapNotNull { it.callExpr } + .cfg + .stmts + .mapNotNull { it.callExpr } .filterIsInstance() .single() @@ -240,7 +246,8 @@ class TsUnknownCallDispatcherTest { className: String = "CallFallbackBaseline", ): EtsMethod = scene.projectClasses .single { it.name == className } - .methods.single { it.name == methodName } + .methods + .single { it.name == methodName } private fun sceneWithout(className: String): EtsScene { val filteredFile = EtsFile( From ba0b432917f8492c37c36ef650128dfd64e87d58 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 23 Aug 2026 01:50:09 +0300 Subject: [PATCH 3/3] [TS Calls] Name compatibility outcomes --- .../call/TsUnknownCallDispatcherTest.kt | 50 ++++++++++++++----- 1 file changed, 37 insertions(+), 13 deletions(-) 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 eb47f55f60..fb71f6263e 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 @@ -41,22 +41,26 @@ class TsUnknownCallDispatcherTest { @Test fun `inventoried unknown calls use normalized compatibility dispatch`() { val cases = listOf( - Case("declaredMethodWithoutBodyContinues", TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, true), + Case( + "declaredMethodWithoutBodyContinues", + TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + reachesReturn = true, + ), Case( "allocatedReceiverWithoutMethodContinues", TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET, - true, + reachesReturn = true, ), Case( "unresolvedStaticCallPrunes", TsUnknownCallFailureReason.STATIC_METHOD_NOT_FOUND, - false, + reachesReturn = false, sceneWithout = "ExternalStatic", ), Case( "unresolvedVirtualCallPrunes", TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, - false, + reachesReturn = false, sceneWithout = "ExternalReceiver", ), Case( @@ -65,32 +69,52 @@ class TsUnknownCallDispatcherTest { TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, ), - false, + reachesReturn = false, sceneWithout = "ExternalReceiver", ), - Case("nonReferenceInstanceCallPrunes", TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, false), + Case( + "nonReferenceInstanceCallPrunes", + TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, + reachesReturn = false, + ), Case( "unresolvedConstructorContinues", TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, - true, + reachesReturn = true, sceneWithout = "ExternalReceiver", ), - Case("unresolvedAnyPointerCallPrunes", TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, false), - Case("nonReferencePointerCallContinues", TsUnknownCallFailureReason.NON_REFERENCE_POINTER, true), + Case( + "unresolvedAnyPointerCallPrunes", + TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, + reachesReturn = false, + ), + Case( + "nonReferencePointerCallContinues", + TsUnknownCallFailureReason.NON_REFERENCE_POINTER, + reachesReturn = true, + ), Case( "intraproceduralAssignmentCallContinues", TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, - true, + reachesReturn = true, tsOptions = TsOptions(interproceduralAnalysis = false), ), Case( "intraproceduralCallStatementContinues", TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, - true, + reachesReturn = true, tsOptions = TsOptions(interproceduralAnalysis = false), ), - Case("logCallSkipsBody", TsUnknownCallFailureReason.LOGGING_CALL, true), - Case("booleanConverterPrunes", TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, false), + Case( + "logCallSkipsBody", + TsUnknownCallFailureReason.LOGGING_CALL, + reachesReturn = true, + ), + Case( + "booleanConverterPrunes", + TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, + reachesReturn = false, + ), ) cases.forEach { case ->