From 4c7364b8f326399ed7cd3d9fee0943903b42634e Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 15 Jun 2013 18:51:45 +0200
Subject: [PATCH] Added automatic testing to termination framework and
corrected some small issues in the ChainProcessor system. Some tests ending
in .BAK should be runnable but can't for now because of a memory leak
somewhere in the framework.
---
.../scala/leon/termination/ChainBuilder.scala | 13 ++
.../leon/termination/ChainProcessor.scala | 44 +++---
.../leon/termination/LoopProcessor.scala | 2 +-
.../scala/leon/termination/Processor.scala | 14 +-
.../leon/termination/RelationProcessor.scala | 2 -
.../termination/looping/Looping1.scala.BAK | 33 +++++
.../termination/looping/Looping2.scala.BAK | 32 +++++
.../termination/looping/Looping3.scala.BAK | 32 +++++
.../termination/looping/Numeric1.scala | 11 ++
.../termination/looping/Numeric2.scala | 13 ++
.../looping/Termination_failling1.scala | 22 +++
.../termination/unknown/Numeric3.scala | 8 ++
.../termination/valid/BinaryTreeImp.scala | 101 +++++++++++++
.../termination/valid/BubbleSort.scala | 74 ++++++++++
.../termination/valid/ComplexChains.scala | 26 ++++
.../termination/valid/Fibonacci.scala | 15 ++
.../termination/valid/HardChains.scala.BAK | 37 +++++
.../termination/valid/ListWithSize.scala | 135 ++++++++++++++++++
.../termination/valid/Numeric1.scala | 11 ++
.../termination/valid/QuickSort.scala | 58 ++++++++
.../termination/valid/RedBlackTree.scala | 59 ++++++++
.../termination/valid/SimpInterpret.scala | 67 +++++++++
.../valid/Termination_passing1.scala | 23 +++
.../valid/Termination_passing2.scala | 20 +++
.../termination/TerminationRegression.scala | 109 ++++++++++++++
25 files changed, 929 insertions(+), 32 deletions(-)
create mode 100644 src/test/resources/regression/termination/looping/Looping1.scala.BAK
create mode 100644 src/test/resources/regression/termination/looping/Looping2.scala.BAK
create mode 100644 src/test/resources/regression/termination/looping/Looping3.scala.BAK
create mode 100644 src/test/resources/regression/termination/looping/Numeric1.scala
create mode 100644 src/test/resources/regression/termination/looping/Numeric2.scala
create mode 100644 src/test/resources/regression/termination/looping/Termination_failling1.scala
create mode 100644 src/test/resources/regression/termination/unknown/Numeric3.scala
create mode 100644 src/test/resources/regression/termination/valid/BinaryTreeImp.scala
create mode 100644 src/test/resources/regression/termination/valid/BubbleSort.scala
create mode 100644 src/test/resources/regression/termination/valid/ComplexChains.scala
create mode 100644 src/test/resources/regression/termination/valid/Fibonacci.scala
create mode 100644 src/test/resources/regression/termination/valid/HardChains.scala.BAK
create mode 100644 src/test/resources/regression/termination/valid/ListWithSize.scala
create mode 100644 src/test/resources/regression/termination/valid/Numeric1.scala
create mode 100644 src/test/resources/regression/termination/valid/QuickSort.scala
create mode 100644 src/test/resources/regression/termination/valid/RedBlackTree.scala
create mode 100644 src/test/resources/regression/termination/valid/SimpInterpret.scala
create mode 100644 src/test/resources/regression/termination/valid/Termination_passing1.scala
create mode 100644 src/test/resources/regression/termination/valid/Termination_passing2.scala
create mode 100644 src/test/scala/leon/test/termination/TerminationRegression.scala
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 065c54db8..741b7c2b6 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -6,7 +6,20 @@ import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.Common._
+object ChainID {
+ private var counter: Int = 0
+ def get: Int = {
+ counter = counter + 1
+ counter
+ }
+}
+
final case class Chain(chain: List[Relation]) {
+ val id = ChainID.get
+
+ override def equals(obj: Any): Boolean = obj.isInstanceOf[Chain] && obj.asInstanceOf[Chain].id == id
+ override def hashCode(): Int = id
+
def funDef : FunDef = chain.head.funDef
def funDefs : Set[FunDef] = chain.map(_.funDef) toSet
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index e50ab2e2a..06c98ed31 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -16,31 +16,33 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
ChainComparator.init
def run(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = {
+ import scala.collection.mutable.{Map => MutableMap}
reporter.info("- Running ChainProcessor")
val allChainMap : Map[FunDef, Set[Chain]] = problem.funDefs.map(funDef => funDef -> ChainBuilder.run(funDef)).toMap
reporter.info("- Computing all possible Chains")
- val possibleChainMap : Map[FunDef, Set[Chain]] = allChainMap.mapValues(chains => chains.filter(chain => isSAT(And(chain.loop()))))
+ var counter = 0
+ val possibleChainMap : Map[FunDef, Set[Chain]] = allChainMap.mapValues(chains => chains.filter(chain => isWeakSAT(And(chain.loop()))))
reporter.info("- Collecting re-entrant Chains")
- val reentrantChainMap : Map[FunDef, Set[Chain]] = possibleChainMap.mapValues(chains => chains.filter(chain => isSAT(And(chain reentrant chain))))
+ val reentrantChainMap : Map[FunDef, Set[Chain]] = possibleChainMap.mapValues(chains => chains.filter(chain => isWeakSAT(And(chain reentrant chain))))
// We build a cross-chain map that determines which chains can reenter into another one after a loop.
// Note: We are also checking reentrance SAT here, so again, we negate the formula!
reporter.info("- Computing cross-chain map")
- val crossChains : Map[Chain, Set[Chain]] = possibleChainMap.map({ case (funDef, chains) =>
+ val crossChains : Map[Chain, Set[Chain]] = possibleChainMap.toSeq.map({ case (funDef, chains) =>
val reentrant = reentrantChainMap(funDef)
- val reentrantPairs = reentrant.map(chain => chain -> Set(chain))
- val crosswise = (chains -- reentrant).map(chain => chain -> {
- reentrant.filter(other => isSAT(And(chain reentrant other)))
+ chains.map(chain => chain -> {
+ val cross = (reentrant - chain).filter(other => isWeakSAT(And(chain reentrant other)))
+ val self = if (reentrant(chain)) Set(chain) else Set()
+ cross ++ self
})
- reentrantPairs ++ crosswise
}).flatten.toMap
- val validChainMap : Map[FunDef, Set[Chain]] = possibleChainMap.map({ case (funDef, chains) => funDef -> chains.filter(crossChains(_).nonEmpty) })
+ val validChainMap : Map[FunDef, Set[Chain]] = possibleChainMap.map({ case (funDef, chains) => funDef -> chains.filter(crossChains(_).nonEmpty) }).toMap
// We use the cross-chains to build chain clusters. For each cluster, we must prove that the SAME argument
// decreases in each of the chains in the cluster!
- reporter.info("- Building initial cluster estimation by fix-point iteration")
- val generalClusters : Map[FunDef, Set[Set[Chain]]] = {
+ reporter.info("- Building cluster estimation by fix-point iteration")
+ val clusters : Map[FunDef, Set[Set[Chain]]] = {
def cluster(set: Set[Chain]): Set[Chain] = {
set ++ set.map(crossChains(_)).flatten
}
@@ -50,6 +52,14 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
if (a == na) a else fix(f, na)
}
+ def reduceClusters(all: List[Set[Chain]]): List[Set[Chain]] = {
+ all.map(cluster => cluster.toSeq.sortBy(_.size).foldLeft(Set[Chain]())({ case (acc, chain) =>
+ val chainElements : Set[Relation] = chain.chain.toSet
+ val seenElements : Set[Relation] = acc.map(_.chain).flatten.toSet
+ if (chainElements -- seenElements nonEmpty) acc + chain else acc
+ })).filter(_.nonEmpty)
+ }
+
def filterClusters(all: List[Set[Chain]]): List[Set[Chain]] = if (all.isEmpty) Nil else {
val newCluster = all.head
val rest = all.tail.filter(set => !set.subsetOf(newCluster))
@@ -58,21 +68,14 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
def build(chains: Set[Chain]): Set[Set[Chain]] = {
val allClusters = chains.map(chain => fix(cluster, Set(chain)))
- filterClusters(allClusters.toList.sortBy(- _.size)).toSet
+ val reducedClusters = reduceClusters(allClusters.toList)
+ val filteredClusters = filterClusters(reducedClusters.sortBy(- _.size))
+ filteredClusters.toSet
}
validChainMap.map({ case (funDef, chains) => funDef -> build(chains) })
}
- reporter.info("- Trimming down to final clusters")
- val clusters : Map[FunDef, Set[Set[Chain]]] = generalClusters.map({ case (funDef, clusters) =>
- funDef -> clusters.map(cluster => cluster.toSeq.sortBy(_.size).foldLeft(Set[Chain]())({ case (acc, chain) =>
- val chainElements : Set[Relation] = chain.chain.toSet
- val seenElements : Set[Relation] = acc.map(_.chain).flatten.toSet
- if (chainElements -- seenElements nonEmpty) acc + chain else acc
- })).filter(_.nonEmpty)
- })
-
reporter.info("- Strengthening postconditions")
strengthenPostconditions(problem.funDefs)
@@ -96,7 +99,6 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
(fd, clusters.map(cluster => cluster -> gen(fd, cluster)))
})
- initSolvers // add structural size functions to solver
formulas.map({ case (fd, clustersWithFormulas) =>
fd -> clustersWithFormulas.filter({ case (cluster, formula) => !isAlwaysSAT(formula) }).map(_._1)
})
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index 5f0c6db3c..a45cc3c7d 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -14,7 +14,7 @@ class LoopProcessor(checker: TerminationChecker, k: Int = 10) extends Processor(
def run(problem: Problem) = {
val allChains : Set[Chain] = problem.funDefs.map(fd => ChainBuilder.run(fd)).flatten
// Get reentrant loops (see ChainProcessor for more details)
- val chains : Set[Chain] = allChains.filter(chain => isSAT(And(chain reentrant chain)))
+ val chains : Set[Chain] = allChains.filter(chain => isWeakSAT(And(chain reentrant chain)))
val nonTerminating = chains.flatMap({ chain =>
val freshArgs : Seq[Expr] = chain.funDef.args.map(arg => arg.id.freshen.toVariable)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 95ec075f5..299d5b338 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -78,7 +78,7 @@ trait Solvable { self: Processor =>
def strengthenPostconditions(funDefs: Set[FunDef]) = Solvable.strengthenPostconditions(funDefs)(this)
- def initSolvers {
+ private def initSolvers {
val program : Program = self.checker.program
val allDefs : Seq[Definition] = program.mainObject.defs ++ StructuralSize.defs
val newProgram : Program = program.copy(mainObject = program.mainObject.copy(defs = allDefs))
@@ -92,7 +92,7 @@ trait Solvable { self: Processor =>
type Solution = (Option[Boolean], Map[Identifier, Expr])
private def solve(problem: Expr): Solution = {
- if (solvers == null) initSolvers
+ initSolvers
// drop functions from constraints that might not terminate (and may therefore
// make Leon unroll them forever...)
val dangerousCallsMap : Map[Expr, Expr] = functionCallsOf(problem).collect({
@@ -123,13 +123,11 @@ trait Solvable { self: Processor =>
solvers.collectFirst({ case Solved(s, model) => (s, model) }) getOrElse (None, Map())
}
- def isSAT(problem: Expr): Boolean = {
- solve(problem)._1 getOrElse false
- }
+ def isStrongSAT(problem: Expr): Boolean = solve(problem)._1 getOrElse false
- def isAlwaysSAT(problem: Expr): Boolean = {
- solve(Not(problem))._1.map(!_) getOrElse false
- }
+ def isWeakSAT(problem: Expr): Boolean = solve(problem)._1 getOrElse true
+
+ def isAlwaysSAT(problem: Expr): Boolean = solve(Not(problem))._1.map(!_) getOrElse false
def getModel(problem: Expr): Option[Map[Identifier, Expr]] = {
val solution = solve(problem)
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 2f094c838..4f2786528 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -35,8 +35,6 @@ class RelationProcessor(checker: TerminationChecker) extends Processor(checker)
case class Dep(deps: Set[FunDef]) extends Result
case object Failure extends Result
- initSolvers
-
val decreasing = formulas.map({ case (fd, formulas) =>
val solved = formulas.map({ case (fid, (gt, ge)) =>
if(isAlwaysSAT(gt)) Success
diff --git a/src/test/resources/regression/termination/looping/Looping1.scala.BAK b/src/test/resources/regression/termination/looping/Looping1.scala.BAK
new file mode 100644
index 000000000..b21e705bf
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Looping1.scala.BAK
@@ -0,0 +1,33 @@
+import leon.Utils._
+
+object ComplexChains {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def looping1(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => looping2(tail)
+ case Cons(head, tail) if head < 0 => looping3(tail)
+ case _ => looping4(Cons(1, list))
+ }
+
+ def looping2(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => looping1(tail)
+ case _ => looping4(list)
+ }
+
+ def looping3(list: List): List = list match {
+ case Cons(head, tail) if head < 0 => looping1(tail)
+ case _ => looping2(Cons(1, list))
+ }
+
+ def looping4(list: List): List = list match {
+ case Cons(head, tail) if head == 0 => looping4(tail)
+ case Cons(_, Cons(_, tail)) => looping1(Cons(1, list))
+ case Cons(_, tail) => looping3(Nil())
+ case Nil() => Nil()
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Looping2.scala.BAK b/src/test/resources/regression/termination/looping/Looping2.scala.BAK
new file mode 100644
index 000000000..fc1da261e
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Looping2.scala.BAK
@@ -0,0 +1,32 @@
+import leon.Utils._
+
+object ComplexChains {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def looping1(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => calling2(list)
+ case Cons(head, tail) if head < 0 => calling3(list)
+ case _ => looping4(Cons(1, list))
+ }
+
+ def calling2(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => looping1(tail)
+ case _ => looping4(list)
+ }
+
+ def calling3(list: List): List = list match {
+ case Cons(head, tail) if head < 0 => looping1(tail)
+ case _ => looping4(list)
+ }
+
+ def looping4(list: List): List = list match {
+ case Cons(_, Cons(_, tail)) => looping1(tail)
+ case Cons(_, tail) => looping1(tail)
+ case Nil() => calling2(Cons(1, Nil()))
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Looping3.scala.BAK b/src/test/resources/regression/termination/looping/Looping3.scala.BAK
new file mode 100644
index 000000000..c6d81a758
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Looping3.scala.BAK
@@ -0,0 +1,32 @@
+import leon.Utils._
+
+object ComplexChains {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def looping1(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => looping2(list)
+ case Cons(head, tail) if head < 0 => looping3(list)
+ case _ => looping4(Cons(1, list))
+ }
+
+ def looping2(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => looping1(tail)
+ case _ => looping3(list)
+ }
+
+ def looping3(list: List): List = list match {
+ case Cons(head, tail) if head < 0 => looping1(tail)
+ case _ => looping2(list)
+ }
+
+ def looping4(list: List): List = list match {
+ case Cons(_, Cons(_, tail)) => looping1(tail)
+ case Cons(_, tail) => looping1(tail)
+ case Nil() => looping2(Cons(1, Nil()))
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Numeric1.scala b/src/test/resources/regression/termination/looping/Numeric1.scala
new file mode 100644
index 000000000..6949040ed
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Numeric1.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Numeric {
+ // division by 0 loops
+ def looping(x: Int, y: Int): Int = {
+ if (x < y) 0
+ else 1 + looping(x - y, y)
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Numeric2.scala b/src/test/resources/regression/termination/looping/Numeric2.scala
new file mode 100644
index 000000000..0d5c2c04f
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Numeric2.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Numeric {
+ def looping1(x: Int): Int = looping2(x - 1)
+
+ def looping2(x: Int): Int = looping3(x - 1)
+
+ def looping3(x: Int): Int = looping4(x - 1)
+
+ def looping4(x: Int): Int = looping1(x + 3)
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Termination_failling1.scala b/src/test/resources/regression/termination/looping/Termination_failling1.scala
new file mode 100644
index 000000000..4904c9fc5
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Termination_failling1.scala
@@ -0,0 +1,22 @@
+import leon.Utils._
+
+object Termination {
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def looping1(list: List) : Int = looping2(list)
+
+ def looping2(list: List) : Int = looping1(list)
+
+ def calling1(list: List, b: Boolean) : Int = if(b) calling2(list) else looping1(list)
+
+ def calling2(list: List) : Int = list match {
+ case Cons(head, tail) => calling1(tail, true)
+ case Nil() => 0
+ }
+
+ def ok(list: List) : Int = 0
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/unknown/Numeric3.scala b/src/test/resources/regression/termination/unknown/Numeric3.scala
new file mode 100644
index 000000000..fd99e3132
--- /dev/null
+++ b/src/test/resources/regression/termination/unknown/Numeric3.scala
@@ -0,0 +1,8 @@
+import leon.Utils._
+
+object Numeric3 {
+ def unknown(x: Int) : Int = if (x > 0) unknown(x - 1) else unknown(5)
+}
+
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
new file mode 100644
index 000000000..3005d1991
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
@@ -0,0 +1,101 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+
+ sealed abstract class Tree
+ case class Leaf() extends Tree
+ case class Node(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 Leaf() => Set.empty
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Leaf() => 0
+ case Node(l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ def binaryTreeProp(t: Tree): Boolean = t match {
+ case Leaf() => true
+ case Node(left, value, right) => {
+ val b1 = left match {
+ case Leaf() => true
+ case Node(a,b,c) => value >= treeMax(Node(a,b,c))
+ }
+ val b2 = right match {
+ case Leaf() => true
+ case Node(a,b,c) => value <= treeMin(Node(a,b,c))
+ }
+ binaryTreeProp(left) && binaryTreeProp(right) && b1 && b2
+ }
+ }
+
+ def treeMin(tree: Node): Int = {
+ require(binaryTreeProp(tree))
+ tree match {
+ case Node(left, value, _) => left match {
+ case Leaf() => value
+ case Node(l, v, r) => treeMin(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+ //def treeMin(tree: Node): Int = {
+ // require(binaryTreeProp(tree))
+ // val Node(left, value, _) = tree
+ // var res = value
+ // var tmpLeft = left
+ // (while(!tmpLeft.isInstanceOf[Leaf]) {
+ // val Node(left, value, _) = tmpLeft
+ // res = value
+ // tmpLeft = left
+ // }) invariant(content(tmpLeft).contains(res))
+ // res
+ //} ensuring(content(tree).contains(_))
+
+ def treeMax(tree: Node): Int = {
+ require(binaryTreeProp(tree))
+ tree match {
+ case Node(_, v, right) => right match {
+ case Leaf() => v
+ case Node(l, v, r) => treeMax(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+
+ def search(t: Tree, x: Int): Boolean = {
+ require(binaryTreeProp(t))
+ t match {
+ case Leaf() => false
+ case Node(left, value, right) =>
+ if(value == x) true
+ else if(value < x) search(right, x)
+ else search(left, x)
+ }
+ } ensuring(res => res == content(t).contains(x))
+
+ def searchImp(t: Tree, x: Int): Boolean = {
+ require(binaryTreeProp(t))
+ var res = false
+ var t2: Tree = t
+ (while(!t2.isInstanceOf[Leaf]) {
+ val Node(left, value, right) = t2
+ if(value == x)
+ res = true
+ else if(value < x)
+ t2 = right
+ else
+ t2 = left
+ })
+ res
+ } ensuring(res => res == content(t).contains(x))
+
+}
diff --git a/src/test/resources/regression/termination/valid/BubbleSort.scala b/src/test/resources/regression/termination/valid/BubbleSort.scala
new file mode 100644
index 000000000..3551ebf16
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/BubbleSort.scala
@@ -0,0 +1,74 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object BubbleSort {
+
+ 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 &&
+ 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 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
+ }
+
+ 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
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/termination/valid/ComplexChains.scala b/src/test/resources/regression/termination/valid/ComplexChains.scala
new file mode 100644
index 000000000..568e09bb1
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/ComplexChains.scala
@@ -0,0 +1,26 @@
+import leon.Utils._
+
+object ComplexChains {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def f1(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => f2(Cons(1, list))
+ case Cons(head, tail) if head < 0 => f3(Cons(-1, list))
+ case Cons(head, tail) => f1(tail)
+ case Nil() => Nil()
+ }
+
+ def f2(list: List): List = f3(Cons(0, list))
+
+ def f3(list: List): List = f1(list match {
+ case Cons(head, Cons(head2, Cons(head3, tail))) => tail
+ case Cons(head, Cons(head2, tail)) => tail
+ case Cons(head, tail) => tail
+ case Nil() => Nil()
+ })
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/Fibonacci.scala b/src/test/resources/regression/termination/valid/Fibonacci.scala
new file mode 100644
index 000000000..f2140e54d
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/Fibonacci.scala
@@ -0,0 +1,15 @@
+object Fibonacci {
+ def fib(x: Int) : Int = {
+ require(x >= 0)
+ if(x < 2) {
+ x
+ } else {
+ fib(x - 1) + fib(x - 2)
+ }
+ }
+
+ // requires that fib is universally quantified to work...
+ def check() : Boolean = {
+ fib(5) == 5
+ } ensuring(_ == true)
+}
diff --git a/src/test/resources/regression/termination/valid/HardChains.scala.BAK b/src/test/resources/regression/termination/valid/HardChains.scala.BAK
new file mode 100644
index 000000000..4ffe63f60
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/HardChains.scala.BAK
@@ -0,0 +1,37 @@
+import leon.Utils._
+
+object HardChains {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def f1(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => f2(list)
+ case Cons(head, tail) if head < 0 => f3(list)
+ case Nil() => Nil()
+ case _ => f4(list)
+ }
+
+ def f2(list: List): List = list match {
+ case Cons(head, tail) if head > 0 => f4(Cons(0, list))
+ case _ => f1(list)
+ }
+
+ def f3(list: List): List = list match {
+ case Cons(head, tail) if head < 0 => f4(Cons(0, list))
+ case Cons(head, tail) if head == 0 => f2(tail)
+ case _ => f4(list)
+ }
+
+ def f4(list: List): List = list match {
+ case Cons(head, tail) if head == 0 => f3(tail)
+ case Cons(head, Cons(head2, Cons(head3, tail))) => tail
+ case Cons(head, Cons(head2, tail)) => tail
+ case Cons(head, tail) if head > 0 => f4(Cons(0, tail))
+ case Cons(head, tail) => f4(tail)
+ case _ => f1(list)
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/ListWithSize.scala b/src/test/resources/regression/termination/valid/ListWithSize.scala
new file mode 100644
index 000000000..868cb4556
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/ListWithSize.scala
@@ -0,0 +1,135 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object ListWithSize {
+ 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
+
+ // proved with unrolling=0
+ 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))
+
+ // proved with unrolling=1
+ def funnyCons(x: Int, l: List) : List = (l match {
+ case Nil() => Cons(x, Nil())
+ case c @ Cons(_,_) => Cons(x, c)
+ }) ensuring(size(_) > 0)
+
+ // proved with unrolling=2
+ 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
+
+ // unclear if we needed this--it was meant to force folding
+ //def appendFold(x : Int, xs : List, ys : List) : Boolean = {
+ // true
+ //} ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys))
+
+ @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 reverse0exposed(l1 : List, l2 : List) : Boolean = {
+ (reverse0(l1, l2) == append(reverse(l1), l2))
+ } // holds
+
+ @induct
+ def sizeAppend(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
+ // proved with unrolling=4
+ @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))
+
+ def reverseConcat0(l1: List, l2: List) : Boolean = {
+ reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
+ } // holds
+
+ // proved with unrolling=2 ???
+ def reverseConcat(l1: List, l2: List) : Boolean = {
+ reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
+ } // holds
+}
diff --git a/src/test/resources/regression/termination/valid/Numeric1.scala b/src/test/resources/regression/termination/valid/Numeric1.scala
new file mode 100644
index 000000000..2c4f65137
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/Numeric1.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Numeric {
+
+ def f1(x: Int): Int = f2(x - 2)
+
+ def f2(x: Int): Int = if (x < 0) 0 else f1(x + 1)
+}
+
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/QuickSort.scala b/src/test/resources/regression/termination/valid/QuickSort.scala
new file mode 100644
index 000000000..83dd2c364
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/QuickSort.scala
@@ -0,0 +1,58 @@
+import scala.collection.immutable.Set
+
+object QuickSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def is_sorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x,Nil()) => true
+ case Cons(x,Cons(y,xs)) => x<=y && is_sorted(Cons(y,xs))
+ }
+
+ def rev_append(aList:List,bList:List): List = aList match {
+ case Nil() => bList
+ case Cons(x,xs) => rev_append(xs,Cons(x,bList))
+ }
+
+ def reverse(list:List): List = rev_append(list,Nil())
+
+ def append(aList:List,bList:List): List = aList match {
+ case Nil() => bList
+ case _ => rev_append(reverse(aList),bList)
+ }
+
+ def greater(n:Int,list:List) : List = list match {
+ case Nil() => Nil()
+ case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
+ }
+
+ def smaller(n:Int,list:List) : List = list match {
+ case Nil() => Nil()
+ case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
+ }
+
+ def equals(n:Int,list:List) : List = list match {
+ case Nil() => Nil()
+ case Cons(x,xs) => if (n==x) Cons(x,equals(n,xs)) else equals(n,xs)
+ }
+
+ def quickSort(list:List): List = (list match {
+ case Nil() => Nil()
+ case Cons(x,Nil()) => list
+ case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
+ }) ensuring(res => contents(res) == contents(list)) // && is_sorted(res))
+
+ def main(args: Array[String]): Unit = {
+ val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
+
+ println(ls)
+ println(quickSort(ls))
+ }
+}
diff --git a/src/test/resources/regression/termination/valid/RedBlackTree.scala b/src/test/resources/regression/termination/valid/RedBlackTree.scala
new file mode 100644
index 000000000..0952a11fe
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/RedBlackTree.scala
@@ -0,0 +1,59 @@
+import scala.collection.immutable.Set
+//import scala.collection.immutable.Multiset
+
+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
+
+ 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)
+ }
+
+ def ins(x : Int, t: Tree): Tree = (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) + 2)
+ ))
+
+ def add(x: Int, t: Tree): Tree = {
+ makeBlack(ins(x, t))
+ } ensuring (content(_) == content(t) ++ Set(x))
+
+ 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)))
+
+ def makeBlack(n: Tree): Tree = n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+
+ def flip(t : Tree) : Tree = t match {
+ case Empty() => Empty()
+ case Node(color,l,e,r) => Node(color,flip(r),e,flip(l))
+ }
+}
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
new file mode 100644
index 000000000..bcb7bafc8
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -0,0 +1,67 @@
+//import scala.collection.immutable.Set
+//import leon.Annotations._
+import leon.Utils._
+
+object Interpret {
+ abstract class BoolTree
+ case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
+ case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
+ case class Not(t : BoolTree) extends BoolTree
+
+ abstract class IntTree
+ case class Const(c:Int) extends IntTree
+ case class Var() extends IntTree
+ case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
+ case class Minus(t1 : IntTree, t2 : IntTree) extends IntTree
+ case class Less(t1 : IntTree, t2 : IntTree) extends BoolTree
+ case class If(cond : BoolTree, t : IntTree, e : IntTree) extends IntTree
+
+ def repOk(t : IntTree) : Boolean = {
+ true
+ }
+
+ def beval(t:BoolTree, x0 : Int) : Boolean = {
+ t match {
+ case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
+ case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
+ case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
+ case Not(t1) => !beval(t1,x0)
+ }
+ }
+
+ def ieval(t:IntTree, x0 : Int) : Int = {
+ t match {
+ case Const(c) => c
+ case Var() => x0
+ case Plus(t1,t2) => ieval(t1,x0) + ieval(t2,x0)
+ case Minus(t1, t2) => ieval(t1,x0) - ieval(t2,x0)
+ case If(c,t1,t2) => if (beval(c,x0)) ieval(t1,x0) else ieval(t2,x0)
+ }
+ }
+ def computesPositive(t : IntTree) : Boolean = {
+ ieval(t,0) >= 0 &&
+ ieval(t,1) >= 0 &&
+ ieval(t,-1) >= 0 &&
+ ieval(t,-2) >= 0 &&
+ ieval(t,2) >= 0
+ }
+ def identityForPositive(t : IntTree) : Boolean = {
+ ieval(t, 5) == 5 &&
+ ieval(t, 33) == 33 &&
+ ieval(t, 0) == 0 &&
+ ieval(t, -1) == 1 &&
+ ieval(t, -2) == 2
+ }
+
+ def treeBad(t : IntTree) : Boolean = {
+ !(repOk(t) && computesPositive(t) && identityForPositive(t))
+ } holds
+
+ def thereIsGoodTree() : Boolean = {
+ !treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
+ } holds
+
+ def main(args : Array[String]) {
+ thereIsGoodTree()
+ }
+}
diff --git a/src/test/resources/regression/termination/valid/Termination_passing1.scala b/src/test/resources/regression/termination/valid/Termination_passing1.scala
new file mode 100644
index 000000000..fffb8bca9
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/Termination_passing1.scala
@@ -0,0 +1,23 @@
+import leon.Utils._
+
+object Termination {
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil extends List
+
+ def f1(list: List) : Int = f2(list)
+
+ def f2(list: List) : Int = list match {
+ case Cons(head, tail) => f1(tail)
+ case Nil() => 0
+ }
+
+ def f3(list: List, b: Boolean) : Int = if(b) f4(list) else f1(list)
+
+ def f4(list: List) : Int = list match {
+ case Cons(head, tail) => f3(tail, true)
+ case Nil() => 0
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/Termination_passing2.scala b/src/test/resources/regression/termination/valid/Termination_passing2.scala
new file mode 100644
index 000000000..8fbbcd83e
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/Termination_passing2.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object Termination {
+ def f1(x: Int, b: Boolean) : Int = {
+ if (b) f2(x)
+ else f3(x)
+ }
+
+ def f2(x: Int) : Int = {
+ if (x < 0) 0
+ else f1(x - 1, true)
+ }
+
+ def f3(x: Int) : Int = {
+ if (x > 0) 0
+ else f1(x + 1, false)
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
new file mode 100644
index 000000000..0ccc6c864
--- /dev/null
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -0,0 +1,109 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package test
+package termination
+
+import leon.termination._
+
+import org.scalatest.FunSuite
+
+import java.io.File
+
+import TestUtils._
+
+class TerminationRegression extends FunSuite {
+ private var counter : Int = 0
+ private def nextInt() : Int = {
+ counter += 1
+ counter
+ }
+ private case class Output(report : TerminationReport, reporter : Reporter)
+
+ private def mkPipeline : Pipeline[List[String],TerminationReport] =
+ leon.plugin.ExtractionPhase andThen leon.SubtypingPhase andThen leon.termination.TerminationPhase
+
+ private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(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("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+ 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 = false,
+ termination = true
+ ),
+ options = leonOptions,
+ files = List(file),
+ reporter = new SilentReporter
+ )
+
+ val pipeline = mkPipeline
+
+ if(forError) {
+ intercept[LeonFatalError]{
+ pipeline.run(ctx)(file.getPath :: Nil)
+ }
+ } else {
+
+ val report = pipeline.run(ctx)(file.getPath :: Nil)
+
+ block(Output(report, ctx.reporter))
+ }
+ }
+ }
+
+ private def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) {
+ val fs = filesInResourceDir(
+ "regression/termination/" + cat,
+ _.endsWith(".scala"))
+
+ for(f <- fs) {
+ mkTest(f, Seq(), forError)(block)
+ }
+ }
+
+ forEachFileIn("valid") { output =>
+ val Output(report, reporter) = output
+ val failures = report.results.collect { case (fd, guarantee) if !guarantee.isGuaranteed => fd }
+ assert(failures.isEmpty, "Functions " + failures.map(_.id) + " should terminate")
+ // can't say anything about error counts because of postcondition strengthening that might fail (normal behavior)
+ // assert(reporter.errorCount === 0)
+ assert(reporter.warningCount === 0)
+ }
+
+ forEachFileIn("looping") { output =>
+ val Output(report, reporter) = output
+ val looping = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("looping") }
+ assert(looping.forall(_._2.isInstanceOf[LoopsGivenInputs]), "Functions " + looping.filter(!_._2.isInstanceOf[LoopsGivenInputs]).map(_._1.id) + " should loop")
+ val calling = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("calling") }
+ assert(calling.forall(_._2.isInstanceOf[CallsNonTerminating]), "Functions " + calling.filter(!_._2.isInstanceOf[CallsNonTerminating]).map(_._1.id) + " should call non-terminating")
+ val ok = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("ok") }
+ assert(ok.forall(_._2.isGuaranteed), "Functions " + ok.filter(!_._2.isGuaranteed).map(_._1.id) + " should terminate")
+// assert(reporter.errorCount >= looping.size + calling.size)
+ assert(reporter.warningCount === 0)
+ }
+
+ forEachFileIn("unknown") { output =>
+ val Output(report, reporter) = output
+ val unknown = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("unknown") }
+ assert(unknown.forall(_._2 == NoGuarantee), "Functions " + unknown.filter(_._2 != NoGuarantee).map(_._1.id) + " should be unknown")
+ // can't say anything about error counts because of postcondition strengthening that might fail (normal behavior)
+ // assert(reporter.errorCount === 0)
+ assert(reporter.warningCount === 0)
+ }
+
+ forEachFileIn("error", true) { output => () }
+
+}
--
GitLab