non-deterministically truncate reads/writes

Author: RalfJung

src/shims/files.rs

@@ -167,6 +167,11 @@ pub trait FileDescription: std::fmt::Debug + FileDescriptionExt {
         throw_unsup_format!("cannot write to {}", self.name());
     }
 
+    /// Determines whether this FD non-deterministically has its reads and writes shortened.
+    fn nondet_short_accesses(&self) -> bool {
+        true
+    }
+
     /// Seeks to the given offset (which can be relative to the beginning, end, or current position).
     /// Returns the new position from the start of the stream.
     fn seek<'tcx>(

src/shims/unix/fd.rs

@@ -4,6 +4,7 @@
 use std::io;
 use std::io::ErrorKind;
 
+use rand::Rng;
 use rustc_abi::Size;
 
 use crate::helpers::check_min_vararg_count;
@@ -263,9 +264,18 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             return this.set_last_error_and_return(LibcError("EBADF"), dest);
         };
 
+        // Non-deterministically decide to further reduce the count, simulating a partial read (but
+        // never to 0, that has different behavior).
+        let count =
+            if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() {
+                count / 2
+            } else {
+                count
+            };
+
         trace!("read: FD mapped to {fd:?}");
         // We want to read at most `count` bytes. We are sure that `count` is not negative
-        // because it was a target's `usize`. Also we are sure that its smaller than
+        // because it was a target's `usize`. Also we are sure that it's smaller than
         // `usize::MAX` because it is bounded by the host's `isize`.
 
         let finish = {
@@ -328,6 +338,15 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             return this.set_last_error_and_return(LibcError("EBADF"), dest);
         };
 
+        // Non-deterministically decide to further reduce the count, simulating a partial write (but
+        // never to 0, that has different behavior).
+        let count =
+            if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() {
+                count / 2
+            } else {
+                count
+            };
+
         let finish = {
             let dest = dest.clone();
             callback!(

src/shims/unix/linux_like/eventfd.rs

@@ -37,6 +37,11 @@ impl FileDescription for EventFd {
         "event"
     }
 
+    fn nondet_short_accesses(&self) -> bool {
+        // We always read and write exactly one `u64`.
+        false
+    }
+
     fn close<'tcx>(
         self,
         _communicate_allowed: bool,

src/shims/windows/fs.rs

@@ -462,6 +462,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
         };
         let io_status_info = this.project_field_named(&io_status_block, "Information")?;
 
+        // It seems like short writes are not a thing on Windows, so we don't truncate `count` here.
+        // FIXME: if we are on a Unix host, short host writes are still visible to the program!
+
         let finish = {
             let io_status = io_status.clone();
             let io_status_info = io_status_info.clone();
@@ -491,7 +494,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 }}
             )
         };
-
         desc.write(this.machine.communicate(), buf, count.try_into().unwrap(), this, finish)?;
 
         // Return status is written to `dest` and `io_status_block` on callback completion.
@@ -556,6 +558,16 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
         };
         let io_status_info = this.project_field_named(&io_status_block, "Information")?;
 
+        let fd = match handle {
+            Handle::File(fd) => fd,
+            _ => this.invalid_handle("NtWriteFile")?,
+        };
+
+        let Some(desc) = this.machine.fds.get(fd) else { this.invalid_handle("NtReadFile")? };
+
+        // It seems like short reads are not a thing on Windows, so we don't truncate `count` here.
+        // FIXME: if we are on a Unix host, short host reads are still visible to the program!
+
         let finish = {
             let io_status = io_status.clone();
             let io_status_info = io_status_info.clone();
@@ -585,14 +597,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 }}
             )
         };
-
-        let fd = match handle {
-            Handle::File(fd) => fd,
-            _ => this.invalid_handle("NtWriteFile")?,
-        };
-
-        let Some(desc) = this.machine.fds.get(fd) else { this.invalid_handle("NtReadFile")? };
-
         desc.read(this.machine.communicate(), buf, count.try_into().unwrap(), this, finish)?;
 
         // See NtWriteFile for commentary on this

tests/fail-dep/libc/libc-epoll-data-race.rs

@@ -10,6 +10,9 @@ use std::convert::TryInto;
 use std::thread;
 use std::thread::spawn;
 
+#[path = "../../utils/libc.rs"]
+mod libc_utils;
+
 #[track_caller]
 fn check_epoll_wait<const N: usize>(epfd: i32, expected_notifications: &[(u32, u64)]) {
     let epoll_event = libc::epoll_event { events: 0, u64: 0 };
@@ -69,12 +72,12 @@ fn main() {
         unsafe { VAL_ONE = 41 };
 
         let data = "abcde".as_bytes().as_ptr();
-        let res = unsafe { libc::write(fds_a[0], data as *const libc::c_void, 5) };
+        let res = unsafe { libc_utils::write_all(fds_a[0], data as *const libc::c_void, 5) };
         assert_eq!(res, 5);
 
         unsafe { VAL_TWO = 51 };
 
-        let res = unsafe { libc::write(fds_b[0], data as *const libc::c_void, 5) };
+        let res = unsafe { libc_utils::write_all(fds_b[0], data as *const libc::c_void, 5) };
         assert_eq!(res, 5);
     });
     thread::yield_now();

tests/fail-dep/libc/socketpair_block_read_twice.rs

@@ -1,12 +1,17 @@
 //@ignore-target: windows # No libc socketpair on Windows
 //~^ERROR: deadlocked
-//~^^ERROR: deadlocked
 // test_race depends on a deterministic schedule.
 //@compile-flags: -Zmiri-deterministic-concurrency
 //@error-in-other-file: deadlock
+//@error-in-other-file: deadlock
+//@error-in-other-file: deadlock
+//@require-annotations-for-level: error
 
 use std::thread;
 
+#[path = "../../utils/libc.rs"]
+mod libc_utils;
+
 // Test the behaviour of a thread being blocked on read, get unblocked, then blocked again.
 
 // The expected execution is
@@ -23,22 +28,27 @@ fn main() {
     let thread1 = thread::spawn(move || {
         // Let this thread block on read.
         let mut buf: [u8; 3] = [0; 3];
-        let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
+        let res = unsafe {
+            libc_utils::read_all(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+            //~^NOTE: inside closure
+        };
         assert_eq!(res, 3);
         assert_eq!(&buf, "abc".as_bytes());
     });
     let thread2 = thread::spawn(move || {
         // Let this thread block on read.
         let mut buf: [u8; 3] = [0; 3];
-        let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
-        //~^ERROR: deadlocked
+        let res = unsafe {
+            libc_utils::read_all(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+            //~^NOTE: inside closure
+        };
         assert_eq!(res, 3);
         assert_eq!(&buf, "abc".as_bytes());
     });
     let thread3 = thread::spawn(move || {
         // Unblock thread1 by writing something.
         let data = "abc".as_bytes().as_ptr();
-        let res = unsafe { libc::write(fds[0], data as *const libc::c_void, 3) };
+        let res = unsafe { libc_utils::write_all(fds[0], data as *const libc::c_void, 3) };
         assert_eq!(res, 3);
     });
     thread1.join().unwrap();

tests/fail-dep/libc/socketpair_block_read_twice.stderr

@@ -1,3 +1,17 @@
+error: the evaluated program deadlocked
+  --> tests/fail-dep/libc/../../utils/libc.rs:LL:CC
+   |
+LL |         let res = libc::read(fd, buf.add(read_so_far), count - read_so_far);
+   |                                                                           ^ this thread got stuck here
+   |
+   = note: BACKTRACE on thread `unnamed-ID`:
+   = note: inside `libc_utils::read_all` at tests/fail-dep/libc/../../utils/libc.rs:LL:CC
+note: inside closure
+  --> tests/fail-dep/libc/socketpair_block_read_twice.rs:LL:CC
+   |
+LL |             libc_utils::read_all(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 error: the evaluated program deadlocked
   --> RUSTLIB/std/src/sys/pal/PLATFORM/thread.rs:LL:CC
    |
@@ -11,23 +25,22 @@ LL |         let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) };
 note: inside `main`
   --> tests/fail-dep/libc/socketpair_block_read_twice.rs:LL:CC
    |
-LL |     thread2.join().unwrap();
+LL |     thread1.join().unwrap();
    |     ^^^^^^^^^^^^^^
 
 error: the evaluated program deadlocked
+  --> tests/fail-dep/libc/../../utils/libc.rs:LL:CC
+   |
+LL |         let res = libc::read(fd, buf.add(read_so_far), count - read_so_far);
+   |                                                                           ^ this thread got stuck here
    |
-   = note: this thread got stuck here
-   = note: (no span available)
    = note: BACKTRACE on thread `unnamed-ID`:
-
-error: the evaluated program deadlocked
+   = note: inside `libc_utils::read_all` at tests/fail-dep/libc/../../utils/libc.rs:LL:CC
+note: inside closure
   --> tests/fail-dep/libc/socketpair_block_read_twice.rs:LL:CC
    |
-LL |         let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
-   |                                                                                                 ^ this thread got stuck here
-   |
-   = note: BACKTRACE on thread `unnamed-ID`:
-   = note: inside closure at tests/fail-dep/libc/socketpair_block_read_twice.rs:LL:CC
+LL |             libc_utils::read_all(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 error: the evaluated program deadlocked
    |

tests/fail-dep/libc/socketpair_block_write_twice.rs

@@ -4,9 +4,14 @@
 // test_race depends on a deterministic schedule.
 //@compile-flags: -Zmiri-deterministic-concurrency
 //@error-in-other-file: deadlock
+//@error-in-other-file: deadlock
+//@require-annotations-for-level: error
 
 use std::thread;
 
+#[path = "../../utils/libc.rs"]
+mod libc_utils;
+
 // Test the behaviour of a thread being blocked on write, get unblocked, then blocked again.
 
 // The expected execution is
@@ -21,25 +26,28 @@ fn main() {
     assert_eq!(res, 0);
     let arr1: [u8; 212992] = [1; 212992];
     // Exhaust the space in the buffer so the subsequent write will block.
-    let res = unsafe { libc::write(fds[0], arr1.as_ptr() as *const libc::c_void, 212992) };
+    let res =
+        unsafe { libc_utils::write_all(fds[0], arr1.as_ptr() as *const libc::c_void, 212992) };
     assert_eq!(res, 212992);
     let thread1 = thread::spawn(move || {
         let data = "abc".as_bytes().as_ptr();
         // The write below will be blocked because the buffer is already full.
-        let res = unsafe { libc::write(fds[0], data as *const libc::c_void, 3) };
+        let res = unsafe { libc_utils::write_all(fds[0], data as *const libc::c_void, 3) };
         assert_eq!(res, 3);
     });
     let thread2 = thread::spawn(move || {
         let data = "abc".as_bytes().as_ptr();
         // The write below will be blocked because the buffer is already full.
-        let res = unsafe { libc::write(fds[0], data as *const libc::c_void, 3) };
-        //~^ERROR: deadlocked
+        let res = unsafe { libc_utils::write_all(fds[0], data as *const libc::c_void, 3) };
+        //~^NOTE: inside closure
         assert_eq!(res, 3);
     });
     let thread3 = thread::spawn(move || {
         // Unblock thread1 by freeing up some space.
         let mut buf: [u8; 3] = [0; 3];
-        let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
+        let res = unsafe {
+            libc_utils::read_all(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+        };
         assert_eq!(res, 3);
         assert_eq!(buf, [1, 1, 1]);
     });

tests/fail-dep/libc/socketpair_block_write_twice.stderr

@@ -21,13 +21,18 @@ error: the evaluated program deadlocked
    = note: BACKTRACE on thread `unnamed-ID`:
 
 error: the evaluated program deadlocked
-  --> tests/fail-dep/libc/socketpair_block_write_twice.rs:LL:CC
+  --> tests/fail-dep/libc/../../utils/libc.rs:LL:CC
    |
-LL |         let res = unsafe { libc::write(fds[0], data as *const libc::c_void, 3) };
-   |                                                                              ^ this thread got stuck here
+LL |         let res = libc::write(fd, buf.add(written_so_far), count - written_so_far);
+   |                                                                                  ^ this thread got stuck here
    |
    = note: BACKTRACE on thread `unnamed-ID`:
-   = note: inside closure at tests/fail-dep/libc/socketpair_block_write_twice.rs:LL:CC
+   = note: inside `libc_utils::write_all` at tests/fail-dep/libc/../../utils/libc.rs:LL:CC
+note: inside closure
+  --> tests/fail-dep/libc/socketpair_block_write_twice.rs:LL:CC
+   |
+LL |         let res = unsafe { libc_utils::write_all(fds[0], data as *const libc::c_void, 3) };
+   |                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 error: the evaluated program deadlocked
    |

tests/pass-dep/libc/libc-epoll-blocking.rs

@@ -6,6 +6,9 @@ use std::convert::TryInto;
 use std::thread;
 use std::thread::spawn;
 
+#[path = "../../utils/libc.rs"]
+mod libc_utils;
+
 // This is a set of testcases for blocking epoll.
 
 fn main() {
@@ -97,7 +100,7 @@ fn test_epoll_block_then_unblock() {
     let thread1 = spawn(move || {
         thread::yield_now();
         let data = "abcde".as_bytes().as_ptr();
-        let res = unsafe { libc::write(fds[1], data as *const libc::c_void, 5) };
+        let res = unsafe { libc_utils::write_all(fds[1], data as *const libc::c_void, 5) };
         assert_eq!(res, 5);
     });
     check_epoll_wait::<1>(epfd, &[(expected_event, expected_value)], 10);
@@ -130,7 +133,7 @@ fn test_notification_after_timeout() {
 
     // Trigger epoll notification after timeout.
     let data = "abcde".as_bytes().as_ptr();
-    let res = unsafe { libc::write(fds[1], data as *const libc::c_void, 5) };
+    let res = unsafe { libc_utils::write_all(fds[1], data as *const libc::c_void, 5) };
     assert_eq!(res, 5);
 
     // Check the result of the notification.