Fix Array.concat approximation

Author: Lipen

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt

@@ -24,6 +24,7 @@ import org.usvm.machine.interpreter.PromiseState
 import org.usvm.machine.interpreter.markResolved
 import org.usvm.machine.interpreter.setResolvedValue
 import org.usvm.sizeSort
+import org.usvm.types.first
 import org.usvm.types.firstOrNull
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
@@ -546,7 +547,6 @@ private fun TsExprResolver.handleArrayJoin(
  * The `start` index is inclusive, and the `end` index is exclusive.
  * If `start` is not provided, it defaults to `0`.
  * If `end` is not provided, it defaults to the length of the array.
- * This method returns the sliced array.
  *
  * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.slice
  */
@@ -566,6 +566,7 @@ private fun TsExprResolver.handleArraySlice(
     }
     val startBv: UExpr<TsSizeSort> = when (start.sort) {
         sizeSort -> start.asExpr(sizeSort)
+
         fp64Sort -> mkFpToBvExpr(
             roundingMode = fpRoundingModeSortDefaultValue(),
             value = start.asExpr(fp64Sort),
@@ -586,6 +587,7 @@ private fun TsExprResolver.handleArraySlice(
     }
     val endBv: UExpr<TsSizeSort> = when (end.sort) {
         sizeSort -> end.asExpr(sizeSort)
+
         fp64Sort -> mkFpToBvExpr(
             roundingMode = fpRoundingModeSortDefaultValue(),
             value = end.asExpr(fp64Sort),
@@ -623,9 +625,20 @@ private fun TsExprResolver.handleArraySlice(
 }
 
 /**
- * Handles the `Array.concat(...arrays)` method call.
- * Concatenates the specified `arrays` to the end of the current array.
- * This method modifies the array in place and returns the modified array.
+ * Handles the `Array.concat(...items)` method call.
+ * Returns a new array containing the elements of the original array followed by the array elements of each argument.
+ *
+ * ### Examples:
+ * ```
+ * let a = [1, 2];
+ * let b = [3, 4];
+ *
+ * a.concat() -> [1, 2]
+ * a.concat(b) -> [1, 2, 3, 4]
+ * a.concat(b, 5) -> [1, 2, 3, 4, 5]
+ *
+ * a == [1, 2] // not modified
+ * ```
  *
  * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.concat
  */
@@ -641,37 +654,44 @@ private fun TsExprResolver.handleArrayConcat(
 
     val args = expr.args.map { resolve(it) ?: return null }
 
+    logger.warn {
+        "Array.concat() is not fully implemented, returning a symbolic array approximation"
+    }
+
     scope.calcOnState {
-        // Read the length of the array
-        val lengthLValue = mkArrayLengthLValue(array, arrayType)
-        val length = scope.calcOnState { memory.read(lengthLValue) }
-
-        // Iterate over the provided arrays and concatenate them
-        args.forEach { arg ->
-            val otherArray = arg.asExpr(addressSort)
-
-            // Read the length of the argument array
-            val argLengthLValue = mkArrayLengthLValue(otherArray, arrayType)
-            val argLength = memory.read(argLengthLValue)
-
-            // Copy the elements from the argument array to the end of the current array
-            memory.memcpy(
-                srcRef = otherArray,
-                dstRef = array,
-                type = arrayType,
-                elementSort = elementSort,
-                fromSrc = 0.toBv().asExpr(sizeSort),
-                fromDst = length,
-                length = argLength,
-            )
-
-            // Update the length of the current array
-            val newLength = mkBvAddExpr(length, argLength)
-            scope.doWithState { memory.write(lengthLValue, newLength, guard = trueExpr) }
+        // Allocate a new array for the concatenated result
+        val resultArray = memory.allocConcrete(arrayType)
+
+        // Read the length of the original array
+        val originalLengthLValue = mkArrayLengthLValue(array, arrayType)
+        val originalLength = memory.read(originalLengthLValue)
+
+        // Calculate the total length of the result
+        var totalLength = originalLength
+        for (arg in args) {
+            // For each array-like argument, add its length to the total length
+            if (arg.sort == addressSort) {
+                // TODO: handle empty type stream
+                val argType = memory.typeStreamOf(arg.asExpr(addressSort)).first()
+                if (argType is EtsArrayType) {
+                    val argLengthLValue = mkArrayLengthLValue(arg.asExpr(addressSort), argType)
+                    val argLength = memory.read(argLengthLValue)
+                    totalLength = mkBvAddExpr(totalLength, argLength)
+                    continue
+                }
+            }
+            // For non-array arguments, treat them as a single element
+            totalLength = mkBvAddExpr(totalLength, 1.toBv())
         }
 
-        // Return the modified array
-        array
+        // TODO: fill the resultArray
+
+        // Set the length of the result array
+        val resultLengthLValue = mkArrayLengthLValue(resultArray, arrayType)
+        memory.write(resultLengthLValue, totalLength, guard = trueExpr)
+
+        // Return the new concatenated array (with symbolic content)
+        resultArray
     }
 }
 
@@ -699,7 +719,7 @@ private fun TsExprResolver.handleArrayIndexOf(
         val length = memory.read(lengthLValue)
 
         // Create a symbolic index that is either -1 (not found) or a valid index
-        val symbolicResult = memory.mocker.createMockSymbol(null, sizeSort, ownership)
+        val symbolicResult = makeSymbolicPrimitive(sizeSort)
 
         // Add constraints: result is either -1 or in range [0, length-1]
         val notFound = mkEq(symbolicResult, mkBv(-1, sizeSort))

usvm-ts/src/test/kotlin/org/usvm/samples/arrays/ArrayMethods.kt

@@ -120,12 +120,14 @@ class ArrayMethods : TsMethodTestRunner() {
         discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
             method = method,
             { x, r ->
-                x.value && r is TsTestValue.TsArray<*>
-                // Note: Current implementation modifies array in-place (spec deviation)
+                // if (x) then [1, 2, 3, 4]
+                x.value && r is TsTestValue.TsArray<*> && r.values.map { it as TsTestValue.TsNumber }
+                    .map { it.number } == listOf(1.0, 2..0, 3.0, 4.0)
             },
             { x, r ->
-                !x.value && r is TsTestValue.TsArray<*>
-                // Note: Should return new array according to spec
+                // if (!x) then [1, 2]
+                x.value && r is TsTestValue.TsArray<*> && r.values.map { it as TsTestValue.TsNumber }
+                    .map { it.number } == listOf(1.0, 2..0)
             },
         )
     }

usvm-ts/src/test/resources/samples/arrays/ArrayMethods.ts

@@ -69,12 +69,11 @@ class ArrayMethods {
     arrayConcat(x: boolean) {
         const arr1 = [1, 2];
         const arr2 = [3, 4];
+        const result = arr1.concat(arr2);
         if (x) {
-            arr1.concat(arr2);
-            return arr1;  // [1, 2, 3, 4] - modified in place
-        } else {
-            const result = arr1.concat(arr2);
             return result;  // [1, 2, 3, 4]
+        } else {
+            return arr1;  // [1, 2]
         }
     }