From 3e8c9098eee26ad53017522d3ecd1949353bc0f9 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 26 Mar 2015 15:39:53 +0100
Subject: [PATCH] Fixed issue in termination checker and added test-cases
---
.../solvers/templates/LambdaManager.scala | 2 +-
.../scala/leon/termination/ChainBuilder.scala | 10 ++--
.../leon/termination/ChainComparator.scala | 2 +-
.../leon/termination/ChainProcessor.scala | 3 +-
.../leon/termination/LoopProcessor.scala | 3 +-
.../higher-order/invalid/Continuations1.scala | 6 +--
.../higher-order/invalid/Lists1.scala | 7 ---
.../higher-order/invalid/Lists2.scala | 51 +++++++++++++++++++
.../higher-order/invalid/Transformation.scala | 49 ++++++++++++++++++
9 files changed, 112 insertions(+), 21 deletions(-)
create mode 100644 testcases/verification/higher-order/invalid/Lists2.scala
create mode 100644 testcases/verification/higher-order/invalid/Transformation.scala
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 6c69b458d..202ecc735 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -88,7 +88,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
clauses ++= newClauses
newCalls.foreach(p => callBlockers += p._1 -> (callBlockers(p._1) ++ p._2))
newApps.foreach(p => appBlockers += p._1 -> (appBlockers(p._1) ++ p._2))
- } else {
+ } else if (!freeLambdas(tpe).contains(caller)) {
val key = b -> app
// make sure that even if byType(tpe) is empty, app is recorded in blockers
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 742aca7aa..a93386655 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -48,7 +48,7 @@ final case class Chain(relations: List[Relation]) {
lazy val finalParams : Seq[ValDef] = inlining.last._1
- def loop(initialSubst: Map[Identifier, Identifier] = Map(), finalSubst: Map[Identifier, Identifier] = Map()) : Seq[Expr] = {
+ def loop(initialArgs: Seq[Identifier] = Seq.empty, finalArgs: Seq[Identifier] = Seq.empty): Seq[Expr] = {
def rec(relations: List[Relation], funDef: TypedFunDef, subst: Map[Identifier, Identifier]): Seq[Expr] = {
val translate : Expr => Expr = {
val map : Map[Expr, Expr] = subst.map(p => p._1.toVariable -> p._2.toVariable)
@@ -61,18 +61,18 @@ final case class Chain(relations: List[Relation]) {
lazy val newArgs = args.map(translate)
path.map(translate) ++ (relations.tail match {
- case Nil => if (finalSubst.isEmpty) Seq.empty else {
- (tfd.params.map(vd => finalSubst(vd.id).toVariable) zip newArgs).map(p => Equals(p._1, p._2))
- }
+ case Nil =>
+ (finalArgs zip newArgs).map { case (finalArg, newArg) => Equals(finalArg.toVariable, newArg) }
case xs =>
val params = tfd.params.map(_.id)
val freshParams = tfd.params.map(arg => FreshIdentifier(arg.id.name, arg.getType, true))
val bindings = (freshParams.map(_.toVariable) zip newArgs).map(p => Equals(p._1, p._2))
bindings ++ rec(xs, tfd, (params zip freshParams).toMap)
})
+
}
- rec(relations, funDef.typed(funDef.tparams.map(_.tp)), initialSubst)
+ rec(relations, funDef.typedWithDef, (funDef.params.map(_.id) zip initialArgs).toMap)
}
/*
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index bcaa86c4e..e3f6ed623 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -203,7 +203,7 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
}
val lowers = if (endpoint == LowerBoundEndpoint || endpoint == AnyEndpoint) {
- Some(And(e2s map { case (path, e2) => implies(andJoin(path), LessThan(e, recons(e2))) }))
+ Some(andJoin(e2s map { case (path, e2) => implies(andJoin(path), LessThan(e, recons(e2))) }))
} else {
None
}
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 3f1c0b437..f7f02d0e1 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -37,8 +37,7 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
val e1 = tupleWrap(fd.params.map(_.toVariable))
val e2s = fdChains.toSeq.map { chain =>
val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
- val finalBindings = (chain.finalParams.map(_.id) zip freshParams).toMap
- (chain.loop(finalSubst = finalBindings), tupleWrap(freshParams.map(_.toVariable)))
+ (chain.loop(finalArgs = freshParams), tupleWrap(freshParams.map(_.toVariable)))
}
(e1, e2s, fdChains)
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index 3fedb900d..52f4a69c2 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -29,8 +29,7 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
for (chain <- cs if !nonTerminating.isDefinedAt(chain.funDef) &&
(chain.funDef.params zip chain.finalParams).forall(p => p._1.getType == p._2.getType)) {
val freshParams = chain.funDef.params.map(arg => FreshIdentifier(arg.id.name, arg.getType, true))
- val finalBindings = (chain.funDef.params.map(_.id) zip freshParams).toMap
- val path = chain.loop(finalSubst = finalBindings)
+ val path = chain.loop(finalArgs = freshParams)
val srcTuple = tupleWrap(chain.funDef.params.map(_.toVariable))
val resTuple = tupleWrap(freshParams.map(_.toVariable))
diff --git a/testcases/verification/higher-order/invalid/Continuations1.scala b/testcases/verification/higher-order/invalid/Continuations1.scala
index 9511a8157..82f4bdea4 100644
--- a/testcases/verification/higher-order/invalid/Continuations1.scala
+++ b/testcases/verification/higher-order/invalid/Continuations1.scala
@@ -20,8 +20,8 @@ object Continuations1 {
pythagoras_cps(a, b)(_ == a*a + b*b)
}.holds
- def lemma2(a: BigInt, b: BigInt): Boolean = {
- require(a > 0 && b > 0)
- pythagoras_cps(a, b)(_ == a*a)
+ def lemma2(a: BigInt, b: BigInt, c: BigInt): Boolean = {
+ require(a > 0 && b > 0 && c > 0)
+ pythagoras_cps(a, b)(_ == c*c)
}.holds
}
diff --git a/testcases/verification/higher-order/invalid/Lists1.scala b/testcases/verification/higher-order/invalid/Lists1.scala
index b84787c4e..e7582fad6 100644
--- a/testcases/verification/higher-order/invalid/Lists1.scala
+++ b/testcases/verification/higher-order/invalid/Lists1.scala
@@ -19,13 +19,6 @@ object Lists1 {
def positive_lemma(list: List[Int]): Boolean = {
positive(list) == forall(list, gt(0))
- }
-
- def failling_1(list: List[Int]): Boolean = {
- list match {
- case Nil() => positive_lemma(list)
- case Cons(head, tail) => positive_lemma(list) && failling_1(tail)
- }
}.holds
}
diff --git a/testcases/verification/higher-order/invalid/Lists2.scala b/testcases/verification/higher-order/invalid/Lists2.scala
new file mode 100644
index 000000000..777223617
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Lists2.scala
@@ -0,0 +1,51 @@
+import leon._
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+
+
+object Lists2 {
+
+ /**
+ * SORTING
+ **/
+
+ def isSorted[A](l: List[A])(implicit ord: (A, A) => Boolean): Boolean = l match {
+ case Cons(h1, Cons(h2, _)) if !ord(h1, h2) => false
+ case Cons(h, t) => isSorted(t)
+ case Nil() => true
+ }
+
+ def sort[A](l: List[A])(implicit ord: (A, A) => Boolean): List[A] = {
+ val (res, sres) = bubble(l)
+ res
+ /*
+ if (sres) {
+ sort(res)
+ } else {
+ res
+ }
+ */
+ } ensuring {
+ isSorted(_)
+ }
+
+ def bubble[A](l: List[A])(implicit ord: (A, A) => Boolean): (List[A], Boolean) = {
+ l match {
+ case Cons(h1, t1 @ Cons(h2, t2)) if !ord(h1, h2) => (Cons(h2, Cons(h1, t2)), true)
+ case Cons(h1, t1) =>
+ val (tres, sres) = bubble(t1)
+ (Cons(h1, tres), sres)
+ case Nil() =>
+ (Nil(), false)
+ }
+ } ensuring { _ match {
+ /*res =>
+ res match {*/
+ case (lr, sr) => if (!sr) isSorted(lr) else true
+ //}
+ }
+ }
+
+}
+
diff --git a/testcases/verification/higher-order/invalid/Transformation.scala b/testcases/verification/higher-order/invalid/Transformation.scala
new file mode 100644
index 000000000..83c265aee
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Transformation.scala
@@ -0,0 +1,49 @@
+import leon._
+import leon.lang._
+
+object Transformation {
+
+ abstract class Expr
+ case class If(cond: Expr, t: Expr, e: Expr) extends Expr
+ case class Add(e1: Expr, e2: Expr) extends Expr
+ case class Equals(e1: Expr, e2: Expr) extends Expr
+ case class Literal(i: BigInt) extends Expr
+
+ def transform(f: Expr => Option[Expr])(expr: Expr): Expr = {
+ val rec = (x: Expr) => transform(f)(x)
+ val newExpr = expr match {
+ case If(cond, t, e) => If(rec(cond), rec(t), rec(e))
+ case Add(e1, e2) => Add(rec(e1), rec(e2))
+ case Equals(e1, e2) => Equals(rec(e1), rec(e2))
+ case Literal(i) => Literal(i)
+ }
+
+ f(newExpr) match {
+ case Some(e) => e
+ case None() => newExpr
+ }
+ }
+
+ def exists(f: Expr => Boolean)(expr: Expr): Boolean = {
+ val rec = (x: Expr) => exists(f)(x)
+ f(expr) || (expr match {
+ case If(cond, t, e) => rec(cond) || rec(t) || rec(e)
+ case Add(e1, e2) => rec(e1) || rec(e2)
+ case Equals(e1, e2) => rec(e1) || rec(e2)
+ case Literal(i) => false
+ })
+ }
+
+ def test(expr: Expr) = {
+ val t = transform(e => e match {
+ case Equals(Add(Literal(i), Literal(j)), e2) => Some(Equals(Literal(i + j), e2))
+ case Equals(e1, Add(Literal(i), Literal(j))) => Some(Equals(e1, Literal(i + j)))
+ case _ => None[Expr]()
+ })(expr)
+
+ !exists(e => e match {
+ case Equals(_, Add(Literal(i), Literal(j))) => true
+ case _ => false
+ })(t)
+ }.holds
+}
--
GitLab