Preserve supported class entries after unsupported inputs or initial UNSAT

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

@@ -23,6 +23,7 @@ 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.TsInitialStateInputGuard
 import org.usvm.machine.types.TsTypeSystem
 import org.usvm.ps.createPathSelector
 import org.usvm.statistics.CompositeUMachineObserver
@@ -59,6 +60,7 @@ data class TsAnalysisResult(
     val stopReason: TsAnalysisStopReason,
     /** Reasons for satisfiable paths excluded by an explicit engine model bound. */
     val unsupportedPaths: List<String>,
+    val infeasibleEntryPoints: List<String> = emptyList(),
 )
 
 /** Terminal states and failure metadata for one TypeScript analysis. */
@@ -69,6 +71,8 @@ data class TsMachineAnalysisResult(
     val unsupportedCall: Boolean,
     val engineFailed: Boolean,
     val unsupportedPaths: List<String>,
+    /** Entry signatures whose initial constraints were UNSAT, distinct from unsupported inputs. */
+    val infeasibleEntryPoints: List<String> = emptyList(),
 ) {
     /** Includes execution bounds and unsupported entry inputs retained in [unsupportedPaths]. */
     val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty()
@@ -165,6 +169,7 @@ class TsMachine(
             states = result.states,
             stopReason = result.stopReason,
             unsupportedPaths = result.unsupportedPaths,
+            infeasibleEntryPoints = result.infeasibleEntryPoints,
         )
     }
 
@@ -184,10 +189,11 @@ class TsMachine(
         interpreter.resetStepFailure()
         failureTrackingUnknownCallObserver.reset()
 
-        val (initialStates, unsupportedPaths) = createInitialStates(methods, targets, configureInitialState)
+        val (initialStates, unsupportedPaths, infeasibleEntryPoints) =
+            createInitialStates(methods, targets, configureInitialState)
 
         if (initialStates.isEmpty()) {
-            return emptyAnalysisResult(unsupportedPaths)
+            return emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints)
         }
 
         val methodsToTrackCoverage =
@@ -299,11 +305,8 @@ class TsMachine(
             stopStrategy = stopStrategy,
         )
 
-        val stopReason = if (pathSelector.isEmpty()) {
-            TsAnalysisStopReason.EXHAUSTED
-        } else {
-            TsAnalysisStopReason.STOPPED
-        }
+        val exhausted = pathSelector.isEmpty()
+        val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED
 
         return TsMachineAnalysisResult(
             states = statesCollector.collectedStates,
@@ -312,6 +315,7 @@ class TsMachine(
             unsupportedCall = failureTrackingUnknownCallObserver.pathStopped,
             engineFailed = interpreter.stepFailed,
             unsupportedPaths = unsupportedPaths.toList(),
+            infeasibleEntryPoints = infeasibleEntryPoints,
         )
     }
 
@@ -353,26 +357,39 @@ class TsMachine(
         return if (targets == null) coveredMethods + entryMethods else coveredMethods
     }
 
-    private fun emptyAnalysisResult(unsupportedPaths: Set<String>) = TsMachineAnalysisResult(
+    private fun emptyAnalysisResult(
+        unsupportedPaths: Set<String>,
+        infeasibleEntryPoints: List<String>,
+    ) = TsMachineAnalysisResult(
         states = emptyList(),
         stopReason = TsAnalysisStopReason.EXHAUSTED,
         timedOut = false,
         unsupportedCall = false,
         engineFailed = false,
         unsupportedPaths = unsupportedPaths.toList(),
+        infeasibleEntryPoints = infeasibleEntryPoints,
+    )
+
+    private data class InitialStatesResult(
+        val initialStates: Map<EtsMethod, TsState>,
+        val unsupportedPaths: MutableSet<String>,
+        val infeasibleEntryPoints: List<String>,
     )
 
     private fun createInitialStates(
         methods: List<EtsMethod>,
         targets: List<TsTarget>,
         configureInitialState: (EtsMethod, TsState) -> Unit,
-    ): Pair<Map<EtsMethod, TsState>, MutableSet<String>> {
+    ): InitialStatesResult {
         val initialStates = mutableMapOf<EtsMethod, TsState>()
         val unsupportedPaths = mutableSetOf<String>()
+        val infeasibleEntryPoints = mutableListOf<String>()
         val constructorInputs = TsConstructorInputGuard()
+        val initialStateInputs = TsInitialStateInputGuard()
 
         methods.forEach { method ->
             val unsupportedReason = constructorInputs.unsupportedReason(method)
+                ?: initialStateInputs.unsupportedReason(method)
             if (unsupportedReason != null) {
                 unsupportedPaths += unsupportedReason
             } else {
@@ -381,11 +398,17 @@ class TsMachine(
                 }
                 if (initialState != null) {
                     initialStates[method] = initialState
+                } else {
+                    infeasibleEntryPoints += method.humanReadableSignature
                 }
             }
         }
 
-        return initialStates to unsupportedPaths
+        return InitialStatesResult(
+            initialStates = initialStates,
+            unsupportedPaths = unsupportedPaths,
+            infeasibleEntryPoints = infeasibleEntryPoints,
+        )
     }
 
     override fun close() {

usvm-ts/src/main/kotlin/org/usvm/machine/types/TsInitialStateInputGuard.kt

@@ -0,0 +1,34 @@
+package org.usvm.machine.types
+
+import org.jacodb.ets.model.EtsAliasType
+import org.jacodb.ets.model.EtsBigIntType
+import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsIntersectionType
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsType
+import org.usvm.util.humanReadableSignature
+
+/** Bounds only input types whose initial-state construction has no implemented domain. */
+internal class TsInitialStateInputGuard {
+    fun unsupportedReason(method: EtsMethod): String? {
+        val genericParameters = method.typeParameters.filterIsInstance<EtsGenericType>().associateBy { it.typeName }
+        for (parameter in method.parameters) {
+            val inputType = parameter.type.initialInputType(genericParameters)
+            val domain = inputType.unsupportedInitialDomain() ?: continue
+
+            return "$domain input parameter '${parameter.name}' in ${method.humanReadableSignature} is not modeled"
+        }
+
+        return null
+    }
+}
+
+private fun EtsType.unsupportedInitialDomain(): String? = when (this) {
+    is EtsFunctionType -> "Callable"
+    EtsBigIntType -> "BigInt"
+    is EtsAliasType -> originalType.unsupportedInitialDomain()
+    // Intersections use each member's sort; unions use the existing unresolved input domain instead.
+    is EtsIntersectionType -> types.firstNotNullOfOrNull { it.unsupportedInitialDomain() }
+    else -> null
+}

usvm-ts/src/test/kotlin/org/usvm/machine/TsEntryStartupInputsTest.kt

@@ -0,0 +1,141 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.SolverType
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.eq
+import org.usvm.util.getResourcePath
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
+import kotlin.test.assertFalse
+import kotlin.test.assertTrue
+import kotlin.time.Duration.Companion.seconds
+
+class TsEntryStartupInputsTest : TsMethodTestRunner() {
+    override val scene = EtsScene(
+        projectFiles = listOf(
+            loadEtsFileAutoConvert(
+                path = getResourcePath("/models/EntryStartupInputs.ts"),
+                provider = EtsIrProvider.TS_FRONTEND,
+            ),
+        ),
+    )
+    private val machineOptions = UMachineOptions(
+        stateCollectionStrategy = StateCollectionStrategy.ALL,
+        stopOnCoverage = 0,
+        timeout = 5.seconds,
+        solverType = SolverType.YICES,
+        throwExceptionOnStepFailure = true,
+    )
+
+    @Test
+    fun `unsupported entry inputs do not discard supported methods of the same class`() {
+        val supported = getMethod(methodName = "supported", className = "EntryStartupInputs")
+        val methods = unsupportedMethods() + supported
+        val configured = mutableListOf<String>()
+
+        val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyzeWithMetadata(methods = methods) { method, _ -> configured += method.name }
+        }
+
+        assertFalse(result.engineFailed)
+        assertEquals(listOf("supported"), configured)
+        assertTrue(result.states.isNotEmpty())
+        assertTrue(result.states.all { it.entrypoint == supported })
+        assertEquals(3, result.unsupportedPaths.size)
+        assertTrue(result.unsupportedPaths.any { "Callable input parameter 'reader'" in it })
+        assertTrue(result.unsupportedPaths.any { "withBigInt" in it && "BigInt input parameter 'value'" in it })
+        assertTrue(result.unsupportedPaths.any { "withGenericBigInt" in it && "BigInt input parameter 'value'" in it })
+
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = supported,
+            { _, value -> value eq 1 },
+            { _, value -> value eq 2 },
+            invariants = arrayOf({ _, value -> (value eq 1) || (value eq 2) }),
+        )
+    }
+
+    @Test
+    fun `an entirely unsupported entry set returns explicit per-method reasons`() {
+        val methods = unsupportedMethods()
+
+        val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyzeWithMetadata(methods = methods)
+        }
+
+        assertFalse(result.engineFailed)
+        assertTrue(result.states.isEmpty())
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason)
+        assertEquals(3, result.unsupportedPaths.size)
+        for (method in methods) {
+            assertTrue(result.unsupportedPaths.any { method.name in it })
+        }
+    }
+
+    @Test
+    fun `unexpected initial-state configuration errors remain failures`() {
+        val method = getMethod(methodName = "supported", className = "EntryStartupInputs")
+
+        TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            val exception = assertFailsWith<IllegalStateException> {
+                machine.analyzeWithMetadata(methods = listOf(method)) { _, _ ->
+                    error("Unexpected configuration defect")
+                }
+            }
+
+            assertEquals("Unexpected configuration defect", exception.message)
+        }
+    }
+
+    @Test
+    fun `an infeasible entry is distinct from unsupported inputs and does not discard another entry`() {
+        val infeasible = getMethod(methodName = "supported", className = "EntryStartupInputs")
+        val independent = getMethod(methodName = "independent", className = "EntryStartupInputs")
+        val methods = unsupportedMethods() + infeasible + independent
+
+        val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyzeWithMetadata(methods = methods) { method, state ->
+                // Deliberately test the initial solver's UNSAT contract, independently of source feasibility.
+                if (method == infeasible) {
+                    state.pathConstraints += state.ctx.falseExpr
+                }
+            }
+        }
+
+        assertFalse(result.engineFailed)
+        assertTrue(result.states.isNotEmpty())
+        assertTrue(result.states.all { it.entrypoint == independent })
+        assertEquals(3, result.unsupportedPaths.size)
+        assertEquals(1, result.infeasibleEntryPoints.size)
+        assertTrue("supported" in result.infeasibleEntryPoints.single())
+    }
+
+    @Test
+    fun `an entirely infeasible entry set is exhausted without an unsupported or engine failure`() {
+        val method = getMethod(methodName = "supported", className = "EntryStartupInputs")
+
+        val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyzeWithMetadata(methods = listOf(method)) { _, state ->
+                state.pathConstraints += state.ctx.falseExpr
+            }
+        }
+
+        assertFalse(result.engineFailed)
+        assertFalse(result.runtimeLimited)
+        assertTrue(result.states.isEmpty())
+        assertTrue(result.unsupportedPaths.isEmpty())
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason)
+        assertEquals(1, result.infeasibleEntryPoints.size)
+        assertTrue("supported" in result.infeasibleEntryPoints.single())
+    }
+
+    private fun unsupportedMethods() = listOf("withCallback", "withBigInt", "withGenericBigInt").map { name ->
+        getMethod(methodName = name, className = "EntryStartupInputs")
+    }
+}

usvm-ts/src/test/resources/models/EntryStartupInputs.ts

@@ -0,0 +1,25 @@
+type Reader = (value: number) => number;
+type Big = bigint;
+
+export class EntryStartupInputs {
+  independent(): number {
+    return 17;
+  }
+
+  supported(value: number): number {
+    if (value > 10) return 1;
+    return 2;
+  }
+
+  withCallback(reader: Reader): number {
+    return reader(2);
+  }
+
+  withBigInt(value: Big): Big {
+    return value;
+  }
+
+  withGenericBigInt<T extends bigint>(value: T): T {
+    return value;
+  }
+}