From 408565db193df0fa79c79193adf6d4a4122b6cfd Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 26 Oct 2012 22:18:00 +0200
Subject: [PATCH] Drastic simplification of Phases/Pipelines
---
src/main/scala/leon/LeonPhase.scala | 6 ++---
src/main/scala/leon/Main.scala | 22 ++++++++--------
src/main/scala/leon/Pipeline.scala | 25 ++++---------------
src/main/scala/leon/Settings.scala | 2 +-
.../scala/leon/verification/Analysis.scala | 4 ++-
.../leon/verification/AnalysisPhase.scala | 6 ++---
.../leon/verification/DefaultTactic.scala | 2 --
.../verification/VerificationReport.scala | 3 +++
src/test/scala/leon/test/ValidPrograms.scala | 7 +++---
9 files changed, 32 insertions(+), 45 deletions(-)
create mode 100644 src/main/scala/leon/verification/VerificationReport.scala
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index d81b8eea7..b18f50d25 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -2,7 +2,7 @@ package leon
import purescala.Definitions.Program
-abstract class LeonPhase[F, T] {
+abstract class LeonPhase[-F, +T] extends Pipeline[F, T] {
val name: String
val description: String
@@ -34,8 +34,8 @@ case class NoopPhase[T]() extends LeonPhase[T, T] {
override def run(ctx: LeonContext)(v: T) = v
}
-case class ExitPhase[T]() extends LeonPhase[T, Unit] {
+case class ExitPhase() extends LeonPhase[Any, Unit] {
val name = "end";
val description = "end"
- override def run(ctx: LeonContext)(v: T) = ()
+ override def run(ctx: LeonContext)(v: Any) = ()
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 831b715db..3f6f9e927 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -104,11 +104,11 @@ object Main {
// Process options we understand:
for(opt <- leonOptions) opt match {
case LeonFlagOption("synthesis") =>
- settings = settings.copy(synthesis = true, xlang = false, analyze = false)
+ settings = settings.copy(synthesis = true, xlang = false, verify = false)
case LeonFlagOption("xlang") =>
settings = settings.copy(synthesis = false, xlang = true)
case LeonFlagOption("parse") =>
- settings = settings.copy(synthesis = false, xlang = false, analyze = false)
+ settings = settings.copy(synthesis = false, xlang = false, verify = false)
case LeonFlagOption("help") =>
displayHelp(reporter)
case _ =>
@@ -117,12 +117,10 @@ object Main {
LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
}
- implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
-
def computePipeline(settings: Settings): Pipeline[List[String], Unit] = {
import purescala.Definitions.Program
- val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
+ val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase
val pipeTransforms: Pipeline[Program, Program] =
if (settings.xlang) {
@@ -141,18 +139,18 @@ object Main {
NoopPhase[Program]()
}
- val pipeAnalysis: Pipeline[Program, Program] =
- if (settings.analyze) {
+ val pipeVerify: Pipeline[Program, Any] =
+ if (settings.verify) {
verification.AnalysisPhase
} else {
NoopPhase[Program]()
}
- pipeBegin followedBy
- pipeTransforms followedBy
- pipeSynthesis followedBy
- pipeAnalysis andThen
- ExitPhase[Program]()
+ pipeBegin andThen
+ pipeTransforms andThen
+ pipeSynthesis andThen
+ pipeVerify andThen
+ ExitPhase()
}
def main(args : Array[String]) {
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 477a08c31..cc79495df 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -1,26 +1,11 @@
package leon
-abstract class Pipeline[F, T] {
- def andThen[G](then: LeonPhase[T, G]): Pipeline[F, G];
- def followedBy[G](pipe: Pipeline[T, G]): Pipeline[F, G];
- def run(ctx: LeonContext)(v: F): T;
-}
-
-class PipeCons[F, V, T](phase: LeonPhase[F, V], then: Pipeline[V, T]) extends Pipeline[F, T] {
- def andThen[G](last: LeonPhase[T, G]) = new PipeCons(phase, then andThen last)
- def followedBy[G](pipe: Pipeline[T, G]) = new PipeCons(phase, then followedBy pipe);
- def run(ctx: LeonContext)(v: F): T = then.run(ctx)(phase.run(ctx)(v))
+abstract class Pipeline[-F, +T] {
+ self =>
- override def toString = {
- phase.toString + " -> " + then.toString
+ def andThen[G](then: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
+ def run(ctx : LeonContext)(v : F) : G = then.run(ctx)(self.run(ctx)(v))
}
-}
-class PipeNil[T]() extends Pipeline[T,T] {
- def andThen[G](last: LeonPhase[T, G]) = new PipeCons(last, new PipeNil)
- def run(ctx: LeonContext)(v: T): T = v
- def followedBy[G](pipe: Pipeline[T, G]) = pipe;
- override def toString = {
- "|"
- }
+ def run(ctx: LeonContext)(v: F): T
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index c9f6af168..f4ff31f49 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -38,5 +38,5 @@ object Settings {
case class Settings(
val synthesis: Boolean = false,
val xlang: Boolean = false,
- val analyze: Boolean = true
+ val verify: Boolean = true
)
diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
index 504016d9d..b6786f30c 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -33,7 +33,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
// construction time. If at least one solver is loaded, verification
// conditions are generated and passed to all solvers. Otherwise, only the
// Analysis extensions are run on the program.
- def analyse : Unit = {
+ def analyse : VerificationReport = {
// We generate all function templates in advance.
for(funDef <- program.definedFunctions if funDef.hasImplementation) {
// this gets cached :D
@@ -53,6 +53,8 @@ class Analysis(val program : Program, val reporter: Reporter) {
reporter.info("Running analysis from extension: " + ae.description)
ae.analyse(program)
})
+
+ new VerificationReport
}
private def generateVerificationConditions : List[VerificationCondition] = {
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 3a218804c..726a7922a 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -3,11 +3,11 @@ package verification
import purescala.Definitions._
-object AnalysisPhase extends UnitPhase[Program] {
+object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
- val description = "Leon Analyses"
+ val description = "Leon Verification"
- def apply(ctx: LeonContext, program: Program) {
+ def run(ctx: LeonContext)(program: Program) : VerificationReport = {
new Analysis(program, ctx.reporter).analyse
}
}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 69d5cf6c4..47a2af0d2 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -42,8 +42,6 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
Implies(matchToIfThenElse(prec.get), bodyAndPost)
}
- import Analysis._
-
withPrec
}
if(functionDefinition.fromLoop)
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
new file mode 100644
index 000000000..2b82dfcee
--- /dev/null
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -0,0 +1,3 @@
+package leon.verification
+
+class VerificationReport
diff --git a/src/test/scala/leon/test/ValidPrograms.scala b/src/test/scala/leon/test/ValidPrograms.scala
index 82af67812..426e78fb2 100644
--- a/src/test/scala/leon/test/ValidPrograms.scala
+++ b/src/test/scala/leon/test/ValidPrograms.scala
@@ -13,12 +13,13 @@ class ValidPrograms extends FunSuite {
"Benchmark [%s] is not a readable file".format(filename))
val ctx = LeonContext(
- Settings(
+ settings = Settings(
synthesis = false,
xlang = false,
- analyze = true
+ verify = true
),
- new SilentReporter
+ files = List(file),
+ reporter = new SilentReporter
)
val pipeline = Main.computePipeline(ctx.settings)
--
GitLab