From c893b6b513f7aca3547037932df857a48f8e5a65 Mon Sep 17 00:00:00 2001
From: Valentyn Sobol <napster_1997@mail.ru>
Date: Mon, 16 Dec 2024 17:46:28 +0300
Subject: [PATCH 1/2] Fix composer handling in set union adapter cache

---
 .../set/primitive/USymbolicSetUnionAdapter.kt | 28 ++++++++++++++++---
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
index 20dc6bdf9..35f383711 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
@@ -19,8 +19,9 @@ import org.usvm.memory.USymbolicCollectionKeyInfo
 import org.usvm.memory.UUpdateNode
 import org.usvm.memory.UWritableMemory
 import org.usvm.memory.key.UHeapRefKeyInfo
-import org.usvm.uctx
 import org.usvm.regions.Region
+import org.usvm.uctx
+import java.lang.ref.WeakReference
 
 sealed class USymbolicSetUnionAdapter<
     SetType, SrcKey, DstKey,
@@ -46,13 +47,13 @@ sealed class USymbolicSetUnionAdapter<
          * */
         val prevIncludesSymbolicallyCache = lastIncludesSymbolicallyCheck
         if (prevIncludesSymbolicallyCache != null) {
-            if (prevIncludesSymbolicallyCache.key == srcKey) {
+            if (prevIncludesSymbolicallyCache.containsCachedValue(srcKey, composer)) {
                 return prevIncludesSymbolicallyCache.result
             }
         }
 
         return setOfKeys.read(srcKey, composer).also {
-            lastIncludesSymbolicallyCheck = IncludesSymbolicallyCache(srcKey, it)
+            lastIncludesSymbolicallyCheck = IncludesSymbolicallyCache(srcKey, composer, it)
         }
     }
 
@@ -66,7 +67,26 @@ sealed class USymbolicSetUnionAdapter<
 
     abstract override fun collectSetElements(elements: USymbolicSetElementsCollector.Elements<DstKey>)
 
-    private data class IncludesSymbolicallyCache<Key>(val key: Key, val result: UBoolExpr)
+    private data class IncludesSymbolicallyCache<Key>(
+        val key: WeakReference<Key>,
+        val composer: WeakReference<UComposer<*, *>>?,
+        val result: UBoolExpr
+    ) {
+        constructor(key: Key, composer: UComposer<*, *>?, result: UBoolExpr) :
+                this(WeakReference(key), composer?.let { WeakReference(it) }, result)
+
+        fun containsCachedValue(key: Key, composer: UComposer<*, *>?): Boolean {
+            val thisKey = this.key.get() ?: return false
+            if (thisKey != key) return false
+
+            if (composer == null) {
+                return this.composer == null
+            }
+
+            val thisComposer = this.composer?.get() ?: return false
+            return thisComposer == composer
+        }
+    }
 }
 
 class UAllocatedToAllocatedSymbolicSetUnionAdapter<SetType, ElemSort : USort>(

From 9da4ee15186ffee25e53c13e3e64e251a11391e6 Mon Sep 17 00:00:00 2001
From: Valentyn Sobol <napster_1997@mail.ru>
Date: Mon, 16 Dec 2024 17:56:30 +0300
Subject: [PATCH 2/2] minor

---
 .../set/primitive/USymbolicSetUnionAdapter.kt  | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
index 35f383711..cb3002194 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
@@ -76,15 +76,19 @@ sealed class USymbolicSetUnionAdapter<
                 this(WeakReference(key), composer?.let { WeakReference(it) }, result)
 
         fun containsCachedValue(key: Key, composer: UComposer<*, *>?): Boolean {
-            val thisKey = this.key.get() ?: return false
-            if (thisKey != key) return false
+            if (!this.key.equalTo(key)) return false
 
-            if (composer == null) {
-                return this.composer == null
-            }
+            val thisComposer = this.composer ?: return composer == null
+            if (composer == null) return false
+
+            return thisComposer.equalTo(composer)
+        }
 
-            val thisComposer = this.composer?.get() ?: return false
-            return thisComposer == composer
+        companion object {
+            private fun <T> WeakReference<T>.equalTo(other: T): Boolean {
+                val value = get() ?: return false
+                return value == other
+            }
         }
     }
 }