Miri: add a flag to do recursive validity checking

README.md

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

src/bin/miri.rs

@@ -44,7 +44,7 @@ use rustc_session::config::{CrateType, ErrorOutputType, OptLevel};
 use rustc_session::search_paths::PathKind;
 use rustc_session::{CtfeBacktrace, EarlyDiagCtxt};
 
-use miri::{BacktraceStyle, BorrowTrackerMethod, ProvenanceMode, RetagFields};
+use miri::{BacktraceStyle, BorrowTrackerMethod, ProvenanceMode, RetagFields, ValidationMode};
 
 struct MiriCompilerCalls {
     miri_config: miri::MiriConfig,
@@ -421,7 +421,9 @@ fn main() {
         } else if arg == "--" {
             after_dashdash = true;
         } else if arg == "-Zmiri-disable-validation" {
-            miri_config.validate = false;
+            miri_config.validation = ValidationMode::No;
+        } else if arg == "-Zmiri-recursive-validation" {
+            miri_config.validation = ValidationMode::Deep;
         } else if arg == "-Zmiri-disable-stacked-borrows" {
             miri_config.borrow_tracker = None;
         } else if arg == "-Zmiri-tree-borrows" {

src/eval.rs

@@ -68,7 +68,7 @@ pub enum IsolatedOp {
     Allow,
 }
 
-#[derive(Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum BacktraceStyle {
     /// Prints a terser backtrace which ideally only contains relevant information.
     Short,
@@ -78,14 +78,24 @@ pub enum BacktraceStyle {
     Off,
 }
 
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum ValidationMode {
+    /// Do not perform any kind of validation.
+    No,
+    /// Validate the interior of the value, but not things behind references.
+    Shallow,
+    /// Fully recursively validate references.
+    Deep,
+}
+
 /// Configuration needed to spawn a Miri instance.
 #[derive(Clone)]
 pub struct MiriConfig {
     /// The host environment snapshot to use as basis for what is provided to the interpreted program.
     /// (This is still subject to isolation as well as `forwarded_env_vars`.)
     pub env: Vec<(OsString, OsString)>,
     /// Determine if validity checking is enabled.
-    pub validate: bool,
+    pub validation: ValidationMode,
     /// Determines if Stacked Borrows or Tree Borrows is enabled.
     pub borrow_tracker: Option<BorrowTrackerMethod>,
     /// Whether `core::ptr::Unique` receives special treatment.
@@ -162,7 +172,7 @@ impl Default for MiriConfig {
     fn default() -> MiriConfig {
         MiriConfig {
             env: vec![],
-            validate: true,
+            validation: ValidationMode::Shallow,
             borrow_tracker: Some(BorrowTrackerMethod::StackedBorrows),
             unique_is_unique: false,
             check_alignment: AlignmentCheck::Int,

src/intrinsics/mod.rs

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

src/lib.rs

@@ -142,6 +142,7 @@ pub use crate::diagnostics::{
 };
 pub use crate::eval::{
     create_ecx, eval_entry, AlignmentCheck, BacktraceStyle, IsolatedOp, MiriConfig, RejectOpWith,
+    ValidationMode,
 };
 pub use crate::helpers::{AccessKind, EvalContextExt as _};
 pub use crate::machine::{

src/machine.rs

@@ -187,7 +187,11 @@ impl fmt::Display for MiriMemoryKind {
 pub type MemoryKind = interpret::MemoryKind<MiriMemoryKind>;
 
 /// Pointer provenance.
-#[derive(Clone, Copy)]
+// This needs to be `Eq`+`Hash` because the `Machine` trait needs that because validity checking
+// *might* be recursive and then it has to track which places have already been visited.
+// These implementations are a bit questionable, and it means we may check the same place multiple
+// times with different provenance, but that is in general not wrong.
+#[derive(Clone, Copy, PartialEq, Eq, Hash)]
 pub enum Provenance {
     /// For pointers with concrete provenance. we exactly know which allocation they are attached to
     /// and what their borrow tag is.
@@ -215,24 +219,6 @@ pub enum Provenance {
     Wildcard,
 }
 
-// This needs to be `Eq`+`Hash` because the `Machine` trait needs that because validity checking
-// *might* be recursive and then it has to track which places have already been visited.
-// However, comparing provenance is meaningless, since `Wildcard` might be any provenance -- and of
-// course we don't actually do recursive checking.
-// We could change `RefTracking` to strip provenance for its `seen` set but that type is generic so that is quite annoying.
-// Instead owe add the required instances but make them panic.
-impl PartialEq for Provenance {
-    fn eq(&self, _other: &Self) -> bool {
-        panic!("Provenance must not be compared")
-    }
-}
-impl Eq for Provenance {}
-impl std::hash::Hash for Provenance {
-    fn hash<H: std::hash::Hasher>(&self, _state: &mut H) {
-        panic!("Provenance must not be hashed")
-    }
-}
-
 /// The "extra" information a pointer has over a regular AllocId.
 #[derive(Copy, Clone, PartialEq)]
 pub enum ProvenanceExtra {
@@ -460,7 +446,7 @@ pub struct MiriMachine<'tcx> {
     pub(crate) isolated_op: IsolatedOp,
 
     /// Whether to enforce the validity invariant.
-    pub(crate) validate: bool,
+    pub(crate) validation: ValidationMode,
 
     /// The table of file descriptors.
     pub(crate) fds: shims::FdTable,
@@ -659,7 +645,7 @@ impl<'tcx> MiriMachine<'tcx> {
             cmd_line: None,
             tls: TlsData::default(),
             isolated_op: config.isolated_op,
-            validate: config.validate,
+            validation: config.validation,
             fds: shims::FdTable::init(config.mute_stdout_stderr),
             dirs: Default::default(),
             layouts,
@@ -801,7 +787,7 @@ impl VisitProvenance for MiriMachine<'_> {
             fds,
             tcx: _,
             isolated_op: _,
-            validate: _,
+            validation: _,
             clock: _,
             layouts: _,
             static_roots: _,
@@ -943,7 +929,11 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
 
     #[inline(always)]
     fn enforce_validity(ecx: &MiriInterpCx<'tcx>, _layout: TyAndLayout<'tcx>) -> bool {
-        ecx.machine.validate
+        ecx.machine.validation != ValidationMode::No
+    }
+    #[inline(always)]
+    fn enforce_validity_recursively(ecx: &InterpCx<'tcx, Self>, _layout: TyAndLayout<'tcx>) -> bool {
+        ecx.machine.validation == ValidationMode::Deep
     }
 
     #[inline(always)]

tests/fail/validity/recursive-validity-ref-bool.rs

@@ -0,0 +1,8 @@
+//@compile-flags: -Zmiri-recursive-validation
+
+fn main() {
+    let x = 3u8;
+    let xref = &x;
+    let xref_wrong_type: &bool = unsafe { std::mem::transmute(xref) }; //~ERROR: encountered 0x03, but expected a boolean
+    let _val = *xref_wrong_type;
+}

tests/fail/validity/recursive-validity-ref-bool.stderr

@@ -0,0 +1,15 @@
+error: Undefined Behavior: constructing invalid value at .<deref>: encountered 0x03, but expected a boolean
+  --> $DIR/recursive-validity-ref-bool.rs:LL:CC
+   |
+LL |     let xref_wrong_type: &bool = unsafe { std::mem::transmute(xref) };
+   |                                           ^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at .<deref>: encountered 0x03, but expected a boolean
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE:
+   = note: inside `main` at $DIR/recursive-validity-ref-bool.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to 1 previous error
+