Add interfaces for langauge providers. Start with VCC provider.

7 files changed, 321 insertions, 123 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
new file mode 100644
index 00000000..e2d82fd9
--- /dev/null
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -0,0 +1,132 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer.Base

+{

+  public class Provider : ILanguageProvider

+  {

+    public static Provider Instance = new Provider();

+    private Provider() { }

+

+    public bool IsMyModel(Model m)

+    {

+      return true;

+    }

+

+    public IEnumerable<IDisplayNode> GetStates(Model m)

+    {

+      yield return GenericNodes.Functions(m);

+      yield return GenericNodes.Constants(m);

+      foreach (var s in m.States)

+        yield return new StateNode(s);

+    }

+  }

+

+  public class StateNode : IDisplayNode

+  {

+    protected Model.CapturedState state;

+

+    public StateNode(Model.CapturedState s)

+    {

+      state = s;

+    }

+

+    public virtual string Name

+    {

+      get { return state.Name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { foreach (var v in state.Variables) yield return v; }

+    }

+

+    public virtual bool Expandable { get { return state.VariableCount != 0; } }

+

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var v in state.Variables) {

+        yield return new ElementNode(v, state.TryGet(v));

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+

+  public class ElementNode : IDisplayNode

+  {

+    protected Model.Element elt;

+    protected string name;

+

+    public ElementNode(string name, Model.Element elt)

+    {

+      this.name = name;

+      this.elt = elt;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get

+      {

+        if (!(elt is Model.Uninterpreted))

+          yield return elt.ToString();

+        foreach (var tupl in elt.Names) {

+          if (tupl.Func.Arity == 0)

+            yield return tupl.Func.Name;

+        }

+      }

+    }

+

+    public virtual bool Expandable { get { return false; } }

+    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

+

+    public object ViewSync { get; set; }

+  }

+

+  public static class GenericNodes

+  {

+    public static IDisplayNode Function(Model.Func f)

+    {

+      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);

+    }

+

+    public static IDisplayNode Functions(Model m)

+    {

+      return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);

+    }

+

+    public static IDisplayNode Constants(Model m)

+    {

+      return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);

+    }

+  }

+

+  public class AppNode : ElementNode

+  {

+    protected Model.FuncTuple tupl;

+

+    public AppNode(Model.FuncTuple t)

+      : base(t.Func.Name, t.Result)

+    {

+      tupl = t;

+      var sb = new StringBuilder();

+      sb.Append(t.Func.Name);

+      if (t.Args.Length > 0) {

+        sb.Append("(");

+        foreach (var a in t.Args)

+          sb.Append(a.ToString()).Append(", ");

+        sb.Length -= 2;

+        sb.Append(")");

+      }

+      name = sb.ToString();

+    }

+  }

+

+}

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 7ccf5d54..6f8811e9 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -14,73 +14,12 @@ namespace Microsoft.Boogie.ModelViewer
     object ViewSync { get; set; }

   }

 

-  public class StateNode : IDisplayNode

+  public interface ILanguageProvider

   {

-    protected Model.CapturedState state;

-

-    public StateNode(Model.CapturedState s)

-    {

-      state = s;

-    }

-

-    public virtual string Name

-    {

-      get { return state.Name; }

-    }

-

-    public virtual IEnumerable<string> Values

-    {

-      get { foreach (var v in state.Variables) yield return v; }

-    }

-

-    public virtual bool Expandable { get { return state.VariableCount != 0; } }

-

-    public virtual IEnumerable<IDisplayNode> Expand()

-    {

-      foreach (var v in state.Variables) {

-        yield return new ElementNode(v, state.TryGet(v));

-      }

-    }

-

-    public object ViewSync { get; set; }

-  }

-

-  public class ElementNode : IDisplayNode

-  {

-    protected Model.Element elt;

-    protected string name;

-

-    public ElementNode(string name, Model.Element elt)

-    {

-      this.name = name;

-      this.elt = elt;

-    }

-

-    public virtual string Name

-    {

-      get { return name; }

-    }

-

-    public virtual IEnumerable<string> Values

-    {

-      get

-      {

-        if (!(elt is Model.Uninterpreted))

-          yield return elt.ToString();

-        foreach (var tupl in elt.Names) {

-          if (tupl.Func.Arity == 0)

-            yield return tupl.Func.Name;

-        }

-      }

-    }

-

-    public virtual bool Expandable { get { return false; } }

-    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

-

-    public object ViewSync { get; set; }

+    bool IsMyModel(Model m);

+    IEnumerable<IDisplayNode> GetStates(Model m);

   }

 

-

   public class ContainerNode<T> : IDisplayNode

   {

     protected string name;

@@ -118,43 +57,5 @@ namespace Microsoft.Boogie.ModelViewer
     public object ViewSync { get; set; }

   }

 

-  public static class GenericNodes

-  {

-    public static IDisplayNode Function(Model.Func f)

-    {

-      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);

-    }

-

-    public static IDisplayNode Functions(Model m)

-    {

-      return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);

-    }

-

-    public static IDisplayNode Constants(Model m)

-    {

-      return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);

-    }

-  }

-

-  public class AppNode : ElementNode

-  {

-    protected Model.FuncTuple tupl;

-

-    public AppNode(Model.FuncTuple t)

-      : base(t.Func.Name, t.Result)

-    {

-      tupl = t;

-      var sb = new StringBuilder();

-      sb.Append(t.Func.Name);

-      if (t.Args.Length > 0) {

-        sb.Append("(");

-        foreach (var a in t.Args)

-          sb.Append(a.ToString()).Append(", ");

-        sb.Length -= 2;

-        sb.Append(")");

-      }

-      name = sb.ToString();

-    }

-  }

 

 }

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index f5a988b1..5441c627 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -56,6 +56,7 @@
       this.listView1.DrawSubItem += new System.Windows.Forms.DrawListViewSubItemEventHandler(this.listView1_DrawSubItem);

       this.listView1.MouseMove += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseMove);

       this.listView1.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

+      this.listView1.Resize += new System.EventHandler(this.listView1_Resize);

       // 

       // name

       // 

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 6a19b357..71fc7742 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -17,6 +17,13 @@ namespace Microsoft.Boogie.ModelViewer
   {

     public string SearchText;

 

+    // TODO this should be dynamically loaded

+    IEnumerable<ILanguageProvider> Providers()

+    {

+      yield return Vcc.Provider.Instance;

+      yield return Base.Provider.Instance;

+    }

+

     public Main()

     {

       InitializeComponent();

@@ -29,11 +36,17 @@ namespace Microsoft.Boogie.ModelViewer
         m = models[0];

       }

 

+      ILanguageProvider prov = null;

+      foreach (var p in Providers()) {

+        if (p.IsMyModel(m)) {

+          prov = p;

+          break;

+        }

+      }

+       

       var items = new List<ListViewItem>();

-      items.Add(new DisplayItem(GenericNodes.Functions(m)));

-      items.Add(new DisplayItem(GenericNodes.Constants(m)));

-      foreach (var s in m.States)

-        items.Add(new DisplayItem(new StateNode(s)));

+      foreach (var i in prov.GetStates(m))

+        items.Add(new DisplayItem(i));

       listView1.Items.AddRange(items.ToArray());

 

       listView1.Columns[1].Width = listView1.Width - listView1.Columns[0].Width - 5;

@@ -53,36 +66,45 @@ namespace Microsoft.Boogie.ModelViewer
     const int plusWidth = 16;

 

     static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };

+    static Pen plusPen = new Pen(Color.FromArgb(0xaa, 0xaa, 0xaa));

     

     private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)

     {

       var item = (DisplayItem)e.Item;

       var rect = e.Bounds;

-      rect.Height -= 1;

+      rect.Y += 1;

+      rect.Height -= 2;

 

       var textBrush = Brushes.Black;

-      if ((e.State & ListViewItemStates.Selected) != 0) {

+      if (listView1.SelectedIndices.Count > 0 && listView1.SelectedIndices[0] == e.ItemIndex) {

         // Draw the background and focus rectangle for a selected item.

         e.Graphics.FillRectangle(Brushes.Navy, rect);

-        e.DrawFocusRectangle();

+        // e.DrawFocusRectangle();

         textBrush = Brushes.White;

       } else {

         e.Graphics.FillRectangle(Brushes.White, rect);

       }

 

       var off = levelMult * item.level;

-      var plusRect = rect;

-      plusRect.Width = plusWidth;

-      plusRect.X += off;

-      var plusBorder = plusRect;

-      plusBorder.Height -= 4;

-      plusBorder.Width -= 4;

-      plusBorder.X += 2;

-      plusBorder.Y += 2;

-      e.Graphics.FillRectangle(Brushes.BlueViolet, plusBorder);

-      // TODO these should be icons

-      if (item.displayNode.Expandable)

-        e.Graphics.DrawString(item.expanded ? "-" : "+", listView1.Font, Brushes.Black, plusRect, center);

+

+      {

+        var plusRect = rect;

+        plusRect.Width = plusWidth;

+        plusRect.X += off;

+        var plusBorder = plusRect;

+        plusBorder.Height = 8;

+        plusBorder.Width = 8;

+        plusBorder.X += 4;

+        plusBorder.Y += 3;        

+        e.Graphics.DrawRectangle(plusPen, plusBorder);

+        if (item.displayNode.Expandable) {

+          float midX = plusBorder.X + plusBorder.Width / 2;

+          float midY = plusBorder.Y + plusBorder.Height / 2;

+          e.Graphics.DrawLine(plusPen, plusBorder.X + 2, midY, plusBorder.Right - 2, midY);

+          if (!item.expanded)

+            e.Graphics.DrawLine(plusPen, midX, plusBorder.Y + 2, midX, plusBorder.Bottom - 2);

+        }

+      }

 

       off += plusWidth + 3;

       var nameRect = rect;

@@ -94,7 +116,7 @@ namespace Microsoft.Boogie.ModelViewer
         nameRect.Width = (int)sz.Width + 20;

       nameRect.X += off;

       e.Graphics.DrawString(item.displayNode.Name, font, textBrush, nameRect);

-      

+

       var valRect = rect;

       valRect.X = nameRect.X + nameRect.Width + 4;

       valRect.Width = listView1.Width - valRect.X;

@@ -168,6 +190,11 @@ namespace Microsoft.Boogie.ModelViewer
       listView1.Invalidate();

     }

 

+    private void listView1_Resize(object sender, EventArgs e)

+    {

+      listView1.Invalidate();

+    }

+

   }

 

   internal class DisplayItem : ListViewItem

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 98ca170d..a2d22f30 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -67,6 +67,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="DataModel.cs" />

     <Compile Include="Main.cs">

       <SubType>Form</SubType>

@@ -82,6 +83,7 @@
     <Compile Include="SearchBox.Designer.cs">

       <DependentUpon>SearchBox.cs</DependentUpon>

     </Compile>

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

     <EmbeddedResource Include="Main.resx">

       <DependentUpon>Main.cs</DependentUpon>

     </EmbeddedResource>

@@ -142,4 +144,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
new file mode 100644
index 00000000..e6323045
--- /dev/null
+++ b/Source/ModelViewer/VccProvider.cs
@@ -0,0 +1,134 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer.Vcc

+{

+  public class Provider : ILanguageProvider

+  {

+    public static Provider Instance = new Provider();

+    private Provider() { }

+

+    public bool IsMyModel(Model m)

+    {

+      return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;

+    }

+

+    public IEnumerable<IDisplayNode> GetStates(Model m)

+    {

+      foreach (var s in m.States)

+        yield return new StateNode(s);

+    }

+  }

+

+  public class StateNode : IDisplayNode

+  {

+    protected Model.CapturedState state;

+    protected string name;

+

+    public StateNode(Model.CapturedState s)

+    {

+      name = s.Name;

+      var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

+      if (idx > 0)

+        name = name.Substring(idx + 1);

+      state = s;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { foreach (var v in state.Variables) yield return v; }

+    }

+

+    public virtual bool Expandable { get { return state.VariableCount != 0; } }

+

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var v in state.Variables) {

+        yield return new ElementNode(v, state.TryGet(v));

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+

+  public class ElementNode : IDisplayNode

+  {

+    protected Model.Element elt;

+    protected string name;

+

+    public ElementNode(string name, Model.Element elt)

+    {

+      this.name = name;

+      this.elt = elt;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get

+      {

+        if (!(elt is Model.Uninterpreted))

+          yield return elt.ToString();

+        foreach (var tupl in elt.Names) {

+          if (tupl.Func.Arity == 0)

+            yield return tupl.Func.Name;

+        }

+      }

+    }

+

+    public virtual bool Expandable { get { return false; } }

+    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

+

+    public object ViewSync { get; set; }

+  }

+

+

+  public class ContainerNode<T> : IDisplayNode

+  {

+    protected string name;

+    protected Func<T, IDisplayNode> convert;

+    protected IEnumerable<T> data;

+

+    public ContainerNode(string name, Func<T, IDisplayNode> convert, IEnumerable<T> data)

+    {

+      this.name = name;

+      this.convert = convert;

+      this.data = data;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { yield break; }

+    }

+

+    public virtual bool Expandable { get { return true; } }

+

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var f in data) {

+        var res = convert(f);

+        if (res != null)

+          yield return res;

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+  

+}

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index addb92de..0d40bc21 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1559,6 +1559,7 @@ namespace VC {
 

       // global variables

       foreach (Declaration d in program.TopLevelDeclarations) {

+        if (d is Constant) continue;

         if (d is Variable) {

           AllVariables.Add((Variable)d);

         }