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 7bc32f9dd..099d52a2e 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/AIPathSelector.kt @@ -93,11 +93,20 @@ Block : BasicBlock { touchedStates.add(parent) } + /** + * Required for proper handling of visited statement + * in [StateWrapper.update] + */ state.pathNode += state.currentStatement - wrapper.update(totalSteps) + wrapper.children.clear() wrapper.currentBlock.states.remove(wrapper.id) + + /** + * If state [isSat], some blocks may have been covered by + * [org.usvm.statistics.CoverageStatistics.onStateTerminated] + */ if (state.isSat()) touchedBlocks.addAll(wrapper.history.keys) @@ -117,7 +126,6 @@ Block : BasicBlock { parentHistory, blockGraph ) - // statesMap[state] = wrapper wrapper } @@ -129,6 +137,7 @@ Block : BasicBlock { val wrapper = statesMap[state] requireNotNull(wrapper) wrapper.update(totalSteps) + // adding current block after we've made a step 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 11231c64e..4566c8b61 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -112,8 +112,8 @@ private fun createPathSelector( ) PathSelectionStrategy.AI -> createAIPathSelector( - requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for GNN path selector" }, - requireNotNull(stepsStatisticsFactory()) { "Steps statistics is required for GNN path selector" }, + requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for AI path selector" }, + requireNotNull(stepsStatisticsFactory()) { "Steps statistics is required for AI path selector" }, blockGraph, options ) @@ -192,7 +192,7 @@ fun createAIPathSelector( } val predictor = options.oracle as? Predictor> - checkNotNull(predictor) + requireNotNull(predictor) { "Oracle is required for AI path selector" } return AIPathSelector( blockGraph, 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 f8d39f2bc..a59f82917 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/BlockGraph.kt @@ -4,16 +4,16 @@ interface BlockGraph { val blocks: List val newBlocks: List - fun predecessors(node: Block): Sequence - fun successors(node: Block): Sequence + fun predecessors(block: Block): Sequence + fun successors(block: Block): Sequence - fun callees(node: Block): Sequence - fun callers(node: Block): Sequence + fun callees(block: Block): Sequence + fun callers(block: Block): Sequence - fun returnOf(node: Block): Sequence + fun returnOf(block: Block): Sequence fun methodOf(block: Block): Method fun blockOf(inst: Statement): Block - fun statementsOf(node: Block): Sequence + fun statementsOf(block: 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 e4a0fc3ed..494baef11 100644 --- a/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt +++ b/usvm-core/src/main/kotlin/org/usvm/utils/StateWrapper.kt @@ -3,6 +3,7 @@ package org.usvm.utils import org.usvm.UState import org.usvm.statistics.BasicBlock import org.usvm.statistics.BlockGraph +import kotlin.properties.Delegates data class StateHistoryElement( val blockId: Int, @@ -22,18 +23,20 @@ class StateWrapper( private var visitedStatement: Statement? = null lateinit var currentBlock: Block - var position: Int = -1 - var pathConditionSize: Int = -1 - var visitedAgainVertices: Int = -1 - var visitedNotCoveredVerticesInZone: Int = -1 - var visitedNotCoveredVerticesOutOfZone: Int = -1 - var instructionsVisitedInCurrentBlock: Int = -1 - var stepWhenMovedLastTime: Int = -1 + var position by Delegates.notNull() + var pathConditionSize by Delegates.notNull() + var visitedAgainVertices by Delegates.notNull() + var visitedNotCoveredVerticesInZone by Delegates.notNull() + var visitedNotCoveredVerticesOutOfZone by Delegates.notNull() + var instructionsVisitedInCurrentBlock by Delegates.notNull() + var stepWhenMovedLastTime by Delegates.notNull() fun update(steps: Int) { val previousBlock = visitedStatement?.let { currentBlock } - visitedStatement = checkNotNull(state.pathNode.parent?.statement) - currentBlock = blockGraph.blockOf(visitedStatement!!) + // getting parent statement because pathNode is pointing to + // next statement (to step on) + visitedStatement = state.pathNode.parent?.statement + currentBlock = blockGraph.blockOf(checkNotNull(visitedStatement)) if (previousBlock != currentBlock) { previousBlock?.states?.remove(this@StateWrapper.id) currentBlock.states.add(this@StateWrapper.id) @@ -45,8 +48,8 @@ class StateWrapper( instructionsVisitedInCurrentBlock++ stepWhenMovedLastTime = steps - updateBlock(stepWhenMovedLastTime) updateVertexCounts() + updateBlock(stepWhenMovedLastTime) } private fun updateVertexCounts() { 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 d7ea96cc6..78708d78d 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcBlockGraph.kt @@ -120,20 +120,20 @@ class JcBlockGraph : BlockGraph { } } - override fun predecessors(node: JcBlock): Sequence = - predecessorMap.getOrDefault(node, emptySet()).asSequence() + override fun predecessors(block: JcBlock): Sequence = + predecessorMap.getOrDefault(block, emptySet()).asSequence() - override fun successors(node: JcBlock): Sequence = - successorMap.getOrDefault(node, emptySet()).asSequence() + override fun successors(block: JcBlock): Sequence = + successorMap.getOrDefault(block, emptySet()).asSequence() - override fun callees(node: JcBlock): Sequence = - calleesMap.getOrDefault(node, emptySet()).asSequence() + override fun callees(block: JcBlock): Sequence = + calleesMap.getOrDefault(block, emptySet()).asSequence() - override fun callers(node: JcBlock): Sequence = - calleesMap.getOrDefault(node, emptySet()).asSequence() + override fun callers(block: JcBlock): Sequence = + calleesMap.getOrDefault(block, emptySet()).asSequence() - override fun returnOf(node: JcBlock): Sequence = - returnMap.getOrDefault(node, emptySet()).asSequence() + override fun returnOf(block: JcBlock): Sequence = + returnMap.getOrDefault(block, emptySet()).asSequence() override fun methodOf(block: JcBlock): JcMethod = block.method @@ -141,6 +141,6 @@ class JcBlockGraph : BlockGraph { override fun blockOf(inst: JcInst): JcBlock = blocks.blockOf(inst) - override fun statementsOf(node: JcBlock): Sequence = - node.stmts.asSequence() + override fun statementsOf(block: JcBlock): Sequence = + block.stmts.asSequence() } \ No newline at end of file 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 ddcee1944..a87bfc67a 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 @@ -46,8 +46,6 @@ private fun Block.toGameMapVertex(): GameMapVertex { touchedByState, containsCall, containsThrow, - - // todo: is it really necessary? states ) } diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt index 6d76ff58b..39309d6bc 100644 --- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt @@ -112,6 +112,9 @@ enum class PathSelectorCombinationStrategy { */ PARALLEL, + /** + * Two path selectors have a common state set and are used one after another. + */ SEQUENTIAL } @@ -268,7 +271,14 @@ data class UMachineOptions( * */ val loopIterationLimit: Int? = null, + /** + * Limit for [PathSelectorCombinationStrategy.SEQUENTIAL] combinator when the switch + * from one path selector to another occurs. + */ val stepsToStart: UInt = 0u, + /** + * Predictor for AI path selector. + */ val oracle: Predictor<*>? = null )