From e0776fcc9484f2d733e5f7ba2b86a891b66e3996 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 7 Sep 2026 19:14:37 +0200 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 4/4] 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); + } +}