New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refine challenges #247

Open

thanhnguyen-aws wants to merge 11 commits into model-checking:main from thanhnguyen-aws:refinechallenges

thanhnguyen-aws commented Feb 17, 2025 •

edited

Loading

In this PR, I refined the existing challenges by:

Added the missing contracts and harnesses for 3 functions write, write_bytes, write_unaligned for the NonNull challenge, then changed the status of this challenge to "resolved".
Edited some descriptions of smallsort
Removed the (optional) correctness checking in NonZero challenge. I will create a separate challenge for it.
I don't add more functions to existing challenge to keep each challenge under manageable size. I will create other challenges for functions inside the same modules as the existing ones.

Resolves #ISSUE-NUMBER

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.


          refine challenges

thanhnguyen-aws requested a review from a team as a code owner

February 17, 2025 18:11

carolynzech reviewed

View reviewed changes

doc/src/challenges/0012-nonzero.md Outdated Show resolved Hide resolved

carolynzech requested changes

View reviewed changes

doc/src/challenges/0006-nonnull.md

@@ @@ -1,6 +1,6 @@ @@
               # Challenge 6: Safety of NonNull
-              - **Status:** Open
+              - **Status:** Resolved

carolynzech Feb 17, 2025

Are we sure this is done? I haven't checked, but IIRC there hasn't been work on it since the CMU students left, and I'd be surprised if they finished it and didn't mark it as resolved themselves.

Author

thanhnguyen-aws Feb 19, 2025

I checked and added the contracts and harnesses for the 3 remaining functions. I believe is is considered resolved now. The code of the harnesses is a little bit messy but it is not hard to be cleaned up later.

doc/src/challenges/0014-convert-num.md

@@ @@ -1,6 +1,6 @@ @@
               # Challenge 14: Safety of Primitive Conversions
-              - **Status:** Open
+              - **Status:** Resolved

carolynzech Feb 17, 2025

As a high-level comment (applies to all three), we like to give credit to those who contributed to the solution (see https://github.com/model-checking/verify-rust-std/pull/224/files) and close the challenge issues as well.

carolynzech Mar 3, 2025

Now that this is done, you should update the PR description to resolve the corresponding challenge issue.

thanhnguyen-aws added 6 commits

February 18, 2025 17:50


          add missing haenesses for nonnull

6c640a3


          add correctness check for write_bytes

d58fe26


          Merge branch 'main' into refinechallenges

717de12


          remove correctness for NonZero challenge

1e662dc


          add contributors for NonNull

00ba598


          add contributors for Primitive conversions

cedd00c

thanhnguyen-aws requested a review from carolynzech

February 19, 2025 19:13


          fix write_bytes contract for unit

69031dc

carolynzech requested changes

View reviewed changes

carolynzech left a comment

I haven't reviewed the harnesses in-depth yet; focused on the contracts and other changes for now.

library/Cargo.lock Outdated

carolynzech Mar 3, 2025

Please revert these changes.

doc/src/challenges/0006-nonnull.md Outdated

               - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
               - **Start date:** *2024/08/16*
               - **End date:** *2025/04/10*
               - **Reward:** *N/A*
+              - **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), Dhvani Kapadia(https://github.com/Dhvani-Kapadia) and JY(https://github.com/Jimmycreative)

carolynzech Mar 3, 2025

You can give yourself credit too if you wrote some harnesses :) but up to you.

carolynzech Mar 3, 2025 •

edited

Loading

Also, let's use full names (Jiun Chi Yang) instead of JY.

doc/src/challenges/0014-convert-num.md

@@ @@ -1,6 +1,6 @@ @@
               # Challenge 14: Safety of Primitive Conversions
-              - **Status:** Open
+              - **Status:** Resolved

carolynzech Mar 3, 2025

Now that this is done, you should update the PR description to resolve the corresponding challenge issue.

library/core/src/ptr/non_null.rs Outdated

+                      count <= isize::MAX as usize &&
+                      (count as isize).checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+                      (self.as_ptr() as isize).checked_add((count as isize).wrapping_mul(core::mem::size_of::<T>() as isize)).is_some() &&
+                      //(count == 0 || ub_checks::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count as isize) as *const ())) &&

carolynzech Mar 3, 2025

We shouldn't merge commented out code.

library/core/src/ptr/non_null.rs

Comment on lines +1192 to +1193

		#[ensures(\|_\|
		ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(self.as_ptr() as const u8, count size_of::<T>())))]

carolynzech Mar 3, 2025

Not sure about this ensures clause... what's the rationale?

library/core/src/ptr/non_null.rs Outdated

+                      (count as isize).checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+                      (self.as_ptr() as isize).checked_add((count as isize).wrapping_mul(core::mem::size_of::<T>() as isize)).is_some() &&
+                      //(count == 0 || ub_checks::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count as isize) as *const ())) &&
+                      ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) &&

carolynzech Mar 3, 2025

The documentation says:

Behavior is undefined if any of the following conditions are violated:
dst must be valid for writes of count * size_of::() bytes.
dst must be properly aligned.

so this validity check should go for count * size_of::<T>() bytes instead of just count.

BTW, I recommend using is_some_and to chain some of your logic together to make it more readable.

carolynzech Mar 3, 2025

Same comment as above about alignment and the can_write predicate.

library/core/src/ptr/non_null.rs Outdated

+                  #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+                  #[requires(
+                      ub_checks::can_write(self.as_ptr()) &&
+                      self.as_ptr().is_aligned()

carolynzech Mar 3, 2025

can_write already implies that the pointer is aligned:

verify-rust-std/library/core/src/ub_checks.rs

Lines 191 to 198 in dcae9fe

    
               /// Check if a pointer can be written to: 
        
               /// * `dst` must be valid for writes. 
        
               /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the 
        
               ///    case. 
        
               pub fn can_write<T: ?Sized>(dst: *mut T) -> bool { 
        
                   let _ = dst; 
        
                   true 
        
               }

library/core/src/ptr/non_null.rs Outdated

@@ @@ -1217,6 +1234,8 @@ impl<T: ?Sized> NonNull<T> { @@
                   #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
                   #[stable(feature = "non_null_convenience", since = "1.80.0")]
                   #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
+                  #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+                  #[requires(ub_checks::can_write(self.as_ptr()))]

carolynzech Mar 3, 2025

You want can_write_unaligned:

verify-rust-std/library/core/src/ub_checks.rs

Lines 208 to 213 in dcae9fe

    
               /// Check if a pointer can be the target of unaligned writes. 
        
               /// * `dst` must be valid for writes. 
        
               pub fn can_write_unaligned<T: ?Sized>(dst: *mut T) -> bool { 
        
                   let _ = dst; 
        
                   true 
        
               }

thanhnguyen-aws added 3 commits

March 3, 2025 12:41


          Merge branch 'main' into refinechallenges

e03cf73


          update contributor name

972bcb2


          update write functions contracts and harnesses

aa5dd30

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet