Did some refactoring of the Dafny drivers.

1 files changed, 18 insertions, 104 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 3e95be92..bb223f54 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -22,6 +22,7 @@ namespace Microsoft.Dafny
   using System.Diagnostics;

   using VC;

   using System.CodeDom.Compiler;

+  using Core;

 

   public class DafnyDriver

   {

@@ -43,14 +44,14 @@ namespace Microsoft.Dafny
       }

       if (CommandLineOptions.Clo.Files.Count == 0)

       {

-        ErrorWriteLine("*** Error: No input files were specified.");

+        printer.ErrorWriteLine("*** Error: No input files were specified.");

         exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

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

         string errMsg = CommandLineOptions.Clo.XmlSink.Open();

         if (errMsg != null) {

-          ErrorWriteLine("*** Error: " + errMsg);

+          printer.ErrorWriteLine("*** Error: " + errMsg);

           exitValue = ExitValue.PREPROCESSING_ERROR;

           goto END;

         }

@@ -75,7 +76,7 @@ namespace Microsoft.Dafny
         if (extension != null) { extension = extension.ToLower(); }

         if (extension != ".dfy")

         {

-            ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file,

+            printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file,

                 extension == null ? "" : extension);

             exitValue = ExitValue.PREPROCESSING_ERROR;

             goto END;

@@ -106,7 +107,7 @@ namespace Microsoft.Dafny
         string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram);

         if (err != null) {

           exitValue = ExitValue.DAFNY_ERROR;

-          ErrorWriteLine(err);

+          printer.ErrorWriteLine(err);

         } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {

           Dafny.Translator translator = new Dafny.Translator();

           Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

@@ -129,12 +130,12 @@ namespace Microsoft.Dafny
           bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;

           switch (oc) {

             case PipelineOutcome.VerificationCompleted:

-              WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

+              printer.WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

               if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram, fileNames[0]);

               break;

             case PipelineOutcome.Done:

-              WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

+              printer.WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

               if (DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram, fileNames[0]);

               break;

@@ -202,7 +203,7 @@ namespace Microsoft.Dafny
             continue;

           }

         } catch (IOException e) {

-          ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

+          printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

           okay = false;

           continue;

         }

@@ -444,7 +445,7 @@ namespace Microsoft.Dafny
       }

       catch (ProverException e)

       {

-        ErrorWriteLine("Fatal Error: ProverException: {0}", e);

+        printer.ErrorWriteLine("Fatal Error: ProverException: {0}", e);

         return PipelineOutcome.FatalError;

       }

 

@@ -486,7 +487,7 @@ namespace Microsoft.Dafny
             }

             catch (UnexpectedProverOutputException upo)

             {

-                AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+                printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

                 errors = null;

                 outcome = VCGen.Outcome.Inconclusive;

             }

@@ -507,20 +508,20 @@ namespace Microsoft.Dafny
                 default:

                     Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome

                 case VCGen.Outcome.Correct:

-                    Inform(String.Format("{0}verified", timeIndication));

+                    printer.Inform(String.Format("{0}verified", timeIndication));

                     verified++;

                     break;

                 case VCGen.Outcome.TimedOut:

                     timeOuts++;

-                    Inform(String.Format("{0}timed out", timeIndication));

+                    printer.Inform(String.Format("{0}timed out", timeIndication));

                     break;

                 case VCGen.Outcome.OutOfMemory:

                     outOfMemories++;

-                    Inform(String.Format("{0}out of memory", timeIndication));

+                    printer.Inform(String.Format("{0}out of memory", timeIndication));

                     break;

                 case VCGen.Outcome.Inconclusive:

                     inconclusives++;

-                    Inform(String.Format("{0}inconclusive", timeIndication));

+                    printer.Inform(String.Format("{0}inconclusive", timeIndication));

                     break;

                 case VCGen.Outcome.Errors:

                     Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

@@ -645,7 +646,7 @@ namespace Microsoft.Dafny
               }

               if (cause == "Error")

               {

-                Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

+                printer.Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

               }

             }

 

@@ -669,95 +670,8 @@ namespace Microsoft.Dafny
 

 

     #region Output

-

-    // TODO(wuestholz): Use the following methods from the Boogie driver instead: ErrorWriteLine, AdvisoryWriteLine, Inform, WriteTrailer.

-

-    static void ErrorWriteLine(string s)

-    {

-      Contract.Requires(s != null);

-      if (!s.Contains("Error: ") && !s.Contains("Error BP"))

-      {

-        Console.WriteLine(s);

-        return;

-      }

-

-      // split the string up into its first line and the remaining lines

-      string remaining = null;

-      int i = s.IndexOf('\r');

-      if (0 <= i)

-      {

-        remaining = s.Substring(i + 1);

-        if (remaining.StartsWith("\n"))

-        {

-          remaining = remaining.Substring(1);

-        }

-        s = s.Substring(0, i);

-      }

-

-      ConsoleColor col = Console.ForegroundColor;

-      Console.ForegroundColor = ConsoleColor.Red;

-      Console.WriteLine(s);

-      Console.ForegroundColor = col;

-

-      if (remaining != null)

-      {

-        Console.WriteLine(remaining);

-      }

-    }

-

-

-    static void ErrorWriteLine(string format, params object[] args)

-    {

-      Contract.Requires(format != null);

-      Contract.Requires(args != null);

-      string s = string.Format(format, args);

-      ErrorWriteLine(s);

-    }

-

-

-    static void AdvisoryWriteLine(string format, params object[] args)

-    {

-      Contract.Requires(format != null);

-      ConsoleColor col = Console.ForegroundColor;

-      Console.ForegroundColor = ConsoleColor.Yellow;

-      Console.WriteLine(format, args);

-      Console.ForegroundColor = col;

-    }

-

-

-    /// <summary>

-    /// Inform the user about something and proceed with translation normally.

-    /// Print newline after the message.

-    /// </summary>

-    static void Inform(string s)

-    {

-      if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)

-      {

-        Console.WriteLine(s);

-      }

-    }

-

-

-    static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)

-    {

-      Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

-      Console.WriteLine();

-      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

-      if (inconclusives != 0)

-      {

-        Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

-      }

-      if (timeOuts != 0)

-      {

-        Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");

-      }

-      if (outOfMemories != 0)

-      {

-        Console.Write(", {0} out of memory", outOfMemories);

-      }

-      Console.WriteLine();

-      Console.Out.Flush();

-    }

+    

+    static OutputPrinter printer = new ConsolePrinter();

 

     #region Dafny output

 

@@ -792,7 +706,7 @@ namespace Microsoft.Dafny
       }

       if (error)

       {

-        ErrorWriteLine(s);

+        printer.ErrorWriteLine(s);

       }

       else

       {