add ownership in composer

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

@@ -15,14 +15,16 @@ import org.usvm.collection.set.primitive.UInputSetReading
 import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.USymbolicCollectionId
 import org.usvm.regions.Region
 
 @Suppress("MemberVisibilityCanBePrivate")
 open class UComposer<Type, USizeSort : USort>(
     ctx: UContext<USizeSort>,
-    val memory: UReadOnlyMemory<Type>
+    val memory: UReadOnlyMemory<Type>,
+    val ownership: MutabilityOwnership
 ) : UExprTransformer<Type, USizeSort>(ctx) {
     open fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort> = apply(expr)
 

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

@@ -62,9 +62,9 @@ open class UContext<USizeSort : USort>(
     private val solver by lazy { components.mkSolver(this) }
     private val typeSystem by lazy { components.mkTypeSystem(this) }
     private val softConstraintsProvider by lazy { components.mkSoftConstraintsProvider(this) }
-    private val composerBuilder: (UReadOnlyMemory<*>) -> UComposer<*, USizeSort> by lazy {
+    private val composerBuilder: (UReadOnlyMemory<*>, MutabilityOwnership) -> UComposer<*, USizeSort> by lazy {
         @Suppress("UNCHECKED_CAST")
-        components.mkComposer(this) as (UReadOnlyMemory<*>) -> UComposer<*, USizeSort>
+        components.mkComposer(this) as (UReadOnlyMemory<*>, MutabilityOwnership) -> UComposer<*, USizeSort>
     }
 
     val defaultOwnership = MutabilityOwnership()
@@ -88,7 +88,8 @@ open class UContext<USizeSort : USort>(
 
     fun <Type> softConstraintsProvider(): USoftConstraintsProvider<Type, USizeSort> = softConstraintsProvider.cast()
 
-    fun <Type> composer(memory: UReadOnlyMemory<Type>): UComposer<Type, USizeSort> = composerBuilder(memory).cast()
+    fun <Type> composer(memory: UReadOnlyMemory<Type>, ownership: MutabilityOwnership): UComposer<Type, USizeSort> =
+        composerBuilder(memory, ownership).cast()
 
     val addressSort: UAddressSort = mkUninterpretedSort("Address")
     val nullRef: UNullRef = UNullRef(this)

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

@@ -1,5 +1,6 @@
 package org.usvm
 
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.model.ULazyModelDecoder
 import org.usvm.model.UModelDecoder
@@ -34,8 +35,8 @@ interface UComponents<Type, USizeSort : USort> {
 
     fun <Context : UContext<USizeSort>> mkComposer(
         ctx: Context,
-    ): (UReadOnlyMemory<Type>) -> UComposer<Type, USizeSort> =
-        { memory: UReadOnlyMemory<Type> -> UComposer(ctx, memory) }
+    ): (UReadOnlyMemory<Type>, MutabilityOwnership) -> UComposer<Type, USizeSort> =
+        { memory: UReadOnlyMemory<Type>, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) }
 
     fun mkStatesForkProvider(): StateForker = if (useSolverForForks) WithSolverStateForker else NoSolverStateForker
 

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

@@ -52,7 +52,7 @@ class UAllocatedArrayId<ArrayType, Sort : USort, USizeSort : USort> internal con
             return key.uctx.withSizeSort<USizeSort>().mkAllocatedArrayReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -129,7 +129,7 @@ class UInputArrayId<ArrayType, Sort : USort, USizeSort : USort> internal constru
             return sort.uctx.withSizeSort<USizeSort>().mkInputArrayReading(collection, key.first, key.second)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

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

@@ -35,7 +35,7 @@ class UInputArrayLengthId<ArrayType, USizeSort : USort> internal constructor(
             return key.uctx.withSizeSort<USizeSort>().mkInputArrayLengthReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt

@@ -35,7 +35,7 @@ class UInputFieldId<Field, Sort : USort> internal constructor(
             return key.uctx.mkInputFieldReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt

@@ -32,7 +32,7 @@ class UInputMapLengthId<MapType, USizeSort : USort> internal constructor(
             return sort.uctx.withSizeSort<USizeSort>().mkInputMapLengthReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt

@@ -66,7 +66,7 @@ class UAllocatedMapId<MapType, KeySort : USort, ValueSort : USort, Reg : Region<
             return key.uctx.mkAllocatedMapReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -133,7 +133,7 @@ class UInputMapId<MapType, KeySort : USort, ValueSort : USort, Reg : Region<Reg>
             return sort.uctx.mkInputMapReading(collection, key.first, key.second)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt

@@ -61,7 +61,7 @@ class UAllocatedRefMapWithInputKeysId<MapType, ValueSort : USort>(
             return key.uctx.mkAllocatedRefMapWithInputKeysReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -126,7 +126,7 @@ class UInputRefMapWithAllocatedKeysId<MapType, ValueSort : USort>(
             return key.uctx.mkInputRefMapWithAllocatedKeysReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -185,7 +185,7 @@ class UInputRefMapWithInputKeysId<MapType, ValueSort : USort>(
             return sort.uctx.mkInputRefMapWithInputKeysReading(collection, key.first, key.second)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt

@@ -57,7 +57,7 @@ class UAllocatedSetId<SetType, ElementSort : USort, Reg : Region<Reg>>(
             return sort.uctx.mkAllocatedSetReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -133,7 +133,7 @@ class UInputSetId<SetType, ElementSort : USort, Reg : Region<Reg>>(
             return sort.uctx.mkInputSetReading(collection, key.first, key.second)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetId.kt

@@ -54,7 +54,7 @@ class UAllocatedRefSetWithInputElementsId<SetType>(
             return key.uctx.mkAllocatedRefSetWithInputElementsReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -128,7 +128,7 @@ class UInputRefSetWithAllocatedElementsId<SetType>(
             return key.uctx.mkInputRefSetWithAllocatedElementsReading(collection, key)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }
@@ -197,7 +197,7 @@ class UInputRefSetWithInputElementsId<SetType>(
             return sort.uctx.mkInputRefSetWithInputElementsReading(collection, key.first, key.second)
         }
 
-        val memory = composer.memory.toWritableMemory()
+        val memory = composer.memory.toWritableMemory(composer.ownership)
         collection.applyTo(memory, key, composer)
         return memory.read(mkLValue(key))
     }

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

@@ -79,7 +79,7 @@ interface UReadOnlyMemory<Type> {
 
     fun nullRef(): UHeapRef
 
-    fun toWritableMemory(): UWritableMemory<Type>
+    fun toWritableMemory(ownership: MutabilityOwnership): UWritableMemory<Type>
 }
 
 interface UWritableMemory<Type> : UReadOnlyMemory<Type> {
@@ -163,7 +163,7 @@ class UMemory<Type, Method>(
             ctx, cloneOwnership, typeConstraints, stack.clone(), mocks.clone(thisOwnership, cloneOwnership), regions
         ).also { ownership = thisOwnership }
 
-    override fun toWritableMemory() =
+    override fun toWritableMemory(ownership: MutabilityOwnership) =
     // To be perfectly rigorous, we should clone stack and types here.
         // But in fact they should not be used, so to optimize things up, we don't touch them.
         UMemory(ctx, ownership, types, stack, mocks, regions)

usvm-core/src/main/kotlin/org/usvm/model/Model.kt

@@ -41,7 +41,7 @@ open class UModelBase<Type>(
     override val ownership: MutabilityOwnership = ctx.defaultOwnership,
 ) : UModel, UWritableMemory<Type> {
     @Suppress("LeakingThis")
-    protected open val composer = ctx.composer(this)
+    protected open val composer = ctx.composer(this, ownership)
 
     /**
      * The evaluator supports only expressions with symbols inheriting [org.usvm.USymbol].
@@ -63,7 +63,7 @@ open class UModelBase<Type>(
 
     override fun nullRef(): UHeapRef = nullRef
 
-    override fun toWritableMemory(): UWritableMemory<Type> = this
+    override fun toWritableMemory(ownership: MutabilityOwnership): UWritableMemory<Type> = this
 
     override fun <Key, Sort : USort> setRegion(
         regionId: UMemoryRegionId<Key, Sort>,

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

@@ -67,7 +67,7 @@ internal class CompositionTest {
         ctx = UContext(components)
         ownership = MutabilityOwnership()
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
-        every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory<Type> -> UComposer(ctx, memory) } }
+        every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory<Type>, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) } }
 
         concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS)
         stackEvaluator = mockk()
@@ -79,7 +79,7 @@ internal class CompositionTest {
         every { memory.stack } returns stackEvaluator
         every { memory.mocker } returns mockEvaluator
 
-        composer = UComposer(ctx, memory)
+        composer = UComposer(ctx, memory, ownership)
     }
 
     @Test
@@ -263,7 +263,7 @@ internal class CompositionTest {
         heapToComposeWith.writeArrayLength(fstConcreteAddress, fstValueFromHeap, arrayType, sizeSort)
         heapToComposeWith.writeArrayLength(sndConcreteAddress, sndValueFromHeap, arrayType, sizeSort)
 
-        val composer = UComposer(ctx, heapToComposeWith)
+        val composer = UComposer(ctx, heapToComposeWith, MutabilityOwnership())
 
         every { fstAddress.accept(composer) } returns fstConcreteAddress
         every { sndAddress.accept(composer) } returns sndConcreteAddress
@@ -314,7 +314,7 @@ internal class CompositionTest {
         val answer = 43.toBv()
 
         // TODO replace with jacoDB type
-        val composer = UComposer(ctx, UMemory<KClass<*>, Any>(ctx, MutabilityOwnership(), mockk()))
+        val composer = UComposer(ctx, UMemory<KClass<*>, Any>(ctx, ownership, mockk()), MutabilityOwnership())
 
         every { fstAddress.accept(composer) } returns sndAddress
         every { fstIndex.accept(composer) } returns sndIndex
@@ -348,13 +348,13 @@ internal class CompositionTest {
         // create a heap with a record: (sndAddress, sndIndex) = 2
         sndMemory.writeArrayIndex(sndAddress, sndIndex, arrayType, mkBv32Sort(), 2.toBv(), mkTrue())
 
-        val sndComposer = UComposer(ctx, sndMemory)
+        val sndComposer = UComposer(ctx, sndMemory, MutabilityOwnership())
 
         val fstMemory = UMemory<KClass<*>, Any>(ctx, ownership, mockk(), mockk())
         // create a heap with a record: (fstAddress, fstIndex) = 1
         fstMemory.writeArrayIndex(fstAddress, fstIndex, arrayType, mkBv32Sort(), 1.toBv(), mkTrue())
 
-        val fstComposer = UComposer(ctx, fstMemory) // TODO replace with jacoDB type
+        val fstComposer = UComposer(ctx, fstMemory, MutabilityOwnership()) // TODO replace with jacoDB type
 
         // Both heaps leave everything untouched
         every { sndAddress.accept(sndComposer) } returns sndAddress
@@ -429,7 +429,7 @@ internal class CompositionTest {
             sndAddressForCompose, concreteIndex, arrayType, regionArray.sort, sndValue, guard = trueExpr
         )
 
-        val composer = UComposer(ctx, heapToComposeWith)
+        val composer = UComposer(ctx, heapToComposeWith, MutabilityOwnership())
 
         every { fstSymbolicIndex.accept(composer) } returns concreteIndex
         every { sndSymbolicIndex.accept(composer) } returns concreteIndex
@@ -463,7 +463,7 @@ internal class CompositionTest {
             ctx, mockk(), mockk(), mockk(), emptyMap(), concreteNullRef
         )
 
-        val composer = spyk(UComposer(ctx, heapToComposeWith))
+        val composer = spyk(UComposer(ctx, heapToComposeWith, MutabilityOwnership()))
 
         every { symbolicIndex.accept(composer) } returns mkBv(2)
         every { symbolicAddress.accept(composer) } returns mkConcreteHeapRef(-1)
@@ -512,7 +512,7 @@ internal class CompositionTest {
         val composeMemory = UMemory<Type, Any>(ctx, MutabilityOwnership(), mockk())
         composeMemory.writeField(aAddress, field, bv32Sort, 42.toBv(), guard = trueExpr)
 
-        val composer = UComposer(ctx, composeMemory)
+        val composer = UComposer(ctx, composeMemory, MutabilityOwnership())
 
         val composedExpression = composer.compose(expression)
 
@@ -527,7 +527,7 @@ internal class CompositionTest {
         )
         val model = UModelBase<Type>(ctx, stackModel, mockk(), mockk(), emptyMap(), concreteNull)
 
-        val composer = UComposer(this, model)
+        val composer = UComposer(this, model, MutabilityOwnership())
 
         val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), mkRegisterReading(1, addressSort))
 
@@ -543,7 +543,7 @@ internal class CompositionTest {
         every { composedMemory.nullRef() } returns concreteNull
         every { composedMemory.stack } returns stackModel
 
-        val composer = UComposer(this, composedMemory)
+        val composer = UComposer(this, composedMemory, MutabilityOwnership())
 
         val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), nullRef)
 
@@ -570,7 +570,7 @@ internal class CompositionTest {
         composeMemory.stack.writeRegister(2, composedSymbolicHeapRef)
         composeMemory.stack.writeRegister(3, mkRegisterReading(3, bv32Sort))
 
-        val composer = UComposer(ctx, composeMemory)
+        val composer = UComposer(ctx, composeMemory, MutabilityOwnership())
 
         val fromRegion0 = UInputArrayId<_, _, USizeSort>(arrayType, bv32Sort)
             .emptyRegion()
@@ -628,7 +628,7 @@ internal class CompositionTest {
         val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to mkBv(0), 1 to mkBv(0), 2 to mkBv(2)))
         every { composedMemory.stack } returns stackModel
 
-        val composer = UComposer(this, composedMemory)
+        val composer = UComposer(this, composedMemory, MutabilityOwnership())
 
         val region = UAllocatedArrayId<_, _, USizeSort>(mockk<Type>(), addressSort, 1).emptyRegion()
         val reading = region.read(mkRegisterReading(0, sizeSort))
@@ -654,15 +654,16 @@ internal class CompositionTest {
 
         val reading = region.read(ref2)
 
-        val composer = spyk(UComposer(this, composedMemory))
+        val composerOwnership = MutabilityOwnership()
+        val composer = spyk(UComposer(this, composedMemory, composerOwnership))
 
         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 { composedMemory.toWritableMemory(composerOwnership) } returns writableMemory
 
         every {
             val lvalue = UFieldLValue(bv32Sort, ref1, field)

usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt

@@ -52,7 +52,7 @@ abstract class SymbolicCollectionTestBase {
         ownership = MutabilityOwnership()
 
         every { components.mkComposer(ctx) } answers {
-            { memory: UReadOnlyMemory<SingleTypeSystem.SingleType> -> UComposer(ctx, memory) }
+            { memory: UReadOnlyMemory<SingleTypeSystem.SingleType>, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) }
         }
 
         val translator = UExprTranslator<SingleTypeSystem.SingleType, USizeSort>(ctx)