diff --git a/library/lang/package.scala b/library/lang/package.scala
index 44351d02ca9328bbbf86063745d233f2db17cd7c..bb7ec69122f4814bd61b1ce79f94c2eab9054c74 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -47,6 +47,9 @@ package object lang {
@ignore
def error[T](reason: java.lang.String): T = sys.error(reason)
+ @ignore
+ def old[T](value: T): T = value
+
@ignore
implicit class Passes[A,B](io : (A,B)) {
val (in, out) = io
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index db477ec494742b0dc2b0e42e098676c4ab55282d..fb64b3311dfdd2af5b06df85ab2cb26088d3233e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -574,6 +574,15 @@ trait ASTExtractors {
}
}
+ object ExOldExpression {
+ def unapply(tree: Apply) : Option[Symbol] = tree match {
+ case a @ Apply(TypeApply(ExSymbol("leon", "lang", "old"), List(tpe)), List(arg)) =>
+ Some(arg.symbol)
+ case _ =>
+ None
+ }
+ }
+
object ExHoleExpression {
def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 24ecca501029604f25dc9c285e797be4562c5a01..4bca0e76794e64a40f32b56679d4a502d0b1590c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1054,6 +1054,15 @@ trait CodeExtraction extends ASTExtractors {
val tupleExprs = exprs.map(e => extractTree(e))
Tuple(tupleExprs)
+ case ex@ExOldExpression(sym) if dctx.isVariable(sym) =>
+ dctx.vars.get(sym).orElse(dctx.mutableVars.get(sym)) match {
+ case Some(builder) =>
+ val Variable(id) = builder()
+ Old(id).setPos(ex.pos)
+ case None =>
+ outOfSubsetError(current, "old can only be used with variables")
+ }
+
case ExErrorExpression(str, tpt) =>
Error(extractType(tpt), str)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c106d1393bcf793a7fe5d6944ecd533d84a42e36..c80d777480f66d795f2bc15eef0a3010452394fb 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -345,6 +345,7 @@ object ExprOps {
val subvs = subs.flatten.toSet
e match {
case Variable(i) => subvs + i
+ case Old(i) => subvs + i
case LetDef(fd, _) => subvs -- fd.params.map(_.id)
case Let(i, _, _) => subvs - i
case LetVar(i, _, _) => subvs - i
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 6e9adae5f6ee3548b1fa70af41b127e6a46a76b4..1569ebfb8ab3d8c0ab7f0e09bbb31f82870fc8f9 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -76,6 +76,10 @@ object Expressions {
val getType = tpe
}
+ case class Old(id: Identifier) extends Expr with Terminal {
+ val getType = id.getType
+ }
+
/** Precondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *require*
*
* @param pred The precondition formula inside ``require(...)``
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6b22810e542bdb9af65251da1c9a4d4ab1ab7142..3b96fff138dd7bc6a91c66acf3e3928fac0e44d0 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -77,6 +77,9 @@ class PrettyPrinter(opts: PrinterOptions,
}
p"$name"
+ case Old(id) =>
+ p"old($id)"
+
case Variable(id) =>
p"$id"
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7ab5925cebf63dd462db2627a45299e46e05978a..e9802d500208b96b5af448391d69c6660a05f843 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -129,6 +129,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
case wh@While(cond, body) =>
+ //TODO: rewrite by re-using the nested function transformation code
val (condRes, condScope, condFun) = toFunction(cond)
val (_, bodyScope, bodyFun) = toFunction(body)
val condBodyFun = condFun ++ bodyFun
@@ -323,7 +324,9 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val newBody =
replace(
modifiedVars.zipWithIndex.map{ case (v, i) =>
- (v.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap +
+ (v.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap ++
+ modifiedVars.zip(freshNames).map{ case (ov, nv) =>
+ (Old(ov), nv.toVariable)}.toMap +
(res.toVariable -> TupleSelect(newRes.toVariable, 1)),
postBody)
Lambda(Seq(newRes), newBody).setPos(post)
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
index fb1a778b8922be1ad8bd5836c5a56740af930374..a8935ab8c1d4eec6980b85f171e695071f2a9442 100644
--- a/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
@@ -4,7 +4,7 @@ object ArrayNested2 {
def test(): Int = {
- var a = Array(1, 2, 0)
+ val a = Array(1, 2, 0)
def nested(): Unit = {
require(a.length == 3)
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala b/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..903dfd63aca5105c9366c459552865646139033e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object NestedOld1 {
+
+ def test(): Int = {
+ var counter = 0
+
+ def inc(): Unit = {
+ counter += 1
+ } ensuring(_ => counter == old(counter) + 1)
+
+ inc()
+ counter
+ } ensuring(_ == 1)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala b/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe6143ecf623c295251ca2b9d75d6474d422fd4f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala
@@ -0,0 +1,24 @@
+import leon.lang._
+
+object NestedOld2 {
+
+ def test(): Int = {
+ var counterPrev = 0
+ var counterNext = 1
+
+ def step(): Unit = {
+ require(counterNext == counterPrev + 1)
+ counterPrev = counterNext
+ counterNext = counterNext+1
+ } ensuring(_ => {
+ counterPrev == old(counterNext) &&
+ counterNext == old(counterNext) + 1 &&
+ counterPrev == old(counterPrev) + 1
+ })
+
+ step()
+ step()
+ counterNext
+ } ensuring(_ == 3)
+
+}