Merge

2 files changed, 61 insertions, 11 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 745d50ef..4a1388d9 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -31,6 +31,7 @@ namespace Microsoft.Dafny
     public string DafnyPrintFile = null;

     public bool Compile = true;

     public bool ForceCompile = false;

+    public bool SpillTargetCode = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -51,12 +52,21 @@ namespace Microsoft.Dafny
         case "compile": {

             int compile = 0;

             if (ps.GetNumericArgument(ref compile, 3)) {

+              // convert option to two booleans

               Compile = compile == 1 || compile == 2;

               ForceCompile = compile == 2;

             }

             return true;

           }

 

+        case "spillTargetCode": {

+            int spill = 0;

+            if (ps.GetNumericArgument(ref spill, 2)) {

+              SpillTargetCode = spill != 0;  // convert to a boolean

+            }

+            return true;

+          }

+

         case "noCheating": {

             int cheat = 0; // 0 is default, allows cheating

             if (ps.GetNumericArgument(ref cheat, 2)) {

@@ -108,6 +118,10 @@ namespace Microsoft.Dafny
                     program, compile Dafny program to C# program out.cs

                 2 - always attempt to compile Dafny program to C# program

                     out.cs, regardless of verification outcome

+  /spillTargetCode:<n>

+                0 (default) - don't write the compiled Dafny program (but

+                    still compile it, if /compile indicates to do so)

+                1 - write the compiled Dafny program as a .cs file

   /noCheating:<n>

                 0 (default) - allow assume statements and free invariants

                 1 - treat all assumptions as asserts, and drop free.

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index eed5cf59..80e24356 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -21,6 +21,7 @@ namespace Microsoft.Dafny
   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics;

   using VC;

+  using System.CodeDom.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

 

   public class DafnyDriver

@@ -173,12 +174,12 @@ namespace Microsoft.Dafny
             case PipelineOutcome.VerificationCompleted:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

               if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)

-                CompileDafnyProgram(dafnyProgram);

+                CompileDafnyProgram(dafnyProgram, fileNames[0]);

               break;

             case PipelineOutcome.Done:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

               if (DafnyOptions.O.ForceCompile)

-                CompileDafnyProgram(dafnyProgram);

+                CompileDafnyProgram(dafnyProgram, fileNames[0]);

               break;

             default:

               // error has already been reported to user

@@ -190,17 +191,52 @@ namespace Microsoft.Dafny
       return exitValue;

     }

 

-    private static void CompileDafnyProgram(Dafny.Program dafnyProgram)

+    private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)

     {

-      string targetFilename = "out.cs";

-      using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {

-        Dafny.Compiler compiler = new Dafny.Compiler(target);

-        compiler.Compile(dafnyProgram);

-        if (compiler.ErrorCount == 0) {

-          Console.WriteLine("Compiled program written to {0}", targetFilename);

+      // Compile the Dafny program into a string that contains the C# program

+      StringWriter sw = new StringWriter();

+      Dafny.Compiler compiler = new Dafny.Compiler(sw);

+      compiler.Compile(dafnyProgram);

+      var csharpProgram = sw.ToString();

+      bool completeProgram = compiler.ErrorCount == 0;

+

+      // blurt out the code to a file

+      if (DafnyOptions.O.SpillTargetCode) {

+        string targetFilename = Path.ChangeExtension(dafnyProgramName, "cs");

+        using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {

+          target.Write(csharpProgram);

+          if (completeProgram) {

+            Console.WriteLine("Compiled program written to {0}", targetFilename);

+          } else {

+            Console.WriteLine("File {0} contains the partially compiled program", targetFilename);

+          }

         }

-        else {

-          Console.WriteLine("File {0} contains the partially compiled program", targetFilename);

+      }

+

+      // compile the program into an assembly

+      if (!completeProgram) {

+        // don't compile

+      } else if (!CodeDomProvider.IsDefinedLanguage("CSharp")) {

+        Console.WriteLine("Error: cannot compile, because there is no provider configured for input language CSharp");

+      } else {

+        var provider = CodeDomProvider.CreateProvider("CSharp");

+        var cp = new System.CodeDom.Compiler.CompilerParameters();

+        cp.GenerateExecutable = true;

+        // TODO: an improvement would be to generate a .dll if there is no Main method

+        cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");

+        cp.GenerateInMemory = false;

+        cp.ReferencedAssemblies.Add("System.Numerics.dll");

+        cp.CompilerOptions = "/debug";

+

+        var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);

+        if (cr.Errors.Count == 0) {

+          Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);

+        } else {

+          Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);

+          foreach (var ce in cr.Errors) {

+            Console.WriteLine(ce.ToString());

+            Console.WriteLine();

+          }

         }

       }

     }