Added coverage test suite.

src/main/scala/leon/purescala/Constructors.scala

@@ -61,7 +61,7 @@ object Constructors {
     else bd
   }
 
-  /** $encodingof ``val (id1, id2, ...) = e; bd``, and returns `bd` if the identifiers are not bound in `bd`.
+  /** $encodingof ``val (...binders...) = value; body`` which is translated to  ``value match { case (...binders...) => body }``, and returns `body` if the identifiers are not bound in `body`.
     * @see [[purescala.Expressions.Let]]
     */
   def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
@@ -72,7 +72,7 @@ object Constructors {
     case xs =>
       require(
         value.getType.isInstanceOf[TupleType],
-        s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$this"
+        s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$value"
       )
 
       Extractors.LetPattern(TuplePattern(None,binders map { b => WildcardPattern(Some(b)) }), value, body)

src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala

@@ -33,10 +33,10 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
   /** If the sub-branches contain identifiers, it returns them unchanged.
       Else it creates a new boolean indicating this branch. */
   def wrapBranch(e: (Expr, Seq[Identifier])): (Expr, Seq[Identifier]) = {
-    if(e._2.isEmpty) { // No need to introduce a new boolean since if one of the child booleans is true, then this IfExpr has been called.
-      val b = FreshIdentifier("l" + e._1.getPos.line + "c" + e._1.getPos.col)
+    if(e._2.isEmpty) {
+      val b = FreshIdentifier("l" + e._1.getPos.line + "c" + e._1.getPos.col, BooleanType)
       (tupleWrap(Seq(e._1, Variable(b))), Seq(b))
-    } else e
+    } else e // No need to introduce a new boolean since if one of the child booleans is true, then this IfExpr has been called.
   }
   
   def hasConditionals(e: Expr) = {
@@ -53,8 +53,13 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
       val (c1, cv1) = markBranches(cond)
       val (t1, tv1) = wrapBranch(markBranches(thenn))
       val (e1, ev1) = wrapBranch(markBranches(elze))
-      // TODO: Deal with the case when t1 and e1 is empty.
-      (IfExpr(c1, t1, e1).copiedFrom(e), cv1 ++ tv1 ++ ev1)
+      if(cv1.isEmpty) {
+        (IfExpr(c1, t1, e1).copiedFrom(e), tv1 ++ ev1)
+      } else {
+        val arg_id = FreshIdentifier("arg", BooleanType)
+        val arg_b = FreshIdentifier("b", BooleanType)
+        (letTuple(Seq(arg_id, arg_b), c1, IfExpr(Variable(arg_id), t1, e1).copiedFrom(e)), cv1 ++ tv1 ++ ev1)
+      }
     case MatchExpr(scrut, cases) =>
       val (c1, cv1) = markBranches(scrut)
       val (new_cases, variables) = (cases map { case MatchCase(pattern, opt, rhs) =>
@@ -77,15 +82,21 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
           }
       }
       e match {
-        case FunctionInvocation(TypedFunDef(fd, targs), args) =>
-          // Should be different since functions will return a boolean as well.
+        case FunctionInvocation(TypedFunDef(fd, targs), args) if fds(fd) =>
+          val new_fd = wrapFunDef(fd)
+          // Is different since functions will return a boolean as well.
           val res_id = FreshIdentifier("res", fd.returnType)
           val res_b = FreshIdentifier("b", BooleanType)
-          val finalIds = (ids :+ res_b)
-          val finalExpr = 
-            tupleWrap(Seq(Variable(res_id), or(finalIds.map(Variable(_)): _*)))
-          val funCall = letTuple(Seq(res_id, res_b), builder(children).copiedFrom(e), finalExpr)
-          (exprBuilder(funCall), finalIds)
+          if(ids.isEmpty) {
+            val funCall = FunctionInvocation(TypedFunDef(new_fd, targs), children).copiedFrom(e)
+            (exprBuilder(funCall), Seq(res_b))
+          } else {
+            val finalIds = (ids :+ res_b)
+            val finalExpr = 
+              tupleWrap(Seq(Variable(res_id), or(finalIds.map(Variable(_)): _*)))
+            val funCall = letTuple(Seq(res_id, res_b), FunctionInvocation(TypedFunDef(new_fd, targs), children).copiedFrom(e), finalExpr)
+            (exprBuilder(funCall), finalIds)
+          }
         case _ =>
           if(ids.isEmpty) {
             (e, Seq.empty)
@@ -96,6 +107,17 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
       }
   }
   
+  var cache = Map[FunDef, FunDef]()
+  
+  def wrapFunDef(fd: FunDef): FunDef = {
+    if(!(cache contains fd)) {
+      val new_fd = fd.duplicate(returnType = TupleType(Seq(fd.returnType, BooleanType)))
+      new_fd.body = None
+      cache += fd -> new_fd
+    }
+    cache(fd)
+  }
+  
   /** The number of expressions is the same as the number of arguments. */
   def result(): Stream[Seq[Expr]] = {
     /* Algorithm:

src/test/scala/leon/integration/solvers/InputCoverageSuite.scala

+package leon.integration.solvers
+
+import org.scalatest.FunSuite
+import org.scalatest.Matchers
+import leon.test.helpers.ExpressionsDSL
+import leon.solvers.string.StringSolver
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Common.Identifier
+import leon.purescala.Expressions._
+import leon.purescala.Definitions._
+import leon.purescala.DefOps
+import leon.purescala.ExprOps
+import leon.purescala.Types._
+import leon.purescala.TypeOps
+import leon.purescala.Constructors._
+import leon.synthesis.rules.{StringRender, TypedTemplateGenerator}
+import scala.collection.mutable.{HashMap => MMap}
+import scala.concurrent.Future
+import scala.concurrent.ExecutionContext.Implicits.global
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import org.scalatest.FunSuite
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import leon.purescala.Types.Int32Type
+import leon.test.LeonTestSuiteWithProgram
+import leon.synthesis.SourceInfo
+import leon.synthesis.CostModels
+import leon.synthesis.graph.AndNode
+import leon.synthesis.SearchContext
+import leon.synthesis.Synthesizer
+import leon.synthesis.SynthesisSettings
+import leon.synthesis.RuleApplication
+import leon.synthesis.RuleClosed
+import leon.evaluators._
+import leon.LeonContext
+import leon.synthesis.rules.DetupleInput
+import leon.synthesis.Rules
+import leon.solvers.ModelBuilder
+import scala.language.implicitConversions
+import leon.LeonContext
+import leon.test.LeonTestSuiteWithProgram
+import leon.test.helpers.ExpressionsDSL
+import leon.synthesis.disambiguation.InputCoverage
+import leon.test.helpers.ExpressionsDSLProgram
+import leon.test.helpers.ExpressionsDSLVariables
+
+class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables {
+  val sources = List("""
+    |import leon.lang._
+    |import leon.collection._
+    |import leon.lang.synthesis._
+    |import leon.annotation._
+    |
+    |object InputCoverageSuite {
+    |  def dummy = 2
+    |  def withIf(cond: Boolean) = {
+    |    if(cond) {
+    |      1
+    |    } else {
+    |      2
+    |    }
+    |  }
+    |  def withIfInIf(cond: Boolean) = {
+    |    if(if(cond) false else true) {
+    |      1
+    |    } else {
+    |      2
+    |    }
+    |  }
+    |  
+    |  def withCoveredFun1(input: Int) = {
+    |    withCoveredFun2(input - 5) + withCoveredFun2(input + 5)
+    |  }
+    |  
+    |  def withCoveredFun2(input: Int) = {
+    |    if(input > 0) {
+    |      2
+    |    } else {
+    |      0
+    |    }
+    |  }
+    |  
+    |  def withCoveredFun3(input: Int) = {
+    |    withCoveredFun2(withCoveredFun2(input + 5))
+    |  }
+    |}""".stripMargin)
+    
+  test("wrapBranch should wrap expressions if they are not already containing wrapped calls"){ ctxprogram =>
+    implicit val (c, p) = ctxprogram
+    val dummy = funDef("InputCoverageSuite.dummy")
+    val coverage = new InputCoverage(dummy, Set(dummy))
+    val simpleExpr = Plus(IntLiteral(1), b)
+    coverage.wrapBranch((simpleExpr, Seq(p.id, q.id))) should equal ((simpleExpr, Seq(p.id, q.id)))
+    val (covered, ids) = coverage.wrapBranch((simpleExpr, Seq()))
+    ids should have size 1
+    covered should equal (Tuple(Seq(simpleExpr, Variable(ids.head))))
+  }
+  
+  test("If-coverage should work"){ ctxprogram =>
+    implicit val (c, p) = ctxprogram
+    val withIf = funDef("InputCoverageSuite.withIf")
+    val coverage = new InputCoverage(withIf, Set(withIf))
+    val expr = withIf.body.get
+    
+    val (res, ids) = coverage.markBranches(expr)
+    ids should have size 2
+    expr match {
+      case IfExpr(cond, thenn, elze) =>
+        res should equal (IfExpr(cond, Tuple(Seq(thenn, Variable(ids(0)))), Tuple(Seq(elze, Variable(ids(1))))))
+      case _ => fail(s"$expr is not an IfExpr")
+    }
+  }
+  
+  test("If-cond-coverage should work"){ ctxprogram =>
+    implicit val (c, p) = ctxprogram
+    val withIfInIf = funDef("InputCoverageSuite.withIfInIf")
+    val coverage = new InputCoverage(withIfInIf, Set(withIfInIf))
+    val expr = withIfInIf.body.get
+    
+    val (res, ids) = coverage.markBranches(expr)
+    ids should have size 4
+    expr match {
+      case IfExpr(IfExpr(cond, t1, e1), t2, e2) =>
+        res match {
+          case MatchExpr(IfExpr(c, t1, e1), Seq(MatchCase(TuplePattern(None, s), None, IfExpr(c2, t2, e2)))) if s.size == 2 =>
+          case _ => fail("should have a shape like (if() else ) match { case (a, b) => if(...) else }")
+        }
+      case _ => fail(s"$expr is not an IfExpr")
+    }
+  }
+  
+  test("fundef combination-coverage should work"){ ctxprogram =>
+    implicit val (c, p) = ctxprogram
+    val withCoveredFun1 = funDef("InputCoverageSuite.withCoveredFun1")
+    val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
+    val coverage = new InputCoverage(withCoveredFun1, Set(withCoveredFun1, withCoveredFun2))
+    val expr = withCoveredFun1.body.get
+    
+    val (res, ids) = coverage.markBranches(expr)
+    ids should have size 2
+    
+    res match {
+      case MatchExpr(funCall, Seq(
+            MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a1)), WildcardPattern(Some(b1)))), None,
+              MatchExpr(funCall2, Seq(
+                MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a2)), WildcardPattern(Some(b2)))), None,
+                  Tuple(Seq(BVPlus(Variable(ida1), Variable(ida2)), Or(Seq(Variable(idb1), Variable(idb2)))))
+            )
+          ))))) =>
+        withClue(res.toString) {
+          ida1 shouldEqual a1
+          ida2 shouldEqual a2
+          Set(idb1.uniqueName, idb2.uniqueName) shouldEqual Set(b1.uniqueName, b2.uniqueName)
+        }
+      case _ =>
+        fail(s"$res is not of type funCall() match { case (a1, b1) => funCall() match { case (a2, b2) => (a1 + a2, b1 || b2) } }")
+    }
+  }
+  
+  test("fundef composition-coverage should work"){ ctxprogram =>
+    implicit val (c, p) = ctxprogram
+    val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
+    val withCoveredFun3 = funDef("InputCoverageSuite.withCoveredFun3")
+    val coverage = new InputCoverage(withCoveredFun3, Set(withCoveredFun3, withCoveredFun2))
+    val expr = withCoveredFun3.body.get
+    
+    val (res, ids) = coverage.markBranches(expr)
+    ids should have size 2
+    res match {
+      case MatchExpr(funCall, Seq(
+            MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a)), WildcardPattern(Some(b1)))), None,
+              MatchExpr(FunctionInvocation(_, Seq(Variable(ida))), Seq(
+                MatchCase(TuplePattern(None, Seq(WildcardPattern(_), WildcardPattern(Some(b2)))), None,
+                  Tuple(Seq(p, Or(Seq(Variable(id1), Variable(id2)))))
+            )
+          ))))) if ida == a && id1 == b1 && id2 == b2 =>
+      case _ =>
+        fail(s"$res is not of type funCall() match { case (a, b1) => funCall(a) match { case (c, b2) => (c, b1 || b2) } }")
+    }
+  }
+}
\ No newline at end of file

src/test/scala/leon/test/helpers/ExpressionsDSL.scala

@@ -9,6 +9,10 @@ import leon.purescala.Common._
 import leon.purescala.Types._
 import leon.purescala.Expressions._
 
+trait ExpressionsDSLVariables_a {
+  val a = FreshIdentifier("a", Int32Type).toVariable
+}
+
 trait ExpressionsDSLVariables {
   val F = BooleanLiteral(false)
   val T = BooleanLiteral(true)
@@ -18,7 +22,6 @@ trait ExpressionsDSLVariables {
   def i(x: Int)     = IntLiteral(x)
   def r(n: BigInt, d: BigInt)  = FractionalLiteral(n, d)
 
-  val a = FreshIdentifier("a", Int32Type).toVariable
   val b = FreshIdentifier("b", Int32Type).toVariable
   val c = FreshIdentifier("c", Int32Type).toVariable
 
@@ -97,7 +100,7 @@ self: Assertions =>
   }
 }
 
-trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
+trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram with ExpressionsDSLVariables_a {
   self: Assertions =>
   
 }