VCC: Better display of data type values

1 files changed, 78 insertions, 13 deletions

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 4354ddc3..27d6422b 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -48,9 +48,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public List<StateNode> states = new List<StateNode>();

     public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();

 

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

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

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

+

     Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();

 

     public const string selfMarker = "\\self";

+    public const int maxDatatypeNameLength = 5;

 

     public VccModel(Model m, ViewOptions opts)

       : base(m, opts)

@@ -1202,7 +1207,63 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

-    private string CanonicalBaseNameCore(string name, Model.Element elt)

+    private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)

+    {

+      Model.FuncTuple ctor = null;

+      int len = 1;

+      string dataTypeType = null;

+      foreach (var app in elt.References) {

+        var n = app.Func.Name;

+        if (app.Result == elt && n.StartsWith("DF#")) {

+          ctor = app;

+        }

+        var tmp = DataTypeName(elt, app);

+        if (tmp != null) dataTypeType = tmp;

+      }

+

+      if (dataTypeType != null) {

+        if (ctor != null && ctor.Args.Length == 0)

+          sb.Append(ctor.Func.Name.Substring(3));

+        else

+          sb.Append(DataTypeShortName(elt, dataTypeType));

+        if (level > 0 && ctor != null && ctor.Args.Length > 0) {

+          sb.Append("(");

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

+            if (i != 0) sb.Append(", ");

+            len += DataTypeToString(sb, level - 1, ctor.Args[i]);

+          }

+          sb.Append(")");

+        }

+      }

+      return len;

+    }

+

+    private string DataTypeShortName(Model.Element elt, string tp)

+    {

+      string res;

+      if (datatypeShortName.TryGetValue(elt, out res)) return res;

+

+      var baseName = tp;

+

+      var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);

+      if (hd != null) {

+        foreach (var nm in hd.References) {

+          if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))

+            baseName = nm.Func.Name.Substring(3);

+        }

+      }

+

+      var useCnt = 0;

+      if (!datatypePrefixUse.TryGetValue(baseName, out useCnt))

+        useCnt = -1;

+      useCnt++;

+      datatypePrefixUse[baseName] = useCnt;

+      res = baseName + "." + useCnt.ToString();

+      datatypeShortName[elt] = res;

+      return res;

+    }

+

+    private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)

     {

       var vm = this;

 

@@ -1234,18 +1295,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

         var dtpName = DataTypeName(elt, tpl);

         if (dtpName != null) {

-          var dgh = model.TryGetFunc("DGH#" + dtpName);

-          if (dgh != null) {

-            var hd = dgh.TryEval(elt);

-            if (hd != null) {

-              foreach (var nm in hd.References) {

-                if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))

-                  return nm.Func.Name.Substring(3);

-              }

-

-            }

+          var sb = new StringBuilder();

+          string prev = null;

+          for (int lev = 0; lev < 10; lev++) {

+            sb.Length = 0;

+            var len = DataTypeToString(sb, lev, elt);

+            if (prev == null || len <= maxDatatypeNameLength)

+              prev = sb.ToString();

           }

-          return dtpName;

+

+          datatypeLongName[elt] = prev;

+          suff = NameSeqSuffix.None;

+          return prev;

         }

       }

 

@@ -1272,9 +1333,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         suff = NameSeqSuffix.None;

         return lit;

       }

+      if (datatypeLongName.TryGetValue(elt, out lit)) {

+        suff = NameSeqSuffix.None;

+        return lit;

+      }

       

       var name = base.CanonicalBaseName(elt, out suff);

-      name = CanonicalBaseNameCore(name, elt);

+      name = CanonicalBaseNameCore(name, elt, true, ref suff);

      

       return name;

     }