Skip to content

Commit

Permalink
fix: auto-formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
sergeypospelov committed Mar 14, 2024
1 parent f43a027 commit 15bdd1f
Show file tree
Hide file tree
Showing 151 changed files with 2,035 additions and 1,207 deletions.
1 change: 0 additions & 1 deletion usvm-python/cpythonadapter/build.gradle.kts
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
import org.apache.tools.ant.taskdefs.condition.Os
import org.gradle.internal.jvm.Jvm
import java.io.*

// Example project: https://github.com/vladsoroka/GradleJniSample

Expand Down
55 changes: 35 additions & 20 deletions usvm-python/src/test/kotlin/manualTest.kt
Original file line number Diff line number Diff line change
@@ -1,27 +1,34 @@
import org.usvm.UMachineOptions
import org.usvm.language.PrimitivePyProgram
import org.usvm.language.PyProgram
import org.usvm.machine.*
import org.usvm.language.PyUnpinnedCallable
import org.usvm.language.StructuredPyProgram
import org.usvm.machine.PyMachine
import org.usvm.machine.interpreters.concrete.ConcretePythonInterpreter
import org.usvm.machine.interpreters.concrete.IllegalOperationException
import org.usvm.machine.results.DefaultPyMachineResultsReceiver
import org.usvm.machine.results.serialization.ObjectWithDictSerializer
import org.usvm.machine.types.*
import org.usvm.machine.types.BasicPythonTypeSystem
import org.usvm.machine.types.PythonAnyType
import org.usvm.machine.types.PythonTypeSystem
import org.usvm.machine.types.PythonTypeSystemWithMypyInfo
import org.usvm.machine.types.getTypeFromTypeHint
import org.usvm.machine.utils.withAdditionalPaths
import org.usvm.python.model.PyResultFailure
import org.usvm.python.model.PyResultSuccess
import org.usvm.runner.CustomPythonTestRunner
import org.usvm.runner.SamplesBuild
import org.usvm.utils.getModulesFromFiles
import org.usvm.utils.getPythonFilesFromRoot
import org.usvm.machine.utils.withAdditionalPaths
import org.usvm.python.model.PyResultFailure
import org.usvm.python.model.PyResultSuccess
import org.utpython.types.*
import org.utpython.types.PythonCallableTypeDescription
import org.utpython.types.PythonConcreteCompositeTypeDescription
import org.utpython.types.general.FunctionType
import org.utpython.types.general.UtType
import org.utpython.types.mypy.MypyBuildDirectory
import org.utpython.types.mypy.buildMypyInfo
import org.utpython.types.mypy.readMypyInfoBuild
import org.utpython.types.pythonDescription
import org.utpython.types.pythonTypeRepresentation
import java.io.File
import kotlin.time.Duration.Companion.seconds

Expand Down Expand Up @@ -72,20 +79,25 @@ private fun getFunctionInfo(
name: String,
module: String,
typeSystem: PythonTypeSystemWithMypyInfo,
program: StructuredPyProgram
program: StructuredPyProgram,
): PyUnpinnedCallable? {
//println("Module: $module, name: $name")
// println("Module: $module, name: $name")
val description = type.pythonDescription()
if (description !is PythonCallableTypeDescription)
if (description !is PythonCallableTypeDescription) {
return null
if (ignoreFunctions.contains(name))
}
if (ignoreFunctions.contains(name)) {
return null
//if (module != "requests.cookies")
}
// if (module != "requests.cookies")
// return null
//if (name != "remove_cookie_by_name")
// if (name != "remove_cookie_by_name")
// return null
if (description.argumentKinds.any { it == PythonCallableTypeDescription.ArgKind.ARG_STAR || it == PythonCallableTypeDescription.ArgKind.ARG_STAR_2 })
if (description.argumentKinds.any {
it == PythonCallableTypeDescription.ArgKind.ARG_STAR || it == PythonCallableTypeDescription.ArgKind.ARG_STAR_2
}) {
return null
}
runCatching {
withAdditionalPaths(program.roots, typeSystem) {
val namespace = program.getNamespaceOfModule(module)!!
Expand Down Expand Up @@ -132,16 +144,17 @@ private fun buildProjectRunConfig(): RunConfig {
val program = StructuredPyProgram(setOf(File(projectPath)))
val typeSystem = PythonTypeSystemWithMypyInfo(mypyBuild, program)
val functions = modules.flatMap { module ->
//println("Module: $module")
if (module in ignoreModules)
// println("Module: $module")
if (module in ignoreModules) {
return@flatMap emptyList()
}
runCatching {
withAdditionalPaths(program.roots, typeSystem) {
program.getNamespaceOfModule(module)
}
}.getOrNull() ?: return@flatMap emptyList() // skip bad modules
}.getOrNull() ?: return@flatMap emptyList() // skip bad modules
mypyBuild.definitions[module]!!.flatMap { (defName, def) ->
//println("Def name: $defName")
// println("Def name: $defName")
val type = def.getUtBotType()
val description = type.pythonDescription()
if (defName.startsWith("__")) {
Expand Down Expand Up @@ -223,7 +236,9 @@ private fun analyze(runConfig: RunConfig) {
if (machine.statistics.functionStatistics.last().coverage == 0.0) {
emptyCoverage.add(f.tag)
}
println("Finished analysing ${f.tag} in ${System.currentTimeMillis() - start} milliseconds. Made $iterations iterations.")
println(
"Finished analysing ${f.tag} in ${System.currentTimeMillis() - start} milliseconds. Made $iterations iterations."
)
println("FUNCTION STATISTICS")
println(machine.statistics.functionStatistics.last().writeReport())
println()
Expand All @@ -242,7 +257,7 @@ private fun analyze(runConfig: RunConfig) {
private data class RunConfig(
val program: PyProgram,
val typeSystem: PythonTypeSystem,
val functions: List<PyUnpinnedCallable>
val functions: List<PyUnpinnedCallable>,
)

@Suppress("SameParameterValue")
Expand All @@ -264,4 +279,4 @@ private fun constructStructuredProgram(): Pair<PyProgram, PythonTypeSystem> {
val program = SamplesBuild.program
val typeSystem = PythonTypeSystemWithMypyInfo(SamplesBuild.mypyBuild, program)
return Pair(program, typeSystem)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@ fun main(args: Array<String>) {
val files = getPythonFilesFromRoot(inputPath)
val modules = getModulesFromFiles(inputPath, files)
buildMypyInfo(pythonPath, files.map { it.canonicalPath }, modules, mypyBuildDir)
}
}
152 changes: 92 additions & 60 deletions usvm-python/src/test/kotlin/org/usvm/runner/PythonTestRunner.kt
Original file line number Diff line number Diff line change
@@ -1,16 +1,21 @@
package org.usvm.runner

import org.usvm.UMachineOptions
import org.usvm.machine.*
import org.usvm.language.*
import org.usvm.language.PyProgram
import org.usvm.language.PyUnpinnedCallable
import org.usvm.machine.PyMachine
import org.usvm.machine.interpreters.concrete.CPythonExecutionException
import org.usvm.machine.interpreters.concrete.ConcretePythonInterpreter
import org.usvm.machine.interpreters.concrete.PyObject
import org.usvm.machine.symbolicobjects.rendering.PyObjectRenderer
import org.usvm.machine.results.*
import org.usvm.machine.results.DefaultPyMachineResultsReceiver
import org.usvm.machine.results.serialization.PythonObjectInfo
import org.usvm.machine.results.serialization.StandardPythonObjectSerializer
import org.usvm.machine.types.*
import org.usvm.machine.symbolicobjects.rendering.PyObjectRenderer
import org.usvm.machine.types.BasicPythonTypeSystem
import org.usvm.machine.types.PythonAnyType
import org.usvm.machine.types.PythonType
import org.usvm.machine.types.PythonTypeSystem
import org.usvm.machine.types.PythonTypeSystemWithMypyInfo
import org.usvm.python.model.PyResultFailure
import org.usvm.python.model.PyResultSuccess
import org.usvm.python.model.PyTest
Expand All @@ -20,8 +25,8 @@ import org.usvm.test.util.checkers.ge

sealed class PythonTestRunner(
override var options: UMachineOptions = UMachineOptions(),
protected var allowPathDiversions: Boolean = false
): TestRunner<PyTest<PythonObjectInfo>, PyUnpinnedCallable, PythonType, PythonCoverage>() {
protected var allowPathDiversions: Boolean = false,
) : TestRunner<PyTest<PythonObjectInfo>, PyUnpinnedCallable, PythonType, PythonCoverage>() {
var timeoutPerRunMs: Long? = null
abstract val typeSystem: PythonTypeSystem
protected abstract val program: PyProgram
Expand Down Expand Up @@ -51,7 +56,7 @@ sealed class PythonTestRunner(
private fun compareWithConcreteRun(
target: PyUnpinnedCallable,
test: PyTest<PythonObjectInfo>,
check: (PyObject) -> String?
check: (PyObject) -> String?,
): String? =
program.withPinnedCallable(target, typeSystem) { pinnedCallable ->
val argModels = test.inputModel.inputArgs
Expand All @@ -68,12 +73,19 @@ sealed class PythonTestRunner(
}

private inline fun <reified FUNCTION_TYPE : Function<Boolean>> createCheckWithConcreteRun(concreteRun: Boolean = true):
(PyUnpinnedCallable, AnalysisResultsNumberMatcher, (PyTest<PythonObjectInfo>, PyObject) -> String?, List<FUNCTION_TYPE>, List<FUNCTION_TYPE>) -> Unit =
(
PyUnpinnedCallable,
AnalysisResultsNumberMatcher,
(PyTest<PythonObjectInfo>, PyObject) -> String?,
List<FUNCTION_TYPE>,
List<FUNCTION_TYPE>,
) -> Unit =
{ target: PyUnpinnedCallable,
analysisResultsNumberMatcher: AnalysisResultsNumberMatcher,
compareConcolicAndConcrete: (PyTest<PythonObjectInfo>, PyObject) -> String?,
invariants: List<FUNCTION_TYPE>,
propertiesToDiscover: List<FUNCTION_TYPE> ->
analysisResultsNumberMatcher: AnalysisResultsNumberMatcher,
compareConcolicAndConcrete: (PyTest<PythonObjectInfo>, PyObject) -> String?,
invariants: List<FUNCTION_TYPE>,
propertiesToDiscover: List<FUNCTION_TYPE>,
->
val onAnalysisResult = { pythonTest: PyTest<PythonObjectInfo> ->
val executionResult = when (val result = pythonTest.result) {
is PyResultSuccess -> result.output
Expand All @@ -86,8 +98,8 @@ sealed class PythonTestRunner(
}
require(comparisonResult == null) {
"Error in CPython patch or approximation: concrete and concolic results differ. " +
"Checker msg: $comparisonResult. " +
"Inputs: ${pythonTest.inputArgs.joinToString(", ")}"
"Checker msg: $comparisonResult. " +
"Inputs: ${pythonTest.inputArgs.joinToString(", ")}"
}
}
result
Expand All @@ -105,9 +117,10 @@ sealed class PythonTestRunner(
}

private inline fun <reified FUNCTION_TYPE : Function<Boolean>> createCheckWithConcreteRunAndNoPredicates():
(PyUnpinnedCallable, (PyTest<PythonObjectInfo>, PyObject) -> String?) -> Unit =
(PyUnpinnedCallable, (PyTest<PythonObjectInfo>, PyObject) -> String?) -> Unit =
{ target: PyUnpinnedCallable,
compareConcolicAndConcrete: (PyTest<PythonObjectInfo>, PyObject) -> String? ->
compareConcolicAndConcrete: (PyTest<PythonObjectInfo>, PyObject) -> String?,
->
createCheckWithConcreteRun<FUNCTION_TYPE>(concreteRun = true)(
target,
ge(0),
Expand All @@ -118,11 +131,12 @@ sealed class PythonTestRunner(
}

private inline fun <reified FUNCTION_TYPE : Function<Boolean>> createCheck():
(PyUnpinnedCallable, AnalysisResultsNumberMatcher, List<FUNCTION_TYPE>, List<FUNCTION_TYPE>) -> Unit =
(PyUnpinnedCallable, AnalysisResultsNumberMatcher, List<FUNCTION_TYPE>, List<FUNCTION_TYPE>) -> Unit =
{ target: PyUnpinnedCallable,
analysisResultsNumberMatcher: AnalysisResultsNumberMatcher,
invariants: List<FUNCTION_TYPE>,
propertiesToDiscover: List<FUNCTION_TYPE> ->
analysisResultsNumberMatcher: AnalysisResultsNumberMatcher,
invariants: List<FUNCTION_TYPE>,
propertiesToDiscover: List<FUNCTION_TYPE>,
->
createCheckWithConcreteRun<FUNCTION_TYPE>(concreteRun = false)(
target,
analysisResultsNumberMatcher,
Expand All @@ -148,55 +162,73 @@ sealed class PythonTestRunner(
createCheckWithConcreteRunAndNoPredicates<(PythonObjectInfo, PythonObjectInfo, PythonObjectInfo) -> Boolean>()

val check3WithConcreteRun =
createCheckWithConcreteRun<(PythonObjectInfo, PythonObjectInfo, PythonObjectInfo, PythonObjectInfo) -> Boolean>()
createCheckWithConcreteRun<(
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
) -> Boolean>()
val check3NoPredicates =
createCheckWithConcreteRunAndNoPredicates<(PythonObjectInfo, PythonObjectInfo, PythonObjectInfo, PythonObjectInfo) -> Boolean>()
createCheckWithConcreteRunAndNoPredicates<(
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
) -> Boolean>()

val check4NoPredicates =
createCheckWithConcreteRunAndNoPredicates<(PythonObjectInfo, PythonObjectInfo, PythonObjectInfo, PythonObjectInfo, PythonObjectInfo) -> Boolean>()
createCheckWithConcreteRunAndNoPredicates<(
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
PythonObjectInfo,
) -> Boolean>()

protected val compareConcolicAndConcreteReprsIfSuccess:
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultSuccess)?.let {
val concolic = it.output.repr
val concrete = ConcretePythonInterpreter.getPythonObjectRepr(concreteResult)
if (concolic == concrete) null else "(Success) Expected $concrete, got $concolic"
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultSuccess)?.let {
val concolic = it.output.repr
val concrete = ConcretePythonInterpreter.getPythonObjectRepr(concreteResult)
if (concolic == concrete) null else "(Success) Expected $concrete, got $concolic"
}
}
}

protected val compareConcolicAndConcreteTypesIfSuccess:
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultSuccess)?.let {
val concolic = it.output.typeName
val concrete = ConcretePythonInterpreter.getPythonObjectTypeName(concreteResult)
if (concolic == concrete) null else "(Success) Expected result type $concrete, got $concolic"
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultSuccess)?.let {
val concolic = it.output.typeName
val concrete = ConcretePythonInterpreter.getPythonObjectTypeName(concreteResult)
if (concolic == concrete) null else "(Success) Expected result type $concrete, got $concolic"
}
}
}

protected val compareConcolicAndConcreteTypesIfFail:
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultFailure)?.let {
if (ConcretePythonInterpreter.getPythonObjectTypeName(concreteResult) != "type")
"Fail in concolic (${it.exception.selfTypeName}), but success in concrete (${ConcretePythonInterpreter.getPythonObjectRepr(concreteResult)})"
else {
val concolic = it.exception.selfTypeName
val concrete = ConcretePythonInterpreter.getNameOfPythonType(concreteResult)
if (concolic == concrete) null else "(Fail) Expected $concrete, got $concolic"
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
(testFromConcolic.result as? PyResultFailure)?.let {
if (ConcretePythonInterpreter.getPythonObjectTypeName(concreteResult) != "type") {
"Fail in concolic (${it.exception.selfTypeName}), but success in concrete (${ConcretePythonInterpreter.getPythonObjectRepr(
concreteResult
)})"
} else {
val concolic = it.exception.selfTypeName
val concrete = ConcretePythonInterpreter.getNameOfPythonType(concreteResult)
if (concolic == concrete) null else "(Fail) Expected $concrete, got $concolic"
}
}
}
}

val standardConcolicAndConcreteChecks:
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
compareConcolicAndConcreteReprsIfSuccess(testFromConcolic, concreteResult) ?:
compareConcolicAndConcreteTypesIfFail(testFromConcolic, concreteResult)
}
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
compareConcolicAndConcreteReprsIfSuccess(testFromConcolic, concreteResult)
?: compareConcolicAndConcreteTypesIfFail(testFromConcolic, concreteResult)
}

val compareConcolicAndConcreteTypes:
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
compareConcolicAndConcreteTypesIfSuccess(testFromConcolic, concreteResult) ?:
compareConcolicAndConcreteTypesIfFail(testFromConcolic, concreteResult)
}
(PyTest<PythonObjectInfo>, PyObject) -> String? = { testFromConcolic, concreteResult ->
compareConcolicAndConcreteTypesIfSuccess(testFromConcolic, concreteResult)
?: compareConcolicAndConcreteTypesIfFail(testFromConcolic, concreteResult)
}

protected open fun constructFunction(name: String, signature: List<PythonType>): PyUnpinnedCallable =
PyUnpinnedCallable.constructCallableFromName(signature, name)
Expand All @@ -205,17 +237,17 @@ sealed class PythonTestRunner(
open class PythonTestRunnerForPrimitiveProgram(
module: String,
options: UMachineOptions = UMachineOptions(),
allowPathDiversions: Boolean = false
): PythonTestRunner(options, allowPathDiversions) {
allowPathDiversions: Boolean = false,
) : PythonTestRunner(options, allowPathDiversions) {
override val program = SamplesBuild.program.getPrimitiveProgram(module)
override val typeSystem = BasicPythonTypeSystem()
}

open class PythonTestRunnerForStructuredProgram(
private val module: String,
options: UMachineOptions = UMachineOptions(),
allowPathDiversions: Boolean = false
): PythonTestRunner(options, allowPathDiversions) {
allowPathDiversions: Boolean = false,
) : PythonTestRunner(options, allowPathDiversions) {
override val program = SamplesBuild.program
override val typeSystem = PythonTypeSystemWithMypyInfo(SamplesBuild.mypyBuild, SamplesBuild.program)
override fun constructFunction(name: String, signature: List<PythonType>): PyUnpinnedCallable =
Expand All @@ -226,7 +258,7 @@ class CustomPythonTestRunner(
override val program: PyProgram,
override val typeSystem: PythonTypeSystem,
options: UMachineOptions = UMachineOptions(),
allowPathDiversions: Boolean = false
): PythonTestRunner(options, allowPathDiversions)
allowPathDiversions: Boolean = false,
) : PythonTestRunner(options, allowPathDiversions)

data class PythonCoverage(val int: Int)
data class PythonCoverage(val int: Int)
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ object SamplesBuild {
private val mypyDirectory = MypyBuildDirectory(File(mypyBuildRoot), setOf(sourcesRoot))
val mypyBuild = readMypyInfoBuild(mypyDirectory)
val program = StructuredPyProgram(setOf(File(sourcesRoot)))
}
}
Loading

0 comments on commit 15bdd1f

Please sign in to comment.