Semester project: corpus based synthesis

src/main/scala/leon/Main.scala

@@ -30,7 +30,8 @@ object Main {
       invariant.engine.InferInvariantsPhase,
       laziness.LazinessEliminationPhase,
       genc.GenerateCPhase,
-      genc.CFileOutputPhase
+      genc.CFileOutputPhase,
+      comparison.ComparisonPhase
     )
   }
 
@@ -59,9 +60,11 @@ object Main {
     val optInferInv    = LeonFlagOptionDef("inferInv",    "Infer invariants from (instrumented) the code",             false)
     val optLazyEval    = LeonFlagOptionDef("lazy",        "Handles programs that may use the 'lazy' construct",        false)
     val optGenc        = LeonFlagOptionDef("genc",        "Generate C code",                                           false)
+    val optComparison  = LeonFlagOptionDef("compare", "Compare the targeted program to the Leon exemple suit", false)
+
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
-      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc)
+      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc, optComparison)
   }
 
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
@@ -177,6 +180,8 @@ object Main {
     val instrumentF = ctx.findOptionOrDefault(optInstrument)
     val lazyevalF = ctx.findOptionOrDefault(optLazyEval)
     val analysisF = verifyF && terminationF
+    val comparisonF = ctx.findOptionOrDefault(optComparison)
+
     // Check consistency in options
 
     if (helpF) {
@@ -206,6 +211,7 @@ object Main {
         else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
         else if (gencF) GenerateCPhase andThen CFileOutputPhase
         else if (lazyevalF) LazinessEliminationPhase
+        else if (comparisonF) comparison.ComparisonPhase andThen PrintReportPhase
         else verification
       }
 
@@ -217,6 +223,7 @@ object Main {
   private var hasFatal = false
 
   def main(args: Array[String]) {
+
     val argsl = args.toList
 
     // Process options

src/main/scala/leon/comparison/Comparator.scala

@@ -0,0 +1,12 @@
+package leon.comparison
+
+import leon.purescala.Expressions.Expr
+
+/**
+  * Created by joachimmuth on 04.05.16.
+  */
+trait Comparator {
+  val name: String
+  def compare(expr_base: Expr, expr: Expr): (Double, String)
+
+}

src/main/scala/leon/comparison/ComparatorClassList.scala

@@ -0,0 +1,63 @@
+package leon.comparison
+
+import leon.comparison.Utils._
+import leon.purescala.Expressions._
+
+/**
+  * Created by joachimmuth on 02.05.16.
+  *
+  * This method shares similarities with the ComparatorByList.
+  * We keep the idea of comparing a list of expressions (disregarding their order), but now, instead of comparing
+  * two expressions (i.e. tree) we will extract the type of each expression.
+  *
+  * x match {
+  *   case 1 => 'a'
+  *   case 2 => 'b'
+  * }
+  *
+  * ComparatorByList -> {complete match, leaf(a), leaf(b)}
+  * ComparatorByListType -> {node(match), leaf(a), leaf(b)}
+  *
+  * x match {
+  *   case 1 => 'a'
+  *   case 2 => 'c'
+  * }
+  *
+  * ComparatorByList -> similarity 33%
+  * ComparatorByListType -> similarity 66%
+  */
+object ComparatorClassList extends Comparator {
+  val name = "ClassList"
+
+  def compare(expr_corpus: Expr, expr: Expr) = {
+    val listClassesA = collectClass(expr_corpus)
+    val listClassesB = collectClass(expr)
+
+    val similarExpr: Int = pairsOfSimilarExp(listClassesA, listClassesB)
+
+    val score = Utils.matchScore(similarExpr, listClassesA.size, listClassesB.size)
+
+    if (score > 0.0 && ComparisonPhase.debug){
+      println("-----------")
+      println("COMPARATOR " + name)
+      println("Expressions: ", expr, expr_corpus)
+      println("List of classes: ", listClassesB, listClassesA)
+      println("-----------")
+    }
+
+    (score, "")
+  }
+
+
+  def pairsOfSimilarExp(listExpr_corpus: List[Class[_ <: Expr]], listExpr: List[Class[_ <: Expr]]): Int = {
+    def helper(listExpr_corpus: List[Class[_ <: Expr]], listExpr: List[Class[_ <: Expr]], acc: Int): Int =
+      listExpr match {
+        case Nil => acc
+        case x::xs if listExpr_corpus.contains(x) => helper(listExpr_corpus diff List(x), xs, acc + 1)
+        case x::xs => helper(listExpr_corpus, xs, acc)
+      }
+
+    helper(listExpr_corpus, listExpr, 0)
+  }
+
+}

src/main/scala/leon/comparison/ComparatorClassTree.scala

@@ -0,0 +1,180 @@
+package leon.comparison
+
+import leon.comparison.Utils._
+import leon.purescala.Expressions._
+
+
+/**
+  * Created by joachimmuth on 12.05.16.
+  *
+  * Go through both trees in parallel and compare each expression based on its class. Try to find the biggest
+  * common tree.
+  *
+  * Procedure:
+  *   - Find all possible pair of roots. Then consider all children of both roots, and check which are
+  *   similar.
+  *   - Consider all possible combinations of children and repeat the same operation on them.
+  *   - Pick the biggest tree in the list of all possible similar tree
+  *   - Remove the tree overlapping the one chosen, and search if it exists an other common tree. Repeat.
+  *   - End with all common and exclusive common tree shared by trees A and B
+  *
+  * The MatchScore is calculated with the size of the common tree, compared with the sizes of trees A and B.
+  */
+object ComparatorClassTree extends Comparator{
+  val name: String = "ClassTree"
+
+
+  def compare(expr_corpus: Expr, expr: Expr) = {
+    val roots = possibleRoots(expr_corpus, expr)
+
+    val trees = roots.flatMap(possibleTrees(_))
+    val exclusives = exclusivesTrees(trees)
+    val sum = exclusives.foldLeft(0)( (acc, tree) => acc + tree.size)
+
+    val listClassesA = collectClass(expr_corpus)
+    val listClassesB = collectClass(expr)
+
+    val score = matchScore(sum, listClassesA.size, listClassesB.size)
+
+    if (score > 0.0 && ComparisonPhase.debug){
+      println("---------------------")
+      println("COMPARATOR " + name)
+      println("Expressions: ", expr_corpus, expr)
+      println("Common Tree: ", exclusives)
+      println("---------------------")
+    }
+
+    (score, "")
+  }
+
+  /**
+    * Extract all non-overlapping trees, in size order
+    * @param trees
+    * @return
+    */
+  def exclusivesTrees(trees: List[myTree[(Expr, Expr)]]): List[myTree[(Expr, Expr)]] = trees match {
+    case Nil => Nil
+    case x :: xs =>
+      val biggest = trees.sortBy(-_.size).head
+      val rest = trees.filter(tree => flatList(tree).intersect( flatList(biggest) ).isEmpty)
+      List(biggest) ++ exclusivesTrees(rest)
+  }
+
+  def flatList(tree: myTree[(Expr, Expr)]): List[Expr] = tree.toList.flatMap(p => List(p._1, p._2))
+
+  /**
+    * list of all similar pair of expressions, based on classes.
+    *
+    * @param expr_corpus
+    * @param expr
+    * @return
+    */
+  def possibleRoots(expr_corpus: Expr, expr: Expr): List[(Expr, Expr)] = {
+    val expressionsA = collectExpr(expr_corpus)
+    val expressionsB = collectExpr(expr)
+
+    val pairOfPossibleRoots = for {
+      exprA <- expressionsA
+      exprB <- expressionsB
+      if areSimilar(exprA.getClass, exprB.getClass)
+    } yield {
+      (exprA, exprB)
+    }
+
+    pairOfPossibleRoots
+  }
+
+
+  /**
+    * With a pair of roots, find all children and find all combination of matching children in order to create a list
+    * of all possible matching tree. Then recursively call itself on each pair of children.
+ *
+    * @param pair of matching root
+    * @return ether a Leaf or a List of all possible similar trees starting with this pair of roots
+    */
+  def possibleTrees(pair: (Expr, Expr)): List[myTree[(Expr, Expr)]] = {
+    val exprA = pair._1
+    val exprB = pair._2
+    val childrenA = getChildren(exprA)
+    val childrenB = getChildren(exprB)
+
+
+    val pairOfMatchingChildren = findPairOfMatchingChildren(childrenA, childrenB)
+    val combinationOfChildren = combineChildren(pairOfMatchingChildren)
+
+
+    if(pairOfMatchingChildren.isEmpty) {
+      List(myTree(pair, List()))
+    } else {
+      combinationOfChildren.foldLeft(List(): List[myTree[(Expr, Expr)]])(
+        (listOfTree, children) => listOfTree ++ treesWithChildCombination(pair, children.map(p => possibleTrees(p)))
+      )
+    }
+  }
+
+  def findPairOfMatchingChildren(childrenA: List[Expr], childrenB: List[Expr]): List[(Expr, Expr)] = {
+    for{
+      childA <- childrenA
+      childB <- childrenB
+      if areSimilar(childA.getClass, childB.getClass)
+    } yield {
+      (childA, childB)
+    }
+  }
+
+  /** All possible combination of pairs of children, given the condition that one child can only be used once.
+    *
+    * IMPROVEMENT: Here, it would be possible to already filter some cases.
+    * When we do the combination, we try all cases, using one pair of matching, two, three, ... we could only keep the
+    * ones using maximum of possible children, as we only want the biggest tree.
+    *
+    * @param pairs
+    * @return
+    */
+  def combineChildren(pairs: List[(Expr, Expr)]): List[List[(Expr, Expr)]] = {
+    combine(pairs).filterNot(p => isSameChildUsedTwice(p)).toList
+  }
+
+  def isSameChildUsedTwice(list: List[(Expr, Expr)]): Boolean = {
+    list.map(_._1).distinct.size != list.size ||
+    list.map(_._2).distinct.size != list.size
+  }
+
+  def combine(in: List[(Expr, Expr)]): Seq[List[(Expr, Expr)]] = {
+    for {
+      len <- 1 to in.length
+      combinations <- in combinations len
+    } yield combinations
+  }
+
+  /**
+    * As we recursively call the method, children will create list of possibilities, as the root does. All this possible
+    * combination need to be transformed into a list of complete tree.
+    *
+    * Technically, we have a combination of Children that return each a list of possible trees. So the upper-level tree
+    * (whom root is named pair) can have all possible combination of theses lists as children.
+    *
+    * @param pair
+    * @param listChildren
+    * @return
+    */
+  def treesWithChildCombination(pair: (Expr, Expr), listChildren: List[List[myTree[(Expr, Expr)]]]): List[myTree[(Expr, Expr)]] = {
+    def combine(list: List[List[myTree[(Expr, Expr)]]]): List[List[myTree[(Expr, Expr)]]] = list match {
+      case Nil => List(Nil)
+      case x :: xs =>
+        for {
+          j <- combine(xs)
+          i <- x
+        } yield i :: j
+    }
+
+    combine(listChildren).map(children => myTree(pair, children))
+  }
+
+
+
+  def areSimilar(getClass: Class[_ <: Expr], getClass1: Class[_ <: Expr]) = {
+    getClass == getClass1
+  }
+
+}