Region tree renaming and fix

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

@@ -333,6 +333,6 @@ class UIsExpr<Type> internal constructor(
 //region Utils
 
 val UBoolExpr.isFalse get() = this === ctx.falseExpr
-val UBoolExpr.isTrue get() = !isFalse
+val UBoolExpr.isTrue get() = this === ctx.trueExpr
 
 //endregion

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

@@ -366,7 +366,7 @@ fun <ArrayType, Sort : USort> initializedAllocatedArrayRegion(
     content: Map<USizeExpr, UExpr<Sort>>,
     guard: UBoolExpr
 ): UAllocatedArrayRegion<ArrayType, Sort> {
-    val emptyRegionTree = emptyRegionTree<UUpdateNode<USizeExpr, Sort>, UArrayIndexRegion>()
+    val emptyRegionTree = emptyRegionTree<UArrayIndexRegion, UUpdateNode<USizeExpr, Sort>>()
 
     val entries = content.entries.associate { (key, value) ->
         val region = indexRegion(key)

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

@@ -77,7 +77,7 @@ interface UMemoryUpdates<Key, Sort : USort> : Sequence<UUpdateNode<Key, Sort>> {
 
     /**
      * Accepts the [visitor]. Implementations should call [UMemoryUpdatesVisitor.visitInitialValue] firstly, then call
-     * [UMemoryUpdatesVisitor.visitUpdateNode] in the chronological order
+     * [UMemoryUpdatesVisitor.visitUpdate] in the chronological order
      * (from the oldest to the newest) with accumulated [Result].
      *
      * Uses [lookupCache] to shortcut the traversal. The actual key is determined by the
@@ -183,6 +183,11 @@ class UFlatUpdates<Key, Sort : USort> private constructor(
         val mappedNode = node.update.map(keyMapper, composer)
         val mappedNext = node.next.map(keyMapper, composer)
 
+        // Doesn't apply the node, if its guard maps to `false`
+        if (mappedNode.guard.isFalse) {
+            return mappedNext
+        }
+
         // If nothing changed, return this updates
         if (mappedNode === node.update && mappedNext === node.next) {
             return this
@@ -250,7 +255,7 @@ class UFlatUpdates<Key, Sort : USort> private constructor(
 //region Tree memory updates
 
 data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
-    private val updates: RegionTree<UUpdateNode<Key, Sort>, Reg>,
+    private val updates: RegionTree<Reg, UUpdateNode<Key, Sort>>,
     private val keyToRegion: (Key) -> Reg,
     private val keyRangeToRegion: (Key, Key) -> Reg,
     private val symbolicEq: (Key, Key) -> UBoolExpr,
@@ -259,7 +264,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
 ) : UMemoryUpdates<Key, Sort> {
     override fun read(key: Key): UTreeUpdates<Key, Reg, Sort> {
         val reg = keyToRegion(key)
-        val updates = updates.localize(reg)
+        val updates = updates.localize(reg) { it.includesSymbolically(key).isFalse }
         if (updates === this.updates) {
             return this
         }
@@ -272,7 +277,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         val newUpdates = updates.write(
             keyToRegion(key),
             update,
-            keyFilter = { it.isIncludedByUpdateConcretely(update) }
+            valueFilter = { it.isIncludedByUpdateConcretely(update) }
         )
 
         return this.copy(updates = newUpdates)
@@ -290,7 +295,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         val newUpdates = updates.write(
             region,
             update,
-            keyFilter = { it.isIncludedByUpdateConcretely(update) }
+            valueFilter = { it.isIncludedByUpdateConcretely(update) }
         )
 
         return this.copy(updates = newUpdates)
@@ -306,15 +311,15 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         val updatesSuffix = mutableListOf<UUpdateNode<Key, Sort>?>()
 
         // reconstructed region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order
-        var splitUpdates = emptyRegionTree<UUpdateNode<Key, Sort>, Reg>()
+        var splitUpdates = emptyRegionTree<Reg, UUpdateNode<Key, Sort>>()
 
         // add an update to result tree
         fun applyUpdate(update: UUpdateNode<Key, Sort>) {
             val region = when (update) {
                 is UPinpointUpdateNode<Key, Sort> -> keyToRegion(update.key)
                 is URangedUpdateNode<*, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey)
             }
-            splitUpdates = splitUpdates.write(region, update, keyFilter = { it.isIncludedByUpdateConcretely(update) })
+            splitUpdates = splitUpdates.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) })
         }
 
         // traverse all updates one by one from the oldest one
@@ -366,31 +371,35 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         var mappedNodeFound = false
 
         // Traverse [updates] using its iterator and fold them into a new updates tree with new mapped nodes
-        val initialEmptyTree = emptyRegionTree<UUpdateNode<Key, Sort>, Reg>()
+        val initialEmptyTree = emptyRegionTree<Reg, UUpdateNode<Key, Sort>>()
         val mappedUpdates = updates.fold(initialEmptyTree) { mappedUpdatesTree, updateNodeWithRegion ->
             val (updateNode, oldRegion) = updateNodeWithRegion
             // Map current node
             val mappedUpdateNode = updateNode.map(keyMapper, composer)
 
+
             // Save information about whether something changed in the current node or not
             if (mappedUpdateNode !== updateNode) {
                 mappedNodeFound = true
             }
 
+            // Doesn't apply the node, if its guard maps to `false`
+            if (mappedUpdateNode.guard.isFalse) {
+                return@fold mappedUpdatesTree
+            }
+
             // Note that following code should be executed after checking for reference equality of a mapped node.
             // Otherwise, it is possible that for a tree with several impossible writes
             // it will be returned as a result, instead of an empty one.
 
             // Extract a new region by the mapped node
-            val newRegion = when (updateNode) {
+            val newRegion = when (mappedUpdateNode) {
                 is UPinpointUpdateNode -> {
-                    mappedUpdateNode as UPinpointUpdateNode
                     val currentRegion = keyToRegion(mappedUpdateNode.key)
                     oldRegion.intersect(currentRegion)
                 }
 
                 is URangedUpdateNode<*, *, Key, Sort> -> {
-                    mappedUpdateNode as URangedUpdateNode<*, *, Key, Sort>
                     val currentRegion = keyRangeToRegion(mappedUpdateNode.fromKey, mappedUpdateNode.toKey)
                     oldRegion.intersect(currentRegion)
                 }
@@ -512,7 +521,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
          * *
          *```
          */
-        private fun leftMostFold(updates: RegionTree<UUpdateNode<Key, Sort>, *>): Result {
+        private fun leftMostFold(updates: RegionTree<*, UUpdateNode<Key, Sort>>): Result {
             var result = cache[updates]
 
             if (result != null) {
@@ -531,7 +540,7 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
 
         private fun notLeftMostFold(
             accumulator: Result,
-            iterator: Iterator<Map.Entry<Region<*>, Pair<UUpdateNode<Key, Sort>, RegionTree<UUpdateNode<Key, Sort>, *>>>>,
+            iterator: Iterator<Map.Entry<Region<*>, Pair<UUpdateNode<Key, Sort>, RegionTree<*, UUpdateNode<Key, Sort>>>>>,
         ): Result {
             var accumulated = accumulator
             while (iterator.hasNext()) {

usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt

@@ -315,11 +315,11 @@ internal class CompositionTest {
 
     @Test
     fun testComposeSeveralTimes() = with(ctx) {
-        val fstAddress = mockk<USymbolicHeapRef>()
-        val fstIndex = mockk<USizeExpr>()
+        val fstAddress = mkRegisterReading(0, addressSort)
+        val fstIndex = mkRegisterReading(1, sizeSort)
 
-        val sndAddress = mockk<USymbolicHeapRef>()
-        val sndIndex = mockk<USizeExpr>()
+        val sndAddress = mkRegisterReading(2, addressSort)
+        val sndIndex = mkRegisterReading(3, sizeSort)
 
         val arrayType: KClass<Array<*>> = Array::class
         // Create an empty region

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

@@ -3,8 +3,10 @@ package org.usvm.memory
 import io.ksmt.utils.mkConst
 import io.mockk.every
 import io.mockk.mockk
+import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
+import org.usvm.Type
 import org.usvm.UBv32Sort
 import org.usvm.UComponents
 import org.usvm.UContext
@@ -71,14 +73,36 @@ class MemoryRegionTests {
             ).write(address, 1.toBv(), guard)
                 .write(address, 2.toBv(), anotherGuard)
 
-           assertTrue(treeUpdates.toList().size == 2)
+           assertEquals(2, treeUpdates.toList().size)
 
             val anotherTreeUpdates = treeUpdates
                 .write(address, 3.toBv(), anotherGuard)
                 .write(address, 4.toBv(), guard)
 
-           assertTrue(anotherTreeUpdates.toList().size == 2)
+            assertEquals(3, anotherTreeUpdates.toList().size)
         }
     }
 
+    @Test
+    fun testKeyFiltering() = with(ctx) {
+        val idx1 = mkRegisterReading(0, sizeSort)
+        val idx2 = mkRegisterReading(1, sizeSort)
+
+        val memoryRegion = emptyAllocatedArrayRegion(mockk<Type>(), 0, sizeSort)
+            .write(idx1, mkBv(0), trueExpr)
+            .write(idx2, mkBv(1), trueExpr)
+
+        val updatesBefore = memoryRegion.updates.toList()
+        assertEquals(2, updatesBefore.size)
+        assertTrue(updatesBefore.first().includesConcretely(idx1, trueExpr))
+        assertTrue(updatesBefore.last().includesConcretely(idx2, trueExpr))
+
+        val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr)
+
+        val updatesAfter = memoryRegionAfter.updates.toList()
+        assertEquals(2, updatesAfter.size)
+        assertTrue(updatesAfter.first().includesConcretely(idx1, trueExpr))
+        assertTrue(updatesAfter.last().includesConcretely(idx2, trueExpr))
+    }
+
 }

usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt

@@ -3,6 +3,7 @@ package org.usvm.model
 import io.mockk.every
 import io.mockk.mockk
 import kotlinx.collections.immutable.persistentMapOf
+import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.usvm.*
@@ -169,4 +170,49 @@ class ModelCompositionTest {
         val expr = composer.compose(reading)
         assertSame(composedRef0, expr)
     }
+
+    @Test
+    fun testComposeAllocatedArrayWithFalseOverwrite() = with(ctx) {
+        val heapEvaluator = UHeapEagerModel<Field, Type>(
+            concreteNull,
+            mapOf(),
+            mapOf(),
+            mapOf(),
+        )
+
+        val index0 = 0.toBv()
+        val index1 = 1.toBv()
+
+        val defaultValue = bv32Sort.sampleUValue()
+        val nonDefaultValue0 = 17.toBv()
+        val nonDefaultValue1 = 42.toBv()
+
+        val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to trueExpr, 1 to falseExpr))
+        val trueGuard = mkRegisterReading(0, boolSort)
+        val falseGuard = mkRegisterReading(1, boolSort)
+
+        val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk())
+
+        val emptyRegion = emptyAllocatedArrayRegion<Type, UBv32Sort>(mockk(), 1, bv32Sort)
+
+        run {
+            val region = emptyRegion
+                .write(index0, nonDefaultValue0, trueGuard)
+                .write(index0, nonDefaultValue1, falseGuard)
+            val reading = region.read(index0)
+
+            val expr = composer.compose(reading)
+            assertEquals(nonDefaultValue0, expr)
+        }
+
+        run {
+            val region = emptyRegion
+                .write(index1, nonDefaultValue0, trueGuard)
+                .write(index0, nonDefaultValue1, falseGuard)
+            val reading = region.read(index0)
+
+            val expr = composer.compose(reading)
+            assertEquals(defaultValue, expr)
+        }
+    }
 }