From e6e3dab15f82e6388f1942bfdbdabfcaaf910530 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 Apr 2016 19:40:41 +0200
Subject: [PATCH] fix recursive function and higher order param
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 11 ++++++++-
.../HigherOrderFunctionsMutableParams5.scala | 23 +++++++++++++++++++
2 files changed, 33 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 9c2623b8d..3b80989e6 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -124,9 +124,18 @@ object AntiAliasingPhase extends TransformationPhase {
val freshBody = replaceFromIDs(rewritingMap.map(p => (p._1, p._2.toVariable)), body)
val explicitBody = makeSideEffectsExplicit(freshBody, fd, freshLocalVars, effects, updatedFunDefs, varsInScope)(ctx)
+ //only now we rewrite variables that stil refer to original higher order functions
+ val ftRewritings: Map[Identifier, Identifier] =
+ fd.params.zip(newFunDef.params).filter({
+ case (ValDef(IsTyped(oid, oft)), ValDef(IsTyped(nid, nft))) if oid != nft => true
+ case _ => false
+ }).map(p => (p._1.id, p._2.id)).toMap
+ val explicitBody2 = replaceFromIDs(ftRewritings.map(p => (p._1, p._2.toVariable)), explicitBody)
+
+
//WARNING: only works if side effects in Tuples are extracted from left to right,
// in the ImperativeTransformation phase.
- val finalBody: Expr = Tuple(explicitBody +: freshLocalVars.map(_.toVariable))
+ val finalBody: Expr = Tuple(explicitBody2 +: freshLocalVars.map(_.toVariable))
freshLocalVars.zip(aliasedParams).foldLeft(finalBody)((bd, vp) => {
LetVar(vp._1, Variable(vp._2), bd)
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala
new file mode 100644
index 000000000..64829e949
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala
@@ -0,0 +1,23 @@
+object HigherOrderFunctionsMutableParams5 {
+
+ case class A(var x: BigInt)
+
+ def repeat(f: (A, BigInt) => Unit, n: BigInt, a: A): Unit = {
+ require(n >= 0)
+ if(n > 0) {
+ f(a, n)
+ repeat(f, n-1, a)
+ }
+ }
+
+ def fImpl(a: A, n: BigInt): Unit = {
+ a.x += 1
+ }
+
+ def test(): BigInt = {
+ val a = A(0)
+ repeat(fImpl, 3, a)
+ a.x
+ } ensuring(_ == 3)
+
+}
--
GitLab