diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 66a9c31eee4673aa3548e30d14d4b54f6ae1822f..ea8c2531660c522017e0abd32b4c1220acd33649 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -9,27 +9,33 @@ trait LeonPhase[-F, +T] extends Pipeline[F, T] with LeonComponent {
// def run(ac: LeonContext)(v: F): T
}
+trait SimpleLeonPhase[-F, +T] extends LeonPhase[F, T] {
+ def apply(ctx: LeonContext, v: F): T
+
+ def run(ctx: LeonContext, v: F): (LeonContext, T) = (ctx, apply(ctx, v))
+}
+
abstract class TransformationPhase extends LeonPhase[Program, Program] {
def apply(ctx: LeonContext, p: Program): Program
- override def run(ctx: LeonContext)(p: Program) = {
+ override def run(ctx: LeonContext, p: Program) = {
ctx.reporter.debug("Running transformation phase: " + name)(utils.DebugSectionLeon)
- apply(ctx, p)
+ (ctx, apply(ctx, p))
}
}
abstract class UnitPhase[T] extends LeonPhase[T, T] {
def apply(ctx: LeonContext, p: T): Unit
- override def run(ctx: LeonContext)(p: T) = {
+ override def run(ctx: LeonContext, p: T) = {
ctx.reporter.debug("Running unit phase phase: " + name)(utils.DebugSectionLeon)
apply(ctx, p)
- p
+ (ctx, p)
}
}
case class NoopPhase[T]() extends LeonPhase[T, T] {
val name = "noop"
val description = "no-op"
- override def run(ctx: LeonContext)(v: T) = v
+ override def run(ctx: LeonContext, v: T) = (ctx, v)
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 23a0a7780463a1ba66809747df5cc9d690463b95..038bd7529e89fc6d29a32eb9dba266c0c7df3c67 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -246,24 +246,28 @@ object Main {
val timer = ctx.timers.total.start()
// Run pipeline
- pipeline.run(ctx)(args.toList) match {
- case (vReport: verification.VerificationReport, tReport: termination.TerminationReport) =>
- ctx.reporter.info(vReport.summaryString)
- ctx.reporter.info(tReport.summaryString)
-
- case report: verification.VerificationReport =>
- ctx.reporter.info(report.summaryString)
-
- case report: termination.TerminationReport =>
- ctx.reporter.info(report.summaryString)
-
- case _ =>
+ val ctx2 = pipeline.run(ctx, args.toList) match {
+ case (ctx2, (vReport: verification.VerificationReport, tReport: termination.TerminationReport)) =>
+ ctx2.reporter.info(vReport.summaryString)
+ ctx2.reporter.info(tReport.summaryString)
+ ctx2
+
+ case (ctx2, report: verification.VerificationReport) =>
+ ctx2.reporter.info(report.summaryString)
+ ctx2
+
+ case (ctx2, report: termination.TerminationReport) =>
+ ctx2.reporter.info(report.summaryString)
+ ctx2
+
+ case (ctx2, _) =>
+ ctx2
}
timer.stop()
- ctx.reporter.whenDebug(DebugSectionTimers) { debug =>
- ctx.timers.outputTable(debug)
+ ctx2.reporter.whenDebug(DebugSectionTimers) { debug =>
+ ctx2.timers.outputTable(debug)
}
hasFatal = false
} catch {
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 3e3c8a915b2084c5b6563028d9e5033639585833..aa1471cb8b962e4261f116fe98699f5eed94b3ec 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -6,24 +6,24 @@ abstract class Pipeline[-F, +T] {
self =>
def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
- def run(ctx : LeonContext)(v : F) : G = {
- val s = self.run(ctx)(v)
+ def run(ctx: LeonContext, v: F): (LeonContext, G) = {
+ val (ctx2, s) = self.run(ctx, v)
if(ctx.findOptionOrDefault(SharedOptions.optStrictPhases)) ctx.reporter.terminateIfError()
- thenn.run(ctx)(s)
+ thenn.run(ctx2, s)
}
}
- def run(ctx: LeonContext)(v: F): T
+ def run(ctx: LeonContext, v: F): (LeonContext, T)
}
object Pipeline {
def both[T, R1, R2](f1: Pipeline[T, R1], f2: Pipeline[T, R2]): Pipeline[T, (R1, R2)] = new Pipeline[T, (R1, R2)] {
- def run(ctx : LeonContext)(t : T): (R1, R2) = {
- val r1 = f1.run(ctx)(t)
+ def run(ctx: LeonContext, t: T): (LeonContext, (R1, R2)) = {
+ val (ctx1, r1) = f1.run(ctx, t)
// don't check for SharedOptions.optStrictPhases because f2 does not depend on the result of f1
- val r2 = f2.run(ctx)(t)
- (r1, r2)
+ val (ctx2, r2) = f2.run(ctx1, t)
+ (ctx2, (r1, r2))
}
}
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index 280a68b7067e152cbac613734821f6077fa2030f..df2f4c42aebc0533fe6fb4b59d263067fa4804a3 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -8,13 +8,13 @@ import purescala.Definitions._
import purescala.DefOps._
import purescala.Expressions._
-object EvaluationPhase extends LeonPhase[Program, Unit] {
+object EvaluationPhase extends UnitPhase[Program] {
val name = "Evaluation"
val description = "Evaluating ground functions"
implicit val debugSection = utils.DebugSectionEvaluation
- def run(ctx: LeonContext)(program: Program): Unit = {
+ def apply(ctx: LeonContext, program: Program): Unit = {
val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 17503361e0bb20a87ed15047eeea99b04688a803..a99c1df18b880ea6e7d0f379041deade3172902a 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -9,7 +9,7 @@ import utils._
import scala.tools.nsc.{Settings,CompilerCommand}
import java.io.File
-object ExtractionPhase extends LeonPhase[List[String], Program] {
+object ExtractionPhase extends SimpleLeonPhase[List[String], Program] {
val name = "Scalac Extraction"
val description = "Extraction of trees from the Scala Compiler"
@@ -20,7 +20,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
implicit val debug = DebugSectionTrees
- def run(ctx: LeonContext)(args: List[String]): Program = {
+ def apply(ctx: LeonContext, args: List[String]): Program = {
val timer = ctx.timers.frontend.start()
val settings = new Settings
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index 70941a6861c2dd01c46da80e016894cd746684c1..e084d830c8b6076f2208cfc70a249121d2d3e8fb 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -24,7 +24,7 @@ import leon.purescala.PrettyPrinter
* This phase performs automatic invariant inference.
* TODO: should time be implicitly made positive
*/
-object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
+object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
val name = "InferInv"
val description = "Invariant Inference"
@@ -45,7 +45,7 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
optDisableInfer)
//TODO provide options for analyzing only selected functions
- def run(ctx: LeonContext)(program: Program): InferenceReport = {
+ def apply(ctx: LeonContext, program: Program): InferenceReport = {
//control printing of statistics
val dumpStats = true
@@ -146,11 +146,11 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
def validateAndCollectNotValidated(prog: Program, ctx: LeonContext, timeout: Int): Set[String] = {
val verifyPipe = AnalysisPhase
val ctxWithTO = createLeonContext(ctx, "--timeout=" + timeout)
- (verifyPipe.run(ctxWithTO)(prog)).results.collect{
+ (verifyPipe.run(ctxWithTO, prog)._2).results.collect{
case (VC(_, fd, VCKinds.Postcondition), Some(vcRes)) if vcRes.isInconclusive =>
fd.id.name
case (VC(_, fd, vcKind), Some(vcRes)) if vcRes.isInvalid =>
throw new IllegalStateException("Invalid" + vcKind + " for function " + fd.id.name)
}.toSet
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/solvers/isabelle/IsabellePhase.scala b/src/main/scala/leon/solvers/isabelle/IsabellePhase.scala
index d7f2fcdc1f032ab7758155cc6bb274c57f45bae0..47edf6b7f0219bc5042011dcd5afa6d559dad07e 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabellePhase.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabellePhase.scala
@@ -9,7 +9,7 @@ import leon.purescala.Definitions._
import leon.utils._
import leon.verification._
-object IsabellePhase extends LeonPhase[Program, VerificationReport] {
+object IsabellePhase extends SimpleLeonPhase[Program, VerificationReport] {
object IsabelleVC extends VCKind("Isabelle", "isa")
@@ -18,7 +18,7 @@ object IsabellePhase extends LeonPhase[Program, VerificationReport] {
implicit val debugSection = DebugSectionIsabelle
- def run(context: LeonContext)(program: Program): VerificationReport = {
+ def apply(context: LeonContext, program: Program): VerificationReport = {
val env = IsabelleEnvironment(context, program)
val report = env.map { env =>
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 543b377843d77372fbce8151337f3a6b09390c94..7e6c3e880e0ed2d608b4d7711abd40ddae1134ee 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -10,7 +10,7 @@ import purescala.ExprOps._
import purescala.Definitions._
import purescala.Constructors._
-object ConvertHoles extends LeonPhase[Program, Program] {
+object ConvertHoles extends TransformationPhase {
val name = "Convert Holes to Choose"
val description = "Convert Holes found in bodies to equivalent Choose"
@@ -97,8 +97,12 @@ object ConvertHoles extends LeonPhase[Program, Program] {
}
- def run(ctx: LeonContext)(pgm: Program): Program = {
- pgm.definedFunctions.foreach(fd => fd.fullBody = convertHoles(fd.fullBody,ctx) )
+ def apply(ctx: LeonContext, pgm: Program): Program = {
+ // TODO: remove side-effects
+ for (fd <- pgm.definedFunctions) {
+ fd.fullBody = convertHoles(fd.fullBody,ctx)
+ }
+
pgm
}
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracle.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
index 0e0790d0cf4a6fec23b158c5ca92a8a9a0bbc7b4..ac3785c43e454431ebf18ecc2df4dcec78a6a16b 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracle.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
@@ -8,7 +8,7 @@ import purescala.ExprOps._
import purescala.Definitions._
import purescala.Constructors._
-object ConvertWithOracle extends LeonPhase[Program, Program] {
+object ConvertWithOracle extends TransformationPhase {
val name = "Convert WithOracle to Choose"
val description = "Convert WithOracle found in bodies to equivalent Choose"
@@ -36,7 +36,8 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
* }
*
*/
- def run(ctx: LeonContext)(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
+ // TODO: Remove side-effects
pgm.definedFunctions.foreach(fd => {
if (fd.hasBody) {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 082e5dd97e8e9b57500f63d78128c5426e4f9190..ef2bb41e75eb256484f1a663699bd16ca6efa40b 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -11,7 +11,7 @@ import leon.utils.ASCIIHelpers
import graph._
-object SynthesisPhase extends LeonPhase[Program, Program] {
+object SynthesisPhase extends TransformationPhase {
val name = "Synthesis"
val description = "Partial synthesis of \"choose\" constructs. Also used by repair during the synthesis stage."
@@ -62,7 +62,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
)
}
- def run(ctx: LeonContext)(program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program): Program = {
val options = processOptions(ctx)
@@ -102,5 +102,4 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
program
}
-
}
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 7aa46f7a09cd8c095495f7aba837a7f072ee273e..dfd1360d5a3ea8536edd6d1ff3df89d07d12fe24 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -7,11 +7,11 @@ package utils
import purescala.DefOps.funDefsFromMain
import purescala.Definitions._
-object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
+object SynthesisProblemExtractionPhase extends SimpleLeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
val name = "Synthesis Problem Extraction"
val description = "Synthesis Problem Extraction"
- def run(ctx: LeonContext)(p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
+ def apply(ctx: LeonContext, p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
// Look for choose()
val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id) if f.body.isDefined) yield {
f -> ChooseInfo.extractFromFunction(ctx, p, f)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index fbfcde51ea4c1f503313707e7132a6f38cd24c30..f75d388d4d2f63317f1c90d063a6404bc78e5edb 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -5,11 +5,11 @@ package termination
import purescala.Definitions._
-object TerminationPhase extends LeonPhase[Program,TerminationReport] {
+object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
val name = "Termination"
val description = "Check termination of PureScala functions"
- def run(ctx : LeonContext)(program : Program) : TerminationReport = {
+ def apply(ctx: LeonContext, program: Program): TerminationReport = {
val startTime = System.currentTimeMillis
// val tc = new SimpleTerminationChecker(ctx, program)
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 148dcba64b12eb96949d109ec5672ccaef3ac437..672999a10d5444fc62465df0c09b34ea1f68a43c 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -11,12 +11,12 @@ import leon.synthesis.{ConvertWithOracle, ConvertHoles}
import leon.verification.InjectAsserts
import leon.xlang.XLangDesugaringPhase
-class PreprocessingPhase(private val desugarXLang: Boolean = false) extends TransformationPhase {
+class PreprocessingPhase(private val desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
val name = "preprocessing"
val description = "Various preprocessings on Leon programs"
- def apply(ctx: LeonContext, p: Program): Program = {
+ override def run(ctx: LeonContext, p: Program): (LeonContext, Program) = {
def debugTrees(title: String): LeonPhase[Program, Program] = {
if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
@@ -52,6 +52,6 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Tran
AdaptationPhase andThen
debugTrees("Program after pre-processing")
- phases.run(ctx)(p)
+ phases.run(ctx, p)
}
}
diff --git a/src/main/scala/leon/utils/TemporaryInputPhase.scala b/src/main/scala/leon/utils/TemporaryInputPhase.scala
index ba561a9504ebcaff583eb3ffd36c18df8b01d714..11b6efb68aa51fb46e2b23af82cbc834b0481abe 100644
--- a/src/main/scala/leon/utils/TemporaryInputPhase.scala
+++ b/src/main/scala/leon/utils/TemporaryInputPhase.scala
@@ -5,12 +5,12 @@ package utils
import java.io.{File, BufferedWriter, FileWriter}
-object TemporaryInputPhase extends LeonPhase[(List[String], List[String]), List[String]] {
+object TemporaryInputPhase extends SimpleLeonPhase[(List[String], List[String]), List[String]] {
val name = "Temporary Input"
val description = "Create source files from string content"
- def run(ctx: LeonContext)(data: (List[String], List[String])): List[String] = {
+ def apply(ctx: LeonContext, data: (List[String], List[String])): List[String] = {
val (contents, opts) = data
val files = contents.map { content =>
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index cb0f37ab514faa26275e655f9e6aacad0d1cb171..4ea8a029dd285cef58bca2ab9c6e35d4ed1202ce 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -10,7 +10,7 @@ import purescala.Expressions._
import purescala.Definitions._
import purescala.Constructors._
-object TypingPhase extends LeonPhase[Program, Program] {
+object TypingPhase extends SimpleLeonPhase[Program, Program] {
val name = "Typing"
val description = "Ensure and enforce certain Leon typing rules"
@@ -28,7 +28,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
*
* 3) Make sure that abstract classes have at least one descendant
*/
- def run(ctx: LeonContext)(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
pgm.definedFunctions.foreach(fd => {
// Part (1)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index c0cc41087ad966d9475d98b5b1b8654459dcbea2..8c6c7d0cef4441a4d62c57214a9cdb39877a1ed2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -10,13 +10,13 @@ import scala.concurrent.duration._
import solvers._
-object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
+object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
implicit val debugSection = utils.DebugSectionVerification
- def run(ctx: LeonContext)(program: Program): VerificationReport = {
+ def apply(ctx: LeonContext, program: Program): VerificationReport = {
val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
val timeout: Option[Long] = ctx.findOption(SharedOptions.optTimeout)
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index ffa8d13a0f2322a53270a52b3d4a2e82ef75cc8c..418da12eb62e1fb1ead33bc0317da9ceb9662e28 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -10,12 +10,12 @@ import Definitions._
import Constructors._
import xlang.Expressions._
-object InjectAsserts extends LeonPhase[Program, Program] {
+object InjectAsserts extends SimpleLeonPhase[Program, Program] {
val name = "Asserts"
val description = "Inject asserts for various correctness conditions (map accesses, array accesses, divisions by zero,..)"
- def run(ctx: LeonContext)(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
def indexUpTo(i: Expr, e: Expr) = {
and(GreaterEquals(i, IntLiteral(0)), LessThan(i, e))
}
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 614057b3bbbc99b7edf8fe2b8af3c3578ff47ea1..187f45b49eac8eeea3188ec197c7de02dba2a760 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -6,7 +6,7 @@ package xlang
import leon.purescala.Definitions.IsLoop
import leon.verification._
-object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]{
+object FixReportLabels extends SimpleLeonPhase[VerificationReport, VerificationReport]{
override val name: String = "fixReportLabels"
override val description: String = "Fix verification report labels to reflect the original imperative VCs"
@@ -16,7 +16,7 @@ object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]
case object InvariantPost extends VCKind("invariant postcondition", "inv. post.")
case object InvariantInd extends VCKind("invariant inductive", "inv. ind.")
- def run(ctx: LeonContext)(vr: VerificationReport): VerificationReport = {
+ def apply(ctx: LeonContext, vr: VerificationReport): VerificationReport = {
//this is enough to convert invariant postcondition and inductive conditions. However the initial validity
//of the invariant (before entering the loop) will still appear as a regular function precondition
//To fix this, we need some information in the VCs about which function the precondtion refers to
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index 9b2561b11d442bacc7e68ae4bb47d2037d92dace..3a7f8be381cfa5fdb87dc6870cf35141f8d8cf33 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -5,17 +5,18 @@ package xlang
import purescala.Definitions.Program
-object XLangDesugaringPhase extends TransformationPhase {
+object XLangDesugaringPhase extends LeonPhase[Program, Program] {
val name = "xlang desugaring"
val description = "Desugar xlang features into PureScala"
- def apply(ctx: LeonContext, pgm: Program): Program = {
+ override def run(ctx: LeonContext, pgm: Program): (LeonContext, Program) = {
val phases =
ArrayTransformation andThen
EpsilonElimination andThen
ImperativeCodeElimination
- phases.run(ctx)(pgm)
+
+ phases.run(ctx, pgm)
}
}
diff --git a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
index 08506febee6139c36527e8059998a8a2436337f4..66994915993456e0c825fcaef18a84168c7b614d 100644
--- a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
@@ -14,13 +14,13 @@ import leon.utils.PreprocessingPhase
class IsabelleLibrarySuite extends LeonRegressionSuite {
- object IsabelleNoopPhase extends LeonPhase[Program, Unit] {
+ object IsabelleNoopPhase extends UnitPhase[Program] {
val name = "isabelle-noop"
val description = "Isabelle definitions"
implicit val debugSection = DebugSectionIsabelle
- def run(context: LeonContext)(program: Program): Unit =
+ def apply(context: LeonContext, program: Program): Unit =
Await.result(IsabelleEnvironment(context, program).map(_ => ()), Duration.Inf)
}
@@ -29,7 +29,7 @@ class IsabelleLibrarySuite extends LeonRegressionSuite {
val ctx = Main.processOptions(Seq("--isabelle:download=true", "--functions=_")).copy(reporter = new TestSilentReporter())
- pipeline.run(ctx)(Nil)
+ pipeline.run(ctx, Nil)
}
}
diff --git a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala b/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
index 75e3727bfbfa7dc9506d35bc5fcf0402715a844a..b9bfccd36bc2abcc3479c9d3a703df0cdfe16ab7 100644
--- a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
+++ b/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
@@ -18,10 +18,10 @@ class FrontEndsSuite extends LeonRegressionSuite {
val ctx = createLeonContext()
if (forError) {
intercept[LeonFatalError]{
- pipeline.run(ctx)(List(f.getAbsolutePath))
+ pipeline.run(ctx, List(f.getAbsolutePath))
}
} else {
- pipeline.run(ctx)(List(f.getAbsolutePath))
+ pipeline.run(ctx, List(f.getAbsolutePath))
}
}
diff --git a/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala b/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala
index b6a7d60f0076038c093abf8d6bec7cefe6f44e41..692951f2eb37100a2782605a06701e28d9905334 100644
--- a/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala
@@ -32,10 +32,10 @@ class OrbInstrumentationTestSuite extends LeonRegressionSuite {
}""")
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
- val program = beginPipe.run(ctx)(testFilename)
+ val (ctx2, program) = beginPipe.run(ctx, testFilename)
val processPipe = InstrumentationPhase
// check properties.
- val instProg = processPipe.run(ctx)(program)
+ val (ctx3, instProg) = processPipe.run(ctx2, program)
val sizeFun = instProg.definedFunctions.find(_.id.name.startsWith("size"))
if(!sizeFun.isDefined || !sizeFun.get.returnType.isInstanceOf[TupleType])
fail("Error in instrumentation")
@@ -43,6 +43,6 @@ class OrbInstrumentationTestSuite extends LeonRegressionSuite {
def toTempFile(content: String): List[String] = {
val pipeline = leon.utils.TemporaryInputPhase
- pipeline.run(createLeonContext())((List(content), Nil))
+ pipeline.run(createLeonContext(), (List(content), Nil))._2
}
}
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 71531eeef02649facfbc439c95bf3c81e5b00ebb..24bd55af32bb3f5f1f2e27f1f9e4913f2a406497 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -23,9 +23,9 @@ class OrbRegressionSuite extends LeonRegressionSuite {
val ctx = createLeonContext("--inferInv", "--minbounds", "--timeout="+bound)
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
- val program = beginPipe.run(ctx)(f.getAbsolutePath :: Nil)
+ val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
val processPipe = InferInvariantsPhase
- val report = processPipe.run(ctx)(program)
+ val (ctx3, report) = processPipe.run(ctx2, program)
val fails = report.conditions.filterNot(_.invariant.isDefined)
if (!fails.isEmpty)
fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 6e75e4729c11cf9c1b2402fcb4c337bb2838c318..4b1e555f4b12137484cedbbf912d943e46ef27e3 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -39,7 +39,7 @@ class RepairSuite extends LeonRegressionSuite {
)
test(name) {
- pipeline.run(ctx)(List(path))
+ pipeline.run(ctx, List(path))
if(reporter.errorCount > 0) {
fail("Errors during repair:\n")//+reporter.lastErrors.mkString("\n"))
}
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index c7f33afba55f14607b350b631f5dbaf6a028890a..5a33b0d8b0b35e3dd44c2fbf6ebf45eb3f8a962e 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -34,9 +34,9 @@ class StablePrintingSuite extends LeonRegressionSuite {
frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
- val program = pipeline.run(ctx)((List(content), Nil))
+ val (ctx2, program) = pipeline.run(ctx, (List(content), Nil))
- (program, opts, ChooseInfo.extractFromProgram(ctx, program))
+ (program, opts, ChooseInfo.extractFromProgram(ctx2, program))
}
case class Job(content: String, choosesToProcess: Set[Int], rules: List[String]) {
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index 0ed158111818698d047bcbff934530ace0e8f7dc..b5e4bfe993f0a92b10f0dbe42582eee162625281 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -33,9 +33,11 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase
- program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
+ val (ctx2, pgm2) = pipeline.run(ctx, f.getAbsolutePath :: Nil)
- chooses = ChooseInfo.extractFromProgram(ctx, program)
+ program = pgm2
+
+ chooses = ChooseInfo.extractFromProgram(ctx2, program)
}
for (ci <- chooses) {
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
index 5a5b92735b5f89892b04cbf271c3ce72a21bf88a..bd5ff225ef190cd82f1b51a8975c495925d7d17a 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
@@ -91,12 +91,12 @@ class SynthesisSuite extends LeonRegressionSuite {
new PreprocessingPhase andThen
SynthesisProblemExtractionPhase
- val (program, results) = pipeline.run(ctx)((List(content), Nil))
+ val (ctx2, (program, results)) = pipeline.run(ctx, (List(content), Nil))
for ((f,cis) <- results; ci <- cis) {
info(f"${ci.fd.id.toString}%-20s")
- val sctx = SynthesisContext(ctx,
+ val sctx = SynthesisContext(ctx2,
SynthesisSettings(),
ci.fd,
program)
@@ -104,7 +104,7 @@ class SynthesisSuite extends LeonRegressionSuite {
val p = ci.problem
if (strats.isDefinedAt(f.id.name)) {
- val search = new TestSearch(ctx, ci, p, strats(f.id.name))
+ val search = new TestSearch(ctx2, ci, p, strats(f.id.name))
val sols = search.search(sctx)
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 5dd5be4b5a1488c82079270b32dc8d6e82ebdab6..5be322e1dc19f33edc8c01ffde51f3ee9612bc5a 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -56,13 +56,13 @@ class TerminationSuite extends LeonRegressionSuite {
if(forError) {
intercept[LeonFatalError]{
- pipeline.run(ctx)(file.getPath :: Nil)
+ pipeline.run(ctx, file.getPath :: Nil)
}
} else {
- val report = pipeline.run(ctx)(file.getPath :: Nil)
+ val (ctx2, report) = pipeline.run(ctx, file.getPath :: Nil)
- block(Output(report, ctx.reporter))
+ block(Output(report, ctx2.reporter))
}
}
}
diff --git a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
index 7d703d10f23ec43a6122da8a11b4218681af89a8..97f6ae603eece13d8c42fac4f25b33a632b7f709 100644
--- a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
+++ b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
@@ -35,7 +35,7 @@ class TestCasesCompile extends LeonRegressionSuite {
val ctx = createLeonContext()
try {
- pipeline.run(ctx)(List(f.getAbsolutePath))
+ pipeline.run(ctx, List(f.getAbsolutePath))
} catch {
case _: LeonFatalError =>
fail(" Failed to compile "+name)
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
index 3036b1cf343dc1efaf2e4a8ce53f63726ec9500f..bd44226988a11516cfadb4eec35174972662d263 100644
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
@@ -16,7 +16,7 @@ class LibraryVerificationSuite extends LeonRegressionSuite {
val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
- val report = pipeline.run(ctx)(Nil)
+ val (ctx2, report) = pipeline.run(ctx, Nil)
assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions)
}
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 4c9602c00aeb363a40e725f55c81270dd9b4cf48..4bf89cee8f78b76a686cfca004c9b8d8f83ae6c8 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -39,7 +39,7 @@ trait VerificationSuite extends LeonRegressionSuite {
val ctx = createLeonContext(files:_*)
try {
- val ast = extraction.run(ctx)(files)
+ val (ctx2, ast) = extraction.run(ctx, files)
val programs = {
val (user, lib) = ast.units partition { _.isMainUnit }
user map { u => (u.id, Program(u :: lib)) }
@@ -50,12 +50,12 @@ trait VerificationSuite extends LeonRegressionSuite {
val ctx = createLeonContext(options: _*)
if (forError) {
intercept[LeonFatalError] {
- pipeBack.run(ctx)(p)
+ pipeBack.run(ctx, p)
}
}
else {
- val report = pipeBack.run(ctx)(p)
- block(Output(report, ctx.reporter))
+ val (ctx2, report) = pipeBack.run(ctx, p)
+ block(Output(report, ctx2.reporter))
}
}
}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 4b03aa9b5d157e88289b336cffdcba02bf162e4b..83730cc760abb29776027b2ef152b9afccbd861a 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -58,12 +58,12 @@ class XLangVerificationSuite extends LeonRegressionSuite {
if(forError) {
intercept[LeonFatalError]{
- pipeline.run(ctx)(file.getPath :: Nil)
+ pipeline.run(ctx, file.getPath :: Nil)
}
} else {
- val report = pipeline.run(ctx)(file.getPath :: Nil)
+ val (ctx2, report) = pipeline.run(ctx, file.getPath :: Nil)
- block(Output(report, ctx.reporter))
+ block(Output(report, ctx2.reporter))
}
}
}
diff --git a/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala b/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala
index ff3d8c04f80ad276b9ed0247042d94ae48304479..23f6de0689d6f9debd1d7eae39eb9ab5fd9053f8 100644
--- a/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala
+++ b/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala
@@ -30,14 +30,14 @@ trait LeonTestSuiteWithProgram extends fixture.FunSuite {
def getFixture(): (LeonContext, Program) = synchronized {
if (fixtureCache.isEmpty) {
- val reporter = new TestSilentReporter
- val im = new InterruptManager(reporter)
+ val reporter = new TestSilentReporter
+ val im = new InterruptManager(reporter)
- val ctx = Main.processOptions(leonOpts).copy(reporter = reporter, interruptManager = im)
+ val ctx = Main.processOptions(leonOpts).copy(reporter = reporter, interruptManager = im)
- val pgm = pipeline.run(ctx)((sources, Nil))
+ val (ctx2, pgm) = pipeline.run(ctx, (sources, Nil))
- fixtureCache = Some((ctx, pgm))
+ fixtureCache = Some((ctx2, pgm))
}
fixtureCache.get