diff --git a/axiomatic/README.md b/axiomatic/README.md new file mode 100644 index 0000000..a43d73a --- /dev/null +++ b/axiomatic/README.md @@ -0,0 +1,50 @@ +# Axiomatic Models Library — opt-in JBMC collections + +This module provides an alternative implementation of +`java.util.HashMap`, `java.util.HashSet`, and `java.util.LinkedHashMap` +for use with JBMC. Compared to `core-models.jar`, these implementations +are **axiomatic**: a HashMap is a single direct-mapped `Object[CAPACITY]` +table (`h(k) = hashCode & MASK`) with `CProver.assume`-based invariants, +designed so that lemma-style verification over large or symbolic maps +avoids the core models' per-entry storage and scan loops. + +## Selection mechanism (validated) + +Put `axiomatic-models.jar` **before** `core-models.jar` on the JBMC +classpath; JBMC's class loader resolves each class to its first +occurrence, so the axiomatic classes shadow the core ones: + +```bash +jbmc --function MyClass.lemma \ + -cp target/classes:axiomatic-models.jar:core-models.jar:cprover-api.jar \ + MyClass +``` + +Verified against a stock JBMC with the sibling +`verification-benchmarks/run.sh` (which accepts a colon-joined models +path, so a core-vs-axiomatic comparison is one command per jar order). + +## Semantic trade-offs — READ BEFORE USE + +These models deliberately deviate from the JDK in ways that are fine +for their intended niche (contracts/lemma verification over maps used +as key-value stores) and WRONG for general-purpose verification: + +* **Null values are not representable**: `put(k, null)` is + indistinguishable from absence (`containsKey` tests `kv[slot] != null`). + Code storing null values gets wrong definite answers. +* **Hash collisions silently overwrite**: two present keys with + `hashCode() & MASK` equal corrupt each other. Wrong definite answers, + not sound nondeterminism. +* **Views are ghost objects**: `keySet()`/`values()`/`entrySet()` + return skolemizing views whose iterators yield nondet elements + constrained to be in the map. Properties over concrete iteration + contents or order can become VACUOUSLY provable — the sibling + benchmark suite demonstrates a false property "verifying" this way + (`OrderProbes.removeReorders_f`). Do not use these models when the + target code iterates and the property depends on the iteration. +* **LinkedHashMap does not model its specified iteration order.** + +For general-purpose verification use `core-models.jar` alone; its +HashMap/HashSet/LinkedHashMap are JDK-conformant (including null +values, collision handling, and iteration order). diff --git a/axiomatic/pom.xml b/axiomatic/pom.xml new file mode 100644 index 0000000..2b84b2d --- /dev/null +++ b/axiomatic/pom.xml @@ -0,0 +1,75 @@ + + 4.0.0 + + org.cprover.models + axiomatic-models + 1.0-SNAPSHOT + jar + + + UTF-8 + + + CProver Axiomatic JDK Models + + Opt-in JBMC model jar that replaces java.util.HashMap, HashSet, and + LinkedHashMap with axiomatic stubs backed by SMT-LIB array theory. + Used together with --axiomatic-collections. + + + + + java8-doclint-disabled + + [1.8,) + + + -Xdoclint:none + + + + + + + org.cprover.util + cprover-api + 1.0.0 + compile + + + + + axiomatic-models + + + maven-dependency-plugin + 2.8 + + + generate-sources + + build-classpath + + + maven.compile.classpath + + + + + + + org.apache.maven.plugins + maven-compiler-plugin + 3.6.1 + + + ${java.home}/lib/rt.jar${path.separator}${maven.compile.classpath} + + 1.8 + 1.8 + + + + + diff --git a/axiomatic/src/main/java/java/util/HashMap.java b/axiomatic/src/main/java/java/util/HashMap.java new file mode 100644 index 0000000..f5b6960 --- /dev/null +++ b/axiomatic/src/main/java/java/util/HashMap.java @@ -0,0 +1,244 @@ +/* + * Axiomatic JBMC model of java.util.HashMap. + * + * Trades the parallel-arrays + linear-scan implementation in + * core-models.jar for a single hash-indexed Object[]. CBMC's + * array theory translates the get / put operations into single + * select / store SMT terms, eliminating the inner unwind loops + * that dominate verification time for Map-heavy lemmas. + * + * put(k, v): kv[h(k)] = v; if was null, sz++ + * get(k): return kv[h(k)] + * containsKey: return kv[h(k)] != null + * + * where h(k) = (k == null ? 0 : k.hashCode()) & MASK. + * + *

Limitations

+ * + * + * + *

Design rationale

+ * + * The class deliberately AVOIDS any explicit init loop. The + * {@code kv} array is allocated by JBMC's + * {@link remove_java_new} pass as a single zero-initialised + * struct ASSIGN — no per-slot loop is emitted. Adding an + * explicit fill loop here would force CBMC to unroll + * {@code CAPACITY} times, defeating the speedup. + */ +package java.util; + +import org.cprover.AxiomaticEntrySetView; +import org.cprover.AxiomaticKeySetView; +import org.cprover.AxiomaticValuesView; +import org.cprover.CProver; + +public class HashMap implements Map { + + /** + * Hash-table capacity. Power of two so {@code & MASK} is + * a valid modulus. Set high enough that collisions are + * effectively impossible for typed keys with good hashCode + * distributions. Raising this number does NOT cost unwinds + * in CBMC's array theory; the array is symbolic. + */ + static final int CAPACITY = 1024; + static final int MASK = CAPACITY - 1; + + /** + * The hash table. Naturally null-initialised by JBMC's + * {@code java_new_array} lowering — no explicit fill loop. + */ + Object[] kv; + + /** Mapping count. Maintained explicitly by put / remove. */ + int sz; + + private void cproverInvariant() { + CProver.assume(this.kv != null); + CProver.assume(this.kv.length == CAPACITY); + CProver.assume(this.sz >= 0); + CProver.assume(this.sz <= CAPACITY); + } + + public HashMap() { + this.kv = new Object[CAPACITY]; + this.sz = 0; + } + + public HashMap(int initialCapacity) { + if (initialCapacity < 0) { + throw new IllegalArgumentException( + "Illegal initial capacity: " + initialCapacity); + } + // initialCapacity is ignored; CAPACITY is constant. + this.kv = new Object[CAPACITY]; + this.sz = 0; + } + + public HashMap(int initialCapacity, float loadFactor) { + this(initialCapacity); + } + + public HashMap(Map m) { + this.kv = new Object[CAPACITY]; + if (m instanceof HashMap) { + @SuppressWarnings("unchecked") + HashMap hm = + (HashMap) m; + CProver.assume(hm.kv != null); + CProver.assume(hm.kv.length == CAPACITY); + // Whole-array assignment: CBMC array theory + // collapses this to a single SMT array term. + this.kv = hm.kv; + this.sz = hm.sz; + } else { + int n = m.size(); + CProver.assume(n >= 0 && n <= CAPACITY); + this.sz = n; + } + } + + /** Hash a key to a slot index. */ + private static int slot(Object key) { + return (key == null ? 0 : key.hashCode()) & MASK; + } + + @Override + public int size() { + cproverInvariant(); + return this.sz; + } + + @Override + public boolean isEmpty() { + cproverInvariant(); + return this.sz == 0; + } + + @SuppressWarnings("unchecked") + @Override + public V get(Object key) { + cproverInvariant(); + return (V) this.kv[slot(key)]; + } + + @Override + public boolean containsKey(Object key) { + cproverInvariant(); + return this.kv[slot(key)] != null; + } + + @SuppressWarnings("unchecked") + @Override + public V put(K key, V value) { + cproverInvariant(); + int i = slot(key); + Object old = this.kv[i]; + this.kv[i] = value; + if (old == null) { + this.sz = this.sz + 1; + return null; + } + return (V) old; + } + + @SuppressWarnings("unchecked") + @Override + public V remove(Object key) { + cproverInvariant(); + int i = slot(key); + Object old = this.kv[i]; + if (old == null) { + return null; + } + this.kv[i] = null; + this.sz = this.sz - 1; + return (V) old; + } + + @Override + public void clear() { + cproverInvariant(); + // Allocate a fresh null-initialised array. Avoids an + // explicit fill loop (see Design rationale). + this.kv = new Object[CAPACITY]; + this.sz = 0; + } + + @Override + public boolean containsValue(Object value) { + cproverInvariant(); + // The only method whose cost scales with CAPACITY. + // Avoid in hot specs. + for (int i = 0; i < CAPACITY; i++) { + Object v = this.kv[i]; + if (v == null) { + continue; + } + if (value == null ? false : value.equals(v)) { + return true; + } + } + return false; + } + + @Override + public void putAll(Map m) { + CProver.notModelled(); + } + + @Override + public Set keySet() { + // The skolemizing iterator yields fresh nondet keys + // constrained to be in the map. We wrap it in a + // ghost HashSet view; the only useful method on the + // returned Set is iterator(), which delegates here. + // If a user code touches other Set methods, they get + // the axiomatic HashSet's behaviour applied to a + // separate ghost set with no contents. + return new AxiomaticKeySetView(this); + } + + @Override + public Collection values() { + return new AxiomaticValuesView(this); + } + + @Override + public Set> entrySet() { + return new AxiomaticEntrySetView(this); + } + + @Override + public boolean equals(Object o) { + if (o == this) return true; + if (!(o instanceof Map)) return false; + CProver.notModelled(); + return false; + } + + @Override + public int hashCode() { + CProver.notModelled(); + return 0; + } + + @Override + public String toString() { + return "HashMap(axiomatic)"; + } +} diff --git a/axiomatic/src/main/java/java/util/HashSet.java b/axiomatic/src/main/java/java/util/HashSet.java new file mode 100644 index 0000000..76a873a --- /dev/null +++ b/axiomatic/src/main/java/java/util/HashSet.java @@ -0,0 +1,174 @@ +/* + * Axiomatic JBMC model of java.util.HashSet. + * + * Trades the parallel-array + linear-scan implementation in + * core-models.jar for a single hash-indexed boolean[] (encoded + * as Object[] to avoid a primitive-array specialisation). + * + * add(e): set kv[h(e)] = PRESENT; if was absent, sz++ + * contains(o): return kv[h(o)] == PRESENT + * remove(o): set kv[h(o)] = ABSENT; if was present, sz-- + * + * where h(o) = (o == null ? 0 : o.hashCode()) & MASK. + * + * Each operation is O(1). Compare with core-models, where add() + * + contains() + remove() each linear-scan up to size entries. + * + * Limitations: + * - Hash collisions silently merge entries. + * - Iteration order is not specified. + * - equals()/hashCode() are opaque (CProver.notModelled). + */ +package java.util; + +import org.cprover.AxiomaticSetIterator; +import org.cprover.CProver; + +public class HashSet extends AbstractSet + implements Set, Cloneable, java.io.Serializable { + + private static final long serialVersionUID = -5024744406713321676L; + + static final int CAPACITY = 1024; + static final int MASK = CAPACITY - 1; + + /** Per-slot occupancy. ABSENT = false, PRESENT = true. */ + boolean[] kv; + + /** Ghost size kept in sync. */ + int sz; + + private void cproverInvariant() { + CProver.assume(this.kv != null); + CProver.assume(this.kv.length == CAPACITY); + CProver.assume(this.sz >= 0); + CProver.assume(this.sz <= CAPACITY); + } + + private void initEmpty() { + this.kv = new boolean[CAPACITY]; + // boolean[] is zero-initialised (false) by JBMC's + // java_new_array lowering — no explicit fill loop. + this.sz = 0; + } + + public HashSet() { + initEmpty(); + } + + public HashSet(int initialCapacity) { + if (initialCapacity < 0) { + throw new IllegalArgumentException( + "Illegal Capacity: " + initialCapacity); + } + // initialCapacity is ignored; CAPACITY is constant. + initEmpty(); + } + + public HashSet(int initialCapacity, float loadFactor) { + this(initialCapacity); + } + + public HashSet(Collection c) { + initEmpty(); + if (c instanceof HashSet) { + HashSet hs = (HashSet) c; + CProver.assume(hs.kv != null); + CProver.assume(hs.kv.length == CAPACITY); + for (int i = 0; i < CAPACITY; i++) { + this.kv[i] = hs.kv[i]; + } + this.sz = hs.sz; + } else { + int n = c.size(); + CProver.assume(n >= 0 && n <= CAPACITY); + this.sz = n; + } + } + + /** Hash an element to a slot index. */ + private static int slot(Object o) { + return (o == null ? 0 : o.hashCode()) & MASK; + } + + @Override + public int size() { + cproverInvariant(); + return this.sz; + } + + @Override + public boolean isEmpty() { + cproverInvariant(); + return this.sz == 0; + } + + @Override + public boolean contains(Object o) { + cproverInvariant(); + return this.kv[slot(o)]; + } + + @Override + public boolean add(E e) { + cproverInvariant(); + int i = slot(e); + if (this.kv[i]) { + return false; + } + this.kv[i] = true; + this.sz = this.sz + 1; + return true; + } + + @Override + public boolean remove(Object o) { + cproverInvariant(); + int i = slot(o); + if (!this.kv[i]) { + return false; + } + this.kv[i] = false; + this.sz = this.sz - 1; + return true; + } + + @Override + public void clear() { + cproverInvariant(); + // Allocate a fresh false-initialised array. Avoids an + // explicit fill loop. + this.kv = new boolean[CAPACITY]; + this.sz = 0; + } + + @Override + public Iterator iterator() { + // Skolemizing iterator: hasNext() returns nondet, + // next() returns a nondet element constrained to be + // in this set (`set.contains(elem)`). JBMC's BMC + // explores all loop iteration counts up to the unwind + // bound; the loop body must hold for every consistent + // element the set contains. + return new AxiomaticSetIterator(this); + } + + @Override + public boolean equals(Object o) { + if (o == this) return true; + if (!(o instanceof Set)) return false; + CProver.notModelled(); + return false; + } + + @Override + public int hashCode() { + CProver.notModelled(); + return 0; + } + + @Override + public String toString() { + return "HashSet(axiomatic)"; + } +} diff --git a/axiomatic/src/main/java/java/util/LinkedHashMap.java b/axiomatic/src/main/java/java/util/LinkedHashMap.java new file mode 100644 index 0000000..2025cb1 --- /dev/null +++ b/axiomatic/src/main/java/java/util/LinkedHashMap.java @@ -0,0 +1,42 @@ +/* + * Axiomatic JBMC model of java.util.LinkedHashMap. + * + * Inherits HashMap's axiomatic encoding. Insertion-order + * preservation is NOT modelled — see "Limitations" below. + */ +package java.util; + +public class LinkedHashMap extends HashMap + implements Map { + + private static final long serialVersionUID = 3801124242820219131L; + + public LinkedHashMap() { + super(); + } + + public LinkedHashMap(int initialCapacity) { + super(initialCapacity); + } + + public LinkedHashMap(int initialCapacity, float loadFactor) { + super(initialCapacity); + } + + /** + * Limitation: the axiomatic encoding does + * not preserve insertion order or implement access-order + * (LRU) semantics. {@code accessOrder} is silently ignored. + * Lemmas whose correctness depends on iteration order MUST + * NOT use this model — fall back to core-models.jar by + * leaving {@code --axiomatic-collections} off. + */ + public LinkedHashMap( + int initialCapacity, float loadFactor, boolean accessOrder) { + super(initialCapacity); + } + + public LinkedHashMap(Map m) { + super(m); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticEntryIterator.java b/axiomatic/src/main/java/org/cprover/AxiomaticEntryIterator.java new file mode 100644 index 0000000..16b31a0 --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticEntryIterator.java @@ -0,0 +1,63 @@ +/* + * Skolemizing iterator for axiomatic HashMap.entrySet(). + * + * Each {@code next()} yields a synthetic + * {@code Map.Entry} whose key is fresh nondet and whose + * value is the result of {@code map.get(key)} — but with a + * `CProver.assume(map.containsKey(key))` so the SAT solver + * can only return entries that the map "has". + * + * {@code hasNext()} returns a fresh nondet boolean each call, + * so JBMC's BMC explores all loop iterations from 0 to the + * unwind bound. A property + * + * for (Map.Entry e : map.entrySet()) {{ assert P(e); }} + * + * is then checked under each iteration count: the loop body + * must hold for every consistent (key, value) pair the map + * contains. This is the standard skolemization of + * forall-over-entries that BMC can verify modulo unwind + * depth. + * + * Without this iterator, the for-each pattern hits an + * UnsupportedOperationException from the throwing entrySet() + * — see the class javadoc on + * {@link java.util.HashMap#entrySet()} (axiomatic version). + */ +package org.cprover; + +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; + +public final class AxiomaticEntryIterator + implements Iterator> { + + private HashMap map; + + public AxiomaticEntryIterator(HashMap m) { + this.map = m; + } + + @Override + public boolean hasNext() { + return CProver.nondetBoolean(); + } + + @Override + @SuppressWarnings("unchecked") + public Map.Entry next() { + K key = (K) CProver.nondetWithoutNullForNotModelled(); + // Skolemization: only return entries the map actually + // contains. Under axiomatic encoding this is + // _kv[pack(map, key_value)] != NULL. + CProver.assume(map.containsKey(key)); + V value = map.get(key); + return new AxiomaticMapEntry<>(key, value); + } + + @Override + public void remove() { + CProver.notModelled(); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticEntrySetView.java b/axiomatic/src/main/java/org/cprover/AxiomaticEntrySetView.java new file mode 100644 index 0000000..844203d --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticEntrySetView.java @@ -0,0 +1,43 @@ +/* + * Set view returned by {@code HashMap.entrySet()} under the + * axiomatic encoding. The only method the for-each idiom + * touches is {@code iterator()}; everything else delegates + * to nondet or throws. + */ +package org.cprover; + +import java.util.AbstractSet; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; + +public final class AxiomaticEntrySetView + extends AbstractSet> { + + private final HashMap map; + + public AxiomaticEntrySetView(HashMap m) { + this.map = m; + } + + @Override + public Iterator> iterator() { + return new AxiomaticEntryIterator<>(map); + } + + @Override + public int size() { + return map.size(); + } + + @Override + public boolean contains(Object o) { + // Defer to map.containsKey when the operand is an + // Entry. Otherwise nondet. + if(o instanceof Map.Entry) { + Map.Entry e = (Map.Entry) o; + return map.containsKey(e.getKey()); + } + return CProver.nondetBoolean(); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticInterpretation.java b/axiomatic/src/main/java/org/cprover/AxiomaticInterpretation.java new file mode 100644 index 0000000..c05b7ab --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticInterpretation.java @@ -0,0 +1,47 @@ +/* + * Marker annotation for methods whose semantics are encoded + * directly into CBMC GOTO IR rather than executed from + * bytecode. JBMC's java_bytecode_axiomatic pass walks + * function bodies and rewrites CALLs to annotated methods + * into the SMT-relevant operation named by `op`. + * + * Currently a no-op when --axiomatic-collections is not set. + * + * The Java method body provided in the model jar is a + * concrete fallback — JBMC ignores it when the lowering pass + * runs, but javac needs it to type-check and other JVM tools + * (test harnesses, IDEs) need it to load classes. + * + * Recognised values for `op`: + * + * "select" — receiver.kv[key] (returns the stored value) + * "store" — receiver.kv := store(receiver.kv, key, value) + * "contains_key" — receiver.kv[key] != UNSET sentinel + * "size" — receiver.size (ghost int) + * "is_empty" — receiver.size == 0 + * "remove" — receiver.kv[key] := UNSET; receiver.size-- + * "clear" — receiver.kv := empty array; receiver.size := 0 + * + * `array` and `sizeVar` parameters name the ghost members + * of the receiver. Default values match the conventions used + * by the axiomatic-models jar. + */ +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.METHOD) +public @interface AxiomaticInterpretation { + /** SMT-relevant operation name (see class javadoc). */ + String op(); + + /** Ghost-array field name on the receiver. */ + String array() default "kv"; + + /** Ghost-int field name on the receiver. */ + String sizeVar() default "size"; +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticKeySetView.java b/axiomatic/src/main/java/org/cprover/AxiomaticKeySetView.java new file mode 100644 index 0000000..3e20abb --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticKeySetView.java @@ -0,0 +1,45 @@ +package org.cprover; + +import java.util.AbstractSet; +import java.util.HashMap; +import java.util.Iterator; + +public final class AxiomaticKeySetView extends AbstractSet { + + private final HashMap map; + + public AxiomaticKeySetView(HashMap m) { + this.map = m; + } + + @Override + @SuppressWarnings("unchecked") + public Iterator iterator() { + // Same skolemization pattern as AxiomaticEntryIterator, + // but yielding only keys. + return new Iterator() { + @Override + public boolean hasNext() { + return CProver.nondetBoolean(); + } + + @Override + public K next() { + K key = (K) CProver.nondetWithoutNullForNotModelled(); + CProver.assume(map.containsKey(key)); + return key; + } + }; + } + + @Override + public int size() { + return map.size(); + } + + @Override + @SuppressWarnings("unchecked") + public boolean contains(Object o) { + return map.containsKey((K) o); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticMapEntry.java b/axiomatic/src/main/java/org/cprover/AxiomaticMapEntry.java new file mode 100644 index 0000000..d3a8465 --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticMapEntry.java @@ -0,0 +1,36 @@ +/* + * Read-only Map.Entry used by AxiomaticEntryIterator. + * Standalone (not depending on core-models.jar's + * org.cprover.CProverMapEntry) so the axiomatic jar can be + * used without core-models on the classpath. + */ +package org.cprover; + +import java.util.Map; + +public final class AxiomaticMapEntry implements Map.Entry { + + private final K key; + private final V value; + + public AxiomaticMapEntry(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 v) { + throw new UnsupportedOperationException( + "AxiomaticMapEntry is read-only"); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticSetIterator.java b/axiomatic/src/main/java/org/cprover/AxiomaticSetIterator.java new file mode 100644 index 0000000..346308f --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticSetIterator.java @@ -0,0 +1,40 @@ +/* + * Skolemizing iterator for axiomatic HashSet.iterator(). + * + * Same idea as {@link AxiomaticEntryIterator}: each call to + * {@code next()} returns a fresh nondet element constrained + * to be in the underlying set; {@code hasNext()} returns a + * fresh nondet boolean so BMC explores all iteration counts + * from 0 to the unwind bound. + */ +package org.cprover; + +import java.util.HashSet; +import java.util.Iterator; + +public final class AxiomaticSetIterator implements Iterator { + + private HashSet set; + + public AxiomaticSetIterator(HashSet s) { + this.set = s; + } + + @Override + public boolean hasNext() { + return CProver.nondetBoolean(); + } + + @Override + @SuppressWarnings("unchecked") + public E next() { + E elem = (E) CProver.nondetWithoutNullForNotModelled(); + CProver.assume(set.contains(elem)); + return elem; + } + + @Override + public void remove() { + CProver.notModelled(); + } +} diff --git a/axiomatic/src/main/java/org/cprover/AxiomaticValuesView.java b/axiomatic/src/main/java/org/cprover/AxiomaticValuesView.java new file mode 100644 index 0000000..bd1e30a --- /dev/null +++ b/axiomatic/src/main/java/org/cprover/AxiomaticValuesView.java @@ -0,0 +1,41 @@ +package org.cprover; + +import java.util.AbstractCollection; +import java.util.HashMap; +import java.util.Iterator; + +public final class AxiomaticValuesView extends AbstractCollection { + + private final HashMap map; + + public AxiomaticValuesView(HashMap m) { + this.map = m; + } + + @Override + @SuppressWarnings("unchecked") + public Iterator iterator() { + return new Iterator() { + @Override + public boolean hasNext() { + return CProver.nondetBoolean(); + } + + @Override + public V next() { + // Skolemize: pick a nondet KEY in the map, + // return its corresponding value. We don't + // expose the key publicly; callers see only + // the value. + Object key = CProver.nondetWithoutNullForNotModelled(); + CProver.assume(((HashMap) map).containsKey(key)); + return ((HashMap) map).get(key); + } + }; + } + + @Override + public int size() { + return map.size(); + } +}