Introduce new NamedState base class to reduce code duplication

3 files changed, 76 insertions, 77 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 0a032f06..50783c44 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -187,7 +187,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
           i++;

         }

       }

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

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

       if (heap != null) {

         foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {

           var field = new FieldName(tpl.Args[2], this);

@@ -255,35 +255,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     }

   }

 

-  class StateNode : IState

+  class StateNode : NamedState

   {

-    internal readonly Model.CapturedState state;

-    readonly string name;

     internal readonly DafnyModel dm;

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

     internal readonly int index;

     

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

+       : base(s, parent)

     {

       dm = parent;

       state = s;

       index = i;

 

-      name = s.Name;

-      var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

-      if (0 <= idx)

-        name = name.Substring(idx + 1);

-      var limit = 30;

-      if (name.Length > limit) {

-        idx = name.IndexOf('(');

-        if (idx > 0) {

-          var prefLen = limit - (name.Length - idx);

-          if (prefLen > 2) {

-            name = name.Substring(0,prefLen) + ".." + name.Substring(idx);

-          }

-        }

-      }

-

       SetupVars();

     }

 

@@ -313,23 +297,12 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       dm.Flush(vars);

     }

 

-    public string Name

-    {

-      get { return name; }

-    }

-

-    public IEnumerable<IDisplayNode> Nodes

+    public override IEnumerable<IDisplayNode> Nodes

     {

       get {

         return vars; 

       }

     }

-

-    public SourceLocation ShowSource()

-    {

-      return dm.GetSourceLocation(state);

-    }

-

   }

 

   class ElementNode : DisplayNode

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 749eb274..621f3837 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -153,6 +153,7 @@ namespace Microsoft.Boogie.ModelViewer
         addList(n.Children);

       }

     }

+

     #region field name sorting

     /*

     static bool HasSpecialChars(string s)

@@ -230,8 +231,6 @@ namespace Microsoft.Boogie.ModelViewer
     }

     #endregion

 

-

-

     #region Displaying source code

     class Position : IComparable<Position>

     {

@@ -258,23 +257,50 @@ namespace Microsoft.Boogie.ModelViewer
       return res;

     }

 

-    protected virtual bool TryParseSourceLocation(string name, out string filename, out int line, out int column)

+    // example parsed token: @"c:\users\foo\bar.c(12,10) : random string"

+    // the ": random string" part is optional

+    public virtual bool TryParseSourceLocation(string name, out string filename, out int line, out int column, out string addInfo)

     {

       filename = name;

       line = 0;

       column = 0;

+      addInfo = "";

 

       var par = name.LastIndexOf('(');      

       if (par <= 0) return false;

 

       filename = name.Substring(0, par);

-      var words = name.Substring(par + 1).Split(',', ')').Where(x => x != "").ToArray();

-      if (words.Length != 2) return false;

+      var words = name.Substring(par + 1).Split(',', ')', ':').Where(x => x != "").ToArray();

+      if (words.Length < 2) return false;

       if (!int.TryParse(words[0], out line) || !int.TryParse(words[1], out column)) return false;

 

+      var colon = name.IndexOf(':', par);

+      if (colon > 0)

+        addInfo = name.Substring(colon).Trim();

+

       return true;

     }

 

+    static char[] dirSeps = new char[] { '\\', '/' };

+    public virtual string ShortenToken(string tok, int fnLimit, bool addAddInfo)

+    {

+      string fn, addInfo;

+      int line, col;

+      if (TryParseSourceLocation(tok, out fn, out line, out col, out addInfo)) {

+        var idx = fn.LastIndexOfAny(dirSeps);

+        if (idx > 0)

+          fn = fn.Substring(idx + 1);

+        if (fn.Length > fnLimit) {

+          fn = fn.Substring(0, fnLimit) + "..";

+        }

+        if (!addAddInfo) addInfo = "";

+        if (addInfo != "")

+          addInfo = ":" + addInfo;

+        return string.Format("{0}({1},{2}){3}", fn, line, col, addInfo);

+      } else {

+        return tok;

+      }

+    }

 

     protected virtual void RtfAppend(StringBuilder sb, char c, ref int pos)

     {

@@ -312,8 +338,8 @@ namespace Microsoft.Boogie.ModelViewer
       foreach (var s in model.States) {

         sIdx++;

         int line, col;

-        string fn;

-        if (!TryParseSourceLocation(s.Name, out fn, out line, out col))

+        string fn, addInfo;

+        if (!TryParseSourceLocation(s.Name, out fn, out line, out col, out addInfo))

           continue;

 

         List<Position> positions;

@@ -373,6 +399,38 @@ namespace Microsoft.Boogie.ModelViewer
     #endregion

   }

 

+  public abstract class NamedState : IState

+  {

+    protected Model.CapturedState state;

+    private LanguageModel langModel; // no point making it protected - they will need VccModel, DafnyModel

+

+    public NamedState(Model.CapturedState s, LanguageModel lm)

+    {

+      this.state = s;

+      this.langModel = lm;

+    }

+

+    public Model.CapturedState State

+    {

+      get { return state; }

+    }

+

+    public virtual string Name

+    {

+      get

+      {

+        return langModel.ShortenToken(state.Name, 20, true);

+      }

+    }

+

+    public virtual SourceLocation ShowSource()

+    {

+      return langModel.GetSourceLocation(state);

+    }

+

+    public abstract IEnumerable<IDisplayNode> Nodes { get; }

+  }

+

   public class EdgeName

   {

     static readonly Model.Element[] emptyArgs = new Model.Element[0];

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 58395385..ff7c6626 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -547,7 +547,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     {

       if (elt == null) return;

 

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

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

       if (map != null)

         map = select_map.TryEval(map);

       if (map != null) {

@@ -601,7 +601,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           var baseName = f.Name.Substring(0, f.Name.LastIndexOf('$'));

           if (baseName.StartsWith("Q#"))

             baseName = baseName.Substring(2);

-          return string.Format("{0}@{1}", baseName, ShortenToken(tok, 10));

+          return string.Format("{0}@{1}", baseName, ShortenToken(tok, 10, false));

         }

       } else if (f.Name.StartsWith("G#")) {

         var idx = f.Name.LastIndexOf("#dt");

@@ -665,7 +665,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       var kind = GetKind(tp, out tpl);

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

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

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

         if (heap != null)

           heap = f_heap.TryEval(heap);

         var addresses = new HashSet<Model.Element>();

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

 

       if (elt != null && !(elt is Model.Boolean)) {

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

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

         

         foreach (var tupl in elt.References) {

           if (!tupl.Args.Contains(elt)) continue; // not looking for aliases (maybe we should?)

@@ -902,41 +902,20 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       return sb.ToString();

     }

-

-    internal string ShortenToken(string name, int limit)

-    {

-      var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

-      if (idx > 0)

-        name = name.Substring(idx + 1);

-      if (name.Length > limit) {

-        idx = name.IndexOf('(');

-        if (idx > 0) {

-          var prefLen = limit - (name.Length - idx);

-          if (prefLen > 2) {

-            name = name.Substring(0, prefLen) + ".." + name.Substring(idx);

-          }

-        }

-      }

-      return name;

-    }

-

   }

 

-  class StateNode : IState

+  class StateNode : NamedState

   {

-    internal Model.CapturedState state;

-    string name;

     internal VccModel vm;

     internal List<VariableNode> vars;

     internal List<ElementNode> commons;

     internal int index;    

     

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

+      : base(s, parent)

     {

       this.vm = parent;

-      state = s;

       index = i;

-      name = parent.ShortenToken(s.Name, 30);

 

       SetupVars();

     }

@@ -976,23 +955,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       commons.AddRange(vm.CommonNodes(this));

     } 

 

-    public string Name

-    {

-      get { return name; }

-    }

-

-    public IEnumerable<IDisplayNode> Nodes

+    public override IEnumerable<IDisplayNode> Nodes

     {

       get {

         return vars.Concat(commons);

       }

     }

-

-    public SourceLocation ShowSource()

-    {

-      return vm.GetSourceLocation(state);

-    }

-

   }

 

   class ElementNode : DisplayNode