From 0fc04443a07af9a22c765c7ce92980c2e72954f1 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 22 Oct 2015 14:28:40 +0200
Subject: [PATCH] test evaluation order of function arguments
---
.../xlang/ImperativeCodeElimination.scala | 18 +++++++++++----
.../valid/FunInvocEvaluationOrder1.scala | 22 +++++++++++++++++++
.../valid/FunInvocEvaluationOrder2.scala | 17 ++++++++++++++
3 files changed, 53 insertions(+), 4 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7a00cb7f8..2f8b89796 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -230,6 +230,15 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
//a function invocation can update variables in scope.
case fi@FunctionInvocation(tfd, args) =>
+
+
+ val (recArgs, argScope, argFun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
+ val (accArgs, accScope, accFun) = acc
+ val (argVal, argScope, argFun) = toFunction(arg)
+ val newScope = (body: Expr) => argScope(replaceNames(argFun, accScope(body)))
+ (argVal +: accArgs, newScope, argFun ++ accFun)
+ })
+
val fd = tfd.fd
state.funDefsMapping.get(fd) match {
case Some((newFd, modifiedVars)) => {
@@ -238,16 +247,17 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val tmpTuple = FreshIdentifier("t", newFd.returnType)
val scope = (body: Expr) => {
- Let(tmpTuple, newInvoc,
+ argScope(Let(tmpTuple, newInvoc,
freshNames.zipWithIndex.foldRight(body)((p, b) =>
Let(p._1, TupleSelect(tmpTuple.toVariable, p._2 + 2), b))
- )
+ ))
}
- val newMap = modifiedVars.zip(freshNames).toMap
+ val newMap = modifiedVars.zip(freshNames).toMap ++ argFun
(TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
}
- case None => (fi, x => x, Map())
+ case None =>
+ (FunctionInvocation(tfd, recArgs).copiedFrom(fi), argScope, argFun)
}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
new file mode 100644
index 000000000..8ef668a2a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
@@ -0,0 +1,22 @@
+object FunInvocEvaluationOrder1 {
+
+ def test(): Int = {
+
+ var res = 10
+ justAddingStuff({
+ res += 1
+ res
+ }, {
+ res *= 2
+ res
+ }, {
+ res += 10
+ res
+ })
+
+ res
+ } ensuring(_ == 32)
+
+ def justAddingStuff(x: Int, y: Int, z: Int): Int = x + y + z
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
new file mode 100644
index 000000000..12090f0f3
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder2 {
+
+ def leftToRight(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def nested(x: BigInt, y: BigInt): BigInt = {
+ require(y >= x)
+ x + y
+ }
+
+ nested({a += 10; a}, {a *= 2; a})
+
+ } ensuring(_ == 30)
+
+}
--
GitLab