From ce900da976076a0a1cf2751dfaa75dcdc0bd1bea Mon Sep 17 00:00:00 2001 From: nostromo Date: Mon, 12 Aug 2024 16:14:55 +0300 Subject: [PATCH 1/6] Add sq_concat support --- .../src/main/c/org_usvm_interpreter_CPythonAdapter.c | 5 +++++ .../src/main/java/org/usvm/interpreter/CPythonAdapter.java | 1 + .../interpreters/concrete/ConcretePythonInterpreter.kt | 1 + .../symbolic/operations/basic/MethodNotifications.kt | 6 +++++- .../src/main/kotlin/org/usvm/machine/types/VirtualTypes.kt | 5 +++++ 5 files changed, 17 insertions(+), 1 deletion(-) 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/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..f3b34ec3c0 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); 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..2203441310 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,10 @@ fun nbAddKt( context.ctx ) { context.curState ?: return - pyAssert(context, left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd)) + val nbAdd = left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd) + val sqConcat = left.evalIsSoft(context, HasSqConcat) and right.evalIsSoft(context, HasSqConcat) + pyAssert(context, context.ctx.mkImplies(nbAdd.not(), sqConcat)) + pyFork(context, nbAdd) } fun nbSubtractKt( 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) From ed6a470f5e032e7460cca5be22d7843465bde97e Mon Sep 17 00:00:00 2001 From: nostromo Date: Mon, 12 Aug 2024 16:16:38 +0300 Subject: [PATCH 2/6] Add "list_concat_usage" test --- .../org/usvm/samples/SimpleTypeInferenceTest.kt | 14 ++++++++++++++ .../test/resources/samples/SimpleTypeInference.py | 6 ++++++ 2 files changed, 20 insertions(+) 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 From b56e3a2017812c9f1ef13f19fe1b9c8efd880bc8 Mon Sep 17 00:00:00 2001 From: nostromo Date: Mon, 12 Aug 2024 16:19:02 +0300 Subject: [PATCH 3/6] Changed test to detect PyMockTypeStream issues --- .../runner/manual/program/PrimitivePrograms.kt | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) 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) } From d4ab7a6825295b5cfe82f48b52b12dc1f7419206 Mon Sep 17 00:00:00 2001 From: nostromo Date: Tue, 13 Aug 2024 10:09:13 +0300 Subject: [PATCH 4/6] Add sq_concat notification --- .../java/org/usvm/interpreter/CPythonAdapter.java | 12 ++++++++++++ .../src/main/kotlin/org/usvm/language/Callables.kt | 1 + .../symbolic/operations/basic/MethodNotifications.kt | 11 +++++++++++ .../org/usvm/machine/ps/types/SymbolTypeTree.kt | 5 +++++ 4 files changed, 29 insertions(+) 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 f3b34ec3c0..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 @@ -1072,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/symbolic/operations/basic/MethodNotifications.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt index 2203441310..3da567f94b 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 @@ -78,6 +78,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)) } From 3c58a20a6dc3620f39bebf4abac95b1e5da7f2d4 Mon Sep 17 00:00:00 2001 From: nostromo Date: Tue, 13 Aug 2024 10:11:05 +0300 Subject: [PATCH 5/6] fix: more accurate nbAddKt function --- .../symbolic/operations/basic/MethodNotifications.kt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 3da567f94b..b26ee3aa60 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 @@ -38,9 +38,14 @@ fun nbAddKt( context.ctx ) { context.curState ?: return + /* + 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. + */ val nbAdd = left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd) val sqConcat = left.evalIsSoft(context, HasSqConcat) and right.evalIsSoft(context, HasSqConcat) - pyAssert(context, context.ctx.mkImplies(nbAdd.not(), sqConcat)) + pyAssert(context, nbAdd.not() implies sqConcat) pyFork(context, nbAdd) } From b6da4e165ad68eb6d54a4f04c327afc89e6ef78b Mon Sep 17 00:00:00 2001 From: nostromo Date: Tue, 13 Aug 2024 17:52:26 +0300 Subject: [PATCH 6/6] fix linter --- .../symbolic/operations/basic/MethodNotifications.kt | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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 b26ee3aa60..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 @@ -39,10 +39,12 @@ fun nbAddKt( ) { context.curState ?: return /* - 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. - */ + * 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)