[TS] Fixes with arrays

usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt

@@ -3,4 +3,5 @@ package org.usvm.machine
 data class TsOptions(
     val interproceduralAnalysis: Boolean = true,
     val enableVisualization: Boolean = false,
+    val maxArraySize: Int = 1_000,
 )

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

@@ -248,3 +248,16 @@ fun TsContext.checkReadingInRange(
         blockOnFalseState = { throwException("Index out of bounds: $index, length: $length") }
     )
 }
+
+fun TsContext.checkLengthBounds(
+    scope: TsStepScope,
+    length: UExpr<TsSizeSort>,
+    maxLength: Int,
+): Unit? {
+    // Check that length is non-negative and does not exceed `maxLength`.
+    val condition = mkAnd(
+        mkBvSignedGreaterOrEqualExpr(length, mkBv(0)),
+        mkBvSignedLessOrEqualExpr(length, mkBv(maxLength))
+    )
+    return scope.assert(condition)
+}

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

@@ -59,14 +59,15 @@
     }
 
     // Read the array element.
-    readArray(scope, arrayRef, bvIndex, arrayType)
+    readArray(scope, arrayRef, bvIndex, arrayType, options.maxArraySize)
 }
 
 fun TsContext.readArray(
     scope: TsStepScope,
     array: UHeapRef,
     index: UExpr<TsSizeSort>,
     arrayType: EtsArrayType,
+    maxArraySize: Int,
 ): UExpr<*>? {
     checkNotFake(array)
 

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

@@ -49,7 +49,7 @@ internal fun TsExprResolver.handleInstanceFieldRef(
 
     // Handle reading "length" property.
     if (value.field.name == "length") {
-        return readLengthProperty(scope, instanceLocal, instance)
+        return readLengthProperty(scope, instanceLocal, instance, options.maxArraySize)
     }
 
     // Read the field.

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

@@ -18,7 +18,8 @@ fun TsContext.readLengthProperty(
     scope: TsStepScope,
     instanceLocal: EtsLocal,
     instance: UHeapRef,
-): UExpr<*> {
+    maxArraySize: Int,
+): UExpr<*>? {
     // Determine the array type.
     val arrayType: EtsArrayType = when (val type = instanceLocal.type) {
         is EtsArrayType -> type
@@ -33,15 +34,16 @@ fun TsContext.readLengthProperty(
     }
 
     // Read the length of the array.
-    return readArrayLength(scope, instance, arrayType)
+    return readArrayLength(scope, instance, arrayType, maxArraySize)
 }
 
 // Reads the length of the array and returns it as a fp64 expression.
 fun TsContext.readArrayLength(
     scope: TsStepScope,
     array: UHeapRef,
     arrayType: EtsArrayType,
-): UExpr<KFp64Sort> {
+    maxArraySize: Int,
+): UExpr<KFp64Sort>? {
     checkNotFake(array)
 
     // Read the length of the array.
@@ -50,10 +52,8 @@ fun TsContext.readArrayLength(
         memory.read(lengthLValue)
     }
 
-    // Ensure that the length is non-negative.
-    scope.doWithState {
-        pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
-    }
+    // Check that the length is within the allowed bounds.
+    checkLengthBounds(scope, length, maxArraySize) ?: return null
 
     // Convert the length to fp64.
     return mkBvToFpExpr(

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

@@ -90,6 +90,7 @@ import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsOptions
 import org.usvm.machine.interpreter.PromiseState
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.getGlobals
@@ -133,6 +134,7 @@ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111
 class TsExprResolver(
     internal val ctx: TsContext,
     internal val scope: TsStepScope,
+    internal val options: TsOptions,
     internal val hierarchy: EtsHierarchy,
 ) : EtsEntity.Visitor<UExpr<out USort>?> {
 

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -75,6 +75,7 @@ import org.usvm.types.TypesResult
 import org.usvm.types.first
 import org.usvm.types.single
 import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.resolveEtsMethods
@@ -89,7 +90,7 @@ typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
 class TsInterpreter(
     private val ctx: TsContext,
     private val graph: TsGraph,
-    private val tsOptions: TsOptions,
+    private val options: TsOptions,
     private val observer: TsInterpreterObserver? = null,
 ) : UInterpreter<TsState>() {
 
@@ -603,7 +604,7 @@ class TsInterpreter(
                 }
             }
 
-            if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
+            if (!options.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
                 mockMethodCall(scope, callExpr.callee)
                 scope.doWithState { newStmt(stmt) }
                 return
@@ -637,7 +638,7 @@ class TsInterpreter(
             return
         }
 
-        if (tsOptions.interproceduralAnalysis) {
+        if (options.interproceduralAnalysis) {
             val exprResolver = exprResolverWithScope(scope)
             exprResolver.resolve(stmt.expr) ?: return
             val nextStmt = stmt.nextStmt ?: return
@@ -696,6 +697,7 @@ class TsInterpreter(
         TsExprResolver(
             ctx = ctx,
             scope = scope,
+            options = options,
             hierarchy = graph.hierarchy,
         )
 
@@ -738,7 +740,13 @@ class TsInterpreter(
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
 
                 if (parameterType is EtsArrayType) {
-                    state.pathConstraints += state.memory.types.evalTypeEquals(ref, parameterType)
+                    state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType)
+
+                    val lengthLValue = mkArrayLengthLValue(ref, parameterType)
+                    val length = state.memory.read(lengthLValue).asExpr(sizeSort)
+                    state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
+                    state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize))
+
                     return@run
                 }
 

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

@@ -25,6 +25,24 @@ class ArrayMethods : TsMethodTestRunner() {
         )
     }
 
+    @Test
+    fun testArrayPushIntoNumber() {
+        val method = getMethod("arrayPushIntoNumber")
+        discoverProperties<TsTestValue.TsArray<*>, TsTestValue.TsArray<*>>(
+            method = method,
+            { x, r -> x.values.size == r.values.size - 1 && (r.values.last() as TsTestValue.TsNumber).number == 123.0 }
+        )
+    }
+
+    @Test
+    fun testArrayPushIntoUnknown() {
+        val method = getMethod("arrayPushIntoUnknown")
+        discoverProperties<TsTestValue.TsArray<*>, TsTestValue.TsArray<*>>(
+            method = method,
+            { x, r -> x.values.size == r.values.size - 1 && (r.values.last() as TsTestValue.TsNumber).number == 123.0 }
+        )
+    }
+
     @Test
     fun testArrayPop() {
         val method = getMethod("arrayPop")

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

@@ -1,6 +1,7 @@
 package org.usvm.samples.arrays
 
 import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.RepeatedTest
 import org.junit.jupiter.api.Test
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
@@ -171,4 +172,13 @@ class InputArrays : TsMethodTestRunner() {
             },
         )
     }
+
+    @RepeatedTest(10)
+    fun `test getLength`() {
+        val method = getMethod("getLength")
+        discoverProperties<TsTestValue.TsArray<TsTestValue>, TsTestValue.TsNumber>(
+            method = method,
+            { x, r -> (r eq x.values.size) },
+        )
+    }
 }

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt

@@ -308,7 +308,7 @@ open class TsTestStateResolver(
                 "Other sorts must be resolved above, but got: $sort"
             }
 
-            val lValue = mkArrayIndexLValue(sort, concreteRef, index, type)
+            val lValue = mkArrayIndexLValue(sort, heapRef, index, type)
             val value = memory.read(lValue)
 
             if (value.sort is UAddressSort) {

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

@@ -12,6 +12,16 @@ class ArrayMethods {
         }
     }
 
+    arrayPushIntoNumber(x: number[]) {
+        x.push(123);
+        return x;
+    }
+
+    arrayPushIntoUnknown(x: any[]) {
+        x.push(123);
+        return x;
+    }
+
     arrayPop(x: boolean) {
         const arr = [10, 20, 30];
         const lastElement = arr.pop();

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

@@ -66,6 +66,10 @@ class InputArrays {
         if (input > 0) return -1; // unreachable, since 'input > 0' implies 'res.length > 0'
         return 0;
     }
+
+    getLength(x: number[]): number {
+        return x.length;
+    }
 }
 
 function createNumberArray(size: number): number[] {