Fixes with arrays

Author: CaelmBleidd

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

@@ -738,7 +738,7 @@ 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)
                     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/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();