Refactor the error reporting code

The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.

3 files changed, 31 insertions, 54 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 50d8c2e3..36664a9b 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -115,19 +115,21 @@ namespace DafnyLanguage
     bool ParseAndTypeCheck() {

       Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);

       Dafny.BuiltIns builtIns = new Dafny.BuiltIns();

-      Dafny.Errors parseErrors = new VSErrors(this);

+

+      var errorReporter = new VSErrorReporter(this);

+      var parseErrors = new Dafny.Errors(errorReporter);

+

       int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, _filename, module, builtIns, parseErrors);

       string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);

       if (errorCount != 0 || errString != null)

         return false;

-      Dafny.Program program = new Dafny.Program(_filename, module, builtIns);

+      Dafny.Program program = new Dafny.Program(_filename, module, builtIns, errorReporter);

 

-      var r = new VSResolver(program, this);

+      var r = new Resolver(program);

       r.ResolveProgram(program);

-      if (r.ErrorCount != 0)

+      if (errorReporter.Count(ErrorLevel.Error) != 0)

         return false;

 

-      program.AdditionalInformation.AddRange(r.AdditionalInformation);

       _program = program;

       return true;  // success

     }

@@ -137,56 +139,31 @@ namespace DafnyLanguage
       _errors.Add(new DafnyError(filename, line - 1, col - 1, cat, msg, _snapshot, isRecycled, null, System.IO.Path.GetFullPath(this._filename) == filename));

     }

 

-    class VSErrors : Dafny.Errors

-    {

-      DafnyDriver dd;

-      public VSErrors(DafnyDriver dd) {

-        this.dd = dd;

-      }

-      public override void SynErr(string filename, int line, int col, string msg) {

-        dd.RecordError(filename, line, col, ErrorCategory.ParseError, msg);

-        count++;

-      }

-      public override void SemErr(string filename, int line, int col, string msg) {

-        dd.RecordError(filename, line, col, ErrorCategory.ResolveError, msg);

-        count++;

-      }

-      public override void Warning(IToken tok, string msg) {

-        dd.RecordError(tok.filename, tok.line, tok.col, ErrorCategory.ParseWarning, msg);

-      }

-    }

-

-    class VSResolver : Dafny.Resolver

+    class VSErrorReporter : Dafny.ErrorReporter

     {

       DafnyDriver dd;

-      Dictionary<IToken, HashSet<AdditionalInformation>> _additionalInformation = new Dictionary<IToken, HashSet<AdditionalInformation>>();

-      public List<AdditionalInformation> AdditionalInformation { get { return _additionalInformation.Values.SelectMany(i => i).ToList(); } }

 

-      public VSResolver(Dafny.Program program, DafnyDriver dd)

-        : base(program) {

+      public VSErrorReporter(DafnyDriver dd) {

         this.dd = dd;

-

-        AdditionalInformationReporter =

-          (addinfo)

-            =>

-            {

-              if (!_additionalInformation.ContainsKey(addinfo.Token)) {

-                _additionalInformation.Add(addinfo.Token, new HashSet<AdditionalInformation>());

-              }

-              _additionalInformation[addinfo.Token].Add(addinfo);

-            };

-      }

-

-      public override void Error(Bpl.IToken tok, string msg, params object[] args) {

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

-        dd.RecordError(tok.filename, tok.line, tok.col, ErrorCategory.ResolveError, s);

-        ErrorCount++;

       }

 

-      public override void Warning(IToken tok, string msg, params object[] args) {

-        if (reportWarnings) {

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

-          dd.RecordError(tok.filename, tok.line, tok.col, ErrorCategory.ResolveWarning, s);

+      // TODO: The error tracking could be made better to track the full information returned by Dafny

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

+        if (base.Message(source, level, tok, msg)) {

+          switch (level) {

+            case ErrorLevel.Error:

+              dd.RecordError(tok.filename, tok.line, tok.col, source == MessageSource.Parser ? ErrorCategory.ParseError : ErrorCategory.ResolveError, msg);

+              break;

+            case ErrorLevel.Warning:

+              dd.RecordError(tok.filename, tok.line, tok.col, source == MessageSource.Parser ? ErrorCategory.ParseWarning : ErrorCategory.ResolveWarning, msg);

+              break;

+            case ErrorLevel.Info:

+              // The AllMessages variable already keeps track of this

+              break;

+          }

+          return true;

+        } else {

+          return false;

         }

       }

     }

@@ -273,7 +250,7 @@ namespace DafnyLanguage
     }

 

     public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {

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

+      Dafny.Translator translator = new Dafny.Translator(dafnyProgram.reporter);

       translator.InsertChecksums = true;

       translator.UniqueIdPrefix = uniqueIdPrefix;

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

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 262dddcd..13991496 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -136,9 +136,9 @@ namespace DafnyLanguage
 

       List<IdRegion> newRegions = new List<IdRegion>();

 

-      foreach (var addInfo in program.AdditionalInformation)

+      foreach (var info in program.reporter.AllMessages[ErrorLevel.Info])

       {

-        IdRegion.Add(newRegions, addInfo.Token, addInfo.Text, addInfo.Length);

+        IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length);

       }

 

       foreach (var module in program.Modules) {

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 6eaec5a6..0ce68809 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -74,10 +74,10 @@ namespace DafnyLanguage
       switch (err.Category) {

         case ErrorCategory.ProcessError:

         case ErrorCategory.ParseError:

-        case ErrorCategory.ParseWarning:

           return "syntax error";  // COLOR: red

         case ErrorCategory.ResolveError:

           return "compiler error";  // COLOR: blue

+        case ErrorCategory.ParseWarning:

         case ErrorCategory.ResolveWarning:

           return "compiler warning";  // COLOR: blue

         case ErrorCategory.InternalError:

@@ -403,7 +403,7 @@ namespace DafnyLanguage
         chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

     }

 

-    static TaskErrorCategory CategoryConversion(ErrorCategory cat)

+    static TaskErrorCategory CategoryConversion(ErrorCategory cat) //CLEMENT: We've lost that info

     {

       switch (cat)

       {