Repaired the abstract evaluator concerning Let expressions.

Added integration/evaluators/AbstractEvaluatorSuite.scala

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))
       }
+    }
   }
 
 

src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala

+/* 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

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 =>
+  
+}