Collect stopped TypeScript inputs through observers

usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt

@@ -6,5 +6,5 @@ import org.usvm.statistics.StepsStatistics
  * [StopStrategy] which stops when the [limit] number of steps is reached.
  */
 class StepLimitStopStrategy(private val limit: ULong, private val stepsStatistics: StepsStatistics<*, *>) : StopStrategy {
-    override fun shouldStop(): Boolean = stepsStatistics.totalSteps > limit
+    override fun shouldStop(): Boolean = stepsStatistics.totalSteps >= limit
 }

usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt

@@ -35,6 +35,7 @@ internal fun <Type, State : UState<Type, *, *, *, *, State>> State.checkSat(cond
         val trueModels = conditionalState.models.filter { it.eval(condition).isTrue }
 
         if (trueModels.isNotEmpty()) {
+            conditionalState.models = trueModels
             return conditionalState
         }
     }
@@ -44,7 +45,7 @@ internal fun <Type, State : UState<Type, *, *, *, *, State>> State.checkSat(cond
 
     return when (solverResult) {
         is USatResult -> {
-            conditionalState.models += solverResult.model
+            conditionalState.models = listOf(solverResult.model)
 
             // If state with the added condition is satisfiable, it means that the original state is satisfiable too,
             // and we can save a model from the solver

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

@@ -30,6 +30,7 @@ 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.jacodb.ets.model.EtsVoidType
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
@@ -167,6 +168,7 @@ class TsContext(
         is EtsStringType -> addressSort
         is EtsNullType -> addressSort
         is EtsUndefinedType -> addressSort
+        is EtsVoidType -> addressSort
         is EtsUnionType -> unresolvedSort
         is EtsIntersectionType -> {
             val memberSorts = type.types.map(::typeToSort)

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

@@ -11,6 +11,7 @@ import org.usvm.UBoolExpr
 import org.usvm.machine.call.TsUnknownCallEvent
 import org.usvm.machine.expr.TsSimpleValueResolver
 import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsState
 import org.usvm.statistics.UInterpreterObserver
 
 @Suppress("unused")
@@ -33,6 +34,14 @@ interface TsInterpreterObserver : UInterpreterObserver {
         // default empty implementation
     }
 
+    /**
+     * Reports a feasible prefix before STOP_PATH prunes an unknown call or a semantic-model residual.
+     * The state is live; observers retaining it must take their own snapshot before this callback returns.
+     */
+    fun onPathStopped(state: TsState, reason: String) {
+        // default empty implementation
+    }
+
     /** Reports a satisfiable path stopped at an explicit runtime modeling boundary. */
     fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
         // default empty implementation

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

@@ -9,6 +9,7 @@ import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
+import org.usvm.UPathSelector
 import org.usvm.api.targets.TsTarget
 import org.usvm.machine.call.TsBuiltInUnknownCallModels
 import org.usvm.machine.call.TsModelUnknownCallDispatcher
@@ -32,6 +33,7 @@ import org.usvm.statistics.TimeStatistics
 import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
+import org.usvm.statistics.collectors.StatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatisticsImpl
@@ -79,6 +81,8 @@ class TsMachine(
     private val observer: TsInterpreterObserver? = null,
     unknownCallDispatcher: TsUnknownCallDispatcher? = null,
     unknownCallModels: TsUnknownCallModelCatalog? = null,
+    /** Creates an observer with access to the analysis queue, including unsupported terminal states. */
+    private val machineObserverFactory: ((UPathSelector<TsState>) -> UMachineObserver<TsState>)? = null,
 ) : UMachine<TsState>() {
     init {
         val hasCompatibleCoverageScope = tsOptions.classCoverageTargets == null ||
@@ -214,15 +218,7 @@ class TsMachine(
             callGraphStatisticsFactory = { callGraphStatistics },
         )
 
-        val statesCollector =
-            when (options.stateCollectionStrategy) {
-                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TsState>(coverageStatistics) {
-                    it.methodResult is TsMethodResult.TsException
-                }
-
-                StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
-                StateCollectionStrategy.ALL -> AllStatesCollector()
-            }
+        val statesCollector = createStatesCollector(coverageStatistics)
 
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
@@ -283,14 +279,23 @@ class TsMachine(
         }
 
         val supportedObserver = CompositeUMachineObserver(observers)
-        val outcomeObserver = UnsupportedPathsObserver(supportedObserver, unsupportedPaths)
+        val outcomeObserver = UnsupportedPathsObserver(
+            delegate = supportedObserver,
+            unsupportedPaths = unsupportedPaths,
+        )
+        val factoryObserver = machineObserverFactory?.invoke(pathSelector)
+        val executionObserver = if (factoryObserver == null) {
+            outcomeObserver
+        } else {
+            CompositeUMachineObserver(outcomeObserver, factoryObserver)
+        }
 
         run(
-            interpreter,
-            pathSelector,
-            observer = outcomeObserver,
+            interpreter = interpreter,
+            pathSelector = pathSelector,
+            observer = executionObserver,
             isStateTerminated = { state -> state.callStack.isEmpty() },
-            stopStrategy = stopStrategy
+            stopStrategy = stopStrategy,
         )
 
         val stopReason = if (pathSelector.isEmpty()) {
@@ -309,6 +314,16 @@ class TsMachine(
         )
     }
 
+    private fun createStatesCollector(
+        coverageStatistics: CoverageStatistics<EtsMethod, EtsStmt, TsState>,
+    ): StatesCollector<TsState> = when (options.stateCollectionStrategy) {
+        StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TsState>(coverageStatistics) {
+            it.methodResult is TsMethodResult.TsException
+        }
+        StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
+        StateCollectionStrategy.ALL -> AllStatesCollector()
+    }
+
     private fun classCoverageMethods(entryMethods: Set<EtsMethod>): Set<EtsMethod> {
         val targets = tsOptions.classCoverageTargets
         val classes = if (targets == null) {
@@ -378,6 +393,10 @@ private class FailureTrackingUnknownCallObserver(
     var pathStopped: Boolean = false
         private set
 
+    override fun onPathStopped(state: TsState, reason: String) {
+        delegate?.onPathStopped(state = state, reason = reason)
+    }
+
     override fun onUnknownCall(event: TsUnknownCallEvent) {
         val decision = event.decision
         val stopsPath = decision is TsUnknownCallDecision.ResidualFallback &&

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

@@ -0,0 +1,65 @@
+package org.usvm.machine
+
+import org.usvm.UPathSelector
+import org.usvm.machine.state.TsState
+import org.usvm.statistics.UMachineObserver
+
+/**
+ * Collects unfinished inputs without changing the machine's ordinary witness collection.
+ *
+ * Install this as the interpreter observer and pass [createMachineObserver] as the machine observer factory.
+ * Call [collectRemainingStates] after a successful analysis, while the machine is still open. Queue extraction
+ * is deferred because `onMachineStopped` also runs on exceptional exits, and draining changes stop metadata.
+ * No additional execution steps or satisfiability checks are performed for queued states.
+ */
+class TsStoppedStatesObserver(
+    private val consumeState: (TsState) -> Unit,
+) : TsInterpreterObserver {
+    private var pathSelector: UPathSelector<TsState>? = null
+    private var machineStopped: Boolean = false
+    private var emissionFailure: Throwable? = null
+
+    fun createMachineObserver(pathSelector: UPathSelector<TsState>): UMachineObserver<TsState> {
+        this.pathSelector = pathSelector
+        machineStopped = false
+        emissionFailure = null
+
+        return object : UMachineObserver<TsState> {
+            override fun onMachineStopped() {
+                machineStopped = true
+            }
+
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                val isStoppedPrefix = stateReachable && state.unsupportedReason != null
+                if (isStoppedPrefix) {
+                    consumeState(state.clone())
+                }
+            }
+        }
+    }
+
+    override fun onPathStopped(state: TsState, reason: String) {
+        // Unknown-call observation must not interrupt fallback pruning; report sink failures on completion.
+        val emission = runCatching {
+            val prefix = state.clone()
+            prefix.unsupportedReason = reason
+            consumeState(prefix)
+        }
+        val failure = emission.exceptionOrNull()
+        if (failure != null && emissionFailure == null) {
+            emissionFailure = failure
+        }
+    }
+
+    fun collectRemainingStates() {
+        val failure = emissionFailure
+        if (failure != null) {
+            throw failure
+        }
+
+        val selector = pathSelector ?: return
+        check(machineStopped) { "Collect queued states only after successful machine analysis" }
+
+        selector.drain().forEach(consumeState)
+    }
+}

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

@@ -52,11 +52,13 @@ class TsModelUnknownCallDispatcher(
 
         when (fallback) {
             TsResidualCallPolicy.STOP_PATH -> {
-                val falseExpr = scope.calcOnState { ctx.falseExpr }
+                val stoppedState = scope.calcOnState { this }
+                val falseExpr = stoppedState.ctx.falseExpr
                 logger.warn {
                     "Stopping path for unknown call ${call.callee} at ${call.callSite.location}: " +
                         "reason=${call.failureReason}"
                 }
+                observer?.onPathStoppedSafely(state = stoppedState, reason = stoppedPathReason(call))
                 scope.assert(falseExpr)
             }
 
@@ -85,9 +87,12 @@ class TsModelUnknownCallDispatcher(
         } else {
             null
         }
-        val stoppedResidualIsSatisfiable = residualGuard != null &&
-            fallback == TsResidualCallPolicy.STOP_PATH &&
-            scope.checkSat(residualGuard) != null
+        val stoppedResidualState = if (residualGuard != null && fallback == TsResidualCallPolicy.STOP_PATH) {
+            scope.checkSat(residualGuard)
+        } else {
+            null
+        }
+        val stoppedResidualIsSatisfiable = stoppedResidualState != null
 
         var modelApplied = false
         var freshResidualApplied = false
@@ -119,11 +124,12 @@ class TsModelUnknownCallDispatcher(
             }
         }
 
-        if (stoppedResidualIsSatisfiable) {
+        if (stoppedResidualState != null) {
             logger.warn {
                 "Stopping residual path for unknown call ${call.callee} at ${call.callSite.location}: " +
                     "reason=${call.failureReason}"
             }
+            observer?.onPathStoppedSafely(state = stoppedResidualState, reason = stoppedPathReason(call))
         }
         scope.forkMulti(guardedStateChanges)
 
@@ -142,6 +148,9 @@ class TsModelUnknownCallDispatcher(
         }
     }
 
+    private fun stoppedPathReason(call: TsUnknownCall): String =
+        "Unknown call ${call.callee} at ${call.callSite.location}: reason=${call.failureReason}"
+
     private fun reportFallback(call: TsUnknownCall) {
         if (fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
             logger.debug {
@@ -204,3 +213,8 @@ class TsModelUnknownCallDispatcher(
         decision = decision,
     )
 }
+
+private fun TsInterpreterObserver.onPathStoppedSafely(state: TsState, reason: String) {
+    runCatching { onPathStopped(state = state, reason = reason) }
+        .onFailure { error -> logger.warn(error) { "Unknown-call observer failed while recording a stopped path" } }
+}