Observe actual solver queries and fair-selector time quanta

usvm-core/src/main/kotlin/org/usvm/ps/ConstantTimeFairPathSelector.kt

@@ -32,6 +32,7 @@ class ConstantTimeFairPathSelector<State, Key, KeyPriority : Comparable<KeyPrior
     private val getKeyPriority: (Key) -> KeyPriority,
     basePathSelectorFactory: (Key) -> UPathSelector<State>,
     private val maxTimeQuantum: Duration = Duration.INFINITE,
+    private val onTimeQuantum: (Key, Duration, Duration) -> Unit = { _, _, _ -> },
 ) : KeyedPathSelector<State, Key>(getKey) {
 
     private data class KeysQueueElement<Key, KeyPriority>(val key: Key, var priority: KeyPriority, var elapsed: Duration)
@@ -72,6 +73,15 @@ class ConstantTimeFairPathSelector<State, Key, KeyPriority : Comparable<KeyPrior
         return activeQueue.peek()
     }
 
+    /** Flush the final partial turn when the machine stops without another peek. */
+    fun finishTimeQuantum() {
+        if (!stopwatch.isRunning) return
+
+        stopwatch.stop()
+        val currentKey = activeQueue.peek() ?: return
+        onTimeQuantum(currentKey.key, currentTimeQuantum, stopwatch.elapsed)
+    }
+
     override fun isEmpty(): Boolean {
         if (activeQueue.isEmpty() && expiredList.isEmpty()) {
             return true
@@ -86,7 +96,7 @@ class ConstantTimeFairPathSelector<State, Key, KeyPriority : Comparable<KeyPrior
         val quantumEnded = stopwatch.isRunning && stopwatch.elapsed >= currentTimeQuantum
         // When time quantum is exceeded or there is nothing to peek, start peeking the next one
         if (quantumEnded || isCurrentPathSelectorEmpty) {
-            stopwatch.stop()
+            finishTimeQuantum()
             activeQueue.remove(currentKey)
             if (!isCurrentPathSelectorEmpty) {
                 currentKey.elapsed += stopwatch.elapsed

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -228,7 +228,10 @@ fun <Method, Statement, Target, State> createPathSelector(
                 getKeyPriority = getMethodCoverage,
                 basePathSelectorFactory = ::createBasePathSelector,
                 maxTimeQuantum = options.maxEntryPointTimeQuantum,
-            )
+                onTimeQuantum = timeStatistics.onEntryPointTimeQuantum,
+            ).also { selector ->
+                timeStatistics.finishTimeQuantum = selector::finishTimeQuantum
+            }
         }
 
         PathSelectorFairnessStrategy.COMPLETELY_FAIR ->

usvm-core/src/main/kotlin/org/usvm/solver/USolverQueryEvent.kt

@@ -0,0 +1,66 @@
+package org.usvm.solver
+
+import io.ksmt.expr.KExpr
+import io.ksmt.solver.KSolver
+import io.ksmt.solver.KSolverConfiguration
+import io.ksmt.solver.KSolverStatus
+import io.ksmt.sort.KBoolSort
+import mu.KLogging
+import kotlin.time.Duration
+import kotlin.time.TimeSource
+
+private val logger = object : KLogging() {}.logger
+
+/**
+ * One completed KSolver check or checkWithAssumptions call, including a failed call.
+ *
+ * Measures wall time inside the check, excluding assertions, model decoding and type solving.
+ * This is not the total cost of a USolver query, which may perform several SMT checks.
+ */
+data class USolverQueryEvent(
+    val elapsedNanos: Long,
+    val status: KSolverStatus?,
+    val failure: String?,
+)
+
+/** Observer failures are logged without changing the solver result or exception. */
+fun <Config : KSolverConfiguration> observeSolverQueries(
+    solver: KSolver<Config>,
+    observer: (USolverQueryEvent) -> Unit,
+): KSolver<Config> = ObservedSolver(solver = solver, observer = observer)
+
+internal class ObservedSolver<Config : KSolverConfiguration>(
+    private val solver: KSolver<Config>,
+    private val observer: (USolverQueryEvent) -> Unit,
+    private val timeSource: TimeSource = TimeSource.Monotonic,
+) : KSolver<Config> by solver {
+    override fun check(timeout: Duration): KSolverStatus = measured { solver.check(timeout = timeout) }
+
+    override fun checkWithAssumptions(
+        assumptions: List<KExpr<KBoolSort>>,
+        timeout: Duration,
+    ): KSolverStatus = measured { solver.checkWithAssumptions(assumptions = assumptions, timeout = timeout) }
+
+    @Suppress("TooGenericExceptionCaught") // Report every backend failure and rethrow the same exception.
+    private inline fun measured(block: () -> KSolverStatus): KSolverStatus {
+        val started = timeSource.markNow()
+        var status: KSolverStatus? = null
+        var failure: String? = null
+        try {
+            val result = block()
+            status = result
+            return result
+        } catch (error: Throwable) {
+            failure = error::class.java.name
+            throw error
+        } finally {
+            val event = USolverQueryEvent(
+                elapsedNanos = started.elapsedNow().inWholeNanoseconds,
+                status = status,
+                failure = failure,
+            )
+            runCatching { observer(event) }
+                .onFailure { error -> logger.warn(error) { "Solver query observer failed while recording an event" } }
+        }
+    }
+}

usvm-core/src/main/kotlin/org/usvm/statistics/TimeStatistics.kt

@@ -7,7 +7,11 @@ import kotlin.time.Duration
 /**
  * Maintains information about time spent on machine processes.
  */
-class TimeStatistics<Method, State : UState<*, Method, *, *, *, State>> : UMachineObserver<State> {
+class TimeStatistics<Method, State : UState<*, Method, *, *, *, State>>(
+    val onEntryPointTimeQuantum: (Method, Duration, Duration) -> Unit = { _, _, _ -> },
+) : UMachineObserver<State> {
+    internal var finishTimeQuantum: () -> Unit = { }
+
     private val stopwatch = RealTimeStopwatch()
     private val methodStopwatch = RealTimeStopwatch()
 
@@ -30,6 +34,7 @@ class TimeStatistics<Method, State : UState<*, Method, *, *, *, State>> : UMachi
 
     override fun onMachineStopped() {
         check(stopwatch.isRunning) { "Machine stopwatch was not running on machine stopped" }
+        finishTimeQuantum()
         stopwatch.stop()
         methodStopwatch.stop()
     }

usvm-core/src/test/kotlin/org/usvm/ps/ConstantTimeFairPathSelectorQuantumTest.kt

@@ -99,6 +99,55 @@ class ConstantTimeFairPathSelectorQuantumTest {
         assertEquals(expected = "b1", actual = nextState)
     }
 
+    @Test
+    fun `measured turns preserve overrun and final partial turn exactly once`() {
+        val stopwatch = TestStopwatch()
+        val turns = mutableListOf<Triple<Char, Duration, Duration>>()
+        val selector = selector(
+            stopwatch = stopwatch,
+            remainingTime = { 30.seconds },
+            maxTimeQuantum = 2.seconds,
+            onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) },
+        )
+        selector.add(states = listOf("a1", "b1", "c1"))
+        assertEquals(expected = "a1", actual = selector.peek())
+
+        stopwatch.elapsedRaw = 4L
+        assertEquals(expected = "b1", actual = selector.peek())
+        stopwatch.elapsedRaw = 1L
+        selector.finishTimeQuantum()
+        selector.finishTimeQuantum()
+
+        assertEquals(
+            expected = listOf(Triple('a', 2.seconds, 4.seconds), Triple('b', 2.seconds, 1.seconds)),
+            actual = turns,
+        )
+    }
+
+    @Test
+    fun `successive turns of the only remaining key remain distinct`() {
+        val stopwatch = TestStopwatch()
+        val turns = mutableListOf<Triple<Char, Duration, Duration>>()
+        val selector = selector(
+            stopwatch = stopwatch,
+            remainingTime = { 30.seconds },
+            maxTimeQuantum = 2.seconds,
+            onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) },
+        )
+        selector.add(states = listOf("a1"))
+        assertEquals(expected = "a1", actual = selector.peek())
+
+        stopwatch.elapsedRaw = 2L
+        assertEquals(expected = "a1", actual = selector.peek())
+        stopwatch.elapsedRaw = 1L
+        selector.finishTimeQuantum()
+
+        assertEquals(
+            expected = listOf(Triple('a', 2.seconds, 2.seconds), Triple('a', 2.seconds, 1.seconds)),
+            actual = turns,
+        )
+    }
+
     @Test
     fun `nonpositive turn bounds are rejected`() {
         for (quantum in listOf(Duration.ZERO, -1.seconds)) {
@@ -118,6 +167,7 @@ class ConstantTimeFairPathSelectorQuantumTest {
         stopwatch: TestStopwatch,
         remainingTime: () -> Duration,
         maxTimeQuantum: Duration,
+        onTimeQuantum: (Char, Duration, Duration) -> Unit = { _, _, _ -> },
     ): ConstantTimeFairPathSelector<String, Char, Char> = ConstantTimeFairPathSelector(
         initialKeys = setOf('a', 'b', 'c'),
         stopwatch = stopwatch,
@@ -126,5 +176,6 @@ class ConstantTimeFairPathSelectorQuantumTest {
         getKeyPriority = { key -> key },
         basePathSelectorFactory = { BfsPathSelector() },
         maxTimeQuantum = maxTimeQuantum,
+        onTimeQuantum = onTimeQuantum,
     )
 }

usvm-core/src/test/kotlin/org/usvm/ps/PathSelectorDrainTest.kt

@@ -15,6 +15,7 @@ import kotlin.test.assertEquals
 import kotlin.test.assertFalse
 import kotlin.test.assertSame
 import kotlin.test.assertTrue
+import kotlin.time.Duration
 import kotlin.time.Duration.Companion.seconds
 
 class PathSelectorDrainTest {
@@ -34,6 +35,7 @@ class PathSelectorDrainTest {
     fun `constant time drain includes unvisited keys without new scheduling events`() {
         val stopwatch = TestStopwatch()
         val children = mutableMapOf<Char, TrackingSelector<String>>()
+        val turns = mutableListOf<Triple<Char, Duration, Duration>>()
         var stopped = false
         val selector = ConstantTimeFairPathSelector(
             initialKeys = setOf('a', 'b', 'c'),
@@ -49,18 +51,20 @@ class PathSelectorDrainTest {
             },
             basePathSelectorFactory = { key -> TrackingSelector<String>().also { children[key] = it } },
             maxTimeQuantum = 2.seconds,
+            onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) },
         )
         selector.add(states = listOf("a1", "a2", "b1", "c1"))
         assertEquals(expected = "a1", actual = selector.peek())
         stopwatch.elapsedRaw = 3L
-        stopwatch.stop()
+        selector.finishTimeQuantum()
         stopped = true
 
         val drained = selector.drain().toList()
 
         assertEquals(expected = setOf("a1", "a2", "b1", "c1"), actual = drained.toSet())
         assertEquals(expected = 4, actual = drained.size)
         assertEquals(expected = 1, actual = children.values.sumOf { it.peekCount })
+        assertEquals(expected = listOf(Triple('a', 2.seconds, 3.seconds)), actual = turns)
         assertEquals(expected = 3.seconds, actual = stopwatch.elapsed)
         assertFalse(stopwatch.isRunning)
         assertTrue(selector.isEmpty())