From 962b36ba90acf2916da8a6d9af1214ef6a426418 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Aug 2024 10:31:06 +0200 Subject: [PATCH 1/3] Challenge proposal: NonNull (#52) --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0006-nonnull.md | 84 ++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 doc/src/challenges/0006-nonnull.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index d5885d4ec7bb7..160ba000dbaed 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -18,5 +18,6 @@ - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [Inductive data type](./challenges/0005-linked-list.md) + - [Safety of NonNull](./challenges/0006-nonnull.md) - [Contracts for SmallSort](./challenges/0008-smallsort.md) - [Memory safety of String](./challenges/0010-string.md) diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md new file mode 100644 index 0000000000000..1e5d8c7bb32c4 --- /dev/null +++ b/doc/src/challenges/0006-nonnull.md @@ -0,0 +1,84 @@ +# Challenge 6: Safety of NonNull + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/53) +- **Start date:** *2024-08-16* +- **End date:** *2024-12-10* + +------------------- + + +## Goal + +Verify absence of undefined behavior of the [`ptr::NonNull` module](https://github.com/rust-lang/rust/blob/master/library/core/src/ptr/non_null.rs). +Most of its functions are marked `unsafe`, yet they are used in 62 other modules +of the standard library. + +### Success Criteria + +Prove absence of undefined behavior of the following 48 public functions. You +may wish to do so by attaching pre- and postconditions to these, and then (if +needed by the tooling that you choose to use) adding verification harnesses. + +1. `NonNull::add` +2. `NonNull::addr` +3. `NonNull::align_offset` +4. `NonNull::as_mut<'a>` +5. `NonNull::as_mut_ptr` +6. `NonNull::as_non_null_ptr` +7. `NonNull::as_ptr` +8. `NonNull::as_ref<'a>` +9. `NonNull::as_uninit_mut<'a>` +10. `NonNull::as_uninit_ref<'a>` +11. `NonNull::as_uninit_slice<'a>` +12. `NonNull::as_uninit_slice_mut<'a>` +13. `NonNull::byte_add` +14. `NonNull::byte_offset_from` +15. `NonNull::byte_offset` +16. `NonNull::byte_sub` +17. `NonNull::cast` +18. `NonNull::copy_from_nonoverlapping` +19. `NonNull::copy_from` +20. `NonNull::copy_to_nonoverlapping` +21. `NonNull::copy_to` +22. `NonNull::dangling` +23. `NonNull::drop_in_place` +24. `NonNull::from_raw_parts` +25. `NonNull::get_unchecked_mut` +26. `NonNull::is_aligned_to` +27. `NonNull::is_aligned` +28. `NonNull::is_empty` +29. `NonNull::len` +30. `NonNull::map_addr` +31. `NonNull::new_unchecked` +32. `NonNull::new` +33. `NonNull::offset_from` +34. `NonNull::offset` +35. `NonNull::read_unaligned` +36. `NonNull::read_volatile` +37. `NonNull::read` +38. `NonNull::replace` +39. `NonNull::slice_from_raw_parts` +40. `NonNull::sub_ptr` +41. `NonNull::sub` +42. `NonNull::swap` +43. `NonNull::to_raw_parts` +44. `NonNull::with_addr` +45. `NonNull::write_bytes` +46. `NonNull::write_unaligned` +47. `NonNull::write_volatile` +48. `NonNull::write` + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From e0d66762a74964548a7e1784bb545c2744e7e8d9 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 27 Aug 2024 13:03:22 -0400 Subject: [PATCH 2/3] Challenge Proposal: `core::time::Duration` (#73) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0009-duration.md | 72 +++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 doc/src/challenges/0009-duration.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 160ba000dbaed..d42f059fa416b 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -20,4 +20,5 @@ - [Inductive data type](./challenges/0005-linked-list.md) - [Safety of NonNull](./challenges/0006-nonnull.md) - [Contracts for SmallSort](./challenges/0008-smallsort.md) + - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - [Memory safety of String](./challenges/0010-string.md) diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md new file mode 100644 index 0000000000000..e2af60ec6c1bb --- /dev/null +++ b/doc/src/challenges/0009-duration.md @@ -0,0 +1,72 @@ +# Challenge 9: Safe abstractions for `core::time::Duration` + +- **Status:** Open +- **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72) +- **Start date:** *2024-08-20* +- **End date:** *2024-12-20* + +------------------- + + +## Goal + +Write function contracts for `core::time::Duration` that can be used as safe abstractions. +Even though the majority of `Duration` methods are safe, many of them are safe abstractions over unsafe code. + +For instance, the `new` method is implemented as follows in v1.3.0: +```rust +pub const fn new(secs: u64, nanos: u32) -> Duration { + if nanos < NANOS_PER_SEC { + // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds(nanos) } } + } else { + let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) { + Some(secs) => secs, + None => panic!("overflow in Duration::new"), + }; + let nanos = nanos % NANOS_PER_SEC; + // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds(nanos) } } + } +} +``` + +### Success Criteria + +Write a [type invariant](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html) for the struct `Duration`. Write function contracts for the following public functions. + +1. `Duration::new(secs: u64, nanos: u32) -> Duration` +2. `Duration::from_secs(secs: u64) -> Duration` +3. `Duration::from_millis(millis: u64) -> Duration` +4. `Duration::from_micros(micros: u64) -> Duration` +5. `Duration::from_nanos(nanos: u64) -> Duration` + +6. `Duration::as_secs(&self) -> u64` +7. `Duration::as_millis(&self) -> u128` +8. `Duration::as_micros(&self) -> u128` +9. `Duration::as_nanos(&self) -> u128` +10. `Duration::subsec_millis(&self) -> u32` +11. `Duration::subsec_micros(&self) -> u32` +12. `Duration::subsec_nanos(&self) -> u32` + +13. `Duration::checked_add(&self, rhs: Duration) -> Option` +14. `Duration::checked_sub(&self, rhs: Duration) -> Option` +15. `Duration::checked_mul(&self, rhs: u32) -> Option` +16. `Duration::checked_div(&self, rhs: u32) -> Option` + +The memory safety and the contracts of the above listed functions must be verified +for all possible input values. + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From b588f710c3aad3492d3c5ee40082424a6c3121cb Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 27 Aug 2024 13:33:23 -0400 Subject: [PATCH 3/3] `NonZero` Challenge (#70) 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: Felipe R. Monteiro --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0012-nonzero.md | 87 ++++++++++++++++++++++++++++++ 2 files changed, 88 insertions(+) create mode 100644 doc/src/challenges/0012-nonzero.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index d42f059fa416b..1c20f2c3f1c72 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -22,3 +22,4 @@ - [Contracts for SmallSort](./challenges/0008-smallsort.md) - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - [Memory safety of String](./challenges/0010-string.md) + - [Safety of NonZero](./challenges/0012-nonzero.md) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md new file mode 100644 index 0000000000000..f5d2dadf84437 --- /dev/null +++ b/doc/src/challenges/0012-nonzero.md @@ -0,0 +1,87 @@ +# Challenge 12: Safety of `NonZero` + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2024-08-23* +- **End date:** *2024-12-10* + +------------------- + +## Goal + +Verify the safety of `NonZero` in `core::num`. + +### Assumptions + +`new` and `get` leverage `transmute_unchecked`, so verifying the safety of these methods would require verifying that transmutations are safe. This task is out of scope for this challenge (instead, it's work for [Challenge 1](0001-core-transmutation.md)). For this challenge, for a transmutation from type `T` to type `U`, it suffices to write and verify a contract that `T` and `U` have the same size. + +You may assume that each `NonZeroInner` type upholds the safety conditions of the `ZeroablePrimitive` trait. Specifically, you need not verify that the integer primitives which implement `ZeroablePrimitive` are valid when 0, or that transmutations to the `Option` type are sound. + +### Success Criteria + +#### Part 1: `new` and `new_unchecked` + +Verify the safety and correctness of `NonZero::new` and `NonZero::new_unchecked`. + +Specifically, write and verify contracts specifying the following: +1. The preconditions specified by the `SAFETY` comments are upheld. +2. For an input `n`: + a. A `NonZero` object is created if and only if the input was nonzero. + b. The value of the `NonZeroInner` object equals `n`. + +#### Part 2: Other Uses of `unsafe` + +Verify the safety of the following functions and methods (all located within `core::num::nonzero`): + +| Function | +|--------- | +| `max` | +| `min` | +| `clamp` | +| `bitor` (all 3 implementations) | +| `count_ones` | +| `rotate_left` | +| `rotate_right` | +| `swap_bytes` | +| `reverse_bits` | +| `from_be` | +| `from_le` | +| `to_be` | +| `to_le` | +| `checked_mul` | +| `saturating_mul` | +| `unchecked_mul` | +| `checked_pow` | +| `saturating_pow` | +| `neg` | +| `checked_add` | +| `saturating_add` | +| `unchecked_add` | +| `checked_next_power_of_two` | +| `midpoint` | +| `isqrt` | +| `abs` | +| `checked_abs` | +| `overflowing_abs` | +| `saturating_abs` | +| `wrapping_abs` | +| `unsigned_abs` | +| `checked_neg` | +| `overflowing_neg` | +| `wrapping_neg` | +| `from_mut` | +| `from_mut_unchecked` | + +You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so! + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, all proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Invoking undefined behavior via compiler intrinsics. +* Reading from uninitialized memory. +* Producing an invalid value. + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above.