diff --git a/library/theories/String.scala b/library/theories/String.scala
index 85e4d90c7e1eca5a72a2d7c74aa0c63437d6c872..ca2b9027df5a9628ab3140416897ee6274904ff9 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -30,3 +30,47 @@ sealed abstract class String {
case class StringCons(head: Char, tail: String) extends String
case class StringNil() extends String
+
+@library
+object String {
+ def fromChar(i: Char): String = {
+ StringCons(i, StringNil())
+ }
+
+ @isabelle.noBody()
+ def fromBigInt(i: BigInt): String =
+ if(i < 0) StringCons('-', fromBigInt(-i))
+ else if(i == BigInt(0)) StringCons('0', StringNil())
+ else if(i == BigInt(1)) StringCons('1', StringNil())
+ else if(i == BigInt(2)) StringCons('2', StringNil())
+ else if(i == BigInt(3)) StringCons('3', StringNil())
+ else if(i == BigInt(4)) StringCons('4', StringNil())
+ else if(i == BigInt(5)) StringCons('5', StringNil())
+ else if(i == BigInt(6)) StringCons('6', StringNil())
+ else if(i == BigInt(7)) StringCons('7', StringNil())
+ else if(i == BigInt(8)) StringCons('8', StringNil())
+ else if(i == BigInt(9)) StringCons('9', StringNil())
+ else fromBigInt(i / 10).concat(fromBigInt(i % 10))
+
+ @isabelle.noBody()
+ def fromInt(i: Int): String = i match {
+ case -2147483648 => StringCons('-', StringCons('2', fromInt(147483648)))
+ case i if i < 0 => StringCons('-', fromInt(-i))
+ case 0 => StringCons('0', StringNil())
+ case 1 => StringCons('1', StringNil())
+ case 2 => StringCons('2', StringNil())
+ case 3 => StringCons('3', StringNil())
+ case 4 => StringCons('4', StringNil())
+ case 5 => StringCons('5', StringNil())
+ case 6 => StringCons('6', StringNil())
+ case 7 => StringCons('7', StringNil())
+ case 8 => StringCons('8', StringNil())
+ case 9 => StringCons('9', StringNil())
+ case i => fromInt(i / 10).concat(fromInt(i % 10))
+ }
+
+ def fromBoolean(b: Boolean): String = {
+ if(b) StringCons('t', StringCons('r', StringCons('u', StringCons('e', StringNil()))))
+ else StringCons('f', StringCons('a', StringCons('l', StringCons('s', StringCons('e', StringNil())))))
+ }
+}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 67dcf315770120734684a459bad0b0d3be96120e..8597a0af22859ba0f730a0b534dd0b244a79a2c0 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/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)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 6b7bf67e0ce10066f4719a34101fcb0d97cf17bc..db8905963760058b97611f0e2b966728cb8b2fd9 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -97,17 +97,17 @@ object DefOps {
}
private def stripPrefix(off: List[String], from: List[String]): List[String] = {
- val commonPrefix = (off zip from).takeWhile(p => p._1 == p._2)
+ val commonPrefix = (off zip from).takeWhile(p => p._1 == p._2)
- val res = off.drop(commonPrefix.size)
+ val res = off.drop(commonPrefix.size)
- if (res.isEmpty) {
- if (off.isEmpty) List()
- else List(off.last)
- } else {
- res
+ if (res.isEmpty) {
+ if (off.isEmpty) List()
+ else List(off.last)
+ } else {
+ res
+ }
}
- }
def simplifyPath(namesOf: List[String], from: Definition, useUniqueIds: Boolean)(implicit pgm: Program) = {
val pathFrom = pathFromRoot(from).dropWhile(_.isInstanceOf[Program])
@@ -318,14 +318,23 @@ object DefOps {
val transformer = new DefinitionTransformer(idMap, fdMap, cdMap) {
override def transformExpr(expr: Expr)(implicit bindings: Map[Identifier, Identifier]): Option[Expr] = expr match {
case fi @ FunctionInvocation(TypedFunDef(fd, tps), args) =>
- fiMapF(fi, transform(fd))
+ val transformFd = transform(fd)
+ if(transformFd != fd)
+ fiMapF(fi, transformFd)
+ else
+ None
//val nfi = fiMapF(fi, transform(fd)) getOrElse expr
//Some(super.transform(nfi))
case cc @ CaseClass(cct, args) =>
- ciMapF(cc, transform(cct).asInstanceOf[CaseClassType])
+ val transformCct = transform(cct).asInstanceOf[CaseClassType]
+ if(transformCct != cct)
+ ciMapF(cc, transformCct)
+ else
+ None
//val ncc = ciMapF(cc, transform(cct).asInstanceOf[CaseClassType]) getOrElse expr
//Some(super.transform(ncc))
- case _ => None
+ case _ =>
+ None
}
override def transformFunDef(fd: FunDef): Option[FunDef] = fdMapF(fd)
@@ -356,8 +365,9 @@ object DefOps {
fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap)
: (Program, Map[Identifier, Identifier], Map[FunDef, FunDef], Map[ClassDef, ClassDef]) = {
replaceDefs(p)(fdMapF, cd => None, fiMapF)
- }
+ }
+ /** Replaces all function calls by an expression depending on the previous function invocation and the new mapped function */
def replaceFunCalls(e: Expr, fdMapF: FunDef => FunDef, fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap): Expr = {
preMap {
case me @ MatchExpr(scrut, cases) =>
@@ -606,9 +616,9 @@ object DefOps {
case AsInstanceOf(e, ct) => Some(AsInstanceOf(e, tpMap(ct)))
case MatchExpr(scrut, cases) =>
Some(MatchExpr(scrut, cases.map{
- case MatchCase(pattern, optGuard, rhs) =>
- MatchCase(replaceClassDefUse(pattern), optGuard, rhs)
- }))
+ case MatchCase(pattern, optGuard, rhs) =>
+ MatchCase(replaceClassDefUse(pattern), optGuard, rhs)
+ }))
case fi @ FunctionInvocation(TypedFunDef(fd, tps), args) =>
defaultFiMap(fi, fdMap(fd)).map(_.setPos(fi))
case _ =>
@@ -662,7 +672,7 @@ object DefOps {
p.definedFunctions.filter(f => f.id.name == after.id.name).map(fd => fd.id.name + " : " + fd) match {
case Nil =>
case e => println("Did you mean " + e)
- }
+ }
println(Thread.currentThread().getStackTrace.map(_.toString).take(10).mkString("\n"))
}
diff --git a/src/main/scala/leon/solvers/theories/StringEncoder.scala b/src/main/scala/leon/solvers/theories/StringEncoder.scala
index 0519814409d09e717babfd17f37a3a541b88c607..02293fab327e7a79f1bb682c5fca65857a45bfd8 100644
--- a/src/main/scala/leon/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/StringEncoder.scala
@@ -22,6 +22,12 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
val Drop = p.library.lookupUnique[FunDef]("leon.theories.String.drop").typed
val Slice = p.library.lookupUnique[FunDef]("leon.theories.String.slice").typed
val Concat = p.library.lookupUnique[FunDef]("leon.theories.String.concat").typed
+
+ val FromInt = p.library.lookupUnique[FunDef]("leon.theories.String.fromInt").typed
+ val FromChar = p.library.lookupUnique[FunDef]("leon.theories.String.fromChar").typed
+ val FromBoolean = p.library.lookupUnique[FunDef]("leon.theories.String.fromBoolean").typed
+ val FromBigInt = p.library.lookupUnique[FunDef]("leon.theories.String.fromBigInt").typed
+
private val stringBijection = new Bijection[String, Expr]()
@@ -48,6 +54,14 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
Some(FunctionInvocation(Take, Seq(FunctionInvocation(Drop, Seq(transform(a), transform(start))), transform(length))).copiedFrom(e))
case SubString(a, start, end) =>
Some(FunctionInvocation(Slice, Seq(transform(a), transform(start), transform(end))).copiedFrom(e))
+ case Int32ToString(a) =>
+ Some(FunctionInvocation(FromInt, Seq(transform(a))).copiedFrom(e))
+ case IntegerToString(a) =>
+ Some(FunctionInvocation(FromBigInt, Seq(transform(a))).copiedFrom(e))
+ case CharToString(a) =>
+ Some(FunctionInvocation(FromChar, Seq(transform(a))).copiedFrom(e))
+ case BooleanToString(a) =>
+ Some(FunctionInvocation(FromBoolean, Seq(transform(a))).copiedFrom(e))
case _ => None
}
@@ -85,6 +99,14 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
case FunctionInvocation(Drop, Seq(a, count)) =>
val ra = transform(a)
Some(SubString(ra, transform(count), StringLength(ra)).copiedFrom(e))
+ case FunctionInvocation(FromInt, Seq(a)) =>
+ Some(Int32ToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromBigInt, Seq(a)) =>
+ Some(IntegerToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromChar, Seq(a)) =>
+ Some(CharToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromBoolean, Seq(a)) =>
+ Some(BooleanToString(transform(a)).copiedFrom(e))
case _ => None
}
diff --git a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
new file mode 100644
index 0000000000000000000000000000000000000000..775ed59d81c48fd97590ca6c848b76a1f3540d7e
--- /dev/null
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -0,0 +1,284 @@
+package leon
+package synthesis.disambiguation
+
+import synthesis.RuleClosed
+import synthesis.Solution
+import evaluators.DefaultEvaluator
+import purescala.Expressions._
+import purescala.ExprOps
+import purescala.Constructors._
+import purescala.Extractors._
+import purescala.Types.{TypeTree, TupleType, BooleanType}
+import purescala.Common.{Identifier, FreshIdentifier}
+import purescala.Definitions.{FunDef, Program, TypedFunDef, ValDef}
+import purescala.DefOps
+import grammars.ValueGrammar
+import bonsai.enumerators.MemoizedEnumerator
+import solvers.Model
+import solvers.ModelBuilder
+import scala.collection.mutable.ListBuffer
+import leon.LeonContext
+import leon.purescala.Definitions.TypedFunDef
+import leon.verification.VerificationContext
+import leon.verification.VerificationPhase
+import leon.solvers._
+import scala.concurrent.duration._
+import leon.verification.VCStatus
+import leon.verification.VCResult
+import leon.evaluators.AbstractEvaluator
+
+/**
+ * @author Mikael
+ * If possible, synthesizes a set of inputs for the function so that they cover all parts of the function.
+ *
+ * @param fds The set of functions to cover
+ * @param fd The calling function
+ */
+class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Program) {
+
+ /** If set, performs a cleaning up step to cover the whole function */
+ var minimizeExamples: Boolean = true
+
+ /** If the sub-branches contain identifiers, it returns them unchanged.
+ Else it creates a new boolean indicating this branch. */
+ def wrapBranch(e: (Expr, Option[Seq[Identifier]])): (Expr, Some[Seq[Identifier]]) = e._2 match {
+ case None =>
+ val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType)
+ (tupleWrap(Seq(e._1, Variable(b))), Some(Seq(b)))
+ case Some(Seq()) =>
+ val b = FreshIdentifier("l" + Math.abs(e._1.getPos.line) + "c" + Math.abs(e._1.getPos.col), BooleanType)
+
+ def putInLastBody(e: Expr): Expr = e match {
+ case Tuple(Seq(v, prev_b)) => Tuple(Seq(v, or(prev_b, b.toVariable))).copiedFrom(e)
+ case LetTuple(binders, value, body) => letTuple(binders, value, putInLastBody(body)).copiedFrom(e)
+ case MatchExpr(scrut, Seq(MatchCase(TuplePattern(optId, binders), None, rhs))) =>
+ MatchExpr(scrut, Seq(MatchCase(TuplePattern(optId, binders), None, putInLastBody(rhs)))).copiedFrom(e)
+ case _ => throw new Exception(s"Unexpected branching case: $e")
+
+ }
+ (putInLastBody(e._1), Some(Seq(b)))
+ case e_2: Some[_] =>
+ // No need to introduce a new boolean since if one of the child booleans is true, then this IfExpr has been called.
+ (e._1, e_2)
+ }
+
+ /** Returns true if there are some branching to monitor in the expression */
+ def hasConditionals(e: Expr) = {
+ ExprOps.exists{ case i:IfExpr => true case m: MatchExpr => true case f: FunctionInvocation if fds(f.tfd.fd) || f.tfd.fd == fd => true case _ => false}(e)
+ }
+
+ /** Merges two set of identifiers.
+ * None means that the attached expression is the original one,
+ * Some(ids) means that it has been augmented with booleans and ids are the "monitoring" boolean flags. */
+ def merge(a: Option[Seq[Identifier]], b: Option[Seq[Identifier]]) = {
+ (a, b) match {
+ case (None, None) => None
+ case (a, None) => a
+ case (None, b) => b
+ case (Some(a), Some(b)) => Some(a ++ b)
+ }
+ }
+
+ /** For each branch in the expression, adds a boolean variable such that the new type of the expression is (previousType, Boolean)
+ * If no variable is output, then the type of the expression is not changed.
+ * If the expression is augmented with a boolean, returns the list of boolean variables which appear in the expression */
+ def markBranches(e: Expr): (Expr, Option[Seq[Identifier]]) =
+ if(!hasConditionals(e)) (e, None) else e match {
+ case IfExpr(cond, thenn, elze) =>
+ val (c1, cv1) = markBranches(cond)
+ val (t1, tv1) = wrapBranch(markBranches(thenn))
+ val (e1, ev1) = wrapBranch(markBranches(elze))
+ cv1 match {
+ case None =>
+ (IfExpr(c1, t1, e1).copiedFrom(e), merge(tv1, ev1))
+ case cv1 =>
+ val arg_id = FreshIdentifier("arg", BooleanType)
+ val arg_b = FreshIdentifier("bc", BooleanType)
+ (letTuple(Seq(arg_id, arg_b), c1, IfExpr(Variable(arg_id), t1, e1).copiedFrom(e)).copiedFrom(e), merge(merge(cv1, tv1), ev1))
+ }
+ case MatchExpr(scrut, cases) =>
+ val (c1, cv1) = markBranches(scrut)
+ val (new_cases, variables) = (cases map { case m@MatchCase(pattern, opt, rhs) =>
+ val (rhs_new, ids) = wrapBranch(markBranches(rhs))
+ (MatchCase(pattern, opt, rhs_new).copiedFrom(m), ids)
+ }).unzip // TODO: Check for unapply with function pattern ?
+ (MatchExpr(c1, new_cases).copiedFrom(e), variables.fold(None)(merge))
+ case Operator(lhsrhs, builder) =>
+ // The exprBuilder adds variable definitions needed to compute the arguments.
+ val (exprBuilder, children, tmpIds, ids) = (((e: Expr) => e, ListBuffer[Expr](), ListBuffer[Identifier](), None: Option[Seq[Identifier]]) /: lhsrhs) {
+ case ((exprBuilder, children, tmpIds, ids), arg) =>
+ val (arg1, argv1) = markBranches(arg)
+ if(argv1.nonEmpty || isNewFunCall(arg1)) {
+ val arg_id = FreshIdentifier("arg", arg.getType)
+ val arg_b = FreshIdentifier("ba", BooleanType)
+ val f = (body: Expr) => letTuple(Seq(arg_id, arg_b), arg1, body).copiedFrom(body)
+ (exprBuilder andThen f, children += Variable(arg_id), tmpIds += arg_b, merge(ids, argv1))
+ } else {
+ (exprBuilder, children += arg, tmpIds, ids)
+ }
+ }
+ e match {
+ case FunctionInvocation(tfd@TypedFunDef(fd, targs), args) if fds(fd) =>
+ val new_fd = wrapFunDef(fd)
+ // Is different since functions will return a boolean as well.
+ tmpIds match {
+ case Seq() =>
+ val funCall = FunctionInvocation(TypedFunDef(new_fd, targs).copiedFrom(tfd), children).copiedFrom(e)
+ (exprBuilder(funCall), if(new_fd != fd) merge(Some(Seq()), ids) else ids)
+ case idvars =>
+ val res_id = FreshIdentifier("res", fd.returnType)
+ val res_b = FreshIdentifier("bb", BooleanType)
+ val finalIds = idvars :+ res_b
+ val finalExpr =
+ tupleWrap(Seq(Variable(res_id), or(finalIds.map(Variable(_)): _*))).copiedFrom(e)
+ val funCall = letTuple(Seq(res_id, res_b), FunctionInvocation(TypedFunDef(new_fd, targs), children).copiedFrom(e), finalExpr).copiedFrom(e)
+ (exprBuilder(funCall), merge(Some(Seq()), ids))
+ }
+ case _ =>
+ tmpIds match {
+ case Seq() =>
+ (e, ids)
+ case idvars =>
+ val finalExpr = tupleWrap(Seq(builder(children).copiedFrom(e), or(idvars.map(Variable): _*))).copiedFrom(e)
+ (exprBuilder(finalExpr), ids)
+ }
+ }
+ }
+
+ /** The cache of transforming functions.*/
+ private var cache = Map[FunDef, FunDef]()
+
+ /** Records all booleans serving to identify which part of the code should be executed.*/
+ private var booleanFlags = Seq[Identifier]()
+
+ /** Augment function definitions which should have boolean markers, leave others untouched. */
+ def wrapFunDef(fd: FunDef): FunDef = {
+ if(!(cache contains fd)) {
+ if(fds(fd)) {
+ val new_fd = fd.duplicate(returnType = TupleType(Seq(fd.returnType, BooleanType)))
+ new_fd.body = None
+ cache += fd -> new_fd
+ val (new_body, bvars) = wrapBranch(markBranches(fd.body.get)) // Recursive call.
+ new_fd.body = Some(new_body) // TODO: Handle post-condition if they exist.
+ booleanFlags ++= bvars.get
+ } else {
+ cache += fd -> fd
+ }
+ }
+ cache(fd)
+ }
+
+ /** Returns true if the expression is a function call with a new function already. */
+ def isNewFunCall(e: Expr): Boolean = e match {
+ case FunctionInvocation(TypedFunDef(fd, targs), args) =>
+ cache.values.exists { f => f == fd }
+ case _ => false
+ }
+
+ /** Returns a stream of covering inputs for the function `f`,
+ * such that if `f` is evaluated on each of these inputs, all parts of `{ f } U fds` will have been executed at least once.
+ *
+ * The number of expressions is the same as the number of arguments of `f` */
+ def result(): Stream[Seq[Expr]] = {
+ cache = Map()
+ booleanFlags = Seq()
+ /* Approximative algorithm Algorithm:
+ * In innermost branches, replace each result by (result, bi) where bi is a boolean described later.
+ * def f(x: Int, z: Boolean): (Int, Boolean) =
+ * x match {
+ * case 0 | 1 =>
+ * if(z) {
+ * ({val (r, b1) = if(z) (x, bt) else (-x, be)
+ * val (res, b) = f(r, z)
+ * (res, b || b1)
+ * case _ =>
+ * val (res, b) = if(z) (x, b2)
+ * else (f(x-1,!z)+f(x-2,!z), b3)
+ * (res*f(x-1,!z), b)
+ * }
+ * Let B be the set of bi.
+ * For each b in B
+ * Set all b' in B to false except b to true
+ * Find a counter-example.
+ * yield it in the stream.
+ */
+
+ /* Change all return types to accommodate the new covering boolean */
+
+ val (program, idMap, fdMap, cdMap) = DefOps.replaceFunDefs(p)({
+ (f: FunDef) =>
+ if((fds contains f) || f == fd) {
+ val new_fd = wrapFunDef(f)
+ if(f == fd) {
+ val h = FreshIdentifier("h", TupleType(Seq(fd.returnType, BooleanType)), false)
+ new_fd.postcondition = Some(Lambda(Seq(ValDef(h)), Not(TupleSelect(Variable(h), 2))))
+ }
+ Some(new_fd)
+ } else
+ None
+ }, {
+ (fi: FunctionInvocation, newFd: FunDef) => //if(cache contains fi.tfd.fd) {
+ Some(TupleSelect(FunctionInvocation(newFd.typed, fi.args), 1))
+ //} else None
+ })
+
+ val start_fd = fdMap.getOrElse(fd, fd)
+
+ var coveredBooleans = Set[Identifier]()
+ // For each boolean flag, set it to true, and find a counter-example which should reach this line.
+ // For each new counter-example, abstract evaluate the original function to remove booleans which have been reached.
+ val covering_examples =
+ for(bvar <- booleanFlags.toStream if !coveredBooleans(bvar)) yield {
+ val (program2, idMap2, fdMap2, cdMap2) = DefOps.replaceFunDefs(program)({
+ (f: FunDef) =>
+ if(ExprOps.exists(e => e match { case Variable(id) => booleanFlags contains id case _ => false })(f.fullBody)) {
+ val new_f = f.duplicate()
+ new_f.fullBody = ExprOps.preMap(e => {
+ e match {
+ case Variable(id) if id == bvar => Some(BooleanLiteral(true))
+ case Variable(id) if booleanFlags contains id => Some(BooleanLiteral(false))
+ case _ => None
+ }
+ })(f.fullBody)
+ Some(new_f)
+ } else None
+ })
+ val start_fd2 = fdMap2.getOrElse(start_fd, start_fd)
+ val tfactory = SolverFactory.getFromSettings(c, program2).withTimeout(5.seconds)
+
+ val vctx = new VerificationContext(c, program2, tfactory)
+ val vcs = VerificationPhase.generateVCs(vctx, Seq(start_fd2))
+ VerificationPhase.checkVCs(vctx, vcs).results(vcs(0)) match {
+ case Some(VCResult(VCStatus.Invalid(model), _, _)) =>
+ val finalExprs = fd.paramIds.map(model)
+ val whoIsEvaluated = functionInvocation(start_fd, finalExprs)
+ val ae = new AbstractEvaluator(c, p)
+ val coveredBooleansForCE = ae.eval(whoIsEvaluated).result match {
+ case Some((Tuple(Seq(_, booleans)), _)) =>
+ val targettedIds = ExprOps.collect(e => e match { case Variable(id) => Set(id) case _ => Set[Identifier]() })(booleans)
+ coveredBooleans ++= targettedIds
+ targettedIds
+ case _ =>
+ Set(bvar)
+ }
+ finalExprs -> coveredBooleansForCE
+ case _ => Seq() -> Set(bvar)
+ }
+ }
+
+ val covering_examples2 = if(minimizeExamples) {
+ // Remove examples whose coverage set is included in some other example.
+ for((covering_example, flags_met) <- covering_examples
+ if !covering_examples.exists{
+ case (other_example, other_flags) =>
+ other_example != covering_example &&
+ flags_met.subsetOf(other_flags)
+ }
+ ) yield covering_example
+ } else {
+ covering_examples.map(_._1)
+ }
+
+ covering_examples2 filter (_.nonEmpty)
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c1c29acbbe91243f68315a94e6ba60cedc11b3a2
--- /dev/null
+++ b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
@@ -0,0 +1,318 @@
+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
+import leon.purescala.Extractors._
+
+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
+ | }
+ | }
+ |
+ | sealed abstract class A
+ | case class B() extends A
+ | case class C(a: String, tail: A) extends A
+ | case class D(a: String, tail: A, b: String) extends A
+ |
+ | def withMatch(a: A): String = {
+ | a match {
+ | case B() => "B"
+ | case C(a, C(b, tail)) => b.toString + withMatch(tail) + a.toString
+ | case C(a, tail) => withMatch(tail) + a.toString
+ | case D(a, tail, b) => a + withMatch(tail) + b
+ | }
+ | }
+ |
+ | 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, Some(Seq(p.id, q.id)))) should equal ((simpleExpr, Some(Seq(p.id, q.id))))
+ coverage.wrapBranch((simpleExpr, None)) match {
+ case (covered, Some(ids)) =>
+ ids should have size 1
+ covered should equal (Tuple(Seq(simpleExpr, Variable(ids.head))))
+ case _ =>
+ fail("No ids added")
+ }
+ }
+
+ 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
+
+ coverage.markBranches(expr) match {
+ case (res, Some(ids)) =>
+ 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")
+ }
+ case _ =>
+ fail("No ids added")
+ }
+ }
+
+ 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
+
+ coverage.markBranches(expr) match {
+ case (res, None) => fail("No ids added")
+ case (res, Some(ids)) =>
+ 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("Match coverage should work with recursive functions") { ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withMatch = funDef("InputCoverageSuite.withMatch")
+ val coverage = new InputCoverage(withMatch, Set(withMatch))
+ val expr = withMatch.body.get
+
+ coverage.markBranches(expr) match {
+ case (res, None) => fail("No ids added")
+ case (res, Some(ids)) =>
+ withClue(res.toString) {
+ ids should have size 4
+ res match {
+ case MatchExpr(scrut,
+ Seq(
+ MatchCase(CaseClassPattern(_, _, Seq()), None, rhs1),
+ MatchCase(CaseClassPattern(_, _, _), None, rhs2),
+ MatchCase(CaseClassPattern(_, _, _), None, rhs3),
+ MatchCase(CaseClassPattern(_, _, _), None, rhs4))
+ ) =>
+ rhs1 match {
+ case Tuple(Seq(_, Variable(b))) => b shouldEqual ids(0)
+ case _ => fail(s"$rhs1 should be a Tuple")
+ }
+ rhs2 match {
+ case LetTuple(_, _, Tuple(Seq(_, Or(Seq(_, Variable(b)))))) => b shouldEqual ids(1)
+ case _ => fail(s"$rhs2 should be a val + tuple like val ... = ... ; (..., ... || ${ids(1)})")
+ }
+
+ case _ => fail(s"$res does not have the format a match { case B() => .... x 4 }")
+ }
+ }
+ }
+ }
+
+ 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
+
+ coverage.markBranches(expr) match {
+ case (res, Some(ids)) if ids.size > 0 =>
+ withClue(res.toString) {
+ fail(s"Should have not added any ids, but got $ids")
+ }
+ case (res, _) =>
+ 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.uniqueName shouldEqual a2.uniqueName
+ ida2.uniqueName shouldEqual a1.uniqueName
+ 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
+
+ coverage.markBranches(expr) match {
+ case (res, None) => fail("No ids added")
+ case (res, Some(ids)) =>
+ 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) } }")
+ }
+ }
+ }
+
+ test("input coverage for booleans should find all of them") { ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withIf = funDef("InputCoverageSuite.withIf")
+ val coverage = new InputCoverage(withIf, Set(withIf))
+ coverage.result().toSet should equal (Set(Seq(b(true)), Seq(b(false))))
+ }
+
+ test("input coverage for ADT should find all of them") { ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withMatch = funDef("InputCoverageSuite.withMatch")
+ val coverage = new InputCoverage(withMatch, Set(withMatch))
+ coverage.minimizeExamples = false
+ val res = coverage.result().toSet
+ res should have size 4
+
+ coverage.minimizeExamples = true
+ val res2 = coverage.result().toSet
+ res2 should have size 3
+ }
+
+ test("input coverage for combined functions should find all of them") { 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 res = coverage.result().toSet.toSeq
+ if(res.size == 1) {
+ val Seq(IntLiteral(a)) = res(0)
+ withClue(s"a=$a") {
+ assert(a + 5 > 0 || a - 5 > 0, "At least one of the two examples should cover the positive case")
+ assert(a + 5 <= 0 || a - 5 <= 0, "At least one of the two examples should cover the negative case")
+ }
+ } else {
+ res should have size 2
+ val Seq(IntLiteral(a)) = res(0)
+ val Seq(IntLiteral(b)) = res(1)
+ withClue(s"a=$a, b=$b") {
+ assert(a + 5 > 0 || b + 5 > 0 || a - 5 > 0 || b - 5 > 0 , "At least one of the two examples should cover the positive case")
+ assert(a + 5 <= 0 || b + 5 <= 0 || a - 5 <= 0 || b - 5 <= 0 , "At least one of the two examples should cover the negative case")
+ }
+ }
+ }
+
+ test("input coverage for composed functions should find all of them") { ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withCoveredFun3 = funDef("InputCoverageSuite.withCoveredFun3")
+ val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
+ val coverage = new InputCoverage(withCoveredFun3, Set(withCoveredFun3, withCoveredFun2))
+ val res = coverage.result().toSet.toSeq
+ def withCoveredFun2Impl(i: Int) = if(i > 0) 2 else 0
+ if(res.size == 1) {
+ val Seq(IntLiteral(a)) = res(0)
+ withClue(s"a=$a") {
+ assert(a + 5 > 0 || withCoveredFun2Impl(a + 5) > 0, "At least one of the two examples should cover the positive case")
+ assert(a + 5 <= 0 || withCoveredFun2Impl(a + 5) <= 0, "At least one of the two examples should cover the negative case")
+ }
+ } else {
+ res should have size 2
+ val Seq(IntLiteral(a)) = res(0)
+ val Seq(IntLiteral(b)) = res(1)
+ withClue(s"a=$a, b=$b") {
+ assert(a + 5 > 0 || withCoveredFun2Impl(a + 5) > 0 || b + 5 > 0 || withCoveredFun2Impl(b + 5) > 0, "At least one of the two examples should cover the positive case")
+ assert(a + 5 <= 0 || withCoveredFun2Impl(a + 5) <= 0 || b + 5 <= 0 || withCoveredFun2Impl(b + 5) <= 0, "At least one of the two examples should cover the negative case")
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 63469ead59c6c4441ce12a92fc92c4349ae99d5b..91b77284cc16518a4b86e0bdcb5ad7e98230061f 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/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 =>
}