Refactoring and docs

PySymGym · Oct 6, 2024 · 6ab3e0d · 6ab3e0d
1 parent b459601
commit 6ab3e0d
Show file tree

Hide file tree

Showing 7 changed files with 55 additions and 35 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
@@ -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
@@ -112,8 +112,8 @@ private fun <Method, Statement, Target, State, Block> 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 <Method, Statement, State, Block> createAIPathSelector(
     }
 
     val predictor = options.oracle as? Predictor<Game<Block>>
-    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
@@ -4,16 +4,16 @@ 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>
+    fun predecessors(block: Block): Sequence<Block>
+    fun successors(block: Block): Sequence<Block>
 
-    fun callees(node: Block): Sequence<Block>
-    fun callers(node: Block): Sequence<Block>
+    fun callees(block: Block): Sequence<Block>
+    fun callers(block: Block): Sequence<Block>
 
-    fun returnOf(node: Block): Sequence<Block>
+    fun returnOf(block: Block): Sequence<Block>
 
 
     fun methodOf(block: Block): Method
     fun blockOf(inst: Statement): Block
-    fun statementsOf(node: Block): Sequence<Statement>
+    fun statementsOf(block: Block): Sequence<Statement>
 }
diff --git 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<Statement, State, Block>(
 
     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<Int>()
+    var pathConditionSize by Delegates.notNull<Int>()
+    var visitedAgainVertices by Delegates.notNull<Int>()
+    var visitedNotCoveredVerticesInZone by Delegates.notNull<Int>()
+    var visitedNotCoveredVerticesOutOfZone by Delegates.notNull<Int>()
+    var instructionsVisitedInCurrentBlock by Delegates.notNull<Int>()
+    var stepWhenMovedLastTime by Delegates.notNull<Int>()
 
     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<Statement, State, Block>(
         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
@@ -120,27 +120,27 @@ class JcBlockGraph : BlockGraph<JcMethod, JcBlock, JcInst> {
         }
     }
 
-    override fun predecessors(node: JcBlock): Sequence<JcBlock> =
-        predecessorMap.getOrDefault(node, emptySet()).asSequence()
+    override fun predecessors(block: JcBlock): Sequence<JcBlock> =
+        predecessorMap.getOrDefault(block, emptySet()).asSequence()
 
-    override fun successors(node: JcBlock): Sequence<JcBlock> =
-        successorMap.getOrDefault(node, emptySet()).asSequence()
+    override fun successors(block: JcBlock): Sequence<JcBlock> =
+        successorMap.getOrDefault(block, emptySet()).asSequence()
 
-    override fun callees(node: JcBlock): Sequence<JcBlock> =
-        calleesMap.getOrDefault(node, emptySet()).asSequence()
+    override fun callees(block: JcBlock): Sequence<JcBlock> =
+        calleesMap.getOrDefault(block, emptySet()).asSequence()
 
-    override fun callers(node: JcBlock): Sequence<JcBlock> =
-        calleesMap.getOrDefault(node, emptySet()).asSequence()
+    override fun callers(block: JcBlock): Sequence<JcBlock> =
+        calleesMap.getOrDefault(block, emptySet()).asSequence()
 
-    override fun returnOf(node: JcBlock): Sequence<JcBlock> =
-        returnMap.getOrDefault(node, emptySet()).asSequence()
+    override fun returnOf(block: JcBlock): Sequence<JcBlock> =
+        returnMap.getOrDefault(block, emptySet()).asSequence()
 
     override fun methodOf(block: JcBlock): JcMethod =
         block.method
 
     override fun blockOf(inst: JcInst): JcBlock =
         blocks.blockOf(inst)
 
-    override fun statementsOf(node: JcBlock): Sequence<JcInst> =
-        node.stmts.asSequence()
+    override fun statementsOf(block: JcBlock): Sequence<JcInst> =
+        block.stmts.asSequence()
 }
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
@@ -46,8 +46,6 @@ private fun <Block : BasicBlock> 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
@@ -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
 )