VCC-BVD: display qualifiers of VCC-generated copies of local variables; hide states that do not update "$s" (heap).

Fix some bugs in source view.
Rename SourceLocation to SourceViewState.

5 files changed, 230 insertions, 75 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 7f8e4ae2..1e9e9cf9 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
       nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions));

     }

 

-    public virtual SourceLocation ShowSource()

+    public virtual SourceViewState ShowSource()

     {

       return null;

     }

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index f8a9abf0..74e206aa 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -42,7 +42,7 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<string> SortFields(IEnumerable<IDisplayNode> fields);

   }

 

-  public class SourceLocation

+  public class SourceViewState

   {

     public string Header;

     public string RichTextContent;

@@ -52,7 +52,7 @@ namespace Microsoft.Boogie.ModelViewer
   public interface IState

   {

     string Name { get; }

-    SourceLocation ShowSource();

+    SourceViewState ShowSource();

     IEnumerable<IDisplayNode> Nodes { get; }

   }

 

@@ -104,7 +104,7 @@ namespace Microsoft.Boogie.ModelViewer
     }

 

 

-    public SourceLocation ShowSource()

+    public SourceViewState ShowSource()

     {

       return null;

     }

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index f6858003..5b3bb870 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -18,7 +18,7 @@ namespace Microsoft.Boogie.ModelViewer
     protected Dictionary<Model.Element, string> canonicalName = new Dictionary<Model.Element, string>();

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

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

-    protected Dictionary<string, SourceLocation> sourceLocations = new Dictionary<string, SourceLocation>();

+    protected Dictionary<string, SourceViewState> sourceLocations = new Dictionary<string, SourceViewState>();

     public readonly Model model;

 

     protected virtual bool UseLocalsForCanonicalNames

@@ -246,53 +246,61 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

-    public SourceLocation GetSourceLocation(Model.CapturedState s)

+    public class SourceLocation

     {

-      SourceLocation res;

-      sourceLocations.TryGetValue(s.Name, out res);

+      public string Filename;

+      public string AddInfo;

+      public int Line;

+      public int Column;

+    }

+

+    public SourceViewState GetSourceLocation(string name)

+    {

+      SourceViewState res;

+      sourceLocations.TryGetValue(name, out res);

       return res;

     }

 

     // 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)

+    public virtual SourceLocation TryParseSourceLocation(string name)

     {

-      filename = name;

-      line = 0;

-      column = 0;

-      addInfo = "";

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

+      if (par <= 0) return null;

 

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

-      if (par <= 0) return false;

+      var res = new SourceLocation() { Filename = name.Substring(0, par) };

 

-      filename = name.Substring(0, par);

       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;

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

+

+      if (!int.TryParse(words[0], out res.Line) || !int.TryParse(words[1], out res.Column)) return null;

 

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

       if (colon > 0)

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

+        res.AddInfo = name.Substring(colon + 1).Trim();

+      else

+        res.AddInfo = "";

 

-      return true;

+      return res;

     }

 

     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 loc = TryParseSourceLocation(tok);

+

+      if (loc != null) {

+        var fn = loc.Filename;

         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 = "";

+        var addInfo = addAddInfo ? loc.AddInfo : "";

         if (addInfo != "")

           addInfo = ":" + addInfo;

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

+        return string.Format("{0}({1},{2}){3}", fn, loc.Line, loc.Column, addInfo);

       } else {

         return tok;

       }

@@ -327,23 +335,23 @@ namespace Microsoft.Boogie.ModelViewer
 

     protected virtual void GenerateSourceLocations(IEnumerable<NamedState> states)

     {

-      sourceLocations = new Dictionary<string, SourceLocation>();

+      sourceLocations = new Dictionary<string, SourceViewState>();

 

       var files = new Dictionary<string, List<Position>>();

       var sIdx = -1;

-      foreach (var s in model.States) {

+      

+      foreach (var s in states) {

+        var sn = s.CapturedStateName;

         sIdx++;

-        int line, col;

-        string fn, addInfo;

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

-          continue;

+        var loc = TryParseSourceLocation(sn);

+        if (loc == null) continue;

 

         List<Position> positions;

-        if (!files.TryGetValue(fn, out positions)) {

+        if (!files.TryGetValue(loc.Filename, out positions)) {

           positions = new List<Position>();

-          files[fn] = positions;

+          files[loc.Filename] = positions;

         }

-        positions.Add(new Position() { Name = s.Name, Line = line, Column = col, Index = sIdx });

+        positions.Add(new Position() { Name = sn, Line = loc.Line, Column = loc.Column, Index = sIdx });

       }

 

       foreach (var kv in files) {

@@ -357,38 +365,36 @@ namespace Microsoft.Boogie.ModelViewer
           continue;

         }

 

+        var pos = new Position() { Line = 1, Column = 1 };

         var currPosIdx = 0;

-        var currLine = 1;

-        var currColumn = 1;

-        var output = new StringBuilder();

-        var charPos = 0;

-        RtfAppendLineNo(output, currLine, ref charPos);

+        var output = new StringBuilder();        

+        RtfAppendLineNo(output, pos.Line, ref pos.CharPos);

 

         foreach (var c in content) {

           if (c == '\n') {

-            currColumn = int.MaxValue; // flush remaining positions in this line

+            pos.Column = int.MaxValue; // flush remaining positions in this line

           }

 

-          while (currPosIdx < positions.Count && positions[currPosIdx].Line <= currLine && positions[currPosIdx].Column <= currColumn) {

-            positions[currPosIdx].CharPos = charPos;

-            RtfAppendStateIdx(output, positions[currPosIdx].Index.ToString(), ref charPos);

+          while (currPosIdx < positions.Count && pos.CompareTo(positions[currPosIdx]) >= 0) {

+            positions[currPosIdx].CharPos = pos.CharPos;

+            RtfAppendStateIdx(output, positions[currPosIdx].Index.ToString(), ref pos.CharPos);

             currPosIdx++;

           }

 

-          RtfAppend(output, c, ref charPos);

+          RtfAppend(output, c, ref pos.CharPos);

 

           if (c == '\n') {

-            currLine++;

-            currColumn = 1;

-            RtfAppendLineNo(output, currLine, ref charPos);

+            pos.Line++;

+            pos.Column = 1;

+            RtfAppendLineNo(output, pos.Line, ref pos.CharPos);

           } else {

-            currColumn++;

+            pos.Column++;

           }

         }

 

         var resStr = output.ToString();

-        foreach (var pos in positions) {

-          sourceLocations[pos.Name] = new SourceLocation() { Header = pos.Name, Location = pos.CharPos, RichTextContent = resStr };

+        foreach (var p in positions) {

+          sourceLocations[p.Name] = new SourceViewState() { Header = p.Name, Location = p.CharPos, RichTextContent = resStr };

         }

       }

     }

@@ -419,9 +425,15 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

-    public virtual SourceLocation ShowSource()

+    // by overriding this, one state can masqureade another

+    public virtual string CapturedStateName

+    {

+      get { return State.Name; }

+    }

+

+    public virtual SourceViewState ShowSource()

     {

-      return langModel.GetSourceLocation(state);

+      return langModel.GetSourceLocation(CapturedStateName);

     }

 

     public abstract IEnumerable<IDisplayNode> Nodes { get; }

diff --git a/Source/ModelViewer/SourceView.cs b/Source/ModelViewer/SourceView.cs
index 07c03cd3..32f03b3d 100644
--- a/Source/ModelViewer/SourceView.cs
+++ b/Source/ModelViewer/SourceView.cs
@@ -23,7 +23,7 @@ namespace Microsoft.Boogie.ModelViewer
         @"{\colortbl;\red0\green0\blue0;\red255\green0\blue0;\red0\green255\blue0;\red0\green0\blue255;\red255\green255\blue255;\red100\green100\blue100;}" +

         @"\viewkind4\uc1\pard\f0\fs17 ";

 

-    internal void SetSourceLocation(SourceLocation r)

+    internal void SetSourceLocation(SourceViewState r)

     {      

       if (r.RichTextContent != prevRtf) {

         richTextBox1.Rtf = prefix + r.RichTextContent + "\r\n}\r\n";

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 4395041f..2cd7c383 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -44,6 +44,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

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

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

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

 

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

 

@@ -111,23 +112,117 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           literalName[fn.GetConstant()] = ":" + fn.Name.Substring(2);

       }

 

-      var idx = 0;

-      foreach (var s in m.States) {

-        var elt = s.TryGet("$s");

-        if (elt != null)

-          literalName[elt] = "\\state'" + idx;

-        idx++;

-      }

-

       DecodeFileNames();

+      ComputeLocalVariableNames();

 

       foreach (var s in m.States) {

-        var sn = new StateNode(states.Count, this, s);

+        var sn = new StateNode(this, s);

+        sn.SetupVars();

         states.Add(sn);

       }

+      var allStates = states.ToArray();

+      states.Clear();

+      var i = 0;

+      while (i < allStates.Length) {

+        var bestState = allStates[i];

+        var bestName = TryParseSourceLocation(bestState.State.Name);

+        i++;

+        while (i < allStates.Length) {          

+          if (allStates[i].State.Variables.Contains("$s"))

+            break;          

+          var curName = TryParseSourceLocation(allStates[i].State.Name);

+          if (CompareNames(curName, bestName) < 0) {

+            bestName = curName;

+            bestState = allStates[i];

+          }

+          i++;

+        }

+

+        var lastState = allStates[i - 1];

+        lastState.capturedStateName = bestState.CapturedStateName;

+        lastState.index = states.Count;

+        states.Add(lastState);

+        lastState.SetupVars();

+      }

+

+      foreach (var s in states) {

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

+        if (elt != null)

+          literalName[elt] = "\\state'" + s.index;

+      }

 

       GenerateSourceLocations(states);

     }

+    

+    int NameBadness(SourceLocation l)

+    {

+      if (l == null) return 5;

+      if (l.Filename.StartsWith("<")) return 4;

+      if (l.AddInfo == "") return 3;

+      return 0;

+    }

+

+    int CompareNames(SourceLocation l1, SourceLocation l2)

+    {

+      if (l1 == l2) return 0;

+

+      var res = NameBadness(l1) - NameBadness(l2);

+      if (res != 0)

+        return res;

+

+      res = l1.Line - l2.Line;

+      if (res == 0)

+        res = l1.Column - l2.Column;

+      return res;

+    }

+

+    private void ComputeLocalVariableNames()

+    {

+      var vars = model.States.SelectMany(s => s.Variables).Where(v => v != null).Distinct();

+      Func<string, string> simpleName = s => { string dummy; return GetUserVariableNameCore(s, out dummy); };

+      var userVars = vars.Where(s => simpleName(s) != null);

+      var conflictsName = Conflicts(userVars, simpleName).ToArray();

+      Func<string, string> qName = s => { string kind, n = GetUserVariableNameCore(s, out kind); return n + " (" + kind + ")"; };

+      var conflictsKind = Conflicts(conflictsName, qName).ToArray();

+

+      var conflictsNameH = new HashSet<string>(conflictsName);

+      var conflictsKindH = new HashSet<string>(conflictsKind);

+

+      foreach (var v in userVars) {

+        if (conflictsKindH.Contains(v)) continue;

+        if (conflictsNameH.Contains(v))

+          localVariableNames[v] = qName(v);

+        else

+          localVariableNames[v] = simpleName(v);

+      }

+

+      var idx = 0;

+      foreach (var v in conflictsKind) {

+        localVariableNames[v] = string.Format("{0} #{1}", qName(v), idx++);

+      }

+    }

+

+    static IEnumerable<A> Conflicts<A, B>(IEnumerable<A> input, Func<A, B> f)

+    {

+      var revMap = new Dictionary<B, A>();

+      var reported = new HashSet<A>();

+

+      foreach (var k in input) {

+        if (reported.Contains(k)) continue;

+        var v = f(k);

+        A tmp;

+        if (revMap.TryGetValue(v, out tmp) && !tmp.Equals(k)) {

+          if (!reported.Contains(tmp)) {

+            yield return tmp;

+            reported.Add(tmp);

+          }

+          yield return k;

+          reported.Add(k);

+        } else {

+          revMap[v] = k;

+        }

+      }

+    }

 

     #region Function name scoring

     static string[][] prefixes = new string[][] {

@@ -272,14 +367,48 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public string GetUserVariableName(string name)

     {

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

+      string res;

+      localVariableNames.TryGetValue(name, out res);

+      return res;

+    }

+

+

+    string GetUserVariableNameCore(string name, out string kind)

+    {

+      if (name.StartsWith("L#")) {

+        kind = "local";

         return name.Substring(2);

-      if (name.StartsWith("SL#") || name.StartsWith("SP#"))

+      }

+

+      if (name.StartsWith("P#")) {

+        kind = "in-param";

+        return name.Substring(2);

+      }

+

+      if (name.StartsWith("SL#")) {

+        kind = "spec local";

         return name.Substring(3);

-      if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1)

-        return name;

+      }

+

+      if (name.StartsWith("SP#")) {

+        kind = "spec in-param";

+        return name.Substring(3);

+      }

+

+      if (name.StartsWith("local.")) {

+        kind = "param copied to local";

+        return name.Substring(6);

+      }

+

+      if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {

+        kind = "call result";

+        return name; 

+      }

+

+      kind = null;

       return null;

     }

+    

 

     private string LiteralName(Model.Element elt)

     {

@@ -299,7 +428,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public Model.Element LocalType(string localName)

     {

-      var v = GetUserVariableName(localName);

+      string dummy;

+      var v = GetUserVariableNameCore(localName, out dummy);

       if (v == null) v = localName;

       var c = model.TryGetFunc("#loc." + v);

       if (c != null) {

@@ -307,7 +437,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         if (localIs != null)

           return localIs.Args[4];

       }

-      return f_mathint.GetConstant();

+      foreach (var s in model.States.Reverse()) {

+        var val = s.TryGet(localName);

+        var tp = GuessType(val);

+        if (tp != tp_mathint)

+          return tp;

+      }

+      return tp_mathint;

     }

 

     public Model.Element Image(Model.Element elt, Model.Func f)

@@ -911,18 +1047,17 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     internal VccModel vm;

     internal List<VariableNode> vars;

     internal List<ElementNode> commons;

-    internal int index;    

+    internal int index;

+    internal string capturedStateName;

     

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

+    public StateNode(VccModel parent, Model.CapturedState s)

       : base(s, parent)

     {

+      this.capturedStateName = s.Name;

       this.vm = parent;

-      index = i;

-

-      SetupVars();

     }

 

-    void SetupVars()

+    internal void SetupVars()

     {

       if (vars != null) return;

       vars = new List<VariableNode>();

@@ -941,7 +1076,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var localName = vm.GetUserVariableName(v);

         if (localName != null) {

           var tp = vm.LocalType(v);

-          var val = state.TryGet(v);

+          var val = state.TryGet(v);          

           val = vm.WrapForUse(val, tp);

           var vn = new VariableNode(this, v, val, tp) { ShortName = localName };

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

@@ -963,6 +1098,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return vars.Concat(commons);

       }

     }

+

+    public override string CapturedStateName

+    {

+      get

+      {

+        return this.capturedStateName;

+      }

+    }

   }

 

   class ElementNode : DisplayNode