DafnyExtension: Added experimental support for diagnosing timeouts.

6 files changed, 100 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/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/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 4c4b1403..4c9a4913 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -122,6 +122,16 @@
         </Strings>

       </Button>

 

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0106" type="Button">

+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>TextChanges</CommandFlag>

+        <Strings>

+          <ButtonText>Re-verify to diagnose timeouts</ButtonText>

+        </Strings>

+      </Button>

+

     </Buttons>

 

     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->

@@ -154,6 +164,7 @@
       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

       <IDSymbol name="cmdidToggleBVD" value="0x0104" />

       <IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />

+      <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0106" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 0acf3554..58c8f0ab 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -53,6 +53,12 @@ namespace DafnyLanguage.DafnyMenu
 

 

     void ShowErrorModel(IWpfTextView activeTextView);

+

+

+    bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView);

+

+

+    void DiagnoseTimeouts(IWpfTextView activeTextView);

   }

 

 

@@ -88,6 +94,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand toggleSnapshotVerificationCommand;

     private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;

     private OleMenuCommand toggleBVDCommand;

+    private OleMenuCommand diagnoseTimeoutsCommand;

 

     bool BVDDisabled;

 

@@ -157,6 +164,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

         mcs.AddCommand(toggleBVDCommand);

 

+        var diagnoseTimeoutsCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidDiagnoseTimeouts);

+        diagnoseTimeoutsCommand = new OleMenuCommand(DiagnoseTimeoutsCallback, diagnoseTimeoutsCommandID);

+        diagnoseTimeoutsCommand.Enabled = true;

+        diagnoseTimeoutsCommand.BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus;

+        mcs.AddCommand(diagnoseTimeoutsCommand);

+

         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);

         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

@@ -301,6 +314,16 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    void diagnoseTimeoutsCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

+      if (MenuProxy != null && atv != null)

+      {

+        var visible = MenuProxy.DiagnoseTimeoutsCommandEnabled(atv);

+        diagnoseTimeoutsCommand.Visible = visible;

+      }

+    }

+

     private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var atv = ActiveTextView;

@@ -317,6 +340,15 @@ namespace DafnyLanguage.DafnyMenu
       toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";

     }

 

+    void DiagnoseTimeoutsCallback(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

+      if (MenuProxy != null && atv != null)

+      {

+        MenuProxy.DiagnoseTimeouts(atv);

+      }

+    }

+

     public void ExecuteAsCompiling(Action action, TextWriter outputWriter)

     {

       IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index b6f30145..427dd888 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -13,5 +13,6 @@ namespace DafnyLanguage.DafnyMenu
     public static uint cmdidToggleSnapshotVerification = 0x103;

     public const uint cmdidToggleBVD = 0x104;

     public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;

+    public static uint cmdidDiagnoseTimeouts = 0x106;

   };

 }
\ No newline at end of file