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)) }