path dependent constraints

mytest/Abs.scala

@@ -3,9 +3,8 @@ import leon.Utils._
 object Abs {
 
 
-  def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = ({
-    require(size <= 5 && /*)
-    require(*/isArray(tab, size) && j >= 0 && j < size)
+  def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+    require(size <= 5 && isArray(tab, size))
     var k = 0
     var tabres = Map.empty[Int, Int]
     (while(k < size) {
@@ -14,9 +13,17 @@ object Abs {
       else
         tabres = tabres.updated(k, tab(k))
       k = k + 1
-    }) invariant(k >= 0 && k <= size && (if(j < k) tabres(j) >= 0 else true))
+    }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
     tabres
-  }) ensuring(res => res(j) >= 0)
+  }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+  def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+    require(isArray(a, size))
+    def rec(i: Int): Boolean = if(i >= size) true else {
+      if(a(i) < 0) false else rec(i+1)
+    }
+    rec(0)
+  }
 
   def isArray(a: Map[Int, Int], size: Int): Boolean = {
     if(size < 0)

mytest/Bubble.scala

@@ -2,8 +2,8 @@ import leon.Utils._
 
 object Bubble {
 
-  def sort(a: Map[Int, Int], size: Int, k: Int, l1: Int, l2: Int): Map[Int, Int] = ({
-    require(size <= 5 && size > 0 && k < size - 1 && k >= 0 && l1 < size && l1 >= 0 && l2 < size && l2 >= 0 && isArray(a, size))
+  def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+    require(size <= 5 && isArray(a, size))
     var i = size - 1
     var j = 0
     var sortedArray = a
@@ -17,35 +17,49 @@ object Bubble {
         }
         j = j + 1
       }) invariant(
-            isArray(sortedArray, size) && 
-            j >= 0 && 
             j <= i &&
-            (if(k >= i) sortedArray(k) <= sortedArray(k+1) else true) && 
-            (if(l1 <= i && l2 > i) sortedArray(l1) <= sortedArray(l2) else true)
+            isArray(sortedArray, size) && 
+            partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+            partitioned(sortedArray, size, 0, j-1, j, j) &&
+            sorted(sortedArray, size, i, size-1)
           )
       i = i - 1
     }) invariant(
+          i >= 0 &&
           isArray(sortedArray, size) && 
-          i >= 0 && 
-          i < size && 
-          (if(k >= i) sortedArray(k) <= sortedArray(k+1) else true) && 
-          (if(l1 <= i && l2 > i) sortedArray(l1) <= sortedArray(l2) else true)
+          partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+          sorted(sortedArray, size, i, size-1)
        )
     sortedArray
-  }) ensuring(res => res(k) <= res(k+1))
-  //ensuring(res => sorted(res, 0, size-1))
+  }) ensuring(res => sorted(res, size, 0, size-1))
 
-  //def sorted(a: Map[Int, Int], l: Int, u: Int): Boolean = {
-  //  require(isArray(a, u+1))
-  //  var k = l
-  //  var isSorted = true
-  //  while(k < u) {
-  //    if(a(k) > a(k+1))
-  //      isSorted = false
-  //    k = k + 1
-  //  }
-  //  isSorted
-  //}
+  def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+    require(isArray(a, size) && l >= 0 && u < size && l <= u)
+    var k = l
+    var isSorted = true
+    while(k <= u) {
+      if(a(k) > a(k+1))
+        isSorted = false
+      k = k + 1
+    }
+    isSorted
+  }
+  
+  def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+    require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size))
+    var i = l1
+    var j = l2
+    var isPartitionned = true
+    while(i <= u1) {
+      while(j <= u2) {
+        if(a(i) > a(j))
+          isPartitionned = false
+        j = j+1
+      }
+      i = i + 1
+    }
+    isPartitionned
+  }
 
 
   def isArray(a: Map[Int, Int], size: Int): Boolean = {

src/main/scala/leon/FunctionClosure.scala

@@ -11,10 +11,16 @@ object FunctionClosure extends Pass {
 
   private var enclosingPreconditions: List[Expr] = Nil
 
+  private var pathConstraints: List[Expr] = Nil
+  private var newFunDefs: Map[FunDef, FunDef] = Map()
+  //private var 
+
   def apply(program: Program): Program = {
+    newFunDefs = Map()
     val funDefs = program.definedFunctions
     funDefs.foreach(fd => {
       enclosingPreconditions = fd.precondition.toList
+      pathConstraints = fd.precondition.toList
       fd.body = Some(functionClosure(fd.getBody, fd.args.map(_.id).toSet))
     })
     program
@@ -22,52 +28,64 @@ object FunctionClosure extends Pass {
 
   private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
     case l @ LetDef(fd, rest) => {
+
       val id = fd.id
       val rt = fd.returnType
       val varDecl = fd.args
       val funBody = fd.getBody
-      val previousEnclosingPreconditions = enclosingPreconditions
-      enclosingPreconditions = fd.precondition match {
-        case Some(pre) => pre :: enclosingPreconditions
-        case None => enclosingPreconditions
-      }
-      val bodyVars: Set[Identifier] = variablesOf(funBody) 
-      val preconditionVars: Set[Identifier] = enclosingPreconditions.foldLeft(Set[Identifier]())((s, pre) => s ++ variablesOf(pre))
-      val vars = bodyVars ++ preconditionVars
-      val capturedVars = vars.intersect(bindedVars).toSeq // this should be the variable used that are in the scope
-      val freshVars: Map[Identifier, Identifier] = capturedVars.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
+      val precondition = fd.precondition
+      val postcondition = fd.postcondition
+
+      val bodyVars: Set[Identifier] = variablesOf(funBody) ++ variablesOf(precondition.getOrElse(BooleanLiteral(true)))
+      val capturedVars = bodyVars.intersect(bindedVars)// this should be the variable used that are in the scope
+      val (constraints, allCapturedVars) = filterConstraints(capturedVars) //all relevant path constraints
+      val capturedVarsWithConstraints = allCapturedVars.toSeq
+
+      val freshVars: Map[Identifier, Identifier] = capturedVarsWithConstraints.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
       val freshVarsExpr: Map[Expr, Expr] = freshVars.map(p => (p._1.toVariable, p._2.toVariable))
-      val freshBody = replace(freshVarsExpr, funBody)
+
       val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
       val newVarDecls = varDecl ++ extraVarDecls
       val newFunId = FreshIdentifier(id.name)
       val newFunDef = new FunDef(newFunId, rt, newVarDecls)
-      enclosingPreconditions = enclosingPreconditions.map(pre => replace(freshVarsExpr, pre)) //introduce the new variables name for the list of preconditions
-      newFunDef.precondition = enclosingPreconditions match {
-        case List() => None
-        case precs => Some(And(precs))
+
+      val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
+      val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
+      newFunDef.precondition = freshConstraints match {
+        case List() => freshPrecondition
+        case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
       }
-      newFunDef.postcondition = fd.postcondition.map(expr => replace(freshVarsExpr, expr))
+      newFunDef.postcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
+
       def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
         case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)))
         case _ => None
       }
+      val freshBody = replace(freshVarsExpr, funBody)
+      val oldPathConstraints = pathConstraints
+      pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
       val recBody = functionClosure(freshBody, bindedVars ++ newVarDecls.map(_.id))
+      pathConstraints = oldPathConstraints
       val recBody2 = searchAndReplaceDFS(substFunInvocInDef)(recBody)
       newFunDef.body = Some(recBody2)
+
       def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
-        case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVars.map(_.toVariable)))
+        case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)))
         case _ => None
       }
-      //need to remove the enclosing precondition before considering the rest
-      enclosingPreconditions = previousEnclosingPreconditions
       val recRest = functionClosure(rest, bindedVars)
       val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
       LetDef(newFunDef, recRest2).setType(l.getType)
     }
+
+    //case fi @ FunctionInvocation(fd, args) => {
+
+    //}
     case l @ Let(i,e,b) => {
       val re = functionClosure(e, bindedVars)
+      pathConstraints ::= Equals(Variable(i), re)
       val rb = functionClosure(b, bindedVars + i)
+      pathConstraints = pathConstraints.tail
       Let(i, re, rb).setType(l.getType)
     }
     case n @ NAryOperator(args, recons) => {
@@ -84,44 +102,40 @@ object FunctionClosure extends Pass {
       val r = functionClosure(t, bindedVars)
       recons(r).setType(u.getType)
     }
-    case i @ IfExpr(t1,t2,t3) => {
-      val r1 = functionClosure(t1, bindedVars)
-      val r2 = functionClosure(t2, bindedVars)
-      val r3 = functionClosure(t3, bindedVars)
-      IfExpr(r1, r2, r3).setType(i.getType)
+    case i @ IfExpr(cond,then,elze) => {
+      val rCond = functionClosure(cond, bindedVars)
+      pathConstraints ::= rCond
+      val rThen = functionClosure(then, bindedVars)
+      pathConstraints = pathConstraints.tail
+      pathConstraints ::= Not(rCond)
+      val rElze = functionClosure(elze, bindedVars)
+      pathConstraints = pathConstraints.tail
+      IfExpr(rCond, rThen, rElze).setType(i.getType)
     }
     case m @ MatchExpr(scrut,cses) => sys.error("Will see")//MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPosInfo(m)
     case t if t.isInstanceOf[Terminal] => t
     case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
   }
 
-  //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, then, elze) => {
-  //        rec(cond, path)
-  //        rec(then, 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
-  //}
+  //filter the list of constraints, only keeping those relevant to the set of variables
+  def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
+    var allVars = vars
+    var newVars: Set[Identifier] = Set()
+    var constraints = pathConstraints
+    var filteredConstraints: List[Expr] = Nil
+    do {
+      allVars ++= newVars
+      newVars = Set()
+      constraints = pathConstraints.filterNot(filteredConstraints.contains(_))
+      constraints.foreach(expr => {
+        val vs = variablesOf(expr)
+        if(!vs.intersect(allVars).isEmpty) {
+          filteredConstraints ::= expr
+          newVars ++= vs.diff(allVars)
+        }
+      })
+    } while(newVars != Set())
+    (filteredConstraints, allVars)
+  }
+
 }