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 aabe58f11ce70ac05c604f41e0db188b60acb9b2 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 20 Sep 2026 01:47:23 +0200 Subject: [PATCH 16/16] Refactor PersistentLinkedStackTest and use Guava testlib + a new PersistentStack impl for hashcode and equals tests --- .../collect/PersistentLinkedStackTest.java | 515 +++++++++++++----- 1 file changed, 368 insertions(+), 147 deletions(-) diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java index e22bbbba4..40acc6767 100644 --- a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java +++ b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java @@ -11,239 +11,460 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.testing.IteratorFeature; +import com.google.common.collect.testing.IteratorTester; +import com.google.common.collect.testing.ListTestSuiteBuilder; +import com.google.common.collect.testing.TestStringListGenerator; +import com.google.common.collect.testing.features.CollectionFeature; +import com.google.common.collect.testing.features.CollectionSize; +import com.google.common.testing.CollectorTester; import com.google.common.testing.EqualsTester; import com.google.common.testing.SerializableTester; +import com.google.errorprone.annotations.Immutable; import com.google.errorprone.annotations.Var; +import java.io.ByteArrayInputStream; +import java.io.ByteArrayOutputStream; +import java.io.IOException; +import java.io.InvalidObjectException; +import java.io.NotSerializableException; +import java.io.ObjectInputStream; +import java.io.ObjectOutputStream; +import java.io.Serial; import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Arrays; import java.util.Iterator; +import java.util.List; import java.util.NoSuchElementException; +import java.util.stream.Stream; +import junit.framework.JUnit4TestAdapter; +import junit.framework.TestSuite; +import org.checkerframework.checker.nullness.qual.Nullable; import org.junit.Test; public class PersistentLinkedStackTest { - @Test - public void testEmptyFactory() { - PersistentStack stack = PersistentLinkedStack.of(); - - assertThat(stack.isEmpty()).isTrue(); + private static final ImmutableList> INPUTS = + ImmutableList.of( + ImmutableList.of(), + ImmutableList.of("a"), + ImmutableList.of("a", "b", "c"), + ImmutableList.of("", "", "b")); + + public static junit.framework.Test suite() { + TestSuite suite = new TestSuite(); + suite.addTest(new JUnit4TestAdapter(PersistentLinkedStackTest.class)); + suite.addTest( + ListTestSuiteBuilder.using( + new TestStringListGenerator() { + @Override + protected ImmutableList create(String[] pElements) { + @Var PersistentLinkedStack stack = PersistentLinkedStack.of(); + for (String element : pElements) { + stack = stack.pushAndCopy(element); + } + return stack.copyToList(); + } + }) + .named("PersistentLinkedStack.copyToList") + .withFeatures(CollectionFeature.KNOWN_ORDER, CollectionSize.ANY) + .createTestSuite()); + return suite; } @Test - public void testSingletonFactory() { - PersistentStack stack = PersistentLinkedStack.of("value"); - - assertThat(stack.isEmpty()).isFalse(); - assertThat(stack.asTopDownIterable()).containsExactly("value"); + public void testIterator() { + for (ImmutableList input : INPUTS) { + PersistentStack stack = pushAll(input); + Iterable view = stack.asTopDownIterable(); + IteratorTester tester = + new IteratorTester<>( + 5, + IteratorFeature.UNMODIFIABLE, + input.reverse(), + IteratorTester.KnownOrder.KNOWN_ORDER) { + @Override + protected Iterator newTargetIterator() { + return view.iterator(); + } + }; + tester.test(); + tester.testForEachRemaining(); + } } @Test - public void testPushAndCopy() { - PersistentStack empty = PersistentLinkedStack.of(); - PersistentStack stack = empty.pushAndCopy("value"); - - assertThat(stack.peek()).isEqualTo("value"); - assertThat(empty.asTopDownIterable()).isEmpty(); - assertThat(empty.isEmpty()).isTrue(); + public void testForEachRemainingBoundaryCases() { + List remaining = new ArrayList<>(); + Iterator iterator = PersistentLinkedStack.of("a").asTopDownIterable().iterator(); + iterator.forEachRemaining(remaining::add); + assertThat(remaining).containsExactly("a"); + + remaining.clear(); + iterator.forEachRemaining(remaining::add); + PersistentLinkedStack.of() + .asTopDownIterable() + .iterator() + .forEachRemaining(remaining::add); + assertThat(remaining).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()); + public void testIteratorsAreIndependent() { + Iterable view = pushAll(ImmutableList.of("a", "b")).asTopDownIterable(); + Iterator first = view.iterator(); + Iterator second = view.iterator(); + + assertThat(first.next()).isEqualTo("b"); + assertThat(second.next()).isEqualTo("b"); + assertThat(first.next()).isEqualTo("a"); + assertThat(second.next()).isEqualTo("a"); } @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); + public void testViewsRemainOnOriginalVersion() { + PersistentStack stack = pushAll(ImmutableList.of("a", "b")); + Iterable view = stack.asTopDownIterable(); + List copy = stack.copyToList(); + PersistentStack extended = stack.pushAndCopy("c"); + + assertThat(extended.peek()).isEqualTo("c"); + assertThat(view).containsExactly("b", "a").inOrder(); + assertThat(copy).containsExactly("a", "b").inOrder(); } @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); + public void testPersistentVersions() { + for (ImmutableList input : INPUTS) { + List> versions = new ArrayList<>(); + versions.add(PersistentLinkedStack.of()); + for (String value : input) { + versions.add(versions.get(versions.size() - 1).pushAndCopy(value)); + } + + for (int i = 0; i < versions.size(); i++) { + PersistentStack version = versions.get(i); + assertThat(version.size()).isEqualTo(i); + assertThat(version.isEmpty()).isEqualTo(i == 0); + assertThat(version.asTopDownIterable()) + .containsExactlyElementsIn(input.subList(0, i).reverse()) + .inOrder(); + if (i > 0) { + assertThat(version.peek()).isEqualTo(input.get(i - 1)); + assertThat(version.popAndCopy()).isSameInstanceAs(versions.get(i - 1)); + } + } + } } @Test - public void testPopReturnsSamePredecessor() { - PersistentStack predecessor = - PersistentLinkedStack.of().pushAndCopy("bottom").pushAndCopy("middle"); - PersistentStack stack = predecessor.pushAndCopy("top"); - - assertThat(stack.popAndCopy()).isSameInstanceAs(predecessor); + public void testBranchesSharePredecessor() { + PersistentStack predecessor = pushAll(ImmutableList.of("bottom", "middle")); + PersistentStack left = predecessor.pushAndCopy("left"); + PersistentStack right = predecessor.pushAndCopy("right"); + + assertThat(left.peek()).isEqualTo("left"); + assertThat(right.peek()).isEqualTo("right"); + assertThat(left.popAndCopy()).isSameInstanceAs(predecessor); + assertThat(right.popAndCopy()).isSameInstanceAs(predecessor); + assertThat(predecessor.asTopDownIterable()).containsExactly("middle", "bottom").inOrder(); } @Test - public void testPeekEmptyThrows() { + public void testCanonicalEmpty() { PersistentStack empty = PersistentLinkedStack.of(); + PersistentStack singleton = PersistentLinkedStack.of("a"); - assertThrows(NoSuchElementException.class, empty::peek); + assertThat(empty.isEmpty()).isTrue(); + assertThat(empty.size()).isEqualTo(0); + assertThat(PersistentLinkedStack.of()).isSameInstanceAs(empty); + assertThat(empty.empty()).isSameInstanceAs(empty); + assertThat(singleton.empty()).isSameInstanceAs(empty); + assertThat(singleton.popAndCopy()).isSameInstanceAs(empty); + assertThat(PersistentLinkedStack.copyOf(ImmutableList.of())).isSameInstanceAs(empty); + assertThat(Stream.empty().collect(PersistentLinkedStack.toPersistentLinkedStack())) + .isSameInstanceAs(empty); } @Test - public void testPopEmptyThrows() { + public void testEmptyOperationsThrow() { PersistentStack empty = PersistentLinkedStack.of(); + assertThrows(NoSuchElementException.class, empty::peek); 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); + public void testOfFactories() { + assertThat(PersistentLinkedStack.of("a").asTopDownIterable()).containsExactly("a"); + assertThat(PersistentLinkedStack.of("a", "b").asTopDownIterable()) + .containsExactly("b", "a") + .inOrder(); + assertThat(PersistentLinkedStack.of("a", "b", "c", "d").asTopDownIterable()) + .containsExactly("d", "c", "b", "a") + .inOrder(); } @Test - public void testCanonicalEmpty() { - PersistentStack empty = PersistentLinkedStack.of(); - PersistentStack singleton = PersistentLinkedStack.of("value"); + public void testArrayIsOneElement() { + String[] value = {"a", "b"}; + PersistentStack stack = PersistentLinkedStack.of(value); - assertThat(PersistentLinkedStack.of()).isSameInstanceAs(empty); - assertThat(singleton.empty()).isSameInstanceAs(empty); - assertThat(singleton.popAndCopy()).isSameInstanceAs(empty); + assertThat(stack.size()).isEqualTo(1); + assertThat(stack.peek()).isSameInstanceAs(value); + assertThat(stack.asTopDownIterable().iterator().next()).isSameInstanceAs(value); } @Test - public void testRejectsNull() { - PersistentStack empty = PersistentLinkedStack.of(); + public void testCopyOf() { + for (ImmutableList input : INPUTS) { + PersistentStack stack = PersistentLinkedStack.copyOf(input); - assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of((String) null)); - assertThrows(NullPointerException.class, () -> empty.pushAndCopy(null)); - assertThrows( - NullPointerException.class, () -> PersistentLinkedStack.of("value").pushAndCopy(null)); + assertThat(stack.size()).isEqualTo(input.size()); + assertThat(stack.asTopDownIterable()).containsExactlyElementsIn(input.reverse()).inOrder(); + } } @Test - public void testIteratorOrderIsTopToBottom() { - PersistentStack stack = - PersistentLinkedStack.of() - .pushAndCopy("bottom") - .pushAndCopy("middle") - .pushAndCopy("top"); + public void testCopyOfDoesNotRetainInput() { + List input = new ArrayList<>(ImmutableList.of("a", "b")); + PersistentStack stack = PersistentLinkedStack.copyOf(input); + input.clear(); - assertThat(stack.asTopDownIterable()).containsExactly("top", "middle", "bottom").inOrder(); + assertThat(stack.asTopDownIterable()).containsExactly("b", "a").inOrder(); + assertThat(stack.size()).isEqualTo(2); } @Test - public void testIteratorExhaustion() { - Iterator iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator(); - - assertThat(iterator.next()).isEqualTo("value"); - assertThrows(NoSuchElementException.class, iterator::next); + public void testCollector() { + CollectorTester> tester = + CollectorTester.of(PersistentLinkedStack.toPersistentLinkedStack()); + for (ImmutableList input : INPUTS) { + tester.expectCollects(pushAll(input), input.toArray(new String[0])); + } } @Test - public void testIteratorRemoveRejected() { - Iterator iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator(); + public void testNulls() { + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of((String) null)); + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of(null, "a")); + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of("a", null)); + assertThrows( + NullPointerException.class, () -> PersistentLinkedStack.of("a", "b", (String[]) null)); + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.copyOf(null)); + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of().pushAndCopy(null)); + assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of("a").pushAndCopy(null)); + } - assertThrows(UnsupportedOperationException.class, iterator::remove); + @Test + public void testNullElements() { + assertThrows( + NullPointerException.class, () -> PersistentLinkedStack.of("a", "b", (String) null)); + assertThrows( + NullPointerException.class, + () -> PersistentLinkedStack.copyOf(Arrays.asList("a", null, "b"))); + assertThrows( + NullPointerException.class, + () -> Stream.of("a", null, "b").collect(PersistentLinkedStack.toPersistentLinkedStack())); } @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"); + public void testEquals() { + PersistentStack tail = PersistentLinkedStack.of("bottom"); + BigInteger value = new BigInteger("123456789012345678901234567890"); + BigInteger equalValue = new BigInteger("123456789012345678901234567890"); new EqualsTester() - .addEqualityGroup(stack, independentlyBuilt) - .addEqualityGroup(differentOrder) - .addEqualityGroup(differentMiddle) - .addEqualityGroup(differentBottom) - .addEqualityGroup(shorter) + .addEqualityGroup(PersistentLinkedStack.of(), new ListStack<>(ImmutableList.of())) + .addEqualityGroup(PersistentLinkedStack.of("a"), new ListStack<>(ImmutableList.of("a"))) + .addEqualityGroup( + tail.pushAndCopy("middle").pushAndCopy("top"), + tail.pushAndCopy("middle").pushAndCopy("top"), + pushAll(ImmutableList.of("bottom", "middle", "top")), + new ListStack<>(ImmutableList.of("top", "middle", "bottom"))) + .addEqualityGroup(tail.pushAndCopy("middle").pushAndCopy("other")) + .addEqualityGroup(tail.pushAndCopy("other").pushAndCopy("top")) + .addEqualityGroup(pushAll(ImmutableList.of("other", "middle", "top"))) + .addEqualityGroup(pushAll(ImmutableList.of("top", "middle", "bottom"))) + .addEqualityGroup(tail.pushAndCopy("top")) + .addEqualityGroup( + pushAll(ImmutableList.of("a", "a")), new ListStack<>(ImmutableList.of("a", "a"))) + .addEqualityGroup( + PersistentLinkedStack.of(value), + PersistentLinkedStack.of(equalValue), + new ListStack<>(ImmutableList.of(equalValue))) + .addEqualityGroup(ImmutableList.of("top", "middle", "bottom")) .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"); + public void testToString() { + assertThat(PersistentLinkedStack.of().toString()).isEqualTo("[]"); + assertThat(PersistentLinkedStack.of("a").toString()).isEqualTo("[a]"); + assertThat(pushAll(ImmutableList.of("bottom", "middle", "top")).toString()) + .isEqualTo("[top, middle, bottom]"); + } - new EqualsTester().addEqualityGroup(stack, equal).addEqualityGroup(different).testEquals(); + @Test + public void testSerializable() { + for (ImmutableList input : INPUTS) { + PersistentStack stack = pushAll(input); + @Var PersistentStack copy = SerializableTester.reserializeAndAssert(stack); + + assertThat(copy.size()).isEqualTo(input.size()); + for (String value : input.reverse()) { + assertThat(copy.peek()).isEqualTo(value); + copy = copy.popAndCopy(); + } + assertThat(copy).isSameInstanceAs(PersistentLinkedStack.of()); + } } @Test - public void testToString() { - PersistentStack empty = PersistentLinkedStack.of(); - PersistentStack stack = - PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top"); + public void testLongStackSerialization() { + int length = 10_000; + @Var PersistentStack stack = PersistentLinkedStack.of(); + for (int i = 0; i < length; i++) { + stack = stack.pushAndCopy(i); + } + @Var PersistentStack copy = SerializableTester.reserializeAndAssert(stack); - assertThat(empty.toString()).isEqualTo("[]"); - assertThat(stack.toString()).isEqualTo("[top, middle, bottom]"); + for (int i = length - 1; i >= 0; i--) { + assertThat(copy.size()).isEqualTo(i + 1); + assertThat(copy.peek()).isEqualTo(i); + copy = copy.popAndCopy(); + } + assertThat(copy).isSameInstanceAs(PersistentLinkedStack.of()); } @Test - public void testSerializationRoundTrip() { - PersistentStack stack = - PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top"); + public void testSerializationRejectsNonSerializableElement() throws IOException { + try (ObjectOutputStream output = new ObjectOutputStream(new ByteArrayOutputStream())) { + assertThrows( + NotSerializableException.class, + () -> output.writeObject(PersistentLinkedStack.of(new Object()))); + } + } - SerializableTester.reserializeAndAssert(stack); + @Test + public void testSerializationRejectsNullArray() { + assertThrows(InvalidObjectException.class, () -> reserializeWithProxyValues(null)); } @Test - public void testEmptySerializationReturnsCanonicalInstance() { - PersistentStack empty = PersistentLinkedStack.of(); + public void testSerializationRejectsNullElement() { + assertThrows( + InvalidObjectException.class, + () -> reserializeWithProxyValues(new Object[] {"top", null, "bottom"})); + } - assertThat(SerializableTester.reserialize(empty)).isSameInstanceAs(empty); + private static PersistentLinkedStack pushAll(Iterable input) { + @Var PersistentLinkedStack stack = PersistentLinkedStack.of(); + for (T value : input) { + stack = stack.pushAndCopy(value); + } + return stack; } - @Test - public void testLongStackSerializationRoundTrip() { - int length = 10_000; - @Var PersistentStack stack = PersistentLinkedStack.of(); - for (int i = 0; i < length; i++) { - stack = stack.pushAndCopy(i); + // The string-only fixture has exactly one object array: the proxy's element array. + @SuppressWarnings("BanSerializableRead") // Reads only locally generated test data. + private static Object reserializeWithProxyValues(@Nullable Object @Nullable [] values) + throws IOException, ClassNotFoundException { + ByteArrayOutputStream bytes = new ByteArrayOutputStream(); + try (ObjectOutputStream output = + new ObjectOutputStream(bytes) { + { + enableReplaceObject(true); + } + + @Override + protected @Nullable Object replaceObject(Object object) { + return object instanceof Object[] ? values : object; + } + }) { + output.writeObject(PersistentLinkedStack.of("value")); + } + try (ObjectInputStream input = + new ObjectInputStream(new ByteArrayInputStream(bytes.toByteArray()))) { + return input.readObject(); + } + } + + /** Independent value-based implementation used only for equality and hash-code tests. */ + @Immutable(containerOf = "T") + private static final class ListStack implements PersistentStack { + + @Serial private static final long serialVersionUID = 1L; + + private final ImmutableList values; + + private ListStack(ImmutableList pValues) { + values = pValues; } - assertThat(SerializableTester.reserialize(stack)).isEqualTo(stack); + @Override + public PersistentStack pushAndCopy(T value) { + return new ListStack<>(ImmutableList.builder().add(value).addAll(values).build()); + } + + @Override + public PersistentStack popAndCopy() { + if (isEmpty()) { + throw new NoSuchElementException(); + } + return new ListStack<>(values.subList(1, values.size())); + } + + @Override + public T peek() { + if (isEmpty()) { + throw new NoSuchElementException(); + } + return values.get(0); + } + + @Override + public PersistentStack empty() { + return new ListStack<>(ImmutableList.of()); + } + + @Override + public boolean isEmpty() { + return values.isEmpty(); + } + + @Override + public int size() { + return values.size(); + } + + @SuppressWarnings("PreferredInterfaceType") + @Override + public Iterable asTopDownIterable() { + return values; + } + + @Override + public ImmutableList copyToList() { + return values.reverse(); + } + + @Override + public PersistentStack takeBottom(int count) { + // Currently not needed in tests + throw new UnsupportedOperationException(); + } + + @Override + public boolean equals(@Nullable Object obj) { + return obj instanceof PersistentStack other + && values.equals(ImmutableList.copyOf(other.asTopDownIterable())); + } + + @Override + public int hashCode() { + return values.hashCode(); + } } }