Add a flag to check the validity of a Stack

Author: saethlin

src/bin/miri.rs

@@ -397,6 +397,9 @@ fn main() {
                     );
                     miri_config.tag_raw = true;
                 }
+                "-Zmiri-verify-stack-consistency" => {
+                    miri_config.verify_stack_cache = true;
+                }
                 "--" => {
                     after_dashdash = true;
                 }

src/eval.rs

@@ -119,6 +119,9 @@ pub struct MiriConfig {
     /// Whether to ignore any output by the program. This is helpful when debugging miri
     /// as its messages don't get intermingled with the program messages.
     pub mute_stdout_stderr: bool,
+    /// Whether we should check the internal validity requirements of the Stack data structure
+    /// itself (in addition to checking the program being executed).
+    pub verify_stack_cache: bool,
 }
 
 impl Default for MiriConfig {
@@ -146,6 +149,7 @@ impl Default for MiriConfig {
             backtrace_style: BacktraceStyle::Short,
             strict_provenance: false,
             mute_stdout_stderr: false,
+            verify_stack_cache: false,
         }
     }
 }

src/machine.rs

@@ -295,6 +295,9 @@ pub struct Evaluator<'mir, 'tcx> {
 
     /// Corresponds to -Zmiri-mute-stdout-stderr and doesn't write the output but acts as if it succeeded.
     pub(crate) mute_stdout_stderr: bool,
+
+    /// Controls whether the borrow stack checks the integrity of its internal caches.
+    pub(crate) verify_stack_cache: bool,
 }
 
 impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
@@ -349,6 +352,7 @@ impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
             check_alignment: config.check_alignment,
             cmpxchg_weak_failure_rate: config.cmpxchg_weak_failure_rate,
             mute_stdout_stderr: config.mute_stdout_stderr,
+            verify_stack_cache: config.verify_stack_cache,
         }
     }
 
@@ -585,6 +589,7 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
                 stacked_borrows,
                 kind,
                 ecx.machine.current_span(),
+                ecx.machine.verify_stack_cache,
             ))
         } else {
             None

src/stacked_borrows.rs

@@ -503,9 +503,9 @@ impl<'tcx> Stack {
 /// Map per-stack operations to higher-level per-location-range operations.
 impl<'tcx> Stacks {
     /// Creates new stack with initial tag.
-    fn new(size: Size, perm: Permission, tag: SbTag) -> Self {
+    fn new(size: Size, perm: Permission, tag: SbTag, verify: bool) -> Self {
         let item = Item { perm, tag, protector: None };
-        let stack = Stack::new(item);
+        let stack = Stack::new(item, verify);
         Stacks {
             stacks: RefCell::new(RangeMap::new(size, stack)),
             history: RefCell::new(AllocHistory::new()),
@@ -549,6 +549,7 @@ impl Stacks {
         state: &GlobalState,
         kind: MemoryKind<MiriMemoryKind>,
         mut current_span: CurrentSpan<'_, '_, '_>,
+        verify: bool,
     ) -> Self {
         let mut extra = state.borrow_mut();
         let (base_tag, perm) = match kind {
@@ -582,7 +583,7 @@ impl Stacks {
                 (tag, Permission::SharedReadWrite)
             }
         };
-        let stacks = Stacks::new(size, perm, base_tag);
+        let stacks = Stacks::new(size, perm, base_tag, verify);
         stacks.history.borrow_mut().log_creation(
             None,
             base_tag,

src/stacked_borrows/stack.rs

@@ -17,7 +17,7 @@ pub struct Stack {
     /// On a read, we need to disable all `Unique` above the granting item. We can avoid most of
     /// this scan by keeping track of the region of the borrow stack that may contain `Unique`s.
     unique_range: Range<usize>,
-    validate_cache: bool,
+    verify_cache: bool,
 }
 
 #[derive(Clone, Debug)]
@@ -49,7 +49,7 @@ impl Stack {
     /// - The StackCache indices don't refer to the parallel tags,
     /// - If top_untagged is Some it is the topmost Untagged
     /// - There are no Unique tags outside of first_unique..last_unique
-    fn check_cache_validity(&self) {
+    fn verify_cache_consistency(&self) {
         for (tag, stack_idx) in self.cache.tags.iter().zip(self.cache.idx.iter()) {
             assert_eq!(self.borrows[*stack_idx].tag, *tag);
         }
@@ -72,8 +72,8 @@ impl Stack {
     /// Find the item granting the given kind of access to the given tag, and return where
     /// it is on the stack.
     pub fn find_granting(&mut self, access: AccessKind, tag: SbTag) -> Option<usize> {
-        if self.validate_cache {
-            self.check_cache_validity();
+        if self.verify_cache {
+            self.verify_cache_consistency();
         }
 
         match tag {
@@ -111,8 +111,8 @@ impl Stack {
     }
 
     pub fn insert(&mut self, new_idx: usize, new: Item) {
-        if self.validate_cache {
-            self.check_cache_validity();
+        if self.verify_cache {
+            self.verify_cache_consistency();
         }
 
         self.borrows.insert(new_idx, new);
@@ -152,13 +152,13 @@ impl Stack {
         }
     }
 
-    pub fn new(item: Item) -> Self {
+    pub fn new(item: Item, verify: bool) -> Self {
         Stack {
             borrows: vec![item],
             cache: StackCache { idx: [0; CACHE_LEN], tags: [item.tag; CACHE_LEN] },
             unique_range: if item.perm == Permission::Unique { 0..1 } else { 0..0 },
             top_untagged: None,
-            validate_cache: false,
+            verify_cache: verify,
         }
     }
 
@@ -175,8 +175,8 @@ impl Stack {
         granting_idx: usize,
         mut visitor: V,
     ) -> crate::InterpResult<'static> {
-        if self.validate_cache {
-            self.check_cache_validity();
+        if self.verify_cache {
+            self.verify_cache_consistency();
         }
 
         if granting_idx < self.unique_range.end {
@@ -205,8 +205,8 @@ impl Stack {
     }
 
     pub fn drain_rev(&mut self, range: std::ops::Range<usize>) -> DrainRev<'_> {
-        if self.validate_cache {
-            self.check_cache_validity();
+        if self.verify_cache {
+            self.verify_cache_consistency();
         }
 
         DrainRev { start: range.start, stack: self, cursor: range.end - 1 }