From 63dedf7113008454f30439b40348e5fb6b8e92ef Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 22 Jun 2015 18:09:23 +0200
Subject: [PATCH] Termination works with a fresh duplicated program
The termination checker updates the functions it checks in place (it
removes and adds post-conditions). We duplicate the program here to
ensure that side-effects do not propagate to other parts (such as
synthesis in the web-interface)
---
.../scala/leon/termination/ComplexTerminationChecker.scala | 2 +-
src/main/scala/leon/termination/ProcessingPipeline.scala | 2 +-
src/main/scala/leon/termination/TerminationChecker.scala | 7 ++++++-
src/main/scala/leon/termination/TerminationPhase.scala | 2 +-
4 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index 024792e23..eef8ddaac 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -8,7 +8,7 @@ import purescala.Expressions._
import scala.collection.mutable.{Map => MutableMap}
-class ComplexTerminationChecker(context: LeonContext, program: Program) extends ProcessingPipeline(context, program) {
+class ComplexTerminationChecker(context: LeonContext, initProgram: Program) extends ProcessingPipeline(context, initProgram) {
val name = "Complex Termination Checker"
val description = "A modular termination checker with a few basic modulesâ„¢"
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index 3b7a36c0a..0dbdb9bd0 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -32,7 +32,7 @@ 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) {
+abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) extends TerminationChecker(context, initProgram) {
implicit val debugSection = utils.DebugSectionTermination
import scala.collection.mutable.{PriorityQueue, Map => MutableMap, Set => MutableSet}
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index 9b12460d2..fb8818922 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -7,7 +7,12 @@ import purescala.Definitions._
import purescala.Expressions._
import purescala.DefOps._
-abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
+abstract class TerminationChecker(val context: LeonContext, initProgram: Program) extends LeonComponent {
+ val program = {
+ val (pgm, _) = replaceFunDefs(initProgram){ fd => Some(fd.duplicate) }
+
+ pgm
+ }
val functions = visibleFunDefsFromMain(program)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index 12af96737..a2bd46d90 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -24,7 +24,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher), Some(excludeByDefault _))
}
- val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
+ val toVerify = tc.program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
val results = toVerify.map { funDef =>
funDef -> tc.terminates(funDef)
--
GitLab