Add support for arrays

usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

@@ -55,7 +55,7 @@ sealed interface TsValue {
         val properties: Map<String, TsValue>,
     ) : TsValue
 
-    data class TsArray(
-        val values: List<TsValue>,
+    data class TsArray<T : TsValue>(
+        val values: List<T>,
     ) : TsValue
 }

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

@@ -7,6 +7,7 @@ import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsRefType
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsUndefinedType
+import org.jacodb.ets.base.EtsUnionType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.model.EtsScene
 import org.usvm.UAddressSort
@@ -46,6 +47,7 @@ class TsContext(
         is EtsNullType -> addressSort
         is EtsUndefinedType -> addressSort
         is EtsUnknownType -> unresolvedSort
+        is EtsUnionType -> unresolvedSort
         else -> TODO("Support all JacoDB types, encountered $type")
     }
 

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

@@ -63,6 +63,7 @@ import org.jacodb.ets.base.EtsTypeOfExpr
 import org.jacodb.ets.base.EtsUnaryExpr
 import org.jacodb.ets.base.EtsUnaryPlusExpr
 import org.jacodb.ets.base.EtsUndefinedConstant
+import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.base.EtsVoidExpr
@@ -74,7 +75,9 @@ import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.api.allocateArray
 import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.collection.array.UArrayIndexLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
@@ -88,6 +91,7 @@ import org.usvm.machine.types.FakeType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.memory.ULValue
 import org.usvm.memory.URegisterStackLValue
+import org.usvm.sizeSort
 import org.usvm.util.fieldLookUp
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
 
@@ -494,8 +498,19 @@ class TsExprResolver(
     // region ACCESS
 
     override fun visit(value: EtsArrayAccess): UExpr<out USort>? {
-        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
-        error("Not supported $value")
+        val instance = resolve(value.array)?.asExpr(ctx.addressSort) ?: return null
+        val index = resolve(value.index)?.asExpr(ctx.fp64Sort) ?: return null
+        val bvIndex = ctx.mkFpToBvExpr(
+            roundingMode = ctx.fpRoundingModeSortDefaultValue(),
+            value = index,
+            bvSize = 32,
+            isSigned = true
+        )
+
+        val sort = if (value.type is EtsUnknownType) ctx.addressSort else ctx.typeToSort(value.type)
+        val lValue = UArrayIndexLValue(sort, instance, bvIndex, value.array.type)
+
+        return scope.calcOnState { memory.read(lValue) }
     }
 
     private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
@@ -546,9 +561,42 @@ class TsExprResolver(
         memory.allocConcrete(expr.type)
     }
 
-    override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+    override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? = with(ctx) {
+        scope.calcOnState {
+            val size = resolve(expr.size) ?: return@calcOnState null
+
+            if (size.sort != fp64Sort) {
+                TODO()
+            }
+
+            val bvSize = mkFpToBvExpr(
+                fpRoundingModeSortDefaultValue(),
+                size.asExpr(fp64Sort),
+                bvSize = 32,
+                isSigned = true
+            )
+
+            val condition = mkAnd(
+                mkEq(
+                    mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), bvSize, signed = true),
+                    size.asExpr(fp64Sort)
+                ),
+                mkAnd(
+                    mkBvSignedLessOrEqualExpr(0.toBv(), bvSize.asExpr(bv32Sort)),
+                    mkBvSignedLessOrEqualExpr(bvSize, Int.MAX_VALUE.toBv().asExpr(bv32Sort))
+                )
+            )
+
+            scope.fork(
+                condition,
+                blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+            )
+
+            val address = memory.allocateArray(expr.type, sizeSort, bvSize)
+            memory.types.allocate(address.address, expr.type)
+
+            address
+        }
     }
 
     override fun visit(expr: EtsLengthExpr): UExpr<out USort>? {
@@ -665,9 +713,8 @@ class TsSimpleValueResolver(
         mkUndefinedValue()
     }
 
-    override fun visit(value: EtsArrayAccess): UExpr<out USort> = with(ctx) {
-        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
-        error("Not supported $value")
+    override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
+        error("Should not be called")
     }
 
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort> = with(ctx) {

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

@@ -2,6 +2,7 @@ package org.usvm.machine.interpreter
 
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
+import org.jacodb.ets.base.EtsArrayAccess
 import org.jacodb.ets.base.EtsAssignStmt
 import org.jacodb.ets.base.EtsCallStmt
 import org.jacodb.ets.base.EtsGotoStmt
@@ -22,6 +23,7 @@ import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UInterpreter
 import org.usvm.api.targets.TsTarget
+import org.usvm.collection.array.UArrayIndexLValue
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.machine.TsApplicationGraph
@@ -130,11 +132,41 @@ class TsInterpreter(
         }
 
         scope.doWithState {
-            val idx = mapLocalToIdx(lastEnteredMethod, stmt.lhv)
-            saveSortForLocal(idx, expr.sort)
+            when (val lhv = stmt.lhv) {
+                is EtsLocal -> {
+                    val idx = mapLocalToIdx(lastEnteredMethod, lhv)
+                    saveSortForLocal(idx, expr.sort)
 
-            val lValue = URegisterStackLValue(expr.sort, idx)
-            memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
+                    val lValue = URegisterStackLValue(expr.sort, idx)
+                    memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
+                }
+
+                is EtsArrayAccess -> {
+                    // TODO save sorts?
+                    val instance = exprResolver.resolve(lhv.array)?.asExpr(ctx.addressSort) ?: return@doWithState
+                    val index = exprResolver.resolve(lhv.index)?.asExpr(ctx.fp64Sort) ?: return@doWithState
+
+                    // TODO fork on floating point field
+                    val bvIndex = ctx.mkFpToBvExpr(
+                        roundingMode = ctx.fpRoundingModeSortDefaultValue(),
+                        value = index,
+                        bvSize = 32,
+                        isSigned = true
+                    )
+
+                    if (stmt.lhv.type == stmt.rhv.type) {
+                        val lValue = UArrayIndexLValue(expr.sort, instance, bvIndex, lhv.array.type)
+                        // TODO error with array values type
+                        memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
+                    } else {
+                        val lValue = UArrayIndexLValue(ctx.unresolvedSort, instance, bvIndex, lhv.array.type)
+                        // TODO create fake object, probably the type of the array should be modified as well
+                        memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
+                    }
+                }
+
+                else -> TODO("Not yet implemented")
+            }
 
             val nextStmt = stmt.nextStmt ?: return@doWithState
             newStmt(nextStmt)

usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt

@@ -0,0 +1,106 @@
+package org.usvm.samples
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import org.usvm.api.TsValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.getResourcePath
+
+class Arrays : TsMethodTestRunner() {
+    override val scene: EtsScene = run {
+        val name = "Arrays.ts"
+        val path = getResourcePath("/samples/$name")
+        val file = loadEtsFileAutoConvert(path)
+        EtsScene(listOf(file))
+    }
+
+    @Test
+    fun testCreateConstantArrayOfNumbers() {
+        val method = getMethod("Arrays", "createConstantArrayOfNumbers")
+        discoverProperties<TsValue.TsNumber>(
+            method = method,
+            { r -> r.number == 1.0 },
+            invariants = arrayOf(
+                { r -> r.number != -1.0 }
+            )
+        )
+    }
+
+    @Test
+    fun testCreateAndReturnConstantArrayOfNumbers() {
+        val method = getMethod("Arrays", "createAndReturnConstantArrayOfNumbers")
+        discoverProperties<TsValue.TsArray<TsValue.TsNumber>>(
+            method = method,
+            { r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0) },
+        )
+    }
+
+    @Test
+    fun testCreateAndAccessArrayOfBooleans() {
+        val method = getMethod("Arrays", "createAndAccessArrayOfBooleans")
+        discoverProperties<TsValue.TsNumber>(
+            method = method,
+            { r -> r.number == 1.0 },
+            invariants = arrayOf(
+                { r -> r.number != -1.0 }
+            )
+        )
+    }
+
+    @Test
+    fun testCreateArrayOfBooleans() {
+        val method = getMethod("Arrays", "createArrayOfBooleans")
+        discoverProperties<TsValue.TsArray<TsValue.TsBoolean>>(
+            method = method,
+            { r -> r.values.map { it.value } == listOf(true, false, true) },
+        )
+    }
+
+    @Test
+    @Disabled("Arrays should contain only fake objects")
+    fun testCreateMixedArray() {
+        val method = getMethod("Arrays", "createMixedArray")
+        discoverProperties<TsValue.TsArray<*>>(
+            method = method,
+            { r ->
+                if (r.values.size != 3) return@discoverProperties false
+                val cond0 = r.values[0] is TsValue.TsNumber.TsDouble
+                val cond1 = r.values[1] is TsValue.TsBoolean
+                val cond2 = r.values[2] is TsValue.TsUndefined
+                cond0 && cond1 && cond2
+            },
+        )
+    }
+
+    @Test
+    fun testCreateArrayOfUnknown() {
+        val method = getMethod("Arrays", "createArrayOfUnknownValues")
+        discoverProperties<TsValue, TsValue, TsValue, TsValue.TsArray<*>>(
+            method = method,
+            { a, _, _, r -> r.values[0] == a && (a as TsValue.TsNumber).number == 1.1 },
+            { _, b, _, r -> r.values[1] == b && (b as TsValue.TsBoolean).value },
+            { _, _, c, r -> r.values[2] == c && c is TsValue.TsUndefined },
+            invariants = arrayOf(
+                { a, b, c, r -> r.values == listOf(a, b, c) }
+            )
+        )
+    }
+
+    @Test
+    @Disabled("Arrays should contain only fake objects")
+    fun testCreateArrayOfNumbersAndPutDifferentTypes() {
+        val method = getMethod("Arrays", "createArrayOfNumbersAndPutDifferentTypes")
+        discoverProperties<TsValue.TsArray<*>>(
+            method = method,
+            { r ->
+                val values = r.values
+                values.size == 3
+                    && (values[0] as TsValue.TsClass).properties.size == 1
+                    && (values[1] as TsValue.TsBoolean).value
+                    && values[2] is TsValue.TsUndefined
+            },
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/samples/MinValue.kt

@@ -21,7 +21,7 @@ class MinValue : TsMethodTestRunner() {
     @Disabled
     fun testMinValue() {
         val method = getMethod("MinValue", "findMinValue")
-        discoverProperties<TsValue.TsArray, TsValue.TsNumber>(
+        discoverProperties<TsValue.TsArray<*>, TsValue.TsNumber>(
             method,
         )
     }

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

@@ -1,6 +1,7 @@
 package org.usvm.util
 
 import org.jacodb.ets.base.EtsAnyType
+import org.jacodb.ets.base.EtsArrayType
 import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsClassType
 import org.jacodb.ets.base.EtsNullType
@@ -166,14 +167,18 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         when (klass) {
             TsValue::class -> EtsAnyType
             TsValue.TsAny::class -> EtsAnyType
-            TsValue.TsArray::class -> TODO()
-            TsValue.TsBoolean::class -> EtsBooleanType
+
+            TsValue.TsArray::class -> {
+                EtsArrayType(EtsAnyType, dimensions = 1) // TODO incorrect
+            }
+
             TsValue.TsClass::class -> {
                 // TODO incorrect
                 val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT)
                 EtsClassType(signature)
             }
 
+            TsValue.TsBoolean::class -> EtsBooleanType
             TsValue.TsString::class -> EtsStringType
             TsValue.TsNumber::class -> EtsNumberType
             TsValue.TsNumber.TsDouble::class -> EtsNumberType
@@ -184,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             // For untyped tests, not to limit objects serialized from models after type coercion.
             TsValue.TsUnknown::class -> EtsUnknownType
             TsValue.TsNull::class -> EtsNullType
+
             TsValue.TsException::class -> {
                 // TODO incorrect
                 val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT)