Skip to content

Commit 80c3ba8

Browse files
authored
Merge pull request rust-lang#4555 from RalfJung/float-err
add a flag to always apply the maximum float error
2 parents 8236def + d4f861e commit 80c3ba8

File tree

8 files changed

+116
-72
lines changed

8 files changed

+116
-72
lines changed

src/tools/miri/README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -319,6 +319,8 @@ environment variable. We first document the most relevant and most commonly used
319319
Can be used without a value; in that case the range defaults to `0..64`.
320320
* `-Zmiri-many-seeds-keep-going` tells Miri to really try all the seeds in the given range, even if
321321
a failing seed has already been found. This is useful to determine which fraction of seeds fails.
322+
* `-Zmiri-max-extra-rounding-error` tells Miri to always apply the maximum error to float operations
323+
that do not have a guaranteed precision. The sign of the error is still non-deterministic.
322324
* `-Zmiri-no-extra-rounding-error` stops Miri from adding extra rounding errors to float operations
323325
that do not have a guaranteed precision.
324326
* `-Zmiri-num-cpus` states the number of available CPUs to be reported by miri. By default, the

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -556,7 +556,9 @@ fn main() {
556556
} else if arg == "-Zmiri-deterministic-floats" {
557557
miri_config.float_nondet = false;
558558
} else if arg == "-Zmiri-no-extra-rounding-error" {
559-
miri_config.float_rounding_error = false;
559+
miri_config.float_rounding_error = miri::FloatRoundingErrorMode::None;
560+
} else if arg == "-Zmiri-max-extra-rounding-error" {
561+
miri_config.float_rounding_error = miri::FloatRoundingErrorMode::Max;
560562
} else if arg == "-Zmiri-strict-provenance" {
561563
miri_config.provenance_mode = ProvenanceMode::Strict;
562564
} else if arg == "-Zmiri-permissive-provenance" {

src/tools/miri/src/eval.rs

Lines changed: 2 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -32,65 +32,6 @@ pub enum MiriEntryFnType {
3232
/// will hang the program.
3333
const MAIN_THREAD_YIELDS_AT_SHUTDOWN: u32 = 256;
3434

35-
#[derive(Copy, Clone, Debug, PartialEq)]
36-
pub enum AlignmentCheck {
37-
/// Do not check alignment.
38-
None,
39-
/// Check alignment "symbolically", i.e., using only the requested alignment for an allocation and not its real base address.
40-
Symbolic,
41-
/// Check alignment on the actual physical integer address.
42-
Int,
43-
}
44-
45-
#[derive(Copy, Clone, Debug, PartialEq)]
46-
pub enum RejectOpWith {
47-
/// Isolated op is rejected with an abort of the machine.
48-
Abort,
49-
50-
/// If not Abort, miri returns an error for an isolated op.
51-
/// Following options determine if user should be warned about such error.
52-
/// Do not print warning about rejected isolated op.
53-
NoWarning,
54-
55-
/// Print a warning about rejected isolated op, with backtrace.
56-
Warning,
57-
58-
/// Print a warning about rejected isolated op, without backtrace.
59-
WarningWithoutBacktrace,
60-
}
61-
62-
#[derive(Copy, Clone, Debug, PartialEq)]
63-
pub enum IsolatedOp {
64-
/// Reject an op requiring communication with the host. By
65-
/// default, miri rejects the op with an abort. If not, it returns
66-
/// an error code, and prints a warning about it. Warning levels
67-
/// are controlled by `RejectOpWith` enum.
68-
Reject(RejectOpWith),
69-
70-
/// Execute op requiring communication with the host, i.e. disable isolation.
71-
Allow,
72-
}
73-
74-
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
75-
pub enum BacktraceStyle {
76-
/// Prints a terser backtrace which ideally only contains relevant information.
77-
Short,
78-
/// Prints a backtrace with all possible information.
79-
Full,
80-
/// Prints only the frame that the error occurs in.
81-
Off,
82-
}
83-
84-
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
85-
pub enum ValidationMode {
86-
/// Do not perform any kind of validation.
87-
No,
88-
/// Validate the interior of the value, but not things behind references.
89-
Shallow,
90-
/// Fully recursively validate references.
91-
Deep,
92-
}
93-
9435
/// Configuration needed to spawn a Miri instance.
9536
#[derive(Clone)]
9637
pub struct MiriConfig {
@@ -171,7 +112,7 @@ pub struct MiriConfig {
171112
/// Whether floating-point operations can behave non-deterministically.
172113
pub float_nondet: bool,
173114
/// Whether floating-point operations can have a non-deterministic rounding error.
174-
pub float_rounding_error: bool,
115+
pub float_rounding_error: FloatRoundingErrorMode,
175116
}
176117

177118
impl Default for MiriConfig {
@@ -213,7 +154,7 @@ impl Default for MiriConfig {
213154
fixed_scheduling: false,
214155
force_intrinsic_fallback: false,
215156
float_nondet: true,
216-
float_rounding_error: true,
157+
float_rounding_error: FloatRoundingErrorMode::Random,
217158
}
218159
}
219160
}

src/tools/miri/src/lib.rs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -138,15 +138,14 @@ pub use crate::data_structures::mono_hash_map::MonoHashMap;
138138
pub use crate::diagnostics::{
139139
EvalContextExt as _, NonHaltingDiagnostic, TerminationInfo, report_error,
140140
};
141-
pub use crate::eval::{
142-
AlignmentCheck, BacktraceStyle, IsolatedOp, MiriConfig, MiriEntryFnType, RejectOpWith,
143-
ValidationMode, create_ecx, eval_entry,
144-
};
141+
pub use crate::eval::{MiriConfig, MiriEntryFnType, create_ecx, eval_entry};
145142
pub use crate::helpers::{AccessKind, EvalContextExt as _, ToU64 as _, ToUsize as _};
146143
pub use crate::intrinsics::EvalContextExt as _;
147144
pub use crate::machine::{
148-
AllocExtra, DynMachineCallback, FrameExtra, MachineCallback, MemoryKind, MiriInterpCx,
149-
MiriInterpCxExt, MiriMachine, MiriMemoryKind, PrimitiveLayouts, Provenance, ProvenanceExtra,
145+
AlignmentCheck, AllocExtra, BacktraceStyle, DynMachineCallback, FloatRoundingErrorMode,
146+
FrameExtra, IsolatedOp, MachineCallback, MemoryKind, MiriInterpCx, MiriInterpCxExt,
147+
MiriMachine, MiriMemoryKind, PrimitiveLayouts, Provenance, ProvenanceExtra, RejectOpWith,
148+
ValidationMode,
150149
};
151150
pub use crate::operator::EvalContextExt as _;
152151
pub use crate::provenance_gc::{EvalContextExt as _, LiveAllocs, VisitProvenance, VisitWith};

src/tools/miri/src/machine.rs

Lines changed: 70 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,75 @@ pub const SIGRTMAX: i32 = 42;
4949
/// base address for each evaluation would produce unbounded memory usage.
5050
const ADDRS_PER_ANON_GLOBAL: usize = 32;
5151

52+
#[derive(Copy, Clone, Debug, PartialEq)]
53+
pub enum AlignmentCheck {
54+
/// Do not check alignment.
55+
None,
56+
/// Check alignment "symbolically", i.e., using only the requested alignment for an allocation and not its real base address.
57+
Symbolic,
58+
/// Check alignment on the actual physical integer address.
59+
Int,
60+
}
61+
62+
#[derive(Copy, Clone, Debug, PartialEq)]
63+
pub enum RejectOpWith {
64+
/// Isolated op is rejected with an abort of the machine.
65+
Abort,
66+
67+
/// If not Abort, miri returns an error for an isolated op.
68+
/// Following options determine if user should be warned about such error.
69+
/// Do not print warning about rejected isolated op.
70+
NoWarning,
71+
72+
/// Print a warning about rejected isolated op, with backtrace.
73+
Warning,
74+
75+
/// Print a warning about rejected isolated op, without backtrace.
76+
WarningWithoutBacktrace,
77+
}
78+
79+
#[derive(Copy, Clone, Debug, PartialEq)]
80+
pub enum IsolatedOp {
81+
/// Reject an op requiring communication with the host. By
82+
/// default, miri rejects the op with an abort. If not, it returns
83+
/// an error code, and prints a warning about it. Warning levels
84+
/// are controlled by `RejectOpWith` enum.
85+
Reject(RejectOpWith),
86+
87+
/// Execute op requiring communication with the host, i.e. disable isolation.
88+
Allow,
89+
}
90+
91+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
92+
pub enum BacktraceStyle {
93+
/// Prints a terser backtrace which ideally only contains relevant information.
94+
Short,
95+
/// Prints a backtrace with all possible information.
96+
Full,
97+
/// Prints only the frame that the error occurs in.
98+
Off,
99+
}
100+
101+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
102+
pub enum ValidationMode {
103+
/// Do not perform any kind of validation.
104+
No,
105+
/// Validate the interior of the value, but not things behind references.
106+
Shallow,
107+
/// Fully recursively validate references.
108+
Deep,
109+
}
110+
111+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
112+
pub enum FloatRoundingErrorMode {
113+
/// Apply a random error (the default).
114+
Random,
115+
/// Don't apply any error.
116+
None,
117+
/// Always apply the maximum error (with a random sign).
118+
Max,
119+
}
120+
52121
/// Extra data stored with each stack frame
53122
pub struct FrameExtra<'tcx> {
54123
/// Extra data for the Borrow Tracker.
@@ -599,7 +668,7 @@ pub struct MiriMachine<'tcx> {
599668
/// Whether floating-point operations can behave non-deterministically.
600669
pub float_nondet: bool,
601670
/// Whether floating-point operations can have a non-deterministic rounding error.
602-
pub float_rounding_error: bool,
671+
pub float_rounding_error: FloatRoundingErrorMode,
603672
}
604673

605674
impl<'tcx> MiriMachine<'tcx> {

src/tools/miri/src/math.rs

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,9 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
1515
val: F,
1616
err_scale: i32,
1717
) -> F {
18-
if !ecx.machine.float_nondet || !ecx.machine.float_rounding_error {
18+
if !ecx.machine.float_nondet
19+
|| matches!(ecx.machine.float_rounding_error, FloatRoundingErrorMode::None)
20+
{
1921
return val;
2022
}
2123

@@ -24,7 +26,12 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
2426
// (When read as binary, the position of the first `1` determines the exponent,
2527
// and the remaining bits fill the mantissa. `PREC` is one plus the size of the mantissa,
2628
// so this all works out.)
27-
let r = F::from_u128(rng.random_range(0..(1 << F::PRECISION))).value;
29+
let r = F::from_u128(match ecx.machine.float_rounding_error {
30+
FloatRoundingErrorMode::Random => rng.random_range(0..(1 << F::PRECISION)),
31+
FloatRoundingErrorMode::Max => (1 << F::PRECISION) - 1, // force max error
32+
FloatRoundingErrorMode::None => unreachable!(),
33+
})
34+
.value;
2835
// Multiply this with 2^(scale - PREC). The result is between 0 and
2936
// 2^PREC * 2^(scale - PREC) = 2^scale.
3037
let err = r.scalbn(err_scale.strict_sub(F::PRECISION.try_into().unwrap()));

src/tools/miri/tests/pass/concurrency/sync.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ use std::time::{Duration, Instant};
99

1010
// We are expecting to sleep for 10ms. How long of a sleep we are accepting?
1111
// Even with 1000ms we still see this test fail on macOS runners.
12-
const MAX_SLEEP_TIME_MS: u64 = 2000;
12+
// On a aarch64-pc-windows-msvc runner, we saw 2.7s!
13+
const MAX_SLEEP_TIME_MS: u64 = 4000;
1314

1415
// Check if Rust barriers are working.
1516

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
//! Check that the flags to control the extra rounding error work.
2+
//@revisions: random max none
3+
//@[max]compile-flags: -Zmiri-max-extra-rounding-error
4+
//@[none]compile-flags: -Zmiri-no-extra-rounding-error
5+
#![feature(cfg_select)]
6+
7+
use std::collections::HashSet;
8+
use std::hint::black_box;
9+
10+
fn main() {
11+
let expected = cfg_select! {
12+
random => 13, // FIXME: why is it 13?
13+
max => 2,
14+
none => 1,
15+
};
16+
// Call `sin(0.5)` a bunch of times and see how many different values we get.
17+
let mut values = HashSet::new();
18+
for _ in 0..(expected * 16) {
19+
let val = black_box(0.5f64).sin();
20+
values.insert(val.to_bits());
21+
}
22+
assert_eq!(values.len(), expected);
23+
}

0 commit comments

Comments
 (0)