From b64f99d2ba5ae280303847b13f0a489b7159e74a Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 25 Jun 2024 18:09:10 -0700 Subject: [PATCH 1/8] Add a challenge for `btree::node` module --- doc/src/challenges/0004-btree-node.md | 69 +++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 doc/src/challenges/0004-btree-node.md diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md new file mode 100644 index 0000000000000..f4a779c924780 --- /dev/null +++ b/doc/src/challenges/0004-btree-node.md @@ -0,0 +1,69 @@ +# Challenge 4: Verify the memory safety of the `alloc::collections::btree::node` module + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) +- **Start date:** *2024-07-01* +- **End date:** *2024-12-10* + +------------------- + + +## Goal + +Verify the memory safety of the [`alloc::collections::btree::node` module](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/btree/node.rs). +This is one of the main modules used for implementing the `BTreeMap` collection, and it includes a lot of unsafe code. + +After annotating functions in this module with their safety contract and verifying those contracts, verify that their usage from `BTreeMap` satisfies the contracts. + +### Success Criteria + +All public functions (especially safe ones) containing unsafe code must be annotated with safety contracts and the contracts have been verified, e.g.: + +1. `LeafNode::new` +1. `NodeRef::new_internal` +1. `NodeRef::as_internal_mut` +1. `NodeRef::len` +1. `NodeRef::ascend` +1. `NodeRef::first_edge` +1. `NodeRef::last_edge` +1. `NodeRef::first_kv` +1. `NodeRef::last_kv` +1. `NodeRef::into_leaf` +1. `NodeRef::keys` +1. `NodeRef::as_leaf_mut` +1. `NodeRef::into_leaf_mut` +1. `NodeRef::as_leaf_dying` +1. `NodeRef::pop_internal_level` +1. `NodeRef::push` +1. `Handle::left_edge` +1. `Handle::right_edge` +1. `Handle::left_kv` +1. `Handle::right_kv` +1. `Handle::insert_recursing` +1. `Handle::descend` +1. `Handle::into_kv` +1. `Handle::key_mut` +1. `Handle::into_val_mut` +1. `Handle::into_kv_mut` +1. `Handle::into_kv_valmut` +1. `Handle::kv_mut` +1. `BalancingContext::do_merge` +1. `BalancingContext::merge_tracking_child_edge` +1. `BalancingContext::steal_left` +1. `BalancingContext::steal_right` +1. `BalancingContext::bulk_steal_left` +1. `BalancingContext::bulk_steal_right` + +The usage of the above functions in `BTreeMap` is proven safe. + +### List of UBs + +All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From ac2854a50d65c2ccdac1e6c5a518d5a828887a01 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 25 Jun 2024 18:13:45 -0700 Subject: [PATCH 2/8] Update summary --- doc/src/SUMMARY.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index dba8cd9090183..8c802c82e7cc4 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -15,3 +15,4 @@ - [Challenges](./challenges.md) - [Core Transmutation](./challenges/0001-core-transmutation.md) - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) + - [Memory safety of the `alloc::collections::btree::node` module](./challenges/0004-btree-node.md) From ae8230f1ff944793a99d8792bae06788bb1cb4b5 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 27 Jun 2024 15:03:04 -0700 Subject: [PATCH 3/8] Address PR comments --- doc/src/challenges/0004-btree-node.md | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index f4a779c924780..96fc618abd252 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -1,4 +1,4 @@ -# Challenge 4: Verify the memory safety of the `alloc::collections::btree::node` module +# Challenge 4: Towards the memory safety of BTreeMap - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) @@ -13,8 +13,6 @@ Verify the memory safety of the [`alloc::collections::btree::node` module](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/btree/node.rs). This is one of the main modules used for implementing the `BTreeMap` collection, and it includes a lot of unsafe code. -After annotating functions in this module with their safety contract and verifying those contracts, verify that their usage from `BTreeMap` satisfies the contracts. - ### Success Criteria All public functions (especially safe ones) containing unsafe code must be annotated with safety contracts and the contracts have been verified, e.g.: @@ -54,8 +52,6 @@ All public functions (especially safe ones) containing unsafe code must be annot 1. `BalancingContext::bulk_steal_left` 1. `BalancingContext::bulk_steal_right` -The usage of the above functions in `BTreeMap` is proven safe. - ### List of UBs All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): From 576e20499ea1bfcba9e4a5ec46d107cbe0d328a7 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 27 Jun 2024 15:16:05 -0700 Subject: [PATCH 4/8] Emphasize unbounded verification --- doc/src/challenges/0004-btree-node.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 96fc618abd252..39b8685ef2e08 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -15,7 +15,7 @@ This is one of the main modules used for implementing the `BTreeMap` collection, ### Success Criteria -All public functions (especially safe ones) containing unsafe code must be annotated with safety contracts and the contracts have been verified, e.g.: +The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.: 1. `LeafNode::new` 1. `NodeRef::new_internal` @@ -52,6 +52,8 @@ All public functions (especially safe ones) containing unsafe code must be annot 1. `BalancingContext::bulk_steal_left` 1. `BalancingContext::bulk_steal_right` +The verification must be unbounded for functions that are recursive or that contain loops (e.g. `Handle::insert_recursing`). + ### List of UBs All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): From 9f7ba6a3cff038d32923c1f5c2c2c5b42063220c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 16 Jul 2024 16:26:32 -0700 Subject: [PATCH 5/8] Address PR comments --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0006-btree-node.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 61d579225f82c..15b0f6f0da3a9 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -17,4 +17,4 @@ - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - [Inductive data type](./challenges/0005-linked-list.md) - - [Memory safety of the `btree::node` module](./challenges/0006-btree-node.md) + - [Memory safety of BTreeMap's `btree::node` module](./challenges/0006-btree-node.md) diff --git a/doc/src/challenges/0006-btree-node.md b/doc/src/challenges/0006-btree-node.md index 39b8685ef2e08..6f252e9bd4bfa 100644 --- a/doc/src/challenges/0006-btree-node.md +++ b/doc/src/challenges/0006-btree-node.md @@ -1,4 +1,4 @@ -# Challenge 4: Towards the memory safety of BTreeMap +# Challenge 4: Memory safety of BTreeMap's `btree::node` module - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) @@ -59,7 +59,7 @@ The verification must be unbounded for functions that are recursive or that cont All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. +* Reading from uninitialized memory. * Mutating immutable bytes. * Producing an invalid value From 52c684b6e665a3e50849c45365b43e4ae8ab1c23 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 16 Jul 2024 16:33:50 -0700 Subject: [PATCH 6/8] Fix index --- doc/src/challenges/0006-btree-node.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0006-btree-node.md b/doc/src/challenges/0006-btree-node.md index 6f252e9bd4bfa..a30d38a9edd9f 100644 --- a/doc/src/challenges/0006-btree-node.md +++ b/doc/src/challenges/0006-btree-node.md @@ -1,4 +1,4 @@ -# Challenge 4: Memory safety of BTreeMap's `btree::node` module +# Challenge 6: Memory safety of BTreeMap's `btree::node` module - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) From 20c092bcb1a1d7d8bb40ed10ce89b3d7ad5ff92f Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 16 Jul 2024 16:47:19 -0700 Subject: [PATCH 7/8] Revert index change --- doc/src/challenges/{0006-btree-node.md => 0004-btree-node.md} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename doc/src/challenges/{0006-btree-node.md => 0004-btree-node.md} (97%) diff --git a/doc/src/challenges/0006-btree-node.md b/doc/src/challenges/0004-btree-node.md similarity index 97% rename from doc/src/challenges/0006-btree-node.md rename to doc/src/challenges/0004-btree-node.md index a30d38a9edd9f..6f252e9bd4bfa 100644 --- a/doc/src/challenges/0006-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -1,4 +1,4 @@ -# Challenge 6: Memory safety of BTreeMap's `btree::node` module +# Challenge 4: Memory safety of BTreeMap's `btree::node` module - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) From 59acfb7c1971405fdb913f710295443d839bcb71 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 18 Jul 2024 16:52:28 -0700 Subject: [PATCH 8/8] Separate list of functions that require unbounded verification --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0004-btree-node.md | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 15b0f6f0da3a9..9a8023d63908a 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -16,5 +16,5 @@ - [Core Transmutation](./challenges/0001-core-transmutation.md) - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) + - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [Inductive data type](./challenges/0005-linked-list.md) - - [Memory safety of BTreeMap's `btree::node` module](./challenges/0006-btree-node.md) diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 6f252e9bd4bfa..6f29ce23eba73 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -18,7 +18,6 @@ This is one of the main modules used for implementing the `BTreeMap` collection, The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.: 1. `LeafNode::new` -1. `NodeRef::new_internal` 1. `NodeRef::as_internal_mut` 1. `NodeRef::len` 1. `NodeRef::ascend` @@ -37,7 +36,6 @@ The memory safety of all public functions (especially safe ones) containing unsa 1. `Handle::right_edge` 1. `Handle::left_kv` 1. `Handle::right_kv` -1. `Handle::insert_recursing` 1. `Handle::descend` 1. `Handle::into_kv` 1. `Handle::key_mut` @@ -45,6 +43,11 @@ The memory safety of all public functions (especially safe ones) containing unsa 1. `Handle::into_kv_mut` 1. `Handle::into_kv_valmut` 1. `Handle::kv_mut` + +Verification must be unbounded for functions that use recursion or contain loops, e.g. + +1. `NodeRef::new_internal` +1. `Handle::insert_recursing` 1. `BalancingContext::do_merge` 1. `BalancingContext::merge_tracking_child_edge` 1. `BalancingContext::steal_left` @@ -52,8 +55,6 @@ The memory safety of all public functions (especially safe ones) containing unsa 1. `BalancingContext::bulk_steal_left` 1. `BalancingContext::bulk_steal_right` -The verification must be unbounded for functions that are recursive or that contain loops (e.g. `Handle::insert_recursing`). - ### List of UBs All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):