Add usvm check param

tamarinvs19 · tamarinvs19 · commit e343606d1406 · 2023-11-14T10:40:10.000+03:00
diff --git a/utbot-cli-python/src/main/kotlin/org/utbot/cli/language/python/sbft/SbftGenerateTestsCommand.kt b/utbot-cli-python/src/main/kotlin/org/utbot/cli/language/python/sbft/SbftGenerateTestsCommand.kt
@@ -105,6 +105,9 @@ class SbftGenerateTestsCommand : CliktCommand(
         help = "(required) Path to usvm directory (ONLY FOR USVM)."
     ).required()
 
+    private val checkUsvm by option("--check-usvm", help = "Check usvm (ONLY FOR USVM).")
+        .flag(default = false)
+
     private fun getPythonMethods(): List<List<PythonMethodHeader>> {
         val parsedModule = PythonParser(sourceFileContent).Module()
 
@@ -150,7 +153,7 @@ class SbftGenerateTestsCommand : CliktCommand(
             return
         }
 
-        val pythonMethodGroups = getPythonMethods()
+        val pythonMethodGroups = getPythonMethods().let { if (checkUsvm) it.take(1) else it }
 
         val globalImportCollection = mutableSetOf<PythonImport>()
         val globalCodeCollection = mutableListOf<String>()
@@ -172,6 +175,7 @@ class SbftGenerateTestsCommand : CliktCommand(
                 coverageOutputFormat = CoverageOutputFormat.Lines,
                 usvmConfig = UsvmConfig(javaCmd, usvmDirectory),
                 prohibitedExceptions = if (prohibitedExceptions == listOf("-")) emptyList() else prohibitedExceptions,
+                checkUsvm = checkUsvm,
             )
 
             val processor = SbftCliProcessor(config)
diff --git a/utbot-python/src/main/kotlin/org/utbot/python/PythonTestCaseGenerator.kt b/utbot-python/src/main/kotlin/org/utbot/python/PythonTestCaseGenerator.kt
@@ -18,7 +18,6 @@ class PythonTestCaseGenerator(
     private val withMinimization = configuration.withMinimization
 
     fun generate(method: PythonMethod, until: Long): List<PythonTestSet> {
-
         logger.info { "Start test generation for ${method.name}" }
         val engine = GlobalPythonEngine(
             method = method,
@@ -27,7 +26,11 @@ class PythonTestCaseGenerator(
             until,
         )
         try {
-            engine.run()
+            if (configuration.checkUsvm) {
+                engine.debugUsvmRun()
+            } else {
+                engine.run()
+            }
         } catch (_: OutOfMemoryError) {
             logger.debug { "Out of memory error. Stop test generation process" }
         }
diff --git a/utbot-python/src/main/kotlin/org/utbot/python/PythonTestGenerationConfig.kt b/utbot-python/src/main/kotlin/org/utbot/python/PythonTestGenerationConfig.kt
@@ -32,6 +32,7 @@ class PythonTestGenerationConfig(
     val coverageOutputFormat: CoverageOutputFormat = CoverageOutputFormat.Lines,
     val usvmConfig: UsvmConfig = UsvmConfig.defaultConfig,
     val prohibitedExceptions: List<String> = defaultProhibitedExceptions,
+    val checkUsvm: Boolean = false,
 ) {
     companion object {
         val defaultProhibitedExceptions = listOf(
diff --git a/utbot-python/src/main/kotlin/org/utbot/python/engine/GlobalPythonEngine.kt b/utbot-python/src/main/kotlin/org/utbot/python/engine/GlobalPythonEngine.kt
@@ -56,7 +56,7 @@ class GlobalPythonEngine(
         ).start()
     }
 
-    private fun runSymbolic() {
+    private fun runSymbolic(debug: Boolean = false) {
         val usvmPythonConfig = USVMPythonConfig(
             StandardLayout(File(configuration.usvmConfig.usvmDirectory)),
             configuration.usvmConfig.javaCmd,
@@ -79,13 +79,19 @@ class GlobalPythonEngine(
                 method.containingPythonClass.pythonName()
             )
         }
-        SymbolicEngine(
+        val engine = SymbolicEngine(
             usvmPythonConfig,
             configuration,
-        ).analyze(
-            USVMPythonRunConfig(config, configuration.timeout, configuration.timeoutForRun * 3),
-            receiver
         )
+        val usvmConfig = USVMPythonRunConfig(config, configuration.timeout, configuration.timeoutForRun * 3)
+        if (debug) {
+            engine.debugRun(usvmConfig)
+        } else {
+            engine.analyze(
+                usvmConfig,
+                receiver
+            )
+        }
         logger.info { "Symbolic: stop receiver" }
         receiver.close()
     }
@@ -113,6 +119,18 @@ class GlobalPythonEngine(
         symbolic.join()
     }
 
+    fun debugUsvmRun() {
+        val symbolic = thread(
+            start = true,
+            isDaemon = true,
+            name = "Symbolic"
+        ) {
+            logger.info { " ...... Checking symbolic ...... " }
+            runSymbolic(debug = true)
+        }
+        symbolic.join()
+    }
+
     private fun constructHintCollector(
         mypyStorage: MypyInfoBuild,
         typeStorage: PythonTypeHintsStorage,
diff --git a/utbot-python/src/main/kotlin/org/utbot/python/engine/symbolic/SymbolicEngine.kt b/utbot-python/src/main/kotlin/org/utbot/python/engine/symbolic/SymbolicEngine.kt
@@ -1,6 +1,7 @@
 package org.utbot.python.engine.symbolic
 
 import mu.KotlinLogging
+import org.usvm.runner.DebugRunner
 import org.usvm.runner.PythonSymbolicAnalysisRunnerImpl
 import org.usvm.runner.USVMPythonConfig
 import org.usvm.runner.USVMPythonRunConfig
@@ -43,4 +44,14 @@ class SymbolicEngine(
             it.analyze(runConfig, receiver, symbolicCancellation)
         }
     }
+
+    fun debugRun(runConfig: USVMPythonRunConfig) {
+        val debugRunner = DebugRunner(usvmPythonConfig)
+        try {
+            debugRunner.runProcessAndPrintInfo(runConfig)
+        } catch (ex: Exception) {
+            logger.error { ex.message }
+            logger.error { ex.stackTrace }
+        }
+    }
 }
