From 14f0f640ee8e3bb297a0aa73c69a3cbcbfa7cc96 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:20:46 +0300 Subject: [PATCH 1/2] Preserve unknown initial keys when copying input reference sets --- .../set/ref/USymbolicRefSetUnionAdapter.kt | 10 +++---- .../org/usvm/api/collections/ObjectMapTest.kt | 28 +++++++++++++++++++ 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetUnionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetUnionAdapter.kt index 6d5e1a354a..50f6b4a6ca 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetUnionAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetUnionAdapter.kt @@ -157,9 +157,8 @@ class UInputToAllocatedSymbolicRefSetUnionAdapter( override fun collectSetElements(elements: USymbolicSetElementsCollector.Elements) { val setElements = USymbolicSetElementsCollector.collect(setOfKeys.updates) - if (setElements.isInput) { - elements.isInput = true - } + // The initial input collection can contain elements absent from its update tree. + elements.isInput = true setElements.elements.mapTo(elements.elements) { it.second } } @@ -211,9 +210,8 @@ class UInputToInputSymbolicRefSetUnionAdapter( override fun collectSetElements(elements: USymbolicSetElementsCollector.Elements>) { val setElements = USymbolicSetElementsCollector.collect(setOfKeys.updates) - if (setElements.isInput) { - elements.isInput = true - } + // The initial input collection can contain elements absent from its update tree. + elements.isInput = true setElements.elements.mapTo(elements.elements) { dstSetRef to it.second } } diff --git a/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt b/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt index 87eb953b77..b7ffff7e94 100644 --- a/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt @@ -253,6 +253,34 @@ class ObjectMapTest : SymbolicCollectionTestBase() { testMapMerge(symbolicMap0, symbolicMap1) } + @Test + fun testCopiedInputMapCanSelectAnInitialKey() = testInputCopyRetainsUnknownKey(throughSecondCopy = false) + + @Test + fun testRepeatedInputMapCopyCanSelectAnInitialKey() = testInputCopyRetainsUnknownKey(throughSecondCopy = true) + + private fun testInputCopyRetainsUnknownKey(throughSecondCopy: Boolean) = scope.doWithState { + val source = ctx.mkRegisterReading(99, ctx.addressSort) + val firstCopy = mkSymbolicObjectMap(mapType) + symbolicObjectMapMergeInto(firstCopy, source, mapType, ctx.sizeSort) + val copy = if (throughSecondCopy) { + val secondCopy = mkSymbolicObjectMap(mapType) + symbolicObjectMapMergeInto(secondCopy, firstCopy, mapType, ctx.sizeSort) + secondCopy + } else { + firstCopy + } + + val selectedKey = symbolicObjectMapAnyKey(copy, mapType) + val sourceContains = symbolicObjectMapContains(source, selectedKey, mapType) + val copyContains = symbolicObjectMapContains(copy, selectedKey, mapType) + + checkWithSolver { + assertPossible { mkAnd(mkNot(mkHeapRefEq(source, nullRef)), sourceContains, copyContains) } + assertImpossible { mkAnd(copyContains, mkNot(sourceContains)) } + } + } + @Test fun testMapRetrieveAnyKey() = scope.doWithState { callStack.push(method = Any(), returnSite = null) From 01cba79336b50d4cc71dbb1e2ce1ab18647113f9 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:22:20 +0300 Subject: [PATCH 2/2] Clarify copied input map regression setup --- .../src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt b/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt index b7ffff7e94..b503971d64 100644 --- a/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/api/collections/ObjectMapTest.kt @@ -260,8 +260,9 @@ class ObjectMapTest : SymbolicCollectionTestBase() { fun testRepeatedInputMapCopyCanSelectAnInitialKey() = testInputCopyRetainsUnknownKey(throughSecondCopy = true) private fun testInputCopyRetainsUnknownKey(throughSecondCopy: Boolean) = scope.doWithState { - val source = ctx.mkRegisterReading(99, ctx.addressSort) + val source = ctx.mkRegisterReading(idx = 99, sort = ctx.addressSort) val firstCopy = mkSymbolicObjectMap(mapType) + symbolicObjectMapMergeInto(firstCopy, source, mapType, ctx.sizeSort) val copy = if (throughSecondCopy) { val secondCopy = mkSymbolicObjectMap(mapType)