diff --git a/library/collection/List.scala b/library/collection/List.scala
index 530bb5b41eb79539550897d201183851f721b262..448aea577adba630090410f2acc4b410c22d0aa5 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -285,46 +285,40 @@ sealed abstract class List[T] {
(take(c), drop(c))
}
- def insertAt(pos: BigInt, l: List[T]): List[T] = {
- if(pos < 0) {
- insertAt(size + pos, l)
- } else if(pos == BigInt(0)) {
- l ++ this
- } else {
- this match {
- case Cons(h, t) =>
- Cons(h, t.insertAt(pos-1, l))
- case Nil() =>
- l
+ def insertAt(pos: BigInt, l: List[T]): List[T] = (this match {
+ case Nil() => l
+ case Cons(h, t) =>
+ if (pos < 0) {
+ insertAt(size + pos, l)
+ } else if (pos == BigInt(0)) {
+ l ++ this
+ } else {
+ Cons(h, t.insertAt(pos - 1, l))
}
- }
- } ensuring { res =>
+ }) ensuring { res =>
res.size == this.size + l.size &&
res.content == this.content ++ l.content
}
- def replaceAt(pos: BigInt, l: List[T]): List[T] = {
- if(pos < 0) {
- replaceAt(size + pos, l)
- } else if(pos == BigInt(0)) {
- l ++ this.drop(l.size)
- } else {
- this match {
- case Cons(h, t) =>
- Cons(h, t.replaceAt(pos-1, l))
- case Nil() =>
- l
+ def replaceAt(pos: BigInt, l: List[T]): List[T] = (this match {
+ case Nil() => l
+ case Cons(h, t) =>
+ if (pos < 0) {
+ replaceAt(size + pos, l)
+ } else if (pos == BigInt(0)) {
+ l ++ this.drop(l.size)
+ } else {
+ Cons(h, t.replaceAt(pos - 1, l))
}
- }
- } ensuring { res =>
+ }) ensuring { res =>
res.content.subsetOf(l.content ++ this.content)
}
def rotate(s: BigInt): List[T] = {
- if (s < 0) {
- rotate(size + s)
- } else if (s > size) {
- rotate(s - size)
+ if (isEmpty) {
+ Nil()
+ } else if (s < 0) {
+ rotate(size+s)
} else {
drop(s) ++ take(s)
}
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 753663bbe1eae8ad0f6ca0e714b1a2102fe11a8c..5537d41e24e2bf6340a2802e5a8bc2de29621772 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -14,13 +14,13 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
def run(problem: Problem) = {
reporter.debug("- Strengthening postconditions")
- checker.strengthenPostconditions(problem.funDefs)(this)
+ checker.strengthenPostconditions(problem.funSet)(this)
reporter.debug("- Strengthening applications")
- checker.strengthenApplications(problem.funDefs)(this)
+ checker.strengthenApplications(problem.funSet)(this)
reporter.debug("- Running ChainBuilder")
- val chainsMap : Map[FunDef, (Set[FunDef], Set[Chain])] = problem.funDefs.map { funDef =>
+ val chainsMap : Map[FunDef, (Set[FunDef], Set[Chain])] = problem.funSet.map { funDef =>
funDef -> checker.getChains(funDef)(this)
}.toMap
@@ -28,7 +28,7 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
if (loopPoints.size > 1) {
reporter.debug("-+> Multiple looping points, can't build chain proof")
- (Nil, List(problem))
+ None
} else {
def exprs(fd: FunDef): (Expr, Seq[(Seq[Expr], Expr)], Set[Chain]) = {
@@ -43,7 +43,7 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
(e1, e2s, fdChains)
}
- val funDefs = if (loopPoints.size == 1) Set(loopPoints.head) else problem.funDefs
+ val funDefs = if (loopPoints.size == 1) Set(loopPoints.head) else problem.funSet
reporter.debug("-+> Searching for structural size decrease")
@@ -60,11 +60,10 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
numericFormulas.exists(formula => definitiveALL(formula))
}
- if (structuralDecreasing || numericDecreasing) {
- (problem.funDefs.map(Cleared), Nil)
- } else {
- (Nil, List(problem))
- }
+ if (structuralDecreasing || numericDecreasing)
+ Some(problem.funDefs map Cleared)
+ else
+ None
}
}
}
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index 78a5c93c4f239805407f3bcd0ec8338f04ece65a..e4936762b2003851b91fb83ecb06379b205b4151 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -9,62 +9,22 @@ import purescala.Expressions._
import scala.collection.mutable.{Map => MutableMap}
class ComplexTerminationChecker(context: LeonContext, program: Program)
- extends TerminationChecker(context, program)
+ extends ProcessingPipeline(context, program)
with StructuralSize
with RelationComparator
with ChainComparator
with Strengthener
- with ComponentBuilder
with RelationBuilder
with ChainBuilder {
val name = "Complex Termination Checker"
val description = "A modular termination checker with a few basic modules™"
- private val pipeline = new ProcessingPipeline(
- program, context, // required for solvers and reporting
- new ComponentProcessor(this),
+ def processors = List(
new RecursionProcessor(this),
new RelationProcessor(this),
new ChainProcessor(this),
new LoopProcessor(this)
)
- private val clearedMap : MutableMap[FunDef, String] = MutableMap()
- private val brokenMap : MutableMap[FunDef, (String, Seq[Expr])] = MutableMap()
- private val maybeBrokenMap : MutableMap[FunDef, (String, Seq[Expr])] = MutableMap()
-
- def initialize() {
- for ((reason, results) <- pipeline.run; result <- results) result match {
- case Cleared(fd) => clearedMap(fd) = reason
- case Broken(fd, args) => brokenMap(fd) = (reason, args)
- case MaybeBroken(fd, args) => maybeBrokenMap(fd) = (reason, args)
- }
- }
-
- private val terminationMap : MutableMap[FunDef, TerminationGuarantee] = MutableMap()
- def terminates(funDef: FunDef): TerminationGuarantee = terminationMap.get(funDef) match {
- case Some(guarantee) => guarantee
- case None => {
- val guarantee = brokenMap.get(funDef) match {
- case Some((reason, args)) => LoopsGivenInputs(reason, args)
- case None => maybeBrokenMap.get(funDef) match {
- case Some((reason, args)) => MaybeLoopsGivenInputs(reason, args)
- case None => program.callGraph.transitiveCallees(funDef) intersect (brokenMap.keys.toSet ++ maybeBrokenMap.keys) match {
- case set if set.nonEmpty => CallsNonTerminating(set)
- case _ => if (pipeline.clear(funDef)) clearedMap.get(funDef) match {
- case Some(reason) => Terminates(reason)
- case None => scala.sys.error(funDef.id + " -> not problem, but not cleared or broken ??")
- } else NoGuarantee
- }
- }
- }
-
- if (guarantee != NoGuarantee) {
- terminationMap(funDef) = guarantee
- }
-
- guarantee
- }
- }
}
diff --git a/src/main/scala/leon/termination/ComponentBuilder.scala b/src/main/scala/leon/termination/ComponentBuilder.scala
deleted file mode 100644
index 2826cb3d4725722167e657defe7932936b1ab093..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/termination/ComponentBuilder.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package termination
-
-import utils._
-
-trait ComponentBuilder {
- def getComponents[T](graph : Map[T,Set[T]]) : List[Set[T]] = SCC.scc(graph)
-}
diff --git a/src/main/scala/leon/termination/ComponentProcessor.scala b/src/main/scala/leon/termination/ComponentProcessor.scala
deleted file mode 100644
index 4a7935d78985dd992c3dd17b01c5946a92fb29cd..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/termination/ComponentProcessor.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package termination
-
-import purescala.Definitions._
-import scala.collection.mutable.{Map => MutableMap}
-
-class ComponentProcessor(val checker: TerminationChecker with ComponentBuilder) extends Processor {
-
- val name: String = "Component Processor"
-
- def run(problem: Problem) = {
- val pairs : Set[(FunDef, FunDef)] = checker.program.callGraph.allCalls.filter({
- case (fd1, fd2) => problem.funDefs(fd1) && problem.funDefs(fd2)
- })
-
- val callGraph : Map[FunDef,Set[FunDef]] = pairs.groupBy(_._1).mapValues(_.map(_._2))
- val components : List[Set[FunDef]] = checker.getComponents(callGraph)
- val fdToSCC : Map[FunDef, Set[FunDef]] = components.map(set => set.map(fd => fd -> set)).flatten.toMap
-
- val terminationCache : MutableMap[FunDef, Boolean] = MutableMap()
- def terminates(fd: FunDef) : Boolean = terminationCache.getOrElse(fd, {
- val scc = fdToSCC.getOrElse(fd, Set()) // functions that aren't called and don't call belong to no SCC
- val result = if (scc(fd)) false else scc.forall(terminates)
- terminationCache(fd) = result
- result
- })
-
- val terminating = problem.funDefs.filter(terminates)
- assert(components.forall(scc => (scc subsetOf terminating) || (scc intersect terminating).isEmpty))
- val newProblems = components.filter(scc => (scc intersect terminating).isEmpty).map(Problem)
- (terminating.map(Cleared), newProblems)
- }
-}
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index a63928021d3e40964e892fa2f604bf5757c93bf6..9f419e8ab1e4a3a10533ff7c6bd5358ddf9bb6ec 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -16,10 +16,10 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
def run(problem: Problem) = {
reporter.debug("- Strengthening applications")
- checker.strengthenApplications(problem.funDefs)(this)
+ checker.strengthenApplications(problem.funSet)(this)
reporter.debug("- Running ChainBuilder")
- val chains : Set[Chain] = problem.funDefs.flatMap(fd => checker.getChains(fd)(this)._2)
+ val chains : Set[Chain] = problem.funSet.flatMap(fd => checker.getChains(fd)(this)._2)
reporter.debug("- Searching for loops")
val nonTerminating: MutableMap[FunDef, Result] = MutableMap.empty
@@ -46,10 +46,10 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
cs.flatMap(c1 => chains.flatMap(c2 => c1.compose(c2)))
}
- val results = nonTerminating.values.toSet
- val remaining = problem.funDefs -- nonTerminating.keys
- val newProblems = if (remaining.nonEmpty) List(Problem(remaining)) else Nil
- (results, newProblems)
+ if (nonTerminating.nonEmpty)
+ Some(nonTerminating.values.toSeq)
+ else
+ None
}
}
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3b7a36c0a3127e95a524a95a296bd1fb5295521f
--- /dev/null
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -0,0 +1,217 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package termination
+
+import purescala.Expressions._
+import purescala.Definitions._
+import utils._
+
+trait Problem {
+ def funSet: Set[FunDef]
+ def funDefs: Seq[FunDef]
+ def contains(fd: FunDef): Boolean = funSet(fd)
+
+ override def toString : String = funDefs.map(_.id).mkString("Problem(", ",", ")")
+}
+
+object Problem {
+ def apply(fds: Set[FunDef]): Problem = new Problem {
+ val funSet = fds
+ lazy val funDefs = funSet.toSeq
+ }
+
+ def apply(fds: Seq[FunDef]): Problem = new Problem {
+ val funDefs = fds
+ lazy val funSet = funDefs.toSet
+ }
+}
+
+sealed abstract class Result(funDef: FunDef)
+case class Cleared(funDef: FunDef) extends Result(funDef)
+case class Broken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
+case class MaybeBroken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
+
+abstract class ProcessingPipeline(context: LeonContext, program: Program) extends TerminationChecker(context, program) {
+ implicit val debugSection = utils.DebugSectionTermination
+
+ import scala.collection.mutable.{PriorityQueue, Map => MutableMap, Set => MutableSet}
+
+ def processors: List[Processor]
+
+ private lazy val processorArray: Array[Processor] = {
+ assert(processors.nonEmpty)
+ 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.funSet, bProblem.funSet)
+
+ 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 problems = new PriorityQueue[(Problem, Int)]
+ def running = problems.nonEmpty
+
+ private val clearedMap : MutableMap[FunDef, String] = MutableMap.empty
+ private val brokenMap : MutableMap[FunDef, (String, Seq[Expr])] = MutableMap.empty
+ private val maybeBrokenMap : MutableMap[FunDef, (String, Seq[Expr])] = MutableMap.empty
+
+ private val unsolved : MutableSet[Problem] = MutableSet.empty
+ private val dependencies : MutableSet[Problem] = MutableSet.empty
+
+ def isProblem(fd: FunDef): Boolean =
+ unsolved.exists(_.contains(fd)) ||
+ dependencies.exists(_.contains(fd)) || {
+ val problemDefs = problems.flatMap(_._1.funDefs).toSet
+ problemDefs(fd) || {
+ val callees = program.callGraph.transitiveCallees(fd)
+ (problemDefs intersect callees).nonEmpty
+ }
+ }
+
+ private def printQueue() {
+ val sb = new StringBuilder()
+ sb.append("- Problems in Queue:\n")
+ for(p @ (problem, index) <- problems) {
+ sb.append(" -> Problem awaiting processor #")
+ sb.append(index + 1)
+ sb.append(" (")
+ sb.append(processorArray(index).name)
+ sb.append(")")
+ if (p == problems.head) sb.append(" <- next")
+ sb.append("\n")
+ for(funDef <- problem.funDefs) {
+ sb.append(" " + funDef.id + "\n")
+ }
+ }
+ reporter.debug(sb.toString)
+ }
+
+ private def printResult(results: List[Result]) {
+ val sb = new StringBuilder()
+ sb.append("- Processing Result:\n")
+ for(result <- results) result match {
+ case Cleared(fd) => sb.append(f" ${fd.id}%-10s Cleared\n")
+ case Broken(fd, args) => sb.append(f" ${fd.id}%-10s ${"Broken for arguments: " + args.mkString("(", ",", ")")}\n")
+ case MaybeBroken(fd, args) => sb.append(f" ${fd.id}%-10s ${"HO construct application breaks for arguments: " + args.mkString("(", ",", ")")}\n")
+ }
+ reporter.debug(sb.toString)
+ }
+
+ private val terminationMap : MutableMap[FunDef, TerminationGuarantee] = MutableMap.empty
+ def terminates(funDef: FunDef): TerminationGuarantee = terminationMap.get(funDef) match {
+ case Some(guarantee) => guarantee
+ case None =>
+ val guarantee = brokenMap.get(funDef) match {
+ case Some((reason, args)) => LoopsGivenInputs(reason, args)
+ case None => maybeBrokenMap.get(funDef) match {
+ case Some((reason, args)) => MaybeLoopsGivenInputs(reason, args)
+ case None =>
+ val callees = program.callGraph.transitiveCallees(funDef)
+ val broken = brokenMap.keys.toSet ++ maybeBrokenMap.keys
+ callees intersect broken match {
+ case set if set.nonEmpty => CallsNonTerminating(set)
+ case _ if isProblem(funDef) => NoGuarantee
+ case _ => clearedMap.get(funDef) match {
+ case Some(reason) => Terminates(reason)
+ case None if !running =>
+ verifyTermination(funDef)
+ terminates(funDef)
+ case _ =>
+ if (!dependencies.exists(_.contains(funDef))) {
+ dependencies ++= generateProblems(funDef)
+ }
+ NoGuarantee
+ }
+ }
+ }
+ }
+
+ if (!running) terminationMap(funDef) = guarantee
+ guarantee
+ }
+
+ private def generateProblems(funDef: FunDef): Seq[Problem] = {
+ val funDefs = program.callGraph.transitiveCallees(funDef) + funDef
+ val pairs = program.callGraph.allCalls.filter { case (fd1, fd2) => funDefs(fd1) && funDefs(fd2) }
+ val callGraph = pairs.groupBy(_._1).mapValues(_.map(_._2))
+ val components = SCC.scc(callGraph)
+
+ for (fd <- funDefs -- components.toSet.flatten) clearedMap(fd) = "Non-recursive"
+
+ components.map(fds => Problem(fds.toSeq))
+ }
+
+ def verifyTermination(funDef: FunDef): Unit = {
+ problems ++= generateProblems(funDef).map(_ -> 0)
+
+ val it = new Iterator[(String, List[Result])] {
+ def hasNext : Boolean = running
+ def next() : (String, List[Result]) = {
+ printQueue()
+ val (problem, index) = problems.head
+ val processor : Processor = processorArray(index)
+ reporter.debug("Running " + processor.name)
+ val result = processor.run(problem)
+ reporter.debug(" +-> " + (if (result.isDefined) "Success" else "Failure"))
+
+ // dequeue and enqueue atomically to make sure the queue always
+ // makes sense (necessary for calls to terminates(fd))
+ problems.dequeue()
+ result match {
+ case None if index == processorArray.length - 1 =>
+ unsolved += problem
+ case None =>
+ problems.enqueue(problem -> (index + 1))
+ case Some(results) =>
+ val impacted = problem.funDefs.flatMap(fd => program.callGraph.transitiveCallers(fd))
+ val reenter = unsolved.filter(p => (p.funDefs intersect impacted).nonEmpty)
+ problems.enqueue(reenter.map(_ -> 0).toSeq : _*)
+ unsolved --= reenter
+ }
+
+ if (dependencies.nonEmpty) {
+ problems.enqueue(dependencies.map(_ -> 0).toSeq : _*)
+ dependencies.clear
+ }
+
+ processor.name -> result.toList.flatten
+ }
+ }
+
+ for ((reason, results) <- it; result <- results) result match {
+ case Cleared(fd) => clearedMap(fd) = reason
+ case Broken(fd, args) => brokenMap(fd) = (reason, args)
+ case MaybeBroken(fd, args) => maybeBrokenMap(fd) = (reason, args)
+ }
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index b6c6972f9925ad5389b99cdad6689ace103c2fa3..46c125d8e7172408443e8c4eb001bbb2c71dbd76 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -12,15 +12,6 @@ import scala.concurrent.duration._
import leon.solvers._
import leon.solvers.z3._
-case class Problem(funDefs: Set[FunDef]) {
- override def toString : String = funDefs.map(_.id).mkString("Problem(", ",", ")")
-}
-
-sealed abstract class Result(funDef: FunDef)
-case class Cleared(funDef: FunDef) extends Result(funDef)
-case class Broken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
-case class MaybeBroken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
-
trait Processor {
val name: String
@@ -30,7 +21,7 @@ trait Processor {
implicit val debugSection = utils.DebugSectionTermination
val reporter = checker.context.reporter
- def run(problem: Problem): (Traversable[Result], Traversable[Problem])
+ def run(problem: Problem): Option[Seq[Result]]
}
trait Solvable extends Processor {
@@ -82,119 +73,3 @@ trait Solvable extends Processor {
}
}
-class ProcessingPipeline(program: Program, context: LeonContext, _processors: Processor*) {
- implicit val debugSection = utils.DebugSectionTermination
-
- import scala.collection.mutable.{Queue => MutableQueue}
-
- assert(_processors.nonEmpty)
- 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 = 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() {
- val sb = new StringBuilder()
- sb.append("- Problems in Queue:\n")
- for((problem, index) <- problems) {
- sb.append(" -> Problem awaiting processor #")
- sb.append(index + 1)
- sb.append(" (")
- sb.append(processors(index).name)
- sb.append(")\n")
- for(funDef <- problem.funDefs) {
- sb.append(" " + funDef.id + "\n")
- }
- }
- reporter.debug(sb.toString)
- }
-
- private def printResult(results: List[Result]) {
- val sb = new StringBuilder()
- sb.append("- Processing Result:\n")
- for(result <- results) result match {
- case Cleared(fd) => sb.append(f" ${fd.id}%-10s Cleared\n")
- case Broken(fd, args) => sb.append(f" ${fd.id}%-10s ${"Broken for arguments: " + args.mkString("(", ",", ")")}\n")
- case MaybeBroken(fd, args) => sb.append(f" ${fd.id}%-10s ${"HO construct application breaks for arguments: " + args.mkString("(", ",", ")")}\n")
- }
- reporter.debug(sb.toString)
- }
-
- def clear(fd: FunDef) : Boolean = {
- lazy val unsolvedDefs = unsolved.map(_.funDefs).flatten
- lazy val problemDefs = problems.map({ case (problem, _) => problem.funDefs }).flatten.toSet
- def issue(defs: Set[FunDef]) : Boolean = defs(fd) || (defs intersect program.callGraph.transitiveCallees(fd)).nonEmpty
- ! (issue(unsolvedDefs) || issue(problemDefs))
- }
-
- def run : Iterator[(String, List[Result])] = new Iterator[(String, List[Result])] {
- // basic sanity check, funDefs shouldn't call themselves in precondition!
- // XXX: it seems like some do...
- // assert(initialProblem.funDefs.forall(fd => !fd.precondition.map({ precondition =>
- // functionCallsOf(precondition).map(fi => program.transitiveCallees(fi.funDef)).flatten
- // }).flatten.toSet(fd)))
-
- def hasNext : Boolean = problems.nonEmpty
- def next() : (String, List[Result]) = {
- printQueue()
- val (problem, index) = problems.head
- val processor : Processor = processors(index)
- reporter.debug("Running " + processor.name)
- val (_results, nextProblems) = processor.run(problem)
- val results = _results.toList
- printResult(results)
-
- // dequeue and enqueue atomically to make sure the queue always
- // makes sense (necessary for calls to clear(fd))
- problems.dequeue()
- nextProblems match {
- case x :: xs if x == problem =>
- assert(xs.isEmpty)
- if (index == processors.length - 1) unsolved += x
- else problems.enqueue(x -> (index + 1))
- case list @ x :: xs =>
- problems.enqueue(list.map(p => p -> 0) : _*)
- problems.enqueue(unsolved.map(p => p -> 0).toSeq : _*)
- unsolved = Set()
- case Nil => // no problem => do nothing!
- }
-
- processor.name -> results.toList
- }
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index eec2e3bca22c3bde632909dd384c8338ecba6b36..d0b29d62f1e1e0e0ee59783dd6a3796f0ec6e84e 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -22,12 +22,14 @@ class RecursionProcessor(val checker: TerminationChecker with RelationBuilder) e
rec(expr, true)
}
- def run(problem: Problem) = if (problem.funDefs.size > 1) (Nil, List(problem)) else {
+ def run(problem: Problem) = if (problem.funDefs.size > 1) None else {
val funDef = problem.funDefs.head
val relations = checker.getRelations(funDef)
val (recursive, others) = relations.partition({ case Relation(_, _, FunctionInvocation(tfd, _), _) => tfd.fd == funDef })
- if (others.exists({ case Relation(_, _, FunctionInvocation(tfd, _), _) => !checker.terminates(tfd.fd).isGuaranteed })) (Nil, List(problem)) else {
+ if (others.exists({ case Relation(_, _, FunctionInvocation(tfd, _), _) => !checker.terminates(tfd.fd).isGuaranteed })) {
+ None
+ } else {
val decreases = funDef.params.zipWithIndex.exists({ case (arg, index) =>
recursive.forall({ case Relation(_, path, FunctionInvocation(_, args), _) =>
args(index) match {
@@ -41,8 +43,10 @@ class RecursionProcessor(val checker: TerminationChecker with RelationBuilder) e
})
})
- if (!decreases) (Nil, List(problem))
- else (Cleared(funDef) :: Nil, Nil)
+ if (decreases)
+ Some(Cleared(funDef) :: Nil)
+ else
+ None
}
}
}
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index e8303c74ac6827723a5f67185cfa34ba52fedbcb..d4d1aad73f1c17d9f9ff323f38e19707a7356ae2 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -19,14 +19,14 @@ class RelationProcessor(
def run(problem: Problem) = {
reporter.debug("- Strengthening postconditions")
- checker.strengthenPostconditions(problem.funDefs)(this)
+ checker.strengthenPostconditions(problem.funSet)(this)
reporter.debug("- Strengthening applications")
- checker.strengthenApplications(problem.funDefs)(this)
+ checker.strengthenApplications(problem.funSet)(this)
val formulas = problem.funDefs.map({ funDef =>
funDef -> checker.getRelations(funDef).collect({
- case Relation(_, path, FunctionInvocation(tfd, args), _) if problem.funDefs(tfd.fd) =>
+ case Relation(_, path, FunctionInvocation(tfd, args), _) if problem.funSet(tfd.fd) =>
val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
def constraint(expr: Expr) = implies(andJoin(path.toSeq), expr)
val greaterThan = checker.sizeDecreasing(e1, e2)
@@ -69,14 +69,15 @@ class RelationProcessor(
val ok = decreasing.collect({ case (fd, Success) => fd })
val nok = decreasing.collect({ case (fd, Dep(fds)) => fd -> fds }).toList
- val (allOk, allNok) = fix(currentReducing, ok, nok)
+ val (allOk, allNok) = fix(currentReducing, ok.toSet, nok)
(allOk, allNok.map(_._1).toSet ++ decreasing.collect({ case (fd, Failure) => fd }))
}
- assert(terminating ++ nonTerminating == problem.funDefs)
+ assert(terminating ++ nonTerminating == problem.funSet)
- val results = terminating.map(Cleared).toList
- val newProblems = if ((problem.funDefs intersect nonTerminating).nonEmpty) List(Problem(nonTerminating)) else Nil
- (results, newProblems)
+ if (nonTerminating.isEmpty)
+ Some(terminating.map(Cleared).toSeq)
+ else
+ None
}
}
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index 7a92744241c9999fac898a24d92e44c18b3fd982..2a6c5bcbc81941bf1d1c8834468f6993100deea8 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -7,12 +7,13 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
+import utils._
import scala.collection.mutable.{ Map => MutableMap }
import scala.annotation.tailrec
-class SimpleTerminationChecker(context: LeonContext, program: Program) extends TerminationChecker(context, program) with ComponentBuilder {
+class SimpleTerminationChecker(context: LeonContext, program: Program) extends TerminationChecker(context, program) {
val name = "T1"
val description = "The simplest form of Terminator™"
@@ -20,7 +21,7 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
private lazy val callGraph: Map[FunDef, Set[FunDef]] =
program.callGraph.allCalls.groupBy(_._1).mapValues(_.map(_._2)) // one liner from hell
- private lazy val components = getComponents(callGraph)
+ private lazy val components = SCC.scc(callGraph)
val allVertices = callGraph.keySet ++ callGraph.values.flatten
val sccArray = components.toArray
@@ -36,7 +37,6 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
private val answerCache = MutableMap.empty[FunDef, TerminationGuarantee]
- def initialize() {}
def terminates(funDef: FunDef) = answerCache.getOrElse(funDef, {
val g = forceCheckTermination(funDef)
answerCache(funDef) = g
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index f881b125ea8a914be7f29edb837f3d38e349271f..9b12460d2c77834b6685c5050dc7d2367e2d5b32 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -11,7 +11,6 @@ abstract class TerminationChecker(val context: LeonContext, val program: Program
val functions = visibleFunDefsFromMain(program)
- def initialize() : Unit
def terminates(funDef : FunDef) : TerminationGuarantee
}
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index d674340d75fe572d118c15a7b866a2c95c3fde00..4ad4aac3f52f147cf19e84d991edbfc35172494c 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -16,9 +16,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
// val tc = new SimpleTerminationChecker(ctx, program)
val tc = new ComplexTerminationChecker(ctx, program)
- tc.initialize()
-
- val results = visibleFunDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
+ val results = funDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
funDef -> tc.terminates(funDef)
}
val endTime = System.currentTimeMillis
diff --git a/src/test/resources/regression/termination/looping/Queue.scala b/src/test/resources/regression/termination/looping/Queue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a571e82e853d96dc84b7376a6751b1281dc50787
--- /dev/null
+++ b/src/test/resources/regression/termination/looping/Queue.scala
@@ -0,0 +1,28 @@
+
+import leon._
+import leon.lang._
+import leon.collection._
+
+sealed abstract class Queue[T] {
+
+ def looping_1: BigInt = {
+ this match {
+ case QEmpty() => 0
+ case QCons(f, r) => f.size + r.size
+ }
+ } ensuring (res => res == this.looping_2.size && res >= 0)
+
+ def looping_2: List[T] = (this match {
+ case QEmpty() => Nil()
+ case QCons(f, r) => f ++ r.reverse
+ }) ensuring (resOne => this.looping_3 == resOne.content && resOne.size == this.looping_1 && resOne.size >= 0)
+
+
+ def looping_3: Set[T] = (this match {
+ case QEmpty() => Set()
+ case QCons(f, r) => f.content ++ r.content
+ }) ensuring (res => res == this.looping_2.content)
+}
+
+case class QCons[T](f : List[T], r: List[T]) extends Queue[T]
+case class QEmpty[T]() extends Queue[T]
diff --git a/src/test/resources/regression/termination/valid/Queue.scala b/src/test/resources/regression/termination/valid/Queue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b73919a7c732a2233273d4f284f4f8c3ad93143
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/Queue.scala
@@ -0,0 +1,27 @@
+
+import leon._
+import leon.lang._
+import leon.collection._
+
+sealed abstract class Queue[T] {
+
+ def size: BigInt = {
+ this match {
+ case QEmpty() => 0
+ case QCons(f, r) => f.size + r.size
+ }
+ } ensuring (res => res == this.toList.size && res >= 0)
+
+ def toList: List[T] = (this match {
+ case QEmpty() => Nil()
+ case QCons(f, r) => f ++ r.reverse
+ }) ensuring (resOne => this.content == resOne.content && resOne.size >= 0)
+
+ def content: Set[T] = this match {
+ case QEmpty() => Set()
+ case QCons(f, r) => f.content ++ r.content
+ }
+}
+
+case class QCons[T](f : List[T], r: List[T]) extends Queue[T]
+case class QEmpty[T]() extends Queue[T]