diff --git a/PERMISSIONS b/PERMISSIONS
index dbe09f25f5c0ed5a33d5f2fe757e84f00f3a516d..20019048dd418bfd5e6eba56ffaa50c6a279e1d3 100755
--- a/PERMISSIONS
+++ b/PERMISSIONS
@@ -12,5 +12,5 @@ tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
exit $_
# **Do not** add new lines after the following two!
-WRITERS kuncak psuter rblanc edarulov
-READERS @lara mazimmer hardy
+WRITERS kuncak psuter rblanc edarulov hojjat
+READERS @lara mazimmer hardy amin
diff --git a/demo/Arith.scala b/demo/Arith.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d4b02f51b5e532a15b9fb3571534316e0cc962ce
--- /dev/null
+++ b/demo/Arith.scala
@@ -0,0 +1,41 @@
+import leon.Utils._
+
+object Arith {
+
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/demo/BubbleSortBug.scala b/demo/BubbleSortBug.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a25554f0305d57c53774cdc0b4d514393217b4f2
--- /dev/null
+++ b/demo/BubbleSortBug.scala
@@ -0,0 +1,39 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object BubbleSortBug {
+
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) < sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(j >= 0 && j <= i && i < sa.length)
+ i = i - 1
+ }) invariant(i >= 0 && i < sa.length)
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
+
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+
+}
diff --git a/demo/List.scala b/demo/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..302e86774c7d1e68e08d48ce957c87ec483b3d56
--- /dev/null
+++ b/demo/List.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object List {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): Int = waypoint(1, (l match {
+ case Cons(_, tail) => sizeTail(tail, 1)
+ case Nil() => 0
+ })) ensuring(_ >= 0)
+
+
+ def sizeTail(l2: List, acc: Int): Int = l2 match {
+ case Cons(_, tail) => sizeTail(tail, acc+1)
+ case Nil() => acc
+ }
+
+}
diff --git a/demo/ListOperations.scala b/demo/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a4fc4f8dc44a90f59a772b52b1a05053316e94d2
--- /dev/null
+++ b/demo/ListOperations.scala
@@ -0,0 +1,107 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case class IPNil() extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: Int, snd: Int) extends IntPair
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : IntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
+ def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv(l: List) : Boolean = {
+ size(l) == sizeTailRec(l)
+ } holds
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def sizeAndContent(l: List) : Boolean = {
+ size(l) == 0 || content(l) != Set.empty[Int]
+ } holds
+
+ def drunk(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
+ def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
+ def reverse0(l1: List, l2: List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverse0(xs, Cons(x, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ def append(l1 : List, l2 : List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x, append(xs, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+
+ @induct
+ def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+
+ def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
+ (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
+ } holds
+
+ @induct
+ def sizeAppend(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
+ @induct
+ def concat(l1: List, l2: List) : List =
+ concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
+ case Nil() => l2 match {
+ case Nil() => reverse(l3)
+ case Cons(y, ys) => {
+ concat0(Nil(), ys, Cons(y, l3))
+ }
+ }
+ case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+}
diff --git a/demo/MaxSum.scala b/demo/MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ba724d255c23b782e1b4de716ccc8d50043e2059
--- /dev/null
+++ b/demo/MaxSum.scala
@@ -0,0 +1,38 @@
+import leon.Utils._
+
+/* VSTTE 2010 challenge 1 */
+
+object MaxSum {
+
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < a.length) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+ (sum, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= a.length)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+}
diff --git a/demo/RedBlackTree.scala b/demo/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f
--- /dev/null
+++ b/demo/RedBlackTree.scala
@@ -0,0 +1,117 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+}
diff --git a/run-demo b/run-demo
new file mode 100755
index 0000000000000000000000000000000000000000..a3db30e6682f1483ccc66b79cc65d5222e82bb90
--- /dev/null
+++ b/run-demo
@@ -0,0 +1 @@
+./leon --timeout=10 --noLuckyTests $@
diff --git a/run-demo-testgen b/run-demo-testgen
new file mode 100755
index 0000000000000000000000000000000000000000..90b0479f2dc548a4b2df35042cc802604aca3ee3
--- /dev/null
+++ b/run-demo-testgen
@@ -0,0 +1 @@
+./leon --nodefaults --extensions=leon.TestGeneration $@
diff --git a/run-tests.sh b/run-tests.sh
index cedaea2d3ec3e75c79161e5a33ac3225368a372d..e39418fb354226b767aedf5c7d1de462707bdf5e 100755
--- a/run-tests.sh
+++ b/run-tests.sh
@@ -6,7 +6,7 @@ failedtests=""
for f in testcases/regression/valid/*.scala; do
echo -n "Running $f, expecting VALID, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = valid ]; then
nbsuccess=$((nbsuccess + 1))
@@ -17,7 +17,7 @@ done
for f in testcases/regression/invalid/*.scala; do
echo -n "Running $f, expecting INVALID, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = invalid ]; then
nbsuccess=$((nbsuccess + 1))
@@ -28,7 +28,7 @@ done
for f in testcases/regression/error/*.scala; do
echo -n "Running $f, expecting ERROR, got: "
- res=`./leon --timeout=5 --oneline "$f"`
+ res=`./leon --noLuckyTests --timeout=10 --oneline "$f"`
echo $res | tr [a-z] [A-Z]
if [ $res = error ]; then
nbsuccess=$((nbsuccess + 1))
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 8c950fd87215da16ebdebc1b13c88dbb78ba66e3..176cb96b1f9fe411be0553afca3a31895d7e962a 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -68,6 +68,7 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
allVCs ++= tactic.generatePostconditions(funDef)
allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+ allVCs ++= tactic.generateArrayAccessChecks(funDef)
}
allVCs = allVCs.sortWith((vc1, vc2) => {
val id1 = vc1.funDef.id.name
diff --git a/src/main/scala/leon/Annotations.scala b/src/main/scala/leon/Annotations.scala
index 0831c8ff81ae212d6e0fd10d5a847c77c88186f4..85e8c00e0379c42f000b61ac14861190bb46963a 100644
--- a/src/main/scala/leon/Annotations.scala
+++ b/src/main/scala/leon/Annotations.scala
@@ -3,4 +3,5 @@ package leon
object Annotations {
class induct extends StaticAnnotation
class axiomatize extends StaticAnnotation
+ class main extends StaticAnnotation
}
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7d0d94458291b71381d8719a25e13751ca3cdd9f
--- /dev/null
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -0,0 +1,298 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object ArrayTransformation extends Pass {
+
+ val description = "Add bound checking for array access and remove array update with side effect"
+
+ def apply(pgm: Program): Program = {
+
+ val allFuns = pgm.definedFunctions
+ allFuns.foreach(fd => {
+ id2FreshId = Map()
+ fd.precondition = fd.precondition.map(transform)
+ fd.body = fd.body.map(transform)
+ fd.postcondition = fd.postcondition.map(transform)
+ })
+ pgm
+ }
+
+ private var id2FreshId = Map[Identifier, Identifier]()
+
+ def transform(expr: Expr): Expr = expr match {
+ case sel@ArraySelect(a, i) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ ArraySelect(ra, ri).setType(sel.getType).setPosInfo(sel),
+ Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
+ ).setType(sel.getType)
+ res
+ }
+ case up@ArrayUpdate(a, i, v) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val rv = transform(v)
+ val Variable(id) = ra
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up)),
+ Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ ).setType(UnitType)
+ res
+ }
+ case up@ArrayUpdated(a, i, v) => {
+ val ra = transform(a)
+ val ri = transform(i)
+ val rv = transform(v)
+ val length = ArrayLength(ra)
+ val res = IfExpr(
+ And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
+ ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up),
+ Error("Index out of bound").setType(ra.getType).setPosInfo(up)
+ ).setType(ra.getType)
+ res
+ }
+ case ArrayClone(a) => {
+ val ra = transform(a)
+ ra
+ }
+ case Let(i, v, b) => {
+ v.getType match {
+ case ArrayType(_) => {
+ val freshIdentifier = FreshIdentifier("t").setType(i.getType)
+ id2FreshId += (i -> freshIdentifier)
+ LetVar(freshIdentifier, transform(v), transform(b))
+ }
+ case _ => Let(i, transform(v), transform(b))
+ }
+ }
+ case Variable(i) => {
+ val freshId = id2FreshId.get(i).getOrElse(i)
+ Variable(freshId)
+ }
+
+ case LetVar(id, e, b) => {
+ val er = transform(e)
+ val br = transform(b)
+ LetVar(id, er, br)
+ }
+ case wh@While(c, e) => {
+ val newWh = While(transform(c), transform(e))
+ newWh.invariant = wh.invariant.map(i => transform(i))
+ newWh.setPosInfo(wh)
+ newWh
+ }
+
+ case ite@IfExpr(c, t, e) => {
+ val rc = transform(c)
+ val rt = transform(t)
+ val re = transform(e)
+ IfExpr(rc, rt, re).setType(rt.getType)
+ }
+
+ case m @ MatchExpr(scrut, cses) => {
+ val scrutRec = transform(scrut)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ }
+ case LetDef(fd, b) => {
+ fd.precondition = fd.precondition.map(transform)
+ fd.body = fd.body.map(transform)
+ fd.postcondition = fd.postcondition.map(transform)
+ val rb = transform(b)
+ LetDef(fd, rb)
+ }
+ case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ case (t: Terminal) => t
+ case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+ }
+
+ //val newFuns: Seq[FunDef] = allFuns.map(fd => {
+ // if(fd.hasImplementation) {
+ // val args = fd.args
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // } else fd
+ //})
+
+ //allFuns.zip(newFuns).foreach{ case (ofd, nfd) => ofd.body.map(body => {
+ // nfd.precondition = ofd.precondition.map(transform)
+ // nfd.postcondition = ofd.postcondition.map(transform)
+ // val newBody = transform(body)
+ // nfd.body = Some(newBody)
+ //})}
+
+ //val Program(id, ObjectDef(objId, _, invariants)) = pgm
+ //val allClasses: Seq[Definition] = pgm.definedClasses
+ //Program(id, ObjectDef(objId, allClasses ++ newFuns, invariants))
+
+
+ //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 var id2id: Map[Identifier, Identifier] = Map()
+ //private var fd2fd: Map[FunDef, FunDef] = Map()
+
+ //private def transform(expr: Expr): Expr = expr match {
+ // case fill@ArrayFill(length, default) => {
+ // var rLength = transform(length)
+ // val rDefault = transform(default)
+ // val rFill = ArrayMake(rDefault).setType(fill.getType)
+ // Tuple(Seq(rFill, rLength)).setType(TupleType(Seq(fill.getType, Int32Type)))
+ // }
+ // case sel@ArraySelect(a, i) => {
+ // val ar = transform(a)
+ // val ir = transform(i)
+ // val length = TupleSelect(ar, 2).setType(Int32Type)
+ // IfExpr(
+ // And(GreaterEquals(ir, IntLiteral(0)), LessThan(ir, length)),
+ // ArraySelect(TupleSelect(ar, 1).setType(ArrayType(sel.getType)), ir).setType(sel.getType).setPosInfo(sel),
+ // Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
+ // ).setType(sel.getType)
+ // }
+ // case up@ArrayUpdate(a, i, v) => {
+ // val ar = transform(a)
+ // val ir = transform(i)
+ // val vr = transform(v)
+ // val Variable(id) = ar
+ // val length = TupleSelect(ar, 2).setType(Int32Type)
+ // val array = TupleSelect(ar, 1).setType(ArrayType(v.getType))
+ // IfExpr(
+ // And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
+ // Assignment(
+ // id,
+ // Tuple(Seq(
+ // ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
+ // length)
+ // ).setType(TupleType(Seq(array.getType, Int32Type)))),
+ // Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ // ).setType(UnitType)
+ // }
+ // case ArrayLength(a) => {
+ // val ar = transform(a)
+ // TupleSelect(ar, 2).setType(Int32Type)
+ // }
+ // case Let(i, v, b) => {
+ // val vr = transform(v)
+ // v.getType match {
+ // case ArrayType(_) => {
+ // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
+ // id2id += (i -> freshIdentifier)
+ // val br = transform(b)
+ // LetVar(freshIdentifier, vr, br)
+ // }
+ // case _ => {
+ // val br = transform(b)
+ // Let(i, vr, br)
+ // }
+ // }
+ // }
+ // case LetVar(id, e, b) => {
+ // val er = transform(e)
+ // val br = transform(b)
+ // LetVar(id, er, br)
+ // }
+ // case wh@While(c, e) => {
+ // val newWh = While(transform(c), transform(e))
+ // newWh.invariant = wh.invariant.map(i => transform(i))
+ // newWh.setPosInfo(wh)
+ // }
+
+ // case ite@IfExpr(c, t, e) => {
+ // val rc = transform(c)
+ // val rt = transform(t)
+ // val re = transform(e)
+ // IfExpr(rc, rt, re).setType(rt.getType)
+ // }
+
+ // case m @ MatchExpr(scrut, cses) => {
+ // val scrutRec = transform(scrut)
+ // val csesRec = cses.map{
+ // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ // }
+ // val tpe = csesRec.head.rhs.getType
+ // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ // }
+ // case LetDef(fd, b) => {
+ // val newFd = if(fd.hasImplementation) {
+ // val body = fd.body.get
+ // val args = fd.args
+ // val newFd =
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.precondition = fd.precondition.map(transform)
+ // freshFunDef.postcondition = fd.postcondition.map(transform)
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // val newBody = transform(body)
+ // newFd.body = Some(newBody)
+ // newFd
+ // } else fd
+ // val rb = transform(b)
+ // LetDef(newFd, rb)
+ // }
+ // case FunctionInvocation(fd, args) => {
+ // val rargs = args.map(transform)
+ // val rfd = fd2fd.get(fd).getOrElse(fd)
+ // FunctionInvocation(rfd, rargs)
+ // }
+
+ // case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ // case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ // case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ // case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
+ // case (t: Terminal) => t
+ // case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+
+ //}
+
+}
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index a01d025431c2ec3c704a1950410334fd322abae9..70ad17f36150a47f846fe67a8bf8db350e03a9bf 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -194,6 +194,35 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
toRet
}
+ def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+ val toRet = if (function.hasBody) {
+ val cleanBody = matchToIfThenElse(function.body.get)
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case Error("Index out of bound") => true
+ case _ => false
+ }), cleanBody)
+
+ def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
+ Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds)))
+ } else {
+ Not(And(conds))
+ }
+
+ allPathConds.map(pc =>
+ new VerificationCondition(
+ withPrecIfDefined(pc._1),
+ if(function.fromLoop) function.parent.get else function,
+ VCKind.ArrayAccess,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ ).toSeq
+ } else {
+ Seq.empty
+ }
+
+ toRet
+ }
+
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
generateMapAccessChecks(function)
}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index e8409aa317356679938accb064985c284e1e0e23..d5c5745c19bcb8b3c58c1496c6a63547d179dcee 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -77,6 +77,7 @@ object Evaluator {
case _ => throw TypeErrorEx(TypeError(first, BooleanType))
}
}
+ case Waypoint(_, arg) => rec(ctx, arg)
case FunctionInvocation(fd, args) => {
val evArgs = args.map(a => rec(ctx, a))
// build a context for the function...
@@ -85,7 +86,9 @@ object Evaluator {
if(fd.hasPrecondition) {
rec(frame, matchToIfThenElse(fd.precondition.get)) match {
case BooleanLiteral(true) => ;
- case BooleanLiteral(false) => throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.")
+ case BooleanLiteral(false) => {
+ throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.: " + fd.precondition.get)
+ }
case other => throw TypeErrorEx(TypeError(other, BooleanType))
}
}
@@ -242,11 +245,50 @@ object Evaluator {
case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
case (l,r) => throw TypeErrorEx(TypeError(r, SetType(l.getType)))
}
+ case SetCardinality(s) => {
+ val sr = rec(ctx, s)
+ sr match {
+ case EmptySet(_) => IntLiteral(0)
+ case FiniteSet(els) => IntLiteral(els.size)
+ case _ => throw TypeErrorEx(TypeError(sr, SetType(AnyType)))
+ }
+ }
case f @ FiniteSet(els) => FiniteSet(els.map(rec(ctx,_)).distinct).setType(f.getType)
case e @ EmptySet(_) => e
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
+ case u @ UnitLiteral => u
+
+ case f @ ArrayFill(length, default) => {
+ val rDefault = rec(ctx, default)
+ val rLength = rec(ctx, length)
+ val IntLiteral(iLength) = rLength
+ FiniteArray((1 to iLength).map(_ => rDefault).toSeq)
+ }
+ case ArrayLength(a) => {
+ var ra = rec(ctx, a)
+ while(!ra.isInstanceOf[FiniteArray])
+ ra = ra.asInstanceOf[ArrayUpdated].array
+ IntLiteral(ra.asInstanceOf[FiniteArray].exprs.size)
+ }
+ case ArrayUpdated(a, i, v) => {
+ val ra = rec(ctx, a)
+ val ri = rec(ctx, i)
+ val rv = rec(ctx, v)
+
+ val IntLiteral(index) = ri
+ val FiniteArray(exprs) = ra
+ FiniteArray(exprs.updated(index, rv))
+ }
+ case ArraySelect(a, i) => {
+ val IntLiteral(index) = rec(ctx, i)
+ val FiniteArray(exprs) = rec(ctx, a)
+ exprs(index)
+ }
+ case FiniteArray(exprs) => {
+ FiniteArray(exprs.map(e => rec(ctx, e)))
+ }
case f @ FiniteMap(ss) => FiniteMap(ss.map(rec(ctx,_)).distinct.asInstanceOf[Seq[SingletonMap]]).setType(f.getType)
case e @ EmptyMap(_,_) => e
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 5905ec99820c7dff51cef6fef88705017a17614d..e9fdde89c3555b41b47b696c542733b0bf411830 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -46,6 +46,7 @@ object Extensions {
def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+ def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
}
// The rest of the code is for dynamically loading extensions
@@ -98,6 +99,7 @@ object Extensions {
allLoaded = defaultExtensions ++ loaded
analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
+ //analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 919b5b4f9740768bb6c8aeba5686b19966027df2..2c429bab38594f4109c467a89e62106d1cc60d6b 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -59,6 +59,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
fallbackSorts = Map.empty
mapSorts = Map.empty
+ arraySorts = Map.empty
funSorts = Map.empty
funDomainConstructors = Map.empty
funDomainSelectors = Map.empty
@@ -98,6 +99,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
+ private var unitSort: Z3Sort = null
+ private var unitValue: Z3AST = null
+
protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
@@ -106,6 +110,14 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
protected[leon] var tupleConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
protected[leon] var tupleSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+ private var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var arrayTupleCons: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorArray: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorLength: Map[TypeTree, Z3FuncDecl] = Map.empty
+
+ private var reverseTupleConstructors: Map[Z3FuncDecl, TupleType] = Map.empty
+ private var reverseTupleSelectors: Map[Z3FuncDecl, (TupleType, Int)] = Map.empty
+
private var intSetMinFun: Z3FuncDecl = null
private var intSetMaxFun: Z3FuncDecl = null
private var setCardFuns: Map[TypeTree, Z3FuncDecl] = Map.empty
@@ -189,6 +201,27 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
setSorts = Map.empty
setCardFuns = Map.empty
+ //unitSort = z3.mkUninterpretedSort("unit")
+ //unitValue = z3.mkFreshConst("Unit", unitSort)
+ //val bound = z3.mkBound(0, unitSort)
+ //val eq = z3.mkEq(bound, unitValue)
+ //val decls = Seq((z3.mkFreshStringSymbol("u"), unitSort))
+ //val unitAxiom = z3.mkForAll(0, Seq(), decls, eq)
+ //println(unitAxiom)
+ //println(unitValue)
+ //z3.assertCnstr(unitAxiom)
+ val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
+ Seq(
+ (
+ "Unit",
+ Seq("Unit"),
+ Seq(Seq())
+ )
+ )
+ )
+ unitSort = us
+ unitValue = unitCons()
+
val intSetSort = typeToSort(SetType(Int32Type))
intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort)
intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort)
@@ -358,6 +391,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
def typeToSort(tt: TypeTree): Z3Sort = tt match {
case Int32Type => intSort
case BooleanType => boolSort
+ case UnitType => unitSort
case AbstractClassType(cd) => adtSorts(cd)
case CaseClassType(cd) => {
if (cd.hasParent) {
@@ -386,6 +420,21 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
ms
}
}
+ case at @ ArrayType(base) => arraySorts.get(at) match {
+ case Some(s) => s
+ case None => {
+ val intSort = typeToSort(Int32Type)
+ val toSort = typeToSort(base)
+ val as = z3.mkArraySort(intSort, toSort)
+ val tupleSortSymbol = z3.mkFreshStringSymbol("Array")
+ val (arrayTupleSort, arrayTupleCons_, Seq(arrayTupleSelectorArray_, arrayTupleSelectorLength_)) = z3.mkTupleSort(tupleSortSymbol, as, intSort)
+ arraySorts += (at -> arrayTupleSort)
+ arrayTupleCons += (at -> arrayTupleCons_)
+ arrayTupleSelectorArray += (at -> arrayTupleSelectorArray_)
+ arrayTupleSelectorLength += (at -> arrayTupleSelectorLength_)
+ arrayTupleSort
+ }
+ }
case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
case Some(s) => s
case None => {
@@ -403,11 +452,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Some(s) => s
case None => {
val tpesSorts = tpes.map(typeToSort)
- val sortSymbol = z3.mkFreshStringSymbol("TupleSort")
+ val sortSymbol = z3.mkFreshStringSymbol("Tuple")
val (tupleSort, consTuple, projsTuple) = z3.mkTupleSort(sortSymbol, tpesSorts: _*)
tupleSorts += (tt -> tupleSort)
tupleConstructors += (tt -> consTuple)
+ reverseTupleConstructors += (consTuple -> tt)
tupleSelectors += (tt -> projsTuple)
+ projsTuple.zipWithIndex.foreach{ case (proj, i) => reverseTupleSelectors += (proj -> (tt, i)) }
tupleSort
}
}
@@ -513,14 +564,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
- //for(clause <- clauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
- //}
+ for(clause <- clauses) {
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
+ }
- //println("The blocking guards: " + guards)
val cc = toZ3Formula(z3, And(clauses)).get
- // println("CC : " + cc)
z3.assertCnstr(cc)
// these are the optional sequence of assumption literals
@@ -561,6 +609,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(a, m, Seq.empty[Z3AST])
}
reporter.info(" - Finished search with blocked literals")
+ Logger.debug("The blocking guards are: " + blockingSet.mkString(", "), 4, "z3solver")
// if (Settings.useCores)
// reporter.info(" - Core is : " + core)
@@ -582,10 +631,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
case (Some(true), m) => { // SAT
validatingStopwatch.start
+ Logger.debug("Model Found: " + m, 4, "z3solver")
val (trueModel, model) = if(Settings.verifyModel)
validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
- else
- (true, modelToMap(m, varsInVC))
+ else {
+ val res = (true, modelToMap(m, varsInVC))
+ lazy val modelAsString = res._2.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
+ reporter.info("- Found a model:")
+ reporter.info(modelAsString)
+ res
+ }
validatingStopwatch.stop
if (trueModel) {
@@ -632,6 +687,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
foundAnswer(Some(true))
} else {
luckyStopwatch.start
+ Logger.debug("Model Found: " + m2, 4, "z3solver")
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
@@ -722,7 +778,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
- // println("Release set : " + toRelease)
blockingSet = blockingSet -- toRelease
@@ -735,16 +790,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - more unrollings")
for((id,polarity) <- toReleaseAsPairs) {
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
- //println("Unlocked : " + (id, !polarity))
for(clause <- newClauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
}
for(ncl <- newClauses) {
z3.assertCnstr(toZ3Formula(z3, ncl).get)
}
- //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
reporter.info(" - finished unrolling")
@@ -912,6 +964,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
z3Vars = z3Vars - i
rb
}
+ case Waypoint(_, e) => rec(e)
case e @ Error(_) => {
val tpe = e.getType
val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
@@ -960,6 +1013,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, intSort)
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
+ case UnitLiteral => unitValue
case Equals(l, r) => z3.mkEq(rec(l), rec(r))
case Plus(l, r) => if(USEBV) z3.mkBVAdd(rec(l), rec(r)) else z3.mkAdd(rec(l), rec(r))
case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
@@ -1043,6 +1097,38 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case MapType(ft, tt) => z3.mkDistinct(z3.mkSelect(rec(m), rec(k)), mapRangeNoneConstructors(tt)())
case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
}
+ case fill@ArrayFill(length, default) => {
+ val at@ArrayType(base) = fill.getType
+ typeToSort(at)
+ val cons = arrayTupleCons(at)
+ val ar = z3.mkConstArray(typeToSort(base), rec(default))
+ val res = cons(ar, rec(length))
+ res
+ }
+ case ArraySelect(a, index) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val res = z3.mkSelect(getArray(ar), rec(index))
+ res
+ }
+ case ArrayUpdated(a, index, newVal) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val cons = arrayTupleCons(a.getType)
+ val store = z3.mkStore(getArray(ar), rec(index), rec(newVal))
+ val res = cons(store, getLength(ar))
+ res
+ }
+ case ArrayLength(a) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val res = getLength(ar)
+ res
+ }
case AnonymousFunctionInvocation(id, args) => id.getType match {
case ft @ FunctionType(fts, tt) => {
val consFD = funDomainConstructors(ft)
@@ -1100,8 +1186,28 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
}
}
+ case Some(ArrayType(dt)) => {
+ val Z3AppAST(decl, args) = z3.getASTKind(t)
+ assert(args.size == 2)
+ val IntLiteral(length) = rec(args(1), Some(Int32Type))
+ val array = model.getArrayValue(args(0)) match {
+ case None => throw new CantTranslateException(t)
+ case Some((map, elseValue)) => {
+ val exprs = map.foldLeft((1 to length).map(_ => rec(elseValue, Some(dt))).toSeq)((acc, p) => {
+ val IntLiteral(index) = rec(p._1, Some(Int32Type))
+ if(index >= 0 && index < length)
+ acc.updated(index, rec(p._2, Some(dt)))
+ else acc
+ })
+ FiniteArray(exprs)
+ }
+ }
+ array
+ }
case other =>
- z3.getASTKind(t) match {
+ if(t == unitValue)
+ UnitLiteral
+ else z3.getASTKind(t) match {
case Z3AppAST(decl, args) => {
val argsSize = args.size
if(argsSize == 0 && z3IdToExpr.isDefinedAt(t)) {
@@ -1121,6 +1227,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
val ccd = reverseADTConstructors(decl)
assert(argsSize == ccd.fields.size)
CaseClass(ccd, (args zip ccd.fields).map(p => rec(p._1, Some(p._2.tpe))))
+ } else if(reverseTupleConstructors.isDefinedAt(decl)) {
+ val TupleType(subTypes) = reverseTupleConstructors(decl)
+ val rargs = args.zip(subTypes).map(p => rec(p._1, Some(p._2)))
+ Tuple(rargs)
} else {
import Z3DeclKind._
val rargs = args.map(rec(_))
@@ -1134,7 +1244,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
val r1 = rargs(1)
val r2 = rargs(2)
try {
- IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType))
+ IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType).get)
} catch {
case e => {
println("I was asking for lub because of this.")
@@ -1194,6 +1304,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
case Z3NumeralAST(Some(v)) => IntLiteral(v)
+ case Z3NumeralAST(None) => {
+ reporter.info("Cannot read exact model from Z3: Integer does not fit in machine word")
+ reporter.info("Exiting procedure now")
+ sys.exit(0)
+ }
case other @ _ => {
System.err.println("Don't know what this is " + other)
System.err.println("REVERSE FUNCTION MAP:")
@@ -1252,16 +1367,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
// Wouldn't it be better/more uniform to pretend the initial formula is a
// function and generate a template for it?
def initialUnrolling(formula : Expr) : (Seq[Expr], Seq[(Identifier,Boolean)]) = {
- val fi = functionCallsOf(formula)
- if(fi.isEmpty) {
- (Seq(formula), Seq.empty)
- } else {
- val startingVar : Identifier = FreshIdentifier("start", true).setType(BooleanType)
-
- val result = treatFunctionInvocationSet(startingVar, true, functionCallsOf(formula))
- //reporter.info(result)
- (Variable(startingVar) +: formula +: result._1, result._2)
- }
+ initialUnrolling0(formula)
}
def unlock(id: Identifier, pol: Boolean) : (Seq[Expr], Seq[(Identifier,Boolean)]) = {
@@ -1273,6 +1379,82 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
treatFunctionInvocationSet(id, pol, copy)
}
}
+
+ //this is mostly copied from FunctionTemplate. This is sort of a quick hack to the problem
+ //of the initial unrolling
+ def initialUnrolling0(formula: Expr): (Seq[Expr], Seq[(Identifier,Boolean)]) = {
+
+ var guardedExprs : Map[(Identifier,Boolean),Seq[Expr]] = Map.empty
+ def storeGuarded(guardVar : Identifier, guardPol : Boolean, expr : Expr) : Unit = {
+ assert(expr.getType == BooleanType)
+ val p : (Identifier,Boolean) = (guardVar,guardPol)
+ if(guardedExprs.isDefinedAt(p)) {
+ val prev : Seq[Expr] = guardedExprs(p)
+ guardedExprs += (p -> (expr +: prev))
+ } else {
+ guardedExprs += (p -> Seq(expr))
+ }
+ }
+
+ def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
+ expr match {
+ case l : Let => sys.error("Let's should have been eliminated.")
+ case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
+
+ case i @ IfExpr(cond, then, elze) => {
+ if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
+ i
+ } else {
+ val newBool : Identifier = FreshIdentifier("b", true).setType(BooleanType)
+ val newExpr : Identifier = FreshIdentifier("e", true).setType(i.getType)
+
+ val crec = rec(pathVar, pathPol, cond)
+ val trec = rec(newBool, true, then)
+ val erec = rec(newBool, false, elze)
+
+ storeGuarded(pathVar, pathPol, Iff(Variable(newBool), crec))
+ storeGuarded(newBool, true, Equals(Variable(newExpr), trec))
+ storeGuarded(newBool, false, Equals(Variable(newExpr), erec))
+ Variable(newExpr)
+ }
+ }
+
+ case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, pathPol, a))).setType(n.getType)
+ case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, pathPol, a1), rec(pathVar, pathPol, a2)).setType(b.getType)
+ case u @ UnaryOperator(a, r) => r(rec(pathVar, pathPol, a)).setType(u.getType)
+ case t : Terminal => t
+ case a : AnonymousFunction => {
+ Settings.reporter.warning("AnonymousFunction literal showed up in the construction of a FunctionTemplate.")
+ a
+ }
+ }
+ }
+ val startingVar : Identifier = FreshIdentifier("start", true).setType(BooleanType)
+ storeGuarded(startingVar, false, BooleanLiteral(false))
+ val newFormula = rec(startingVar, true, formula)
+ storeGuarded(startingVar, true, newFormula)
+
+ val asClauses : Seq[Expr] = {
+ (for(((b,p),es) <- guardedExprs; e <- es) yield {
+ Implies(if(!p) Not(Variable(b)) else Variable(b), e)
+ }).toSeq
+ }
+
+ val blockers : Map[(Identifier,Boolean),Set[FunctionInvocation]] = {
+ Map((for((p, es) <- guardedExprs) yield {
+ val calls = es.foldLeft(Set.empty[FunctionInvocation])((s,e) => s ++ functionCallsOf(e))
+ if(calls.isEmpty) {
+ None
+ } else {
+ registerBlocked(p._1, p._2, calls)
+ Some((p, calls))
+ }
+ }).flatten.toSeq : _*)
+ }
+
+ (asClauses, blockers.keys.toSeq)
+
+ }
}
}
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index d9426510ee76f9703514df4219cff8761db26995..8a6fd5bffd1a7c6a9a6a9b6fdde5e8bd3598f940 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -9,121 +9,153 @@ object FunctionClosure extends Pass {
val description = "Closing function with its scoping variables"
- private var enclosingPreconditions: List[Expr] = Nil
-
private var pathConstraints: List[Expr] = Nil
+ private var enclosingLets: List[(Identifier, Expr)] = Nil
private var newFunDefs: Map[FunDef, FunDef] = Map()
+ private var topLevelFuns: Set[FunDef] = Set()
def apply(program: Program): Program = {
newFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
- enclosingPreconditions = fd.precondition.toList
pathConstraints = fd.precondition.toList
- fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet))
- fd.postcondition = fd.postcondition.map(b => functionClosure(b, fd.args.map(_.id).toSet))
+ fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
- program
+ val Program(id, ObjectDef(objId, defs, invariants)) = program
+ Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
}
- private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
+ private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
case l @ LetDef(fd, rest) => {
-
- val id = fd.id
- val rt = fd.returnType
- val varDecl = fd.args
- val precondition = fd.precondition
- val postcondition = fd.postcondition
-
- val bodyVars: Set[Identifier] = variablesOf(fd.body.getOrElse(BooleanLiteral(true))) ++
- variablesOf(precondition.getOrElse(BooleanLiteral(true))) ++
- variablesOf(postcondition.getOrElse(BooleanLiteral(true)))
-
- val capturedVars = bodyVars.intersect(bindedVars)// this should be the variable used that are in the scope
- val (constraints, allCapturedVars) = filterConstraints(capturedVars) //all relevant path constraints
- val capturedVarsWithConstraints = allCapturedVars.toSeq
-
- val freshVars: Map[Identifier, Identifier] = capturedVarsWithConstraints.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
- val freshVarsExpr: Map[Expr, Expr] = freshVars.map(p => (p._1.toVariable, p._2.toVariable))
-
- val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
- val newVarDecls = varDecl ++ extraVarDecls
- val newFunId = FreshIdentifier(id.name)
- val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
+ val capturedVars: Set[Identifier] = bindedVars.diff(enclosingLets.map(_._1).toSet)
+ val capturedConstraints: Set[Expr] = pathConstraints.toSet
+
+ val freshIds: Map[Identifier, Identifier] = capturedVars.map(id => (id, FreshIdentifier(id.name).setType(id.getType))).toMap
+ val freshVars: Map[Expr, Expr] = freshIds.map(p => (p._1.toVariable, p._2.toVariable))
+
+ val extraVarDeclOldIds: Seq[Identifier] = capturedVars.toSeq
+ val extraVarDeclFreshIds: Seq[Identifier] = extraVarDeclOldIds.map(freshIds(_))
+ val extraVarDecls: Seq[VarDecl] = extraVarDeclFreshIds.map(id => VarDecl(id, id.getType))
+ val newVarDecls: Seq[VarDecl] = fd.args ++ extraVarDecls
+ val newBindedVars: Set[Identifier] = bindedVars ++ fd.args.map(_.id)
+ val newFunId = FreshIdentifier(fd.id.name)
+
+ val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
+ topLevelFuns += newFunDef
newFunDef.fromLoop = fd.fromLoop
newFunDef.parent = fd.parent
newFunDef.addAnnotation(fd.annotations.toSeq:_*)
- val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
- val freshPostcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
- val freshBody = fd.body.map(b => replace(freshVarsExpr, b))
- val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
-
- def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
- case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)).setPosInfo(fi))
- case _ => None
+ def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
+ val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
+ val newId = FreshIdentifier(p._1.name).setType(p._1.getType)
+ val newMap = acc._2 + (p._1 -> newId)
+ val newBody = functionClosure(acc._1, newBindedVars, freshIds ++ newMap, fd2FreshFd)
+ (Let(newId, p._2, newBody), newMap)
+ })
+ functionClosure(newExpr, newBindedVars, freshIds, fd2FreshFd)
}
- val oldPathConstraints = pathConstraints
- pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
- val recPrecondition = freshConstraints match { //Actually, we do not allow nested fundef in precondition
- case List() => freshPrecondition
- case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
- }
- val recBody = freshBody.map(b =>
- functionClosure(b, bindedVars ++ newVarDecls.map(_.id))
- ).map(b => searchAndReplaceDFS(substFunInvocInDef)(b))
- pathConstraints = oldPathConstraints
- newFunDef.precondition = recPrecondition
- newFunDef.body = recBody
+
+ val newPrecondition = simplifyLets(introduceLets(And((capturedConstraints ++ fd.precondition).toSeq), fd2FreshFd))
+ newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
+
+ val freshPostcondition = fd.postcondition.map(post => introduceLets(post, fd2FreshFd))
newFunDef.postcondition = freshPostcondition
+
+ pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
+ //val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable))))))
+ val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable))))))
+ newFunDef.body = freshBody
+ pathConstraints = pathConstraints.tail
- def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
- case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
- case _ => None
- }
- val recRest = searchAndReplaceDFS(substFunInvocInRest)(functionClosure(rest, bindedVars))
- LetDef(newFunDef, recRest).setType(l.getType)
+ //val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd ->
+ // ((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable)))))
+ val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable)))))
+ freshRest.setType(l.getType)
}
case l @ Let(i,e,b) => {
- val re = functionClosure(e, bindedVars)
- pathConstraints ::= Equals(Variable(i), re)
- val rb = functionClosure(b, bindedVars + i)
- pathConstraints = pathConstraints.tail
+ val re = functionClosure(e, bindedVars, id2freshId, fd2FreshFd)
+ //we need the enclosing lets to always refer to the original ids, because it might be expand later in a highly nested function
+ enclosingLets ::= (i, replace(id2freshId.map(p => (p._2.toVariable, p._1.toVariable)), re))
+ //pathConstraints :: Equals(i.toVariable, re)
+ val rb = functionClosure(b, bindedVars + i, id2freshId, fd2FreshFd)
+ enclosingLets = enclosingLets.tail
+ //pathConstraints = pathConstraints.tail
Let(i, re, rb).setType(l.getType)
}
+ case i @ IfExpr(cond,then,elze) => {
+ /*
+ when acumulating path constraints, take the condition without closing it first, so this
+ might not work well with nested fundef in if then else condition
+ */
+ val rCond = functionClosure(cond, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints ::= cond//rCond
+ val rThen = functionClosure(then, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ pathConstraints ::= Not(cond)//Not(rCond)
+ val rElze = functionClosure(elze, bindedVars, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ IfExpr(rCond, rThen, rElze).setType(i.getType)
+ }
+ case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match {
+ case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi)
+ case Some((nfd, extraArgs)) =>
+ FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++
+ extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).setPosInfo(fi)
+ }
case n @ NAryOperator(args, recons) => {
- var change = false
- val rargs = args.map(a => functionClosure(a, bindedVars))
+ val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd))
recons(rargs).setType(n.getType)
}
case b @ BinaryOperator(t1,t2,recons) => {
- val r1 = functionClosure(t1, bindedVars)
- val r2 = functionClosure(t2, bindedVars)
+ val r1 = functionClosure(t1, bindedVars, id2freshId, fd2FreshFd)
+ val r2 = functionClosure(t2, bindedVars, id2freshId, fd2FreshFd)
recons(r1,r2).setType(b.getType)
}
case u @ UnaryOperator(t,recons) => {
- val r = functionClosure(t, bindedVars)
+ val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd)
recons(r).setType(u.getType)
}
- case i @ IfExpr(cond,then,elze) => {
- val rCond = functionClosure(cond, bindedVars)
- pathConstraints ::= rCond
- val rThen = functionClosure(then, bindedVars)
- pathConstraints = pathConstraints.tail
- pathConstraints ::= Not(rCond)
- val rElze = functionClosure(elze, bindedVars)
- pathConstraints = pathConstraints.tail
- IfExpr(rCond, rThen, rElze).setType(i.getType)
+ case m @ MatchExpr(scrut,cses) => {
+ val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => {
+ val binders = pat.binders
+ val cond = conditionForPattern(scrut, pat)
+ pathConstraints ::= cond
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ SimpleCase(pat, rRhs)
+ }
+ case GuardedCase(pat, guard, rhs) => {
+ val binders = pat.binders
+ val cond = conditionForPattern(scrut, pat)
+ pathConstraints ::= cond
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ val rGuard = functionClosure(guard, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ pathConstraints = pathConstraints.tail
+ GuardedCase(pat, rGuard, rRhs)
+ }
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
}
- case m @ MatchExpr(scrut,cses) => { //TODO: will not work if there are actual nested function in cases
- //val rScrut = functionClosure(scrut, bindedVars)
- m
+ case v @ Variable(id) => id2freshId.get(id) match {
+ case None => v
+ case Some(nid) => Variable(nid)
}
case t if t.isInstanceOf[Terminal] => t
case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionClosure: " + unhandled)
}
+ def freshIdInPat(pat: Pattern, id2freshId: Map[Identifier, Identifier]): Pattern = pat match {
+ case InstanceOfPattern(binder, classTypeDef) => InstanceOfPattern(binder.map(id2freshId(_)), classTypeDef)
+ case WildcardPattern(binder) => WildcardPattern(binder.map(id2freshId(_)))
+ case CaseClassPattern(binder, caseClassDef, subPatterns) => CaseClassPattern(binder.map(id2freshId(_)), caseClassDef, subPatterns.map(freshIdInPat(_, id2freshId)))
+ case TuplePattern(binder, subPatterns) => TuplePattern(binder.map(id2freshId(_)), subPatterns.map(freshIdInPat(_, id2freshId)))
+ }
+
//filter the list of constraints, only keeping those relevant to the set of variables
def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
var allVars = vars
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index eb139f824166e44feda604bd36976689a3ae7541..d3cd29907c5cd8c30fb574d06ddd1682e5bfa59a 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -15,11 +15,9 @@ object ImperativeCodeElimination extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
- Logger.debug("Transforming to functional code the following function:\n" + fd, 5, "imperative")
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
- Logger.debug("Resulting functional code is:\n" + fd, 5, "imperative")
}))
pgm
}
@@ -52,8 +50,10 @@ object ImperativeCodeElimination extends Pass {
val (tRes, tScope, tFun) = toFunction(tExpr)
val (eRes, eScope, eFun) = toFunction(eExpr)
+ val iteRType = leastUpperBound(tRes.getType, eRes.getType).get
+
val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varInScope).toSeq
- val resId = FreshIdentifier("res").setType(ite.getType)
+ val resId = FreshIdentifier("res").setType(iteRType)
val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
val iteType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
@@ -76,7 +76,7 @@ object ImperativeCodeElimination extends Pass {
if(freshIds.isEmpty)
Let(resId, tupleId.toVariable, body)
else
- Let(resId, TupleSelect(tupleId.toVariable, 1),
+ Let(resId, TupleSelect(tupleId.toVariable, 1).setType(iteRType),
freshIds.zipWithIndex.foldLeft(body)((b, id) =>
Let(id._1,
TupleSelect(tupleId.toVariable, id._2 + 2).setType(id._1.getType),
@@ -225,8 +225,13 @@ object ImperativeCodeElimination extends Pass {
}
case LetDef(fd, b) => {
//Recall that here the nested function should not access mutable variables from an outside scope
+ val newFd = if(!fd.hasImplementation) fd else {
+ val (fdRes, fdScope, fdFun) = toFunction(fd.getBody)
+ fd.body = Some(fdScope(fdRes))
+ fd
+ }
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
- (bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)), bodyFun)
+ (bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)), bodyFun)
}
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index e9818f16debfb19ccdbeaec6f1212f169918990f..9af1b41e731e32ff4b25942c4ec4f6ac63f91b0a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -32,8 +32,9 @@ object Main {
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
Logger.debug("Default action on program: " + program, 3, "main")
- val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
+ val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
val program2 = passManager.run(program)
+ assert(program2.isPure)
val analysis = new Analysis(program2, reporter)
analysis.analyse
}
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index bebd985778beeda1a7995ebb9917712aa7403e25..307a227ffb0ce0decb39624b1dde34bc6a589a39 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -8,6 +8,7 @@ class PassManager(passes: Seq[Pass]) {
passes.foldLeft(program)((pgm, pass) => {
Logger.debug("Running Pass: " + pass.description, 1, "passman")
val newPgm = pass(pgm)
+ TypeChecking(newPgm)
Logger.debug("Resulting program: " + newPgm, 3, "passman")
newPgm
})
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index 5562c75db5965e7d5f5916aa8923da065b1e3bb6..d52d6fe0d380b90424c239f3d302fb3620d502c4 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -12,9 +12,11 @@ object Simplificator extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => fd.body.map(body => {
- fd.body = Some(simplifyLets(body))
- }))
+ allFuns.foreach(fd => {
+ fd.body = fd.body.map(simplifyLets)
+ fd.precondition = fd.precondition.map(simplifyLets)
+ fd.postcondition = fd.postcondition.map(simplifyLets)
+ })
pgm
}
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f6d4b259f19ab5e19e462cd4ba137d39bba16917
--- /dev/null
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -0,0 +1,120 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object TypeChecking extends Pass {
+
+ val description = "Type check the AST"
+
+ def apply(pgm: Program): Program = {
+ val allFuns = pgm.definedFunctions
+
+ allFuns.foreach(fd => {
+ fd.precondition.foreach(typeCheck)
+ fd.postcondition.foreach(typeCheck)
+ fd.body.foreach(typeCheck)
+ })
+
+ pgm
+ }
+
+ private def typeCheck(expr: Expr): Unit = { //expr match {
+ //quick hack
+ //searchAndReplaceDFS(e => {
+ // if(e.getType == Untyped) {
+ // println("Expression is untyped: " + e)
+ // }
+ // None
+ //})(expr)
+
+ //case l@Let(i, v, b) => {
+ // if(l.getType == Untyp
+ // val vr = transform(v)
+ // v.getType match {
+ // case ArrayType(_) => {
+ // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
+ // id2id += (i -> freshIdentifier)
+ // val br = transform(b)
+ // LetVar(freshIdentifier, vr, br)
+ // }
+ // case _ => {
+ // val br = transform(b)
+ // Let(i, vr, br)
+ // }
+ // }
+ //}
+ //case LetVar(id, e, b) => {
+ // val er = transform(e)
+ // val br = transform(b)
+ // LetVar(id, er, br)
+ //}
+ //case wh@While(c, e) => {
+ // val newWh = While(transform(c), transform(e))
+ // newWh.invariant = wh.invariant.map(i => transform(i))
+ // newWh.setPosInfo(wh)
+ //}
+
+ //case ite@IfExpr(c, t, e) => {
+ // val rc = transform(c)
+ // val rt = transform(t)
+ // val re = transform(e)
+ // IfExpr(rc, rt, re).setType(rt.getType)
+ //}
+
+ //case m @ MatchExpr(scrut, cses) => {
+ // val scrutRec = transform(scrut)
+ // val csesRec = cses.map{
+ // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ // }
+ // val tpe = csesRec.head.rhs.getType
+ // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ //}
+ //case LetDef(fd, b) => {
+ // val newFd = if(fd.hasImplementation) {
+ // val body = fd.body.get
+ // val args = fd.args
+ // val newFd =
+ // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
+ // val newArgs = args.map(vd => {
+ // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
+ // id2id += (vd.id -> freshId)
+ // val newTpe = transform(vd.tpe)
+ // VarDecl(freshId, newTpe)
+ // })
+ // val freshFunName = FreshIdentifier(fd.id.name)
+ // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
+ // fd2fd += (fd -> freshFunDef)
+ // freshFunDef.fromLoop = fd.fromLoop
+ // freshFunDef.parent = fd.parent
+ // freshFunDef.precondition = fd.precondition.map(transform)
+ // freshFunDef.postcondition = fd.postcondition.map(transform)
+ // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ // freshFunDef
+ // } else fd
+ // val newBody = transform(body)
+ // newFd.body = Some(newBody)
+ // newFd
+ // } else fd
+ // val rb = transform(b)
+ // LetDef(newFd, rb)
+ //}
+ //case FunctionInvocation(fd, args) => {
+ // val rargs = args.map(transform)
+ // val rfd = fd2fd.get(fd).getOrElse(fd)
+ // FunctionInvocation(rfd, rargs)
+ //}
+
+ //case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
+ //case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
+ //case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
+
+ //case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
+ //case (t: Terminal) => t
+ //case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
+ }
+
+}
diff --git a/src/main/scala/leon/Utils.scala b/src/main/scala/leon/Utils.scala
index ae60002b693a0b74657fa8640a7eef56a641703f..15006c7bc0820fae25274411ac4c5f5c9ef6a70f 100644
--- a/src/main/scala/leon/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -16,4 +16,7 @@ object Utils {
def invariant(x: Boolean): Unit = ()
}
implicit def while2Invariant(u: Unit) = InvariantFunction
+
+
+ def waypoint[A](i: Int, expr: A): A = expr
}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 01545bc3e87bd3606591b464f59098a5b0d8dd8c..e5556f1acf52fa3f8472556bcc66d3572c032488 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,6 +49,7 @@ object VCKind extends Enumeration {
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
val MapAccess = Value("map acc.")
+ val ArrayAccess = Value("arr. acc.")
val InvariantInit = Value("inv init.")
val InvariantInd = Value("inv ind.")
val InvariantPost = Value("inv post.")
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b64d6cb05d58ad1dd0420d27f21cfd0b3955b2bd..1ff95e4c922d08cf0b400c2049dc0d8139da6380 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -17,6 +17,7 @@ trait CodeExtraction extends Extractors {
import StructuralExtractors._
import ExpressionExtractors._
+
private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
private lazy val multisetTraitSym = try {
@@ -28,6 +29,10 @@ trait CodeExtraction extends Extractors {
private lazy val someClassSym = definitions.getClass("scala.Some")
private lazy val function1TraitSym = definitions.getClass("scala.Function1")
+ private lazy val arraySym = definitions.getClass("scala.Array")
+
+ def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
+
def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
@@ -198,6 +203,7 @@ trait CodeExtraction extends Extractors {
a.atp.safeToString match {
case "leon.Annotations.induct" => funDef.addAnnotation("induct")
case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ case "leon.Annotations.main" => funDef.addAnnotation("main")
case _ => ;
}
}
@@ -245,6 +251,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)
})
@@ -255,6 +262,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) => {
@@ -285,15 +294,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
@@ -335,6 +352,13 @@ trait CodeExtraction extends Extractors {
}
}
+
+ private var currentFunDef: FunDef = null
+
+ //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
* errors. */
@@ -400,6 +424,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)
})
@@ -411,6 +436,8 @@ trait CodeExtraction extends Extractors {
var reqCont: Option[Expr] = None
var ensCont: Option[Expr] = None
+ currentFunDef = funDef
+
realBody match {
case ExEnsuredExpression(body2, resSym, contract) => {
varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
@@ -440,15 +467,22 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
- reqCont.map(e =>
+ bodyAttempt.foreach(e =>
+ 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.map(e =>
+ 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
@@ -465,429 +499,530 @@ trait CodeExtraction extends Extractors {
case _ => (tr, None)
}
- var handleRest = true
- val psExpr = nextExpr match {
- case ExTuple(tpes, exprs) => {
- val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
- val tupleExprs = exprs.map(e => rec(e))
- Tuple(tupleExprs).setType(tupleType)
- }
- case ExTupleExtract(tuple, index) => {
- val tupleExpr = rec(tuple)
- val TupleType(tpes) = tupleExpr.getType
- if(tpes.size < index)
- throw ImpureCodeEncounteredException(tree)
- else
- TupleSelect(tupleExpr, index).setType(tpes(index-1))
- }
- case ExValDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
- }
- handleRest = false
- val res = Let(newID, valTree, restTree)
- res
- }
- case dd@ExFunctionDef(n, p, t, b) => {
- 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
- mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
- val funDefWithBody = extractFunDef(funDef, b)
- mutableVarSubsts ++= oldMutableVarSubst
- val restTree = rest match {
- case Some(rst) => rec(rst)
- case None => UnitLiteral
- }
- defsToDefs.remove(dd.symbol)
- handleRest = false
- LetDef(funDefWithBody, restTree)
- }
- case ExVarDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- mutableVarSubsts += (vs -> (() => Variable(newID)))
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
- }
- handleRest = false
- val res = LetVar(newID, valTree, restTree)
- res
+ val e2: Option[Expr] = nextExpr match {
+ case ExParameterlessMethodCall(t,n) => {
+ val selector = rec(t)
+ val selType = selector.getType
+
+ if(!selType.isInstanceOf[CaseClassType])
+ None
+ else {
+
+ val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+
+ val fieldID = selDef.fields.find(_.id.name == n.toString) match {
+ case None => {
+ if(!silent)
+ unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ case Some(vd) => vd.id
+ }
+
+ Some(CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType))
+ }
}
+ case _ => None
+ }
+ var handleRest = true
+ val psExpr = e2 match {
+ case Some(e3) => e3
+ case None => nextExpr match {
+ case ExTuple(tpes, exprs) => {
+ val tupleExprs = exprs.map(e => rec(e))
+ val tupleType = TupleType(tupleExprs.map(expr => bestRealType(expr.getType)))
+ Tuple(tupleExprs).setType(tupleType)
+ }
+ case ExTupleExtract(tuple, index) => {
+ val tupleExpr = rec(tuple)
+ val TupleType(tpes) = tupleExpr.getType
+ if(tpes.size < index)
+ throw ImpureCodeEncounteredException(tree)
+ else
+ TupleSelect(tupleExpr, index).setType(tpes(index-1))
+ }
+ case ExValDef(vs, tpt, bdy) => {
+ 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))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
+ }
+ val res = Let(newID, valTree, restTree)
+ res
+ }
+ case dd@ExFunctionDef(n, p, t, b) => {
+ 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
+ }
+ defsToDefs.remove(dd.symbol)
+ handleRest = false
+ LetDef(funDefWithBody, restTree)
+ }
+ 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 _ =>
+ //}
+ 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))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
+ }
+ val res = LetVar(newID, valTree, restTree)
+ res
+ }
- case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
- case Some(fun) => {
- val Variable(id) = fun()
- val rhsTree = rec(rhs)
- Assignment(id, rhsTree)
+ case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
+ 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 => {
+ unit.error(tr.pos, "Undeclared variable.")
+ throw ImpureCodeEncounteredException(tr)
+ }
}
- case None => {
- unit.error(tr.pos, "Undeclared variable.")
- throw ImpureCodeEncounteredException(tr)
+ case wh@ExWhile(cond, body) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ }
+ case wh@ExWhileWithInvariant(cond, body, inv) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ val invTree = rec(inv)
+ val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ w.invariant = Some(invTree)
+ w
}
- }
- case wh@ExWhile(cond, body) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- }
- case wh@ExWhileWithInvariant(cond, body, inv) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- val invTree = rec(inv)
- val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- w.invariant = Some(invTree)
- w
- }
- case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
- case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
- case ExUnitLiteral() => UnitLiteral
+ case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
+ case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
+ case ExUnitLiteral() => UnitLiteral
- case ExTyped(e,tpt) => rec(e)
- case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
- case Some(fun) => fun()
- case None => mutableVarSubsts.get(sym) match {
+ case ExTyped(e,tpt) => rec(e)
+ case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
case Some(fun) => fun()
- case None => {
- unit.error(tr.pos, "Unidentified variable.")
- throw ImpureCodeEncounteredException(tr)
+ case None => mutableVarSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => {
+ unit.error(tr.pos, "Unidentified variable.")
+ throw ImpureCodeEncounteredException(tr)
+ }
}
}
- }
- case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
- val pstpe = scalaType2PureScala(unit, silent)(tpe)
- val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
- varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
- val c1 = rec(predBody)
- previousVarSubst match {
- case Some(f) => varSubsts(varSym) = f
- case None => varSubsts.remove(varSym)
- }
- if(containsEpsilon(c1)) {
- unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
- throw ImpureCodeEncounteredException(epsi)
- }
- Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
- }
- case ExSomeConstruction(tpe, arg) => {
- // println("Got Some !" + tpe + ":" + arg)
- val underlying = scalaType2PureScala(unit, silent)(tpe)
- OptionSome(rec(arg)).setType(OptionType(underlying))
- }
- case ExCaseClassConstruction(tpt, args) => {
- val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
- if(!cctype.isInstanceOf[CaseClassType]) {
- if(!silent) {
- unit.error(tr.pos, "Construction of a non-case class.")
+ case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
+ val pstpe = scalaType2PureScala(unit, silent)(tpe)
+ val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
+ varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+ val c1 = rec(predBody)
+ previousVarSubst match {
+ case Some(f) => varSubsts(varSym) = f
+ case None => varSubsts.remove(varSym)
}
- throw ImpureCodeEncounteredException(tree)
+ if(containsEpsilon(c1)) {
+ unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
+ throw ImpureCodeEncounteredException(epsi)
+ }
+ Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
}
- val nargs = args.map(rec(_))
- val cct = cctype.asInstanceOf[CaseClassType]
- CaseClass(cct.classDef, nargs).setType(cct)
- }
- case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
- case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
- case ExNot(e) => Not(rec(e)).setType(BooleanType)
- case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
- case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
- case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
- case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
- case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
- case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
- case ExEquals(l, r) => {
- val rl = rec(l)
- val rr = rec(r)
- ((rl.getType,rr.getType) match {
- case (SetType(_), SetType(_)) => SetEquals(rl, rr)
- case (BooleanType, BooleanType) => Iff(rl, rr)
- case (_, _) => Equals(rl, rr)
- }).setType(BooleanType)
- }
- case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
- case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
- case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
- case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
- case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
- case ExFiniteSet(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteSet(args.map(rec(_))).setType(SetType(underlying))
- }
- case ExFiniteMultiset(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
- }
- case ExEmptySet(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptySet(underlying).setType(SetType(underlying))
- }
- case ExEmptyMultiset(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMultiset(underlying).setType(MultisetType(underlying))
- }
- case ExEmptyMap(ft, tt) => {
- val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
- val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
- }
- case ExSetMin(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Min should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+ case ExWaypointExpression(tpe, i, tree) => {
+ val pstpe = scalaType2PureScala(unit, silent)(tpe)
+ val IntLiteral(ri) = rec(i)
+ Waypoint(ri, rec(tree)).setType(pstpe)
}
- SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExSetMax(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Max should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSomeConstruction(tpe, arg) => {
+ // println("Got Some !" + tpe + ":" + arg)
+ val underlying = scalaType2PureScala(unit, silent)(tpe)
+ OptionSome(rec(arg)).setType(OptionType(underlying))
}
- SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExUnion(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetUnion(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ case ExCaseClassConstruction(tpt, args) => {
+ val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
+ if(!cctype.isInstanceOf[CaseClassType]) {
+ if(!silent) {
+ unit.error(tr.pos, "Construction of a non-case class.")
+ }
throw ImpureCodeEncounteredException(tree)
}
+ val nargs = args.map(rec(_))
+ val cct = cctype.asInstanceOf[CaseClassType]
+ CaseClass(cct.classDef, nargs).setType(cct)
}
- }
- case ExIntersection(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
+ case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
+ case ExNot(e) => Not(rec(e)).setType(BooleanType)
+ case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
+ case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
+ case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
+ case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
+ case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
+ case ExEquals(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ ((rl.getType,rr.getType) match {
+ case (SetType(_), SetType(_)) => SetEquals(rl, rr)
+ case (BooleanType, BooleanType) => Iff(rl, rr)
+ case (_, _) => Equals(rl, rr)
+ }).setType(BooleanType)
+ }
+ case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
+ case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
+ case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
+ case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExFiniteSet(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteSet(args.map(rec(_))).setType(SetType(underlying))
+ }
+ case ExFiniteMultiset(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
+ }
+ case ExEmptySet(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptySet(underlying).setType(SetType(underlying))
+ }
+ case ExEmptyMultiset(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMultiset(underlying).setType(MultisetType(underlying))
+ }
+ case ExEmptyMap(ft, tt) => {
+ val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
+ val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
+ }
+ case ExSetMin(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Min should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
}
- }
- case ExSetContains(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => ElementOfSet(rr, rl)
- case _ => {
- if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ case ExSetMax(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Max should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
}
- }
- case ExSetSubset(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SubsetOf(rl, rr)
- case _ => {
- if(!silent) unit.error(tree.pos, "Subset on non set expression.")
- throw ImpureCodeEncounteredException(tree)
+ case ExUnion(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetUnion(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetMinus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetDifference(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExIntersection(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetCard(t) => {
- val rt = rec(t)
- rt.getType match {
- case s @ SetType(_) => SetCardinality(rt)
- case m @ MultisetType(_) => MultisetCardinality(rt)
- case _ => {
- if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetContains(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => ElementOfSet(rr, rl)
+ case _ => {
+ if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMultisetToSet(t) => {
- val rt = rec(t)
- rt.getType match {
- case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
- case _ => {
- if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetSubset(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SubsetOf(rl, rr)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Subset on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapUpdated(m,f,t) => {
- val rm = rec(m)
- val rf = rec(f)
- val rt = rec(t)
- val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
- rm.getType match {
- case MapType(ft, tt) =>
- MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
- case _ => {
- if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetMinus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetDifference(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case ExSetCard(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case s @ SetType(_) => SetCardinality(rt)
+ case m @ MultisetType(_) => MultisetCardinality(rt)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapIsDefinedAt(m,k) => {
- val rm = rec(m)
- val rk = rec(k)
- MapIsDefinedAt(rm, rk)
- }
-
- case ExPlusPlusPlus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- MultisetPlus(rl, rr).setType(rl.getType)
- }
- case app@ExApply(lhs,args) => {
- val rlhs = rec(lhs)
- val rargs = args map rec
- rlhs.getType match {
- case MapType(_,tt) =>
- assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
- case FunctionType(fts, tt) => {
- rlhs match {
- case Variable(id) =>
- AnonymousFunctionInvocation(id, rargs).setType(tt)
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
- throw ImpureCodeEncounteredException(tree)
- }
+ case ExMultisetToSet(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
+ case _ => {
+ if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
+ throw ImpureCodeEncounteredException(tree)
}
}
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on unexpected type")
- throw ImpureCodeEncounteredException(tree)
+ }
+ case up@ExUpdated(m,f,t) => {
+ val rm = rec(m)
+ val rf = rec(f)
+ val rt = rec(t)
+ rm.getType match {
+ case MapType(ft, tt) => {
+ val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
+ MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
+ }
+ case ArrayType(bt) => {
+ ArrayUpdated(rm, rf, rt).setType(rm.getType).setPosInfo(up.pos.line, up.pos.column)
+ }
+ case _ => {
+ if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExIfThenElse(t1,t2,t3) => {
- val r1 = rec(t1)
- val r2 = rec(t2)
- val r3 = rec(t3)
- IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
- }
-
- case ExIsInstanceOf(tt, cc) => {
- val ccRec = rec(cc)
- val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
- checkType match {
- case CaseClassType(ccd) => {
- val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
- if(!ccRec.getType.isInstanceOf[ClassType]) {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
- throw ImpureCodeEncounteredException(tr)
- } else {
- val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
- val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+ case ExMapIsDefinedAt(m,k) => {
+ val rm = rec(m)
+ val rk = rec(k)
+ MapIsDefinedAt(rm, rk)
+ }
- if(rootType != testedExprRootType) {
- unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
- throw ImpureCodeEncounteredException(tr)
- } else {
- CaseClassInstanceOf(ccd, ccRec)
+ case ExPlusPlusPlus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ MultisetPlus(rl, rr).setType(rl.getType)
+ }
+ case app@ExApply(lhs,args) => {
+ val rlhs = rec(lhs)
+ val rargs = args map rec
+ rlhs.getType match {
+ case MapType(_,tt) =>
+ assert(rargs.size == 1)
+ MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
+ case FunctionType(fts, tt) => {
+ rlhs match {
+ case Variable(id) =>
+ AnonymousFunctionInvocation(id, rargs).setType(tt)
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
+ case ArrayType(bt) => {
+ assert(rargs.size == 1)
+ ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
+ }
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on unexpected type")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
- case _ => {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
- throw ImpureCodeEncounteredException(tr)
+ }
+ // for now update only occurs on Array. later we might have to distinguished depending on the type of the lhs
+ case update@ExUpdate(lhs, index, newValue) => {
+ val lhsRec = rec(lhs)
+ lhsRec match {
+ case Variable(_) =>
+ case _ => {
+ unit.error(tree.pos, "array update only works on variables")
+ 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)
}
- }
-
- case lc @ ExLocalCall(sy,nm,ar) => {
- if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
- if(!silent)
- unit.error(tr.pos, "Invoking an invalid function.")
- throw ImpureCodeEncounteredException(tr)
+ case ExArrayLength(t) => {
+ val rt = rec(t)
+ ArrayLength(rt)
}
- val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
- }
- case pm @ ExPatternMatching(sel, cses) => {
- val rs = rec(sel)
- val rc = cses.map(rewriteCaseDef(_))
- val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
- MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
- }
-
- // this one should stay after all others, cause it also catches UMinus
- // and Not, for instance.
- case ExParameterlessMethodCall(t,n) => {
- val selector = rec(t)
- val selType = selector.getType
-
- if(!selType.isInstanceOf[CaseClassType]) {
- if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not purescala?)")
- throw ImpureCodeEncounteredException(tr)
+ 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)
+ val defaultValueRec = rec(defaultValue)
+ ArrayFill(lengthRec, defaultValueRec).setType(ArrayType(underlying))
+ }
+ case ExIfThenElse(t1,t2,t3) => {
+ val r1 = rec(t1)
+ if(containsLetDef(r1)) {
+ unit.error(t1.pos, "Condition of if-then-else expression should not contain nested function definition")
+ throw ImpureCodeEncounteredException(t1)
+ }
+ val r2 = rec(t2)
+ val r3 = rec(t3)
+ val lub = leastUpperBound(r2.getType, r3.getType)
+ lub match {
+ case Some(lub) => IfExpr(r1, r2, r3).setType(lub)
+ case None =>
+ unit.error(nextExpr.pos, "Both branches of ifthenelse have incompatible types")
+ throw ImpureCodeEncounteredException(t1)
+ }
}
- val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+ case ExIsInstanceOf(tt, cc) => {
+ val ccRec = rec(cc)
+ val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
+ checkType match {
+ case CaseClassType(ccd) => {
+ val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
+ if(!ccRec.getType.isInstanceOf[ClassType]) {
+ unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
+ val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+
+ if(rootType != testedExprRootType) {
+ unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ CaseClassInstanceOf(ccd, ccRec)
+ }
+ }
+ }
+ case _ => {
+ unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ }
+ }
- val fieldID = selDef.fields.find(_.id.name == n.toString) match {
- case None => {
+ case lc @ ExLocalCall(sy,nm,ar) => {
+ if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ unit.error(tr.pos, "Invoking an invalid function.")
throw ImpureCodeEncounteredException(tr)
}
- case Some(vd) => vd.id
+ val fd = defsToDefs(sy)
+ FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
+ }
+ case pm @ ExPatternMatching(sel, cses) => {
+ val rs = rec(sel)
+ val rc = cses.map(rewriteCaseDef(_))
+ val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
+ MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
}
- CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType)
- }
-
- // default behaviour is to complain :)
- case _ => {
- if(!silent) {
- println(tr)
- reporter.info(tr.pos, "Could not extract as PureScala.", true)
+
+ // default behaviour is to complain :)
+ case _ => {
+ if(!silent) {
+ println(tr)
+ reporter.info(tr.pos, "Could not extract as PureScala.", true)
+ }
+ throw ImpureCodeEncounteredException(tree)
}
- throw ImpureCodeEncounteredException(tree)
}
}
- 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)
}
@@ -897,6 +1032,7 @@ trait CodeExtraction extends Extractors {
def rec(tr: Type): purescala.TypeTrees.TypeTree = tr match {
case tpe if tpe == IntClass.tpe => Int32Type
case tpe if tpe == BooleanClass.tpe => BooleanType
+ case tpe if tpe == UnitClass.tpe => UnitType
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
@@ -906,6 +1042,7 @@ trait CodeExtraction extends Extractors {
case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4)))
case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4),rec(t5)))
case TypeRef(_, sym, ftt :: ttt :: Nil) if isFunction1TraitSym(sym) => FunctionType(List(rec(ftt)), rec(ttt))
+ case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) => ArrayType(rec(btt))
case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
if(!silent) {
@@ -928,4 +1065,31 @@ 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 MatchExpr(_, cses) => cses.flatMap{
+ case SimpleCase(_, rhs) => getReturnedExpr(rhs)
+ case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
+ }
+ 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 04cece3d96670c4723fc09e13f0deaf2bf62dd09..eae46482780a0362946b5ddacce1eae632ffc1e9 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -174,6 +174,19 @@ trait Extractors {
case _ => None
}
}
+ object ExWaypointExpression {
+ def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
+ case Apply(
+ TypeApply(Select(Select(funcheckIdent, utilsName), waypoint), typeTree :: Nil),
+ List(i, expr)) => {
+ if (utilsName.toString == "Utils" && waypoint.toString == "waypoint")
+ Some((typeTree.tpe, i, expr))
+ else
+ None
+ }
+ case _ => None
+ }
+ }
object ExValDef {
@@ -632,10 +645,13 @@ trait Extractors {
}
}
- object ExMapUpdated {
+ object ExUpdated {
def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match {
case Apply(TypeApply(Select(lhs, n), typeTreeList), List(from, to)) if (n.toString == "updated") =>
Some((lhs, from, to))
+ case Apply(
+ Apply(TypeApply(Select(Apply(_, Seq(lhs)), n), _), Seq(index, value)),
+ List(Apply(_, _))) if (n.toString == "updated") => Some((lhs, index, value))
case _ => None
}
}
@@ -646,6 +662,14 @@ trait Extractors {
case _ => None
}
}
+ object ExUpdate {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Select(lhs, update),
+ index :: newValue :: Nil) if(update.toString == "update") => Some((lhs, index, newValue))
+ case _ => None
+ }
+ }
object ExMapIsDefinedAt {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
@@ -653,5 +677,42 @@ trait Extractors {
case _ => None
}
}
+
+ object ExArrayLength {
+ def unapply(tree: Select): Option[Tree] = tree match {
+ case Select(t, n) if (n.toString == "length") => Some(t)
+ case _ => None
+ }
+ }
+
+ object ExArrayClone {
+ def unapply(tree: Apply): Option[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 {
+ case Apply(
+ Apply(
+ Apply(
+ TypeApply(
+ Select(Select(Ident(scala), arrayObject), fillMethod),
+ baseType :: Nil
+ ),
+ length :: Nil
+ ),
+ defaultValue :: Nil
+ ),
+ manifest
+ ) if(scala.toString == "scala" &&
+ arrayObject.toString == "Array" &&
+ fillMethod.toString == "fill") => Some((baseType, length, defaultValue))
+ case _ => None
+ }
+ }
+
}
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f2da8a7cef1f1f3b0290a35a260f40ceefbf6705..3c18e858fcfeba8fa7d02421536e1080c5999847 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -53,6 +53,16 @@ object Definitions {
def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
def caseClassDef(name: String) = mainObject.caseClassDef(name)
def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id
+ def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure))
+
+ def writeScalaFile(filename: String) {
+ import java.io.FileWriter
+ import java.io.BufferedWriter
+ val fstream = new FileWriter(filename)
+ val out = new BufferedWriter(fstream)
+ out.write(ScalaPrinter(this))
+ out.close
+ }
}
/** Objects work as containers for class definitions, functions (def's) and
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index d1a39f7172fafb612c2201b2c4322615a0aabdef..b7b5bd343c2adc3bf973440776951a124a0ddd08 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -139,8 +139,8 @@ object PrettyPrinter {
sb.append("\n")
}
- case Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
- case TupleSelect(t, i) => {
+ case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
+ case s@TupleSelect(t, i) => {
pp(t, sb, lvl)
sb.append("._" + i)
sb
@@ -154,6 +154,12 @@ object PrettyPrinter {
nsb
}
+ case Waypoint(i, expr) => {
+ sb.append("waypoint_" + i + "(")
+ pp(expr, sb, lvl)
+ sb.append(")")
+ }
+
case OptionSome(a) => {
var nsb = sb
nsb.append("Some(")
@@ -249,6 +255,50 @@ object PrettyPrinter {
nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
nsb
}
+ case ArrayLength(a) => {
+ 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)
+ sb.append(")(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case am@ArrayMake(v) => {
+ sb.append("Array.make(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case sel@ArraySelect(ar, i) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(")")
+ }
+ case up@ArrayUpdate(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(") = ")
+ pp(v, sb, lvl)
+ }
+ case up@ArrayUpdated(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append(".updated(")
+ pp(i, sb, lvl)
+ sb.append(", ")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case FiniteArray(exprs) => {
+ ppNary(sb, exprs, "Array(", ", ", ")", lvl)
+ }
case Distinct(exprs) => {
var nsb = sb
@@ -377,6 +427,7 @@ object PrettyPrinter {
case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
+ case ArrayType(bt) => pp(bt, sb.append("Array["), lvl).append("]")
case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..501096c45db7c82d88c441e53a6564065423944d
--- /dev/null
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -0,0 +1,563 @@
+package leon.purescala
+
+/** This pretty-printer only print valid scala syntax */
+object ScalaPrinter {
+ import Common._
+ import Trees._
+ import TypeTrees._
+ import Definitions._
+
+ import java.lang.StringBuffer
+
+ def apply(tree: Expr): String = {
+ val retSB = pp(tree, new StringBuffer, 0)
+ retSB.toString
+ }
+
+ def apply(tpe: TypeTree): String = {
+ val retSB = pp(tpe, new StringBuffer, 0)
+ retSB.toString
+ }
+
+ def apply(defn: Definition): String = {
+ val retSB = pp(defn, new StringBuffer, 0)
+ retSB.toString
+ }
+
+ private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
+ sb.append(" " * lvl)
+ sb
+ }
+
+ // EXPRESSIONS
+ // all expressions are printed in-line
+ private def ppUnary(sb: StringBuffer, expr: Expr, op1: String, op2: String, lvl: Int): StringBuffer = {
+ var nsb: StringBuffer = sb
+ nsb.append(op1)
+ nsb = pp(expr, nsb, lvl)
+ nsb.append(op2)
+ nsb
+ }
+
+ private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String, lvl: Int): StringBuffer = {
+ var nsb: StringBuffer = sb
+ nsb.append("(")
+ nsb = pp(left, nsb, lvl)
+ nsb.append(op)
+ nsb = pp(right, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
+
+ private def ppNary(sb: StringBuffer, exprs: Seq[Expr], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
+ var nsb = sb
+ nsb.append(pre)
+ val sz = exprs.size
+ var c = 0
+
+ exprs.foreach(ex => {
+ nsb = pp(ex, nsb, lvl) ; c += 1 ; if(c < sz) nsb.append(op)
+ })
+
+ nsb.append(post)
+ nsb
+ }
+
+ private def pp(tree: Expr, sb: StringBuffer, lvl: Int): StringBuffer = tree match {
+ case Variable(id) => sb.append(id)
+ case DeBruijnIndex(idx) => sys.error("Not Valid Scala")
+ case Let(b,d,e) => {
+ sb.append("locally {\n")
+ ind(sb, lvl+1)
+ sb.append("val " + b + " = ")
+ pp(d, sb, lvl+1)
+ sb.append("\n")
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("}\n")
+ ind(sb, lvl)
+ sb
+ }
+ case LetVar(b,d,e) => {
+ sb.append("locally {\n")
+ ind(sb, lvl+1)
+ sb.append("var " + b + " = ")
+ pp(d, sb, lvl+1)
+ sb.append("\n")
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("}\n")
+ ind(sb, lvl)
+ sb
+ }
+ case LetDef(fd,e) => {
+ sb.append("\n")
+ pp(fd, sb, lvl+1)
+ sb.append("\n")
+ sb.append("\n")
+ ind(sb, lvl)
+ pp(e, sb, lvl)
+ sb
+ }
+ case And(exprs) => ppNary(sb, exprs, "(", " && ", ")", lvl) // \land
+ case Or(exprs) => ppNary(sb, exprs, "(", " || ", ")", lvl) // \lor
+ case Not(Equals(l, r)) => ppBinary(sb, l, r, " != ", lvl) // \neq
+ case Iff(l,r) => sys.error("Not Scala Code")
+ case Implies(l,r) => sys.error("Not Scala Code")
+ case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
+ case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
+ case IntLiteral(v) => sb.append(v)
+ case BooleanLiteral(v) => sb.append(v)
+ case StringLiteral(s) => sb.append("\"" + s + "\"")
+ case UnitLiteral => sb.append("()")
+ case Block(exprs, last) => {
+ sb.append("{\n")
+ (exprs :+ last).foreach(e => {
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append("\n")
+ })
+ ind(sb, lvl)
+ sb.append("}\n")
+ sb
+ }
+ case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
+ case wh@While(cond, body) => {
+ wh.invariant match {
+ case Some(inv) => {
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("@invariant: ")
+ pp(inv, sb, lvl)
+ sb.append("\n")
+ ind(sb, lvl)
+ }
+ case None =>
+ }
+ sb.append("while(")
+ pp(cond, sb, lvl)
+ sb.append(")\n")
+ ind(sb, lvl+1)
+ pp(body, sb, lvl+1)
+ sb.append("\n")
+ }
+
+ case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
+ case s@TupleSelect(t, i) => {
+ pp(t, sb, lvl)
+ sb.append("._" + i)
+ sb
+ }
+
+ case e@Epsilon(pred) => sys.error("Not Scala Code")
+ case Waypoint(i, expr) => pp(expr, sb, lvl)
+
+ case OptionSome(a) => {
+ var nsb = sb
+ nsb.append("Some(")
+ nsb = pp(a, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
+
+ case OptionNone(_) => sb.append("None")
+
+ case CaseClass(cd, args) => {
+ var nsb = sb
+ nsb.append(cd.id)
+ nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
+ nsb
+ }
+ case CaseClassInstanceOf(cd, e) => {
+ var nsb = sb
+ nsb = pp(e, nsb, lvl)
+ nsb.append(".isInstanceOf[" + cd.id + "]")
+ nsb
+ }
+ case CaseClassSelector(_, cc, id) => pp(cc, sb, lvl).append("." + id)
+ case FunctionInvocation(fd, args) => {
+ var nsb = sb
+ nsb.append(fd.id)
+ nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
+ nsb
+ }
+ case AnonymousFunction(es, ev) => {
+ var nsb = sb
+ nsb.append("{")
+ es.foreach {
+ case (as, res) =>
+ nsb = ppNary(nsb, as, "", " ", "", lvl)
+ nsb.append(" -> ")
+ nsb = pp(res, nsb, lvl)
+ nsb.append(", ")
+ }
+ nsb.append("else -> ")
+ nsb = pp(ev, nsb, lvl)
+ nsb.append("}")
+ }
+ case AnonymousFunctionInvocation(id, args) => {
+ var nsb = sb
+ nsb.append(id)
+ nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
+ nsb
+ }
+ case Plus(l,r) => ppBinary(sb, l, r, " + ", lvl)
+ case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
+ case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
+ case Division(l,r) => ppBinary(sb, l, r, " / ", lvl)
+ case Modulo(l,r) => ppBinary(sb, l, r, " % ", lvl)
+ case LessThan(l,r) => ppBinary(sb, l, r, " < ", lvl)
+ case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
+ case LessEquals(l,r) => ppBinary(sb, l, r, " <= ", lvl) // \leq
+ case GreaterEquals(l,r) => ppBinary(sb, l, r, " >= ", lvl) // \geq
+ case FiniteSet(rs) => ppNary(sb, rs, "{", ", ", "}", lvl)
+ case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
+ case EmptySet(bt) => sb.append("Set()") // Ø
+ case EmptyMultiset(_) => sys.error("Not Valid Scala")
+ case Not(ElementOfSet(s,e)) => sys.error("TODO")
+ //case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
+ //case SubsetOf(l,r) => ppBinary(sb, l, r, " \u2286 ", lvl) // \subseteq
+ //case Not(SubsetOf(l,r)) => ppBinary(sb, l, r, " \u2288 ", lvl) // \notsubseteq
+ case SetMin(s) => pp(s, sb, lvl).append(".min")
+ case SetMax(s) => pp(s, sb, lvl).append(".max")
+ // case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
+ // case MultisetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
+ // case MapUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
+ // case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
+ // case MultisetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
+ // case SetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
+ // case MultisetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
+ // case SetCardinality(t) => ppUnary(sb, t, "|", "|", lvl)
+ // case MultisetCardinality(t) => ppUnary(sb, t, "|", "|", lvl)
+ // case MultisetPlus(l,r) => ppBinary(sb, l, r, " \u228E ", lvl) // U+
+ // case MultisetToSet(e) => pp(e, sb, lvl).append(".toSet")
+ case EmptyMap(_,_) => sb.append("Map()")
+ case SingletonMap(f,t) => ppBinary(sb, f, t, " -> ", lvl)
+ case FiniteMap(rs) => ppNary(sb, rs, "Map(", ", ", ")", lvl)
+ case MapGet(m,k) => {
+ var nsb = sb
+ pp(m, nsb, lvl)
+ nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
+ nsb
+ }
+ case MapIsDefinedAt(m,k) => {
+ var nsb = sb
+ pp(m, nsb, lvl)
+ nsb.append(".isDefinedAt")
+ nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
+ nsb
+ }
+ case ArrayLength(a) => {
+ 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)
+ sb.append(")(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case am@ArrayMake(v) => sys.error("Not Scala Code")
+ case sel@ArraySelect(ar, i) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(")")
+ }
+ case up@ArrayUpdate(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(") = ")
+ pp(v, sb, lvl)
+ }
+ case up@ArrayUpdated(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append(".updated(")
+ pp(i, sb, lvl)
+ sb.append(", ")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case FiniteArray(exprs) => {
+ ppNary(sb, exprs, "Array(", ", ", ")", lvl)
+ }
+
+ case Distinct(exprs) => {
+ var nsb = sb
+ nsb.append("distinct")
+ nsb = ppNary(nsb, exprs, "(", ", ", ")", lvl)
+ nsb
+ }
+
+ case IfExpr(c, t, e) => {
+ var nsb = sb
+ nsb.append("(if (")
+ nsb = pp(c, nsb, lvl)
+ nsb.append(")\n")
+ ind(nsb, lvl+1)
+ nsb = pp(t, nsb, lvl+1)
+ nsb.append("\n")
+ ind(nsb, lvl)
+ nsb.append("else\n")
+ ind(nsb, lvl+1)
+ nsb = pp(e, nsb, lvl+1)
+ nsb.append(")")
+ nsb
+ }
+
+ case mex @ MatchExpr(s, csc) => {
+ def ppc(sb: StringBuffer, p: Pattern): StringBuffer = p match {
+ //case InstanceOfPattern(None, ctd) =>
+ //case InstanceOfPattern(Some(id), ctd) =>
+ case CaseClassPattern(bndr, ccd, subps) => {
+ var nsb = sb
+ bndr.foreach(b => nsb.append(b + " @ "))
+ nsb.append(ccd.id).append("(")
+ var c = 0
+ val sz = subps.size
+ subps.foreach(sp => {
+ nsb = ppc(nsb, sp)
+ if(c < sz - 1)
+ nsb.append(", ")
+ c = c + 1
+ })
+ nsb.append(")")
+ }
+ case WildcardPattern(None) => sb.append("_")
+ case WildcardPattern(Some(id)) => sb.append(id)
+ case TuplePattern(bndr, subPatterns) => {
+ bndr.foreach(b => sb.append(b + " @ "))
+ sb.append("(")
+ subPatterns.init.foreach(p => {
+ ppc(sb, p)
+ sb.append(", ")
+ })
+ ppc(sb, subPatterns.last)
+ sb.append(")")
+ }
+ case _ => sb.append("Pattern?")
+ }
+
+ var nsb = sb
+ nsb.append("(")
+ nsb == pp(s, nsb, lvl)
+ // if(mex.posInfo != "") {
+ // nsb.append(" match@(" + mex.posInfo + ") {\n")
+ // } else {
+ nsb.append(" match {\n")
+ // }
+
+ csc.foreach(cs => {
+ ind(nsb, lvl+1)
+ nsb.append("case ")
+ nsb = ppc(nsb, cs.pattern)
+ cs.theGuard.foreach(g => {
+ nsb.append(" if ")
+ nsb = pp(g, nsb, lvl+1)
+ })
+ nsb.append(" => ")
+ nsb = pp(cs.rhs, nsb, lvl+1)
+ nsb.append("\n")
+ })
+ ind(nsb, lvl).append("}")
+ nsb.append(")")
+ nsb
+ }
+
+ case ResultVariable() => sb.append("res")
+ case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
+ case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
+
+ case e @ Error(desc) => {
+ var nsb = sb
+ nsb.append("error(\"" + desc + "\")[")
+ nsb = pp(e.getType, nsb, lvl)
+ nsb.append("]")
+ nsb
+ }
+
+ case _ => sb.append("Expr?")
+ }
+
+ // TYPE TREES
+ // all type trees are printed in-line
+ private def ppNaryType(sb: StringBuffer, tpes: Seq[TypeTree], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
+ var nsb = sb
+ nsb.append(pre)
+ val sz = tpes.size
+ var c = 0
+
+ tpes.foreach(t => {
+ nsb = pp(t, nsb, lvl) ; c += 1 ; if(c < sz) nsb.append(op)
+ })
+
+ nsb.append(post)
+ nsb
+ }
+
+ private def pp(tpe: TypeTree, sb: StringBuffer, lvl: Int): StringBuffer = tpe match {
+ case Untyped => sb.append("???")
+ case UnitType => sb.append("Unit")
+ case Int32Type => sb.append("Int")
+ case BooleanType => sb.append("Boolean")
+ case ArrayType(bt) => pp(bt, sb.append("Array["), lvl).append("]")
+ case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
+ case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
+ case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
+ case OptionType(bt) => pp(bt, sb.append("Option["), lvl).append("]")
+ case FunctionType(fts, tt) => {
+ var nsb = sb
+ if (fts.size > 1)
+ nsb = ppNaryType(nsb, fts, "(", ", ", ")", lvl)
+ else if (fts.size == 1)
+ nsb = pp(fts.head, nsb, lvl)
+ nsb.append(" => ")
+ pp(tt, nsb, lvl)
+ }
+ case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
+ case c: ClassType => sb.append(c.classDef.id)
+ case _ => sb.append("Type?")
+ }
+
+ // DEFINITIONS
+ // all definitions are printed with an end-of-line
+ private def pp(defn: Definition, sb: StringBuffer, lvl: Int): StringBuffer = {
+
+ defn match {
+ case Program(id, mainObj) => {
+ assert(lvl == 0)
+ pp(mainObj, sb, lvl)
+ }
+
+ case ObjectDef(id, defs, invs) => {
+ var nsb = sb
+ ind(nsb, lvl)
+ nsb.append("object ")
+ nsb.append(id)
+ nsb.append(" {\n")
+
+ var c = 0
+ val sz = defs.size
+
+ defs.foreach(df => {
+ nsb = pp(df, nsb, lvl+1)
+ if(c < sz - 1) {
+ nsb.append("\n\n")
+ }
+ c = c + 1
+ })
+
+ nsb.append("\n")
+ ind(nsb, lvl).append("}\n")
+ }
+
+ case AbstractClassDef(id, parent) => {
+ var nsb = sb
+ ind(nsb, lvl)
+ nsb.append("sealed abstract class ")
+ nsb.append(id)
+ parent.foreach(p => nsb.append(" extends " + p.id))
+ nsb
+ }
+
+ case CaseClassDef(id, parent, varDecls) => {
+ var nsb = sb
+ ind(nsb, lvl)
+ nsb.append("case class ")
+ nsb.append(id)
+ nsb.append("(")
+ var c = 0
+ val sz = varDecls.size
+
+ varDecls.foreach(vd => {
+ nsb.append(vd.id)
+ nsb.append(": ")
+ nsb = pp(vd.tpe, nsb, lvl)
+ if(c < sz - 1) {
+ nsb.append(", ")
+ }
+ c = c + 1
+ })
+ nsb.append(")")
+ parent.foreach(p => nsb.append(" extends " + p.id))
+ nsb
+ }
+
+ case fd @ FunDef(id, rt, args, body, pre, post) => {
+ var nsb = sb
+
+ //for(a <- fd.annotations) {
+ // ind(nsb, lvl)
+ // nsb.append("@" + a + "\n")
+ //}
+
+ ind(nsb, lvl)
+ nsb.append("def ")
+ nsb.append(id)
+ nsb.append("(")
+
+ val sz = args.size
+ var c = 0
+
+ args.foreach(arg => {
+ nsb.append(arg.id)
+ nsb.append(" : ")
+ nsb = pp(arg.tpe, nsb, lvl)
+
+ if(c < sz - 1) {
+ nsb.append(", ")
+ }
+ c = c + 1
+ })
+
+ nsb.append(") : ")
+ nsb = pp(rt, nsb, lvl)
+ nsb.append(" = (")
+ if(body.isDefined) {
+ pre match {
+ case None => pp(body.get, nsb, lvl)
+ case Some(prec) => {
+ nsb.append("{\n")
+ ind(nsb, lvl+1)
+ nsb.append("require(")
+ nsb = pp(prec, nsb, lvl+1)
+ nsb.append(")\n")
+ pp(body.get, nsb, lvl+1)
+ nsb.append("\n")
+ ind(nsb, lvl)
+ nsb.append("}")
+ }
+ }
+ } else
+ nsb.append("[unknown function implementation]")
+
+ post match {
+ case None => {
+ nsb.append(")")
+ }
+ case Some(postc) => {
+ nsb.append(" ensuring(res => ") //TODO, not very general solution...
+ nsb = pp(postc, nsb, lvl)
+ nsb.append("))")
+ }
+ }
+
+ nsb
+ }
+
+ case _ => sb.append("Defn?")
+ }
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 638db0c2024152c46b9f735263b11e9ce01b5ca2..bfad43aae71ffb22c33c09cf8667d7920acca9ab 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -76,9 +76,17 @@ object Trees {
}
case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
- case class Tuple(exprs: Seq[Expr]) extends Expr
+ case class Tuple(exprs: Seq[Expr]) extends Expr {
+ val subTpes = exprs.map(_.getType).map(bestRealType)
+ if(!subTpes.exists(_ == Untyped)) {
+ setType(TupleType(subTpes))
+ }
+
+ }
case class TupleSelect(tuple: Expr, index: Int) extends Expr
+ case class Waypoint(i: Int, expr: Expr) extends Expr
+
object MatchExpr {
def apply(scrutinee: Expr, cases: Seq[MatchCase]) : MatchExpr = {
scrutinee.getType match {
@@ -148,6 +156,7 @@ object Trees {
case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern
+
/* Propositional logic */
object And {
def apply(l: Expr, r: Expr) : Expr = (l,r) match {
@@ -379,6 +388,25 @@ object Trees {
val fixedType = BooleanType
}
+ /* Array operations */
+ case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr
+ case class ArrayMake(defaultValue: Expr) extends Expr
+ case class ArraySelect(array: Expr, index: Expr) extends Expr with ScalacPositional
+ //the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the function variant
+ //ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is keep all the way to the backend
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType {
+ val fixedType = UnitType
+ }
+ case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional
+ case class ArrayLength(array: Expr) extends Expr with FixedType {
+ 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
case class Cons(head: Expr, tail: Expr) extends Expr
@@ -411,6 +439,10 @@ object Trees {
case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
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 Waypoint(i, t) => Some((t, (expr: Expr) => Waypoint(i, expr)))
case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
}
@@ -446,6 +478,8 @@ object Trees {
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
+ case ArrayFill(t1, t2) => Some((t1, t2, ArrayFill))
+ case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh)))
@@ -463,6 +497,9 @@ object Trees {
case FiniteSet(args) => Some((args, FiniteSet))
case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
case FiniteMultiset(args) => Some((args, FiniteMultiset))
+ case ArrayUpdate(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
+ case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))))
+ case FiniteArray(args) => Some((args, FiniteArray))
case Distinct(args) => Some((args, Distinct))
case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
case Tuple(args) => Some((args, Tuple))
@@ -598,7 +635,7 @@ object Trees {
case Some(newEx) => {
somethingChanged = true
if(newEx.getType == Untyped) {
- Settings.reporter.warning("REPLACING WITH AN UNTYPED EXPRESSION !")
+ Settings.reporter.warning("REPLACING [" + ex + "] WITH AN UNTYPED EXPRESSION !")
Settings.reporter.warning("Here's the new expression: " + newEx)
}
newEx
@@ -798,13 +835,19 @@ object Trees {
searchAndReplaceDFS(applyToTree)(expr)
}
- //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks
+ //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while, blocks, array, ...
+ //this is expected to be true when entering the "backend" of Leon
def isPure(expr: Expr): Boolean = {
def convert(t: Expr) : Boolean = t match {
case Block(_, _) => false
case Assignment(_, _) => false
case While(_, _) => false
case LetVar(_, _, _) => false
+ case LetDef(_, _) => false
+ case ArrayUpdate(_, _, _) => false
+ case ArrayMake(_) => false
+ case ArrayClone(_) => false
+ case Epsilon(_) => false
case _ => true
}
def combine(b1: Boolean, b2: Boolean) = b1 && b2
@@ -813,6 +856,11 @@ object Trees {
case Assignment(_, _) => false
case While(_, _) => false
case LetVar(_, _, _) => false
+ case LetDef(_, _) => false
+ case ArrayUpdate(_, _, _) => false
+ case ArrayMake(_) => false
+ case ArrayClone(_) => false
+ case Epsilon(_) => false
case _ => b
}
treeCatamorphism(convert, combine, compute, expr)
@@ -842,6 +890,18 @@ object Trees {
}
treeCatamorphism(convert, combine, compute, expr)
}
+ def containsIfExpr(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (i: IfExpr) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (i: IfExpr) => true
+ case _ => c
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
def variablesOf(expr: Expr) : Set[Identifier] = {
def convert(t: Expr) : Set[Identifier] = t match {
@@ -1229,6 +1289,24 @@ object Trees {
toRet
}
+ def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
+ case WildcardPattern(_) => BooleanLiteral(true)
+ case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
+ case CaseClassPattern(_, ccd, subps) => {
+ assert(ccd.fields.size == subps.size)
+ val pairs = ccd.fields.map(_.id).toList zip subps.toList
+ val subTests = pairs.map(p => conditionForPattern(CaseClassSelector(ccd, in, p._1), p._2))
+ val together = And(subTests)
+ And(CaseClassInstanceOf(ccd, in), together)
+ }
+ case TuplePattern(_, subps) => {
+ val TupleType(tpes) = in.getType
+ assert(tpes.size == subps.size)
+ val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+ And(subTests)
+ }
+ }
+
private def convertMatchToIfThenElse(expr: Expr) : Expr = {
def mapForPattern(in: Expr, pattern: Pattern) : Map[Identifier,Expr] = pattern match {
case WildcardPattern(None) => Map.empty
@@ -1258,24 +1336,6 @@ object Trees {
}
}
- def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
- case WildcardPattern(_) => BooleanLiteral(true)
- case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
- case CaseClassPattern(_, ccd, subps) => {
- assert(ccd.fields.size == subps.size)
- val pairs = ccd.fields.map(_.id).toList zip subps.toList
- val subTests = pairs.map(p => conditionForPattern(CaseClassSelector(ccd, in, p._1), p._2))
- val together = And(subTests)
- And(CaseClassInstanceOf(ccd, in), together)
- }
- case TuplePattern(_, subps) => {
- val TupleType(tpes) = in.getType
- assert(tpes.size == subps.size)
- val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
- And(subTests)
- }
- }
-
def rewritePM(e: Expr) : Option[Expr] = e match {
case m @ MatchExpr(scrut, cases) => {
// println("Rewriting the following PM: " + e)
@@ -1406,4 +1466,34 @@ object Trees {
case FunctionType(fromTypes, toType) => AnonymousFunction(Seq.empty, simplestValue(toType)).setType(tpe)
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
}
+
+ //guarentee that all IfExpr will be at the top level and as soon as you encounter a non-IfExpr, then no more IfExpr can be find in the sub-expressions
+ //require no-match, no-ets and only pure code
+ def hoistIte(expr: Expr): Expr = {
+ def transform(expr: Expr): Option[Expr] = expr match {
+ case uop@UnaryOperator(IfExpr(c, t, e), op) => Some(IfExpr(c, op(t).setType(uop.getType), op(e).setType(uop.getType)).setType(uop.getType))
+ case bop@BinaryOperator(IfExpr(c, t, e), t2, op) => Some(IfExpr(c, op(t, t2).setType(bop.getType), op(e, t2).setType(bop.getType)).setType(bop.getType))
+ case bop@BinaryOperator(t1, IfExpr(c, t, e), op) => Some(IfExpr(c, op(t1, t).setType(bop.getType), op(t1, e).setType(bop.getType)).setType(bop.getType))
+ case nop@NAryOperator(ts, op) => {
+ val iteIndex = ts.indexWhere{ case IfExpr(_, _, _) => true case _ => false }
+ if(iteIndex == -1) None else {
+ val (beforeIte, startIte) = ts.splitAt(iteIndex)
+ val afterIte = startIte.tail
+ val IfExpr(c, t, e) = startIte.head
+ Some(IfExpr(c,
+ op(beforeIte ++ Seq(t) ++ afterIte).setType(nop.getType),
+ op(beforeIte ++ Seq(e) ++ afterIte).setType(nop.getType)
+ ).setType(nop.getType))
+ }
+ }
+ case _ => None
+ }
+
+ def fix[A](f: (A) => A, a: A): A = {
+ val na = f(a)
+ if(a == na) a else fix(f, na)
+ }
+ fix(searchAndReplaceDFS(transform), expr)
+ }
+
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 31947bf28177682e1376f0fd013944ef9dc37c05..01aea89f986c7263cb312763864006714581057c 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -18,7 +18,7 @@ object TypeTrees {
def setType(tt: TypeTree): self.type = _type match {
case None => _type = Some(tt); this
- case Some(o) if o != tt => scala.sys.error("Resetting type information.")
+ case Some(o) if o != tt => scala.sys.error("Resetting type information! Type [" + o + "] is modified to [" + tt)
case _ => this
}
}
@@ -47,7 +47,7 @@ object TypeTrees {
case other => other
}
- def leastUpperBound(t1: TypeTree, t2: TypeTree): TypeTree = (t1,t2) match {
+ def leastUpperBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
case (c1: ClassType, c2: ClassType) => {
import scala.collection.immutable.Set
var c: ClassTypeDef = c1.classDef
@@ -72,19 +72,19 @@ object TypeTrees {
}
if(found.isEmpty) {
- scala.sys.error("Asking for lub of unrelated class types : " + t1 + " and " + t2)
+ None
} else {
- classDefToClassType(found.get)
+ Some(classDefToClassType(found.get))
}
}
- case (o1, o2) if (o1 == o2) => o1
- case (o1,BottomType) => o1
- case (BottomType,o2) => o2
- case (o1,AnyType) => AnyType
- case (AnyType,o2) => AnyType
+ case (o1, o2) if (o1 == o2) => Some(o1)
+ case (o1,BottomType) => Some(o1)
+ case (BottomType,o2) => Some(o2)
+ case (o1,AnyType) => Some(AnyType)
+ case (AnyType,o2) => Some(AnyType)
- case _ => scala.sys.error("Asking for lub of unrelated types: " + t1 + " and " + t2)
+ case _ => None
}
// returns the number of distinct values that inhabit a type
@@ -100,6 +100,7 @@ object TypeTrees {
case UnitType => FiniteSize(1)
case Int32Type => InfiniteSize
case ListType(_) => InfiniteSize
+ case ArrayType(_) => InfiniteSize
case TupleType(bases) => {
val baseSizes = bases.map(domainSize(_))
baseSizes.find(_ == InfiniteSize) match {
@@ -148,6 +149,7 @@ object TypeTrees {
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
case class OptionType(base: TypeTree) extends TypeTree
case class FunctionType(from: List[TypeTree], to: TypeTree) extends TypeTree
+ case class ArrayType(base: TypeTree) extends TypeTree
sealed abstract class ClassType extends TypeTree {
val classDef: ClassTypeDef
diff --git a/src/main/scala/leon/testgen/CallGraph.scala b/src/main/scala/leon/testgen/CallGraph.scala
new file mode 100644
index 0000000000000000000000000000000000000000..16e31057390e2cea0fd1714d7631c819593ecc04
--- /dev/null
+++ b/src/main/scala/leon/testgen/CallGraph.scala
@@ -0,0 +1,388 @@
+package leon.testgen
+
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+import leon.purescala.Common._
+import leon.FairZ3Solver
+
+class CallGraph(val program: Program) {
+
+ sealed abstract class ProgramPoint
+ case class FunctionStart(fd: FunDef) extends ProgramPoint
+ case class ExpressionPoint(wp: Expr, id: Int) extends ProgramPoint
+ private var epid = -1
+ private def freshExpressionPoint(wp: Expr) = {epid += 1; ExpressionPoint(wp, epid)}
+
+ case class TransitionLabel(cond: Expr, assignment: Map[Variable, Expr])
+
+ private lazy val graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = buildGraph
+ private lazy val programPoints: Set[ProgramPoint] = {
+ graph.flatMap(pair => pair._2.map(edge => edge._1).toSet + pair._1).toSet
+ }
+
+ private def buildGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
+ var callGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = Map()
+
+ program.definedFunctions.foreach(fd => {
+ val body = fd.body.get
+ //val cleanBody = hoistIte(expandLets(matchToIfThenElse(body)))
+ val cleanBody = expandLets(matchToIfThenElse(body))
+ val subgraph = collectWithPathCondition(cleanBody, FunctionStart(fd))
+ callGraph ++= subgraph
+ })
+
+ callGraph = addFunctionInvocationsEdges(callGraph)
+
+ callGraph = simplifyGraph(callGraph)
+
+ callGraph
+ }
+
+ private def simplifyGraph(graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]]): Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
+ def fix[A](f: (A) => A, a: A): A = {
+ val na = f(a)
+ if(a == na) a else fix(f, na)
+ }
+ fix(compressGraph, graph)
+ }
+
+ //does a one level compression of the graph
+ private def compressGraph(graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]]): Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
+ var newGraph = graph
+
+ graph.find{
+ case (point, edges) => {
+ edges.exists{
+ case edge@(p2@ExpressionPoint(e, _), TransitionLabel(BooleanLiteral(true), assign)) if assign.isEmpty && !e.isInstanceOf[Waypoint] => {
+ val edgesOfPoint: Set[(ProgramPoint, TransitionLabel)] = graph.get(p2).getOrElse(Set()) //should be unique entry point and cannot be a FunctionStart
+ newGraph += (point -> ((edges - edge) ++ edgesOfPoint))
+ newGraph -= p2
+ true
+ }
+ case _ => false
+ }
+ }
+ }
+
+ newGraph
+ }
+
+
+ private def addFunctionInvocationsEdges(graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]]): Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
+ var augmentedGraph = graph
+
+ graph.foreach{
+ case (point@ExpressionPoint(FunctionInvocation(fd, args), _), edges) => {
+ val newPoint = FunctionStart(fd)
+ val newTransition = TransitionLabel(BooleanLiteral(true), fd.args.zip(args).map{ case (VarDecl(id, _), arg) => (id.toVariable, arg) }.toMap)
+ augmentedGraph += (point -> (edges + ((newPoint, newTransition))))
+ }
+ case _ => ;
+ }
+
+ augmentedGraph
+ }
+
+ private def collectWithPathCondition(expression: Expr, startingPoint: ProgramPoint): Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
+ var callGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = Map()
+
+ def rec(expr: Expr, path: List[Expr], startingPoint: ProgramPoint): Unit = {
+ val transitions: Set[(ProgramPoint, TransitionLabel)] = callGraph.get(startingPoint) match {
+ case None => Set()
+ case Some(s) => s
+ }
+ expr match {
+ //case FunctionInvocation(fd, args) => {
+ // val newPoint = FunctionStart(fd)
+ // val newTransition = TransitionLabel(And(path.toSeq), fd.args.zip(args).map{ case (VarDecl(id, _), arg) => (id.toVariable, arg) }.toMap)
+ // callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ // args.foreach(arg => rec(arg, path, startingPoint))
+ //}
+ //this case is actually now handled in the unaryOp case
+ //case way@Waypoint(i, e) => {
+ // val newPoint = ExpressionPoint(way)
+ // val newTransition = TransitionLabel(And(path.toSeq), Map())
+ // callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ // rec(e, List(), newPoint)
+ //}
+ case IfExpr(cond, then, elze) => {
+ rec(cond, path, startingPoint)
+ rec(then, cond :: path, startingPoint)
+ rec(elze, Not(cond) :: path, startingPoint)
+ }
+ case n@NAryOperator(args, _) => {
+ val newPoint = freshExpressionPoint(n)
+ val newTransition = TransitionLabel(And(path.toSeq), Map())
+ callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ args.foreach(rec(_, List(), newPoint))
+ }
+ case b@BinaryOperator(t1, t2, _) => {
+ val newPoint = freshExpressionPoint(b)
+ val newTransition = TransitionLabel(And(path.toSeq), Map())
+ callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ rec(t1, List(), newPoint)
+ rec(t2, List(), newPoint)
+ }
+ case u@UnaryOperator(t, _) => {
+ val newPoint = freshExpressionPoint(u)
+ val newTransition = TransitionLabel(And(path.toSeq), Map())
+ callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ rec(t, List(), newPoint)
+ }
+ case t : Terminal => {
+ val newPoint = freshExpressionPoint(t)
+ val newTransition = TransitionLabel(And(path.toSeq), Map())
+ callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
+ }
+ case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
+ }
+ }
+
+ rec(expression, List(), startingPoint)
+ callGraph
+ }
+
+ //given a path, follow the path to build the logical constraint that need to be satisfiable
+ def pathConstraint(path: Seq[(ProgramPoint, ProgramPoint, TransitionLabel)], assigns: List[Map[Expr, Expr]] = List()): Expr = {
+ if(path.isEmpty) BooleanLiteral(true) else {
+ val (_, _, TransitionLabel(cond, assign)) = path.head
+ val finalCond = assigns.foldRight(cond)((map, acc) => replace(map, acc))
+ And(finalCond,
+ pathConstraint(
+ path.tail,
+ if(assign.isEmpty) assigns else assign.asInstanceOf[Map[Expr, Expr]] :: assigns
+ )
+ )
+ }
+ }
+
+ private def isMain(fd: FunDef): Boolean = {
+ fd.annotations.exists(_ == "main")
+ }
+
+ def findAllPaths(z3Solver: FairZ3Solver): Set[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = {
+ val waypoints: Set[ProgramPoint] = programPoints.filter{ case ExpressionPoint(Waypoint(_, _), _) => true case _ => false }
+ val sortedWaypoints: Seq[ProgramPoint] = waypoints.toSeq.sortWith((p1, p2) => {
+ val (ExpressionPoint(Waypoint(i1, _), _), ExpressionPoint(Waypoint(i2, _), _)) = (p1, p2)
+ i1 <= i2
+ })
+
+ val functionPoints: Set[ProgramPoint] = programPoints.flatMap{ case f@FunctionStart(fd) => Set[ProgramPoint](f) case _ => Set[ProgramPoint]() }
+ val mainPoint: Option[ProgramPoint] = functionPoints.find{ case FunctionStart(fd) => isMain(fd) case p => sys.error("unexpected: " + p) }
+
+ assert(mainPoint != None)
+
+ if(sortedWaypoints.size == 0) {
+ findSimplePaths(mainPoint.get)
+ } else {
+ visitAllWaypoints(mainPoint.get :: sortedWaypoints.toList, z3Solver) match {
+ case None => Set()
+ case Some(p) => Set(p)
+ }
+ //Set(
+ // sortedWaypoints.zip(sortedWaypoints.tail).foldLeft(Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]())((path, waypoint) =>
+ // path ++ findPath(waypoint._1, waypoint._2))
+ //)
+ }
+ }
+
+ def visitAllWaypoints(waypoints: List[ProgramPoint], z3Solver: FairZ3Solver): Option[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = {
+ def rec(head: ProgramPoint, tail: List[ProgramPoint], path: Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]):
+ Option[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = {
+ tail match {
+ case Nil => Some(path)
+ case x::xs => {
+ val allPaths = findSimplePaths(head, Some(x))
+ var completePath: Option[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = None
+ allPaths.find(intermediatePath => {
+ val pc = pathConstraint(path ++ intermediatePath)
+ z3Solver.init()
+ z3Solver.restartZ3
+
+ var testcase: Option[Map[Identifier, Expr]] = None
+
+ val (solverResult, model) = z3Solver.decideWithModel(pc, false)
+ solverResult match {
+ case None => {
+ false
+ }
+ case Some(true) => {
+ false
+ }
+ case Some(false) => {
+ val recPath = rec(x, xs, path ++ intermediatePath)
+ recPath match {
+ case None => false
+ case Some(path) => {
+ completePath = Some(path)
+ true
+ }
+ }
+ }
+ }
+ })
+ completePath
+ }
+ }
+ }
+ rec(waypoints.head, waypoints.tail, Seq())
+ }
+
+ def findSimplePaths(from: ProgramPoint, to: Option[ProgramPoint] = None): Set[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = {
+ def dfs(point: ProgramPoint, path: List[(ProgramPoint, ProgramPoint, TransitionLabel)], visitedPoints: Set[ProgramPoint]):
+ Set[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = graph.get(point) match {
+ case None => Set(path.reverse)
+ case Some(edges) => {
+ if(to != None && to.get == point)
+ Set(path.reverse)
+ else if(to == None && edges.forall((edge: (ProgramPoint, TransitionLabel)) => visitedPoints.contains(edge._1) || point == edge._1))
+ Set(path.reverse)
+ else {
+ edges.flatMap((edge: (ProgramPoint, TransitionLabel)) => {
+ val (neighbour, transition) = edge
+ if(visitedPoints.contains(neighbour) || point == neighbour)
+ Set[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]]()
+ else
+ dfs(neighbour, (point, neighbour, transition) :: path, visitedPoints + point)
+ })
+ }
+ }
+ }
+
+ dfs(from, List(), Set())
+ }
+
+ //find a path that goes through all waypoint in order
+ def findPath(from: ProgramPoint, to: ProgramPoint): Seq[(ProgramPoint, ProgramPoint, TransitionLabel)] = {
+ var visitedPoints: Set[ProgramPoint] = Set()
+ var history: Map[ProgramPoint, (ProgramPoint, TransitionLabel)] = Map()
+ var toVisit: List[ProgramPoint] = List(from)
+
+ var currentPoint: ProgramPoint = null
+ while(!toVisit.isEmpty && currentPoint != to) {
+ currentPoint = toVisit.head
+ if(currentPoint != to) {
+ visitedPoints += currentPoint
+ toVisit = toVisit.tail
+ graph.get(currentPoint).foreach(edges => edges.foreach{
+ case (neighbour, transition) =>
+ if(!visitedPoints.contains(neighbour) && !toVisit.contains(neighbour)) {
+ toVisit ::= neighbour
+ history += (neighbour -> ((currentPoint, transition)))
+ }
+ })
+ }
+ }
+
+ def rebuildPath(point: ProgramPoint, path: List[(ProgramPoint, ProgramPoint, TransitionLabel)]): Seq[(ProgramPoint, ProgramPoint, TransitionLabel)] = {
+ if(point == from) path else {
+ val (previousPoint, transition) = history(point)
+ val newPath = (previousPoint, point, transition) :: path
+ rebuildPath(previousPoint, newPath)
+ }
+ }
+
+ //TODO: handle case where the target node is not found
+ rebuildPath(to, List())
+ }
+
+
+ lazy val toDotString: String = {
+ var vertexLabels: Set[(String, String)] = Set()
+ var vertexId = -1
+ var point2vertex: Map[ProgramPoint, Int] = Map()
+ //return id and label
+ def getVertex(p: ProgramPoint): (String, String) = point2vertex.get(p) match {
+ case Some(id) => ("v_" + id, ppPoint(p))
+ case None => {
+ vertexId += 1
+ point2vertex += (p -> vertexId)
+ val pair = ("v_" + vertexId, ppPoint(p))
+ vertexLabels += pair
+ pair
+ }
+ }
+
+ def ppPoint(p: ProgramPoint): String = p match {
+ case FunctionStart(fd) => fd.id.name
+ case ExpressionPoint(Waypoint(i, e), _) => "WayPoint " + i
+ case ExpressionPoint(e, _) => e.toString
+ }
+ def ppLabel(l: TransitionLabel): String = {
+ val TransitionLabel(cond, assignments) = l
+ cond.toString + ", " + assignments.map(p => p._1 + " -> " + p._2).mkString("\n")
+ }
+
+ val edges: List[(String, String, String)] = graph.flatMap(pair => {
+ val (startPoint, edges) = pair
+ val (startId, _) = getVertex(startPoint)
+ edges.map(pair => {
+ val (endPoint, label) = pair
+ val (endId, _) = getVertex(endPoint)
+ (startId, endId, ppLabel(label))
+ }).toList
+ }).toList
+
+ val res = (
+ "digraph " + program.id.name + " {\n" +
+ vertexLabels.map(p => p._1 + " [label=\"" + p._2 + "\"];").mkString("\n") + "\n" +
+ edges.map(p => p._1 + " -> " + p._2 + " [label=\"" + p._3 + "\"];").mkString("\n") + "\n" +
+ "}")
+
+ res
+ }
+
+ def writeDotFile(filename: String) {
+ import java.io.FileWriter
+ import java.io.BufferedWriter
+ val fstream = new FileWriter(filename)
+ val out = new BufferedWriter(fstream)
+ out.write(toDotString)
+ out.close
+ }
+
+}
+
+ //def hoistIte(expr: Expr): (Seq[Expr] => Expr, Seq[Expr]) = expr match {
+ // case ite@IfExpr(c, t, e) => {
+ // val (iteThen, valsThen) = hoistIte(t)
+ // val nbValsThen = valsThen.size
+ // val (iteElse, valsElse) = hoistIte(e)
+ // val nbValsElse = valsElse.size
+ // def ite(es: Seq[Expr]): Expr = {
+ // val argsThen = es.take(nbValsThen)
+ // val argsElse = es.drop(nbValsThen)
+ // IfExpr(c, iteThen(argsThen), iteElse(argsElse), e2)
+ // }
+ // (ite, valsThen ++ valsElse)
+ // }
+ // case BinaryOperator(t1, t2, op) => {
+ // val (iteLeft, valsLeft) = hoistIte(t1)
+ // val (iteRight, valsRight) = hoistIte(t2)
+ // def ite(e1: Expr, e2: Expr): Expr = {
+
+ // }
+ // iteLeft(
+ // iteRight(
+ // op(thenValRight, thenValLeft),
+ // op(thenValRight, elseValLeft)
+ // ), iteRight(
+ // op(elseValRight, thenValLeft),
+ // op(elseValRight, elseValLeft)
+ // )
+ // )
+ // }
+ // case NAryOperator(args, op) => {
+
+ // }
+ // case (t: Terminal) => {
+ // def ite(es: Seq[Expr]): Expr = {
+ // require(es.size == 1)
+ // es.head
+ // }
+ // (ite, Seq(t))
+ // }
+ // case _ => scala.sys.error("Unhandled tree in hoistIte : " + expr)
+ //}
+
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1b48d72579f0ff620ef7d35f41e9bcfe841f3ac4
--- /dev/null
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -0,0 +1,145 @@
+package leon.testgen
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+import leon.purescala.ScalaPrinter
+import leon.Extensions._
+import leon.FairZ3Solver
+import leon.Reporter
+
+import scala.collection.mutable.{Set => MutableSet}
+
+class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
+
+ def description: String = "Generate random testcases"
+ override def shortDescription: String = "test"
+
+ private val z3Solver = new FairZ3Solver(reporter)
+
+ def analyse(program: Program) {
+ z3Solver.setProgram(program)
+ reporter.info("Running test generation")
+
+ val testcases = generateTestCases(program)
+
+ val topFunDef = program.definedFunctions.find(fd => isMain(fd)).get
+//fd.body.exists(body => body match {
+// case Waypoint(1, _) => true
+// case _ => false
+// })
+ val testFun = new FunDef(FreshIdentifier("test"), UnitType, Seq())
+ val funInvocs = testcases.map(testcase => {
+ val params = topFunDef.args
+ val args = topFunDef.args.map{
+ case VarDecl(id, tpe) => testcase.get(id) match {
+ case Some(v) => v
+ case None => simplestValue(tpe)
+ }
+ }
+ FunctionInvocation(topFunDef, args)
+ }).toSeq
+ testFun.body = Some(Block(funInvocs, UnitLiteral))
+
+ val Program(id, ObjectDef(objId, defs, invariants)) = program
+ val testProgram = Program(id, ObjectDef(objId, testFun +: defs , invariants))
+ testProgram.writeScalaFile("TestGen.scalax")
+
+ reporter.info("Running from waypoint with the following testcases:\n")
+ reporter.info(testcases.mkString("\n"))
+ }
+
+ private def isMain(fd: FunDef): Boolean = {
+ fd.annotations.exists(_ == "main")
+ }
+
+ def generatePathConditions(program: Program): Set[Expr] = {
+
+ val callGraph = new CallGraph(program)
+ callGraph.writeDotFile("testgen.dot")
+ val constraints = callGraph.findAllPaths(z3Solver).map(path => {
+ println("Path is: " + path)
+ val cnstr = callGraph.pathConstraint(path)
+ println("constraint is: " + cnstr)
+ cnstr
+ })
+ constraints
+ }
+
+ private def generateTestCases(program: Program): Set[Map[Identifier, Expr]] = {
+ val allPaths = generatePathConditions(program)
+
+ allPaths.flatMap(pathCond => {
+ reporter.info("Now considering path condition: " + pathCond)
+
+ var testcase: Option[Map[Identifier, Expr]] = None
+ //val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
+
+ z3Solver.init()
+ z3Solver.restartZ3
+ val (solverResult, model) = z3Solver.decideWithModel(pathCond, false)
+
+ solverResult match {
+ case None => Seq()
+ case Some(true) => {
+ reporter.info("The path is unreachable")
+ Seq()
+ }
+ case Some(false) => {
+ reporter.info("The model should be used as the testcase")
+ Seq(model)
+ }
+ }
+ })
+ }
+
+ //private def generatePathConditions(funDef: FunDef): Seq[Expr] = if(!funDef.hasImplementation) Seq() else {
+ // val body = funDef.body.get
+ // val cleanBody = hoistIte(expandLets(matchToIfThenElse(body)))
+ // collectWithPathCondition(cleanBody)
+ //}
+
+ //private def generateTestCases(funDef: FunDef): Seq[Map[Identifier, Expr]] = {
+ // val allPaths = generatePathConditions(funDef)
+
+ // allPaths.flatMap(pathCond => {
+ // reporter.info("Now considering path condition: " + pathCond)
+
+ // var testcase: Option[Map[Identifier, Expr]] = None
+ // //val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
+ //
+ // z3Solver.init()
+ // z3Solver.restartZ3
+ // val (solverResult, model) = z3Solver.decideWithModel(pathCond, false)
+
+ // solverResult match {
+ // case None => Seq()
+ // case Some(true) => {
+ // reporter.info("The path is unreachable")
+ // Seq()
+ // }
+ // case Some(false) => {
+ // reporter.info("The model should be used as the testcase")
+ // Seq(model)
+ // }
+ // }
+ // })
+ //}
+
+ //prec: ite are hoisted and no lets nor match occurs
+ //private def collectWithPathCondition(expression: Expr): Seq[Expr] = {
+ // var allPaths: Seq[Expr] = Seq()
+
+ // def rec(expr: Expr, path: List[Expr]): Seq[Expr] = expr match {
+ // case IfExpr(cond, then, elze) => rec(then, cond :: path) ++ rec(elze, Not(cond) :: path)
+ // case _ => Seq(And(path.toSeq))
+ // }
+
+ // rec(expression, List())
+ //}
+
+}
+
+
+
diff --git a/testcases/Abs.scala b/testcases/Abs.scala
index 5efb41797b5dc4401407c5fea7c3fc6a7591f4f2..52baf710140b76bf5edeeda52ef9e0da5385734f 100644
--- a/testcases/Abs.scala
+++ b/testcases/Abs.scala
@@ -1,51 +1,5 @@
-import leon.Utils._
-
object Abs {
-
- def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size <= 5 && isArray(tab, size))
- var k = 0
- var tabres = Map.empty[Int, Int]
- (while(k < size) {
- if(tab(k) < 0)
- tabres = tabres.updated(k, -tab(k))
- else
- tabres = tabres.updated(k, tab(k))
- k = k + 1
- }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
- tabres
- }) ensuring(res => isArray(res, size) && isPositive(res, size))
-
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 10 && isArray(a, size))
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size)
- true
- else {
- if(a(i) < 0)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
-
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
+ def abs(x: Int): Int = (if(x < 0) -x else x) ensuring(_ >= 0)
}
diff --git a/testcases/AbsArray.scala b/testcases/AbsArray.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0086891cdafc5a62987d5563695b38983de24fb4
--- /dev/null
+++ b/testcases/AbsArray.scala
@@ -0,0 +1,51 @@
+import leon.Utils._
+
+object AbsArray {
+
+
+ def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size <= 5 && isArray(tab, size))
+ var k = 0
+ var tabres = Map.empty[Int, Int]
+ (while(k < size) {
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
+ k = k + 1
+ }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
+ tabres
+ }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 10 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/testcases/AbsFun.scala b/testcases/AbsFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8186824b03bca673a899a8505347c09c86e43360
--- /dev/null
+++ b/testcases/AbsFun.scala
@@ -0,0 +1,65 @@
+import leon.Utils._
+
+object AbsFun {
+
+
+ def isPositive(a : Array[Int], size : Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ rec(0, a, size)
+ }
+
+ def rec(i: Int, a: Array[Int], size: Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length && i >= 0)
+
+ if(i >= size) true
+ else {
+ if (a(i) < 0)
+ false
+ else
+ rec(i + 1, a, size)
+ }
+ }
+
+ def abs(tab: Array[Int]): Array[Int] = {
+ require(tab.length >= 0)
+ val t = while0(Array.fill(tab.length)(0), 0, tab)
+ t._1
+ } ensuring(res => isPositive(res, res.length))
+
+
+ def while0(t: Array[Int], k: Int, tab: Array[Int]): (Array[Int], Int) = {
+ require(tab.length >= 0 &&
+ t.length == tab.length &&
+ k >= 0 &&
+ k <= tab.length &&
+ isPositive(t, k))
+
+ if(k < tab.length) {
+ val nt = if(tab(k) < 0) {
+ t.updated(k, -tab(k))
+ } else {
+ t.updated(k, tab(k))
+ }
+ while0(nt, k+1, tab)
+ } else {
+ (t, k)
+ }
+ } ensuring(res =>
+ res._2 >= tab.length &&
+ res._1.length == tab.length &&
+ res._2 >= 0 &&
+ res._2 <= tab.length &&
+ isPositive(res._1, res._2))
+
+ def property(t: Array[Int], k: Int): Boolean = {
+ require(isPositive(t, k) && t.length >= 0 && k >= 0)
+ if(k < t.length) {
+ val nt = if(t(k) < 0) {
+ t.updated(k, -t(k))
+ } else {
+ t.updated(k, t(k))
+ }
+ isPositive(nt, k+1)
+ } else true
+ } holds
+}
diff --git a/testcases/BinarySearch.scala b/testcases/BinarySearch.scala
index 92d4cf0667fe0175b80ae0da34679e991efcc633..986ee41ae6a057065bc8520c5af010092b67b2b2 100644
--- a/testcases/BinarySearch.scala
+++ b/testcases/BinarySearch.scala
@@ -4,10 +4,10 @@ import leon.Utils._
object BinarySearch {
- def binarySearch(a: Map[Int, Int], size: Int, key: Int): Int = ({
- require(isArray(a, size) && size < 5 && sorted(a, size, 0, size - 1))
+ def binarySearch(a: Array[Int], key: Int): Int = ({
+ require(a.length > 0 && sorted(a, 0, a.length - 1))
var low = 0
- var high = size - 1
+ var high = a.length - 1
var res = -1
(while(low <= high && res == -1) {
@@ -21,13 +21,27 @@ object BinarySearch {
high = i - 1
else if(v < key)
low = i + 1
- }) invariant(0 <= low && low <= high + 1 && high < size && (if(res >= 0) a(res) == key else (!occurs(a, 0, low, key) && !occurs(a, high + 1, size, key))))
+ }) invariant(
+ res >= -1 &&
+ res < a.length &&
+ 0 <= low &&
+ low <= high + 1 &&
+ high >= -1 &&
+ high < a.length &&
+ (if (res >= 0)
+ a(res) == key else
+ (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+ )
+ )
res
- }) ensuring(res => res >= -1 && res < size && (if(res >= 0) a(res) == key else !occurs(a, 0, size, key)))
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
- def occurs(a: Map[Int, Int], from: Int, to: Int, key: Int): Boolean = {
- require(isArray(a, to) && to < 5 && from >= 0)
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
if(i >= to)
@@ -43,31 +57,16 @@ object BinarySearch {
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
-
- def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
- val t = sortedWhile(true, l, l, u, a, size)
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
t._1
}
- def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
if(k < u) {
- sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
} else (isSorted, k)
}
}
diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala
index 4e274e2707b0cff262e712ab4b78b53eee0db990..3551ebf16416f68bd932adc512177edc6f2611d8 100644
--- a/testcases/BubbleSort.scala
+++ b/testcases/BubbleSort.scala
@@ -2,44 +2,44 @@ import leon.Utils._
/* The calculus of Computation textbook */
-object Bubble {
+object BubbleSort {
- def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size < 5 && isArray(a, size))
- var i = size - 1
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
var j = 0
- var sortedArray = a
+ val sa = a.clone
(while(i > 0) {
j = 0
(while(j < i) {
- if(sortedArray(j) > sortedArray(j+1)) {
- val tmp = sortedArray(j)
- sortedArray = sortedArray.updated(j, sortedArray(j+1))
- sortedArray = sortedArray.updated(j+1, tmp)
+ if(sa(j) > sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
}
j = j + 1
}) invariant(
j >= 0 &&
j <= i &&
- i < size &&
- isArray(sortedArray, size) &&
- partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- sorted(sortedArray, size, i, size-1) &&
- partitioned(sortedArray, size, 0, j-1, j, j)
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j-1, j, j)
)
i = i - 1
}) invariant(
i >= 0 &&
- i < size &&
- isArray(sortedArray, size) &&
- partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- sorted(sortedArray, size, i, size-1)
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
)
- sortedArray
- }) ensuring(res => sorted(res, size, 0, size-1))
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
- def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
var k = l
var isSorted = true
(while(k < u) {
@@ -49,57 +49,9 @@ object Bubble {
}) invariant(k <= u && k >= l)
isSorted
}
- /*
- // --------------------- sorted --------------------
- def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
- val t = sortedWhile(true, l, l, u, a, size)
- t._1
- }
-
- def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
- if(k < u) {
- sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
- } else (isSorted, k)
- }
- */
-
- /*
- // ------------- partitioned ------------------
- def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
- if(l2 > u2 || l1 > u1)
- true
- else {
- val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
- t._2
- }
- }
- def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
-
- if(i <= u1) {
- val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
- partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
- } else (j, isPartitionned, i)
- }
- def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
- require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
- if (j <= u2) {
- partitionedNestedWhile(
- (if (a(i) > a(j))
- false
- else
- isPartitionned),
- j + 1, i, l1, u1, size, u2, a, l2)
- } else (isPartitionned, j)
- }
- */
-
- def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
if(l2 > u2 || l1 > u1)
true
else {
@@ -119,14 +71,4 @@ object Bubble {
}
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
- def rec(i: Int): Boolean = if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- if(size <= 0)
- false
- else
- rec(0)
- }
-
}
diff --git a/testcases/LinearSearch.scala b/testcases/LinearSearch.scala
index e91a3f2679b33b8b35e7d64989db1b7ade451d14..e18c4039c7d7f7418399ff16483d1b18cc6895a9 100644
--- a/testcases/LinearSearch.scala
+++ b/testcases/LinearSearch.scala
@@ -4,29 +4,29 @@ import leon.Utils._
object LinearSearch {
- def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
- require(size <= 5 && isArray(a, size))
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
var i = 0
var found = false
- (while(i < size) {
+ (while(i < a.length) {
if(a(i) == c)
found = true
i = i + 1
- }) invariant(i <= size &&
- i >= 0 &&
- (if(found) contains(a, i, c) else !contains(a, i, c))
- )
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
found
- }) ensuring(res => if(res) contains(a, size, c) else !contains(a, size, c))
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
- def contains(a: Map[Int, Int], size: Int, c: Int): Boolean = {
- require(isArray(a, size) && size <= 5)
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
content(a, size).contains(c)
}
-
- def content(a: Map[Int, Int], size: Int): Set[Int] = {
- require(isArray(a, size) && size <= 5)
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
var set = Set.empty[Int]
var i = 0
(while(i < size) {
@@ -36,18 +36,4 @@ object LinearSearch {
set
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
diff --git a/testcases/ListImp.scala b/testcases/ListImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f3887419ecf59c6241ed530febbac6400538f6bd
--- /dev/null
+++ b/testcases/ListImp.scala
@@ -0,0 +1,49 @@
+import leon.Utils._
+
+object ListImp {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def size(l: List) : Int = {
+ var r = 0
+ (while(!l.isInstanceOf[Nil]) {
+ r = r+1
+ }) invariant(r >= 0)
+ r
+ } ensuring(res => res >= 0)
+
+ def reverse(l: List): List = {
+ var r: List = Nil()
+ var l2: List = l
+
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(l2) == content(l))
+
+ r
+ } ensuring(res => content(res) == content(l))
+
+ def append(l1 : List, l2 : List) : List = {
+ var r: List = l2
+ var tmp: List = reverse(l1)
+
+ (while(!tmp.isInstanceOf[Nil]) {
+ val Cons(head, tail) = tmp
+ tmp = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(tmp) == content(l1) ++ content(l2))
+
+ r
+ } ensuring(content(_) == content(l1) ++ content(l2))
+
+
+}
diff --git a/testcases/MaxSum.scala b/testcases/MaxSum.scala
index 07c5d12ab2450cc95af964c7078759a13fe8f0cb..ba724d255c23b782e1b4de716ccc8d50043e2059 100644
--- a/testcases/MaxSum.scala
+++ b/testcases/MaxSum.scala
@@ -4,44 +4,26 @@ import leon.Utils._
object MaxSum {
-
- def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
- require(isArray(a, size) && size < 5 && isPositive(a, size))
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
var sum = 0
var max = 0
var i = 0
- (while(i < size) {
+ (while(i < a.length) {
if(max < a(i))
max = a(i)
sum = sum + a(i)
i = i + 1
- }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
(sum, max)
- }) ensuring(res => res._1 <= size * res._2)
+ }) ensuring(res => res._1 <= a.length * res._2)
-/*
- def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size)
- true
- else {
- if(a(i) > n)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
- */
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 5 && isArray(a, size))
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
- if(i >= size)
+ if(i >= a.length)
true
else {
if(a(i) < 0)
@@ -53,18 +35,4 @@ object MaxSum {
rec(0)
}
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
}
diff --git a/testcases/master-thesis-regis/Arithmetic.scala b/testcases/master-thesis-regis/Arithmetic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9173132e00e9e01d27155d1eec95eacc2aa44f1e
--- /dev/null
+++ b/testcases/master-thesis-regis/Arithmetic.scala
@@ -0,0 +1,73 @@
+import leon.Utils._
+
+object Arithmetic {
+
+ /* VSTTE 2008 - Dafny paper */
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+ /* VSTTE 2008 - Dafny paper */
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+ /* VSTTE 2008 - Dafny paper */
+ def addBuggy(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+ def sum(n: Int): Int = {
+ require(n >= 0)
+ var r = 0
+ var i = 0
+ (while(i < n) {
+ i = i + 1
+ r = r + i
+ }) invariant(r >= i && i >= 0 && r >= 0)
+ r
+ } ensuring(_ >= n)
+
+}
diff --git a/testcases/master-thesis-regis/ArrayOperations.scala b/testcases/master-thesis-regis/ArrayOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..91eb371faa8e550f3d85dfa17d13ba2ef3d6e101
--- /dev/null
+++ b/testcases/master-thesis-regis/ArrayOperations.scala
@@ -0,0 +1,207 @@
+import leon.Utils._
+
+object ArrayOperations {
+
+ /* VSTTE 2008 - Dafny paper */
+ def binarySearch(a: Array[Int], key: Int): Int = ({
+ require(a.length > 0 && sorted(a, 0, a.length - 1))
+ var low = 0
+ var high = a.length - 1
+ var res = -1
+
+ (while(low <= high && res == -1) {
+ val i = (high + low) / 2
+ val v = a(i)
+
+ if(v == key)
+ res = i
+
+ if(v > key)
+ high = i - 1
+ else if(v < key)
+ low = i + 1
+ }) invariant(
+ res >= -1 &&
+ res < a.length &&
+ 0 <= low &&
+ low <= high + 1 &&
+ high >= -1 &&
+ high < a.length &&
+ (if (res >= 0)
+ a(res) == key else
+ (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+ )
+ )
+ res
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+
+ /* The calculus of Computation textbook */
+ def bubbleSort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) > sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j-1, j, j)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
+ )
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
+
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+ /* The calculus of Computation textbook */
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
+ var i = 0
+ var found = false
+ (while(i < a.length) {
+ if(a(i) == c)
+ found = true
+ i = i + 1
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
+ found
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
+
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ content(a, size).contains(c)
+ }
+
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ var set = Set.empty[Int]
+ var i = 0
+ (while(i < size) {
+ set = set ++ Set(a(i))
+ i = i + 1
+ }) invariant(i >= 0 && i <= size)
+ set
+ }
+
+ def abs(tab: Array[Int]): Array[Int] = ({
+ require(tab.length >= 0)
+ var k = 0
+ val tabres = Array.fill(tab.length)(0)
+ (while(k < tab.length) {
+ if(tab(k) < 0)
+ tabres(k) = -tab(k)
+ else
+ tabres(k) = tab(k)
+ k = k + 1
+ }) invariant(
+ tabres.length == tab.length &&
+ k >= 0 && k <= tab.length &&
+ isPositive(tabres, k))
+ tabres
+ }) ensuring(res => isPositive(res, res.length))
+
+ def isPositive(a: Array[Int], size: Int): Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ /* VSTTE 2010 challenge 1 */
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a, a.length))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < a.length) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+ (sum, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+}
diff --git a/testcases/master-thesis-regis/Constraints.scala b/testcases/master-thesis-regis/Constraints.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b7c7133ddcbd5018cc6bf6b896d326e439deaf2
--- /dev/null
+++ b/testcases/master-thesis-regis/Constraints.scala
@@ -0,0 +1,76 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ }
+
+ def setSize(set: Set[Int]): Int = {
+ if(set == Set.empty[Int])
+ 0
+ else {
+ val elem = epsilon((x : Int) => set contains x)
+ 1 + setSize(set -- Set[Int](elem))
+ }
+ } ensuring(_ >= 0)
+
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = {
+ if(set == Set.empty[Int])
+ MyNil()
+ else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+ }
+
+ def sizeToListEq(lst: MyList): Boolean = {
+ size(toList(toSet(lst))) == size(lst)
+ } holds
+
+ def sizeToListLessEq(lst: MyList): Boolean = {
+ size(toList(toSet(lst))) <= size(lst)
+ } holds
+
+ def toListEq(lst: MyList): Boolean = {
+ toList(toSet(lst)) == lst
+ } holds
+
+ def positiveNum(): Int = {
+ epsilon((x: Int) => x > 0)
+ } ensuring(_ > 0)
+
+ def negativeNum(): Int = {
+ epsilon((x: Int) => x < 0)
+ } ensuring(_ < 0)
+
+ def linearEquation(): (Int, Int) = {
+ val sol = epsilon((t: (Int, Int)) =>
+ 2*t._1 + 3*t._2 == 10 && t._1 >= 0 && t._2 >= 0)
+ sol
+ } ensuring(res => res == (2, 2) || res == (5, 0))
+
+
+ def nonDeterministicExecution(): Int = {
+ var i = 0
+ var b = epsilon((x: Boolean) => true)
+ while(b) {
+ i = i + 1
+ b = epsilon((x: Boolean) => true)
+ }
+ i
+ } ensuring(_ <= 10)
+
+
+}
diff --git a/testcases/master-thesis-regis/ListOperations.scala b/testcases/master-thesis-regis/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4bb59c26472cfb9f07a09b6571db86cb62b18db7
--- /dev/null
+++ b/testcases/master-thesis-regis/ListOperations.scala
@@ -0,0 +1,146 @@
+import leon.Utils._
+import leon.Annotations._
+
+object ListOperations {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class IPList
+ case class IPCons(head: (Int, Int), tail: IPList) extends IPList
+ case class IPNil() extends IPList
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def iplContent(l: IPList) : Set[(Int, Int)] = l match {
+ case IPNil() => Set.empty[(Int, Int)]
+ case IPCons(x, xs) => Set(x) ++ iplContent(xs)
+ }
+
+ def size(l: List) : Int = {
+ var r = 0
+ var l2 = l
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(_, tail) = l2
+ l2 = tail
+ r = r+1
+ }) invariant(r >= 0)
+ r
+ } ensuring(res => res >= 0)
+
+ def sizeBuggy(l: List) : Int = {
+ var r = -1
+ var l2 = l
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(_, tail) = l2
+ l2 = tail
+ r = r+1
+ }) invariant(r >= 0)
+ r
+ } ensuring(res => res >= 0)
+
+ def sizeFun(l: List) : Int = l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + sizeFun(t)
+ }
+
+ def iplSizeFun(l: IPList) : Int = l match {
+ case IPNil() => 0
+ case IPCons(_, t) => 1 + iplSizeFun(t)
+ }
+
+ def iplSize(l: IPList) : Int = {
+ var r = 0
+ var l2 = l
+ (while(!l2.isInstanceOf[IPNil]) {
+ val IPCons(_, tail) = l2
+ l2 = tail
+ r = r+1
+ }) invariant(r >= 0)
+ r
+ } ensuring(_ >= 0)
+
+ def sizeImpEqFun(l: List): Boolean = (size(l) == sizeFun(l)) ensuring(_ == true)
+
+ def zip(l1: List, l2: List) : IPList = ({
+ require(sizeFun(l1) == sizeFun(l2))
+ var r: IPList = IPNil()
+ var ll1: List = l1
+ var ll2 = l2
+
+ (while(!ll1.isInstanceOf[Nil]) {
+ val Cons(l1head, l1tail) = ll1
+ val Cons(l2head, l2tail) = if(!ll2.isInstanceOf[Nil]) ll2 else Cons(0, Nil())
+ r = IPCons((l1head, l2head), r)
+ ll1 = l1tail
+ ll2 = l2tail
+ }) invariant(iplSizeFun(r) + sizeFun(ll1) == sizeFun(l1))
+
+ iplReverse(r)
+ }) ensuring(res => iplSizeFun(res) == sizeFun(l1))
+
+ def iplReverse(l: IPList): IPList = {
+ var r: IPList = IPNil()
+ var l2: IPList = l
+
+ (while(!l2.isInstanceOf[IPNil]) {
+ val IPCons(head, tail) = l2
+ l2 = tail
+ r = IPCons(head, r)
+ }) invariant(iplContent(r) ++ iplContent(l2) == iplContent(l) && iplSizeFun(r) + iplSizeFun(l2) == iplSizeFun(l))
+
+ r
+ } ensuring(res => iplContent(res) == iplContent(l) && iplSizeFun(res) == iplSizeFun(l))
+
+ def reverse(l: List): List = {
+ var r: List = Nil()
+ var l2: List = l
+
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(l2) == content(l) && sizeFun(r) + sizeFun(l2) == sizeFun(l))
+
+ r
+ } ensuring(res => content(res) == content(l) && sizeFun(res) == sizeFun(l))
+
+ def listEqReverse(l: List): Boolean = {
+ l == reverse(l)
+ } ensuring(_ == true)
+
+ def append(l1 : List, l2 : List) : List = {
+ var r: List = l2
+ var tmp: List = reverse(l1)
+
+ (while(!tmp.isInstanceOf[Nil]) {
+ val Cons(head, tail) = tmp
+ tmp = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(tmp) == content(l1) ++ content(l2))
+
+ r
+ } ensuring(content(_) == content(l1) ++ content(l2))
+
+ def appendBuggy(l1 : List, l2 : List) : List = {
+ var r: List = l2
+ var tmp: List = l1
+
+ while(!tmp.isInstanceOf[Nil]) {
+ val Cons(head, tail) = tmp
+ tmp = tail
+ r = Cons(head, r)
+ }
+
+ r
+ }
+
+ def appendEqAppendBuggy(l1: List, l2: List): Boolean = {
+ append(l1, l2) == appendBuggy(l1, l2)
+ } ensuring(_ == true)
+
+}
diff --git a/testcases/regression/InfiniteLoop.scala b/testcases/regression/InfiniteLoop.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e9e5d0d5c7e258a77fdb418df3b51194fd6a9594
--- /dev/null
+++ b/testcases/regression/InfiniteLoop.scala
@@ -0,0 +1,12 @@
+object InfiniteLoop {
+
+ def infinite(): Int = {
+ var i = 0
+ var sum = 0
+ while (i < 10) {
+ sum = sum + i
+ }
+ sum
+ }
+
+}
diff --git a/testcases/regression/error/Array1.scala b/testcases/regression/error/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0056f18864ba168abb5735daf0db1e0bb76eda5
--- /dev/null
+++ b/testcases/regression/error/Array1.scala
@@ -0,0 +1,8 @@
+object Array1 {
+
+ def foo(): Int = {
+ (Array.fill(5)(5))(2) = 3
+ 0
+ }
+
+}
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
new file mode 100644
index 0000000000000000000000000000000000000000..9154460c37237761b6c8f2d0ecb0b34fb3ec0bf6
--- /dev/null
+++ b/testcases/regression/error/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..a2c2fbd6ddfde2b3cca2dcc08fb61a79f0ae471c
--- /dev/null
+++ b/testcases/regression/error/Array3.scala
@@ -0,0 +1,12 @@
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(5)
+ if(a.length > 2)
+ a(1) = 2
+ 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/invalid/Array1.scala b/testcases/regression/invalid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8451250c8f9e9c95684b4ea10490aced2a23f6e
--- /dev/null
+++ b/testcases/regression/invalid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/testcases/regression/invalid/Array2.scala b/testcases/regression/invalid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54ab5e3c27918596af58c427fabedd2016a33db9
--- /dev/null
+++ b/testcases/regression/invalid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 4)
+
+}
diff --git a/testcases/regression/invalid/Array3.scala b/testcases/regression/invalid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0c1bb76fdce099bd095c59d8c03fe8e6508a9776
--- /dev/null
+++ b/testcases/regression/invalid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i <= a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/testcases/regression/invalid/Array4.scala b/testcases/regression/invalid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5b5e7406165ad214a7d5d5fffd85d2d4fce226e0
--- /dev/null
+++ b/testcases/regression/invalid/Array4.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/testcases/regression/invalid/Array5.scala b/testcases/regression/invalid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7
--- /dev/null
+++ b/testcases/regression/invalid/Array5.scala
@@ -0,0 +1,10 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/testcases/regression/invalid/Epsilon1.scala b/testcases/regression/invalid/Epsilon1.scala
index 859ced1c19b0c3688ad8eef433fbc290c672fbe9..c3c0a48be96f594fe725518a7289333bb587ef40 100644
--- a/testcases/regression/invalid/Epsilon1.scala
+++ b/testcases/regression/invalid/Epsilon1.scala
@@ -2,8 +2,11 @@ import leon.Utils._
object Epsilon1 {
- def greaterWrong(x: Int): Int = {
- epsilon((y: Int) => y >= x)
- } ensuring(_ > x)
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+
+ //this should not hold
+ def property2(x: Int): Boolean = {
+ rand2(x) == rand2(x+1)
+ } holds
}
diff --git a/testcases/regression/invalid/Epsilon4.scala b/testcases/regression/invalid/Epsilon4.scala
index 52ee6dbe66c2d5b3517d5d84f90f35f8f10aa38d..6619e59d6f9d9721c4bc7587b47dac79f48bf437 100644
--- a/testcases/regression/invalid/Epsilon4.scala
+++ b/testcases/regression/invalid/Epsilon4.scala
@@ -23,5 +23,5 @@ object Epsilon4 {
def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
- def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+ //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
}
diff --git a/testcases/regression/invalid/Epsilon6.scala b/testcases/regression/invalid/Epsilon6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc5aca78c3818a94df43146aba16077ffab50a71
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon6.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon6 {
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/testcases/regression/invalid/MyTuple3.scala b/testcases/regression/invalid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da9f85b16a48f0676d1f15741ad47536e14b57ab
--- /dev/null
+++ b/testcases/regression/invalid/MyTuple3.scala
@@ -0,0 +1,7 @@
+object MyTuple3 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/testcases/regression/invalid/Unit1.scala b/testcases/regression/invalid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e
--- /dev/null
+++ b/testcases/regression/invalid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(_ != ())
+
+}
diff --git a/testcases/regression/valid/Array1.scala b/testcases/regression/valid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3815f03443448a28fb60475b49c09c981a1377f9
--- /dev/null
+++ b/testcases/regression/valid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 3)
+
+}
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/Array2.scala b/testcases/regression/valid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f149a9305cb4b53a4a9353b82e25468c898bdc8
--- /dev/null
+++ b/testcases/regression/valid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/Array3.scala b/testcases/regression/valid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bbb1845b80c0ca747cb0c830828bacdc9668943f
--- /dev/null
+++ b/testcases/regression/valid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fd76e02faa83f8fd1bda5fef7c91e7df7fc29864
--- /dev/null
+++ b/testcases/regression/valid/Array4.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+}
diff --git a/testcases/regression/valid/Array5.scala b/testcases/regression/valid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14bed6eff332db69600353001488c46a3e56aa5d
--- /dev/null
+++ b/testcases/regression/valid/Array5.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/testcases/regression/valid/Array6.scala b/testcases/regression/valid/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bdd6b0c5d9bee06eec14b9f5917762c67af4751b
--- /dev/null
+++ b/testcases/regression/valid/Array6.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array6 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2 && a(2) == 5)
+ a(2)
+ } ensuring(_ == 5)
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/testcases/regression/valid/Array7.scala b/testcases/regression/valid/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..55bbbb72908e2b192152162d82d2ed9fea67923b
--- /dev/null
+++ b/testcases/regression/valid/Array7.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+
+object Array7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length > 0)
+ val a2 = Array.fill(a.length)(0)
+ var i = 0
+ (while(i < a.length) {
+ a2(i) = a(i)
+ i = i + 1
+ }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
+ a2
+ } ensuring(_(0) == a(0))
+
+
+}
diff --git a/testcases/regression/valid/Array8.scala b/testcases/regression/valid/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..270b181220b55af1588f63e7953221ae71f9bde3
--- /dev/null
+++ b/testcases/regression/valid/Array8.scala
@@ -0,0 +1,8 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length >= 2)
+ a.updated(1, 3)
+ } ensuring(res => res.length == a.length && res(1) == 3)
+
+}
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)
+ }
+
+}
diff --git a/testcases/regression/valid/Epsilon2.scala b/testcases/regression/valid/Epsilon2.scala
index b4f53f36bf3b5c76a7c2fad5a4f1cdfed12587a9..36e5268e2b1ccdbc710dc8d6410ce6968231c7d1 100644
--- a/testcases/regression/valid/Epsilon2.scala
+++ b/testcases/regression/valid/Epsilon2.scala
@@ -3,16 +3,11 @@ import leon.Utils._
object Epsilon1 {
def rand(): Int = epsilon((x: Int) => true)
- def rand2(x: Int): Int = epsilon((y: Int) => true)
//this should hold, that is the expected semantic of our epsilon
def property1(): Boolean = {
rand() == rand()
} holds
- //this should hold, that is the expected semantic of our epsilon
- def property2(x: Int): Boolean = {
- rand2(x) == rand2(x+1)
- } holds
}
diff --git a/testcases/regression/valid/Field1.scala b/testcases/regression/valid/Field1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..116557ab7b883d01a10168aeaf529d5300ee5f19
--- /dev/null
+++ b/testcases/regression/valid/Field1.scala
@@ -0,0 +1,11 @@
+object Field1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.size
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/valid/Field2.scala b/testcases/regression/valid/Field2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a96610235a68754b84e58f73f5e435ce642ebc9
--- /dev/null
+++ b/testcases/regression/valid/Field2.scala
@@ -0,0 +1,11 @@
+object Field2 {
+
+ abstract sealed class A
+ case class B(length: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.length
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/valid/IfExpr3.scala b/testcases/regression/valid/IfExpr3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86d4e494a7ce8fd22024020bb9580b393af8377a
--- /dev/null
+++ b/testcases/regression/valid/IfExpr3.scala
@@ -0,0 +1,19 @@
+object IfExpr1 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ 5
+ //var a = 3
+ //var b = 1
+ //b = b + 1
+ //a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/IfExpr4.scala b/testcases/regression/valid/IfExpr4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..94b99fde39e6f7e10b1c898548d60592023ffbd6
--- /dev/null
+++ b/testcases/regression/valid/IfExpr4.scala
@@ -0,0 +1,18 @@
+object IfExpr4 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ var a = 3
+ var b = 1
+ b = b + 1
+ a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/MyTuple4.scala b/testcases/regression/valid/MyTuple4.scala
index 4b87272e23f7d9f2a3c33c29b5d455b88f234ddb..6fcfed661beca0487da4b02db71677e2dbaac60e 100644
--- a/testcases/regression/valid/MyTuple4.scala
+++ b/testcases/regression/valid/MyTuple4.scala
@@ -1,5 +1,5 @@
-object MyTuple1 {
+object MyTuple4 {
abstract class A
case class B(i: Int) extends A
diff --git a/testcases/regression/valid/MyTuple6.scala b/testcases/regression/valid/MyTuple6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a54710fbbe54d9532a5ab4d2ba9906a48ad37acc
--- /dev/null
+++ b/testcases/regression/valid/MyTuple6.scala
@@ -0,0 +1,8 @@
+object MyTuple6 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ require(t._1 > 0 && t._2 > 1)
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/testcases/regression/valid/Nested10.scala b/testcases/regression/valid/Nested10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b3c4f865367ca84a52091e89b655ac6438dc65a2
--- /dev/null
+++ b/testcases/regression/valid/Nested10.scala
@@ -0,0 +1,14 @@
+object Nested10 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = {
+ i + j + n
+ }
+ def rec2(j: Int) = {
+ rec1(j)
+ }
+ rec2(2)
+ } ensuring(i + 4 == _)
+
+}
diff --git a/testcases/regression/valid/Nested11.scala b/testcases/regression/valid/Nested11.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0316fc5f2ba3497691bc48b1d573933ba2cea027
--- /dev/null
+++ b/testcases/regression/valid/Nested11.scala
@@ -0,0 +1,14 @@
+object Nested11 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(j: Int) = b match {
+ case B(b) => i + j + b
+ }
+ rec1(2)
+ } ensuring(i + 5 == _)
+
+}
diff --git a/testcases/regression/valid/Nested12.scala b/testcases/regression/valid/Nested12.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05ac1569f630f1fc905a84f0550cbbaa42047906
--- /dev/null
+++ b/testcases/regression/valid/Nested12.scala
@@ -0,0 +1,17 @@
+object Nested12 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(a: A, j: Int, j2: Int) = a match {
+ case B(b) => i + j + j2 + b
+ }
+ def rec2(a: A, k: Int) = a match {
+ case B(b) => rec1(a, b, k)
+ }
+ rec2(b, 2)
+ } ensuring(i + 8 == _)
+
+}
diff --git a/testcases/regression/valid/Nested13.scala b/testcases/regression/valid/Nested13.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ccb742494564433dffe096210fac07b37a663dfe
--- /dev/null
+++ b/testcases/regression/valid/Nested13.scala
@@ -0,0 +1,21 @@
+object Nested13 {
+
+ abstract class D
+ case class E(e: Int) extends D
+ case class F(d: D, f: Int) extends D
+
+ def foo(a : Int): Int = {
+
+ def rec1(d: D, j: Int): Int = d match {
+ case E(e) => j + e + a
+ case F(dNext, f) => f + rec1(dNext, j)
+ }
+
+ def rec2(d: D, i : Int) : Int = d match {
+ case E(e) => e
+ case F(dNext, f) => rec1(d, i)
+ }
+
+ rec2(F(E(2), 3), 0)
+ } ensuring(a + 5 == _)
+}
diff --git a/testcases/regression/valid/Nested14.scala b/testcases/regression/valid/Nested14.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba
--- /dev/null
+++ b/testcases/regression/valid/Nested14.scala
@@ -0,0 +1,11 @@
+object Nested14 {
+
+ def foo(i: Int): Int = {
+ def rec1(j: Int): Int = {
+ def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
+ rec2(j)
+ }
+ rec1(3)
+ } ensuring(0 == _)
+
+}
diff --git a/testcases/regression/valid/Nested2.scala b/testcases/regression/valid/Nested2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cc7220b02109c394e71c127e4cd3f53d6714ed7f
--- /dev/null
+++ b/testcases/regression/valid/Nested2.scala
@@ -0,0 +1,13 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested3.scala b/testcases/regression/valid/Nested3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..be6e6d04a335d12d079a9e3dc1a4b14ec0164014
--- /dev/null
+++ b/testcases/regression/valid/Nested3.scala
@@ -0,0 +1,15 @@
+object Nested3 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c
+ e
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested4.scala b/testcases/regression/valid/Nested4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea1e6066c6f4b7aaf6df23065e3011b86471b7f4
--- /dev/null
+++ b/testcases/regression/valid/Nested4.scala
@@ -0,0 +1,19 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ e
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/Nested5.scala b/testcases/regression/valid/Nested5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6ba128f415ecc3c61ebcccb42b65100d15373982
--- /dev/null
+++ b/testcases/regression/valid/Nested5.scala
@@ -0,0 +1,12 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+}
diff --git a/testcases/regression/valid/Nested6.scala b/testcases/regression/valid/Nested6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1c0220c0447dba10ccd710d60e5f19b1c1ec6e18
--- /dev/null
+++ b/testcases/regression/valid/Nested6.scala
@@ -0,0 +1,14 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(prop(a, b) && a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+ def prop(x: Int, y: Int): Boolean = x + y > 0
+
+}
diff --git a/testcases/regression/valid/Nested7.scala b/testcases/regression/valid/Nested7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62f5a567f49be174873a24711e630f69e8469a22
--- /dev/null
+++ b/testcases/regression/valid/Nested7.scala
@@ -0,0 +1,19 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c + bar(a) + bar(b) + bar(c)
+ }
+ rec1(2) + bar(a)
+ } ensuring(_ > 0)
+
+
+ def bar(x: Int): Int = {
+ require(x >= 0)
+ x
+ } ensuring(_ >= 0)
+
+}
diff --git a/testcases/regression/valid/Nested8.scala b/testcases/regression/valid/Nested8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e8a05e40e6cd1b2428e03bcf1a9f96c67797c698
--- /dev/null
+++ b/testcases/regression/valid/Nested8.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+object Nested8 {
+
+ def foo(a: Int): Int = {
+ require(a > 0)
+
+ def bar(b: Int): Int = {
+ if(a < b) {
+ def rec(c: Int): Int = {
+ require(c > 0)
+ c + b
+ } ensuring(_ > 0)
+ rec(2)
+ } else 3
+ }
+ bar(1)
+ } ensuring(_ > 0)
+
+ /*
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+ */
+
+}
diff --git a/testcases/regression/valid/Nested9.scala b/testcases/regression/valid/Nested9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3344a2c7973bed9da2c42208742c34c184b458ac
--- /dev/null
+++ b/testcases/regression/valid/Nested9.scala
@@ -0,0 +1,23 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ def rec2(f: Int): Int = {
+ require(f >= c)
+ f + e
+ } ensuring(_ > 0)
+ rec2(c+1)
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/valid/NestedVar.scala b/testcases/regression/valid/NestedVar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a26b7312b2f5f85509c6e55cc706fb29845202b1
--- /dev/null
+++ b/testcases/regression/valid/NestedVar.scala
@@ -0,0 +1,17 @@
+object NestedVar {
+
+ def foo(): Int = {
+ val a = 3
+ def rec(x: Int): Int = {
+ var b = 3
+ var c = 3
+ if(x > 0)
+ b = 2
+ else
+ c = 2
+ c+b
+ }
+ rec(a)
+ } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/Unit1.scala b/testcases/regression/valid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7b890d762648cba480c817506c7eee22259860d
--- /dev/null
+++ b/testcases/regression/valid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(_ == ())
+
+}
diff --git a/testcases/regression/valid/Unit2.scala b/testcases/regression/valid/Unit2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac659589af503a8a79f261f9eb05be095e2e0943
--- /dev/null
+++ b/testcases/regression/valid/Unit2.scala
@@ -0,0 +1,7 @@
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(_ == ())
+
+}
diff --git a/testcases/testgen/Abs.scala b/testcases/testgen/Abs.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4aa8307c8ec3da1d9ff941994b084d8590ce3afc
--- /dev/null
+++ b/testcases/testgen/Abs.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+import leon.Annotations._
+
+object Abs {
+
+ @main
+ def abs(x: Int): Int = {
+ if(x < 0) -x else x
+ } ensuring(_ >= 0)
+
+}
diff --git a/testcases/testgen/Abs2.scala b/testcases/testgen/Abs2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d640f941bf299ce06e0e84e40e2a2f98c39a4c4c
--- /dev/null
+++ b/testcases/testgen/Abs2.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+import leon.Annotations._
+
+object Abs2 {
+
+ @main
+ def f(x: Int): Int = if(x < 0) g(-x) else g(x)
+
+ def g(y: Int): Int = if(y < 0) -y else y
+
+}
diff --git a/testcases/testgen/Diamond.scala b/testcases/testgen/Diamond.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dbd354e94ffe82de38d7a83997fa1553189f7c0b
--- /dev/null
+++ b/testcases/testgen/Diamond.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Diamond {
+
+ def foo(x: Int): Int = waypoint(1, if(x < 0) bar(x) else bar(x))
+
+ def bar(y: Int): Int = if(y > 5) y else -y
+
+}
diff --git a/testcases/testgen/Imp.scala b/testcases/testgen/Imp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8257e6619ca299a8e56fd3d78076c54f8b731882
--- /dev/null
+++ b/testcases/testgen/Imp.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+import leon.Annotations._
+
+object Imp {
+
+ @main
+ def foo(i: Int): Int = {
+ var a = 0
+ a = a + 3
+ if(i < a)
+ a = a + 1
+ else
+ a = a - 1
+ a
+ } ensuring(_ >= 0)
+
+}
diff --git a/testcases/testgen/ImpWaypoint.scala b/testcases/testgen/ImpWaypoint.scala
new file mode 100644
index 0000000000000000000000000000000000000000..932d362b6faada0d8acf684d96d6bcaada0cca21
--- /dev/null
+++ b/testcases/testgen/ImpWaypoint.scala
@@ -0,0 +1,20 @@
+
+import leon.Utils._
+import leon.Annotations._
+
+object Imp {
+
+ @main
+ def foo(i: Int): Int = {
+ var a = 0
+ a = a + 3
+ if(i < a)
+ waypoint(1, a = a + 1)
+ else
+ a = a - 1
+ a
+ } ensuring(_ >= 0)
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b21928d924998d5dcd89ea2c278928c77aecf46a
--- /dev/null
+++ b/testcases/testgen/List.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+import leon.Annotations._
+
+object List {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ @main
+ def size(l: List): Int = (l match {
+ case Cons(_, tail) => sizeTail(tail, 1)
+ case Nil() => 0
+ }) ensuring(_ >= 0)
+
+ def sizeTail(l2: List, acc: Int): Int = l2 match {
+ case Cons(_, tail) => sizeTail(tail, acc+1)
+ case Nil() => acc
+ }
+}
diff --git a/testcases/testgen/MultiCall.scala b/testcases/testgen/MultiCall.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6742cc4ca224b8bef044745dc6cd12d60683ac80
--- /dev/null
+++ b/testcases/testgen/MultiCall.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+import leon.Annotations._
+
+object MultiCall {
+
+ @main
+ def a(i: Int): Int = if(i < 0) b(i) else c(i)
+
+ def b(j: Int): Int = if(j == -5) d(j) else e(j)
+ def c(k: Int): Int = if(k == 5) d(k) else e(k)
+
+ def d(l: Int): Int = l
+ def e(m: Int): Int = m
+
+}
diff --git a/testcases/testgen/Sum.scala b/testcases/testgen/Sum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5f1c6c481f36d195f1fe6d58c591a5d91918871b
--- /dev/null
+++ b/testcases/testgen/Sum.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+import leon.Annotations._
+
+object Sum {
+
+ @main
+ def sum(n: Int): Int = {
+ if(n <= 0) waypoint(4, 0) else waypoint(3, waypoint(2, n + sum(n-1)))
+ } ensuring(_ >= 0)
+
+}