xlang does nothing unless needed

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,

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]])

src/main/scala/leon/xlang/ArrayTransformation.scala

-/* 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)
-    )
-  }
-
-}

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
+  }
+
 }

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