Skip to content

Commit 2c8bd9b

Browse files
authored
Merge pull request #4561 from RalfJung/short-fd-ops
add flag to not shorten FD reads/writes; don't shorten pipe operations
2 parents 1421247 + 2839853 commit 2c8bd9b

File tree

8 files changed

+50
-19
lines changed

8 files changed

+50
-19
lines changed

src/tools/miri/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -323,6 +323,10 @@ environment variable. We first document the most relevant and most commonly used
323323
that do not have a guaranteed precision. The sign of the error is still non-deterministic.
324324
* `-Zmiri-no-extra-rounding-error` stops Miri from adding extra rounding errors to float operations
325325
that do not have a guaranteed precision.
326+
* `-Zmiri-no-short-fd-operations` stops Miri from artificially forcing `read`/`write` operations
327+
to only process a part of their buffer. Note that whenever Miri uses host operations to
328+
implement `read`/`write` (e.g. for file-backed file descriptors), the host system can still
329+
introduce short reads/writes.
326330
* `-Zmiri-num-cpus` states the number of available CPUs to be reported by miri. By default, the
327331
number of available CPUs is `1`. Note that this flag does not affect how miri handles threads in
328332
any way.

src/tools/miri/src/bin/miri.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -559,6 +559,8 @@ fn main() {
559559
miri_config.float_rounding_error = miri::FloatRoundingErrorMode::None;
560560
} else if arg == "-Zmiri-max-extra-rounding-error" {
561561
miri_config.float_rounding_error = miri::FloatRoundingErrorMode::Max;
562+
} else if arg == "-Zmiri-no-short-fd-operations" {
563+
miri_config.short_fd_operations = false;
562564
} else if arg == "-Zmiri-strict-provenance" {
563565
miri_config.provenance_mode = ProvenanceMode::Strict;
564566
} else if arg == "-Zmiri-permissive-provenance" {

src/tools/miri/src/eval.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,8 @@ pub struct MiriConfig {
113113
pub float_nondet: bool,
114114
/// Whether floating-point operations can have a non-deterministic rounding error.
115115
pub float_rounding_error: FloatRoundingErrorMode,
116+
/// Whether Miri artifically introduces short reads/writes on file descriptors.
117+
pub short_fd_operations: bool,
116118
}
117119

118120
impl Default for MiriConfig {
@@ -155,6 +157,7 @@ impl Default for MiriConfig {
155157
force_intrinsic_fallback: false,
156158
float_nondet: true,
157159
float_rounding_error: FloatRoundingErrorMode::Random,
160+
short_fd_operations: true,
158161
}
159162
}
160163
}

src/tools/miri/src/machine.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -669,6 +669,9 @@ pub struct MiriMachine<'tcx> {
669669
pub float_nondet: bool,
670670
/// Whether floating-point operations can have a non-deterministic rounding error.
671671
pub float_rounding_error: FloatRoundingErrorMode,
672+
673+
/// Whether Miri artifically introduces short reads/writes on file descriptors.
674+
pub short_fd_operations: bool,
672675
}
673676

674677
impl<'tcx> MiriMachine<'tcx> {
@@ -830,6 +833,7 @@ impl<'tcx> MiriMachine<'tcx> {
830833
force_intrinsic_fallback: config.force_intrinsic_fallback,
831834
float_nondet: config.float_nondet,
832835
float_rounding_error: config.float_rounding_error,
836+
short_fd_operations: config.short_fd_operations,
833837
}
834838
}
835839

@@ -1006,6 +1010,7 @@ impl VisitProvenance for MiriMachine<'_> {
10061010
force_intrinsic_fallback: _,
10071011
float_nondet: _,
10081012
float_rounding_error: _,
1013+
short_fd_operations: _,
10091014
} = self;
10101015

10111016
threads.visit_provenance(visit);

src/tools/miri/src/shims/files.rs

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -168,8 +168,9 @@ pub trait FileDescription: std::fmt::Debug + FileDescriptionExt {
168168
}
169169

170170
/// Determines whether this FD non-deterministically has its reads and writes shortened.
171-
fn nondet_short_accesses(&self) -> bool {
172-
true
171+
fn short_fd_operations(&self) -> bool {
172+
// We only enable this for FD kinds where we think short accesses gain useful test coverage.
173+
false
173174
}
174175

175176
/// Seeks to the given offset (which can be relative to the beginning, end, or current position).
@@ -395,6 +396,13 @@ impl FileDescription for FileHandle {
395396
communicate_allowed && self.file.is_terminal()
396397
}
397398

399+
fn short_fd_operations(&self) -> bool {
400+
// While short accesses on file-backed FDs are very rare (at least for sufficiently small
401+
// accesses), they can realistically happen when a signal interrupts the syscall.
402+
// FIXME: we should return `false` if this is a named pipe...
403+
true
404+
}
405+
398406
fn as_unix<'tcx>(&self, ecx: &MiriInterpCx<'tcx>) -> &dyn UnixFileDescription {
399407
assert!(
400408
ecx.target_os_is_unix(),

src/tools/miri/src/shims/unix/fd.rs

Lines changed: 18 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -274,12 +274,15 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
274274
}
275275
// Non-deterministically decide to further reduce the count, simulating a partial read (but
276276
// never to 0, that would indicate EOF).
277-
let count =
278-
if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() {
279-
count / 2 // since `count` is at least 2, the result is still at least 1
280-
} else {
281-
count
282-
};
277+
let count = if this.machine.short_fd_operations
278+
&& fd.short_fd_operations()
279+
&& count >= 2
280+
&& this.machine.rng.get_mut().random()
281+
{
282+
count / 2 // since `count` is at least 2, the result is still at least 1
283+
} else {
284+
count
285+
};
283286

284287
trace!("read: FD mapped to {fd:?}");
285288
// 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> {
360363
// Non-deterministically decide to further reduce the count, simulating a partial write.
361364
// We avoid reducing the write size to 0: the docs seem to be entirely fine with that,
362365
// but the standard library is not (https://github.com/rust-lang/rust/issues/145959).
363-
let count =
364-
if fd.nondet_short_accesses() && count >= 2 && this.machine.rng.get_mut().random() {
365-
count / 2
366-
} else {
367-
count
368-
};
366+
let count = if this.machine.short_fd_operations
367+
&& fd.short_fd_operations()
368+
&& count >= 2
369+
&& this.machine.rng.get_mut().random()
370+
{
371+
count / 2
372+
} else {
373+
count
374+
};
369375

370376
let finish = {
371377
let dest = dest.clone();

src/tools/miri/src/shims/unix/linux_like/eventfd.rs

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -37,11 +37,6 @@ impl FileDescription for EventFd {
3737
"event"
3838
}
3939

40-
fn nondet_short_accesses(&self) -> bool {
41-
// We always read and write exactly one `u64`.
42-
false
43-
}
44-
4540
fn close<'tcx>(
4641
self,
4742
_communicate_allowed: bool,

src/tools/miri/src/shims/unix/unnamed_socket.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,14 @@ impl FileDescription for AnonSocket {
123123
anonsocket_write(self, ptr, len, ecx, finish)
124124
}
125125

126+
fn short_fd_operations(&self) -> bool {
127+
// Pipes guarantee that sufficiently small accesses are not broken apart:
128+
// <https://pubs.opengroup.org/onlinepubs/9799919799/functions/write.html#tag_17_699_08>.
129+
// For now, we don't bother checking for the size, and just entirely disable
130+
// short accesses on pipes.
131+
matches!(self.fd_type, AnonSocketType::Socketpair)
132+
}
133+
126134
fn as_unix<'tcx>(&self, _ecx: &MiriInterpCx<'tcx>) -> &dyn UnixFileDescription {
127135
self
128136
}

0 commit comments

Comments
 (0)