comments

renamed `y_initial_state` to `y_current_perm` because
it is confusing for the "..._initial_state" to be the only LocationState
in the entire test that is not `_.is_initial()`.

src/borrow_tracker/tree_borrows/tree/tests.rs

@@ -124,8 +124,8 @@ mod spurious_read {
     }
 
     /// Relative position of `x` and `y`.
-    /// `y` cannot be a child of `x` because the compiler won't blindly
-    /// insert spurious reads through `x` if it has children.
+    /// `y` cannot be a child of `x` because `x` gets retagged as the first
+    /// thing in the pattern, so it cannot have children.
     #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
     enum RelPosXY {
         MutuallyForeign,
@@ -242,6 +242,7 @@ mod spurious_read {
         Access(TestAccess),
         RetX(RetX),
         RetY(RetY),
+        /// The inner `LocStateProt` must be an initial state (as per the `is_initial` function)
         RetagY(LocStateProt),
     }
 
@@ -325,7 +326,8 @@ mod spurious_read {
     }
 
     #[derive(Clone, PartialEq, Eq, Hash)]
-    /// The states of two pointers to the same location.
+    /// The states of two pointers to the same location,
+    /// and their relationship to each other in the tree.
     ///
     /// Note that the two states interact: using one pointer can have
     /// an impact on the other.
@@ -348,11 +350,16 @@ mod spurious_read {
             Ok(Self { x, y, ..self })
         }
 
+        /// Perform a read on the given pointer if its state is `initialized`.
+        /// Must be called just after reborrowing a pointer.
         fn read_if_initialized(self, ptr: PtrSelector) -> Result<Self, ()> {
             let initialized = match ptr {
                 PtrSelector::X => self.x.state.initialized,
                 PtrSelector::Y => self.y.state.initialized,
-                PtrSelector::Other => true,
+                PtrSelector::Other =>
+                    panic!(
+                        "the `initialized` status of `PtrSelector::Other` is unknown, do not pass it to `read_if_initialized`"
+                    ),
             };
             if initialized {
                 self.perform_test_access(&TestAccess { ptr, kind: AccessKind::Read })
@@ -372,6 +379,8 @@ mod spurious_read {
         }
 
         fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
+            assert!(new_y.is_initial());
+            // `xy_rel` changes to "mutually foreign" now: `y` can no longer be a parent of `x`.
             Self { y: new_y, xy_rel: RelPosXY::MutuallyForeign, ..self }
                 .read_if_initialized(PtrSelector::Y)
         }
@@ -404,7 +413,7 @@ mod spurious_read {
         }
     }
 
-    /// Arbitrary sequence of accesses, as experienced by two mutually foreign pointers
+    /// Arbitrary sequence of events, as experienced by two mutually foreign pointers
     /// to the same location.
     #[derive(Clone)]
     struct OpaqueCode<RetX, RetY> {
@@ -520,15 +529,20 @@ mod spurious_read {
 
     #[derive(Clone, Debug)]
     struct Pattern {
-        /// The relative position of `x` and `y` at the beginning of the pattern.
-        /// Might change if the opaque code contains any `retag y`.
+        /// The relative position of `x` and `y` at the beginning of the arbitrary
+        /// code (i.e., just after `x` got created).
+        /// Might change during the execution if said arbitrary code contains any `retag y`.
         xy_rel: RelPosXY,
-        /// Permission that `x` will be retagged as (always protected until
-        /// a possible `ret x` in the second phase).
+        /// Permission that `x` will be created as
+        /// (always protected until a possible `ret x` in the second phase).
+        /// This one should be initial (as per `is_initial`).
         x_retag_perm: LocationState,
         /// Permission that `y` has at the beginning of the pattern.
-        /// Might by reset if the opaque code contains any `retag y`.
-        y_initial_state: LocationState,
+        /// Can be any state, not necessarily initial
+        /// (since `y` exists already before the pattern starts).
+        /// This state might be reset during the execution if the opaque code
+        /// contains any `retag y`, but only to an initial state this time.
+        y_current_perm: LocationState,
         /// Whether `y` starts with a protector.
         /// Might change if the opaque code contains any `ret y`.
         y_protected: bool,
@@ -538,15 +552,14 @@ mod spurious_read {
         fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
             let mut v = Vec::new();
             for xy_rel in RelPosXY::exhaustive() {
-                for (x_retag_perm, y_initial_state) in
-                    <(LocationState, LocationState)>::exhaustive()
+                for (x_retag_perm, y_current_perm) in <(LocationState, LocationState)>::exhaustive()
                 {
                     // We can only do spurious reads for initialized locations anyway.
                     precondition!(x_retag_perm.initialized);
-                    // And we don't allow `x` to start as `Disabled` because it's protected.
-                    precondition!(!x_retag_perm.permission.is_disabled());
+                    // And `x` just retagged must be initial.
+                    precondition!(x_retag_perm.permission.is_initial());
                     for y_protected in bool::exhaustive() {
-                        v.push(Pattern { xy_rel, x_retag_perm, y_initial_state, y_protected });
+                        v.push(Pattern { xy_rel, x_retag_perm, y_current_perm, y_protected });
                     }
                 }
             }
@@ -572,7 +585,7 @@ mod spurious_read {
         /// This does not yet include a possible read-on-reborrow through `x`.
         fn retag_permissions(&self) -> (LocStateProt, LocStateProt) {
             let x = LocStateProt { state: self.x_retag_perm, prot: true };
-            let y = LocStateProt { state: self.y_initial_state, prot: self.y_protected };
+            let y = LocStateProt { state: self.y_current_perm, prot: self.y_protected };
             (x, y)
         }
 
@@ -598,7 +611,7 @@ mod spurious_read {
                 // Failed to retag `x` in the source (e.g. `y` was protected Active)
                 continue;
             };
-            // `x` must stay protected, but the function of `y` might return here
+            // `x` must stay protected, but the function protecting `y` might return here
             for (final_source, opaque) in
                 initial_source.all_states_reachable_via_opaque_code::</*X*/ NoRet, /*Y*/ AllowRet>()
             {