summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/Namer.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ModelViewer/Namer.cs')
-rw-r--r--Source/ModelViewer/Namer.cs1160
1 files changed, 580 insertions, 580 deletions
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 0eb2418e..3adf0a11 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -1,580 +1,580 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Numerics;
-
-namespace Microsoft.Boogie.ModelViewer
-{
- public enum NameSeqSuffix
- {
- None,
- WhenNonZero,
- Always
- }
-
- public abstract class LanguageModel : ILanguageSpecificModel
- {
- protected Dictionary<string, int> baseNameUse = new Dictionary<string, int>();
- 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, SourceViewState> sourceLocations = new Dictionary<string, SourceViewState>();
- public readonly Model model;
-
- protected virtual bool UseLocalsForCanonicalNames
- {
- get { return false; }
- }
-
- public readonly ViewOptions viewOpts;
- public LanguageModel(Model model, ViewOptions opts)
- {
- this.model = model;
- viewOpts = opts;
- }
-
- public string AsPow2(Model.Integer elt)
- {
- var n = BigInteger.Parse(elt.Numeral);
- var pow = new BigInteger(4096*4);
- var k = 14;
- var neg = false;
-
- if (n < 0) {
- n = -n;
- neg = true;
- }
-
- while (k < 150) {
- var diff = pow / 1000;
- if (pow - diff < n && n < pow + diff) {
- diff = n - pow;
- var res = string.Format("2^{0}{1}{2}", k, diff >= 0 ? "+" : "", diff);
- if (neg) res = "-(" + res + ")";
- return res;
- }
- if (n < pow) break;
- k++;
- pow *= 2;
- }
-
- return elt.ToString();
- }
-
- // Elements (other than integers and Booleans) get canonical names of the form
- // "<base>'<idx>", where <base> is returned by this function, and <idx> is given
- // starting with 0, and incrementing when there are conflicts between bases.
- //
- // This function needs to return an appropriate base name for the element. It is given
- // the element.
- //
- // A reasonable strategy is to check if it's a name of the local, and if so return it,
- // and otherwise use the type of element (e.g., return "seq" for elements representing
- // sequences). It is also possible to return "" in such cases.
- //
- // The suff output parameter specifies whether the number sequence suffix should be
- // always added, only when it's non-zero, or never.
- protected virtual string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
- {
- string res;
- if (elt is Model.Integer || elt is Model.Boolean) {
- suff = NameSeqSuffix.None;
- return elt.ToString();
- }
- suff = NameSeqSuffix.Always;
- if (UseLocalsForCanonicalNames) {
- if (localValue.TryGetValue(elt, out res))
- return res;
- }
- return "";
- }
-
- public virtual void RegisterLocalValue(string name, Model.Element elt)
- {
- string curr;
- if (localValue.TryGetValue(elt, out curr) && CompareFieldNames(name, curr) >= 0)
- return;
- localValue[elt] = name;
- }
-
- protected virtual string AppendSuffix(string baseName, int id)
- {
- return baseName + "'" + id.ToString();
- }
-
- 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);
- if (baseName == "")
- suff = NameSeqSuffix.Always;
-
- if (viewOpts.DebugMode && !(elt is Model.Boolean) && !(elt is Model.Number)) {
- baseName += string.Format("({0})", elt);
- suff = NameSeqSuffix.WhenNonZero;
- }
-
- int cnt;
- if (!baseNameUse.TryGetValue(baseName, out cnt))
- cnt = -1;
- cnt++;
-
- if (suff == NameSeqSuffix.Always || (cnt > 0 && suff == NameSeqSuffix.WhenNonZero))
- res = AppendSuffix(baseName, cnt);
- else
- res = baseName;
-
- baseNameUse[baseName] = cnt;
- canonicalName.Add(elt, res);
- invCanonicalName[res.Replace(" ", "")] = elt;
- return res;
- }
-
- public virtual Model.Element FindElement(string canonicalName)
- {
- Model.Element res;
- if (invCanonicalName.TryGetValue(canonicalName.Replace(" ", ""), out res))
- return res;
- return null;
- }
-
- public virtual string PathName(IEnumerable<IDisplayNode> path)
- {
- return path.Select(n => n.Name).Concat(".");
- }
-
- public abstract IEnumerable<IState> States { get; }
-
- /// <summary>
- /// Walks each input tree in BFS order, and force evaluation of Name and Value properties
- /// (to get reasonable numbering of canonical values).
- /// </summary>
- public void Flush(IEnumerable<IDisplayNode> roots)
- {
- var workList = new Queue<IDisplayNode>();
-
- Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>
- {
- var ch = new Dictionary<string, IDisplayNode>();
- foreach (var x in nodes) {
- if (ch.ContainsKey(x.Name)) {
- // throw new System.InvalidOperationException("duplicated model entry: " + x.Name);
- }
- ch[x.Name] = x;
- }
- foreach (var k in SortFields(nodes))
- workList.Enqueue(ch[k]);
- };
-
- addList(roots);
-
- var visited = new HashSet<Model.Element>();
- while (workList.Count > 0) {
- var n = workList.Dequeue();
-
- var dummy1 = n.Name;
- var dummy2 = n.Value;
-
- if (n.Element != null) {
- if (visited.Contains(n.Element))
- continue;
- visited.Add(n.Element);
- }
-
- addList(n.Children);
- }
- }
-
- #region field name sorting
- /*
- static bool HasSpecialChars(string s)
- {
- for (int i = 0; i < s.Length; ++i)
- switch (s[i]) {
- case '[':
- case '<':
- case '>':
- case ']':
- case '#':
- case '\\':
- case '(':
- case ')':
- return true;
- }
- return false;
- }
- */
-
- static ulong GetNumber(string s, int beg)
- {
- ulong res = 0;
- while (beg < s.Length) {
- var c = s[beg];
- if ('0' <= c && c <= '9') {
- res *= 10;
- res += (uint)c - (uint)'0';
- }
- beg++;
- }
- return res;
- }
-
- public virtual int CompareFieldNames(string f1, string f2)
- {
- /*
- bool s1 = HasSpecialChars(f1);
- bool s2 = HasSpecialChars(f2);
- if (s1 && !s2)
- return 1;
- if (!s1 && s2)
- return -1; */
- var len = Math.Min(f1.Length, f2.Length);
- var numberPos = -1;
- for (int i = 0; i < len; ++i) {
- var c1 = f1[i];
- var c2 = f2[i];
- if ('0' <= c1 && c1 <= '9' && '0' <= c2 && c2 <= '9') {
- numberPos = i;
- break;
- }
- if (c1 != c2)
- break;
- }
-
- if (numberPos >= 0) {
- var v1 = GetNumber(f1, numberPos);
- var v2 = GetNumber(f2, numberPos);
-
- if (v1 < v2) return -1;
- else if (v1 > v2) return 1;
- }
-
- return string.CompareOrdinal(f1, f2);
- }
-
- public virtual int CompareFields(IDisplayNode n1, IDisplayNode n2)
- {
- var diff = (int)n1.Category - (int)n2.Category;
- if (diff != 0) return diff;
- else return CompareFieldNames(n1.Name, n2.Name);
- }
-
- public virtual IEnumerable<string> SortFields(IEnumerable<IDisplayNode> fields_)
- {
- var fields = new List<IDisplayNode>(fields_);
- fields.Sort(CompareFields);
- return fields.Select(f => f.Name);
- }
- #endregion
-
- #region Displaying source code
- class Position : IComparable<Position>
- {
- public int Line, Column, Index;
- public int CharPos;
- public string Name;
-
- public int CompareTo(Position other)
- {
- if (this.Line == other.Line)
- return this.Column - other.Column;
- return this.Line - other.Line;
- }
- }
-
- public class SourceLocation
- {
- 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 SourceLocation TryParseSourceLocation(string name)
- {
- var par = name.LastIndexOf('(');
- if (par <= 0) return null;
-
- var res = new SourceLocation() { Filename = name.Substring(0, par) };
-
- var words = name.Substring(par + 1).Split(',', ')', ':').Where(x => x != "").ToArray();
- 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)
- res.AddInfo = name.Substring(colon + 1).Trim();
- else
- res.AddInfo = "";
-
- return res;
- }
-
- static char[] dirSeps = new char[] { '\\', '/' };
- public virtual string ShortenToken(string tok, int fnLimit, bool addAddInfo)
- {
- 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) + "..";
- }
- var addInfo = addAddInfo ? loc.AddInfo : "";
- if (addInfo != "")
- addInfo = ":" + addInfo;
- return string.Format("{0}({1},{2}){3}", fn, loc.Line, loc.Column, addInfo);
- } else {
- return tok;
- }
- }
-
- protected virtual void RtfAppend(StringBuilder sb, char c, ref int pos)
- {
- pos++;
- switch (c) {
- case '\r': pos--; break;
- case '\\': sb.Append("\\\\"); break;
- case '\n': sb.Append("\\par\n"); break;
- case '{': sb.Append("\\{"); break;
- case '}': sb.Append("\\}"); break;
- default: sb.Append(c); break;
- }
- }
-
- protected virtual void RtfAppendStateIdx(StringBuilder sb, string label, ref int pos)
- {
- label += ".";
- pos += label.Length;
- sb.Append(@"{\sub\cf5\highlight4 ").Append(label).Append("}");
- }
-
- protected virtual void RtfAppendLineNo(StringBuilder sb, int num, ref int pos)
- {
- string n = string.Format("{0:0000}: ", num);
- pos += n.Length;
- sb.Append(@"{\cf6 ").Append(n).Append("}");
- }
-
- protected virtual void GenerateSourceLocations(IEnumerable<NamedState> states)
- {
- sourceLocations = new Dictionary<string, SourceViewState>();
-
- var files = new Dictionary<string, List<Position>>();
- var sIdx = -1;
-
- foreach (var s in states) {
- var sn = s.CapturedStateName;
- sIdx++;
- var loc = TryParseSourceLocation(sn);
- if (loc == null) continue;
-
- List<Position> positions;
- if (!files.TryGetValue(loc.Filename, out positions)) {
- positions = new List<Position>();
- files[loc.Filename] = positions;
- }
- positions.Add(new Position() { Name = sn, Line = loc.Line, Column = loc.Column, Index = sIdx });
- }
-
- foreach (var kv in files) {
- var positions = kv.Value;
- positions.Sort();
-
- string content = "";
- if (System.IO.File.Exists(kv.Key)) {
- try {
- content = System.IO.File.ReadAllText(kv.Key);
- } catch {
- continue;
- }
- } else {
- continue;
- }
-
- var pos = new Position() { Line = 1, Column = 1 };
- var currPosIdx = 0;
- var output = new StringBuilder();
- RtfAppendLineNo(output, pos.Line, ref pos.CharPos);
-
- foreach (var c in content) {
- if (c == '\n') {
- pos.Column = int.MaxValue; // flush remaining positions in this line
- }
-
- 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 pos.CharPos);
-
- if (c == '\n') {
- pos.Line++;
- pos.Column = 1;
- RtfAppendLineNo(output, pos.Line, ref pos.CharPos);
- } else {
- pos.Column++;
- }
- }
-
- var resStr = output.ToString();
- foreach (var p in positions) {
- sourceLocations[p.Name] = new SourceViewState() { Header = p.Name, Location = p.CharPos, RichTextContent = resStr };
- }
- }
- }
- #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);
- }
- }
-
- // by overriding this, one state can masqureade another
- public virtual string CapturedStateName
- {
- get { return State.Name; }
- }
-
- public virtual SourceViewState ShowSource()
- {
- return langModel.GetSourceLocation(CapturedStateName);
- }
-
- public abstract IEnumerable<IDisplayNode> Nodes { get; }
- }
-
- public class EdgeName
- {
- ILanguageSpecificModel langModel;
- string format;
- string cachedName;
- Model.Element[] args;
-
- public EdgeName(ILanguageSpecificModel n, string format, params Model.Element[] args)
- {
- this.langModel = n;
- this.format = format;
- this.args = args.ToArray();
- }
-
- public EdgeName(string name) : this(null, name)
- {
- Util.Assert(name != null);
- }
-
- public override string ToString()
- {
- if (cachedName != null)
- return cachedName;
- cachedName = Format();
- return cachedName;
- }
-
- public override int GetHashCode()
- {
- int res = format.GetHashCode();
- foreach (var c in args) {
- res += c.GetHashCode();
- res *= 13;
- }
- return res;
- }
-
- public override bool Equals(object obj)
- {
- EdgeName e = obj as EdgeName;
- if (e == null) return false;
- if (e == this) return true;
- if (e.format != this.format || e.args.Length != this.args.Length)
- return false;
- for (int i = 0; i < this.args.Length; ++i)
- if (this.args[i] != e.args[i])
- return false;
- return true;
- }
-
- protected virtual string Format()
- {
- if (args == null || args.Length == 0)
- return format;
-
- var res = new StringBuilder(format.Length);
- for (int i = 0; i < format.Length; ++i) {
- var c = format[i];
-
- /*
- var canonical = false;
- if (c == '%' && i < format.Length - 1) {
- if (format[i + 1] == 'c') {
- ++i;
- canonical = true;
- }
- }
- */
-
- if (c == '%' && i < format.Length - 1) {
- var j = i + 1;
- while (j < format.Length && char.IsDigit(format[j]))
- j++;
- var len = j - i - 1;
- if (len > 0) {
- var idx = int.Parse(format.Substring(i + 1, len));
- res.Append(langModel.CanonicalName(args[idx]));
- i = j - 1;
- continue;
- }
- }
-
- res.Append(c);
- }
-
- return res.ToString();
- }
-
- public virtual IEnumerable<Model.Element> Dependencies
- {
- get { return args; }
- }
- }
-
-}
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Numerics;
+
+namespace Microsoft.Boogie.ModelViewer
+{
+ public enum NameSeqSuffix
+ {
+ None,
+ WhenNonZero,
+ Always
+ }
+
+ public abstract class LanguageModel : ILanguageSpecificModel
+ {
+ protected Dictionary<string, int> baseNameUse = new Dictionary<string, int>();
+ 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, SourceViewState> sourceLocations = new Dictionary<string, SourceViewState>();
+ public readonly Model model;
+
+ protected virtual bool UseLocalsForCanonicalNames
+ {
+ get { return false; }
+ }
+
+ public readonly ViewOptions viewOpts;
+ public LanguageModel(Model model, ViewOptions opts)
+ {
+ this.model = model;
+ viewOpts = opts;
+ }
+
+ public string AsPow2(Model.Integer elt)
+ {
+ var n = BigInteger.Parse(elt.Numeral);
+ var pow = new BigInteger(4096*4);
+ var k = 14;
+ var neg = false;
+
+ if (n < 0) {
+ n = -n;
+ neg = true;
+ }
+
+ while (k < 150) {
+ var diff = pow / 1000;
+ if (pow - diff < n && n < pow + diff) {
+ diff = n - pow;
+ var res = string.Format("2^{0}{1}{2}", k, diff >= 0 ? "+" : "", diff);
+ if (neg) res = "-(" + res + ")";
+ return res;
+ }
+ if (n < pow) break;
+ k++;
+ pow *= 2;
+ }
+
+ return elt.ToString();
+ }
+
+ // Elements (other than integers and Booleans) get canonical names of the form
+ // "<base>'<idx>", where <base> is returned by this function, and <idx> is given
+ // starting with 0, and incrementing when there are conflicts between bases.
+ //
+ // This function needs to return an appropriate base name for the element. It is given
+ // the element.
+ //
+ // A reasonable strategy is to check if it's a name of the local, and if so return it,
+ // and otherwise use the type of element (e.g., return "seq" for elements representing
+ // sequences). It is also possible to return "" in such cases.
+ //
+ // The suff output parameter specifies whether the number sequence suffix should be
+ // always added, only when it's non-zero, or never.
+ protected virtual string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
+ {
+ string res;
+ if (elt is Model.Integer || elt is Model.Boolean) {
+ suff = NameSeqSuffix.None;
+ return elt.ToString();
+ }
+ suff = NameSeqSuffix.Always;
+ if (UseLocalsForCanonicalNames) {
+ if (localValue.TryGetValue(elt, out res))
+ return res;
+ }
+ return "";
+ }
+
+ public virtual void RegisterLocalValue(string name, Model.Element elt)
+ {
+ string curr;
+ if (localValue.TryGetValue(elt, out curr) && CompareFieldNames(name, curr) >= 0)
+ return;
+ localValue[elt] = name;
+ }
+
+ protected virtual string AppendSuffix(string baseName, int id)
+ {
+ return baseName + "'" + id.ToString();
+ }
+
+ 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);
+ if (baseName == "")
+ suff = NameSeqSuffix.Always;
+
+ if (viewOpts.DebugMode && !(elt is Model.Boolean) && !(elt is Model.Number)) {
+ baseName += string.Format("({0})", elt);
+ suff = NameSeqSuffix.WhenNonZero;
+ }
+
+ int cnt;
+ if (!baseNameUse.TryGetValue(baseName, out cnt))
+ cnt = -1;
+ cnt++;
+
+ if (suff == NameSeqSuffix.Always || (cnt > 0 && suff == NameSeqSuffix.WhenNonZero))
+ res = AppendSuffix(baseName, cnt);
+ else
+ res = baseName;
+
+ baseNameUse[baseName] = cnt;
+ canonicalName.Add(elt, res);
+ invCanonicalName[res.Replace(" ", "")] = elt;
+ return res;
+ }
+
+ public virtual Model.Element FindElement(string canonicalName)
+ {
+ Model.Element res;
+ if (invCanonicalName.TryGetValue(canonicalName.Replace(" ", ""), out res))
+ return res;
+ return null;
+ }
+
+ public virtual string PathName(IEnumerable<IDisplayNode> path)
+ {
+ return path.Select(n => n.Name).Concat(".");
+ }
+
+ public abstract IEnumerable<IState> States { get; }
+
+ /// <summary>
+ /// Walks each input tree in BFS order, and force evaluation of Name and Value properties
+ /// (to get reasonable numbering of canonical values).
+ /// </summary>
+ public void Flush(IEnumerable<IDisplayNode> roots)
+ {
+ var workList = new Queue<IDisplayNode>();
+
+ Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>
+ {
+ var ch = new Dictionary<string, IDisplayNode>();
+ foreach (var x in nodes) {
+ if (ch.ContainsKey(x.Name)) {
+ // throw new System.InvalidOperationException("duplicated model entry: " + x.Name);
+ }
+ ch[x.Name] = x;
+ }
+ foreach (var k in SortFields(nodes))
+ workList.Enqueue(ch[k]);
+ };
+
+ addList(roots);
+
+ var visited = new HashSet<Model.Element>();
+ while (workList.Count > 0) {
+ var n = workList.Dequeue();
+
+ var dummy1 = n.Name;
+ var dummy2 = n.Value;
+
+ if (n.Element != null) {
+ if (visited.Contains(n.Element))
+ continue;
+ visited.Add(n.Element);
+ }
+
+ addList(n.Children);
+ }
+ }
+
+ #region field name sorting
+ /*
+ static bool HasSpecialChars(string s)
+ {
+ for (int i = 0; i < s.Length; ++i)
+ switch (s[i]) {
+ case '[':
+ case '<':
+ case '>':
+ case ']':
+ case '#':
+ case '\\':
+ case '(':
+ case ')':
+ return true;
+ }
+ return false;
+ }
+ */
+
+ static ulong GetNumber(string s, int beg)
+ {
+ ulong res = 0;
+ while (beg < s.Length) {
+ var c = s[beg];
+ if ('0' <= c && c <= '9') {
+ res *= 10;
+ res += (uint)c - (uint)'0';
+ }
+ beg++;
+ }
+ return res;
+ }
+
+ public virtual int CompareFieldNames(string f1, string f2)
+ {
+ /*
+ bool s1 = HasSpecialChars(f1);
+ bool s2 = HasSpecialChars(f2);
+ if (s1 && !s2)
+ return 1;
+ if (!s1 && s2)
+ return -1; */
+ var len = Math.Min(f1.Length, f2.Length);
+ var numberPos = -1;
+ for (int i = 0; i < len; ++i) {
+ var c1 = f1[i];
+ var c2 = f2[i];
+ if ('0' <= c1 && c1 <= '9' && '0' <= c2 && c2 <= '9') {
+ numberPos = i;
+ break;
+ }
+ if (c1 != c2)
+ break;
+ }
+
+ if (numberPos >= 0) {
+ var v1 = GetNumber(f1, numberPos);
+ var v2 = GetNumber(f2, numberPos);
+
+ if (v1 < v2) return -1;
+ else if (v1 > v2) return 1;
+ }
+
+ return string.CompareOrdinal(f1, f2);
+ }
+
+ public virtual int CompareFields(IDisplayNode n1, IDisplayNode n2)
+ {
+ var diff = (int)n1.Category - (int)n2.Category;
+ if (diff != 0) return diff;
+ else return CompareFieldNames(n1.Name, n2.Name);
+ }
+
+ public virtual IEnumerable<string> SortFields(IEnumerable<IDisplayNode> fields_)
+ {
+ var fields = new List<IDisplayNode>(fields_);
+ fields.Sort(CompareFields);
+ return fields.Select(f => f.Name);
+ }
+ #endregion
+
+ #region Displaying source code
+ class Position : IComparable<Position>
+ {
+ public int Line, Column, Index;
+ public int CharPos;
+ public string Name;
+
+ public int CompareTo(Position other)
+ {
+ if (this.Line == other.Line)
+ return this.Column - other.Column;
+ return this.Line - other.Line;
+ }
+ }
+
+ public class SourceLocation
+ {
+ 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 SourceLocation TryParseSourceLocation(string name)
+ {
+ var par = name.LastIndexOf('(');
+ if (par <= 0) return null;
+
+ var res = new SourceLocation() { Filename = name.Substring(0, par) };
+
+ var words = name.Substring(par + 1).Split(',', ')', ':').Where(x => x != "").ToArray();
+ 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)
+ res.AddInfo = name.Substring(colon + 1).Trim();
+ else
+ res.AddInfo = "";
+
+ return res;
+ }
+
+ static char[] dirSeps = new char[] { '\\', '/' };
+ public virtual string ShortenToken(string tok, int fnLimit, bool addAddInfo)
+ {
+ 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) + "..";
+ }
+ var addInfo = addAddInfo ? loc.AddInfo : "";
+ if (addInfo != "")
+ addInfo = ":" + addInfo;
+ return string.Format("{0}({1},{2}){3}", fn, loc.Line, loc.Column, addInfo);
+ } else {
+ return tok;
+ }
+ }
+
+ protected virtual void RtfAppend(StringBuilder sb, char c, ref int pos)
+ {
+ pos++;
+ switch (c) {
+ case '\r': pos--; break;
+ case '\\': sb.Append("\\\\"); break;
+ case '\n': sb.Append("\\par\n"); break;
+ case '{': sb.Append("\\{"); break;
+ case '}': sb.Append("\\}"); break;
+ default: sb.Append(c); break;
+ }
+ }
+
+ protected virtual void RtfAppendStateIdx(StringBuilder sb, string label, ref int pos)
+ {
+ label += ".";
+ pos += label.Length;
+ sb.Append(@"{\sub\cf5\highlight4 ").Append(label).Append("}");
+ }
+
+ protected virtual void RtfAppendLineNo(StringBuilder sb, int num, ref int pos)
+ {
+ string n = string.Format("{0:0000}: ", num);
+ pos += n.Length;
+ sb.Append(@"{\cf6 ").Append(n).Append("}");
+ }
+
+ protected virtual void GenerateSourceLocations(IEnumerable<NamedState> states)
+ {
+ sourceLocations = new Dictionary<string, SourceViewState>();
+
+ var files = new Dictionary<string, List<Position>>();
+ var sIdx = -1;
+
+ foreach (var s in states) {
+ var sn = s.CapturedStateName;
+ sIdx++;
+ var loc = TryParseSourceLocation(sn);
+ if (loc == null) continue;
+
+ List<Position> positions;
+ if (!files.TryGetValue(loc.Filename, out positions)) {
+ positions = new List<Position>();
+ files[loc.Filename] = positions;
+ }
+ positions.Add(new Position() { Name = sn, Line = loc.Line, Column = loc.Column, Index = sIdx });
+ }
+
+ foreach (var kv in files) {
+ var positions = kv.Value;
+ positions.Sort();
+
+ string content = "";
+ if (System.IO.File.Exists(kv.Key)) {
+ try {
+ content = System.IO.File.ReadAllText(kv.Key);
+ } catch {
+ continue;
+ }
+ } else {
+ continue;
+ }
+
+ var pos = new Position() { Line = 1, Column = 1 };
+ var currPosIdx = 0;
+ var output = new StringBuilder();
+ RtfAppendLineNo(output, pos.Line, ref pos.CharPos);
+
+ foreach (var c in content) {
+ if (c == '\n') {
+ pos.Column = int.MaxValue; // flush remaining positions in this line
+ }
+
+ 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 pos.CharPos);
+
+ if (c == '\n') {
+ pos.Line++;
+ pos.Column = 1;
+ RtfAppendLineNo(output, pos.Line, ref pos.CharPos);
+ } else {
+ pos.Column++;
+ }
+ }
+
+ var resStr = output.ToString();
+ foreach (var p in positions) {
+ sourceLocations[p.Name] = new SourceViewState() { Header = p.Name, Location = p.CharPos, RichTextContent = resStr };
+ }
+ }
+ }
+ #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);
+ }
+ }
+
+ // by overriding this, one state can masqureade another
+ public virtual string CapturedStateName
+ {
+ get { return State.Name; }
+ }
+
+ public virtual SourceViewState ShowSource()
+ {
+ return langModel.GetSourceLocation(CapturedStateName);
+ }
+
+ public abstract IEnumerable<IDisplayNode> Nodes { get; }
+ }
+
+ public class EdgeName
+ {
+ ILanguageSpecificModel langModel;
+ string format;
+ string cachedName;
+ Model.Element[] args;
+
+ public EdgeName(ILanguageSpecificModel n, string format, params Model.Element[] args)
+ {
+ this.langModel = n;
+ this.format = format;
+ this.args = args.ToArray();
+ }
+
+ public EdgeName(string name) : this(null, name)
+ {
+ Util.Assert(name != null);
+ }
+
+ public override string ToString()
+ {
+ if (cachedName != null)
+ return cachedName;
+ cachedName = Format();
+ return cachedName;
+ }
+
+ public override int GetHashCode()
+ {
+ int res = format.GetHashCode();
+ foreach (var c in args) {
+ res += c.GetHashCode();
+ res *= 13;
+ }
+ return res;
+ }
+
+ public override bool Equals(object obj)
+ {
+ EdgeName e = obj as EdgeName;
+ if (e == null) return false;
+ if (e == this) return true;
+ if (e.format != this.format || e.args.Length != this.args.Length)
+ return false;
+ for (int i = 0; i < this.args.Length; ++i)
+ if (this.args[i] != e.args[i])
+ return false;
+ return true;
+ }
+
+ protected virtual string Format()
+ {
+ if (args == null || args.Length == 0)
+ return format;
+
+ var res = new StringBuilder(format.Length);
+ for (int i = 0; i < format.Length; ++i) {
+ var c = format[i];
+
+ /*
+ var canonical = false;
+ if (c == '%' && i < format.Length - 1) {
+ if (format[i + 1] == 'c') {
+ ++i;
+ canonical = true;
+ }
+ }
+ */
+
+ if (c == '%' && i < format.Length - 1) {
+ var j = i + 1;
+ while (j < format.Length && char.IsDigit(format[j]))
+ j++;
+ var len = j - i - 1;
+ if (len > 0) {
+ var idx = int.Parse(format.Substring(i + 1, len));
+ res.Append(langModel.CanonicalName(args[idx]));
+ i = j - 1;
+ continue;
+ }
+ }
+
+ res.Append(c);
+ }
+
+ return res.ToString();
+ }
+
+ public virtual IEnumerable<Model.Element> Dependencies
+ {
+ get { return args; }
+ }
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 07:40:45 +0000