From 654c221a38cbb00e81ac19ccb50a12345328483a Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Fri, 24 Apr 2015 15:44:34 +0200 Subject: [PATCH] Add EvaluationPhase to try out evaluation, fix evaluation of CharLiteral --- src/main/scala/leon/Main.scala | 9 +++- .../leon/evaluators/EvaluationPhase.scala | 45 +++++++++++++++++++ .../leon/evaluators/RecursiveEvaluator.scala | 4 +- 3 files changed, 55 insertions(+), 3 deletions(-) create mode 100644 src/main/scala/leon/evaluators/EvaluationPhase.scala diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index e9eb7b6e5..da74e9878 100644 --- a/src/main/scala/leon/Main.scala +++ b/src/main/scala/leon/Main.scala @@ -21,7 +21,8 @@ object Main { synthesis.SynthesisPhase, termination.TerminationPhase, verification.AnalysisPhase, - repair.RepairPhase + repair.RepairPhase, + evaluators.EvaluationPhase ) } @@ -42,9 +43,10 @@ object Main { val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false) val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", true ) val optHelp = LeonFlagOptionDef("help", "Show help message", false) + val optEval = LeonFlagOptionDef("eval", "Evaluate ground functions", false) override val definedOptions: Set[LeonOptionDef[Any]] = - Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify) + Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify, optEval) } @@ -128,6 +130,7 @@ object Main { import xlang.XLangAnalysisPhase import verification.AnalysisPhase import repair.RepairPhase + import evaluators.EvaluationPhase import MainComponent._ val helpF = ctx.findOptionOrDefault(optHelp) @@ -137,6 +140,7 @@ object Main { val repairF = ctx.findOptionOrDefault(optRepair) val terminationF = ctx.findOptionOrDefault(optTermination) val verifyF = ctx.findOptionOrDefault(optVerify) + val evalF = ctx.findOptionOrDefault(optEval) if (helpF) { displayVersion(ctx.reporter) @@ -157,6 +161,7 @@ object Main { else if (repairF) RepairPhase else if (terminationF) TerminationPhase else if (xlangF) XLangAnalysisPhase + else if (evalF) EvaluationPhase else if (verifyF) FunctionClosure andThen AnalysisPhase else NoopPhase() } diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala new file mode 100644 index 000000000..27155c9ee --- /dev/null +++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala @@ -0,0 +1,45 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon +package evaluators + +import purescala.Definitions._ +import purescala.DefOps._ +import purescala.Expressions._ + +object EvaluationPhase extends LeonPhase[Program, Unit] { + val name = "Evaluation" + val description = "Evaluating ground functions" + + implicit val debugSection = utils.DebugSectionEvaluation + + def run(ctx: LeonContext)(program: Program): Unit = { + val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions) + + val reporter = ctx.reporter + + val fdFilter = { + import OptionsHelpers._ + + filterInclusive(evalFuns.map(fdMatcher), None) + } + + val toEvaluate = funDefsFromMain(program).toList.filter(_.params.size == 0).filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos) + + if (toEvaluate.isEmpty) reporter.warning("No ground functions found with the given names") + + val eval = new DefaultEvaluator(ctx, program) + for (fd <- toEvaluate) { + reporter.info(s" - Evaluating ${fd.id}") + val call = FunctionInvocation(fd.typedWithDef, Seq()) + eval.eval(call) match { + case EvaluationResults.Successful(ex) => + reporter.info(s" => $ex") + case EvaluationResults.RuntimeError(msg) => + reporter.warning(s" Runtime Error: $msg") + case EvaluationResults.EvaluatorError(msg) => + reporter.warning(s" Evaluator Error: $msg") + } + } + } +} diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala index 1c33acc3b..925ad6313 100644 --- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala @@ -565,8 +565,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int throw RuntimeError("MatchError: "+rscrut+" did not match any of the cases") } + case l : CharLiteral => l + case other => - context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator.") + context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator ("+other.getClass+").") throw EvalError("Unhandled case in Evaluator : " + other) } -- GitLab