diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt index 13144c086d..64508bd67c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt +++ b/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 } diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt index abc3a58b93..50056e51d4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt +++ b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt @@ -35,6 +35,7 @@ internal fun > 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 > 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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 054d583873..9c260c84d0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/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) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index abe997f713..2030dd3802 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 54efdbc45f..85b3bd587c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/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) -> UMachineObserver)? = null, ) : UMachine() { init { val hasCompatibleCoverageScope = tsOptions.classCoverageTargets == null || @@ -214,15 +218,7 @@ class TsMachine( callGraphStatisticsFactory = { callGraphStatistics }, ) - val statesCollector = - when (options.stateCollectionStrategy) { - StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { - it.methodResult is TsMethodResult.TsException - } - - StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector() - StateCollectionStrategy.ALL -> AllStatesCollector() - } + val statesCollector = createStatesCollector(coverageStatistics) val observers = mutableListOf>(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, + ): StatesCollector = when (options.stateCollectionStrategy) { + StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { + it.methodResult is TsMethodResult.TsException + } + StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector() + StateCollectionStrategy.ALL -> AllStatesCollector() + } + private fun classCoverageMethods(entryMethods: Set): Set { 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 && diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsStoppedStatesObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsStoppedStatesObserver.kt new file mode 100644 index 0000000000..5f5154b047 --- /dev/null +++ b/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? = null + private var machineStopped: Boolean = false + private var emissionFailure: Throwable? = null + + fun createMachineObserver(pathSelector: UPathSelector): UMachineObserver { + this.pathSelector = pathSelector + machineStopped = false + emissionFailure = null + + return object : UMachineObserver { + 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) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 5ab9ad9772..bb17d5f108 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/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" } } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt new file mode 100644 index 0000000000..f0a3815c0d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt @@ -0,0 +1,121 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.state.TsState +import org.usvm.util.TsMethodTestRunner +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** Prefix collection contracts, including a snapshot before the unknown-call policy prunes it. */ +class TsMachineStoppedPathsTest : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/arrays/ArrayMethods.ts") + + private fun options() = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + @Test + fun `unknown push retains its feasible input prefix without claiming a returned result`() { + val method = getMethod(methodName = "arrayPush", className = "ArrayMethods") + val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) + + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + + val outcome = TsMachine( + scene = scene, + options = options(), + tsOptions = tsOptions, + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) + assertTrue(outcome.unsupportedCall) + assertFalse(outcome.engineFailed) + assertTrue(outcome.states.isEmpty()) + assertTrue(suspendedStates.isNotEmpty()) + assertTrue(suspendedStates.all { it.models.isNotEmpty() }) + assertTrue(suspendedStates.all { it.callStack.isNotEmpty() }) + assertTrue(suspendedStates.all { it.unsupportedReason?.contains("push") == true }) + } + + @Test + fun `unknown call without a stopped state observer retains ordinary witness behavior`() { + val method = getMethod(methodName = "arrayPush", className = "ArrayMethods") + val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) + + val outcome = TsMachine( + scene = scene, + options = options(), + tsOptions = tsOptions, + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(outcome.unsupportedCall) + assertTrue(outcome.states.isEmpty()) + } + + @Test + fun `a runtime conversion limit preserves the reached input instead of a terminal witness`() { + val stringScene = loadScene("/samples/lang/Strings.ts") + val owner = stringScene.projectAndSdkClasses.single { it.name == "Strings" } + val method = owner.methods.single { it.name == "stringWithNumber" } + + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + + val outcome = TsMachine( + scene = stringScene, + options = options(), + tsOptions = TsOptions(), + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } + + assertTrue(outcome.runtimeLimited) + assertTrue(outcome.unsupportedPaths.any { it.contains("STRING_CONCAT_OPERAND_CONVERSION") }) + assertTrue(outcome.states.isEmpty()) + assertTrue(suspendedStates.isNotEmpty()) + assertTrue(suspendedStates.all { it.models.isNotEmpty() }) + assertTrue(suspendedStates.all { it.unsupportedReason != null }) + } + + @Test + fun `prefix emission errors remain analysis errors instead of silently lost candidates`() { + val method = getMethod(methodName = "arrayPush", className = "ArrayMethods") + val stoppedObserver = TsStoppedStatesObserver { error("candidate sink failed") } + val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) + + val failure = assertFailsWith { + TsMachine( + scene = scene, + options = options(), + tsOptions = tsOptions, + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + } + } + + assertEquals(expected = "candidate sink failed", actual = failure.message) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt new file mode 100644 index 0000000000..a57b056b0b --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt @@ -0,0 +1,251 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.util.TsMethodTestRunner +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertSame +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** Low-level queue and lifecycle contracts; real-source native coverage is checked by the Calls adapter. */ +class TsMachineSuspendedStatesTest : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/StaticOverloads.ts") + + @Test + fun `step limit emits unfinished states after stopping without running another step`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val lifecycle = mutableListOf() + var steps = 0 + var terminalStates = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + terminalStates++ + } + + override fun onMachineStopped() { + lifecycle += "stopped" + } + } + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + stepLimit = 1uL, + ) + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { state -> + suspendedStates += state + lifecycle += "suspended" + } + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + assertTrue(suspendedStates.isEmpty()) + stoppedObserver.collectRemainingStates() + result + } + + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = outcome.stopReason) + assertFalse(outcome.timedOut) + assertEquals(expected = 1, actual = steps) + assertEquals(expected = 0, actual = terminalStates) + assertTrue(outcome.states.isEmpty()) + assertEquals(expected = listOf("stopped", "suspended"), actual = lifecycle) + + val suspended = suspendedStates.single() + assertSame(method, suspended.entrypoint) + assertTrue(suspended.callStack.isNotEmpty()) + assertTrue(suspended.models.isNotEmpty()) + val returnedFromEntryPoint = (suspended.methodResult as? TsMethodResult.Success.RegularCall)?.method == method + assertFalse(returnedFromEntryPoint) + } + + @Test + fun `zero timeout exposes the unexecuted initial state as a suspended input`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + var steps = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.ZERO, + ) + + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithOutcome(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } + + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = outcome.stopReason) + assertEquals(expected = 0, actual = steps) + assertTrue(outcome.states.isEmpty()) + assertSame(method, suspendedStates.single().entrypoint) + assertTrue(suspendedStates.single().models.isNotEmpty()) + } + + @Test + fun `analysis without a stopped state observer retains ordinary witness behavior`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + stepLimit = 1uL, + ) + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + } + + @Test + fun `path exhaustion keeps terminal witnesses and has no suspended states`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) + assertTrue(outcome.states.isNotEmpty()) + assertTrue(suspendedStates.isEmpty()) + } + + @Test + fun `exceptional machine stop does not emit queued inputs`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + val observer = object : UMachineObserver { + override fun onStatePeeked(state: TsState) { + error("machine step observer failed") + } + } + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + val failure = assertFailsWith { + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + } + } + + assertEquals(expected = "machine step observer failed", actual = failure.message) + assertTrue(suspendedStates.isEmpty()) + } + + @Test + fun `queued input sink failure remains visible after a timeout`() { + val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") + val stoppedObserver = TsStoppedStatesObserver { error("queued input sink failed") } + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.ZERO, + ) + + val failure = assertFailsWith { + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + assertTrue(result.timedOut) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = result.stopReason) + stoppedObserver.collectRemainingStates() + } + } + + assertEquals(expected = "queued input sink failed", actual = failure.message) + } + + @Test + fun `empty analysis has no stopped states to collect`() { + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + + val outcome = TsMachine( + scene = scene, + tsOptions = TsOptions(), + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = emptyList()) + stoppedObserver.collectRemainingStates() + result + } + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(suspendedStates.isEmpty()) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallStoppedPrefixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallStoppedPrefixTest.kt new file mode 100644 index 0000000000..ac2217f04d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallStoppedPrefixTest.kt @@ -0,0 +1,359 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UBoolExpr +import org.usvm.UMachineOptions +import org.usvm.isTrue +import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.model.UModelBase +import org.usvm.solver.USatResult +import org.usvm.solver.UUnsatResult +import org.usvm.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsUnknownCallStoppedPrefixTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/baseline/CallFallbackBaseline.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val fullScene = EtsScene(listOf(sourceFile)) + + @Test + fun `stop fallback reports a feasible live prefix before pruning`() { + val observer = RecordingStoppedPathObserver() + + val states = analyzeAllStates( + methodName = "declaredMethodWithoutBodyContinues", + fallback = TsResidualCallPolicy.STOP_PATH, + models = noModels, + observer = observer, + ) + + assertTrue(states.isEmpty()) + val prefix = observer.paths.single() + assertTrue(prefix.wasFeasible) + assertFalse(prefix.state.pathConstraints.isFalse) + assertTrue(prefix.state.callStack.isNotEmpty()) + val event = observer.events.single() + val pendingCall = assertIs(prefix.state.currentStatement) + assertEquals(expected = event.callSite, actual = pendingCall.returnSite) + assertEquals(expected = event.callSite.location, actual = pendingCall.location) + assertEquals(expected = event.callee, actual = pendingCall.callee.signature) + assertTrue(prefix.reason.contains(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE.name)) + assertEquals(expected = listOf("stopped-prefix", "PATH_STOPPED"), actual = observer.notifications) + } + + @Test + fun `partial stop callback preserves the feasible residual guard before model forking`() { + val observer = RecordingStoppedPathObserver() + var supportedGuard: UBoolExpr? = null + val model = object : TestModel(id = "residual-prefix-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val condition = requireNotNull(call.arguments.single().resolved).asExpr(state.ctx.boolSort) + supportedGuard = condition + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { + requireNotNull(call.arguments.single().resolved) + }, + ) + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), + ) + } + } + val method = method(fullScene, "modeledUnknownCallForks") + + TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.STOP_PATH), + observer = observer, + unknownCallModels = catalog(model), + ).use { machine -> + val states = machine.analyze(methods = listOf(method)) + + assertEquals(expected = 1, actual = states.size) + val prefix = observer.paths.single() + assertTrue(prefix.wasFeasible) + assertFalse(prefix.state.pathConstraints.isFalse) + assertTrue(prefix.state.callStack.isNotEmpty()) + val residual = prefix.state.ctx.mkNot(requireNotNull(supportedGuard)) + assertTrue(prefix.state.models.isNotEmpty()) + assertTrue(prefix.state.models.all { it.eval(residual).isTrue }) + val feasibility = prefix.state.ctx.solver().check(prefix.state.pathConstraints) + assertIs>(feasibility) + + val overlappingConstraints = prefix.state.pathConstraints.clone() + overlappingConstraints += requireNotNull(supportedGuard) + val overlap = prefix.state.ctx.solver().check(overlappingConstraints) + assertIs>(overlap) + assertEquals( + expected = listOf("stopped-prefix", "MODEL_APPLIED", "PATH_STOPPED"), + actual = observer.notifications, + ) + } + } + + @Test + fun `residual prefix discards cached models outside its guard`() { + val observer = RecordingStoppedPathObserver() + var residualGuard: UBoolExpr? = null + var cachedModelOrder = emptyList() + val model = object : TestModel(id = "cached-residual-prefix-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val value = requireNotNull(call.arguments.single().resolved) + val condition = value.asExpr(state.ctx.boolSort) + val residual = state.ctx.mkNot(condition) + residualGuard = residual + + // Seed two feasible cached models deliberately in the wrong order for residual extraction. + fun modelFor(guard: UBoolExpr): UModelBase { + val constraints = state.pathConstraints.clone() + constraints += guard + return when (val result = state.ctx.solver().check(constraints)) { + is USatResult -> result.model + else -> error("Both Boolean domains must be feasible in this dispatcher fixture") + } + } + val supportedModel = modelFor(guard = condition) + val residualModel = modelFor(guard = residual) + state.models = listOf(supportedModel, residualModel) + cachedModelOrder = state.models.map { it.eval(condition).isTrue } + + return TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { value }, + ), + ), + residualGuard = residual, + ) + } + } + + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + fallback = TsResidualCallPolicy.STOP_PATH, + models = catalog(model), + observer = observer, + ) + + assertEquals(expected = listOf(true, false), actual = cachedModelOrder) + assertEquals(expected = 1, actual = states.size) + val prefix = observer.paths.single().state + val guard = requireNotNull(residualGuard) + assertTrue(prefix.models.isNotEmpty()) + assertTrue(prefix.models.first().eval(guard).isTrue) + assertTrue(prefix.models.all { it.eval(guard).isTrue }) + assertEquals(expected = 1, actual = prefix.models.size) + } + + @Test + fun `unsatisfiable model residual never reports a stopped prefix`() { + val observer = RecordingStoppedPathObserver() + val model = object : TestModel(id = "unsat-residual-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val execution = ForkingModel.apply(state = state, call = call) + return TsUnknownCallModelExecution( + successors = execution.successors, + residualGuard = state.ctx.falseExpr, + ) + } + } + + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + fallback = TsResidualCallPolicy.STOP_PATH, + models = catalog(model), + observer = observer, + ) + + assertEquals(expected = 2, actual = states.size) + assertTrue(observer.paths.isEmpty()) + assertEquals(expected = listOf("MODEL_APPLIED"), actual = observer.notifications) + } + + @Test + fun `throwing stopped path observer does not change fallback or partial exploration`() { + val cases = listOf( + ObservationFailureCase( + fallback = TsResidualCallPolicy.STOP_PATH, + models = noModels, + expectedFinalStateCount = 0, + ), + ObservationFailureCase( + fallback = TsResidualCallPolicy.STOP_PATH, + models = catalog(SupportedTrueResidualFalseModel), + expectedFinalStateCount = 1, + methodName = "modeledUnknownCallForks", + ), + ) + for (case in cases) { + var stoppedCount = 0 + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onPathStopped(state: TsState, reason: String) { + stoppedCount++ + error("stopped-prefix observer failure") + } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val states = analyzeAllStates( + methodName = case.methodName, + fallback = case.fallback, + models = case.models, + observer = observer, + ) + + assertEquals(expected = case.expectedFinalStateCount, actual = states.size) + assertEquals(expected = 1, actual = stoppedCount) + assertEquals(expected = TsUnknownCallOutcome.PATH_STOPPED, actual = events.last().outcome) + } + } + + private fun method( + scene: EtsScene, + methodName: String, + className: String = "CallFallbackBaseline", + ): EtsMethod = scene.projectClasses + .single { it.name == className } + .methods + .single { it.name == methodName } + + private fun analyzeAllStates( + methodName: String, + fallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, + models: TsUnknownCallModelCatalog = noModels, + observer: TsInterpreterObserver? = null, + ): List { + val method = method(fullScene, methodName) + return TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(unknownCallFallback = fallback), + observer = observer, + unknownCallModels = models, + ).use { machine -> + machine.analyze(listOf(method)) + } + } + + private object ForkingModel : TestModel(id = "forking-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val result = requireNotNull(call.arguments.single().resolved) + val condition = result.asExpr(state.ctx.boolSort) + val completion = TsUnknownCallModelCompletion.Normal { result } + + return TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = condition, + completion = completion, + ), + TsUnknownCallModelSuccessor( + guard = state.ctx.mkNot(condition), + completion = completion, + ), + ), + ) + } + } + + private object SupportedTrueResidualFalseModel : TestModel(id = "partial-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val result = requireNotNull(call.arguments.single().resolved) + val condition = result.asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), + ) + } + } + + private abstract class TestModel( + override val id: String, + methodName: String, + enclosingClassName: String? = null, + ) : TsUnknownCallModel { + override val target = TsUnknownCallTarget(methodName = methodName, enclosingClassName = enclosingClassName) + } + + private class RecordingStoppedPathObserver : TsInterpreterObserver { + val paths = mutableListOf() + val events = mutableListOf() + val notifications = mutableListOf() + + override fun onPathStopped(state: TsState, reason: String) { + val wasFeasible = !state.pathConstraints.isFalse + paths += StoppedPathSnapshot(state = state.clone(), reason = reason, wasFeasible = wasFeasible) + notifications += "stopped-prefix" + } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + notifications += event.outcome.name + } + } + + private data class StoppedPathSnapshot( + val state: TsState, + val reason: String, + val wasFeasible: Boolean, + ) + + private data class ObservationFailureCase( + val fallback: TsResidualCallPolicy, + val models: TsUnknownCallModelCatalog, + val expectedFinalStateCount: Int, + val methodName: String = "declaredMethodWithoutBodyContinues", + ) + + private companion object { + val noModels = TsUnknownCallModelCatalog(emptyList()) + + fun catalog(vararg models: TsUnknownCallModel): TsUnknownCallModelCatalog = + TsUnknownCallModelCatalog(models.toList()) + + val allStatesMachineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + exceptionsPropagation = true, + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + stopOnTargetsReached = false, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt new file mode 100644 index 0000000000..922edac6ad --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt @@ -0,0 +1,23 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.test.util.checkers.eq as exactly + +class VoidAssignment : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/VoidAssignment.ts") + + @Test + fun `assigned void call returns undefined after its mutation`() { + val method = getMethod("assignmentResult") + + checkMatches( + method = method, + analysisResultNumberMatches = exactly(1), + { result -> result eq 1 }, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts b/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts new file mode 100644 index 0000000000..26107ae476 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts @@ -0,0 +1,22 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class VoidMutation { + value: number = 0; + + change(): void { + this.value = 7; + } +} + +class VoidAssignment { + assignmentResult(): number { + const instance = new VoidMutation(); + const result = instance.change(); + const observation = { result, value: instance.value }; + if (observation.result === undefined && observation.value === 7) { + return 1; + } + return 0; + } +}