Input arrays support

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

@@ -52,7 +52,6 @@ class TsContext(
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
-
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
@@ -77,14 +76,15 @@ class TsContext(
         else -> TODO("${type::class.simpleName} is not yet supported: $type")
     }
 
-    // TODO: for now, ALL descriptors for array are UNKNOWN
-    //  in order to make ALL reading/writing, including '.length' access consistent
-    //  and possible in cases when the array type is not known.
-    //  For example, when we access '.length' of some array, we do not care about its type,
-    //  but we HAVE TO use some type consistent with the type used when this array was created.
-    //  Note: Using UnknownType everywhere does not lead to any errors yet,
-    //  since we do not rely on array types in any way.
-    fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType
+    fun arrayDescriptorOf(type: EtsArrayType): EtsType {
+        return when (type.elementType) {
+            is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1)
+            is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1)
+            is EtsArrayType -> TODO("Unsupported yet: $type")
+            is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1)
+            else -> EtsArrayType(EtsUnknownType, dimensions = 1)
+        }
+    }
 
     fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType {
         check(isFakeObject())

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

@@ -23,6 +23,7 @@ import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
+import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatisticsImpl
 import org.usvm.statistics.distances.PlainCallGraphStatistics
 import org.usvm.stopstrategies.createStopStrategy
@@ -94,6 +95,10 @@ class TsMachine(
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
 
+        if (options.useSoftConstraints) {
+            observers.add(SoftConstraintsObserver())
+        }
+
         val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
 
         val stopStrategy = createStopStrategy(

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

@@ -5,6 +5,7 @@
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsAddExpr
 import org.jacodb.ets.model.EtsAndExpr
+import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayAccess
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsAwaitExpr
@@ -14,6 +15,7 @@
 import org.jacodb.ets.model.EtsBitOrExpr
 import org.jacodb.ets.model.EtsBitXorExpr
 import org.jacodb.ets.model.EtsBooleanConstant
+import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
@@ -44,6 +46,7 @@
 import org.jacodb.ets.model.EtsNullConstant
 import org.jacodb.ets.model.EtsNullishCoalescingExpr
 import org.jacodb.ets.model.EtsNumberConstant
+import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsOrExpr
 import org.jacodb.ets.model.EtsParameterRef
 import org.jacodb.ets.model.EtsPostDecExpr
@@ -77,15 +80,16 @@
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.allocateArray
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
-import org.usvm.isTrue
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
 import org.usvm.machine.TsVirtualMethodCallStmt
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.interpreter.isInitialized
@@ -590,6 +594,9 @@
 
     override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
         val array = resolve(value.array)?.asExpr(addressSort) ?: return null
+
+        checkUndefinedOrNullPropertyRead(array) ?: return null
+
         val index = resolve(value.index)?.asExpr(fp64Sort) ?: return null
         val bvIndex = mkFpToBvExpr(
             roundingMode = fpRoundingModeSortDefaultValue(),
@@ -598,20 +605,73 @@
             isSigned = true,
         ).asExpr(sizeSort)
 
-        val lValue = mkArrayIndexLValue(
-            sort = addressSort,
-            ref = array,
-            index = bvIndex,
-            type = value.array.type as EtsArrayType
-        )
-        val expr = scope.calcOnState { memory.read(lValue) }
+        val arrayType = value.array.type as? EtsArrayType
+            ?: error("Expected EtsArrayType, but got ${value.array.type}")
+        val sort = typeToSort(arrayType.elementType)
+
+        val lengthLValue = mkArrayLengthLValue(array, arrayType)
+        val length = scope.calcOnState { memory.read(lengthLValue) }
+
+        checkNegativeIndexRead(bvIndex) ?: return null
+        checkReadingInRange(bvIndex, length) ?: return null
+
+        val expr = if (sort is TsUnresolvedSort) {
+            // Concrete arrays with the unresolved sort should consist of fake objects only.
+            if (array is UConcreteHeapRef) {
+                // Read a fake object from the array.
+                val lValue = mkArrayIndexLValue(
+                    sort = addressSort,
+                    ref = array,
+                    index = bvIndex,
+                    type = arrayType
+                )
+
+                scope.calcOnState { memory.read(lValue) }
+            } else {
+                // If the array is not concrete, we need to allocate a fake object
+                val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
+                val boolLValue = mkArrayIndexLValue(boolSort, array, bvIndex, boolArrayType)
+
+                val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
+                val fpLValue = mkArrayIndexLValue(fp64Sort, array, bvIndex, numberArrayType)
+
+                val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+                val refLValue = mkArrayIndexLValue(addressSort, array, bvIndex, unknownArrayType)
+
+                scope.calcOnState {
+                    val boolValue = memory.read(boolLValue)
+                    val fpValue = memory.read(fpLValue)
+                    val refValue = memory.read(refLValue)
+
+                    // Read an object from the memory at first,
+                    // we don't need to recreate it if it is already a fake object.
+                    val fakeObj = if (refValue.isFakeObject()) {
+                        refValue
+                    } else {
+                        mkFakeValue(scope, boolValue, fpValue, refValue).also {
+                            lValuesToAllocatedFakeObjects += refLValue to it
+                        }
+                    }
+
+                    memory.write(refLValue, fakeObj.asExpr(addressSort), guard = trueExpr)
 
-        check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
+                    fakeObj
+                }
+            }
+        } else {
+            val lValue = mkArrayIndexLValue(
+                sort = sort,
+                ref = array,
+                index = bvIndex,
+                type = arrayType
+            )
+            scope.calcOnState { memory.read(lValue) }
+        }
 
         return expr
     }
 
-    private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
+    fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
         val neqNull = mkAnd(
             mkHeapRefEq(instance, mkUndefinedValue()).not(),
             mkHeapRefEq(instance, mkTsNullValue()).not()
@@ -623,6 +683,24 @@
         )
     }
 
+    fun checkNegativeIndexRead(index: UExpr<TsSizeSort>) = with(ctx) {
+        val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0))
+
+        scope.fork(
+            condition,
+            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+        )
+    }
+
+    fun checkReadingInRange(index: UExpr<TsSizeSort>, length: UExpr<TsSizeSort>) = with(ctx) {
+        val condition = mkBvSignedLessExpr(index, length)
+
+        scope.fork(
+            condition,
+            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+        )
+    }
+
     private fun allocateException(type: EtsType): (TsState) -> Unit = { state ->
         val address = state.memory.allocConcrete(type)
         state.throwExceptionWithoutStackFrameDrop(address, type)
@@ -675,9 +753,10 @@
                 val fakeRef = if (ref.isFakeObject()) {
                     ref
                 } else {
-                    mkFakeValue(scope, bool, fp, ref)
+                    mkFakeValue(scope, bool, fp, ref).also {
+                        lValuesToAllocatedFakeObjects += refLValue to it
+                    }
                 }
-
                 memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
 
                 fakeRef
@@ -696,33 +775,47 @@
         // TODO It is a hack for array's length
         if (value.field.name == "length") {
             if (value.instance.type is EtsArrayType) {
-                val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
+                val arrayType = value.instance.type as EtsArrayType
+                val lengthLValue = mkArrayLengthLValue(instanceRef, arrayType)
                 val length = scope.calcOnState { memory.read(lengthLValue) }
+                scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
+
                 return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
             }
 
             // TODO: handle "length" property for arrays inside fake objects
             if (instanceRef.isFakeObject()) {
                 val fakeType = instanceRef.getFakeType(scope)
-                // TODO: replace '.isTrue' with fork or assert
-                if (fakeType.refTypeExpr.isTrue) {
-                    val refLValue = getIntermediateRefLValue(instanceRef.address)
-                    val obj = scope.calcOnState { memory.read(refLValue) }
-                    // TODO: fix array type. It should be the same as the type used when "writing" the length.
-                    //  However, current value.instance typically has 'unknown' type, and the best we can do here is
-                    //  to pretend that this is an array-like object (with "array length", not just "length" field),
-                    //  and "cast" instance to "unknown[]". The same could be done for any length writes, making
-                    //  the array type (for length) consistent (unknown everywhere), but less precise.
-                    val lengthLValue = mkArrayLengthLValue(obj, EtsArrayType(EtsUnknownType, 1))
-                    val length = scope.calcOnState { memory.read(lengthLValue) }
-                    return mkBvToFpExpr(
-                        fp64Sort,
-                        fpRoundingModeSortDefaultValue(),
-                        length.asExpr(sizeSort),
-                        signed = true
-                    )
+
+                // If we want to get length from a fake object, we assume that it is an array.
+                scope.doWithState { pathConstraints += fakeType.refTypeExpr }
+
+                val refLValue = getIntermediateRefLValue(instanceRef.address)
+                val obj = scope.calcOnState { memory.read(refLValue) }
+
+                val type = value.instance.type
+                val arrayType = type as? EtsArrayType ?: run {
+                    check(type is EtsAnyType || type is EtsUnknownType) {
+                        "Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type"
+                    }
+
+                    // We don't know the type of the array, since it is a fake object
+                    // If we'd know the type, we would have used it instead of creating a fake object
+                    EtsArrayType(EtsUnknownType, dimensions = 1)
                 }
+                val lengthLValue = mkArrayLengthLValue(obj, arrayType)
+                val length = scope.calcOnState { memory.read(lengthLValue) }
+
+                scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
+
+                return mkBvToFpExpr(
+                    fp64Sort,
+                    fpRoundingModeSortDefaultValue(),
+                    length.asExpr(sizeSort),
+                    signed = true
+                )
+
             }
         }
 
         return handleFieldRef(value.instance, instanceRef, value.field, hierarchy)
@@ -779,6 +872,12 @@
     }
 
     override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? = with(ctx) {
+        val arrayType = expr.type
+
+        require(arrayType is EtsArrayType) {
+            "Expected EtsArrayType in newArrayExpr, but got ${arrayType::class.simpleName}"
+        }
+
         scope.calcOnState {
             val size = resolve(expr.size) ?: return@calcOnState null
 
@@ -809,7 +908,10 @@
                 blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
             )
 
-            val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type
+            if (arrayType.elementType is EtsArrayType) {
+                TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287")
+            }
+
             val address = memory.allocateArray(arrayType, sizeSort, bvSize)
 
             address

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

@@ -73,18 +73,30 @@ class TsVoidSort(ctx: TsContext) : USort(ctx) {
     }
 }
 
-fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
+fun UExpr<*>.toConcreteBoolValue(): Boolean = when (this) {
     ctx.trueExpr -> true
     ctx.falseExpr -> false
-    else -> error("Cannot extract boolean from $this")
+    else -> error("Cannot extract Boolean from $this")
 }
 
-fun extractInt(expr: UExpr<out USort>): Int =
-    (expr as? KBitVec32Value)?.intValue ?: error("Cannot extract int from $expr")
-
-fun UExpr<out USort>.extractDouble(): Double {
+/**
+ * Extracts a double value from [this] expression if possible.
+ * Otherwise, throws an error.
+ */
+fun UExpr<*>.extractDouble(): Double {
     if (this@extractDouble is KFp64Value) {
         return value
     }
-    error("Cannot extract double from $this")
+    error("Cannot extract Double from $this")
+}
+
+/**
+ * Extracts an integer value from [this] expression if possible.
+ * Otherwise, throws an error.
+ */
+fun UExpr<*>.extractInt(): Int {
+    if (this@extractInt is KBitVec32Value) {
+        return intValue
+    }
+    error("Cannot extract Int from $this")
 }