[TS] Evaluate instanceof against runtime constructor values

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

@@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanLiteralType
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsLexicalEnvType
@@ -91,6 +92,16 @@ class TsContext(
     // String constant caching at context level
     private val stringConstants: MutableMap<String, UConcreteHeapRef> = mutableMapOf()
 
+    private val classConstructorRefs: MutableMap<EtsClassSignature, UConcreteHeapRef> = mutableMapOf()
+    private val constructorSignatures: MutableMap<UConcreteHeapRef, EtsClassSignature> = mutableMapOf()
+
+    fun classConstructorRef(signature: EtsClassSignature): UConcreteHeapRef =
+        classConstructorRefs.getOrPut(signature) {
+            allocateStaticRef().also { constructorSignatures[it] = signature }
+        }
+
+    fun classConstructorSignature(ref: UConcreteHeapRef): EtsClassSignature? = constructorSignatures[ref]
+
     /**
      * Reverse mapping from heap references to their original string constant values.
      * This is used during test resolution to retrieve the actual string content when

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

@@ -17,6 +17,7 @@ import org.usvm.machine.call.deduplicateEtsFilesBySignature
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
+import org.usvm.machine.types.TsConstructorInputGuard
 import org.usvm.machine.types.TsTypeSystem
 import org.usvm.ps.createPathSelector
 import org.usvm.statistics.CompositeUMachineObserver
@@ -80,13 +81,15 @@ class TsMachine(
             )
         }
         ?: scene
-    private val graph = TsGraph(analysisScene)
-    private val typeSystem = TsTypeSystem(analysisScene, typeOperationsTimeout = 1.seconds, graph.hierarchy)
+    private val runtimeScene = analysisScene.withCoreRuntimeSdk()
+    private val graph = TsGraph(runtimeScene)
+    private val typeSystem = TsTypeSystem(runtimeScene, typeOperationsTimeout = 1.seconds, graph.hierarchy)
     private val components = TsComponents(typeSystem, options)
     private val ctx = TsContext(
-        scene = analysisScene,
+        scene = runtimeScene,
         components = components,
-        applicationAndSdkClasses = scene.projectAndSdkClasses,
+        // Model bodies are reachable only through their dispatcher and its domain guards.
+        applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses,
     )
     private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher(
         models = requireNotNull(resolvedUnknownCallModels),
@@ -113,12 +116,15 @@ class TsMachine(
         methods: List<EtsMethod>,
         targets: List<TsTarget> = emptyList(),
     ): TsAnalysisResult {
-        val initialStates = mutableMapOf<EtsMethod, TsState>()
-        methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) }
+        val (initialStates, unsupportedPaths) = createInitialStates(methods, targets)
+
+        if (initialStates.isEmpty()) {
+            return TsAnalysisResult(emptyList(), TsAnalysisStopReason.EXHAUSTED, unsupportedPaths.toList())
+        }
 
         val methodsToTrackCoverage =
             when (options.coverageZone) {
-                CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet()
+                CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet()
                 CoverageZone.CLASS -> TODO("Unsupported yet")
             }
 
@@ -157,8 +163,6 @@ class TsMachine(
 
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
-        val unsupportedPaths = mutableSetOf<String>()
-
         if (tsOptions.enableVisualization) {
             observers += TsStateVisualizer()
         }
@@ -196,7 +200,7 @@ class TsMachine(
         if (logger.isInfoEnabled) {
             observers.add(
                 StatisticsByMethodPrinter(
-                    getMethods = { methods },
+                    getMethods = { initialStates.keys.toList() },
                     print = logger::info,
                     getMethodSignature = { it.humanReadableSignature },
                     coverageStatistics = coverageStatistics,
@@ -242,6 +246,26 @@ class TsMachine(
         )
     }
 
+    private fun createInitialStates(
+        methods: List<EtsMethod>,
+        targets: List<TsTarget>,
+    ): Pair<Map<EtsMethod, TsState>, MutableSet<String>> {
+        val initialStates = mutableMapOf<EtsMethod, TsState>()
+        val unsupportedPaths = mutableSetOf<String>()
+        val constructorInputs = TsConstructorInputGuard()
+
+        methods.forEach { method ->
+            val unsupportedReason = constructorInputs.unsupportedReason(method)
+            if (unsupportedReason != null) {
+                unsupportedPaths += unsupportedReason
+            } else {
+                initialStates[method] = interpreter.getInitialState(method, targets)
+            }
+        }
+
+        return initialStates to unsupportedPaths
+    }
+
     override fun close() {
         components.close()
     }

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

@@ -0,0 +1,17 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsFileSignature
+
+private val runtimeFile = EtsFileSignature(
+    projectName = "usvm.ts.runtime",
+    fileName = "TypeError",
+)
+private val typeErrorSignature = EtsClassSignature(
+    name = "TypeError",
+    file = runtimeFile,
+)
+
+/** Type identity of terminal JavaScript TypeError exceptions produced by the interpreter. */
+internal val TS_TYPE_ERROR_TYPE = EtsClassType(typeErrorSignature)

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

@@ -0,0 +1,65 @@
+package org.usvm.machine
+
+import org.jacodb.ets.dto.EtsFileDto
+import org.jacodb.ets.dto.toEtsFile
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsFile
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.etsIrSerializerScript
+import org.jacodb.ets.utils.generateEtsIR
+import org.usvm.util.EtsHierarchy
+import kotlin.io.path.deleteIfExists
+import kotlin.io.path.inputStream
+
+private val coreRuntimeClassNames = setOf("Object", "Function", "Array")
+
+// JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports
+// declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes.
+private val coreRuntimeSdk: EtsFileDto by lazy {
+    val library = etsIrSerializerScript(EtsIrProvider.TS_FRONTEND).resolveSibling("lib.es5.d.ts")
+    val ir = generateEtsIR(library, loadEntrypoints = false, provider = EtsIrProvider.TS_FRONTEND)
+    try {
+        val file = ir.inputStream().use { EtsFileDto.loadFromJson(it) }
+        file.copy(
+            classes = file.classes.filter { it.signature.name in coreRuntimeClassNames },
+            namespaces = emptyList(),
+        )
+    } finally {
+        ir.deleteIfExists()
+    }
+}
+
+/** Standard Function and Array declarations use dedicated values, not ordinary class-instance witnesses. */
+internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean =
+    signature.file == EtsHierarchy.OBJECT_CLASS.signature.file &&
+        signature.name in setOf("Function", "Array")
+
+/**
+ * Load Object, Function and Array from the standard declarations bundled in the pinned JacoDB dependency.
+ * Keep their signatures and members and preserve SDK declarations supplied by the caller. Declaration files
+ * describe prototypes and APIs; executing an SDK API still requires an interpreter implementation or model.
+ */
+internal fun EtsScene.withCoreRuntimeSdk(): EtsScene {
+    val missingNames = coreRuntimeClassNames - sdkClasses.map { it.name }.toSet()
+    if (missingNames.isEmpty()) return this
+
+    val library = coreRuntimeSdk.toEtsFile()
+    val classes = library.classes.filter { it.name in missingNames }
+    check(classes.map { it.name }.toSet() == missingNames) { "Core TypeScript SDK declarations are missing" }
+    val file = EtsFile(signature = library.signature, classes = classes, namespaces = emptyList())
+
+    return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + file, projectName = projectName)
+}
+
+/** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */
+internal fun EtsScene.sdkConstructorForGlobal(local: EtsLocal): EtsClass? =
+    sdkClasses.singleOrNull { it.name == local.name }
+
+internal fun EtsScene.runtimeFunctionType(): EtsClassType {
+    val functionClass = sdkClasses.singleOrNull { it.name == "Function" }
+        ?: throw UnsupportedOperationException("SDK Function identity is ambiguous or unavailable")
+    return EtsClassType(functionClass.signature)
+}

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

@@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
+import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsNullType
@@ -36,6 +37,7 @@ import org.usvm.machine.types.TsUnresolvedValue
 import org.usvm.machine.types.iteUnresolvedValue
 import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.machine.types.mkFakeValue
+import org.usvm.machine.types.requiresConstructorWitness
 import org.usvm.machine.types.toAuxiliaryType
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.TsResolutionResult
@@ -225,6 +227,20 @@ private fun TsContext.prepareInitialInputField(
     activeInitial: UBoolExpr,
     hierarchy: EtsHierarchy,
 ): TsUnresolvedValue? {
+    // A write, deletion or absent property can make the declared initial value irrelevant.
+    // Do not reject the entire input object just because another field needs a constructor witness.
+    val unsupportedInitial = when {
+        declaration?.type?.requiresConstructorWitness() == true -> "Constructor-typed input field"
+        declaration?.type is EtsGenericType -> "Unresolved generic input field"
+        else -> null
+    }
+    if (unsupportedInitial != null) {
+        scope.fork(mkNot(activeInitial), blockOnFalseState = {
+            terminateAsUnsupported(reason = "$unsupportedInitial is not modeled")
+        }) ?: return null
+        return value
+    }
+
     val optional = declaration?.optional == true
     val sort = declaration?.let { typeToSort(it.type) } ?: unresolvedSort
     val expectedKind = when (sort) {