From 2f9b7d82ecb597ec65ba83afbedb9c107a9b51e4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 18:24:58 +0300 Subject: [PATCH 1/3] Retain feasible prefixes and queued inputs when TypeScript analysis stops --- usvm-core/src/main/kotlin/org/usvm/Machine.kt | 14 +- .../org/usvm/statistics/UMachineObserver.kt | 10 + .../stopstrategies/StepLimitStopStrategy.kt | 2 +- .../main/kotlin/org/usvm/utils/StateUtils.kt | 3 +- .../org/usvm/machine/TsInterpreterObserver.kt | 9 + .../main/kotlin/org/usvm/machine/TsMachine.kt | 112 +++++- .../call/TsUnknownCallModelDispatcher.kt | 24 +- .../usvm/machine/TsMachineStoppedPathsTest.kt | 106 ++++++ .../machine/TsMachineSuspendedStatesTest.kt | 145 +++++++ .../call/TsUnknownCallStoppedPrefixTest.kt | 359 ++++++++++++++++++ .../main/kotlin/org/usvm/UMachineOptions.kt | 6 + 11 files changed, 762 insertions(+), 28 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallStoppedPrefixTest.kt diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt index 775fd5b989..9b40b796d6 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt @@ -28,6 +28,7 @@ abstract class UMachine> : AutoCloseable { * won't be analyzed further. It is called on an original state and every forked state as well. * @param stopStrategy is called on every step, before peeking a next state from the path selector. * Returning `true` aborts analysis. + * @return whether execution exhausted its queued states before any optional suspended-state emission. */ protected fun run( interpreter: UInterpreter, @@ -35,8 +36,8 @@ abstract class UMachine> : AutoCloseable { observer: UMachineObserver, isStateTerminated: (State) -> Boolean, stopStrategy: StopStrategy = StopStrategy { false } - ) { - logger.debug().bracket("$this.run($interpreter, ${pathSelector::class.simpleName})") { + ): Boolean { + return logger.debug().bracket("$this.run($interpreter, ${pathSelector::class.simpleName})") { observer.onMachineStarted() try { while (!pathSelector.isEmpty() && !stopStrategy.shouldStop()) { @@ -90,10 +91,17 @@ abstract class UMachine> : AutoCloseable { observer.onMachineStopped() } - if (!pathSelector.isEmpty()) { + val exhaustedBeforeFlush = pathSelector.isEmpty() + if (!exhaustedBeforeFlush) { val stopReason = stopStrategy.stopReason() logger.debug { stopReason } + + if (options.emitRemainingStatesOnStop) { + pathSelector.drain().forEach(observer::onStateSuspended) + } } + + exhaustedBeforeFlush } } diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt index 4185629ad7..da1eedd569 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt @@ -20,6 +20,12 @@ interface UMachineObserver { */ fun onStateTerminated(state: State, stateReachable: Boolean) { } + /** + * Called for a nonterminal input retained at a frontend execution boundary or after normal machine stop. + * Queued-state emission performs no additional execution or satisfiability checks. + */ + fun onStateSuspended(state: State) { } + /** * Called on each symbolic execution step. If the state has forked, [forks] are not empty. */ @@ -48,6 +54,10 @@ class CompositeUMachineObserver( observers.forEach { it.onStateTerminated(state, stateReachable) } } + override fun onStateSuspended(state: State) { + observers.forEach { it.onStateSuspended(state) } + } + override fun onState(parent: State, forks: Sequence) { observers.forEach { it.onState(parent, forks) } } 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/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..d74fa0d764 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 @@ -56,9 +58,11 @@ data class TsAnalysisResult( val stopReason: TsAnalysisStopReason, /** Reasons for satisfiable paths excluded by an explicit engine model bound. */ val unsupportedPaths: List, + /** Live inputs at an execution limit; these states have not completed their entry point. */ + val suspendedStates: List = emptyList(), ) -/** Terminal states and failure metadata for one TypeScript analysis. */ +/** Terminal states, suspended inputs and failure metadata for one TypeScript analysis. */ data class TsMachineAnalysisResult( val states: List, val stopReason: TsAnalysisStopReason, @@ -66,6 +70,8 @@ data class TsMachineAnalysisResult( val unsupportedCall: Boolean, val engineFailed: Boolean, val unsupportedPaths: List, + /** Feasible stopped prefixes and queued states at limits, separately from completed witnesses. */ + val suspendedStates: List = emptyList(), ) { /** Includes execution bounds and unsupported entry inputs retained in [unsupportedPaths]. */ val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() @@ -160,6 +166,7 @@ class TsMachine( states = result.states, stopReason = result.stopReason, unsupportedPaths = result.unsupportedPaths, + suspendedStates = result.suspendedStates, ) } @@ -214,18 +221,12 @@ 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 suspendedStatesCollector = SuspendedStatesCollector() val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) + observers.add(suspendedStatesCollector) if (tsOptions.enableVisualization) { observers += TsStateVisualizer() } @@ -283,17 +284,18 @@ class TsMachine( } val supportedObserver = CompositeUMachineObserver(observers) - val outcomeObserver = UnsupportedPathsObserver(supportedObserver, unsupportedPaths) - - run( - interpreter, - pathSelector, + val outcomeObserver = UnsupportedPathsObserver( + delegate = supportedObserver, + unsupportedPaths = unsupportedPaths, + emitStoppedPaths = options.emitRemainingStatesOnStop, + ) + val exhausted = runWithStoppedPathEmission( + pathSelector = pathSelector, observer = outcomeObserver, - isStateTerminated = { state -> state.callStack.isEmpty() }, - stopStrategy = stopStrategy + stopStrategy = stopStrategy, ) - val stopReason = if (pathSelector.isEmpty()) { + val stopReason = if (exhausted) { TsAnalysisStopReason.EXHAUSTED } else { TsAnalysisStopReason.STOPPED @@ -306,9 +308,55 @@ class TsMachine( unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, engineFailed = interpreter.stepFailed, unsupportedPaths = unsupportedPaths.toList(), + suspendedStates = suspendedStatesCollector.states.toList(), ) } + 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 runWithStoppedPathEmission( + pathSelector: UPathSelector, + observer: UMachineObserver, + stopStrategy: StopStrategy, + ): Boolean { + failureTrackingUnknownCallObserver.onPathStoppedListener = if (options.emitRemainingStatesOnStop) { + { state, reason -> + // STOP_PATH prunes the original next: retain its feasible prefix before that mutation. + val prefix = state.clone() + prefix.unsupportedReason = reason + observer.onStateSuspended(prefix) + } + } else { + null + } + + val exhausted = try { + run( + interpreter = interpreter, + pathSelector = pathSelector, + observer = observer, + isStateTerminated = { state -> state.callStack.isEmpty() }, + stopStrategy = stopStrategy, + ) + } finally { + failureTrackingUnknownCallObserver.onPathStoppedListener = null + } + val emissionFailure = failureTrackingUnknownCallObserver.pathEmissionFailure + if (emissionFailure != null) { + throw emissionFailure + } + + return exhausted + } + private fun classCoverageMethods(entryMethods: Set): Set { val targets = tsOptions.classCoverageTargets val classes = if (targets == null) { @@ -372,12 +420,35 @@ class TsMachine( } } +private class SuspendedStatesCollector : UMachineObserver { + val states = mutableListOf() + + override fun onStateSuspended(state: TsState) { + states += state + } +} + private class FailureTrackingUnknownCallObserver( private val delegate: TsInterpreterObserver?, ) : TsInterpreterObserver { var pathStopped: Boolean = false private set + var onPathStoppedListener: ((TsState, String) -> Unit)? = null + + var pathEmissionFailure: Throwable? = null + private set + + override fun onPathStopped(state: TsState, reason: String) { + val emission = runCatching { onPathStoppedListener?.invoke(state, reason) } + val failure = emission.exceptionOrNull() + if (failure != null && pathEmissionFailure == null) { + pathEmissionFailure = failure + } + + delegate?.onPathStopped(state, reason) + } + override fun onUnknownCall(event: TsUnknownCallEvent) { val decision = event.decision val stopsPath = decision is TsUnknownCallDecision.ResidualFallback && @@ -391,6 +462,7 @@ private class FailureTrackingUnknownCallObserver( fun reset() { pathStopped = false + pathEmissionFailure = null } } @@ -398,12 +470,16 @@ private class FailureTrackingUnknownCallObserver( private class UnsupportedPathsObserver( private val delegate: UMachineObserver, private val unsupportedPaths: MutableSet, + private val emitStoppedPaths: Boolean, ) : UMachineObserver by delegate { override fun onStateTerminated(state: TsState, stateReachable: Boolean) { val unsupportedReason = state.unsupportedReason if (unsupportedReason != null) { if (stateReachable) { unsupportedPaths += unsupportedReason + if (emitStoppedPaths) { + delegate.onStateSuspended(state) + } } return } 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..7d87d7a7bb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt @@ -0,0 +1,106 @@ +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.statistics.UMachineObserver +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(emit: Boolean) = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + emitRemainingStatesOnStop = emit, + ) + + @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 outcome = TsMachine( + scene = scene, + options = options(emit = true), + tsOptions = tsOptions, + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedCall) + assertFalse(outcome.engineFailed) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.suspendedStates.isNotEmpty()) + assertTrue(outcome.suspendedStates.all { it.models.isNotEmpty() }) + assertTrue(outcome.suspendedStates.all { it.callStack.isNotEmpty() }) + assertTrue(outcome.suspendedStates.all { it.unsupportedReason?.contains("push") == true }) + } + + @Test + fun `stopped path collection stays disabled by default`() { + val method = getMethod(methodName = "arrayPush", className = "ArrayMethods") + val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) + + val outcome = TsMachine( + scene = scene, + options = options(emit = false), + tsOptions = tsOptions, + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(outcome.unsupportedCall) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.suspendedStates.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 outcome = TsMachine( + scene = stringScene, + options = options(emit = true), + tsOptions = TsOptions(), + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(outcome.runtimeLimited) + assertTrue(outcome.unsupportedPaths.any { it.contains("STRING_CONCAT_OPERAND_CONVERSION") }) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.suspendedStates.isNotEmpty()) + assertTrue(outcome.suspendedStates.all { it.models.isNotEmpty() }) + assertTrue(outcome.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 observer = object : UMachineObserver { + override fun onStateSuspended(state: TsState) { + error("candidate sink failed") + } + } + val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) + + val failure = assertFailsWith { + TsMachine( + scene = scene, + options = options(emit = true), + tsOptions = tsOptions, + machineObserver = observer, + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + } + + 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..b4e379ae47 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt @@ -0,0 +1,145 @@ +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.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" + } + + override fun onStateSuspended(state: TsState) { + lifecycle += "suspended" + } + } + val options = UMachineOptions( + solverType = SolverType.YICES, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + stepLimit = 1uL, + emitRemainingStatesOnStop = true, + ) + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.STOPPED, 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 = outcome.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, + emitRemainingStatesOnStop = true, + ) + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> machine.analyzeWithOutcome(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.STOPPED, outcome.stopReason) + assertEquals(expected = 0, actual = steps) + assertTrue(outcome.states.isEmpty()) + assertSame(method, outcome.suspendedStates.single().entrypoint) + assertTrue(outcome.suspendedStates.single().models.isNotEmpty()) + } + + @Test + fun `suspended state emission is opt in`() { + 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(TsAnalysisStopReason.STOPPED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.suspendedStates.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, + emitRemainingStatesOnStop = true, + ) + + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isNotEmpty()) + assertTrue(outcome.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-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt index 0784b8d18f..497f3fd5b0 100644 --- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt @@ -273,4 +273,10 @@ data class UMachineOptions( * Disable this for budget/exhaustion experiments that must retain those states between turns. */ val removeCoveredEntryPoints: Boolean = true, + /** + * Emit interrupted inputs through the nonterminal observer callback. The core flushes queued states + * after a normal stop; frontends can also retain feasible prefixes at unsupported execution boundaries. + * Draining does not execute additional interpreter steps or check state satisfiability. + */ + val emitRemainingStatesOnStop: Boolean = false, ) From c4f0698b5a7274a50223156ce1f584bf09e9406c Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 14 Oct 2026 18:59:37 +0300 Subject: [PATCH 2/3] Store TypeScript void results as undefined values (#503) --- .../main/kotlin/org/usvm/machine/TsContext.kt | 2 ++ .../org/usvm/samples/lang/VoidAssignment.kt | 23 +++++++++++++++++++ .../resources/samples/lang/VoidAssignment.ts | 22 ++++++++++++++++++ 3 files changed, 47 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt create mode 100644 usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts 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/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; + } +} From 2b7355bf058f2ce24add3cb99272330c69e1cfe5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 19:26:10 +0300 Subject: [PATCH 3/3] Collect stopped TypeScript inputs through observers Preserve the Unit-returning machine loop and shared observer API. Bind an optional TS observer to each analysis queue and let the caller collect unfinished inputs after successful analysis, while retaining unknown-call prefixes before pruning. --- usvm-core/src/main/kotlin/org/usvm/Machine.kt | 14 +- .../org/usvm/statistics/UMachineObserver.kt | 10 -- .../main/kotlin/org/usvm/machine/TsMachine.kt | 89 ++--------- .../usvm/machine/TsStoppedStatesObserver.kt | 65 ++++++++ .../usvm/machine/TsMachineStoppedPathsTest.kt | 67 ++++---- .../machine/TsMachineSuspendedStatesTest.kt | 146 +++++++++++++++--- .../main/kotlin/org/usvm/UMachineOptions.kt | 6 - 7 files changed, 251 insertions(+), 146 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsStoppedStatesObserver.kt diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt index 9b40b796d6..775fd5b989 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt @@ -28,7 +28,6 @@ abstract class UMachine> : AutoCloseable { * won't be analyzed further. It is called on an original state and every forked state as well. * @param stopStrategy is called on every step, before peeking a next state from the path selector. * Returning `true` aborts analysis. - * @return whether execution exhausted its queued states before any optional suspended-state emission. */ protected fun run( interpreter: UInterpreter, @@ -36,8 +35,8 @@ abstract class UMachine> : AutoCloseable { observer: UMachineObserver, isStateTerminated: (State) -> Boolean, stopStrategy: StopStrategy = StopStrategy { false } - ): Boolean { - return logger.debug().bracket("$this.run($interpreter, ${pathSelector::class.simpleName})") { + ) { + logger.debug().bracket("$this.run($interpreter, ${pathSelector::class.simpleName})") { observer.onMachineStarted() try { while (!pathSelector.isEmpty() && !stopStrategy.shouldStop()) { @@ -91,17 +90,10 @@ abstract class UMachine> : AutoCloseable { observer.onMachineStopped() } - val exhaustedBeforeFlush = pathSelector.isEmpty() - if (!exhaustedBeforeFlush) { + if (!pathSelector.isEmpty()) { val stopReason = stopStrategy.stopReason() logger.debug { stopReason } - - if (options.emitRemainingStatesOnStop) { - pathSelector.drain().forEach(observer::onStateSuspended) - } } - - exhaustedBeforeFlush } } diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt index da1eedd569..4185629ad7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt @@ -20,12 +20,6 @@ interface UMachineObserver { */ fun onStateTerminated(state: State, stateReachable: Boolean) { } - /** - * Called for a nonterminal input retained at a frontend execution boundary or after normal machine stop. - * Queued-state emission performs no additional execution or satisfiability checks. - */ - fun onStateSuspended(state: State) { } - /** * Called on each symbolic execution step. If the state has forked, [forks] are not empty. */ @@ -54,10 +48,6 @@ class CompositeUMachineObserver( observers.forEach { it.onStateTerminated(state, stateReachable) } } - override fun onStateSuspended(state: State) { - observers.forEach { it.onStateSuspended(state) } - } - override fun onState(parent: State, forks: Sequence) { observers.forEach { it.onState(parent, forks) } } 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 d74fa0d764..85b3bd587c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -58,11 +58,9 @@ data class TsAnalysisResult( val stopReason: TsAnalysisStopReason, /** Reasons for satisfiable paths excluded by an explicit engine model bound. */ val unsupportedPaths: List, - /** Live inputs at an execution limit; these states have not completed their entry point. */ - val suspendedStates: List = emptyList(), ) -/** Terminal states, suspended inputs and failure metadata for one TypeScript analysis. */ +/** Terminal states and failure metadata for one TypeScript analysis. */ data class TsMachineAnalysisResult( val states: List, val stopReason: TsAnalysisStopReason, @@ -70,8 +68,6 @@ data class TsMachineAnalysisResult( val unsupportedCall: Boolean, val engineFailed: Boolean, val unsupportedPaths: List, - /** Feasible stopped prefixes and queued states at limits, separately from completed witnesses. */ - val suspendedStates: List = emptyList(), ) { /** Includes execution bounds and unsupported entry inputs retained in [unsupportedPaths]. */ val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() @@ -85,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 || @@ -166,7 +164,6 @@ class TsMachine( states = result.states, stopReason = result.stopReason, unsupportedPaths = result.unsupportedPaths, - suspendedStates = result.suspendedStates, ) } @@ -223,10 +220,8 @@ class TsMachine( val statesCollector = createStatesCollector(coverageStatistics) - val suspendedStatesCollector = SuspendedStatesCollector() val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) - observers.add(suspendedStatesCollector) if (tsOptions.enableVisualization) { observers += TsStateVisualizer() } @@ -287,15 +282,23 @@ class TsMachine( val outcomeObserver = UnsupportedPathsObserver( delegate = supportedObserver, unsupportedPaths = unsupportedPaths, - emitStoppedPaths = options.emitRemainingStatesOnStop, ) - val exhausted = runWithStoppedPathEmission( + val factoryObserver = machineObserverFactory?.invoke(pathSelector) + val executionObserver = if (factoryObserver == null) { + outcomeObserver + } else { + CompositeUMachineObserver(outcomeObserver, factoryObserver) + } + + run( + interpreter = interpreter, pathSelector = pathSelector, - observer = outcomeObserver, + observer = executionObserver, + isStateTerminated = { state -> state.callStack.isEmpty() }, stopStrategy = stopStrategy, ) - val stopReason = if (exhausted) { + val stopReason = if (pathSelector.isEmpty()) { TsAnalysisStopReason.EXHAUSTED } else { TsAnalysisStopReason.STOPPED @@ -308,7 +311,6 @@ class TsMachine( unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, engineFailed = interpreter.stepFailed, unsupportedPaths = unsupportedPaths.toList(), - suspendedStates = suspendedStatesCollector.states.toList(), ) } @@ -322,41 +324,6 @@ class TsMachine( StateCollectionStrategy.ALL -> AllStatesCollector() } - private fun runWithStoppedPathEmission( - pathSelector: UPathSelector, - observer: UMachineObserver, - stopStrategy: StopStrategy, - ): Boolean { - failureTrackingUnknownCallObserver.onPathStoppedListener = if (options.emitRemainingStatesOnStop) { - { state, reason -> - // STOP_PATH prunes the original next: retain its feasible prefix before that mutation. - val prefix = state.clone() - prefix.unsupportedReason = reason - observer.onStateSuspended(prefix) - } - } else { - null - } - - val exhausted = try { - run( - interpreter = interpreter, - pathSelector = pathSelector, - observer = observer, - isStateTerminated = { state -> state.callStack.isEmpty() }, - stopStrategy = stopStrategy, - ) - } finally { - failureTrackingUnknownCallObserver.onPathStoppedListener = null - } - val emissionFailure = failureTrackingUnknownCallObserver.pathEmissionFailure - if (emissionFailure != null) { - throw emissionFailure - } - - return exhausted - } - private fun classCoverageMethods(entryMethods: Set): Set { val targets = tsOptions.classCoverageTargets val classes = if (targets == null) { @@ -420,33 +387,14 @@ class TsMachine( } } -private class SuspendedStatesCollector : UMachineObserver { - val states = mutableListOf() - - override fun onStateSuspended(state: TsState) { - states += state - } -} - private class FailureTrackingUnknownCallObserver( private val delegate: TsInterpreterObserver?, ) : TsInterpreterObserver { var pathStopped: Boolean = false private set - var onPathStoppedListener: ((TsState, String) -> Unit)? = null - - var pathEmissionFailure: Throwable? = null - private set - override fun onPathStopped(state: TsState, reason: String) { - val emission = runCatching { onPathStoppedListener?.invoke(state, reason) } - val failure = emission.exceptionOrNull() - if (failure != null && pathEmissionFailure == null) { - pathEmissionFailure = failure - } - - delegate?.onPathStopped(state, reason) + delegate?.onPathStopped(state = state, reason = reason) } override fun onUnknownCall(event: TsUnknownCallEvent) { @@ -462,7 +410,6 @@ private class FailureTrackingUnknownCallObserver( fun reset() { pathStopped = false - pathEmissionFailure = null } } @@ -470,16 +417,12 @@ private class FailureTrackingUnknownCallObserver( private class UnsupportedPathsObserver( private val delegate: UMachineObserver, private val unsupportedPaths: MutableSet, - private val emitStoppedPaths: Boolean, ) : UMachineObserver by delegate { override fun onStateTerminated(state: TsState, stateReachable: Boolean) { val unsupportedReason = state.unsupportedReason if (unsupportedReason != null) { if (stateReachable) { unsupportedPaths += unsupportedReason - if (emitStoppedPaths) { - delegate.onStateSuspended(state) - } } return } 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/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt index 7d87d7a7bb..f0a3815c0d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineStoppedPathsTest.kt @@ -6,7 +6,6 @@ import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.state.TsState -import org.usvm.statistics.UMachineObserver import org.usvm.util.TsMethodTestRunner import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -18,11 +17,10 @@ import kotlin.time.Duration class TsMachineStoppedPathsTest : TsMethodTestRunner() { override val scene: EtsScene = loadScene("/samples/arrays/ArrayMethods.ts") - private fun options(emit: Boolean) = UMachineOptions( + private fun options() = UMachineOptions( solverType = SolverType.YICES, stopOnCoverage = 0, timeout = Duration.INFINITE, - emitRemainingStatesOnStop = emit, ) @Test @@ -30,36 +28,44 @@ class TsMachineStoppedPathsTest : TsMethodTestRunner() { 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(emit = true), + options = options(), tsOptions = tsOptions, - ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } - assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) assertTrue(outcome.unsupportedCall) assertFalse(outcome.engineFailed) assertTrue(outcome.states.isEmpty()) - assertTrue(outcome.suspendedStates.isNotEmpty()) - assertTrue(outcome.suspendedStates.all { it.models.isNotEmpty() }) - assertTrue(outcome.suspendedStates.all { it.callStack.isNotEmpty() }) - assertTrue(outcome.suspendedStates.all { it.unsupportedReason?.contains("push") == true }) + 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 `stopped path collection stays disabled by default`() { + 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(emit = false), + options = options(), tsOptions = tsOptions, ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } assertTrue(outcome.unsupportedCall) assertTrue(outcome.states.isEmpty()) - assertTrue(outcome.suspendedStates.isEmpty()) } @Test @@ -68,37 +74,46 @@ class TsMachineStoppedPathsTest : TsMethodTestRunner() { 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(emit = true), + options = options(), tsOptions = TsOptions(), - ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + 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(outcome.suspendedStates.isNotEmpty()) - assertTrue(outcome.suspendedStates.all { it.models.isNotEmpty() }) - assertTrue(outcome.suspendedStates.all { it.unsupportedReason != null }) + 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 observer = object : UMachineObserver { - override fun onStateSuspended(state: TsState) { - error("candidate sink failed") - } - } + val stoppedObserver = TsStoppedStatesObserver { error("candidate sink failed") } val tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())) val failure = assertFailsWith { TsMachine( scene = scene, - options = options(emit = true), + options = options(), tsOptions = tsOptions, - machineObserver = observer, - ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + 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 index b4e379ae47..a57b056b0b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineSuspendedStatesTest.kt @@ -9,6 +9,7 @@ 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 @@ -36,34 +37,41 @@ class TsMachineSuspendedStatesTest : TsMethodTestRunner() { override fun onMachineStopped() { lifecycle += "stopped" } - - override fun onStateSuspended(state: TsState) { - lifecycle += "suspended" - } } val options = UMachineOptions( solverType = SolverType.YICES, stopOnCoverage = 0, timeout = Duration.INFINITE, stepLimit = 1uL, - emitRemainingStatesOnStop = true, ) + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { state -> + suspendedStates += state + lifecycle += "suspended" + } val outcome = TsMachine( scene = scene, options = options, tsOptions = TsOptions(), machineObserver = observer, - ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + assertTrue(suspendedStates.isEmpty()) + stoppedObserver.collectRemainingStates() + result + } - assertEquals(TsAnalysisStopReason.STOPPED, outcome.stopReason) + 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 = outcome.suspendedStates.single() + val suspended = suspendedStates.single() assertSame(method, suspended.entrypoint) assertTrue(suspended.callStack.isNotEmpty()) assertTrue(suspended.models.isNotEmpty()) @@ -84,25 +92,33 @@ class TsMachineSuspendedStatesTest : TsMethodTestRunner() { solverType = SolverType.YICES, stopOnCoverage = 0, timeout = Duration.ZERO, - emitRemainingStatesOnStop = true, ) + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + val outcome = TsMachine( scene = scene, options = options, tsOptions = TsOptions(), machineObserver = observer, - ).use { machine -> machine.analyzeWithOutcome(methods = listOf(method)) } + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithOutcome(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } - assertEquals(TsAnalysisStopReason.STOPPED, outcome.stopReason) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = outcome.stopReason) assertEquals(expected = 0, actual = steps) assertTrue(outcome.states.isEmpty()) - assertSame(method, outcome.suspendedStates.single().entrypoint) - assertTrue(outcome.suspendedStates.single().models.isNotEmpty()) + assertSame(method, suspendedStates.single().entrypoint) + assertTrue(suspendedStates.single().models.isNotEmpty()) } @Test - fun `suspended state emission is opt in`() { + fun `analysis without a stopped state observer retains ordinary witness behavior`() { val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads") val options = UMachineOptions( solverType = SolverType.YICES, @@ -117,9 +133,8 @@ class TsMachineSuspendedStatesTest : TsMethodTestRunner() { tsOptions = TsOptions(), ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } - assertEquals(TsAnalysisStopReason.STOPPED, outcome.stopReason) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = outcome.stopReason) assertTrue(outcome.states.isEmpty()) - assertTrue(outcome.suspendedStates.isEmpty()) } @Test @@ -129,17 +144,108 @@ class TsMachineSuspendedStatesTest : TsMethodTestRunner() { solverType = SolverType.YICES, stopOnCoverage = 0, timeout = Duration.INFINITE, - emitRemainingStatesOnStop = true, ) + val suspendedStates = mutableListOf() + val stoppedObserver = TsStoppedStatesObserver { suspendedStates += it } + val outcome = TsMachine( scene = scene, options = options, tsOptions = TsOptions(), - ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + observer = stoppedObserver, + machineObserverFactory = stoppedObserver::createMachineObserver, + ).use { machine -> + val result = machine.analyzeWithMetadata(methods = listOf(method)) + stoppedObserver.collectRemainingStates() + result + } - assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) assertTrue(outcome.states.isNotEmpty()) - assertTrue(outcome.suspendedStates.isEmpty()) + 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-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt index 497f3fd5b0..0784b8d18f 100644 --- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt @@ -273,10 +273,4 @@ data class UMachineOptions( * Disable this for budget/exhaustion experiments that must retain those states between turns. */ val removeCoveredEntryPoints: Boolean = true, - /** - * Emit interrupted inputs through the nonterminal observer callback. The core flushes queued states - * after a normal stop; frontends can also retain feasible prefixes at unsupported execution boundaries. - * Draining does not execute additional interpreter steps or check state satisfiability. - */ - val emitRemainingStatesOnStop: Boolean = false, )