Remove wrapper functions from c.rs · model-checking/verify-rust-std@642c69b (original) (raw)
`@@ -221,15 +221,6 @@ fn random_number() -> usize {
`
221
221
`}
`
222
222
`}
`
223
223
``
224
``
`` -
// Abstracts over ReadFileEx
and WriteFileEx
``
225
``
`-
type AlertableIoFn = unsafe extern "system" fn(
`
226
``
`-
BorrowedHandle<'_>,
`
227
``
`-
*mut core::ffi::c_void,
`
228
``
`-
u32,
`
229
``
`-
*mut c::OVERLAPPED,
`
230
``
`-
c::LPOVERLAPPED_COMPLETION_ROUTINE,
`
231
``
`-
) -> c::BOOL;
`
232
``
-
233
224
`impl AnonPipe {
`
234
225
`pub fn handle(&self) -> &Handle {
`
235
226
`&self.inner
`
`@@ -244,7 +235,10 @@ impl AnonPipe {
`
244
235
`pub fn read(&self, buf: &mut [u8]) -> io::Result {
`
245
236
`let result = unsafe {
`
246
237
`let len = crate::cmp::min(buf.len(), u32::MAX as usize) as u32;
`
247
``
`-
self.alertable_io_internal(c::ReadFileEx, buf.as_mut_ptr() as _, len)
`
``
238
`+
let ptr = buf.as_mut_ptr();
`
``
239
`+
self.alertable_io_internal(|overlapped, callback| {
`
``
240
`+
c::ReadFileEx(self.inner.as_raw_handle(), ptr, len, overlapped, callback)
`
``
241
`+
})
`
248
242
`};
`
249
243
``
250
244
`match result {
`
`@@ -260,7 +254,10 @@ impl AnonPipe {
`
260
254
`pub fn read_buf(&self, mut buf: BorrowedCursor<'_>) -> io::Result<()> {
`
261
255
`let result = unsafe {
`
262
256
`let len = crate::cmp::min(buf.capacity(), u32::MAX as usize) as u32;
`
263
``
`-
self.alertable_io_internal(c::ReadFileEx, buf.as_mut().as_mut_ptr() as _, len)
`
``
257
`+
let ptr = buf.as_mut().as_mut_ptr().cast::();
`
``
258
`+
self.alertable_io_internal(|overlapped, callback| {
`
``
259
`+
c::ReadFileEx(self.inner.as_raw_handle(), ptr, len, overlapped, callback)
`
``
260
`+
})
`
264
261
`};
`
265
262
``
266
263
`match result {
`
`@@ -295,7 +292,9 @@ impl AnonPipe {
`
295
292
`pub fn write(&self, buf: &[u8]) -> io::Result {
`
296
293
`unsafe {
`
297
294
`let len = crate::cmp::min(buf.len(), u32::MAX as usize) as u32;
`
298
``
`-
self.alertable_io_internal(c::WriteFileEx, buf.as_ptr() as _, len)
`
``
295
`+
self.alertable_io_internal(|overlapped, callback| {
`
``
296
`+
c::WriteFileEx(self.inner.as_raw_handle(), buf.as_ptr(), len, overlapped, callback)
`
``
297
`+
})
`
299
298
`}
`
300
299
`}
`
301
300
``
`@@ -323,12 +322,9 @@ impl AnonPipe {
`
323
322
`` /// [ReadFileEx
]: https://docs.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-readfileex
``
324
323
`` /// [WriteFileEx
]: https://docs.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-writefileex
``
325
324
`/// [Asynchronous Procedure Call]: https://docs.microsoft.com/en-us/windows/win32/sync/asynchronous-procedure-calls
`
326
``
`-
#[allow(unsafe_op_in_unsafe_fn)]
`
327
325
`unsafe fn alertable_io_internal(
`
328
326
`&self,
`
329
``
`-
io: AlertableIoFn,
`
330
``
`-
buf: *mut core::ffi::c_void,
`
331
``
`-
len: u32,
`
``
327
`+
io: impl FnOnce(&mut c::OVERLAPPED, c::LPOVERLAPPED_COMPLETION_ROUTINE) -> c::BOOL,
`
332
328
`) -> io::Result {
`
333
329
`// Use "alertable I/O" to synchronize the pipe I/O.
`
334
330
`// This has four steps.
`
`@@ -366,20 +362,25 @@ impl AnonPipe {
`
366
362
`lpOverlapped: *mut c::OVERLAPPED,
`
367
363
`) {
`
368
364
`` // Set async_result
using a pointer smuggled through hEvent
.
``
369
``
`-
let result =
`
370
``
`-
AsyncResult { error: dwErrorCode, transferred: dwNumberOfBytesTransferred };
`
371
``
`-
*(*lpOverlapped).hEvent.cast::<Option>() = Some(result);
`
``
365
`+
// SAFETY:
`
``
366
`+
// At this point, the OVERLAPPED struct will have been written to by the OS,
`
``
367
`` +
// except for our hEvent
field which we set to a valid AsyncResult pointer (see below)
``
``
368
`+
unsafe {
`
``
369
`+
let result =
`
``
370
`+
AsyncResult { error: dwErrorCode, transferred: dwNumberOfBytesTransferred };
`
``
371
`+
*(*lpOverlapped).hEvent.cast::<Option>() = Some(result);
`
``
372
`+
}
`
372
373
`}
`
373
374
``
374
375
`// STEP 1: Start the I/O operation.
`
375
``
`-
let mut overlapped: c::OVERLAPPED = crate::mem::zeroed();
`
``
376
`+
let mut overlapped: c::OVERLAPPED = unsafe { crate::mem::zeroed() };
`
376
377
`` // hEvent
is unused by ReadFileEx
and WriteFileEx
.
``
377
378
`// Therefore the documentation suggests using it to smuggle a pointer to the callback.
`
378
379
` overlapped.hEvent = core::ptr::addr_of_mut!(async_result) as *mut _;
`
379
380
``
380
381
`// Asynchronous read of the pipe.
`
381
382
`` // If successful, callback
will be called once it completes.
``
382
``
`-
let result = io(self.inner.as_handle(), buf, len, &mut overlapped, Some(callback));
`
``
383
`+
let result = io(&mut overlapped, Some(callback));
`
383
384
`if result == c::FALSE {
`
384
385
`// We can return here because the call failed.
`
385
386
`// After this we must not return until the I/O completes.
`
`@@ -390,7 +391,7 @@ impl AnonPipe {
`
390
391
`let result = loop {
`
391
392
`// STEP 2: Enter an alertable state.
`
392
393
`` // The second parameter of SleepEx
is used to make this sleep alertable.
``
393
``
`-
c::SleepEx(c::INFINITE, c::TRUE);
`
``
394
`+
unsafe { c::SleepEx(c::INFINITE, c::TRUE) };
`
394
395
`if let Some(result) = async_result {
`
395
396
`break result;
`
396
397
`}
`