Add sq_concat notification

UnitTestBot · Aug 13, 2024 · d4ab7a6 · d4ab7a6
1 parent b56e3a2
commit d4ab7a6
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 0 deletions.
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
@@ -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
@@ -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/...ain/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt b/...ain/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
@@ -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))
                     }