DafnyExtension: Worked on integrating BVD.

10 files changed, 176 insertions, 46 deletions

diff --git a/Source/DafnyMenu/BvdToolWindow.cs b/Source/DafnyMenu/BvdToolWindow.cs
new file mode 100644
index 00000000..0316d558
--- /dev/null
+++ b/Source/DafnyMenu/BvdToolWindow.cs
@@ -0,0 +1,59 @@
+using System;

+using System.Collections;

+using System.ComponentModel;

+using System.Drawing;

+using System.Data;

+using System.Windows;

+using System.Runtime.InteropServices;

+using Microsoft.VisualStudio.Shell.Interop;

+using Microsoft.VisualStudio.Shell;

+

+namespace DafnyLanguage.DafnyMenu

+{

+  /// <summary>

+  /// This class implements the tool window exposed by this package and hosts a user control.

+  ///

+  /// In Visual Studio tool windows are composed of a frame (implemented by the shell) and a pane, 

+  /// usually implemented by the package implementer.

+  ///

+  /// This class derives from the ToolWindowPane class provided from the MPF in order to use its 

+  /// implementation of the IVsUIElementPane interface.

+  /// </summary>

+  [Guid(GuidList.guidToolWindowPersistanceString)]

+  public class BvdToolWindow : ToolWindowPane

+  {

+    private static readonly Lazy<Microsoft.Boogie.ModelViewer.Main> bvdInstance = new Lazy<Microsoft.Boogie.ModelViewer.Main>(() => new Microsoft.Boogie.ModelViewer.Main(new string[] { }, true));

+    

+    /// <summary>

+    /// Standard constructor for the tool window.

+    /// </summary>

+    public BvdToolWindow() :

+      base(null)

+    {

+      // Set the window title reading it from the resources.

+      this.Caption = "Boogie Verification Debugger";

+      // Set the image that will appear on the tab of the window frame

+      // when docked with an other window

+      // The resource ID correspond to the one defined in the resx file

+      // while the Index is the offset in the bitmap strip. Each image in

+      // the strip being 16x16.

+      // this.BitmapResourceID = 301;

+      // this.BitmapIndex = 1;

+

+      // This is the user control hosted by the tool window; Note that, even if this class implements IDisposable,

+      // we are not calling Dispose on this object. This is because ToolWindowPane calls Dispose on 

+      // the object returned by the Content property.

+      // base.Content = new MyControl();

+    }

+

+    public override System.Windows.Forms.IWin32Window Window

+    {

+      get { return bvdInstance.Value; }

+    }

+

+    public static Microsoft.Boogie.ModelViewer.Main BVD

+    {

+      get { return bvdInstance.Value; }

+    }

+  }

+}

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 6cd493c6..7fb6cfab 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -52,13 +52,23 @@
     <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

     <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop" />

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <EmbedInteropTypes>True</EmbedInteropTypes>

+    </Reference>

     <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0" />

     <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

+    <Reference Include="ModelViewer">

+      <HintPath>..\..\..\boogie\Binaries\ModelViewer.dll</HintPath>

+    </Reference>

+    <Reference Include="PresentationCore" />

+    <Reference Include="PresentationFramework" />

     <Reference Include="System" />

     <Reference Include="System.Core" />

     <Reference Include="System.Design" />

+    <Reference Include="System.Windows.Forms" />

+    <Reference Include="WindowsBase" />

   </ItemGroup>

   <ItemGroup>

     <COMReference Include="EnvDTE">

@@ -72,6 +82,7 @@
     </COMReference>

   </ItemGroup>

   <ItemGroup>

+    <Compile Include="BvdToolWindow.cs" />

     <Compile Include="Guids.cs" />

     <Compile Include="Resources.Designer.cs">

       <AutoGen>True</AutoGen>

@@ -92,6 +103,7 @@
     <EmbeddedResource Include="VSPackage.resx">

       <MergeWithCTO>true</MergeWithCTO>

       <ManifestResourceName>VSPackage</ManifestResourceName>

+      <SubType>Designer</SubType>

     </EmbeddedResource>

   </ItemGroup>

   <ItemGroup>

@@ -102,20 +114,18 @@
   <ItemGroup>

     <VSCTCompile Include="DafnyMenu.vsct">

       <ResourceName>Menus.ctmenu</ResourceName>

+      <SubType>Designer</SubType>

     </VSCTCompile>

   </ItemGroup>

   <ItemGroup>

-    <None Include="Resources\Images.png" />

-  </ItemGroup>

-  <ItemGroup>

-    <Content Include="Resources\Package.ico" />

-  </ItemGroup>

-  <ItemGroup>

     <ProjectReference Include="..\DafnyExtension\DafnyExtension.csproj">

       <Project>{6e9a5e14-0763-471c-a129-80a879d9e7ba}</Project>

       <Name>DafnyExtension</Name>

     </ProjectReference>

   </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Resources\" />

+  </ItemGroup>

   <PropertyGroup>

     <UseCodebase>true</UseCodebase>

   </PropertyGroup>

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 5cb2975d..25c8dea9 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,6 +103,15 @@
         </Strings>

       </Button>

 

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

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

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <Strings>

+          <ButtonText>Show error model</ButtonText>

+        </Strings>

+      </Button>

+

     </Buttons>

 

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

@@ -133,6 +142,7 @@
       <IDSymbol name="cmdidRunVerifier" value="0x0101" />

       <IDSymbol name="cmdidStopVerifier" value="0x0102" />

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

+      <IDSymbol name="cmdidShowErrorModel" value="0x0104" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 294b0b75..1506e893 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -1,13 +1,12 @@
 using System;

+using System.ComponentModel.Design;

 using System.Diagnostics;

 using System.Globalization;

+using System.Linq;

 using System.Runtime.InteropServices;

-using System.ComponentModel.Design;

-using Microsoft.Win32;

-using Microsoft.VisualStudio;

-using Microsoft.VisualStudio.Shell.Interop;

-using Microsoft.VisualStudio.OLE.Interop;

 using Microsoft.VisualStudio.Shell;

+using Microsoft.VisualStudio.Shell.Interop;

+

 

 namespace DafnyLanguage.DafnyMenu

 {

@@ -26,10 +25,12 @@ namespace DafnyLanguage.DafnyMenu
   [PackageRegistration(UseManagedResourcesOnly = true)]

   // This attribute is used to register the information needed to show this package

   // in the Help/About dialog of Visual Studio.

-  [InstalledProductRegistration("#110", "#112", "1.0", IconResourceID = 400)]

+  [InstalledProductRegistration("#110", "#112", "1.0")]

   // This attribute is needed to let the shell know that this package exposes some menus.

   [ProvideMenuResource("Menus.ctmenu", 1)]

   [ProvideAutoLoad("{6c7ed99a-206a-4937-9e08-b389de175f68}")]

+  [ProvideToolWindow(typeof(BvdToolWindow), Transient = true)]

+  [ProvideToolWindowVisibility(typeof(BvdToolWindow), GuidList.guidDafnyMenuCmdSetString)]

   [Guid(GuidList.guidDafnyMenuPkgString)]

   public sealed class DafnyMenuPackage : Package

   {

@@ -39,6 +40,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;

     private OleMenuCommand stopVerifierCommand;

     private OleMenuCommand toggleSnapshotVerificationCommand;

+    private OleMenuCommand showErrorModelCommand;

 

     /// <summary>

     /// Default constructor of the package.

@@ -92,6 +94,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);

         mcs.AddCommand(toggleSnapshotVerificationCommand);

 

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

+        showErrorModelCommand = new OleMenuCommand(ShowErrorModelCallback, showErrorModelCommandID);

+        showErrorModelCommand.Enabled = true;

+        showErrorModelCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

+        mcs.AddCommand(showErrorModelCommand);

+

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

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

         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

@@ -110,8 +118,7 @@ namespace DafnyLanguage.DafnyMenu
     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

-      if (tagger != null)

+      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))

       {

         tagger.StopVerification();

       }

@@ -121,8 +128,7 @@ namespace DafnyLanguage.DafnyMenu
     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

-      if (tagger != null)

+      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))

       {

         tagger.StartVerification();

       }

@@ -131,7 +137,8 @@ namespace DafnyLanguage.DafnyMenu
     void menuCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      var isActive = dte.ActiveDocument.FullName.EndsWith(".dfy", StringComparison.OrdinalIgnoreCase);

+      var isActive = dte.ActiveDocument != null

+                     && dte.ActiveDocument.FullName.EndsWith(".dfy", StringComparison.OrdinalIgnoreCase);

       menuCommand.Visible = isActive;

       menuCommand.Enabled = isActive;

     }

@@ -140,26 +147,32 @@ namespace DafnyLanguage.DafnyMenu
     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

-      runVerifierCommand.Visible = tagger != null && tagger.VerificationDisabled;

-      runVerifierCommand.Enabled = tagger != null && tagger.VerificationDisabled;

+      var enabled = dte.ActiveDocument != null

+                 && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)

+                 && tagger != null && tagger.VerificationDisabled;

+      runVerifierCommand.Visible = enabled;

+      runVerifierCommand.Enabled = enabled;

     }

 

     void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

-      stopVerifierCommand.Visible = !(tagger != null && tagger.VerificationDisabled);

-      stopVerifierCommand.Enabled = !(tagger != null && tagger.VerificationDisabled);

+      var disabled = dte.ActiveDocument != null

+                    && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)

+                    && tagger != null && tagger.VerificationDisabled;

+      stopVerifierCommand.Visible = !disabled;

+      stopVerifierCommand.Enabled = !disabled;

     }

 

     void compileCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      Microsoft.Dafny.Program program;

-      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);

-      compileCommand.Enabled = (program != null);

+      ResolverTagger resolver;

+      var enabled = dte.ActiveDocument != null

+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

+                    && resolver.Program != null;

+      compileCommand.Enabled = enabled;

     }

 

     #endregion

@@ -173,19 +186,64 @@ namespace DafnyLanguage.DafnyMenu
     private void CompileCallback(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      Microsoft.Dafny.Program program;

-      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);

+      ResolverTagger resolver;

 

-      if (program != null)

+      if (dte.ActiveDocument != null

+          && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

+          && resolver.Program != null)

       {

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

         uint cookie = 0;

         statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);

 

-        DafnyDriver.Compile(program);

+        DafnyDriver.Compile(resolver.Program);

 

         statusBar.Progress(ref cookie, 0, "", 0, 0);

       }

     }

+

+    /// <summary>

+    /// Show error model.

+    /// </summary>

+    /// <param name="sender"></param>

+    /// <param name="e"></param>

+    void showErrorModelCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      ResolverTagger resolver;

+      var visible = dte.ActiveDocument != null

+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

+                    && resolver.Program != null

+                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));

+      showErrorModelCommand.Visible = false; // TODO(wuestholz): Enable this.

+    }

+

+    private void ShowErrorModelCallback(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      ResolverTagger resolver = null;

+      var show = dte.ActiveDocument != null

+                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

+                 && resolver.Program != null

+                 && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));

+      if (show)

+      {

+        var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);

+        if ((window == null) || (window.Frame == null))

+        {

+          throw new NotSupportedException("Can not create BvdToolWindow.");

+        }

+

+        var models = resolver.VerificationErrors.Select(err => err.Model).Where(m => !string.IsNullOrEmpty(m)).ToArray();

+

+        for (int i = 0; i < models.Length; i++)

+        {

+          BvdToolWindow.BVD.ReadModel(models[i], i);

+        }

+

+        IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;

+        Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(windowFrame.Show());

+      }

+    }

   }

 }

diff --git a/Source/DafnyMenu/Guids.cs b/Source/DafnyMenu/Guids.cs
index dc392c09..8013d590 100644
--- a/Source/DafnyMenu/Guids.cs
+++ b/Source/DafnyMenu/Guids.cs
@@ -11,5 +11,11 @@ namespace DafnyLanguage.DafnyMenu
 

     public static readonly Guid guidDafnyMenuCmdSet = new Guid(guidDafnyMenuCmdSetString);

     public static readonly Guid guidDafnyMenuPkgSet = new Guid(guidDafnyMenuPkgString);

+

+    public const string guidBvdToolboxPkgString = "8b93ddf6-009c-46b9-a0d2-628405a4e466";

+    public const string guidBvdToolboxCmdSetString = "11635790-762b-495f-8c85-9de3a8fe91bd";

+    public const string guidToolWindowPersistanceString = "6f1cb50b-18fa-4d03-b480-71be56c50053";

+

+    public static readonly Guid guidBvdToolboxCmdSet = new Guid(guidBvdToolboxCmdSetString);

   };

 }
\ No newline at end of file
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 0cf3869e..f5905ea3 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -10,6 +10,7 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidRunVerifier = 0x101;

     public const uint cmdidStopVerifier = 0x102;

     public const uint cmdidMenu = 0x1021;

-    public static int cmdidToggleSnapshotVerification = 0x103;

+    public static uint cmdidToggleSnapshotVerification = 0x103;

+    public const uint cmdidShowErrorModel = 0x104;

   };

 }
\ No newline at end of file
diff --git a/Source/DafnyMenu/Resources.Designer.cs b/Source/DafnyMenu/Resources.Designer.cs
index d934633f..c58dad40 100644
--- a/Source/DafnyMenu/Resources.Designer.cs
+++ b/Source/DafnyMenu/Resources.Designer.cs
@@ -1,7 +1,7 @@
 //------------------------------------------------------------------------------

 // <auto-generated>

 //     This code was generated by a tool.

-//     Runtime Version:4.0.30319.18033

+//     Runtime Version:4.0.30319.18051

 //

 //     Changes to this file may cause incorrect behavior and will be lost if

 //     the code is regenerated.

diff --git a/Source/DafnyMenu/Resources/Images.png b/Source/DafnyMenu/Resources/Images.png
deleted file mode 100644
index 51fe0d15..00000000
--- a/Source/DafnyMenu/Resources/Images.png
+++ /dev/null
diff --git a/Source/DafnyMenu/Resources/Package.ico b/Source/DafnyMenu/Resources/Package.ico
deleted file mode 100644
index 449296f4..00000000
--- a/Source/DafnyMenu/Resources/Package.ico
+++ /dev/null
diff --git a/Source/DafnyMenu/VSPackage.resx b/Source/DafnyMenu/VSPackage.resx
index 8ab9cc50..effe10d4 100644
--- a/Source/DafnyMenu/VSPackage.resx
+++ b/Source/DafnyMenu/VSPackage.resx
@@ -1,14 +1,4 @@
 <?xml version="1.0" encoding="utf-8"?>

-<!--

-    VS SDK Notes: This resx file contains the resources that will be consumed from your package by Visual Studio.

-    For example, Visual Studio will attempt to load resource '400' from this resource stream when it needs to

-    load your package's icon. Because Visual Studio will always look in the VSPackage.resources stream first for

-    resources it needs, you should put additional resources that Visual Studio will load directly into this resx 

-    file. 

-

-    Resources that you would like to access directly from your package in a strong-typed fashion should be stored 

-    in Resources.resx or another resx file.

--->

 <root>

   <!-- 

     Microsoft ResX Schema 

@@ -127,14 +117,10 @@
   <resheader name="writer">

     <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

   </resheader>

-  <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" />

   <data name="110" xml:space="preserve">

     <value>DafnyMenu</value>

   </data>

   <data name="112" xml:space="preserve">

     <value>This is a menu for invoking Dafny.</value>

   </data>

-  <data name="400" type="System.Resources.ResXFileRef, System.Windows.Forms">

-    <value>Resources\Package.ico;System.Drawing.Icon, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a</value>

-  </data>

 </root>
\ No newline at end of file