From 57710fe219d542d2f1d2fa259df5303c5cadd744 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 8 Jan 2013 21:50:32 +0100
Subject: [PATCH] "Support" for `choose` in evaluators.
What this commit really introduces is a graceful failure when asked to
evaluate a `choose` expression. In particular, it makes it possible for
codegen evaluator to compile functions that contain `choose`
expressions, and even evaluate them, as long as the execution path
doesn't meet a `choose` expressions.
---
.../LeonCodeGenEvaluationException.java | 11 +++++++
.../runtime/LeonCodeGenRuntimeException.java | 2 ++
.../scala/leon/codegen/CodeGeneration.scala | 7 +++++
.../leon/evaluators/CodeGenEvaluator.scala | 3 ++
.../leon/evaluators/DefaultEvaluator.scala | 3 ++
.../test/evaluators/EvaluatorsTests.scala | 30 +++++++++++++++++++
6 files changed, 56 insertions(+)
create mode 100644 src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
new file mode 100644
index 000000000..f4ba02da8
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
@@ -0,0 +1,11 @@
+package leon.codegen.runtime;
+
+/** Such exceptions are thrown when the evaluator is asked to do something it
+ * cannot do, for instance evaluating a `choose` expression. It should be
+ * distinguished from `LeonCodeGenRuntimeException`s, which are thrown when
+ * the evaluator runs into a runtime error (.get on an undefined map, etc.). */
+public class LeonCodeGenEvaluationException extends Exception {
+ public LeonCodeGenEvaluationException(String msg) {
+ super(msg);
+ }
+}
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
index 39cb3bfc1..8a3e6b86a 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
@@ -1,5 +1,7 @@
package leon.codegen.runtime;
+/** Such exceptions are thrown when the evaluator encounters a runtime error,
+ * for instance `.get` with an undefined key on a map. */
public class LeonCodeGenRuntimeException extends Exception {
public LeonCodeGenRuntimeException(String msg) {
super(msg);
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 65eb47562..11e57f36e 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -22,6 +22,7 @@ object CodeGeneration {
private val MapClass = "leon/codegen/runtime/Map"
private val CaseClassClass = "leon/codegen/runtime/CaseClass"
private val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
+ private val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
def defToJVMName(p : Program, d : Definition) : String = "Leon$CodeGen$" + d.id.uniqueName
@@ -288,6 +289,12 @@ object CodeGeneration {
ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
ch << ATHROW
+ case Choose(_, _) =>
+ ch << New(ImpossibleEvaluationClass) << DUP
+ ch << Ldc("Cannot execute choose.")
+ ch << InvokeSpecial(ImpossibleEvaluationClass, constructorName, "(Ljava/lang/String;)V")
+ ch << ATHROW
+
case b if b.getType == BooleanType && canDelegateToMkBranch =>
val fl = ch.getFreshLabel("boolfalse")
val al = ch.getFreshLabel("boolafter")
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 9b9702f31..c9f6bed91 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -45,6 +45,9 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
// and the check above would fail.
case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenRuntimeException") =>
EvaluationFailure(t.getMessage)
+
+ case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenEvaluationException") =>
+ EvaluationError(t.getMessage)
}
})
}
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index a6998f10b..9b0bbdc2e 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -284,6 +284,9 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
BooleanLiteral(newArgs.distinct.size == newArgs.size)
}
+ case Choose(_, _) =>
+ throw EvalError("Cannot evaluate choose.")
+
case other => {
context.reporter.error("Error: don't know how to handle " + other + " in Evaluator.")
throw EvalError("Unhandled case in Evaluator : " + other)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 2633a1b9c..d832950cc 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -141,6 +141,19 @@ class EvaluatorsTests extends FunSuite {
}
}
+ private def checkEvaluatorError(evaluator : Evaluator, in : Expr) {
+ evaluator.eval(in) match {
+ case EvaluationFailure(msg) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it failed instead (%s).".format(in, evaluator.name, msg))
+
+ case EvaluationSuccessful(result) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it produced the result '%s' instead.".format(in, evaluator.name, result))
+
+ case EvaluationError(_) =>
+ // that's the desired outcome
+ }
+ }
+
private def T = BooleanLiteral(true)
private def F = BooleanLiteral(false)
private def IL(i : Int) = IntLiteral(i)
@@ -357,4 +370,21 @@ class EvaluatorsTests extends FunSuite {
checkComp(e, MapIsDefinedAt(mkCall("finite2"), IL(3)), F)
}
}
+
+ test("Misc") {
+ val p = """|object Program {
+ | import leon.Utils._
+ |
+ | def c(i : Int) : Int = choose { (j : Int) => j > i }
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ for(e <- evaluators) {
+ checkEvaluatorError(e, mkCall("c", IL(42)))
+ }
+ }
}
--
GitLab