From 6be834e8f71d8f099576df4b9ed237d64866e035 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 22 Nov 2011 18:33:22 -0800 Subject: Dafny: call C# compiler directly from inside Dafny, and optionally produce a .cs file with the new /spillTargetCode switch --- Source/Dafny/DafnyOptions.cs | 14 ++++++++++ Source/DafnyDriver/DafnyDriver.cs | 58 +++++++++++++++++++++++++++++++-------- Test/VSComp2010/Answer | 5 ---- Test/VSComp2010/runtest.bat | 4 +-- Test/VSI-Benchmarks/runtest.bat | 8 +----- Test/dafny1/runtest.bat | 8 +----- Test/dafny2/runtest.bat | 8 +----- Test/vacid0/runtest.bat | 8 +----- Test/vstte2012/runtest.bat | 8 +----- 9 files changed, 67 insertions(+), 54 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: + 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: 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(); + } } } } 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 ) -- cgit v1.2.3