From 950381a54821ed3f321f3d10d4c428d0794f2f4d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 4 Dec 2015 17:56:08 +0100
Subject: [PATCH] Fix bugs in Evaluators, add tests
---
.../leon/evaluators/RecursiveEvaluator.scala | 8 ++--
.../leon/evaluators/StreamEvaluator.scala | 12 +++---
.../evaluators/EvaluatorSuite.scala | 41 +++++++++++++++++++
3 files changed, 51 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 914636ed1..c3f9eed0f 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -631,11 +631,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
None
}
case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(FunctionInvocation(up.unapplyFun, Seq(scrut))) match {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get =>
+ e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match {
+ case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get =>
- val res = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map {
+ case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
+ val res = subs zip unwrapTuple(arg, subs.size) map {
case (s,a) => matchesPattern(s,a)
}
if (res.forall(_.isDefined)) {
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index f9ef63bdd..9cc6dd132 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -252,12 +252,12 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
} else {
Stream()
}
- case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(FunctionInvocation(up.unapplyFun, Seq(scrut))) flatMap {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get =>
+ case (UnapplyPattern(ob, unapplyFun, subs), scrut) =>
+ e(functionInvocation(unapplyFun.fd, Seq(scrut))) flatMap {
+ case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get =>
- val subMaps = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map {
+ case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
+ val subMaps = subs zip unwrapTuple(arg, subs.size) map {
case (s,a) => matchesPattern(s,a)
}
cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
@@ -305,7 +305,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Some(step(expr, es))
} catch {
case _: RuntimeError =>
- // EvalErrors stop the computation alltogether
+ // EvalErrors stop the computation altogether
None
}
}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index ff882c961..84b0087ca 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -187,6 +187,38 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
| def f3 = C(42).isInstanceOf[A]
|}""".stripMargin,
+ """import leon.lang._
+ |import leon.collection._
+ |
+ |object Foo {
+ | def unapply(i: BigInt): Option[BigInt] = if (i > 0) Some(i) else None()
+ |}
+ |
+ |object Unapply {
+ | def foo =
+ | (BigInt(1) match {
+ | case Foo(i) => i
+ | case _ => BigInt(0)
+ | }) + (BigInt(-12) match {
+ | case Foo(i) => i
+ | case _ => BigInt(2)
+ | })
+ |
+ | def size[A](l: List[A]): BigInt = l match {
+ | case _ :: _ :: _ :: Nil() => 3
+ | case _ :: _ :: Nil() => 2
+ | case _ :: Nil() => 1
+ | case Nil() => 0
+ | case _ :: _ => 42
+ | }
+ |
+ | def s1 = size(1 :: 2 :: 3 :: Nil[Int]())
+ | def s2 = size(Nil[Int]())
+ | def s3 = size(List(1,2,3,4,5,6,7,8))
+ |
+ |}
+ """.stripMargin,
+
"""object Casts1 {
| abstract class Foo
| case class Bar1(v: BigInt) extends Foo
@@ -371,6 +403,15 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
}
}
+ test("Unapply") { implicit fix =>
+ for(e <- allEvaluators) {
+ eval(e, fcall("Unapply.foo")()) === bi(3)
+ eval(e, fcall("Unapply.s1")()) === bi(3)
+ eval(e, fcall("Unapply.s2")()) === bi(0)
+ eval(e, fcall("Unapply.s3")()) === bi(42)
+ }
+ }
+
test("Casts1") { implicit fix =>
def bar1(es: Expr*) = cc("Casts1.Bar1")(es: _*)
def bar2(es: Expr*) = cc("Casts1.Bar2")(es: _*)
--
GitLab