Skip to content
Snippets Groups Projects
Main.scala 10.10 KiB
/* Copyright 2009-2016 EPFL, Lausanne */

package leon

import leon.utils._

object Main {

  lazy val allPhases: List[LeonPhase[_, _]] = {
    List(
      frontends.scalac.ExtractionPhase,
      frontends.scalac.ClassgenPhase,
      utils.TypingPhase,
      utils.FileOutputPhase,
      purescala.RestoreMethods,
      xlang.AntiAliasingPhase,
      xlang.EpsilonElimination,
      xlang.ImperativeCodeElimination,
      xlang.FixReportLabels,
      xlang.XLangDesugaringPhase,
      purescala.FunctionClosure,
      synthesis.SynthesisPhase,
      termination.TerminationPhase,
      verification.VerificationPhase,
      repair.RepairPhase,
      evaluators.EvaluationPhase,
      solvers.isabelle.AdaptationPhase,
      solvers.isabelle.IsabellePhase,
      transformations.InstrumentationPhase,
      invariant.engine.InferInvariantsPhase,
      laziness.LazinessEliminationPhase,
      genc.GenerateCPhase,
      genc.CFileOutputPhase
    )
  }

  // Add whatever you need here.
  lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
    solvers.unrolling.UnrollingProcedure, MainComponent, GlobalOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
  )

  /*
   * 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 = "Selection of Leon functionality. Default: verify"

    val optEval        = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default: evaluation)", "default", "[codegen|default]")
    val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify",     false)
    val optRepair      = LeonFlagOptionDef("repair",      "Repair selected functions",                                 false)
    val optSynthesis   = LeonFlagOptionDef("synthesis",   "Partial synthesis of choose() constructs",                  false)
    val optIsabelle    = LeonFlagOptionDef("isabelle",    "Run Isabelle verification",                                 false)
    val optNoop        = LeonFlagOptionDef("noop",        "No operation performed, just output program",               false)
    val optVerify      = LeonFlagOptionDef("verify",      "Verify function contracts",                                 false)
    val optHelp        = LeonFlagOptionDef("help",        "Show help message",                                         false)
    val optInstrument  = LeonFlagOptionDef("instrument",  "Instrument the code for inferring time/depth/stack bounds", false)
    val optInferInv    = LeonFlagOptionDef("inferInv",    "Infer invariants from (instrumented) the code",             false)
    val optLazyEval    = LeonFlagOptionDef("lazy",        "Handles programs that may use the 'lazy' construct",        false)
    val optGenc        = LeonFlagOptionDef("genc",        "Generate C code",                                           false)

    override val definedOptions: Set[LeonOptionDef[Any]] =
      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc)
  }

  lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)

  def displayHelp(reporter: Reporter, error: Boolean) = {