From 8d1a95b3ac01a723d5440fdf3238e6acb15a0d4c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 23 Jun 2015 15:35:58 +0200
Subject: [PATCH] Fix problems with options
Move optEval to MainComponent
Add helpful comments
Beautify how debugSections are printed
Termination and analysis should happen iff --verify and --termination
---
src/main/scala/leon/Main.scala | 25 +++++++++++--------
src/main/scala/leon/SharedOptions.scala | 20 +++++++++------
.../leon/evaluators/EvaluationPhase.scala | 3 ++-
.../scala/leon/synthesis/SynthesisPhase.scala | 2 +-
4 files changed, 31 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 04df65e6d..1933e5acb 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,20 +31,25 @@ object Main {
solvers.z3.FairZ3Component, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component
)
+ /*
+ * This object holds the options that determine the selected pipeline of Leon.
+ * Please put any further such options here to have them print nicely in --help message.
+ */
object MainComponent extends LeonComponent {
val name = "main"
val description = "Options that determine the feature of Leon to be used (mutually exclusive). Default: verify"
- val optTermination = LeonFlagOptionDef("termination", "Check program termination", false)
- val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
- val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
- val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
- 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 = LeonStringOptionDef("eval", "Evaluate ground functions with selected evaluator", "default", "[code|default]")
+ val optXLang = LeonFlagOptionDef("xlang", "Verification with support for extra program constructs (imperative,...)", false)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ 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)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optVerify)
+ Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optEval, optVerify)
}
@@ -149,10 +154,10 @@ object Main {
val synthesisF = ctx.findOptionOrDefault(optSynthesis)
val xlangF = ctx.findOptionOrDefault(optXLang)
val repairF = ctx.findOptionOrDefault(optRepair)
- val analysisF = ctx.findOption(optVerify).isDefined && ctx.findOption(optTermination).isDefined
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
- val evalF = ctx.findOption(SharedOptions.optEval)
+ val evalF = ctx.findOption(optEval)
+ val analysisF = verifyF && terminationF
def debugTrees(title: String): LeonPhase[Program, Program] = {
if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index cbddcd015..369043e66 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -5,6 +5,12 @@ package leon
import leon.utils.{DebugSections, DebugSection}
import OptionParsers._
+/*
+ * This object contains options that are shared among different modules of Leon.
+ *
+ * Options that determine the pipeline of Leon are not stored here,
+ * but in MainComponent in Main.scala.
+ */
object SharedOptions extends LeonComponent {
val name = "sharedOptions"
@@ -22,8 +28,6 @@ object SharedOptions extends LeonComponent {
val usageRhs = "f1,f2,..."
}
- val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "[code|default]")
-
val optSelectedSolvers = new LeonOptionDef[Set[String]] {
val name = "solvers"
val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
@@ -35,10 +39,13 @@ object SharedOptions extends LeonComponent {
val optDebug = new LeonOptionDef[Set[DebugSection]] {
import OptionParsers._
val name = "debug"
- val description = (
- "Enable detailed messages per component.\nAvailable:" +:
- DebugSections.all.toSeq.map(_.name).sorted
- ).mkString("\n ")
+ val description = {
+ val sects = DebugSections.all.toSeq.map(_.name).sorted
+ val (first, second) = sects.splitAt(sects.length/2)
+ "Enable detailed messages per component.\nAvailable:\n" +
+ " " + first.mkString(", ") + ",\n" +
+ " " + second.mkString(", ")
+ }
val default = Set[DebugSection]()
val usageRhs = "d1,d2,..."
val debugParser: OptionParser[Set[DebugSection]] = s => {
@@ -66,7 +73,6 @@ object SharedOptions extends LeonComponent {
optSelectedSolvers,
optDebug,
optWatch,
- optEval,
optTimeout
)
}
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index 13c5418ae..5cd45f2dc 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -3,6 +3,7 @@
package leon
package evaluators
+import leon.Main.MainComponent
import purescala.Definitions._
import purescala.DefOps._
import purescala.Expressions._
@@ -16,7 +17,7 @@ object EvaluationPhase extends LeonPhase[Program, Unit] {
def run(ctx: LeonContext)(program: Program): Unit = {
val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
- val evaluator = ctx.findOptionOrDefault(SharedOptions.optEval)
+ val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
val reporter = ctx.reporter
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 0287ec02e..25824923d 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -15,7 +15,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val name = "Synthesis"
val description = "Partial synthesis of \"choose\" constructs. Also used by repair during the synthesis stage."
- val optManual = LeonStringOptionDef("manual", "Manual search", default = "", "cmd")
+ val optManual = LeonStringOptionDef("manual", "Manual search", default = "", "[cmd]")
val optCostModel = LeonStringOptionDef("costmodel", "Use a specific cost model for this search", "FIXME", "cm")
val optDerivTrees = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
--
GitLab