Add incrementation of a game

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

@@ -4,41 +4,80 @@ import org.usvm.UState
 import org.usvm.statistics.BasicBlock
 import org.usvm.statistics.BlockGraph
 import org.usvm.statistics.StepsStatistics
+import org.usvm.util.OnnxModel
+import org.usvm.util.Oracle
 import org.usvm.util.Predictor
 import org.usvm.utils.Game
 import org.usvm.utils.StateWrapper
+import org.usvm.utils.isSat
 
 
 class AIPathSelector<Statement, State, Block>(
     private val blockGraph: BlockGraph<*, Block, Statement>,
     private val stepsStatistics: StepsStatistics<*, State>,
     private val predictor: Predictor<Game<Block>>,
 ) : UPathSelector<State> where
-State : UState<*, *, Statement , *, *, State>,
+State : UState<*, *, Statement, *, *, State>,
 Block : BasicBlock {
     private val statesMap = mutableMapOf<State, StateWrapper<Statement, State, Block>>()
     private var lastPeekedState: State? = null
     private val totalSteps
         get() = stepsStatistics.totalSteps.toInt()
 
+    private var touchedStates = mutableListOf<StateWrapper<Statement, State, Block>>()
+    private var touchedBlocks = mutableListOf<Block>()
+    private var newBlocks = listOf<Block>()
+
     private fun predict(): State {
         val wrappers = statesMap.values
         val vertices = blockGraph.blocks
-        val predictedId = predictor.predictState(Game(vertices, wrappers, blockGraph))
+        val game = buildGame(vertices, wrappers)
+        val predictedId = predictor.predictState(game)
         val predictedState = statesMap.keys.find { it.id == predictedId }
 
         return checkNotNull(predictedState)
     }
 
+    private fun buildGame(
+        vertices: List<Block>,
+        wrappers: MutableCollection<StateWrapper<Statement, State, Block>>
+    ): Game<Block> {
+        val game = when (predictor) {
+            is OnnxModel<Game<Block>> -> Game(vertices, wrappers, blockGraph)
+            is Oracle<Game<Block>> -> {
+                // if we played with default searcher before
+                // client has no information about the game
+                if (lastPeekedState == null) {
+                    Game(vertices, wrappers, blockGraph)
+                } else {
+                    if (blockGraph.newBlocks != newBlocks) {
+                        touchedBlocks.addAll(blockGraph.newBlocks)
+                        newBlocks = blockGraph.newBlocks.toList()
+                    }
+                    if (touchedStates.isEmpty()) touchedStates.addAll(wrappers)
+                    val delta = Game(touchedBlocks.toList(), touchedStates.toList(), blockGraph)
+                    delta
+                }
+            }
+        }
+        touchedStates.clear()
+        touchedBlocks.clear()
+
+        return game
+    }
+
     override fun isEmpty() = statesMap.isEmpty()
 
     override fun peek(): State {
-        if (statesMap.size == 1) {
+        if (totalSteps == 0) {
             return statesMap.keys.single().also { lastPeekedState = it }
         }
 
         val predictedState = predict()
         lastPeekedState = predictedState
+        val wrapper = checkNotNull(statesMap[lastPeekedState])
+        touchedBlocks.add(wrapper.currentBlock)
+        touchedStates.add(wrapper)
 
         return predictedState
     }
@@ -50,8 +89,15 @@ Block : BasicBlock {
             parent?.children?.remove(wrapper)
 
             state.pathNode += state.currentStatement
+
             wrapper.update(totalSteps)
             wrapper.children.clear()
+            wrapper.currentBlock.states.remove(wrapper.id)
+            if (state.isSat())
+                touchedBlocks.addAll(wrapper.history.keys)
+
+            touchedStates.remove(wrapper)
+
         }
     }
 
@@ -71,10 +117,14 @@ Block : BasicBlock {
             statesMap[state] = wrapper
             wrapper
         }
+        touchedStates.addAll(wrappers)
         lastPeekedStateWrapper?.addChildren(wrappers)
     }
 
     override fun update(state: State) {
-        statesMap[state]?.update(totalSteps)
+        val wrapper = statesMap[state]
+        requireNotNull(wrapper)
+        wrapper.update(totalSteps)
+        touchedBlocks.add(wrapper.currentBlock)
     }
 }

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

@@ -158,10 +158,7 @@ private fun <Method, Statement, Target, State, Block> createPathSelector(
 
         PathSelectorCombinationStrategy.SEQUENTIAL -> {
             val selector = SequentialPathSelector(selectors, options.stepsToStart, requireNotNull(stepsStatisticsFactory()))
-
-            val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory)
-            val resultSelector = mergingSelector.wrapIfRequired(options, loopStatisticFactory)
-
+            val resultSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory)
             resultSelector.add(initialStates.toList())
 
             resultSelector

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

@@ -21,12 +21,14 @@ class SequentialPathSelector<State>(
     override fun isEmpty() = currentSelector.isEmpty() && selectors.all { it.isEmpty() }
 
     override fun peek(): State {
+        val peeked = currentSelector.peek()
+
         // currently only either 1 or 2 selectors are supported
         if (totalSteps == stepsToSwitch) {
             ptr = (ptr + 1) % selectors.size
             currentSelector = selectors[ptr]
         }
-        return currentSelector.peek()
+        return peeked
     }
 
     override fun update(state: State) {

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

@@ -1,5 +1,7 @@
 package org.usvm.statistics
 
+import org.usvm.StateId
+
 interface BasicBlock {
     val id: Int
     var inCoverageZone: Boolean
@@ -9,4 +11,6 @@ interface BasicBlock {
     var touchedByState: Boolean
     val containsCall: Boolean
     val containsThrow: Boolean
+
+    val states: MutableList<StateId>
 }

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

@@ -2,6 +2,7 @@ package org.usvm.statistics
 
 interface BlockGraph<Method, Block, Statement> {
     val blocks: List<Block>
+    val newBlocks: List<Block>
 
     fun predecessors(node: Block): Sequence<Block>
     fun successors(node: Block): Sequence<Block>

usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt

@@ -35,19 +35,25 @@ class StateWrapper<Statement, State, Block>(
     var stepWhenMovedLastTime: Int = 0
 
     fun update(steps: Int) {
+        val previousBlock = visitedStatement?.let { currentBlock }
         visitedStatement = checkNotNull(state.pathNode.parent?.statement)
         currentBlock = blockGraph.blockOf(visitedStatement!!)
+        if (previousBlock != currentBlock) {
+            previousBlock?.states?.remove(this@StateWrapper.id)
+            currentBlock.states.add(this@StateWrapper.id)
 
-        position = currentBlock.id
-        pathConditionSize = parentPathConditionSize + state.forkPoints.depth
+            position = currentBlock.id
+            pathConditionSize = parentPathConditionSize + state.forkPoints.depth
+            instructionsVisitedInCurrentBlock = 0
+        }
         visitedAgainVertices = history.values.count { it.numOfVisits > 1 }
-        instructionsVisitedInCurrentBlock = blockGraph.statementsOf(currentBlock).indexOf(visitedStatement) + 1
+        instructionsVisitedInCurrentBlock++
         stepWhenMovedLastTime = steps
 
         updateBlock(stepWhenMovedLastTime)
     }
 
-    fun updateBlock(steps: Int) {
+    private fun updateBlock(steps: Int) {
         history.getOrPut(currentBlock) { StateHistoryElement(position) }.apply {
             val statements = blockGraph.statementsOf(currentBlock)
             if (statements.first() == visitedStatement) {

usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlock.kt

@@ -3,6 +3,7 @@ package org.usvm.machine
 import org.jacodb.api.jvm.JcMethod
 import org.jacodb.api.jvm.cfg.JcInst
 import org.jacodb.api.jvm.cfg.JcInstRef
+import org.usvm.StateId
 import org.usvm.statistics.BasicBlock
 
 data class JcBlock(
@@ -32,4 +33,5 @@ data class JcBlock(
         return inst.index <= end.index && inst.index >= start.index
     }
 
+    override val states = mutableListOf<StateId>()
 }

usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt

@@ -13,6 +13,8 @@ class JcBlockGraph : BlockGraph<JcMethod, JcBlock, JcInst> {
     private val methodToBlocks = mutableMapOf<JcMethod, List<JcBlock>>()
     override val blocks: List<JcBlock>
         get() = methodToBlocks.values.flatten()
+    override var newBlocks = mutableListOf<JcBlock>()
+        private set
 
     private val methodsCache = mutableMapOf<JcMethod, JcGraph>()
 
@@ -86,7 +88,7 @@ class JcBlockGraph : BlockGraph<JcMethod, JcBlock, JcInst> {
 
     private fun cutBlockGraph(blockGraph: JcBlockGraph) {
         val starterBlocks = blockGraph.iterator()
-        val newBlocks = mutableListOf<JcBlock>()
+        newBlocks = mutableListOf()
         starterBlocks.forEach { block ->
             val stmts = blockGraph.instructions(block)
             val currentBlockStmts = mutableListOf<JcInst>()

usvm-ml-gameserver/src/main/kotlin/org.usvm/JavaMethodRunner.kt

@@ -1,20 +1,19 @@
 package org.usvm
 
 import org.usvm.gameserver.GameMap
+import org.usvm.gameserver.Searcher.BFS
+import org.usvm.gameserver.Searcher.DFS
 import org.usvm.machine.JcMachine
+import org.usvm.machine.state.JcState
 import org.usvm.util.JacoDBContainer
+import org.usvm.util.Predictor
 import org.usvm.util.getJcMethodByName
+import org.usvm.util.loadClasspathFromJar
 import org.usvm.util.mapsKey
 import java.io.File
 import kotlin.time.Duration
-import kotlin.time.Duration.Companion.milliseconds
-import org.usvm.gameserver.Searcher.BFS
-import org.usvm.gameserver.Searcher.DFS
-import org.usvm.machine.state.JcState
-import org.usvm.util.Oracle
-import org.usvm.util.loadClasspathFromJar
 
-class JavaMethodRunner(gameMap: GameMap, oracle: Oracle<*>? = null) {
+class JavaMethodRunner(gameMap: GameMap, oracle: Predictor<*>? = null) {
     val jacodbCpKey: String
         get() = mapsKey
 
@@ -37,9 +36,7 @@ class JavaMethodRunner(gameMap: GameMap, oracle: Oracle<*>? = null) {
         pathSelectorCombinationStrategy = PathSelectorCombinationStrategy.SEQUENTIAL,
         coverageZone = CoverageZone.TRANSITIVE,
         exceptionsPropagation = true,
-        timeout = 60_000.milliseconds,
-        stepsFromLastCovered = 3500L,
-        solverTimeout = Duration.INFINITE,
+        timeout = Duration.INFINITE,
         typeOperationsTimeout = Duration.INFINITE,
 
         stepLimit = stepLimit.toULong(),

usvm-ml-gameserver/src/main/kotlin/org.usvm/util/Conversion.kt

@@ -21,7 +21,7 @@ private fun StateHistoryElement.toStateHistoryElem(): StateHistoryElem {
     )
 }
 
-private fun <Block: BasicBlock> StateWrapper<*, *, Block>.toState(): State {
+private fun <Block : BasicBlock> StateWrapper<*, *, Block>.toState(): State {
     return State(
         id,
         position.toUInt(),
@@ -36,7 +36,7 @@ private fun <Block: BasicBlock> StateWrapper<*, *, Block>.toState(): State {
     )
 }
 
-private fun <Block: BasicBlock> Block.toGameMapVertex(states: Collection<StateWrapper<*, *, *>>): GameMapVertex {
+private fun <Block : BasicBlock> Block.toGameMapVertex(): GameMapVertex {
     return GameMapVertex(
         id.toUInt(),
         inCoverageZone,
@@ -46,47 +46,49 @@ private fun <Block: BasicBlock> Block.toGameMapVertex(states: Collection<StateWr
         touchedByState,
         containsCall,
         containsThrow,
+
+        // todo: is it really necessary?
         states
-            .filter { this.id == it.position }
-            .map { it.id }
     )
 }
 
-private fun <Block: BasicBlock> BlockGraph<*, Block, *>.toGameMapEdge(): List<GameMapEdge> {
+private fun <Block : BasicBlock> BlockGraph<*, Block, *>.toGameMapEdge(blocks: Collection<Block>): List<GameMapEdge> {
     return blocks.flatMap { block ->
-        successors(block).map { successor ->
+        val successorsEdges = successors(block).map { successor ->
             GameMapEdge(
                 vertexFrom = block.id.toUInt(),
                 vertexTo = successor.id.toUInt(),
                 label = GameEdgeLabel(0)
             )
         }
 
-        callees(block).map { callee ->
+        val calleesEdges = callees(block).map { callee ->
             GameMapEdge(
                 vertexFrom = block.id.toUInt(),
                 vertexTo = callee.id.toUInt(),
                 label = GameEdgeLabel(1)
             )
         }
 
-        returnOf(block).map { returnSite ->
+        val returnOfEdges = returnOf(block).map { returnSite ->
             GameMapEdge(
                 vertexFrom = block.id.toUInt(),
                 vertexTo = returnSite.id.toUInt(),
                 label = GameEdgeLabel(2)
             )
         }
+
+        successorsEdges + calleesEdges + returnOfEdges
     }
 }
 
-fun <Block: BasicBlock> createGameState(
+fun <Block : BasicBlock> createGameState(
     game: Game<Block>
-    ): GameState {
+): GameState {
     val (vertices, stateWrappers, blockGraph) = game
     return GameState(
-        graphVertices = vertices.map { it.toGameMapVertex(stateWrappers) },
+        graphVertices = vertices.map { it.toGameMapVertex() },
         states = stateWrappers.map { it.toState() },
-        map = blockGraph.toGameMapEdge()
+        map = blockGraph.toGameMapEdge(vertices)
     )
 }