More fixes for real applications

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 = "4ff7243d3a"
+    const val jacodb = "238c1ccd14"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -56,7 +56,9 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
         contract {
             callsInPlace(block, InvocationKind.EXACTLY_ONCE)
         }
-        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        check(canProcessFurtherOnCurrentStep) {
+            "Caller should check before processing the current hop further"
+        }
         return originalState.block()
     }
 

usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt

@@ -1,7 +1,7 @@
 package org.usvm.memory
 
+import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
-import kotlinx.collections.immutable.toPersistentMap
 import org.usvm.UBoolExpr
 import org.usvm.UComposer
 import org.usvm.UExpr
@@ -317,44 +317,52 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         guardBuilder: GuardBuilder,
         composer: UComposer<*, *>?,
     ): UTreeUpdates<Key, Reg, Sort> {
-        var restRecordsAreIrrelevant = false
-        val symbolicSubtreesStack =
-            mutableListOf<Pair<Reg, Pair<UUpdateNode<Key, Sort>, RegionTree<Reg, UUpdateNode<Key, Sort>>>>>()
-
-        fun traverseTreeWhilePredicateSatisfied(tree: RegionTree<Reg, UUpdateNode<Key, Sort>>) {
+        // returns fully symbolic tree entries after splitting
+        fun traverseTreeWhilePredicateSatisfied(
+            tree: RegionTree<Reg, UUpdateNode<Key, Sort>>,
+        ): List<Pair<Reg, Pair<UUpdateNode<Key, Sort>, RegionTree<Reg, UUpdateNode<Key, Sort>>>>> {
+            val symbolicEntries =
+                mutableListOf<Pair<Reg, Pair<UUpdateNode<Key, Sort>, RegionTree<Reg, UUpdateNode<Key, Sort>>>>>()
             // process nodes of the same level from newest to oldest
-            for ((reg, entry) in tree.entries.toList().reversed()) {
+            for ((reg, entry) in tree.entries.toList().asReversed()) {
                 val (node, subtree) = entry
                 val splitUpdate = node.split(key, predicate, matchingWrites, guardBuilder, composer)
-                // range nodes are considered to belong to invariant tree since they can contain concretes
-                if (splitUpdate === null || node is URangedUpdateNode<*, *, Key, Sort>) {
-                    traverseTreeWhilePredicateSatisfied(subtree)
-                    if (restRecordsAreIrrelevant) break
-                } else {
-                    // since [splitWrite] preserves invariant that records satisfying predicate are always
-                    // at the top of the tree  we can just add rest branch to splitTreeEntries
-                    symbolicSubtreesStack += reg to entry
+                when (splitUpdate) {
+                    null -> {
+                        val restSymbolicTree = traverseTreeWhilePredicateSatisfied(subtree)
+                        symbolicEntries += restSymbolicTree
+                    }
+                    // range nodes are considered to belong to concrete subtree since they can contain concretes
+                    is URangedUpdateNode<*, *, Key, Sort> -> {
+                        val restSymbolicEntries = traverseTreeWhilePredicateSatisfied(subtree)
+                        val restTree = RegionTree(restSymbolicEntries.asReversed().toPersistentMap())
+                        symbolicEntries.add(reg to (splitUpdate to restTree))
+                    }
+
+                    else -> {
+                        // since [splitWrite] preserves invariant that records satisfying predicate are always
+                        // at the top of the tree  we can just add rest branch to splitTreeEntries
+                        symbolicEntries.add(reg to entry)
+                    }
                 }
 
-                if (guardBuilder.isFalse) {
-                    restRecordsAreIrrelevant = true
-                    break
-                }
+                if (guardBuilder.isFalse) break
             }
+
+            return symbolicEntries
         }
 
-        traverseTreeWhilePredicateSatisfied(updates)
+        val symbolicEntries = traverseTreeWhilePredicateSatisfied(updates)
 
-        val splitTreeEntries =
-            mutableMapOf<Reg, Pair<UUpdateNode<Key, Sort>, RegionTree<Reg, UUpdateNode<Key, Sort>>>>()
+        return this.copy(updates = RegionTree(symbolicEntries.asReversed().toPersistentMap()))
+    }
 
-        // reconstruct region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order
-        while (symbolicSubtreesStack.isNotEmpty()) {
-            val (reg, entry) = symbolicSubtreesStack.removeLast()
-            splitTreeEntries[reg] = entry
+    private fun <K, V> List<Pair<K, V>>.toPersistentMap(): PersistentMap<K, V> {
+        val builder = persistentMapOf<K, V>().builder()
+        for ((reg, tree) in this) {
+            builder[reg] = tree
         }
-
-        return this.copy(updates = RegionTree(splitTreeEntries.toPersistentMap()))
+        return builder.build()
     }
 
     override fun splitWrite(

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

@@ -79,18 +79,43 @@ 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,
+        val timeFormat: TimeFormat = TimeFormat.Microseconds,
+    ) {
+        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.nanoTime()
         }
     }
 
@@ -100,6 +125,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.nanoTime() - 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,17 +163,18 @@ 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)
             st = st.parent() ?: break
         }
     }
 
-    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,36 +183,51 @@ 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,
         )
     }
 
+    private fun formatTime(time: Long): Long {
+        return when (profilerOptions.timeFormat) {
+            TimeFormat.Nanoseconds -> time
+            TimeFormat.Microseconds -> time / MICRO_IN_NANO
+            TimeFormat.Milliseconds -> time / MILLIES_IN_NANO
+        }
+    }
+
     private fun computeProfileFrame(
         slice: StateId?,
         inst: Statement,
         root: TrieNode<Statement, *>,
     ): 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 = formatTime(timeStats),
+            selfTime = formatTime(selfTime),
             children,
             profilerOptions,
             statementOperations,
@@ -181,26 +236,36 @@ 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>,
     ) {
         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 +277,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 +298,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")
                 }
             }
@@ -288,4 +361,15 @@ open class UDebugProfileObserver<Statement, Method, State : UState<*, Method, St
         BeforeStep,
         AfterStep,
     }
+
+    enum class TimeFormat {
+        Milliseconds,
+        Microseconds,
+        Nanoseconds,
+    }
+
+    companion object {
+        private const val MICRO_IN_NANO = 1000L
+        private const val MILLIES_IN_NANO = 1_000_000L
+    }
 }

usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt

@@ -445,4 +445,41 @@ class HeapRefSplittingTest {
 
         return array to ref
     }
+
+    @Test
+    fun testRangedUpdateWithMixedWrite() = with(ctx) {
+        val ref = allocateConcreteRef()
+        val idx0 = mkSizeExpr(0)
+        val idx1 = mkSizeExpr(1)
+        val idx2 = mkSizeExpr(2)
+
+        val concreteValue1 = allocateConcreteRef()
+        val symbolicValue2 = mkRegisterReading(0, addressSort)
+        val concreteValue3 = allocateConcreteRef()
+
+        heap.writeArrayIndex(ref, idx0, arrayDescr.first, arrayDescr.second, concreteValue1, trueExpr)
+        heap.writeArrayIndex(ref, idx1, arrayDescr.first, arrayDescr.second, symbolicValue2, trueExpr)
+        heap.writeArrayIndex(ref, idx2, arrayDescr.first, arrayDescr.second, concreteValue3, trueExpr)
+
+        heap.memcpy(ref, ref, arrayDescr.first, arrayDescr.second, idx1, idx0, idx1)
+
+        val read = heap.readArrayIndex(ref, idx0, arrayDescr.first, arrayDescr.second)
+        assertSame(symbolicValue2, read)
+    }
+
+    @Test
+    fun testClone() = with(ctx) {
+        val ref = allocateConcreteRef()
+        val idx = mkSizeExpr(2)
+
+        val concreteValue = allocateConcreteRef()
+
+        heap.writeArrayIndex(ref, idx, arrayDescr.first, arrayDescr.second, concreteValue, trueExpr)
+
+        val copyRef = allocateConcreteRef()
+        heap.memcpy(ref, copyRef, arrayDescr.first, arrayDescr.second, mkBv(0), mkBv(0), mkBv(3))
+
+        val read = heap.readArrayIndex(copyRef, idx, arrayDescr.first, arrayDescr.second)
+        assertSame(read, concreteValue)
+    }
 }