AntiAliasing limitation of consumed/owned mut params

[yannbolliger]

Stainless doesn't distinguish between owned objects and referenced/shared/borrowed objects, because on the JVM every object is a reference. Therefore, AntiAliasing in Stainless hinders the Rust frontend to pass such code:

#[var(field)]
struct S { field: i32 }

fn set_field(mut s: S) -> S {
  s.field = 789;
  s
} 

Which corresponds to the following in Scala (and is transformed to it by the Rust frontend's extraction). Internally, the mut s: S is translated to a LetVar at the beginning of the function:

sealed case class S((field: Int) @var)

def set_field(var0: S): S = {
  var (s: S) @var = var0
  s.field = 789
  s
}

But this is not allowed in Stainless, because Stainless can't see that the parameter var0 is consumed/owned and can be modified at will. Neither does it see that var0 is not used after the LetVar assignment. Finally, Stainless fails with Illegal Aliasing: var0.

[jad-hamza]

val s = var0 works for this one, but I don't know if that's good enough for your use case?

[yannbolliger]

Take-away from the discussion with @jad-hamza:

• We need something that is basically like snapshot. It tells Stainless that we operate on a new copy/version of the ADT that no one else has access to. This is the same as the idea of the @owned flag, @romac suggested.
• This primitive should be added as a tree in Stainless.
• Functions that use the primitive on all their mutable parameters can be @pure because they only operate on the new copy of the params.
• In the best case, this can even make it possible to set all ADT fields to @var.