New symbolic path selectors

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt

@@ -17,10 +17,22 @@ class InstructionSymbolicChecker(
     ctx: ExecutionContext,
     rootMethod: Method,
 ) : SymbolicTraverser(ctx, rootMethod) {
-    override val pathSelector: SymbolicPathSelector = DequePathSelector()
+    override val pathSelector: SymbolicPathSelector
     override val callResolver: SymbolicCallResolver = DefaultCallResolver(ctx)
     override val invokeDynamicResolver: SymbolicInvokeDynamicResolver = DefaultCallResolver(ctx)
 
+    init {
+        val pathSelectorName = kexConfig.getStringValue("symbolic", "pathSelector", "sgs")
+        val n = kexConfig.getIntValue("symbolic", "n", 2)
+        pathSelector = when (pathSelectorName) {
+            "bfs" -> BFS()
+            "sgs" -> SGS(n)
+            "priority-bfs" -> PriorityBFS(n)
+            else -> throw IllegalArgumentException("PathSelector '$pathSelectorName' doesn't exist. " +
+                    "Check InstructionSymbolicChecker to see available path selectors")
+        }
+    }
+
     companion object {
         @ExperimentalTime
         @DelicateCoroutinesApi

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt

@@ -10,7 +10,10 @@ interface SymbolicPathSelector : SuspendableIterator<Pair<TraverserState, BasicB
     suspend operator fun plusAssign(data: Pair<TraverserState, BasicBlock>) = add(data.first, data.second)
 }
 
-class DequePathSelector : SymbolicPathSelector {
+/**
+ * Implements bfs algorithm
+ */
+class BFS : SymbolicPathSelector {
     private val queue = queueOf<Pair<TraverserState, BasicBlock>>()
 
     override suspend fun add(state: TraverserState, block: BasicBlock) {
@@ -21,3 +24,84 @@ class DequePathSelector : SymbolicPathSelector {
 
     override suspend fun next(): Pair<TraverserState, BasicBlock> = queue.poll()
 }
+
+/**
+ * Implements n-subpath algorithm, which makes path decisions based on the frequency of visits to paths of length n
+ */
+class SGS(val n: Int = 2) : SymbolicPathSelector {
+    private val eSVector = mutableSetOf<ExecutionState>()
+    private val pathVisits = mutableMapOf<List<BasicBlock>, Int>()
+
+    override suspend fun add(state: TraverserState, block: BasicBlock) {
+        val newState = ExecutionState(state to block, n)
+        eSVector.add(newState)
+        if (pathVisits[newState.path] == null) {
+            pathVisits[newState.path] = 0
+        }
+    }
+
+    override suspend fun hasNext(): Boolean = eSVector.isNotEmpty()
+
+    override suspend fun next(): Pair<TraverserState, BasicBlock> {
+        val minPath = eSVector.minOf { pathVisits[it.path]!! }
+
+        val selectSet = mutableSetOf<ExecutionState>()
+
+        for (elem in eSVector) {
+            if (pathVisits[elem.path] == minPath) {
+                selectSet.add(elem)
+            }
+        }
+
+        val result =  selectSet.random()
+        pathVisits[result.path] = pathVisits[result.path]!! + 1
+        eSVector.remove(result)
+        return result.node
+    }
+
+    class ExecutionState(
+        val node: Pair<TraverserState, BasicBlock>,
+        pathLength: Int
+    ) {
+        val path: List<BasicBlock> = node.first.blockPath.takeLast(pathLength)
+    }
+}
+
+/**
+ * Implements bfs algorithm, which takes into account frequency of visits to paths of length n from n-subpath
+ */
+class PriorityBFS(val n: Int = 2) : SymbolicPathSelector {
+    private val eSVector = mutableSetOf<ExecutionState>()
+    private val p = mutableMapOf<List<BasicBlock>, Int>()
+
+    override suspend fun add(state: TraverserState, block: BasicBlock) {
+        val newState = ExecutionState(state to block, n)
+        eSVector.add(newState)
+        if (p[newState.path] == null) {
+            p[newState.path] = 0
+        }
+    }
+
+    override suspend fun hasNext(): Boolean = eSVector.isNotEmpty()
+
+    override suspend fun next(): Pair<TraverserState, BasicBlock> {
+        val minLen = eSVector.minOf { it.path.size }
+        val filteredESVector = eSVector.filter { it.path.size == minLen }
+
+        val minPath = filteredESVector.minOf { p[it.path]!! }
+        val filteredESVector2 = filteredESVector.filter { p[it.path] == minPath }
+
+        val result =  filteredESVector2.random()
+
+        p[result.path] = p[result.path]!! + 1
+        eSVector.remove(result)
+        return result.node
+    }
+
+    class ExecutionState(
+        val node: Pair<TraverserState, BasicBlock>,
+        pathLength: Int
+    ) {
+        val path: List<BasicBlock> = node.first.blockPath.takeLast(pathLength)
+    }
+}

kex.ini

@@ -2,6 +2,7 @@
 [kex]
 runtimeDepsPath = runtime-deps/
 libPath = lib/
+rtVersion = 1.8
 kexRtVersion = 0.0.1
 intrinsicsVersion = 0.1.0
 junitVersion = 4.13.2
@@ -12,7 +13,6 @@ computeCoverage = true
 computeCoverageSaturation = false
 printDetailedCoverage = true
 useReflectionInfo = false
-minimizeTestSuite = false
 
 [compile]
 enabled = true
@@ -74,6 +74,7 @@ exclude = class io.netty.buffer.ByteBuf
 timeLimit = 120
 numberOfExecutors = 8
 numberOfConcreteMethods = 3
+pathSelector = sgs
 
 [concolic]
 timeLimit = 120
@@ -126,8 +127,8 @@ useADSolver = false
 
 [ksmt]
 solver = z3
-solver = cvc5
-solver = bitwuzla
+; solver = cvc5
+; solver = bitwuzla
 ; solver = yices
 runners = 1
 seed = 42