From c7aea6cf8b829580060b96b1d1b994490cc01cab Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 17 Mar 2016 17:53:59 +0100
Subject: [PATCH] xlang does nothing unless needed
---
src/main/scala/leon/Main.scala | 2 +-
.../scala/leon/xlang/AntiAliasingPhase.scala | 16 ++++-----
.../leon/xlang/ArrayTransformation.scala | 35 -------------------
.../xlang/ImperativeCodeElimination.scala | 10 +++++-
.../leon/xlang/XLangDesugaringPhase.scala | 1 -
5 files changed, 18 insertions(+), 46 deletions(-)
delete mode 100644 src/main/scala/leon/xlang/ArrayTransformation.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 02a21c508..1c1e52b17 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -13,7 +13,7 @@ object Main {
utils.TypingPhase,
utils.FileOutputPhase,
purescala.RestoreMethods,
- xlang.ArrayTransformation,
+ xlang.AntiAliasingPhase,
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
xlang.FixReportLabels,
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index d237c89d5..f1ea90043 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -63,8 +63,8 @@ object AntiAliasingPhase extends TransformationPhase {
/*
* Create a new FunDef for a given FunDef in the program.
* Adapt the signature to express its effects. In case the
- * function has no effect, this will still introduce a fresh
- * FunDef as the body might have to be updated anyway.
+ * function has no effect, this will still return the original
+ * fundef.
*/
private def updateFunDef(fd: FunDef, effects: Effects)(ctx: LeonContext): FunDef = {
@@ -87,13 +87,13 @@ object AntiAliasingPhase extends TransformationPhase {
// case _ => ()
//})
- val newReturnType: TypeTree = if(aliasedParams.isEmpty) fd.returnType else {
- tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
+ if(aliasedParams.isEmpty) fd else {
+ val newReturnType: TypeTree = tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
+ val newFunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, newReturnType)
+ newFunDef.addFlags(fd.flags)
+ newFunDef.setPos(fd)
+ newFunDef
}
- val newFunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, newReturnType)
- newFunDef.addFlags(fd.flags)
- newFunDef.setPos(fd)
- newFunDef
}
private def updateBody(fd: FunDef, effects: Effects, updatedFunDefs: Map[FunDef, FunDef], varsInScope: Map[FunDef, Set[Identifier]])
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
deleted file mode 100644
index 7c66bc3eb..000000000
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.xlang
-
-import leon.UnitPhase
-import leon.LeonContext
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps.simplePostTransform
-import leon.purescala.Extractors.IsTyped
-import leon.purescala.Types.ArrayType
-import leon.xlang.Expressions._
-
-object ArrayTransformation extends UnitPhase[Program] {
-
- val name = "Array Transformation"
- val description = "Remove side-effectful array updates"
-
- def apply(ctx: LeonContext, pgm: Program) = {
- pgm.definedFunctions.foreach(fd =>
- fd.fullBody = simplePostTransform {
- case up@ArrayUpdate(a, i, v) =>
- val ra@Variable(id) = a
- Assignment(id, ArrayUpdated(ra, i, v).setPos(up)).setPos(up)
-
- case l@Let(i, IsTyped(v, ArrayType(_)), b) =>
- LetVar(i, v, b).setPos(l)
-
- case e =>
- e
- }(fd.fullBody)
- )
- }
-
-}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 89a5ad4cd..de75b7a29 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -21,7 +21,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
def apply(ctx: LeonContext, pgm: Program): Unit = {
for {
fd <- pgm.definedFunctions
- body <- fd.body
+ body <- fd.body if exists(requireRewriting)(body)
} {
val (res, scope, _) = toFunction(body)(State(fd, Set(), Map()))
fd.body = Some(scope(res))
@@ -351,4 +351,12 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
})(expr)
}
+ private def requireRewriting(expr: Expr) = expr match {
+ case (e: Block) => true
+ case (e: Assignment) => true
+ case (e: While) => true
+ case (e: LetVar) => true
+ case _ => false
+ }
+
}
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index 51c2721d0..54e298a22 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -12,7 +12,6 @@ object XLangDesugaringPhase extends LeonPhase[Program, Program] {
override def run(ctx: LeonContext, pgm: Program): (LeonContext, Program) = {
val phases =
- //ArrayTransformation andThen
AntiAliasingPhase andThen
EpsilonElimination andThen
ImperativeCodeElimination
--
GitLab