From c8af9e6c20a6cc6a87a4903be36c6eb2286be58c Mon Sep 17 00:00:00 2001 From: ancavar Date: Sun, 22 Sep 2024 17:33:44 +0300 Subject: [PATCH] Add incrementation of a game --- .../main/kotlin/org/usvm/ps/AIPathSelector.kt | 58 +++++++++++++++++-- .../kotlin/org/usvm/ps/PathSelectorFactory.kt | 5 +- .../org/usvm/ps/SequentialPathSelector.kt | 4 +- .../kotlin/org/usvm/statistics/BasicBlock.kt | 4 ++ .../kotlin/org/usvm/statistics/BlockGraph.kt | 1 + .../kotlin/org/usvm/utils/StateWrapper.kt | 14 +++-- .../main/kotlin/org/usvm/machine/JcBlock.kt | 2 + .../kotlin/org/usvm/machine/JcBlockGraph.kt | 4 +- .../main/kotlin/org.usvm/JavaMethodRunner.kt | 17 +++--- .../main/kotlin/org.usvm/util/Conversion.kt | 26 +++++---- 10 files changed, 99 insertions(+), 36 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt index 5bdbd4b128..2550fe8c5b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt @@ -4,9 +4,12 @@ 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( @@ -14,31 +17,67 @@ class AIPathSelector( private val stepsStatistics: StepsStatistics<*, State>, private val predictor: Predictor>, ) : UPathSelector where -State : UState<*, *, Statement , *, *, State>, +State : UState<*, *, Statement, *, *, State>, Block : BasicBlock { private val statesMap = mutableMapOf>() private var lastPeekedState: State? = null private val totalSteps get() = stepsStatistics.totalSteps.toInt() + private var touchedStates = mutableListOf>() + private var touchedBlocks = mutableListOf() + private var newBlocks = listOf() + 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, + wrappers: MutableCollection> + ): Game { + val game = when (predictor) { + is OnnxModel> -> Game(vertices, wrappers, blockGraph) + is Oracle> -> { + // 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) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index 381da35188..11231c64e4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -158,10 +158,7 @@ private fun 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 diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/SequentialPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/SequentialPathSelector.kt index 9874d2b6c5..a92792ff3b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/SequentialPathSelector.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/SequentialPathSelector.kt @@ -21,12 +21,14 @@ class SequentialPathSelector( 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) { diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/BasicBlock.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/BasicBlock.kt index 51b4f1e5a6..d79b69f4f0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/BasicBlock.kt +++ b/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 } diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt index 2598439444..f8d39f2bc2 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt @@ -2,6 +2,7 @@ package org.usvm.statistics interface BlockGraph { val blocks: List + val newBlocks: List fun predecessors(node: Block): Sequence fun successors(node: Block): Sequence diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt b/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt index f0b897b7bd..aa2930e06f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt +++ b/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt @@ -35,19 +35,25 @@ class StateWrapper( 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) { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlock.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlock.kt index ec92fb0b33..04972b6b5a 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlock.kt +++ b/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() } \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt index a707aa1b48..e8afb3732d 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt @@ -13,6 +13,8 @@ class JcBlockGraph : BlockGraph { private val methodToBlocks = mutableMapOf>() override val blocks: List get() = methodToBlocks.values.flatten() + override var newBlocks = mutableListOf() + private set private val methodsCache = mutableMapOf() @@ -86,7 +88,7 @@ class JcBlockGraph : BlockGraph { private fun cutBlockGraph(blockGraph: JcBlockGraph) { val starterBlocks = blockGraph.iterator() - val newBlocks = mutableListOf() + newBlocks = mutableListOf() starterBlocks.forEach { block -> val stmts = blockGraph.instructions(block) val currentBlockStmts = mutableListOf() diff --git a/usvm-ml-gameserver/src/main/kotlin/org.usvm/JavaMethodRunner.kt b/usvm-ml-gameserver/src/main/kotlin/org.usvm/JavaMethodRunner.kt index a428e5a487..a24f98ba04 100644 --- a/usvm-ml-gameserver/src/main/kotlin/org.usvm/JavaMethodRunner.kt +++ b/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(), diff --git a/usvm-ml-gameserver/src/main/kotlin/org.usvm/util/Conversion.kt b/usvm-ml-gameserver/src/main/kotlin/org.usvm/util/Conversion.kt index 881bdd1e0d..ddcee19445 100644 --- a/usvm-ml-gameserver/src/main/kotlin/org.usvm/util/Conversion.kt +++ b/usvm-ml-gameserver/src/main/kotlin/org.usvm/util/Conversion.kt @@ -21,7 +21,7 @@ private fun StateHistoryElement.toStateHistoryElem(): StateHistoryElem { ) } -private fun StateWrapper<*, *, Block>.toState(): State { +private fun StateWrapper<*, *, Block>.toState(): State { return State( id, position.toUInt(), @@ -36,7 +36,7 @@ private fun StateWrapper<*, *, Block>.toState(): State { ) } -private fun Block.toGameMapVertex(states: Collection>): GameMapVertex { +private fun Block.toGameMapVertex(): GameMapVertex { return GameMapVertex( id.toUInt(), inCoverageZone, @@ -46,15 +46,15 @@ private fun Block.toGameMapVertex(states: Collection BlockGraph<*, Block, *>.toGameMapEdge(): List { +private fun BlockGraph<*, Block, *>.toGameMapEdge(blocks: Collection): List { return blocks.flatMap { block -> - successors(block).map { successor -> + val successorsEdges = successors(block).map { successor -> GameMapEdge( vertexFrom = block.id.toUInt(), vertexTo = successor.id.toUInt(), @@ -62,7 +62,7 @@ private fun BlockGraph<*, Block, *>.toGameMapEdge(): List + val calleesEdges = callees(block).map { callee -> GameMapEdge( vertexFrom = block.id.toUInt(), vertexTo = callee.id.toUInt(), @@ -70,23 +70,25 @@ private fun BlockGraph<*, Block, *>.toGameMapEdge(): List + val returnOfEdges = returnOf(block).map { returnSite -> GameMapEdge( vertexFrom = block.id.toUInt(), vertexTo = returnSite.id.toUInt(), label = GameEdgeLabel(2) ) } + + successorsEdges + calleesEdges + returnOfEdges } } -fun createGameState( +fun createGameState( game: Game - ): 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) ) }