diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 9cc0dc9c6af811444024a05dd95b93c518df31eb..f238d4a854bd881c74a3205ef5b727a220e34ae1 100644
--- a/src/main/scala/leon/Main.scala
+++ b/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
}
diff --git a/src/main/scala/leon/genc/CFileOutputPhase.scala b/src/main/scala/leon/genc/CFileOutputPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2b7797183da17ccb6e326a85a779a4ef58be9e2
--- /dev/null
+++ b/src/main/scala/leon/genc/CFileOutputPhase.scala
@@ -0,0 +1,54 @@
+/* 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)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/genc/GenerateCPhase.scala b/src/main/scala/leon/genc/GenerateCPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c30d32274db7370a8f9af5616df3cbe505b0389e
--- /dev/null
+++ b/src/main/scala/leon/genc/GenerateCPhase.scala
@@ -0,0 +1,20 @@
+/* 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
+ }
+
+}
+
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index a0b790243a6dc309953d07ba02d504e463185880..b3133d700fed92bb500423201dc4288832b07319 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/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
)
}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 4a395912a6b9dc92a9828fc90bed421baf009c97..06f35dc3a47df0a48836e6137eaae96218745d39 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/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)