Unsoundness when using `swap` due to AntiAliasing not flagging

[samuelchassot]

Stainless verifies this program:

import stainless.lang._
import stainless.collection._
import stainless.annotation._

case class X(var x: BigInt)

object Unsound:
  def simplerUnsoundExample(): Unit = {
    val a = Array[X](X(0), X(0), X(0))
    val newV = X(1)
    swap(a, 0, Array(newV), 0)
    assert(a(0).x == 1)
    newV.x = 3
    assert(a(0).x == 1) // WRONG <--- should be 3
  }

  def simplerUnsoundExampleCell(): Unit = {
    val a = Cell[X](X(0))
    val newV = X(1)
    swap(a, Cell(newV))
    assert(a.v.x == 1)
    newV.x = 3
    assert(a.v.x == 1) // WRONG <--- should be 3
  }
end Unsound

but it is wrong.

AntiAliasing should reject it, or other VCs generated to verify it correctly.

[samuelchassot]

This function is rejected by AntiAliasing:

def antiAliasingRejected(): Unit = {
    val newV = X(1)
    val b = Cell(newV)
    assert(b.v.x == 1)
    newV.x = 3
    assert(b.v.x == 3)
  }

with this message:

[  Info  ] Detected file modifications
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing finished                                   
[  Info  ] Running phase AntiAliasing                               
[ Error  ] unsound/Unsound.scala:43:13: Illegal aliasing: Cell[X](newV)
[ Error  ] Hint: this error occurs due to:
[ Error  ]   -the type of b (Cell[X]) being mutable
[ Error  ]   -the definition of b not being fresh
[ Error  ]   -the definition of b containing variables of mutable types
[ Error  ]   that also appear after the declaration of b:
[ Error  ]     -newV (of type X)
[ Error  ] 
               val b = Cell(newV)

I argue the above examples should be rejected for the same reason.

[samuelchassot]

This version of the function with Cell swap is rejected. This one and the example above are essentially identical and should both be rejected:

def simplerUnsoundExampleCellRejected(): Unit = {
    val a = Cell[X](X(0))
    val newV = X(1)
    val b = Cell(newV)
    swap(a, b)
    assert(a.v.x == 1)
    newV.x = 3  // <------ REJECTED
    assert(a.v.x == 1) // WRONG <--- should be 3
  }

[samuelchassot]

After reflexion, it is due to the fact that swap modifies the targets in AntiAliasing: it should indeed swap the targets because the values are swapped, so should the targets. Issue for now: the transform function returns only an Expr, not the Env; so not an easy fix.

[vkuncak]

Let's generalize it to return an environment! It's a non-trivial change, but opens up many different possibilities, including WSkS transductions as in https://www.brics.dk/PALE/

[samuelchassot]

Let's generalize it to return an environment! It's a non-trivial change, but opens up many different possibilities, including WSkS transductions as in https://www.brics.dk/PALE/

Okay! I'll work on that, maybe with @mario-bucev depending on his schedule!

[samuelchassot]

Let's try to first impose a restriction on swap to only take a variable as argument. This would solve this unsoundness issue.

[mario-bucev]

Unfortunately, AntiAliasing is difficult to trick:

import stainless.lang._

case class X(var x: BigInt)

object Unsound:
  def swaap(c1: Cell[X], c2: Cell[X]): Unit =
    swap(c1, c2) // Ok, only variables

  def simplerUnsoundExampleCell(): Unit = {
    val a = Cell[X](X(0))
    val newV = X(1)
    swaap(a, Cell(newV))
    assert(a.v.x == 1)
    newV.x = 3
    assert(a.v.x == 1) // WRONG <--- should be 3
  }

end Unsound

[samuelchassot]

And if we disallow ´Cell´ to appear in arguments altogether?

[mario-bucev]

I think this should work for non-insane cases. However, there is a normalization phase that may bind some arguments and pass these bindings to the function; this check should be done before this transformation e.g. in EffectsChecker.