From ed0c6412c2069545f6614959b051f831a8ad739c Mon Sep 17 00:00:00 2001 From: tochilinak Date: Fri, 25 Jul 2025 15:05:48 +0300 Subject: [PATCH 1/8] tmp: USetMemoryRegion is now not internal --- .../main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt index 2268378f87..46803e8d81 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt @@ -83,7 +83,7 @@ interface USetRegion> : ): USetRegion } -internal class USetMemoryRegion>( +class USetMemoryRegion>( private val setType: SetType, private val elementSort: ElementSort, private val elementInfo: USymbolicCollectionKeyInfo, Reg>, From 264a4586988e9eeae283f1e507522861b69219ab Mon Sep 17 00:00:00 2001 From: tochilinak Date: Mon, 28 Jul 2025 14:40:27 +0300 Subject: [PATCH 2/8] implemented initializedSet --- .../collection/set/primitive/USetRegion.kt | 2 +- .../set/primitive/USymbolicSetId.kt | 39 +++++++++++++++++++ 2 files changed, 40 insertions(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt index 46803e8d81..2268378f87 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt @@ -83,7 +83,7 @@ interface USetRegion> : ): USetRegion } -class USetMemoryRegion>( +internal class USetMemoryRegion>( private val setType: SetType, private val elementSort: ElementSort, private val elementInfo: USymbolicCollectionKeyInfo, Reg>, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index bf1f0f50d8..839fa9f700 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -2,6 +2,8 @@ package org.usvm.collection.set.primitive import io.ksmt.cache.hash import io.ksmt.utils.uncheckedCast +import kotlinx.collections.immutable.persistentMapOf +import kotlinx.collections.immutable.toPersistentMap import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UComposer @@ -12,13 +14,17 @@ import org.usvm.collection.set.USetRegionBuilder import org.usvm.collection.set.USymbolicSetElement import org.usvm.collection.set.USymbolicSetElementRegion import org.usvm.collection.set.USymbolicSetKeyInfo +import org.usvm.collections.immutable.persistentHashMapOf 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 +121,37 @@ class UAllocatedSetId>( } override fun hashCode(): Int = hash(setAddress, setType, elementSort) + + fun initializedSet( + content: Set>, + guard: UBoolExpr + ): USymbolicCollection, UExpr, 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) + check(region.compare(unionRegion) == 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, UBoolSort>>()) + }.toPersistentMap() + + val updates = UTreeUpdates( + updates = RegionTree(map), + keyInfo() + ) + + return USymbolicCollection(this, updates) + } } class UInputSetId>( @@ -180,3 +217,5 @@ class UInputSetId>( override fun hashCode(): Int = hash(setType, elementSort) } + +//private typealias UInitializedSetRegionValue = Pair, Sort>, RegionTree<, UUpdateNode, Sort>>> From d2df3e5b22a9183a8c05c05255e10540701cce7d Mon Sep 17 00:00:00 2001 From: tochilinak Date: Tue, 29 Jul 2025 10:56:04 +0300 Subject: [PATCH 3/8] initializeAllocatedSet --- .../collection/set/primitive/USetRegion.kt | 25 +++++++++++++++++++ .../set/primitive/USymbolicSetId.kt | 14 ++++++----- 2 files changed, 33 insertions(+), 6 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt index 2268378f87..9024a1ca73 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt @@ -6,6 +6,7 @@ import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collection.array.UArrayRegion import org.usvm.collection.set.USymbolicSetEntries import org.usvm.collection.set.USymbolicSetElement import org.usvm.collection.set.USymbolicSetElementsCollector @@ -81,6 +82,16 @@ interface USetRegion> : operationGuard: UBoolExpr, ownership: MutabilityOwnership, ): USetRegion + + fun initializeAllocatedSet( + address: UConcreteHeapAddress, + setType: SetType, + sort: ElementSort, + content: Set>, + operationGuard: UBoolExpr, + ownership: MutabilityOwnership, + makeDisjointCheck: Boolean = true, + ): USetRegion } internal class USetMemoryRegion>( @@ -203,6 +214,20 @@ internal class USetMemoryRegion> }, ) + override fun initializeAllocatedSet( + address: UConcreteHeapAddress, + setType: SetType, + sort: ElementSort, + content: Set>, + operationGuard: UBoolExpr, + ownership: MutabilityOwnership, + makeDisjointCheck: Boolean, + ): USetRegion { + 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 = foldHeapRefWithStaticAsSymbolic( ref = ref, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 839fa9f700..196fdc2e9d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -124,7 +124,8 @@ class UAllocatedSetId>( fun initializedSet( content: Set>, - guard: UBoolExpr + guard: UBoolExpr, + makeDisjointCheck: Boolean = true, ): USymbolicCollection, UExpr, UBoolSort> { val ctx = guard.ctx @@ -133,10 +134,13 @@ class UAllocatedSetId>( val update = UPinpointUpdateNode(value, elementInfo, ctx.trueExpr, guard) val region = elementInfo.keyToRegion(value) - check(region.compare(unionRegion) == Region.ComparisonResult.DISJOINT) { - "Cannot create initializedSet if regions of given elements intersect" + + if (makeDisjointCheck) { + check(region.compare(unionRegion) == Region.ComparisonResult.DISJOINT) { + "Cannot create initializedSet if regions of given elements intersect" + } + unionRegion = unionRegion.union(region) } - unionRegion = unionRegion.union(region) region to update } @@ -217,5 +221,3 @@ class UInputSetId>( override fun hashCode(): Int = hash(setType, elementSort) } - -//private typealias UInitializedSetRegionValue = Pair, Sort>, RegionTree<, UUpdateNode, Sort>>> From e9f8050b84b42dfdd005fff4a66819ff32990916 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Wed, 30 Jul 2025 15:41:45 +0300 Subject: [PATCH 4/8] fix --- .../kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 196fdc2e9d..58c8db2f66 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -136,7 +136,7 @@ class UAllocatedSetId>( val region = elementInfo.keyToRegion(value) if (makeDisjointCheck) { - check(region.compare(unionRegion) == Region.ComparisonResult.DISJOINT) { + check(unionRegion.compare(region) == Region.ComparisonResult.DISJOINT) { "Cannot create initializedSet if regions of given elements intersect" } unionRegion = unionRegion.union(region) From 7b00e7b91c12eca41be7c654f312dfbcbc6cf831 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Wed, 30 Jul 2025 15:42:59 +0300 Subject: [PATCH 5/8] import fix --- .../kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt | 2 -- 1 file changed, 2 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 58c8db2f66..4aab626266 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -2,7 +2,6 @@ package org.usvm.collection.set.primitive import io.ksmt.cache.hash import io.ksmt.utils.uncheckedCast -import kotlinx.collections.immutable.persistentMapOf import kotlinx.collections.immutable.toPersistentMap import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -14,7 +13,6 @@ import org.usvm.collection.set.USetRegionBuilder import org.usvm.collection.set.USymbolicSetElement import org.usvm.collection.set.USymbolicSetElementRegion import org.usvm.collection.set.USymbolicSetKeyInfo -import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UPinpointUpdateNode import org.usvm.memory.USymbolicCollection From 8c572175e7d71aec659442678ccc7a32f09dedc9 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Wed, 30 Jul 2025 16:42:52 +0300 Subject: [PATCH 6/8] detekt fix --- .../org/usvm/collection/set/primitive/USetRegion.kt | 13 +++++++++---- .../usvm/collection/set/primitive/USymbolicSetId.kt | 1 - 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt index 9024a1ca73..ac013e640c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt @@ -6,14 +6,13 @@ import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort -import org.usvm.collection.array.UArrayRegion -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 @@ -225,7 +224,13 @@ internal class USetMemoryRegion> ): USetRegion { 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) + return USetMemoryRegion( + setType, + elementSort, + elementInfo, + allocatedSets.put(setId, newCollection, ownership), + inputSet + ) } override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries = diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 4aab626266..18166ff0e0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -125,7 +125,6 @@ class UAllocatedSetId>( guard: UBoolExpr, makeDisjointCheck: Boolean = true, ): USymbolicCollection, UExpr, UBoolSort> { - val ctx = guard.ctx var unionRegion = elementInfo.bottomRegion() val entries = content.map { value -> From ab2245006b30bf65373383d9c3d906a1e65a77c3 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Wed, 30 Jul 2025 17:04:34 +0300 Subject: [PATCH 7/8] Valentyn's fix in UComposer --- usvm-core/src/main/kotlin/org/usvm/Composition.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index 574b91908d..7f23afc945 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -31,8 +31,8 @@ open class UComposer( override fun transform(expr: UIteExpr): UExpr = 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) } } From d6cc4ff65bd26d49cec441e7d28c49b47b6dce58 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Thu, 31 Jul 2025 14:10:21 +0300 Subject: [PATCH 8/8] PR fix --- .../kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 18166ff0e0..f700b2ca12 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -123,7 +123,7 @@ class UAllocatedSetId>( fun initializedSet( content: Set>, guard: UBoolExpr, - makeDisjointCheck: Boolean = true, + makeDisjointCheck: Boolean = false, // for debug purposes ): USymbolicCollection, UExpr, UBoolSort> { val ctx = guard.ctx var unionRegion = elementInfo.bottomRegion()