From a74f22ea4939b3c9c86032816504b0e3e3f08d08 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 18 Nov 2015 15:52:03 +0100
Subject: [PATCH] Try to use StreamEvaluator for repair
---
.../leon/evaluators/AngelicEvaluator.scala | 22 +++-
.../leon/evaluators/StreamEvaluator.scala | 8 +-
src/main/scala/leon/purescala/ExprOps.scala | 37 +++++-
.../scala/leon/repair/RepairNDEvaluator.scala | 76 ++----------
src/main/scala/leon/repair/rules/Focus.scala | 9 +-
src/main/scala/leon/utils/StreamUtils.scala | 24 ++--
.../resources/regression/repair/Heap3.scala | 113 ++++++++++++++++++
.../evaluators/EvaluatorSuite.scala | 2 +-
.../leon/regression/repair/RepairSuite.scala | 6 +-
.../leon/unit/evaluators/EvaluatorSuite.scala | 2 +-
10 files changed, 205 insertions(+), 94 deletions(-)
create mode 100644 src/test/resources/regression/repair/Heap3.scala
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index c1374b54f..090eeff0f 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -4,12 +4,11 @@ package leon
package evaluators
import leon.solvers.Model
-import purescala.Definitions.Program
import purescala.Expressions.Expr
import EvaluationResults._
-class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
- extends Evaluator(ctx, prog)
+class AngelicEvaluator(underlying: NDEvaluator)
+ extends Evaluator(underlying.context, underlying.program)
with DeterministicEvaluator
{
val description: String = "angelic evaluator"
@@ -24,3 +23,20 @@ class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
other.asInstanceOf[Result[Nothing]]
}
}
+
+class DemonicEvaluator(underlying: NDEvaluator)
+ extends Evaluator(underlying.context, underlying.program)
+ with DeterministicEvaluator
+{
+ val description: String = "demonic evaluator"
+ val name: String = "Interpreter that demands an underlying non-deterministic program has unique solution"
+
+ def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
+ case Successful(Stream(h)) =>
+ Successful(h)
+ case Successful(_) =>
+ RuntimeError("Underlying ND-evaluator did not return unique solution!")
+ case other@(RuntimeError(_) | EvaluatorError(_)) =>
+ other.asInstanceOf[Result[Nothing]]
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 5b387368b..72a4dd243 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -13,7 +13,7 @@ import purescala.Definitions.{TypedFunDef, Program}
import purescala.Expressions._
import leon.solvers.SolverFactory
-import leon.utils.StreamUtils.cartesianProduct
+import leon.utils.StreamUtils._
class StreamEvaluator(ctx: LeonContext, prog: Program)
extends ContextualEvaluator(ctx, prog, 50000)
@@ -75,8 +75,10 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Stream()
case NDValue(tp) =>
- import grammars.ValueGrammar
- ValueGrammar.getProductions(tp).toStream.map{ g => g.builder(Seq())}
+ // FIXME: This is the only source of infinite values, and will in a way break
+ // the evaluator: the evaluator is not designed to fairly handle infinite streams.
+ // Of course currently it is only used for boolean type, which is finite :)
+ valuesOf(tp)
case IfExpr(cond, thenn, elze) =>
e(cond).distinct.flatMap {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 5c86318e4..1736e2f43 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1139,12 +1139,47 @@ object ExprOps {
GenericValue(tp, 0)
case FunctionType(from, to) =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true)))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, alwaysShowUniqueID = true)))
Lambda(args, simplestValue(to))
case _ => throw LeonFatalError("I can't choose simplest value for type " + tpe)
}
+ def valuesOf(tp: TypeTree): Stream[Expr] = {
+ import utils.StreamUtils._
+ tp match {
+ case BooleanType =>
+ Stream(BooleanLiteral(false), BooleanLiteral(true))
+ case Int32Type =>
+ Stream.iterate(0) { prev =>
+ if (prev > 0) -prev else -prev + 1
+ } map IntLiteral
+ case IntegerType =>
+ Stream.iterate(BigInt(0)) { prev =>
+ if (prev > 0) -prev else -prev + 1
+ } map InfiniteIntegerLiteral
+ case UnitType =>
+ Stream(UnitLiteral())
+ case tp: TypeParameter =>
+ Stream.from(0) map (GenericValue(tp, _))
+ case TupleType(stps) =>
+ cartesianProduct(stps map (tp => valuesOf(tp))) map Tuple
+ case SetType(base) =>
+ def elems = valuesOf(base)
+ elems.scanLeft(Stream(FiniteSet(Set(), base): Expr)){ (prev, curr) =>
+ prev flatMap {
+ case fs@FiniteSet(elems, tp) =>
+ Stream(fs, FiniteSet(elems + curr, tp))
+ }
+ }.flatten // FIXME Need cp οr is this fine?
+ case cct: CaseClassType =>
+ cartesianProduct(cct.fieldsTypes map valuesOf) map (CaseClass(cct, _))
+ case act: AbstractClassType =>
+ interleave(act.knownCCDescendants.map(cct => valuesOf(cct)))
+ }
+ }
+
+
/** Hoists all IfExpr at top level.
*
* Guarantees that all IfExpr will be at the top level and as soon as you
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index e9d63b1b9..bd0c50fce 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -5,77 +5,17 @@ package leon.repair
import leon.purescala._
import Definitions._
import Expressions._
-import Types._
-import ExprOps.postMap
-import Constructors.not
import leon.LeonContext
-import leon.evaluators.DefaultEvaluator
-import scala.util.Try
+import leon.evaluators.StreamEvaluator
-// This evaluator treats the condition cond non-deterministically in the following sense:
-// If a function invocation fails or violates a postcondition for cond,
-// it backtracks and gets executed again for !cond
-class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr) extends DefaultEvaluator(ctx, prog) {
+/** This evaluator treats the expression [[expr]] (reference equality) as a non-deterministic value */
+class RepairNDEvaluator(ctx: LeonContext, prog: Program, expr: Expr) extends StreamEvaluator(ctx, prog) {
- override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
-
- case FunctionInvocation(tfd, args) if tfd.fd == fd =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgs = args.map(a => e(a))
-
- // build a mapping for the function...
- val frame = rctx.newVars(tfd.paramSubst(evArgs))
-
- if(tfd.hasPrecondition) {
- e(tfd.precondition.get)(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) =>
- throw RuntimeError("Precondition violation for " + tfd.id.name + " reached in evaluation.: " + tfd.precondition.get)
- case other =>
- throw RuntimeError(typeErrorMsg(other, BooleanType))
- }
- }
-
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation.")
- }
-
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
-
- def treat(subst : Expr => Expr) = {
- val callResult = e(subst(body))(frame, gctx)
-
- tfd.postcondition match {
- case Some(post) =>
- e(subst(Application(post, Seq(callResult))))(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + tfd.id.name + " reached in evaluation.")
- case other => throw EvalError(typeErrorMsg(other, BooleanType))
- }
- case None =>
- }
-
- callResult
- }
-
- Try {
- treat(e => e)
- }.getOrElse {
- treat( postMap {
- // Use reference equality, just in case cond appears again in the program
- case c if c eq cond => Some(not(cond))
- case _ => None
- })
- }
-
- case _ => super.e(expr)
+ override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Stream[Expr] = expr match {
+ case c if c eq expr =>
+ e(NDValue(c.getType))
+ case other =>
+ super.e(other)
}
-
-
-
}
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index d6b4d874f..6a7754cf0 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -5,7 +5,7 @@ package repair
package rules
import synthesis._
-import evaluators._
+import leon.evaluators._
import purescala.Expressions._
import purescala.Common._
@@ -92,12 +92,7 @@ case object Focus extends PreprocessingRule("Focus") {
def ws(g: Expr) = andJoin(Guide(g) +: wss)
def testCondition(cond: Expr) = {
- val ndSpec = postMap {
- case c if c eq cond => Some(not(cond)) // Use reference equality
- case _ => None
- }(fdSpec)
-
- forAllTests(ndSpec, Map(), new RepairNDEvaluator(ctx, program, fd, cond))
+ forAllTests(fdSpec, Map(), new AngelicEvaluator( new RepairNDEvaluator(ctx, program, cond)))
}
guides.flatMap {
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index c972f2e27..2ea08a593 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -3,17 +3,23 @@
package leon.utils
object StreamUtils {
- def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
- var ss = streams
- while(ss.nonEmpty && ss.head.isEmpty) {
- ss = ss.tail
+
+ def interleave[T](streams: Stream[Stream[T]]): Stream[T] = {
+ def rec(streams: Stream[Stream[T]], diag: Int): Stream[T] = {
+ if(streams.isEmpty) Stream() else {
+ val (take, leave) = streams.splitAt(diag)
+ val (nonEmpty, empty) = take partition (_.nonEmpty)
+ nonEmpty.map(_.head) ++ rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
+ }
}
- if(ss.isEmpty) return Stream.empty
- if(ss.size == 1) return ss.head
+ rec(streams, 1)
+ }
- // TODO: This circular-shifts the list. I'd be interested in a constant time
- // operation. Perhaps simply by choosing the right data-structure?
- Stream.cons(ss.head.head, interleave(ss.tail :+ ss.head.tail))
+ def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
+ if (streams.isEmpty) Stream() else {
+ val nonEmpty = streams filter (_.nonEmpty)
+ nonEmpty.toStream.map(_.head) ++ interleave(nonEmpty.map(_.tail))
+ }
}
def cartesianProduct[T](streams : Seq[Stream[T]]) : Stream[List[T]] = {
diff --git a/src/test/resources/regression/repair/Heap3.scala b/src/test/resources/regression/repair/Heap3.scala
new file mode 100644
index 000000000..3305b5d15
--- /dev/null
+++ b/src/test/resources/regression/repair/Heap3.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2015 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.lang._
+import leon.collection._
+
+object Heaps {
+
+ sealed abstract class Heap {
+ val rank : BigInt = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[BigInt] = this match {
+ case Leaf() => Set[BigInt]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:BigInt, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : BigInt, i2 : BigInt) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): BigInt = { t match {
+ case Leaf() => BigInt(0)
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 >= v2) // FIXME swapped the branches
+ makeN(v2, l2, merge(h1, r2))
+ else
+ makeN(v1, l1, merge(r1, h2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: BigInt, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: BigInt, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[BigInt] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index 82c419b04..ff882c961 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -206,7 +206,7 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
List(
new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
+ new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
)
}
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 50b845f92..5b6667d5f 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -16,6 +16,7 @@ class RepairSuite extends LeonRegressionSuite {
val fileToFun = Map(
"Compiler1.scala" -> "desugar",
+ "Heap3.scala" -> "merge",
"Heap4.scala" -> "merge",
"ListEasy.scala" -> "pad",
"List1.scala" -> "pad",
@@ -23,7 +24,10 @@ class RepairSuite extends LeonRegressionSuite {
"MergeSort2.scala" -> "merge"
)
- for (file <- filesInResourceDir("regression/repair/", _.endsWith(".scala")) if fileToFun contains file.getName) {
+ for (file <- filesInResourceDir("regression/repair/", _.endsWith(".scala"))) {
+ if (!(fileToFun contains file.getName)) {
+ fail(s"Don't know which function to repair for ${file.getName}")
+ }
val path = file.getAbsoluteFile.toString
val name = file.getName
diff --git a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
index 4002a0af0..b510c01bb 100644
--- a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
@@ -20,7 +20,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
List(
new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
+ new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
)
}
--
GitLab