Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)

Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it
looks for one in Binaries/z3.exe (mostly for backwards-compatibility with
already set-up source installations).

7 files changed, 47 insertions, 18 deletions

diff --git a/Binaries/z3 b/Binaries/z3
deleted file mode 100755
index 7c60feb4..00000000
--- a/Binaries/z3
+++ /dev/null
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 1986ea6d..08e53d5c 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -9,8 +9,11 @@ namespace Microsoft.Dafny
 {

   public class DafnyOptions : Bpl.CommandLineOptions

   {

-    public DafnyOptions()

+    private ErrorReporter errorReporter;

+

+    public DafnyOptions(ErrorReporter errorReporter = null)

       : base("Dafny", "Dafny program verifier") {

+        this.errorReporter = errorReporter;

         SetZ3ExecutableName();

     }

 

@@ -257,13 +260,37 @@ namespace Microsoft.Dafny
       // TODO: provide attribute help here

     }

 

+    

+    /// <summary>

+    /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. 

+    /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.

+    /// For developers though (and people getting this from source), it's convenient to be able to run right away, 

+    /// so we vendor a Windows version.

+    /// </summary>

     private void SetZ3ExecutableName() {

       var platform = (int)System.Environment.OSVersion.Platform;

-      var isLinux = platform == 4 || platform ==  128; // http://www.mono-project.com/docs/faq/technical/

 

-      //TODO should we also vendor an OSX build?

-      var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

-      Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe");

+      // http://www.mono-project.com/docs/faq/technical/

+      var isUnix = platform == 4 || platform == 128;

+      

+      var z3binName = isUnix ? "z3" : "z3.exe";

+      var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

+      var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");

+      var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);

+

+      if (!System.IO.File.Exists(z3BinPath) && !isUnix) {

+        // This is most likely a Windows user running from source without downloading z3 

+        // separately; this is ok, since we vendor z3.exe.

+        z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);

+      }

+      

+      if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {

+        var tok = new Bpl.Token(1, 1) { filename = "*** " };

+        errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", 

+          z3binName, z3BinDir, System.Environment.NewLine);

+      } else {

+        Z3ExecutablePath = z3BinPath;

+      }

     }

 

     public override void Usage() {

diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
index 4cfbf20e..760392ca 100644
--- a/Source/Dafny/Reporting.cs
+++ b/Source/Dafny/Reporting.cs
@@ -143,7 +143,7 @@ namespace Microsoft.Dafny {
     }

 

     public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

-      if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) {

+      if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) {

         // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI

         msg = msg.Replace(Environment.NewLine, Environment.NewLine + " ");

 

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4b5ae8d8..c45d66fc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -40,10 +40,11 @@ namespace Microsoft.Dafny
     public static int ThreadMain(string[] args)

     {

       Contract.Requires(cce.NonNullElements(args));

-         

+

+      ErrorReporter reporter = new ConsoleErrorReporter();

       ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors

 

-      DafnyOptions.Install(new DafnyOptions());

+      DafnyOptions.Install(new DafnyOptions(reporter));

 

       ExitValue exitValue = ExitValue.VERIFIED;

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

@@ -92,7 +93,7 @@ namespace Microsoft.Dafny
           goto END;

         }

       }

-      exitValue = ProcessFiles(CommandLineOptions.Clo.Files);

+      exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter);

 

       END:

         if (CommandLineOptions.Clo.XmlSink != null) {

@@ -112,7 +113,7 @@ namespace Microsoft.Dafny
     }

 

 

-    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)

+    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

 

@@ -128,7 +129,7 @@ namespace Microsoft.Dafny
         {

           Console.WriteLine();

           Console.WriteLine("-------------------- {0} --------------------", f);

-          var ev = ProcessFiles(new List<string> { f }, lookForSnapshots, f);

+          var ev = ProcessFiles(new List<string> { f }, reporter, lookForSnapshots, f);

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -142,7 +143,7 @@ namespace Microsoft.Dafny
         var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);

         foreach (var s in snapshotsByVersion)

         {

-          var ev = ProcessFiles(new List<string>(s), false, programId);

+          var ev = ProcessFiles(new List<string>(s), reporter, false, programId);

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -153,7 +154,6 @@ namespace Microsoft.Dafny
       

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {

         Dafny.Program dafnyProgram;

-        ErrorReporter reporter = new ConsoleErrorReporter();

         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";

         string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram);

         if (err != null) {

diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
index 3204fdb3..e54e2b48 100644
--- a/Source/DafnyServer/DafnyHelper.cs
+++ b/Source/DafnyServer/DafnyHelper.cs
@@ -29,18 +29,21 @@ namespace Microsoft.Dafny {
   class DafnyHelper {

     private string fname;

     private string source;

+    private string[] args;

 

     private readonly Dafny.ErrorReporter reporter;

     private Dafny.Program dafnyProgram;

     private Bpl.Program boogieProgram;

 

-    public DafnyHelper(string fname, string source) {

+    public DafnyHelper(string[] args, string fname, string source) {

+      this.args = args;

       this.fname = fname;

       this.source = source;

       this.reporter = new Dafny.ConsoleErrorReporter();

     }

 

     public bool Verify() {

+      ServerUtils.ApplyArgs(args, reporter);

       return Parse() && Resolve() && Translate() && Boogie();

     }

 

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 59b3abb9..5e2c6f96 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -43,8 +43,8 @@ namespace Microsoft.Dafny {
       }

     }

 

-    internal static void ApplyArgs(string[] args) {

-      Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

+    internal static void ApplyArgs(string[] args, ErrorReporter reporter) {

+      Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter));

       Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden

 

       if (CommandLineOptions.Clo.Parse(args)) {

diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index a00688b1..eb740e70 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -52,8 +52,7 @@ namespace Microsoft.Dafny {
     }

 

     internal void Run() {

-      ServerUtils.ApplyArgs(args);

-      new DafnyHelper(filename, ProgramSource).Verify();

+      new DafnyHelper(args, filename, ProgramSource).Verify();

     }

   }

 }