VCC: improvements in showing arrays, addresses, and embeddings

2 files changed, 51 insertions, 21 deletions

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index fce9522d..49ff93ea 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -106,6 +106,7 @@ namespace Microsoft.Boogie.ModelViewer
     public virtual string CanonicalName(Model.Element elt)

     {

       string res;

+      if (elt == null) return "?";

       if (canonicalName.TryGetValue(elt, out res)) return res;

       NameSeqSuffix suff;

       var baseName = CanonicalBaseName(elt, out suff);

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index cbaecbd8..b5ba6c22 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
                                f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,

                                f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field, f_idx, f_field_plus,

                                f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array, f_active_option, f_int_to_field,

-                               f_blob_type, f_array_emb, f_addr, f_address_root;

+                               f_blob_type, f_array_emb, f_addr, f_address_root, f_base, f_field_arr_size, f_field_arr_root, f_field_arr_index;

     public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset, tp_heaptp;

     public readonly Model.Element elt_me, elt_null;

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

@@ -95,7 +95,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_blob_type = m.MkFunc("$blob_type", 1);

       f_array_emb = m.MkFunc("$array_emb", 2);

       f_addr = m.MkFunc("$addr", 1);

+      f_base = m.MkFunc("$base", 1);

       f_address_root = m.MkFunc("$address_root", 2);

+      f_field_arr_index = m.MkFunc("$field_arr_index", 1);

+      f_field_arr_size = m.MkFunc("$field_arr_size", 1);

+      f_field_arr_root = m.MkFunc("$field_arr_root", 1);

 

       tp_bool = m.GetFunc("^^bool").GetConstant();

       tp_mathint = m.GetFunc("^^mathint").GetConstant();

@@ -233,7 +237,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     static string[][] totals = new string[][] {

       new string[] {

-      "$addr", "$current_timestamp", 

+      "$current_timestamp", 

       "$full_stop", "$function_entry", "$ptr_to_i4",

       "$ptr_to_i8", "$ptr_to_u4", "$ptr_to_u8", 

       "$span", "$sizeof", "$in_domain", 

@@ -246,7 +250,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       },

 

       new string[] {

-      "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr",

+      "$addr", "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr",

       "$in_range_spec_ptr", "$is_sequential_field", "$is_volatile_field",

       "$is_ghost_field", "$is_phys_field", "$is_math_type", "$invok_state",

       "$is_primitive",

@@ -793,6 +797,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

+    void AddPointerFunction(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func fn, Model.Element tp)

+    {

+      if (elt == null) return;

+

+      var val = fn.TryEval(elt);

+      if (val != null) {

+        res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });

+      }

+    }

+

     void AddPtrType(StateNode state, Model.Element elt, List<ElementNode> res)

     {

       var f = f_field.TryEval(elt);

@@ -924,32 +938,45 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }

 

         if (elt != null) {

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

-            var addr = app.Result;

-            Model.Element val = null, atp = tp;

-

-            addresses.Add(app.Result);

-

-            foreach (var papp in f_ptr.AppsWithResult(addr)) {

-              var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[0]), papp.Args[1]);

-              if (tmp != null) {

-                val = tmp;

-                var tt = f_field_type.TryEval(papp.Args[0]);

-                if (tt != null) atp = tt;

+          var eltBase = f_base.TryEval(elt);

+          var eltField = f_field.TryEval(elt);

+          if (eltBase != null && eltField != null) {

+            foreach (var app in f_field_plus.AppsWithArg(0, eltField)) {

+              var fieldName = app.Result;

+              var addr = f_ptr.TryEval(fieldName, eltBase);

+              if (addr == null) continue;

+

+              Model.Element val = null, atp = tp;

+

+              addresses.Add(addr);

+

+              foreach (var papp in f_ptr.AppsWithResult(addr)) {

+                var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[0]), papp.Args[1]);

+                if (tmp != null) {

+                  val = tmp;

+                  var tt = f_field_type.TryEval(papp.Args[0]);

+                  if (tt != null) atp = tt;

+                }

               }

-            }

 

-            if (val != null)

-              val = WrapForUse(val, atp);

-            result.Add(new MapletNode(state, new EdgeName(this, "[%0]", app.Args[1]), val, atp) { Category = NodeCategory.Maplet });

-            if (addr != null)

-              result.Add(new MapletNode(state, new EdgeName(this, "&[%0]", app.Args[1]), addr, GuessPtrTo(atp)) { Category = NodeCategory.Maplet });

+              if (val != null)

+                val = WrapForUse(val, atp);

+              result.Add(new MapletNode(state, new EdgeName(this, "[%0]", app.Args[1]), val, atp) { Category = NodeCategory.Maplet });

+              if (addr != null)

+                result.Add(new MapletNode(state, new EdgeName(this, "&[%0]", app.Args[1]), addr, GuessPtrTo(atp)) { Category = NodeCategory.Maplet });

+            }

           }

         }

 

         if (elt != null) {

           foreach (var ptr in f_ptr.AppsWithArg(1, elt)) {

             if (addresses.Contains(ptr.Result)) continue;

+            var fld = ptr.Args[0];

+            var idx = f_field_arr_index.TryEval(fld);

+            if (idx != null) {

+              var xtp = f_field_type.TryEval(fld);

+              result.Add(new MapletNode(state, new EdgeName(this, "&[%0] of %1", idx, f_field_arr_size.TryEval(fld)), ptr.Result, GuessPtrTo(xtp)) { Category = NodeCategory.Maplet });

+            }

             if (!IsConstantField(ptr.Args[0])) continue;

             BuildFieldNode(result, state, ptr.Result, ptr.Args[0], null, ptr.Result);

           }

@@ -959,6 +986,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         AddSpecialField(state, elt, result, "\\owner", f_owners);

         AddSpecialField(state, elt, result, "\\root", f_roots);

         AddSpecialField(state, elt, result, "\\timestamp", f_timestamps);

+        AddPointerFunction(state, elt, result, "\\embedding", f_base, tp_object);

+        AddPointerFunction(state, elt, result, "\\addr", f_addr, tp_mathint);

 

         if (viewOpts.ViewLevel >= 1 && elt != null) {

           AddPtrType(state, elt, result);