Mocking method without entrypoint (#137)

UnitTestBot · Nov 22, 2023 · 9d8a839 · 9d8a839
1 parent 14f383a
commit 9d8a839
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 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
@@ -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
@@ -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)