From b80015182981044b6f5fca4139d112549bc9ffb9 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 21 Oct 2016 09:38:15 +0200
Subject: [PATCH] Reorganized options and added a simple main to Inox
---
src/main/scala/inox/Context.scala | 2 +-
src/main/scala/inox/Main.scala | 167 ++++++++++++++++++
src/main/scala/inox/Options.scala | 68 ++-----
src/main/scala/inox/ast/Printers.scala | 6 +-
.../inox/evaluators/ContextualEvaluator.scala | 3 +-
.../scala/inox/evaluators/Evaluator.scala | 9 +-
.../inox/evaluators/SolvingEvaluator.scala | 7 +-
src/main/scala/inox/solvers/Solver.scala | 18 +-
.../scala/inox/solvers/SolverFactory.scala | 6 +-
.../inox/solvers/smtlib/CVC4Solver.scala | 1 -
.../inox/solvers/smtlib/SMTLIBDebugger.scala | 2 +-
.../solvers/unrolling/UnrollingSolver.scala | 11 +-
12 files changed, 195 insertions(+), 105 deletions(-)
create mode 100644 src/main/scala/inox/Main.scala
diff --git a/src/main/scala/inox/Context.scala b/src/main/scala/inox/Context.scala
index 1cf9d8dab..54a8bf20d 100644
--- a/src/main/scala/inox/Context.scala
+++ b/src/main/scala/inox/Context.scala
@@ -25,7 +25,7 @@ object Context {
Context(
reporter,
new InterruptManager(reporter),
- options = Options.empty + InoxOptions.optDebug(Set(ast.DebugSectionTrees: DebugSection))
+ options = Options.empty + Main.optDebug(Set(ast.DebugSectionTrees: DebugSection))
)
}
}
diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
new file mode 100644
index 000000000..e19602e40
--- /dev/null
+++ b/src/main/scala/inox/Main.scala
@@ -0,0 +1,167 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+
+import solvers._
+
+trait MainHelpers {
+
+ protected def getDebugSections: Set[DebugSection] = Set(
+ ast.DebugSectionTrees,
+ datagen.DebugSectionDataGen,
+ solvers.DebugSectionSolver
+ )
+
+ protected final val debugSections = getDebugSections
+
+ final object optDebug extends OptionDef[Set[DebugSection]] {
+ import OptionParsers._
+ val name = "debug"
+ val default = Set[DebugSection]()
+ val usageRhs = "d1,d2,..."
+
+ private val debugParser: OptionParser[Set[DebugSection]] = s => {
+ if (s == "all") Some(debugSections)
+ else debugSections.find(_.name == s).map(Set(_))
+ }
+
+ val parser: String => Option[Set[DebugSection]] = {
+ setParser[Set[DebugSection]](debugParser)(_).map(_.flatten)
+ }
+ }
+
+ protected def getOptions: Map[OptionDef[_], String] = Map(
+ optTimeout -> "Set a timeout for each proof attempt (in sec.)",
+ optSelectedSolvers -> {
+ "Use solvers s1, s2,...\nAvailable: " +
+ solvers.SolverFactory.solverNames.toSeq.sortBy(_._1).map {
+ case (name, desc) => f"\n $name%-14s : $desc"
+ }
+ },
+ optDebug -> {
+ val sects = debugSections.toSeq.map(_.name).sorted
+ val (first, second) = sects.splitAt(sects.length/2 + 1)
+ "Enable detailed messages per component.\nAvailable:\n" +
+ " " + first.mkString(", ") + ",\n" +
+ " " + second.mkString(", ")
+ },
+ ast.optPrintPositions -> "Attach positions to trees when printing",
+ ast.optPrintUniqueIds -> "Always print unique ids",
+ ast.optPrintTypes -> "Attach types to trees when printing",
+ solvers.optCheckModels -> "Double-check counter-examples with evaluator",
+ solvers.optSilentErrors -> "Fail silently into UNKNOWN when encountering an error",
+ solvers.unrolling.optUnrollFactor -> "Number of unrollings to perform in each unfold step",
+ solvers.unrolling.optFeelingLucky -> "Use evaluator to find counter-examples early",
+ solvers.unrolling.optUnrollAssumptions -> "Use unsat-assumptions to drive unfolding while remaining fair",
+ solvers.smtlib.optCVC4Options -> "Pass extra options to CVC4",
+ evaluators.optMaxCalls -> "Maximum number of function invocations allowed during evaluation",
+ evaluators.optIgnoreContracts -> "Don't fail on invalid contracts during evaluation"
+ )
+
+ protected final val options = getOptions
+
+ private def helpString(opt: OptionDef[_]): String = {
+ f"${opt.usageDesc}%-28s" + options(opt).replaceAll("\n", "\n" + " " * 28)
+ }
+
+ /** The current files on which Inox is running.
+ *
+ * This option cannot be filled through option parsing and must always be
+ * instantiated manually (see [[processOptions]]). We therefore MUST NOT add
+ * it to the [[options]] map!
+ */
+ final object optFiles extends OptionDef[Seq[java.io.File]] {
+ val name = "files"
+ val default = Seq[java.io.File]()
+ val usageRhs = "No possible usage"
+ val parser = { (_: String) => throw FatalError("Unparsable option \"files\"") }
+ }
+
+ protected def processOptions(args: Seq[String]): Context = {
+ val initReporter = new DefaultReporter(Set())
+
+ val opts = args.filter(_.startsWith("--"))
+
+ val files = args.filterNot(_.startsWith("-")).map(new java.io.File(_))
+
+ val inoxOptions: Seq[OptionValue[_]] = opts.map { opt =>
+ val (name, value) = OptionsHelpers.nameValue(opt) getOrElse initReporter.fatalError(
+ s"Malformed option $opt. Options should have the form --name or --name=value"
+ )
+
+ // find respective OptionDef, or report an error
+ val df = options.keys.find(_.name == name) getOrElse initReporter.fatalError(
+ s"Unknown option: $name\nTry the --help option for more information."
+ )
+
+ df.parse(value)(initReporter)
+ }
+
+ val reporter = new DefaultReporter(
+ inoxOptions.collectFirst {
+ case OptionValue(`optDebug`, sections) => sections.asInstanceOf[Set[DebugSection]]
+ }.getOrElse(Set[DebugSection]())
+ )
+
+ reporter.whenDebug(DebugSectionOptions) { debug =>
+ debug("Options considered:")
+ for (io <- inoxOptions) debug(io.toString)
+ }
+
+ Context(
+ reporter = reporter,
+ options = Options(inoxOptions),
+ interruptManager = new utils.InterruptManager(reporter)
+ )
+ }
+
+ def exit(error: Boolean) = sys.exit(if (error) 1 else 0)
+
+ def setup(args: Array[String]): Context = {
+ val ctx = try {
+ processOptions(args.toList)
+ } catch {
+ case FatalError(msg) =>
+ exit(error = true)
+ }
+
+ ctx.interruptManager.registerSignalHandler()
+
+ ctx
+ }
+}
+
+object Main extends MainHelpers {
+
+ def main(args: Array[String]): Unit = {
+ val ctx = setup(args)
+
+ val files = ctx.options.findOptionOrDefault(optFiles)
+ if (files.isEmpty) {
+ ctx.reporter.fatalError(s"Input file was not specified.\nTry the --help option for more information.")
+ } else {
+ for (file <- files) {
+ val (syms, expr) = new tip.Parser(file).parseScript
+ val program = InoxProgram(ctx, syms)
+ import program._
+ import program.ctx._
+
+ import SolverResponses._
+ SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
+ case SatWithModel(model) =>
+ reporter.info(" => SAT")
+ for ((vd, res) <- model) {
+ reporter.info(f"${vd.asString}%-15s -> ${res.asString}")
+ }
+ exit(error = false)
+ case Unsat =>
+ reporter.info(" => UNSAT")
+ exit(error = false)
+ case Unknown =>
+ reporter.info(" => UNKNOWN")
+ exit(error = true)
+ }
+ }
+ }
+ }
+}
diff --git a/src/main/scala/inox/Options.scala b/src/main/scala/inox/Options.scala
index 2b06bd458..bce9b9cd1 100644
--- a/src/main/scala/inox/Options.scala
+++ b/src/main/scala/inox/Options.scala
@@ -7,9 +7,10 @@ import OptionParsers._
import scala.util.Try
import scala.reflect.ClassTag
+object DebugSectionOptions extends DebugSection("options")
+
abstract class OptionDef[A] {
val name: String
- val description: String
def default: A
val parser: OptionParser[A]
val usageRhs: String
@@ -19,10 +20,6 @@ abstract class OptionDef[A] {
else s"--$name=$usageRhs"
}
- def helpString = {
- f"$usageDesc%-28s" + description.replaceAll("\n", "\n" + " " * 28)
- }
-
private def parseValue(s: String)(implicit reporter: Reporter): A = {
parser(s).getOrElse(
reporter.fatalError(
@@ -40,7 +37,6 @@ abstract class OptionDef[A] {
def apply(value: A): OptionValue[A] = OptionValue(this)(value)
- // @mk: FIXME: Is this cool?
override def equals(other: Any) = other match {
case that: OptionDef[_] => this.name == that.name
case _ => false
@@ -49,20 +45,20 @@ abstract class OptionDef[A] {
override def hashCode = name.hashCode
}
-case class FlagOptionDef(name: String, description: String, default: Boolean) extends OptionDef[Boolean] {
+case class FlagOptionDef(name: String, default: Boolean) extends OptionDef[Boolean] {
val parser = booleanParser
val usageRhs = ""
}
-case class StringOptionDef(name: String, description: String, default: String, usageRhs: String) extends OptionDef[String] {
+case class StringOptionDef(name: String, default: String, usageRhs: String) extends OptionDef[String] {
val parser = stringParser
}
-case class LongOptionDef(name: String, description: String, default: Long, usageRhs: String) extends OptionDef[Long] {
+case class LongOptionDef(name: String, default: Long, usageRhs: String) extends OptionDef[Long] {
val parser = longParser
}
-case class IntOptionDef(name: String, description: String, default: Int, usageRhs: String) extends OptionDef[Int] {
+case class IntOptionDef(name: String, default: Int, usageRhs: String) extends OptionDef[Int] {
val parser = intParser
}
@@ -184,51 +180,11 @@ object Options {
def empty: Options = Options(Seq())
}
-object InoxOptions {
-
- val optSelectedSolvers = new OptionDef[Set[String]] {
- val name = "solvers"
- val description = "Use solvers s1, s2,...\n" +
- solvers.SolverFactory.solversPretty
- val default = Set("nativez3")
- val parser = setParser(stringParser)
- val usageRhs = "s1,s2,..."
- }
-
- val optDebug = new OptionDef[Set[DebugSection]] {
- import OptionParsers._
- val name = "debug"
- val description = {
- /*
- val sects = DebugSections.all.toSeq.map(_.name).sorted
- val (first, second) = sects.splitAt(sects.length/2 + 1)
- */
- "Enable detailed messages per component." /* +
- "\nAvailable:\n" +
- " " + first.mkString(", ") + ",\n" +
- " " + second.mkString(", ")*/
- }
- val default = Set[DebugSection]()
- val usageRhs = "d1,d2,..."
- private val debugParser: OptionParser[Set[DebugSection]] = s => {
- /*
- if (s == "all") {
- Some(DebugSections.all)
- } else {
- DebugSections.all.find(_.name == s).map(Set(_))
- }*/
- None
-
- }
- val parser: String => Option[Set[DebugSection]] = {
- setParser[Set[DebugSection]](debugParser)(_).map(_.flatten)
- }
- }
+object optTimeout extends LongOptionDef("timeout", 0L, "t")
- val optTimeout = LongOptionDef(
- "timeout",
- "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)",
- 0L,
- "t"
- )
+object optSelectedSolvers extends OptionDef[Set[String]] {
+ val name = "solvers"
+ val default = Set("nativez3")
+ val parser = setParser(stringParser)
+ val usageRhs = "s1,s2,..."
}
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 998527990..14a811659 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -7,9 +7,9 @@ import utils._
import org.apache.commons.lang3.StringEscapeUtils
import scala.language.implicitConversions
-object optPrintPositions extends FlagOptionDef("printpositions", "Attach positions to trees when printing", false)
-object optPrintUniqueIds extends FlagOptionDef("printids", "Always print unique ids", false)
-object optPrintTypes extends FlagOptionDef("printtypes", "Attach types to trees when printing", false)
+object optPrintPositions extends FlagOptionDef("printpositions", false)
+object optPrintUniqueIds extends FlagOptionDef("printids", false)
+object optPrintTypes extends FlagOptionDef("printtypes", false)
trait Printers {
self: Trees =>
diff --git a/src/main/scala/inox/evaluators/ContextualEvaluator.scala b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
index 3b4380a5f..cc58e8188 100644
--- a/src/main/scala/inox/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
@@ -3,8 +3,7 @@
package inox
package evaluators
-object optMaxCalls extends IntOptionDef("maxcalls",
- "Maximum number of function invocations allowed during evaluation", 50000, "<PosInt> | -1 (for unbounded")
+object optMaxCalls extends IntOptionDef("maxcalls", 50000, "<PosInt> | -1 (for unbounded")
trait ContextualEvaluator extends Evaluator {
import program._
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index 4283f2bfb..7dc2ee94a 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -3,14 +3,7 @@
package inox
package evaluators
-object EvaluatorOptions {
- val options = Seq(
- optIgnoreContracts
- )
-}
-
-object optIgnoreContracts extends FlagOptionDef(
- "ignorecontracts", "Don't fail on invalid contracts during evaluation", false)
+object optIgnoreContracts extends FlagOptionDef("ignorecontracts", false)
trait Evaluator {
val program: Program
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 1a720c78a..40ad462ce 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -14,10 +14,9 @@ trait SolvingEvaluator extends Evaluator {
import program.symbols._
private object optForallCache extends OptionDef[MutableMap[program.trees.Forall, Boolean]] {
- val parser = { (_: String) => throw FatalError("Unparsable option \"bankOption\"") }
- val name = "bank-option"
- val description = "Evaluation bank shared between solver and evaluator"
- val usageRhs = ""
+ val parser = { (_: String) => throw FatalError("Unparsable option \"forallCache\"") }
+ val name = "forall-cache"
+ val usageRhs = "No possible usage"
def default = MutableMap.empty
}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index ca04942d7..b90817b93 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -5,22 +5,8 @@ package solvers
import utils._
-object SolverOptions {
- val options = Seq(
- optCheckModels,
- optSilentErrors,
- unrolling.optUnrollFactor,
- unrolling.optFeelingLucky,
- unrolling.optUnrollAssumptions,
- smtlib.optCVC4Options
- )
-}
-
-object optCheckModels extends FlagOptionDef(
- "checkmodels", "Double-check counter-examples with evaluator", false)
-
-object optSilentErrors extends FlagOptionDef(
- "silenterrors", "Fail silently into UNKNOWN when encountering an error", false)
+object optCheckModels extends FlagOptionDef("checkmodels", false)
+object optSilentErrors extends FlagOptionDef("silenterrors", false)
case object DebugSectionSolver extends DebugSection("solver")
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index c02ac30a0..8f6610dca 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -113,10 +113,6 @@ object SolverFactory {
}
}
- val solversPretty = "Available: " + solverNames.toSeq.sortBy(_._1).map {
- case (name, desc) => f"\n $name%-14s : $desc"
- }
-
val solvers: Set[String] = solverNames.map(_._1).toSet
def apply(name: String, p: InoxProgram, opts: Options): SolverFactory {
@@ -127,7 +123,7 @@ object SolverFactory {
def apply(p: InoxProgram, opts: Options): SolverFactory {
val program: p.type
type S <: TimeoutSolver { val program: p.type }
- } = opts.findOptionOrDefault(InoxOptions.optSelectedSolvers).toSeq match {
+ } = opts.findOptionOrDefault(optSelectedSolvers).toSeq match {
case Seq() => throw FatalError("No selected solver")
case Seq(single) => apply(single, p, opts)
case multiple => PortfolioSolverFactory(p) {
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
index 428431877..092792f46 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
@@ -8,7 +8,6 @@ import inox.OptionParsers._
object optCVC4Options extends OptionDef[Set[String]] {
val name = "solver:cvc4"
- val description = "Pass extra arguments to CVC4"
val default = Set[String]()
val parser = setParser(stringParser)
val usageRhs = "<cvc4-opt>"
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
index 89d23a60d..37eaca9f6 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
@@ -21,7 +21,7 @@ trait SMTLIBDebugger extends SMTLIBTarget {
/* Printing VCs */
protected lazy val debugOut: Option[java.io.FileWriter] = {
if (ctx.reporter.isDebugEnabled) {
- val file = "" // TODO: real file name
+ val file = ctx.options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
val n = DebugFileNumbers.next(targetName + file)
val fileName = s"smt-sessions/$targetName-$file-$n.smt2"
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 9929f0e05..08f296e02 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -12,14 +12,9 @@ import combinators._
import scala.collection.mutable.{Map => MutableMap}
-object optUnrollFactor extends LongOptionDef(
- "unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
-
-object optFeelingLucky extends FlagOptionDef(
- "feelinglucky", "Use evaluator to find counter-examples early", false)
-
-object optUnrollAssumptions extends FlagOptionDef(
- "unrollassumptions", "Use unsat-assumptions to drive unfolding while remaining fair", false)
+object optUnrollFactor extends LongOptionDef("unrollfactor", default = 1, "<PosInt>")
+object optFeelingLucky extends FlagOptionDef("feelinglucky", false)
+object optUnrollAssumptions extends FlagOptionDef("unrollassumptions", false)
trait AbstractUnrollingSolver extends Solver { self =>
--
GitLab