Embed information about function closures within trees. Simpler phase.

src/main/scala/leon/purescala/Definitions.scala

@@ -317,6 +317,10 @@ object Definitions {
     var precondition: Option[Expr] = None
     var postcondition: Option[Expr] = None
 
+    // Metadata kept here after transformations
+    var parent: Option[FunDef] = None
+    var orig: Option[FunDef] = None
+
     def hasImplementation : Boolean = body.isDefined
     def hasBody = hasImplementation
     def hasPrecondition : Boolean = precondition.isDefined

src/main/scala/leon/xlang/FunctionClosure.scala

@@ -13,7 +13,7 @@ import leon.purescala.TreeOps._
 import leon.purescala.TypeTrees._
 import leon.xlang.Trees._
 
-object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef], Map[FunDef, FunDef])] {
+object FunctionClosure extends TransformationPhase {
 
   val name = "Function Closure"
   val description = "Closing function with its scoping variables"
@@ -24,20 +24,14 @@ object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef],
   private var newFunDefs: Map[FunDef, FunDef] = Map()
   private var topLevelFuns: Set[FunDef] = Set()
   private var parent: FunDef = null //refers to the current toplevel parent
-  private var parents: Map[FunDef, FunDef] = null //each hoisted function mapped to its original parent
-  private var freshFunDefs: Map[FunDef, FunDef] = null //mapping from original FunDef in LetDef to the fresh ones
-  /* but notice the private keyword */
 
-  //return modified program, new funDef to their original parents, old FunDef to freshly introduced FunDef
-  def run(ctx: LeonContext)(program: Program): (Program, Map[FunDef, FunDef], Map[FunDef, FunDef]) = {
+  def apply(ctx: LeonContext, program: Program): Program = {
 
     pathConstraints = Nil
     enclosingLets  = Nil
     newFunDefs  = Map()
     topLevelFuns = Set()
     parent = null
-    parents = Map()
-    freshFunDefs = Map()
 
     val funDefs = program.definedFunctions
     funDefs.foreach(fd => {
@@ -47,7 +41,7 @@ object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef],
     })
     val Program(id, ObjectDef(objId, defs, invariants)) = program
     val res = Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
-    (res, parents, freshFunDefs)
+    res
   }
 
   private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
@@ -68,8 +62,9 @@ object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef],
       val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
       topLevelFuns += newFunDef
       newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
-      parents += (newFunDef -> parent)
-      freshFunDefs += (fd -> newFunDef)
+      newFunDef.parent = Some(parent)
+      fd.parent        = Some(parent)
+      newFunDef.orig   = Some(fd)
 
       def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
         val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {

src/main/scala/leon/xlang/XlangAnalysisPhase.scala

@@ -16,17 +16,20 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
     val pgm1 = ArrayTransformation(ctx, pgm)
     val pgm2 = EpsilonElimination(ctx, pgm1)
     val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
-    val (pgm4, parents, freshFunDefs) = FunctionClosure.run(ctx)(pgm3)
+    val pgm4 = FunctionClosure.run(ctx)(pgm3)
 
-    val originalFunDefs = freshFunDefs.map(x => (x._2, x._1))
-
-    def functionWasLoop(fd: FunDef): Boolean = originalFunDefs.get(fd) match {
+    def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
       case None => false //meaning, this was a top level function
       case Some(nested) => wasLoop.contains(nested) //could have been a LetDef originally
     }
-    def subFunctionsOf(fd: FunDef): Set[FunDef] = parents.flatMap((p: (FunDef, FunDef)) => p match {
-      case (child, parent) => if(parent == fd) List(child) else List() 
-    }).toSet
+
+    var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
+    pgm4.definedFunctions.foreach { fd => fd.parent match {
+      case Some(p) =>
+        subFunctionsOf += p -> (subFunctionsOf(p) + fd)
+      case _ =>
+    }}
+
 
     val newOptions = ctx.options map {
       case LeonValueOption("functions", ListValue(fs)) => {
@@ -41,17 +44,17 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
             case None =>
           }
         })
-        
+
         LeonValueOption("functions", ListValue(freshToAnalyse.toList))
       }
       case opt => opt
     }
 
     val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
-    completeVerificationReport(vr, parents, functionWasLoop _)
+    completeVerificationReport(vr, functionWasLoop _)
   }
 
-  def completeVerificationReport(vr: VerificationReport, parents: Map[FunDef, FunDef], functionWasLoop: FunDef => Boolean): VerificationReport = {
+  def completeVerificationReport(vr: VerificationReport, functionWasLoop: FunDef => Boolean): VerificationReport = {
     val vcs = vr.conditions
 
     //this is enough to convert invariant postcondition and inductive conditions. However the initial validity
@@ -66,7 +69,7 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
       if(functionWasLoop(funDef)) {
         val freshVc = new VerificationCondition(
           vc.condition, 
-          parents(funDef), 
+          funDef.parent.getOrElse(funDef), 
           if(vc.kind == VCKind.Postcondition) VCKind.InvariantPost else if(vc.kind == VCKind.Precondition) VCKind.InvariantInd else vc.kind,
           vc.tactic,
           vc.info).setPosInfo(funDef)