UHeapReading composition fixes (#37)

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

@@ -1,5 +1,8 @@
 package org.usvm
 
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KIteExpr
+import io.ksmt.sort.KSort
 import org.usvm.constraints.UTypeEvaluator
 import org.usvm.memory.UReadOnlySymbolicHeap
 import org.usvm.memory.URegionId
@@ -18,6 +21,15 @@ open class UComposer<Field, Type>(
     override fun <Sort : USort> transform(expr: USymbol<Sort>): UExpr<Sort> =
         error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
 
+    override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T> =
+        transformExprAfterTransformed(expr, expr.condition) { condition ->
+            when {
+                condition.isTrue -> apply(expr.trueBranch)
+                condition.isFalse -> apply(expr.falseBranch)
+                else -> super.transform(expr)
+            }
+        }
+
     override fun <Sort : USort> transform(
         expr: URegisterReading<Sort>,
     ): UExpr<Sort> = with(expr) { stackEvaluator.readRegister(idx, sort) }

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

@@ -50,7 +50,7 @@ data class USymbolicMemoryRegion<out RegionId : URegionId<Key, Sort, RegionId>,
     val sort: Sort get() = regionId.sort
 
     // If we replace it with get(), we have to check for nullability in read function.
-    val defaultValue = regionId.defaultValue
+    private val defaultValue = regionId.defaultValue
 
     private fun read(key: Key, updates: UMemoryUpdates<Key, Sort>): UExpr<Sort> {
         val lastUpdatedElement = updates.lastUpdatedElementOrNull()
@@ -79,6 +79,7 @@ data class USymbolicMemoryRegion<out RegionId : URegionId<Key, Sort, RegionId>,
     override fun read(key: Key): UExpr<Sort> {
         if (sort == sort.uctx.addressSort) {
             // Here we split concrete heap addresses from symbolic ones to optimize further memory operations.
+            // But doing this for composition seems a little bit strange
             return splittingRead(key) { it is UConcreteHeapRef }
         }
 
@@ -157,12 +158,14 @@ data class USymbolicMemoryRegion<out RegionId : URegionId<Key, Sort, RegionId>,
         matchingWrites: MutableList<GuardedExpr<UExpr<Sort>>>,
         guardBuilder: GuardBuilder,
     ): USymbolicMemoryRegion<RegionId, Key, Sort> {
-        // TODO: either check in USymbolicMemoryRegion constructor that we do not construct memory region with
-        //       non-null reference as default value, or implement splitting by default value.
-        assert(defaultValue == null || !predicate(defaultValue))
-
         val splitUpdates = updates.read(key).split(key, predicate, matchingWrites, guardBuilder)
 
+        // we traversed all updates, so predicate says that key misses all the writes to this memory region,
+        // therefore, the key maps to the default value
+        if (defaultValue != null && predicate(defaultValue)) {
+            matchingWrites += defaultValue with guardBuilder.nonMatchingUpdatesGuard
+        }
+
         return if (splitUpdates === updates) {
             this
         } else {
@@ -230,7 +233,11 @@ data class USymbolicMemoryRegion<out RegionId : URegionId<Key, Sort, RegionId>,
     override fun toString(): String =
         buildString {
             append('<')
-            append(defaultValue)
+            if (defaultValue != null) {
+                append(defaultValue)
+            } else {
+                append("_")
+            }
             updates.forEach {
                 append(it.toString())
             }

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

@@ -103,7 +103,6 @@ interface UMemoryUpdatesVisitor<Key, Sort : USort, Result> {
 }
 
 
-
 //region Flat memory updates
 
 class UFlatUpdates<Key, Sort : USort> private constructor(
@@ -307,60 +306,44 @@ data class UTreeUpdates<Key, Reg : Region<Reg>, Sort : USort>(
         matchingWrites: MutableList<GuardedExpr<UExpr<Sort>>>,
         guardBuilder: GuardBuilder,
     ): UTreeUpdates<Key, Reg, Sort> {
-        // the suffix of the [updates], starting from the earliest update satisfying `predicate(update.value(key))`
-        val updatesSuffix = mutableListOf<UUpdateNode<Key, Sort>?>()
-
         // reconstructed region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order
-        var splitUpdates = emptyRegionTree<Reg, UUpdateNode<Key, Sort>>()
+        var splitRegionTree = 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, valueFilter = { it.isIncludedByUpdateConcretely(update) })
+            splitRegionTree =
+                splitRegionTree.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) })
         }
 
-        // traverse all updates one by one from the oldest one
-        for (update in this) {
-            val satisfies = predicate(update.value(key))
-
-            if (updatesSuffix.isNotEmpty()) {
-                updatesSuffix += update
-            } else if (satisfies) {
-                // we found the first matched update, so we have to apply already visited updates
-                // definitely unsatisfying `predicate(update.value(key))`
-                for (prevUpdate in this) {
-                    if (prevUpdate === update) {
-                        break
-                    }
-                    applyUpdate(update)
-                }
-                updatesSuffix += update
-            }
+
+        var hasChanged = false
+        // here we split updates from the newest to the oldest
+        val splitUpdates = toMutableList<UUpdateNode<Key, Sort>?>().apply { reverse() }
+        for ((idx, update) in splitUpdates.withIndex()) {
+            val splitUpdate = update?.split(key, predicate, matchingWrites, guardBuilder)
+            hasChanged = hasChanged or (update !== splitUpdate)
+            splitUpdates[idx] = splitUpdate
         }
 
-        // no matching updates were found
-        if (updatesSuffix.isEmpty()) {
+        // if nothing changed, return this
+        if (!hasChanged) {
             return this
         }
 
+        // traverse all updates one by one from the oldest one
         // here we collect matchingWrites and update guardBuilder in the correct order (from the newest to the oldest)
-        for (idx in updatesSuffix.indices.reversed()) {
-            val update = requireNotNull(updatesSuffix[idx])
-            updatesSuffix[idx] = update.split(key, predicate, matchingWrites, guardBuilder)
-        }
-
-        // here we apply the remaining updates
-        for (update in updatesSuffix) {
+        for (update in splitUpdates.asReversed()) {
             if (update != null) {
                 applyUpdate(update)
             }
         }
 
 
-        return this.copy(updates = splitUpdates)
+        return this.copy(updates = splitRegionTree)
     }
 
 

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

@@ -9,6 +9,7 @@ import io.ksmt.expr.transformer.KTransformerBase
 import io.ksmt.sort.KBv32Sort
 import io.mockk.every
 import io.mockk.mockk
+import io.mockk.spyk
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.assertThrows
@@ -33,6 +34,7 @@ import org.usvm.memory.USymbolicArrayIndex
 import org.usvm.memory.UUpdateNode
 import org.usvm.memory.emptyAllocatedArrayRegion
 import org.usvm.memory.emptyInputArrayRegion
+import org.usvm.model.UHeapEagerModel
 import org.usvm.model.URegistersStackEagerModel
 import kotlin.reflect.KClass
 import kotlin.test.assertEquals
@@ -425,6 +427,38 @@ internal class CompositionTest {
         assertSame(fstComposedValue, sndComposedValue)
     }
 
+    @Test
+    fun testUAllocatedArrayAddressSortIndexReading() = with(ctx) {
+        val arrayType: KClass<Array<*>> = Array::class
+
+        val symbolicIndex = mockk<USizeExpr>()
+        val symbolicAddress = mkRegisterReading(0, addressSort)
+
+        val regionArray = emptyAllocatedArrayRegion(arrayType, 0, addressSort)
+            .write(mkBv(0), symbolicAddress, trueExpr)
+            .write(mkBv(1), mkConcreteHeapRef(1), trueExpr)
+
+        val reading = mkAllocatedArrayReading(regionArray, symbolicIndex)
+
+        val concreteNullRef = mkConcreteHeapRef(NULL_ADDRESS)
+        val heapToComposeWith = UHeapEagerModel<Field, KClass<Array<*>>>(
+            concreteNullRef,
+            emptyMap(),
+            emptyMap(),
+            emptyMap()
+        )
+
+        val typeEvaluator = mockk<UTypeEvaluator<KClass<Array<*>>>>()
+        val composer = spyk(UComposer(ctx, stackEvaluator, heapToComposeWith, typeEvaluator, mockEvaluator))
+
+        every { symbolicIndex.accept(composer) } returns mkBv(2)
+        every { symbolicAddress.accept(composer) } returns mkConcreteHeapRef(-1)
+
+        val composedReading = composer.compose(reading)
+
+        assertSame(composedReading, concreteNullRef)
+    }
+
     @Test
     fun testUFieldReading() = with(ctx) {
         val aAddress = mockk<USymbolicHeapRef>()

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

@@ -1,10 +1,10 @@
 package org.usvm.memory
 
+import io.ksmt.utils.getValue
 import io.mockk.every
 import io.mockk.mockk
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
-import io.ksmt.utils.getValue
 import org.usvm.Field
 import org.usvm.Type
 import org.usvm.UComponents

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

@@ -1,11 +1,11 @@
 package org.usvm.memory
 
+import io.ksmt.expr.rewrite.simplify.KExprSimplifier
+import io.ksmt.utils.getValue
 import io.mockk.every
 import io.mockk.mockk
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
-import io.ksmt.expr.rewrite.simplify.KExprSimplifier
-import io.ksmt.utils.getValue
 import org.usvm.Field
 import org.usvm.Type
 import org.usvm.UAddressSort
@@ -33,6 +33,7 @@ class HeapRefSplittingTest {
         every { components.mkTypeSystem(any()) } returns mockk()
         ctx = UContext(components)
         heap = URegionHeap(ctx)
+
         valueFieldDescr = mockk<Field>() to ctx.bv32Sort
         addressFieldDescr = mockk<Field>() to ctx.addressSort
         arrayDescr = mockk<Type>() to ctx.addressSort

usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt

@@ -16,6 +16,7 @@ import org.usvm.UAddressSort
 import org.usvm.UBv32Sort
 import org.usvm.UComponents
 import org.usvm.UContext
+import org.usvm.memory.UAllocatedToAllocatedKeyConverter
 import org.usvm.memory.UInputToAllocatedKeyConverter
 import org.usvm.memory.UInputToInputKeyConverter
 import org.usvm.memory.URegionHeap
@@ -279,6 +280,76 @@ class TranslationTest {
         assertSame(KSolverStatus.UNSAT, status)
     }
 
+    @Test
+    fun testTranslateInputToInputArrayCopyAddressSort() = with(ctx) {
+        val ref1 = mkRegisterReading(0, addressSort)
+        val idx1 = mkRegisterReading(1, sizeSort)
+        val val1 = mkConcreteHeapRef(1)
+
+        val ref2 = mkRegisterReading(2, addressSort)
+        val idx2 = mkRegisterReading(3, sizeSort)
+        val val2 = mkRegisterReading(5, addressSort)
+
+        val inputRegion1 = emptyInputArrayRegion(valueArrayDescr, addressSort)
+            .write(ref1 to idx1, val1, trueExpr)
+            .write(ref2 to idx2, val2, trueExpr)
+
+
+        val keyConverter = UInputToInputKeyConverter(ref1 to mkBv(0), ref1 to mkBv(0), mkBv(5))
+        var inputRegion2 = emptyInputArrayRegion(mockk<Type>(), addressSort)
+
+        val idx = mkRegisterReading(4, sizeSort)
+        val reading1 = inputRegion2.read(ref2 to idx)
+
+        inputRegion2 = inputRegion2
+            .copyRange(inputRegion1, ref1 to mkBv(0), ref1 to mkBv(5), keyConverter, trueExpr)
+
+        val reading2 = inputRegion2.read(ref2 to idx)
+
+        val expr = (reading1 neq reading2) and (ref1 neq ref2)
+        val translated = translator.translate(expr)
+
+        val solver = KZ3Solver(this)
+        solver.assert(translated)
+        val status = solver.check()
+
+        assertSame(KSolverStatus.UNSAT, status)
+    }
+
+    @Test
+    fun testTranslateAllocatedToAllocatedArrayCopyAddressSort() = with(ctx) {
+        val idx1 = mkRegisterReading(1, sizeSort)
+        val val1 = mkConcreteHeapRef(1)
+
+        val idx2 = mkRegisterReading(3, sizeSort)
+        val val2 = mkRegisterReading(5, addressSort)
+
+        val allocatedRegion1 = emptyAllocatedArrayRegion(valueArrayDescr, 1, addressSort)
+            .write(idx1, val1, trueExpr)
+            .write(idx2, val2, trueExpr)
+
+        val keyConverter = UAllocatedToAllocatedKeyConverter(mkConcreteHeapRef(1) to mkBv(0), mkConcreteHeapRef(1) to mkBv(0), mkBv(5))
+        var allocatedRegion2 = emptyAllocatedArrayRegion(mockk<Type>(), 2, addressSort)
+
+        val idx = mkRegisterReading(4, sizeSort)
+        val readingBeforeCopy = allocatedRegion2.read(idx)
+
+        allocatedRegion2 = allocatedRegion2
+            .copyRange(allocatedRegion1, mkBv(0), mkBv(5), keyConverter, trueExpr)
+
+        val readingAfterCopy = allocatedRegion2.read(idx)
+
+        val outsideOfCopy = mkBvSignedLessExpr(idx, mkBv(0)) or mkBvSignedLessExpr(mkBv(5), idx)
+        val expr = (readingBeforeCopy neq readingAfterCopy) and outsideOfCopy
+        val translated = translator.translate(expr)
+
+        val solver = KZ3Solver(this)
+        solver.assert(translated)
+        val status = solver.check()
+
+        assertSame(KSolverStatus.UNSAT, status)
+    }
+
     @Test
     fun testCachingOfTranslatedMemoryUpdates() = with(ctx) {
         val allocatedRegion = emptyAllocatedArrayRegion(valueArrayDescr, 0, sizeSort)

usvm-jvm/src/samples/java/org/usvm/samples/arrays/OneDimensional.java

@@ -1,5 +1,7 @@
 package org.usvm.samples.arrays;
 
+import org.usvm.samples.objects.WrappedInt;
+
 public class OneDimensional {
     static int sumOf(int[] arr) {
         int sum = 0;
@@ -16,6 +18,18 @@ static int sumOf(int[] arr) {
         return sum;
     }
 
+    static int symbolicIndex(int a, WrappedInt b, int index) {
+        WrappedInt[] arr = new WrappedInt[]{new WrappedInt(1), new WrappedInt(2), b};
+        arr[0].setValue(a);
+        if (arr[index].getValue() == 5) {
+            if (index == 0) {
+                return -1;
+            }
+            return 0;
+        }
+        return 1;
+    }
+
     static int[] minus(int[] a, int[] b) {
         if (a != null && a.length == 0) {
             return null;

usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/TestOneDimensional.kt

@@ -2,9 +2,10 @@ package org.usvm.samples.arrays
 
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.test.util.checkers.eq
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 
-class TetOneDimensional : JavaMethodTestRunner() {
+class TestOneDimensional : JavaMethodTestRunner() {
     @Test
     fun `Test sumOf`() {
         checkDiscoveredPropertiesWithExceptions(
@@ -16,6 +17,20 @@ class TetOneDimensional : JavaMethodTestRunner() {
         )
     }
 
+    @Test
+    fun `Test symbolicIndex`() {
+        checkDiscoveredPropertiesWithExceptions(
+            OneDimensional::symbolicIndex,
+            eq(5),
+            { _, _, index, r -> index !in 0..2 && r.exceptionOrNull() is IndexOutOfBoundsException },
+            { _, b, index, r -> b == null && index == 2 && r.exceptionOrNull() is NullPointerException },
+            { a, _, index, r -> a == 5 && index == 0 && r.getOrNull() == -1 },
+            { _, b, index, r -> b.value == 5 && index == 2 && r.getOrNull() == 0 },
+            { _, _, _, r -> r.getOrNull() == 1 },
+        )
+    }
+
+
     @Test
     fun `Test minus`() {
         checkDiscoveredPropertiesWithExceptions(