added -optimize option to compiler.

2 files changed, 24 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index a6827d5f..125ab11e 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -55,6 +55,7 @@ namespace Microsoft.Dafny
     public bool ignoreAutoReq = false;

     public bool AllowGlobals = false;

     public bool CountVerificationErrors = true;

+    public bool Optimize = false;

 

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

       var args = ps.args;  // convenient synonym

@@ -180,6 +181,11 @@ namespace Microsoft.Dafny
           return true;

         }

 

+        case "optimize": {

+            Optimize = true;

+            return true;

+        }

+

         default:

           break;

       }

@@ -270,6 +276,12 @@ namespace Microsoft.Dafny
                     of verification errors.

                 1 (default) - If preprocessing succeeds, set exit code to the number of

                               verification errors.

+  /optimize     Produce optimized C# code, meaning:

+                  - selects optimized C# prelude by passing 

+                    /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires 

+                    System.Collections.Immutable.dll in the source directory to successfully 

+                    compile).

+                  - passes /optimize flag to csc.exe.

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index a769b829..cf464754 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -15,6 +15,8 @@ namespace Microsoft.Dafny
   using System.Collections.Generic;

   using System.Diagnostics.Contracts;

   using System.IO;

+  using System.Reflection;

+

   using Microsoft.Boogie;

   using Bpl = Microsoft.Boogie;

 

@@ -330,7 +332,7 @@ namespace Microsoft.Dafny
       }

       else

       {

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

+        var provider = CodeDomProvider.CreateProvider("CSharp", new Dictionary<string, string> { { "CompilerVersion", "v4.0" } });

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

         cp.GenerateExecutable = hasMain;

         if (DafnyOptions.O.RunAfterCompile) {

@@ -344,6 +346,15 @@ namespace Microsoft.Dafny
         }

         cp.CompilerOptions = "/debug /nowarn:0164 /nowarn:0219";  // warning CS0164 complains about unreferenced labels, CS0219 is about unused variables

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

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

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

+

+        if (DafnyOptions.O.Optimize) {

+          var libPath = Path.GetDirectoryName(dafnyProgramName);

+          cp.CompilerOptions += string.Format(" /optimize /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE /lib:{0}", libPath);

+          cp.ReferencedAssemblies.Add("System.Collections.Immutable.dll");

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

+        }

 

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

         var assemblyName = Path.GetFileName(cr.PathToAssembly);