Update Leon's main function & command line options to generate C code

src/main/scala/leon/Main.scala

@@ -27,7 +27,9 @@ object Main {
       solvers.isabelle.AdaptationPhase,
       solvers.isabelle.IsabellePhase,
       transformations.InstrumentationPhase,
-      invariant.engine.InferInvariantsPhase)
+      invariant.engine.InferInvariantsPhase,
+      genc.GenerateCPhase,
+      genc.CFileOutputPhase)
   }
 
   // Add whatever you need here.
@@ -53,9 +55,10 @@ object Main {
     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 optGenc        = LeonFlagOptionDef("genc",        "Generate C code",                                           false)
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
-      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv)
+      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optGenc)
   }
 
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
@@ -151,6 +154,8 @@ object Main {
     import repair.RepairPhase
     import evaluators.EvaluationPhase
     import solvers.isabelle.IsabellePhase
+    import genc.GenerateCPhase
+    import genc.CFileOutputPhase
     import MainComponent._
     import invariant.engine.InferInvariantsPhase
     import transformations.InstrumentationPhase
@@ -163,11 +168,17 @@ object Main {
     val isabelleF    = ctx.findOptionOrDefault(optIsabelle)
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
+    val gencF        = ctx.findOptionOrDefault(optGenc)
     val evalF        = ctx.findOption(optEval).isDefined
     val inferInvF    = ctx.findOptionOrDefault(optInferInv)
     val instrumentF  = ctx.findOptionOrDefault(optInstrument)
     val analysisF    = verifyF && terminationF
 
+    // Check consistency in options
+    if (gencF && !xlangF) {
+      ctx.reporter.fatalError("Generating C code with --genc requires --xlang")
+    }
+
     if (helpF) {
       displayVersion(ctx.reporter)
       displayHelp(ctx.reporter, error = false)
@@ -175,7 +186,7 @@ object Main {
       val pipeBegin: Pipeline[List[String], Program] =
         ClassgenPhase andThen
         ExtractionPhase andThen
-        new PreprocessingPhase(xlangF)
+        new PreprocessingPhase(xlangF, gencF)
 
       val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
 
@@ -189,6 +200,7 @@ object Main {
         else if (evalF) EvaluationPhase
         else if (inferInvF) InferInvariantsPhase
         else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
+        else if (gencF) GenerateCPhase andThen CFileOutputPhase
         else verification
       }
 

src/main/scala/leon/genc/CFileOutputPhase.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+
+object CFileOutputPhase extends UnitPhase[CAST.Prog] {
+
+  val name = "C File Output"
+  val description = "Output converted C program to the specified file (default leon.c)"
+
+  val optOutputFile = new LeonOptionDef[String] {
+    val name = "o"
+    val description = "Output file"
+    val default = "leon.c"
+    val usageRhs = "file"
+    val parser = OptionParsers.stringParser
+  }
+
+  override val definedOptions: Set[LeonOptionDef[Any]] = Set(optOutputFile)
+
+  def apply(ctx: LeonContext, program: CAST.Prog) {
+    // Get the output file name from command line options, or use default
+    val outputFile = new File(ctx.findOptionOrDefault(optOutputFile))
+    val parent = outputFile.getParentFile()
+    try {
+      if (parent != null) {
+        parent.mkdirs()
+      }
+    } catch {
+      case _ : java.io.IOException => ctx.reporter.fatalError("Could not create directory " + parent)
+    }
+
+    // Output C code to the file
+    try {
+      val fstream = new FileWriter(outputFile)
+      val out = new BufferedWriter(fstream)
+
+      val p = new CPrinter
+      p.print(program)
+
+      out.write(p.toString)
+      out.close()
+
+      ctx.reporter.info(s"Output written to $outputFile")
+    } catch {
+      case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
+    }
+  }
+
+}

src/main/scala/leon/genc/GenerateCPhase.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import purescala.Definitions.Program
+
+object GenerateCPhase extends SimpleLeonPhase[Program, CAST.Prog] {
+
+  val name = "Generate C"
+  val description = "Generate equivalent C code from Leon's AST"
+
+  def apply(ctx: LeonContext, program: Program) = {
+    ctx.reporter.debug("Running code conversion phase: " + name)(utils.DebugSectionLeon)
+    val cprogram = new CConverter(ctx, program).convert
+    cprogram
+  }
+
+}
+

src/main/scala/leon/utils/DebugSections.scala

@@ -24,6 +24,7 @@ case object DebugSectionXLang        extends DebugSection("xlang",        1 << 1
 case object DebugSectionTypes        extends DebugSection("types",        1 << 13)
 case object DebugSectionIsabelle     extends DebugSection("isabelle",     1 << 14)
 case object DebugSectionReport       extends DebugSection("report",       1 << 15)
+case object DebugSectionGenC         extends DebugSection("genc",         1 << 16)
 
 object DebugSections {
   val all = Set[DebugSection](
@@ -42,6 +43,7 @@ object DebugSections {
     DebugSectionXLang,
     DebugSectionTypes,
     DebugSectionIsabelle,
-    DebugSectionReport
+    DebugSectionReport,
+    DebugSectionGenC
   )
 }

src/main/scala/leon/utils/PreprocessingPhase.scala

@@ -9,7 +9,7 @@ import leon.solvers.isabelle.AdaptationPhase
 import leon.verification.InjectAsserts
 import leon.xlang.{NoXLangFeaturesChecking, XLangDesugaringPhase}
 
-class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
+class PreprocessingPhase(desugarXLang: Boolean = false, genc: Boolean = false) extends LeonPhase[Program, Program] {
 
   val name = "preprocessing"
   val description = "Various preprocessings on Leon programs"
@@ -39,19 +39,27 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
       CheckADTFieldsTypes                    andThen
       InliningPhase
 
-    val pipeX = if(desugarXLang) {
+    val pipeX = if (!genc && desugarXLang) {
+      // Do not desugar when generating C code
       XLangDesugaringPhase andThen
       debugTrees("Program after xlang desugaring")
     } else {
       NoopPhase[Program]()
     }
 
+    def pipeEnd = if (genc) {
+      // No InjectAsserts, FunctionClosure and AdaptationPhase phases
+      NoopPhase[Program]()
+    } else {
+      InjectAsserts  andThen
+      FunctionClosure andThen
+      AdaptationPhase
+    }
+
     val phases =
       pipeBegin andThen
       pipeX andThen
-      InjectAsserts andThen
-      FunctionClosure andThen
-      AdaptationPhase andThen
+      pipeEnd andThen
       debugTrees("Program after pre-processing")
 
     phases.run(ctx, p)