Mutable references: mut cells everywhere

[yannbolliger]

Proposal for supporting mutable references. Closes #140

Original solution
The envisioned solution was to wrap mutably borrowed references in a case class MutRef[@mutable T](t: T) when the borrow happens. At the end of the loan's lifetime, we would reassign the changes made on the MutRef object's field back to the original object. A little example:

pub fn main() {
  let mut x = 1;
  let y = &mut x; // borrow happens
  *y = 2;
  assert!(x == 2) // original used again, hence loan over
}

Would have been translated to the following in Scala:

object Mutable {
  final case class MutRef[@mutable T](var t: T)
  def main() = {
    var x = 1
    val y = MutRef(x) // borrow as a wrap in MutRef
    y.t = 2
    x = y.t // propagate changes back to the original
    assert(x == 2)
  }
}

In the above example, the reassignment of changes to the original x is necessary because of Scala semantics. In other cases where the original is an object, Scala semantics would be correct for our use-case but Stainless is not able to track the aliasing that is created by the wrap into MutRef. The following examples shows a weird case of this:

pub struct Thing<T> { field: T }

pub fn change_thing<T>(thing: &mut Thing<T>, t: T) {
  *thing = Thing { field: t };
}

pub fn main() {
  let mut thing = Thing { field: 123 };
  change_thing(&mut thing, 456);
  assert!(thing.field == 456);

  let thing2 = &mut thing;
  change_thing(thing2, 789);
  assert!(thing.field == 789);

  let thing3 = &mut thing;
  *thing3 = Thing { field: 0 };
  assert!(thing.field == 0);
}

This is translated to the following in Scala (only the main is shown):

  def main() = {
    val thing = Thing(123)
    change_thing(MutRef(thing), 456) // MutRef is not bound, last binding is 'thing'
    assert(thing.field == 456)

    val thing2 = MutRef(thing)  // MutRef is bound to 'thing2'
    change_thing(thing2, 789)
    thing = thing2.t
    assert(thing.field == 789)

    val thing3 = MutRef(thing)  // MutRef is bound to 'thing3'
    thing3.t = Thing(0)
    thing = thing3.t
    assert(thing.field == 0)
  }

Stainless correctly tracks aliasing in the first block, where the borrow happens in the argument of the function. This is probably due to the fact that the last binding of that value is still thing. Then, the changes are correctly applied back to thing in the AntiAliasing phase.

For the two later blocks, this is not the case. The newly created MutRef(thing) is bound to a name and Stainless correctly tracks changes to the MutRef objects thing2 and thing3. But it does not track the fact that they are still aliasing thing and therefore it doesn't propagate changes back to thing.

The example demonstrates, how the manual reassignment of changes to the original object at the end of the loan's lifetime is necessary to guarantee correctness. However, to implement this revealed itself to be very hard/impossible by only looking at the HIR (high-level intermediated representation in rustc) because the HIR does not know when the lifetime of a reference is over. Rustc performs borrow checking and lifetime resolution only later in the compilation and uses the MIR (mid-level IR), a sort of CFG that is much further apart from Stainless' AST, to do so.

Work-around

Thanks to @romac, I found a solution to that problem. Instead of propagating the changes back to the original, we can lift a variable that is later borrowed into a MutRef from the start. In that manner, borrowing simply becomes aliasing and Stainless can track the changes to the field of the object all the way through.

object Mutable {
  final case class MutRef[@mutable T](var t: T)
  def main() = {
    var x = MutRef(1)
    val y = x // borrowing simply becomes aliasing
    y.t = 2
    assert(x.t == 2) // changes are already performed on the original object
  }
}

Thanks to the fact that y is a val, Stainless is able to track the aliasing that is introduced and hence correctly verifies the above example.

[yannbolliger]

Closing in favour of #164. Most of the changes here are contained there.