forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 16
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into floats-ints-challenge
- Loading branch information
Showing
4 changed files
with
246 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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<T>::add` | ||
2. `NonNull<T>::addr` | ||
3. `NonNull<T>::align_offset` | ||
4. `NonNull<T>::as_mut<'a>` | ||
5. `NonNull<T>::as_mut_ptr` | ||
6. `NonNull<T>::as_non_null_ptr` | ||
7. `NonNull<T>::as_ptr` | ||
8. `NonNull<T>::as_ref<'a>` | ||
9. `NonNull<T>::as_uninit_mut<'a>` | ||
10. `NonNull<T>::as_uninit_ref<'a>` | ||
11. `NonNull<T>::as_uninit_slice<'a>` | ||
12. `NonNull<T>::as_uninit_slice_mut<'a>` | ||
13. `NonNull<T>::byte_add` | ||
14. `NonNull<T>::byte_offset_from<U: ?Sized>` | ||
15. `NonNull<T>::byte_offset` | ||
16. `NonNull<T>::byte_sub` | ||
17. `NonNull<T>::cast<U>` | ||
18. `NonNull<T>::copy_from_nonoverlapping` | ||
19. `NonNull<T>::copy_from` | ||
20. `NonNull<T>::copy_to_nonoverlapping` | ||
21. `NonNull<T>::copy_to` | ||
22. `NonNull<T>::dangling` | ||
23. `NonNull<T>::drop_in_place` | ||
24. `NonNull<T>::from_raw_parts` | ||
25. `NonNull<T>::get_unchecked_mut<I>` | ||
26. `NonNull<T>::is_aligned_to` | ||
27. `NonNull<T>::is_aligned` | ||
28. `NonNull<T>::is_empty` | ||
29. `NonNull<T>::len` | ||
30. `NonNull<T>::map_addr` | ||
31. `NonNull<T>::new_unchecked` | ||
32. `NonNull<T>::new` | ||
33. `NonNull<T>::offset_from` | ||
34. `NonNull<T>::offset` | ||
35. `NonNull<T>::read_unaligned` | ||
36. `NonNull<T>::read_volatile` | ||
37. `NonNull<T>::read` | ||
38. `NonNull<T>::replace` | ||
39. `NonNull<T>::slice_from_raw_parts` | ||
40. `NonNull<T>::sub_ptr` | ||
41. `NonNull<T>::sub` | ||
42. `NonNull<T>::swap` | ||
43. `NonNull<T>::to_raw_parts` | ||
44. `NonNull<T>::with_addr` | ||
45. `NonNull<T>::write_bytes` | ||
46. `NonNull<T>::write_unaligned` | ||
47. `NonNull<T>::write_volatile` | ||
48. `NonNull<T>::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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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<Duration>` | ||
14. `Duration::checked_sub(&self, rhs: Duration) -> Option<Duration>` | ||
15. `Duration::checked_mul(&self, rhs: u32) -> Option<Duration>` | ||
16. `Duration::checked_div(&self, rhs: u32) -> Option<Duration>` | ||
|
||
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. |