Dafny: call C# compiler directly from inside Dafny, and optionally produce a .cs file with the new /spillTargetCode switch

9 files changed, 67 insertions, 54 deletions

diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs
index 745d50ef..4a1388d9 100644
--- a/Dafny/DafnyOptions.cs
+++ b/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/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs
index eed5cf59..80e24356 100644
--- a/DafnyDriver/DafnyDriver.cs
+++ b/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();

+          }

         }

       }

     }

diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index dc523fdf..9a083fa3 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -2,24 +2,19 @@
 -------------------- Problem1-SumMax.dfy --------------------

 

 Dafny program verifier finished with 4 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem2-Invert.dfy --------------------

 

 Dafny program verifier finished with 7 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem3-FindZero.dfy --------------------

 

 Dafny program verifier finished with 7 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem4-Queens.dfy --------------------

 

 Dafny program verifier finished with 9 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem5-DoubleEndedQueue.dfy --------------------

 

 Dafny program verifier finished with 21 verified, 0 errors

-Compiled program written to out.cs

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index e16eda13..9535d677 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -11,7 +11,5 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
             Problem5-DoubleEndedQueue.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% %* %%f

-

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a733a1c0..611f9251 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 15bd28a1..524765cf 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -26,11 +26,5 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             UltraFilter.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 50b4ca18..6c723ea5 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,11 +16,5 @@ for %%f in (
   ) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index 32c6a984..efe7b3d5 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 07b5859e..5145cb56 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -14,11 +14,5 @@ for %%f in (
   ) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )