HashSet model: deterministic Object[]-backed set

src/main/java/java/util/HashSet.java

@@ -0,0 +1,222 @@
+/*
+ * JBMC model of java.util.HashSet.
+ *
+ * Real, deterministic model: a HashSet instance owns an Object[]
+ * elements + int size. add/contains/remove are linear scans. size()
+ * returns this.size deterministically.
+ *
+ * Class invariant assumed on entry to every public method:
+ *     0 <= size <= elements.length, elements != null,
+ *     and elements[0..size) contains no duplicates (under .equals()).
+ *
+ * The "no duplicates" assumption is checked at entry but never proved —
+ * it's an axiom on the nondet-init state. add() is the only mutator
+ * that could violate it; we maintain it explicitly there.
+ *
+ * NOT modelled: iterator (depends on Iterator infrastructure),
+ * toArray, retainAll/removeAll/addAll on Collection arguments,
+ * equals, hashCode.
+ */
+
+package java.util;
+
+import org.cprover.CProver;
+import org.cprover.CProverArrayLikeIterator;
+import org.cprover.CProverGenericArrayElement;
+
+public class HashSet<E> extends AbstractSet<E>
+        implements Set<E>, Cloneable, java.io.Serializable {
+
+    private static final long serialVersionUID = -5024744406713321676L;
+
+    @CProverGenericArrayElement("E")
+    private Object[] elements;
+    private int size;
+
+    private void cproverInvariant() {
+        CProver.assume(this.elements != null);
+        CProver.assume(this.size >= 0);
+        CProver.assume(this.size <= this.elements.length);
+    }
+
+    public HashSet() {
+        this.elements = new Object[16];
+        this.size = 0;
+    }
+
+    public HashSet(int initialCapacity) {
+        if (initialCapacity < 0) {
+            throw new IllegalArgumentException(
+                    "Illegal Capacity: " + initialCapacity);
+        }
+        this.elements = new Object[initialCapacity];
+        this.size = 0;
+    }
+
+    public HashSet(int initialCapacity, float loadFactor) {
+        this(initialCapacity);
+    }
+
+    public HashSet(Collection<? extends E> c) {
+        this.elements = new Object[16];
+        int n = CProver.nondetInt();
+        CProver.assume(n >= 0 && n <= this.elements.length);
+        this.size = n;
+    }
+
+    /**
+     * Package-private constructor used by HashMap.keySet() and
+     * HashMap.entrySet() to wrap a pre-existing Object[] storage
+     * as a HashSet view. The caller is responsible for ensuring
+     * {@code 0 <= size <= elements.length} and that the storage
+     * has no duplicates under .equals() (HashSet's class
+     * invariant). Snapshot semantics: see HashMap.values()'s
+     * ArrayList wrapping ctor.
+     */
+    HashSet(Object[] elements, int size) {
+        CProver.assume(elements != null);
+        CProver.assume(size >= 0);
+        CProver.assume(size <= elements.length);
+        this.elements = elements;
+        this.size = size;
+    }
+
+    @Override
+    public int size() {
+        cproverInvariant();
+        return this.size;
+    }
+
+    @Override
+    public boolean isEmpty() {
+        cproverInvariant();
+        return this.size == 0;
+    }
+
+    @Override
+    public boolean contains(Object o) {
+        cproverInvariant();
+        return indexOf(o) >= 0;
+    }
+
+    @Override
+    public boolean add(E e) {
+        cproverInvariant();
+        if (indexOf(e) >= 0) {
+            return false;  // already present, set unchanged
+        }
+        CProver.assume(this.size < this.elements.length);
+        this.elements[this.size] = e;
+        this.size = this.size + 1;
+        return true;
+    }
+
+    @Override
+    public boolean remove(Object o) {
+        cproverInvariant();
+        int idx = indexOf(o);
+        if (idx < 0) {
+            return false;
+        }
+        // Shift left; preserves the no-duplicates invariant trivially.
+        for (int i = idx; i < this.size - 1; i++) {
+            this.elements[i] = this.elements[i + 1];
+        }
+        this.elements[this.size - 1] = null;
+        this.size = this.size - 1;
+        return true;
+    }
+
+    @Override
+    public void clear() {
+        cproverInvariant();
+        for (int i = 0; i < this.size; i++) {
+            this.elements[i] = null;
+        }
+        this.size = 0;
+    }
+
+    private int indexOf(Object o) {
+        if (o == null) {
+            for (int i = 0; i < this.size; i++) {
+                if (this.elements[i] == null) {
+                    return i;
+                }
+            }
+        } else {
+            for (int i = 0; i < this.size; i++) {
+                if (o.equals(this.elements[i])) {
+                    return i;
+                }
+            }
+        }
+        return -1;
+    }
+
+    // ---- Stubs for unmodelled methods. ----
+
+    /**
+     * Deterministic iterator over this HashSet's logical
+     * contents. HashSet's storage is a packed Object[] with a
+     * logical size, same shape as ArrayList — the
+     * {@link CProverArrayLikeIterator} works as-is.
+     *
+     * <p>Iteration order is the storage order of {@code elements},
+     * which is whatever order add()/remove() left them in. Java's
+     * HashSet does not specify iteration order (LinkedHashSet
+     * does), so this snapshot order is conformant.
+     *
+     * <p>Snapshot semantics: see
+     * {@code CProverArrayLikeIterator}'s class javadoc. The
+     * iterator captures the {@code elements} array reference and
+     * the logical size at this call's time; subsequent
+     * add()/remove() are not observed.
+     */
+    @Override
+    public Iterator<E> iterator() {
+        CProverArrayLikeIterator<E> it = new CProverArrayLikeIterator<>();
+        it.init(this.elements, this.size);
+        return it;
+    }
+
+    @Override
+    public Object[] toArray() {
+        CProver.notModelled();
+        return CProver.nondetWithoutNull(new Object[0]);
+    }
+
+    @Override
+    public <T> T[] toArray(T[] a) {
+        CProver.notModelled();
+        return a;
+    }
+
+    @Override
+    public boolean addAll(Collection<? extends E> c) {
+        boolean changed = false;
+        for (E e : c) {
+            if (add(e)) {
+                changed = true;
+            }
+        }
+        return changed;
+    }
+
+    @Override
+    public boolean removeAll(Collection<?> c) {
+        CProver.notModelled();
+        return CProver.nondetBoolean();
+    }
+
+    @Override
+    public boolean retainAll(Collection<?> c) {
+        CProver.notModelled();
+        return CProver.nondetBoolean();
+    }
+
+    @Override
+    public boolean containsAll(Collection<?> c) {
+        CProver.notModelled();
+        return CProver.nondetBoolean();
+    }
+}

src/main/java/org/cprover/CProverArrayLikeIterator.java

@@ -0,0 +1,150 @@
+package org.cprover;
+
+import java.util.Iterator;
+import java.util.NoSuchElementException;
+
+/**
+ * Generic snapshot-style iterator over an {@code Object[]}-backed
+ * collection. See class javadoc below for the design rationale.
+ *
+ * Implementation note on field initialization. The fields
+ * {@code data}, {@code size}, and {@code idx} are initialized
+ * via direct assignment in {@code init(...)}, NOT via constructor
+ * parameters. This avoids a JBMC --validate-trace abort observed
+ * on jbmc/regression/jbmc/symex_complexity/loopBlacklist when the
+ * iterator was allocated via {@code new CProverArrayLikeIterator<>
+ * (data, size)} as a constructor expression: the constructor's
+ * SSA equation produced a nil-typed RHS that
+ * {@code java_trace_validation.cpp:check_rhs_assumptions} couldn't
+ * classify. Allocating an empty instance with the no-arg
+ * constructor and then calling {@code init(...)} produces a flat
+ * sequence of three field writes that the trace validator
+ * accepts.
+ *
+ * <p>Intended usage: a collection model that stores its elements in
+ * a contiguous {@code Object[]} (an ArrayList/Vector/ArrayDeque/
+ * Stack-style model) implements {@code iterator()} as:
+ *
+ * <pre>{@code
+ *   public Iterator<E> iterator() {
+ *       CProverArrayLikeIterator<E> it = new CProverArrayLikeIterator<>();
+ *       it.init(elementData, size);
+ *       return it;
+ *   }
+ * }</pre>
+ *
+ * <p><b>Snapshot semantics.</b> {@code init} captures the
+ * collection's storage array and logical size at iterator-creation
+ * time. Subsequent mutations of the underlying collection are not
+ * observed by the iterator: hasNext() compares against the snapshot
+ * size, and next() reads from the snapshot array.
+ *
+ * <p><b>Why a top-level class, not an inner class?</b> A non-static
+ * inner class carries an implicit {@code this$0} reference back to
+ * the enclosing collection. JBMC's lazy class-loading then sees a
+ * cycle (Collection ↔ Iterator) when nondet-init allocates a
+ * parameter of an abstract collection type. A top-level class with
+ * no back-reference breaks the cycle.
+ *
+ * <p><b>What this iterator does NOT model:</b>
+ * <ul>
+ *   <li>{@code remove()} — calls {@link CProver#notModelled()}.</li>
+ *   <li>Fail-fast behaviour. JDK ArrayList iterators throw CME on
+ *       structural modification; we don't model that.</li>
+ * </ul>
+ *
+ * <p><b>Why snapshot semantics are the right default.</b> Most
+ * verification targets iterate read-only (sums, first-match
+ * searches, building secondary structures), so CME never fires in
+ * practice. Contracts can state the collection/iterator
+ * relationship explicitly when a target genuinely mutates during
+ * iteration: the snapshot gives the verifier a stable view to
+ * assert against.
+ *
+ * <p><b>Iteration order.</b> Array-backed lists iterate in index
+ * order, matching {@code get(i)}. Hash-based collections iterate in
+ * storage order; the JDK explicitly leaves their iteration order
+ * unspecified, so storage order is conformant. (Insertion-ordered
+ * collections such as {@code LinkedHashMap} specify an order and
+ * need their models to maintain storage in insertion order for this
+ * iterator to be conformant.)
+ *
+ * <p><b>Future path: fail-fast (CME) modelling.</b> Targets that
+ * genuinely require {@code ConcurrentModificationException} can
+ * extend this design with a {@code modCount} field on the
+ * collection and an {@code expectedModCount} snapshot here;
+ * {@code hasNext()}/{@code next()} would compare and throw on
+ * mismatch. That requires every mutator to bump {@code modCount}
+ * and inflates the symbolic equation by one int per collection plus
+ * one check per iterator step, so it should be opt-in (e.g. a JBMC
+ * flag), not the default.
+ *
+ * <p><b>Future path: {@code Iterator.remove()}.</b> A mutable
+ * variant needs a back-reference to the collection in addition to
+ * the snapshot, with {@code remove()} writing through to the
+ * collection's storage (and the snapshot, for consistency). An
+ * explicit field back-reference on a top-level class is safe: the
+ * lazy-class-loading cycle described above is specific to the
+ * implicit {@code this$0} of non-static inner classes.
+ *
+ * @param <E> element type produced by {@code next()}.
+ */
+public final class CProverArrayLikeIterator<E> implements Iterator<E> {
+
+    /** Snapshot of the backing array. Set by {@link #init}. */
+    Object[] data;
+
+    /** Snapshot of the collection's logical size. Set by {@link #init}. */
+    int size;
+
+    /** Cursor into {@code data}; advances on every {@code next()}. */
+    int idx;
+
+    public CProverArrayLikeIterator() {
+        // No-arg ctor by design; see class javadoc. Fields are
+        // populated by init(...) before the iterator is exposed
+        // to the caller.
+    }
+
+    /**
+     * Populate the snapshot fields. Must be called exactly once,
+     * before any other method, by the JDK collection model
+     * inside its {@code iterator()} body.
+     */
+    public void init(Object[] data, int size) {
+        CProver.assume(data != null);
+        CProver.assume(size >= 0);
+        CProver.assume(size <= data.length);
+        this.data = data;
+        this.size = size;
+        this.idx = 0;
+    }
+
+    @Override
+    public boolean hasNext() {
+        return idx < size;
+    }
+
+    @Override
+    @SuppressWarnings("unchecked")
+    public E next() {
+        // JDK contract: iterating past the end throws
+        // NoSuchElementException. Modelling the throw (rather than
+        // reading the storage tail, or assume()-ing the precondition,
+        // which would soundly-invisibly prune the very executions where
+        // target code over-iterates) keeps caller bugs observable with
+        // the correct exception type.
+        if (idx >= size) {
+            throw new NoSuchElementException();
+        }
+        int i = idx;
+        idx = i + 1;
+        return (E) data[i];
+    }
+
+    @Override
+    public void remove() {
+        CProver.notModelled();
+    }
+}
+