Merge pull request #4561 from RalfJung/short-fd-ops
add flag to not shorten FD reads/writes; don't shorten pipe operations
This commit is contained in:
commit
2c8bd9bc26
8 changed files with 50 additions and 19 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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" {
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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(),
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue