Mutable references

[yannbolliger]

For now, the frontend allows only local mutation and no mutable borrowing for safety reasons. It would however, provide great value to also allow mutable references. This should be possible by targetting the imperative phase of Stainless.

Example in Scala: https://github.com/jad-hamza/stainless/blob/72c0052255878c440e0a1d00260f4ebf04ba5860/frontends/benchmarks/imperative/valid/ReturnWithMutation.scala

[yannbolliger]

The current plan is to support mutable references &mut T by modelling them as mutable ADT:

case class Mut[T](var value: T)

In that way we can model the fact, that one can remotely overwrite the entire T i.e.

fn foo(x: &mut Bar) { 
  *x = Bar(...)
}

[yannbolliger]

Survey of possible problems with mutable references

• Clone erasure for mutable things could already be unsafe Check soundness of clone erasure #136

• All functions are annotated pure code. This would have to be to inferred. Could it pose verification problems?

  • Currently, only the laws in type_class fail if run without pure annotations on all functions. But the annotation can still be added manually, or it (in Rust!) it's simple to detect effects based on the presence of &mut in function signatures.
  • Test this with recursive functions

• Function params with mut T, & T, Box<T> and &mut T?
  In general: as soon as something is mut we have unique ownership, safe to assume no aliasing.

• What about higher-order functions in generics extraction? @gsps

• Mutable references modelled as Mut[T](var t: T) don't need to be redefined as LetVar in functions! (Take care in bindings). Example

• We currently rely on the fact, that we never return &mut T and insert a fresh copy at return.
  This is also true for final expressions/values of blocks/match arms/if-else. This will break with mutable references.
  See examples here and here.

• LetVar in blocks currently introduce a fresh copy.

  pub struct Thing<T> {
    field: T,
  }
  
  pub fn change_thing<T>(thing: Thing<T>, t: T) -> Thing<T> {
    let mut new_field = thing.field;
    new_field = t;
    Thing { field: new_field }
  }

  results in

   @pure
   def change_thing[T @mutable](thing: Thing[T @mutable], t: T @mutable): Thing[T @mutable] = {
     var (new_field: T @mutable) @var = freshCopy(thing.field)
     new_field = t
     freshCopy(Thing[T @mutable](new_field))
   }

  Benchmark here