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/libc-read-and-uninit-premature-eof.rs

@@ -18,8 +18,9 @@ fn main() {
         let fd = libc::open(cpath.as_ptr(), libc::O_RDONLY);
         assert_ne!(fd, -1);
         let mut buf: MaybeUninit<[u8; 4]> = std::mem::MaybeUninit::uninit();
-        // Read 4 bytes from a 3-byte file.
-        assert_eq!(libc::read(fd, buf.as_mut_ptr().cast::<std::ffi::c_void>(), 4), 3);
+        // Read up to 4 bytes from a 3-byte file.
+        let res = libc::read(fd, buf.as_mut_ptr().cast::<std::ffi::c_void>(), 4);
+        assert!(res > 0 && res <= 3);
         buf.assume_init(); //~ERROR: encountered uninitialized memory, but expected an integer
         assert_eq!(libc::close(fd), 0);
     }

tests/fail-dep/libc/libc_epoll_block_two_thread.rs

@@ -75,9 +75,10 @@ fn main() {
     });
 
     let thread3 = spawn(move || {
+        // Just a single write, so we only wake up one of them.
         let data = "abcde".as_bytes().as_ptr();
         let res = unsafe { libc::write(fds[1], data as *const libc::c_void, 5) };
-        assert_eq!(res, 5);
+        assert!(res > 0 && res <= 5);
     });
 
     thread1.join().unwrap();

tests/fail-dep/libc/socketpair_block_read_twice.rs

@@ -4,6 +4,7 @@
 // test_race depends on a deterministic schedule.
 //@compile-flags: -Zmiri-deterministic-concurrency
 //@error-in-other-file: deadlock
+//@require-annotations-for-level: error
 
 use std::thread;
 
@@ -22,24 +23,26 @@ fn main() {
     assert_eq!(res, 0);
     let thread1 = thread::spawn(move || {
         // Let this thread block on read.
-        let mut buf: [u8; 3] = [0; 3];
+        let mut buf: [u8; 1] = [0; 1];
         let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
-        assert_eq!(res, 3);
-        assert_eq!(&buf, "abc".as_bytes());
+        assert_eq!(res, buf.len().cast_signed());
+        assert_eq!(&buf, "a".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
-        assert_eq!(res, 3);
-        assert_eq!(&buf, "abc".as_bytes());
+        let mut buf: [u8; 1] = [0; 1];
+        let res = unsafe {
+            libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t)
+            //~^ERROR: deadlock
+        };
+        assert_eq!(res, buf.len().cast_signed());
+        assert_eq!(&buf, "a".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) };
-        assert_eq!(res, 3);
+        let data = "a".as_bytes();
+        let res = unsafe { libc::write(fds[0], data.as_ptr() as *const libc::c_void, data.len()) };
+        assert_eq!(res, data.len().cast_signed());
     });
     thread1.join().unwrap();
     thread2.join().unwrap();

tests/fail-dep/libc/socketpair_block_read_twice.stderr

@@ -23,8 +23,8 @@ error: the evaluated program deadlocked
 error: the evaluated program deadlocked
   --> 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
+LL |             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

tests/fail-dep/libc/socketpair_block_write_twice.rs

@@ -4,44 +4,49 @@
 // test_race depends on a deterministic schedule.
 //@compile-flags: -Zmiri-deterministic-concurrency
 //@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
 // 1. Thread 1 blocks.
 // 2. Thread 2 blocks.
 // 3. Thread 3 unblocks both thread 1 and thread 2.
-// 4. Thread 1 reads.
+// 4. Thread 1 writes.
 // 5. Thread 2's `write` can never complete -> deadlocked.
 fn main() {
     let mut fds = [-1, -1];
     let res = unsafe { libc::socketpair(libc::AF_UNIX, libc::SOCK_STREAM, 0, fds.as_mut_ptr()) };
     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();
+        let data = "a".as_bytes();
         // 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) };
-        assert_eq!(res, 3);
+        let res = unsafe { libc::write(fds[0], data.as_ptr() as *const libc::c_void, data.len()) };
+        assert_eq!(res, data.len().cast_signed());
     });
     let thread2 = thread::spawn(move || {
-        let data = "abc".as_bytes().as_ptr();
+        let data = "a".as_bytes();
         // 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
-        assert_eq!(res, 3);
+        let res = unsafe { libc::write(fds[0], data.as_ptr() as *const libc::c_void, data.len()) };
+        //~^ERROR: deadlock
+        assert_eq!(res, data.len().cast_signed());
     });
     let thread3 = thread::spawn(move || {
         // Unblock thread1 by freeing up some space.
-        let mut buf: [u8; 3] = [0; 3];
+        let mut buf: [u8; 1] = [0; 1];
         let res = unsafe { libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) };
-        assert_eq!(res, 3);
-        assert_eq!(buf, [1, 1, 1]);
+        assert_eq!(res, buf.len().cast_signed());
+        assert_eq!(buf, [1]);
     });
     thread1.join().unwrap();
     thread2.join().unwrap();