From 98d0bef556025add4a8d8486f1b07c7cc0200b52 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 11 Jun 2024 18:24:04 -0400 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Michael Tautschnig --- doc/src/intrinsics-memory.md | 70 ++++++++++++++++++------------------ 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/doc/src/intrinsics-memory.md b/doc/src/intrinsics-memory.md index 49e44e7329acb..d34055f66472e 100644 --- a/doc/src/intrinsics-memory.md +++ b/doc/src/intrinsics-memory.md @@ -1,6 +1,6 @@ # Challenge 2: Verify the memory safery of core intrinsics using raw pointers -- **Status:** *One of the following: [Open | Resolved | Expired]* Open +- **Status:** Open - **Tracking Issue:** *Link to issue* - **Start date:** *YY/MM/DD* - **End date:** *YY/MM/DD* @@ -10,42 +10,42 @@ ## Goal -Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract and verify their usage in the standard library are in fact safe. +Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract. Verify their usage in the standard library is in fact safe. -### Success Criteria* +### Success Criteria 1. All the following intrinsic functions must be annotated with safety contracts. 2. Any fallback intrinsic implementation must be verified. -3. For intrinsics modeled in the tool of choice, explain how its implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter. -4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audit, and the list of (implicit and explicit) properties that are guarantee. -5. The verification of each intrinsics should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usages. +3. For intrinsics modeled in the tool of choice, explain how their implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter. +4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audited, and the list of (implicit and explicit) properties that are guaranteed. +5. The verification of each intrinsic should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usage. -#### Functions for verification +### Functions for verification |Function |Location | |--- |--- | |typed_swap | core::intrisics | -vtable_size| core::intrisics | -vtable_align| core::intrisics | -copy_nonoverlapping| core::intrisics | -copy| core::intrisics | -write_bytes| core::intrisics | -size_of_val| core::intrisics | -arith_offset| core::intrisics | -volatile_copy_nonoverlapping_memory| core::intrisics | -volatile_copy_memory| core::intrisics | -volatile_set_memory| core::intrisics | -volatile_load| core::intrisics | -volatile_store| core::intrisics | -unaligned_volatile_load| core::intrisics | -unaligned_volatile_store| core::intrisics | -compare_bytes| core::intrisics | -min_align_of_val| core::intrisics | -ptr_offset_from| core::intrisics | -ptr_offset_from_unsigned| core::intrisics | -read_via_copy| core::intrisics | -write_via_move| core::intrisics | +|vtable_size| core::intrisics | +|vtable_align| core::intrisics | +|copy_nonoverlapping| core::intrisics | +|copy| core::intrisics | +|write_bytes| core::intrisics | +|size_of_val| core::intrisics | +|arith_offset| core::intrisics | +|volatile_copy_nonoverlapping_memory| core::intrisics | +|volatile_copy_memory| core::intrisics | +|volatile_set_memory| core::intrisics | +|volatile_load| core::intrisics | +|volatile_store| core::intrisics | +|unaligned_volatile_load| core::intrisics | +|unaligned_volatile_store| core::intrisics | +|compare_bytes| core::intrisics | +|min_align_of_val| core::intrisics | +|ptr_offset_from| core::intrisics | +|ptr_offset_from_unsigned| core::intrisics | +|read_via_copy| core::intrisics | +|write_via_move| core::intrisics | | | | @@ -55,10 +55,10 @@ write_via_move| core::intrisics | |Function |Location | |--- |--- | |copy_from_slice | core::slice | -parse_u64_into | std::fmt | -swap | core::mem | -align_of_val | core::mem | -zeroed | core::mem::maybe_uninit | +|parse_u64_into | std::fmt | +|swap | core::mem | +|align_of_val | core::mem | +|zeroed | core::mem::maybe_uninit | | | | @@ -68,10 +68,10 @@ zeroed | core::mem::maybe_uninit | |Function |Location | |--- |--- | |copy_from_slice | std::ptr | -parse_u64_into | std::ptr | -swap | std::ptr | -align_of_val | std::ptr | -zeroed | std::ptr | +|parse_u64_into | std::ptr | +|swap | std::ptr | +|align_of_val | std::ptr | +|zeroed | std::ptr | | | |