From b12edb9f49ea4172529e0ef331db495273a64695 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 26 Mar 2015 18:18:57 +0100
Subject: [PATCH] More termination fixes and more testcases
---
.../scala/leon/termination/Processor.scala | 33 +++++-
.../leon/termination/RecursionProcessor.scala | 11 +-
.../leon/termination/RelationBuilder.scala | 6 +-
.../higher-order/valid/ListOps1.scala | 111 ++++++++++++++++++
.../higher-order/valid/Relations.scala | 39 ++++++
5 files changed, 196 insertions(+), 4 deletions(-)
create mode 100644 testcases/verification/higher-order/valid/ListOps1.scala
create mode 100644 testcases/verification/higher-order/valid/Relations.scala
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 063f03e60..4cf83a131 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -89,8 +89,39 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
private val processors: Array[Processor] = _processors.toArray
private val reporter: Reporter = context.reporter
+ implicit object ProblemOrdering extends Ordering[(Problem, Int)] {
+ def compare(a: (Problem, Int), b: (Problem, Int)): Int = {
+ val ((aProblem, aIndex), (bProblem, bIndex)) = (a,b)
+ val (aDefs, bDefs) = (aProblem.funDefs, bProblem.funDefs)
+
+ val aCallees: Set[FunDef] = aDefs.flatMap(program.callGraph.transitiveCallees)
+ val bCallees: Set[FunDef] = bDefs.flatMap(program.callGraph.transitiveCallees)
+
+ lazy val aCallers: Set[FunDef] = aDefs.flatMap(program.callGraph.transitiveCallers)
+ lazy val bCallers: Set[FunDef] = bDefs.flatMap(program.callGraph.transitiveCallers)
+
+ val aCallsB = bDefs.subsetOf(aCallees)
+ val bCallsA = aDefs.subsetOf(bCallees)
+
+ if (aCallsB && !bCallsA) {
+ -1
+ } else if (bCallsA && !aCallsB) {
+ 1
+ } else {
+ val smallerPool = bCallees.size compare aCallees.size
+ if (smallerPool != 0) smallerPool else {
+ val largerImpact = aCallers.size compare bCallers.size
+ if (largerImpact != 0) largerImpact else {
+ bIndex compare aIndex
+ }
+ }
+ }
+ }
+ }
+
private val initialProblem : Problem = Problem(program.definedFunctions.toSet)
- private val problems : MutableQueue[(Problem,Int)] = MutableQueue((initialProblem, 0))
+ private val problems = new scala.collection.mutable.PriorityQueue[(Problem, Int)] += (initialProblem -> 0)
+// private val problems : MutableQueue[(Problem,Int)] = MutableQueue((initialProblem, 0))
private var unsolved : Set[Problem] = Set()
private def printQueue() {
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 210dfed17..70aca729f 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -29,8 +29,15 @@ class RecursionProcessor(val checker: TerminationChecker with RelationBuilder) e
if (others.exists({ case Relation(_, _, FunctionInvocation(tfd, _), _) => !checker.terminates(tfd.fd).isGuaranteed })) (Nil, List(problem)) else {
val decreases = funDef.params.zipWithIndex.exists({ case (arg, index) =>
- recursive.forall({ case Relation(_, _, FunctionInvocation(_, args), _) =>
- isSubtreeOf(args(index), arg.id)
+ recursive.forall({ case Relation(_, path, FunctionInvocation(_, args), _) =>
+ args(index) match {
+ // handle case class deconstruction in match expression!
+ case Variable(id) => path.reverse.exists {
+ case Equals(Variable(vid), ccs) if vid == id => isSubtreeOf(ccs, arg.id)
+ case _ => false
+ }
+ case expr => isSubtreeOf(expr, arg.id)
+ }
})
})
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index 018eca2e7..cb5ac129c 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -43,7 +43,11 @@ trait RelationBuilder { self: TerminationChecker with Strengthener =>
def collect(e: Expr, path: Seq[Expr]): Option[Relation] = e match {
case fi @ FunctionInvocation(f, args) if self.functions(f.fd) =>
- Some(Relation(funDef, path, fi, inLambda))
+ val flatPath = path flatMap {
+ case And(es) => es
+ case expr => Seq(expr)
+ }
+ Some(Relation(funDef, flatPath, fi, inLambda))
case _ => None
}
diff --git a/testcases/verification/higher-order/valid/ListOps1.scala b/testcases/verification/higher-order/valid/ListOps1.scala
new file mode 100644
index 000000000..59903df08
--- /dev/null
+++ b/testcases/verification/higher-order/valid/ListOps1.scala
@@ -0,0 +1,111 @@
+import leon._
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+
+
+object ListOps1 {
+
+ /**
+ * * Simple List operations
+ * **/
+
+ def partition[A](f: A => Boolean, l: List[A]): (List[A], List[A]) = {
+ l match {
+ case Cons(h, t) =>
+ val (h1, h2) = if (f(h)) (Cons(h, Nil()), Nil[A]())
+ else (Nil[A](), Cons(h, Nil()))
+ val (t1, t2) = partition(f, t)
+ (h1 ++ t1, h2 ++ t2)
+ case Nil() => (Nil[A](), Nil[A]())
+ }
+ } ensuring { x: (List[A], List[A]) => x match {
+ case (a, b) => a.forall(f) &&
+ b.forall(x => !f(x)) &&
+ a.size + b.size == l.size &&
+ a.content ++ b.content == l.content
+ }}
+
+ def collect[A, B](f: A => Option[B], l: List[A]): List[B] = {
+ l match {
+ case Cons(h, t) =>
+ f(h) match {
+ case Some(b) => Cons(b, collect(f, t))
+ case None() => collect(f, t)
+ }
+ case Nil() => Nil()
+ }
+ } ensuring {
+ res => res.size <= l.size
+ }
+
+ def collectFirst[A, B](f: A => Option[B], l: List[A]): Option[B] = {
+ l match {
+ case Cons(h, t) =>
+ f(h).orElse(collectFirst(f, t))
+ case Nil() => None()
+ }
+ } ensuring {
+ res => !l.isEmpty || res.isEmpty
+ }
+
+
+ def count[A](f: A => Boolean, l: List[A]): Int = {
+ l match {
+ case Cons(h, t) =>
+ (if (f(h)) 1 else 0) + count(f, t)
+ case Nil() => 0
+ }
+ } ensuring {
+ res => !(res > 0) || !l.isEmpty
+ }
+
+ def dropWhile[A](f: A => Boolean, l: List[A]): List[A] = {
+ l match {
+ case Cons(h, t) if f(h) => dropWhile(f, t)
+ case Cons(h, t) if !f(h) => l
+ case Nil() => Nil()
+ }
+ } ensuring {
+ res =>
+ if(res.size < l.size) {
+ f(l.head)
+ } else {
+ l.isEmpty || !f(l.head)
+ }
+ }
+
+ def forall[A](f: A => Boolean, l: List[A]): Boolean = {
+ l match {
+ case Cons(h, t) if f(h) => forall(f, t)
+ case Cons(_, t) => false
+ case Nil() => true
+ }
+ } ensuring {
+ res => res == !exists[A]({ x => !f(x) }, l)
+ }
+
+ def exists[A](f: A => Boolean, l: List[A]): Boolean = {
+ l match {
+ case Cons(h, t) if f(h) => true
+ case Cons(_, t) => exists(f, t)
+ case Nil() => false
+ }
+ } ensuring {
+ res => res == res
+ }
+
+
+ /**
+ * * Map with universal quantifier in post as a witness argument
+ * **/
+
+ def mapWitness[A,B](f: A => B, l: List[A], w: A): List[B] = {
+ l match {
+ case Cons(h, t) => f(h) :: mapWitness(f, t, w)
+ case Nil() => Nil()
+ }
+ } ensuring {
+ res => if (l.content contains w) res.content contains f(w) else true
+ }
+}
diff --git a/testcases/verification/higher-order/valid/Relations.scala b/testcases/verification/higher-order/valid/Relations.scala
new file mode 100644
index 000000000..8a84b2d8e
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Relations.scala
@@ -0,0 +1,39 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+
+object Relations {
+ sealed case class G[A](domain: List[A])
+
+ def forall[A](p: A => Boolean)(implicit g: G[A]) : Boolean = {
+ g.domain.forall(p)
+ }
+ def exists[A](p: A => Boolean)(implicit g: G[A]) : Boolean = {
+ g.domain.exists(p)
+ }
+
+ def circ[A](r1: ((A,A)) ⇒ Boolean, r2: ((A,A)) ⇒ Boolean)(implicit g: G[A]) : (((A,A)) => Boolean) = {
+ case (x,z) => exists((y:A) => r1(x,y) && r2(y,z))
+ }
+
+ def eq[A](s1: A ⇒ Boolean, s2: A ⇒ Boolean)(implicit g: G[A]): Boolean = {
+ forall((x:A) => s1(x)==s2(x))
+ }
+
+ def setOf[A](l: List[A]): (A => Boolean) = (l.contains(_))
+
+ def test(r1: ((Int,Int)) => Boolean, r2: ((Int,Int)) => Boolean): Boolean = {
+ implicit val g1: G[Int] = G[Int](List(1,2))
+ implicit val g2: G[(Int,Int)] = G(List(1 -> 1, 1 -> 2, 2 -> 2, 2 -> 1, 3 -> 2, 3 -> 1))
+ //val r1: ((Int,Int)) => Boolean = setOf(List(1 -> 2, 2 -> 3, 3 -> 1))
+ //val r2: ((Int,Int)) => Boolean = setOf(List(1 -> 1, 2 -> 3, 3 -> 2))
+ val commutative =
+ eq(circ(r1, r2), circ(r2, r1))
+
+ val r3: ((Int,Int)) => Boolean = setOf(List(1 -> 5, 2 -> 2, 1 -> 2))
+ val associative =
+ eq(circ(circ(r1,r2), r3), circ(r1, circ(r2, r3)))
+ associative
+ }.holds
+
+}
--
GitLab