Merge branch 'main' into verify-intrinsics

celinval · Dec 6, 2024 · e3dc274 · e3dc274
2 parents e7f1e66 + ee9b7c3
commit e3dc274
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 17 deletions.
diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md
@@ -88,7 +88,7 @@ At least 3 of the following usages were proven safe:
 
 | Function          | Location      |
 |-------------------|---------------|
-| \[u8\]::is_asc_ii | core::slice   |
+| \[u8\]::is_ascii | core::slice   |
 | String::remove    | alloc::string |
  | Vec::swap_remove | alloc::vec |
  | Option::as_slice | core::option |

diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
@@ -1,11 +1,12 @@
 # Challenge 11: Safety of Methods for Numeric Primitive Types
 
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
 - **Start date:** *2024/08/20*
-- **End date:** *2025/04/10*
+- **End date:** *2024/12/04*
 - **Reward:** *N/A*
+- **Contributors**: [Rajath M Kotyal](https://github.com/rajathkotyal), [Yen-Yun Wu](https://github.com/Yenyun035), [Lanfei Ma](https://github.com/lanfeima), [Junfeng Jin](https://github.com/MWDZ)
 
 -------------------
 

diff --git a/doc/src/tools.md b/doc/src/tools.md
@@ -4,7 +4,7 @@ The verification tool ecosystem for Rust is rapidly growing, and we welcome the
 In this chapter, you can find a list of tools that have already been approved for new solutions,
 what is their CI current status, as well as more details on how to use them.
 
-If the tool you would like to add a new tool to the list of tool applications,
+If you would like to add a new tool to the list of tool applications,
 please see the [Tool Application](general-rules.md#tool-applications) section.
 
 ## Approved tools:

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
@@ -3604,18 +3604,24 @@ mod verify {
                 }
 
                 check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked());
-                //check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
-                //check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
+                check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
+                check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
 
                 // FIXME: The functions that are commented out are currently failing verification.
                 // Debugging the issue is currently blocked by:
                 // https://github.com/model-checking/kani/issues/3670
                 //
                 // Public functions that call safe abstraction `make_slice`.
-                // check_safe_abstraction!(check_as_slice, $ty, as_slice);
-                // check_safe_abstraction!(check_as_ref, $ty, as_ref);
+                check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.as_slice();
+                });
+                check_safe_abstraction!(check_as_ref, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.as_ref();
+                });
 
-                // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
+                check_safe_abstraction!(check_advance_back_by, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.advance_back_by(kani::any());
+                });
 
                 check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.is_empty();
@@ -3626,12 +3632,12 @@ mod verify {
                 check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.size_hint();
                 });
-                //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
-                //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
+                check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
+                check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
                 check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.next_back();
                 });
-                //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
+                check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
                 check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.next();
                 });

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
@@ -2000,10 +2000,6 @@ pub mod verify {
         }
     }
 
-    /* This harness check `small_slice_eq` with dangling pointer to slice
-       with zero size. Kani finds safety issue of `small_slice_eq` in this
-       harness and hence the proof will fail.
-
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
     #[kani::unwind(4)]
@@ -2022,5 +2018,4 @@ pub mod verify {
             true
         );
     }
-    */
 }