Skip to content

Commit

Permalink
[smart_table] add clear and some nits (#9746)
Browse files Browse the repository at this point in the history
  • Loading branch information
lightmark authored Aug 28, 2023
1 parent c215378 commit 6b13cd4
Show file tree
Hide file tree
Showing 5 changed files with 90 additions and 12 deletions.
56 changes: 51 additions & 5 deletions aptos-move/framework/aptos-stdlib/doc/smart_table.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ it tolerates collisions.
- [Function `new_with_config`](#0x1_smart_table_new_with_config)
- [Function `destroy_empty`](#0x1_smart_table_destroy_empty)
- [Function `destroy`](#0x1_smart_table_destroy)
- [Function `clear`](#0x1_smart_table_clear)
- [Function `add`](#0x1_smart_table_add)
- [Function `add_all`](#0x1_smart_table_add_all)
- [Function `unzip_entries`](#0x1_smart_table_unzip_entries)
Expand All @@ -39,6 +40,7 @@ it tolerates collisions.
- [Struct `SmartTable`](#@Specification_1_SmartTable)
- [Function `new_with_config`](#@Specification_1_new_with_config)
- [Function `destroy`](#@Specification_1_destroy)
- [Function `clear`](#@Specification_1_clear)
- [Function `add_all`](#@Specification_1_add_all)
- [Function `to_simple_map`](#@Specification_1_to_simple_map)
- [Function `split_one_bucket`](#@Specification_1_split_one_bucket)
Expand Down Expand Up @@ -361,13 +363,41 @@ Destroy a table completely when V has <code>drop</code>.


<pre><code><b>public</b> <b>fun</b> <a href="smart_table.md#0x1_smart_table_destroy">destroy</a>&lt;K: drop, V: drop&gt;(<a href="table.md#0x1_table">table</a>: <a href="smart_table.md#0x1_smart_table_SmartTable">SmartTable</a>&lt;K, V&gt;) {
<b>let</b> i = 0;
<a href="smart_table.md#0x1_smart_table_clear">clear</a>(&<b>mut</b> <a href="table.md#0x1_table">table</a>);
<a href="smart_table.md#0x1_smart_table_destroy_empty">destroy_empty</a>(<a href="table.md#0x1_table">table</a>);
}
</code></pre>



</details>

<a name="0x1_smart_table_clear"></a>

## Function `clear`

Clear a table completely when T has <code>drop</code>.


<pre><code><b>public</b> <b>fun</b> <a href="smart_table.md#0x1_smart_table_clear">clear</a>&lt;K: drop, V: drop&gt;(<a href="table.md#0x1_table">table</a>: &<b>mut</b> <a href="smart_table.md#0x1_smart_table_SmartTable">smart_table::SmartTable</a>&lt;K, V&gt;)
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="smart_table.md#0x1_smart_table_clear">clear</a>&lt;K: drop, V: drop&gt;(<a href="table.md#0x1_table">table</a>: &<b>mut</b> <a href="smart_table.md#0x1_smart_table_SmartTable">SmartTable</a>&lt;K, V&gt;) {
*<a href="table_with_length.md#0x1_table_with_length_borrow_mut">table_with_length::borrow_mut</a>(&<b>mut</b> <a href="table.md#0x1_table">table</a>.buckets, 0) = <a href="../../move-stdlib/doc/vector.md#0x1_vector_empty">vector::empty</a>();
<b>let</b> i = 1;
<b>while</b> (i &lt; <a href="table.md#0x1_table">table</a>.num_buckets) {
<a href="table_with_length.md#0x1_table_with_length_remove">table_with_length::remove</a>(&<b>mut</b> <a href="table.md#0x1_table">table</a>.buckets, i);
i = i + 1;
};
<b>let</b> <a href="smart_table.md#0x1_smart_table_SmartTable">SmartTable</a> { buckets, num_buckets: _, level: _, size: _, split_load_threshold: _, target_bucket_size: _ } = <a href="table.md#0x1_table">table</a>;
<a href="table_with_length.md#0x1_table_with_length_destroy_empty">table_with_length::destroy_empty</a>(buckets);
<a href="table.md#0x1_table">table</a>.num_buckets = 1;
<a href="table.md#0x1_table">table</a>.level = 0;
<a href="table.md#0x1_table">table</a>.size = 0;
}
</code></pre>

Expand Down Expand Up @@ -1003,7 +1033,7 @@ Update <code>target_bucket_size</code>.
map_spec_set = spec_set,
map_spec_del = spec_remove,
map_spec_len = spec_len,
map_spec_has_key = spec_contains;
map_spec_has_key = spec_contains;
</code></pre>


Expand Down Expand Up @@ -1035,6 +1065,22 @@ Update <code>target_bucket_size</code>.



<pre><code><b>pragma</b> verify = <b>false</b>;
</code></pre>



<a name="@Specification_1_clear"></a>

### Function `clear`


<pre><code><b>public</b> <b>fun</b> <a href="smart_table.md#0x1_smart_table_clear">clear</a>&lt;K: drop, V: drop&gt;(<a href="table.md#0x1_table">table</a>: &<b>mut</b> <a href="smart_table.md#0x1_smart_table_SmartTable">smart_table::SmartTable</a>&lt;K, V&gt;)
</code></pre>




<pre><code><b>pragma</b> verify = <b>false</b>;
</code></pre>

Expand Down Expand Up @@ -1083,7 +1129,7 @@ Update <code>target_bucket_size</code>.



<pre><code><b>pragma</b> verify= <b>false</b>;
<pre><code><b>pragma</b> verify = <b>false</b>;
</code></pre>


Expand Down
3 changes: 2 additions & 1 deletion aptos-move/framework/aptos-stdlib/doc/smart_vector.md
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,7 @@ Aborts if <code>v</code> is not empty.

## Function `destroy`

Destroy a table completely when T has <code>drop</code>.
Destroy a vector completely when T has <code>drop</code>.


<pre><code><b>public</b> <b>fun</b> <a href="smart_vector.md#0x1_smart_vector_destroy">destroy</a>&lt;T: drop&gt;(v: <a href="smart_vector.md#0x1_smart_vector_SmartVector">smart_vector::SmartVector</a>&lt;T&gt;)
Expand All @@ -324,6 +324,7 @@ Destroy a table completely when T has <code>drop</code>.

## Function `clear`

Clear a vector completely when T has <code>drop</code>.


<pre><code><b>public</b> <b>fun</b> <a href="smart_vector.md#0x1_smart_vector_clear">clear</a>&lt;T: drop&gt;(v: &<b>mut</b> <a href="smart_vector.md#0x1_smart_vector_SmartVector">smart_vector::SmartVector</a>&lt;T&gt;)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -103,13 +103,21 @@ module aptos_std::smart_table {

/// Destroy a table completely when V has `drop`.
public fun destroy<K: drop, V: drop>(table: SmartTable<K, V>) {
let i = 0;
clear(&mut table);
destroy_empty(table);
}

/// Clear a table completely when T has `drop`.
public fun clear<K: drop, V: drop>(table: &mut SmartTable<K, V>) {
*table_with_length::borrow_mut(&mut table.buckets, 0) = vector::empty();
let i = 1;
while (i < table.num_buckets) {
table_with_length::remove(&mut table.buckets, i);
i = i + 1;
};
let SmartTable { buckets, num_buckets: _, level: _, size: _, split_load_threshold: _, target_bucket_size: _ } = table;
table_with_length::destroy_empty(buckets);
table.num_buckets = 1;
table.level = 0;
table.size = 0;
}

/// Add (key, value) pair in the hash map, it may grow one bucket if current load factor exceeds the threshold.
Expand Down Expand Up @@ -435,4 +443,22 @@ module aptos_std::smart_table {
assert!(simple_map::length(&map) == 200, 0);
destroy(table);
}

#[test]
public fun smart_table_clear_test() {
let table = new();
let i = 0u64;
while (i < 200) {
add(&mut table, i, i);
i = i + 1;
};
clear(&mut table);
let i = 0;
while (i < 200) {
add(&mut table, i, i);
i = i + 1;
};
assert!(table.size == 200, 0);
destroy(table);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ spec aptos_std::smart_table {
map_spec_set = spec_set,
map_spec_del = spec_remove,
map_spec_len = spec_len,
map_spec_has_key = spec_contains;
map_spec_has_key = spec_contains;
}

spec new_with_config<K: copy + drop + store, V: store>(num_initial_buckets: u64, split_load_threshold: u8, target_bucket_size: u64): SmartTable<K, V> {
Expand All @@ -26,8 +26,12 @@ spec aptos_std::smart_table {
pragma verify = false;
}

spec clear<K: drop, V: drop>(table: &mut SmartTable<K, V>) {
pragma verify = false;
}

spec split_one_bucket<K, V>(table: &mut SmartTable<K, V>) {
pragma verify= false;
pragma verify = false;
}

spec bucket_index(level: u8, num_buckets: u64, hash: u64): u64 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -74,12 +74,13 @@ module aptos_std::smart_vector {
option::destroy_none(big_vec);
}

/// Destroy a table completely when T has `drop`.
/// Destroy a vector completely when T has `drop`.
public fun destroy<T: drop>(v: SmartVector<T>) {
clear(&mut v);
destroy_empty(v);
}

/// Clear a vector completely when T has `drop`.
public fun clear<T: drop>(v: &mut SmartVector<T>) {
v.inline_vec = vector[];
if (option::is_some(&v.big_vec)) {
Expand Down

0 comments on commit 6b13cd4

Please sign in to comment.