lifetime checking: errors not detected

[mppf]

This issue collects interesting lifetime checking cases that the current effort does not detect.

array-resize-with-ref

proc testInvalidRefAfterArrayResize() {
  var D = {1..100};
  var A:[D] int;
  ref myRef = A[1];
  D = {1..1000}; // assigning to D resizes A, invalidating references!
  myRef = 20;
  writeln(A[1]);
}
testInvalidRefAfterArrayResize();

assign-owned

class MyClass { var x:int; }
proc testInvalidBorrowAfterAssignOwned() {
  var own = new owned MyClass(1);
  {
    var instance = own.borrow();
    var otherOwned = new owned MyClass(2);
    own = otherOwned; // deletes MyClass(1)
    writeln(instance); // use-after-free
  }
}
testInvalidBorrowAfterAssignOwned();

clear-owned

class MyClass { var x:int; }
proc testInvalidBorrowAfterClearOwned() {
  var own = new owned MyClass(1);
  {
    var instance = own.borrow();
    own.clear(); // deletes MyClass
    writeln(instance); // use-after-free
  }
}
testInvalidBorrowAfterClearOwned();

reset-owned

class MyClass { var x:int; }
proc testInvalidBorrowAfterResetOwned() {
  var own = new owned MyClass(1);
  {
    var instance = own.borrow();
    var otherInstance = new unmanaged MyClass(2);
    own.retain(otherInstance); // deletes MyClass
    writeln(instance); // use-after-free
  }
}
testInvalidBorrowAfterResetOwned();

assign-owned-array

class MyClass { var x:int; }
proc testInvalidBorrowAfterAssignOwnedInArray() {
  var A:[1..10] owned MyClass;
  A[1] = new owned MyClass(1);
  {
    var instance = A[1].borrow();
    var otherOwned = new owned MyClass(2);
    A[1] = otherOwned; // deletes MyClass(1)
    writeln(instance); // use-after-free
  }
}
testInvalidBorrowAfterAssignOwnedInArray();

Going further

It might be possible to detect these cases by assuming that any function accepting an Owned(T) by reference has the ability to clear it; and therefore any borrows from it will be invalid if they span a call to such a function.

How would such an analysis handle records or arrays containing Owned? One strategy would be to apply the same rule to these. But, that might be so conservative that an example such as the following would be excluded, even though it doesn't contain a use-after-free:

proc test() {
  const n = 100;
  var A:[1..n] Owned(MyClass);
  ... initialize A ...
  var borrow =  A[1].borrow();
  for i in 2..n {
    A[i] = add(borrow, A[i]); // here, A[i] returns a mutable ref, and so
                                            // the called array accessor function takes in A by ref
                                            // and so the conservative analysis would assume it can
                                            // invalidate `borrow`. 
  }
}
test();

Here is a ref-focused variant of the same program:

proc test() {
  const n = 100;
  var A:[1..n] int;
  ... initialize A ...
  ref eltRef =  A[1];
  for i in 2..n {
    A[i] = add(eltRef, A[i]); // here, A[i] returns a mutable ref, and so
                                            // the called array accessor function takes in A by ref
                                            // and so the conservative analysis would assume it can
                                            // invalidate `eltRef`.
  }
}
test();

It seems that doing an acceptable job with these might require compiler analysis to say which functions actually have the capability to invalidate a borrow (based upon their bodies). But even that would rule out something like this, unless complex techniques like symbolic execution or iteration space analysis are applied:

proc test() {
  const n = 100;
  var A:[1..n] Owned(MyClass);
  ... initialize A ...
  var pivotElement:int = f(A);
  var borrow =  A[pivotElement].borrow();
  for i in 1..n {
    if i != pivotElement {
      // Inside this conditional, we know that setting A[i] is not going to
      // invalidate `borrow`, but will the compiler know that?
      A[i] = add(eltRef, A[i]);
    }
  }
}
test();

Besides these issues, race conditional can be involved in use-after-free errors, and it's hard to see how to detect such issues at compile-time without pretty drastic measures (such as Rust's only-one-mutable-ref rule).

[bradcray]

I've just filed a few other cases that might be considered part of this issue's list:

11021: lifetime checking and initializing fields with 'new borrowed'

11022: lifetime checking and loop expressions

[mppf]

I added another related issue:

lifetime checker issues with combination of owned and borrowed #11666

[mppf]

I just learned that Swift has a rule for exclusive write access but only within a thread. https://github.com/apple/swift-evolution/blob/master/proposals/0176-enforce-exclusive-access-to-memory.md https://docs.swift.org/swift-book/LanguageGuide/MemorySafety.html

I wonder if some of these same ideas could apply. I'm just not sure if it could be practical.