Simplify composition (#53)

---------

Co-authored-by: Valentyn Sobol <[email protected]>

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

@@ -11,7 +11,6 @@ import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading
 import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
 import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
 import org.usvm.memory.UReadOnlyMemory
-import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
 import org.usvm.util.Region
 
@@ -62,18 +61,8 @@ open class UComposer<Type>(
         expr: UCollectionReading<CollectionId, Key, Sort>,
         key: Key,
     ): UExpr<Sort> = with(expr) {
-        val mappedCollectionId = collection.collectionId.map(this@UComposer)
-        val mappedKey = mappedCollectionId.keyMapper(this@UComposer)(key)
-        val decomposedKey = mappedCollectionId.rebindKey(mappedKey)
-        if (decomposedKey != null) {
-            @Suppress("UNCHECKED_CAST")
-            // I'm terribly sorry to do this cast, but it's impossible to do it type safe way :(
-            val mappedCollection =
-                collection.mapTo(this@UComposer, decomposedKey.collectionId) as USymbolicCollection<*, Any?, Sort>
-            return mappedCollection.read(decomposedKey.key)
-        }
-        val mappedCollection = collection.mapTo(this@UComposer, mappedCollectionId)
-        return mappedCollection.read(mappedKey)
+        val mappedKey = collection.collectionId.keyMapper(this@UComposer)(key)
+        return collection.read(mappedKey, this@UComposer)
     }
 
     override fun transform(expr: UInputArrayLengthReading<Type>): USizeExpr =
@@ -115,3 +104,6 @@ open class UComposer<Type>(
 
     override fun transform(expr: UNullRef): UExpr<UAddressSort> = memory.nullRef()
 }
+
+@Suppress("NOTHING_TO_INLINE")
+inline fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr

usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt

@@ -8,12 +8,12 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USizeExpr
 import org.usvm.USort
-import org.usvm.memory.key.USizeExprKeyInfo
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.foldHeapRef
+import org.usvm.memory.key.USizeExprKeyInfo
 import org.usvm.memory.map
 
 data class UArrayIndexLValue<ArrayType, Sort : USort>(
@@ -70,8 +70,14 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort>(
         arrayType: ArrayType,
         sort: Sort,
         address: UConcreteHeapAddress
-    ): UAllocatedArray<ArrayType, Sort> = allocatedArrays[address]
-        ?: UAllocatedArrayId(arrayType, sort, address).emptyRegion()
+    ): UAllocatedArray<ArrayType, Sort> {
+        var collection = allocatedArrays[address]
+        if (collection == null) {
+            collection = UAllocatedArrayId(arrayType, sort, address).emptyRegion()
+            allocatedArrays = allocatedArrays.put(address, collection)
+        }
+        return collection
+    }
 
     private fun updateAllocatedArray(ref: UConcreteHeapAddress, updated: UAllocatedArray<ArrayType, Sort>) =
         UArrayMemoryRegion(allocatedArrays.put(ref, updated), inputArray)

usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt

@@ -35,7 +35,7 @@ class UArrayRegionDecoder<ArrayType, Sort : USort>(
     private val allocatedRegions =
         mutableMapOf<UConcreteHeapAddress, UAllocatedArrayRegionTranslator<ArrayType, Sort>>()
 
-    private var inputRegion: UInputArrayRegionTranslator<ArrayType, Sort>? = null
+    private var inputRegionTranslator: UInputArrayRegionTranslator<ArrayType, Sort>? = null
 
     fun allocatedArrayRegionTranslator(
         collectionId: UAllocatedArrayId<ArrayType, Sort>
@@ -51,19 +51,19 @@ class UArrayRegionDecoder<ArrayType, Sort : USort>(
     fun inputArrayRegionTranslator(
         collectionId: UInputArrayId<ArrayType, Sort>
     ): URegionTranslator<UInputArrayId<ArrayType, Sort>, USymbolicArrayIndex, Sort> {
-        if (inputRegion == null) {
+        if (inputRegionTranslator == null) {
             check(collectionId.arrayType == regionId.arrayType && collectionId.sort == regionId.sort) {
                 "Unexpected collection: $collectionId"
             }
-            inputRegion = UInputArrayRegionTranslator(collectionId, exprTranslator)
+            inputRegionTranslator = UInputArrayRegionTranslator(collectionId, exprTranslator)
         }
-        return inputRegion!!
+        return inputRegionTranslator!!
     }
 
     override fun decodeLazyRegion(
         model: KModel,
         mapping: Map<UHeapRef, UConcreteHeapRef>
-    ) = UArrayLazyModelRegion(regionId, model, mapping, inputRegion)
+    ) = inputRegionTranslator?.let { UArrayLazyModelRegion(regionId, model, mapping, it) }
 }
 
 private class UAllocatedArrayRegionTranslator<ArrayType, Sort : USort>(
@@ -145,11 +145,13 @@ private class UAllocatedArrayUpdatesTranslator<Sort : USort>(
         val key = mkFreshConst("k", previous.sort.domain)
 
         val keyMapper = sourceCollection.collectionId.keyMapper(exprTranslator)
-        val convertedKey = keyMapper(adapter.convert(key))
+        val convertedKey = keyMapper(adapter.convert(key, composer = null))
 
-        val isInside = update.includesSymbolically(key).translated // already includes guard
+        val isInside = update.includesSymbolically(key, composer = null).translated // already includes guard
 
-        val result = sourceCollection.collectionId.instantiate(sourceCollection, convertedKey).translated
+        val result = sourceCollection.collectionId.instantiate(
+            sourceCollection, convertedKey, composer = null
+        ).translated
 
         val ite = mkIte(isInside, result, previous.select(key))
         return mkArrayLambda(key.decl, ite)
@@ -187,11 +189,13 @@ private class UInputArrayUpdatesTranslator<Sort : USort>(
         val key2 = mkFreshConst("k2", previous.sort.domain1)
 
         val keyMapper = sourceCollection.collectionId.keyMapper(exprTranslator)
-        val convertedKey = keyMapper(adapter.convert(key1 to key2))
+        val convertedKey = keyMapper(adapter.convert(key1 to key2, composer = null))
 
-        val isInside = update.includesSymbolically(key1 to key2).translated // already includes guard
+        val isInside = update.includesSymbolically(key1 to key2, composer = null).translated // already includes guard
 
-        val result = sourceCollection.collectionId.instantiate(sourceCollection, convertedKey).translated
+        val result = sourceCollection.collectionId.instantiate(
+            sourceCollection, convertedKey, composer = null
+        ).translated
 
         val ite = mkIte(isInside, result, previous.select(key1, key2))
         return mkArrayLambda(key1.decl, key2.decl, ite)

usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt

@@ -12,28 +12,26 @@ import org.usvm.solver.UCollectionDecoder
 abstract class UArrayModelRegion<ArrayType, Sort : USort>(
     private val regionId: UArrayRegionId<ArrayType, Sort>,
 ) : UReadOnlyMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> {
-    val defaultValue by lazy { regionId.sort.sampleUValue() }
-
-    abstract val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>?
+    abstract val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>
 
     override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> {
-        val ref = modelEnsureConcreteInputRef(key.ref) ?: return defaultValue
-        return inputArray?.read(ref to key.index) ?: defaultValue
+        val ref = modelEnsureConcreteInputRef(key.ref)
+        return inputArray.read(ref to key.index)
     }
 }
 
 class UArrayLazyModelRegion<ArrayType, Sort : USort>(
     regionId: UArrayRegionId<ArrayType, Sort>,
     private val model: KModel,
     private val addressesMapping: AddressesMapping,
-    private val inputArrayDecoder: UCollectionDecoder<USymbolicArrayIndex, Sort>?
+    private val inputArrayDecoder: UCollectionDecoder<USymbolicArrayIndex, Sort>
 ) : UArrayModelRegion<ArrayType, Sort>(regionId) {
-    override val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>? by lazy {
-        inputArrayDecoder?.decodeCollection(model, addressesMapping)
+    override val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort> by lazy {
+        inputArrayDecoder.decodeCollection(model, addressesMapping)
     }
 }
 
 class UArrayEagerModelRegion<ArrayType, Sort : USort>(
     regionId: UArrayRegionId<ArrayType, Sort>,
-    override val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>?
+    override val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>
 ) : UArrayModelRegion<ArrayType, Sort>(regionId)