Merge

4 files changed, 103 insertions, 36 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index f4eb4fb7..ea21f12b 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -45,7 +45,7 @@ namespace DafnyLanguage
 

         ExecutionEngine.printer = new DummyPrinter();

         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

-        ToggleIncrementalVerification();

+        ChangeIncrementalVerification(1);

       }

     }

 

@@ -215,11 +215,30 @@ namespace DafnyLanguage
       }

     }

 

-    public static bool ToggleIncrementalVerification()

+    public static int IncrementalVerificationMode()

     {

-      // TODO(wuestholz): Change this once there are more than two options.

-      Dafny.DafnyOptions.Clo.VerifySnapshots = (Dafny.DafnyOptions.Clo.VerifySnapshots + 1) % 2;

-      return 0 < Dafny.DafnyOptions.Clo.VerifySnapshots;

+      return Dafny.DafnyOptions.Clo.VerifySnapshots;

+    }

+

+    public static int ChangeIncrementalVerification(int mode)

+    {

+      var old = Dafny.DafnyOptions.Clo.VerifySnapshots;

+      if (mode == 1 && old != 0)

+      {

+        // Disable mode 1.

+        Dafny.DafnyOptions.Clo.VerifySnapshots = 0;

+      }

+      else if (mode == 2 && old == 2)

+      {

+        // Disable mode 2.

+        Dafny.DafnyOptions.Clo.VerifySnapshots = 1;

+      }

+      else

+      {

+        // Enable mode.

+        Dafny.DafnyOptions.Clo.VerifySnapshots = mode;

+      }

+      return Dafny.DafnyOptions.Clo.VerifySnapshots;

     }

 

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

@@ -230,7 +249,8 @@ namespace DafnyLanguage
 

       resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations);

 

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

+      // TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie.

+      PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, er);

       switch (oc) {

         case PipelineOutcome.Done:

         case PipelineOutcome.VerificationCompleted:

@@ -248,7 +268,7 @@ namespace DafnyLanguage
     /// else.  Hence, any resolution errors and type checking errors are due to errors in

     /// the translation.

     /// </summary>

-    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string requestId, ErrorReporterDelegate er)

+    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string programId, string requestId, ErrorReporterDelegate er)

     {

       Contract.Requires(program != null);

 

@@ -257,8 +277,8 @@ namespace DafnyLanguage
         ExecutionEngine.EliminateDeadVariables(program);

         ExecutionEngine.CollectModSets(program);

         ExecutionEngine.CoalesceBlocks(program);

-        ExecutionEngine.Inline(program);  

-        return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);

+        ExecutionEngine.Inline(program);

+        return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), programId, er, requestId);

       }

       return oc;

     }

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index a67ba602..11e1287f 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -17,9 +17,20 @@ namespace DafnyLanguage
       this.DafnyMenuPackage = DafnyMenuPackage;

     }

 

-    public bool ToggleSnapshotVerification(IWpfTextView activeTextView)

+    public int ToggleSnapshotVerification(IWpfTextView activeTextView)

     {

-      return DafnyDriver.ToggleIncrementalVerification();

+      return DafnyDriver.ChangeIncrementalVerification(1);

+    }

+

+    public int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView)

+    {

+      return DafnyDriver.ChangeIncrementalVerification(2);

+    }

+

+    public bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView)

+    {

+      return activeTextView != null

+             && 0 < DafnyDriver.IncrementalVerificationMode();

     }

 

     public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 48f5d1b4..5068354a 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -5,6 +5,7 @@ using System.Linq;
 using Microsoft.VisualStudio.Text;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

+using System.Diagnostics.Contracts;

 

 

 namespace DafnyLanguage

@@ -69,11 +70,12 @@ namespace DafnyLanguage
     }

   }

 

-  internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>

+  internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>, IDisposable

   {

     ITextBuffer _buffer;

     ITextSnapshot _snapshot;

     List<TokenRegion> _regions;

+    bool _disposed;

 

     internal DafnyTokenTagger(ITextBuffer buffer) {

       _buffer = buffer;

@@ -83,6 +85,19 @@ namespace DafnyLanguage
       _buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);

     }

 

+    public void Dispose() {

+      lock (this) {

+        if (!_disposed) {

+          _buffer.Changed -= ReparseFile;

+          _buffer = null;

+          _snapshot = null;

+          _regions = null;

+          _disposed = true;

+        }

+      }

+      GC.SuppressFinalize(this);

+    }

+

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

 

     public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

@@ -148,20 +163,24 @@ namespace DafnyLanguage
     private static List<TokenRegion> Rescan(ITextSnapshot newSnapshot) {

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

 

-      bool stillScanningLongComment = false;

-      SnapshotPoint commentStart = new SnapshotPoint();  // used only when stillScanningLongComment

-      SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint();  // used only when stillScanningLongComment

+      int longCommentDepth = 0;

+      SnapshotPoint commentStart = new SnapshotPoint();  // used only when longCommentDepth != 0

+      SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint();  // used only when longCommentDepth != 0

       foreach (ITextSnapshotLine line in newSnapshot.Lines) {

         string txt = line.GetText();  // the current line (without linebreak characters)

         int N = txt.Length;  // length of the current line

         int cur = 0;  // offset into the current line

 

-        if (stillScanningLongComment) {

-          if (ScanForEndOfComment(txt, ref cur)) {

+        if (longCommentDepth != 0) {

+          ScanForEndOfComment(txt, ref longCommentDepth, ref cur);

+          if (longCommentDepth == 0) {

+            // we just finished parsing a long comment

             newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment));

-            stillScanningLongComment = false;

           } else {

+            // we're still parsing the long comment

+            Contract.Assert(cur == txt.Length);

             commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);

+            goto OUTER_CONTINUE;

           }

         }

 

@@ -179,9 +198,9 @@ namespace DafnyLanguage
             if ('a' <= ch && ch <= 'z') break;

             if ('A' <= ch && ch <= 'Z') break;

             if ('0' <= ch && ch <= '9') { ty = DafnyTokenKind.Number; break; }

+            if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers

             if (ch == '"') { ty = DafnyTokenKind.String; break; }

             if (ch == '/') { ty = DafnyTokenKind.Comment; break; }

-            if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers

           }

 

           // advance to the end of the token

@@ -211,7 +230,7 @@ namespace DafnyLanguage
               }

             }

           } else if (ty == DafnyTokenKind.Comment) {

-            if (end == N) continue;  // this was not the start of a comment

+            if (end == N) continue;  // this was not the start of a comment; it was just a single "/" and we don't care to color it

             char ch = txt[end];

             if (ch == '/') {

               // a short comment

@@ -220,15 +239,18 @@ namespace DafnyLanguage
               // a long comment; find the matching "*/"

               end++;

               commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);

-              if (ScanForEndOfComment(txt, ref end)) {

+              Contract.Assert(longCommentDepth == 0);

+              longCommentDepth = 1;

+              ScanForEndOfComment(txt, ref longCommentDepth, ref end);

+              if (longCommentDepth == 0) {

+                // we finished scanning a long comment, and "end" is set to right after it

                 newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment));

               } else {

-                stillScanningLongComment = true;

                 commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);

               }

               continue;

             } else {

-              // not a comment

+              // not a comment; it was just a single "/" and we don't care to color it

               continue;

             }

           } else {

@@ -322,7 +344,7 @@ namespace DafnyLanguage
                 #endregion

                   break;

                 default:

-                  continue;  // it was an identifier

+                  continue;  // it was an identifier, so we don't color it

               }

             }

           }

@@ -332,26 +354,40 @@ namespace DafnyLanguage
       OUTER_CONTINUE: ;

       }

 

-      if (stillScanningLongComment) {

+      if (longCommentDepth != 0) {

+        // This was a malformed comment, running to the end of the buffer.  Above, we let "commentEndAsWeKnowIt" be the end of the

+        // last line, so we can use it here.

         newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));

       }

 

       return newRegions;

     }

 

-    private static bool ScanForEndOfComment(string txt, ref int end) {

-      int N = txt.Length;

-      for (; end < N; end++) {

+    /// <summary>

+    /// Scans "txt" beginning with depth "depth", which is assumed to be non-0.  Any occurrences of "/*" or "*/"

+    /// increment or decrement "depth".  If "depth" ever reaches 0, then "end" returns as the number of characters

+    /// consumed from "txt" (including the last "*/").  If "depth" is still non-0 when the entire "txt" has

+    /// been consumed, then "end" returns as the length of "txt".  (Note, "end" may return as the length of "txt"

+    /// if "depth" is still non-0 or if "depth" became 0 from reading the last characters of "txt".)

+    /// </summary>

+    private static void ScanForEndOfComment(string txt, ref int depth, ref int end) {

+      Contract.Requires(depth > 0);

+

+      int Nminus1 = txt.Length - 1;  // no reason ever to look at the last character of the line, unless the second-to-last character is '*' or '/'

+      for (; end < Nminus1; ) {

         char ch = txt[end];

-        if (ch == '*' && end + 1 < N) {

-          ch = txt[end + 1];

-          if (ch == '/') {

-            end += 2;

-            return true;

-          }

+        if (ch == '*' && txt[end + 1] == '/') {

+          end += 2;

+          depth--;

+          if (depth == 0) { return; }

+        } else if (ch == '/' && txt[end + 1] == '*') {

+          end += 2;

+          depth++;

+        } else {

+          end++;

         }

       }

-      return false;  // hit end-of-line without finding end-of-comment

+      end = txt.Length;  // we didn't look at the last character, but we still consumed all the output

     }

   }

 

diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index 3b2316b9..f4f66193 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -6,7 +6,7 @@
     <Description xml:space="preserve">This is a language mode for using the Dafny language inside Visual Studio.</Description>

   </Metadata>

   <Installation InstalledByMsi="false">

-    <InstallationTarget Version="[11.0,12.0)" Id="Microsoft.VisualStudio.Pro" />

+    <InstallationTarget Version="[11.0,13.0)" Id="Microsoft.VisualStudio.Pro" />

   </Installation>

   <Dependencies>

     <Dependency Id="Microsoft.Framework.NDP" DisplayName="Microsoft .NET Framework" d:Source="Manual" Version="4.5" />