From 6a021146f2a3a8f66e3116d8d932a3496eb0fb90 Mon Sep 17 00:00:00 2001 From: Samuel Thomas Date: Mon, 25 Nov 2024 12:46:52 -0600 Subject: [PATCH 01/11] add challenge for safety of primitive conversions --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0014-convert-num.md | 138 +++++++++++++++++++++++++ 2 files changed, 139 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0014-convert-num.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 4e15d7cacdb50..d917b907e3d54 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -26,4 +26,4 @@ - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) - [13: Safety of `CStr`](./challenges/0013-cstr.md) - + - [14: Safety of Primitive Conversions](./challenges/0013-convert-num.md) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md new file mode 100644 index 0000000000000..4999630accc8c --- /dev/null +++ b/doc/src/challenges/0014-convert-num.md @@ -0,0 +1,138 @@ +# Challenge 14: Safety of Primitive Conversions + +- **Status:** Open +- **Tracking Issue:** *None* +- **Start date:** *TBD* +- **End date:** *TBD* +- **Prize:** *TBD* + +------------------- + +## Goal + +Verify the safety of number conversions in `core::convert::num`. + +There are three classes of conversions that use unsafe code. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses. + +### Success Criteria + +#### Safety for Float to Int + +```rust +macro_rules! impl_float_to_int { + ($Float:ty => $($Int:ty),+) => { + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl private::Sealed for $Float {} + $( + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl FloatToInt<$Int> for $Float { + #[inline] + unsafe fn to_int_unchecked(self) -> $Int { + // SAFETY: the safety contract must be upheld by the caller. + unsafe { crate::intrinsics::float_to_int_unchecked(self) } + } + } + )+ + } +} +``` + +The safety constraints referenced in the comments are that the input value must: ([[https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked][docs]]) +- Not be NaN +- Not be infinite +- Be representable in the return type Int, after truncating off its fractional part + +The intrinsic corresponds to the [[https://llvm.org/docs/LangRef.html#fptoui-to-instruction][fptoui]]/[[https://llvm.org/docs/LangRef.html#fptosi-to-instruction][fptosi]] LLVM instructions, which may be useful for reference. + +#### NonZero Conversions + +Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions. + +There are two macros that implement these conversions: an infallible and fallible version. These are all of the types for which conversions are implemented. You should be able to use the macro to generate the function contracts. + +non-zero unsigned integer -> non-zero unsigned integer +- `impl_nonzero_int_from_nonzero_int!(u8 => u16);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u32);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u8 => usize);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u32);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u16 => usize);` +- `impl_nonzero_int_from_nonzero_int!(u32 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u32 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u64 => u128);` + +non-zero signed integer -> non-zero signed integer +- `impl_nonzero_int_from_nonzero_int!(i8 => i16);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i32);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i8 => isize);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i32);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i16 => isize);` +- `impl_nonzero_int_from_nonzero_int!(i32 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i32 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i64 => i128);` + +non-zero unsigned -> non-zero signed integer +- `impl_nonzero_int_from_nonzero_int!(u8 => i16);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i32);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u8 => isize);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i32);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u32 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u32 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u64 => i128);` + +There are also the fallible versions. + +unsigned non-zero integer -> unsigned non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);` +- `impl_nonzero_int_try_from_nonzero_int!(u32 => u8, u16, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(u64 => u8, u16, u32, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(u128 => u8, u16, u32, u64, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(usize => u8, u16, u32, u64, u128);` + +signed non-zero integer -> signed non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(i16 => i8);` +- `impl_nonzero_int_try_from_nonzero_int!(i32 => i8, i16, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(i64 => i8, i16, i32, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(i128 => i8, i16, i32, i64, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(isize => i8, i16, i32, i64, i128);` + +unsigned non-zero integer -> signed non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(u8 => i8);` +- `impl_nonzero_int_try_from_nonzero_int!(u16 => i8, i16, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u32 => i8, i16, i32, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u64 => i8, i16, i32, i64, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u128 => i8, i16, i32, i64, i128, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(usize => i8, i16, i32, i64, i128, isize);` + +signed non-zero integer -> unsigned non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(i8 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i16 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);` + +### 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 09255640f9ae273230043ae17c2c33f328eca1fb Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Tue, 10 Dec 2024 11:38:19 -0600 Subject: [PATCH 02/11] Update doc/src/SUMMARY.md Co-authored-by: Michael Tautschnig --- doc/src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index d917b907e3d54..d2b265a81217d 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -26,4 +26,4 @@ - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) - [13: Safety of `CStr`](./challenges/0013-cstr.md) - - [14: Safety of Primitive Conversions](./challenges/0013-convert-num.md) + - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md) From 880de4c8eda79e33002d0c45c921acdf3dd32152 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Tue, 10 Dec 2024 11:41:36 -0600 Subject: [PATCH 03/11] add dates --- doc/src/challenges/0014-convert-num.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 4999630accc8c..de352c0d0f64b 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -2,8 +2,8 @@ - **Status:** Open - **Tracking Issue:** *None* -- **Start date:** *TBD* -- **End date:** *TBD* +- **Start date:** 2024/12/15 +- **End date:** 2025/2/28 - **Prize:** *TBD* ------------------- From 1199e83aa0194a35c91e2138a8f575b402d6a258 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Tue, 10 Dec 2024 11:47:38 -0600 Subject: [PATCH 04/11] fix markdown links --- doc/src/challenges/0014-convert-num.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index de352c0d0f64b..c5e6dd79a5ac8 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -37,12 +37,14 @@ macro_rules! impl_float_to_int { } ``` -The safety constraints referenced in the comments are that the input value must: ([[https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked][docs]]) +The safety constraints referenced in the comments are that the input value must: - Not be NaN - Not be infinite - Be representable in the return type Int, after truncating off its fractional part + +These constraints are given in the [documenation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). -The intrinsic corresponds to the [[https://llvm.org/docs/LangRef.html#fptoui-to-instruction][fptoui]]/[[https://llvm.org/docs/LangRef.html#fptosi-to-instruction][fptosi]] LLVM instructions, which may be useful for reference. +The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. #### NonZero Conversions From 695748291428271b8090b3bcafc02dce779ce45c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Dec 2024 11:36:04 +0100 Subject: [PATCH 05/11] Update doc/src/challenges/0014-convert-num.md --- doc/src/challenges/0014-convert-num.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index c5e6dd79a5ac8..15766d58b2ab6 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -1,7 +1,7 @@ # Challenge 14: Safety of Primitive Conversions - **Status:** Open -- **Tracking Issue:** *None* +- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220 - **Start date:** 2024/12/15 - **End date:** 2025/2/28 - **Prize:** *TBD* From 02bad407fe5574c770e4a895dc838545c6e6cb0a Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Wed, 11 Dec 2024 16:14:45 -0600 Subject: [PATCH 06/11] Update doc/src/challenges/0014-convert-num.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0014-convert-num.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 15766d58b2ab6..09a7c78ccdfa1 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -42,7 +42,7 @@ The safety constraints referenced in the comments are that the input value must: - Not be infinite - Be representable in the return type Int, after truncating off its fractional part -These constraints are given in the [documenation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). +These constraints are given in the [documentation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. From b2c545f2743caed5c1e6939410b1106f506b4eb2 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Fri, 13 Dec 2024 11:18:17 -0600 Subject: [PATCH 07/11] move list of contracts up to Success Criteria --- doc/src/challenges/0014-convert-num.md | 67 +++++++++++++------------- 1 file changed, 33 insertions(+), 34 deletions(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 09a7c78ccdfa1..1bab0cc1ca9ad 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -16,41 +16,9 @@ There are three classes of conversions that use unsafe code. All conversions use ### Success Criteria -#### Safety for Float to Int - -```rust -macro_rules! impl_float_to_int { - ($Float:ty => $($Int:ty),+) => { - #[unstable(feature = "convert_float_to_int", issue = "67057")] - impl private::Sealed for $Float {} - $( - #[unstable(feature = "convert_float_to_int", issue = "67057")] - impl FloatToInt<$Int> for $Float { - #[inline] - unsafe fn to_int_unchecked(self) -> $Int { - // SAFETY: the safety contract must be upheld by the caller. - unsafe { crate::intrinsics::float_to_int_unchecked(self) } - } - } - )+ - } -} -``` - -The safety constraints referenced in the comments are that the input value must: -- Not be NaN -- Not be infinite -- Be representable in the return type Int, after truncating off its fractional part - -These constraints are given in the [documentation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). - -The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. - -#### NonZero Conversions - Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions. -There are two macros that implement these conversions: an infallible and fallible version. These are all of the types for which conversions are implemented. You should be able to use the macro to generate the function contracts. +Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: `impl_nonzero_int_from_nonzero_int!` and `impl_nonzero_int_try_from_nonzero_int!`. For contracts using `impl_nonzero_int_from_nonzero_int!` there should be one contract for each implemented conversion. For contracts using `impl_nonzero_int_try_from_nonzero_int!` there should be two contracts for each conversion, one with an assumption that guarantees the absence of a panic and one with no assumption that is marked by a `#[should_panic]` attribute. non-zero unsigned integer -> non-zero unsigned integer - `impl_nonzero_int_from_nonzero_int!(u8 => u16);` @@ -93,7 +61,7 @@ non-zero unsigned -> non-zero signed integer - `impl_nonzero_int_from_nonzero_int!(u32 => i128);` - `impl_nonzero_int_from_nonzero_int!(u64 => i128);` -There are also the fallible versions. +There are also the fallible versions. Remember to cover both the panicking and non-panicking cases. unsigned non-zero integer -> unsigned non-zero integer - `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);` @@ -125,6 +93,37 @@ signed non-zero integer -> unsigned non-zero integer - `impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);` - `impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);` + +#### Safety for Float to Int + +```rust +macro_rules! impl_float_to_int { + ($Float:ty => $($Int:ty),+) => { + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl private::Sealed for $Float {} + $( + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl FloatToInt<$Int> for $Float { + #[inline] + unsafe fn to_int_unchecked(self) -> $Int { + // SAFETY: the safety contract must be upheld by the caller. + unsafe { crate::intrinsics::float_to_int_unchecked(self) } + } + } + )+ + } +} +``` + +The safety constraints referenced in the comments are that the input value must: +- Not be NaN +- Not be infinite +- Be representable in the return type Int, after truncating off its fractional part + +These constraints are given in the [documentation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). + +The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. + ### List of UBs In addition to any properties called out as `SAFETY` comments in the source From d5f2fb93e54ee4d06c59fa6613196041b24d7004 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Mon, 16 Dec 2024 17:39:26 -0600 Subject: [PATCH 08/11] Update doc/src/challenges/0014-convert-num.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0014-convert-num.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 1bab0cc1ca9ad..2539127b741de 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -18,7 +18,11 @@ There are three classes of conversions that use unsafe code. All conversions use Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions. -Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: `impl_nonzero_int_from_nonzero_int!` and `impl_nonzero_int_try_from_nonzero_int!`. For contracts using `impl_nonzero_int_from_nonzero_int!` there should be one contract for each implemented conversion. For contracts using `impl_nonzero_int_try_from_nonzero_int!` there should be two contracts for each conversion, one with an assumption that guarantees the absence of a panic and one with no assumption that is marked by a `#[should_panic]` attribute. +Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: `impl_nonzero_int_from_nonzero_int!` and `impl_nonzero_int_try_from_nonzero_int!`. + +For each invocation of `impl_nonzero_int_from_nonzero_int!`, prove that the conversion it implements does not cause undefined behavior nor panic. For example, for `impl_nonzero_int_from_nonzero_int!(u8 => u16);`, prove that calling `NonZero::from(small: NonZero)` does not cause undefined behavior nor panic for an arbitrary `small` that satisfies the `NonZero` type invariant. + +For each invocation of `impl_nonzero_int_try_from_nonzero_int!`, prove that the conversion it implements does not cause undefined behavior. For example, for `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);`, prove that calling `NonZero::try_from(value: NonZero)` does not cause undefined behavior for an arbitrary `value` that satisfies the `NonZero` type invariant. Additionally, prove that if the `value` does not fit into the target type (e.g., `value` is too large to fit into a `NonZero`) that the function panics. non-zero unsigned integer -> non-zero unsigned integer - `impl_nonzero_int_from_nonzero_int!(u8 => u16);` From 0de2dd05e627e58d6c9051238902b4aeeb50fdfd Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Mon, 16 Dec 2024 17:39:37 -0600 Subject: [PATCH 09/11] Update doc/src/challenges/0014-convert-num.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0014-convert-num.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 2539127b741de..5027621f8d960 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -16,6 +16,7 @@ There are three classes of conversions that use unsafe code. All conversions use ### Success Criteria +#### NonZero Conversions Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions. Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: `impl_nonzero_int_from_nonzero_int!` and `impl_nonzero_int_try_from_nonzero_int!`. From 5c8d331880d91886618f1bafab88da24921b5828 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Mon, 16 Dec 2024 17:39:55 -0600 Subject: [PATCH 10/11] Update doc/src/challenges/0014-convert-num.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0014-convert-num.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index 5027621f8d960..dc692b195d0c6 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -128,6 +128,11 @@ The safety constraints referenced in the comments are that the input value must: These constraints are given in the [documentation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. +Prove safety for each of the following conversions: +impl_float_to_int!(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); +impl_float_to_int!(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); +impl_float_to_int!(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); +impl_float_to_int!(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); ### List of UBs From 041e9d2bb585c554f99e5bdc564bed8af1643899 Mon Sep 17 00:00:00 2001 From: Cole Vick Date: Mon, 16 Dec 2024 17:48:38 -0600 Subject: [PATCH 11/11] formatting fixes --- doc/src/challenges/0014-convert-num.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index dc692b195d0c6..e6dc78666718d 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -12,7 +12,7 @@ Verify the safety of number conversions in `core::convert::num`. -There are three classes of conversions that use unsafe code. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses. +There are two conversions that use unsafe code: conversion from NonZero integer to NonZero integer and conversion from floating point number to integer. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses. ### Success Criteria @@ -129,10 +129,11 @@ These constraints are given in the [documentation](https://doc.rust-lang.org/std The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. Prove safety for each of the following conversions: -impl_float_to_int!(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); -impl_float_to_int!(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); -impl_float_to_int!(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); -impl_float_to_int!(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize); + +- `impl_float_to_int!(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` ### List of UBs