[TS] Add symbolic UTF-16 string storage and Array primitives

usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt

@@ -1,6 +1,7 @@
 package org.usvm.machine.call
 
 import org.jacodb.ets.model.EtsAnyType
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsLocal
@@ -48,3 +49,7 @@ internal fun EtsType.isBuiltinDateGlobalType(): Boolean = this is EtsFunctionTyp
     signature.name.isEmpty() &&
     signature.parameters.isEmpty() &&
     signature.returnType == EtsStringType
+
+internal fun EtsType.isBuiltinArrayGlobalType(): Boolean = this is EtsFunctionType &&
+    signature.returnType is EtsArrayType &&
+    signature.enclosingClass.file == EtsClassSignature.UNKNOWN.file

usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt

@@ -2,6 +2,7 @@ package org.usvm.machine.call.intrinsic
 
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsArrayType
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.machine.call.TsEtsIrUnknownCallModel
 import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact
@@ -13,6 +14,7 @@ import org.usvm.machine.call.TsUnknownCallModel
 import org.usvm.machine.call.TsUnknownCallTarget
 import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
 import org.usvm.util.arrayStorageType
+import org.usvm.util.isUnmodifiedDenseInputArray
 
 /** Built-in Array algorithms implemented by ordinary TypeScript bodies. */
 internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
@@ -48,22 +50,24 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                     falseExpr
                 } else {
                     val elementSort = typeToSort(receiverType.elementType)
+                    val hasNoMissingSlots = array is UConcreteHeapRef &&
+                        state.isUnmodifiedDenseInputArray(array, receiverType)
                     val excludesMissingSlot = when {
                         searchElement == mkUndefinedValue() &&
                             (
                                 call.callee.name in setOf("indexOf", "lastIndexOf") ||
                                     elementSort == fp64Sort || elementSort == boolSort
-                                ) -> falseExpr
+                                ) -> mkBool(hasNoMissingSlots)
 
                         elementSort == fp64Sort && searchElement?.sort == fp64Sort -> {
                             val searchNumber = searchElement.asExpr(fp64Sort)
                             val zero = mkFp64(0.0)
 
-                            mkNot(mkFpEqualExpr(searchNumber, zero))
+                            mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, zero)))
                         }
 
                         elementSort == boolSort && searchElement?.sort == boolSort -> {
-                            searchElement.asExpr(boolSort)
+                            mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort))
                         }
 
                         else -> trueExpr

usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt

@@ -0,0 +1,88 @@
+package org.usvm.machine.call.intrinsic
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.call.TsUnknownCallModelCompletion
+import org.usvm.machine.call.TsUnknownCallModelExecution
+import org.usvm.machine.call.TsUnknownCallModelSuccessor
+import org.usvm.machine.call.TsUnknownCallTarget
+import org.usvm.machine.state.TsState
+
+/** Exact `Array.isArray` semantics for the genuine global `Array` built-in. */
+internal object TsArrayIsArrayIntrinsicModel : TsBuiltInUnknownCallModel {
+    const val MODEL_ID: String = "ts.array.isArray"
+
+    private val anyArrayType = EtsArrayType(elementType = EtsUnknownType, dimensions = 1)
+
+    override val id: String = MODEL_ID
+    override val target = TsUnknownCallTarget(
+        methodName = "isArray",
+    )
+
+    override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
+        if (!call.hasGlobalArrayOwner()) {
+            return null
+        }
+
+        val value = when {
+            call.arguments.isEmpty() -> return state.normalExecution(state.ctx.falseExpr)
+            else -> call.arguments.first().resolved ?: return null
+        }
+        val result = state.isArray(value)
+
+        return state.normalExecution(result)
+    }
+
+    private fun TsUnknownCall.hasGlobalArrayOwner(): Boolean {
+        val owner = receiver?.source as? EtsLocal ?: return false
+        val ownerType = owner.type as? EtsFunctionType ?: return false
+        val signatureFile = ownerType.signature.enclosingClass.file
+
+        return owner.name == "Array" &&
+            ownerType.signature.returnType is EtsArrayType &&
+            signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT &&
+            signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT
+    }
+
+    private fun TsState.isArray(value: UExpr<*>) = with(ctx) {
+        when {
+            value.isFakeObject() -> {
+                val fakeType = value.getFakeType(memory)
+                val reference = value.extractRef(memory)
+
+                mkAnd(
+                    fakeType.refTypeExpr,
+                    isNonNullArrayReference(reference),
+                )
+            }
+
+            value.sort == addressSort -> isNonNullArrayReference(value.asExpr(addressSort))
+            else -> falseExpr
+        }
+    }
+
+    private fun TsState.isNonNullArrayReference(reference: UHeapRef): UBoolExpr = with(ctx) {
+        val isDefined = mkNot(mkEq(reference, mkUndefinedValue()))
+        val isNonNull = mkNot(mkEq(reference, mkTsNullValue()))
+
+        mkAnd(isDefined, isNonNull, memory.types.evalIsSubtype(reference, anyArrayType))
+    }
+
+    private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) {
+        val successor = TsUnknownCallModelSuccessor(
+            guard = trueExpr,
+            completion = TsUnknownCallModelCompletion.Normal { result },
+        )
+
+        TsUnknownCallModelExecution(successors = listOf(successor))
+    }
+
+    private const val UNKNOWN_SIGNATURE_COMPONENT: String = "%unk"
+}

usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt

@@ -21,9 +21,11 @@ import org.usvm.machine.call.TsUnknownCallTarget
 import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
 import org.usvm.machine.state.TsState
 import org.usvm.sizeSort
+import org.usvm.util.copyStringRange
 import org.usvm.util.mkStringBackingElementLValue
 import org.usvm.util.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
+import org.usvm.util.stringFromCodeUnit
 
 /** Built-in String algorithms implemented by ordinary TypeScript bodies. */
 internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
@@ -94,11 +96,48 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         }
     }
 
+    private val sliceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
+        val inputs = call.resolvedInstanceInputs() ?: return@TsEtsIrUnknownCallModelInputAdapter null
+        val receiver = inputs.firstOrNull()?.takeIf { it.sort == state.ctx.addressSort }
+            ?: return@TsEtsIrUnknownCallModelInputAdapter null
+        val arguments = inputs.drop(1)
+        if (arguments.size > 2) {
+            return@TsEtsIrUnknownCallModelInputAdapter null
+        }
+
+        fun numericOrDefault(index: Int, default: UExpr<*>): UExpr<*> {
+            val value = arguments.getOrNull(index) ?: return default
+            return when {
+                value == state.ctx.mkUndefinedValue() -> default
+                value.sort == state.ctx.fp64Sort -> value
+                else -> return default
+            }
+        }
+
+        val start = numericOrDefault(index = 0, default = state.ctx.mkFp64(0.0))
+        val end = numericOrDefault(
+            index = 1,
+            default = state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort),
+        )
+        if (arguments.any { value -> value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort }) {
+            return@TsEtsIrUnknownCallModelInputAdapter null
+        }
+
+        listOf(receiver, start, end)
+    }
+
+    private val noArgumentsAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call ->
+        if (call.arguments.isNotEmpty()) {
+            null
+        } else {
+            call.resolvedInstanceInputs()
+        }
+    }
+
     private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs ->
         with(state.ctx) {
             val receiver = inputs.firstOrNull()
-            // Symbolic String parameters do not initialize the backing character array yet.
-            if (receiver !is UConcreteHeapRef || getStringConstantValue(receiver) == null) {
+            if (receiver !is UConcreteHeapRef || receiver.hasFakeValueBranch()) {
                 falseExpr
             } else {
                 state.memory.types.evalTypeEquals(receiver, EtsStringType)
@@ -110,9 +149,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         with(state.ctx) {
             val receiver = inputs.getOrNull(0)
             val searchString = inputs.getOrNull(1)
-            val receiverIsConstant = receiver is UConcreteHeapRef && getStringConstantValue(receiver) != null
-            val searchStringIsConstant =
-                searchString is UConcreteHeapRef && getStringConstantValue(searchString) != null
+            val receiverIsConstant = receiver is UConcreteHeapRef && !receiver.hasFakeValueBranch()
+            val searchStringIsConstant = searchString is UConcreteHeapRef && !searchString.hasFakeValueBranch()
 
             if (!receiverIsConstant || !searchStringIsConstant) {
                 falseExpr
@@ -125,6 +163,38 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         }
     }
 
+    private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
+        with(state.ctx) {
+            val receiverGuard = receiverDomain.evaluate(state, call, inputs)
+            val receiver = inputs.firstOrNull() as? UConcreteHeapRef
+                ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr
+            val characters = state.memory.read(mkStringBackingLValue(receiver))
+                .asExpr(addressSort)
+            val length = state.memory.read(mkStringBackingLengthLValue(characters))
+            val characterGuards = (0 until MAX_ASCII_CASE_LENGTH).map { index ->
+                val symbolicIndex = mkBv(index)
+                val codeUnit = state.memory.read(
+                    mkStringBackingElementLValue(ref = characters, index = symbolicIndex)
+                )
+                val isOutsideLength = mkBvSignedGreaterOrEqualExpr(symbolicIndex, length)
+                val asciiMax = mkBv(ASCII_MAX_CODE_UNIT, bv16Sort)
+                val isAscii = mkBvUnsignedLessOrEqualExpr(codeUnit, asciiMax)
+                mkOr(
+                    isOutsideLength,
+                    isAscii,
+                )
+            }
+
+            val maximumLength = mkBv(MAX_ASCII_CASE_LENGTH)
+            val withinLengthLimit = mkBvSignedLessOrEqualExpr(length, maximumLength)
+            mkAnd(
+                receiverGuard,
+                withinLengthLimit,
+                *characterGuards.toTypedArray(),
+            )
+        }
+    }
+
     private val receiverAndConcreteIndexDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
         if (inputs.getOrNull(1) !is KFp64Value) {
             state.ctx.falseExpr
@@ -177,6 +247,24 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 inputAdapter = optionalEndPositionAdapter,
                 domainGuard = receiverAndSearchDomain,
             ),
+            sourceModel(
+                id = "ts.string.slice",
+                methodName = "slice",
+                inputAdapter = sliceAdapter,
+                domainGuard = receiverDomain,
+            ),
+            sourceModel(
+                id = "ts.string.toUpperCase",
+                methodName = "toUpperCase",
+                inputAdapter = noArgumentsAdapter,
+                domainGuard = asciiReceiverDomain,
+            ),
+            sourceModel(
+                id = "ts.string.toLowerCase",
+                methodName = "toLowerCase",
+                inputAdapter = noArgumentsAdapter,
+                domainGuard = asciiReceiverDomain,
+            ),
             primitiveModel(
                 methodName = "length",
                 arity = 1,
@@ -192,6 +280,11 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 arity = 1,
                 implementation = ::stringFromCodeUnit,
             ),
+            primitiveModel(
+                methodName = "copyRange",
+                arity = 3,
+                implementation = ::stringCopyRange,
+            ),
         )
     }
 
@@ -214,9 +307,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
             add(MATH_FLOOR_MODEL_ID)
             add(PRIMITIVE_LENGTH_ID)
             add(PRIMITIVE_CODE_UNIT_AT_ID)
-            if (methodName == "charAt") {
+            if (methodName in setOf("charAt", "toUpperCase", "toLowerCase")) {
                 add(PRIMITIVE_FROM_CODE_UNIT_ID)
             }
+            if (methodName == "slice") {
+                add(PRIMITIVE_COPY_RANGE_ID)
+            }
         },
     )
 
@@ -305,16 +401,58 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         state: TsState,
         inputs: List<UExpr<*>>,
     ): TsUnknownCallModelExecution? = with(state.ctx) {
-        val code = inputs.singleOrNull() as? KFp64Value ?: return null
+        val code = inputs.singleOrNull()?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
         val successor = TsUnknownCallModelSuccessor(
             guard = trueExpr,
             completion = TsUnknownCallModelCompletion.Normal {
-                mkInitializedStringConstant(code.value.toInt().toChar().toString())
+                if (code is KFp64Value) {
+                    mkInitializedStringConstant(code.value.toInt().toChar().toString())
+                } else {
+                    stringFromCodeUnit(code)
+                }
+            },
+        )
+
+        TsUnknownCallModelExecution(
+            successors = listOf(successor),
+        )
+    }
+
+    private fun stringCopyRange(
+        state: TsState,
+        inputs: List<UExpr<*>>,
+    ): TsUnknownCallModelExecution? = with(state.ctx) {
+        val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null
+        val start = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
+        val end = inputs.getOrNull(2)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
+        if (receiver.hasFakeValueBranch()) {
+            return null
+        }
+
+        val from = mkFpToBvExpr(
+            roundingMode = fpRoundingModeSortDefaultValue(),
+            value = start,
+            bvSize = sizeSort.sizeBits.toInt(),
+            isSigned = true,
+        ).asExpr(sizeSort)
+        val to = mkFpToBvExpr(
+            roundingMode = fpRoundingModeSortDefaultValue(),
+            value = end,
+            bvSize = sizeSort.sizeBits.toInt(),
+            isSigned = true,
+        ).asExpr(sizeSort)
+        val length = mkBvSubExpr(to, from)
+        val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType)
+        val successor = TsUnknownCallModelSuccessor(
+            guard = receiverIsString,
+            completion = TsUnknownCallModelCompletion.Normal {
+                copyStringRange(receiver = receiver, from = from, length = length)
             },
         )
 
         TsUnknownCallModelExecution(
             successors = listOf(successor),
+            residualGuard = receiverIsString.takeUnless { it == trueExpr }?.let(::mkNot),
         )
     }
 
@@ -366,5 +504,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
     private const val PRIMITIVE_LENGTH_ID = "ts.string.primitive.length"
     private const val PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt"
     private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit"
+    private const val PRIMITIVE_COPY_RANGE_ID = "ts.string.primitive.copyRange"
     private const val MATH_FLOOR_MODEL_ID = "ts.math.floor"
+    private const val MAX_ASCII_CASE_LENGTH = 16
+    private const val ASCII_MAX_CODE_UNIT = 0x7f
 }