Skip to content

[TS] Preserve analysis work across bounded phases #546

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
CaelmBleidd wants to merge 1 commit into from
Closed

[TS] Preserve analysis work across bounded phases #546

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/TsAnalysisSession.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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()
}
}
240 changes: 167 additions & 73 deletions usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -185,60 +188,66 @@ class TsMachine(
methods: List<EtsMethod>,
targets: List<TsTarget> = 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<EtsMethod>,
targets: List<TsTarget> = 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<EtsMethod>,
targets: List<TsTarget>,
configureInitialState: (EtsMethod, TsState) -> Unit,
): TsAnalysisSession {
interpreter.resetStepFailure()
failureTrackingUnknownCallObserver.reset()

val (initialStates, unsupportedPaths, infeasibleEntryPoints) =
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<EtsMethod, EtsStmt, TsState>(
methods = methodsToTrackCoverage,
applicationGraph = graph,
)

val callGraphStatistics: PlainCallGraphStatistics<EtsMethod> =
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<UMachineObserver<TsState>>(coverageStatistics)
observers.add(statesCollector)
if (tsOptions.enableVisualization) {
observers += TsStateVisualizer()
}

if (options.useSoftConstraints) {
observers.add(SoftConstraintsObserver())
}

val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
var timedOut = false
var finished = false
val stopStrategy = object : StopStrategy {
val strategy = createStopStrategy(
options,
Expand All @@ -252,22 +261,133 @@ 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()}" }
}

return result
}
}

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<EtsMethod>,
): CoverageStatistics<EtsMethod, EtsStmt, TsState> {
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<EtsMethod, TsState>,
timeStatistics: TimeStatistics<EtsMethod, TsState>,
coverageStatistics: CoverageStatistics<EtsMethod, EtsStmt, TsState>,
): UPathSelector<TsState> {
val callGraphStatistics: PlainCallGraphStatistics<EtsMethod> = 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<EtsMethod, TsState>,
coverageStatistics: CoverageStatistics<EtsMethod, EtsStmt, TsState>,
statesCollector: StatesCollector<TsState>,
timeStatistics: TimeStatistics<EtsMethod, TsState>,
stepsStatistics: StepsStatistics<EtsMethod, TsState>,
): UMachineObserver<TsState> {
val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics, statesCollector)
if (tsOptions.enableVisualization) {
observers += TsStateVisualizer()
}

if (options.useSoftConstraints) {
observers.add(SoftConstraintsObserver())
}

observers.add(timeStatistics)
observers.add(stepsStatistics)
machineObserver?.let { observers.add(it) }
Expand All @@ -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(
Expand Down Expand Up @@ -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()
}
}
Expand Down
Loading
Loading