From 37050f9502fdbbf2f4de66b447086c0bc5a6a641 Mon Sep 17 00:00:00 2001 From: Mark Efremov <140056918+jefremof@users.noreply.github.com> Date: Fri, 16 Aug 2024 11:45:00 +0300 Subject: [PATCH] [python] First step in supporting type inference, based on the usage of `sq_concat` (#207) * Add sq_concat support * Add "list_concat_usage" test * Changed test to detect PyMockTypeStream issues * Add sq_concat notification * fix: more accurate nbAddKt function * fix linter --- .../c/org_usvm_interpreter_CPythonAdapter.c | 5 ++++ .../manual/program/PrimitivePrograms.kt | 14 +++++------ .../usvm/samples/SimpleTypeInferenceTest.kt | 14 +++++++++++ .../resources/samples/SimpleTypeInference.py | 6 +++++ .../org/usvm/interpreter/CPythonAdapter.java | 13 ++++++++++ .../kotlin/org/usvm/language/Callables.kt | 1 + .../concrete/ConcretePythonInterpreter.kt | 1 + .../operations/basic/MethodNotifications.kt | 24 ++++++++++++++++++- .../usvm/machine/ps/types/SymbolTypeTree.kt | 5 ++++ .../org/usvm/machine/types/VirtualTypes.kt | 5 ++++ 10 files changed, 79 insertions(+), 9 deletions(-) diff --git a/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c b/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c index b547607539..e1a4ef7ada 100644 --- a/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c +++ b/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c @@ -441,6 +441,11 @@ JNIEXPORT jint JNICALL Java_org_usvm_interpreter_CPythonAdapter_typeHasNbPositiv return type->tp_as_number && type->tp_as_number->nb_positive; } +JNIEXPORT jint JNICALL Java_org_usvm_interpreter_CPythonAdapter_typeHasSqConcat(JNIEnv *env, jobject _, jlong type_ref) { + QUERY_TYPE_HAS_PREFIX + return type->tp_as_sequence && type->tp_as_sequence->sq_concat; +} + JNIEXPORT jint JNICALL Java_org_usvm_interpreter_CPythonAdapter_typeHasSqLength(JNIEnv *env, jobject _, jlong type_ref) { QUERY_TYPE_HAS_PREFIX return type->tp_as_sequence && type->tp_as_sequence->sq_length; diff --git a/usvm-python/src/test/kotlin/org/usvm/runner/manual/program/PrimitivePrograms.kt b/usvm-python/src/test/kotlin/org/usvm/runner/manual/program/PrimitivePrograms.kt index a541ef5aac..024faabe89 100644 --- a/usvm-python/src/test/kotlin/org/usvm/runner/manual/program/PrimitivePrograms.kt +++ b/usvm-python/src/test/kotlin/org/usvm/runner/manual/program/PrimitivePrograms.kt @@ -16,13 +16,11 @@ val sampleStringFunction = StringProgramProvider( /** * Sample of a function that cannot be covered right now. * */ -val listConcatProgram = StringProgramProvider( +val tupleConcatProgram = StringProgramProvider( """ - def list_concat(x): - y = x + [1] - if len(y[::-1]) == 5: - return 1 - return 2 + def tuple_concat(x, y): + z = x + y + return z + (1, 2, 3) """.trimIndent(), - "list_concat", -) { listOf(PythonAnyType) } + "tuple_concat", +) { listOf(PythonAnyType, PythonAnyType) } diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt index 88f1975fb5..540620f061 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt @@ -93,6 +93,20 @@ class SimpleTypeInferenceTest: PythonTestRunnerForPrimitiveProgram("SimpleTypeIn ) } + @Test + fun testListConcatUsage() { + check2WithConcreteRun( + constructFunction("list_concat_usage", List(2) { PythonAnyType }), + ignoreNumberOfAnalysisResults, + standardConcolicAndConcreteChecks, + /* invariants = */ emptyList(), + /* propertiesToDiscover = */ listOf( + { _, _, res -> res.selfTypeName == "AssertionError" }, + { _, _, res -> res.repr == "None" } + ) + ) + } + @Test fun testLenUsage() { check1WithConcreteRun( diff --git a/usvm-python/src/test/resources/samples/SimpleTypeInference.py b/usvm-python/src/test/resources/samples/SimpleTypeInference.py index 95c402f88b..ee1adc4407 100644 --- a/usvm-python/src/test/resources/samples/SimpleTypeInference.py +++ b/usvm-python/src/test/resources/samples/SimpleTypeInference.py @@ -50,6 +50,12 @@ def isinstance_sample(x): return "Not reachable" +def list_concat_usage(x, y): + z = x + y + z += [] + assert z + + def len_usage(x): if len(x) == 5: return 1 diff --git a/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java b/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java index 83dd4e7e79..867e2e4736 100644 --- a/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java +++ b/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java @@ -89,6 +89,7 @@ public class CPythonAdapter { public native int typeHasNbMatrixMultiply(long type); public native int typeHasNbNegative(long type); public native int typeHasNbPositive(long type); + public native int typeHasSqConcat(long type); public native int typeHasSqLength(long type); public native int typeHasMpLength(long type); public native int typeHasMpSubscript(long type); @@ -1071,6 +1072,18 @@ public static void notifyNbPositive(ConcolicRunContext context, SymbolForCPython nbPositiveKt(context, on.obj); } + @CPythonAdapterJavaMethod(cName = "sq_concat") + @CPythonFunction( + argCTypes = {CType.PyObject, CType.PyObject}, + argConverters = {ObjectConverter.StandardConverter, ObjectConverter.StandardConverter} + ) + public static void notifySqConcat(ConcolicRunContext context, SymbolForCPython left, SymbolForCPython right) { + if (left.obj == null || right.obj == null) + return; + context.curOperation = new MockHeader(SqConcatMethod.INSTANCE, Arrays.asList(left.obj, right.obj), null); + sqConcatKt(context, left.obj, right.obj); + } + @CPythonAdapterJavaMethod(cName = "sq_length") @CPythonFunction( argCTypes = {CType.PyObject}, diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/Callables.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/Callables.kt index de2f3aed0d..48feed0c13 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/Callables.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/language/Callables.kt @@ -59,6 +59,7 @@ data object NbMultiplyMethod : TypeMethod(false) data object NbMatrixMultiplyMethod : TypeMethod(false) data object NbNegativeMethod : TypeMethod(false) data object NbPositiveMethod : TypeMethod(false) +data object SqConcatMethod : TypeMethod(false) data object SqLengthMethod : TypeMethod(true) data object MpSubscriptMethod : TypeMethod(false) data object MpAssSubscriptMethod : TypeMethod(false) diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt index 06ba3885de..c4a22560f3 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt @@ -242,6 +242,7 @@ object ConcretePythonInterpreter { val typeHasNbMatrixMultiply = createTypeQuery { pythonAdapter.typeHasNbMatrixMultiply(it) } val typeHasNbNegative = createTypeQuery { pythonAdapter.typeHasNbNegative(it) } val typeHasNbPositive = createTypeQuery { pythonAdapter.typeHasNbPositive(it) } + val typeHasSqConcat = createTypeQuery { pythonAdapter.typeHasSqConcat(it) } val typeHasSqLength = createTypeQuery { pythonAdapter.typeHasSqLength(it) } val typeHasMpLength = createTypeQuery { pythonAdapter.typeHasMpLength(it) } val typeHasMpSubscript = createTypeQuery { pythonAdapter.typeHasMpSubscript(it) } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt index 0e4704799a..2b0d2cf44c 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt @@ -15,6 +15,7 @@ import org.usvm.machine.types.HasNbMultiply import org.usvm.machine.types.HasNbNegative import org.usvm.machine.types.HasNbPositive import org.usvm.machine.types.HasNbSubtract +import org.usvm.machine.types.HasSqConcat import org.usvm.machine.types.HasSqLength import org.usvm.machine.types.HasTpCall import org.usvm.machine.types.HasTpGetattro @@ -37,7 +38,17 @@ fun nbAddKt( context.ctx ) { context.curState ?: return - pyAssert(context, left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd)) + /* + * The __add__ method corresponds both to the nb_add and sq_concat slots, + * so it is crucial not to assert the presence of nb_add, but to fork on these + * two possible options. + * Moreover, for now it was decided, that operation `sq_concat` makes sense + * only in the situation, when both operands have the corresponding slot. + */ + val nbAdd = left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd) + val sqConcat = left.evalIsSoft(context, HasSqConcat) and right.evalIsSoft(context, HasSqConcat) + pyAssert(context, nbAdd.not() implies sqConcat) + pyFork(context, nbAdd) } fun nbSubtractKt( @@ -74,6 +85,17 @@ fun nbPositiveKt(context: ConcolicRunContext, on: UninterpretedSymbolicPythonObj pyAssert(context, on.evalIsSoft(context, HasNbPositive)) } +fun sqConcatKt( + context: ConcolicRunContext, + left: UninterpretedSymbolicPythonObject, + right: UninterpretedSymbolicPythonObject, +) = with( + context.ctx +) { + context.curState ?: return + pyAssert(context, left.evalIsSoft(context, HasSqConcat) and right.evalIsSoft(context, HasSqConcat)) +} + fun sqLengthKt(context: ConcolicRunContext, on: UninterpretedSymbolicPythonObject) { context.curState ?: return val sqLength = on.evalIsSoft(context, HasSqLength) diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/types/SymbolTypeTree.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/types/SymbolTypeTree.kt index 346348d948..26598ca94b 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/types/SymbolTypeTree.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/types/SymbolTypeTree.kt @@ -10,6 +10,7 @@ import org.usvm.language.NbMultiplyMethod import org.usvm.language.NbNegativeMethod import org.usvm.language.NbPositiveMethod import org.usvm.language.NbSubtractMethod +import org.usvm.language.SqConcatMethod import org.usvm.language.SqLengthMethod import org.usvm.language.TpCallMethod import org.usvm.language.TpGetattro @@ -95,6 +96,10 @@ class SymbolTypeTree( listOf(createBinaryProtocol("__mul__", pythonAnyType, returnType)) } + SqConcatMethod -> { returnType: UtType -> + listOf(createBinaryProtocol("__add__", pythonAnyType, returnType)) + } + SqLengthMethod -> { _: UtType -> listOf(createUnaryProtocol("__len__", typeHintsStorage.pythonInt)) } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/types/VirtualTypes.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/types/VirtualTypes.kt index cf0301a36f..ed421de3e9 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/types/VirtualTypes.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/types/VirtualTypes.kt @@ -98,6 +98,11 @@ object HasNbPositive : TypeProtocol() { ConcretePythonInterpreter.typeHasNbPositive(type.asObject) } +object HasSqConcat : TypeProtocol() { + override fun acceptsConcrete(type: ConcretePythonType): Boolean = + ConcretePythonInterpreter.typeHasSqConcat(type.asObject) +} + object HasSqLength : TypeProtocol() { override fun acceptsConcrete(type: ConcretePythonType): Boolean = ConcretePythonInterpreter.typeHasSqLength(type.asObject)