From 5f2798ea25521dc74b3d8c0cbe495f03832259d5 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 10 Jul 2024 11:23:14 -0500 Subject: [PATCH] Add a challenge for `linked_list` (#30) > Please add a description of your PR. > If this is a solution to an open challenge, please explain your solution. > > Don't forget to check our book to ensure your solution satisfy the overall > requirements as well as the challenge success criteria. > By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0005-linked-list.md | 50 ++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 doc/src/challenges/0005-linked-list.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 992ca46a7c818..21713571824ce 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -16,3 +16,4 @@ - [Core Transmutation](./challenges/0001-core-transmutation.md) - [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) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md new file mode 100644 index 0000000000000..5701acb7b82d2 --- /dev/null +++ b/doc/src/challenges/0005-linked-list.md @@ -0,0 +1,50 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *24/07/01* +- **End date:** *24/12/10* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate the its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clearn | alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](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.