More work on the generic namer

5 files changed, 77 insertions, 55 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index de0121e9..c2ffdf4b 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -167,6 +167,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     public static IEnumerable<T> Singleton<T>(T e) { yield return e; }

 

+    public static IEnumerable<T> Concat1<T>(this IEnumerable<T> s, T e) { return s.Concat(Singleton(e)); }

+

     public static IEnumerable<T> Map<S, T>(this IEnumerable<S> inp, Func<S, T> conv)

     {

       foreach (var s in inp) yield return conv(s);

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index e538e8b3..8da0166f 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -136,12 +136,13 @@ namespace Microsoft.Boogie.ModelViewer
       if (!item.active)

         textBrush = grayedOut;

 

-      var sz = e.Graphics.MeasureString(item.dispNode.Name.FullName(), font);

+      var dispName = item.dispNode.Name.ShortName();

+      var sz = e.Graphics.MeasureString(dispName, font);

       nameRect.Width = currentStateView.Columns[0].Width - 1 - off;

       if (nameRect.Width < sz.Width + 2)

         nameRect.Width = (int)sz.Width + 20;

       nameRect.X += off;

-      e.Graphics.DrawString(item.dispNode.Name.FullName(), font, textBrush, nameRect);

+      e.Graphics.DrawString(dispName, font, textBrush, nameRect);

 

       var valRect = rect;

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

@@ -269,7 +270,7 @@ namespace Microsoft.Boogie.ModelViewer
         this.ToolTipText = values;

       }

 

-      this.SubItems[0].Text = dispNode.Name.FullName();

+      this.SubItems[0].Text = dispNode.Name.ShortName();

       this.SubItems[1].Text = values;

     }

 

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 772c3c78..30e0c65b 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -9,9 +9,9 @@ namespace Microsoft.Boogie.ModelViewer
   {

     internal Model.Element elt;

     internal List<IEdgeName> nodes = new List<IEdgeName>();

-    internal IEdgeName minName;

     internal int score = 10000;

     internal string theName;

+    internal bool unfolded;

 

     internal EltName(Model.Element e)

     {

@@ -38,31 +38,30 @@ namespace Microsoft.Boogie.ModelViewer
 

     int EdgeNameScore(IEdgeName name)

     {

-      return name.Dependencies.Select(e => GetName(e).score).Max() + name.Score;

+      return name.Dependencies.Select(e => GetName(e).score).Concat1(0).Max() + name.Score;

     }

 

     void ComputeBestName()

     {

       while (true) {

         var changes = 0;

-        foreach (var elt in eltNames) {

-          foreach (var edge in elt.nodes) {

-            var newScore = EdgeNameScore(edge);

-            if (newScore < elt.score) {

-              elt.score = newScore;

-              elt.minName = edge;

-              changes++;

-            }

+        var thisElts = eltNames.ToArray();

+        foreach (var elt in thisElts) {

+          var newScore = elt.nodes.Select(EdgeNameScore).Concat1(int.MaxValue).Min();

+          if (newScore < elt.score) {

+            elt.score = newScore;

+            changes++;

           }

         }

-        if (changes == 0)

+        if (changes == 0 && thisElts.Length == eltNames.Count)

           break;

       }

       eltNames.Sort((x,y) => x.score - y.score);

       foreach (var elt in eltNames) {

-        if (elt.minName == null)

-          elt.minName = elt.nodes[0];

-        elt.theName = elt.minName.FullName();

+        if (elt.nodes.Count > 0) {

+          elt.nodes.Sort((x, y) => EdgeNameScore(x) - EdgeNameScore(y));

+          elt.theName = elt.nodes[0].FullName();

+        }

       }

     }

 

@@ -71,8 +70,9 @@ namespace Microsoft.Boogie.ModelViewer
       if (n.Element != null) {

         var prev = GetName(n.Element);

         prev.nodes.Add(n.Name);

-        if (prev.nodes.Count > 1) // we've already been here

+        if (prev.unfolded) // we've already been here

           return;

+        prev.unfolded = true;

       }

 

       if (!n.Expandable) return;

@@ -82,6 +82,12 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

+    public void AddName(Model.Element elt, IEdgeName name)

+    {

+      var e = GetName(elt);

+      e.nodes.Add(name);

+    }

+

     public void ComputeNames(IEnumerable<IDisplayNode> n)

     {

       n.Iter(Unfold);

@@ -92,6 +98,11 @@ namespace Microsoft.Boogie.ModelViewer
     {

       return GetName(elt).theName;

     }

+

+    public virtual IEnumerable<IEdgeName> Aliases(Model.Element elt)

+    {

+      return GetName(elt).nodes;

+    }

   }

 

   public class EdgeName : IEdgeName

@@ -116,8 +127,10 @@ namespace Microsoft.Boogie.ModelViewer
     {

       var beg = formatMixed.IndexOf("%(");

       var end = formatMixed.IndexOf("%)");

-      if (beg >= 0 && end > beg)

+      if (beg >= 0 && end > beg) {

         this.formatShort = formatMixed.Substring(0, beg) + formatMixed.Substring(end + 2);

+        this.formatFull = formatMixed.Replace("%(", "").Replace("%)", "");

+      }

     }

 

     public EdgeName(string name) : this(null, name, emptyArgs) { }

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index 3d7384ad..30998164 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -76,15 +76,15 @@ namespace Microsoft.Boogie.ModelViewer
           if (wasExpanded) return;

           wasExpanded = true;

 

-          var created = new Dictionary<IEdgeName, SkeletonItem>();

+          var created = new Dictionary<string, SkeletonItem>();

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

             var dn = displayNodes[i];

             if (dn == null || !dn.Expandable) continue;

             foreach (var child in dn.Expand()) {

               SkeletonItem skelChild;

-              if (!created.TryGetValue(child.Name, out skelChild)) {

+              if (!created.TryGetValue(child.Name.ShortName(), out skelChild)) {

                 skelChild = new SkeletonItem(child.Name, this);

-                created.Add(child.Name, skelChild);

+                created.Add(child.Name.ShortName(), skelChild);

                 children.Add(skelChild);

               }

               skelChild.displayNodes[i] = child;

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 30ec3def..4aad9a25 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -22,7 +22,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var sn = new StateNode(vm, s);

         vm.states.Add(sn);

       }

-      vm.ComputeNames();

       return vm.states;

     }

   }

@@ -40,8 +39,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public readonly Model model;

     public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,

                                f_select_value, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;

-    Dictionary<Model.Element, string> primaryName = new Dictionary<Model.Element, string>();

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

+    Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

     public List<StateNode> states = new List<StateNode>();

 

     public VccModel(Model m)

@@ -63,14 +61,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_map_t = m.MkFunc("$map_t", 2);

     }

 

-    public void ComputeNames()

-    {

-      //var namer = new Namer(this);

-      //allNames = namer.ComputeNames();

-      foreach (var e in allNames)

-        primaryName[e.Key] = e.Value[0];

-    }

-

     public string GetUserVariableName(string name)

     {

       if (name.StartsWith("L#") || name.StartsWith("P#"))

@@ -133,33 +123,44 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public string TypeName(Model.Element elt)

     {

       string res;

-      if (!primaryName.TryGetValue(elt, out res)) {

-        primaryName[elt] = elt.ToString(); // avoid infinite recursion

+      if (!typeName.TryGetValue(elt, out res)) {

+        typeName[elt] = elt.ToString(); // avoid infinite recursion

         res = TypeNameCore(elt);

-        primaryName[elt] = res;

+        typeName[elt] = res;

       }

       return res;

     }

 

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

+

     public string ConstantFieldName(Model.Element elt)

     {

       var bestScore = int.MaxValue;

       string bestName = null;

 

       foreach (var t in elt.Names) {

+        var score = int.MaxValue;

+        string name = null;

         if (t.Args.Length == 0) {

-          var name = t.Func.Name;

-          var score = 0;

-          if (name.Contains('.')) score += 10;

-          if (name.Contains('#')) score -= 1;

-          if (score < bestScore) {

-            bestScore = score;

-            bestName = name;

+          name = t.Func.Name;

+          score = 0;

+          var dotIdx = name.IndexOf('.');

+          if (dotIdx > 0) {

+            score += 10;

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

           }

+          if (name.Contains('#')) score -= 1;

+        } else if (synthethic_fields.Contains(t.Func.Name)) {

+          name = string.Format("{0}<{1}>", t.Func.Name.Substring(3), TypeName(t.Args[0]));

+          score = 5;

+        }

+        if (score < bestScore) {

+          bestScore = score;

+          bestName = name;

         }

       }

 

-      return bestName;    

+      return bestName;

     }

 

     public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)

@@ -260,15 +261,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       return result;

     }

-

-    public string[] ElementNames(Model.Element elt)

-    {

-      string[] res;

-      if (allNames.TryGetValue(elt, out res))

-        return res;

-      return new string[] { elt.ToString() };

-    }

-

   }

 

 #if false

@@ -498,7 +490,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       if (vm.states.Count > 0) {

         var prev = vm.states.Last();

-        names = prev.vars.Map(v => v.Name.FullName());

+        names = prev.vars.Map(v => v.realName);

       }

 

       names = names.Concat(state.Variables).Distinct();

@@ -515,6 +507,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }

       }

 

+      ComputeNames();

+    }

+

+    void ComputeNames()

+    {

+      foreach (var e in vm.model.Elements) {

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

+        if (n != null)

+          namer.AddName(n, new EdgeName(n.ToString()));

+      }

       namer.ComputeNames(vars);

     }

 

@@ -575,7 +577,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     {

       get

       {

-        return vm.ElementNames(Element);

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

+          if (edge != Name)

+            yield return edge.FullName();

       }

     }

 

@@ -637,10 +641,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   class VariableNode : ElementNode

   {

     public bool updatedHere;

+    public string realName;

 

     public VariableNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

       : base(par, realName, elt, tp)

     {

+      this.realName = realName;

       name = new EdgeName(vm.GetUserVariableName(realName));

     }