initializeAllocatedSet in USetRegion (#316)

* tmp: USetMemoryRegion is now not internal

* implemented initializedSet

* initializeAllocatedSet

* fix

* import fix

* detekt fix

* Valentyn's fix in UComposer

* PR fix

Author: tochilinak

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

@@ -31,8 +31,8 @@ open class UComposer<Type, USizeSort : USort>(
     override fun <T : USort> transform(expr: UIteExpr<T>): UExpr<T> =
         transformExprAfterTransformed(expr, expr.condition) { condition ->
             when {
-                condition.isTrue -> apply(expr.trueBranch)
-                condition.isFalse -> apply(expr.falseBranch)
+                condition.isTrue -> transformExprAfterTransformed(expr, expr.trueBranch) { it }
+                condition.isFalse -> transformExprAfterTransformed(expr, expr.falseBranch) { it }
                 else -> super.transform(expr)
             }
         }

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

@@ -6,13 +6,13 @@ import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
-import org.usvm.collection.set.USymbolicSetEntries
 import org.usvm.collection.set.USymbolicSetElement
 import org.usvm.collection.set.USymbolicSetElementsCollector
+import org.usvm.collection.set.USymbolicSetEntries
 import org.usvm.collections.immutable.getOrPut
 import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
-import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -81,6 +81,16 @@ interface USetRegion<SetType, ElementSort : USort, Reg : Region<Reg>> :
         operationGuard: UBoolExpr,
         ownership: MutabilityOwnership,
     ): USetRegion<SetType, ElementSort, Reg>
+
+    fun initializeAllocatedSet(
+        address: UConcreteHeapAddress,
+        setType: SetType,
+        sort: ElementSort,
+        content: Set<UExpr<ElementSort>>,
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
+        makeDisjointCheck: Boolean = true,
+    ): USetRegion<SetType, ElementSort, Reg>
 }
 
 internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>(
@@ -203,6 +213,26 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         },
     )
 
+    override fun initializeAllocatedSet(
+        address: UConcreteHeapAddress,
+        setType: SetType,
+        sort: ElementSort,
+        content: Set<UExpr<ElementSort>>,
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
+        makeDisjointCheck: Boolean,
+    ): USetRegion<SetType, ElementSort, Reg> {
+        val setId = UAllocatedSetId(address, elementSort, setType, elementInfo)
+        val newCollection = setId.initializedSet(content, operationGuard, makeDisjointCheck)
+        return USetMemoryRegion(
+            setType,
+            elementSort,
+            elementInfo,
+            allocatedSets.put(setId, newCollection, ownership),
+            inputSet
+        )
+    }
+
     override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries<SetType, ElementSort, Reg> =
         foldHeapRefWithStaticAsSymbolic(
             ref = ref,

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

@@ -2,6 +2,7 @@ package org.usvm.collection.set.primitive
 
 import io.ksmt.cache.hash
 import io.ksmt.utils.uncheckedCast
+import kotlinx.collections.immutable.toPersistentMap
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UComposer
@@ -13,12 +14,15 @@ import org.usvm.collection.set.USymbolicSetElement
 import org.usvm.collection.set.USymbolicSetElementRegion
 import org.usvm.collection.set.USymbolicSetKeyInfo
 import org.usvm.memory.ULValue
+import org.usvm.memory.UPinpointUpdateNode
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
 import org.usvm.memory.USymbolicCollectionKeyInfo
 import org.usvm.memory.UTreeUpdates
+import org.usvm.memory.UUpdateNode
 import org.usvm.memory.UWritableMemory
 import org.usvm.regions.Region
+import org.usvm.regions.RegionTree
 import org.usvm.regions.emptyRegionTree
 import org.usvm.uctx
 import java.util.IdentityHashMap
@@ -115,6 +119,40 @@ class UAllocatedSetId<SetType, ElementSort : USort, Reg : Region<Reg>>(
     }
 
     override fun hashCode(): Int = hash(setAddress, setType, elementSort)
+
+    fun initializedSet(
+        content: Set<UExpr<ElementSort>>,
+        guard: UBoolExpr,
+        makeDisjointCheck: Boolean = false, // for debug purposes
+    ): USymbolicCollection<UAllocatedSetId<SetType, ElementSort, Reg>, UExpr<ElementSort>, UBoolSort> {
+        val ctx = guard.ctx
+        var unionRegion = elementInfo.bottomRegion()
+        val entries = content.map { value ->
+            val update = UPinpointUpdateNode(value, elementInfo, ctx.trueExpr, guard)
+
+            val region = elementInfo.keyToRegion(value)
+
+            if (makeDisjointCheck) {
+                check(unionRegion.compare(region) == Region.ComparisonResult.DISJOINT) {
+                    "Cannot create initializedSet if regions of given elements intersect"
+                }
+                unionRegion = unionRegion.union(region)
+            }
+
+            region to update
+        }
+
+        val map = entries.associate {
+            it.first to (it.second to emptyRegionTree<Reg, UUpdateNode<UExpr<ElementSort>, UBoolSort>>())
+        }.toPersistentMap()
+
+        val updates = UTreeUpdates(
+            updates = RegionTree(map),
+            keyInfo()
+        )
+
+        return USymbolicCollection(this, updates)
+    }
 }
 
 class UInputSetId<SetType, ElementSort : USort, Reg : Region<Reg>>(