From a46ea1f7fb4448df4bc762ff21c062d1936e0cb0 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 Jan 2016 16:00:08 +0100
Subject: [PATCH] fix some issues with asserts and xlang
---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 6 ++++--
.../xlang/ImperativeCodeElimination.scala | 21 +++++++++++++------
.../verification/xlang/valid/Assert3.scala | 2 +-
3 files changed, 20 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 820d74662..b97297fb0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -837,11 +837,13 @@ trait SMTLIBTarget extends Interruptible {
val rargs = args.zip(tt.bases).map(fromSMT)
tupleWrap(rargs)
- case ArrayType(baseType) =>
+ case at@ArrayType(baseType) =>
val IntLiteral(size) = fromSMT(args(0), Int32Type)
val RawArrayValue(_, elems, default) = fromSMT(args(1), RawArrayType(Int32Type, baseType))
- if (size > 10) {
+ if (size < 0) {
+ unsupported(at, "Cannot build an array of negative length: " + size)
+ } else if (size > 10) {
val definedElements = elems.collect {
case (IntLiteral(i), value) => (i, value)
}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 01472565e..ac9535783 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -152,14 +152,13 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
case Block(exprs, expr) =>
val (scope, fun) = exprs.foldRight((body: Expr) => body, Map[Identifier, Identifier]())((e, acc) => {
val (accScope, accFun) = acc
- val (_, rScope, rFun) = toFunction(e)
+ val (rVal, rScope, rFun) = toFunction(e)
val scope = (body: Expr) => {
- val withoutPrec = rScope(replaceNames(rFun, accScope(body)))
- e match {
+ rVal match {
case FunctionInvocation(tfd, args) if tfd.hasPrecondition =>
- Assert(tfd.withParamSubst(args, tfd.precondition.get), Some("Precondition failed"), withoutPrec)
+ rScope(replaceNames(rFun, Let(FreshIdentifier("tmp", tfd.returnType), rVal, accScope(body))))
case _ =>
- withoutPrec
+ rScope(replaceNames(rFun, accScope(body)))
}
}
@@ -211,7 +210,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
}
- case None =>
+ case None =>
(FunctionInvocation(tfd, recArgs).copiedFrom(fi), argScope, argFun)
}
@@ -315,6 +314,15 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val ifExpr = args.reduceRight((el, acc) => IfExpr(el, BooleanLiteral(true), acc))
toFunction(ifExpr)
+ //TODO: this should be handled properly by the Operator case, but there seems to be a subtle bug in the way Let's are lifted
+ // which leads to Assert refering to the wrong value of a var in some cases.
+ case a@Assert(cond, msg, body) =>
+ val (condVal, condScope, condFun) = toFunction(cond)
+ val (bodyRes, bodyScope, bodyFun) = toFunction(body)
+ val scope = (body: Expr) => condScope(Assert(condVal, msg, replaceNames(condFun, bodyScope(body))).copiedFrom(a))
+ (bodyRes, scope, condFun ++ bodyFun)
+
+
case n @ Operator(args, recons) =>
val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
val (accArgs, accScope, accFun) = acc
@@ -322,6 +330,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val newScope = (body: Expr) => argScope(replaceNames(argFun, accScope(body)))
(argVal +: accArgs, newScope, argFun ++ accFun)
})
+
(recons(recArgs).copiedFrom(n), scope, fun)
case _ =>
diff --git a/src/test/resources/regression/verification/xlang/valid/Assert3.scala b/src/test/resources/regression/verification/xlang/valid/Assert3.scala
index 58af2ef08..49e2f6c55 100644
--- a/src/test/resources/regression/verification/xlang/valid/Assert3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Assert3.scala
@@ -11,7 +11,7 @@ object Assert3 {
j += 1
assert(j == i + 1)
j += 2
- assert(j == i + 2)
+ assert(j == i + 3)
j
--
GitLab