epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 49 forks source link

AntiAliasing: avoid rebuilding mutated objects when possible #1507

Closed mario-bucev closed 3 months ago

mario-bucev commented 3 months ago

AntiAliasing#mapApplication used to "rebuild" the mutated object(s) from function calls where a reassignment could be possible. For instance, if we have:

case class Ref(var x: Int, var y: Int)
case class RefRef(var lhs: Ref, var rhs: Ref)

def modifyLhs(rr: RefRef, v: Int): Unit = {
  rr.lhs.x = v
  rr.lhs.y = v
}
def test(testRR: RefRef): Unit = {
  val rrAlias = testRR
  val lhsAlias = testRR.lhs
  modifyLhs(testRR, 123)
  // ...
}

Then before this PR, mapApplication would transform test as follows:

def modifyLhs(rr: RefRef, v: Int): (Unit, RefRef) = 
  ((), RefRef(Ref(v, v), rr.rhs))

def test(testRR: RefRef) = {
  var rrAlias: RefRef = testRR
  var lhsAlias: Ref = testRR.lhs
  val res: (Unit, RefRef) = modifyLhs(testRR, 123)
  testRR = RefRef(Ref(res._2.lhs.x, testRR.lhs.y), testRR.rhs)
  lhsAlias = testRR.lhs
  rrAlias = testRR
  testRR = RefRef(Ref(testRR.lhs.x, res._2.lhs.y), testRR.rhs)
  lhsAlias = testRR.lhs
  rrAlias = testRR
  // ...
}

This is due to applying each effect individually. With this PR, test is transformed as follows:

def test(testRR: RefRef) = {
  var rrAlias: RefRef = testRR
  var lhsAlias: Ref = testRR.lhs
  val res: (Unit, RefRef) = modifyLhs(testRR, 123)
  testRR = res._2
  rrAlias = testRR
  lhsAlias = testRR.lhs
  // ...
}

This in part resolves the issue when an @opaque function mutates an argument and uses the mutated argument in a ensuring, causing a discrepancy between the "updated" object used in the ensuring and the "rebuilt" object (for which we would like to use the ensuring property, but fail to do so; see valid/OpaqueMutation which used to fail).