First working version

UnitTestBot · Sep 19, 2023 · ceb15dd · ceb15dd
1 parent 343a895
commit ceb15dd
Show file tree

Hide file tree

Showing 9 changed files with 459 additions and 371 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/distances/InterprocDistanceCalculator.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/distances/InterprocDistanceCalculator.kt
@@ -104,6 +104,10 @@ internal class InterprocDistanceCalculator<Method, Statement>(
         currentStatement: Statement,
         callStack: UCallStack<Method, Statement>
     ): InterprocDistance {
+        if (callStack.isEmpty()) {
+            return InterprocDistance(UInt.MAX_VALUE, ReachabilityKind.NONE)
+        }
+
         val lastMethod = callStack.lastMethod()
         val lastFrameDistance = calculateFrameDistance(lastMethod, currentStatement)
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/targets/UTarget.kt b/usvm-core/src/main/kotlin/org/usvm/targets/UTarget.kt
@@ -21,28 +21,8 @@ abstract class UTarget<Statement, Target, TargetController : UTargetController>(
     val location: Statement? = null,
 ) where Target : UTarget<Statement, Target, TargetController> {
     private val childrenImpl = mutableListOf<Target>()
-    private var parent: Target? = null
-
-    private var status: Status = Status.UNPROCESSED
-
-    // TODO move it
-    enum class Status {
-        UNPROCESSED,
-        PROCESSING,
-        PROCESSED
-    }
-
-    fun processing() {
-        require(status == Status.UNPROCESSED)
-
-        status = Status.PROCESSING
-    }
-
-    fun processed() {
-        require(status == Status.PROCESSING)
-
-        status = Status.PROCESSED
-    }
+    var parent: Target? = null
+        private set
 
     /**
      * List of the child targets which should be reached after this target.
@@ -60,10 +40,6 @@ abstract class UTarget<Statement, Target, TargetController : UTargetController>(
     var isRemoved = false
         private set
 
-    // TODO add docs
-    fun <State : UState<*, *, *, *, Target, State>> isReachedBy(state: State): Boolean? =
-        location?.let { it == state.currentStatement }
-
     /**
      * Adds a child target to this target.
      * TODO: avoid possible recursion
@@ -84,9 +60,9 @@ abstract class UTarget<Statement, Target, TargetController : UTargetController>(
      * should try to propagate the target. If the target without children has been
      * visited, it is logically removed from tree.
      */
-    protected fun <State : UState<*, *, Statement, *, Target, *>> propagate(byState: State) {
+    fun <T, State : UState<*, *, Statement, *, T, State>> propagate(byState: State) {
         @Suppress("UNCHECKED_CAST")
-        if (byState.tryPropagateTarget(this as Target) && isTerminal) {
+        if (byState.tryPropagateTarget(this as T) && isTerminal) {
             remove()
         }
     }

diff --git a/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt b/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt
@@ -2,5 +2,5 @@ package org.usvm.targets
 
 // TODO add self generic for the controller
 interface UTargetController {
-    val targets: MutableCollection<UTarget<*, *, *>>
+    val targets: MutableCollection<out UTarget<*, *, *>>
 }