diff options
-rw-r--r-- | Source/Dafny/DafnyOptions.cs | 14 | ||||
-rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 58 | ||||
-rw-r--r-- | Test/VSComp2010/Answer | 5 | ||||
-rw-r--r-- | Test/VSComp2010/runtest.bat | 4 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/runtest.bat | 8 | ||||
-rw-r--r-- | Test/dafny1/runtest.bat | 8 | ||||
-rw-r--r-- | Test/dafny2/runtest.bat | 8 | ||||
-rw-r--r-- | Test/vacid0/runtest.bat | 8 | ||||
-rw-r--r-- | Test/vstte2012/runtest.bat | 8 | ||||
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 2 | ||||
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj | 19 |
11 files changed, 81 insertions, 61 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();
+ }
}
}
}
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
)
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 19a5e1df..31cc412e 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -167,7 +167,7 @@ namespace DafnyLanguage : base(program) {
this.dd = dd;
}
- protected override void Error(IToken tok, string msg, params object[] args) {
+ protected override void Error(Bpl.IToken tok, string msg, params object[] args) {
string s = string.Format(msg, args);
dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
ErrorCount++;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index 4ae02e17..cf33e5a0 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -57,21 +57,28 @@ <SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\DafnyPipeline.dll</HintPath>
</Reference>
- <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\Binaries\FSharp.Core.dll</HintPath>
+ <Reference Include="Graph">
+ <HintPath>..\..\..\..\Binaries\Graph.dll</HintPath>
</Reference>
- <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\Binaries\FSharp.PowerPack.dll</HintPath>
+ <Reference Include="Houdini">
+ <HintPath>..\..\..\..\Binaries\Houdini.dll</HintPath>
</Reference>
<Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
</Reference>
+ <Reference Include="Model">
+ <HintPath>..\..\..\..\Binaries\Model.dll</HintPath>
+ </Reference>
+ <Reference Include="ParserHelper">
+ <HintPath>..\..\..\..\Binaries\ParserHelper.dll</HintPath>
+ </Reference>
<Reference Include="Provers.Z3">
<HintPath>..\..\..\..\Binaries\Provers.Z3.dll</HintPath>
</Reference>
+ <Reference Include="VCExpr">
+ <HintPath>..\..\..\..\Binaries\VCExpr.dll</HintPath>
+ </Reference>
<Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>
|