Introduce array access VC in DefaultTactic

Previously, array access were generated via a code transformation in
ArrayTransformation in xlang, where Array Select and Update were
wrapped in if-then-else with an Error in the else branch. They are
now natively supported in VC generation.  Some testcases --- that would
trigger bugs when --xlang is not used with functional array ---- are
included in this commit

The commit introduces a new abstraction to traverse Leon trees and collect
path conditions. This traverser is used for the implementation of the
VC generation for arrays.

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

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
+    //}
 }

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)

src/test/resources/regression/verification/purescala/invalid/Array1.scala

+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+  def foo(a: Array[Int]): Int = {
+    a(2)
+  }
+
+}

src/test/resources/regression/verification/purescala/invalid/Array2.scala

+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+  def foo(a: Array[Int]): Int = {
+    require(a.length > 2)
+    a(2)
+  } ensuring(_ == 0)
+
+}

src/test/resources/regression/verification/purescala/invalid/Array3.scala

+import leon.Utils._
+
+object Test {
+
+  def find(c: Array[Int], i: Int): Int = {
+    if(c(i) == i)
+      42
+    else
+      12
+  } ensuring(_ > 0)
+
+}

src/test/resources/regression/verification/purescala/invalid/Array4.scala

+/* Copyright 2009-2013 EPFL, Lausanne */
+
+import leon.Utils._
+
+object Array4 {
+
+  def foo(a: Array[Int]): Int = {
+    val tmp = a.updated(0, 0)
+    42
+  }
+
+}

src/test/resources/regression/verification/xlang/invalid/Array6.scala

+/* 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)
+  }
+
+}