From 53a0a09db0fc69421993e4cea9e884f8d9b25656 Mon Sep 17 00:00:00 2001
From: tochilinak <tochilina.2002@yandex.ru>
Date: Thu, 19 Jun 2025 12:54:02 +0300
Subject: [PATCH 1/4] add time profiling

---
 .../usvm/statistics/UDebugProfileObserver.kt  | 112 ++++++++++++++----
 .../machine/utils/PyDebugProfileObserver.kt   |   2 +
 2 files changed, 90 insertions(+), 24 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
index 91467ef299..992450af12 100644
--- a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
@@ -79,18 +79,42 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
          * Add padding to instructions in profiler report.
          * */
         val padInstructionEnd: Int = 0,
-    )
+        /**
+         * Profile time spent on each instruction.
+         * */
+        val profileTime: Boolean = true,
+        /**
+         * Profile number of forks on each instruction.
+         * */
+        val profileForks: Boolean = true,
+    ) {
+        init {
+            require(!profileTime || momentOfUpdate == MomentOfUpdate.BeforeStep) {
+                "Time profiling in now supported only if momentOfUpdate in BeforeStep"
+            }
+        }
+    }
 
     protected val instructionStats = hashMapOf<Statement, MutableMap<StateId, StatsCounter>>()
     protected val methodCalls = hashMapOf<Method, MutableMap<StateId, StatsCounter>>()
 
-    private val stackTraceTracker = StackTraceTracker<Statement, Method, State>(statementOperations)
+    private val stackTraceTracker = StackTraceTracker(statementOperations)
     private val stackTraces = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
     private val forksCount = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
+    private val instructionTime = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
+
+    private var lastPeekMoment = 0L
+    private var lastStackTrace: TrieNode<Statement, *>? = null
 
     override fun onStatePeeked(state: State) {
-        if (profilerOptions.momentOfUpdate == MomentOfUpdate.BeforeStep) {
-            processStateUpdate(state)
+        if (profilerOptions.momentOfUpdate != MomentOfUpdate.BeforeStep) {
+            return
+        }
+
+        processStateUpdate(state)
+
+        if (profilerOptions.profileTime) {
+            lastPeekMoment = System.currentTimeMillis()
         }
     }
 
@@ -100,6 +124,20 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
                 processStateUpdate(it)
             }
         }
+
+        if (profilerOptions.momentOfUpdate == MomentOfUpdate.BeforeStep && profilerOptions.profileTime) {
+            val stackTrace = lastStackTrace
+                ?: error("stackTraceAfterPeek should have been memorized")
+            incrementInstructionTime(parent, stackTrace, System.currentTimeMillis() - lastPeekMoment)
+        }
+    }
+
+    private fun incrementInstructionTime(state: State, stackTrace: TrieNode<Statement, *>, time: Long) {
+        var st = stackTrace
+        while (true) {
+            instructionTime.increment(st, state, value = time)
+            st = st.parent() ?: break
+        }
     }
 
     private fun processStateUpdate(state: State) {
@@ -124,6 +162,7 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         val fork = statementOperations.forkHappened(state, node)
 
         var st = stackTraceTracker.getStackTrace(state, node.statement)
+        lastStackTrace = st
         while (true) {
             stackTraces.increment(st, state)
             if (fork) forksCount.increment(st, state)
@@ -131,10 +170,10 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         }
     }
 
-    private fun <K> MutableMap<K, MutableMap<StateId, StatsCounter>>.increment(key: K, state: State) {
+    private fun <K> MutableMap<K, MutableMap<StateId, StatsCounter>>.increment(key: K, state: State, value: Long = 1L) {
         val stateStats = this.getOrPut(key) { hashMapOf() }
         val stats = stateStats.getOrPut(state.id) { StatsCounter() }
-        stats.increment()
+        stats.add(value)
     }
 
     private fun aggregateStackTraces(slice: StateId?): ProfileFrame<Statement, Method, State> {
@@ -143,10 +182,12 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         }
         return ProfileFrame(
             inst = null,
-            total = -1,
-            self = -1,
+            totalSteps = -1,
+            selfSteps = -1,
             totalForks = -1,
             selfForks = -1,
+            totalTime = -1,
+            selfTime = -1,
             children = children,
             profilerOptions,
             statementOperations,
@@ -160,19 +201,24 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
     ): ProfileFrame<Statement, Method, State> {
         val allNodeStats = stackTraces[root].orEmpty()
         val allForkStats = forksCount[root].orEmpty()
+        val allTimeStats = instructionTime[root].orEmpty()
         val children = root.children.mapValues { (i, node) -> computeProfileFrame(slice, i, node) }
 
         val nodeStats = allNodeStats.sumOfSlice(slice)
         val forkStats = allForkStats.sumOfSlice(slice)
+        val timeStats = allTimeStats.sumOfSlice(slice)
 
-        val selfStat = nodeStats - children.values.sumOf { it.total }
+        val selfStat = nodeStats - children.values.sumOf { it.totalSteps }
         val selfForks = forkStats - children.values.sumOf { it.totalForks }
+        val selfTime = timeStats - children.values.sumOf { it.totalTime }
         return ProfileFrame(
             inst,
-            nodeStats,
-            selfStat,
-            forkStats,
-            selfForks,
+            totalSteps = nodeStats,
+            selfSteps = selfStat,
+            totalForks = forkStats,
+            selfForks = selfForks,
+            totalTime = timeStats,
+            selfTime = selfTime,
             children,
             profilerOptions,
             statementOperations,
@@ -181,10 +227,12 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
 
     private class ProfileFrame<Statement, Method, State : UState<*, Method, Statement, *, *, *>>(
         val inst: Statement?,
-        val total: Long,
-        val self: Long,
+        val totalSteps: Long,
+        val selfSteps: Long,
         val totalForks: Long,
         val selfForks: Long,
+        val totalTime: Long,
+        val selfTime: Long,
         val children: Map<Statement, ProfileFrame<Statement, Method, State>>,
         private val profilerOptions: Options,
         private val statementOperations: StatementOperations<Statement, Method, State>,
@@ -192,15 +240,23 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         fun print(str: StringBuilder, indent: String) {
             val sortedChildren = children.entries
                 .groupBy { statementOperations.getMethodOfStatement(it.key) }.entries
-                .sortedByDescending { entry -> entry.value.sumOf { it.value.total } }
+                .sortedByDescending { entry -> entry.value.sumOf { it.value.totalSteps } }
 
             for ((method, inst) in sortedChildren) {
-                val total = inst.sumOf { it.value.total }
-                val self = inst.sumOf { it.value.self }
+                val total = inst.sumOf { it.value.totalSteps }
+                val self = inst.sumOf { it.value.selfSteps }
                 val totalForks = inst.sumOf { it.value.totalForks }
                 val selfForks = inst.sumOf { it.value.selfForks }
                 val methodRepr = statementOperations.printMethodName(method)
-                str.appendLine("$indent|__ $methodRepr | Steps $self/$total | Forks $selfForks/$totalForks")
+
+                str.append("$indent|__ $methodRepr | Steps $self/$total")
+                if (profilerOptions.profileForks) {
+                    str.append(" | Forks $selfForks/$totalForks")
+                }
+                if (profilerOptions.profileTime) {
+                    str.append(" | Time $selfTime/$totalTime")
+                }
+                str.appendLine()
 
                 val children = if (profilerOptions.printNonVisitedStatements) {
                     val allStatements = statementOperations.getAllMethodStatements(method)
@@ -212,10 +268,12 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
                         } ?: let {
                             val emptyFrame = ProfileFrame(
                                 childStmt,
-                                total = 0L,
-                                self = 0L,
+                                totalSteps = 0L,
+                                selfSteps = 0L,
                                 totalForks = 0L,
                                 selfForks = 0L,
+                                totalTime = 0L,
+                                selfTime = 0L,
                                 emptyMap(),
                                 profilerOptions,
                                 statementOperations,
@@ -231,10 +289,16 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
 
                 for ((i, child) in children) {
                     val instRepr = statementOperations.printStatement(i).padEnd(profilerOptions.padInstructionEnd)
-                    val line = "$indent$INDENT$instRepr" +
-                        " | Steps ${child.self}/${child.total}" +
-                        " | Forks ${child.selfForks}/${child.totalForks}"
+
+                    var line = "$indent$INDENT$instRepr | Steps ${child.selfSteps}/${child.totalSteps}"
+                    if (profilerOptions.profileForks) {
+                        line += " | Forks ${child.selfForks}/${child.totalForks}"
+                    }
+                    if (profilerOptions.profileTime) {
+                        line += " | Time ${child.selfTime}/${child.totalTime}"
+                    }
                     str.appendLine(line)
+
                     child.print(str, "$indent$INDENT$INDENT")
                 }
             }
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/utils/PyDebugProfileObserver.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/utils/PyDebugProfileObserver.kt
index 977f4d1555..3f4db9baf4 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/utils/PyDebugProfileObserver.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/utils/PyDebugProfileObserver.kt
@@ -57,5 +57,7 @@ val pyDebugProfileObserver = UDebugProfileObserver(
     profilerOptions = UDebugProfileObserver.Options(
         momentOfUpdate = UDebugProfileObserver.MomentOfUpdate.AfterStep,
         printNonVisitedStatements = true,
+        profileTime = false,
+        profileForks = false,
     ),
 )

From 1bd6e37ec1a32e7dbf7633450963b04ed7fdae4b Mon Sep 17 00:00:00 2001
From: tochilinak <tochilina.2002@yandex.ru>
Date: Thu, 19 Jun 2025 14:57:14 +0300
Subject: [PATCH 2/4] Timing in nanoseconds

---
 .../usvm/statistics/UDebugProfileObserver.kt  | 23 +++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
index 992450af12..0b3418ebae 100644
--- a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
@@ -87,6 +87,7 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
          * Profile number of forks on each instruction.
          * */
         val profileForks: Boolean = true,
+        val timeFormat: TimeFormat = TimeFormat.Microseconds,
     ) {
         init {
             require(!profileTime || momentOfUpdate == MomentOfUpdate.BeforeStep) {
@@ -114,7 +115,7 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         processStateUpdate(state)
 
         if (profilerOptions.profileTime) {
-            lastPeekMoment = System.currentTimeMillis()
+            lastPeekMoment = System.nanoTime()
         }
     }
 
@@ -128,7 +129,7 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         if (profilerOptions.momentOfUpdate == MomentOfUpdate.BeforeStep && profilerOptions.profileTime) {
             val stackTrace = lastStackTrace
                 ?: error("stackTraceAfterPeek should have been memorized")
-            incrementInstructionTime(parent, stackTrace, System.currentTimeMillis() - lastPeekMoment)
+            incrementInstructionTime(parent, stackTrace, System.nanoTime() - lastPeekMoment)
         }
     }
 
@@ -194,6 +195,14 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         )
     }
 
+    private fun formatTime(time: Long): Long {
+        return when (profilerOptions.timeFormat) {
+            TimeFormat.Nanoseconds -> time
+            TimeFormat.Microseconds -> time / 1000L
+            TimeFormat.Milliseconds -> time / 1000000L
+        }
+    }
+
     private fun computeProfileFrame(
         slice: StateId?,
         inst: Statement,
@@ -217,8 +226,8 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
             selfSteps = selfStat,
             totalForks = forkStats,
             selfForks = selfForks,
-            totalTime = timeStats,
-            selfTime = selfTime,
+            totalTime = formatTime(timeStats),
+            selfTime = formatTime(selfTime),
             children,
             profilerOptions,
             statementOperations,
@@ -352,4 +361,10 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         BeforeStep,
         AfterStep,
     }
+
+    enum class TimeFormat {
+        Milliseconds,
+        Microseconds,
+        Nanoseconds,
+    }
 }

From 24f1fb9c13ce2c3fd3fd4d44f49408100737bab3 Mon Sep 17 00:00:00 2001
From: tochilinak <tochilina.2002@yandex.ru>
Date: Thu, 19 Jun 2025 15:11:22 +0300
Subject: [PATCH 3/4] detekt fix

---
 .../kotlin/org/usvm/statistics/UDebugProfileObserver.kt  | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
index 0b3418ebae..9efca55224 100644
--- a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
@@ -198,8 +198,8 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
     private fun formatTime(time: Long): Long {
         return when (profilerOptions.timeFormat) {
             TimeFormat.Nanoseconds -> time
-            TimeFormat.Microseconds -> time / 1000L
-            TimeFormat.Milliseconds -> time / 1000000L
+            TimeFormat.Microseconds -> time / MICRO_IN_NANO
+            TimeFormat.Milliseconds -> time / MILLIES_IN_NANO
         }
     }
 
@@ -367,4 +367,9 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         Microseconds,
         Nanoseconds,
     }
+
+    companion object {
+        private const val MICRO_IN_NANO = 1000L
+        private const val MILLIES_IN_NANO = 1000_000L
+    }
 }

From 00faa32b725410e6b0bffb001e5efa5ea89fe4f4 Mon Sep 17 00:00:00 2001
From: tochilinak <tochilina.2002@yandex.ru>
Date: Thu, 19 Jun 2025 15:30:06 +0300
Subject: [PATCH 4/4] detekt fix

---
 .../main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
index 9efca55224..145e3907be 100644
--- a/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt
@@ -370,6 +370,6 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
 
     companion object {
         private const val MICRO_IN_NANO = 1000L
-        private const val MILLIES_IN_NANO = 1000_000L
+        private const val MILLIES_IN_NANO = 1_000_000L
     }
 }