diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 735462cd4acecaad24139b444b7f9e7f98fbbda0..7d0d94458291b71381d8719a25e13751ca3cdd9f 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -21,7 +21,6 @@ object ArrayTransformation extends Pass {
pgm
}
-
private var id2FreshId = Map[Identifier, Identifier]()
def transform(expr: Expr): Expr = expr match {
@@ -61,6 +60,10 @@ object ArrayTransformation extends Pass {
).setType(ra.getType)
res
}
+ case ArrayClone(a) => {
+ val ra = transform(a)
+ ra
+ }
case Let(i, v, b) => {
v.getType match {
case ArrayType(_) => {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 2b3187e1ae116fe01c79f2d408d1682287549dca..a05dd1f289ed4829ef0f29a49f31635f23bf5c1a 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -249,6 +249,7 @@ trait CodeExtraction extends Extractors {
val newParams = params.map(p => {
val ptpe = st2ps(p.tpt.tpe)
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ owners += (Variable(newID) -> None)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
})
@@ -259,6 +260,8 @@ trait CodeExtraction extends Extractors {
var realBody = body
var reqCont: Option[Expr] = None
var ensCont: Option[Expr] = None
+
+ currentFunDef = funDef
realBody match {
case ExEnsuredExpression(body2, resSym, contract) => {
@@ -289,15 +292,23 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
+ bodyAttempt.foreach(e =>
+ if(e.getType.isInstanceOf[ArrayType]) {
+ //println(owners)
+ //println(getOwner(e))
+ getOwner(e) match {
+ case Some(Some(fd)) if fd == funDef =>
+ case None =>
+ case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
+ }
+ })
reqCont.map(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
ensCont.map(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
funDef.body = bodyAttempt
funDef.precondition = reqCont
@@ -341,7 +352,10 @@ trait CodeExtraction extends Extractors {
private var currentFunDef: FunDef = null
- private var owners: Map[Expr, Option[FunDef]] = Map()
+
+ //This is a bit missleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
+ //that it can have any owner
+ private var owners: Map[Expr, Option[FunDef]] = Map()
/** Forces conversion from scalac AST to purescala AST, throws an Exception
* if impossible. If not in 'silent mode', non-pure AST nodes are reported as
@@ -408,6 +422,7 @@ trait CodeExtraction extends Extractors {
val newParams = params.map(p => {
val ptpe = scalaType2PureScala(unit, silent) (p.tpt.tpe)
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ owners += (Variable(newID) -> None)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
})
@@ -451,20 +466,21 @@ trait CodeExtraction extends Extractors {
}
bodyAttempt.foreach(e =>
- if(e.getType.isInstanceOf[ArrayType] && owners.get(e).getOrElse(null) != funDef) {
- unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
- throw ImpureCodeEncounteredException(realBody)
+ if(e.getType.isInstanceOf[ArrayType]) {
+ getOwner(e) match {
+ case Some(Some(fd)) if fd == funDef =>
+ case None =>
+ case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
+ }
})
reqCont.foreach(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
ensCont.foreach(e =>
if(containsLetDef(e)) {
unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- throw ImpureCodeEncounteredException(realBody)
})
funDef.body = bodyAttempt
funDef.precondition = reqCont
@@ -500,6 +516,16 @@ trait CodeExtraction extends Extractors {
val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
val valTree = rec(bdy)
+ handleRest = false
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
val restTree = rest match {
case Some(rst) => {
varSubsts(vs) = (() => Variable(newID))
@@ -509,7 +535,6 @@ trait CodeExtraction extends Extractors {
}
case None => UnitLiteral
}
- handleRest = false
val res = Let(newID, valTree, restTree)
res
}
@@ -517,9 +542,11 @@ trait CodeExtraction extends Extractors {
val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
defsToDefs += (dd.symbol -> funDef)
val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
+ val oldCurrentFunDef = currentFunDef
mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
val funDefWithBody = extractFunDef(funDef, b)
mutableVarSubsts ++= oldMutableVarSubst
+ currentFunDef = oldCurrentFunDef
val restTree = rest match {
case Some(rst) => rec(rst)
case None => UnitLiteral
@@ -530,15 +557,25 @@ trait CodeExtraction extends Extractors {
}
case ExVarDef(vs, tpt, bdy) => {
val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- binderTpe match {
- case ArrayType(_) =>
- unit.error(tree.pos, "Cannot declare array variables, only val are alllowed")
- throw ImpureCodeEncounteredException(tree)
- case _ =>
- }
+ //binderTpe match {
+ // case ArrayType(_) =>
+ // unit.error(tree.pos, "Cannot declare array variables, only val are alllowed")
+ // throw ImpureCodeEncounteredException(tree)
+ // case _ =>
+ //}
val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
val valTree = rec(bdy)
mutableVarSubsts += (vs -> (() => Variable(newID)))
+ handleRest = false
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
val restTree = rest match {
case Some(rst) => {
varSubsts(vs) = (() => Variable(newID))
@@ -548,7 +585,6 @@ trait CodeExtraction extends Extractors {
}
case None => UnitLiteral
}
- handleRest = false
val res = LetVar(newID, valTree, restTree)
res
}
@@ -557,6 +593,14 @@ trait CodeExtraction extends Extractors {
case Some(fun) => {
val Variable(id) = fun()
val rhsTree = rec(rhs)
+ if(rhsTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(rhsTree) match {
+ case None =>
+ case Some(_) =>
+ unit.error(nextExpr.pos, "Cannot alias array")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+ }
Assignment(id, rhsTree)
}
case None => {
@@ -830,6 +874,16 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tree)
}
}
+ getOwner(lhsRec) match {
+ case Some(Some(fd)) if fd != currentFunDef =>
+ unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
+ throw ImpureCodeEncounteredException(nextExpr)
+ case Some(None) =>
+ unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
+ throw ImpureCodeEncounteredException(nextExpr)
+ case Some(_) =>
+ case None => sys.error("This array: " + lhsRec + " should have had an owner")
+ }
val indexRec = rec(index)
val newValueRec = rec(newValue)
ArrayUpdate(lhsRec, indexRec, newValueRec).setPosInfo(update.pos.line, update.pos.column)
@@ -838,6 +892,10 @@ trait CodeExtraction extends Extractors {
val rt = rec(t)
ArrayLength(rt)
}
+ case ExArrayClone(t) => {
+ val rt = rec(t)
+ ArrayClone(rt)
+ }
case ExArrayFill(baseType, length, defaultValue) => {
val underlying = scalaType2PureScala(unit, silent)(baseType.tpe)
val lengthRec = rec(length)
@@ -941,17 +999,20 @@ trait CodeExtraction extends Extractors {
}
}
- if(handleRest) {
+ val res = if(handleRest) {
rest match {
case Some(rst) => {
val recRst = rec(rst)
- PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ val block = PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ block
}
case None => psExpr
}
} else {
psExpr
}
+
+ res
}
rec(tree)
}
@@ -994,4 +1055,27 @@ trait CodeExtraction extends Extractors {
def mkPosString(pos: scala.tools.nsc.util.Position) : String = {
pos.line + "," + pos.column
}
+
+ def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
+ case Let(_, _, rest) => getReturnedExpr(rest)
+ case LetVar(_, _, rest) => getReturnedExpr(rest)
+ case PBlock(_, rest) => getReturnedExpr(rest)
+ case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
+ case _ => Seq(expr)
+ }
+
+ def getOwner(exprs: Seq[Expr]): Option[Option[FunDef]] = {
+ val exprOwners: Seq[Option[Option[FunDef]]] = exprs.map(owners.get(_))
+ if(exprOwners.exists(_ == None))
+ None
+ else if(exprOwners.exists(_ == Some(None)))
+ Some(None)
+ else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
+ Some(None)
+ else
+ exprOwners(0)
+ }
+
+ def getOwner(expr: Expr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
+
}
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 13b6392edbaf0e61d0182c27e327610d76d64edc..b45fef576bbc8d06a87f9289f4be5822ec884fa5 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -672,6 +672,13 @@ trait Extractors {
}
}
+ object ExArrayClone {
+ def unapply(tree: Apply): Option[Tree] = {println(tree); tree match {
+ case Apply(Select(t, n), List()) if (n.toString == "clone") => Some(t)
+ case _ => None
+ }}
+ }
+
object ExArrayFill {
def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f03c624af8acddea63ad6c68f993446ffb3cda92..21a9393b142b177d49ba985988512c5dbe885c5f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -253,6 +253,10 @@ object PrettyPrinter {
pp(a, sb, lvl)
sb.append(".length")
}
+ case ArrayClone(a) => {
+ pp(a, sb, lvl)
+ sb.append(".clone")
+ }
case fill@ArrayFill(size, v) => {
sb.append("Array.fill(")
pp(size, sb, lvl)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 1c015cfe6e1127a178746786d2fe7678c6b30c4d..aff4f7c5560ebf7a6b70989e11d3291b9a41dc5e 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -399,6 +399,10 @@ object Trees {
val fixedType = Int32Type
}
case class FiniteArray(exprs: Seq[Expr]) extends Expr
+ case class ArrayClone(array: Expr) extends Expr {
+ if(array.getType != Untyped)
+ setType(array.getType)
+ }
/* List operations */
case class NilList(baseType: TypeTree) extends Expr with Terminal
@@ -433,6 +437,7 @@ object Trees {
case Assignment(id, e) => Some((e, Assignment(id, _)))
case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
case ArrayLength(a) => Some((a, ArrayLength))
+ case ArrayClone(a) => Some((a, ArrayClone))
case ArrayMake(t) => Some((t, ArrayMake))
case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
@@ -837,6 +842,7 @@ object Trees {
case LetDef(_, _) => false
case ArrayUpdate(_, _, _) => false
case ArrayMake(_) => false
+ case ArrayClone(_) => false
case Epsilon(_) => false
case _ => true
}
@@ -849,6 +855,7 @@ object Trees {
case LetDef(_, _) => false
case ArrayUpdate(_, _, _) => false
case ArrayMake(_) => false
+ case ArrayClone(_) => false
case Epsilon(_) => false
case _ => b
}
diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala
index 8e85143ac10414572114f6a24c09e194853af8de..3551ebf16416f68bd932adc512177edc6f2611d8 100644
--- a/testcases/BubbleSort.scala
+++ b/testcases/BubbleSort.scala
@@ -8,7 +8,7 @@ object BubbleSort {
require(a.length >= 1)
var i = a.length - 1
var j = 0
- val sa = a
+ val sa = a.clone
(while(i > 0) {
j = 0
(while(j < i) {
diff --git a/testcases/regression/error/Array10.scala b/testcases/regression/error/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9973626b83a01c7a8a944bcf808274d7989b3a66
--- /dev/null
+++ b/testcases/regression/error/Array10.scala
@@ -0,0 +1,12 @@
+object Array10 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array2.scala b/testcases/regression/error/Array2.scala
index 8ae7054ca20927b87d6032810f5e4fed87e4ba86..9154460c37237761b6c8f2d0ecb0b34fb3ec0bf6 100644
--- a/testcases/regression/error/Array2.scala
+++ b/testcases/regression/error/Array2.scala
@@ -1,8 +1,9 @@
object Array2 {
def foo(): Int = {
- var a = Array.fill(5)(5)
- 0
+ val a = Array.fill(5)(5)
+ val b = a
+ b(3)
}
}
diff --git a/testcases/regression/error/Array3.scala b/testcases/regression/error/Array3.scala
index 451dd9db06873a8dc9c88a4d5c8285c5ab063a73..a2c2fbd6ddfde2b3cca2dcc08fb61a79f0ae471c 100644
--- a/testcases/regression/error/Array3.scala
+++ b/testcases/regression/error/Array3.scala
@@ -4,7 +4,8 @@ object Array3 {
val a = Array.fill(5)(5)
if(a.length > 2)
a(1) = 2
- else 0
+ else
+ 0
0
}
diff --git a/testcases/regression/error/Array4.scala b/testcases/regression/error/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ab0115af5e8737c6baab851822643490e79334f
--- /dev/null
+++ b/testcases/regression/error/Array4.scala
@@ -0,0 +1,8 @@
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ val b = a
+ b(3)
+ }
+
+}
diff --git a/testcases/regression/error/Array5.scala b/testcases/regression/error/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..005d3d389dd1e748d139283a6fbdcb93aa8d525c
--- /dev/null
+++ b/testcases/regression/error/Array5.scala
@@ -0,0 +1,10 @@
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2) = 4
+ a(2)
+ }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/error/Array6.scala b/testcases/regression/error/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15c87a08554c7e9563cbad9b47a881376e45a4c5
--- /dev/null
+++ b/testcases/regression/error/Array6.scala
@@ -0,0 +1,10 @@
+
+object Array6 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array7.scala b/testcases/regression/error/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..abb83e1c0bd931bf1d41a132fef6fb74ea25318b
--- /dev/null
+++ b/testcases/regression/error/Array7.scala
@@ -0,0 +1,9 @@
+object Array7 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ var b = a
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/error/Array8.scala b/testcases/regression/error/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..89af32efdb89273ecf6b275b5a8f2f787bb73a1f
--- /dev/null
+++ b/testcases/regression/error/Array8.scala
@@ -0,0 +1,7 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ a
+ }
+
+}
diff --git a/testcases/regression/error/Array9.scala b/testcases/regression/error/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5dc9d3aea24f7c38b8a374659058c9d0ca7fb336
--- /dev/null
+++ b/testcases/regression/error/Array9.scala
@@ -0,0 +1,11 @@
+object Array9 {
+
+ def foo(a: Array[Int]): Int = {
+ def rec(): Array[Int] = {
+ a
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/testcases/regression/valid/Array10.scala b/testcases/regression/valid/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311
--- /dev/null
+++ b/testcases/regression/valid/Array10.scala
@@ -0,0 +1,9 @@
+object Array10 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val b = a.clone
+ b(0)
+ } ensuring(res => res == a(0))
+
+}
diff --git a/testcases/regression/valid/Array9.scala b/testcases/regression/valid/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f49333236abfaf63caa278405a89670b1c9c115d
--- /dev/null
+++ b/testcases/regression/valid/Array9.scala
@@ -0,0 +1,15 @@
+object Array9 {
+
+ def foo(i: Int): Array[Int] = {
+ require(i > 0)
+ val a = Array.fill(i)(0)
+ a
+ } ensuring(res => res.length == i)
+
+ def bar(i: Int): Int = {
+ require(i > 0)
+ val b = foo(i)
+ b(0)
+ }
+
+}