Used mocking for Throwable methods instead of skip

usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt

@@ -47,7 +47,7 @@ class JcApplicationGraph(
 
     private val typedMethodsCache = ConcurrentHashMap<JcMethod, JcTypedMethod>()
 
-    val JcMethod.typed
+    val JcMethod.typed: JcTypedMethod
         get() = typedMethodsCache.getOrPut(this) {
             enclosingClass.toType().declaredMethods.first { it.method == this }
         }

usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt

@@ -57,8 +57,8 @@ import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.interpreter.JcExprResolver
 import org.usvm.machine.interpreter.JcStepScope
+import org.usvm.machine.mocks.mockMethod
 import org.usvm.machine.state.JcState
-import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.skipMethodInvocationWithValue
 import org.usvm.sizeSort
 import org.usvm.types.first
@@ -510,12 +510,11 @@ class JcMethodApproximationResolver(
 
     private fun skipMethodIfThrowable(methodCall: JcMethodCall): Boolean = with(methodCall) {
         if (method.enclosingClass.name == "java.lang.Throwable") {
-            scope.doWithState {
-                val nextStmt = applicationGraph.successors(methodCall.returnSite).single()
-                newStmt(nextStmt)
-            }
+            // We assume that methods of java.lang.Throwable are not really required to be analysed and can be simply mocked
+            mockMethod(scope, methodCall, applicationGraph)
             return true
         }
+
         return false
     }
 

usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt

@@ -56,6 +56,7 @@ import org.usvm.machine.JcMethodCall
 import org.usvm.machine.JcMethodCallBaseInst
 import org.usvm.machine.JcMethodEntrypointInst
 import org.usvm.machine.JcVirtualMethodCallInst
+import org.usvm.machine.mocks.mockMethod
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.addNewMethodCall
@@ -65,7 +66,6 @@ import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
-import org.usvm.machine.state.skipMethodInvocationWithValue
 import org.usvm.machine.state.throwExceptionAndDropStackFrame
 import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop
 import org.usvm.memory.ULValue
@@ -250,7 +250,7 @@ class JcInterpreter(
                 }
 
                 if (stmt.method.isNative) {
-                    mockMethod(scope, stmt)
+                    mockMethod(scope, stmt, applicationGraph)
                     return
                 }
 
@@ -586,34 +586,4 @@ class JcInterpreter(
         val exprResolver = exprResolverWithScope(scope)
         return approximationResolver.approximate(scope, exprResolver, methodCall)
     }
-
-    private fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall) {
-        val returnType = with(applicationGraph) { methodCall.method.typed }.returnType
-        mockMethod(scope, methodCall, returnType)
-    }
-
-    private fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall, returnType: JcType) = with(methodCall) {
-        logger.warn { "Mocked: ${method.enclosingClass.name}::${method.name}" }
-
-        if (returnType == ctx.cp.void) {
-            scope.doWithState { skipMethodInvocationWithValue(methodCall, ctx.voidValue) }
-            return@with
-        }
-
-        val mockSort = ctx.typeToSort(returnType)
-        val mockValue = scope.calcOnState {
-            memory.mocker.call(method, arguments.asSequence(), mockSort)
-        }
-
-        if (mockSort == ctx.addressSort) {
-            val constraint = scope.calcOnState {
-                memory.types.evalIsSubtype(mockValue.asExpr(ctx.addressSort), returnType)
-            }
-            scope.assert(constraint) ?: return
-        }
-
-        scope.doWithState {
-            skipMethodInvocationWithValue(methodCall, mockValue)
-        }
-    }
 }

usvm-jvm/src/main/kotlin/org/usvm/machine/mocks/JcMocker.kt

@@ -0,0 +1,50 @@
+package org.usvm.machine.mocks
+
+import io.ksmt.utils.asExpr
+import org.jacodb.api.JcType
+import org.jacodb.api.ext.void
+import org.usvm.UMocker
+import org.usvm.machine.JcApplicationGraph
+import org.usvm.machine.JcMethodCall
+import org.usvm.machine.interpreter.JcStepScope
+import org.usvm.machine.logger
+import org.usvm.machine.state.skipMethodInvocationWithValue
+
+/**
+ * Mocks this [methodCall] with its return type according to the [applicationGraph].
+ */
+fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall, applicationGraph: JcApplicationGraph) {
+    val returnType = with(applicationGraph) { methodCall.method.typed }.returnType
+    mockMethod(scope, methodCall, returnType)
+}
+
+/**
+ * Mocks this [methodCall] using [UMocker] of this [scope] with a value of corresponding [returnType],
+ * and moves to the next stmt.
+ */
+fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall, returnType: JcType) = with(methodCall) {
+    logger.warn { "Mocked: ${method.enclosingClass.name}::${method.name}" }
+
+    val ctx = scope.calcOnState { ctx }
+
+    if (returnType == ctx.cp.void) {
+        scope.doWithState { skipMethodInvocationWithValue(methodCall, ctx.voidValue) }
+        return@with
+    }
+
+    val mockSort = ctx.typeToSort(returnType)
+    val mockValue = scope.calcOnState {
+        memory.mocker.call(method, arguments.asSequence(), mockSort)
+    }
+
+    if (mockSort == ctx.addressSort) {
+        val constraint = scope.calcOnState {
+            memory.types.evalIsSubtype(mockValue.asExpr(ctx.addressSort), returnType)
+        }
+        scope.assert(constraint) ?: return
+    }
+
+    scope.doWithState {
+        skipMethodInvocationWithValue(methodCall, mockValue)
+    }
+}

usvm-jvm/src/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java

@@ -146,4 +146,14 @@ public int symbolicExceptionCheck(Exception e) {
             return 4;
         }
     }
-}
+
+    public Class<? extends Throwable> tryThrowableMethod() {
+        Throwable throwable = new RuntimeException();
+        try {
+            Throwable cause = throwable.getCause();
+            return cause.getClass();
+        } catch (NullPointerException e) {
+            return NullPointerException.class;
+        }
+    }
+}

usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt

@@ -124,4 +124,14 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() {
             { _, e, r -> e !is RuntimeException && r == 4 },
         )
     }
-}
+
+    @Test
+    fun testTryThrowableMethod() {
+        checkDiscoveredProperties(
+            ExceptionExamples::tryThrowableMethod,
+            eq(2),
+            { _, r -> r == NullPointerException::class.java },
+            { _, r -> r == Throwable::class.java },
+        )
+    }
+}