diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index d81b8eea718d40639c0ff5edce6bdc57c0837f83..b18f50d2559a196b22163b3c62ed3def2f610ef0 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 831b715db3beb67b5fa1e1c8be22bd4a52e1573f..3f6f9e9278a6504a5e465db6870b84b987e67bfa 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 477a08c31250ba1996ddccd59262631fe75499c1..cc79495df619d9cb6ed74fb7a8fb03f628e07d6b 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 c9f6af1681735ad3e1b1b176a2b16e178caf9ecf..f4ff31f49292dcd90d911c28b88aee516d048561 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 504016d9dfcf842a7e0e05990e16003a5b522cc8..b6786f30c973734d9b3e2b648c00957e63bd3aaf 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 3a218804c0052a80e442b0fbbfd7cdacfe5a3fe0..726a7922a59de70142369301a5e57917c4b1ad2e 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 69d5cf6c4636e912f0cff1baca6b1dd354748e3f..47a2af0d2a098722e36af1c2e829bf31e5734a59 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 0000000000000000000000000000000000000000..2b82dfcee0d00581075985630da40bff71c1ee0b
--- /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 82af678129f6f01bd21d6c588b0daea70f4b9545..426e78fb27f2422d9f86952d9995374b1917202f 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)