summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-11-22 23:56:31 -0800
committerGravatar qadeer <qadeer@microsoft.com>2011-11-22 23:56:31 -0800
commit01c3e8e8045cfa8a2b5f0746897441ebf027749d (patch)
treefe4121725d31e6dec11de890e49cdf057dc92dbf /Source
parent0fdcd28a14d89fd878f334ad3d80f42363760fc5 (diff)
parent58c58e5833cbbfdd29df72f643025c01f080dde9 (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/DafnyOptions.cs14
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs58
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();
+ }
}
}
}