DafnyExtension: toward some fixes

5 files changed, 80 insertions, 46 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index b7b2cd6d..79194d97 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -47,7 +47,7 @@ namespace DafnyLanguage
       }

     }

 

-    public Dafny.Program Process() {

+    public Dafny.Program ProcessResolution() {

       if (!ParseAndTypeCheck()) {

         return null;

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index db91cd92..4f414b91 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -89,16 +89,24 @@ namespace DafnyLanguage
 

     void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {

       var r = sender as ResolverTagger;

-      if (r != null && r._program != null) {

-        if (!ComputeIdentifierRegions(r._program, r._snapshot))

-          return;  // no new regions

+      if (r != null) {

+        ITextSnapshot snap;

+        Microsoft.Dafny.Program prog;

+        lock (this) {

+          snap = r._snapshot;

+          prog = r._program;

+        }

+        if (prog != null) {

+          if (!ComputeIdentifierRegions(prog, snap))

+            return;  // no new regions

 

-        var chng = TagsChanged;

-        if (chng != null) {

-          NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);

-          if (spans.Count > 0) {

-            SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

-            chng(this, new SnapshotSpanEventArgs(span));

+          var chng = TagsChanged;

+          if (chng != null) {

+            NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);

+            if (spans.Count > 0) {

+              SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

+              chng(this, new SnapshotSpanEventArgs(span));

+            }

           }

         }

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index e51e9887..a47cdba7 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -91,16 +91,24 @@ namespace DafnyLanguage
 

     void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {

       var r = sender as ResolverTagger;

-      if (r != null && r._program != null) {

-        if (!ComputeOutliningRegions(r._program, r._snapshot))

-          return;  // no new regions

-

-        var chng = TagsChanged;

-        if (chng != null) {

-          NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);

-          if (spans.Count > 0) {

-            SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

-            chng(this, new SnapshotSpanEventArgs(span));

+      if (r != null) {

+        ITextSnapshot snap;

+        Microsoft.Dafny.Program prog;

+        lock (this) {

+          snap = r._snapshot;

+          prog = r._program;

+        }

+        if (prog != null) {

+          if (!ComputeOutliningRegions(prog, snap))

+            return;  // no new regions

+

+          var chng = TagsChanged;

+          if (chng != null) {

+            NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);

+            if (spans.Count > 0) {

+              SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

+              chng(this, new SnapshotSpanEventArgs(span));

+            }

           }

         }

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index 34dcce3c..d8a60647 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -121,19 +121,22 @@ namespace DafnyLanguage
         // If r._program is null, then the current buffer contains a Dafny fragment that does not resolve.  If it is non-null,

         // then r._program has been successfully resolved, so when things have been sufficiently idle, we're ready to verify it.

         resolver = r;

-        latestProgram = r._program;

-        latestSnapshot = latestProgram != null ? r._snapshot : null;

+        lock (r) {

+          latestProgram = r._program;

+          latestSnapshot = latestProgram != null ? r._snapshot : null;

+        }

       }

     }

 

     bool verificationInProgress;  // this field is protected by "this"

+    bool verificationRequested;  // this field is protected by "this".  Invariant:  verificationRequested ==> verificationInProgress

     public void DoTheVerification(object sender, EventArgs args) {

       var buffer = sender as ITextBuffer;

       if (buffer != null && latestProgram != null && resolver != null) {

         bool tagsChanged = false;

         lock (this) {

           if (verificationInProgress) {

-            // take no further action

+            verificationRequested = true;

             return;

           }

           verificationInProgress = true;

@@ -185,25 +188,30 @@ namespace DafnyLanguage
       }

 

       public void Start() {

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

-        bool success = DafnyDriver.Verify(program, errorInfo => {

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

-          foreach (var aux in errorInfo.Aux) {

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

+        bool verifySomeMore = true;

+        while (verifySomeMore) {

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

+          bool success = DafnyDriver.Verify(program, errorInfo => {

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

+            foreach (var aux in errorInfo.Aux) {

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

+            }

+          });

+

+          lock (pt) {

+            verifySomeMore = pt.verificationRequested;

+            pt.verificationInProgress = verifySomeMore;

+            pt.verificationRequested = false;

+            if (pt.bufferChangesPreVerificationStart.Count != 0) {

+              pt.bufferChangesPreVerificationStart = new List<SnapshotSpan>();

+            }

+            resolver.PopulateErrorList(newErrors, true, snapshot);  // TODO:  is this appropriate to do inside the monitor?

           }

-        });

 

-        lock (pt) {

-          pt.verificationInProgress = false;

-          if (pt.bufferChangesPreVerificationStart.Count != 0) {

-            pt.bufferChangesPreVerificationStart = new List<SnapshotSpan>();

+          var chng = pt.TagsChanged;

+          if (chng != null) {

+            chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

           }

-          resolver.PopulateErrorList(newErrors, true, snapshot);  // TODO:  is this appropriate to do inside the monitor?

-        }

-

-        var chng = pt.TagsChanged;

-        if (chng != null) {

-          chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

         }

       }

     }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index 2017cfaa..398629ab 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -70,11 +70,12 @@ namespace DafnyLanguage
   {

     ITextBuffer _buffer;

     ITextDocument _document;

+    // 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>();

     ErrorListProvider _errorProvider;

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

 

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

       _buffer = buffer;

@@ -138,15 +139,22 @@ namespace DafnyLanguage
           yield return new TagSpan<DafnyResolverTag>(span, new DafnyErrorResolverTag(ty, err.Message));

         }

       }

-      if (_program != null) {

-        yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(_snapshot, 0, _snapshot.Length), new DafnySuccessResolverTag(_program));

+

+      ITextSnapshot snap;

+      Dafny.Program prog;

+      lock (this) {

+        snap = _snapshot;

+        prog = _program;

+      }

+      if (prog != null) {

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

       }

     }

 

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

 

     /// <summary>

-    /// Calls the Dafny verifier on the program, updates the Error List accordingly.

+    /// Calls the Dafny parser/resolver/type checker on the program, updates the Error List accordingly.

     /// </summary>

     void ProcessFile(object sender, EventArgs args) {

       ITextSnapshot snapshot = _buffer.CurrentSnapshot;

@@ -158,7 +166,7 @@ namespace DafnyLanguage
       List<DafnyError> newErrors;

       Dafny.Program program;

       try {

-        program = driver.Process();

+        program = driver.ProcessResolution();

         newErrors = driver.Errors;

       } catch (Exception e) {

         newErrors = new List<DafnyError>();

@@ -166,8 +174,10 @@ namespace DafnyLanguage
         program = null;

       }

 

-      _snapshot = snapshot;

-      _program = program;

+      lock (this) {

+        _snapshot = snapshot;

+        _program = program;

+      }

       PopulateErrorList(newErrors, false, snapshot);

     }