Finished syntactic checks for foralls

src/main/scala/leon/purescala/CheckForalls.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package purescala
+
+import Common._
+import Definitions._
+import Expressions._
+import Extractors._
+import ExprOps._
+
+object CheckForalls extends UnitPhase[Program] {
+  
+  val name = "Foralls"
+  val description = "Check syntax of foralls to guarantee sound instantiations"
+
+  def apply(ctx: LeonContext, program: Program) = {
+    program.definedFunctions.foreach { fd =>
+      if (fd.body.exists(b => exists {
+        case f: Forall => true
+        case _ => false
+      } (b))) ctx.reporter.warning("Universal quantification in function bodies is not supported in " + fd)
+
+      val foralls = (fd.precondition.toSeq ++ fd.postcondition.toSeq).flatMap { prec =>
+        collect[Forall] {
+          case f: Forall => Set(f)
+          case _ => Set.empty
+        } (prec)
+      }
+
+      val free = fd.params.map(_.id).toSet ++ (fd.postcondition match {
+        case Some(Lambda(args, _)) => args.map(_.id)
+        case _ => Seq.empty
+      })
+
+      object Matcher {
+        def unapply(e: Expr): Option[(Identifier, Seq[Expr])] = e match {
+          case Application(Variable(id), args) if free(id) => Some(id -> args)
+          case ArraySelect(Variable(id), index) if free(id) => Some(id -> Seq(index))
+          case MapGet(Variable(id), key) if free(id) => Some(id -> Seq(key))
+          case _ => None
+        }
+      }
+
+      for (Forall(args, TopLevelAnds(conjuncts)) <- foralls) {
+        val quantified = args.map(_.id).toSet
+
+        for (conjunct <- conjuncts) {
+          val matchers = collect[(Identifier, Seq[Expr])] {
+            case Matcher(id, args) => Set(id -> args)
+            case _ => Set.empty
+          } (conjunct)
+
+          if (matchers.exists { case (id, args) =>
+            args.exists(arg => arg match {
+              case Matcher(_, _) => false
+              case Variable(id) => false
+              case _ if (variablesOf(arg) & quantified).nonEmpty => true
+              case _ => false
+            })
+          }) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
+
+          if (matchers.map(_._1).toSet.size != 1)
+            ctx.reporter.warning("Quantification conjuncts must contain exactly one matcher in " + conjunct)
+
+          preTraversal {
+            case Matcher(_, _) => // OK
+            case LessThan(_: Variable, _: Variable) => // OK
+            case LessEquals(_: Variable, _: Variable) => // OK
+            case GreaterThan(_: Variable, _: Variable) => // OK
+            case GreaterEquals(_: Variable, _: Variable) => // OK
+            case And(_) => // OK
+            case Or(_) => // OK
+            case Implies(_, _) => // OK
+            case BinaryOperator(Matcher(_, _), _, _) => // OK
+            case BinaryOperator(_, Matcher(_, _), _) => // OK
+            case BinaryOperator(e1, _, _) if (variablesOf(e1) & quantified).isEmpty => // OK
+            case BinaryOperator(_, e2, _) if (variablesOf(e2) & quantified).isEmpty => // OK
+            case FunctionInvocation(_, args) if {
+              val argVars = args.flatMap(variablesOf).toSet
+              (argVars & quantified).size <= 1 && (argVars & free).isEmpty
+            } => // OK
+            case UnaryOperator(_, _) => // OK
+            case BinaryOperator(e1, e2, _) if ((variablesOf(e1) ++ variablesOf(e2)) & quantified).isEmpty => // OK
+            case NAryOperator(es, _) if (es.flatMap(variablesOf).toSet & quantified).isEmpty => // OK
+            case _: Terminal => // OK
+            case e => ctx.reporter.warning("Invalid operation " + e + " on quantified variables")
+          } (conjunct)
+        }
+      }
+    }
+  }
+}

src/main/scala/leon/solvers/templates/QuantificationManager.scala

@@ -94,6 +94,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
 
   private var knownStack: List[Set[T]] = List(Set.empty)
   private def known(idT: T): Boolean = knownStack.head(idT) || byID.isDefinedAt(idT)
+  private def correspond(qm: Matcher[T], m: Matcher[T]): Boolean = qm.tpe match {
+    case _: FunctionType => qm.tpe == m.tpe && (qm.caller == m.caller || !known(m.caller))
+    case _ => qm.tpe == m.tpe
+  }
 
   override def push(): Unit = {
     quantificationsStack = quantifications :: quantificationsStack
@@ -156,7 +160,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     }
 
     def instantiate(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
-      val Matcher(caller, tpe, args) = matcher
 
       // Build a mapping from applications in the quantified statement to all potential concrete
       // applications previously encountered. Also make sure the current `app` is in the mapping
@@ -165,25 +168,21 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       val matcherMappings: Set[Set[(T, Matcher[T], Matcher[T])]] = matchers
         // 1. select an application in the quantified proposition for which the current app can
         //    be bound when generating the new constraints
-        .filter(_.tpe == tpe)
+        .filter(qm => correspond(qm, matcher))
         // 2. build the instantiation mapping associated to the chosen current application binding
         .flatMap { bindingMatcher => matchers
           // 2.1. select all potential matches for each quantified application
-          .map { case qm @ Matcher(qcaller, qtpe, qargs) =>
-            if (qm == bindingMatcher) {
-              bindingMatcher -> Set(blocker -> matcher)
-            } else {
-              val instances: Set[(T, Matcher[T])] = instantiated.filter {
-                case (b, m @ Matcher(caller, tpe, _)) => tpe == qtpe
-              }
-
-              // concrete applications can appear multiple times in the constraint, and this is also the case
-              // for the current application for which we are generating the constraints
-              val withCurrent = if (tpe == qtpe) instances + (blocker -> matcher) else instances
-
-              qm -> withCurrent
-            }
-          }
+          .map(qm => if (qm == bindingMatcher) {
+            bindingMatcher -> Set(blocker -> matcher)
+          } else {
+            val instances: Set[(T, Matcher[T])] = instantiated.filter { case (b, m) => correspond(qm, m) }
+
+            // concrete applications can appear multiple times in the constraint, and this is also the case
+            // for the current application for which we are generating the constraints
+            val withCurrent = if (correspond(qm, matcher)) instances + (blocker -> matcher) else instances
+
+            qm -> withCurrent
+          })
           // 2.2. based on the possible bindings for each quantified application, build a set of
           //      instantiation mappings that can be used to instantiate all necessary constraints
           .foldLeft[Set[Set[(T, Matcher[T], Matcher[T])]]] (Set(Set.empty)) {

src/main/scala/leon/solvers/templates/Templates.scala

@@ -126,6 +126,8 @@ object Template {
 
   private def matchersOf[T](encodeExpr: Expr => T)(expr: Expr): Set[Matcher[T]] = collect[Matcher[T]] {
     case Application(caller, args) => Set(Matcher(encodeExpr(caller), caller.getType, args.map(encodeExpr)))
+    case ArraySelect(arr, index) => Set(Matcher(encodeExpr(arr), arr.getType, Seq(encodeExpr(index))))
+    case MapGet(map, key) => Set(Matcher(encodeExpr(map), map.getType, Seq(encodeExpr(key))))
     case _ => Set.empty
   }(expr)
 

src/main/scala/leon/utils/PreprocessingPhase.scala

@@ -34,7 +34,8 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Tran
       CompleteAbstractDefinitions            andThen
       CheckADTFieldsTypes                    andThen
       InjectAsserts                          andThen
-      InliningPhase
+      InliningPhase                          andThen
+      CheckForalls
 
     val pipeX = if(desugarXLang) {
       XLangDesugaringPhase andThen