From 1ccd34501a539172e31ce9620d7ba0de8b8fe356 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Tue, 19 Sep 2023 18:12:56 +0300 Subject: [PATCH] Fix tree updates iterator (#64) --- .../usvm/memory/SymbolicCollectionUpdates.kt | 1 + .../kotlin/org/usvm/memory/UpdateNodes.kt | 14 ------- .../test/kotlin/org/usvm/CompositionTest.kt | 16 +++++--- ...moryRegionTests.kt => MemoryRegionTest.kt} | 40 ++++++++++++++++++- .../kotlin/org/usvm/regions/ProductRegion.kt | 4 ++ 5 files changed, 55 insertions(+), 20 deletions(-) rename usvm-core/src/test/kotlin/org/usvm/memory/{MemoryRegionTests.kt => MemoryRegionTest.kt} (73%) 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 3d836fb18e..a6b297ac9a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt @@ -337,6 +337,7 @@ data class UTreeUpdates, Sort : USort>( ) : Iterator> { // A set of values we already emitted by this iterator. // Note that it contains ONLY elements that have duplicates by key in the RegionTree. + // Reference equality on UUpdateNodes is very important here. private val emittedUpdates = hashSetOf>() // We can return just `hasNext` value without checking for duplicates since diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt index 5ea08424f5..ead674bd06 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt @@ -115,11 +115,6 @@ class UPinpointUpdateNode( return res } - override fun equals(other: Any?): Boolean = - other is UPinpointUpdateNode<*, *> && this.key == other.key && this.guard == other.guard - - override fun hashCode(): Int = key.hashCode() * 31 + guard.hashCode() // Ignores value - override fun toString(): String = "{$key <- $value}".takeIf { guard.isTrue } ?: "{$key <- $value | $guard}" } @@ -204,15 +199,6 @@ class URangedUpdateNode && - this.adapter == other.adapter && - this.guard == other.guard - - // Ignores update - override fun hashCode(): Int = adapter.hashCode() * 31 + guard.hashCode() - /** * Applies this update node to the [memory] with applying composition via [composer]. */ diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 6928ceff61..7f3ce9b6f4 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -363,12 +363,18 @@ internal class CompositionTest { val sndComposedExpr = sndComposer.compose(fstArrayIndexReading) val fstComposedExpr = fstComposer.compose(sndComposedExpr) - val expectedRegion = region - .write(USymbolicArrayIndex(fstAddress, fstIndex), 1.toBv(), guard = mkTrue()) - .write(USymbolicArrayIndex(sndAddress, sndIndex), 2.toBv(), guard = mkTrue()) - require(fstComposedExpr is UInputArrayReading<*, *>) - assert(fstComposedExpr.collection.updates.toList() == expectedRegion.updates.toList()) + + val updates = fstComposedExpr.collection.updates.toList() + assertEquals(2, updates.size) + val update0 = assertIs>(updates[0]) + val update1 = assertIs>(updates[1]) + + assertEquals(update0.key, USymbolicArrayIndex(fstAddress, fstIndex)) + assertEquals(update0.value, 1.toBv()) + + assertEquals(update1.key, USymbolicArrayIndex(sndAddress, sndIndex)) + assertEquals(update1.value, 2.toBv()) } @Test diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt similarity index 73% rename from usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt rename to usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt index e2dd572c56..acee445d42 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt @@ -13,12 +13,14 @@ import org.usvm.UComponents import org.usvm.UContext import org.usvm.UHeapRef import org.usvm.collection.array.UAllocatedArrayId +import org.usvm.collection.array.UInputArrayId import org.usvm.regions.SetRegion import org.usvm.regions.emptyRegionTree +import kotlin.random.Random import kotlin.test.assertNotNull import kotlin.test.assertTrue -class MemoryRegionTests { +class MemoryRegionTest { private lateinit var ctx: UContext @BeforeEach @@ -107,4 +109,40 @@ class MemoryRegionTests { assertTrue(updatesAfter.last().includesConcretely(idx2, trueExpr)) } + /** + * Tests random writes and reads with array region to ensure there are no REs. + */ + @Test + fun testSymbolicWrites(): Unit = with(ctx) { + val random = Random(42) + val range = 3 + + val concreteRefs = List(range) { mkConcreteHeapRef(it) } + val symbolicRefs = List(range) { mkRegisterReading(it, addressSort) } + val refs = concreteRefs + symbolicRefs + + val concreteIndices = List(range) { mkSizeExpr(it) } + val symbolicIndices = List(range) { mkRegisterReading(it, sizeSort) } + val indices = concreteIndices + symbolicIndices + + val testsCount = 100 + repeat(testsCount) { + var memoryRegion = UInputArrayId(mockk(), addressSort) + .emptyRegion() + + val writesCount = 20 + repeat(writesCount) { + val ref = symbolicRefs.random(random) + val idx = indices.random(random) + val value = refs.random(random) + + memoryRegion = memoryRegion.write(ref to idx, value, trueExpr) + } + + val readRef = symbolicRefs.random(random) + val readIdx = indices.random(random) + + memoryRegion.read(readRef to readIdx) + } + } } \ No newline at end of file diff --git a/usvm-util/src/main/kotlin/org/usvm/regions/ProductRegion.kt b/usvm-util/src/main/kotlin/org/usvm/regions/ProductRegion.kt index 3abb7fd700..6edba23897 100644 --- a/usvm-util/src/main/kotlin/org/usvm/regions/ProductRegion.kt +++ b/usvm-util/src/main/kotlin/org/usvm/regions/ProductRegion.kt @@ -122,4 +122,8 @@ data class ProductRegion, Y : Region>(val products: List + ("$a X $b").prependIndent("\t") + } }