From c3d33dab1562999ef0583cdb9ef7f3d64f6c6d05 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 14 Sep 2026 15:49:54 +0200 Subject: [PATCH 1/5] Optimize PathCopyingPersistentTreeMap when same k/v pair is inserted In this case we can reuse the same object instances as the input. This has no visible behavior change except that the map object sometimes remains the same instance after putAndCopy(). But this is not what anyone would rely on, as it is common for persistent data structures to do things like this. For example, removeAndCopy() also returns the same map object if there are no changes. --- .../collect/PathCopyingPersistentTreeMap.java | 3 +++ .../PathCopyingPersistentTreeMapTest.java | 26 +++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index 561e4b2b0..516612a5a 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -554,6 +554,9 @@ private static , V> Node putAndCopy0( Node newRight = putAndCopy0(key, value, current.right); current = current.withRightChild(newRight); + } else if (key == current.getKey() && value == current.getValue()) { + return current; + } else { current = new Node<>(key, value, current.left, current.right, current.getColor()); } diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java index 7a425f792..b757c41e0 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java @@ -434,4 +434,30 @@ public void testEntrySetContains() { assertThat(second.entrySet().containsAll(first.entrySet())).isFalse(); assertThat(first.entrySet().containsAll(second.entrySet())).isFalse(); } + + @Test + public void testRemovingMissingKey() { + map = map.putAndCopy("a", "").putAndCopy("b", "").putAndCopy("y", "").putAndCopy("z", ""); + + assertWithMessage("Removing missing key should produce same map") + .that(map.removeAndCopy("key")) + .isSameInstanceAs(map); + } + + @Test + @SuppressWarnings("checkstyle:IllegalInstantiation") + public void testSettingIdenticalKeyValue() { + String k = "key"; + String v = "value"; + map = + map.putAndCopy("a", "") + .putAndCopy("b", "") + .putAndCopy(k, v) + .putAndCopy("y", "") + .putAndCopy("z", ""); + + assertWithMessage("Reinserting same k/v pair should produce same map") + .that(map.putAndCopy(k, v)) + .isSameInstanceAs(map); + } } From 115ec2d105f5e49ff0c3e96c29a460c4dcd4f790 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 14 Sep 2026 16:18:22 +0200 Subject: [PATCH 2/5] Use the old key object when reinserting same key in map This affects cases where a new object that compares equal to an existing key object is used for insertion. Previously PathCopyingPersistentTreeMap would use the new key object, now we use the old key object. There are no strict rules on what to use, but this is what HashMap and TreeMap do (as seen in some new tests), and so it is not a bad idea to be consistent. Also it allows us to reuse the same object a little bit more often (if identical value with new key object is inserted). --- .../collect/PathCopyingPersistentTreeMap.java | 15 +++- .../PathCopyingPersistentTreeMapTest.java | 78 +++++++++++++++++-- 2 files changed, 84 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index 516612a5a..1f8019f37 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -137,6 +137,14 @@ Node withColor(boolean color) { } } + Node withValue(V newValue) { + if (newValue == getValue()) { + return this; + } else { + return new Node<>(getKey(), newValue, left, right, isRed); + } + } + @SuppressWarnings("ReferenceEquality") // cannot use equals() for check whether tree is the same Node withLeftChild(Node newLeft) { if (newLeft == left) { @@ -554,11 +562,10 @@ private static , V> Node putAndCopy0( Node newRight = putAndCopy0(key, value, current.right); current = current.withRightChild(newRight); - } else if (key == current.getKey() && value == current.getValue()) { - return current; - } else { - current = new Node<>(key, value, current.left, current.right, current.getColor()); + // This always keeps the old key object (if it compares equal but is not the same instance), + // but uses the new value object. This is not strictly necessary but what JDK maps do as well. + current = current.withValue(value); } // restore invariants diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java index b757c41e0..389f6f133 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java @@ -12,6 +12,7 @@ import static com.google.common.truth.Truth.assertWithMessage; import static org.junit.Assert.assertThrows; +import com.google.common.collect.FluentIterable; import com.google.common.collect.Ordering; import com.google.common.collect.testing.NavigableMapTestSuiteBuilder; import com.google.common.collect.testing.TestStringSortedMapGenerator; @@ -21,6 +22,7 @@ import com.google.common.testing.EqualsTester; import com.google.errorprone.annotations.Var; import java.util.Collection; +import java.util.HashMap; import java.util.Map; import java.util.NavigableMap; import java.util.Random; @@ -446,18 +448,84 @@ public void testRemovingMissingKey() { @Test @SuppressWarnings("checkstyle:IllegalInstantiation") - public void testSettingIdenticalKeyValue() { - String k = "key"; - String v = "value"; + public void testSettingIdenticalObjects() { + String k1 = new String("key"); + String k2 = new String("key"); + String v1 = new String("value"); + String v2 = new String("value"); map = map.putAndCopy("a", "") .putAndCopy("b", "") - .putAndCopy(k, v) + .putAndCopy(k1, v1) .putAndCopy("y", "") .putAndCopy("z", ""); assertWithMessage("Reinserting same k/v pair should produce same map") - .that(map.putAndCopy(k, v)) + .that(map.putAndCopy(k1, v1)) .isSameInstanceAs(map); + + assertWithMessage("Reinserting same value should produce same map") + .that(map.putAndCopy(k2, v1)) + .isSameInstanceAs(map); + + assertWithMessage("Inserting new value should produce map with new value") + .that(map.putAndCopy(k1, v2).get(k1)) + .isSameInstanceAs(v2); + + assertWithMessage("Inserting new k/v pair should keep old key") + .that( + FluentIterable.from(map.putAndCopy(k2, v2).keySet()) + .filter(s -> s.length() > 1) + .first() + .get()) + .isSameInstanceAs(k1); + assertWithMessage("Inserting new k/v pair should produce map with new value") + .that(map.putAndCopy(k2, v2).get(k2)) + .isSameInstanceAs(v2); + } + + @Test + public void testSettingIdenticalObjectsInHashMap() { + testSettingIdenticalObjectsInStandardMap(new HashMap<>()); + } + + @Test + public void testSettingIdenticalObjectsInTreeMap() { + testSettingIdenticalObjectsInStandardMap(new TreeMap<>()); + } + + @SuppressWarnings("checkstyle:IllegalInstantiation") + private static void testSettingIdenticalObjectsInStandardMap(Map map) { + // not testing own code, but checking expectations of other map implementations + + String k1 = new String("key"); + String k2 = new String("key"); + String k3 = new String("key"); + String v1 = new String("value"); + String v2 = new String("value"); + String v3 = new String("value"); + map.put("a", ""); + map.put("b", ""); + map.put(k1, v1); + map.put("y", ""); + map.put("z", ""); + + map.put(k2, v1); + assertWithMessage("Inserting same value should keep old key") + .that(FluentIterable.from(map.keySet()).filter(s -> s.length() > 1).first().get()) + .isSameInstanceAs(k1); + + map.put(k1, v2); + assertWithMessage("Inserting new value should produce map with new value") + .that(map.get(k1)) + .isSameInstanceAs(v2); + + map.put(k3, v3); + assertWithMessage("Inserting new k/v pair should keep old key") + .that(FluentIterable.from(map.keySet()).filter(s -> s.length() > 1).first().get()) + .isSameInstanceAs(k1); + assertWithMessage("Inserting new k/v pair should produce map with new value") + .that(map.get(k1)) + .isSameInstanceAs(v3); } } From 5996ef1de488eb2d9b1671c112786ed65f8c7ef7 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 14 Sep 2026 17:06:31 +0200 Subject: [PATCH 3/5] Also suppress our Refaster rule for new String() --- .../common/collect/PathCopyingPersistentTreeMapTest.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java index 389f6f133..ab8bf97af 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMapTest.java @@ -447,7 +447,7 @@ public void testRemovingMissingKey() { } @Test - @SuppressWarnings("checkstyle:IllegalInstantiation") + @SuppressWarnings({"checkstyle:IllegalInstantiation", "StringUselessMethods"}) public void testSettingIdenticalObjects() { String k1 = new String("key"); String k2 = new String("key"); @@ -494,7 +494,7 @@ public void testSettingIdenticalObjectsInTreeMap() { testSettingIdenticalObjectsInStandardMap(new TreeMap<>()); } - @SuppressWarnings("checkstyle:IllegalInstantiation") + @SuppressWarnings({"checkstyle:IllegalInstantiation", "StringUselessMethods"}) private static void testSettingIdenticalObjectsInStandardMap(Map map) { // not testing own code, but checking expectations of other map implementations From 52968857eca1120da36f9f4fcb89872f7e2a5caf Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 18 Sep 2026 08:02:02 +0200 Subject: [PATCH 4/5] Update API documentation of our persistent map We do not want make it sound as if we guarantee to return fresh object instances. This was wrong already for removeAndCopy() and is now also wrong for putAndCopy(). --- .../common/collect/PathCopyingPersistentTreeMap.java | 2 +- src/org/sosy_lab/common/collect/PersistentMap.java | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index 1f8019f37..f01bf40c4 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -54,7 +54,7 @@ * always compares according to the natural ordering. All methods may throw {@link * ClassCastException} is key objects are passed that do not implement {@link Comparable}. * - *

The natural ordering of the keys needs to be consistent with equals. + *

The natural ordering of the keys needs to be consistent with equals and object identity. * *

As for all {@link PersistentMap}s, all collection views and all iterators are immutable. They * do not reflect changes made to the map and all their modifying operations throw {@link diff --git a/src/org/sosy_lab/common/collect/PersistentMap.java b/src/org/sosy_lab/common/collect/PersistentMap.java index 4bb3ca2dd..88ffbfc1e 100644 --- a/src/org/sosy_lab/common/collect/PersistentMap.java +++ b/src/org/sosy_lab/common/collect/PersistentMap.java @@ -20,8 +20,8 @@ /** * Interface for persistent map. A persistent data structure is immutable, but provides cheap * copy-and-write operations. Thus all write operations ({{@link #putAndCopy(Object, Object)}, - * {{@link #removeAndCopy(Object)}}) will not modify the current instance, but return a new instance - * instead. + * {{@link #removeAndCopy(Object)}}) will not modify the current instance, but return an updated + * instance instead. * *

All modifying operations inherited from {@link Map} are not supported and will always throw * {@link UnsupportedOperationException}. All collections returned by methods of this interface are @@ -35,11 +35,11 @@ @Immutable(containerOf = {"K", "V"}) public interface PersistentMap extends Map { - /** Replacement for {{@link #put(Object, Object)} that returns a fresh instance. */ + /** Replacement for {{@link #put(Object, Object)} that returns an updated map. */ @CheckReturnValue PersistentMap putAndCopy(@CompatibleWith("K") K key, @CompatibleWith("V") V value); - /** Replacement for {{@link #remove(Object)} that returns a fresh instance. */ + /** Replacement for {{@link #remove(Object)} that returns an updated map. */ @CheckReturnValue PersistentMap removeAndCopy(@CompatibleWith("K") Object key); From fd5a927c9211733689bb3a747f95e159257ed1d7 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 18 Sep 2026 08:03:48 +0200 Subject: [PATCH 5/5] Update comment for developers about why we reuse old key As suggested by Thomas in review. --- .../common/collect/PathCopyingPersistentTreeMap.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index f01bf40c4..74bb8c597 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -563,8 +563,13 @@ private static , V> Node putAndCopy0( current = current.withRightChild(newRight); } else { - // This always keeps the old key object (if it compares equal but is not the same instance), - // but uses the new value object. This is not strictly necessary but what JDK maps do as well. + // This always keeps the old (equal) key object. This has useful implications: + // Because we reuse the old key object, the key instance does not change and potential `==` + // comparisons on the key at other locations still work successfully. + // We do always use the new value object; but in case that the new value object is identical + // to the old value object, we can reuse the existing Node object and the whole map. This also + // enables `==` comparisons to succeed and saves some memory. + // This behavior also matches what JDK maps do. current = current.withValue(value); }