[TS] Recognize strict optional Array constructor signatures

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

@@ -10,6 +10,8 @@ import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
+import org.jacodb.ets.model.EtsUndefinedType
+import org.jacodb.ets.model.EtsUnionType
 import org.jacodb.ets.model.EtsUnknownType
 import org.jacodb.ets.model.EtsValue
 import org.usvm.UConcreteHeapRef
@@ -44,10 +46,14 @@ private fun EtsFunctionType.isBuiltinNumberType(): Boolean {
 private fun EtsFunctionType.isBuiltinArrayType(): Boolean {
     val parameter = signature.parameters.singleOrNull() ?: return false
     val arrayType = signature.returnType as? EtsArrayType ?: return false
+    val lengthTypes = (parameter.type as? EtsUnionType)?.types?.toSet()
+    val acceptsNumericLength = parameter.type == EtsNumberType ||
+        lengthTypes == setOf(EtsNumberType, EtsUndefinedType)
+
     return signature.enclosingClass == EtsClassSignature.UNKNOWN &&
         signature.name.isEmpty() &&
         arrayType.elementType == EtsAnyType && arrayType.dimensions == 1 &&
-        parameter.type == EtsNumberType && parameter.isOptional && !parameter.isRest
+        acceptsNumericLength && parameter.isOptional && !parameter.isRest
 }
 
 private fun EtsValue.isLegacyBuiltinGlobal(

usvm-ts/src/test/kotlin/org/usvm/machine/expr/StrictCollectionOperationsTest.kt

@@ -0,0 +1,66 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.utils.loadEtsProjectAutoConvert
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.Test
+
+class StrictCollectionOperationsTest : TsMethodTestRunner() {
+    override val scene = loadEtsProjectAutoConvert(
+        getResourcePath("/models/strict-collections"),
+        useArkAnalyzerTypeInference = null,
+    )
+    override val tsOptions = TsOptions(eraseTypeAssertions = true)
+
+    override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, machineOptions ->
+        TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+    }
+
+    @TempDir
+    lateinit var directory: Path
+
+    init {
+        options = options.copy(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            stopOnCoverage = 0,
+            throwExceptionOnStepFailure = true,
+        )
+    }
+
+    @Test
+    fun `Array from accepts the native strict null checks constructor signature`() {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = getMethod(methodName = "nativeFromKeys", className = "StrictCollections"),
+            { result -> result.number == 1.0 },
+            invariants = arrayOf({ result -> result.number == 1.0 }),
+        )
+    }
+
+    @Test
+    fun `Node confirms strict project collection behavior`() {
+        val source = getResourcePath("/models/strict-collections/StrictCollections.ts").readText()
+
+        assertNodeReplay(
+            source = source + "if (StrictCollections.nativeFromKeys() !== 1) throw Error('strict from');",
+            directory = directory,
+            name = "native-strict-collection-operations",
+            timeoutMessage = "Native strict collection regression timed out",
+        )
+    }
+}

usvm-ts/src/test/resources/models/strict-collections/StrictCollections.ts

@@ -0,0 +1,8 @@
+export class StrictCollections {
+    static nativeFromKeys(): number {
+        const map = new Map<string, number>();
+        map.set('a', 3).set('b', 5);
+        const keys = Array.from(map.keys());
+        return keys.length === 2 && keys[0] === 'a' && keys[1] === 'b' ? 1 : 0;
+    }
+}

usvm-ts/src/test/resources/models/strict-collections/tsconfig.json

@@ -0,0 +1,8 @@
+{
+  "compilerOptions": {
+    "target": "ES2021",
+    "module": "commonjs",
+    "strictNullChecks": true
+  },
+  "files": ["StrictCollections.ts"]
+}