DafnyExtension: Made it possible to activate the more advanced verification result caching in Boogie (experimental for now).

5 files changed, 86 insertions, 10 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index f4eb4fb7..36b07d60 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) {

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/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 0e8c7855..813ccd23 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,6 +103,16 @@
         </Strings>

       </Button>

 

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleMoreAdvancedSnapshotVerification" priority="0x0105" type="Button">

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

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <CommandFlag>TextChanges</CommandFlag>

+        <Strings>

+          <ButtonText>Enable more advanced on-demand re-verification</ButtonText>

+        </Strings>

+      </Button>

+

       <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">

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

         <CommandFlag>DynamicVisibility</CommandFlag>

@@ -144,6 +154,7 @@
       <IDSymbol name="cmdidStopVerifier" value="0x0102" />

       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

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

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

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 114ddf10..58bf2a26 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -19,7 +19,13 @@ namespace DafnyLanguage.DafnyMenu
 

   public interface IMenuProxy

   {

-    bool ToggleSnapshotVerification(IWpfTextView activeTextView);

+    int ToggleSnapshotVerification(IWpfTextView activeTextView);

+

+

+    int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView);

+

+

+    bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView);

 

 

     bool StopVerifierCommandEnabled(IWpfTextView activeTextView);

@@ -80,6 +86,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;

     private OleMenuCommand stopVerifierCommand;

     private OleMenuCommand toggleSnapshotVerificationCommand;

+    private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;

     private OleMenuCommand toggleBVDCommand;

 

     bool BVDDisabled;

@@ -138,6 +145,11 @@ namespace DafnyLanguage.DafnyMenu
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);

         mcs.AddCommand(toggleSnapshotVerificationCommand);

 

+        var toggleMoreAdvancedSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleMoreAdvancedSnapshotVerification);

+        toggleMoreAdvancedSnapshotVerificationCommand = new OleMenuCommand(ToggleMoreAdvancedSnapshotVerificationCallback, toggleMoreAdvancedSnapshotVerificationCommandID);

+        toggleMoreAdvancedSnapshotVerificationCommand.BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus;

+        mcs.AddCommand(toggleMoreAdvancedSnapshotVerificationCommand);

+

         var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleBVD);

         toggleBVDCommand = new OleMenuCommand(ToggleBVDCallback, showErrorModelCommandID);

         toggleBVDCommand.Enabled = true;

@@ -191,8 +203,20 @@ namespace DafnyLanguage.DafnyMenu
       var atv = ActiveTextView;

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

       {

-        var on = MenuProxy.ToggleSnapshotVerification(atv);

-        toggleSnapshotVerificationCommand.Text = (on ? "Disable" : "Enable") + " on-demand re-verification";

+        var mode = MenuProxy.ToggleSnapshotVerification(atv);

+        toggleSnapshotVerificationCommand.Text = (mode == 1 ? "Disable" : "Enable") + " on-demand re-verification";

+        toggleMoreAdvancedSnapshotVerificationCommand.Text = (mode == 2 ? "Disable" : "Enable") + " more advanced on-demand re-verification";

+      }

+    }

+

+    void ToggleMoreAdvancedSnapshotVerificationCallback(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        var mode = MenuProxy.ToggleMoreAdvancedSnapshotVerification(atv);

+        toggleSnapshotVerificationCommand.Text = (mode != 0 ? "Disable" : "Enable") + " on-demand re-verification";

+        toggleMoreAdvancedSnapshotVerificationCommand.Text = (mode == 2 ? "Disable" : "Enable") + " more advanced on-demand re-verification";

       }

     }

 

@@ -276,6 +300,16 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        var visible = MenuProxy.MoreAdvancedSnapshotVerificationCommandEnabled(atv);

+        toggleMoreAdvancedSnapshotVerificationCommand.Visible = visible;

+      }

+    }

+

     void ToggleBVDCallback(object sender, EventArgs e)

     {

       BVDDisabled = !BVDDisabled;

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index f3452cb9..b6f30145 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -12,5 +12,6 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidMenu = 0x1021;

     public static uint cmdidToggleSnapshotVerification = 0x103;

     public const uint cmdidToggleBVD = 0x104;

+    public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;

   };

 }
\ No newline at end of file