Review fixes

UnitTestBot · Jul 20, 2023 · 1bd58b0 · 1bd58b0
1 parent 38c2b2b
commit 1bd58b0
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 15 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/CallStack.kt b/usvm-core/src/main/kotlin/org/usvm/CallStack.kt
@@ -36,11 +36,10 @@ class UCallStack<Method, Statement> private constructor(
     }
 
     fun stackTrace(currentInstruction: Statement): List<UStackTraceFrame<Method, Statement>> {
-        val stacktrace: MutableList<UStackTraceFrame<Method, Statement>> = stack
-            .zipWithNext()
-            .mapTo(mutableListOf()) {
-                UStackTraceFrame(it.first.method, it.second.returnSite!!)
-            }
+        val stacktrace = stack
+            .asSequence()
+            .zipWithNext { first, second -> UStackTraceFrame<Method, Statement>(first.method, second.returnSite!!) }
+            .toMutableList()
 
         return stacktrace + UStackTraceFrame(stack.last().method, currentInstruction)
     }

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,7 +78,9 @@ 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")
+            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/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
@@ -100,7 +100,7 @@ import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.addNewMethodCall
 import org.usvm.machine.state.createUnprocessedException
-import org.usvm.util.extractJcType
+import org.usvm.util.extractJcRefType
 
 /**
  * An expression resolver based on JacoDb 3-address code. A result of resolving is `null`, iff
@@ -541,7 +541,7 @@ class JcExprResolver(
 
     // region implicit exceptions
 
-    private fun allocateException(type: JcType): (JcState) -> Unit = { state ->
+    private fun allocateException(type: JcRefType): (JcState) -> Unit = { state ->
         val address = state.memory.alloc(type)
         state.createUnprocessedException(address, type)
     }
@@ -724,23 +724,23 @@ class JcExprResolver(
     }
 
     private val arrayIndexOutOfBoundsExceptionType by lazy {
-        ctx.extractJcType(IndexOutOfBoundsException::class)
+        ctx.extractJcRefType(IndexOutOfBoundsException::class)
     }
 
     private val negativeArraySizeExceptionType by lazy {
-        ctx.extractJcType(NegativeArraySizeException::class)
+        ctx.extractJcRefType(NegativeArraySizeException::class)
     }
 
     private val arithmeticExceptionType by lazy {
-        ctx.extractJcType(ArithmeticException::class)
+        ctx.extractJcRefType(ArithmeticException::class)
     }
 
     private val nullPointerExceptionType by lazy {
-        ctx.extractJcType(NullPointerException::class)
+        ctx.extractJcRefType(NullPointerException::class)
     }
 
     private val classCastExceptionType by lazy {
-        ctx.extractJcType(ClassCastException::class)
+        ctx.extractJcRefType(ClassCastException::class)
     }
 
     companion object {

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt
@@ -215,7 +215,7 @@ class JcInterpreter(
 
     @Suppress("UNUSED_PARAMETER")
     private fun visitCatchStmt(scope: JcStepScope, stmt: JcCatchInst) {
-        error("The catch instruction must be unfolded during processing of the instructions led to it")
+        error("The catch instruction must be unfolded during processing of the instructions led to it. Encountered inst: $stmt")
     }
 
     private fun visitSwitchStmt(scope: JcStepScope, stmt: JcSwitchInst) {

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt
@@ -1,7 +1,10 @@
 package org.usvm.util
 
+import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
 import org.usvm.machine.JcContext
 import kotlin.reflect.KClass
 
-fun JcContext.extractJcType(clazz: KClass<*>): JcType = cp.findTypeOrNull(clazz.qualifiedName!!)!!
+fun JcContext.extractJcType(clazz: KClass<*>): JcType = cp.findTypeOrNull(clazz.qualifiedName!!)!!
+
+fun JcContext.extractJcRefType(clazz: KClass<*>): JcRefType = extractJcType(clazz) as JcRefType