Add strong mode for tree borrows

Author: HKalbasi

src/bin/miri.rs

@@ -517,6 +517,14 @@ fn main() {
             miri_config.borrow_tracker =
                 Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
                     precise_interior_mut: true,
+                    start_mut_ref_on_fn_entry_as_active: false,
+                }));
+            miri_config.provenance_mode = ProvenanceMode::Strict;
+        } else if arg == "-Zmiri-tree-borrows-strong" {
+            miri_config.borrow_tracker =
+                Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
+                    precise_interior_mut: true,
+                    start_mut_ref_on_fn_entry_as_active: true,
                 }));
             miri_config.provenance_mode = ProvenanceMode::Strict;
         } else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {

src/borrow_tracker/mod.rs

@@ -233,6 +233,7 @@ pub enum BorrowTrackerMethod {
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub struct TreeBorrowsParams {
     pub precise_interior_mut: bool,
+    pub start_mut_ref_on_fn_entry_as_active: bool,
 }
 
 impl BorrowTrackerMethod {

src/borrow_tracker/tree_borrows/mod.rs

@@ -146,6 +146,16 @@ impl<'tcx> NewPermission {
         let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.typing_env());
         let is_protected = retag_kind == RetagKind::FnEntry;
 
+        let start_mut_ref_on_fn_entry_as_active = cx
+            .machine
+            .borrow_tracker
+            .as_ref()
+            .unwrap()
+            .borrow()
+            .borrow_tracker_method
+            .get_tree_borrows_params()
+            .start_mut_ref_on_fn_entry_as_active;
+
         if matches!(ref_mutability, Some(Mutability::Mut) | None if !ty_is_unpin) {
             // Mutable reference / Box to pinning type: retagging is a NOP.
             // FIXME: with `UnsafePinned`, this should do proper per-byte tracking.
@@ -155,6 +165,9 @@ impl<'tcx> NewPermission {
         let freeze_perm = match ref_mutability {
             // Shared references are frozen.
             Some(Mutability::Not) => Permission::new_frozen(),
+            // Mutable references on fn entry are activated based on config
+            Some(Mutability::Mut) if start_mut_ref_on_fn_entry_as_active && is_protected =>
+                Permission::new_active(),
             // Mutable references and Boxes are reserved.
             _ => Permission::new_reserved_frz(),
         };

src/borrow_tracker/tree_borrows/perms.rs

@@ -90,7 +90,7 @@ impl PartialOrd for PermissionPriv {
 impl PermissionPriv {
     /// Check if `self` can be the initial state of a pointer.
     fn is_initial(&self) -> bool {
-        matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell)
+        matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell | Active)
     }
 
     /// Reject `ReservedIM` that cannot exist in the presence of a protector.

tests/fail/both_borrows/spurious_write_may_be_added.rs

@@ -0,0 +1,15 @@
+//@revisions: stack tree
+//@[tree]compile-flags: -Zmiri-tree-borrows-strong
+
+fn may_insert_spurious_write(_x: &mut u32) {}
+
+fn main() {
+    let target = &mut 42;
+    let target_alias = &*target;
+    let target_alias_ptr = target_alias as *const _;
+    may_insert_spurious_write(target);
+    // now `target_alias` is invalid
+    let _val = unsafe { *target_alias_ptr };
+    //~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
+    //~[tree]| ERROR: /read access through .* is forbidden/
+}

tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr

@@ -0,0 +1,25 @@
+error: Undefined Behavior: attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let _val = unsafe { *target_alias_ptr };
+   |                         ^^^^^^^^^^^^^^^^^ this error occurs as part of an access at ALLOC[0x0..0x4]
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
+   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
+help: <TAG> was created by a SharedReadOnly retag at offsets [0x0..0x4]
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let target_alias_ptr = target_alias as *const _;
+   |                            ^^^^^^^^^^^^
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a Unique function-entry retag inside this call
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     may_insert_spurious_write(target);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = note: BACKTRACE (of the first span):
+   = note: inside `main` at tests/fail/both_borrows/spurious_write_may_be_added.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
+

tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr

@@ -0,0 +1,27 @@
+error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let _val = unsafe { *target_alias_ptr };
+   |                         ^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
+   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information
+   = help: the accessed tag <TAG> has state Disabled which forbids this child read access
+help: the accessed tag <TAG> was created here, in the initial state Frozen
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let target_alias = &*target;
+   |                        ^^^^^^^^
+help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL | fn may_insert_spurious_write(_x: &mut u32) {}
+   |                                              ^
+   = help: this transition corresponds to a loss of read permissions
+   = note: BACKTRACE (of the first span):
+   = note: inside `main` at tests/fail/both_borrows/spurious_write_may_be_added.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
+