Fixes with arrays

Author: CaelmBleidd

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

@@ -2,6 +2,7 @@ package org.usvm.machine.expr
 
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsInstanceCallExpr
@@ -301,7 +302,14 @@ private fun TsExprResolver.handleArrayPush(
             index = length,
             type = arrayType,
         )
-        memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
+
+        if (arg.sort != elementSort && (arrayType.elementType is EtsUnknownType || arrayType.elementType is EtsAnyType)) {
+            val wrappedArg = arg.toFakeObject(scope)
+            lValuesToAllocatedFakeObjects += newIndexLValue to wrappedArg
+            memory.write(newIndexLValue, wrappedArg.asExpr(elementSort), guard = trueExpr)
+        } else {
+            memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
+        }
 
         // Return the new length of the array (as per ECMAScript spec for Array.push)
         mkBvToFpExpr(

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/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt

@@ -304,7 +304,11 @@ class TsTypeSystem(
             is EtsClassType,
                 ->
                 if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
-                    scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType
+                    val classes = scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType
+
+                    classes + classes.map { EtsArrayType(it, 1) } +
+                        EtsArrayType(EtsNumberType, 1) +
+                        EtsArrayType(EtsBooleanType, 1)
                 } else {
                     hierarchy.classesForType(t)
                         .asSequence()

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();