From 5f9356bf8fd8e33553e26ed8bd7edf1e2c83a512 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Mar 2016 11:43:02 +0100
Subject: [PATCH] Fix ugly mess with reports in Main
---
src/main/scala/leon/Main.scala | 31 ++++++-------------
.../leon/termination/TerminationReport.scala | 3 +-
.../scala/leon/utils/PrintReportPhase.scala | 16 ++++++++++
src/main/scala/leon/utils/Report.scala | 8 +++++
.../verification/VerificationReport.scala | 3 +-
5 files changed, 38 insertions(+), 23 deletions(-)
create mode 100644 src/main/scala/leon/utils/PrintReportPhase.scala
create mode 100644 src/main/scala/leon/utils/Report.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 90e222933..db23f2a6a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -3,6 +3,7 @@
package leon
import leon.utils._
+import leon.verification.VerificationReport
object Main {
@@ -11,7 +12,7 @@ object Main {
frontends.scalac.ExtractionPhase,
frontends.scalac.ClassgenPhase,
utils.TypingPhase,
- FileOutputPhase,
+ utils.FileOutputPhase,
purescala.RestoreMethods,
xlang.ArrayTransformation,
xlang.EpsilonElimination,
@@ -192,14 +193,18 @@ object Main {
ExtractionPhase andThen
new PreprocessingPhase(xlangF)
- val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
+ val verification =
+ VerificationPhase andThen
+ (if (xlangF) FixReportLabels else NoopPhase[VerificationReport]()) andThen
+ PrintReportPhase
+ val termination = TerminationPhase andThen PrintReportPhase
val pipeProcess: Pipeline[Program, Any] = {
if (noopF) RestoreMethods andThen FileOutputPhase
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
- else if (analysisF) Pipeline.both(verification, TerminationPhase)
- else if (terminationF) TerminationPhase
+ else if (analysisF) Pipeline.both(verification, termination)
+ else if (terminationF) termination
else if (isabelleF) IsabellePhase
else if (evalF) EvaluationPhase
else if (inferInvF) InferInvariantsPhase
@@ -264,23 +269,7 @@ object Main {
val timer = ctx.timers.total.start()
// Run pipeline
- 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
- }
+ val (ctx2, _) = pipeline.run(ctx, args.toList)
timer.stop()
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index 7a10fe411..c7fc3a0b3 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -4,9 +4,10 @@ package leon
package termination
import purescala.Definitions._
+import utils.Report
import utils.ASCIIHelpers._
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
+case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
def summaryString : String = {
var t = Table("Termination summary")
diff --git a/src/main/scala/leon/utils/PrintReportPhase.scala b/src/main/scala/leon/utils/PrintReportPhase.scala
new file mode 100644
index 000000000..cf19df757
--- /dev/null
+++ b/src/main/scala/leon/utils/PrintReportPhase.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package utils
+
+/** Pretty-prints a [[Report]] */
+case object PrintReportPhase extends UnitPhase[Report] {
+
+ override val description: String = "Print a Leon report"
+ override val name: String = "PrintReport"
+
+ override def apply(ctx: LeonContext, rep: Report): Unit = {
+ ctx.reporter.info(rep.summaryString)
+ }
+
+}
diff --git a/src/main/scala/leon/utils/Report.scala b/src/main/scala/leon/utils/Report.scala
new file mode 100644
index 000000000..4e4a64dbe
--- /dev/null
+++ b/src/main/scala/leon/utils/Report.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.utils
+
+/** Represents a pretty-printable report */
+abstract class Report {
+ def summaryString: String
+}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 847a23a2a..374122f72 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -4,8 +4,9 @@ package leon
package verification
import purescala.Definitions.Program
+import utils.Report
-case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) extends Report {
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
}
--
GitLab