[TS] Model Array and Error constructors and String.replaceAll

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt

@@ -163,6 +163,7 @@ internal class CurrentTsCallsSymbolicEngine(
             maxArraySize = maxOf(TsOptions().maxArraySize, inputCapacity),
             unknownCallModelSelection = modelSelection,
             unknownCallFallback = request.profile.fallback,
+            eraseTypeAssertions = true,
         )
         val symbolicInputs = CallsSymbolicInputs(
             inputs = request.function.inputs,

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsTypeAssertionTest.kt

@@ -0,0 +1,36 @@
+package org.usvm.ts.calls
+
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.PropertyInput
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertNotNull
+
+internal class CurrentTsCallsTypeAssertionTest : CurrentTsCallsSymbolicEngineTestSupport() {
+    @Test
+    fun `Calls erases type assertions and replays the original runtime number`() {
+        val fixture = fixture(
+            source = """
+                export function assertedNumber(value: number): boolean {
+                  const asserted = value as unknown as string;
+                  if (typeof asserted === "number" && asserted === 42) {
+                    return true;
+                  }
+                  return false;
+                }
+            """.trimIndent(),
+            exportName = "assertedNumber",
+            inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())),
+            targetStatement = "return true;",
+        )
+
+        val result = fixture.search(modelIds = emptySet())
+
+        val inputs = assertNotNull(result.inputs, result.toString())
+        val value = assertIs<JsConcreteValue.Number>(inputs.single()).toDouble()
+        assertEquals(42.0, value)
+        fixture.assertReplayConfirmed(inputs)
+    }
+}

usvm-ts/UNKNOWN_CALL_MODELS.md

@@ -67,14 +67,17 @@ The built-in catalog includes the following public APIs and their internal stora
 | --- | --- | --- |
 | `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. |
 | `ts.array.isArray` | Kotlin runtime-type primitive | The genuine global Array predicate, including null, undefined and fake-value wrappers. |
+| `ts.array.fromLength` | TypeScript/EtsIR body with a heap-allocation primitive | Genuine callable `Array(length)` with one numeric argument. Valid lengths up to 16 allocate holes that read as `undefined`; larger valid lengths use fallback. |
 | `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. |
 | `ts.array.includes`, `ts.array.indexOf`, `ts.array.lastIndexOf` | TypeScript/EtsIR bodies | One-dimensional arrays and numeric positions, with the missing-slot exclusions below. |
-| `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push, these operations require a current dense-array proof. |
+| `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push and full-range `fill(value)`, these operations require a current dense-array proof. |
 | `ts.string.charAt`, `ts.string.charCodeAt`, `ts.string.includes`, `ts.string.indexOf`, `ts.string.lastIndexOf`, `ts.string.startsWith`, `ts.string.endsWith` | TypeScript/EtsIR bodies | Strings in initialized UTF-16 storage, including symbolic code units and numeric positions. |
 | `ts.string.slice`, `ts.string.substring`, `ts.string.trim`, `ts.string.trimStart`, `ts.string.trimEnd` | TypeScript/EtsIR bodies | UTF-16 range copying; substring clamps/swaps bounds, and trim uses the ECMAScript whitespace set. |
+| `ts.string.replaceAll` | TypeScript/EtsIR body | String receiver, string search and string replacement; non-overlapping UTF-16 matches, empty search and ECMAScript dollar substitutions for a dollar sign, the match, its prefix and its suffix. RegExp, callbacks and argument coercions use fallback. |
 | `ts.string.toLowerCase`, `ts.string.toUpperCase` | TypeScript/EtsIR bodies | ASCII strings of at most 16 code units; other strings use residual fallback. |
 | `ts.math.abs`, `ts.math.ceil`, `ts.math.floor`, `ts.math.max`, `ts.math.min`, `ts.math.round`, `ts.math.sqrt`, `ts.math.trunc` | Kotlin FP primitives | Numeric arguments; dynamic coercions use fallback. |
 | `ts.number.isFinite`, `ts.number.isInteger`, `ts.number.isNaN`, `ts.number.isSafeInteger` | Kotlin FP/type primitives | Non-coercing Number predicates, including runtime-kind guards. |
+| `ts.error.constructor` | TypeScript/EtsIR body | Genuine `new Error(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside this model. |
 | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. |
 
 Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are
@@ -105,10 +108,19 @@ modeled array methods can still use fallback after its first mutation or copy.
 named-property writes or unsupported length growth. These events are separate from unknown-call model decisions.
 Exhaustion after a runtime limitation does not establish that a source target is unreachable; a reached target
 still requires original-source replay.
+named-property access, unsupported length growth, or assigning a runtime kind absent from a typed array's storage.
+Reads may return an element or `undefined`; subsequent numeric operations and typed writes preserve that runtime-kind
+guard. TypeScript `as` and angle-bracket assertions are erased only with `TsOptions(eraseTypeAssertions = true)`
+and never change a value or constrain its runtime kind in that mode. The default retains the existing ETS cast
+constraints and unsupported-cast behavior. The TypeScript Calls engine explicitly enables erasure.
+These events are separate from unknown-call model decisions.
+The Calls runner writes them synchronously and reports `RUNTIME_LIMITATION` when search exhausts after such a stop
+without reaching the target. An actual timeout remains `TIMEOUT`; a reached target still requires original-source replay.
 
 Calls preflight checks input binding and source/IR target mapping before choosing a model/fallback profile. Excluded functions remain in the corpus support ledger. Comparative runs use a frozen common
 target set; failures discovered after that freeze remain scheduled failures. The analysis budget is 30 seconds per
-target and seed; JVM/frontend startup and original-source replay have separate recorded limits.
+target, profile and seed; JVM/frontend startup and original-source replay have separate recorded limits. Readiness
+traverses reachable same-file callees and the initializers triggered by their static-field accesses.
 
 ### `unknownCallFallback`
 

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

@@ -98,6 +98,7 @@ enum class TsRuntimeFeatureLimitationReason {
     ARRAY_NAMED_PROPERTY_WRITE,
     ARRAY_INDEX_GROWTH,
     ARRAY_ITERATOR_UNSUPPORTED,
+    ARRAY_ELEMENT_KIND_WRITE,
     ARRAY_LENGTH_CAPACITY,
     ARRAY_LENGTH_GROWTH,
     STRING_ITERATOR_UNSUPPORTED,

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

@@ -27,6 +27,8 @@ data class TsOptions(
     val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH,
     /** Fixed experiment clock used by `Date.now()` and `new Date()`; `null` leaves those calls unsupported. */
     val dateNowMilliseconds: Double? = null,
+    /** Erase TypeScript assertions; false retains the existing ETS cast constraints and unsupported casts. */
+    val eraseTypeAssertions: Boolean = false,
 ) {
     init {
         val isValidDateNow = dateNowMilliseconds == null ||

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

@@ -2,11 +2,16 @@ package org.usvm.machine.call.intrinsic
 
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.cast
+import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
+import org.usvm.api.initializeArray
 import org.usvm.api.initializeArrayLength
 import org.usvm.machine.call.TsEtsIrUnknownCallModel
 import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact
@@ -21,10 +26,14 @@ import org.usvm.machine.call.TsUnknownCallModelSuccessor
 import org.usvm.machine.call.TsUnknownCallTarget
 import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
 import org.usvm.machine.call.resolvedInstanceInputs
+import org.usvm.machine.expr.mkFpToUint32AfterValidation
+import org.usvm.machine.expr.mkValidArrayLength
 import org.usvm.machine.state.TsState
+import org.usvm.machine.types.TsUnresolvedArrayKind
 import org.usvm.sizeSort
 import org.usvm.util.arrayStorageType
 import org.usvm.util.componentType
+import org.usvm.util.initializeArrayKind
 import org.usvm.util.isUnmodifiedDenseInputArray
 import org.usvm.util.mkArrayLengthLValue
 
@@ -122,8 +131,9 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
     private val fillDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
         val (array, arrayType) = state.concreteArray(call, inputs)
             ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
-        val isDenseInput = state.isUnmodifiedDenseInputArray(array, arrayType)
-        if (!isDenseInput) {
+        val fillsWholeArray = call.arguments.size == 1
+        val hasKnownSlotValues = fillsWholeArray || state.isUnmodifiedDenseInputArray(array, arrayType)
+        if (!hasKnownSlotValues) {
             return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr
         }
 
@@ -295,8 +305,31 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         if (call.arguments.isEmpty()) call.resolvedInstanceInputs(maxArgumentCount = call.arguments.size) else null
     }
 
+    private val arrayConstructorAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
+        if (!call.hasGlobalArrayConstructorShape() || call.arguments.size != 1) {
+            return@TsEtsIrUnknownCallModelInputAdapter null
+        }
+
+        val length = call.arguments.single().resolved
+            ?.takeIf { value -> value.sort == state.ctx.fp64Sort }
+            ?: return@TsEtsIrUnknownCallModelInputAdapter null
+        listOf(length)
+    }
+
     override val models: List<TsUnknownCallModel> by lazy {
+        val arrayConstructorModel = TsEtsIrUnknownCallModel(
+            id = ARRAY_FROM_LENGTH_ID,
+            target = TsUnknownCallTarget(
+                methodName = "Array",
+                failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND,
+            ),
+            artifact = artifact("fromLength"),
+            inputAdapter = arrayConstructorAdapter,
+            requiredModelIds = setOf(PRIMITIVE_ALLOCATE_ID),
+        )
+
         listOf(
+            arrayConstructorModel,
             sourceModel(
                 id = "ts.array.pop",
                 methodName = "pop",
@@ -357,6 +390,11 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 arity = 2,
                 implementation = ::growArray,
             ),
+            primitiveModel(
+                methodName = "allocate",
+                arity = 1,
+                implementation = ::allocateArray,
+            ),
             primitiveModel(
                 methodName = "allocateLike",
                 arity = 2,
@@ -500,6 +538,60 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
+    private fun allocateArray(
+        state: TsState,
+        inputs: List<UExpr<*>>,
+    ): TsUnknownCallModelExecution? = with(state.ctx) {
+        val fpLength = inputs.singleOrNull()
+            ?.takeIf { value -> value.sort == fp64Sort }
+            ?.asExpr(fp64Sort)
+            ?: return null
+        val validLength = mkValidArrayLength(fpLength)
+        val maximumLength = mkFp64(MAX_SOURCE_ARRAY_LENGTH.toDouble())
+        val withinModelCapacity = mkFpLessOrEqualExpr(
+            fpLength,
+            maximumLength,
+        )
+        val supportedLength = mkAnd(validLength, withinModelCapacity)
+        val length = mkFpToUint32AfterValidation(fpLength, validLength).asExpr(sizeSort)
+        val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+
+        // The model covers only valid, bounded one-number lengths. All other inputs remain residual.
+        val validSuccessor = TsUnknownCallModelSuccessor(
+            guard = supportedLength,
+            completion = TsUnknownCallModelCompletion.Normal {
+                val descriptor = arrayDescriptorOf(arrayType)
+                val result = memory.allocConcrete(arrayType)
+                val undefinedSlots = List(MAX_SOURCE_ARRAY_LENGTH) { mkUndefinedValue() }
+                memory.initializeArray(
+                    arrayHeapRef = result,
+                    type = descriptor,
+                    sort = addressSort,
+                    sizeSort = sizeSort,
+                    contents = undefinedSlots.asSequence(),
+                )
+                TsUnresolvedArrayKind.entries.forEach { kind ->
+                    initializeArrayKind(
+                        array = result,
+                        kind = kind,
+                        values = List(MAX_SOURCE_ARRAY_LENGTH) { falseExpr },
+                    )
+                }
+                memory.initializeArrayLength(
+                    arrayHeapRef = result,
+                    type = descriptor,
+                    sizeSort = sizeSort,
+                    count = length,
+                )
+                result
+            },
+        )
+        TsUnknownCallModelExecution(
+            successors = listOf(validSuccessor),
+            residualGuard = mkNot(supportedLength),
+        )
+    }
+
     private fun allocateArrayLike(
         state: TsState,
         inputs: List<UExpr<*>>,
@@ -545,7 +637,31 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         )
     }
 
+    private fun TsUnknownCall.hasGlobalArrayConstructorShape(): Boolean {
+        val owner = receiver?.source as? EtsLocal ?: return false
+        val ownerSignature = (owner.type as? EtsFunctionType)?.signature ?: return false
+        val ownerParameter = ownerSignature.parameters.singleOrNull() ?: return false
+        val ownerReturnType = ownerSignature.returnType as? EtsArrayType ?: return false
+        val callReturnType = resultType as? EtsArrayType ?: return false
+        val signatureFile = ownerSignature.enclosingClass.file
+
+        return owner.name == "Array" &&
+            signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT &&
+            signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT &&
+            ownerSignature.name.isEmpty() &&
+            ownerParameter.type == EtsNumberType &&
+            ownerParameter.isOptional &&
+            !ownerParameter.isRest &&
+            ownerReturnType.elementType == EtsAnyType &&
+            ownerReturnType.dimensions == 1 &&
+            callReturnType.elementType == EtsAnyType &&
+            callReturnType.dimensions == 1
+    }
+
     private const val MATH_FLOOR_MODEL_ID = "ts.math.floor"
+    private const val ARRAY_FROM_LENGTH_ID = "ts.array.fromLength"
     private const val PRIMITIVE_GROW_ID = "ts.array.primitive.grow"
+    private const val PRIMITIVE_ALLOCATE_ID = "ts.array.primitive.allocate"
     private const val PRIMITIVE_ALLOCATE_LIKE_ID = "ts.array.primitive.allocateLike"
+    private const val UNKNOWN_SIGNATURE_COMPONENT = "%unk"
 }