From 264db304826a17881ad21df416d63ec0070f5b50 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:09:13 +0300 Subject: [PATCH 1/3] Separate raw class search and snapshot timing phases --- .../usvm/ts/calls/CallsClassRawAnalysis.kt | 56 +++++++++++++++++-- .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 5 +- .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 7 +++ 3 files changed, 63 insertions(+), 5 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt index bfb41b31b2..2dabf09748 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -13,6 +13,8 @@ import org.usvm.statistics.UMachineObserver import java.nio.file.Files import java.nio.file.Path import java.nio.file.StandardOpenOption +import kotlin.time.TimeMark +import kotlin.time.TimeSource @Serializable internal data class CallsClassRawIrPoint( @@ -58,6 +60,14 @@ internal data class CallsClassRawAnalysis( val budgetMillis: Long, val analysisElapsedMillis: Long, val budgetOverrunMillis: Long, + val timingSchemaVersion: Int = 0, + val analysisSetupElapsedMillis: Long = 0, + val searchElapsedMillis: Long = 0, + val remainingStateDrainMillis: Long = 0, + /** Snapshot work overlaps search or drain; it is not an additional phase. */ + val searchSnapshotElapsedNanos: Long = 0, + val drainSnapshotElapsedNanos: Long = 0, + val journalFinalizeMillis: Long = 0, val timeQuantumMillis: Long, val collectedStatesLimit: Int? = null, val profile: CallsExperimentProfile, @@ -120,6 +130,20 @@ internal class ClassRawAnalysisObserver( private var solverNanos = 0L private var quantumCount = 0L private var quantumOverruns = 0L + private var searchStarted: TimeMark? = null + private var searchElapsedMillis = 0L + private var draining = false + private var remainingStateDrainMillis = 0L + private var searchSnapshotNanos = 0L + private var drainSnapshotNanos = 0L + + override fun onMachineStarted() { + searchStarted = TimeSource.Monotonic.markNow() + } + + override fun onMachineStopped() { + searchElapsedMillis = searchStarted?.elapsedNow()?.inWholeMilliseconds ?: 0 + } fun recordOriginalEntry(stmt: EtsStmt) { val point = stmt.toClassRawIrPoint(sourceFile = sourceFile) @@ -180,9 +204,16 @@ internal class ClassRawAnalysisObserver( /** Drain only after analyzeWithMetadata has computed its real stop reason. */ fun retainRemainingStates(selector: UPathSelector?) { - selector?.drain()?.forEach { state -> - remainingStates++ - saveSnapshot(state = state, outcome = "SUSPENDED") + val started = TimeSource.Monotonic.markNow() + draining = true + try { + selector?.drain()?.forEach { state -> + remainingStates++ + saveSnapshot(state = state, outcome = "SUSPENDED") + } + } finally { + remainingStateDrainMillis = started.elapsedNow().inWholeMilliseconds + draining = false } } @@ -198,6 +229,7 @@ internal class ClassRawAnalysisObserver( } private fun saveSnapshot(state: TsState, outcome: String) { + val started = TimeSource.Monotonic.markNow() val saved = runCatching { snapshots.append { reference -> val stmt = state.lastStmt @@ -236,11 +268,20 @@ internal class ClassRawAnalysisObserver( ) } } + val elapsedNanos = started.elapsedNow().inWholeNanoseconds + if (draining) { + drainSnapshotNanos += elapsedNanos + } else { + searchSnapshotNanos += elapsedNanos + } } fun result(manifest: CallsClassStartManifest, analysisElapsedMillis: Long): CallsClassRawAnalysis { val encodedUniverse = encodeCallsArtifact(universe).toByteArray(Charsets.UTF_8) + val finalizeStarted = TimeSource.Monotonic.markNow() val journals = snapshots.finish() + val journalFinalizeMillis = finalizeStarted.elapsedNow().inWholeMilliseconds + // Exploratory execution may retain interpreter failures as terminal states. // Such a failure must still invalidate this diagnostic denominator. check(universeViolations.isEmpty()) { @@ -250,7 +291,14 @@ internal class ClassRawAnalysisObserver( return CallsClassRawAnalysis( budgetMillis = manifest.budgetMillis, analysisElapsedMillis = analysisElapsedMillis, - budgetOverrunMillis = (analysisElapsedMillis - manifest.budgetMillis).coerceAtLeast(0), + budgetOverrunMillis = (searchElapsedMillis - manifest.budgetMillis).coerceAtLeast(0), + timingSchemaVersion = 1, + analysisSetupElapsedMillis = (analysisElapsedMillis - searchElapsedMillis).coerceAtLeast(0), + searchElapsedMillis = searchElapsedMillis, + remainingStateDrainMillis = remainingStateDrainMillis, + searchSnapshotElapsedNanos = searchSnapshotNanos, + drainSnapshotElapsedNanos = drainSnapshotNanos, + journalFinalizeMillis = journalFinalizeMillis, timeQuantumMillis = manifest.timeQuantumMillis, profile = manifest.profile, seed = manifest.seed, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 6c4e75f8fa..7c03bb6e5c 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -609,7 +609,10 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { ) } finally { analysisElapsedMillis = analysisStarted.elapsedNow().inWholeMilliseconds - raw?.retainRemainingStates(selector = remainingSelector) + if (raw != null) { + checkpoint(next = "DRAIN_REMAINING") + raw.retainRemainingStates(selector = remainingSelector) + } } } case.verifyInputs() diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index acd94c5d99..762742f42a 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -164,6 +164,13 @@ class CallsClassStartSmokeTest { assertTrue(raw.sourceMappedIrUniverse.containsAll(raw.sourceMappedIrEntered)) assertTrue(raw.stateSnapshotFailures.isEmpty(), raw.stateSnapshotFailures.toString()) assertTrue(Files.isRegularFile(directory.resolve("output/states.jsonl.gz"))) + assertEquals(1, raw.timingSchemaVersion) + assertTrue(raw.searchElapsedMillis > 0) + assertEquals(raw.analysisElapsedMillis, raw.analysisSetupElapsedMillis + raw.searchElapsedMillis) + assertEquals((raw.searchElapsedMillis - raw.budgetMillis).coerceAtLeast(0), raw.budgetOverrunMillis) + assertTrue(raw.searchSnapshotElapsedNanos > 0) + assertEquals(0L, raw.drainSnapshotElapsedNanos) + assertEquals(0L, raw.remainingStates) } @Test From c0a51b564a7cc39afd6406ec1e4f7ac7a250a2cf Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 16:15:32 +0300 Subject: [PATCH 2/3] Update JacoDB to the latest merged neo revision --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index a36dd82748..23d6290d8c 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "c6d1fe316cdca9b08a674e1638ff6d485ae17824" + const val jacodb = "4251d2023db7b4bda53a232998968c1f9c2784fe" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" From dd10892d1337710bc95dcd9788765bbb45ab1f22 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 16:49:33 +0300 Subject: [PATCH 3/3] Use the published JitPack version of the current neo commit --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 23d6290d8c..fa3a6c9aca 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "4251d2023db7b4bda53a232998968c1f9c2784fe" + const val jacodb = "4251d2023d" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0"