Handle aliases better

4 files changed, 20 insertions, 194 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index eae222aa..46125e74 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -30,12 +30,12 @@
       this.currentStateView = new System.Windows.Forms.ListView();

       this.name = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.value = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

+      this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.splitContainer1 = new System.Windows.Forms.SplitContainer();

       this.stateList = new System.Windows.Forms.ListView();

       this.columnHeader3 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.columnHeader1 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.columnHeader2 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

-      this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit();

       this.splitContainer1.Panel1.SuspendLayout();

       this.splitContainer1.Panel2.SuspendLayout();

@@ -80,6 +80,11 @@
       this.value.Text = "Value";

       this.value.Width = 99;

       // 

+      // aliases

+      // 

+      this.aliases.Text = "Aliases";

+      this.aliases.Width = 325;

+      // 

       // splitContainer1

       // 

       this.splitContainer1.Dock = System.Windows.Forms.DockStyle.Fill;

@@ -107,6 +112,7 @@
       this.stateList.FullRowSelect = true;

       this.stateList.GridLines = true;

       this.stateList.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable;

+      this.stateList.HideSelection = false;

       this.stateList.Location = new System.Drawing.Point(0, 0);

       this.stateList.MultiSelect = false;

       this.stateList.Name = "stateList";

@@ -132,11 +138,6 @@
       this.columnHeader2.Text = "Value";

       this.columnHeader2.Width = 116;

       // 

-      // aliases

-      // 

-      this.aliases.Text = "Aliases";

-      this.aliases.Width = 325;

-      // 

       // Main

       // 

       this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 800455f0..609bf571 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -223,8 +223,15 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void stateList_SelectedIndexChanged(object sender, EventArgs e)

     {

+

       if (stateList.SelectedItems.Count == 0) return;

       var sel = stateList.SelectedItems[0].Index;

+

+      var normalFont = stateList.Font;

+      var boldFont = new Font(normalFont, FontStyle.Bold);

+      stateList.Items[currentState].Font = normalFont;

+      stateList.Items[sel].Font = boldFont;

+

       SetState(sel);

     }

 

@@ -294,7 +301,10 @@ namespace Microsoft.Boogie.ModelViewer
       if (dn == null) return "";

 

       var sb = new StringBuilder();

+      var canon = dn.CanonicalValue;

       foreach (var n in dn.Aliases) {

+        if (n == canon)

+          continue;

         sb.Append(n).Append(", ");

         if (sb.Length > 300)

           break;

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 859b718a..5d9f41d9 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -147,7 +147,7 @@ namespace Microsoft.Boogie.ModelViewer
     {

       string res;

       if (canonicalNames.TryGetValue(elt, out res))

-        return res;

+        return res; // +" " + elt.ToString();

       return elt.ToString();

     }

 

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index cabc6171..5fbcb86c 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -25,6 +25,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       foreach (var s in vm.states) s.ComputeNames();

       Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

       Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

+      // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

       return vm.states;

     }

   }

@@ -265,192 +266,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return result;

     }

   }

-

-#if false

-  class Namer

-  {

-    VccModel vm;

-    Model model { get { return vm.model; } }

-    List<StateNode> states { get { return vm.states; } }

-

-    internal Namer(VccModel v) { vm = v; }

-

-    public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root" };

-    Dictionary<Model.Element, List<EltName>> names = new Dictionary<Model.Element, List<EltName>>();

-    Dictionary<Model.Element, EltName> bestNameFor = new Dictionary<Model.Element, EltName>();

-    List<EltName> resolutionOrder = new List<EltName>();

-    Dictionary<Model.Element, string[]> finalNames = new Dictionary<Model.Element, string[]>();

-

-

-    class EltName

-    {

-      public Model.Element For;

-      public int Score;

-      public string Format;

-      public Model.Element[] Arguments;

-      public string Resolved;

-    }

-

-    private void AddName(Model.Element elt, int sc, string fmt, params Model.Element[] args)

-    {

-      List<EltName> l;

-      if (!names.TryGetValue(elt, out l)) {

-        l = new List<EltName>();

-        names.Add(elt, l);

-      }

-      l.Add(new EltName() { Arguments = args, Format = fmt, Score = sc, For = elt });

-    }

-

-    private void AddAnyName(Model.Element elt)

-    {

-      if (names.ContainsKey(elt)) return;

-      var nm = new EltName() { Arguments = new Model.Element[0], Format = string.Format("<{0}>", elt.ToString()), Score = 50, For = elt };

-      var l = new List<EltName>();

-      l.Add(nm);

-      names[elt] = l;

-    }

-

-    private int GetApproxScore(Model.Element e)

-    {

-      EltName n;

-      if (bestNameFor.TryGetValue(e, out n))

-        return n.Score;

-      return 100;

-    }

-

-    private int CompareNames(EltName x, EltName y)

-    {

-      if (x == y) return 0;

-      if (x.Score == y.Score) {

-        if (x.Arguments.Length == y.Arguments.Length)

-          return x.Arguments.Map(GetApproxScore).Sum() - y.Arguments.Map(GetApproxScore).Sum();

-        else

-          return x.Arguments.Length - y.Arguments.Length;

-      } else {

-        return x.Score - y.Score;

-      }

-    }

-

-

-    private void WorkOutBestNameFor(Model.Element e)

-    {

-      if (bestNameFor.ContainsKey(e)) return;

-      if (!names.ContainsKey(e)) AddAnyName(e);

-      var nm = names[e];

-      nm.Sort(CompareNames);

-      var best = nm[0];

-      bestNameFor[e] = best;

-      foreach (var a in best.Arguments)

-        WorkOutBestNameFor(a);

-      resolutionOrder.Add(best);

-    }

-

-    private void ResolveNames()

-    {

-      var keys = names.Keys.ToArray();

-      foreach (var e in keys)

-        WorkOutBestNameFor(e);

-      var res1 = resolutionOrder.ToArray();

-      foreach (var nm in res1) {

-        var nms = names[nm.For];

-        foreach (var subname in nms.Skip(1)) {

-          subname.Arguments.Iter(WorkOutBestNameFor);

-          resolutionOrder.Add(subname);

-        }

-      }

-

-      foreach (var nm in resolutionOrder) {

-        var s = nm.Format;

-        for (int i = nm.Arguments.Length - 1; i >= 0; --i) {

-          var argName = bestNameFor[nm.Arguments[i]];

-          var strName = argName.Resolved;

-          if (strName == null) strName = argName.For.ToString();

-          s = s.Replace("&" + i, strName);

-        }

-        nm.Resolved = s;

-      }

-

-      foreach (var e in names) {

-        finalNames[e.Key] = e.Value.Map(n => n.Resolved).ToArray();

-      }

-    }

-

-    public Dictionary<Model.Element,string[]> ComputeNames()

-    {

-      ComputeFields();

-      ComputeLocals();

-      ComputeLiterals();

-      ComputeFieldRefs();

-

-      ResolveNames();

-

-      return finalNames;

-    }

-

-    private void ComputeFieldRefs()

-    {

-      var fieldStateId = new Dictionary<Model.Element, int>();

-      for (int i = 0; i < states.Count; ++i) {

-        var hp = vm.f_heap.TryEval(states[i].state.TryGet("$s"));

-        foreach (var fld in vm.f_select_field.AppsWithArg(0, hp)) {

-          if (!fieldStateId.ContainsKey(fld.Result)) {

-            fieldStateId[fld.Result] = i;

-            foreach (var sel in vm.f_select_value.AppsWithArg(0, fld.Result)) {

-              var val = sel.Result;

-              var ftp = vm.f_field_type.TryEval(fld.Args[1]);

-              val = vm.WrapForUse(val, ftp);

-              AddName(val, 20, string.Format("&0->&1.{0}", i), sel.Args[1], fld.Args[1]);

-            }

-          }

-        }

-      }

-    }

-

-    private void ComputeLiterals()

-    {

-      foreach (var e in model.Elements) {

-        Model.Number n = e as Model.Number;

-        if (n != null)

-          AddName(n, 5, n.ToString());

-      }

-    }

-

-    private void ComputeLocals()

-    {

-      var defined = new HashSet<Tuple<Model.Element, string>>();

-      for (int i = 0; i < states.Count; ++i) {

-        foreach (var v in states[i].vars) {

-          var t = Tuple.Create(v.Element, v.Name);

-          if (!defined.Contains(t)) {

-            defined.Add(t);

-            AddName(v.Element, 10, string.Format("{0}.{1}", v.Name, i));

-          }

-        }

-      }

-    }

-

-    private void ComputeFields()

-    {

-      var fields = vm.f_select_field.Apps.Map(a => a.Args[1]).Concat(vm.f_ptr.Apps.Map(a => a.Args[0]));

-      foreach (var f in fields) {

-        foreach (var fn in synthethic_fields) {

-          foreach (var tpl in model.MkFunc(fn, 1).AppsWithResult(f))

-            AddName(f, 5, string.Format("{0}<{1}>", fn.Substring(3), vm.TypeName(tpl.Args[0])));

-        }

-        foreach (var nm in f.Names) {

-          if (nm.Func.Arity == 0) {

-            var n = nm.Func.Name;

-            var idx = n.LastIndexOf('.');

-            if (idx > 0) n = n.Substring(idx + 1);

-            AddName(f, 5, n);

-          }

-        }

-        AddAnyName(f);

-      }

-    }

-

-  }

-#endif

   

   class StateNode : IState

   {

@@ -592,7 +407,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           yield break;

         } else {

           foreach (var edge in stateNode.namer.Aliases(Element))

-            if (edge != Name)

+            if (!edge.Equals(Name))

               yield return edge.FullName();

         }

       }