Skip to content

Commit 54633bd

Browse files
tochilinaktochilinak
authored
Add time profiling in UDebugProfileObserver (#293)
* add time profiling * Timing in nanoseconds * detekt fix * detekt fix
1 parent fcb3f5f commit 54633bd

File tree

2 files changed

+110
-24
lines changed

2 files changed

+110
-24
lines changed

‎usvm-core/src/main/kotlin/org/usvm/statistics/UDebugProfileObserver.kt‎

Lines changed: 108 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -79,18 +79,43 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
7979
* Add padding to instructions in profiler report.
8080
* */
8181
val padInstructionEnd: Int = 0,
82-
)
82+
/**
83+
* Profile time spent on each instruction.
84+
* */
85+
val profileTime: Boolean = true,
86+
/**
87+
* Profile number of forks on each instruction.
88+
* */
89+
val profileForks: Boolean = true,
90+
val timeFormat: TimeFormat = TimeFormat.Microseconds,
91+
) {
92+
init {
93+
require(!profileTime || momentOfUpdate == MomentOfUpdate.BeforeStep) {
94+
"Time profiling in now supported only if momentOfUpdate in BeforeStep"
95+
}
96+
}
97+
}
8398

8499
protected val instructionStats = hashMapOf<Statement, MutableMap<StateId, StatsCounter>>()
85100
protected val methodCalls = hashMapOf<Method, MutableMap<StateId, StatsCounter>>()
86101

87-
private val stackTraceTracker = StackTraceTracker<Statement, Method, State>(statementOperations)
102+
private val stackTraceTracker = StackTraceTracker(statementOperations)
88103
private val stackTraces = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
89104
private val forksCount = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
105+
private val instructionTime = hashMapOf<TrieNode<Statement, *>, MutableMap<StateId, StatsCounter>>()
106+
107+
private var lastPeekMoment = 0L
108+
private var lastStackTrace: TrieNode<Statement, *>? = null
90109

91110
override fun onStatePeeked(state: State) {
92-
if (profilerOptions.momentOfUpdate == MomentOfUpdate.BeforeStep) {
93-
processStateUpdate(state)
111+
if (profilerOptions.momentOfUpdate != MomentOfUpdate.BeforeStep) {
112+
return
113+
}
114+
115+
processStateUpdate(state)
116+
117+
if (profilerOptions.profileTime) {
118+
lastPeekMoment = System.nanoTime()
94119
}
95120
}
96121

@@ -100,6 +125,20 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
100125
processStateUpdate(it)
101126
}
102127
}
128+
129+
if (profilerOptions.momentOfUpdate == MomentOfUpdate.BeforeStep && profilerOptions.profileTime) {
130+
val stackTrace = lastStackTrace
131+
?: error("stackTraceAfterPeek should have been memorized")
132+
incrementInstructionTime(parent, stackTrace, System.nanoTime() - lastPeekMoment)
133+
}
134+
}
135+
136+
private fun incrementInstructionTime(state: State, stackTrace: TrieNode<Statement, *>, time: Long) {
137+
var st = stackTrace
138+
while (true) {
139+
instructionTime.increment(st, state, value = time)
140+
st = st.parent() ?: break
141+
}
103142
}
104143

105144
private fun processStateUpdate(state: State) {
@@ -124,17 +163,18 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
124163
val fork = statementOperations.forkHappened(state, node)
125164

126165
var st = stackTraceTracker.getStackTrace(state, node.statement)
166+
lastStackTrace = st
127167
while (true) {
128168
stackTraces.increment(st, state)
129169
if (fork) forksCount.increment(st, state)
130170
st = st.parent() ?: break
131171
}
132172
}
133173

134-
private fun <K> MutableMap<K, MutableMap<StateId, StatsCounter>>.increment(key: K, state: State) {
174+
private fun <K> MutableMap<K, MutableMap<StateId, StatsCounter>>.increment(key: K, state: State, value: Long = 1L) {
135175
val stateStats = this.getOrPut(key) { hashMapOf() }
136176
val stats = stateStats.getOrPut(state.id) { StatsCounter() }
137-
stats.increment()
177+
stats.add(value)
138178
}
139179

140180
private fun aggregateStackTraces(slice: StateId?): ProfileFrame<Statement, Method, State> {
@@ -143,36 +183,51 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
143183
}
144184
return ProfileFrame(
145185
inst = null,
146-
total = -1,
147-
self = -1,
186+
totalSteps = -1,
187+
selfSteps = -1,
148188
totalForks = -1,
149189
selfForks = -1,
190+
totalTime = -1,
191+
selfTime = -1,
150192
children = children,
151193
profilerOptions,
152194
statementOperations,
153195
)
154196
}
155197

198+
private fun formatTime(time: Long): Long {
199+
return when (profilerOptions.timeFormat) {
200+
TimeFormat.Nanoseconds -> time
201+
TimeFormat.Microseconds -> time / MICRO_IN_NANO
202+
TimeFormat.Milliseconds -> time / MILLIES_IN_NANO
203+
}
204+
}
205+
156206
private fun computeProfileFrame(
157207
slice: StateId?,
158208
inst: Statement,
159209
root: TrieNode<Statement, *>,
160210
): ProfileFrame<Statement, Method, State> {
161211
val allNodeStats = stackTraces[root].orEmpty()
162212
val allForkStats = forksCount[root].orEmpty()
213+
val allTimeStats = instructionTime[root].orEmpty()
163214
val children = root.children.mapValues { (i, node) -> computeProfileFrame(slice, i, node) }
164215

165216
val nodeStats = allNodeStats.sumOfSlice(slice)
166217
val forkStats = allForkStats.sumOfSlice(slice)
218+
val timeStats = allTimeStats.sumOfSlice(slice)
167219

168-
val selfStat = nodeStats - children.values.sumOf { it.total }
220+
val selfStat = nodeStats - children.values.sumOf { it.totalSteps }
169221
val selfForks = forkStats - children.values.sumOf { it.totalForks }
222+
val selfTime = timeStats - children.values.sumOf { it.totalTime }
170223
return ProfileFrame(
171224
inst,
172-
nodeStats,
173-
selfStat,
174-
forkStats,
175-
selfForks,
225+
totalSteps = nodeStats,
226+
selfSteps = selfStat,
227+
totalForks = forkStats,
228+
selfForks = selfForks,
229+
totalTime = formatTime(timeStats),
230+
selfTime = formatTime(selfTime),
176231
children,
177232
profilerOptions,
178233
statementOperations,
@@ -181,26 +236,36 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
181236

182237
private class ProfileFrame<Statement, Method, State : UState<*, Method, Statement, *, *, *>>(
183238
val inst: Statement?,
184-
val total: Long,
185-
val self: Long,
239+
val totalSteps: Long,
240+
val selfSteps: Long,
186241
val totalForks: Long,
187242
val selfForks: Long,
243+
val totalTime: Long,
244+
val selfTime: Long,
188245
val children: Map<Statement, ProfileFrame<Statement, Method, State>>,
189246
private val profilerOptions: Options,
190247
private val statementOperations: StatementOperations<Statement, Method, State>,
191248
) {
192249
fun print(str: StringBuilder, indent: String) {
193250
val sortedChildren = children.entries
194251
.groupBy { statementOperations.getMethodOfStatement(it.key) }.entries
195-
.sortedByDescending { entry -> entry.value.sumOf { it.value.total } }
252+
.sortedByDescending { entry -> entry.value.sumOf { it.value.totalSteps } }
196253

197254
for ((method, inst) in sortedChildren) {
198-
val total = inst.sumOf { it.value.total }
199-
val self = inst.sumOf { it.value.self }
255+
val total = inst.sumOf { it.value.totalSteps }
256+
val self = inst.sumOf { it.value.selfSteps }
200257
val totalForks = inst.sumOf { it.value.totalForks }
201258
val selfForks = inst.sumOf { it.value.selfForks }
202259
val methodRepr = statementOperations.printMethodName(method)
203-
str.appendLine("$indent|__ $methodRepr | Steps $self/$total | Forks $selfForks/$totalForks")
260+
261+
str.append("$indent|__ $methodRepr | Steps $self/$total")
262+
if (profilerOptions.profileForks) {
263+
str.append(" | Forks $selfForks/$totalForks")
264+
}
265+
if (profilerOptions.profileTime) {
266+
str.append(" | Time $selfTime/$totalTime")
267+
}
268+
str.appendLine()
204269

205270
val children = if (profilerOptions.printNonVisitedStatements) {
206271
val allStatements = statementOperations.getAllMethodStatements(method)
@@ -212,10 +277,12 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
212277
} ?: let {
213278
val emptyFrame = ProfileFrame(
214279
childStmt,
215-
total = 0L,
216-
self = 0L,
280+
totalSteps = 0L,
281+
selfSteps = 0L,
217282
totalForks = 0L,
218283
selfForks = 0L,
284+
totalTime = 0L,
285+
selfTime = 0L,
219286
emptyMap(),
220287
profilerOptions,
221288
statementOperations,
@@ -231,10 +298,16 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
231298

232299
for ((i, child) in children) {
233300
val instRepr = statementOperations.printStatement(i).padEnd(profilerOptions.padInstructionEnd)
234-
val line = "$indent$INDENT$instRepr" +
235-
" | Steps ${child.self}/${child.total}" +
236-
" | Forks ${child.selfForks}/${child.totalForks}"
301+
302+
var line = "$indent$INDENT$instRepr | Steps ${child.selfSteps}/${child.totalSteps}"
303+
if (profilerOptions.profileForks) {
304+
line += " | Forks ${child.selfForks}/${child.totalForks}"
305+
}
306+
if (profilerOptions.profileTime) {
307+
line += " | Time ${child.selfTime}/${child.totalTime}"
308+
}
237309
str.appendLine(line)
310+
238311
child.print(str, "$indent$INDENT$INDENT")
239312
}
240313
}
@@ -288,4 +361,15 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
288361
BeforeStep,
289362
AfterStep,
290363
}
364+
365+
enum class TimeFormat {
366+
Milliseconds,
367+
Microseconds,
368+
Nanoseconds,
369+
}
370+
371+
companion object {
372+
private const val MICRO_IN_NANO = 1000L
373+
private const val MILLIES_IN_NANO = 1_000_000L
374+
}
291375
}

‎usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/utils/PyDebugProfileObserver.kt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,5 +57,7 @@ val pyDebugProfileObserver = UDebugProfileObserver(
5757
profilerOptions = UDebugProfileObserver.Options(
5858
momentOfUpdate = UDebugProfileObserver.MomentOfUpdate.AfterStep,
5959
printNonVisitedStatements = true,
60+
profileTime = false,
61+
profileForks = false,
6062
),
6163
)

0 commit comments

Comments
 (0)