diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9ec20b64184f8298431b2fe540e8158d70c39ae3..0ffca50ba25cd39956aeeefe16c114e1498dfdbb 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -672,7 +672,7 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
}
- new LeonModuleDef(FreshIdentifier(nameStr), newDefs)
+ LeonModuleDef(FreshIdentifier(nameStr), newDefs, nameStr contains "$standalone")
}
@@ -728,7 +728,7 @@ trait CodeExtraction extends ASTExtractors {
NoTree(funDef.returnType)
}
- funDef.fullBody = finalBody;
+ funDef.fullBody = finalBody
// Post-extraction sanity checks
@@ -751,12 +751,12 @@ trait CodeExtraction extends ASTExtractors {
private def extractPattern(p: Tree, binder: Option[Identifier] = None)(implicit dctx: DefContext): (Pattern, DefContext) = p match {
case b @ Bind(name, t @ Typed(pat, tpt)) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(tpt)).setPos(b.pos)
+ val newID = FreshIdentifier(name.toString).setType(extractType(tpt)).setPos(b.pos).setOwner(currentFunDef)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(t, Some(newID))(pctx)
case b @ Bind(name, pat) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(b)).setPos(b.pos)
+ val newID = FreshIdentifier(name.toString).setType(extractType(b)).setPos(b.pos).setOwner(currentFunDef)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(pat, Some(newID))(pctx)
@@ -839,7 +839,7 @@ trait CodeExtraction extends ASTExtractors {
val res = current match {
case ExEnsuredExpression(body, resVd, contract) =>
- val resId = FreshIdentifier(resVd.symbol.name.toString).setType(extractType(current)).setPos(resVd.pos)
+ val resId = FreshIdentifier(resVd.symbol.name.toString).setType(extractType(current)).setPos(resVd.pos).setOwner(currentFunDef)
val post = extractTree(contract)(dctx.withNewVar(resVd.symbol -> (() => Variable(resId))))
val b = try {
@@ -852,7 +852,7 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(b, resId, post)
case t @ ExHoldsExpression(body) =>
- val resId = FreshIdentifier("holds").setType(BooleanType).setPos(current.pos)
+ val resId = FreshIdentifier("holds").setType(BooleanType).setPos(current.pos).setOwner(currentFunDef)
val post = Variable(resId).setPos(current.pos)
val b = try {
@@ -918,7 +918,7 @@ trait CodeExtraction extends ASTExtractors {
case ExValDef(vs, tpt, bdy) =>
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe).setOwner(currentFunDef)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -953,7 +953,7 @@ trait CodeExtraction extends ASTExtractors {
val oldCurrentFunDef = currentFunDef
- val funDefWithBody = extractFunBody(fd, params, b)(newDctx.copy(mutableVars = Map()))
+ val funDefWithBody = extractFunBody(fd, params, b)(newDctx.copy(mutableVars = Map())).setOwner(oldCurrentFunDef)
currentFunDef = oldCurrentFunDef
@@ -970,7 +970,7 @@ trait CodeExtraction extends ASTExtractors {
case ExVarDef(vs, tpt, bdy) => {
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe).setOwner(currentFunDef)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -1094,7 +1094,7 @@ trait CodeExtraction extends ASTExtractors {
val newOracles = oracles map { case (tpt, sym) =>
val aTpe = extractType(tpt)
val oTpe = oracleType(ops.pos, aTpe)
- val newID = FreshIdentifier(sym.name.toString).setType(oTpe)
+ val newID = FreshIdentifier(sym.name.toString).setType(oTpe).setOwner(currentFunDef)
owners += (newID -> None)
newID
}
@@ -1112,7 +1112,7 @@ trait CodeExtraction extends ASTExtractors {
case chs @ ExChooseExpression(args, body) =>
val vars = args map { case (tpt, sym) =>
val aTpe = extractType(tpt)
- val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
+ val newID = FreshIdentifier(sym.name.toString).setType(aTpe).setOwner(currentFunDef)
owners += (newID -> None)
newID
}
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 28b197b474440807b78d55f997bf69ff93603608..dd1a6de02e35913f3a2ab11365c49eef3f2597c1 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -4,6 +4,7 @@ package leon
package purescala
import utils._
+import Definitions.Definition
object Common {
import Trees.Variable
@@ -54,6 +55,16 @@ object Common {
def toVariable : Variable = Variable(this)
def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
+
+ var owner : Option[Definition] = None
+
+ def setOwner(df : Definition) : Identifier = { this.owner = Some(df); this }
+
+ def ownerChain : List[Identifier] = owner match {
+ case None => List(this)
+ case Some(ow) => ow.id :: ow.id.ownerChain
+ }
+
}
private object UniqueCounter {
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 1932cfd6de3d39889b46c6e47b89ede74425d395..582ebba3c9f17ab4fc615de76bd0e0f6366fa974 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -14,8 +14,14 @@ object Definitions {
import TypeTreeOps._
sealed abstract class Definition extends Tree {
+
val id: Identifier
- var enclosing : Option[Definition] = None // The definition/scope enclosing this definition
+
+ def owner = id.owner
+ def setOwner(owner : Definition) : this.type = { id.owner = Some(owner); this }
+
+ var origOwner : Option[Definition] = None // The definition/scope enclosing this definition
+
def subDefinitions : Seq[Definition] // The enclosed scopes/definitions by this definition
override def hashCode : Int = id.hashCode
override def equals(that : Any) : Boolean = that match {
@@ -25,12 +31,15 @@ object Definitions {
override def copiedFrom(o : Tree) : this.type = {
super.copiedFrom(o)
o match {
- case df : Definition => enclosing = df.enclosing
- case _ => // FIXME should this ever happen?
+ case df : Definition if df.owner.isDefined => this.setOwner(df.owner.get)
+ case _ => this // FIXME should this ever happen?
}
- this
+
}
+ // TODO: this seems quite elegant, but make sure it works
+ def setSubDefOwners() = for (df <- subDefinitions) df.setOwner(this)
+
}
/** A ValDef declares a new identifier to be of a certain type. */
@@ -47,12 +56,13 @@ object Definitions {
}
def toVariable : Variable = Variable(id).setType(tpe)
+ setSubDefOwners()
}
/** A wrapper for a program. For now a program is simply a single object. The
* name is meaningless and we just use the package name as id. */
case class Program(id: Identifier, units: List[UnitDef]) extends Definition {
- enclosing = None
+ origOwner = None
def subDefinitions = units
def definedFunctions = units.flatMap(_.definedFunctions)
@@ -79,6 +89,7 @@ object Definitions {
out.write(ScalaPrinter(this))
out.close
}
+ setSubDefOwners()
}
object Program {
@@ -91,9 +102,11 @@ object Definitions {
case class TypeParameterDef(tp: TypeParameter) extends Definition {
def subDefinitions = Seq()
val id = tp.id
+ setSubDefOwners()
}
+
object UnitDef {
def apply(id : Identifier, modules : Seq[ModuleDef]) : UnitDef = UnitDef(id,modules, true)
}
@@ -124,13 +137,15 @@ object Definitions {
out.write(ScalaPrinter(this))
out.close
}
+
+ setSubDefOwners()
}
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
- case class ModuleDef(id: Identifier, defs : Seq[Definition]) extends Definition {
+ case class ModuleDef(id: Identifier, defs : Seq[Definition], isSynthetic : Boolean = false) extends Definition {
def subDefinitions = defs
@@ -156,6 +171,7 @@ object Definitions {
case other => other // FIXME: huh?
}})
+ setSubDefOwners()
}
@@ -164,7 +180,7 @@ object Definitions {
sealed trait ClassDef extends Definition {
self =>
- def subDefinitions = methods
+ def subDefinitions = fields ++ methods ++ tparams
val id: Identifier
val tparams: Seq[TypeParameterDef]
@@ -185,6 +201,7 @@ object Definitions {
def registerMethod(fd: FunDef) = {
_methods = _methods ::: List(fd)
+ fd.setOwner(this)
}
def clearMethods() {
@@ -228,6 +245,7 @@ object Definitions {
lazy val definedFunctions : Seq[FunDef] = methods
lazy val definedClasses = Seq(this)
lazy val classHierarchyRoots = if (this.hasParent) Seq(this) else Nil
+
}
/** Abstract classes. */
@@ -240,7 +258,7 @@ object Definitions {
val isCaseObject = false
lazy val singleCaseClasses : Seq[CaseClassDef] = Nil
-
+ setSubDefOwners()
}
/** Case classes/objects. */
@@ -249,12 +267,13 @@ object Definitions {
val parent: Option[AbstractClassType],
val isCaseObject: Boolean) extends ClassDef {
- var _fields = Seq[ValDef]()
+ private var _fields = Seq[ValDef]()
def fields = _fields
def setFields(fields: Seq[ValDef]) {
_fields = fields
+ _fields foreach { _.setOwner(this)}
}
@@ -270,7 +289,7 @@ object Definitions {
}
lazy val singleCaseClasses : Seq[CaseClassDef] = if (hasParent) Nil else Seq(this)
-
+ setSubDefOwners()
}
@@ -300,26 +319,31 @@ object Definitions {
val defType : DefType
) extends Definition {
- var fullBody: Expr = NoTree(returnType)
+ private var fullBody_ : Expr = NoTree(returnType)
+ def fullBody = fullBody_
+ def fullBody_= (e : Expr) {
+ fullBody_ = e
+ nestedFuns map {_.setOwner(this)}
+ }
def body: Option[Expr] = withoutSpec(fullBody)
- def body_=(b: Option[Expr]) = fullBody = withBody(fullBody, b)
+ def body_=(b: Option[Expr]) = {
+ fullBody = withBody(fullBody, b)
+ }
def precondition = preconditionOf(fullBody)
def precondition_=(oe: Option[Expr]) = {
- fullBody = withPrecondition(fullBody, oe)
+ fullBody = withPrecondition(fullBody, oe)
}
def postcondition = postconditionOf(fullBody)
def postcondition_=(op: Option[(Identifier, Expr)]) = {
- fullBody = withPostcondition(fullBody, op)
+ fullBody = withPostcondition(fullBody, op)
}
- def subDefinitions = Seq()
-
- // Metadata kept here after transformations
- var parent: Option[FunDef] = None
- var orig: Option[FunDef] = None
+ def nestedFuns = directlyNestedFunDefs(fullBody)
+
+ def subDefinitions = params ++ tparams ++ nestedFuns.toList
def duplicate: FunDef = {
val fd = new FunDef(id, tparams, returnType, params, defType)
@@ -328,10 +352,10 @@ object Definitions {
}
def copyContentFrom(from : FunDef) {
- this.fullBody = from.fullBody
- this.parent = from.parent
- this.orig = from.orig
- this.enclosing = from.enclosing
+ this.fullBody = from.fullBody
+ //this.parent = from.parent
+ //this.orig = from.orig
+ this.origOwner = from.origOwner
this.addAnnotation(from.annotations.toSeq : _*)
}
@@ -367,6 +391,7 @@ object Definitions {
TypedFunDef(this, Nil)
}
+ setSubDefOwners()
// Deprecated, old API
@deprecated("Use .body instead", "2.3")
def implementation : Option[Expr] = body
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 5151f2b708a1448922370697f96f452107c14eaf..225070f6f834f99a8bd357f28108aa8b3e892216 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -62,9 +62,9 @@ object FunctionClosure extends TransformationPhase {
val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs, fd.defType).copiedFrom(fd)
topLevelFuns += newFunDef
newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
- newFunDef.parent = Some(parent)
- fd.parent = Some(parent)
- newFunDef.orig = Some(fd)
+ newFunDef.setOwner(parent)
+ fd .setOwner(parent)
+ newFunDef.origOwner = 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/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7338b58107e1f4c9e9ae0981f33c09c5d6365ae4..c661714b84193325daf86d48947ec05009590101 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -372,16 +372,17 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
// Definitions
- case Program(id, units) =>
- p"""${nary(units, "\n\n")}"""
+ case Program(id, units) =>
+ p"""${nary(units, "\n\n")}"""
+
case UnitDef(id,modules,isBasic) =>
if (isBasic) {
p"""|package $id {
| ${nary(modules,"\n\n")}
|}"""
}
- case ModuleDef(id, defs) =>
+ case ModuleDef(id, defs, _) =>
p"""|object $id {
| ${nary(defs, "\n\n")}
|}"""
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 0a808649884927dada2f31a1f14ea8957ea335ae..0b44f5d55eebfe1ae5b4bec7e162adbda9df2d2b 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -21,7 +21,7 @@ object RestoreMethods extends TransformationPhase {
var fd2Md = Map[FunDef, FunDef]()
var whoseMethods = Map[ClassDef, Seq[FunDef]]()
- for ( (Some(cd : ClassDef), funDefs) <- p.definedFunctions.groupBy(_.enclosing).toSeq ) {
+ for ( (Some(cd : ClassDef), funDefs) <- p.definedFunctions.groupBy(_.origOwner).toSeq ) {
whoseMethods += cd -> funDefs
for (fn <- funDefs) {
val theName = try {
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 67cec4c0e39105361c8fa84358a1c012f1a44a97..2277f606037279c0091681c61f39922e20c680ed 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -368,7 +368,15 @@ object TreeOps {
case _ => Set()
}(expr)
}
-
+
+ /** Returns functions in directly nested LetDefs */
+ def directlyNestedFunDefs(e: Expr): Set[FunDef] = {
+ foldRight[Set[FunDef]]{
+ case (LetDef(fd,bd), _) => Set(fd)
+ case (_, subs) => subs.foldLeft(Set[FunDef]())(_ ++ _)
+ }(e)
+ }
+
def negate(expr: Expr) : Expr = (expr match {
case Let(i,b,e) => Let(i,b,negate(e))
case Not(e) => e
diff --git a/src/main/scala/leon/utils/ScopingPhase.scala b/src/main/scala/leon/utils/ScopingPhase.scala
index deb2e8a13689eef50d1993295c10f512938c2e47..839f53855bf50e5db10ac3a43ebdf9f8eb597342 100644
--- a/src/main/scala/leon/utils/ScopingPhase.scala
+++ b/src/main/scala/leon/utils/ScopingPhase.scala
@@ -15,7 +15,7 @@ object ScopingPhase extends UnitPhase[Program] {
}
private def insertScopingInformation(df : Definition , parent : Option[Definition]) {
- df.enclosing = parent
+ df.origOwner = parent
for (sub <- df.subDefinitions){
insertScopingInformation(sub, Some(df))
}
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 3d236b1b4810570fc11e494722a71c025f8633d3..3ec56711560a4a2e3750a729410950bccd292fbf 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -21,14 +21,15 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
val pgm4 = purescala.FunctionClosure.run(ctx)(pgm3)
- 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 functionWasLoop(fd: FunDef): Boolean = fd.origOwner match {
+ case Some(nested : FunDef) => // was a nested function
+ wasLoop.contains(nested)
+ case _ => false //meaning, this was a top level function
}
var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
- pgm4.definedFunctions.foreach { fd => fd.parent match {
- case Some(p) =>
+ pgm4.definedFunctions.foreach { fd => fd.owner match {
+ case Some(p : FunDef) =>
subFunctionsOf += p -> (subFunctionsOf(p) + fd)
case _ =>
}}
@@ -72,7 +73,7 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
if(functionWasLoop(funDef)) {
val freshVc = new VerificationCondition(
vc.condition,
- funDef.parent.getOrElse(funDef),
+ funDef.owner match { case Some(fd : FunDef) => fd; case _ => funDef },
if(vc.kind == VCPostcondition) VCInvariantPost else if(vc.kind == VCPrecondition) VCInvariantInd else vc.kind,
vc.tactic,
vc.info).setPos(funDef)