Rework canonical name computation

Sort fields inteligently (allow for override as well)

7 files changed, 214 insertions, 43 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 247021a0..096bb35a 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -27,6 +27,11 @@ namespace Microsoft.Boogie.ModelViewer.Base
     {

       yield return new TopState("TOP", GetStateNodes(m));

     }

+

+    public IEnumerable<string> SortFields(IEnumerable<string> fields)

+    {

+      return Namer.DefaultSortFields(fields);

+    }

   }

 

   public class StateNode : DisplayNode

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index cf599dc1..fe2fd8a3 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -30,6 +30,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

       return dm.states;

     }

+

+    public IEnumerable<string> SortFields(IEnumerable<string> fields)

+    {

+      return Namer.DefaultSortFields(fields);

+    }

   }

 

   class DafnyModel

@@ -189,18 +194,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         return elt;

     }

   }

-  

-  class StateNode : IState

+

+  class StateNode : IState, INamerCallbacks

   {

     internal readonly Model.CapturedState state;

     readonly string name;

     internal readonly DafnyModel dm;

     internal readonly List<VariableNode> vars = new List<VariableNode>();

-    internal readonly Namer namer = new Namer();

+    internal readonly Namer namer;

     internal readonly int index;

     

     public StateNode(int i, DafnyModel parent, Model.CapturedState s)

     {

+      namer = new Namer(this);

       dm = parent;

       state = s;

       index = i;

@@ -248,7 +254,12 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         if (e is Model.Number || e is Model.Boolean)

           namer.AddName(e, new EdgeName(e.ToString()));

       }

-    } 

+    }

+

+    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      return Namer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+    }

 

     internal void ComputeNames()

     {

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index a640055f..05bc6168 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -9,6 +9,23 @@ namespace Microsoft.Boogie.ModelViewer
   {

     bool IsMyModel(Model m);

     IEnumerable<IState> GetStates(Model m);

+    IEnumerable<string> SortFields(IEnumerable<string> fields);

+  }

+

+  public interface INamerCallbacks

+  {

+    // Elements (other than integers and Booleans) get canonical names of the form 

+    // "<base>'<idx>", where <base> is returned by this function, and <idx> is given 

+    // starting with 0, and incrementing when they are conflicts between bases.

+    //

+    // This function needs to return an appropriate base name for the element. It is given

+    // the element, and if possible an IEdgeName in a particular stat that seems to be the

+    // best bet to construct the canonical name from.

+    //

+    // A reasonable strategy is to check if it's a name of the local, and if so return it,

+    // and otherwise use the type of element (e.g., return "seq" for elements representing

+    // sequences). It is also possible to return "" in such cases.

+    string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx);

   }

 

   [Flags]

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 08869c17..64160981 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -19,6 +19,7 @@ namespace Microsoft.Boogie.ModelViewer
     SkeletonItem unfoldingRoot;

     int currentState;

     IState[] states;

+    internal ILanguageProvider langProvider;

 

     // TODO this should be dynamically loaded

     IEnumerable<ILanguageProvider> Providers()

@@ -56,16 +57,18 @@ namespace Microsoft.Boogie.ModelViewer
         m = models[0];

       }

 

-      ILanguageProvider prov = null;

+      this.Text = Path.GetFileName(filename) + " - Boogie Model Viewer";

+

+      langProvider = null;

       foreach (var p in Providers()) {

         if (p.IsMyModel(m)) {

-          prov = p;

+          langProvider = p;

           break;

         }

       }

       

       var items = new List<ListViewItem>();

-      states = prov.GetStates(m).ToArray();

+      states = langProvider.GetStates(m).ToArray();

       unfoldingRoot = new SkeletonItem(this, states.Length);

       unfoldingRoot.PopulateRoot(states);

 

@@ -303,8 +306,9 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

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

-      this.SubItems[1].Text = dispNode.CanonicalValue;

-      this.SubItems[2].Text = aliases;

+      this.SubItems[1].Text = active ? dispNode.CanonicalValue : "";

+      this.SubItems[2].Text = active ? aliases : "";

+      

     }

 

     internal DisplayItem()

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 282a2530..7ac24500 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -23,11 +23,17 @@ namespace Microsoft.Boogie.ModelViewer
 

   public class Namer

   {

+    INamerCallbacks cb;

     internal const int maxScore = 10000;

     List<EltName> eltNames = new List<EltName>();

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

     Dictionary<Model.Element, string> canonicalNames;

 

+    public Namer(INamerCallbacks cb)

+    {

+      this.cb = cb;

+    }

+

     EltName GetName(Model.Element elt)

     {

       EltName res;

@@ -104,6 +110,67 @@ namespace Microsoft.Boogie.ModelViewer
       ComputeBestName();

     }

 

+    public static string DefaultCanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      if (edgeName == null)

+        return "";

+      var name = edgeName.FullName();

+      return name;

+    }

+

+    static bool HasAny(string s, string chrs)

+    {

+      foreach (var c in s)

+        if (chrs.Contains(c))

+          return true;

+      return false;

+    }

+

+    static ulong GetNumber(string s, int beg)

+    {

+      var end = beg;

+      while (end < s.Length && char.IsDigit(s[end]))

+        end++;

+      return ulong.Parse(s.Substring(beg, end - beg)); 

+    }

+

+    public static int CompareFields(string f1, string f2)

+    {

+      bool s1 = HasAny(f1, "[<>]");

+      bool s2 = HasAny(f2, "[<>]");

+      if (s1 && !s2)

+        return -1;

+      if (!s1 && s2)

+        return 1;

+      var len = Math.Min(f1.Length, f2.Length);

+      var numberPos = -1;

+      for (int i = 0; i < len; ++i) {

+        if (char.IsDigit(f1[i]) && char.IsDigit(f2[i])) {

+          numberPos = i;

+          break;

+        }

+        if (f1[i] != f2[i])

+          break;

+      }

+

+      if (numberPos >= 0) {

+        var v1 = GetNumber(f1, numberPos);

+        var v2 = GetNumber(f2, numberPos);

+

+        if (v1 < v2) return -1;

+        else if (v1 > v2) return 1;

+      }

+

+      return string.CompareOrdinal(f1, f2);

+    }

+

+    public static IEnumerable<string> DefaultSortFields(IEnumerable<string> fields_)

+    {

+      var fields = new List<string>(fields_);

+      fields.Sort();

+      return fields;

+    }

+

     public static void ComputeCanonicalNames(IEnumerable<Namer> namers)

     {

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

@@ -111,7 +178,7 @@ namespace Microsoft.Boogie.ModelViewer
       for (int i = 0; i < namersArr.Length; ++i) {

         foreach (var n in namersArr[i].eltNames) {

           n.stateIdx = i;

-          if (n.nodes.Count == 0) continue;

+          //if (n.nodes.Count == 0) continue;

           EltName curr;

           if (names.TryGetValue(n.elt, out curr) && curr.score <= n.score)

             continue;

@@ -119,22 +186,32 @@ namespace Microsoft.Boogie.ModelViewer
         }

       }

 

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

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

+      var usedNames = new Dictionary<string, int>();

+      Model model = null;

       foreach (var n in names.Values) {

-        if (n.elt is Model.Boolean || n.elt is Model.Number)

-          canonicals[n.elt] = n.nodes[0].FullName();

-        else

-          canonicals[n.elt] = "'" + n.nodes[0].FullName() + "-" + n.stateIdx;

+        string name = "";

+        model = n.elt.Model;

+        if (n.nodes.Count == 0) {

+          name = namersArr[0].cb.CanonicalBaseName(n.elt, null, 0);

+          name = AppendIndex(usedNames, name);

+        } else if (n.elt is Model.Boolean || n.elt is Model.Number)

+          name = n.nodes[0].FullName();

+        else {

+          name = namersArr[0].cb.CanonicalBaseName(n.elt, n.nodes[0], n.stateIdx);

+          name = AppendIndex(usedNames, name);

+        }

+        canonicals[n.elt] = name;

       }

 

-      var unnamedIdx = 1;

-

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

         namersArr[i].canonicalNames = canonicals;

-        foreach (var n in namersArr[i].eltNames) {

-          if (!canonicals.ContainsKey(n.elt)) {

-            canonicals[n.elt] = string.Format("${0}", unnamedIdx++);

-          }

+      }

+

+      foreach (var e in model.Elements) {

+        if (!canonicals.ContainsKey(e)) {

+          var name = namersArr[0].cb.CanonicalBaseName(e, null, 0);

+          canonicals[e] = AppendIndex(usedNames, name);

         }

       }

 

@@ -143,10 +220,20 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

+    private static string AppendIndex(Dictionary<string, int> usedNames, string name)

+    {

+      var idx = 0;

+      if (!usedNames.TryGetValue(name, out idx))

+        idx = 0;

+      usedNames[name] = idx + 1;

+      name = name + "'" + idx;

+      return name;

+    }

+

     public virtual string CanonicalName(Model.Element elt)

     {

       string res;

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

+      if (canonicalNames != null && canonicalNames.TryGetValue(elt, out res))

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

       return elt.ToString();

     }

@@ -179,15 +266,9 @@ namespace Microsoft.Boogie.ModelViewer
       Score = args.Length * 10;

     }

 

-    public EdgeName(Namer n, string formatMixed, params Model.Element[] args)

-      : this(n, formatMixed, formatMixed, args)

+    public EdgeName(Namer n, string formatBoth, params Model.Element[] args)

+      : this(n, formatBoth, formatBoth, args)

     {

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

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

-      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) { }

@@ -233,6 +314,15 @@ namespace Microsoft.Boogie.ModelViewer
       var res = new StringBuilder(format.Length);

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

         var c = format[i];

+        var canonical = false;

+

+        if (c == '%' && i < format.Length - 1) {

+          if (format[i + 1] == 'c') {

+            ++i;

+            canonical = true;

+          }

+        }

+

         if (c == '%' && i < format.Length - 1) {

           var j = i + 1;

           while (j < format.Length && char.IsDigit(format[j]))

@@ -240,7 +330,7 @@ namespace Microsoft.Boogie.ModelViewer
           var len = j - i - 1;

           if (len > 0) {

             var idx = int.Parse(format.Substring(i + 1, len));

-            res.Append(namer.ElementName(args[idx]));

+            res.Append(canonical ? namer.CanonicalName(args[idx]) : namer.ElementName(args[idx]));

             i = j - 1;

             continue;

           }

diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index 30998164..08f2b3f0 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -77,19 +77,26 @@ namespace Microsoft.Boogie.ModelViewer
           wasExpanded = true;

 

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

+          var names = new List<string>();

           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.ShortName(), out skelChild)) {

+              var name = child.Name.ShortName();

+              if (!created.TryGetValue(name, out skelChild)) {

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

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

-                children.Add(skelChild);

+                created.Add(name, skelChild);

+                names.Add(name);

+                

               }

               skelChild.displayNodes[i] = child;

             }

           }

+

+          foreach (var name in main.langProvider.SortFields(names)) {

+            children.Add(created[name]);

+          }

         }

       }

     }

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 5fbcb86c..9832bff1 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -23,11 +23,17 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         vm.states.Add(sn);

       }

       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));

+      for (int i = 0; i < 1; i++) {

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

+      }

       return vm.states;

     }

+

+    public IEnumerable<string> SortFields(IEnumerable<string> fields)

+    {

+      return Namer.DefaultSortFields(fields);

+    }

+

   }

 

   enum DataKind

@@ -42,7 +48,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;

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

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

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

 

@@ -58,6 +64,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_heap = m.MkFunc("$heap", 1);

       f_select_field = m.MkFunc("Select_[$field][$ptr]$int", 2);

       f_select_value = m.MkFunc("Select_[$ptr]$int", 2);

+      f_field = m.MkFunc("$field", 1);

       f_field_type = m.MkFunc("$field_type", 1);

       f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);

       f_ptr_to_int = m.MkFunc("$ptr_to_int", 1);

@@ -245,7 +252,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
               var ftp = f_field_type.TryEval(fld.Args[1]);

               val = WrapForUse(val, ftp);

               var nm = ConstantFieldName(fld.Args[1]);

-              var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) { Score = 100 } : new EdgeName(state.namer, "%(%0->%)" + nm, elt) { Score = 10 };

+              var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) { Score = 100 } : new EdgeName(state.namer, "%0->" + nm, nm, elt) { Score = 10 };

               result.Add(new FieldNode(state, edgname, val, ftp));

             }

           }

@@ -257,7 +264,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {

             foreach (var app in sel.AppsWithArg(0, elt)) {

               var val = WrapForUse(app.Result, elTp);

-              var edgname = new EdgeName(state.namer, "%(%0%)[%1]", elt, app.Args[1]) { Score = 20 };

+              var edgname = new EdgeName(state.namer, "%0[%c1]", "[%c1]", elt, app.Args[1]) { Score = 20 };

               result.Add(new MapletNode(state, edgname, val, elTp));

             }

           }

@@ -266,8 +273,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return result;

     }

   }

-  

-  class StateNode : IState

+

+  class StateNode : IState, INamerCallbacks

   {

     internal Model.CapturedState state;

     string name;

@@ -278,7 +285,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     

     public StateNode(int i, VccModel parent, Model.CapturedState s)

     {

-      this.namer = new Namer();

+      this.namer = new Namer(this);

       this.vm = parent;

       state = s;

       index = i;

@@ -301,6 +308,36 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       SetupVars();

     }

 

+    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      var name = Namer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+

+      if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

+        name = "";

+

+      if (name != "")

+        return name;

+

+      foreach (var tpl in elt.References) {

+        var fn = tpl.Func;

+        if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

+          return "map";

+        if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)

+          return "map";

+      }

+

+      var fld = vm.f_field.TryEval(elt);

+      if (fld != null) {

+        var tp = vm.f_field_type.TryEval(fld);

+        if (tp != null) {

+          return vm.TypeName(tp);

+        }

+      }

+

+      // return elt.ToString(); // for debugging

+      return "";

+    }

+

     void SetupVars()

     {

       if (vars != null) return;