diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index c3803718ed934dbf75abdc2189cc4d6af69de93f..a653b86105f256716a79691078d30e8bb9c49b34 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1086,6 +1086,27 @@ object TreeOps {
def traverse(e: Expr): T
}
+ class CollectorWithPaths[T](matcher: PartialFunction[Expr, T]) extends TransformerWithPC {
+ type C = Seq[Expr]
+ val initC = Nil
+ def register(e: Expr, path: C) = path :+ e
+
+ var results: Seq[(T, Expr)] = Nil
+
+ override def rec(e: Expr, path: C) = {
+ if(matcher.isDefinedAt(e)) {
+ val res = matcher(e)
+ results = results :+ (res, And(path))
+ e
+ } else super.rec(e, path)
+ }
+
+ def traverse(e: Expr) = {
+ results = Nil
+ rec(e, initC)
+ results
+ }
+ }
class ChooseCollectorWithPaths extends TransformerWithPC with Traverser[Seq[(Choose, Expr)]] {
type C = Seq[Expr]
val initC = Nil
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 0e258e9aa4d46c852826d6b838c2b524d23bbe6d..f2ec7534ac4f08607c7324f91598d299320c6f16 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -165,18 +165,28 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
val toRet = if (function.hasBody) {
val cleanBody = matchToIfThenElse(function.body.get)
- val allPathConds = collectWithPathCondition((t => t match {
- case Error("Index out of bound") => true
- case _ => false
- }), cleanBody)
+ val allPathConds = new CollectorWithPaths({
+ case expr@ArraySelect(a, i) => (expr, a, i)
+ case expr@ArrayUpdated(a, i, _) => (expr, a, i)
+ }).traverse(cleanBody)
+
+ val arrayAccessConditions = allPathConds.map{
+ case ((expr, array, index), pathCond) => {
+ val length = ArrayLength(array)
+ val negative = LessThan(index, IntLiteral(0))
+ val tooBig = GreaterEquals(index, length)
+ (And(pathCond, Or(negative, tooBig)), expr)
+ }
+ }
- def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
- Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds)))
+ def withPrecIfDefined(conds: Expr) : Expr = if (function.hasPrecondition) {
+ Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), conds))
} else {
- Not(And(conds))
+ Not(conds)
}
- allPathConds.map(pc =>
+
+ arrayAccessConditions.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
function, //if(function.fromLoop) function.parent.get else function,
@@ -194,34 +204,42 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
generateMapAccessChecks(function)
}
- // prec: there should be no lets and no pattern-matching in this expression
def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
- var collected : Set[(Seq[Expr],Expr)] = Set.empty
-
- def rec(expr: Expr, path: List[Expr]) : Unit = {
- if(matcher(expr)) {
- collected = collected + ((path.reverse, expr))
- }
-
- expr match {
- case Let(i,e,b) => {
- rec(e, path)
- rec(b, Equals(Variable(i), e) :: path)
- }
- case IfExpr(cond, thenn, elze) => {
- rec(cond, path)
- rec(thenn, cond :: path)
- rec(elze, Not(cond) :: path)
- }
- case NAryOperator(args, _) => args.foreach(rec(_, path))
- case BinaryOperator(t1, t2, _) => rec(t1, path); rec(t2, path)
- case UnaryOperator(t, _) => rec(t, path)
- case t : Terminal => ;
- case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
- }
- }
-
- rec(expression, Nil)
- collected
+ new CollectorWithPaths({
+ case e if matcher(e) => e
+ }).traverse(expression).map{
+ case (e, And(es)) => (es, e)
+ case (e1, e2) => (Seq(e2), e1)
+ }.toSet
}
+ // prec: there should be no lets and no pattern-matching in this expression
+ //def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
+ // var collected : Set[(Seq[Expr],Expr)] = Set.empty
+
+ // def rec(expr: Expr, path: List[Expr]) : Unit = {
+ // if(matcher(expr)) {
+ // collected = collected + ((path.reverse, expr))
+ // }
+
+ // expr match {
+ // case Let(i,e,b) => {
+ // rec(e, path)
+ // rec(b, Equals(Variable(i), e) :: path)
+ // }
+ // case IfExpr(cond, thenn, elze) => {
+ // rec(cond, path)
+ // rec(thenn, cond :: path)
+ // rec(elze, Not(cond) :: path)
+ // }
+ // case NAryOperator(args, _) => args.foreach(rec(_, path))
+ // case BinaryOperator(t1, t2, _) => rec(t1, path); rec(t2, path)
+ // case UnaryOperator(t, _) => rec(t, path)
+ // case t : Terminal => ;
+ // case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
+ // }
+ // }
+
+ // rec(expression, Nil)
+ // collected
+ //}
}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 4d6ad43251a5d139a27caaf235e091f0eb054096..ac9e655a2c2e25a7072fadd3139740cb3fabcf41 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -33,41 +33,12 @@ object ArrayTransformation extends TransformationPhase {
def transform(expr: Expr): Expr = (expr match {
- case sel@ArraySelect(a, i) => {
- val ra = transform(a)
- val ri = transform(i)
- val length = ArrayLength(ra)
- val res = IfExpr(
- And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- ArraySelect(ra, ri).setType(sel.getType).setPos(sel),
- Error("Index out of bound").setType(sel.getType).setPos(sel)
- ).setType(sel.getType)
- res
- }
case up@ArrayUpdate(a, i, v) => {
val ra = transform(a)
val ri = transform(i)
val rv = transform(v)
val Variable(id) = ra
- val length = ArrayLength(ra)
- val res = IfExpr(
- And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPos(up)),
- Error("Index out of bound").setType(UnitType).setPos(up)
- ).setType(UnitType)
- res
- }
- case up@ArrayUpdated(a, i, v) => {
- val ra = transform(a)
- val ri = transform(i)
- val rv = transform(v)
- val length = ArrayLength(ra)
- val res = IfExpr(
- And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- ArrayUpdated(ra, ri, rv).setType(ra.getType).setPos(up),
- Error("Index out of bound").setType(ra.getType).setPos(up)
- ).setType(ra.getType)
- res
+ Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPos(up))
}
case ArrayClone(a) => {
val ra = transform(a)
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array1.scala b/src/test/resources/regression/verification/purescala/invalid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..740f38a96314fb9babbff944fe7a35f0210b50ea
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Array1.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array2.scala b/src/test/resources/regression/verification/purescala/invalid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4cc49498f6b6510edc7ce23b8511eabad243774d
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Array2.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array3.scala b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d744e8078156510486cf12486557cfea6b23d27
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
@@ -0,0 +1,12 @@
+import leon.Utils._
+
+object Test {
+
+ def find(c: Array[Int], i: Int): Int = {
+ if(c(i) == i)
+ 42
+ else
+ 12
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array4.scala b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cb0c2409c26ca61e394bc1a0bf00a382097a013f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ val tmp = a.updated(0, 0)
+ 42
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array6.scala b/src/test/resources/regression/verification/xlang/invalid/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41b35fd03318f89cd7419f08a101ed74ef7f0922
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array6.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val a2 = a.updated(1, 2)
+ a2(0)
+ }
+
+}