Skip to content

Commit 6a02114

Browse files
sgpthomassgpthomas
committed
add challenge for safety of primitive conversions
1 parent 5e44e6e commit 6a02114

File tree

2 files changed

+139
-1
lines changed

2 files changed

+139
-1
lines changed

‎doc/src/SUMMARY.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,4 +26,4 @@
2626
- [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
2727
- [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
2828
- [13: Safety of `CStr`](./challenges/0013-cstr.md)
29-
29+
- [14: Safety of Primitive Conversions](./challenges/0013-convert-num.md)

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

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# Challenge 14: Safety of Primitive Conversions
2+
3+
- **Status:** Open
4+
- **Tracking Issue:** *None*
5+
- **Start date:** *TBD*
6+
- **End date:** *TBD*
7+
- **Prize:** *TBD*
8+
9+
-------------------
10+
11+
## Goal
12+
13+
Verify the safety of number conversions in `core::convert::num`.
14+
15+
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.
16+
17+
### Success Criteria
18+
19+
#### Safety for Float to Int
20+
21+
```rust
22+
macro_rules! impl_float_to_int {
23+
($Float:ty => $($Int:ty),+) => {
24+
#[unstable(feature = "convert_float_to_int", issue = "67057")]
25+
impl private::Sealed for $Float {}
26+
$(
27+
#[unstable(feature = "convert_float_to_int", issue = "67057")]
28+
impl FloatToInt<$Int> for $Float {
29+
#[inline]
30+
unsafe fn to_int_unchecked(self) -> $Int {
31+
// SAFETY: the safety contract must be upheld by the caller.
32+
unsafe { crate::intrinsics::float_to_int_unchecked(self) }
33+
}
34+
}
35+
)+
36+
}
37+
}
38+
```
39+
40+
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]])
41+
- Not be NaN
42+
- Not be infinite
43+
- Be representable in the return type Int, after truncating off its fractional part
44+
45+
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.
46+
47+
#### NonZero Conversions
48+
49+
Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions.
50+
51+
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.
52+
53+
non-zero unsigned integer -> non-zero unsigned integer
54+
- `impl_nonzero_int_from_nonzero_int!(u8 => u16);`
55+
- `impl_nonzero_int_from_nonzero_int!(u8 => u32);`
56+
- `impl_nonzero_int_from_nonzero_int!(u8 => u64);`
57+
- `impl_nonzero_int_from_nonzero_int!(u8 => u128);`
58+
- `impl_nonzero_int_from_nonzero_int!(u8 => usize);`
59+
- `impl_nonzero_int_from_nonzero_int!(u16 => u32);`
60+
- `impl_nonzero_int_from_nonzero_int!(u16 => u64);`
61+
- `impl_nonzero_int_from_nonzero_int!(u16 => u128);`
62+
- `impl_nonzero_int_from_nonzero_int!(u16 => usize);`
63+
- `impl_nonzero_int_from_nonzero_int!(u32 => u64);`
64+
- `impl_nonzero_int_from_nonzero_int!(u32 => u128);`
65+
- `impl_nonzero_int_from_nonzero_int!(u64 => u128);`
66+
67+
non-zero signed integer -> non-zero signed integer
68+
- `impl_nonzero_int_from_nonzero_int!(i8 => i16);`
69+
- `impl_nonzero_int_from_nonzero_int!(i8 => i32);`
70+
- `impl_nonzero_int_from_nonzero_int!(i8 => i64);`
71+
- `impl_nonzero_int_from_nonzero_int!(i8 => i128);`
72+
- `impl_nonzero_int_from_nonzero_int!(i8 => isize);`
73+
- `impl_nonzero_int_from_nonzero_int!(i16 => i32);`
74+
- `impl_nonzero_int_from_nonzero_int!(i16 => i64);`
75+
- `impl_nonzero_int_from_nonzero_int!(i16 => i128);`
76+
- `impl_nonzero_int_from_nonzero_int!(i16 => isize);`
77+
- `impl_nonzero_int_from_nonzero_int!(i32 => i64);`
78+
- `impl_nonzero_int_from_nonzero_int!(i32 => i128);`
79+
- `impl_nonzero_int_from_nonzero_int!(i64 => i128);`
80+
81+
non-zero unsigned -> non-zero signed integer
82+
- `impl_nonzero_int_from_nonzero_int!(u8 => i16);`
83+
- `impl_nonzero_int_from_nonzero_int!(u8 => i32);`
84+
- `impl_nonzero_int_from_nonzero_int!(u8 => i64);`
85+
- `impl_nonzero_int_from_nonzero_int!(u8 => i128);`
86+
- `impl_nonzero_int_from_nonzero_int!(u8 => isize);`
87+
- `impl_nonzero_int_from_nonzero_int!(u16 => i32);`
88+
- `impl_nonzero_int_from_nonzero_int!(u16 => i64);`
89+
- `impl_nonzero_int_from_nonzero_int!(u16 => i128);`
90+
- `impl_nonzero_int_from_nonzero_int!(u32 => i64);`
91+
- `impl_nonzero_int_from_nonzero_int!(u32 => i128);`
92+
- `impl_nonzero_int_from_nonzero_int!(u64 => i128);`
93+
94+
There are also the fallible versions.
95+
96+
unsigned non-zero integer -> unsigned non-zero integer
97+
- `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);`
98+
- `impl_nonzero_int_try_from_nonzero_int!(u32 => u8, u16, usize);`
99+
- `impl_nonzero_int_try_from_nonzero_int!(u64 => u8, u16, u32, usize);`
100+
- `impl_nonzero_int_try_from_nonzero_int!(u128 => u8, u16, u32, u64, usize);`
101+
- `impl_nonzero_int_try_from_nonzero_int!(usize => u8, u16, u32, u64, u128);`
102+
103+
signed non-zero integer -> signed non-zero integer
104+
- `impl_nonzero_int_try_from_nonzero_int!(i16 => i8);`
105+
- `impl_nonzero_int_try_from_nonzero_int!(i32 => i8, i16, isize);`
106+
- `impl_nonzero_int_try_from_nonzero_int!(i64 => i8, i16, i32, isize);`
107+
- `impl_nonzero_int_try_from_nonzero_int!(i128 => i8, i16, i32, i64, isize);`
108+
- `impl_nonzero_int_try_from_nonzero_int!(isize => i8, i16, i32, i64, i128);`
109+
110+
unsigned non-zero integer -> signed non-zero integer
111+
- `impl_nonzero_int_try_from_nonzero_int!(u8 => i8);`
112+
- `impl_nonzero_int_try_from_nonzero_int!(u16 => i8, i16, isize);`
113+
- `impl_nonzero_int_try_from_nonzero_int!(u32 => i8, i16, i32, isize);`
114+
- `impl_nonzero_int_try_from_nonzero_int!(u64 => i8, i16, i32, i64, isize);`
115+
- `impl_nonzero_int_try_from_nonzero_int!(u128 => i8, i16, i32, i64, i128, isize);`
116+
- `impl_nonzero_int_try_from_nonzero_int!(usize => i8, i16, i32, i64, i128, isize);`
117+
118+
signed non-zero integer -> unsigned non-zero integer
119+
- `impl_nonzero_int_try_from_nonzero_int!(i8 => u8, u16, u32, u64, u128, usize);`
120+
- `impl_nonzero_int_try_from_nonzero_int!(i16 => u8, u16, u32, u64, u128, usize);`
121+
- `impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);`
122+
- `impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);`
123+
- `impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);`
124+
- `impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);`
125+
126+
### List of UBs
127+
128+
In addition to any properties called out as `SAFETY` comments in the source
129+
code,
130+
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):
131+
132+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
133+
* Reading from uninitialized memory.
134+
* Mutating immutable bytes.
135+
* Producing an invalid value
136+
137+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
138+
in addition to the ones listed above.

0 commit comments

Comments
 (0)