Module std::map

A hash map, HashMap, keyed by any K: Hash + Eq (see std::cmp). Methods that may grow the table ask for Alloc (new, with_capacity, insert); those that destroy entries ask for Free (remove, clear); lookups need no capability.

Source: std/map.weir; committed interface: std/map.iface. Index

struct HashMap

pub struct HashMap<K, V> {
    /* private fields */
}

A hash map from K to V: SwissTable-style open addressing over groups of sixteen slots, with the entries stored densely in one buffer. Lookup, insert and remove are expected O(1) (insert amortised: the table doubles at 3/4 load, moving no entry). Iteration visits entries in insertion order until a HashMap::remove, which moves the last entry into the hole. Keys are hashed with a std::cmp::Hasher: fixed secrets for HashMap::new (the same layout on every run), a secret seed for HashMap::new_randomized and HashMap::with_seed (for keys an attacker chooses). At most 3 · 2^30 entries; a larger map fails as an allocation does.

impl<K, V> HashMap<K, V>

method len

pub fn len(&self) -> usize

The number of entries.

Committed interface (std/map.iface): the signature alone.

method is_empty

pub fn is_empty(&self) -> Bool

true when the map has no entries.

Committed interface (std/map.iface): the signature alone.

method for_each

pub fn for_each(&self, f: fn(&K, &V))

Calls f on every key and value, in entry order (see HashMap).

Committed interface (std/map.iface):

holds what may not move at a scheduling point: always
enters the backing of self
callback f: envelope {A, S}; pinned: always; holds self, f
writes regions type K, type V

method for_each_mut

pub fn for_each_mut(&mut self, f: fn(&K, &mut V))

Calls f on every key and a mutable borrow of its value, in entry order.

Committed interface (std/map.iface):

holds what may not move at a scheduling point: always
enters the backing of self
writes through self: everything
callback f: envelope {A, S}; pinned: always; holds self, f
writes regions type K, type V

impl<K: copy, V: copy> HashMap<K, V>

method iter

pub fn iter(&self) -> MapIter<K, V>

An iterator over copies of the entries as (key, value), in insertion order until a remove. It borrows the map while it lives.

Committed interface (std/map.iface): the signature alone.

impl<K: copy, V> HashMap<K, V>

method keys

pub fn keys(&self) -> MapKeys<K, V>

An iterator over copies of the keys, in the order of HashMap::iter. It borrows the map while it lives.

Committed interface (std/map.iface): the signature alone.

impl<K, V: copy> HashMap<K, V>

method values

pub fn values(&self) -> MapValues<K, V>

An iterator over copies of the values, in the order of HashMap::iter. It borrows the map while it lives.

Committed interface (std/map.iface): the signature alone.

impl<K: Hash + Eq, V> HashMap<K, V>

method get

pub fn get(&self, k: &K) -> Option<&{self} V>

The value for k, or None when the map has no such key.

Committed interface (std/map.iface):

bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
scheduling point: Eq not quiet | Hash not quiet
holds what may not move at a scheduling point: Eq not quiet | Hash not quiet
enters the backing of self, k
writes regions type K
loan of Hash across the backing of k
loan of Eq across the backing of self
loan of Eq across the backing of k

method get_mut

pub fn get_mut(&mut self, k: &K) -> Option<&{self} mut V>

A mutable borrow of the value for k, or None when the map has no such key.

Committed interface (std/map.iface):

bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
scheduling point: Eq not quiet | Hash not quiet
holds what may not move at a scheduling point: Eq not quiet | Hash not quiet
enters the backing of self, k
writes through self: everything
writes regions type K
loan of Hash across the backing of k
loan of Eq across the backing of self
loan of Eq across the backing of k

method contains_key

pub fn contains_key(&self, k: &K) -> Bool

true when the map has an entry for k.

Committed interface (std/map.iface):

bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
scheduling point: Eq not quiet | Hash not quiet
holds what may not move at a scheduling point: Eq not quiet | Hash not quiet
enters the backing of self, k
writes regions type K
loan of Hash across the backing of k
loan of Eq across the backing of self
loan of Eq across the backing of k

impl<K: Hash + Eq + drops {Free}, V: drops {Free}> HashMap<K, V>

method remove

pub fn remove(&mut self, k: &K) -> Option<V> with Free

Removes k's entry and returns its value, or None when there is none. The stored key is destroyed, hence with Free. The last entry moves into the removed one's place.

Committed interface (std/map.iface):

bound Free: Free any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
scheduling point: Eq not quiet | Hash not quiet
holds what may not move at a scheduling point: Eq not quiet | Hash not quiet
writes through self: everything and its shape
destroys values of K
writes regions type K
loan of Hash across the backing of self
loan of Hash across the backing of k
loan of Eq across the backing of self
loan of Eq across the backing of k

method clear

pub fn clear(&mut self) with Free

Destroys every entry (with Free) and keeps the table's memory for reuse.

Committed interface (std/map.iface):

bound Free: Free any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
writes through self: everything and its shape
destroys values of K, V

impl<K: Hash + Eq + drops {Alloc}, V: drops {Alloc}> HashMap<K, V>

method new

pub fn new() -> HashMap<K, V> with Alloc

An empty map whose hasher has fixed secrets (std::cmp::Hasher::new): its layout is the same on every run, which simulation and tests want, and fine for keys the program trusts; keys an attacker chooses (a server's headers) take HashMap::new_randomized. It allocates nothing until the first HashMap::insert.

Committed interface (std/map.iface):

bound Alloc: Alloc any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
aborts: Alloc.alloc
scheduling point: Eq not quiet | Hash not quiet

method with_seed

pub fn with_seed(seed: u64) -> HashMap<K, V> with Alloc

An empty map whose hasher is keyed by seed (Hasher::with_seed).

Committed interface (std/map.iface):

bound Alloc: Alloc any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
aborts: Alloc.alloc
scheduling point: Eq not quiet | Hash not quiet

method new_randomized

pub fn new_randomized() -> HashMap<K, V> with Alloc, Random

An empty map keyed by a seed drawn from the caller's Random: an attacker who cannot predict the draw cannot build keys that collide in it. Under std::sim's worlds the draw is the world's seed's, so a run is reproducible; natively with OsRandom([0u8; 256], 0) { … } (std::rand) draws from the operating system. The root supplies no Random, so the caller installs one.

Committed interface (std/map.iface):

bound Alloc: Alloc any
bound Random: Random any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
aborts: Alloc.alloc
scheduling point: Eq not quiet | Hash not quiet | Random not quiet

method with_capacity

pub fn with_capacity(n: usize) -> HashMap<K, V> with Alloc

A map that holds n entries without growing.

Committed interface (std/map.iface):

bound Alloc: Alloc any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
aborts: Alloc.alloc

method insert

pub fn insert(&mut self, k: K, v: V) -> Option<V> with Alloc

Maps k to v. Returns the old value when k was present (the new key replaces the old one), else None. with Alloc: it may grow the table and the entry buffer.

Committed interface (std/map.iface):

bound Alloc: Alloc any
bound Hash: Hash<K> any row {Diverge}
bound Eq: Eq<K> any row {Diverge}
aborts: Alloc.alloc
scheduling point: Eq not quiet | Hash not quiet
holds what may not move at a scheduling point: Eq not quiet
writes through self: everything and its shape
destroys values of K, V
writes regions type K
loan of Hash across the backing of self
loan of Hash across the backing of k
loan of Eq across the backing of self
loan of Eq across the backing of k

struct MapIter

pub struct MapIter<K, V>: forget {
    /* private fields */
}

The iterator HashMap::iter returns: copies of the entries as pairs, borrowing the map.

Implementations:

struct MapKeys

pub struct MapKeys<K, V>: forget {
    /* private fields */
}

The iterator HashMap::keys returns: copies of the keys, borrowing the map.

Implementations:

struct MapValues

pub struct MapValues<K, V>: forget {
    /* private fields */
}

The iterator HashMap::values returns: copies of the values, borrowing the map.

Implementations: