Merge

5 files changed, 58 insertions, 12 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 5b8cc943..7f39fe34 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -239,6 +239,11 @@ namespace DafnyLanguage
       return Dafny.DafnyOptions.Clo.VerifySnapshots;

     }

 

+    public static void SetDiagnoseTimeouts(bool v)

+    {

+      Dafny.DafnyOptions.Clo.RunDiagnosticsOnTimeout = v;

+    }

+

     public static int ChangeIncrementalVerification(int mode)

     {

       var old = Dafny.DafnyOptions.Clo.VerifySnapshots;

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 11e1287f..9ddc8344 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -67,6 +67,15 @@ namespace DafnyLanguage
       }

     }

 

+    public void DiagnoseTimeouts(IWpfTextView activeTextView)

+    {

+      DafnyLanguage.ProgressTagger tagger;

+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))

+      {

+        tagger.StartVerification(false, true);

+      }

+    }

+

     public bool MenuEnabled(IWpfTextView activeTextView)

     {

       return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";

@@ -80,6 +89,14 @@ namespace DafnyLanguage
                     && resolver.Program != null;

     }

 

+    public bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView)

+    {

+      ResolverTagger resolver;

+      return activeTextView != null

+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

+                    && resolver.VerificationErrors.Any(err => err.Message.Contains("timed out"));

+    }

+

     public void Compile(IWpfTextView activeTextView)

     {

       ResolverTagger resolver;

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index c4b88f98..85771e94 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -160,6 +160,7 @@ namespace DafnyLanguage
               }

               if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {

                 var nm =

+                  m is Dafny.InductivePredicate ? "inductive predicate" :

                   m is Dafny.CoPredicate ? "copredicate" :

                   // m is Dafny.PrefixPredicate ? "prefix predicate" :  // this won't ever occur here

                   m is Dafny.Predicate ? "predicate" :

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index b4e58d3d..c3f56259 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -197,6 +197,7 @@ namespace DafnyLanguage
     bool verificationInProgress;  // this field is protected by "this".  Invariant:  !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0

     System.Threading.Tasks.Task verificationTask;

     public bool VerificationDisabled { get; private set; }

+    bool isDiagnosingTimeouts;

     string lastRequestId;

 

     public static readonly IDictionary<ITextBuffer, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<ITextBuffer, ProgressTagger>();

@@ -227,14 +228,21 @@ namespace DafnyLanguage
         if (prog == null || VerificationDisabled) return;

         // We have a successfully resolved program to verify

 

-        var resolvedVersion = snap.Version.VersionNumber;

-        if (bufferChangesPostVerificationStart.Count == 0) {

-          // Nothing new to verify.  No reason to start a new verification.

-          return;

-        } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {

-          // There have been buffer changes since the program that was resolved.  Do nothing here,

-          // and instead just await the next resolved program.

-          return;

+        var dt = isDiagnosingTimeouts;

+        if (!dt)

+        {

+          var resolvedVersion = snap.Version.VersionNumber;

+          if (bufferChangesPostVerificationStart.Count == 0)

+          {

+            // Nothing new to verify.  No reason to start a new verification.

+            return;

+          }

+          else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion))

+          {

+            // There have been buffer changes since the program that was resolved.  Do nothing here,

+            // and instead just await the next resolved program.

+            return;

+          }

         }

 

         // at this time, we're committed to running the verifier

@@ -254,10 +262,14 @@ namespace DafnyLanguage
         }

 

         verificationTask = System.Threading.Tasks.Task.Factory.StartNew(

-          () => RunVerifier(prog, snap, lastRequestId, resolver),

+          () => RunVerifier(prog, snap, lastRequestId, resolver, dt),

           TaskCreationOptions.LongRunning);

 

         verificationInProgress = true;

+        if (dt)

+        {

+          isDiagnosingTimeouts = false;

+        }

 

         // Change orange progress markers into yellow ones

         Contract.Assert(bufferChangesPreVerificationStart.Count == 0);  // follows from monitor invariant

@@ -293,7 +305,7 @@ namespace DafnyLanguage
       }

     }

 

-    public void StartVerification()

+    public void StartVerification(bool clearCache = true, bool diagnoseTimeouts = false)

     {

       lock (this)

       {

@@ -301,7 +313,11 @@ namespace DafnyLanguage
         bufferChangesPostVerificationStart.Clear();

         bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));

         VerificationDisabled = false;

-        ClearCachedVerificationResults();

+        isDiagnosingTimeouts = diagnoseTimeouts;

+        if (clearCache)

+        {

+          ClearCachedVerificationResults();

+        }

         NotifyAboutChangedTags(_buffer.CurrentSnapshot);

       }

     }

@@ -314,7 +330,7 @@ namespace DafnyLanguage
       }

     }

 

-    void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder) {

+    void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder, bool diagnoseTimeouts) {

       Contract.Requires(program != null);

       Contract.Requires(snapshot != null);

       Contract.Requires(requestId != null);

@@ -332,6 +348,8 @@ namespace DafnyLanguage
         _version++;

       }

 

+      DafnyDriver.SetDiagnoseTimeouts(diagnoseTimeouts);

+

       try

       {

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

@@ -369,6 +387,10 @@ namespace DafnyLanguage
       {

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

       }

+      finally

+      {

+        DafnyDriver.SetDiagnoseTimeouts(!diagnoseTimeouts);

+      }

 

       lock (this) {

         bufferChangesPreVerificationStart.Clear();

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 0019ce81..af141ad7 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -308,6 +308,7 @@ namespace DafnyLanguage
                 case "import":

                 case "in":

                 case "include":

+                case "inductive":

                 case "int":

                 case "invariant":

                 case "iterator":