From c8eb81d6e41be67df66f8378bf75ea793d1132ba Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 7 Mar 2016 17:42:44 +0100
Subject: [PATCH] SharedOptions -> GlobalOptions
---
...{SharedOptions.scala => GlobalOptions.scala} | 9 +++++++--
src/main/scala/leon/LeonContext.scala | 2 +-
src/main/scala/leon/Main.scala | 17 +++++++++--------
src/main/scala/leon/Pipeline.scala | 2 +-
.../scala/leon/evaluators/EvaluationPhase.scala | 2 +-
.../leon/frontends/scalac/CodeExtraction.scala | 2 +-
.../invariant/engine/InferenceContext.scala | 6 +++---
.../laziness/LazinessEliminationPhase.scala | 2 +-
.../scala/leon/purescala/PrinterOptions.scala | 6 +++---
src/main/scala/leon/repair/RepairPhase.scala | 4 ++--
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/solvers/SolverFactory.scala | 4 ++--
.../solvers/combinators/UnrollingSolver.scala | 1 -
.../leon/solvers/isabelle/AdaptationPhase.scala | 2 +-
.../solvers/isabelle/IsabelleEnvironment.scala | 4 ++--
src/main/scala/leon/synthesis/SourceInfo.scala | 2 +-
.../scala/leon/synthesis/SynthesisPhase.scala | 4 ++--
.../leon/termination/TerminationPhase.scala | 2 +-
.../leon/verification/VerificationPhase.scala | 4 ++--
.../leon/regression/repair/RepairSuite.scala | 4 ++--
20 files changed, 43 insertions(+), 38 deletions(-)
rename src/main/scala/leon/{SharedOptions.scala => GlobalOptions.scala} (92%)
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/GlobalOptions.scala
similarity index 92%
rename from src/main/scala/leon/SharedOptions.scala
rename to src/main/scala/leon/GlobalOptions.scala
index b68e64c83..4973852c2 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/GlobalOptions.scala
@@ -10,7 +10,7 @@ import OptionParsers._
* Options that determine the pipeline of Leon are not stored here,
* but in [[Main.MainComponent]] instead.
*/
-object SharedOptions extends LeonComponent {
+object GlobalOptions extends LeonComponent {
val name = "sharedOptions"
val description = "Options shared by multiple components of Leon"
@@ -66,7 +66,12 @@ object SharedOptions extends LeonComponent {
val parser: String => Set[DebugSection] = setParser[Set[DebugSection]](debugParser)(_).flatten
}
- val optTimeout = LeonLongOptionDef("timeout", "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)", 0L, "t")
+ val optTimeout = LeonLongOptionDef(
+ "timeout",
+ "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)",
+ 0L,
+ "t"
+ )
override val definedOptions: Set[LeonOptionDef[Any]] = Set(
optStrictPhases,
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 000e785b0..229891418 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -40,7 +40,7 @@ object LeonContext {
LeonContext(
reporter,
new InterruptManager(reporter),
- options = Seq(LeonOption[Set[DebugSection]](SharedOptions.optDebug)(Set(DebugSectionTrees)))
+ options = Seq(LeonOption[Set[DebugSection]](GlobalOptions.optDebug)(Set(DebugSectionTrees)))
)
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 509a04d38..f8cfa690e 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -35,7 +35,7 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- solvers.combinators.UnrollingProcedure, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
+ solvers.combinators.UnrollingProcedure, MainComponent, GlobalOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
)
/*
@@ -74,14 +74,14 @@ object Main {
reporter.info("")
reporter.title("Additional global options")
- for (opt <- SharedOptions.definedOptions.toSeq.sortBy(_.name)) {
+ for (opt <- GlobalOptions.definedOptions.toSeq.sortBy(_.name)) {
reporter.info(opt.helpString)
}
reporter.info("")
reporter.title("Additional options, by component:")
- for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
+ for (c <- (allComponents - MainComponent - GlobalOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
reporter.info(s"${c.name} (${c.description})")
for (opt <- c.definedOptions.toSeq.sortBy(_.name)) {
@@ -127,8 +127,9 @@ object Main {
val reporter = new DefaultReporter(
leonOptions.collectFirst {
- case LeonOption(SharedOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
- }.getOrElse(Set[DebugSection]()))
+ case LeonOption(GlobalOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
+ }.getOrElse(Set[DebugSection]())
+ )
reporter.whenDebug(DebugSectionOptions) { debug =>
debug("Options considered by Leon:")
@@ -159,13 +160,13 @@ object Main {
import genc.CFileOutputPhase
import MainComponent._
import invariant.engine.InferInvariantsPhase
- import transformations._
+ import transformations.InstrumentationPhase
import laziness._
val helpF = ctx.findOptionOrDefault(optHelp)
val noopF = ctx.findOptionOrDefault(optNoop)
val synthesisF = ctx.findOptionOrDefault(optSynthesis)
- val xlangF = ctx.findOptionOrDefault(SharedOptions.optXLang)
+ val xlangF = ctx.findOptionOrDefault(GlobalOptions.optXLang)
val repairF = ctx.findOptionOrDefault(optRepair)
val isabelleF = ctx.findOptionOrDefault(optIsabelle)
val terminationF = ctx.findOptionOrDefault(optTermination)
@@ -239,7 +240,7 @@ object Main {
ctx.interruptManager.registerSignalHandler()
- val doWatch = ctx.findOptionOrDefault(SharedOptions.optWatch)
+ val doWatch = ctx.findOptionOrDefault(GlobalOptions.optWatch)
if (doWatch) {
val watcher = new FilesWatcher(ctx, ctx.files ++ Build.libFiles.map { new java.io.File(_) })
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index aa1471cb8..24875b4a6 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -8,7 +8,7 @@ abstract class Pipeline[-F, +T] {
def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
def run(ctx: LeonContext, v: F): (LeonContext, G) = {
val (ctx2, s) = self.run(ctx, v)
- if(ctx.findOptionOrDefault(SharedOptions.optStrictPhases)) ctx.reporter.terminateIfError()
+ if(ctx.findOptionOrDefault(GlobalOptions.optStrictPhases)) ctx.reporter.terminateIfError()
thenn.run(ctx2, s)
}
}
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index df2f4c42a..79ae30a5b 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -15,7 +15,7 @@ object EvaluationPhase extends UnitPhase[Program] {
implicit val debugSection = utils.DebugSectionEvaluation
def apply(ctx: LeonContext, program: Program): Unit = {
- val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
+ val evalFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4b3c577ad..65ea83c7f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -71,7 +71,7 @@ trait CodeExtraction extends ASTExtractors {
/** An exception thrown when non-purescala compatible code is encountered. */
sealed class ImpureCodeEncounteredException(pos: Position, msg: String, ot: Option[Tree]) extends Exception(msg) {
def emit() {
- val debugInfo = if (ctx.findOptionOrDefault(SharedOptions.optDebug) contains utils.DebugSectionTrees) {
+ val debugInfo = if (ctx.findOptionOrDefault(GlobalOptions.optDebug) contains utils.DebugSectionTrees) {
ot.map { t =>
val strWr = new java.io.StringWriter()
new global.TreePrinter(new java.io.PrintWriter(strWr)).printTree(t)
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index 48a45b048..904ae7728 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -33,13 +33,13 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
val withmult = leonContext.findOption(optWithMult).getOrElse(false)
val usereals = leonContext.findOption(optUseReals).getOrElse(false)
val useCegis: Boolean = leonContext.findOption(optCegis).getOrElse(false)
- val dumpStats = leonContext.findOption(SharedOptions.optBenchmark).getOrElse(false)
+ val dumpStats = leonContext.findOption(GlobalOptions.optBenchmark).getOrElse(false)
// the following options have default values
val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
val nlTimeout = leonContext.findOption(optNLTimeout).getOrElse(15L)
- val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
- val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
+ val totalTimeout = leonContext.findOption(GlobalOptions.optTimeout) // in secs
+ val functionsToInfer = leonContext.findOption(GlobalOptions.optFunctions)
val reporter = leonContext.reporter
val maxCegisBound = 1000
val statsSuffix = leonContext.findOption(optStatsSuffix).getOrElse("-stats" + FileCountGUID.getID)
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 9c1abab53..60daeb0d3 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -116,7 +116,7 @@ object LazinessEliminationPhase extends TransformationPhase {
checkInstrumentationSpecs(instProg, checkCtx,
checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false))
// dump stats
- if (ctx.findOption(SharedOptions.optBenchmark).getOrElse(false)) {
+ if (ctx.findOption(GlobalOptions.optBenchmark).getOrElse(false)) {
val modid = prog.units.find(_.isMainUnit).get.id
val filename = modid + "-stats.txt"
val pw = new PrintWriter(filename)
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 6a95b265d..22c4c0247 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -14,9 +14,9 @@ case class PrinterOptions (
object PrinterOptions {
def fromContext(ctx: LeonContext): PrinterOptions = {
- val debugTrees = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTrees
- val debugTypes = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTypes
- val debugPositions = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionPositions
+ val debugTrees = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTrees
+ val debugTypes = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTypes
+ val debugPositions = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionPositions
PrinterOptions(
baseIndent = 0,
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 342d41ddd..1481b0e78 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -13,8 +13,8 @@ object RepairPhase extends UnitPhase[Program]() {
implicit val debugSection = utils.DebugSectionRepair
def apply(ctx: LeonContext, program: Program) = {
- val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
- val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.optTimeout) map { _ * 1000 }
+ val repairFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
+ val verifTimeoutMs: Option[Long] = ctx.findOption(GlobalOptions.optTimeout) map { _ * 1000 }
val reporter = ctx.reporter
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 49f9c0ff2..65b6aee97 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -29,7 +29,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val reporter = ctx.reporter
- val doBenchmark = ctx.findOptionOrDefault(SharedOptions.optBenchmark)
+ val doBenchmark = ctx.findOptionOrDefault(GlobalOptions.optBenchmark)
var program = initProgram
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 4f8b1f50a..18b8a72a1 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -49,7 +49,7 @@ object SolverFactory {
}.mkString("")
def getFromSettings(implicit ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+ val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
if (((names contains "fairz3") || (names contains "unrollz3")) && !hasNativeZ3) {
if (hasZ3) {
@@ -138,7 +138,7 @@ object SolverFactory {
// Fast solver used by simplifications, to discharge simple tautologies
def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+ val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
if ((names contains "fairz3") && !hasNativeZ3) {
if (hasZ3) {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 95a8cdd67..e00faa54c 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package combinators
-import purescala.Printable
import purescala.Common._
import purescala.Definitions._
import purescala.Quantification._
diff --git a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
index 2d3218c7b..ace759b4e 100644
--- a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
+++ b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
@@ -32,7 +32,7 @@ object AdaptationPhase extends TransformationPhase {
CaseClass(CaseClassType(dummy, List(tree)), Nil)
val enabled =
- context.findOptionOrDefault(SharedOptions.optSelectedSolvers).contains("isabelle") ||
+ context.findOptionOrDefault(GlobalOptions.optSelectedSolvers).contains("isabelle") ||
context.findOptionOrDefault(Main.MainComponent.optIsabelle)
if (!enabled) program
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 5856374e2..fa7b3d034 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -9,7 +9,7 @@ import scala.concurrent.ExecutionContext.Implicits.global
import leon.LeonContext
import leon.OptionsHelpers._
-import leon.SharedOptions
+import leon.GlobalOptions
import leon.purescala.Definitions._
import leon.purescala.Expressions._
import leon.purescala.Common._
@@ -34,7 +34,7 @@ object IsabelleEnvironment {
val funFilter =
// FIXME duplicated from AnalysisPhase
- filterInclusive[FunDef](context.findOption(SharedOptions.optFunctions).map(fdMatcher(program)), Some(_.annotations contains "library"))
+ filterInclusive[FunDef](context.findOption(GlobalOptions.optFunctions).map(fdMatcher(program)), Some(_.annotations contains "library"))
val funs = program.definedFunctions.filter(funFilter)
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index ca689cca0..70f116d5f 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -21,7 +21,7 @@ object SourceInfo {
}
def extractFromProgram(ctx: LeonContext, prog: Program): List[SourceInfo] = {
- val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
+ val functions = ctx.findOption(GlobalOptions.optFunctions) map { _.toSet }
def excludeByDefault(fd: FunDef): Boolean = {
fd.annotations contains "library"
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7c90d3e3b..2385f5079 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -32,7 +32,7 @@ object SynthesisPhase extends TransformationPhase {
def processOptions(ctx: LeonContext): SynthesisSettings = {
val ms = ctx.findOption(optManual)
- val timeout = ctx.findOption(SharedOptions.optTimeout)
+ val timeout = ctx.findOption(GlobalOptions.optTimeout)
if (ms.isDefined && timeout.isDefined) {
ctx.reporter.warning("Defining timeout with manual search")
}
@@ -58,7 +58,7 @@ object SynthesisPhase extends TransformationPhase {
costModel = costModel,
rules = Rules.all(ctx.findOptionOrDefault(optCEGISNaiveGrammar)),
manualSearch = ms,
- functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
+ functions = ctx.findOption(GlobalOptions.optFunctions) map { _.toSet },
cegisUseOptTimeout = ctx.findOptionOrDefault(optCEGISOptTimeout),
cegisUseVanuatoo = ctx.findOptionOrDefault(optCEGISVanuatoo),
cegisMaxSize = ctx.findOptionOrDefault(optCEGISMaxSize).toInt
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index f75d388d4..15f2dbe5a 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -20,7 +20,7 @@ object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher(program)), Some(excludeByDefault _))
+ filterInclusive(ctx.findOption(GlobalOptions.optFunctions).map(fdMatcher(program)), Some(excludeByDefault _))
}
val toVerify = tc.program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 04c4ecdcc..b9da4addb 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -22,8 +22,8 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
implicit val debugSection = utils.DebugSectionVerification
def apply(ctx: LeonContext, program: Program): VerificationReport = {
- val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
- val timeout: Option[Long] = ctx.findOption(SharedOptions.optTimeout)
+ val filterFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
+ val timeout: Option[Long] = ctx.findOption(GlobalOptions.optTimeout)
val reporter = ctx.reporter
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 5f9861362..653afe38f 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -38,9 +38,9 @@ class RepairSuite extends LeonRegressionSuite {
reporter = reporter,
interruptManager = new InterruptManager(reporter),
options = Seq(
- LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
+ LeonOption(GlobalOptions.optFunctions)(Seq(fileToFun(name))),
LeonOption(VerificationPhase.optParallelVCs)(true),
- LeonOption(SharedOptions.optTimeout)(180L)
+ LeonOption(GlobalOptions.optTimeout)(180L)
)
)
--
GitLab