/*

* Copyright (c) 1997, 2013, Oracle and/or its affiliates. All rights reserved.

* DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.

*

* This code is free software; you can redistribute it and/or modify it

* under the terms of the GNU General Public License version 2 only, as

* published by the Free Software Foundation. Oracle designates this

* particular file as subject to the "Classpath" exception as provided

* by Oracle in the LICENSE file that accompanied this code.

*

* This code is distributed in the hope that it will be useful, but WITHOUT

* ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or

* FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License

* version 2 for more details (a copy is included in the LICENSE file that

* accompanied this code).

*

* You should have received a copy of the GNU General Public License version

* 2 along with this work; if not, write to the Free Software Foundation,

* Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.

*

* Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA

* or visit www.oracle.com if you need additional information or have any

* questions.

*/

package java.util;

import java.io.IOException;

import java.io.InvalidObjectException;

import java.io.Serializable;

import java.lang.reflect.ParameterizedType;

import java.lang.reflect.Type;

import java.util.function.BiConsumer;

import java.util.function.BiFunction;

import java.util.function.Consumer;

import java.util.function.Function;

import org.cprover.CProver;

/**

* Hash table based implementation of the <tt>Map</tt> interface. This

* implementation provides all of the optional map operations, and permits

* <tt>null</tt> values and the <tt>null</tt> key. (The <tt>HashMap</tt>

* class is roughly equivalent to <tt>Hashtable</tt>, except that it is

* unsynchronized and permits nulls.) This class makes no guarantees as to

* the order of the map; in particular, it does not guarantee that the order

* will remain constant over time.

*

* <p>This implementation provides constant-time performance for the basic

* operations (<tt>get</tt> and <tt>put</tt>), assuming the hash function

* disperses the elements properly among the buckets. Iteration over

* collection views requires time proportional to the "capacity" of the

* <tt>HashMap</tt> instance (the number of buckets) plus its size (the number

* of key-value mappings). Thus, it's very important not to set the initial

* capacity too high (or the load factor too low) if iteration performance is

* important.

*

* <p>An instance of <tt>HashMap</tt> has two parameters that affect its

* performance: <i>initial capacity</i> and <i>load factor</i>. The

* <i>capacity</i> is the number of buckets in the hash table, and the initial

* capacity is simply the capacity at the time the hash table is created. The

* <i>load factor</i> is a measure of how full the hash table is allowed to

* get before its capacity is automatically increased. When the number of

* entries in the hash table exceeds the product of the load factor and the

* current capacity, the hash table is <i>rehashed</i> (that is, internal data

* structures are rebuilt) so that the hash table has approximately twice the

* number of buckets.

*

* <p>As a general rule, the default load factor (.75) offers a good

* tradeoff between time and space costs. Higher values decrease the

* space overhead but increase the lookup cost (reflected in most of

* the operations of the <tt>HashMap</tt> class, including

* <tt>get</tt> and <tt>put</tt>). The expected number of entries in

* the map and its load factor should be taken into account when

* setting its initial capacity, so as to minimize the number of

* rehash operations. If the initial capacity is greater than the

* maximum number of entries divided by the load factor, no rehash

* operations will ever occur.

*

* <p>If many mappings are to be stored in a <tt>HashMap</tt>

* instance, creating it with a sufficiently large capacity will allow

* the mappings to be stored more efficiently than letting it perform

* automatic rehashing as needed to grow the table. Note that using

* many keys with the same {@code hashCode()} is a sure way to slow

* down performance of any hash table. To ameliorate impact, when keys

* are {@link Comparable}, this class may use comparison order among

* keys to help break ties.

*

* <p><strong>Note that this implementation is not synchronized.</strong>

* If multiple threads access a hash map concurrently, and at least one of

* the threads modifies the map structurally, it <i>must</i> be

* synchronized externally. (A structural modification is any operation

* that adds or deletes one or more mappings; merely changing the value

* associated with a key that an instance already contains is not a

* structural modification.) This is typically accomplished by

* synchronizing on some object that naturally encapsulates the map.

*

* If no such object exists, the map should be "wrapped" using the

* {@link Collections#synchronizedMap Collections.synchronizedMap}

* method. This is best done at creation time, to prevent accidental

* unsynchronized access to the map:<pre>

* Map m = Collections.synchronizedMap(new HashMap(...));</pre>

*

* <p>The iterators returned by all of this class's "collection view methods"

* are <i>fail-fast</i>: if the map is structurally modified at any time after

* the iterator is created, in any way except through the iterator's own

* <tt>remove</tt> method, the iterator will throw a

* {@link ConcurrentModificationException}. Thus, in the face of concurrent

* modification, the iterator fails quickly and cleanly, rather than risking

* arbitrary, non-deterministic behavior at an undetermined time in the

* future.

*

* <p>Note that the fail-fast behavior of an iterator cannot be guaranteed

* as it is, generally speaking, impossible to make any hard guarantees in the

* presence of unsynchronized concurrent modification. Fail-fast iterators

* throw <tt>ConcurrentModificationException</tt> on a best-effort basis.

* Therefore, it would be wrong to write a program that depended on this

* exception for its correctness: <i>the fail-fast behavior of iterators

* should be used only to detect bugs.</i>

*

* <p>This class is a member of the

* <a href="{@docRoot}/../technotes/guides/collections/index.html">

* Java Collections Framework</a>.

*

* @param <K> the type of keys maintained by this map

* @param <V> the type of mapped values

*

* @author Doug Lea

* @author Josh Bloch

* @author Arthur van Hoff

* @author Neal Gafter

* @see Object#hashCode()

* @see Collection

* @see Map

* @see TreeMap

* @see Hashtable

* @since 1.2

*

* @diffblue.limitedSupport

* <p>

* For performance reasons, there may be restrictions on the number of elements

* that can be stored in the model of HashMap:

* <p><ul>

* <li> HashMaps constructed using constructors of this class will have a

* fixed capacity of CProver.defaultContainerCapacity().

* <li> Non-deterministic HashMaps are currently only of size 0 or 1.

* Any functions that constrain a nondeterministically generated HashMap to be

* greater than a certain size may not deliver correct results.

* <li> HashMaps read from `--static-values` are currently unlimited.

* </ul>

*

* <p>Functions that make repeated calls to any method may not work correctly, for

* example, see the {@link #put} method.</p>

*

* <p>Does not implement

* <ul>

* <li>TreeNode</li>

* <li>spliterators</li>

* <li>methods depending on external classes notModelled (e.g. Function)</li>

* </ul>

* </p>

*

* <p>JBMC will not work correctly for hash maps on types that do

* not implement the <code>.equals()</code> and <code>.hashcode()</code>

* methods.

* </p>

*

* <p><code>HashMap&lt;ArrayList,...&gt;</code> is not supported because

* <code>ArrayList.equals()</code> cannot be implemented (needs lazy loading v2).

* </p>

*

* <p><code>HashMap&lt;StringBuilder,...&gt;</code> is not supported because

* of an issue.

* </p>

*

* <p>HashMaps on array types are not supported because of an issue.

* </p>

*

* <p>HashMaps cannot access nested <code>HashMap</code>s,

* <code>HashSet</code>s, <code>ArrayList</code>s.

* </p>

*

* There are other issues that might affect JBMC of HashMap.

*

* @diffblue.todo

*/

public class HashMap<K,V> extends AbstractMap<K,V>

implements Map<K,V>, Cloneable, Serializable {

// DIFFBLUE MODEL LIBRARY Private variable not used in model

// private static final long serialVersionUID = 362498820763181265L;

/*

* Implementation notes.

*

* This map usually acts as a binned (bucketed) hash table, but

* when bins get too large, they are transformed into bins of

* TreeNodes, each structured similarly to those in

* java.util.TreeMap. Most methods try to use normal bins, but

* relay to TreeNode methods when applicable (simply by checking

* instanceof a node). Bins of TreeNodes may be traversed and

* used like any others, but additionally support faster lookup

* when overpopulated. However, since the vast majority of bins in

* normal use are not overpopulated, checking for existence of

* tree bins may be delayed in the course of table methods.

*

* Tree bins (i.e., bins whose elements are all TreeNodes) are

* ordered primarily by hashCode, but in the case of ties, if two

* elements are of the same "class C implements Comparable<C>",

* type then their compareTo method is used for ordering. (We

* conservatively check generic types via reflection to validate

* this -- see method comparableClassFor). The added complexity

* of tree bins is worthwhile in providing worst-case O(log n)

* operations when keys either have distinct hashes or are

* orderable, Thus, performance degrades gracefully under

* accidental or malicious usages in which hashCode() methods

* return values that are poorly distributed, as well as those in

* which many keys share a hashCode, so long as they are also

* Comparable. (If neither of these apply, we may waste about a

* factor of two in time and space compared to taking no

* precautions. But the only known cases stem from poor user

* programming practices that are already so slow that this makes

* little difference.)

*

* Because TreeNodes are about twice the size of regular nodes, we

* use them only when bins contain enough nodes to warrant use

* (see TREEIFY_THRESHOLD). And when they become too small (due to

* removal or resizing) they are converted back to plain bins. In

* usages with well-distributed user hashCodes, tree bins are

* rarely used. Ideally, under random hashCodes, the frequency of

* nodes in bins follows a Poisson distribution

* (http://en.wikipedia.org/wiki/Poisson_distribution) with a

* parameter of about 0.5 on average for the default resizing

* threshold of 0.75, although with a large variance because of

* resizing granularity. Ignoring variance, the expected

* occurrences of list size k are (exp(-0.5) * pow(0.5, k) /

* factorial(k)). The first values are:

*

* 0: 0.60653066

* 1: 0.30326533

* 2: 0.07581633

* 3: 0.01263606

* 4: 0.00157952

* 5: 0.00015795

* 6: 0.00001316

* 7: 0.00000094

* 8: 0.00000006

* more: less than 1 in ten million

*

* The root of a tree bin is normally its first node. However,

* sometimes (currently only upon Iterator.remove), the root might

* be elsewhere, but can be recovered following parent links

* (method TreeNode.root()).

*

* All applicable internal methods accept a hash code as an

* argument (as normally supplied from a public method), allowing

* them to call each other without recomputing user hashCodes.

* Most internal methods also accept a "tab" argument, that is

* normally the current table, but may be a new or old one when

* resizing or converting.

*

* When bin lists are treeified, split, or untreeified, we keep

* them in the same relative access/traversal order (i.e., field

* Node.next) to better preserve locality, and to slightly

* simplify handling of splits and traversals that invoke

* iterator.remove. When using comparators on insertion, to keep a

* total ordering (or as close as is required here) across

* rebalancings, we compare classes and identityHashCodes as

* tie-breakers.

*

* The use and transitions among plain vs tree modes is

* complicated by the existence of subclass LinkedHashMap. See

* below for hook methods defined to be invoked upon insertion,

* removal and access that allow LinkedHashMap internals to

* otherwise remain independent of these mechanics. (This also

* requires that a map instance be passed to some utility methods

* that may create new nodes.)

*

* The concurrent-programming-like SSA-based coding style helps

* avoid aliasing errors amid all of the twisty pointer operations.

*/

/**

* The default initial capacity - MUST be a power of two.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final int DEFAULT_INITIAL_CAPACITY = 1 << 4; // aka 16

/**

* The maximum capacity, used if a higher value is implicitly specified

* by either of the constructors with arguments.

* MUST be a power of two <= 1<<30.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final int MAXIMUM_CAPACITY = 1 << 30;

/**

* The load factor used when none specified in constructor.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final float DEFAULT_LOAD_FACTOR = 0.75f;

/**

* The bin count threshold for using a tree rather than list for a

* bin. Bins are converted to trees when adding an element to a

* bin with at least this many nodes. The value must be greater

* than 2 and should be at least 8 to mesh with assumptions in

* tree removal about conversion back to plain bins upon

* shrinkage.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final int TREEIFY_THRESHOLD = 8;

/**

* The bin count threshold for untreeifying a (split) bin during a

* resize operation. Should be less than TREEIFY_THRESHOLD, and at

* most 6 to mesh with shrinkage detection under removal.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final int UNTREEIFY_THRESHOLD = 6;

/**

* The smallest table capacity for which bins may be treeified.

* (Otherwise the table is resized if too many nodes in a bin.)

* Should be at least 4 * TREEIFY_THRESHOLD to avoid conflicts

* between resizing and treeification thresholds.

*/

// DIFFBLUE MODEL LIBRARY Package-private variable not used in model

// static final int MIN_TREEIFY_CAPACITY = 64;

// DIFFBLUE MODEL LIBRARY

// Limit for the initialCapacity value passed as argument to a constructor.

// Prevents out of memory errors in the JVM when running generated traces.

// Actual behaviour will depend on the memory limits of the JVM.

static final int CPROVER_MAX_CAPACITY = 1 << 20;

/**

* Basic hash bin node, used for most entries. (See below for

* TreeNode subclass, and in LinkedHashMap for its Entry subclass.)

*

* @diffblue.limitedSupport

* In the original implementation, HashMap uses an array of nodes which can

* be part of either a linked list or tree list.

* We use a simplified version where each array entry is simply a pair of

* one key and one value.

* While it would make more sense to call this class Pair rather than Node,

* we keep the original name to stay as close as possible to the original

* code and for compatibility with subclasses.

*

* The methods equals() and toString() are not modelled for this inner class,

* though this should not affect the overall use of the Node class

* by HashMap.

*/

static class Node<K,V> implements Map.Entry<K,V> {

// DIFFBLUE MODEL LIBRARY Variable not needed in model.

// final int hash;

final K key;

V value;

// DIFFBLUE MODEL LIBRARY Variable not needed in model.

// Node<K,V> next;

// DIFFBLUE MODEL LIBRARY

// We use a simplified constructor that only takes two arguments.

// Node(int hash, K key, V value, Node<K,V> next) {

// this.hash = hash;

// this.key = key;

// this.value = value;

// this.next = next;

// }

Node(K key, V value) {

this.key = key;

this.value = value;

}

public final K getKey() { return key; }

public final V getValue() { return value; }

public final String toString() {

// return key + "=" + value;

CProver.notModelled();

return CProver.nondetWithoutNullForNotModelled();

}

// DIFFBLUE MODEL LIBRARY

// Always return 0 to be consistent with the current model of

// Object.hashCode.

public final int hashCode() {

// return Objects.hashCode(key) ^ Objects.hashCode(value);

return 0;

}

public final V setValue(V newValue) {

V oldValue = value;

value = newValue;

return oldValue;

}

public final boolean equals(Object o) {

// if (o == this)

// return true;

// if (o instanceof Map.Entry) {

// Map.Entry<?,?> e = (Map.Entry<?,?>)o;

// if (Objects.equals(key, e.getKey()) &&

// Objects.equals(value, e.getValue()))

// return true;

// }

// return false;

CProver.notModelled();

return CProver.nondetBoolean();

}

}

/* ---------------- Static utilities -------------- */

/**

* Computes key.hashCode() and spreads (XORs) higher bits of hash

* to lower. Because the table uses power-of-two masking, sets of

* hashes that vary only in bits above the current mask will

* always collide. (Among known examples are sets of Float keys

* holding consecutive whole numbers in small tables.) So we

* apply a transform that spreads the impact of higher bits

* downward. There is a tradeoff between speed, utility, and

* quality of bit-spreading. Because many common sets of hashes

* are already reasonably distributed (so don't benefit from

* spreading), and because we use trees to handle large sets of

* collisions in bins, we just XOR some shifted bits in the

* cheapest possible way to reduce systematic lossage, as well as

* to incorporate impact of the highest bits that would otherwise

* never be used in index calculations because of table bounds.

*/

// DIFFBLUE MODEL LIBRARY Package-private method not used in model

// static final int hash(Object key) {

// int h;

// return (key == null) ? 0 : (h = key.hashCode()) ^ (h >>> 16);

// }

/**

* Returns x's Class if it is of the form "class C implements

* Comparable<C>", else null.

*/

// DIFFBLUE MODEL LIBRARY Package-private method not used in model

// static Class<?> comparableClassFor(Object x) {

// if (x instanceof Comparable) {

// Class<?> c; Type[] ts, as; Type t; ParameterizedType p;

// if ((c = x.getClass()) == String.class) // bypass checks

// return c;

// if ((ts = c.getGenericInterfaces()) != null) {

// for (int i = 0; i < ts.length; ++i) {

// if (((t = ts[i]) instanceof ParameterizedType) &&

// ((p = (ParameterizedType)t).getRawType() ==

// Comparable.class) &&

// (as = p.getActualTypeArguments()) != null &&

// as.length == 1 && as[0] == c) // type arg is c

// return c;

// }

// }

// }

// return null;

// }

/**

* Returns k.compareTo(x) if x matches kc (k's screened comparable

* class), else 0.

*/

// DIFFBLUE MODEL LIBRARY Package-private method not used in model

// @SuppressWarnings({"rawtypes","unchecked"}) // for cast to Comparable

// static int compareComparables(Class<?> kc, Object k, Object x) {

// return (x == null || x.getClass() != kc ? 0 :

// ((Comparable)k).compareTo(x));

// }

/**

* Returns a power of two size for the given target capacity.

*/

// DIFFBLUE MODEL LIBRARY Package-private method not used in model

// static final int tableSizeFor(int cap) {

// int n = cap - 1;

// n |= n >>> 1;

// n |= n >>> 2;

// n |= n >>> 4;

// n |= n >>> 8;

// n |= n >>> 16;

// return (n < 0) ? 1 : (n >= MAXIMUM_CAPACITY) ? MAXIMUM_CAPACITY : n + 1;

// }

/* ---------------- Fields -------------- */

/**

* The table, initialized on first use, and resized as

* necessary. When allocated, length is always a power of two.

* (We also tolerate length zero in some operations to allow

* bootstrapping mechanics that are currently not needed.)

*/

// DIFFBLUE MODEL LIBRARY

// This field is allowed to be null in the original implementation to save

// memory, but in the model we restrict it to be non-null to restrict the

// number of branches to consider.

transient Node<K,V>[] table;

/**

* Holds cached entrySet(). Note that AbstractMap fields are used

* for keySet() and values().

*/

// DIFFBLUE MODEL LIBRARY

// This field is never read in our model. We include it because some

// classes which extend this one reference it.

// transient Set<Map.Entry<K,V>> entrySet;

transient Set<Map.Entry<K,V>> entrySet = null;

/**

* The number of key-value mappings contained in this map.

*/

transient int size;

/**

* The number of times this HashMap has been structurally modified

* Structural modifications are those that change the number of mappings in

* the HashMap or otherwise modify its internal structure (e.g.,

* rehash). This field is used to make iterators on Collection-views of

* the HashMap fail-fast. (See ConcurrentModificationException).

*/

transient int modCount;

/**

* The next size value at which to resize (capacity * load factor).

*

* @serial

*/

// (The javadoc description is true upon serialization.

// Additionally, if the table array has not been allocated, this

// field holds the initial array capacity, or zero signifying

// DEFAULT_INITIAL_CAPACITY.)

// DIFFBLUE MODEL LIBRARY Variable not used in model

// int threshold;

/**

* The load factor for the hash table.

*

* @serial

*/

// DIFFBLUE MODEL LIBRARY Variable not used in the model

// final float loadFactor;

// DIFFBLUE MODEL LIBRARY

// Fields inherited from AbstractMap:

// transient Set<K> keySet;

// transient Collection<V> values;

/* ---------------- Public operations -------------- */

/**

* Constructs an empty <tt>HashMap</tt> with the specified initial

* capacity and load factor.

*

* @param initialCapacity the initial capacity

* @param loadFactor the load factor

* @throws IllegalArgumentException if the initial capacity is negative

* or the load factor is nonpositive

*

* @diffblue.fullSupport

* <p> In the original implementation, the table field of a new HashMap

* object is initially null in the case of the first three constructors, and

* is only initialised when {@link #put} or {@link #putAll} is called.

* We simplify this in the model so that a table array is always initialised

* on object creation. The state after using a modelled constructor is

* equivalent to the state of a HashMap that was created, had an element

* added and then had that element removed again in the implementation from

* the jdk (except for modCount being 0).</p>

*

* <p>The <code>initialCapacity</code> value is limited to 2^20, to avoid

* generating tests that might exceed the memory limits of the JVM.</p>

*/

// DIFFBLUE MODEL LIBRARY

// @SuppressWarnings is needed for the type cast to Node<K,V>[].

@SuppressWarnings("unchecked")

public HashMap(int initialCapacity, float loadFactor) {

// if (initialCapacity < 0)

// throw new IllegalArgumentException("Illegal initial capacity: " +

// initialCapacity);

// if (initialCapacity > MAXIMUM_CAPACITY)

// initialCapacity = MAXIMUM_CAPACITY;

// if (loadFactor <= 0 || Float.isNaN(loadFactor))

// throw new IllegalArgumentException("Illegal load factor: " +

// loadFactor);

// this.loadFactor = loadFactor;

// this.threshold = tableSizeFor(initialCapacity);

// DIFFBLUE MODEL LIBRARY

// The string operations on the exception arguments can significantly

// slow down JBMC in some cases. This should be reviewed

// again with improved versions of the string solver.

CProver.assume(initialCapacity <= CPROVER_MAX_CAPACITY);

if (initialCapacity < 0)

throw new IllegalArgumentException();

if (loadFactor <= 0 || Float.isNaN(loadFactor))

throw new IllegalArgumentException();

this.table = (Node<K,V>[]) new Node[5];

this.size = 0;

this.modCount = 0;

}

/**

* Constructs an empty <tt>HashMap</tt> with the specified initial

* capacity and the default load factor (0.75).

*

* @param initialCapacity the initial capacity.

* @throws IllegalArgumentException if the initial capacity is negative.

*

* @diffblue.fullSupport

* <p>Instead of calling {@link #HashMap(int, float) this(int, float)}, we

* model this constructor explicitly in order to avoid the exception for

* invalid loadFactor values. This exception can slow down JBMC

* especially in the case of recursive unwinding.</p>

*

* <p>The <code>initialCapacity</code> value is limited to 2^20, to avoid

* generating tests that might exceed the memory limits of the JVM.</p>

*/

public HashMap(int initialCapacity) {

// this(initialCapacity, DEFAULT_LOAD_FACTOR);

CProver.assume(initialCapacity <= CPROVER_MAX_CAPACITY);

if (initialCapacity < 0)

throw new IllegalArgumentException();

this.table = (Node<K,V>[]) new Node[5];

this.size = 0;

this.modCount = 0;

}

/**

* Constructs an empty <tt>HashMap</tt> with the default initial capacity

* (16) and the default load factor (0.75).

*

* @diffblue.fullSupport

*/

// DIFFBLUE MODEL LIBRARY

// @SuppressWarnings is needed for the type cast to Node<K,V>[].

@SuppressWarnings("unchecked")

public HashMap() {

// DIFFBLUE MODEL LIBRARY

// this.loadFactor = DEFAULT_LOAD_FACTOR;

this.table = (Node<K,V>[]) new Node[5];

this.size = 0;

this.modCount = 0;

}

/**

* Constructs a new <tt>HashMap</tt> with the same mappings as the

* specified <tt>Map</tt>. The <tt>HashMap</tt> is created with

* default load factor (0.75) and an initial capacity sufficient to

* hold the mappings in the specified <tt>Map</tt>.

*

* @param m the map whose mappings are to be placed in this map

* @throws NullPointerException if the specified map is null

*

* @diffblue.fullSupport

* The implementation does not check for duplicates in the Map parameter

* to speed up JBMC, but this is OK because a Map cannot

* contain duplicate keys.

*/

@SuppressWarnings("unchecked")

public HashMap(Map<? extends K, ? extends V> m) {

// DIFFBLUE MODEL LIBRARY

// this.loadFactor = DEFAULT_LOAD_FACTOR;

// putMapEntries(m, false);

this.size = m.size();

this.table = (Node<K,V>[]) new Node[5];

this.modCount = 0;

int index = 0;

for (Map.Entry<? extends K, ? extends V> e : m.entrySet()) {

K key = e.getKey();

V value = e.getValue();

// DIFFBLUE MODEL LIBRARY

// Custom implementation of put that does not check for duplicates

// (Can save a lot of time in JBMC)

table[index] = new Node(key, value);

index++;

}

}

/**

* Implements Map.putAll and Map constructor

*

* @param m the map

* @param evict false when initially constructing this map, else

* true (relayed to method afterNodeInsertion).

*/

// DIFFBLUE MODEL LIBRARY Package-private method not used in model

// final void putMapEntries(Map<? extends K, ? extends V> m, boolean evict) {

// int s = m.size();

// if (s > 0) {

// if (table == null) { // pre-size

// float ft = ((float)s / loadFactor) + 1.0F;

// int t = ((ft < (float)MAXIMUM_CAPACITY) ?

// (int)ft : MAXIMUM_CAPACITY);

// if (t > threshold)

// threshold = tableSizeFor(t);

// }

// else if (s > threshold)

// resize();

// for (Map.Entry<? extends K, ? extends V> e : m.entrySet()) {

// K key = e.getKey();

// V value = e.getValue();

// putVal(hash(key), key, value, false, evict);

// }

// }

// }

/**

* Returns the number of key-value mappings in this map.

*

* @return the number of key-value mappings in this map

*

* @diffblue.fullSupport

*/

// DIFFBLUE MODEL LIBRARY

// Implementation from jdk.

public int size() {

return size;

}

/**

* Returns <tt>true</tt> if this map contains no key-value mappings.

*

* @return <tt>true</tt> if this map contains no key-value mappings

*

* @diffblue.fullSupport

*/

// DIFFBLUE MODEL LIBRARY

// Implementation from jdk.

public boolean isEmpty() {

return size == 0;

}

/**

* Returns the value to which the specified key is mapped,

* or {@code null} if this map contains no mapping for the key.

*

* <p>More formally, if this map contains a mapping from a key

* {@code k} to a value {@code v} such that {@code (key==null ? k==null :

* key.equals(k))}, then this method returns {@code v}; otherwise

* it returns {@code null}. (There can be at most one such mapping.)

*

* <p>A return value of {@code null} does not <i>necessarily</i>

* indicate that the map contains no mapping for the key; it's also

* possible that the map explicitly maps the key to {@code null}.

* The {@link #containsKey containsKey} operation may be used to

* distinguish these two cases.

*

* @see #put(Object, Object)

*

* @diffblue.fullSupport

*/

// DIFFBLUE MODEL LIBRARY

// Similar to original implementation, using cproverIndexOfKey instead of

// getNode to find the specified key in elementData.

public V get(Object key) {

// Node<K,V> e;

// return (e = getNode(hash(key), key)) == null ? null : e.value;

int index = cproverIndexOfKey(key);

return index < 0 ? null : table[index].value;

}

/**

* Implements Map.get and related methods

*

* @param hash hash for key

* @param key the key

* @return the node, or null if none

*/

// DIFFBLUE MODEL LIBRARY

// We do not use this method in the model. Instead, we use the newly defined

// method cproverIndexOfKey(Object key) to find the index of a node (pair)

// with a given key in the array.

// final Node<K,V> getNode(int hash, Object key) {

// Node<K,V>[] tab; Node<K,V> first, e; int n; K k;

// if ((tab = table) != null && (n = tab.length) > 0 &&

// (first = tab[(n - 1) & hash]) != null) {

// if (first.hash == hash && // always check first node

// ((k = first.key) == key || (key != null && key.equals(k))))

// return first;

// if ((e = first.next) != null) {

// if (first instanceof TreeNode)

// return ((TreeNode<K,V>)first).getTreeNode(hash, key);

// do {

// if (e.hash == hash &&

// ((k = e.key) == key || (key != null && key.equals(k))))

// return e;

// } while ((e = e.next) != null);

// }

// }

// return null;

// }

/**

* Returns <tt>true</tt> if this map contains a mapping for the

* specified key.

*

* @param key The key whose presence in this map is to be tested

* @return <tt>true</tt> if this map contains a mapping for the specified

* key.

*

* @diffblue.fullSupport

*/

// DIFFBLUE MODEL LIBRARY

// Similar to original implementation, using cproverIndexOfKey instead of

// getNode to find the specified key in elementData.

public boolean containsKey(Object key) {

// return getNode(hash(key), key) != null;

return cproverIndexOfKey(key) >= 0;

}

/**

* Associates the specified value with the specified key in this map.

* If the map previously contained a mapping for the key, the old

* value is replaced.

*

* @param key key with which the specified value is to be associated

* @param value value to be associated with the specified key

* @return the previous value associated with <tt>key</tt>, or

* <tt>null</tt> if there was no mapping for <tt>key</tt>.

* (A <tt>null</tt> return can also indicate that the map

* previously associated <tt>null</tt> with <tt>key</tt>.)

*

* @diffblue.limitedSupport

* <p>Calling this method more than 5 times on a nondeterministically generated

* HashMap or 8 times on a hardcoded HashMap can affect JBMC.</p>

*/

// DIFFBLUE MODEL LIBRARY

// We use cproverIndexOfKey to check if a mapping for the specified key is

// already present, then replace the associated value if it is present, or

// append a new key-value pair to elementData otherwise.

public V put(K key, V value) {

// return putVal(hash(key), key, value, false, true);

int index = cproverIndexOfKey(key);

if (index >= 0) { // existing mapping for key

V oldValue = table[index].value;

table[index].value = value;

return oldValue;

}

else { // key not present

CProver.assume(table.length > size);

table[size++] = new Node<K,V>(key, value);

modCount++;

return null;

}

}

/**

* Implements Map.put and related methods

*

* @param hash hash for key

* @param key the key

* @param value the value to put

* @param onlyIfAbsent if true, don't change existing value

* @param evict if false, the table is in creation mode.

* @return previous value, or null if none

*/

// DIFFBLUE MODEL LIBRARY

// We do not use this method in the model.

// final V putVal(int hash, K key, V value, boolean onlyIfAbsent,

// boolean evict) {

// Node<K,V>[] tab; Node<K,V> p; int n, i;

// if ((tab = table) == null || (n = tab.length) == 0)

// n = (tab = resize()).length;

// if ((p = tab[i = (n - 1) & hash]) == null)

// tab[i] = newNode(hash, key, value, null);

// else {

// Node<K,V> e; K k;

// if (p.hash == hash &&

// ((k = p.key) == key || (key != null && key.equals(k))))

// e = p;

// else if (p instanceof TreeNode)

// e = ((TreeNode<K,V>)p).putTreeVal(this, tab, hash, key, value);

// else {

// for (int binCount = 0; ; ++binCount) {

// if ((e = p.next) == null) {

// p.next = newNode(hash, key, value, null);

// if (binCount >= TREEIFY_THRESHOLD - 1) // -1 for 1st

// treeifyBin(tab, hash);

// break;

// }

// if (e.hash == hash &&

// ((k = e.key) == key || (key != null && key.equals(k))))

// break;

// p = e;

// }

// }

// if (e != null) { // existing mapping for key

// V oldValue = e.value;

// if (!onlyIfAbsent || oldValue == null)

// e.value = value;

// afterNodeAccess(e);

// return oldValue;

// }

// }

// ++modCount;

// if (++size > threshold)

// resize();

// afterNodeInsertion(evict);

// return null;

// }

/**

* Initializes or doubles table size. If null, allocates in

* accord with initial capacity target held in field threshold.

* Otherwise, because we are using power-of-two expansion, the

* elements from each bin must either stay at same index, or move

* with a power of two offset in the new table.

*

* @return the table

*/

// DIFFBLUE MODEL LIBRARY

// We do not use this method in the model.

// final Node<K,V>[] resize() {

// Node<K,V>[] oldTab = table;

// int oldCap = (oldTab == null) ? 0 : oldTab.length;

// int oldThr = threshold;

// int newCap, newThr = 0;

// if (oldCap > 0) {

// if (oldCap >= MAXIMUM_CAPACITY) {

// threshold = Integer.MAX_VALUE;

// return oldTab;

// }

// else if ((newCap = oldCap << 1) < MAXIMUM_CAPACITY &&

// oldCap >= DEFAULT_INITIAL_CAPACITY)

// newThr = oldThr << 1; // double threshold

// }

// else if (oldThr > 0) // initial capacity was placed in threshold

// newCap = oldThr;

// else { // zero initial threshold signifies using defaults

// newCap = DEFAULT_INITIAL_CAPACITY;

// newThr = (int)(DEFAULT_LOAD_FACTOR * DEFAULT_INITIAL_CAPACITY);

// }

// if (newThr == 0) {

// float ft = (float)newCap * loadFactor;

// newThr = (newCap < MAXIMUM_CAPACITY && ft < (float)MAXIMUM_CAPACITY ?

// (int)ft : Integer.MAX_VALUE);

// }

// threshold = newThr;

// @SuppressWarnings({"rawtypes","unchecked"})

// Node<K,V>[] newTab = (Node<K,V>[])new Node[newCap];

// table = newTab;

// if (oldTab != null) {

// for (int j = 0; j < oldCap; ++j) {

// Node<K,V> e;

// if ((e = oldTab[j]) != null) {

// oldTab[j] = null;

// if (e.next == null)

// newTab[e.hash & (newCap - 1)] = e;

// else if (e instanceof TreeNode)

// ((TreeNode<K,V>)e).split(this, newTab, j, oldCap);

// else { // preserve order

// Node<K,V> loHead = null, loTail = null;

// Node<K,V> hiHead = null, hiTail = null;

// Node<K,V> next;

// do {

// next = e.next;

// if ((e.hash & oldCap) == 0) {

// if (loTail == null)

// loHead = e;

// else

// loTail.next = e;

// loTail = e;

// }

// else {

// if (hiTail == null)

// hiHead = e;

// else

// hiTail.next = e;

// hiTail = e;

// }

// } while ((e = next) != null);

// if (loTail != null) {

// loTail.next = null;

// newTab[j] = loHead;

// }

// if (hiTail != null) {

// hiTail.next = null;

// newTab[j + oldCap] = hiHead;

// }

// }

// }

// }

// }

// return newTab;

// }

/**

* Replaces all linked nodes in bin at index for given hash unless

* table is too small, in which case resizes instead.

*/

// DIFFBLUE MODEL LIBRARY

// We do not use this method in the model.

// final void treeifyBin(Node<K,V>[] tab, int hash) {

// int n, index; Node<K,V> e;

// if (tab == null || (n = tab.length) < MIN_TREEIFY_CAPACITY)

// resize();

// else if ((e = tab[index = (n - 1) & hash]) != null) {

// TreeNode<K,V> hd = null, tl = null;

// do {

// TreeNode<K,V> p = replacementTreeNode(e, null);

// if (tl == null)