From 283985393a98761e656c86c5f6f153e9f90eb7e2 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 3 Sep 2025 10:27:20 +0200 Subject: [PATCH] add flag to not shorten FD reads/writes; don't shorten pipe operations --- src/tools/miri/README.md | 4 +++ src/tools/miri/src/bin/miri.rs | 2 ++ src/tools/miri/src/eval.rs | 3 ++ src/tools/miri/src/machine.rs | 5 ++++ src/tools/miri/src/shims/files.rs | 12 ++++++-- src/tools/miri/src/shims/unix/fd.rs | 30 +++++++++++-------- .../miri/src/shims/unix/linux_like/eventfd.rs | 5 ---- .../miri/src/shims/unix/unnamed_socket.rs | 8 +++++ 8 files changed, 50 insertions(+), 19 deletions(-) diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index cb4a56b58ac8..517aa343a6d4 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -323,6 +323,10 @@ environment variable. We first document the most relevant and most commonly used that do not have a guaranteed precision. The sign of the error is still non-deterministic. * `-Zmiri-no-extra-rounding-error` stops Miri from adding extra rounding errors to float operations that do not have a guaranteed precision. +* `-Zmiri-no-short-fd-operations` stops Miri from artificially forcing `read`/`write` operations + to only process a part of their buffer. Note that whenever Miri uses host operations to + implement `read`/`write` (e.g. for file-backed file descriptors), the host system can still + introduce short reads/writes. * `-Zmiri-num-cpus` states the number of available CPUs to be reported by miri. By default, the number of available CPUs is `1`. Note that this flag does not affect how miri handles threads in any way. diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs index 8fd8d332978d..9b0bee72aeff 100644 --- a/src/tools/miri/src/bin/miri.rs +++ b/src/tools/miri/src/bin/miri.rs @@ -559,6 +559,8 @@ fn main() { miri_config.float_rounding_error = miri::FloatRoundingErrorMode::None; } else if arg == "-Zmiri-max-extra-rounding-error" { miri_config.float_rounding_error = miri::FloatRoundingErrorMode::Max; + } else if arg == "-Zmiri-no-short-fd-operations" { + miri_config.short_fd_operations = false; } else if arg == "-Zmiri-strict-provenance" { miri_config.provenance_mode = ProvenanceMode::Strict; } else if arg == "-Zmiri-permissive-provenance" { diff --git a/src/tools/miri/src/eval.rs b/src/tools/miri/src/eval.rs index f174a448a810..caed98f04f32 100644 --- a/src/tools/miri/src/eval.rs +++ b/src/tools/miri/src/eval.rs @@ -113,6 +113,8 @@ pub struct MiriConfig { pub float_nondet: bool, /// Whether floating-point operations can have a non-deterministic rounding error. pub float_rounding_error: FloatRoundingErrorMode, + /// Whether Miri artifically introduces short reads/writes on file descriptors. + pub short_fd_operations: bool, } impl Default for MiriConfig { @@ -155,6 +157,7 @@ impl Default for MiriConfig { force_intrinsic_fallback: false, float_nondet: true, float_rounding_error: FloatRoundingErrorMode::Random, + short_fd_operations: true, } } } diff --git a/src/tools/miri/src/machine.rs b/src/tools/miri/src/machine.rs index 7802a58f1123..9067c5d33cb6 100644 --- a/src/tools/miri/src/machine.rs +++ b/src/tools/miri/src/machine.rs @@ -669,6 +669,9 @@ pub struct MiriMachine<'tcx> { pub float_nondet: bool, /// Whether floating-point operations can have a non-deterministic rounding error. pub float_rounding_error: FloatRoundingErrorMode, + + /// Whether Miri artifically introduces short reads/writes on file descriptors. + pub short_fd_operations: bool, } impl<'tcx> MiriMachine<'tcx> { @@ -830,6 +833,7 @@ impl<'tcx> MiriMachine<'tcx> { force_intrinsic_fallback: config.force_intrinsic_fallback, float_nondet: config.float_nondet, float_rounding_error: config.float_rounding_error, + short_fd_operations: config.short_fd_operations, } } @@ -1006,6 +1010,7 @@ impl VisitProvenance for MiriMachine<'_> { force_intrinsic_fallback: _, float_nondet: _, float_rounding_error: _, + short_fd_operations: _, } = self; threads.visit_provenance(visit); diff --git a/src/tools/miri/src/shims/files.rs b/src/tools/miri/src/shims/files.rs index 0d4642c6ad0e..8c29cb040b55 100644 --- a/src/tools/miri/src/shims/files.rs +++ b/src/tools/miri/src/shims/files.rs @@ -168,8 +168,9 @@ pub trait FileDescription: std::fmt::Debug + FileDescriptionExt { } /// Determines whether this FD non-deterministically has its reads and writes shortened. - fn nondet_short_accesses(&self) -> bool { - true + fn short_fd_operations(&self) -> bool { + // We only enable this for FD kinds where we think short accesses gain useful test coverage. + false } /// Seeks to the given offset (which can be relative to the beginning, end, or current position). @@ -395,6 +396,13 @@ impl FileDescription for FileHandle { communicate_allowed && self.file.is_terminal() } + fn short_fd_operations(&self) -> bool { + // While short accesses on file-backed FDs are very rare (at least for sufficiently small + // accesses), they can realistically happen when a signal interrupts the syscall. + // FIXME: we should return `false` if this is a named pipe... + true + } + fn as_unix<'tcx>(&self, ecx: &MiriInterpCx<'tcx>) -> &dyn UnixFileDescription { assert!( ecx.target_os_is_unix(), diff --git a/src/tools/miri/src/shims/unix/fd.rs b/src/tools/miri/src/shims/unix/fd.rs index 9fbecffc55d9..95e26ef5d5d8 100644 --- a/src/tools/miri/src/shims/unix/fd.rs +++ b/src/tools/miri/src/shims/unix/fd.rs @@ -274,12 +274,15 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { } // Non-deterministically decide to further reduce the count, simulating a partial read (but // never to 0, that would indicate EOF). - let count = - if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() { - count / 2 // since `count` is at least 2, the result is still at least 1 - } else { - count - }; + let count = if this.machine.short_fd_operations + && fd.short_fd_operations() + && count >= 2 + && this.machine.rng.get_mut().random() + { + count / 2 // since `count` is at least 2, the result is still at least 1 + } else { + count + }; trace!("read: FD mapped to {fd:?}"); // We want to read at most `count` bytes. We are sure that `count` is not negative @@ -360,12 +363,15 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { // Non-deterministically decide to further reduce the count, simulating a partial write. // We avoid reducing the write size to 0: the docs seem to be entirely fine with that, // but the standard library is not (https://github.com/rust-lang/rust/issues/145959). - let count = - if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() { - count / 2 - } else { - count - }; + let count = if this.machine.short_fd_operations + && fd.short_fd_operations() + && count >= 2 + && this.machine.rng.get_mut().random() + { + count / 2 + } else { + count + }; let finish = { let dest = dest.clone(); diff --git a/src/tools/miri/src/shims/unix/linux_like/eventfd.rs b/src/tools/miri/src/shims/unix/linux_like/eventfd.rs index 2d35ef064db8..ee7deb8d3830 100644 --- a/src/tools/miri/src/shims/unix/linux_like/eventfd.rs +++ b/src/tools/miri/src/shims/unix/linux_like/eventfd.rs @@ -37,11 +37,6 @@ 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, diff --git a/src/tools/miri/src/shims/unix/unnamed_socket.rs b/src/tools/miri/src/shims/unix/unnamed_socket.rs index 817ddd7954df..7eb82851033d 100644 --- a/src/tools/miri/src/shims/unix/unnamed_socket.rs +++ b/src/tools/miri/src/shims/unix/unnamed_socket.rs @@ -123,6 +123,14 @@ impl FileDescription for AnonSocket { anonsocket_write(self, ptr, len, ecx, finish) } + fn short_fd_operations(&self) -> bool { + // Pipes guarantee that sufficiently small accesses are not broken apart: + // . + // For now, we don't bother checking for the size, and just entirely disable + // short accesses on pipes. + matches!(self.fd_type, AnonSocketType::Socketpair) + } + fn as_unix<'tcx>(&self, _ecx: &MiriInterpCx<'tcx>) -> &dyn UnixFileDescription { self }