From 959719aaa7145a74d942f78bb9831bdd957d4317 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 05:38:42 +0000
Subject: [PATCH] add support for array in argument list
---
src/main/scala/leon/ArrayTransformation.scala | 49 +++++++++++++++++--
testcases/regression/valid/Array4.scala | 7 +++
2 files changed, 51 insertions(+), 5 deletions(-)
create mode 100644 testcases/regression/valid/Array4.scala
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index dd1fee89e..a61605287 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -12,15 +12,54 @@ object ArrayTransformation extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => fd.body.map(body => {
- val newBody = transform(body)
- fd.body = Some(newBody)
- }))
- pgm
+ val newFuns: Seq[Definition] = allFuns.map(fd => {
+ if(fd.hasImplementation) {
+ val body = fd.body.get
+ id2id = Map()
+ val args = fd.args
+ val newFd =
+ if(args.exists(vd => containsArrayType(vd.tpe))) {
+ println("args has array")
+ val newArgs = args.map(vd => {
+ val freshId = FreshIdentifier(vd.id.name).setType(TupleType(Seq(vd.tpe, Int32Type)))
+ id2id += (vd.id -> freshId)
+ val newTpe = transform(vd.tpe)
+ VarDecl(freshId, newTpe)
+ })
+ val freshFunName = FreshIdentifier(fd.id.name)
+ val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
+ freshFunDef.fromLoop = fd.fromLoop
+ freshFunDef.parent = fd.parent
+ freshFunDef.precondition = fd.precondition
+ freshFunDef.postcondition = fd.postcondition
+ freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ freshFunDef
+ } else fd
+ val newBody = transform(body)
+ newFd.body = Some(newBody)
+ newFd
+ } else fd
+ })
+
+ val Program(id, ObjectDef(objId, _, invariants)) = pgm
+ val allClasses: Seq[Definition] = pgm.definedClasses
+ Program(id, ObjectDef(objId, allClasses ++ newFuns, invariants))
}
private var id2id: Map[Identifier, Identifier] = Map()
+ private def transform(tpe: TypeTree): TypeTree = tpe match {
+ case ArrayType(base) => TupleType(Seq(ArrayType(transform(base)), Int32Type))
+ case TupleType(tpes) => TupleType(tpes.map(transform))
+ case t => t
+ }
+ private def containsArrayType(tpe: TypeTree): Boolean = tpe match {
+ case ArrayType(base) => true
+ case TupleType(tpes) => tpes.exists(containsArrayType)
+ case t => false
+ }
+
+
private def transform(expr: Expr): Expr = expr match {
case fill@ArrayFill(length, default) => {
var rLength = transform(length)
diff --git a/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala
new file mode 100644
index 000000000..479f243ba
--- /dev/null
+++ b/testcases/regression/valid/Array4.scala
@@ -0,0 +1,7 @@
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ } ensuring(_ == 3)
+
+}
--
GitLab