diff options
author | Son Ho | 2022-02-09 02:01:49 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 02:01:49 +0100 |
commit | 85c4f981d7c7328810b8b76b00c617803e2e0f17 (patch) | |
tree | 7b3f66aea2a85d0ac0f967ea89358bed13530417 /examples | |
parent | 5c9019003187f14797ba4d4514fec1cf2ac03d65 (diff) |
Remove the hashmap example (which was moved to Charon)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/misc/Cargo.toml | 9 | ||||
-rw-r--r-- | examples/misc/Makefile | 15 | ||||
-rw-r--r-- | examples/misc/src/hashmap.rs | 189 | ||||
-rw-r--r-- | examples/misc/src/main.rs | 5 |
4 files changed, 0 insertions, 218 deletions
diff --git a/examples/misc/Cargo.toml b/examples/misc/Cargo.toml deleted file mode 100644 index 31ffeaf9..00000000 --- a/examples/misc/Cargo.toml +++ /dev/null @@ -1,9 +0,0 @@ -[package] -name = "misc" -version = "0.1.0" -authors = ["Son Ho <hosonmarc@gmail.com>"] -edition = "2018" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] diff --git a/examples/misc/Makefile b/examples/misc/Makefile deleted file mode 100644 index a8e3fbc6..00000000 --- a/examples/misc/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -CHARON_HOME=../../../charon/charon - -all: build test translate - -.PHONY: build -build: - cargo build - -.PHONY: test -test: - cargo test - -.PHONY: translate -translate: - cd $(CHARON_HOME) && cargo run ../../aeneas/examples/misc/src/hashmap.rs diff --git a/examples/misc/src/hashmap.rs b/examples/misc/src/hashmap.rs deleted file mode 100644 index 721a859a..00000000 --- a/examples/misc/src/hashmap.rs +++ /dev/null @@ -1,189 +0,0 @@ -//! A hashmap implementation. -//! TODO: we will need function pointers/closures if we want to make the map -//! generic in the key type. - -use std::vec::Vec; -pub type Key = usize; // TODO: make this generic -pub type Hash = usize; - -pub enum List<T> { - Cons(Key, T, Box<List<T>>), - Nil, -} - -/// A hash function for the keys. -/// Rk.: we use shared references because we anticipate on the generic -/// hash map version. -pub fn hash_key(k: &Key) -> Hash { - // Do nothing for now, we might want to implement something smarter - // in the future - *k -} - -/// A hash map from [u64] to values -pub struct HashMap<T> { - /// The current number of values in the table - num_values: usize, - /// The max load factor, expressed as a fraction - /// TODO: use - max_load_factor: (usize, usize), - /// The table itself - slots: Vec<List<T>>, -} - -impl<T> HashMap<T> { - /// Allocate a vector of slots of a given size. - /// We would need a loop, but can't use loops for now... - fn allocate_slots(mut slots: Vec<List<T>>, n: usize) -> Vec<List<T>> { - if n == 0 { - slots - } else { - slots.push(List::Nil); - HashMap::allocate_slots(slots, n - 1) - } - } - - pub fn new() -> Self { - let slots = HashMap::allocate_slots(Vec::new(), 32); - HashMap { - num_values: 0, - max_load_factor: (4, 5), - slots, - } - } - - /// We need a loop here too... - /// Also, we start with the end, so that F* sees that the function terminates. - fn clear_slots(slots: &mut Vec<List<T>>, i: usize) { - if i > 0 { - let i = i - 1; - slots[i] = List::Nil; - HashMap::clear_slots(slots, i) - } else { - () - } - } - - pub fn clear(&mut self) { - self.num_values = 0; - let len = self.slots.len(); - HashMap::clear_slots(&mut self.slots, len); - } - - pub fn len(&self) -> usize { - self.num_values - } - - fn insert_in_list(key: Key, value: T, ls: &mut List<T>) { - match ls { - List::Nil => *ls = List::Cons(key, value, Box::new(List::Nil)), - List::Cons(ckey, cvalue, ls) => { - if *ckey == key { - *cvalue = value; - } else { - HashMap::insert_in_list(key, value, ls) - } - } - } - } - - pub fn insert(&mut self, key: Key, value: T) { - let hash = hash_key(&key); - let hash_mod = hash % self.slots.len(); - // We may want to use slots[...] instead of get_mut... - HashMap::insert_in_list(key, value, &mut self.slots[hash_mod]); - } - - fn get_in_list<'l, 'k>(key: &'k Key, ls: &'l List<T>) -> Option<&'l T> { - match ls { - List::Nil => None, - List::Cons(ckey, cvalue, ls) => { - if *ckey == *key { - Some(cvalue) - } else { - HashMap::get_in_list(key, ls) - } - } - } - } - - /// The signature is not exactly the same as the one in - /// [https://doc.rust-lang.org/std/collections/struct.HashMap.html#method.get_mut] - /// (the region paramaters are more precise here). - pub fn get<'l, 'k>(&'l self, key: &'k Key) -> Option<&'l T> { - let hash = hash_key(key); - let hash_mod = hash % self.slots.len(); - HashMap::get_in_list(key, &self.slots[hash_mod]) - } - - fn get_mut_in_list<'l, 'k>(key: &'k Key, ls: &'l mut List<T>) -> Option<&'l mut T> { - match ls { - List::Nil => None, - List::Cons(ckey, cvalue, ls) => { - if *ckey == *key { - Some(cvalue) - } else { - HashMap::get_mut_in_list(key, ls) - } - } - } - } - - /// Same remark as for [get]. - pub fn get_mut<'l, 'k>(&'l mut self, key: &'k Key) -> Option<&'l mut T> { - let hash = hash_key(key); - let hash_mod = hash % self.slots.len(); - HashMap::get_mut_in_list(key, &mut self.slots[hash_mod]) - } - - fn remove_from_list(key: &Key, ls: &mut List<T>) -> Option<T> { - match ls { - List::Nil => None, - List::Cons(ckey, _, tl) => { - if *ckey == *key { - // We have to move under borrows, so we need to use - // [std::mem::replace] in several steps. - // Retrieve the tail - let mv_ls = std::mem::replace(ls, List::Nil); - match mv_ls { - List::Nil => unreachable!(), - List::Cons(_, cvalue, tl) => { - // Make the list equal to its tail - *ls = *tl; - // Returned the dropped value - Some(cvalue) - } - } - } else { - HashMap::remove_from_list(key, tl) - } - } - } - } - - /// Same remark as for [get]. - pub fn remove(&mut self, key: &Key) -> Option<T> { - let hash = hash_key(key); - let hash_mod = hash % self.slots.len(); - HashMap::remove_from_list(key, &mut self.slots[hash_mod]) - } -} - -#[test] -fn test1() { - let mut hm: HashMap<u64> = HashMap::new(); - hm.insert(0, 42); - hm.insert(128, 18); - hm.insert(1024, 138); - hm.insert(1056, 256); - assert!(*hm.get(&128).unwrap() == 18); - let x = hm.get_mut(&1024).unwrap(); - *x = 56; - assert!(*hm.get(&1024).unwrap() == 56); - assert!(hm.get(&10).is_none()); - let x = hm.remove(&1024).unwrap(); - assert!(x == 56); - assert!(*hm.get(&0).unwrap() == 42); - assert!(*hm.get(&128).unwrap() == 18); - assert!(*hm.get(&1056).unwrap() == 256); -} diff --git a/examples/misc/src/main.rs b/examples/misc/src/main.rs deleted file mode 100644 index 4a984052..00000000 --- a/examples/misc/src/main.rs +++ /dev/null @@ -1,5 +0,0 @@ -mod hashmap; - -use hashmap::HashMap; - -fn main() {} |