Added RandomizedPriorityActionStrategy

UnitTestBot · Feb 22, 2024 · 553d719 · 553d719
1 parent cfd5d91
commit 553d719
Show file tree

Hide file tree

Showing 9 changed files with 179 additions and 75 deletions.
diff --git a/usvm-python/src/test/kotlin/manualTest.kt b/usvm-python/src/test/kotlin/manualTest.kt
@@ -54,9 +54,9 @@ private fun buildSampleRunConfig(): RunConfig {
         """.trimIndent()
     )*/
     val function = PyUnpinnedCallable.constructCallableFromName(
-        listOf(PythonAnyType),
-        "f",
-        "tricky.CompositeObjects"
+        listOf(typeSystem.pythonList),
+        "reverse_usage",
+        "Lists"
     )
     val functions = listOf(function)
     return RunConfig(program, typeSystem, functions)

diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt
@@ -12,7 +12,7 @@ import kotlin.time.Duration.Companion.seconds
 
 class ListsTest : PythonTestRunnerForPrimitiveProgram(
     "Lists",
-    UMachineOptions(stepLimit = 20U)
+    UMachineOptions(stepLimit = 35U)
 ) {
     init {
         timeoutPerRunMs = 2000
@@ -165,7 +165,7 @@ class ListsTest : PythonTestRunnerForPrimitiveProgram(
             constructFunction("sum_of_elements", listOf(typeSystem.pythonList)),
             ignoreNumberOfAnalysisResults,
             standardConcolicAndConcreteChecks,
-            /* invariants = */ listOf { x, res -> x.typeName == "list" && res.typeName == "int" },
+            /* invariants = */ listOf { x, _ -> x.typeName == "list" },
             /* propertiesToDiscover = */ List(4) { index ->
                 { _, res -> res.repr == (index + 1).toString() }
             }
@@ -178,7 +178,7 @@ class ListsTest : PythonTestRunnerForPrimitiveProgram(
             constructFunction("for_loop", listOf(typeSystem.pythonList)),
             ignoreNumberOfAnalysisResults,
             standardConcolicAndConcreteChecks,
-            /* invariants = */ listOf { x, res -> x.typeName == "list" && res.typeName == "int" },
+            /* invariants = */ listOf { x, _ -> x.typeName == "list" },
             /* propertiesToDiscover = */ List(3) { index ->
                 { _, res -> res.repr == (index + 1).toString() }
             }

diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
@@ -27,7 +27,7 @@ import kotlin.random.Random
 class PyMachine(
     private val program: PyProgram,
     private val typeSystem: PythonTypeSystem,
-    private val pathSelectorType: PyPathSelectorType = PyPathSelectorType.DelayedForkByInstructionAndTypeRatingByHintsDfs,
+    private val pathSelectorType: PyPathSelectorType = PyPathSelectorType.DelayedForkByInstructionWeightedDfs,
     private val printErrorMsg: Boolean = false
 ): UMachine<PyState>() {
     private val ctx = PyContext(typeSystem)

diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt
@@ -18,11 +18,12 @@ import kotlin.random.Random
 private val logger = object : KLogging() {}.logger
 
 enum class PyPathSelectorType {
-    BaselineDfs,
-    BaselineWeightedByNumberOfVirtual,
-    TypeRatingByHintsDfs,
-    DelayedForkByInstructionDfs,
-    DelayedForkByInstructionAndTypeRatingByHintsDfs
+    BaselinePriorityDfs,
+    BaselineWeightedDfs,
+    BaselinePriorityWeightedByNumberOfVirtual,
+    BaselinePriorityPlusTypeRatingByHintsDfs,
+    DelayedForkByInstructionPriorityDfs,
+    DelayedForkByInstructionWeightedDfs
 }
 
 fun createPyPathSelector(
@@ -32,26 +33,41 @@ fun createPyPathSelector(
     newStateObserver: NewStateObserver
 ): PyVirtualPathSelector<*, *> =
     when (type) {
-        PyPathSelectorType.BaselineDfs ->
-            createBaselineDfsPyPathSelector(ctx, random, newStateObserver)
-        PyPathSelectorType.BaselineWeightedByNumberOfVirtual ->
+        PyPathSelectorType.BaselinePriorityDfs ->
+            createBaselinePriorityDfsPyPathSelector(ctx, random, newStateObserver)
+        PyPathSelectorType.BaselineWeightedDfs ->
+            createBaselineWeightedDfsPyPathSelector(ctx, random, newStateObserver)
+        PyPathSelectorType.BaselinePriorityWeightedByNumberOfVirtual ->
             createBaselineWeightedByNumberOfVirtualPyPathSelector(ctx, random, newStateObserver)
-        PyPathSelectorType.TypeRatingByHintsDfs ->
+        PyPathSelectorType.BaselinePriorityPlusTypeRatingByHintsDfs ->
             createTypeRatingByHintsDfsPyPathSelector(ctx, random, newStateObserver)
-        PyPathSelectorType.DelayedForkByInstructionDfs ->
-            createDelayedForkByInstructionDfsPyPathSelector(ctx, random, newStateObserver)
-        PyPathSelectorType.DelayedForkByInstructionAndTypeRatingByHintsDfs ->
-            createDelayedForkByInstructionAndTypeRatingByHintsDfsPyPathSelector(ctx, random, newStateObserver)
+        PyPathSelectorType.DelayedForkByInstructionPriorityDfs ->
+            createDelayedForkByInstructionPriorityDfsPyPathSelector(ctx, random, newStateObserver)
+        PyPathSelectorType.DelayedForkByInstructionWeightedDfs ->
+            createDelayedForkByInstructionWeightedDfsPyPathSelector(ctx, random, newStateObserver)
     }
 
-fun createBaselineDfsPyPathSelector(
+fun createBaselinePriorityDfsPyPathSelector(
     ctx: PyContext,
     random: Random,
     newStateObserver: NewStateObserver
 ): PyVirtualPathSelector<*, *> =
     PyVirtualPathSelector(
         ctx,
-        makeBaselineActionStrategy(random),
+        makeBaselinePriorityActionStrategy(random),
+        BaselineDelayedForkStrategy(),
+        BaselineDFGraphCreation { DfsPathSelector() },
+        newStateObserver
+    )
+
+fun createBaselineWeightedDfsPyPathSelector(
+    ctx: PyContext,
+    random: Random,
+    newStateObserver: NewStateObserver
+): PyVirtualPathSelector<*, *> =
+    PyVirtualPathSelector(
+        ctx,
+        makeBaselineWeightedActionStrategy(random),
         BaselineDelayedForkStrategy(),
         BaselineDFGraphCreation { DfsPathSelector() },
         newStateObserver
@@ -64,7 +80,7 @@ fun createBaselineWeightedByNumberOfVirtualPyPathSelector(
 ): PyVirtualPathSelector<*, *> =
     PyVirtualPathSelector(
         ctx,
-        makeBaselineActionStrategy(random),
+        makeBaselinePriorityActionStrategy(random),
         BaselineDelayedForkStrategy(),
         BaselineDFGraphCreation {
             WeightedPathSelector(
@@ -88,41 +104,41 @@ fun createBaselineWeightedByNumberOfVirtualPyPathSelector(
         newStateObserver
     )
 
-fun createDelayedForkByInstructionDfsPyPathSelector(
+fun createDelayedForkByInstructionPriorityDfsPyPathSelector(
     ctx: PyContext,
     random: Random,
     newStateObserver: NewStateObserver
 ): PyVirtualPathSelector<*, *> =
     PyVirtualPathSelector(
         ctx,
-        makeDelayedForkByInstructionActionStrategy(random),
+        makeDelayedForkByInstructionPriorityStrategy(random),
         BaselineDelayedForkStrategy(),
         DelayedForkByInstructionGraphCreation { DfsPathSelector() },
         newStateObserver
     )
 
-fun createTypeRatingByHintsDfsPyPathSelector(
+fun createDelayedForkByInstructionWeightedDfsPyPathSelector(
     ctx: PyContext,
     random: Random,
     newStateObserver: NewStateObserver
 ): PyVirtualPathSelector<*, *> =
     PyVirtualPathSelector(
         ctx,
-        makeBaselineActionStrategy(random),
-        TypeRatingByNumberOfHints(),
-        BaselineDFGraphCreation { DfsPathSelector() },
+        makeDelayedForkByInstructionWeightedStrategy(random),
+        BaselineDelayedForkStrategy(),
+        DelayedForkByInstructionGraphCreation { DfsPathSelector() },
         newStateObserver
     )
 
-fun createDelayedForkByInstructionAndTypeRatingByHintsDfsPyPathSelector(
+fun createTypeRatingByHintsDfsPyPathSelector(
     ctx: PyContext,
     random: Random,
     newStateObserver: NewStateObserver
 ): PyVirtualPathSelector<*, *> =
     PyVirtualPathSelector(
         ctx,
-        makeDelayedForkByInstructionActionStrategy(random),
+        makeBaselinePriorityActionStrategy(random),
         TypeRatingByNumberOfHints(),
-        DelayedForkByInstructionGraphCreation { DfsPathSelector() },
+        BaselineDFGraphCreation { DfsPathSelector() },
         newStateObserver
     )
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/Action.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/Action.kt
@@ -0,0 +1,12 @@
+package org.usvm.machine.ps.strategies.impls
+
+import org.usvm.machine.ps.strategies.DelayedForkGraph
+import org.usvm.machine.ps.strategies.DelayedForkState
+import org.usvm.machine.ps.strategies.PyPathSelectorAction
+import kotlin.random.Random
+
+
+abstract class Action<DFState: DelayedForkState, in DFGraph: DelayedForkGraph<DFState>> {
+    abstract fun isAvailable(graph: DFGraph): Boolean
+    abstract fun makeAction(graph: DFGraph, random: Random): PyPathSelectorAction<DFState>
+}
diff --git a/...usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt b/...usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt
@@ -7,23 +7,40 @@ import org.usvm.machine.PyState
 import org.usvm.machine.ps.strategies.*
 import kotlin.random.Random
 
-fun makeBaselineActionStrategy(
+val baselineProbabilities = listOf(1.0, 0.6, 0.9, 0.7, 1.0)
+val baselineWeights = listOf(100.0, 0.6, 0.3, 0.088, 0.012)
+
+fun makeBaselinePriorityActionStrategy(
+    random: Random
+): RandomizedPriorityActionStrategy<DelayedForkState, BaselineDelayedForkGraph> =
+    RandomizedPriorityActionStrategy(
+        random,
+        listOf(
+            PeekExecutedStateWithConcreteType,
+            PeekFromRoot,
+            ServeNewDelayedFork,
+            PeekFromStateWithDelayedFork,
+            ServeOldDelayedFork
+        ),
+        baselineProbabilities
+    )
+
+fun makeBaselineWeightedActionStrategy(
     random: Random
 ): WeightedActionStrategy<DelayedForkState, BaselineDelayedForkGraph> =
     WeightedActionStrategy(
         random,
         listOf(
+            PeekExecutedStateWithConcreteType,
             PeekFromRoot,
             ServeNewDelayedFork,
             PeekFromStateWithDelayedFork,
-            ServeOldDelayedFork,
-            PeekExecutedStateWithConcreteType
-        )
+            ServeOldDelayedFork
+        ),
+        baselineWeights
     )
 
-sealed class BaselineAction(
-    weight: Double
-): Action<DelayedForkState, BaselineDelayedForkGraph>(weight) {
+sealed class BaselineAction: Action<DelayedForkState, BaselineDelayedForkGraph>() {
     protected fun chooseAvailableVertex(
         available: List<DelayedForkGraphInnerVertex<DelayedForkState>>,
         random: Random
@@ -34,7 +51,19 @@ sealed class BaselineAction(
     }
 }
 
-object PeekFromRoot: BaselineAction(0.6) {
+object PeekExecutedStateWithConcreteType: BaselineAction() {
+    override fun isAvailable(graph: BaselineDelayedForkGraph): Boolean =
+        !graph.pathSelectorForExecutedStatesWithConcreteTypes.isEmpty()
+
+    override fun makeAction(
+        graph: BaselineDelayedForkGraph,
+        random: Random
+    ): PyPathSelectorAction<DelayedForkState> =
+        Peek(graph.pathSelectorForExecutedStatesWithConcreteTypes)
+
+}
+
+object PeekFromRoot: BaselineAction() {
     override fun isAvailable(graph: BaselineDelayedForkGraph): Boolean =
         !graph.pathSelectorWithoutDelayedForks.isEmpty()
 
@@ -44,7 +73,7 @@ object PeekFromRoot: BaselineAction(0.6) {
     override fun toString(): String = "PeekFromRoot"
 }
 
-object ServeNewDelayedFork: BaselineAction(0.3) {
+object ServeNewDelayedFork: BaselineAction() {
     private val predicate = { node: DelayedForkGraphInnerVertex<DelayedForkState> ->
         node.delayedForkState.successfulTypes.isEmpty() && node.delayedForkState.size > 0
     }
@@ -60,7 +89,7 @@ object ServeNewDelayedFork: BaselineAction(0.3) {
     override fun toString(): String = "ServeNewDelayedFork"
 }
 
-object PeekFromStateWithDelayedFork: BaselineAction(0.088) {
+object PeekFromStateWithDelayedFork: BaselineAction() {
     override fun isAvailable(graph: BaselineDelayedForkGraph): Boolean =
         !graph.pathSelectorWithDelayedForks.isEmpty()
 
@@ -71,7 +100,7 @@ object PeekFromStateWithDelayedFork: BaselineAction(0.088) {
     override fun toString(): String = "PeekFromStateWithDelayedFork"
 }
 
-object ServeOldDelayedFork: BaselineAction(0.012) {
+object ServeOldDelayedFork: BaselineAction() {
     private val predicate = { node: DelayedForkGraphInnerVertex<DelayedForkState> ->
         node.delayedForkState.successfulTypes.isNotEmpty() && node.delayedForkState.size > 0
     }
@@ -87,18 +116,6 @@ object ServeOldDelayedFork: BaselineAction(0.012) {
     override fun toString(): String = "ServeOldDelayedFork"
 }
 
-object PeekExecutedStateWithConcreteType: BaselineAction(100.0) {
-    override fun isAvailable(graph: BaselineDelayedForkGraph): Boolean =
-        !graph.pathSelectorForExecutedStatesWithConcreteTypes.isEmpty()
-
-    override fun makeAction(
-        graph: BaselineDelayedForkGraph,
-        random: Random
-    ): PyPathSelectorAction<DelayedForkState> =
-        Peek(graph.pathSelectorForExecutedStatesWithConcreteTypes)
-
-}
-
 class BaselineDelayedForkStrategy: DelayedForkStrategy<DelayedForkState> {
     private var lastIdx = -1
     override fun chooseTypeRating(state: DelayedForkState): TypeRating {

diff --git a/...hon-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/DelayedForkByInstruction.kt b/...hon-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/DelayedForkByInstruction.kt
@@ -7,23 +7,37 @@ import org.usvm.machine.PyState
 import org.usvm.machine.ps.strategies.*
 import kotlin.random.Random
 
-fun makeDelayedForkByInstructionActionStrategy(
+fun makeDelayedForkByInstructionPriorityStrategy(
+    random: Random
+): RandomizedPriorityActionStrategy<DelayedForkState, DelayedForkByInstructionGraph> =
+    RandomizedPriorityActionStrategy(
+        random,
+        listOf(
+            PeekExecutedStateWithConcreteType,
+            PeekFromRoot,
+            ServeNewDelayedForkByInstruction,
+            PeekFromStateWithDelayedFork,
+            ServeOldDelayedForkByInstruction
+        ),
+        baselineProbabilities
+    )
+
+fun makeDelayedForkByInstructionWeightedStrategy(
     random: Random
 ): WeightedActionStrategy<DelayedForkState, DelayedForkByInstructionGraph> =
     WeightedActionStrategy(
         random,
         listOf(
+            PeekExecutedStateWithConcreteType,
             PeekFromRoot,
             ServeNewDelayedForkByInstruction,
             PeekFromStateWithDelayedFork,
-            ServeOldDelayedForkByInstruction,
-            PeekExecutedStateWithConcreteType
-        )
+            ServeOldDelayedForkByInstruction
+        ),
+        baselineWeights
     )
 
-sealed class DelayedForkByInstructionAction(
-    weight: Double
-): Action<DelayedForkState, DelayedForkByInstructionGraph>(weight) {
+sealed class DelayedForkByInstructionAction: Action<DelayedForkState, DelayedForkByInstructionGraph>() {
     protected fun findAvailableInstructions(
         graph: DelayedForkByInstructionGraph,
         isAvailable: (DelayedForkGraphInnerVertex<DelayedForkState>) -> Boolean,
@@ -50,7 +64,7 @@ sealed class DelayedForkByInstructionAction(
     }
 }
 
-object ServeNewDelayedForkByInstruction: DelayedForkByInstructionAction(ServeNewDelayedFork.weight) {
+object ServeNewDelayedForkByInstruction: DelayedForkByInstructionAction() {
     private val predicate = { node: DelayedForkGraphInnerVertex<DelayedForkState> ->
         node.delayedForkState.successfulTypes.isEmpty() && node.delayedForkState.size > 0
     }
@@ -67,7 +81,7 @@ object ServeNewDelayedForkByInstruction: DelayedForkByInstructionAction(ServeNew
     override fun toString(): String = "ServeNewDelayedForkByInstruction"
 }
 
-object ServeOldDelayedForkByInstruction: DelayedForkByInstructionAction(ServeOldDelayedFork.weight) {
+object ServeOldDelayedForkByInstruction: DelayedForkByInstructionAction() {
     private val predicate = { node: DelayedForkGraphInnerVertex<DelayedForkState> ->
         node.delayedForkState.successfulTypes.isNotEmpty() && node.delayedForkState.size > 0
     }