@@ -303,14 +303,28 @@ impl<'tcx> Stack {
303303 /// is met: We cannot push `Uniq` onto frozen stacks.
304304 /// `kind` indicates which kind of reference is being created.
305305 fn create ( & mut self , bor : Borrow , kind : RefKind ) {
306- if self . frozen_since . is_some ( ) {
307- // A frozen location? Possible if we create a barrier, then push again.
308- assert ! ( bor. is_shared( ) , "We should never try creating a unique borrow for a frozen stack" ) ;
309- trace ! ( "create: Not doing anything on frozen location" ) ;
306+ // When creating a frozen reference, freeze. This ensures F1.
307+ // We also do *not* push anything else to the stack, making sure that no nother kind
308+ // of access (like writing through raw pointers) is permitted.
309+ if kind == RefKind :: Frozen {
310+ let bor_t = match bor {
311+ Borrow :: Shr ( Some ( t) ) => t,
312+ _ => bug ! ( "Creating illegal borrow {:?} for frozen ref" , bor) ,
313+ } ;
314+ // It is possible that we already are frozen (e.g. if we just pushed a barrier,
315+ // the redundancy check would not have kicked in).
316+ match self . frozen_since {
317+ Some ( loc_t) => assert ! ( loc_t <= bor_t, "Trying to freeze location for longer than it was already frozen" ) ,
318+ None => {
319+ trace ! ( "create: Freezing" ) ;
320+ self . frozen_since = Some ( bor_t) ;
321+ }
322+ }
310323 return ;
311324 }
312- // First, push. We do this even if we will later freeze, because we
313- // will allow mutation of shared data at the expense of unfreezing.
325+ assert ! ( self . frozen_since. is_none( ) , "Trying to create non-frozen reference to frozen location" ) ;
326+
327+ // Push new item to the stack.
314328 let itm = match bor {
315329 Borrow :: Uniq ( t) => BorStackItem :: Uniq ( t) ,
316330 Borrow :: Shr ( _) => BorStackItem :: Shr ,
@@ -325,15 +339,6 @@ impl<'tcx> Stack {
325339 trace ! ( "create: Pushing {:?}" , itm) ;
326340 self . borrows . push ( itm) ;
327341 }
328- // Then, maybe freeze. This is part 2 of ensuring F1.
329- if kind == RefKind :: Frozen {
330- let bor_t = match bor {
331- Borrow :: Shr ( Some ( t) ) => t,
332- _ => bug ! ( "Creating illegal borrow {:?} for frozen ref" , bor) ,
333- } ;
334- trace ! ( "create: Freezing" ) ;
335- self . frozen_since = Some ( bor_t) ;
336- }
337342 }
338343
339344 /// Add a barrier
0 commit comments