Remove UnprocessedJcException

UnitTestBot · Jul 24, 2023 · 6655de5 · 6655de5
1 parent 1bd58b0
commit 6655de5
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 23 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt
@@ -78,9 +78,6 @@ class JcTestResolver(
         val result = when (val res = state.methodResult) {
             is JcMethodResult.NoCall -> error("No result found")
             is JcMethodResult.Success -> with(afterScope) { Result.success(resolveExpr(res.value, method.returnType)) }
-            is JcMethodResult.UnprocessedJcException -> {
-                error("An unprocessed exception should never occur in the Resolver, but it did: $res")
-            }
             is JcMethodResult.JcException -> Result.failure(resolveException(res, afterScope))
         }
         val coverage = resolveCoverage(method, state)

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt
@@ -35,18 +35,4 @@ sealed interface JcMethodResult {
     ) : JcMethodResult {
         override fun toString(): String = "${this::class.simpleName}: Address: $address, type: ${type.typeName}"
     }
-
-    /**
-     * An unprocessed exception thrown by a method.
-     *
-     * The difference between it and the [JcMethodResult.JcException] is that
-     * this exception must be treated as an intermediate result of the method analysis,
-     * and it must be handled by an interpreter later, while the [JcException]
-     * is a final result that could be produced as a result of the symbolic execution.
-     */
-    class UnprocessedJcException(
-        address: UHeapRef,
-        type: JcType,
-        symbolicStackTrace: List<UStackTraceFrame<JcMethod, JcInst>>
-    ) : JcException(address, type, symbolicStackTrace)
 }
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
@@ -34,7 +34,7 @@ fun JcState.returnValue(valueToReturn: UExpr<out USort>) {
  * Create an unprocessed exception with the [address] and the [type] and assign it to the [JcState.methodResult].
  */
 fun JcState.createUnprocessedException(address: UHeapRef, type: JcType) {
-    methodResult = JcMethodResult.UnprocessedJcException(address, type, callStack.stackTrace(lastStmt))
+    methodResult = JcMethodResult.JcException(address, type, callStack.stackTrace(lastStmt))
 }
 
 fun JcState.throwException(exception: JcMethodResult.JcException) {
@@ -45,11 +45,7 @@ fun JcState.throwException(exception: JcMethodResult.JcException) {
     }
 
     // TODO: the last place where we distinguish implicitly thrown and explicitly thrown exceptions
-    methodResult = if (exception is JcMethodResult.UnprocessedJcException) {
-        JcMethodResult.JcException(exception.address, exception.type, exception.symbolicStackTrace)
-    } else {
-        exception
-    }
+    methodResult = exception
 
     if (returnSite != null) {
         newStmt(returnSite)