diff --git a/settings.gradle.kts b/settings.gradle.kts index 5f14532fcf..d11ddb66d9 100644 --- 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" \ No newline at end of file +include("usvm-python:usvm-python-commons") +findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" \ No newline at end of file diff --git a/usvm-python/build.gradle.kts b/usvm-python/build.gradle.kts index 1ad9d52fb3..e7db484d65 100644 --- 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 index 73c434b993..c40f9c6aa5 100644 --- 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) { - 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) { val clsName = if (args[4] == "") 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] != "") { + val pathSelectorName = args[7] + val pathSelector = PyPathSelectorType.valueOf(pathSelectorName) + if (args[8] != "") { 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) { File(mypyDirPath), programRoots.map { File(it) }.toSet(), "localhost", - socketPort + socketPort, + pathSelector ) runner.use { if (clsName == null) { diff --git a/usvm-python/usvm-python-object-model/build.gradle.kts b/usvm-python/usvm-python-commons/build.gradle.kts similarity index 100% rename from usvm-python/usvm-python-object-model/build.gradle.kts rename to usvm-python/usvm-python-commons/build.gradle.kts diff --git a/usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyObjectModel.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyObjectModel.kt similarity index 100% rename from usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyObjectModel.kt rename to usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyObjectModel.kt diff --git a/usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyObjectModelVisitor.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyObjectModelVisitor.kt similarity index 100% rename from usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyObjectModelVisitor.kt rename to usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyObjectModelVisitor.kt diff --git a/usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyTest.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyTest.kt similarity index 100% rename from usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/PyTest.kt rename to usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/PyTest.kt diff --git a/usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/Utils.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/model/Utils.kt similarity index 100% rename from usvm-python/usvm-python-object-model/src/main/kotlin/org/usvm/python/model/Utils.kt rename to usvm-python/usvm-python-commons/src/main/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 new file mode 100644 index 0000000000..c22e635b69 --- /dev/null +++ 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 +} \ No newline at end of file diff --git a/usvm-python/usvm-python-main/build.gradle.kts b/usvm-python/usvm-python-main/build.gradle.kts index e8308e57ec..5104da3236 100644 --- 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 index dc3f3e9309..d97df5cbb4 100644 --- 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 index 6adcfd60ef..e74f196190 100644 --- 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 index c9ba995b77..6b5921848d 100644 --- 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, 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 index e9ece5e40f..c969a4e28f 100644 --- 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 index 5afb07749a..0d55425fe7 100644 --- 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,5 +1,6 @@ package org.usvm.runner +import org.usvm.python.ps.PyPathSelectorType import org.usvm.runner.venv.VenvConfig data class USVMPythonConfig( @@ -7,7 +8,8 @@ data class USVMPythonConfig( val javaCmd: String, val mypyBuildDir: String, val roots: Set, - 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 index 8a5f3f062c..78cdffc591 100644 --- 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 index 5f03a2b018..c023df50d7 100644 --- 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(