small optimizations + add filter to remove number of candidate states

kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexInteger.kt

@@ -7,13 +7,7 @@ import org.vorpal.research.kfg.type.TypeFactory
 
 @InheritorOf("KexType")
 @Serializable
-sealed class KexInteger : KexType() {
-    override fun hashCode() = name.hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        return other?.javaClass == this.javaClass
-    }
-}
+sealed class KexInteger : KexType()
 
 @InheritorOf("KexType")
 @Serializable

kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexReal.kt

@@ -19,12 +19,6 @@ object KexFloat : KexReal() {
         get() = WORD
 
     override fun getKfgType(types: TypeFactory): Type = types.floatType
-
-    override fun hashCode() = name.hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        return other is KexFloat
-    }
 }
 
 @InheritorOf("KexType")
@@ -37,10 +31,4 @@ object KexDouble : KexReal() {
         get() = DWORD
 
     override fun getKfgType(types: TypeFactory): Type = types.doubleType
-
-    override fun hashCode() = name.hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        return other is KexDouble
-    }
 }

kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexType.kt

@@ -307,12 +307,6 @@ object KexVoid : KexType() {
         get() = throw IllegalAccessError("Trying to get bit size of void")
 
     override fun getKfgType(types: TypeFactory): Type = types.voidType
-
-    override fun hashCode() = name.hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        return other is KexVoid
-    }
 }
 
 fun KexType.unMemspaced() = when (this) {

kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt

@@ -100,6 +100,8 @@ sealed class ClauseList : Iterable<Clause> {
 
     abstract fun subState(startInclusive: Int, endExclusive: Int): ClauseList
 
+    open fun subState(endExclusive: Int): ClauseList = subState(0, endExclusive)
+
     abstract operator fun plus(other: ClauseList): ClauseList
     abstract operator fun plus(other: Clause): ClauseList
     override fun toString(): String {
@@ -171,23 +173,35 @@ data class PersistentClauseList(
 
     override fun lastIndexOf(element: Clause): Int = state.lastIndexOf(element)
 
-    override fun subState(startInclusive: Int, endExclusive: Int): PersistentClauseList =
-        PersistentClauseList(state.subList(startInclusive, endExclusive).toPersistentList())
+    override fun subState(startInclusive: Int, endExclusive: Int): PersistentClauseList = when (startInclusive) {
+        0 -> subState(endExclusive)
+        else -> PersistentClauseList(state.subList(startInclusive, endExclusive).toPersistentList())
+    }
+
+    override fun subState(endExclusive: Int): PersistentClauseList {
+        var newClauses = state
+        var index = size - 1
+        repeat(size - endExclusive) {
+            newClauses = newClauses.removeAt(index--)
+        }
+        return PersistentClauseList(newClauses)
+    }
 
     override fun subList(fromIndex: Int, toIndex: Int): PersistentList<Clause> =
         state.subList(fromIndex, toIndex).toPersistentList()
 
     override fun plus(other: ClauseList): PersistentClauseList = PersistentClauseList(state.addAll(other.state))
     override fun plus(other: Clause): PersistentClauseList = PersistentClauseList(state.add(other))
 
-    fun dropLast(n: Int): PersistentClauseList = subState(0, maxOf(0, size - n))
+    fun dropLast(n: Int): PersistentClauseList = subState(maxOf(0, size - n))
 }
 
 @Serializable
 sealed class PathCondition : Iterable<PathClause> {
     abstract val path: List<PathClause>
     override fun iterator(): Iterator<PathClause> = path.iterator()
     abstract fun subPath(startInclusive: Int, endExclusive: Int): PathCondition
+    open fun subPath(endExclusive: Int): PathCondition = subPath(0, endExclusive)
     fun asState() = BasicState(path.map { it.predicate })
 
     abstract operator fun plus(other: PathCondition): PathCondition
@@ -265,13 +279,22 @@ data class PersistentPathCondition(
         subList(startInclusive, endExclusive).toPersistentList()
     )
 
+    override fun subPath(endExclusive: Int): PersistentPathCondition {
+        var newPath = path
+        var index = size - 1
+        repeat(size - endExclusive) {
+            newPath = newPath.removeAt(index--)
+        }
+        return PersistentPathCondition(newPath)
+    }
+
     override fun subList(fromIndex: Int, toIndex: Int): PersistentList<PathClause> =
         path.subList(fromIndex, toIndex).toPersistentList()
 
     override fun plus(other: PathCondition): PersistentPathCondition = PersistentPathCondition(path.addAll(other.path))
     override fun plus(other: PathClause): PersistentPathCondition = PersistentPathCondition(path.add(other))
 
-    fun dropLast(n: Int): PersistentPathCondition = subPath(0, maxOf(0, size - n))
+    fun dropLast(n: Int): PersistentPathCondition = subPath(maxOf(0, size - n))
 }
 
 @Serializable

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt

@@ -94,7 +94,7 @@ class ContextGuidedSelector(
 
         val currentStateState = currentState.context.symbolicState
         val stateSize = currentStateState.clauses.indexOf(currentState.activeClause)
-        val state = currentStateState.clauses.subState(0, stateSize)
+        val state = currentStateState.clauses.subState(stateSize)
 
         return method to persistentSymbolicState(
             state,

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt

@@ -5,6 +5,7 @@ import kotlinx.collections.immutable.toPersistentList
 import org.vorpal.research.kex.ExecutionContext
 import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException
 import org.vorpal.research.kex.asm.manager.instantiationManager
+import org.vorpal.research.kex.config.kexConfig
 import org.vorpal.research.kex.ktype.KexRtManager.isKexRt
 import org.vorpal.research.kex.ktype.kexType
 import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate
@@ -253,6 +254,8 @@ class CandidateState(
     val nextInstruction: Instruction?
     var score: Long = 0L
 
+    private val hashCode = state.hashCode()
+
     init {
         val cm = method.cm
         val currentClause = state.path.last()
@@ -342,7 +345,7 @@ class CandidateState(
     }
 
     override fun hashCode(): Int {
-        return state.hashCode()
+        return hashCode
     }
 }
 
@@ -363,6 +366,8 @@ class ExecutionGraph(
         it["STATE" to root.instruction] = root
     }
     private val instructionGraph = InstructionGraph(targets)
+    private val maximalCandidateCapacity = kexConfig.getLongValue("concolic", "maximalCandidateCapacity", 50_000L)
+
     val candidates = CandidateSet(ctx)
 
     override val entry: Vertex
@@ -376,6 +381,8 @@ class ExecutionGraph(
         private var totalScore: Long = 0L
         private val candidates = hashSetOf<CandidateState>()
 
+        val size get() = candidates.size
+
         override fun iterator(): Iterator<CandidateState> = candidates.iterator()
 
         fun isEmpty() = candidates.isEmpty()
@@ -421,6 +428,13 @@ class ExecutionGraph(
             }
             return unreachable { log.error("Unexpected error") }
         }
+
+        fun cleanUnreachables(): Boolean {
+            if (!isValid) recomputeScores()
+            return candidates.removeAll { it.score <= 1 }.also {
+                totalScore = candidates.sumOf { it.score }
+            }
+        }
     }
 
     private fun CandidateState.recomputeScore() {
@@ -473,8 +487,13 @@ class ExecutionGraph(
 
             // candidate states calculation part
             ++clauseIndex
-            // TODO: limit number of states
-//                if (clauseIndex > 10_000) break
+
+            // limit maximum number of states in candidate set
+            if (candidates.size > maximalCandidateCapacity) {
+                val cleanupSuccessful = candidates.cleanUnreachables()
+                if (!cleanupSuccessful) break
+            }
+
             if (clause is PathClause) ++pathIndex
 
             val type = when (clause) {
@@ -496,8 +515,8 @@ class ExecutionGraph(
                 candidates.addAll(
                     currentVertex.addStateAndProduceCandidates(
                         ctx, persistentSymbolicState(
-                            symbolicState.clauses.subState(0, clauseIndex),
-                            symbolicState.path.subPath(0, pathIndex),
+                            symbolicState.clauses.subState(clauseIndex),
+                            symbolicState.path.subPath(pathIndex),
                             symbolicState.concreteTypes,
                             symbolicState.concreteValues,
                             symbolicState.termMap

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt

@@ -16,6 +16,7 @@ import org.vorpal.research.kthelper.logging.log
 import org.vorpal.research.kthelper.`try`
 import java.net.ServerSocket
 
+@Suppress("unused")
 class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : ConcolicPathSelector {
 
     override val ctx = concolicPathSelector.ctx
@@ -74,8 +75,8 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) :
         val state = graph.findStateByPathClause(pathClause) ?: return null
 
         val revertedClause = reverse(pathClause) ?: return null
-        val clauses = state.clauses.subState(0, state.clauses.indexOf(pathClause))
-        val path = state.path.subPath(0, state.path.indexOf(pathClause))
+        val clauses = state.clauses.subState(state.clauses.indexOf(pathClause))
+        val path = state.path.subPath(state.path.indexOf(pathClause))
 
         return persistentSymbolicState(
             clauses,