From bed3267b5f87e1f12676d1555ee51409460e65ab Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Fri, 6 Dec 2024 08:03:38 +0100 Subject: [PATCH 1/4] Update 0003-pointer-arithmentic.md (#210) --- doc/src/challenges/0003-pointer-arithmentic.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 902d3a7f55752..b85c4f45e1a78 100644 --- 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 | From e70a892165226dfc06abe2bc9b4473501e223928 Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Fri, 6 Dec 2024 05:41:26 -0800 Subject: [PATCH 2/4] Close Challenge 11 (#206) Resolves #59 ### Changes * Marked Challenge 11 as resolved * Changed the end date of the challenge * Added the contributors --- doc/src/challenges/0011-floats-ints.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md index 1a1c872b88f1f..2d80453e25c3c 100644 --- 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) ------------------- From eae6c8bc2a4393c0c6704603038b00253c83a118 Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Fri, 6 Dec 2024 20:57:54 +0100 Subject: [PATCH 3/4] Update tools.md (#207) --- doc/src/tools.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools.md b/doc/src/tools.md index 1e86d661ccb2e..0eaba7c40d4d8 100644 --- 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: From ee9b7c311ab494329382b483e35cec622d7e565e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Dec 2024 14:30:39 -0800 Subject: [PATCH 4/4] Enable harnesses that were blocked by Kani's spurious CEX (#211) In #148 and #122, we had to comment out a few harnesses due to the issue https://github.com/model-checking/kani/issues/3670. But now that the fix has been pushed, we can enable them. --- library/core/src/slice/iter.rs | 22 ++++++++++++++-------- library/core/src/str/pattern.rs | 5 ----- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 5005563233d2d..5ea9204a28fd0 100644 --- 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 index 7792bfbbac718..6540608344fa1 100644 --- 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 ); } - */ }