Skip to content

Commit 1eab3a0

Browse files
committed
Auto merge of #3786 - RalfJung:rustup, r=RalfJung
Rustup
2 parents 3f09710 + d7e9d90 commit 1eab3a0

File tree

9 files changed

+62
-30
lines changed

9 files changed

+62
-30
lines changed

README.md

+2
Original file line numberDiff line numberDiff line change
@@ -398,6 +398,8 @@ to Miri failing to detect cases of undefined behavior in a program.
398398
application instead of raising an error within the context of Miri (and halting
399399
execution). Note that code might not expect these operations to ever panic, so
400400
this flag can lead to strange (mis)behavior.
401+
* `-Zmiri-recursive-validation` is a *highly experimental* flag that makes validity checking
402+
recurse below references.
401403
* `-Zmiri-retag-fields[=<all|none|scalar>]` controls when Stacked Borrows retagging recurses into
402404
fields. `all` means it always recurses (the default, and equivalent to `-Zmiri-retag-fields`
403405
without an explicit value), `none` means it never recurses, `scalar` means it only recurses for

rust-version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1df0458781d6fd753a68c4cdc4de5313b1635dbd
1+
29e924841f06bb181d87494eba2783761bc1ddec

src/bin/miri.rs

+5-2
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ use std::str::FromStr;
3030

3131
use tracing::debug;
3232

33-
use miri::{BacktraceStyle, BorrowTrackerMethod, ProvenanceMode, RetagFields};
3433
use rustc_data_structures::sync::Lrc;
3534
use rustc_driver::Compilation;
3635
use rustc_hir::def_id::LOCAL_CRATE;
@@ -53,6 +52,8 @@ use rustc_session::{CtfeBacktrace, EarlyDiagCtxt};
5352
use rustc_span::def_id::DefId;
5453
use rustc_target::spec::abi::Abi;
5554

55+
use miri::{BacktraceStyle, BorrowTrackerMethod, ProvenanceMode, RetagFields, ValidationMode};
56+
5657
struct MiriCompilerCalls {
5758
miri_config: miri::MiriConfig,
5859
}
@@ -474,7 +475,9 @@ fn main() {
474475
} else if arg == "--" {
475476
after_dashdash = true;
476477
} else if arg == "-Zmiri-disable-validation" {
477-
miri_config.validate = false;
478+
miri_config.validation = ValidationMode::No;
479+
} else if arg == "-Zmiri-recursive-validation" {
480+
miri_config.validation = ValidationMode::Deep;
478481
} else if arg == "-Zmiri-disable-stacked-borrows" {
479482
miri_config.borrow_tracker = None;
480483
} else if arg == "-Zmiri-tree-borrows" {

src/eval.rs

+13-3
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ pub enum IsolatedOp {
6868
Allow,
6969
}
7070

71-
#[derive(Copy, Clone, PartialEq, Eq)]
71+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
7272
pub enum BacktraceStyle {
7373
/// Prints a terser backtrace which ideally only contains relevant information.
7474
Short,
@@ -78,14 +78,24 @@ pub enum BacktraceStyle {
7878
Off,
7979
}
8080

81+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
82+
pub enum ValidationMode {
83+
/// Do not perform any kind of validation.
84+
No,
85+
/// Validate the interior of the value, but not things behind references.
86+
Shallow,
87+
/// Fully recursively validate references.
88+
Deep,
89+
}
90+
8191
/// Configuration needed to spawn a Miri instance.
8292
#[derive(Clone)]
8393
pub struct MiriConfig {
8494
/// The host environment snapshot to use as basis for what is provided to the interpreted program.
8595
/// (This is still subject to isolation as well as `forwarded_env_vars`.)
8696
pub env: Vec<(OsString, OsString)>,
8797
/// Determine if validity checking is enabled.
88-
pub validate: bool,
98+
pub validation: ValidationMode,
8999
/// Determines if Stacked Borrows or Tree Borrows is enabled.
90100
pub borrow_tracker: Option<BorrowTrackerMethod>,
91101
/// Whether `core::ptr::Unique` receives special treatment.
@@ -162,7 +172,7 @@ impl Default for MiriConfig {
162172
fn default() -> MiriConfig {
163173
MiriConfig {
164174
env: vec![],
165-
validate: true,
175+
validation: ValidationMode::Shallow,
166176
borrow_tracker: Some(BorrowTrackerMethod::StackedBorrows),
167177
unique_is_unique: false,
168178
check_alignment: AlignmentCheck::Int,

src/intrinsics/mod.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
153153
// Would not be considered UB, or the other way around (`is_val_statically_known(0)`).
154154
"is_val_statically_known" => {
155155
let [arg] = check_arg_count(args)?;
156-
this.validate_operand(arg)?;
156+
this.validate_operand(arg, /*recursive*/ false)?;
157157
let branch: bool = this.machine.rng.get_mut().gen();
158158
this.write_scalar(Scalar::from_bool(branch), dest)?;
159159
}

src/lib.rs

+1
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,7 @@ pub use crate::diagnostics::{
142142
};
143143
pub use crate::eval::{
144144
create_ecx, eval_entry, AlignmentCheck, BacktraceStyle, IsolatedOp, MiriConfig, RejectOpWith,
145+
ValidationMode,
145146
};
146147
pub use crate::helpers::{AccessKind, EvalContextExt as _};
147148
pub use crate::machine::{

src/machine.rs

+16-23
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,11 @@ impl fmt::Display for MiriMemoryKind {
187187
pub type MemoryKind = interpret::MemoryKind<MiriMemoryKind>;
188188

189189
/// Pointer provenance.
190-
#[derive(Clone, Copy)]
190+
// This needs to be `Eq`+`Hash` because the `Machine` trait needs that because validity checking
191+
// *might* be recursive and then it has to track which places have already been visited.
192+
// These implementations are a bit questionable, and it means we may check the same place multiple
193+
// times with different provenance, but that is in general not wrong.
194+
#[derive(Clone, Copy, PartialEq, Eq, Hash)]
191195
pub enum Provenance {
192196
/// For pointers with concrete provenance. we exactly know which allocation they are attached to
193197
/// and what their borrow tag is.
@@ -215,24 +219,6 @@ pub enum Provenance {
215219
Wildcard,
216220
}
217221

218-
// This needs to be `Eq`+`Hash` because the `Machine` trait needs that because validity checking
219-
// *might* be recursive and then it has to track which places have already been visited.
220-
// However, comparing provenance is meaningless, since `Wildcard` might be any provenance -- and of
221-
// course we don't actually do recursive checking.
222-
// We could change `RefTracking` to strip provenance for its `seen` set but that type is generic so that is quite annoying.
223-
// Instead owe add the required instances but make them panic.
224-
impl PartialEq for Provenance {
225-
fn eq(&self, _other: &Self) -> bool {
226-
panic!("Provenance must not be compared")
227-
}
228-
}
229-
impl Eq for Provenance {}
230-
impl std::hash::Hash for Provenance {
231-
fn hash<H: std::hash::Hasher>(&self, _state: &mut H) {
232-
panic!("Provenance must not be hashed")
233-
}
234-
}
235-
236222
/// The "extra" information a pointer has over a regular AllocId.
237223
#[derive(Copy, Clone, PartialEq)]
238224
pub enum ProvenanceExtra {
@@ -460,7 +446,7 @@ pub struct MiriMachine<'tcx> {
460446
pub(crate) isolated_op: IsolatedOp,
461447

462448
/// Whether to enforce the validity invariant.
463-
pub(crate) validate: bool,
449+
pub(crate) validation: ValidationMode,
464450

465451
/// The table of file descriptors.
466452
pub(crate) fds: shims::FdTable,
@@ -659,7 +645,7 @@ impl<'tcx> MiriMachine<'tcx> {
659645
cmd_line: None,
660646
tls: TlsData::default(),
661647
isolated_op: config.isolated_op,
662-
validate: config.validate,
648+
validation: config.validation,
663649
fds: shims::FdTable::init(config.mute_stdout_stderr),
664650
dirs: Default::default(),
665651
layouts,
@@ -801,7 +787,7 @@ impl VisitProvenance for MiriMachine<'_> {
801787
fds,
802788
tcx: _,
803789
isolated_op: _,
804-
validate: _,
790+
validation: _,
805791
clock: _,
806792
layouts: _,
807793
static_roots: _,
@@ -943,7 +929,14 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
943929

944930
#[inline(always)]
945931
fn enforce_validity(ecx: &MiriInterpCx<'tcx>, _layout: TyAndLayout<'tcx>) -> bool {
946-
ecx.machine.validate
932+
ecx.machine.validation != ValidationMode::No
933+
}
934+
#[inline(always)]
935+
fn enforce_validity_recursively(
936+
ecx: &InterpCx<'tcx, Self>,
937+
_layout: TyAndLayout<'tcx>,
938+
) -> bool {
939+
ecx.machine.validation == ValidationMode::Deep
947940
}
948941

949942
#[inline(always)]
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
//@compile-flags: -Zmiri-recursive-validation
2+
3+
fn main() {
4+
let x = 3u8;
5+
let xref = &x;
6+
let xref_wrong_type: &bool = unsafe { std::mem::transmute(xref) }; //~ERROR: encountered 0x03, but expected a boolean
7+
let _val = *xref_wrong_type;
8+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
error: Undefined Behavior: constructing invalid value at .<deref>: encountered 0x03, but expected a boolean
2+
--> $DIR/recursive-validity-ref-bool.rs:LL:CC
3+
|
4+
LL | let xref_wrong_type: &bool = unsafe { std::mem::transmute(xref) };
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at .<deref>: encountered 0x03, but expected a boolean
6+
|
7+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
8+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
9+
= note: BACKTRACE:
10+
= note: inside `main` at $DIR/recursive-validity-ref-bool.rs:LL:CC
11+
12+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
13+
14+
error: aborting due to 1 previous error
15+

0 commit comments

Comments
 (0)