Added pathSelector parameter to usvm-python-runner

UnitTestBot · Feb 29, 2024 · 1b10351 · 1b10351
1 parent bf2826a
commit 1b10351
Show file tree

Hide file tree

Showing 17 changed files with 40 additions and 26 deletions.
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -25,5 +25,5 @@ include("usvm-python:usvm-python-main")
 findProject(":usvm-python:usvm-python-main")?.name = "usvm-python-main"
 include("usvm-python:usvm-python-runner")
 findProject(":usvm-python:usvm-python-runner")?.name = "usvm-python-runner"
-include("usvm-python:usvm-python-object-model")
-findProject(":usvm-python:usvm-python-object-model")?.name = "usvm-python-object-model"
+include("usvm-python:usvm-python-commons")
+findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
diff --git a/usvm-python/build.gradle.kts b/usvm-python/build.gradle.kts
@@ -8,7 +8,7 @@ plugins {
 dependencies {
     implementation(project(":usvm-core"))
     implementation(project(":usvm-python:usvm-python-main"))
-    implementation(project(":usvm-python:usvm-python-object-model"))
+    implementation(project(":usvm-python:usvm-python-commons"))
     implementation("com.github.UnitTestBot:PythonTypesAPI:${Versions.pythonTypesAPIHash}")
     implementation("ch.qos.logback:logback-classic:${Versions.logback}")
 }

diff --git a/usvm-python/src/main/kotlin/org/usvm/runner/UtBotPythonRunnerEntryPoint.kt b/usvm-python/src/main/kotlin/org/usvm/runner/UtBotPythonRunnerEntryPoint.kt
@@ -2,10 +2,11 @@ package org.usvm.runner
 
 import org.usvm.machine.interpreters.concrete.ConcretePythonInterpreter
 import org.usvm.machine.interpreters.concrete.venv.VenvConfig
+import org.usvm.python.ps.PyPathSelectorType
 import java.io.File
 
 fun main(args: Array<String>) {
-    var prefixNumberOfArgs = 8
+    var prefixNumberOfArgs = 9
     require(args.size >= prefixNumberOfArgs + 1) { "Incorrect number of arguments" }
     val mypyDirPath = args[0]
     val socketPort = args[1].toIntOrNull() ?: error("Second argument must be integer")
@@ -14,13 +15,15 @@ fun main(args: Array<String>) {
     val clsName = if (args[4] == "<no_class>") null else args[4]
     val timeoutPerRunMs = args[5].toLongOrNull() ?: error("Sixth argument must be integer")
     val timeoutMs = args[6].toLongOrNull() ?: error("Seventh argument must be integer")
-    if (args[7] != "<no_venv>") {
+    val pathSelectorName = args[7]
+    val pathSelector = PyPathSelectorType.valueOf(pathSelectorName)
+    if (args[8] != "<no_venv>") {
         prefixNumberOfArgs += 2
         require(args.size >= prefixNumberOfArgs + 1) { "Incorrect number of arguments" }
         val venvConfig = VenvConfig(
-            basePath = File(args[7]),
-            libPath = File(args[8]),
-            binPath = File(args[9])
+            basePath = File(args[8]),
+            libPath = File(args[9]),
+            binPath = File(args[10])
         )
         ConcretePythonInterpreter.setVenv(venvConfig)
         System.err.println("VenvConfig: $venvConfig")
@@ -32,7 +35,8 @@ fun main(args: Array<String>) {
         File(mypyDirPath),
         programRoots.map { File(it) }.toSet(),
         "localhost",
-        socketPort
+        socketPort,
+        pathSelector
     )
     runner.use {
         if (clsName == null) {

diff --git a/...usvm-python-object-model/build.gradle.kts → ...thon/usvm-python-commons/build.gradle.kts b/...usvm-python-object-model/build.gradle.kts → ...thon/usvm-python-commons/build.gradle.kts
diff --git a/...in/org/usvm/python/model/PyObjectModel.kt → ...in/org/usvm/python/model/PyObjectModel.kt b/...in/org/usvm/python/model/PyObjectModel.kt → ...in/org/usvm/python/model/PyObjectModel.kt
diff --git a/...usvm/python/model/PyObjectModelVisitor.kt → ...usvm/python/model/PyObjectModelVisitor.kt b/...usvm/python/model/PyObjectModelVisitor.kt → ...usvm/python/model/PyObjectModelVisitor.kt
diff --git a/...in/kotlin/org/usvm/python/model/PyTest.kt → ...in/kotlin/org/usvm/python/model/PyTest.kt b/...in/kotlin/org/usvm/python/model/PyTest.kt → ...in/kotlin/org/usvm/python/model/PyTest.kt
diff --git a/...ain/kotlin/org/usvm/python/model/Utils.kt → ...ain/kotlin/org/usvm/python/model/Utils.kt b/...ain/kotlin/org/usvm/python/model/Utils.kt → ...ain/kotlin/org/usvm/python/model/Utils.kt
diff --git a/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt
@@ -0,0 +1,12 @@
+package org.usvm.python.ps
+
+enum class PyPathSelectorType {
+    BaselinePriorityDfs,
+    BaselineWeightedDfs,
+    BaselinePriorityRandomTree,
+    BaselinePriorityWeightedByNumberOfVirtual,
+    BaselinePriorityPlusTypeRatingByHintsDfs,
+    DelayedForkByInstructionPriorityDfs,
+    DelayedForkByInstructionWeightedDfs,
+    DelayedForkByInstructionWeightedRandomTree
+}
diff --git a/usvm-python/usvm-python-main/build.gradle.kts b/usvm-python/usvm-python-main/build.gradle.kts
@@ -14,7 +14,7 @@ tasks.compileJava {
 dependencies {
     implementation(project(":usvm-core"))
     implementation(project(mapOf("path" to ":usvm-python:usvm-python-annotations")))
-    implementation(project(mapOf("path" to ":usvm-python:usvm-python-object-model")))
+    implementation(project(mapOf("path" to ":usvm-python:usvm-python-commons")))
     annotationProcessor(project(":usvm-python:usvm-python-annotations"))
 
     implementation("com.github.UnitTestBot:PythonTypesAPI:${Versions.pythonTypesAPIHash}")

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
@@ -9,7 +9,6 @@ import org.usvm.language.types.PythonTypeSystemWithMypyInfo
 import org.usvm.machine.interpreters.concrete.ConcretePythonInterpreter
 import org.usvm.machine.interpreters.symbolic.USVMPythonInterpreter
 import org.usvm.machine.model.toPyModel
-import org.usvm.machine.ps.PyPathSelectorType
 import org.usvm.machine.ps.createPyPathSelector
 import org.usvm.machine.results.PyMachineResultsReceiver
 import org.usvm.machine.results.observers.NewStateObserver
@@ -19,6 +18,7 @@ import org.usvm.machine.utils.PythonMachineStatisticsOnFunction
 import org.usvm.machine.utils.isGenerator
 import org.usvm.machine.utils.unfoldGenerator
 import org.usvm.memory.UMemory
+import org.usvm.python.ps.PyPathSelectorType
 import org.usvm.solver.USatResult
 import org.usvm.statistics.CompositeUMachineObserver
 import org.usvm.statistics.UMachineObserver

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
@@ -14,22 +14,12 @@ import org.usvm.ps.RandomTreePathSelector
 import org.usvm.ps.WeightedPathSelector
 import org.usvm.python.model.PyTupleObject
 import org.usvm.python.model.calculateNumberOfMocks
+import org.usvm.python.ps.PyPathSelectorType
 import kotlin.math.max
 import kotlin.random.Random
 
 private val logger = object : KLogging() {}.logger
 
-enum class PyPathSelectorType {
-    BaselinePriorityDfs,
-    BaselineWeightedDfs,
-    BaselinePriorityRandomTree,
-    BaselinePriorityWeightedByNumberOfVirtual,
-    BaselinePriorityPlusTypeRatingByHintsDfs,
-    DelayedForkByInstructionPriorityDfs,
-    DelayedForkByInstructionWeightedDfs,
-    DelayedForkByInstructionWeightedRandomTree
-}
-
 fun createPyPathSelector(
     initialState: PyState,
     type: PyPathSelectorType,

diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/runner/PyMachineSocketRunner.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/runner/PyMachineSocketRunner.kt
@@ -8,6 +8,7 @@ import org.usvm.machine.PyMachine
 import org.usvm.machine.results.PyMachineResultsReceiver
 import org.usvm.machine.results.observers.*
 import org.usvm.machine.results.serialization.EmptyObjectSerializer
+import org.usvm.python.ps.PyPathSelectorType
 import org.utpython.types.PythonCallableTypeDescription
 import org.utpython.types.PythonCompositeTypeDescription
 import org.utpython.types.general.FunctionType
@@ -21,14 +22,15 @@ class PyMachineSocketRunner(
     mypyDirPath: File,
     programRoots: Set<File>,
     socketIp: String,
-    socketPort: Int
+    socketPort: Int,
+    pathSelector: PyPathSelectorType
 ): AutoCloseable {
     private val mypyDir = MypyBuildDirectory(mypyDirPath, programRoots.map { it.canonicalPath }.toSet())
     private val mypyBuild = readMypyInfoBuild(mypyDir)
     private val communicator = PickledObjectCommunicator(socketIp, socketPort)
     private val program = StructuredPyProgram(programRoots)
     private val typeSystem = PythonTypeSystemWithMypyInfo(mypyBuild, program)
-    private val machine = PyMachine(program, typeSystem)
+    private val machine = PyMachine(program, typeSystem, pathSelectorType = pathSelector)
     override fun close() {
         communicator.close()
         machine.close()

diff --git a/usvm-python/usvm-python-runner/build.gradle.kts b/usvm-python/usvm-python-runner/build.gradle.kts
@@ -4,6 +4,7 @@ plugins {
 }
 
 dependencies {
+    implementation(project(mapOf("path" to ":usvm-python:usvm-python-commons")))
     api("io.github.microutils:kotlin-logging:${Versions.klogging}")
     testImplementation("ch.qos.logback:logback-classic:${Versions.logback}")
 }

diff --git a/usvm-python/usvm-python-runner/src/main/kotlin/org/usvm/runner/Config.kt b/usvm-python/usvm-python-runner/src/main/kotlin/org/usvm/runner/Config.kt
@@ -1,13 +1,15 @@
 package org.usvm.runner
 
+import org.usvm.python.ps.PyPathSelectorType
 import org.usvm.runner.venv.VenvConfig
 
 data class USVMPythonConfig(
     val distributionLayout: DistributionLayout,
     val javaCmd: String,
     val mypyBuildDir: String,
     val roots: Set<String>,
-    val venvConfig: VenvConfig?
+    val venvConfig: VenvConfig?,
+    val pathSelector: PyPathSelectorType
 )
 
 sealed class USVMPythonCallableConfig

diff --git a/usvm-python/usvm-python-runner/src/main/kotlin/org/usvm/runner/USVMPythonRunner.kt b/usvm-python/usvm-python-runner/src/main/kotlin/org/usvm/runner/USVMPythonRunner.kt
@@ -48,6 +48,7 @@ open class USVMPythonRunner(private val config: USVMPythonConfig): AutoCloseable
             *functionConfigArgs.toTypedArray(),
             runConfig.timeoutPerRunMs.toString(),
             runConfig.timeoutMs.toString(),
+            config.pathSelector.name,
             *venvArgs.toTypedArray(),
             *config.roots.toList().toTypedArray()
         )

diff --git a/usvm-python/usvm-python-runner/src/test/kotlin/org/usvm/runner/manualTest.kt b/usvm-python/usvm-python-runner/src/test/kotlin/org/usvm/runner/manualTest.kt
@@ -1,5 +1,6 @@
 package org.usvm.runner
 
+import org.usvm.python.ps.PyPathSelectorType
 import java.io.File
 
 fun main() {
@@ -14,7 +15,8 @@ fun main() {
         "java",
         mypyDir.canonicalPath,
         setOf(root.canonicalPath),
-        venvConfig
+        venvConfig,
+        PyPathSelectorType.BaselinePriorityDfs
     )
     val runConfig = USVMPythonRunConfig(
         USVMPythonFunctionConfig(