Add unsafe blocks in unsafe Thread::new · model-checking/verify-rust-std@7a0b2fb (original) (raw)
`@@ -22,36 +22,40 @@ pub struct Thread {
`
22
22
``
23
23
`impl Thread {
`
24
24
`// unsafe: see thread::Builder::spawn_unchecked for safety requirements
`
25
``
`-
#[allow(unsafe_op_in_unsafe_fn)]
`
26
``
`-
// FIXME: check the internal safety
`
27
25
`pub unsafe fn new(stack: usize, p: Box<dyn FnOnce()>) -> io::Result {
`
28
26
`let p = Box::into_raw(Box::new(p));
`
29
27
``
30
28
`// CreateThread rounds up values for the stack size to the nearest page size (at least 4kb).
`
31
29
`// If a value of zero is given then the default stack size is used instead.
`
32
``
`-
let ret = c::CreateThread(
`
33
``
`-
ptr::null_mut(),
`
34
``
`-
stack,
`
35
``
`-
Some(thread_start),
`
36
``
`-
p as *mut _,
`
37
``
`-
c::STACK_SIZE_PARAM_IS_A_RESERVATION,
`
38
``
`-
ptr::null_mut(),
`
39
``
`-
);
`
40
``
`-
let ret = HandleOrNull::from_raw_handle(ret);
`
``
30
`` +
// SAFETY: thread_start has the right ABI for a thread's entry point.
``
``
31
`` +
// p is simply passed through to the new thread without being touched.
``
``
32
`+
let ret = unsafe {
`
``
33
`+
let ret = c::CreateThread(
`
``
34
`+
ptr::null_mut(),
`
``
35
`+
stack,
`
``
36
`+
Some(thread_start),
`
``
37
`+
p as *mut _,
`
``
38
`+
c::STACK_SIZE_PARAM_IS_A_RESERVATION,
`
``
39
`+
ptr::null_mut(),
`
``
40
`+
);
`
``
41
`+
HandleOrNull::from_raw_handle(ret)
`
``
42
`+
};
`
41
43
`return if let Ok(handle) = ret.try_into() {
`
42
44
`Ok(Thread { handle: Handle::from_inner(handle) })
`
43
45
`} else {
`
44
46
`// The thread failed to start and as a result p was not consumed. Therefore, it is
`
45
47
`// safe to reconstruct the box so that it gets deallocated.
`
46
``
`-
drop(Box::from_raw(p));
`
``
48
`+
unsafe { drop(Box::from_raw(p)) };
`
47
49
`Err(io::Error::last_os_error())
`
48
50
`};
`
49
51
``
50
52
`unsafe extern "system" fn thread_start(main: *mut c_void) -> u32 {
`
51
53
`// Next, reserve some stack space for if we otherwise run out of stack.
`
52
54
` stack_overflow::reserve_stack();
`
53
55
`// Finally, let's run some code.
`
54
``
`-
Box::from_raw(main as *mut Box<dyn FnOnce()>)();
`
``
56
`+
// SAFETY: We are simply recreating the box that was leaked earlier.
`
``
57
`` +
// It's the responsibility of the one who call Thread::new to ensure this is safe to call here.
``
``
58
`+
unsafe { Box::from_raw(main as *mut Box<dyn FnOnce()>)() };
`
55
59
`0
`
56
60
`}
`
57
61
`}
`