Memory composition support

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

@@ -1,7 +1,5 @@
 package org.usvm
 
-import org.ksmt.utils.asExpr
-
 @Suppress("MemberVisibilityCanBePrivate")
 open class UComposer<Field, Type>(
     ctx: UContext,
@@ -34,41 +32,33 @@ open class UComposer<Field, Type>(
         typeEvaluator.evalIs(composedAddress, type)
     }
 
-    override fun transform(expr: UArrayLength<Type>): USizeExpr = with(expr) {
-        val composedAddress = compose(address)
-        heapEvaluator.readArrayLength(composedAddress, region.regionId.arrayType)
-    }
-
-    override fun <Sort : USort> transform(
-        expr: UInputArrayReading<Type, Sort>
+    fun <RegionId : URegionId<Key>, Key, Sort : USort> transformHeapReading(
+        expr: UHeapReading<RegionId, Key, Sort>,
+        key: Key
     ): UExpr<Sort> = with(expr) {
-        val composedAddress = compose(address)
-        val composedIndex = compose(index)
-        // TODO compose the region
+        val instantiator = { key: Key, memoryRegion: UMemoryRegion<RegionId, Key, Sort> ->
+            // Create a copy of this heap to avoid its modification
+            val heapToApplyUpdates = heapEvaluator.toMutableHeap()
+            memoryRegion.applyTo(heapToApplyUpdates)
+            region.regionId.read(key, sort, heapToApplyUpdates)
+        }
 
-        heapEvaluator.readArrayIndex(
-            composedAddress,
-            composedIndex,
-            region.regionId.arrayType,
-            sort
-        ).asExpr(sort)
+        val mappedRegion = region.map(this@UComposer, instantiator)
+        val mappedKey = region.regionId.keyMapper(this@UComposer)(key)
+        mappedRegion.read(mappedKey)
     }
 
-    override fun <Sort : USort> transform(
-        expr: UAllocatedArrayReading<Type, Sort>
-    ): UExpr<Sort> = with(expr) {
-        val composedIndex = compose(index)
-        // TODO compose the region
-        val heapRef = uctx.mkConcreteHeapRef(region.regionId.address)
+    override fun transform(expr: UArrayLength<Type>): USizeExpr =
+        transformHeapReading(expr, expr.address)
 
-        heapEvaluator.readArrayIndex(heapRef, composedIndex, region.regionId.arrayType, sort).asExpr(sort)
-    }
+    override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort> =
+        transformHeapReading(expr, expr.address to expr.index)
 
-    override fun <Sort : USort> transform(expr: UFieldReading<Field, Sort>): UExpr<Sort> = with(expr) {
-        val composedAddress = compose(address)
-        // TODO compose the region
-        heapEvaluator.readField(composedAddress, region.regionId.field, sort).asExpr(sort)
-    }
+    override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort> =
+        transformHeapReading(expr, expr.index)
 
     override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> = expr
+
+    override fun <Sort : USort> transform(expr: UFieldReading<Field, Sort>): UExpr<Sort> =
+        transformHeapReading(expr, expr.address)
 }

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

@@ -8,9 +8,9 @@ import org.ksmt.utils.cast
 
 @Suppress("LeakingThis")
 open class UContext(
-    private val operationMode: OperationMode = OperationMode.CONCURRENT, // TODO replace it when we have KSMT 0.3.3 version
-    private val astManagementMode: AstManagementMode = AstManagementMode.GC, // TODO replace it when we have KSMT 0.3.3 version
-    private val simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY
+    operationMode: OperationMode = OperationMode.CONCURRENT,
+    astManagementMode: AstManagementMode = AstManagementMode.GC,
+    simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY
 ) : KContext(operationMode, astManagementMode, simplificationMode) {
 
     val addressSort: UAddressSort = mkUninterpretedSort("Address")
@@ -31,7 +31,7 @@ open class UContext(
 
     private val inputFieldReadingCache = mkAstInterner<UFieldReading<*, out USort>>()
 
-    fun <Field, Sort : USort> mkFieldReading(
+    fun <Field, Sort : USort> mkInputFieldReading(
         region: UInputFieldMemoryRegion<Field, Sort>,
         address: UHeapRef,
     ): UFieldReading<Field, Sort> = inputFieldReadingCache.createIfContextActive {
@@ -57,12 +57,12 @@ open class UContext(
         UInputArrayReading(this, region, address, index)
     }.cast()
 
-    private val arrayLengthCache = mkAstInterner<UArrayLength<*>>()
+    private val inputArrayLengthCache = mkAstInterner<UArrayLength<*>>()
 
-    fun <ArrayType> mkArrayLength(
+    fun <ArrayType> mkInputArrayLength(
         region: UInputArrayLengthMemoryRegion<ArrayType>,
         address: UHeapRef,
-    ): UArrayLength<ArrayType> = arrayLengthCache.createIfContextActive {
+    ): UArrayLength<ArrayType> = inputArrayLengthCache.createIfContextActive {
         UArrayLength(this, region, address)
     }.cast()
 

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

@@ -49,7 +49,7 @@ class UConcreteHeapRef internal constructor(ctx: UContext, val address: UConcret
     }
 
     override fun print(printer: ExpressionPrinter) {
-        TODO("Not yet implemented")
+        printer.append("(concreteAddr $address)")
     }
 
     val isNull = (address == nullAddress)
@@ -85,7 +85,6 @@ class UArrayIndexRef<ArrayType>(
 abstract class USymbol<Sort : USort>(ctx: UContext) : UExpr<Sort>(ctx) {
 }
 
-@Suppress("UNUSED_PARAMETER")
 class URegisterReading<Sort : USort> internal constructor(
     ctx: UContext,
     val idx: Int,
@@ -105,7 +104,7 @@ class URegisterReading<Sort : USort> internal constructor(
     override fun internHashCode(): Int = hash(idx, sort)
 }
 
-abstract class UHeapReading<RegionId, Key, Sort : USort>(
+abstract class UHeapReading<RegionId : URegionId<Key>, Key, Sort : USort>(
     ctx: UContext,
     val region: UMemoryRegion<RegionId, Key, Sort>
 ) : USymbol<Sort>(ctx) {
@@ -128,7 +127,7 @@ class UFieldReading<Field, Sort : USort> internal constructor(
         return (transformer as UExprTransformer<Field, *>).transform(this)
     }
 
-    override fun toString(): String = "$address.${region.regionId.field}"
+    override fun toString(): String = "$address.${region.field}"
 
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { region }, { address })
 
@@ -156,7 +155,7 @@ class UAllocatedArrayReading<ArrayType, Sort : USort> internal constructor(
 
     override fun internHashCode(): Int = hash(region, index)
 
-    override fun toString(): String = "0x${region.regionId.address}[$index]"
+    override fun toString(): String = "0x${region.allocatedAddress}[$index]"
 }
 
 class UInputArrayReading<ArrayType, Sort : USort> internal constructor(
@@ -260,3 +259,10 @@ class UIsExpr<Type> internal constructor(
     override fun internHashCode(): Int = hash(ref, type)
 }
 //endregion
+
+//region Utils
+
+val UBoolExpr.isFalse get() = this === ctx.falseExpr
+val UBoolExpr.isTrue get() = !isFalse
+
+//endregion