From 955577c4d968687e6b671c2e69d2157912cd3570 Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Thu, 12 Dec 2024 10:32:12 -0800 Subject: [PATCH] Proofs for `Vec::swap_remove`, `Option::as_slice`, and `VecDeque::swap` (#212) Resolves: #76 ### Changes * Adds proofs for the following functions using raw pointer operations: * `Vec::swap_remove` * `Option::as_slice` * `VecDeque::swap` * ideally the usages should have been verified by stubbing the contracts for reaw pointer operations like `byte_add`, `add` and `offset`, but stubbing cannot be done for these functions at this time due to https://github.com/model-checking/kani/issues/3732 * Marks Challenge 3 as Resolved and changes its end date. * Adds contributors. #### PoCs: * `Vec::swap_remove`: @MayureshJoshi25 * `Option::as_slice`, `VecDeque::swap`: @stogaru By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Yifei Wang <1277495324@qq.com> Co-authored-by: MayureshJoshi25 Co-authored-by: Yifei Wang <40480373+xsxszab@users.noreply.github.com> Co-authored-by: Michael Tautschnig Co-authored-by: szlee118 Co-authored-by: szlee118 <33711285+szlee118@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro --- .../challenges/0003-pointer-arithmentic.md | 5 +- .../alloc/src/collections/vec_deque/mod.rs | 43 +++++++++++++++++ library/alloc/src/vec/mod.rs | 46 +++++++++++++++++++ library/core/src/option.rs | 27 +++++++++++ 4 files changed, 119 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index b85c4f45e1a7..65fb3074cf48 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -1,10 +1,11 @@ # Challenge 3: Verifying Raw Pointer Arithmetic Operations -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76) - **Start date:** *2024/06/24* -- **End date:** *2025/04/10* +- **End date:** *2024/12/11* - **Reward:** *N/A* +- **Contributors:** [Surya Togaru](https://github.com/stogaru), [Yifei Wang](https://github.com/xsxszab), [Szu-Yu Lee](https://github.com/szlee118), [Mayuresh Joshi](https://github.com/MayureshJoshi25) ------------------- diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index cf51a84bb6f2..a0d34f8bb8c4 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -58,6 +58,9 @@ mod spec_from_iter; #[cfg(test)] mod tests; +#[cfg(kani)] +use core::kani; + /// A double-ended queue implemented with a growable ring buffer. /// /// The "default" usage of this type as a queue is to use [`push_back`] to add to @@ -3079,3 +3082,43 @@ impl From<[T; N]> for VecDeque { deq } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::kani; + use crate::collections::VecDeque; + + #[kani::proof] + fn check_vecdeque_swap() { + // The array's length is set to an arbitrary value, which defines its size. + // In this case, implementing a dynamic array is not possible using any_array + // The more elements in the array the longer the veification time. + const ARRAY_LEN: usize = 40; + let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let mut deque: VecDeque = VecDeque::from(arr); + let len = deque.len(); + + // Generate valid indices within bounds + let i = kani::any_where(|&x: &usize| x < len); + let j = kani::any_where(|&x: &usize| x < len); + + // Capture the elements at i and j before the swap + let elem_i_before = deque[i]; + let elem_j_before = deque[j]; + + // Perform the swap + deque.swap(i, j); + + // Postcondition: Verify elements have swapped places + assert_eq!(deque[i], elem_j_before); + assert_eq!(deque[j], elem_i_before); + + // Ensure other elements remain unchanged + let k = kani::any_where(|&x: &usize| x < len); + if k != i && k != j { + assert!(deque[k] == arr[k]); + } + } + +} diff --git a/library/alloc/src/vec/mod.rs b/library/alloc/src/vec/mod.rs index 990b7e8f7612..370c412af83a 100644 --- a/library/alloc/src/vec/mod.rs +++ b/library/alloc/src/vec/mod.rs @@ -4032,3 +4032,49 @@ impl TryFrom> for [T; N] { Ok(array) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::kani; + use crate::vec::Vec; + + // Size chosen for testing the empty vector (0), middle element removal (1) + // and last element removal (2) cases while keeping verification tractable + const ARRAY_LEN: usize = 3; + + #[kani::proof] + pub fn verify_swap_remove() { + + // Creating a vector directly from a fixed length arbitrary array + let mut arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let mut vect = Vec::from(&arr); + + // Recording the original length and a copy of the vector for validation + let original_len = vect.len(); + let original_vec = vect.clone(); + + // Generating a nondeterministic index which is guaranteed to be within bounds + let index: usize = kani::any_where(|x| *x < original_len); + + let removed = vect.swap_remove(index); + + // Verifying that the length of the vector decreases by one after the operation is performed + assert!(vect.len() == original_len - 1, "Length should decrease by 1"); + + // Verifying that the removed element matches the original element at the index + assert!(removed == original_vec[index], "Removed element should match original"); + + // Verifying that the removed index now contains the element originally at the vector's last index if applicable + if index < original_len - 1 { + assert!(vect[index] == original_vec[original_len - 1], "Index should contain last element"); + } + + // Check that all other unaffected elements remain unchanged + let k = kani::any_where(|&x: &usize| x < original_len - 1); + if k != index { + assert!(vect[k] == arr[k]); + } + + } +} diff --git a/library/core/src/option.rs b/library/core/src/option.rs index 29d1956af955..052cff05faf8 100644 --- a/library/core/src/option.rs +++ b/library/core/src/option.rs @@ -2572,3 +2572,30 @@ impl [Option; N] { self.try_map(core::convert::identity) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + use crate::option::Option; + + #[kani::proof] + fn verify_as_slice() { + if kani::any() { + // Case 1: Option is Some + let value: u32 = kani::any(); + let some_option: Option = Some(value); + + let slice = some_option.as_slice(); + assert_eq!(slice.len(), 1); // The slice should have exactly one element + assert_eq!(slice[0], value); // The value in the slice should match + } else { + // Case 2: Option is None + let none_option: Option = None; + + let empty_slice = none_option.as_slice(); + assert_eq!(empty_slice.len(), 0); // The slice should be empty + assert!(empty_slice.is_empty()); // Explicit check for emptiness + } + } +}