From 62c98020e9aead3a4cf38914b34c34dccb38e80b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 01:09:32 +0200
Subject: [PATCH] Function closure makes sure that all ids updated
---
.../purescala/DefinitionTransformer.scala | 5 ---
.../leon/purescala/FunctionClosure.scala | 3 ++
.../leon/purescala/TreeTransformer.scala | 4 +++
.../purescala/valid/Nested18.scala | 15 +++++++++
.../unit/purescala/FunctionClosureSuite.scala | 32 +++++++++++++++++++
5 files changed, 54 insertions(+), 5 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/Nested18.scala
diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 2588ed8fe..6dfea1dbe 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -45,11 +45,6 @@ class DefinitionTransformer(
idMap += id -> nid
nid
})
- case LetDef(fds, body) =>
- val rFds = fds map transform
- val rBody = transform(body)
- LetDef(rFds, rBody).copiedFrom(e)
-
case _ => super.transform(e)
}
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index e69050bf6..98d819eb2 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -180,6 +180,9 @@ object FunctionClosure extends TransformationPhase {
case _ => None
}(instBody)
+ //HACK to make sure substitution happened even in nested fundef
+ newFd.fullBody = replaceFromIDs(freeMap.map(p => (p._1, p._2.toVariable)), newFd.fullBody)
+
FunSubst(newFd, freeMap, tparamsMap.map{ case (from, to) => from.tp -> to})
}
diff --git a/src/main/scala/leon/purescala/TreeTransformer.scala b/src/main/scala/leon/purescala/TreeTransformer.scala
index d74da4f8f..a1f6e2ad6 100644
--- a/src/main/scala/leon/purescala/TreeTransformer.scala
+++ b/src/main/scala/leon/purescala/TreeTransformer.scala
@@ -38,6 +38,10 @@ trait TreeTransformer {
case LetVar(a, expr, body) =>
val newA = transform(a)
LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
+ case LetDef(fds, body) =>
+ val rFds = fds map transform
+ val rBody = transform(body)
+ LetDef(rFds, rBody).copiedFrom(e)
case CaseClass(cct, args) =>
CaseClass(transform(cct).asInstanceOf[CaseClassType], args map transform).copiedFrom(e)
case CaseClassSelector(cct, caseClass, selector) =>
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested18.scala b/src/test/resources/regression/verification/purescala/valid/Nested18.scala
new file mode 100644
index 000000000..a35c2f4b9
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested18.scala
@@ -0,0 +1,15 @@
+object Nested18 {
+
+ def test(a: BigInt): BigInt = {
+ require(a > 0)
+ def f(b: BigInt): BigInt = {
+ def g(c: BigInt): BigInt = {
+ require(a > 0)
+ c
+ }
+ g(b)
+ }
+ f(12)
+ }
+
+}
diff --git a/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala b/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
index faef38195..2019c0452 100644
--- a/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
+++ b/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
@@ -97,6 +97,38 @@ class FunctionClosureSuite extends FunSuite with helpers.ExpressionsDSL {
fail("Unexpected fun def: " + cfd)
}
})
+
+
+ val deeplyNested2 = new FunDef(FreshIdentifier("deeplyNested"), Seq(), Seq(ValDef(z.id)), IntegerType)
+ deeplyNested2.body = Some(Require(GreaterEquals(x, bi(0)), z))
+
+ val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
+ nested2.body = Some(LetDef(Seq(deeplyNested2), FunctionInvocation(deeplyNested2.typed, Seq(y))))
+
+ val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
+ fd2.body = Some(Require(GreaterEquals(x, bi(0)),
+ LetDef(Seq(nested2), FunctionInvocation(nested2.typed, Seq(x)))))
+
+ val cfds2 = FunctionClosure.close(fd2)
+ assert(cfds2.size === 3)
+
+ cfds2.foreach(cfd => {
+ if(cfd.id.name == "f") {
+ assert(cfd.returnType === fd2.returnType)
+ assert(cfd.params.size === fd2.params.size)
+ assert(freeVars(cfd).isEmpty)
+ } else if(cfd.id.name == "nested") {
+ assert(cfd.returnType === nested2.returnType)
+ assert(cfd.params.size === 2)
+ assert(freeVars(cfd).isEmpty)
+ } else if(cfd.id.name == "deeplyNested") {
+ assert(cfd.returnType === deeplyNested2.returnType)
+ assert(cfd.params.size === 2)
+ assert(freeVars(cfd).isEmpty)
+ } else {
+ fail("Unexpected fun def: " + cfd)
+ }
+ })
}
private def freeVars(fd: FunDef): Set[Identifier] = variablesOf(fd.fullBody) -- fd.paramIds
--
GitLab