From dfdb0418cbeace1d964f45a6b38e40af471e6a30 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 3 Oct 2013 16:55:33 +0200
Subject: [PATCH] Add debug section for termination
---
src/main/scala/leon/Reporter.scala | 2 ++
src/main/scala/leon/purescala/Trees.scala | 1 -
.../leon/solvers/z3/FunctionTemplate.scala | 2 +-
.../leon/termination/ChainProcessor.scala | 18 +++++++++-------
.../scala/leon/termination/Processor.scala | 21 ++++++-------------
.../termination/TerminationRegression.scala | 2 +-
6 files changed, 20 insertions(+), 26 deletions(-)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 0f693f1ae..c13bfa60e 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -97,6 +97,7 @@ case object DebugSectionSynthesis extends DebugSection("synthesis", 1 << 1
case object DebugSectionTimers extends DebugSection("timers", 1 << 2)
case object DebugSectionOptions extends DebugSection("options", 1 << 3)
case object DebugSectionVerification extends DebugSection("verification", 1 << 4)
+case object DebugSectionTermination extends DebugSection("termination", 1 << 5)
object DebugSections {
val all = Set[DebugSection](
@@ -104,6 +105,7 @@ object DebugSections {
DebugSectionSynthesis,
DebugSectionTimers,
DebugSectionOptions,
+ DebugSectionTermination,
DebugSectionVerification
)
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index bbcfa9bb0..68d87237e 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -64,7 +64,6 @@ object Trees {
val fixedType = funDef.returnType
funDef.args.zip(args).foreach {
- case (a, ResultVariable()) => true // assume its correct... don't know how to get context to really check
case (a, c) => typeCheck(c, a.tpe)
}
}
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 5a3f2e2f4..59380d875 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -27,7 +27,7 @@ class FunctionTemplate private(
guardedExprs : Map[Identifier,Seq[Expr]],
isRealFunDef : Boolean) {
- private val isTerminatingForAllInputs : Boolean = (
+ private def isTerminatingForAllInputs : Boolean = (
isRealFunDef
&& !funDef.hasPrecondition
&& solver.getTerminator.terminates(funDef).isGuaranteed
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 2d6ad5b41..83e20354b 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -17,17 +17,19 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
def run(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = {
import scala.collection.mutable.{Map => MutableMap}
- reporter.info("- Running ChainProcessor")
+ implicit val debugSection = DebugSectionTermination
+
+ reporter.debug("- Running ChainProcessor")
val allChainMap : Map[FunDef, Set[Chain]] = problem.funDefs.map(funDef => funDef -> ChainBuilder.run(funDef)).toMap
- reporter.info("- Computing all possible Chains")
+ reporter.debug("- Computing all possible Chains")
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")
+ reporter.debug("- Collecting re-entrant Chains")
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")
+ reporter.debug("- Computing cross-chain map")
val crossChains : Map[Chain, Set[Chain]] = possibleChainMap.toSeq.map({ case (funDef, chains) =>
val reentrant = reentrantChainMap(funDef)
chains.map(chain => chain -> {
@@ -41,7 +43,7 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
// 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 cluster estimation by fix-point iteration")
+ reporter.debug("- 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
@@ -76,7 +78,7 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
validChainMap.map({ case (funDef, chains) => funDef -> build(chains) })
}
- reporter.info("- Strengthening postconditions")
+ reporter.debug("- Strengthening postconditions")
strengthenPostconditions(problem.funDefs)
def buildLoops(fd: FunDef, cluster: Set[Chain]): (Expr, Seq[(Seq[Expr], Expr)]) = {
@@ -104,13 +106,13 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
})
}
- reporter.info("- Searching for structural size decrease")
+ reporter.debug("- Searching for structural size decrease")
val sizeCleared : ClusterMap = clear(clusters, (fd, cluster) => {
val (e1, e2s) = buildLoops(fd, cluster)
ChainComparator.sizeDecreasing(e1, e2s)
})
- reporter.info("- Searching for numeric convergence")
+ reporter.debug("- Searching for numeric convergence")
val numericCleared : ClusterMap = clear(sizeCleared, (fd, cluster) => {
val (e1, e2s) = buildLoops(fd, cluster)
ChainComparator.numericConverging(e1, e2s, cluster, checker)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index e230c8701..dd826a56a 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -80,11 +80,7 @@ object Solvable {
trait Solvable { self: Processor =>
override def process(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = {
- try {
- self.run(problem)
- } finally {
- destroySolvers
- }
+ self.run(problem)
}
private var solvers: List[SolverFactory[Solver]] = null
@@ -95,22 +91,15 @@ trait Solvable { self: Processor =>
private def initSolvers {
val structDefs = StructuralSize.defs
if (structDefs != lastDefs || solvers == null) {
- destroySolvers
-
val program : Program = self.checker.program
val allDefs : Seq[Definition] = program.mainObject.defs ++ structDefs
val newProgram : Program = program.copy(mainObject = program.mainObject.copy(defs = allDefs))
val context : LeonContext = self.checker.context
- val solvers0 = new FairZ3SolverFactory(context, newProgram) :: Nil
- solvers = solvers0.map(_.withTimeout(500))
+ solvers = new TimeoutSolverFactory(SolverFactory(() => new FairZ3Solver(context, newProgram)), 500) :: Nil
}
}
- protected def destroySolvers {
- if (solvers != null) solvers.foreach(_.free())
- }
-
type Solution = (Option[Boolean], Map[Identifier, Expr])
private def solve(problem: Expr): Solution = {
@@ -151,6 +140,8 @@ trait Solvable { self: Processor =>
}
class ProcessingPipeline(program: Program, context: LeonContext, _processors: Processor*) {
+ implicit val debugSection = DebugSectionTermination
+
import scala.collection.mutable.{Queue => MutableQueue}
assert(_processors.nonEmpty)
@@ -174,7 +165,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
sb.append(" " + funDef.id + "\n")
}
}
- reporter.info(sb.toString)
+ reporter.debug(sb.toString)
}
private def printResult(results: List[Result]) {
@@ -184,7 +175,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
case Cleared(fd) => sb.append(" %-10s %s\n".format(fd.id, "Cleared"))
case Broken(fd, args) => sb.append(" %-10s %s\n".format(fd.id, "Broken for arguments: " + args.mkString("(", ",", ")")))
}
- reporter.info(sb.toString)
+ reporter.debug(sb.toString)
}
def clear(fd: FunDef) : Boolean = {
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 977da326d..f65daf86a 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -99,6 +99,6 @@ class TerminationRegression extends LeonTestSuite {
assert(reporter.warningCount === 0)
}
- forEachFileIn("error", true) { output => () }
+ //forEachFileIn("error", true) { output => () }
}
--
GitLab