From 2db018edaf2168ef64571bd2c53f8acc161c5cec Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 22 Apr 2016 20:04:39 +0200
Subject: [PATCH] fix issue with nested functions updating mutable param
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 5 +++--
src/main/scala/leon/xlang/ExprOps.scala | 10 ++++++++++
.../valid/NestedFunParamsMutation3.scala | 20 +++++++++++++++++++
3 files changed, 33 insertions(+), 2 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation3.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 2b7176fb3..baa8a0d2f 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -15,6 +15,7 @@ import leon.purescala.DependencyFinder
import leon.purescala.DefinitionTransformer
import leon.utils.Bijection
import leon.xlang.Expressions._
+import leon.xlang.ExprOps._
object AntiAliasingPhase extends TransformationPhase {
@@ -210,7 +211,7 @@ object AntiAliasingPhase extends TransformationPhase {
val newBody = fd.body.map(body => {
- val freshBody = replaceFromIDs(rewritingMap.map(p => (p._1, p._2.toVariable)), body)
+ val freshBody = rewriteIDs(rewritingMap, body)
val explicitBody = makeSideEffectsExplicit(freshBody, fd, freshLocalVars, effects, updatedFunDefs, varsInScope)(ctx)
//only now we rewrite function parameters that changed names when the new function was introduced
@@ -352,7 +353,7 @@ object AntiAliasingPhase extends TransformationPhase {
}
//we need to replace local fundef by the new updated fun defs.
- case l@LetDef(fds, body) => {
+ case l@LetDef(fds, body) => {
//this might be traversed several time in case of doubly nested fundef,
//so we need to ignore the second times by checking if updatedFunDefs
//contains a mapping or not
diff --git a/src/main/scala/leon/xlang/ExprOps.scala b/src/main/scala/leon/xlang/ExprOps.scala
index e4680286f..35d7914e2 100644
--- a/src/main/scala/leon/xlang/ExprOps.scala
+++ b/src/main/scala/leon/xlang/ExprOps.scala
@@ -6,6 +6,7 @@ package xlang
import purescala.Expressions._
import xlang.Expressions._
import purescala.ExprOps._
+import purescala.Common._
object ExprOps {
@@ -38,5 +39,14 @@ object ExprOps {
None
})(expr)
}
+
+ def rewriteIDs(substs: Map[Identifier, Identifier], expr: Expr) : Expr = {
+ postMap({
+ case Assignment(i, v) => substs.get(i).map(ni => Assignment(ni, v))
+ case FieldAssignment(o, i, v) => substs.get(i).map(ni => FieldAssignment(o, ni, v))
+ case Variable(i) => substs.get(i).map(ni => Variable(ni))
+ case _ => None
+ })(expr)
+ }
}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation3.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation3.scala
new file mode 100644
index 000000000..e4f149333
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation3.scala
@@ -0,0 +1,20 @@
+object NestedFunParamsMutation3 {
+
+ case class Counter(var i: BigInt) {
+ def reset() = {
+ i = 0
+ }
+ }
+
+
+ def main(c: Counter): Unit = {
+
+ def sub(): Unit = {
+ c.reset()
+ }
+ sub()
+ assert(c.i == 0)
+ }
+
+}
+
--
GitLab