From 554d6e66ae5172b4fe88c3eab526e2e404126705 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 5 Oct 2015 16:29:09 +0200
Subject: [PATCH] Refactor Phases/Pipelines
1) run's prototype follows apply's prototype: (ctx, v) instead of
(ctx)(v)
2) run() returns a possibly updated context. SimpleLeonPhase defines
apply and returns the same context.
---
src/main/scala/leon/LeonPhase.scala | 16 +++++++---
src/main/scala/leon/Main.scala | 32 +++++++++++--------
src/main/scala/leon/Pipeline.scala | 16 +++++-----
.../leon/evaluators/EvaluationPhase.scala | 4 +--
.../frontends/scalac/ExtractionPhase.scala | 4 +--
.../engine/InferInvariantsPhase.scala | 8 ++---
.../leon/solvers/isabelle/IsabellePhase.scala | 4 +--
.../scala/leon/synthesis/ConvertHoles.scala | 10 ++++--
.../leon/synthesis/ConvertWithOracle.scala | 5 +--
.../scala/leon/synthesis/SynthesisPhase.scala | 5 ++-
.../SynthesisProblemExtractionPhase.scala | 4 +--
.../leon/termination/TerminationPhase.scala | 4 +--
.../scala/leon/utils/PreprocessingPhase.scala | 6 ++--
.../leon/utils/TemporaryInputPhase.scala | 4 +--
src/main/scala/leon/utils/TypingPhase.scala | 4 +--
.../leon/verification/AnalysisPhase.scala | 4 +--
.../leon/verification/InjectAsserts.scala | 4 +--
.../scala/leon/xlang/FixReportLabels.scala | 4 +--
.../leon/xlang/XLangDesugaringPhase.scala | 7 ++--
.../leon/isabelle/IsabelleLibrarySuite.scala | 6 ++--
.../regression/frontends/FrontEndsSuite.scala | 4 +--
.../orb/OrbInstrumentationTestSuite.scala | 6 ++--
.../regression/orb/OrbRegressionSuite.scala | 4 +--
.../leon/regression/repair/RepairSuite.scala | 2 +-
.../synthesis/StablePrintingSuite.scala | 4 +--
.../synthesis/SynthesisRegressionSuite.scala | 6 ++--
.../regression/synthesis/SynthesisSuite.scala | 6 ++--
.../termination/TerminationSuite.scala | 6 ++--
.../testcases/TestCasesCompile.scala | 2 +-
.../LibraryVerificationSuite.scala | 2 +-
.../verification/VerificationSuite.scala | 8 ++---
.../verification/XLangVerificationSuite.scala | 6 ++--
.../leon/test/LeonTestSuiteWithProgram.scala | 10 +++---
33 files changed, 117 insertions(+), 100 deletions(-)
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 66a9c31ee..ea8c25316 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 23a0a7780..038bd7529 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 3e3c8a915..aa1471cb8 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 280a68b70..df2f4c42a 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 17503361e..a99c1df18 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 70941a686..e084d830c 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 d7f2fcdc1..47edf6b7f 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 543b37784..7e6c3e880 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 0e0790d0c..ac3785c43 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 082e5dd97..ef2bb41e7 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 7aa46f7a0..dfd1360d5 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 fbfcde51e..f75d388d4 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 148dcba64..672999a10 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 ba561a950..11b6efb68 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 cb0f37ab5..4ea8a029d 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 c0cc41087..8c6c7d0ce 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 ffa8d13a0..418da12eb 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 614057b3b..187f45b49 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 9b2561b11..3a7f8be38 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 08506febe..669949159 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 75e3727bf..b9bfccd36 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 b6a7d60f0..692951f2e 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 71531eeef..24bd55af3 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 6e75e4729..4b1e555f4 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 c7f33afba..5a33b0d8b 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 0ed158111..b5e4bfe99 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 5a5b92735..bd5ff225e 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 5dd5be4b5..5be322e1d 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 7d703d10f..97f6ae603 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 3036b1cf3..bd4422698 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 4c9602c00..4bf89cee8 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 4b03aa9b5..83730cc76 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 ff3d8c04f..23f6de068 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
--
GitLab