diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 96215b68b268752f7534a2b9fe0dc23db1d38cbf..c5877e1e4d3705c67ebe51eb97c57daf8da58b33 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 = {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 1cee46865717b0e214e66ff41fac0c07039031fa..724f6a0fca6e4b2c91c1d288013ef8fb9a817b41 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -213,6 +213,49 @@ object ExprOps {
}
+ /** Pre-transformation of the tree, with a context value from "top-down".
+ *
+ * Takes a partial function of replacements.
+ * Substitutes '''before''' recursing down the trees. The function returns
+ * an option of the new value, as well as the new context to be used for
+ * the recursion in its children. The context is "lost" when going back up,
+ * so changes made by one node will not be see by its siblings.
+ */
+ def preMapWithContext[C](f: (Expr, C) => (Option[Expr], C), applyRec: Boolean = false)
+ (e: Expr, c: C): Expr = {
+
+ def rec(expr: Expr, context: C): Expr = {
+
+ val (newV, newCtx) = {
+ if(applyRec) {
+ var ctx = context
+ val finalV = fixpoint{ e: Expr => {
+ val res = f(e, ctx)
+ ctx = res._2
+ res._1.getOrElse(e)
+ }} (expr)
+ (finalV, ctx)
+ } else {
+ val res = f(expr, context)
+ (res._1.getOrElse(expr), res._2)
+ }
+ }
+
+ val Operator(es, builder) = newV
+ val newEs = es.map(e => rec(e, newCtx))
+
+ if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
+ builder(newEs).copiedFrom(newV)
+ } else {
+ newV
+ }
+
+ }
+
+ rec(e, c)
+ }
+
+
/** Applies functions and combines results in a generic way
*
* Start with an initial value, and apply functions to nodes before
@@ -376,6 +419,14 @@ object ExprOps {
}(expr)
}
+ /** Returns all Function calls found in the expression */
+ def nestedFunDefsOf(expr: Expr): Set[FunDef] = {
+ collect[FunDef] {
+ case LetDef(fds, _) => fds.toSet
+ case _ => Set()
+ }(expr)
+ }
+
/** Returns functions in directly nested LetDefs */
def directlyNestedFunDefs(e: Expr): Set[FunDef] = {
fold[Set[FunDef]]{
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7eb391088ea64c276aa0bbf7836e4a9511aa978c
--- /dev/null
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -0,0 +1,383 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+package leon.xlang
+
+import leon.TransformationPhase
+import leon.LeonContext
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.DefOps._
+import leon.purescala.Types._
+import leon.purescala.Constructors._
+import leon.purescala.Extractors._
+import leon.xlang.Expressions._
+
+object AntiAliasingPhase extends TransformationPhase {
+
+ val name = "Anti-Aliasing"
+ val description = "Make aliasing explicit"
+
+ override def apply(ctx: LeonContext, pgm: Program): Program = {
+ val fds = allFunDefs(pgm)
+ fds.foreach(fd => checkAliasing(fd)(ctx))
+
+ var updatedFunctions: Map[FunDef, FunDef] = Map()
+
+ val effects = effectsAnalysis(pgm)
+
+ //for each fun def, all the vars the the body captures. Only
+ //mutable types.
+ val varsInScope: Map[FunDef, Set[Identifier]] = (for {
+ fd <- fds
+ } yield {
+ val allFreeVars = fd.body.map(bd => variablesOf(bd)).getOrElse(Set())
+ val freeVars = allFreeVars -- fd.params.map(_.id)
+ val mutableFreeVars = freeVars.filter(id => id.getType.isInstanceOf[ArrayType])
+ (fd, mutableFreeVars)
+ }).toMap
+
+ /*
+ * The first pass will introduce all new function definitions,
+ * so that in the next pass we can update function invocations
+ */
+ for {
+ fd <- fds
+ } {
+ updatedFunctions += (fd -> updateFunDef(fd, effects)(ctx))
+ }
+
+ for {
+ fd <- fds
+ } {
+ updateBody(fd, effects, updatedFunctions, varsInScope)(ctx)
+ }
+
+ val res = replaceFunDefs(pgm)(fd => updatedFunctions.get(fd), (fi, fd) => None)
+ //println(res._1)
+ res._1
+ }
+
+ /*
+ * 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.
+ */
+ private def updateFunDef(fd: FunDef, effects: Effects)(ctx: LeonContext): FunDef = {
+
+ val ownEffects = effects(fd)
+ val aliasedParams: Seq[Identifier] = fd.params.zipWithIndex.flatMap{
+ case (vd, i) if ownEffects.contains(i) => Some(vd)
+ case _ => None
+ }.map(_.id)
+
+ fd.body.foreach(body => getReturnedExpr(body).foreach{
+ case v@Variable(id) if aliasedParams.contains(id) =>
+ ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object")
+ case _ => ()
+ })
+ //val allBodies: Set[Expr] =
+ // fd.body.toSet.flatMap((bd: Expr) => nestedFunDefsOf(bd).flatMap(_.body)) ++ fd.body
+ //allBodies.foreach(body => getReturnedExpr(body).foreach{
+ // case v@Variable(id) if aliasedParams.contains(id) =>
+ // ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object: "k+ v)
+ // case _ => ()
+ //})
+
+ val newReturnType: TypeTree = if(aliasedParams.isEmpty) fd.returnType else {
+ 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
+ }
+
+ private def updateBody(fd: FunDef, effects: Effects, updatedFunDefs: Map[FunDef, FunDef], varsInScope: Map[FunDef, Set[Identifier]])
+ (ctx: LeonContext): Unit = {
+
+ val ownEffects = effects(fd)
+ val aliasedParams: Seq[Identifier] = fd.params.zipWithIndex.flatMap{
+ case (vd, i) if ownEffects.contains(i) => Some(vd)
+ case _ => None
+ }.map(_.id)
+
+ val newFunDef = updatedFunDefs(fd)
+
+ if(aliasedParams.isEmpty) {
+ val newBody = fd.body.map(body => {
+ makeSideEffectsExplicit(body, Seq(), effects, updatedFunDefs, varsInScope)(ctx)
+ })
+ newFunDef.body = newBody
+ newFunDef.precondition = fd.precondition
+ newFunDef.postcondition = fd.postcondition
+ } else {
+ val freshLocalVars: Seq[Identifier] = aliasedParams.map(v => v.freshen)
+ val rewritingMap: Map[Identifier, Identifier] = aliasedParams.zip(freshLocalVars).toMap
+
+ val newBody = fd.body.map(body => {
+
+ val freshBody = replaceFromIDs(rewritingMap.map(p => (p._1, p._2.toVariable)), body)
+ val explicitBody = makeSideEffectsExplicit(freshBody, freshLocalVars, effects, updatedFunDefs, varsInScope)(ctx)
+
+ //WARNING: only works if side effects in Tuples are extracted from left to right,
+ // in the ImperativeTransformation phase.
+ val finalBody: Expr = Tuple(explicitBody +: freshLocalVars.map(_.toVariable))
+
+ freshLocalVars.zip(aliasedParams).foldLeft(finalBody)((bd, vp) => {
+ LetVar(vp._1, Variable(vp._2), bd)
+ })
+
+ })
+
+ val newPostcondition = fd.postcondition.map(post => {
+ val Lambda(Seq(res), postBody) = post
+ val newRes = ValDef(FreshIdentifier(res.id.name, newFunDef.returnType))
+ val newBody =
+ replace(
+ aliasedParams.zipWithIndex.map{ case (id, i) =>
+ (id.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap ++
+ aliasedParams.map(id =>
+ (Old(id), id.toVariable): (Expr, Expr)).toMap +
+ (res.toVariable -> TupleSelect(newRes.toVariable, 1)),
+ postBody)
+ Lambda(Seq(newRes), newBody).setPos(post)
+ })
+
+ newFunDef.body = newBody
+ newFunDef.precondition = fd.precondition
+ newFunDef.postcondition = newPostcondition
+ }
+ }
+
+ //We turn all local val of mutable objects into vars and explicit side effects
+ //using assignments. We also make sure that no aliasing is being done.
+ private def makeSideEffectsExplicit
+ (body: Expr, aliasedParams: Seq[Identifier], effects: Effects, updatedFunDefs: Map[FunDef, FunDef], varsInScope: Map[FunDef, Set[Identifier]])
+ (ctx: LeonContext): Expr = {
+ preMapWithContext[Set[Identifier]]((expr, bindings) => expr match {
+
+ case up@ArrayUpdate(a, i, v) => {
+ val ra@Variable(id) = a
+ if(bindings.contains(id))
+ (Some(Assignment(id, ArrayUpdated(ra, i, v).setPos(up)).setPos(up)), bindings)
+ else
+ (None, bindings)
+ }
+
+ case l@Let(id, IsTyped(v, ArrayType(_)), b) => {
+ val varDecl = LetVar(id, v, b).setPos(l)
+ (Some(varDecl), bindings + id)
+ }
+
+ case l@LetVar(id, IsTyped(v, ArrayType(_)), b) => {
+ (None, bindings + id)
+ }
+
+ //we need to replace local fundef by the new updated fun defs.
+ case l@LetDef(fds, body) => {
+ //this might be traversed several time in case of doubly nested fundef,
+ //so we need to ignore the second times by checking if updatedFunDefs
+ //contains a mapping or not
+ val nfds = fds.map(fd => updatedFunDefs.get(fd).getOrElse(fd))
+ (Some(LetDef(nfds, body)), bindings)
+ }
+
+ case fi@FunctionInvocation(fd, args) => {
+
+ val vis: Set[Identifier] = varsInScope.get(fd.fd).getOrElse(Set())
+ args.find({
+ case Variable(id) => vis.contains(id)
+ case _ => false
+ }).foreach(aliasedArg =>
+ ctx.reporter.fatalError(aliasedArg.getPos, "Illegal passing of aliased parameter: " + aliasedArg))
+
+ updatedFunDefs.get(fd.fd) match {
+ case None => (None, bindings)
+ case Some(nfd) => {
+ val nfi = FunctionInvocation(nfd.typed(fd.tps), args).setPos(fi)
+ val fiEffects = effects.getOrElse(fd.fd, Set())
+ if(fiEffects.nonEmpty) {
+ val modifiedArgs: Seq[Variable] =
+ args.zipWithIndex.filter{ case (arg, i) => fiEffects.contains(i) }
+ .map(_._1.asInstanceOf[Variable])
+
+ val duplicatedParams = modifiedArgs.diff(modifiedArgs.distinct).distinct
+ if(duplicatedParams.nonEmpty)
+ ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
+
+ val freshRes = FreshIdentifier("res", nfd.returnType)
+
+ val extractResults = Block(
+ modifiedArgs.zipWithIndex.map(p => Assignment(p._1.id, TupleSelect(freshRes.toVariable, p._2 + 2))),
+ TupleSelect(freshRes.toVariable, 1))
+
+
+ val newExpr = Let(freshRes, nfi, extractResults)
+ (Some(newExpr), bindings)
+ } else {
+ (Some(nfi), bindings)
+ }
+ }
+ }
+ }
+
+ case _ => (None, bindings)
+
+ })(body, aliasedParams.toSet)
+ }
+
+ //TODO: in the future, any object with vars could be aliased and so
+ // we will need a general property
+
+ private type Effects = Map[FunDef, Set[Int]]
+
+ /*
+ * compute effects for each function in the program, including any nested
+ * functions (LetDef).
+ */
+ private def effectsAnalysis(pgm: Program): Effects = {
+
+ //currently computed effects (incremental)
+ var effects: Map[FunDef, Set[Int]] = Map()
+ //missing dependencies for a function for its effects to be complete
+ var missingEffects: Map[FunDef, Set[FunctionInvocation]] = Map()
+
+ def effectsFullyComputed(fd: FunDef): Boolean = !missingEffects.isDefinedAt(fd)
+
+ for {
+ fd <- allFunDefs(pgm)
+ } {
+ fd.body match {
+ case None =>
+ effects += (fd -> Set())
+ case Some(body) => {
+ val mutableParams = fd.params.filter(vd => vd.getType match {
+ case ArrayType(_) => true
+ case _ => false
+ })
+ val mutatedParams = mutableParams.filter(vd => exists {
+ case ArrayUpdate(Variable(a), _, _) => a == vd.id
+ case _ => false
+ }(body))
+ val mutatedParamsIndices = fd.params.zipWithIndex.flatMap{
+ case (vd, i) if mutatedParams.contains(vd) => Some(i)
+ case _ => None
+ }.toSet
+ effects = effects + (fd -> mutatedParamsIndices)
+
+ val missingCalls: Set[FunctionInvocation] = functionCallsOf(body).filterNot(fi => fi.tfd.fd == fd)
+ if(missingCalls.nonEmpty)
+ missingEffects += (fd -> missingCalls)
+ }
+ }
+ }
+
+ def rec(): Unit = {
+ val previousMissingEffects = missingEffects
+
+ for{ (fd, calls) <- missingEffects } {
+ var newMissingCalls: Set[FunctionInvocation] = calls
+ for(fi <- calls) {
+ val mutatedArgs = invocEffects(fi)
+ val mutatedFunParams: Set[Int] = fd.params.zipWithIndex.flatMap{
+ case (vd, i) if mutatedArgs.contains(vd.id) => Some(i)
+ case _ => None
+ }.toSet
+ effects += (fd -> (effects(fd) ++ mutatedFunParams))
+
+ if(effectsFullyComputed(fi.tfd.fd)) {
+ newMissingCalls -= fi
+ }
+ }
+ if(newMissingCalls.isEmpty)
+ missingEffects = missingEffects - fd
+ else
+ missingEffects += (fd -> newMissingCalls)
+ }
+
+ if(missingEffects != previousMissingEffects) {
+ rec()
+ }
+ }
+
+ def invocEffects(fi: FunctionInvocation): Set[Identifier] = {
+ //TODO: the require should be fine once we consider nested functions as well
+ //require(effects.isDefinedAt(fi.tfd.fd)
+ val mutatedParams: Set[Int] = effects.get(fi.tfd.fd).getOrElse(Set())
+ fi.args.zipWithIndex.flatMap{
+ case (Variable(id), i) if mutatedParams.contains(i) => Some(id)
+ case _ => None
+ }.toSet
+ }
+
+ rec()
+ effects
+ }
+
+
+ def checkAliasing(fd: FunDef)(ctx: LeonContext): Unit = {
+ def checkReturnValue(body: Expr, bindings: Set[Identifier]): Unit = {
+ getReturnedExpr(body).foreach{
+ case IsTyped(v@Variable(id), ArrayType(_)) if bindings.contains(id) =>
+ ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object: " + v)
+ case _ => ()
+ }
+ }
+
+ fd.body.foreach(bd => {
+ val params = fd.params.map(_.id).toSet
+ checkReturnValue(bd, params)
+ preMapWithContext[Set[Identifier]]((expr, bindings) => expr match {
+ case l@Let(id, IsTyped(v, ArrayType(_)), b) => {
+ v match {
+ case FiniteArray(_, _, _) => ()
+ case FunctionInvocation(_, _) => ()
+ case ArrayUpdated(_, _, _) => ()
+ case _ => ctx.reporter.fatalError(l.getPos, "Cannot alias array: " + l)
+ }
+ (None, bindings + id)
+ }
+ case l@LetVar(id, IsTyped(v, ArrayType(_)), b) => {
+ v match {
+ case FiniteArray(_, _, _) => ()
+ case FunctionInvocation(_, _) => ()
+ case ArrayUpdated(_, _, _) => ()
+ case _ => ctx.reporter.fatalError(l.getPos, "Cannot alias array: " + l)
+ }
+ (None, bindings + id)
+ }
+ case l@LetDef(fds, body) => {
+ fds.foreach(fd => fd.body.foreach(bd => checkReturnValue(bd, bindings)))
+ (None, bindings)
+ }
+
+ case _ => (None, bindings)
+ })(bd, params)
+ })
+ }
+
+ /*
+ * A bit hacky, but not sure of the best way to do something like that
+ * currently.
+ */
+ private def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
+ case Let(_, _, rest) => getReturnedExpr(rest)
+ case LetVar(_, _, rest) => getReturnedExpr(rest)
+ case Block(_, rest) => getReturnedExpr(rest)
+ case IfExpr(_, thenn, elze) => getReturnedExpr(thenn) ++ getReturnedExpr(elze)
+ case MatchExpr(_, cses) => cses.flatMap{ cse => getReturnedExpr(cse.rhs) }
+ case e => Seq(expr)
+ }
+
+
+ /*
+ * returns all fun def in the program, including local definitions inside
+ * other functions (LetDef).
+ */
+ private def allFunDefs(pgm: Program): Seq[FunDef] =
+ pgm.definedFunctions.flatMap(fd =>
+ fd.body.toSet.flatMap((bd: Expr) =>
+ nestedFunDefsOf(bd)) + fd)
+}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 20048c0ba60b0d968877c713c1ddfe9f9d25f98d..a298e90b16f405a19856c1a38a276a04153fd500 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -67,7 +67,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val (tRes, tScope, tFun) = toFunction(tExpr)
val (eRes, eScope, eFun) = toFunction(eExpr)
- val iteRType = leastUpperBound(tRes.getType, eRes.getType).get
+ val iteRType = leastUpperBound(tRes.getType, eRes.getType).getOrElse(Untyped)
val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varsInScope).toSeq
val resId = FreshIdentifier("res", iteRType)
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index 3a7f8be381cfa5fdb87dc6870cf35141f8d8cf33..59dd3217714f964be5f9ff6a1428617c6e54e17a 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -12,7 +12,8 @@ object XLangDesugaringPhase extends LeonPhase[Program, Program] {
override def run(ctx: LeonContext, pgm: Program): (LeonContext, Program) = {
val phases =
- ArrayTransformation andThen
+ //ArrayTransformation andThen
+ AntiAliasingPhase andThen
EpsilonElimination andThen
ImperativeCodeElimination
diff --git a/src/test/resources/regression/frontends/error/xlang/Array2.scala b/src/test/resources/regression/frontends/error/xlang/Array2.scala
deleted file mode 100644
index b1b370395d7e0b648e0b88875b3678eaf4668eb5..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array2.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-object Array2 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- val b = a
- b(3)
- }
-
-}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array3.scala b/src/test/resources/regression/frontends/error/xlang/Array3.scala
deleted file mode 100644
index 14a8512015102bd235a9efe41782ba7d5a46fd44..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array3.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-object Array3 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- if(a.length > 2)
- a(1) = 2
- else
- 0
- 0
- }
-
-}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array4.scala b/src/test/resources/regression/frontends/error/xlang/Array4.scala
deleted file mode 100644
index e41535d6d267986ba7764a6f457970c6ab33b733..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array4.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-object Array4 {
-
- def foo(a: Array[Int]): Int = {
- val b = a
- b(3)
- }
-
-}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array5.scala b/src/test/resources/regression/frontends/error/xlang/Array5.scala
deleted file mode 100644
index 8b7254e9482ddc7df1196c03b1a191c54e86ea0f..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array5.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-object Array5 {
-
- def foo(a: Array[Int]): Int = {
- a(2) = 4
- a(2)
- }
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/frontends/error/xlang/Array6.scala b/src/test/resources/regression/frontends/error/xlang/Array6.scala
deleted file mode 100644
index c4d0c09541d3c7fe4ea4be1527cd704e96d54bb1..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array6.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-
-object Array6 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- var b = a
- b(0)
- }
-
-}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array7.scala b/src/test/resources/regression/frontends/error/xlang/Array7.scala
deleted file mode 100644
index ab6f4c20da5a84adfd8509a60174d78c0c423654..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/frontends/error/xlang/Array7.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-object Array7 {
-
- def foo(): Int = {
- val a = Array.fill(5)(5)
- var b = a
- b(0)
- }
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f0e622c66c31e4fe01ff8be5c1b08e17d4d330eb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation1 {
+
+ def update(a: Array[BigInt]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ def f(): BigInt = {
+ val a = Array.fill(10)(BigInt(0))
+ update(a)
+ a(0)
+ } ensuring(res => res == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..801b35e0cc545f160fc8061e34fd0ee06b7c3f73
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation2 {
+
+ def rec(a: Array[BigInt]): BigInt = {
+ require(a.length > 1 && a(0) >= 0)
+ if(a(0) == 0)
+ a(1)
+ else {
+ a(0) = a(0) - 1
+ a(1) = a(1) + a(0)
+ rec(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f575167444f839c0ee900a35de5e4e822624dc21
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation3 {
+
+ def odd(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) false
+ else {
+ a(0) = a(0) - 1
+ even(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+ def even(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) true
+ else {
+ a(0) = a(0) - 1
+ odd(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31af4cd5885ea66a2d11e9387ba7e306423ec4d7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation4 {
+
+ def multipleArgs(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ if(a1(0) == 10)
+ a2(0) = 13
+ else
+ a2(0) = a1(0) + 1
+ }
+
+ def transitiveEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleArgs(a1, a2)
+ } ensuring(_ => a2(0) >= a1(0))
+
+ def transitiveReverseEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleArgs(a2, a1)
+ } ensuring(_ => a1(0) >= a2(0))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..249a79d1f3b7d8df8c941ab3121c4eafed149e03
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
@@ -0,0 +1,21 @@
+
+import leon.lang._
+
+object ArrayParamMutation5 {
+
+ def mutuallyRec1(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a1(0) > 0 && a2.length > 0)
+ if(a1(0) == 10) {
+ ()
+ } else {
+ mutuallyRec2(a1, a2)
+ }
+ } ensuring(res => a1(0) == 10)
+
+ def mutuallyRec2(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0 && a1(0) > 0)
+ a1(0) = 10
+ mutuallyRec1(a1, a2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..29ded427fa6546a103d8da6f98cefc1415f389a6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation6 {
+
+ def multipleEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ a1(0) = 11
+ a2(0) = 12
+ } ensuring(_ => a1(0) != a2(0))
+
+ def f(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleEffects(a1, a2)
+ } ensuring(_ => a1(0) == 11 && a2(0) == 12)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..53d67729fd57723d1693c564e99cd3d66ee095ef
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+
+object ArrayParamMutation7 {
+
+ def f(i: BigInt)(implicit world: Array[BigInt]): BigInt = {
+ require(world.length == 3)
+
+ world(1) += 1 //global counter of f
+
+ val res = i*i
+ world(0) = res
+ res
+ }
+
+ def mainProgram(): Unit = {
+
+ implicit val world: Array[BigInt] = Array(0,0,0)
+
+ f(1)
+ assert(world(0) == 1)
+ f(2)
+ assert(world(0) == 4)
+ f(4)
+ assert(world(0) == 16)
+
+ assert(world(1) == 3)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..68aa737eb42e6e51073dac27b799e06bde928400
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object ArrayParamMutation8 {
+
+ def odd(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) false
+ else {
+ a(0) = a(0) - 1
+ even(a)
+ }
+ } ensuring(res => if(old(a)(0) % 2 == 1) res else !res)
+
+ def even(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) true
+ else {
+ a(0) = a(0) - 1
+ odd(a)
+ }
+ } ensuring(res => if(old(a)(0) % 2 == 0) res else !res)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f5046b6cf3b40382ccc5d989d81d73bc577da9f7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+
+object ArrayParamMutation9 {
+ def abs(a: Array[Int]) {
+ require(a.length > 0)
+ var i = 0;
+ (while (i < a.length) {
+ a(i) = if (a(i) < 0) -a(i) else a(i) // <-- this makes Leon crash
+ i = i + 1
+ }) invariant(i >= 0)
+ }
+
+
+ def main = {
+ val a = Array(0, -1, 2, -3)
+
+ abs(a)
+
+ a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7250a7bcfd572c49584110d213f9e9991a10c9f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object NestedFunParamsMutation1 {
+
+ def f(): Int = {
+ def g(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ val a = Array(1,2,3,4)
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..799a87c6e9e70bf6ef89bfc1fb7a6e116adb7feb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+
+object NestedFunParamsMutation2 {
+
+ def f(): Int = {
+ def g(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ def h(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ g(a)
+ }
+
+ val a = Array(1,2,3,4)
+ h(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array1.scala b/src/test/resources/regression/xlang/error/Array1.scala
similarity index 100%
rename from src/test/resources/regression/frontends/error/xlang/Array1.scala
rename to src/test/resources/regression/xlang/error/Array1.scala
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing1.scala b/src/test/resources/regression/xlang/error/ArrayAliasing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..30b1652dac16f1f8a9c7b36d83d9a0a52811e3c6
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing1.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object ArrayAliasing1 {
+
+ def f1(): BigInt = {
+ val a = Array.fill(10)(BigInt(0))
+ val b = a
+ b(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
+
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing10.scala b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05737b03d9816be72cf52f4913f57a482abf76dd
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object ArrayAliasing10 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+
+ def rec(): Array[Int] = {
+
+ def nestedRec(): Array[Int] = {
+ a
+ }
+ nestedRec()
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing2.scala b/src/test/resources/regression/xlang/error/ArrayAliasing2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4e906865a8848aaa00150c67de16f6b32136c64a
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing2.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing2 {
+
+ def f1(a: Array[BigInt]): BigInt = {
+ val b = a
+ b(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing3.scala b/src/test/resources/regression/xlang/error/ArrayAliasing3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0398fc37b9dc2028e1535878ec377bef1620dd88
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing3.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing3 {
+
+ def f1(a: Array[BigInt], b: Boolean): BigInt = {
+ val c = if(b) a else Array[BigInt](1,2,3,4,5)
+ c(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing4.scala b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2632782c39e853744744b66309ef10342bee386b
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing4 {
+
+ def f1(a: Array[BigInt]): Array[BigInt] = {
+ require(a.length > 0)
+ a(0) = 10
+ a
+ } ensuring(res => res(0) == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing5.scala b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b9363d1ab5a627df29e6a0f0018c73850dcbb529
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ArrayAliasing5 {
+
+
+ def f1(a: Array[BigInt], b: Array[BigInt]): Unit = {
+ require(a.length > 0 && b.length > 0)
+ a(0) = 10
+ b(0) = 20
+ } ensuring(_ => a(0) == 10 && b(0) == 20)
+
+
+ def callWithAliases(): Unit = {
+ val a = Array[BigInt](0,0,0,0)
+ f1(a, a)
+ }
+
+}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array8.scala b/src/test/resources/regression/xlang/error/ArrayAliasing6.scala
similarity index 80%
rename from src/test/resources/regression/frontends/error/xlang/Array8.scala
rename to src/test/resources/regression/xlang/error/ArrayAliasing6.scala
index bbe5bd5fd92b0f4f9662379693d06924bdaf5461..963a134bf71da7a625252411854d73272f56d574 100644
--- a/src/test/resources/regression/frontends/error/xlang/Array8.scala
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing6.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-object Array8 {
+object ArrayAliasing6 {
def foo(a: Array[Int]): Array[Int] = {
a
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing7.scala b/src/test/resources/regression/xlang/error/ArrayAliasing7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..21bc94502327b334f2e4e5887d4a7286731c78b7
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing7.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object ArrayAliasing7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ val b = a
+ b
+ }
+
+}
diff --git a/src/test/resources/regression/frontends/error/xlang/Array9.scala b/src/test/resources/regression/xlang/error/ArrayAliasing8.scala
similarity index 86%
rename from src/test/resources/regression/frontends/error/xlang/Array9.scala
rename to src/test/resources/regression/xlang/error/ArrayAliasing8.scala
index fbc7dd7376e0966df5ed6eb93bafa7427aeab9e8..e7c27cc9cebf657033da4c07936ce16a510075a0 100644
--- a/src/test/resources/regression/frontends/error/xlang/Array9.scala
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing8.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-object Array9 {
+object ArrayAliasing8 {
def foo(a: Array[Int]): Int = {
def rec(): Array[Int] = {
diff --git a/src/test/resources/regression/frontends/error/xlang/Array10.scala b/src/test/resources/regression/xlang/error/ArrayAliasing9.scala
similarity index 87%
rename from src/test/resources/regression/frontends/error/xlang/Array10.scala
rename to src/test/resources/regression/xlang/error/ArrayAliasing9.scala
index 563cdacdf7e0e66ff56eec571fae4d3e3bbe10be..c84d29c3fbb4866100173b7ac0e7b4d0da9a1e57 100644
--- a/src/test/resources/regression/frontends/error/xlang/Array10.scala
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing9.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-object Array10 {
+object ArrayAliasing9 {
def foo(): Int = {
val a = Array.fill(5)(0)
diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12feace5413c23e688ac194192482120793b4e24
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+ def f(): Int = {
+ val a = Array(1,2,3,4)
+
+ def g(b: Array[Int]): Unit = {
+ require(b.length > 0 && a.length > 0)
+ b(0) = 10
+ a(0) = 17
+ } ensuring(_ => b(0) == 10)
+
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+}
diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81a9b82b39fb47af105ef2e3122fe86a8b10dbb6
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+ def f(a: Array(1,2,3,4)): Int = {
+
+ def g(b: Array[Int]): Unit = {
+ require(b.length > 0 && a.length > 0)
+ b(0) = 10
+ a(0) = 17
+ } ensuring(_ => b(0) == 10)
+
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala b/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
index b9bfccd36bc2abcc3479c9d3a703df0cdfe16ab7..a0e52aa0b083c04a5a3e1141d2f3287a1995611e 100644
--- a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
+++ b/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
@@ -36,7 +36,6 @@ class FrontEndsSuite extends LeonRegressionSuite {
}
val pipeNormal = xlang.NoXLangFeaturesChecking andThen NoopPhase() // redundant NoopPhase to trigger throwing error between phases
- val pipeX = NoopPhase[Program]()
val baseDir = "regression/frontends/"
forEachFileIn(baseDir+"passing/") { f =>
@@ -45,8 +44,5 @@ class FrontEndsSuite extends LeonRegressionSuite {
forEachFileIn(baseDir+"error/simple/") { f =>
testFrontend(f, pipeNormal, true)
}
- forEachFileIn(baseDir+"error/xlang/") { f =>
- testFrontend(f, pipeX, true)
- }
}
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index f2ae97880694baac498b94570f81beb1c21c422f..446d06675cdb9b3eb1c7095137ab95e8a928c399 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -41,7 +41,7 @@ trait VerificationSuite extends LeonRegressionSuite {
VerificationPhase andThen
(if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
- val ctx = createLeonContext(files:_*)
+ val ctx = createLeonContext(files:_*).copy(reporter = new TestErrorReporter)
try {
val (_, ast) = extraction.run(ctx, files)
diff --git a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41260ec2df6f9d9f32827c39e7f700da15ccca9e
--- /dev/null
+++ b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
@@ -0,0 +1,46 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.regression.xlang
+
+import leon._
+import leon.test._
+import purescala.Definitions.Program
+import java.io.File
+
+class XLangDesugaringSuite extends LeonRegressionSuite {
+ // Hard-code output directory, for Eclipse purposes
+
+ val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase(true)
+
+ def testFrontend(f: File, forError: Boolean) = {
+ test ("Testing " + f.getName) {
+ val ctx = createLeonContext()
+ if (forError) {
+ intercept[LeonFatalError]{
+ pipeline.run(ctx, List(f.getAbsolutePath))
+ }
+ } else {
+ pipeline.run(ctx, List(f.getAbsolutePath))
+ }
+ }
+
+ }
+
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"))
+
+ for(f <- fs) {
+ block(f)
+ }
+ }
+
+ val baseDir = "regression/xlang/"
+
+ forEachFileIn(baseDir+"passing/") { f =>
+ testFrontend(f, false)
+ }
+ forEachFileIn(baseDir+"error/") { f =>
+ testFrontend(f, true)
+ }
+
+}
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
index 2cf9ea4f7f6c78d4f07002a01f434a150e0d9034..2a8761584222f02c1e4bf85b6fd031c603771079 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/src/test/scala/leon/test/TestSilentReporter.scala
@@ -13,3 +13,10 @@ class TestSilentReporter extends DefaultReporter(Set()) {
case _ =>
}
}
+
+class TestErrorReporter extends DefaultReporter(Set()) {
+ override def emit(msg: Message): Unit = msg match {
+ case Message(this.ERROR | this.FATAL, _, _) => super.emit(msg)
+ case _ =>
+ }
+}
diff --git a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
index b448953acf1856cf1df12289880000226f78f8bf..827596fc6cd116aefc752a37aeb30647e3ebdf99 100644
--- a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
@@ -279,4 +279,44 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
}
+
+ test("preMapWithContext") { ctx =>
+ val expr = Plus(bi(1), Minus(bi(2), bi(3)))
+ def op(e : Expr, set: Set[Int]): (Option[Expr], Set[Int]) = e match {
+ case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => (Some(bi(2)), set)
+ case InfiniteIntegerLiteral(one) if one == BigInt(1) => (Some(bi(2)), set)
+ case InfiniteIntegerLiteral(two) if two == BigInt(2) => (Some(bi(42)), set)
+ case _ => (None, set)
+ }
+
+ assert(preMapWithContext(op, false)(expr, Set()) === Plus(bi(2), bi(2)))
+ assert(preMapWithContext(op, true)(expr, Set()) === Plus(bi(42), bi(42)))
+
+ val expr2 = Let(x.id, bi(1), Let(y.id, bi(2), Plus(x, y)))
+ def op2(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (None, bindings + (id -> v))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+
+ assert(preMapWithContext(op2, false)(expr2, Map()) === Let(x.id, bi(1), Let(y.id, bi(2), Plus(bi(1), bi(2)))))
+
+ def op3(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), bindings + (id -> v))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+ assert(preMapWithContext(op3, true)(expr2, Map()) === Plus(bi(1), bi(2)))
+
+
+ val expr4 = Plus(Let(y.id, bi(2), y),
+ Let(y.id, bi(4), y))
+ def op4(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), if(bindings.contains(id)) bindings else (bindings + (id -> v)))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+ assert(preMapWithContext(op4, true)(expr4, Map()) === Plus(bi(2), bi(4)))
+ }
+
}
diff --git a/testcases/verification/xlang/AbsFun.scala b/testcases/verification/xlang/AbsFun.scala
index fe37632df68bc4ae1c164bb034902e45b18365c4..a6ff9679e27fc32ff4dd8b62a1cf2170386083d8 100644
--- a/testcases/verification/xlang/AbsFun.scala
+++ b/testcases/verification/xlang/AbsFun.scala
@@ -35,11 +35,7 @@ object AbsFun {
isPositive(t, k))
if(k < tab.length) {
- val nt = if(tab(k) < 0) {
- t.updated(k, -tab(k))
- } else {
- t.updated(k, tab(k))
- }
+ val nt = t.updated(k, if(tab(k) < 0) -tab(k) else tab(k))
while0(nt, k+1, tab)
} else {
(t, k)
@@ -54,11 +50,7 @@ object AbsFun {
def property(t: Array[Int], k: Int): Boolean = {
require(isPositive(t, k) && t.length >= 0 && k >= 0)
if(k < t.length) {
- val nt = if(t(k) < 0) {
- t.updated(k, -t(k))
- } else {
- t.updated(k, t(k))
- }
+ val nt = t.updated(k, if(t(k) < 0) -t(k) else t(k))
isPositive(nt, k+1)
} else true
} holds