Challenge 5: Verify functions iterating over inductive data type: linked_list
- Status: Open
- Tracking Issue: #29
- Start date: 24/07/01
- End date: 24/12/10
Goal
Verify the memory safety of alloc::collections::linked_list functions 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:
- 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 in addition to the ones listed above.