Support arrays containing values of different types

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

@@ -1,6 +1,7 @@
 package org.usvm.machine
 
 import io.ksmt.sort.KFp64Sort
+import io.ksmt.utils.asExpr
 import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsNumberType
@@ -20,6 +21,8 @@ import org.usvm.USort
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.expr.TsUndefinedSort
 import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.types.FakeType
 import kotlin.contracts.ExperimentalContracts
 import kotlin.contracts.contract
 
@@ -60,6 +63,37 @@ class TsContext(
         return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET
     }
 
+    fun UExpr<out USort>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
+        if (isFakeObject()) {
+            return this
+        }
+
+        val ref = createFakeObjectRef()
+
+        scope.calcOnState {
+            when (sort) {
+                boolSort -> {
+                    val lvalue = getIntermediateBoolLValue(ref.address)
+                    memory.write(lvalue, [email protected](boolSort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.fromBool(this@TsContext))
+                }
+                fp64Sort -> {
+                    val lValue = getIntermediateFpLValue(ref.address)
+                    memory.write(lValue, [email protected](fp64Sort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.fromFp(this@TsContext))
+                }
+                addressSort -> {
+                    val lValue = getIntermediateRefLValue(ref.address)
+                    memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
+                    memory.write(lValue, [email protected](addressSort), guard = trueExpr)
+                }
+                else -> TODO("Not yet supported")
+            }
+        }
+
+        return ref
+    }
+
     fun createFakeObjectRef(): UConcreteHeapRef {
         val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
         return mkConcreteHeapRef(address)

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

@@ -6,6 +6,7 @@ import mu.KotlinLogging
 import org.jacodb.ets.base.EtsAddExpr
 import org.jacodb.ets.base.EtsAndExpr
 import org.jacodb.ets.base.EtsArrayAccess
+import org.jacodb.ets.base.EtsArrayType
 import org.jacodb.ets.base.EtsAwaitExpr
 import org.jacodb.ets.base.EtsBinaryExpr
 import org.jacodb.ets.base.EtsBitAndExpr
@@ -78,6 +79,7 @@ import org.usvm.USort
 import org.usvm.api.allocateArray
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.collection.array.UArrayIndexLValue
+import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
@@ -497,20 +499,22 @@ class TsExprResolver(
 
     // region ACCESS
 
-    override fun visit(value: EtsArrayAccess): UExpr<out USort>? {
+    override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
         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(),
+        val bvIndex = mkFpToBvExpr(
+            roundingMode = 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)
+        val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type)
+        val expr = scope.calcOnState { memory.read(lValue) }
+
+        check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
 
-        return scope.calcOnState { memory.read(lValue) }
+        return expr
     }
 
     private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
@@ -535,7 +539,16 @@ class TsExprResolver(
 
         checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
 
-        // TODO: checkNullPointer(instanceRef)
+        // TODO It is a hack for array's length
+        if (value.instance.type is EtsArrayType && value.field.name == "length") {
+            val lValue = UArrayLengthLValue(instanceRef, value.instance.type, ctx.sizeSort)
+            val expr = scope.calcOnState { memory.read(lValue) }
+
+            check(expr.sort == ctx.sizeSort)
+
+            return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true)
+        }
+
         val fieldType = scene.fieldLookUp(value.field).type
         val sort = typeToSort(fieldType)
         val lValue = UFieldLValue(sort, instanceRef, value.field.name)

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

@@ -24,6 +24,7 @@ import org.usvm.StepScope
 import org.usvm.UInterpreter
 import org.usvm.api.targets.TsTarget
 import org.usvm.collection.array.UArrayIndexLValue
+import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.machine.TsApplicationGraph
@@ -38,6 +39,7 @@ import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
 import org.usvm.memory.URegisterStackLValue
+import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
 import org.usvm.utils.ensureSat
 
@@ -123,11 +125,11 @@ class TsInterpreter(
         }
     }
 
-    private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) {
+    private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) {
         val exprResolver = exprResolverWithScope(scope)
         val expr = exprResolver.resolve(stmt.rhv) ?: return
 
-        check(expr.sort != ctx.unresolvedSort) {
+        check(expr.sort != unresolvedSort) {
             "A value of the unresolved sort should never be returned from `resolve` function"
         }
 
@@ -138,31 +140,33 @@ class TsInterpreter(
                     saveSortForLocal(idx, expr.sort)
 
                     val lValue = URegisterStackLValue(expr.sort, idx)
-                    memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
+                    memory.write(lValue, expr.asExpr(lValue.sort), guard = 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
+                    val instance = exprResolver.resolve(lhv.array)?.asExpr(addressSort) ?: return@doWithState
+                    val index = exprResolver.resolve(lhv.index)?.asExpr(fp64Sort) ?: return@doWithState
 
                     // TODO fork on floating point field
-                    val bvIndex = ctx.mkFpToBvExpr(
-                        roundingMode = ctx.fpRoundingModeSortDefaultValue(),
+                    val bvIndex = mkFpToBvExpr(
+                        roundingMode = 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)
-                    }
+                    ).asExpr(sizeSort)
+
+                    val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort)
+                    val currentLength = memory.read(lengthLValue).asExpr(sizeSort)
+
+                    val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength)
+                    val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength)
+
+                    memory.write(lengthLValue, newLength, guard = trueExpr)
+
+                    val fakeExpr = expr.toFakeObject(scope)
+
+                    val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type)
+                    memory.write(lValue, fakeExpr, guard = trueExpr)
                 }
 
                 else -> TODO("Not yet implemented")

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt

@@ -421,9 +421,57 @@ sealed interface TsBinaryOperator {
             scope: TsStepScope,
         ): UExpr<out USort> {
             check(lhs.isFakeObject() || rhs.isFakeObject())
-            // TODO: delegating to '==' is not correct in general case
-            return with(Eq) {
-                resolveFakeObject(lhs, rhs, scope)
+
+            return scope.calcOnState {
+                when {
+                    lhs.isFakeObject() && rhs.isFakeObject() -> {
+                        val lhsType = memory.typeStreamOf(lhs).single() as FakeType
+                        val rhsType = memory.typeStreamOf(rhs).single() as FakeType
+
+                        scope.assert(
+                            mkAnd(
+                                lhsType.boolTypeExpr eq rhsType.boolTypeExpr,
+                                lhsType.fpTypeExpr eq rhsType.fpTypeExpr,
+                                // TODO support type equality
+                                lhsType.refTypeExpr eq rhsType.refTypeExpr
+                            )
+                        )
+                    }
+
+                    lhs.isFakeObject() -> {
+                        val lhsType = memory.typeStreamOf(lhs).single() as FakeType
+
+                        val condition = when (rhs.sort) {
+                            boolSort -> lhsType.boolTypeExpr
+                            fp64Sort -> lhsType.fpTypeExpr
+                            // TODO support type equality
+                            addressSort -> lhsType.refTypeExpr
+                            else -> error("Unsupported sort ${rhs.sort}")
+                        }
+
+                        scope.assert(condition)
+                    }
+
+                    rhs.isFakeObject() -> {
+                        val rhsType = memory.typeStreamOf(rhs).single() as FakeType
+
+                        scope.assert(rhsType.mkExactlyOneTypeConstraint(ctx))
+
+                        val condition = when (lhs.sort) {
+                            boolSort -> rhsType.boolTypeExpr
+                            fp64Sort -> rhsType.fpTypeExpr
+                            // TODO support type equality
+                            addressSort -> rhsType.refTypeExpr
+                            else -> error("Unsupported sort ${lhs.sort}")
+                        }
+
+                        scope.assert(condition)
+                    }
+                }
+
+                return@calcOnState with(Eq) {
+                    resolveFakeObject(lhs, rhs, scope)
+                }
             }
         }
 

usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt

@@ -27,6 +27,20 @@ class FakeType(
             mkOr(boolTypeExpr, fpTypeExpr, refTypeExpr),
         )
     }
+
+    companion object {
+        fun fromBool(ctx: TsContext): FakeType {
+            return FakeType(ctx.mkTrue(), ctx.mkFalse(), ctx.mkFalse())
+        }
+
+        fun fromFp(ctx: TsContext): FakeType {
+            return FakeType(ctx.mkFalse(), ctx.mkTrue(), ctx.mkFalse())
+        }
+
+        fun fromRef(ctx: TsContext): FakeType {
+            return FakeType(ctx.mkFalse(), ctx.mkFalse(), ctx.mkTrue())
+        }
+    }
 }
 
 data class ExprWithTypeConstraint<T : USort>(val constraint: UBoolExpr, val expr: UExpr<T>)

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

@@ -2,7 +2,6 @@ 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
@@ -59,7 +58,6 @@ class Arrays : TsMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Arrays should contain only fake objects")
     fun testCreateMixedArray() {
         val method = getMethod("Arrays", "createMixedArray")
         discoverProperties<TsValue.TsArray<*>>(
@@ -75,7 +73,7 @@ class Arrays : TsMethodTestRunner() {
     }
 
     @Test
-    fun testCreateArrayOfUnknown() {
+    fun testCreateArrayOfUnknownValues() {
         val method = getMethod("Arrays", "createArrayOfUnknownValues")
         discoverProperties<TsValue, TsValue, TsValue, TsValue.TsArray<*>>(
             method = method,
@@ -89,18 +87,42 @@ class Arrays : TsMethodTestRunner() {
     }
 
     @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[0] is TsValue.TsNull
                     && (values[1] as TsValue.TsBoolean).value
                     && values[2] is TsValue.TsUndefined
             },
         )
     }
+
+    @Test
+    fun testAllocatedArrayLengthExpansion() {
+        val method = getMethod("Arrays", "allocatedArrayLengthExpansion")
+        discoverProperties<TsValue.TsArray<*>>(
+            method = method,
+            { r -> r.values.size == 6
+                && (r.values[0] as TsValue.TsNumber).number == 1.0
+                && (r.values[1] as TsValue.TsNumber).number == 2.0
+                && (r.values[2] as TsValue.TsNumber).number == 3.0
+                && r.values[3] is TsValue.TsUndefined
+                && r.values[4] is TsValue.TsUndefined
+                && (r.values[5] as TsValue.TsNumber).number == 5.0
+            }
+        )
+    }
+
+    @Test
+    fun testWriteInTheIndexEqualToLength() {
+        val method = getMethod("Arrays", "writeInTheIndexEqualToLength")
+        discoverProperties<TsValue.TsArray<TsValue.TsNumber>>(
+            method = method,
+            { r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) },
+        )
+    }
 }

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

@@ -170,14 +170,16 @@ open class TsTestStateResolver(
 
         val values = (0 until length.intValue).map {
             val index = ctx.mkSizeExpr(it)
-            // TODO wrong sort
-            val lValue = if (type.elementType is EtsUnknownType) {
-                UArrayIndexLValue(ctx.addressSort, expr, index, type)
-            } else {
-                UArrayIndexLValue(ctx.typeToSort(type.elementType), expr, index, type)
+            val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type)
+            val value = memory.read(lValue)
+
+            if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) {
+                return@map TsValue.TsUndefined
             }
-            val value = memory.read(lValue) // TODO write reading???
-            resolveExpr(value, type.elementType)
+
+            with(ctx) { check(value.isFakeObject()) { "Only fake objects are allowed in arrays" } }
+
+            resolveFakeObject(value as UConcreteHeapRef)
         }
 
         return TsValue.TsArray(values)