DafnyExtension: Made it display verification errors incrementally.

5 files changed, 137 insertions, 66 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index b740e5cf..7ad2045b 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -196,12 +196,14 @@ namespace DafnyLanguage
       return Dafny.DafnyOptions.Clo.VerifySnapshots;

     }

 

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

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

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

       translator.InsertChecksums = true;

       translator.UniqueIdPrefix = uniqueIdPrefix;

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

 

+      resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations);

+

       PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er);

       switch (oc) {

         case PipelineOutcome.Done:

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 86fb2696..49c7bb01 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -107,8 +107,8 @@ namespace DafnyLanguage
         ITextSnapshot snap;

         Microsoft.Dafny.Program prog;

         lock (this) {

-          snap = r._snapshot;

-          prog = r._program;

+          snap = r.Snapshot;

+          prog = r.Program;

         }

         if (prog != null) {

           if (!ComputeIdentifierRegions(prog, snap))

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 0e7d1f1d..99611db8 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -97,8 +97,8 @@ namespace DafnyLanguage
         ITextSnapshot snap;

         Microsoft.Dafny.Program prog;

         lock (this) {

-          snap = r._snapshot;

-          prog = r._program;

+          snap = r.Snapshot;

+          prog = r.Program;

         }

         if (prog != null) {

           if (!ComputeOutliningRegions(prog, snap))

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 12099293..597f3143 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -188,19 +188,26 @@ namespace DafnyLanguage
     /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method.

     /// </summary>

     public void UponIdle(object sender, EventArgs args) {

-      Dafny.Program prog;

-      ITextSnapshot snap;

+      if (resolver != null)

+      {

+        resolver.UpdateErrorList(resolver.Snapshot);

+      }

+

       lock (this) {

         if (verificationInProgress) {

           // This UponIdle message came at an inopportune time--we've already kicked off a verification.

           // Just back off.

+          

           return;

         }

 

         if (resolver == null) return;

+        

+        Dafny.Program prog;

+        ITextSnapshot snap;

         lock (resolver) {

-          prog = resolver._program;

-          snap = resolver._snapshot;

+          prog = resolver.Program;

+          snap = resolver.Snapshot;

         }

         if (prog == null || verificationDisabled) return;

         // We have a successfully resolved program to verify

@@ -286,7 +293,6 @@ namespace DafnyLanguage
       }

     }

 

-

     /// <summary>

     /// Thread entry point.

     /// </summary>

@@ -297,35 +303,32 @@ namespace DafnyLanguage
       Contract.Requires(errorListHolder != null);

 

       // Run the verifier

-      var newErrors = new List<DafnyError>();

       try

       {

-        bool success = DafnyDriver.Verify(program, GetHashCode().ToString(), requestId, errorInfo =>

+        bool success = DafnyDriver.Verify(program, errorListHolder, GetHashCode().ToString(), requestId, errorInfo =>

         {

           errorInfo.BoogieErrorCode = null;

           if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))

           {

             var s = RequestIdToSnapshot[errorInfo.RequestId];

-            newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s));

+            errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s), errorInfo.ImplementationName, requestId);

             foreach (var aux in errorInfo.Aux)

             {

-              newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s));

+              errorListHolder.AddError(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s), errorInfo.ImplementationName, requestId);

             }

           }

+          // errorListHolder.UpdateErrorList(snapshot);

         });

         if (!success)

         {

-          newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error", snapshot));

+          errorListHolder.AddError(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error", snapshot), "$$program$$", requestId);

         }

       }

       catch (Exception e)

       {

-        newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot));

+        errorListHolder.AddError(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot), "$$program$$", requestId);

       }

 

-      errorListHolder.VerificationErrors = newErrors;

-      errorListHolder.UpdateErrorList(snapshot);

-

       lock (this) {

         bufferChangesPreVerificationStart.Clear();

         verificationInProgress = false;

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 349bc09f..54e29070 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -38,7 +38,8 @@ namespace DafnyLanguage
     [Import]

     ITextDocumentFactoryService _textDocumentFactory = null;

 

-    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag

+    {

       // create a single tagger for each buffer.

       Func<ITagger<T>> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger<T>; };

       return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);

@@ -60,7 +61,8 @@ namespace DafnyLanguage
   {

     public readonly string Typ;

     public readonly string Msg;

-    public DafnyErrorResolverTag(string typ, string msg) {

+    public DafnyErrorResolverTag(string typ, string msg)

+    {

       Typ = typ;

       Msg = msg;

     }

@@ -69,7 +71,8 @@ namespace DafnyLanguage
   public class DafnySuccessResolverTag : DafnyResolverTag

   {

     public readonly Dafny.Program Program;

-    public DafnySuccessResolverTag(Dafny.Program program) {

+    public DafnySuccessResolverTag(Dafny.Program program)

+    {

       Program = program;

     }

   }

@@ -86,24 +89,66 @@ namespace DafnyLanguage
     readonly ITextDocument _document;

     readonly ErrorListProvider _errorProvider;

 

-    // The _snapshot and _program fields should be updated and read together, so they are protected by "this"

-    public ITextSnapshot _snapshot;  // may be null

-    public Dafny.Program _program;  // non-null only if the snapshot contains a Dafny program that type checks

+    // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"

+    public ITextSnapshot Snapshot;  // may be null

+    public Dafny.Program Program;  // non-null only if the snapshot contains a Dafny program that type checks

 

     List<DafnyError> _resolutionErrors = new List<DafnyError>();  // if nonempty, then _snapshot is the snapshot from which the errors were produced

 

-    List<DafnyError> _verificationErrors = new List<DafnyError>();

-    public List<DafnyError> VerificationErrors

+    internal void AddError(DafnyError error, string unitId, string requestId)

     {

-      get

+      ErrorContainer entry;

+      if (_verificationErrors.TryGetValue(unitId, out entry))

       {

-        return _verificationErrors;

+        lock (entry)

+        {

+          if (entry.RequestId == null || new DateTime(long.Parse(entry.RequestId)) < new DateTime(long.Parse(requestId)))

+          {

+            entry.Errors.Clear();

+            entry.RequestId = requestId;

+          }

+        }

+        entry.Errors.Push(error);

       }

-      set

+    }

+

+    string MostRecentRequestId;

+    

+    internal void ReInitializeVerificationErrors(string mostRecentRequestId, List<Microsoft.Boogie.Declaration> units)

+    {

+      var implNames = units.OfType<Microsoft.Boogie.Implementation>().Select(impl => impl.Name);

+      lock (this)

       {

-        Contract.Requires(value != null);

+        MostRecentRequestId = mostRecentRequestId;

+        var outOfDatekeys = _verificationErrors.Keys.Except(implNames);

+        foreach (var key in outOfDatekeys)

+        {

+          ErrorContainer oldError;

+          _verificationErrors.TryRemove(key, out oldError);

+        }

 

-        _verificationErrors = value;

+        var newKeys = implNames.Except(_verificationErrors.Keys).ToList();

+        newKeys.Add("$$program$$");

+        foreach (var key in newKeys)

+        {

+          _verificationErrors.TryAdd(key, new ErrorContainer());

+        }

+      }

+    }

+

+    public class ErrorContainer

+    {

+      internal string RequestId;

+      internal ConcurrentStack<DafnyError> Errors = new ConcurrentStack<DafnyError>();

+    }

+

+    public readonly ConcurrentDictionary<string, ErrorContainer> _verificationErrors = new ConcurrentDictionary<string, ErrorContainer>();

+

+    public IEnumerable<DafnyError> VerificationErrors

+    {

+      get

+      {

+        return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors);

       }

     }

 

@@ -127,11 +172,12 @@ namespace DafnyLanguage
 

     public static readonly IDictionary<string, Dafny.Program> Programs = new ConcurrentDictionary<string, Dafny.Program>();

 

-    internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {

+    internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory)

+    {

       _buffer = buffer;

       if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))

         _document = null;

-      _snapshot = null;  // this makes sure the next snapshot will look different

+      Snapshot = null;  // this makes sure the next snapshot will look different

       _errorProvider = new ErrorListProvider(serviceProvider);

 

       BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);

@@ -171,14 +217,18 @@ namespace DafnyLanguage
     /// <summary>

     /// Find the Error tokens in the set of all tokens and create an ErrorTag for each

     /// </summary>

-    public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

+    public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans)

+    {

       if (spans.Count == 0) yield break;

       var currentSnapshot = spans[0].Snapshot;

-      foreach (var err in AllErrors) {

-        if (err.Category != ErrorCategory.ProcessError) {

+      foreach (var err in AllErrors)

+      {

+        if (err.Category != ErrorCategory.ProcessError)

+        {

           var span = err.Span.TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

           string ty;  // the COLORs below indicate what I see on my machine

-          switch (err.Category) {

+          switch (err.Category)

+          {

             default:  // unexpected category

             case ErrorCategory.ParseError:

             case ErrorCategory.ParseWarning:

@@ -198,11 +248,13 @@ namespace DafnyLanguage
 

       ITextSnapshot snap;

       Dafny.Program prog;

-      lock (this) {

-        snap = _snapshot;

-        prog = _program;

+      lock (this)

+      {

+        snap = Snapshot;

+        prog = Program;

       }

-      if (prog != null) {

+      if (prog != null)

+      {

         yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));

       }

     }

@@ -213,25 +265,30 @@ namespace DafnyLanguage
     /// <summary>

     /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.

     /// </summary>

-    void ResolveBuffer(object sender, EventArgs args) {

+    void ResolveBuffer(object sender, EventArgs args)

+    {

       ITextSnapshot snapshot = _buffer.CurrentSnapshot;

-      if (snapshot == _snapshot)

+      if (snapshot == Snapshot)

         return;  // we've already done this snapshot

 

       var driver = new DafnyDriver(snapshot, _document != null ? _document.FilePath : "<program>");

       List<DafnyError> newErrors;

       Dafny.Program program;

-      try {

+      try

+      {

         program = driver.ProcessResolution();

         newErrors = driver.Errors;

-      } catch (Exception e) {

+      }

+      catch (Exception e)

+      {

         newErrors = new List<DafnyError> { new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) };

         program = null;

       }

 

-      lock (this) {

-        _snapshot = snapshot;

-        _program = program;

+      lock (this)

+      {

+        Snapshot = snapshot;

+        Program = program;

       }

 

       if (program != null && _document != null)

@@ -244,28 +301,34 @@ namespace DafnyLanguage
       }

 

       _resolutionErrors = newErrors;

+

       UpdateErrorList(snapshot);

     }

 

-    public void UpdateErrorList(ITextSnapshot snapshot) {

+    public void UpdateErrorList(ITextSnapshot snapshot)

+    {

       _errorProvider.SuspendRefresh();  // reduce flickering

       _errorProvider.Tasks.Clear();

-      foreach (var err in AllErrors) {

-        var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive);

+      foreach (var err in AllErrors)

+      {

+        var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeInclusive);

         var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

         var line = snapshot.GetLineFromPosition(span.Start.Position);

         var columnNum = span.Start - line.Start;

-        ErrorTask task = new ErrorTask() {

+        ErrorTask task = new ErrorTask()

+        {

           Category = TaskCategory.BuildCompile,

           ErrorCategory = CategoryConversion(err.Category),

           Text = err.Message,

           Line = lineNum,

           Column = columnNum

         };

-        if (_document != null) {

+        if (_document != null)

+        {

           task.Document = _document.FilePath;

         }

-        if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) {

+        if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

+        {

           task.Navigate += new EventHandler(NavigateHandler);

         }

         _errorProvider.Tasks.Add(task);

@@ -276,8 +339,10 @@ namespace DafnyLanguage
         chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

     }

 

-    static TaskErrorCategory CategoryConversion(ErrorCategory cat) {

-      switch (cat) {

+    static TaskErrorCategory CategoryConversion(ErrorCategory cat)

+    {

+      switch (cat)

+      {

         case ErrorCategory.ParseError:

         case ErrorCategory.ResolveError:

         case ErrorCategory.VerificationError:

@@ -293,7 +358,8 @@ namespace DafnyLanguage
       }

     }

 

-    void NavigateHandler(object sender, EventArgs arguments) {

+    void NavigateHandler(object sender, EventArgs arguments)

+    {

       var task = sender as ErrorTask;

       if (task == null || task.Document == null)

         return;

@@ -321,9 +387,11 @@ namespace DafnyLanguage
 

       // Get the VsTextBuffer

       VsTextBuffer buffer = docData as VsTextBuffer;

-      if (buffer == null) {

+      if (buffer == null)

+      {

         IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider;

-        if (bufferProvider != null) {

+        if (bufferProvider != null)

+        {

           IVsTextLines lines;

           Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines));

           buffer = lines as VsTextBuffer;

@@ -339,7 +407,6 @@ namespace DafnyLanguage
       // Finally, move the cursor

       Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column));

     }

-

   }

 

 

@@ -361,11 +428,10 @@ namespace DafnyLanguage
     /// <summary>

     /// "line" and "col" are expected to be 0-based

     /// </summary>

-    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot) {

-      Contract.Requires(0 <= line);

-      Contract.Requires(0 <= col);

-      Line = line;

-      Column = col;

+    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot)

+    {

+      Line = Math.Max(0, line);

+      Column = Math.Max(0, col);

       Category = cat;

       Message = msg;

       Snapshot = snapshot;