Refactor/generalize collection of correctness cond.

src/main/scala/leon/purescala/ExprOps.scala

@@ -1270,6 +1270,10 @@ object ExprOps {
     }
   }
 
+  def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
+    CollectorWithPaths(f).traverse(expr)
+  }
+
   def patternSize(p: Pattern): Int = p match {
     case wp: WildcardPattern =>
       1
@@ -2047,4 +2051,46 @@ object ExprOps {
       None
   }
 
+
+  /** Collects correctness conditions from within an expression
+    * (taking into account the path condition).
+    *
+    * Collection of preconditions of function invocations
+    * can be disabled (mainly for [[leon.verification.Tactic]]).
+    *
+    * @param e The expression to traverse
+    * @param collectFIs Whether we also want to collect preconditions for function invocations
+    * @return A sequence of pairs (expression, condition)
+    */
+  def collectCorrectnessConditions(e: Expr, collectFIs: Boolean = true): Seq[(Expr, Expr)] = {
+    val conds = collectWithPC {
+
+      case m @ MatchExpr(scrut, cases) =>
+        (m, orJoin(cases map (matchCaseCondition(scrut, _))))
+
+      case e @ Error(_, _) =>
+        (e, BooleanLiteral(false))
+
+      case a @ Assert(cond, _, _) =>
+        (a, cond)
+
+      case e @ Ensuring(body, post) =>
+        (e, application(post, Seq(body)))
+
+      case r @ Require(pred, e) =>
+        (r, pred)
+
+      case fi @ FunctionInvocation(tfd, args) if tfd.hasPrecondition && collectFIs =>
+        (fi, tfd.withParamSubst(args, tfd.precondition.get))
+    }(e)
+
+    conds map {
+      case ((e, cond), path) =>
+        (e, implies(path, cond))
+    }
+  }
+
+
+
+
 }

src/main/scala/leon/purescala/TransformerWithPC.scala

@@ -16,11 +16,11 @@ abstract class TransformerWithPC extends Transformer {
   protected def register(cond: Expr, path: C): C
 
   protected def rec(e: Expr, path: C): Expr = e match {
-    case Let(i, e, b) =>
-      val se = rec(e, path)
+    case Let(i, v, b) =>
+      val se = rec(v, path)
       val sb = rec(b, register(Equals(Variable(i), se), path))
       Let(i, se, sb).copiedFrom(e)
-
+      
     case p:Passes =>
       applyAsMatches(p,rec(_,path))
 
@@ -71,8 +71,6 @@ abstract class TransformerWithPC extends Transformer {
     case o @ Operator(es, builder) =>
       builder(es.map(rec(_, path))).copiedFrom(o)
 
-    case t : Terminal => t
-
     case _ =>
       sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
   }

src/main/scala/leon/verification/DefaultTactic.scala

@@ -9,82 +9,76 @@ import purescala.Definitions._
 import purescala.Constructors._
 
 class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
-    val description = "Default verification condition generation approach"
+  val description = "Default verification condition generation approach"
 
-    def generatePostconditions(fd: FunDef): Seq[VC] = {
-      (fd.postcondition, fd.body) match {
-        case (Some(post), Some(body)) =>
-          val vc = implies(precOrTrue(fd), application(post, Seq(body)))
-
-          Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
-        case _ =>
-          Nil
-      }
+  def generatePostconditions(fd: FunDef): Seq[VC] = {
+    (fd.postcondition, fd.body) match {
+      case (Some(post), Some(body)) =>
+        val vc = implies(precOrTrue(fd), application(post, Seq(body)))
+        Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
+      case _ =>
+        Nil
     }
-  
-    def generatePreconditions(fd: FunDef): Seq[VC] = {
-      fd.body match {
-        case Some(body) =>
-          val calls = collectWithPC {
-            case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get)
-          }(body)
+  }
 
-          calls.map {
-            case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
-              val pre2 = tfd.withParamSubst(args, pre)
-              val vc = implies(and(precOrTrue(fd), path), pre2)
-              val fiS = sizeLimit(fi.asString, 40)
-              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
-          }
+  def generatePreconditions(fd: FunDef): Seq[VC] = {
+    fd.body match {
+      case Some(body) =>
+        val calls = collectWithPC {
+          case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get)
+        }(body)
 
-        case None =>
-          Nil
-      }
-    }
+        calls.map {
+          case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
+            val pre2 = tfd.withParamSubst(args, pre)
+            val vc = implies(and(precOrTrue(fd), path), pre2)
+            val fiS = sizeLimit(fi.asString, 40)
+            VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
+        }
 
-    def generateCorrectnessConditions(fd: FunDef): Seq[VC] = {
-      fd.body match {
-        case Some(body) =>
-          val calls = collectWithPC {
+      case None =>
+        Nil
+    }
+  }
 
-            case m @ MatchExpr(scrut, cases) =>
-              (m, VCKinds.ExhaustiveMatch, orJoin(cases map (matchCaseCondition(scrut, _))))
+  def generateCorrectnessConditions(fd: FunDef): Seq[VC] = {
 
-            case e @ Error(_, _) =>
-              (e, VCKinds.Assert, BooleanLiteral(false))
+    def eToVCKind(e: Expr) = e match {
+      case _ : MatchExpr =>
+        VCKinds.ExhaustiveMatch
 
-            case a @ Assert(cond, Some(err), _) => 
-              val kind = if (err.startsWith("Map ")) {
-                VCKinds.MapUsage
-              } else if (err.startsWith("Array ")) {
-                VCKinds.ArrayUsage
-              } else if (err.startsWith("Division ")) {
-                VCKinds.DivisionByZero
-              } else if (err.startsWith("Modulo ")) {
-                VCKinds.ModuloByZero
-              } else if (err.startsWith("Remainder ")) {
-                VCKinds.RemainderByZero
-              } else if (err.startsWith("Cast ")) {
-                VCKinds.CastError
-              } else {
-                VCKinds.Assert
-              }
+      case Assert(_, Some(err), _) =>
+        if (err.startsWith("Map ")) {
+          VCKinds.MapUsage
+        } else if (err.startsWith("Array ")) {
+          VCKinds.ArrayUsage
+        } else if (err.startsWith("Division ")) {
+          VCKinds.DivisionByZero
+        } else if (err.startsWith("Modulo ")) {
+          VCKinds.ModuloByZero
+        } else if (err.startsWith("Remainder ")) {
+          VCKinds.RemainderByZero
+        } else if (err.startsWith("Cast ")) {
+          VCKinds.CastError
+        } else {
+          VCKinds.Assert
+        }
 
-              (a, kind, cond)
-            case a @ Assert(cond, None, _) => (a, VCKinds.Assert, cond)
-            // Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
-            case a @ Ensuring(body, post) => (a, VCKinds.Assert, application(post, Seq(body)))
-          }(body)
+      case _ =>
+        VCKinds.Assert
+    }
 
-          calls.map {
-            case ((e, kind, correctnessCond), path) =>
-              val vc = implies(and(precOrTrue(fd), path), correctnessCond)
+    fd.body.toSeq.flatMap { body =>
+      // We don't collect preconditions here, because these are handled by generatePreconditions
+      val calls = collectCorrectnessConditions(body, collectFIs = false)
 
-              VC(vc, fd, kind).setPos(e)
-          }
+      calls.map {
+        case (e, correctnessCond) =>
+          val vc = implies(precOrTrue(fd), correctnessCond)
 
-        case None =>
-          Nil
+          VC(vc, fd, eToVCKind(e)).setPos(e)
       }
     }
+  }
+
 }

src/main/scala/leon/verification/Tactic.scala

@@ -10,7 +10,7 @@ import purescala.ExprOps._
 abstract class Tactic(vctx: VerificationContext) {
   val description : String
 
-  implicit val ctx = vctx.context
+  implicit protected val ctx = vctx.context
 
   def generateVCs(fd: FunDef): Seq[VC] = {
     generatePostconditions(fd) ++
@@ -28,10 +28,6 @@ abstract class Tactic(vctx: VerificationContext) {
     case None => BooleanLiteral(true)
   }
 
-  protected def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
-    CollectorWithPaths(f).traverse(expr)
-  }
-
   protected def sizeLimit(s: String, limit: Int) = {
     require(limit > 3)
     // Crop the call to display it properly