Add optimization to applyTo

UnitTestBot · Aug 31, 2023 · 0632cdc · 0632cdc
1 parent 50d4a45
commit 0632cdc
Show file tree

Hide file tree

Showing 14 changed files with 92 additions and 465 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt
@@ -105,4 +105,5 @@ open class UComposer<Type>(
     override fun transform(expr: UNullRef): UExpr<UAddressSort> = memory.nullRef()
 }
 
-fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr
+@Suppress("NOTHING_TO_INLINE")
+inline fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt
@@ -73,6 +73,7 @@ abstract class USymbolicArrayCopyAdapter<SrcKey, DstKey>(
         srcCollectionId: USymbolicCollectionId<SrcKey, *, *>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,
         guard: UBoolExpr,
+        srcKey: SrcKey,
         composer: UComposer<*>
     )
 
@@ -127,6 +128,7 @@ class USymbolicArrayAllocatedToAllocatedCopyAdapter(
         srcCollectionId: USymbolicCollectionId<USizeExpr, *, *>,
         dstCollectionId: USymbolicCollectionId<USizeExpr, *, *>,
         guard: UBoolExpr,
+        srcKey: USizeExpr,
         composer: UComposer<*>
     ) = with(ctx) {
         check(dstCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $dstCollectionId" }
@@ -163,6 +165,7 @@ class USymbolicArrayAllocatedToInputCopyAdapter(
         srcCollectionId: USymbolicCollectionId<USizeExpr, *, *>,
         dstCollectionId: USymbolicCollectionId<USymbolicArrayIndex, *, *>,
         guard: UBoolExpr,
+        srcKey: USizeExpr,
         composer: UComposer<*>
     ) = with(ctx) {
         check(dstCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -199,6 +202,7 @@ class USymbolicArrayInputToAllocatedCopyAdapter(
         srcCollectionId: USymbolicCollectionId<USymbolicArrayIndex, *, *>,
         dstCollectionId: USymbolicCollectionId<USizeExpr, *, *>,
         guard: UBoolExpr,
+        srcKey: USymbolicArrayIndex,
         composer: UComposer<*>
     ) = with(ctx) {
         check(dstCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $dstCollectionId" }
@@ -236,6 +240,7 @@ class USymbolicArrayInputToInputCopyAdapter(
         srcCollectionId: USymbolicCollectionId<USymbolicArrayIndex, *, *>,
         dstCollectionId: USymbolicCollectionId<USymbolicArrayIndex, *, *>,
         guard: UBoolExpr,
+        srcKey: USymbolicArrayIndex,
         composer: UComposer<*>
     ) = with(ctx) {
         check(dstCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $dstCollectionId" }

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt
@@ -55,7 +55,7 @@ class UAllocatedArrayId<ArrayType, Sort : USort> internal constructor(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UArrayIndexLValue(sort, key.uctx.mkConcreteHeapRef(address), key, arrayType))
     }
 
@@ -134,7 +134,7 @@ class UInputArrayId<ArrayType, Sort : USort> internal constructor(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UArrayIndexLValue(sort, key.first, key.second, arrayType))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt
@@ -37,7 +37,7 @@ class UInputArrayLengthId<ArrayType> internal constructor(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UArrayLengthLValue(key, arrayType))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt
@@ -38,7 +38,7 @@ class UInputFieldId<Field, Sort : USort> internal constructor(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UFieldLValue(sort, key, field))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt
@@ -1,6 +1,5 @@
 package org.usvm.collection.map
 
-import io.ksmt.utils.uncheckedCast
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UComposer
@@ -40,14 +39,16 @@ abstract class USymbolicMapMergeAdapter<SrcKey, DstKey>(
     override fun toString(collection: USymbolicCollection<*, SrcKey, *>): String =
         "(merge $collection)"
 
+
     override fun <Type> applyTo(
         memory: UWritableMemory<Type>,
         srcCollectionId: USymbolicCollectionId<SrcKey, *, *>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,
         guard: UBoolExpr,
+        srcKey: SrcKey,
         composer: UComposer<*>
     ) {
-        setOfKeys.applyTo(memory, composer)
+        setOfKeys.applyTo(memory, srcKey,  composer)
         TODO()
     }
 
@@ -56,18 +57,6 @@ abstract class USymbolicMapMergeAdapter<SrcKey, DstKey>(
 
     private fun <Reg : Region<Reg>> convertRegion(srcReg: Reg): Reg =
         srcReg // TODO: implement valid region conversion logic
-
-    companion object {
-        private inline fun <KeySort : USort, Key, T> mapKeyType(
-            key: Key,
-            concrete: (UExpr<KeySort>) -> T,
-            symbolic: (USymbolicMapKey<KeySort>) -> T
-        ): T = when (key) {
-            is UExpr<*> -> concrete(key.uncheckedCast())
-            is Pair<*, *> -> symbolic(key.uncheckedCast())
-            else -> error("Unexpected key: $key")
-        }
-    }
 }
 
 class USymbolicMapAllocatedToAllocatedMergeAdapter<KeySort : USort>(

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt
@@ -34,7 +34,7 @@ class UInputMapLengthId<MapType> internal constructor(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UMapLengthLValue(key, mapType))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt
@@ -69,7 +69,7 @@ class UAllocatedMapId<MapType, KeySort : USort, ValueSort : USort, Reg : Region<
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UMapEntryLValue(keySort, sort, key.uctx.mkConcreteHeapRef(address), key, mapType, keyInfo))
     }
 
@@ -139,7 +139,7 @@ class UInputMapId<MapType, KeySort : USort, ValueSort : USort, Reg : Region<Reg>
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(UMapEntryLValue(keySort, sort, key.first, key.second, mapType, keyInfo))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt
@@ -63,7 +63,7 @@ class UAllocatedRefMapWithInputKeysId<MapType, ValueSort : USort>(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(URefMapEntryLValue(sort, key.uctx.mkConcreteHeapRef(mapAddress), key, mapType))
     }
 
@@ -130,7 +130,7 @@ class UInputRefMapWithAllocatedKeysId<MapType, ValueSort : USort>(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(URefMapEntryLValue(sort, key, key.uctx.mkConcreteHeapRef(keyAddress), mapType))
     }
 
@@ -191,7 +191,7 @@ class UInputRefMapWithInputKeysId<MapType, ValueSort : USort>(
         }
 
         val memory = composer.memory.toWritableMemory()
-        collection.applyTo(memory, composer)
+        collection.applyTo(memory, key, composer)
         return memory.read(URefMapEntryLValue(sort, key.first, key.second, mapType))
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
@@ -7,7 +7,6 @@ import org.usvm.UComposer
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
-import org.usvm.compose
 import org.usvm.isFalse
 import org.usvm.isTrue
 import org.usvm.uctx
@@ -148,12 +147,12 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
         }
     }
 
-    fun <Type> applyTo(memory: UWritableMemory<Type>, composer: UComposer<*>) {
+    fun <Type> applyTo(memory: UWritableMemory<Type>, key: Key, composer: UComposer<*>) {
         // Apply each update on the copy
         for (update in updates) {
             val guard = composer.compose(update.guard)
 
-            if (guard.isFalse) {
+            if (guard.isFalse || update.includesSymbolically(key, composer).isFalse) {
                 continue
             }
 
@@ -165,7 +164,9 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
                     guard
                 )
 
-                is URangedUpdateNode<*, *, Key, Sort> -> update.applyTo(memory, collectionId, composer)
+                is URangedUpdateNode<*, *, Key, Sort> -> {
+                    update.applyTo(memory, collectionId, key, composer)
+                }
             }
         }
     }

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt
@@ -32,6 +32,7 @@ interface USymbolicCollectionAdapter<SrcKey, DstKey> {
         srcCollectionId: USymbolicCollectionId<SrcKey, *, *>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,
         guard: UBoolExpr,
+        srcKey: SrcKey,
         composer: UComposer<*>
     )
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
@@ -216,10 +216,19 @@ class URangedUpdateNode<CollectionId : USymbolicCollectionId<SrcKey, Sort, Colle
     fun applyTo(
         memory: UWritableMemory<*>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,
+        key: DstKey,
         composer: UComposer<*>,
     ) {
-        sourceCollection.applyTo(memory, composer)
-        adapter.applyTo(memory, sourceCollection.collectionId, dstCollectionId, composer.compose(guard), composer)
+        val convertedKey = adapter.convert(key, composer)
+        sourceCollection.applyTo(memory, convertedKey, composer)
+        adapter.applyTo(
+            memory,
+            sourceCollection.collectionId,
+            dstCollectionId,
+            composer.compose(guard),
+            convertedKey,
+            composer
+        )
     }
 
     override fun toString(): String =

diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
@@ -10,31 +10,34 @@ import io.ksmt.sort.KBv32Sort
 import io.mockk.every
 import io.mockk.mockk
 import io.mockk.spyk
+import io.mockk.verify
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.assertThrows
 import org.usvm.api.writeArrayIndex
 import org.usvm.api.writeArrayLength
 import org.usvm.api.writeField
+import org.usvm.collection.array.UAllocatedArrayId
+import org.usvm.collection.array.UAllocatedArrayReading
+import org.usvm.collection.array.UInputArrayId
+import org.usvm.collection.array.UInputArrayReading
+import org.usvm.collection.array.USymbolicArrayIndex
+import org.usvm.collection.array.USymbolicArrayIndexKeyInfo
+import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter
+import org.usvm.collection.array.length.UInputArrayLengthId
+import org.usvm.collection.field.UFieldLValue
+import org.usvm.collection.field.UInputFieldId
 import org.usvm.constraints.UTypeEvaluator
+import org.usvm.memory.UFlatUpdates
 import org.usvm.memory.UMemory
 import org.usvm.memory.UPinpointUpdateNode
 import org.usvm.memory.URangedUpdateNode
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.UReadOnlyRegistersStack
-import org.usvm.memory.UUpdateNode
-import org.usvm.memory.UFlatUpdates
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionUpdates
-import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter
-import org.usvm.collection.array.UAllocatedArrayId
-import org.usvm.collection.array.UAllocatedArrayReading
-import org.usvm.collection.array.UInputArrayId
-import org.usvm.collection.array.UInputArrayReading
-import org.usvm.collection.array.length.UInputArrayLengthId
-import org.usvm.collection.field.UInputFieldId
-import org.usvm.collection.array.USymbolicArrayIndex
-import org.usvm.collection.array.USymbolicArrayIndexKeyInfo
+import org.usvm.memory.UUpdateNode
+import org.usvm.memory.UWritableMemory
 import org.usvm.model.UModelBase
 import org.usvm.model.URegistersStackEagerModel
 import org.usvm.util.SetRegion
@@ -620,4 +623,45 @@ internal class CompositionTest {
         val expr = composer.compose(reading)
         assertSame(concreteNull, expr)
     }
+
+    @Test
+    fun testUpdatesSimplification() = with(ctx) {
+        val composedMemory: UReadOnlyMemory<Type> = mockk()
+
+        val field = mockk<Field>()
+
+        val ref0 = mkRegisterReading(0, addressSort)
+        val ref1 = mkRegisterReading(1, addressSort)
+        val ref2 = mkRegisterReading(2, addressSort)
+
+        val region = UInputFieldId(field, bv32Sort)
+            .emptyRegion()
+            .write(ref0, mkBv(0), trueExpr)
+            .write(ref1, mkBv(1), trueExpr)
+
+        val reading = region.read(ref2)
+
+        val composer = spyk(UComposer(this, composedMemory))
+
+        val writableMemory: UWritableMemory<Type> = mockk()
+
+        every { composer.transform(ref0) } returns mkConcreteHeapRef(-1)
+        every { composer.transform(ref1) } returns ref1
+        every { composer.transform(ref2) } returns ref2
+
+        every { composedMemory.toWritableMemory() } returns writableMemory
+
+        every {
+            val lvalue = UFieldLValue(bv32Sort, ref1, field)
+            writableMemory.write(lvalue, mkBv(1), trueExpr)
+        } returns Unit
+        every {
+            val lvalue = UFieldLValue(bv32Sort, ref2, field)
+            writableMemory.read(lvalue)
+        } returns mkBv(42)
+
+        val composedReading = composer.compose(reading)
+        assertEquals(mkBv(42), composedReading)
+        verify(exactly = 1) { writableMemory.write(any<UFieldLValue<Field, UBv32Sort>>(), any(), any())}
+    }
 }