Open yannbolliger opened 3 years ago
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(...)
}
Survey of possible problems with mutable references
[x] Clone erasure for mutable things could already be unsafe #136
[ ] All functions are annotated pure
code. This would have to be to inferred. Could it pose verification problems?
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.[ ] 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
[x] Mutable references modelled as Mut[T](var t: T)
don't need to be redefined as LetVar in functions! (Take care in bindings
). Example
[x] 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.
[x] 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))
}
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