diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 23236cb7317ecc048271094f092109722a09f889..2b8baa99424dbd7de9d4d2c4d87c82293e4de2b1 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -7,6 +7,7 @@ import purescala.Extractors.Operator
import purescala.Constructors._
import purescala.Expressions._
import purescala.Types._
+import purescala.Common.Identifier
import purescala.Definitions.{TypedFunDef, Program}
import purescala.DefOps
import purescala.TypeOps
@@ -14,10 +15,37 @@ import purescala.ExprOps
import purescala.Expressions.Expr
import leon.utils.DebugSectionSynthesis
+case class AbstractRecContext(mappings: Map[Identifier, Expr], mappingsAbstract: Map[Identifier, Expr]) extends RecContext[AbstractRecContext] {
+ def newVars(news: Map[Identifier, Expr], newsAbstract: Map[Identifier, Expr]): AbstractRecContext = copy(news, newsAbstract)
+ def newVars(news: Map[Identifier, Expr]): AbstractRecContext = copy(news, news)
+
+ def withNewVar(id: Identifier, v: (Expr, Expr)): AbstractRecContext = {
+ newVars(mappings + (id -> v._1), mappingsAbstract + (id -> v._2))
+ }
+
+ def withNewVars2(news: Map[Identifier, (Expr, Expr)]): AbstractRecContext = {
+ newVars(mappings ++ news.mapValues(_._1), mappingsAbstract ++ news.mapValues(_._2))
+ }
+
+ override def withNewVar(id: Identifier, v: Expr): AbstractRecContext = {
+ newVars(mappings + (id -> v), mappingsAbstract + (id -> v))
+ }
+
+ override def withNewVars(news: Map[Identifier, Expr]): AbstractRecContext = {
+ newVars(mappings ++ news, mappingsAbstract ++ news)
+ }
+}
+
+
+trait HasAbstractRecContext extends ContextualEvaluator {
+ type RC = AbstractRecContext
+ def initRC(mappings: Map[Identifier, Expr]) = AbstractRecContext(mappings, mappings)
+}
+
/** The evaluation returns a pair (e, t),
* where e is the expression evaluated as much as possible, and t is the way the expression has been evaluated.
* Caution: If and Match statement require the condition to be non-abstract. */
-class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasDefaultRecContext {
+class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasAbstractRecContext {
lazy val scalaEv = new ScalacEvaluator(underlying, ctx, prog)
/** Evaluates resuts which can be evaluated directly
@@ -26,14 +54,21 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
underlying.setEvaluationFailOnChoose(true)
override type Value = (Expr, Expr)
- override val description: String = "Evaluates string programs but keeps the formula which generated the string"
- override val name: String = "String Tracing evaluator"
-
- protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = expr match {
+ override val description: String = "Evaluates string programs but keeps the formula which generated the value"
+ override val name: String = "Abstract evaluator"
+
+
+ protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = {
+ implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings)
+ expr match {
case Variable(id) =>
- rctx.mappings.get(id) match {
- case Some(v) if v != expr =>
+ (rctx.mappings.get(id), rctx.mappingsAbstract.get(id)) match {
+ case (Some(v), None) if v != expr => // We further evaluate v to make sure it is a value
e(v)
+ case (Some(v), Some(va)) if v != expr =>
+ (e(v)._1, va)
+ case (Some(v), Some(va)) =>
+ (v, va)
case _ =>
(expr, expr)
}
@@ -53,12 +88,11 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
case MatchExpr(scrut, cases) =>
val (escrut, tscrut) = e(scrut)
- val rscrut = escrut
- cases.toStream.map(c => underlying.matchesCase(rscrut, c)).find(_.nonEmpty) match {
+ cases.toStream.map(c => underlying.matchesCase(escrut, c)).find(_.nonEmpty) match {
case Some(Some((c, mappings))) =>
e(c.rhs)(rctx.withNewVars(mappings), gctx)
case _ =>
- throw RuntimeError("MatchError(Abstract evaluation): "+rscrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
+ throw RuntimeError("MatchError(Abstract evaluation): "+escrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
}
case FunctionInvocation(tfd, args) =>
@@ -88,6 +122,9 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
}
}
callResult
+ case Let(i, ex, b) =>
+ val (first, second) = e(ex)
+ e(b)(rctx.withNewVar(i, (first, second)), gctx)
case Operator(es, builder) =>
val (ees, ts) = es.map(e).unzip
if(ees forall ExprOps.isValue) {
@@ -95,6 +132,7 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
} else {
(builder(ees), builder(ts))
}
+ }
}
diff --git a/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..99678f887250e717f6cbb24071240c03c38f7ba1
--- /dev/null
+++ b/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
@@ -0,0 +1,92 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.integration.evaluators
+
+import leon.test._
+import helpers.ExpressionsDSLProgram
+import leon.evaluators._
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import org.scalatest.Matchers
+
+class AbstractEvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSLProgram with Matchers {
+ //override def a = super[ExpressionsDSL].a
+
+ val sources = List("""
+import leon.lang._
+
+object AbstractTests {
+ abstract class Tree
+ case class Node(w: Tree, x: Int, y: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def param(x: String) = x + x
+
+ def test() = {
+ val x = "19"
+ val w = 9
+ val y = w*w+5
+ val z = y.toString
+ val res = param(x) + z
+ res
+ }
+
+ def test2(right: Boolean, c: Tree): Int = {
+ if(right) {
+ c match {
+ case Leaf() => 0
+ case Node(_, a, Leaf()) => a
+ case Node(_, _, n) => test2(right, n)
+ }
+ } else {
+ c match {
+ case Leaf() => 0
+ case Node(Leaf(), a, _) => a
+ case Node(n, _, _) => test2(right, n)
+ }
+ }
+ }
+}""")
+
+ test("Abstract evaluator should keep track of variables") { implicit fix =>
+ val testFd = funDef("AbstractTests.test")
+
+ val ae = new AbstractEvaluator(fix._1, fix._2)
+
+ val res = ae.eval(FunctionInvocation(testFd.typed, Seq()))
+
+ res.result match {
+ case Some((e, expr)) =>
+ e should equal (StringLiteral("191986"))
+ expr should equal (StringConcat(StringConcat(StringLiteral("19"), StringLiteral("19")), Int32ToString(BVPlus(BVTimes(IntLiteral(9), IntLiteral(9)), IntLiteral(5)))))
+ case None =>
+ fail("No result!")
+ }
+ }
+
+ test("Abstract evaluator should correctly handle boolean and recursive") { implicit fix =>
+ val testFd = funDef("AbstractTests.test2")
+ val Leaf = cc("AbstractTests.Leaf")()
+ def Node(left: Expr, n: Expr, right: Expr) = cc("AbstractTests.Node")(left, n, right)
+
+ val ae = new AbstractEvaluator(fix._1, fix._2)
+
+ val res = ae.eval(FunctionInvocation(testFd.typed, Seq(BooleanLiteral(true), Node(Leaf, IntLiteral(5), Leaf)))).result match {
+ case Some((e, expr)) =>
+ e should equal (IntLiteral(5))
+ expr should equal (IntLiteral(5))
+ case None =>
+ fail("No result!")
+ }
+ val a = id("a", Int32Type)
+ ae.eval(FunctionInvocation(testFd.typed, Seq(BooleanLiteral(true), Node(Leaf, Variable(a), Leaf)))).result match {
+ case Some((e, expr)) =>
+ e should equal (Variable(a))
+ expr should equal (Variable(a))
+ case None =>
+ fail("No result!")
+ }
+ }
+
+}
\ 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 fa118cbcc94a14bce81ffdacd9af4c5f154f8c6e..63469ead59c6c4441ce12a92fc92c4349ae99d5b 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -9,9 +9,7 @@ import leon.purescala.Common._
import leon.purescala.Types._
import leon.purescala.Expressions._
-trait ExpressionsDSL {
- self: Assertions =>
-
+trait ExpressionsDSLVariables {
val F = BooleanLiteral(false)
val T = BooleanLiteral(true)
@@ -35,6 +33,11 @@ trait ExpressionsDSL {
val p = FreshIdentifier("p", BooleanType).toVariable
val q = FreshIdentifier("q", BooleanType).toVariable
val r = FreshIdentifier("r", BooleanType).toVariable
+}
+
+trait ExpressionsDSLProgram {
+self: Assertions =>
+
def id(name: String, tpe: TypeTree)(implicit pgm: Program): Identifier = {
FreshIdentifier(name, tpe)
@@ -93,3 +96,8 @@ trait ExpressionsDSL {
FunctionInvocation(tfd, args.toSeq)
}
}
+
+trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
+ self: Assertions =>
+
+}