From 53343bf12f3286f30d36b36752fac39a7326cbde Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Sat, 13 Jul 2013 19:03:29 +0200
Subject: [PATCH] Embed information about function closures within trees.
Simpler phase.
---
.../scala/leon/purescala/Definitions.scala | 4 +++
.../scala/leon/xlang/FunctionClosure.scala | 17 +++++--------
.../scala/leon/xlang/XlangAnalysisPhase.scala | 25 +++++++++++--------
3 files changed, 24 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index ae14f7b62..93a51b9f5 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/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
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 8ade819e4..3b6a74394 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/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) => {
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 13c8d619f..4fb3c98bc 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/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)
--
GitLab