From aa874f7b9e31206142fd12bd22c94e8fa5933968 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 6 Jan 2016 16:11:46 +0100
Subject: [PATCH] Added input coverage.
---
src/main/scala/leon/purescala/DefOps.scala | 27 ++---
.../disambiguation/InputCoverage.scala | 99 +++++++++++++++++++
2 files changed, 113 insertions(+), 13 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 6b7bf67e0..5b70c2a35 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])
@@ -356,8 +356,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 +607,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 +663,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/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
new file mode 100644
index 000000000..c72416a93
--- /dev/null
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -0,0 +1,99 @@
+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
+import purescala.Definitions.{FunDef, Program}
+import purescala.DefOps
+import grammars.ValueGrammar
+import bonsai.enumerators.MemoizedEnumerator
+import solvers.Model
+import solvers.ModelBuilder
+import scala.collection.mutable.ListBuffer
+
+import leon.LeonContext
+
+/**
+ * @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) {
+ var numToCoverForEachExample: Int = 1
+
+ /** The number of expressions is the same as the number of arguments. */
+ def result(): Stream[Seq[Expr]] = {
+ /* Algorithm:
+ * 1) Consider only match/case and if/else statements.
+ * def f(x: Int, z: Boolean): Int =
+ * x match {
+ * case 0 | 1 => 1
+ * case _ =>
+ * if(z) x*f(x-1,!z)
+ * else f(x-1,!z)+f(x-2,!z)
+ * }
+ * 2) 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 => (1, b1)
+ * case _ =>
+ * if(z) (x*f(x-1,!z), b2)
+ * else (f(x-1,!z)+f(x-2,!z), b3)
+ * }
+ * 3) If the function is recursive, recover the previous values and left-OR them with the returning bi.
+ * def f(x: Int, z: Boolean): (Int, Boolean) =
+ * x match {
+ * case 0 | 1 => (1, b1)
+ * case _ =>
+ * if(z) {
+ * val (r, bf) = f(x-1,!z)
+ * (x*r, b2 || bf)}
+ * else {
+ * val (r, bf) = f(x-1,!z)
+ * val (r2, bf2) = f(x-2,!z)
+ * (r+r2, b3 || bf || bf2)
+ * }
+ * }
+ * 4) Add the post-condition
+ * ensuring { res => !res._2 }
+ * 5) 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 changeReturnTypes = { (p: Program) =>
+ val (program, idMap, fdMap, cdMap) = DefOps.replaceFunDefs(p)({
+ (f: FunDef) =>
+ if((fds contains f) || f == fd) {
+ Some(f.duplicate(returnType = TupleType(Seq(f.returnType, BooleanType))))
+ } else
+ None
+ }, {
+ (fi: FunctionInvocation, newFd: FunDef) =>
+ Some(TupleSelect(FunctionInvocation(newFd.typed, fi.args), 1))
+ })
+ (program, fdMap(fd), fds.map(fdMap))
+ }
+ val addNewReturnVariables = { (p: Program, fd: FunDef, fds: Set[FunDef]) =>
+
+ }
+
+ (changeReturnTypes andThen
+ addNewReturnVariables.tupled)(p)
+
+
+ ???
+ }
+}
\ No newline at end of file
--
GitLab