[TS] Evaluate instanceof against runtime constructor values

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

@@ -149,19 +149,29 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
             MachineResult(
                 states = entryObserver.reachedStates,
                 stopReason = outcome.stopReason,
+                unsupportedPaths = outcome.unsupportedPaths,
             )
         }
         val states = analysis.states
         if (states.isEmpty()) {
             val status = when (analysis.stopReason) {
-                TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED
+                TsAnalysisStopReason.EXHAUSTED -> {
+                    if (analysis.unsupportedPaths.isEmpty()) {
+                        CallsSymbolicStatus.UNREACHED
+                    } else {
+                        CallsSymbolicStatus.UNSUPPORTED
+                    }
+                }
                 // The machine options above disable every stop condition except the per-target timeout.
-                TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT
+                TsAnalysisStopReason.STOPPED -> {
+                    CallsSymbolicStatus.TIMEOUT
+                }
             }
 
             return result(
                 status = status,
                 startedAt = startedAt,
+                diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null },
             )
         }
 
@@ -284,6 +294,7 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
     private data class MachineResult(
         val states: List<TsState>,
         val stopReason: TsAnalysisStopReason,
+        val unsupportedPaths: List<String>,
     )
 }
 

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
@@ -17,6 +18,7 @@ import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
 import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringLiteralType
@@ -66,6 +68,9 @@ class TsContext(
 
     val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this)
 
+    /** Array storage for UTF-16 code units; ordinary TypeScript arrays never use this region. */
+    internal val stringBackingArrayDescriptor: EtsType = EtsRawType(kind = "usvm.ts.string.backing")
+
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
@@ -87,6 +92,18 @@ 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]
+
+    fun classConstructorRefs(): Collection<UConcreteHeapRef> = classConstructorRefs.values
+
     /**
      * 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

@@ -1,9 +1,22 @@
 package org.usvm.machine
 
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsAliasType
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsClassValueType
+import org.jacodb.ets.model.EtsFileSignature
+import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsIntersectionType
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsTupleType
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
+import org.jacodb.ets.model.EtsUnionType
 import org.usvm.CoverageZone
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
@@ -49,6 +62,8 @@ enum class TsAnalysisStopReason {
 data class TsAnalysisResult(
     val states: List<TsState>,
     val stopReason: TsAnalysisStopReason,
+    /** Reasons for satisfiable paths excluded by an explicit engine model bound. */
+    val unsupportedPaths: List<String>,
 )
 
 class TsMachine(
@@ -101,6 +116,7 @@ class TsMachine(
     )
     private val cfgStatistics = CfgStatisticsImpl(graph)
 
+    /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */
     fun analyze(
         methods: List<EtsMethod>,
         targets: List<TsTarget> = emptyList(),
@@ -110,12 +126,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")
             }
 
@@ -154,7 +173,6 @@ class TsMachine(
 
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
-
         if (tsOptions.enableVisualization) {
             observers += TsStateVisualizer()
         }
@@ -192,7 +210,7 @@ class TsMachine(
         if (logger.isInfoEnabled) {
             observers.add(
                 StatisticsByMethodPrinter(
-                    getMethods = { methods },
+                    getMethods = { initialStates.keys.toList() },
                     print = logger::info,
                     getMethodSignature = { it.humanReadableSignature },
                     coverageStatistics = coverageStatistics,
@@ -202,10 +220,25 @@ class TsMachine(
             )
         }
 
+        val supportedObserver = CompositeUMachineObserver(observers)
+        val outcomeObserver = object : UMachineObserver<TsState> by supportedObserver {
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                val unsupportedReason = state.unsupportedReason
+                if (unsupportedReason != null) {
+                    if (stateReachable) {
+                        unsupportedPaths += unsupportedReason
+                    }
+                    return
+                }
+
+                supportedObserver.onStateTerminated(state, stateReachable)
+            }
+        }
+
         run(
             interpreter,
             pathSelector,
-            observer = CompositeUMachineObserver(observers),
+            observer = outcomeObserver,
             isStateTerminated = { state -> state.callStack.isEmpty() },
             stopStrategy = stopStrategy
         )
@@ -216,10 +249,172 @@ class TsMachine(
             TsAnalysisStopReason.STOPPED
         }
 
-        return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason)
+        return TsAnalysisResult(
+            states = statesCollector.collectedStates,
+            stopReason = stopReason,
+            unsupportedPaths = unsupportedPaths.toList(),
+        )
+    }
+
+    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 classesBySignature = analysisScene.projectAndSdkClasses.associateBy { it.signature }
+
+        methods.forEach { method ->
+            val genericParameters = method.typeParameters.filterIsInstance<EtsGenericType>().associateBy { it.typeName }
+            val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter ->
+                val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature)
+                gap?.let { parameter to it }
+            }
+            if (unsupportedParameter != null) {
+                val (parameter, gap) = unsupportedParameter
+                unsupportedPaths += "${gap.description} '${parameter.name}' " +
+                    "in ${method.humanReadableSignature} is not modeled"
+            } else {
+                initialStates[method] = interpreter.getInitialState(method, targets)
+            }
+        }
+
+        return initialStates to unsupportedPaths
     }
 
     override fun close() {
         components.close()
     }
 }
+
+private enum class ConstructorInputGap(val description: String) {
+    CONSTRUCTOR_VALUE("Constructor-typed parameter"),
+    UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"),
+}
+
+private fun EtsType.constructorInputGap(
+    genericParameters: Map<String, EtsGenericType>,
+    classesBySignature: Map<EtsClassSignature, EtsClass>,
+    visitedGenerics: Set<String> = emptySet(),
+    visitedClasses: Set<EtsClassSignature> = emptySet(),
+): ConstructorInputGap? = when (this) {
+    is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE
+    is EtsUnionType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsIntersectionType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsTupleType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsArrayType -> elementType.constructorInputGap(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsClassType -> constructorInputGapInClass(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsAliasType -> originalType.constructorInputGap(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsGenericType -> {
+        if (typeName in visitedGenerics) {
+            null
+        } else {
+            val declaration = genericParameters[typeName]
+            listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType)
+                .firstNotNullOfOrNull {
+                    it.constructorInputGap(
+                        genericParameters,
+                        classesBySignature,
+                        visitedGenerics + typeName,
+                        visitedClasses,
+                    )
+                }
+        }
+    }
+    else -> null
+}
+
+private fun EtsClassType.constructorInputGapInClass(
+    genericParameters: Map<String, EtsGenericType>,
+    classesBySignature: Map<EtsClassSignature, EtsClass>,
+    visitedGenerics: Set<String>,
+    visitedClasses: Set<EtsClassSignature>,
+): ConstructorInputGap? {
+    val typeArgumentGap = typeParameters.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    if (typeArgumentGap != null) {
+        return typeArgumentGap
+    }
+
+    if (signature in visitedClasses) {
+        return null
+    }
+
+    val clazz = classesBySignature[signature] ?: return null
+    val nextVisitedClasses = visitedClasses + signature
+    val fieldGap = clazz.fields.firstNotNullOfOrNull { field ->
+        if (field.modifiers.isStatic) return@firstNotNullOfOrNull null
+
+        field.type.constructorInputGap(
+            genericParameters,
+            classesBySignature,
+            visitedGenerics,
+            nextVisitedClasses,
+        )
+    }
+    if (fieldGap != null) {
+        return fieldGap
+    }
+
+    val superClass = clazz.superClass ?: return null
+    val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) {
+        classesBySignature.values.filter { it.name == superClass.name }
+    } else {
+        listOfNotNull(classesBySignature[superClass])
+    }
+
+    return superClasses.firstNotNullOfOrNull { parent ->
+        val parentGap = EtsClassType(parent.signature).constructorInputGap(
+            genericParameters,
+            classesBySignature,
+            visitedGenerics,
+            nextVisitedClasses,
+        )
+        if (parentGap != null) return@firstNotNullOfOrNull parentGap
+
+        // The frontend omits extends type arguments, so an inherited T may contain a constructor.
+        val parentGenerics = parent.typeParameters.filterIsInstance<EtsGenericType>()
+            .mapTo(mutableSetOf()) { it.typeName }
+        val unresolvedGenericField = parent.fields.any { field ->
+            !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics)
+        }
+        if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null
+    }
+}
+
+private fun EtsType.containsGeneric(names: Set<String>): Boolean = when (this) {
+    is EtsGenericType -> typeName in names
+    is EtsUnionType -> types.any { it.containsGeneric(names) }
+    is EtsIntersectionType -> types.any { it.containsGeneric(names) }
+    is EtsTupleType -> types.any { it.containsGeneric(names) }
+    is EtsArrayType -> elementType.containsGeneric(names)
+    is EtsClassType -> typeParameters.any { it.containsGeneric(names) }
+    is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) }
+    is EtsAliasType -> originalType.containsGeneric(names)
+    else -> false
+}

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)