From 3e4b964f48bffbbbde7404ea7dc9653955e5c339 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 15 Jan 2016 13:09:20 +0100
Subject: [PATCH] remove owners check in frontend
---
.../frontends/scalac/CodeExtraction.scala | 85 +------------------
1 file changed, 1 insertion(+), 84 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3e9366400..5a9193033 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -137,10 +137,6 @@ trait CodeExtraction extends ASTExtractors {
private var currentFunDef: FunDef = null
- //This is a bit misleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
- //that it can have any owner
- private var owners: Map[Identifier, Option[FunDef]] = Map()
-
// This one never fails, on error, it returns Untyped
def leonType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = {
try {
@@ -639,7 +635,6 @@ trait CodeExtraction extends ASTExtractors {
val ptpe = leonType(sym.tpe)(nctx, sym.pos)
val tpe = if (sym.isByNameParam) FunctionType(Seq(), ptpe) else ptpe
val newID = FreshIdentifier(sym.name.toString, tpe).setPos(sym.pos)
- owners += (newID -> None)
val vd = LeonValDef(newID).setPos(sym.pos)
if (sym.isByNameParam) {
@@ -798,21 +793,7 @@ trait CodeExtraction extends ASTExtractors {
}} else body0
val finalBody = try {
- flattenBlocks(extractTreeOrNoTree(body)(fctx)) match {
- case e if e.getType.isInstanceOf[ArrayType] =>
- getOwner(e) match {
- case Some(Some(fd)) if fd == funDef =>
- e
-
- case None =>
- e
-
- case _ =>
- outOfSubsetError(body, "Function cannot return an array that is not locally defined")
- }
- case e =>
- e
- }
+ flattenBlocks(extractTreeOrNoTree(body)(fctx))
} catch {
case e: ImpureCodeEncounteredException =>
e.emit()
@@ -1090,15 +1071,6 @@ trait CodeExtraction extends ASTExtractors {
val newID = FreshIdentifier(vs.name.toString, binderTpe)
val valTree = extractTree(bdy)
- if(valTree.getType.isInstanceOf[ArrayType]) {
- getOwner(valTree) match {
- case None =>
- owners += (newID -> Some(currentFunDef))
- case _ =>
- outOfSubsetError(tr, "Cannot alias array")
- }
- }
-
val restTree = rest match {
case Some(rst) =>
val nctx = dctx.withNewVar(vs -> (() => Variable(newID)))
@@ -1151,15 +1123,6 @@ trait CodeExtraction extends ASTExtractors {
val newID = FreshIdentifier(vs.name.toString, binderTpe)
val valTree = extractTree(bdy)
- if(valTree.getType.isInstanceOf[ArrayType]) {
- getOwner(valTree) match {
- case None =>
- owners += (newID -> Some(currentFunDef))
- case Some(_) =>
- outOfSubsetError(tr, "Cannot alias array")
- }
- }
-
val restTree = rest match {
case Some(rst) => {
val nv = vs -> (() => Variable(newID))
@@ -1178,9 +1141,6 @@ trait CodeExtraction extends ASTExtractors {
case Some(fun) =>
val Variable(id) = fun()
val rhsTree = extractTree(rhs)
- if(rhsTree.getType.isInstanceOf[ArrayType] && getOwner(rhsTree).isDefined) {
- outOfSubsetError(tr, "Cannot alias array")
- }
Assignment(id, rhsTree)
case None =>
@@ -1223,18 +1183,6 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Array update only works on variables")
}
- getOwner(lhsRec) match {
- // case Some(Some(fd)) if fd != currentFunDef =>
- // outOfSubsetError(tr, "cannot update an array that is not defined locally")
-
- // case Some(None) =>
- // outOfSubsetError(tr, "cannot update an array that is not defined locally")
-
- case Some(_) =>
-
- case None => sys.error("This array: " + lhsRec + " should have had an owner")
- }
-
val indexRec = extractTree(index)
val newValueRec = extractTree(newValue)
ArrayUpdate(lhsRec, indexRec, newValueRec)
@@ -1309,7 +1257,6 @@ trait CodeExtraction extends ASTExtractors {
val aTpe = extractType(tpt)
val oTpe = oracleType(ops.pos, aTpe)
val newID = FreshIdentifier(sym.name.toString, oTpe)
- owners += (newID -> None)
newID
}
@@ -1331,7 +1278,6 @@ trait CodeExtraction extends ASTExtractors {
val vds = args map { vd =>
val aTpe = extractType(vd.tpt)
val newID = FreshIdentifier(vd.symbol.name.toString, aTpe)
- owners += (newID -> None)
LeonValDef(newID)
}
@@ -1347,7 +1293,6 @@ trait CodeExtraction extends ASTExtractors {
val vds = args map { case (tpt, sym) =>
val aTpe = extractType(tpt)
val newID = FreshIdentifier(sym.name.toString, aTpe)
- owners += (newID -> None)
LeonValDef(newID)
}
@@ -1908,34 +1853,6 @@ trait CodeExtraction extends ASTExtractors {
}
}
- private def getReturnedExpr(expr: LeonExpr): Seq[LeonExpr] = expr match {
- case Let(_, _, rest) => getReturnedExpr(rest)
- case LetVar(_, _, rest) => getReturnedExpr(rest)
- case LeonBlock(_, rest) => getReturnedExpr(rest)
- case IfExpr(_, thenn, elze) => getReturnedExpr(thenn) ++ getReturnedExpr(elze)
- case MatchExpr(_, cses) => cses.flatMap{ cse => getReturnedExpr(cse.rhs) }
- case _ => Seq(expr)
- }
-
- def getOwner(exprs: Seq[LeonExpr]): Option[Option[FunDef]] = {
- val exprOwners: Seq[Option[Option[FunDef]]] = exprs.map {
- case Variable(id) =>
- owners.get(id)
- case _ =>
- None
- }
-
- if(exprOwners.contains(None))
- None
- else if(exprOwners.contains(Some(None)))
- Some(None)
- else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
- Some(None)
- else
- exprOwners.head
- }
-
- def getOwner(expr: LeonExpr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
}
def containsLetDef(expr: LeonExpr): Boolean = {
--
GitLab