Todo fixes, symbolic stacktrace

UnitTestBot · Jul 19, 2023 · 14c17e5 · 14c17e5
1 parent 72af3be
commit 14c17e5
Show file tree

Hide file tree

Showing 6 changed files with 29 additions and 9 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/CallStack.kt b/usvm-core/src/main/kotlin/org/usvm/CallStack.kt
@@ -5,6 +5,11 @@ data class UCallStackFrame<Method, Statement>(
     val returnSite: Statement?,
 )
 
+data class UStackTraceFrame<Method, Statement>(
+    val method: Method,
+    val instruction: Statement,
+)
+
 class UCallStack<Method, Statement> private constructor(
     private val stack: ArrayDeque<UCallStackFrame<Method, Statement>>,
 ) : Collection<UCallStackFrame<Method, Statement>> by stack {
@@ -30,6 +35,16 @@ class UCallStack<Method, Statement> private constructor(
         return UCallStack(newStack)
     }
 
+    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!!)
+            }
+
+        return stacktrace + UStackTraceFrame(stack.last().method, currentInstruction)
+    }
+
     override fun toString(): String {
         var frameCounter = 0
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt
@@ -36,7 +36,11 @@ fun createStopStrategy(
 
     val stepsFromLastCovered = options.stepsFromLastCovered
     if (stepsFromLastCovered != null) {
-        stopStrategies.add(StepsFromLastCoveredStopStrategy(stepsFromLastCovered.toULong(), getCollectedStatesCount))
+        val stepsFromLastCoveredStopStrategy = StepsFromLastCoveredStopStrategy(
+            stepsFromLastCovered.toULong(),
+            getCollectedStatesCount
+        )
+        stopStrategies.add(stepsFromLastCoveredStopStrategy)
     }
 
     if (stopStrategies.isEmpty()) {

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt
@@ -11,7 +11,6 @@ import org.jacodb.impl.features.SyncUsagesExtension
 import org.usvm.statistics.ApplicationGraph
 import java.util.concurrent.ConcurrentHashMap
 
-// TODO: add trap handlers
 /**
  * A [JcApplicationGraphImpl] wrapper.
  */

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) {
-        TODO("Not yet implemented")
+        error("The catch instruction must be unfolded during processing of the instructions led to it")
     }
 
     private fun visitSwitchStmt(scope: JcStepScope, stmt: JcSwitchInst) {

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
@@ -2,9 +2,11 @@ package org.usvm.machine.state
 
 import org.jacodb.api.JcMethod
 import org.jacodb.api.JcType
+import org.jacodb.api.cfg.JcInst
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.UStackTraceFrame
 
 /**
  * Represents a result of a method invocation.
@@ -29,7 +31,7 @@ sealed interface JcMethodResult {
     open class JcException(
         val address: UHeapRef,
         val type: JcType,
-//        val symbolicStackTrace: List<JcMethod> // TODO should it contain locations? Probably, yes. Add message?
+        val symbolicStackTrace: List<UStackTraceFrame<JcMethod, JcInst>>
     ) : JcMethodResult {
         override fun toString(): String = "${this::class.simpleName}: Address: $address, type: ${type.typeName}"
     }
@@ -45,5 +47,6 @@ sealed interface JcMethodResult {
     class UnprocessedJcException(
         address: UHeapRef,
         type: JcType,
-    ) : JcException(address, type)
+        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
@@ -31,11 +31,10 @@ fun JcState.returnValue(valueToReturn: UExpr<out USort>) {
 }
 
 /**
- * TODO change docs
- * Create an unprocessed exception from the [exception] and assign it to the [JcState.methodResult].
+ * 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)
+    methodResult = JcMethodResult.UnprocessedJcException(address, type, callStack.stackTrace(lastStmt))
 }
 
 fun JcState.throwException(exception: JcMethodResult.JcException) {
@@ -47,7 +46,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)
+        JcMethodResult.JcException(exception.address, exception.type, exception.symbolicStackTrace)
     } else {
         exception
     }