Implement find-all-names

1 files changed, 312 insertions, 46 deletions

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

         vm.states.Add(sn);

       }

+      vm.ComputeNames();

       return vm.states;

     }

   }

@@ -29,7 +30,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   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;

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

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

 

     public VccModel(Model m)

     {

@@ -46,9 +51,17 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       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);

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

+    }

+

+    public void ComputeNames()

+    {

+      var namer = new Namer(this);

+      allNames = namer.ComputeNames();

+      foreach (var e in allNames)

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

     }

 

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

     public string GetUserVariableName(string name)

     {

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

@@ -77,59 +90,292 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return null;

     }

 

-    public string ConstantName(Model.Element elt)

+    string TypeNameCore(Model.Element elt)

+    {

+      var deref = Image(elt, f_ptr_to);

+      if (deref != null)

+        return TypeName(deref) + "*";

+      deref = Image(elt, f_spec_ptr_to);

+      if (deref != null)

+        return TypeName(deref) + "^";

+      foreach (var app in elt.Names)

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

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

+      return elt.ToString();

+    }

+

+    public string TypeName(Model.Element elt)

     {

-      foreach (var n in elt.Names) {

-        if (n.Func.Arity == 0)

-          return n.Func.Name;

+      string res;

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

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

+        res = TypeNameCore(elt);

+        primaryName[elt] = res;

       }

-      return "<unknown>";

+      return res;

     }

 

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

+    public string FieldName(Model.Element elt)

     {

-      var deref = Image(tp, f_ptr_to);

+      return primaryName[elt];

+    }

+

+    public int CompareFields(ElementNode f1, ElementNode f2)

+    {

+      var n1 = f1.Name;

+      var n2 = f2.Name;

+      int s1 = n1.Contains('<') ? 1 : 0;

+      int s2 = n2.Contains('<') ? 1 : 0;

+      if (s1 == s2)

+        return string.CompareOrdinal(n1, n2);

+      else

+        return s2 - s1;

+    }

+

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

+    {

+      var derefPh = Image(tp, f_ptr_to);

+      var derefSp = Image(tp, f_spec_ptr_to);

+

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

+        return elt;

+

       Model.Element casted = null;

 

-      var ptrElt = elt;

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

-        ptrElt = f_int_to_ptr.TryEval(ptrElt);        

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

+        var tmp = f_int_to_ptr.TryEval(elt);

+        if (tmp != null)

+          elt = tmp;

       }

 

-      if (deref != null) {

-        casted = f_phys_ptr_cast.TryEval(ptrElt, deref);

+      if (derefPh != null) {

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

+      } else if (derefSp != null) {

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

+      }

+

+      if (casted != null) return casted;

+      return elt;

+    }

+

+    public IEnumerable<FieldNode> GetFields(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);

+          }

+        }

+      }

+    }

+

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

+    {

+      string[] res;

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

+        return res;

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

+    }

+

+  }

+

+  class Namer

+  {

+    VccModel vm;

+    Model model { get { return vm.model; } }

+    List<StateNode> states { get { return vm.states; } }

+

+    internal Namer(VccModel v) { vm = v; }

+

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

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

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

+    List<EltName> resolutionOrder = new List<EltName>();

+    Dictionary<Model.Element, string[]> finalNames = new Dictionary<Model.Element, string[]>();

+

+

+    class EltName

+    {

+      public Model.Element For;

+      public int Score;

+      public string Format;

+      public Model.Element[] Arguments;

+      public string Resolved;

+    }

+

+    private void AddName(Model.Element elt, int sc, string fmt, params Model.Element[] args)

+    {

+      List<EltName> l;

+      if (!names.TryGetValue(elt, out l)) {

+        l = new List<EltName>();

+        names.Add(elt, l);

+      }

+      l.Add(new EltName() { Arguments = args, Format = fmt, Score = sc, For = elt });

+    }

+

+    private void AddAnyName(Model.Element elt)

+    {

+      if (names.ContainsKey(elt)) return;

+      var nm = new EltName() { Arguments = new Model.Element[0], Format = string.Format("<{0}>", elt.ToString()), Score = 50, For = elt };

+      var l = new List<EltName>();

+      l.Add(nm);

+      names[elt] = l;

+    }

+

+    private int GetApproxScore(Model.Element e)

+    {

+      EltName n;

+      if (bestNameFor.TryGetValue(e, out n))

+        return n.Score;

+      return 100;

+    }

+

+    private int CompareNames(EltName x, EltName y)

+    {

+      if (x == y) return 0;

+      if (x.Score == y.Score) {

+        if (x.Arguments.Length == y.Arguments.Length)

+          return x.Arguments.Map(GetApproxScore).Sum() - y.Arguments.Map(GetApproxScore).Sum();

+        else

+          return x.Arguments.Length - y.Arguments.Length;

       } else {

-        deref = Image(tp, f_spec_ptr_to);

-        if (deref != null)

-          casted = f_spec_ptr_cast.TryEval(ptrElt, deref);

+        return x.Score - y.Score;

+      }

+    }

+

+

+    private void WorkOutBestNameFor(Model.Element e)

+    {

+      if (bestNameFor.ContainsKey(e)) return;

+      if (!names.ContainsKey(e)) AddAnyName(e);

+      var nm = names[e];

+      nm.Sort(CompareNames);

+      var best = nm[0];

+      bestNameFor[e] = best;

+      foreach (var a in best.Arguments)

+        WorkOutBestNameFor(a);

+      resolutionOrder.Add(best);

+    }

+

+    private void ResolveNames()

+    {

+      var keys = names.Keys.ToArray();

+      foreach (var e in keys)

+        WorkOutBestNameFor(e);

+      var res1 = resolutionOrder.ToArray();

+      foreach (var nm in res1) {

+        var nms = names[nm.For];

+        foreach (var subname in nms.Skip(1)) {

+          subname.Arguments.Iter(WorkOutBestNameFor);

+          resolutionOrder.Add(subname);

+        }

+      }

+

+      foreach (var nm in resolutionOrder) {

+        var s = nm.Format;

+        for (int i = nm.Arguments.Length - 1; i >= 0; --i) {

+          var argName = bestNameFor[nm.Arguments[i]];

+          var strName = argName.Resolved;

+          if (strName == null) strName = argName.For.ToString();

+          s = s.Replace("&" + i, strName);

+        }

+        nm.Resolved = s;

       }

 

-      if (deref != null && casted == null)

-        casted = ptrElt;

-

-      if (casted != null) {

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

-            if (val != null) {

-              yield return new FieldNode(state, ConstantName(fld.Args[1]), val, f_field_type.TryEval(fld.Args[1]));

+      foreach (var e in names) {

+        finalNames[e.Key] = e.Value.Map(n => n.Resolved).ToArray();

+      }

+    }

+

+    public Dictionary<Model.Element,string[]> ComputeNames()

+    {

+      ComputeFields();

+      ComputeLocals();

+      ComputeLiterals();

+      ComputeFieldRefs();

+

+      ResolveNames();

+

+      return finalNames;

+    }

+

+    private void ComputeFieldRefs()

+    {

+      var fieldStateId = new Dictionary<Model.Element, int>();

+      for (int i = 0; i < states.Count; ++i) {

+        var hp = vm.f_heap.TryEval(states[i].state.TryGet("$s"));

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

+          if (!fieldStateId.ContainsKey(fld.Result)) {

+            fieldStateId[fld.Result] = i;

+            foreach (var sel in vm.f_select_value.AppsWithArg(0, fld.Result)) {

+              var val = sel.Result;

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

+              val = vm.WrapForUse(val, ftp);

+              AddName(val, 20, string.Format("&0->&1.{0}", i), sel.Args[1], fld.Args[1]);

             }

           }

         }

       }

     }

-  }

 

+    private void ComputeLiterals()

+    {

+      foreach (var e in model.Elements) {

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

+        if (n != null)

+          AddName(n, 5, n.ToString());

+      }

+    }

+

+    private void ComputeLocals()

+    {

+      var defined = new HashSet<Tuple<Model.Element, string>>();

+      for (int i = 0; i < states.Count; ++i) {

+        foreach (var v in states[i].vars) {

+          var t = Tuple.Create(v.Element, v.Name);

+          if (!defined.Contains(t)) {

+            defined.Add(t);

+            AddName(v.Element, 10, string.Format("{0}.{1}", v.Name, i));

+          }

+        }

+      }

+    }

+

+    private void ComputeFields()

+    {

+      var fields = vm.f_select_field.Apps.Map(a => a.Args[1]).Concat(vm.f_ptr.Apps.Map(a => a.Args[0]));

+      foreach (var f in fields) {

+        foreach (var fn in synthethic_fields) {

+          foreach (var tpl in model.MkFunc(fn, 1).AppsWithResult(f))

+            AddName(f, 5, string.Format("{0}<{1}>", fn.Substring(3), vm.TypeName(tpl.Args[0])));

+        }

+        foreach (var nm in f.Names) {

+          if (nm.Func.Arity == 0) {

+            var n = nm.Func.Name;

+            var idx = n.LastIndexOf('.');

+            if (idx > 0) n = n.Substring(idx + 1);

+            AddName(f, 5, n);

+          }

+        }

+        AddAnyName(f);

+      }

+    }

+

+  }

+  

   class StateNode : IState

   {

     internal Model.CapturedState state;

     string name;

     internal VccModel vm;

-    List<VariableNode> vars = new List<VariableNode>();

-

+    internal List<VariableNode> vars;

+    

     public StateNode(VccModel parent, Model.CapturedState s)

     {

       this.vm = parent;

@@ -150,10 +396,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         }

       }

 

+      SetupVars();

+    }

+

+    void SetupVars()

+    {

+      if (vars != null) return;

+      vars = new List<VariableNode>();

+

       var names = Util.Empty<string>();

 

-      if (parent.states.Count > 0) {

-        var prev = parent.states.Last();

+      if (vm.states.Count > 0) {

+        var prev = vm.states.Last();

         names = prev.vars.Map(v => v.EdgeName);

       }

 

@@ -161,9 +415,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       var curVars = state.Variables.ToDictionary(x => x);

       foreach (var v in names) {

-        if (parent.GetUserVariableName(v) != null) {

-          var vn = new VariableNode(this, v, state.TryGet(v));

-          vn.updatedHere = parent.states.Count > 0 && curVars.ContainsKey(v);

+        if (vm.GetUserVariableName(v) != null) {

+          var tp = vm.LocalType(v);

+          var val = state.TryGet(v);

+          val = vm.WrapForUse(val, tp);

+          var vn = new VariableNode(this, v, val, tp);

+          vn.updatedHere = vm.states.Count > 0 && curVars.ContainsKey(v);

           vars.Add(vn);

         }

       }

@@ -176,7 +433,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public IEnumerable<IDisplayNode> Nodes

     {

-      get { return vars; }

+      get {

+        return vars; 

+      }

     }

 

   }

@@ -198,6 +457,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       this.elt = elt;

     }

 

+    public override Model.Element Element

+    {

+      get

+      {

+        return elt;

+      }

+    }

+

     protected virtual void DoInitChildren()

     {

     }

@@ -222,12 +489,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     {

       get

       {

-        if (!(elt is Model.Uninterpreted))

-          yield return elt.ToString();

-        foreach (var tupl in elt.Names) {

-          if (tupl.Func.Arity == 0)

-            yield return tupl.Func.Name;

-        }

+        return vm.ElementNames(Element);

       }

     }

 

@@ -252,14 +514,17 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public FieldNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

       : base(par, realName, elt, tp)

     {

+      /*

       var idx = realName.LastIndexOf('.');

       if (idx > 0)

         name = realName.Substring(idx + 1);

+       */

     }

 

     protected override void DoInitChildren()

     {

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

+      children.Sort(vm.CompareFields);

     }

   }

 

@@ -268,8 +533,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   {

     public bool updatedHere;

 

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

-      : base(par, realName, elt, par.vm.LocalType(realName))

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

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

     {

       name = vm.GetUserVariableName(realName);

     }

@@ -277,6 +542,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     protected override void DoInitChildren()

     {

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

+      children.Sort(vm.CompareFields);

     }

 

     public override NodeState State