From e0776fcc9484f2d733e5f7ba2b86a891b66e3996 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 7 Sep 2026 19:14:37 +0200 Subject: [PATCH 01/16] Add interface PersistentStack for copy-efficient persistent stacks --- .../common/collect/PersistentStack.java | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 src/org/sosy_lab/common/collect/PersistentStack.java diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java new file mode 100644 index 000000000..2529b5455 --- /dev/null +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -0,0 +1,85 @@ +// This file is part of SoSy-Lab Common, +// a library of useful utilities: +// https://github.com/sosy-lab/java-common-lib +// +// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.common.collect; + +import com.google.errorprone.annotations.CheckReturnValue; +import com.google.errorprone.annotations.Immutable; +import java.io.Serializable; +import java.util.NoSuchElementException; + +/** + * Interface for persistent stacks. A persistent data structure is structurally immutable, but + * provides cheap copy-and-write operations. Operations that conceptually modify the stack return + * another stack while leaving the current instance unchanged. + * + *

Implementations are expected to provide {@link #pushAndCopy(Object)}, {@link #popAndCopy()}, + * {@link #peek()}, {@link #empty()}, {@link #isEmpty()}, and {@link #size()} in O(1) time. + * Iteration proceeds from the top of the stack to the bottom. + * + *

Null values are not supported. + * + *

Implementations support standard Java Object Serialization. Serialization succeeds only if + * each contained value and its serialized object graph are serializable at runtime; otherwise, + * serialization fails according to the standard rules, for example with {@link + * java.io.NotSerializableException}. + * + *

This serialization contract applies to conforming Java SE runtimes. GraalVM in JVM mode uses + * the same semantics, while GraalVM Native Image may require explicit serialization metadata or + * configuration. Support in non-Java-SE environments, such as Android or GWT, is not guaranteed. + * Deserialization may also be rejected by configured {@link java.io.ObjectInputFilter} policies, + * and portability of serialized data depends on the serialized forms of contained values. + * + *

After a stack reference has been made visible to other threads through synchronization, a + * {@code volatile} field, or a concurrency utility, its immutable structure may be accessed + * concurrently. Such coordination is still required to publish or update a shared reference to a + * stack version, and compound updates require synchronization or an atomic operation. No + * thread-safety guarantee is made for iterator instances. + * + *

Values are stored by reference: they are not copied or made immutable or thread-safe. Changes + * to mutable values can affect equality and hash codes. Operations that depend on values also + * depend on their thread safety. + * + * @param The type of values. + */ +@Immutable(containerOf = "T") +public interface PersistentStack extends Iterable, Serializable { + + /** + * Returns a stack with {@code value} on top, leaving this stack unchanged. + * + * @throws NullPointerException if {@code value} is null + */ + @CheckReturnValue + PersistentStack pushAndCopy(T value); + + /** + * Returns a stack without this stack's top value, leaving this stack unchanged. + * + * @throws NoSuchElementException if this stack is empty + */ + @CheckReturnValue + PersistentStack popAndCopy(); + + /** + * Returns this stack's top value without modifying the stack. + * + * @throws NoSuchElementException if this stack is empty + */ + T peek(); + + /** Returns an empty stack of the same implementation. */ + @CheckReturnValue + PersistentStack empty(); + + /** Returns whether this stack contains no values. */ + boolean isEmpty(); + + /** Returns the number of values in this stack. */ + int size(); +} From 7623f26d136a1b2d5afd0b7002c54d2f48634643 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 7 Sep 2026 19:16:31 +0200 Subject: [PATCH 02/16] Add an extended implementation of the PersistentStack present in CPAchecker. This PersistentLinkedStack comes with an iterator and serialization proxy. It is copy efficient and allows O(1) push/pop. --- .../common/collect/PersistentLinkedStack.java | 273 ++++++++++++++++++ 1 file changed, 273 insertions(+) create mode 100644 src/org/sosy_lab/common/collect/PersistentLinkedStack.java diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java new file mode 100644 index 000000000..c9878d01e --- /dev/null +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -0,0 +1,273 @@ +// This file is part of SoSy-Lab Common, +// a library of useful utilities: +// https://github.com/sosy-lab/java-common-lib +// +// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.common.collect; + +import static com.google.common.base.Preconditions.checkNotNull; + +import com.google.common.collect.UnmodifiableIterator; +import com.google.errorprone.annotations.Immutable; +import com.google.errorprone.annotations.Var; +import java.io.InvalidObjectException; +import java.io.ObjectInputStream; +import java.io.Serial; +import java.io.Serializable; +import java.util.Iterator; +import java.util.NoSuchElementException; +import java.util.Objects; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * A persistent stack. Pushes structurally share the complete previous stack, and pops return the + * existing tail without copying, while leaving the original stack unchanged. Thus {@link + * #pushAndCopy(Object)}, {@link #popAndCopy()}, {@link #peek()}, {@link #empty()}, {@link + * #isEmpty()}, and {@link #size()} run in O(1) time. Iteration, {@link #equals(Object)}, {@link + * #hashCode()}, and {@link #toString()} have O(n) worst-case stack-traversal overhead. When two + * equal-size {@link PersistentLinkedStack} instances share a tail, {@code equals} traverses only + * the k nodes preceding that tail and thus has O(k) traversal overhead. These bounds exclude work + * performed by element methods. + * + *

All structural state is final and correctly constructed, so the immutable stack structure may + * be accessed concurrently without synchronization. Publishing or updating a shared reference to a + * stack version still requires coordination, and compound updates require synchronization or an + * atomic operation. Each traversal has an independent iterator; a single iterator instance has no + * thread-safety guarantee. Values are stored by reference and are not copied or made immutable or + * thread-safe. + * + *

Null values are not supported. + * + *

Serialization: Serialization and deserialization have O(n) stack-traversal overhead and + * use O(n) temporary memory, excluding the processing of element object graphs. A flattened proxy + * stores the logical values in top-to-bottom order instead of serializing the linked nodes. This + * avoids recursive traversal of long stacks and keeps node and cache fields out of the serialized + * form. Deserialization rejects null proxy data and rebuilds the stack from bottom to top while + * validating each value, thereby preserving order and restoring the canonical empty instance. + * Because each stack is flattened independently, distinct, structurally related stacks serialized + * together have their shared non-empty tails reconstructed independently; {@link #popAndCopy()} on + * a deserialized stack nevertheless returns its existing tail. Element object graphs must not + * contain references back to the containing stack because proxy replacement cannot restore such + * cycles. Persisted data remains readable only while the proxy and element serialized forms remain + * compatible. + * + * @param the type of values + */ +@Immutable(containerOf = "T") +public final class PersistentLinkedStack implements PersistentStack { + + @Serial private static final long serialVersionUID = -4286928240765960519L; + + private static final PersistentLinkedStack EMPTY = new PersistentLinkedStack<>(); + + /** The top value, null exactly for the empty singleton. */ + @SuppressWarnings("serial") // writeReplace prevents direct serialization of this field. + private final @Nullable T top; + + /** The linked tail, null exactly for the empty singleton. */ + private final @Nullable PersistentLinkedStack tail; + + /** + * The size, cached for O(1) access. It is zero exactly for the empty stack and otherwise equals + * {@code tail.size + 1}. The cache is one logical 4-byte {@code int}; its actual footprint + * depends on JVM object layout and alignment. It often fits into padding with compressed + * references and 8-byte alignment, but may add an alignment unit otherwise. + */ + private final int size; + + private PersistentLinkedStack() { + top = null; + tail = null; + size = 0; + } + + private PersistentLinkedStack(T pTop, PersistentLinkedStack pTail) { + top = checkNotNull(pTop); + tail = checkNotNull(pTail); + size = pTail.size + 1; + } + + /** Returns an empty stack. */ + @SuppressWarnings("unchecked") + public static PersistentLinkedStack of() { + return (PersistentLinkedStack) EMPTY; + } + + /** + * Returns a stack containing {@code value}. + * + * @throws NullPointerException if {@code value} is null + */ + public static PersistentLinkedStack of(T value) { + return new PersistentLinkedStack<>(value, PersistentLinkedStack.of()); + } + + @Override + public PersistentLinkedStack pushAndCopy(T value) { + return new PersistentLinkedStack<>(value, this); + } + + @Override + public PersistentLinkedStack popAndCopy() { + if (isEmpty()) { + throw new NoSuchElementException(); + } + return checkNotNull(tail); + } + + @Override + public T peek() { + if (isEmpty()) { + throw new NoSuchElementException(); + } + return checkNotNull(top); + } + + @Override + public PersistentLinkedStack empty() { + return of(); + } + + @Override + public boolean isEmpty() { + return size == 0; + } + + @Override + public int size() { + return size; + } + + @Override + public Iterator iterator() { + return new StackIterator<>(this); + } + + @Override + @SuppressWarnings("ReferenceEquality") // Node identity detects structurally shared tails. + public boolean equals(@Nullable Object obj) { + if (obj == this) { + return true; + } + if (!(obj instanceof PersistentLinkedStack other)) { + return false; + } + if (size != other.size()) { + return false; + } + + @Var PersistentLinkedStack thisRemainder = this; + @Var PersistentLinkedStack otherRemainder = other; + while (thisRemainder != otherRemainder) { + if (!Objects.equals(thisRemainder.top, otherRemainder.top)) { + return false; + } + thisRemainder = checkNotNull(thisRemainder.tail); + otherRemainder = checkNotNull(otherRemainder.tail); + } + return true; + } + + @Override + public int hashCode() { + @Var int hashCode = PersistentLinkedStack.class.hashCode(); + for (T value : this) { + hashCode = 31 * hashCode + value.hashCode(); + } + return hashCode; + } + + /** + * Returns the values in top-to-bottom order, separated by {@code ", "} and enclosed in square + * brackets: {@code [top, ..., bottom]}. The empty stack is represented as {@code []}. + */ + @Override + public String toString() { + StringBuilder result = new StringBuilder("["); + Iterator iterator = iterator(); + while (iterator.hasNext()) { + result.append(iterator.next()); + if (iterator.hasNext()) { + result.append(", "); + } + } + return result.append(']').toString(); + } + + @Serial + private Object writeReplace() { + return new SerializationProxy(this); + } + + @Serial + @SuppressWarnings("unused") // Serialization hook prevents bypassing the proxy. + private void readObject(ObjectInputStream pInputStream) throws InvalidObjectException { + throw new InvalidObjectException("Serialization proxy required"); + } + + /** Flat serialized form containing the logical values in top-to-bottom order. */ + private static final class SerializationProxy implements Serializable { + + @Serial private static final long serialVersionUID = 2702329958583141147L; + + /** Nullable only to model malformed serialized input, which {@link #readResolve()} rejects. */ + @SuppressWarnings("serial") // ObjectOutputStream checks each element graph at runtime. + private final @Nullable Object @Nullable [] values; + + private SerializationProxy(PersistentLinkedStack stack) { + values = new Object[stack.size]; + @Var int index = 0; + for (Object value : stack) { + values[index] = value; + index++; + } + } + + @Serial + private Object readResolve() throws InvalidObjectException { + @Nullable Object @Nullable [] serializedValues = values; + if (serializedValues == null) { + throw new InvalidObjectException("Stack values must not be null"); + } + + @Var PersistentLinkedStack stack = PersistentLinkedStack.of(); + // Push bottom-to-top to reconstruct the original iteration order. + for (@Var int index = serializedValues.length - 1; index >= 0; index--) { + @Nullable Object value = serializedValues[index]; + if (value == null) { + throw new InvalidObjectException("Stack values must not contain null"); + } + stack = stack.pushAndCopy(value); + } + return stack; + } + } + + private static final class StackIterator extends UnmodifiableIterator { + + private @Nullable PersistentLinkedStack stack; + + private StackIterator(PersistentLinkedStack pStack) { + stack = pStack; + } + + @Override + public boolean hasNext() { + return stack != null && !stack.isEmpty(); + } + + @Override + public T next() { + @Nullable PersistentLinkedStack currentStack = stack; + if (currentStack == null || currentStack.isEmpty()) { + throw new NoSuchElementException(); + } + T value = checkNotNull(currentStack.top); + stack = currentStack.tail; + return value; + } + } +} From d6da36685c4a2ae7d7dbbf6b2bacdc01823b06e9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 7 Sep 2026 19:17:06 +0200 Subject: [PATCH 03/16] Add the new persistent stack to PackageSanityTests --- src/org/sosy_lab/common/collect/PackageSanityTest.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/common/collect/PackageSanityTest.java b/src/org/sosy_lab/common/collect/PackageSanityTest.java index d349efcf9..877ce29e1 100644 --- a/src/org/sosy_lab/common/collect/PackageSanityTest.java +++ b/src/org/sosy_lab/common/collect/PackageSanityTest.java @@ -16,6 +16,8 @@ public class PackageSanityTest extends AbstractPackageSanityTests { { setDistinctValues( PersistentLinkedList.class, PersistentLinkedList.of(), PersistentLinkedList.of("test")); + setDistinctValues( + PersistentLinkedStack.class, PersistentLinkedStack.of(), PersistentLinkedStack.of("test")); @SuppressWarnings("unchecked") OurSortedMap singletonMap = (PathCopyingPersistentTreeMap) From 504a2dadca92f2638a13d5d50c5bcb773b73d2fe Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 7 Sep 2026 19:26:30 +0200 Subject: [PATCH 04/16] Add tests for PersistentLinkedStack --- .../collect/PersistentLinkedStackTest.java | 248 ++++++++++++++++++ 1 file changed, 248 insertions(+) create mode 100644 src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java new file mode 100644 index 000000000..303c2b429 --- /dev/null +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java @@ -0,0 +1,248 @@ +// This file is part of SoSy-Lab Common, +// a library of useful utilities: +// https://github.com/sosy-lab/java-common-lib +// +// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.common.collect; + +import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; + +import com.google.common.testing.EqualsTester; +import com.google.common.testing.SerializableTester; +import com.google.errorprone.annotations.Var; +import java.math.BigInteger; +import java.util.Iterator; +import java.util.NoSuchElementException; +import org.junit.Test; + +public class PersistentLinkedStackTest { + + @Test + public void testEmptyFactory() { + PersistentStack stack = PersistentLinkedStack.of(); + + assertThat(stack.isEmpty()).isTrue(); + } + + @Test + public void testSingletonFactory() { + PersistentStack stack = PersistentLinkedStack.of("value"); + + assertThat(stack.isEmpty()).isFalse(); + assertThat(stack).containsExactly("value"); + } + + @Test + public void testPushAndCopy() { + PersistentStack empty = PersistentLinkedStack.of(); + PersistentStack stack = empty.pushAndCopy("value"); + + assertThat(stack.peek()).isEqualTo("value"); + assertThat(empty).isEmpty(); + } + + @Test + public void testDuplicateEmptyStrings() { + PersistentStack stack = + PersistentLinkedStack.of().pushAndCopy("").pushAndCopy(""); + + assertThat(stack.size()).isEqualTo(2); + assertThat(stack.peek()).isEmpty(); + PersistentStack popped = stack.popAndCopy(); + assertThat(popped.size()).isEqualTo(1); + assertThat(popped.peek()).isEqualTo(stack.peek()); + } + + @Test + public void testIntegerValues() { + PersistentStack stack = + PersistentLinkedStack.of().pushAndCopy(1).pushAndCopy(2); + + assertThat(stack.size()).isEqualTo(2); + assertThat(stack.peek()).isEqualTo(2); + PersistentStack popped = stack.popAndCopy(); + assertThat(popped.size()).isEqualTo(1); + assertThat(popped.peek()).isEqualTo(1); + } + + @Test + public void testBigIntegerValueEqualityAndIdentity() { + BigInteger sharedValue = new BigInteger("123456789012345678901234567890"); + BigInteger equalValue = new BigInteger("123456789012345678901234567890"); + PersistentStack first = PersistentLinkedStack.of(sharedValue); + PersistentStack sameReference = PersistentLinkedStack.of(sharedValue); + PersistentStack equalReference = PersistentLinkedStack.of(equalValue); + + assertThat(first).isNotSameInstanceAs(sameReference); + assertThat(first).isEqualTo(sameReference); + assertThat(first.peek()).isSameInstanceAs(sharedValue); + assertThat(sameReference.peek()).isSameInstanceAs(sharedValue); + + assertThat(equalValue).isNotSameInstanceAs(sharedValue); + assertThat(equalValue).isEqualTo(sharedValue); + assertThat(first).isEqualTo(equalReference); + assertThat(equalReference.peek()).isSameInstanceAs(equalValue); + assertThat(equalReference.peek()).isNotSameInstanceAs(sharedValue); + } + + @Test + public void testPopReturnsSamePredecessor() { + PersistentStack predecessor = + PersistentLinkedStack.of().pushAndCopy("bottom").pushAndCopy("middle"); + PersistentStack stack = predecessor.pushAndCopy("top"); + + assertThat(stack.popAndCopy()).isSameInstanceAs(predecessor); + } + + @Test + public void testPeekEmptyThrows() { + PersistentStack empty = PersistentLinkedStack.of(); + + assertThrows(NoSuchElementException.class, empty::peek); + } + + @Test + public void testPopEmptyThrows() { + PersistentStack empty = PersistentLinkedStack.of(); + + assertThrows(NoSuchElementException.class, empty::popAndCopy); + } + + @Test + public void testSizeAcrossPersistentVersions() { + PersistentStack empty = PersistentLinkedStack.of(); + PersistentStack one = empty.pushAndCopy("one"); + PersistentStack two = one.pushAndCopy("two"); + + assertThat(empty.size()).isEqualTo(0); + assertThat(one.size()).isEqualTo(1); + assertThat(two.size()).isEqualTo(2); + assertThat(two.popAndCopy().size()).isEqualTo(1); + assertThat(empty.size()).isEqualTo(0); + assertThat(one.size()).isEqualTo(1); + assertThat(two.size()).isEqualTo(2); + } + + @Test + public void testCanonicalEmpty() { + PersistentStack empty = PersistentLinkedStack.of(); + PersistentStack singleton = PersistentLinkedStack.of("value"); + + assertThat(PersistentLinkedStack.of()).isSameInstanceAs(empty); + assertThat(singleton.empty()).isSameInstanceAs(empty); + assertThat(singleton.popAndCopy()).isSameInstanceAs(empty); + } + + @Test + public void testRejectsNull() { + PersistentStack empty = PersistentLinkedStack.of(); + + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of((String) null)); + assertThrows(NullPointerException.class, () -> empty.pushAndCopy(null)); + assertThrows( + NullPointerException.class, () -> PersistentLinkedStack.of("value").pushAndCopy(null)); + } + + @Test + public void testIteratorOrderIsTopToBottom() { + PersistentStack stack = + PersistentLinkedStack.of() + .pushAndCopy("bottom") + .pushAndCopy("middle") + .pushAndCopy("top"); + + assertThat(stack).containsExactly("top", "middle", "bottom").inOrder(); + } + + @Test + public void testIteratorExhaustion() { + Iterator iterator = PersistentLinkedStack.of("value").iterator(); + + assertThat(iterator.next()).isEqualTo("value"); + assertThrows(NoSuchElementException.class, iterator::next); + } + + @Test + public void testIteratorRemoveRejected() { + Iterator iterator = PersistentLinkedStack.of("value").iterator(); + + assertThrows(UnsupportedOperationException.class, iterator::remove); + } + + @Test + public void testEquality() { + PersistentStack stack = + PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top"); + PersistentStack independentlyBuilt = + PersistentLinkedStack.of() + .pushAndCopy("bottom") + .pushAndCopy("middle") + .pushAndCopy("top"); + PersistentStack differentOrder = + PersistentLinkedStack.of("top").pushAndCopy("middle").pushAndCopy("bottom"); + PersistentStack differentMiddle = + PersistentLinkedStack.of("bottom").pushAndCopy("other").pushAndCopy("top"); + PersistentStack differentBottom = + PersistentLinkedStack.of("other").pushAndCopy("middle").pushAndCopy("top"); + PersistentStack shorter = PersistentLinkedStack.of("middle").pushAndCopy("top"); + + new EqualsTester() + .addEqualityGroup(stack, independentlyBuilt) + .addEqualityGroup(differentOrder) + .addEqualityGroup(differentMiddle) + .addEqualityGroup(differentBottom) + .addEqualityGroup(shorter) + .testEquals(); + } + + @Test + public void testEqualityWithSharedTail() { + PersistentLinkedStack sharedTail = + PersistentLinkedStack.of("bottom").pushAndCopy("shared"); + PersistentStack stack = sharedTail.pushAndCopy("middle").pushAndCopy("top"); + PersistentStack equal = sharedTail.pushAndCopy("middle").pushAndCopy("top"); + PersistentStack different = sharedTail.pushAndCopy("other").pushAndCopy("top"); + + new EqualsTester().addEqualityGroup(stack, equal).addEqualityGroup(different).testEquals(); + } + + @Test + public void testToString() { + PersistentStack empty = PersistentLinkedStack.of(); + PersistentStack stack = + PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top"); + + assertThat(empty.toString()).isEqualTo("[]"); + assertThat(stack.toString()).isEqualTo("[top, middle, bottom]"); + } + + @Test + public void testSerializationRoundTrip() { + PersistentStack stack = + PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top"); + + SerializableTester.reserializeAndAssert(stack); + } + + @Test + public void testEmptySerializationReturnsCanonicalInstance() { + PersistentStack empty = PersistentLinkedStack.of(); + + assertThat(SerializableTester.reserialize(empty)).isSameInstanceAs(empty); + } + + @Test + public void testLongStackSerializationRoundTrip() { + int length = 10_000; + @Var PersistentStack stack = PersistentLinkedStack.of(); + for (int i = 0; i < length; i++) { + stack = stack.pushAndCopy(i); + } + + assertThat(SerializableTester.reserialize(stack)).isEqualTo(stack); + } +} From 401977f4c3222bdf109224f88decfc800a06290b Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:09:30 +0200 Subject: [PATCH 05/16] Switch PersistentLinkedStack to using a AbstractIterator --- .../common/collect/PersistentLinkedStack.java | 28 ++++++++----------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index c9878d01e..370a1797f 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -10,7 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; -import com.google.common.collect.UnmodifiableIterator; +import com.google.common.collect.AbstractIterator; import com.google.errorprone.annotations.Immutable; import com.google.errorprone.annotations.Var; import java.io.InvalidObjectException; @@ -246,28 +246,22 @@ private Object readResolve() throws InvalidObjectException { } } - private static final class StackIterator extends UnmodifiableIterator { + private static final class StackIterator extends AbstractIterator { - private @Nullable PersistentLinkedStack stack; + private PersistentLinkedStack remaining; - private StackIterator(PersistentLinkedStack pStack) { - stack = pStack; + private StackIterator(PersistentLinkedStack stack) { + remaining = stack; } @Override - public boolean hasNext() { - return stack != null && !stack.isEmpty(); - } - - @Override - public T next() { - @Nullable PersistentLinkedStack currentStack = stack; - if (currentStack == null || currentStack.isEmpty()) { - throw new NoSuchElementException(); + protected @Nullable T computeNext() { + if (remaining.isEmpty()) { + return endOfData(); } - T value = checkNotNull(currentStack.top); - stack = currentStack.tail; - return value; + T result = remaining.peek(); + remaining = remaining.popAndCopy(); + return result; } } } From 83f01637c8b1e17513cb9371c26b3273e533864a Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:12:04 +0200 Subject: [PATCH 06/16] Shorten PersistentStack interface documentation --- .../common/collect/PersistentStack.java | 22 ++++--------------- 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java index 2529b5455..de9d26858 100644 --- a/src/org/sosy_lab/common/collect/PersistentStack.java +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -24,26 +24,12 @@ * *

Null values are not supported. * - *

Implementations support standard Java Object Serialization. Serialization succeeds only if - * each contained value and its serialized object graph are serializable at runtime; otherwise, - * serialization fails according to the standard rules, for example with {@link - * java.io.NotSerializableException}. + *

Instances and their views are thread-safe; iterator instances have no thread-safety guarantee. + * Elements are not copied, and their own thread-safety requirements still apply. * - *

This serialization contract applies to conforming Java SE runtimes. GraalVM in JVM mode uses - * the same semantics, while GraalVM Native Image may require explicit serialization metadata or - * configuration. Support in non-Java-SE environments, such as Android or GWT, is not guaranteed. - * Deserialization may also be rejected by configured {@link java.io.ObjectInputFilter} policies, - * and portability of serialized data depends on the serialized forms of contained values. + *

Stacks are serializable when their elements are serializable. * - *

After a stack reference has been made visible to other threads through synchronization, a - * {@code volatile} field, or a concurrency utility, its immutable structure may be accessed - * concurrently. Such coordination is still required to publish or update a shared reference to a - * stack version, and compound updates require synchronization or an atomic operation. No - * thread-safety guarantee is made for iterator instances. - * - *

Values are stored by reference: they are not copied or made immutable or thread-safe. Changes - * to mutable values can affect equality and hash codes. Operations that depend on values also - * depend on their thread safety. + *

Values are stored by reference: they are not copied or made immutable or thread-safe. * * @param The type of values. */ From ca7f6dd04471ab6c1e895b5de40a19ca7acefcac Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:21:19 +0200 Subject: [PATCH 07/16] Remove iterable from PersistentStack, and add methods asTopDownIterable() and copyToList(), as well as implementations and updates of calls relying on iterable --- .../common/collect/PersistentLinkedStack.java | 16 +++++++++++----- .../collect/PersistentLinkedStackTest.java | 11 ++++++----- .../sosy_lab/common/collect/PersistentStack.java | 12 +++++++++++- 3 files changed, 28 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index 370a1797f..b2d8129a9 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -11,6 +11,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import com.google.common.collect.AbstractIterator; +import com.google.common.collect.ImmutableList; import com.google.errorprone.annotations.Immutable; import com.google.errorprone.annotations.Var; import java.io.InvalidObjectException; @@ -142,8 +143,13 @@ public int size() { } @Override - public Iterator iterator() { - return new StackIterator<>(this); + public Iterable asTopDownIterable() { + return () -> new StackIterator<>(this); + } + + @Override + public ImmutableList copyToList() { + return ImmutableList.copyOf(asTopDownIterable()).reverse(); } @Override @@ -174,7 +180,7 @@ public boolean equals(@Nullable Object obj) { @Override public int hashCode() { @Var int hashCode = PersistentLinkedStack.class.hashCode(); - for (T value : this) { + for (T value : this.asTopDownIterable()) { hashCode = 31 * hashCode + value.hashCode(); } return hashCode; @@ -187,7 +193,7 @@ public int hashCode() { @Override public String toString() { StringBuilder result = new StringBuilder("["); - Iterator iterator = iterator(); + Iterator iterator = asTopDownIterable().iterator(); while (iterator.hasNext()) { result.append(iterator.next()); if (iterator.hasNext()) { @@ -220,7 +226,7 @@ private static final class SerializationProxy implements Serializable { private SerializationProxy(PersistentLinkedStack stack) { values = new Object[stack.size]; @Var int index = 0; - for (Object value : stack) { + for (Object value : stack.asTopDownIterable()) { values[index] = value; index++; } diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java index 303c2b429..e22bbbba4 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java @@ -33,7 +33,7 @@ public void testSingletonFactory() { PersistentStack stack = PersistentLinkedStack.of("value"); assertThat(stack.isEmpty()).isFalse(); - assertThat(stack).containsExactly("value"); + assertThat(stack.asTopDownIterable()).containsExactly("value"); } @Test @@ -42,7 +42,8 @@ public void testPushAndCopy() { PersistentStack stack = empty.pushAndCopy("value"); assertThat(stack.peek()).isEqualTo("value"); - assertThat(empty).isEmpty(); + assertThat(empty.asTopDownIterable()).isEmpty(); + assertThat(empty.isEmpty()).isTrue(); } @Test @@ -155,12 +156,12 @@ public void testIteratorOrderIsTopToBottom() { .pushAndCopy("middle") .pushAndCopy("top"); - assertThat(stack).containsExactly("top", "middle", "bottom").inOrder(); + assertThat(stack.asTopDownIterable()).containsExactly("top", "middle", "bottom").inOrder(); } @Test public void testIteratorExhaustion() { - Iterator iterator = PersistentLinkedStack.of("value").iterator(); + Iterator iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator(); assertThat(iterator.next()).isEqualTo("value"); assertThrows(NoSuchElementException.class, iterator::next); @@ -168,7 +169,7 @@ public void testIteratorExhaustion() { @Test public void testIteratorRemoveRejected() { - Iterator iterator = PersistentLinkedStack.of("value").iterator(); + Iterator iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator(); assertThrows(UnsupportedOperationException.class, iterator::remove); } diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java index de9d26858..010ab6ebd 100644 --- a/src/org/sosy_lab/common/collect/PersistentStack.java +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -11,6 +11,7 @@ import com.google.errorprone.annotations.CheckReturnValue; import com.google.errorprone.annotations.Immutable; import java.io.Serializable; +import java.util.List; import java.util.NoSuchElementException; /** @@ -34,7 +35,7 @@ * @param The type of values. */ @Immutable(containerOf = "T") -public interface PersistentStack extends Iterable, Serializable { +public interface PersistentStack extends Serializable { /** * Returns a stack with {@code value} on top, leaving this stack unchanged. @@ -68,4 +69,13 @@ public interface PersistentStack extends Iterable, Serializable { /** Returns the number of values in this stack. */ int size(); + + /** + * Returns an unmodifiable top-to-bottom view in O(1) time. Each iterator traverses this stack + * version independently. + */ + Iterable asTopDownIterable(); + + /** Returns an unmodifiable bottom-to-top list in O(n) time and space. */ + List copyToList(); } From 047438e4797e5fb85725a1fa6731df53d0e6cee5 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:28:38 +0200 Subject: [PATCH 08/16] Make equals and hashcode of PersistentLinkedStack work on all PersistentStacks --- .../common/collect/PersistentLinkedStack.java | 31 +++++++++---------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index b2d8129a9..68db2b8b8 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -20,7 +20,6 @@ import java.io.Serializable; import java.util.Iterator; import java.util.NoSuchElementException; -import java.util.Objects; import org.checkerframework.checker.nullness.qual.Nullable; /** @@ -153,37 +152,37 @@ public ImmutableList copyToList() { } @Override - @SuppressWarnings("ReferenceEquality") // Node identity detects structurally shared tails. + @SuppressWarnings("ReferenceEquality") // Identical tails need no further comparison. public boolean equals(@Nullable Object obj) { if (obj == this) { return true; } - if (!(obj instanceof PersistentLinkedStack other)) { - return false; - } - if (size != other.size()) { + if (!(obj instanceof PersistentStack other) || size != other.size()) { return false; } - @Var PersistentLinkedStack thisRemainder = this; - @Var PersistentLinkedStack otherRemainder = other; - while (thisRemainder != otherRemainder) { - if (!Objects.equals(thisRemainder.top, otherRemainder.top)) { + @Var PersistentStack left = this; + @Var PersistentStack right = other; + while (!left.isEmpty()) { + if (left == right) { + return true; + } + if (!left.peek().equals(right.peek())) { return false; } - thisRemainder = checkNotNull(thisRemainder.tail); - otherRemainder = checkNotNull(otherRemainder.tail); + left = left.popAndCopy(); + right = right.popAndCopy(); } return true; } @Override public int hashCode() { - @Var int hashCode = PersistentLinkedStack.class.hashCode(); - for (T value : this.asTopDownIterable()) { - hashCode = 31 * hashCode + value.hashCode(); + @Var int hash = 1; + for (T value : asTopDownIterable()) { + hash = 31 * hash + value.hashCode(); } - return hashCode; + return hash; } /** From 79da4f59ec62f1c34f255a39463f4b3f87a26064 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:30:18 +0200 Subject: [PATCH 09/16] Refactor and simplify PersistentLinkedStack toString using a Joiner --- .../common/collect/PersistentLinkedStack.java | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index 68db2b8b8..f9faf7b13 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.base.Joiner; import com.google.common.collect.AbstractIterator; import com.google.common.collect.ImmutableList; import com.google.errorprone.annotations.Immutable; @@ -191,15 +192,7 @@ public int hashCode() { */ @Override public String toString() { - StringBuilder result = new StringBuilder("["); - Iterator iterator = asTopDownIterable().iterator(); - while (iterator.hasNext()) { - result.append(iterator.next()); - if (iterator.hasNext()) { - result.append(", "); - } - } - return result.append(']').toString(); + return "[" + Joiner.on(", ").join(asTopDownIterable()) + "]"; } @Serial From c427fa1b928e50be505a33572ac94e2648f5cdbd Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:49:43 +0200 Subject: [PATCH 10/16] Add PersistentStack equals and hashCode JavaDoc --- .../common/collect/PersistentStack.java | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java index 010ab6ebd..4efd5ed58 100644 --- a/src/org/sosy_lab/common/collect/PersistentStack.java +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -13,6 +13,7 @@ import java.io.Serializable; import java.util.List; import java.util.NoSuchElementException; +import org.checkerframework.checker.nullness.qual.Nullable; /** * Interface for persistent stacks. A persistent data structure is structurally immutable, but @@ -78,4 +79,30 @@ public interface PersistentStack extends Serializable { /** Returns an unmodifiable bottom-to-top list in O(n) time and space. */ List copyToList(); + + /** + * Returns {@code true} if and only if {@code obj} is a {@link PersistentStack} with the same + * number of elements and equal corresponding elements in top-to-bottom order. Elements are + * compared using {@link Object#equals(Object)}. + * + *

Equality is independent of the concrete implementation and structural sharing. All empty + * stacks are equal. + * + * @param obj the object to compare with this stack + * @return whether the object is equal to this stack + */ + @Override + boolean equals(@Nullable Object obj); + + /** + * Returns the hash code of this stack. + * + *

The hash code is computed starting with {@code hash = 1} and applying + * {@code hash = 31 * hash + element.hashCode()} to each element in top-to-bottom order, using + * Java {@code int} arithmetic. The hash code of an empty stack is {@code 1}. + * + * @return the hash code of this stack + */ + @Override + int hashCode(); } From 2f4f6508461d3ff39402750d3b914059e64acaf7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:53:07 +0200 Subject: [PATCH 11/16] Refactor PersistentLinkedStack with of() method for more than 2 arguments, and copyOf() impl, as well as toPersistentLinkedStack() impl + updates to readResolve() based on the new methods --- .../common/collect/PersistentLinkedStack.java | 61 ++++++++++++++----- 1 file changed, 46 insertions(+), 15 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index f9faf7b13..5394612a4 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -13,14 +13,17 @@ import com.google.common.base.Joiner; import com.google.common.collect.AbstractIterator; import com.google.common.collect.ImmutableList; +import com.google.common.collect.Lists; import com.google.errorprone.annotations.Immutable; import com.google.errorprone.annotations.Var; import java.io.InvalidObjectException; import java.io.ObjectInputStream; import java.io.Serial; import java.io.Serializable; -import java.util.Iterator; +import java.util.Arrays; import java.util.NoSuchElementException; +import java.util.stream.Collector; +import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; /** @@ -195,6 +198,41 @@ public String toString() { return "[" + Joiner.on(", ").join(asTopDownIterable()) + "]"; } + /** + * Returns a stack by pushing the arguments from left to right. The last argument is on top. + * + * @throws NullPointerException if an element or the varargs array is null + */ + @SafeVarargs + public static PersistentLinkedStack of(T first, T second, T... remaining) { + @Var PersistentLinkedStack result = of(first).pushAndCopy(second); + for (T value : remaining) { + result = result.pushAndCopy(value); + } + return result; + } + + /** + * Returns a stack by pushing the elements in iteration order. The last element is on top. + * + * @throws NullPointerException if {@code values} or an element is null + */ + public static PersistentLinkedStack copyOf(Iterable values) { + checkNotNull(values); + @Var PersistentLinkedStack result = of(); + for (T value : values) { + result = result.pushAndCopy(value); + } + return result; + } + + /** Returns a collector that pushes elements in encounter order, with the last element on top. */ + @SuppressWarnings("NoFunctionalReturnType") + public static Collector> toPersistentLinkedStack() { + return Collectors.collectingAndThen( + ImmutableList.toImmutableList(), PersistentLinkedStack::copyOf); + } + @Serial private Object writeReplace() { return new SerializationProxy(this); @@ -226,21 +264,14 @@ private SerializationProxy(PersistentLinkedStack stack) { @Serial private Object readResolve() throws InvalidObjectException { - @Nullable Object @Nullable [] serializedValues = values; - if (serializedValues == null) { - throw new InvalidObjectException("Stack values must not be null"); - } - - @Var PersistentLinkedStack stack = PersistentLinkedStack.of(); - // Push bottom-to-top to reconstruct the original iteration order. - for (@Var int index = serializedValues.length - 1; index >= 0; index--) { - @Nullable Object value = serializedValues[index]; - if (value == null) { - throw new InvalidObjectException("Stack values must not contain null"); - } - stack = stack.pushAndCopy(value); + try { + return PersistentLinkedStack.copyOf(Lists.reverse(Arrays.asList(checkNotNull(values)))); + } catch (NullPointerException e) { + InvalidObjectException exception = + new InvalidObjectException("Stack values must not be null or contain null"); + exception.initCause(e); + throw exception; } - return stack; } } From 98f9a57da0357a172ee6622dca89c8ca9e276de9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 00:53:17 +0200 Subject: [PATCH 12/16] Format PersistentStack --- src/org/sosy_lab/common/collect/PersistentStack.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java index 4efd5ed58..ee3194066 100644 --- a/src/org/sosy_lab/common/collect/PersistentStack.java +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -97,9 +97,9 @@ public interface PersistentStack extends Serializable { /** * Returns the hash code of this stack. * - *

The hash code is computed starting with {@code hash = 1} and applying - * {@code hash = 31 * hash + element.hashCode()} to each element in top-to-bottom order, using - * Java {@code int} arithmetic. The hash code of an empty stack is {@code 1}. + *

The hash code is computed starting with {@code hash = 1} and applying {@code hash = 31 * + * hash + element.hashCode()} to each element in top-to-bottom order, using Java {@code int} + * arithmetic. The hash code of an empty stack is {@code 1}. * * @return the hash code of this stack */ From 7a1918c8641f5c4664dd1165d1dbdec1d326aabf Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 01:03:43 +0200 Subject: [PATCH 13/16] Add method takeBottom(int) that allows to take n elements from the bottom of the PersistentStack --- .../common/collect/PersistentLinkedStack.java | 15 +++++++++++++++ .../sosy_lab/common/collect/PersistentStack.java | 8 ++++++++ 2 files changed, 23 insertions(+) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index 5394612a4..12a309dee 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -9,6 +9,7 @@ package org.sosy_lab.common.collect; import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkPositionIndex; import com.google.common.base.Joiner; import com.google.common.collect.AbstractIterator; @@ -198,6 +199,20 @@ public String toString() { return "[" + Joiner.on(", ").join(asTopDownIterable()) + "]"; } + @Override + public PersistentLinkedStack takeBottom(int count) { + checkPositionIndex(count, size); + if (count == 0) { + return of(); + } + + @Var PersistentLinkedStack result = this; + while (result.size > count) { + result = result.popAndCopy(); + } + return result; + } + /** * Returns a stack by pushing the arguments from left to right. The last argument is on top. * diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java index ee3194066..be8b1b2f2 100644 --- a/src/org/sosy_lab/common/collect/PersistentStack.java +++ b/src/org/sosy_lab/common/collect/PersistentStack.java @@ -80,6 +80,14 @@ public interface PersistentStack extends Serializable { /** Returns an unmodifiable bottom-to-top list in O(n) time and space. */ List copyToList(); + /** + * Returns a stack containing the bottom {@code count} elements. + * + * @throws IndexOutOfBoundsException if {@code count} is outside {@code [0, size()]} + */ + @CheckReturnValue + PersistentStack takeBottom(int count); + /** * Returns {@code true} if and only if {@code obj} is a {@link PersistentStack} with the same * number of elements and equal corresponding elements in top-to-bottom order. Elements are From 4d8056a6bd41183a9db776630a208f357f0e7fb9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 01:04:26 +0200 Subject: [PATCH 14/16] Improve readResolve() in PersistentLinkedStack --- .../common/collect/PersistentLinkedStack.java | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index 12a309dee..dbb3b6594 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -279,14 +279,21 @@ private SerializationProxy(PersistentLinkedStack stack) { @Serial private Object readResolve() throws InvalidObjectException { - try { - return PersistentLinkedStack.copyOf(Lists.reverse(Arrays.asList(checkNotNull(values)))); - } catch (NullPointerException e) { - InvalidObjectException exception = - new InvalidObjectException("Stack values must not be null or contain null"); - exception.initCause(e); - throw exception; + @Nullable Object @Nullable [] serializedValues = values; + if (serializedValues == null) { + throw new InvalidObjectException("Stack values must not be null"); } + + @Var PersistentLinkedStack stack = PersistentLinkedStack.of(); + // The serialized order is top-to-bottom; push in the opposite direction. + for (@Var int index = serializedValues.length - 1; index >= 0; index--) { + @Nullable Object value = serializedValues[index]; + if (value == null) { + throw new InvalidObjectException("Stack values must not contain null"); + } + stack = stack.pushAndCopy(value); + } + return stack; } } From 8cac22c83b70c8d0d2c492d7edf68dc24e739648 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 01:07:16 +0200 Subject: [PATCH 15/16] Format PersistentLinkedStack --- src/org/sosy_lab/common/collect/PersistentLinkedStack.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java index dbb3b6594..a337fd33a 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java @@ -14,14 +14,12 @@ import com.google.common.base.Joiner; import com.google.common.collect.AbstractIterator; import com.google.common.collect.ImmutableList; -import com.google.common.collect.Lists; import com.google.errorprone.annotations.Immutable; import com.google.errorprone.annotations.Var; import java.io.InvalidObjectException; import java.io.ObjectInputStream; import java.io.Serial; import java.io.Serializable; -import java.util.Arrays; import java.util.NoSuchElementException; import java.util.stream.Collector; import java.util.stream.Collectors; From 5e8a49ab1ba6343cf94f91c578e6f0075523fb7e Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 01:22:33 +0200 Subject: [PATCH 16/16] Refactor PersistentLinkedList as a delegate of PersistentLinkedStack --- .../common/collect/PersistentLinkedList.java | 374 ++++++------------ 1 file changed, 120 insertions(+), 254 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedList.java b/src/org/sosy_lab/common/collect/PersistentLinkedList.java index c0bbc5f23..b5de8f002 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedList.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedList.java @@ -9,9 +9,9 @@ package org.sosy_lab.common.collect; import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkPositionIndex; import static com.google.common.base.Preconditions.checkState; -import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; import com.google.common.collect.UnmodifiableListIterator; @@ -20,221 +20,158 @@ import com.google.errorprone.annotations.InlineMe; import com.google.errorprone.annotations.Var; import java.util.AbstractSequentialList; +import java.util.ArrayList; import java.util.Arrays; import java.util.Comparator; -import java.util.EnumSet; import java.util.Iterator; import java.util.List; import java.util.ListIterator; import java.util.NoSuchElementException; -import java.util.Objects; -import java.util.Set; -import java.util.function.BiConsumer; -import java.util.function.BinaryOperator; -import java.util.function.Function; -import java.util.function.Supplier; import java.util.function.UnaryOperator; import java.util.stream.Collector; +import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; /** - * A single-linked-list implementation of {@link PersistentList}. Null values are not supported - * (similarly to {@link ImmutableList}). + * A {@link PersistentList} backed by a {@link PersistentLinkedStack}. List order is top-to-bottom + * stack order. Null elements are not supported. * - *

Adding to the front of the list needs only O(1) time and memory. + *

Prepending, head access, tail access, and size take O(1) time. Updates share unchanged stack + * nodes. * - *

This implementation supports almost all operations, except for the {@link - * ListIterator#hasPrevious()} and {@link ListIterator#previous()} methods of its list iterator. - * This means you cannot traverse this list in reverse order. + *

List iterators support forward traversal only; {@link ListIterator#hasPrevious()} and {@link + * ListIterator#previous()} are unsupported. * - *

All instances of this class are fully-thread safe. However, note that each modifying operation - * allocates a new instance whose reference needs to be published safely in order to be usable by - * other threads. Two concurrent accesses to a modifying operation on the same instance will create - * two new maps, each reflecting exactly the operation executed by the current thread, and not - * reflecting the operation executed by the other thread. + *

The list structure is immutable and thread-safe. Elements are not copied; iterator instances + * have no thread-safety guarantee. + * + * @param the type of elements */ @Immutable(containerOf = "T") @SuppressWarnings({ "deprecation", // javac complains about deprecated methods from PersistentList - "Immutable", // AbstractList.modCount is mutable but safe + "Immutable", // AbstractList.modCount is mutable but unused }) public final class PersistentLinkedList extends AbstractSequentialList implements PersistentList { - private final @Nullable T head; // only null for the empty list - private final @Nullable PersistentLinkedList tail; // only null for the empty list + private static final PersistentLinkedList EMPTY = + new PersistentLinkedList<>(PersistentLinkedStack.of()); - private PersistentLinkedList(@Nullable T head, @Nullable PersistentLinkedList tail) { - this.head = head; - this.tail = tail; - } + private final PersistentStack stack; - @SuppressWarnings("rawtypes") - private static final PersistentLinkedList EMPTY = makeEmpty(); + private PersistentLinkedList(PersistentStack pStack) { + stack = checkNotNull(pStack); + } - @SuppressWarnings({"rawtypes", "unchecked"}) - private static PersistentLinkedList makeEmpty() { - return new PersistentLinkedList(null, null); + private static PersistentLinkedList fromStack(PersistentStack stack) { + return stack.isEmpty() ? of() : new PersistentLinkedList<>(stack); } - /** - * Returns the empty list. - * - * @return The empty list - */ - @SuppressWarnings("unchecked") + /** Returns the empty list. */ + @SuppressWarnings("unchecked") // The empty list contains no elements. public static PersistentLinkedList of() { - return EMPTY; + return (PersistentLinkedList) EMPTY; } - /** - * Returns a list containing the specified value. - * - * @return A list containing the specified value - */ + /** Returns a list containing the given element. */ public static PersistentLinkedList of(T value) { - checkNotNull(value); - return new PersistentLinkedList<>(value, PersistentLinkedList.of()); + return new PersistentLinkedList<>(PersistentLinkedStack.of(value)); } - /** - * Returns a list containing the specified values. - * - * @return A list containing the specified values - */ + /** Returns a list containing the given elements in argument order. */ public static PersistentLinkedList of(T v1, T v2) { return of(v2).with(v1); } - /** - * Returns a list containing the specified values. - * - * @return A list containing the specified values - */ + /** Returns a list containing the given elements in argument order. */ public static PersistentLinkedList of(T v1, T v2, T v3) { return of(v3).with(v2).with(v1); } - /** - * Returns a list containing the specified values. - * - * @return A list containing the specified values - */ - @SuppressWarnings("unchecked") + /** Returns a list containing the given elements in argument order. */ + @SafeVarargs + @SuppressWarnings("varargs") // The array is only read and is not retained. public static PersistentLinkedList of(T v1, T... values) { return copyOf(values).with(v1); } - /** - * Returns a list containing the specified values. - * - * @return A list containing the specified values - */ - @SuppressWarnings("unchecked") + /** Returns a list containing the given elements in array order. */ + @SafeVarargs + @SuppressWarnings("varargs") // The array is only read and is not retained. public static PersistentLinkedList copyOf(T... values) { return copyOf(Arrays.asList(values)); } /** - * Returns A new list with the values from the Iterable. - * - * @return A new list with the values from the Iterable + * Returns a list in iteration order, reusing {@code values} if it is a {@code + * PersistentLinkedList}. */ public static PersistentLinkedList copyOf(List values) { - if (values instanceof PersistentLinkedList) { - return (PersistentLinkedList) values; - } - @Var PersistentLinkedList result = PersistentLinkedList.of(); - for (T value : Lists.reverse(values)) { - result = result.with(value); + if (values instanceof PersistentLinkedList list) { + return list; } - return result; + return PersistentLinkedList.of().withAll(values); } /** - * Returns the value at the start of the list for non-empty lists. + * Returns the first element. * - * @throws NoSuchElementException if the list is empty. - * @return The value at the start of the list + * @throws NoSuchElementException if this list is empty */ public T head() { - if (isEmpty()) { - throw new NoSuchElementException(); - } else { - return head; - } + return stack.peek(); } /** - * Returns the remainder of the list without the first element for non-empty lists. + * Returns the list without its first element, sharing the remaining stack nodes. * - * @throws IllegalStateException if the list is empty. - * @return The remainder of the list without the first element + * @throws IllegalStateException if this list is empty */ public PersistentLinkedList tail() { checkState(!isEmpty()); - return tail; + return fromStack(stack.popAndCopy()); } - /** - * Returns a new list with value as the head and the old list as the tail. - * - * @return A new list with value as the head and the old list as the tail - */ + /** Returns a list with {@code value} prepended in O(1) time and space. */ @Override public PersistentLinkedList with(T value) { - checkNotNull(value); - return new PersistentLinkedList<>(value, this); + return fromStack(stack.pushAndCopy(value)); } - /** - * Returns a new list with values as the head and the old list as the tail. - * - * @return A new list with value sas the head and the old list as the tail - */ + /** Returns a list with {@code values} prepended in their iteration order. */ @Override - public PersistentLinkedList withAll(@Var List values) { - @Var PersistentLinkedList result = this; - if (values instanceof PersistentLinkedList) { - // does not support listIterator() and thus fails on Lists.reverse() - values = ImmutableList.copyOf(values); + public PersistentLinkedList withAll(List values) { + if (values.isEmpty()) { + return this; } - for (T value : Lists.reverse(values)) { - result = result.with(value); + @Var PersistentStack result = stack; + // A snapshot also supports inputs whose list iterators cannot traverse backwards. + for (T value : ImmutableList.copyOf(values).reverse()) { + result = result.pushAndCopy(value); } - return result; + return fromStack(result); } - /** - * Returns a new list omitting the specified value. Note: O(N) - * - * @return A new list omitting the specified value - */ + /** Returns a list without the first occurrence of {@code value}, or this list if absent. */ @Override public PersistentLinkedList without(@Nullable T value) { - @Var PersistentLinkedList suffix = of(); // remainder of list after value - - // find position of value and update suffix - @Var int pos = 0; - for (PersistentLinkedList list = this; !list.isEmpty(); list = list.tail) { - if (Objects.equals(value, list.head)) { - suffix = list.tail; - break; - } - pos++; + int index = indexOf(value); + if (index < 0) { + return this; } - // get start of list until value - // into a separate list so we can iterate in reverse - ImmutableList prefix = FluentIterable.from(this).limit(pos).toList(); - - // concatenate prefix and suffix - @Var PersistentLinkedList result = suffix; - for (T v : prefix.reverse()) { - result = result.with(v); + List prefix = new ArrayList<>(index); + @Var PersistentStack result = stack; + for (int i = 0; i < index; i++) { + prefix.add(result.peek()); + result = result.popAndCopy(); } - - return result; + result = result.popAndCopy(); + for (T element : Lists.reverse(prefix)) { + result = result.pushAndCopy(element); + } + return fromStack(result); } @Override @@ -242,82 +179,90 @@ public PersistentLinkedList empty() { return of(); } - /** - * Returns the number of elements in the list. Note: O(N) - * - * @return The number of elements in the list - */ + /** Returns the number of elements in O(1) time. */ @Override public int size() { - @Var int size = 0; - for (PersistentLinkedList list = this; !list.isEmpty(); list = list.tail) { - ++size; - } - return size; + return stack.size(); } @Override - @SuppressWarnings("ReferenceEquality") // singleton instance public boolean isEmpty() { - return this == EMPTY; + return stack.isEmpty(); } - /** - * Returns a new list with the elements in the reverse order. This operation runs in O(n). - * - * @return A new list with the elements in the reverse order - */ + /** Returns a list in reverse order in O(n) time and space. */ @Override public PersistentLinkedList reversed() { - @Var PersistentLinkedList result = empty(); - for (PersistentLinkedList p = this; !p.isEmpty(); p = p.tail) { - result = result.with(p.head); - } - return result; + return fromStack(PersistentLinkedStack.copyOf(stack.asTopDownIterable())); } @Override public Iterator iterator() { - return new Iter<>(this); + return stack.asTopDownIterable().iterator(); } @Override public ListIterator listIterator(int index) { - if (index < 0) { - throw new IndexOutOfBoundsException(); - } - ListIterator it = new Iter<>(this); + checkPositionIndex(index, size()); + ListIterator result = new Iter<>(iterator()); for (int i = 0; i < index; i++) { - if (!it.hasNext()) { - throw new IndexOutOfBoundsException(); - } - it.next(); + result.next(); } - return it; + return result; + } + + /** Returns a collector that collects elements in reverse encounter order. */ + @SuppressWarnings("NoFunctionalReturnType") + public static Collector> toPersistentLinkedList() { + return Collectors.collectingAndThen( + PersistentLinkedStack.toPersistentLinkedStack(), PersistentLinkedList::fromStack); + } + + /** + * Returns a collector that collects elements in reverse encounter order. + * + * @deprecated use {@link #toPersistentLinkedList()} + */ + @Deprecated + @InlineMe( + replacement = "PersistentLinkedList.toPersistentLinkedList()", + imports = "org.sosy_lab.common.collect.PersistentLinkedList") + public static Collector> collector() { + return toPersistentLinkedList(); + } + + @Deprecated + @Override + @DoNotCall + public void replaceAll(UnaryOperator pOperator) { + throw new UnsupportedOperationException(); + } + + @Deprecated + @Override + @DoNotCall + public void sort(Comparator pComparator) { + throw new UnsupportedOperationException(); } private static final class Iter extends UnmodifiableListIterator { - private PersistentLinkedList list; + private final Iterator delegate; private int nextIndex = 0; - private Iter(PersistentLinkedList list) { - this.list = list; + private Iter(Iterator pDelegate) { + delegate = pDelegate; } @Override public boolean hasNext() { - return !list.isEmpty(); + return delegate.hasNext(); } @Override public T next() { - if (list.isEmpty()) { - throw new NoSuchElementException(); - } + T result = delegate.next(); nextIndex++; - T result = list.head; - list = list.tail; return result; } @@ -341,83 +286,4 @@ public T previous() { throw new UnsupportedOperationException(); } } - - /** - * Return a {@link Collector} that creates PersistentLinkedLists and can be used in {@link - * java.util.stream.Stream#collect(Collector)}. The returned collector does not support parallel - * streams. - */ - @SuppressWarnings("NoFunctionalReturnType") - public static Collector> toPersistentLinkedList() { - return new Collector, PersistentLinkedList>() { - - @Override - public Supplier> supplier() { - return PersistentLinkedListBuilder::new; - } - - @Override - public BiConsumer, T> accumulator() { - return PersistentLinkedListBuilder::add; - } - - @Override - public BinaryOperator> combiner() { - return (a, b) -> { - throw new UnsupportedOperationException("Should be used sequentially"); - }; - } - - @Override - public Function, PersistentLinkedList> finisher() { - return PersistentLinkedListBuilder::build; - } - - @Override - public Set characteristics() { - return EnumSet.noneOf(Characteristics.class); - } - }; - } - - /** - * Return a {@link Collector} that creates PersistentLinkedLists and can be used in {@link - * java.util.stream.Stream#collect(Collector)}. The returned collector does not support parallel - * streams. - * - * @deprecated renamed to {@link #toPersistentLinkedList()} to conform with Guava's naming - */ - @Deprecated - @InlineMe( - replacement = "PersistentLinkedList.toPersistentLinkedList()", - imports = "org.sosy_lab.common.collect.PersistentLinkedList") - public static Collector> collector() { - return toPersistentLinkedList(); - } - - private static final class PersistentLinkedListBuilder { - private PersistentLinkedList list = PersistentLinkedList.of(); - - void add(T e) { - list = list.with(e); - } - - PersistentLinkedList build() { - return list; - } - } - - @Deprecated - @Override - @DoNotCall - public void replaceAll(UnaryOperator pOperator) { - throw new UnsupportedOperationException(); - } - - @Deprecated - @Override - @DoNotCall - public void sort(Comparator pC) { - throw new UnsupportedOperationException(); - } }