From 0cac24caff23fe5db0b12c57b128684afd727044 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 3 Jun 2013 14:52:17 -0700 Subject: Did some refactoring of the Dafny drivers. --- Source/DafnyDriver/DafnyDriver.cs | 122 ++++++-------------------------------- 1 file changed, 18 insertions(+), 104 deletions(-) (limited to 'Source/DafnyDriver/DafnyDriver.cs') 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; - } - - - /// - /// Inform the user about something and proceed with translation normally. - /// Print newline after the message. - /// - 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 { -- cgit v1.2.3