From 9d8a839075b053f80b3b3c7c71cbe1a0716f399a Mon Sep 17 00:00:00 2001
From: Yury Kamenev <yurkam447@gmail.com>
Date: Wed, 22 Nov 2023 19:14:28 +0300
Subject: [PATCH] Mocking method without entrypoint (#137)

---
 .../org/usvm/machine/interpreter/JcInterpreter.kt      | 10 +++++++---
 .../main/kotlin/org/usvm/machine/state/JcStateUtils.kt |  8 +-------
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
index d7856dda95..ec68b37f92 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
@@ -238,7 +238,9 @@ class JcInterpreter(
                 }
 
                 val method = stmt.method
-                val entryPoint = applicationGraph.entryPoints(method).single()
+                val entryPoint = applicationGraph.entryPoints(method).singleOrNull()
+                    ?: error("Entrypoint method $method has no entry points")
+
                 scope.doWithState {
                     newStmt(entryPoint)
                 }
@@ -250,13 +252,15 @@ class JcInterpreter(
                     return
                 }
 
-                if (stmt.method.isNative) {
+                val entryPoint = applicationGraph.entryPoints(stmt.method).singleOrNull()
+
+                if (stmt.method.isNative || entryPoint == null) {
                     mockMethod(scope, stmt, applicationGraph)
                     return
                 }
 
                 scope.doWithState {
-                    addNewMethodCall(applicationGraph, stmt)
+                    addNewMethodCall(stmt, entryPoint)
                 }
             }
 
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
index f330606fff..f32a1c3727 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
@@ -9,7 +9,6 @@ import org.jacodb.api.ext.cfg.locals
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
-import org.usvm.machine.JcApplicationGraph
 import org.usvm.machine.JcConcreteMethodCallInst
 import org.usvm.machine.JcDynamicMethodCallInst
 import org.usvm.machine.JcMethodCall
@@ -58,13 +57,8 @@ fun JcState.throwExceptionAndDropStackFrame() {
     }
 }
 
-fun JcState.addNewMethodCall(
-    applicationGraph: JcApplicationGraph,
-    methodCall: JcConcreteMethodCallInst
-) {
+fun JcState.addNewMethodCall(methodCall: JcConcreteMethodCallInst, entryPoint: JcInst) {
     val method = methodCall.method
-    val entryPoint = applicationGraph.entryPoints(method).singleOrNull()
-        ?: error("No entrypoint found for method: $method")
     callStack.push(method, methodCall.returnSite)
     memory.stack.push(methodCall.arguments.toTypedArray(), method.localsCount)
     newStmt(entryPoint)