From e40e99cdf38b2b6a73efdf5c7484fd7d042f91ff Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 29 Aug 2013 18:43:03 +0200
Subject: [PATCH] Add synthesis regression test suite
For now only synthesis tests that 100% pass. The rest of benchmarks need
to be investigated due to memory consumption issues
---
.../scala/leon/synthesis/BoundedSearch.scala | 24 +++++
.../leon/synthesis/SynthesisOptions.scala | 1 +
.../scala/leon/synthesis/Synthesizer.scala | 8 +-
.../regression/synthesis/Church/Add.scala | 24 +++++
.../synthesis/Church/Distinct.scala | 37 +++++++
.../regression/synthesis/Church/Mult.scala | 37 +++++++
.../regression/synthesis/Church/Squared.scala | 44 +++++++++
.../regression/synthesis/List/Delete.scala | 40 ++++++++
.../regression/synthesis/List/Diff.scala | 58 +++++++++++
.../regression/synthesis/List/Insert.scala | 27 +++++
.../regression/synthesis/List/Split.scala | 98 +++++++++++++++++++
.../regression/synthesis/List/Union.scala | 49 ++++++++++
.../synthesis/SynthesisRegressionSuite.scala | 73 ++++++++++++++
.../leon/test/synthesis/SynthesisSuite.scala | 15 ---
14 files changed, 519 insertions(+), 16 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/BoundedSearch.scala
create mode 100644 src/test/resources/regression/synthesis/Church/Add.scala
create mode 100644 src/test/resources/regression/synthesis/Church/Distinct.scala
create mode 100644 src/test/resources/regression/synthesis/Church/Mult.scala
create mode 100644 src/test/resources/regression/synthesis/Church/Squared.scala
create mode 100644 src/test/resources/regression/synthesis/List/Delete.scala
create mode 100644 src/test/resources/regression/synthesis/List/Diff.scala
create mode 100644 src/test/resources/regression/synthesis/List/Insert.scala
create mode 100644 src/test/resources/regression/synthesis/List/Split.scala
create mode 100644 src/test/resources/regression/synthesis/List/Union.scala
create mode 100644 src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
diff --git a/src/main/scala/leon/synthesis/BoundedSearch.scala b/src/main/scala/leon/synthesis/BoundedSearch.scala
new file mode 100644
index 000000000..5f7785225
--- /dev/null
+++ b/src/main/scala/leon/synthesis/BoundedSearch.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+class BoundedSearch(synth: Synthesizer,
+ problem: Problem,
+ rules: Seq[Rule],
+ costModel: CostModel,
+ searchBound: Int) extends SimpleSearch(synth, problem, rules, costModel) {
+
+ def this(synth: Synthesizer, problem: Problem, searchBound: Int) = {
+ this(synth, problem, synth.rules, synth.options.costModel, searchBound)
+ }
+
+ override def searchStep() {
+ val (closed, total) = g.getStatus
+ if (total > searchBound) {
+ stop()
+ } else {
+ super.searchStep()
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
index c776ab044..9f867cabd 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -13,6 +13,7 @@ case class SynthesisOptions(
costModel: CostModel = CostModel.default,
rules: Seq[Rule] = Rules.all ++ Heuristics.all,
manualSearch: Boolean = false,
+ searchBound: Option[Int] = None,
// Cegis related options
cegisUseUninterpretedProbe: Boolean = false,
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a0232558e..a0d1e19a7 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -46,7 +46,13 @@ class Synthesizer(val context : LeonContext,
} else if (options.searchWorkers > 1) {
new ParallelSearch(this, problem, options.searchWorkers)
} else {
- new SimpleSearch(this, problem)
+ options.searchBound match {
+ case Some(b) =>
+ new BoundedSearch(this, problem, b)
+
+ case None =>
+ new SimpleSearch(this, problem)
+ }
}
val sigINT = new Signal("INT")
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
new file mode 100644
index 000000000..7b1b6b95f
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -0,0 +1,24 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ // def add(x : Num, y : Num) : Num = (x match {
+ // case Z => y
+ // case S(p) => add(p, S(y))
+ // }) ensuring (value(_) == value(x) + value(y))
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
new file mode 100644
index 000000000..a7a0189c2
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -0,0 +1,37 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x : Num, y : Num) : Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
new file mode 100644
index 000000000..42519e663
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -0,0 +1,37 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x : Num, y : Num) : Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def mult(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(y)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
new file mode 100644
index 000000000..096f212a6
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -0,0 +1,44 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x : Num, y : Num) : Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def mult(x: Num, y: Num): Num = (y match {
+ case S(p) =>
+ add(mult(x, p), x)
+ case Z =>
+ Z
+ }) ensuring { value(_) == value(x) * value(y) }
+
+ def squared(x: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(x)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
new file mode 100644
index 000000000..9fdef981b
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -0,0 +1,40 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def delete(in1: List, v: Int): List = {
+ // in1 match {
+ // case Cons(h,t) =>
+ // if (h == v) {
+ // delete(t, v)
+ // } else {
+ // Cons(h, delete(t, v))
+ // }
+ // case Nil =>
+ // Nil
+ // }
+ //} ensuring { content(_) == content(in1) -- Set(v) }
+
+ def delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- Set(v)
+ }
+}
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
new file mode 100644
index 000000000..3e7121eb1
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -0,0 +1,58 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Diff {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def delete(in1: List, v: Int): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ def union(in1: List, in2: List): List = {
+ in1 match {
+ case Cons(h, t) =>
+ Cons(h, union(t, in2))
+ case Nil =>
+ in2
+ }
+ } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ // def diff(in1: List, in2: List): List = {
+ // in2 match {
+ // case Nil =>
+ // in1
+ // case Cons(h, t) =>
+ // diff(delete(in1, h), t)
+ // }
+ // } ensuring { content(_) == content(in1) -- content(in2) }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+}
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
new file mode 100644
index 000000000..e5b21b45d
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -0,0 +1,27 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Insert {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ //def insert(in1: List, v: Int): List = {
+ // Cons(v, in1)
+ //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+}
diff --git a/src/test/resources/regression/synthesis/List/Split.scala b/src/test/resources/regression/synthesis/List/Split.scala
new file mode 100644
index 000000000..5aa4a8f1f
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split.scala
@@ -0,0 +1,98 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def insert(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ Set(v)
+ //}
+
+ def delete(in1: List, v: Int): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ //def delete(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- Set(v)
+ //}
+
+ def union(in1: List, in2: List): List = {
+ in1 match {
+ case Cons(h, t) =>
+ Cons(h, union(t, in2))
+ case Nil =>
+ in2
+ }
+ } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ //def union(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ content(in2)
+ //}
+
+ def diff(in1: List, in2: List): List = {
+ in2 match {
+ case Nil =>
+ in1
+ case Cons(h, t) =>
+ diff(delete(in1, h), t)
+ }
+ } ensuring { content(_) == content(in1) -- content(in2) }
+
+ //def diff(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- content(in2)
+ //}
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ // def split(list : List) : (List,List) = (list match {
+ // case Nil => (Nil, Nil)
+ // case Cons(x, Nil) => (Cons(x, Nil), Nil)
+ // case Cons(x1, Cons(x2, xs)) =>
+ // val (s1,s2) = split(xs)
+ // (Cons(x1, s1), Cons(x2, s2))
+ // }) ensuring(res => splitSpec(list, res))
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
new file mode 100644
index 000000000..adcc943fd
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -0,0 +1,49 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Union {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def delete(in1: List, v: Int): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ // def union(in1: List, in2: List): List = {
+ // in1 match {
+ // case Cons(h, t) =>
+ // Cons(h, union(t, in2))
+ // case Nil =>
+ // in2
+ // }
+ // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
new file mode 100644
index 000000000..eda49bbcf
--- /dev/null
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -0,0 +1,73 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package test
+package synthesis
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.solvers.z3._
+import leon.solvers.Solver
+import leon.synthesis._
+import leon.synthesis.utils._
+
+import java.io.File
+
+import TestUtils._
+
+class SynthesisRegressionSuite extends LeonTestSuite {
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"))
+
+ for(f <- fs) {
+ block(f)
+ }
+ }
+
+ private def testSynthesis(cat: String, f: File, bound: Int) {
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = true,
+ xlang = false,
+ verify = false
+ ),
+ files = List(f),
+ reporter = new TestSilentReporter
+ )
+
+ val opts = SynthesisOptions(searchBound = Some(bound))
+
+ val pipeline = plugin.ExtractionPhase andThen SubtypingPhase
+
+ val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
+
+ var chooses = ChooseInfo.extractFromProgram(ctx, program, opts)
+
+ for (ci <- chooses) {
+ test(cat+": "+f.getName()+" - "+ci.fd.id.name) {
+ val (sol, isComplete) = ci.synthesizer.synthesize()
+ if (!isComplete) {
+ fail("Solution was not found. (Search bound: "+bound+")")
+ }
+ }
+ }
+ }
+
+ forEachFileIn("regression/synthesis/Church/") { f =>
+ testSynthesis("Church", f, 200)
+ }
+
+ forEachFileIn("regression/synthesis/List/") { f =>
+ testSynthesis("List", f, 200)
+ }
+
+ forEachFileIn("regression/synthesis/SortedList/") { f =>
+ testSynthesis("SortedList", f, 400)
+ }
+
+ forEachFileIn("regression/synthesis/StrictSortedList/") { f =>
+ testSynthesis("StrictSortedList", f, 400)
+ }
+}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index d134c980e..574efa3fe 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -136,20 +136,6 @@ class SynthesisSuite extends LeonTestSuite {
}
}
-
- def assertFastEnough(sctx: SynthesisContext, rr: Traversable[RuleInstantiation], timeoutMs: Long) {
- for (alt <- rr) {
- val ts = System.currentTimeMillis
-
- val res = alt.apply(sctx)
-
- val t = System.currentTimeMillis - ts
-
- t should be <= timeoutMs
- }
- }
-
-
forProgram("Cegis 1")(
"""
import scala.collection.immutable.Set
@@ -173,7 +159,6 @@ object Injection {
) {
case (sctx, fd, p) =>
assertAllAlternativesSucceed(sctx, rules.CEGIS.instantiateOn(sctx, p))
- assertFastEnough(sctx, rules.CEGIS.instantiateOn(sctx, p), 100)
}
forProgram("Cegis 2")(
--
GitLab