[TS] Model the Array constructor

`new Array(n)` used to allocate an object of an unresolved class (8
occurrences on the maths corpus probe), so none of the array
approximations applied to it and every subsequent operation on the array
was mocked. Now:
- `new Array` in EtsNewExpr allocates a genuine array object
  (EtsArrayType, length 0), so the array method approximations and the
  constructor handling apply to it;
- the `constructor` call on an array-typed instance is approximated:
  the zero-argument form keeps the empty length, the single-argument form
  sets the length with the same size-validity fork as EtsNewArrayExpr
  (non-integral or negative sizes throw, as in JS); the multi-argument
  literal form is left to the logged mock fallback.

Author: CaelmBleidd

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

@@ -11,10 +11,12 @@ import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsUnknownType
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.initializeArray
+import org.usvm.api.initializeArrayLength
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.api.memcpy
 import org.usvm.api.typeStreamOf
@@ -120,6 +122,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
             .takeIf { it !is TsUnresolvedSort }
             ?: addressSort
 
+        // Handle the `Array` constructor: `new Array()` / `new Array(n)`
+        if (expr.callee.name == CONSTRUCTOR_NAME) {
+            return from(handleArrayConstructor(expr, instanceType))
+        }
+
         // Handle 'Array.push()' method calls
         if (expr.callee.name == "push") {
             return from(handleArrayPush(expr, instanceType, elementSort))
@@ -574,6 +581,66 @@ private fun TsExprResolver.handleArrayPop(
  *
  * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.fill
  */
+/**
+ * The `Array` constructor. `new Array()` keeps the zero length set at allocation;
+ * `new Array(n)` sets the length to `n`, forking on the validity of the size
+ * (a non-integral or out-of-range `n` throws a RangeError in JS).
+ * The multi-argument literal form `new Array(a, b, ...)` is not approximated.
+ */
+private fun TsExprResolver.handleArrayConstructor(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,
+): UExpr<*>? = with(ctx) {
+    val resolved = resolve(expr.instance)?.asExpr(addressSort) ?: return null
+    val array = resolved as? UConcreteHeapRef ?: run {
+        logger.warn { "Array constructor on a non-concrete instance is not approximated" }
+        return null
+    }
+
+    when (expr.args.size) {
+        0 -> array
+
+        1 -> {
+            val size = resolve(expr.args.single()) ?: return null
+            if (size.sort != fp64Sort) {
+                logger.warn { "Unsupported sort for the Array constructor size: ${size.sort}" }
+                return null
+            }
+            val bvSize = mkFpToBvExpr(
+                roundingMode = fpRoundingModeSortDefaultValue(),
+                value = size.asExpr(fp64Sort),
+                bvSize = 32,
+                isSigned = true,
+            )
+            val isValidSize = mkAnd(
+                mkEq(
+                    mkBvToFpExpr(
+                        sort = fp64Sort,
+                        roundingMode = fpRoundingModeSortDefaultValue(),
+                        value = bvSize,
+                        signed = true,
+                    ),
+                    size.asExpr(fp64Sort),
+                ),
+                mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)),
+            )
+            scope.fork(
+                isValidSize,
+                blockOnFalseState = { throwException("Invalid array length: ${size.asExpr(fp64Sort)}") },
+            ) ?: return null
+            scope.doWithState {
+                memory.initializeArrayLength(array, arrayType, sizeSort, bvSize.asExpr(sizeSort))
+            }
+            array
+        }
+
+        else -> {
+            logger.warn { "The literal form of the Array constructor is not approximated: ${expr.args.size} args" }
+            null
+        }
+    }
+}
+
 private fun TsExprResolver.handleArrayFill(
     expr: EtsInstanceCallExpr,
     arrayType: EtsArrayType,

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

@@ -973,6 +973,18 @@ class TsExprResolver(
             expr.type
         }
 
+        if (expr.type.typeName == "Array") {
+            // `new Array(...)`: allocate a genuine array object so that the array
+            // approximations apply; the length is set by the constructor call
+            // that immediately follows the allocation.
+            val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+            return@with scope.calcOnState {
+                val address = memory.allocConcrete(arrayType)
+                memory.initializeArrayLength(address, arrayType, sizeSort, mkBv(0).asExpr(sizeSort))
+                address
+            }
+        }
+
         if (expr.type.typeName == "Boolean") {
             val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxByOrNull { it.methods.size }
                 ?: error("No Boolean class found in SDK")