Merge pull request #4561 from RalfJung/short-fd-ops

add flag to not shorten FD reads/writes; don't shorten pipe operations

8 files changed, 50 insertions, 19 deletions

diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md
index cb4a56b58ac..517aa343a6d 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 8fd8d332978..9b0bee72aef 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 f174a448a81..caed98f04f3 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 e0ee9541948..e4540fb9bc5 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 0d4642c6ad0..8c29cb040b5 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 9fbecffc55d..95e26ef5d5d 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 2d35ef064db..ee7deb8d383 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 817ddd7954d..7eb82851033 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:
+        // <https://pubs.opengroup.org/onlinepubs/9799919799/functions/write.html#tag_17_699_08>.
+        // 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
     }