Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

AntiAliasing: avoid rebuilding mutated objects when possible #1507

Merged
merged 1 commit into from
Apr 12, 2024

Conversation

mario-bucev
Copy link
Collaborator

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).

@mario-bucev mario-bucev merged commit 97caa41 into epfl-lara:main Apr 12, 2024
2 checks passed
@mario-bucev mario-bucev deleted the antialiasing-mapapp branch April 12, 2024 08:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants