Review fixes

usvm-core/src/main/kotlin/org/usvm/Machine.kt

@@ -3,7 +3,6 @@ package org.usvm
 import mu.KLogging
 import org.usvm.statistics.UMachineObserver
 import org.usvm.stopstrategies.StopStrategy
-import org.usvm.stopstrategies.stopReason
 import org.usvm.util.bracket
 import org.usvm.util.debug
 
@@ -67,7 +66,7 @@ abstract class UMachine<State> : AutoCloseable {
             }
 
             if (!pathSelector.isEmpty()) {
-                logger.debug { stopReason(stopStrategy) }
+                logger.debug { stopStrategy.stopReason() }
             }
         }
     }

usvm-core/src/main/kotlin/org/usvm/ps/ExceptionPropagationPathSelector.kt

@@ -2,46 +2,45 @@ package org.usvm.ps
 
 import org.usvm.UPathSelector
 import org.usvm.UState
+import java.util.IdentityHashMap
 
 /**
  * A class designed to give the highest priority to the states containing exceptions.
  */
 class ExceptionPropagationPathSelector<State : UState<*, *, *, *>>(
     private val selector: UPathSelector<State>,
 ) : UPathSelector<State> {
-    // An internal queue for states containing exceptions
-    private val exceptionalStates: MutableList<State> = mutableListOf()
-
-    // A set containing hash codes of the identities of the states
-    // containing in the `exceptionalStates`. It is required
-    // to be able to determine whether a particular state is in the queue.
-    private val exceptionalStatesHashCodes: MutableSet<Int> = mutableSetOf()
-
-    // A set of hash codes of the states that were added in the internal selector.
+    // An internal queue for states containing exceptions.
+    // Note that we use an identity map here to be able
+    // to determine whether some state is already in the queue or not
+    // without extra time consumption.
+    // We use only keys from this map.
+    private val exceptionalStates = IdentityHashMap<State, Any?>()
+
+    // An identity map of the states that were added in the internal selector.
     // That means that these states present not only in the internal queue, but in
     // the queue of the selector, and we have to process them as well.
-    private val statesInSelectorHashCodes: MutableSet<Int> = mutableSetOf()
+    // We use only keys from this map.
+    private val statesInSelector = IdentityHashMap<State, Any?>()
 
     override fun isEmpty(): Boolean = exceptionalStates.isEmpty() && selector.isEmpty()
 
     /**
      * Returns an exceptional state from the internal queue if it is not empty, or
      * the result of [peek] method called on the wrapper selector.
      */
-    override fun peek(): State = exceptionalStates.lastOrNull() ?: selector.peek()
+    override fun peek(): State = exceptionalStates.keys.lastOrNull() ?: selector.peek()
 
     override fun update(state: State) {
-        val stateHashCode = System.identityHashCode(state)
-        val alreadyInExceptionalStates = stateHashCode in exceptionalStatesHashCodes
+        val alreadyInExceptionalStates = state in exceptionalStates
         val isExceptional = state.isExceptional
 
         when {
             // A case when the state became exceptional, but at the
             // previous step it didn't contain any exceptions.
             // We add this exceptional state to the internal queue.
             isExceptional && !alreadyInExceptionalStates -> {
-                exceptionalStatesHashCodes += stateHashCode
-                exceptionalStates += state
+                exceptionalStates += state to null
             }
             // A case when the state contained an exception at the previous step,
             // but it doesn't contain it anymore. There are two possibilities:
@@ -51,12 +50,11 @@ class ExceptionPropagationPathSelector<State : UState<*, *, *, *>>(
             // exceptional queue, in the second one just removal is enough since
             // it was added in the selector earlier.
             !isExceptional && alreadyInExceptionalStates -> {
-                exceptionalStatesHashCodes -= stateHashCode
                 exceptionalStates -= state
 
-                if (stateHashCode !in statesInSelectorHashCodes) {
+                if (state !in statesInSelector) {
                     selector.add(listOf(state))
-                    statesInSelectorHashCodes += stateHashCode
+                    statesInSelector += state to null
                 }
             }
 
@@ -65,7 +63,7 @@ class ExceptionPropagationPathSelector<State : UState<*, *, *, *>>(
         }
 
         // If the state is contained in the selector, we must call `update` operation for it.
-        if (stateHashCode in statesInSelectorHashCodes) {
+        if (state in statesInSelector) {
             selector.update(state)
         }
     }
@@ -79,35 +77,28 @@ class ExceptionPropagationPathSelector<State : UState<*, *, *, *>>(
         val statesToAdd = mutableListOf<State>()
 
         states.forEach {
-            val identityHashCode = System.identityHashCode(it)
-
             // It if it is an exceptional state, we don't have to worry whether it
             // is contains in the selector or not. It was either already added in it,
             // or will be added later if required, when it becomes unexceptional one.
             if (it.isExceptional) {
-                exceptionalStates += it
-                exceptionalStatesHashCodes += identityHashCode
+                exceptionalStates += it to null
             } else {
                 // Otherwise, we simply add it to the selector directly.
                 statesToAdd += it
-                statesInSelectorHashCodes += identityHashCode
+                statesInSelector += it to null
             }
         }
 
         selector.add(statesToAdd)
     }
 
     override fun remove(state: State) {
-        val stateHashCode = System.identityHashCode(state)
-
-        if (stateHashCode in exceptionalStatesHashCodes) {
+        if (state in exceptionalStates) {
             exceptionalStates -= state
-            exceptionalStatesHashCodes -= stateHashCode
         }
 
-        if (stateHashCode in statesInSelectorHashCodes) {
+        if (state in statesInSelector) {
             selector.remove(state)
-            statesInSelectorHashCodes.remove(stateHashCode)
         }
     }
-}
+}

usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt

@@ -39,7 +39,7 @@ class CoverageStatistics<Method, Statement, State : UState<*, *, Method, Stateme
      * e.g., like in the [TransitiveCoverageZoneObserver].
      */
     fun addCoverageZone(method: Method) {
-        if (method in uncoveredStatements.keys) return
+        if (method in uncoveredStatements) return
 
         val methodStatements = bfsTraversal(
             applicationGraph.entryPoints(method).toList(),

usvm-core/src/main/kotlin/org/usvm/statistics/TransitiveCoverageZoneObserver.kt

@@ -1,7 +1,7 @@
 package org.usvm.statistics
 
 /**
- * Adds new coverage zones if some state contained an instruction
+ * Adds new coverage zones if some state contains an instruction
  * that doesn't belong to any of the already known coverage zones.
  *
  * [ignoreMethod] is a predicate allowing to filter out some methods,

usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepsFromLastCoveredStopStrategy.kt

@@ -5,16 +5,8 @@ package org.usvm.stopstrategies
  */
 class StepsFromLastCoveredStopStrategy(
     private val limit: ULong,
-    getCollectedStatesCount: (() -> Int)?,
+    private val collectedStateCount: () -> Int,
 ) : StopStrategy {
-    private val collectedStateCount: () -> Int
-
-    init {
-        collectedStateCount = requireNotNull(getCollectedStatesCount) {
-            "You must specify a provider of the number of collected states to be able to use this stop strategy"
-        }
-    }
-
     private var counter = 0UL
     private var lastStatesCounter = collectedStateCount()
 

usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategy.kt

@@ -9,6 +9,8 @@ fun interface StopStrategy {
      * If true, symbolic execution process is terminated.
      */
     fun shouldStop(): Boolean
+
+    fun stopReason(): String = "Stop reason: ${this::class.simpleName ?: this}"
 }
 
 class GroupedStopStrategy(
@@ -18,14 +20,7 @@ class GroupedStopStrategy(
 
     override fun shouldStop() = strategies.any { it.shouldStop() }
 
-    fun stopReason(): String = strategies
+    override fun stopReason(): String = strategies
         .filter { it.shouldStop() }
         .joinToString(prefix = "Stop reasons: ", separator = ", ") { "${it::class.simpleName ?: it}" }
 }
-
-fun stopReason(stopStrategy: StopStrategy): String =
-    if (stopStrategy is GroupedStopStrategy) {
-        stopStrategy.stopReason()
-    } else {
-        "Stop reason: ${stopStrategy::class.simpleName ?: stopStrategy}"
-    }

usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt

@@ -35,7 +35,7 @@ fun createStopStrategy(
     }
 
     val stepsFromLastCovered = options.stepsFromLastCovered
-    if (stepsFromLastCovered != null) {
+    if (stepsFromLastCovered != null && getCollectedStatesCount != null) {
         val stepsFromLastCoveredStopStrategy = StepsFromLastCoveredStopStrategy(
             stepsFromLastCovered.toULong(),
             getCollectedStatesCount