From 7b301ed4776fd2c4c6f3a28878e1a7b1378cab68 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Jul 2026 22:50:26 +0000 Subject: [PATCH 1/2] Iterator infrastructure for collection models: snapshot iterators + generic-element annotation Three top-level org.cprover support classes for collection models' iterator()/enhanced-for support. They are inert until collection models reference them (none in this repo do yet -- the javadoc describes intended usage); landing them separately keeps the model changes reviewable. - CProverArrayLikeIterator: generic snapshot iterator over an Object[]-backed collection; captures (storage, size) at iterator() time. Top-level rather than an inner class deliberately: a non-static inner class's implicit this$0 creates a Collection <-> Iterator lazy-class-loading cycle that aborts JBMC's nondet initialisation of abstract collection parameters. The class javadoc carries the full design rationale (snapshot-vs-fail-fast trade-off, iteration-order conformance, and the documented opt-in future paths for CME modelling and Iterator.remove()). next() past the end throws NoSuchElementException per the JDK contract. An assume() guard on the precondition would be unsound here: it would prune exactly the executions in which target code over-iterates, hiding those bugs behind vacuously-passing paths; modelling the throw keeps them observable with the correct exception type. - CProverMapEntry: read-only snapshot Map.Entry for entrySet() views of parallel-array map models. Deliberately final; entry-driven mutation calls for a separate write-through entry class (documented), not subclassing. - @CProverGenericArrayElement: marks an Object[] field as holding a model class's generic-parameter elements, so JBMC's nondet object factory can specialise the element type. Co-authored-by: Kiro --- .../org/cprover/CProverArrayLikeIterator.java | 150 ++++++++++++++++++ .../cprover/CProverGenericArrayElement.java | 51 ++++++ .../java/org/cprover/CProverMapEntry.java | 77 +++++++++ 3 files changed, 278 insertions(+) create mode 100644 src/main/java/org/cprover/CProverArrayLikeIterator.java create mode 100644 src/main/java/org/cprover/CProverGenericArrayElement.java create mode 100644 src/main/java/org/cprover/CProverMapEntry.java diff --git a/src/main/java/org/cprover/CProverArrayLikeIterator.java b/src/main/java/org/cprover/CProverArrayLikeIterator.java new file mode 100644 index 0000000..ec9ca88 --- /dev/null +++ b/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. + * + *

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: + * + * 

{@code
+ *   public Iterator iterator() {
+ *       CProverArrayLikeIterator it = new CProverArrayLikeIterator<>();
+ *       it.init(elementData, size);
+ *       return it;
+ *   }
+ * }
+ * + *

Snapshot semantics. {@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. + * + *

Why a top-level class, not an inner class? 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. + * + *

What this iterator does NOT model: + *

    + *
  • {@code remove()} — calls {@link CProver#notModelled()}.
    • + *
  • Fail-fast behaviour. JDK ArrayList iterators throw CME on + * structural modification; we don't model that.
    • + *
+ * + *

Why snapshot semantics are the right default. 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. + * + *

Iteration order. 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.) + * + *

Future path: fail-fast (CME) modelling. 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. + * + *

Future path: {@code Iterator.remove()}. 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 element type produced by {@code next()}. + */ +public final class CProverArrayLikeIterator implements Iterator { + + /** 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(); + } +} + diff --git a/src/main/java/org/cprover/CProverGenericArrayElement.java b/src/main/java/org/cprover/CProverGenericArrayElement.java new file mode 100644 index 0000000..c216c9c --- /dev/null +++ b/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} 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 { @CProverGenericArrayElement("K") + * private Object[] keys; }}, the value is {@code "K"}. + */ + String value(); +} diff --git a/src/main/java/org/cprover/CProverMapEntry.java b/src/main/java/org/cprover/CProverMapEntry.java new file mode 100644 index 0000000..5d8d242 --- /dev/null +++ b/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. + * + *

Intended usage: a map model that stores keys and values in + * parallel {@code Object[]} arrays and needs {@code entrySet()} to + * expose a {@code Set>} 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). + * + *

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 key type. + * @param value type. + */ +public final class CProverMapEntry implements Map.Entry { + + 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; + } +} From ed2267b57be6d4385b796f9abe4082717d34037e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 00:28:25 +0000 Subject: [PATCH 2/2] HashSet model: deterministic Object[]-backed set Executable model of java.util.HashSet over a duplicate-free Object[] prefix: add/remove/contains/size/isEmpty/clear, addAll/removeAll/ retainAll/containsAll, toArray, and iterator() via CProverArrayLikeIterator (snapshot semantics). Iteration is storage order, conformant with HashSet's unspecified-order contract. Null elements are supported per the JDK. A package-private wrapping constructor exposes a pre-existing storage prefix so map models can build keySet()/entrySet() views without copying. Co-authored-by: Kiro --- src/main/java/java/util/HashSet.java | 222 +++++++++++++++++++++++++++ 1 file changed, 222 insertions(+) create mode 100644 src/main/java/java/util/HashSet.java diff --git a/src/main/java/java/util/HashSet.java b/src/main/java/java/util/HashSet.java new file mode 100644 index 0000000..94e30ea --- /dev/null +++ b/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 extends AbstractSet + implements Set, 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 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. + * + *

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. + * + *

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 iterator() { + CProverArrayLikeIterator 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[] toArray(T[] a) { + CProver.notModelled(); + return a; + } + + @Override + public boolean addAll(Collection 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(); + } +}