From 2cb4367ead30895ad3256fb78ecfdd5ea644b2cd Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 14 Apr 2015 16:48:17 +0200
Subject: [PATCH] TransformationPhase -> UnitPhase, when possible
---
.../leon/purescala/CompleteAbstractDefinitions.scala | 6 ++----
src/main/scala/leon/xlang/ArrayTransformation.scala | 7 +++----
src/main/scala/leon/xlang/EpsilonElimination.scala | 11 ++++-------
src/main/scala/leon/xlang/XLangAnalysisPhase.scala | 12 ++++++------
4 files changed, 15 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index 482bd06cf..5508bb0a6 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -7,20 +7,18 @@ import Common._
import Definitions._
import Expressions._
-object CompleteAbstractDefinitions extends TransformationPhase {
+object CompleteAbstractDefinitions extends UnitPhase[Program] {
val name = "Materialize abstract functions"
val description = "Inject fake choose-like body in abstract definitions"
- def apply(ctx: LeonContext, program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program) = {
for (u <- program.units; m <- u.modules; fd <- m.definedFunctions; if fd.body.isEmpty) {
val post = fd.postcondition getOrElse (
Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
)
fd.body = Some(Choose(post))
}
- // Translation is in-place
- program
}
}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 90360fe3d..c82ce1dd0 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -2,7 +2,7 @@
package leon.xlang
-import leon.TransformationPhase
+import leon.UnitPhase
import leon.LeonContext
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -11,16 +11,15 @@ import leon.xlang.Expressions._
import leon.purescala.Extractors._
import leon.purescala.Types._
-object ArrayTransformation extends TransformationPhase {
+object ArrayTransformation extends UnitPhase[Program] {
val name = "Array Transformation"
val description = "Add bound checking for array access and remove array update with side effect"
- def apply(ctx: LeonContext, pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program) = {
pgm.definedFunctions.foreach(fd => {
fd.fullBody = transform(fd.fullBody)(Map())
})
- pgm
}
def transform(expr: Expr)(implicit env: Map[Identifier, Identifier]): Expr = (expr match {
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 3333ab255..88e0acc2f 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -2,24 +2,22 @@
package leon.xlang
-import leon.TransformationPhase
-import leon.LeonContext
+import leon.{UnitPhase, TransformationPhase, LeonContext}
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
import leon.purescala.ExprOps._
import leon.xlang.Expressions._
-object EpsilonElimination extends TransformationPhase {
+object EpsilonElimination extends UnitPhase[Program] {
val name = "Epsilon Elimination"
val description = "Remove all epsilons from the program"
- def apply(ctx: LeonContext, pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program) = {
- val allFuns = pgm.definedFunctions
for {
- fd <- allFuns
+ fd <- pgm.definedFunctions
body <- fd.body
} {
val newBody = postMap{
@@ -37,7 +35,6 @@ object EpsilonElimination extends TransformationPhase {
}(body)
fd.body = Some(newBody)
}
- pgm
}
}
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 400716980..2198605ee 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -16,10 +16,10 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
- val pgm1 = ArrayTransformation(ctx, pgm)
- val pgm2 = EpsilonElimination(ctx, pgm1)
- val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
- val pgm4 = purescala.FunctionClosure.run(ctx)(pgm3)
+ ArrayTransformation(ctx, pgm) // In-place
+ EpsilonElimination(ctx, pgm) // In-place
+ val (pgm1, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm)
+ val pgm2 = purescala.FunctionClosure.run(ctx)(pgm1)
def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
case Some(nested) => // could have been a LetDef originally
@@ -28,7 +28,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
- pgm4.definedFunctions.foreach { fd => fd.owner match {
+ pgm2.definedFunctions.foreach { fd => fd.owner match {
case Some(p : FunDef) =>
subFunctionsOf += p -> (subFunctionsOf(p) + fd)
case _ =>
@@ -54,7 +54,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
case opt => opt
}
- val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
+ val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm2)
completeVerificationReport(vr, functionWasLoop)
}
--
GitLab