diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt new file mode 100644 index 0000000000..d416647c4e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt @@ -0,0 +1,51 @@ +package org.usvm.machine + +/** + * One analysis whose queue and statistics survive a phase yield. The owning [TsMachine] must stay open. + * Closing the session discards pending work without closing the machine or its solvers. + */ +class TsAnalysisSession internal constructor( + advancePhase: (ULong?) -> TsMachineAnalysisResult, + analysisFinished: () -> Boolean, + release: () -> Unit, +) : AutoCloseable { + private var advancePhase: ((ULong?) -> TsMachineAnalysisResult)? = advancePhase + private var analysisFinished: (() -> Boolean)? = analysisFinished + private var release: (() -> Unit)? = release + private var advancing = false + + /** True after path exhaustion or a configured analysis limit, rather than a phase yield. */ + val isFinished: Boolean + get() = analysisFinished?.invoke() ?: true + + /** + * Runs at most [maxSteps] additional interpreter steps. Analysis-wide limits remain cumulative. + * A finished analysis returns its last snapshot without executing or notifying observers again. + * Bounded phases currently require one runnable entry point; multi-entry scheduling is uninterrupted. + */ + fun advance(maxSteps: ULong? = null): TsMachineAnalysisResult { + val phase = checkNotNull(advancePhase) { "Analysis session is closed" } + check(!advancing) { "Analysis session is already advancing" } + + advancing = true + var succeeded = false + try { + val result = phase(maxSteps) + succeeded = true + return result + } finally { + advancing = false + if (!succeeded) close() + } + } + + override fun close() { + check(!advancing) { "Cannot close an advancing analysis session" } + val releaseAnalysis = release ?: return + + advancePhase = null + analysisFinished = null + release = null + releaseAnalysis() + } +} 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 80e389983f..32c1df3928 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -143,6 +143,9 @@ class TsMachine( throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) private val cfgStatistics = CfgStatisticsImpl(graph) + private var activeAnalysis: TsAnalysisSession? = null + private var preparingAnalysis = false + private var closed = false /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( @@ -185,7 +188,38 @@ class TsMachine( methods: List, targets: List = emptyList(), configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, - ): TsMachineAnalysisResult { + ): TsMachineAnalysisResult = openAnalysis( + methods = methods, + targets = targets, + configureInitialState = configureInitialState, + ).use { session -> session.advance() } + + /** Prepares one retained analysis; close it before starting another analysis on this machine. */ + fun openAnalysis( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): TsAnalysisSession { + check(!closed) { "Machine is closed" } + check(activeAnalysis == null && !preparingAnalysis) { + "Close the current analysis session before starting another" + } + + preparingAnalysis = true + try { + val session = prepareAnalysis(methods.toList(), targets.toList(), configureInitialState) + activeAnalysis = session + return session + } finally { + preparingAnalysis = false + } + } + + private fun prepareAnalysis( + methods: List, + targets: List, + configureInitialState: (EtsMethod, TsState) -> Unit, + ): TsAnalysisSession { interpreter.resetStepFailure() failureTrackingUnknownCallObserver.reset() @@ -193,52 +227,27 @@ class TsMachine( createInitialStates(methods, targets, configureInitialState) if (initialStates.isEmpty()) { - return emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints) + val result = emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints) + return TsAnalysisSession( + advancePhase = { result }, + analysisFinished = { true }, + release = { activeAnalysis = null }, + ) } - val methodsToTrackCoverage = - when (options.coverageZone) { - CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet() - CoverageZone.CLASS -> classCoverageMethods(entryMethods = initialStates.keys) - } - - val coverageStatistics = CoverageStatistics( - methods = methodsToTrackCoverage, - applicationGraph = graph, - ) - - val callGraphStatistics: PlainCallGraphStatistics = - when (options.targetSearchDepth) { - 0u -> PlainCallGraphStatistics() - else -> TODO("Unsupported yet") - } - + val coverageStatistics = createCoverageStatistics(entryMethods = initialStates.keys) val timeStatistics = createTimeStatistics() - - val pathSelector = createPathSelector( + val pathSelector = createAnalysisPathSelector( initialStates = initialStates, - options = options, - applicationGraph = graph, timeStatistics = timeStatistics, - coverageStatisticsFactory = { coverageStatistics }, - cfgStatisticsFactory = { cfgStatistics }, - callGraphStatisticsFactory = { callGraphStatistics }, + coverageStatistics = coverageStatistics, ) val statesCollector = createStatesCollector(coverageStatistics) - val observers = mutableListOf>(coverageStatistics) - observers.add(statesCollector) - if (tsOptions.enableVisualization) { - observers += TsStateVisualizer() - } - - if (options.useSoftConstraints) { - observers.add(SoftConstraintsObserver()) - } - val stepsStatistics = StepsStatistics() var timedOut = false + var finished = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -252,15 +261,14 @@ class TsMachine( override fun shouldStop(): Boolean { if (options.timeout <= kotlin.time.Duration.ZERO) { timedOut = true + finished = true return true } val result = strategy.shouldStop() - if (result && timeStatistics.runningTime >= options.timeout) { - timedOut = true - } - if (result) { + timedOut = timeStatistics.runningTime >= options.timeout + finished = true logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } } @@ -268,6 +276,118 @@ class TsMachine( } } + val supportedObserver = createAnalysisObserver( + initialStates = initialStates, + coverageStatistics = coverageStatistics, + statesCollector = statesCollector, + timeStatistics = timeStatistics, + stepsStatistics = stepsStatistics, + ) + val outcomeObserver = UnsupportedPathsObserver( + delegate = supportedObserver, + unsupportedPaths = unsupportedPaths, + ) + val factoryObserver = machineObserverFactory?.invoke(pathSelector) + val executionObserver = if (factoryObserver == null) { + outcomeObserver + } else { + CompositeUMachineObserver(outcomeObserver, factoryObserver) + } + + var lastResult: TsMachineAnalysisResult? = null + return TsAnalysisSession( + advancePhase = { maxSteps -> + if (finished) { + requireNotNull(lastResult) + } else { + require(maxSteps == null || initialStates.size == 1) { + "Bounded analysis phases require one runnable entry point" + } + + val phaseStartSteps = stepsStatistics.totalSteps + val phaseStopStrategy = StopStrategy { + val analysisStopped = stopStrategy.shouldStop() + val phaseStopped = maxSteps != null && stepsStatistics.totalSteps - phaseStartSteps >= maxSteps + analysisStopped || phaseStopped + } + + run( + interpreter = interpreter, + pathSelector = pathSelector, + observer = executionObserver, + isStateTerminated = { state -> state.callStack.isEmpty() }, + stopStrategy = phaseStopStrategy, + ) + + val exhausted = pathSelector.isEmpty() + finished = finished || exhausted + val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED + val result = TsMachineAnalysisResult( + states = statesCollector.collectedStates.toList(), + stopReason = stopReason, + timedOut = timedOut, + unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, + engineFailed = interpreter.stepFailed, + unsupportedPaths = unsupportedPaths.toList(), + infeasibleEntryPoints = infeasibleEntryPoints, + ) + lastResult = result + result + } + }, + analysisFinished = { finished }, + release = { activeAnalysis = null }, + ) + } + + private fun createCoverageStatistics( + entryMethods: Set, + ): CoverageStatistics { + val methodsToTrackCoverage = when (options.coverageZone) { + CoverageZone.METHOD, CoverageZone.TRANSITIVE -> entryMethods.toHashSet() + CoverageZone.CLASS -> classCoverageMethods(entryMethods = entryMethods) + } + + return CoverageStatistics(methods = methodsToTrackCoverage, applicationGraph = graph) + } + + private fun createAnalysisPathSelector( + initialStates: Map, + timeStatistics: TimeStatistics, + coverageStatistics: CoverageStatistics, + ): UPathSelector { + val callGraphStatistics: PlainCallGraphStatistics = when (options.targetSearchDepth) { + 0u -> PlainCallGraphStatistics() + else -> TODO("Unsupported yet") + } + + return createPathSelector( + initialStates = initialStates, + options = options, + applicationGraph = graph, + timeStatistics = timeStatistics, + coverageStatisticsFactory = { coverageStatistics }, + cfgStatisticsFactory = { cfgStatistics }, + callGraphStatisticsFactory = { callGraphStatistics }, + ) + } + + private fun createAnalysisObserver( + initialStates: Map, + coverageStatistics: CoverageStatistics, + statesCollector: StatesCollector, + timeStatistics: TimeStatistics, + stepsStatistics: StepsStatistics, + ): UMachineObserver { + val observers = mutableListOf>(coverageStatistics, statesCollector) + if (tsOptions.enableVisualization) { + observers += TsStateVisualizer() + } + + if (options.useSoftConstraints) { + observers.add(SoftConstraintsObserver()) + } + observers.add(timeStatistics) observers.add(stepsStatistics) machineObserver?.let { observers.add(it) } @@ -280,43 +400,12 @@ class TsMachine( getMethodSignature = { it.humanReadableSignature }, coverageStatistics = coverageStatistics, timeStatistics = timeStatistics, - stepsStatistics = stepsStatistics + stepsStatistics = stepsStatistics, ) ) } - val supportedObserver = CompositeUMachineObserver(observers) - val outcomeObserver = UnsupportedPathsObserver( - delegate = supportedObserver, - unsupportedPaths = unsupportedPaths, - ) - val factoryObserver = machineObserverFactory?.invoke(pathSelector) - val executionObserver = if (factoryObserver == null) { - outcomeObserver - } else { - CompositeUMachineObserver(outcomeObserver, factoryObserver) - } - - run( - interpreter = interpreter, - pathSelector = pathSelector, - observer = executionObserver, - isStateTerminated = { state -> state.callStack.isEmpty() }, - stopStrategy = stopStrategy, - ) - - val exhausted = pathSelector.isEmpty() - val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED - - return TsMachineAnalysisResult( - states = statesCollector.collectedStates, - stopReason = stopReason, - timedOut = timedOut, - unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, - engineFailed = interpreter.stepFailed, - unsupportedPaths = unsupportedPaths.toList(), - infeasibleEntryPoints = infeasibleEntryPoints, - ) + return CompositeUMachineObserver(observers) } private fun createStatesCollector( @@ -412,6 +501,11 @@ class TsMachine( } override fun close() { + if (closed) return + check(!preparingAnalysis) { "Cannot close the machine while preparing an analysis" } + + activeAnalysis?.close() + closed = true components.close() } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt new file mode 100644 index 0000000000..2a213e14cb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsAnalysisSessionTest.kt @@ -0,0 +1,359 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.PathSelectorFairnessStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** Queue, budget and ownership contracts; generated witnesses are also checked in the native runtime. */ +class TsAnalysisSessionTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/samples/lang/Exceptions.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val method by lazy { getMethod(methodName = "conditionalCatch", className = "Exceptions") } + private val analysisOptions = UMachineOptions( + solverType = SolverType.YICES, + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `one step phases reuse the initial state and prefix queries and preserve native outcomes`() { + val direct = execute(phased = false) + + val phased = execute(phased = true) + + assertEquals(expected = 1, actual = phased.initializations) + assertEquals(expected = direct.steps, actual = phased.steps) + assertEquals(expected = direct.queries, actual = phased.queries) + assertTrue(phased.phases > 1) + assertEquals(expected = setOf(1.0, 2.0), actual = phased.tests.map(::resultNumber).toSet()) + assertEquals( + expected = direct.tests.map(::resultNumber).toSet(), + actual = phased.tests.map(::resultNumber).toSet(), + ) + + val script = buildString { + appendLine(source.readText()) + phased.tests.forEach { test -> + val input = assertIs(test.before.parameters.single()).number + val expected = if (input == 0.0) 2.0 else 1.0 + assertEquals(expected = expected, actual = resultNumber(test)) + + appendLine("if (new Exceptions().conditionalCatch($input) !== $expected) {") + appendLine(" throw Error('session witness');") + appendLine("}") + } + } + assertNodeReplay( + source = script, + directory = directory, + name = "analysis-session", + timeoutMessage = "Native replay of retained-session witnesses timed out", + ) + } + + @Test + fun `analysis step limit is cumulative and cannot be reset by another advance`() { + var steps = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val options = analysisOptions.copy(stepLimit = 2uL) + + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + val first = session.advance(maxSteps = 1uL) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = first.stopReason) + assertFalse(session.isFinished) + + val second = session.advance(maxSteps = 1uL) + assertEquals(expected = TsAnalysisStopReason.STOPPED, actual = second.stopReason) + assertTrue(session.isFinished) + assertFalse(second.timedOut) + assertEquals(expected = 2, actual = steps) + + assertEquals(expected = second, actual = session.advance()) + assertEquals(expected = 2, actual = steps) + } + } + } + + @Test + fun `phase snapshots do not acquire states collected by later advances`() { + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + var snapshot = session.advance(maxSteps = 1uL) + var phases = 1 + while (snapshot.states.isEmpty() && !session.isFinished) { + assertTrue(phases++ < MAX_PHASES) + snapshot = session.advance(maxSteps = 1uL) + } + assertEquals(expected = 1, actual = snapshot.states.size) + val firstState = snapshot.states.single() + + val final = session.advance() + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = final.stopReason) + assertEquals(expected = 2, actual = final.states.size) + assertEquals(expected = listOf(firstState), actual = snapshot.states) + } + } + } + + @Test + fun `closing a session releases the machine and closing the machine invalidates the session`() { + val machine = TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()) + machine.use { + val session = machine.openAnalysis(methods = listOf(method)) + session.advance(maxSteps = 1uL) + assertFailsWith { machine.openAnalysis(methods = listOf(method)) } + assertFailsWith { machine.analyzeWithMetadata(methods = listOf(method)) } + + session.close() + session.close() + + assertTrue(session.isFinished) + assertFailsWith { session.advance() } + assertEquals( + expected = TsAnalysisStopReason.EXHAUSTED, + actual = machine.analyzeWithMetadata(methods = listOf(method)).stopReason, + ) + + val next = machine.openAnalysis(methods = listOf(method)) + machine.close() + + assertTrue(next.isFinished) + assertFailsWith { next.advance() } + assertFailsWith { machine.openAnalysis(methods = listOf(method)) } + } + } + + @Test + fun `timeout stops the analysis rather than yielding a resumable phase`() { + var steps = 0 + val observer = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val options = analysisOptions.copy(timeout = Duration.ZERO) + + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = listOf(method)).use { session -> + val result = session.advance(maxSteps = 1uL) + + assertTrue(result.timedOut) + assertTrue(session.isFinished) + assertEquals(expected = 0, actual = steps) + assertEquals(expected = result, actual = session.advance()) + } + } + } + + @Test + fun `empty analysis is finished without invoking machine lifecycle observers`() { + var starts = 0 + val observer = object : UMachineObserver { + override fun onMachineStarted() { + starts++ + } + } + + TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + machine.openAnalysis(methods = emptyList()).use { session -> + assertTrue(session.isFinished) + + val result = session.advance() + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertTrue(result.states.isEmpty()) + assertEquals(expected = 0, actual = starts) + } + } + } + + @Test + fun `bounded phases reject multiple runnable entries without changing uninterrupted scheduling`() { + val other = getMethod(methodName = "caughtValue", className = "Exceptions") + val methods = listOf(method, other) + + for (fairness in PathSelectorFairnessStrategy.entries) { + val options = analysisOptions.copy(pathSelectorFairnessStrategy = fairness, timeout = 10.seconds) + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + val session = machine.openAnalysis(methods = methods) + + val failure = assertFailsWith { session.advance(maxSteps = 1uL) } + + assertTrue(failure.message.orEmpty().contains("one runnable entry point")) + assertTrue(session.isFinished) + + val result = machine.analyzeWithMetadata(methods = methods) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = methods.toSet(), actual = result.states.map { it.entrypoint }.toSet()) + } + } + } + + @Test + fun `initial state callbacks cannot open a nested analysis and failed preparation releases the owner`() { + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + val failure = assertFailsWith { + machine.openAnalysis(methods = listOf(method), configureInitialState = { _, _ -> + machine.openAnalysis(methods = emptyList()) + }) + } + + assertTrue(failure.message.orEmpty().contains("current analysis session")) + val result = machine.analyzeWithMetadata(methods = listOf(method)) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + } + } + + @Test + fun `an exceptional advance invalidates its session and releases the machine`() { + var failNextStep = true + val observer = object : UMachineObserver { + override fun onStatePeeked(state: TsState) { + if (failNextStep) { + failNextStep = false + error("phase observer failed") + } + } + } + + TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ).use { machine -> + val session = machine.openAnalysis(methods = listOf(method)) + + val failure = assertFailsWith { session.advance(maxSteps = 1uL) } + + assertEquals(expected = "phase observer failed", actual = failure.message) + assertTrue(session.isFinished) + assertFailsWith { session.advance() } + assertEquals( + expected = TsAnalysisStopReason.EXHAUSTED, + actual = machine.analyzeWithMetadata(methods = listOf(method)).stopReason, + ) + } + } + + private fun execute(phased: Boolean): Execution { + var initializations = 0 + var steps = 0 + var queries = 0 + var phases = 0 + val machineObserver = object : UMachineObserver { + override fun onState(parent: TsState, forks: Sequence) { + steps++ + } + } + val interpreterObserver = object : TsInterpreterObserver { + override fun onSolverQuery(event: TsSolverQueryEvent) { + queries++ + } + } + + val outcome = TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = machineObserver, + observer = interpreterObserver, + ).use { machine -> + machine.openAnalysis(methods = listOf(method), configureInitialState = { _, _ -> initializations++ }) + .use { session -> + var result: TsMachineAnalysisResult + do { + assertTrue(phases++ < MAX_PHASES) + result = session.advance(maxSteps = if (phased) 1uL else null) + } while (!session.isFinished) + + val stepsAtFinish = steps + val queriesAtFinish = queries + session.advance() + assertEquals(expected = stepsAtFinish, actual = steps) + assertEquals(expected = queriesAtFinish, actual = queries) + result + } + } + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = outcome.stopReason) + assertFalse(outcome.engineFailed) + assertFalse(outcome.unsupportedCall) + assertTrue(outcome.unsupportedPaths.isEmpty()) + + return Execution( + initializations = initializations, + steps = steps, + queries = queries, + phases = phases, + tests = outcome.states.map { state -> TsTestResolver().resolve(method, state) }, + ) + } + + private fun resultNumber(test: TsTest): Double = assertIs(test.returnValue).number + + private data class Execution( + val initializations: Int, + val steps: Int, + val queries: Int, + val phases: Int, + val tests: List, + ) + + companion object { + private const val MAX_PHASES = 200 + } +}