Make it display maps

1 files changed, 132 insertions, 39 deletions

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index dd39b1b2..ea0544bf 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -27,11 +27,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     }

   }

 

+  enum DataKind

+  {

+    Flat,

+    PhysPtr,

+    SpecPtr,

+    Map

+  }

+

   class VccModel

   {

     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_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[]>();

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

@@ -52,6 +60,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);

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

       f_ptr = m.MkFunc("$ptr", 2);

+      f_map_t = m.MkFunc("$map_t", 2);

     }

 

     public void ComputeNames()

@@ -98,9 +107,26 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       deref = Image(elt, f_spec_ptr_to);

       if (deref != null)

         return TypeName(deref) + "^";

+      var mapt = f_map_t.AppWithResult(elt);

+      if (mapt != null)

+        return string.Format("{1}[{0}]", TypeName(mapt.Args[0]), TypeName(mapt.Args[1]));

+

       foreach (var app in elt.Names)

-        if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^"))

-          return app.Func.Name.Substring(1);

+        if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {

+          var n = app.Func.Name.Substring(1); 

+          switch (n) {

+            case "^i1": return "int8_t";

+            case "^u1": return "uint8_t";

+            case "^i2": return "int16_t";

+            case "^u2": return "uint16_t";

+            case "^i4": return "int32_t";

+            case "^u4": return "uint32_t";

+            case "^i8": return "int64_t";

+            case "^u8": return "uint64_t";

+            case "^bool": return "bool";

+            default: return n;

+          }          

+        }

       return elt.ToString();

     }

 

@@ -132,47 +158,100 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return s2 - s1;

     }

 

-    public Model.Element WrapForUse(Model.Element elt, Model.Element tp)

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

     {

-      var derefPh = Image(tp, f_ptr_to);

-      var derefSp = Image(tp, f_spec_ptr_to);

+      tpl = f_ptr_to.AppWithResult(tp);

+      if (tpl != null) return DataKind.PhysPtr;

+      tpl = f_spec_ptr_to.AppWithResult(tp);

+      if (tpl != null) return DataKind.SpecPtr;

+      tpl = f_map_t.AppWithResult(tp);

+      if (tpl != null) return DataKind.Map;

+      return DataKind.Flat;

+    }

 

-      if (derefPh == null && derefSp == null)

-        return elt;

+    public DataKind GetKind(Model.Element tp)

+    {

+      Model.FuncTuple dummy;

+      return GetKind(tp, out dummy);

+    }

 

-      Model.Element casted = null;

 

-      if (elt.Kind == Model.ElementKind.Integer) {

-        var tmp = f_int_to_ptr.TryEval(elt);

-        if (tmp != null)

-          elt = tmp;

+    public Model.Element WrapForUse(Model.Element elt, Model.Element tp)

+    {

+      Model.FuncTuple tpl;

+      var kind = GetKind(tp, out tpl);

+

+      if (kind == DataKind.Flat) return elt;

+

+      if (kind == DataKind.Map) {

+        if (elt.Kind == Model.ElementKind.Integer) {

+          Model.Element theMap = null;

+          foreach (var conv in model.Functions)

+            // really, we should reconstruct the name of this function, but this is painful

+            if (conv.Arity == 1 && conv.Name.StartsWith("$int_to_map_t")) {

+              var app = conv.AppWithArg(0, elt);

+              if (app != null) {

+                theMap = app.Result;          

+                break;

+              }

+            }

+          if (theMap == null) return elt;

+          return theMap;

+        }

+        return elt;

       }

 

-      if (derefPh != null) {

-        casted = f_phys_ptr_cast.TryEval(elt, derefPh);

-      } else if (derefSp != null) {

-        casted = f_spec_ptr_cast.TryEval(elt, derefSp);

+      if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {

+        if (elt.Kind == Model.ElementKind.Integer) {

+          var tmp = f_int_to_ptr.TryEval(elt);

+          if (tmp != null)

+            elt = tmp;

+        }

       }

 

-      if (casted != null) return casted;

+      if (kind == DataKind.PhysPtr)

+        return Util.OrElse(f_phys_ptr_cast.TryEval(elt, tpl.Args[0]), elt);

+

+      if (kind == DataKind.SpecPtr)

+        return Util.OrElse(f_spec_ptr_cast.TryEval(elt, tpl.Args[0]), elt);

+

+      Util.Assert(false);

       return elt;

     }

 

-    public IEnumerable<FieldNode> GetFields(StateNode state, Model.Element elt, Model.Element tp)

+    public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)

     {

-      var heap = state.state.TryGet("$s");

-      if (heap != null)

-        heap = f_heap.TryEval(heap);

-      if (heap != null) {

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

-          var val = f_select_value.TryEval(fld.Result, elt);

-          if (val != null) {

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

-            val = WrapForUse(val, ftp);

-            yield return new FieldNode(state, FieldName(fld.Args[1]), val, ftp);

+      List<ElementNode> result = new List<ElementNode>();

+      Model.FuncTuple tpl;

+

+      var kind = GetKind(tp, out tpl);

+      if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {

+        var heap = state.state.TryGet("$s");

+        if (heap != null)

+          heap = f_heap.TryEval(heap);

+        if (heap != null) {

+          foreach (var fld in f_select_field.AppsWithArg(0, heap)) {

+            var val = f_select_value.TryEval(fld.Result, elt);

+            if (val != null) {

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

+              val = WrapForUse(val, ftp);

+              result.Add(new FieldNode(state, FieldName(fld.Args[1]), val, ftp));

+            }

           }

+          result.Sort(CompareFields);

         }

+      } else if (kind == DataKind.Map) {

+        var elTp = tpl.Args[1];

+        foreach (var sel in model.Functions)

+          if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {

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

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

+              result.Add(new MapletNode(state, "[" + ElementNames(app.Args[1])[0] + "]", val, elTp));

+            }

+          }

       }

+

+      return result;

     }

 

     public string[] ElementNames(Model.Element elt)

@@ -467,6 +546,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     protected virtual void DoInitChildren()

     {

+      children.AddRange(vm.GetExpansion(stateNode, elt, tp));

     }

 

     protected void InitChildren()

@@ -493,6 +573,24 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

+    public override string ToolTip

+    {

+      get

+      {

+        var sb = new StringBuilder();

+        sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));

+        int limit = 30;

+        foreach (var n in Values){

+          sb.AppendFormat("   = {0}\n", n); 

+          if (limit-- < 0) {

+            sb.Append("...");

+            break;

+          }

+        }

+        return sb.ToString();

+      }

+    }

+

     public override bool Expandable

     {

       get

@@ -520,15 +618,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         name = realName.Substring(idx + 1);

        */

     }

+  }

 

-    protected override void DoInitChildren()

+  class MapletNode : ElementNode

+  {

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

+      : base(par, realName, elt, tp)

     {

-      children.AddRange(vm.GetFields(stateNode, elt, tp));

-      children.Sort(vm.CompareFields);

     }

   }

 

-

   class VariableNode : ElementNode

   {

     public bool updatedHere;

@@ -539,12 +638,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       name = vm.GetUserVariableName(realName);

     }

 

-    protected override void DoInitChildren()

-    {

-      children.AddRange(vm.GetFields(stateNode, elt, tp));

-      children.Sort(vm.CompareFields);

-    }

-

     public override NodeState State

     {

       get