From 076f7ee12059aeb08c7f4c007f948d90ee526353 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 29 Oct 2012 20:48:27 +0100
Subject: [PATCH] Integrated testing.
---
src/main/scala/leon/Reporter.scala | 59 +++++-----
.../purescala/invalid/InsertionSort.scala | 42 +++++++
.../purescala/invalid/ListOperations.scala | 107 ++++++++++++++++++
.../invalid/PropositionalLogic.scala | 86 ++++++++++++++
.../verification/purescala/invalid/README | 2 +
.../purescala/invalid/RedBlackTree.scala | 102 +++++++++++++++++
.../purescala/valid/AssociativeList.scala | 4 +-
.../purescala/valid/InsertionSort.scala | 13 ---
.../purescala/valid/ListOperations.scala | 4 -
.../purescala/valid/PropositionalLogic.scala | 11 --
.../purescala/valid/RedBlackTree.scala | 19 ----
.../scala/leon/test/PureScalaPrograms.scala | 84 ++++++++++++++
src/test/scala/leon/test/ValidPrograms.scala | 48 --------
13 files changed, 456 insertions(+), 125 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/README
create mode 100644 src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
create mode 100644 src/test/scala/leon/test/PureScalaPrograms.scala
delete mode 100644 src/test/scala/leon/test/ValidPrograms.scala
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 814c4352a..81ed31be8 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -5,20 +5,31 @@ import purescala.Trees.Expr
import purescala.PrettyPrinter
abstract class Reporter {
- def error(msg: Any) : Unit
- def warning(msg: Any) : Unit
- def info(msg: Any) : Unit
- def fatalError(msg: Any) : Nothing
+ def infoFunction(msg: Any) : Unit
+ def warningFunction(msg: Any) : Unit
+ def errorFunction(msg: Any) : Unit
+ def fatalErrorFunction(msg: Any) : Nothing
- def error(definition: Definition, msg: Any) : Unit = error(msg)
- def warning(definition: Definition, msg: Any) : Unit = warning(msg)
- def info(definition: Definition, msg: Any) : Unit = info(msg)
- def fatalError(definition: Definition, msg: Any) : Nothing = fatalError(msg)
+ // This part of the implementation is non-negociable.
+ private var _errorCount : Int = 0
+ private var _warningCount : Int = 0
- def error(expr: Expr, msg: Any) : Unit = error(msg)
- def warning(expr: Expr, msg: Any) : Unit = warning(msg)
- def info(expr: Expr, msg: Any) : Unit = info(msg)
- def fatalError(expr: Expr, msg: Any) : Nothing = fatalError(msg)
+ final def errorCount : Int = _errorCount
+ final def warningCount : Int = _warningCount
+
+ final def info(msg: Any) = infoFunction(msg)
+ final def warning(msg: Any) = {
+ _warningCount += 1
+ warningFunction(msg)
+ }
+ final def error(msg: Any) = {
+ _errorCount += 1
+ errorFunction(msg)
+ }
+ final def fatalError(msg: Any) = {
+ _errorCount += 1
+ fatalErrorFunction(msg)
+ }
}
class DefaultReporter extends Reporter {
@@ -39,26 +50,18 @@ class DefaultReporter extends Reporter {
msg.trim.replaceAll("\n", "\n" + (" " * (pfx.size)))
}
- def error(msg: Any) = output(reline(errorPfx, msg.toString))
- def warning(msg: Any) = output(reline(warningPfx, msg.toString))
- def info(msg: Any) = output(reline(infoPfx, msg.toString))
- def fatalError(msg: Any) = { output(reline(fatalPfx, msg.toString)); sys.exit(0) }
- override def error(definition: Definition, msg: Any) = output(reline(errorPfx, PrettyPrinter(definition) + "\n" + msg.toString))
- override def warning(definition: Definition, msg: Any) = output(reline(warningPfx, PrettyPrinter(definition) + "\n" + msg.toString))
- override def info(definition: Definition, msg: Any) = output(reline(infoPfx, PrettyPrinter(definition) + "\n" + msg.toString))
- override def fatalError(definition: Definition, msg: Any) = { output(reline(fatalPfx, PrettyPrinter(definition) + "\n" + msg.toString)); sys.exit(0) }
- override def error(expr: Expr, msg: Any) = output(reline(errorPfx, PrettyPrinter(expr) + "\n" + msg.toString))
- override def warning(expr: Expr, msg: Any) = output(reline(warningPfx, PrettyPrinter(expr) + "\n" + msg.toString))
- override def info(expr: Expr, msg: Any) = output(reline(infoPfx, PrettyPrinter(expr) + "\n" + msg.toString))
- override def fatalError(expr: Expr, msg: Any) = { output(reline(fatalPfx, PrettyPrinter(expr) + "\n" + msg.toString)); sys.exit(0) }
+ def errorFunction(msg: Any) = output(reline(errorPfx, msg.toString))
+ def warningFunction(msg: Any) = output(reline(warningPfx, msg.toString))
+ def infoFunction(msg: Any) = output(reline(infoPfx, msg.toString))
+ def fatalErrorFunction(msg: Any) = { output(reline(fatalPfx, msg.toString)); sys.exit(0) }
}
class QuietReporter extends DefaultReporter {
- override def warning(msg : Any) = {}
- override def info(msg : Any) = {}
+ override def warningFunction(msg : Any) = {}
+ override def infoFunction(msg : Any) = {}
}
class SilentReporter extends QuietReporter {
- override def error(msg : Any) = {}
- override def fatalError(msg : Any) = throw new Exception("Fatal error: " + msg.toString)
+ override def errorFunction(msg : Any) = {}
+ override def fatalErrorFunction(msg : Any) = throw new Exception("Fatal error: " + msg.toString)
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
new file mode 100644
index 000000000..fd9d8d7b6
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
@@ -0,0 +1,42 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: Int) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def buggySortedIns(e: Int, l: List): List = {
+ // require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
new file mode 100644
index 000000000..a4fc4f8dc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/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/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
new file mode 100644
index 000000000..a35c3ef9b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: Int) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def vars(f: Formula): Set[Int] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[Int](i)
+ case Literal(i) => Set[Int](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ // @induct
+ // def wrongCommutative(f: Formula) : Boolean = {
+ // nnf(simplify(f)) == simplify(nnf(f))
+ // } holds
+
+ @induct
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ } holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ } holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/README b/src/test/resources/regression/verification/purescala/invalid/README
new file mode 100644
index 000000000..3b276ff54
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/README
@@ -0,0 +1,2 @@
+This particular directory contains PureScala programs that have *at least* one
+failing verification condition.
diff --git a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
new file mode 100644
index 000000000..3baf9d015
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
@@ -0,0 +1,102 @@
+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)
+
+ 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)
+ }
+
+ 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 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 buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(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)))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
index f5a2fc041..0356d8ec0 100644
--- a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -29,9 +29,9 @@ object AssociativeList {
case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
}
- def update(l1: List, l2: List): List = (l2 match {
+ def updateAll(l1: List, l2: List): List = (l2 match {
case Nil() => l1
- case Cons(x, xs) => update(updateElem(l1, x), xs)
+ case Cons(x, xs) => updateAll(updateElem(l1, x), xs)
}) ensuring(domain(_) == domain(l1) ++ domain(l2))
def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index d2ae67b3b..a4fffee35 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -48,19 +48,6 @@ object InsertionSort {
&& size(res) == size(l) + 1
)
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def buggySortedIns(e: Int, l: List): List = {
- // require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
/* Insertion sort yields a sorted list of same size and content as the input
* list */
def sort(l: List): List = (l match {
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
index a4fc4f8dc..27541d9bd 100644
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -82,10 +82,6 @@ object ListOperations {
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
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
index a35c3ef9b..5dd7d5057 100644
--- a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -61,17 +61,6 @@ object PropositionalLogic {
def fv(f : Formula) = { vars(nnf(f)) }
- // @induct
- // def wrongCommutative(f: Formula) : Boolean = {
- // nnf(simplify(f)) == simplify(nnf(f))
- // } holds
-
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
- require(isNNF(f))
- isNNF(simplify(f))
- } holds
-
@induct
def nnfIsStable(f: Formula) : Boolean = {
require(isNNF(f))
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
index bc2de6ba9..65d873ad4 100644
--- a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -82,11 +82,6 @@ object RedBlackTree {
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) =>
@@ -100,18 +95,4 @@ object RedBlackTree {
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/src/test/scala/leon/test/PureScalaPrograms.scala b/src/test/scala/leon/test/PureScalaPrograms.scala
new file mode 100644
index 000000000..92fbb68eb
--- /dev/null
+++ b/src/test/scala/leon/test/PureScalaPrograms.scala
@@ -0,0 +1,84 @@
+package leon
+package test
+
+import leon.verification.{AnalysisPhase,VerificationReport}
+
+import org.scalatest.FunSuite
+
+import java.io.File
+
+class PureScalaPrograms extends FunSuite {
+ private var counter : Int = 0
+ private def nextInt() : Int = {
+ counter += 1
+ counter
+ }
+ private case class Output(report : VerificationReport, reporter : Reporter)
+
+ private def mkPipeline : Pipeline[List[String],VerificationReport] =
+ leon.plugin.ExtractionPhase andThen leon.verification.AnalysisPhase
+
+ private def mkTest(file : File)(block: Output=>Unit) = {
+ val fullName = file.getPath()
+ val start = fullName.indexOf("regression")
+ val displayName = if(start != -1) {
+ fullName.substring(start, fullName.length)
+ } else {
+ fullName
+ }
+
+ test("PureScala program %3d: [%s]".format(nextInt(), displayName)) {
+ assert(file.exists && file.isFile && file.canRead,
+ "Benchmark [%s] is not a readable file".format(displayName))
+
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = false,
+ xlang = false,
+ verify = true
+ ),
+ files = List(file),
+ reporter = new SilentReporter
+ )
+
+ val pipeline = mkPipeline
+
+ val report = pipeline.run(ctx)("--timeout=2" :: file.getPath :: Nil)
+
+ block(Output(report, ctx.reporter))
+ }
+ }
+
+ private def forEachFileIn(dirName : String)(block : Output=>Unit) {
+ import scala.collection.JavaConversions._
+
+ val dir = this.getClass.getClassLoader.getResource(dirName)
+
+ if(dir == null || dir.getProtocol != "file") {
+ assert(false, "Tests have to be run from within `sbt`, for otherwise " +
+ "the test files will be harder to access (and we dislike that).")
+ }
+
+ for(f <- (new File(dir.toURI())).listFiles() if f.getPath().endsWith(".scala")) {
+ mkTest(f)(block)
+ }
+ }
+
+ forEachFileIn("regression/verification/purescala/valid") { output =>
+ val Output(report, reporter) = output
+ assert(report.totalConditions === report.totalValid,
+ "All verification conditions should be valid.")
+ assert(reporter.errorCount === 0)
+ assert(reporter.warningCount === 0)
+ }
+
+ forEachFileIn("regression/verification/purescala/invalid") { output =>
+ val Output(report, reporter) = output
+ assert(report.totalInvalid > 0,
+ "There should be at least one invalid verification condition.")
+ assert(report.totalUnknown === 0,
+ "There should not be unknown verification conditions.")
+ assert(reporter.errorCount >= report.totalInvalid)
+ assert(reporter.warningCount === 0)
+ }
+}
diff --git a/src/test/scala/leon/test/ValidPrograms.scala b/src/test/scala/leon/test/ValidPrograms.scala
deleted file mode 100644
index 37df60f22..000000000
--- a/src/test/scala/leon/test/ValidPrograms.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-package leon
-package test
-
-import org.scalatest.FunSuite
-
-import java.io.File
-
-class ValidPrograms extends FunSuite {
- def runBasicLeonOnFile(filename : String) : Unit = {
- val file = new File(filename)
-
- assert(file.exists && file.isFile && file.canRead,
- "Benchmark [%s] is not a readable file".format(filename))
-
- val ctx = LeonContext(
- settings = Settings(
- synthesis = false,
- xlang = false,
- verify = true
- ),
- files = List(file),
- reporter = new SilentReporter
- )
-
- val pipeline = Main.computePipeline(ctx.settings)
- pipeline.run(ctx)("--timeout=2" :: file.getPath :: Nil)
- }
-
- def mkTest(filename : String) = {
- test("Valid PureScala program: [%s]".format(filename)) {
- runBasicLeonOnFile(filename)
- assert(true)
- }
- }
-
- test("List files") {
- import scala.collection.JavaConversions._
-
- val ress = this.getClass.getClassLoader.getResources("/regression/verification/purescala/valid/")
-
- for(res <- ress) {
- println(res)
- }
- }
-
- // Sorry for leaving this there...
- // mkTest("/home/psuter/Test.scala")
-}
--
GitLab