Iterator infrastructure for collection models: snapshot iterators + generic-element annotation

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();
+    }
+}
+

src/main/java/org/cprover/CProverGenericArrayElement.java

@@ -0,0 +1,51 @@
+/*
+ * Field-level annotation for modeled-collection backing
+ * arrays whose element type is logically the enclosing
+ * class's generic K (or V, E, ...) parameter, but which
+ * Java's type erasure forces to declare as Object[].
+ *
+ * Example: in an array-backed map model that stores keys and
+ * values in parallel {@code Object[]} arrays,
+ *
+ *     @CProverGenericArrayElement("K")
+ *     private Object[] keys;
+ *
+ *     @CProverGenericArrayElement("V")
+ *     private Object[] values;
+ *
+ * tells JBMC's object factory that, when nondet-initializing
+ * a {@code HashMap<Integer, SpecValue>} instance, the
+ * keys[] elements should be allocated as {@code Integer}
+ * instances and the values[] elements as {@code SpecValue}
+ * instances — rather than as generic {@code Object}
+ * instances which won't match {@code .equals(Integer.valueOf(n))}
+ * in containsKey(...).
+ *
+ * Without this annotation, lemmas with preconditions like
+ * {@code precondition(map.containsKey(absN))} are vacuously
+ * SUCCESSFUL because the factory cannot generate a satisfying
+ * keys[i].equals(Integer.valueOf(absN)) state — it allocates
+ * keys[i] as a base Object, which has no {@code value} field
+ * and whose {@code @class_identifier} is not "Integer".
+ *
+ * @see CProverArrayLikeIterator
+ */
+package org.cprover;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.FIELD)
+public @interface CProverGenericArrayElement {
+    /**
+     * Simple name of the enclosing class's generic type
+     * parameter whose specialization should be used as the
+     * element type of the annotated array. For
+     * {@code class HashMap<K, V> { @CProverGenericArrayElement("K")
+     * private Object[] keys; }}, the value is {@code "K"}.
+     */
+    String value();
+}

src/main/java/org/cprover/CProverMapEntry.java

@@ -0,0 +1,77 @@
+package org.cprover;
+
+import java.util.Map;
+
+/**
+ * Snapshot {@link Map.Entry} implementation for map models.
+ *
+ * <p>Intended usage: a map model that stores keys and values in
+ * parallel {@code Object[]} arrays and needs {@code entrySet()} to
+ * expose a {@code Set<Map.Entry<K, V>>} constructs one entry per
+ * (keys[i], values[i]) pair. That gives the model a deterministic,
+ * iterable view without depending on the JDK's
+ * {@code AbstractMap.SimpleEntry} (whose body, like everything
+ * else in {@code AbstractMap}, JBMC stubs out).
+ *
+ * <p>This entry is deliberately {@code final} and read-only:
+ * {@code setValue} calls {@link CProver#notModelled()}. Most
+ * production map iteration doesn't mutate via the entry; a target
+ * that needs {@code setValue} calls for a separate mutable entry
+ * class holding a write-through reference to the map's storage,
+ * mirroring the mutable-iterator path described in
+ * {@link CProverArrayLikeIterator}.
+ *
+ * @param <K> key type.
+ * @param <V> value type.
+ */
+public final class CProverMapEntry<K, V> implements Map.Entry<K, V> {
+
+    private final K key;
+    private final V value;
+
+    public CProverMapEntry(K key, V value) {
+        this.key = key;
+        this.value = value;
+    }
+
+    @Override
+    public K getKey() {
+        return key;
+    }
+
+    @Override
+    public V getValue() {
+        return value;
+    }
+
+    @Override
+    public V setValue(V newValue) {
+        // Snapshot entries don't write back to the underlying
+        // map. Targets that need entry-driven mutation can
+        // subclass; the common read-only iteration case is fine.
+        CProver.notModelled();
+        return value;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (!(o instanceof Map.Entry)) {
+            return false;
+        }
+        Map.Entry<?, ?> other = (Map.Entry<?, ?>) o;
+        Object ok = other.getKey();
+        Object ov = other.getValue();
+        boolean keyEq = (key == null) ? (ok == null) : key.equals(ok);
+        boolean valEq = (value == null) ? (ov == null) : value.equals(ov);
+        return keyEq && valEq;
+    }
+
+    @Override
+    public int hashCode() {
+        // Java's Map.Entry contract: XOR of key.hashCode() and
+        // value.hashCode(), with null hashCode treated as 0.
+        int kh = (key == null) ? 0 : key.hashCode();
+        int vh = (value == null) ? 0 : value.hashCode();
+        return kh ^ vh;
+    }
+}