Skip to content

non-deterministically truncate reads/writes #4481

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jul 21, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 15 additions & 1 deletion src/shims/files.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::any::Any;
use std::collections::BTreeMap;
use std::fs::{File, Metadata};
use std::io::{IsTerminal, Seek, SeekFrom, Write};
use std::io::{ErrorKind, IsTerminal, Seek, SeekFrom, Write};
use std::marker::CoercePointee;
use std::ops::Deref;
use std::rc::{Rc, Weak};
Expand Down Expand Up @@ -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>(
Expand Down Expand Up @@ -334,6 +339,15 @@ impl FileDescription for FileHandle {
) -> InterpResult<'tcx> {
assert!(communicate_allowed, "isolation should have prevented even opening a file");

if !self.writable {
// Linux hosts return EBADF here which we can't translate via the platform-independent
// code since it does not map to any `io::ErrorKind` -- so if we don't do anything
// special, we'd throw an "unsupported error code" here. Windows returns something that
// gets translated to `PermissionDenied`. That seems like a good value so let's just use
// this everywhere, even if it means behavior on Unix targets does not match the real
// thing.
return finish.call(ecx, Err(ErrorKind::PermissionDenied.into()));
}
let result = ecx.write_to_host(&self.file, len, ptr)?;
finish.call(ecx, result)
}
Expand Down
21 changes: 20 additions & 1 deletion src/shims/unix/fd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 = {
Expand Down Expand Up @@ -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!(
Expand Down
5 changes: 5 additions & 0 deletions src/shims/unix/linux_like/eventfd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
22 changes: 13 additions & 9 deletions src/shims/windows/fs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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
Expand Down
7 changes: 5 additions & 2 deletions tests/fail-dep/libc/libc-epoll-data-race.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 };
Expand Down Expand Up @@ -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();
Expand Down
8 changes: 6 additions & 2 deletions tests/fail-dep/libc/libc-read-and-uninit-premature-eof.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,9 @@ use std::mem::MaybeUninit;
#[path = "../../utils/mod.rs"]
mod utils;

#[path = "../../utils/libc.rs"]
mod libc_utils;

fn main() {
let path =
utils::prepare_with_content("fail-libc-read-and-uninit-premature-eof.txt", &[1u8, 2, 3]);
Expand All @@ -18,8 +21,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 as much as we can from a 3-byte file.
let res = libc_utils::read_all(fd, buf.as_mut_ptr().cast::<std::ffi::c_void>(), 4);
assert!(res == 3);
buf.assume_init(); //~ERROR: encountered uninitialized memory, but expected an integer
assert_eq!(libc::close(fd), 0);
}
Expand Down
3 changes: 2 additions & 1 deletion tests/fail-dep/libc/libc_epoll_block_two_thread.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
25 changes: 14 additions & 11 deletions tests/fail-dep/libc/socketpair_block_read_twice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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();
Expand Down
4 changes: 2 additions & 2 deletions tests/fail-dep/libc/socketpair_block_read_twice.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
29 changes: 17 additions & 12 deletions tests/fail-dep/libc/socketpair_block_write_twice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
4 changes: 2 additions & 2 deletions tests/fail-dep/libc/socketpair_block_write_twice.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ error: the evaluated program deadlocked
error: the evaluated program deadlocked
--> tests/fail-dep/libc/socketpair_block_write_twice.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 = unsafe { libc::write(fds[0], data.as_ptr() as *const libc::c_void, data.len()) };
| ^ 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
Expand Down
7 changes: 5 additions & 2 deletions tests/pass-dep/libc/libc-epoll-blocking.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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.
Expand Down
Loading
Loading