Fix tree updates iterator (#64)

Author: sergeypospelov

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

@@ -337,6 +337,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
     ) : Iterator<UUpdateNode<Key, Sort>> {
         // 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<UUpdateNode<Key, Sort>>()
 
         // We can return just `hasNext` value without checking for duplicates since

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

@@ -115,11 +115,6 @@ class UPinpointUpdateNode<Key, Sort : USort>(
         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<CollectionId : USymbolicCollectionId<SrcKey, Sort, Colle
         return resultUpdateNode
     }
 
-    // Ignores update
-    override fun equals(other: Any?): Boolean =
-        other is 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].
      */

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<UPinpointUpdateNode<USymbolicArrayIndex, USizeSort>>(updates[0])
+        val update1 = assertIs<UPinpointUpdateNode<USymbolicArrayIndex, USizeSort>>(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

usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt renamed to 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<Type>(), 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)
+        }
+    }
 }

usvm-util/src/main/kotlin/org/usvm/regions/ProductRegion.kt

@@ -122,4 +122,8 @@ data class ProductRegion<X : Region<X>, Y : Region<Y>>(val products: List<Pair<X
         }
         return ProductRegion(newProducts)
     }
+
+    override fun toString(): String = products.joinToString(prefix = "{", separator = ", ", postfix = "}") { (a , b) ->
+        ("$a X $b").prependIndent("\t")
+    }
 }