fix checking Mut access on frozen location

[web.git] / ralf / _posts / 2018-08-07-stacked-borrows.md

diff --git a/ralf/_posts/2018-08-07-stacked-borrows.md b/ralf/_posts/2018-08-07-stacked-borrows.md
index bf9f9a6d8fa726bf76343513a7072ade521c9e6b..37cdf504668b6fbb2ce48d9819c586125a2a34de 100644 (file)
--- a/ralf/_posts/2018-08-07-stacked-borrows.md
+++ b/ralf/_posts/2018-08-07-stacked-borrows.md
@@ -147,7 +147,7 @@ Shared references with interior mutability do not really have any restrictions i
 For every location in memory, we keep track of a stack of borrows (`Uniq(_)` or `Raw`), and potentially "top off" this stack by freezing the location.
 A frozen location is never written to, and no `Uniq` is pushed.
 
 For every location in memory, we keep track of a stack of borrows (`Uniq(_)` or `Raw`), and potentially "top off" this stack by freezing the location.
 A frozen location is never written to, and no `Uniq` is pushed.
 

-Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `mem::size_of::<T>` many bytes).
+Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `size_of_val` many bytes).

 Whenever a shared reference is created, if there is no interior mutability, we freeze the locations if they are not already frozen.
 If there is interior mutability, we just push a `Raw`.
 Whenever a raw pointer is created from a mutable reference, we push a `Raw`.
 Whenever a shared reference is created, if there is no interior mutability, we freeze the locations if they are not already frozen.
 If there is interior mutability, we just push a `Raw`.
 Whenever a raw pointer is created from a mutable reference, we push a `Raw`.


@@ -239,7 +239,7 @@ It is also needed to explain why we can put the [`noalias` parameter attribute](
 
 Consider the following code:
 {% highlight rust %}
 
 Consider the following code:
 {% highlight rust %}

-fn demo5(x: &mut i32, y: usize) -> i32 {
+fn demo5(x: &mut i32, y: usize) {

   *x = 42;
   foo(y);
 }
   *x = 42;
   foo(y);
 }


@@ -336,8 +336,11 @@ impl MemoryByte {
         self.frz_since.map_or(false, |loc_t| loc_t <= acc_t),
       Mut(acc_m) =>
         // Raw pointers are fine with frozen locations. This is important because &Cell is raw!
         self.frz_since.map_or(false, |loc_t| loc_t <= acc_t),
       Mut(acc_m) =>
         // Raw pointers are fine with frozen locations. This is important because &Cell is raw!

-        (acc_m.is_raw() && self.frozen_since.is_some()) ||
-        self.borrows.last().map_or(false, |loc_itm| loc_itm == Mut(acc_m)),
+        if self.frozen_since.is_some() {
+          acc_m.is_raw()
+        } else {
+          self.borrows.last().map_or(false, |loc_itm| loc_itm == Mut(acc_m))
+        }

     }
   }
 
     }
   }