From 5bbea678c059b6e325b48750831891ea8c54e4b6 Mon Sep 17 00:00:00 2001 From: Roman Pozharskiy Date: Wed, 18 Jun 2025 17:53:31 +0300 Subject: [PATCH 1/2] fix splitting for range updates --- .../usvm/memory/SymbolicCollectionUpdates.kt | 70 ++++++++++--------- .../org/usvm/memory/HeapRefSplittingTest.kt | 37 ++++++++++ 2 files changed, 74 insertions(+), 33 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt index 3f3057cad3..b4bd1745d7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt @@ -1,12 +1,8 @@ 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 -import org.usvm.USort -import org.usvm.isFalse +import org.usvm.* import org.usvm.regions.Region import org.usvm.regions.RegionTree import org.usvm.regions.emptyRegionTree @@ -317,44 +313,52 @@ data class UTreeUpdates, Sort : USort>( guardBuilder: GuardBuilder, composer: UComposer<*, *>?, ): UTreeUpdates { - var restRecordsAreIrrelevant = false - val symbolicSubtreesStack = - mutableListOf, RegionTree>>>>() - - fun traverseTreeWhilePredicateSatisfied(tree: RegionTree>) { + // returns fully symbolic tree entries after splitting + fun traverseTreeWhilePredicateSatisfied( + tree: RegionTree>, + ): List, RegionTree>>>> { + val symbolicEntries = + mutableListOf, RegionTree>>>>() // 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, RegionTree>>>() + 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 List>.toPersistentMap(): PersistentMap { + val builder = persistentMapOf().builder() + for ((reg, tree) in this) { + builder[reg] = tree } - - return this.copy(updates = RegionTree(splitTreeEntries.toPersistentMap())) + return builder.build() } override fun splitWrite( diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt index 9488981e04..ff1609472d 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt +++ b/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) + } } From fb39a7e7b7967a0e74fe619456d88bc6702846fe Mon Sep 17 00:00:00 2001 From: Roman Pozharskiy Date: Wed, 18 Jun 2025 17:59:44 +0300 Subject: [PATCH 2/2] fix imports --- .../kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt index b4bd1745d7..96222b319b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt @@ -2,7 +2,11 @@ package org.usvm.memory import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf -import org.usvm.* +import org.usvm.UBoolExpr +import org.usvm.UComposer +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.isFalse import org.usvm.regions.Region import org.usvm.regions.RegionTree import org.usvm.regions.emptyRegionTree