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

+ * + *

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